diff --git a/heapster-saw/examples/string_set.v b/heapster-saw/examples/string_set.v index 49b0ee4f60..a1f7650c6e 100644 --- a/heapster-saw/examples/string_set.v +++ b/heapster-saw/examples/string_set.v @@ -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, top3:string<>, - top4:string<>, ghost8:llvmframe [x12:8, x11:8, x10:8], - x22:(ghost26:lifetime). - ghost26:true, arg25:string_set, 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, arg27:string<> -o - ghost26:true, arg25:string_set, 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, 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, x20:string<> + (z26). z26:true, x22:string_set, x23:string<> Could not determine enough variables to prove permissions: - (z23). z23:true, x19:string_set"%string)) tt). + (z26). z26:true, x22:string_set"%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. diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs index 457aa272bb..d648b68b75 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs @@ -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) @@ -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 = @@ -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 @@ -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 exact offset, length, and shape, because + -- 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 |] diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 19d7652461..5a43e27973 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -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