start malloc_init

LiveVerif/src/LiveVerif/LiveParsing.v

@@ -131,6 +131,8 @@ Notation "load32( a )" := (expr.load access_size.four a)
 Notation  "load( a )" := (expr.load access_size.word a)
   (in custom live_expr at level 1, a custom live_expr at level 100, only parsing).
 
+Notation NULL := 0.
+
 Set Ltac2 Backtrace.
 
 Goal forall (word: Type) (x: word),
@@ -259,6 +261,8 @@ Goal True.
   pose */ uintptr_t s = O(1, 2); /*.
   pose */ uintptr_t s = O(10, s, s); /*.
   pose live_expr:(s << s) as x.
+  pose */ store(s, NULL); /*.
+  pose */ if (s != NULL) { /*.
   pose */ s = s; /*.
   pose */ s = 12; /*.
   pose */ s = (-12); /*.

LiveVerif/src/LiveVerifExamples/onesize_malloc.v

@@ -85,6 +85,51 @@ Proof.
   intros n m M. steps.
 Qed.
 
+#[export] Instance spec_of_malloc_init: fnspec :=                                .**/
+
+uintptr_t malloc_init (uintptr_t p, uintptr_t n) /**#
+  ghost_args := (R: mem -> Prop);
+  requires t m := 8 <= malloc_block_size < 2 ^ 32 /\
+                  \[n] mod malloc_block_size = 0 /\
+                  <{ * array (uint 8) (sizeof malloc_state_t) ? /[malloc_state_ptr]
+                     * array (uint 8) \[n] ? p
+                     * R }> m;
+  ensures t' m' p := t' = t /\
+        <{ * allocator
+           * R }> m' #**/                                                     /**.
+Derive malloc_init SuchThat (fun_correct! malloc_init) As malloc_init_ok.          .**/
+{                                                                          /**. .**/
+  store(malloc_state_ptr, p);                                              /**. .**/
+  uintptr_t tail = NULL;                                                   /**. .**/
+  uintptr_t head = p + n;                                                  /**.
+
+  assert (\[n] = \[n] / malloc_block_size * malloc_block_size) as NAlt. {
+    Z.div_mod_to_equations. (* <-- also adds eqs for non-const modulo *)
+    lia.
+  }
+  assert (0 <= \[n] / malloc_block_size). {
+    zify_goal.
+    Z.div_mod_to_equations. (* <-- also adds eqs for non-const modulo *)
+    lia.
+  }
+  forget (\[n] / malloc_block_size) as c.
+  let h := find #(array (uint 8)) in rewrite NAlt in h.
+  let h := find #(head = ??) in replace n with /[c * malloc_block_size] in Def1 by steps.
+  pose proof (fixed_size_free_list_nil malloc_block_size tail map.empty
+                ltac:(assumption) ltac:(unfold emp; auto)) as A.
+  rewrite <- (mmap.du_empty_r m3) in D0.
+  forget (map.empty (map := mem)) as m.
+  change (m |= fixed_size_free_list malloc_block_size tail) in A.
+  delete #(tail = ??).
+  let h := find #(8 <= malloc_block_size) in move h after tail.
+  delete #(?? mod malloc_block_size = 0).
+  loop invariant above tail.
+                                                                                .**/
+  while (head != p) /* decreases c */ {                                    /**. .**/
+    head = head - malloc_block_size;                                       /**. .**/
+    store(head, tail);                                                     /**.
+Abort.
+
 #[export] Instance spec_of_malloc: fnspec :=                                    .**/
 
 uintptr_t malloc (uintptr_t n) /**#

bedrock2/src/bedrock2/find_hyp.v

@@ -81,6 +81,12 @@ Notation "b" := (fun ff: False => b) (in custom pat at level 0, b constr at leve
 Notation "# p" := ltac:(find_hyp_by_pat p)
   (at level 6, p custom pat at level 0, only parsing).
 
+(* Because we prefer
+     let h := find #(my ?? pattern) in ...
+   over
+     let h := constr:(#(my ?? pattern)) in ... *)
+Ltac find h := h.
+
 Goal forall a b: nat, a = 5 -> a < b -> a < 3 /\ 1 <= a -> a < 4 /\ b < 4 -> False.
   intros.
   pose proof #(?? < b) as AB.