Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


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

6 files changed, 331 insertions, 0 deletions

diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp
new file mode 100644
index 00000000..9220c53e
--- /dev/null
+++ b/unittests/Expr/ExprTest.cpp
@@ -0,0 +1,112 @@
+//===-- ExprTest.cpp ------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "gtest/gtest.h"
+
+#include "klee/Expr.h"
+
+using namespace klee;
+
+namespace {
+
+ref<Expr> getConstant(int value, Expr::Width width) {
+  int64_t ext = value;
+  uint64_t trunc = ext & (((uint64_t) -1LL) >> (64 - width));
+  return ConstantExpr::create(trunc, width);
+}
+
+TEST(ExprTest, BasicConstruction) {
+  EXPECT_EQ(ref<Expr>(0, 32),
+            SubExpr::create(ref<Expr>(10, 32),
+                            ref<Expr>(10, 32)));
+}
+
+TEST(ExprTest, ConcatExtract) {
+  Array *array = new Array(0, 1, 256);
+  ref<Expr> read8 = Expr::createTempRead(array, 8);
+  Array *array2 = new Array(0, 2, 256);
+  ref<Expr> read8_2 = Expr::createTempRead(array2, 8);
+  ref<Expr> c100 = getConstant(100, 8);
+
+  ref<Expr> concat1 = ConcatExpr::create4(read8, read8, c100, read8_2);
+  EXPECT_EQ(2U, concat1.getNumKids());
+  EXPECT_EQ(2U, concat1.getKid(1).getNumKids());
+  EXPECT_EQ(2U, concat1.getKid(1).getKid(1).getNumKids());
+
+  ref<Expr> extract1 = ExtractExpr::create(concat1, 8, 16);
+  EXPECT_EQ(Expr::Concat, extract1.getKind());
+  EXPECT_EQ(read8, extract1.getKid(0));
+  EXPECT_EQ(c100, extract1.getKid(1));
+
+  ref<Expr> extract2 = ExtractExpr::create(concat1, 6, 26);
+  EXPECT_EQ( Expr::Concat, extract2.getKind());
+  EXPECT_EQ( read8, extract2.getKid(0));
+  EXPECT_EQ( Expr::Concat, extract2.getKid(1).getKind());
+  EXPECT_EQ( read8, extract2.getKid(1).getKid(0));
+  EXPECT_EQ( Expr::Concat, extract2.getKid(1).getKid(1).getKind());
+  EXPECT_EQ( c100, extract2.getKid(1).getKid(1).getKid(0));
+  EXPECT_EQ( Expr::Extract, extract2.getKid(1).getKid(1).getKid(1).getKind());
+  
+  ref<Expr> extract3 = ExtractExpr::create(concat1, 24, 1);
+  EXPECT_EQ(Expr::Extract, extract3.getKind());
+
+  ref<Expr> extract4 = ExtractExpr::create(concat1, 27, 2);
+  EXPECT_EQ(Expr::Extract, extract4.getKind());
+  const ExtractExpr* tmp = dyn_ref_cast<ExtractExpr>(extract4);
+  EXPECT_EQ(3U, tmp->offset);
+  EXPECT_EQ(2U, tmp->getWidth());
+
+  ref<Expr> extract5 = ExtractExpr::create(concat1, 17, 5);
+  EXPECT_EQ(Expr::Extract, extract5.getKind());
+
+  ref<Expr> extract6 = ExtractExpr::create(concat1, 3, 26);
+  EXPECT_EQ(Expr::Concat, extract6.getKind());
+  EXPECT_EQ(Expr::Extract, extract6.getKid(0).getKind());
+  EXPECT_EQ(Expr::Concat, extract6.getKid(1).getKind());
+  EXPECT_EQ(read8, extract6.getKid(1).getKid(0));
+  EXPECT_EQ(Expr::Concat, extract6.getKid(1).getKid(1).getKind());
+  EXPECT_EQ(c100, extract6.getKid(1).getKid(1).getKid(0));
+  EXPECT_EQ(Expr::Extract, extract6.getKid(1).getKid(1).getKid(1).getKind());
+
+  ref<Expr> concat10 = ConcatExpr::create4(read8, c100, c100, read8);    
+  ref<Expr> extract10 = ExtractExpr::create(concat10, 8, 16);
+  EXPECT_EQ(Expr::Constant, extract10.getKind());
+}
+
+TEST(ExprTest, ExtractConcat) {
+  Array *array = new Array(0, 3, 256);
+  ref<Expr> read64 = Expr::createTempRead(array, 64);
+
+  Array *array2 = new Array(0, 4, 256);
+  ref<Expr> read8_2 = Expr::createTempRead(array2, 8);
+  
+  ref<Expr> extract1 = ExtractExpr::create(read64, 36, 4);
+  ref<Expr> extract2 = ExtractExpr::create(read64, 32, 4);
+  
+  ref<Expr> extract3 = ExtractExpr::create(read64, 12, 3);
+  ref<Expr> extract4 = ExtractExpr::create(read64, 10, 2);
+  ref<Expr> extract5 = ExtractExpr::create(read64, 2, 8);
+   
+  ref<Expr> kids1[6] = { extract1, extract2,
+			 read8_2,
+			 extract3, extract4, extract5 };
+  ref<Expr> concat1 = ConcatExpr::createN(6, kids1);
+  EXPECT_EQ(29U, concat1.getWidth());
+  
+  ref<Expr> extract6 = ExtractExpr::create(read8_2, 2, 5);
+  ref<Expr> extract7 = ExtractExpr::create(read8_2, 1, 1);
+  
+  ref<Expr> kids2[3] = { extract1, extract6, extract7 };
+  ref<Expr> concat2 = ConcatExpr::createN(3, kids2);
+  EXPECT_EQ(10U, concat2.getWidth());
+  EXPECT_EQ(Expr::Extract, concat2.getKid(0).getKind());
+  EXPECT_EQ(Expr::Extract, concat2.getKid(1).getKind());
+}
+
+}
diff --git a/unittests/Expr/Makefile b/unittests/Expr/Makefile
new file mode 100644
index 00000000..14945b1a
--- /dev/null
+++ b/unittests/Expr/Makefile
@@ -0,0 +1,11 @@
+##===- unittests/Expr/Makefile -----------------------------*- Makefile -*-===##
+
+LEVEL := ../..
+TESTNAME := Expr
+USEDLIBS := kleaverExpr.a kleeBasic.a
+LINK_COMPONENTS := support
+
+include $(LEVEL)/Makefile.config
+include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
+
+LIBS += -lstp 
diff --git a/unittests/Makefile b/unittests/Makefile
new file mode 100755
index 00000000..545d7fa7
--- /dev/null
+++ b/unittests/Makefile
@@ -0,0 +1,18 @@
+##===- unittests/Makefile ----------------------------------*- Makefile -*-===##
+
+LEVEL = ..
+
+include $(LEVEL)/Makefile.config
+
+LIBRARYNAME = UnitTestMain
+BUILD_ARCHIVE = 1
+CPP.Flags += -I$(LLVM_SRC_ROOT)/utils/unittest/googletest/include/
+CPP.Flags += -Wno-variadic-macros
+
+# FIXME: Parallel dirs is broken?
+DIRS = Expr Solver
+
+include $(LEVEL)/Makefile.common
+
+clean::
+	$(Verb) $(RM) -f *Tests
diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile
new file mode 100644
index 00000000..583025fb
--- /dev/null
+++ b/unittests/Solver/Makefile
@@ -0,0 +1,11 @@
+##===- unittests/Solver/Makefile ---------------------------*- Makefile -*-===##
+
+LEVEL := ../..
+TESTNAME := Solver
+USEDLIBS := kleaverSolver.a kleaverExpr.a kleeSupport.a kleeBasic.a
+LINK_COMPONENTS := support
+
+include $(LEVEL)/Makefile.config
+include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
+
+LIBS += -lstp 
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
new file mode 100644
index 00000000..1b1e0f3f
--- /dev/null
+++ b/unittests/Solver/SolverTest.cpp
@@ -0,0 +1,164 @@
+//===-- SolverTest.cpp ----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "gtest/gtest.h"
+
+#include "klee/Constraints.h"
+#include "klee/Expr.h"
+#include "klee/Solver.h"
+
+using namespace klee;
+
+namespace {
+
+const int g_constants[] = { -1, 1, 4, 17, 0 };
+const Expr::Width g_types[] = { Expr::Bool,
+				Expr::Int8,
+				Expr::Int16,
+				Expr::Int32,
+				Expr::Int64 };
+
+ref<Expr> getConstant(int value, Expr::Width width) {
+  int64_t ext = value;
+  uint64_t trunc = ext & (((uint64_t) -1LL) >> (64 - width));
+  return ConstantExpr::create(trunc, width);
+}
+
+
+template<class T>
+void testOperation(Solver &solver,
+                   int value,
+                   Expr::Width operandWidth,
+                   Expr::Width resultWidth) {
+  std::vector<Expr::CreateArg> symbolicArgs;
+  
+  for (unsigned i = 0; i < T::numKids; i++) {
+    if (!T::isValidKidWidth(i, operandWidth))
+      return;
+
+    unsigned size = Expr::getMinBytesForWidth(operandWidth);
+    static unsigned id = 0;
+    Array *array = new Array(0, ++id, size);
+    symbolicArgs.push_back(Expr::CreateArg(Expr::createTempRead(array, 
+                                                                operandWidth)));
+  }
+  
+  if (T::needsResultType())
+    symbolicArgs.push_back(Expr::CreateArg(resultWidth));
+  
+  ref<Expr> fullySymbolicExpr = Expr::createFromKind(T::kind, symbolicArgs);
+
+  // For each kid, replace the kid with a constant value and verify
+  // that the fully symbolic expression is equivalent to it when the
+  // replaced value is appropriated constrained.
+  for (unsigned kid = 0; kid < T::numKids; kid++) {
+    std::vector<Expr::CreateArg> partiallyConstantArgs(symbolicArgs);
+    for (unsigned i = 0; i < T::numKids; i++)
+      if (i==kid)
+        partiallyConstantArgs[i] = getConstant(value, operandWidth);
+
+    ref<Expr> expr = 
+      NotOptimizedExpr::create(EqExpr::create(partiallyConstantArgs[kid].expr,
+                                              symbolicArgs[kid].expr));
+    
+    ref<Expr> partiallyConstantExpr =
+      Expr::createFromKind(T::kind, partiallyConstantArgs);
+    
+    ref<Expr> queryExpr = EqExpr::create(fullySymbolicExpr, 
+                                         partiallyConstantExpr);
+    
+    ConstraintManager constraints;
+    constraints.addConstraint(expr);
+    bool res;
+    bool success = solver.mustBeTrue(Query(constraints, queryExpr), res);
+    EXPECT_EQ(true, success) << "Constraint solving failed";
+
+    if (success) {
+      EXPECT_EQ(true, res) << "Evaluation failed!\n" 
+                           << "query " << queryExpr 
+                           << " with " << expr;
+    }
+  }
+}
+
+template<class T>
+void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true, 
+                unsigned maxWidth = 64) {
+  for (unsigned j=0; j<sizeof(g_types)/sizeof(g_types[0]); j++) {
+    Expr::Width type = g_types[j]; 
+
+    if (type > maxWidth) continue;
+
+    for (unsigned i=0; i<sizeof(g_constants)/sizeof(g_constants[0]); i++) {
+      int value = g_constants[i];
+      if (!tryZero && !value) continue;
+      if (type == Expr::Bool && !tryBool) continue;
+
+      if (!T::needsResultType()) {
+        testOperation<T>(solver, value, type, type);
+        continue;
+      }
+
+      for (unsigned k=0; k<sizeof(g_types)/sizeof(g_types[0]); k++) {
+        Expr::Width resultType = g_types[k];
+          
+        // nasty hack to give only Trunc/ZExt/SExt the right types
+        if (T::kind == Expr::SExt || T::kind == Expr::ZExt) {
+          if (Expr::getMinBytesForWidth(type) >= 
+              Expr::getMinBytesForWidth(resultType)) 
+            continue;
+        }
+            
+        testOperation<T>(solver, value, type, resultType);
+      }
+    }
+  }
+}
+
+TEST(SolverTest, Evaluation) {
+  STPSolver *stpSolver = new STPSolver(true); 
+  Solver *solver = stpSolver;
+
+  solver = createCexCachingSolver(solver);
+  solver = createCachingSolver(solver);
+  solver = createIndependentSolver(solver);
+
+  testOpcode<SelectExpr>(*solver);
+  testOpcode<ZExtExpr>(*solver);
+  testOpcode<SExtExpr>(*solver);
+  
+  testOpcode<AddExpr>(*solver);
+  testOpcode<SubExpr>(*solver);
+  testOpcode<MulExpr>(*solver, false, true, 8);
+  testOpcode<SDivExpr>(*solver, false, false, 8);
+  testOpcode<UDivExpr>(*solver, false, false, 8);
+  testOpcode<SRemExpr>(*solver, false, false, 8);
+  testOpcode<URemExpr>(*solver, false, false, 8);
+  testOpcode<ShlExpr>(*solver, false);
+  testOpcode<LShrExpr>(*solver, false);
+  testOpcode<AShrExpr>(*solver, false);
+  testOpcode<AndExpr>(*solver);
+  testOpcode<OrExpr>(*solver);
+  testOpcode<XorExpr>(*solver);
+
+  testOpcode<EqExpr>(*solver);
+  testOpcode<NeExpr>(*solver);
+  testOpcode<UltExpr>(*solver);
+  testOpcode<UleExpr>(*solver);
+  testOpcode<UgtExpr>(*solver);
+  testOpcode<UgeExpr>(*solver);
+  testOpcode<SltExpr>(*solver);
+  testOpcode<SleExpr>(*solver);
+  testOpcode<SgtExpr>(*solver);
+  testOpcode<SgeExpr>(*solver);
+
+  delete solver;
+}
+
+}
diff --git a/unittests/TestMain.cpp b/unittests/TestMain.cpp
new file mode 100644
index 00000000..095076b2
--- /dev/null
+++ b/unittests/TestMain.cpp
@@ -0,0 +1,15 @@
+//===--- unittests/TestMain.cpp - unittest driver -------------------------===//
+//
+//                     The LLVM Compiler Infrastructure
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "gtest/gtest.h"
+
+int main(int argc, char **argv) {
+  testing::InitGoogleTest(&argc, argv);
+  return RUN_ALL_TESTS();
+}