From 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 3 Feb 2021 17:14:23 +0100 Subject: All Ocmp expanded in RTL --- riscV/Op.v | 44 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) (limited to 'riscV/Op.v') diff --git a/riscV/Op.v b/riscV/Op.v index ae38f361..1ca6f2e9 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -171,7 +171,13 @@ Inductive operation : Type := | OExoril (n: int64) (**r xor immediate *) | OEluil (n: int64) (**r load upper-immediate *) | OEaddilr0 (n: int64) (**r add immediate *) - | OEloadli (n: int64). (**r load an immediate int64 *) + | OEloadli (n: int64) (**r load an immediate int64 *) + | OEfeqd (**r compare equal *) + | OEfltd (**r compare less-than *) + | OEfled (**r compare less-than/equal *) + | OEfeqs (**r compare equal *) + | OEflts (**r compare less-than *) + | OEfles. (**r compare less-than/equal *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -367,6 +373,12 @@ Definition eval_operation | OEluil n, nil => Some(Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64) | OEloadli n, nil => Some (Vlong n) + | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2) + | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2) + | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2) + | OEfeqs, v1::v2::nil => Some (Val.cmpfs Ceq v1 v2) + | OEflts, v1::v2::nil => Some (Val.cmpfs Clt v1 v2) + | OEfles, v1::v2::nil => Some (Val.cmpfs Cle v1 v2) | _, _ => None end. @@ -542,6 +554,12 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEluil _ => (nil, Tlong) | OEaddilr0 _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) + | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) + | OEfltd => (Tfloat :: Tfloat :: nil, Tint) + | OEfled => (Tfloat :: Tfloat :: nil, Tint) + | OEfeqs => (Tsingle :: Tsingle :: nil, Tint) + | OEflts => (Tsingle :: Tsingle :: nil, Tint) + | OEfles => (Tsingle :: Tsingle :: nil, Tint) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -778,6 +796,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - trivial. - trivial. - trivial. +- destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. +- destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. +- destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. +- destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. +- destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. +- destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. Qed. (* This should not be simplified to "false" because it breaks proofs elsewhere. *) @@ -1462,6 +1492,18 @@ Proof. - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int. - apply eval_cmplu_bool_inj; auto. - inv H4; simpl; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. Qed. Lemma eval_addressing_inj: -- cgit