libTriton  version 1.0 build 1549
liftingToSMT.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 <algorithm>
9#include <map>
10#include <vector>
11
12#include <triton/astEnums.hpp>
15
16
17
18namespace triton {
19 namespace engines {
20 namespace lifters {
21
23 : astCtxt(astCtxt), symbolic(symbolic) {
24 }
25
26
27 void LiftingToSMT::requiredFunctions(std::ostream& stream) {
28 stream << "(define-fun bswap8 ((value (_ BitVec 8))) (_ BitVec 8)" << std::endl;
29 stream << " value" << std::endl;
30 stream << ")" << std::endl;
31
32 stream << std::endl;
33 stream << "(define-fun bswap16 ((value (_ BitVec 16))) (_ BitVec 16)" << std::endl;
34 stream << " (bvor" << std::endl;
35 stream << " (bvshl" << std::endl;
36 stream << " (bvand value (_ bv255 16))" << std::endl;
37 stream << " (_ bv8 16)" << std::endl;
38 stream << " )" << std::endl;
39 stream << " (bvand (bvlshr value (_ bv8 16)) (_ bv255 16))" << std::endl;
40 stream << " )" << std::endl;
41 stream << ")" << std::endl;
42
43 stream << std::endl;
44 stream << "(define-fun bswap32 ((value (_ BitVec 32))) (_ BitVec 32)" << std::endl;
45 stream << " (bvor" << std::endl;
46 stream << " (bvshl" << std::endl;
47 stream << " (bvor" << std::endl;
48 stream << " (bvshl" << std::endl;
49 stream << " (bvor" << std::endl;
50 stream << " (bvshl" << std::endl;
51 stream << " (bvand value (_ bv255 32))" << std::endl;
52 stream << " (_ bv8 32)" << std::endl;
53 stream << " )" << std::endl;
54 stream << " (bvand (bvlshr value (_ bv8 32)) (_ bv255 32))" << std::endl;
55 stream << " )" << std::endl;
56 stream << " (_ bv8 32)" << std::endl;
57 stream << " )" << std::endl;
58 stream << " (bvand (bvlshr value (_ bv16 32)) (_ bv255 32))" << std::endl;
59 stream << " )" << std::endl;
60 stream << " (_ bv8 32)" << std::endl;
61 stream << " )" << std::endl;
62 stream << " (bvand (bvlshr value (_ bv24 32)) (_ bv255 32))" << std::endl;
63 stream << " )" << std::endl;
64 stream << ")" << std::endl;
65
66 stream << std::endl;
67 stream << "(define-fun bswap64 ((value (_ BitVec 64))) (_ BitVec 64)" << std::endl;
68 stream << " (bvor" << std::endl;
69 stream << " (bvshl" << std::endl;
70 stream << " (bvor" << std::endl;
71 stream << " (bvshl" << std::endl;
72 stream << " (bvor" << std::endl;
73 stream << " (bvshl" << std::endl;
74 stream << " (bvor" << std::endl;
75 stream << " (bvshl" << std::endl;
76 stream << " (bvor" << std::endl;
77 stream << " (bvshl" << std::endl;
78 stream << " (bvor" << std::endl;
79 stream << " (bvshl" << std::endl;
80 stream << " (bvor" << std::endl;
81 stream << " (bvshl" << std::endl;
82 stream << " (bvand value (_ bv255 64))" << std::endl;
83 stream << " (_ bv8 64)" << std::endl;
84 stream << " )" << std::endl;
85 stream << " (bvand (bvlshr value (_ bv8 64)) (_ bv255 64))" << std::endl;
86 stream << " )" << std::endl;
87 stream << " (_ bv8 64)" << std::endl;
88 stream << " )" << std::endl;
89 stream << " (bvand (bvlshr value (_ bv16 64)) (_ bv255 64))" << std::endl;
90 stream << " )" << std::endl;
91 stream << " (_ bv8 64)" << std::endl;
92 stream << " )" << std::endl;
93 stream << " (bvand (bvlshr value (_ bv24 64)) (_ bv255 64))" << std::endl;
94 stream << " )" << std::endl;
95 stream << " (_ bv8 64)" << std::endl;
96 stream << " )" << std::endl;
97 stream << " (bvand (bvlshr value (_ bv32 64)) (_ bv255 64))" << std::endl;
98 stream << " )" << std::endl;
99 stream << " (_ bv8 64)" << std::endl;
100 stream << " )" << std::endl;
101 stream << " (bvand (bvlshr value (_ bv40 64)) (_ bv255 64))" << std::endl;
102 stream << " )" << std::endl;
103 stream << " (_ bv8 64)" << std::endl;
104 stream << " )" << std::endl;
105 stream << " (bvand (bvlshr value (_ bv48 64)) (_ bv255 64))" << std::endl;
106 stream << " )" << std::endl;
107 stream << " (_ bv8 64)" << std::endl;
108 stream << " )" << std::endl;
109 stream << " (bvand (bvlshr value (_ bv56 64)) (_ bv255 64))" << std::endl;
110 stream << " )" << std::endl;
111 stream << ")" << std::endl;
112
113 stream << std::endl;
114 }
115
116
117 std::ostream& LiftingToSMT::liftToSMT(std::ostream& stream, const triton::engines::symbolic::SharedSymbolicExpression& expr, bool assert_, bool icomment) {
118 /* Save the AST representation mode */
119 triton::ast::representations::mode_e mode = this->astCtxt->getRepresentationMode();
120 this->astCtxt->setRepresentationMode(triton::ast::representations::SMT_REPRESENTATION);
121
122 /* Collect SSA form */
123 auto ssa = this->symbolic->sliceExpressions(expr);
124 std::vector<triton::usize> symExprs;
125 for (const auto& se : ssa) {
126 symExprs.push_back(se.first);
127 }
128
129 /* Collect used symbolic variables */
130 std::map<triton::usize, triton::engines::symbolic::SharedSymbolicVariable> symVars;
131 for (const auto& n : triton::ast::search(expr->getAst(), triton::ast::VARIABLE_NODE)) {
132 auto var = reinterpret_cast<triton::ast::VariableNode*>(n.get())->getSymbolicVariable();
133 symVars[var->getId()] = var;
134 }
135
136 /* Print required functions */
137 this->requiredFunctions(stream);
138
139 /* Declare arrays if exist */
140 for (const auto& array : triton::ast::search(expr->getAst(), triton::ast::ARRAY_NODE)) {
141 auto n = this->astCtxt->declare(array);
142 stream << n << std::endl;
143 }
144
145 /* Print symbolic variables */
146 for (const auto& var : symVars) {
147 auto n = this->astCtxt->declare(this->astCtxt->variable(var.second));
148 stream << n << std::endl;
149 }
150
151 /* Sort SSA */
152 std::sort(symExprs.begin(), symExprs.end());
153 if (assert_) {
154 /* The last node will be handled later to separate conjuncts */
155 symExprs.pop_back();
156 }
157
158 /* Print symbolic expressions */
159 for (const auto& id : symExprs) {
160 auto& e = ssa[id];
161 stream << e->getFormattedExpression();
162 if (icomment && !e->getDisassembly().empty()) {
163 if (e->getComment().empty()) {
164 stream << " ; ";
165 }
166 else {
167 stream << " - ";
168 }
169 stream << e->getDisassembly();
170 }
171 stream << std::endl;
172 }
173
174 if (assert_) {
175 /* Print conjuncts in separate asserts */
176 std::vector<triton::ast::SharedAbstractNode> exprs;
177 std::vector<triton::ast::SharedAbstractNode> wl{expr->getAst()};
178
179 while (!wl.empty()) {
180 auto n = wl.back();
181 wl.pop_back();
182
183 if (n->getType() != ast::LAND_NODE) {
184 exprs.push_back(n);
185 continue;
186 }
187
188 for (const auto& child : n->getChildren()) {
189 wl.push_back(child);
190 }
191 }
192
193 for (auto it = exprs.crbegin(); it != exprs.crend(); ++it) {
194 stream << this->astCtxt->assert_(*it) << std::endl;
195 }
196
197 stream << "(check-sat)" << std::endl;
198 stream << "(get-model)" << std::endl;
199 }
200
201 /* Restore the AST representation mode */
202 this->astCtxt->setRepresentationMode(mode);
203
204 return stream;
205 }
206
207 }; /* lifters namespace */
208 }; /* engines namespace */
209}; /* triton namespace */
Variable node.
Definition: ast.hpp:878
TRITON_EXPORT LiftingToSMT(const triton::ast::SharedAstContext &astCtxt, triton::engines::symbolic::SymbolicEngine *symbolic)
Constructor.
TRITON_EXPORT std::ostream & liftToSMT(std::ostream &stream, const triton::engines::symbolic::SharedSymbolicExpression &expr, bool assert_=false, bool icomment=false)
Lifts a symbolic expression and all its references to SMT format. If assert_ is true,...
TRITON_EXPORT std::unordered_map< triton::usize, SharedSymbolicExpression > sliceExpressions(const SharedSymbolicExpression &expr)
Slices all expressions from a given one.
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:3697
std::shared_ptr< triton::ast::AstContext > SharedAstContext
Shared AST context.
Definition: ast.hpp:65
mode_e
All types of representation mode.
Definition: astEnums.hpp:98
std::shared_ptr< triton::engines::symbolic::SymbolicExpression > SharedSymbolicExpression
Shared Symbolic Expression.
Definition: ast.hpp:40
The Triton namespace.