GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
682 stars 44 forks source link

crucible-llvm: Use the "UndefinedBehavior" type in more places during translation #722

Open langston-barrett opened 3 years ago

langston-barrett commented 3 years ago

There are a few spots in LLVM module translation where functions like reportError are used:

https://github.com/GaloisInc/crucible/blob/a42ef5b65faea52d3530d53ed7ac800a3a14f1e3/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs#L1210-L1215

where it may be better to use something that attaches an UndefinedBehavior, like poisonSideCondition:

https://github.com/GaloisInc/crucible/blob/a42ef5b65faea52d3530d53ed7ac800a3a14f1e3/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs#L118-L127

This would be good for two reasons:

One issue I see in Translation.Instruction in particular is that the main way to attach instances of UndefinedBehavior is via side-conditions, whereas in some cases functions like caseptr have been used to the point where the behavior is always undefined in the given branch (the reportError example linked above is an instance of this). In this case, there's no sensible value to return.

There are two approaches I can see to address this:

langston-barrett commented 3 years ago

In addition to reportError, assertExpr is used a lot (indirectly through pointerAsBitvectorExpr) where it would be nice to have a side condition instead.