# Module CSEproof

Correctness proof for common subexpression elimination.

Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import Values Memory Builtins Events Globalenvs Smallstep.
Require Import Op Registers RTL.
Require Import ValueDomain ValueAOp ValueAnalysis.
Require Import CSEdomain CombineOp CombineOpproof CSE.

Definition match_prog (prog tprog: RTL.program) :=
match_program (fun cu f tf => transf_fundef (romem_for cu) f = OK tf) eq prog tprog.

Lemma transf_program_match:
forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
intros. eapply match_transform_partial_program_contextual; eauto.
Qed.

# Soundness of operations over value 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 Pos.lt_le_trans with next1; auto.
red; intros. apply Pos.lt_le_trans with next1; auto. apply H1; auto.
Qed.

Extensionality with respect to valuations.

Definition valu_agree (valu1 valu2: valuation) (upto: valnum) :=
forall v, Plt v upto -> valu2 v = valu1 v.

Section EXTEN.

Variable valu1: valuation.
Variable upto: valnum.
Variable valu2: valuation.
Hypothesis AGREE: valu_agree valu1 valu2 upto.
Variable bc: block_classification.
Variable ge: genv.
Variable sp: val.
Variable rs: regset.
Variable m: mem.

Lemma valnums_val_exten:
forall vl,
(forall v, In v vl -> Plt v upto) ->
map valu2 vl = map valu1 vl.
Proof.
intros. apply list_map_exten. intros. symmetry. auto.
Qed.

Lemma In_valnum_rhs_inj v rh1 rh2:
raw_rhs rh1 = raw_rhs rh2 -> In v (valnums_rhs rh1) <-> In v (valnums_rhs rh2).
Proof.
destruct rh1; destruct rh2; simpl; intros X; inv X; reflexivity.
Qed.

Definition rhs_vmatch valu rh: Prop :=
match rh with
| Op _ _ => True
exists a, eval_addressing ge sp addr (map valu vl) = Some a /\ vmatch bc a aa
end.

Lemma rhs_eval_to_exten_va rh1 rh2 v
(REQ: raw_rhs rh1 = raw_rhs rh2)
(RHM: rhs_vmatch valu1 rh2):
rhs_eval_to bc valu1 ge sp m rh1 v ->
(forall v, In v (valnums_rhs rh1) -> Plt v upto) ->
rhs_eval_to bc valu2 ge sp m rh2 v.
Proof.
destruct 1; destruct rh2; simpl in *; inv REQ; simpl; intros.
- constructor. rewrite valnums_val_exten by assumption. auto.
- eapply load_eval_to; eauto. rewrite valnums_val_exten by assumption. auto.
destruct RHM as (a2 & X & VM). rewrite? valnums_val_exten in X by assumption. rewrite X in H; inv H; auto.
(*
- apply load_notrap1_eval_to; auto. rewrite valnums_val_exten by assumption. assumption.
- eapply load_notrap2_eval_to; eauto. rewrite valnums_val_exten by assumption. assumption.
*)

Qed.

Lemma rhs_eval_to_exten rh1 v:
rhs_eval_to bc valu1 ge sp m rh1 v ->
(forall v, In v (valnums_rhs rh1) -> Plt v upto) ->
rhs_eval_to bc valu2 ge sp m rh1 v.
Proof.
intros; eapply rhs_eval_to_exten_va; eauto.
destruct H; simpl; eauto.
Qed.

Lemma equation_holds_exten:
forall e,
equation_holds bc valu1 ge sp m e ->
wf_equation upto e ->
equation_holds bc valu2 ge sp m e.
Proof.
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.

Lemma numbering_holds_exten:
forall n,
numbering_holds bc valu1 ge sp rs m n ->
Ple n.(num_next) upto ->
numbering_holds bc valu2 ge sp rs m n.
Proof.
intros. destruct H. constructor; intros.
- auto.
- apply equation_holds_exten. auto.
eapply wf_equation_incr; eauto with cse.
- rewrite AGREE. eauto. eapply Pos.lt_le_trans; eauto. eapply wf_num_reg; eauto.
Qed.

End EXTEN.

Ltac splitall := repeat (match goal with |- _ /\ _ => split end).

Lemma valnum_reg_holds:
forall bc valu1 ge sp rs m n r n' v,
numbering_holds bc valu1 ge sp rs m n ->
valnum_reg n r = (n', v) ->
exists valu2,
numbering_holds bc 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.
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. extlia.
rewrite PTree.gsspec in H0. destruct (peq r0 r).
inv H0; extlia.
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.
+ extlia.
+ extlia.
Qed.

Lemma valnum_regs_holds:
forall rl bc valu1 ge sp rs m n n' vl,
numbering_holds bc valu1 ge sp rs m n ->
valnum_regs n rl = (n', vl) ->
exists valu2,
numbering_holds bc 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 rl; simpl; intros.
- inv H0. exists valu1; splitall; auto. red; auto. simpl; tauto. extlia.
- 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 bc 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. extlia.
+ simpl; intros. destruct H0; auto. subst v1; extlia.
+ extlia.
Qed.

Lemma find_valnum_rhs_charact:
forall rh v eqs,
find_valnum_rhs rh eqs = Some v -> exists r, raw_rhs r = raw_rhs rh /\ In (Eq v true r) eqs.
Proof.
induction eqs; simpl; intros.
- inv H.
- destruct a. destruct (strict && eq_rhs rh r) eqn:T.
+ InvBooleans. inv H. exists r. intuition.
+ exploit IHeqs; eauto. intros (r0 & P & Q); exists r0; intuition.
Qed.

Lemma find_valnum_rhs'_charact:
forall rh v eqs,
find_valnum_rhs' rh eqs = Some v -> exists r strict, raw_rhs r = raw_rhs rh /\ In (Eq v strict r) eqs.
Proof.
induction eqs; simpl; intros.
- inv H.
- destruct a. destruct (eq_rhs rh r) eqn:T.
+ inv H. exists r; exists strict; intuition.
+ exploit IHeqs; eauto. intros (r0 & s & P & IN). exists r0; exists s; intuition.
Qed.

Lemma find_valnum_num_charact:
forall v r eqs, find_valnum_num v eqs = Some r -> In (Eq v true r) eqs.
Proof.
induction eqs; simpl; intros.
- inv H.
- destruct a. destruct (strict && peq v v0) eqn:T.
+ InvBooleans. inv H; intuition.
+ exploit IHeqs; eauto.
Qed.

Lemma reg_valnum_sound:
forall n v r bc valu ge sp rs m,
reg_valnum n v = Some r ->
numbering_holds bc valu ge sp rs m n ->
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.
rewrite E; auto with coqlib.
Qed.

Lemma regs_valnums_sound:
forall n bc valu ge sp rs m,
numbering_holds bc valu ge sp rs m n ->
forall vl rl,
regs_valnums n vl = Some rl ->
rs##rl = map valu vl.
Proof.
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 find_rhs_sound:
forall n rh r bc valu ge sp rs m,
find_rhs n rh = Some r ->
numbering_holds bc valu ge sp rs m n ->
exists rh0 v, raw_rhs rh0 = raw_rhs rh /\ rhs_eval_to bc valu ge sp m rh0 v /\ Val.lessdef v rs#r.
Proof.
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 (r0 & strict & REQ & IN).
erewrite reg_valnum_sound by eauto.
exploit num_holds_eq; eauto. intros EH. inv EH; eauto.
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.
Proof.
induction l; simpl.
tauto.
destruct (eq x a).
subst a. rewrite IHl. tauto.
simpl. rewrite IHl. intuition congruence.
Qed.

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.
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 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.

Lemma rhs_eval_to_inj:
forall bc valu ge sp m rh1 rh2 v1 v2,
rhs_eval_to bc valu ge sp m rh1 v1 ->
rhs_eval_to bc valu ge sp m rh2 v2 ->
raw_rhs rh1 = raw_rhs rh2 -> v1 = v2.
Proof.
intros. inv H; inv H0; simpl in *; try congruence.
inv H1. rewrite H2 in H; inv H; auto.
Qed.

Lemma find_valnum_rhs_inj rh1 rh2 neqs:
raw_rhs rh1 = raw_rhs rh2 -> find_valnum_rhs rh1 neqs = find_valnum_rhs rh2 neqs.
Proof.
intros H; induction neqs; simpl; auto.
unfold eq_rhs. rewrite H; rewrite IHneqs; auto.
Qed.

forall rh bc valu1 ge sp rs m n rd rs',
numbering_holds bc valu1 ge sp rs m n ->
rhs_eval_to bc valu1 ge sp m rh (rs'#rd) ->
wf_rhs n.(num_next) rh ->
(forall r, r <> rd -> rs'#r = rs#r) ->
forall rh' (REQ: raw_rhs rh' = raw_rhs rh) (RHM: rhs_vmatch bc ge sp valu1 rh'),
exists valu2, numbering_holds bc valu2 ge sp rs' m (add_rhs n rd rh').
Proof.
destruct (find_valnum_rhs rh n.(num_eqs)) as [vres|] eqn:FIND.
- (* A value number exists already *)
exploit find_valnum_rhs_charact; eauto. intros (r & EQ & 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).
{ eapply rhs_eval_to_inj; eauto. }
exists valu1; intuition.
erewrite find_valnum_rhs_inj; eauto.
rewrite FIND; simpl.
constructor; simpl; intros.
+ constructor; simpl; intros.
* eauto with cse.
* rewrite PTree.gsspec in H5. destruct (peq _ rd).
inv H5. auto.
eauto with cse.
* eapply update_reg_charact; eauto with cse.
+ eauto with cse.
+ rewrite PTree.gsspec in H5. destruct (peq _ rd).
congruence.
rewrite H2 by auto. eauto with cse.

- (* 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; intuition.
erewrite find_valnum_rhs_inj; eauto.
erewrite FIND; simpl.
constructor; simpl; intros.
+ constructor; simpl; intros.
* destruct H3. inv H3. simpl; split. extlia.
red; intros. apply Plt_trans_succ. apply H1. erewrite In_valnum_rhs_inj; eauto.
apply wf_equation_incr with (num_next n). eauto with cse. extlia.
* rewrite PTree.gsspec in H3. destruct (peq r rd).
inv H3. extlia.
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_va. 4: eauto. all: 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.

forall bc valu1 ge sp rs m n op (args: list reg) v dst,
numbering_holds bc valu1 ge sp rs m n ->
eval_operation ge sp op rs##args m = Some v ->
exists valu2, numbering_holds bc valu2 ge sp (rs#dst <- v) m (add_op n dst op args).
Proof.
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 (Op op vl)); simpl; eauto.
+ constructor. rewrite Regmap.gss. congruence.
+ intros. apply Regmap.gso; auto.
Qed.

forall ae am bc valu1 ge sp rs m n addr (args: list reg) a chunk v dst app,
numbering_holds bc valu1 ge (Vptr sp Ptrofs.zero) rs m n ->
Mem.loadv chunk m a = Some v ->
app = VA.State ae am ->
ematch bc rs ae ->
bc sp = BCstack ->
genv_match bc ge ->
exists valu2, numbering_holds bc valu2 ge (Vptr sp Ptrofs.zero) (rs#dst <- v) m (add_load app n dst chunk addr args).
Proof.
destruct (valnum_regs n args) as [n1 vl] eqn:VN.
exploit valnum_regs_holds; eauto.
intros (valu2 & A & B & C & D & E).
+ econstructor. rewrite <- B; eauto.
- rewrite Regmap.gss; auto.
rewrite H1; auto.
- eapply eval_static_addressing_sound; eauto with va.
+ intros. apply Regmap.gso; auto.
+ rewrite <- B; eauto.
eexists; split; eauto.
Qed.

Lemma set_unknown_holds:
forall bc valu ge sp rs m n r v,
numbering_holds bc valu ge sp rs m n ->
numbering_holds bc valu ge sp (rs#r <- v) m (set_unknown n r).
Proof.
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.

Lemma set_res_unknown_holds:
forall bc valu ge sp rs m n r v,
numbering_holds bc valu ge sp rs m n ->
numbering_holds bc valu ge sp (regmap_setres r v rs) m (set_res_unknown n r).
Proof.
intros. destruct r; simpl; auto. apply set_unknown_holds; auto.
Qed.

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.
induction eqs; simpl; intros.
- tauto.
- destruct a. destruct (pred r0) eqn:PRED.
tauto.
inv H. inv H0. auto. tauto.
Qed.

Lemma kill_equations_hold:
forall bc bc' valu ge sp rs m n pred m',
numbering_holds bc valu ge sp rs m n ->
(forall r v,
pred r = false ->
rhs_eval_to bc valu ge sp m r v ->
rhs_eval_to bc' valu ge sp m' r v) ->
numbering_holds bc' valu ge sp rs m' (kill_equations pred n).
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].
exploit num_holds_eq; eauto. intro EH; inv EH; econstructor; eauto.
- eauto with cse.
Qed.

Lemma wkill_eqs_charact:
forall pred s l r eqs,
In (Eq l s r) (wkill_eqs pred eqs) ->
pred r = false /\ s = false /\ (exists strict, In (Eq l strict r) eqs).
Proof.
induction eqs; simpl; intros.
- tauto.
- destruct a. destruct (pred r0) eqn:PRED.
+ destruct IHeqs as (OK & ? & (? & IN)); eauto.
+ inv H. inv H0; eauto.
destruct IHeqs as (OK & ? & (? & IN)); eauto.
Qed.

Lemma external_call_readonly_load ef ge args m t res m' v chunk b ofs
(EXTCALL: external_call ef ge args m t res m')
(VALIDB: Mem.valid_block m b)
(RO: forall i:Z, ofs <= i < ofs + (size_chunk chunk) -> ~ Mem.perm m b i Max Writable):
Mem.load chunk m b ofs = Some v.
Proof.
destruct 1 as (_ & ALIGNED).
intros (bytes' & LOADB' & EQv').
Qed.

forall rm (bc bc': block_classification) valu ge sp rs m n m' ef args t res am
(ROM: romatch bc m rm)
(NUM: numbering_holds bc valu ge sp rs m n)
(EXTCALL: external_call ef ge args m t res m')
(MM: mmatch bc m am)
(BCP: forall b, Plt b (Mem.nextblock m) -> bc' b = bc b),
numbering_holds bc' valu ge sp rs m' (kill_all_loads rm n).
Proof.
intros; constructor; simpl; intros; eauto with cse.
- constructor; simpl; intros; eauto with cse.
destruct e; exploit wkill_eqs_charact; eauto. intros (A & B & (s & C)).
exploit num_holds_wf; eauto.
intros; exploit wf_num_eqs; eauto.
- destruct eq. exploit wkill_eqs_charact; eauto. intros (FILT & B & (s & C)).
exploit num_holds_eq; eauto. subst.
intro EH. assert (X: exists v0, rhs_eval_to bc valu ge sp m r v0 /\ Val.lessdef v0 (valu v)).
{ inv EH; eexists; split; eauto. }
destruct X as (v0 & RHS & LESSDEF).
destruct RHS as [op lv v1 EVAL|? ? ? ? ? ? EVAL EQ VM]; simpl in *.
* econstructor; eauto. econstructor; erewrite <- EVAL; apply op_depends_on_memory_correct; auto.
* rewrite negb_false_iff in FILT.
assert (ALT: forall b i p, a = (Vptr b i) ->
pmatch bc b i p ->
is_ro_ptr rm p = true ->
(aa = Ptr p \/ aa = Ifptr p) ->
equation_holds bc' valu ge sp m' (Eq v false (Load chunk addr vl aa))).
+ clear VM FILT; intros b i p EQa PM FILT ALT. subst. simpl in *.
generalize (is_ro_ptr_sound _ _ _ _ _ _ ROM PM FILT). intros RONLY.
exploit pmatch_mmatch_valid; eauto. intros VALIDB.
exploit pmatch_preserv; eauto. intros PM'.
econstructor; eauto. econstructor; eauto.
-- destruct ALT; subst; econstructor; auto.
++ eapply eq_holds_lessdef with (v:=Vundef); econstructor; eauto.
-- destruct ALT; subst; econstructor; auto.
+ inv VM; try (do 3 (econstructor; eauto)); simpl in *; exploit ALT; eauto.
Qed.

forall rm valu sp ge rs m n b ofs chunk v m' bc ap
(ROHYP: romatch bc m rm)
(NUM: numbering_holds bc valu ge sp rs m n)
(STORE: Mem.store chunk m b (Ptrofs.unsigned ofs) v = Some m')
(PM: pmatch bc b ofs ap),
numbering_holds bc valu ge sp rs m'
(kill_equations (filter_after_store rm n ap (size_chunk chunk)) n).
Proof.
intros. eapply kill_equations_hold; eauto.
intros. unfold filter_after_store in H; inv H0.
- constructor. rewrite <- H1. apply op_valid_pointer_eq.
intros; erewrite <- Mem.store_preserv_valid; eauto.
- econstructor; eauto.
destruct a; simpl in *; try congruence.
rewrite negb_false_iff in H.
exploit orb_prop; eauto. clear H; destruct 1 as [H | H].
intros; eapply is_ro_ptr_sound with (p:=(aptr_of_aval aa)); eauto.
exploit match_aptr_of_aval; eauto.
eapply pdisjoint_sound. eauto.
eapply match_aptr_of_aval; eauto.
eauto.
Qed.

forall rm valu ge sp rs m n addr args a chunk v m' bc approx ae am
(ROHYP: romatch bc m rm),
numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m n ->
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 bc valu ge (Vptr sp Ptrofs.zero) rs m'
Proof.
intros.
destruct a; simpl in *; try discriminate.
eapply match_aptr_of_aval; eauto.
Qed.

forall rm valu ge sp rs m n addr b ofs chunk v m' bc approx ae am t
(ROHYP: romatch bc m rm)
(NUM: numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m n)
(EVAL: eval_builtin_arg ge (fun r : positive => rs # r) (Vptr sp Ptrofs.zero) m addr (Vptr b ofs))
(VOL: volatile_store ge chunk m b ofs v t m')
(GE: genv_match bc ge)
(SP: bc sp = BCstack)
(EM: ematch bc rs ae)
(MM: mmatch bc m am)
(APP: approx = VA.State ae am),
numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m'
Proof.
intros.
destruct VOL.
+ (* mem unchanged ! *)
intros. eapply kill_equations_hold; eauto.
subst; simpl.
apply match_aptr_of_aval.
eapply abuiltin_arg_sound; eauto with va.
Qed.

Lemma store_normalized_range_sound:
forall bc chunk v,
vmatch bc v (store_normalized_range chunk) ->
Proof.
intros. unfold Val.load_result; remember Archi.ptr64 as ptr64.
destruct chunk; simpl in *; destruct v; auto.
- inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto.
- inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto.
- inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto.
- inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto.
- destruct ptr64; auto.
- destruct ptr64; auto.
- destruct ptr64; auto.
Qed.

forall valu1 ge sp rs m' n addr args a chunk m src (bc:block_classification) ae approx am
(BCSP: bc sp = BCstack)
(GE: genv_match bc ge),
numbering_holds bc valu1 ge (Vptr sp Ptrofs.zero) rs m' n ->
Mem.storev chunk m a rs#src = Some m' ->
ematch bc rs ae ->
approx = VA.State ae am ->
exists valu2, numbering_holds bc valu2 ge (Vptr sp Ptrofs.zero) rs m' (add_store_result approx n chunk addr args src).
Proof.
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 Pos.lt_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; simpl in *; try congruence. erewrite 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.

Lemma kill_loads_after_storebytes_holds rm valu ge sp rs m n dst b ofs bytes m' bc sz
(ROHYP: romatch bc m rm):
numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m n ->
pmatch bc b ofs dst ->
Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' ->
genv_match bc ge ->
bc sp = BCstack ->
length bytes = Z.to_nat sz -> sz >= 0 ->
numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m'
Proof.
intros H H0 H1 H2 H3 H4 H5. eapply kill_equations_hold; eauto.
intros r v H6 H7. unfold filter_after_store in H6; inv H7.
- constructor. rewrite <- H8. apply op_valid_pointer_eq.
intros; exploit Mem.storebytes_preserv_valid; eauto.
- econstructor; eauto.
destruct a; simpl in *; try congruence.
simpl.
rewrite negb_false_iff in H6.
exploit orb_prop; eauto. clear H6; destruct 1 as [H6 | H6].
eapply is_ro_ptr_sound; eauto.
eapply match_aptr_of_aval; eauto.
rewrite H4. rewrite Z2Nat.id by lia.
eapply pdisjoint_sound. eauto.
apply match_aptr_of_aval; eauto.
auto.
(*
- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate.
eapply load_notrap2_eval_to; eauto. rewrite <- H11.
destruct a; simpl in H10; try discriminate; simpl; trivial.
rewrite negb_false_iff in H8.
rewrite H6. rewrite Z2Nat.id by lia.
eapply pdisjoint_sound. eauto.
erewrite <- regs_valnums_sound by eauto. eauto with va.
auto.
*)

Qed.

Lemma option_equiv A (x y: option A): (forall v, x = Some v <-> y = Some v) -> x=y.
Proof.
intros H; destruct x; destruct y; congruence || (exploit H; eauto; intuition).
Qed.

forall m b1 ofs1 sz bytes b2 ofs2 m' chunk i,
Mem.loadbytes m b1 ofs1 sz = Some bytes ->
Mem.storebytes m b2 ofs2 bytes = Some m' ->
ofs1 <= i -> i + size_chunk chunk <= ofs1 + sz ->
(align_chunk chunk | ofs2 - ofs1) ->
Mem.load chunk m b1 i = Mem.load chunk m' b2 (i + (ofs2 - ofs1)).
Proof.
intros; apply option_equiv. intros v.
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; lia).
unfold n1; lia.
unfold n3, n2, n1; lia.
intros (bytes1 & bytes23 & LB1 & LB23 & EQ).
clear H.
unfold n2; lia.
unfold n3, n2, n1; lia.
intros (bytes2 & bytes3 & LB2 & LB3 & EQ').
subst bytes23; subst bytes.
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 Z2Nat.id. unfold n1; lia. }
assert (L2: Z.of_nat (length bytes2) = n2).
{ erewrite Mem.loadbytes_length by eauto. apply Z2Nat.id. unfold n2; lia. }
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; lia.
right; left; lia. }
replace (ofs1 + n1) with i in LB2 by (unfold n1; lia).
assert (bytes2' = bytes2). { unfold n2 in LB2. congruence. }
subst bytes2'.
exploit Mem.load_valid_access; eauto. intros [P Q].
- replace (i + (ofs2 - ofs1)) with (ofs2 + n1) in * by (unfold n1; lia); auto.
subst.
- replace (i + (ofs2 - ofs1)) with (ofs2 + n1) in * by (unfold n1; lia).
assert (bytes2' = bytes2).
{ unfold n2 in LB''. congruence. }
subst; auto.
- exploit Mem.load_valid_access; eauto. intros [_ Q].
replace (i + (ofs2 - ofs1)) with ((ofs2 - ofs1) + i) in Q by lia.
Qed.

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...
try (rename i into ofs).
destruct (zle src (Ptrofs.unsigned ofs) &&
zle (Ptrofs.unsigned ofs + size_chunk m) (src + sz) &&
zeq (delta mod align_chunk m) 0 && zle 0 (Ptrofs.unsigned ofs + delta) &&
zle (Ptrofs.unsigned ofs + delta) Ptrofs.max_unsigned)...
inv H. destruct H0. split. auto. red; simpl; tauto.
Qed.

Lemma shift_memcpy_eq_holds:
forall (bc:block_classification) src dst sz e e' m sp bytes m' valu ge
(BCSP: bc sp = BCstack),
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 bc valu ge (Vptr sp Ptrofs.zero) m e ->
equation_holds bc valu ge (Vptr sp Ptrofs.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]...
try (rename i into ofs).
set (i1 := Ptrofs.unsigned ofs) 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 Ptrofs.max_unsigned)...
simpl in H; inv H.
assert (LD:
Mem.loadv chunk m (Vptr sp ofs) = Mem.loadv chunk m' (Vptr sp (Ptrofs.repr j))).
{
simpl; intros. rewrite Ptrofs.unsigned_repr by lia.
unfold j, delta. eapply load_memcpy; eauto.
apply Zmod_divide; auto. generalize (align_chunk_pos chunk); lia.
}
inv H2.
+ inv H3. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2].
simpl in E2; rewrite Ptrofs.add_zero_l in E2. subst.
rewrite H8.
erewrite LD; eauto.
repeat constructor; auto.
+ inv H4. exploit eval_addressing_Ainstack_inv; eauto. intros [E1 E2].
simpl in E2; rewrite Ptrofs.add_zero_l in E2. subst.
eapply eq_holds_lessdef; eauto.
erewrite LD; eauto.
repeat constructor; auto.
Qed.

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.
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.

forall m bsrc osrc sz bytes bdst odst m' valu ge sp rs n1 n2 bc asrc adst,
Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz = Some bytes ->
Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes = Some m' ->
numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m n1 ->
numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m' n2 ->
pmatch bc bsrc osrc asrc ->
pmatch bc bdst odst adst ->
bc sp = BCstack ->
Ple (num_next n1) (num_next n2) ->
numbering_holds bc valu ge (Vptr sp Ptrofs.zero) rs m' (add_memcpy n1 n2 asrc adst sz).
Proof.
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.
}
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.
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

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 bc valu op args op' args',
(forall v rhs, eqs v = Some rhs -> rhs_eval_to bc 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 bc: block_classification.
Variable n: numbering.
Variable valu: valnum -> val.
Hypothesis n_holds: numbering_holds bc valu ge sp rs m n.

Lemma reduce_rec_sound:
forall niter op args op' rl' res,
reduce_rec A f n niter op args = Some(op', rl') ->
sem op (map valu args) = Some res ->
sem op' (rs##rl') = Some res.
Proof.
induction niter; simpl; intros.
discriminate.
destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args)
as [[op1 args1] | ] eqn:?.
+ assert (sem op1 (map valu args1) = Some res).
- rewrite <- H0. eapply f_sound; eauto.
simpl; intros.
exploit num_holds_eq; eauto.
eapply find_valnum_num_charact; eauto with cse.
intros EH; inv EH; eauto.
- 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_sound; eauto.
discriminate.
+ discriminate.
Qed.

Lemma reduce_sound:
forall op rl vl op' rl' res,
reduce A f n op rl vl = (op', rl') ->
map valu vl = rs##rl ->
sem op rs##rl = Some res ->
sem op' rs##rl' = Some res.
Proof.
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.
Qed.

End REDUCE.

Section REDUCELD.

Variable A: Type.
Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum).
Variable ge: genv.
Variable sp: val.
Variable rs: regset.
Variable m: mem.
Variable sem: A -> list val -> option val.
Hypothesis f_sound:
forall eqs bc valu op args op' args' r,
(forall v rhs, eqs v = Some rhs -> rhs_eval_to bc valu ge sp m rhs (valu v)) ->
f eqs op args = Some(op', args') ->
sem op (map valu args) = Some r ->
exists r',
sem op' (map valu args') = Some r' /\ Val.lessdef r r'.
Variable bc: block_classification.
Variable n: numbering.
Variable valu: valnum -> val.
Hypothesis n_holds: numbering_holds bc valu ge sp rs m n.

Lemma reduce_rec_lessdef_sound:
forall niter op args op' rl' r,
reduce_rec A f n niter op args = Some(op', rl') ->
sem op (map valu args) = Some r ->
exists r',
sem op' (rs##rl') = Some r' /\ Val.lessdef r r'.
Proof.
induction niter; simpl; intros.
discriminate.
destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args)
as [[op1 args1] | ] eqn:?; try discriminate.
assert (exists r': val, sem op1 (map valu args1) = Some r' /\ Val.lessdef r r').
- exploit f_sound.
+ simpl; intros.
exploit num_holds_eq; eauto.
eapply find_valnum_num_charact; eauto with cse.
eapply H1.
intros EH; inv EH; eauto.
+ eexact Heqo.
+ eexact H0.
+ intros. eauto.
- destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ] eqn:?.
destruct H1. destruct H1.
exploit IHniter. eexact Heqo0. eexact H1. inv H.
intros. destruct H. destruct H. exists x0. split; eauto.
eapply Val.lessdef_trans. eexact H2. eexact H3.
destruct (regs_valnums n args1) as [rl|] eqn:?; try discriminate.
inv H. erewrite regs_valnums_sound; eauto.
Qed.

Lemma reduce_lessdef_sound:
forall op rl vl op' rl' r,
reduce A f n op rl vl = (op', rl') ->
map valu vl = rs##rl ->
sem op rs##rl = Some r ->
exists r', sem op' rs##rl' = Some r' /\ Val.lessdef r r'.
Proof.
unfold reduce; intros.
destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ] eqn:?.
eapply reduce_rec_lessdef_sound; eauto. inv H. eexact Heqo. congruence.
exists r. inv H. auto.
Qed.

End REDUCELD.

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 satisfiability at pc'.

Theorem analysis_correct_1:
forall bc ge sp rs m f rm vapprox approx pc pc' i,
analyze f rm vapprox = Some approx ->
f.(fn_code)!pc = Some i -> In pc' (successors_instr i) ->
(exists valu, numbering_holds bc valu ge sp rs m (transfer f rm vapprox pc approx!!pc)) ->
(exists valu, numbering_holds bc valu ge sp rs m approx!!pc').
Proof.
intros.
assert (Numbering.ge approx!!pc' (transfer f rm vapprox pc approx!!pc)).
eapply Solver.fixpoint_solution; eauto.
destruct H2 as (valu & NH). exists valu; apply H3. auto.
Qed.

Theorem analysis_correct_entry:
forall bc ge sp rs m f rm vapprox approx,
analyze f rm vapprox = Some approx ->
exists valu, numbering_holds bc valu ge sp rs m approx!!(f.(fn_entrypoint)).
Proof.
intros.
replace (approx!!(f.(fn_entrypoint))) with Solver.L.top.
exists (fun v => Vundef). apply empty_numbering_holds.
symmetry. eapply Solver.fixpoint_entry; eauto.
Qed.

# Semantic preservation

Section PRESERVATION.

Variable prog: program.
Variable tprog : program.
Hypothesis TRANSF: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSF).

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_match TRANSF).

Lemma functions_translated:
forall (v: val) (f: RTL.fundef),
Genv.find_funct ge v = Some f ->
exists cu tf, Genv.find_funct tge v = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
Proof (Genv.find_funct_match TRANSF).

Lemma funct_ptr_translated:
forall (b: block) (f: RTL.fundef),
Genv.find_funct_ptr ge b = Some f ->
exists cu tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef (romem_for cu) f = OK tf /\ linkorder cu prog.
Proof (Genv.find_funct_ptr_match TRANSF).

Lemma sig_preserved:
forall rm 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 (analyze f rm (vanalyze rm f)); try discriminate. inv EQ; auto.
Qed.

Definition transf_function' (f: function) (approxs: PMap.t numbering) : function :=
mkfunction
f.(fn_sig)
f.(fn_params)
f.(fn_stacksize)
(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 cu tfd, find_function tge ros rs' = Some tfd
/\ transf_fundef (romem_for cu) 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:
```           st1 --------------- st2
|                   |
t|                   |t
|                   |
v                   v
st1'--------------- st2'```
Left: RTL execution in the original program. Right: RTL execution in the optimized program. Precondition (top) and postcondition (bottom): agreement between the states, including the fact that the numbering at pc (returned by the static analysis) is satisfiable.

Definition analyze (cu: program) (f: function) :=
CSE.analyze f (romem_for cu) (vanalyze (romem_for cu) f).

Inductive match_stackframes: list stackframe -> list stackframe -> Prop :=
| match_stackframes_nil:
match_stackframes nil nil
| match_stackframes_cons:
forall res sp pc rs f s rs' s' cu approx
(ANALYZE: analyze cu f = Some approx)
(SAT: forall v bc m,
exists valu, numbering_holds bc 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').

Inductive match_states: state -> state -> Prop :=
| match_states_intro:
forall bc s sp pc rs m s' rs' m' f cu approx
(ANALYZE: analyze cu f = Some approx)
(SOUND: sound_state_base vrelax cu ge bc (State s f sp pc rs m))
(SAT: exists valu, numbering_holds bc 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')
| match_states_call:
forall bc s f tf args m s' args' m' cu
(SOUND: sound_state_base vrelax cu ge bc (Callstate s f args m))
(STACKS: match_stackframes s s')
(TFD: transf_fundef (romem_for cu) f = OK tf)
(ARGS: Val.lessdef_list args args')
(MEXT: Mem.extends m m'),
match_states (Callstate s f args m)
(Callstate s' tf args' m')
| match_states_return:
forall s s' v v' m m'
(STACK: match_stackframes s s')
(RES: Val.lessdef v v')
(MEXT: Mem.extends m m'),
match_states (Returnstate s v m)
(Returnstate s' v' m').

Ltac TransfInstr :=
match goal with
| 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 option_map; rewrite H1; reflexivity ]
end.

As usual, the proof of simulation is a case analysis over the transition in the source code. We need to prove that the CSE domain remains synchronized with the Value domain (at least on bc). There are two cases in the proof: - NXT_SOUND hypothesis enables to restart from a new ValueAnalysis on context switch. - otherwise, we use ValueAnalyse.sound_step_base to step the ValueAnalysis on the current function.

Lemma transf_step_correct:
forall s1 t s2, step ge s1 t s2 ->
forall s1' (MS: match_states s1 s1') (NXT_SOUND: sound_state vrelax prog s2),
exists s2', step tge s1' t s2' /\ match_states s2 s2'.
Proof.
intros s1 t s2 STEP. generalize STEP.
destruct 1; intros; inv MS; try (TransfInstr; intro C);
(* the tactical below makes ValueAnalysis step, using sound_step_base: this produces a SOUND2 hypothesis (with bc'=bc when possible). *)
try (exploit sound_step_base; eauto; intros (bc' & SOUND2 & EQbc); simpl in EQbc; rewrite H in EQbc; try (exploit EQbc; [ reflexivity | intros; subst; clear EQbc])); clear STEP.

- (* Inop *)
eexists; split.
{ eapply exec_Inop; eauto. }
econstructor; eauto.
eapply analysis_correct_1; eauto. simpl; auto.
unfold transfer; rewrite H; eauto.

- (* Iop *)
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).
* apply set_reg_lessdef; auto.
+ (* possibly optimized *)
destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
destruct SAT as (valu1 & NH1).
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 (rh0 & v' & REQ & EV & LD).
assert (v' = v). { inv EV; simpl in *; try congruence. } subst v'.
econstructor; split.
{ eapply exec_Iop; eauto. simpl; eauto. }
econstructor; eauto.
eapply analysis_correct_1; eauto. simpl; auto.
unfold transfer; rewrite H.
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:?.
exploit (reduce_lessdef_sound operation combine_op ge sp rs m (fun op vl => eval_operation ge sp op vl m)); intros; eauto.
exploit combine_op_sound; eauto.
destruct H1 as (v' & EV' & LD').
exploit (eval_operation_lessdef). eapply regs_lessdef_regs; eauto. eexact MEXT. eexact EV'.
intros [v'' [EV'' LD'']].
econstructor; split.
{ eapply exec_Iop. eexact C. erewrite eval_operation_preserved. eexact EV''.
exact symbols_preserved. }
econstructor; eauto.
eapply analysis_correct_1; eauto. simpl; auto.
unfold transfer; rewrite H.
apply set_reg_lessdef; auto.
eapply (Val.lessdef_trans v v' v''); auto.

destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
destruct SAT as (valu1 & NH1).
exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
destruct trap; inv H0.
+ (* TRAP *)
* (* replaced by move *)
exploit find_rhs_sound; eauto. intros (rh0' & v' & REQ & EV & LD).
assert (v'=v). {
inv EV; simpl in *; try congruence.
inv REQ. rewrite <- EQ in H0. rewrite H0 in EVAL; inv EVAL.
} subst v'.
econstructor; split.
eapply exec_Iop; eauto. simpl; eauto.
inv SOUND; econstructor; eauto.
-- eapply analysis_correct_1; eauto. simpl; auto.
unfold transfer; rewrite H.
-- apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
intros [a' [A B]].
{ rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
intros [v' [X Y]].
econstructor; split.
inv SOUND; econstructor; eauto.
-- eapply analysis_correct_1; eauto. simpl; auto.
unfold transfer; rewrite H.
-- apply set_reg_lessdef; auto.
+ (* NOTRAP1 *)
assert (exists a' : val,
eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a')
as Haa'.
{ apply eval_addressing_lessdef with (vl1 := rs ## args).
apply regs_lessdef_regs; assumption.
assumption. }
destruct Haa' as [a' [Ha'1 Ha'2]].
assert (
exists v' : val,
Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by
destruct Hload' as [v' [Hv'1 Hv'2]].
econstructor. split.
(try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved)).
econstructor; eauto.
-- eapply analysis_correct_1; eauto. simpl; eauto.
unfold transfer. rewrite H.
exists valu1.
apply set_unknown_holds.
assumption.
-- apply set_reg_lessdef; assumption.
+ (* NOTRAP2 *)
assert (exists a' : val,
eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef v a')
as Haa'.
apply eval_addressing_lessdef with (vl1 := rs ## args).
apply regs_lessdef_regs; assumption.
assumption.
destruct Haa' as [a' [Ha'1 Ha'2]].
{
econstructor. split.
try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
econstructor; eauto.
eapply analysis_correct_1; eauto. simpl; eauto.
unfold transfer. rewrite H.
exists valu1.
apply set_unknown_holds.
assumption.
apply set_reg_lessdef; eauto.
}
{
econstructor. split.
try (intros a EVAL';
rewrite eval_addressing_preserved with (ge1 := ge) in EVAL'; [| exact symbols_preserved];
inv Ha'2; rewrite Ha'1 in EVAL'; inv EVAL'; auto).
econstructor; eauto.
eapply analysis_correct_1; eauto. simpl; eauto.
unfold transfer. rewrite H.
exists valu1.
apply set_unknown_holds.
assumption.
apply set_reg_lessdef.
constructor. assumption.
}
* econstructor. split.
rewrite eval_addressing_preserved with (ge1 := ge).
intros a EVAL'. eapply eval_addressing_lessdef_none with (vl1 := rs ## args) in EVAL.
erewrite EVAL in EVAL'. congruence.
apply regs_lessdef_regs; assumption.
exact symbols_preserved.
++ econstructor; eauto.
eapply analysis_correct_1; eauto. simpl; eauto.
unfold transfer. rewrite H.
exists valu1.
apply set_unknown_holds.
assumption.
apply set_reg_lessdef.
constructor. assumption.

- (* Istore *)
destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
destruct SAT as [valu1 NH1].
exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
intros [a' [A B]].
{ rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
exploit Mem.storev_extends; eauto. intros [m'' [X Y]].
econstructor; split.
{ eapply exec_Istore; eauto. }
inv SOUND; econstructor; eauto.
eapply analysis_correct_1; eauto. simpl; auto.
unfold transfer; rewrite H.

- (* Icall *)
exploit find_function_translated; eauto. intros (cu' & tf & FIND' & TRANSF' & LINK').
econstructor; split.
{ eapply exec_Icall; eauto.
eapply sig_preserved; eauto. }
clear SOUND bc' SOUND2 EQbc. inv NXT_SOUND. destruct (H1 _ LINK') as (bc' & SOUND). clear H1.
econstructor; eauto.
-- eapply match_stackframes_cons with (cu := cu); 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 (cu' & tf & FIND' & TRANSF' & LINK').
exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]].
econstructor; split.
{ eapply exec_Itailcall; eauto.
eapply sig_preserved; eauto. }
clear SOUND bc' SOUND2 EQbc. inv NXT_SOUND. destruct (H1 _ LINK') as (bc' & SOUND). clear H1.
econstructor; eauto.
apply regs_lessdef_regs; auto.

- (* Ibuiltin *)
clear EQbc SOUND2 bc'.
inv SOUND.
exploit sound_exec_builtin_aux; eauto.
-- intros (bc' & ae' & am' & TR & EM' & RO' & MM' & GE' & SP' & STP & EQbc & UNCH).
set (sp:=Vptr sp0 Ptrofs.zero).
assert (SOUND2: sound_state_base vrelax cu ge bc' (State s f sp pc' (regmap_setres res vres rs) m')).
{ eapply sound_succ_state; eauto.
* unfold ValueAnalysis.transfer. rewrite H. rewrite TR; simpl. intuition eauto.
* eapply sound_stack_preserved; eauto.
}
clear RO' MM'.
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).
econstructor; split.
eapply exec_Ibuiltin; eauto.
eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
eapply external_call_symbols_preserved; eauto. apply senv_preserved.
econstructor; eauto.
* eapply analysis_correct_1; eauto; simpl; auto.
unfold transfer; rewrite H.
destruct SAT as [valu NH].
assert (CASE1: exists valu, numbering_holds bc' valu ge sp (regmap_setres res vres rs) m' empty_numbering).
{ exists valu; apply empty_numbering_holds. }
assert (CASE2: m' = m -> bc' = bc -> exists valu, numbering_holds bc' valu ge sp (regmap_setres res vres rs) m' (set_res_unknown approx#pc res)).
{ intros. subst. exists valu. apply set_res_unknown_holds; auto. }
(* NB: if needed below, look at H1 for knowing [ef] remaining cases *)
destruct ef; try ((apply CASE1; fail) || (apply CASE2; inv H1; auto; fail)).
+ (* EF_builtin *) destruct (lookup_builtin_function name sg) as [bf|] eqn:LK.
++ (* Some bf *) apply CASE2; auto. simpl in H1. red in H1; rewrite LK in H1; inv H1; auto.
apply EQbc; simpl. rewrite LK; auto.
++ (* None *)
exists valu. apply set_res_unknown_holds.
+ (* EF_vstore *) inv H0; auto. inv H3; auto. inv H4; auto.
simpl in H1. inv H1.
exists valu.
apply set_res_unknown_holds.
exploit EQbc; auto; intros; subst.
+ (* EF_memcpy *) inv H0; auto. inv H3; auto. inv H4; auto.
simpl in H1. inv H1.
exists valu.
apply set_res_unknown_holds.
unfold vanalyze, vrelax in *; rewrite AN.
assert (pmatch bc bsrc osrc (xaaddr_arg (romem_for cu) (VA.State ae am) a0))
assert (pmatch bc bdst odst (xaaddr_arg (romem_for cu) (VA.State ae am) a1))
exploit EQbc; auto; intros; subst.
++ simpl. apply Ple_refl.
* apply set_res_lessdef; auto.

- (* Icond *)
destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
elim SAT; intros valu1 NH1.
exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
destruct (combine_cond' cond vl) eqn:?; auto.
+ (* optimized by pruning a branch *)
econstructor; split.
eapply exec_Inop; eauto.
assert (eval_condition cond (map valu2 vl) m = Some b) by (rewrite <- EQ; auto).
exploit (combine_cond'_sound m valu2 cond vl b b0); eauto.
intros; subst.
econstructor; eauto.
destruct b0; eapply analysis_correct_1; eauto; simpl; auto;
unfold transfer; rewrite H; auto.
+ (* unchanged *)
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. }
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 *)
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 *)
exploit Mem.free_parallel_extends; eauto. intros [m'' [A B]].
econstructor; split.
eapply exec_Ireturn; eauto.
econstructor; eauto.
destruct or; simpl; auto.

- (* internal function *)
monadInv TFD. unfold transf_function in EQ. fold (analyze cu f) in EQ.
destruct (analyze cu f) as [approx|] eqn:Heqo; inv EQ.
exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl.
intros (m'' & A & B).
econstructor; split.
{ eapply exec_function_internal; simpl; eauto. }
clear A; simpl.
inv SOUND.
exploit (allocate_stack ge); eauto.
intros (bc' & A1 & B1 & C1 & D1 & E1 & F1 & G1).
exploit (analyze_entrypoint vrelax (romem_for cu) f args m' bc'); eauto.
intros (ae & am & AN & EM & MM').
econstructor; eauto.
-- (* sound *)
econstructor; eauto.
erewrite Mem.alloc_result; eauto.
apply sound_stack_exten with bc; auto.
apply sound_stack_inv with m; auto.
intros; apply F1. erewrite Mem.alloc_result by eauto. auto.
-- eapply analysis_correct_entry; eauto.
-- apply init_regs_lessdef; auto.

- (* external function *)
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. apply senv_preserved.
econstructor; eauto.

- (* return *)
inv STACK.
econstructor; split.
{ eapply exec_return; eauto. }
inv NXT_SOUND. destruct (H _ LINK) as (bc & SOUND). clear H.
econstructor; eauto.
apply set_reg_lessdef; auto.
Qed.

Lemma transf_initial_states:
forall st1, initial_state prog st1 ->
exists st2, initial_state tprog st2 /\ match_states st1 st2 .
Proof.
intros. inversion H. exploit sound_initial; eauto. intros SOUND.
exploit funct_ptr_translated; eauto. intros (cu & tf & A & B & C).
exists (Callstate nil tf nil m0); split.
- econstructor; eauto.
eapply (Genv.init_mem_match TRANSF); eauto.
replace (prog_main tprog) with (prog_main prog).
rewrite symbols_preserved. eauto.
symmetry. eapply match_program_main; eauto.
rewrite <- H3. eapply sig_preserved; eauto.
- subst. inv SOUND. exploit H4; eauto. clear H4.
intros SOUND; inv SOUND.
econstructor; eauto.
+ econstructor; eauto.
+ 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 st1 st2 r M X; destruct M; inv X. inv RES. inv STACK. constructor.
Qed.

Theorem transf_program_correct:
forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
eapply forward_simulation_step with
(match_states := fun s1 s2 => sound_state vrelax prog s1 /\ match_states s1 s2).
- apply senv_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 sound_step; eauto. eapply H.
intros; exploit transf_step_correct; eauto.
intros [s2' [A B]]. exists s2'; intuition; auto.
Qed.

End PRESERVATION.