search

JonathanSalwan / Triton

Triton is a dynamic binary analysis library. Build your own program analysis tools, automate your reverse engineering, perform software verification or just emulate code.
https://triton-library.github.io
Apache License 2.0
3.4k stars 524 forks source link

Fix Bitwuzla VARIABLE_NODE translation #1289

Closed cnheitman closed 9 months ago

cnheitman commented 9 months ago

This PR fix an issue with the in the Triton to Bitwuzla translation for VARIABLE_NODE. If a variable node appears more that once in an expression, different term for that node will be created. That means, bitwuzla_mk_const will return different BitwuzlaTerms for the same symbol. The fix checks whether the term was already created and returns it, otherwise creates a new one.

JonathanSalwan commented 9 months ago

Is it an old bug or is it due to the new bitwuzla version?

cnheitman commented 9 months ago

I think this also happens in the old version of Bitwuzla but I haven't checked.