GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
628 stars 42 forks source link

`crucible`: online solver backend does not always gracefully handle the solver process being killed #1159

Open danmatichuk opened 8 months ago

danmatichuk commented 8 months ago

In Lang.Crucible.Backend.Online interactions with the solver process are generally guarded with exception handlers in order to ensure that the solver process is transparently restarted when necessary. However, in some cases closing the IO channel will raise an IO exception despite being wrapped in maybe (i.e. maybe (return ()) hClose auxh). This can potentially get the online solver into an inconsistent state, or get higher-level tools into an inconsistent state.