search

trailofbits / manticore

Symbolic execution tool
https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/
GNU Affero General Public License v3.0
3.69k stars 472 forks source link

Add boolector support #2403

Closed montyly closed 3 years ago

montyly commented 3 years ago

We can leverage dev-evm-experiments to add boolector support

https://github.com/trailofbits/manticore/blob/f0d59ce0021994b9a9b6ea3df3ccfb4719426aad/manticore/core/smtlib/solver.py#L46

https://github.com/trailofbits/manticore/blob/f0d59ce0021994b9a9b6ea3df3ccfb4719426aad/manticore/core/smtlib/solver.py#L1260-L1264

We need to add consts.boolector_bin to prevent boolector to be hardcoded.

Boolector does not work if a variable is named BV, and require to change https://github.com/trailofbits/manticore/blob/3da969bf49c69c2a0f00088a96643d8b1b75264f/manticore/core/smtlib/constraints.py#L396 (master)

To

https://github.com/trailofbits/manticore/blob/f0d59ce0021994b9a9b6ea3df3ccfb4719426aad/manticore/core/smtlib/constraints.py#L397 (dev-evm-experiment)

(or to BITVEC, or another similar name)

ggrieco-tob commented 3 years ago

Which versions of boolector you tested? Ubuntu provides this one:

$ boolector -v
[btormain] Boolector Version 1.5.118 6b56be42e9d2a80527f44ae7ef8b031e8e4ce478
[btormain] gcc (Ubuntu 7.3.0-14ubuntu1) 7.3.0
montyly commented 3 years ago

I used 3.1.0. The latest version is 3.2.1 (https://github.com/Boolector/boolector/releases),

I think we should provide support for the latest version, and be ok if our support does not work with the version on ubuntu packages.

ggrieco-tob commented 3 years ago

Exactly how boolector was compiled? It seems it requires another sat solver. I compiled it using minisat, but I'm not sure that's the "correct" one.