1
//! \file
2
/*
3
**  Copyright (C) - Triton
4
**
5
**  This program is under the terms of the Apache License 2.0.
6
*/
7

8
#include <list>
9
#include <triton/exceptions.hpp>
10
#include <triton/symbolicSimplification.hpp>
11

12

13

14
/*! \page SMT_simplification_page SMT simplification passes
15
    \brief [**internal**] All information about the SMT simplification passes.
16

17
\tableofcontents
18
\section SMT_simplification_description Description
19
<hr>
20

21
Triton allows you to optimize your AST (See: \ref py_AstContext_page) just before the assignment to a register, a memory
22
or a volatile symbolic expression. The record of a simplification pass is really straightforward. You have to record your simplification
23
callback using the triton::API::addCallback() function. Your simplification callback
24
must takes as parameters a triton::API and a triton::ast::SharedAbstractNode. The callback must return a triton::ast::SharedAbstractNode.
25
Then, your callback will be called before every symbolic assignment. Note that you can record several simplification callbacks or
26
remove a specific callback using the triton::API::removeCallback() function.
27

28
\subsection SMT_simplification_triton Simplification via Triton's rules
29
<hr>
30

31
Below, a little example which replaces all \f$ A \oplus A \rightarrow A = 0\f$.
32

33
~~~~~~~~~~~~~{.cpp}
34
// Rule: if (bvxor x x) -> (_ bv0 x_size)
35
triton::ast::SharedAbstractNode xor_simplification(triton::API& ctx, const triton::ast::SharedAbstractNode& node) {
36

37
  if (node->getType() == triton::ast::BVXOR_NODE) {
38
    if (node->getChildren()[0]->equalTo(node->getChildren()[1]))
39
      return ctx.getAstContext().bv(0, node->getBitvectorSize());
40
  }
41

42
  return node;
43
}
44

45
int main(int ac, const char *av[]) {
46
  ...
47
  // Record a simplification callback
48
  api.addCallback(xor_simplification);
49
  ...
50
}
51
~~~~~~~~~~~~~
52

53
Another example (this time in Python) which replaces a node with this rule \f$ ((A \land \lnot{B}) \lor (\lnot{A} \land B)) \rightarrow (A \oplus B) \f$.
54

55
~~~~~~~~~~~~~{.py}
56
# Rule: if ((a & ~b) | (~a & b)) -> (a ^ b)
57
def xor_bitwise(ctx, node):
58

59
    def getNot(node):
60
        a = node.getChildren()[0]
61
        b = node.getChildren()[1]
62
        if a.getType() == AST_NODE.BVNOT and b.getType() != AST_NODE.BVNOT:
63
            return a
64
        if b.getType() == AST_NODE.BVNOT and a.getType() != AST_NODE.BVNOT:
65
            return b
66
        return None
67

68
    def getNonNot(node):
69
        a = node.getChildren()[0]
70
        b = node.getChildren()[1]
71
        if a.getType() != AST_NODE.BVNOT and b.getType() == AST_NODE.BVNOT:
72
            return a
73
        if b.getType() != AST_NODE.BVNOT and a.getType() == AST_NODE.BVNOT:
74
            return b
75
        return None
76

77
    if node.getType() == AST_NODE.BVOR:
78
        c1 = node.getChildren()[0]
79
        c2 = node.getChildren()[1]
80
        if c1.getType() == AST_NODE.BVAND and c2.getType() == AST_NODE.BVAND:
81
            c1_not    = getNot(c1)
82
            c2_not    = getNot(c2)
83
            c1_nonNot = getNonNot(c1)
84
            c2_nonNot = getNonNot(c2)
85
            if c1_not.equalTo(~c2_nonNot) and c2_not.equalTo(~c1_nonNot):
86
                return c1_nonNot ^ c2_nonNot
87
    return node
88

89

90
if __name__ == "__main__":
91
    ctx = TritonContext()
92

93
    # Set arch to init engines
94
    ctx.setArchitecture(ARCH.X86_64)
95

96
    # Record simplifications
97
    ctx.addCallback(SYMBOLIC_SIMPLIFICATION, xor_bitwise)
98

99
    a = bv(1, 8)
100
    b = bv(2, 8)
101
    c = (~b & a) | (~a & b)
102
    print 'Expr: ', c
103
    c = ctx.simplify(c)
104
    print 'Simp: ', c
105
~~~~~~~~~~~~~
106

107
\subsection SMT_simplification_z3 Simplification via Z3
108
<hr>
109

110
As Triton is able to convert a Triton's AST to a Z3's AST and vice versa, you can benefit to the power of Z3
111
to simplify your expression, then, come back to a Triton's AST and apply your own rules.
112

113
~~~~~~~~~~~~~{.py}
114
>>> var = ctx.newSymbolicVariable(8)
115
>>> a = ctx.getAstContext().variable(var)
116
>>> b = bv(0x38, 8)
117
>>> c = bv(0xde, 8)
118
>>> d = bv(0x4f, 8)
119
>>> e = a * ((b & c) | d)
120

121
>>> print e
122
(bvmul SymVar_0 (bvor (bvand (_ bv56 8) (_ bv222 8)) (_ bv79 8)))
123

124
>>> usingZ3 = True
125
>>> f = ctx.simplify(e, usingZ3)
126
>>> print f
127
(bvmul (_ bv95 8) SymVar_0)
128
~~~~~~~~~~~~~
129

130
Note that applying a SMT simplification doesn't means that your expression will be more readable by an humain.
131
For example, if we perform a simplification of a bitwise operation (as described in the previous section), the
132
new expression is not really useful for an humain.
133

134
~~~~~~~~~~~~~{.py}
135
>>> a = ctx.getAstContext().variable(var)
136
>>> b = bv(2, 8)
137
>>> c = (~b & a) | (~a & b) # a ^ b
138

139
>>> print c
140
(bvor (bvand (bvnot (_ bv2 8)) SymVar_0) (bvand (bvnot SymVar_0) (_ bv2 8)))
141

142
>>> d = ctx.simplify(c, True)
143
>>> print d
144
(concat ((_ extract 7 2) SymVar_0) (bvnot ((_ extract 1 1) SymVar_0)) ((_ extract 0 0) SymVar_0))
145
~~~~~~~~~~~~~
146

147
As you can see, Z3 tries to apply a bit-to-bit simplification. That's why, Triton allows you to deal with both,
148
Z3's simplification passes and your own rules.
149

150
*/
151

152

153

154

155
namespace triton {
156
  namespace engines {
157
    namespace symbolic {
158

159

160 1
      SymbolicSimplification::SymbolicSimplification(triton::callbacks::Callbacks* callbacks) {
161 1
        this->callbacks = callbacks;
162
      }
163

164

165 0
      SymbolicSimplification::SymbolicSimplification(const SymbolicSimplification& other) {
166 0
        this->copy(other);
167
      }
168

169

170 1
      void SymbolicSimplification::copy(const SymbolicSimplification& other) {
171 1
        this->callbacks = other.callbacks;
172
      }
173

174

175 1
      triton::ast::SharedAbstractNode SymbolicSimplification::processSimplification(const triton::ast::SharedAbstractNode& node) const {
176 1
        std::list<triton::ast::SharedAbstractNode> worklist;
177 1
        triton::ast::SharedAbstractNode snode = node;
178

179 1
        if (node == nullptr)
180 0
          throw triton::exceptions::SymbolicSimplification("SymbolicSimplification::processSimplification(): node cannot be null.");
181

182 1
        if (this->callbacks && this->callbacks->isDefined(triton::callbacks::SYMBOLIC_SIMPLIFICATION)) {
183 1
          snode = this->callbacks->processCallbacks(triton::callbacks::SYMBOLIC_SIMPLIFICATION, node);
184
          /*
185
           *  We use a worklist strategy to avoid recursive calls
186
           *  and so stack overflow when going through a big AST.
187
           */
188
          worklist.push_back(snode);
189 1
          while (worklist.size()) {
190 1
            auto ast = worklist.front();
191 1
            worklist.pop_front();
192 1
            bool needs_update = false;
193 1
            for (triton::uint32 index = 0; index < ast->getChildren().size(); index++) {
194 1
              auto child = ast->getChildren()[index];
195
              /* Don't apply simplification on nodes like String, Integer, etc. */
196 1
              if (child->getBitvectorSize()) {
197 1
                auto schild = this->callbacks->processCallbacks(triton::callbacks::SYMBOLIC_SIMPLIFICATION, child);
198 1
                ast->setChild(index, schild);
199 1
                needs_update |= !schild->canReplaceNodeWithoutUpdate(child);
200 1
                worklist.push_back(schild);
201
              }
202
            }
203 1
            if (needs_update) {
204 0
              ast->init(true);
205
            }
206
          }
207
        }
208

209 1
        return snode;
210
      }
211

212

213 1
      SymbolicSimplification& SymbolicSimplification::operator=(const SymbolicSimplification& other) {
214 1
        this->copy(other);
215 1
        return *this;
216
      }
217

218
    }; /* symbolic namespace */
219
  }; /* engines namespace */
220 1
}; /*triton namespace */

Read our documentation on viewing source code .

Loading