remove deprecated Pate.Proof modules

pate.cabal

@@ -151,10 +151,6 @@ library
                        Pate.Panic,
                        Pate.Parallel,
                        Pate.Pointer,
-                       Pate.Proof,
-                       Pate.Proof.Instances,
-                       Pate.Proof.Operations,
-                       Pate.Proof.CounterExample,
                        Pate.Register,
                        Pate.Register.Traversal,
                        Pate.Solver,

src/Data/Macaw/CFGSlice.hs

@@ -34,6 +34,7 @@ module Data.Macaw.CFGSlice
   , termStmtToBlockEnd
   , blockEndSliceFns
   , copyBlockEnd
+  , ppExitCase
   ) where
 
 import qualified GHC.Generics as G
@@ -83,6 +84,15 @@ data MacawBlockEndCase =
   | MacawBlockEndArch
   deriving (Eq, Enum, Bounded, Ord, Show, G.Generic)
 
+ppExitCase :: MacawBlockEndCase -> String
+ppExitCase ec = case ec of
+  MacawBlockEndJump -> "arbitrary jump"
+  MacawBlockEndCall -> "function call"
+  MacawBlockEndReturn -> "function return"
+  MacawBlockEndBranch -> "branch"
+  MacawBlockEndArch -> "arch-specific"
+  MacawBlockEndFail -> "analysis failure"
+
 instance JSON.ToJSON MacawBlockEndCase
 
 class HasArchTermEndCase (f :: (M.Type -> Kind.Type) -> Kind.Type) where

src/Pate/CLI.hs

@@ -25,6 +25,7 @@ import qualified System.IO as IO
 import qualified What4.Interface as WI
 
 import qualified Data.Macaw.CFG as MC
+import qualified Data.Macaw.CFGSlice as MCS
 
 import qualified Pate.Arch as PA
 import qualified Pate.Block as PB
@@ -36,7 +37,6 @@ import qualified Pate.Loader as PL
 import qualified Pate.Loader.ELF as PLE
 import qualified Pate.Memory.MemTrace as PMT
 import qualified Pate.PatchPair as PPa
-import qualified Pate.Proof.Instances as PPI
 import qualified Pate.Solver as PS
 import qualified Pate.Script as PSc
 import qualified Pate.Timeout as PTi
@@ -64,7 +64,9 @@ mkRunConfig archLoader opts rcfg mtt = let
       }
 
     mklogger :: forall arch. PA.SomeValidArch arch -> IO (PL.Logger arch)
-    mklogger proxy = error "replace this function"
+    mklogger proxy = do
+      (logger, consumers) <- startLogger proxy (verbosity opts) (logFile opts)
+      return $ PL.Logger logger consumers
 
     verificationCfg =
       PC.defaultVerificationCfg
@@ -264,8 +266,8 @@ terminalFormatEvent evt =
                        ) <> PP.line)
     PE.StrongestPostDesync pPair (PVSC.TotalityCounterexample (oIP, oEnd, oInstr) (pIP, pEnd, pInstr)) ->
       layout ( PP.vcat [ PP.pretty pPair PP.<+> "program control flow desynchronized"
-                       , "  Original: 0x" <> PP.pretty (showHex oIP "") PP.<+> PP.pretty (PPI.ppExitCase oEnd) PP.<+> PP.viaShow oInstr
-                       , "  Patched : 0x" <> PP.pretty (showHex pIP "") PP.<+> PP.pretty (PPI.ppExitCase pEnd) PP.<+> PP.viaShow pInstr
+                       , "  Original: 0x" <> PP.pretty (showHex oIP "") PP.<+> PP.pretty (MCS.ppExitCase oEnd) PP.<+> PP.viaShow oInstr
+                       , "  Patched : 0x" <> PP.pretty (showHex pIP "") PP.<+> PP.pretty (MCS.ppExitCase pEnd) PP.<+> PP.viaShow pInstr
                        ] <> PP.line)
     -- FIXME: handle other events
     _ -> layout ""

src/Pate/Event.hs

@@ -38,7 +38,6 @@ import qualified Pate.Hints.CSV as PHC
 import qualified Pate.Hints.DWARF as PHD
 import qualified Pate.Hints.JSON as PHJ
 import qualified Pate.Hints.BSI as PHB
-import qualified Pate.Proof.Instances as PFI
 import qualified Pate.SimState as PS
 import qualified Pate.PatchPair as PPa
 import qualified Pate.Equivalence as PE

src/Pate/Metrics.hs

@@ -15,7 +15,6 @@ import qualified Data.Time as TM
 
 import qualified Pate.Event as PE
 import qualified Pate.Loader.ELF as PLE
-import qualified Pate.Proof.Instances as PFI
 
 data BinaryMetrics =
   BinaryMetrics { executableBytes :: !Int

src/Pate/Monad.hs

@@ -83,9 +83,6 @@ module Pate.Monad
   , applyCurrentAsms
   , applyCurrentAsmsExpr
   , currentAsm
-  -- nonces
-  , freshNonce
-  , withProofNonce
   -- caching
   , lookupBlockCache
   , modifyBlockCache
@@ -195,7 +192,6 @@ import           Pate.Monad.Environment as PME
 import           Pate.Panic
 import qualified Pate.Parallel as Par
 import qualified Pate.PatchPair as PPa
-import qualified Pate.Proof as PF
 import           Pate.SimState
 import qualified Pate.SimulatorRegisters as PSR
 import qualified Pate.Solver as PSo
@@ -274,15 +270,6 @@ ifConfig checkCfg ifT ifF = (CMR.asks $ checkCfg . envConfig) >>= \case
   True -> ifT
   False -> ifF
 
-freshNonce :: EquivM sym arch (N.Nonce (PF.SymScope sym) tp)
-freshNonce = error "replace this function"
-
-withProofNonce ::
-  forall tp sym arch a.
-  (PF.ProofNonce sym tp -> EquivM sym arch a) ->
-  EquivM sym arch a
-withProofNonce f = error "replace this function"
-
 -- | Start the timer to be used as the initial time when computing
 -- the duration in a nested 'emitEvent'
 startTimer :: EquivM sym arch a -> EquivM sym arch a

src/Pate/Monad/Environment.hs

@@ -67,7 +67,6 @@ import qualified Pate.Memory.MemTrace as MT
 import qualified Pate.Monad.Context as PMC
 import qualified Pate.PatchPair as PPa
 import qualified Pate.Location as PL
-import qualified Pate.Proof as PF
 import qualified Pate.Solver as PSo
 import qualified Pate.SymbolTable as PSym
 import qualified Pate.Verification.Override as PVO
@@ -99,9 +98,6 @@ data EquivEnv sym arch where
     -- ^ the current assumption frame, accumulated as assumptions are added
     , envPathCondition :: PAS.AssumptionSet sym
     -- ^ assumptions specific to a particular path (subsumed by envCurrentFrame)
-    , envNonceGenerator :: N.NonceGenerator IO (PF.SymScope sym)
-    , envParentNonce :: Some (PF.ProofNonce sym)
-    -- ^ nonce of the parent proof node currently in scope
     , envUndefPointerOps :: MT.UndefinedPtrOps sym
     , envParentBlocks :: [PB.BlockPair arch]
     -- ^ all block pairs on this path from the toplevel