From 6f290d8f9e9d7faac295cb51fc96884a18f4ded4 Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Thu, 21 May 2009 04:36:41 +0000 Subject: 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 --- unittests/Expr/ExprTest.cpp | 112 +++++++++++++++++++++++++++ unittests/Expr/Makefile | 11 +++ unittests/Makefile | 18 +++++ unittests/Solver/Makefile | 11 +++ unittests/Solver/SolverTest.cpp | 164 ++++++++++++++++++++++++++++++++++++++++ unittests/TestMain.cpp | 15 ++++ 6 files changed, 331 insertions(+) create mode 100644 unittests/Expr/ExprTest.cpp create mode 100644 unittests/Expr/Makefile create mode 100755 unittests/Makefile create mode 100644 unittests/Solver/Makefile create mode 100644 unittests/Solver/SolverTest.cpp create mode 100644 unittests/TestMain.cpp (limited to 'unittests') 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 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(0, 32), + SubExpr::create(ref(10, 32), + ref(10, 32))); +} + +TEST(ExprTest, ConcatExtract) { + Array *array = new Array(0, 1, 256); + ref read8 = Expr::createTempRead(array, 8); + Array *array2 = new Array(0, 2, 256); + ref read8_2 = Expr::createTempRead(array2, 8); + ref c100 = getConstant(100, 8); + + ref 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 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 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 extract3 = ExtractExpr::create(concat1, 24, 1); + EXPECT_EQ(Expr::Extract, extract3.getKind()); + + ref extract4 = ExtractExpr::create(concat1, 27, 2); + EXPECT_EQ(Expr::Extract, extract4.getKind()); + const ExtractExpr* tmp = dyn_ref_cast(extract4); + EXPECT_EQ(3U, tmp->offset); + EXPECT_EQ(2U, tmp->getWidth()); + + ref extract5 = ExtractExpr::create(concat1, 17, 5); + EXPECT_EQ(Expr::Extract, extract5.getKind()); + + ref 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 concat10 = ConcatExpr::create4(read8, c100, c100, read8); + ref extract10 = ExtractExpr::create(concat10, 8, 16); + EXPECT_EQ(Expr::Constant, extract10.getKind()); +} + +TEST(ExprTest, ExtractConcat) { + Array *array = new Array(0, 3, 256); + ref read64 = Expr::createTempRead(array, 64); + + Array *array2 = new Array(0, 4, 256); + ref read8_2 = Expr::createTempRead(array2, 8); + + ref extract1 = ExtractExpr::create(read64, 36, 4); + ref extract2 = ExtractExpr::create(read64, 32, 4); + + ref extract3 = ExtractExpr::create(read64, 12, 3); + ref extract4 = ExtractExpr::create(read64, 10, 2); + ref extract5 = ExtractExpr::create(read64, 2, 8); + + ref kids1[6] = { extract1, extract2, + read8_2, + extract3, extract4, extract5 }; + ref concat1 = ConcatExpr::createN(6, kids1); + EXPECT_EQ(29U, concat1.getWidth()); + + ref extract6 = ExtractExpr::create(read8_2, 2, 5); + ref extract7 = ExtractExpr::create(read8_2, 1, 1); + + ref kids2[3] = { extract1, extract6, extract7 }; + ref 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 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 +void testOperation(Solver &solver, + int value, + Expr::Width operandWidth, + Expr::Width resultWidth) { + std::vector 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 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 partiallyConstantArgs(symbolicArgs); + for (unsigned i = 0; i < T::numKids; i++) + if (i==kid) + partiallyConstantArgs[i] = getConstant(value, operandWidth); + + ref expr = + NotOptimizedExpr::create(EqExpr::create(partiallyConstantArgs[kid].expr, + symbolicArgs[kid].expr)); + + ref partiallyConstantExpr = + Expr::createFromKind(T::kind, partiallyConstantArgs); + + ref 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 +void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true, + unsigned maxWidth = 64) { + for (unsigned j=0; j maxWidth) continue; + + for (unsigned i=0; i(solver, value, type, type); + continue; + } + + for (unsigned k=0; k= + Expr::getMinBytesForWidth(resultType)) + continue; + } + + testOperation(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(*solver); + testOpcode(*solver); + testOpcode(*solver); + + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver, false, true, 8); + testOpcode(*solver, false, false, 8); + testOpcode(*solver, false, false, 8); + testOpcode(*solver, false, false, 8); + testOpcode(*solver, false, false, 8); + testOpcode(*solver, false); + testOpcode(*solver, false); + testOpcode(*solver, false); + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver); + + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*solver); + testOpcode(*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(); +} -- cgit 1.4.1