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 --- backend/CSEproof.v | 1608 +++++++++++++++++++++++++++------------------------- 1 file changed, 830 insertions(+), 778 deletions(-) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 478b6f02..6c9331a6 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -16,6 +16,8 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Errors. +Require Import Integers. +Require Import Floats. Require Import Values. Require Import Memory. Require Import Events. @@ -24,713 +26,692 @@ Require Import Smallstep. Require Import Op. Require Import Registers. Require Import RTL. -Require Import RTLtyping. Require Import Kildall. +Require Import ValueDomain. +Require Import ValueAOp. +Require Import ValueAnalysis. +Require Import CSEdomain. Require Import CombineOp. Require Import CombineOpproof. Require Import CSE. -(** * Semantic properties of value numberings *) +(** * Soundness of operations over value numberings *) -(** ** Well-formedness of numberings *) +Remark wf_equation_incr: + forall next1 next2 e, + wf_equation next1 e -> Ple next1 next2 -> wf_equation next2 e. +Proof. + unfold wf_equation; intros; destruct e. destruct H. split. + apply Plt_le_trans with next1; auto. + red; intros. apply Plt_le_trans with next1; auto. apply H1; auto. +Qed. -(** A numbering is well-formed if all registers mentioned in equations - are less than the ``next'' register number given in the numbering. - This guarantees that the next register is fresh with respect to - the equations. *) +(** Extensionality with respect to valuations. *) -Definition wf_rhs (next: valnum) (rh: rhs) : Prop := - match rh with - | Op op vl => forall v, In v vl -> Plt v next - | Load chunk addr vl => forall v, In v vl -> Plt v next - end. +Definition valu_agree (valu1 valu2: valuation) (upto: valnum) := + forall v, Plt v upto -> valu2 v = valu1 v. -Definition wf_equation (next: valnum) (vr: valnum) (rh: rhs) : Prop := - Plt vr next /\ wf_rhs next rh. +Section EXTEN. -Inductive wf_numbering (n: numbering) : Prop := - wf_numbering_intro - (EQS: forall v rh, - In (v, rh) n.(num_eqs) -> wf_equation n.(num_next) v rh) - (REG: forall r v, - PTree.get r n.(num_reg) = Some v -> Plt v n.(num_next)) - (VAL: forall r v, - In r (PMap.get v n.(num_val)) -> PTree.get r n.(num_reg) = Some v). +Variable valu1: valuation. +Variable upto: valnum. +Variable valu2: valuation. +Hypothesis AGREE: valu_agree valu1 valu2 upto. +Variable ge: genv. +Variable sp: val. +Variable rs: regset. +Variable m: mem. -Lemma wf_empty_numbering: - wf_numbering empty_numbering. +Lemma valnums_val_exten: + forall vl, + (forall v, In v vl -> Plt v upto) -> + map valu2 vl = map valu1 vl. Proof. - unfold empty_numbering; split; simpl; intros. - contradiction. - rewrite PTree.gempty in H. congruence. - rewrite PMap.gi in H. contradiction. + intros. apply list_map_exten. intros. symmetry. auto. Qed. -Lemma wf_rhs_increasing: - forall next1 next2 rh, - Ple next1 next2 -> - wf_rhs next1 rh -> wf_rhs next2 rh. +Lemma rhs_eval_to_exten: + forall r v, + rhs_eval_to valu1 ge sp m r v -> + (forall v, In v (valnums_rhs r) -> Plt v upto) -> + rhs_eval_to valu2 ge sp m r v. Proof. - intros; destruct rh; simpl; intros; apply Plt_Ple_trans with next1; auto. + intros. inv H; simpl in *. +- constructor. rewrite valnums_val_exten by assumption. auto. +- econstructor; eauto. rewrite valnums_val_exten by assumption. auto. Qed. -Lemma wf_equation_increasing: - forall next1 next2 vr rh, - Ple next1 next2 -> - wf_equation next1 vr rh -> wf_equation next2 vr rh. +Lemma equation_holds_exten: + forall e, + equation_holds valu1 ge sp m e -> + wf_equation upto e -> + equation_holds valu2 ge sp m e. Proof. - intros. destruct H0. split. - apply Plt_Ple_trans with next1; auto. - apply wf_rhs_increasing with next1; auto. + intros. destruct e. destruct H0. inv H. +- constructor. rewrite AGREE by auto. apply rhs_eval_to_exten; auto. +- econstructor. apply rhs_eval_to_exten; eauto. rewrite AGREE by auto. auto. Qed. -(** We now show that all operations over numberings - preserve well-formedness. *) - -Lemma wf_valnum_reg: - forall n r n' v, - wf_numbering n -> - valnum_reg n r = (n', v) -> - wf_numbering n' /\ Plt v n'.(num_next) /\ Ple n.(num_next) n'.(num_next). +Lemma numbering_holds_exten: + forall n, + numbering_holds valu1 ge sp rs m n -> + Ple n.(num_next) upto -> + numbering_holds valu2 ge sp rs m n. Proof. - intros until v. unfold valnum_reg. intros WF VREG. inversion WF. - destruct ((num_reg n)!r) as [v'|] eqn:?. -(* found *) - inv VREG. split. auto. split. eauto. apply Ple_refl. -(* not found *) - inv VREG. split. - split; simpl; intros. - apply wf_equation_increasing with (num_next n). apply Ple_succ. auto. - rewrite PTree.gsspec in H. destruct (peq r0 r). - inv H. apply Plt_succ. - apply Plt_trans_succ; eauto. - rewrite PMap.gsspec in H. destruct (peq v (num_next n)). - subst v. simpl in H. destruct H. subst r0. apply PTree.gss. contradiction. - rewrite PTree.gso. eauto. exploit VAL; eauto. congruence. - simpl. split. apply Plt_succ. apply Ple_succ. + 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. Qed. -Lemma wf_valnum_regs: - forall rl n n' vl, - wf_numbering n -> - valnum_regs n rl = (n', vl) -> - wf_numbering n' /\ - (forall v, In v vl -> Plt v n'.(num_next)) /\ - Ple n.(num_next) n'.(num_next). -Proof. - induction rl; intros. - simpl in H0. inversion H0. subst n'; subst vl. - simpl. intuition. - simpl in H0. - caseEq (valnum_reg n a). intros n1 v1 EQ1. - caseEq (valnum_regs n1 rl). intros ns vs EQS. - rewrite EQ1 in H0; rewrite EQS in H0; simpl in H0. - inversion H0. subst n'; subst vl. - generalize (wf_valnum_reg _ _ _ _ H EQ1); intros [A1 [B1 C1]]. - generalize (IHrl _ _ _ A1 EQS); intros [As [Bs Cs]]. - split. auto. - split. simpl; intros. elim H1; intro. - subst v. eapply Plt_Ple_trans; eauto. - auto. - eapply Ple_trans; eauto. -Qed. +End EXTEN. -Lemma find_valnum_rhs_correct: - forall rh vn eqs, - find_valnum_rhs rh eqs = Some vn -> In (vn, rh) eqs. -Proof. - induction eqs; simpl. - congruence. - case a; intros v r'. case (eq_rhs rh r'); intro. - intro. left. congruence. - intro. right. auto. -Qed. +Ltac splitall := repeat (match goal with |- _ /\ _ => split end). -Lemma find_valnum_num_correct: - forall rh vn eqs, - find_valnum_num vn eqs = Some rh -> In (vn, rh) eqs. +Lemma valnum_reg_holds: + forall valu1 ge sp rs m n r n' v, + numbering_holds valu1 ge sp rs m n -> + valnum_reg n r = (n', v) -> + exists valu2, + numbering_holds valu2 ge sp rs m n' + /\ rs#r = valu2 v + /\ valu_agree valu1 valu2 n.(num_next) + /\ Plt v n'.(num_next) + /\ Ple n.(num_next) n'.(num_next). Proof. - induction eqs; simpl. - congruence. - destruct a as [v' r']. destruct (peq vn v'); intros. - left. congruence. - right. auto. + unfold valnum_reg; intros. + destruct (num_reg n)!r as [v'|] eqn:NR. +- inv H0. exists valu1; splitall. + + auto. + + eauto with cse. + + red; auto. + + eauto with cse. + + apply Ple_refl. +- inv H0; simpl. + set (valu2 := fun vn => if peq vn n.(num_next) then rs#r else valu1 vn). + assert (AG: valu_agree valu1 valu2 n.(num_next)). + { red; intros. unfold valu2. apply peq_false. apply Plt_ne; auto. } + exists valu2; splitall. ++ 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). + 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. + 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. + rewrite peq_false. eauto with cse. apply Plt_ne; eauto with cse. ++ unfold valu2. rewrite peq_true; auto. ++ auto. ++ xomega. ++ xomega. Qed. -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. +Lemma valnum_regs_holds: + forall rl valu1 ge sp rs m n n' vl, + numbering_holds valu1 ge sp rs m n -> + valnum_regs n rl = (n', vl) -> + exists valu2, + numbering_holds valu2 ge sp rs m n' + /\ rs##rl = map valu2 vl + /\ valu_agree valu1 valu2 n.(num_next) + /\ (forall v, In v vl -> Plt v n'.(num_next)) + /\ Ple n.(num_next) n'.(num_next). Proof. - induction l; simpl. - tauto. - destruct (eq x a). - subst a. rewrite IHl. tauto. - simpl. rewrite IHl. intuition congruence. + induction rl; simpl; intros. +- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. xomega. +- 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. + intros (valu2 & A & B & C & D & E). + exploit (IHrl valu2); eauto. + intros (valu3 & P & Q & R & S & T). + exists valu3; splitall. + + auto. + + simpl; f_equal; auto. rewrite R; auto. + + red; intros. transitivity (valu2 v); auto. apply R. xomega. + + simpl; intros. destruct H0; auto. subst v1; xomega. + + xomega. Qed. -Lemma wf_forget_reg: - forall n rd r v, - wf_numbering n -> - In r (PMap.get v (forget_reg n rd)) -> r <> rd /\ PTree.get r n.(num_reg) = Some v. +Lemma find_valnum_rhs_charact: + forall rh v eqs, + find_valnum_rhs rh eqs = Some v -> In (Eq v true rh) eqs. Proof. - unfold forget_reg; intros. inversion H. - destruct ((num_reg n)!rd) as [vd|] eqn:?. - rewrite PMap.gsspec in H0. destruct (peq v vd). - subst vd. rewrite in_remove in H0. destruct H0. split. auto. eauto. - split; eauto. exploit VAL; eauto. congruence. - split; eauto. exploit VAL; eauto. congruence. + induction eqs; simpl; intros. +- inv H. +- destruct a. destruct (strict && eq_rhs rh r) eqn:T. + + InvBooleans. inv H. left; auto. + + right; eauto. Qed. -Lemma wf_update_reg: - forall n rd vd r v, - wf_numbering n -> - In r (PMap.get v (update_reg n rd vd)) -> PTree.get r (PTree.set rd vd n.(num_reg)) = Some v. +Lemma find_valnum_rhs'_charact: + forall rh v eqs, + find_valnum_rhs' rh eqs = Some v -> exists strict, In (Eq v strict rh) eqs. Proof. - unfold update_reg; intros. inversion H. rewrite PMap.gsspec in H0. - destruct (peq v vd). - subst v; simpl in H0. destruct H0. - subst r. apply PTree.gss. - exploit wf_forget_reg; eauto. intros [A B]. rewrite PTree.gso; eauto. - exploit wf_forget_reg; eauto. intros [A B]. rewrite PTree.gso; eauto. + induction eqs; simpl; intros. +- inv H. +- destruct a. destruct (eq_rhs rh r) eqn:T. + + inv H. exists strict; auto. + + exploit IHeqs; eauto. intros [s IN]. exists s; auto. Qed. -Lemma wf_add_rhs: - forall n rd rh, - wf_numbering n -> - wf_rhs n.(num_next) rh -> - wf_numbering (add_rhs n rd rh). +Lemma find_valnum_num_charact: + forall v r eqs, find_valnum_num v eqs = Some r -> In (Eq v true r) eqs. Proof. - intros. inversion H. unfold add_rhs. - destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|] eqn:?. -(* found *) - exploit find_valnum_rhs_correct; eauto. intros IN. - split; simpl; intros. - auto. - rewrite PTree.gsspec in H1. destruct (peq r rd). - inv H1. exploit EQS; eauto. intros [A B]. auto. - eauto. - eapply wf_update_reg; eauto. -(* not found *) - split; simpl; intros. - destruct H1. - inv H1. split. apply Plt_succ. apply wf_rhs_increasing with n.(num_next). apply Ple_succ. auto. - apply wf_equation_increasing with n.(num_next). apply Ple_succ. auto. - rewrite PTree.gsspec in H1. destruct (peq r rd). - inv H1. apply Plt_succ. - apply Plt_trans_succ. eauto. - eapply wf_update_reg; eauto. + induction eqs; simpl; intros. +- inv H. +- destruct a. destruct (strict && peq v v0) eqn:T. + + InvBooleans. inv H. auto. + + eauto. Qed. -Lemma wf_add_op: - forall n rd op rs, - wf_numbering n -> - wf_numbering (add_op n rd op rs). +Lemma reg_valnum_sound: + forall n v r valu ge sp rs m, + reg_valnum n v = Some r -> + numbering_holds valu ge sp rs m n -> + rs#r = valu v. Proof. - intros. unfold add_op. destruct (is_move_operation op rs) as [r|] eqn:?. -(* move *) - destruct (valnum_reg n r) as [n' v] eqn:?. - exploit wf_valnum_reg; eauto. intros [A [B C]]. inversion A. - constructor; simpl; intros. - eauto. - rewrite PTree.gsspec in H0. destruct (peq r0 rd). inv H0. auto. eauto. - eapply wf_update_reg; eauto. -(* not a move *) - destruct (valnum_regs n rs) as [n' vs] eqn:?. - exploit wf_valnum_regs; eauto. intros [A [B C]]. - eapply wf_add_rhs; eauto. + 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. + rewrite E; auto with coqlib. Qed. -Lemma wf_add_load: - forall n rd chunk addr rs, - wf_numbering n -> - wf_numbering (add_load n rd chunk addr rs). +Lemma regs_valnums_sound: + forall n valu ge sp rs m, + numbering_holds valu ge sp rs m n -> + forall vl rl, + regs_valnums n vl = Some rl -> + rs##rl = map valu vl. Proof. - intros. unfold add_load. - caseEq (valnum_regs n rs). intros n' vl EQ. - generalize (wf_valnum_regs _ _ _ _ H EQ). intros [A [B C]]. - apply wf_add_rhs; auto. + induction vl; simpl; intros. +- 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. Qed. -Lemma wf_add_unknown: - forall n rd, - wf_numbering n -> - wf_numbering (add_unknown n rd). +Lemma find_rhs_sound: + forall n rh r valu ge sp rs m, + find_rhs n rh = Some r -> + numbering_holds valu ge sp rs m n -> + exists v, rhs_eval_to valu ge sp m rh v /\ Val.lessdef v rs#r. Proof. - intros. inversion H. unfold add_unknown. constructor; simpl; intros. - eapply wf_equation_increasing; eauto. auto with coqlib. - rewrite PTree.gsspec in H0. destruct (peq r rd). - inv H0. auto with coqlib. - apply Plt_trans_succ; eauto. - exploit wf_forget_reg; eauto. intros [A B]. rewrite PTree.gso; eauto. + unfold find_rhs; intros. destruct (find_valnum_rhs' rh (num_eqs n)) as [vres|] eqn:E; try discriminate. + exploit find_valnum_rhs'_charact; eauto. intros [strict IN]. + erewrite reg_valnum_sound by eauto. + exploit num_holds_eq; eauto. intros EH. inv EH. +- exists (valu vres); auto. +- exists v; auto. Qed. -Remark kill_eqs_in: - forall pred v rhs eqs, - In (v, rhs) (kill_eqs pred eqs) -> In (v, rhs) eqs /\ pred rhs = false. +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 eqs; simpl; intros. + induction l; simpl. tauto. - destruct (pred (snd a)) eqn:?. - exploit IHeqs; eauto. tauto. - simpl in H; destruct H. subst a. auto. exploit IHeqs; eauto. tauto. -Qed. - -Lemma wf_kill_equations: - forall pred n, wf_numbering n -> wf_numbering (kill_equations pred n). -Proof. - intros. inversion H. unfold kill_equations; split; simpl; intros. - exploit kill_eqs_in; eauto. intros [A B]. auto. - eauto. - eauto. -Qed. - -Lemma wf_add_store: - forall n chunk addr rargs rsrc, - wf_numbering n -> wf_numbering (add_store n chunk addr rargs rsrc). -Proof. - intros. unfold add_store. - destruct (valnum_regs n rargs) as [n1 vargs] eqn:?. - exploit wf_valnum_regs; eauto. intros [A [B C]]. - assert (wf_numbering (kill_equations (filter_after_store chunk addr vargs) n1)). - apply wf_kill_equations. auto. - destruct chunk; auto; apply wf_add_rhs; auto. + destruct (eq x a). + subst a. rewrite IHl. tauto. + simpl. rewrite IHl. intuition congruence. Qed. -Lemma wf_transfer: - forall f pc n, wf_numbering n -> wf_numbering (transfer f pc n). +Lemma forget_reg_charact: + forall n rd r v, + wf_numbering n -> + In r (PMap.get v (forget_reg n rd)) -> r <> rd /\ In r (PMap.get v n.(num_val)). Proof. - intros. unfold transfer. - destruct (f.(fn_code)!pc); auto. - destruct i; auto. - apply wf_add_op; auto. - apply wf_add_load; auto. - apply wf_add_store; auto. - apply wf_empty_numbering. - apply wf_empty_numbering. - destruct e; (apply wf_empty_numbering || - apply wf_add_unknown; auto; apply wf_kill_equations; auto). -Qed. - -(** As a consequence, the numberings computed by the static analysis - are well formed. *) - -Theorem wf_analyze: - forall f approx pc, analyze f = Some approx -> wf_numbering approx!!pc. + unfold forget_reg; intros. + destruct (PTree.get rd n.(num_reg)) as [vd|] eqn:GET. +- rewrite PMap.gsspec in H0. destruct (peq v vd). + + 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. + +Lemma update_reg_charact: + forall n rd vd r v, + wf_numbering n -> + In r (PMap.get v (update_reg n rd vd)) -> + PTree.get r (PTree.set rd vd n.(num_reg)) = Some v. Proof. - unfold analyze; intros. - eapply Solver.fixpoint_invariant with (P := wf_numbering); eauto. - exact wf_empty_numbering. - intros. eapply wf_transfer; eauto. + unfold update_reg; intros. + rewrite PMap.gsspec in H0. + destruct (peq v vd). +- 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. +- exploit forget_reg_charact; eauto. intros [A B]. + rewrite PTree.gso by auto. eapply wf_num_val; eauto. Qed. -(** ** Properties of satisfiability of numberings *) - -Module ValnumEq. - Definition t := valnum. - Definition eq := peq. -End ValnumEq. - -Module VMap := EMap(ValnumEq). - -Section SATISFIABILITY. - -Variable ge: genv. -Variable sp: val. - -(** Agremment between two mappings from value numbers to values - up to a given value number. *) - -Definition valu_agree (valu1 valu2: valnum -> val) (upto: valnum) : Prop := - forall v, Plt v upto -> valu2 v = valu1 v. - -Lemma valu_agree_refl: - forall valu upto, valu_agree valu valu upto. +Lemma rhs_eval_to_inj: + forall valu ge sp m rh v1 v2, + rhs_eval_to valu ge sp m rh v1 -> rhs_eval_to valu ge sp m rh v2 -> v1 = v2. Proof. - intros; red; auto. + intros. inv H; inv H0; congruence. Qed. -Lemma valu_agree_trans: - forall valu1 valu2 valu3 upto12 upto23, - valu_agree valu1 valu2 upto12 -> - valu_agree valu2 valu3 upto23 -> - Ple upto12 upto23 -> - valu_agree valu1 valu3 upto12. +Lemma add_rhs_holds: + forall valu1 ge sp rs m n rd rh rs', + numbering_holds valu1 ge sp rs m n -> + rhs_eval_to valu1 ge sp m rh (rs'#rd) -> + wf_rhs n.(num_next) rh -> + (forall r, r <> rd -> rs'#r = rs#r) -> + exists valu2, numbering_holds valu2 ge sp rs' m (add_rhs n rd rh). Proof. - intros; red; intros. transitivity (valu2 v). - apply H0. apply Plt_Ple_trans with upto12; auto. - apply H; auto. -Qed. + unfold add_rhs; intros. + destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|] eqn:FIND. + +- (* A value number exists already *) + exploit find_valnum_rhs_charact; eauto. intros IN. + exploit wf_num_eqs; eauto with cse. intros [A B]. + exploit num_holds_eq; eauto. intros EH. inv EH. + assert (rs'#rd = valu1 vres) by (eapply rhs_eval_to_inj; eauto). + exists valu1; constructor; simpl; intros. ++ constructor; simpl; intros. + * eauto with cse. + * rewrite PTree.gsspec in H5. destruct (peq r rd). + inv H5. auto. + eauto with cse. + * eapply update_reg_charact; eauto with cse. ++ eauto with cse. ++ rewrite PTree.gsspec in H5. destruct (peq r rd). + congruence. + rewrite H2 by auto. eauto with cse. -Lemma valu_agree_list: - forall valu1 valu2 upto vl, - valu_agree valu1 valu2 upto -> - (forall v, In v vl -> Plt v upto) -> - map valu2 vl = map valu1 vl. -Proof. - intros. apply list_map_exten. intros. symmetry. apply H. auto. +- (* Assigning a new value number *) + set (valu2 := fun v => if peq v n.(num_next) then rs'#rd else valu1 v). + assert (AG: valu_agree valu1 valu2 n.(num_next)). + { 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. + * 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. ++ 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. + apply Plt_ne; eauto with cse. Qed. -(** The [numbering_holds] predicate (defined in file [CSE]) is - extensional with respect to [valu_agree]. *) - -Lemma numbering_holds_exten: - forall valu1 valu2 n rs m, - valu_agree valu1 valu2 n.(num_next) -> - wf_numbering n -> +Lemma add_op_holds: + forall valu1 ge sp rs m n op (args: list reg) v dst, numbering_holds valu1 ge sp rs m n -> - numbering_holds valu2 ge sp rs m n. + eval_operation ge sp op rs##args m = Some v -> + exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_op n dst op args). Proof. - intros. inversion H0. inversion H1. split; intros. - exploit EQS; eauto. intros [A B]. red in B. - generalize (H2 _ _ H4). - unfold equation_holds; destruct rh. - rewrite (valu_agree_list valu1 valu2 n.(num_next)). - rewrite H. auto. auto. auto. auto. - rewrite (valu_agree_list valu1 valu2 n.(num_next)). - rewrite H. auto. auto. auto. auto. - rewrite H. auto. eauto. + unfold add_op; intros. + destruct (is_move_operation op args) as [src|] eqn:ISMOVE. +- (* special case for moves *) + 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. + intros (valu2 & A & B & C & D & E). + exists valu2; constructor; simpl; intros. ++ constructor; simpl; intros; eauto with cse. + * rewrite PTree.gsspec in H0. destruct (peq r dst). + inv H0. auto. + eauto with cse. + * eapply update_reg_charact; eauto with cse. ++ eauto with cse. ++ 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. + intros (valu2 & A & B & C & D & E). + eapply add_rhs_holds; eauto. ++ constructor. rewrite Regmap.gss. congruence. ++ intros. apply Regmap.gso; auto. Qed. -(** [valnum_reg] and [valnum_regs] preserve the [numbering_holds] predicate. - Moreover, it is always the case that the returned value number has - the value of the given register in the final assignment of values to - value numbers. *) - -Lemma valnum_reg_holds: - forall valu1 rs n r n' v m, - wf_numbering n -> +Lemma add_load_holds: + forall valu1 ge sp rs m n addr (args: list reg) a chunk v dst, numbering_holds valu1 ge sp rs m n -> - valnum_reg n r = (n', v) -> - exists valu2, - numbering_holds valu2 ge sp rs m n' /\ - valu2 v = rs#r /\ - valu_agree valu1 valu2 n.(num_next). + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + exists valu2, numbering_holds valu2 ge sp (rs#dst <- v) m (add_load n dst chunk addr args). Proof. - intros until v. unfold valnum_reg. - caseEq (n.(num_reg)!r). - (* Register already has a value number *) - intros. inversion H2. subst n'; subst v0. - inversion H1. - exists valu1. split. auto. - split. symmetry. auto. - apply valu_agree_refl. - (* Register gets a fresh value number *) - intros. inversion H2. subst n'. subst v. inversion H1. - set (valu2 := VMap.set n.(num_next) rs#r valu1). - assert (AG: valu_agree valu1 valu2 n.(num_next)). - red; intros. unfold valu2. apply VMap.gso. - auto with coqlib. - destruct (numbering_holds_exten _ _ _ _ _ AG H0 H1) as [A B]. - exists valu2. - split. split; simpl; intros. auto. - unfold valu2, VMap.set, ValnumEq.eq. - rewrite PTree.gsspec in H5. destruct (peq r0 r). - inv H5. rewrite peq_true. auto. - rewrite peq_false. auto. - assert (Plt vn (num_next n)). inv H0. eauto. - red; intros; subst; eapply Plt_strict; eauto. - split. unfold valu2. rewrite VMap.gss. auto. - auto. + unfold add_load; intros. + destruct (valnum_regs n args) as [n1 vl] eqn:VN. + 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. ++ intros. apply Regmap.gso; auto. Qed. -Lemma valnum_regs_holds: - forall rs rl valu1 n n' vl m, - wf_numbering n -> - numbering_holds valu1 ge sp rs m n -> - valnum_regs n rl = (n', vl) -> - exists valu2, - numbering_holds valu2 ge sp rs m n' /\ - List.map valu2 vl = rs##rl /\ - valu_agree valu1 valu2 n.(num_next). +Lemma set_unknown_holds: + forall valu ge sp rs m n r v, + numbering_holds valu ge sp rs m n -> + numbering_holds valu ge sp (rs#r <- v) m (set_unknown n r). Proof. - induction rl; simpl; intros. - (* base case *) - inversion H1; subst n'; subst vl. - exists valu1. split. auto. split. auto. apply valu_agree_refl. - (* inductive case *) - caseEq (valnum_reg n a); intros n1 v1 EQ1. - caseEq (valnum_regs n1 rl); intros ns vs EQs. - rewrite EQ1 in H1; rewrite EQs in H1. inversion H1. subst vl; subst n'. - generalize (valnum_reg_holds _ _ _ _ _ _ _ H H0 EQ1). - intros [valu2 [A [B C]]]. - generalize (wf_valnum_reg _ _ _ _ H EQ1). intros [D [E F]]. - generalize (IHrl _ _ _ _ _ D A EQs). - intros [valu3 [P [Q R]]]. - exists valu3. - split. auto. - split. simpl. rewrite R. congruence. auto. - eapply valu_agree_trans; eauto. + intros; constructor; simpl; intros. +- constructor; simpl; intros. + + eauto with cse. + + 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]. + rewrite PTree.gro; eauto with cse. +- eauto with cse. +- rewrite PTree.grspec in H0. destruct (PTree.elt_eq r0 r). + discriminate. + rewrite Regmap.gso; eauto with cse. Qed. -(** A reformulation of the [equation_holds] predicate in terms - of the value to which a right-hand side of an equation evaluates. *) - -Definition rhs_evals_to - (valu: valnum -> val) (rh: rhs) (m: mem) (v: val) : Prop := - match rh with - | Op op vl => - eval_operation ge sp op (List.map valu vl) m = Some v - | Load chunk addr vl => - exists a, - eval_addressing ge sp addr (List.map valu vl) = Some a /\ - Mem.loadv chunk m a = Some v - end. - -Lemma equation_evals_to_holds_1: - forall valu rh v vres m, - rhs_evals_to valu rh m v -> - equation_holds valu ge sp m vres rh -> - valu vres = v. +Lemma kill_eqs_charact: + forall pred l strict r eqs, + In (Eq l strict r) (kill_eqs pred eqs) -> + pred r = false /\ In (Eq l strict r) eqs. Proof. - intros until m. unfold rhs_evals_to, equation_holds. - destruct rh. congruence. - intros [a1 [A1 B1]] [a2 [A2 B2]]. congruence. + induction eqs; simpl; intros. +- tauto. +- destruct a. destruct (pred r0) eqn:PRED. + tauto. + inv H. inv H0. auto. tauto. Qed. -Lemma equation_evals_to_holds_2: - forall valu rh v vres m, - wf_rhs vres rh -> - rhs_evals_to valu rh m v -> - equation_holds (VMap.set vres v valu) ge sp m vres rh. +Lemma kill_equations_hold: + forall valu ge sp rs m n pred m', + numbering_holds valu ge sp rs m n -> + (forall r v, + pred r = false -> + rhs_eval_to valu ge sp m r v -> + rhs_eval_to valu ge sp m' r v) -> + numbering_holds valu ge sp rs m' (kill_equations pred n). Proof. - intros until m. unfold wf_rhs, rhs_evals_to, equation_holds. - rewrite VMap.gss. - assert (forall vl: list valnum, - (forall v, In v vl -> Plt v vres) -> - map (VMap.set vres v valu) vl = map valu vl). - intros. apply list_map_exten. intros. - symmetry. apply VMap.gso. apply Plt_ne. auto. - destruct rh; intros; rewrite H; auto. + 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]. + exploit num_holds_eq; eauto. intro EH; inv EH; econstructor; eauto. +- eauto with cse. Qed. -(** The numbering obtained by adding an equation [rd = rhs] is satisfiable - in a concrete register set where [rd] is set to the value of [rhs]. *) - -Lemma add_rhs_satisfiable_gen: - forall n rh valu1 rs rd rs' m, - wf_numbering n -> - wf_rhs n.(num_next) rh -> - numbering_holds valu1 ge sp rs m n -> - rhs_evals_to valu1 rh m (rs'#rd) -> - (forall r, r <> rd -> rs'#r = rs#r) -> - numbering_satisfiable ge sp rs' m (add_rhs n rd rh). +Lemma kill_all_loads_hold: + forall valu ge sp rs m n m', + numbering_holds valu ge sp rs m n -> + numbering_holds valu ge sp rs m' (kill_all_loads n). Proof. - intros. unfold add_rhs. - caseEq (find_valnum_rhs rh n.(num_eqs)). - (* RHS found *) - intros vres FINDVN. inversion H1. - exists valu1. split; simpl; intros. - auto. - rewrite PTree.gsspec in H6. - destruct (peq r rd). - inv H6. - symmetry. eapply equation_evals_to_holds_1; eauto. - apply H4. apply find_valnum_rhs_correct. congruence. - rewrite H3; auto. - (* RHS not found *) - intro FINDVN. - set (valu2 := VMap.set n.(num_next) (rs'#rd) valu1). - assert (AG: valu_agree valu1 valu2 n.(num_next)). - red; intros. unfold valu2. apply VMap.gso. - auto with coqlib. - elim (numbering_holds_exten _ _ _ _ _ AG H H1); intros. - exists valu2. split; simpl; intros. - destruct H6. - inv H6. unfold valu2. eapply equation_evals_to_holds_2; eauto. auto. - rewrite PTree.gsspec in H6. destruct (peq r rd). - unfold valu2. inv H6. rewrite VMap.gss. auto. - rewrite H3; auto. + intros. eapply kill_equations_hold; eauto. + unfold filter_loads; intros. inv H1. + constructor. rewrite <- H2. apply op_depends_on_memory_correct; auto. + discriminate. Qed. -Lemma add_rhs_satisfiable: - forall n rh valu1 rs rd v m, - wf_numbering n -> - wf_rhs n.(num_next) rh -> - numbering_holds valu1 ge sp rs m n -> - rhs_evals_to valu1 rh m v -> - numbering_satisfiable ge sp (rs#rd <- v) m (add_rhs n rd rh). +Lemma kill_loads_after_store_holds: + forall valu ge sp rs m n addr args a chunk v m' bc approx ae am, + numbering_holds valu ge (Vptr sp Int.zero) rs m n -> + eval_addressing ge (Vptr sp Int.zero) addr rs##args = Some a -> + Mem.storev chunk m a v = Some m' -> + genv_match bc ge -> + bc sp = BCstack -> + ematch bc rs ae -> + approx = VA.State ae am -> + numbering_holds valu ge (Vptr sp Int.zero) rs m' + (kill_loads_after_store approx n chunk addr args). Proof. - intros. eapply add_rhs_satisfiable_gen; eauto. - rewrite Regmap.gss; auto. - intros. apply Regmap.gso; auto. + intros. apply kill_equations_hold with m; auto. + intros. unfold filter_after_store in H6; inv H7. +- constructor. rewrite <- H8. apply op_depends_on_memory_correct; auto. +- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate. + econstructor; eauto. rewrite <- H9. + destruct a; simpl in H1; try discriminate. + destruct a0; simpl in H9; try discriminate. + 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. + erewrite <- regs_valnums_sound by eauto. eauto with va. + apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto with va. Qed. -(** [add_op] returns a numbering that is satisfiable in the register - set after execution of the corresponding [Iop] instruction. *) - -Lemma add_op_satisfiable: - forall n rs op args dst v m, - wf_numbering n -> - numbering_satisfiable ge sp rs m n -> - eval_operation ge sp op rs##args m = Some v -> - numbering_satisfiable ge sp (rs#dst <- v) m (add_op n dst op args). +Lemma store_normalized_range_sound: + forall bc chunk v, + vmatch bc v (store_normalized_range chunk) -> + Val.lessdef (Val.load_result chunk v) v. Proof. - intros. inversion H0. - unfold add_op. - caseEq (@is_move_operation reg op args). - intros arg EQ. - destruct (is_move_operation_correct _ _ EQ) as [A B]. subst op args. - caseEq (valnum_reg n arg). intros n1 v1 VL. - generalize (valnum_reg_holds _ _ _ _ _ _ _ H H2 VL). intros [valu2 [A [B C]]]. - generalize (wf_valnum_reg _ _ _ _ H VL). intros [D [E F]]. - elim A; intros. exists valu2; split; simpl; intros. - auto. rewrite Regmap.gsspec. rewrite PTree.gsspec in H5. - destruct (peq r dst). simpl in H1. congruence. auto. - intro NEQ. caseEq (valnum_regs n args). intros n1 vl VRL. - generalize (valnum_regs_holds _ _ _ _ _ _ _ H H2 VRL). intros [valu2 [A [B C]]]. - generalize (wf_valnum_regs _ _ _ _ H VRL). intros [D [E F]]. - apply add_rhs_satisfiable with valu2; auto. - simpl. congruence. + intros. destruct chunk; simpl in *; destruct v; auto. +- inv H. rewrite is_sgn_sign_ext in H3 by omega. rewrite H3; auto. +- inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto. +- inv H. rewrite is_sgn_sign_ext in H3 by omega. rewrite H3; auto. +- inv H. rewrite is_uns_zero_ext in H3 by omega. rewrite H3; auto. +- inv H. rewrite Float.singleoffloat_of_single by auto. auto. Qed. -(** [add_load] returns a numbering that is satisfiable in the register - set after execution of the corresponding [Iload] instruction. *) - -Lemma add_load_satisfiable: - forall n rs chunk addr args dst a v m, - wf_numbering n -> - numbering_satisfiable ge sp rs m n -> +Lemma add_store_result_hold: + forall valu1 ge sp rs m' n addr args a chunk m src bc ae approx am, + numbering_holds valu1 ge sp rs m' n -> eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - numbering_satisfiable ge sp (rs#dst <- v) m (add_load n dst chunk addr args). + Mem.storev chunk m a rs#src = Some m' -> + ematch bc rs ae -> + approx = VA.State ae am -> + exists valu2, numbering_holds valu2 ge sp rs m' (add_store_result approx n chunk addr args src). Proof. - intros. inversion H0. - unfold add_load. - caseEq (valnum_regs n args). intros n1 vl VRL. - generalize (valnum_regs_holds _ _ _ _ _ _ _ H H3 VRL). intros [valu2 [A [B C]]]. - generalize (wf_valnum_regs _ _ _ _ H VRL). intros [D [E F]]. - apply add_rhs_satisfiable with valu2; auto. - simpl. exists a; split; congruence. + 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_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. + 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. eapply vmatch_ge. apply vincl_ge; eauto. apply H2. ++ eauto with cse. + +- exists valu1; auto. Qed. -(** [add_unknown] returns a numbering that is satisfiable in the - register set after setting the target register to any value. *) - -Lemma add_unknown_satisfiable: - forall n rs dst v m, - wf_numbering n -> - numbering_satisfiable ge sp rs m n -> - numbering_satisfiable ge sp (rs#dst <- v) m (add_unknown n dst). +Lemma kill_loads_after_storebytes_holds: + forall valu ge sp rs m n dst b ofs bytes m' bc approx ae am sz, + numbering_holds valu ge (Vptr sp Int.zero) rs m n -> + rs#dst = Vptr b ofs -> + Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> + genv_match bc ge -> + bc sp = BCstack -> + ematch bc rs ae -> + approx = VA.State ae am -> + length bytes = nat_of_Z sz -> sz >= 0 -> + numbering_holds valu ge (Vptr sp Int.zero) rs m' + (kill_loads_after_storebytes approx n dst sz). Proof. - intros. destruct H0 as [valu A]. - set (valu' := VMap.set n.(num_next) v valu). - assert (numbering_holds valu' ge sp rs m n). - eapply numbering_holds_exten; eauto. - unfold valu'; red; intros. apply VMap.gso. auto with coqlib. - destruct H0 as [B C]. - exists valu'; split; simpl; intros. - eauto. - rewrite PTree.gsspec in H0. rewrite Regmap.gsspec. - destruct (peq r dst). inversion H0. unfold valu'. rewrite VMap.gss; auto. - eauto. + intros. apply kill_equations_hold with m; auto. + intros. unfold filter_after_store in H8; inv H9. +- constructor. rewrite <- H10. apply op_depends_on_memory_correct; auto. +- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate. + econstructor; eauto. rewrite <- H11. + destruct a; simpl in H10; try discriminate. + 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. + erewrite <- regs_valnums_sound by eauto. eauto with va. + unfold aaddr. apply match_aptr_of_aval. rewrite <- H0. apply H4. Qed. -(** Satisfiability of [kill_equations]. *) - -Lemma kill_equations_holds: - forall pred valu n rs m m', - (forall v r, - equation_holds valu ge sp m v r -> pred r = false -> equation_holds valu ge sp m' v r) -> - numbering_holds valu ge sp rs m n -> - numbering_holds valu ge sp rs m' (kill_equations pred n). +Lemma load_memcpy: + forall m b1 ofs1 sz bytes b2 ofs2 m' chunk i v, + Mem.loadbytes m b1 ofs1 sz = Some bytes -> + Mem.storebytes m b2 ofs2 bytes = Some m' -> + Mem.load chunk m b1 i = Some v -> + ofs1 <= i -> i + size_chunk chunk <= ofs1 + sz -> + (align_chunk chunk | ofs2 - ofs1) -> + Mem.load chunk m' b2 (i + (ofs2 - ofs1)) = Some v. Proof. - intros. destruct H0 as [A B]. red; simpl. split; intros. - exploit kill_eqs_in; eauto. intros [C D]. eauto. - auto. + 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. + unfold n3, n2, n1; omega. + intros (bytes1 & bytes23 & LB1 & LB23 & EQ). + clear H. + exploit Mem.loadbytes_split; eauto. + unfold n2; omega. + unfold n3, n2, n1; omega. + intros (bytes2 & bytes3 & LB2 & LB3 & EQ'). + 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. } + subst bytes2'. + exploit Mem.storebytes_split; eauto. intros (m1 & SB1 & SB23). + clear H0. + exploit Mem.storebytes_split; eauto. intros (m2 & SB2 & SB3). + clear SB23. + assert (L1: Z.of_nat (length bytes1) = n1). + { 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 *. + 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. + right; left; omega. } + 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''. + apply Z.divide_add_r; auto. Qed. -(** [kill_loads] preserves satisfiability. Moreover, the resulting numbering - is satisfiable in any concrete memory state. *) - -Lemma kill_loads_satisfiable: - forall n rs m m', - numbering_satisfiable ge sp rs m n -> - numbering_satisfiable ge sp rs m' (kill_loads n). -Proof. - intros. destruct H as [valu A]. exists valu. eapply kill_equations_holds with (m := m); eauto. - intros. destruct r; simpl in *. rewrite <- H. apply op_depends_on_memory_correct; auto. - congruence. +Lemma shift_memcpy_eq_wf: + forall src sz delta e e' next, + shift_memcpy_eq src sz delta e = Some e' -> + wf_equation next e -> + wf_equation next e'. +Proof with (try discriminate). + unfold shift_memcpy_eq; intros. + 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) && + zle (Int.unsigned i + delta) Int.max_unsigned)... + inv H. destruct H0. split. auto. red; simpl; tauto. Qed. -(** [add_store] returns a numbering that is satisfiable in the memory state - after execution of the corresponding [Istore] instruction. *) - -Lemma add_store_satisfiable: - forall n rs chunk addr args src a m m', - wf_numbering n -> - numbering_satisfiable ge sp rs m n -> - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a (rs#src) = Some m' -> - Val.has_type (rs#src) (type_of_chunk_use chunk) -> - numbering_satisfiable ge sp rs m' (add_store n chunk addr args src). -Proof. - intros. unfold add_store. destruct H0 as [valu A]. - destruct (valnum_regs n args) as [n1 vargs] eqn:?. - exploit valnum_regs_holds; eauto. intros [valu' [B [C D]]]. - exploit wf_valnum_regs; eauto. intros [U [V W]]. - set (n2 := kill_equations (filter_after_store chunk addr vargs) n1). - assert (numbering_holds valu' ge sp rs m' n2). - apply kill_equations_holds with (m := m); auto. - intros. destruct r; simpl in *. - rewrite <- H0. apply op_depends_on_memory_correct; auto. - destruct H0 as [a' [P Q]]. - destruct (eq_list_valnum vargs l); simpl in H4; try congruence. subst l. - rewrite negb_false_iff in H4. - exists a'; split; auto. - destruct a; simpl in H2; try congruence. - destruct a'; simpl in Q; try congruence. - simpl. rewrite <- Q. - rewrite C in P. eapply Mem.load_store_other; eauto. - exploit addressing_separated_sound; eauto. intuition congruence. - assert (N2: numbering_satisfiable ge sp rs m' n2). - exists valu'; auto. - set (n3 := add_rhs n2 src (Load chunk addr vargs)). - assert (N3: Val.load_result chunk (rs#src) = rs#src -> numbering_satisfiable ge sp rs m' n3). - intro EQ. unfold n3. apply add_rhs_satisfiable_gen with valu' rs. - apply wf_kill_equations; auto. - red. auto. auto. - red. exists a; split. congruence. - rewrite <- EQ. destruct a; simpl in H2; try discriminate. simpl. - eapply Mem.load_store_same; eauto. - auto. - destruct chunk; auto; apply N3. - simpl in H3. destruct (rs#src); auto || contradiction. - simpl in H3. destruct (rs#src); auto || contradiction. - simpl in H3. destruct (rs#src); auto || contradiction. - simpl in H3. destruct (rs#src); auto || contradiction. +Lemma shift_memcpy_eq_holds: + forall src dst sz e e' m sp bytes m' valu ge, + shift_memcpy_eq src sz (dst - src) e = Some e' -> + Mem.loadbytes m sp src sz = Some bytes -> + Mem.storebytes m sp dst bytes = Some m' -> + equation_holds valu ge (Vptr sp Int.zero) m e -> + 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 rhs as [op vl | chunk addr vl]... + destruct addr... + set (i1 := Int.unsigned i) in *. set (j := i1 + delta) in *. + destruct (zle src i1)... + destruct (zle (i1 + size_chunk chunk) (src + sz))... + destruct (zeq (delta mod align_chunk chunk) 0)... + destruct (zle 0 j)... + destruct (zle j Int.max_unsigned)... + simpl in H; inv H. + assert (LD: forall v, + 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. + 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 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. + econstructor. simpl. rewrite Int.add_zero_l. eauto. apply LD; auto. Qed. -(** Correctness of [reg_valnum]: if it returns a register [r], - that register correctly maps back to the given value number. *) - -Lemma reg_valnum_correct: - forall n v r, wf_numbering n -> reg_valnum n v = Some r -> n.(num_reg)!r = Some v. +Lemma add_memcpy_eqs_charact: + forall e' src sz delta eqs2 eqs1, + In e' (add_memcpy_eqs src sz delta eqs1 eqs2) -> + In e' eqs2 \/ exists e, In e eqs1 /\ shift_memcpy_eq src sz delta e = Some e'. Proof. - unfold reg_valnum; intros. inv H. - destruct ((num_val n)#v) as [| r1 rl] eqn:?; inv H0. - eapply VAL. rewrite Heql. auto with coqlib. + 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 IHeqs1 as [A | [e [A B]]]; auto. right; exists e; auto. + + destruct IHeqs1 as [A | [e [A B]]]; auto. right; exists e; auto. Qed. -(** Correctness of [find_rhs]: if successful and in a - satisfiable numbering, the returned register does contain the - result value of the operation or memory load. *) - -Lemma find_rhs_correct: - forall valu rs m n rh r, - wf_numbering n -> - numbering_holds valu ge sp rs m n -> - find_rhs n rh = Some r -> - rhs_evals_to valu rh m rs#r. +Lemma add_memcpy_holds: + forall m bsrc osrc sz bytes bdst odst m' valu ge sp rs n1 n2 bc approx ae am rsrc rdst, + Mem.loadbytes m bsrc (Int.unsigned osrc) sz = Some bytes -> + Mem.storebytes m bdst (Int.unsigned odst) bytes = Some m' -> + numbering_holds valu ge (Vptr sp Int.zero) rs m n1 -> + numbering_holds valu ge (Vptr sp Int.zero) rs m' n2 -> + genv_match bc ge -> + bc sp = BCstack -> + ematch bc rs ae -> + approx = VA.State ae am -> + rs#rsrc = Vptr bsrc osrc -> + rs#rdst = Vptr bdst odst -> + Ple (num_next n1) (num_next n2) -> + numbering_holds valu ge (Vptr sp Int.zero) rs m' (add_memcpy approx n1 n2 rsrc rdst sz). Proof. - intros until r. intros WF NH. - unfold find_rhs. - caseEq (find_valnum_rhs rh n.(num_eqs)); intros. - exploit find_valnum_rhs_correct; eauto. intros. - exploit reg_valnum_correct; eauto. intros. - inversion NH. - generalize (H3 _ _ H1). rewrite (H4 _ _ H2). - destruct rh; simpl; auto. - discriminate. + intros. unfold add_memcpy. + destruct (aaddr approx rsrc) eqn:ASRC; auto. + destruct (aaddr approx rdst) eqn:ADST; auto. + assert (A: forall r b o i, + rs#r = Vptr b o -> aaddr approx r = Stk i -> b = sp /\ i = o). + { + intros until i. unfold aaddr; subst approx. intros. + specialize (H5 r). rewrite H6 in H5. rewrite match_aptr_of_aval in H5. + rewrite H10 in H5. inv H5. split; auto. eapply bc_stack; eauto. + } + exploit (A rsrc); eauto. intros [P Q]. + exploit (A rdst); eauto. intros [U V]. + subst bsrc ofs bdst ofs0. + constructor; simpl; intros; 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. +- exploit add_memcpy_eqs_charact; eauto. intros [X | (e0 & X & Y)]. + eauto with cse. + eapply shift_memcpy_eq_holds; eauto with cse. Qed. (** Correctness of operator reduction *) @@ -740,29 +721,19 @@ Section REDUCE. Variable A: Type. Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum). Variable V: Type. +Variable ge: genv. +Variable sp: val. Variable rs: regset. Variable m: mem. Variable sem: A -> list val -> option V. Hypothesis f_sound: forall eqs valu op args op' args', - (forall v rhs, eqs v = Some rhs -> equation_holds valu ge sp m v rhs) -> + (forall v rhs, eqs v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v)) -> f eqs op args = Some(op', args') -> sem op' (map valu args') = sem op (map valu args). Variable n: numbering. Variable valu: valnum -> val. Hypothesis n_holds: numbering_holds valu ge sp rs m n. -Hypothesis n_wf: wf_numbering n. - -Lemma regs_valnums_correct: - forall vl rl, regs_valnums n vl = Some rl -> rs##rl = map valu vl. -Proof. - induction vl; simpl; intros. - inv H. auto. - destruct (reg_valnum n a) as [r1|] eqn:?; try discriminate. - destruct (regs_valnums n vl) as [rx|] eqn:?; try discriminate. - inv H. simpl; decEq; auto. - eapply (proj2 n_holds); eauto. eapply reg_valnum_correct; eauto. -Qed. Lemma reduce_rec_sound: forall niter op args op' rl' res, @@ -776,11 +747,14 @@ Proof. as [[op1 args1] | ] eqn:?. assert (sem op1 (map valu args1) = Some res). rewrite <- H0. eapply f_sound; eauto. - simpl; intros. apply (proj1 n_holds). eapply find_valnum_num_correct; eauto. + simpl; intros. + 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:?. inv H. eapply IHniter; eauto. destruct (regs_valnums n args1) as [rl|] eqn:?. - inv H. erewrite regs_valnums_correct; eauto. + inv H. erewrite regs_valnums_sound; eauto. discriminate. discriminate. Qed. @@ -800,8 +774,6 @@ Qed. End REDUCE. -End SATISFIABILITY. - (** 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 @@ -809,26 +781,26 @@ End SATISFIABILITY. satisfiability at [pc']. *) Theorem analysis_correct_1: - forall ge sp rs m f approx pc pc' i, - analyze f = Some approx -> + forall ge sp rs m f vapprox approx pc pc' i, + analyze f vapprox = Some approx -> f.(fn_code)!pc = Some i -> In pc' (successors_instr i) -> - numbering_satisfiable ge sp rs m (transfer f pc approx!!pc) -> - numbering_satisfiable ge sp rs m approx!!pc'. + (exists valu, numbering_holds valu ge sp rs m (transfer f vapprox pc approx!!pc)) -> + (exists valu, numbering_holds valu ge sp rs m approx!!pc'). Proof. intros. - assert (Numbering.ge approx!!pc' (transfer f pc approx!!pc)). + assert (Numbering.ge approx!!pc' (transfer f vapprox pc approx!!pc)). eapply Solver.fixpoint_solution; eauto. - apply H3. auto. + destruct H2 as [valu NH]. exists valu; apply H3. auto. Qed. Theorem analysis_correct_entry: - forall ge sp rs m f approx, - analyze f = Some approx -> - numbering_satisfiable ge sp rs m approx!!(f.(fn_entrypoint)). + forall ge sp rs m f vapprox approx, + analyze f vapprox = Some approx -> + exists valu, numbering_holds valu ge sp rs m approx!!(f.(fn_entrypoint)). Proof. intros. replace (approx!!(f.(fn_entrypoint))) with Solver.L.top. - apply empty_numbering_satisfiable. + exists (fun v => Vundef). apply empty_numbering_holds. symmetry. eapply Solver.fixpoint_entry; eauto. Qed. @@ -841,45 +813,34 @@ Variable tprog : program. Hypothesis TRANSF: transf_program prog = OK tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. +Let rm := romem_for_program prog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_transf_partial transf_fundef prog TRANSF). +Proof (Genv.find_symbol_transf_partial (transf_fundef rm) prog TRANSF). Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof (Genv.find_var_info_transf_partial transf_fundef prog TRANSF). +Proof (Genv.find_var_info_transf_partial (transf_fundef rm) prog TRANSF). Lemma functions_translated: forall (v: val) (f: RTL.fundef), Genv.find_funct ge v = Some f -> - exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial transf_fundef prog TRANSF). + exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef rm f = OK tf. +Proof (Genv.find_funct_transf_partial (transf_fundef rm) prog TRANSF). Lemma funct_ptr_translated: forall (b: block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial transf_fundef prog TRANSF). + exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef rm f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial (transf_fundef rm) prog TRANSF). Lemma sig_preserved: - forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. + forall f tf, transf_fundef rm f = OK tf -> funsig tf = funsig f. Proof. unfold transf_fundef; intros. destruct f; monadInv H; auto. - unfold transf_function in EQ. destruct (type_function f); try discriminate. - destruct (analyze f); try discriminate. inv EQ; auto. -Qed. - -Lemma find_function_translated: - forall ros rs f, - find_function ge ros rs = Some f -> - exists tf, find_function tge ros rs = Some tf /\ transf_fundef f = OK tf. -Proof. - intros until f; destruct ros; simpl. - intro. apply functions_translated; auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i); intro. - apply funct_ptr_translated; auto. - discriminate. + unfold transf_function in EQ. + destruct (analyze f (vanalyze rm f)); try discriminate. inv EQ; auto. Qed. Definition transf_function' (f: function) (approxs: PMap.t numbering) : function := @@ -890,6 +851,50 @@ Definition transf_function' (f: function) (approxs: PMap.t numbering) : function (transf_code approxs f.(fn_code)) f.(fn_entrypoint). +Definition regs_lessdef (rs1 rs2: regset) : Prop := + forall r, Val.lessdef (rs1#r) (rs2#r). + +Lemma regs_lessdef_regs: + forall rs1 rs2, regs_lessdef rs1 rs2 -> + forall rl, Val.lessdef_list rs1##rl rs2##rl. +Proof. + induction rl; constructor; auto. +Qed. + +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. + destruct (peq r0 r); auto. +Qed. + +Lemma init_regs_lessdef: + forall rl vl1 vl2, + Val.lessdef_list vl1 vl2 -> + regs_lessdef (init_regs vl1 rl) (init_regs vl2 rl). +Proof. + induction rl; simpl; intros. + red; intros. rewrite Regmap.gi. auto. + inv H. red; intros. rewrite Regmap.gi. auto. + apply set_reg_lessdef; auto. +Qed. + +Lemma find_function_translated: + forall ros rs fd rs', + find_function ge ros rs = Some fd -> + regs_lessdef rs rs' -> + exists tfd, find_function tge ros rs' = Some tfd /\ transf_fundef rm fd = OK tfd. +Proof. + unfold find_function; intros; destruct ros. +- specialize (H0 r). inv H0. + apply functions_translated; auto. + rewrite <- H2 in H; discriminate. +- rewrite symbols_preserved. destruct (Genv.find_symbol ge i). + apply funct_ptr_translated; auto. + discriminate. +Qed. + (** The proof of semantic preservation is a simulation argument using diagrams of the following form: << @@ -906,45 +911,44 @@ Definition transf_function' (f: function) (approxs: PMap.t numbering) : function the numbering at [pc] (returned by the static analysis) is satisfiable. *) -Inductive match_stackframes: list stackframe -> list stackframe -> typ -> Prop := +Inductive match_stackframes: list stackframe -> list stackframe -> Prop := | match_stackframes_nil: - match_stackframes nil nil Tint + match_stackframes nil nil | match_stackframes_cons: - forall res sp pc rs f approx tyenv s s' ty - (ANALYZE: analyze f = Some approx) - (WTF: wt_function f tyenv) - (WTREGS: wt_regset tyenv rs) - (TYRES: subtype ty (tyenv res) = true) - (SAT: forall v m, numbering_satisfiable ge sp (rs#res <- v) m approx!!pc) - (STACKS: match_stackframes s s' (proj_sig_res (fn_sig f))), + forall res sp pc rs f approx s rs' s' + (ANALYZE: analyze f (vanalyze rm f) = Some approx) + (SAT: forall v m, exists valu, numbering_holds valu ge sp (rs#res <- v) m approx!!pc) + (RLD: regs_lessdef rs rs') + (STACKS: match_stackframes s s'), match_stackframes (Stackframe res f sp pc rs :: s) - (Stackframe res (transf_function' f approx) sp pc rs :: s') - ty. + (Stackframe res (transf_function' f approx) sp pc rs' :: s'). Inductive match_states: state -> state -> Prop := | match_states_intro: - forall s sp pc rs m s' f approx tyenv - (ANALYZE: analyze f = Some approx) - (WTF: wt_function f tyenv) - (WTREGS: wt_regset tyenv rs) - (SAT: numbering_satisfiable ge sp rs m approx!!pc) - (STACKS: match_stackframes s s' (proj_sig_res (fn_sig f))), + forall s sp pc rs m s' rs' m' f approx + (ANALYZE: analyze f (vanalyze rm f) = Some approx) + (SAT: exists valu, numbering_holds valu ge sp rs m approx!!pc) + (RLD: regs_lessdef rs rs') + (MEXT: Mem.extends m m') + (STACKS: match_stackframes s s'), match_states (State s f sp pc rs m) - (State s' (transf_function' f approx) sp pc rs m) + (State s' (transf_function' f approx) sp pc rs' m') | match_states_call: - forall s f tf args m s', - match_stackframes s s' (proj_sig_res (funsig f)) -> - Val.has_type_list args (sig_args (funsig f)) -> - transf_fundef f = OK tf -> + forall s f tf args m s' args' m', + match_stackframes s s' -> + transf_fundef rm f = OK tf -> + Val.lessdef_list args args' -> + Mem.extends m m' -> match_states (Callstate s f args m) - (Callstate s' tf args m) + (Callstate s' tf args' m') | match_states_return: - forall s s' ty v m, - match_stackframes s s' ty -> - Val.has_type v ty -> + forall s s' v v' m m', + match_stackframes s s' -> + Val.lessdef v v' -> + Mem.extends m m' -> match_states (Returnstate s v m) - (Returnstate s' v m). + (Returnstate s' v' m'). Ltac TransfInstr := match goal with @@ -960,196 +964,241 @@ Ltac TransfInstr := Lemma transf_step_correct: forall s1 t s2, step ge s1 t s2 -> - forall s1' (MS: match_states s1 s1'), + forall s1' (MS: match_states s1 s1') (SOUND: sound_state prog s1), exists s2', step tge s1' t s2' /\ match_states s2 s2'. Proof. induction 1; intros; inv MS; try (TransfInstr; intro C). (* Inop *) - exists (State s' (transf_function' f approx) sp pc' rs m); split. - apply exec_Inop; auto. +- econstructor; split. + eapply exec_Inop; eauto. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H; auto. (* Iop *) - exists (State s' (transf_function' f approx) sp pc' (rs#res <- v) m); split. - destruct (is_trivial_op op) eqn:?. - eapply exec_Iop'; eauto. - rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. +- destruct (is_trivial_op op) eqn:TRIV. ++ (* unchanged *) + exploit eval_operation_lessdef. eapply regs_lessdef_regs; eauto. eauto. eauto. + intros [v' [A B]]. + econstructor; split. + 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. + destruct SAT as [valu NH]. eapply add_op_holds; eauto. + apply set_reg_lessdef; auto. ++ (* possibly optimized *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. - assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. destruct SAT as [valu1 NH1]. - exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. - assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + 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 *) - assert (EV: rhs_evals_to ge sp valu2 (Op op vl) m rs#r). eapply find_rhs_correct; eauto. - assert (RES: rs#r = v). red in EV. congruence. - eapply exec_Iop'; eauto. simpl. congruence. - (* possibly simplified *) +* (* replaced by move *) + 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. + eapply analysis_correct_1; eauto. simpl; auto. + 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. intros; eapply combine_op_sound; eauto. - eapply exec_Iop'; eauto. - rewrite <- RES. apply eval_operation_preserved. exact symbols_preserved. - (* state matching *) + exploit eval_operation_lessdef. eapply regs_lessdef_regs; eauto. eauto. eauto. + intros [v' [A B]]. + econstructor; split. + eapply exec_Iop with (v := v'); eauto. + rewrite <- A. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. - eapply wt_exec_Iop; eauto. eapply wt_instr_at; eauto. eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. - eapply add_op_satisfiable; eauto. eapply wf_analyze; eauto. + eapply add_op_holds; eauto. + apply set_reg_lessdef; auto. - (* Iload *) - exists (State s' (transf_function' f approx) sp pc' (rs#dst <- v) m); split. +- (* Iload *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. - assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. destruct SAT as [valu1 NH1]. - exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. - assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + 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 *) - assert (EV: rhs_evals_to ge sp valu2 (Load chunk addr vl) m rs#r). eapply find_rhs_correct; eauto. - assert (RES: rs#r = v). red in EV. destruct EV as [a' [EQ1 EQ2]]. congruence. - eapply exec_Iop'; eauto. simpl. congruence. - (* possibly simplified *) ++ (* replaced by move *) + 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. + eapply analysis_correct_1; eauto. simpl; auto. + 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. - intros; eapply combine_addr_sound; eauto. - assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a). - rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved. + { 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. + intros [v' [X Y]]. + econstructor; split. eapply exec_Iload; eauto. - (* state matching *) econstructor; eauto. - eapply wt_exec_Iload; eauto. eapply wt_instr_at; eauto. eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. - eapply add_load_satisfiable; eauto. eapply wf_analyze; eauto. + eapply add_load_holds; eauto. + apply set_reg_lessdef; auto. - (* Istore *) - exists (State s' (transf_function' f approx) sp pc' rs m'); split. +- (* Istore *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. - assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. destruct SAT as [valu1 NH1]. - exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. - assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + 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. - intros; eapply combine_addr_sound; eauto. - assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a). - rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved. + { 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.storev_extends; eauto. intros [m'' [X Y]]. + econstructor; split. eapply exec_Istore; eauto. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. - eapply add_store_satisfiable; eauto. eapply wf_analyze; eauto. - exploit wt_instr_at; eauto. intros WTI; inv WTI. - eapply Val.has_subtype; eauto. + inv SOUND. + eapply add_store_result_hold; eauto. + eapply kill_loads_after_store_holds; eauto. - (* Icall *) +- (* Icall *) exploit find_function_translated; eauto. intros [tf [FIND' TRANSF']]. econstructor; split. eapply exec_Icall; eauto. apply sig_preserved; auto. - exploit wt_instr_at; eauto. intros WTI; inv WTI. econstructor; eauto. econstructor; eauto. intros. eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. - apply empty_numbering_satisfiable. - eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. + exists (fun _ => Vundef); apply empty_numbering_holds. + apply regs_lessdef_regs; auto. - (* Itailcall *) +- (* Itailcall *) 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. - exploit wt_instr_at; eauto. intros WTI; inv WTI. econstructor; eauto. - replace (proj_sig_res (funsig fd)) with (proj_sig_res (fn_sig f)). auto. - unfold proj_sig_res. rewrite H6; auto. - eapply Val.has_subtype_list; eauto. apply wt_regset_list; auto. + apply regs_lessdef_regs; auto. - (* Ibuiltin *) +- (* Ibuiltin *) + exploit external_call_mem_extends; eauto. + instantiate (1 := rs'##args). apply regs_lessdef_regs; auto. + intros (v' & m1' & P & Q & R & S). econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - eapply wt_exec_Ibuiltin; eauto. eapply wt_instr_at; eauto. eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - assert (CASE1: numbering_satisfiable ge sp (rs#res <- v) m' empty_numbering). - { apply empty_numbering_satisfiable. } - assert (CASE2: m' = m -> numbering_satisfiable ge sp (rs#res <- v) m' (add_unknown approx#pc res)). - { intros. rewrite H1. apply add_unknown_satisfiable. - eapply wf_analyze; eauto. auto. } - assert (CASE3: numbering_satisfiable ge sp (rs#res <- v) m' - (add_unknown (kill_loads approx#pc) res)). - { apply add_unknown_satisfiable. apply wf_kill_equations. eapply wf_analyze; eauto. - eapply kill_loads_satisfiable; eauto. } - destruct ef; auto; apply CASE2; inv H0; auto. - - (* Icond *) +* unfold transfer; rewrite H. + destruct SAT as [valu NH]. + assert (CASE1: exists valu, numbering_holds valu ge sp (rs#res <- v) m' empty_numbering). + { exists valu; apply empty_numbering_holds. } + assert (CASE2: m' = m -> exists valu, numbering_holds valu ge sp (rs#res <- v) m' (set_unknown approx#pc res)). + { intros. rewrite H1. exists valu. apply set_unknown_holds; auto. } + assert (CASE3: exists valu, numbering_holds valu ge sp (rs#res <- v) m' + (set_unknown (kill_all_loads approx#pc) res)). + { exists valu. apply set_unknown_holds. eapply kill_all_loads_hold; eauto. } + destruct ef. + + apply CASE1. + + apply CASE3. + + apply CASE2; inv H0; auto. + + apply CASE3. + + apply CASE2; inv H0; auto. + + apply CASE3; auto. + + apply CASE1. + + apply CASE1. + + destruct args as [ | rdst args]; auto. + destruct args as [ | rsrc args]; auto. + destruct args; auto. + simpl in H0. inv H0. + exists valu. + apply set_unknown_holds. + inv SOUND. eapply add_memcpy_holds; eauto. + eapply kill_loads_after_storebytes_holds; eauto. + eapply Mem.loadbytes_length; eauto. + omega. + simpl. apply Ple_refl. + + apply CASE2; inv H0; auto. + + apply CASE2; inv H0; auto. + + apply CASE1. +* apply set_reg_lessdef; auto. + +- (* Icond *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. - assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. elim SAT; intros valu1 NH1. - exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. - assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + 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. - intros; eapply combine_cond_sound; 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 eval_condition_lessdef; eauto. apply regs_lessdef_regs; auto. econstructor; eauto. destruct b; eapply analysis_correct_1; eauto; simpl; auto; unfold transfer; rewrite H; auto. - (* Ijumptable *) +- (* Ijumptable *) + generalize (RLD arg); rewrite H0; intro LD; inv LD. econstructor; split. eapply exec_Ijumptable; eauto. econstructor; eauto. eapply analysis_correct_1; eauto. simpl. eapply list_nth_z_in; eauto. unfold transfer; rewrite H; auto. - (* Ireturn *) +- (* Ireturn *) + exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]]. econstructor; split. eapply exec_Ireturn; eauto. econstructor; eauto. - exploit wt_instr_at; eauto. intros WTI; inv WTI; simpl. - auto. - unfold proj_sig_res; rewrite H2. eapply Val.has_subtype; eauto. + destruct or; simpl; auto. - (* internal function *) - monadInv H7. unfold transf_function in EQ. - destruct (type_function f) as [tyenv|] eqn:?; try discriminate. - destruct (analyze f) as [approx|] eqn:?; inv EQ. - assert (WTF: wt_function f tyenv). apply type_function_correct; 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. + intros (m'' & A & B). econstructor; split. - eapply exec_function_internal; eauto. + eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. - apply wt_init_regs. inv WTF. eapply Val.has_subtype_list; eauto. - apply analysis_correct_entry; auto. + eapply analysis_correct_entry; eauto. + apply init_regs_lessdef; auto. - (* external function *) - monadInv H7. +- (* external function *) + monadInv H6. + exploit external_call_mem_extends; eauto. + intros (v' & m1' & P & Q & R & S). econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - simpl. eapply external_call_well_typed; eauto. - (* return *) - inv H3. +- (* return *) + inv H2. econstructor; split. eapply exec_return; eauto. econstructor; eauto. - apply wt_regset_assign; auto. eapply Val.has_subtype; eauto. + apply set_reg_lessdef; auto. Qed. Lemma transf_initial_states: @@ -1165,24 +1214,27 @@ Proof. rewrite symbols_preserved. eauto. symmetry. eapply transform_partial_program_main; eauto. rewrite <- H3. apply sig_preserved; auto. - constructor. rewrite H3. constructor. rewrite H3. constructor. auto. + constructor. constructor. auto. auto. apply Mem.extends_refl. Qed. Lemma transf_final_states: forall st1 st2 r, match_states st1 st2 -> final_state st1 r -> final_state st2 r. Proof. - intros. inv H0. inv H. inv H4. constructor. + intros. inv H0. inv H. inv H5. inv H3. constructor. Qed. Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. - eapply forward_simulation_step. - eexact symbols_preserved. - eexact transf_initial_states. - eexact transf_final_states. - exact transf_step_correct. + eapply forward_simulation_step with + (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2). +- eexact symbols_preserved. +- 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 [s2' [A B]]. exists s2'; split. auto. split. eapply sound_step; eauto. auto. Qed. End PRESERVATION. -- cgit