lemma, hints, and specs needed to enable proofs about new []

rocq-brick-libcpp/proof/dune

@@ -11,5 +11,5 @@
  (theories
   Lens Lens.Elpi Equations Equations.Prop Equations.Type
   Stdlib
-  bluerock iris stdpp elpi elpi_elpi ExtLib Ltac2))
+  bluerock iris stdpp elpi elpi_elpi ExtLib Ltac2 bluerock.cpp.stdlib))
 (include dune.inc)

rocq-brick-libcpp/proof/dune.inc

@@ -17,6 +17,15 @@
   	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v  -- -std=c++20 -stdlib=libc++ ))))
  (alias (name srcs) (deps test.cpp))
 )
+(subdir newarr
+ (rule
+  (targets test_cpp.v.stderr test_cpp.v)
+  (alias test_ast)
+  (deps (:input test.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v  -- -std=c++20 -stdlib=libc++ ))))
+ (alias (name srcs) (deps test.cpp))
+)
 (subdir semaphore
  (rule
   (targets inc_hpp.v.stderr inc_hpp.v)

rocq-brick-libcpp/proof/newarr/hints.v

@@ -0,0 +1,99 @@
+Require Import bluerock.auto.cpp.hints.prelude.
+
+Require Import bluerock.prelude.telescopes.
+Require Import bluerock.iris.extra.bi.telescopes.
+
+Require Import bluerock.lang.cpp.logic.dispatch.
+Require Import bluerock.auto.cpp.definitions.
+Require Import bluerock.auto.cpp.specifications.
+
+Require Import bluerock.auto.cpp.hints.invoke.
+Require Import bluerock.auto.cpp.hints.alignment.
+Require Import bluerock.auto.cpp.hints.prim.
+Require Import bluerock.auto.cpp.hints.sizeof.
+
+Require Export bluerock.cpp.virtual.
+
+Import linearity.
+
+
+Section with_Σ.
+  Context `{Σ : cpp_logic} {σ : genv} (tu : translation_unit).
+  Context (ρ : region).
+
+  #[local] Set Universe Polymorphism.
+  #[local] Open Scope free_scope.
+
+  Notation wp_prval := (wp_prval tu ρ).
+  Notation wp_operand := (wp_operand tu ρ).
+  Notation wp_lval := (wp_lval tu ρ).
+  Notation wp_xval := (wp_xval tu ρ).
+  Notation wp_glval := (wp_glval tu ρ).
+  Notation wp_init := (wp_init tu ρ).
+  Notation wp_initialize := (wp_initialize tu ρ).
+
+
+  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.
+
+  Definition wp_operand_array_new_glob_unsound_B := [BWD] wp_operand_array_new_glob_unsound.
+
+
+End with_Σ.
+
+(** import this file only when you want your proofs to ignore the case when dynamic allocation fails (typically due to memory insufficiency) *)
+#[global] Hint Resolve
+ wp_operand_array_new_glob_unsound_B | 150 : db_bluerock_wp.

rocq-brick-libcpp/proof/newarr/spec_exc.v

@@ -0,0 +1,24 @@
+Require Import bluerock.auto.cpp.specs.
+
+Require Import bluerock.cpp.stdlib.new.inc_new_cpp.
+Require Import bluerock.cpp.stdlib.new.spec.
+
+Import cpp_notation.
+
+
+#[local] Set Primitive Projections.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, module ⊧ σ}.
+
+
+  (** This stdlib function communicates allocation failures using exceptions. Because the BRiCk semantics doesnt support exceptions yet, we assume that allocation failures never happen. Only use this spec in places where you dont care what happens after a dynamic allocation failure. Even when the exception is unhandled, it can execute arbitrary code before exiting, e.g. due to stack unwinding. It may make sense to wrap the default implementation in a function that catches the exception and does exit(1) right away, to ensure that the stack unwinding code doesnt do anything worse than exiting. *)
+  cpp.spec "operator new[](size_t)" as operator_new_array with
+      (\arg{sz} "sz" (Vn sz)
+       \post{p}[Vptr p]
+          p |-> (blockR sz 1$m **
+                   nonnullR **
+                   alignedR STDCPP_DEFAULT_NEW_ALIGNMENT **
+                   allocatedR 1 sz)).
+
+End with_cpp.

rocq-brick-libcpp/proof/newarr/test.cpp

@@ -0,0 +1,23 @@
+int * testnew() {
+  int *x;
+  x=new int;
+  *x=1;
+  return x;
+}
+
+int * testnewarr() {
+  int *x=new int[2];
+  x[0]=1;
+  x[1]=2;
+  return x;
+}
+
+void testnewdel() {
+  int *x = testnew();
+  delete x;
+}
+
+void testnewarrdel() {
+  int *x = testnewarr();
+  delete [] x;
+}

rocq-brick-libcpp/proof/newarr/test.v

@@ -0,0 +1,147 @@
+Require Import bluerock.auto.cpp.proof.
+Require Import bluerock.cpp.stdlib.allocator.spec.
+Require Import bluerock.cpp.stdlib.cassert.spec.
+Require Import bluerock.cpp.stdlib.vector.spec.
+Require Import bluerock.cpp.stdlib.atomic.spec.
+Require Import bluerock.cpp.stdlib.algorithms.spec.
+Require Import bluerock.cpp.stdlib.new.spec_exc.
+Require Import bluerock.brick.libcpp.newarr.spec_exc.
+Require Import bluerock.brick.libcpp.newarr.hints.
+Require Import bluerock.cpp.spec.concepts.
+Require Import bluerock.cpp.spec.concepts.experimental.
+Require Import bluerock.brick.libcpp.newarr.test_cpp.
+Require Import bluerock.cpp.stdlib.new.hints.
+
+Import linearity.
+Disable Notation "::wpOperand".
+Print new_delete.wp_operand_array_new_glob.
+Section specsproofs.
+  Context `{Σ : cpp_logic, MOD:test_cpp.module ⊧ σ}.
+
+  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 **
+      match ty with
+      | Tint  => [| overhead = 0%N |]
+      | _ =>  True (* TODO: this needs to be strengthened for many cases *)
+      end
+      **  (base |-> new_token.R 1
+                {| new_token.alloc_ty := ty;
+                   new_token.storage_ptr := bookKeepingLoc.["unsigned char" ! overhead];
+                  new_token.overhead := overhead |}).
+
+  cpp.spec "testnew()" as testnewspec with (
+    \pre emp
+    \post{p:ptr}[Vptr p] dynAllocatedR "int" p ** p |-> primR "int" 1 (Vint 1)
+    ).
+
+  Lemma prf: verify[module] testnewspec.
+  Proof using MOD.
+    verify_spec.
+    go;[ego | ego |].
+    unfold dynAllocatedR. go.
+    ego.
+    eagerUnifyU.
+    normalize_ptrs.
+    go.
+  Qed.
+  cpp.spec "testnewarr()" as testnewarrspec 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
+    ).
+
+  Lemma prf3: verify[module] testnewarrspec.
+  Proof using MOD. 
+    verify_spec.
+    go.
+    unfold dynAllocatedR.
+    go.
+    iExists _.
+    eagerUnifyU.
+    go.
+    simpl.
+    rewrite arrayR_eq.
+    unfold arrayR_def.
+    go.
+    rewrite arrR_eq.
+    unfold arrR_def.
+    go.
+    simpl.
+    ego.
+    unfold dynAllocatedR.
+    ego.
+    rewrite arrayR_eq.
+    unfold arrayR_def.
+    go.
+    rewrite arrR_eq.
+    unfold arrR_def.
+    go.
+  Qed.
+
+
+  cpp.spec "testnewdel()" as testnewdelspec with (
+        \post emp).
+
+  Opaque dynAllocatedR.
+
+  Lemma prfdel: verify[module] testnewdelspec.
+  Proof using MOD.
+    verify_spec.
+    go;[ego|].
+    Transparent dynAllocatedR.
+    go.
+    case_bool_decide; Forward.rwHyps; try go;[].
+    go.
+    normalize_ptrs.
+    go.
+  Qed.
+
+  cpp.spec "testnewarrdel()" as testnewarrdelspec with (
+        \post emp).
+
+  Lemma anyRexpand (x:ptr) ty (n:N) q:
+    ([∗list] i ∈ (seqN 0 n), x.[ty ! Z.of_N i] |-> anyR ty q) |-- x |-> anyR (Tarray ty n) q.
+  Proof. Admitted.
+
+  Lemma trueemp: True ⊢ emp:mpred.
+  Proof. Admitted.
+
+  Lemma allocatedNullForget q (sz:N):
+    (0<sz)%N ->
+    nullptr |-> allocatedR q sz |-- emp.
+  Proof using. Admitted.
+
+  Lemma prf2del: verify[module] testnewarrdelspec.
+  Proof using MOD.
+    verify_spec.
+    go;[ego|].
+    Transparent dynAllocatedR.
+    Search arrayR nullptr.
+    go.
+    rewrite arrayR_eq.
+    unfold arrayR_def.
+    go.
+    rewrite arrR_eq.
+    unfold arrR_def.
+    go.
+    case_bool_decide; subst; try go.
+    rewrite <- anyRexpand.
+    unfold seqN.
+    simpl.
+    go.
+    normalize_ptrs.
+    replace (overhead + - overhead)%Z with 0%Z by lia.
+    normalize_ptrs.
+    go.
+    case_bool_decide; Forward.rwHyps; try go.
+    { rewrite <- allocatedNullForget;[| lia]. eagerUnifyU. go. iClear "#". iStopProof. auto. apply trueemp.
+    }
+    { iClear "#". iStopProof. auto. apply trueemp. }
+  Qed.
+
+End specsproofs.