Improve Heapster implication prover for opaque named shapes (#1394)

* Implement a command to introduce new SAWCore primitives via Heapster * did some work to improve the implication prover for opaque named shapes, including: modalizeShape for opaque named shapes is now a no-op; and proveVarLLVMBlock now eliminates a perm on the LHS when it cannot find a match to prove opaque named shapes on the right * generated Coq file changed a bit * small fix to comment Co-authored-by: Chris Phifer <[email protected]>
GaloisInc · Jul 22, 2021 · 95a6a1a · 95a6a1a
1 parent d2b99ca
commit 95a6a1a
Show file tree

Hide file tree

Showing 3 changed files with 52 additions and 17 deletions.
diff --git 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<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.

diff --git 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
@@ -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