From b92a58f962ecf12c30483b5880efcdd606729e87 Mon Sep 17 00:00:00 2001 From: Jennifer Paykin Date: Fri, 29 Oct 2021 10:16:43 -0700 Subject: [PATCH 1/3] Updating the output type of alloca in heapster --- .../src/Verifier/SAW/Heapster/Permissions.hs | 11 +++++++++++ .../src/Verifier/SAW/Heapster/SAWTranslation.hs | 6 ++++-- .../src/Verifier/SAW/Heapster/TypedCrucible.hs | 12 +++++------- 3 files changed, 20 insertions(+), 9 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs index 3e18d2eb9b..10671ac065 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs @@ -4308,6 +4308,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 = diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index 35b23a423c..521cb199c0 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -4080,14 +4080,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 |] -> diff --git a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs b/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs index 80071e8ceb..843551fba4 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/TypedCrucible.hs +++ b/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 []] From 8fe52ecf605d2f7bda5868601f82e822f2bcde8d Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 4 Nov 2021 16:46:56 -0700 Subject: [PATCH 2/3] fixed a bug in widening that was exposed by the typedAlloca change: when widening two shapes that do not match, return the empty shape, rather than generating a fresh shape variable --- heapster-saw/src/Verifier/SAW/Heapster/Widening.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs index d0f603566b..98c8606774 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs +++ b/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) = From c28c0a35df368c3aa434394e981573647c500241 Mon Sep 17 00:00:00 2001 From: Eddy Westbrook Date: Thu, 4 Nov 2021 16:47:15 -0700 Subject: [PATCH 3/3] fixed the contains0 proof --- heapster-saw/examples/arrays_proofs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/heapster-saw/examples/arrays_proofs.v b/heapster-saw/examples/arrays_proofs.v index 479f8d7a5a..74701a9023 100644 --- a/heapster-saw/examples/arrays_proofs.v +++ b/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.