From ab23a226492bff4f2084b16e8e544011cca7636d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 26 Jan 2022 10:15:51 -0500 Subject: [PATCH 1/4] Support building with GHC 9.0 This contains a variety of fixes needed to make the packages in the `saw-script` repo compile with GHC 9.0: * GHC 9.0 implements simplified subsumption (see [here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#simplified-subsumption)). This requires manually eta expanding some function applications to accommodate (see, for instance, the expansions of `getAllLLVM` in `SAWScript.Crucible.LLVM.MethodSpecIR`. * GHC's constraint solver now solves constraints in each top-level group sooner (see [here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#the-order-of-th-splices-is-more-important)). This affects `heapster-saw`, as it uses declaration splices extensively. I did some fairly involved rearranging of data type declarations and TH-generated instances to make everything typecheck. It's not exactly pretty, but it gets the job done. * GHC 9.0 now enables `-Wstar-is-type` in `-Wall`, so this patch replaces some uses of `*` with `Data.Kind.Type` in `saw-core-what4` and `crux-mir-comp`. `Data.Kind` requires the use of GHC 8.0 or later, so this patch also updates the lower bounds on `base` to `>= 4.9` in the appropriate `.cabal` files. (I'm fairly certain that this requirement was already present implicity, but better to be explicit about it.) * The upper version bounds on `base` in `saw-remote-api` were raised to allow it to build with `base-4.15.*`, which is bundled with GHC 9.0. * The `cryptol` submodule was bumped to incorporate the changes from GaloisInc/cryptol#1233, which allow it to build with GHC 9.0. --- README.md | 2 +- crux-mir-comp/crux-mir-comp.cabal | 2 +- .../src/Mir/Compositional/Override.hs | 6 +- crux-mir-comp/src/Mir/Cryptol.hs | 5 +- deps/cryptol | 2 +- heapster-saw/heapster-saw.cabal | 1 + .../src/Verifier/SAW/Heapster/CruUtil.hs | 24 +- .../src/Verifier/SAW/Heapster/Implication.hs | 57 +- .../src/Verifier/SAW/Heapster/Permissions.hs | 1750 +++++++++-------- .../src/Verifier/SAW/Heapster/RustTypes.hs | 80 +- saw-core-what4/saw-core-what4.cabal | 2 +- .../src/Verifier/SAW/Simulator/What4.hs | 7 +- saw-remote-api/saw-remote-api.cabal | 2 +- src/SAWScript/Crucible/LLVM/Builtins.hs | 6 +- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 4 +- src/SAWScript/Crucible/LLVM/X86.hs | 2 +- src/SAWScript/Value.hs | 2 +- 17 files changed, 991 insertions(+), 963 deletions(-) diff --git a/README.md b/README.md index 2b4f7cf1fb..64192769b0 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,7 @@ To build SAWScript and related utilities from source: * Ensure that you have the `cabal` and `ghc` executables in your `PATH`. If you don't already have them, we recommend using `ghcup` to install them: . We recommend - Cabal 3.4 or newer, and GHC 8.8 or 8.10. + Cabal 3.4 or newer, and GHC 8.8, 8.10, or 9.0. * Ensure that you have the C libraries and header files for `terminfo`, which generally comes as part of `ncurses` on most diff --git a/crux-mir-comp/crux-mir-comp.cabal b/crux-mir-comp/crux-mir-comp.cabal index 4b6b14ce87..fbb95ec9f9 100644 --- a/crux-mir-comp/crux-mir-comp.cabal +++ b/crux-mir-comp/crux-mir-comp.cabal @@ -19,7 +19,7 @@ extra-source-files: README.md library default-language: Haskell2010 - build-depends: base >= 4.7 && < 5, + build-depends: base >= 4.9 && < 5, text, prettyprinter >= 1.7.0, crucible, diff --git a/crux-mir-comp/src/Mir/Compositional/Override.hs b/crux-mir-comp/src/Mir/Compositional/Override.hs index 53f4665205..957657a6c3 100644 --- a/crux-mir-comp/src/Mir/Compositional/Override.hs +++ b/crux-mir-comp/src/Mir/Compositional/Override.hs @@ -66,7 +66,7 @@ import Mir.Compositional.MethodSpec type MirOverrideMatcher sym a = forall p rorw rtp args ret. MS.OverrideMatcher' sym MIR rorw (OverrideSim (p sym) sym MIR rtp args ret) a -data MethodSpec = MethodSpec +data MethodSpec = MethodSpec { _msCollectionState :: CollectionState , _msSpec :: MIRMethodSpec } @@ -244,7 +244,7 @@ runSpec cs mh ms = ovrWithBackend $ \bak -> -- TODO: see if we need any other assertions from LLVM OverrideMatcher - -- Handle preconditions and postconditions. + -- Handle preconditions and postconditions. -- Convert preconditions to `osAsserts` forM_ (ms ^. MS.csPreState . MS.csConditions) $ \cond -> do @@ -379,7 +379,7 @@ matchArg sym sc eval allocSpecs shp rv sv = go shp rv sv "" go (TupleShape _ _ flds) rvs (MS.SetupStruct () False svs) = goFields flds rvs svs go (ArrayShape _ _ shp) vec (MS.SetupArray () svs) = case vec of - MirVector_Vector v -> zipWithM_ (go shp) (toList v) svs + MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p go shp rv sv diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 6c07729bb1..e083c18c66 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -19,6 +19,7 @@ import Control.Monad.IO.Class import qualified Data.ByteString as BS import Data.Functor.Const import Data.IORef +import qualified Data.Kind as Kind import Data.Map (Map) import qualified Data.Map as Map import Data.String (fromString) @@ -241,10 +242,10 @@ loadCryptolFunc col sig modulePath name = do cryptolRun sc (Text.unpack fnName) argShps retShp (SAW.ttTerm tt) where - listToCtx :: forall k (f :: k -> *). [Some f] -> Some (Assignment f) + listToCtx :: forall k (f :: k -> Kind.Type). [Some f] -> Some (Assignment f) listToCtx xs = go xs (Some Empty) where - go :: forall k (f :: k -> *). [Some f] -> Some (Assignment f) -> Some (Assignment f) + go :: forall k (f :: k -> Kind.Type). [Some f] -> Some (Assignment f) -> Some (Assignment f) go [] acc = acc go (Some x : xs) (Some acc) = go xs (Some $ acc :> x) diff --git a/deps/cryptol b/deps/cryptol index 08cd609c4c..413788c578 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 08cd609c4c58ebb5a4cd22ad053d8255ce8d1fc5 +Subproject commit 413788c57877aa58b6656eb7757e711e91d499fc diff --git a/heapster-saw/heapster-saw.cabal b/heapster-saw/heapster-saw.cabal index f8ad6390b9..ed87d5fb5a 100644 --- a/heapster-saw/heapster-saw.cabal +++ b/heapster-saw/heapster-saw.cabal @@ -38,6 +38,7 @@ library filepath, language-rust, hobbits ^>= 1.4, + extra, hs-source-dirs: src build-tool-depends: alex:alex, diff --git a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs index aaccef503b..0b527541a6 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/CruUtil.hs @@ -371,8 +371,8 @@ $(mkNuMatching [t| UB.PtrComparisonOperator |]) $(mkNuMatching [t| forall v. NuMatching v => StorageTypeF v |]) $(mkNuMatching [t| StorageType |]) -$(mkNuMatching [t| forall f. NuMatchingAny1 f => UB.UndefinedBehavior f |]) $(mkNuMatching [t| forall f. NuMatchingAny1 f => Poison.Poison f |]) +$(mkNuMatching [t| forall f. NuMatchingAny1 f => UB.UndefinedBehavior f |]) -- $(mkNuMatching [t| forall f. NuMatchingAny1 f => BadBehavior f |]) -- $(mkNuMatching [t| forall f. NuMatchingAny1 f => LLVMSafetyAssertion f |]) $(mkNuMatching [t| forall f. NuMatchingAny1 f => LLVMSideCondition f |]) @@ -390,17 +390,6 @@ instance NuMatchingAny1 (EmptyExprExtension f) where $(mkNuMatching [t| AVXOp1 |]) $(mkNuMatching [t| forall f tp. NuMatchingAny1 f => ExtX86 f tp |]) -$(mkNuMatching [t| forall f tp. NuMatchingAny1 f => - LLVMExtensionExpr f tp |]) - -instance NuMatchingAny1 f => NuMatchingAny1 (LLVMExtensionExpr f) where - nuMatchingAny1Proof = nuMatchingProof - -{- -$(mkNuMatching [t| forall w f tp. NuMatchingAny1 f => LLVMStmt w f tp |]) --} - -$(mkNuMatching [t| forall tp. GlobalVar tp |]) instance NuMatching (Nonce s tp) where nuMatchingProof = unsafeMbTypeRepr @@ -411,6 +400,17 @@ instance Closable (Nonce s tp) where instance Liftable (Nonce s tp) where mbLift = unClosed . mbLift . fmap toClosed +$(mkNuMatching [t| forall tp. GlobalVar tp |]) +$(mkNuMatching [t| forall f tp. NuMatchingAny1 f => + LLVMExtensionExpr f tp |]) + +instance NuMatchingAny1 f => NuMatchingAny1 (LLVMExtensionExpr f) where + nuMatchingAny1Proof = nuMatchingProof + +{- +$(mkNuMatching [t| forall w f tp. NuMatchingAny1 f => LLVMStmt w f tp |]) +-} + instance Closable (BV.BV w) where toClosed = unsafeClose diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index a50a3b9d21..36fc7e28ac 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -37,6 +37,7 @@ import qualified Data.BitVector.Sized as BV import GHC.TypeLits import Control.Lens hiding ((:>), ix) import Control.Applicative +import Control.Monad.Extra (concatMapM) import Control.Monad.State.Strict hiding (ap) import qualified Data.Type.RList as RL @@ -1512,22 +1513,40 @@ idLocalPermImpl = LocalPermImpl $ PermImpl_Done $ LocalImplRet Refl -- type IsLLVMPointerTypeList w ps = RAssign ((:~:) (LLVMPointerType w)) ps -$(mkNuMatching [t| forall a. EqPerm a |]) -$(mkNuMatching [t| forall ps a. NuMatching a => EqProofStep ps a |]) -$(mkNuMatching [t| forall ps a. NuMatching a => EqProof ps a |]) -$(mkNuMatching [t| forall ps_in ps_out. SimplImpl ps_in ps_out |]) -$(mkNuMatching [t| forall ps_in ps_outs. PermImpl1 ps_in ps_outs |]) -$(mkNuMatching [t| forall r bs_pss. NuMatchingAny1 r => MbPermImpls r bs_pss |]) -$(mkNuMatching [t| forall r ps. NuMatchingAny1 r => PermImpl r ps |]) -$(mkNuMatching [t| forall ps_in ps_out. LocalPermImpl ps_in ps_out |]) -$(mkNuMatching [t| forall ps ps'. LocalImplRet ps ps' |]) - instance NuMatchingAny1 EqPerm where nuMatchingAny1Proof = nuMatchingProof instance NuMatchingAny1 (LocalImplRet ps) where nuMatchingAny1Proof = nuMatchingProof +-- Many of these types are mutually recursive. Moreover, Template Haskell +-- declaration splices strictly separate top-level groups, so if we were to +-- write each $(mkNuMatching [t| ... |]) splice individually, the splices +-- involving mutually recursive types would not typecheck. As a result, we +-- must put everything into a single splice so that it forms a single top-level +-- group. +$(concatMapM mkNuMatching + [ [t| forall a. EqPerm a |] + , [t| forall ps a. NuMatching a => EqProofStep ps a |] + , [t| forall ps a. NuMatching a => EqProof ps a |] + , [t| forall ps_in ps_out. SimplImpl ps_in ps_out |] + , [t| forall ps_in ps_outs. PermImpl1 ps_in ps_outs |] + , [t| forall r bs_pss. NuMatchingAny1 r => MbPermImpls r bs_pss |] + , [t| forall r ps. NuMatchingAny1 r => PermImpl r ps |] + , [t| forall ps_in ps_out. LocalPermImpl ps_in ps_out |] + , [t| forall ps ps'. LocalImplRet ps ps' |] + ]) + +-- | A splitting of an existential list of permissions into a prefix, a single +-- variable plus permission, and then a suffix +data DistPermsSplit ps where + DistPermsSplit :: RAssign Proxy ps1 -> RAssign Proxy ps2 -> + DistPerms (ps1 :++: ps2) -> + ExprVar a -> ValuePerm a -> + DistPermsSplit (ps1 :> a :++: ps2) + +$(mkNuMatching [t| forall ps. DistPermsSplit ps |]) + -- | Compile-time flag for whether to prune failure branches in 'implCatchM' pruneFailingBranches :: Bool @@ -6245,7 +6264,7 @@ proveVarLLVMArrayH x first_p _ ps mb_ap = -- | Prove an array permission by proving its first cell and then its remaining -- cells and appending them together -proveVarLLVMArray_FromHead :: +proveVarLLVMArray_FromHead :: (1 <= w, KnownNat w, NuMatchingAny1 r) => ExprVar (LLVMPointerType w) -> Mb vars (LLVMArrayPerm w) -> ImplM vars s r (ps :> LLVMPointerType w) ps () @@ -7063,7 +7082,7 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps -- Prove the corresponding field permission proveVarImplInt x (mbValPerm_LLVMField mb_fp) >>> getTopDistPerm x >>>= \(ValPerm_LLVMField fp) -> - + -- Finally, convert the field perm to a block and move it into position implSimplM Proxy (SImpl_IntroLLVMBlockField x fp) >>> implSwapInsertConjM x (Perm_LLVMBlock $ llvmFieldPermToBlock fp) ps' 0 @@ -7081,7 +7100,7 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps proveVarImplInt x (mbMapCl $(mkClosed [| ValPerm_LLVMArray . fromJust . llvmBlockPermToArray |]) mb_bp) >>> getTopDistPerm x >>>= \(ValPerm_LLVMArray ap) -> - + -- Finally, convert the array perm to a block and move it into position implSimplM Proxy (SImpl_IntroLLVMBlockArray x ap) >>> implSwapInsertConjM x (Perm_LLVMBlock $ fromJust $ @@ -7124,7 +7143,7 @@ proveVarLLVMBlocks2 x ps psubst mb_bp mb_sh mb_bps -- If proving a tagged union shape, first prove an equality permission for the --- tag and then use that equality permission to +-- tag and then use that equality permission to proveVarLLVMBlocks2 x ps psubst mb_bp _ mb_bps | Just [nuP| SomeTaggedUnionShape mb_tag_u |] <- mbLLVMBlockToTaggedUnion mb_bp , mb_shs <- mbTaggedUnionDisjs mb_tag_u @@ -8125,14 +8144,6 @@ funPermExDistIns fun_perm args = fmap (varSubst (permVarSubstOfNames args)) $ mbSeparate args $ mbValuePermsToDistPerms $ funPermIns fun_perm --- | A splitting of an existential list of permissions into a prefix, a single --- variable plus permission, and then a suffix -data DistPermsSplit ps where - DistPermsSplit :: RAssign Proxy ps1 -> RAssign Proxy ps2 -> - DistPerms (ps1 :++: ps2) -> - ExprVar a -> ValuePerm a -> - DistPermsSplit (ps1 :> a :++: ps2) - -- | Make a "base case" 'DistPermsSplit' where the split is at the end baseDistPermsSplit :: DistPerms ps -> ExprVar a -> ValuePerm a -> DistPermsSplit (ps :> a) @@ -8418,5 +8429,3 @@ proveVarsImplVarEVars mb_ps = proveVarImpl :: NuMatchingAny1 r => ExprVar a -> Mb vars (ValuePerm a) -> ImplM vars s r (ps :> a) ps () proveVarImpl x mb_p = proveVarsImplAppend $ fmap (distPerms1 x) mb_p - -$(mkNuMatching [t| forall ps. DistPermsSplit ps |]) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 1d214983dc..cdd6dda041 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -93,6 +93,801 @@ import GHC.Stack import Debug.Trace +---------------------------------------------------------------------- +-- * Data types and related types +---------------------------------------------------------------------- + +-- | The Haskell type of expression variables +type ExprVar = (Name :: CrucibleType -> Type) + +-- | Crucible type for lifetimes; we give them a Crucible type so they can be +-- existentially bound in the same way as other Crucible objects +type LifetimeType = IntrinsicType "Lifetime" EmptyCtx + +-- | Crucible type for read/write modalities; we give them a Crucible type so +-- they can be used as variables in recursive permission definitions +type RWModalityType = IntrinsicType "RWModality" EmptyCtx + +-- | Crucible type for lists of expressions and permissions on them +type PermListType = IntrinsicType "PermList" EmptyCtx + +-- | Crucible type for LLVM stack frame objects +type LLVMFrameType w = IntrinsicType "LLVMFrame" (EmptyCtx ::> BVType w) + +-- | Crucible type for value permissions themselves +type ValuePermType a = IntrinsicType "Perm" (EmptyCtx ::> a) + +-- | Crucible type for LLVM shapes +type LLVMShapeType w = IntrinsicType "LLVMShape" (EmptyCtx ::> BVType w) + +-- | Crucible type for LLVM memory blocks +type LLVMBlockType w = IntrinsicType "LLVMBlock" (EmptyCtx ::> BVType w) + +-- | Expressions that are considered "pure" for use in permissions. Note that +-- these are in a normal form, that makes them easier to analyze. +data PermExpr (a :: CrucibleType) where + -- | A variable of any type + PExpr_Var :: ExprVar a -> PermExpr a + + -- | A unit literal + PExpr_Unit :: PermExpr UnitType + + -- | A literal Boolean number + PExpr_Bool :: Bool -> PermExpr BoolType + + -- | A literal natural number + PExpr_Nat :: Natural -> PermExpr NatType + + -- | A literal string + PExpr_String :: String -> PermExpr (StringType Unicode) + + -- | A bitvector expression is a linear expression in @N@ variables, i.e., sum + -- of constant times variable factors plus a constant + -- + -- FIXME: make the offset a 'Natural' + PExpr_BV :: (1 <= w, KnownNat w) => + [BVFactor w] -> BV w -> PermExpr (BVType w) + + -- | A struct expression is an expression for each argument of the struct type + PExpr_Struct :: PermExprs (CtxToRList args) -> PermExpr (StructType args) + + -- | The @always@ lifetime that is always current + PExpr_Always :: PermExpr LifetimeType + + -- | An LLVM value that represents a word, i.e., whose region identifier is 0 + PExpr_LLVMWord :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> + PermExpr (LLVMPointerType w) + + -- | An LLVM value built by adding an offset to an LLVM variable + PExpr_LLVMOffset :: (1 <= w, KnownNat w) => + ExprVar (LLVMPointerType w) -> + PermExpr (BVType w) -> + PermExpr (LLVMPointerType w) + + -- | A literal function pointer + PExpr_Fun :: FnHandle args ret -> PermExpr (FunctionHandleType args ret) + + -- | An empty permission list + PExpr_PermListNil :: PermExpr PermListType + + -- | A cons of an expression and a permission on it to a permission list + PExpr_PermListCons :: TypeRepr a -> PermExpr a -> ValuePerm a -> + PermExpr PermListType -> PermExpr PermListType + + -- | A read/write modality + PExpr_RWModality :: RWModality -> PermExpr RWModalityType + + -- | The empty / vacuously true shape + PExpr_EmptyShape :: PermExpr (LLVMShapeType w) + + -- | A named shape along with arguments for it, with optional read/write and + -- lifetime modalities that are applied to the body of the shape + PExpr_NamedShape :: KnownNat w => Maybe (PermExpr RWModalityType) -> + Maybe (PermExpr LifetimeType) -> + NamedShape b args w -> PermExprs args -> + PermExpr (LLVMShapeType w) + + -- | The equality shape + PExpr_EqShape :: PermExpr (LLVMBlockType w) -> PermExpr (LLVMShapeType w) + + -- | A shape for a pointer to another memory block, i.e., a @memblock@ + -- permission, with a given shape. This @memblock@ permission will have the + -- same read/write and lifetime modalities as the @memblock@ permission + -- containing this pointer shape, unless they are specifically overridden by + -- the pointer shape; i.e., we have that + -- + -- > [l]memblock(rw,off,len,ptrsh(rw',l',sh)) = + -- > [l]memblock(rw,off,len,fieldsh([l']memblock(rw',0,len(sh),sh))) + -- + -- where @rw'@ and/or @l'@ can be 'Nothing', in which case they default to + -- @rw@ and @l@, respectively. + PExpr_PtrShape :: Maybe (PermExpr RWModalityType) -> + Maybe (PermExpr LifetimeType) -> + PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w) + + -- | A shape for a single field with a given permission + PExpr_FieldShape :: (1 <= w, KnownNat w) => LLVMFieldShape w -> + PermExpr (LLVMShapeType w) + + -- | A shape for an array of @len@ individual regions of memory, called "array + -- cells"; the size of each cell in bytes is given by the array stride, which + -- must be known statically, and each cell has shape given by the supplied + -- LLVM shape, also called the cell shape + PExpr_ArrayShape :: (1 <= w, KnownNat w) => + PermExpr (BVType w) -> Bytes -> + PermExpr (LLVMShapeType w) -> + PermExpr (LLVMShapeType w) + + -- | A sequence of two shapes + PExpr_SeqShape :: PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w) -> + PermExpr (LLVMShapeType w) + + -- | A disjunctive shape + PExpr_OrShape :: PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w) -> + PermExpr (LLVMShapeType w) + + -- | An existential shape + PExpr_ExShape :: KnownRepr TypeRepr a => + Binding a (PermExpr (LLVMShapeType w)) -> + PermExpr (LLVMShapeType w) + + -- | A false shape + PExpr_FalseShape :: PermExpr (LLVMShapeType w) + + -- | A permission as an expression + PExpr_ValPerm :: ValuePerm a -> PermExpr (ValuePermType a) + +-- | A sequence of permission expressions +type PermExprs = RAssign PermExpr + +{- +data PermExprs (as :: RList CrucibleType) where + PExprs_Nil :: PermExprs RNil + PExprs_Cons :: PermExprs as -> PermExpr a -> PermExprs (as :> a) +-} + +-- | A bitvector variable, possibly multiplied by a constant +data BVFactor w where + -- | A variable of type @'BVType' w@ multiplied by a constant @i@, which + -- should be in the range @0 <= i < 2^w@ + BVFactor :: (1 <= w, KnownNat w) => BV w -> ExprVar (BVType w) -> + BVFactor w + +-- | Whether a permission allows reads or writes +data RWModality + = Write + | Read + deriving Eq + +-- | The Haskell type of permission variables, that is, variables that range +-- over 'ValuePerm's +type PermVar (a :: CrucibleType) = Name (ValuePermType a) + +-- | Ranges @[off,off+len)@ of bitvector values @x@ equal to @off+y@ for some +-- unsigned @y < len@. Note that ranges are allowed to wrap around 0, meaning +-- @off+y@ can overflow when testing whether @x@ is in the range. Thus, @x@ is +-- in range @[off,off+len)@ iff @x-off@ is unsigned less than @len@. +data BVRange w = BVRange { bvRangeOffset :: PermExpr (BVType w), + bvRangeLength :: PermExpr (BVType w) } + +-- | Propositions about bitvectors +data BVProp w + -- | True iff the two expressions are equal + = BVProp_Eq (PermExpr (BVType w)) (PermExpr (BVType w)) + -- | True iff the two expressions are not equal + | BVProp_Neq (PermExpr (BVType w)) (PermExpr (BVType w)) + -- | True iff the first expression is unsigned less-than the second + | BVProp_ULt (PermExpr (BVType w)) (PermExpr (BVType w)) + -- | True iff the first expression is unsigned @<=@ the second + | BVProp_ULeq (PermExpr (BVType w)) (PermExpr (BVType w)) + -- | True iff the first expression is unsigned @<=@ the difference of the + -- second minus the third + | (1 <= w, KnownNat w) => + BVProp_ULeq_Diff (PermExpr (BVType w)) (PermExpr (BVType w)) + (PermExpr (BVType w)) + +-- | An atomic permission is a value permission that is not one of the compound +-- constructs in the 'ValuePerm' type; i.e., not a disjunction, existential, +-- recursive, or equals permission. These are the permissions that we can put +-- together with separating conjuctions. +data AtomicPerm (a :: CrucibleType) where + -- | Gives permissions to a single field pointed to by an LLVM pointer + Perm_LLVMField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) => + LLVMFieldPerm w sz -> + AtomicPerm (LLVMPointerType w) + + -- | Gives permissions to an array pointer to by an LLVM pointer + Perm_LLVMArray :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> + AtomicPerm (LLVMPointerType w) + + -- | Gives read or write access to a memory block, whose contents also give + -- some permissions + Perm_LLVMBlock :: (1 <= w, KnownNat w) => LLVMBlockPerm w -> + AtomicPerm (LLVMPointerType w) + + -- | Says that we have permission to free the memory pointed at by this + -- pointer if we have write permission to @e@ words of size @w@ + Perm_LLVMFree :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> + AtomicPerm (LLVMPointerType w) + + -- | Says that we known an LLVM value is a function pointer whose function has + -- the given permissions + Perm_LLVMFunPtr :: (1 <= w, KnownNat w) => + TypeRepr (FunctionHandleType cargs ret) -> + ValuePerm (FunctionHandleType cargs ret) -> + AtomicPerm (LLVMPointerType w) + + -- | Says that a memory block has a given shape + Perm_LLVMBlockShape :: (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w) -> + AtomicPerm (LLVMBlockType w) + + -- | Says we know an LLVM value is a pointer value, meaning that its block + -- value is non-zero. Note that this does not say the pointer is allocated. + Perm_IsLLVMPtr :: (1 <= w, KnownNat w) => + AtomicPerm (LLVMPointerType w) + + -- | A named conjunctive permission + Perm_NamedConj :: NameSortIsConj ns ~ 'True => + NamedPermName ns args a -> PermExprs args -> + PermOffset a -> AtomicPerm a + + -- | Permission to allocate (via @alloca@) on an LLVM stack frame, and + -- permission to delete that stack frame if we have exclusive permissions to + -- all the given LLVM pointer objects + Perm_LLVMFrame :: (1 <= w, KnownNat w) => LLVMFramePerm w -> + AtomicPerm (LLVMFrameType w) + + -- | Ownership permission for a lifetime, including an assertion that it is + -- still current and permission to end that lifetime. A lifetime also + -- represents a permission "borrow" of some sub-permissions out of some larger + -- permissions. For example, we might borrow a portion of an array, or a + -- portion of a larger data structure. When the lifetime is ended, you have to + -- give back to sub-permissions to get back the larger permissions. Together, + -- these are a form of permission implication, so we write lifetime ownership + -- permissions as @lowned(Pin -o Pout)@. Intuitively, @Pin@ must be given back + -- before the lifetime is ended, and @Pout@ is returned afterwards. + -- Additionally, a lifetime may contain some other lifetimes, meaning the all + -- must end before the current one can be ended. + Perm_LOwned :: [PermExpr LifetimeType] -> + LOwnedPerms ps_in -> LOwnedPerms ps_out -> + AtomicPerm LifetimeType + + -- | Assertion that a lifetime is current during another lifetime + Perm_LCurrent :: PermExpr LifetimeType -> AtomicPerm LifetimeType + + -- | Assertion that a lifetime has finished + Perm_LFinished :: AtomicPerm LifetimeType + + -- | A struct permission = a sequence of permissions for each field + Perm_Struct :: RAssign ValuePerm (CtxToRList ctx) -> + AtomicPerm (StructType ctx) + + -- | A function permission + Perm_Fun :: FunPerm ghosts (CtxToRList cargs) gouts ret -> + AtomicPerm (FunctionHandleType cargs ret) + + -- | An LLVM permission that asserts a proposition about bitvectors + Perm_BVProp :: (1 <= w, KnownNat w) => BVProp w -> + AtomicPerm (LLVMPointerType w) + +-- | A value permission is a permission to do something with a value, such as +-- use it as a pointer. This also includes a limited set of predicates on values +-- (you can think about this as "permission to assume the value satisfies this +-- predicate" if you like). +data ValuePerm (a :: CrucibleType) where + + -- | Says that a value is equal to a known static expression + ValPerm_Eq :: PermExpr a -> ValuePerm a + + -- | The disjunction of two value permissions + ValPerm_Or :: ValuePerm a -> ValuePerm a -> ValuePerm a + + -- | An existential binding of a value in a value permission + -- + -- FIXME: turn the 'KnownRepr' constraint into a normal 'TypeRepr' argument + ValPerm_Exists :: KnownRepr TypeRepr a => + Binding a (ValuePerm b) -> + ValuePerm b + + -- | A named permission + ValPerm_Named :: NamedPermName ns args a -> PermExprs args -> + PermOffset a -> ValuePerm a + + -- | A permission variable plus an offset + ValPerm_Var :: PermVar a -> PermOffset a -> ValuePerm a + + -- | A separating conjuction of 0 or more atomic permissions, where 0 + -- permissions is the trivially true permission + ValPerm_Conj :: [AtomicPerm a] -> ValuePerm a + + -- | The false value permission + ValPerm_False :: ValuePerm a + +-- | A sequence of value permissions +{- +data ValuePerms as where + ValPerms_Nil :: ValuePerms RNil + ValPerms_Cons :: ValuePerms as -> ValuePerm a -> ValuePerms (as :> a) +-} + +type ValuePerms = RAssign ValuePerm + +-- | A binding of 0 or more variables, each with permissions +type MbValuePerms ctx = Mb ctx (ValuePerms ctx) + +-- | A frame permission is a list of the pointers that have been allocated in +-- the frame and their corresponding allocation sizes in words of size +-- @w@. Write permissions of the given sizes are required to these pointers in +-- order to delete the frame. +type LLVMFramePerm w = [(PermExpr (LLVMPointerType w), Integer)] + +-- | A permission for a pointer to a specific field of a given size +data LLVMFieldPerm w sz = + LLVMFieldPerm { llvmFieldRW :: PermExpr RWModalityType, + -- ^ Whether this is a read or write permission + llvmFieldLifetime :: PermExpr LifetimeType, + -- ^ The lifetime during which this field permission is active + llvmFieldOffset :: PermExpr (BVType w), + -- ^ The offset from the pointer in bytes of this field + llvmFieldContents :: ValuePerm (LLVMPointerType sz) + -- ^ The permissions we get for the value read from this field + } + +-- | Helper type to represent byte offsets +-- +-- > stride * ix + off +-- +-- from the beginning of an array permission. Such an expression refers to +-- offset @off@, which must be a statically-known constant, in array cell @ix@. +data LLVMArrayIndex w = + LLVMArrayIndex { llvmArrayIndexCell :: PermExpr (BVType w), + llvmArrayIndexOffset :: BV w } + +-- | A permission to an array of @len@ individual regions of memory, called +-- "array cells". The size of each cell in bytes is given by the array /stride/, +-- which must be known statically, and each cell has shape given by the supplied +-- LLVM shape, also called the cell shape. +data LLVMArrayPerm w = + LLVMArrayPerm { llvmArrayRW :: PermExpr RWModalityType, + -- ^ Whether this array gives read or write access + llvmArrayLifetime :: PermExpr LifetimeType, + -- ^ The lifetime during which this array permission is valid + llvmArrayOffset :: PermExpr (BVType w), + -- ^ The offset from the pointer in bytes of this array + llvmArrayLen :: PermExpr (BVType w), + -- ^ The number of array blocks + llvmArrayStride :: Bytes, + -- ^ The array stride in bytes + llvmArrayCellShape :: PermExpr (LLVMShapeType w), + -- ^ The shape of each cell in the array + llvmArrayBorrows :: [LLVMArrayBorrow w] + -- ^ Indices or index ranges that are missing from this array + } + +-- | An index or range of indices that are missing from an array perm +-- +-- FIXME: think about calling the just @LLVMArrayIndexSet@ +data LLVMArrayBorrow w + = FieldBorrow (PermExpr (BVType w)) + -- ^ Borrow a specific cell of an array permission + | RangeBorrow (BVRange w) + -- ^ Borrow a range of array cells, where each cell is 'llvmArrayStride' + -- bytes long + +-- | An LLVM block permission is read or write access to the memory at a given +-- offset with a given length with a given shape +data LLVMBlockPerm w = + LLVMBlockPerm { llvmBlockRW :: PermExpr RWModalityType, + -- ^ Whether this is a read or write block permission + llvmBlockLifetime :: PermExpr LifetimeType, + -- ^ The lifetime during with this block permission is active + llvmBlockOffset :: PermExpr (BVType w), + -- ^ The offset of the block from the pointer in bytes + llvmBlockLen :: PermExpr (BVType w), + -- ^ The length of the block in bytes + llvmBlockShape :: PermExpr (LLVMShapeType w) + -- ^ The shape of the permissions in the block + } + +-- | An LLVM shape for a single pointer field of unknown size +data LLVMFieldShape w = + forall sz. (1 <= sz, KnownNat sz) => + LLVMFieldShape (ValuePerm (LLVMPointerType sz)) + +-- | A form of permission used in lifetime ownership permissions +data LOwnedPerm a where + LOwnedPermField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) => + PermExpr (LLVMPointerType w) -> LLVMFieldPerm w sz -> + LOwnedPerm (LLVMPointerType w) + LOwnedPermArray :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) -> + LLVMArrayPerm w -> LOwnedPerm (LLVMPointerType w) + LOwnedPermBlock :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) -> + LLVMBlockPerm w -> LOwnedPerm (LLVMPointerType w) + +-- | A sequence of 'LOwnedPerm's +type LOwnedPerms = RAssign LOwnedPerm + +-- | A function permission is a set of input and output permissions inside a +-- context of ghost variables @ghosts@ with an additional context of output +-- ghost variables @gouts@ +data FunPerm ghosts args gouts ret where + FunPerm :: CruCtx ghosts -> CruCtx args -> CruCtx gouts -> TypeRepr ret -> + MbValuePerms (ghosts :++: args) -> + MbValuePerms ((ghosts :++: args) :++: gouts :> ret) -> + FunPerm ghosts args gouts ret + +-- | A function permission that existentially quantifies the ghost types +data SomeFunPerm args ret where + SomeFunPerm :: FunPerm ghosts args gouts ret -> SomeFunPerm args ret + +-- | The different sorts of name, each of which comes with a 'Bool' flag +-- indicating whether the name can be used as an atomic permission. A recursive +-- sort also comes with a second flag indicating whether it is a reachability +-- permission. +data NameSort = DefinedSort Bool | OpaqueSort Bool | RecursiveSort Bool Bool + +type DefinedSort = 'DefinedSort +type OpaqueSort = 'OpaqueSort +type RecursiveSort = 'RecursiveSort + +-- | Test whether a name of a given 'NameSort' is conjoinable +type family NameSortIsConj (ns::NameSort) :: Bool where + NameSortIsConj (DefinedSort b) = b + NameSortIsConj (OpaqueSort b) = b + NameSortIsConj (RecursiveSort b _) = b + +-- | Test whether a name of a given 'NameSort' is a reachability permission +type family IsReachabilityName (ns::NameSort) :: Bool where + IsReachabilityName (DefinedSort _) = 'False + IsReachabilityName (OpaqueSort _) = 'False + IsReachabilityName (RecursiveSort _ reach) = reach + +-- | A singleton representation of 'NameSort' +data NameSortRepr (ns::NameSort) where + DefinedSortRepr :: BoolRepr b -> NameSortRepr (DefinedSort b) + OpaqueSortRepr :: BoolRepr b -> NameSortRepr (OpaqueSort b) + RecursiveSortRepr :: BoolRepr b -> BoolRepr reach -> + NameSortRepr (RecursiveSort b reach) + +-- | A constraint that the last argument of a reachability permission is a +-- permission argument +data NameReachConstr ns args a where + NameReachConstr :: (IsReachabilityName ns ~ 'True) => + NameReachConstr ns (args :> a) a + NameNonReachConstr :: (IsReachabilityName ns ~ 'False) => + NameReachConstr ns args a + +-- | A name for a named permission +data NamedPermName ns args a = NamedPermName { + namedPermNameName :: String, + namedPermNameType :: TypeRepr a, + namedPermNameArgs :: CruCtx args, + namedPermNameSort :: NameSortRepr ns, + namedPermNameReachConstr :: NameReachConstr ns args a + } + +-- | An existentially quantified 'NamedPermName' +data SomeNamedPermName where + SomeNamedPermName :: NamedPermName ns args a -> SomeNamedPermName + +-- | A named LLVM shape is a name, a list of arguments, and a body, where the +-- Boolean flag @b@ determines whether the shape can be unfolded or not +data NamedShape b args w = NamedShape { + namedShapeName :: String, + namedShapeArgs :: CruCtx args, + namedShapeBody :: NamedShapeBody b args w + } + +data NamedShapeBody b args w where + -- | A defined shape is just a definition in terms of the arguments + DefinedShapeBody :: Mb args (PermExpr (LLVMShapeType w)) -> + NamedShapeBody 'True args w + + -- | An opaque shape has no body, just a length and a translation to a type + OpaqueShapeBody :: Mb args (PermExpr (BVType w)) -> Ident -> + NamedShapeBody 'False args w + + -- | A recursive shape body has a one-step unfolding to a shape, which can + -- refer to the shape itself via the last bound variable; it also has + -- identifiers for the type it is translated to, along with fold and unfold + -- functions for mapping to and from this type. The fold and unfold functions + -- can be undefined if we are in the process of defining this recusive shape. + RecShapeBody :: Mb (args :> LLVMShapeType w) (PermExpr (LLVMShapeType w)) -> + Ident -> Maybe (Ident, Ident) -> + NamedShapeBody 'True args w + +-- | An offset that is added to a permission. Only makes sense for llvm +-- permissions (at least for now...?) +data PermOffset a where + NoPermOffset :: PermOffset a + -- | NOTE: the invariant is that the bitvector offset is non-zero + LLVMPermOffset :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> + PermOffset (LLVMPointerType w) + +-- | The semantics of a named permission, which can can either be an opaque +-- named permission, a recursive named permission, a defined permission, or an +-- LLVM shape +data NamedPerm ns args a where + NamedPerm_Opaque :: OpaquePerm b args a -> NamedPerm (OpaqueSort b) args a + NamedPerm_Rec :: RecPerm b reach args a -> + NamedPerm (RecursiveSort b reach) args a + NamedPerm_Defined :: DefinedPerm b args a -> NamedPerm (DefinedSort b) args a + +-- | An opaque named permission is just a name and a SAW core type given by +-- identifier that it is translated to +data OpaquePerm b args a = OpaquePerm { + opaquePermName :: NamedPermName (OpaqueSort b) args a, + opaquePermTrans :: Ident + } + +-- | The interpretation of a recursive permission as a reachability permission. +-- Reachability permissions are recursive permissions of the form +-- +-- > reach = eq(x) | p +-- +-- where @reach@ occurs exactly once in @p@ in the form @reach@ and @x@ +-- does not occur at all in @p@. This means their interpretations look like a +-- list type, where the @eq(x)@ is the nil constructor and the @p@ is the +-- cons. To support the transitivity rule, we need an append function for these +-- lists, which is given by the transitivity method listed here, which has type +-- +-- > trans : forall args (x y:A), t args x -> t args y -> t args y +-- +-- where @args@ are the arguments and @A@ is the translation of type @a@ (which +-- may correspond to 0 or more arguments) +data ReachMethods reach args a where + ReachMethods :: { + reachMethodTrans :: Ident + } -> ReachMethods (args :> a) a 'True + NoReachMethods :: ReachMethods args a 'False + +-- | A recursive permission is a disjunction of 1 or more permissions, each of +-- which can contain the recursive permission itself. NOTE: it is an error to +-- have an empty list of cases. A recursive permission is also associated with a +-- SAW datatype, given by a SAW 'Ident', and each disjunctive permission case is +-- associated with a constructor of that datatype. The @b@ flag indicates +-- whether this recursive permission can be used as an atomic permission, which +-- should be 'True' iff all of the cases are conjunctive permissions as in +-- 'isConjPerm'. If the recursive permission is a reachability permission, then +-- it also has a 'ReachMethods' structure. +data RecPerm b reach args a = RecPerm { + recPermName :: NamedPermName (RecursiveSort b reach) args a, + recPermTransType :: Ident, + recPermFoldFun :: Ident, + recPermUnfoldFun :: Ident, + recPermReachMethods :: ReachMethods args a reach, + recPermCases :: [Mb args (ValuePerm a)] + } + +-- | A defined permission is a name and a permission to which it is +-- equivalent. The @b@ flag indicates whether this permission can be used as an +-- atomic permission, which should be 'True' iff the associated permission is a +-- conjunctive permission as in 'isConjPerm'. +data DefinedPerm b args a = DefinedPerm { + definedPermName :: NamedPermName (DefinedSort b) args a, + definedPermDef :: Mb args (ValuePerm a) +} + +-- | A pair of a variable and its permission; we give it its own datatype to +-- make certain typeclass instances (like pretty-printing) specific to it +data VarAndPerm a = VarAndPerm (ExprVar a) (ValuePerm a) + +-- | A list of "distinguished" permissions to named variables +-- FIXME: just call these VarsAndPerms or something like that... +type DistPerms = RAssign VarAndPerm + +-- | A special-purpose 'DistPerms' that specifies a list of permissions needed +-- to prove that a lifetime is current +data LifetimeCurrentPerms ps_l where + -- | The @always@ lifetime needs no proof that it is current + AlwaysCurrentPerms :: LifetimeCurrentPerms RNil + -- | A variable @l@ that is @lowned@ is current, requiring perms + -- + -- > l:lowned[ls](ps_in -o ps_out) + LOwnedCurrentPerms :: ExprVar LifetimeType -> [PermExpr LifetimeType] -> + LOwnedPerms ps_in -> LOwnedPerms ps_out -> + LifetimeCurrentPerms (RNil :> LifetimeType) + + -- | A variable @l@ that is @lcurrent@ during another lifetime @l'@ is + -- current, i.e., if @ps@ ensure @l'@ is current then we need perms + -- + -- > ps, l:lcurrent(l') + CurrentTransPerms :: LifetimeCurrentPerms ps_l -> ExprVar LifetimeType -> + LifetimeCurrentPerms (ps_l :> LifetimeType) + +-- | A lifetime functor is a function from a lifetime plus a set of 0 or more +-- rwmodalities to a permission that satisfies a number of properties discussed +-- in Issue #62 (FIXME: copy those here). Rather than try to enforce these +-- properties, we syntactically restrict lifetime functors to one of a few forms +-- that are guaranteed to satisfy the properties. The @args@ type lists all +-- arguments (which should all be rwmodalities) other than the lifetime +-- argument. +data LifetimeFunctor args a where + -- | The functor @\(l,rw) -> [l]ptr((rw,off) |-> p)@ + LTFunctorField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) => + PermExpr (BVType w) -> ValuePerm (LLVMPointerType sz) -> + LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w) + + -- | The functor @\(l,rw) -> [l]array(rw,off, PermExpr (BVType w) -> + PermExpr (BVType w) -> Bytes -> + PermExpr (LLVMShapeType w) -> [LLVMArrayBorrow w] -> + LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w) + + -- | The functor @\(l,rw) -> [l]memblock(rw,off,len,sh) + LTFunctorBlock :: (1 <= w, KnownNat w) => + PermExpr (BVType w) -> PermExpr (BVType w) -> + PermExpr (LLVMShapeType w) -> + LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w) + + -- FIXME: add functors for arrays and named permissions + +-- | An 'LLVMBlockPerm' with a proof that its type is valid +data SomeLLVMBlockPerm a where + SomeLLVMBlockPerm :: (1 <= w, KnownNat w) => LLVMBlockPerm w -> + SomeLLVMBlockPerm (LLVMPointerType w) + +-- | A block permission in a binding at some unknown type +data SomeBindingLLVMBlockPerm w = + forall a. SomeBindingLLVMBlockPerm (Binding a (LLVMBlockPerm w)) + +-- | A tagged union shape is a shape of the form +-- +-- > sh1 orsh sh2 orsh ... orsh shn +-- +-- where each @shi@ is equivalent up to associativity of the @;@ operator to a +-- shape of the form +-- +-- > fieldsh(eq(llvmword(bvi)));shi' +-- +-- That is, each disjunct of the shape starts with an equality permission that +-- determines which disjunct should be used. These shapes are represented as a +-- list of the disjuncts, which are tagged with the bitvector values @bvi@ used +-- in the equality permission. +data TaggedUnionShape w sz + = TaggedUnionShape (NonEmpty (BV sz, PermExpr (LLVMShapeType w))) + +-- | A 'TaggedUnionShape' with existentially quantified tag size +data SomeTaggedUnionShape w + = forall sz. (1 <= sz, KnownNat sz) => + SomeTaggedUnionShape (TaggedUnionShape w sz) + +-- | Like a substitution but assigns variables instead of arbitrary expressions +-- to bound variables +data PermVarSubst (ctx :: RList CrucibleType) where + PermVarSubst_Nil :: PermVarSubst RNil + PermVarSubst_Cons :: PermVarSubst ctx -> Name tp -> PermVarSubst (ctx :> tp) + +-- | An entry in a permission environment that associates a permission and +-- corresponding SAW identifier with a Crucible function handle +data PermEnvFunEntry where + PermEnvFunEntry :: args ~ CtxToRList cargs => FnHandle cargs ret -> + FunPerm ghosts args gouts ret -> Ident -> + PermEnvFunEntry + +-- | An existentially quantified 'NamedPerm' +data SomeNamedPerm where + SomeNamedPerm :: NamedPerm ns args a -> SomeNamedPerm + +-- | An existentially quantified LLVM shape with arguments +data SomeNamedShape where + SomeNamedShape :: (1 <= w, KnownNat w) => NamedShape b args w -> + SomeNamedShape + +-- | An entry in a permission environment that associates a 'GlobalSymbol' with +-- a permission and a translation of that permission +data PermEnvGlobalEntry where + PermEnvGlobalEntry :: (1 <= w, KnownNat w) => GlobalSymbol -> + ValuePerm (LLVMPointerType w) -> [OpenTerm] -> + PermEnvGlobalEntry + +-- | The different sorts hints for blocks +data BlockHintSort args where + -- | This hint specifies the ghost args and input permissions for a block + BlockEntryHintSort :: + CruCtx top_args -> CruCtx ghosts -> + MbValuePerms ((top_args :++: CtxToRList args) :++: ghosts) -> + BlockHintSort args + + -- | This hint says that the input perms for a block should be generalized + GenPermsHintSort :: BlockHintSort args + + -- | This hint says that a block should be a join point + JoinPointHintSort :: BlockHintSort args + +-- | A hint for a block +data BlockHint blocks init ret args where + BlockHint :: FnHandle init ret -> Assignment CtxRepr blocks -> + BlockID blocks args -> BlockHintSort args -> + BlockHint blocks init ret args + +-- | A "hint" from the user for type-checking +data Hint where + Hint_Block :: BlockHint blocks init ret args -> Hint + +-- | A permission environment that maps function names, permission names, and +-- 'GlobalSymbols' to their respective permission structures +data PermEnv = PermEnv { + permEnvFunPerms :: [PermEnvFunEntry], + permEnvNamedPerms :: [SomeNamedPerm], + permEnvNamedShapes :: [SomeNamedShape], + permEnvGlobalSyms :: [PermEnvGlobalEntry], + permEnvHints :: [Hint] + } + + +---------------------------------------------------------------------- +-- * Template Haskell–generated instances +---------------------------------------------------------------------- + +instance NuMatchingAny1 PermExpr where + nuMatchingAny1Proof = nuMatchingProof + +instance NuMatchingAny1 ValuePerm where + nuMatchingAny1Proof = nuMatchingProof + +instance NuMatchingAny1 VarAndPerm where + nuMatchingAny1Proof = nuMatchingProof + +instance NuMatchingAny1 LOwnedPerm where + nuMatchingAny1Proof = nuMatchingProof + +instance NuMatchingAny1 DistPerms where + nuMatchingAny1Proof = nuMatchingProof + +$(mkNuMatching [t| forall a . BVFactor a |]) +$(mkNuMatching [t| RWModality |]) +$(mkNuMatching [t| forall b args w. NamedShapeBody b args w |]) +$(mkNuMatching [t| forall b args w. NamedShape b args w |]) +$(mkNuMatching [t| forall w . LLVMFieldShape w |]) +$(mkNuMatching [t| forall a . PermExpr a |]) +$(mkNuMatching [t| forall w. BVRange w |]) +$(mkNuMatching [t| forall w. BVProp w |]) +$(mkNuMatching [t| forall w sz . LLVMFieldPerm w sz |]) +$(mkNuMatching [t| forall w . LLVMArrayBorrow w |]) +$(mkNuMatching [t| forall w . LLVMArrayPerm w |]) +$(mkNuMatching [t| forall w . LLVMBlockPerm w |]) +$(mkNuMatching [t| forall ns. NameSortRepr ns |]) +$(mkNuMatching [t| forall ns args a. NameReachConstr ns args a |]) +$(mkNuMatching [t| forall ns args a. NamedPermName ns args a |]) +$(mkNuMatching [t| forall a. PermOffset a |]) +$(mkNuMatching [t| forall w . LOwnedPerm w |]) +$(mkNuMatching [t| forall ghosts args gouts ret. FunPerm ghosts args gouts ret |]) +$(mkNuMatching [t| forall a . AtomicPerm a |]) +$(mkNuMatching [t| forall a . ValuePerm a |]) +-- $(mkNuMatching [t| forall as. ValuePerms as |]) +$(mkNuMatching [t| forall a . VarAndPerm a |]) + +$(mkNuMatching [t| forall w . LLVMArrayIndex w |]) +$(mkNuMatching [t| forall args ret. SomeFunPerm args ret |]) +$(mkNuMatching [t| SomeNamedPermName |]) +$(mkNuMatching [t| forall b args a. OpaquePerm b args a |]) +$(mkNuMatching [t| forall args a reach. ReachMethods args a reach |]) +$(mkNuMatching [t| forall b reach args a. RecPerm b reach args a |]) +$(mkNuMatching [t| forall b args a. DefinedPerm b args a |]) +$(mkNuMatching [t| forall ns args a. NamedPerm ns args a |]) +$(mkNuMatching [t| forall args a. LifetimeFunctor args a |]) +$(mkNuMatching [t| forall ps. LifetimeCurrentPerms ps |]) +$(mkNuMatching [t| forall a. SomeLLVMBlockPerm a |]) +$(mkNuMatching [t| forall w. SomeBindingLLVMBlockPerm w |]) + +$(mkNuMatching [t| forall w sz. TaggedUnionShape w sz |]) +$(mkNuMatching [t| forall w. SomeTaggedUnionShape w |]) +$(mkNuMatching [t| forall ctx. PermVarSubst ctx |]) +$(mkNuMatching [t| PermEnvFunEntry |]) +$(mkNuMatching [t| SomeNamedPerm |]) +$(mkNuMatching [t| SomeNamedShape |]) +$(mkNuMatching [t| PermEnvGlobalEntry |]) +$(mkNuMatching [t| forall args. BlockHintSort args |]) +$(mkNuMatching [t| forall blocks init ret args. + BlockHint blocks init ret args |]) +$(mkNuMatching [t| Hint |]) +$(mkNuMatching [t| PermEnv |]) + +-- NOTE: this instance would require a NuMatching instance for NameMap... +-- $(mkNuMatching [t| forall ps. PermSet ps |]) + + ---------------------------------------------------------------------- -- * Utility Functions and Definitions ---------------------------------------------------------------------- @@ -470,13 +1265,6 @@ instance PermPretty Integer where -- * Expressions for Permissions ---------------------------------------------------------------------- --- | The Haskell type of expression variables -type ExprVar = (Name :: CrucibleType -> Type) - --- | Crucible type for lifetimes; we give them a Crucible type so they can be --- existentially bound in the same way as other Crucible objects -type LifetimeType = IntrinsicType "Lifetime" EmptyCtx - -- | The object-level representation of 'LifetimeType' lifetimeTypeRepr :: TypeRepr LifetimeType lifetimeTypeRepr = knownRepr @@ -492,203 +1280,66 @@ pattern LifetimeRepr <- -- | A lifetime is an expression of type 'LifetimeType' --type Lifetime = PermExpr LifetimeType --- | Crucible type for read/write modalities; we give them a Crucible type so --- they can be used as variables in recursive permission definitions -type RWModalityType = IntrinsicType "RWModality" EmptyCtx - --- | The object-level representation of 'RWModalityType' -rwModalityTypeRepr :: TypeRepr RWModalityType -rwModalityTypeRepr = knownRepr - --- | Pattern for building/destructing RWModality types -pattern RWModalityRepr :: () => (ty ~ RWModalityType) => TypeRepr ty -pattern RWModalityRepr <- - IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "RWModality") -> - Just Refl) - Empty - where RWModalityRepr = IntrinsicRepr knownSymbol Empty - --- | Crucible type for lists of expressions and permissions on them -type PermListType = IntrinsicType "PermList" EmptyCtx - --- | Pattern for building/desctructing permission list types -pattern PermListRepr :: () => ty ~ PermListType => TypeRepr ty -pattern PermListRepr <- - IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "PermList") -> - Just Refl) Empty - where - PermListRepr = IntrinsicRepr knownSymbol Empty - --- | Crucible type for LLVM stack frame objects -type LLVMFrameType w = IntrinsicType "LLVMFrame" (EmptyCtx ::> BVType w) - --- | Pattern for building/desctructing LLVM frame types -pattern LLVMFrameRepr :: () => (1 <= w, ty ~ LLVMFrameType w) => - NatRepr w -> TypeRepr ty -pattern LLVMFrameRepr w <- - IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVMFrame") -> - Just Refl) - (viewAssign -> AssignExtend Empty (BVRepr w)) - where - LLVMFrameRepr w = IntrinsicRepr knownSymbol (Ctx.extend Empty (BVRepr w)) - --- | Crucible type for value permissions themselves -type ValuePermType a = IntrinsicType "Perm" (EmptyCtx ::> a) - --- | Pattern for building/desctructing permissions as expressions -pattern ValuePermRepr :: () => (ty ~ ValuePermType a) => TypeRepr a -> - TypeRepr ty -pattern ValuePermRepr a <- - IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "Perm") -> - Just Refl) - (viewAssign -> AssignExtend Empty a) - where - ValuePermRepr a = IntrinsicRepr knownSymbol (Ctx.extend Empty a) - --- | Crucible type for LLVM shapes -type LLVMShapeType w = IntrinsicType "LLVMShape" (EmptyCtx ::> BVType w) - --- | Pattern for building/desctructing LLVM frame types -pattern LLVMShapeRepr :: () => (1 <= w, ty ~ LLVMShapeType w) => - NatRepr w -> TypeRepr ty -pattern LLVMShapeRepr w <- - IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVMShape") -> - Just Refl) - (viewAssign -> AssignExtend Empty (BVRepr w)) - where - LLVMShapeRepr w = IntrinsicRepr knownSymbol (Ctx.extend Empty (BVRepr w)) - --- | Crucible type for LLVM memory blocks -type LLVMBlockType w = IntrinsicType "LLVMBlock" (EmptyCtx ::> BVType w) - --- | Pattern for building/desctructing LLVM frame types -pattern LLVMBlockRepr :: () => (1 <= w, ty ~ LLVMBlockType w) => - NatRepr w -> TypeRepr ty -pattern LLVMBlockRepr w <- - IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVMBlock") -> - Just Refl) - (viewAssign -> AssignExtend Empty (BVRepr w)) - where - LLVMBlockRepr w = IntrinsicRepr knownSymbol (Ctx.extend Empty (BVRepr w)) - - --- | Expressions that are considered "pure" for use in permissions. Note that --- these are in a normal form, that makes them easier to analyze. -data PermExpr (a :: CrucibleType) where - -- | A variable of any type - PExpr_Var :: ExprVar a -> PermExpr a - - -- | A unit literal - PExpr_Unit :: PermExpr UnitType - - -- | A literal Boolean number - PExpr_Bool :: Bool -> PermExpr BoolType - - -- | A literal natural number - PExpr_Nat :: Natural -> PermExpr NatType - - -- | A literal string - PExpr_String :: String -> PermExpr (StringType Unicode) - - -- | A bitvector expression is a linear expression in @N@ variables, i.e., sum - -- of constant times variable factors plus a constant - -- - -- FIXME: make the offset a 'Natural' - PExpr_BV :: (1 <= w, KnownNat w) => - [BVFactor w] -> BV w -> PermExpr (BVType w) - - -- | A struct expression is an expression for each argument of the struct type - PExpr_Struct :: PermExprs (CtxToRList args) -> PermExpr (StructType args) - - -- | The @always@ lifetime that is always current - PExpr_Always :: PermExpr LifetimeType - - -- | An LLVM value that represents a word, i.e., whose region identifier is 0 - PExpr_LLVMWord :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> - PermExpr (LLVMPointerType w) - - -- | An LLVM value built by adding an offset to an LLVM variable - PExpr_LLVMOffset :: (1 <= w, KnownNat w) => - ExprVar (LLVMPointerType w) -> - PermExpr (BVType w) -> - PermExpr (LLVMPointerType w) - - -- | A literal function pointer - PExpr_Fun :: FnHandle args ret -> PermExpr (FunctionHandleType args ret) - - -- | An empty permission list - PExpr_PermListNil :: PermExpr PermListType - - -- | A cons of an expression and a permission on it to a permission list - PExpr_PermListCons :: TypeRepr a -> PermExpr a -> ValuePerm a -> - PermExpr PermListType -> PermExpr PermListType - - -- | A read/write modality - PExpr_RWModality :: RWModality -> PermExpr RWModalityType - - -- | The empty / vacuously true shape - PExpr_EmptyShape :: PermExpr (LLVMShapeType w) - - -- | A named shape along with arguments for it, with optional read/write and - -- lifetime modalities that are applied to the body of the shape - PExpr_NamedShape :: KnownNat w => Maybe (PermExpr RWModalityType) -> - Maybe (PermExpr LifetimeType) -> - NamedShape b args w -> PermExprs args -> - PermExpr (LLVMShapeType w) - - -- | The equality shape - PExpr_EqShape :: PermExpr (LLVMBlockType w) -> PermExpr (LLVMShapeType w) - - -- | A shape for a pointer to another memory block, i.e., a @memblock@ - -- permission, with a given shape. This @memblock@ permission will have the - -- same read/write and lifetime modalities as the @memblock@ permission - -- containing this pointer shape, unless they are specifically overridden by - -- the pointer shape; i.e., we have that - -- - -- > [l]memblock(rw,off,len,ptrsh(rw',l',sh)) = - -- > [l]memblock(rw,off,len,fieldsh([l']memblock(rw',0,len(sh),sh))) - -- - -- where @rw'@ and/or @l'@ can be 'Nothing', in which case they default to - -- @rw@ and @l@, respectively. - PExpr_PtrShape :: Maybe (PermExpr RWModalityType) -> - Maybe (PermExpr LifetimeType) -> - PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w) - - -- | A shape for a single field with a given permission - PExpr_FieldShape :: (1 <= w, KnownNat w) => LLVMFieldShape w -> - PermExpr (LLVMShapeType w) - - -- | A shape for an array of @len@ individual regions of memory, called "array - -- cells"; the size of each cell in bytes is given by the array stride, which - -- must be known statically, and each cell has shape given by the supplied - -- LLVM shape, also called the cell shape - PExpr_ArrayShape :: (1 <= w, KnownNat w) => - PermExpr (BVType w) -> Bytes -> - PermExpr (LLVMShapeType w) -> - PermExpr (LLVMShapeType w) +-- | The object-level representation of 'RWModalityType' +rwModalityTypeRepr :: TypeRepr RWModalityType +rwModalityTypeRepr = knownRepr - -- | A sequence of two shapes - PExpr_SeqShape :: PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w) -> - PermExpr (LLVMShapeType w) +-- | Pattern for building/destructing RWModality types +pattern RWModalityRepr :: () => (ty ~ RWModalityType) => TypeRepr ty +pattern RWModalityRepr <- + IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "RWModality") -> + Just Refl) + Empty + where RWModalityRepr = IntrinsicRepr knownSymbol Empty - -- | A disjunctive shape - PExpr_OrShape :: PermExpr (LLVMShapeType w) -> PermExpr (LLVMShapeType w) -> - PermExpr (LLVMShapeType w) +-- | Pattern for building/desctructing permission list types +pattern PermListRepr :: () => ty ~ PermListType => TypeRepr ty +pattern PermListRepr <- + IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "PermList") -> + Just Refl) Empty + where + PermListRepr = IntrinsicRepr knownSymbol Empty - -- | An existential shape - PExpr_ExShape :: KnownRepr TypeRepr a => - Binding a (PermExpr (LLVMShapeType w)) -> - PermExpr (LLVMShapeType w) +-- | Pattern for building/desctructing LLVM frame types +pattern LLVMFrameRepr :: () => (1 <= w, ty ~ LLVMFrameType w) => + NatRepr w -> TypeRepr ty +pattern LLVMFrameRepr w <- + IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVMFrame") -> + Just Refl) + (viewAssign -> AssignExtend Empty (BVRepr w)) + where + LLVMFrameRepr w = IntrinsicRepr knownSymbol (Ctx.extend Empty (BVRepr w)) - -- | A false shape - PExpr_FalseShape :: PermExpr (LLVMShapeType w) +-- | Pattern for building/desctructing permissions as expressions +pattern ValuePermRepr :: () => (ty ~ ValuePermType a) => TypeRepr a -> + TypeRepr ty +pattern ValuePermRepr a <- + IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "Perm") -> + Just Refl) + (viewAssign -> AssignExtend Empty a) + where + ValuePermRepr a = IntrinsicRepr knownSymbol (Ctx.extend Empty a) - -- | A permission as an expression - PExpr_ValPerm :: ValuePerm a -> PermExpr (ValuePermType a) +-- | Pattern for building/desctructing LLVM frame types +pattern LLVMShapeRepr :: () => (1 <= w, ty ~ LLVMShapeType w) => + NatRepr w -> TypeRepr ty +pattern LLVMShapeRepr w <- + IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVMShape") -> + Just Refl) + (viewAssign -> AssignExtend Empty (BVRepr w)) + where + LLVMShapeRepr w = IntrinsicRepr knownSymbol (Ctx.extend Empty (BVRepr w)) +-- | Pattern for building/desctructing LLVM frame types +pattern LLVMBlockRepr :: () => (1 <= w, ty ~ LLVMBlockType w) => + NatRepr w -> TypeRepr ty +pattern LLVMBlockRepr w <- + IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVMBlock") -> + Just Refl) + (viewAssign -> AssignExtend Empty (BVRepr w)) + where + LLVMBlockRepr w = IntrinsicRepr knownSymbol (Ctx.extend Empty (BVRepr w)) --- | A sequence of permission expressions -type PermExprs = RAssign PermExpr -- | Pattern for an empty 'PermExprs' list pattern PExprs_Nil :: () => (tps ~ RNil) => PermExprs tps @@ -703,12 +1354,6 @@ pattern PExprs_Cons es e <- es :>: e {-# COMPLETE PExprs_Nil, PExprs_Cons #-} -{- -data PermExprs (as :: RList CrucibleType) where - PExprs_Nil :: PermExprs RNil - PExprs_Cons :: PermExprs as -> PermExpr a -> PermExprs (as :> a) --} - -- | Convert a 'PermExprs' to an 'RAssign' exprsToRAssign :: PermExprs as -> RAssign PermExpr as exprsToRAssign PExprs_Nil = MNil @@ -717,7 +1362,7 @@ exprsToRAssign (PExprs_Cons es e) = exprsToRAssign es :>: e -- | Convert an 'RAssign' to a 'PermExprs' rassignToExprs :: RAssign PermExpr as -> PermExprs as rassignToExprs MNil = PExprs_Nil -rassignToExprs (es :>: e) = PExprs_Cons (rassignToExprs es) e +rassignToExprs (es :>: e) = PExprs_Cons (rassignToExprs es) e -- | Convert a list of names to a 'PermExprs' list namesToExprs :: RAssign Name as -> PermExprs as @@ -838,20 +1483,6 @@ findAtomicPermInList x pred plist = foldPermListAtomic x (\p rest -> if pred p then Just p else rest) Nothing plist --- | A bitvector variable, possibly multiplied by a constant -data BVFactor w where - -- | A variable of type @'BVType' w@ multiplied by a constant @i@, which - -- should be in the range @0 <= i < 2^w@ - BVFactor :: (1 <= w, KnownNat w) => BV w -> ExprVar (BVType w) -> - BVFactor w - --- | Whether a permission allows reads or writes -data RWModality - = Write - | Read - deriving Eq - - instance Eq (PermExpr a) where (PExpr_Var x1) == (PExpr_Var x2) = x1 == x2 (PExpr_Var _) == _ = False @@ -1569,154 +2200,9 @@ offsetBVRange off (BVRange off' len) = (BVRange (bvAdd off' off) len) -- * Permissions ---------------------------------------------------------------------- --- | The Haskell type of permission variables, that is, variables that range --- over 'ValuePerm's -type PermVar (a :: CrucibleType) = Name (ValuePermType a) - --- | Ranges @[off,off+len)@ of bitvector values @x@ equal to @off+y@ for some --- unsigned @y < len@. Note that ranges are allowed to wrap around 0, meaning --- @off+y@ can overflow when testing whether @x@ is in the range. Thus, @x@ is --- in range @[off,off+len)@ iff @x-off@ is unsigned less than @len@. -data BVRange w = BVRange { bvRangeOffset :: PermExpr (BVType w), - bvRangeLength :: PermExpr (BVType w) } - deriving Eq - --- | Propositions about bitvectors -data BVProp w - -- | True iff the two expressions are equal - = BVProp_Eq (PermExpr (BVType w)) (PermExpr (BVType w)) - -- | True iff the two expressions are not equal - | BVProp_Neq (PermExpr (BVType w)) (PermExpr (BVType w)) - -- | True iff the first expression is unsigned less-than the second - | BVProp_ULt (PermExpr (BVType w)) (PermExpr (BVType w)) - -- | True iff the first expression is unsigned @<=@ the second - | BVProp_ULeq (PermExpr (BVType w)) (PermExpr (BVType w)) - -- | True iff the first expression is unsigned @<=@ the difference of the - -- second minus the third - | (1 <= w, KnownNat w) => - BVProp_ULeq_Diff (PermExpr (BVType w)) (PermExpr (BVType w)) - (PermExpr (BVType w)) - +deriving instance Eq (BVRange w) deriving instance Eq (BVProp w) --- | An atomic permission is a value permission that is not one of the compound --- constructs in the 'ValuePerm' type; i.e., not a disjunction, existential, --- recursive, or equals permission. These are the permissions that we can put --- together with separating conjuctions. -data AtomicPerm (a :: CrucibleType) where - -- | Gives permissions to a single field pointed to by an LLVM pointer - Perm_LLVMField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) => - LLVMFieldPerm w sz -> - AtomicPerm (LLVMPointerType w) - - -- | Gives permissions to an array pointer to by an LLVM pointer - Perm_LLVMArray :: (1 <= w, KnownNat w) => LLVMArrayPerm w -> - AtomicPerm (LLVMPointerType w) - - -- | Gives read or write access to a memory block, whose contents also give - -- some permissions - Perm_LLVMBlock :: (1 <= w, KnownNat w) => LLVMBlockPerm w -> - AtomicPerm (LLVMPointerType w) - - -- | Says that we have permission to free the memory pointed at by this - -- pointer if we have write permission to @e@ words of size @w@ - Perm_LLVMFree :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> - AtomicPerm (LLVMPointerType w) - - -- | Says that we known an LLVM value is a function pointer whose function has - -- the given permissions - Perm_LLVMFunPtr :: (1 <= w, KnownNat w) => - TypeRepr (FunctionHandleType cargs ret) -> - ValuePerm (FunctionHandleType cargs ret) -> - AtomicPerm (LLVMPointerType w) - - -- | Says that a memory block has a given shape - Perm_LLVMBlockShape :: (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w) -> - AtomicPerm (LLVMBlockType w) - - -- | Says we know an LLVM value is a pointer value, meaning that its block - -- value is non-zero. Note that this does not say the pointer is allocated. - Perm_IsLLVMPtr :: (1 <= w, KnownNat w) => - AtomicPerm (LLVMPointerType w) - - -- | A named conjunctive permission - Perm_NamedConj :: NameSortIsConj ns ~ 'True => - NamedPermName ns args a -> PermExprs args -> - PermOffset a -> AtomicPerm a - - -- | Permission to allocate (via @alloca@) on an LLVM stack frame, and - -- permission to delete that stack frame if we have exclusive permissions to - -- all the given LLVM pointer objects - Perm_LLVMFrame :: (1 <= w, KnownNat w) => LLVMFramePerm w -> - AtomicPerm (LLVMFrameType w) - - -- | Ownership permission for a lifetime, including an assertion that it is - -- still current and permission to end that lifetime. A lifetime also - -- represents a permission "borrow" of some sub-permissions out of some larger - -- permissions. For example, we might borrow a portion of an array, or a - -- portion of a larger data structure. When the lifetime is ended, you have to - -- give back to sub-permissions to get back the larger permissions. Together, - -- these are a form of permission implication, so we write lifetime ownership - -- permissions as @lowned(Pin -o Pout)@. Intuitively, @Pin@ must be given back - -- before the lifetime is ended, and @Pout@ is returned afterwards. - -- Additionally, a lifetime may contain some other lifetimes, meaning the all - -- must end before the current one can be ended. - Perm_LOwned :: [PermExpr LifetimeType] -> - LOwnedPerms ps_in -> LOwnedPerms ps_out -> - AtomicPerm LifetimeType - - -- | Assertion that a lifetime is current during another lifetime - Perm_LCurrent :: PermExpr LifetimeType -> AtomicPerm LifetimeType - - -- | Assertion that a lifetime has finished - Perm_LFinished :: AtomicPerm LifetimeType - - -- | A struct permission = a sequence of permissions for each field - Perm_Struct :: RAssign ValuePerm (CtxToRList ctx) -> - AtomicPerm (StructType ctx) - - -- | A function permission - Perm_Fun :: FunPerm ghosts (CtxToRList cargs) gouts ret -> - AtomicPerm (FunctionHandleType cargs ret) - - -- | An LLVM permission that asserts a proposition about bitvectors - Perm_BVProp :: (1 <= w, KnownNat w) => BVProp w -> - AtomicPerm (LLVMPointerType w) - - --- | A value permission is a permission to do something with a value, such as --- use it as a pointer. This also includes a limited set of predicates on values --- (you can think about this as "permission to assume the value satisfies this --- predicate" if you like). -data ValuePerm (a :: CrucibleType) where - - -- | Says that a value is equal to a known static expression - ValPerm_Eq :: PermExpr a -> ValuePerm a - - -- | The disjunction of two value permissions - ValPerm_Or :: ValuePerm a -> ValuePerm a -> ValuePerm a - - -- | An existential binding of a value in a value permission - -- - -- FIXME: turn the 'KnownRepr' constraint into a normal 'TypeRepr' argument - ValPerm_Exists :: KnownRepr TypeRepr a => - Binding a (ValuePerm b) -> - ValuePerm b - - -- | A named permission - ValPerm_Named :: NamedPermName ns args a -> PermExprs args -> - PermOffset a -> ValuePerm a - - -- | A permission variable plus an offset - ValPerm_Var :: PermVar a -> PermOffset a -> ValuePerm a - - -- | A separating conjuction of 0 or more atomic permissions, where 0 - -- permissions is the trivially true permission - ValPerm_Conj :: [AtomicPerm a] -> ValuePerm a - - -- | The false value permission - ValPerm_False :: ValuePerm a - -- | Build an equality permission in a binding mbValPerm_Eq :: Mb ctx (PermExpr a) -> Mb ctx (ValuePerm a) mbValPerm_Eq = mbMapCl $(mkClosed [| ValPerm_Eq |]) @@ -1818,22 +2304,13 @@ pattern ValPerm_LCurrent :: () => (a ~ LifetimeType) => PermExpr LifetimeType -> ValuePerm a pattern ValPerm_LCurrent l <- ValPerm_Conj [Perm_LCurrent l] where - ValPerm_LCurrent l = ValPerm_Conj [Perm_LCurrent l] - --- | A single @lfinished@ permission -pattern ValPerm_LFinished :: () => (a ~ LifetimeType) => ValuePerm a -pattern ValPerm_LFinished <- ValPerm_Conj [Perm_LFinished] - where - ValPerm_LFinished = ValPerm_Conj [Perm_LFinished] - --- | A sequence of value permissions -{- -data ValuePerms as where - ValPerms_Nil :: ValuePerms RNil - ValPerms_Cons :: ValuePerms as -> ValuePerm a -> ValuePerms (as :> a) --} + ValPerm_LCurrent l = ValPerm_Conj [Perm_LCurrent l] -type ValuePerms = RAssign ValuePerm +-- | A single @lfinished@ permission +pattern ValPerm_LFinished :: () => (a ~ LifetimeType) => ValuePerm a +pattern ValPerm_LFinished <- ValPerm_Conj [Perm_LFinished] + where + ValPerm_LFinished = ValPerm_Conj [Perm_LFinished] pattern ValPerms_Nil :: () => (tps ~ RNil) => ValuePerms tps pattern ValPerms_Nil = MNil @@ -1865,30 +2342,10 @@ assignToPerms :: RAssign ValuePerm ps -> ValuePerms ps assignToPerms MNil = ValPerms_Nil assignToPerms (ps :>: p) = ValPerms_Cons (assignToPerms ps) p --- | A binding of 0 or more variables, each with permissions -type MbValuePerms ctx = Mb ctx (ValuePerms ctx) - --- | A frame permission is a list of the pointers that have been allocated in --- the frame and their corresponding allocation sizes in words of size --- @w@. Write permissions of the given sizes are required to these pointers in --- order to delete the frame. -type LLVMFramePerm w = [(PermExpr (LLVMPointerType w), Integer)] - -- | An LLVM pointer permission is an 'AtomicPerm' of type 'LLVMPointerType' type LLVMPtrPerm w = AtomicPerm (LLVMPointerType w) --- | A permission for a pointer to a specific field of a given size -data LLVMFieldPerm w sz = - LLVMFieldPerm { llvmFieldRW :: PermExpr RWModalityType, - -- ^ Whether this is a read or write permission - llvmFieldLifetime :: PermExpr LifetimeType, - -- ^ The lifetime during which this field permission is active - llvmFieldOffset :: PermExpr (BVType w), - -- ^ The offset from the pointer in bytes of this field - llvmFieldContents :: ValuePerm (LLVMPointerType sz) - -- ^ The permissions we get for the value read from this field - } - deriving Eq +deriving instance Eq (LLVMFieldPerm w sz) -- | Helper to get a 'NatRepr' for the size of an 'LLVMFieldPerm' llvmFieldSize :: KnownNat sz => LLVMFieldPerm w sz -> NatRepr sz @@ -1937,42 +2394,12 @@ llvmFieldRange fp = BVRange (llvmFieldOffset fp) (bvInt $ llvmFieldSizeBytes fp) --- | Helper type to represent byte offsets --- --- > stride * ix + off --- --- from the beginning of an array permission. Such an expression refers to --- offset @off@, which must be a statically-known constant, in array cell @ix@. -data LLVMArrayIndex w = - LLVMArrayIndex { llvmArrayIndexCell :: PermExpr (BVType w), - llvmArrayIndexOffset :: BV w } - -- NOTE: we need a custom instance of Eq so we can use bvEq on the cell instance Eq (LLVMArrayIndex w) where LLVMArrayIndex e1 i1 == LLVMArrayIndex e2 i2 = bvEq e1 e2 && i1 == i2 --- | A permission to an array of @len@ individual regions of memory, called --- "array cells". The size of each cell in bytes is given by the array /stride/, --- which must be known statically, and each cell has shape given by the supplied --- LLVM shape, also called the cell shape. -data LLVMArrayPerm w = - LLVMArrayPerm { llvmArrayRW :: PermExpr RWModalityType, - -- ^ Whether this array gives read or write access - llvmArrayLifetime :: PermExpr LifetimeType, - -- ^ The lifetime during which this array permission is valid - llvmArrayOffset :: PermExpr (BVType w), - -- ^ The offset from the pointer in bytes of this array - llvmArrayLen :: PermExpr (BVType w), - -- ^ The number of array blocks - llvmArrayStride :: Bytes, - -- ^ The array stride in bytes - llvmArrayCellShape :: PermExpr (LLVMShapeType w), - -- ^ The shape of each cell in the array - llvmArrayBorrows :: [LLVMArrayBorrow w] - -- ^ Indices or index ranges that are missing from this array - } - deriving Eq +deriving instance Eq (LLVMArrayPerm w) -- | Get the stride of an array in bits llvmArrayStrideBits :: LLVMArrayPerm w -> Integer @@ -2008,33 +2435,8 @@ mbLLVMArrayCellShape = mbMapCl $(mkClosed [| llvmArrayCellShape |]) mbLLVMArrayBorrows :: Mb ctx (LLVMArrayPerm w) -> Mb ctx [LLVMArrayBorrow w] mbLLVMArrayBorrows = mbMapCl $(mkClosed [| llvmArrayBorrows |]) --- | An index or range of indices that are missing from an array perm --- --- FIXME: think about calling the just @LLVMArrayIndexSet@ -data LLVMArrayBorrow w - = FieldBorrow (PermExpr (BVType w)) - -- ^ Borrow a specific cell of an array permission - | RangeBorrow (BVRange w) - -- ^ Borrow a range of array cells, where each cell is 'llvmArrayStride' - -- bytes long - deriving Eq - - --- | An LLVM block permission is read or write access to the memory at a given --- offset with a given length with a given shape -data LLVMBlockPerm w = - LLVMBlockPerm { llvmBlockRW :: PermExpr RWModalityType, - -- ^ Whether this is a read or write block permission - llvmBlockLifetime :: PermExpr LifetimeType, - -- ^ The lifetime during with this block permission is active - llvmBlockOffset :: PermExpr (BVType w), - -- ^ The offset of the block from the pointer in bytes - llvmBlockLen :: PermExpr (BVType w), - -- ^ The length of the block in bytes - llvmBlockShape :: PermExpr (LLVMShapeType w) - -- ^ The shape of the permissions in the block - } - deriving Eq +deriving instance Eq (LLVMArrayBorrow w) +deriving instance Eq (LLVMBlockPerm w) -- | Get the rw-modality-in-binding of a block permission in binding mbLLVMBlockRW :: Mb ctx (LLVMBlockPerm w) -> Mb ctx (PermExpr RWModalityType) @@ -2066,30 +2468,12 @@ llvmBlockRange bp = BVRange (llvmBlockOffset bp) (llvmBlockLen bp) mbLLVMBlockRange :: Mb ctx (LLVMBlockPerm w) -> Mb ctx (BVRange w) mbLLVMBlockRange = mbMapCl $(mkClosed [| llvmBlockRange |]) --- | An LLVM shape for a single pointer field of unknown size -data LLVMFieldShape w = - forall sz. (1 <= sz, KnownNat sz) => - LLVMFieldShape (ValuePerm (LLVMPointerType sz)) - instance Eq (LLVMFieldShape w) where (LLVMFieldShape p1) == (LLVMFieldShape p2) | Just Refl <- testEquality (exprType p1) (exprType p2) = p1 == p2 _ == _ = False --- | A form of permission used in lifetime ownership permissions -data LOwnedPerm a where - LOwnedPermField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) => - PermExpr (LLVMPointerType w) -> LLVMFieldPerm w sz -> - LOwnedPerm (LLVMPointerType w) - LOwnedPermArray :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) -> - LLVMArrayPerm w -> LOwnedPerm (LLVMPointerType w) - LOwnedPermBlock :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) -> - LLVMBlockPerm w -> LOwnedPerm (LLVMPointerType w) - --- | A sequence of 'LOwnedPerm's -type LOwnedPerms = RAssign LOwnedPerm - instance TestEquality LOwnedPerm where testEquality (LOwnedPermField e1 fp1) (LOwnedPermField e2 fp2) | Just Refl <- testEquality (exprType e1) (exprType e2) @@ -2203,15 +2587,6 @@ lownedPermsOffsetsForLLVMVar x (lops :>: lop) lownedPermsOffsetsForLLVMVar x (lops :>: _) = lownedPermsOffsetsForLLVMVar x lops --- | A function permission is a set of input and output permissions inside a --- context of ghost variables @ghosts@ with an additional context of output --- ghost variables @gouts@ -data FunPerm ghosts args gouts ret where - FunPerm :: CruCtx ghosts -> CruCtx args -> CruCtx gouts -> TypeRepr ret -> - MbValuePerms (ghosts :++: args) -> - MbValuePerms ((ghosts :++: args) :++: gouts :> ret) -> - FunPerm ghosts args gouts ret - -- | Extract the @args@ context from a function permission funPermArgs :: FunPerm ghosts args gouts ret -> CruCtx args funPermArgs (FunPerm _ args _ _ _ _) = args @@ -2247,46 +2622,12 @@ funPermOuts :: FunPerm ghosts args gouts ret -> funPermOuts (FunPerm _ _ _ _ _ perms_out) = perms_out --- | A function permission that existentially quantifies the ghost types -data SomeFunPerm args ret where - SomeFunPerm :: FunPerm ghosts args gouts ret -> SomeFunPerm args ret - - --- | The different sorts of name, each of which comes with a 'Bool' flag --- indicating whether the name can be used as an atomic permission. A recursive --- sort also comes with a second flag indicating whether it is a reachability --- permission. -data NameSort = DefinedSort Bool | OpaqueSort Bool | RecursiveSort Bool Bool - -type DefinedSort = 'DefinedSort -type OpaqueSort = 'OpaqueSort -type RecursiveSort = 'RecursiveSort - --- | Test whether a name of a given 'NameSort' is conjoinable -type family NameSortIsConj (ns::NameSort) :: Bool where - NameSortIsConj (DefinedSort b) = b - NameSortIsConj (OpaqueSort b) = b - NameSortIsConj (RecursiveSort b _) = b - -- | Test whether a name of a given 'NameSort' can be folded / unfolded type family NameSortCanFold (ns::NameSort) :: Bool where NameSortCanFold (DefinedSort _) = 'True NameSortCanFold (OpaqueSort _) = 'False NameSortCanFold (RecursiveSort b _) = 'True --- | Test whether a name of a given 'NameSort' is a reachability permission -type family IsReachabilityName (ns::NameSort) :: Bool where - IsReachabilityName (DefinedSort _) = 'False - IsReachabilityName (OpaqueSort _) = 'False - IsReachabilityName (RecursiveSort _ reach) = reach - --- | A singleton representation of 'NameSort' -data NameSortRepr (ns::NameSort) where - DefinedSortRepr :: BoolRepr b -> NameSortRepr (DefinedSort b) - OpaqueSortRepr :: BoolRepr b -> NameSortRepr (OpaqueSort b) - RecursiveSortRepr :: BoolRepr b -> BoolRepr reach -> - NameSortRepr (RecursiveSort b reach) - -- | Get a 'BoolRepr' for whether a name sort is conjunctive nameSortIsConjRepr :: NameSortRepr ns -> BoolRepr (NameSortIsConj ns) nameSortIsConjRepr (DefinedSortRepr b) = b @@ -2335,14 +2676,6 @@ instance TestEquality NameSortRepr where = Just Refl testEquality (RecursiveSortRepr _ _) _ = Nothing --- | A constraint that the last argument of a reachability permission is a --- permission argument -data NameReachConstr ns args a where - NameReachConstr :: (IsReachabilityName ns ~ 'True) => - NameReachConstr ns (args :> a) a - NameNonReachConstr :: (IsReachabilityName ns ~ 'False) => - NameReachConstr ns args a - -- | Extract a 'BoolRepr' from a 'NameReachConstr' for whether the name it -- constrains is a reachability name nameReachConstrBool :: NameReachConstr ns args a -> @@ -2350,15 +2683,6 @@ nameReachConstrBool :: NameReachConstr ns args a -> nameReachConstrBool NameReachConstr = TrueRepr nameReachConstrBool NameNonReachConstr = FalseRepr --- | A name for a named permission -data NamedPermName ns args a = NamedPermName { - namedPermNameName :: String, - namedPermNameType :: TypeRepr a, - namedPermNameArgs :: CruCtx args, - namedPermNameSort :: NameSortRepr ns, - namedPermNameReachConstr :: NameReachConstr ns args a - } - -- FIXME: NamedPermNames should maybe say something about which arguments are -- covariant? Right now we assume lifetime and rwmodalities are covariant -- w.r.t. their respective orders, and everything else is invariant, but that @@ -2380,10 +2704,6 @@ instance Eq (NamedPermName ns args a) where n1 == n2 | Just (Refl, Refl, Refl) <- testNamedPermNameEq n1 n2 = True _ == _ = False --- | An existentially quantified 'NamedPermName' -data SomeNamedPermName where - SomeNamedPermName :: NamedPermName ns args a -> SomeNamedPermName - instance Eq SomeNamedPermName where (SomeNamedPermName n1) == (SomeNamedPermName n2) | Just (Refl, Refl, Refl) <- testNamedPermNameEq n1 n2 = True @@ -2395,14 +2715,6 @@ data SomeNamedConjPermName where NameSortIsConj ns ~ 'True => NamedPermName ns args a -> SomeNamedConjPermName --- | A named LLVM shape is a name, a list of arguments, and a body, where the --- Boolean flag @b@ determines whether the shape can be unfolded or not -data NamedShape b args w = NamedShape { - namedShapeName :: String, - namedShapeArgs :: CruCtx args, - namedShapeBody :: NamedShapeBody b args w - } - -- | Test if two 'NamedShapes' of possibly different @b@ and @args@ arguments -- are equal namedShapeEq :: NamedShape b1 args1 w -> NamedShape b2 args2 w -> @@ -2417,24 +2729,6 @@ namedShapeEq nmsh1 nmsh2 Just (Refl,Refl) namedShapeEq _ _ = Nothing -data NamedShapeBody b args w where - -- | A defined shape is just a definition in terms of the arguments - DefinedShapeBody :: Mb args (PermExpr (LLVMShapeType w)) -> - NamedShapeBody 'True args w - - -- | An opaque shape has no body, just a length and a translation to a type - OpaqueShapeBody :: Mb args (PermExpr (BVType w)) -> Ident -> - NamedShapeBody 'False args w - - -- | A recursive shape body has a one-step unfolding to a shape, which can - -- refer to the shape itself via the last bound variable; it also has - -- identifiers for the type it is translated to, along with fold and unfold - -- functions for mapping to and from this type. The fold and unfold functions - -- can be undefined if we are in the process of defining this recusive shape. - RecShapeBody :: Mb (args :> LLVMShapeType w) (PermExpr (LLVMShapeType w)) -> - Ident -> Maybe (Ident, Ident) -> - NamedShapeBody 'True args w - deriving instance Eq (NamedShapeBody b args w) -- | Test if a 'NamedShape' is recursive @@ -2464,14 +2758,6 @@ mbNamedShapeCanUnfoldRepr = namedShapeCanUnfold :: NamedShape b args w -> Bool namedShapeCanUnfold = boolVal . namedShapeCanUnfoldRepr --- | An offset that is added to a permission. Only makes sense for llvm --- permissions (at least for now...?) -data PermOffset a where - NoPermOffset :: PermOffset a - -- | NOTE: the invariant is that the bitvector offset is non-zero - LLVMPermOffset :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> - PermOffset (LLVMPointerType w) - instance Eq (PermOffset a) where NoPermOffset == NoPermOffset = True (LLVMPermOffset e1) == (LLVMPermOffset e2) = e1 == e2 @@ -2541,97 +2827,29 @@ setNthPermExpr (PExprs_Cons args _) Member_Base a = setNthPermExpr (PExprs_Cons args arg) (Member_Step memb) a = PExprs_Cons (setNthPermExpr args memb a) arg --- | Get a list of 'Member' proofs for each expression in a 'PermExprs' list -getPermExprsMembers :: PermExprs args -> - [Some (Member args :: CrucibleType -> Type)] -getPermExprsMembers PExprs_Nil = [] -getPermExprsMembers (PExprs_Cons args _) = - map (\case Some memb -> Some (Member_Step memb)) (getPermExprsMembers args) - ++ [Some Member_Base] - --- | The semantics of a named permission, which can can either be an opaque --- named permission, a recursive named permission, a defined permission, or an --- LLVM shape -data NamedPerm ns args a where - NamedPerm_Opaque :: OpaquePerm b args a -> NamedPerm (OpaqueSort b) args a - NamedPerm_Rec :: RecPerm b reach args a -> - NamedPerm (RecursiveSort b reach) args a - NamedPerm_Defined :: DefinedPerm b args a -> NamedPerm (DefinedSort b) args a - --- | Extract the name back out of the interpretation of a 'NamedPerm' -namedPermName :: NamedPerm ns args a -> NamedPermName ns args a -namedPermName (NamedPerm_Opaque op) = opaquePermName op -namedPermName (NamedPerm_Rec rp) = recPermName rp -namedPermName (NamedPerm_Defined dp) = definedPermName dp - --- | Extract out the argument context of the name of a 'NamedPerm' -namedPermArgs :: NamedPerm ns args a -> CruCtx args -namedPermArgs = namedPermNameArgs . namedPermName - --- | An opaque named permission is just a name and a SAW core type given by --- identifier that it is translated to -data OpaquePerm b args a = OpaquePerm { - opaquePermName :: NamedPermName (OpaqueSort b) args a, - opaquePermTrans :: Ident - } - --- | The interpretation of a recursive permission as a reachability permission. --- Reachability permissions are recursive permissions of the form --- --- > reach = eq(x) | p --- --- where @reach@ occurs exactly once in @p@ in the form @reach@ and @x@ --- does not occur at all in @p@. This means their interpretations look like a --- list type, where the @eq(x)@ is the nil constructor and the @p@ is the --- cons. To support the transitivity rule, we need an append function for these --- lists, which is given by the transitivity method listed here, which has type --- --- > trans : forall args (x y:A), t args x -> t args y -> t args y --- --- where @args@ are the arguments and @A@ is the translation of type @a@ (which --- may correspond to 0 or more arguments) -data ReachMethods reach args a where - ReachMethods :: { - reachMethodTrans :: Ident - } -> ReachMethods (args :> a) a 'True - NoReachMethods :: ReachMethods args a 'False +-- | Get a list of 'Member' proofs for each expression in a 'PermExprs' list +getPermExprsMembers :: PermExprs args -> + [Some (Member args :: CrucibleType -> Type)] +getPermExprsMembers PExprs_Nil = [] +getPermExprsMembers (PExprs_Cons args _) = + map (\case Some memb -> Some (Member_Step memb)) (getPermExprsMembers args) + ++ [Some Member_Base] --- | A recursive permission is a disjunction of 1 or more permissions, each of --- which can contain the recursive permission itself. NOTE: it is an error to --- have an empty list of cases. A recursive permission is also associated with a --- SAW datatype, given by a SAW 'Ident', and each disjunctive permission case is --- associated with a constructor of that datatype. The @b@ flag indicates --- whether this recursive permission can be used as an atomic permission, which --- should be 'True' iff all of the cases are conjunctive permissions as in --- 'isConjPerm'. If the recursive permission is a reachability permission, then --- it also has a 'ReachMethods' structure. -data RecPerm b reach args a = RecPerm { - recPermName :: NamedPermName (RecursiveSort b reach) args a, - recPermTransType :: Ident, - recPermFoldFun :: Ident, - recPermUnfoldFun :: Ident, - recPermReachMethods :: ReachMethods args a reach, - recPermCases :: [Mb args (ValuePerm a)] - } +-- | Extract the name back out of the interpretation of a 'NamedPerm' +namedPermName :: NamedPerm ns args a -> NamedPermName ns args a +namedPermName (NamedPerm_Opaque op) = opaquePermName op +namedPermName (NamedPerm_Rec rp) = recPermName rp +namedPermName (NamedPerm_Defined dp) = definedPermName dp + +-- | Extract out the argument context of the name of a 'NamedPerm' +namedPermArgs :: NamedPerm ns args a -> CruCtx args +namedPermArgs = namedPermNameArgs . namedPermName -- | Get the @trans@ method from a 'RecPerm' for a reachability permission recPermTransMethod :: RecPerm b 'True args a -> Ident recPermTransMethod (RecPerm { recPermReachMethods = ReachMethods { .. }}) = reachMethodTrans --- | A defined permission is a name and a permission to which it is --- equivalent. The @b@ flag indicates whether this permission can be used as an --- atomic permission, which should be 'True' iff the associated permission is a --- conjunctive permission as in 'isConjPerm'. -data DefinedPerm b args a = DefinedPerm { - definedPermName :: NamedPermName (DefinedSort b) args a, - definedPermDef :: Mb args (ValuePerm a) -} - --- | A pair of a variable and its permission; we give it its own datatype to --- make certain typeclass instances (like pretty-printing) specific to it -data VarAndPerm a = VarAndPerm (ExprVar a) (ValuePerm a) - -- | Extract the permissions from a 'VarAndPerm' varAndPermPerm :: VarAndPerm a -> ValuePerm a varAndPermPerm (VarAndPerm _ p) = p @@ -2639,10 +2857,6 @@ varAndPermPerm (VarAndPerm _ p) = p -- | A pair that is specifically pretty-printing with a colon data ColonPair a b = ColonPair a b --- | A list of "distinguished" permissions to named variables --- FIXME: just call these VarsAndPerms or something like that... -type DistPerms = RAssign VarAndPerm - -- | Pattern for an empty 'DistPerms' pattern DistPermsNil :: () => (ps ~ RNil) => DistPerms ps pattern DistPermsNil = MNil @@ -2810,25 +3024,6 @@ lcurrentPerm :: PermExpr LifetimeType -> ExprVar LifetimeType -> lcurrentPerm PExpr_Always l2 = (l2, ValPerm_True) lcurrentPerm (PExpr_Var l) l2 = (l, ValPerm_LCurrent $ PExpr_Var l2) --- | A special-purpose 'DistPerms' that specifies a list of permissions needed --- to prove that a lifetime is current -data LifetimeCurrentPerms ps_l where - -- | The @always@ lifetime needs no proof that it is current - AlwaysCurrentPerms :: LifetimeCurrentPerms RNil - -- | A variable @l@ that is @lowned@ is current, requiring perms - -- - -- > l:lowned[ls](ps_in -o ps_out) - LOwnedCurrentPerms :: ExprVar LifetimeType -> [PermExpr LifetimeType] -> - LOwnedPerms ps_in -> LOwnedPerms ps_out -> - LifetimeCurrentPerms (RNil :> LifetimeType) - - -- | A variable @l@ that is @lcurrent@ during another lifetime @l'@ is - -- current, i.e., if @ps@ ensure @l'@ is current then we need perms - -- - -- > ps, l:lcurrent(l') - CurrentTransPerms :: LifetimeCurrentPerms ps_l -> ExprVar LifetimeType -> - LifetimeCurrentPerms (ps_l :> LifetimeType) - -- | Get the lifetime that a 'LifetimeCurrentPerms' is about lifetimeCurrentPermsLifetime :: LifetimeCurrentPerms ps_l -> PermExpr LifetimeType @@ -2854,33 +3049,6 @@ mbLifetimeCurrentPermsProxies mb_l = case mbMatch mb_l of [nuMP| CurrentTransPerms cur_ps _ |] -> mbLifetimeCurrentPermsProxies cur_ps :>: Proxy --- | A lifetime functor is a function from a lifetime plus a set of 0 or more --- rwmodalities to a permission that satisfies a number of properties discussed --- in Issue #62 (FIXME: copy those here). Rather than try to enforce these --- properties, we syntactically restrict lifetime functors to one of a few forms --- that are guaranteed to satisfy the properties. The @args@ type lists all --- arguments (which should all be rwmodalities) other than the lifetime --- argument. -data LifetimeFunctor args a where - -- | The functor @\(l,rw) -> [l]ptr((rw,off) |-> p)@ - LTFunctorField :: (1 <= w, KnownNat w, 1 <= sz, KnownNat sz) => - PermExpr (BVType w) -> ValuePerm (LLVMPointerType sz) -> - LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w) - - -- | The functor @\(l,rw) -> [l]array(rw,off, PermExpr (BVType w) -> - PermExpr (BVType w) -> Bytes -> - PermExpr (LLVMShapeType w) -> [LLVMArrayBorrow w] -> - LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w) - - -- | The functor @\(l,rw) -> [l]memblock(rw,off,len,sh) - LTFunctorBlock :: (1 <= w, KnownNat w) => - PermExpr (BVType w) -> PermExpr (BVType w) -> - PermExpr (LLVMShapeType w) -> - LifetimeFunctor (RNil :> RWModalityType) (LLVMPointerType w) - - -- FIXME: add functors for arrays and named permissions - -- | Apply a functor to its arguments to get out a permission ltFuncApply :: LifetimeFunctor args a -> PermExprs args -> PermExpr LifetimeType -> ValuePerm a @@ -3738,11 +3906,6 @@ llvmAtomicPermToBlock (Perm_LLVMArray ap) = llvmArrayPermToBlock ap llvmAtomicPermToBlock (Perm_LLVMBlock bp) = Just bp llvmAtomicPermToBlock _ = Nothing --- | An 'LLVMBlockPerm' with a proof that its type is valid -data SomeLLVMBlockPerm a where - SomeLLVMBlockPerm :: (1 <= w, KnownNat w) => LLVMBlockPerm w -> - SomeLLVMBlockPerm (LLVMPointerType w) - -- | Convert an atomic permission whose type is unknown to a @memblock@, if -- possible, along with a proof that its type is a valid llvm pointer type llvmAtomicPermToSomeBlock :: AtomicPerm a -> Maybe (SomeLLVMBlockPerm a) @@ -4020,10 +4183,6 @@ mbDisjBlockToSubShape :: Bool -> Mb ctx (LLVMBlockPerm w) -> mbDisjBlockToSubShape flag = mbMapCl ($(mkClosed [| disjBlockToSubShape |]) `clApply` toClosed flag) --- | A block permission in a binding at some unknown type -data SomeBindingLLVMBlockPerm w = - forall a. SomeBindingLLVMBlockPerm (Binding a (LLVMBlockPerm w)) - -- | Match an existential shape with the given bidning type matchExShape :: TypeRepr a -> PermExpr (LLVMShapeType w) -> Maybe (Binding a (PermExpr (LLVMShapeType w))) @@ -4151,27 +4310,6 @@ remLLVMBLockPermRange rng bp = return (bps_l ++ [bp_r]) --- | A tagged union shape is a shape of the form --- --- > sh1 orsh sh2 orsh ... orsh shn --- --- where each @shi@ is equivalent up to associativity of the @;@ operator to a --- shape of the form --- --- > fieldsh(eq(llvmword(bvi)));shi' --- --- That is, each disjunct of the shape starts with an equality permission that --- determines which disjunct should be used. These shapes are represented as a --- list of the disjuncts, which are tagged with the bitvector values @bvi@ used --- in the equality permission. -data TaggedUnionShape w sz - = TaggedUnionShape (NonEmpty (BV sz, PermExpr (LLVMShapeType w))) - --- | A 'TaggedUnionShape' with existentially quantified tag size -data SomeTaggedUnionShape w - = forall sz. (1 <= sz, KnownNat sz) => - SomeTaggedUnionShape (TaggedUnionShape w sz) - -- | Extract the disjunctive shapes from a 'TaggedUnionShape' taggedUnionDisjs :: TaggedUnionShape w sz -> [PermExpr (LLVMShapeType w)] taggedUnionDisjs (TaggedUnionShape disjs) = @@ -6058,12 +6196,6 @@ subst1 e = subst (singletonSubst e) -- because there are different ways one might do it, so we need to use -- OVERLAPPING and/or INCOHERENT pragmas for them --- | Like a substitution but assigns variables instead of arbitrary expressions --- to bound variables -data PermVarSubst (ctx :: RList CrucibleType) where - PermVarSubst_Nil :: PermVarSubst RNil - PermVarSubst_Cons :: PermVarSubst ctx -> Name tp -> PermVarSubst (ctx :> tp) - emptyVarSubst :: PermVarSubst RNil emptyVarSubst = PermVarSubst_Nil @@ -6275,7 +6407,7 @@ mbFactorNameBoundP :: PartialSubst vars -> mbFactorNameBoundP psubst (mbMatch -> [nuMP| BVFactor (BV.BV mb_n) mb_z |]) = let n = mbLift mb_n in case mbNameBoundP mb_z of - Left memb -> case psubstLookup psubst memb of + Left memb -> case psubstLookup psubst memb of Nothing -> Left (n, memb) Just e' -> Right (bvMultBV (BV.mkBV knownNat n) e') Right z -> Right (bvFactorExpr (BV.mkBV knownNat n) z) @@ -6903,7 +7035,7 @@ instance AbstractNamedShape w (AtomicPerm a) where abstractNSM (Perm_LLVMFunPtr tp p) = fmap (Perm_LLVMFunPtr tp) <$> abstractNSM p abstractNSM (Perm_LLVMBlockShape sh) = fmap Perm_LLVMBlockShape <$> abstractNSM sh abstractNSM Perm_IsLLVMPtr = pureBindingM Perm_IsLLVMPtr - abstractNSM (Perm_NamedConj n args off) = + abstractNSM (Perm_NamedConj n args off) = mbMap2 (Perm_NamedConj n) <$> abstractNSM args <*> abstractNSM off abstractNSM (Perm_LLVMFrame fp) = fmap Perm_LLVMFrame <$> abstractNSM fp abstractNSM (Perm_LOwned ls ps_in ps_out) = @@ -6964,57 +7096,6 @@ instance AbstractNamedShape w (FunPerm ghosts args gouts ret) where <*> abstractNSM perms_out -$(mkNuMatching [t| forall a . PermExpr a |]) -$(mkNuMatching [t| forall a . BVFactor a |]) -$(mkNuMatching [t| forall w. BVRange w |]) -$(mkNuMatching [t| forall w. BVProp w |]) -$(mkNuMatching [t| forall a . AtomicPerm a |]) -$(mkNuMatching [t| forall a . ValuePerm a |]) --- $(mkNuMatching [t| forall as. ValuePerms as |]) -$(mkNuMatching [t| forall a . VarAndPerm a |]) - -instance NuMatchingAny1 PermExpr where - nuMatchingAny1Proof = nuMatchingProof - -instance NuMatchingAny1 ValuePerm where - nuMatchingAny1Proof = nuMatchingProof - -instance NuMatchingAny1 VarAndPerm where - nuMatchingAny1Proof = nuMatchingProof - -$(mkNuMatching [t| forall w sz . LLVMFieldPerm w sz |]) -$(mkNuMatching [t| forall w . LLVMArrayPerm w |]) -$(mkNuMatching [t| forall w . LLVMBlockPerm w |]) -$(mkNuMatching [t| RWModality |]) -$(mkNuMatching [t| forall w . LLVMArrayIndex w |]) -$(mkNuMatching [t| forall w . LLVMArrayBorrow w |]) -$(mkNuMatching [t| forall w . LLVMFieldShape w |]) -$(mkNuMatching [t| forall w . LOwnedPerm w |]) -$(mkNuMatching [t| forall ghosts args gouts ret. FunPerm ghosts args gouts ret |]) -$(mkNuMatching [t| forall args ret. SomeFunPerm args ret |]) -$(mkNuMatching [t| forall ns. NameSortRepr ns |]) -$(mkNuMatching [t| forall ns args a. NameReachConstr ns args a |]) -$(mkNuMatching [t| forall ns args a. NamedPermName ns args a |]) -$(mkNuMatching [t| SomeNamedPermName |]) -$(mkNuMatching [t| forall b args w. NamedShape b args w |]) -$(mkNuMatching [t| forall b args w. NamedShapeBody b args w |]) -$(mkNuMatching [t| forall a. PermOffset a |]) -$(mkNuMatching [t| forall ns args a. NamedPerm ns args a |]) -$(mkNuMatching [t| forall b args a. OpaquePerm b args a |]) -$(mkNuMatching [t| forall args a reach. ReachMethods args a reach |]) -$(mkNuMatching [t| forall b reach args a. RecPerm b reach args a |]) -$(mkNuMatching [t| forall b args a. DefinedPerm b args a |]) -$(mkNuMatching [t| forall args a. LifetimeFunctor args a |]) -$(mkNuMatching [t| forall ps. LifetimeCurrentPerms ps |]) -$(mkNuMatching [t| forall a. SomeLLVMBlockPerm a |]) -$(mkNuMatching [t| forall w. SomeBindingLLVMBlockPerm w |]) - -instance NuMatchingAny1 LOwnedPerm where - nuMatchingAny1Proof = nuMatchingProof - -instance NuMatchingAny1 DistPerms where - nuMatchingAny1Proof = nuMatchingProof - instance Liftable RWModality where mbLift mb_rw = case mbMatch mb_rw of [nuMP| Write |] -> Write @@ -7062,49 +7143,6 @@ instance Liftable (ReachMethods args a reach) where -- * Permission Environments ---------------------------------------------------------------------- --- | An entry in a permission environment that associates a permission and --- corresponding SAW identifier with a Crucible function handle -data PermEnvFunEntry where - PermEnvFunEntry :: args ~ CtxToRList cargs => FnHandle cargs ret -> - FunPerm ghosts args gouts ret -> Ident -> - PermEnvFunEntry - --- | An existentially quantified 'NamedPerm' -data SomeNamedPerm where - SomeNamedPerm :: NamedPerm ns args a -> SomeNamedPerm - --- | An existentially quantified LLVM shape with arguments -data SomeNamedShape where - SomeNamedShape :: (1 <= w, KnownNat w) => NamedShape b args w -> - SomeNamedShape - --- | An entry in a permission environment that associates a 'GlobalSymbol' with --- a permission and a translation of that permission -data PermEnvGlobalEntry where - PermEnvGlobalEntry :: (1 <= w, KnownNat w) => GlobalSymbol -> - ValuePerm (LLVMPointerType w) -> [OpenTerm] -> - PermEnvGlobalEntry - --- | The different sorts hints for blocks -data BlockHintSort args where - -- | This hint specifies the ghost args and input permissions for a block - BlockEntryHintSort :: - CruCtx top_args -> CruCtx ghosts -> - MbValuePerms ((top_args :++: CtxToRList args) :++: ghosts) -> - BlockHintSort args - - -- | This hint says that the input perms for a block should be generalized - GenPermsHintSort :: BlockHintSort args - - -- | This hint says that a block should be a join point - JoinPointHintSort :: BlockHintSort args - --- | A hint for a block -data BlockHint blocks init ret args where - BlockHint :: FnHandle init ret -> Assignment CtxRepr blocks -> - BlockID blocks args -> BlockHintSort args -> - BlockHint blocks init ret args - -- | Get the 'BlockHintSort' for a 'BlockHint' blockHintSort :: BlockHint blocks init ret args -> BlockHintSort args blockHintSort (BlockHint _ _ _ sort) = sort @@ -7124,34 +7162,7 @@ isJoinPointHint :: BlockHintSort args -> Bool isJoinPointHint JoinPointHintSort = True isJoinPointHint _ = False --- FIXME: all the per-block hints - --- | A "hint" from the user for type-checking -data Hint where - Hint_Block :: BlockHint blocks init ret args -> Hint - --- | A permission environment that maps function names, permission names, and --- 'GlobalSymbols' to their respective permission structures -data PermEnv = PermEnv { - permEnvFunPerms :: [PermEnvFunEntry], - permEnvNamedPerms :: [SomeNamedPerm], - permEnvNamedShapes :: [SomeNamedShape], - permEnvGlobalSyms :: [PermEnvGlobalEntry], - permEnvHints :: [Hint] - } - -$(mkNuMatching [t| forall w sz. TaggedUnionShape w sz |]) -$(mkNuMatching [t| forall w. SomeTaggedUnionShape w |]) -$(mkNuMatching [t| forall ctx. PermVarSubst ctx |]) -$(mkNuMatching [t| PermEnvFunEntry |]) -$(mkNuMatching [t| SomeNamedPerm |]) -$(mkNuMatching [t| SomeNamedShape |]) -$(mkNuMatching [t| PermEnvGlobalEntry |]) -$(mkNuMatching [t| forall args. BlockHintSort args |]) -$(mkNuMatching [t| forall blocks init ret args. - BlockHint blocks init ret args |]) -$(mkNuMatching [t| Hint |]) -$(mkNuMatching [t| PermEnv |]) +-- FIXME: all the per-block hints -- | The empty 'PermEnv' emptyPermEnv :: PermEnv @@ -7439,9 +7450,6 @@ permSetVars = distPermSet :: DistPerms ps -> PermSet ps distPermSet perms = PermSet NameMap.empty perms --- NOTE: this instance would require a NuMatching instance for NameMap... --- $(mkNuMatching [t| forall ps. PermSet ps |]) - -- | The lens for the permissions associated with a given variable varPerm :: ExprVar a -> Lens' (PermSet ps) (ValuePerm a) varPerm x = diff --git a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs index 71c6fedef2..10092e415c 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs @@ -68,6 +68,50 @@ import Verifier.SAW.Heapster.CruUtil import Verifier.SAW.Heapster.Permissions +---------------------------------------------------------------------- +-- * Data types and related types +---------------------------------------------------------------------- + +-- | A permission of some llvm pointer type +data SomeLLVMPerm = + forall w. (1 <= w, KnownNat w) => SomeLLVMPerm (ValuePerm (LLVMPointerType w)) + +-- | An 'ArgLayoutPerm' is a set of permissions on a sequence of 0 or more +-- arguments, given by the @tps@ type-level argument. These permissions are +-- similar to the language of permissions on a Crucible struct, except that the +-- langauge is restricted to ensure that they can always be appended. +data ArgLayoutPerm ctx where + ALPerm :: RAssign ValuePerm (CtxToRList ctx) -> ArgLayoutPerm ctx + ALPerm_Or :: ArgLayoutPerm ctx -> ArgLayoutPerm ctx -> ArgLayoutPerm ctx + ALPerm_Exists :: KnownRepr TypeRepr a => + Binding a (ArgLayoutPerm ctx) -> ArgLayoutPerm ctx + +-- | An argument layout captures how argument values are laid out as a Crucible +-- struct of 0 or more machine words / fields +data ArgLayout where + ArgLayout :: CtxRepr ctx -> ArgLayoutPerm ctx -> ArgLayout + +-- | Function permission that is existential over all types (note that there +-- used to be 3 type variables instead of 4 for 'FunPerm', thus the name) +data Some3FunPerm = + forall ghosts args gouts ret. Some3FunPerm (FunPerm ghosts args gouts ret) + +-- | A name-binding over some list of types +data SomeTypedMb a where + SomeTypedMb :: CruCtx ctx -> Mb ctx a -> SomeTypedMb a + + +---------------------------------------------------------------------- +-- * Template Haskell–generated instances +---------------------------------------------------------------------- + +$(mkNuMatching [t| SomeLLVMPerm |]) +$(mkNuMatching [t| forall ctx. ArgLayoutPerm ctx |]) +$(mkNuMatching [t| ArgLayout |]) +$(mkNuMatching [t| Some3FunPerm |]) +$(mkNuMatching [t| forall a. NuMatching a => SomeTypedMb a |]) + + ---------------------------------------------------------------------- -- * Helper Definitions ---------------------------------------------------------------------- @@ -147,12 +191,6 @@ assocAppend4 fs1 ctx2 ctx3 ctx4 fs234 = let (fs2, fs3, fs4) = rlSplit3 ctx2 ctx3 ctx4 fs234 in RL.append (RL.append (RL.append fs1 fs2) fs3) fs4 --- | A permission of some llvm pointer type -data SomeLLVMPerm = - forall w. (1 <= w, KnownNat w) => SomeLLVMPerm (ValuePerm (LLVMPointerType w)) - -$(mkNuMatching [t| SomeLLVMPerm |]) - -- | Info used for converting Rust types to shapes -- NOTE: @rciRecType@ should probably have some info about lifetimes data RustConvInfo = @@ -607,16 +645,6 @@ instance RsConvert w (StructField Span) (PermExpr (LLVMShapeType w)) where -- * Computing the ABI-Specific Layout of Rust Types ---------------------------------------------------------------------- --- | An 'ArgLayoutPerm' is a set of permissions on a sequence of 0 or more --- arguments, given by the @tps@ type-level argument. These permissions are --- similar to the language of permissions on a Crucible struct, except that the --- langauge is restricted to ensure that they can always be appended. -data ArgLayoutPerm ctx where - ALPerm :: RAssign ValuePerm (CtxToRList ctx) -> ArgLayoutPerm ctx - ALPerm_Or :: ArgLayoutPerm ctx -> ArgLayoutPerm ctx -> ArgLayoutPerm ctx - ALPerm_Exists :: KnownRepr TypeRepr a => - Binding a (ArgLayoutPerm ctx) -> ArgLayoutPerm ctx - -- | Build an 'ArgLayoutPerm' that just assigns @true@ to every field trueArgLayoutPerm :: Assignment prx ctx -> ArgLayoutPerm ctx trueArgLayoutPerm ctx = ALPerm (RL.map (const ValPerm_True) $ assignToRList ctx) @@ -664,11 +692,6 @@ appendArgLayoutPerms ctx1 ctx2 p (ALPerm_Exists mb_q) = appendArgLayoutPerms ctx1 ctx2 (ALPerm ps) (ALPerm qs) = ALPerm $ assignToRListAppend ctx1 ctx2 ps qs --- | An argument layout captures how argument values are laid out as a Crucible --- struct of 0 or more machine words / fields -data ArgLayout where - ArgLayout :: CtxRepr ctx -> ArgLayoutPerm ctx -> ArgLayout - -- | Count the number of fields of an 'ArgLayout' argLayoutNumFields :: ArgLayout -> Int argLayoutNumFields (ArgLayout ctx _) = sizeInt $ size ctx @@ -754,11 +777,6 @@ shapeToBlockPerm :: (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w) -> Maybe (ValuePerm (LLVMPointerType w)) shapeToBlockPerm = fmap ValPerm_LLVMBlock . shapeToBlock --- | Function permission that is existential over all types (note that there --- used to be 3 type variables instead of 4 for 'FunPerm', thus the name) -data Some3FunPerm = - forall ghosts args gouts ret. Some3FunPerm (FunPerm ghosts args gouts ret) - instance PermPretty Some3FunPerm where permPrettyM (Some3FunPerm fun_perm) = permPrettyM fun_perm @@ -1041,10 +1059,6 @@ layoutFun abi arg_shs ret_sh = -- * Converting Function Types ---------------------------------------------------------------------- --- | A name-binding over some list of types -data SomeTypedMb a where - SomeTypedMb :: CruCtx ctx -> Mb ctx a -> SomeTypedMb a - instance Functor SomeTypedMb where fmap f (SomeTypedMb ctx mb_a) = SomeTypedMb ctx (fmap f mb_a) @@ -1474,9 +1488,3 @@ parseNamedShapeFromRustDecl env w str fail ("Error parsing top-level item: " ++ show err) parseNamedShapeFromRustDecl _ _ str = fail ("Malformed Rust type: " ++ str) - - -$(mkNuMatching [t| forall ctx. ArgLayoutPerm ctx |]) -$(mkNuMatching [t| ArgLayout |]) -$(mkNuMatching [t| Some3FunPerm |]) -$(mkNuMatching [t| forall a. NuMatching a => SomeTypedMb a |]) diff --git a/saw-core-what4/saw-core-what4.cabal b/saw-core-what4/saw-core-what4.cabal index b7504e73ba..050bb62b67 100644 --- a/saw-core-what4/saw-core-what4.cabal +++ b/saw-core-what4/saw-core-what4.cabal @@ -15,7 +15,7 @@ Description: library build-depends: - base == 4.*, + base >= 4.9, bv-sized >= 1.0.0, containers, lens, diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 6fe47a7c7c..232d685758 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -64,6 +64,7 @@ import qualified Control.Arrow as A import Data.Bits import Data.IORef +import Data.Kind (Type) import Data.List (genericTake) import Data.Map (Map) import qualified Data.Map as Map @@ -117,7 +118,7 @@ import Verifier.SAW.Simulator.What4.ReturnTrip --------------------------------------------------------------------- -- empty datatype to index (open) type families -- for this backend -data What4 (sym :: *) +data What4 (sym :: Type) -- | A What4 symbolic array where the domain and co-domain types do not appear -- in the type @@ -791,7 +792,7 @@ w4SolveBasic sym sc addlPrims ecMap ref unintSet t = ---------------------------------------------------------------------- -- Uninterpreted function cache -data SymFnWrapper sym :: Ctx.Ctx BaseType -> * where +data SymFnWrapper sym :: Ctx.Ctx BaseType -> Type where SymFnWrapper :: !(W.SymFn sym args ret) -> SymFnWrapper sym (args Ctx.::> ret) type SymFnCache sym = Map W.SolverSymbol (MapF (Assignment BaseTypeRepr) (SymFnWrapper sym)) @@ -842,7 +843,7 @@ parseUninterpreted :: parseUninterpreted sym ref app ty = case ty of VPiType nm _ body - -> pure $ VFun nm $ \x -> + -> pure $ VFun nm $ \x -> do x' <- force x app' <- applyUnintApp sym app x' t2 <- applyPiBody body (ready x') diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index 0a45b0e85e..539fbe4ec6 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -34,7 +34,7 @@ common errors -Werror=overlapping-patterns common deps - build-depends: base >=4.11.1.0 && <4.15, + build-depends: base >=4.11.1.0 && <4.16, aeson >= 1.4.2 && < 2.0, aig, argo, diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index c7088a055f..4dc5da2414 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1735,7 +1735,7 @@ llvm_execute_func :: [AllLLVM MS.SetupValue] -> LLVMCrucibleSetupM () llvm_execute_func args = - LLVMCrucibleSetupM $ Setup.crucible_execute_func (map getAllLLVM args) + LLVMCrucibleSetupM $ Setup.crucible_execute_func (map (\a -> getAllLLVM a) args) getLLVMCrucibleContext :: CrucibleSetup (LLVM arch) (LLVMCrucibleContext arch) getLLVMCrucibleContext = view Setup.csCrucibleContext <$> get @@ -1837,7 +1837,7 @@ constructExpandedSetupValue cc sc loc t = traverse (constructExpandedSetupValue cc sc loc) (Crucible.siFieldTypes si) -- FIXME: should this always be unpacked? - pure $ mkAllLLVM $ SetupStruct () False $ map getAllLLVM fields + pure $ mkAllLLVM $ SetupStruct () False $ map (\a -> getAllLLVM a) fields Crucible.PtrType symTy -> case Crucible.asMemType symTy of @@ -1851,7 +1851,7 @@ constructExpandedSetupValue cc sc loc t = Crucible.ArrayType n memTy -> do elements_ <- replicateM (fromIntegral n) (constructExpandedSetupValue cc sc loc memTy) - pure $ mkAllLLVM $ SetupArray () $ map getAllLLVM elements_ + pure $ mkAllLLVM $ SetupArray () $ map (\a -> getAllLLVM a) elements_ Crucible.FloatType -> failUnsupportedType "Float" Crucible.DoubleType -> failUnsupportedType "Double" diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index 49b7907ca0..1a76ba1aa6 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -554,10 +554,10 @@ anySetupTerm :: TypedTerm -> AllLLVM MS.SetupValue anySetupTerm typedTerm = mkAllLLVM (MS.SetupTerm typedTerm) anySetupArray :: [AllLLVM MS.SetupValue] -> AllLLVM MS.SetupValue -anySetupArray vals = mkAllLLVM (MS.SetupArray () $ map getAllLLVM vals) +anySetupArray vals = mkAllLLVM (MS.SetupArray () $ map (\a -> getAllLLVM a) vals) anySetupStruct :: Bool -> [AllLLVM MS.SetupValue] -> AllLLVM MS.SetupValue -anySetupStruct b vals = mkAllLLVM (MS.SetupStruct () b $ map getAllLLVM vals) +anySetupStruct b vals = mkAllLLVM (MS.SetupStruct () b $ map (\a -> getAllLLVM a) vals) anySetupElem :: AllLLVM MS.SetupValue -> Int -> AllLLVM MS.SetupValue anySetupElem val idx = mkAllLLVM (MS.SetupElem () (getAllLLVM val) idx) diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 017593d5e9..0db88b49a8 100644 --- a/src/SAWScript/Crucible/LLVM/X86.hs +++ b/src/SAWScript/Crucible/LLVM/X86.hs @@ -423,7 +423,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se ctx :: C.SimContext (Macaw.MacawSimulatorState Sym) Sym (Macaw.MacawExt Macaw.X86_64) ctx = C.SimContext { C._ctxBackend = SomeBackend bak - , C.ctxSolverProof = id + , C.ctxSolverProof = \x -> x , C.ctxIntrinsicTypes = C.LLVM.llvmIntrinsicTypes , C.simHandleAllocator = halloc , C.printHandle = stdout diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 8bc714696f..917d399452 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -646,7 +646,7 @@ instance Applicative LLVMCrucibleSetupM where instance Monad LLVMCrucibleSetupM where return = pure LLVMCrucibleSetupM m >>= f = - LLVMCrucibleSetupM (m >>= runLLVMCrucibleSetupM . f) + LLVMCrucibleSetupM (m >>= \x -> runLLVMCrucibleSetupM (f x)) throwCrucibleSetup :: ProgramLoc -> String -> CrucibleSetup ext a throwCrucibleSetup loc msg = X.throw $ SS.CrucibleSetupException loc msg From 349b4b21553fb7376e787a356e1add82272e19da Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 26 Jan 2022 11:42:06 -0500 Subject: [PATCH 2/4] Regenerate cabal.GHC-8.8.4.config --- cabal.GHC-8.8.4.config | 310 ++++++++++++++++++++++++----------------- 1 file changed, 182 insertions(+), 128 deletions(-) diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config index f8f48bdbaf..d80be71981 100644 --- a/cabal.GHC-8.8.4.config +++ b/cabal.GHC-8.8.4.config @@ -1,6 +1,6 @@ +active-repositories: hackage.haskell.org:merge constraints: any.Cabal ==3.0.1.0, - any.FloatingHex ==0.5, - any.Glob ==0.10.1, + any.Glob ==0.10.2, any.GraphSCC ==1.0.4, GraphSCC -use-maps, any.HUnit ==1.6.2.0, @@ -8,124 +8,130 @@ constraints: any.Cabal ==3.0.1.0, any.IntervalMap ==0.6.1.2, any.MemoTrie ==0.6.10, MemoTrie -examples, - any.MonadRandom ==0.5.2, + any.MonadRandom ==0.5.3, + any.OneTuple ==0.3.1, any.Only ==0.1, any.QuickCheck ==2.14.2, QuickCheck -old-random +templatehaskell, - any.StateVar ==1.2.1, + any.StateVar ==1.2.2, any.abstract-deque ==0.3, abstract-deque -usecas, any.abstract-par ==0.3.3, any.adjunctions ==4.4, any.aeson ==1.5.6.0, aeson -bytestring-builder -cffi -developer -fast, - any.alex ==3.2.6, - alex +small_base, - any.ansi-terminal ==0.11, + any.aeson-typescript ==0.3.0.1, + any.alex ==3.2.7.1, + any.ansi-terminal ==0.11.1, ansi-terminal -example, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, any.appar ==0.1.8, + any.arithmoi ==0.12.0.1, any.array ==0.5.4.0, any.asn1-encoding ==0.9.6, any.asn1-parse ==0.9.5, any.asn1-types ==0.3.4, any.assoc ==1.0.2, - any.async ==2.2.3, + any.async ==2.2.4, async -bench, - any.attoparsec ==0.13.2.5, + any.attoparsec ==0.14.4, attoparsec -developer, any.auto-update ==0.1.6, any.base ==4.13.0.0, any.base-compat ==0.11.2, any.base-compat-batteries ==0.11.2, - any.base-orphans ==0.8.4, - any.base16-bytestring ==1.0.1.0, - any.base64-bytestring ==1.2.0.1, - any.basement ==0.0.11, - any.bifunctors ==5.5.7, + any.base-orphans ==0.8.6, + any.base16-bytestring ==1.0.2.0, + any.base64-bytestring ==1.2.1.0, + any.basement ==0.0.12, + any.bifunctors ==5.5.11, bifunctors +semigroups +tagged, any.bimap ==0.4.0, any.binary ==0.8.7.0, - any.binary-orphans ==1.0.1, + any.binary-orphans ==1.0.2, + any.binary-parsers ==0.2.4.0, any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.2.1, + any.blaze-builder ==0.4.2.2, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.2.8, - any.boomerang ==1.4.6, + any.boomerang ==1.4.7, any.bsb-http-chunked ==0.0.0.4, - any.bv-sized ==1.0.2, + any.bv-sized ==1.0.3, any.byteorder ==1.0.4, any.bytestring ==0.10.10.1, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, - any.c2hs ==0.28.7, - c2hs +base3 -regression, - any.cabal-doctest ==1.0.8, - any.call-stack ==0.3.0, + any.bytestring-lexing ==0.5.0.8, + any.cabal-doctest ==1.0.9, + any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cassava ==0.5.2.0, cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.1, + any.cereal ==0.5.8.2, cereal -bytestring-builder, + any.chimera ==0.3.2.0, + chimera +representable, any.clock ==0.8.2, clock -llvm, any.code-page ==0.2.1, - any.colour ==2.3.5, + any.colour ==2.3.6, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, - any.concurrent-output ==1.10.12, - any.conduit ==1.3.4.1, + any.concurrent-extra ==0.7.0.12, + any.concurrent-output ==1.10.14, + any.conduit ==1.3.4.2, any.conduit-extra ==1.3.5, any.config-schema ==1.2.2.0, - any.config-value ==0.8.1, - any.constraints ==0.12, + any.config-value ==0.8.2, + any.constraints ==0.13.2, any.containers ==0.6.2.1, - any.contravariant ==1.5.3, + any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, any.cookie ==0.4.5, - any.crackNum ==2.4, - any.criterion ==1.5.9.0, + any.criterion ==1.5.12.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.2.0, + any.criterion-measurement ==0.1.3.0, criterion-measurement -fast, crucible +unsafe-operations, - any.cryptohash-md5 ==0.11.100.1, - any.cryptohash-sha1 ==0.11.100.1, + any.cryptohash-md5 ==0.11.101.0, + any.cryptohash-sha1 ==0.11.101.0, cryptol +relocatable -static, - any.cryptonite ==0.28, + cryptol-remote-api -notthreaded -static, + any.cryptonite ==0.29, cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, any.cryptonite-conduit ==0.2.2, any.data-accessor ==0.2.3, data-accessor +category +monadfail +splitbase, any.data-binary-ieee754 ==0.4.4, any.data-default-class ==0.1.2.0, - any.data-fix ==0.3.1, + any.data-fix ==0.3.2, any.data-inttrie ==0.1.4, any.data-ref ==0.0.2, any.deepseq ==1.4.4.0, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.5.9, + any.deriving-compat ==0.6, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.0, any.distributive ==0.6.2.1, distributive +semigroups +tagged, any.dlist ==1.0, dlist -werror, - any.doctest ==0.16.3, + any.doctest ==0.20.0, any.dotgen ==0.4.3, dotgen -devel, any.easy-file ==0.2.2, any.either ==5.0.1.1, - any.entropy ==0.4.1.6, + any.entropy ==0.4.1.7, entropy -halvm, any.erf ==2.0.0.0, + any.errors ==2.3.0, + any.exact-pi ==0.5.0.1, any.exceptions ==0.10.4, exceptions +transformers-0-4, any.executable-path ==0.0.3.1, - any.extra ==1.7.9, + any.extensible-exceptions ==0.1.1.4, + any.extra ==1.7.10, any.fail ==4.9.0.0, - any.fast-logger ==3.0.3, + any.fast-logger ==3.1.1, any.fgl ==5.7.0.3, fgl +containers042, any.fgl-visualize ==0.1.0.1, @@ -133,10 +139,13 @@ constraints: any.Cabal ==3.0.1.0, any.filemanip ==0.3.6.3, any.filepath ==1.4.2.1, any.fingertree ==0.1.4.2, - any.free ==5.1.3, - any.generic-deriving ==1.13.1, + any.free ==5.1.7, + any.generic-deriving ==1.14.1, generic-deriving +base-4-9, - any.generic-random ==1.3.0.1, + any.generic-lens ==2.2.1.0, + any.generic-lens-core ==2.2.1.0, + any.generic-random ==1.5.0.1, + generic-random -enable-inspect, any.ghc ==8.8.4, any.ghc-boot ==8.8.4, any.ghc-boot-th ==8.8.4, @@ -144,88 +153,104 @@ constraints: any.Cabal ==3.0.1.0, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.5.3, any.ghci ==8.8.4, + any.githash ==0.1.6.2, any.gitrev ==1.3.1, + any.graphviz ==2999.20.1.0, + graphviz -test-parsing, any.happy ==1.20.0, - any.hashable ==1.3.4.1, + any.hashable ==1.3.5.0, hashable +integer-gmp -random-initial-seed, - any.hashtables ==1.2.4.1, + any.hashtables ==1.2.4.2, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, any.haskeline ==0.7.5.0, any.haskell-lexer ==1.1, any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.7, - any.hedgehog ==1.0.4, + any.haskell-src-meta ==0.8.8, + any.hedgehog ==1.0.5, + any.hedgehog-classes ==0.2.5.3, + hedgehog-classes +aeson +comonad +primitive +semirings +vector, any.heredoc ==0.2.0.0, any.hobbits ==1.4, + any.hostname ==1.0, any.hourglass ==0.2.12, any.hpc ==0.6.0.3, - any.hsc2hs ==0.68.7, + any.hsc2hs ==0.68.8, hsc2hs -in-ghc-tree, - any.hspec ==2.7.8, - any.hspec-core ==2.7.8, - any.hspec-discover ==2.7.8, + any.hspec ==2.9.4, + any.hspec-core ==2.9.4, + any.hspec-discover ==2.9.4, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, - any.http2 ==2.0.6, - http2 -devel, - any.indexed-traversable ==0.1.1, + any.http2 ==3.0.2, + http2 -devel -doc -h2spec, + any.indexed-profunctors ==0.1.1, + any.indexed-traversable ==0.1.2, + any.indexed-traversable-instances ==0.1.1, any.integer-gmp ==1.0.2.0, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, + any.integer-roots ==1.0.2.0, any.interpolate ==0.2.1, - any.invariant ==0.5.3, - any.io-streams ==1.5.2.0, + any.invariant ==0.5.5, + any.io-streams ==1.5.2.1, io-streams +network -nointeractivetests +zlib, - any.iproute ==1.7.10, + any.iproute ==1.7.12, any.itanium-abi ==0.1.1.1, any.js-chart ==2.9.4.1, any.json ==0.10, json +generic -mapdict +parsec +pretty +split-base, - any.kan-extensions ==5.2.2, - any.language-c ==0.8.3, - language-c -allwarnings +iecfpextension +separatesyb +usebytestrings, - any.lens ==4.19.2, - lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.2, + any.kan-extensions ==5.2.3, + any.kvitable ==1.0.0.0, + language-rust +enablequasiquotes +usebytestrings, + any.lens ==5.0.1, + lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, + any.libBF ==0.6.3, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.1.3, + any.lifted-async ==0.10.2.2, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, any.logict ==0.7.0.3, - any.math-functions ==0.3.4.1, + any.lucid ==2.9.12.1, + any.lumberjack ==1.0.0.1, + any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, - any.megaparsec ==8.0.0, + any.megaparsec ==9.0.1, megaparsec -dev, - any.memory ==0.15.0, + any.memory ==0.16.0, memory +support_basement +support_bytestring +support_deepseq +support_foundation, any.microlens ==0.4.12.0, - any.microlens-th ==0.4.3.6, - any.microstache ==1.0.1.2, + any.microlens-th ==0.4.3.10, + any.microstache ==1.0.2, any.mmorph ==1.1.5, - any.modern-uri ==0.3.4.1, + any.mod ==0.1.2.2, + mod +semirings +vector, + any.modern-uri ==0.3.4.2, modern-uri -dev, - any.monad-control ==1.0.2.3, + any.monad-control ==1.0.3.1, any.monad-par ==0.3.5, monad-par -chaselev -newgeneric, any.monad-par-extras ==0.3.3, any.monadLib ==3.10, - any.mono-traversable ==1.0.15.1, + any.mono-traversable ==1.0.15.3, any.mtl ==2.2.2, - any.mwc-random ==0.15.0.1, + any.mwc-random ==0.15.0.2, any.nats ==1.1.2, nats +binary +hashable +template-haskell, - any.network ==3.1.2.1, + any.network ==3.1.2.7, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.0.10, - any.newtype-generics ==0.6, + any.newtype-generics ==0.6.1, + any.numtype-dk ==0.5.0.3, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, + any.optparse-simple ==0.1.1.4, + optparse-simple -build-example, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, parameterized-utils +unsafe-operations, @@ -233,129 +258,158 @@ constraints: any.Cabal ==3.0.1.0, any.parser-combinators ==1.3.0, parser-combinators -dev, any.pem ==0.2.4, + any.polyparse ==1.13, any.pretty ==1.1.3.6, any.pretty-hex ==1.1, any.pretty-show ==1.10, - any.prettyprinter ==1.7.0, - prettyprinter -buildreadme, - any.prettyprinter-ansi-terminal ==1.1.2, - any.primitive ==0.7.1.0, + any.prettyprinter ==1.7.1, + prettyprinter -buildreadme +text, + any.prettyprinter-ansi-terminal ==1.1.3, + any.primitive ==0.7.3.0, any.process ==1.6.9.0, - any.profunctors ==5.6, - any.psqueues ==0.2.7.2, - any.quickcheck-instances ==0.3.25.2, + any.profunctors ==5.6.2, + any.psqueues ==0.2.7.3, + any.quickcheck-instances ==0.3.27, quickcheck-instances -bytestring-builder, any.quickcheck-io ==0.2.0, - any.random ==1.2.0, + any.random ==1.2.1, any.raw-strings-qq ==1.1, any.reflection ==2.1.6, reflection -slow +template-haskell, - any.regex-base ==0.94.0.1, + any.regex-base ==0.94.0.2, any.regex-compat ==0.95.2.1, - any.resourcet ==1.2.4.2, + any.regex-posix ==0.96.0.1, + regex-posix -_regex-posix-clib, + any.resourcet ==1.2.4.3, any.rts ==1.0, + any.s-cargot ==0.1.4.0, + s-cargot -build-example, any.safe ==0.3.19, any.sbv ==8.15, - sbv -skiphlinttester, - any.scientific ==0.3.6.2, + any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12, - any.semigroupoids ==5.3.4, - semigroupoids +comonad +containers +contravariant +distributive +doctests +tagged +unordered-containers, - any.semigroups ==0.19.1, + any.semigroupoids ==5.3.7, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, + any.semigroups ==0.19.2, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, + any.semirings ==0.6, + semirings +containers +unordered-containers, any.setenv ==0.1.1.3, - any.silently ==1.2.5.1, + any.silently ==1.2.5.2, any.simple-get-opt ==0.4, any.simple-sendfile ==0.2.30, simple-sendfile +allow-bsd, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1, any.split ==0.2.3.4, - any.splitmix ==0.1.0.3, + any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.15.2.0, + any.statistics ==0.16.0.1, any.stm ==2.5.0.0, - any.streaming-commons ==0.2.2.1, + any.streaming-commons ==0.2.2.3, streaming-commons -use-bytestring-builder, any.strict ==0.4.0.1, strict +assoc, + any.string-interpolate ==0.3.1.1, + string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.1, any.tagged ==0.8.6.1, tagged +deepseq +transformers, - any.tasty ==1.2.3, - tasty +clock, - any.tasty-ant-xml ==1.1.7, - any.tasty-hedgehog ==1.0.1.0, - any.tasty-hspec ==1.1.6, + any.tasty ==1.4.2.1, + tasty +clock +unix, + any.tasty-ant-xml ==1.1.8, + any.tasty-checklist ==1.0.3.0, + any.tasty-expected-failure ==0.12.3, + any.tasty-golden ==2.3.5, + tasty-golden -build-example, + any.tasty-hedgehog ==1.1.0.0, + any.tasty-hspec ==1.2, any.tasty-hunit ==0.10.0.3, - any.tasty-quickcheck ==0.10.1.2, + any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==1.1.0.0, + any.tasty-sugar ==1.1.1.0, any.template-haskell ==2.15.0.0, any.temporary ==1.3, any.terminal-size ==0.3.2.1, any.terminfo ==0.4.1.4, + any.test-framework ==0.8.2.0, + any.test-framework-hunit ==0.3.0.2, + test-framework-hunit -base3 +base4, any.text ==1.2.4.0, - any.text-short ==0.1.3, + any.text-conversions ==0.3.1, + any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.4.2.0, - any.th-compat ==0.1.1, - any.th-expand-syns ==0.4.6.0, + any.th-abstraction ==0.4.3.0, + any.th-compat ==0.1.3, + any.th-expand-syns ==0.4.9.0, any.th-lift ==0.8.2, - any.th-lift-instances ==0.1.18, - any.th-orphans ==0.13.11, - any.th-reify-many ==0.1.9, + any.th-lift-instances ==0.1.19, + any.th-orphans ==0.13.12, + any.th-reify-many ==0.1.10, any.these ==1.1.1.1, these +assoc, any.time ==1.9.3, - any.time-compat ==1.9.5, + any.time-compat ==1.9.6.1, time-compat -old-locale, any.time-manager ==0.0.0, + any.tls ==1.5.7, + tls +compat -hans +network, + any.tls-session-manager ==0.0.4, any.transformers ==0.5.6.2, - any.transformers-base ==0.4.5.2, + any.transformers-base ==0.4.6, transformers-base +orphaninstances, any.transformers-compat ==0.6.6, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, - any.typed-process ==0.2.6.0, + any.typed-process ==0.2.8.0, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, + any.unix ==2.7.2.2, + any.unix-compat ==0.5.4, + unix-compat -old-time, + any.unix-time ==0.4.7, + any.unliftio ==0.2.20, any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.13.0, + any.unordered-containers ==0.2.16.0, unordered-containers -debug, any.utf8-string ==1.0.2, - any.uuid ==1.3.14, - any.uuid-types ==1.0.4, + any.uuid ==1.3.15, + any.uuid-types ==1.0.5, any.vault ==0.3.1.5, vault +useghc, - any.vector ==0.12.2.0, + any.vector ==0.12.3.1, vector +boundschecks -internalchecks -unsafechecks -wall, any.vector-algorithms ==0.8.0.4, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-binary-instances ==0.2.5.1, - any.vector-th-unbox ==0.2.1.9, - any.versions ==4.0.3, + any.vector-binary-instances ==0.2.5.2, + any.vector-th-unbox ==0.2.2, + any.versions ==5.0.2, any.void ==0.7.3, void -safe, any.wai ==3.2.3, - any.wai-extra ==3.1.6, + any.wai-extra ==3.1.8, wai-extra -build-example, - any.wai-logger ==2.3.6, - any.warp ==3.3.14, + any.wai-logger ==2.3.7, + any.warp ==3.3.18, warp +allow-sendfilefd -network-bytestring -warp-debug, + any.warp-tls ==3.3.2, any.wcwidth ==0.0.2, wcwidth -cli +split-base, + any.weigh ==0.0.16, what4 -drealtestdisable -solvertests -stptestdisable, - any.xdg-basedir ==0.2.2, any.wl-pprint-annotated ==0.1.0.1, + any.wl-pprint-text ==1.2.0.2, any.word8 ==0.1.3, - any.x509 ==1.7.5, + any.x509 ==1.7.6, + any.x509-store ==1.6.9, + any.x509-validation ==1.6.12, any.xml ==1.3.14, - any.yaml ==0.11.5.0, + any.yaml ==0.11.7.0, yaml +no-examples +no-exe, - any.zenc ==0.1.1, + any.zenc ==0.1.2, any.zlib ==0.6.2.3, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 +index-state: hackage.haskell.org 2022-01-24T13:23:29Z From 501f98be91c44a4b1d0982e4ddf62199d2fc1806 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 26 Jan 2022 11:47:38 -0500 Subject: [PATCH 3/4] CI: Consistently use GHC 8.10.7 --- .github/workflows/ci.yml | 18 +- cabal.GHC-8.10.3.config | 358 ------------------ ...C-8.10.4.config => cabal.GHC-8.10.7.config | 321 +++++++++------- 3 files changed, 188 insertions(+), 509 deletions(-) delete mode 100644 cabal.GHC-8.10.3.config rename cabal.GHC-8.10.4.config => cabal.GHC-8.10.7.config (58%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f3bc97cdfd..b3f3047f82 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,5 +1,5 @@ # Overall configuration notes: -# - Artifact uploads for binaries are from GHC 8.10.3 +# - Artifact uploads for binaries are from GHC 8.10.7 # - Builds for Ubuntu happen on 18.04 (would like to include 20.04, in addition) # - Builds for macOS builds on 10.15 (to avoid GHC bug on macOS 11; solvable with GHC > 8.10.4) # - Docker builds happen nightly, on manual invocation, and on release branch commits @@ -68,7 +68,7 @@ jobs: fail-fast: false matrix: os: [ubuntu-18.04, macos-10.15, windows-latest] - ghc: ["8.8.4", "8.10.3"] + ghc: ["8.8.4", "8.10.7"] exclude: - os: windows-latest ghc: "8.8.4" @@ -133,7 +133,7 @@ jobs: dest: dist-tests - uses: actions/upload-artifact@v2 - if: "matrix.ghc == '8.10.3'" + if: "matrix.ghc == '8.10.7'" with: path: dist-tests name: dist-tests-${{ matrix.os }} @@ -150,21 +150,21 @@ jobs: - shell: bash run: .github/ci.sh zip_dist_with_solvers $NAME-with-solvers - - if: matrix.ghc == '8.10.3' && needs.config.outputs.release == 'true' + - if: matrix.ghc == '8.10.7' && needs.config.outputs.release == 'true' shell: bash env: SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }} SIGNING_KEY: ${{ secrets.SIGNING_KEY }} run: .github/ci.sh sign $NAME.tar.gz - - if: matrix.ghc == '8.10.3' && needs.config.outputs.release == 'true' + - if: matrix.ghc == '8.10.7' && needs.config.outputs.release == 'true' shell: bash env: SIGNING_PASSPHRASE: ${{ secrets.SIGNING_PASSPHRASE }} SIGNING_KEY: ${{ secrets.SIGNING_KEY }} run: .github/ci.sh sign $NAME-with-solvers.tar.gz - - if: matrix.ghc == '8.10.3' + - if: matrix.ghc == '8.10.7' uses: actions/upload-artifact@v2 with: name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }}) @@ -172,7 +172,7 @@ jobs: if-no-files-found: error retention-days: ${{ needs.config.outputs.retention-days }} - - if: matrix.ghc == '8.10.3' + - if: matrix.ghc == '8.10.7' uses: actions/upload-artifact@v2 with: name: ${{ steps.config.outputs.name }} (GHC ${{ matrix.ghc }}) @@ -180,7 +180,7 @@ jobs: if-no-files-found: error retention-days: ${{ needs.config.outputs.retention-days }} - - if: "matrix.ghc == '8.10.3'" + - if: "matrix.ghc == '8.10.7'" uses: actions/upload-artifact@v2 with: path: dist/bin @@ -474,7 +474,7 @@ jobs: - hmac-failure - awslc - blst - ghc: ["8.10.3"] + ghc: ["8.10.7"] steps: - uses: actions/checkout@v2 - run: | diff --git a/cabal.GHC-8.10.3.config b/cabal.GHC-8.10.3.config deleted file mode 100644 index 4dcb82d68c..0000000000 --- a/cabal.GHC-8.10.3.config +++ /dev/null @@ -1,358 +0,0 @@ -constraints: any.Cabal ==3.2.1.0, - any.FloatingHex ==0.5, - any.Glob ==0.10.1, - any.GraphSCC ==1.0.4, - GraphSCC -use-maps, - any.HUnit ==1.6.2.0, - any.IfElse ==0.85, - any.IntervalMap ==0.6.1.2, - any.MemoTrie ==0.6.10, - MemoTrie -examples, - any.MonadRandom ==0.5.2, - any.Only ==0.1, - any.QuickCheck ==2.14.2, - QuickCheck -old-random +templatehaskell, - any.StateVar ==1.2.1, - any.abstract-deque ==0.3, - abstract-deque -usecas, - any.abstract-par ==0.3.3, - any.adjunctions ==4.4, - any.aeson ==1.5.6.0, - aeson -bytestring-builder -cffi -developer -fast, - any.alex ==3.2.6, - alex +small_base, - any.ansi-terminal ==0.11, - ansi-terminal -example, - any.ansi-wl-pprint ==0.6.9, - ansi-wl-pprint -example, - any.appar ==0.1.8, - any.array ==0.5.4.0, - any.asn1-encoding ==0.9.6, - any.asn1-parse ==0.9.5, - any.asn1-types ==0.3.4, - any.assoc ==1.0.2, - any.async ==2.2.3, - async -bench, - any.attoparsec ==0.13.2.5, - attoparsec -developer, - any.auto-update ==0.1.6, - any.base ==4.14.1.0, - any.base-compat ==0.11.2, - any.base-compat-batteries ==0.11.2, - any.base-orphans ==0.8.4, - any.base16-bytestring ==1.0.1.0, - any.base64-bytestring ==1.2.0.1, - any.basement ==0.0.11, - any.bifunctors ==5.5.7, - bifunctors +semigroups +tagged, - any.bimap ==0.4.0, - any.binary ==0.8.8.0, - any.binary-orphans ==1.0.1, - any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.2.1, - any.blaze-html ==0.9.1.2, - any.blaze-markup ==0.8.2.8, - any.boomerang ==1.4.6, - any.bsb-http-chunked ==0.0.0.4, - any.bv-sized ==1.0.2, - any.byteorder ==1.0.4, - any.bytestring ==0.10.12.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, - any.c2hs ==0.28.7, - c2hs +base3 -regression, - any.cabal-doctest ==1.0.8, - any.call-stack ==0.3.0, - any.case-insensitive ==1.2.1.0, - any.cassava ==0.5.2.0, - cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.1, - cereal -bytestring-builder, - any.clock ==0.8.2, - clock -llvm, - any.code-page ==0.2.1, - any.colour ==2.3.5, - any.comonad ==5.0.8, - comonad +containers +distributive +indexed-traversable, - any.concurrent-output ==1.10.12, - any.conduit ==1.3.4.1, - any.conduit-extra ==1.3.5, - any.config-schema ==1.2.2.0, - any.config-value ==0.8.1, - any.constraints ==0.12, - any.containers ==0.6.2.1, - any.contravariant ==1.5.3, - contravariant +semigroups +statevar +tagged, - any.cookie ==0.4.5, - any.crackNum ==2.4, - any.criterion ==1.5.9.0, - criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.2.0, - criterion-measurement -fast, - crucible +unsafe-operations, - any.cryptohash-md5 ==0.11.100.1, - any.cryptohash-sha1 ==0.11.100.1, - cryptol +relocatable -static, - any.cryptonite ==0.28, - cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, - any.cryptonite-conduit ==0.2.2, - any.data-accessor ==0.2.3, - data-accessor +category +monadfail +splitbase, - any.data-binary-ieee754 ==0.4.4, - any.data-default-class ==0.1.2.0, - any.data-fix ==0.3.1, - any.data-inttrie ==0.1.4, - any.data-ref ==0.0.2, - any.deepseq ==1.4.4.0, - any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.5.9, - deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, - any.directory ==1.3.6.0, - any.distributive ==0.6.2.1, - distributive +semigroups +tagged, - any.dlist ==1.0, - dlist -werror, - any.doctest ==0.16.3, - any.dotgen ==0.4.3, - dotgen -devel, - any.easy-file ==0.2.2, - any.either ==5.0.1.1, - any.entropy ==0.4.1.6, - entropy -halvm, - any.erf ==2.0.0.0, - any.exceptions ==0.10.4, - any.executable-path ==0.0.3.1, - any.extra ==1.7.9, - any.fail ==4.9.0.0, - any.fast-logger ==3.0.3, - any.fgl ==5.7.0.3, - fgl +containers042, - any.fgl-visualize ==0.1.0.1, - any.filelock ==0.1.1.5, - any.filemanip ==0.3.6.3, - any.filepath ==1.4.2.1, - any.fingertree ==0.1.4.2, - any.free ==5.1.3, - any.generic-deriving ==1.13.1, - generic-deriving +base-4-9, - any.generic-random ==1.3.0.1, - any.ghc ==8.10.3, - any.ghc-boot ==8.10.3, - any.ghc-boot-th ==8.10.3, - any.ghc-heap ==8.10.3, - any.ghc-paths ==0.1.0.12, - any.ghc-prim ==0.6.1, - any.ghci ==8.10.3, - any.gitrev ==1.3.1, - any.happy ==1.20.0, - any.hashable ==1.3.4.1, - hashable +integer-gmp -random-initial-seed, - any.hashtables ==1.2.4.1, - hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, - any.haskeline ==0.8.0.1, - any.haskell-lexer ==1.1, - any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.7, - any.hedgehog ==1.0.4, - any.heredoc ==0.2.0.0, - any.hourglass ==0.2.12, - any.hpc ==0.6.1.0, - any.hsc2hs ==0.68.7, - hsc2hs -in-ghc-tree, - any.hspec ==2.7.8, - any.hspec-core ==2.7.8, - any.hspec-discover ==2.7.8, - any.hspec-expectations ==0.8.2, - any.http-date ==0.0.11, - any.http-types ==0.12.3, - any.http2 ==2.0.6, - http2 -devel, - any.indexed-traversable ==0.1.1, - any.integer-gmp ==1.0.3.0, - any.integer-logarithms ==1.0.3.1, - integer-logarithms -check-bounds +integer-gmp, - any.interpolate ==0.2.1, - any.invariant ==0.5.3, - any.io-streams ==1.5.2.0, - io-streams +network -nointeractivetests +zlib, - any.iproute ==1.7.11, - any.itanium-abi ==0.1.1.1, - any.js-chart ==2.9.4.1, - any.json ==0.10, - json +generic -mapdict +parsec +pretty +split-base, - any.kan-extensions ==5.2.2, - any.language-c ==0.8.3, - language-c -allwarnings +iecfpextension +separatesyb +usebytestrings, - any.lens ==4.19.2, - lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.2, - libBF -system-libbf, - any.libyaml ==0.1.2, - libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.1.3, - any.lifted-base ==0.2.3.12, - llvm-pretty-bc-parser -fuzz -regressions, - any.logict ==0.7.0.3, - any.math-functions ==0.3.4.1, - math-functions +system-erf +system-expm1, - any.megaparsec ==8.0.0, - megaparsec -dev, - any.memory ==0.15.0, - memory +support_basement +support_bytestring +support_deepseq +support_foundation, - any.microlens ==0.4.12.0, - any.microlens-th ==0.4.3.6, - any.microstache ==1.0.1.2, - any.mmorph ==1.1.5, - any.modern-uri ==0.3.4.1, - modern-uri -dev, - any.monad-control ==1.0.2.3, - any.monad-par ==0.3.5, - monad-par -chaselev -newgeneric, - any.monad-par-extras ==0.3.3, - any.monadLib ==3.10, - any.mono-traversable ==1.0.15.1, - any.mtl ==2.2.2, - any.mwc-random ==0.15.0.1, - any.nats ==1.1.2, - nats +binary +hashable +template-haskell, - any.network ==3.1.2.1, - network -devel, - any.network-byte-order ==0.1.6, - any.network-info ==0.2.0.10, - any.newtype-generics ==0.6, - any.old-locale ==1.0.0.7, - any.old-time ==1.1.0.3, - any.optparse-applicative ==0.16.1.0, - optparse-applicative +process, - any.panic ==0.4.0.1, - any.parallel ==3.2.2.0, - parameterized-utils +unsafe-operations, - any.parsec ==3.1.14.0, - any.parser-combinators ==1.3.0, - parser-combinators -dev, - any.pem ==0.2.4, - any.pretty ==1.1.3.6, - any.pretty-hex ==1.1, - any.pretty-show ==1.10, - any.prettyprinter ==1.7.0, - prettyprinter -buildreadme, - any.prettyprinter-ansi-terminal ==1.1.2, - any.primitive ==0.7.1.0, - any.process ==1.6.9.0, - any.profunctors ==5.6, - any.psqueues ==0.2.7.2, - any.quickcheck-instances ==0.3.25.2, - quickcheck-instances -bytestring-builder, - any.quickcheck-io ==0.2.0, - any.random ==1.2.0, - any.raw-strings-qq ==1.1, - any.reflection ==2.1.6, - reflection -slow +template-haskell, - any.regex-base ==0.94.0.1, - any.regex-compat ==0.95.2.1, - any.resourcet ==1.2.4.2, - any.rts ==1.0, - any.safe ==0.3.19, - any.sbv ==8.15, - sbv -skiphlinttester, - any.scientific ==0.3.6.2, - scientific -bytestring-builder -integer-simple, - any.scotty ==0.12, - any.semigroupoids ==5.3.4, - semigroupoids +comonad +containers +contravariant +distributive +doctests +tagged +unordered-containers, - any.semigroups ==0.19.1, - semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, - any.setenv ==0.1.1.3, - any.silently ==1.2.5.1, - any.simple-get-opt ==0.4, - any.simple-sendfile ==0.2.30, - simple-sendfile +allow-bsd, - any.simple-smt ==0.9.7, - any.smallcheck ==1.2.1, - any.split ==0.2.3.4, - any.splitmix ==0.1.0.3, - splitmix -optimised-mixer, - any.statistics ==0.15.2.0, - any.stm ==2.5.0.0, - any.streaming-commons ==0.2.2.1, - streaming-commons -use-bytestring-builder, - any.strict ==0.4.0.1, - strict +assoc, - any.syb ==0.7.2.1, - any.tagged ==0.8.6.1, - tagged +deepseq +transformers, - any.tasty ==1.2.3, - tasty +clock, - any.tasty-ant-xml ==1.1.7, - any.tasty-hedgehog ==1.0.1.0, - any.tasty-hspec ==1.1.6, - any.tasty-hunit ==0.10.0.3, - any.tasty-quickcheck ==0.10.1.2, - any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==1.1.0.0, - any.template-haskell ==2.16.0.0, - any.temporary ==1.3, - any.terminal-size ==0.3.2.1, - any.terminfo ==0.4.1.4, - any.text ==1.2.4.1, - any.text-short ==0.1.3, - text-short -asserts, - any.tf-random ==0.5, - any.th-abstraction ==0.4.2.0, - any.th-compat ==0.1.1, - any.th-expand-syns ==0.4.6.0, - any.th-lift ==0.8.2, - any.th-lift-instances ==0.1.18, - any.th-orphans ==0.13.11, - any.th-reify-many ==0.1.9, - any.these ==1.1.1.1, - these +assoc, - any.time ==1.9.3, - any.time-compat ==1.9.5, - time-compat -old-locale, - any.time-manager ==0.0.0, - any.transformers ==0.5.6.2, - any.transformers-base ==0.4.5.2, - transformers-base +orphaninstances, - any.transformers-compat ==0.6.6, - transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, - any.type-equality ==1, - any.typed-process ==0.2.6.0, - any.unbounded-delays ==0.1.1.1, - any.uniplate ==1.6.13, - any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.13.0, - unordered-containers -debug, - any.utf8-string ==1.0.2, - any.uuid ==1.3.14, - any.uuid-types ==1.0.4, - any.vault ==0.3.1.5, - vault +useghc, - any.vector ==0.12.2.0, - vector +boundschecks -internalchecks -unsafechecks -wall, - any.vector-algorithms ==0.8.0.4, - vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-binary-instances ==0.2.5.1, - any.vector-th-unbox ==0.2.1.9, - any.versions ==4.0.3, - any.void ==0.7.3, - void -safe, - any.wai ==3.2.3, - any.wai-extra ==3.1.6, - wai-extra -build-example, - any.wai-logger ==2.3.6, - any.warp ==3.3.14, - warp +allow-sendfilefd -network-bytestring -warp-debug, - any.wcwidth ==0.0.2, - wcwidth -cli +split-base, - what4 -drealtestdisable -solvertests -stptestdisable, - any.wl-pprint-annotated ==0.1.0.1, - any.word8 ==0.1.3, - any.x509 ==1.7.5, - any.xml ==1.3.14, - any.yaml ==0.11.5.0, - yaml +no-examples +no-exe, - any.zenc ==0.1.1, - any.zlib ==0.6.2.3, - zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, - any.zlib-bindings ==0.1.1.5 diff --git a/cabal.GHC-8.10.4.config b/cabal.GHC-8.10.7.config similarity index 58% rename from cabal.GHC-8.10.4.config rename to cabal.GHC-8.10.7.config index bcde304b2e..90a56fbd41 100644 --- a/cabal.GHC-8.10.4.config +++ b/cabal.GHC-8.10.7.config @@ -1,7 +1,6 @@ active-repositories: hackage.haskell.org:merge constraints: any.Cabal ==3.2.1.0, - any.FloatingHex ==0.5, - any.Glob ==0.10.1, + any.Glob ==0.10.2, any.GraphSCC ==1.0.4, GraphSCC -use-maps, any.HUnit ==1.6.2.0, @@ -9,126 +8,129 @@ constraints: any.Cabal ==3.2.1.0, any.IntervalMap ==0.6.1.2, any.MemoTrie ==0.6.10, MemoTrie -examples, - any.MonadRandom ==0.5.2, + any.MonadRandom ==0.5.3, + any.OneTuple ==0.3.1, any.Only ==0.1, any.QuickCheck ==2.14.2, QuickCheck -old-random +templatehaskell, - any.StateVar ==1.2.1, - abcBridge -enable-extra-tests +enable-pthreads, + any.StateVar ==1.2.2, any.abstract-deque ==0.3, abstract-deque -usecas, any.abstract-par ==0.3.3, any.adjunctions ==4.4, any.aeson ==1.5.6.0, aeson -bytestring-builder -cffi -developer -fast, - any.alex ==3.2.6, - alex +small_base, - any.ansi-terminal ==0.11, + any.aeson-typescript ==0.3.0.1, + any.alex ==3.2.7.1, + any.ansi-terminal ==0.11.1, ansi-terminal -example, any.ansi-wl-pprint ==0.6.9, ansi-wl-pprint -example, any.appar ==0.1.8, + any.arithmoi ==0.12.0.1, any.array ==0.5.4.0, any.asn1-encoding ==0.9.6, any.asn1-parse ==0.9.5, any.asn1-types ==0.3.4, any.assoc ==1.0.2, - any.async ==2.2.3, + any.async ==2.2.4, async -bench, - any.attoparsec ==0.13.2.5, + any.attoparsec ==0.14.4, attoparsec -developer, any.auto-update ==0.1.6, - any.base ==4.14.1.0, + any.base ==4.14.3.0, any.base-compat ==0.11.2, any.base-compat-batteries ==0.11.2, - any.base-orphans ==0.8.4, - any.base16-bytestring ==1.0.1.0, - any.base64-bytestring ==1.2.0.1, - any.basement ==0.0.11, - any.bifunctors ==5.5.7, + any.base-orphans ==0.8.6, + any.base16-bytestring ==1.0.2.0, + any.base64-bytestring ==1.2.1.0, + any.basement ==0.0.12, + any.bifunctors ==5.5.11, bifunctors +semigroups +tagged, any.bimap ==0.4.0, any.binary ==0.8.8.0, - any.binary-orphans ==1.0.1, + any.binary-orphans ==1.0.2, + any.binary-parsers ==0.2.4.0, any.bitwise ==1.0.0.1, - any.blaze-builder ==0.4.2.1, + any.blaze-builder ==0.4.2.2, any.blaze-html ==0.9.1.2, any.blaze-markup ==0.8.2.8, - any.boomerang ==1.4.6, + any.boomerang ==1.4.7, any.bsb-http-chunked ==0.0.0.4, - any.bv-sized ==1.0.2, + any.bv-sized ==1.0.3, any.byteorder ==1.0.4, any.bytestring ==0.10.12.0, - any.bytestring-builder ==0.10.8.2.0, - bytestring-builder +bytestring_has_builder, - any.c2hs ==0.28.7, - c2hs +base3 -regression, - any.cabal-doctest ==1.0.8, - any.call-stack ==0.3.0, + any.bytestring-lexing ==0.5.0.8, + any.cabal-doctest ==1.0.9, + any.call-stack ==0.4.0, any.case-insensitive ==1.2.1.0, any.cassava ==0.5.2.0, cassava -bytestring--lt-0_10_4, - any.cereal ==0.5.8.1, + any.cereal ==0.5.8.2, cereal -bytestring-builder, + any.chimera ==0.3.2.0, + chimera +representable, any.clock ==0.8.2, clock -llvm, any.code-page ==0.2.1, - any.colour ==2.3.5, + any.colour ==2.3.6, any.comonad ==5.0.8, comonad +containers +distributive +indexed-traversable, - any.concurrent-output ==1.10.12, - any.conduit ==1.3.4.1, + any.concurrent-extra ==0.7.0.12, + any.concurrent-output ==1.10.14, + any.conduit ==1.3.4.2, any.conduit-extra ==1.3.5, any.config-schema ==1.2.2.0, - any.config-value ==0.8.1, - any.constraints ==0.12, - any.containers ==0.6.2.1, - any.contravariant ==1.5.3, + any.config-value ==0.8.2, + any.constraints ==0.13.2, + any.containers ==0.6.5.1, + any.contravariant ==1.5.5, contravariant +semigroups +statevar +tagged, any.cookie ==0.4.5, - any.crackNum ==2.4, - any.criterion ==1.5.9.0, + any.criterion ==1.5.12.0, criterion -embed-data-files -fast, - any.criterion-measurement ==0.1.2.0, + any.criterion-measurement ==0.1.3.0, criterion-measurement -fast, crucible +unsafe-operations, - any.cryptohash-md5 ==0.11.100.1, - any.cryptohash-sha1 ==0.11.100.1, + any.cryptohash-md5 ==0.11.101.0, + any.cryptohash-sha1 ==0.11.101.0, cryptol +relocatable -static, - cryptol-saw-core +build-css, - any.cryptonite ==0.28, + cryptol-remote-api -notthreaded -static, + any.cryptonite ==0.29, cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, any.cryptonite-conduit ==0.2.2, any.data-accessor ==0.2.3, data-accessor +category +monadfail +splitbase, any.data-binary-ieee754 ==0.4.4, any.data-default-class ==0.1.2.0, - any.data-fix ==0.3.1, + any.data-fix ==0.3.2, any.data-inttrie ==0.1.4, any.data-ref ==0.0.2, any.deepseq ==1.4.4.0, any.dense-linear-algebra ==0.1.0.0, - any.deriving-compat ==0.5.9, + any.deriving-compat ==0.6, deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, any.directory ==1.3.6.0, any.distributive ==0.6.2.1, distributive +semigroups +tagged, any.dlist ==1.0, dlist -werror, - any.doctest ==0.16.3, + any.doctest ==0.20.0, any.dotgen ==0.4.3, dotgen -devel, any.easy-file ==0.2.2, any.either ==5.0.1.1, - any.entropy ==0.4.1.6, + any.entropy ==0.4.1.7, entropy -halvm, any.erf ==2.0.0.0, + any.errors ==2.3.0, + any.exact-pi ==0.5.0.1, any.exceptions ==0.10.4, any.executable-path ==0.0.3.1, any.extensible-exceptions ==0.1.1.4, - any.extra ==1.7.9, + any.extra ==1.7.10, any.fail ==4.9.0.0, - any.fast-logger ==3.0.3, + any.fast-logger ==3.1.1, any.fgl ==5.7.0.3, fgl +containers042, any.fgl-visualize ==0.1.0.1, @@ -136,100 +138,118 @@ constraints: any.Cabal ==3.2.1.0, any.filemanip ==0.3.6.3, any.filepath ==1.4.2.1, any.fingertree ==0.1.4.2, - any.free ==5.1.3, - any.generic-deriving ==1.13.1, + any.free ==5.1.7, + any.generic-deriving ==1.14.1, generic-deriving +base-4-9, - any.generic-random ==1.3.0.1, - any.ghc ==8.10.4, - any.ghc-boot ==8.10.4, - any.ghc-boot-th ==8.10.4, - any.ghc-heap ==8.10.4, + any.generic-lens ==2.2.1.0, + any.generic-lens-core ==2.2.1.0, + any.generic-random ==1.5.0.1, + generic-random -enable-inspect, + any.ghc ==8.10.7, + any.ghc-boot ==8.10.7, + any.ghc-boot-th ==8.10.7, + any.ghc-heap ==8.10.7, any.ghc-paths ==0.1.0.12, any.ghc-prim ==0.6.1, - any.ghci ==8.10.4, + any.ghci ==8.10.7, + any.githash ==0.1.6.2, any.gitrev ==1.3.1, + any.graphviz ==2999.20.1.0, + graphviz -test-parsing, any.happy ==1.20.0, - any.hashable ==1.3.4.1, + any.hashable ==1.3.5.0, hashable +integer-gmp -random-initial-seed, - any.hashtables ==1.2.4.1, + any.hashtables ==1.2.4.2, hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, - any.haskeline ==0.8.0.1, + any.haskeline ==0.8.2, any.haskell-lexer ==1.1, any.haskell-src-exts ==1.23.1, - any.haskell-src-meta ==0.8.7, - any.hedgehog ==1.0.4, + any.haskell-src-meta ==0.8.8, + any.hedgehog ==1.0.5, + any.hedgehog-classes ==0.2.5.3, + hedgehog-classes +aeson +comonad +primitive +semirings +vector, any.heredoc ==0.2.0.0, any.hobbits ==1.4, any.hostname ==1.0, any.hourglass ==0.2.12, any.hpc ==0.6.1.0, - any.hsc2hs ==0.68.7, + any.hsc2hs ==0.68.8, hsc2hs -in-ghc-tree, - any.hspec ==2.7.8, - any.hspec-core ==2.7.8, - any.hspec-discover ==2.7.8, + any.hspec ==2.9.4, + any.hspec-core ==2.9.4, + any.hspec-discover ==2.9.4, any.hspec-expectations ==0.8.2, any.http-date ==0.0.11, any.http-types ==0.12.3, - any.http2 ==2.0.6, - http2 -devel, - any.indexed-traversable ==0.1.1, + any.http2 ==3.0.2, + http2 -devel -doc -h2spec, + any.indexed-profunctors ==0.1.1, + any.indexed-traversable ==0.1.2, + any.indexed-traversable-instances ==0.1.1, any.integer-gmp ==1.0.3.0, any.integer-logarithms ==1.0.3.1, integer-logarithms -check-bounds +integer-gmp, + any.integer-roots ==1.0.2.0, any.interpolate ==0.2.1, - any.invariant ==0.5.3, - any.io-streams ==1.5.2.0, + any.invariant ==0.5.5, + any.io-streams ==1.5.2.1, io-streams +network -nointeractivetests +zlib, - any.iproute ==1.7.11, + any.iproute ==1.7.12, any.itanium-abi ==0.1.1.1, any.js-chart ==2.9.4.1, any.json ==0.10, json +generic -mapdict +parsec +pretty +split-base, - any.kan-extensions ==5.2.2, - any.language-c ==0.8.3, - language-c -allwarnings +iecfpextension +separatesyb +usebytestrings, + any.kan-extensions ==5.2.3, + any.kvitable ==1.0.0.0, language-rust +enablequasiquotes +usebytestrings, - any.lens ==4.19.2, - lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.2, + any.lens ==5.0.1, + lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, + any.libBF ==0.6.3, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, - any.lifted-async ==0.10.1.3, + any.lifted-async ==0.10.2.2, any.lifted-base ==0.2.3.12, llvm-pretty-bc-parser -fuzz -regressions, any.logict ==0.7.0.3, - any.math-functions ==0.3.4.1, + any.lucid ==2.9.12.1, + any.lumberjack ==1.0.0.1, + any.math-functions ==0.3.4.2, math-functions +system-erf +system-expm1, + any.megaparsec ==9.0.1, megaparsec -dev, - any.memory ==0.15.0, + any.memory ==0.16.0, memory +support_basement +support_bytestring +support_deepseq +support_foundation, any.microlens ==0.4.12.0, - any.microlens-th ==0.4.3.6, - any.microstache ==1.0.1.2, + any.microlens-th ==0.4.3.10, + any.microstache ==1.0.2, any.mmorph ==1.1.5, - any.modern-uri ==0.3.4.1, + any.mod ==0.1.2.2, + mod +semirings +vector, + any.modern-uri ==0.3.4.2, modern-uri -dev, - any.monad-control ==1.0.2.3, + any.monad-control ==1.0.3.1, any.monad-par ==0.3.5, monad-par -chaselev -newgeneric, any.monad-par-extras ==0.3.3, any.monadLib ==3.10, - any.mono-traversable ==1.0.15.1, + any.mono-traversable ==1.0.15.3, any.mtl ==2.2.2, - any.mwc-random ==0.15.0.1, + any.mwc-random ==0.15.0.2, any.nats ==1.1.2, nats +binary +hashable +template-haskell, - any.network ==3.1.2.1, + any.network ==3.1.2.7, network -devel, any.network-byte-order ==0.1.6, any.network-info ==0.2.0.10, - any.newtype-generics ==0.6, + any.newtype-generics ==0.6.1, + any.numtype-dk ==0.5.0.3, any.old-locale ==1.0.0.7, any.old-time ==1.1.0.3, any.optparse-applicative ==0.16.1.0, optparse-applicative +process, + any.optparse-simple ==0.1.1.4, + optparse-simple -build-example, any.panic ==0.4.0.1, any.parallel ==3.2.2.0, parameterized-utils +unsafe-operations, @@ -237,69 +257,77 @@ constraints: any.Cabal ==3.2.1.0, any.parser-combinators ==1.3.0, parser-combinators -dev, any.pem ==0.2.4, + any.polyparse ==1.13, any.pretty ==1.1.3.6, any.pretty-hex ==1.1, any.pretty-show ==1.10, - any.prettyprinter ==1.7.0, - prettyprinter -buildreadme, - any.prettyprinter-ansi-terminal ==1.1.2, - any.primitive ==0.7.1.0, - any.process ==1.6.9.0, - any.profunctors ==5.6, - any.psqueues ==0.2.7.2, - any.quickcheck-instances ==0.3.25.2, + any.prettyprinter ==1.7.1, + prettyprinter -buildreadme +text, + any.prettyprinter-ansi-terminal ==1.1.3, + any.primitive ==0.7.3.0, + any.process ==1.6.13.2, + any.profunctors ==5.6.2, + any.psqueues ==0.2.7.3, + any.quickcheck-instances ==0.3.27, quickcheck-instances -bytestring-builder, any.quickcheck-io ==0.2.0, - any.random ==1.2.0, + any.random ==1.2.1, any.raw-strings-qq ==1.1, any.reflection ==2.1.6, reflection -slow +template-haskell, - any.regex-base ==0.94.0.1, + any.regex-base ==0.94.0.2, any.regex-compat ==0.95.2.1, - any.regex-posix ==0.96.0.0, + any.regex-posix ==0.96.0.1, regex-posix -_regex-posix-clib, - any.resourcet ==1.2.4.2, - any.rts ==1.0, + any.resourcet ==1.2.4.3, + any.rts ==1.0.1, + any.s-cargot ==0.1.4.0, + s-cargot -build-example, any.safe ==0.3.19, - saw-remote-api +builtin-abc, - saw-script +builtin-abc, any.sbv ==8.15, - sbv -skiphlinttester, - any.scientific ==0.3.6.2, + any.scientific ==0.3.7.0, scientific -bytestring-builder -integer-simple, any.scotty ==0.12, - any.semigroupoids ==5.3.4, - semigroupoids +comonad +containers +contravariant +distributive +doctests +tagged +unordered-containers, - any.semigroups ==0.19.1, + any.semigroupoids ==5.3.7, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, + any.semigroups ==0.19.2, semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, + any.semirings ==0.6, + semirings +containers +unordered-containers, any.setenv ==0.1.1.3, - any.silently ==1.2.5.1, + any.silently ==1.2.5.2, any.simple-get-opt ==0.4, any.simple-sendfile ==0.2.30, simple-sendfile +allow-bsd, any.simple-smt ==0.9.7, any.smallcheck ==1.2.1, any.split ==0.2.3.4, - any.splitmix ==0.1.0.3, + any.splitmix ==0.1.0.4, splitmix -optimised-mixer, - any.statistics ==0.15.2.0, - any.stm ==2.5.0.0, - any.streaming-commons ==0.2.2.1, + any.statistics ==0.16.0.1, + any.stm ==2.5.0.1, + any.streaming-commons ==0.2.2.3, streaming-commons -use-bytestring-builder, any.strict ==0.4.0.1, strict +assoc, + any.string-interpolate ==0.3.1.1, + string-interpolate -bytestring-builder -extended-benchmarks -text-builder, any.syb ==0.7.2.1, any.tagged ==0.8.6.1, tagged +deepseq +transformers, - any.tasty ==1.4.1, + any.tasty ==1.4.2.1, tasty +clock +unix, any.tasty-ant-xml ==1.1.8, - any.tasty-hedgehog ==1.0.1.0, - any.tasty-hspec ==1.1.6, + any.tasty-checklist ==1.0.3.0, + any.tasty-expected-failure ==0.12.3, + any.tasty-golden ==2.3.5, + tasty-golden -build-example, + any.tasty-hedgehog ==1.1.0.0, + any.tasty-hspec ==1.2, any.tasty-hunit ==0.10.0.3, - any.tasty-quickcheck ==0.10.1.2, + any.tasty-quickcheck ==0.10.2, any.tasty-smallcheck ==0.8.2, - any.tasty-sugar ==1.1.0.0, + any.tasty-sugar ==1.1.1.0, any.template-haskell ==2.16.0.0, any.temporary ==1.3, any.terminal-size ==0.3.2.1, @@ -308,70 +336,79 @@ constraints: any.Cabal ==3.2.1.0, any.test-framework-hunit ==0.3.0.2, test-framework-hunit -base3 +base4, any.text ==1.2.4.1, - any.text-short ==0.1.3, + any.text-conversions ==0.3.1, + any.text-short ==0.1.5, text-short -asserts, any.tf-random ==0.5, - any.th-abstraction ==0.3.2.0, - any.th-compat ==0.1.1, - any.th-expand-syns ==0.4.6.0, + any.th-abstraction ==0.4.3.0, + any.th-compat ==0.1.3, + any.th-expand-syns ==0.4.9.0, any.th-lift ==0.8.2, - any.th-lift-instances ==0.1.18, - any.th-orphans ==0.13.11, - any.th-reify-many ==0.1.9, + any.th-lift-instances ==0.1.19, + any.th-orphans ==0.13.12, + any.th-reify-many ==0.1.10, any.these ==1.1.1.1, these +assoc, any.time ==1.9.3, - any.time-compat ==1.9.5, + any.time-compat ==1.9.6.1, time-compat -old-locale, any.time-manager ==0.0.0, + any.tls ==1.5.7, + tls +compat -hans +network, + any.tls-session-manager ==0.0.4, any.transformers ==0.5.6.2, - any.transformers-base ==0.4.5.2, + any.transformers-base ==0.4.6, transformers-base +orphaninstances, any.transformers-compat ==0.6.6, transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, any.type-equality ==1, - any.typed-process ==0.2.6.0, + any.typed-process ==0.2.8.0, any.unbounded-delays ==0.1.1.1, any.uniplate ==1.6.13, any.unix ==2.7.2.2, - any.unix-compat ==0.5.3, + any.unix-compat ==0.5.4, unix-compat -old-time, any.unix-time ==0.4.7, + any.unliftio ==0.2.20, any.unliftio-core ==0.2.0.1, - any.unordered-containers ==0.2.13.0, + any.unordered-containers ==0.2.16.0, unordered-containers -debug, any.utf8-string ==1.0.2, - any.uuid ==1.3.14, - any.uuid-types ==1.0.4, + any.uuid ==1.3.15, + any.uuid-types ==1.0.5, any.vault ==0.3.1.5, vault +useghc, - any.vector ==0.12.2.0, + any.vector ==0.12.3.1, vector +boundschecks -internalchecks -unsafechecks -wall, any.vector-algorithms ==0.8.0.4, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, - any.vector-binary-instances ==0.2.5.1, - any.vector-th-unbox ==0.2.1.9, - any.versions ==4.0.3, + any.vector-binary-instances ==0.2.5.2, + any.vector-th-unbox ==0.2.2, + any.versions ==5.0.2, any.void ==0.7.3, void -safe, any.wai ==3.2.3, - any.wai-extra ==3.1.6, + any.wai-extra ==3.1.8, wai-extra -build-example, - any.wai-logger ==2.3.6, - any.warp ==3.3.14, + any.wai-logger ==2.3.7, + any.warp ==3.3.18, warp +allow-sendfilefd -network-bytestring -warp-debug, + any.warp-tls ==3.3.2, any.wcwidth ==0.0.2, wcwidth -cli +split-base, any.weigh ==0.0.16, what4 -drealtestdisable -solvertests -stptestdisable, any.wl-pprint-annotated ==0.1.0.1, + any.wl-pprint-text ==1.2.0.2, any.word8 ==0.1.3, - any.x509 ==1.7.5, + any.x509 ==1.7.6, + any.x509-store ==1.6.9, + any.x509-validation ==1.6.12, any.xml ==1.3.14, - any.yaml ==0.11.5.0, + any.yaml ==0.11.7.0, yaml +no-examples +no-exe, - any.zenc ==0.1.1, + any.zenc ==0.1.2, any.zlib ==0.6.2.3, zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, any.zlib-bindings ==0.1.1.5 -index-state: hackage.haskell.org 2021-03-11T19:34:00Z +index-state: hackage.haskell.org 2022-01-24T13:23:29Z From e6fad77cc20e973fdda845dd1a20f77fdcf38e71 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 26 Jan 2022 11:51:07 -0500 Subject: [PATCH 4/4] CI: Test GHC 9.0.2 --- .github/workflows/ci.yml | 7 +- cabal.GHC-9.0.2.config | 415 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 421 insertions(+), 1 deletion(-) create mode 100644 cabal.GHC-9.0.2.config diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b3f3047f82..5f08806864 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -68,10 +68,15 @@ jobs: fail-fast: false matrix: os: [ubuntu-18.04, macos-10.15, windows-latest] - ghc: ["8.8.4", "8.10.7"] + ghc: ["8.8.4", "8.10.7", "9.0.2"] exclude: - os: windows-latest ghc: "8.8.4" + # Exclude 9.0 on Windows for now until + # https://github.com/commercialhaskell/stackage/issues/6400 + # is resolved + - os: windows-latest + ghc: "9.0.2" outputs: cabal-test-suites-json: ${{ steps.cabal-test-suites.outputs.targets-json }} steps: diff --git a/cabal.GHC-9.0.2.config b/cabal.GHC-9.0.2.config new file mode 100644 index 0000000000..721ac648de --- /dev/null +++ b/cabal.GHC-9.0.2.config @@ -0,0 +1,415 @@ +active-repositories: hackage.haskell.org:merge +constraints: any.Cabal ==3.4.1.0, + any.Glob ==0.10.2, + any.GraphSCC ==1.0.4, + GraphSCC -use-maps, + any.HUnit ==1.6.2.0, + any.IfElse ==0.85, + any.IntervalMap ==0.6.1.2, + any.MemoTrie ==0.6.10, + MemoTrie -examples, + any.MonadRandom ==0.5.3, + any.OneTuple ==0.3.1, + any.Only ==0.1, + any.QuickCheck ==2.14.2, + QuickCheck -old-random +templatehaskell, + any.StateVar ==1.2.2, + any.abstract-deque ==0.3, + abstract-deque -usecas, + any.abstract-par ==0.3.3, + any.adjunctions ==4.4, + any.aeson ==1.5.6.0, + aeson -bytestring-builder -cffi -developer -fast, + any.aeson-typescript ==0.3.0.1, + any.alex ==3.2.7.1, + any.ansi-terminal ==0.11.1, + ansi-terminal -example, + any.ansi-wl-pprint ==0.6.9, + ansi-wl-pprint -example, + any.appar ==0.1.8, + any.arithmoi ==0.12.0.1, + any.array ==0.5.4.0, + any.asn1-encoding ==0.9.6, + any.asn1-parse ==0.9.5, + any.asn1-types ==0.3.4, + any.assoc ==1.0.2, + any.async ==2.2.4, + async -bench, + any.attoparsec ==0.14.4, + attoparsec -developer, + any.auto-update ==0.1.6, + any.base ==4.15.1.0, + any.base-compat ==0.11.2, + any.base-compat-batteries ==0.11.2, + any.base-orphans ==0.8.6, + any.base16-bytestring ==1.0.2.0, + any.base64-bytestring ==1.2.1.0, + any.basement ==0.0.12, + any.bifunctors ==5.5.11, + bifunctors +semigroups +tagged, + any.bimap ==0.4.0, + any.binary ==0.8.8.0, + any.binary-orphans ==1.0.2, + any.binary-parsers ==0.2.4.0, + any.bitwise ==1.0.0.1, + any.blaze-builder ==0.4.2.2, + any.blaze-html ==0.9.1.2, + any.blaze-markup ==0.8.2.8, + any.boomerang ==1.4.7, + any.bsb-http-chunked ==0.0.0.4, + any.bv-sized ==1.0.3, + any.byteorder ==1.0.4, + any.bytestring ==0.10.12.1, + any.bytestring-lexing ==0.5.0.8, + any.cabal-doctest ==1.0.9, + any.call-stack ==0.4.0, + any.case-insensitive ==1.2.1.0, + any.cassava ==0.5.2.0, + cassava -bytestring--lt-0_10_4, + any.cereal ==0.5.8.2, + cereal -bytestring-builder, + any.chimera ==0.3.2.0, + chimera +representable, + any.clock ==0.8.2, + clock -llvm, + any.code-page ==0.2.1, + any.colour ==2.3.6, + any.comonad ==5.0.8, + comonad +containers +distributive +indexed-traversable, + any.concurrent-extra ==0.7.0.12, + any.concurrent-output ==1.10.14, + any.conduit ==1.3.4.2, + any.conduit-extra ==1.3.5, + any.config-schema ==1.2.2.0, + any.config-value ==0.8.2, + any.constraints ==0.13.2, + any.containers ==0.6.4.1, + any.contravariant ==1.5.5, + contravariant +semigroups +statevar +tagged, + any.cookie ==0.4.5, + any.criterion ==1.5.12.0, + criterion -embed-data-files -fast, + any.criterion-measurement ==0.1.3.0, + criterion-measurement -fast, + crucible +unsafe-operations, + any.cryptohash-md5 ==0.11.101.0, + any.cryptohash-sha1 ==0.11.101.0, + cryptol +relocatable -static, + cryptol-remote-api -notthreaded -static, + any.cryptonite ==0.29, + cryptonite -check_alignment +integer-gmp -old_toolchain_inliner +support_aesni +support_deepseq -support_pclmuldq +support_rdrand -support_sse +use_target_attributes, + any.cryptonite-conduit ==0.2.2, + any.data-accessor ==0.2.3, + data-accessor +category +monadfail +splitbase, + any.data-binary-ieee754 ==0.4.4, + any.data-default-class ==0.1.2.0, + any.data-fix ==0.3.2, + any.data-inttrie ==0.1.4, + any.data-ref ==0.0.2, + any.deepseq ==1.4.5.0, + any.dense-linear-algebra ==0.1.0.0, + any.deriving-compat ==0.6, + deriving-compat +base-4-9 +new-functor-classes +template-haskell-2-11, + any.directory ==1.3.6.2, + any.distributive ==0.6.2.1, + distributive +semigroups +tagged, + any.dlist ==1.0, + dlist -werror, + any.doctest ==0.20.0, + any.dotgen ==0.4.3, + dotgen -devel, + any.easy-file ==0.2.2, + any.either ==5.0.1.1, + any.entropy ==0.4.1.7, + entropy -halvm, + any.erf ==2.0.0.0, + any.errors ==2.3.0, + any.exact-pi ==0.5.0.1, + any.exceptions ==0.10.4, + any.executable-path ==0.0.3.1, + any.extensible-exceptions ==0.1.1.4, + any.extra ==1.7.10, + any.fail ==4.9.0.0, + any.fast-logger ==3.1.1, + any.fgl ==5.7.0.3, + fgl +containers042, + any.fgl-visualize ==0.1.0.1, + any.filelock ==0.1.1.5, + any.filemanip ==0.3.6.3, + any.filepath ==1.4.2.1, + any.fingertree ==0.1.4.2, + any.free ==5.1.7, + any.generic-deriving ==1.14.1, + generic-deriving +base-4-9, + any.generic-lens ==2.2.1.0, + any.generic-lens-core ==2.2.1.0, + any.generic-random ==1.5.0.1, + generic-random -enable-inspect, + any.ghc ==9.0.2, + any.ghc-bignum ==1.1, + any.ghc-boot ==9.0.2, + any.ghc-boot-th ==9.0.2, + any.ghc-heap ==9.0.2, + any.ghc-paths ==0.1.0.12, + any.ghc-prim ==0.7.0, + any.ghci ==9.0.2, + any.githash ==0.1.6.2, + any.gitrev ==1.3.1, + any.graphviz ==2999.20.1.0, + graphviz -test-parsing, + any.happy ==1.20.0, + any.hashable ==1.3.5.0, + hashable +integer-gmp -random-initial-seed, + any.hashtables ==1.2.4.2, + hashtables -bounds-checking -debug -detailed-profiling -portable -sse42 +unsafe-tricks, + any.haskeline ==0.8.2, + any.haskell-lexer ==1.1, + any.haskell-src-exts ==1.23.1, + any.haskell-src-meta ==0.8.8, + any.hedgehog ==1.0.5, + any.hedgehog-classes ==0.2.5.3, + hedgehog-classes +aeson +comonad +primitive +semirings +vector, + any.heredoc ==0.2.0.0, + any.hobbits ==1.4, + any.hostname ==1.0, + any.hourglass ==0.2.12, + any.hpc ==0.6.1.0, + any.hsc2hs ==0.68.8, + hsc2hs -in-ghc-tree, + any.hspec ==2.9.4, + any.hspec-core ==2.9.4, + any.hspec-discover ==2.9.4, + any.hspec-expectations ==0.8.2, + any.http-date ==0.0.11, + any.http-types ==0.12.3, + any.http2 ==3.0.2, + http2 -devel -doc -h2spec, + any.indexed-profunctors ==0.1.1, + any.indexed-traversable ==0.1.2, + any.indexed-traversable-instances ==0.1.1, + any.integer-gmp ==1.1, + any.integer-logarithms ==1.0.3.1, + integer-logarithms -check-bounds +integer-gmp, + any.integer-roots ==1.0.2.0, + any.interpolate ==0.2.1, + any.invariant ==0.5.5, + any.io-streams ==1.5.2.1, + io-streams +network -nointeractivetests +zlib, + any.iproute ==1.7.12, + any.itanium-abi ==0.1.1.1, + any.js-chart ==2.9.4.1, + any.json ==0.10, + json +generic -mapdict +parsec +pretty +split-base, + any.kan-extensions ==5.2.3, + any.kvitable ==1.0.0.0, + language-rust +enablequasiquotes +usebytestrings, + any.lens ==5.0.1, + lens -benchmark-uniplate -dump-splices +inlining -j +test-hunit +test-properties +test-templates +trustworthy, + any.libBF ==0.6.3, + libBF -system-libbf, + any.libyaml ==0.1.2, + libyaml -no-unicode -system-libyaml, + any.lifted-async ==0.10.2.2, + any.lifted-base ==0.2.3.12, + llvm-pretty-bc-parser -fuzz -regressions, + any.logict ==0.7.0.3, + any.lucid ==2.9.12.1, + any.lumberjack ==1.0.0.1, + any.math-functions ==0.3.4.2, + math-functions +system-erf +system-expm1, + any.megaparsec ==9.0.1, + megaparsec -dev, + any.memory ==0.16.0, + memory +support_basement +support_bytestring +support_deepseq +support_foundation, + any.microlens ==0.4.12.0, + any.microlens-th ==0.4.3.10, + any.microstache ==1.0.2, + any.mmorph ==1.1.5, + any.mod ==0.1.2.2, + mod +semirings +vector, + any.modern-uri ==0.3.4.2, + modern-uri -dev, + any.monad-control ==1.0.3.1, + any.monad-par ==0.3.5, + monad-par -chaselev -newgeneric, + any.monad-par-extras ==0.3.3, + any.monadLib ==3.10, + any.mono-traversable ==1.0.15.3, + any.mtl ==2.2.2, + any.mwc-random ==0.15.0.2, + any.nats ==1.1.2, + nats +binary +hashable +template-haskell, + any.network ==3.1.2.7, + network -devel, + any.network-byte-order ==0.1.6, + any.network-info ==0.2.0.10, + any.newtype-generics ==0.6.1, + any.numtype-dk ==0.5.0.3, + any.old-locale ==1.0.0.7, + any.old-time ==1.1.0.3, + any.optparse-applicative ==0.16.1.0, + optparse-applicative +process, + any.optparse-simple ==0.1.1.4, + optparse-simple -build-example, + any.panic ==0.4.0.1, + any.parallel ==3.2.2.0, + parameterized-utils +unsafe-operations, + any.parsec ==3.1.14.0, + any.parser-combinators ==1.3.0, + parser-combinators -dev, + any.pem ==0.2.4, + any.polyparse ==1.13, + any.pretty ==1.1.3.6, + any.pretty-hex ==1.1, + any.pretty-show ==1.10, + any.prettyprinter ==1.7.1, + prettyprinter -buildreadme +text, + any.prettyprinter-ansi-terminal ==1.1.3, + any.primitive ==0.7.3.0, + any.process ==1.6.13.2, + any.profunctors ==5.6.2, + any.psqueues ==0.2.7.3, + any.quickcheck-instances ==0.3.27, + quickcheck-instances -bytestring-builder, + any.quickcheck-io ==0.2.0, + any.random ==1.2.1, + any.raw-strings-qq ==1.1, + any.reflection ==2.1.6, + reflection -slow +template-haskell, + any.regex-base ==0.94.0.2, + any.regex-compat ==0.95.2.1, + any.regex-posix ==0.96.0.1, + regex-posix -_regex-posix-clib, + any.resourcet ==1.2.4.3, + any.rts ==1.0.2, + any.s-cargot ==0.1.4.0, + s-cargot -build-example, + any.safe ==0.3.19, + any.sbv ==8.15, + any.scientific ==0.3.7.0, + scientific -bytestring-builder -integer-simple, + any.scotty ==0.12, + any.semigroupoids ==5.3.7, + semigroupoids +comonad +containers +contravariant +distributive +tagged +unordered-containers, + any.semigroups ==0.19.2, + semigroups +binary +bytestring -bytestring-builder +containers +deepseq +hashable +tagged +template-haskell +text +transformers +unordered-containers, + any.semirings ==0.6, + semirings +containers +unordered-containers, + any.setenv ==0.1.1.3, + any.silently ==1.2.5.2, + any.simple-get-opt ==0.4, + any.simple-sendfile ==0.2.30, + simple-sendfile +allow-bsd, + any.simple-smt ==0.9.7, + any.smallcheck ==1.2.1, + any.split ==0.2.3.4, + any.splitmix ==0.1.0.4, + splitmix -optimised-mixer, + any.statistics ==0.16.0.1, + any.stm ==2.5.0.0, + any.streaming-commons ==0.2.2.3, + streaming-commons -use-bytestring-builder, + any.strict ==0.4.0.1, + strict +assoc, + any.string-interpolate ==0.3.1.1, + string-interpolate -bytestring-builder -extended-benchmarks -text-builder, + any.syb ==0.7.2.1, + any.tagged ==0.8.6.1, + tagged +deepseq +transformers, + any.tasty ==1.4.2.1, + tasty +clock +unix, + any.tasty-ant-xml ==1.1.8, + any.tasty-checklist ==1.0.3.0, + any.tasty-expected-failure ==0.12.3, + any.tasty-golden ==2.3.5, + tasty-golden -build-example, + any.tasty-hedgehog ==1.1.0.0, + any.tasty-hspec ==1.2, + any.tasty-hunit ==0.10.0.3, + any.tasty-quickcheck ==0.10.2, + any.tasty-smallcheck ==0.8.2, + any.tasty-sugar ==1.1.1.0, + any.template-haskell ==2.17.0.0, + any.temporary ==1.3, + any.terminal-size ==0.3.2.1, + any.terminfo ==0.4.1.5, + any.test-framework ==0.8.2.0, + any.test-framework-hunit ==0.3.0.2, + test-framework-hunit -base3 +base4, + any.text ==1.2.5.0, + any.text-conversions ==0.3.1, + any.text-short ==0.1.5, + text-short -asserts, + any.tf-random ==0.5, + any.th-abstraction ==0.4.3.0, + any.th-compat ==0.1.3, + any.th-expand-syns ==0.4.9.0, + any.th-lift ==0.8.2, + any.th-lift-instances ==0.1.19, + any.th-orphans ==0.13.12, + any.th-reify-many ==0.1.10, + any.these ==1.1.1.1, + these +assoc, + any.time ==1.9.3, + any.time-compat ==1.9.6.1, + time-compat -old-locale, + any.time-manager ==0.0.0, + any.tls ==1.5.7, + tls +compat -hans +network, + any.tls-session-manager ==0.0.4, + any.transformers ==0.5.6.2, + any.transformers-base ==0.4.6, + transformers-base +orphaninstances, + any.transformers-compat ==0.6.6, + transformers-compat -five +five-three -four +generic-deriving +mtl -three -two, + any.type-equality ==1, + any.typed-process ==0.2.8.0, + any.unbounded-delays ==0.1.1.1, + any.uniplate ==1.6.13, + any.unix ==2.7.2.2, + any.unix-compat ==0.5.4, + unix-compat -old-time, + any.unix-time ==0.4.7, + any.unliftio ==0.2.20, + any.unliftio-core ==0.2.0.1, + any.unordered-containers ==0.2.16.0, + unordered-containers -debug, + any.utf8-string ==1.0.2, + any.uuid ==1.3.15, + any.uuid-types ==1.0.5, + any.vault ==0.3.1.5, + vault +useghc, + any.vector ==0.12.3.1, + vector +boundschecks -internalchecks -unsafechecks -wall, + any.vector-algorithms ==0.8.0.4, + vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, + any.vector-binary-instances ==0.2.5.2, + any.vector-th-unbox ==0.2.2, + any.versions ==5.0.2, + any.void ==0.7.3, + void -safe, + any.wai ==3.2.3, + any.wai-extra ==3.1.8, + wai-extra -build-example, + any.wai-logger ==2.3.7, + any.warp ==3.3.18, + warp +allow-sendfilefd -network-bytestring -warp-debug, + any.warp-tls ==3.3.2, + any.wcwidth ==0.0.2, + wcwidth -cli +split-base, + any.weigh ==0.0.16, + what4 -drealtestdisable -solvertests -stptestdisable, + any.wl-pprint-annotated ==0.1.0.1, + any.wl-pprint-text ==1.2.0.2, + any.word8 ==0.1.3, + any.x509 ==1.7.6, + any.x509-store ==1.6.9, + any.x509-validation ==1.6.12, + any.xml ==1.3.14, + any.yaml ==0.11.7.0, + yaml +no-examples +no-exe, + any.zenc ==0.1.2, + any.zlib ==0.6.2.3, + zlib -bundled-c-zlib -non-blocking-ffi -pkg-config, + any.zlib-bindings ==0.1.1.5 +index-state: hackage.haskell.org 2022-01-24T13:23:29Z