Ccompu expansion

1 files changed, 32 insertions, 6 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index c55479ff..4de168cc 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -156,7 +156,9 @@ Inductive operation : Type :=
   | 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 *)
+  | OEsltuw (optR0: option bool)                 (**r set-less-than unsigned *)
   | OEsltiw (n: int)                             (**r set-less-than immediate *)
+  | OEsltiuw (n: int)                             (**r set-less-than unsigned immediate *)
   | OExoriw (n: int)                             (**r xor immediate *)
   | OEluiw (n: int)                              (**r load upper-immediate *)
   | OEaddiwr0 (n: int).                          (**r add immediate *)
@@ -338,7 +340,9 @@ Definition eval_operation
   | 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)
+  | OEsltuw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32)
   | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
+  | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) 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)
@@ -501,7 +505,9 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEseqw _ => (Tint :: Tint :: nil, Tint)
   | OEsnew _ => (Tint :: Tint :: nil, Tint)
   | OEsltw _ => (Tint :: Tint :: nil, Tint)
+  | OEsltuw _ => (Tint :: Tint :: nil, Tint)
   | OEsltiw _ => (Tint :: nil, Tint)
+  | OEsltiuw _ => (Tint :: nil, Tint)
   | OExoriw _ => (Tint :: nil, Tint)
   | OEluiw _ => (nil, Tint)
   | OEaddiwr0 _ => (nil, Tint)
@@ -718,8 +724,11 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   destruct Val.cmpu_bool... all: destruct b...
 - destruct optR0 as [[]|]; simpl; unfold Val.cmp;
   destruct Val.cmp_bool... all: destruct b...
+- destruct optR0 as [[]|]; simpl; unfold Val.cmpu;
+  destruct Val.cmpu_bool... all: destruct b...
 - unfold Val.cmp; destruct Val.cmp_bool...
   all: destruct b...
+- unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
 - destruct v0...
 - trivial.
 - trivial.
@@ -915,6 +924,8 @@ Definition op_depends_on_memory (op: operation) : bool :=
   | Ocmp cmp => cond_depends_on_memory cmp
   | OEseqw _ => negb Archi.ptr64
   | OEsnew _ => negb Archi.ptr64
+  | OEsltiuw _ => negb Archi.ptr64
+  | OEsltuw _ => negb Archi.ptr64
   | _ => false
   end.
 
@@ -940,8 +951,8 @@ Proof.
   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;
+       try destruct optR0 as [[]|]; simpl;
+       destruct v; try destruct v0; simpl; auto;
        apply negb_false_iff in H; try rewrite H; auto.
 Qed.
 
@@ -1104,7 +1115,20 @@ Proof.
   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,
+Lemma eval_cmpu_bool_inj: forall c v v' v0 v'0,
+  Val.inject f v v' ->
+  Val.inject f v0 v'0 ->
+  Val.inject f (Val.cmpu (Mem.valid_pointer m1) c v v0)
+  (Val.cmpu (Mem.valid_pointer m2) c v' v'0).
+Proof.
+  intros until v'0. intros HV1 HV2.
+  unfold Val.cmpu; 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m1) c _ _) eqn:?; eauto.
+  exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
+  intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+Qed.
+
+Lemma eval_cmpu_bool_inj_opt: 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)
@@ -1329,12 +1353,14 @@ Proof.
     destruct b; simpl; constructor.
     simpl; constructor.
 
-  - apply eval_cmpu_bool_inj; auto.
-  - apply eval_cmpu_bool_inj; auto.
+  - apply eval_cmpu_bool_inj_opt; auto.
+  - apply eval_cmpu_bool_inj_opt; 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.
+  - apply eval_cmpu_bool_inj_opt; auto.
   - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int.
+  - apply eval_cmpu_bool_inj; auto.
   - inv H4; simpl; auto.
 Qed.
 
@@ -1593,4 +1619,4 @@ Definition builtin_arg_ok
   match ba with
   | (BA _ | BA_splitlong (BA _) (BA _)) => true
   | _ => builtin_arg_ok_1 ba c
-  end.  
+  end.