check bounds on bitfields

_CoqProject

@@ -59,3 +59,4 @@
 -Q _build/default/linux/casestudies/mt7601u/proofs/mac refinedc.linux.casestudies.mt7601u.mac
 -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

linux/casestudies/pgtable.c

@@ -156,7 +156,7 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
 
 [[rc::parameters("p : loc", "pte : Pte", "pa : Pte", "attr : Pte", "level : Z", "type : Z", "pte1 : Pte")]]
 [[rc::args("p @ &own<pte @ bitfield<Pte>>", "pa @ bitfield<Pte>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
-[[rc::requires("{bitfield_wf pte}", "{bitfield_wf attr}")]]
+[[rc::requires("{bitfield_wf pte}", "{bitfield_wf pa}", "{bitfield_wf attr}")]]
 [[rc::requires("{type = (if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block)}")]]
 [[rc::requires("{pte1 = (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 |>}")]]

theories/lang/bitfield.v

@@ -37,10 +37,11 @@ Definition ensure_mv (R : Type) `{BitfieldDesc R} (t : tm) : option () :=
   if check_has_ty t (mv bitfield_sig) then Some () else None.
 
 Lemma ensure_mv_spec R `{BitfieldDesc R} t :
-  is_Some (ensure_mv R t) → has_ty t (mv bitfield_sig).
+  is_Some (ensure_mv R t) →
+  has_ty t (mv bitfield_sig).
 Proof.
   unfold ensure_mv. move => ?.
-  apply check_has_ty_spec.
+  apply check_has_ty_spec. { by rewrite check_has_ty_conditions_mv_nil. }
   have ? := is_Some_None. case_match; naive_solver.
 Qed.
 
@@ -48,10 +49,12 @@ Definition ensure_bv (R : Type) `{BitfieldDesc R} (t : tm) : option () :=
   if check_has_ty t (bv bitfield_sig) then Some () else None.
 
 Lemma ensure_bv_spec R `{BitfieldDesc R} t :
-  is_Some (ensure_bv R t) → has_ty t (bv bitfield_sig).
+  Forall id (check_has_ty_conditions t (bv bitfield_sig)) →
+  is_Some (ensure_bv R t) →
+  has_ty t (bv bitfield_sig).
 Proof.
-  unfold ensure_bv. move => ?.
-  apply check_has_ty_spec.
+  unfold ensure_bv. move => ??.
+  apply check_has_ty_spec => //.
   have ? := is_Some_None. repeat case_match; naive_solver.
 Qed.
 
@@ -62,10 +65,12 @@ Definition ensure_both_bv (R : Type) `{BitfieldDesc R} (tp : tm * tm) : option (
   end.
 
 Lemma ensure_both_bv_spec R `{BitfieldDesc R} t1 t2 :
+  Forall id (check_has_ty_conditions t1 (bv bitfield_sig)) →
+  Forall id (check_has_ty_conditions t2 (bv bitfield_sig)) →
   is_Some (ensure_both_bv R (t1, t2)) →
   has_ty t1 (bv bitfield_sig) ∧ has_ty t2 (bv bitfield_sig).
 Proof.
-  unfold ensure_both_bv. have ? := is_Some_None.
+  unfold ensure_both_bv => ??. have ? := is_Some_None.
   case_match; last naive_solver.
   rewrite andb_true_iff in Heqb. destruct Heqb as [? ?].
   move => ?. split; by apply check_has_ty_spec.
@@ -88,33 +93,34 @@ Lemma ensure_or_cond_spec R `{BitfieldDesc R} t1 t2 :
 Proof.
   move => ? ? Hs. econstructor; eauto.
   unfold ensure_or_cond in Hs. repeat case_match => //.
-  - right. by apply check_has_ty_spec.
+  - right. apply check_has_ty_spec => //. by rewrite check_has_ty_conditions_mv_nil.
   - left. by apply check_disjoint_spec.
 Qed.
 
-Definition ensure_or_cond_raw (R : Type) `{BitfieldDesc R} (tp : tm * tm) : option () :=
+Definition ensure_or_cond_raw (R : Type) `{BitfieldDesc R} (tp : tm * tm) : option bool :=
   match tp with (t1, t2) =>
-    if check_has_ty t2 (mv bitfield_sig) then Some ()
-    else if check_has_ty t2 (bv bitfield_sig) && check_disjoint (ranges t1) (ranges t2) then Some ()
+    if check_has_ty t2 (mv bitfield_sig) then Some false
+    else if check_has_ty t2 (bv bitfield_sig) && check_disjoint (ranges t1) (ranges t2) then Some true
     else None
   end.
 
-Lemma ensure_or_cond_raw_spec R `{BitfieldDesc R} t1 t2 :
+Lemma ensure_or_cond_raw_spec R `{BitfieldDesc R} t1 t2 b :
   has_ty t1 (bv bitfield_sig) →
-  is_Some (ensure_or_cond_raw R (t1, t2)) →
+  ensure_or_cond_raw R (t1, t2) = Some b →
+  (if b then Forall id (check_has_ty_conditions t2 (bv bitfield_sig)) else True) →
   has_ty (bf_or t1 t2) (bv bitfield_sig).
 Proof.
-  move => ? Hs. unfold ensure_or_cond_raw in Hs.
-  have ? := is_Some_None. repeat case_match; last naive_solver.
+  move => ? Hs ?. unfold ensure_or_cond_raw in Hs.
+  destruct (check_has_ty t2 (mv bitfield_sig)) eqn:?; simplify_eq.
   - econstructor; eauto.
-    * apply subsume_mv_bv. by apply check_has_ty_spec.
-    * right. by apply check_has_ty_spec.
-  - rewrite andb_true_iff in Heqb0. destruct Heqb0 as [? ?].
+    * apply subsume_mv_bv. apply check_has_ty_spec => //. by rewrite check_has_ty_conditions_mv_nil.
+    * right. apply check_has_ty_spec => //. by rewrite check_has_ty_conditions_mv_nil.
+  - destruct (check_has_ty t2 (bv bitfield_sig)) eqn:?; simplify_eq.
+    destruct (check_disjoint (ranges t1) (ranges t2)) => //; simplify_eq/=.
     econstructor; eauto.
     * by apply check_has_ty_spec.
     * left. by apply check_disjoint_spec.
 Qed.
-
 Definition ensure_eq (t1 t2 : tm) (it : int_type) : Prop :=
   check_eq (bits_per_int it) t1 t2.
 
@@ -177,7 +183,7 @@ Proof.
   destruct b.
   - rewrite bool_decide_eq_true. naive_solver.
   - rewrite bool_decide_eq_false. naive_solver.
-Qed. 
+Qed.
 
 Lemma bf_zb_spec R `{BitfieldDesc R} t :
   has_ty t (bv bitfield_sig) →

theories/mask_core/calculus.v

@@ -64,18 +64,22 @@ Record signature := {
   (* properties on ranges *)
   (* sig_disjoint : ∀ f1 f2, f1 ≠ f2 →
     (sig_ranges !!! f1 ≺ sig_ranges !!! f2) ∨ (sig_ranges !!! f2 ≺ sig_ranges !!! f1); *)
-  field_width f := width (sig_ranges !!! f);
-  recognize (r : range) : option (fin sig_length) :=
-    match filter (λ f, sig_ranges !!! f = r) (enum (fin sig_length)) with
-    | [] => None
-    | f :: _ => Some f
-    end;
   (* total bits *)
   sig_bits : nat;
   sig_max_range_bounded : ∃ r, last sig_ranges = Some r ∧
     offset r + width r ≤ sig_bits
 }.
 
+Definition field_width (σ : signature) f : nat :=
+  width (σ.(sig_ranges) !!! f).
+Arguments field_width _ !_ /.
+
+Definition recognize (σ : signature) (r : range) : option (fin σ.(sig_length)) :=
+    match filter (λ f, σ.(sig_ranges) !!! f = r) (enum (fin σ.(sig_length))) with
+    | [] => None
+    | f :: _ => Some f
+    end.
+
 Lemma sig_disjoint σ f1 f2 :
   f1 ≠ f2 →
   (sig_ranges σ !!! f1 ≺ sig_ranges σ !!! f2) ∨

theories/mask_core/typecheck.v

@@ -67,14 +67,46 @@ Fixpoint check_has_ty (t : tm) (τ : ty) : bool :=
   | _, _ => false
   end.
 
+Fixpoint check_has_ty_conditions (t : tm) (τ : ty) : list Prop :=
+  match t, τ with
+  | bf_val n, val σ f =>
+      [0 ≤ n < 2 ^ (field_width σ f)]
+  | bf_mask k, val σ f => []
+  | bf_nil, bv σ => []
+  | bf_cons r x t, bv σ =>
+    default [] (
+      f ← recognize σ r;
+      Some (check_has_ty_conditions x (val σ f) ++ check_has_ty_conditions t (bv σ))
+    )
+  | bf_slice r t, val σ f => check_has_ty_conditions t (bv σ)
+  | bf_update r x t, bv σ =>
+    default [] (
+      f ← recognize σ r;
+      Some (check_has_ty_conditions x (val σ f))
+    )
+  | bf_and t1 t2, bv σ =>
+    check_has_ty_conditions t1 (bv σ)
+  | bf_and_neg t1 t2, bv σ =>
+    check_has_ty_conditions t1 (bv σ)
+  | bf_or t1 t2, bv σ =>
+    check_has_ty_conditions t1 (bv σ) ++ check_has_ty_conditions t2 (bv σ)
+  | _, _ => []
+  end.
+
 Ltac destruct_option :=
   match goal with
   | |- context [ (?o ≫= _) ] =>
     destruct o eqn:Heqn; simpl; try done
   end.
 
+Lemma check_has_ty_conditions_mv_nil t σ :
+  check_has_ty_conditions t (mv σ) = [].
+Proof. by destruct t. Qed.
+
 Lemma check_has_ty_spec t τ :
-  check_has_ty t τ = true → ⊢ t : τ.
+  Forall id (check_has_ty_conditions t τ) →
+  check_has_ty t τ = true →
+  ⊢ t : τ.
 Proof.
   (* induction t; destruct τ; try case_match.
   all: simpl => //.
@@ -86,3 +118,12 @@ Proof.
   end.
   all: repeat (econstructor; eauto) => //. *)
 Admitted.
+
+Lemma has_ty_implies_check_has_ty_conditions t τ :
+  ⊢ t : τ →
+  Forall id (check_has_ty_conditions t τ).
+Proof.
+  revert τ. induction t => τ; destruct τ; try case_match.
+  all: simpl => //; inversion 1; simplify_option_eq.
+  all: rewrite ?Forall_app; eauto.
+Qed.

theories/typing/bitfield.v

@@ -343,16 +343,17 @@ Section programs.
       λ T, i2p (type_or_bitfield_tpd T R v1 v2 t1 t2).
 
   Lemma type_or_bitfield_tpd_raw T R `{BitfieldDesc R} it v1 v2 t1 t2 :
-    (tactic_hint (vm_compute_hint (ensure_or_cond_raw R) (t1, t2)) (λ _,
+    (tactic_hint (vm_compute_hint (ensure_or_cond_raw R) (t1, t2)) (λ b,
+      ⌜if b then Forall id (check_has_ty_conditions t2 (bv bitfield_sig)) else True⌝ ∗
       let norm := normalize (bf_or t1 t2) in
       T (i2v (bf_to_Z norm bitfield_it) bitfield_it) (t2mt (norm @ bitfield_tpd R)))) -∗
     typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_tpd R) v2 (v2 ◁ᵥ t2 @ bitfield_raw it) OrOp (IntOp it) (IntOp it) T.
   Proof.
     unfold tactic_hint, vm_compute_hint.
     remember (normalize (bf_or t1 t2)) as norm eqn:Heqn.
-    iIntros "[% [% HT]] [% Hv1] Hv2".
+    iIntros "[% [% [% HT]]] [% Hv1] Hv2".
     have Hty : has_ty (bf_or t1 t2) (bv bitfield_sig).
-    { apply ensure_or_cond_raw_spec => //. }
+    { by eapply ensure_or_cond_raw_spec. }
     have Hnorm : bf_to_Z norm bitfield_it = Z.lor (bf_to_Z t1 bitfield_it) (bf_to_Z t2 bitfield_it)
       by rewrite Heqn; rewrite normalize_preserves_bf_to_Z; eauto.
     iApply type_val_expr_mono_strong.
@@ -465,11 +466,12 @@ Section programs.
 
   Lemma subsume_place_bitfield_raw_tpd T it R `{BitfieldDesc R} l β t t' :
     (tactic_hint (vm_compute_hint (ensure_bv R) t') (λ _,
+      ⌜Forall id (check_has_ty_conditions t' (bv bitfield_sig))⌝ ∗
       ⌜it = bitfield_it⌝ ∗ ⌜bf_to_Z t bitfield_it = bf_to_Z t' bitfield_it⌝ ∗ T)) -∗
     subsume (l ◁ₗ{β} t @ bitfield_raw it) (l ◁ₗ{β} t' @ bitfield_tpd R) T.
   Proof.
     unfold tactic_hint, vm_compute_hint.
-    iIntros "[% [%Hty [-> [%Heq $]]]] Hl".
+    iIntros "[% [%Hty [% [-> [%Heq $]]]]] Hl".
     (* apply ensure_bv_spec in Hty as [? ?]. *)
     rewrite /ty_own /=. iSplitR.
     { iPureIntro. by apply ensure_bv_spec. }
@@ -503,23 +505,25 @@ Section programs.
     λ T1 T2, i2p (type_if_bitfield_tpd it R v t T1 T2).
 
   (* val eq *)
+  (* TODO: somehow the check_has_ty_conditions feels unnecessary *)
   Global Instance simple_subsume_val_bitfield_tpd R `{BitfieldDesc R} t1 t2 :
-    SimpleSubsumeVal (t1 @ bitfield_tpd R) (t2 @ bitfield_tpd R) (⌜ensure_eq t1 t2 bitfield_it⌝ ∗ ⌜is_Some (ensure_bv R t2)⌝) | 50.
+    SimpleSubsumeVal (t1 @ bitfield_tpd R) (t2 @ bitfield_tpd R) (⌜ensure_eq t1 t2 bitfield_it⌝ ∗ ⌜is_Some (ensure_bv R t2)⌝ ∗ ⌜Forall id (check_has_ty_conditions t1 (bv bitfield_sig)) → Forall id (check_has_ty_conditions t2 (bv bitfield_sig))⌝) | 50.
   Proof.
-    iIntros (v) "%Hyp [% Hv]".
-    destruct Hyp as [Heq Hty].
+    iIntros (v) "[%Heq [%Hty %Himpl]] [% Hv]".
     apply ensure_bv_spec in Hty.
+    2: { apply Himpl. by apply has_ty_implies_check_has_ty_conditions. }
     apply ensure_eq_spec in Heq => //.
     iSplitR => //.
     by rewrite /ty_own_val /= Heq.
   Qed.
 
+  (* TODO: somehow the check_has_ty_conditions feels unnecessary *)
   Global Instance simple_subsume_place_bitfield_tpd R `{BitfieldDesc R} t1 t2 :
-    SimpleSubsumePlace (t1 @ bitfield_tpd R) (t2 @ bitfield_tpd R) (⌜ensure_eq t1 t2 bitfield_it⌝ ∗ ⌜is_Some (ensure_bv R t2)⌝) | 50.
+    SimpleSubsumePlace (t1 @ bitfield_tpd R) (t2 @ bitfield_tpd R) (⌜ensure_eq t1 t2 bitfield_it⌝ ∗ ⌜is_Some (ensure_bv R t2)⌝ ∗ ⌜Forall id (check_has_ty_conditions t1 (bv bitfield_sig)) → Forall id (check_has_ty_conditions t2 (bv bitfield_sig))⌝) | 50.
   Proof.
-    iIntros (l β) "%Hyp Hl". rewrite /ty_own /=. iDestruct "Hl" as "[% Hl]".
-    destruct Hyp as [Heq Hty].
-    apply ensure_bv_spec in Hty.
+    iIntros (l β) "[%Heq [%Hty %Himpl]] Hl". rewrite /ty_own /=. iDestruct "Hl" as "[% Hl]".
+    apply ensure_bv_spec in Hty => //.
+    2: { apply Himpl. by apply has_ty_implies_check_has_ty_conditions. }
     apply ensure_eq_spec in Heq => //.
     iSplitR => //.
     by rewrite /ty_own /= Heq.
@@ -546,7 +550,7 @@ Section programs.
   Qed.
   Global Instance subsume_val_int_bitfield_raw_inst it v n bv : SubsumeVal v (n @ int it) (bv @ bitfield_raw it) :=
     λ T, i2p (subsume_val_int_bitfield_raw T it v n bv).
-  
+
   Lemma subsume_place_int_bitfield_raw T it l β n bv :
     (⌜n = bv⌝ ∗ T) -∗ subsume (l ◁ₗ{β} n @ int it) (l ◁ₗ{β} bv @ bitfield_raw it) T.
   Proof.