Updating the output type of alloca in heapster

heapster-saw/examples/arrays_proofs.v

@@ -69,7 +69,7 @@ Lemma no_errors_contains0
 Proof.
   unfold contains0, contains0__tuple_fun, contains0_precond.
   prove_refinement_match_letRecM_l.
-  - exact (fun a' i _ _ _ _ => assumingM (contains0_invariant a a' i) noErrorsSpec).
+  - exact (fun a' i _ _ _ _ _ => assumingM (contains0_invariant a a' i) noErrorsSpec).
   unfold contains0_invariant, noErrorsSpec.
   fold bvMem_lo; fold bvMem_hi.
   time "no_errors_contains0" prove_refinement.

heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs

@@ -4449,6 +4449,17 @@ llvmFieldsPermOfSize :: (1 <= w, KnownNat w) => f w -> Integer ->
                         ValuePerm (LLVMPointerType w)
 llvmFieldsPermOfSize w n = ValPerm_Conj $ llvmFieldsOfSize w n
 
+-- | Return a memblock permission with empty shape of given size
+llvmEmptyBlockPermOfSize :: (1 <= w, KnownNat w) => f w -> Integer ->
+                        ValuePerm (LLVMPointerType w)
+llvmEmptyBlockPermOfSize _ n = ValPerm_LLVMBlock $
+    LLVMBlockPerm { llvmBlockRW       = PExpr_RWModality Write
+                  , llvmBlockLifetime = PExpr_Always
+                  , llvmBlockOffset   = bvInt 0
+                  , llvmBlockLen      = bvInt n
+                  , llvmBlockShape    = PExpr_EmptyShape
+                  }
+
 -- | Create an LLVM shape for a single byte with @true@ permissions
 llvmByteTrueShape :: (1 <= w, KnownNat w) => PermExpr (LLVMShapeType w)
 llvmByteTrueShape =

heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs

@@ -4101,14 +4101,16 @@ translateLLVMStmt mb_stmt m = case mbMatch mb_stmt of
         w :: Proxy w = Proxy in
     withKnownNat ?ptrWidth $
     inExtTransM ETrans_LLVM $
-    translateClosed (llvmFieldsPermOfSize w sz) >>= \ptrans_tp ->
+    translateClosed (llvmEmptyBlockPermOfSize w sz) >>= \ptrans_tp ->
     withPermStackM (:>: Member_Base)
     (\(pctx :>: _) ->
       pctx
       :>: PTrans_Conj [APTrans_LLVMFrame $
                        flip nuMultiWithElim1 (extMb mb_fperm) $
                        \(_ :>: ret) fperm -> (PExpr_Var ret, sz):fperm]
-      :>: typeTransF ptrans_tp [])
+      -- the unitOpenTerm argument is because ptrans_tp is a memblock permission
+      -- with an empty shape; the empty shape expects a unit argument
+      :>: typeTransF ptrans_tp [unitOpenTerm])
     m
 
   [nuMP| TypedLLVMCreateFrame |] ->

heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs

@@ -501,16 +501,14 @@ data TypedLLVMStmt ret ps_in ps_out where
       (ps :> LLVMPointerType w :++: ps_l)
       (ps :> LLVMPointerType w :++: ps_l)
 
-  -- | Allocate an object of the given size on the given LLVM frame, broken into
-  -- word-sized fields followed by a field at the end with the remaining size:
+  -- | Allocate an object of the given size on the given LLVM frame, described
+  -- as a memory block with empty shape:
   --
   -- Type:
   -- > fp:frame(ps) -o fp:frame(ps,(ret,i)),
-  -- >                 ret:ptr((W,0) |-> true, (W,M) |-> true, (W,2*M) |-> true,
-  -- >                         ..., (w, (i-1)*M, 8*(sz-(i-1)*M)) |-> true)
+  -- >                 ret:memblock(W,0,sz,emptysh)
   --
-  -- where @sz@ is the number of bytes allocated, @M@ is the machine word size in
-  -- bytes, and @i@ is the greatest natural number such that @(i-1)*M < sz@
+  -- where @sz@ is the number of bytes allocated
   TypedLLVMAlloca ::
     HasPtrWidth w =>
     !(TypedReg (LLVMFrameType w)) ->
@@ -683,7 +681,7 @@ typedLLVMStmtOut (TypedLLVMAlloca
                   (TypedReg f) (fperms :: LLVMFramePerm w) len) ret =
   withKnownNat ?ptrWidth $
   distPerms2 f (ValPerm_Conj [Perm_LLVMFrame ((PExpr_Var ret, len):fperms)])
-  ret (llvmFieldsPermOfSize Proxy len)
+  ret (llvmEmptyBlockPermOfSize Proxy len)
 typedLLVMStmtOut TypedLLVMCreateFrame ret =
   withKnownNat ?ptrWidth $
   distPerms1 ret $ ValPerm_Conj [Perm_LLVMFrame []]

heapster-saw/src/Verifier/SAW/Heapster/Widening.hs

@@ -427,6 +427,10 @@ widenExpr' tp sh1 (PExpr_ExShape mb_sh2) =
   do x <- bindFreshVar knownRepr
      widenExpr tp sh1 (varSubst (singletonVarSubst x) mb_sh2)
 
+-- For two shapes that don't match any of the above cases, return the most
+-- general shape, which is the empty shape
+widenExpr' (LLVMShapeRepr _) _ _ = return $ PExpr_EmptyShape
+
 -- NOTE: this assumes that permission expressions only occur in covariant
 -- positions
 widenExpr' (ValuePermRepr tp) (PExpr_ValPerm p1) (PExpr_ValPerm p2) =