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 }} 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