diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md index b9c6e08f4..f6ebac5bf 100644 --- a/crucible/CHANGELOG.md +++ b/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 diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index 345425f10..eb076d174 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/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)) diff --git a/crucible/src/Lang/Crucible/Backend/Online.hs b/crucible/src/Lang/Crucible/Backend/Online.hs index 1142e42e8..8b46d96b8 100644 --- a/crucible/src/Lang/Crucible/Backend/Online.hs +++ b/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 diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index 38ea32b42..504765c8b 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/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. diff --git a/crucible/src/Lang/Crucible/Backend/Simple.hs b/crucible/src/Lang/Crucible/Backend/Simple.hs index 8c23ecb58..f550a98f1 100644 --- a/crucible/src/Lang/Crucible/Backend/Simple.hs +++ b/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)