libTriton  version 1.0 build 1549
z3Solver.cpp
Go to the documentation of this file.
1
2/*
3** Copyright (C) - Triton
4**
5** This program is under the terms of the Apache License 2.0.
6*/
7
8#include <chrono>
9#include <string>
10
11#include <triton/astContext.hpp>
12#include <triton/exceptions.hpp>
15#include <triton/tritonToZ3.hpp>
17#include <triton/z3Solver.hpp>
18#include <triton/z3ToTriton.hpp>
19
20
21
22namespace triton {
23 namespace engines {
24 namespace solver {
25
26 z3::expr Z3Solver::mk_or(z3::expr_vector args) {
27 std::vector<Z3_ast> array;
28
29 for (triton::uint32 i = 0; i < args.size(); i++)
30 array.push_back(args[i]);
31
32 return to_expr(args.ctx(), Z3_mk_or(args.ctx(), static_cast<triton::uint32>(array.size()), &(array[0])));
33 }
34
35
37 this->timeout = 0;
38 this->memoryLimit = 0;
39 }
40
41
42 std::vector<std::unordered_map<triton::usize, SolverModel>> Z3Solver::getModels(const triton::ast::SharedAbstractNode& node, triton::uint32 limit, triton::engines::solver::status_e* status, triton::uint32 timeout, triton::uint32* solvingTime) const {
43 std::vector<std::unordered_map<triton::usize, SolverModel>> ret;
45 triton::ast::TritonToZ3 z3Ast{false};
46
47 try {
48 if (onode == nullptr)
49 throw triton::exceptions::SolverEngine("Z3Solver::getModels(): node cannot be null.");
50
51 /* Z3 does not need an assert() as root node */
52 if (node->getType() == triton::ast::ASSERT_NODE)
53 onode = node->getChildren()[0];
54
55 if (onode->isLogical() == false)
56 throw triton::exceptions::SolverEngine("Z3Solver::getModels(): Must be a logical node.");
57
58 z3::expr expr = z3Ast.convert(onode);
59 z3::context& ctx = expr.ctx();
60 z3::solver solver(ctx);
61
62 /* Create a solver and add the expression */
63 solver.add(expr);
64
65 z3::params p(ctx);
66
67 /* Define the timeout */
68 if (timeout) {
69 p.set(":timeout", timeout);
70 }
71 else if (this->timeout) {
72 p.set(":timeout", this->timeout);
73 }
74
75 /* Define memory limit */
76 if (this->memoryLimit) {
77 p.set(":max_memory", this->memoryLimit);
78 }
79
80 solver.set(p);
81
82 /* Get time of solving start */
83 auto start = std::chrono::system_clock::now();
84
85 /* Get first model */
86 z3::check_result res = solver.check();
87
88 /* Write back the status code of the first constraint */
89 this->writeBackStatus(solver, res, status);
90
91 /* Check if it is sat */
92 while (res == z3::sat && limit >= 1) {
93 /* Get model */
94 z3::model m = solver.get_model();
95
96 /* Traversing the model */
97 std::unordered_map<triton::usize, SolverModel> smodel;
98 z3::expr_vector args(ctx);
99 for (triton::uint32 i = 0; i < m.size(); i++) {
100
101 /* Get the z3 variable */
102 z3::func_decl z3Variable = m[i];
103
104 /* Get the name as std::string from a z3 variable */
105 std::string varName = z3Variable.name().str();
106
107 /* Get z3 expr */
108 z3::expr exp = m.get_const_interp(z3Variable);
109
110 /* Get the size of a z3 expr */
111 triton::uint32 bvSize = exp.get_sort().bv_size();
112
113 /* Get the value of a z3 expr */
114 std::string svalue = Z3_get_numeral_string(ctx, exp);
115
116 /* Convert a string value to a integer value */
117 triton::uint512 value = triton::uint512(svalue.c_str());
118
119 /* Create a triton model */
120 SolverModel trionModel = SolverModel(z3Ast.variables[varName], value);
121
122 /* Map the result */
123 smodel[trionModel.getId()] = trionModel;
124
125 /* Uniq result */
126 if (exp.get_sort().is_bv())
127 args.push_back(ctx.bv_const(varName.c_str(), bvSize) != ctx.bv_val(svalue.c_str(), bvSize));
128 }
129
130 /* Check that model is available */
131 if (smodel.empty())
132 break;
133
134 /* Push model */
135 ret.push_back(smodel);
136
137 if (--limit) {
138 /* Escape last models */
139 if (!args.empty()) {
140 solver.add(this->mk_or(args));
141 }
142
143 /* Get next model */
144 res = solver.check();
145 }
146 }
147
148 /* Get time of solving end */
149 auto end = std::chrono::system_clock::now();
150
151 if (solvingTime)
152 *solvingTime = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
153 }
154 catch (const z3::exception& e) {
155 if (!strcmp(e.msg(), "max. memory exceeded")) {
156 if (status) {
158 }
159 return {};
160 }
161 throw triton::exceptions::SolverEngine(std::string("Z3Solver::getModels(): ") + e.msg());
162 }
163
164 return ret;
165 }
166
167
169 triton::ast::TritonToZ3 z3Ast{false};
170
171 if (node == nullptr)
172 throw triton::exceptions::SolverEngine("Z3Solver::isSat(): node cannot be null.");
173
174 if (node->isLogical() == false)
175 throw triton::exceptions::SolverEngine("Z3Solver::isSat(): Must be a logical node.");
176
177 try {
178 z3::expr expr = z3Ast.convert(node);
179 z3::context& ctx = expr.ctx();
180 z3::solver solver(ctx);
181
182 /* Create a solver and add the expression */
183 solver.add(expr);
184
185 z3::params p(ctx);
186
187 /* Define the timeout */
188 if (timeout) {
189 p.set(":timeout", timeout);
190 }
191 else if (this->timeout) {
192 p.set(":timeout", this->timeout);
193 }
194
195 /* Define memory limit */
196 if (this->memoryLimit) {
197 p.set(":max_memory", this->memoryLimit);
198 }
199
200 solver.set(p);
201
202 /* Get time of solving start */
203 auto start = std::chrono::system_clock::now();
204
205 z3::check_result res = solver.check();
206
207 /* Get time of solving end */
208 auto end = std::chrono::system_clock::now();
209
210 if (solvingTime)
211 *solvingTime = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
212
213 this->writeBackStatus(solver, res, status);
214 return res == z3::sat;
215 }
216 catch (const z3::exception& e) {
217 if (!strcmp(e.msg(), "max. memory exceeded")) {
218 if (status) {
220 }
221 return {};
222 }
223 throw triton::exceptions::SolverEngine(std::string("Z3Solver::isSat(): ") + e.msg());
224 }
225 }
226
227
228 std::unordered_map<triton::usize, SolverModel> Z3Solver::getModel(const triton::ast::SharedAbstractNode& node, triton::engines::solver::status_e* status, triton::uint32 timeout, triton::uint32 *solvingTime) const {
229 std::unordered_map<triton::usize, SolverModel> ret;
230 std::vector<std::unordered_map<triton::usize, SolverModel>> allModels;
231
232 allModels = this->getModels(node, 1, status, timeout, solvingTime);
233 if (allModels.size() > 0)
234 ret = allModels.front();
235
236 return ret;
237 }
238
239
241 if (node == nullptr)
242 throw triton::exceptions::AstLifting("Z3Solver::simplify(): node cannot be null.");
243
244 try {
245 triton::ast::TritonToZ3 z3Ast{false};
246 triton::ast::Z3ToTriton tritonAst{node->getContext()};
247
248 /* From Triton to Z3 */
249 z3::expr expr = z3Ast.convert(node);
250
251 /* Simplify and back to Triton's AST */
252 auto snode = tritonAst.convert(expr.simplify());
253
254 return snode;
255 }
256 catch (const z3::exception& e) {
257 throw triton::exceptions::AstLifting(std::string("Z3Solver::evaluate(): ") + e.msg());
258 }
259 }
260
261
263 if (node == nullptr)
264 throw triton::exceptions::AstLifting("Z3Solver::simplify(): node cannot be null.");
265
266 try {
267 triton::ast::TritonToZ3 z3ast{true};
268
269 /* From Triton to Z3 */
270 z3::expr expr = z3ast.convert(node);
271
272 /* Simplify the expression to get a constant */
273 expr = expr.simplify();
274
275 triton::uint512 res = 0;
276 if (expr.get_sort().is_bool())
277 res = Z3_get_bool_value(expr.ctx(), expr) == Z3_L_TRUE ? true : false;
278 else
279 res = triton::uint512{Z3_get_numeral_string(expr.ctx(), expr)};
280
281 return res;
282 }
283 catch (const z3::exception& e) {
284 throw triton::exceptions::AstLifting(std::string("Z3Solver::evaluate(): ") + e.msg());
285 }
286 }
287
288
289 void Z3Solver::writeBackStatus(z3::solver& solver, z3::check_result res, triton::engines::solver::status_e* status) const {
290 if (status != nullptr) {
291 switch (res) {
292 case z3::sat:
294 break;
295
296 case z3::unsat:
298 break;
299
300 case z3::unknown:
301 if (solver.reason_unknown() == "timeout") {
303 }
304 else if (solver.reason_unknown() == "max. memory exceeded") {
306 }
307 else {
309 }
310 break;
311 }
312 }
313 }
314
315
316 std::string Z3Solver::getName(void) const {
317 return "z3";
318 }
319
320
322 this->timeout = ms;
323 }
324
325
327 this->memoryLimit = limit;
328 }
329
330 };
331 };
332};
Converts a Triton's AST to Z3's AST.
Definition: tritonToZ3.hpp:37
TRITON_EXPORT z3::expr convert(const triton::ast::SharedAbstractNode &node)
Converts to Z3's AST.
Definition: tritonToZ3.cpp:40
Converts a Z3's AST to a Triton's AST.
Definition: z3ToTriton.hpp:36
TRITON_EXPORT triton::ast::SharedAbstractNode convert(const z3::expr &expr)
Converts to Triton's AST.
Definition: z3ToTriton.cpp:24
This class is used to represent a constraint model solved.
Definition: solverModel.hpp:42
TRITON_EXPORT triton::usize getId(void) const
Returns the id of the variable.
Definition: solverModel.cpp:41
TRITON_EXPORT std::unordered_map< triton::usize, SolverModel > getModel(const triton::ast::SharedAbstractNode &node, triton::engines::solver::status_e *status=nullptr, triton::uint32 timeout=0, triton::uint32 *solvingTime=nullptr) const
Computes and returns a model from a symbolic constraint. State is returned in the status pointer as w...
Definition: z3Solver.cpp:228
TRITON_EXPORT Z3Solver()
Constructor.
Definition: z3Solver.cpp:36
TRITON_EXPORT triton::uint512 evaluate(const triton::ast::SharedAbstractNode &node) const
Evaluates a Triton's AST via Z3 and returns a concrete value.
Definition: z3Solver.cpp:262
TRITON_EXPORT bool isSat(const triton::ast::SharedAbstractNode &node, triton::engines::solver::status_e *status=nullptr, triton::uint32 timeout=0, triton::uint32 *solvingTime=nullptr) const
Returns true if an expression is satisfiable.
Definition: z3Solver.cpp:168
TRITON_EXPORT std::string getName(void) const
Returns the name of this solver.
Definition: z3Solver.cpp:316
TRITON_EXPORT void setTimeout(triton::uint32 ms)
Defines a solver timeout (in milliseconds).
Definition: z3Solver.cpp:321
TRITON_EXPORT triton::ast::SharedAbstractNode simplify(const triton::ast::SharedAbstractNode &node) const
Converts a Triton's AST to a Z3's AST, perform a Z3 simplification and returns a Triton's AST.
Definition: z3Solver.cpp:240
TRITON_EXPORT void setMemoryLimit(triton::uint32 mem)
Defines a solver memory consumption limit (in megabytes).
Definition: z3Solver.cpp:326
TRITON_EXPORT std::vector< std::unordered_map< triton::usize, SolverModel > > getModels(const triton::ast::SharedAbstractNode &node, triton::uint32 limit, triton::engines::solver::status_e *status=nullptr, triton::uint32 timeout=0, triton::uint32 *solvingTime=nullptr) const
Computes and returns several models from a symbolic constraint. The limit is the number of models ret...
Definition: z3Solver.cpp:42
The exception class used by all AST lifting (e.g z3 <-> triton).
Definition: exceptions.hpp:413
The exception class used by the solver engine.
Definition: exceptions.hpp:185
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition: ast.hpp:59
math::wide_integer::uint512_t uint512
unsigned 512-bits
Definition: tritonTypes.hpp:69
std::uint32_t uint32
unisgned 32-bits
Definition: tritonTypes.hpp:39
The Triton namespace.