Add evaluation support to kleaver (now the default).

 - Currently only handles validity queries.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72933 91177308-0d34-0410-b5e6-96231b3b80d8

4 files changed, 80 insertions, 5 deletions

diff --git a/test/Expr/Evaluate.pc b/test/Expr/Evaluate.pc
new file mode 100644
index 00000000..354b0489
--- /dev/null
+++ b/test/Expr/Evaluate.pc
@@ -0,0 +1,13 @@
+# RUN: %kleaver -evaluate %s > %t.log
+
+# RUN: grep "Query 0:	INVALID" %t.log
+# Query 0
+(query [] (Not (Ult (ReadLSB w32 0 arr65)
+                    16)))
+
+# RUN: grep "Query 1:	VALID" %t.log
+# Query 1
+(query [(Eq N0:(ReadLSB w32 0 arr1) 10)
+        (Eq N1:(ReadLSB w32 4 arr1) 20)]
+       (Eq (Add w32 N0 N1)
+           30))
\ No newline at end of file
diff --git a/test/Expr/dg.exp b/test/Expr/dg.exp
index 879685ca..94fc4df8 100644
--- a/test/Expr/dg.exp
+++ b/test/Expr/dg.exp
@@ -1,3 +1,3 @@
 load_lib llvm.exp
 
-RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{ll,llx,c,cpp,tr}]]
+RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]]
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 283b5bef..0bb184bb 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -11,7 +11,7 @@ LEVEL=../..
 TOOLNAME = kleaver
 # FIXME: Ideally we wouldn't have any LLVM dependencies here, which
 # means kicking out klee's Support.
-USEDLIBS = kleaverExpr.a kleaverSolver.a kleeSupport.a kleeBasic.a
+USEDLIBS = kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
 LINK_COMPONENTS = support
 
 include $(LEVEL)/Makefile.common
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 621776ee..7c437e47 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -1,6 +1,7 @@
 #include "expr/Lexer.h"
 #include "expr/Parser.h"
 
+#include "klee/Constraints.h"
 #include "klee/Expr.h"
 #include "klee/Solver.h"
 #include "klee/util/ExprPPrinter.h"
@@ -27,17 +28,20 @@ namespace {
 
   enum ToolActions {
     PrintTokens,
-    PrintAST
+    PrintAST,
+    Evaluate
   };
 
   static llvm::cl::opt<ToolActions> 
   ToolAction(llvm::cl::desc("Tool actions:"),
-             llvm::cl::init(PrintTokens),
+             llvm::cl::init(Evaluate),
              llvm::cl::values(
              clEnumValN(PrintTokens, "print-tokens",
                         "Print tokens from the input file."),
              clEnumValN(PrintAST, "print-ast",
                         "Print parsed AST nodes from the input file."),
+             clEnumValN(Evaluate, "evaluate",
+                        "Print parsed AST nodes from the input file."),
              clEnumValEnd));
 }
 
@@ -50,7 +54,9 @@ static std::string escapedString(const char *start, unsigned length) {
     } else if (c == '\n') {
       s << "\\n";
     } else {
-      s << "\\x" << hexdigit(((unsigned char) c >> 4) & 0xF) << hexdigit((unsigned char) c & 0xF);
+      s << "\\x" 
+        << hexdigit(((unsigned char) c >> 4) & 0xF) 
+        << hexdigit((unsigned char) c & 0xF);
     }
   }
   return s.str();
@@ -89,6 +95,58 @@ static bool PrintInputAST(const char *Filename,
   return success;
 }
 
+static bool EvaluateInputAST(const char *Filename,
+                          const MemoryBuffer *MB) {
+  std::vector<Decl*> Decls;
+  Parser *P = Parser::Create(Filename, MB);
+  P->SetMaxErrors(20);
+  while (Decl *D = P->ParseTopLevelDecl()) {
+    Decls.push_back(D);
+  }
+
+  bool success = true;
+  if (unsigned N = P->GetNumErrors()) {
+    llvm::cerr << Filename << ": parse failure: "
+               << N << " errors.\n";
+    success = false;
+  }
+  delete P;
+
+  // FIXME: Support choice of solver.
+  Solver *S, *STP = new STPSolver(true);
+  S = createCexCachingSolver(STP);
+  S = createCachingSolver(S);
+  S = createIndependentSolver(S);
+
+  unsigned Index = 0;
+  for (std::vector<Decl*>::iterator it = Decls.begin(),
+         ie = Decls.end(); it != ie; ++it) {
+    Decl *D = *it;
+    if (QueryCommand *QC = dyn_cast<QueryCommand>(D)) {
+      llvm::cout << "Query " << Index << ":\t";
+
+      assert(QC->Values.empty() && QC->Objects.empty() && 
+             "FIXME: Support counterexample query commands!");
+      bool result;
+      if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
+                        result)) {
+        llvm::cout << (result ? "VALID" : "INVALID");
+      } else {
+        llvm::cout << "FAIL";
+      }
+
+      llvm::cout << "\n";
+      ++Index;
+    }
+
+    delete D;
+  }
+
+  delete S;
+
+  return success;
+}
+
 int main(int argc, char **argv) {
   bool success = true;
 
@@ -109,6 +167,10 @@ int main(int argc, char **argv) {
   case PrintAST:
     success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB);
     break;
+  case Evaluate:
+    success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(),
+                               MB);
+    break;
   default:
     llvm::cerr << argv[0] << ": ERROR: Unknown program action!\n";
   }