Stream writer boogie file translation and function trimming for large binaries

UQ-PAC / BASIL

Apache License 2.0

8 stars 0 forks source link

Stream writer boogie file translation and function trimming for large binaries #152

Closed ailrst closed 9 months ago

ailrst commented 10 months ago

Make it so we can again lift cntlm to a state boogie can parse (note you need to give the JVM more memory for the adt to parse).

Changes

use a Writer to output the boogie file rather than concatenating to a string
coalesce the 'constant' data section specifications into 64-bitvectors where allowed rather than always using 8-bitvectors. (the old encoding is preserved but not linked up to a cli flag)
separate specifications from implementations in the boogie output
add options to set the main function and function call depth for the reach-ability trimming, omitting the implementation for the leaf functions
Fixes a bug with the assume() translation with coercing the condition to a bool, since bap seems to output both bools and bitvectors at different times

l-kent commented 10 months ago

Fixes a bug with the assume() translation with coercing the condition to a bool, since bap seems to output both bools and bitvectors at different times

Can you provide an example of this?

l-kent commented 10 months ago

separate specifications from implementations in the boogie output

Is there a particular reason we want to do this now?

ailrst commented 9 months ago

Fixes a bug with the assume() translation with coercing the condition to a bool, since bap seems to output both bools and bitvectors at different times

Can you provide an example of this?

examples/cntlm-new creates conditionals with bvslt9(LocalVar(#3331, bv9), 32bv9) which are type bool.

separate specifications from implementations in the boogie output

Is there a particular reason we want to do this now?

I was thinking it neccessary for omitting the implementation of some of the procedures but it obviously isn't, there's not really a need. It does let you override the spec and implementation separately though.

l-kent commented 9 months ago

It does let you override the spec and implementation separately though.

Is this something we want to do or may want to in future?

examples/cntlm-new creates conditionals with bvslt9(LocalVar(#3331, bv9), 32bv9) which are type bool.

It's great to have an example of BAP actually producing one of those comparison operations, thanks. The tricky thing with the comparator instructions is that technically, directly translating them (as is currently done in BAPtoIR) is incorrect, as the BAP SLT returns a bitvector of size 1, but the SMT/Boogie SLT returns a boolean (BAP doesn't distinguish between these as types but SMT/Boogie do). Knowing these can occur inside the BAP conditionals means we can specifically address them now.