libTriton version 1.0 build 1592
Loading...
Searching...
No Matches
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>
13#include <triton/liftingToSMT.hpp>
14#include <triton/tritonTypes.hpp>
15
16
17
18namespace triton {
19 namespace engines {
20 namespace lifters {
21
22 LiftingToSMT::LiftingToSMT(const triton::ast::SharedAstContext& astCtxt, triton::engines::symbolic::SymbolicEngine* symbolic)
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 /* Print symbolic variables */
140 for (const auto& var : symVars) {
141 auto n = this->astCtxt->declare(this->astCtxt->variable(var.second));
142 stream << n << std::endl;
143 }
144
145 /* Sort SSA */
146 std::sort(symExprs.begin(), symExprs.end());
147 if (assert_) {
148 /* The last node will be handled later to separate conjuncts */
149 symExprs.pop_back();
150 }
151
152 /* Print symbolic expressions */
153 for (const auto& id : symExprs) {
154 auto& e = ssa[id];
155 stream << e->getFormattedExpression();
156 if (icomment && !e->getDisassembly().empty()) {
157 if (e->getComment().empty()) {
158 stream << " ; ";
159 }
160 else {
161 stream << " - ";
162 }
163 stream << e->getDisassembly();
164 }
165 stream << std::endl;
166 }
167
168 if (assert_) {
169 /* Print conjuncts in separate asserts */
170 std::vector<triton::ast::SharedAbstractNode> exprs;
171 std::vector<triton::ast::SharedAbstractNode> wl{expr->getAst()};
172
173 while (!wl.empty()) {
174 auto n = wl.back();
175 wl.pop_back();
176
177 if (n->getType() != ast::LAND_NODE) {
178 exprs.push_back(n);
179 continue;
180 }
181
182 for (const auto& child : n->getChildren()) {
183 wl.push_back(child);
184 }
185 }
186
187 for (auto it = exprs.crbegin(); it != exprs.crend(); ++it) {
188 stream << this->astCtxt->assert_(*it) << std::endl;
189 }
190
191 stream << "(check-sat)" << std::endl;
192 stream << "(get-model)" << std::endl;
193 }
194
195 /* Restore the AST representation mode */
196 this->astCtxt->setRepresentationMode(mode);
197
198 return stream;
199 }
200
201 }; /* lifters namespace */
202 }; /* engines namespace */
203}; /* triton namespace */
triton::ast::VariableNode
Variable node.
Definition ast.hpp:878
triton::engines::lifters::LiftingToSMT::LiftingToSMT
TRITON_EXPORT LiftingToSMT(const triton::ast::SharedAstContext &astCtxt, triton::engines::symbolic::SymbolicEngine *symbolic)
Constructor.
Definition liftingToSMT.cpp:22
triton::engines::lifters::LiftingToSMT::liftToSMT
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,...
Definition liftingToSMT.cpp:117
triton::engines::symbolic::SymbolicEngine::sliceExpressions
TRITON_EXPORT std::unordered_map< triton::usize, SharedSymbolicExpression > sliceExpressions(const SharedSymbolicExpression &expr)
Slices all expressions from a given one.
Definition symbolicEngine.cpp:487
triton::ast::SharedAstContext
std::shared_ptr< triton::ast::AstContext > SharedAstContext
Shared AST context.
Definition ast.hpp:65
triton::ast::search
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
triton::ast::VARIABLE_NODE
@ VARIABLE_NODE
Definition astEnums.hpp:82
triton::ast::LAND_NODE
@ LAND_NODE
Definition astEnums.hpp:74
triton::ast::representations::mode_e
mode_e
All types of representation mode.
Definition astEnums.hpp:98
triton::ast::representations::SMT_REPRESENTATION
@ SMT_REPRESENTATION
Definition astEnums.hpp:99
triton::engines::symbolic::SharedSymbolicExpression
std::shared_ptr< triton::engines::symbolic::SymbolicExpression > SharedSymbolicExpression
Shared Symbolic Expression.
Definition ast.hpp:40
triton
The Triton namespace.
Definition architecture.cpp:27
Generated by doxygen 1.10.0