Delete dead code2

pate.cabal

@@ -138,7 +138,6 @@ library
                        Pate.Hints.JSON,
                        Pate.Hints.DWARF,
                        Pate.IOReplay,
-                       Pate.JSONReport,
                        Pate.Location,
                        Pate.Monad,
                        Pate.Monad.Context,

src/Pate/CLI.hs

@@ -43,7 +43,6 @@ import qualified Pate.Timeout as PTi
 import qualified Pate.Verbosity as PV
 import qualified Pate.Verification.StrongestPosts.CounterExample as PVSC
 
-import qualified Pate.JSONReport as JR
 import           Pate.TraceTree
 import Data.Maybe (fromMaybe)
 
@@ -65,18 +64,7 @@ mkRunConfig archLoader opts rcfg mtt = let
       }
 
     mklogger :: forall arch. PA.SomeValidArch arch -> IO (PL.Logger arch)
-    mklogger proxy = do
-        (logger, consumers) <- startLogger proxy (verbosity opts) (logFile opts)
-        case proofSummaryJSON opts of
-          Nothing -> return $ PL.Logger logger consumers
-          Just proofJSONFile -> do
-            pc <- JR.consumeProofEvents proofJSONFile
-            let recordProofEvent evt =
-                  case evt of
-                    PE.ProofIntermediate bp sp _ -> JR.sendEvent pc (Just (JR.SomeProofEvent bp sp))
-                    _ -> return ()
-            let jl = LJ.LogAction recordProofEvent
-            return $ PL.Logger (logger <> jl) ((JR.waitForConsumer pc, JR.sendEvent pc Nothing) : consumers)
+    mklogger proxy = error "replace this function"
 
     verificationCfg =
       PC.defaultVerificationCfg
@@ -240,30 +228,8 @@ terminalFormatEvent evt =
                        , PP.viaShow $ PB.concreteAddress blkP
                        , PP.line
                        ]
-    PE.CheckedEquivalence (PPa.PatchPair (PE.Blocks _ blkO _) (PE.Blocks _ blkP _)) res duration ->
-      let
-        origAddr = PB.concreteAddress blkO
-        patchedAddr = PB.concreteAddress blkP
-        pfx = mconcat [ "Checked original block at "
-                      , PP.viaShow origAddr
-                      , " against patched block at "
-                      , PP.viaShow patchedAddr
-                      , " "
-                      , PP.parens (PP.viaShow duration)
-                      ]
-      in case res of
-        PE.Equivalent ->
-          let okStyle = PPRT.color PPRT.Green <> PPRT.bold
-          in layoutLn (pfx <> " " <> PP.brackets (PP.annotate okStyle "✓"))
-        PE.Inconclusive ->
-          let qStyle = PPRT.color PPRT.Magenta <> PPRT.bold
-          in layoutLn (pfx <> " " <> PP.brackets (PP.annotate qStyle "?"))
-        PE.Inequivalent _mdl ->
-          let failStyle = PPRT.color PPRT.Red <> PPRT.bold
-          in layoutLn (pfx <> " " <> PP.brackets (PP.annotate failStyle "✗"))
     PE.ErrorRaised err -> layoutLn ("ERROR:" <> PP.pretty err)
     PE.Warning err -> layoutLn ("WARNING:" <> PP.pretty err)
-    PE.ProvenGoal _ prf _ -> layoutLn (PP.viaShow prf)
     PE.HintErrorsCSV errs -> layoutLn (PP.vsep (map PP.viaShow (F.toList errs)))
     PE.HintErrorsJSON errs -> layoutLn (PP.vsep (map PP.viaShow (F.toList errs)))
     PE.HintErrorsDWARF errs -> layoutLn (PP.vsep (map PP.viaShow (F.toList errs)))

src/Pate/Event.hs

@@ -10,9 +10,7 @@
 module Pate.Event (
   Blocks(..),
   BlocksPair,
-  EquivalenceResult(..),
   BlockTargetResult(..),
-  BranchCompletenessResult(..),
   Event(..),
   SolverResultKind(..),
   SolverProofKind(..)
@@ -40,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 as PF
 import qualified Pate.Proof.Instances as PFI
 import qualified Pate.SimState as PS
 import qualified Pate.PatchPair as PPa
@@ -59,10 +56,6 @@ data Blocks arch bin where
 
 type BlocksPair arch = PPa.PatchPair (Blocks arch)
 
-data EquivalenceResult arch = Equivalent
-                            | Inconclusive
-                            | Inequivalent (PF.InequivalenceResult arch)
-
 data BlockTargetResult = Reachable
                        | InconclusiveTarget
                        | Unreachable
@@ -72,10 +65,6 @@ instance IsTraceNode k "blocktargetresult" where
   type TraceNodeType k "blocktargetresult" = BlockTargetResult
   prettyNode () result = PP.pretty (show result)
 
-data BranchCompletenessResult arch = BranchesComplete
-                                   | InconclusiveBranches
-                                   | BranchesIncomplete (PF.InequivalenceResult arch)
-
 
 -- | Events that can be reported from the verifier
 --
@@ -87,16 +76,9 @@ data Event arch where
   ErrorRaised :: PEE.EquivalenceError -> Event arch
   Warning :: PEE.EquivalenceError -> Event arch
   -- | final top-level result
-  ProvenGoal :: BlocksPair arch ->  PFI.SomeProofNonceExpr arch PF.ProofBlockSliceType -> TM.NominalDiffTime -> Event arch
-  -- | intermediate results
-  ProofIntermediate :: BlocksPair arch -> PFI.SomeProofNonceExpr arch tp -> TM.NominalDiffTime -> Event arch
-  ProofStarted :: BlocksPair arch -> PFI.SomeProofNonceExpr arch tp -> TM.NominalDiffTime -> Event arch
-
-  CheckedBranchCompleteness :: BlocksPair arch -> BranchCompletenessResult arch -> TM.NominalDiffTime -> Event arch
   DiscoverBlockPair :: BlocksPair arch -> PPa.PatchPair (PB.BlockTarget arch) -> BlockTargetResult -> TM.NominalDiffTime -> Event arch
   ComputedPrecondition :: BlocksPair arch -> TM.NominalDiffTime -> Event arch
   ElfLoaderWarnings :: [DEE.ElfParseError] -> Event arch
-  CheckedEquivalence :: BlocksPair arch -> EquivalenceResult arch -> TM.NominalDiffTime -> Event arch
   LoadedBinaries :: PLE.LoadedELF arch -> PLE.LoadedELF arch -> Event arch
   -- | Function/block start hints that point to unmapped addresses
   FunctionEntryInvalidHints :: PB.WhichBinaryRepr bin -> [(T.Text, Word64)] -> Event arch

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 as PPr
 import qualified Pate.Proof.Instances as PFI
 
 data BinaryMetrics =
@@ -71,20 +70,12 @@ summarize e m =
       m { originalBinaryMetrics = Just (loadedBinaryMetrics origElf)
         , patchedBinaryMetrics = Just (loadedBinaryMetrics patchedElf)
         }
-    PE.ProofIntermediate _bp (PFI.SomeProofNonceExpr _sym nonceExpr) _tm ->
-      case PPr.prfNonceBody nonceExpr of
-        PPr.ProofTriple {} -> m { verifiedGoals = verifiedGoals m + 1 }
-        _ -> m
     -- The following cases don't contribute to the aggregate metrics
-    PE.CheckedEquivalence {} -> m
     PE.ComputedPrecondition {} -> m
     PE.ElfLoaderWarnings {} -> m
     PE.AnalysisStart {} -> m
     PE.ErrorRaised {} -> m
     PE.Warning {} -> m
-    PE.CheckedBranchCompleteness {} -> m
-    PE.ProvenGoal {} -> m
-    PE.ProofStarted {} -> m
     PE.DiscoverBlockPair {} -> m
     PE.HintErrorsCSV {} -> m
     PE.HintErrorsJSON {} -> m

src/Pate/Monad.hs

@@ -275,19 +275,13 @@ ifConfig checkCfg ifT ifF = (CMR.asks $ checkCfg . envConfig) >>= \case
   False -> ifF
 
 freshNonce :: EquivM sym arch (N.Nonce (PF.SymScope sym) tp)
-freshNonce = do
-  gen <- CMR.asks envNonceGenerator
-  liftIO $ N.freshNonce gen
+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 = withValid $ do
-  nonce <- freshNonce
-  let proofNonce = PF.ProofNonce nonce
-  CMR.local (\env -> env { envParentNonce = Some proofNonce }) (f proofNonce)
-
+withProofNonce f = error "replace this function"
 
 -- | Start the timer to be used as the initial time when computing
 -- the duration in a nested 'emitEvent'