generalize onesize_malloc and tree_set over bitwidth

They are compiled twice:
- once in LiveVerif/src/LiveVerifExamples
- once through a symlink in LiveVerifEx64/src/LiveVerifExamples
But depending on where the file is, a different LiveVerifBitwidth.v
gets loaded when doing `Load LiveVerif.`

LiveVerif/src/LiveVerif/LiveParsing.v

@@ -4,6 +4,7 @@ Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
 Require Import bedrock2.Syntax.
 Require Import LiveVerif.LiveExpr.
 Require Import LiveVerif.LiveSnippet.
+Require Import coqutil.Word.Bitwidth.
 Require Import coqutil.Tactics.Tactics.
 Require Import coqutil.Tactics.reference_to_string.
 (* TODO consolidate with variants in coqutil: *)
@@ -263,6 +264,30 @@ Notation "'do' /* 'initial_ghosts' g0 ; 'decreases' m0 */ {" := (SDoTailrec g0 m
 Notation "} 'while' ( e ) ;" := (SEndDo e)
   (in custom snippet at level 0, e custom live_expr).
 
+Ltac exact_bitwidth :=
+  let bw := constr:(_ : Bitwidth _) in
+  lazymatch type of bw with
+  | Bitwidth ?w => exact w
+  end.
+
+Notation bitwidth := ltac:(exact_bitwidth) (only parsing).
+
+Ltac exact_bytes_per_word :=
+  let bw := constr:(_ : Bitwidth _) in
+  lazymatch type of bw with
+  | Bitwidth 32 => exact 4
+  | Bitwidth 64 => exact 8
+  end.
+
+Notation bytes_per_word := ltac:(exact_bytes_per_word) (only parsing).
+
+Notation "'sizeof(uintptr_t)'" := (expr.literal bytes_per_word)
+  (in custom live_expr at level 1, only parsing).
+
+Goal forall (BW: Bitwidth 32),
+    */ uintptr_t v = sizeof(uintptr_t); /* = SAssign true "v" (RExpr (expr.literal 4)).
+Proof. intros. reflexivity. Succeed Qed. Abort.
+
 Goal True.
   pose */ /* hello, world! */ /* as s.
   pose */ /* The way we implement C comments is a bit limited:

LiveVerif/src/LiveVerif/LiveVerif.v

@@ -1,8 +1,15 @@
 (* This file needs to be included with `Load LiveVerif`, after importing LiveVerifLib *)
 
+(* Somewhere on the load path, there needs to be a file named LiveVerifBitwidth.v which
+   contains either
+   `Require Import coqutil.Word.Bitwidth32.` or
+   `Require Import coqutil.Word.Bitwidth64.`
+  The current file doesn't contain this because it is designed to be bitwidth-independent. *)
+Load LiveVerifBitwidth.
+
 Section LiveVerif.
   Import Coq.Strings.String.
-  Context {word: word.word 32} {mem: map.map word Byte.byte}.
+  Context {word: word.word bitwidth} {mem: map.map word Byte.byte}.
   Context {word_ok: word.ok word} {mem_ok: map.ok mem}.
   Local Open Scope word_scope.
   Local Open Scope string_scope. Local Open Scope Z_scope.

LiveVerif/src/LiveVerif/LiveVerifLib.v

@@ -15,7 +15,7 @@ Require Export bedrock2.Map.DisjointUnion.
 Require Export bedrock2.ZnWords.
 Require Export bedrock2.unzify.
 Require Export bedrock2.ptsto_bytes bedrock2.Scalars.
-Require Export coqutil.Word.Bitwidth32.
+Require Export coqutil.Word.Bitwidth.
 Require coqutil.Datatypes.String coqutil.Map.SortedList coqutil.Map.SortedListString.
 Require Export bedrock2.SepBulletPoints.
 Require Export bedrock2.SepappBulletPoints.

LiveVerif/src/LiveVerifExamples/LiveVerifBitwidth.v

@@ -0,0 +1 @@
+Require Import coqutil.Word.Bitwidth32.

LiveVerif/src/LiveVerifExamples/onesize_malloc.v

@@ -31,7 +31,7 @@ Inductive fixed_size_free_list(block_size: Z): word -> mem -> Prop :=
 | fixed_size_free_list_cons p q m:
   p <> /[0] ->
   <{ * <{ + uintptr q
-          + anyval (array (uint 8) (block_size - 4)) }> p
+          + anyval (array (uint 8) (block_size - sizeof uintptr)) }> p
      * fixed_size_free_list block_size q }> m ->
   fixed_size_free_list block_size p m.
 
@@ -46,7 +46,7 @@ Definition allocator_with_potential_failure(f: option Z): mem -> Prop :=
                        malloc_block_size < n
            | None => True
            end)
-    * emp (8 <= malloc_block_size < 2 ^ 32)
+    * emp (2 * sizeof uintptr <= malloc_block_size < 2 ^ bitwidth)
   }>).
 
 Definition allocator: mem -> Prop :=
@@ -123,9 +123,9 @@ Axiom TODO: False.
 
 void Malloc_init (uintptr_t p, uintptr_t n) /**#
   ghost_args := (R: mem -> Prop);
-  requires t m := 8 <= malloc_block_size < 2 ^ 32 /\
+  requires t m := 2 * sizeof uintptr <= malloc_block_size < 2 ^ bitwidth /\
                   \[n] mod malloc_block_size = 0 /\
-                  \[p] + \[n] < 2 ^ 32 /\ (* <-- no wrap around because otherwise
+                  \[p] + \[n] < 2 ^ bitwidth /\ (* <-- no wrap around because otherwise
                                              some pointers in free list might be null *)
                   <{ * array (uint 8) (sizeof malloc_state_t) ? /[malloc_state_ptr]
                      * array (uint 8) \[n] ? p
@@ -158,16 +158,16 @@ Derive Malloc_init SuchThat (fun_correct! Malloc_init) As Malloc_init_ok.
   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.
+  let h := find #(?? <= malloc_block_size < ??) in move h after tail.
   delete #(?? mod malloc_block_size = 0).
-  prove (c * malloc_block_size < 2 ^ 32).
+  prove (c * malloc_block_size < 2 ^ bitwidth).
   delete #(\[n] = ??). (* try to not use n any more *)
   loop invariant above tail.
                                                                                 .**/
   while (head != p) /* decreases c */ {                                    /**. .**/
     head = head - malloc_block_size;                                       /**.
 
-    assert (\[head ^- p] + 4 <= c * malloc_block_size). {
+    assert (\[head ^- p] + sizeof uintptr <= c * malloc_block_size). {
       (* TODO can we automate this proof so that the assertion is not needed
          any more, because the subrange check that needs it finds it on its own? *)
       subst head.

LiveVerif/src/LiveVerifExamples/tree_set.v

@@ -46,7 +46,7 @@ Fixpoint bst'(sk: tree_skeleton)(s: set Z)(addr: word){struct sk}: mem -> Prop :
   | Node skL skR => EX (p: word) (v: Z) (q: word),
       <{ * emp (addr <> /[0])
          * emp (s v)
-         * freeable 12 addr
+         * freeable (sizeof uintptr * 2 + 4) addr
          * <{ + uintptr p
               + uint 32 v
               + uintptr q }> addr
@@ -63,7 +63,7 @@ Definition bst(s: set Z)(addr: word): mem -> Prop :=
 Local Hint Extern 1 (PredicateSize (bst' ?sk)) =>
   let r := eval cbv iota in
     (match sk with
-     | Node _ _ => 12
+     | Node _ _ => sizeof uintptr * 2 + 4
      | Leaf => 0
      end) in
   exact r
@@ -99,15 +99,15 @@ Lemma invert_bst'_nonnull{sk s p m}:
     exists skL skR pL v pR,
       sk = Node skL skR /\
       s v /\
-      <{ * freeable 12 p
+      <{ * freeable (sizeof uintptr * 2 + 4) p
          * <{ + uintptr pL
               + uint 32 v
               + uintptr pR }> p
          * bst' skL (fun x => s x /\ x < v) pL
          * bst' skR (fun x => s x /\ v < x) pR }> m.
 Proof.
   intros.
-  destruct sk; simpl in *|-.
+  destruct sk; simpl in *.
   { exfalso. unfold with_mem, emp in *. intuition idtac. }
   repeat heapletwise_step.
   eexists _, _, p0, v, q. split. 1: reflexivity.
@@ -158,6 +158,8 @@ Ltac zset_solver :=
 Ltac step_hook ::=
   match goal with
   | |- _ => progress cbn [bst']
+  | |- context C[8 * 2 + 4] => let g := context C[20] in change g (* TODO generalize *)
+  | |- context C[4 * 2 + 4] => let g := context C[12] in change g (* TODO generalize *)
   | sk: tree_skeleton |- _ => progress subst sk
   | |- same_set _ _ => reflexivity (* <- might instantiate evars and we're fine with that *)
   | |- same_set _ _ => zset_solver
@@ -219,7 +221,7 @@ Ltac predicates_safe_to_cancel_hook hypPred conclPred ::=
 
 void bst_init(uintptr_t p) /**#
   ghost_args := (R: mem -> Prop);
-  requires t m := <{ * array (uint 8) 4 ? p
+  requires t m := <{ * array (uint 8) (sizeof uintptr) ? p
                      * R }> m;
   ensures t' m' := t' = t /\
                    <{ * bst (fun _ => False) p
@@ -237,18 +239,18 @@ uintptr_t bst_alloc_node( ) /**#
   requires t m := <{ * allocator
                      * R }> m;
   ensures t' m' res := t' = t /\
-                       ((\[res] =  0 /\ <{ * allocator_failed_below 12
+                       ((\[res] =  0 /\ <{ * allocator_failed_below (sizeof uintptr * 2 + 4)
                                            * R }> m') \/
                         (\[res] <> 0 /\ <{ * allocator
-                                           * freeable 12 res
+                                           * freeable (sizeof uintptr * 2 + 4) res
                                            * uintptr ? res
-                                           * uint 32 ? (res ^+ /[4])
-                                           * uintptr ? (res ^+ /[8])
+                                           * uint 32 ? (res ^+ /[sizeof uintptr])
+                                           * uintptr ? (res ^+ /[sizeof uintptr + 4])
                                            * R }> m')) #**/                /**.
 Derive bst_alloc_node SuchThat (fun_correct! bst_alloc_node)
 As bst_alloc_node_ok.                                                           .**/
 {                                                                          /**. .**/
-  uintptr_t res = Malloc(12);                                              /**. .**/
+  uintptr_t res = Malloc(sizeof(uintptr_t) + 4 + sizeof(uintptr_t));       /**. .**/
   return res;                                                              /**. .**/
 }                                                                          /**.
   destruct_one_match_hyp; steps.
@@ -259,11 +261,12 @@ Qed.
 
 uintptr_t bst_add(uintptr_t p, uintptr_t vAdd) /**#
   ghost_args := s (R: mem -> Prop);
-  requires t m := <{ * allocator
+  requires t m := \[vAdd] < 2 ^ 32 /\
+                  <{ * allocator
                      * bst s p
                      * R }> m;
   ensures t' m' r := t' = t /\
-                     ((\[r] = 0 /\ <{ * allocator_failed_below 12
+                     ((\[r] = 0 /\ <{ * allocator_failed_below (sizeof uintptr * 2 + 4)
                                       * bst s p
                                       * R }> m') \/
                       (\[r] = 1 /\ <{ * allocator
@@ -289,7 +292,7 @@ Derive bst_add SuchThat (fun_correct! bst_add) As bst_add_ok.
   while (a && !found)
     /* initial_ghosts(p, s, sk, R); decreases(measure) */
   {                                                                        /**. .**/
-    uintptr_t x = load32(a + 4);                                           /**. .**/
+    uintptr_t x = load32(a + sizeof(uintptr_t));                           /**. .**/
     if (x == vAdd) /* split */ {                                           /**. .**/
       found = 1;                                                           /**. .**/
     }                                                                      /**.
@@ -301,7 +304,7 @@ Derive bst_add SuchThat (fun_correct! bst_add) As bst_add_ok.
         a = load(p);                                                       /**. .**/
       }                                                                    /**. .**/
       else {                                                               /**. .**/
-        p = a + 8;                                                         /**. .**/
+        p = a + sizeof(uintptr_t) + 4;                                     /**. .**/
         a = load(p);                                                       /**. .**/
       }                                                                    /**. .**/
     }                                                                      /**. .**/
@@ -316,8 +319,8 @@ Derive bst_add SuchThat (fun_correct! bst_add) As bst_add_ok.
     uintptr_t res = bst_alloc_node();                                      /**. .**/
     if (res) /* split */ {                                                 /**. .**/
       store(res, 0);                                                       /**. .**/
-      store32(res+4, vAdd);                                                /**. .**/
-      store(res+8, 0);                                                     /**. .**/
+      store32(res + sizeof(uintptr_t), vAdd);                              /**. .**/
+      store(res + sizeof(uintptr_t) + 4, 0);                               /**. .**/
       store(p, res);                                                       /**. .**/
       return 1;                                                            /**. .**/
     }                                                                      /**. .**/
@@ -357,14 +360,14 @@ Derive bst_contains SuchThat (fun_correct! bst_contains) As bst_contains_ok.
   while (!found && a != 0)
     /* initial_ghosts(p, s, sk, R); decreases measure */
   {                                                                        /**. .**/
-    uintptr_t here = load32(a+4);                                          /**. .**/
+    uintptr_t here = load32(a + sizeof(uintptr_t));                        /**. .**/
     if (query < here) /* split */ {                                        /**. .**/
       p = a;                                                               /**. .**/
       a = load(p);                                                         /**. .**/
     }                                                                      /**. .**/
     else {                                                                 /**. .**/
       if (here < query) /* split */ {                                      /**. .**/
-        p = a + 8;                                                         /**. .**/
+        p = a + sizeof(uintptr_t) + 4;                                     /**. .**/
         a = load(p);                                                       /**. .**/
       }                                                                    /**. .**/
       else {                                                               /**. .**/

LiveVerifEx64/Makefile

@@ -0,0 +1,66 @@
+.DEFAULT_GOAL := all
+
+.PHONY: clean force all coq install test
+
+# Absolute paths so that emacs compile mode knows where to find the errors
+# even under parallel make, where the 'Entering/Leaving directory ...'
+# messages get mixed up.
+# Using cygpath -m because Coq on Windows cannot handle cygwin paths.
+SRCDIR := $(shell cygpath -m "$$(pwd)" 2>/dev/null || pwd)/src
+
+ALL_VS := $(shell find $(SRCDIR) -name '*.v')
+
+DEPS_DIR ?= ../deps
+
+# Note: make does not interpret "\n", and this is intended
+DEPFLAGS_COQUTIL_NL=-Q $(DEPS_DIR)/coqutil/src/coqutil coqutil\n
+DEPFLAGS_NL=
+CURFLAGS_NL=-Q ../bedrock2/src/bedrock2 bedrock2\n-Q ../LiveVerif/src/LiveVerif LiveVerif\n-Q src/LiveVerifExamples LiveVerifExamples\n
+
+EXTERNAL_DEPENDENCIES?=
+EXTERNAL_COQUTIL?=
+
+ifneq ($(EXTERNAL_COQUTIL),1)
+DEPFLAGS_NL+=$(DEPFLAGS_COQUTIL_NL)
+endif
+
+ifneq ($(EXTERNAL_DEPENDENCIES),1)
+ALLDEPFLAGS_NL=$(CURFLAGS_NL)$(DEPFLAGS_NL)
+else
+ALLDEPFLAGS_NL=$(CURFLAGS_NL)
+endif
+
+ALLDEPFLAGS=$(subst \n, ,$(ALLDEPFLAGS_NL))
+
+# We auto-update _CoqProject,
+# but only change the timestamp if the set of files that it lists changed
+
+PRINT_DEPFLAGS_NL := printf -- '$(ALLDEPFLAGS_NL)'
+PRINT_ALL_VS := printf -- '%s\n' $(sort $(ALL_VS))
+PRINT_COQPROJECT := { $(PRINT_DEPFLAGS_NL); $(PRINT_ALL_VS); }
+OLD_COQPROJECT_CONTENTS := $(strip $(shell cat _CoqProject 2>/dev/null))
+NEW_COQPROJECT_CONTENTS := $(strip $(shell $(PRINT_COQPROJECT)))
+
+ifneq ($(OLD_COQPROJECT_CONTENTS),$(NEW_COQPROJECT_CONTENTS))
+_CoqProject: force
+	@echo updating $@
+	@$(PRINT_COQPROJECT) > $@
+endif
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -docroot LiveVerif $(COQMF_ARGS) -f _CoqProject -o Makefile.coq
+
+coq: Makefile.coq $(ALL_VS)
+	$(MAKE) --no-print-directory -f Makefile.coq
+
+all: coq
+
+force:
+
+clean:: Makefile.coq
+	$(MAKE) -f Makefile.coq clean
+	find . -type f \( -name '*~' -o -name '*.aux' -o -name '.lia.cache' -o -name '.nia.cache' \) -delete
+	rm -f Makefile.coq Makefile.coq.conf _CoqProject
+
+install::
+	$(MAKE) -f Makefile.coq install

LiveVerifEx64/src/LiveVerifExamples/LiveVerifBitwidth.v

@@ -0,0 +1 @@
+Require Import coqutil.Word.Bitwidth64.

LiveVerifEx64/src/LiveVerifExamples/onesize_malloc.v

@@ -0,0 +1 @@
+../../../LiveVerif/src/LiveVerifExamples/onesize_malloc.v

LiveVerifEx64/src/LiveVerifExamples/tree_set.v

@@ -0,0 +1 @@
+../../../LiveVerif/src/LiveVerifExamples/tree_set.v

Makefile

@@ -1,6 +1,6 @@
 default_target: all
 
-.PHONY: update_all clone_all coqutil riscv-coq bedrock2_noex bedrock2_ex LiveVerif_noex LiveVerif_ex compiler_noex compiler_ex kami processor end2end all clean_coqutil clean_riscv-coq clean_bedrock2 clean_LiveVerif clean_compiler clean_kami clean_processor clean_end2end clean_manglenames clean install_coqutil install_kami install_riscv-coq install_bedrock2 install_bedrock2_ex install_bedrock2_noex install_LiveVerif install_LiveVerif_ex install_LiveVerif_noex install_compiler install_processor install_end2end install
+.PHONY: update_all clone_all coqutil riscv-coq bedrock2_noex bedrock2_ex LiveVerif_noex LiveVerif_ex LiveVerifEx64 compiler_noex compiler_ex kami processor end2end all clean_coqutil clean_riscv-coq clean_bedrock2 clean_LiveVerif clean_LiveVerifEx64 clean_compiler clean_kami clean_processor clean_end2end clean_manglenames clean install_coqutil install_kami install_riscv-coq install_bedrock2 install_bedrock2_ex install_bedrock2_noex install_LiveVerif install_LiveVerifEx64 install_LiveVerif_ex install_LiveVerif_noex install_compiler install_processor install_end2end install
 
 clone_all:
 	git submodule update --init --recursive
@@ -116,6 +116,15 @@ install_LiveVerif:
 install_LiveVerif_noex:
 	$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerif install_noex
 
+LiveVerifEx64: LiveVerif_noex
+	$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerifEx64
+
+clean_LiveVerifEx64:
+	$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerifEx64 clean
+
+install_LiveVerifEx64:
+	$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerifEx64 install
+
 install_LiveVerif_ex:
 	$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerif install_ex
 
@@ -149,12 +158,12 @@ clean_end2end:
 install_end2end:
 	$(MAKE) -C $(ABS_ROOT_DIR)/end2end install
 
-all: bedrock2_ex LiveVerif_ex compiler_ex processor end2end
+all: bedrock2_ex LiveVerif_ex LiveVerifEx64 compiler_ex processor end2end
 
-clean: clean_bedrock2 clean_LiveVerif clean_compiler clean_processor clean_end2end
+clean: clean_bedrock2 clean_LiveVerif clean_LiveVerifEx64 clean_compiler clean_processor clean_end2end
 
 clean_deps: clean_coqutil clean_kami clean_riscv-coq
 
 clean_all: clean_deps clean
 
-install: install_bedrock2 install_LiveVerif install_compiler install_processor install_end2end
+install: install_bedrock2 install_LiveVerif install_LiveVerifEx64 install_compiler install_processor install_end2end