diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,7 @@ +2024-03-08 + * Version bump (3.19). (#53) + * Provide more detailed feedback upon a successful run of the verifier. + * Make the examples build with Copilot 3.19. (#53) + +2024-02-06 + * Initial release of `copilot-verifier`. diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 --- a/CHANGELOG.md +++ /dev/null @@ -1,5 +0,0 @@ -# Release history for copilot-verifier - -## 0.1 (February 2024) - -* Initial release of `copilot-verifier. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,9 +1,11 @@ +[![Build Status](https://github.com/Copilot-Language/copilot-verifier/workflows/copilot-verifier/badge.svg)](https://github.com/Copilot-Language/copilot-verifier/actions?query=workflow%3Acopilot-verifier) +[![Version on Hackage](https://img.shields.io/hackage/v/copilot-verifier.svg)](https://hackage.haskell.org/package/copilot-verifier) + # Copilot Verifier -This "Copilot Verifier" is an add-on to the -[Copilot Stream DSL](https://copilot-language.github.io) -for verifying the correctness of C code generated -by the `copilot-c99` package. +Copilot Verifier is an add-on to the [Copilot Stream +DSL](https://copilot-language.github.io) for verifying the correctness of C +code generated by the `copilot-c99` package. The main idea of the verifier is to use the [Crucible symbolic simulator](https://github.com/galoisinc/crucible) @@ -14,6 +16,10 @@ verification conditions are then dispatched to SMT solvers to be automatically solved. We will have more to say about exactly what is meant by this correspondence below. + +Copilot Verifier is described in the ICFP 2023 paper [_Trustworthy Runtime +Verification via Bisimulation (Experience +Report)_](https://dl.acm.org/doi/abs/10.1145/3607841). ## Building 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: 0.1 +Version: 3.19 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024 @@ -10,17 +10,18 @@ Category: Language Synopsis: System for verifying the correctness of generated Copilot programs Description: - @copilot-verifier@ is an add-on to the for verifying the correctness of C code generated by the - @copilot-c99@ package. + @copilot-verifier@ is an add-on to the [Copilot Stream + DSL](https://copilot-language.github.io) for verifying the correctness of C + code generated by the @copilot-c99@ package. . - @copilot-verifier@ uses the to interpret the semantics of the generated C program and - and to produce verification conditions sufficient to guarantee that the - meaning of the generated program corresponds in a precise way to the meaning - of the original stream specification. The generated verification conditions - are then dispatched to SMT solvers to be automatically solved. -extra-doc-files: CHANGELOG.md, README.md + @copilot-verifier@ uses the [Crucible symbolic + simulator](https://github.com/galoisinc/crucible) to interpret the semantics + of the generated C program and and to produce verification conditions + sufficient to guarantee that the meaning of the generated program corresponds + in a precise way to the meaning of the original stream specification. The + generated verification conditions are then dispatched to SMT solvers to be + automatically solved. +extra-doc-files: CHANGELOG, README.md source-repository head type: git @@ -44,13 +45,13 @@ bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0, - copilot >= 3.18.1 && < 3.19, - copilot-c99 >= 3.18.1 && < 3.19, - copilot-core >= 3.18.1 && < 3.19, - copilot-libraries >= 3.18.1 && < 3.19, - copilot-language >= 3.18.1 && < 3.19, - copilot-prettyprinter >= 3.18.1 && < 3.19, - copilot-theorem >= 3.18.1 && < 3.19, + copilot >= 3.19 && < 3.20, + copilot-c99 >= 3.19 && < 3.20, + copilot-core >= 3.19 && < 3.20, + copilot-libraries >= 3.19 && < 3.20, + copilot-language >= 3.19 && < 3.20, + copilot-prettyprinter >= 3.19 && < 3.20, + copilot-theorem >= 3.19 && < 3.20, crucible >= 0.7 && < 0.8, crucible-llvm >= 0.6 && < 0.7, crux >= 0.7 && < 0.8, 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 @@ -10,7 +10,7 @@ data S = S { field :: Field "field" Int16 } instance Struct S where - typename _ = "s" + typeName _ = "s" toValues s = [Value Int16 (field s)] instance Typed S where 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 @@ -24,7 +24,7 @@ -- | `Struct` instance for `Volts`. instance Struct Volts where - typename _ = "volts" + typeName _ = "volts" toValues vlts = [ Value Word16 (numVolts vlts) , Value Bool (flag vlts) ] @@ -41,7 +41,7 @@ -- | `Battery` instance for `Struct`. instance Struct Battery where - typename _ = "battery" + typeName _ = "battery" toValues battery = [ Value typeOf (temp battery) , Value typeOf (volts battery) , Value typeOf (other battery) diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs b/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs --- a/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs +++ b/examples/Copilot/Verifier/Examples/ShouldPass/WCV.hs @@ -9,13 +9,12 @@ module Copilot.Verifier.Examples.ShouldPass.WCV where import Language.Copilot -import qualified Copilot.Theorem.What4 as CT +-- import qualified Copilot.Theorem.What4 as CT import Copilot.Compile.C99 import Copilot.Verifier ( Verbosity, VerifierOptions(..) , defaultVerifierOptions, verifyWithOptions ) -import qualified Prelude as P -import Data.Foldable (forM_) +-- import Data.Foldable (forM_) import qualified Control.Monad as Monad @@ -38,44 +37,6 @@ type Vect2 = (Stream Double, Stream Double) --------------------------------- --- External streams for relative position and velocity. --------------------------------- - --- | The relative x velocity between ownship and the intruder. -vx :: Stream Double -vx = extern "relative_velocity_x" Nothing - --- | The relative y velocity between ownship and the intruder. -vy :: Stream Double -vy = extern "relative_velocity_y" Nothing - --- | The relative z velocity between ownship and the intruder. -vz :: Stream Double -vz = extern "relative_velocity_z" Nothing - --- | The relative velocity as a 2D vector. -v :: (Stream Double, Stream Double) -v = (vx, vy) - - --- | The relative x position between ownship and the intruder. -sx :: Stream Double -sx = extern "relative_position_x" Nothing - --- | The relative y position between ownship and the intruder. -sy :: Stream Double -sy = extern "relative_position_y" Nothing - --- | The relative z position between ownship and the intruder. -sz :: Stream Double -sz = extern "relative_position_z" Nothing - --- | The relative position as a 2D vector. -s :: (Stream Double, Stream Double) -s = (sx, sy) - - ------------------ -- The following section contains basic libraries for working with vectors. ------------------ @@ -169,7 +130,41 @@ (norm s <= dthr) || (((dcpa s v) <= dthr) && (0 <= (tvar s v)) && ((tvar s v) <= tthr)) +spec :: Spec spec = do + -- External streams for relative position and velocity. + let -- The relative x velocity between ownship and the intruder. + vx :: Stream Double + vx = extern "relative_velocity_x" Nothing + + -- The relative y velocity between ownship and the intruder. + vy :: Stream Double + vy = extern "relative_velocity_y" Nothing + + -- The relative z velocity between ownship and the intruder. + vz :: Stream Double + vz = extern "relative_velocity_z" Nothing + + -- The relative velocity as a 2D vector. + v :: (Stream Double, Stream Double) + v = (vx, vy) + + + -- The relative x position between ownship and the intruder. + sx :: Stream Double + sx = extern "relative_position_x" Nothing + + -- The relative y position between ownship and the intruder. + sy :: Stream Double + sy = extern "relative_position_y" Nothing + + -- The relative z position between ownship and the intruder. + sz :: Stream Double + sz = extern "relative_position_z" Nothing + + -- The relative position as a 2D vector. + s :: (Stream Double, Stream Double) + s = (sx, sy) Monad.void $ prop "1a" (forAll $ (tau s v) ~= (tau (neg s) (neg v))) -- Monad.void $ prop "3d" (forAll $ (wcv tep s sz v vz) == (wcv tep (neg s) (-sz) (neg v) (-vz))) trigger "well_clear_violation" (wcv tep s sz v vz) [] diff --git a/src/Copilot/Verifier.hs b/src/Copilot/Verifier.hs --- a/src/Copilot/Verifier.hs +++ b/src/Copilot/Verifier.hs @@ -255,7 +255,7 @@ Log.sayCopilot $ Log.CompiledBitcodeFile prefix bcFile -- Run the main verification procedure - verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile + verifyBitcode opts csettings properties spec cruxOpts llvmOpts csrc bcFile -- | Do the (surprisingly large amount) of options munging necessary to set up @@ -325,9 +325,10 @@ Spec {- ^ The input Copilot specification -} -> CruxOptions {- ^ Crux options -} -> LLVMOptions {- ^ CruxLLVM options -} -> + FilePath {- ^ Path to the generated C file (for logging purposes only) -} -> FilePath {- ^ Path to the bitcode file to verify -} -> IO () -verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile = +verifyBitcode opts csettings properties spec cruxOpts llvmOpts cFile bcFile = do -- Set up the expression builder and symbolic backend halloc <- newHandleAllocator sym <- newExprBuilder FloatUninterpretedRepr CopilotVerifierData globalNonceGenerator @@ -383,13 +384,28 @@ -- First check that the initial state of the program matches the starting -- segment of the associated Copilot streams. let cruxOptsInit = setCruxOfflineSolverOutput "initial-step" cruxOpts - verifyInitialState cruxOptsInit adapters clRefs simctx initialMem - (CW4.initialStreamState proofStateBundle) + initGoals <- + verifyInitialState cruxOptsInit adapters clRefs simctx initialMem + (CW4.initialStreamState proofStateBundle) -- Now, the real meat. Carry out the bisimulation step of the proof. let cruxOptsTrans = setCruxOfflineSolverOutput "transition-step" cruxOpts - verifyStepBisimulation opts cruxOptsTrans adapters csettings - clRefs simctx llvmMod trans memVar initialMem proofStateBundle + bisimGoals <- + verifyStepBisimulation opts cruxOptsTrans adapters csettings + clRefs simctx llvmMod trans memVar initialMem proofStateBundle + + Log.sayCopilot $ Log.SuccessfulProofSummary cFile initGoals bisimGoals + -- We only want to inform users about Noisy if the verbosity level is + -- sufficiently low. Crux's logging framework isn't particularly + -- suited to doing this, as it assumes that all log messages enabled + -- for low verbosity levels should also be enabled for higher + -- verbosity levels. That is a reasonable assumption most of the time, + -- but not here. + -- + -- To compensate, we hack around the issue by manually checking the + -- verbosity level before logging the message. + when (verbosity opts < Noisy) $ + Log.sayCopilot Log.NoisyVerbositySuggestion where -- If @logSmtInteractions@ is enabled, enable offline solver output in the -- supplied 'CruxOptions' with the supplied file template. Otherwise, return @@ -433,7 +449,7 @@ SimCtxt Crux sym LLVM -> MemImpl sym -> CW4.BisimulationProofState sym -> - IO () + IO Integer verifyInitialState cruxOpts adapters clRefs simctx mem initialState = withBackend simctx $ \bak -> do Log.sayCopilot $ Log.ComputingConditions Log.InitialState @@ -473,7 +489,7 @@ GlobalVar Mem -> MemImpl sym -> CW4.BisimulationProofBundle sym -> - IO () + IO Integer verifyStepBisimulation opts cruxOpts adapters csettings clRefs simctx llvmMod modTrans memVar mem prfbundle = withBackend simctx $ \bak -> do Log.sayCopilot $ Log.ComputingConditions Log.StepBisimulation @@ -1279,7 +1295,7 @@ CopilotLogRefs sym -> Log.VerificationStep -> SimCtxt Crux sym LLVM -> - IO () + IO Integer proveObls cruxOpts adapters clRefs step simctx = withBackend simctx $ \bak -> do let sym = backendGetSym bak @@ -1300,6 +1316,9 @@ summarizeObls _ (Just obls) = map (view labeledPredMsg . proofGoal) (goalsToList obls) -} +-- | Compute the number of goals that were proven during verification, logging +-- the goals as they are proven. If all goals are proven successfully, return +-- the number of goals. Otherwise, log the failing proof goals and abort. presentResults :: Log.Logs msgs => Log.SupportsCopilotLogMessage msgs => @@ -1309,15 +1328,17 @@ LLVMAnnMap sym -> Log.VerificationStep -> (ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) -> - IO () + IO Integer presentResults sym vaMap laMap step (num, goals) | numTotalGoals == 0 - = Log.sayCopilot Log.AllGoalsProved + = do Log.sayCopilot Log.AllGoalsProved + pure 0 -- All goals were proven | numProvedGoals == numTotalGoals = do traverse_ (logVerifierAssertions sym vaMap laMap step num) goals printGoals + pure numProvedGoals -- There were some unproved goals, so fail with exit code 1 | otherwise 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 @@ -81,6 +81,15 @@ -> Integer -- ^ Number of total goals -> CopilotLogMessage + SuccessfulProofSummary :: + FilePath + -- ^ Name of the generated C file. + -> Integer + -- ^ Number of goals proven during for the initial state of the proof. + -> Integer + -- ^ Number of goals proven during the bisimulation step of the proof. + -> CopilotLogMessage + NoisyVerbositySuggestion :: CopilotLogMessage ----- -- Types of proof goals the verifier emits @@ -448,6 +457,36 @@ [ "Proved", T.pack (show numProvedGoals) , "of" , T.pack (show numTotalGoals), "total goals" + ] +copilotLogMessageToSayWhat (SuccessfulProofSummary cFileName initGoals bisimGoals) = + copilotSimply $ T.unlines + [ "" + , "copilot-verifier has produced a mathematical proof that the behavior of" + , "the generated C program (" <> T.pack cFileName + <> ") precisely matches the behavior of" + , "the Copilot specification. This proof shows that the behaviors match for" + , "all possible moments in time, and in doing so, copilot-verifier examined" + , "how the programs behave at the start of execution (the \"initial state\")" + , "and at an arbitrary point of time in execution (the \"step bisimulation\")." + , "copilot-verifier decomposed the overall proof into smaller goals, the" + , "number of which depends on the size and complexity of the program. In this" + , "example, there are " <> T.pack (show initGoals) <> " initial state goal(s)" + <> " and " <> T.pack (show bisimGoals) <> " step bisimulation goal(s)," + , "and copilot-verifier was able to prove all of them." + ] +copilotLogMessageToSayWhat NoisyVerbositySuggestion = + copilotSimply $ T.unlines + [ "" + , "copilot-verifier is displaying an abridged summary of the verification results." + , "copilot-verifier also includes a \"noisy\" mode that prints detailed" + , "descriptions of each individual proof goal, including what type of goal it is," + , "why it needs to be proven, and where in the Copilot specification and/or C code" + , "the proof goal originated from. To enable noisy mode, invoke the verifier with" + , "the following options:" + , "" + , "```" + , "verifyWithOptions (defaultVerifierOptions { verbosity = Noisy }) ..." + , "```" ] copilotLogMessageToSayWhat (StreamValueEqualityProofGoal step goalIdx numTotalGoals