GaloisInc / crucible

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

Don't `panic` in `AssumptionStack.popFrame` #1168

Open langston-barrett opened 7 months ago

langston-barrett commented 7 months ago

Consider the following program, written against Crucible's public API:

module Main where

import Prelude
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Lang.Crucible.Backend.AssumptionStack

main :: IO ()
main = do
  Some gen <- newIONonceGenerator
  stk <- initAssumptionStack gen
  frameId <- pushFrame stk
  _frameId <- pushFrame stk
  _result <- popFrame @() frameId stk
  putStrLn "No panic?"

This program panics:

%< ---------------------------------------------------
  Revision:  bb50c0d16922e13d6358ce9abc7042ed13feccab
  Branch:    master
  Location:  AssumptionStack.popFrame
  Message:   Push/pop mismatch in assumption stack!
             *** Current frame:  0
             *** Expected ident: 1
CallStack (from HasCallStack):
  panic, called at src/Lang/Crucible/Panic.hs:11:9 in crucible-0.6-inplace:Lang.Crucible.Panic
  panic, called at src/Lang/Crucible/Backend/AssumptionStack.hs:204:16 in crucible-0.6-inplace:Lang.Crucible.Backend.AssumptionStack
%< ---------------------------------------------------

I would argue that I have not found a bug in Crucible. More specifically, the only bug here is that this function calls panic when passed invalid arguments, but is exposed via a public API where such arguments may, in fact, be passed. This panic (and others like it) should either be reified in the return type (e.g., Either), or turned into a dedicated Exception instance (which should be noted in the Haddocks). Panics should be reserved for situations that are considered by Crucible to be literally impossible.

RyanGlScott commented 7 months ago

I agree. It would nice to be able to recover more gracefully in situations like this, so this change would be welcome.