Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve Heapster implication prover for opaque named shapes #1394

Merged
merged 5 commits into from
Jul 22, 2021
Merged

Improve Heapster implication prover for opaque named shapes #1394

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
d089eed
Implement a command to introduce new SAWCore primitives via Heapster
ChrisEPhifer Jul 20, 2021
4785a08
did some work to improve the implication prover for opaque named shap…
Jul 21, 2021
503a65c
Merge remote-tracking branch 'origin/master' into heapster-opaque-nam…
Jul 22, 2021
d2f14cb
generated Coq file changed a bit
Jul 22, 2021
2aa97b4
small fix to comment
Jul 22, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 13 additions & 12 deletions heapster-saw/examples/string_set.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,23 +42,24 @@ Definition string_set_remove : forall (p0 : string_set), forall (p1 : string), C
@listRemoveM (@SAWCoreScaffolding.String) (@SAWCoreScaffolding.equalString).

Definition insert_remove__tuple_fun : @CompM.lrtTupleType (@CompM.LRT_Cons (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit)))))) (@CompM.LRT_Nil)) :=
@CompM.multiFixM (@CompM.LRT_Cons (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit)))))) (@CompM.LRT_Nil)) (fun (insert_remove : @CompM.lrtToType (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit))))))) => pair (fun (p0 : string_set) (p1 : string) (p2 : string) => @CompM.letRecM (@CompM.LRT_Nil) (prod string_set (prod string unit)) tt (@errorM CompM _ (prod string_set (prod string unit)) "At string_set.c:15:3 ($14 = call $13($10, $11);)
Regs: $13 = x22, $10 = x19, $11 = x20
@CompM.multiFixM (@CompM.LRT_Cons (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit)))))) (@CompM.LRT_Nil)) (fun (insert_remove : @CompM.lrtToType (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit))))))) => pair (fun (p0 : string_set) (p1 : string) (p2 : string) => @CompM.letRecM (@CompM.LRT_Nil) (prod string_set (prod string unit)) tt (@errorM CompM _ (prod string_set (prod string unit)) "At string_set.c:15:3 ($17 = call $16($13, $14);)
Regs: $16 = x25 @ , $13 = x22 @ , $14 = x23 @
Input perms: top1:true, top2:string_set<W, top1>, top3:string<>,
top4:string<>, ghost8:llvmframe [x12:8, x11:8, x10:8],
x22:(ghost26:lifetime).
ghost26:true, arg25:string_set<W, ghost26>, arg24:string<>
top4:string<>, ghost8:llvmframe [C[&str2]12:8, C[&str1]11:8,
C[&set]10:8],
x25:(ghost29:lifetime).
ghost29:true, arg28:string_set<W, ghost29>, arg27:string<>
-o
ghost26:true, arg25:string_set<W, ghost26>, arg24:true,
ret23:true, x19:eq(top2), x20:eq(top3), x10:ptr((W,0) |->
eq(x19)),
x11:ptr((W,0) |-> eq(x20)), x12:ptr((W,0) |-> eq(local7)),
local7:eq(top4)
ghost29:true, arg28:string_set<W, ghost29>, arg27:true,
ret26:true, x22:eq(top2), x23:eq(top3),
C[&set]10:ptr((W,0) |-> eq(x22)), C[&str1]11:ptr((W,0) |->
eq(x23)),
C[&str2]12:ptr((W,0) |-> eq(local7)), local7:eq(top4)
Could not prove
(z23). z23:true, x19:string_set<W, z23>, x20:string<>
(z26). z26:true, x22:string_set<W, z26>, x23:string<>

Could not determine enough variables to prove permissions:
(z23). z23:true, x19:string_set<W, z23>"%string)) tt).
(z26). z26:true, x22:string_set<W, z26>"%string)) tt).

Definition insert_remove : @CompM.lrtToType (@CompM.LRT_Fun string_set (fun (perm0 : string_set) => @CompM.LRT_Fun string (fun (perm1 : string) => @CompM.LRT_Fun string (fun (perm2 : string) => @CompM.LRT_Ret (prod string_set (prod string unit)))))) :=
SAWCoreScaffolding.fst insert_remove__tuple_fun.
Expand Down
39 changes: 34 additions & 5 deletions heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3929,7 +3929,8 @@ implIntroLLVMBlockNamed _ _ =
error "implIntroLLVMBlockNamed: malformed permission"

-- | Eliminate a @memblock@ permission on the top of the stack, if possible,
-- otherwise fail
-- otherwise fail. The elimination does not have to completely remove any
-- @memblock@ permission, it just needs to make some sort of progress.
implElimLLVMBlock :: (1 <= w, KnownNat w, NuMatchingAny1 r) =>
ExprVar (LLVMPointerType w) -> LLVMBlockPerm w ->
ImplM vars s r (ps :> LLVMPointerType w)
Expand All @@ -3953,16 +3954,22 @@ implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
implElimLLVMBlock x (bp { llvmBlockShape = sh' })
implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
PExpr_EqShape (PExpr_Var y) }) =
-- For shape eqsh(y), prove y:block(sh) for some sh, apply
-- For shape eqsh(y), prove y:block(sh) for some sh, and apply
-- SImpl_IntroLLVMBlockFromEq, and then recursively eliminate the resulting
-- memblock permission
-- memblock permission, unless the resulting shape cannot be eliminated, in
-- which case we have still made progress so we can just stop
mbVarsM () >>>= \mb_unit ->
withExtVarsM (proveVarImplInt y $ mbCombine RL.typeCtxProxies $ flip fmap mb_unit $ const $
nu $ \sh -> ValPerm_Conj1 $
Perm_LLVMBlockShape $ PExpr_Var sh) >>>= \(_, sh) ->
let bp' = bp { llvmBlockShape = sh } in
implSimplM Proxy (SImpl_IntroLLVMBlockFromEq x bp' y) >>>
implElimLLVMBlock x bp'
case sh of
PExpr_NamedShape _ _ nmsh _
| not (namedShapeCanUnfold nmsh) ->
-- Opaque shapes cannot be further eliminated, so stop
return ()
_ -> implElimLLVMBlock x bp'
implElimLLVMBlock x bp@(LLVMBlockPerm { llvmBlockShape =
PExpr_PtrShape maybe_rw maybe_l sh })
| Just len <- llvmShapeLength sh =
Expand Down Expand Up @@ -5375,7 +5382,8 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of
implSwapInsertConjM x (Perm_LLVMBlock bp_out) ps'' 0


-- If proving a named shape, prove its unfolding first and then fold it
-- If proving an unfoldable named shape, prove its unfolding first and then
-- fold it
[nuMP| mb_bp : mb_bps |]
| [nuMP| PExpr_NamedShape rw l nmsh args |] <- mbMatch $ fmap llvmBlockShape mb_bp
, [nuMP| TrueRepr |] <- mbMatch $ fmap namedShapeCanUnfoldRepr nmsh
Expand All @@ -5402,6 +5410,27 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of
implSwapInsertConjM x (Perm_LLVMBlock bp') ps_out' 0


-- If proving an opaque named shape, the only way to prove the memblock
-- permission is to have it on the left, but we don't have a memblock
-- permission on the left with this exactly offset, length, and shape, because
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Grammar nitpick: Should be "exact offset, length, ..." instead of "exactly offset, length, ..."

-- it would have matched some previous case, so try to eliminate a memblock
-- and recurse
[nuMP| mb_bp : mb_bps |]
| [nuMP| PExpr_NamedShape _ _ nmsh _ |] <- mbMatch $ fmap llvmBlockShape mb_bp
, [nuMP| FalseRepr |] <- mbMatch $ fmap namedShapeCanUnfoldRepr nmsh
, Just off <- partialSubst psubst $ fmap llvmBlockOffset mb_bp
, Just i <- findIndex (\case
p@(Perm_LLVMBlock _) ->
isJust (llvmPermContainsOffset off p)
_ -> False) ps
, Perm_LLVMBlock bp <- ps!!i ->
implGetPopConjM x ps i >>> implElimPopLLVMBlock x bp >>>
proveVarImplInt x (fmap ValPerm_Conj $
mbMap2 (++)
(fmap (map Perm_LLVMBlock) $ mbMap2 (:) mb_bp mb_bps)
mb_ps)


-- If proving an equality shape eqsh(z) for evar z which has already been set,
-- substitute for z and recurse
[nuMP| mb_bp : mb_bps |]
Expand Down
5 changes: 5 additions & 0 deletions heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3368,6 +3368,11 @@ modalizeShape _ _ (PExpr_Var _) =
-- adding a modalized variable shape constructor
Nothing
modalizeShape _ _ PExpr_EmptyShape = Just PExpr_EmptyShape
modalizeShape _ _ sh@(PExpr_NamedShape _ _ nmsh _)
| not (namedShapeCanUnfold nmsh) =
-- Opaque shapes are not affected by modalization, because we assume they do
-- not have any top-level pointers in them
Just sh
modalizeShape rw l (PExpr_NamedShape rw' l' nmsh args) =
-- If a named shape already has modalities, they take precedence
Just $ PExpr_NamedShape (rw' <|> rw) (l' <|> l) nmsh args
Expand Down