23 : astCtxt(astCtxt), symbolic(symbolic) {
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;
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;
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;
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;
124 std::vector<triton::usize> symExprs;
125 for (
const auto& se : ssa) {
126 symExprs.push_back(se.first);
130 std::map<triton::usize, triton::engines::symbolic::SharedSymbolicVariable> symVars;
133 symVars[var->getId()] = var;
137 this->requiredFunctions(stream);
140 for (
const auto& var : symVars) {
141 auto n = this->astCtxt->declare(this->astCtxt->variable(var.second));
142 stream << n << std::endl;
146 std::sort(symExprs.begin(), symExprs.end());
153 for (
const auto&
id : symExprs) {
155 stream << e->getFormattedExpression();
156 if (icomment && !e->getDisassembly().empty()) {
157 if (e->getComment().empty()) {
163 stream << e->getDisassembly();
170 std::vector<triton::ast::SharedAbstractNode> exprs;
171 std::vector<triton::ast::SharedAbstractNode> wl{expr->getAst()};
173 while (!wl.empty()) {
182 for (
const auto& child : n->getChildren()) {
187 for (
auto it = exprs.crbegin(); it != exprs.crend(); ++it) {
188 stream << this->astCtxt->assert_(*it) << std::endl;
191 stream <<
"(check-sat)" << std::endl;
192 stream <<
"(get-model)" << std::endl;
196 this->astCtxt->setRepresentationMode(mode);
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,...
The symbolic engine class.
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.
std::shared_ptr< triton::ast::AstContext > SharedAstContext
Shared AST context.
mode_e
All types of representation mode.
std::shared_ptr< triton::engines::symbolic::SymbolicExpression > SharedSymbolicExpression
Shared Symbolic Expression.