diff --git a/cryptol-saw-core/cryptol-saw-core.cabal b/cryptol-saw-core/cryptol-saw-core.cabal index 9a38024a2f..0235b3679d 100644 --- a/cryptol-saw-core/cryptol-saw-core.cabal +++ b/cryptol-saw-core/cryptol-saw-core.cabal @@ -27,6 +27,7 @@ library containers, cryptol >= 2.3.0, data-inttrie >= 0.1.4, + deepseq, integer-gmp, modern-uri, mtl, diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs index dac3549deb..2617dbf144 100644 --- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs +++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs @@ -6,12 +6,15 @@ Maintainer : huffman Stability : provisional -} {-# LANGUAGE PatternGuards #-} +{-# LANGUAGE DeriveGeneric #-} module Verifier.SAW.TypedTerm where +import Control.DeepSeq import Control.Monad (foldM) import Data.Map (Map) import qualified Data.Map as Map import Data.Text (Text) +import GHC.Generics import Cryptol.ModuleSystem.Name (nameIdent) import qualified Cryptol.TypeCheck.AST as C @@ -36,8 +39,8 @@ data TypedTerm = { ttType :: TypedTermType , ttTerm :: Term } - deriving Show - + deriving (Show, Generic) +instance NFData TypedTerm -- | The different notion of Cryptol types that -- as SAWCore term might have. @@ -45,7 +48,9 @@ data TypedTermType = TypedTermSchema C.Schema | TypedTermKind C.Kind | TypedTermOther Term - deriving Show + deriving (Show, Generic) + +instance NFData TypedTermType ttTermLens :: Functor f => (Term -> f Term) -> TypedTerm -> f TypedTerm @@ -149,7 +154,9 @@ data TypedExtCns = { tecType :: C.Type , tecExt :: ExtCns Term } - deriving Show + deriving (Show, Generic) + +instance NFData TypedExtCns -- | Recognize 'TypedTerm's that are external constants. asTypedExtCns :: TypedTerm -> Maybe TypedExtCns diff --git a/saw-core/saw-core.cabal b/saw-core/saw-core.cabal index 6775dc328b..a33cc1deaf 100644 --- a/saw-core/saw-core.cabal +++ b/saw-core/saw-core.cabal @@ -30,6 +30,7 @@ library containers, data-inttrie, data-ref, + deepseq, directory, filepath, hashable >= 1.3.4, diff --git a/saw-core/src/Verifier/SAW/Name.hs b/saw-core/src/Verifier/SAW/Name.hs index d979ea82d1..5fe7533f8e 100644 --- a/saw-core/src/Verifier/SAW/Name.hs +++ b/saw-core/src/Verifier/SAW/Name.hs @@ -51,6 +51,7 @@ module Verifier.SAW.Name , bestAlias ) where +import Control.DeepSeq import Control.Exception (assert) import Data.Char import Data.Hashable @@ -79,6 +80,8 @@ newtype ModuleName = ModuleName Text instance Hashable ModuleName -- automatically derived +instance NFData ModuleName + instance Show ModuleName where show (ModuleName s) = Text.unpack s @@ -110,6 +113,7 @@ data Ident = deriving (Eq, Ord, Generic) instance Hashable Ident -- automatically derived +instance NFData Ident instance Show Ident where show (Ident m s) = shows m ('.' : Text.unpack s) @@ -177,7 +181,9 @@ data NameInfo [Text] -- ^ A collection of aliases for this name. Sorter or "less-qualified" -- aliases should be nearer the front of the list - deriving (Eq,Ord,Show) + deriving (Eq,Ord,Show,Generic) + +instance NFData NameInfo nameURI :: NameInfo -> URI nameURI = @@ -225,7 +231,7 @@ data ExtCns e = , ecName :: !NameInfo , ecType :: !e } - deriving (Show, Functor, Foldable, Traversable) + deriving (Show, Functor, Foldable, Traversable, Generic) instance Eq (ExtCns e) where x == y = ecVarIndex x == ecVarIndex y @@ -236,6 +242,7 @@ instance Ord (ExtCns e) where instance Hashable (ExtCns e) where hashWithSalt x ec = hashWithSalt x (ecVarIndex ec) +instance NFData e => NFData (ExtCns e) -- Primitive Names ------------------------------------------------------------ @@ -246,7 +253,9 @@ data PrimName e = , primName :: !Ident , primType :: e } - deriving (Show, Functor, Foldable, Traversable) + deriving (Show, Functor, Foldable, Traversable, Generic) + +instance NFData e => NFData (PrimName e) instance Eq (PrimName e) where x == y = primVarIndex x == primVarIndex y diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index 4d267f3435..bd30e5f677 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/saw-core/src/Verifier/SAW/Rewriter.hs @@ -2,6 +2,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE NamedFieldPuns #-} @@ -61,6 +62,7 @@ module Verifier.SAW.Rewriter import Control.Applicative ((<$>), pure, (<*>)) import Data.Foldable (Foldable) #endif +import Control.DeepSeq import Control.Monad.Identity import Control.Monad.State import Control.Monad.Trans.Maybe @@ -73,7 +75,7 @@ import Data.Set (Set) import qualified Data.Set as Set import Control.Monad.Trans.Writer.Strict import Numeric.Natural - +import GHC.Generics import Verifier.SAW.Cache import Verifier.SAW.Conversion @@ -86,7 +88,7 @@ import Verifier.SAW.Prelude.Constants data RewriteRule a = RewriteRule { ctxt :: [Term], lhs :: Term, rhs :: Term, permutative :: Bool, annotation :: Maybe a } - deriving (Show) + deriving (Show, Generic) -- ^ Invariant: The set of loose variables in @lhs@ must be exactly -- @[0 .. length ctxt - 1]@. The @rhs@ may contain a subset of these. @@ -95,6 +97,8 @@ instance Eq (RewriteRule a) where RewriteRule c1 l1 r1 p1 _a1 == RewriteRule c2 l2 r2 p2 _a2 = c1 == c2 && l1 == l2 && r1 == r2 && p1 == p2 +instance NFData a => NFData (RewriteRule a) + ctxtRewriteRule :: RewriteRule a -> [Term] ctxtRewriteRule = ctxt diff --git a/saw-core/src/Verifier/SAW/Term/Functor.hs b/saw-core/src/Verifier/SAW/Term/Functor.hs index 59c3e3276d..a50ea6da2d 100644 --- a/saw-core/src/Verifier/SAW/Term/Functor.hs +++ b/saw-core/src/Verifier/SAW/Term/Functor.hs @@ -66,6 +66,7 @@ import Data.Bits #if !MIN_VERSION_base(4,8,0) import Data.Foldable (Foldable) #endif +import Control.DeepSeq import qualified Data.Foldable as Foldable (and, foldl') import Data.Hashable import Data.Map (Map) @@ -101,6 +102,7 @@ data Sort = TypeSort Natural | PropSort deriving (Eq, Generic, TH.Lift) +instance NFData Sort -- Prop is the lowest sort instance Ord Sort where @@ -216,6 +218,7 @@ data FlatTermF e deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic) instance Hashable e => Hashable (FlatTermF e) -- automatically derived +instance NFData e => NFData (FlatTermF e) -- Capture more type information here so we can -- use it during evaluation time to remember the @@ -232,6 +235,7 @@ data CompiledRecursor e = deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic) instance Hashable e => Hashable (CompiledRecursor e) -- automatically derived +instance NFData e => NFData (CompiledRecursor e) -- | Test if the association list used in a 'RecordType' or 'RecordValue' uses -- precisely the given field names and no more. If so, return the values @@ -347,7 +351,7 @@ data TermF e deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic) instance Hashable e => Hashable (TermF e) -- automatically derived. - +instance NFData e => NFData (TermF e) -- Term Datatype --------------------------------------------------------------- @@ -360,12 +364,14 @@ data Term , stAppTermF :: !(TermF Term) } | Unshared !(TermF Term) - deriving (Show, Typeable) + deriving (Show, Typeable, Generic) instance Hashable Term where hashWithSalt salt STApp{ stAppIndex = i } = salt `combine` 0x00000000 `hashWithSalt` hash i hashWithSalt salt (Unshared t) = salt `combine` 0x55555555 `hashWithSalt` hash t +instance NFData Term + -- | Combine two given hash values. 'combine' has zero as a left -- identity. (FNV hash, copied from Data.Hashable 1.2.1.0.) @@ -431,6 +437,9 @@ unwrapTermF (Unshared tf) = tf -- Bit n is a 1 iff n is in the set. newtype BitSet = BitSet Integer deriving (Eq, Ord, Show) +instance NFData BitSet where + rnf (BitSet x) = rnf x + -- | The empty 'BitSet' emptyBitSet :: BitSet emptyBitSet = BitSet 0 diff --git a/saw-core/src/Verifier/SAW/TermNet.hs b/saw-core/src/Verifier/SAW/TermNet.hs index 3c7a6dd101..0d9e6954aa 100644 --- a/saw-core/src/Verifier/SAW/TermNet.hs +++ b/saw-core/src/Verifier/SAW/TermNet.hs @@ -29,6 +29,7 @@ module Verifier.SAW.TermNet , content -- :: Net a -> [a] ) where +import Control.DeepSeq import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe (fromMaybe) @@ -117,6 +118,11 @@ data Net a | Net { comb :: Net a, var :: Net a, atoms :: Map Text (Net a) } deriving Show +-- NB, this doesn't actually force the annotations +instance NFData (Net a) where + rnf (Leaf ls) = foldr seq () ls + rnf (Net a b c) = rnf (a,b,c) + {- Invariant: A well-formed term net should satisfy @valid 1@. Every sub-net should satisfy @valid n@ for some non-negative @n@. diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index a9cc7e7135..ec4efa89bd 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -12,6 +12,7 @@ Grow\", and is prevalent across the Crucible codebase. {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} @@ -24,12 +25,14 @@ Grow\", and is prevalent across the Crucible codebase. module SAWScript.Crucible.Common.MethodSpec where import Data.Constraint (Constraint) +import GHC.Generics import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set) import Data.Time.Clock import Data.Void (Void) +import Control.DeepSeq import Control.Monad.Trans.Maybe import Control.Monad.Trans (lift) import Control.Lens @@ -55,9 +58,11 @@ import SAWScript.Prover.SolverStats import SAWScript.Utils (bullets) import SAWScript.Proof (TheoremNonce) + -- | How many allocations have we made in this method spec? newtype AllocIndex = AllocIndex Int - deriving (Eq, Ord, Show) + deriving (Eq, Ord, Show, Generic) +instance NFData AllocIndex nextAllocIndex :: AllocIndex -> AllocIndex nextAllocIndex (AllocIndex n) = AllocIndex (n + 1) @@ -65,7 +70,8 @@ nextAllocIndex (AllocIndex n) = AllocIndex (n + 1) -- | Are we writing preconditions or postconditions? data PrePost = PreState | PostState - deriving (Eq, Ord, Show) + deriving (Eq, Ord, Show, Generic) +instance NFData PrePost -------------------------------------------------------------------------------- -- *** Extension-specific information @@ -152,8 +158,25 @@ type SetupValueHas (c :: Type -> Constraint) ext = , c (CastType ext) ) +deriving instance Generic (SetupValue ext) deriving instance (SetupValueHas Show ext) => Show (SetupValue ext) +instance + ( NFData (B (HasSetupNull ext)) + , NFData (B (HasSetupStruct ext)) + , NFData (B (HasSetupArray ext)) + , NFData (B (HasSetupElem ext)) + , NFData (B (HasSetupUnion ext)) + , NFData (B (HasSetupField ext)) + , NFData (B (HasSetupCast ext)) + , NFData (B (HasGhostState ext)) + , NFData (B (HasSetupGlobal ext)) + , NFData (B (HasSetupGlobalInitializer ext)) + , NFData (TypeName ext) + , NFData (CastType ext) + ) => NFData (SetupValue ext) + + -- TypedTerm is neither Eq nor Ord -- deriving instance (SetupValueHas Eq ext) => Eq (SetupValue ext) -- deriving instance (SetupValueHas Ord ext) => Ord (SetupValue ext) @@ -286,7 +309,10 @@ data ConditionMetadata = , conditionType :: String , conditionContext :: String } - deriving (Show, Eq, Ord) + deriving (Show, Eq, Ord, Generic) + +instance NFData ConditionMetadata + -------------------------------------------------------------------------------- -- *** StateSpec @@ -300,9 +326,25 @@ data SetupCondition ext where TypedTerm -> SetupCondition ext +deriving instance Generic (SetupCondition ext) deriving instance ( SetupValueHas Show ext , Show (B (HasGhostState ext)) ) => Show (SetupCondition ext) +instance + ( NFData (B (HasSetupNull ext)) + , NFData (B (HasSetupStruct ext)) + , NFData (B (HasSetupArray ext)) + , NFData (B (HasSetupElem ext)) + , NFData (B (HasSetupUnion ext)) + , NFData (B (HasSetupField ext)) + , NFData (B (HasSetupCast ext)) + , NFData (B (HasGhostState ext)) + , NFData (B (HasSetupGlobal ext)) + , NFData (B (HasSetupGlobalInitializer ext)) + , NFData (TypeName ext) + , NFData (CastType ext) + ) => NFData (SetupCondition ext) + -- | Verification state (either pre- or post-) specification data StateSpec ext = StateSpec @@ -319,6 +361,23 @@ data StateSpec ext = StateSpec } makeLenses ''StateSpec +deriving instance Generic (StateSpec ext) +instance + ( NFData (B (HasSetupNull ext)) + , NFData (B (HasSetupStruct ext)) + , NFData (B (HasSetupArray ext)) + , NFData (B (HasSetupElem ext)) + , NFData (B (HasSetupUnion ext)) + , NFData (B (HasSetupField ext)) + , NFData (B (HasSetupCast ext)) + , NFData (B (HasGhostState ext)) + , NFData (B (HasSetupGlobal ext)) + , NFData (B (HasSetupGlobalInitializer ext)) + , NFData (TypeName ext) + , NFData (CastType ext) + , NFData (AllocSpec ext) + , NFData (PointsTo ext) + ) => NFData (StateSpec ext) initialStateSpec :: StateSpec ext initialStateSpec = StateSpec @@ -353,13 +412,38 @@ data CrucibleMethodSpecIR ext = , _csCodebase :: Codebase ext -- ^ the codebase this spec was verified against , _csLoc :: ProgramLoc -- ^ where in the SAWscript was this spec? } - + makeLenses ''CrucibleMethodSpecIR +deriving instance Generic (CrucibleMethodSpecIR ext) +instance + ( NFData (B (HasSetupNull ext)) + , NFData (B (HasSetupStruct ext)) + , NFData (B (HasSetupArray ext)) + , NFData (B (HasSetupElem ext)) + , NFData (B (HasSetupUnion ext)) + , NFData (B (HasSetupField ext)) + , NFData (B (HasSetupCast ext)) + , NFData (B (HasGhostState ext)) + , NFData (B (HasSetupGlobal ext)) + , NFData (B (HasSetupGlobalInitializer ext)) + , NFData (TypeName ext) + , NFData (CastType ext) + , NFData (AllocSpec ext) + , NFData (PointsTo ext) + , NFData (MethodId ext) + , NFData (ExtType ext) + , NFData (AllocGlobal ext) + , NFData (Codebase ext) + ) => + NFData (CrucibleMethodSpecIR ext) data ProofMethod = SpecAdmitted | SpecProved +instance NFData ProofMethod where + rnf pm = seq pm () + type SpecNonce ext = Nonce GlobalNonceGenerator (ProvedSpec ext) data ProvedSpec ext = @@ -374,6 +458,28 @@ data ProvedSpec ext = , _psElapsedTime :: NominalDiffTime -- ^ The time elapsed during the proof of this specification } +deriving instance Generic (ProvedSpec ext) +instance + ( NFData (B (HasSetupNull ext)) + , NFData (B (HasSetupStruct ext)) + , NFData (B (HasSetupArray ext)) + , NFData (B (HasSetupElem ext)) + , NFData (B (HasSetupUnion ext)) + , NFData (B (HasSetupField ext)) + , NFData (B (HasSetupCast ext)) + , NFData (B (HasGhostState ext)) + , NFData (B (HasSetupGlobal ext)) + , NFData (B (HasSetupGlobalInitializer ext)) + , NFData (TypeName ext) + , NFData (CastType ext) + , NFData (AllocSpec ext) + , NFData (PointsTo ext) + , NFData (MethodId ext) + , NFData (ExtType ext) + , NFData (AllocGlobal ext) + , NFData (Codebase ext) + ) => NFData (ProvedSpec ext) + makeLenses ''ProvedSpec mkProvedSpec :: diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 467991af82..cb196d8f8a 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -91,6 +91,7 @@ module SAWScript.Crucible.LLVM.Builtins import Prelude hiding (fail) +import Control.DeepSeq import qualified Control.Exception as X import Control.Lens @@ -297,7 +298,7 @@ llvm_verify (Some lm) nm lemmas checkSat setup tactic = end <- io getCurrentTime let diff = diffUTCTime end start ps <- io (MS.mkProvedSpec MS.SpecProved method_spec stats deps lemmaSet diff) - returnProof $ SomeLLVM ps + returnProof . SomeLLVM $! force ps llvm_refine_spec :: Some LLVMModule -> @@ -315,7 +316,7 @@ llvm_refine_spec (Some lm) nm lemmas setup tactic = end <- io getCurrentTime let diff = diffUTCTime end start ps <- io (MS.mkProvedSpec MS.SpecProved method_spec stats deps lemmaSet diff) - returnProof $ SomeLLVM ps + returnProof . SomeLLVM $! force ps llvm_unsafe_assume_spec :: Some LLVMModule -> @@ -327,7 +328,7 @@ llvm_unsafe_assume_spec (Some lm) nm setup = do printOutLnTop Info $ unwords ["Assume override", (method_spec ^. csName)] ps <- io (MS.mkProvedSpec MS.SpecAdmitted method_spec mempty mempty mempty 0) - returnProof $ SomeLLVM ps + returnProof . SomeLLVM $! force ps llvm_array_size_profile :: ProofScript () -> @@ -488,7 +489,7 @@ llvm_compositional_extract (Some lm) nm func_name lemmas checkSat setup tactic = end <- io getCurrentTime let diff = diffUTCTime end start ps <- io (MS.mkProvedSpec MS.SpecProved extracted_method_spec stats deps lemmaSet diff) - returnProof (SomeLLVM ps) + returnProof . SomeLLVM $! force ps setupValueAsExtCns :: SetupValue (LLVM arch) -> Maybe (ExtCns Term) setupValueAsExtCns = diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 7b9763f7f2..11d35b68cd 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -9,6 +9,7 @@ Stability : provisional {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DoAndIfThenElse #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE FlexibleContexts #-} @@ -118,6 +119,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR , testResolved ) where +import Control.DeepSeq import Control.Lens import Control.Monad (when) import Data.Functor.Compose (Compose(..)) @@ -129,6 +131,7 @@ import qualified Prettyprinter as PPL import qualified Text.LLVM.AST as L import qualified Text.LLVM.PP as L import qualified Text.PrettyPrint.HughesPJ as PP +import GHC.Generics (Generic) import qualified Data.LLVM.BitCode as LLVM @@ -155,6 +158,7 @@ import qualified SAWScript.Crucible.Common.Setup.Type as Setup import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL import SAWScript.Proof (TheoremNonce) +import SAWScript.Utils () import Verifier.SAW.Simulator.What4.ReturnTrip ( toSC, saw_ctx ) @@ -163,6 +167,7 @@ import Verifier.SAW.SharedTerm import Verifier.SAW.TypedTerm + -------------------------------------------------------------------------------- -- ** Language features @@ -191,7 +196,9 @@ data LLVMMethodId = LLVMMethodId { _llvmMethodName :: String , _llvmMethodParent :: Maybe String -- ^ Something to do with breakpoints... - } deriving (Eq, Ord, Show) + } deriving (Eq, Ord, Show, Generic) + +instance NFData LLVMMethodId makeLenses ''LLVMMethodId @@ -215,7 +222,9 @@ data LLVMAllocSpecInit -- ^ allocation is initialized with a fresh symbolic array of bytes | LLVMAllocSpecNoInitialization -- ^ allocation not initialized - deriving (Eq, Ord, Show) + deriving (Eq, Ord, Show, Generic) + +instance NFData LLVMAllocSpecInit data LLVMAllocSpec = LLVMAllocSpec @@ -227,7 +236,9 @@ data LLVMAllocSpec = , _allocSpecFresh :: Bool -- ^ Whether declared with @crucible_fresh_pointer@ , _allocSpecInit :: LLVMAllocSpecInit } - deriving (Eq, Show) + deriving (Eq, Show, Generic) + +instance NFData LLVMAllocSpec makeLenses ''LLVMAllocSpec @@ -263,6 +274,9 @@ data LLVMModule arch = -- 'loadLLVMModule' is the only function that is allowed to create -- values of type 'LLVMModule'. +instance NFData (LLVMModule arch) where + rnf (LLVMModule path m _mt) = rnf (path, m) + -- | The file path that the LLVM module was loaded from. modFilePath :: LLVMModule arch -> FilePath modFilePath = _modFilePath @@ -393,10 +407,15 @@ data LLVMPointsTo arch -- command, which doesn't quite fit into the 'LLVMPointsToValue' paradigm. -- The 'String' represents the name of the field within the bitfield. | LLVMPointsToBitfield MS.ConditionMetadata (MS.SetupValue (LLVM arch)) String (MS.SetupValue (LLVM arch)) + deriving (Generic) data LLVMPointsToValue arch = ConcreteSizeValue (MS.SetupValue (LLVM arch)) | SymbolicSizeValue TypedTerm TypedTerm + deriving (Generic) + +instance NFData (LLVMPointsToValue arch) +instance NFData (LLVMPointsTo arch) -- | Return the 'ProgramLoc' corresponding to an 'LLVMPointsTo' statement. llvmPointsToProgramLoc :: LLVMPointsTo arch -> ProgramLoc @@ -429,6 +448,10 @@ instance PPL.Pretty (LLVMPointsToValue arch) where type instance MS.AllocGlobal (LLVM arch) = LLVMAllocGlobal arch data LLVMAllocGlobal arch = LLVMAllocGlobal ProgramLoc L.Symbol + deriving (Generic) + +instance NFData (LLVMAllocGlobal arch) + ppAllocGlobal :: LLVMAllocGlobal arch -> PPL.Doc ann ppAllocGlobal (LLVMAllocGlobal _loc (L.Symbol name)) = @@ -628,7 +651,9 @@ data ResolvedPathItem = ResolvedField String | ResolvedElem Int | ResolvedCast L.Type - deriving (Show, Eq, Ord) + deriving (Show, Eq, Ord, Generic) + +instance NFData ResolvedPathItem type ResolvedPath = [ResolvedPathItem] @@ -652,7 +677,9 @@ data LLVMResolvedState = { _rsAllocs :: Map MS.AllocIndex [ResolvedPath] , _rsGlobals :: Map String [ResolvedPath] } - deriving (Eq, Ord, Show) + deriving (Eq, Ord, Show, Generic) + +instance NFData LLVMResolvedState emptyResolvedState :: LLVMResolvedState emptyResolvedState = ResolvedState Map.empty Map.empty diff --git a/src/SAWScript/Position.hs b/src/SAWScript/Position.hs index ef7dfecf5b..ac6c3a39ab 100644 --- a/src/SAWScript/Position.hs +++ b/src/SAWScript/Position.hs @@ -15,6 +15,7 @@ Stability : provisional module SAWScript.Position where +import Control.DeepSeq import Control.Lens import Data.Data (Data) import Data.List (intercalate) @@ -38,6 +39,8 @@ data Pos = Range !FilePath -- file | PosREPL deriving (Data, Generic, Eq) +instance NFData Pos + renderDoc :: PP.Doc ann -> String renderDoc doc = PP.renderString (PP.layoutPretty opts doc) where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8) diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index 823352d3d6..1b527efe2d 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -7,6 +7,7 @@ Stability : provisional -} {-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ParallelListComp #-} @@ -92,6 +93,7 @@ module SAWScript.Proof , predicateToSATQuery ) where +import Control.DeepSeq import qualified Control.Monad.Fail as F import Control.Monad.Except import Data.IORef @@ -103,6 +105,7 @@ import qualified Data.Set as Set import Data.Text (Text) import qualified Data.Text as Text import Data.Time.Clock +import GHC.Generics (Generic) import Data.Parameterized.Nonce @@ -128,6 +131,7 @@ import SAWScript.Crucible.Common as Common import qualified Verifier.SAW.Simulator.What4 as W4Sim import qualified Verifier.SAW.Simulator.What4.ReturnTrip as W4Sim import SAWScript.Panic(panic) +import SAWScript.Utils () -- bring in some orphan instances -- | A proposition is a saw-core type of type `Prop`. -- In particular, this includes any pi type whose result @@ -136,6 +140,9 @@ import SAWScript.Panic(panic) newtype Prop = Prop Term -- INVARIANT: The type of the given term is `Prop` +instance NFData Prop where + rnf (Prop x) = rnf x + unProp :: Prop -> Term unProp (Prop tm) = tm @@ -318,6 +325,9 @@ data Theorem = | LocalAssumption Prop Pos TheoremNonce -- This constructor is used to construct "hypothetical" theorems that -- are intended to be used in local scopes when proving implications. + deriving Generic + +instance NFData Theorem data TheoremDB = TheoremDB @@ -380,6 +390,10 @@ data TheoremSummary = AdmittedTheorem Text | TestedTheorem Integer | ProvedTheorem SolverStats + deriving Generic + +instance NFData TheoremSummary + instance Monoid TheoremSummary where mempty = ProvedTheorem mempty @@ -468,6 +482,9 @@ data Evidence -- | This type of evidence is used to modify a goal to prove by applying -- 'hoistIfsInGoal'. | HoistIfsEvidence Evidence + deriving Generic + +instance NFData Evidence -- | The the proposition proved by a given theorem. thmProp :: Theorem -> Prop diff --git a/src/SAWScript/Prover/SolverStats.hs b/src/SAWScript/Prover/SolverStats.hs index 5fb1627d65..ba9bff82bf 100644 --- a/src/SAWScript/Prover/SolverStats.hs +++ b/src/SAWScript/Prover/SolverStats.hs @@ -5,8 +5,12 @@ Maintainer : atomb Stability : provisional -} +{-# LANGUAGE DeriveGeneric #-} + module SAWScript.Prover.SolverStats where +import GHC.Generics +import Control.DeepSeq import Data.Semigroup import Data.Set (Set) import qualified Data.Set as Set @@ -28,7 +32,9 @@ data SolverStats -- be the size of an AIG network, etc. , solverStatsGoalSize :: Integer } - deriving (Show) + deriving (Show, Generic) + +instance NFData SolverStats solverStats :: String -> Integer -> SolverStats solverStats nm sz = SolverStats (Set.singleton nm) sz diff --git a/src/SAWScript/Utils.hs b/src/SAWScript/Utils.hs index b7d57d260c..6cd1bf73ef 100644 --- a/src/SAWScript/Utils.hs +++ b/src/SAWScript/Utils.hs @@ -9,6 +9,7 @@ Stability : provisional {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE LambdaCase #-} @@ -41,6 +42,13 @@ import qualified System.IO.Error as IOE import System.Exit import Text.Printf import Numeric(showFFloat) +import qualified Text.LLVM.AST as L +import qualified Lang.Crucible.CFG.Core as C +import qualified Lang.Crucible.LLVM.MemType as CL +import qualified Lang.Crucible.LLVM.DataLayout as CL +import qualified Lang.Crucible.LLVM.MemModel as CL +import Data.Parameterized.Nonce +import What4.ProgramLoc import qualified Lang.JVM.Codebase as JSS @@ -265,3 +273,26 @@ neNubOrd (hd NE.:| tl) = hd NE.:| loop (Set.singleton hd) tl loop prev (x:xs) | Set.member x prev = loop prev xs | otherwise = x : loop (Set.insert x prev) xs + +-- orphan instances! + +instance NFData CL.MemType where + rnf x = seq x () +instance NFData CL.Ident where + rnf x = seq x () +instance NFData CL.Mutability where + rnf x = seq x () +instance NFData CL.Alignment where + rnf x = seq x () +instance NFData L.Module where + rnf x = seq x () +instance NFData L.Type where + rnf x = seq x () +instance NFData L.Symbol where + rnf x = seq x () +instance NFData ProgramLoc where + rnf ploc = seq ploc () +instance NFData (C.GlobalVar tp) where + rnf var = seq var () +instance NFData (Nonce s tp) where + rnf n = seq n ()