From 5d760146dd52b14505069400a667a83622def886 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 14:07:54 -0500 Subject: [PATCH 1/9] crucible: Turn a tuple into `PoppedFrame` Pure refactoring, no functional change. --- .../Lang/Crucible/Backend/AssumptionStack.hs | 28 +++++++------ .../src/Lang/Crucible/Backend/ProofGoals.hs | 40 ++++++++++++------- 2 files changed, 40 insertions(+), 28 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index 345425f10..d00d9b5d9 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -173,10 +173,11 @@ 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 + where gc1 = poppedCollector frm + gc' = case poppedGoals frm of Nothing -> gc1 Just g -> gcAddGoals g gc1 Right _ -> @@ -194,17 +195,17 @@ popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asm 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) + Left frm + | ident == poppedFrameId frm -> + let gc' = case poppedGoals frm of + Nothing -> poppedCollector frm + Just g -> gcAddGoals g (poppedCollector frm) + in (gc', poppedAssumptions frm) | otherwise -> panic "AssumptionStack.popFrame" [ "Push/pop mismatch in assumption stack!" , "*** Current frame: " ++ showFrameId ident - , "*** Expected ident: " ++ showFrameId ident' + , "*** Expected ident: " ++ showFrameId (poppedFrameId frm) ] Right _ -> panic "AssumptionStack.popFrame" @@ -224,13 +225,14 @@ popFrameAndGoals :: popFrameAndGoals ident stk = atomicModifyIORef' (proofObligations stk) $ \gc -> case gcPop gc of - Left (ident', assumes, mg, gc1) - | ident == ident' -> (gc1, (assumes, mg)) + Left frm + | ident == poppedFrameId frm -> + (poppedCollector frm, (poppedAssumptions frm, poppedGoals frm)) | otherwise -> panic "AssumptionStack.popFrameAndGoals" [ "Push/pop mismatch in assumption stack!" , "*** Current frame: " ++ showFrameId ident - , "*** Expected ident: " ++ showFrameId ident' + , "*** Expected ident: " ++ showFrameId (poppedFrameId frm) ] Right _ -> panic "AssumptionStack.popFrameAndGoals" diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index 38ea32b42..9ec9daa51 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -28,6 +28,7 @@ module Lang.Crucible.Backend.ProofGoals , traverseGoalCollectorWithAssumptions -- ** Context management + , PoppedFrame(..) , gcAddAssumes, gcProve , gcPush, gcPop, gcAddGoals, @@ -266,22 +267,27 @@ gcAddAssumes as' (CollectingAssumptions as gls) = CollectingAssumptions (as <> a 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. - +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. -} +-- | 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 + } + 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 +299,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 +309,14 @@ 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 -> + let gc' = poppedCollector poppedFrame + in case poppedGoals poppedFrame of + Just g -> gcFinish (gcAddGoals g gc') + Nothing -> gcFinish gc' + Right a -> a -- | Reset the goal collector to the empty assumption state; but first -- collect all the pending proof goals and stash them. From e1ffc0724e7e593ceb345f3bb07b10a443644a5f Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 14:18:49 -0500 Subject: [PATCH 2/9] crucible: Helper for collecting `PoppedFrame` goals --- .../src/Lang/Crucible/Backend/AssumptionStack.hs | 10 ++-------- crucible/src/Lang/Crucible/Backend/ProofGoals.hs | 15 ++++++++++----- 2 files changed, 12 insertions(+), 13 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index d00d9b5d9..860540c38 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -176,10 +176,7 @@ popFramesUntil ident stk = atomicModifyIORef' (proofObligations stk) (go 1) Left frm | ident == poppedFrameId frm -> (gc',n) | otherwise -> go (n+1) gc' - where gc1 = poppedCollector frm - gc' = case poppedGoals frm of - Nothing -> gc1 - Just g -> gcAddGoals g gc1 + where gc' = collectPoppedGoals frm Right _ -> panic "AssumptionStack.popFrameUntil" [ "Frame not found in stack." @@ -197,10 +194,7 @@ popFrame ident stk = case gcPop gc of Left frm | ident == poppedFrameId frm -> - let gc' = case poppedGoals frm of - Nothing -> poppedCollector frm - Just g -> gcAddGoals g (poppedCollector frm) - in (gc', poppedAssumptions frm) + (collectPoppedGoals frm, poppedAssumptions frm) | otherwise -> panic "AssumptionStack.popFrame" [ "Push/pop mismatch in assumption stack!" diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index 9ec9daa51..ecc2b103b 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -29,6 +29,7 @@ module Lang.Crucible.Backend.ProofGoals -- ** Context management , PoppedFrame(..) + , collectPoppedGoals , gcAddAssumes, gcProve , gcPush, gcPop, gcAddGoals, @@ -284,6 +285,14 @@ data PoppedFrame asmp goal , 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) + gcPop :: Monoid asmp => GoalCollector asmp goal -> @@ -311,11 +320,7 @@ gcPop = go Nothing mempty gcFinish :: Monoid asmp => GoalCollector asmp goal -> Maybe (Goals asmp goal) gcFinish gc = case gcPop gc of - Left poppedFrame -> - let gc' = poppedCollector poppedFrame - in case poppedGoals poppedFrame of - Just g -> gcFinish (gcAddGoals g gc') - Nothing -> gcFinish gc' + Left poppedFrame -> gcFinish (collectPoppedGoals poppedFrame) Right a -> a -- | Reset the goal collector to the empty assumption state; but first From c1f38003465fd263fe2bb229adf123ee05197e80 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 14:30:27 -0500 Subject: [PATCH 3/9] crucible: Helper for popping frames from `AssumptionStack` --- .../Lang/Crucible/Backend/AssumptionStack.hs | 75 +++++++++++-------- 1 file changed, 43 insertions(+), 32 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index 860540c38..734f0b6c1 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 #-} @@ -54,6 +55,7 @@ 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 @@ -185,28 +187,37 @@ 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) + -- | 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 popFrame ident stk = - atomicModifyIORef' (proofObligations stk) $ \gc -> - case gcPop gc of - Left frm - | ident == poppedFrameId frm -> - (collectPoppedGoals frm, poppedAssumptions frm) - | otherwise -> - panic "AssumptionStack.popFrame" - [ "Push/pop mismatch in assumption stack!" - , "*** Current frame: " ++ showFrameId ident - , "*** Expected ident: " ++ showFrameId (poppedFrameId frm) - ] - Right _ -> - panic "AssumptionStack.popFrame" - [ "Pop with no push in goal collector." - , "*** Current frame: " ++ showFrameId ident - ] - + popFrameUnchecked stk <&> + \case + Left frm + | ident == poppedFrameId frm -> poppedAssumptions frm + | otherwise -> + panic "AssumptionStack.popFrame" + [ "Push/pop mismatch in assumption stack!" + , "*** Current frame: " ++ showFrameId ident + , "*** Expected ident: " ++ showFrameId (poppedFrameId frm) + ] + Right _ -> + panic "AssumptionStack.popFrame" + [ "Pop with no push in goal collector." + , "*** Current frame: " ++ showFrameId ident + ] where showFrameId (FrameIdentifier x) = show x @@ -217,22 +228,22 @@ popFrameAndGoals :: AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast)) popFrameAndGoals ident stk = - atomicModifyIORef' (proofObligations stk) $ \gc -> - case gcPop gc of - Left frm - | ident == poppedFrameId frm -> - (poppedCollector frm, (poppedAssumptions frm, poppedGoals frm)) - | otherwise -> - panic "AssumptionStack.popFrameAndGoals" - [ "Push/pop mismatch in assumption stack!" - , "*** Current frame: " ++ showFrameId ident - , "*** Expected ident: " ++ showFrameId (poppedFrameId frm) - ] - Right _ -> - panic "AssumptionStack.popFrameAndGoals" - [ "Pop with no push in goal collector." - , "*** Current frame: " ++ showFrameId ident + popFrameUnchecked stk <&> + \case + Left frm + | ident == poppedFrameId frm -> + (poppedAssumptions frm, poppedGoals frm) + | otherwise -> + panic "AssumptionStack.popFrameAndGoals" + [ "Push/pop mismatch in assumption stack!" + , "*** Current frame: " ++ showFrameId ident + , "*** Expected ident: " ++ showFrameId (poppedFrameId frm) ] + Right _ -> + panic "AssumptionStack.popFrameAndGoals" + [ "Pop with no push in goal collector." + , "*** Current frame: " ++ showFrameId ident + ] where showFrameId (FrameIdentifier x) = show x From 24b63490e4cdb9f3e433d9a94a587f764e6112d6 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 14:43:18 -0500 Subject: [PATCH 4/9] crucible: Another helper for popping frames from `AssumptionStack` --- .../Lang/Crucible/Backend/AssumptionStack.hs | 79 +++++++++++-------- 1 file changed, 44 insertions(+), 35 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index 734f0b6c1..8ef10a6ae 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -60,6 +60,8 @@ 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) @@ -198,29 +200,52 @@ popFrameUnchecked stk = 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 -popFrame ident stk = +popFrameChecked :: + Monoid asmp => + FrameIdentifier -> + AssumptionStack asmp ast -> + IO (Either PopFrameError (PoppedFrame asmp ast)) +popFrameChecked ident stk = popFrameUnchecked stk <&> \case Left frm - | ident == poppedFrameId frm -> poppedAssumptions frm - | otherwise -> - panic "AssumptionStack.popFrame" - [ "Push/pop mismatch in assumption stack!" - , "*** Current frame: " ++ showFrameId ident - , "*** Expected ident: " ++ showFrameId (poppedFrameId frm) - ] - Right _ -> - panic "AssumptionStack.popFrame" - [ "Pop with no push in goal collector." - , "*** Current frame: " ++ showFrameId ident - ] - where - showFrameId (FrameIdentifier x) = show x + | 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. +popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp +popFrame ident stk = + popFrameChecked ident stk <&> + \case + Left err -> panic "AssumptionStack.popFrame" [show err] + Right frm -> poppedAssumptions frm popFrameAndGoals :: Monoid asmp => @@ -228,26 +253,10 @@ popFrameAndGoals :: AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast)) popFrameAndGoals ident stk = - popFrameUnchecked stk <&> + popFrameChecked ident stk <&> \case - Left frm - | ident == poppedFrameId frm -> - (poppedAssumptions frm, poppedGoals frm) - | otherwise -> - panic "AssumptionStack.popFrameAndGoals" - [ "Push/pop mismatch in assumption stack!" - , "*** Current frame: " ++ showFrameId ident - , "*** Expected ident: " ++ showFrameId (poppedFrameId frm) - ] - Right _ -> - panic "AssumptionStack.popFrameAndGoals" - [ "Pop with no push in goal collector." - , "*** Current frame: " ++ showFrameId ident - ] - - where - showFrameId (FrameIdentifier x) = show x - + 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 From e27eba6295e55ab07ed4c934b869b989c9ee8606 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 14:45:20 -0500 Subject: [PATCH 5/9] crucible: Document error conditions in `AssumptionStack` --- crucible/src/Lang/Crucible/Backend/AssumptionStack.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index 8ef10a6ae..b045444cb 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -224,6 +224,9 @@ instance Show PopFrameError where -- | 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. +-- +-- Returns 'Left' if there are no frames on the stack, or if the top frame +-- doesn\'t have the provided 'FrameIdentifier'. popFrameChecked :: Monoid asmp => FrameIdentifier -> @@ -240,6 +243,9 @@ popFrameChecked ident stk = -- | 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'. popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp popFrame ident stk = popFrameChecked ident stk <&> @@ -247,6 +253,10 @@ popFrame ident stk = 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 -> From ea7e24d51ea90da20e62a688f0c45431cf1fa22f Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 15:06:02 -0500 Subject: [PATCH 6/9] crucible: Rename `popFrame{,OrPanic}`, `popFrame{Checked,}` --- .../src/Lang/Crucible/Backend/AssumptionStack.hs | 16 +++++++++------- crucible/src/Lang/Crucible/Backend/Online.hs | 2 +- crucible/src/Lang/Crucible/Backend/Simple.hs | 2 +- 3 files changed, 11 insertions(+), 9 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index b045444cb..c26ee4f7e 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -39,7 +39,9 @@ module Lang.Crucible.Backend.AssumptionStack , saveAssumptionStack , restoreAssumptionStack , pushFrame + , PopFrameError(..) , popFrame + , popFrameOrPanic , popFrameAndGoals , popFramesUntil , resetStack @@ -227,12 +229,12 @@ instance Show PopFrameError where -- -- Returns 'Left' if there are no frames on the stack, or if the top frame -- doesn\'t have the provided 'FrameIdentifier'. -popFrameChecked :: +popFrame :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO (Either PopFrameError (PoppedFrame asmp ast)) -popFrameChecked ident stk = +popFrame ident stk = popFrameUnchecked stk <&> \case Left frm @@ -246,9 +248,9 @@ popFrameChecked ident stk = -- -- Panics 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 asmp -popFrame ident stk = - popFrameChecked ident stk <&> +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 @@ -263,7 +265,7 @@ popFrameAndGoals :: AssumptionStack asmp ast -> IO (asmp, Maybe (Goals asmp ast)) popFrameAndGoals ident stk = - popFrameChecked ident stk <&> + popFrame ident stk <&> \case Left err -> panic "AssumptionStack.popFrameAndGoals" [show err] Right frm -> (poppedAssumptions frm, poppedGoals frm) @@ -278,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/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) From b62ca9e4950379a3e1cb1c85284bb917e9c9c45a Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 15:18:28 -0500 Subject: [PATCH 7/9] crucible: Don't export the constructor of `AssumptionStack` Appears not to be needed: https://github.com/search?q=owner%3AGaloisInc+%2FAssumptionStack%2F+language%3AHaskell&type=code&l=Haskell --- crucible/src/Lang/Crucible/Backend/AssumptionStack.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index c26ee4f7e..eb076d174 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -33,7 +33,7 @@ module Lang.Crucible.Backend.AssumptionStack , FrameIdentifier , AssumptionFrame(..) , AssumptionFrames(..) - , AssumptionStack(..) + , AssumptionStack -- ** Manipulating assumption stacks , initAssumptionStack , saveAssumptionStack From 2bf03d1411270bdbeb1f01cab7ed5ff45c62514b Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 15:21:27 -0500 Subject: [PATCH 8/9] crucible: Add `AssumptionStack` refactors to CHANGELOG --- crucible/CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) 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 From a633fd9985801184ad8f510955d668a7ee5043ab Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Wed, 24 Jan 2024 16:01:12 -0500 Subject: [PATCH 9/9] crucible: Fix position of Haddock comment, remove comma --- crucible/src/Lang/Crucible/Backend/ProofGoals.hs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs index ecc2b103b..504765c8b 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -267,15 +267,10 @@ 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. -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. -} - -- | A frame, popped by 'gcPop' data PoppedFrame asmp goal = PoppedFrame - { -- | The frame identifier of the popped frame, + { -- | The frame identifier of the popped frame poppedFrameId :: !FrameIdentifier -- | The assumptions that were forgotten by the pop , poppedAssumptions :: asmp @@ -293,6 +288,10 @@ collectPoppedGoals frm = 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 ->