From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/CSEproof.v | 276 ++++++++++++++++++++++++++--------------------------- 1 file changed, 138 insertions(+), 138 deletions(-) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 70f9bfc7..07c7008d 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -100,9 +100,9 @@ Lemma numbering_holds_exten: Proof. intros. destruct H. constructor; intros. - auto. -- apply equation_holds_exten. auto. - eapply wf_equation_incr; eauto with cse. -- rewrite AGREE. eauto. eapply Plt_le_trans; eauto. eapply wf_num_reg; eauto. +- apply equation_holds_exten. auto. + eapply wf_equation_incr; eauto with cse. +- rewrite AGREE. eauto. eapply Plt_le_trans; eauto. eapply wf_num_reg; eauto. Qed. End EXTEN. @@ -136,16 +136,16 @@ Proof. + constructor; simpl; intros. * constructor; simpl; intros. apply wf_equation_incr with (num_next n). eauto with cse. xomega. - rewrite PTree.gsspec in H0. destruct (peq r0 r). + rewrite PTree.gsspec in H0. destruct (peq r0 r). inv H0; xomega. apply Plt_trans_succ; eauto with cse. rewrite PMap.gsspec in H0. destruct (peq v (num_next n)). replace r0 with r by (simpl in H0; intuition). rewrite PTree.gss. subst; auto. - exploit wf_num_val; eauto with cse. intro. + exploit wf_num_val; eauto with cse. intro. rewrite PTree.gso by congruence. auto. * eapply equation_holds_exten; eauto with cse. * unfold valu2. rewrite PTree.gsspec in H0. destruct (peq r0 r). - inv H0. rewrite peq_true; auto. + inv H0. rewrite peq_true; auto. rewrite peq_false. eauto with cse. apply Plt_ne; eauto with cse. + unfold valu2. rewrite peq_true; auto. + auto. @@ -169,9 +169,9 @@ Proof. - destruct (valnum_reg n a) as [n1 v1] eqn:V1. destruct (valnum_regs n1 rl) as [n2 vs] eqn:V2. inv H0. - exploit valnum_reg_holds; eauto. + exploit valnum_reg_holds; eauto. intros (valu2 & A & B & C & D & E). - exploit (IHrl valu2); eauto. + exploit (IHrl valu2); eauto. intros (valu3 & P & Q & R & S & T). exists valu3; splitall. + auto. @@ -187,7 +187,7 @@ Lemma find_valnum_rhs_charact: Proof. induction eqs; simpl; intros. - inv H. -- destruct a. destruct (strict && eq_rhs rh r) eqn:T. +- destruct a. destruct (strict && eq_rhs rh r) eqn:T. + InvBooleans. inv H. left; auto. + right; eauto. Qed. @@ -198,9 +198,9 @@ Lemma find_valnum_rhs'_charact: Proof. induction eqs; simpl; intros. - inv H. -- destruct a. destruct (eq_rhs rh r) eqn:T. +- destruct a. destruct (eq_rhs rh r) eqn:T. + inv H. exists strict; auto. - + exploit IHeqs; eauto. intros [s IN]. exists s; auto. + + exploit IHeqs; eauto. intros [s IN]. exists s; auto. Qed. Lemma find_valnum_num_charact: @@ -208,8 +208,8 @@ Lemma find_valnum_num_charact: Proof. induction eqs; simpl; intros. - inv H. -- destruct a. destruct (strict && peq v v0) eqn:T. - + InvBooleans. inv H. auto. +- destruct a. destruct (strict && peq v v0) eqn:T. + + InvBooleans. inv H. auto. + eauto. Qed. @@ -220,7 +220,7 @@ Lemma reg_valnum_sound: rs#r = valu v. Proof. unfold reg_valnum; intros. destruct (num_val n)#v as [ | r1 rl] eqn:E; inv H. - eapply num_holds_reg; eauto. eapply wf_num_val; eauto with cse. + eapply num_holds_reg; eauto. eapply wf_num_val; eauto with cse. rewrite E; auto with coqlib. Qed. @@ -235,7 +235,7 @@ Proof. - inv H0; auto. - destruct (reg_valnum n a) as [r1|] eqn:RV1; try discriminate. destruct (regs_valnums n vl) as [rl1|] eqn:RVL; inv H0. - simpl; f_equal. eapply reg_valnum_sound; eauto. eauto. + simpl; f_equal. eapply reg_valnum_sound; eauto. eauto. Qed. Lemma find_rhs_sound: @@ -256,10 +256,10 @@ Remark in_remove: forall (A: Type) (eq: forall (x y: A), {x=y}+{x<>y}) x y l, In y (List.remove eq x l) <-> x <> y /\ In y l. Proof. - induction l; simpl. + induction l; simpl. tauto. - destruct (eq x a). - subst a. rewrite IHl. tauto. + destruct (eq x a). + subst a. rewrite IHl. tauto. simpl. rewrite IHl. intuition congruence. Qed. @@ -274,7 +274,7 @@ Proof. + subst v. rewrite in_remove in H0. intuition. + split; auto. exploit wf_num_val; eauto. congruence. - split; auto. exploit wf_num_val; eauto. congruence. -Qed. +Qed. Lemma update_reg_charact: forall n rd vd r v, @@ -285,7 +285,7 @@ Proof. unfold update_reg; intros. rewrite PMap.gsspec in H0. destruct (peq v vd). -- subst v. destruct H0. +- subst v. destruct H0. + subst r. apply PTree.gss. + exploit forget_reg_charact; eauto. intros [A B]. rewrite PTree.gso by auto. eapply wf_num_val; eauto. @@ -324,7 +324,7 @@ Proof. eauto with cse. * eapply update_reg_charact; eauto with cse. + eauto with cse. -+ rewrite PTree.gsspec in H5. destruct (peq r rd). ++ rewrite PTree.gsspec in H5. destruct (peq r rd). congruence. rewrite H2 by auto. eauto with cse. @@ -334,17 +334,17 @@ Proof. { red; intros. unfold valu2. apply peq_false. apply Plt_ne; auto. } exists valu2; constructor; simpl; intros. + constructor; simpl; intros. - * destruct H3. inv H3. simpl; split. xomega. - red; intros. apply Plt_trans_succ; eauto. - apply wf_equation_incr with (num_next n). eauto with cse. xomega. + * destruct H3. inv H3. simpl; split. xomega. + red; intros. apply Plt_trans_succ; eauto. + apply wf_equation_incr with (num_next n). eauto with cse. xomega. * rewrite PTree.gsspec in H3. destruct (peq r rd). inv H3. xomega. apply Plt_trans_succ; eauto with cse. * apply update_reg_charact; eauto with cse. + destruct H3. inv H3. - constructor. unfold valu2 at 2; rewrite peq_true. - eapply rhs_eval_to_exten; eauto. - eapply equation_holds_exten; eauto with cse. + constructor. unfold valu2 at 2; rewrite peq_true. + eapply rhs_eval_to_exten; eauto. + eapply equation_holds_exten; eauto with cse. + rewrite PTree.gsspec in H3. unfold valu2. destruct (peq r rd). inv H3. rewrite peq_true; auto. rewrite peq_false. rewrite H2 by auto. eauto with cse. @@ -363,7 +363,7 @@ Proof. exploit is_move_operation_correct; eauto. intros [A B]; subst op args. simpl in H0. inv H0. destruct (valnum_reg n src) as [n1 vsrc] eqn:VN. - exploit valnum_reg_holds; eauto. + exploit valnum_reg_holds; eauto. intros (valu2 & A & B & C & D & E). exists valu2; constructor; simpl; intros. + constructor; simpl; intros; eauto with cse. @@ -372,15 +372,15 @@ Proof. eauto with cse. * eapply update_reg_charact; eauto with cse. + eauto with cse. -+ rewrite PTree.gsspec in H0. rewrite Regmap.gsspec. ++ rewrite PTree.gsspec in H0. rewrite Regmap.gsspec. destruct (peq r dst). congruence. eauto with cse. - (* general case *) destruct (valnum_regs n args) as [n1 vl] eqn:VN. - exploit valnum_regs_holds; eauto. + exploit valnum_regs_holds; eauto. intros (valu2 & A & B & C & D & E). - eapply add_rhs_holds; eauto. -+ constructor. rewrite Regmap.gss. congruence. + eapply add_rhs_holds; eauto. ++ constructor. rewrite Regmap.gss. congruence. + intros. apply Regmap.gso; auto. Qed. @@ -393,10 +393,10 @@ Lemma add_load_holds: Proof. unfold add_load; intros. destruct (valnum_regs n args) as [n1 vl] eqn:VN. - exploit valnum_regs_holds; eauto. + exploit valnum_regs_holds; eauto. intros (valu2 & A & B & C & D & E). - eapply add_rhs_holds; eauto. -+ econstructor. rewrite <- B; eauto. rewrite Regmap.gss; auto. + eapply add_rhs_holds; eauto. ++ econstructor. rewrite <- B; eauto. rewrite Regmap.gss; auto. + intros. apply Regmap.gso; auto. Qed. @@ -408,13 +408,13 @@ Proof. intros; constructor; simpl; intros. - constructor; simpl; intros. + eauto with cse. - + rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r). - discriminate. + + rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r). + discriminate. eauto with cse. - + exploit forget_reg_charact; eauto with cse. intros [A B]. + + exploit forget_reg_charact; eauto with cse. intros [A B]. rewrite PTree.gro; eauto with cse. - eauto with cse. -- rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r). +- rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r). discriminate. rewrite Regmap.gso; eauto with cse. Qed. @@ -429,7 +429,7 @@ Qed. Lemma kill_eqs_charact: forall pred l strict r eqs, - In (Eq l strict r) (kill_eqs pred eqs) -> + In (Eq l strict r) (kill_eqs pred eqs) -> pred r = false /\ In (Eq l strict r) eqs. Proof. induction eqs; simpl; intros. @@ -451,7 +451,7 @@ Proof. intros; constructor; simpl; intros. - constructor; simpl; intros; eauto with cse. destruct e. exploit kill_eqs_charact; eauto. intros [A B]. eauto with cse. -- destruct eq. exploit kill_eqs_charact; eauto. intros [A B]. +- destruct eq. exploit kill_eqs_charact; eauto. intros [A B]. exploit num_holds_eq; eauto. intro EH; inv EH; econstructor; eauto. - eauto with cse. Qed. @@ -461,7 +461,7 @@ Lemma kill_all_loads_hold: numbering_holds valu ge sp rs m n -> numbering_holds valu ge sp rs m' (kill_all_loads n). Proof. - intros. eapply kill_equations_hold; eauto. + intros. eapply kill_equations_hold; eauto. unfold filter_loads; intros. inv H1. constructor. rewrite <- H2. apply op_depends_on_memory_correct; auto. discriminate. @@ -486,11 +486,11 @@ Proof. econstructor; eauto. rewrite <- H9. destruct a; simpl in H1; try discriminate. destruct a0; simpl in H9; try discriminate. - simpl. + simpl. rewrite negb_false_iff in H6. unfold aaddressing in H6. eapply Mem.load_store_other. eauto. - eapply pdisjoint_sound. eauto. - apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. + eapply pdisjoint_sound. eauto. + apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va. Qed. @@ -516,22 +516,22 @@ Lemma add_store_result_hold: approx = VA.State ae am -> exists valu2, numbering_holds valu2 ge sp rs m' (add_store_result approx n chunk addr args src). Proof. - unfold add_store_result; intros. - unfold avalue; rewrite H3. + unfold add_store_result; intros. + unfold avalue; rewrite H3. destruct (vincl (AE.get src ae) (store_normalized_range chunk)) eqn:INCL. - destruct (valnum_reg n src) as [n1 vsrc] eqn:VR1. destruct (valnum_regs n1 args) as [n2 vargs] eqn:VR2. - exploit valnum_reg_holds; eauto. intros (valu2 & A & B & C & D & E). + exploit valnum_reg_holds; eauto. intros (valu2 & A & B & C & D & E). exploit valnum_regs_holds; eauto. intros (valu3 & P & Q & R & S & T). exists valu3. constructor; simpl; intros. + constructor; simpl; intros; eauto with cse. - destruct H4; eauto with cse. subst e. split. - eapply Plt_le_trans; eauto. + destruct H4; eauto with cse. subst e. split. + eapply Plt_le_trans; eauto. red; simpl; intros. auto. + destruct H4; eauto with cse. subst eq. apply eq_holds_lessdef with (Val.load_result chunk rs#src). apply load_eval_to with a. rewrite <- Q; auto. destruct a; try discriminate. simpl. eapply Mem.load_store_same; eauto. - rewrite B. rewrite R by auto. apply store_normalized_range_sound with bc. + rewrite B. rewrite R by auto. apply store_normalized_range_sound with bc. rewrite <- B. eapply vmatch_ge. apply vincl_ge; eauto. apply H2. + eauto with cse. @@ -557,12 +557,12 @@ Proof. - destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate. econstructor; eauto. rewrite <- H11. destruct a; simpl in H10; try discriminate. - simpl. + simpl. rewrite negb_false_iff in H8. eapply Mem.load_storebytes_other. eauto. - rewrite H6. rewrite nat_of_Z_eq by auto. - eapply pdisjoint_sound. eauto. - unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. + rewrite H6. rewrite nat_of_Z_eq by auto. + eapply pdisjoint_sound. eauto. + unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. auto. Qed. @@ -576,14 +576,14 @@ Lemma load_memcpy: (align_chunk chunk | ofs2 - ofs1) -> Mem.load chunk m' b2 (i + (ofs2 - ofs1)) = Some v. Proof. - intros. + intros. generalize (size_chunk_pos chunk); intros SPOS. set (n1 := i - ofs1). set (n2 := size_chunk chunk). set (n3 := sz - (n1 + n2)). replace sz with (n1 + (n2 + n3)) in H by (unfold n3, n2, n1; omega). - exploit Mem.loadbytes_split; eauto. - unfold n1; omega. + exploit Mem.loadbytes_split; eauto. + unfold n1; omega. unfold n3, n2, n1; omega. intros (bytes1 & bytes23 & LB1 & LB23 & EQ). clear H. @@ -591,7 +591,7 @@ Proof. unfold n2; omega. unfold n3, n2, n1; omega. intros (bytes2 & bytes3 & LB2 & LB3 & EQ'). - subst bytes23; subst bytes. + subst bytes23; subst bytes. exploit Mem.load_loadbytes; eauto. intros (bytes2' & A & B). assert (bytes2' = bytes2). { replace (ofs1 + n1) with i in LB2 by (unfold n1; omega). unfold n2 in LB2. congruence. } @@ -604,17 +604,17 @@ Proof. { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n1; omega. } assert (L2: Z.of_nat (length bytes2) = n2). { erewrite Mem.loadbytes_length by eauto. apply nat_of_Z_eq. unfold n2; omega. } - rewrite L1 in *. rewrite L2 in *. + rewrite L1 in *. rewrite L2 in *. assert (LB': Mem.loadbytes m2 b2 (ofs2 + n1) n2 = Some bytes2). { rewrite <- L2. eapply Mem.loadbytes_storebytes_same; eauto. } assert (LB'': Mem.loadbytes m' b2 (ofs2 + n1) n2 = Some bytes2). - { rewrite <- LB'. eapply Mem.loadbytes_storebytes_other; eauto. - unfold n2; omega. + { rewrite <- LB'. eapply Mem.loadbytes_storebytes_other; eauto. + unfold n2; omega. right; left; omega. } - exploit Mem.load_valid_access; eauto. intros [P Q]. + exploit Mem.load_valid_access; eauto. intros [P Q]. rewrite B. apply Mem.loadbytes_load. - replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; omega). - exact LB''. + replace (i + (ofs2 - ofs1)) with (ofs2 + n1) by (unfold n1; omega). + exact LB''. apply Z.divide_add_r; auto. Qed. @@ -625,7 +625,7 @@ Lemma shift_memcpy_eq_wf: wf_equation next e'. Proof with (try discriminate). unfold shift_memcpy_eq; intros. - destruct e. destruct r... destruct a... + destruct e. destruct r... destruct a... destruct (zle src (Int.unsigned i) && zle (Int.unsigned i + size_chunk m) (src + sz) && zeq (delta mod align_chunk m) 0 && zle 0 (Int.unsigned i + delta) && @@ -642,7 +642,7 @@ Lemma shift_memcpy_eq_holds: equation_holds valu ge (Vptr sp Int.zero) m' e'. Proof with (try discriminate). intros. set (delta := dst - src) in *. unfold shift_memcpy_eq in H. - destruct e as [l strict rhs] eqn:E. + destruct e as [l strict rhs] eqn:E. destruct rhs as [op vl | chunk addr vl]... destruct addr... set (i1 := Int.unsigned i) in *. set (j := i1 + delta) in *. @@ -656,16 +656,16 @@ Proof with (try discriminate). Mem.loadv chunk m (Vptr sp i) = Some v -> Mem.loadv chunk m' (Vptr sp (Int.repr j)) = Some v). { - simpl; intros. rewrite Int.unsigned_repr by omega. - unfold j, delta. eapply load_memcpy; eauto. + simpl; intros. rewrite Int.unsigned_repr by omega. + unfold j, delta. eapply load_memcpy; eauto. apply Zmod_divide; auto. generalize (align_chunk_pos chunk); omega. } inv H2. + inv H3. destruct vl... simpl in H6. rewrite Int.add_zero_l in H6. inv H6. - apply eq_holds_strict. econstructor. simpl. rewrite Int.add_zero_l. eauto. + apply eq_holds_strict. econstructor. simpl. rewrite Int.add_zero_l. eauto. apply LD; auto. + inv H4. destruct vl... simpl in H7. rewrite Int.add_zero_l in H7. inv H7. - apply eq_holds_lessdef with v; auto. + apply eq_holds_lessdef with v; auto. econstructor. simpl. rewrite Int.add_zero_l. eauto. apply LD; auto. Qed. @@ -677,7 +677,7 @@ Proof. induction eqs1; simpl; intros. - auto. - destruct (shift_memcpy_eq src sz delta a) as [e''|] eqn:SHIFT. - + destruct H. subst e''. right; exists a; auto. + + destruct H. subst e''. right; exists a; auto. destruct IHeqs1 as [A | [e [A B]]]; auto. right; exists e; auto. + destruct IHeqs1 as [A | [e [A B]]]; auto. right; exists e; auto. Qed. @@ -695,7 +695,7 @@ Lemma add_memcpy_holds: numbering_holds valu ge (Vptr sp Int.zero) rs m' (add_memcpy n1 n2 asrc adst sz). Proof. intros. unfold add_memcpy. - destruct asrc; auto; destruct adst; auto. + destruct asrc; auto; destruct adst; auto. assert (A: forall b o i, pmatch bc b o (Stk i) -> b = sp /\ i = o). { intros. inv H7. split; auto. eapply bc_stack; eauto. @@ -703,11 +703,11 @@ Proof. apply A in H3; destruct H3. subst bsrc ofs. apply A in H4; destruct H4. subst bdst ofs0. constructor; simpl; intros; eauto with cse. -- constructor; simpl; eauto with cse. +- constructor; simpl; eauto with cse. intros. exploit add_memcpy_eqs_charact; eauto. intros [X | (e0 & X & Y)]. eauto with cse. - apply wf_equation_incr with (num_next n1); auto. - eapply shift_memcpy_eq_wf; eauto with cse. + apply wf_equation_incr with (num_next n1); auto. + eapply shift_memcpy_eq_wf; eauto with cse. - exploit add_memcpy_eqs_charact; eauto. intros [X | (e0 & X & Y)]. eauto with cse. eapply shift_memcpy_eq_holds; eauto with cse. @@ -747,7 +747,7 @@ Proof. assert (sem op1 (map valu args1) = Some res). rewrite <- H0. eapply f_sound; eauto. simpl; intros. - exploit num_holds_eq; eauto. + exploit num_holds_eq; eauto. eapply find_valnum_num_charact; eauto with cse. intros EH; inv EH; auto. destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ] eqn:?. @@ -765,7 +765,7 @@ Lemma reduce_sound: sem op rs##rl = Some res -> sem op' rs##rl' = Some res. Proof. - unfold reduce; intros. + unfold reduce; intros. destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ] eqn:?; inv H. eapply reduce_rec_sound; eauto. congruence. auto. @@ -775,8 +775,8 @@ End REDUCE. (** The numberings associated to each instruction by the static analysis are inductively satisfiable, in the following sense: the numbering - at the function entry point is satisfiable, and for any RTL execution - from [pc] to [pc'], satisfiability at [pc] implies + at the function entry point is satisfiable, and for any RTL execution + from [pc] to [pc'], satisfiability at [pc] implies satisfiability at [pc']. *) Theorem analysis_correct_1: @@ -797,7 +797,7 @@ Theorem analysis_correct_entry: analyze f vapprox = Some approx -> exists valu, numbering_holds valu ge sp rs m approx!!(f.(fn_entrypoint)). Proof. - intros. + intros. replace (approx!!(f.(fn_entrypoint))) with Solver.L.top. exists (fun v => Vundef). apply empty_numbering_holds. symmetry. eapply Solver.fixpoint_entry; eauto. @@ -843,7 +843,7 @@ Lemma sig_preserved: Proof. unfold transf_fundef; intros. destruct f; monadInv H; auto. unfold transf_function in EQ. - destruct (analyze f (vanalyze rm f)); try discriminate. inv EQ; auto. + destruct (analyze f (vanalyze rm f)); try discriminate. inv EQ; auto. Qed. Definition transf_function' (f: function) (approxs: PMap.t numbering) : function := @@ -868,7 +868,7 @@ Lemma set_reg_lessdef: forall r v1 v2 rs1 rs2, Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2). Proof. - intros; red; intros. repeat rewrite Regmap.gsspec. + intros; red; intros. repeat rewrite Regmap.gsspec. destruct (peq r0 r); auto. Qed. @@ -958,7 +958,7 @@ Ltac TransfInstr := | H1: (PTree.get ?pc ?c = Some ?instr), f: function, approx: PMap.t numbering |- _ => cut ((transf_function' f approx).(fn_code)!pc = Some(transf_instr approx!!pc instr)); [ simpl transf_instr - | unfold transf_function', transf_code; simpl; rewrite PTree.gmap; + | unfold transf_function', transf_code; simpl; rewrite PTree.gmap; unfold option_map; rewrite H1; reflexivity ] end. @@ -975,8 +975,8 @@ Proof. (* Inop *) - econstructor; split. eapply exec_Inop; eauto. - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H; auto. (* Iop *) @@ -987,9 +987,9 @@ Proof. econstructor; split. eapply exec_Iop with (v := v'); eauto. rewrite <- A. apply eval_operation_preserved. exact symbols_preserved. - econstructor; eauto. + econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. + unfold transfer; rewrite H. destruct SAT as [valu NH]. eapply add_op_holds; eauto. apply set_reg_lessdef; auto. + (* possibly optimized *) @@ -998,31 +998,31 @@ Proof. exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). destruct (find_rhs n1 (Op op vl)) as [r|] eqn:?. * (* replaced by move *) - exploit find_rhs_sound; eauto. intros (v' & EV & LD). + exploit find_rhs_sound; eauto. intros (v' & EV & LD). assert (v' = v) by (inv EV; congruence). subst v'. econstructor; split. eapply exec_Iop; eauto. simpl; eauto. - econstructor; eauto. + econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_op_holds; eauto. + unfold transfer; rewrite H. + eapply add_op_holds; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. * (* possibly simplified *) destruct (reduce operation combine_op n1 op args vl) as [op' args'] eqn:?. assert (RES: eval_operation ge sp op' rs##args' m = Some v). - eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. + eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. intros; eapply combine_op_sound; eauto. exploit eval_operation_lessdef. eapply regs_lessdef_regs; eauto. eauto. eauto. intros [v' [A B]]. econstructor; split. - eapply exec_Iop with (v := v'); eauto. + eapply exec_Iop with (v := v'); eauto. rewrite <- A. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_op_holds; eauto. - apply set_reg_lessdef; auto. + unfold transfer; rewrite H. + eapply add_op_holds; eauto. + apply set_reg_lessdef; auto. - (* Iload *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. @@ -1030,31 +1030,31 @@ Proof. exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. + (* replaced by move *) - exploit find_rhs_sound; eauto. intros (v' & EV & LD). + exploit find_rhs_sound; eauto. intros (v' & EV & LD). assert (v' = v) by (inv EV; congruence). subst v'. econstructor; split. eapply exec_Iop; eauto. simpl; eauto. - econstructor; eauto. + econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_load_holds; eauto. + unfold transfer; rewrite H. + eapply add_load_holds; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. + (* load is preserved, but addressing is possibly simplified *) destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). - { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. intros; eapply combine_addr_sound; eauto. } exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR. intros [a' [A B]]. assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a'). { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. } - exploit Mem.loadv_extends; eauto. + exploit Mem.loadv_extends; eauto. intros [v' [X Y]]. econstructor; split. eapply exec_Iload; eauto. econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. eapply add_load_holds; eauto. apply set_reg_lessdef; auto. @@ -1064,7 +1064,7 @@ Proof. exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). - { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. intros; eapply combine_addr_sound; eauto. } exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR. intros [a' [A B]]. @@ -1074,35 +1074,35 @@ Proof. econstructor; split. eapply exec_Istore; eauto. econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. + eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. inv SOUND. - eapply add_store_result_hold; eauto. + eapply add_store_result_hold; eauto. eapply kill_loads_after_store_holds; eauto. - (* Icall *) - exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. + exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. econstructor; split. eapply exec_Icall; eauto. apply sig_preserved; auto. - econstructor; eauto. - econstructor; eauto. - intros. eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. + econstructor; eauto. + econstructor; eauto. + intros. eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. exists (fun _ => Vundef); apply empty_numbering_holds. apply regs_lessdef_regs; auto. - (* Itailcall *) - exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. + exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]]. econstructor; split. eapply exec_Itailcall; eauto. apply sig_preserved; auto. - econstructor; eauto. + econstructor; eauto. apply regs_lessdef_regs; auto. - (* Ibuiltin *) - exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. + exploit (@eval_builtin_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. intros (vargs' & A & B). exploit external_call_mem_extends; eauto. intros (v' & m1' & P & Q & R & S). @@ -1124,7 +1124,7 @@ Proof. { exists valu. apply set_res_unknown_holds. eapply kill_all_loads_hold; eauto. } destruct ef. + apply CASE1. - + apply CASE3. + + apply CASE3. + apply CASE2; inv H1; auto. + apply CASE3. + apply CASE1. @@ -1133,15 +1133,15 @@ Proof. simpl in H1. inv H1. exists valu. apply set_res_unknown_holds. - inv SOUND. unfold vanalyze, rm; rewrite AN. + inv SOUND. unfold vanalyze, rm; rewrite AN. assert (pmatch bc bsrc osrc (aaddr_arg (VA.State ae am) a0)) - by (eapply aaddr_arg_sound_1; eauto). + by (eapply aaddr_arg_sound_1; eauto). assert (pmatch bc bdst odst (aaddr_arg (VA.State ae am) a1)) - by (eapply aaddr_arg_sound_1; eauto). - eapply add_memcpy_holds; eauto. - eapply kill_loads_after_storebytes_holds; eauto. - eapply Mem.loadbytes_length; eauto. - simpl. apply Ple_refl. + by (eapply aaddr_arg_sound_1; eauto). + eapply add_memcpy_holds; eauto. + eapply kill_loads_after_storebytes_holds; eauto. + eapply Mem.loadbytes_length; eauto. + simpl. apply Ple_refl. + apply CASE2; inv H1; auto. + apply CASE2; inv H1; auto. + apply CASE1. @@ -1154,10 +1154,10 @@ Proof. exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). destruct (reduce condition combine_cond n1 cond args vl) as [cond' args'] eqn:?. assert (RES: eval_condition cond' rs##args' m = Some b). - { eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. + { eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. intros; eapply combine_cond_sound; eauto. } econstructor; split. - eapply exec_Icond; eauto. + eapply exec_Icond; eauto. eapply eval_condition_lessdef; eauto. apply regs_lessdef_regs; auto. econstructor; eauto. destruct b; eapply analysis_correct_1; eauto; simpl; auto; @@ -1166,7 +1166,7 @@ Proof. - (* Ijumptable *) generalize (RLD arg); rewrite H0; intro LD; inv LD. econstructor; split. - eapply exec_Ijumptable; eauto. + eapply exec_Ijumptable; eauto. econstructor; eauto. eapply analysis_correct_1; eauto. simpl. eapply list_nth_z_in; eauto. unfold transfer; rewrite H; auto. @@ -1176,21 +1176,21 @@ Proof. econstructor; split. eapply exec_Ireturn; eauto. econstructor; eauto. - destruct or; simpl; auto. + destruct or; simpl; auto. - (* internal function *) - monadInv H6. unfold transf_function in EQ. - destruct (analyze f (vanalyze rm f)) as [approx|] eqn:?; inv EQ. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + monadInv H6. unfold transf_function in EQ. + destruct (analyze f (vanalyze rm f)) as [approx|] eqn:?; inv EQ. + exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. intros (m'' & A & B). econstructor; split. - eapply exec_function_internal; simpl; eauto. + eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. eapply analysis_correct_entry; eauto. apply init_regs_lessdef; auto. - (* external function *) - monadInv H6. + monadInv H6. exploit external_call_mem_extends; eauto. intros (v' & m1' & P & Q & R & S). econstructor; split. @@ -1211,7 +1211,7 @@ Lemma transf_initial_states: forall st1, initial_state prog st1 -> exists st2, initial_state tprog st2 /\ match_states st1 st2. Proof. - intros. inversion H. + intros. inversion H. exploit funct_ptr_translated; eauto. intros [tf [A B]]. exists (Callstate nil tf nil m0); split. econstructor; eauto. @@ -1224,10 +1224,10 @@ Proof. Qed. Lemma transf_final_states: - forall st1 st2 r, + forall st1 st2 r, match_states st1 st2 -> final_state st1 r -> final_state st2 r. Proof. - intros. inv H0. inv H. inv H5. inv H3. constructor. + intros. inv H0. inv H. inv H5. inv H3. constructor. Qed. Theorem transf_program_correct: @@ -1236,10 +1236,10 @@ Proof. eapply forward_simulation_step with (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2). - eexact public_preserved. -- intros. exploit transf_initial_states; eauto. intros [s2 [A B]]. +- intros. exploit transf_initial_states; eauto. intros [s2 [A B]]. exists s2. split. auto. split. apply sound_initial; auto. auto. - intros. destruct H. eapply transf_final_states; eauto. -- intros. destruct H0. exploit transf_step_correct; eauto. +- intros. destruct H0. exploit transf_step_correct; eauto. intros [s2' [A B]]. exists s2'; split. auto. split. eapply sound_step; eauto. auto. Qed. -- cgit