trailofbits / circuitous

binary->LLVM->circuits
Apache License 2.0
17 stars 6 forks source link

Handle undefined results properly #139

Open lkorenc opened 2 years ago

lkorenc commented 2 years ago

Currently some instruction may leave an output value undefined, e.g. ROR. Ideally, circuit should accept both (we consider OF to be undefined after ->) t1: [ ... ] -> t2: [ OF = 0 ] t1: [ ... ] -> t2: [ OF = 1 ]

In circuitous we have several ways of handling this:

lkorenc commented 2 years ago

See https://github.com/lifting-bits/remill/issues/541 for information about particular semantics and to report newly found inconsistent instructions.