about summary refs log tree commit diff homepage
path: root/unittests/Expr/ArrayExprTest.cpp
blob: 47375abd1a24275e1c675d22fbbc79f4c39b85d5 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
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));
}
}