Warning Cleanup: unused imports, unused variables, missing cabal modu…

…les, incomplete cases
GaloisInc · Feb 26, 2024 · 6359ed0 · 6359ed0
1 parent 305f43d
commit 6359ed0
Show file tree

Hide file tree

Showing 29 changed files with 70 additions and 141 deletions.
diff --git a/arch/Pate/AArch32.hs b/arch/Pate/AArch32.hs
@@ -13,6 +13,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# OPTIONS_GHC -Wno-unused-imports #-}
 module Pate.AArch32 (
     SA.AArch32
   , AArch32Opts(..)
@@ -326,8 +327,8 @@ stubOverrides =
     r4 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R4")
 
     v0 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_V0")
-    v1 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_V1")
-    v2 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_V2")
+    _v1 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_V1")
+    _v2 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_V2")
     --r3 = ARMReg.ARMGlobalBV (ASL.knownGlobalRef @"_R3")
 
 instance MCS.HasArchTermEndCase MAA.ARMTermStmt where

diff --git a/arch/Pate/PPC.hs b/arch/Pate/PPC.hs
@@ -12,6 +12,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# OPTIONS_GHC -Wno-unused-imports #-}
 
 module Pate.PPC (
     PPC.PPC64

diff --git a/pate.cabal b/pate.cabal
@@ -356,6 +356,7 @@ library pate-repl-base-helper
   build-depends:       template-haskell
   hs-source-dirs:      tools/pate-repl, tools/pate
   exposed-modules:     Repl, ReplHelper
+  other-modules:       Output
   build-depends:       pate-repl-base, pate-base
 
 library pate-base

diff --git a/src/Pate/Arch.hs b/src/Pate/Arch.hs
@@ -74,7 +74,6 @@ import qualified Lang.Crucible.Types as LCT
 import qualified Lang.Crucible.LLVM.MemModel as CLM
 
 import qualified Pate.AssumptionSet as PAS
-import qualified Pate.Address as PAd
 import qualified Pate.Binary as PB
 import qualified Pate.Block as PB
 import qualified Pate.Memory.MemTrace as PMT
@@ -94,10 +93,7 @@ import qualified What4.JSON as W4S
 
 import Pate.Config (PatchData)
 import Data.Macaw.AbsDomain.AbsState (AbsBlockState)
-import Pate.Address (ConcreteAddress)
 import qualified Data.ElfEdit as EEP
-import qualified Data.Parameterized.List as P
-import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.TraversableFC as TFC
 import qualified Data.Aeson as JSON
 import           Data.Aeson ( (.=) )
@@ -371,7 +367,6 @@ mkWriteOverride ::
   MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ return register -} ->
   StubOverride arch
 mkWriteOverride nm fd_reg buf_reg flen rOut = StubOverride $ \sym wsolver -> do
-  let w_mem = MC.memWidthNatRepr @(MC.ArchAddrWidth arch)
   -- TODO: must be less than len
   zero_nat <- W4.natLit sym 0
   let w_mem = MC.memWidthNatRepr @(MC.ArchAddrWidth arch)

diff --git a/src/Pate/CLI.hs b/src/Pate/CLI.hs
@@ -29,7 +29,6 @@ import qualified Data.Macaw.CFG as MC
 import qualified Pate.Arch as PA
 import qualified Pate.Block as PB
 import qualified Pate.Config as PC
-import qualified Pate.Equivalence as PEq
 import qualified Pate.Equivalence.Error as PEE
 import qualified Pate.Event as PE
 import qualified Pate.Loader as PL
@@ -38,7 +37,6 @@ 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

diff --git a/src/Pate/Discovery.hs b/src/Pate/Discovery.hs
@@ -36,7 +36,6 @@ module Pate.Discovery (
 
 import           Control.Lens ( (^.) )
 import           Control.Monad (forM,filterM)
-import           Control.Monad.Fail (fail)
 import           Control.Monad.Trans (lift)
 import qualified Control.Monad.Catch as CMC
 import qualified Control.Monad.Except as CME
@@ -79,7 +78,6 @@ import qualified Data.Macaw.Types as MT
 import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.LLVM.MemModel as CLM
 import qualified Lang.Crucible.Simulator as CS
-import qualified Lang.Crucible.Simulator.RegValue as CS
 
 import qualified Lang.Crucible.Types as CT
 import qualified What4.Interface as WI
@@ -112,12 +110,9 @@ import qualified What4.ExprHelpers as WEH
 
 import           Pate.TraceTree
 import qualified Control.Monad.IO.Unlift as IO
-import Data.Parameterized.SetF (AsOrd(..))
 import qualified Data.ByteString.Char8 as BSC
-import qualified Data.Macaw.Architecture.Info as MAI
 import Control.Applicative
 import qualified Data.Vector as V
-import qualified Data.Macaw.Discovery.ParsedContents as Parsed
 
 --------------------------------------------------------
 -- Block pair matching
@@ -203,11 +198,11 @@ discoverPairs bundle = withTracing @"debug" "discoverPairs" $ withSym $ \sym ->
 --   with a potential null jump target is a return
 --   Formally this is extremely unsound - but we need to track more symbolic
 --   information in order to resolve this when macaw fails
-relaxedReturnCondition ::
+_relaxedReturnCondition ::
   forall sym arch v.
   SimBundle sym arch v ->
   EquivM sym arch (WI.Pred sym)
-relaxedReturnCondition bundle = withSym $ \sym -> PPa.joinPatchPred (\x y -> liftIO $ WI.andPred sym x y) $ \bin -> do
+_relaxedReturnCondition bundle = withSym $ \sym -> PPa.joinPatchPred (\x y -> liftIO $ WI.andPred sym x y) $ \bin -> do
   out <- PPa.get bin (PSS.simOut bundle)
   let blkend = PSS.simOutBlockEnd out
   is_return <- liftIO $ MCS.isBlockEndCase (Proxy @arch) sym blkend MCS.MacawBlockEndReturn
@@ -267,11 +262,11 @@ isMatchingCall bundle = withSym $ \sym -> do
 
 -- | True for a pair of original and patched block targets that represent a valid pair of
 -- jumps
-compatibleTargets ::
+_compatibleTargets ::
   PB.BlockTarget arch PB.Original ->
   PB.BlockTarget arch PB.Patched ->
   Bool
-compatibleTargets blkt1 blkt2 = (PB.targetEndCase blkt1 == PB.targetEndCase blkt2) &&
+_compatibleTargets blkt1 blkt2 = (PB.targetEndCase blkt1 == PB.targetEndCase blkt2) &&
   PB.concreteBlockEntry (PB.targetCall blkt1) == PB.concreteBlockEntry (PB.targetCall blkt2) &&
   case (PB.targetReturn blkt1, PB.targetReturn blkt2) of
     (Just blk1, Just blk2) -> PB.concreteBlockEntry blk1 == PB.concreteBlockEntry blk2
@@ -671,12 +666,12 @@ findPLTSymbol blk = fnTrace "findPLTSymbol" $ do
     [sym] -> return (Just sym)
     _ -> return Nothing
 
-isPLTTarget ::
+_isPLTTarget ::
   forall bin sym arch.
   PB.KnownBinary bin =>
   PB.BlockTarget arch bin ->
   EquivM sym arch Bool  
-isPLTTarget bt = case PB.asFunctionEntry (PB.targetCall bt) of
+_isPLTTarget bt = case PB.asFunctionEntry (PB.targetCall bt) of
   Just fe -> isPLTFunction fe
   Nothing -> return False
 

diff --git a/src/Pate/Discovery/ParsedFunctions.hs b/src/Pate/Discovery/ParsedFunctions.hs
@@ -38,10 +38,9 @@ import qualified Data.Foldable as F
 import qualified Data.IORef as IORef
 import qualified Data.Map as Map
 import qualified Data.Map.Merge.Strict as Map
-import           Data.Maybe ( mapMaybe, listToMaybe )
-import qualified Data.Parameterized.Classes as PC
+import           Data.Maybe ( mapMaybe )
 import qualified Data.Parameterized.Map as MapF
-import           Data.Parameterized.Some ( Some(..), viewSome )
+import           Data.Parameterized.Some ( Some(..) )
 import qualified Data.Set as Set
 import qualified Prettyprinter as PP
 import qualified Prettyprinter.Render.Text as PPT
@@ -67,9 +66,7 @@ import           Pate.Discovery.PLT (extraJumpClassifier, extraReturnClassifier,
 
 import           Pate.TraceTree
 import Control.Monad.IO.Class (liftIO)
-import Control.Monad (forM)
 
-import Debug.Trace
 import Control.Applicative ((<|>))
 import Data.Macaw.Utils.IncComp (incCompResult)
 import qualified Data.Text as T
@@ -482,7 +479,7 @@ parsedFunctionContaining ::
   PB.ConcreteBlock arch bin ->
   ParsedFunctionMap arch bin ->
   IO (Maybe (Some (MD.DiscoveryFunInfo arch)))
-parsedFunctionContaining blk pfm@(ParsedFunctionMap pfmRef mCFGDir _pd _ _ _ _ _ _) = do
+parsedFunctionContaining blk pfm@(ParsedFunctionMap _pfmRef mCFGDir _pd _ _ _ _ _ _) = do
   let faddr = PB.functionSegAddr (PB.blockFunctionEntry blk)
 
   st <- getParsedFunctionState faddr pfm

diff --git a/src/Pate/Equivalence/Condition.hs b/src/Pate/Equivalence/Condition.hs
@@ -43,7 +43,6 @@ import qualified What4.Interface as W4
 import qualified Prettyprinter as PP
 
 import qualified Data.Macaw.CFG as MM
-import qualified Data.Aeson as JSON
 
 import qualified Pate.Arch as PA
 import qualified Pate.AssumptionSet as PAS

diff --git a/src/Pate/Equivalence/RegisterDomain.hs b/src/Pate/Equivalence/RegisterDomain.hs
@@ -50,7 +50,6 @@ import qualified Prettyprinter as PP
 import qualified Pate.Location as PL
 import qualified Pate.Solver as PS
 import qualified Pate.ExprMappable as PEM
-import           Pate.TraceTree
 import qualified What4.JSON as W4S
 
 ---------------------------------------------

diff --git a/src/Pate/Loader.hs b/src/Pate/Loader.hs
@@ -43,7 +43,6 @@ import qualified Pate.Verification as PV
 import qualified Pate.Equivalence.Error as PEE
 import qualified Control.Monad.Reader as CMR
 import           Pate.TraceTree
-import qualified Data.IORef as IO
 
 data RunConfig =
   RunConfig

diff --git a/src/Pate/Loader/ELF.hs b/src/Pate/Loader/ELF.hs
@@ -51,11 +51,8 @@ import qualified Pate.Hints.JSON as PHJ
 import qualified Pate.Hints.BSI as PHB
 import Data.Macaw.Memory.Permissions as MP (execute,read)
 
-import Data.Bits ((.|.), Bits ((.&.)))
+import Data.Bits ((.|.))
 import qualified Control.Monad.Reader as CMR
-import qualified System.IO as IO
-import qualified System.Directory as IO
-import qualified System.Exit as SE
 
 data LoadedELF arch =
   LoadedELF

diff --git a/src/Pate/Monad.hs b/src/Pate/Monad.hs
@@ -111,14 +111,12 @@ import           GHC.Stack ( HasCallStack, callStack )
 
 import           Control.Lens ( (&), (.~) )
 import qualified Control.Monad.Fail as MF
-import           Control.Monad (void)
-import           Control.Monad.IO.Class (liftIO)
 import qualified Control.Monad.IO.Unlift as IO
 import qualified Control.Concurrent as IO
 import           Control.Exception hiding ( try, finally, catch, mask )
 import           Control.Monad.Catch hiding ( catches, tryJust, Handler )
 import qualified Control.Monad.Reader as CMR
-import           Control.Monad.Reader ( asks, ask )
+import           Control.Monad.Reader ( asks )
 import           Control.Monad.Except
 
 import           Data.Maybe ( fromMaybe )
@@ -158,7 +156,6 @@ import qualified Data.Macaw.BinaryLoader as MBL
 
 import qualified What4.Expr as WE
 import qualified What4.Expr.GroundEval as W4G
-import qualified What4.Expr.Builder as W4B
 import qualified What4.Interface as W4
 import qualified What4.SatResult as W4R
 import qualified What4.Symbol as WS
@@ -194,9 +191,6 @@ import qualified Pate.Timeout as PT
 import qualified Pate.Verification.Concretize as PVC
 import           Pate.TraceTree
 import Data.Functor.Const (Const(..))
-import Unsafe.Coerce (unsafeCoerce)
-import Debug.Trace
-import Data.List
 
 atPriority :: 
   NodePriority ->

diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs
@@ -75,20 +75,17 @@ module Pate.PatchPair (
 
 import           Prelude hiding (zip)
 import           GHC.Stack (HasCallStack)
-import           Control.Monad.Trans (lift)
 import           Control.Monad.Trans.Maybe
 import           Control.Monad.Except
 import           Control.Monad.Catch
 import qualified Control.Monad.Trans as CMT
-import           Control.Monad.IO.Class (MonadIO)
 
 import           Data.Functor.Const ( Const(..) )
 import qualified Data.Kind as DK
 import           Data.Parameterized.Classes
 import qualified Data.Parameterized.TraversableF as TF
 import qualified Prettyprinter as PP
 import qualified Data.Aeson as JSON
-import qualified Compat.Aeson as JSON
 
 import qualified Pate.Binary as PB
 import qualified Pate.ExprMappable as PEM

diff --git a/src/Pate/Register.hs b/src/Pate/Register.hs
@@ -23,7 +23,6 @@ import qualified Lang.Crucible.CFG.Core as CC
 import qualified Lang.Crucible.LLVM.MemModel as CLM
 
 import qualified Pate.Arch as PA
-import qualified Pate.ExprMappable as PEM
 
 -- | Helper for doing a case-analysis on registers
 data RegisterCase arch tp where

diff --git a/src/Pate/SimState.hs b/src/Pate/SimState.hs
@@ -36,7 +36,7 @@ Functionality for handling the inputs and outputs of crucible.
 module Pate.SimState
   ( -- simulator state
     SimState(..)
-  , StackBase(..)
+  , StackBase
   , freshStackBase
   , SimInput(..)
   , SimOutput(..)

diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs
@@ -115,29 +115,26 @@ module Pate.TraceTree (
 
 import           GHC.TypeLits ( Symbol, KnownSymbol )
 import           Data.Kind ( Type )
-import           Control.Monad.IO.Class (MonadIO, liftIO)
 import qualified Control.Monad.IO.Class as IO
 import qualified Control.Monad.IO.Unlift as IO
 import qualified Data.IORef as IO
 import           Data.String
 import qualified Data.Map as Map
 import           Data.Map ( Map )
 import           Data.Default
-import           Data.List ((!!), find, isPrefixOf)
-import           Control.Monad.Trans (lift)
+import           Data.List (isPrefixOf)
 import           Control.Monad.Trans.Maybe
 import qualified Control.Monad.Reader as CMR
 import qualified Control.Monad.Trans as CMT
 import           Control.Monad.Except
 import           Control.Monad.Catch
-import           Control.Monad (void, unless, forM) -- GHC 9.6
+ -- GHC 9.6
 import           Control.Applicative
 
 import qualified Prettyprinter as PP
 import qualified Prettyprinter.Render.String as PP
 
 import qualified Data.Aeson as JSON
-import qualified Compat.Aeson as JSON
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
 import           Data.Parameterized.SymbolRepr ( knownSymbol, symbolRepr, SomeSym(..), SymbolRepr )
@@ -148,7 +145,6 @@ import qualified Data.Set as Set
 import Data.Set (Set)
 import GHC.IO (unsafePerformIO)
 import qualified Control.Concurrent as IO
-import qualified System.IO as IO
 import Data.Maybe (catMaybes)
 import Control.Concurrent (threadDelay)
 import Control.Monad.State.Strict (StateT (..), MonadState (..))

diff --git a/src/Pate/Verification.hs b/src/Pate/Verification.hs
@@ -74,7 +74,6 @@ import qualified Pate.Equivalence.Error as PEE
 import qualified Pate.Event as PE
 import qualified Pate.Hints as PH
 import qualified Pate.Loader.ELF as PLE
-import qualified Pate.Location as PL
 import qualified Pate.Memory as PM
 import qualified Pate.Memory.MemTrace as MT
 import           Pate.Monad

diff --git a/src/Pate/Verification/ConditionalEquiv.hs b/src/Pate/Verification/ConditionalEquiv.hs
@@ -37,7 +37,6 @@ import qualified What4.Interface as W4
 
 import qualified Pate.AssumptionSet as PAS
 import qualified Pate.Config as PC
-import qualified Pate.SimState as PS
 import qualified Pate.Verification.Simplify as PSi
 import           Pate.Monad
 
@@ -112,8 +111,6 @@ computeEqCondition eqPred vals = withTracing @"function_name" "computeEqConditio
         -- counter-example, compute another path condition and continue
         W4R.Sat fn_ -> Just <$> do
           fn <- wrapGroundEvalFn fn_ (S.singleton (Some eqPred))
-          vars <- (S.toList . S.unions) <$> mapM (\(Some e') -> liftIO $ WEH.boundVars e') (S.toList vals)
-          let varsE = map (\(Some v) -> Some (W4.varExpr sym v)) vars
 
           binds <- extractBindings fn vals
           subTree @"expr" "Bindings" $ do

diff --git a/src/Pate/Verification/DemandDiscovery.hs b/src/Pate/Verification/DemandDiscovery.hs
@@ -128,6 +128,7 @@ concreteBlockFromBVAddr _proxy binRepr mem bv =
                                 , PB.functionSymbol = Nothing
                                 , PB.functionBinRepr = binRepr
                                 , PB.functionIgnored = False
+                                , PB.functionEnd = Nothing
                                 }
       return PB.ConcreteBlock { PB.concreteAddress = addr
                               , PB.concreteBlockEntry = PB.BlockEntryInitFunction