1 //===-- SolverTest.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/Constraints.h"
14 #include "klee/Expr/Expr.h"
15 #include "klee/Solver/Solver.h"
16 #include "klee/Solver/SolverCmdLine.h"
17
18 #include "llvm/ADT/StringExtras.h"
19
20 #include <iostream>
21
22 using namespace klee;
23
24 namespace {
25
26 const int g_constants[] = { -1, 1, 4, 17, 0 };
27 const Expr::Width g_types[] = { Expr::Bool,
28 Expr::Int8,
29 Expr::Int16,
30 Expr::Int32,
31 Expr::Int64 };
32
getConstant(int value,Expr::Width width)33 ref<Expr> getConstant(int value, Expr::Width width) {
34 int64_t ext = value;
35 uint64_t trunc = ext & (((uint64_t) -1LL) >> (64 - width));
36 return ConstantExpr::create(trunc, width);
37 }
38
39 // We have to have the cache globally scopped (and not in ``testOperation``)
40 // because the Solver (i.e. in STP's case the STPBuilder) holds on to pointers
41 // to allocated Arrays.
42 ArrayCache ac;
43
44 template<class T>
testOperation(Solver & solver,int value,Expr::Width operandWidth,Expr::Width resultWidth)45 void testOperation(Solver &solver,
46 int value,
47 Expr::Width operandWidth,
48 Expr::Width resultWidth) {
49 std::vector<Expr::CreateArg> symbolicArgs;
50
51 for (unsigned i = 0; i < T::numKids; i++) {
52 if (!T::isValidKidWidth(i, operandWidth))
53 return;
54
55 unsigned size = Expr::getMinBytesForWidth(operandWidth);
56 static uint64_t id = 0;
57 const Array *array = ac.CreateArray("arr" + llvm::utostr(++id), size);
58 symbolicArgs.push_back(Expr::CreateArg(Expr::createTempRead(array,
59 operandWidth)));
60 }
61
62 if (T::needsResultType())
63 symbolicArgs.push_back(Expr::CreateArg(resultWidth));
64
65 ref<Expr> fullySymbolicExpr = Expr::createFromKind(T::kind, symbolicArgs);
66
67 // For each kid, replace the kid with a constant value and verify
68 // that the fully symbolic expression is equivalent to it when the
69 // replaced value is appropriated constrained.
70 for (unsigned kid = 0; kid < T::numKids; kid++) {
71 std::vector<Expr::CreateArg> partiallyConstantArgs(symbolicArgs);
72 partiallyConstantArgs[kid] = getConstant(value, operandWidth);
73
74 ref<Expr> expr =
75 NotOptimizedExpr::create(EqExpr::create(partiallyConstantArgs[kid].expr,
76 symbolicArgs[kid].expr));
77
78 ref<Expr> partiallyConstantExpr =
79 Expr::createFromKind(T::kind, partiallyConstantArgs);
80
81 ref<Expr> queryExpr = EqExpr::create(fullySymbolicExpr,
82 partiallyConstantExpr);
83
84 ConstraintSet constraints;
85 ConstraintManager cm(constraints);
86 cm.addConstraint(expr);
87 bool res;
88 bool success = solver.mustBeTrue(Query(constraints, queryExpr), res);
89 EXPECT_EQ(true, success) << "Constraint solving failed";
90
91 if (success) {
92 EXPECT_EQ(true, res) << "Evaluation failed!\n"
93 << "query " << queryExpr
94 << " with " << expr;
95 }
96 }
97 }
98
99 template<class T>
testOpcode(Solver & solver,bool tryBool=true,bool tryZero=true,unsigned maxWidth=64)100 void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true,
101 unsigned maxWidth = 64) {
102 for (unsigned j=0; j<sizeof(g_types)/sizeof(g_types[0]); j++) {
103 Expr::Width type = g_types[j];
104
105 if (type > maxWidth) continue;
106
107 for (unsigned i=0; i<sizeof(g_constants)/sizeof(g_constants[0]); i++) {
108 int value = g_constants[i];
109 if (!tryZero && !value) continue;
110 if (type == Expr::Bool && !tryBool) continue;
111
112 if (!T::needsResultType()) {
113 testOperation<T>(solver, value, type, type);
114 continue;
115 }
116
117 for (unsigned k=0; k<sizeof(g_types)/sizeof(g_types[0]); k++) {
118 Expr::Width resultType = g_types[k];
119
120 // nasty hack to give only Trunc/ZExt/SExt the right types
121 if (T::kind == Expr::SExt || T::kind == Expr::ZExt) {
122 if (Expr::getMinBytesForWidth(type) >=
123 Expr::getMinBytesForWidth(resultType))
124 continue;
125 }
126
127 testOperation<T>(solver, value, type, resultType);
128 }
129 }
130 }
131 }
132
TEST(SolverTest,Evaluation)133 TEST(SolverTest, Evaluation) {
134 Solver *solver = klee::createCoreSolver(CoreSolverToUse);
135
136 solver = createCexCachingSolver(solver);
137 solver = createCachingSolver(solver);
138 solver = createIndependentSolver(solver);
139
140 testOpcode<SelectExpr>(*solver);
141 testOpcode<ZExtExpr>(*solver);
142 testOpcode<SExtExpr>(*solver);
143
144 testOpcode<AddExpr>(*solver);
145 testOpcode<SubExpr>(*solver);
146 testOpcode<MulExpr>(*solver, false, true, 8);
147 testOpcode<SDivExpr>(*solver, false, false, 8);
148 testOpcode<UDivExpr>(*solver, false, false, 8);
149 testOpcode<SRemExpr>(*solver, false, false, 8);
150 testOpcode<URemExpr>(*solver, false, false, 8);
151 testOpcode<ShlExpr>(*solver, false);
152 testOpcode<LShrExpr>(*solver, false);
153 testOpcode<AShrExpr>(*solver, false);
154 testOpcode<AndExpr>(*solver);
155 testOpcode<OrExpr>(*solver);
156 testOpcode<XorExpr>(*solver);
157
158 testOpcode<EqExpr>(*solver);
159 testOpcode<NeExpr>(*solver);
160 testOpcode<UltExpr>(*solver);
161 testOpcode<UleExpr>(*solver);
162 testOpcode<UgtExpr>(*solver);
163 testOpcode<UgeExpr>(*solver);
164 testOpcode<SltExpr>(*solver);
165 testOpcode<SleExpr>(*solver);
166 testOpcode<SgtExpr>(*solver);
167 testOpcode<SgeExpr>(*solver);
168
169 delete solver;
170 }
171
172 }
173