1 //===-- ExprTest.cpp ------------------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9
10 #include "gtest/gtest.h"
11
12 #include "klee/Expr/ArrayCache.h"
13 #include "klee/Expr/ArrayExprOptimizer.h"
14 #include "klee/Expr/Assignment.h"
15 #include "klee/Expr/Expr.h"
16
17 #include <llvm/Support/CommandLine.h>
18
19 #include <iostream>
20
21 using namespace klee;
22 namespace klee {
23 extern llvm::cl::opt<ArrayOptimizationType> OptimizeArray;
24 }
25
26 namespace {
27
getConstant(int value,Expr::Width width)28 ref<Expr> getConstant(int value, Expr::Width width) {
29 int64_t ext = value;
30 uint64_t trunc = ext & (((uint64_t)-1LL) >> (64 - width));
31 return ConstantExpr::create(trunc, width);
32 }
33
34 static ArrayCache ac;
35
TEST(ArrayExprTest,HashCollisions)36 TEST(ArrayExprTest, HashCollisions) {
37 klee::OptimizeArray = ALL;
38 std::vector<ref<ConstantExpr>> constVals(256,
39 ConstantExpr::create(5, Expr::Int8));
40 const Array *array = ac.CreateArray("arr0", 256, constVals.data(),
41 constVals.data() + constVals.size(),
42 Expr::Int32, Expr::Int8);
43 const Array *symArray = ac.CreateArray("symIdx", 4);
44 ref<Expr> symIdx = Expr::createTempRead(symArray, Expr::Int32);
45 UpdateList ul(array, 0);
46 ul.extend(getConstant(3, Expr::Int32), getConstant(11, Expr::Int8));
47 ref<Expr> firstRead = ReadExpr::create(ul, symIdx);
48 ul.extend(getConstant(6, Expr::Int32), getConstant(42, Expr::Int8));
49 ul.extend(getConstant(6, Expr::Int32), getConstant(42, Expr::Int8));
50 ref<Expr> updatedRead = ReadExpr::create(ul, symIdx);
51
52 // This test requires hash collision and should be updated if the hash
53 // function changes
54 ASSERT_NE(updatedRead, firstRead);
55 ASSERT_EQ(updatedRead->hash(), firstRead->hash());
56
57 std::vector<unsigned char> value = {6, 0, 0, 0};
58 std::vector<std::vector<unsigned char>> values = {value};
59 std::vector<const Array *> assigmentArrays = {symArray};
60 auto a = std::make_unique<Assignment>(assigmentArrays, values,
61 /*_allowFreeValues=*/true);
62
63 EXPECT_NE(a->evaluate(updatedRead), a->evaluate(firstRead));
64 EXPECT_EQ(a->evaluate(updatedRead), getConstant(42, Expr::Int8));
65 EXPECT_EQ(a->evaluate(firstRead), getConstant(5, Expr::Int8));
66
67 ExprOptimizer opt;
68 auto oFirstRead = opt.optimizeExpr(firstRead, true);
69 auto oUpdatedRead = opt.optimizeExpr(updatedRead, true);
70 EXPECT_NE(oFirstRead, firstRead);
71 EXPECT_NE(updatedRead, oUpdatedRead);
72
73 EXPECT_NE(a->evaluate(oUpdatedRead), a->evaluate(oFirstRead));
74 EXPECT_EQ(a->evaluate(oUpdatedRead), getConstant(42, Expr::Int8));
75 EXPECT_EQ(a->evaluate(oFirstRead), getConstant(5, Expr::Int8));
76 }
77 }
78