From 96b77a4a211745cdee375b38ce4313dfc70efe8f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 29 Sep 2016 21:04:27 +0100 Subject: Fix bug in `AssignmentEvaluator` where NotOptimizedExpr would not (#466) * Add unittest to check that the `Assignment` class can evaluate expressions containing a `NotOptimizedExpr`. * Fix the `AssignmentTest.FoldNotOptimized` unit test by teaching the `ExprEvaluator` to fold `NotOptimizedExpr` nodes. --- unittests/Assignment/AssignmentTest.cpp | 35 +++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 unittests/Assignment/AssignmentTest.cpp (limited to 'unittests/Assignment/AssignmentTest.cpp') diff --git a/unittests/Assignment/AssignmentTest.cpp b/unittests/Assignment/AssignmentTest.cpp new file mode 100644 index 00000000..0eaa28f1 --- /dev/null +++ b/unittests/Assignment/AssignmentTest.cpp @@ -0,0 +1,35 @@ +#include "klee/util/ArrayCache.h" +#include "klee/util/Assignment.h" +#include "gtest/gtest.h" +#include +#include + +int finished = 0; + +using namespace klee; + +TEST(AssignmentTest, FoldNotOptimized) +{ + ArrayCache ac; + const Array* array = ac.CreateArray("simple_array", /*size=*/ 1); + // Create a simple assignment + std::vector objects; + std::vector value; + std::vector< std::vector > values; + objects.push_back(array); + value.push_back(128); + values.push_back(value); + // We want to simplify to a constant so allow free values so + // if the assignment is incomplete we don't get back a constant. + Assignment assignment(objects, values, /*_allowFreeValues=*/true); + + // Now make an expression that reads from the array at position + // zero. + ref read = NotOptimizedExpr::alloc(Expr::createTempRead(array, Expr::Int8)); + + // Now evaluate. The OptimizedExpr should be folded + ref evaluated = assignment.evaluate(read); + const ConstantExpr* asConstant = dyn_cast(evaluated); + ASSERT_TRUE(asConstant != NULL); + ASSERT_EQ(asConstant->getZExtValue(), (unsigned) 128); +} -- cgit v1.2.3