diff --git a/arch/Pate/AArch32.hs b/arch/Pate/AArch32.hs index 4770029c..7f1fae62 100644 --- 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 index d390b0fd..c3e327a6 100644 --- 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 index 62040e16..be3476bb 100644 --- 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 index 6d242d8a..0514bb3e 100644 --- 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/Discovery.hs b/src/Pate/Discovery.hs index fb76a3d8..541faebd 100644 --- 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 @@ -214,11 +209,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 @@ -278,11 +273,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 @@ -682,12 +677,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 index 7d74e4bc..1410be45 100644 --- 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/RegisterDomain.hs b/src/Pate/Equivalence/RegisterDomain.hs index 69bbf12d..79844e43 100644 --- 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/ELF.hs b/src/Pate/Loader/ELF.hs index 432ccd06..c78a4e47 100644 --- 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 index ba2f677e..9db83c71 100644 --- 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/SimState.hs b/src/Pate/SimState.hs index e578c4ad..7cd2db36 100644 --- 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 index 6a0f0598..6a7f57a2 100644 --- a/src/Pate/TraceTree.hs +++ b/src/Pate/TraceTree.hs @@ -115,7 +115,6 @@ 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 @@ -123,21 +122,19 @@ 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) diff --git a/src/Pate/Verification.hs b/src/Pate/Verification.hs index 3dedaee0..d00fac96 100644 --- 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 index 49523f9f..fbde76b6 100644 --- 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 index 5cc6a692..e396c4f7 100644 --- 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 diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index f105ca29..0438defa 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -154,14 +154,12 @@ import qualified Pate.Verification.AbstractDomain as PAD import Pate.Verification.AbstractDomain ( AbstractDomain, AbstractDomainSpec ) import Pate.TraceTree import qualified Pate.Binary as PBi -import Data.Parameterized (Some(..), Pair (..)) +import Data.Parameterized (Some(..)) import Control.Applicative (Const(..)) import qualified Control.Monad.IO.Unlift as IO -import Pate.Solver (ValidSym) import Control.Monad.Reader (local, MonadReader (ask)) import SemMC.Formula.Env (SomeSome(..)) import qualified Pate.Location as PL -import qualified Pate.ExprMappable as PEM -- | Gas is used to ensure that our fixpoint computation terminates -- in a reasonable amount of time. Gas is expended each time @@ -539,11 +537,11 @@ dropPostDomains :: PairGraph sym arch dropPostDomains nd priority pg = dropObservableReports nd $ Set.foldl' (\pg_ nd' -> dropDomain nd' priority pg_) pg (getEdgesFrom pg nd) -dropDomainRefinement :: +_dropDomainRefinement :: GraphNode arch -> PairGraph sym arch -> PairGraph sym arch -dropDomainRefinement nd pg = pg { pairGraphDomainRefinements = Map.delete nd (pairGraphDomainRefinements pg)} +_dropDomainRefinement nd pg = pg { pairGraphDomainRefinements = Map.delete nd (pairGraphDomainRefinements pg)} -- | Delete the abstract domain for the given node, following -- any reachable edges and discarding those domains as well @@ -941,8 +939,8 @@ updateSyncPoint :: (SyncPoint arch -> SyncPoint arch) -> PairGraph sym arch updateSyncPoint pg nd f = case getDivergePoint nd of - Just divergePoint | Just sync <- asSyncPoint pg nd -> - pg { pairGraphSyncPoints = Map.insert divergePoint (f sync) (pairGraphSyncPoints pg)} + Just dp | Just sync <- asSyncPoint pg nd -> + pg { pairGraphSyncPoints = Map.insert dp (f sync) (pairGraphSyncPoints pg)} _ -> pg asSyncPoint :: diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index b69b2726..72f376ac 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/src/Pate/Verification/PairGraph/Node.hs @@ -46,7 +46,6 @@ module Pate.Verification.PairGraph.Node ( import Prettyprinter ( Pretty(..), sep, (<+>), Doc ) import qualified Data.Aeson as JSON -import qualified Compat.Aeson as HMS import qualified Data.Parameterized.TraversableF as TF import qualified Pate.Arch as PA diff --git a/src/Pate/Verification/Simplify.hs b/src/Pate/Verification/Simplify.hs index 313a209f..069650b5 100644 --- a/src/Pate/Verification/Simplify.hs +++ b/src/Pate/Verification/Simplify.hs @@ -147,8 +147,8 @@ tracedSimpCheck = WEH.SimpCheck $ \e_orig e_simp -> withValid $ withSym $ \sym - emitError $ PEE.InconsistentSimplificationResult (PEE.SimpResult (Proxy @sym) e_orig e_simp) return e_orig -getSimpCheck :: EquivM sym arch (WEH.SimpCheck sym (EquivM_ sym arch)) -getSimpCheck = do +_getSimpCheck :: EquivM sym arch (WEH.SimpCheck sym (EquivM_ sym arch)) +_getSimpCheck = do shouldCheck <- CMR.asks (PC.cfgCheckSimplifier . envConfig) case shouldCheck of True -> return tracedSimpCheck diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 3b414cf8..a179d86c 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -27,7 +27,7 @@ import GHC.Stack ( HasCallStack ) import qualified Control.Concurrent.MVar as MVar import Control.Lens ( view, (^.) ) -import Control.Monad (foldM, forM, unless, void, when) +import Control.Monad (foldM, forM) import Control.Monad.IO.Class import qualified Control.Monad.IO.Unlift as IO import Control.Monad.Reader (asks, local) @@ -37,11 +37,9 @@ import Numeric (showHex) import Prettyprinter import qualified Data.BitVector.Sized as BV -import qualified Data.ByteString as BS import qualified Data.ByteString.Char8 as BSC import qualified Data.Map as Map import qualified Data.Set as Set -import Data.List (findIndex) import Data.Maybe (mapMaybe, catMaybes) import Data.Proxy import Data.Functor.Const @@ -53,7 +51,6 @@ import Data.Parameterized.Classes import Data.Parameterized.NatRepr import Data.Parameterized.Some import qualified Data.Parameterized.TraversableF as TF -import qualified Data.Parameterized.TraversableFC as TFC import Data.Parameterized.Nonce import qualified Data.Parameterized.Context as Ctx @@ -65,7 +62,6 @@ import qualified Lang.Crucible.Backend as LCB import qualified Lang.Crucible.LLVM.MemModel as CLM import qualified Lang.Crucible.Simulator.RegValue as LCS import Lang.Crucible.Simulator.SymSequence -import qualified Lang.Crucible.Utils.MuxTree as MT import qualified Data.Macaw.CFG as MM import qualified Data.Macaw.CFGSlice as MCS @@ -81,7 +77,6 @@ import qualified Pate.Discovery as PD import qualified Pate.Discovery.ParsedFunctions as PD import qualified Pate.Config as PCfg import qualified Pate.Equivalence as PE -import qualified Pate.Equivalence.RegisterDomain as PER import qualified Pate.Equivalence.EquivalenceDomain as PEq import qualified Pate.Equivalence.MemoryDomain as PEm import qualified Pate.Equivalence.Condition as PEC @@ -91,7 +86,6 @@ import qualified Pate.Event as PE import qualified Pate.Memory as PM import qualified Pate.MemCell as PMc import qualified Pate.Memory.MemTrace as MT -import qualified Pate.Location as PL import Pate.Monad import qualified Pate.Monad.Context as PMC import qualified Pate.Monad.Environment as PME @@ -102,26 +96,23 @@ import qualified Pate.SimState as PS import qualified Pate.SimulatorRegisters as PSR import qualified Pate.Verification.StrongestPosts.CounterExample as CE import qualified Pate.Register.Traversal as PRt -import Pate.Discovery.PLT (extraJumpClassifier, ExtraJumps(..), ExtraJumpTarget(..)) +import Pate.Discovery.PLT (ExtraJumps, ExtraJumpTarget(..)) import Pate.TraceTree import qualified Pate.Verification.Validity as PVV import qualified Pate.Verification.SymbolicExecution as PVSy -import qualified Pate.Verification.ConditionalEquiv as PVC import qualified Pate.Verification.Simplify as PSi import Pate.Verification.PairGraph -import Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, mkNodeEntry, mkNodeReturn, nodeBlocks, addContext, returnToEntry, graphNodeBlocks, returnOfEntry, NodeReturn (nodeFuns), asSingleReturn, rootEntry, rootReturn, getDivergePoint, asSingleNode, mkNodeEntry', functionEntryOf, eqUptoDivergePoint, asSingleGraphNode ) +import Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, mkNodeEntry, mkNodeReturn, nodeBlocks, addContext, returnToEntry, graphNodeBlocks, returnOfEntry, NodeReturn (nodeFuns), asSingleReturn, rootEntry, getDivergePoint, asSingleNode, mkNodeEntry', functionEntryOf, eqUptoDivergePoint, asSingleGraphNode ) import Pate.Verification.Widening import qualified Pate.Verification.AbstractDomain as PAD import Data.Monoid (All(..), Any (..)) -import Data.Maybe (fromMaybe, fromJust) -import qualified System.IO as IO +import Data.Maybe (fromMaybe) import Control.Monad (forM_) import qualified Data.Macaw.Discovery as MD -import Data.Foldable (foldl') import qualified Pate.ExprMappable as PEM -import Pate.Verification.StrongestPosts.CounterExample (RegsCounterExample(..), prettyRegsCE) +import Pate.Verification.StrongestPosts.CounterExample (RegsCounterExample(..)) import qualified Data.Macaw.BinaryLoader as MBL import What4.Partial (justPartExpr) import qualified Data.Aeson as JSON @@ -391,10 +382,10 @@ handleSyncPoint pg nd _spec = case getDivergePoint nd of Nothing -> return Nothing -addressOfNode :: +_addressOfNode :: GraphNode arch -> EquivM sym arch (PPa.PatchPairC (MM.ArchSegmentOff arch)) -addressOfNode nd = PPa.forBinsC $ \bin -> do +_addressOfNode nd = PPa.forBinsC $ \bin -> do blk <- PPa.get bin (graphNodeBlocks nd) blockToSegOff blk @@ -654,12 +645,12 @@ atomicJump :: atomicJump (from,to) domSpec gr0 = withSym $ \sym -> do -} -addImmediateEqDomRefinementChoice :: +_addImmediateEqDomRefinementChoice :: GraphNode arch -> PAD.AbstractDomain sym arch v -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) -addImmediateEqDomRefinementChoice nd preD gr0 = do +_addImmediateEqDomRefinementChoice nd preD gr0 = do let gr1 = gr0 choose @"()" ("Refine equivalence domain for sync point?") $ \choice -> do let go condK = do @@ -2031,7 +2022,7 @@ findPLTSymbol blkO blkP = -- TODO: This is a bit tricky because it might involve architecture-specific -- reasoning -handleArchStmt :: +_handleArchStmt :: PS.SimScope sym arch v -> SimBundle sym arch v -> NodeEntry arch {- ^ current entry point -} -> @@ -2041,7 +2032,7 @@ handleArchStmt :: PPa.PatchPair (PB.ConcreteBlock arch) {- ^ next entry point -} -> Maybe (PPa.PatchPair (PB.ConcreteBlock arch)) {- ^ return point -} -> EquivM sym arch (PairGraph sym arch) -handleArchStmt scope bundle currBlock d gr endCase pPair mpRetPair = fnTrace "handleArchStmt" $ case endCase of +_handleArchStmt scope bundle currBlock d gr endCase pPair mpRetPair = fnTrace "handleArchStmt" $ case endCase of -- this is the jump case for returns, if we return *with* a return site, then -- this is actually a normal jump MCS.MacawBlockEndReturn | Just pRetPair <- mpRetPair, pPair == pRetPair -> @@ -2273,11 +2264,11 @@ isMismatchedStubs (PPa.PatchPairC ma mb) = case (ma, mb) of (Nothing, Just{}) -> True (Nothing, Nothing) -> False -singletonBundle :: +_singletonBundle :: PBi.WhichBinaryRepr bin -> SimBundle sym arch v -> EquivM sym arch (SimBundle sym arch v) -singletonBundle bin (SimBundle in_ out_) = +_singletonBundle bin (SimBundle in_ out_) = SimBundle <$> PPa.asSingleton bin in_ <*> PPa.asSingleton bin out_ handleDivergingPaths :: @@ -2316,7 +2307,7 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi Just DeferDecision -> return DeferDecision Just ChooseSyncPoint -> return DeferDecision _ -> do - () <- withTracing @"message" "Equivalence Counter-example" $ withSym $ \sym -> do + () <- withTracing @"message" "Equivalence Counter-example" $ withSym $ \_sym -> do -- we've already introduced the path condition here, so we just want to see how we got here res <- getSomeGroundTrace scope bundle dom Nothing emitTrace @"trace_events" res diff --git a/src/Pate/Verification/SymbolicExecution.hs b/src/Pate/Verification/SymbolicExecution.hs index db93beae..798355a2 100644 --- a/src/Pate/Verification/SymbolicExecution.hs +++ b/src/Pate/Verification/SymbolicExecution.hs @@ -17,12 +17,9 @@ module Pate.Verification.SymbolicExecution ( import qualified System.Directory as SD import System.FilePath ( (), (<.>) ) -import qualified Prettyprinter as PP import qualified Prettyprinter.Render.Text as PPT import Control.Lens ( (^.) ) -import Control.Monad ( forM_ ) -import Control.Monad.IO.Class ( liftIO ) import qualified Control.Monad.Reader as CMR import qualified Data.List as DL import qualified Data.Parameterized.Context as Ctx @@ -89,7 +86,6 @@ isTerminalBlock pb = MCS.MacawBlockEndBranch -> False MCS.MacawBlockEndFail -> True MCS.MacawBlockEndArch -> True - _ -> error $ "Unexpected terminal block case:" ++ show c -- | Construct an initial 'CS.SimContext' for Crucible -- diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index 649e79e1..b2c783e7 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -96,7 +96,7 @@ import qualified Pate.Config as PC import Pate.Verification.PairGraph import qualified Pate.Verification.ConditionalEquiv as PVC import qualified Pate.Verification.Validity as PVV -import Pate.Verification.PairGraph.Node ( GraphNode(..), pattern GraphNodeEntry, pattern GraphNodeReturn, nodeFuns, graphNodeBlocks ) +import Pate.Verification.PairGraph.Node ( GraphNode(..), pattern GraphNodeEntry, pattern GraphNodeReturn ) import qualified Pate.Verification.StrongestPosts.CounterExample as CE import qualified Pate.AssumptionSet as PAs @@ -109,12 +109,8 @@ import qualified Pate.Monad.Context as PMC import Data.Functor.Const (Const(..)) import Pate.Verification.Concretize (symbolicFromConcrete) import qualified Pate.Arch as PA -import Data.Parameterized (Pair(..)) import Data.Kind (Type) import qualified Data.Aeson as JSON -import qualified Prettyprinter as PP -import qualified What4.Expr.GroundEval as W4 -import qualified Lang.Crucible.Utils.MuxTree as MT import Pate.Verification.Domain (universalDomain) -- | Generate a fresh abstract domain value for the given graph node. @@ -419,7 +415,7 @@ addRefinementChoice nd gr0 = withTracing @"message" "Modify Proof Node" $ do -- TODO: allow updates here emitTrace @"interactiveBundle" b return gr2 - choice "Strengthen conditions" $ \(TupleF3 scope bundle d) gr2 -> withSym $ \sym -> do + choice "Strengthen conditions" $ \(TupleF3 scope _bundle _d) gr2 -> withSym $ \_sym -> do let go condK gr0_ = case getCondition gr0_ nd condK of Just eqCondSpec -> withTracing @"message" (conditionName condK) $ withSym $ \sym -> do (_, eqCond) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) eqCondSpec @@ -716,7 +712,7 @@ pickMany pickIn = go mempty pickIn forM_ (zip [0..] (pickRegs remaining)) $ \(idx, Some r) -> case PA.displayRegister r of PA.Normal{} -> choice "" (PickRegister r) $ do - let (hd_,(_:tl_)) = splitAt idx (pickRegs remaining) + (hd_,(_:tl_)) <- return $ splitAt idx (pickRegs remaining) return $ (mempty { pickRegs = [Some r] } <> acc, remaining { pickRegs = hd_++tl_ }) -- in general we can include any register, but it likely -- makes sense to only consider registers that we have @@ -724,11 +720,11 @@ pickMany pickIn = go mempty pickIn _ -> return () forM_ (zip [0..] (pickStack remaining)) $ \(idx, Some c) -> do choice "" (PickStack c) $ do - let (hd_,(_:tl_)) = splitAt idx (pickStack remaining) + (hd_,(_:tl_)) <- return $ splitAt idx (pickStack remaining) return $ (mempty { pickStack = [Some c] } <> acc, remaining { pickStack = hd_++tl_ }) forM_ (zip [0..] (pickGlobal remaining)) $ \(idx, Some c) -> do choice "" (PickGlobal c) $ do - let (hd_,(_:tl_)) = splitAt idx (pickGlobal remaining) + (hd_,(_:tl_)) <- return $ splitAt idx (pickGlobal remaining) return $ (mempty { pickGlobal = [Some c] } <> acc, remaining { pickGlobal = hd_++tl_ }) go acc' remaining' @@ -763,14 +759,14 @@ refineEquivalenceDomain dom = withSym $ \sym -> do -- | True if the satisfiability of the predicate only depends on -- variables from the given binary -isEqCondSingleSided :: +_isEqCondSingleSided :: forall sym arch bin v. PS.SimScope sym arch v -> PB.BlockPair arch -> PBi.WhichBinaryRepr bin -> PEC.EquivalenceCondition sym arch v -> EquivM sym arch Bool -isEqCondSingleSided scope blks bin eqCond = withSym $ \sym -> do +_isEqCondSingleSided scope blks bin eqCond = withSym $ \sym -> do goalTimeout <- CMR.asks (PC.cfgGoalTimeout . envConfig) -- rewrite the free variables for the other binary into arbitrary (free) terms and -- determine if the resulting predicate is equal to the original @@ -1015,9 +1011,9 @@ runMaybeTF m = runMaybeT m >>= \case Just a -> return $ JustF a Nothing -> return $ NothingF -toMaybe :: MaybeCF a c tp -> Maybe (a tp c) -toMaybe (JustF a) = Just a -toMaybe NothingF = Nothing +_toMaybe :: MaybeCF a c tp -> Maybe (a tp c) +_toMaybe (JustF a) = Just a +_toMaybe NothingF = Nothing memVars :: PS.SimVars sym arch v bin -> EquivM sym arch (Set.Set (Some (W4.BoundVar sym))) diff --git a/tools/pate-repl/Repl.hs b/tools/pate-repl/Repl.hs index 5e6c6bc1..a7be7056 100644 --- a/tools/pate-repl/Repl.hs +++ b/tools/pate-repl/Repl.hs @@ -26,7 +26,6 @@ module Repl where import qualified Language.Haskell.TH as TH -import qualified System.Console.ANSI as ANSI import qualified Options.Applicative as OA import qualified System.IO as IO import qualified System.IO.Unsafe as IO @@ -36,9 +35,7 @@ import Control.Monad ( forM ) import Control.Monad.State ( MonadState, StateT, modify, gets, runStateT, get, put ) import qualified Control.Monad.IO.Class as IO import Data.Proxy -import qualified Data.Text.IO as Text import qualified Data.Text as Text -import qualified Data.Text.Lazy as TextL import Text.Read (readMaybe) import System.Exit import System.Environment @@ -48,8 +45,6 @@ import Data.Parameterized.Classes import Data.List.Split (splitOn) import qualified Prettyprinter as PP import Prettyprinter ( (<+>) ) -import qualified Prettyprinter.Render.Terminal as PPRT -import qualified Prettyprinter.Render.Text as PPText import Data.Parameterized.SymbolRepr ( KnownSymbol, knownSymbol, SymbolRepr, symbolRepr ) @@ -58,7 +53,6 @@ import qualified Pate.Arch as PA import qualified Pate.ArchLoader as PAL import qualified Pate.Config as PC import qualified Pate.Solver as PS -import qualified Pate.Script as PSc import qualified Pate.Equivalence as PEq import qualified Pate.CLI as CLI import qualified Pate.Loader as PL @@ -67,7 +61,6 @@ import qualified ReplBase import ReplBase ( Sym, Arch ) import Pate.TraceTree hiding (asChoice) -import What4.Expr.Builder as W4B import Unsafe.Coerce(unsafeCoerce) @@ -212,7 +205,7 @@ isSubTreeNode (TraceNode{}) = do loadSomeTree :: IO.ThreadId -> SomeTraceTree PA.ValidRepr -> LoadOpts -> IO Bool -loadSomeTree tid topTraceTree opts = do +loadSomeTree tid topTraceTree _opts = do viewSomeTraceTree topTraceTree (return False) $ \(PA.ValidRepr sym arch) (toptree :: TraceTree k) -> do let st = ReplState { replNode = Some (TraceNode @"toplevel" () () toptree) @@ -314,7 +307,6 @@ addNextNodes node = isTraceNode node $ do (IO.liftIO $ nodeShownAt tags node) >>= \case True -> do nextSubs <- fmap concat $ forM nextTrees $ \(n, Some nextNode) -> do - prevNodes <- gets replPrev next <- maybeSubNodes nextNode (return []) (gets replNext) issub <- isSubTreeNode nextNode case (issub, next) of @@ -353,7 +345,7 @@ mkStatusTag st = case ppStatusTag st of Nothing -> Nothing ppSuffix :: Int -> NodeStatus -> SymbolRepr nm -> ReplM sym arch (Maybe (PP.Doc a)) -ppSuffix nesting s nm = do +ppSuffix _nesting s nm = do tags <- gets replTags case tags of [Simplified] -> return $ mkStatusTag s @@ -381,7 +373,7 @@ maybeSubNodes :: ReplM sym arch a -> ReplM sym arch a -> ReplM sym arch a -maybeSubNodes nd@(TraceNode lbl v subtree) g f = do +maybeSubNodes nd@(TraceNode _lbl _v _subtree) g f = do prevNodes <- gets replPrev isSubTreeNode nd >>= \case True -> withNode nd $ f @@ -410,7 +402,7 @@ prettyNextNodes startAt onlyFinished = do nextNodes <- gets replNext ValidSymArchRepr sym _ <- gets replValidRepr ppContents' <- - mapM (\(nesting, Some (nd@(TraceNode lbl v subtree) :: TraceNode sym arch nm)) -> do + mapM (\(nesting, Some ((TraceNode lbl v subtree) :: TraceNode sym arch nm)) -> do b <- IO.liftIO $ getTreeStatus subtree json <- IO.liftIO $ jsonNode @_ @'(sym, arch) @nm sym lbl v case prettyNodeAt @'(sym, arch) @nm tags lbl v of @@ -575,17 +567,17 @@ loadTraceNode node = do isBlocked :: forall sym arch. ReplM sym arch Bool isBlocked = do - (Some (node@(TraceNode _ _ subtree))) <- gets replNode + (Some (TraceNode _ _ subtree)) <- gets replNode st <- IO.liftIO $ getTreeStatus subtree return $ isBlockedStatus st asChoice :: forall sym arch nm. TraceNode sym arch nm -> ReplM sym arch (Maybe (SomeChoice '(sym,arch))) -asChoice (node@(TraceNode _ v _)) = case testEquality (knownSymbol @nm) (knownSymbol @"choice") of +asChoice (TraceNode _ v _) = case testEquality (knownSymbol @nm) (knownSymbol @"choice") of Just Refl -> return $ Just v Nothing -> return Nothing asChoiceTree :: forall sym arch nm. TraceNode sym arch nm -> ReplM sym arch (Maybe (SomeChoiceHeader '(sym,arch))) -asChoiceTree (node@(TraceNode _ v _)) = case testEquality (knownSymbol @nm) (knownSymbol @"choiceTree") of +asChoiceTree (TraceNode _ v _) = case testEquality (knownSymbol @nm) (knownSymbol @"choiceTree") of Just Refl -> return $ Just v Nothing -> return Nothing @@ -597,7 +589,7 @@ goto_status'' f (Some node@(TraceNode _ _ subtree) : xs) = do goto_node' node >> (goto_status' f) False -> goto_status'' f xs -goto_status'' f [] = return () +goto_status'' _f [] = return () goto_status' :: (NodeStatus -> Bool) -> ReplM sym arch () goto_status' f = do @@ -620,7 +612,7 @@ goto_prompt = execReplM (goto_status' isBlockedStatus >> ls') next :: IO () next = execReplM $ do nextNodes <- gets replNext - goto' (length nextNodes - 1) + _ <- goto' (length nextNodes - 1) return () goto_node' :: TraceNode sym arch nm -> ReplM sym arch () @@ -636,7 +628,6 @@ goto' idx = do Just (SomeChoice c) -> do IO.liftIO $ choicePick c (IO.liftIO $ IO.threadDelay 100) - Some curNode <- currentNode top' IO.liftIO $ wait (Just <$> currentNode) @@ -663,7 +654,7 @@ waitRepl lastShown = do PO.printBreak prettyNextNodes lastShown False >>= PO.printOutputLn False -> do - Some (node@(TraceNode _ _ t)) <- gets replNode + Some (TraceNode _ _ t) <- gets replNode st <- IO.liftIO $ getTreeStatus t case isFinished st of True -> PO.printErrLn "No such option" >> return () diff --git a/tools/pate/Main.hs b/tools/pate/Main.hs index b97196d5..463700f1 100644 --- a/tools/pate/Main.hs +++ b/tools/pate/Main.hs @@ -3,14 +3,11 @@ module Main ( main ) where import qualified System.Exit as SE -import Pate.TraceTree import qualified Pate.CLI as CLI import qualified Options.Applicative as OA import qualified Pate.ArchLoader as PAL import qualified Pate.Loader as PL import qualified Pate.Equivalence as PEq -import qualified Pate.Config as PC -import qualified Pate.Script as PS import qualified System.IO as IO main :: IO () diff --git a/tools/pate/Output.hs b/tools/pate/Output.hs index c8e79595..50a56d7a 100644 --- a/tools/pate/Output.hs +++ b/tools/pate/Output.hs @@ -63,8 +63,8 @@ data Output_ = data Output = Output { outputC :: Output_ - , output_this :: Maybe (PP.Doc ()) - , output_tag :: Maybe (Text.Text) + , _output_this :: Maybe (PP.Doc ()) + , _output_tag :: Maybe (Text.Text) } output :: Output_ -> Output