tritonToZ3 seg fault #1024
Assignees
Labels
Comments
|
I've just tried. >>> from triton import *
>>> Triton = TritonContext()
>>> astctx = Triton.getAstContext()
>>>
>>> Triton.setArchitecture(ARCH.X86_64)
>>> insn = Instruction()
>>> insn.setOpcode(b"\x48\x01\xD8")
>>> Triton.processing(insn)
True
>>> sexpr = insn.getSymbolicExpressions()[0]
>>> ast = sexpr.getAst()
>>> ast
(bvadd (_ bv0 64) (_ bv0 64))
>>> astctx.tritonToZ3(ast)
0 + 0
>>>Make sure your z3 headers used at the compile are the same as the libz3.so linked to libtriton.so |
|
Also, make sure that |
|
4.8.11 is not 4.8.10. I repeat it's not a Triton issue, it's related to the way you compile triton with different z3 versions on your system. |
|
versions are equal: also throws a seg fault |
|
Is the version you used to compile triton is also the 4.8.10? |
|
Is the version you used to compile triton is also the 4.8.10? - yes gdb state:
Program received signal SIGSEGV, Segmentation fault. argc=1, argv=0x7fffffffe018, init=, fini=, rtld_fini=, stack_end=0x7fffffffe008) at ../csu/libc-start.c:308 #15 0x00000000005f9ece in _start () |
|
Maybe building with z3 from master will help? |
|
Ok. I've pulled the version |
|
@sh4m2hwz can you try this following patch? diff --git a/src/libtriton/bindings/python/objects/pyAstContext.cpp b/src/libtriton/bindings/python/objects/pyAstContext.cpp
index 1b0b422c..b65289d4 100644
--- a/src/libtriton/bindings/python/objects/pyAstContext.cpp
+++ b/src/libtriton/bindings/python/objects/pyAstContext.cpp
@@ -1592,20 +1592,17 @@ namespace triton {
return PyErr_Format(PyExc_TypeError, "tritonToZ3(): z3 module not found.");
}
- // z3.main_ctx().ctx.value
PyObject* z3MainCtx = PyObject_CallObject(PyObject_GetAttrString(z3mod, "main_ctx"), nullptr);
- PyObject* z3CtxPtr = PyObject_GetAttrString(PyObject_GetAttrString(z3MainCtx, "ctx"), "value");
- Z3_context z3Ctx = reinterpret_cast<Z3_context>(PyLong_AsVoidPtr(z3CtxPtr));
- Py_DECREF(z3CtxPtr);
- Py_DECREF(z3MainCtx);
+ z3::context* z3Ctx = new z3::context(); // FIXME: memory leak
+ PyObject_SetAttrString(PyObject_GetAttrString(z3MainCtx, "ctx"), "value", PyLong_FromVoidPtr(z3Ctx));
// Convert the node to a Z3++ expression and translate it into
// python's z3 main context
z3::expr expr = tritonToZ3Ast.convert(PyAstNode_AsAstNode(node));
- Z3_ast ast = Z3_translate(expr.ctx(), expr, z3Ctx);
+ Z3_ast ast = Z3_translate(expr.ctx(), expr, *z3Ctx);
// Check that everything went fine
- if (Z3_get_error_code(z3Ctx) != Z3_OK) {
+ if (Z3_get_error_code(*z3Ctx) != Z3_OK) {
Py_DECREF(z3mod);
return PyErr_Format(PyExc_RuntimeError, "tritonToZ3(): Z3 AST translation failed.");
}
@@ -1626,7 +1623,6 @@ namespace triton {
// Cleanup
Py_DECREF(z3mod);
-
return retExpr;
} |
|
patch don't work for smaller constraints, medium or bigger size constraints: |
|
Ok, well i don't know how to fix this as Z3 do not provides CPython API... So translating a z3 C++ object to a python object (PyObject*) is kind of hacky. Everything is done here, if you have some ideas... |
|
Hi captain! My snippet to reproduce it: from triton import *
ctx = TritonContext(ARCH.X86_64)
actx = ctx.getAstContext()
rax = ctx.symbolizeRegister(ctx.registers.rax)
expr = ctx.newSymbolicExpression(actx.variable(rax) == 12)
e_z3 = actx.tritonToZ3(expr.getAst())Note: that liftToSMT is not really suitable as I need to push / pop constaints by reusing the same SMT solver object. |
|
Hey Admiral. Mmmmh, ok fun fact but since this issue was opened it looks like they fixed the issue on z3 side. All PoC posted in this thread work with So to resume it looks like Z3 team changed something on their API from |
|
For the record, @cnheitman pinpointed the issue. The libz3.so used between triton and the z3 python module should be the same library ! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The text was updated successfully, but these errors were encountered: