lemma, hints, and specs needed to enable proofs about new [] #6
Conversation
…em to veify the following function:
int * testnew2() {
int *x=new int[2];
x[0]=1;
x[1]=2;
return x;
}
with spec:
cpp.spec "testnew2()" as testnew2spec with
(
\pre emp
\post{p:ptr}[Vptr p] dynAllocatedR "int[2]" p
** p |-> arrayR "int" (fun x => primR "int" 1 (Vint x)) [1;2]%Z
).
| Theorem wp_operand_array_new_glob_unsound : | ||
| forall (array_size : Expr) (oinit : option Expr) | ||
| new_fn (pass_align : bool) new_args new_targs aty Q targs | ||
| (nfty := normalize_type new_fn.2) | ||
| (_ : args_for <$> as_function nfty = Some targs), | ||
| args_for <$> as_function new_fn.2 = Some new_targs -> | ||
| (letI* v, free := wp_operand array_size in | ||
| Exists array_sizeN, [| v = Vn array_sizeN |] ** | ||
| (* The size must be non-negative. *) | ||
| [| 0 <= array_sizeN |]%N ** | ||
| Exists alloc_sz alloc_al, | ||
| let array_ty := Tarray aty array_sizeN in | ||
| [| size_of _ array_ty = Some alloc_sz |] ** | ||
| [| align_of aty = Some alloc_al |] ** (** <-- TODO FM-975 *) | ||
| [| has_type_prop alloc_sz Tsize_t |] ** | ||
| (* (Q (Vptr nullptr) free //\\ *)( | ||
| (* ^^ handles when the overhead exceeds the size? when does that happen? how can a user guarantee that doesnt happen: it seems the LHS of //\\ needs to be tightened *) | ||
| Forall overhead_sz : N, | ||
| [| has_type_prop (overhead_sz + alloc_sz)%N Tsize_t |] -* | ||
| let implicit_args := | ||
| new_implicits pass_align (overhead_sz + alloc_sz) alloc_al in | ||
| letI* _, args, vargs, free := | ||
| wp_unmaterialized_args tu ρ evaluation_order.nd [] new_targs (implicit_args ++ new_args) in | ||
| letI* res := wp_invoke_O tu new_fn.2 (inl $ Vptr $ _global new_fn.1) args vargs in | ||
| match res with | ||
| | Vptr storage_base => | ||
| if bool_decide (storage_base = nullptr) then | ||
| Q (Vptr storage_base) free | ||
| else | ||
| let storage_ptr := storage_base .[ Tbyte ! overhead_sz ] in | ||
| (* [blockR alloc_sz -|- tblockR (Tarray aty array_size)] *) | ||
| storage_base |-> blockR (overhead_sz + alloc_sz) 1$m ** | ||
| storage_base |-> alignedR STDCPP_DEFAULT_NEW_ALIGNMENT ** | ||
| (Forall (obj_ptr : ptr), | ||
| storage_ptr |-> alignedR alloc_al -* | ||
|
|
||
| (* This also ensures these pointers share their | ||
| address (see [provides_storage_same_address]) *) | ||
| provides_storage storage_ptr obj_ptr array_ty -* | ||
| letI* free'' := | ||
| match oinit with | ||
| | Some init => wp_initialize array_ty obj_ptr init | ||
| | None => default_initialize tu array_ty obj_ptr | ||
| end | ||
| in | ||
| (* Track the type we are allocating | ||
| so it can be checked at [delete] | ||
| *) | ||
| obj_ptr |-> new_token.R 1 (new_token.mk array_ty storage_ptr overhead_sz) -* | ||
| Q (Vptr obj_ptr) (free'' >*> free)) | ||
| | _ => False | ||
| end)) | ||
| |-- wp_operand (Enew new_fn new_args (new_form.Allocating pass_align) aty (Some array_size) oinit) Q. | ||
| Proof. | ||
| Admitted. |
There was a problem hiding this comment.
Do you know why you needed this hint? I don't see a similar version for the non-array version.
There was a problem hiding this comment.
Without that hint, the go gets stuck at the beginning:
thread_info : biIndex
_Σ : gFunctors
Σ : cpp_logic thread_info _Σ
σ : genv
MOD : source ⊧ σ
hf : fracG () _Σ
_PostPred_ : ptr → mpred
PostCond : PostCondition
x_addr : ptr
============================
_ : denoteModule source
_ : operator_new_array
--------------------------------------□
_ : PostCond
--------------------------------------∗
wp_operand source [region: "x" @ x_addr; return {?: "int*"}]
(Enew ("operator new[](unsigned long)"%cpp_name, "void*(unsigned long)"%cpp_type) [] (new_form.Allocating false) "int"
(Some (Ecast (Cintegral "unsigned long") (Eint 2 "int"))) None)
(λ (v : val) (free : FreeTemps),
x_addr |-> primR "int*" 1$m v -∗
interp source free
(wp_decls source [region: "x" @ x_addr; return {?: "int*"}] []
(λ (ρ : region) (free' : FreeTemps),
▷ wp_block source ρ
[Sexpr (Eassign (Esubscript (Ecast Cl2r (Evar "x" "int*")) (Eint 0 "int") "int") (Eint 1 "int") "int");
Sexpr (Eassign (Esubscript (Ecast Cl2r (Evar "x" "int*")) (Eint 1 "int") "int") (Eint 2 "int") "int");
Sreturn (Some (Ecast Cl2r (Evar "x" "int*")))]
(Kfree source (free' >*> FreeTemps.delete "int*" x_addr) (Kcleanup source [] (Kreturn (λ v0 : ptr, ▷ _PostPred_ v0)))))))
There was a problem hiding this comment.
Alright, I will take a look. Maybe there is something wrong about our hint.
There was a problem hiding this comment.
The hint in this PR is derived from the following in cpp2v. I only removed the cons enforcement of the 2nd arg of Enew and commented out the left conjunct of //\\ as that resulted in an unprovable goal from a reasonable state.
*** [ new_delete.wp_operand_array_new_glob@{} :
There was a problem hiding this comment.
I removed the type of that definition since it is in not in public code.
|
What is your definition of |
Definition dynAllocatedR ty (base:ptr) : mpred :=
Exists (bookKeepingLoc:ptr) (overhead:N),
match (size_of _ ty) with
| Some sz => bookKeepingLoc |-> pred.allocatedR 1 (overhead+sz)
| None => False
end
** (base |-> new_token.R 1
{| new_token.alloc_ty := ty;
new_token.storage_ptr := bookKeepingLoc.["unsigned char" ! overhead];
new_token.overhead := overhead |}).The proof was done with linearity. So it has everything remaining after the arrayR ownership. Also, it is general enough to also work for the non array case: cpp.spec "testnew()" as testnewspec with (
\pre emp
\post{p:ptr}[Vptr p] dynAllocatedR "int" p ** p |-> primR "int" 1 (Vint 1)
).for int * testnew() {
int *x;
x=new int;
*x=1;
return x;
}To this PR, I will add a test.v and test.cpp with these proofs/functions |
|
We should add a call to |
I added the delete proofs in test.v/.cpp. Indeed, the defn of Also, the proofs may need some cleanup. I am not sure the about the right hints to automate these proofs (e.g. remove ego/iExists/unfold). |
|
I am going to pull the other specs that we have of |
|
Your PR (#11) looks perfect. Making |
2 participants
Used these specs to verify the following function:
with spec: