Cleanup build warnings by removing unused imports, unused variables, etc

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

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

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

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)

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

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
 

src/Pate/Discovery/PLT.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeOperators #-}
 
 module Pate.Discovery.PLT (
     PLTStubInfo(..)

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

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

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
 
 ---------------------------------------------

src/Pate/ExprMappable.hs

@@ -16,8 +16,6 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE LambdaCase #-}
 
--- must come after TypeFamilies, see also https://gitlab.haskell.org/ghc/ghc/issues/18006
-{-# LANGUAGE NoMonoLocalBinds #-}
 {-# OPTIONS_GHC -fno-warn-simplifiable-class-constraints #-}
 
 module Pate.ExprMappable (
@@ -63,7 +61,6 @@ import qualified Lang.Crucible.Utils.MuxTree as MT
 import Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.TraversableF as TF
 import Data.Text
-import Control.Monad (forM)
 
 -- Expression binding
 

src/Pate/Ground.hs

@@ -28,8 +28,6 @@ Grounding symbolic expressions
 {-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE ImplicitParams #-}
 
--- must come after TypeFamilies, see also https://gitlab.haskell.org/ghc/ghc/issues/18006
-{-# LANGUAGE NoMonoLocalBinds #-}
 
 module Pate.Ground 
   ( IsGroundSym

src/Pate/IOReplay.hs

@@ -73,7 +73,7 @@ data IOAction ret = IOActionValue ret =>
   IOAction { ioActionArgs  :: [IOActionArg], ioActionRet :: ret }
 
 data IOActionStore = 
-  IOActionStore { storeQueued :: [T.Text], storeActions :: [Some IOAction], storeDesync :: Bool }
+  IOActionStore { _storeQueued :: [T.Text], _storeActions :: [Some IOAction], _storeDesync :: Bool }
 
 ioActionStore :: MVar IOActionStore
 ioActionStore = unsafePerformIO (newMVar (IOActionStore [] [] False))

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

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

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 ->

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

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

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(..)

src/Pate/Solver.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
 -- | Definitions of solvers usable in the pate verifier
 module Pate.Solver (
     Solver(..)
@@ -26,7 +27,6 @@ import qualified What4.Solver as WS
 
 import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.Backend.Online as CBO
-import Data.Data (Typeable)
 import qualified What4.JSON as W4S
 
 -- | The solvers supported by the pate verifier