From 3a334c9c313412e7fa5d4864d6c537f2003fc929 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 11 Mar 2024 14:50:21 -0400 Subject: [PATCH] Revert "Merge pull request #1169 from langston-barrett/lb/assumption-stack-refactor" This reverts commit 6157bbe44d9d0e0f429a4a0b60b96e17a4ca5b68, reversing changes made to 02cd934c4339a0cb113622b946e5b0d308b65df4. --- crucible/CHANGELOG.md | 5 - .../Lang/Crucible/Backend/AssumptionStack.hs | 126 +++++++----------- crucible/src/Lang/Crucible/Backend/Online.hs | 2 +- .../src/Lang/Crucible/Backend/ProofGoals.hs | 46 +++---- crucible/src/Lang/Crucible/Backend/Simple.hs | 2 +- 5 files changed, 67 insertions(+), 114 deletions(-) diff --git a/crucible/CHANGELOG.md b/crucible/CHANGELOG.md index 8a502f7ef..ac1e40487 100644 --- a/crucible/CHANGELOG.md +++ b/crucible/CHANGELOG.md @@ -1,8 +1,3 @@ -# next -- TBA - -* Rename `Lang.Crucible.Backend.popFrame` to `popFrameOrPanic`, - provide helpers such as `popFrame` to manage assumptions without `panic`ing. - # 0.7 -- 2024-02-05 * Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to diff --git a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs index eb076d174..345425f10 100644 --- a/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs +++ b/crucible/src/Lang/Crucible/Backend/AssumptionStack.hs @@ -18,7 +18,6 @@ solvers. -} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} @@ -33,15 +32,13 @@ module Lang.Crucible.Backend.AssumptionStack , FrameIdentifier , AssumptionFrame(..) , AssumptionFrames(..) - , AssumptionStack + , AssumptionStack(..) -- ** Manipulating assumption stacks , initAssumptionStack , saveAssumptionStack , restoreAssumptionStack , pushFrame - , PopFrameError(..) , popFrame - , popFrameOrPanic , popFrameAndGoals , popFramesUntil , resetStack @@ -57,13 +54,10 @@ 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) @@ -179,10 +173,12 @@ popFramesUntil ident stk = atomicModifyIORef' (proofObligations stk) (go 1) where go n gc = case gcPop gc of - Left frm - | ident == poppedFrameId frm -> (gc',n) + Left (ident', _assumes, mg, gc1) + | ident == ident' -> (gc',n) | otherwise -> go (n+1) gc' - where gc' = collectPoppedGoals frm + where gc' = case mg of + Nothing -> gc1 + Just g -> gcAddGoals g gc1 Right _ -> panic "AssumptionStack.popFrameUntil" [ "Frame not found in stack." @@ -191,84 +187,60 @@ 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. --- --- 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 :: Monoid asmp => FrameIdentifier -> AssumptionStack asmp ast -> IO asmp popFrame ident stk = - popFrameUnchecked stk <&> - \case - Left frm - | ident == poppedFrameId frm -> Right frm - | otherwise -> Left (WrongFrame ident (poppedFrameId frm)) - Right _ -> Left NoFrames + 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 --- | 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 = - popFrame ident stk <&> - \case - Left err -> panic "AssumptionStack.popFrameAndGoals" [show err] - Right frm -> (poppedAssumptions frm, poppedGoals frm) + 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 + -- | Run an action in the scope of a fresh assumption frame. -- The frame will be popped and returned on successful @@ -280,5 +252,5 @@ inFreshFrame stk action = (pushFrame stk) (\ident -> popFrame ident stk) (\ident -> do x <- action - frm <- popFrameOrPanic ident stk + frm <- popFrame ident stk return (frm, x)) diff --git a/crucible/src/Lang/Crucible/Backend/Online.hs b/crucible/src/Lang/Crucible/Backend/Online.hs index 8b46d96b8..1142e42e8 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 <- popFrameOrPanic ident (assumptionStack bak) + do frm <- popFrame 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 504765c8b..38ea32b42 100644 --- a/crucible/src/Lang/Crucible/Backend/ProofGoals.hs +++ b/crucible/src/Lang/Crucible/Backend/ProofGoals.hs @@ -28,8 +28,6 @@ module Lang.Crucible.Backend.ProofGoals , traverseGoalCollectorWithAssumptions -- ** Context management - , PoppedFrame(..) - , collectPoppedGoals , gcAddAssumes, gcProve , gcPush, gcPop, gcAddGoals, @@ -267,35 +265,23 @@ gcAddAssumes :: Monoid asmp => asmp -> GoalCollector asmp goal -> GoalCollector gcAddAssumes as' (CollectingAssumptions as gls) = CollectingAssumptions (as <> as') gls gcAddAssumes as' gls = CollectingAssumptions as' gls --- | 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 '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 '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 (PoppedFrame asmp goal) (Maybe (Goals asmp goal)) + Either (FrameIdentifier, asmp, Maybe (Goals asmp goal), GoalCollector asmp goal) + (Maybe (Goals asmp goal)) gcPop = go Nothing mempty where @@ -307,7 +293,7 @@ gcPop = go Nothing mempty Right (goalsConj (proveAll gs) hole) go hole as (CollectorFrame fid gc) = - Left (PoppedFrame fid as hole gc) + Left (fid, as, hole, gc) go hole as (CollectingAssumptions as' gc) = go (assuming as' <$> hole) (as' <> as) gc @@ -317,10 +303,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 poppedFrame -> gcFinish (collectPoppedGoals poppedFrame) - Right a -> a +gcFinish gc = case gcPop gc of + Left (_,_,Just g,gc1) -> gcFinish (gcAddGoals g gc1) + Left (_,_,Nothing,gc1) -> gcFinish gc1 + 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 f550a98f1..8c23ecb58 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.popFrameOrPanic ident (sbAssumptionStack bak) + AS.popFrame ident (sbAssumptionStack bak) popAssumptionFrameAndObligations bak ident = do AS.popFrameAndGoals ident (sbAssumptionStack bak)