From 7698300cfe2d3f944ce2e1d4a60a263620487718 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 20 Dec 2013 13:05:53 +0000 Subject: Merge of branch value-analysis. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/ConstpropOpproof.v | 422 ++++++++++++++++++++------------------------- 1 file changed, 190 insertions(+), 232 deletions(-) (limited to 'powerpc/ConstpropOpproof.v') diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 2aba9c2c..e7dd3a41 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Correctness proof for constant propagation (processor-dependent part). *) +(** Correctness proof for operator strength reduction. *) Require Import Coqlib. Require Import AST. @@ -23,168 +23,8 @@ Require Import Events. Require Import Op. Require Import Registers. Require Import RTL. +Require Import ValueDomain. Require Import ConstpropOp. -Require Import Constprop. - -(** * Correctness of the static analysis *) - -Section ANALYSIS. - -Variable ge: genv. -Variable sp: val. - -(** We first show that the dataflow analysis is correct with respect - to the dynamic semantics: the approximations (sets of values) - of a register at a program point predicted by the static analysis - are a superset of the values actually encountered during concrete - executions. We formalize this correspondence between run-time values and - compile-time approximations by the following predicate. *) - -Definition val_match_approx (a: approx) (v: val) : Prop := - match a with - | Unknown => True - | I p => v = Vint p - | F p => v = Vfloat p - | L p => v = Vlong p - | G symb ofs => v = symbol_address ge symb ofs - | S ofs => v = Val.add sp (Vint ofs) - | _ => False - end. - -Inductive val_list_match_approx: list approx -> list val -> Prop := - | vlma_nil: - val_list_match_approx nil nil - | vlma_cons: - forall a al v vl, - val_match_approx a v -> - val_list_match_approx al vl -> - val_list_match_approx (a :: al) (v :: vl). - -Ltac SimplVMA := - match goal with - | H: (val_match_approx (I _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | H: (val_match_approx (F _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | H: (val_match_approx (L _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | H: (val_match_approx (G _ _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | H: (val_match_approx (S _) ?v) |- _ => - simpl in H; (try subst v); SimplVMA - | _ => - idtac - end. - -Ltac InvVLMA := - match goal with - | H: (val_list_match_approx nil ?vl) |- _ => - inv H - | H: (val_list_match_approx (?a :: ?al) ?vl) |- _ => - inv H; SimplVMA; InvVLMA - | _ => - idtac - end. - -(** We then show that [eval_static_operation] is a correct abstract - interpretations of [eval_operation]: if the concrete arguments match - the given approximations, the concrete results match the - approximations returned by [eval_static_operation]. *) - -Lemma eval_static_condition_correct: - forall cond al vl m b, - val_list_match_approx al vl -> - eval_static_condition cond al = Some b -> - eval_condition cond vl m = Some b. -Proof. - intros until b. - unfold eval_static_condition. - case (eval_static_condition_match cond al); intros; - InvVLMA; simpl; congruence. -Qed. - -Remark shift_symbol_address: - forall symb ofs n, - symbol_address ge symb (Int.add ofs n) = Val.add (symbol_address ge symb ofs) (Vint n). -Proof. - unfold symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. -Qed. - -Lemma eval_static_operation_correct: - forall op al vl m v, - val_list_match_approx al vl -> - eval_operation ge sp op vl m = Some v -> - val_match_approx (eval_static_operation op al) v. -Proof. - intros until v. - unfold eval_static_operation. - case (eval_static_operation_match op al); intros; - InvVLMA; simpl in *; FuncInv; try subst v; auto. - - destruct (propagate_float_constants tt); simpl; auto. - - rewrite shift_symbol_address; auto. - - rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. auto. - - rewrite Int.add_commut; auto. - - rewrite Val.add_assoc. rewrite Int.add_commut. auto. - - change (Val.add (Vint n1) (Val.add sp (Vint n2)) = Val.add sp (Vint (Int.add n1 n2))). - rewrite Val.add_permut. auto. - - rewrite shift_symbol_address; auto. - - rewrite Val.add_assoc; auto. - - rewrite shift_symbol_address; auto. - - unfold symbol_address. destruct (Genv.find_symbol ge s1); auto. - - rewrite Val.sub_add_opp. rewrite Val.add_assoc. simpl. rewrite Int.sub_add_opp. auto. - - destruct (Int.eq n2 Int.zero). inv H0. - destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto. - destruct (Int.eq n2 Int.zero); inv H0; simpl; auto. - - destruct (Int.ltu n2 Int.iwordsize); simpl; auto. - destruct (Int.ltu n2 Int.iwordsize); simpl; auto. - destruct (Int.ltu n Int.iwordsize); simpl; auto. - destruct (Int.ltu n (Int.repr 31)); inv H0. simpl; auto. - destruct (Int.ltu n2 Int.iwordsize); simpl; auto. - - unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0. - simpl; auto. - - destruct (propagate_float_constants tt); simpl; auto. - - unfold eval_static_condition_val, Val.of_optbool. - destruct (eval_static_condition c vl0) eqn:?. - rewrite (eval_static_condition_correct _ _ _ m _ H Heqo). - destruct b; simpl; auto. - simpl; auto. -Qed. - -Lemma eval_static_addressing_correct: - forall addr al vl v, - val_list_match_approx al vl -> - eval_addressing ge sp addr vl = Some v -> - val_match_approx (eval_static_addressing addr al) v. -Proof. - intros until v. unfold eval_static_addressing. - case (eval_static_addressing_match addr al); intros; - InvVLMA; simpl in *; FuncInv; try subst v; auto. - rewrite shift_symbol_address; auto. - rewrite Val.add_assoc. auto. - repeat rewrite shift_symbol_address. auto. - fold (Val.add (Vint n1) (symbol_address ge id ofs)). - repeat rewrite shift_symbol_address. apply Val.add_commut. - repeat rewrite Val.add_assoc. auto. - fold (Val.add (Vint n1) (Val.add sp (Vint ofs))). - rewrite Val.add_permut. decEq. rewrite Val.add_commut. auto. - rewrite shift_symbol_address. auto. -Qed. (** * Correctness of strength reduction *) @@ -196,51 +36,91 @@ Qed. Section STRENGTH_REDUCTION. -Variable app: D.t. +Variable bc: block_classification. +Variable ge: genv. +Hypothesis GENV: genv_match bc ge. +Variable sp: block. +Hypothesis STACK: bc sp = BCstack. +Variable ae: AE.t. Variable rs: regset. Variable m: mem. -Hypothesis MATCH: forall r, val_match_approx (approx_reg app r) rs#r. +Hypothesis MATCH: ematch bc rs ae. + +Lemma match_G: + forall r id ofs, + AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef rs#r (symbol_address ge id ofs). +Proof. + intros. apply vmatch_ptr_gl with bc; auto. rewrite <- H. apply MATCH. +Qed. + +Lemma match_S: + forall r ofs, + AE.get r ae = Ptr(Stk ofs) -> Val.lessdef rs#r (Vptr sp ofs). +Proof. + intros. apply vmatch_ptr_stk with bc; auto. rewrite <- H. apply MATCH. +Qed. Ltac InvApproxRegs := match goal with | [ H: _ :: _ = _ :: _ |- _ ] => injection H; clear H; intros; InvApproxRegs - | [ H: ?v = approx_reg app ?r |- _ ] => + | [ H: ?v = AE.get ?r ae |- _ ] => generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs | _ => idtac end. +Ltac SimplVM := + match goal with + | [ H: vmatch _ ?v (I ?n) |- _ ] => + let E := fresh in + assert (E: v = Vint n) by (inversion H; auto); + rewrite E in *; clear H; SimplVM + | [ H: vmatch _ ?v (F ?n) |- _ ] => + let E := fresh in + assert (E: v = Vfloat n) by (inversion H; auto); + rewrite E in *; clear H; SimplVM + | [ H: vmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] => + let E := fresh in + assert (E: Val.lessdef v (Op.symbol_address ge id ofs)) by (eapply vmatch_ptr_gl; eauto); + clear H; SimplVM + | [ H: vmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] => + let E := fresh in + assert (E: Val.lessdef v (Vptr sp ofs)) by (eapply vmatch_ptr_stk; eauto); + clear H; SimplVM + | _ => idtac + end. + Lemma cond_strength_reduction_correct: forall cond args vl, - vl = approx_regs app args -> + vl = map (fun r => AE.get r ae) args -> let (cond', args') := cond_strength_reduction cond args vl in eval_condition cond' rs##args' m = eval_condition cond rs##args m. Proof. intros until vl. unfold cond_strength_reduction. - case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVMA. - rewrite H0. apply Val.swap_cmp_bool. - rewrite H. auto. - rewrite H0. apply Val.swap_cmpu_bool. - rewrite H. auto. - auto. + case (cond_strength_reduction_match cond args vl); simpl; intros; InvApproxRegs; SimplVM. +- apply Val.swap_cmp_bool. +- auto. +- apply Val.swap_cmpu_bool. +- auto. +- auto. Qed. Lemma make_addimm_correct: forall n r, let (op, args) := make_addimm n r in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v. Proof. intros. unfold make_addimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto. exists (Val.add rs#r (Vint n)); auto. Qed. - + Lemma make_shlimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shlimm n r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v. Proof. intros; unfold make_shlimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -254,7 +134,7 @@ Lemma make_shrimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shrimm n r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v. Proof. intros; unfold make_shrimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -268,7 +148,7 @@ Lemma make_shruimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shruimm n r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. Proof. intros; unfold make_shruimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -282,7 +162,7 @@ Lemma make_mulimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_mulimm n r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v. Proof. intros; unfold make_mulimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -301,7 +181,7 @@ Lemma make_divimm_correct: Val.divs rs#r1 rs#r2 = Some v -> rs#r2 = Vint n -> let (op, args) := make_divimm n r1 r2 in - exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. destruct (Int.is_power2 n) eqn:?. @@ -316,7 +196,7 @@ Lemma make_divuimm_correct: Val.divu rs#r1 rs#r2 = Some v -> rs#r2 = Vint n -> let (op, args) := make_divuimm n r1 r2 in - exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. destruct (Int.is_power2 n) eqn:?. @@ -330,22 +210,35 @@ Proof. Qed. Lemma make_andimm_correct: - forall n r, - let (op, args) := make_andimm n r in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v. + forall n r x, + vmatch bc rs#r x -> + let (op, args) := make_andimm n r x in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v. Proof. intros; unfold make_andimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto. + destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero + | _ => false end) eqn:UNS. + destruct x; try congruence. + exists (rs#r); split; auto. + inv H; auto. simpl. replace (Int.and i n) with i; auto. + generalize (Int.eq_spec (Int.zero_ext n0 (Int.not n)) Int.zero); rewrite UNS; intro EQ. + Int.bit_solve. destruct (zlt i0 n0). + replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). + rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. + rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. + rewrite Int.bits_not by auto. apply negb_involutive. + rewrite H5 by auto. auto. econstructor; split; eauto. auto. Qed. Lemma make_orimm_correct: forall n r, let (op, args) := make_orimm n r in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v. Proof. intros; unfold make_orimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -358,7 +251,7 @@ Qed. Lemma make_xorimm_correct: forall n r, let (op, args) := make_xorimm n r in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v. Proof. intros; unfold make_xorimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -370,7 +263,7 @@ Lemma make_mulfimm_correct: forall n r1 r2, rs#r2 = Vfloat n -> let (op, args) := make_mulfimm n r1 r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. @@ -383,7 +276,7 @@ Lemma make_mulfimm_correct_2: forall n r1 r2, rs#r1 = Vfloat n -> let (op, args) := make_mulfimm n r2 r1 r2 in - exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros. @@ -393,81 +286,146 @@ Proof. simpl. econstructor; split; eauto. Qed. +Lemma make_cast8signed_correct: + forall r x, + vmatch bc rs#r x -> + let (op, args) := make_cast8signed r x in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. +Proof. + intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. + exists rs#r; split; auto. + assert (V: vmatch bc rs#r (Sgn 8)). + { eapply vmatch_ge; eauto. apply vincl_ge; auto. } + inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + econstructor; split; simpl; eauto. +Qed. + +Lemma make_cast16signed_correct: + forall r x, + vmatch bc rs#r x -> + let (op, args) := make_cast16signed r x in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. +Proof. + intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. + exists rs#r; split; auto. + assert (V: vmatch bc rs#r (Sgn 16)). + { eapply vmatch_ge; eauto. apply vincl_ge; auto. } + inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + econstructor; split; simpl; eauto. +Qed. + +Lemma make_singleoffloat_correct: + forall r x, + vmatch bc rs#r x -> + let (op, args) := make_singleoffloat r x in + exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.singleoffloat rs#r) v. +Proof. + intros; unfold make_singleoffloat. + destruct (vincl x Fsingle && generate_float_constants tt) eqn:INCL. + InvBooleans. exists rs#r; split; auto. + assert (V: vmatch bc rs#r Fsingle). + { eapply vmatch_ge; eauto. apply vincl_ge; auto. } + inv V; simpl; auto. rewrite Float.singleoffloat_of_single by auto. auto. + econstructor; split; simpl; eauto. +Qed. + Lemma op_strength_reduction_correct: forall op args vl v, - vl = approx_regs app args -> - eval_operation ge sp op rs##args m = Some v -> + vl = map (fun r => AE.get r ae) args -> + eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v -> let (op', args') := op_strength_reduction op args vl in - exists w, eval_operation ge sp op' rs##args' m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some w /\ Val.lessdef v w. Proof. intros until v; unfold op_strength_reduction; case (op_strength_reduction_match op args vl); simpl; intros. +(* cast8signed *) + InvApproxRegs; SimplVM; inv H0. apply make_cast8signed_correct; auto. +(* cast8signed *) + InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto. (* add *) - InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.add_commut. apply make_addimm_correct. - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_addimm_correct. + InvApproxRegs; SimplVM; inv H0. fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. apply make_addimm_correct. + InvApproxRegs; SimplVM; inv H0. apply make_addimm_correct. + InvApproxRegs; SimplVM; inv H0. econstructor; split; eauto. apply Val.add_lessdef; auto. + InvApproxRegs; SimplVM; inv H0. econstructor; split; eauto. rewrite Val.add_commut. apply Val.add_lessdef; auto. (* sub *) - InvApproxRegs; SimplVMA. inv H0. rewrite H1. econstructor; split; eauto. - InvApproxRegs; SimplVMA. inv H0. rewrite H. rewrite Val.sub_add_opp. apply make_addimm_correct. + InvApproxRegs; SimplVM; inv H0. fold (Val.sub (Vint n1) rs#r2). econstructor; split; eauto. + InvApproxRegs; SimplVM; inv H0. rewrite Val.sub_add_opp. apply make_addimm_correct. (* mul *) - InvApproxRegs; SimplVMA. inv H0. rewrite H1. rewrite Val.mul_commut. apply make_mulimm_correct; auto. - InvApproxRegs; SimplVMA. inv H0. rewrite H. apply make_mulimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. fold (Val.mul (Vint n1) rs#r2). rewrite Val.mul_commut. apply make_mulimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_mulimm_correct; auto. (* divs *) - assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto. + assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divimm_correct; auto. (* divu *) - assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVMA; auto. + assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divuimm_correct; auto. (* and *) - InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.and_commut. apply make_andimm_correct. - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_andimm_correct. + InvApproxRegs; SimplVM; inv H0. fold (Val.and (Vint n1) rs#r2). rewrite Val.and_commut. apply make_andimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_andimm_correct. auto. + inv H; inv H0. apply make_andimm_correct. auto. (* or *) - InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.or_commut. apply make_orimm_correct. - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_orimm_correct. + InvApproxRegs; SimplVM; inv H0. fold (Val.or (Vint n1) rs#r2). rewrite Val.or_commut. apply make_orimm_correct. + InvApproxRegs; SimplVM; inv H0. apply make_orimm_correct. (* xor *) - InvApproxRegs. SimplVMA. inv H0. rewrite H1. rewrite Val.xor_commut. apply make_xorimm_correct. - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_xorimm_correct. + InvApproxRegs; SimplVM; inv H0. fold (Val.xor (Vint n1) rs#r2). rewrite Val.xor_commut. apply make_xorimm_correct. + InvApproxRegs; SimplVM; inv H0. apply make_xorimm_correct. (* shl *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shlimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_shlimm_correct; auto. (* shr *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shrimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_shrimm_correct; auto. (* shru *) - InvApproxRegs. SimplVMA. inv H0. rewrite H. apply make_shruimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto. +(* singleoffloat *) + InvApproxRegs; SimplVM; inv H0. apply make_singleoffloat_correct; auto. (* cmp *) generalize (cond_strength_reduction_correct c args0 vl0). destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros. rewrite <- H1 in H0; auto. econstructor; split; eauto. (* mulf *) - inv H0. assert (rs#r2 = Vfloat n2). InvApproxRegs; SimplVMA; auto. - apply make_mulfimm_correct; auto. - inv H0. assert (rs#r1 = Vfloat n1). InvApproxRegs; SimplVMA; auto. - apply make_mulfimm_correct_2; auto. + InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto. + InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2). + rewrite <- H2. apply make_mulfimm_correct_2; auto. (* default *) exists v; auto. Qed. - + +Remark shift_symbol_address: + forall symb ofs n, + Op.symbol_address ge symb (Int.add ofs n) = Val.add (Op.symbol_address ge symb ofs) (Vint n). +Proof. + unfold Op.symbol_address; intros. destruct (Genv.find_symbol ge symb); auto. +Qed. + Lemma addr_strength_reduction_correct: - forall addr args vl, - vl = approx_regs app args -> + forall addr args vl res, + vl = map (fun r => AE.get r ae) args -> + eval_addressing ge (Vptr sp Int.zero) addr rs##args = Some res -> let (addr', args') := addr_strength_reduction addr args vl in - eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args. + exists res', eval_addressing ge (Vptr sp Int.zero) addr' rs##args' = Some res' /\ Val.lessdef res res'. Proof. - intros until vl. unfold addr_strength_reduction. - destruct (addr_strength_reduction_match addr args vl); simpl; intros; InvApproxRegs; SimplVMA. - rewrite H; rewrite H0. rewrite shift_symbol_address. auto. - rewrite H; rewrite H0. rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut; auto. - rewrite H; rewrite H0. rewrite Val.add_assoc; auto. - rewrite H; rewrite H0. rewrite Val.add_permut; auto. - rewrite H0. auto. - rewrite H. rewrite Val.add_commut. auto. - rewrite H0. rewrite Val.add_commut; auto. - rewrite H; auto. - rewrite H. rewrite shift_symbol_address. auto. - rewrite H. rewrite shift_symbol_address. auto. - rewrite H. rewrite Val.add_assoc. auto. - auto. + intros until res. unfold addr_strength_reduction. + destruct (addr_strength_reduction_match addr args vl); simpl; + intros VL EA; InvApproxRegs; SimplVM; try (inv EA). +- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. +- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. + econstructor; split; eauto. apply Val.add_lessdef; auto. +- rewrite Int.add_zero_l. + change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)). + econstructor; split; eauto. apply Val.add_lessdef; auto. +- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_zero_l. rewrite Int.add_commut. + change (Vptr sp (Int.add n2 n1)) with (Val.add (Vptr sp n2) (Vint n1)). + rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. +- econstructor; split; eauto. apply Val.add_lessdef; auto. +- rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. +- fold (Val.add (Vint n1) rs#r2). + rewrite Val.add_commut. econstructor; split; eauto. +- econstructor; split; eauto. +- rewrite shift_symbol_address. econstructor; split; eauto. +- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. +- rewrite Int.add_zero_l. + change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)). + econstructor; split; eauto. apply Val.add_lessdef; auto. +- exists res; auto. Qed. End STRENGTH_REDUCTION. - -End ANALYSIS. - -- cgit