diff --git a/heapster-saw/examples/rust_data.saw b/heapster-saw/examples/rust_data.saw index 6066848b6a..5f8e1c0a17 100644 --- a/heapster-saw/examples/rust_data.saw +++ b/heapster-saw/examples/rust_data.saw @@ -309,8 +309,8 @@ heapster_assume_fun_rename_prim env hashmap_u64_u64_insert_sym "hashmap_u64_u64_ // String::deref string_deref <- heapster_find_trait_method_symbol env "core::ops::deref::Deref::deref"; -//heapster_assume_fun_rename_prim env string_deref "string_deref" -// "<'a> fn (&'a String) -> &'a str"; +heapster_assume_fun_rename_prim env string_deref "string_deref" + "<'a> fn (&'a String) -> &'a str"; // String::fmt string_fmt <- heapster_find_trait_method_symbol env diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index a939725d19..594b91f78d 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -532,8 +532,8 @@ data SimplImpl ps_in ps_out where -- > x:eq(handle) -o x:fun_perm SImpl_ConstFunPerm :: args ~ CtxToRList cargs => - ExprVar (FunctionHandleType cargs ret) -> - FnHandle cargs ret -> FunPerm ghosts (CtxToRList cargs) ret -> Ident -> + ExprVar (FunctionHandleType cargs ret) -> FnHandle cargs ret -> + FunPerm ghosts (CtxToRList cargs) gouts ret -> Ident -> SimplImpl (RNil :> FunctionHandleType cargs ret) (RNil :> FunctionHandleType cargs ret) @@ -7397,7 +7397,7 @@ proveVarAtomicImpl x ps mb_p = case mbMatch mb_p of foldr (\(i::Int,p) rest -> case p of Perm_Fun fun_perm - | Just (Refl,Refl,Refl) <- funPermEq3 fun_perm fun_perm' -> + | Just (Refl,Refl,Refl,Refl) <- funPermEq4 fun_perm fun_perm' -> implCopyConjM x ps i >>> implPopM x (ValPerm_Conj ps) _ -> rest) (proveVarAtomicImplUnfoldOrFail x ps mb_p) @@ -7712,8 +7712,8 @@ proveVarImplH x p mb_p = case (p, mbMatch mb_p) of use implStatePermEnv >>>= \env -> case lookupFunPerm env f of Just (SomeFunPerm fun_perm, ident) - | [nuMP| Just (Refl,Refl,Refl) |] <- - mbMatch $ fmap (funPermEq3 fun_perm) mb_fun_perm -> + | [nuMP| Just (Refl,Refl,Refl, Refl) |] <- + mbMatch $ fmap (funPermEq4 fun_perm) mb_fun_perm -> introEqCopyM x (PExpr_Fun f) >>> implPopM x p >>> implSimplM Proxy (SImpl_ConstFunPerm x f fun_perm ident) @@ -7820,7 +7820,7 @@ distPermsToExDistPerms = emptyMb -- | Substitute arguments into a function permission to get the existentially -- quantified input permissions needed on the arguments -funPermExDistIns :: FunPerm ghosts args ret -> RAssign Name args -> +funPermExDistIns :: FunPerm ghosts args gouts ret -> RAssign Name args -> ExDistPerms ghosts (ghosts :++: args) funPermExDistIns fun_perm args = fmap (varSubst (permVarSubstOfNames args)) $ mbSeparate args $ @@ -8072,6 +8072,16 @@ proveVarsImpl ps | Refl <- mbLift (fmap RL.prependRNilEq $ mbDistPermsToValuePerms ps) = proveVarsImplAppend ps +-- | Prove a list of existentially-quantified distinguished permissions and put +-- those proofs onto the stack, and then return the expressions assigned to the +-- existential variables +proveVarsImplEVarExprs :: NuMatchingAny1 r => ExDistPerms vars as -> + ImplM vars s r as RNil (PermExprs vars) +proveVarsImplEVarExprs ps = + proveVarsImpl ps >>> + use implStateVars >>>= \vars -> + fmap (exprsOfSubst . completePSubst vars) getPSubst + -- | Prove a list of existentially-quantified permissions and put the proofs on -- the stack, similarly to 'proveVarsImpl', but ensure that the existential -- variables are themselves only instanitated with variables, not arbitrary diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y index b9b6d57cb5..dd56cb132f 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Parser.y +++ b/heapster-saw/src/Verifier/SAW/Heapster/Parser.y @@ -205,7 +205,9 @@ permOffset :: { Maybe AstExpr } funPerm :: { AstFunPerm } : '(' ctx ')' '.' funPermList '-o' funPermList - { AstFunPerm (pos $6) $2 $5 $7 } + { AstFunPerm (pos $6) $2 $5 [] $7 } + | '(' ctx ')' '.' funPermList '-o' '(' ctx ')' '.' funPermList + { AstFunPerm (pos $6) $2 $5 $8 $11 } funPermList :: { [(Located String, AstExpr)] } : 'empty' { [] } diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 6c63b4b2e4..40eea5033e 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -97,6 +97,15 @@ import Debug.Trace -- * Utility Functions and Definitions ---------------------------------------------------------------------- +-- | Call 'RL.split' twice to split a nested appended 'RAssign' into three +rlSplit3 :: prx1 ctx1 -> RAssign prx2 ctx2 -> RAssign prx3 ctx3 -> + RAssign f ((ctx1 :++: ctx2) :++: ctx3) -> + (RAssign f ctx1, RAssign f ctx2, RAssign f ctx3) +rlSplit3 (ctx1 :: prx1 ctx1) (ctx2 :: RAssign prx2 ctx2) ctx3 fs123 = + let (fs12, fs3) = RL.split (Proxy :: Proxy (ctx1 :++: ctx2)) ctx3 fs123 in + let (fs1, fs2) = RL.split ctx1 ctx2 fs12 in + (fs1, fs2, fs3) + -- | Take the ceiling of a division ceil_div :: Integral a => a -> a -> a ceil_div a b = (a + b - fromInteger 1) `div` b @@ -1653,7 +1662,7 @@ data AtomicPerm (a :: CrucibleType) where AtomicPerm (StructType ctx) -- | A function permission - Perm_Fun :: FunPerm ghosts (CtxToRList cargs) ret -> + Perm_Fun :: FunPerm ghosts (CtxToRList cargs) gouts ret -> AtomicPerm (FunctionHandleType cargs ret) -- | An LLVM permission that asserts a proposition about bitvectors @@ -2104,8 +2113,8 @@ lownedPermExprAndPerm (LOwnedPermBlock e bp) = -- | Convert an 'LOwnedPerm' to a variable plus permission, if possible lownedPermVarAndPerm :: LOwnedPerm a -> Maybe (VarAndPerm a) lownedPermVarAndPerm lop - | ExprAndPerm (PExpr_Var x) p <- lownedPermExprAndPerm lop = - Just $ VarAndPerm x p + | Just (x, off) <- asVarOffset (lownedPermExpr lop) = + Just $ VarAndPerm x (offsetPerm off $ lownedPermPerm lop) lownedPermVarAndPerm _ = Nothing -- | Convert an expression plus permission to an 'LOwnedPerm', if possible @@ -2181,43 +2190,52 @@ lownedPermsOffsetsForLLVMVar x (lops :>: _) = lownedPermsOffsetsForLLVMVar x lops -- | A function permission is a set of input and output permissions inside a --- context of ghost variables -data FunPerm ghosts args ret where - FunPerm :: CruCtx ghosts -> CruCtx args -> TypeRepr ret -> +-- 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 :> ret) -> - FunPerm ghosts args ret + MbValuePerms ((ghosts :++: args) :++: gouts :> ret) -> + FunPerm ghosts args gouts ret -- | Extract the @args@ context from a function permission -funPermArgs :: FunPerm ghosts args ret -> CruCtx args -funPermArgs (FunPerm _ args _ _ _) = args +funPermArgs :: FunPerm ghosts args gouts ret -> CruCtx args +funPermArgs (FunPerm _ args _ _ _ _) = args -- | Extract the @ghosts@ context from a function permission -funPermGhosts :: FunPerm ghosts args ret -> CruCtx ghosts -funPermGhosts (FunPerm ghosts _ _ _ _) = ghosts +funPermGhosts :: FunPerm ghosts args gouts ret -> CruCtx ghosts +funPermGhosts (FunPerm ghosts _ _ _ _ _) = ghosts -- | Extract the @ghosts@ and @args@ contexts from a function permission -funPermTops :: FunPerm ghosts args ret -> CruCtx (ghosts :++: args) +funPermTops :: FunPerm ghosts args gouts ret -> CruCtx (ghosts :++: args) funPermTops fun_perm = appendCruCtx (funPermGhosts fun_perm) (funPermArgs fun_perm) -- | Extract the return type from a function permission -funPermRet :: FunPerm ghosts args ret -> TypeRepr ret -funPermRet (FunPerm _ _ ret _ _) = ret +funPermRet :: FunPerm ghosts args gouts ret -> TypeRepr ret +funPermRet (FunPerm _ _ _ ret _ _) = ret + +-- | Extract the return types including ghosts from a function permission +funPermRets :: FunPerm ghosts args gouts ret -> CruCtx (gouts :> ret) +funPermRets fun_perm = CruCtxCons (funPermGouts fun_perm) (funPermRet fun_perm) + +-- | Extract the @gouts@ context from a function permission +funPermGouts :: FunPerm ghosts args gouts ret -> CruCtx gouts +funPermGouts (FunPerm _ _ gouts _ _ _) = gouts -- | Extract the input permissions of a function permission -funPermIns :: FunPerm ghosts args ret -> MbValuePerms (ghosts :++: args) -funPermIns (FunPerm _ _ _ perms_in _) = perms_in +funPermIns :: FunPerm ghosts args gouts ret -> MbValuePerms (ghosts :++: args) +funPermIns (FunPerm _ _ _ _ perms_in _) = perms_in -- | Extract the output permissions of a function permission -funPermOuts :: FunPerm ghosts args ret -> - MbValuePerms (ghosts :++: args :> ret) -funPermOuts (FunPerm _ _ _ _ perms_out) = perms_out +funPermOuts :: FunPerm ghosts args gouts ret -> + MbValuePerms ((ghosts :++: args) :++: gouts :> ret) +funPermOuts (FunPerm _ _ _ _ _ perms_out) = perms_out --- | A function permission that existentially quantifies the @ghosts@ types +-- | A function permission that existentially quantifies the ghost types data SomeFunPerm args ret where - SomeFunPerm :: FunPerm ghosts args ret -> SomeFunPerm args ret + SomeFunPerm :: FunPerm ghosts args gouts ret -> SomeFunPerm args ret -- | The different sorts of name, each of which comes with a 'Bool' flag @@ -2967,7 +2985,7 @@ instance Eq (AtomicPerm a) where (Perm_Struct ps1) == (Perm_Struct ps2) = ps1 == ps2 (Perm_Struct _) == _ = False (Perm_Fun fperm1) == (Perm_Fun fperm2) - | Just Refl <- funPermEq fperm1 fperm2 = True + | Just (Refl, Refl) <- funPermEq fperm1 fperm2 = True (Perm_Fun _) == _ = False (Perm_NamedConj n1 args1 off1) == (Perm_NamedConj n2 args2 off2) | Just (Refl, Refl, Refl) <- testNamedPermNameEq n1 n2 = @@ -2987,28 +3005,33 @@ instance Eq (ValuePerms as) where -} -- | Test if function permissions with different ghost argument lists are equal -funPermEq :: FunPerm ghosts1 args ret -> FunPerm ghosts2 args ret -> - Maybe (ghosts1 :~: ghosts2) -funPermEq (FunPerm ghosts1 _ _ perms_in1 perms_out1) - (FunPerm ghosts2 _ _ perms_in2 perms_out2) +funPermEq :: FunPerm ghosts1 args gouts1 ret -> + FunPerm ghosts2 args gouts2 ret -> + Maybe (ghosts1 :~: ghosts2, gouts1 :~: gouts2) +funPermEq (FunPerm ghosts1 _ gouts1 _ perms_in1 perms_out1) + (FunPerm ghosts2 _ gouts2 _ perms_in2 perms_out2) | Just Refl <- testEquality ghosts1 ghosts2 + , Just Refl <- testEquality gouts1 gouts2 , perms_in1 == perms_in2 && perms_out1 == perms_out2 - = Just Refl + = Just (Refl, Refl) funPermEq _ _ = Nothing --- | Test if function permissions with all 3 type args different are equal -funPermEq3 :: FunPerm ghosts1 args1 ret1 -> FunPerm ghosts2 args2 ret2 -> - Maybe (ghosts1 :~: ghosts2, args1 :~: args2, ret1 :~: ret2) -funPermEq3 (FunPerm ghosts1 args1 ret1 perms_in1 perms_out1) - (FunPerm ghosts2 args2 ret2 perms_in2 perms_out2) +-- | Test if function permissions with all 4 type args different are equal +funPermEq4 :: FunPerm ghosts1 args1 gouts1 ret1 -> + FunPerm ghosts2 args2 gouts2 ret2 -> + Maybe (ghosts1 :~: ghosts2, args1 :~: args2, + gouts1 :~: gouts2, ret1 :~: ret2) +funPermEq4 (FunPerm ghosts1 args1 ret1 gouts1 perms_in1 perms_out1) + (FunPerm ghosts2 args2 ret2 gouts2 perms_in2 perms_out2) | Just Refl <- testEquality ghosts1 ghosts2 , Just Refl <- testEquality args1 args2 + , Just Refl <- testEquality gouts1 gouts2 , Just Refl <- testEquality ret1 ret2 , perms_in1 == perms_in2 && perms_out1 == perms_out2 - = Just (Refl, Refl, Refl) -funPermEq3 _ _ = Nothing + = Just (Refl, Refl, Refl, Refl) +funPermEq4 _ _ = Nothing -instance Eq (FunPerm ghosts args ret) where +instance Eq (FunPerm ghosts args gouts ret) where fperm1 == fperm2 = isJust (funPermEq fperm1 fperm2) instance PermPretty (NamedPermName ns args a) where @@ -3145,24 +3168,32 @@ instance PermPretty (LOwnedPerm a) where instance PermPrettyF LOwnedPerm where permPrettyMF = permPrettyM -instance PermPretty (FunPerm ghosts args ret) where - permPrettyM (FunPerm ghosts args _ mb_ps_in mb_ps_out) = - let dps_in = extMb $ mbValuePermsToDistPerms mb_ps_in - dps_out = mbValuePermsToDistPerms mb_ps_out - dps = mbMap2 (,) dps_in dps_out in +instance PermPretty (FunPerm ghosts args gouts ret) where + permPrettyM (FunPerm ghosts args gouts _ mb_ps_in mb_ps_out) = fmap mbLift $ strongMbM $ - flip nuMultiWithElim1 dps $ \(ghosts_args_ns :>: ret_n) (ps_in, ps_out) -> - let (ghosts_ns, args_ns) = - RL.split Proxy (cruCtxProxies args) ghosts_args_ns in + flip nuMultiWithElim1 (mbValuePermsToDistPerms mb_ps_out) $ + \(ghosts_args_gouts_ns :>: ret_n) ps_out -> + let (ghosts_ns, args_ns, gouts_ns) = + rlSplit3 (cruCtxProxies ghosts) (cruCtxProxies args) + (cruCtxProxies gouts) ghosts_args_gouts_ns in + let ps_in = + varSubst (permVarSubstOfNames $ RL.append ghosts_ns args_ns) + (mbValuePermsToDistPerms mb_ps_in) in local (ppInfoAddExprName "ret" ret_n) $ local (ppInfoAddExprNames "arg" args_ns) $ local (ppInfoAddTypedExprNames ghosts ghosts_ns) $ + local (ppInfoAddTypedExprNames gouts gouts_ns) $ do pp_ps_in <- permPrettyM ps_in pp_ps_out <- permPrettyM ps_out pp_ghosts <- permPrettyM (RL.map2 VarAndType ghosts_ns $ cruCtxToTypes ghosts) + pp_gouts <- case gouts of + CruCtxNil -> return mempty + _ -> parens <$> permPrettyM (RL.map2 VarAndType gouts_ns $ + cruCtxToTypes gouts) return $ align $ - sep [parens pp_ghosts <> dot, pp_ps_in, pretty "-o", pp_ps_out] + sep [parens pp_ghosts <> dot, pp_ps_in, pretty "-o", + pp_gouts <> pp_ps_out] instance PermPretty (BVRange w) where permPrettyM (BVRange e1 e2) = @@ -3393,7 +3424,8 @@ tryAppendStructPerms _ _ _ _ = mzero -- | Helper function to build a 'Perm_LLVMFunPtr' from a 'FunPerm' -mkPermLLVMFunPtr :: (1 <= w, KnownNat w) => f w -> FunPerm ghosts args ret -> +mkPermLLVMFunPtr :: (1 <= w, KnownNat w) => f w -> + FunPerm ghosts args gouts ret -> AtomicPerm (LLVMPointerType w) mkPermLLVMFunPtr (_w :: f w) fun_perm = case cruCtxToReprEq (funPermArgs fun_perm) of @@ -5141,9 +5173,7 @@ lownedPermsToDistPerms (lops :>: lop) = -- | Convert the expressions of an 'LOwnedPerms' to variables, if possible lownedPermsVars :: LOwnedPerms ps -> Maybe (RAssign Name ps) -lownedPermsVars MNil = Just MNil -lownedPermsVars (lops :>: lop) = - (:>:) <$> lownedPermsVars lops <*> lownedPermVar lop +lownedPermsVars = fmap distPermsVars . lownedPermsToDistPerms -- | Test if an 'LOwnedPerm' could help prove any of a list of permissions lownedPermCouldProve :: LOwnedPerm a -> DistPerms ps -> Bool @@ -5170,26 +5200,33 @@ lownedPermsCouldProve lops ps = RL.foldr (\lop rest -> lownedPermCouldProve lop ps || rest) False lops +{- -- | Convert a 'FunPerm' in a name-binding to a 'FunPerm' that takes those bound -- names as additional ghost arguments with the supplied input permissions and -- no output permissions mbFunPerm :: CruCtx ctx -> Mb ctx (ValuePerms ctx) -> - Mb ctx (FunPerm ghosts args ret) -> - FunPerm (ctx :++: ghosts) args ret -mbFunPerm ctx mb_ps (mbMatch -> [nuMP| FunPerm mb_ghosts mb_args mb_ret ps_in ps_out |]) = + Mb ctx (FunPerm ghosts args gouts ret) -> + FunPerm (ctx :++: ghosts) args gouts ret +mbFunPerm ctx mb_ps (mbMatch -> + [nuMP| FunPerm mb_ghosts mb_args + mb_gouts mb_ret ps_in ps_out |]) = let ghosts = mbLift mb_ghosts args = mbLift mb_args ctx_perms = trueValuePerms $ cruCtxToTypes ctx - arg_types = cruCtxToTypes args - ghost_types = cruCtxToTypes ghosts - prxys = mapRAssign (const Proxy) (RL.append ghost_types arg_types) in + args_prxs = cruCtxProxies args + ghosts_prxs = cruCtxProxies ghosts + gouts_prxs = cruCtxProxies gouts + prxs_in = RL.append ghosts_prxs args_prxs + prxs_out = + RL.append ghosts_prxs $ RL.append args_prxs gouts_prxs :>: Proxy in case RL.appendAssoc ctx ghosts arg_types of Refl -> - FunPerm (appendCruCtx ctx ghosts) args (mbLift mb_ret) - (mbCombine prxys $ + FunPerm (appendCruCtx ctx ghosts) args (mbLift mb_gouts) (mbLift mb_ret) + (mbCombine prxs_in $ mbMap2 (\ps mb_ps_in -> fmap (RL.append ps) mb_ps_in) mb_ps ps_in) (fmap (RL.append ctx_perms) $ - mbCombine (prxys :>: Proxy) ps_out) + mbCombine prxs_out ps_out) +-} -- | Substitute ghost and regular arguments into a function permission to get -- its input permissions for those arguments, where ghost arguments are given @@ -5197,7 +5234,7 @@ mbFunPerm ctx mb_ps (mbMatch -> [nuMP| FunPerm mb_ghosts mb_args mb_ret ps_in ps -- For a 'FunPerm' of the form @(gctx). xs:ps -o xs:ps'@, return -- -- > [gs/gctx]xs : [gexprs/gctx]ps, g1:eq(gexpr1), ..., gm:eq(gexprm) -funPermDistIns :: FunPerm ghosts args ret -> RAssign Name ghosts -> +funPermDistIns :: FunPerm ghosts args gouts ret -> RAssign Name ghosts -> PermExprs ghosts -> RAssign Name args -> DistPerms ((ghosts :++: args) :++: ghosts) funPermDistIns fun_perm ghosts gexprs args = @@ -5213,12 +5250,15 @@ funPermDistIns fun_perm ghosts gexprs args = -- For a 'FunPerm' of the form @(gctx). xs:ps -o xs:ps'@, return -- -- > [gs/gctx]xs : [gexprs/gctx]ps' -funPermDistOuts :: FunPerm ghosts args ret -> RAssign Name ghosts -> - PermExprs ghosts -> RAssign Name (args :> ret) -> - DistPerms (ghosts :++: args :> ret) -funPermDistOuts fun_perm ghosts gexprs args_and_ret = - valuePermsToDistPerms (RL.append ghosts args_and_ret) $ - subst (appendSubsts (substOfExprs gexprs) (substOfVars args_and_ret)) $ +funPermDistOuts :: FunPerm ghosts args gouts ret -> RAssign Name ghosts -> + PermExprs ghosts -> RAssign Name args -> + RAssign Name (gouts :> ret) -> + DistPerms ((ghosts :++: args) :++: gouts :> ret) +funPermDistOuts fun_perm ghosts gexprs args gouts_ret = + valuePermsToDistPerms (RL.append (RL.append ghosts args) gouts_ret) $ + subst (appendSubsts + (appendSubsts (substOfExprs gexprs) (substOfVars args)) + (substOfVars gouts_ret)) $ funPermOuts fun_perm -- | Unfold a recursive permission given a 'RecPerm' for it @@ -5350,6 +5390,11 @@ instance FreeVars (ValuePerms tps) where freeVars ValPerms_Nil = NameSet.empty freeVars (ValPerms_Cons ps p) = NameSet.union (freeVars ps) (freeVars p) +instance FreeVars (DistPerms tps) where + freeVars dperms = + NameSet.unions $ + RL.mapToList (\(VarAndPerm x p) -> NameSet.insert x (freeVars p)) dperms + instance FreeVars (LLVMFieldPerm w sz) where freeVars (LLVMFieldPerm {..}) = NameSet.unions [freeVars llvmFieldRW, freeVars llvmFieldLifetime, @@ -5391,8 +5436,8 @@ instance FreeVars (LOwnedPerm a) where instance FreeVars (LOwnedPerms ps) where freeVars = NameSet.unions . RL.mapToList freeVars -instance FreeVars (FunPerm ghosts args ret) where - freeVars (FunPerm _ _ _ perms_in perms_out) = +instance FreeVars (FunPerm ghosts args gouts ret) where + freeVars (FunPerm _ _ _ _ perms_in perms_out) = NameSet.union (NameSet.liftNameSet $ fmap freeVars perms_in) (NameSet.liftNameSet $ fmap freeVars perms_out) @@ -5855,15 +5900,21 @@ instance SubstVar s m => Substable s (LOwnedPerm a) m where instance SubstVar s m => Substable1 s LOwnedPerm m where genSubst1 = genSubst -instance SubstVar s m => Substable s (FunPerm ghosts args ret) m where - genSubst s (mbMatch -> [nuMP| FunPerm ghosts args ret perms_in 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 s m => Substable s (FunPerm ghosts args gouts ret) m where + genSubst s (mbMatch -> + [nuMP| FunPerm mb_ghosts mb_args mb_gouts + mb_ret perms_in perms_out |]) = + let ghosts = mbLift mb_ghosts + args = mbLift mb_args + gouts = mbLift mb_gouts + ret = mbLift mb_ret + ghosts_args_prxs = + RL.append (cruCtxProxies ghosts) (cruCtxProxies args) + ghosts_args_gouts_ret_prxs = + RL.append ghosts_args_prxs (cruCtxProxies gouts) :>: Proxy in + FunPerm ghosts args gouts ret + <$> genSubstMb ghosts_args_prxs s perms_in + <*> genSubstMb ghosts_args_gouts_ret_prxs s perms_out instance SubstVar PermVarSubst m => Substable PermVarSubst (LifetimeCurrentPerms ps) m where @@ -5934,14 +5985,11 @@ substOfVars :: RAssign ExprVar ctx -> PermSubst ctx substOfVars = PermSubst . RL.map PExpr_Var substOfExprs :: PermExprs ctx -> PermSubst ctx -substOfExprs PExprs_Nil = PermSubst MNil -substOfExprs (PExprs_Cons es e) = consSubst (substOfExprs es) e +substOfExprs = PermSubst -- FIXME: Maybe PermSubst should just be PermExprs? exprsOfSubst :: PermSubst ctx -> PermExprs ctx -exprsOfSubst (PermSubst MNil) = PExprs_Nil -exprsOfSubst (PermSubst (es :>: e)) = - PExprs_Cons (exprsOfSubst $ PermSubst es) e +exprsOfSubst = unPermSubst substLookup :: PermSubst ctx -> Member ctx a -> PermExpr a substLookup (PermSubst m) memb = RL.get memb m @@ -6665,11 +6713,12 @@ instance AbstractVars (LOwnedPerms ps) where `clMbMbApplyM` abstractPEVars ns1 ns2 ps `clMbMbApplyM` abstractPEVars ns1 ns2 p -instance AbstractVars (FunPerm ghosts args ret) where - abstractPEVars ns1 ns2 (FunPerm ghosts args ret perms_in perms_out) = +instance AbstractVars (FunPerm ghosts args gouts ret) where + abstractPEVars ns1 ns2 (FunPerm ghosts args gouts ret perms_in perms_out) = absVarsReturnH ns1 ns2 ($(mkClosed [| FunPerm |]) - `clApply` toClosed ghosts `clApply` toClosed args `clApply` toClosed ret) + `clApply` toClosed ghosts `clApply` toClosed args + `clApply` toClosed gouts `clApply` toClosed ret) `clMbMbApplyM` abstractPEVars ns1 ns2 perms_in `clMbMbApplyM` abstractPEVars ns1 ns2 perms_out @@ -6880,10 +6929,10 @@ instance AbstractNamedShape w (ValuePerms as) where abstractNSM (ValPerms_Cons ps p) = mbMap2 ValPerms_Cons <$> abstractNSM ps <*> abstractNSM p -instance AbstractNamedShape w (FunPerm ghosts args ret) where - abstractNSM (FunPerm ghosts args ret perms_in perms_out) = - mbMap2 (FunPerm ghosts args ret) <$> abstractNSM perms_in - <*> abstractNSM perms_out +instance AbstractNamedShape w (FunPerm ghosts args gouts ret) where + abstractNSM (FunPerm ghosts args gouts ret perms_in perms_out) = + mbMap2 (FunPerm ghosts args gouts ret) <$> abstractNSM perms_in + <*> abstractNSM perms_out $(mkNuMatching [t| forall a . PermExpr a |]) @@ -6912,7 +6961,7 @@ $(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 ret. FunPerm ghosts args ret |]) +$(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 |]) @@ -6988,7 +7037,7 @@ instance Liftable (ReachMethods args a reach) where -- corresponding SAW identifier with a Crucible function handle data PermEnvFunEntry where PermEnvFunEntry :: args ~ CtxToRList cargs => FnHandle cargs ret -> - FunPerm ghosts args ret -> Ident -> + FunPerm ghosts args gouts ret -> Ident -> PermEnvFunEntry -- | An existentially quantified 'NamedPerm' @@ -7184,7 +7233,8 @@ permEnvAddOpaqueShape env nm args mb_len tp_id = -- | Add a global symbol with a function permission to a 'PermEnv' permEnvAddGlobalSymFun :: (1 <= w, KnownNat w) => PermEnv -> GlobalSymbol -> - f w -> FunPerm ghosts args ret -> OpenTerm -> PermEnv + f w -> FunPerm ghosts args gouts ret -> + OpenTerm -> PermEnv permEnvAddGlobalSymFun env sym (w :: f w) fun_perm t = let p = ValPerm_Conj1 $ mkPermLLVMFunPtr w fun_perm in env { permEnvGlobalSyms = diff --git a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs index bc77d6cdf8..71c6fedef2 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/RustTypes.hs @@ -24,6 +24,7 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +-- {-# OPTIONS_GHC -freduction-depth=0 #-} module Verifier.SAW.Heapster.RustTypes where @@ -68,9 +69,84 @@ import Verifier.SAW.Heapster.Permissions ---------------------------------------------------------------------- --- * Helper Definitions for Translation +-- * Helper Definitions ---------------------------------------------------------------------- +-- | A version of 'mbSeparate' that takes in an explicit phantom argument for +-- the first context +mbSeparatePrx :: prx1 ctx1 -> RAssign prx2 ctx2 -> Mb (ctx1 :++: ctx2) a -> + Mb ctx1 (Mb ctx2 a) +mbSeparatePrx _ = mbSeparate + +-- | Reassociate a binding list +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 | Refl <- RL.appendAssoc ctx1 ctx2 ctx3 = mb_a + +-- | Reassociate a binding list in the reverse direction of 'mbAssoc' +mbUnAssoc :: prx1 ctx1 -> RAssign prx2 ctx2 -> RAssign prx3 ctx3 -> + Mb ((ctx1 :++: ctx2) :++: ctx3) a -> + Mb (ctx1 :++: (ctx2 :++: ctx3)) a +mbUnAssoc ctx1 ctx2 ctx3 mb_a | Refl <- RL.appendAssoc ctx1 ctx2 ctx3 = mb_a + +-- | Prove type-level equality by reassociating four type lists +appendAssoc4 :: RAssign Proxy ctx1 -> RAssign Proxy ctx2 -> + RAssign Proxy ctx3 -> RAssign Proxy ctx4 -> + ctx1 :++: ((ctx2 :++: ctx3) :++: ctx4) :~: + ((ctx1 :++: ctx2) :++: ctx3) :++: ctx4 +appendAssoc4 ctx1 ctx2 ctx3 ctx4 + | Refl <- RL.appendAssoc ctx1 (RL.append ctx2 ctx3) ctx4 + , Refl <- RL.appendAssoc ctx1 ctx2 ctx3 + = Refl + +-- | Reassociate a binding list of four contexts +mbAssoc4 :: RAssign Proxy ctx1 -> RAssign Proxy ctx2 -> + RAssign Proxy ctx3 -> RAssign Proxy ctx4 -> + Mb (ctx1 :++: ((ctx2 :++: ctx3) :++: ctx4)) a -> + Mb (((ctx1 :++: ctx2) :++: ctx3) :++: ctx4) a +mbAssoc4 ctx1 ctx2 ctx3 ctx4 mb_a + | Refl <- appendAssoc4 ctx1 ctx2 ctx3 ctx4 = mb_a + +-- | Combine bindings lists using 'mbCombine' and reassociate them +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) + +-- | Combine bindings lists using 'mbCombine' and reassociate them +mbCombineAssoc4 :: + RAssign Proxy ctx1 -> RAssign Proxy ctx2 -> + RAssign Proxy ctx3 -> RAssign Proxy ctx4 -> + Mb ctx1 (Mb ((ctx2 :++: ctx3) :++: ctx4) a) -> + Mb (((ctx1 :++: ctx2) :++: ctx3) :++: ctx4) a +mbCombineAssoc4 ctx1 ctx2 ctx3 ctx4 mb_mb_a + | Refl <- appendAssoc4 ctx1 ctx2 ctx3 ctx4 + = mbCombine ((ctx2 `RL.append` ctx3) `RL.append` ctx4) mb_mb_a + +-- | Prepend and reassociate an 'RAssign' +assocAppend :: RAssign f ctx1 -> prx2 ctx2 -> RAssign prx3 ctx3 -> + RAssign f (ctx2 :++: ctx3) -> + RAssign f ((ctx1 :++: ctx2) :++: ctx3) +assocAppend fs1 ctx2 ctx3 fs23 = + let (fs2, fs3) = RL.split ctx2 ctx3 fs23 in + RL.append (RL.append fs1 fs2) fs3 + +-- | Prepend and reassociate an 'RAssign' to get one with four type contexts +assocAppend4 :: RAssign f ctx1 -> prx2 ctx2 -> RAssign prx3 ctx3 -> + RAssign prx4 ctx4 -> + RAssign f ((ctx2 :++: ctx3) :++: ctx4) -> + RAssign f (((ctx1 :++: ctx2) :++: ctx3) :++: ctx4) +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)) @@ -678,9 +754,10 @@ 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 +-- | 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 ret. Some3FunPerm (FunPerm ghosts args ret) + forall ghosts args gouts ret. Some3FunPerm (FunPerm ghosts args gouts ret) instance PermPretty Some3FunPerm where permPrettyM (Some3FunPerm fun_perm) = permPrettyM fun_perm @@ -734,7 +811,8 @@ funPerm3FromMbArgLayout ctx [nuMP| ALPerm mb_ps_in |] , ps_out_all <- RL.append ghost_perms (assignToRListAppend ctx1 ctx ps1_out $ trueValuePerms $ assignToRList ctx) :>: ret_perm = - return $ Some3FunPerm $ FunPerm ghosts ctx_args ret_tp mb_ps_in_all + return $ Some3FunPerm $ + FunPerm ghosts ctx_args CruCtxNil ret_tp mb_ps_in_all (nuMulti (cruCtxProxies ctx_all :>: Proxy) $ \_ -> ps_out_all) funPerm3FromMbArgLayout ctx [nuMP| ALPerm_Exists mb_p |] ghosts ctx1 ps1_in ps1_out ret_tp ret_perm = @@ -768,94 +846,43 @@ funPerm3FromArgLayoutNoArgs layout ret ret_perm = funPerm3FromArgLayout layout Ctx.empty MNil MNil ret ret_perm --- FIXME: should we save any of these? -{- --- | Extend a name binding by adding a name in the middle -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 (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 -> - RAssign f (ctx1 :++: ctx2) -> - RAssign f (ctx1 :++: ((RNil :> b) :++: ctx2)) -rassignInsertMiddle ctx1 ctx2 fb fs = - let (fs1, fs2) = RL.split ctx1 ctx2 fs in - RL.append fs1 (RL.append (MNil :>: fb) fs2) - --- | Prepend an argument with input and output perms to a 'Some3FunPerm' -funPerm3PrependArg :: TypeRepr arg -> ValuePerm arg -> ValuePerm arg -> - Some3FunPerm -> Some3FunPerm -funPerm3PrependArg arg_tp arg_in arg_out (Some3FunPerm - (FunPerm ghosts args ret - ps_in ps_out)) = - let args_prxs = cruCtxProxies args in - Some3FunPerm $ FunPerm ghosts (appendCruCtx (singletonCruCtx arg_tp) args) ret - (extMbMiddle ghosts args_prxs arg_tp $ - fmap (rassignInsertMiddle ghosts args_prxs arg_in) ps_in) - (extMbMiddle ghosts (args_prxs :>: Proxy) arg_tp $ - fmap (rassignInsertMiddle ghosts (args_prxs :>: Proxy) arg_out) ps_out) --} - -mbSeparatePrx :: prx1 ctx1 -> RAssign prx2 ctx2 -> Mb (ctx1 :++: ctx2) a -> - Mb ctx1 (Mb ctx2 a) -mbSeparatePrx _ = mbSeparate - -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 (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 -> - 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) -> - RAssign f ((ctx1 :++: ctx2) :++: ctx3) -assocAppend fs1 ctx2 ctx3 fs23 = - let (fs2, fs3) = RL.split ctx2 ctx3 fs23 in - RL.append (RL.append fs1 fs2) fs3 - --- | Add ghost variables for the bound names in a 'Some3FunPerm' in a binding -mbGhostsFunPerm3 :: CruCtx new_ghosts -> Mb new_ghosts Some3FunPerm -> - Some3FunPerm -mbGhostsFunPerm3 new_ghosts (mbMatch -> [nuMP| Some3FunPerm - (FunPerm ghosts args - ret ps_in ps_out) |]) = +-- | Add ghost variables with the supplied permissions for the bound names in a +-- 'FunPerm' in a binding +mbGhostsFunPerm :: + CruCtx new_ghosts -> + Mb ((new_ghosts :++: ghosts) :++: args) (ValuePerms new_ghosts) -> + Mb new_ghosts (FunPerm ghosts args gouts ret) -> + FunPerm (new_ghosts :++: ghosts) args gouts ret +mbGhostsFunPerm new_ghosts mb_new_ps (mbMatch -> + [nuMP| FunPerm ghosts args + gouts ret ps_in ps_out |]) = let new_prxs = cruCtxProxies new_ghosts ghosts_prxs = cruCtxProxies $ mbLift ghosts + rets_prxs = cruCtxProxies (mbLift gouts) :>: Proxy args_prxs = cruCtxProxies $ mbLift args in - Some3FunPerm $ FunPerm (appendCruCtx new_ghosts $ - 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 (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 (RL.append ghosts_prxs args_prxs :>: Proxy) ps_out) + FunPerm (appendCruCtx new_ghosts $ mbLift ghosts) + (mbLift args) (mbLift gouts) (mbLift ret) + (mbMap2 (\new_ps ps -> assocAppend new_ps ghosts_prxs args_prxs ps) mb_new_ps $ + mbAssoc new_prxs ghosts_prxs args_prxs $ + mbCombine (RL.append ghosts_prxs args_prxs) ps_in) + (mbAssoc4 new_prxs ghosts_prxs args_prxs rets_prxs $ + fmap (assocAppend4 (RL.map (const ValPerm_True) new_prxs) + ghosts_prxs args_prxs rets_prxs) $ + mbCombine (RL.append + (RL.append ghosts_prxs args_prxs) rets_prxs) ps_out) + +-- | Add ghost variables with no permissions for the bound names in a +-- 'Some3FunPerm' in a binding +mbGhostsFunPerm3 :: CruCtx new_ghosts -> Mb new_ghosts Some3FunPerm -> + Some3FunPerm +mbGhostsFunPerm3 new_ghosts (mbMatch -> [nuMP| Some3FunPerm fun_perm |]) = + let new_ps = + nuMulti (cruCtxProxies + ((new_ghosts + `appendCruCtx` mbLift (fmap funPermGhosts fun_perm)) + `appendCruCtx` mbLift (fmap funPermArgs fun_perm))) $ + const $ RL.map (const ValPerm_True) (cruCtxProxies new_ghosts) in + Some3FunPerm $ mbGhostsFunPerm new_ghosts new_ps fun_perm -- | Try to compute the layout of a structure of the given shape as a value, @@ -1098,6 +1125,13 @@ tyParamName (TyParam _ ident _ _ _) = name ident extMbOuter :: RAssign Proxy ctx1 -> Mb ctx2 a -> Mb (ctx1 :++: ctx2) a extMbOuter prxs mb_a = mbCombine (mbToProxy mb_a) $ nuMulti prxs $ const mb_a +extMbAppInner :: NuMatching a => any ctx1 -> + RAssign Proxy ctx2 -> RAssign Proxy ctx3 -> + Mb (ctx1 :++: ctx2) a -> Mb (ctx1 :++: ctx2 :++: ctx3) a +extMbAppInner (_ :: any ctx1) ctx2 ctx3 mb_a = + mbCombine (RL.append ctx2 ctx3) $ + mbMapCl ($(mkClosed [| extMbMulti |]) `clApply` toClosed ctx3) $ + mbSeparate @_ @ctx1 ctx2 mb_a -- | Add a lifetime described by a 'LifetimeDef' to a 'Some3FunPerm' mbLifetimeFunPerm :: LifetimeDef Span -> Binding LifetimeType Some3FunPerm -> @@ -1105,36 +1139,46 @@ mbLifetimeFunPerm :: LifetimeDef Span -> Binding LifetimeType Some3FunPerm -> mbLifetimeFunPerm (LifetimeDef _ _ [] _) (mbMatch -> [nuMP| Some3FunPerm fun_perm |]) = do let ghosts = mbLift $ fmap funPermGhosts fun_perm + let ghosts_prxs = cruCtxProxies ghosts + let gouts = mbLift $ fmap funPermGouts fun_perm + let rets_prxs = cruCtxProxies gouts :>: Proxy let args = mbLift $ fmap funPermArgs fun_perm let args_prxs = cruCtxProxies args let ret = mbLift $ fmap funPermRet fun_perm + let l_prxs = MNil :>: (Proxy :: Proxy LifetimeType) let mb_ps_in = - mbCombineAssoc (MNil :>: Proxy) (cruCtxProxies ghosts) args_prxs $ + mbCombineAssoc l_prxs ghosts_prxs args_prxs $ fmap (mbValuePermsToDistPerms . funPermIns) fun_perm let mb_ps_out = - mbCombineAssoc (MNil :>: Proxy) (cruCtxProxies ghosts) (args_prxs :>: Proxy) $ + mbCombineAssoc4 l_prxs ghosts_prxs args_prxs rets_prxs $ fmap (mbValuePermsToDistPerms . funPermOuts) fun_perm - let mb_l = - extMbMulti (cruCtxProxies args) $ - extMbMulti (cruCtxProxies ghosts) (nu id) + let mb_l = extMbMulti args_prxs $ extMbMulti ghosts_prxs $ nu id + let mb_l_out = + extMbMulti rets_prxs $ extMbMulti args_prxs $ + extMbMulti ghosts_prxs $ nu id [nuMP| Some mb_lops_in |] <- mbMatchM $ mbMap2 lownedPermsForLifetime mb_l mb_ps_in [nuMP| Some mb_lops_out |] <- - mbMatchM $ mbMap2 lownedPermsForLifetime (extMb mb_l) mb_ps_out + mbMatchM $ mbMap2 lownedPermsForLifetime mb_l_out mb_ps_out case abstractMbLOPsModalities mb_lops_in of SomeTypedMb ghosts' mb_mb_lops_in_abs -> return $ mbGhostsFunPerm3 ghosts' $ flip fmap mb_mb_lops_in_abs $ \mb_lops_in_abs -> - Some3FunPerm $ FunPerm (appendCruCtx - (singletonCruCtx LifetimeRepr) ghosts) args ret + Some3FunPerm $ + FunPerm (appendCruCtx + (singletonCruCtx LifetimeRepr) ghosts) args gouts ret (mbMap3 (\ps_in lops_in lops_in_abs -> assocAppend (MNil :>: ValPerm_LOwned [] lops_in lops_in_abs) ghosts args_prxs $ distPermsToValuePerms ps_in) mb_ps_in mb_lops_in mb_lops_in_abs) (mbMap3 (\ps_out lops_out lops_in_abs -> - assocAppend (MNil :>: ValPerm_LOwned [] lops_out lops_in_abs) - ghosts (args_prxs :>: Proxy) $ distPermsToValuePerms ps_out) - mb_ps_out mb_lops_out (extMb mb_lops_in_abs)) + let (ps_ghosts, ps_args, ps_rets) = + rlSplit3 ghosts_prxs args_prxs rets_prxs $ + distPermsToValuePerms ps_out in + (((MNil :>: ValPerm_LOwned [] lops_out lops_in_abs) + `RL.append` ps_ghosts) `RL.append` ps_args) + `RL.append` ps_rets) + mb_ps_out mb_lops_out (extMbMulti rets_prxs mb_lops_in_abs)) mbLifetimeFunPerm (LifetimeDef _ _ _bounds _) _ = fail "Rust lifetime bounds not yet supported!" @@ -1148,6 +1192,215 @@ withLifetimes (ldef : ldefs) m = LifetimeRepr) (withLifetimes ldefs m) >>= mbLifetimeFunPerm ldef +-- | An object of type @a@ inside some name-binding context where each bound +-- name is assigned its own permission +data SomeMbWithPerms a where + SomeMbWithPerms :: CruCtx ctx -> MbValuePerms ctx -> Mb ctx a -> + SomeMbWithPerms a + +instance Functor SomeMbWithPerms where + fmap f (SomeMbWithPerms ctx ps mb_a) = SomeMbWithPerms ctx ps (fmap f mb_a) + +instance Applicative SomeMbWithPerms where + pure a = SomeMbWithPerms CruCtxNil (emptyMb MNil) $ emptyMb a + liftA2 f (SomeMbWithPerms ctx1 mb_ps1 mb_a1) (SomeMbWithPerms ctx2 mb_ps2 mb_a2) = + SomeMbWithPerms (appendCruCtx ctx1 ctx2) + (mbCombine (cruCtxProxies ctx2) $ flip fmap mb_ps1 $ \ps1 -> + flip fmap mb_ps2 $ \ps2 -> RL.append ps1 ps2) + (mbCombine (cruCtxProxies ctx2) $ + flip fmap mb_a1 $ \a1 -> flip fmap mb_a2 $ \a2 -> f a1 a2) + +-- NOTE: the Monad instance fails here because it requires the output type of f +-- to satisfy NuMatching. That is, it is a "restricted monad", that is only a +-- monad over types that satisfy the NuMatching restriction. Thus we define +-- bindSomeMbWithPerms to add this restriction. +{- +instance Monad SomeMbWithPerms where + return = pure + (SomeMbWithPerms ctx1 mb_ps1 mb_a) >>= f = + case mbMatch (fmap f mb_a) of + [nuMP| SomeMbWithPerms ctx2 mb_mb_ps2 mb_mb_b |] -> + let ctx2_prxs = cruCtxProxies $ mbLift ctx2 in + SomeMbWithPerms (appendCruCtx ctx1 $ mbLift ctx2) + (mbCombine ctx2_prxs $ + mbMap2 (\ps1 mb_ps2 -> fmap (RL.append ps1) mb_ps2) mb_ps1 mb_mb_ps2) + (mbCombine ctx2_prxs mb_mb_b) +-} + +-- | A monadic bind for 'SomeMbWithPerms', which requires a 'NuMatching' +-- instance for the output type +bindSomeMbWithPerms :: NuMatching b => SomeMbWithPerms a -> + (a -> SomeMbWithPerms b) -> SomeMbWithPerms b +bindSomeMbWithPerms (SomeMbWithPerms ctx1 mb_ps1 mb_a) f = + case mbMatch (fmap f mb_a) of + [nuMP| SomeMbWithPerms ctx2 mb_mb_ps2 mb_mb_b |] -> + let ctx2_prxs = cruCtxProxies $ mbLift ctx2 in + SomeMbWithPerms (appendCruCtx ctx1 $ mbLift ctx2) + (mbCombine ctx2_prxs $ + mbMap2 (\ps1 mb_ps2 -> fmap (RL.append ps1) mb_ps2) mb_ps1 mb_mb_ps2) + (mbCombine ctx2_prxs mb_mb_b) + +-- | Make a 'SomeMbWithPerms' with a single bound variable +someMbWithPermsVar1 :: TypeRepr a -> ValuePerm a -> SomeMbWithPerms (ExprVar a) +someMbWithPermsVar1 tp p = + SomeMbWithPerms (singletonCruCtx tp) (nu $ const (MNil :>: p)) (nu id) + +-- | Move a 'SomeMbWithPerms' out of a binding by adding the bound variables as +-- variables that are bound with @true@ permissions by the 'SomeMbWithPerms' +mbSomeMbWithPerms :: NuMatching a => CruCtx ctx -> Mb ctx (SomeMbWithPerms a) -> + SomeMbWithPerms a +mbSomeMbWithPerms ctx (mbMatch -> [nuMP| SomeMbWithPerms ctx' mb_ps' mb_a |]) = + let ctx'_prxs = cruCtxProxies $ mbLift ctx' in + SomeMbWithPerms (appendCruCtx ctx $ mbLift ctx') + (fmap (RL.append $ trueValuePerms (cruCtxProxies ctx)) $ + mbCombine ctx'_prxs mb_ps') + (mbCombine ctx'_prxs mb_a) + +-- | Add additional gnost output variables to a 'FunPerm' +mbGoutsFunPerm :: + out_ctx ~ ((ghosts :++: args) :++: gouts :> ret) => + CruCtx ghosts -> CruCtx args -> CruCtx gouts -> TypeRepr ret -> + MbValuePerms (ghosts :++: args) -> CruCtx new_gouts -> + Mb new_gouts (Mb out_ctx (ValuePerms new_gouts)) -> + Mb new_gouts (Mb out_ctx (ValuePerms out_ctx)) -> + FunPerm ghosts args (gouts :++: new_gouts) ret +mbGoutsFunPerm ghosts args gouts ret ps_in gouts' mb_gps' mb_ps_out' + | ga_prxs <- cruCtxProxies $ appendCruCtx ghosts args + , gouts_prxs <- cruCtxProxies gouts + , gag_prxs <- RL.append ga_prxs gouts_prxs + , ret_prxs <- cruCtxProxies $ singletonCruCtx ret + , gouts'_prxs <- cruCtxProxies gouts' + , Refl <- RL.appendAssoc ga_prxs gouts_prxs gouts'_prxs = + FunPerm ghosts args (appendCruCtx gouts gouts') ret ps_in $ + mbCombine ret_prxs $ mbCombine gouts'_prxs $ + mbSwap gag_prxs $ fmap (mbSeparate ret_prxs) $ + mbMap2 + (mbMap2 + (\gps' ps_out' -> + let (ga_perms, gouts_perms, MNil :>: ret_perm) = + rlSplit3 ga_prxs gouts_prxs ret_prxs ps_out' in + RL.append ga_perms (RL.append gouts_perms gps') :>: ret_perm)) + mb_gps' mb_ps_out' + +-- | Find each subterm of the input that is a field, array, or block permission +-- with a different lifetime than the supplied one. Abstract out these +-- permissions by replacing each such permission @p@ with an @eq(x)@ permission +-- for a fresh variable @x@ which is itself assigned permission @p@. Only do +-- this abstraction, though, at locations where @x@ in the resulting permission +-- is a determined variable. When the supplied lifetime is omitted, i.e., is +-- 'Nothing', only perform this abstraction at strict subterms. +class AbstractVarsForLifetimes a where + abstractVarsForLifetimes :: Maybe (PermExpr LifetimeType) -> a -> + SomeMbWithPerms a + +instance AbstractVarsForLifetimes (ValuePerms ps) where + abstractVarsForLifetimes l = traverseRAssign (abstractVarsForLifetimes l) + +-- | Return the type of an atomic permission if we can compute it, specifically +-- if it is a field, array, or block permission +atomicPermType :: AtomicPerm a -> Maybe (TypeRepr a) +atomicPermType (Perm_LLVMField _) = Just knownRepr +atomicPermType (Perm_LLVMArray _) = Just knownRepr +atomicPermType (Perm_LLVMBlock _) = Just knownRepr +atomicPermType _ = Nothing + +instance AbstractVarsForLifetimes (ValuePerm a) where + abstractVarsForLifetimes (Just l) p@(ValPerm_Conj ps) + | any (/= l) (mapMaybe atomicPermLifetime ps) + , tp:_ <- mapMaybe atomicPermType ps = + bindSomeMbWithPerms (abstractVarsForLifetimes Nothing p) $ \p' -> + ValPerm_Eq <$> PExpr_Var <$> someMbWithPermsVar1 tp p' + abstractVarsForLifetimes l (ValPerm_Conj ps) = + ValPerm_Conj <$> traverse (abstractVarsForLifetimes l) ps + abstractVarsForLifetimes l (ValPerm_Exists mb_p) = + -- Any existentials also become abstracted variables, so they can be bound + -- as ghosts or gouts (depending on whether they occur in the input or + -- output permissions) + mbSomeMbWithPerms knownRepr $ fmap (abstractVarsForLifetimes l) mb_p + abstractVarsForLifetimes _ p = pure p + +-- NOTE: for AtomicPerms, we don't ever replace the permission itself, since we +-- don't want to replace each individual permission pi in a conjunction p1*..*pn +-- with an equality perm, but instead want to replace the entire conjunction all +-- at once. This is handled in the above case for ValPerm_Conj. +instance AbstractVarsForLifetimes (AtomicPerm a) where + abstractVarsForLifetimes _ (Perm_LLVMField fp) = + (\p -> Perm_LLVMField $ fp { llvmFieldContents = p }) <$> + abstractVarsForLifetimes (Just $ llvmFieldLifetime fp) (llvmFieldContents fp) + -- FIXME: we can't yet abstract array permissions, because shapes in arrays + -- could be repeated multiple times and thus we would have to somehow abstract + -- over multiple copies of the same variable for that to work... + abstractVarsForLifetimes _ (Perm_LLVMBlock bp) = + (\sh -> Perm_LLVMBlock $ bp { llvmBlockShape = sh }) <$> + abstractVarsForLifetimesSh (llvmBlockRW bp) (llvmBlockLifetime bp) + (llvmBlockShape bp) + abstractVarsForLifetimes _ (Perm_Struct ps) = + -- NOTE: for struct perms we want to abstract any permission with any + -- non-always lifetime, so we set l to always + Perm_Struct <$> + traverseRAssign (abstractVarsForLifetimes (Just PExpr_Always)) ps + abstractVarsForLifetimes _ p = pure p + +-- | Like 'abstractVarsForLifetimes' but for an LLVM shape inside a @memblock@ +-- with the given modalities +abstractVarsForLifetimesSh :: (1 <= w, KnownNat w) => PermExpr RWModalityType -> + PermExpr LifetimeType -> + PermExpr (LLVMShapeType w) -> + SomeMbWithPerms (PermExpr (LLVMShapeType w)) +abstractVarsForLifetimesSh _ l (PExpr_FieldShape (LLVMFieldShape p)) = + PExpr_FieldShape <$> LLVMFieldShape <$> abstractVarsForLifetimes (Just l) p +abstractVarsForLifetimesSh rw l (PExpr_PtrShape maybe_rw (Just l') sh) + | l /= l' + , rw' <- maybe rw id maybe_rw + , Just len <- llvmShapeLength sh = + -- NOTE: abstracting a shape should return one with the same length + bindSomeMbWithPerms (abstractVarsForLifetimesSh rw' l' sh) $ \sh' -> + PExpr_FieldShape <$> LLVMFieldShape <$> ValPerm_Eq <$> PExpr_Var <$> + someMbWithPermsVar1 knownRepr (ValPerm_LLVMBlock $ + LLVMBlockPerm rw' l' (bvInt 0) len sh') +abstractVarsForLifetimesSh rw l (PExpr_PtrShape maybe_rw maybe_l sh) = + let rw' = maybe rw id maybe_rw in + PExpr_PtrShape maybe_rw maybe_l <$> abstractVarsForLifetimesSh rw' l sh +abstractVarsForLifetimesSh rw l (PExpr_SeqShape sh1 sh2) = + PExpr_SeqShape <$> abstractVarsForLifetimesSh rw l sh1 <*> + abstractVarsForLifetimesSh rw l sh2 +abstractVarsForLifetimesSh rw l (PExpr_ExShape mb_sh) = + mbSomeMbWithPerms knownRepr $ fmap (abstractVarsForLifetimesSh rw l) mb_sh +abstractVarsForLifetimesSh _ _ sh = pure sh + +-- | A 'SomeMbWithPerms' in a binding +data MbSomeMbWithPerms ctx a where + MbSomeMbWithPerms :: CruCtx ctx' -> Mb ctx' (Mb ctx (ValuePerms ctx')) -> + Mb ctx' (Mb ctx a) -> + MbSomeMbWithPerms ctx a + +mbAbstractVarsForLifetimes :: Mb ctx (ValuePerms ps) -> + MbSomeMbWithPerms ctx (ValuePerms ps) +mbAbstractVarsForLifetimes mb_ps + | [nuMP| SomeMbWithPerms ctx' mb_ctx_ps' mb_ps' |] <- + mbMatch (fmap (abstractVarsForLifetimes Nothing) mb_ps) + , ctx'_prxs <- cruCtxProxies $ mbLift ctx' = + MbSomeMbWithPerms (mbLift ctx') (mbSwap ctx'_prxs mb_ctx_ps') + (mbSwap ctx'_prxs mb_ps') + +-- | For both the input and output permissions of a function permission, find +-- all permissions @p@ in with a lifetime that are contained inside a struct +-- permission or a field or block permission with a different lifetime, and +-- replace each such permission with an @eq(z)@ permission for a fresh ghost +-- variable @z@ that is itself assigned permissions @p@. +abstractFunVarsForLifetimes :: Some3FunPerm -> Some3FunPerm +abstractFunVarsForLifetimes (Some3FunPerm + (FunPerm ghosts args gouts ret ps_in ps_out)) + | MbSomeMbWithPerms ghosts' mb_gps' mb_ps_in' <- + mbAbstractVarsForLifetimes ps_in + , MbSomeMbWithPerms gouts' mb_gops' mb_ps_out' <- + mbAbstractVarsForLifetimes ps_out + , ghosts_prxs <- cruCtxProxies ghosts + , args_prxs <- cruCtxProxies args = + Some3FunPerm $ mbGhostsFunPerm ghosts' + (mbCombineAssoc ghosts' ghosts_prxs args_prxs mb_gps') $ + flip fmap mb_ps_in' $ \ps_in' -> + mbGoutsFunPerm ghosts args gouts ret ps_in' gouts' mb_gops' mb_ps_out' -- | Convert a monomorphic function type, i.e., one with no type arguments rsConvertMonoFun :: (1 <= w, KnownNat w) => prx w -> Span -> Abi -> @@ -1167,7 +1420,7 @@ rsConvertFun w abi (Generics ldefs _tparams@[] withLifetimes ldefs $ do arg_shapes <- mapM (rsConvert w) args ret_shape <- maybe (return PExpr_EmptyShape) (rsConvert w) maybe_ret_tp - layoutFun abi arg_shapes ret_shape + abstractFunVarsForLifetimes <$> layoutFun abi arg_shapes ret_shape rsConvertFun _ _ _ _ = fail "rsConvertFun: unsupported Rust function type" diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index 5f20df7d4c..d77917b534 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -77,6 +77,14 @@ import Verifier.SAW.Heapster.TypedCrucible import GHC.Stack +-- | FIXME: document and move to Hobbits +suffixMembers :: prx1 ctx1 -> RAssign prx2 ctx2 -> + RAssign (Member (ctx1 :++: ctx2)) ctx2 +suffixMembers _ MNil = MNil +suffixMembers ctx1 (ctx2 :>: _) = + RL.map Member_Step (suffixMembers ctx1 ctx2) :>: Member_Base + + ---------------------------------------------------------------------- -- * Translation Monads ---------------------------------------------------------------------- @@ -1067,7 +1075,8 @@ data AtomicPermTrans ctx a where AtomicPermTrans ctx (StructType args) -- | The translation of functional permission is a SAW term of functional type - APTrans_Fun :: Mb ctx (FunPerm ghosts (CtxToRList cargs) ret) -> OpenTerm -> + APTrans_Fun :: Mb ctx (FunPerm ghosts (CtxToRList cargs) gouts ret) -> + OpenTerm -> AtomicPermTrans ctx (FunctionHandleType cargs ret) -- | Propositional permissions are represented by a SAW term @@ -1830,18 +1839,32 @@ instance TransInfo info => instance TransInfo info => Translate info ctx (LOwnedPerms ps) (TypeTrans (PermTransCtx ctx ps)) where - translate = translate . fmap (RL.map lownedPermPerm) + translate mb_lops = + translate $ flip fmap mb_lops $ \lops -> + -- NOTE: if we can't translate lops to a DistPerms, we just translate the + -- "raw" / un-offset permissions returned by lownedPermPerm, so that we at + -- least have something to return, and it doesn't really matter what because + -- in this case lops can't really be instantiated anyway + maybe (RL.map lownedPermPerm lops) distPermsToValuePerms $ + lownedPermsToDistPerms lops -- Translate a FunPerm to a pi-abstraction (FIXME: more documentation!) instance TransInfo info => - Translate info ctx (FunPerm ghosts args ret) OpenTerm where - translate (mbMatch -> [nuMP| FunPerm ghosts args ret perms_in perms_out |]) = - 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 (pxys :>: Proxy) perms_out + Translate info ctx (FunPerm ghosts args gouts ret) OpenTerm where + translate (mbMatch -> + [nuMP| FunPerm ghosts args gouts ret perms_in perms_out |]) = + let tops = appendCruCtx (mbLift ghosts) (mbLift args) + tops_prxs = cruCtxProxies tops + rets = CruCtxCons (mbLift gouts) (mbLift ret) + rets_prxs = cruCtxProxies rets in + (infoCtx <$> ask) >>= \ctx -> + case RL.appendAssoc ctx tops_prxs rets_prxs of + Refl -> + piExprCtx tops $ + piPermCtx (mbCombine tops_prxs perms_in) $ \_ -> + applyTransM (return $ globalOpenTerm "Prelude.CompM") $ + translateRetType rets $ + mbCombine (RL.append tops_prxs rets_prxs) perms_out -- | Lambda-abstraction over a permission lambdaPermTrans :: TransInfo info => String -> Mb ctx (ValuePerm a) -> @@ -1866,25 +1889,26 @@ piPermCtx ps f = -- | Build the return type for a function; FIXME: documentation -translateRetType :: TransInfo info => TypeRepr ret -> - Mb (ctx :> ret) (ValuePerms ps) -> +translateRetType :: TransInfo info => CruCtx rets -> + Mb (ctx :++: rets) (ValuePerms ps) -> TransM info ctx OpenTerm -translateRetType ret ret_perms = - do tptrans <- translateClosed ret - sigmaTypeTransM "ret" tptrans (\etrans -> - inExtTransM etrans $ translate ret_perms) +translateRetType rets ret_perms = + do tptrans <- translateClosed rets + sigmaTypeTransM "ret" tptrans (flip inExtMultiTransM + (translate ret_perms)) -- | Build the return type for the function resulting from an entrypoint translateEntryRetType :: TransInfo info => - TypedEntry phase ext blocks tops ret args ghosts -> + TypedEntry phase ext blocks tops rets args ghosts -> TransM info ((tops :++: args) :++: ghosts) OpenTerm -translateEntryRetType (TypedEntry {..}) = +translateEntryRetType (TypedEntry {..} + :: TypedEntry phase ext blocks tops rets args ghosts) = let mb_perms_out = - mbCombine RL.typeCtxProxies $ + mbCombine (cruCtxProxies typedEntryRets) $ extMbMulti (cruCtxProxies typedEntryGhosts) $ extMbMulti (cruCtxProxies typedEntryArgs) $ - mbSeparate (MNil :>: Proxy) typedEntryPermsOut in - translateRetType typedEntryRet mb_perms_out + mbSeparate @_ @tops (cruCtxProxies typedEntryRets) typedEntryPermsOut in + translateRetType typedEntryRets mb_perms_out ---------------------------------------------------------------------- @@ -1895,24 +1919,24 @@ translateEntryRetType (TypedEntry {..}) = -- bound to its translation if it has one: only those entrypoints marked as the -- heads of strongly-connect components have translations as letrec-bound -- variables -data TypedEntryTrans ext blocks tops ret args ghosts = +data TypedEntryTrans ext blocks tops rets args ghosts = TypedEntryTrans { typedEntryTransEntry :: - TypedEntry TransPhase ext blocks tops ret args ghosts, + TypedEntry TransPhase ext blocks tops rets args ghosts, typedEntryTransFun :: Maybe OpenTerm } -- | A mapping from a block to the SAW functions for each entrypoint -data TypedBlockTrans ext blocks tops ret args = +data TypedBlockTrans ext blocks tops rets args = TypedBlockTrans { typedBlockTransEntries :: - [Some (TypedEntryTrans ext blocks tops ret args)] } + [Some (TypedEntryTrans ext blocks tops rets args)] } -- | A mapping from all block entrypoints to their SAW translations -type TypedBlockMapTrans ext blocks tops ret = - RAssign (TypedBlockTrans ext blocks tops ret) blocks +type TypedBlockMapTrans ext blocks tops rets = + RAssign (TypedBlockTrans ext blocks tops rets) blocks -- | Look up the translation of an entry by entry ID lookupEntryTrans :: TypedEntryID blocks args -> - TypedBlockMapTrans ext blocks tops ret -> - Some (TypedEntryTrans ext blocks tops ret args) + TypedBlockMapTrans ext blocks tops rets -> + Some (TypedEntryTrans ext blocks tops rets args) lookupEntryTrans entryID blkMap = maybe (error "lookupEntryTrans") id $ find (\(Some entryTrans) -> @@ -1922,8 +1946,8 @@ lookupEntryTrans entryID blkMap = -- | Look up the translation of an entry by entry ID and make sure that it has -- the supplied ghost arguments lookupEntryTransCast :: TypedEntryID blocks args -> CruCtx ghosts -> - TypedBlockMapTrans ext blocks tops ret -> - TypedEntryTrans ext blocks tops ret args ghosts + TypedBlockMapTrans ext blocks tops rets -> + TypedEntryTrans ext blocks tops rets args ghosts lookupEntryTransCast entryID ghosts blkMap | Some entry_trans <- lookupEntryTrans entryID blkMap , Just Refl <- testEquality ghosts (typedEntryGhosts $ @@ -1939,7 +1963,7 @@ data SomeTypedCallSite blocks tops args vars = -- | Look up a call site by id in a 'TypedBlockMapTrans' lookupCallSite :: TypedCallSiteID blocks args vars -> - TypedBlockMapTrans ext blocks tops ret -> + TypedBlockMapTrans ext blocks tops rets -> SomeTypedCallSite blocks tops args vars lookupCallSite siteID blkMap | Some entry_trans <- lookupEntryTrans (callSiteDest siteID) blkMap @@ -1954,7 +1978,7 @@ lookupCallSite siteID blkMap -- | Contextual info for an implication translation -data ImpTransInfo ext blocks tops ret ps ctx = +data ImpTransInfo ext blocks tops rets ps ctx = ImpTransInfo { itiExprCtx :: ExprTransCtx ctx, @@ -1962,12 +1986,12 @@ data ImpTransInfo ext blocks tops ret ps ctx = itiPermStack :: PermTransCtx ctx ps, itiPermStackVars :: RAssign (Member ctx) ps, itiPermEnv :: PermEnv, - itiBlockMapTrans :: TypedBlockMapTrans ext blocks tops ret, + itiBlockMapTrans :: TypedBlockMapTrans ext blocks tops rets, itiReturnType :: OpenTerm, itiChecksFlag :: ChecksFlag } -instance TransInfo (ImpTransInfo ext blocks tops ret ps) where +instance TransInfo (ImpTransInfo ext blocks tops rets ps) where infoCtx = itiExprCtx infoEnv = itiPermEnv extTransInfo etrans (ImpTransInfo {..}) = @@ -1980,15 +2004,15 @@ instance TransInfo (ImpTransInfo ext blocks tops ret ps) where -- | The monad for translating permission implications -type ImpTransM ext blocks tops ret ps = - TransM (ImpTransInfo ext blocks tops ret ps) +type ImpTransM ext blocks tops rets ps = + TransM (ImpTransInfo ext blocks tops rets ps) -- | Run an 'ImpTransM' computation in a 'TypeTransM' context (FIXME: better -- documentation; e.g., the pctx starts on top of the stack) -impTransM :: forall ctx ps ext blocks tops ret a. +impTransM :: forall ctx ps ext blocks tops rets a. RAssign (Member ctx) ps -> PermTransCtx ctx ps -> - TypedBlockMapTrans ext blocks tops ret -> - OpenTerm -> ImpTransM ext blocks tops ret ps ctx a -> + TypedBlockMapTrans ext blocks tops rets -> + OpenTerm -> ImpTransM ext blocks tops rets ps ctx a -> TypeTransM ctx a impTransM pvars pctx mapTrans retType = withInfoM $ \(TypeTransInfo ectx env checks) -> @@ -2003,45 +2027,45 @@ impTransM pvars pctx mapTrans retType = -- | Embed a type translation into an impure translation -- FIXME: should no longer need this... -tpTransM :: TypeTransM ctx a -> ImpTransM ext blocks tops ret ps ctx a +tpTransM :: TypeTransM ctx a -> ImpTransM ext blocks tops rets ps ctx a tpTransM = withInfoM (\(ImpTransInfo {..}) -> TypeTransInfo itiExprCtx itiPermEnv itiChecksFlag) -- | Run an implication translation computation in an "empty" environment, where -- there are no variables in scope and no permissions held anywhere -inEmptyEnvImpTransM :: ImpTransM ext blocks tops ret RNil RNil a -> - ImpTransM ext blocks tops ret ps ctx a +inEmptyEnvImpTransM :: ImpTransM ext blocks tops rets RNil RNil a -> + ImpTransM ext blocks tops rets ps ctx a inEmptyEnvImpTransM = withInfoM (\(ImpTransInfo {..}) -> ImpTransInfo { itiExprCtx = MNil, itiPermCtx = MNil, itiPermStack = MNil, itiPermStackVars = MNil, .. }) -- | Get most recently bound variable -getTopVarM :: ImpTransM ext blocks tops ret ps (ctx :> tp) (ExprTrans tp) +getTopVarM :: ImpTransM ext blocks tops rets ps (ctx :> tp) (ExprTrans tp) getTopVarM = (\(_ :>: p) -> p) <$> itiExprCtx <$> ask -- | Get the top permission on the stack -getTopPermM :: ImpTransM ext blocks tops ret (ps :> tp) ctx (PermTrans ctx tp) +getTopPermM :: ImpTransM ext blocks tops rets (ps :> tp) ctx (PermTrans ctx tp) getTopPermM = (\(_ :>: p) -> p) <$> itiPermStack <$> ask -- | Helper to disambiguate the @ext@ type variable getExtReprM :: PermCheckExtC ext => - ImpTransM ext blocks tops ret ps ctx (ExtRepr ext) + ImpTransM ext blocks tops rets ps ctx (ExtRepr ext) getExtReprM = return knownRepr -- | Apply a transformation to the (translation of the) current perm stack withPermStackM :: (RAssign (Member ctx) ps_in -> RAssign (Member ctx) ps_out) -> (PermTransCtx ctx ps_in -> PermTransCtx ctx ps_out) -> - ImpTransM ext blocks tops ret ps_out ctx a -> - ImpTransM ext blocks tops ret ps_in ctx a + ImpTransM ext blocks tops rets ps_out ctx a -> + ImpTransM ext blocks tops rets ps_in ctx a withPermStackM f_vars f_p = withInfoM $ \info -> info { itiPermStack = f_p (itiPermStack info), itiPermStackVars = f_vars (itiPermStackVars info) } -- | Get the current permission stack as a 'DistPerms' in context -getPermStackDistPerms :: ImpTransM ext blocks tops ret ps ctx +getPermStackDistPerms :: ImpTransM ext blocks tops rets ps ctx (Mb ctx (DistPerms ps)) getPermStackDistPerms = do stack <- itiPermStack <$> ask @@ -2054,8 +2078,8 @@ getPermStackDistPerms = permTransCtxPerms prxs stack -- | Run a computation if the current 'ChecksFlag' is set -ifChecksFlagM :: ImpTransM ext blocks tops ret ps ctx () -> - ImpTransM ext blocks tops ret ps ctx () +ifChecksFlagM :: ImpTransM ext blocks tops rets ps ctx () -> + ImpTransM ext blocks tops rets ps ctx () ifChecksFlagM m = (itiChecksFlag <$> ask) >>= \checks -> if checksFlagSet checks then m else return () @@ -2064,7 +2088,7 @@ ifChecksFlagM m = -- fails to hold. The 'String' names the construct being translated. assertPermStackM :: HasCallStack => String -> (RAssign (Member ctx) ps -> PermTransCtx ctx ps -> Bool) -> - ImpTransM ext blocks tops ret ps ctx () + ImpTransM ext blocks tops rets ps ctx () assertPermStackM nm f = ifChecksFlagM (ask >>= \info -> @@ -2075,7 +2099,7 @@ assertPermStackM nm f = -- given 'DistPerms' assertPermStackTopEqM :: HasCallStack => ps ~ (ps1 :++: ps2) => String -> f ps1 -> Mb ctx (DistPerms ps2) -> - ImpTransM ext blocks tops ret ps ctx () + ImpTransM ext blocks tops rets ps ctx () assertPermStackTopEqM nm prx expected = ifChecksFlagM (getPermStackDistPerms >>= \perms -> @@ -2090,7 +2114,7 @@ assertPermStackTopEqM nm prx expected = -- | Assert that the current permission stack equals the given 'DistPerms' assertPermStackEqM :: HasCallStack => String -> Mb ctx (DistPerms ps) -> - ImpTransM ext blocks tops ret ps ctx () + ImpTransM ext blocks tops rets ps ctx () assertPermStackEqM nm perms = -- FIXME: unify this function with assertPermStackTopEqM ifChecksFlagM @@ -2105,7 +2129,7 @@ assertPermStackEqM nm perms = -- | Assert that the top permission is as given by the arguments assertTopPermM :: HasCallStack => String -> Mb ctx (ExprVar a) -> Mb ctx (ValuePerm a) -> - ImpTransM ext blocks tops ret (ps :> a) ctx () + ImpTransM ext blocks tops rets (ps :> a) ctx () assertTopPermM nm x p = ifChecksFlagM (getPermStackDistPerms >>= \stack_perms -> @@ -2122,13 +2146,13 @@ assertTopPermM nm x p = -- | Get the (translation of the) perms for a variable getVarPermM :: Mb ctx (ExprVar tp) -> - ImpTransM ext blocks tops ret ps ctx (PermTrans ctx tp) + ImpTransM ext blocks tops rets ps ctx (PermTrans ctx tp) getVarPermM x = RL.get (translateVar x) <$> itiPermCtx <$> ask -- | Assert that a variable has a given permission assertVarPermM :: HasCallStack => String -> Mb ctx (ExprVar tp) -> Mb ctx (ValuePerm tp) -> - ImpTransM ext blocks tops ret ps ctx () + ImpTransM ext blocks tops rets ps ctx () assertVarPermM nm x p = do x_p <- permTransPerm (mbToProxy p) <$> getVarPermM x if x_p == p then return () else @@ -2139,45 +2163,46 @@ assertVarPermM nm x p = -- | Set the (translation of the) perms for a variable in a computation setVarPermM :: Mb ctx (ExprVar tp) -> PermTrans ctx tp -> - ImpTransM ext blocks tops ret ps ctx a -> - ImpTransM ext blocks tops ret ps ctx a + ImpTransM ext blocks tops rets ps ctx a -> + ImpTransM ext blocks tops rets ps ctx a setVarPermM x p = local $ \info -> info { itiPermCtx = RL.set (translateVar x) p $ itiPermCtx info } -- | Clear all permissions in the permission variable map in a sub-computation, -- leaving only those permissions on the top of the stack -clearVarPermsM :: ImpTransM ext blocks tops ret ps ctx a -> - ImpTransM ext blocks tops ret ps ctx a +clearVarPermsM :: ImpTransM ext blocks tops rets ps ctx a -> + ImpTransM ext blocks tops rets ps ctx a clearVarPermsM = local $ \info -> info { itiPermCtx = RL.map (const PTrans_True) $ itiPermCtx info } -- | The current non-monadic return type -returnTypeM :: ImpTransM ext blocks tops ret ps_out ctx OpenTerm +returnTypeM :: ImpTransM ext blocks tops rets ps_out ctx OpenTerm returnTypeM = itiReturnType <$> ask -- | Build the monadic return type @CompM ret@, where @ret@ is the current -- return type in 'itiReturnType' -compReturnTypeM :: ImpTransM ext blocks tops ret ps_out ctx OpenTerm +compReturnTypeM :: ImpTransM ext blocks tops rets ps_out ctx OpenTerm compReturnTypeM = applyOpenTerm (globalOpenTerm "Prelude.CompM") <$> returnTypeM -- | Like 'compReturnTypeM' but build a 'TypeTrans' -compReturnTypeTransM :: ImpTransM ext blocks tops ret ps_out ctx (TypeTrans OpenTerm) +compReturnTypeTransM :: + ImpTransM ext blocks tops rets ps_out ctx (TypeTrans OpenTerm) compReturnTypeTransM = flip mkTypeTrans1 id <$> compReturnTypeM -- | Build an @errorM@ computation with the given error message -mkErrorCompM :: String -> ImpTransM ext blocks tops ret ps_out ctx OpenTerm +mkErrorCompM :: String -> ImpTransM ext blocks tops rets ps_out ctx OpenTerm mkErrorCompM msg = applyMultiTransM (return $ globalOpenTerm "Prelude.errorM") [returnTypeM, return $ stringLitOpenTerm $ pack msg] -- | The typeclass for the implication translation of a functor at any -- permission set inside any binding to an 'OpenTerm' -class NuMatchingAny1 f => ImplTranslateF f ext blocks tops ret where - translateF :: Mb ctx (f ps) -> ImpTransM ext blocks tops ret ps ctx OpenTerm +class NuMatchingAny1 f => ImplTranslateF f ext blocks tops rets where + translateF :: Mb ctx (f ps) -> ImpTransM ext blocks tops rets ps ctx OpenTerm ---------------------------------------------------------------------- @@ -2186,29 +2211,30 @@ class NuMatchingAny1 f => ImplTranslateF f ext blocks tops ret where -- | Translate the output permissions of a 'SimplImpl' translateSimplImplOut :: Mb ctx (SimplImpl ps_in ps_out) -> - ImpTransM ext blocks tops ret ps ctx + ImpTransM ext blocks tops rets ps ctx (TypeTrans (PermTransCtx ctx ps_out)) translateSimplImplOut = translate . mbSimplImplOut -- | Translate the head output permission of a 'SimplImpl' translateSimplImplOutHead :: Mb ctx (SimplImpl ps_in (ps_out :> a)) -> - ImpTransM ext blocks tops ret ps ctx + ImpTransM ext blocks tops rets ps ctx (TypeTrans (PermTrans ctx a)) translateSimplImplOutHead = translate . mbMapCl $(mkClosed [| varAndPermPerm . RL.head |]) . mbSimplImplOut -- | Translate the head of the tail of the output permission of a 'SimplImpl' translateSimplImplOutTailHead :: Mb ctx (SimplImpl ps_in (ps_out :> a :> b)) -> - ImpTransM ext blocks tops ret ps ctx + ImpTransM ext blocks tops rets ps ctx (TypeTrans (PermTrans ctx a)) translateSimplImplOutTailHead = translate . mbMapCl $(mkClosed [| varAndPermPerm . RL.head . RL.tail |]) . mbSimplImplOut -- | Translate a 'SimplImpl' to a function on translation computations -translateSimplImpl :: Proxy ps -> Mb ctx (SimplImpl ps_in ps_out) -> - ImpTransM ext blocks tops ret (ps :++: ps_out) ctx OpenTerm -> - ImpTransM ext blocks tops ret (ps :++: ps_in) ctx OpenTerm +translateSimplImpl :: + Proxy ps -> Mb ctx (SimplImpl ps_in ps_out) -> + ImpTransM ext blocks tops rets (ps :++: ps_out) ctx OpenTerm -> + ImpTransM ext blocks tops rets (ps :++: ps_in) ctx OpenTerm translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of [nuMP| SImpl_Drop _ _ |] -> withPermStackM (\(xs :>: _) -> xs) (\(ps :>: _) -> ps) m @@ -3288,9 +3314,9 @@ data ImplFailCont -- | "Force" the translation of a possibly failing computation to always return -- a computation, even if it is just the failing computation forceImplTrans :: Maybe (ImplFailCont -> - ImpTransM ext blocks tops ret ps ctx OpenTerm) -> + ImpTransM ext blocks tops rets ps ctx OpenTerm) -> ImplFailCont -> - ImpTransM ext blocks tops ret ps ctx OpenTerm + ImpTransM ext blocks tops rets ps ctx OpenTerm forceImplTrans (Just trans) k = trans k forceImplTrans Nothing (ImplFailContTerm errM) = return errM forceImplTrans Nothing (ImplFailContMsg str) = @@ -3301,7 +3327,7 @@ forceImplTrans Nothing (ImplFailContMsg str) = -- | Perform a failure by jumping to a failure continuation or signaling an -- error, using an alternate error message in the latter case implTransAltErr :: String -> ImplFailCont -> - ImpTransM ext blocks tops ret ps ctx OpenTerm + ImpTransM ext blocks tops rets ps ctx OpenTerm implTransAltErr _ (ImplFailContTerm errM) = return errM implTransAltErr str (ImplFailContMsg _) = returnTypeM >>= \tp -> @@ -3313,25 +3339,25 @@ implTransAltErr str (ImplFailContMsg _) = -- the argument fails translatePermImplUnary :: RL.TypeCtx bs => - ImplTranslateF r ext blocks tops ret => + ImplTranslateF r ext blocks tops rets => 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) -> + (ImpTransM ext blocks tops rets ps_out (ctx :++: bs) OpenTerm -> + ImpTransM ext blocks tops rets ps ctx OpenTerm) -> PermImplTransM (ImplFailCont -> - ImpTransM ext blocks tops ret ps ctx OpenTerm) + ImpTransM ext blocks tops rets ps ctx OpenTerm) translatePermImplUnary (mbMatch -> [nuMP| MbPermImpls_Cons _ _ mb_impl |]) f = translatePermImpl Proxy (mbCombine RL.typeCtxProxies mb_impl) >>= \trans -> return $ \k -> f $ trans k -- | Translate a 'PermImpl1' to a function on translation computations -translatePermImpl1 :: ImplTranslateF r ext blocks tops ret => +translatePermImpl1 :: ImplTranslateF r ext blocks tops rets => Proxy '(ext, blocks, tops, ret) -> Mb ctx (PermImpl1 ps ps_outs) -> Mb ctx (MbPermImpls r ps_outs) -> PermImplTransM (ImplFailCont -> - ImpTransM ext blocks tops ret ps ctx OpenTerm) + ImpTransM ext blocks tops rets ps ctx OpenTerm) translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impls) of -- A failure translates to a call to the catch handler, which is the most recent -- Impl1_Catch, if one exists, or the SAW errorM function otherwise @@ -3775,12 +3801,12 @@ translatePermImpl1 prx mb_impl mb_impls = case (mbMatch mb_impl, mbMatch mb_impl -- | Translate a 'PermImpl' in the 'PermImplTransM' monad to a function that -- takes a failure continuation and returns a monadic computation to generate -- the translation as a term -translatePermImpl :: ImplTranslateF r ext blocks tops ret => +translatePermImpl :: ImplTranslateF r ext blocks tops rets => Proxy '(ext, blocks, tops, ret) -> Mb ctx (PermImpl r ps) -> PermImplTransM (ImplFailCont -> - ImpTransM ext blocks tops ret ps ctx OpenTerm) + ImpTransM ext blocks tops rets ps ctx OpenTerm) translatePermImpl prx mb_impl = case mbMatch mb_impl of [nuMP| PermImpl_Done r |] -> return $ const $ translateF r @@ -3788,9 +3814,9 @@ translatePermImpl prx mb_impl = case mbMatch mb_impl of translatePermImpl1 prx impl1 mb_impls -instance ImplTranslateF r ext blocks tops ret => - Translate (ImpTransInfo - ext blocks tops ret ps) ctx (AnnotPermImpl r ps) OpenTerm where +instance ImplTranslateF r ext blocks tops rets => + Translate (ImpTransInfo ext blocks tops rets ps) + ctx (AnnotPermImpl r ps) OpenTerm where translate (mbMatch -> [nuMP| AnnotPermImpl err impl |]) = let (transF, (errs,_)) = runPermImplTransM $ translatePermImpl Proxy impl in forceImplTrans transF $ @@ -3799,7 +3825,7 @@ instance ImplTranslateF r ext blocks tops ret => "\n\n--------------------\n\n" errs)) -- We translate a LocalImplRet to a term that returns all current permissions -instance ImplTranslateF (LocalImplRet ps) ext blocks ps_in ret where +instance ImplTranslateF (LocalImplRet ps) ext blocks ps_in rets where translateF _ = do pctx <- itiPermStack <$> ask ret_tp <- returnTypeM @@ -3808,7 +3834,7 @@ instance ImplTranslateF (LocalImplRet ps) ext blocks ps_in ret where -- | Translate a local implication to its output, adding an error message translateLocalPermImpl :: String -> Mb ctx (LocalPermImpl ps_in ps_out) -> - ImpTransM ext blocks tops ret ps_in ctx OpenTerm + ImpTransM ext blocks tops rets ps_in ctx OpenTerm translateLocalPermImpl err (mbMatch -> [nuMP| LocalPermImpl impl |]) = clearVarPermsM $ translate $ fmap (AnnotPermImpl err) impl @@ -3822,7 +3848,7 @@ translateCurryLocalPermImpl :: PermTransCtx ctx ps1 -> RAssign (Member ctx) ps1 -> TypeTrans (PermTransCtx ctx ps2) -> RAssign (Member ctx) ps2 -> TypeTrans (PermTransCtx ctx ps_out) -> - ImpTransM ext blocks tops ret ps ctx OpenTerm + ImpTransM ext blocks tops rets ps ctx OpenTerm translateCurryLocalPermImpl err impl pctx1 vars1 tp_trans2 vars2 tp_trans_out = lambdaTransM "x_local" tp_trans2 $ \pctx2 -> local (\info -> info { itiReturnType = typeTransType1 tp_trans_out }) $ @@ -4124,7 +4150,7 @@ debugPrettyPermCtx prxs (ptranss :>: ptrans) = -- stack. The 'String' argument is the name of the construct being applied, for -- use in error reporting. translateApply :: String -> OpenTerm -> Mb ctx (DistPerms ps) -> - ImpTransM ext blocks tops ret ps ctx OpenTerm + ImpTransM ext blocks tops rets ps ctx OpenTerm translateApply nm f perms = do assertPermStackEqM nm perms expr_ctx <- itiExprCtx <$> ask @@ -4143,12 +4169,12 @@ translateApply nm f perms = -- | Translate a call to (the translation of) an entrypoint, by either calling -- the letrec-bound variable for the entrypoint, if it has one, or by just -- translating the body of the entrypoint if it does not. -translateCallEntry :: forall ext tops args ghosts blocks ctx ret. +translateCallEntry :: forall ext tops args ghosts blocks ctx rets. PermCheckExtC ext => String -> - TypedEntryTrans ext blocks tops ret args ghosts -> + TypedEntryTrans ext blocks tops rets args ghosts -> Mb ctx (RAssign ExprVar (tops :++: args)) -> Mb ctx (RAssign ExprVar ghosts) -> - ImpTransM ext blocks tops ret + ImpTransM ext blocks tops rets ((tops :++: args) :++: ghosts) ctx OpenTerm translateCallEntry nm entry_trans mb_tops_args mb_ghosts = -- First test that the stack == the required perms for entryID @@ -4178,7 +4204,7 @@ translateCallEntry nm entry_trans mb_tops_args mb_ghosts = instance PermCheckExtC ext => - Translate (ImpTransInfo ext blocks tops ret ps) ctx + Translate (ImpTransInfo ext blocks tops rets ps) ctx (CallSiteImplRet blocks tops args ghosts ps) OpenTerm where translate (mbMatch -> [nuMP| CallSiteImplRet entryID ghosts Refl mb_tavars mb_gvars |]) = @@ -4189,12 +4215,12 @@ instance PermCheckExtC ext => instance PermCheckExtC ext => ImplTranslateF (CallSiteImplRet blocks tops args ghosts) - ext blocks tops ret where + ext blocks tops rets where translateF mb_tgt = translate mb_tgt instance PermCheckExtC ext => - Translate (ImpTransInfo ext blocks tops ret ps) ctx + Translate (ImpTransInfo ext blocks tops rets ps) ctx (TypedJumpTarget blocks tops ps) OpenTerm where translate (mbMatch -> [nuMP| TypedJumpTarget siteID _ _ mb_perms_in |]) = do SomeTypedCallSite site <- @@ -4204,7 +4230,7 @@ instance PermCheckExtC ext => varSubst (permVarSubstOfNames $ distPermsVars perms_in) mb_impl instance PermCheckExtC ext => - ImplTranslateF (TypedJumpTarget blocks tops) ext blocks tops ret where + ImplTranslateF (TypedJumpTarget blocks tops) ext blocks tops rets where translateF mb_tgt = translate mb_tgt @@ -4213,10 +4239,11 @@ instance PermCheckExtC ext => ---------------------------------------------------------------------- -- | Translate a 'TypedStmt' to a function on translation computations -translateStmt :: PermCheckExtC ext => - ProgramLoc -> Mb ctx (TypedStmt ext rets ps_in ps_out) -> - ImpTransM ext blocks tops ret ps_out (ctx :++: rets) OpenTerm -> - ImpTransM ext blocks tops ret ps_in ctx OpenTerm +translateStmt :: + PermCheckExtC ext => ProgramLoc -> + Mb ctx (TypedStmt ext stmt_rets ps_in ps_out) -> + ImpTransM ext blocks tops rets ps_out (ctx :++: stmt_rets) OpenTerm -> + ImpTransM ext blocks tops rets ps_in ctx OpenTerm translateStmt loc mb_stmt m = case mbMatch mb_stmt of [nuMP| TypedSetReg tp e |] -> do tp_trans <- translate tp @@ -4231,16 +4258,19 @@ translateStmt loc mb_stmt m = case mbMatch mb_stmt of inExtTransM etrans $ withPermStackM (:>: Member_Base) (:>: PTrans_Eq (extMb e)) m - [nuMP| stmt@(TypedCall _freg fun_perm _ gexprs args) |] -> + [nuMP| TypedCall _freg fun_perm _ gexprs args |] -> do f_trans <- getTopPermM + ectx_outer <- itiExprCtx <$> ask let f = case f_trans 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 RL.typeCtxProxies - $ fmap (\stmt' -> nu $ \ret -> - typedStmtOut stmt' (MNil :>: ret)) stmt - ret_tp <- translate $ fmap funPermRet fun_perm + let rets = mbLift $ mbMapCl $(mkClosed [| funPermRets |]) fun_perm + let rets_prxs = cruCtxProxies rets + rets_trans <- translateClosed rets + let perms_out = + mbCombine rets_prxs $ flip mbMapCl mb_stmt + ($(mkClosed [| \prxs stmt -> nuMulti prxs (typedStmtOut stmt) |]) + `clApply` toClosed rets_prxs) ectx_gexprs <- translate gexprs ectx_args <- translate args pctx_in <- RL.tail <$> itiPermStack <$> ask @@ -4250,18 +4280,21 @@ translateStmt loc mb_stmt m = case mbMatch mb_stmt of applyOpenTermMulti f (exprCtxToTerms ectx_gexprs ++ exprCtxToTerms ectx_args ++ permCtxToTerms pctx_ghosts_args) - fret_tp <- sigmaTypeTransM "ret" ret_tp (flip inExtTransM - (translate perms_out)) + fret_tp <- sigmaTypeTransM "ret" rets_trans (flip inExtMultiTransM + (translate perms_out)) applyMultiTransM (return $ globalOpenTerm "Prelude.bindM") [return fret_tp, returnTypeM, return fret_trm, lambdaOpenTermTransM "call_ret_val" fret_tp $ \ret_val -> - sigmaElimTransM "elim_call_ret_val" ret_tp - (flip inExtTransM (translate perms_out)) compReturnTypeTransM - (\ret_trans pctx -> - inExtTransM ret_trans $ + sigmaElimTransM "elim_call_ret_val" rets_trans + (flip inExtMultiTransM (translate perms_out)) compReturnTypeTransM + (\rets_ectx pctx -> + inExtMultiTransM rets_ectx $ withPermStackM (\(vars :>: _) -> - (fst (RL.split Proxy ectx_gexprs vars) :>: Member_Base)) + RL.append + (fst (RL.split + (RL.append ectx_gexprs ectx_args) ectx_gexprs vars)) $ + suffixMembers ectx_outer rets_prxs) (const pctx) m) ret_val] @@ -4279,8 +4312,8 @@ translateStmt loc mb_stmt m = case mbMatch mb_stmt of -- | Translate a 'TypedStmt' to a function on translation computations translateLLVMStmt :: Mb ctx (TypedLLVMStmt r ps_in ps_out) -> - ImpTransM ext blocks tops ret ps_out (ctx :> r) OpenTerm -> - ImpTransM ext blocks tops ret ps_in ctx OpenTerm + ImpTransM ext blocks tops rets ps_out (ctx :> r) OpenTerm -> + ImpTransM ext blocks tops rets ps_in ctx OpenTerm translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of [nuMP| ConstructLLVMWord (TypedReg x) |] -> inExtTransM ETrans_LLVM $ @@ -4424,32 +4457,34 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of ---------------------------------------------------------------------- instance PermCheckExtC ext => - Translate (ImpTransInfo ext blocks tops ret ps) ctx - (TypedRet tops ret ps) OpenTerm where - translate (mbMatch -> [nuMP| TypedRet Refl tp r mb_perms |]) = + Translate (ImpTransInfo ext blocks tops rets ps) ctx + (TypedRet tops rets ps) OpenTerm where + translate (mbMatch -> [nuMP| TypedRet Refl mb_rets mb_rets_ns mb_perms |]) = do let perms = mbMap2 - (\reg mbps -> varSubst (singletonVarSubst $ typedRegVar reg) mbps) - r mb_perms + (\rets_ns ps -> varSubst (permVarSubstOfNames rets_ns) ps) + mb_rets_ns mb_perms () <- assertPermStackEqM "TypedRet" perms - r_trans <- translate r - tp_trans <- translate tp + rets_trans <- translate mb_rets + let rets_prxs = cruCtxProxies $ mbLift mb_rets + rets_ns_trans <- translate mb_rets_ns ret_tp <- returnTypeM sigma_trm <- - sigmaTransM "r" tp_trans (flip inExtTransM $ - translate $ mbCombine RL.typeCtxProxies mb_perms) - r_trans (itiPermStack <$> ask) + sigmaTransM "r" rets_trans + (flip inExtMultiTransM $ + translate $ mbCombine rets_prxs mb_perms) + rets_ns_trans (itiPermStack <$> ask) return $ applyOpenTermMulti (globalOpenTerm "Prelude.returnM") [ret_tp, sigma_trm] instance PermCheckExtC ext => - ImplTranslateF (TypedRet tops ret) ext blocks tops ret where + ImplTranslateF (TypedRet tops rets) ext blocks tops rets where translateF mb_ret = translate mb_ret instance PermCheckExtC ext => - Translate (ImpTransInfo ext blocks tops ret ps) ctx - (TypedTermStmt blocks tops ret ps) OpenTerm where + Translate (ImpTransInfo ext blocks tops rets ps) ctx + (TypedTermStmt blocks tops rets ps) OpenTerm where translate mb_x = case mbMatch mb_x of [nuMP| TypedJump impl_tgt |] -> translate impl_tgt [nuMP| TypedBr reg impl_tgt1 impl_tgt2 |] -> @@ -4464,8 +4499,8 @@ instance PermCheckExtC ext => instance PermCheckExtC ext => - Translate (ImpTransInfo ext blocks tops ret ps) ctx - (TypedStmtSeq ext blocks tops ret ps) OpenTerm where + Translate (ImpTransInfo ext blocks tops rets ps) ctx + (TypedStmtSeq ext blocks tops rets ps) OpenTerm where translate mb_x = case mbMatch mb_x of [nuMP| TypedImplStmt impl_seq |] -> translate impl_seq [nuMP| TypedConsStmt loc stmt pxys mb_seq |] -> @@ -4474,7 +4509,7 @@ instance PermCheckExtC ext => instance PermCheckExtC ext => ImplTranslateF (TypedStmtSeq - ext blocks tops ret) ext blocks tops ret where + ext blocks tops rets) ext blocks tops rets where translateF mb_seq = translate mb_seq @@ -4483,17 +4518,17 @@ instance PermCheckExtC ext => ---------------------------------------------------------------------- -- | An entrypoint over some regular and ghost arguments -data SomeTypedEntry ext blocks tops ret = +data SomeTypedEntry ext blocks tops rets = forall ghosts args. - SomeTypedEntry (TypedEntry TransPhase ext blocks tops ret args ghosts) + SomeTypedEntry (TypedEntry TransPhase ext blocks tops rets args ghosts) -- | Get all entrypoints in a block map that will be translated to letrec-bound -- variables, which is all entrypoints with in-degree > 1 -- -- FIXME: consider whether we want let and not letRec for entrypoints that have -- in-degree > 1 but are not the heads of loops -typedBlockLetRecEntries :: TypedBlockMap TransPhase ext blocks tops ret -> - [SomeTypedEntry ext blocks tops ret] +typedBlockLetRecEntries :: TypedBlockMap TransPhase ext blocks tops rets -> + [SomeTypedEntry ext blocks tops rets] typedBlockLetRecEntries = concat . RL.mapToList (map (\(Some entry) -> SomeTypedEntry entry) @@ -4504,8 +4539,8 @@ typedBlockLetRecEntries = -- corresponds to a letrec-bound variable foldBlockMapLetRec :: (forall args ghosts. - TypedEntry TransPhase ext blocks tops ret args ghosts -> b -> b) -> - b -> TypedBlockMap TransPhase ext blocks tops ret -> b + TypedEntry TransPhase ext blocks tops rets args ghosts -> b -> b) -> + b -> TypedBlockMap TransPhase ext blocks tops rets -> b foldBlockMapLetRec f r = foldr (\(SomeTypedEntry entry) -> f entry) r . typedBlockLetRecEntries @@ -4526,7 +4561,7 @@ piLRTTransM x tps body_f = -- | Build a @LetRecType@ that describes the type of the translation of a -- 'TypedEntry' -translateEntryLRT :: TypedEntry TransPhase ext blocks tops ret args ghosts -> +translateEntryLRT :: TypedEntry TransPhase ext blocks tops rets args ghosts -> TypeTransM ctx OpenTerm translateEntryLRT entry@(TypedEntry {..}) = inEmptyCtxTransM $ @@ -4540,7 +4575,7 @@ translateEntryLRT entry@(TypedEntry {..}) = -- | Build a @LetRecTypes@ list that describes the types of all of the -- entrypoints in a 'TypedBlockMap' -translateBlockMapLRTs :: TypedBlockMap TransPhase ext blocks tops ret -> +translateBlockMapLRTs :: TypedBlockMap TransPhase ext blocks tops rets -> TypeTransM ctx OpenTerm translateBlockMapLRTs = foldBlockMapLetRec @@ -4553,13 +4588,13 @@ translateBlockMapLRTs = -- | Lambda-abstract over all the entrypoints in a 'TypedBlockMap' that -- correspond to letrec-bound functions, putting the lambda-bound variables into -- a 'TypedBlockMapTrans' structure and passing it to the supplied body function -lambdaBlockMap :: TypedBlockMap TransPhase ext blocks tops ret -> - (TypedBlockMapTrans ext blocks tops ret -> +lambdaBlockMap :: TypedBlockMap TransPhase ext blocks tops rets -> + (TypedBlockMapTrans ext blocks tops rets -> TypeTransM ctx OpenTerm) -> TypeTransM ctx OpenTerm lambdaBlockMap = helper where - helper :: RAssign (TypedBlock TransPhase ext blocks tops ret) blks -> - (RAssign (TypedBlockTrans ext blocks tops ret) blks -> + helper :: RAssign (TypedBlock TransPhase ext blocks tops rets) blks -> + (RAssign (TypedBlockTrans ext blocks tops rets) blks -> TypeTransM ctx OpenTerm) -> TypeTransM ctx OpenTerm helper MNil f = f MNil @@ -4587,8 +4622,8 @@ lambdaBlockMap = helper where -- over the top-level, local, and ghost arguments and (the translations of) the -- input permissions of the entrypoint translateEntryBody :: PermCheckExtC ext => - TypedBlockMapTrans ext blocks tops ret -> - TypedEntry TransPhase ext blocks tops ret args ghosts -> + TypedBlockMapTrans ext blocks tops rets -> + TypedEntry TransPhase ext blocks tops rets args ghosts -> TypeTransM ctx OpenTerm translateEntryBody mapTrans entry = inEmptyCtxTransM $ @@ -4601,8 +4636,8 @@ translateEntryBody mapTrans entry = -- | Translate all the entrypoints in a 'TypedBlockMap' that correspond to -- letrec-bound functions to SAW core functions as in 'translateEntryBody' translateBlockMapBodies :: PermCheckExtC ext => - TypedBlockMapTrans ext blocks tops ret -> - TypedBlockMap TransPhase ext blocks tops ret -> + TypedBlockMapTrans ext blocks tops rets -> + TypedBlockMap TransPhase ext blocks tops rets -> TypeTransM ctx OpenTerm translateBlockMapBodies mapTrans = foldBlockMapLetRec @@ -4615,21 +4650,21 @@ translateBlockMapBodies mapTrans = translateCFG :: PermCheckExtC ext => PermEnv -> ChecksFlag -> - TypedCFG ext blocks ghosts inits ret -> + TypedCFG ext blocks ghosts inits gouts ret -> OpenTerm -translateCFG env checks (cfg :: TypedCFG ext blocks ghosts inits ret) = +translateCFG env checks (cfg :: TypedCFG ext blocks ghosts inits gouts ret) = let h = tpcfgHandle cfg fun_perm = tpcfgFunPerm cfg blkMap = tpcfgBlockMap cfg ctx = typedFnHandleAllArgs h inits = typedFnHandleArgs h ghosts = typedFnHandleGhosts h - retType = typedFnHandleRetType h in + retTypes = typedFnHandleRetTypes h in runNilTypeTransM env checks $ lambdaExprCtx ctx $ -- We translate retType before extending the expr context to contain another -- copy of inits, as it is easier to do it here - translateRetType retType (tpcfgOutputPerms cfg) >>= \retTypeTrans -> + translateRetType retTypes (tpcfgOutputPerms cfg) >>= \retTypeTrans -> -- Extend the expr context to contain another copy of the initial arguments -- inits, since the initial entrypoint for the entire function takes two @@ -4687,7 +4722,7 @@ translateCFG env checks (cfg :: TypedCFG ext blocks ghosts inits ret) = -- a 'String' name we want to translate it to data SomeCFGAndPerm ext where SomeCFGAndPerm :: GlobalSymbol -> String -> CFG ext blocks inits ret -> - FunPerm ghosts (CtxToRList inits) ret -> + FunPerm ghosts (CtxToRList inits) gouts ret -> SomeCFGAndPerm ext -- | Extract the 'GlobalSymbol' from a 'SomeCFGAndPerm' @@ -4702,14 +4737,14 @@ someCFGAndPermToName (SomeCFGAndPerm _ nm _ _) = nm -- description of the SAW core type it translates to someCFGAndPermLRT :: PermEnv -> SomeCFGAndPerm ext -> OpenTerm someCFGAndPermLRT env (SomeCFGAndPerm _ _ _ - (FunPerm ghosts args ret perms_in perms_out)) = + (FunPerm ghosts args gouts ret perms_in perms_out)) = runNilTypeTransM env noChecks $ translateClosed (appendCruCtx ghosts args) >>= \ctx_trans -> piLRTTransM "arg" ctx_trans $ \ectx -> inCtxTransM ectx $ translate perms_in >>= \perms_trans -> piLRTTransM "perm" perms_trans $ \_ -> - translateRetType ret perms_out >>= \ret_tp -> + translateRetType (CruCtxCons gouts ret) perms_out >>= \ret_tp -> return $ ctorOpenTerm "Prelude.LRT_Ret" [ret_tp] -- | Extract the 'FunPerm' of a 'SomeCFGAndPerm' as a permission on LLVM @@ -4808,7 +4843,7 @@ tcTranslateAddCFGs sc mod_name env checks endianness dlevel cfgs_and_perms = -- | Translate a 'FunPerm' to the SAW core type it represents translateCompleteFunPerm :: SharedContext -> PermEnv -> - FunPerm ghosts args ret -> IO Term + FunPerm ghosts args gouts ret -> IO Term translateCompleteFunPerm sc env fun_perm = completeNormOpenTerm sc $ runNilTypeTransM env noChecks (translate $ emptyMb fun_perm) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs index 5e3275f2da..2ac7d0a5f0 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypeChecker.hs @@ -687,17 +687,22 @@ tcSortedMbValuePerms ctx perms = -- | Check a function permission of the form -- --- > (x1:tp1, ...). arg1:p1, ... -o arg1:p1', ..., argn:pn', ret:p_ret +-- > (x1:tp1, ...). arg1:p1, ... -o +-- > (y1:tp1', ..., ym:tpm'). arg1:p1', ..., argn:pn', ret:p_ret -- -- for some arbitrary context @x1:tp1, ...@ of ghost variables tcFunPerm :: CruCtx args -> TypeRepr ret -> AstFunPerm -> Tc (SomeFunPerm args ret) -tcFunPerm args ret (AstFunPerm _ untyCtx ins outs) = +tcFunPerm args ret (AstFunPerm _ untyCtx ins untyCtxOut outs) = do Some ghosts_ctx@(ParsedCtx _ ghosts) <- tcCtx untyCtx + Some gouts_ctx@(ParsedCtx _ gouts) <- tcCtx untyCtxOut let args_ctx = mkArgsParsedCtx args - ghosts_args_ctx = appendParsedCtx ghosts_ctx args_ctx - perms_in <- tcSortedMbValuePerms ghosts_args_ctx ins - perms_out <- tcSortedMbValuePerms (consParsedCtx "ret" ret ghosts_args_ctx) outs - pure (SomeFunPerm (FunPerm ghosts args ret perms_in perms_out)) + perms_in_ctx = appendParsedCtx ghosts_ctx args_ctx + perms_out_ctx = + appendParsedCtx (appendParsedCtx ghosts_ctx args_ctx) + (consParsedCtx "ret" ret gouts_ctx) + perms_in <- tcSortedMbValuePerms perms_in_ctx ins + perms_out <- tcSortedMbValuePerms perms_out_ctx outs + pure (SomeFunPerm (FunPerm ghosts args gouts ret perms_in perms_out)) ---------------------------------------------------------------------- -- * Parsing Permission Sets and Function Permissions diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index 4608dfcc18..21116bbaca 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs @@ -191,30 +191,42 @@ regWithValExpr (RegNoVal (TypedReg x)) = PExpr_Var x data TypedExpr ext tp = TypedExpr !(App ext RegWithVal tp) !(Maybe (PermExpr tp)) --- | A "typed" function handle is a normal function handle along with a context --- of ghost variables -data TypedFnHandle ghosts args ret where - TypedFnHandle :: !(CruCtx ghosts) -> !(FnHandle cargs ret) -> - TypedFnHandle ghosts (CtxToRList cargs) ret +-- | A "typed" function handle is a normal function handle along with contexts +-- of ghost input and output variables +data TypedFnHandle ghosts args gouts ret where + TypedFnHandle :: !(CruCtx ghosts) -> !(CruCtx gouts) -> + !(FnHandle cargs ret) -> + TypedFnHandle ghosts (CtxToRList cargs) gouts ret -- | Extract out the context of ghost arguments from a 'TypedFnHandle' -typedFnHandleGhosts :: TypedFnHandle ghosts args ret -> CruCtx ghosts -typedFnHandleGhosts (TypedFnHandle ghosts _) = ghosts +typedFnHandleGhosts :: TypedFnHandle ghosts args gouts ret -> CruCtx ghosts +typedFnHandleGhosts (TypedFnHandle ghosts _ _) = ghosts + +-- | Extract out the context of output ghost arguments from a 'TypedFnHandle' +typedFnHandleGouts :: TypedFnHandle ghosts args gouts ret -> CruCtx gouts +typedFnHandleGouts (TypedFnHandle _ gouts _) = gouts -- | Extract out the context of regular arguments from a 'TypedFnHandle' -typedFnHandleArgs :: TypedFnHandle ghosts args ret -> CruCtx args -typedFnHandleArgs (TypedFnHandle _ h) = mkCruCtx $ handleArgTypes h +typedFnHandleArgs :: TypedFnHandle ghosts args gouts ret -> CruCtx args +typedFnHandleArgs (TypedFnHandle _ _ h) = mkCruCtx $ handleArgTypes h -- | Extract out the context of all arguments of a 'TypedFnHandle', including -- the lifetime argument -typedFnHandleAllArgs :: TypedFnHandle ghosts args ret -> CruCtx (ghosts :++: args) +typedFnHandleAllArgs :: TypedFnHandle ghosts args gouts ret -> + CruCtx (ghosts :++: args) typedFnHandleAllArgs h = appendCruCtx (typedFnHandleGhosts h) (typedFnHandleArgs h) -- | Extract out the return type of a 'TypedFnHandle' -typedFnHandleRetType :: TypedFnHandle ghosts args ret -> TypeRepr ret -typedFnHandleRetType (TypedFnHandle _ h) = handleReturnType h +typedFnHandleRetType :: TypedFnHandle ghosts args gouts ret -> TypeRepr ret +typedFnHandleRetType (TypedFnHandle _ _ h) = handleReturnType h + +-- | Extract out all the return types of a 'TypedFnHandle' +typedFnHandleRetTypes :: TypedFnHandle ghosts args gouts ret -> + CruCtx (gouts :> ret) +typedFnHandleRetTypes (TypedFnHandle _ gouts h) = + CruCtxCons gouts $ handleReturnType h -- | As in standard Crucible, blocks are identified by membership proofs that @@ -326,7 +338,8 @@ instance NuMatchingAny1 RegWithVal where nuMatchingAny1Proof = nuMatchingProof $(mkNuMatching [t| forall ext tp. NuMatchingExtC ext => TypedExpr ext tp |]) -$(mkNuMatching [t| forall ghosts args ret. TypedFnHandle ghosts args ret |]) +$(mkNuMatching [t| forall ghosts args gouts ret. + TypedFnHandle ghosts args gouts ret |]) $(mkNuMatching [t| forall blocks args. TypedBlockID blocks args |]) $(mkNuMatching [t| forall blocks args. TypedEntryID blocks args |]) $(mkNuMatching [t| forall blocks args ghosts. TypedCallSiteID blocks args ghosts |]) @@ -373,7 +386,7 @@ instance Liftable (TypedCallSiteID blocks args vars) where -- | Typed Crucible statements with the given Crucible syntax extension and the -- given set of return values -data TypedStmt ext (rets :: RList CrucibleType) ps_in ps_out where +data TypedStmt ext (stmt_rets :: RList CrucibleType) ps_in ps_out where -- | Assign a pure Crucible expressions to a register, where pure here means -- that its translation to SAW will be pure (i.e., no LLVM pointer operations) @@ -395,11 +408,11 @@ data TypedStmt ext (rets :: RList CrucibleType) ps_in ps_out where -- > [gexprs/ghosts]ps_out TypedCall :: args ~ CtxToRList cargs => !(TypedReg (FunctionHandleType cargs ret)) -> - !(FunPerm ghosts args ret) -> + !(FunPerm ghosts args gouts ret) -> !(TypedRegs ghosts) -> !(PermExprs ghosts) -> !(TypedRegs args) -> - TypedStmt ext (RNil :> ret) + TypedStmt ext (gouts :> ret) ((ghosts :++: args) :++: ghosts :> FunctionHandleType cargs ret) - (ghosts :++: args :> ret) + ((ghosts :++: args) :++: gouts :> ret) -- | Assert a boolean condition, printing the given string on failure TypedAssert :: !(TypedReg BoolType) -> !(TypedReg (StringType Unicode)) -> @@ -569,7 +582,7 @@ data TypedLLVMStmt ret ps_in ps_out where TypedLLVMStmt (LLVMPointerType w) RNil (RNil :> LLVMPointerType w) -- | Return the input permissions for a 'TypedStmt' -typedStmtIn :: TypedStmt ext rets ps_in ps_out -> DistPerms ps_in +typedStmtIn :: TypedStmt ext stmt_rets ps_in ps_out -> DistPerms ps_in typedStmtIn (TypedSetReg _ _) = DistPermsNil typedStmtIn (TypedSetRegPermExpr _ _) = DistPermsNil typedStmtIn (TypedCall (TypedReg f) fun_perm ghosts gexprs args) = @@ -628,17 +641,17 @@ typedLLVMStmtIn (TypedLLVMResolveGlobal _ _) = typedLLVMStmtIn (TypedLLVMIte _ _ _ _) = DistPermsNil -- | Return the output permissions for a 'TypedStmt' -typedStmtOut :: TypedStmt ext rets ps_in ps_out -> RAssign Name rets -> - DistPerms ps_out +typedStmtOut :: TypedStmt ext stmt_rets ps_in ps_out -> + RAssign Name stmt_rets -> DistPerms ps_out typedStmtOut (TypedSetReg _ (TypedExpr _ (Just e))) (_ :>: ret) = distPerms1 ret (ValPerm_Eq e) typedStmtOut (TypedSetReg _ (TypedExpr _ Nothing)) (_ :>: ret) = distPerms1 ret ValPerm_True typedStmtOut (TypedSetRegPermExpr _ e) (_ :>: ret) = distPerms1 ret (ValPerm_Eq e) -typedStmtOut (TypedCall _ fun_perm ghosts gexprs args) (_ :>: ret) = - funPermDistOuts fun_perm (typedRegsToVars - ghosts) gexprs (typedRegsToVars args :>: ret) +typedStmtOut (TypedCall _ fun_perm ghosts gexprs args) rets = + funPermDistOuts fun_perm (typedRegsToVars ghosts) gexprs + (typedRegsToVars args) rets typedStmtOut (TypedAssert _ _) _ = DistPermsNil typedStmtOut (TypedLLVMStmt llvmStmt) (_ :>: ret) = typedLLVMStmtOut llvmStmt ret @@ -697,12 +710,12 @@ typedLLVMStmtOut (TypedLLVMIte _ _ (TypedReg x1) (TypedReg x2)) ret = -- | Check that the permission stack of the given permission set matches the -- input permissions of the given statement, and replace them with the output -- permissions of the statement -applyTypedStmt :: TypedStmt ext rets ps_in ps_out -> RAssign Name rets -> - PermSet ps_in -> PermSet ps_out -applyTypedStmt stmt rets = +applyTypedStmt :: TypedStmt ext stmt_rets ps_in ps_out -> + RAssign Name stmt_rets -> PermSet ps_in -> PermSet ps_out +applyTypedStmt stmt stmt_rets = modifyDistPerms $ \perms -> if perms == typedStmtIn stmt then - typedStmtOut stmt rets + typedStmtOut stmt stmt_rets else error "applyTypedStmt: unexpected input permissions!" @@ -716,73 +729,73 @@ applyTypedStmt stmt rets = data AnnotPermImpl r ps = AnnotPermImpl !String !(PermImpl r ps) -- | Typed return argument -data TypedRet tops ret ps = +data TypedRet tops rets ps = TypedRet - !(ps :~: tops :> ret) !(TypeRepr ret) !(TypedReg ret) - !(Binding ret (DistPerms ps)) + !(ps :~: tops :++: rets) !(CruCtx rets) !(RAssign ExprVar rets) + !(Mb rets (DistPerms ps)) -- | Typed Crucible block termination statements -data TypedTermStmt blocks tops ret ps_in where +data TypedTermStmt blocks tops rets ps_in where -- | Jump to the given jump target TypedJump :: !(AnnotPermImpl (TypedJumpTarget blocks tops) ps_in) -> - TypedTermStmt blocks tops ret ps_in + TypedTermStmt blocks tops rets ps_in -- | Branch on condition: if true, jump to the first jump target, and -- otherwise jump to the second jump target TypedBr :: !(TypedReg BoolType) -> !(AnnotPermImpl (TypedJumpTarget blocks tops) ps_in) -> !(AnnotPermImpl (TypedJumpTarget blocks tops) ps_in) -> - TypedTermStmt blocks tops ret ps_in + TypedTermStmt blocks tops rets ps_in -- | Return from function, providing the return value and also proof that the -- current permissions imply the required return permissions - TypedReturn :: !(AnnotPermImpl (TypedRet tops ret) ps_in) -> - TypedTermStmt blocks tops ret ps_in + TypedReturn :: !(AnnotPermImpl (TypedRet tops rets) ps_in) -> + TypedTermStmt blocks tops rets ps_in -- | Block ends with an error TypedErrorStmt :: !(Maybe String) -> !(TypedReg (StringType Unicode)) -> - TypedTermStmt blocks tops ret ps_in + TypedTermStmt blocks tops rets ps_in -- | A typed sequence of Crucible statements -data TypedStmtSeq ext blocks tops ret ps_in where +data TypedStmtSeq ext blocks tops rets ps_in where -- | A permission implication step, which modifies the current permission -- set. This can include pattern-matches and/or assertion failures. - TypedImplStmt :: !(AnnotPermImpl (TypedStmtSeq ext blocks tops ret) ps_in) -> - TypedStmtSeq ext blocks tops ret ps_in + TypedImplStmt :: !(AnnotPermImpl (TypedStmtSeq ext blocks tops rets) ps_in) -> + TypedStmtSeq ext blocks tops rets ps_in -- | Typed version of 'ConsStmt', which binds new variables for the return -- 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 + !(TypedStmt ext stmt_rets ps_in ps_next) -> + !(RAssign Proxy stmt_rets) -> + !(Mb stmt_rets (TypedStmtSeq ext blocks tops rets ps_next)) -> + TypedStmtSeq ext blocks tops rets ps_in -- | Typed version of 'TermStmt', which terminates the current block TypedTermStmt :: !ProgramLoc -> - !(TypedTermStmt blocks tops ret ps_in) -> - TypedStmtSeq ext blocks tops ret ps_in + !(TypedTermStmt blocks tops rets ps_in) -> + TypedStmtSeq ext blocks tops rets ps_in $(mkNuMatching [t| forall r ps. NuMatchingAny1 r => AnnotPermImpl r ps |]) $(mkNuMatching [t| forall tp ps_out ps_in. TypedLLVMStmt tp ps_out ps_in |]) -$(mkNuMatching [t| forall ext rets ps_in ps_out. NuMatchingExtC ext => - TypedStmt ext rets ps_in ps_out |]) -$(mkNuMatching [t| forall tops ret ps. TypedRet tops ret ps |]) +$(mkNuMatching [t| forall ext stmt_rets ps_in ps_out. NuMatchingExtC ext => + TypedStmt ext stmt_rets ps_in ps_out |]) +$(mkNuMatching [t| forall tops rets ps. TypedRet tops rets ps |]) -instance NuMatchingAny1 (TypedRet tops ret) where +instance NuMatchingAny1 (TypedRet tops rets) where nuMatchingAny1Proof = nuMatchingProof -$(mkNuMatching [t| forall blocks tops ret ps_in. - TypedTermStmt blocks tops ret ps_in |]) -$(mkNuMatching [t| forall ext blocks tops ret ps_in. - NuMatchingExtC ext => TypedStmtSeq ext blocks tops ret ps_in |]) +$(mkNuMatching [t| forall blocks tops rets ps_in. + TypedTermStmt blocks tops rets ps_in |]) +$(mkNuMatching [t| forall ext blocks tops rets ps_in. + NuMatchingExtC ext => TypedStmtSeq ext blocks tops rets ps_in |]) instance NuMatchingExtC ext => - NuMatchingAny1 (TypedStmtSeq ext blocks tops ret) where + NuMatchingAny1 (TypedStmtSeq ext blocks tops rets) where nuMatchingAny1Proof = nuMatchingProof @@ -982,12 +995,14 @@ instance (PermCheckExtC ext, SubstVar PermVarSubst m) => instance SubstVar PermVarSubst m => - Substable PermVarSubst (TypedRet tops ret ps) m where - genSubst s (mbMatch -> [nuMP| TypedRet e tp ret mb_perms |]) = - TypedRet (mbLift e) (mbLift tp) <$> genSubst s ret <*> genSubst s mb_perms + Substable PermVarSubst (TypedRet tops rets ps) m where + genSubst s (mbMatch -> [nuMP| TypedRet e rets ret_vars mb_perms |]) = + give (cruCtxProxies $ mbLift rets) + (TypedRet (mbLift e) (mbLift rets) <$> genSubst s ret_vars + <*> genSubst s mb_perms) instance SubstVar PermVarSubst m => - Substable1 PermVarSubst (TypedRet tops ret) m where + Substable1 PermVarSubst (TypedRet tops rets) m where genSubst1 = genSubst instance SubstVar PermVarSubst m => @@ -1001,7 +1016,7 @@ instance SubstVar PermVarSubst m => genSubst1 = genSubst instance SubstVar PermVarSubst m => - Substable PermVarSubst (TypedTermStmt blocks tops ret ps_in) m where + Substable PermVarSubst (TypedTermStmt blocks tops rets ps_in) m where genSubst s mb_x = case mbMatch mb_x of [nuMP| TypedJump impl_tgt |] -> TypedJump <$> genSubst s impl_tgt [nuMP| TypedBr reg impl_tgt1 impl_tgt2 |] -> @@ -1013,18 +1028,19 @@ instance SubstVar PermVarSubst m => TypedErrorStmt (mbLift str) <$> genSubst s r instance (PermCheckExtC ext, SubstVar PermVarSubst m) => - Substable PermVarSubst (TypedStmtSeq ext blocks tops ret ps_in) m where + Substable PermVarSubst (TypedStmtSeq ext blocks tops rets ps_in) m where genSubst s mb_x = case mbMatch mb_x of [nuMP| TypedImplStmt impl_seq |] -> TypedImplStmt <$> genSubst s impl_seq [nuMP| TypedConsStmt loc stmt pxys mb_seq |] -> - TypedConsStmt (mbLift loc) <$> genSubst s stmt <*> pure (mbLift pxys) <*> give (mbLift pxys) (genSubst s 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 + Substable1 PermVarSubst (TypedStmtSeq ext blocks tops rets) m where genSubst1 = genSubst @@ -1185,7 +1201,7 @@ typedCallSiteArgVarPerms (TypedCallSite {..}) = -- implicitly take extra "ghost" arguments, that are needed to express the input -- and output permissions. The first of these ghost arguments are the top-level -- inputs to the entire function. -data TypedEntry phase ext blocks tops ret args ghosts = +data TypedEntry phase ext blocks tops rets args ghosts = TypedEntry { -- | The identifier for this particular entrypoing @@ -1194,8 +1210,8 @@ data TypedEntry phase ext blocks tops ret args ghosts = typedEntryTops :: !(CruCtx tops), -- | The real arguments to this block typedEntryArgs :: !(CruCtx args), - -- | The return value from the entire function - typedEntryRet :: !(TypeRepr ret), + -- | The return values (including ghosts) from the entire function + typedEntryRets :: !(CruCtx rets), -- | The call sites that jump to this particular entrypoint typedEntryCallers :: ![Some (TypedCallSite phase blocks tops args ghosts)], -- | The ghost variables for this entrypoint @@ -1203,21 +1219,21 @@ data TypedEntry phase ext blocks tops ret args ghosts = -- | The input permissions for this entrypoint typedEntryPermsIn :: !(MbValuePerms ((tops :++: args) :++: ghosts)), -- | The output permissions for the function (cached locally) - typedEntryPermsOut :: !(MbValuePerms (tops :> ret)), + typedEntryPermsOut :: !(MbValuePerms (tops :++: rets)), -- | The type-checked body of the entrypoint typedEntryBody :: !(TransData phase (Mb ((tops :++: args) :++: ghosts) - (TypedStmtSeq ext blocks tops ret + (TypedStmtSeq ext blocks tops rets ((tops :++: args) :++: ghosts)))) } -- | Test if an entrypoint has in-degree greater than 1 -typedEntryHasMultiInDegree :: TypedEntry phase ext blocks tops ret args ghosts -> +typedEntryHasMultiInDegree :: TypedEntry phase ext blocks tops rets args ghosts -> Bool typedEntryHasMultiInDegree entry = length (typedEntryCallers entry) > 1 -- | Get the types of all the inputs of an entrypoint -typedEntryAllArgs :: TypedEntry phase ext blocks tops ret args ghosts -> +typedEntryAllArgs :: TypedEntry phase ext blocks tops rets args ghosts -> CruCtx ((tops :++: args) :++: ghosts) typedEntryAllArgs (TypedEntry {..}) = appendCruCtx (appendCruCtx typedEntryTops typedEntryArgs) typedEntryGhosts @@ -1225,8 +1241,8 @@ typedEntryAllArgs (TypedEntry {..}) = -- | Transition a 'TypedEntry' from type-checking to translation phase if its -- body is present and all call site implications have been proved completeTypedEntry :: - TypedEntry TCPhase ext blocks tops ret args ghosts -> - Maybe (TypedEntry TransPhase ext blocks tops ret args ghosts) + TypedEntry TCPhase ext blocks tops rets args ghosts -> + Maybe (TypedEntry TransPhase ext blocks tops rets args ghosts) completeTypedEntry (TypedEntry { .. }) | Just body <- typedEntryBody , Just callers <- mapM (traverseF completeTypedCallSite) typedEntryCallers @@ -1236,15 +1252,15 @@ completeTypedEntry _ = Nothing -- | Build an entrypoint from a call site, using that call site's permissions as -- the entyrpoint input permissions singleCallSiteEntry :: TypedCallSiteID blocks args vars -> - CruCtx tops -> CruCtx args -> TypeRepr ret -> + CruCtx tops -> CruCtx args -> CruCtx rets -> MbValuePerms ((tops :++: args) :++: vars) -> - MbValuePerms (tops :> ret) -> - TypedEntry TCPhase ext blocks tops ret args vars -singleCallSiteEntry siteID tops args ret perms_in perms_out = + MbValuePerms (tops :++: rets) -> + TypedEntry TCPhase ext blocks tops rets args vars +singleCallSiteEntry siteID tops args rets perms_in perms_out = TypedEntry { typedEntryID = callSiteDest siteID, typedEntryTops = tops, - typedEntryArgs = args, typedEntryRet = ret, + typedEntryArgs = args, typedEntryRets = rets, typedEntryCallers = [Some $ idTypedCallSite siteID tops args perms_in], typedEntryGhosts = callSiteVars siteID, typedEntryPermsIn = perms_in, typedEntryPermsOut = perms_out, @@ -1253,7 +1269,7 @@ singleCallSiteEntry siteID tops args ret perms_in perms_out = -- | Test if an entrypoint contains a call site with the given caller typedEntryHasCaller :: TypedEntryID blocks args_src -> - TypedEntry phase ext blocks tops ret args ghosts -> + TypedEntry phase ext blocks tops rets args ghosts -> Bool typedEntryHasCaller callerID (typedEntryCallers -> callers) = any (\(Some site) -> @@ -1264,7 +1280,7 @@ typedEntryHasCaller callerID (typedEntryCallers -> callers) = -- id to have the same variables. typedEntryCallerSite :: TypedCallSiteID blocks args vars -> - TypedEntry phase ext blocks tops ret args ghosts -> + TypedEntry phase ext blocks tops rets args ghosts -> Maybe (TypedCallSite phase blocks tops args ghosts vars) typedEntryCallerSite siteID (typedEntryCallers -> callers) = listToMaybe $ flip mapMaybe callers $ \(Some site) -> @@ -1279,8 +1295,8 @@ typedEntryCallerSite siteID (typedEntryCallers -> callers) = data TypedBlockSort = JoinSort | MultiEntrySort -- | A typed Crucible block is a list of typed entrypoints to that block -data TypedBlock phase ext (blocks :: RList (RList CrucibleType)) tops ret args = - forall cargs. (CtxToRList cargs ~ args) => +data TypedBlock phase ext (blocks :: RList (RList CrucibleType)) tops rets args = + forall gouts ret cargs. (CtxToRList cargs ~ args, rets ~ (gouts :> ret)) => TypedBlock { -- | An identifier for this block @@ -1293,21 +1309,35 @@ data TypedBlock phase ext (blocks :: RList (RList CrucibleType)) tops ret args = -- disallowed for user-supplied permissions typedBlockCanWiden :: Bool, -- | The entrypoints into this block - _typedBlockEntries :: [Some (TypedEntry phase ext blocks tops ret args)], + _typedBlockEntries :: [Some (TypedEntry phase ext blocks tops rets args)], -- | Debug name information for the current block _typedBlockNames :: [Maybe String] } -makeLenses ''TypedBlock +-- NOTE: this doesn't work because of the rets ~ (gouts :> ret) constraint +-- makeLenses ''TypedBlock + +-- | The lens for '_typedBlockEntries' +typedBlockEntries :: Lens' (TypedBlock phase ext blocks tops rets args) + [Some (TypedEntry phase ext blocks tops rets args)] +typedBlockEntries = + lens _typedBlockEntries (\tblk entries -> + tblk { _typedBlockEntries = entries }) + +-- | The lens for '_typedBlockNames' +typedBlockNames :: Lens' (TypedBlock phase ext blocks tops rets args) + [Maybe String] +typedBlockNames = + lens _typedBlockNames (\tblk ns -> tblk { _typedBlockNames = ns }) -- | The input argument types of a block -blockArgs :: TypedBlock phase ext blocks tops ret args -> CruCtx args +blockArgs :: TypedBlock phase ext blocks tops rets args -> CruCtx args blockArgs (TypedBlock {..}) = mkCruCtx $ blockInputs typedBlockBlock -- | Get the 'Int' index of the location of entrypoint in the -- 'typedBlockEntries' of a block, if it exists blockEntryMaybeIx :: TypedEntryID blocks args -> - TypedBlock phase ext blocks tops ret args -> + TypedBlock phase ext blocks tops rets args -> Maybe Int blockEntryMaybeIx entryID blk = findIndex (\(Some entry) -> entryID == typedEntryID entry) @@ -1316,7 +1346,7 @@ blockEntryMaybeIx entryID blk = -- | Get the 'Int' index of the location of entrypoint in the -- 'typedBlockEntries' of a block, or raise an error if it does not exist blockEntryIx :: TypedEntryID blocks args -> - TypedBlock phase ext blocks tops ret args -> + TypedBlock phase ext blocks tops rets args -> Int blockEntryIx entryID blk = maybe (error "blockEntryIx: no such entrypoint!") id $ @@ -1324,7 +1354,7 @@ blockEntryIx entryID blk = -- | Test if an entrypoint ID has a corresponding entrypoint in a block entryIDInBlock :: TypedEntryID blocks args -> - TypedBlock phase ext blocks tops ret args -> Bool + TypedBlock phase ext blocks tops rets args -> Bool entryIDInBlock entryID blk = isJust $ blockEntryMaybeIx entryID blk -- | The 'Lens' for finding a 'TypedEntry' by id in a 'TypedBlock' @@ -1344,8 +1374,8 @@ emptyBlockOfSort :: Assignment CtxRepr cblocks -> TypedBlockSort -> Block ext cblocks ret cargs -> - TypedBlock TCPhase ext (CtxCtxToRList - cblocks) tops ret (CtxToRList cargs) + TypedBlock TCPhase ext (CtxCtxToRList cblocks) tops (gouts :> ret) (CtxToRList + cargs) emptyBlockOfSort names cblocks sort blk | Refl <- reprReprToCruCtxCtxEq cblocks = TypedBlock (indexToTypedBlockID (size cblocks) $ @@ -1356,19 +1386,19 @@ emptyBlockForPerms :: [Maybe String] -> Assignment CtxRepr cblocks -> Block ext cblocks ret cargs -> CruCtx tops -> - TypeRepr ret -> CruCtx ghosts -> + TypeRepr ret -> CruCtx ghosts -> CruCtx gouts -> MbValuePerms ((tops :++: CtxToRList cargs) :++: ghosts) -> - MbValuePerms (tops :> ret) -> + MbValuePerms (tops :++: gouts :> ret) -> TypedBlock TCPhase ext (CtxCtxToRList - cblocks) tops ret (CtxToRList cargs) -emptyBlockForPerms names cblocks blk tops ret ghosts perms_in perms_out + cblocks) tops (gouts :> ret) (CtxToRList cargs) +emptyBlockForPerms names cblocks blk tops ret ghosts gouts perms_in perms_out | Refl <- reprReprToCruCtxCtxEq cblocks , blockID <- indexToTypedBlockID (size cblocks) $ blockIDIndex $ blockID blk , args <- mkCruCtx (blockInputs blk) = TypedBlock blockID blk JoinSort False [Some TypedEntry { typedEntryID = TypedEntryID blockID 0, typedEntryTops = tops, - typedEntryArgs = args, typedEntryRet = ret, + typedEntryArgs = args, typedEntryRets = CruCtxCons gouts ret, typedEntryCallers = [], typedEntryGhosts = ghosts, typedEntryPermsIn = perms_in, typedEntryPermsOut = perms_out, typedEntryBody = Nothing }] @@ -1376,8 +1406,8 @@ emptyBlockForPerms names cblocks blk tops ret ghosts perms_in perms_out -- | Transition a 'TypedBlock' from type-checking to translation phase, by -- making sure that all of data needed for the translation phase is present -completeTypedBlock :: TypedBlock TCPhase ext blocks tops ret args -> - Maybe (TypedBlock TransPhase ext blocks tops ret args) +completeTypedBlock :: TypedBlock TCPhase ext blocks tops rets args -> + Maybe (TypedBlock TransPhase ext blocks tops rets args) completeTypedBlock (TypedBlock { .. }) | Just entries <- mapM (traverseF completeTypedEntry) _typedBlockEntries = Just $ TypedBlock { _typedBlockEntries = entries, .. } @@ -1385,9 +1415,9 @@ completeTypedBlock _ = Nothing -- | Add a new entrypoint to a block, making sure that its entry ID does not -- already exist in the block -addEntryToBlock :: TypedEntry phase ext blocks tops ret args ghosts -> - TypedBlock phase ext blocks tops ret args -> - TypedBlock phase ext blocks tops ret args +addEntryToBlock :: TypedEntry phase ext blocks tops rets args ghosts -> + TypedBlock phase ext blocks tops rets args -> + TypedBlock phase ext blocks tops rets args addEntryToBlock entry blk | entryIDInBlock (typedEntryID entry) blk = error "addEntryToBlock: entry with the same ID already in block!" @@ -1403,7 +1433,7 @@ freshInt xs = 1 + maximum xs -- entrypoint for that block, and otherwise, for a 'MultiEntrySort' block, it -- will create a new entrypoint id. newCallSiteID :: TypedEntryID blocks args_src -> CruCtx vars -> - TypedBlock phase ext blocks tops ret args -> + TypedBlock phase ext blocks tops rets args -> TypedCallSiteID blocks args vars -- If blk has JoinSort but has no entrypoints yet, we will create one. It cannot @@ -1441,8 +1471,8 @@ newCallSiteID _ _ _ = error "newCallSiteID: impossible case!" -- has a call site with the given call site id. entryAddCallSite :: TypedCallSiteID blocks args vars -> MbValuePerms ((tops :++: args) :++: vars) -> - TypedEntry TCPhase ext blocks tops ret args ghosts -> - TypedEntry TCPhase ext blocks tops ret args ghosts + TypedEntry TCPhase ext blocks tops rets args ghosts -> + TypedEntry TCPhase ext blocks tops rets args ghosts entryAddCallSite siteID _ entry | any (\(Some site) -> isJust $ testEquality (typedCallSiteID site) siteID) @@ -1458,11 +1488,11 @@ entryAddCallSite siteID perms_in entry = -- the given call site ID does not yet exist. It is an error if the block -- already has a call site with the given call site id. blockAddCallSite :: TypedCallSiteID blocks args vars -> - CruCtx tops -> TypeRepr ret -> + CruCtx tops -> CruCtx rets -> MbValuePerms ((tops :++: args) :++: vars) -> - MbValuePerms (tops :> ret) -> - TypedBlock TCPhase ext blocks tops ret args -> - TypedBlock TCPhase ext blocks tops ret args + MbValuePerms (tops :++: rets) -> + TypedBlock TCPhase ext blocks tops rets args -> + TypedBlock TCPhase ext blocks tops rets args -- If the entrypoint for the site ID exists, update it with entrySetCallSite blockAddCallSite siteID _ _ perms_in _ blk | Just _ <- blockEntryMaybeIx (callSiteDest siteID) blk = @@ -1472,49 +1502,49 @@ blockAddCallSite siteID _ _ perms_in _ blk blk -- Otherwise, make a new entrypoint -blockAddCallSite siteID tops ret perms_in perms_out blk = +blockAddCallSite siteID tops rets perms_in perms_out blk = addEntryToBlock (singleCallSiteEntry - siteID tops (blockArgs blk) ret perms_in perms_out) blk + siteID tops (blockArgs blk) rets perms_in perms_out) blk -- | A map assigning a 'TypedBlock' to each 'BlockID' -type TypedBlockMap phase ext blocks tops ret = - RAssign (TypedBlock phase ext blocks tops ret) blocks +type TypedBlockMap phase ext blocks tops rets = + RAssign (TypedBlock phase ext blocks tops rets) blocks -instance Show (TypedEntry phase ext blocks tops ret args ghosts) where +instance Show (TypedEntry phase ext blocks tops rets args ghosts) where show (TypedEntry { .. }) = "" -instance Show (TypedBlock phase ext blocks tops ret args) where +instance Show (TypedBlock phase ext blocks tops rets args) where show = concatMap (\(Some entry) -> show entry) . (^. typedBlockEntries) -instance Show (TypedBlockMap phase ext blocks tops ret) where +instance Show (TypedBlockMap phase ext blocks tops rets) where show blkMap = show $ RL.mapToList show blkMap -- | Transition a 'TypedBlockMap' from type-checking to translation phase, by -- making sure that all of data needed for the translation phase is present -completeTypedBlockMap :: TypedBlockMap TCPhase ext blocks tops ret -> - Maybe (TypedBlockMap TransPhase ext blocks tops ret) +completeTypedBlockMap :: TypedBlockMap TCPhase ext blocks tops rets -> + Maybe (TypedBlockMap TransPhase ext blocks tops rets) completeTypedBlockMap = traverseRAssign completeTypedBlock -- | The 'Lens' for finding a 'TypedBlock' by id in a 'TypedBlockMap' blockByID :: TypedBlockID blocks args -> Lens' - (TypedBlockMap phase ext blocks tops ret) - (TypedBlock phase ext blocks tops ret args) + (TypedBlockMap phase ext blocks tops rets) + (TypedBlock phase ext blocks tops rets args) blockByID blkID = let memb = typedBlockIDMember blkID in lens (RL.get memb) (flip $ RL.set memb) -- | Look up a 'TypedEntry' by its 'TypedEntryID' lookupEntry :: TypedEntryID blocks args -> - TypedBlockMap phase ext blocks tops ret -> - Some (TypedEntry phase ext blocks tops ret args) + TypedBlockMap phase ext blocks tops rets -> + Some (TypedEntry phase ext blocks tops rets args) lookupEntry entryID = view (blockByID (entryBlockID entryID) . entryByID entryID) -- | Find all call sites called by an entrypoint entryCallees :: TypedEntryID blocks args -> - TypedBlockMap phase ext blocks tops ret -> + TypedBlockMap phase ext blocks tops rets -> [Some (TypedEntryID blocks)] entryCallees entryID = concat . RL.mapToList @@ -1528,12 +1558,12 @@ entryCallees entryID = -- sites to entrypoints in multi-entry blocks, delete those entrypoints as well, -- etc. deleteEntryCallees :: TypedEntryID blocks args -> - TypedBlockMap phase ext blocks tops ret -> - TypedBlockMap phase ext blocks tops ret + TypedBlockMap phase ext blocks tops rets -> + TypedBlockMap phase ext blocks tops rets deleteEntryCallees topEntryID = execState (deleteCallees topEntryID) where -- Delete call sites of a caller from all of its callees deleteCallees :: TypedEntryID blocks args' -> - State (TypedBlockMap phase ext blocks tops ret) () + State (TypedBlockMap phase ext blocks tops rets) () deleteCallees callerID = get >>= \blkMap -> mapM_ (\(Some calleeID) -> @@ -1541,7 +1571,7 @@ deleteEntryCallees topEntryID = execState (deleteCallees topEntryID) where -- Delete call sites of a caller to a particular callee deleteCall :: TypedEntryID blocks args1 -> TypedEntryID blocks args2 -> - State (TypedBlockMap phase ext blocks tops ret) () + State (TypedBlockMap phase ext blocks tops rets) () deleteCall callerID calleeID = (typedBlockSort <$> use (blockByID $ entryBlockID calleeID)) >>= \case JoinSort -> @@ -1566,7 +1596,7 @@ deleteEntryCallees topEntryID = execState (deleteCallees topEntryID) where -- arguments of the function permission) get the function input permissions and -- the normal arguments get equality permissions to their respective top-level -- variables. -funPermToBlockInputs :: FunPerm ghosts args ret -> +funPermToBlockInputs :: FunPerm ghosts args gouts ret -> MbValuePerms ((ghosts :++: args) :++: args) funPermToBlockInputs fun_perm = let args_prxs = cruCtxProxies $ funPermArgs fun_perm in @@ -1583,15 +1613,16 @@ funPermToBlockInputs fun_perm = initTypedBlockMap :: KnownRepr ExtRepr ext => PermEnv -> - FunPerm ghosts (CtxToRList init) ret -> + FunPerm ghosts (CtxToRList init) gouts ret -> CFG ext cblocks init ret -> Assignment (Constant Bool) cblocks -> TypedBlockMap TCPhase ext (CtxCtxToRList cblocks) - (ghosts :++: CtxToRList init) ret + (ghosts :++: CtxToRList init) (gouts :> ret) initTypedBlockMap env fun_perm cfg sccs = let block_map = cfgBlockMap cfg cblocks = fmapFC blockInputs block_map namess = computeCfgNames knownRepr (size sccs) cfg + gouts = funPermGouts fun_perm ret = funPermRet fun_perm tops = funPermTops fun_perm top_perms_in = funPermToBlockInputs fun_perm @@ -1602,11 +1633,13 @@ initTypedBlockMap env fun_perm cfg sccs = hints = lookupBlockHints env (cfgHandle cfg) cblocks blkID in case hints of _ | Just Refl <- testEquality (cfgEntryBlockID cfg) blkID -> - emptyBlockForPerms names cblocks blk tops ret CruCtxNil top_perms_in perms_out + emptyBlockForPerms names cblocks blk tops ret + CruCtxNil gouts top_perms_in perms_out (find isBlockEntryHint -> Just (BlockEntryHintSort tops' ghosts perms_in)) | Just Refl <- testEquality tops tops' -> - emptyBlockForPerms names cblocks blk tops ret ghosts perms_in perms_out + emptyBlockForPerms names cblocks blk tops ret + ghosts gouts perms_in perms_out _ | is_scc || any isJoinPointHint hints -> emptyBlockOfSort names cblocks JoinSort blk _ -> emptyBlockOfSort names cblocks MultiEntrySort blk) $ @@ -1626,22 +1659,23 @@ data TypedCFG (blocks :: RList (RList CrucibleType)) (ghosts :: RList CrucibleType) (inits :: RList CrucibleType) + (gouts :: RList CrucibleType) (ret :: CrucibleType) - = TypedCFG { tpcfgHandle :: !(TypedFnHandle ghosts inits ret) - , tpcfgFunPerm :: !(FunPerm ghosts inits ret) - , tpcfgBlockMap :: - !(TypedBlockMap TransPhase ext blocks (ghosts :++: inits) ret) + = TypedCFG { tpcfgHandle :: !(TypedFnHandle ghosts inits gouts ret) + , tpcfgFunPerm :: !(FunPerm ghosts inits gouts ret) + , tpcfgBlockMap :: !(TypedBlockMap TransPhase ext blocks + (ghosts :++: inits) (gouts :> ret)) , tpcfgEntryID :: !(TypedEntryID blocks inits) } -- | Get the input permissions for a 'CFG' -tpcfgInputPerms :: TypedCFG ext blocks ghosts inits ret -> +tpcfgInputPerms :: TypedCFG ext blocks ghosts inits gouts ret -> MbValuePerms (ghosts :++: inits) tpcfgInputPerms = funPermIns . tpcfgFunPerm -- | Get the output permissions for a 'CFG' -tpcfgOutputPerms :: TypedCFG ext blocks ghosts inits ret -> - MbValuePerms (ghosts :++: inits :> ret) +tpcfgOutputPerms :: TypedCFG ext blocks ghosts inits gouts ret -> + MbValuePerms ((ghosts :++: inits) :++: gouts :> ret) tpcfgOutputPerms = funPermOuts . tpcfgFunPerm @@ -1677,19 +1711,19 @@ buildBlockIDMap sz = data SomePtrWidth where SomePtrWidth :: HasPtrWidth w => SomePtrWidth -- | Top-level state, maintained outside of permission-checking single blocks -data TopPermCheckState ext cblocks blocks tops ret = +data TopPermCheckState ext cblocks blocks tops rets = TopPermCheckState { -- | The top-level inputs of the function being type-checked stTopCtx :: !(CruCtx tops), - -- | The return type of the function being type-checked - stRetType :: !(TypeRepr ret), + -- | The return types including ghosts of the function being type-checked + stRetTypes :: !(CruCtx rets), -- | The return permission of the function being type-checked - stRetPerms :: !(MbValuePerms (tops :> ret)), + stRetPerms :: !(MbValuePerms (tops :++: rets)), -- | A mapping from 'BlockID's to 'TypedBlockID's stBlockTrans :: !(Assignment (BlockIDTrans blocks) cblocks), -- | The current set of type-checked blocks - _stBlockMap :: !(TypedBlockMap TCPhase ext blocks tops ret), + _stBlockMap :: !(TypedBlockMap TCPhase ext blocks tops rets), -- | The permissions environment stPermEnv :: !PermEnv, -- | The un-translated input types of all of the Crucible blocks @@ -1715,19 +1749,19 @@ emptyTopPermCheckState :: HasPtrWidth w => KnownRepr ExtRepr ext => PermEnv -> - FunPerm ghosts (CtxToRList init) ret -> + FunPerm ghosts (CtxToRList init) gouts ret -> EndianForm -> DebugLevel -> CFG ext cblocks init ret -> Assignment (Constant Bool) cblocks -> TopPermCheckState ext cblocks (CtxCtxToRList cblocks) - (ghosts :++: CtxToRList init) ret + (ghosts :++: CtxToRList init) (gouts :> ret) emptyTopPermCheckState env fun_perm endianness dlevel cfg sccs = let blkMap = cfgBlockMap cfg in TopPermCheckState { stTopCtx = funPermTops fun_perm - , stRetType = funPermRet fun_perm + , stRetTypes = funPermRets fun_perm , stRetPerms = funPermOuts fun_perm , stBlockTrans = buildBlockIDMap (Ctx.size blkMap) , _stBlockMap = initTypedBlockMap env fun_perm cfg sccs @@ -1742,14 +1776,14 @@ emptyTopPermCheckState env fun_perm endianness dlevel cfg sccs = -- | Look up a Crucible block id in a top-level perm-checking state stLookupBlockID :: BlockID cblocks args -> - TopPermCheckState ext cblocks blocks tops ret -> + TopPermCheckState ext cblocks blocks tops rets -> TypedBlockID blocks (CtxToRList args) stLookupBlockID (BlockID ix) st = unBlockIDTrans $ stBlockTrans st Ctx.! ix -- | The top-level monad for permission-checking CFGs -type TopPermCheckM ext cblocks blocks tops ret = - State (TopPermCheckState ext cblocks blocks tops ret) +type TopPermCheckM ext cblocks blocks tops rets = + State (TopPermCheckState ext cblocks blocks tops rets) {- -- | A datakind for the type-level parameters needed to define blocks, including @@ -1773,54 +1807,54 @@ type family BlkArgs (args :: BlkParams) :: RList CrucibleType where -- | A change to a 'TypedBlockMap' -data TypedBlockMapDelta blocks tops ret where +data TypedBlockMapDelta blocks tops rets where -- | Add a call site to a block for a particular caller to have the supplied -- permissions over the supplied variables TypedBlockMapAddCallSite :: TypedCallSiteID blocks args vars -> MbValuePerms ((tops :++: args) :++: vars) -> - TypedBlockMapDelta blocks tops ret + TypedBlockMapDelta blocks tops rets -- | Apply a 'TypedBlockMapDelta' to a 'TypedBlockMap' -applyTypedBlockMapDelta :: TypedBlockMapDelta blocks tops ret -> - TopPermCheckState ext cblocks blocks tops ret -> - TopPermCheckState ext cblocks blocks tops ret +applyTypedBlockMapDelta :: TypedBlockMapDelta blocks tops rets -> + TopPermCheckState ext cblocks blocks tops rets -> + TopPermCheckState ext cblocks blocks tops rets applyTypedBlockMapDelta (TypedBlockMapAddCallSite siteID perms_in) top_st = over (stBlockMap . member (entryBlockMember $ callSiteDest siteID)) - (blockAddCallSite siteID (stTopCtx top_st) (stRetType top_st) + (blockAddCallSite siteID (stTopCtx top_st) (stRetTypes top_st) perms_in (stRetPerms top_st)) top_st -- | Apply a list of 'TypedBlockMapDelta's to a 'TopPermCheckState' -applyDeltasToTopState :: [TypedBlockMapDelta blocks tops ret] -> - TopPermCheckState ext cblocks blocks tops ret -> - TopPermCheckState ext cblocks blocks tops ret +applyDeltasToTopState :: [TypedBlockMapDelta blocks tops rets] -> + TopPermCheckState ext cblocks blocks tops rets -> + TopPermCheckState ext cblocks blocks tops rets applyDeltasToTopState deltas top_st = foldl (flip applyTypedBlockMapDelta) top_st deltas -- | The state that can be modified by "inner" computations = a list of changes -- / "deltas" to the current 'TypedBlockMap' -data InnerPermCheckState blocks tops ret = +data InnerPermCheckState blocks tops rets = InnerPermCheckState { - innerStateDeltas :: [TypedBlockMapDelta blocks tops ret] + innerStateDeltas :: [TypedBlockMapDelta blocks tops rets] } -- | Build an empty, closed 'InnerPermCheckState' -clEmptyInnerPermCheckState :: Closed (InnerPermCheckState blocks tops ret) +clEmptyInnerPermCheckState :: Closed (InnerPermCheckState blocks tops rets) clEmptyInnerPermCheckState = $(mkClosed [| InnerPermCheckState [] |]) -- | The "inner" monad that runs inside 'PermCheckM' continuations. It can see -- but not modify the top-level state, but it can add 'TypedBlockMapDelta's to -- be applied later to the top-level state. -type InnerPermCheckM ext cblocks blocks tops ret = - ReaderT (TopPermCheckState ext cblocks blocks tops ret) - (State (Closed (InnerPermCheckState blocks tops ret))) +type InnerPermCheckM ext cblocks blocks tops rets = + ReaderT (TopPermCheckState ext cblocks blocks tops rets) + (State (Closed (InnerPermCheckState blocks tops rets))) -- | The local state maintained while type-checking is the current permission -- set and the permissions required on return from the entire function. -data PermCheckState ext blocks tops ret ps = +data PermCheckState ext blocks tops rets ps = PermCheckState { stCurPerms :: !(PermSet ps), @@ -1840,7 +1874,7 @@ emptyPermCheckState :: RAssign ExprVar tops -> TypedEntryID blocks args -> [Maybe String] -> - PermCheckState ext blocks tops ret ps + PermCheckState ext blocks tops rets ps emptyPermCheckState perms tops entryID names = PermCheckState { stCurPerms = perms, stExtState = emptyPermCheckExtState knownRepr, @@ -1852,45 +1886,43 @@ emptyPermCheckState perms tops entryID names = stDebug = names } -- | Like the 'set' method of a lens, but allows the @ps@ argument to change -setSTCurPerms :: PermSet ps2 -> PermCheckState ext blocks tops ret ps1 -> - PermCheckState ext blocks tops ret ps2 +setSTCurPerms :: PermSet ps2 -> PermCheckState ext blocks tops rets ps1 -> + PermCheckState ext blocks tops rets ps2 setSTCurPerms perms (PermCheckState {..}) = PermCheckState { stCurPerms = perms, .. } modifySTCurPerms :: (PermSet ps1 -> PermSet ps2) -> - PermCheckState ext blocks tops ret ps1 -> - PermCheckState ext blocks tops ret ps2 + PermCheckState ext blocks tops rets ps1 -> + PermCheckState ext blocks tops rets ps2 modifySTCurPerms f_perms st = setSTCurPerms (f_perms $ stCurPerms st) st -nextDebugName :: - PermCheckM ext cblocks blocks tops ret a ps a ps - (Maybe String) +nextDebugName :: PermCheckM ext cblocks blocks tops rets a ps a ps (Maybe String) nextDebugName = do st <- get put st { stDebug = drop 1 (stDebug st)} pure (foldr (\x _ -> x) Nothing (stDebug st)) -- | The generalized monad for permission-checking -type PermCheckM ext cblocks blocks tops ret r1 ps1 r2 ps2 = +type PermCheckM ext cblocks blocks tops rets r1 ps1 r2 ps2 = GenStateContT - (PermCheckState ext blocks tops ret ps1) r1 - (PermCheckState ext blocks tops ret ps2) r2 - (InnerPermCheckM ext cblocks blocks tops ret) + (PermCheckState ext blocks tops rets ps1) r1 + (PermCheckState ext blocks tops rets ps2) r2 + (InnerPermCheckM ext cblocks blocks tops rets) -- | The generalized monad for permission-checking statements -type StmtPermCheckM ext cblocks blocks tops ret ps1 ps2 = - PermCheckM ext cblocks blocks tops ret - (TypedStmtSeq ext blocks tops ret ps1) ps1 - (TypedStmtSeq ext blocks tops ret ps2) ps2 +type StmtPermCheckM ext cblocks blocks tops rets ps1 ps2 = + PermCheckM ext cblocks blocks tops rets + (TypedStmtSeq ext blocks tops rets ps1) ps1 + (TypedStmtSeq ext blocks tops rets ps2) ps2 -- | Lift an 'InnerPermCheckM' computation to a 'PermCheckM' computation -liftPermCheckM :: InnerPermCheckM ext cblocks blocks tops ret a -> - PermCheckM ext cblocks blocks tops ret r ps r ps a +liftPermCheckM :: InnerPermCheckM ext cblocks blocks tops rets a -> + PermCheckM ext cblocks blocks tops rets r ps r ps a liftPermCheckM = lift -- | Lift an 'InnerPermCheckM' to a 'TopPermCheckM' -liftInnerToTopM :: InnerPermCheckM ext cblocks blocks tops ret a -> - TopPermCheckM ext cblocks blocks tops ret a +liftInnerToTopM :: InnerPermCheckM ext cblocks blocks tops rets a -> + TopPermCheckM ext cblocks blocks tops rets a liftInnerToTopM m = do st <- get let (a, cl_inner_st) = @@ -1901,8 +1933,8 @@ liftInnerToTopM m = -- | Get the current top-level state modulo the modifications to the current -- block info map -top_get :: PermCheckM ext cblocks blocks tops ret r ps r ps - (TopPermCheckState ext cblocks blocks tops ret) +top_get :: PermCheckM ext cblocks blocks tops rets r ps r ps + (TopPermCheckState ext cblocks blocks tops rets) top_get = gcaptureCC $ \k -> do top_st <- ask deltas <- innerStateDeltas <$> unClosed <$> get @@ -1910,7 +1942,7 @@ top_get = gcaptureCC $ \k -> -- | Set the extension-specific state setInputExtState :: ExtRepr ext -> CruCtx as -> RAssign Name as -> - PermCheckM ext cblocks blocks tops ret r ps r ps () + PermCheckM ext cblocks blocks tops rets r ps r ps () setInputExtState ExtRepr_Unit _ _ = pure () setInputExtState ExtRepr_LLVM tps ns | [SomeExprVarFrame rep n] <- findLLVMFrameVars tps ns @@ -1930,9 +1962,9 @@ runPermCheckM :: CruCtx args -> CruCtx ghosts -> MbValuePerms ((tops :++: args) :++: ghosts) -> (RAssign ExprVar tops -> RAssign ExprVar args -> RAssign ExprVar ghosts -> DistPerms ((tops :++: args) :++: ghosts) -> - PermCheckM ext cblocks blocks tops ret () ps_out r ((tops :++: args) - :++: ghosts) ()) -> - TopPermCheckM ext cblocks blocks tops ret (Mb ((tops :++: args) :++: ghosts) r) + PermCheckM ext cblocks blocks tops rets () ps_out r ((tops :++: args) + :++: ghosts) ()) -> + TopPermCheckM ext cblocks blocks tops rets (Mb ((tops :++: args) :++: ghosts) r) runPermCheckM names entryID args ghosts mb_perms_in m = get >>= \(TopPermCheckState {..}) -> let args_prxs = cruCtxProxies args @@ -1985,7 +2017,7 @@ noNames' (CruCtxCons xs _) = noNames' xs :>: Constant Nothing -- | Call 'debugNames'' with a known type list. dbgNames :: KnownRepr CruCtx tps => - PermCheckM ext cblocks blocks tops ret a ps a ps + PermCheckM ext cblocks blocks tops rets a ps a ps (RAssign (Constant (Maybe String)) tps) dbgNames = dbgNames' knownRepr @@ -1993,7 +2025,7 @@ dbgNames = dbgNames' knownRepr -- as needed to populate the given type list. dbgNames' :: CruCtx tps -> - PermCheckM ext cblocks blocks tops ret a ps a ps + PermCheckM ext cblocks blocks tops rets a ps a ps (RAssign (Constant (Maybe String)) tps) dbgNames' CruCtxNil = pure MNil dbgNames' (CruCtxCons ts _) = @@ -2003,8 +2035,8 @@ dbgNames' (CruCtxCons ts _) = -- | Emit a 'TypedBlockMapDelta', which must be 'Closed', in an -- 'InnerPermCheckM' computation -innerEmitDelta :: Closed (TypedBlockMapDelta blocks tops ret) -> - InnerPermCheckM ext cblocks blocks tops ret () +innerEmitDelta :: Closed (TypedBlockMapDelta blocks tops rets) -> + InnerPermCheckM ext cblocks blocks tops rets () innerEmitDelta cl_delta = modify (clApply ($(mkClosed [| \delta st -> @@ -2017,7 +2049,7 @@ innerEmitDelta cl_delta = callBlockWithPerms :: TypedEntryID blocks args_src -> TypedBlockID blocks args -> CruCtx vars -> Closed (MbValuePerms ((tops :++: args) :++: vars)) -> - InnerPermCheckM ext cblocks blocks tops ret + InnerPermCheckM ext cblocks blocks tops rets (TypedCallSiteID blocks args vars) callBlockWithPerms srcEntryID destID vars cl_perms_in = do blk <- view (stBlockMap . member (typedBlockIDMember destID)) <$> ask @@ -2028,24 +2060,24 @@ callBlockWithPerms srcEntryID destID vars cl_perms_in = -- | Look up the current primary permission associated with a variable getVarPerm :: ExprVar a -> - PermCheckM ext cblocks blocks tops ret r ps r ps (ValuePerm a) + PermCheckM ext cblocks blocks tops rets r ps r ps (ValuePerm a) getVarPerm x = gets (view (varPerm x) . stCurPerms) -- | Set the current primary permission associated with a variable setVarPerm :: ExprVar a -> ValuePerm a -> - PermCheckM ext cblocks blocks tops ret r ps r ps () + PermCheckM ext cblocks blocks tops rets r ps r ps () setVarPerm x p = modify (modifySTCurPerms (set (varPerm x) p)) -- | Look up the current primary permission associated with a register getRegPerm :: TypedReg a -> - PermCheckM ext cblocks blocks tops ret r ps r ps (ValuePerm a) + PermCheckM ext cblocks blocks tops rets r ps r ps (ValuePerm a) getRegPerm (TypedReg x) = getVarPerm x -- | Eliminate any disjunctions, existentials, or recursive permissions for a -- register and then return the resulting "simple" permission, leaving it on the -- top of the stack getPushSimpleRegPerm :: PermCheckExtC ext => TypedReg a -> - StmtPermCheckM ext cblocks blocks tops ret + StmtPermCheckM ext cblocks blocks tops rets (ps :> a) ps (ValuePerm a) getPushSimpleRegPerm r = getRegPerm r >>>= \p_init -> @@ -2057,7 +2089,7 @@ getPushSimpleRegPerm r = -- | Eliminate any disjunctions, existentials, or recursive permissions for a -- register and then return the resulting "simple" permission getSimpleRegPerm :: PermCheckExtC ext => TypedReg a -> - StmtPermCheckM ext cblocks blocks tops ret ps ps + StmtPermCheckM ext cblocks blocks tops rets ps ps (ValuePerm a) getSimpleRegPerm r = snd <$> pcmEmbedImplM TypedImplStmt emptyCruCtx (getSimpleVarPerm $ @@ -2066,7 +2098,7 @@ getSimpleRegPerm r = -- | A version of 'getEqualsExpr' for 'TypedReg's getRegEqualsExpr :: PermCheckExtC ext => TypedReg a -> - StmtPermCheckM ext cblocks blocks tops ret ps ps (PermExpr a) + StmtPermCheckM ext cblocks blocks tops rets ps ps (PermExpr a) getRegEqualsExpr r = snd <$> pcmEmbedImplM TypedImplStmt emptyCruCtx (getEqualsExpr $ PExpr_Var $ typedRegVar r) @@ -2078,7 +2110,7 @@ getRegEqualsExpr r = -- contents as the return value. getAtomicOrWordLLVMPerms :: (1 <= w, KnownNat w, PermCheckExtC ext) => TypedReg (LLVMPointerType w) -> - StmtPermCheckM ext cblocks blocks tops ret + StmtPermCheckM ext cblocks blocks tops rets (ps :> LLVMPointerType w) ps (Either (PermExpr (BVType w)) [AtomicPerm (LLVMPointerType w)]) @@ -2130,7 +2162,7 @@ getAtomicOrWordLLVMPerms r = -- bitvector word is found getAtomicLLVMPerms :: (1 <= w, KnownNat w, PermCheckExtC ext) => TypedReg (LLVMPointerType w) -> - StmtPermCheckM ext cblocks blocks tops ret + StmtPermCheckM ext cblocks blocks tops rets (ps :> LLVMPointerType w) ps [AtomicPerm (LLVMPointerType w)] @@ -2165,7 +2197,7 @@ findLLVMFrameVars (CruCtxCons tps _) (ns :>: _) = findLLVMFrameVars tps ns -- | Get the current frame pointer on LLVM architectures getFramePtr :: NatRepr w -> - PermCheckM LLVM cblocks blocks tops ret r ps r ps + PermCheckM LLVM cblocks blocks tops rets r ps r ps (Maybe (TypedReg (LLVMFrameType w))) getFramePtr w = gets stExtState >>= \case @@ -2177,13 +2209,13 @@ getFramePtr w = setFramePtr :: NatRepr w -> TypedReg (LLVMFrameType w) -> - PermCheckM LLVM cblocks blocks tops ret r ps r ps () + PermCheckM LLVM cblocks blocks tops rets r ps r ps () setFramePtr rep fp = modify (\st -> st { stExtState = PermCheckExtState_LLVM (Just (SomeFrameReg rep fp)) }) -- | Look up the type of a free variable, or raise an error if it is unknown getVarType :: ExprVar a -> - PermCheckM ext cblocks blocks tops ret r ps r ps (TypeRepr a) + PermCheckM ext cblocks blocks tops rets r ps r ps (TypeRepr a) getVarType x = gets (NameMap.lookup x . stVarTypes) >>= \case Just tp -> pure tp @@ -2194,7 +2226,7 @@ getVarType x = -- | Look up the types of multiple free variables getVarTypes :: RAssign Name tps -> - PermCheckM ext cblocks blocks tops ret r ps r ps (CruCtx tps) + PermCheckM ext cblocks blocks tops rets r ps r ps (CruCtx tps) getVarTypes MNil = pure CruCtxNil getVarTypes (xs :>: x) = CruCtxCons <$> getVarTypes xs <*> getVarType x @@ -2204,7 +2236,7 @@ setVarType :: Maybe String -> -- ^ The C name of the variable, if applicable ExprVar a -> -- ^ The Hobbits variable itself TypeRepr a -> -- ^ The type of the variable - PermCheckM ext cblocks blocks tops ret r ps r ps () + PermCheckM ext cblocks blocks tops rets r ps r ps () setVarType maybe_str dbg x tp = let str' = case (maybe_str,dbg) of @@ -2223,23 +2255,23 @@ setVarTypes :: RAssign (Constant (Maybe String)) tps -> RAssign Name tps -> CruCtx tps -> - PermCheckM ext cblocks blocks tops ret r ps r ps () + PermCheckM ext cblocks blocks tops rets r ps r ps () setVarTypes _ MNil MNil CruCtxNil = pure () setVarTypes str (ds :>: Constant d) (ns :>: n) (CruCtxCons ts t) = do setVarTypes str ds ns ts setVarType str d n t -- | Get the current 'PPInfo' -permGetPPInfo :: PermCheckM ext cblocks blocks tops ret r ps r ps PPInfo +permGetPPInfo :: PermCheckM ext cblocks blocks tops rets r ps r ps PPInfo permGetPPInfo = gets stPPInfo -- | Get the current prefix string to give context to error messages -getErrorPrefix :: PermCheckM ext cblocks blocks tops ret r ps r ps (Doc ()) +getErrorPrefix :: PermCheckM ext cblocks blocks tops rets r ps r ps (Doc ()) getErrorPrefix = gets (fromMaybe emptyDoc . stErrPrefix) -- | Emit debugging output using the current 'PPInfo' stmtTraceM :: (PPInfo -> Doc ()) -> - PermCheckM ext cblocks blocks tops ret r ps r ps String + PermCheckM ext cblocks blocks tops rets r ps r ps String stmtTraceM f = do dlevel <- stDebugLevel <$> top_get doc <- f <$> permGetPPInfo @@ -2247,8 +2279,8 @@ stmtTraceM f = debugTrace dlevel str (return str) -- | Failure in the statement permission-checking monad -stmtFailM :: (PPInfo -> Doc ()) -> PermCheckM ext cblocks blocks tops ret r1 ps1 - (TypedStmtSeq ext blocks tops ret ps2) ps2 a +stmtFailM :: (PPInfo -> Doc ()) -> PermCheckM ext cblocks blocks tops rets r1 ps1 + (TypedStmtSeq ext blocks tops rets ps2) ps2 a stmtFailM msg = getErrorPrefix >>>= \err_prefix -> stmtTraceM (\i -> err_prefix <> line <> @@ -2267,8 +2299,8 @@ data WithImplState vars a ps ps' = -- -- FIXME: this is not used, but is still here in case we need it later... localPermCheckM :: - PermCheckM ext cblocks blocks tops ret r_out ps_out r_in ps_in r_out -> - PermCheckM ext cblocks blocks tops ret r' ps_in r' ps_in r_in + PermCheckM ext cblocks blocks tops rets r_out ps_out r_in ps_in r_out -> + PermCheckM ext cblocks blocks tops rets r' ps_in r' ps_in r_in localPermCheckM m = get >>= \st -> liftPermCheckM (runGenStateContT m st (\_ -> pure)) @@ -2276,8 +2308,8 @@ localPermCheckM m = -- | Call 'runImplM' in the 'PermCheckM' monad pcmRunImplM :: CruCtx vars -> Doc () -> (a -> r ps_out) -> - ImplM vars (InnerPermCheckState blocks tops ret) r ps_out ps_in a -> - PermCheckM ext cblocks blocks tops ret r' ps_in r' ps_in + ImplM vars (InnerPermCheckState blocks tops rets) r ps_out ps_in a -> + PermCheckM ext cblocks blocks tops rets r' ps_in r' ps_in (AnnotPermImpl r ps_in) pcmRunImplM vars fail_doc retF impl_m = getErrorPrefix >>>= \err_prefix -> @@ -2295,9 +2327,9 @@ pcmRunImplM vars fail_doc retF impl_m = -- | Call 'runImplImplM' in the 'PermCheckM' monad pcmRunImplImplM :: CruCtx vars -> Doc () -> - ImplM vars (InnerPermCheckState blocks tops ret) r ps_out ps_in (PermImpl - r ps_out) -> - PermCheckM ext cblocks blocks tops ret r' ps_in r' ps_in + ImplM vars (InnerPermCheckState blocks tops rets) r ps_out ps_in (PermImpl + r ps_out) -> + PermCheckM ext cblocks blocks tops rets r' ps_in r' ps_in (AnnotPermImpl r ps_in) pcmRunImplImplM vars fail_doc impl_m = getErrorPrefix >>>= \err_prefix -> @@ -2315,8 +2347,8 @@ pcmRunImplImplM vars fail_doc impl_m = -- also supplying an overall error message for failures pcmEmbedImplWithErrM :: (forall ps. AnnotPermImpl r ps -> r ps) -> CruCtx vars -> Doc () -> - ImplM vars (InnerPermCheckState blocks tops ret) r ps_out ps_in a -> - PermCheckM ext cblocks blocks tops ret (r ps_out) ps_out (r ps_in) ps_in + ImplM vars (InnerPermCheckState blocks tops rets) r ps_out ps_in a -> + PermCheckM ext cblocks blocks tops rets (r ps_out) ps_out (r ps_in) ps_in (PermSubst vars, a) pcmEmbedImplWithErrM f_impl vars fail_doc m = getErrorPrefix >>>= \err_prefix -> @@ -2341,8 +2373,8 @@ pcmEmbedImplWithErrM f_impl vars fail_doc m = -- | Embed an implication computation inside a permission-checking computation pcmEmbedImplM :: (forall ps. AnnotPermImpl r ps -> r ps) -> CruCtx vars -> - ImplM vars (InnerPermCheckState blocks tops ret) r ps_out ps_in a -> - PermCheckM ext cblocks blocks tops ret (r ps_out) ps_out (r ps_in) ps_in + ImplM vars (InnerPermCheckState blocks tops rets) r ps_out ps_in a -> + PermCheckM ext cblocks blocks tops rets (r ps_out) ps_out (r ps_in) ps_in (PermSubst vars, a) pcmEmbedImplM f_impl vars m = pcmEmbedImplWithErrM f_impl vars mempty m @@ -2350,14 +2382,14 @@ pcmEmbedImplM f_impl vars m = pcmEmbedImplWithErrM f_impl vars mempty m -- @vars@ is empty stmtEmbedImplM :: ImplM RNil (InnerPermCheckState - blocks tops ret) (TypedStmtSeq ext blocks tops ret) ps_out ps_in a -> - StmtPermCheckM ext cblocks blocks tops ret ps_out ps_in a + blocks tops rets) (TypedStmtSeq ext blocks tops rets) ps_out ps_in a -> + StmtPermCheckM ext cblocks blocks tops rets ps_out ps_in a stmtEmbedImplM m = snd <$> pcmEmbedImplM TypedImplStmt emptyCruCtx m -- | Recombine any outstanding distinguished permissions back into the main -- permission set, in the context of type-checking statements stmtRecombinePerms :: - PermCheckExtC ext => StmtPermCheckM ext cblocks blocks tops ret RNil ps_in () + PermCheckExtC ext => StmtPermCheckM ext cblocks blocks tops rets RNil ps_in () stmtRecombinePerms = get >>>= \(!st) -> let dist_perms = view distPerms (stCurPerms st) in @@ -2373,7 +2405,7 @@ ppProofError ppInfo mb_ps = -- them to the top of the stack stmtProvePermsAppend :: PermCheckExtC ext => CruCtx vars -> ExDistPerms vars ps -> - StmtPermCheckM ext cblocks blocks tops ret + StmtPermCheckM ext cblocks blocks tops rets (ps_in :++: ps) ps_in (PermSubst vars) stmtProvePermsAppend vars ps = permGetPPInfo >>>= \ppInfo -> @@ -2384,7 +2416,7 @@ stmtProvePermsAppend vars ps = -- context of the empty permission stack stmtProvePerms :: PermCheckExtC ext => CruCtx vars -> ExDistPerms vars ps -> - StmtPermCheckM ext cblocks blocks tops ret + StmtPermCheckM ext cblocks blocks tops rets ps RNil (PermSubst vars) stmtProvePerms vars ps = permGetPPInfo >>>= \ppInfo -> @@ -2396,7 +2428,7 @@ stmtProvePerms vars ps = -- any existential lifetime variables stmtProvePermsFreshLs :: PermCheckExtC ext => CruCtx vars -> ExDistPerms vars ps -> - StmtPermCheckM ext cblocks blocks tops ret + StmtPermCheckM ext cblocks blocks tops rets ps RNil (PermSubst vars) stmtProvePermsFreshLs vars ps = permGetPPInfo >>>= \ppInfo -> @@ -2407,7 +2439,7 @@ stmtProvePermsFreshLs vars ps = -- | Prove a single permission in the context of type-checking statements stmtProvePerm :: (PermCheckExtC ext, KnownRepr CruCtx vars) => TypedReg a -> Mb vars (ValuePerm a) -> - StmtPermCheckM ext cblocks blocks tops ret + StmtPermCheckM ext cblocks blocks tops rets (ps :> a) ps (PermSubst vars) stmtProvePerm (TypedReg x) mb_p = permGetPPInfo >>>= \ppInfo -> @@ -2419,11 +2451,11 @@ stmtProvePerm (TypedReg x) mb_p = -- | Try to prove that a register equals a constant integer (of the given input -- type) using equality permissions in the context resolveConstant :: TypedReg tp -> - StmtPermCheckM ext cblocks blocks tops ret ps ps + StmtPermCheckM ext cblocks blocks tops rets ps ps (Maybe Integer) resolveConstant = helper . PExpr_Var . typedRegVar where helper :: PermExpr a -> - StmtPermCheckM ext cblocks blocks tops ret ps ps + StmtPermCheckM ext cblocks blocks tops rets ps ps (Maybe Integer) helper (PExpr_Var x) = getVarPerm x >>= \case @@ -2451,7 +2483,7 @@ resolveConstant = helper . PExpr_Var . typedRegVar where -- | Convert a register of one type to one of another type, if possible convertRegType :: PermCheckExtC ext => ExtRepr ext -> ProgramLoc -> TypedReg tp1 -> TypeRepr tp1 -> TypeRepr tp2 -> - StmtPermCheckM ext cblocks blocks tops ret RNil RNil + StmtPermCheckM ext cblocks blocks tops rets RNil RNil (TypedReg tp2) convertRegType _ _ reg tp1 tp2 | Just Refl <- testEquality tp1 tp2 = pure reg @@ -2511,7 +2543,7 @@ convertRegType _ _ x tp1 tp2 = -- @bv@, using the current endianness to determine how this extraction works extractBVBytes :: (1 <= w, KnownNat w) => ProgramLoc -> NatRepr sz -> Bytes -> TypedReg (BVType w) -> - StmtPermCheckM LLVM cblocks blocks tops ret RNil RNil + StmtPermCheckM LLVM cblocks blocks tops rets RNil RNil (TypedReg (BVType sz)) extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) = let w :: NatRepr w = knownNat in @@ -2552,12 +2584,12 @@ extractBVBytes loc sz off_bytes (reg :: TypedReg (BVType w)) = -- freshly-bound names for the return values. Return those freshly-bound names -- for the return values. emitStmt :: - CruCtx rets -> - RAssign (Constant (Maybe String)) rets -> + CruCtx stmt_rets -> + RAssign (Constant (Maybe String)) stmt_rets -> ProgramLoc -> - TypedStmt ext rets ps_in ps_out -> - StmtPermCheckM ext cblocks blocks tops ret ps_out ps_in - (RAssign Name rets) + TypedStmt ext stmt_rets ps_in ps_out -> + StmtPermCheckM ext cblocks blocks tops rets ps_out ps_in + (RAssign Name stmt_rets) emitStmt tps names loc stmt = gopenBinding ((TypedConsStmt loc stmt (cruCtxProxies tps) <$>) . strongMbM) @@ -2572,9 +2604,8 @@ emitLLVMStmt :: TypeRepr tp -> Maybe String -> ProgramLoc -> - TypedLLVMStmt tp ps_in ps_out -> - StmtPermCheckM LLVM cblocks blocks tops ret - ps_out ps_in (Name tp) + TypedLLVMStmt tp ps_in ps_out -> + StmtPermCheckM LLVM cblocks blocks tops rets ps_out ps_in (Name tp) emitLLVMStmt tp name loc stmt = RL.head <$> emitStmt (singletonCruCtx tp) (RL.singleton (Constant name)) loc (TypedLLVMStmt stmt) @@ -2595,7 +2626,7 @@ tcReg ctx (Reg ix) = ctx ! ix -- | Type-check a Crucible register and also look up its value, if known tcRegWithVal :: PermCheckExtC ext => CtxTrans ctx -> Reg ctx tp -> - StmtPermCheckM ext cblocks blocks tops ret ps ps + StmtPermCheckM ext cblocks blocks tops rets ps ps (RegWithVal tp) tcRegWithVal ctx r_untyped = let r = tcReg ctx r_untyped in @@ -2613,7 +2644,7 @@ tcRegs ctx (viewAssign -> AssignExtend regs reg) = -- includes its permissions and all those relevant to any register it is equal -- to, possibly plus some offset ppRelevantPerms :: TypedReg tp -> - PermCheckM ext cblocks blocks tops ret r ps r ps (Doc ()) + PermCheckM ext cblocks blocks tops rets r ps r ps (Doc ()) ppRelevantPerms r = getRegPerm r >>>= \p -> permGetPPInfo >>>= \ppInfo -> @@ -2630,7 +2661,7 @@ ppRelevantPerms r = -- | Pretty-print a Crucible 'Reg' and what 'TypedReg' it is equal to, along -- with the relevant permissions for that 'TypedReg' ppCruRegAndPerms :: CtxTrans ctx -> Reg ctx a -> - PermCheckM ext cblocks blocks tops ret r ps r ps (Doc ()) + PermCheckM ext cblocks blocks tops rets r ps r ps (Doc ()) ppCruRegAndPerms ctx r = permGetPPInfo >>>= \ppInfo -> ppRelevantPerms (tcReg ctx r) >>>= \doc -> @@ -2641,7 +2672,7 @@ ppCruRegAndPerms ctx r = -- their permissions, the variables in those permissions etc., as in -- 'varPermsTransFreeVars' getRelevantPerms :: [SomeName CrucibleType] -> - PermCheckM ext cblocks blocks tops ret r ps r ps + PermCheckM ext cblocks blocks tops rets r ps r ps (Some DistPerms) getRelevantPerms (namesListToNames -> SomeRAssign ns) = gets stCurPerms >>>= \perms -> @@ -2656,7 +2687,7 @@ ppCruRegsAndTopsPerms :: [Maybe String] -> CtxTrans ctx -> [Some (Reg ctx)] -> - PermCheckM ext cblocks blocks tops ret r ps r ps (Doc (), Doc ()) + PermCheckM ext cblocks blocks tops rets r ps r ps (Doc (), Doc ()) ppCruRegsAndTopsPerms names ctx regs = permGetPPInfo >>>= \ppInfo -> gets stTopVars >>>= \tops -> @@ -2683,7 +2714,7 @@ setErrorPrefix :: Doc () -> CtxTrans ctx -> [Some (Reg ctx)] -> - PermCheckM ext cblocks blocks tops ret r ps r ps () + PermCheckM ext cblocks blocks tops rets r ps r ps () setErrorPrefix names loc stmt_pp ctx regs = ppCruRegsAndTopsPerms names ctx regs >>>= \(regs_pp, perms_pp) -> let prefix = @@ -2705,7 +2736,7 @@ archWidth _ = knownNat -- | Type-check a Crucibe block id into a 'TypedBlockID' tcBlockID :: BlockID cblocks args -> - StmtPermCheckM ext cblocks blocks tops ret ps ps + StmtPermCheckM ext cblocks blocks tops rets ps ps (TypedBlockID blocks (CtxToRList args)) tcBlockID blkID = stLookupBlockID blkID <$> top_get @@ -2713,11 +2744,10 @@ tcBlockID blkID = stLookupBlockID blkID <$> top_get -- 'PermExpr' value that we can use as an @eq(e)@ permission on the output of -- the expression tcExpr :: - forall ext tp cblocks blocks tops ret ps. + forall ext tp cblocks blocks tops rets ps. (PermCheckExtC ext, KnownRepr ExtRepr ext) => App ext RegWithVal tp -> - StmtPermCheckM ext cblocks blocks tops ret ps ps - (Maybe (PermExpr tp)) + StmtPermCheckM ext cblocks blocks tops rets ps ps (Maybe (PermExpr tp)) tcExpr (ExtensionApp _e_ext :: App ext RegWithVal tp) | ExtRepr_LLVM <- knownRepr :: ExtRepr ext = error "tcExpr: unexpected LLVM expression" @@ -2897,7 +2927,7 @@ tcExpr _ = pure Nothing -- 'True' even if the arguments do not satisfy the permissions. couldSatisfyPermsM :: PermCheckExtC ext => CruCtx args -> TypedRegs args -> Mb ghosts (ValuePerms args) -> - StmtPermCheckM ext cblocks blocks tops ret ps ps Bool + StmtPermCheckM ext cblocks blocks tops rets ps ps Bool couldSatisfyPermsM CruCtxNil _ _ = pure True couldSatisfyPermsM (CruCtxCons tps (BVRepr _)) (TypedRegsCons args arg) (mbMatch -> [nuMP| ValPerms_Cons ps (ValPerm_Eq mb_e) |]) = @@ -2924,7 +2954,7 @@ tcEmitStmt :: CtxTrans ctx -> ProgramLoc -> Stmt ext ctx ctx' -> - StmtPermCheckM ext cblocks blocks tops ret RNil RNil (CtxTrans ctx') + StmtPermCheckM ext cblocks blocks tops rets RNil RNil (CtxTrans ctx') tcEmitStmt ctx loc stmt = do _ <- stmtTraceM (const (pretty "Type-checking statement:" <+> ppStmt (size ctx) stmt)) @@ -2941,12 +2971,12 @@ tcEmitStmt ctx loc stmt = tcEmitStmt' :: - forall ext ctx ctx' cblocks blocks tops ret. + forall ext ctx ctx' cblocks blocks tops rets. (PermCheckExtC ext, KnownRepr ExtRepr ext) => CtxTrans ctx -> ProgramLoc -> Stmt ext ctx ctx' -> - StmtPermCheckM ext cblocks blocks tops ret RNil RNil + StmtPermCheckM ext cblocks blocks tops rets RNil RNil (CtxTrans ctx') tcEmitStmt' ctx loc (SetReg _ (App (ExtensionApp e_ext @@ -2958,9 +2988,9 @@ tcEmitStmt' ctx loc (SetReg tp (App e)) = traverseFC (tcRegWithVal ctx) e >>= \e_with_vals -> tcExpr e_with_vals >>= \maybe_val -> let typed_e = TypedExpr e_with_vals maybe_val in - let rets = (singletonCruCtx tp) in - dbgNames' rets >>= \names -> - emitStmt rets names loc (TypedSetReg tp typed_e) >>>= \(_ :>: x) -> + let stmt_rets = (singletonCruCtx tp) in + dbgNames' stmt_rets >>= \names -> + emitStmt stmt_rets names loc (TypedSetReg tp typed_e) >>>= \(_ :>: x) -> stmtRecombinePerms >>> pure (addCtxName ctx x) @@ -2968,7 +2998,7 @@ tcEmitStmt' ctx loc (ExtendAssign stmt_ext :: Stmt ext ctx ctx') | ExtRepr_LLVM <- knownRepr :: ExtRepr ext = tcEmitLLVMStmt Proxy ctx loc stmt_ext -tcEmitStmt' ctx loc (CallHandle ret freg_untyped _args_ctx args_untyped) = +tcEmitStmt' ctx loc (CallHandle _ret freg_untyped _args_ctx args_untyped) = let freg = tcReg ctx freg_untyped args = tcRegs ctx args_untyped {- args_subst = typedRegsToVarSubst args -} in @@ -2992,7 +3022,8 @@ tcEmitStmt' ctx loc (CallHandle ret freg_untyped _args_ctx args_untyped) = case some_fun_perm of SomeFunPerm fun_perm -> let ghosts = funPermGhosts fun_perm - args_ns = typedRegsToVars args in + args_ns = typedRegsToVars args + rets = funPermRets fun_perm in (stmtProvePermsFreshLs ghosts (funPermExDistIns fun_perm args_ns)) >>>= \gsubst -> let gexprs = exprsOfSubst gsubst in @@ -3001,11 +3032,10 @@ tcEmitStmt' ctx loc (CallHandle ret freg_untyped _args_ctx args_untyped) = stmtProvePermsAppend CruCtxNil (emptyMb $ eqDistPerms ghosts_ns gexprs) >>>= \_ -> stmtProvePerm freg (emptyMb $ ValPerm_Conj1 $ Perm_Fun fun_perm) >>>= \_ -> - let rets = singletonCruCtx ret in dbgNames' rets >>>= \names -> - emitStmt rets names loc - (TypedCall freg fun_perm - (varsToTypedRegs ghosts_ns) gexprs args) >>>= \(_ :>: ret') -> + emitStmt rets names loc (TypedCall freg fun_perm + (varsToTypedRegs ghosts_ns) gexprs args) + >>>= \(_ :>: ret') -> stmtRecombinePerms >>> pure (addCtxName ctx ret') @@ -3024,7 +3054,7 @@ tcEmitLLVMSetExpr :: CtxTrans ctx -> ProgramLoc -> LLVMExtensionExpr (Reg ctx) tp -> - StmtPermCheckM LLVM cblocks blocks tops ret RNil RNil + StmtPermCheckM LLVM cblocks blocks tops rets RNil RNil (CtxTrans (ctx ::> tp)) -- Type-check a pointer-building expression, which is only valid when the block @@ -3181,9 +3211,9 @@ tcEmitLLVMSetExpr _ctx _loc X86Expr{} = withLifetimeCurrentPerms :: PermCheckExtC ext => PermExpr LifetimeType -> (forall ps_l. LifetimeCurrentPerms ps_l -> - StmtPermCheckM ext cblocks blocks tops ret (ps_out :++: ps_l) + StmtPermCheckM ext cblocks blocks tops rets (ps_out :++: ps_l) (ps_in :++: ps_l) a) -> - StmtPermCheckM ext cblocks blocks tops ret ps_out ps_in a + StmtPermCheckM ext cblocks blocks tops rets ps_out ps_in a withLifetimeCurrentPerms l m = -- Get the proof steps needed to prove that the lifetime l is current stmtEmbedImplM (getLifetimeCurrentPerms l) >>>= \(Some cur_perms) -> @@ -3203,11 +3233,11 @@ withLifetimeCurrentPerms l m = -- permission off the stack before returning. Return the resulting return -- register. emitTypedLLVMLoad :: - forall w sz arch cblocks blocks tops ret ps. + forall w sz arch cblocks blocks tops rets ps. (HasPtrWidth w, 1 <= sz, KnownNat sz) => Proxy arch -> ProgramLoc -> TypedReg (LLVMPointerType w) -> LLVMFieldPerm w sz -> DistPerms ps -> - StmtPermCheckM LLVM cblocks blocks tops ret + StmtPermCheckM LLVM cblocks blocks tops rets (ps :> LLVMPointerType w :> LLVMPointerType sz) (ps :> LLVMPointerType w) (Name (LLVMPointerType sz)) @@ -3230,7 +3260,7 @@ emitTypedLLVMStore :: LLVMFieldPerm w sz -> PermExpr (LLVMPointerType sz) -> DistPerms ps -> - StmtPermCheckM LLVM cblocks blocks tops ret + StmtPermCheckM LLVM cblocks blocks tops rets (ps :> LLVMPointerType w) (ps :> LLVMPointerType w) (Name UnitType) @@ -3244,12 +3274,12 @@ open _ = ?ptrWidth -- | Typecheck a statement and emit it in the current statement sequence, -- starting and ending with an empty stack of distinguished permissions tcEmitLLVMStmt :: - forall arch ctx tp cblocks blocks tops ret. + forall arch ctx tp cblocks blocks tops rets. Proxy arch -> CtxTrans ctx -> ProgramLoc -> LLVMStmt (Reg ctx) tp -> - StmtPermCheckM LLVM cblocks blocks tops ret RNil RNil + StmtPermCheckM LLVM cblocks blocks tops rets RNil RNil (CtxTrans (ctx ::> tp)) -- Type-check a word-sized load of an LLVM pointer by requiring a standard ptr @@ -3776,7 +3806,7 @@ generalizeUnneededEqPerms = -- | Type-check a Crucible jump target tcJumpTarget :: PermCheckExtC ext => CtxTrans ctx -> JumpTarget cblocks ctx -> - StmtPermCheckM ext cblocks blocks tops ret RNil RNil + StmtPermCheckM ext cblocks blocks tops rets RNil RNil (AnnotPermImpl (TypedJumpTarget blocks tops) RNil) tcJumpTarget ctx (JumpTarget blkID args_tps args) = top_get >>= \top_st -> @@ -3897,8 +3927,8 @@ tcJumpTarget ctx (JumpTarget blkID args_tps args) = -- | Type-check a termination statement tcTermStmt :: PermCheckExtC ext => CtxTrans ctx -> TermStmt cblocks ret ctx -> - StmtPermCheckM ext cblocks blocks tops ret RNil RNil - (TypedTermStmt blocks tops ret RNil) + StmtPermCheckM ext cblocks blocks tops (gouts :> ret) RNil RNil + (TypedTermStmt blocks tops (gouts :> ret) RNil) tcTermStmt ctx (Jump tgt) = TypedJump <$> tcJumpTarget ctx tgt tcTermStmt ctx (Br reg tgt1 tgt2) = @@ -3919,30 +3949,34 @@ tcTermStmt ctx (Br reg tgt1 tgt2) = "tcTermStmt: br reg unknown, checking both branches...") >> (TypedBr treg <$> tcJumpTarget ctx tgt1 <*> tcJumpTarget ctx tgt2) tcTermStmt ctx (Return reg) = - let treg = tcReg ctx reg in + let ret_n = typedRegVar $ tcReg ctx reg in get >>>= \st -> top_get >>>= \top_st -> let tops = stTopVars st + rets = stRetTypes top_st + CruCtxCons gouts _ = rets mb_ret_perms = + give (cruCtxProxies rets) $ varSubst (permVarSubstOfNames tops) $ - mbSeparate (MNil :>: Proxy) $ + mbSeparate (cruCtxProxies rets) $ mbValuePermsToDistPerms (stRetPerms top_st) - req_perms = - varSubst (singletonVarSubst $ typedRegVar treg) mb_ret_perms - err = ppProofError (stPPInfo st) req_perms in - mapM (\(Some x) -> ppRelevantPerms $ TypedReg x) (RL.mapToList Some $ - distPermsVars req_perms) + mb_req_perms = + fmap (varSubst (singletonVarSubst ret_n)) $ + mbSeparate (MNil :>: Proxy) mb_ret_perms + err = ppProofError (stPPInfo st) mb_req_perms in + mapM (\(SomeName x) -> ppRelevantPerms $ TypedReg x) (NameSet.toList $ + freeVars mb_req_perms) >>>= \pps_before -> stmtTraceM (\i -> pretty "Type-checking return statement" <> line <> pretty "Current perms:" <> softline <> ppCommaSep pps_before <> line <> pretty "Required perms:" <> softline <> - permPretty i req_perms) >>> + permPretty i mb_req_perms) >>> TypedReturn <$> - pcmRunImplM CruCtxNil err - (const $ TypedRet Refl (stRetType top_st) treg mb_ret_perms) - (proveVarsImpl $ distPermsToExDistPerms req_perms) + pcmRunImplM gouts err + (\gouts_ns -> TypedRet Refl rets (gouts_ns :>: ret_n) mb_ret_perms) + (proveVarsImplVarEVars mb_req_perms) tcTermStmt ctx (ErrorStmt reg) = let treg = tcReg ctx reg in getRegPerm treg >>>= \treg_p -> @@ -3966,9 +4000,9 @@ tcEmitStmtSeq :: [Maybe String] -> CtxTrans ctx -> StmtSeq ext cblocks ret ctx -> - PermCheckM ext cblocks blocks tops ret + PermCheckM ext cblocks blocks tops (gouts :> ret) () RNil - (TypedStmtSeq ext blocks tops ret RNil) RNil + (TypedStmtSeq ext blocks tops (gouts :> ret) RNil) RNil () tcEmitStmtSeq names ctx (ConsStmt loc stmt stmts) = setErrorPrefix names loc (ppStmt (Ctx.size ctx) stmt) ctx (stmtInputRegs stmt) >>> @@ -3983,10 +4017,11 @@ tcBlockEntryBody :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => [Maybe String] -> Block ext cblocks ret args -> - TypedEntry TCPhase ext blocks tops ret (CtxToRList args) ghosts -> - TopPermCheckM ext cblocks blocks tops ret + TypedEntry TCPhase ext blocks tops (gouts :> ret) (CtxToRList args) ghosts -> + TopPermCheckM ext cblocks blocks tops (gouts :> ret) (Mb ((tops :++: CtxToRList args) :++: ghosts) - (TypedStmtSeq ext blocks tops ret ((tops :++: CtxToRList args) :++: ghosts))) + (TypedStmtSeq ext blocks tops (gouts :> ret) + ((tops :++: CtxToRList args) :++: ghosts))) tcBlockEntryBody names blk entry@(TypedEntry {..}) = runPermCheckM names typedEntryID typedEntryArgs typedEntryGhosts typedEntryPermsIn $ \tops_ns args_ns ghosts_ns perms -> @@ -4014,10 +4049,10 @@ proveCallSiteImpl :: TypedEntryID blocks args -> CruCtx args -> CruCtx ghosts -> CruCtx vars -> MbValuePerms ((tops :++: args) :++: vars) -> MbValuePerms ((tops :++: args) :++: ghosts) -> - TopPermCheckM ext cblocks blocks tops ret (CallSiteImpl - blocks - ((tops :++: args) :++: vars) - tops args ghosts) + TopPermCheckM ext cblocks blocks tops rets (CallSiteImpl + blocks + ((tops :++: args) :++: vars) + tops args ghosts) proveCallSiteImpl srcID destID args ghosts vars mb_perms_in mb_perms_out = fmap CallSiteImpl $ runPermCheckM [] srcID args vars mb_perms_in $ \tops_ns args_ns _ perms_in -> @@ -4052,9 +4087,9 @@ callSiteSetGhosts _ (TypedCallSite {..}) = -- permissions if that implication does not already exist visitCallSite :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => - TypedEntry TCPhase ext blocks tops ret args ghosts -> + TypedEntry TCPhase ext blocks tops rets args ghosts -> TypedCallSite TCPhase blocks tops args ghosts vars -> - TopPermCheckM ext cblocks blocks tops ret + TopPermCheckM ext cblocks blocks tops rets (TypedCallSite TCPhase blocks tops args ghosts vars) visitCallSite _ site@(TypedCallSite { typedCallSiteImpl = Just _ }) = return site @@ -4069,8 +4104,8 @@ visitCallSite (TypedEntry {..}) site@(TypedCallSite {..}) -- | Widen the permissions held by all callers of an entrypoint to compute new, -- weaker input permissions that can hopefully be satisfied by them widenEntry :: PermCheckExtC ext => DebugLevel -> PermEnv -> - TypedEntry TCPhase ext blocks tops ret args ghosts -> - Some (TypedEntry TCPhase ext blocks tops ret args) + TypedEntry TCPhase ext blocks tops rets args ghosts -> + Some (TypedEntry TCPhase ext blocks tops rets args) widenEntry dlevel env (TypedEntry {..}) = debugTrace dlevel ("Widening entrypoint: " ++ show typedEntryID) $ case foldl1' (widen dlevel env typedEntryTops typedEntryArgs) $ @@ -4093,9 +4128,9 @@ visitEntry :: (PermCheckExtC ext, CtxToRList cargs ~ args, KnownRepr ExtRepr ext) => [Maybe String] -> Bool -> Block ext cblocks ret cargs -> - TypedEntry TCPhase ext blocks tops ret args ghosts -> - TopPermCheckM ext cblocks blocks tops ret - (Some (TypedEntry TCPhase ext blocks tops ret args)) + TypedEntry TCPhase ext blocks tops (gouts :> ret) args ghosts -> + TopPermCheckM ext cblocks blocks tops (gouts :> ret) + (Some (TypedEntry TCPhase ext blocks tops (gouts :> ret) args)) -- If the entry is already complete, do nothing visitEntry _ _ _ entry @@ -4140,9 +4175,9 @@ visitEntry names can_widen blk entry = visitBlock :: (PermCheckExtC ext, KnownRepr ExtRepr ext) => Bool -> {- ^ Whether widening can be applied in type-checking this block -} - TypedBlock TCPhase ext blocks tops ret args -> - TopPermCheckM ext cblocks blocks tops ret - (TypedBlock TCPhase ext blocks tops ret args) + TypedBlock TCPhase ext blocks tops rets args -> + TopPermCheckM ext cblocks blocks tops rets + (TypedBlock TCPhase ext blocks tops rets args) visitBlock can_widen blk@(TypedBlock {..}) = (stCBlocksEq <$> get) >>= \Refl -> flip (set typedBlockEntries) blk <$> @@ -4178,16 +4213,17 @@ maxWideningIters = 5 -- | Type-check a Crucible CFG tcCFG :: - forall w ext cblocks ghosts inits ret. + forall w ext cblocks ghosts inits gouts ret. (PermCheckExtC ext, KnownRepr ExtRepr ext, 1 <= w, 16 <= w) => NatRepr w -> PermEnv -> EndianForm -> DebugLevel -> - FunPerm ghosts (CtxToRList inits) ret -> + FunPerm ghosts (CtxToRList inits) gouts ret -> CFG ext cblocks inits ret -> - TypedCFG ext (CtxCtxToRList cblocks) ghosts (CtxToRList inits) ret + TypedCFG ext (CtxCtxToRList cblocks) ghosts (CtxToRList inits) gouts ret tcCFG w env endianness dlevel fun_perm cfg = let h = cfgHandle cfg ghosts = funPermGhosts fun_perm + gouts = funPermGouts fun_perm (nodes, sccs) = cfgOrderWithSCCs cfg init_st = let ?ptrWidth = w in @@ -4196,7 +4232,7 @@ tcCFG w env endianness dlevel fun_perm cfg = Some $ stLookupBlockID blkID init_st) nodes in let tp_blk_map = flip evalState init_st $ main_loop maxWideningIters tp_nodes in - TypedCFG { tpcfgHandle = TypedFnHandle ghosts h + TypedCFG { tpcfgHandle = TypedFnHandle ghosts gouts h , tpcfgFunPerm = fun_perm , tpcfgBlockMap = tp_blk_map , tpcfgEntryID = @@ -4204,8 +4240,8 @@ tcCFG w env endianness dlevel fun_perm cfg = where main_loop :: Int -> [Some (TypedBlockID blocks :: RList CrucibleType -> Type)] -> - TopPermCheckM ext cblocks blocks tops ret - (TypedBlockMap TransPhase ext blocks tops ret) + TopPermCheckM ext cblocks blocks tops rets + (TypedBlockMap TransPhase ext blocks tops rets) main_loop rem_iters _ -- We may have to iterate through the CFG twice with widening turned off -- to finally get everything to quiesce, once to ensure all block bodies diff --git a/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs b/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs index e87b38a845..557b858282 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/UntypedAST.hs @@ -8,9 +8,10 @@ import Verifier.SAW.Heapster.Located -- @(context). inputs -o outputs@ data AstFunPerm = AstFunPerm Pos - [(Located String, AstType)] - [(Located String, AstExpr)] - [(Located String, AstExpr)] -- ^ @-o@ position, context, inputs, outputs + [(Located String, AstType)] -- ^ The context of ghost variables + [(Located String, AstExpr)] -- ^ The input permissions + [(Located String, AstType)] -- ^ The context of ghost output variables + [(Located String, AstExpr)] -- ^ The output permissions deriving Show -- | Unchecked array permission