Work on simplified example for the BFF paper.

_CoqProject

@@ -60,3 +60,4 @@
 -Q _build/default/linux/casestudies/proofs/x86_pgtable refinedc.linux.casestudies.x86_pgtable
 -Q _build/default/linux/casestudies/proofs/tcp_input refinedc.linux.casestudies.tcp_input
 -Q _build/default/linux/casestudies/proofs/bits refinedc.linux.casestudies.bits
+-Q _build/default/examples/proofs/bff_paper_example refinedc.examples.bff_paper_example

examples/bff_paper_example.c

+#include <stdbool.h>
+#include <refinedc.h>
+
+#define __bf_shf(x) (__builtin_ffsll(x) - 1)
+
+typedef uint64_t u64;
+typedef uint32_t u32;
+
+#define BITS_PER_LONG (sizeof(long) * 8)
+
+#define BIT(i) (1UL << (i))
+
+#define GENMASK(h, l) \
+  rc_reduce_expr( \
+    ((~0UL) - (1UL << (l)) + 1) & (~0UL >> (BITS_PER_LONG - 1 - (h))) \
+  )
+
+// Simplified static check (uses GCC statement-as-expression).
+#define FIELD_GET(_mask, _reg) \
+  (typeof(_mask))(((_reg) & (_mask)) >> __bf_shf(_mask))
+
+// Simplified static check (uses GCC statement-as-expression).
+#define FIELD_PREP(_mask, _val)                 \
+  ((typeof(_mask))(_val) << __bf_shf(_mask)) & (_mask)
+
+typedef u64 pte_t;
+
+#define PTE_VALID        BIT(0)
+#define PTE_TYPE         BIT(1)
+#define PTE_LEAF_ATTR_LO GENMASK(11, 2)
+#define PTE_ADDR_MASK    GENMASK(47, 12)
+#define PTE_LEAF_ATTR_HI GENMASK(63, 51)
+
+//@rc::bitfields Pte as u64
+//@  pte_valid       : bool[0]
+//@  pte_type        : integer[1]
+//@  pte_leaf_attr_lo: integer[2 ..11]
+//@  pte_addr        : integer[12..47]
+//@  pte_undef       : integer[48..50]
+//@  pte_leaf_attr_hi: integer[51..63]
+//@rc::end
+
+#define PTE_TYPE_BLOCK 0
+#define PTE_TYPE_PAGE  1
+#define PTE_TYPE_TABLE 1
+
+//@rc::inlined_prelude
+//@Definition pte_type_block : Z := 0.
+//@Definition pte_type_page  : Z := 1.
+//@rc::end
+
+#define MAX_LEVEL 4U
+
+//@rc::inlined_prelude
+//@Definition max_level : Z := 4.
+//@
+//@Definition pte_from_addr (pa : Pte) : Pte :=
+//@  zero_Pte <| pte_addr := pte_addr pa |>.
+//@
+//@Definition pte_pa (pa : Pte) : tm :=
+//@  bf_cons (range_of 12 36) (bf_val $ pte_addr pa) bf_nil.
+//@rc::end
+
+[[rc::parameters("pte : Pte")]]
+[[rc::args("pte @ bitfield<Pte>")]]
+[[rc::requires("{bitfield_wf pte}")]] // FIXME not necessary.
+[[rc::returns("{pte_valid pte} @ boolean<bool_it>")]]
+static bool pte_valid(pte_t pte) {
+  return 0 != (pte & PTE_VALID);
+  //return (pte & PTE_VALID);
+}
+
+[[rc::parameters("pa : Pte")]]
+[[rc::args("pa @ bitfield<Pte>")]]
+[[rc::returns("{pte_pa pa} @ bitfield_tpd<Pte>")]]
+static pte_t phys_to_pte(u64 pa) {
+  pte_t pte = pa & PTE_ADDR_MASK;
+  // Simplified away deadcode (fixed PAGE_SHIFT of 12).
+  return pte;
+}
+
+//@rc::inlined_prelude
+//@Definition result_pte pa level attr :=
+//@  let type := if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block in
+//@  (pte_from_addr pa) <| pte_valid := true |>
+//@                     <| pte_type := type |>
+//@                     <| pte_leaf_attr_lo := pte_leaf_attr_lo attr |>
+//@                     <| pte_leaf_attr_hi := pte_leaf_attr_hi attr |>.
+//@rc::end
+
+[[rc::parameters("p : loc", "old : Pte", "pa : Pte", "attr : Pte", "level : Z")]]
+[[rc::args("p @ &own<old @ bitfield<Pte>>", "pa @ bitfield<Pte>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
+[[rc::requires("{old.(pte_valid) = false}")]]
+[[rc::requires("{bitfield_wf old}", "{bitfield_wf pa}", "{bitfield_wf attr}")]] // FIXME not necessary.
+[[rc::returns("{true} @ boolean<bool_it>")]]
+[[rc::ensures("own p : {result_pte pa level attr} @ bitfield<Pte>")]]
+static bool set_valid_leaf_pte(pte_t *ptep, u64 pa, pte_t attr, u32 level) {
+  pte_t old = *ptep;
+  pte_t pte = phys_to_pte(pa);
+  u64 type = (level == MAX_LEVEL - 1) ?
+             PTE_TYPE_PAGE :
+             PTE_TYPE_BLOCK;
+  pte |= attr & (PTE_LEAF_ATTR_LO | PTE_LEAF_ATTR_HI);
+  pte |= FIELD_PREP(PTE_TYPE, type);
+  pte |= PTE_VALID;
+
+  /* Tolerate KVM recreating the exact same mapping. */
+  if(pte_valid(old))
+    return old == pte;
+
+  // smp_store_release(ptep, pte);
+  *ptep = pte;
+  return true;
+}