From 4df03aaf5204d2f15885b49fe3f5c9cb61b4596d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Feb 2021 18:31:46 +0100 Subject: Ccompu expansion --- riscV/Op.v | 38 ++++++++++++++++++++++++++++++++------ 1 file changed, 32 insertions(+), 6 deletions(-) (limited to 'riscV/Op.v') 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. -- cgit