Refactor AssumptionStack

crucible/CHANGELOG.md

@@ -1,3 +1,8 @@
+# next
+
+* Rename `Lang.Crucible.Backend.popFrame` to `popFrameOrPanic`,
+  provide helpers such as `popFrame` to manage assumptions without `panic`ing.
+
 # 0.6
 
 * Separate backend data structures.  The "symbolic backend" is a

crucible/src/Lang/Crucible/Backend/AssumptionStack.hs

@@ -18,6 +18,7 @@ solvers.
 -}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -32,13 +33,15 @@ module Lang.Crucible.Backend.AssumptionStack
   , FrameIdentifier
   , AssumptionFrame(..)
   , AssumptionFrames(..)
-  , AssumptionStack(..)
+  , AssumptionStack
     -- ** Manipulating assumption stacks
   , initAssumptionStack
   , saveAssumptionStack
   , restoreAssumptionStack
   , pushFrame
+  , PopFrameError(..)
   , popFrame
+  , popFrameOrPanic
   , popFrameAndGoals
   , popFramesUntil
   , resetStack
@@ -54,10 +57,13 @@ module Lang.Crucible.Backend.AssumptionStack
   ) where
 
 import           Control.Exception (bracketOnError)
+import           Data.Functor ((<&>))
 import qualified Data.Foldable as F
 import           Data.IORef
 import           Data.Parameterized.Nonce
 
+import qualified Prettyprinter as PP
+
 import           Lang.Crucible.Backend.ProofGoals
 import           Lang.Crucible.Panic (panic)
 
@@ -173,12 +179,10 @@ popFramesUntil ident stk = atomicModifyIORef' (proofObligations stk) (go 1)
  where
  go n gc =
     case gcPop gc of
-      Left (ident', _assumes, mg, gc1)
-        | ident == ident' -> (gc',n)
+      Left frm
+        | ident == poppedFrameId frm -> (gc',n)
         | otherwise -> go (n+1) gc'
-       where gc' = case mg of
-                     Nothing -> gc1
-                     Just g  -> gcAddGoals g gc1
+       where gc' = collectPoppedGoals frm
       Right _ ->
         panic "AssumptionStack.popFrameUntil"
           [ "Frame not found in stack."
@@ -187,60 +191,84 @@ popFramesUntil ident stk = atomicModifyIORef' (proofObligations stk) (go 1)
 
  showFrameId (FrameIdentifier x) = show x
 
+-- | Call 'gcPop' on the 'proofObligations' of this 'AssumptionStack'
+popFrameUnchecked ::
+  Monoid asmp =>
+  AssumptionStack asmp ast ->
+  IO (Either (PoppedFrame asmp ast) (Maybe (Goals asmp ast)))
+popFrameUnchecked stk =
+  atomicModifyIORef' (proofObligations stk) $ \gc ->
+    case gcPop gc of
+      Left frm -> (collectPoppedGoals frm, Left frm)
+      Right mgs -> (gc, Right mgs)
+
+data PopFrameError
+  = NoFrames
+    -- | Expected, actual
+  | WrongFrame FrameIdentifier FrameIdentifier
+
+instance PP.Pretty PopFrameError where
+  pretty =
+    \case
+      NoFrames -> PP.pretty "Pop with no push in goal collector."
+      WrongFrame expected actual ->
+        PP.hsep
+          [ PP.pretty "Mismatch in assumption stack frames."
+          , PP.pretty "Expected ident:"
+          , PP.viaShow expected
+          , PP.pretty "Current frame:"
+          , PP.viaShow actual
+          ]
+
+instance Show PopFrameError where
+  show = show . PP.pretty
+
 -- | Pop a previously-pushed assumption frame from the stack.
 --   All assumptions in that frame will be forgotten.  The
 --   assumptions contained in the popped frame are returned.
-popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
+--
+--   Returns 'Left' if there are no frames on the stack, or if the top frame
+--   doesn\'t have the provided 'FrameIdentifier'.
+popFrame ::
+  Monoid asmp =>
+  FrameIdentifier ->
+  AssumptionStack asmp ast ->
+  IO (Either PopFrameError (PoppedFrame asmp ast))
 popFrame ident stk =
-  atomicModifyIORef' (proofObligations stk) $ \gc ->
-       case gcPop gc of
-         Left (ident', assumes, mg, gc1)
-           | ident == ident' ->
-                let gc' = case mg of
-                            Nothing -> gc1
-                            Just g  -> gcAddGoals g gc1
-                 in (gc', assumes)
-           | otherwise ->
-               panic "AssumptionStack.popFrame"
-                [ "Push/pop mismatch in assumption stack!"
-                , "*** Current frame:  " ++ showFrameId ident
-                , "*** Expected ident: " ++ showFrameId ident'
-                ]
-         Right _  ->
-           panic "AssumptionStack.popFrame"
-             [ "Pop with no push in goal collector."
-             , "*** Current frame: " ++ showFrameId ident
-             ]
-
-  where
-  showFrameId (FrameIdentifier x) = show x
+  popFrameUnchecked stk <&>
+    \case
+      Left frm
+        | ident == poppedFrameId frm -> Right frm
+        | otherwise -> Left (WrongFrame ident (poppedFrameId frm))
+      Right _ -> Left NoFrames
 
+-- | Pop a previously-pushed assumption frame from the stack.
+--   All assumptions in that frame will be forgotten.  The
+--   assumptions contained in the popped frame are returned.
+--
+--   Panics if there are no frames on the stack, or if the top frame doesn\'t
+--   have the provided 'FrameIdentifier'.
+popFrameOrPanic :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp
+popFrameOrPanic ident stk =
+  popFrame ident stk <&>
+    \case
+      Left err -> panic "AssumptionStack.popFrame" [show err]
+      Right frm -> poppedAssumptions frm
 
+-- | Pop the assumptions and goals from the top frame.
+--
+--   Panics if there are no frames on the stack, or if the top frame doesn\'t
+--   have the provided 'FrameIdentifier'.
 popFrameAndGoals ::
   Monoid asmp =>
   FrameIdentifier ->
   AssumptionStack asmp ast ->
   IO (asmp, Maybe (Goals asmp ast))
 popFrameAndGoals ident stk =
-  atomicModifyIORef' (proofObligations stk) $ \gc ->
-       case gcPop gc of
-         Left (ident', assumes, mg, gc1)
-           | ident == ident' -> (gc1, (assumes, mg))
-           | otherwise ->
-               panic "AssumptionStack.popFrameAndGoals"
-                [ "Push/pop mismatch in assumption stack!"
-                , "*** Current frame:  " ++ showFrameId ident
-                , "*** Expected ident: " ++ showFrameId ident'
-                ]
-         Right _  ->
-           panic "AssumptionStack.popFrameAndGoals"
-             [ "Pop with no push in goal collector."
-             , "*** Current frame: " ++ showFrameId ident
-             ]
-
-  where
-  showFrameId (FrameIdentifier x) = show x
-
+  popFrame ident stk <&>
+    \case
+      Left err -> panic "AssumptionStack.popFrameAndGoals" [show err]
+      Right frm -> (poppedAssumptions frm, poppedGoals frm)
 
 -- | Run an action in the scope of a fresh assumption frame.
 --   The frame will be popped and returned on successful
@@ -252,5 +280,5 @@ inFreshFrame stk action =
      (pushFrame stk)
      (\ident -> popFrame ident stk)
      (\ident -> do x <- action
-                   frm <- popFrame ident stk
+                   frm <- popFrameOrPanic ident stk
                    return (frm, x))

crucible/src/Lang/Crucible/Backend/Online.hs

@@ -579,7 +579,7 @@ instance (IsSymInterface (B.ExprBuilder scope st fs), OnlineSolver solver) =>
 
   popAssumptionFrame bak ident =
     -- NB, pop the frame whether or not the solver pop succeeds
-    do frm <- popFrame ident (assumptionStack bak)
+    do frm <- popFrameOrPanic ident (assumptionStack bak)
        withSolverProcess bak (pure ()) pop
        return frm
 

crucible/src/Lang/Crucible/Backend/ProofGoals.hs

@@ -28,6 +28,8 @@ module Lang.Crucible.Backend.ProofGoals
   , traverseGoalCollectorWithAssumptions
 
     -- ** Context management
+  , PoppedFrame(..)
+  , collectPoppedGoals
   , gcAddAssumes, gcProve
   , gcPush, gcPop, gcAddGoals,
 
@@ -265,23 +267,35 @@ gcAddAssumes :: Monoid asmp => asmp -> GoalCollector asmp goal -> GoalCollector
 gcAddAssumes as' (CollectingAssumptions as gls) = CollectingAssumptions (as <> as') gls
 gcAddAssumes as' gls = CollectingAssumptions as' gls
 
-{- | Pop to the last push, or all the way to the top, if there were no more pushes.
-If the result is 'Left', then we popped until an explicitly marked push;
-in that case we return:
-
-    1. the frame identifier of the popped frame,
-    2. the assumptions that were forgotten,
-    3. any proof goals that were generated since the frame push, and
-    4. the state of the collector before the push.
+-- | A frame, popped by 'gcPop'
+data PoppedFrame asmp goal
+  = PoppedFrame
+    { -- | The frame identifier of the popped frame
+      poppedFrameId :: !FrameIdentifier
+      -- | The assumptions that were forgotten by the pop
+    , poppedAssumptions :: asmp
+      -- | Any proof goals that were generated since the frame push
+    , poppedGoals :: Maybe (Goals asmp goal)
+      -- | The state of the collector before the push.
+    , poppedCollector :: GoalCollector asmp goal
+    }
+
+-- | Retrieve the 'GoalCollector' from a 'PoppedFrame', adding the
+-- 'poppedGoals' (if there are any) via 'gcAddGoals'.
+collectPoppedGoals :: PoppedFrame asmp goal -> GoalCollector asmp goal
+collectPoppedGoals frm =
+  case poppedGoals frm of
+    Nothing -> poppedCollector frm
+    Just goals -> gcAddGoals goals (poppedCollector frm)
 
+{- | Pop to the last push, or all the way to the top, if there were no more pushes.
+If the result is 'Left', then we popped until an explicitly marked push.
 If the result is 'Right', then we popped all the way to the top, and the
 result is the goal tree, or 'Nothing' if there were no goals. -}
-
 gcPop ::
   Monoid asmp =>
   GoalCollector asmp goal ->
-  Either (FrameIdentifier, asmp, Maybe (Goals asmp goal), GoalCollector asmp goal)
-         (Maybe (Goals asmp goal))
+  Either (PoppedFrame asmp goal) (Maybe (Goals asmp goal))
 gcPop = go Nothing mempty
   where
 
@@ -293,7 +307,7 @@ gcPop = go Nothing mempty
     Right (goalsConj (proveAll gs) hole)
 
   go hole as (CollectorFrame fid gc) =
-    Left (fid, as, hole, gc)
+    Left (PoppedFrame fid as hole gc)
 
   go hole as (CollectingAssumptions as' gc) =
     go (assuming as' <$> hole) (as' <> as) gc
@@ -303,10 +317,10 @@ gcPop = go Nothing mempty
 
 -- | Get all currently collected goals.
 gcFinish :: Monoid asmp => GoalCollector asmp goal -> Maybe (Goals asmp goal)
-gcFinish gc = case gcPop gc of
-                Left (_,_,Just g,gc1)  -> gcFinish (gcAddGoals g gc1)
-                Left (_,_,Nothing,gc1) -> gcFinish gc1
-                Right a -> a
+gcFinish gc =
+  case gcPop gc of
+    Left poppedFrame -> gcFinish (collectPoppedGoals poppedFrame)
+    Right a -> a
 
 -- | Reset the goal collector to the empty assumption state; but first
 --   collect all the pending proof goals and stash them.

crucible/src/Lang/Crucible/Backend/Simple.hs

@@ -103,7 +103,7 @@ instance IsSymInterface (B.ExprBuilder t st fs) =>
     AS.pushFrame (sbAssumptionStack bak)
 
   popAssumptionFrame bak ident = do
-    AS.popFrame ident (sbAssumptionStack bak)
+    AS.popFrameOrPanic ident (sbAssumptionStack bak)
 
   popAssumptionFrameAndObligations bak ident = do
     AS.popFrameAndGoals ident (sbAssumptionStack bak)