Merge pull request #468 from GaloisInc/deleteDeadCode2

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,
@@ -152,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,14 +37,12 @@ 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
 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)
 
@@ -66,17 +65,8 @@ 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)
+      (logger, consumers) <- startLogger proxy (verbosity opts) (logFile opts)
+      return $ PL.Logger logger consumers
 
     verificationCfg =
       PC.defaultVerificationCfg
@@ -240,30 +230,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)))
@@ -298,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

@@ -10,9 +10,7 @@
 module Pate.Event (
   Blocks(..),
   BlocksPair,
-  EquivalenceResult(..),
   BlockTargetResult(..),
-  BranchCompletenessResult(..),
   Event(..),
   SolverResultKind(..),
   SolverProofKind(..)
@@ -40,8 +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
 import qualified Pate.Equivalence as PE
@@ -59,10 +55,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 +64,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 +75,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,8 +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 =
   BinaryMetrics { executableBytes :: !Int
@@ -71,20 +69,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