From aabbbae32f8aeb775224f3ecb4d98ad222a08121 Mon Sep 17 00:00:00 2001 From: Eric Mertens Date: Mon, 10 May 2021 13:44:12 -0700 Subject: [PATCH] use new hobbits --- heapster-saw.cabal | 2 +- src/Verifier/SAW/Heapster/IRTTranslation.hs | 26 +++-- src/Verifier/SAW/Heapster/Implication.hs | 115 +++++++++++--------- src/Verifier/SAW/Heapster/Permissions.hs | 85 ++++++++++----- src/Verifier/SAW/Heapster/RustTypes.hs | 59 ++++++---- src/Verifier/SAW/Heapster/SAWTranslation.hs | 93 ++++++++-------- src/Verifier/SAW/Heapster/TypedCrucible.hs | 12 +- 7 files changed, 230 insertions(+), 162 deletions(-) diff --git a/heapster-saw.cabal b/heapster-saw.cabal index 45c078a..27e7d03 100644 --- a/heapster-saw.cabal +++ b/heapster-saw.cabal @@ -35,7 +35,7 @@ library vector, filepath, language-rust, - hobbits >= 1.3.2 + hobbits ^>= 1.4, hs-source-dirs: src build-tool-depends: alex:alex, diff --git a/src/Verifier/SAW/Heapster/IRTTranslation.hs b/src/Verifier/SAW/Heapster/IRTTranslation.hs index ae11b14..a989fba 100644 --- a/src/Verifier/SAW/Heapster/IRTTranslation.hs +++ b/src/Verifier/SAW/Heapster/IRTTranslation.hs @@ -31,6 +31,7 @@ module Verifier.SAW.Heapster.IRTTranslation ( import Numeric.Natural import Data.Foldable import Data.Functor.Const +import Data.Reflection import Control.Monad.Reader import Control.Monad.State import Control.Monad.Except @@ -106,12 +107,16 @@ inExtIRTTyVarsTransM = withReaderT $ -- | Combine a binding inside an @args :++: ext@ binding into a single -- @args :++: ext'@ binding -irtTMbCombine :: forall args ext ctx a. - Mb (args :++: ext) (Mb ctx a) -> - IRTTyVarsTransM args ext (Mb (args :++: (ext :++: ctx)) a) +irtTMbCombine :: + forall args ext c a. + Mb (args :++: ext) (Binding c a) -> + IRTTyVarsTransM args ext (Mb (args :++: (ext :> c)) a) irtTMbCombine x = do ext <- irtTExtCtx <$> ask - return $ mbCombine (fmap mbCombine (mbSeparate @_ @args ext x)) + return $ + mbCombine (ext :>: Proxy) $ + fmap (mbCombine RL.typeCtxProxies ) $ + mbSeparate @_ @args ext x -- | Create an @args :++: ext@ binding irtNus :: (RAssign Name args -> RAssign Name ext -> b) -> @@ -119,7 +124,7 @@ irtNus :: (RAssign Name args -> RAssign Name ext -> b) -> irtNus f = do args <- irtTArgsCtx <$> ask ext <- irtTExtCtx <$> ask - return $ mbCombine (nus args (nus ext . f)) + return $ mbCombine ext (nus (RL.map (\_->Proxy) args) (nus ext . f)) -- | Turn an @args :++: ext@ binding into just an @args@ binding using -- 'partialSubst' @@ -128,9 +133,10 @@ irtTSubstExt :: (Substable PartialSubst a Maybe, NuMatching a) => IRTTyVarsTransM args ext (Mb args a) irtTSubstExt x = do ext <- irtTExtCtx <$> ask - let x' = mbSwap (mbSeparate ext x) + let x' = mbSwap ext (mbSeparate ext x) emptyPS = PartialSubst $ RL.map (\_ -> PSubstElem Nothing) ext - case partialSubst emptyPS x' of + args <- RL.map (const Proxy) . irtTArgsCtx <$> ask + case give args (partialSubst emptyPS x') of Just x'' -> return x'' Nothing -> throwError $ "non-array permission in a recursive perm body" ++ " depends on an existential variable!" @@ -253,7 +259,7 @@ irtTTranslateVar p x = extCtx <- irtTExtCtx <$> ask let err _ = error "arguments to irtTTranslateVar do not match" memb = mbLift $ fmap (either id err . mbNameBoundP) - (mbSwap (mbSeparate extCtx x)) + (mbSwap extCtx (mbSeparate extCtx x)) tp_trans = getConst $ RL.get memb argsCtx -- if x (and thus also p) has no translation, return an empty list case tp_trans of @@ -450,7 +456,7 @@ valuePermIRTDesc mb_p ixs = case (mbMatch mb_p, ixs) of do let tp = mbBindingType p tp_trans <- tupleTypeTrans <$> translateClosed tp xf <- lambdaTransM "x_irt" tp_trans (\x -> inExtTransM x $ - valuePermIRTDesc (mbCombine p) ixs' >>= irtProd) + valuePermIRTDesc (mbCombine RL.typeCtxProxies p) ixs' >>= irtProd) irtCtor "Prelude.IRT_sigT" [natOpenTerm ix, xf] ([nuMP| ValPerm_Named npn args off |], _) -> namedPermIRTDesc npn args off ixs @@ -551,7 +557,7 @@ shapeExprIRTDesc mb_expr ixs = case (mbMatch mb_expr, ixs) of do let tp = mbBindingType mb_sh tp_trans <- tupleTypeTrans <$> translateClosed tp xf <- lambdaTransM "x_irt" tp_trans (\x -> inExtTransM x $ - shapeExprIRTDesc (mbCombine mb_sh) ixs' >>= irtProd) + shapeExprIRTDesc (mbCombine RL.typeCtxProxies mb_sh) ixs' >>= irtProd) irtCtor "Prelude.IRT_sigT" [natOpenTerm ix, xf] _ -> error $ "malformed IRTVarIdxs: " ++ show ixs diff --git a/src/Verifier/SAW/Heapster/Implication.hs b/src/Verifier/SAW/Heapster/Implication.hs index cabe9c2..81cc66a 100644 --- a/src/Verifier/SAW/Heapster/Implication.hs +++ b/src/Verifier/SAW/Heapster/Implication.hs @@ -33,6 +33,7 @@ import Data.Maybe import Data.List import Data.Kind as Kind import Data.Functor.Compose +import Data.Reflection import qualified Data.BitVector.Sized as BV import GHC.TypeLits import Control.Lens hiding ((:>), ix) @@ -1245,7 +1246,9 @@ data PermImpl r ps where -- contexts of bound variables for that implication tree. data MbPermImpls r bs_pss where MbPermImpls_Nil :: MbPermImpls r RNil - MbPermImpls_Cons :: !(MbPermImpls r bs_pss) -> !(Mb bs (PermImpl r ps)) -> + MbPermImpls_Cons :: CruCtx bs -> + !(MbPermImpls r bs_pss) -> + !(Mb bs (PermImpl r ps)) -> MbPermImpls r (bs_pss :> '(bs,ps)) -- | A local implication, from an input to an output permission set @@ -1297,8 +1300,8 @@ permImplStep :: NuMatchingAny1 r => PermImpl1 ps_in ps_outs -> permImplStep impl1@(Impl1_Fail _) mb_impls = PermImpl_Step impl1 mb_impls -- Catch --> call the permImplCatch function -permImplStep Impl1_Catch ((MbPermImpls_Cons - (MbPermImpls_Cons _ mb_pimpl1) mb_pimpl2)) = +permImplStep Impl1_Catch ((MbPermImpls_Cons _ + (MbPermImpls_Cons _ _ mb_pimpl1) mb_pimpl2)) = permImplCatch (elimEmptyMb mb_pimpl1) (elimEmptyMb mb_pimpl2) -- Unary rules applied to failure --> failures @@ -1326,8 +1329,8 @@ permImplStep impl1@(Impl1_TryProveBVProp _ _ _) mb_impls = permImplStepUnary impl1 mb_impls -- An or elimination fails if both branches fail -permImplStep (Impl1_ElimOr _ _ _) (MbPermImpls_Cons - (MbPermImpls_Cons MbPermImpls_Nil +permImplStep (Impl1_ElimOr _ _ _) (MbPermImpls_Cons _ + (MbPermImpls_Cons _ MbPermImpls_Nil (matchMbImplFail -> Just msg1)) (matchMbImplFail -> Just msg2)) = PermImpl_Step (Impl1_Fail @@ -1346,7 +1349,7 @@ permImplStepUnary :: NuMatchingAny1 r => MbPermImpls r (RNil :> '(bs, ps_out)) -> PermImpl r ps_in -- If the continuation implication is a failure, percolate it up -permImplStepUnary _ (MbPermImpls_Cons _ (matchMbImplFail -> Just msg)) = +permImplStepUnary _ (MbPermImpls_Cons _ _ (matchMbImplFail -> Just msg)) = PermImpl_Step (Impl1_Fail msg) MbPermImpls_Nil -- If the continuation implication is a catch with a failure on the right-hand @@ -1382,10 +1385,10 @@ matchMbImplCatchFail :: NuMatchingAny1 r => Maybe (Mb ctx (PermImpl r ps), String) matchMbImplCatchFail mb_impl = case mbMatch mb_impl of [nuMP| PermImpl_Step Impl1_Catch - (MbPermImpls_Cons (MbPermImpls_Cons _ mb_impl1) + (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |] - | Just msg <- matchMbImplFail (mbCombine mb_impl2) -> - Just (mbCombine mb_impl1, msg) + | Just msg <- matchMbImplFail (mbCombine RL.typeCtxProxies mb_impl2) -> + Just (mbCombine RL.typeCtxProxies mb_impl1, msg) _ -> Nothing -- | Produce a branching proof tree that performs the first implication and, if @@ -1403,13 +1406,13 @@ permImplCatch (PermImpl_Step (Impl1_Fail str1) _) (PermImpl_Step permImplCatch pimpl1@(PermImpl_Step (Impl1_Fail _) _) pimpl2 = permImplCatch pimpl2 pimpl1 permImplCatch (PermImpl_Step Impl1_Catch - (MbPermImpls_Cons - (MbPermImpls_Cons _ mb_pimpl_1a) mb_pimpl_1b)) pimpl2 = + (MbPermImpls_Cons _ + (MbPermImpls_Cons _ _ mb_pimpl_1a) mb_pimpl_1b)) pimpl2 = permImplCatch (elimEmptyMb mb_pimpl_1a) $ permImplCatch (elimEmptyMb mb_pimpl_1b) pimpl2 permImplCatch pimpl1 pimpl2 = PermImpl_Step Impl1_Catch $ - MbPermImpls_Cons (MbPermImpls_Cons MbPermImpls_Nil $ emptyMb pimpl1) $ + MbPermImpls_Cons knownRepr (MbPermImpls_Cons knownRepr MbPermImpls_Nil $ emptyMb pimpl1) $ emptyMb pimpl2 @@ -1422,57 +1425,57 @@ permImplSucceeds :: PermImpl r ps -> Int permImplSucceeds (PermImpl_Done _) = 2 permImplSucceeds (PermImpl_Step (Impl1_Fail _) _) = 0 permImplSucceeds (PermImpl_Step Impl1_Catch - (MbPermImpls_Cons (MbPermImpls_Cons _ mb_impl1) mb_impl2)) = + (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2)) = max (mbLift $ fmap permImplSucceeds mb_impl1) (mbLift $ fmap permImplSucceeds mb_impl2) -permImplSucceeds (PermImpl_Step (Impl1_Push _ _) (MbPermImpls_Cons _ mb_impl)) = +permImplSucceeds (PermImpl_Step (Impl1_Push _ _) (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl -permImplSucceeds (PermImpl_Step (Impl1_Pop _ _) (MbPermImpls_Cons _ mb_impl)) = +permImplSucceeds (PermImpl_Step (Impl1_Pop _ _) (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl permImplSucceeds (PermImpl_Step (Impl1_ElimOr _ _ _) - (MbPermImpls_Cons (MbPermImpls_Cons _ mb_impl1) mb_impl2)) = + (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2)) = max (mbLift (fmap permImplSucceeds mb_impl1)) (mbLift (fmap permImplSucceeds mb_impl2)) permImplSucceeds (PermImpl_Step (Impl1_ElimExists _ _) - (MbPermImpls_Cons _ mb_impl)) = + (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl permImplSucceeds (PermImpl_Step (Impl1_Simpl _ _) - (MbPermImpls_Cons _ mb_impl)) = + (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl permImplSucceeds (PermImpl_Step (Impl1_LetBind _ _) - (MbPermImpls_Cons _ mb_impl)) = + (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl permImplSucceeds (PermImpl_Step (Impl1_ElimStructField _ _ _ _) - (MbPermImpls_Cons _ mb_impl)) = + (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl permImplSucceeds (PermImpl_Step (Impl1_ElimLLVMFieldContents _ _) - (MbPermImpls_Cons _ mb_impl)) = + (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl permImplSucceeds (PermImpl_Step (Impl1_ElimLLVMBlockToEq _ _) - (MbPermImpls_Cons _ mb_impl)) = + (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl permImplSucceeds (PermImpl_Step Impl1_BeginLifetime - (MbPermImpls_Cons _ mb_impl)) = + (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl permImplSucceeds (PermImpl_Step (Impl1_TryProveBVProp _ _ _) - (MbPermImpls_Cons _ mb_impl)) = + (MbPermImpls_Cons _ _ mb_impl)) = mbLift $ fmap permImplSucceeds mb_impl -- FIXME: no longer needed...? -traversePermImpl :: forall m ps r1 r2. - MonadStrongBind m => (forall ps'. r1 ps' -> m (r2 ps')) -> - PermImpl r1 ps -> m (PermImpl r2 ps) -traversePermImpl f (PermImpl_Done r) = PermImpl_Done <$> f r -traversePermImpl f (PermImpl_Step impl1 mb_perm_impls) = - PermImpl_Step impl1 <$> helper mb_perm_impls - where - helper :: MbPermImpls r1 bs_pss -> m (MbPermImpls r2 bs_pss) - helper MbPermImpls_Nil = return MbPermImpls_Nil - helper (MbPermImpls_Cons mb_impls mb_impl) = - do mb_impls' <- helper mb_impls - mb_impl' <- strongMbM (fmap (traversePermImpl f) mb_impl) - return (MbPermImpls_Cons mb_impls' mb_impl') +-- traversePermImpl :: forall m ps r1 r2. +-- MonadStrongBind m => (forall ps'. r1 ps' -> m (r2 ps')) -> +-- PermImpl r1 ps -> m (PermImpl r2 ps) +-- traversePermImpl f (PermImpl_Done r) = PermImpl_Done <$> f r +-- traversePermImpl f (PermImpl_Step impl1 mb_perm_impls) = +-- PermImpl_Step impl1 <$> helper mb_perm_impls +-- where +-- helper :: MbPermImpls r1 bs_pss -> m (MbPermImpls r2 bs_pss) +-- helper MbPermImpls_Nil = return MbPermImpls_Nil +-- helper (MbPermImpls_Cons _ mb_impls mb_impl) = +-- do mb_impls' <- helper mb_impls +-- mb_impl' <- strongMbM (fmap (traversePermImpl f) mb_impl) +-- return (MbPermImpls_Cons _ mb_impls' mb_impl') -- | Assert a condition and print an error message if it fails -- @@ -2491,8 +2494,9 @@ instance (NuMatchingAny1 r, SubstVar PermVarSubst m, Substable PermVarSubst (MbPermImpls r bs_pss) m where genSubst s mb_impls = case mbMatch mb_impls of [nuMP| MbPermImpls_Nil |] -> return MbPermImpls_Nil - [nuMP| MbPermImpls_Cons mb_impl mb_impls' |] -> - MbPermImpls_Cons <$> genSubst s mb_impl <*> genSubst s mb_impls' + [nuMP| MbPermImpls_Cons mpx mb_impl mb_impls' |] -> + let px = mbLift mpx in + MbPermImpls_Cons px <$> genSubst s mb_impl <*> genSubstMb (cruCtxProxies px) s mb_impls' -- FIXME: shouldn't need the SubstVar PermVarSubst m assumption... instance SubstVar PermVarSubst m => @@ -3199,7 +3203,7 @@ implApplyImpl1 impl1 mb_ms = (State (Closed s) (MbPermImpls r ps_outs)) a helper MbPermSets_Nil _ = gabortM (return MbPermImpls_Nil) helper (MbPermSets_Cons mbperms ctx mbperm) (args :>: Impl1Cont f) = - gparallel (\m1 m2 -> MbPermImpls_Cons <$> m1 <*> m2) + gparallel (\m1 m2 -> MbPermImpls_Cons ctx <$> m1 <*> m2) (helper mbperms args) (gopenBinding strongMbM mbperm >>>= \(ns, perms') -> gmodify (set implStatePerms perms' . @@ -4139,7 +4143,7 @@ implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape = -- SImpl_IntroLLVMBlockFromEq, and then recursively eliminate the resulting -- memblock permission mbVarsM () >>>= \mb_unit -> - withExtVarsM (proveVarImplInt y $ mbCombine $ flip fmap mb_unit $ const $ + withExtVarsM (proveVarImplInt y $ mbCombine RL.typeCtxProxies $ flip fmap mb_unit $ const $ nu $ \sh -> ValPerm_Conj1 $ Perm_LLVMBlockShape $ PExpr_Var sh) >>>= \(_, sh) -> let bp' = bp { llvmBlockShape = sh } in @@ -4780,7 +4784,7 @@ type NeededPerms vars = Some (RAssign (Compose (Mb vars) VarAndPerm)) neededPermsToExDistPerms :: RAssign prx vars -> RAssign (Compose (Mb vars) VarAndPerm) ps -> Mb vars (DistPerms ps) -neededPermsToExDistPerms vars MNil = nuMulti vars (const MNil) +neededPermsToExDistPerms vars MNil = nuMulti (RL.map (\_-> Proxy) vars) (const MNil) neededPermsToExDistPerms vars (ps :>: Compose mb_vap) = mbMap2 (:>:) (neededPermsToExDistPerms vars ps) mb_vap @@ -5591,7 +5595,7 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of -- Locally bind z_sh for the shape of the memblock perm and recurse let mb_bp' = - mbCombine $ flip fmap mb_bp $ \bp -> + mbCombine RL.typeCtxProxies $ flip fmap mb_bp $ \bp -> nu $ \z_sh -> bp { llvmBlockShape = PExpr_Var z_sh } in proveVarLLVMBlocksExt1 x ps psubst mb_bp' mb_bps mb_ps >>> @@ -5692,7 +5696,7 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of -- Locally bind z_sh for the shape of the memblock perm and recurse let mb_bp' = - mbCombine $ flip fmap mb_bp $ \bp -> + mbCombine RL.typeCtxProxies $ flip fmap mb_bp $ \bp -> nu $ \z_sh -> bp { llvmBlockShape = PExpr_Var z_sh } in proveVarLLVMBlocksExt1 x ps psubst mb_bp' mb_bps mb_ps >>> @@ -5886,7 +5890,7 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of -- Prove the sub-shape in the context of a new existential variable let mb_bp' = - mbCombine $ + mbCombine RL.typeCtxProxies $ mbMap2 (\bp mb_sh -> fmap (\sh -> bp { llvmBlockShape = sh }) mb_sh) mb_bp mb_mb_sh in @@ -5897,7 +5901,7 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of implSplitSwapConjsM x ps' 1 >>> -- Prove an existential around the memblock permission we proved - partialSubstForceM (mbMap2 (,) + partialSubstForceM (mbMap2 (,) mb_bp mb_mb_sh) "proveVarLLVMBlock" >>>= \(bp,mb_sh) -> introExistsM x e (fmap (\sh -> ValPerm_LLVMBlock $ bp { llvmBlockShape = sh }) mb_sh) >>> @@ -5945,7 +5949,7 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of -- Recursively prove a membblock with shape fieldsh(eq(y)) for fresh evar y let mb_bp' = - mbCombine $ flip fmap mb_bp $ \bp -> + mbCombine RL.typeCtxProxies $ flip fmap mb_bp $ \bp -> nu $ \(y :: ExprVar (LLVMPointerType sz)) -> bp { llvmBlockShape = PExpr_FieldShape $ LLVMFieldShape $ @@ -5994,7 +5998,7 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of -- the first one has the length of the atomic perm we found and the other -- has the remaining length, and recurse let mb_bps12 = - mbCombine $ flip fmap mb_bp $ \bp -> + mbCombine RL.typeCtxProxies $ flip fmap mb_bp $ \bp -> nuMulti (MNil :>: Proxy :>: Proxy) $ \(_ :>: z_sh1 :>: z_sh2) -> [bp { llvmBlockLen = len1, llvmBlockShape = PExpr_Var z_sh1 }, bp { llvmBlockOffset = bvAdd (llvmBlockOffset bp) len1, @@ -6120,9 +6124,12 @@ proveVarAtomicImplUnfoldOrFail x ps mb_ap = -- the LHS is on the top of the stack and represents all the permissions on @x@, -- i.e., we also assume the variable permissions for @x@ are currently -- @true@. Any remaining perms for @x@ are popped off of the stack. -proveVarAtomicImpl :: NuMatchingAny1 r => ExprVar a -> [AtomicPerm a] -> - Mb vars (AtomicPerm a) -> - ImplM vars s r (ps :> a) (ps :> a) () +proveVarAtomicImpl :: + NuMatchingAny1 r => + ExprVar a -> + [AtomicPerm a] -> + Mb vars (AtomicPerm a) -> + ImplM vars s r (ps :> a) (ps :> a) () proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of [nuMP| Perm_LLVMField mb_fp |] -> @@ -6217,7 +6224,9 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of -- just builds the equality proofs and computes the new LHS and RHS, but -- we don't actually perform the casts until later. substEqsWithProof (ps_inL, ps_outL) >>>= \eqp_psL -> - substEqsWithProof (mb_ps_inR, mb_ps_outR) >>>= \eqp_mb_psR -> + gget >>>= \s -> + give (cruCtxProxies (view implStateVars s)) + (substEqsWithProof (mb_ps_inR, mb_ps_outR)) >>>= \eqp_mb_psR -> let (ps_inL',ps_outL') = someEqProofRHS eqp_psL (mb_ps_inR',mb_ps_outR') = someEqProofRHS eqp_mb_psR in @@ -6484,7 +6493,7 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of -- Prove x:exists (z:tp).p by proving x:p in an extended vars context (_, [nuMP| ValPerm_Exists mb_p' |]) -> - withExtVarsM (proveVarImplH x p $ mbCombine mb_p') >>>= \((), e) -> + withExtVarsM (proveVarImplH x p (mbCombine RL.typeCtxProxies mb_p')) >>>= \((), e) -> partialSubstForceM mb_p' "proveVarImpl" >>>= introExistsM x e diff --git a/src/Verifier/SAW/Heapster/Permissions.hs b/src/Verifier/SAW/Heapster/Permissions.hs index c14d051..699cf39 100644 --- a/src/Verifier/SAW/Heapster/Permissions.hs +++ b/src/Verifier/SAW/Heapster/Permissions.hs @@ -34,6 +34,7 @@ import Data.List hiding (sort) import Data.List.NonEmpty (NonEmpty(..)) import Data.String import Data.Proxy +import Data.Reflection import Data.Functor.Constant import qualified Data.BitVector.Sized as BV import Data.BitVector.Sized (BV) @@ -4318,13 +4319,17 @@ mbFunPerm :: CruCtx ctx -> Mb ctx (ValuePerms ctx) -> mbFunPerm ctx mb_ps (mbMatch -> [nuMP| FunPerm mb_ghosts mb_args mb_ret ps_in ps_out |]) = let ghosts = mbLift mb_ghosts args = mbLift mb_args - ctx_perms = trueValuePerms $ cruCtxToTypes ctx in - case RL.appendAssoc ctx ghosts (cruCtxToTypes args) of + ctx_perms = trueValuePerms $ cruCtxToTypes ctx + arg_types = cruCtxToTypes args + ghost_types = cruCtxToTypes ghosts + prxys = mapRAssign (const Proxy) (RL.append ghost_types arg_types) in + case RL.appendAssoc ctx ghosts arg_types of Refl -> FunPerm (appendCruCtx ctx ghosts) args (mbLift mb_ret) - (mbCombine $ + (mbCombine prxys $ mbMap2 (\ps mb_ps_in -> fmap (RL.append ps) mb_ps_in) mb_ps ps_in) - (fmap (RL.append ctx_perms) $ mbCombine ps_out) + (fmap (RL.append ctx_perms) $ + mbCombine (prxys :>: Proxy) ps_out) -- | Substitute ghost and regular arguments into a function permission to get -- its input permissions for those arguments, where ghost arguments are given @@ -4909,17 +4914,30 @@ instance (Substable s a m, Substable s b m, Substable s c m, Substable s d m) => Substable s (a,b,c,d) m where genSubst s abcd = (,,,) <$> genSubst s (fmap (\(a,_,_,_) -> a) abcd) - <*> genSubst s (fmap (\(_,b,_,_) -> b) abcd) - <*> genSubst s (fmap (\(_,_,c,_) -> c) abcd) - <*> genSubst s (fmap (\(_,_,_,d) -> d) abcd) + <*> genSubst s (fmap (\(_,b,_,_) -> b) abcd) + <*> genSubst s (fmap (\(_,_,c,_) -> c) abcd) + <*> genSubst s (fmap (\(_,_,_,d) -> d) abcd) instance (NuMatching a, Substable s a m) => Substable s (Maybe a) m where genSubst s mb_x = case mbMatch mb_x of [nuMP| Just a |] -> Just <$> genSubst s a [nuMP| Nothing |] -> return Nothing -instance (Substable s a m, NuMatching a) => Substable s (Mb ctx a) m where - genSubst s mbmb = mbM $ fmap (genSubst s) (mbSwap mbmb) +instance {-# INCOHERENT #-} (Given (RAssign Proxy ctx), Substable s a m, NuMatching a) => Substable s (Mb ctx a) m where + genSubst = genSubstMb given + +instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Mb RNil a) m where + genSubst = genSubstMb RL.typeCtxProxies + +instance {-# INCOHERENT #-} (Substable s a m, NuMatching a) => Substable s (Binding c a) m where + genSubst = genSubstMb RL.typeCtxProxies + +genSubstMb :: + Substable s a m => + NuMatching a => + RAssign Proxy ctx -> + s ctx' -> Mb ctx' (Mb ctx a) -> m (Mb ctx a) +genSubstMb p s mbmb = mbM (fmap (genSubst s) (mbSwap p mbmb)) instance SubstVar s m => Substable s (Member ctx a) m where genSubst _ mb_memb = return $ mbLift mb_memb @@ -5003,7 +5021,7 @@ instance SubstVar s m => Substable s (PermExpr a) m where [nuMP| PExpr_OrShape sh1 sh2 |] -> PExpr_OrShape <$> genSubst s sh1 <*> genSubst s sh2 [nuMP| PExpr_ExShape mb_sh |] -> - PExpr_ExShape <$> genSubst s mb_sh + PExpr_ExShape <$> genSubstMb RL.typeCtxProxies s mb_sh [nuMP| PExpr_ValPerm p |] -> PExpr_ValPerm <$> genSubst s p @@ -5050,17 +5068,22 @@ instance SubstVar s m => Substable s (AtomicPerm a) m where instance SubstVar s m => Substable s (NamedShape b args w) m where genSubst s (mbMatch -> [nuMP| NamedShape str args body |]) = - NamedShape (mbLift str) (mbLift args) <$> genSubst s body + NamedShape (mbLift str) (mbLift args) <$> genSubstNSB (cruCtxProxies (mbLift args)) s body -instance SubstVar s m => Substable s (NamedShapeBody b args w) m where - genSubst s mb_body = case mbMatch mb_body of +genSubstNSB :: + SubstVar s m => + RAssign Proxy args -> + s ctx -> Mb ctx (NamedShapeBody b args w) -> m (NamedShapeBody b args w) +genSubstNSB px s mb_body = case mbMatch mb_body of [nuMP| DefinedShapeBody mb_sh |] -> - DefinedShapeBody <$> genSubst s mb_sh + DefinedShapeBody <$> genSubstMb px s mb_sh [nuMP| OpaqueShapeBody mb_len trans_id |] -> - OpaqueShapeBody <$> genSubst s mb_len <*> return (mbLift trans_id) + OpaqueShapeBody <$> genSubstMb px s mb_len <*> return (mbLift trans_id) [nuMP| RecShapeBody mb_sh trans_id fold_id unfold_id |] -> - RecShapeBody <$> genSubst s mb_sh <*> return (mbLift trans_id) - <*> return (mbLift fold_id) <*> return (mbLift unfold_id) + RecShapeBody <$> genSubstMb (px :>: Proxy) s mb_sh + <*> return (mbLift trans_id) + <*> return (mbLift fold_id) + <*> return (mbLift unfold_id) instance SubstVar s m => Substable s (NamedPermName ns args a) m where genSubst _ mb_rpn = return $ mbLift mb_rpn @@ -5072,8 +5095,8 @@ instance SubstVar s m => Substable s (PermOffset a) m where instance SubstVar s m => Substable s (NamedPerm ns args a) m where genSubst s mb_np = case mbMatch mb_np of - [nuMP| NamedPerm_Opaque p |] -> NamedPerm_Opaque <$> genSubst s p - [nuMP| NamedPerm_Rec p |] -> NamedPerm_Rec <$> genSubst s p + [nuMP| NamedPerm_Opaque p |] -> NamedPerm_Opaque <$> genSubst s p + [nuMP| NamedPerm_Rec p |] -> NamedPerm_Rec <$> genSubst s p [nuMP| NamedPerm_Defined p |] -> NamedPerm_Defined <$> genSubst s p instance SubstVar s m => Substable s (OpaquePerm ns args a) m where @@ -5083,11 +5106,11 @@ instance SubstVar s m => Substable s (OpaquePerm ns args a) m where instance SubstVar s m => Substable s (RecPerm ns reach args a) m where genSubst s (mbMatch -> [nuMP| RecPerm rpn dt_i f_i u_i reachMeths cases |]) = RecPerm (mbLift rpn) (mbLift dt_i) (mbLift f_i) (mbLift u_i) - (mbLift reachMeths) <$> mapM (genSubst s) (mbList cases) + (mbLift reachMeths) <$> mapM (genSubstMb (cruCtxProxies (mbLift (fmap namedPermNameArgs rpn))) s) (mbList cases) instance SubstVar s m => Substable s (DefinedPerm ns args a) m where genSubst s (mbMatch -> [nuMP| DefinedPerm n p |]) = - DefinedPerm (mbLift n) <$> genSubst s p + DefinedPerm (mbLift n) <$> genSubstMb (cruCtxProxies (mbLift (fmap namedPermNameArgs n))) s p instance SubstVar s m => Substable s (ValuePerm a) m where genSubst s mb_p = case mbMatch mb_p of @@ -5097,7 +5120,7 @@ instance SubstVar s m => Substable s (ValuePerm a) m where [nuMP| ValPerm_Exists p |] -> -- FIXME: maybe we don't need extSubst at all, but can just use the -- Substable instance for Mb ctx a from above - ValPerm_Exists <$> genSubst s p + ValPerm_Exists <$> genSubstMb RL.typeCtxProxies s p -- nuM (\x -> genSubst (extSubst s x) $ mbCombine p) [nuMP| ValPerm_Named n args off |] -> ValPerm_Named (mbLift n) <$> genSubst s args <*> genSubst s off @@ -5170,8 +5193,13 @@ instance SubstVar s m => Substable1 s LOwnedPerm m where instance SubstVar s m => Substable s (FunPerm ghosts args ret) m where genSubst s (mbMatch -> [nuMP| FunPerm ghosts args ret perms_in perms_out |]) = - FunPerm (mbLift ghosts) (mbLift args) (mbLift ret) - <$> genSubst s perms_in <*> genSubst s perms_out + let gpx = mbLift ghosts + apx = mbLift args + rpx = mbLift ret + gapx = RL.append (cruCtxProxies gpx) (cruCtxProxies apx) in + FunPerm gpx apx rpx + <$> genSubstMb gapx s perms_in + <*> genSubstMb (gapx :>: Proxy) s perms_out instance SubstVar PermVarSubst m => Substable PermVarSubst (LifetimeCurrentPerms ps) m where @@ -5387,7 +5415,7 @@ emptyPSubst = PartialSubst . helper where -- substitution inside a binding for all of its variables psubstMbDom :: PartialSubst ctx -> Mb ctx (NameSet CrucibleType) psubstMbDom (PartialSubst elems) = - nuMulti elems $ \ns -> + nuMulti (RL.map (\_-> Proxy) elems) $ \ns -> NameSet.fromList $ catMaybes $ RL.toList $ RL.map2 (\n (PSubstElem maybe_e) -> if isJust maybe_e @@ -5398,7 +5426,7 @@ psubstMbDom (PartialSubst elems) = -- substitution inside a binding for all of its variables psubstMbUnsetVars :: PartialSubst ctx -> Mb ctx (NameSet CrucibleType) psubstMbUnsetVars (PartialSubst elems) = - nuMulti elems $ \ns -> + nuMulti (RL.map (\_ -> Proxy) elems) $ \ns -> NameSet.fromList $ catMaybes $ RL.toList $ RL.map2 (\n (PSubstElem maybe_e) -> if maybe_e == Nothing @@ -5456,7 +5484,7 @@ instance SubstVar PartialSubst Maybe where -- | Wrapper function to apply a partial substitution to an expression type partialSubst :: Substable PartialSubst a Maybe => PartialSubst ctx -> Mb ctx a -> Maybe a -partialSubst s mb = genSubst s mb +partialSubst = genSubst -- | Apply a partial substitution, raising an error (with the given string) if -- this fails @@ -5627,7 +5655,8 @@ instance AbstractVars a => AbstractVars (Mb (ctx :: RList Type) a) where mbLift $ nuMultiWithElim1 (\ns a -> - clApply ( $(mkClosed [| \prxs -> fmap mbSwap . mbSeparate prxs |]) + clApply ( $(mkClosed [| \prxs2 prxs -> fmap (mbSwap prxs2) . mbSeparate prxs |]) + `clApply` closedProxies ns2 `clApply` closedProxies ns) <$> abstractPEVars (append ns1 ns) ns2 a) mb diff --git a/src/Verifier/SAW/Heapster/RustTypes.hs b/src/Verifier/SAW/Heapster/RustTypes.hs index c752ce5..1abd194 100644 --- a/src/Verifier/SAW/Heapster/RustTypes.hs +++ b/src/Verifier/SAW/Heapster/RustTypes.hs @@ -137,7 +137,7 @@ rustCtxOfNames tp = inRustCtx :: NuMatching a => RustCtx ctx -> RustConvM a -> RustConvM (Mb ctx a) inRustCtx ctx m = - mbM $ nuMulti ctx $ \ns -> + mbM $ nuMulti (RL.map (\_-> Proxy) ctx) $ \ns -> let ns_ctx = RL.toList $ RL.map2 (\n (Pair (Constant str) tp) -> Constant (str, Some (Typed tp n))) ns ctx in @@ -351,7 +351,8 @@ data ArgLayout where instance Semigroup ArgLayout where ArgLayout ghosts1 args1 mb_ps1 <> ArgLayout ghosts2 args2 mb_ps2 = ArgLayout (RL.append ghosts1 ghosts2) (RL.append args1 args2) $ - mbCombine $ fmap (\ps1 -> fmap (\ps2 -> RL.append ps1 ps2) mb_ps2) mb_ps1 + mbCombine (RL.mapRAssign (const Proxy) ghosts2) $ + fmap (\ps1 -> fmap (\ps2 -> RL.append ps1 ps2) mb_ps2) mb_ps1 instance Monoid ArgLayout where mempty = ArgLayout MNil MNil (emptyMb $ MNil) @@ -365,8 +366,8 @@ argLayout1 p = -- additional ghost argument for the bound name mbArgLayout :: KnownRepr TypeRepr a => Binding a ArgLayout -> ArgLayout mbArgLayout (mbMatch -> [nuMP| ArgLayout ghosts args mb_ps |]) = - ArgLayout (mbLift ghosts :>: KnownReprObj) (mbLift args) (mbCombine $ - mbSwap mb_ps) + ArgLayout (mbLift ghosts :>: KnownReprObj) (mbLift args) + (mbCombine RL.typeCtxProxies (mbSwap (RL.mapRAssign (const Proxy) (mbLift ghosts)) mb_ps)) -- | Convert an 'ArgLayout' to a permission on a @struct@ of its arguments argLayoutStructPerm :: ArgLayout -> Some (Typed ValuePerm) @@ -433,18 +434,23 @@ funPerm3FromArgLayout (ArgLayout ghosts args mb_arg_perms) ret_tp ret_perm = let gs_args_prxs = RL.map (const Proxy) (RL.append ghosts args) in Some3FunPerm $ FunPerm (knownCtxToCruCtx ghosts) (knownCtxToCruCtx args) ret_tp - (extMbMulti args $ + (extMbMulti (RL.map (\_ -> Proxy) args) $ fmap (RL.append $ RL.map (const ValPerm_True) ghosts) mb_arg_perms) (nuMulti (gs_args_prxs :>: Proxy) $ const (RL.map (const ValPerm_True) gs_args_prxs :>: ret_perm)) -- | Extend a name binding by adding a name in the middle -extMbMiddle :: prx1 ctx1 -> RAssign prx2 ctx2 -> prxb b -> - Mb (ctx1 :++: ctx2) a -> - Mb (ctx1 :++: ((RNil :> b) :++: ctx2)) a +extMbMiddle :: + forall prx1 ctx1 prx2 ctx2 prxb a b. + prx1 ctx1 -> RAssign prx2 ctx2 -> prxb b -> + Mb (ctx1 :++: ctx2) a -> + Mb (ctx1 :++: ((RNil :> b) :++: ctx2)) a extMbMiddle (_ :: prx1 ctx1) ctx2 (_ :: prxb b) mb_a = - mbCombine $ fmap (mbCombine . nu @_ @b . const) $ + mbCombine (RL.append (MNil :>: (Proxy :: Proxy b)) pxys) $ + fmap (mbCombine pxys . nu @_ @b . const) $ mbSeparate @_ @ctx1 ctx2 mb_a + where + pxys = RL.mapRAssign (const Proxy) ctx2 -- | Insert an object into the middle of an 'RAssign' rassignInsertMiddle :: prx1 ctx1 -> RAssign prx2 ctx2 -> f b -> @@ -475,15 +481,22 @@ mbAssoc :: prx1 ctx1 -> RAssign prx2 ctx2 -> RAssign prx3 ctx3 -> Mb (ctx1 :++: (ctx2 :++: ctx3)) a -> Mb ((ctx1 :++: ctx2) :++: ctx3) a mbAssoc ctx1 ctx2 ctx3 mb_a = - mbCombine $ mbCombine $ fmap (mbSeparatePrx ctx2 ctx3) $ + mbCombine (RL.mapRAssign (const Proxy) ctx3) $ + mbCombine (RL.mapRAssign (const Proxy) ctx2) $ + fmap (mbSeparatePrx ctx2 ctx3) $ mbSeparatePrx ctx1 (RL.append (RL.map (const Proxy) ctx2) (RL.map (const Proxy) ctx3)) mb_a -mbCombineAssoc :: prx1 ctx1 -> prx2 ctx2 -> RAssign prx3 ctx3 -> - Mb ctx1 (Mb (ctx2 :++: ctx3) a) -> - Mb ((ctx1 :++: ctx2) :++: ctx3) a -mbCombineAssoc _ ctx2 ctx3 = - mbCombine . mbCombine . fmap (mbSeparatePrx ctx2 ctx3) +mbCombineAssoc :: + prx1 ctx1 -> + RAssign prx2 ctx2 -> + RAssign prx3 ctx3 -> + Mb ctx1 (Mb (ctx2 :++: ctx3) a) -> + Mb ((ctx1 :++: ctx2) :++: ctx3) a +mbCombineAssoc _ ctx2 ctx3 + = mbCombine (RL.mapRAssign (const Proxy) ctx3) + . mbCombine (RL.mapRAssign (const Proxy) ctx2) + . fmap (mbSeparatePrx ctx2 ctx3) assocAppend :: RAssign f ctx1 -> prx2 ctx2 -> RAssign prx3 ctx3 -> RAssign f (ctx2 :++: ctx3) -> @@ -505,10 +518,12 @@ mbGhostsFunPerm3 new_ghosts (mbMatch -> [nuMP| Some3FunPerm mbLift ghosts) (mbLift args) (mbLift ret) (mbAssoc new_prxs ghosts_prxs args_prxs $ fmap (assocAppend (RL.map (const ValPerm_True) new_prxs) - ghosts_prxs args_prxs) $ mbCombine ps_in) + ghosts_prxs args_prxs) $ + mbCombine (RL.append ghosts_prxs args_prxs) ps_in) (mbAssoc new_prxs ghosts_prxs (args_prxs :>: Proxy) $ fmap (assocAppend (RL.map (const ValPerm_True) new_prxs) - ghosts_prxs (args_prxs :>: Proxy)) $ mbCombine ps_out) + ghosts_prxs (args_prxs :>: Proxy)) $ + mbCombine (RL.append ghosts_prxs args_prxs :>: Proxy) ps_out) -- | Try to compute the layout of a structure of the given shape as a value, -- over 1 or more registers, if this is possible @@ -656,7 +671,8 @@ instance Functor SomeTypedMb where instance Applicative SomeTypedMb where pure a = SomeTypedMb CruCtxNil $ emptyMb a liftA2 f (SomeTypedMb ctx1 mb_a1) (SomeTypedMb ctx2 mb_a2) = - SomeTypedMb (appendCruCtx ctx1 ctx2) $ mbCombine $ + SomeTypedMb (appendCruCtx ctx1 ctx2) $ + mbCombine (cruCtxProxies ctx2) $ flip fmap mb_a1 $ \a1 -> flip fmap mb_a2 $ \a2 -> f a1 a2 -- | Abstract over all the read/write and lifetime modalities in an @@ -714,9 +730,6 @@ lownedPermsForLifetime l (_ :>: vap) = lifetimeDefName :: LifetimeDef a -> String lifetimeDefName (LifetimeDef _ (Lifetime name _) _ _) = name -extMbOuter :: RAssign prx ctx1 -> Mb ctx2 a -> Mb (ctx1 :++: ctx2) a -extMbOuter prxs mb_a = mbCombine $ nuMulti prxs $ const mb_a - -- | Add a lifetime described by a 'LifetimeDef' to a 'Some3FunPerm' mbLifetimeFunPerm :: LifetimeDef Span -> Binding LifetimeType Some3FunPerm -> RustConvM Some3FunPerm @@ -727,10 +740,10 @@ mbLifetimeFunPerm (LifetimeDef _ _ [] _) let args_prxs = cruCtxProxies args let ret = mbLift $ fmap funPermRet fun_perm let mb_ps_in = - mbCombineAssoc (MNil :>: Proxy) ghosts args_prxs $ + mbCombineAssoc (MNil :>: Proxy) (cruCtxProxies ghosts) args_prxs $ fmap (mbValuePermsToDistPerms . funPermIns) fun_perm let mb_ps_out = - mbCombineAssoc (MNil :>: Proxy) ghosts (args_prxs :>: Proxy) $ + mbCombineAssoc (MNil :>: Proxy) (cruCtxProxies ghosts) (args_prxs :>: Proxy) $ fmap (mbValuePermsToDistPerms . funPermOuts) fun_perm let mb_l = extMbMulti (cruCtxProxies args) $ diff --git a/src/Verifier/SAW/Heapster/SAWTranslation.hs b/src/Verifier/SAW/Heapster/SAWTranslation.hs index f642137..4265f96 100644 --- a/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -323,7 +323,7 @@ nuMultiTransM :: TransInfo info => (RAssign Name ctx -> b) -> TransM info ctx (Mb ctx b) nuMultiTransM f = do info <- ask - return $ nuMulti (infoCtx info) f + return $ nuMulti (RL.map (\_ -> Proxy) (infoCtx info)) f -- | Apply the result of a translation to that of another applyTransM :: TransM info ctx OpenTerm -> TransM info ctx OpenTerm -> @@ -801,7 +801,7 @@ instance TransInfo info => [nuMP| PExpr_ExShape mb_sh |] -> do tp_trans <- translate $ fmap bindingType mb_sh tp_f_trm <- lambdaTupleTransM "x_exsh" tp_trans $ \e -> - transTupleTerm <$> inExtTransM e (translate $ mbCombine mb_sh) + transTupleTerm <$> inExtTransM e (translate $ mbCombine RL.typeCtxProxies mb_sh) return $ ETrans_Term (dataTypeOpenTerm "Prelude.Sigma" [typeTransTupleType tp_trans, tp_f_trm]) @@ -1066,7 +1066,7 @@ eqPermTransCtx :: forall (ctx :: RList CrucibleType) (ps :: RList CrucibleType) RAssign any ctx -> RAssign (Member ctx) ps -> PermTransCtx ctx ps eqPermTransCtx ns = - RL.map (\memb -> PTrans_Eq $ nuMulti ns (PExpr_Var . RL.get memb)) + RL.map (\memb -> PTrans_Eq $ nuMulti (RL.map (\_-> Proxy) ns) (PExpr_Var . RL.get memb)) instance IsTermTrans (PermTrans ctx a) where @@ -1174,7 +1174,9 @@ permTransPermEq ptrans mb_p = extsMb :: CruCtx ctx2 -> Mb ctx a -> Mb (ctx :++: ctx2) a -extsMb ctx = mbCombine . fmap (nus (cruCtxProxies ctx) . const) +extsMb ctx = mbCombine proxies . fmap (nus proxies . const) + where + proxies = cruCtxProxies ctx -- | Generic function to extend the context of the translation of a permission class ExtPermTrans f where @@ -1556,7 +1558,7 @@ instance TransInfo info => tp_trans <- translateClosed tp mkPermTypeTrans1 p <$> sigmaTypeTransM "x_ex" tp_trans (\x -> inExtTransM x $ - translate $ mbCombine p1) + translate $ mbCombine RL.typeCtxProxies p1) [nuMP| ValPerm_Named npn args off |] -> do env <- infoEnv <$> ask args_trans <- translate args @@ -1713,10 +1715,12 @@ instance TransInfo info => instance TransInfo info => Translate info ctx (FunPerm ghosts args ret) OpenTerm where translate (mbMatch -> [nuMP| FunPerm ghosts args ret perms_in perms_out |]) = - piExprCtx (appendCruCtx (mbLift ghosts) (mbLift args)) $ - piPermCtx (mbCombine perms_in) $ \_ -> + let ctx = appendCruCtx (mbLift ghosts) (mbLift args) + pxys = cruCtxProxies ctx in + piExprCtx ctx $ + piPermCtx (mbCombine pxys perms_in) $ \_ -> applyTransM (return $ globalOpenTerm "Prelude.CompM") $ - translateRetType (mbLift ret) $ mbCombine perms_out + translateRetType (mbLift ret) $ mbCombine (pxys :>: Proxy) perms_out -- | Lambda-abstraction over a permission lambdaPermTrans :: TransInfo info => String -> Mb ctx (ValuePerm a) -> @@ -2071,7 +2075,7 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of tp_trans <- translateClosed tp etrans <- translate e sigma_trm <- - sigmaTransM "x_ex" tp_trans (flip inExtTransM $ translate $ mbCombine p) + sigmaTransM "x_ex" tp_trans (flip inExtTransM $ translate $ mbCombine RL.typeCtxProxies p) etrans getTopPermM withPermStackM id ((:>: PTrans_Term (fmap ValPerm_Exists p) sigma_trm) . RL.tail) @@ -2982,14 +2986,15 @@ implTransAltErr str (ImplFailContMsg _) = -- translation function if the argument succeeds and fails if the translation of -- the argument fails translatePermImplUnary :: + RL.TypeCtx bs => ImplTranslateF r ext blocks tops ret => Mb ctx (MbPermImpls r (RNil :> '(bs,ps_out))) -> (ImpTransM ext blocks tops ret ps_out (ctx :++: bs) OpenTerm -> ImpTransM ext blocks tops ret ps ctx OpenTerm) -> PermImplTransM (ImplFailCont -> - ImpTransM ext blocks tops ret ps ctx OpenTerm) -translatePermImplUnary (mbMatch -> [nuMP| MbPermImpls_Cons _ mb_impl |]) f = - translatePermImpl Proxy (mbCombine mb_impl) >>= \trans -> + ImpTransM ext blocks tops ret ps ctx OpenTerm) +translatePermImplUnary (mbMatch -> [nuMP| MbPermImpls_Cons _ _ mb_impl |]) f = + translatePermImpl Proxy (mbCombine RL.typeCtxProxies mb_impl) >>= \trans -> return $ \k -> f $ trans k @@ -3008,9 +3013,9 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl tell [mbLift str] >> mzero ([nuMP| Impl1_Catch |], - [nuMP| (MbPermImpls_Cons (MbPermImpls_Cons _ mb_impl1) mb_impl2) |]) -> - pitmCatching (translatePermImpl prx $ mbCombine mb_impl1) >>= \maybe_trans1 -> - pitmCatching (translatePermImpl prx $ mbCombine mb_impl2) >>= \maybe_trans2 -> + [nuMP| (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |]) -> + pitmCatching (translatePermImpl prx $ mbCombine RL.typeCtxProxies mb_impl1) >>= \maybe_trans1 -> + pitmCatching (translatePermImpl prx $ mbCombine RL.typeCtxProxies mb_impl2) >>= \maybe_trans2 -> case (maybe_trans1, maybe_trans2) of (Just trans1, Just trans2) -> return $ \k -> @@ -3040,9 +3045,9 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl -- If both branches of an or elimination fail, the whole thing fails; otherwise, -- an or elimination performs a pattern-match on an Either ([nuMP| Impl1_ElimOr x p1 p2 |], - [nuMP| (MbPermImpls_Cons (MbPermImpls_Cons _ mb_impl1) mb_impl2) |]) -> - pitmCatching (translatePermImpl prx $ mbCombine mb_impl1) >>= \maybe_trans1 -> - pitmCatching (translatePermImpl prx $ mbCombine mb_impl2) >>= \maybe_trans2 -> + [nuMP| (MbPermImpls_Cons _ (MbPermImpls_Cons _ _ mb_impl1) mb_impl2) |]) -> + pitmCatching (translatePermImpl prx $ mbCombine RL.typeCtxProxies mb_impl1) >>= \maybe_trans1 -> + pitmCatching (translatePermImpl prx $ mbCombine RL.typeCtxProxies mb_impl2) >>= \maybe_trans2 -> case (maybe_trans1, maybe_trans2) of (Nothing, Nothing) -> mzero _ -> @@ -3069,7 +3074,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl top_ptrans <- getTopPermM tp_trans <- translateClosed tp sigmaElimTransM "x_elimEx" tp_trans - (flip inExtTransM $ translate $ mbCombine p) + (flip inExtTransM $ translate $ mbCombine RL.typeCtxProxies p) compReturnTypeTransM (\etrans ptrans -> inExtTransM etrans $ @@ -3098,7 +3103,7 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl let etrans_y = case etrans_x of ETrans_Struct flds -> RL.get (mbLift memb) flds _ -> error "translatePermImpl1: Impl1_ElimStructField" - let mb_y = mbCombine $ fmap (const $ nu $ \y -> PExpr_Var y) x + let mb_y = mbCombine RL.typeCtxProxies $ fmap (const $ nu $ \y -> PExpr_Var y) x inExtTransM etrans_y $ withPermStackM (:>: Member_Base) (\(pctx :>: PTrans_Conj [APTrans_Struct pctx_str]) -> @@ -3116,12 +3121,12 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl unPTransLLVMField "translatePermImpl1: Impl1_ElimLLVMFieldContents" knownNat ptrans_x in pctx :>: PTrans_Conj [APTrans_LLVMField - (mbCombine $ + (mbCombine RL.typeCtxProxies $ fmap (\fld -> nu $ \y -> fld { llvmFieldContents = ValPerm_Eq (PExpr_Var y)}) mb_fld) $ - PTrans_Eq (mbCombine $ + PTrans_Eq (mbCombine RL.typeCtxProxies $ fmap (const $ nu PExpr_Var) mb_fld)] :>: ptrans') m @@ -3177,8 +3182,8 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl -- implTransAltErr, not the entire type-checking error message, because this is -- considered just an assertion and not a failure ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_Eq e1 e2) prop_str |], - [nuMP| MbPermImpls_Cons _ mb_impl' |]) -> - translatePermImpl prx (mbCombine mb_impl') >>= \trans -> + [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) -> + translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans -> return $ \k -> do prop_tp_trans <- translate prop applyMultiTransM (return $ globalOpenTerm "Prelude.maybe") @@ -3193,8 +3198,8 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl -- For an inequality test, we don't need a proof, so just insert an if ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_Neq e1 e2) prop_str |], - [nuMP| MbPermImpls_Cons _ mb_impl' |]) -> - translatePermImpl prx (mbCombine mb_impl') >>= \trans -> + [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) -> + translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans -> return $ \k -> let w = natVal2 prop in applyMultiTransM (return $ globalOpenTerm "Prelude.ite") @@ -3218,8 +3223,8 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl -} ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULt e1 e2) prop_str |], - [nuMP| MbPermImpls_Cons _ mb_impl' |]) -> - translatePermImpl prx (mbCombine mb_impl') >>= \trans -> + [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) -> + translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans -> return $ \k -> do prop_tp_trans <- translate prop applyMultiTransM (return $ globalOpenTerm "Prelude.maybe") @@ -3245,8 +3250,8 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl -} ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq e1 e2) prop_str |], - [nuMP| MbPermImpls_Cons _ mb_impl' |]) -> - translatePermImpl prx (mbCombine mb_impl') >>= \trans -> + [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) -> + translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans -> return $ \k -> do prop_tp_trans <- translate prop applyMultiTransM (return $ globalOpenTerm "Prelude.maybe") @@ -3262,8 +3267,8 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl ([nuMP| Impl1_TryProveBVProp x prop@(BVProp_ULeq_Diff e1 e2 e3) prop_str |], - [nuMP| MbPermImpls_Cons _ mb_impl' |]) -> - translatePermImpl prx (mbCombine mb_impl') >>= \trans -> + [nuMP| MbPermImpls_Cons _ _ mb_impl' |]) -> + translatePermImpl prx (mbCombine RL.typeCtxProxies mb_impl') >>= \trans -> return $ \k -> do prop_tp_trans <- translate prop applyMultiTransM (return $ globalOpenTerm "Prelude.maybe") @@ -3724,7 +3729,8 @@ translateStmt loc mb_stmt m = case mbMatch mb_stmt of PTrans_Conj [APTrans_Fun _ f_trm] -> f_trm _ -> error "translateStmt: TypedCall: unexpected function permission" -- let perms_in = fmap (distPermsSnoc . typedStmtIn) stmt - let perms_out = mbCombine $ fmap (\stmt' -> nu $ \ret -> + let perms_out = mbCombine RL.typeCtxProxies + $ fmap (\stmt' -> nu $ \ret -> typedStmtOut stmt' (MNil :>: ret)) stmt ret_tp <- translate $ fmap funPermRet fun_perm ectx_gexprs <- translate gexprs @@ -3811,11 +3817,11 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of (knownNat @sz) p_ptr in RL.append (pctx :>: PTrans_Conj [APTrans_LLVMField - (mbCombine $ + (mbCombine RL.typeCtxProxies $ fmap (\fp -> nu $ \ret -> fp { llvmFieldContents = ValPerm_Eq (PExpr_Var ret)}) mb_fp) - (PTrans_Eq $ mbCombine $ + (PTrans_Eq $ mbCombine RL.typeCtxProxies $ fmap (const $ nu $ \ret -> PExpr_Var ret) mb_fp)] :>: p_ret) pctx_l) m @@ -3887,7 +3893,7 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of inExtTransM ETrans_LLVM $ do b <- translate1 $ extMb mb_r1 tptrans <- - translate $ mbCombine $ flip fmap mb_stmt $ \stmt -> nu $ \ret -> + translate $ mbCombine RL.typeCtxProxies $ flip fmap mb_stmt $ \stmt -> nu $ \ret -> distPermsHeadPerm $ typedLLVMStmtOut stmt ret let t = applyOpenTerm (globalOpenTerm "Prelude.boolToEither") b withPermStackM (:>: Member_Base) (:>: typeTransF tptrans [t]) m @@ -3911,7 +3917,7 @@ instance PermCheckExtC ext => ret_tp <- returnTypeM sigma_trm <- sigmaTransM "r" tp_trans (flip inExtTransM $ - translate $ mbCombine mb_perms) + translate $ mbCombine RL.typeCtxProxies mb_perms) r_trans (itiPermStack <$> ask) return $ applyOpenTermMulti (globalOpenTerm "Prelude.returnM") @@ -3942,8 +3948,8 @@ instance PermCheckExtC ext => (TypedStmtSeq ext blocks tops ret ps) OpenTerm where translate mb_x = case mbMatch mb_x of [nuMP| TypedImplStmt impl_seq |] -> translate impl_seq - [nuMP| TypedConsStmt loc stmt mb_seq |] -> - translateStmt (mbLift loc) stmt (translate $ mbCombine mb_seq) + [nuMP| TypedConsStmt loc stmt pxys mb_seq |] -> + translateStmt (mbLift loc) stmt (translate $ mbCombine (mbLift pxys) mb_seq) [nuMP| TypedTermStmt _ term_stmt |] -> translate term_stmt instance PermCheckExtC ext => @@ -4126,7 +4132,7 @@ translateCFG env (cfg :: TypedCFG ext blocks ghosts inits ret) = all_pctx = RL.append pctx inits_eq_perms in impTransM all_membs all_pctx mapTrans retTypeTrans $ translateCallEntryID "CFG" (tpcfgEntryBlockID cfg) Proxy - (nuMulti all_pctx $ \_ -> PExprs_Nil) + (nuMulti (RL.map (\_-> Proxy) all_pctx) $ \_ -> PExprs_Nil) (mbValuePermsToDistPerms $ funPermToBlockInputs fun_perm) ) ] @@ -4293,7 +4299,7 @@ translateCompleteTypeInCtx :: SharedContext -> PermEnv -> translateCompleteTypeInCtx sc env args ret = completeOpenTerm sc $ runNilTypeTransM (piExprCtx args (typeTransType1 <$> translate ret')) env - where ret' = mbCombine . emptyMb $ ret + where ret' = mbCombine (cruCtxProxies args) . emptyMb $ ret -- | Translate an input list of 'ValuePerms' and an output 'ValuePerm' to a SAW -- core function type in a manner similar to 'translateCompleteFunPerm', except @@ -4307,5 +4313,6 @@ translateCompletePureFun sc env ctx args ret = completeOpenTerm sc $ runNilTypeTransM (piExprCtx ctx $ piPermCtx args' $ const $ typeTransTupleType <$> translate ret') env - where args' = mbCombine . emptyMb $ args - ret' = mbCombine . emptyMb $ ret + where args' = mbCombine pxys . emptyMb $ args + ret' = mbCombine pxys . emptyMb $ ret + pxys = cruCtxProxies ctx diff --git a/src/Verifier/SAW/Heapster/TypedCrucible.hs b/src/Verifier/SAW/Heapster/TypedCrucible.hs index 806e3b7..607d92b 100644 --- a/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -31,6 +31,7 @@ import qualified Data.Text as Text import Data.List (findIndex) import Data.Type.Equality import Data.Kind +import Data.Reflection import qualified Data.BitVector.Sized as BV import GHC.TypeLits @@ -601,6 +602,7 @@ data TypedStmtSeq ext blocks tops ret ps_in where -- value(s) of each statement TypedConsStmt :: !ProgramLoc -> !(TypedStmt ext rets ps_in ps_next) -> + !(RAssign Proxy rets) -> !(Mb rets (TypedStmtSeq ext blocks tops ret ps_next)) -> TypedStmtSeq ext blocks tops ret ps_in @@ -862,11 +864,12 @@ instance (PermCheckExtC ext, SubstVar PermVarSubst m) => genSubst s mb_x = case mbMatch mb_x of [nuMP| TypedImplStmt impl_seq |] -> TypedImplStmt <$> genSubst s impl_seq - [nuMP| TypedConsStmt loc stmt mb_seq |] -> - TypedConsStmt (mbLift loc) <$> genSubst s stmt <*> genSubst s mb_seq + [nuMP| TypedConsStmt loc stmt pxys mb_seq |] -> + TypedConsStmt (mbLift loc) <$> genSubst s stmt <*> pure (mbLift pxys) <*> give (mbLift pxys) (genSubst s mb_seq) [nuMP| TypedTermStmt loc term_stmt |] -> TypedTermStmt (mbLift loc) <$> genSubst s term_stmt + instance (PermCheckExtC ext, SubstVar PermVarSubst m) => Substable1 PermVarSubst (TypedStmtSeq ext blocks tops ret) m where genSubst1 = genSubst @@ -2074,7 +2077,7 @@ emitStmt :: CruCtx rets -> ProgramLoc -> (RAssign Name rets) emitStmt tps loc stmt = gopenBinding - ((TypedConsStmt loc stmt <$>) . strongMbM) + ((TypedConsStmt loc stmt (cruCtxProxies tps) <$>) . strongMbM) (mbPure (cruCtxProxies tps) ()) >>>= \(ns, ()) -> setVarTypes "x" ns tps >>> gmodify (modifySTCurPerms $ applyTypedStmt stmt ns) >>> @@ -3117,6 +3120,7 @@ tcJumpTarget ctx (JumpTarget blkID args_tps args) = let ghosts = entryGhosts entryID ghosts_prxs = cruCtxProxies ghosts ex_perms = + give ghosts_prxs $ varSubst (permVarSubstOfNames tops_args_ns) $ mbSeparate ghosts_prxs $ mbValuePermsToDistPerms entry_perms_in in @@ -3337,7 +3341,7 @@ tcBlockEntry in_deg blk (BlockEntryInfo {..}) = let args_prxs = cruCtxProxies entryInfoArgs ghosts_prxs = cruCtxProxies $ entryGhosts entryInfoID ret_perms = - mbCombine $ extMbMulti ghosts_prxs $ extMbMulti args_prxs $ + mbCombine RL.typeCtxProxies $ extMbMulti ghosts_prxs $ extMbMulti args_prxs $ mbSeparate (MNil :>: Proxy) stRetPerms in fmap (TypedEntry entryInfoID (addInDegrees in_deg entryInfoInDegree) stTopCtx entryInfoArgs stRetType entryInfoPermsIn ret_perms) $