[optimize-array] Hash collision test

2 files changed, 78 insertions, 2 deletions

diff --git a/unittests/Expr/ArrayExprTest.cpp b/unittests/Expr/ArrayExprTest.cpp
new file mode 100644
index 00000000..47375abd
--- /dev/null
+++ b/unittests/Expr/ArrayExprTest.cpp
@@ -0,0 +1,75 @@
+//===-- 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 <iostream>
+
+#include "../../lib/Expr/ArrayExprOptimizer.h"
+#include "klee/Expr/ArrayCache.h"
+#include "klee/Expr/Assignment.h"
+#include "klee/Expr/Expr.h"
+#include <llvm/Support/CommandLine.h>
+
+using namespace klee;
+namespace klee {
+extern llvm::cl::opt<ArrayOptimizationType> OptimizeArray;
+}
+
+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);
+}
+
+static ArrayCache ac;
+
+TEST(ArrayExprTest, HashCollisions) {
+  klee::OptimizeArray = ALL;
+  std::vector<ref<ConstantExpr>> constVals(256,
+                                           ConstantExpr::create(5, Expr::Int8));
+  const Array *array = ac.CreateArray("arr0", 256, constVals.data(),
+                                      constVals.data() + constVals.size(),
+                                      Expr::Int32, Expr::Int8);
+  const Array *symArray = ac.CreateArray("symIdx", 4);
+  ref<Expr> symIdx = Expr::createTempRead(symArray, Expr::Int32);
+  UpdateList ul(array, 0);
+  ul.extend(getConstant(3, Expr::Int32), getConstant(11, Expr::Int8));
+  ref<Expr> firstRead = ReadExpr::create(ul, symIdx);
+  ul.extend(getConstant(6, Expr::Int32), getConstant(42, Expr::Int8));
+  ul.extend(getConstant(6, Expr::Int32), getConstant(42, Expr::Int8));
+  ref<Expr> updatedRead = ReadExpr::create(ul, symIdx);
+
+  // This test requires hash collision and should be updated if the hash
+  // function changes
+  ASSERT_NE(updatedRead, firstRead);
+  ASSERT_EQ(updatedRead->hash(), firstRead->hash());
+
+  std::vector<unsigned char> value = {6, 0, 0, 0};
+  std::vector<std::vector<unsigned char>> values = {value};
+  std::vector<const Array *> assigmentArrays = {symArray};
+  auto a = std::make_unique<Assignment>(assigmentArrays, values,
+                                        /*_allowFreeValues=*/true);
+
+  EXPECT_NE(a->evaluate(updatedRead), a->evaluate(firstRead));
+  EXPECT_EQ(a->evaluate(updatedRead), getConstant(42, Expr::Int8));
+  EXPECT_EQ(a->evaluate(firstRead), getConstant(5, Expr::Int8));
+
+  ExprOptimizer opt;
+  auto oFirstRead = opt.optimizeExpr(firstRead, true);
+  auto oUpdatedRead = opt.optimizeExpr(updatedRead, true);
+  EXPECT_NE(oFirstRead, firstRead);
+  EXPECT_NE(updatedRead, oUpdatedRead);
+
+  EXPECT_NE(a->evaluate(oUpdatedRead), a->evaluate(oFirstRead));
+  EXPECT_EQ(a->evaluate(oUpdatedRead), getConstant(42, Expr::Int8));
+  EXPECT_EQ(a->evaluate(oFirstRead), getConstant(5, Expr::Int8));
+}
+}
diff --git a/unittests/Expr/CMakeLists.txt b/unittests/Expr/CMakeLists.txt
index 84dce619..34bc5a01 100644
--- a/unittests/Expr/CMakeLists.txt
+++ b/unittests/Expr/CMakeLists.txt
@@ -1,3 +1,4 @@
 add_klee_unit_test(ExprTest
-  ExprTest.cpp)
-target_link_libraries(ExprTest PRIVATE kleaverExpr)
+  ExprTest.cpp
+  ArrayExprTest.cpp)
+target_link_libraries(ExprTest PRIVATE kleaverExpr kleeSupport kleaverSolver)