search

GaloisInc / crucible

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

Assumptions/Assertions inaccessible to execution features #763

Open robdockins opened 3 years ago

robdockins commented 3 years ago

The bookeeping for making logical assumptions or assertions about programs under simulation is currently handled by the Lang.Crucible.Backend module, which exposes the IsBoolSolver API. This API is designed to cooperate closely with the steps of the symbolic simulator, and maintains stacks of assumptions that closely correspond to the control-flow paths followed by simulation.

Because this bookkeeping is done entirely internally, it isn't possible for an ExecutionFeature to monitor or take action when assumptions or assertions are made. I think it would be better design to rework this part of the API so that these events are exposed as part of the execution of programs and reorganize, e.g. the OnlineBackend as an execution feature instead. The motivation for this is the desire for Crux to keep track of events that occur along the execution of a program, and attach those events to proof goals. Currently, there isn't an easy way to do this.

RyanGlScott commented 2 years ago

@robdockins, was this issue addressed by #945, or did that solve a different problem?

robdockins commented 2 years ago

That solved a different, but related, problem.