Basic verification summary implementation (#767)

Implements the necessary plumbing to track everything verified within SAW and report a summary of it all after verification completes. It currently adds one experimental command, `summarize_verification`, which prints a summary of all `Theorem` or `*MethodSpec` values created along with various details about each.

We should adapt the `SolverStats` tracking to include proofs done by rewriting and `trivial`, as well. Currently, proofs based entirely on rewriting are printed as axioms, which isn’t right.

saw-script.cabal

@@ -163,6 +163,8 @@ library
     SAWScript.Prover.Exporter
     SAWScript.Prover.Versions
 
+    SAWScript.VerificationSummary
+
     SAWScript.X86
     SAWScript.X86Spec
 

src/SAWScript/Builtins.hs

@@ -136,6 +136,7 @@ import qualified SAWScript.Prover.ABC as Prover
 import qualified SAWScript.Prover.What4 as Prover
 import qualified SAWScript.Prover.Exporter as Prover
 import qualified SAWScript.Prover.MRSolver as Prover
+import SAWScript.VerificationSummary
 
 showPrim :: SV.Value -> TopLevel String
 showPrim v = do
@@ -506,7 +507,7 @@ beta_reduce_goal =
      return ((), mempty, Just (goal { goalProp = Prop trm' }))
 
 goal_apply :: Theorem -> ProofScript ()
-goal_apply (Theorem (Prop rule)) =
+goal_apply (Theorem (Prop rule) _stats) =
   StateT $ \(ProofState goals concl stats timeout) ->
   case goals of
     [] -> fail "goal_apply failed: no subgoal"
@@ -551,7 +552,7 @@ goal_assume =
           | looseVars body /= emptyBitSet -> fail "goal_assume failed: dependent pi type"
           | otherwise ->
             let goal' = goal { goalProp = Prop body } in
-            return (Theorem (Prop tp), ProofState (goal' : goals') concl stats timeout)
+            return (Theorem (Prop tp) mempty, ProofState (goal' : goals') concl stats timeout)
 
 goal_intro :: String -> ProofScript TypedTerm
 goal_intro s =
@@ -571,7 +572,7 @@ goal_intro s =
              return (tt, ProofState (goal' : goals') concl stats timeout)
 
 goal_insert :: Theorem -> ProofScript ()
-goal_insert (Theorem (Prop t)) =
+goal_insert (Theorem (Prop t) _stats) =
   StateT $ \(ProofState goals concl stats timeout) ->
   case goals of
     [] -> fail "goal_insert failed: no subgoal"
@@ -839,7 +840,7 @@ provePrintPrim script t = do
   opts <- rwPPOpts <$> getTopLevelRW
   case finishProof pstate of
     (_,Just thm) -> do printOutLnTop Info "Valid"
-                       return thm
+                       SV.returnProof thm
     (_,Nothing) -> fail $ "prove: " ++ show (length (psGoals pstate)) ++ " unsolved subgoal(s)\n"
                      ++ SV.showsProofResult opts (SV.flipSatResult r) ""
 
@@ -937,7 +938,7 @@ beta_reduce_term (TypedTerm schema t) = do
   return (TypedTerm schema t')
 
 addsimp :: Theorem -> Simpset -> Simpset
-addsimp (Theorem (Prop t)) ss = addRule (ruleOfProp t) ss
+addsimp (Theorem (Prop t) _stats) ss = addRule (ruleOfProp t) ss
 
 addsimp' :: Term -> Simpset -> Simpset
 addsimp' t ss = addRule (ruleOfProp t) ss
@@ -1293,21 +1294,21 @@ prove_core script input =
      let r = SV.flipSatResult r'
      opts <- rwPPOpts <$> getTopLevelRW
      case finishProof pstate of
-       (_,Just thm) -> return thm
+       (_,Just thm) -> SV.returnProof thm
        (_,Nothing)  -> fail $ "prove_core: " ++ show (length (psGoals pstate)) ++ " unsolved subgoal(s)\n"
                          ++ SV.showsProofResult opts r ""
 
 core_axiom :: String -> TopLevel Theorem
 core_axiom input =
   do t <- parseCore input
-     return (Theorem (Prop t))
+     SV.returnProof (Theorem (Prop t) mempty)
 
 core_thm :: String -> TopLevel Theorem
 core_thm input =
   do t <- parseCore input
      sc <- getSharedContext
      ty <- io $ scTypeOf sc t
-     return (Theorem (Prop ty))
+     SV.returnProof (Theorem (Prop ty) mempty) -- TODO: this is proved, not assumed
 
 get_opt :: Int -> TopLevel String
 get_opt n = do
@@ -1409,3 +1410,12 @@ approxmc t = do
   case msg of
     [l] -> io $ putStrLn l
     _ -> fail $ "Garbled result from approxmc\n\n" ++ out
+
+summarize_verification :: TopLevel ()
+summarize_verification =
+  do values <- rwProofs <$> getTopLevelRW
+     let jspecs  = [ s | SV.VJVMMethodSpec s <- values ]
+         lspecs  = [ s | SV.VLLVMCrucibleMethodSpec s <- values ]
+         thms    = [ t | SV.VTheorem t <- values ]
+         summary = computeVerificationSummary jspecs lspecs thms
+     io $ putStrLn $ prettyVerificationSummary summary

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -238,7 +238,7 @@ crucible_jvm_verify bic opts cls nm lemmas checkSat setup tactic =
      -- attempt to verify the proof obligations
      stats <- verifyObligations cc methodSpec tactic assumes asserts
      io $ writeFinalProfile
-     return (methodSpec & MS.csSolverStats .~ stats)
+     returnProof (methodSpec & MS.csSolverStats .~ stats)
 
 
 crucible_jvm_unsafe_assume_spec ::
@@ -256,7 +256,8 @@ crucible_jvm_unsafe_assume_spec bic opts cls nm setup =
      (_cls', method) <- io $ findMethod cb pos nm cls -- TODO: switch to crucible-jvm version
      let loc = SS.toW4Loc "_SAW_assume_spec" pos
      let st0 = initialCrucibleSetupState cc method loc
-     (view Setup.csMethodSpec) <$> execStateT (runJVMSetupM setup) st0
+     ms <- (view Setup.csMethodSpec) <$> execStateT (runJVMSetupM setup) st0
+     returnProof ms
 
 verifyObligations ::
   JVMCrucibleContext ->

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -266,7 +266,7 @@ crucible_llvm_verify bic opts (Some lm) nm lemmas checkSat setup tactic =
   do lemmas' <- checkModuleCompatibility lm lemmas
      withMethodSpec bic opts lm nm setup $ \cc method_spec ->
        do (res_method_spec, _) <- verifyMethodSpec bic opts cc method_spec lemmas' checkSat tactic Nothing
-          return $ SomeLLVM res_method_spec
+          returnProof $ SomeLLVM res_method_spec
 
 crucible_llvm_unsafe_assume_spec ::
   BuiltinContext   ->
@@ -279,7 +279,7 @@ crucible_llvm_unsafe_assume_spec bic opts (Some lm) nm setup =
   withMethodSpec bic opts lm nm setup $ \_ method_spec ->
   do printOutLnTop Info $
        unwords ["Assume override", (method_spec ^. csName)]
-     return $ SomeLLVM method_spec
+     returnProof $ SomeLLVM method_spec
 
 crucible_llvm_array_size_profile ::
   BuiltinContext ->

src/SAWScript/Crucible/LLVM/X86.hs

@@ -325,9 +325,9 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl
         C.AbortedResult{} -> printOutLn opts Warn "Warning: function never returns"
         C.TimeoutResult{} -> fail "Execution timed out"
 
-      checkGoals sym opts sc tactic
+      stats <- checkGoals sym opts sc tactic
 
-      pure $ SomeLLVM methodSpec
+      returnProof $ SomeLLVM (methodSpec & MS.csSolverStats .~ stats)
   | otherwise = fail "LLVM module must be 64-bit"
 
 --------------------------------------------------------------------------------
@@ -782,21 +782,20 @@ checkGoals ::
   Options ->
   SharedContext ->
   ProofScript SatResult ->
-  TopLevel ()
+  TopLevel SolverStats
 checkGoals sym opts sc tactic = do
   gs <- liftIO $ getGoals sym
   liftIO . printOutLn opts Info $ mconcat
     [ "Simulation finished, running solver on "
     , show $ length gs
     , " goals"
     ]
-  forM_ (zip [0..] gs) $ \(n, g) -> do
+  stats <- forM (zip [0..] gs) $ \(n, g) -> do
     term <- liftIO $ gGoal sc g
     let proofgoal = ProofGoal n "vc" (show $ gMessage g) term
     r <- evalStateT tactic $ startProof proofgoal
     case r of
-      Unsat stats -> do
-        liftIO . printOutLn opts Info $ ppStats stats
+      Unsat stats -> return stats
       SatMulti stats vals -> do
         printOutLnTop Info $ unwords ["Subgoal failed:", show $ gMessage g]
         printOutLnTop Info (show stats)
@@ -810,3 +809,4 @@ checkGoals sym opts sc tactic = do
         printOutLnTop OnlyCounterExamples "----------------------------------"
         throwTopLevel "Proof failed."
   liftIO $ printOutLn opts Info "All goals succeeded"
+  return (mconcat stats)

src/SAWScript/Interpreter.hs

@@ -424,6 +424,7 @@ buildTopLevelEnv proxy opts =
                    , rwTypedef    = Map.empty
                    , rwDocs       = primDocEnv primsAvail
                    , rwCryptol    = ce0
+                   , rwProofs     = []
                    , rwPPOpts     = SAWScript.Value.defaultPPOpts
                    , rwJVMTrans   = jvmTrans
                    , rwPrimsAvail = primsAvail
@@ -2392,6 +2393,13 @@ primitives = Map.fromList
     (pureVal disable_crucible_profiling)
     Current
     ["Stop recording profiling information."]
+
+  , prim "summarize_verification" "TopLevel ()"
+    (pureVal summarize_verification)
+    Experimental
+    [ "Print a human-readable summary of all verifications performed"
+    , "so far."
+    ]
   ]
 
   where

src/SAWScript/Proof.hs

@@ -19,7 +19,11 @@ newtype Prop = Prop { unProp :: Term }
 
 -- | A theorem is a proposition which has been wrapped in a
 -- constructor indicating that it has already been proved.
-data Theorem = Theorem { thmProp :: Prop }
+data Theorem =
+  Theorem
+  { thmProp :: Prop
+  , thmStats :: SolverStats
+  }
 
 -- | A @ProofGoal@ contains a proposition to be proved, along with
 -- some metadata.
@@ -103,5 +107,5 @@ startProof g = ProofState [g] g mempty Nothing
 finishProof :: ProofState -> (SolverStats, Maybe Theorem)
 finishProof (ProofState gs concl stats _) =
   case gs of
-    []    -> (stats, Just (Theorem (goalProp concl)))
+    []    -> (stats, Just (Theorem (goalProp concl) stats))
     _ : _ -> (stats, Nothing)

src/SAWScript/Value.hs

@@ -278,7 +278,7 @@ showsPrecValue opts p v =
     VTopLevel {} -> showString "<<TopLevel>>"
     VSimpset ss -> showString (showSimpset opts ss)
     VProofScript {} -> showString "<<proof script>>"
-    VTheorem (Theorem (Prop t)) ->
+    VTheorem (Theorem (Prop t) _stats) ->
       showString "Theorem " .
       showParen True (showString (SAWCorePP.scPrettyTerm opts' t))
     VJavaSetup {} -> showString "<<Java Setup>>"
@@ -385,6 +385,7 @@ data TopLevelRW =
   , rwTypedef :: Map SS.Name SS.Type
   , rwDocs    :: Map SS.Name String
   , rwCryptol :: CEnv.CryptolEnv
+  , rwProofs  :: [Value] {- ^ Values, generated anywhere, that represent proofs. -}
   , rwPPOpts  :: PPOpts
   -- , rwCrucibleLLVMCtx :: Crucible.LLVMContext
   , rwJVMTrans :: CJ.JVMContext
@@ -461,6 +462,12 @@ getTopLevelRW = TopLevel get
 putTopLevelRW :: TopLevelRW -> TopLevel ()
 putTopLevelRW rw = TopLevel (put rw)
 
+returnProof :: IsValue v => v -> TopLevel v
+returnProof v = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwProofs = toValue v : rwProofs rw }
+  return v
+
 -- | Access the current state of Java Class translation
 getJVMTrans :: TopLevel  CJ.JVMContext
 getJVMTrans = TopLevel (gets rwJVMTrans)

src/SAWScript/VerificationSummary.hs

@@ -0,0 +1,104 @@
+{-# LANGUAGE OverloadedStrings #-}
+{- |
+Module      : SAWScript.VerificationSummary
+Description : Summaries of verification for human consumption.
+License     : BSD3
+Maintainer  : atomb
+-}
+
+module SAWScript.VerificationSummary
+  ( computeVerificationSummary
+  , prettyVerificationSummary
+  ) where
+
+import Control.Lens
+import qualified Data.Set as Set
+import Data.String
+import Text.PrettyPrint.ANSI.Leijen
+
+import qualified Lang.Crucible.JVM as CJ
+import SAWScript.Crucible.Common.MethodSpec
+import qualified SAWScript.Crucible.Common.MethodSpec as CMS
+import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMSLLVM
+import qualified SAWScript.Crucible.JVM.MethodSpecIR as CMSJVM
+import SAWScript.Proof
+import SAWScript.Prover.SolverStats
+import qualified Verifier.SAW.Term.Pretty as PP
+
+type JVMTheorem =  CMS.CrucibleMethodSpecIR CJ.JVM
+type LLVMTheorem = CMSLLVM.SomeLLVM CMS.CrucibleMethodSpecIR
+
+data VerificationSummary =
+  VerificationSummary
+  { vsJVMMethodSpecs :: [JVMTheorem]
+  , vsLLVMMethodSpecs :: [LLVMTheorem]
+  , vsTheorems :: [Theorem]
+  }
+
+vsVerifSolvers :: VerificationSummary -> Set.Set String
+vsVerifSolvers vs =
+  Set.unions $
+  map (\ms -> solverStatsSolvers (ms ^. csSolverStats)) (vsJVMMethodSpecs vs) ++
+  map (\(CMSLLVM.SomeLLVM ms) -> solverStatsSolvers (ms ^. csSolverStats)) (vsLLVMMethodSpecs vs)
+
+vsTheoremSolvers :: VerificationSummary -> Set.Set String
+vsTheoremSolvers = Set.unions . map getSolvers . vsTheorems
+  where getSolvers (Theorem _ ss) = solverStatsSolvers ss
+
+vsAllSolvers :: VerificationSummary -> Set.Set String
+vsAllSolvers vs = Set.union (vsVerifSolvers vs) (vsTheoremSolvers vs)
+
+computeVerificationSummary :: [JVMTheorem] -> [LLVMTheorem] -> [Theorem] -> VerificationSummary
+computeVerificationSummary = VerificationSummary
+
+prettyVerificationSummary :: VerificationSummary -> String
+prettyVerificationSummary vs@(VerificationSummary jspecs lspecs thms) =
+  show $ vsep
+  [ prettyJVMSpecs jspecs
+  , prettyLLVMSpecs lspecs
+  , prettyTheorems thms
+  , prettySolvers (Set.toList (vsAllSolvers vs))
+  ] where
+      section nm = "#" <+> nm
+      item txt = "*" <+> txt
+      code txt = vsep ["~~~~", txt, "~~~~"]
+      subitem = indent 4 . item
+      sectionWithItems _ _ [] = mempty
+      sectionWithItems nm prt items =
+        vsep [section nm, "", vsep (map prt items)]
+      verifStatus s = if Set.null (solverStatsSolvers (s ^. CMS.csSolverStats))
+                      then "assumed"
+                      else "verified"
+      -- TODO: ultimately the goal is for the following to summarize all
+      -- preconditions made by this verification, but we need to extract
+      -- a bunch more information for that to be meaningful.
+      {-
+      condStatus s = (if null (s ^. (CMS.csPreState . CMS.csConditions))
+                      then "without"
+                      else "with") <+> "conditions"
+                      -}
+      prettyJVMSpecs ss =
+        sectionWithItems "JVM Methods Analyzed" prettyJVMSpec ss
+      prettyJVMSpec s =
+        vsep [ item (fromString (s ^. CMSJVM.csMethodName))
+             -- , subitem (condStatus s)
+             , subitem (verifStatus s)
+             ]
+      prettyLLVMSpecs ss =
+        sectionWithItems "LLVM Functions Analyzed" prettyLLVMSpec ss
+      prettyLLVMSpec (CMSLLVM.SomeLLVM s) =
+        vsep [ item (fromString (s ^. CMSLLVM.csName))
+             -- , subitem (condStatus s)
+             , subitem (verifStatus s)
+             ]
+      prettyTheorems ts =
+        sectionWithItems "Theorems Proved or Assumed" (item . prettyTheorem) ts
+      prettyTheorem t =
+        vsep [ if Set.null (solverStatsSolvers (thmStats t))
+               then "Axiom:"
+               else "Theorem:"
+             , code (indent 2 (PP.ppTerm PP.defaultPPOpts (unProp (thmProp t))))
+             , ""
+             ]
+      prettySolvers ss =
+        sectionWithItems "Solvers Used" (item . fromString) ss