wip e1000 & sizeof(p) in C code

where p is a separation logic predicate, but also a C type

LiveVerif/src/LiveVerif/LiveVerifLib.v

@@ -36,6 +36,12 @@ Require Export coqutil.Datatypes.RecordSetters.
 Require Export LiveVerif.LiveRules.
 Require Export LiveVerif.PackageContext.
 Require Export LiveVerif.LiveProgramLogic.
+
 Require Export bedrock2.tweak_tacs. Ltac tweak_sidecond_hook ::= try solve [steps].
+
 Require Export LiveVerif.LiveParsing.
+(* extension of LiveParsing that depends on the whole SepLib: *)
+Notation "'sizeof(' p ')'" := (expr.literal (invisible_cast (PredicateSize p) _))
+  (in custom live_expr at level 1, p constr at level 0, only parsing).
+
 Require Coq.derive.Derive.

LiveVerif/src/LiveVerifExamples/e1000.v

@@ -4,6 +4,7 @@ Require Import bedrock2.TraceInspection.
 Require Import bedrock2.e1000_state.
 Require Import bedrock2.e1000_read_write_step.
 Require Import LiveVerifExamples.mbuf.
+Require Import LiveVerifExamples.fmalloc.
 
 Load LiveVerif.
 
@@ -39,39 +40,70 @@ Definition e1000_ctx_raw(c: e1000_ctx_t): word -> mem -> Prop := .**/
     uintptr_t rx_ring_base;
     uintptr_t tx_ring_base;
     uintptr_t tx_buf_allocator;
-  } e1000_ctx_t;
+  } e1000_ctx_raw;
 /**.
 
-(*
 Definition e1000_ctx(c: e1000_ctx_t)(a: word): mem -> Prop :=
   <{ * e1000_ctx_raw c a
-     * circular_buffer_slice ...
-*)
+     (* software-owned receive-related memory, ie unused receive descriptors & buffers: *)
+     * (EX (unused_rxq_elems: list (rx_desc_t * buf)), <{
+         * emp (len unused_rxq_elems + c.(current_rxq_len) = RX_RING_SIZE)
+         * circular_buffer_slice (rxq_elem MBUF_SIZE) RX_RING_SIZE
+             ((\[c.(current_RDH)] + c.(current_rxq_len)) mod RX_RING_SIZE)
+             unused_rxq_elems c.(rx_ring_base)
+       }>)
+     (* software-owned transmit-related memory, ie unused transmit descriptors & buffers:
+        Contrary to receive-related memory, we split buffers and descriptors because
+        the buffers are owned by the allocator *)
+     * (EX (unused_tx_descs: list tx_desc_t), <{
+         * emp (len unused_tx_descs + c.(current_txq_len) = TX_RING_SIZE)
+         * circular_buffer_slice tx_desc TX_RING_SIZE
+             ((\[c.(current_TDH)] + c.(current_txq_len)) mod TX_RING_SIZE)
+             unused_tx_descs c.(tx_ring_base)
+       }>)
+     * allocator MBUF_SIZE (TX_RING_SIZE - c.(current_txq_len)) c.(tx_buf_allocator)
+  }>.
 
 (* Provided by the network stack, not implemented here *)
 Instance spec_of_net_rx_eth: fnspec :=                                          .**/
 
-void net_rx_eth(uintptr_t a) /**#
-  ghost_args := mb (R: mem -> Prop);
-  requires t m := <{ * mbuf mb a
+void net_rx_eth(uintptr_t a, uintptr_t n) /**#
+  ghost_args := bs (R: mem -> Prop);
+  requires t m := <{ * mbuf \[n] bs a
                      * R }> m;
   (* rx may change the mbuf arbitrarily, but must return it *)
-  ensures t' m' := t' = t /\ exists mb',
-       <{ * mbuf mb' a
+  ensures t' m' := t' = t /\ exists bs' n',
+       <{ * mbuf n' bs' a
           * R }> m' #**/                                                   /**.
 
 
+Definition e1000_driver_mem_required: Z :=
+  MBUF_SIZE * RX_RING_SIZE + MBUF_SIZE * TX_RING_SIZE +
+  sizeof rx_desc * RX_RING_SIZE + sizeof tx_desc * TX_RING_SIZE +
+  sizeof fmalloc_state + sizeof e1000_ctx_raw.
+
+Goal exists n: Z, e1000_driver_mem_required = n.
+Proof. eexists. cbv. (* ca 66KB *) reflexivity. Succeed Qed. Abort.
+
+
 #[export] Instance spec_of_e1000_init: fnspec :=                                .**/
 
 uintptr_t e1000_init(uintptr_t b) /**#
   ghost_args := (R: mem -> Prop);
-  requires t m := <{ * array (uint 8) (sizeof e1000_ctx_raw) ? b
+  requires t m := <{ * array (uint 8) e1000_driver_mem_required ? b
                      * R }> m;
-  ensures t' m' r := t' = t /\
-       <{ * e1000_ctx_raw (* TODO not raw *) ? r
+  ensures t' m' r := t' = t /\ (* TODO trace will actually have setup interactions *)
+       <{ * e1000_ctx ? r
           * R }> m' #**/                                                   /**.
 Derive e1000_init SuchThat (fun_correct! e1000_init) As e1000_init_ok.          .**/
-{                                                                          /**.
+{                                                                          /**. .**/
+  b = b + MBUF_SIZE * RX_RING_SIZE;                                        /**. .**/
+  b = b + MBUF_SIZE * TX_RING_SIZE;                                        /**. .**/
+  b = b + sizeof(rx_desc) * RX_RING_SIZE;                                  /**. .**/
+  b = b + sizeof(tx_desc) * TX_RING_SIZE;                                  /**. .**/
+  b = b + sizeof(fmalloc_state);                                           /**. .**/
+  return b;                                                                /**. .**/
+} /**.
 Abort.
 
 #[export] Instance spec_of_e1000_rx: fnspec :=                                  .**/

LiveVerif/src/LiveVerifExamples/fmalloc.v

@@ -4,17 +4,17 @@ Require Import LiveVerif.LiveVerifLib.
 
 Load LiveVerif.
 
-Record fmalloc_state := {
+Record fmalloc_state_t := {
   block_size: Z;
   free_list: word;
 }.
 
-Definition fmalloc_state_t(s: fmalloc_state): word -> mem -> Prop := .**/
+Definition fmalloc_state(s: fmalloc_state_t): word -> mem -> Prop := .**/
 
 typedef struct __attribute__ ((__packed__)) {
   size_t block_size;
   uintptr_t free_list;
-} fmalloc_state_t;
+} fmalloc_state;
 
 /**.
 
@@ -49,7 +49,7 @@ Lemma fixed_size_free_list_nonnull: forall blk_size n a m,
     fixed_size_free_list blk_size n a m ->
     exists q n', n = S n' /\
     <{ * <{ + uintptr q
-            + anyval (array (uint 8) (blk_size - sizeof(uintptr))) }> a
+            + anyval (array (uint 8) (blk_size - sizeof uintptr)) }> a
        * fixed_size_free_list blk_size n' q }> m.
 Proof.
   intros. destruct n; simpl in *.
@@ -59,7 +59,7 @@ Qed.
 
 Definition allocator(block_size nRemaining: Z)(outer_addr: word): mem -> Prop :=
   ex1 (fun addr => <{
-    * fmalloc_state_t {| block_size := block_size; free_list := addr |} outer_addr
+    * fmalloc_state {| block_size := block_size; free_list := addr |} outer_addr
     * fixed_size_free_list block_size (Z.to_nat nRemaining) addr
     * emp (0 <= nRemaining /\ 2 * sizeof uintptr <= block_size < 2 ^ bitwidth)
   }>).
@@ -85,9 +85,9 @@ Local Hint Unfold
 
 Ltac predicates_safe_to_cancel_hook hypPred conclPred ::=
   lazymatch conclPred with
-  | fmalloc_state_t {| free_list := ?addr2 |} =>
+  | fmalloc_state {| free_list := ?addr2 |} =>
       lazymatch hypPred with
-      | fmalloc_state_t {| free_list := ?addr1 |} =>
+      | fmalloc_state {| free_list := ?addr1 |} =>
           is_evar addr2; unify addr1 addr2
       end
   end.
@@ -99,7 +99,7 @@ void fmalloc_init(uintptr_t a, uintptr_t buf, uintptr_t blk_size, uintptr_t n) /
   requires t m := 2 * sizeof uintptr <= \[blk_size] /\
                   (* disallow wrap to avoid null pointers in free list: *)
                   \[buf] <> 0 /\ \[buf] + \[n] * \[blk_size] < 2 ^ bitwidth /\
-                  <{ * array (uint 8) (sizeof fmalloc_state_t) ? a
+                  <{ * array (uint 8) (sizeof fmalloc_state) ? a
                      * array (uint 8) (\[blk_size] * \[n]) ? buf
                      * R }> m;
   ensures t' m' := t' = t /\
@@ -228,7 +228,7 @@ Derive fmalloc_init SuchThat (fun_correct! fmalloc_init) As fmalloc_init_ok.
   repeat heapletwise_step.
                                                                                 .**/
 }                                                                          /**.
-  unfold fmalloc_state_t, split_concl_at.
+  unfold fmalloc_state, split_concl_at.
   steps.
 Qed.
 

LiveVerif/src/LiveVerifExamples/mbuf.v

@@ -5,16 +5,24 @@ Load LiveVerif.
 
 Definition MBUF_SIZE := 2048.
 
+(* Note: this will result in mbufs slightly bigger than half of a 4KB page,
+   so most mbufs will span two pages, which seems bad --> don't do this!
 Record mbuf_t := {
   mbuf_len: Z;
   mbuf_data: list Z;
 }.
-
 Definition mbuf(r: mbuf_t): word -> mem -> Prop := .**/
   typedef struct __attribute__ ((__packed__)) {
     size_t mbuf_len;
     uint8_t mbuf_data[MBUF_SIZE];
-  } mbuf_t;
-/**.
+  } mbuf;
+/**. *)
+
+Definition mbuf(n: Z)(bs: list Z)(a: word): mem -> Prop :=
+  <{ * array (uint 8) n bs a
+     * array (uint 8) (MBUF_SIZE - n) ? (a ^+ /[n]) }>.
 
 End LiveVerif.
+
+#[export] Hint Extern 1 (PredicateSize (mbuf ?n ?bs)) => exact MBUF_SIZE
+: typeclass_instances.

bedrock2/src/bedrock2/e1000_read_write_step.v

@@ -201,7 +201,7 @@ Section WithMem.
      * vs @[+i, mod n] addr  *)
 
   Definition e1000_invariant(s: initialized_e1000_state)
-    (rxq: list (rx_desc * buf))(txq: list (tx_desc * buf)): mem -> Prop :=
+    (rxq: list (rx_desc_t * buf))(txq: list (tx_desc_t * buf)): mem -> Prop :=
     <{ * circular_buffer_slice (rxq_elem s.(rx_buf_size))
            s.(rx_queue_cap) s.(rx_queue_head) rxq s.(rx_queue_base_addr)
        * circular_buffer_slice txq_elem
@@ -233,7 +233,7 @@ Section WithMem.
           we receive the memory chunk for each descriptor between old and new RDH,
           as well as the buffers pointed to by them, which contain newly received
           packets *)
-        forall mRcv (done: list (rx_desc * buf)),
+        forall mRcv (done: list (rx_desc_t * buf)),
           len done <= len rxq ->
           List.map fst done = List.map fst rxq[:len done] ->
           (* snd (new buffer) can be any bytes *)
@@ -273,7 +273,7 @@ Section WithMem.
           RDH (excl, because otherwise queue considered empty), and by doing so, abandons
           the memory chunks corresponding to these descriptors and the buffers pointed to
           by them, thus providing more space for hardware to store received packets *)
-        exists (fresh: list (rx_desc * buf)),
+        exists (fresh: list (rx_desc_t * buf)),
           len rxq + len fresh < s.(rx_queue_cap) /\
           LittleEndian.combine sz val = (s.(rx_queue_head) + len rxq + len fresh)
                                          mod s.(rx_queue_cap) /\
@@ -287,7 +287,7 @@ Section WithMem.
           TDH (excl, because otherwise queue considered empty), and by doing so, indicates
           that between old and new TDT, there are new packets to be sent, and yields
           the descriptor chunks and the buffers pointed to by them to hardware *)
-        exists (toSend: list (tx_desc * buf)),
+        exists (toSend: list (tx_desc_t * buf)),
           len txq + len toSend < s.(tx_queue_cap) /\
           LittleEndian.combine sz val = (s.(tx_queue_head) + len txq + len toSend)
                                          mod s.(tx_queue_cap) /\
@@ -399,7 +399,7 @@ Section WithMem.
       externally_owned_mem t mNIC ->
       e1000_initialized s t ->
       e1000_invariant s rxq txq mNIC ->
-      (forall m' mRcv (done: list (rx_desc * buf)) new_RDH,
+      (forall m' mRcv (done: list (rx_desc_t * buf)) new_RDH,
           (* need explicit mRcv because it appears in trace *)
           map.split m' m mRcv ->
           \[new_RDH] = (s.(rx_queue_head) + len done) mod s.(rx_queue_cap) ->

bedrock2/src/bedrock2/e1000_state.v

@@ -44,7 +44,7 @@ Definition E1000_TDH := R 0x3810. (* transmit descriptor queue head *)
 Definition E1000_TDT := R 0x3818. (* transmit descriptor queue tail *)
 
 (* Receive Descriptors (Section 3.2.3) *)
-Record rx_desc: Set := {
+Record rx_desc_t: Set := {
   (* 64 bits *) rx_desc_addr: Z; (* address of buffer to write to *)
   (* 16 bits *) rx_desc_length: Z; (* length of packet received *)
   (* 16 bits *) rx_desc_csum: Z; (* checksum *)
@@ -54,7 +54,7 @@ Record rx_desc: Set := {
 }.
 
 (* Transmit Descriptors (Section 3.3.3) *)
-Record tx_desc: Set := {
+Record tx_desc_t: Set := {
   (* 64 bits *) tx_desc_addr: Z; (* address of buffer to read from *)
   (* 16 bits *) tx_desc_length: Z; (* length of packet to be sent *)
   (*  8 bits *) tx_desc_cso: Z; (* checksum offset: where to insert checksum (if enabled) *)
@@ -124,8 +124,8 @@ Record e1000_config: Set := {
 
 Record e1000_state := {
   get_e1000_config :> e1000_config;
-  rx_queue: list rx_desc;
-  tx_queue: list tx_desc;
+  rx_queue: list rx_desc_t;
+  tx_queue: list tx_desc_t;
   rx_queue_head: Z; (* RDH *)
   tx_queue_head: Z; (* TDH *)
   (* We keep track of tx buffers because these remain unchanged when handed back to
@@ -232,7 +232,7 @@ Section WithMem.
              (List.map (Z.mul sz) (circular_interval modulus startIndex (List.length vs))).
   End WithElem.
 
-  Definition rx_desc_t(r: rx_desc): word -> mem -> Prop := .**/
+  Definition rx_desc(r: rx_desc_t): word -> mem -> Prop := .**/
     typedef struct __attribute__ ((__packed__)) {
       uint64_t rx_desc_addr;
       uint16_t rx_desc_length;
@@ -246,11 +246,11 @@ Section WithMem.
   (* A receive descriptor together with the buffer it points to *)
   (* Note: buf_len is the total allocated amount and usually bigger than
      rx_desc_length, which is the actual length of the received packet *)
-  Definition rxq_elem(buf_len: Z)(v: rx_desc * buf)(addr: word): mem -> Prop :=
-    sep (rx_desc_t (fst v) addr)
+  Definition rxq_elem(buf_len: Z)(v: rx_desc_t * buf)(addr: word): mem -> Prop :=
+    sep (rx_desc (fst v) addr)
         (array (uint 8) buf_len (snd v) /[rx_desc_addr (fst v)]).
 
-  Definition tx_desc_t(r: tx_desc): word -> mem -> Prop := .**/
+  Definition tx_desc(r: tx_desc_t): word -> mem -> Prop := .**/
     typedef struct __attribute__ ((__packed__)) {
       uint64_t tx_desc_addr;
       uint16_t tx_desc_length;
@@ -264,15 +264,15 @@ Section WithMem.
 
   (* A transmit descriptor together with the buffer it points to *)
   (* Note: length of buffer is given by tx_desc_length field *)
-  Definition txq_elem(v: tx_desc * buf)(addr: word): mem -> Prop :=
-    sep (tx_desc_t (fst v) addr)
+  Definition txq_elem(v: tx_desc_t * buf)(addr: word): mem -> Prop :=
+    sep (tx_desc (fst v) addr)
         (array (uint 8) (tx_desc_length (fst v)) (snd v) /[tx_desc_addr (fst v)]).
 
 End WithMem.
 
 (* For the purpose of laying out rx/tx queue elements contiguously in memory,
    only the size of the first part (the descriptor) matters: *)
-#[export] Hint Extern 1 (PredicateSize (rxq_elem _)) => exact (sizeof rx_desc_t)
+#[export] Hint Extern 1 (PredicateSize (rxq_elem _)) => exact (sizeof rx_desc)
   : typeclass_instances.
-#[export] Hint Extern 1 (PredicateSize txq_elem) => exact (sizeof tx_desc_t)
+#[export] Hint Extern 1 (PredicateSize txq_elem) => exact (sizeof tx_desc)
   : typeclass_instances.

bedrock2/src/bedrock2/old_dma/e1000.v

@@ -69,7 +69,7 @@ Section WithMem.
       \[new_RDH] = (s.(rx_queue_head) + len packets) mod s.(rx_queue_capacity) ->
       (* we get back a (wrapping) slice of the rx queue as well as the corresponding
          buffers *)
-      <{ * circular_buffer_slice rx_desc_t s.(rx_queue_capacity) s.(rx_queue_head)
+      <{ * circular_buffer_slice rx_desc s.(rx_queue_capacity) s.(rx_queue_head)
                                  s.(rx_queue)[:len packets] /[rdba]
          * scattered_array (array (uint 8) s.(rx_buf_size)) packets
              (List.map (fun d => /[d.(rx_desc_addr)]) s.(rx_queue)[:len packets])
@@ -90,7 +90,7 @@ Section WithMem.
       \[new_RDT] = (s.(rx_queue_head) + len s.(rx_queue) + len fillable)
                      mod s.(rx_queue_capacity) ->
       len fillable = len new_descs ->
-      <{ * circular_buffer_slice rx_desc_t s.(rx_queue_capacity) s.(rx_queue_head)
+      <{ * circular_buffer_slice rx_desc s.(rx_queue_capacity) s.(rx_queue_head)
                                  new_descs /[rdba]
          * scattered_array (array (uint 8) s.(rx_buf_size)) fillable
              (List.map (fun d => /[d.(rx_desc_addr)]) new_descs)
@@ -114,7 +114,7 @@ Section WithMem.
       \[new_TDH] = (s.(tx_queue_head) + len packets) mod s.(tx_queue_capacity) ->
       (* we get back a (wrapping) slice of the tx queue as well as the corresponding
          buffers *)
-      <{ * circular_buffer_slice tx_desc_t s.(tx_queue_capacity) s.(tx_queue_head)
+      <{ * circular_buffer_slice tx_desc s.(tx_queue_capacity) s.(tx_queue_head)
                                  s.(tx_queue)[:len packets] /[tdba]
          * layout_absolute (List.map (fun pkt => array' (uint 8) pkt) packets)
                            (List.map word.of_Z buf_addrs)
@@ -138,7 +138,7 @@ Section WithMem.
                      mod s.(tx_queue_capacity) ->
       (* we get back a (wrapping) slice of the tx queue as well as the corresponding
          buffers *)
-      <{ * circular_buffer_slice tx_desc_t s.(tx_queue_capacity) s.(tx_queue_head)
+      <{ * circular_buffer_slice tx_desc s.(tx_queue_capacity) s.(tx_queue_head)
                                  new_descs /[tdba]
          * layout_absolute (List.map (fun pkt => array' (uint 8) pkt) packets)
                            (List.map word.of_Z buf_addrs)
@@ -262,7 +262,7 @@ Section WithMem.
       subst mGive2a. clear Hsd.
       (* But now, M1a and M2a imply: *)
       replace new_descs2 with new_descs1 in * by case TODO.
-      set (addrs := (List.map (fun d : rx_desc => /[rx_desc_addr d]) new_descs1)) in *.
+      set (addrs := (List.map (fun d : rx_desc_t => /[rx_desc_addr d]) new_descs1)) in *.
       move M1b at bottom. move M2b at bottom.
       (* same addresses in M1b and M2b and same element size means same footprint: *)
       assert (map.same_domain mGive1b mGive2b) as Hsd by case TODO.
@@ -299,7 +299,7 @@ Section WithMem.
           let new_RDH := /[(old_RDH + len packets) mod cfg.(rx_queue_capacity)] in
           (* we get back a (wrapping) slice of the rx queue as well as the corresponding
              buffers *)
-          <{ * circular_buffer_slice rx_desc_t cfg.(rx_queue_capacity) old_RDH
+          <{ * circular_buffer_slice rx_desc cfg.(rx_queue_capacity) old_RDH
                                      old_rx_descs[:len packets] /[rdba]
              * scattered_array (array (uint 8) cfg.(rx_buf_size)) packets
                    (List.map (fun d => /[d.(rx_desc_addr)]) (old_rx_descs[:len packets]))