Skip to content

Commit fe825bd

Browse files
JonathanSalwanJonathanSalwan
committed
Fix #571: Add the IFF AST node
1 parent 9c5c39e commit fe825bd

18 files changed

+164
-16
lines changed

‎.build_number

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
1397
1+
1398

‎src/libtriton/ast/ast.cpp

+48
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,7 @@ namespace triton {
9393
case BVULT_NODE:
9494
case DISTINCT_NODE:
9595
case EQUAL_NODE:
96+
case IFF_NODE:
9697
case LAND_NODE:
9798
case LNOT_NODE:
9899
case LOR_NODE:
@@ -1874,6 +1875,52 @@ namespace triton {
18741875
}
18751876

18761877

1878+
/* ====== iff */
1879+
1880+
1881+
IffNode::IffNode(const SharedAbstractNode& expr1, const SharedAbstractNode& expr2): AbstractNode(IFF_NODE, expr1->getContext()) {
1882+
this->addChild(expr1);
1883+
this->addChild(expr2);
1884+
}
1885+
1886+
1887+
void IffNode::init(void) {
1888+
if (this->children.size() < 2)
1889+
throw triton::exceptions::Ast("IffNode::init(): Must take at least two children.");
1890+
1891+
if (this->children[0]->isLogical() == false)
1892+
throw triton::exceptions::Ast("IffNode::init(): Must take a logical node as first argument.");
1893+
1894+
if (this->children[1]->isLogical() == false)
1895+
throw triton::exceptions::Ast("IffNode::init(): Must take a logical node as second argument.");
1896+
1897+
/* Init attributes */
1898+
triton::uint512 P = this->children[0]->evaluate();
1899+
triton::uint512 Q = this->children[1]->evaluate();
1900+
1901+
this->size = 1;
1902+
this->eval = (P && Q) || (!P && !Q);
1903+
1904+
/* Init children and spread information */
1905+
for (triton::uint32 index = 0; index < this->children.size(); index++) {
1906+
this->children[index]->setParent(this);
1907+
this->symbolized |= this->children[index]->isSymbolized();
1908+
}
1909+
1910+
/* Init parents */
1911+
this->initParents();
1912+
}
1913+
1914+
1915+
triton::uint512 IffNode::hash(triton::uint32 deep) const {
1916+
triton::uint512 h = this->type, s = this->children.size();
1917+
if (s) h = h * s;
1918+
for (triton::uint32 index = 0; index < this->children.size(); index++)
1919+
h = h * triton::ast::hash2n(this->children[index]->hash(deep+1), index+1);
1920+
return triton::ast::rotl(h, deep);
1921+
}
1922+
1923+
18771924
/* ====== ite */
18781925

18791926

@@ -2405,6 +2452,7 @@ namespace triton {
24052452
case DISTINCT_NODE: newNode = std::make_shared<DistinctNode>(*reinterpret_cast<DistinctNode*>(node)); break;
24062453
case EQUAL_NODE: newNode = std::make_shared<EqualNode>(*reinterpret_cast<EqualNode*>(node)); break;
24072454
case EXTRACT_NODE: newNode = std::make_shared<ExtractNode>(*reinterpret_cast<ExtractNode*>(node)); break;
2455+
case IFF_NODE: newNode = std::make_shared<IffNode>(*reinterpret_cast<IffNode*>(node)); break;
24082456
case ITE_NODE: newNode = std::make_shared<IteNode>(*reinterpret_cast<IteNode*>(node)); break;
24092457
case LAND_NODE: newNode = std::make_shared<LandNode>(*reinterpret_cast<LandNode*>(node)); break;
24102458
case LET_NODE: newNode = std::make_shared<LetNode>(*reinterpret_cast<LetNode*>(node)); break;

‎src/libtriton/ast/astContext.cpp

+9
Original file line numberDiff line numberDiff line change
@@ -421,6 +421,15 @@ namespace triton {
421421
}
422422

423423

424+
SharedAbstractNode AstContext::iff(const SharedAbstractNode& expr1, const SharedAbstractNode& expr2) {
425+
SharedAbstractNode node = std::make_shared<IffNode>(expr1, expr2);
426+
if (node == nullptr)
427+
throw triton::exceptions::Ast("Node builders - Not enough memory");
428+
node->init();
429+
return node;
430+
}
431+
432+
424433
SharedAbstractNode AstContext::ite(const SharedAbstractNode& ifExpr, const SharedAbstractNode& thenExpr, const SharedAbstractNode& elseExpr) {
425434
SharedAbstractNode node = std::make_shared<IteNode>(ifExpr, thenExpr, elseExpr);
426435
if (node == nullptr)

‎src/libtriton/ast/representations/astPythonRepresentation.cpp

+8
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ namespace triton {
6161
case DISTINCT_NODE: return this->print(stream, reinterpret_cast<triton::ast::DistinctNode*>(node)); break;
6262
case EQUAL_NODE: return this->print(stream, reinterpret_cast<triton::ast::EqualNode*>(node)); break;
6363
case EXTRACT_NODE: return this->print(stream, reinterpret_cast<triton::ast::ExtractNode*>(node)); break;
64+
case IFF_NODE: return this->print(stream, reinterpret_cast<triton::ast::IffNode*>(node)); break;
6465
case ITE_NODE: return this->print(stream, reinterpret_cast<triton::ast::IteNode*>(node)); break;
6566
case LAND_NODE: return this->print(stream, reinterpret_cast<triton::ast::LandNode*>(node)); break;
6667
case LET_NODE: return this->print(stream, reinterpret_cast<triton::ast::LetNode*>(node)); break;
@@ -365,6 +366,13 @@ namespace triton {
365366
}
366367

367368

369+
/* iff representation */
370+
std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::IffNode* node) {
371+
stream << "(" << node->getChildren()[0] << " and " << node->getChildren()[1] << ") or (not " << node->getChildren()[0] << " and not " << node->getChildren()[1] << ")";
372+
return stream;
373+
}
374+
375+
368376
/* ite representation */
369377
std::ostream& AstPythonRepresentation::print(std::ostream& stream, triton::ast::IteNode* node) {
370378
stream << "(" << node->getChildren()[1] << " if " << node->getChildren()[0] << " else " << node->getChildren()[2] << ")";

‎src/libtriton/ast/representations/astSmtRepresentation.cpp

+8
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ namespace triton {
6161
case DISTINCT_NODE: return this->print(stream, reinterpret_cast<triton::ast::DistinctNode*>(node)); break;
6262
case EQUAL_NODE: return this->print(stream, reinterpret_cast<triton::ast::EqualNode*>(node)); break;
6363
case EXTRACT_NODE: return this->print(stream, reinterpret_cast<triton::ast::ExtractNode*>(node)); break;
64+
case IFF_NODE: return this->print(stream, reinterpret_cast<triton::ast::IffNode*>(node)); break;
6465
case ITE_NODE: return this->print(stream, reinterpret_cast<triton::ast::IteNode*>(node)); break;
6566
case LAND_NODE: return this->print(stream, reinterpret_cast<triton::ast::LandNode*>(node)); break;
6667
case LET_NODE: return this->print(stream, reinterpret_cast<triton::ast::LetNode*>(node)); break;
@@ -361,6 +362,13 @@ namespace triton {
361362
}
362363

363364

365+
/* iff representation */
366+
std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::IffNode* node) {
367+
stream << "(iff " << node->getChildren()[0] << " " << node->getChildren()[1] << ")";
368+
return stream;
369+
}
370+
371+
364372
/* ite representation */
365373
std::ostream& AstSmtRepresentation::print(std::ostream& stream, triton::ast::IteNode* node) {
366374
stream << "(ite " << node->getChildren()[0] << " " << node->getChildren()[1] << " " << node->getChildren()[2] << ")";

‎src/libtriton/ast/z3/tritonToZ3Ast.cpp

+7
Original file line numberDiff line numberDiff line change
@@ -186,6 +186,13 @@ namespace triton {
186186
return to_expr(this->context, Z3_mk_extract(this->context, hv, lv, value));
187187
}
188188

189+
case IFF_NODE: {
190+
z3::expr op1 = this->convert(node->getChildren()[0]);
191+
z3::expr op2 = this->convert(node->getChildren()[1]);
192+
193+
return to_expr(this->context, Z3_mk_iff(this->context, op1, op2));
194+
}
195+
189196
case ITE_NODE: {
190197
z3::expr op1 = this->convert(node->getChildren()[0]); // condition
191198
z3::expr op2 = this->convert(node->getChildren()[1]); // if true

‎src/libtriton/ast/z3/z3ToTritonAst.cpp

+7
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,13 @@ namespace triton {
5656
break;
5757
}
5858

59+
case Z3_OP_IFF: {
60+
if (expr.num_args() != 2)
61+
throw triton::exceptions::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_IFF must contain two arguments.");
62+
node = this->astCtxt.iff(this->convert(expr.arg(0)), this->convert(expr.arg(1)));
63+
break;
64+
}
65+
5966
case Z3_OP_ITE: {
6067
if (expr.num_args() != 3)
6168
throw triton::exceptions::AstTranslations("Z3ToTritonAst::visit(): Z3_OP_ITE must contain three arguments.");

‎src/libtriton/bindings/python/objects/pyAstContext.cpp

+27
Original file line numberDiff line numberDiff line change
@@ -401,6 +401,10 @@ e.g: `(= expr1 epxr2)`.
401401
Creates an `extract` node. The `high` and `low` fields represent the bits position.<br>
402402
e.g: `((_ extract high low) expr1)`.
403403
404+
- <b>\ref py_AstNode_page iff(\ref py_AstNode_page expr1, \ref py_AstNode_page expr2)</b><br>
405+
Creates an `iff` node (if and only if).<br>
406+
e.g: `(iff expr1 expr2)`.
407+
404408
- <b>\ref py_AstNode_page ite(\ref py_AstNode_page ifExpr, \ref py_AstNode_page thenExpr, \ref py_AstNode_page elseExpr)</b><br>
405409
Creates an `ite` node (if-then-else node).<br>
406410
e.g: `(ite ifExpr thenExpr elseExpr)`.
@@ -1268,6 +1272,28 @@ namespace triton {
12681272
}
12691273

12701274

1275+
static PyObject* AstContext_iff(PyObject* self, PyObject* args) {
1276+
PyObject* op1 = nullptr;
1277+
PyObject* op2 = nullptr;
1278+
1279+
/* Extract arguments */
1280+
PyArg_ParseTuple(args, "|OO", &op1, &op2);
1281+
1282+
if (op1 == nullptr || !PyAstNode_Check(op1))
1283+
return PyErr_Format(PyExc_TypeError, "iff(): expected a AstNode as first argument");
1284+
1285+
if (op2 == nullptr || !PyAstNode_Check(op2))
1286+
return PyErr_Format(PyExc_TypeError, "iff(): expected a AstNode as second argument");
1287+
1288+
try {
1289+
return PyAstNode(PyAstContext_AsAstContext(self)->iff(PyAstNode_AsAstNode(op1), PyAstNode_AsAstNode(op2)));
1290+
}
1291+
catch (const triton::exceptions::Exception& e) {
1292+
return PyErr_Format(PyExc_TypeError, "%s", e.what());
1293+
}
1294+
}
1295+
1296+
12711297
static PyObject* AstContext_ite(PyObject* self, PyObject* args) {
12721298
PyObject* op1 = nullptr;
12731299
PyObject* op2 = nullptr;
@@ -1508,6 +1534,7 @@ namespace triton {
15081534
{"duplicate", AstContext_duplicate, METH_O, ""},
15091535
{"equal", AstContext_equal, METH_VARARGS, ""},
15101536
{"extract", AstContext_extract, METH_VARARGS, ""},
1537+
{"iff", AstContext_iff, METH_VARARGS, ""},
15111538
{"ite", AstContext_ite, METH_VARARGS, ""},
15121539
{"land", AstContext_land, METH_O, ""},
15131540
{"let", AstContext_let, METH_VARARGS, ""},

‎src/libtriton/includes/triton/ast.hpp

+9
Original file line numberDiff line numberDiff line change
@@ -521,6 +521,15 @@ namespace triton {
521521
};
522522

523523

524+
//! `(iff <expr1> <expr2>)`
525+
class IffNode : public AbstractNode {
526+
public:
527+
TRITON_EXPORT IffNode(const SharedAbstractNode& expr1, const SharedAbstractNode& expr2);
528+
TRITON_EXPORT void init(void);
529+
TRITON_EXPORT triton::uint512 hash(triton::uint32 deep) const;
530+
};
531+
532+
524533
//! `(ite <ifExpr> <thenExpr> <elseExpr>)`
525534
class IteNode : public AbstractNode {
526535
public:

‎src/libtriton/includes/triton/astContext.hpp

+3
Original file line numberDiff line numberDiff line change
@@ -208,6 +208,9 @@ namespace triton {
208208
//! AST C++ API - extract node builder
209209
TRITON_EXPORT SharedAbstractNode extract(triton::uint32 high, triton::uint32 low, const SharedAbstractNode& expr);
210210

211+
//! AST C++ API - iff node builder
212+
TRITON_EXPORT SharedAbstractNode iff(const SharedAbstractNode& expr1, const SharedAbstractNode& expr2);
213+
211214
//! AST C++ API - ite node builder
212215
TRITON_EXPORT SharedAbstractNode ite(const SharedAbstractNode& ifExpr, const SharedAbstractNode& thenExpr, const SharedAbstractNode& elseExpr);
213216

‎src/libtriton/includes/triton/astEnums.hpp

+11-10
Original file line numberDiff line numberDiff line change
@@ -66,16 +66,17 @@ namespace triton {
6666
DISTINCT_NODE = 163, /*!< (distinct x y) */
6767
EQUAL_NODE = 167, /*!< (= x y) */
6868
EXTRACT_NODE = 173, /*!< ((_ extract x y) z) */
69-
ITE_NODE = 181, /*!< (ite x y z) */
70-
LAND_NODE = 191, /*!< (and x y) */
71-
LET_NODE = 193, /*!< (let ((x y)) z) */
72-
LNOT_NODE = 197, /*!< (and x y) */
73-
LOR_NODE = 199, /*!< (or x y) */
74-
REFERENCE_NODE = 223, /*!< Reference node */
75-
STRING_NODE = 227, /*!< String node */
76-
SX_NODE = 229, /*!< ((_ sign_extend x) y) */
77-
VARIABLE_NODE = 233, /*!< Variable node */
78-
ZX_NODE = 239, /*!< ((_ zero_extend x) y) */
69+
IFF_NODE = 181, /*!< (iff x y) */
70+
ITE_NODE = 191, /*!< (ite x y z) */
71+
LAND_NODE = 193, /*!< (and x y) */
72+
LET_NODE = 197, /*!< (let ((x y)) z) */
73+
LNOT_NODE = 199, /*!< (and x y) */
74+
LOR_NODE = 223, /*!< (or x y) */
75+
REFERENCE_NODE = 227, /*!< Reference node */
76+
STRING_NODE = 229, /*!< String node */
77+
SX_NODE = 233, /*!< ((_ sign_extend x) y) */
78+
VARIABLE_NODE = 239, /*!< Variable node */
79+
ZX_NODE = 241, /*!< ((_ zero_extend x) y) */
7980
};
8081

8182
//! The Representations namespace

‎src/libtriton/includes/triton/astPythonRepresentation.hpp

+3
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,9 @@ namespace triton {
162162
//! Displays the node according to the representation mode.
163163
TRITON_EXPORT std::ostream& print(std::ostream& stream, triton::ast::ExtractNode* node);
164164

165+
//! Displays the node according to the representation mode.
166+
TRITON_EXPORT std::ostream& print(std::ostream& stream, triton::ast::IffNode* node);
167+
165168
//! Displays the node according to the representation mode.
166169
TRITON_EXPORT std::ostream& print(std::ostream& stream, triton::ast::IteNode* node);
167170

‎src/libtriton/includes/triton/astSmtRepresentation.hpp

+3
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,9 @@ namespace triton {
162162
//! Displays the node according to the representation mode.
163163
TRITON_EXPORT std::ostream& print(std::ostream& stream, triton::ast::ExtractNode* node);
164164

165+
//! Displays the node according to the representation mode.
166+
TRITON_EXPORT std::ostream& print(std::ostream& stream, triton::ast::IffNode* node);
167+
165168
//! Displays the node according to the representation mode.
166169
TRITON_EXPORT std::ostream& print(std::ostream& stream, triton::ast::IteNode* node);
167170

‎src/testers/unittests/test_ast_conversion.py

+5-1
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,7 @@ def test_smtbinop(self):
144144
self.astCtxt.concat,
145145
self.astCtxt.distinct,
146146
self.astCtxt.equal,
147+
self.astCtxt.iff,
147148
self.astCtxt.land,
148149
self.astCtxt.lor,
149150
]
@@ -157,7 +158,9 @@ def test_smtbinop(self):
157158
if op == self.astCtxt.concat:
158159
n = op([self.v1, self.v2])
159160
elif op in (self.astCtxt.land, self.astCtxt.lor):
160-
n = op([self.v1 != 0, self.v2 != 0])
161+
n = op([self.v1 != cv1, self.v2 != cv2])
162+
elif op == self.astCtxt.iff:
163+
n = op(self.v1 > cv1, self.v2 < cv2)
161164
else:
162165
n = op(self.v1, self.v2)
163166
self.assertEqual(n.evaluate(),
@@ -272,6 +275,7 @@ def test_fuzz(self):
272275
(self.astCtxt.lnot, 1),
273276
(self.astCtxt.land, 2),
274277
(self.astCtxt.lor, 2),
278+
(self.astCtxt.iff, 2),
275279
]
276280
self.to_bool = [
277281
(self.astCtxt.bvsge, 2),

‎src/testers/unittests/test_ast_duplication.py

+1
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ def setUp(self):
6161
self.astCtxt.concat([self.v1, self.v2]),
6262
self.astCtxt.distinct(self.v1, self.v2),
6363
self.astCtxt.equal(self.v1, self.v2),
64+
self.astCtxt.iff(self.v1 == self.v1, self.v2 == self.v1),
6465
self.astCtxt.extract(4, 2, self.v1),
6566
self.astCtxt.extract(7, 0, self.v1),
6667
self.astCtxt.ite(self.v1 == 2, self.v1, self.v2),

‎src/testers/unittests/test_ast_eval.py

+10
Original file line numberDiff line numberDiff line change
@@ -802,6 +802,16 @@ def test_srem(self):
802802
]
803803
self.check_ast(tests)
804804

805+
def test_iff(self):
806+
"""Check iff operations."""
807+
tests = [
808+
self.astCtxt.iff(self.astCtxt.equal(self.astCtxt.bv(1, 8), self.astCtxt.bv(1, 8)), self.astCtxt.equal(self.astCtxt.bv(1, 8), self.astCtxt.bv(1, 8))),
809+
self.astCtxt.iff(self.astCtxt.equal(self.astCtxt.bv(1, 8), self.astCtxt.bv(1, 8)), self.astCtxt.equal(self.astCtxt.bv(2, 8), self.astCtxt.bv(1, 8))),
810+
self.astCtxt.iff(self.astCtxt.equal(self.astCtxt.bv(1, 8), self.astCtxt.bv(2, 8)), self.astCtxt.equal(self.astCtxt.bv(1, 8), self.astCtxt.bv(1, 8))),
811+
self.astCtxt.iff(self.astCtxt.equal(self.astCtxt.bv(1, 8), self.astCtxt.bv(2, 8)), self.astCtxt.equal(self.astCtxt.bv(2, 8), self.astCtxt.bv(1, 8))),
812+
]
813+
self.check_ast(tests)
814+
805815
def test_reference(self):
806816
"""Check evaluation of reference node after variable update."""
807817
self.sv1 = self.Triton.newSymbolicVariable(8)

‎src/testers/unittests/test_ast_representation.py

+1
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,7 @@ def setUp(self):
7272
(self.astCtxt.extract(4, 2, self.v1), "((_ extract 4 2) SymVar_0)", "((SymVar_0 >> 2) & 0x7)"),
7373
(self.astCtxt.extract(6, 0, self.v1), "((_ extract 6 0) SymVar_0)", "(SymVar_0 & 0x7F)"),
7474
(self.astCtxt.extract(7, 0, self.v1), "SymVar_0", "SymVar_0"),
75+
(self.astCtxt.iff(self.v1 == 1, self.v2 == 2), "(iff (= SymVar_0 (_ bv1 8)) (= SymVar_1 (_ bv2 8)))", "((SymVar_0 == 0x1) and (SymVar_1 == 0x2)) or (not (SymVar_0 == 0x1) and not (SymVar_1 == 0x2))"),
7576
(self.astCtxt.ite(self.v1 == 1, self.v1, self.v2), "(ite (= SymVar_0 (_ bv1 8)) SymVar_0 SymVar_1)", "(SymVar_0 if (SymVar_0 == 0x1) else SymVar_1)"),
7677
(self.astCtxt.land([self.v1 == 1, self.v2 == 2]), "(and (= SymVar_0 (_ bv1 8)) (= SymVar_1 (_ bv2 8)))", "((SymVar_0 == 0x1) and (SymVar_1 == 0x2))"),
7778
(self.astCtxt.let("alias", self.v1, self.v2), "(let ((alias SymVar_0)) SymVar_1)", "SymVar_1"),

‎src/testers/unittests/test_ast_undefined.py ‎src/testers/unittests/test_undefined_registers.py

+3-4
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
#!/usr/bin/env python2
22
# coding: utf-8
3-
"""Test architectures."""
3+
"""Test the undefined register behavior."""
44

55
import unittest
66
from triton import *
77

88

9-
class TestASTUndefined(unittest.TestCase):
9+
class TestUndefinedRegisters(unittest.TestCase):
1010

11-
"""Testing the undefined node."""
11+
"""Testing the undefined register behavior."""
1212

1313
def setUp(self):
1414
"""Define the arch."""
@@ -64,4 +64,3 @@ def test_undefined_off(self):
6464
self.assertEqual(REG.X86_64.ZF in self.ctx.getSymbolicRegisters(), True)
6565
self.assertEqual(REG.X86_64.AF in self.ctx.getSymbolicRegisters(), True)
6666
self.assertEqual(REG.X86_64.PF in self.ctx.getSymbolicRegisters(), True)
67-

0 commit comments

Comments
 (0)