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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
//===-- 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 "klee/Expr.h"
using namespace klee;
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);
}
TEST(ExprTest, BasicConstruction) {
EXPECT_EQ(ref<Expr>(0, 32),
SubExpr::create(ref<Expr>(10, 32),
ref<Expr>(10, 32)));
}
TEST(ExprTest, ConcatExtract) {
Array *array = new Array(0, 1, 256);
ref<Expr> read8 = Expr::createTempRead(array, 8);
Array *array2 = new Array(0, 2, 256);
ref<Expr> read8_2 = Expr::createTempRead(array2, 8);
ref<Expr> c100 = getConstant(100, 8);
ref<Expr> concat1 = ConcatExpr::create4(read8, read8, c100, read8_2);
EXPECT_EQ(2U, concat1.getNumKids());
EXPECT_EQ(2U, concat1.getKid(1).getNumKids());
EXPECT_EQ(2U, concat1.getKid(1).getKid(1).getNumKids());
ref<Expr> extract1 = ExtractExpr::create(concat1, 8, 16);
EXPECT_EQ(Expr::Concat, extract1.getKind());
EXPECT_EQ(read8, extract1.getKid(0));
EXPECT_EQ(c100, extract1.getKid(1));
ref<Expr> extract2 = ExtractExpr::create(concat1, 6, 26);
EXPECT_EQ( Expr::Concat, extract2.getKind());
EXPECT_EQ( read8, extract2.getKid(0));
EXPECT_EQ( Expr::Concat, extract2.getKid(1).getKind());
EXPECT_EQ( read8, extract2.getKid(1).getKid(0));
EXPECT_EQ( Expr::Concat, extract2.getKid(1).getKid(1).getKind());
EXPECT_EQ( c100, extract2.getKid(1).getKid(1).getKid(0));
EXPECT_EQ( Expr::Extract, extract2.getKid(1).getKid(1).getKid(1).getKind());
ref<Expr> extract3 = ExtractExpr::create(concat1, 24, 1);
EXPECT_EQ(Expr::Extract, extract3.getKind());
ref<Expr> extract4 = ExtractExpr::create(concat1, 27, 2);
EXPECT_EQ(Expr::Extract, extract4.getKind());
const ExtractExpr* tmp = dyn_ref_cast<ExtractExpr>(extract4);
EXPECT_EQ(3U, tmp->offset);
EXPECT_EQ(2U, tmp->getWidth());
ref<Expr> extract5 = ExtractExpr::create(concat1, 17, 5);
EXPECT_EQ(Expr::Extract, extract5.getKind());
ref<Expr> extract6 = ExtractExpr::create(concat1, 3, 26);
EXPECT_EQ(Expr::Concat, extract6.getKind());
EXPECT_EQ(Expr::Extract, extract6.getKid(0).getKind());
EXPECT_EQ(Expr::Concat, extract6.getKid(1).getKind());
EXPECT_EQ(read8, extract6.getKid(1).getKid(0));
EXPECT_EQ(Expr::Concat, extract6.getKid(1).getKid(1).getKind());
EXPECT_EQ(c100, extract6.getKid(1).getKid(1).getKid(0));
EXPECT_EQ(Expr::Extract, extract6.getKid(1).getKid(1).getKid(1).getKind());
ref<Expr> concat10 = ConcatExpr::create4(read8, c100, c100, read8);
ref<Expr> extract10 = ExtractExpr::create(concat10, 8, 16);
EXPECT_EQ(Expr::Constant, extract10.getKind());
}
TEST(ExprTest, ExtractConcat) {
Array *array = new Array(0, 3, 256);
ref<Expr> read64 = Expr::createTempRead(array, 64);
Array *array2 = new Array(0, 4, 256);
ref<Expr> read8_2 = Expr::createTempRead(array2, 8);
ref<Expr> extract1 = ExtractExpr::create(read64, 36, 4);
ref<Expr> extract2 = ExtractExpr::create(read64, 32, 4);
ref<Expr> extract3 = ExtractExpr::create(read64, 12, 3);
ref<Expr> extract4 = ExtractExpr::create(read64, 10, 2);
ref<Expr> extract5 = ExtractExpr::create(read64, 2, 8);
ref<Expr> kids1[6] = { extract1, extract2,
read8_2,
extract3, extract4, extract5 };
ref<Expr> concat1 = ConcatExpr::createN(6, kids1);
EXPECT_EQ(29U, concat1.getWidth());
ref<Expr> extract6 = ExtractExpr::create(read8_2, 2, 5);
ref<Expr> extract7 = ExtractExpr::create(read8_2, 1, 1);
ref<Expr> kids2[3] = { extract1, extract6, extract7 };
ref<Expr> concat2 = ConcatExpr::createN(3, kids2);
EXPECT_EQ(10U, concat2.getWidth());
EXPECT_EQ(Expr::Extract, concat2.getKid(0).getKind());
EXPECT_EQ(Expr::Extract, concat2.getKid(1).getKind());
}
}
|
