From 43e7b6702a76306f20687bc9aba93ae465d6e4be Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 14 Apr 2019 10:47:14 +0200 Subject: Implement a `Osel` operation for PowerPC This operation compiles down to an `isel` instruction (conditional move). The semantics is given by `Val.select`. --- powerpc/Asmgen.v | 16 ++++++++++++++++ powerpc/Asmgenproof.v | 10 ++++++++++ powerpc/Asmgenproof1.v | 35 +++++++++++++++++++++++++++++++++++ powerpc/NeedOp.v | 5 +++++ powerpc/Op.v | 43 ++++++++++++++++++++++++++++++++++--------- powerpc/PrintOp.ml | 4 ++++ powerpc/ValueAOp.v | 2 ++ 7 files changed, 106 insertions(+), 9 deletions(-) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index dba24a5a..62efc17f 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -404,6 +404,18 @@ Definition transl_cond_op else Pxori r' r' (Cint Int.one) :: k) end. +(** Translation of a select operation *) + +Definition transl_select_op + (cond: condition) (args: list mreg) (r1 r2 rd: ireg) (k: code) := + if ireg_eq r1 r2 then + OK (Pmr rd r1 :: k) + else + (let p := crbit_for_cond cond in + let r1' := if snd p then r1 else r2 in + let r2' := if snd p then r2 else r1 in + transl_cond cond args (Pisel rd r1' r2' (fst p) :: k)). + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -610,6 +622,10 @@ Definition transl_op do r1 <- ireg_of a1; do r <- ireg_of res; OK (Plhi r r1 :: k) | Ocmp cmp, _ => transl_cond_op cmp args res k + | Osel cmp ty, a1 :: a2 :: args => + assertion (typ_eq ty Tint || typ_eq ty Tlong); + do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; + transl_select_op cmp args r1 r2 r k (*c PPC64 operations *) | Olongconst n, nil => do r <- ireg_of res; OK (loadimm64 r n k) diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index d0d82cb5..4d0b41ba 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -248,6 +248,15 @@ Proof. destruct (snd (crbit_for_cond c0)); TailNoLabel. Qed. +Remark transl_select_op_label: + forall cond args r1 r2 rd k c, + transl_select_op cond args r1 r2 rd k = OK c -> tail_nolabel k c. +Proof. + unfold transl_select_op; intros. destruct (ireg_eq r1 r2). + TailNoLabel. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. +Qed. + Remark transl_op_label: forall op args r k c, transl_op op args r k = OK c -> tail_nolabel k c. @@ -275,6 +284,7 @@ Opaque Int.eq. destruct Int64.eq. TailNoLabel. destruct ireg_eq; [apply tail_nolabel_cons; unfold nolabel;auto|]; eapply tail_nolabel_trans; TailNoLabel. - eapply transl_cond_op_label; eauto. +- eapply transl_select_op_label; eauto. Qed. Remark transl_memory_access_label: diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index b891e42f..8c9fd2bd 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1258,6 +1258,35 @@ Proof. intuition Simpl. rewrite RES1. destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto. Qed. + +Lemma transl_select_op_correct: + forall cond args ty r1 r2 rd k rs m c, + transl_select_op cond args r1 r2 rd k = OK c -> + important_preg r1 = true -> important_preg r2 = true -> + exists rs', + exec_straight ge fn c rs m k rs' m + /\ Val.lessdef (Val.select (eval_condition cond (map rs (map preg_of args)) m) rs#r1 rs#r2 ty) rs'#rd + /\ forall r, important_preg r = true -> r <> rd -> rs'#r = rs#r. +Proof. + intros until c. intros TR IMP1 IMP2. + unfold transl_select_op in TR. + destruct (ireg_eq r1 r2). + - inv TR. econstructor; split; [|split]. + + apply exec_straight_one. simpl; eauto. auto. + + Simpl. destruct (eval_condition cond rs ## (preg_of ## args) m) as [[]|]; simpl; auto using Val.lessdef_normalize. + + intros; Simpl. + - destruct (transl_cond_correct_1 cond args _ rs m _ TR) as (rs1 & A & B & C). + set (bit := fst (crbit_for_cond cond)) in *. + set (dir := snd (crbit_for_cond cond)) in *. + set (ob := eval_condition cond rs##(preg_of##args) m) in *. + econstructor; split; [|split]. + + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. + reflexivity. + + Simpl. + rewrite <- (C r1), <- (C r2) by auto. + rewrite B. destruct dir; destruct ob as [[]|]; simpl; auto using Val.lessdef_normalize. + + intros. Simpl. +Qed. (** Translation of arithmetic operations. *) @@ -1455,6 +1484,12 @@ Opaque Val.add. (* Ocmp *) - destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto. exists rs'; auto with asmgen. + (* Osel *) +- assert (X: forall mr r, ireg_of mr = OK r -> important_preg r = true). + { intros. apply ireg_of_eq in H. apply important_data_preg_1. rewrite <- H. + auto with asmgen. } + destruct (transl_select_op_correct _ _ t _ _ _ _ rs m _ EQ3) as (rs' & A & B & C); + eauto. Qed. Lemma transl_op_correct: diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 9a579cc5..5ea09bd8 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -65,6 +65,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ofloatofwords | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocmp c => needs_of_condition c + | Osel c ty => nv :: nv :: needs_of_condition c end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -147,6 +148,10 @@ Proof. erewrite needs_of_condition_sound by eauto. subst v; simpl. auto with na. subst v; auto with na. +- destruct (eval_condition c args m) as [b|] eqn:EC. + erewrite needs_of_condition_sound by eauto. + apply select_sound; auto. + simpl; auto with na. Qed. Lemma operation_is_redundant_sound: diff --git a/powerpc/Op.v b/powerpc/Op.v index e6f942c1..0f082c1f 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -150,8 +150,9 @@ Inductive operation : Type := | Olowlong: operation (**r [rd = low-word(r1)] *) | Ohighlong: operation (**r [rd = high-word(r1)] *) (*c Boolean tests: *) - | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) - + | Ocmp: condition -> operation (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + | Osel: condition -> typ -> operation. + (**r [rd = rs1] if condition holds, [rd = rs2] otherwise. *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -173,7 +174,7 @@ Proof. Defined. Definition beq_operation: forall (x y: operation), bool. - generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec eq_condition; boolean_equality. + generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec typ_eq eq_condition; boolean_equality. Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. @@ -306,6 +307,7 @@ Definition eval_operation | Olowlong, v1::nil => Some(Val.loword v1) | Ohighlong, v1::nil => Some(Val.hiword v1) | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m)) + | Osel c ty, v1::v2::vl => Some(Val.select (eval_condition c vl m) v1 v2 ty) | _, _ => None end. @@ -455,6 +457,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Olowlong => (Tlong :: nil, Tint) | Ohighlong => (Tlong :: nil, Tint) | Ocmp c => (type_of_condition c, Tint) + | Osel c ty => (ty :: ty :: type_of_condition c, ty) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -575,6 +578,7 @@ Proof with (try exact I; try reflexivity). destruct v0... destruct v0... destruct (eval_condition c vl m); simpl... destruct b... + unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I. Qed. End SOUNDNESS. @@ -727,22 +731,40 @@ Definition is_trivial_op (op: operation) : bool := (** Operations that depend on the memory state. *) +Definition condition_depends_on_memory (c: condition) : bool := + match c with + | Ccompu _ => true + | Ccompuimm _ _ => true + | Ccomplu _ => Archi.ppc64 + | Ccompluimm _ _ => Archi.ppc64 + | _ => false + end. + Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp (Ccompu _) => true - | Ocmp (Ccompuimm _ _) => true - | Ocmp (Ccomplu _) => Archi.ppc64 - | Ocmp (Ccompluimm _ _) => Archi.ppc64 + | Ocmp c => condition_depends_on_memory c + | Osel c ty => condition_depends_on_memory c | _ => false end. +Lemma condition_depends_on_memory_correct: + forall c args m1 m2, + condition_depends_on_memory c = false -> + eval_condition c args m1 = eval_condition c args m2. +Proof. + intros. destruct c; simpl; auto; discriminate. +Qed. + Lemma op_depends_on_memory_correct: forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, op_depends_on_memory op = false -> eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. - intros until m2. destruct op; simpl; try congruence. unfold eval_condition. - destruct c; simpl; auto; try discriminate. + intros until m2. destruct op; simpl; try congruence; intros C. +- f_equal; f_equal; apply condition_depends_on_memory_correct; auto. +- destruct args; auto. destruct args; auto. + rewrite (condition_depends_on_memory_correct c args m1 m2 C). + auto. Qed. (** Global variables mentioned in an operation or addressing mode *) @@ -989,6 +1011,9 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. + apply Val.select_inject; auto. + destruct (eval_condition c vl1 m1) eqn:?; auto. + right; symmetry; eapply eval_condition_inj; eauto. Qed. Lemma eval_addressing_inj: diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index cffaafdb..8d7f17ab 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -110,6 +110,10 @@ let print_operation reg pp = function | Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1 | Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) + | Osel (c, ty), r1::r2::args -> + fprintf pp "%a ?%s %a : %a" + (print_condition reg) (c, args) + (PrintAST.name_of_type ty) reg r1 reg r2 | Olongconst n, [] -> fprintf pp "%LdL" (camlint64_of_coqint n) | Ocast32signed, [r1] -> fprintf pp "int32signed(%a)" reg r1 | Ocast32unsigned, [r1] -> fprintf pp "int32unsigned(%a)" reg r1 diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index f7f65e9e..a270d857 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -141,6 +141,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Olowlong, v1::nil => loword v1 | Ohighlong, v1::nil => hiword v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) + | Osel c ty, v1::v2::vl => select (eval_static_condition c vl) v1 v2 | _, _ => Vbot end. @@ -211,6 +212,7 @@ Proof. apply rolml_sound; auto. apply floatofwords_sound; auto. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. + apply select_sound; auto. eapply eval_static_condition_sound; eauto. Qed. End SOUNDNESS. -- cgit