From 5b86f7b3dcdc50877936c0172de14c29139e863c Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 29 Feb 2024 11:50:30 -0500 Subject: [PATCH 1/2] Better user feedback upon a successful verification Upon a successful run of the verifier, we now print out a general description of what `copilot-verifier` did, along with brief explanations of what the various proof goals indicate. This should make it easier to interpret the results if you are not an expert in formal verification. We also print out a suggestion to turn the verbosity to `Noisy` if you want a more detailed look into what each proof goal means. --- copilot-verifier-demo/src/Demo1.hs | 4 +- copilot-verifier/src/Copilot/Verifier.hs | 43 +++++++++++++++----- copilot-verifier/src/Copilot/Verifier/Log.hs | 39 ++++++++++++++++++ 3 files changed, 73 insertions(+), 13 deletions(-) diff --git a/copilot-verifier-demo/src/Demo1.hs b/copilot-verifier-demo/src/Demo1.hs index f8c460b..919c255 100644 --- a/copilot-verifier-demo/src/Demo1.hs +++ b/copilot-verifier-demo/src/Demo1.hs @@ -27,6 +27,6 @@ main :: IO () main = do interpret 6 spec - -- spec' <- reify spec + spec' <- reify spec -- compile "demo1" spec' - -- verify mkDefaultCSettings [] "demo1" spec' \ No newline at end of file + verifyWithOptions defaultVerifierOptions{verbosity = Noisy} mkDefaultCSettings [] "demo1" spec' diff --git a/copilot-verifier/src/Copilot/Verifier.hs b/copilot-verifier/src/Copilot/Verifier.hs index 40c8c12..2ea1657 100644 --- a/copilot-verifier/src/Copilot/Verifier.hs +++ b/copilot-verifier/src/Copilot/Verifier.hs @@ -255,7 +255,7 @@ verifyWithOptions opts csettings0 properties prefix spec = 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 @@ verifyBitcode :: 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 @@ verifyBitcode opts csettings properties spec cruxOpts llvmOpts bcFile = -- 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 @@ verifyInitialState :: 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 @@ verifyStepBisimulation :: 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 @@ proveObls :: 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 _ Nothing = [] 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 @@ presentResults :: 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/copilot-verifier/src/Copilot/Verifier/Log.hs b/copilot-verifier/src/Copilot/Verifier/Log.hs index 14eef42..9cc2b18 100644 --- a/copilot-verifier/src/Copilot/Verifier/Log.hs +++ b/copilot-verifier/src/Copilot/Verifier/Log.hs @@ -81,6 +81,15 @@ data CopilotLogMessage where -> 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 @@ -449,6 +458,36 @@ copilotLogMessageToSayWhat (OnlySomeGoalsProved numProvedGoals numTotalGoals) = , "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 (StreamValueEquality From 1e6616bbd1b845801d819a66ab7c2762d8ba8c06 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 29 Feb 2024 13:07:34 -0500 Subject: [PATCH 2/2] CI: Use haskell-actions/setup --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index e9f08a3..75c6778 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -30,7 +30,7 @@ jobs: with: submodules: true - - uses: haskell/actions/setup@v1 + - uses: haskell-actions/setup@v2 id: setup-haskell with: ghc-version: ${{ matrix.ghc-version }}