path: root/backend/CSE2proof.v

(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*                                                             *)
(*  Copyright VERIMAG. All rights reserved.                    *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

(*
Replace available expressions by the register containing their value.

Proofs.

David Monniaux, CNRS, VERIMAG
 *)

Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps.

Require Import Globalenvs Values.
Require Import Linking Values Memory Globalenvs Events Smallstep.
Require Import Registers Op RTL.
Require Import CSE2 CSE2deps CSE2depsproof.
Require Import Lia.

Lemma args_unaffected:
  forall rs : regset,
  forall dst : reg,
  forall v,
  forall args : list reg,
    existsb (fun y : reg => peq dst y) args = false ->
    (rs # dst <- v ## args) = (rs ## args).
Proof.
  induction args; simpl; trivial.
  destruct (peq dst a) as [EQ | NEQ]; simpl.
  { discriminate.
  }
  intro EXIST.
  f_equal.
  {
    apply Regmap.gso.
    congruence.
  }
  apply IHargs.
  assumption.
Qed.

Section SOUNDNESS.
  Variable F V : Type.
  Variable genv: Genv.t F V.
  Variable sp : val.

Section SAME_MEMORY.
  Variable m : mem.

Definition sem_sym_val sym rs (v : option val) : Prop :=
  match sym with
  | SMove src => v = Some (rs # src)
  | SOp op args =>
    v = (eval_operation genv sp op (rs ## args) m)
  | SLoad chunk addr args =>
    match eval_addressing genv sp addr rs##args with
    | Some a => match Mem.loadv chunk m a with
                | Some dat => v = Some dat
                | None => v = None \/ v = Some Vundef
                end
    | None   => v = None \/ v = Some Vundef
    end
  end.
    
Definition sem_reg (rel : RELATION.t) (x : reg) (rs : regset) (v : val) : Prop :=
  match rel ! x with
  | None => True
  | Some sym => sem_sym_val sym rs (Some (rs # x)) 
  end.

Definition sem_rel (rel : RELATION.t) (rs : regset) :=
  forall x : reg, (sem_reg rel x rs (rs # x)).

Definition sem_rel_b (relb : RB.t) (rs : regset) :=
  match relb with
  | Some rel => sem_rel rel rs
  | None => False
  end.

Definition fmap_sem (fmap : option (PMap.t RB.t))
  (pc : node) (rs : regset) :=
  match fmap with
  | None => True
  | Some m => sem_rel_b (PMap.get pc m) rs
  end.

Lemma subst_arg_ok:
  forall f,
  forall pc,
  forall rs,
  forall arg,
    fmap_sem (forward_map f) pc rs ->
    rs # (subst_arg (forward_map f) pc arg) = rs # arg.
Proof.
  intros until arg.
  intro SEM.
  unfold fmap_sem in SEM.
  destruct (forward_map f) as [map |]in *; trivial.
  simpl.
  unfold sem_rel_b, sem_rel, sem_reg in *.
  destruct (map # pc).
  2: contradiction.
  pose proof (SEM arg) as SEMarg.
  simpl. unfold forward_move.
  unfold sem_sym_val in *.
  destruct (t ! arg); trivial.
  destruct s; congruence.
Qed.

Lemma subst_args_ok:
  forall f,
  forall pc,
  forall rs,
  fmap_sem (forward_map f) pc rs ->
  forall args,
    rs ## (subst_args (forward_map f) pc args) = rs ## args.
Proof.
  induction args; trivial.
  simpl.
  f_equal.
  apply subst_arg_ok; assumption.
  assumption.
Qed.

Lemma kill_reg_sound :
  forall rel : RELATION.t,
  forall dst : reg,
  forall rs,
  forall v,
    sem_rel rel rs ->
    sem_rel (kill_reg dst rel) (rs # dst <- v).
Proof.
  unfold sem_rel, kill_reg, sem_reg, sem_sym_val.
  intros until v.
  intros REL x.
  rewrite PTree.gfilter1.
  destruct (Pos.eq_dec dst x).
  {
    subst x.
    rewrite PTree.grs.
    trivial.
  }
  rewrite PTree.gro by congruence.
  rewrite Regmap.gso by congruence.
  destruct (rel ! x) as [relx | ] eqn:RELx; trivial.
  unfold kill_sym_val.
  pose proof (REL x) as RELinstx.
  rewrite RELx in RELinstx.
  destruct relx eqn:SYMVAL.
  {
    destruct (peq dst src); simpl.
    { reflexivity. }
    rewrite Regmap.gso by congruence.
    assumption.
  }
  { destruct existsb eqn:EXISTS; simpl.
    { reflexivity. }
    rewrite args_unaffected by exact EXISTS.
    assumption.
  }
  { destruct existsb eqn:EXISTS; simpl.
    { reflexivity. }
    rewrite args_unaffected by exact EXISTS.
    assumption.
  }
Qed.

Lemma write_same:
  forall rs : regset,
  forall src dst : reg,
    (rs # dst <- (rs # src)) # src = rs # src.
Proof.
  intros.
  destruct (peq src dst).
  {
    subst dst.
    apply Regmap.gss.
  }
  rewrite Regmap.gso by congruence.
  reflexivity.
Qed.

Lemma move_sound :
  forall rel : RELATION.t,
  forall src dst : reg,
  forall rs,
    sem_rel rel rs ->
    sem_rel (move src dst rel) (rs # dst <- (rs # src)).
Proof.
  intros until rs. intros REL x.
  pose proof (kill_reg_sound rel dst rs (rs # src) REL x) as KILL.
  pose proof (REL src) as RELsrc.
  unfold move.
  destruct (peq x dst).
  {
    subst x.
    unfold sem_reg.
    rewrite PTree.gss.
    rewrite Regmap.gss.
    unfold sem_reg in *.
    simpl.
    unfold forward_move.
    destruct (rel ! src) as [ sv |]; simpl.
    destruct sv eqn:SV; simpl in *.
    {
      destruct (peq dst src0).
      {
        subst src0.
        rewrite Regmap.gss.
        reflexivity.
      }
      rewrite Regmap.gso by congruence.
      assumption.
    }
    all: f_equal; symmetry; apply write_same.
  }
  rewrite Regmap.gso by congruence.
  unfold sem_reg.
  rewrite PTree.gso by congruence.
  rewrite Regmap.gso in KILL by congruence.
  exact KILL.
Qed.

Lemma move_cases_neq:
  forall dst rel a,
    a <> dst ->
    (forward_move (kill_reg dst rel) a) <> dst.
Proof.
  intros until a. intro NEQ.
  unfold kill_reg, forward_move.
  rewrite PTree.gfilter1.
  rewrite PTree.gro by congruence.
  destruct (rel ! a); simpl.
  2: congruence.
  destruct s.
  {
    unfold kill_sym_val.
    destruct peq; simpl; congruence.
  }
  all: simpl;
    destruct negb; simpl; congruence.
Qed.

Lemma args_replace_dst :
  forall rel,
  forall args : list reg,
  forall dst : reg,
  forall rs : regset,
  forall v,
    (sem_rel rel rs) ->
    not (In dst args) ->
    (rs # dst <- v)
    ## (map
          (forward_move (kill_reg dst rel)) args) = rs ## args.
Proof.
  induction args; simpl.
  1: reflexivity.
  intros until v.
  intros REL NOT_IN.
  rewrite IHargs by auto.
  f_equal.
  pose proof (REL a) as RELa.
  rewrite Regmap.gso by (apply move_cases_neq; auto).
  unfold kill_reg.
  unfold sem_reg in RELa.
  unfold forward_move.
  rewrite PTree.gfilter1.
  rewrite PTree.gro by auto.
  destruct (rel ! a); simpl; trivial.
  destruct s; simpl in *; destruct negb; simpl; congruence.
Qed.

Lemma oper2_sound :
  forall rel : RELATION.t,
  forall op : operation,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall v,
    sem_rel rel rs ->
    not (In dst args) ->
    eval_operation genv sp op (rs ## args) m = Some v ->
    sem_rel (oper2 op dst args rel) (rs # dst <- v).
Proof.
  intros until v.
  intros REL NOT_IN EVAL x.
  pose proof (kill_reg_sound rel dst rs v REL x) as KILL.
  unfold oper2.
  destruct (peq x dst).
  {
    subst x.
    unfold sem_reg.
    rewrite PTree.gss.
    rewrite Regmap.gss.
    simpl.
    rewrite args_replace_dst by auto.
    symmetry.
    assumption.
  }
  rewrite Regmap.gso by congruence.
  unfold sem_reg.
  rewrite PTree.gso by congruence.
  rewrite Regmap.gso in KILL by congruence.
  exact KILL.
Qed.

Lemma oper1_sound :
  forall rel : RELATION.t,
  forall op : operation,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall v,
    sem_rel rel rs ->
    eval_operation genv sp op (rs ## args) m = Some v ->
    sem_rel (oper1 op dst args rel) (rs # dst <- v).
Proof.
  intros until v.
  intros REL EVAL.
  unfold oper1.
  destruct in_dec.
  {
    apply kill_reg_sound; auto. 
  }
  apply oper2_sound; auto.
Qed.

Lemma find_op_sound :
  forall rel : RELATION.t,
  forall op : operation,
  forall src : reg,
  forall args: list reg,
  forall rs : regset,
    sem_rel rel rs ->
    find_op rel op args = Some src ->
    (eval_operation genv sp op (rs ## args) m) = Some (rs # src).
Proof.
  intros until rs.
  unfold find_op.
  rewrite PTree.fold_spec.
  intro REL.
  assert (
     forall start,
             match start with
             | None => True
             | Some src => eval_operation genv sp op rs ## args m = Some rs # src
             end -> fold_left
    (fun (a : option reg) (p : positive * sym_val) =>
     find_op_fold op args a (fst p) (snd p)) (PTree.elements rel) start =
                    Some src ->
             eval_operation genv sp op rs ## args m = Some rs # src) as REC.
  {
    unfold sem_rel, sem_reg in REL.
    generalize (PTree.elements_complete rel).
    generalize (PTree.elements rel).
    induction l; simpl.
    {
      intros.
      subst start.
      assumption.
    }
    destruct a as [r sv]; simpl.
    intros COMPLETE start GEN.
    apply IHl.
    {
      intros.
      apply COMPLETE.
      right.
      assumption.
    }
    unfold find_op_fold.
    destruct start.
    assumption.
    destruct sv; trivial.
    destruct eq_operation; trivial.
    subst op0.
    destruct eq_args; trivial.
    subst args0.
    simpl.
    assert ((rel ! r) = Some (SOp op args)) as RELatr.
    {
      apply COMPLETE.
      left.
      reflexivity.
    }
    pose proof (REL r) as RELr.
    rewrite RELatr in RELr.
    simpl in RELr.
    symmetry.
    assumption.
  }
  apply REC; auto.
Qed.


Lemma find_load_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall src : reg,
  forall args: list reg,
  forall rs : regset,
    sem_rel rel rs ->
    find_load rel chunk addr args = Some src ->
    match eval_addressing genv sp addr rs##args with
    | Some a => match Mem.loadv chunk m a with
                | Some dat => rs#src = dat
                | None => rs#src = Vundef
                end
    | None   => rs#src = Vundef
    end.
Proof.
  intros until rs.
  unfold find_load.
  rewrite PTree.fold_spec.
  intro REL.
  assert (
     forall start,
             match start with
             | None => True
             | Some src =>
               match eval_addressing genv sp addr rs##args with
               | Some a => match Mem.loadv chunk m a with
                           | Some dat => rs#src = dat
                           | None => rs#src = Vundef
                           end
               | None   => rs#src = Vundef
               end
             end ->
    fold_left
    (fun (a : option reg) (p : positive * sym_val) =>
     find_load_fold chunk addr args a (fst p) (snd p)) (PTree.elements rel) start =
    Some src ->
    match eval_addressing genv sp addr rs##args with
               | Some a => match Mem.loadv chunk m a with
                           | Some dat => rs#src = dat
                           | None => rs#src = Vundef
                           end
               | None   => rs#src = Vundef
               end) as REC.
  
  {
    unfold sem_rel, sem_reg in REL.
    generalize (PTree.elements_complete rel).
    generalize (PTree.elements rel).
    induction l; simpl.
    {
      intros.
      subst start.
      assumption.
    }
    destruct a as [r sv]; simpl.
    intros COMPLETE start GEN.
    apply IHl.
    {
      intros.
      apply COMPLETE.
      right.
      assumption.
    }
    unfold find_load_fold.
    destruct start.
    assumption.
    destruct sv; trivial.
    destruct chunk_eq; trivial.
    subst chunk0.
    destruct eq_addressing; trivial.
    subst addr0.
    destruct eq_args; trivial.
    subst args0.
    simpl.
    assert ((rel ! r) = Some (SLoad chunk addr args)) as RELatr.
    {
      apply COMPLETE.
      left.
      reflexivity.
    }
    pose proof (REL r) as RELr.
    rewrite RELatr in RELr.
    simpl in RELr.
    destruct eval_addressing.
    { destruct Mem.loadv.
      congruence.
      destruct RELr; congruence.
    }
    destruct RELr; congruence.
  }
  apply REC; auto.
Qed.


Lemma find_load_sound' :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall src : reg,
  forall args: list reg,
  forall rs : regset,
  forall a,
  forall v,
    sem_rel rel rs ->
    find_load rel chunk addr args = Some src ->
    eval_addressing genv sp addr rs##args = Some a ->
    Mem.loadv chunk m a = Some v ->
    v = rs # src.
Proof.
  intros until v. intros REL FINDLOAD ADDR LOAD.
  pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z.
  destruct eval_addressing in *.
  {
    replace a with v0 in * by congruence.
    destruct Mem.loadv in * ; congruence.
  }
  discriminate.
Qed.

Lemma find_load_notrap1_sound' :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall src : reg,
  forall args: list reg,
  forall rs : regset,
    sem_rel rel rs ->
    find_load rel chunk addr args = Some src ->
    eval_addressing genv sp addr rs##args = None ->
    rs # src = Vundef.
Proof.
  intros until rs. intros REL FINDLOAD ADDR.
  pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z.
  rewrite ADDR in Z.
  assumption.
Qed.

Lemma find_load_notrap2_sound' :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall src : reg,
  forall args: list reg,
  forall rs : regset,
  forall a,
    sem_rel rel rs ->
    find_load rel chunk addr args = Some src ->
    eval_addressing genv sp addr rs##args = Some a ->
    Mem.loadv chunk m a = None ->
    rs # src = Vundef.
Proof.
  intros until a. intros REL FINDLOAD ADDR LOAD.
  pose proof (find_load_sound rel chunk addr src args rs REL FINDLOAD) as Z.
  rewrite ADDR in Z.
  destruct Mem.loadv.
  discriminate.
  assumption.
Qed.

Lemma forward_move_map:
  forall rel args rs,
    sem_rel rel rs ->
    rs ## (map (forward_move rel) args) = rs ## args.
Proof.
  induction args; simpl; trivial.
  intros rs REL.
  f_equal.
  2: (apply IHargs; assumption).
  unfold forward_move, sem_rel, sem_reg, sem_sym_val in *.
  pose proof (REL a) as RELa.
  destruct (rel ! a); trivial.
  destruct s; congruence.
Qed.


Lemma forward_move_rs:
  forall rel arg rs,
    sem_rel rel rs ->
    rs # (forward_move rel arg) = rs # arg.
Proof.
  unfold forward_move, sem_rel, sem_reg, sem_sym_val in *.
  intros until rs.
  intro REL.
  pose proof (REL arg) as RELarg.
  destruct (rel ! arg); trivial.
  destruct s; congruence.
Qed.

Lemma oper_sound :
  forall rel : RELATION.t,
  forall op : operation,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall v,
    sem_rel rel rs ->
    eval_operation genv sp op (rs ## args) m = Some v ->
    sem_rel (oper op dst args rel) (rs # dst <- v).
Proof.
  intros until v.
  intros REL EVAL.
  unfold oper.
  destruct find_op eqn:FIND.
  {
    assert (eval_operation genv sp op rs ## (map (forward_move rel) args) m = Some rs # r) as FIND_OP.
    {
      apply (find_op_sound rel); trivial.
    }
    rewrite forward_move_map in FIND_OP by assumption.
    replace v with (rs # r) by congruence.
    apply move_sound; auto.
  }
  apply oper1_sound; trivial.
Qed.

Lemma gen_oper_sound :
  forall rel : RELATION.t,
  forall op : operation,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall v,
    sem_rel rel rs ->
    eval_operation genv sp op (rs ## args) m = Some v ->
    sem_rel (gen_oper op dst args rel) (rs # dst <- v).
Proof.
  intros until v.
  intros REL EVAL.
  unfold gen_oper.
  destruct op.
  { destruct args as [ | h0 t0].
    apply oper_sound; auto.
    destruct t0.
    {
      simpl in *.
      replace v with (rs # h0) by congruence.
      apply move_sound; auto.
    }
    apply oper_sound; auto.
  }
  all: apply oper_sound; auto.
Qed.


Lemma load2_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall a,
  forall v,
    sem_rel rel rs ->
    not (In dst args) ->
    eval_addressing genv sp addr (rs ## args) = Some a ->
    Mem.loadv chunk m a = Some v ->
    sem_rel (load2 chunk addr dst args rel) (rs # dst <- v).
Proof.
  intros until v.
  intros REL NOT_IN ADDR LOAD x.
  pose proof (kill_reg_sound rel dst rs v REL x) as KILL.
  unfold load2.
  destruct (peq x dst).
  {
    subst x.
    unfold sem_reg.
    rewrite PTree.gss.
    rewrite Regmap.gss.
    simpl.
    rewrite args_replace_dst by auto.
    destruct eval_addressing.
    {
      replace a with v0 in * by congruence.
      destruct Mem.loadv; congruence.
    }
    discriminate.
  }
  rewrite Regmap.gso by congruence.
  unfold sem_reg.
  rewrite PTree.gso by congruence.
  rewrite Regmap.gso in KILL by congruence.
  exact KILL.
Qed.

Lemma load2_notrap1_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
    sem_rel rel rs ->
    not (In dst args) ->
    eval_addressing genv sp addr (rs ## args) = None ->
    sem_rel (load2 chunk addr dst args rel) (rs # dst <- Vundef).
Proof.
  intros until rs.
  intros REL NOT_IN ADDR x.
  pose proof (kill_reg_sound rel dst rs Vundef REL x) as KILL.
  unfold load2.
  destruct (peq x dst).
  {
    subst x.
    unfold sem_reg.
    rewrite PTree.gss.
    rewrite Regmap.gss.
    simpl.
    rewrite args_replace_dst by auto.
    rewrite ADDR.
    right.
    trivial.
  }
  rewrite Regmap.gso by congruence.
  unfold sem_reg.
  rewrite PTree.gso by congruence.
  rewrite Regmap.gso in KILL by congruence.
  exact KILL.
Qed.

Lemma load2_notrap2_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall a,
    sem_rel rel rs ->
    not (In dst args) ->
    eval_addressing genv sp addr (rs ## args) = Some a ->
    Mem.loadv chunk m a = None ->
    sem_rel (load2 chunk addr dst args rel) (rs # dst <- Vundef).
Proof.
  intros until a.
  intros REL NOT_IN ADDR LOAD x.
  pose proof (kill_reg_sound rel dst rs Vundef REL x) as KILL.
  unfold load2.
  destruct (peq x dst).
  {
    subst x.
    unfold sem_reg.
    rewrite PTree.gss.
    rewrite Regmap.gss.
    simpl.
    rewrite args_replace_dst by auto.
    rewrite ADDR.
    rewrite LOAD.
    right; trivial.
  }
  rewrite Regmap.gso by congruence.
  unfold sem_reg.
  rewrite PTree.gso by congruence.
  rewrite Regmap.gso in KILL by congruence.
  exact KILL.
Qed.

Lemma load1_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall a,
  forall v,
    sem_rel rel rs ->
    eval_addressing genv sp addr (rs ## args) = Some a ->
    Mem.loadv chunk m a = Some v ->
    sem_rel (load1 chunk addr dst args rel) (rs # dst <- v).
Proof.
  intros until v.
  intros REL ADDR LOAD.
  unfold load1.
  destruct in_dec.
  {
    apply kill_reg_sound; auto. 
  }
  apply load2_sound with (a := a); auto.
Qed.

Lemma load1_notrap1_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
    sem_rel rel rs ->
    eval_addressing genv sp addr (rs ## args) = None ->
    sem_rel (load1 chunk addr dst args rel) (rs # dst <- Vundef).
Proof.
  intros until rs.
  intros REL ADDR LOAD.
  unfold load1.
  destruct in_dec.
  {
    apply kill_reg_sound; auto. 
  }
  apply load2_notrap1_sound; auto.
Qed.

Lemma load1_notrap2_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall a,
    sem_rel rel rs ->
    eval_addressing genv sp addr (rs ## args) = Some a ->
    Mem.loadv chunk m a = None ->
    sem_rel (load1 chunk addr dst args rel) (rs # dst <- Vundef).
Proof.
  intros until a.
  intros REL ADDR LOAD.
  unfold load1.
  destruct in_dec.
  {
    apply kill_reg_sound; auto. 
  }
  apply load2_notrap2_sound with (a := a); auto.
Qed.

Lemma load_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall a,
  forall v,
    sem_rel rel rs ->
    eval_addressing genv sp addr (rs ## args) = Some a ->
    Mem.loadv chunk m a = Some v ->
    sem_rel (load chunk addr dst args rel) (rs # dst <- v).
Proof.
  intros until v.
  intros REL ADDR LOAD.
  unfold load.
  destruct find_load as [src | ] eqn:FIND.
  {
    assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with
    | Some a => match Mem.loadv chunk m a with
                | Some dat => rs#src = dat
                | None => rs#src = Vundef
                end
    | None   => rs#src = Vundef
    end) as FIND_LOAD.
    {
      apply (find_load_sound rel); trivial.
    }
    rewrite forward_move_map in FIND_LOAD by assumption.
    destruct eval_addressing in *.
    2: discriminate.
    replace v0 with a in * by congruence.
    destruct Mem.loadv in *.
    2: discriminate.
    replace v with (rs # src) by congruence.
    apply move_sound; auto.
  }
  apply load1_sound with (a := a); trivial.
Qed.

Lemma load_notrap1_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
    sem_rel rel rs ->
    eval_addressing genv sp addr (rs ## args) = None ->
    sem_rel (load chunk addr dst args rel) (rs # dst <- Vundef).
Proof.
  intros until rs.
  intros REL ADDR.
  unfold load.
  destruct find_load as [src | ] eqn:FIND.
  {
    assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with
    | Some a => match Mem.loadv chunk m a with
                | Some dat => rs#src = dat
                | None => rs#src = Vundef
                end
    | None   => rs#src = Vundef
    end) as FIND_LOAD.
    {
      apply (find_load_sound rel); trivial.
    }
    rewrite forward_move_map in FIND_LOAD by assumption.
    destruct eval_addressing in *.
    discriminate.
    rewrite <- FIND_LOAD.
    apply move_sound; auto.
  }
  apply load1_notrap1_sound; trivial.
Qed.

Lemma load_notrap2_sound :
  forall rel : RELATION.t,
  forall chunk : memory_chunk,
  forall addr : addressing,
  forall dst : reg,
  forall args: list reg,
  forall rs : regset,
  forall a,
    sem_rel rel rs ->
    eval_addressing genv sp addr (rs ## args) = Some a ->
    Mem.loadv chunk m a = None ->
    sem_rel (load chunk addr dst args rel) (rs # dst <- Vundef).
Proof.
  intros until a.
  intros REL ADDR.
  unfold load.
  destruct find_load as [src | ] eqn:FIND.
  {
    assert (match eval_addressing genv sp addr rs## (map (forward_move rel) args) with
    | Some a => match Mem.loadv chunk m a with
                | Some dat => rs#src = dat
                | None => rs#src = Vundef
                end
    | None   => rs#src = Vundef
    end) as FIND_LOAD.
    {
      apply (find_load_sound rel); trivial.
    }
    rewrite forward_move_map in FIND_LOAD by assumption.
    rewrite ADDR in FIND_LOAD.
    destruct Mem.loadv; intro.
    discriminate.
    rewrite <- FIND_LOAD.
    apply move_sound; auto.
  }
  apply load1_notrap2_sound; trivial.
Qed.

Lemma kill_reg_weaken:
  forall res mpc rs,
    sem_rel mpc rs ->
    sem_rel (kill_reg res mpc) rs.
Proof.
  intros until rs.
  intros REL x.
  pose proof (REL x) as RELx.
  unfold kill_reg, sem_reg in *.
  rewrite PTree.gfilter1.
  destruct (peq res x).
  { subst x.
    rewrite PTree.grs.
    reflexivity.
  }
  rewrite PTree.gro by congruence.
  destruct (mpc ! x) as [sv | ]; trivial.
  destruct negb; trivial.
Qed.

Lemma top_ok:
  forall rs, sem_rel RELATION.top rs.
Proof.
  unfold sem_rel, sem_reg, RELATION.top.
  intros.
  rewrite PTree.gempty.
  reflexivity.
Qed.

Lemma sem_rel_ge:
  forall r1 r2 : RELATION.t,
    (RELATION.ge r1 r2) ->
    forall rs : regset,
      (sem_rel r2 rs) -> (sem_rel r1 rs).
Proof.
  intros r1 r2 GE rs RE x.
  pose proof (RE x) as REx.
  pose proof (GE x) as GEx.
  unfold sem_reg in *.
  destruct (r1 ! x) as [r1x | ] in *;
    destruct (r2 ! x) as [r2x | ] in *;
    congruence.
Qed.
End SAME_MEMORY.

Lemma kill_mem_sound :
  forall m m' : mem,
  forall rel : RELATION.t,
  forall rs,
    sem_rel m rel rs -> sem_rel m' (kill_mem rel) rs.
Proof.
  unfold sem_rel, sem_reg.
  intros until rs.
  intros SEM x.
  pose proof (SEM x) as SEMx.
  unfold kill_mem.
  rewrite PTree.gfilter1.
  unfold kill_sym_val_mem.
  destruct (rel ! x) as [ sv | ].
  2: reflexivity.
  destruct sv; simpl in *; trivial.
  {
    destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial.
    rewrite SEMx.
    apply op_depends_on_memory_correct; auto.
  }
Qed.
  
Lemma kill_store_sound :
  forall m m' : mem,
  forall rel : RELATION.t,
  forall chunk addr args a v rs,
    (eval_addressing genv sp addr (rs ## args)) = Some a ->
    (Mem.storev chunk m a v) = Some m' ->
    sem_rel m rel rs -> sem_rel m' (kill_store chunk addr args rel) rs.
Proof.
  unfold sem_rel, sem_reg.
  intros until rs.
  intros ADDR STORE SEM x.
  pose proof (SEM x) as SEMx.
  unfold kill_store, kill_store1.
  rewrite PTree.gfilter1.
  destruct (rel ! x) as [ sv | ].
  2: reflexivity.
  destruct sv; simpl in *; trivial.
  {
    destruct op_depends_on_memory eqn:DEPENDS; simpl; trivial.
    rewrite SEMx.
    apply op_depends_on_memory_correct; auto.
  }
  destruct may_overlap eqn:OVERLAP; simpl; trivial.
  destruct (eval_addressing genv sp addr0 rs ## args0) eqn:ADDR0.
  {
    erewrite may_overlap_sound with (args := (map (forward_move rel) args)).
    all: try eassumption.
    
    erewrite forward_move_map by eassumption.
    assumption.
  }
  intuition congruence.
Qed.

Lemma kill_builtin_res_sound:
  forall res (m : mem) (rs : regset) vres (rel : RELATION.t)
         (REL : sem_rel m rel rs),
         (sem_rel m (kill_builtin_res res rel) (regmap_setres res vres rs)).
Proof.
  destruct res; simpl; intros; trivial.
  apply kill_reg_sound; trivial.
Qed.
End SOUNDNESS.

Definition match_prog (p tp: RTL.program) :=
  match_program (fun cu f tf => tf = transf_fundef f) eq p tp.

Lemma transf_program_match:
  forall p, match_prog p (transf_program p).
Proof.
  intros. apply match_transform_program; auto.
Qed.

Section PRESERVATION.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  Genv.find_funct tge v = Some (transf_fundef f).
Proof (Genv.find_funct_transf TRANSL).

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  Genv.find_funct_ptr tge v = Some (transf_fundef f).
Proof (Genv.find_funct_ptr_transf TRANSL).

Lemma symbols_preserved:
  forall id,
  Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_transf TRANSL).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_transf TRANSL).

Lemma sig_preserved:
  forall f, funsig (transf_fundef f) = funsig f.
Proof.
  destruct f; trivial.
Qed.

Lemma find_function_translated:
  forall ros rs fd,
  find_function ge ros rs = Some fd ->
  find_function tge ros rs = Some (transf_fundef fd).
Proof.
  unfold find_function; intros. destruct ros as [r|id].
  eapply functions_translated; eauto.
  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
  eapply function_ptr_translated; eauto.
Qed.

Lemma transf_function_at:
  forall (f : function) (pc : node) (i : instruction),
  (fn_code f)!pc = Some i ->
  (fn_code (transf_function f))!pc =
    Some(transf_instr (forward_map f) pc i).
Proof.
  intros until i. intro CODE.
  unfold transf_function; simpl.
  rewrite PTree.gmap.
  unfold option_map.
  rewrite CODE.
  reflexivity.
Qed.

Definition is_killed_in_map (map : PMap.t RB.t) pc res :=
  match PMap.get pc map with
  | None => True
  | Some rel => exists rel', RELATION.ge rel (kill_reg res rel')
  end.

Definition is_killed_in_fmap fmap pc res :=
  match fmap with
  | None => True
  | Some map => is_killed_in_map map pc res
  end.

Lemma external_call_sound:
  forall ef (rel : RELATION.t) sp (m m' : mem) (rs : regset) vargs t vres
         (REL : sem_rel fundef unit ge sp m rel rs)
         (CALL : external_call ef ge vargs m t vres m'),
    sem_rel fundef unit ge sp m' (apply_external_call ef rel) rs.
Proof.
  destruct ef; intros; simpl in *.
  all: eauto using kill_mem_sound.
  all: unfold builtin_or_external_sem in *.
  1, 2: destruct (Builtins.lookup_builtin_function name sg);
    eauto using kill_mem_sound;
    inv CALL; eauto using kill_mem_sound.
  all: inv CALL.
  all: eauto using kill_mem_sound.
Qed.
  
Definition sem_rel_b' := sem_rel_b fundef unit ge.
Definition fmap_sem' := fmap_sem fundef unit ge.
Definition subst_arg_ok' := subst_arg_ok fundef unit ge.
Definition subst_args_ok' := subst_args_ok fundef unit ge.
Definition kill_mem_sound' := kill_mem_sound fundef unit ge.
Definition kill_store_sound' := kill_store_sound fundef unit ge.

Lemma sem_rel_b_ge:
  forall rb1 rb2 : RB.t,
    (RB.ge rb1 rb2) ->
    forall sp m,
    forall rs : regset,
      (sem_rel_b' sp m rb2 rs) -> (sem_rel_b' sp m rb1 rs).
Proof.
  unfold sem_rel_b', sem_rel_b.
  destruct rb1 as [r1 | ];
    destruct rb2 as [r2 | ]; simpl;
      intros GE sp m rs RE; try contradiction.
  apply sem_rel_ge with (r2 := r2); assumption.
Qed.

Lemma apply_instr'_bot :
  forall code,
  forall pc,
    RB.eq (apply_instr' code pc RB.bot) RB.bot.
Proof.
  reflexivity.
Qed.

Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
| match_frames_intro: forall res f sp pc rs,
    (forall m : mem,
     forall vres, (fmap_sem' sp m (forward_map f) pc rs # res <- vres)) ->
    match_frames (Stackframe res f sp pc rs)
                 (Stackframe res (transf_function f) sp pc rs).

Inductive match_states: RTL.state -> RTL.state -> Prop :=
  | match_regular_states: forall stk f sp pc rs m stk'
                                 (STACKS: list_forall2 match_frames stk stk'),
      (fmap_sem' sp m (forward_map f) pc rs) ->
      match_states (State stk f sp pc rs m)
                   (State stk' (transf_function f) sp pc rs m)
  | match_callstates: forall stk f args m stk'
        (STACKS: list_forall2 match_frames stk stk'),
      match_states (Callstate stk f args m)
                   (Callstate stk' (transf_fundef f) args m)
  | match_returnstates: forall stk v m stk'
        (STACKS: list_forall2 match_frames stk stk'),
      match_states (Returnstate stk v m)
                   (Returnstate stk' v m).
  
Ltac TR_AT :=
  match goal with
  | [ A: (fn_code _)!_ = Some _ |- _ ] =>
        generalize (transf_function_at _ _ _ A); intros
  end.

Lemma step_simulation:
  forall S1 t S2, RTL.step ge S1 t S2 ->
  forall S1', match_states S1 S1' ->
              exists S2', RTL.step tge S1' t S2' /\ match_states S2 S2'.
Proof.
  induction 1; intros S1' MS; inv MS; try TR_AT.
- (* nop *)
  econstructor; split. eapply exec_Inop; eauto.
  constructor; auto.
  
  simpl in *.
  unfold fmap_sem', fmap_sem in *.
  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
  apply sem_rel_b_ge with (rb2 := map # pc); trivial.
  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
  {
    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
    2: apply apply_instr'_bot.
    simpl. tauto.
  }
  unfold apply_instr'.
  unfold sem_rel_b in *.
  destruct (map # pc) in *; try contradiction.
  rewrite H.
  reflexivity.
- (* op *)
  unfold transf_instr in *.
  destruct (if is_trivial_op op then None else find_op_in_fmap (forward_map f) pc op
               (subst_args (forward_map f) pc args)) eqn:FIND_OP.
  {
    destruct (is_trivial_op op).
    discriminate.
    unfold find_op_in_fmap, fmap_sem', fmap_sem in *.
    destruct (forward_map f) as [map |] eqn:MAP.
    2: discriminate.
    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
    destruct (map # pc) as [mpc | ] eqn:MPC.
    2: discriminate.
    econstructor; split.
    {
      eapply exec_Iop with (v := v); eauto.
      simpl.
      rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
      {
        rewrite MAP in H0.
        rewrite find_op_sound with (rel := mpc) (src := r) in H0 by assumption.
        assumption.
      }
      unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
    }
    constructor; eauto.
    unfold fmap_sem', fmap_sem in *.
    rewrite MAP.
    apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)).
    {
      replace (Some (gen_oper op res args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
      {
        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
        2: apply apply_instr'_bot.
        simpl. tauto.
      }
      unfold apply_instr'.
      rewrite H.
      rewrite MPC.
      reflexivity.
    }
    unfold sem_rel_b', sem_rel_b.
    apply gen_oper_sound; auto.
  }
  {
    econstructor; split.
    {
      eapply exec_Iop with (v := v); eauto.
      rewrite (subst_args_ok' sp m) by assumption.
      rewrite <- H0.
      apply eval_operation_preserved. exact symbols_preserved.
    }
    constructor; eauto.
    unfold fmap_sem', fmap_sem in *.
    unfold find_op_in_fmap, fmap_sem', fmap_sem in *.
    destruct (forward_map f) as [map |] eqn:MAP.
    2: constructor.
    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
    destruct (map # pc) as [mpc | ] eqn:MPC.
    2: contradiction.

    apply sem_rel_b_ge with (rb2 := Some (gen_oper op res args mpc)).
    {
      replace (Some (gen_oper op res args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
      {
        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
        2: apply apply_instr'_bot.
        simpl. tauto.
      }
      unfold apply_instr'.
      rewrite H.
      rewrite MPC.
      reflexivity.
    }
    unfold sem_rel_b', sem_rel_b.
    apply gen_oper_sound; auto.
  }
    
(* load *)
- unfold transf_instr in *. inv H0.
  + destruct find_load_in_fmap eqn:FIND_LOAD.
    {
      unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
      destruct (forward_map f) as [map |] eqn:MAP.
      2: discriminate.
      change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
      destruct (map # pc) as [mpc | ] eqn:MPC.
      2: discriminate.
      econstructor; split.
      {
        eapply exec_Iop with (v := v); eauto.
        simpl.
        rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL.
        {
          f_equal.
          symmetry.
          rewrite MAP in EVAL.
          eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
          all: eassumption.
        }
        unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
      }
      constructor; eauto.
      unfold fmap_sem', fmap_sem in *.
      rewrite MAP.
      apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
      {
        replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
        {
          eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
          2: apply apply_instr'_bot.
          simpl. tauto.
        }
        unfold apply_instr'.
        rewrite H.
        rewrite MPC.
        simpl.
        reflexivity.
      }
      unfold sem_rel_b', sem_rel_b.
      apply load_sound with (a := a); auto.
    }
    {  
    econstructor; split.
    assert (eval_addressing tge sp addr rs ## args = Some a).
    rewrite <- EVAL.
    apply eval_addressing_preserved. exact symbols_preserved.
    eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
    rewrite (subst_args_ok' sp m); assumption.
    constructor; auto.

    simpl in *.
    unfold fmap_sem', fmap_sem in *.
    destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
    destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
    apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
    {
      replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
      {
        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
        2: apply apply_instr'_bot.
        simpl. tauto.
      }
      unfold apply_instr'.
      rewrite H.
      rewrite MPC.
      simpl.
      reflexivity.
    }
    apply load_sound with (a := a); assumption.
    }
    
  + destruct (eval_addressing) eqn:EVAL in LOAD.
    * specialize (LOAD v).
      destruct find_load_in_fmap eqn:FIND_LOAD.
        {
          unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
          destruct (forward_map f) as [map |] eqn:MAP.
          2: discriminate.
          change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
          destruct (map # pc) as [mpc | ] eqn:MPC.
          2: discriminate.
          econstructor; split.
          {
            eapply exec_Iop with (v := Vundef); eauto.
            simpl.
            rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL.
            {
              f_equal.
              rewrite MAP in EVAL.
              eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
              all: try eassumption. apply LOAD; auto.
            }
            unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
          }
          constructor; eauto.
          unfold fmap_sem', fmap_sem in *.
          rewrite MAP.
          apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
          {
            replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
            {
              eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
              2: apply apply_instr'_bot.
              simpl. tauto.
            }
            unfold apply_instr'.
            rewrite H.
            rewrite MPC.
            simpl.
            reflexivity.
          }
          unfold sem_rel_b', sem_rel_b.
          apply load_notrap2_sound with (a := v); auto.
        }
        {  
        econstructor; split.
        assert (eval_addressing tge sp addr rs ## args = Some v).
        rewrite <- EVAL.
        apply eval_addressing_preserved. exact symbols_preserved.
        eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
        rewrite (subst_args_ok' sp m).
        intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'; auto.
        assumption.
        constructor; auto.

        simpl in *.
        unfold fmap_sem', fmap_sem in *.
        destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
        destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
        apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
        {
          replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
          {
            eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
            2: apply apply_instr'_bot.
            simpl. tauto.
          }
          unfold apply_instr'.
          rewrite H.
          rewrite MPC.
          simpl.
          reflexivity.
        }
        apply load_notrap2_sound with (a := v); auto.
        }
        
    * destruct find_load_in_fmap eqn:FIND_LOAD.
      {
        unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
        destruct (forward_map f) as [map |] eqn:MAP.
        2: discriminate.
        change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
        destruct (map # pc) as [mpc | ] eqn:MPC.
        2: discriminate.
        econstructor; split.
        {
          eapply exec_Iop with (v := Vundef); eauto.
          simpl.
          rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL.
          {
            f_equal.
            rewrite MAP in EVAL.
            eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
            all: eassumption.
          }
          unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
        }
        constructor; eauto.
        unfold fmap_sem', fmap_sem in *.
        rewrite MAP.
        apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
        {
          replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
          {
            eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
            2: apply apply_instr'_bot.
            simpl. tauto.
          }
          unfold apply_instr'.
          rewrite H.
          rewrite MPC.
          simpl.
          reflexivity.
        }
        unfold sem_rel_b', sem_rel_b.
        apply load_notrap1_sound; auto.
      }
      {  
      econstructor; split.
      assert (eval_addressing tge sp addr rs ## args = None).
      rewrite <- EVAL.
      apply eval_addressing_preserved. exact symbols_preserved.
      eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
      rewrite (subst_args_ok' sp m); eauto. congruence.
      constructor; auto.

      simpl in *.
      unfold fmap_sem', fmap_sem in *.
      destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
      destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
      apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
      {
        replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
        {
          eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
          2: apply apply_instr'_bot.
          simpl. tauto.
        }
        unfold apply_instr'.
        rewrite H.
        rewrite MPC.
        simpl.
        reflexivity.
      }
      apply load_notrap1_sound; assumption.
      }
  
- (* store *)
  econstructor. split.
  {
    assert (eval_addressing tge sp addr rs ## args = Some a).
    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
    eapply exec_Istore; eauto.
    - rewrite (subst_args_ok' sp m) by assumption.
      eassumption.
    - rewrite (subst_arg_ok' sp m) by assumption.
      eassumption.
  }
  
  constructor; auto.
  simpl in *.
  unfold fmap_sem', fmap_sem in *.
  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
  apply sem_rel_b_ge with (rb2 := Some (kill_store chunk addr args mpc)); trivial.
  {
  replace (Some (kill_store chunk addr args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
  {
    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
    2: apply apply_instr'_bot.
    simpl. tauto.
  }
  unfold apply_instr'.
  unfold sem_rel_b in *.
  rewrite MPC.
  rewrite H.
  reflexivity.
  }
  eapply (kill_store_sound' sp m); eassumption.
  
(* call *)
- econstructor; split.
  eapply exec_Icall with (fd := transf_fundef fd); eauto.
    eapply find_function_translated; eauto.
    apply sig_preserved.
  rewrite (subst_args_ok' sp m) by assumption.
  constructor. constructor; auto.

  constructor.
  {
    intros m' vres.
    unfold fmap_sem', fmap_sem in *.
    destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
    destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
    apply sem_rel_b_ge with (rb2 := Some (kill_reg res (kill_mem mpc))).
    {
      replace (Some (kill_reg res (kill_mem mpc))) with (apply_instr' (fn_code f) pc (map # pc)).
      {
        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
        2: apply apply_instr'_bot.
        simpl. tauto.
      }
      unfold apply_instr'.
      rewrite H.
      rewrite MPC.
      reflexivity.
    }
    apply kill_reg_sound.
    apply (kill_mem_sound' sp m).
    assumption.
  }
  
(* tailcall *)
- econstructor; split.
  eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
    eapply find_function_translated; eauto.
    apply sig_preserved.
  rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption.
  constructor. auto.

(* builtin *)
- 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.
  constructor; auto.

  simpl in *.
  unfold fmap_sem', fmap_sem in *.
  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
  
  apply sem_rel_b_ge with (rb2 := Some (kill_builtin_res res (apply_external_call ef mpc))).
  {
    replace (Some (kill_builtin_res res (apply_external_call ef mpc))) with (apply_instr' (fn_code f) pc (map # pc)).
    {
      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
      2: apply apply_instr'_bot.
      simpl. tauto.
    }
    unfold apply_instr'.
    rewrite H.
    rewrite MPC.
    reflexivity.
  }
  apply kill_builtin_res_sound.
  eapply external_call_sound with (m := m); eassumption.

(* cond *)
- econstructor; split.
  eapply exec_Icond; eauto.
  rewrite (subst_args_ok' sp m); eassumption.
  constructor; auto.

  simpl in *.
  unfold fmap_sem', fmap_sem in *.
  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
  apply sem_rel_b_ge with (rb2 := map # pc); trivial.
  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
  {
    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
    2: apply apply_instr'_bot.
    simpl.
    destruct b; tauto.
  }
  unfold apply_instr'.
  unfold sem_rel_b in *.
  destruct (map # pc) in *; try contradiction.
  rewrite H.
  reflexivity.

(* jumptbl *)
- econstructor; split.
  eapply exec_Ijumptable; eauto.
  rewrite (subst_arg_ok' sp m); eassumption.
  constructor; auto.

  simpl in *.
  unfold fmap_sem', fmap_sem in *.
  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
  apply sem_rel_b_ge with (rb2 := map # pc); trivial.
  replace (map # pc) with (apply_instr' (fn_code f) pc (map # pc)).
  {
    eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
    2: apply apply_instr'_bot.
    simpl.
    apply list_nth_z_in with (n := Int.unsigned n).
    assumption.
  }
  unfold apply_instr'.
  unfold sem_rel_b in *.
  destruct (map # pc) in *; try contradiction.
  rewrite H.
  reflexivity.
  
(* return *)
- destruct or as [arg | ].
  {
    econstructor; split.
    eapply exec_Ireturn; eauto.
    unfold regmap_optget.
    rewrite (subst_arg_ok' (Vptr stk Ptrofs.zero) m) by eassumption.
    constructor; auto.
  }
    econstructor; split.
    eapply exec_Ireturn; eauto.
    constructor; auto.
  
  
(* internal function *)
-  simpl. econstructor; split.
  eapply exec_function_internal; eauto.
  constructor; auto.

  simpl in *.
  unfold fmap_sem', fmap_sem in *.
  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
  apply sem_rel_b_ge with (rb2 := Some RELATION.top).
  {
    eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption.
  }
  apply top_ok.
  
(* external function *)
- econstructor; split.
  eapply exec_function_external; eauto.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
    constructor; auto.

(* return *)
- inv STACKS. inv H1.
  econstructor; split.
  eapply exec_return; eauto.
  constructor; auto.
Qed.


Lemma transf_initial_states:
  forall S1, RTL.initial_state prog S1 ->
  exists S2, RTL.initial_state tprog S2 /\ match_states S1 S2.
Proof.
  intros. inv H. econstructor; split.
  econstructor.
    eapply (Genv.init_mem_transf TRANSL); eauto.
    rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
    eapply function_ptr_translated; eauto.
    rewrite <- H3; apply sig_preserved.
  constructor. constructor.
Qed.

Lemma transf_final_states:
  forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.
Proof.
  intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
  eapply forward_simulation_step.
  apply senv_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  exact step_simulation.
Qed.

End PRESERVATION.