Expansion of Ccompimm in RTL [Admitted checker]

1 files changed, 92 insertions, 2 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index 2271ecd2..c55479ff 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -152,7 +152,14 @@ Inductive operation : Type :=
   | Osingleoflong            (**r [rd = float32_of_signed_long(r1)] *)
   | Osingleoflongu           (**r [rd = float32_of_unsigned_int(r1)] *)
 (*c Boolean tests: *)
-  | Ocmp (cond: condition).  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
+  | OEseqw (optR0: option bool)                  (**r [rd <- rs1 == rs2] (pseudo) *)
+  | OEsnew (optR0: option bool)                  (**r [rd <- rs1 != rs2] (pseudo) *)
+  | OEsltw (optR0: option bool)                  (**r set-less-than *)
+  | OEsltiw (n: int)                             (**r set-less-than immediate *)
+  | OExoriw (n: int)                             (**r xor immediate *)
+  | OEluiw (n: int)                              (**r load upper-immediate *)
+  | OEaddiwr0 (n: int).                          (**r add immediate *)
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -179,8 +186,9 @@ Defined.
 
 Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition; intros.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition bool_dec; intros.
   decide equality.
+  all: destruct optR0, optR1; decide equality.
 Defined.
 
 (* Alternate definition: 
@@ -203,6 +211,15 @@ Global Opaque eq_condition eq_addressing eq_operation.
   to lists of values.  Return [None] when the computation can trigger an
   error, e.g. integer division by zero.  [eval_condition] returns a boolean,
   [eval_operation] and [eval_addressing] return a value. *)
+  
+Definition zero32 := (Vint Int.zero).
+  
+Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 vz: val): B :=
+  match optR0 with
+  | None => sem v1 v2
+  | Some true => sem vz v1
+  | Some false => sem v1 vz
+  end.
 
 Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
   match cond, vl with
@@ -318,6 +335,13 @@ Definition eval_operation
   | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1))
   | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1))
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
+  | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
+  | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
+  | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32)
+  | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
+  | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
+  | OEluiw n, nil => Some(Vint (Int.shl n (Int.repr 12)))
+  | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
   | _, _ => None
   end.
 
@@ -474,6 +498,13 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osingleoflong => (Tlong :: nil, Tsingle)
   | Osingleoflongu => (Tlong :: nil, Tsingle)
   | Ocmp c => (type_of_condition c, Tint)
+  | OEseqw _ => (Tint :: Tint :: nil, Tint)
+  | OEsnew _ => (Tint :: Tint :: nil, Tint)
+  | OEsltw _ => (Tint :: Tint :: nil, Tint)
+  | OEsltiw _ => (Tint :: nil, Tint)
+  | OExoriw _ => (Tint :: nil, Tint)
+  | OEluiw _ => (nil, Tint)
+  | OEaddiwr0 _ => (nil, Tint)
   end.
 
 Definition type_of_addressing (addr: addressing) : list typ :=
@@ -680,6 +711,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; cbn; trivial.
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
+  
+- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+  destruct Val.cmpu_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+  destruct Val.cmpu_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmp;
+  destruct Val.cmp_bool... all: destruct b...
+- unfold Val.cmp; destruct Val.cmp_bool...
+  all: destruct b...
+- destruct v0...
+- trivial.
+- trivial.
 Qed.
 
 (* This should not be simplified to "false" because it breaks proofs elsewhere. *)
@@ -870,6 +913,8 @@ Definition cond_depends_on_memory (cond : condition) : bool :=
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
   | Ocmp cmp => cond_depends_on_memory cmp
+  | OEseqw _ => negb Archi.ptr64
+  | OEsnew _ => negb Archi.ptr64
   | _ => false
   end.
 
@@ -893,6 +938,11 @@ Proof.
   intros until m2. destruct op; simpl; try congruence.
   intro DEPEND.
   f_equal. f_equal. apply cond_depends_on_memory_correct; trivial.
+  all: intros; repeat (destruct args; auto);
+       unfold Val.cmpu, Val.cmpu_bool;
+       destruct optR0 as [[]|]; simpl;
+       destruct v, v0; simpl; auto;
+       apply negb_false_iff in H; try rewrite H; auto.
 Qed.
 
 Lemma cond_valid_pointer_eq:
@@ -913,6 +963,10 @@ Proof.
   intros until m2. destruct op; simpl; try congruence.
   intros MEM; destruct cond; repeat (destruct args; simpl; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
+  all: intros MEM; repeat (destruct args; simpl; try congruence);
+       try destruct optR0 as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto;
+       unfold Val.cmpu;
+       erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -1040,6 +1094,34 @@ Proof.
 - inv H3; inv H2; simpl in H0; inv H0; auto.
 Qed.
 
+Lemma eval_cmpu_bool_inj': forall b c v v' v0 v0',
+  Val.inject f v v' ->
+  Val.inject f v0 v0' ->
+  Val.cmpu_bool (Mem.valid_pointer m1) c v v0 = Some b ->
+  Val.cmpu_bool (Mem.valid_pointer m2) c v' v0' = Some b.
+Proof.
+  intros.
+  eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
+Qed.
+
+Lemma eval_cmpu_bool_inj: forall c v v' v0 v'0 optR0,
+  Val.inject f v v' ->
+  Val.inject f v0 v'0 ->
+  Val.inject f (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32)
+  (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32).
+Proof.
+  intros until optR0. intros HV1 HV2.
+  destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmpu; 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto;
+  assert (HVI: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int.
+  + exploit eval_cmpu_bool_inj'. eapply HVI. eapply HV1. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+  + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+  + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
+    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+Qed.
+
 Ltac TrivialExists :=
   match goal with
   | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] =>
@@ -1246,6 +1328,14 @@ Proof.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
     destruct b; simpl; constructor.
     simpl; constructor.
+
+  - apply eval_cmpu_bool_inj; auto.
+  - apply eval_cmpu_bool_inj; auto.
+  - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp;
+    inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto;
+    try apply Val.inject_int.
+  - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int.
+  - inv H4; simpl; auto.
 Qed.
 
 Lemma eval_addressing_inj: