From 996f2e071baaf52105714283d141af2eac8ffbfb Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 15 Apr 2019 15:21:49 +0200 Subject: Implement a `Osel` operation for x86 The operation compiles down to conditional moves. --- x86/Asm.v | 11 ++-- x86/Asmgen.v | 33 +++++++++++ x86/Asmgenproof.v | 15 ++++- x86/Asmgenproof1.v | 164 +++++++++++++++++++++++++++++++++++++++++++++------- x86/Machregs.v | 1 + x86/NeedOp.v | 5 ++ x86/Op.v | 45 +++++++++++--- x86/PrintOp.ml | 4 ++ x86/SelectOp.vp | 30 +++++++++- x86/SelectOpproof.v | 26 +++++++++ x86/ValueAOp.v | 2 + 11 files changed, 298 insertions(+), 38 deletions(-) (limited to 'x86') diff --git a/x86/Asm.v b/x86/Asm.v index 32235c2d..58e28c40 100644 --- a/x86/Asm.v +++ b/x86/Asm.v @@ -851,11 +851,12 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Ptestq_ri r1 n => Next (nextinstr (compare_longs (Val.andl (rs r1) (Vlong n)) (Vlong Int64.zero) rs m)) m | Pcmov c rd r1 => - match eval_testcond c rs with - | Some true => Next (nextinstr (rs#rd <- (rs#r1))) m - | Some false => Next (nextinstr rs) m - | None => Next (nextinstr (rs#rd <- Vundef)) m - end + let v := + match eval_testcond c rs with + | Some b => if b then rs#r1 else rs#rd + | None => Vundef + end in + Next (nextinstr (rs#rd <- v)) m | Psetcc c rd => Next (nextinstr (rs#rd <- (Val.of_optbool (eval_testcond c rs)))) m (** Arithmetic operations over double-precision floats *) diff --git a/x86/Asmgen.v b/x86/Asmgen.v index dedbfbe6..73e3263e 100644 --- a/x86/Asmgen.v +++ b/x86/Asmgen.v @@ -305,6 +305,35 @@ Definition mk_jcc (cond: extcond) (lbl: label) (k: code) := | Cond_or c1 c2 => Pjcc c1 lbl :: Pjcc c2 lbl :: k end. +Definition negate_testcond (c: testcond) : testcond := + match c with + | Cond_e => Cond_ne | Cond_ne => Cond_e + | Cond_b => Cond_ae | Cond_be => Cond_a + | Cond_ae => Cond_b | Cond_a => Cond_be + | Cond_l => Cond_ge | Cond_le => Cond_g + | Cond_ge => Cond_l | Cond_g => Cond_le + | Cond_p => Cond_np | Cond_np => Cond_p + end. + +Definition mk_sel (cond: extcond) (rd r2: ireg) (k: code) := + match cond with + | Cond_base c => + OK (Pcmov (negate_testcond c) rd r2 :: k) + | Cond_and c1 c2 => + OK (Pcmov (negate_testcond c1) rd r2 :: + Pcmov (negate_testcond c2) rd r2 :: k) + | Cond_or c1 c2 => + Error (msg "Asmgen.mk_sel") (**r should never happen, see [SelectOp.select] *) + end. + +Definition transl_sel + (cond: condition) (args: list mreg) (rd r2: ireg) (k: code) : res code := + if ireg_eq rd r2 then + OK (Pmov_rr rd r2 :: k) (* must generate one instruction... *) + else + do k1 <- mk_sel (testcond_for_condition cond) rd r2 k; + transl_cond cond args k1. + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -597,6 +626,10 @@ Definition transl_op | Ocmp c, args => do r <- ireg_of res; transl_cond c args (mk_setcc (testcond_for_condition c) r k) + | Osel c ty, a1 :: a2 :: args => + assertion (mreg_eq a1 res); + do r <- ireg_of res; do r2 <- ireg_of a2; + transl_sel c args r r2 k | _, _ => Error(msg "Asmgen.transl_op") end. diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index 3aa87a4c..f1fd41e3 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -194,6 +194,14 @@ Proof. intros. destruct xc; simpl; TailNoLabel. Qed. +Remark mk_sel_label: + forall xc rd r2 k c, + mk_sel xc rd r2 k = OK c -> + tail_nolabel k c. +Proof. + unfold mk_sel; intros; destruct xc; inv H; TailNoLabel. +Qed. + Remark transl_cond_label: forall cond args k c, transl_cond cond args k = OK c -> @@ -221,6 +229,9 @@ Proof. destruct (Float32.eq_dec n Float32.zero); TailNoLabel. destruct (normalize_addrmode_64 x) as [am' [delta|]]; TailNoLabel. eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_setcc_label. + unfold transl_sel in EQ2. destruct (ireg_eq x x0); monadInv EQ2. + TailNoLabel. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_sel_label; eauto. Qed. Remark transl_load_label: @@ -706,7 +717,7 @@ Opaque loadind. intros. simpl in TR. destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR) as [rs' [A [B C]]]. - rewrite EC in B. + rewrite EC in B. destruct B as [B _]. destruct (testcond_for_condition cond); simpl in *. (* simple jcc *) exists (Pjcc c1 lbl); exists k; exists rs'. @@ -744,7 +755,7 @@ Opaque loadind. left; eapply exec_straight_steps; eauto. intros. simpl in TR. destruct (transl_cond_correct tge tf cond args _ _ rs0 m' TR) as [rs' [A [B C]]]. - rewrite EC in B. + rewrite EC in B. destruct B as [B _]. destruct (testcond_for_condition cond); simpl in *. (* simple jcc *) econstructor; split. diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index 904debdc..fd88954e 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -208,7 +208,8 @@ Proof. set (x' := Int.add x tnm1). set (rs2 := nextinstr (compare_ints (Vint x) (Vint Int.zero) rs1 m)). set (rs3 := nextinstr (rs2#RCX <- (Vint x'))). - set (rs4 := nextinstr (if Int.lt x Int.zero then rs3#RAX <- (Vint x') else rs3)). + set (v' := if Int.lt x Int.zero then Vint x' else Vint x). + set (rs4 := nextinstr (rs3#RAX <- v')). set (rs5 := nextinstr_nf (rs4#RAX <- (Val.shr rs4#RAX (Vint n)))). assert (rs3#RAX = Vint x). unfold rs3. Simplifs. assert (rs3#RCX = Vint x'). unfold rs3. Simplifs. @@ -218,13 +219,12 @@ Proof. change (rs2 RAX) with (rs1 RAX). rewrite A. simpl. rewrite Int.repr_unsigned. rewrite Int.add_zero_l. auto. auto. apply exec_straight_step with rs4 m. simpl. - rewrite Int.lt_sub_overflow. unfold rs4. destruct (Int.lt x Int.zero); simpl; auto. - unfold rs4. destruct (Int.lt x Int.zero); simpl; auto. + rewrite Int.lt_sub_overflow. unfold rs4, v'. rewrite H, H0. destruct (Int.lt x Int.zero); simpl; auto. + auto. apply exec_straight_one. auto. auto. split. unfold rs5. Simplifs. unfold rs4. rewrite nextinstr_inv; auto with asmgen. - destruct (Int.lt x Int.zero). rewrite Pregmap.gss. rewrite A; auto. rewrite A; rewrite H; auto. + rewrite Pregmap.gss. unfold v'. rewrite A. reflexivity. intros. unfold rs5. Simplifs. unfold rs4. Simplifs. - transitivity (rs3#r). destruct (Int.lt x Int.zero). Simplifs. auto. unfold rs3. Simplifs. unfold rs2. Simplifs. unfold compare_ints. Simplifs. Qed. @@ -913,6 +913,7 @@ Lemma transl_cond_correct: /\ match eval_condition cond (map rs (map preg_of args)) m with | None => True | Some b => eval_extcond (testcond_for_condition cond) rs' = Some b + /\ eval_extcond (testcond_for_condition (negate_condition cond)) rs' = Some (negb b) end /\ forall r, data_preg r = true -> rs'#r = rs r. Proof. @@ -921,58 +922,78 @@ Proof. - (* comp *) simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto. + split. destruct (Val.cmp_bool c0 (rs x) (rs x0)) eqn:?; auto. split. + eapply testcond_for_signed_comparison_32_correct; eauto. eapply testcond_for_signed_comparison_32_correct; eauto. + rewrite Val.negate_cmp_bool, Heqo; auto. intros. unfold compare_ints. Simplifs. - (* compu *) simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto. + split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto. split. eapply testcond_for_unsigned_comparison_32_correct; eauto. + eapply testcond_for_unsigned_comparison_32_correct; eauto. + rewrite Val.negate_cmpu_bool, Heqo; auto. intros. unfold compare_ints. Simplifs. - (* compimm *) simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int.eq_dec n Int.zero). econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. destruct (rs x); simpl; auto. subst. rewrite Int.and_idem. + split. destruct (rs x); simpl; auto. subst. rewrite Int.and_idem. split. + eapply testcond_for_signed_comparison_32_correct; eauto. eapply testcond_for_signed_comparison_32_correct; eauto. + rewrite Val.negate_cmp_bool; auto. intros. unfold compare_ints. Simplifs. econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. destruct (Val.cmp_bool c0 (rs x) (Vint n)) eqn:?; auto. + split. destruct (Val.cmp_bool c0 (rs x) (Vint n)) eqn:?; auto. split. eapply testcond_for_signed_comparison_32_correct; eauto. + eapply testcond_for_signed_comparison_32_correct; eauto. + rewrite Val.negate_cmp_bool, Heqo; auto. intros. unfold compare_ints. Simplifs. - (* compuimm *) simpl. rewrite (ireg_of_eq _ _ EQ). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint n)) eqn:?; auto. + split. destruct (Val.cmpu_bool (Mem.valid_pointer m) c0 (rs x) (Vint n)) eqn:?; auto; split. + eapply testcond_for_unsigned_comparison_32_correct; eauto. eapply testcond_for_unsigned_comparison_32_correct; eauto. + rewrite Val.negate_cmpu_bool, Heqo; auto. intros. unfold compare_ints. Simplifs. - (* compl *) simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct (Val.cmpl_bool c0 (rs x) (rs x0)) eqn:?; auto. + split. destruct (Val.cmpl_bool c0 (rs x) (rs x0)) eqn:?; auto. split. eapply testcond_for_signed_comparison_64_correct; eauto. + eapply testcond_for_signed_comparison_64_correct; eauto. + rewrite Val.negate_cmpl_bool, Heqo; auto. intros. unfold compare_longs. Simplifs. - (* complu *) simpl. rewrite (ireg_of_eq _ _ EQ). rewrite (ireg_of_eq _ _ EQ1). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto. + split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (rs x0)) eqn:?; auto. split. + eapply testcond_for_unsigned_comparison_64_correct; eauto. eapply testcond_for_unsigned_comparison_64_correct; eauto. + rewrite Val.negate_cmplu_bool, Heqo; auto. intros. unfold compare_longs. Simplifs. - (* compimm *) simpl. rewrite (ireg_of_eq _ _ EQ). destruct (Int64.eq_dec n Int64.zero). econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. destruct (rs x); simpl; auto. subst. rewrite Int64.and_idem. + split. destruct (rs x); simpl; auto. subst. rewrite Int64.and_idem. split. eapply testcond_for_signed_comparison_64_correct; eauto. + eapply testcond_for_signed_comparison_64_correct; eauto. + rewrite Val.negate_cmpl_bool; auto. intros. unfold compare_longs. Simplifs. econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. destruct (Val.cmpl_bool c0 (rs x) (Vlong n)) eqn:?; auto. + split. destruct (Val.cmpl_bool c0 (rs x) (Vlong n)) eqn:?; auto. split. + eapply testcond_for_signed_comparison_64_correct; eauto. eapply testcond_for_signed_comparison_64_correct; eauto. + rewrite Val.negate_cmpl_bool, Heqo; auto. intros. unfold compare_longs. Simplifs. - (* compuimm *) simpl. rewrite (ireg_of_eq _ _ EQ). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (Vlong n)) eqn:?; auto. + split. destruct (Val.cmplu_bool (Mem.valid_pointer m) c0 (rs x) (Vlong n)) eqn:?; auto. split. eapply testcond_for_unsigned_comparison_64_correct; eauto. + eapply testcond_for_unsigned_comparison_64_correct; eauto. + rewrite Val.negate_cmplu_bool, Heqo; auto. intros. unfold compare_longs. Simplifs. - (* compf *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). @@ -981,7 +1002,9 @@ Proof. destruct c0; simpl; auto. unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. split. destruct (rs x); destruct (rs x0); simpl; auto. - repeat rewrite swap_floats_commut. apply testcond_for_float_comparison_correct. + repeat rewrite swap_floats_commut. split. + apply testcond_for_float_comparison_correct. + apply testcond_for_neg_float_comparison_correct. intros. Simplifs. apply compare_floats_inv; auto with asmgen. - (* notcompf *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). @@ -990,7 +1013,9 @@ Proof. destruct c0; simpl; auto. unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats_inv; auto with asmgen. split. destruct (rs x); destruct (rs x0); simpl; auto. - repeat rewrite swap_floats_commut. apply testcond_for_neg_float_comparison_correct. + repeat rewrite swap_floats_commut. split. + apply testcond_for_neg_float_comparison_correct. + rewrite negb_involutive. apply testcond_for_float_comparison_correct. intros. Simplifs. apply compare_floats_inv; auto with asmgen. - (* compfs *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). @@ -999,7 +1024,9 @@ Proof. destruct c0; simpl; auto. unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. split. destruct (rs x); destruct (rs x0); simpl; auto. - repeat rewrite swap_floats_commut. apply testcond_for_float32_comparison_correct. + repeat rewrite swap_floats_commut. split. + apply testcond_for_float32_comparison_correct. + apply testcond_for_neg_float32_comparison_correct. intros. Simplifs. apply compare_floats32_inv; auto with asmgen. - (* notcompfs *) simpl. rewrite (freg_of_eq _ _ EQ). rewrite (freg_of_eq _ _ EQ1). @@ -1008,7 +1035,9 @@ Proof. destruct c0; simpl; auto. unfold nextinstr. rewrite Pregmap.gss. rewrite compare_floats32_inv; auto with asmgen. split. destruct (rs x); destruct (rs x0); simpl; auto. - repeat rewrite swap_floats_commut. apply testcond_for_neg_float32_comparison_correct. + repeat rewrite swap_floats_commut. split. + apply testcond_for_neg_float32_comparison_correct. + rewrite negb_involutive. apply testcond_for_float32_comparison_correct. intros. Simplifs. apply compare_floats32_inv; auto with asmgen. - (* maskzero *) simpl. rewrite (ireg_of_eq _ _ EQ). @@ -1133,6 +1162,94 @@ Proof. intuition Simplifs. Qed. +Definition negate_extcond (xc: extcond) : extcond := + match xc with + | Cond_base c => Cond_base (negate_testcond c) + | Cond_and c1 c2 => Cond_or (negate_testcond c1) (negate_testcond c2) + | Cond_or c1 c2 => Cond_and (negate_testcond c1) (negate_testcond c2) + end. + +Remark negate_testcond_for_condition: + forall cond, + negate_extcond (testcond_for_condition cond) = testcond_for_condition (negate_condition cond). +Proof. + intros. destruct cond; try destruct c; reflexivity. +Qed. + +Lemma mk_sel_correct: + forall xc ty rd r2 k c ob rs m, + mk_sel xc rd r2 k = OK c -> + rd <> r2 -> + match ob with + | Some b => eval_extcond xc rs = Some b /\ eval_extcond (negate_extcond xc) rs = Some (negb b) + | None => True + end -> + exists rs', + exec_straight ge fn c rs m k rs' m + /\ Val.lessdef (Val.select ob rs#rd rs#r2 ty) rs'#rd + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs r. +Proof. + intros. destruct xc; monadInv H; simpl in H1. +- econstructor; split. + eapply exec_straight_one. reflexivity. reflexivity. + set (v := match eval_testcond (negate_testcond c0) rs with + | Some true => rs r2 + | Some false => rs rd + | None => Vundef + end). + split. rewrite nextinstr_inv, Pregmap.gss by eauto with asmgen. + destruct ob; simpl; auto. destruct H1 as [_ B]; unfold v; rewrite B. + destruct b; apply Val.lessdef_normalize. + intros; Simplifs. +- econstructor; split. + eapply exec_straight_two. + reflexivity. reflexivity. reflexivity. reflexivity. + set (v1 := match eval_testcond (negate_testcond c1) rs with + | Some true => rs r2 + | Some false => rs rd + | None => Vundef + end). + rewrite eval_testcond_nextinstr, eval_testcond_set_ireg. + set (v2 := match eval_testcond (negate_testcond c2) rs with + | Some true => nextinstr rs # rd <- v1 r2 + | Some false => nextinstr rs # rd <- v1 rd + | None => Vundef + end). + split. rewrite nextinstr_inv, Pregmap.gss by eauto with asmgen. + destruct ob; simpl; auto. + destruct H1 as [_ B]. + destruct (eval_testcond (negate_testcond c1) rs) as [b1|]; try discriminate. + destruct (eval_testcond (negate_testcond c2) rs) as [b2|]; try discriminate. + inv B. apply negb_sym in H1. subst b. + replace v2 with (if b2 then rs#r2 else v1). + unfold v1. destruct b1, b2; apply Val.lessdef_normalize. + unfold v2. destruct b2; symmetry; Simplifs. + intros; Simplifs. +Qed. + +Lemma transl_sel_correct: + forall ty cond args rd r2 k c rs m, + transl_sel cond args rd r2 k = OK c -> + 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#rd rs#r2 ty) rs'#rd + /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs r. +Proof. + unfold transl_sel; intros. destruct (ireg_eq rd r2); monadInv H. +- econstructor; split. + apply exec_straight_one; reflexivity. + split. rewrite nextinstr_inv, Pregmap.gss by auto with asmgen. + destruct eval_condition as [[]|]; simpl; auto using Val.lessdef_normalize. + intros; Simplifs. +- destruct (transl_cond_correct _ _ _ _ rs m EQ0) as (rs1 & A & B & C). + rewrite <- negate_testcond_for_condition in B. + destruct (mk_sel_correct _ ty _ _ _ _ _ rs1 m EQ n B) as (rs2 & D & E & F). + exists rs2; split. + eapply exec_straight_trans; eauto. + split. rewrite ! C in E by auto with asmgen. exact E. + intros. rewrite F; auto. +Qed. + (** Translation of arithmetic operations. *) Ltac ArgsInv := @@ -1142,7 +1259,9 @@ Ltac ArgsInv := | [ H: bind _ _ = OK _ |- _ ] => monadInv H; ArgsInv | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv - | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *; clear H; ArgsInv + | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in *; + let X := fresh "EQ" in generalize (ireg_of_eq _ _ H); intros X; + clear H; ArgsInv | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in *; clear H; ArgsInv | _ => idtac end. @@ -1334,9 +1453,12 @@ Transparent destroyed_by_op. exists rs3. split. eapply exec_straight_trans. eexact P. eexact S. split. rewrite T. destruct (eval_condition cond rs ## (preg_of ## args) m). - rewrite Q. auto. + destruct Q as [Q _]. rewrite Q. auto. simpl; auto. intros. transitivity (rs2 r); auto. +(* selection *) + rewrite EQ1. exploit transl_sel_correct; eauto. intros (rs' & A & B & C). + exists rs'; split. eexact A. eauto. Qed. (** Translation of memory loads. *) diff --git a/x86/Machregs.v b/x86/Machregs.v index bdf492ed..6f3064b8 100644 --- a/x86/Machregs.v +++ b/x86/Machregs.v @@ -351,6 +351,7 @@ Definition two_address_op (op: operation) : bool := | Olongofsingle => false | Osingleoflong => false | Ocmp c => false + | Osel c op => true end. (* Constraints on constant propagation for builtins *) diff --git a/x86/NeedOp.v b/x86/NeedOp.v index 68ecc745..d9a58fbb 100644 --- a/x86/NeedOp.v +++ b/x86/NeedOp.v @@ -120,6 +120,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointoffloat | Ofloatofint | Ointofsingle | Osingleofint => op1 (default nv) | Olongoffloat | Ofloatoflong | Olongofsingle | Osingleoflong => 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 := @@ -231,6 +232,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/x86/Op.v b/x86/Op.v index 79c84ca2..16d75426 100644 --- a/x86/Op.v +++ b/x86/Op.v @@ -167,7 +167,9 @@ Inductive operation : Type := | Olongofsingle (**r [rd = signed_long_of_float32(r1)] *) | Osingleoflong (**r [rd = float32_of_signed_long(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. *) + | Osel: condition -> typ -> operation. + (**r [rd = rs1] if condition holds, [rd = rs2] otherwise. *) (** Comparison functions (used in modules [CSE] and [Allocation]). *) @@ -186,7 +188,7 @@ Defined. Definition beq_operation: forall (x y: operation), bool. Proof. - generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_addressing eq_condition; boolean_equality. + generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec ident_eq typ_eq eq_addressing eq_condition; boolean_equality. Defined. Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}. @@ -407,6 +409,7 @@ Definition eval_operation | Olongofsingle, v1::nil => Val.longofsingle v1 | Osingleoflong, v1::nil => Val.singleoflong 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. @@ -578,6 +581,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Olongofsingle => (Tsingle :: nil, Tlong) | Osingleoflong => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) + | Osel c ty => (ty :: ty :: type_of_condition c, ty) end. (** Weak type soundness results for [eval_operation]: @@ -735,6 +739,7 @@ Proof with (try exact I; try reflexivity). destruct v0; simpl in H0; inv H0. destruct (Float32.to_long f); inv H2... destruct v0; simpl in H0; inv H0... destruct (eval_condition cond vl m); simpl... destruct b... + unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I. Qed. End SOUNDNESS. @@ -958,23 +963,42 @@ 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 _ => negb Archi.ptr64 + | Ccompuimm _ _ => negb Archi.ptr64 + | Ccomplu _ => Archi.ptr64 + | Ccompluimm _ _ => Archi.ptr64 + | _ => false + end. + Definition op_depends_on_memory (op: operation) : bool := match op with - | Ocmp (Ccompu _) => negb Archi.ptr64 - | Ocmp (Ccompuimm _ _) => negb Archi.ptr64 - | Ocmp (Ccomplu _) => Archi.ptr64 - | Ocmp (Ccompluimm _ _) => Archi.ptr64 + | 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 until m2. + destruct c; simpl; intros SF; auto; rewrite ? negb_false_iff in SF; + unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. +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. - destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF; - unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. + 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 *) @@ -1290,6 +1314,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. End EVAL_COMPAT. diff --git a/x86/PrintOp.ml b/x86/PrintOp.ml index faa5bb5f..6aa4d450 100644 --- a/x86/PrintOp.ml +++ b/x86/PrintOp.ml @@ -164,6 +164,10 @@ let print_operation reg pp = function | Olongofsingle, [r1] -> fprintf pp "longofsingle(%a)" reg r1 | Osingleoflong, [r1] -> fprintf pp "singleoflong(%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 "" diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index a1583600..cf0f37ec 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -456,7 +456,35 @@ Nondetfunction cast16signed (e: expr) := Eop Ocast16signed (e ::: Enil) end. -(** Floating-point conversions *) +(** ** Selection *) + +Definition select_supported (ty: typ) : bool := + match ty with + | Tint => true + | Tlong => Archi.ptr64 + | _ => false + end. + +(** [Asmgen.mk_sel] cannot always handle the conditions that are + implemented as a "and" of two processor flags. However it can + handle the negation of those conditions, which are implemented + as an "or". So, for the risky conditions we just take their + negation and swap the two arguments of the [select]. *) + +Definition select_swap (cond: condition) := + match cond with + | Ccompf Cne | Ccompfs Cne | Cnotcompf Ceq | Cnotcompfs Ceq => true + | _ => false + end. + +Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) := + if select_supported ty then + if select_swap cond + then Some (Eop (Osel (negate_condition cond) ty) (e2 ::: e1 ::: args)) + else Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)) + else None. + +(** ** Floating-point conversions *) Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil). Definition floatofsingle (e: expr) := Eop Ofloatofsingle (e ::: Enil). diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index fdbadaa8..b412ccf7 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -769,6 +769,32 @@ Proof. 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. + destruct (select_supported ty); try discriminate. + destruct (select_swap cond); inv H. +- exists (Val.select (Some (negb b)) v2 v1 ty); split. + apply eval_Eop with (v2 :: v1 :: vl). + constructor; auto. constructor; auto. + simpl. rewrite eval_negate_condition, H3; auto. + destruct b; auto. +- exists (Val.select (Some b) v1 v2 ty); split. + apply eval_Eop with (v1 :: v2 :: vl). + constructor; auto. constructor; auto. + simpl. rewrite H3; auto. + auto. +Qed. + Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. Proof. red; intros. unfold singleoffloat. TrivialExists. diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v index 1021a9c8..d0b8427a 100644 --- a/x86/ValueAOp.v +++ b/x86/ValueAOp.v @@ -160,6 +160,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Olongofsingle, v1::nil => longofsingle v1 | Osingleoflong, v1::nil => singleoflong 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. @@ -258,6 +259,7 @@ Proof. eapply eval_static_addressing_32_sound; eauto. eapply eval_static_addressing_64_sound; eauto. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. + apply select_sound; auto. eapply eval_static_condition_sound; eauto. Qed. End SOUNDNESS. -- cgit