Skip to content

Commit f1af89b

Browse files
RyanGlScottRyanGlScott
committed
Use Crux's logging framework for copilot-verifier log messages
1 parent b5b8484 commit f1af89b

3 files changed

Lines changed: 158 additions & 36 deletions

File tree

‎copilot-verifier/copilot-verifier.cabal‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@ common bldflags
2323
default-extensions:
2424
NondecreasingIndentation
2525
build-depends:
26+
aeson >= 1.5 && < 2.1,
2627
base >= 4.8 && < 4.15,
2728
bv-sized >= 1.0.0 && < 1.1,
2829
bytestring,
@@ -55,6 +56,7 @@ library
5556
hs-source-dirs: src
5657
exposed-modules:
5758
Copilot.Verifier
59+
Copilot.Verifier.Log
5860

5961
library copilot-verifier-examples
6062
import: bldflags

‎copilot-verifier/src/Copilot/Verifier.hs‎

Lines changed: 66 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
11
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE DeriveAnyClass #-}
3+
{-# LANGUAGE DeriveGeneric #-}
4+
{-# LANGUAGE DerivingStrategies #-}
25
{-# LANGUAGE ExplicitNamespaces #-}
36
{-# LANGUAGE GADTs #-}
47
{-# LANGUAGE OverloadedStrings #-}
@@ -16,6 +19,7 @@ import Control.Lens (view, (^.), to)
1619
import Control.Monad (foldM, forM_)
1720
import Control.Monad.IO.Class (liftIO)
1821
import Control.Monad.State (execStateT, lift, StateT(..))
22+
import Data.Aeson (ToJSON)
1923
import qualified Data.Text as Text
2024
import qualified Data.Map.Strict as Map
2125
import Data.IORef (newIORef, modifyIORef, IORef)
@@ -25,6 +29,7 @@ import Data.List.NonEmpty (NonEmpty(..))
2529
import qualified Data.List.NonEmpty as NE
2630
import qualified Data.Vector as V
2731
import qualified Data.BitVector.Sized as BV
32+
import GHC.Generics (Generic)
2833
import qualified Prettyprinter as PP
2934
import System.Exit (exitFailure)
3035
import System.FilePath ((</>))
@@ -35,6 +40,8 @@ import qualified Copilot.Core.Type as CT
3540

3641
import qualified Copilot.Theorem.What4 as CW4
3742

43+
import qualified Copilot.Verifier.Log as Log
44+
3845
import Data.Parameterized.Ctx (EmptyCtx)
3946
import Data.Parameterized.Context (pattern Empty)
4047
import qualified Data.Parameterized.Context as Ctx
@@ -103,19 +110,14 @@ import Crux.Config (cfgJoin, Config(..))
103110
import Crux.Config.Load (fromFile, fromEnv)
104111
import Crux.Config.Common (cruxOptions, CruxOptions(..), postprocessOptions, outputOptions )
105112
import Crux.Goal (proveGoalsOffline, provedGoalsTree)
106-
import Crux.Log
107-
( cruxLogMessageToSayWhat, withCruxLogMessage, outputHandle
108-
, Logs, SupportsCruxLogMessage, logGoal
109-
)
113+
import qualified Crux.Log as Log
110114
import Crux.Types (SimCtxt, Crux, ProcessedGoals(..), ProofResult(..))
111115

112116
import Crux.LLVM.Config (llvmCruxConfig, LLVMOptions(..))
113117
import Crux.LLVM.Compile (genBitCode)
118+
import qualified Crux.LLVM.Log as Log
114119
import Crux.LLVM.Simulate (setupSimCtxt, parseLLVM, explainFailure)
115-
import CruxLLVMMain
116-
( CruxLLVMLogging, withCruxLLVMLogging
117-
, cruxLLVMLoggingToSayWhat, processLLVMOptions
118-
)
120+
import CruxLLVMMain (processLLVMOptions)
119121

120122
import What4.Config
121123
(extendConfig)
@@ -137,6 +139,7 @@ import What4.Symbol (safeSymbol)
137139

138140
verify :: CSettings -> [String] -> String -> Spec -> IO ()
139141
verify csettings0 properties prefix spec =
142+
withCopilotLogging $
140143
do (cruxOpts, llvmOpts, csettings, csrc) <-
141144
do llvmcfg <- llvmCruxConfig
142145
let cfg = cfgJoin cruxOptions llvmcfg
@@ -152,24 +155,26 @@ verify csettings0 properties prefix spec =
152155
let csettings = csettings0{ cSettingsOutputDirectory = odir }
153156
let csrc = odir </> prefix ++ ".c"
154157
let cruxOpts1 = cruxOpts0{ outDir = odir, bldDir = odir, inputFiles = [csrc] }
155-
ocfg <- defaultOutputConfig cruxLogMessageToSayWhat
158+
ocfg <- defaultOutputConfig copilotLoggingToSayWhat
156159
let ?outputConfig = ocfg (Just (outputOptions cruxOpts1))
157-
cruxOpts2 <- withCruxLogMessage (postprocessOptions cruxOpts1)
160+
cruxOpts2 <- postprocessOptions cruxOpts1
158161
(cruxOpts3, llvmOpts2) <- processLLVMOptions (cruxOpts2, llvmOpts0{ optLevel = 0 })
159162
return (cruxOpts3, llvmOpts2, csettings, csrc)
160163

161164
compileWith csettings prefix spec
162-
putStrLn ("Generated " ++ show csrc)
163-
164-
ocfg <- defaultOutputConfig cruxLLVMLoggingToSayWhat
165+
ocfg <- defaultOutputConfig copilotLoggingToSayWhat
165166
let ?outputConfig = ocfg (Just (outputOptions cruxOpts))
166-
bcFile <- withCruxLLVMLogging (genBitCode cruxOpts llvmOpts)
167-
putStrLn ("Compiled " ++ prefix ++ " into " ++ bcFile)
167+
Log.sayCopilot $ Log.GeneratedCFile csrc
168+
169+
bcFile <- genBitCode cruxOpts llvmOpts
170+
Log.sayCopilot $ Log.CompiledBitcodeFile prefix bcFile
168171

169172
verifyBitcode csettings properties spec cruxOpts llvmOpts bcFile
170173

171174
verifyBitcode ::
172-
Logs CruxLLVMLogging =>
175+
Log.Logs msgs =>
176+
Log.SupportsCruxLogMessage msgs =>
177+
Log.SupportsCopilotLogMessage msgs =>
173178
CSettings ->
174179
[String] ->
175180
Spec ->
@@ -184,23 +189,21 @@ verifyBitcode csettings properties spec cruxOpts llvmOpts bcFile =
184189
startCaching sym
185190
bbMapRef <- newIORef mempty
186191
let ?recordLLVMAnnotation = \an bb -> modifyIORef bbMapRef (Map.insert an bb)
187-
ocfg <- defaultOutputConfig cruxLLVMLoggingToSayWhat
188-
let ?outputConfig = ocfg (Just (outputOptions cruxOpts))
189192

190193
let adapters = [z3Adapter] -- TODO? configurable
191194
extendConfig (solver_adapter_config_options z3Adapter) (getConfiguration sym)
192195

193196
memVar <- mkMemVar "llvm_memory" halloc
194197

195198
let simctx = (setupSimCtxt halloc sym (memOpts llvmOpts) memVar)
196-
{ printHandle = view outputHandle ?outputConfig }
199+
{ printHandle = view Log.outputHandle ?outputConfig }
197200

198201
llvmMod <- parseLLVM bcFile
199202
(Some trans, _warns) <-
200203
let ?transOpts = transOpts llvmOpts
201204
in translateModule halloc memVar llvmMod
202205

203-
putStrLn ("Translated bitcode into Crucible")
206+
Log.sayCopilot Log.TranslatedToCrucible
204207

205208
let llvmCtxt = trans ^. transContext
206209
let ?lc = llvmCtxt ^. llvmTypeCtx
@@ -209,11 +212,10 @@ verifyBitcode csettings properties spec cruxOpts llvmOpts bcFile =
209212

210213
llvmPtrWidth llvmCtxt $ \ptrW ->
211214
withPtrWidth ptrW $
212-
withCruxLLVMLogging $
213215
do emptyMem <- initializeAllMemory sym llvmCtxt llvmMod
214216
initialMem <- populateAllGlobals sym (globalInitMap trans) emptyMem
215217

216-
putStrLn "Generating proof state data"
218+
Log.sayCopilot Log.GeneratingProofState
217219
proofStateBundle <- CW4.computeBisimulationProofBundle sym properties spec
218220

219221
verifyInitialState cruxOpts adapters bbMapRef simctx initialMem
@@ -224,8 +226,9 @@ verifyBitcode csettings properties spec cruxOpts llvmOpts bcFile =
224226

225227
verifyInitialState ::
226228
IsSymInterface sym =>
227-
Logs msgs =>
228-
SupportsCruxLogMessage msgs =>
229+
Log.Logs msgs =>
230+
Log.SupportsCruxLogMessage msgs =>
231+
Log.SupportsCopilotLogMessage msgs =>
229232
sym ~ ExprBuilder t st fs =>
230233
HasPtrWidth wptr =>
231234
HasLLVMAnn sym =>
@@ -241,20 +244,21 @@ verifyInitialState ::
241244
IO ()
242245
verifyInitialState cruxOpts adapters bbMapRef simctx mem initialState =
243246
do let sym = simctx^.ctxSymInterface
244-
putStrLn "Computing initial state verification conditions"
247+
Log.sayCopilot $ Log.ComputingConditions Log.InitialState
245248
frm <- pushAssumptionFrame sym
246249

247250
assertStateRelation sym mem initialState
248251

249252
popUntilAssumptionFrame sym frm
250253

251-
putStrLn "Proving initial state verification conditions"
254+
Log.sayCopilot $ Log.ProvingConditions Log.InitialState
252255
proveObls cruxOpts adapters bbMapRef simctx
253256

254257
verifyStepBisimulation ::
255258
IsSymInterface sym =>
256-
Logs msgs =>
257-
SupportsCruxLogMessage msgs =>
259+
Log.Logs msgs =>
260+
Log.SupportsCruxLogMessage msgs =>
261+
Log.SupportsCopilotLogMessage msgs =>
258262
sym ~ ExprBuilder t st fs =>
259263
HasPtrWidth wptr =>
260264
HasLLVMAnn sym =>
@@ -277,7 +281,7 @@ verifyStepBisimulation ::
277281
IO ()
278282
verifyStepBisimulation cruxOpts adapters csettings bbMapRef simctx llvmMod modTrans memVar mem prfbundle =
279283
do let sym = simctx^.ctxSymInterface
280-
putStrLn "Computing step bisimulation verification conditions"
284+
Log.sayCopilot $ Log.ComputingConditions Log.StepBisimulation
281285

282286
frm <- pushAssumptionFrame sym
283287

@@ -303,7 +307,7 @@ verifyStepBisimulation cruxOpts adapters csettings bbMapRef simctx llvmMod modTr
303307

304308
popUntilAssumptionFrame sym frm
305309

306-
putStrLn "Proving step bisimulation verification conditions"
310+
Log.sayCopilot $ Log.ProvingConditions Log.StepBisimulation
307311
proveObls cruxOpts adapters bbMapRef simctx
308312

309313

@@ -875,8 +879,9 @@ from a `PtrRepr` in `computeEqualVals` to handle structs.
875879
proveObls ::
876880
IsSymInterface sym =>
877881
sym ~ ExprBuilder t st fs =>
878-
Logs msgs =>
879-
SupportsCruxLogMessage msgs =>
882+
Log.Logs msgs =>
883+
Log.SupportsCruxLogMessage msgs =>
884+
Log.SupportsCopilotLogMessage msgs =>
880885
CruxOptions ->
881886
[SolverAdapter st] ->
882887
IORef (LLVMAnnMap sym) ->
@@ -899,14 +904,15 @@ summarizeObls _ (Just obls) = map (view labeledPredMsg . proofGoal) (goalsToList
899904
-}
900905

901906
presentResults ::
902-
Logs msgs =>
907+
Log.Logs msgs =>
908+
Log.SupportsCopilotLogMessage msgs =>
903909
IsSymInterface sym =>
904910
sym ->
905911
(ProcessedGoals, Maybe (Goals (Assumptions sym) (Assertion sym, [ProgramLoc], ProofResult sym))) ->
906912
IO ()
907913
presentResults sym (num, goals)
908914
| numTotalGoals == 0
909-
= putStrLn $ "All obligations proved by concrete simplification"
915+
= Log.sayCopilot Log.AllGoalsProved
910916

911917
-- All goals were proven
912918
| numProvedGoals == numTotalGoals
@@ -921,8 +927,32 @@ presentResults sym (num, goals)
921927
numProvedGoals = provedGoals num
922928

923929
printGoals =
924-
do putStrLn $ unwords ["Proved",show numProvedGoals, "of", show numTotalGoals, "total goals"]
930+
do Log.sayCopilot $ Log.OnlySomeGoalsProved numProvedGoals numTotalGoals
925931
goals' <- provedGoalsTree sym goals
926932
case goals' of
927-
Just g -> logGoal g
933+
Just g -> Log.logGoal g
928934
Nothing -> return ()
935+
936+
data CopilotLogging
937+
= LoggingCrux Log.CruxLogMessage
938+
| LoggingCruxLLVM Log.CruxLLVMLogMessage
939+
| LoggingCopilot Log.CopilotLogMessage
940+
deriving stock Generic
941+
deriving anyclass ToJSON
942+
943+
copilotLoggingToSayWhat :: CopilotLogging -> Log.SayWhat
944+
copilotLoggingToSayWhat (LoggingCrux msg) = Log.cruxLogMessageToSayWhat msg
945+
copilotLoggingToSayWhat (LoggingCruxLLVM msg) = Log.cruxLLVMLogMessageToSayWhat msg
946+
copilotLoggingToSayWhat (LoggingCopilot msg) = Log.copilotLogMessageToSayWhat msg
947+
948+
withCopilotLogging ::
949+
( ( Log.SupportsCruxLogMessage CopilotLogging
950+
, Log.SupportsCruxLLVMLogMessage CopilotLogging
951+
, Log.SupportsCopilotLogMessage CopilotLogging
952+
) => computation ) ->
953+
computation
954+
withCopilotLogging computation = do
955+
let ?injectCruxLogMessage = LoggingCrux
956+
?injectCruxLLVMLogMessage = LoggingCruxLLVM
957+
?injectCopilotLogMessage = LoggingCopilot
958+
in computation

‎copilot-verifier/src/Copilot/Verifier/Log.hs‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
{-# LANGUAGE ConstraintKinds #-}
2+
{-# LANGUAGE DeriveAnyClass #-}
3+
{-# LANGUAGE DeriveGeneric #-}
4+
{-# LANGUAGE DerivingStrategies #-}
5+
{-# LANGUAGE ImplicitParams #-}
6+
{-# LANGUAGE OverloadedStrings #-}
7+
module Copilot.Verifier.Log
8+
( SupportsCopilotLogMessage
9+
, CopilotLogMessage(..)
10+
, VerificationStep(..)
11+
, sayCopilot
12+
, copilotLogMessageToSayWhat
13+
) where
14+
15+
import Crux (SayLevel (..), SayWhat (..))
16+
import qualified Crux.Log as Log
17+
import Data.Aeson (ToJSON)
18+
import Data.Text (Text)
19+
import qualified Data.Text as T
20+
import GHC.Generics (Generic)
21+
22+
data CopilotLogMessage
23+
= GeneratedCFile FilePath -- The path of the generated C File
24+
| CompiledBitcodeFile String -- The prefix to use in the compiled bitcode's directory
25+
FilePath -- The name of the generated LLVM bitcode file
26+
| TranslatedToCrucible
27+
| GeneratingProofState
28+
| ComputingConditions VerificationStep
29+
| ProvingConditions VerificationStep
30+
| AllGoalsProved
31+
| OnlySomeGoalsProved Integer -- Number of goals proved
32+
Integer -- Number of total goals
33+
deriving stock Generic
34+
deriving anyclass ToJSON
35+
36+
data VerificationStep
37+
= InitialState
38+
| StepBisimulation
39+
deriving stock Generic
40+
deriving anyclass ToJSON
41+
42+
type SupportsCopilotLogMessage msgs =
43+
(?injectCopilotLogMessage :: CopilotLogMessage -> msgs)
44+
45+
sayCopilot ::
46+
Log.Logs msgs =>
47+
SupportsCopilotLogMessage msgs =>
48+
CopilotLogMessage ->
49+
IO ()
50+
sayCopilot msg =
51+
let ?injectMessage = ?injectCopilotLogMessage
52+
in Log.say msg
53+
54+
copilotTag :: Text
55+
copilotTag = "copilot-verifier"
56+
57+
-- copilotFail :: Text -> SayWhat
58+
-- copilotFail = SayWhat Fail copilotTag
59+
60+
copilotOK :: Text -> SayWhat
61+
copilotOK = SayWhat OK copilotTag
62+
63+
-- copilotWarn :: Text -> SayWhat
64+
-- copilotWarn = SayWhat Warn copilotTag
65+
66+
copilotLogMessageToSayWhat :: CopilotLogMessage -> SayWhat
67+
copilotLogMessageToSayWhat (GeneratedCFile csrc) =
68+
copilotOK $ "Generated " <> T.pack (show csrc)
69+
copilotLogMessageToSayWhat (CompiledBitcodeFile prefix bcFile) =
70+
copilotOK $ "Compiled " <> T.pack prefix <> " into " <> T.pack bcFile
71+
copilotLogMessageToSayWhat TranslatedToCrucible =
72+
copilotOK "Translated bitcode into Crucible"
73+
copilotLogMessageToSayWhat GeneratingProofState =
74+
copilotOK "Generating proof state data"
75+
copilotLogMessageToSayWhat (ComputingConditions step) =
76+
copilotOK $ "Computing " <> describeVerificationStep step <> " verification conditions"
77+
copilotLogMessageToSayWhat (ProvingConditions step) =
78+
copilotOK $ "Proving " <> describeVerificationStep step <> " verification conditions"
79+
copilotLogMessageToSayWhat AllGoalsProved =
80+
copilotOK "All obligations proved by concrete simplification"
81+
copilotLogMessageToSayWhat (OnlySomeGoalsProved numProvedGoals numTotalGoals) =
82+
copilotOK $ T.unwords
83+
[ "Proved", T.pack (show numProvedGoals)
84+
, "of"
85+
, T.pack (show numTotalGoals), "total goals"
86+
]
87+
88+
describeVerificationStep :: VerificationStep -> Text
89+
describeVerificationStep InitialState = "initial state"
90+
describeVerificationStep StepBisimulation = "step bisimulation"

0 commit comments

Comments
 (0)