libTriton version 1.0 build 1592
Loading...
Searching...
No Matches
synthesizer.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 <stack>
10#include <unordered_set>
11#include <vector>
12
13#include <triton/ast.hpp>
14#include <triton/exceptions.hpp>
18
19
20
21namespace triton {
22 namespace engines {
23 namespace synthesis {
24
26 : symbolic(symbolic) {
27 #ifdef TRITON_Z3_INTERFACE
29 #endif
30 }
31
32
33 SynthesisResult Synthesizer::synthesize(const triton::ast::SharedAbstractNode& input, bool constant, bool subexpr, bool opaque) {
34 SynthesisResult result;
35
36 // Save the input node
37 result.setInput(input);
38
39 // Start to record the time of the synthesizing
40 auto start = std::chrono::system_clock::now();
41
42 // Do not alter original input
43 auto node = triton::ast::newInstance(input.get(), true);
44
45 // Do the synthesize and if nothing has been synthesized, try on children expression
46 if (this->do_synthesize(node, constant, opaque, result) == false) {
47 if (subexpr == true) {
48 while (this->childrenSynthesis(node, constant, opaque, result));
49 }
50 }
51
53 if (this->var2expr.size()) {
54 this->substituteSubExpression(result.getOutput());
55 }
56
57 // Stop to record the time of the synthesizing
58 auto end = std::chrono::system_clock::now();
59
60 // Saving the time of the synthesizing
61 result.setTime(std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count());
62
63 return result;
64 }
65
66
67 bool Synthesizer::do_synthesize(const triton::ast::SharedAbstractNode& node, bool constant, bool opaque, SynthesisResult& result) {
68 bool ret = false;
69
70 // How many variables in the expression?
72
73 // If there is one symbolic variable, do unary operators synthesis
74 if (vars.size() == 1 && node->getLevel() > 2) {
75 ret = this->unaryOperatorSynthesis(vars, node, result);
76
77 // Do also constant synthesis
78 if (ret == false && constant == true) {
79 ret = this->constantSynthesis(vars, node, result);
80 }
81 }
82
83 // If there is two symbolic variables, do binary operators synthesis
84 else if (vars.size() == 2 && node->getLevel() > 2) {
85 ret = this->binaryOperatorSynthesis(vars, node, result);
86 }
87
88 // If nothing worked, do constant opaque synthesis
89 if (vars.size() && ret == false && opaque == true && node->getLevel() > 2) {
90 ret = this->opaqueConstantSynthesis(vars, node, result);
91 }
92
93 return ret;
94 }
95
96
97 bool Synthesizer::opaqueConstantSynthesis(const std::deque<triton::ast::SharedAbstractNode>& vars, const triton::ast::SharedAbstractNode& node, SynthesisResult& result) {
98 /* We need Z3 solver in order to use quantifier logic */
99 #ifdef TRITON_Z3_INTERFACE
100
101 auto actx = node->getContext();
102 auto var_c = this->symbolic->newSymbolicVariable(triton::engines::symbolic::UNDEFINED_VARIABLE, 0, node->getBitvectorSize(), "");
103 auto model = this->solver.getModel(actx->forall(vars, actx->equal(node, actx->variable(var_c))));
104
105 if (model.size()) {
106 auto constant = model.at(var_c->getId()).getValue();
107 auto size = model.at(var_c->getId()).getSize();
108
109 /* Replace the constant variable to a bitvector */
110 result.setOutput(actx->bv(constant, size));
111 result.setSuccess(true);
112 return true;
113 }
114
115 #endif
116
117 return false;
118 }
119
120
121 bool Synthesizer::constantSynthesis(const std::deque<triton::ast::SharedAbstractNode>& vars, const triton::ast::SharedAbstractNode& node, SynthesisResult& result) {
122 /* We need Z3 solver in order to use quantifier logic */
123 #ifdef TRITON_Z3_INTERFACE
124
125 /* We start by getting the symbolic variable of the expression */
126 auto var_x = reinterpret_cast<triton::ast::VariableNode*>(vars[0].get())->getSymbolicVariable();
127 auto actx = node->getContext();
128
129 triton::uint32 bits = var_x->getSize();
130 triton::uint32 insize = node->getBitvectorSize();
131 triton::uint32 outsize = bits;
132
133 /* We suppose variables are 8, 16, 32 or 64-bit long */
134 if ((bits != 8 && bits != 16 && bits != 32 && bits != 64) || insize != outsize)
135 return false;
136
137 /* We create the constant variable */
138 auto var_c = this->symbolic->newSymbolicVariable(triton::engines::symbolic::UNDEFINED_VARIABLE, 0, bits, "");
139
140 /* Create the constant operator table */
141 std::array<ConstantEntry, 6> operatorTable = {
142 ConstantEntry(1, actx->bvadd(actx->variable(var_x), actx->variable(var_c))), // x + c
143 ConstantEntry(1, actx->bvand(actx->variable(var_x), actx->variable(var_c))), // x & c
144 ConstantEntry(1, actx->bvmul(actx->variable(var_x), actx->variable(var_c))), // x * c
145 ConstantEntry(0, actx->bvsub(actx->variable(var_c), actx->variable(var_x))), // c - x
146 ConstantEntry(1, actx->bvsub(actx->variable(var_x), actx->variable(var_c))), // x - c
147 ConstantEntry(1, actx->bvxor(actx->variable(var_x), actx->variable(var_c))) // x ^ c
148 };
149
150 std::vector<triton::ast::SharedAbstractNode> x = {actx->variable(var_x)};
151 for (auto const& entry : operatorTable) {
152 /* For all X, there exists a constant C, such that operator is equal to node */
153 auto model = this->solver.getModel(actx->forall(x, actx->equal(entry.op, node)));
154 /* If a constant is found */
155 if (model.size()) {
156 auto constant = model.at(var_c->getId()).getValue();
157 auto size = model.at(var_c->getId()).getSize();
158 auto output = triton::ast::newInstance(entry.op.get());
159
160 /* Replace the constant variable to a bitvector */
161 output->setChild(entry.position, actx->bv(constant, size));
162 result.setOutput(output);
163 result.setSuccess(true);
164 return true;
165 }
166 }
167
168 #endif
169 return false;
170 }
171
172
173 bool Synthesizer::unaryOperatorSynthesis(const std::deque<triton::ast::SharedAbstractNode>& vars, const triton::ast::SharedAbstractNode& node, SynthesisResult& result) {
174 /* We start by saving orignal value of symbolic variable */
175 auto var_x = reinterpret_cast<triton::ast::VariableNode*>(vars[0].get())->getSymbolicVariable();
176 auto actx = node->getContext();
177
178 triton::uint512 save_x = actx->getVariableValue(var_x->getName());
179 triton::uint32 bits = var_x->getSize();
180
181 /* We suppose variables are 8, 16, 32 or 64-bit long */
182 if (bits != 8 && bits != 16 && bits != 32 && bits != 64)
183 return false;
184
185 /*
186 * NOTE: More the oracle table will grow more it will take time to looking
187 * for a potential synthesis. Currently, the complexity is O(n) where
188 * n is the number of entry in the table. At some point we have to
189 * change this.
190 */
191 for (auto const& it : triton::engines::synthesis::oracles::unopTable) {
192 triton::ast::ast_e op = it.first;
193 std::array<UnaryEntry, 40> oracles = it.second;
194
195 // Ignore bswap oracle for 8 bit value.
196 if (bits == 8 && op == triton::ast::BSWAP_NODE) {
197 continue;
198 }
199
200 bool found = true;
201 for (auto const& oracle : oracles) {
202 // Ignore oracle that is not on same size
203 if (oracle.bits != bits) {
204 continue;
205 }
206
207 // Inject value
208 actx->updateVariable(var_x->getName(), oracle.x);
209 if (node->evaluate() != oracle.r) {
210 found = false;
211 break;
212 }
213 }
214
215 // If an oracle is found, we craft a synthesized node.
216 if (found) {
217 switch (op) {
218 case triton::ast::BSWAP_NODE: result.setOutput(actx->bswap(actx->variable(var_x))); break;
219 case triton::ast::BVNEG_NODE: result.setOutput(actx->bvneg(actx->variable(var_x))); break;
220 case triton::ast::BVNOT_NODE: result.setOutput(actx->bvnot(actx->variable(var_x))); break;
221 default:
222 throw triton::exceptions::SynthesizerEngine("Synthesizer::unaryOperatorSynthesis(): Invalid type of operator.");
223 }
224
225 // Adjust the size of the destination
226 auto out = result.getOutput();
227 auto in = node;
228 auto outsize = out->getBitvectorSize();
229 auto insize = in->getBitvectorSize();
230 if (insize > outsize) {
231 result.setOutput(actx->zx(insize - outsize, out));
232 }
233
234 // Stop iterating over oracles
235 result.setSuccess(true);
236 break;
237 }
238 // If not found, continuing to iterate over oracles
239 }
240
241 // Whatever the result, we must restore orignal value of the symbolic variable
242 actx->updateVariable(var_x->getName(), save_x);
243
244 return result.successful();
245 }
246
247
248 bool Synthesizer::binaryOperatorSynthesis(const std::deque<triton::ast::SharedAbstractNode>& vars, const triton::ast::SharedAbstractNode& node, SynthesisResult& result) {
249 /* We start by saving orignal value of symbolic variables */
250 auto var_x = reinterpret_cast<triton::ast::VariableNode*>(vars[0].get())->getSymbolicVariable();
251 auto var_y = reinterpret_cast<triton::ast::VariableNode*>(vars[1].get())->getSymbolicVariable();
252 auto actx = node->getContext();
253
254 triton::uint512 save_x = actx->getVariableValue(var_x->getName());
255 triton::uint512 save_y = actx->getVariableValue(var_y->getName());
256 triton::uint32 bits = var_x->getSize();
257
258 /* We suppose variables are on a same size */
259 if (var_x->getSize() != var_y->getSize())
260 return false;
261
262 /* We suppose variables are 8, 16, 32 or 64-bit long */
263 if (bits != 8 && bits != 16 && bits != 32 && bits != 64)
264 return false;
265
266 for (auto const& it : triton::engines::synthesis::oracles::binopTable) {
267 triton::ast::ast_e op = it.first;
268 std::array<BinaryEntry, 40> oracles = it.second;
269
270 bool found = true;
271 for (auto const& oracle : oracles) {
272 // Ignore oracle that is not on same size
273 if (oracle.bits != bits) {
274 continue;
275 }
276
277 // Inject values
278 actx->updateVariable(var_x->getName(), oracle.x);
279 actx->updateVariable(var_y->getName(), oracle.y);
280 if (node->evaluate() != oracle.r) {
281 found = false;
282 break;
283 }
284 }
285
286 // If an oracle is found, we craft a synthesized node.
287 if (found) {
288 switch (op) {
289 case triton::ast::BVADD_NODE: result.setOutput(actx->bvadd(actx->variable(var_x), actx->variable(var_y))); break;
290 case triton::ast::BVAND_NODE: result.setOutput(actx->bvand(actx->variable(var_x), actx->variable(var_y))); break;
291 case triton::ast::BVMUL_NODE: result.setOutput(actx->bvmul(actx->variable(var_x), actx->variable(var_y))); break;
292 case triton::ast::BVNAND_NODE: result.setOutput(actx->bvnand(actx->variable(var_x), actx->variable(var_y))); break;
293 case triton::ast::BVNOR_NODE: result.setOutput(actx->bvnor(actx->variable(var_x), actx->variable(var_y))); break;
294 case triton::ast::BVOR_NODE: result.setOutput(actx->bvor(actx->variable(var_x), actx->variable(var_y))); break;
295 case triton::ast::BVROL_NODE: result.setOutput(actx->bvrol(actx->variable(var_x), actx->variable(var_y))); break;
296 case triton::ast::BVROR_NODE: result.setOutput(actx->bvror(actx->variable(var_x), actx->variable(var_y))); break;
297 case triton::ast::BVSDIV_NODE: result.setOutput(actx->bvsdiv(actx->variable(var_x), actx->variable(var_y))); break;
298 case triton::ast::BVSMOD_NODE: result.setOutput(actx->bvsmod(actx->variable(var_x), actx->variable(var_y))); break;
299 case triton::ast::BVSREM_NODE: result.setOutput(actx->bvsrem(actx->variable(var_x), actx->variable(var_y))); break;
300 case triton::ast::BVSUB_NODE: result.setOutput(actx->bvsub(actx->variable(var_x), actx->variable(var_y))); break;
301 case triton::ast::BVUDIV_NODE: result.setOutput(actx->bvudiv(actx->variable(var_x), actx->variable(var_y))); break;
302 case triton::ast::BVUREM_NODE: result.setOutput(actx->bvurem(actx->variable(var_x), actx->variable(var_y))); break;
303 case triton::ast::BVXNOR_NODE: result.setOutput(actx->bvxnor(actx->variable(var_x), actx->variable(var_y))); break;
304 case triton::ast::BVXOR_NODE: result.setOutput(actx->bvxor(actx->variable(var_x), actx->variable(var_y))); break;
305 default:
306 throw triton::exceptions::SynthesizerEngine("Synthesizer::binaryOperatorSynthesis(): Invalid type of operator.");
307 }
308
309 // Adjust the size of the destination
310 auto out = result.getOutput();
311 auto in = node;
312 auto outsize = out->getBitvectorSize();
313 auto insize = in->getBitvectorSize();
314 if (insize > outsize) {
315 result.setOutput(actx->zx(insize - outsize, out));
316 }
317
318 // Stop iterating over oracles
319 result.setSuccess(true);
320 break;
321 }
322 // If not found, continuing to iterate over oracles
323 }
324
325 // Whatever the result, we must restore orignal value of symbolic variables
326 actx->updateVariable(var_x->getName(), save_x);
327 actx->updateVariable(var_y->getName(), save_y);
328
329 return result.successful();
330 }
331
332
333 bool Synthesizer::childrenSynthesis(const triton::ast::SharedAbstractNode& node, bool constant, bool opaque, SynthesisResult& result) {
334 std::stack<triton::ast::AbstractNode*> worklist;
335 std::unordered_set<const triton::ast::AbstractNode*> visited;
336
337 bool ret = false;
338 worklist.push(node.get());
339 while (!worklist.empty()) {
340 auto current = worklist.top();
341 worklist.pop();
342
343 // This means that node is already visited and we will not need to visited it second time
344 if (visited.find(current) != visited.end()) {
345 continue;
346 }
347 visited.insert(current);
348
349 // Unroll reference
350 if (current->getType() == triton::ast::REFERENCE_NODE) {
351 worklist.push(reinterpret_cast<triton::ast::ReferenceNode*>(current)->getSymbolicExpression()->getAst().get());
352 }
353 else {
354 triton::usize index = 0;
355 // Apply synthesis on every child
356 for (const auto& child : current->getChildren()) {
357 SynthesisResult tmp;
358 if (this->do_synthesize(child, constant, opaque, tmp)) {
359 /* Symbolize the sub expression */
360 triton::ast::SharedAbstractNode subvar = this->symbolizeSubExpression(child, tmp);
361 /* Replace the child on the fly */
362 current->setChild(index++, subvar);
363 /* Set true because we synthesized at least one child */
364 result.setSuccess(true);
365 ret = true;
366 continue;
367 }
368 worklist.push(child.get());
369 index++;
370 }
371 }
372 }
373
374 /*
375 * If we synthesized at least one child, we set the output as 'node'
376 * because it has been modified on the fly
377 */
378 if (result.successful()) {
379 result.setOutput(node);
380 }
381
382 return ret;
383 }
384
385
386 triton::ast::SharedAbstractNode Synthesizer::symbolizeSubExpression(const triton::ast::SharedAbstractNode& node, SynthesisResult& tmpResult) {
387 triton::ast::SharedAstContext actx = node->getContext();
388 triton::ast::SharedAbstractNode subvar = nullptr;
389
390 auto it = this->hash2var.find(tmpResult.getOutput()->getHash());
391 if (it != this->hash2var.end()) {
392 /* If we already symbolized the node, return its symbolic variable */
393 subvar = it->second;
394 }
395 else {
396 /* Otherwise we create a new symbolic variable for this sub expression */
397 subvar = actx->variable(this->symbolic->newSymbolicVariable(triton::engines::symbolic::UNDEFINED_VARIABLE, 0, node->getBitvectorSize()));
398 this->hash2var.insert({tmpResult.getOutput()->getHash(), subvar});
399 this->var2expr.insert({subvar, tmpResult.getOutput()});
400 }
401
402 return subvar;
403 }
404
405
406 void Synthesizer::substituteSubExpression(const triton::ast::SharedAbstractNode& node) {
407 std::stack<triton::ast::AbstractNode*> worklist;
408 std::unordered_set<const triton::ast::AbstractNode*> visited;
409
410 worklist.push(node.get());
411 while (!worklist.empty()) {
412 auto current = worklist.top();
413 worklist.pop();
414
415 // This means that node is already visited and we will not need to visited it second time
416 if (visited.find(current) != visited.end()) {
417 continue;
418 }
419 visited.insert(current);
420
421 // Unroll reference
422 if (current->getType() == triton::ast::REFERENCE_NODE) {
423 worklist.push(reinterpret_cast<triton::ast::ReferenceNode*>(current)->getSymbolicExpression()->getAst().get());
424 }
425 else {
426 triton::usize index = 0;
427 for (const auto& child : current->getChildren()) {
428 if (child->getType() == triton::ast::VARIABLE_NODE) {
429 auto it = this->var2expr.find(child);
430 if (it != this->var2expr.end()) {
431 auto subexpr = this->var2expr[child];
432 current->setChild(index, subexpr);
433 worklist.push(subexpr.get());
434 }
435 }
436 else {
437 worklist.push(child.get());
438 }
439 index++;
440 }
441 }
442 }
443 }
444
445 }; /* synthesis namespace */
446 }; /* engines namespace */
447}; /* triton namespace */
TRITON_EXPORT SharedAstContext getContext(void) const
Access to its context.
Definition ast.cpp:50
Reference node.
Definition ast.hpp:789
Variable node.
Definition ast.hpp:878
TRITON_EXPORT void setSolver(triton::engines::solver::solver_e kind)
Initializes a predefined solver.
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...
TRITON_EXPORT SharedSymbolicVariable newSymbolicVariable(triton::engines::symbolic::variable_e type, triton::uint64 source, triton::uint32 size, const std::string &alias="")
Adds a symbolic variable.
The SynthesisResult engine class.
TRITON_EXPORT void setTime(triton::usize ms)
Sets the time.
TRITON_EXPORT const triton::ast::SharedAbstractNode getOutput(void)
Gets the output node.
TRITON_EXPORT void setInput(const triton::ast::SharedAbstractNode &input)
Sets the input node.
TRITON_EXPORT SynthesisResult synthesize(const triton::ast::SharedAbstractNode &node, bool constant=true, bool subexpr=true, bool opaque=false)
Synthesizes a given node. If constant is true, perform a constant synthesis. If opaque is true,...
TRITON_EXPORT Synthesizer(triton::engines::symbolic::SymbolicEngine *symbolic)
Constructor.
The exception class used by the synthesizer engine.
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition ast.hpp:59
SharedAbstractNode newInstance(AbstractNode *node, bool unroll)
AST C++ API - Duplicates the AST.
Definition ast.cpp:3604
std::shared_ptr< triton::ast::AstContext > SharedAstContext
Shared AST context.
Definition ast.hpp:65
std::deque< SharedAbstractNode > search(const SharedAbstractNode &node, triton::ast::ast_e match)
Returns a deque of collected matched nodes via a depth-first pre order traversal.
Definition ast.cpp:3710
std::map< triton::ast::ast_e, std::array< UnaryEntry, 40 > > unopTable
The oracle table for unary operators. Each entry is a UnaryEntry object.
std::map< triton::ast::ast_e, std::array< BinaryEntry, 40 > > binopTable
The oracle table for binary operators. Each entry is a BinaryEntry object.
@ UNDEFINED_VARIABLE
Undefined assignment.
std::size_t usize
unsigned MAX_INT 32 or 64 bits according to the CPU.
std::uint32_t uint32
unisgned 32-bits
The Triton namespace.