From 96b77a4a211745cdee375b38ce4313dfc70efe8f Mon Sep 17 00:00:00 2001
From: Dan Liew <delcypher@gmail.com>
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 +++++++++++++++++++++++++++++++++
 unittests/Assignment/Makefile           | 12 +++++++++++
 2 files changed, 47 insertions(+)
 create mode 100644 unittests/Assignment/AssignmentTest.cpp
 create mode 100644 unittests/Assignment/Makefile

(limited to 'unittests/Assignment')

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 <iostream>
+#include <vector>
+
+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<const Array*> objects;
+  std::vector<unsigned char> value;
+  std::vector< std::vector<unsigned char> > 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<Expr> read = NotOptimizedExpr::alloc(Expr::createTempRead(array, Expr::Int8));
+
+  // Now evaluate. The OptimizedExpr should be folded
+  ref<Expr> evaluated = assignment.evaluate(read);
+  const ConstantExpr* asConstant = dyn_cast<ConstantExpr>(evaluated);
+  ASSERT_TRUE(asConstant != NULL);
+  ASSERT_EQ(asConstant->getZExtValue(), (unsigned) 128);
+}
diff --git a/unittests/Assignment/Makefile b/unittests/Assignment/Makefile
new file mode 100644
index 00000000..d4110c80
--- /dev/null
+++ b/unittests/Assignment/Makefile
@@ -0,0 +1,12 @@
+##===- unittests/Assignment/Makefile -----------------------*- Makefile -*-===##
+
+LEVEL := ../..
+include $(LEVEL)/Makefile.config
+
+TESTNAME := Assignment
+USEDLIBS := kleaverExpr.a
+LINK_COMPONENTS := support
+
+include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest
+
+CXXFLAGS += -DLLVM_29_UNITTEST
-- 
cgit 1.4.1