Merge pull request #396 from andreamattavelli/fix_kleaver_parser

Fixed bug #375 in Kleaver's parser and added --clear-array-decls-after-query option to Kleaver.

4 files changed, 258 insertions, 24 deletions

diff --git a/include/expr/Parser.h b/include/expr/Parser.h
index d2135f12..a9133e9d 100644
--- a/include/expr/Parser.h
+++ b/include/expr/Parser.h
@@ -228,9 +228,8 @@ namespace expr {
     /// \arg MB - The input data.
     /// \arg Builder - The expression builder to use for constructing
     /// expressions.
-    static Parser *Create(const std::string Name,
-                          const llvm::MemoryBuffer *MB,
-                          ExprBuilder *Builder);
+    static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB,
+                          ExprBuilder *Builder, bool ClearArrayAfterQuery);
   };
 }
 }
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index e914cb80..572b9572 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -111,6 +111,7 @@ namespace {
     const MemoryBuffer *TheMemoryBuffer;
     ExprBuilder *Builder;
     ArrayCache TheArrayCache;
+    bool ClearArrayAfterQuery;
 
     Lexer TheLexer;
     unsigned MaxErrors;
@@ -322,14 +323,11 @@ namespace {
     void Error(const char *Message) { Error(Message, Tok); }
 
   public:
-    ParserImpl(const std::string _Filename,
-               const MemoryBuffer *MB,
-               ExprBuilder *_Builder) : Filename(_Filename),
-                                        TheMemoryBuffer(MB),
-                                        Builder(_Builder),
-                                        TheLexer(MB),
-                                        MaxErrors(~0u),
-                                        NumErrors(0) {}
+    ParserImpl(const std::string _Filename, const MemoryBuffer *MB,
+               ExprBuilder *_Builder, bool _ClearArrayAfterQuery)
+        : Filename(_Filename), TheMemoryBuffer(MB), Builder(_Builder),
+          ClearArrayAfterQuery(_ClearArrayAfterQuery), TheLexer(MB),
+          MaxErrors(~0u), NumErrors(0) {}
 
     virtual ~ParserImpl();
 
@@ -492,9 +490,9 @@ DeclResult ParserImpl::ParseArrayDecl() {
       Values.clear();
     }
 
-    for (unsigned i = 0; i != Size.get(); ++i) {
-      // FIXME: Must be constant expression.
-    }
+    // for (unsigned i = 0; i != Size.get(); ++i) {
+    // TODO: Check: Must be constant expression.
+    //}
   }
 
   // FIXME: Validate that size makes sense for domain type.
@@ -532,7 +530,7 @@ DeclResult ParserImpl::ParseArrayDecl() {
   ArrayDecl *AD = new ArrayDecl(Label, Size.get(), 
                                 DomainType.get(), RangeType.get(), Root);
 
-  ArraySymTab.insert(std::make_pair(Label, AD));
+  ArraySymTab[Label] = AD;
 
   // Create the initial version reference.
   VersionSymTab.insert(std::make_pair(Label,
@@ -681,7 +679,13 @@ DeclResult ParserImpl::ParseQueryCommand() {
 
  exit:
   if (Tok.kind != Token::EndOfFile)
-    ExpectRParen("unexpected argument to 'query'.");  
+    ExpectRParen("unexpected argument to 'query'.");
+
+  // If we assume that the queries are independent, we clear the array
+  // table from the previous declarations
+  if (ClearArrayAfterQuery)
+    ArraySymTab.clear();
+
   return new QueryCommand(Constraints, Res.get(), Values, Objects);
 }
 
@@ -1641,10 +1645,9 @@ Parser::Parser() {
 Parser::~Parser() {
 }
 
-Parser *Parser::Create(const std::string Filename,
-                       const MemoryBuffer *MB,
-                       ExprBuilder *Builder) {
-  ParserImpl *P = new ParserImpl(Filename, MB, Builder);
+Parser *Parser::Create(const std::string Filename, const MemoryBuffer *MB,
+                       ExprBuilder *Builder, bool ClearArrayAfterQuery) {
+  ParserImpl *P = new ParserImpl(Filename, MB, Builder, ClearArrayAfterQuery);
   P->Initialize();
   return P;
 }
diff --git a/test/Solver/2016-04-12-array-parsing-bug.kquery b/test/Solver/2016-04-12-array-parsing-bug.kquery
new file mode 100644
index 00000000..d53fa35f
--- /dev/null
+++ b/test/Solver/2016-04-12-array-parsing-bug.kquery
@@ -0,0 +1,227 @@
+# RUN: %kleaver %s > %t
+# RUN: %kleaver --clear-array-decls-after-query %s > %t
+
+array A-data[8] : w32 -> w8 = symbolic
+array A-data-stat[144] : w32 -> w8 = symbolic
+array arg0[3] : w32 -> w8 = symbolic
+array arg1[3] : w32 -> w8 = symbolic
+array const_arr1[768] : w32 -> w8 = [0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 3 32 2 32 2 32 2 32 2 32 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 1 96 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 213 8 213 8 213 8 213 8 213 8 213 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 4 192 4 192 4 192 4 192 4 192 4 192 8 214 8 214 8 214 8 214 8 214 8 214 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 4 192 4 192 4 192 4 192 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0]
+array const_arr8[277] : w32 -> w8 = [0 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 24 2 2 25 2 2 2 2 2 2 2 2 2 2 23 2 2 2 2 2 22 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21]
+array model_version[4] : w32 -> w8 = symbolic
+array n_args[4] : w32 -> w8 = symbolic
+array n_args_1[4] : w32 -> w8 = symbolic
+array stdin[8] : w32 -> w8 = symbolic
+array stdin-stat[144] : w32 -> w8 = symbolic
+array stdout[1024] : w32 -> w8 = symbolic
+array stdout-stat[144] : w32 -> w8 = symbolic
+(query [(Ult N0:(ReadLSB w32 0 n_args)
+              2)
+         (Eq false (Slt 0 N0))
+         (Ult N1:(ReadLSB w32 0 n_args_1)
+              3)
+         (Slt 0 N1)
+         (Slt 1 N1)
+         (Eq false
+             (Eq 0
+                 (And w64 (ReadLSB w64 8 A-data-stat)
+                          2147483647)))
+         (Ult (ReadLSB w64 56 A-data-stat)
+              65536)
+         (Eq false
+             (Eq 0
+                 (And w64 (ReadLSB w64 8 stdin-stat)
+                          2147483647)))
+         (Ult (ReadLSB w64 56 stdin-stat)
+              65536)
+         (Eq false
+             (Eq 0
+                 (And w64 (ReadLSB w64 8 stdout-stat)
+                          2147483647)))
+         (Ult (ReadLSB w64 56 stdout-stat)
+              65536)
+         (Eq 1
+             (ReadLSB w32 0 model_version))
+         (Eq 45 (Read w8 0 arg0))
+         (Eq false
+             (Eq 0 N2:(Read w8 1 arg0)))
+         (Eq false (Eq 45 N2))
+         (Eq 100
+             (AShr w32 (Shl w32 (SExt w32 N2) 24)
+                       24))
+         (Eq 0
+             (And w16 (ReadLSB w16 N3:(Extract w32 0 (Add w64 256
+                                                              (Mul w64 2
+                                                                       (ZExt w64 N4:(Read w8 0 arg1))))) const_arr1)
+                      8192))
+         (Eq false (Eq 84 N4))
+         (Eq false
+             (Ult (Add w64 18446744073664565360
+                           N5:(Select w64 (Eq 0 N4) 44986256 51741584))
+                  2))
+         (Eq false
+             (Ult (Add w32 4294967248
+                           (ZExt w32 N6:(Read w8 (Extract w32 0 (Add w64 18446744073657810032 N5))
+                                                 U0:[2=0] @ arg1)))
+                  10))
+         (Eq false (Eq 45 N6))
+         (Eq false (Eq 43 N6))
+         (Eq 0
+             (And w16 (ReadLSB w16 N7:(Extract w32 0 (Add w64 256
+                                                              (Mul w64 2 (ZExt w64 N6)))) const_arr1)
+                      1024))
+         (Eq false (Eq 40 N6))
+         (Eq false
+             (Slt N8:(SExt w32 N6) 1))
+         (Ult 96
+              (Add w32 4294967286
+                       (ZExt w32 (Read w8 (Extract w32 0 (SExt w64 N8))
+                                          const_arr8))))
+         (Eq 7 (Read w8 0 U0))
+         (Eq 13 (Read w8 1 U0))]
+        false []
+        [n_args
+         n_args_1
+         arg0
+         arg1
+         A-data
+         A-data-stat
+         stdin
+         stdin-stat
+         stdout
+         stdout-stat
+         model_version])
+
+array A-data[8] : w32 -> w8 = symbolic
+array A-data-stat[144] : w32 -> w8 = symbolic
+array arg0[11] : w32 -> w8 = symbolic
+array arg1[3] : w32 -> w8 = symbolic
+array model_version[4] : w32 -> w8 = symbolic
+array n_args[4] : w32 -> w8 = symbolic
+array n_args_1[4] : w32 -> w8 = symbolic
+array stdin[8] : w32 -> w8 = symbolic
+array stdin-stat[144] : w32 -> w8 = symbolic
+array stdout[1024] : w32 -> w8 = symbolic
+array stdout-stat[144] : w32 -> w8 = symbolic
+(query [(Ult N0:(ReadLSB w32 0 n_args)
+              2)
+         (Slt 0 N0)
+         (Ult N1:(ReadLSB w32 0 n_args_1)
+              3)
+         (Slt 0 N1)
+         (Eq false (Slt 1 N1))
+         (Eq false
+             (Eq 0
+                 (And w64 (ReadLSB w64 8 A-data-stat)
+                          2147483647)))
+         (Ult (ReadLSB w64 56 A-data-stat)
+              65536)
+         (Eq false
+             (Eq 0
+                 (And w64 (ReadLSB w64 8 stdin-stat)
+                          2147483647)))
+         (Ult (ReadLSB w64 56 stdin-stat)
+              65536)
+         (Eq false
+             (Eq 0
+                 (And w64 (ReadLSB w64 8 stdout-stat)
+                          2147483647)))
+         (Ult (ReadLSB w64 56 stdout-stat)
+              65536)
+         (Eq 1
+             (ReadLSB w32 0 model_version))
+         (Eq 45 (Read w8 0 arg0))
+         (Eq 45 (Read w8 1 arg0))
+         (Eq 61 (Read w8 3 arg0))
+         (Eq 116 (Read w8 2 arg0))
+         (Eq false
+             (Eq 0 (Read w8 4 arg0)))
+         (Eq false
+             (Eq 0
+                 N2:(Read w8 7 U0:[10=0] @ arg0)))
+         (Eq 0 (Read w8 8 U0))
+         (Eq 11 (Read w8 4 U0))
+         (Eq 63 (Read w8 5 U0))
+         (Eq 8 (Read w8 6 U0))
+         (Eq false (Eq 39 N2))
+         (Or (Eq 122 N2)
+             (Or (Eq 121 N2)
+                 (Or (Eq 120 N2)
+                     (Or (Eq 119 N2)
+                         (Or (Eq 118 N2)
+                             (Or (Eq 117 N2)
+                                 (Or (Eq 116 N2)
+                                     (Or (Eq 115 N2)
+                                         (Or (Eq 114 N2)
+                                             (Or (Eq 113 N2)
+                                                 (Or (Eq 112 N2)
+                                                     (Or (Eq 111 N2)
+                                                         (Or (Eq 110 N2)
+                                                             (Or (Eq 109 N2)
+                                                                 (Or (Eq 108 N2)
+                                                                     (Or (Eq 107 N2)
+                                                                         (Or (Eq 106 N2)
+                                                                             (Or (Eq 105 N2)
+                                                                                 (Or (Eq 104 N2)
+                                                                                     (Or (Eq 103 N2)
+                                                                                         (Or (Eq 102 N2)
+                                                                                             (Or (Eq 101 N2)
+                                                                                                 (Or (Eq 100 N2)
+                                                                                                     (Or (Eq 99 N2)
+                                                                                                         (Or (Eq 98 N2)
+                                                                                                             (Or (Eq 97 N2)
+                                                                                                                 (Or (Eq 95 N2)
+                                                                                                                     (Or (Eq 93 N2)
+                                                                                                                         (Or (Eq 90 N2)
+                                                                                                                             (Or (Eq 89 N2)
+                                                                                                                                 (Or (Eq 88 N2)
+                                                                                                                                     (Or (Eq 87 N2)
+                                                                                                                                         (Or (Eq 86 N2)
+                                                                                                                                             (Or (Eq 85 N2)
+                                                                                                                                                 (Or (Eq 84 N2)
+                                                                                                                                                     (Or (Eq 83 N2)
+                                                                                                                                                         (Or (Eq 82 N2)
+                                                                                                                                                             (Or (Eq 81 N2)
+                                                                                                                                                                 (Or (Eq 80 N2)
+                                                                                                                                                                     (Or (Eq 79 N2)
+                                                                                                                                                                         (Or (Eq 78 N2)
+                                                                                                                                                                             (Or (Eq 77 N2)
+                                                                                                                                                                                 (Or (Eq 76 N2)
+                                                                                                                                                                                     (Or (Eq 75 N2)
+                                                                                                                                                                                         (Or (Eq 74 N2)
+                                                                                                                                                                                             (Or (Eq 73 N2)
+                                                                                                                                                                                                 (Or (Eq 72 N2)
+                                                                                                                                                                                                     (Or (Eq 71 N2)
+                                                                                                                                                                                                         (Or (Eq 70 N2)
+                                                                                                                                                                                                             (Or (Eq 69 N2)
+                                                                                                                                                                                                                 (Or (Eq 68 N2)
+                                                                                                                                                                                                                     (Or (Eq 67 N2)
+                                                                                                                                                                                                                         (Or (Eq 66 N2)
+                                                                                                                                                                                                                             (Or (Eq 65 N2)
+                                                                                                                                                                                                                                 (Or (Eq 58 N2)
+                                                                                                                                                                                                                                     (Or (Eq 57 N2)
+                                                                                                                                                                                                                                         (Or (Eq 56 N2)
+                                                                                                                                                                                                                                             (Or (Eq 55 N2)
+                                                                                                                                                                                                                                                 (Or (Eq 54 N2)
+                                                                                                                                                                                                                                                     (Or (Eq 53 N2)
+                                                                                                                                                                                                                                                         (Or (Eq 52 N2)
+                                                                                                                                                                                                                                                             (Or (Eq 51 N2)
+                                                                                                                                                                                                                                                                 (Or (Eq 50 N2)
+                                                                                                                                                                                                                                                                     (Or (Eq 49 N2)
+                                                                                                                                                                                                                                                                         (Or (Eq 48 N2)
+                                                                                                                                                                                                                                                                             (Or (Eq 47 N2)
+                                                                                                                                                                                                                                                                                 (Or (Eq 46 N2)
+                                                                                                                                                                                                                                                                                     (Or (Eq 45 N2)
+                                                                                                                                                                                                                                                                                         (Or (Eq 44 N2)
+                                                                                                                                                                                                                                                                                             (Or (Eq 43 N2) (Eq 37 N2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))]
+        false []
+        [n_args
+         arg0
+         n_args_1
+         arg1
+         A-data
+         A-data-stat
+         stdin
+         stdin-stat
+         stdout
+         stdout-stat
+         model_version])
\ No newline at end of file
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 9c374eb8..a937d761 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -95,6 +95,11 @@ namespace {
   llvm::cl::opt<std::string> directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."),
 		                                               llvm::cl::init("."));
 
+  llvm::cl::opt<bool> ClearArrayAfterQuery(
+      "clear-array-decls-after-query",
+      llvm::cl::desc("We discard the previous array declarations after a query "
+                     "is performed. Default: false"),
+      llvm::cl::init(false));
 }
 
 static std::string getQueryLogPath(const char filename[])
@@ -160,7 +165,7 @@ static bool PrintInputAST(const char *Filename,
                           const MemoryBuffer *MB,
                           ExprBuilder *Builder) {
   std::vector<Decl*> Decls;
-  Parser *P = Parser::Create(Filename, MB, Builder);
+  Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery);
   P->SetMaxErrors(20);
 
   unsigned NumQueries = 0;
@@ -193,7 +198,7 @@ static bool EvaluateInputAST(const char *Filename,
                              const MemoryBuffer *MB,
                              ExprBuilder *Builder) {
   std::vector<Decl*> Decls;
-  Parser *P = Parser::Create(Filename, MB, Builder);
+  Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery);
   P->SetMaxErrors(20);
   while (Decl *D = P->ParseTopLevelDecl()) {
     Decls.push_back(D);
@@ -327,8 +332,8 @@ static bool printInputAsSMTLIBv2(const char *Filename,
 {
 	//Parse the input file
 	std::vector<Decl*> Decls;
-	Parser *P = Parser::Create(Filename, MB, Builder);
-	P->SetMaxErrors(20);
+        Parser *P = Parser::Create(Filename, MB, Builder, ClearArrayAfterQuery);
+        P->SetMaxErrors(20);
 	while (Decl *D = P->ParseTopLevelDecl())
 	{
 		Decls.push_back(D);