From 3e47c1b17e8ff03400106a80117eb86d7e7f9da6 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Feb 2021 13:30:57 +0100 Subject: Expansion of Ccompimm in RTL [Admitted checker] --- riscV/Op.v | 94 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 92 insertions(+), 2 deletions(-) (limited to 'riscV/Op.v') 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: -- cgit