diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,18 @@ +2024-09-09 + * Version bump (4.0). (#69) + * Support verifying programs that use array updates. (#63) + * Support verifying programs that use struct updates. (#57) + +2024-08-03 + * Support building with `crucible-llvm-0.7` and `crux-llvm-0.9`. (#64) + * Support GHC 9.4 through 9.8. (#65) + +2024-07-30 + * When using `Noisy` verbosity, always log proof goals related to the + core correspondence proof, even if the goals are trivial. (#51) + * When using `Noisy` verbosity, log more information about which proof + goals arise before or after calling the `step()` function. (#52) + 2024-07-11 * Version bump (3.20). (#58) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -29,7 +29,7 @@ * Ensure that you have the `cabal` and `ghc` executables in your `PATH`. If you don't already have them, we recommend using `ghcup` to install them: https://www.haskell.org/ghcup/. We recommend `Cabal` 3.10 or newer, and one of - GHC 8.10, 9.2, or 9.4. + GHC 9.4, 9.6, or 9.8. * Ensure that you have the `clang` and `llvm-link` utilities from LLVM in your `PATH`. Currently, LLVM versions up to 16 are supported. LLVM binaries are diff --git a/copilot-verifier.cabal b/copilot-verifier.cabal --- a/copilot-verifier.cabal +++ b/copilot-verifier.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: copilot-verifier -Version: 3.20 +Version: 4.0 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024 @@ -41,20 +41,20 @@ NondecreasingIndentation build-depends: aeson >= 1.5 && < 2.3, - base >= 4.8 && < 4.18, + base >= 4.8 && < 4.20, bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0, - copilot-c99 >= 3.20 && < 3.21, - copilot-core >= 3.20 && < 3.21, - copilot-theorem >= 3.20 && < 3.21, - crucible >= 0.7 && < 0.8, - crucible-llvm >= 0.6 && < 0.7, - crux >= 0.7 && < 0.8, - crux-llvm >= 0.8 && < 0.9, + copilot-c99 >= 4.0 && < 4.1, + copilot-core >= 4.0 && < 4.1, + copilot-theorem >= 4.0 && < 4.1, + crucible >= 0.7.1 && < 0.8, + crucible-llvm >= 0.7 && < 0.8, + crux >= 0.7.1 && < 0.8, + crux-llvm >= 0.9 && < 0.10, filepath, lens, - llvm-pretty, + llvm-pretty >= 0.12.1.0 && < 0.13, mtl, panic >= 0.3, parameterized-utils >= 2.1.4 && < 2.2, @@ -62,7 +62,7 @@ text, transformers, vector, - what4 >= 0.4 + what4 >= 1.6.1 && < 1.7 library import: bldflags @@ -78,9 +78,9 @@ hs-source-dirs: examples build-depends: case-insensitive, - copilot >= 3.20 && < 3.21, - copilot-language >= 3.20 && < 3.21, - copilot-prettyprinter >= 3.20 && < 3.21, + copilot >= 4.0 && < 4.1, + copilot-language >= 4.0 && < 4.1, + copilot-prettyprinter >= 4.0 && < 4.1, copilot-verifier exposed-modules: Copilot.Verifier.Examples @@ -116,6 +116,8 @@ Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap Copilot.Verifier.Examples.ShouldPass.Structs + Copilot.Verifier.Examples.ShouldPass.UpdateArray + Copilot.Verifier.Examples.ShouldPass.UpdateStruct Copilot.Verifier.Examples.ShouldPass.Voting Copilot.Verifier.Examples.ShouldPass.WCV diff --git a/examples/Copilot/Verifier/Examples.hs b/examples/Copilot/Verifier/Examples.hs --- a/examples/Copilot/Verifier/Examples.hs +++ b/examples/Copilot/Verifier/Examples.hs @@ -41,6 +41,8 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Partial.ShiftRTooLarge as Pass.ShiftRTooLarge import qualified Copilot.Verifier.Examples.ShouldPass.Partial.SubSignedWrap as Pass.SubSignedWrap import qualified Copilot.Verifier.Examples.ShouldPass.Structs as Structs +import qualified Copilot.Verifier.Examples.ShouldPass.UpdateArray as UpdateArray +import qualified Copilot.Verifier.Examples.ShouldPass.UpdateStruct as UpdateStruct import qualified Copilot.Verifier.Examples.ShouldPass.Voting as Voting import qualified Copilot.Verifier.Examples.ShouldPass.WCV as WCV @@ -72,6 +74,8 @@ , example "Heater" (Heater.verifySpec verb) , example "IntOps" (IntOps.verifySpec verb) , example "Structs" (Structs.verifySpec verb) + , example "UpdateArray" (UpdateArray.verifySpec verb) + , example "UpdateStruct" (UpdateStruct.verifySpec verb) , example "Voting" (Voting.verifySpec verb) , example "WCV" (WCV.verifySpec verb) diff --git a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs --- a/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs +++ b/examples/Copilot/Verifier/Examples/ShouldFail/Partial/IndexOutOfBounds.hs @@ -19,7 +19,7 @@ stream2 = extern "stream2" Nothing _ <- prop "withinBounds" (forAll (stream2 < constW32 2)) - trigger "streamIndex" ((stream1 .!! stream2) == 1) [arg stream1, arg stream2] + trigger "streamIndex" ((stream1 ! stream2) == 1) [arg stream1, arg stream2] verifySpec :: Verbosity -> IO () verifySpec verb = do diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs --- a/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs +++ b/examples/Copilot/Verifier/Examples/ShouldPass/Array.hs @@ -31,7 +31,7 @@ -- It passes the current value of arr as an argument. -- The prototype of 'func' would be: -- void func (int8_t arg[3]); - trigger "func" (arr .!! 0) [arg arr] + trigger "func" (arr ! 0) [arg arr] -- Compile the spec verifySpec :: Verbosity -> IO () diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs --- a/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs +++ b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayGen.hs @@ -8,7 +8,7 @@ import qualified Prelude hiding ((++), (>)) spec :: Spec -spec = trigger "f" (stream .!! 0 > 0) [arg stream] +spec = trigger "f" (stream ! 0 > 0) [arg stream] where stream :: Stream (Array 2 Int16) stream = [array [3,4]] ++ rest diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs --- a/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs +++ b/examples/Copilot/Verifier/Examples/ShouldPass/ArrayOfStructs.hs @@ -17,7 +17,7 @@ typeOf = Struct (S (Field 0)) spec :: Spec -spec = trigger "f" ((stream .!! 0)#field == 27) [arg stream] +spec = trigger "f" ((stream ! 0)#field == 27) [arg stream] where stream :: Stream (Array 2 S) stream = [array [S (Field 27), S (Field 42)]] ++ stream diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs b/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs --- a/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs +++ b/examples/Copilot/Verifier/Examples/ShouldPass/Structs.hs @@ -61,15 +61,15 @@ -- Check equality, indexing into nested structs and arrays. Note that this is -- trivial by equality. void $ prop "Example 1" $ forAll $ - (((battery#volts) .!! 0)#numVolts) == (((battery#volts) .!! 0)#numVolts) + (((battery#volts) ! 0)#numVolts) == (((battery#volts) ! 0)#numVolts) -- Same as previous example, but get a different array index (so should be -- false). void $ prop "Example 2" $ forAll $ - (((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4) + (((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4) -- Same as previous example, but in trigger form - trigger "otherTrig" ((((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)) + trigger "otherTrig" ((((battery#other) ! 2) ! 3) == (((battery#other) ! 2) ! 4)) [arg battery] verifySpec :: Verbosity -> IO () diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/UpdateArray.hs b/examples/Copilot/Verifier/Examples/ShouldPass/UpdateArray.hs new file mode 100644 --- /dev/null +++ b/examples/Copilot/Verifier/Examples/ShouldPass/UpdateArray.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE DataKinds #-} + +-- | An example showing of using @copilot-verifier@ to verify a specification +-- involving arrays where individual elements are updated. +module Copilot.Verifier.Examples.ShouldPass.UpdateArray where + +import Language.Copilot +import Copilot.Compile.C99 +import Copilot.Verifier ( Verbosity, VerifierOptions(..) + , defaultVerifierOptions, verifyWithOptions ) + +spec :: Spec +spec = do + let pair :: Stream (Array 2 Word32) + pair = extern "pair" Nothing + + -- Check equality, indexing into array and modifying the value. Note that + -- this is trivial by equality. + trigger "trig_1" + (((pair !! 0 =$ (+1)) ! 0) == ((pair ! 0) + 1)) + [arg pair] + + -- Same as previous example, but get a different array index (so should be + -- false). + trigger "trig_2" + (((pair !! 0 =$ (+1)) ! 1) == ((pair ! 0) + 1)) + [arg pair] + +verifySpec :: Verbosity -> IO () +verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb} + mkDefaultCSettings [] "updateArray" diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs b/examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs new file mode 100644 --- /dev/null +++ b/examples/Copilot/Verifier/Examples/ShouldPass/UpdateStruct.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE RebindableSyntax #-} +{-# LANGUAGE DataKinds #-} + +-- | An example showing of using @copilot-verifier@ to verify a specification +-- involving structs where individual fields are updated. +module Copilot.Verifier.Examples.ShouldPass.UpdateStruct where + +import Language.Copilot +import Copilot.Compile.C99 +import Copilot.Verifier ( Verbosity, VerifierOptions(..) + , defaultVerifierOptions, verifyWithOptions ) + +-- | Definition for `Volts`. +data Volts = Volts + { numVolts :: Field "numVolts" Word32 + , flag :: Field "flag" Bool + } + +-- | `Struct` instance for `Volts`. +instance Struct Volts where + typeName _ = "volts" + toValues vlts = [ Value Word32 (numVolts vlts) + , Value Bool (flag vlts) + ] + +-- | `Volts` instance for `Typed`. +instance Typed Volts where + typeOf = Struct (Volts (Field 0) (Field False)) + +data Battery = Battery + { temp :: Field "temp" Word32 + , volts :: Field "volts" (Array 10 Volts) + , other :: Field "other" (Array 10 (Array 5 Word32)) + } + +-- | `Battery` instance for `Struct`. +instance Struct Battery where + typeName _ = "battery" + toValues battery = [ Value typeOf (temp battery) + , Value typeOf (volts battery) + , Value typeOf (other battery) + ] + +-- | `Battery` instance for `Typed`. Note that `undefined` is used as an +-- argument to `Field`. This argument is never used, so `undefined` will never +-- throw an error. +instance Typed Battery where + typeOf = Struct (Battery (Field 0) (Field undefined) (Field undefined)) + +spec :: Spec +spec = do + let battery :: Stream Battery + battery = extern "battery" Nothing + + -- Update a struct field, then check it for equality. + trigger "updateTrig" + ((battery ## temp =$ (+1))#temp == (battery#temp + 1)) + [arg battery] + +verifySpec :: Verbosity -> IO () +verifySpec verb = reify spec >>= verifyWithOptions defaultVerifierOptions{verbosity = verb} + mkDefaultCSettings [] "updateStruct" diff --git a/src/Copilot/Verifier.hs b/src/Copilot/Verifier.hs --- a/src/Copilot/Verifier.hs +++ b/src/Copilot/Verifier.hs @@ -66,7 +66,8 @@ , pushAssumptionFrame, popUntilAssumptionFrame , getProofObligations, clearProofObligations , LabeledPred(..), abortExecBecause, AbortExecReason(..), addAssumption - , addDurableProofObligation, assert, CrucibleAssumption(..), ppAbortExecReason + , addDurableAssertion, addDurableProofObligation + , CrucibleAssumption(..), ppAbortExecReason , IsSymBackend(..), HasSymInterface(..) , labeledPred, labeledPredMsg -- , ProofObligations, proofGoal, goalsToList, labeledPredMsg @@ -78,7 +79,7 @@ import Lang.Crucible.Simulator ( SimContext(..), ctxSymInterface, ExecResult(..), ExecState(..) , defaultAbortHandler, runOverrideSim, partialValue, gpValue - , GlobalVar, executeCrucible, OverrideSim, regValue + , GlobalVar, executeCrucible, OverrideSim, ovrWithBackend, regValue , readGlobal, modifyGlobal, callCFG, emptyRegMap, RegEntry(..) , AbortedResult(..) ) @@ -455,7 +456,8 @@ do Log.sayCopilot $ Log.ComputingConditions Log.InitialState frm <- pushAssumptionFrame bak - assertStateRelation bak clRefs mem initialState + assertStateRelation bak clRefs mem + Log.InitialStateRelation initialState popUntilAssumptionFrame bak frm @@ -500,7 +502,8 @@ mem' <- setupPrestate bak mem prfbundle -- sanity check, verify that we set up the memory in the expected relation - assertStateRelation bak clRefs mem' (CW4.preStreamState prfbundle) + assertStateRelation bak clRefs mem' + Log.PreStepStateRelation (CW4.preStreamState prfbundle) -- set up trigger guard global variables let halloc = simHandleAllocator simctx @@ -515,7 +518,8 @@ mem'' <- executeStep opts csettings clRefs simctx memVar mem' llvmMod modTrans triggerGlobals overrides (CW4.assumptions prfbundle) (CW4.sideConds prfbundle) -- assert the poststate is in the relation - assertStateRelation bak clRefs mem'' (CW4.postStreamState prfbundle) + assertStateRelation bak clRefs mem'' + Log.PostStepStateRelation (CW4.postStreamState prfbundle) popUntilAssumptionFrame bak frm @@ -554,14 +558,15 @@ CopilotLogRefs sym -> (Name, GlobalVar NatType, Pred sym) -> (Name, BoolExpr t, [(Some Type, CW4.XExpr sym)]) -> - OverrideTemplate (Crux sym) sym arch (RegEntry sym Mem) EmptyCtx Mem + OverrideTemplate (Crux sym) sym LLVM arch triggerOverride clRefs (_,triggerGlobal,_) (nm, _guard, args) = let args' = map toTypeRepr args in case Ctx.fromList args' of Some argCtx -> basic_llvm_override $ LLVMOverride decl argCtx UnitRepr $ - \memOps bak calledArgs -> + \memOps calledArgs -> + ovrWithBackend $ \bak -> do let sym = backendGetSym bak modifyGlobal triggerGlobal $ \count -> do -- See Note [Global variables for trigger functions] @@ -644,7 +649,7 @@ L.Module -> ModuleTranslation arch -> [(Name, GlobalVar NatType, Pred sym)] -> - [OverrideTemplate (Crux sym) sym arch (RegEntry sym Mem) EmptyCtx Mem] -> + [OverrideTemplate (Crux sym) sym LLVM arch] -> [Pred sym] {- User-provided property assumptions -} -> [Pred sym] {- Side conditions related to partial operations -} -> IO (MemImpl sym) @@ -699,7 +704,7 @@ runStep :: OverrideSim (Crux sym) sym LLVM (RegEntry sym Mem) EmptyCtx Mem (MemImpl sym) runStep = do -- set up built-in functions and trigger overrides - register_llvm_overrides llvmmod [] triggerOverrides llvm_ctx + _ <- register_llvm_overrides llvmmod [] triggerOverrides llvm_ctx -- set up functions defined in the module registerLazyModule sayTranslationWarning modTrans @@ -838,13 +843,13 @@ HasLLVMAnn sym => (?memOpts :: MemOptions) => (?lc :: TypeContext) => - bak -> CopilotLogRefs sym -> MemImpl sym -> + Log.StateRelationStep -> CW4.BisimulationProofState sym -> IO () -assertStateRelation bak clRefs mem prfst = +assertStateRelation bak clRefs mem stateRelStep prfst = -- For each stream in the proof state, assert that the -- generated ring buffer global contains the corresponding -- values. @@ -882,7 +887,7 @@ modifyIORef' (verifierAssertionMapRef clRefs) $ Map.insert bannIdxVal $ Log.RingBufferIndexLoadAssertion - $ Log.RingBufferIndexLoad sym locIdxVal (Text.pack idxName) pIdxVal + $ Log.RingBufferIndexLoad sym stateRelStep locIdxVal (Text.pack idxName) pIdxVal buflen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth buflen) typeLen' <- bvLit sym ?ptrWidth (BV.mkBV ?ptrWidth (toInteger typeLen)) @@ -903,7 +908,7 @@ $ Map.insert bannv' $ Log.RingBufferLoadAssertion $ Log.SomeSome - $ Log.RingBufferLoad sym locv' bufNameT i buflen ctp typeRepr pv' + $ Log.RingBufferLoad sym stateRelStep locv' bufNameT i buflen ctp typeRepr pv' eq <- computeEqualVals bak clRefs mem ctp v typeRepr v' (ann, eq') <- annotateTerm sym eq let shortmsg = "State equality condition: " ++ show nm ++ " index value " ++ show i @@ -914,7 +919,7 @@ $ Map.insert (BoolAnn ann) $ Log.StreamValueEqualityAssertion $ Log.SomeSome - $ Log.StreamValueEquality sym loc bufNameT i buflen ctp v typeRepr v' + $ Log.StreamValueEquality sym stateRelStep loc bufNameT i buflen ctp v typeRepr v' addDurableProofObligation bak (LabeledPred eq' (SimError loc rsn)) return () @@ -1236,8 +1241,13 @@ `if guard_cond then 1 else 0`. -} --- | Like @crucible-llvm@'s @doLoad@, but also returning the 'BoolAnn' and --- 'Pred' asserting the validity of the load. +-- | Like @crucible-llvm@'s @doLoad@, but with the following differences: +-- +-- * This function returns the 'BoolAnn' and 'Pred' asserting the validity of +-- the load, which the verifier needs for logging purposes. +-- +-- * This always generates a durable proof goal so that Crucible will always +-- record it, even if it is trivial. doLoadWithAnn :: ( IsSymBackend sym bak, HasPtrWidth wptr, HasLLVMAnn sym , ?memOpts :: MemOptions ) => @@ -1256,24 +1266,29 @@ where sym = backendGetSym bak --- | Like @crucible-llvm@'s @assertSafe@, but also returning the 'BoolAnn' and --- 'Pred' corresponding the assertion. +-- | Like @crucible-llvm@'s @assertSafe@, but with the following differences: +-- +-- * This function returns the 'BoolAnn' and 'Pred' corresponding to the +-- assertion, which the verifier needs for logging purposes. +-- +-- * This generates a durable assertion so that Crucible will always record it, +-- even if it is trivial. assertSafeWithAnn :: IsSymBackend sym bak => bak -> PartLLVMVal sym -> IO (BoolAnn sym, Pred sym, LLVMVal sym) -assertSafeWithAnn bak partVal = +assertSafeWithAnn bak partVal = do + loc <- getCurrentProgramLoc sym + let err = SimError loc rsn case partVal of NoErr p v -> do (ann, p') <- annotateTerm sym p - assert bak p' rsn + addDurableAssertion bak (LabeledPred p' err) return (BoolAnn ann, p', v) Err p -> do - loc <- getCurrentProgramLoc sym - let err = SimError loc rsn (_ann, p') <- annotateTerm sym p - addProofObligation bak (LabeledPred p' err) + addDurableProofObligation bak (LabeledPred p' err) abortExecBecause (AssertionFailure err) where rsn = AssertFailureSimError "Error during memory load" "" diff --git a/src/Copilot/Verifier/Log.hs b/src/Copilot/Verifier/Log.hs --- a/src/Copilot/Verifier/Log.hs +++ b/src/Copilot/Verifier/Log.hs @@ -13,6 +13,7 @@ ( SupportsCopilotLogMessage , CopilotLogMessage(..) , VerificationStep(..) + , StateRelationStep(..) , VerifierAssertion(..) , SomeSome(..) , StreamValueEquality(..) @@ -187,6 +188,34 @@ deriving stock Generic deriving anyclass ToJSON +-- | The provenance of an assertion. +data AssertionProvenance + = VerifierProvenance + -- ^ Assertions that the verifier directly makes to check the correspondence + -- between the Copilot specification and the generated C code. Because these + -- assertions are core to the proof that the verifier is computing, these + -- assertions' proof goals are always logged, even if they are trivial. + | StepExecutionProvenance + -- ^ Assertions that arise during symbolic execution of the @step()@ + -- function as part of proving the memory safety of the generated C code. + -- These assertions' proof goals are only logged if they are non-trivial, + -- as there would be an excessive number of these proof goals otherwise. + +-- | At what step of the proof are we checking the state relation? We record +-- this so that we can better distinguish between transition step–related +-- proof goals that arise before or after calling the @step()@ function. +data StateRelationStep + = InitialStateRelation + -- ^ Check the state relation for the initial state. + | PreStepStateRelation + -- ^ During the transition step of the proof, check the state relation + -- before calling the @step()@ function. + | PostStepStateRelation + -- ^ During the transition step of the proof, check the state relation + -- after calling the @step()@ function. + deriving stock Generic + deriving anyclass ToJSON + -- | Types of assertions that the verifier can make, which will count towards -- the total number of proof goals. data VerifierAssertion sym @@ -211,6 +240,8 @@ data StreamValueEquality sym copilotType crucibleType where StreamValueEquality :: sym + -> StateRelationStep + -- ^ When the values are checked for equality -> WPL.ProgramLoc -- ^ The locations of the values -> Text @@ -271,8 +302,10 @@ data RingBufferLoad sym copilotType crucibleType where RingBufferLoad :: sym + -> StateRelationStep + -- ^ When the ring buffer is loaded from -> WPL.ProgramLoc - -- ^ The location of the trigger + -- ^ The location of the buffer -> Text -- ^ The name of the buffer -> Integer @@ -293,8 +326,10 @@ data RingBufferIndexLoad sym where RingBufferIndexLoad :: sym + -> StateRelationStep + -- ^ When the index's global variable is loaded from -> WPL.ProgramLoc - -- ^ The location of the trigger + -- ^ The location of the global index -> Text -- ^ The name of the global index -> WI.Pred sym @@ -489,15 +524,15 @@ , "```" ] copilotLogMessageToSayWhat - (StreamValueEqualityProofGoal step goalIdx numTotalGoals + (StreamValueEqualityProofGoal verifStep goalIdx numTotalGoals (StreamValueEquality - sym loc + sym stateRelStep loc bufName offset len copilotTy copilotVal crucibleTy crucibleVal)) = copilotNoisily $ - displayProofGoal - step goalIdx numTotalGoals + displayStateRelationProofGoal + verifStep stateRelStep VerifierProvenance goalIdx numTotalGoals "asserting the equality between two stream values" [ renderStrict $ ppProgramLoc loc , "* Ring buffer name: " <> bufName @@ -514,7 +549,7 @@ (TriggersInvokedCorrespondingly loc name expected actual)) = copilotNoisily $ displayProofGoal - step goalIdx numTotalGoals + step VerifierProvenance goalIdx numTotalGoals "asserting triggers fired in corresponding ways" [ renderStrict $ ppProgramLoc loc , "* Trigger name: " <> T.pack name @@ -532,7 +567,7 @@ crucibleTy crucibleVal)) = copilotNoisily $ displayProofGoal - step goalIdx numTotalGoals + step VerifierProvenance goalIdx numTotalGoals "asserting the equality between two trigger arguments" [ renderStrict $ ppProgramLoc loc , "* Trigger name: " <> T.pack triggerName @@ -544,12 +579,12 @@ , renderStrict $ PP.indent 4 $ ppCrucibleValue sym crucibleTy crucibleVal ] copilotLogMessageToSayWhat - (RingBufferLoadProofGoal step goalIdx numTotalGoals + (RingBufferLoadProofGoal verifStep goalIdx numTotalGoals (RingBufferLoad - _sym loc bufName offset len copilotTy _crucibleTy p)) = + _sym stateRelStep loc bufName offset len copilotTy _crucibleTy p)) = copilotNoisily $ - displayProofGoal - step goalIdx numTotalGoals + displayStateRelationProofGoal + verifStep stateRelStep VerifierProvenance goalIdx numTotalGoals "asserting the validity of a memory load from a stream's ring buffer in C" [ renderStrict $ ppProgramLoc loc , "* Ring buffer name: " <> bufName @@ -560,11 +595,11 @@ , renderStrict $ PP.indent 4 $ WI.printSymExpr p ] copilotLogMessageToSayWhat - (RingBufferIndexLoadProofGoal step goalIdx numTotalGoals - (RingBufferIndexLoad _sym loc idxName p)) = + (RingBufferIndexLoadProofGoal verifStep goalIdx numTotalGoals + (RingBufferIndexLoad _sym stateRelStep loc idxName p)) = copilotNoisily $ - displayProofGoal - step goalIdx numTotalGoals + displayStateRelationProofGoal + verifStep stateRelStep VerifierProvenance goalIdx numTotalGoals "asserting the validity of a memory load from the index to a stream's ring buffer in C" [ renderStrict $ ppProgramLoc loc , "* Ring buffer index name: " <> idxName @@ -577,7 +612,7 @@ _sym loc copilotTy _crucibleTy p)) = copilotNoisily $ displayProofGoal - step goalIdx numTotalGoals + step VerifierProvenance goalIdx numTotalGoals "asserting the validity of a memory load from a pointer argument to a trigger" [ renderStrict $ ppProgramLoc loc , "* Copilot type: " <> T.pack (showsCopilotType 0 copilotTy "") @@ -589,7 +624,7 @@ (AccessorFunctionLoad _sym loc accessorName p)) = copilotNoisily $ displayProofGoal - step goalIdx numTotalGoals + step StepExecutionProvenance goalIdx numTotalGoals "asserting the validity of a memory load from a stream accessor function" [ renderStrict $ ppProgramLoc loc , "* Accessor function name: " <> WF.functionName accessorName @@ -601,7 +636,7 @@ (GuardFunctionLoad _sym loc accessorName p)) = copilotNoisily $ displayProofGoal - step goalIdx numTotalGoals + step StepExecutionProvenance goalIdx numTotalGoals "asserting the validity of a memory load from a trigger guard function" [ renderStrict $ ppProgramLoc loc , "* Guard function name: " <> WF.functionName accessorName @@ -613,7 +648,7 @@ (UnknownFunctionLoad _sym loc accessorName p)) = copilotNoisily $ displayProofGoal - step goalIdx numTotalGoals + step StepExecutionProvenance goalIdx numTotalGoals "asserting the validity of a memory load from an unknown function" [ renderStrict $ ppProgramLoc loc , "* Function name: " <> WF.functionName accessorName @@ -636,7 +671,7 @@ LCLE.BBUndefinedBehavior ub -> copilotNoisily $ displayProofGoal - step goalIdx numTotalGoals + step StepExecutionProvenance goalIdx numTotalGoals "asserting that LLVM undefined behavior does not occur" $ ppLoc : ppCallStackLines ++ [ "* Undefined behavior description:" @@ -645,7 +680,7 @@ LCLE.BBMemoryError me -> copilotNoisily $ displayProofGoal - step goalIdx numTotalGoals + step StepExecutionProvenance goalIdx numTotalGoals "asserting that LLVM memory unsafety does not occur" $ ppLoc : ppCallStackLines ++ [ "* Memory unsafety description:" @@ -659,15 +694,17 @@ -- | Display information about an emitted proof goal. displayProofGoal :: VerificationStep + -> AssertionProvenance -> Integer -> Integer -> Text -> [Text] -> Text -displayProofGoal step goalIdx numTotalGoals why ls = T.unlines $ +displayProofGoal step assertProv goalIdx numTotalGoals why ls = T.unlines $ [ banner , "Emitted a proof goal (" <> why <> ")" , " During the " <> displayStep + , " Required for proving the " <> displayAssertProv , " Proof goal " <> T.pack (show goalIdx) <> " (" <> T.pack (show numTotalGoals) @@ -683,6 +720,35 @@ "initial bisimulation state step" StepBisimulation -> "transition step of bisimulation" + displayAssertProv = + case assertProv of + VerifierProvenance -> + "correspondence between the spec and C code" + StepExecutionProvenance -> + "memory safety of the generated step() function" + +-- | Display information about an emitted proof goal that involves checking the +-- state relation. +displayStateRelationProofGoal :: + VerificationStep + -> StateRelationStep + -> AssertionProvenance + -> Integer + -> Integer + -> Text + -> [Text] + -> Text +displayStateRelationProofGoal verifStep stateRelStep assertProv goalIdx numTotalGoals why = + displayProofGoal verifStep assertProv goalIdx numTotalGoals why' + where + why' :: Text + why' = + case stateRelStep of + PreStepStateRelation -> why <> " before calling step()" + PostStepStateRelation -> why <> " after calling step()" + -- `displayProofGoal` already makes a note of the fact that we're + -- checking the initial state, so no need to do so again here. + InitialStateRelation -> why ppProgramLoc :: WPL.ProgramLoc -> PP.Doc a ppProgramLoc pl = PP.vcat