From 49342474c19558709c8cea6d70eaba9a4dd7a150 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 15 Apr 2019 17:50:30 +0200 Subject: Implement a `Osel` operation for ARM The operation comples down to conditional moves. Both integer and floating-point conditional moves are supported. --- arm/Asm.v | 9 +++++++++ arm/AsmToJSON.ml | 3 ++- arm/Asmgen.v | 13 +++++++++++++ arm/Asmgenproof.v | 1 + arm/Asmgenproof1.v | 25 ++++++++++++++++++++++++- arm/NeedOp.v | 5 +++++ arm/Op.v | 37 ++++++++++++++++++++++++++++++++----- arm/PrintOp.ml | 4 ++++ arm/SelectOp.vp | 3 +++ arm/SelectOpproof.v | 14 ++++++++++++++ arm/TargetPrinter.ml | 6 ++++++ arm/ValueAOp.v | 2 ++ 12 files changed, 115 insertions(+), 7 deletions(-) diff --git a/arm/Asm.v b/arm/Asm.v index e6d1b4fc..194074ac 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -220,6 +220,7 @@ Inductive instruction : Type := | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> ptrofs -> instruction (**r load the address of a symbol *) | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *) + | Pfmovite: testcond -> freg -> freg -> freg -> instruction (**r FP conditional move *) | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *) | Padc: ireg -> ireg -> shift_op -> instruction (**r add with carry *) @@ -783,6 +784,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | None => Vundef end in Next (nextinstr (rs#r1 <- v)) m + | Pfmovite cond r1 ifso ifnot => + let v := + match eval_testcond cond rs with + | Some true => rs#ifso + | Some false => rs#ifnot + | None => Vundef + end in + Next (nextinstr (rs#r1 <- v)) m | Pbtbl r tbl => match rs#r with | Vint n => diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index 3874e141..dfad6972 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -259,7 +259,8 @@ let pp_instructions pp ic = | Pmla(r1, r2, r3, r4) -> instruction pp "Pmla" [Ireg r1; Ireg r2; Ireg r3; Ireg r4] | Pmov(r1, so) -> instruction pp "Pmov" [Ireg r1; Shift so] | Pmovite(cond, r1, so1, so2) -> instruction pp "Pmovite" [Ireg r1; Condition (TargetPrinter.condition_name cond); Shift so1; Condition (TargetPrinter.neg_condition_name cond); Shift so2] - | Pmovt(r1, n) -> instruction pp "Pmovt" [Ireg r1; Long n] + | Pfmovite(cond, r1, r2, r3) -> instruction pp "Pfmovite" [DFreg r1; Condition (TargetPrinter.condition_name cond); DFreg r2; Condition (TargetPrinter.neg_condition_name cond); DFreg r3] + | Pmovt(r1, n) -> instruction pp "Pmovt" [Ireg r1; Long n] | Pmovw(r1, n) -> instruction pp "Pmovw" [Ireg r1; Long n] | Pmul(r1, r2, r3) -> instruction pp "Pmul" [Ireg r1; Ireg r2; Ireg r3] | Pmvn(r1, so) -> instruction pp "Pmvn" [Ireg r1; Shift so] diff --git a/arm/Asmgen.v b/arm/Asmgen.v index f12ea870..1a1e7f2f 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -555,6 +555,19 @@ Definition transl_op do r <- ireg_of res; transl_cond cmp args (Pmovite (cond_for_cond cmp) r (SOimm Int.one) (SOimm Int.zero) :: k) + | Osel cmp ty, a1 :: a2 :: args => + match preg_of res with + | IR r => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + transl_cond cmp args + (Pmovite (cond_for_cond cmp) r (SOreg r1) (SOreg r2) :: k) + | FR r => + do r1 <- freg_of a1; do r2 <- freg_of a2; + transl_cond cmp args + (Pfmovite (cond_for_cond cmp) r r1 r2 :: k) + | _ => + Error(msg "Asmgen.Osel") + end | _, _ => Error(msg "Asmgen.transl_op") end. diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 2c001f45..25f91d23 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -270,6 +270,7 @@ Opaque Int.eq. destruct Archi.thumb2_support; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. + destruct (preg_of r); monadInv H; (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto|TailNoLabel]). Qed. Remark transl_memory_access_label: diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index edf35bb8..807e069d 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -1189,7 +1189,7 @@ Lemma transl_op_correct_same: forall op args res k c (rs: regset) m v, transl_op op args res k = OK c -> eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v -> - match op with Ocmp _ => False | Oaddrstack _ => False | _ => True end -> + match op with Ocmp _ => False | Osel _ _ => False | Oaddrstack _ => False | _ => True end -> exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of res) = v @@ -1333,6 +1333,8 @@ Transparent destroyed_by_op. intuition Simpl. (* Ocmp *) contradiction. + (* Osel *) + contradiction. Qed. Lemma transl_op_correct: @@ -1369,6 +1371,27 @@ Proof. split; intros; Simpl. destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto. destruct B as [B1 B2]; rewrite B1. destruct b; auto. +- (* Osel *) + clear SAME. simpl in H. ArgsInv. simpl in H0; inv H0. + assert (D1: data_preg (preg_of m0) = true) by auto with asmgen. + assert (D2: data_preg (preg_of m1) = true) by auto with asmgen. + destruct (preg_of res) eqn:RES; monadInv H. ++ inv EQ2. rewrite (ireg_of_eq _ _ EQ), (ireg_of_eq _ _ EQ1) in *. + exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + rewrite ! C by auto. + destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto. + destruct B as [B1 B2]; rewrite B1. destruct b; apply Val.lessdef_normalize. ++ inv EQ2. rewrite (freg_of_eq _ _ EQ), (freg_of_eq _ _ EQ1) in *. + exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. + split; intros; Simpl. + rewrite ! C by auto. + destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto. + destruct B as [B1 B2]; rewrite B1. destruct b; apply Val.lessdef_normalize. Qed. (** Translation of loads and stores. *) diff --git a/arm/NeedOp.v b/arm/NeedOp.v index dee7cae1..c70c7e40 100644 --- a/arm/NeedOp.v +++ b/arm/NeedOp.v @@ -83,6 +83,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | 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 := @@ -183,6 +184,10 @@ Proof. - apply notint_sound; auto. - apply notint_sound. apply needs_of_shift_sound; auto. - apply needs_of_shift_sound; auto. +- 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/arm/Op.v b/arm/Op.v index 8e1cd367..cc90e043 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -140,7 +140,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. *) @@ -174,7 +176,7 @@ Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intros. + generalize Int.eq_dec Ptrofs.eq_dec ident_eq typ_eq; intros. generalize Float.eq_dec Float32.eq_dec; intros. generalize eq_shift; intro. generalize eq_condition; intro. @@ -294,6 +296,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. @@ -419,6 +422,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 := @@ -511,6 +515,7 @@ Proof with (try exact I; try reflexivity). destruct v0... destruct v0... destruct (eval_condition c vl m)... destruct b... + unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I. Qed. End SOUNDNESS. @@ -682,19 +687,37 @@ 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 _ | Ccompushift _ _| Ccompuimm _ _ => true + | _ => false + end. + Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp (Ccompu _ | Ccompushift _ _| Ccompuimm _ _) => true + | 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. - intros. destruct c; simpl; auto; congruence. + 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 *) @@ -929,6 +952,10 @@ 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/arm/PrintOp.ml b/arm/PrintOp.ml index 642fff80..d74acf3f 100644 --- a/arm/PrintOp.ml +++ b/arm/PrintOp.ml @@ -129,6 +129,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 | _ -> fprintf pp "" let print_addressing reg pp = function diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index c361df65..61ea6283 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -382,6 +382,9 @@ Definition compf (c: comparison) (e1: expr) (e2: expr) := Definition compfs (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). +Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) := + Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)). + (** ** Integer conversions *) Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index d4aac9b6..f281f7ce 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -735,6 +735,20 @@ Proof. intros; red; intros. unfold compfs. TrivialExists. Qed. +Theorem eval_select: + forall le ty cond al vl a1 v1 a2 v2 a b, + select ty cond al a1 a2 = Some a -> + eval_exprlist ge sp e m le al vl -> + eval_expr ge sp e m le a1 v1 -> + eval_expr ge sp e m le a2 v2 -> + eval_condition cond vl m = Some b -> + exists v, + eval_expr ge sp e m le a v + /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v. +Proof. + unfold select; intros; inv H. rewrite <- H3; TrivialExists. +Qed. + Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). Proof. red; intros until x. unfold cast8signed; case (cast8signed_match a); intros. diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 20989615..64448648 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -443,6 +443,12 @@ struct (condition_name cond) ireg r1 shift_op ifso; fprintf oc " mov%s %a, %a\n" (neg_condition_name cond) ireg r1 shift_op ifnot + | Pfmovite(cond, r1, ifso, ifnot) -> + fprintf oc " ite %s\n" (condition_name cond); + fprintf oc " vmov%s %a, %a\n" + (condition_name cond) freg r1 freg ifso; + fprintf oc " vmov%s %a, %a\n" + (neg_condition_name cond) freg r1 freg ifnot | Pbtbl(r, tbl) -> if !Clflags.option_mthumb then begin fprintf oc " lsl r14, %a, #2\n" ireg r; diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v index e19ddd6d..a3fd9d7d 100644 --- a/arm/ValueAOp.v +++ b/arm/ValueAOp.v @@ -127,6 +127,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. @@ -205,6 +206,7 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. fold (Val.sub (Vint i) a1). auto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. + apply select_sound; auto. eapply eval_static_condition_sound; eauto. Qed. End SOUNDNESS. -- cgit