path: root/mppa_k1c/lib/RTLpathLivegen.v

(** Building a RTLpath program with liveness annotation.
*)


Require Import Coqlib.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import Globalenvs Smallstep RTL RTLpath.
Require Import Bool Errors Linking Values Events.
Require Import Program.

Local Open Scope lazy_bool_scope.

Local Open Scope option_monad_scope.

Axiom build_path_map: RTL.function -> path_map.

Extract Constant build_path_map => "RTLpathLivegenaux.build_path_map".

Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool :=
  match rl with
  | nil => true
  | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive
  end.

Definition exit_checker {A} (pm: path_map) (alive: Regset.t) (pc: node) (v:A): option A :=
   SOME path <- pm!pc IN
   ASSERT Regset.subset path.(input_regs) alive IN
   Some v.

Lemma exit_checker_path_entry A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res:
  exit_checker pm alive pc v = Some res -> path_entry pm pc.
Proof.
  unfold exit_checker, path_entry.
  inversion_SOME path; simpl; congruence.
Qed.

Lemma exit_checker_res A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res:
  exit_checker pm alive pc v = Some res -> v=res.
Proof.
  unfold exit_checker, path_entry.
  inversion_SOME path; try_simplify_someHyps.
  inversion_ASSERT; try_simplify_someHyps.
Qed.

(* FIXME - what about trap? *)
Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option (Regset.t * node)  :=
  match i with
  | Inop pc' => Some (alive, pc')
  | Iop op args dst pc' => 
      ASSERT list_mem args alive IN
      Some (Regset.add dst alive, pc')
  | Iload _ chunk addr args dst pc' =>
      ASSERT list_mem args alive IN
      Some (Regset.add dst alive, pc')
  | Istore chunk addr args src pc' =>
      ASSERT Regset.mem src alive IN
      ASSERT list_mem args alive IN
      Some (alive, pc')
  | Icond cond args ifso ifnot _ =>
      ASSERT list_mem args alive IN
      exit_checker pm alive ifso (alive, ifnot)
  | _ => None (* TODO jumptable ? *)
  end.


Local Hint Resolve exit_checker_path_entry: core.

Lemma iinst_checker_path_entry (pm: path_map) (alive: Regset.t) (i: instruction) res pc:
  iinst_checker pm alive i = Some res -> 
  early_exit i = Some pc -> path_entry pm pc.
Proof.
  destruct i; simpl; try_simplify_someHyps; subst.
  inversion_ASSERT; try_simplify_someHyps.
Qed.

Lemma iinst_checker_default_succ (pm: path_map) (alive: Regset.t) (i: instruction) res pc:
  iinst_checker pm alive i = Some res -> 
  pc = snd res ->
  default_succ i = Some pc.
Proof.
  destruct i; simpl; try_simplify_someHyps; subst;
  repeat (inversion_ASSERT); try_simplify_someHyps.
  intros; exploit exit_checker_res; eauto.
  intros; subst. simpl; auto.
Qed.

Fixpoint ipath_checker (ps:nat) (f: RTL.function) (pm: path_map) (alive: Regset.t) (pc:node): option (Regset.t * node) :=
  match ps with
  | O => Some (alive, pc)
  | S p =>
    SOME i <- f.(fn_code)!pc IN
    SOME res <- iinst_checker pm alive i IN
    ipath_checker p f pm (fst res) (snd res)
  end.

Lemma ipath_checker_wellformed f pm ps: forall alive pc res,
   ipath_checker ps f pm alive pc = Some res -> 
   wellformed_path f.(fn_code) pm 0 (snd res) ->
   wellformed_path f.(fn_code) pm ps pc.
Proof.
  induction ps; simpl; try_simplify_someHyps.
  inversion_SOME i; inversion_SOME res'.
  intros. eapply wf_internal_node; eauto.
  * eapply iinst_checker_default_succ; eauto.
  * intros; eapply iinst_checker_path_entry; eauto.
Qed.

Definition reg_option_mem (or: option reg) (alive: Regset.t) :=
  match or with None => true | Some r => Regset.mem r alive end.

Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) :=
  match ros with inl r => Regset.mem r alive | inr s => true end.

(* NB: definition following [regmap_setres] in [RTL.step] semantics *)
Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t :=
  match res with
  | BR r => Regset.add r alive
  | _ => alive
  end.

Fixpoint exit_list_checker (pm: path_map) (alive: Regset.t) (l: list node): bool :=
   match l with
   | nil => true
   | pc::l' => exit_checker pm alive pc tt &&& exit_list_checker pm alive l'
   end.

Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true.
Proof.
  destruct o; simpl; intuition. 
  - eauto.
  - firstorder. try_simplify_someHyps.
Qed.

Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true.
Proof.
   intros; rewrite lazy_and_Some_true; firstorder.
   destruct x; auto.
Qed.


Lemma exit_list_checker_correct pm alive l pc:
  exit_list_checker pm alive l = true -> List.In pc l -> exit_checker pm alive pc tt = Some tt.
Proof.
  intros EXIT PC; induction l; intuition.
  simpl in * |-. rewrite lazy_and_Some_tt_true in EXIT.
  firstorder (subst; eauto).
Qed.

Local Hint Resolve exit_list_checker_correct: core.

Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
   match i with
   | Icall sig ros args res pc' =>
      ASSERT list_mem args alive IN
      ASSERT reg_sum_mem ros alive IN
      exit_checker pm (Regset.add res alive) pc' tt
   | Itailcall sig ros args =>
      ASSERT list_mem args alive IN
      ASSERT reg_sum_mem ros alive IN
      Some tt
   | Ibuiltin ef args res pc' =>
      ASSERT list_mem (params_of_builtin_args args) alive IN 
      exit_checker pm (reg_builtin_res res alive) pc' tt
   | Ijumptable arg tbl =>
      ASSERT Regset.mem arg alive IN
      ASSERT exit_list_checker pm alive tbl IN
      Some tt
   | Ireturn optarg =>
      ASSERT (reg_option_mem optarg) alive IN 
      Some tt
   | _ => 
      SOME res <- iinst_checker pm alive i IN
      exit_checker pm (fst res) (snd res) tt
   end.

Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
  inst_checker pm alive i = Some tt ->
  c!pc = Some i -> wellformed_path c pm 0 pc.
Proof.
  intros CHECK PC. eapply wf_last_node; eauto.
  clear c pc PC. intros pc PC.
  destruct i; simpl in * |- *; intuition (subst; eauto);
  try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
  intros X; exploit exit_checker_res; eauto.
  clear X. intros; subst; eauto.
Qed.

Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
   SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc  IN
   SOME i <- f.(fn_code)!(snd res) IN
   inst_checker pm (fst res) i.

Lemma path_checker_wellformed f pm pc path:
   path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
Proof.
  unfold path_checker.
  inversion_SOME res.
  inversion_SOME i.
  intros; eapply ipath_checker_wellformed; eauto.
  eapply inst_checker_wellformed; eauto.
Qed.

Fixpoint list_path_checker f pm (l:list (node*path_info)): bool :=
  match l with
  | nil => true
  | (pc, path)::l' =>
      path_checker f pm pc path &&& list_path_checker f pm l'
  end.

Lemma list_path_checker_correct f pm l: 
  list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt.
Proof.
  intros CHECKER e H; induction l as [|(pc & path) l]; intuition.
  simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
Qed.

Definition function_checker (f: RTL.function) pm: bool := 
  pm!(f.(fn_entrypoint)) &&& list_path_checker f pm (PTree.elements pm).

Lemma function_checker_correct f pm pc path: 
  function_checker f pm = true -> 
  pm!pc = Some path -> 
  path_checker f pm pc path = Some tt.
Proof.
  unfold function_checker; rewrite lazy_and_Some_true.
  intros (ENTRY & PATH) PC.
  exploit list_path_checker_correct; eauto.
  - eapply PTree.elements_correct; eauto.
  - simpl; auto.
Qed.

Lemma function_checker_wellformed_path_map f pm:
  function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.
Proof.
  unfold wellformed_path_map.
  intros; eapply path_checker_wellformed; eauto.
  intros; eapply function_checker_correct; eauto.
Qed.

Lemma function_checker_path_entry f pm:
  function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).
Proof.
  unfold function_checker; rewrite lazy_and_Some_true;
  unfold path_entry. firstorder congruence.
Qed.

Definition liveness_ok_function (f: function): Prop :=
  forall pc path, f.(fn_path)!pc = Some path -> path_checker f f.(fn_path) pc path = Some tt.

Program Definition transf_function (f: RTL.function): { r: res function | forall f', r = OK f' -> liveness_ok_function f' /\ f'.(fn_RTL) = f } :=
  let pm := build_path_map f in
  match function_checker f pm with
  | true => OK {| fn_RTL := f; fn_path := pm |}
  | false => Error(msg "RTLpathGen: function_checker failed")
  end.
Obligation 1.
  apply function_checker_path_entry; auto.
Qed.
Obligation 2.
  apply function_checker_wellformed_path_map; auto.
Qed.
Obligation 3.
  unfold liveness_ok_function; simpl; intros; intuition.
  apply function_checker_correct; auto.
Qed.

Definition transf_fundef (f: RTL.fundef) : res fundef :=
  transf_partial_fundef (fun f => ` (transf_function f)) f.

Inductive liveness_ok_fundef: fundef -> Prop :=
  | liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f)
  | liveness_ok_External ef: liveness_ok_fundef (External ef).

Lemma transf_fundef_correct f f':
  transf_fundef f = OK f' -> (liveness_ok_fundef f') /\ fundef_RTL f' = f.
Proof.
  intros TRANSF; destruct f; simpl; monadInv TRANSF.
  - destruct (transf_function f) as [res H]; simpl in * |- *; auto.
    destruct (H _ EQ).
    intuition subst; auto. apply liveness_ok_Internal; auto.
  - intuition. apply liveness_ok_External; auto.
Qed.

Definition transf_program (p: RTL.program) : res program :=
  transform_partial_program transf_fundef p.

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

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.

Section PRESERVATION.

Variables prog: RTL.program.
Variables tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.
Let tge := Genv.globalenv (program_RTL tprog).

Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  rewrite <- (Genv.find_symbol_match TRANSL).
  apply (Genv.find_symbol_match (match_prog_RTL tprog)).
Qed.

Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z.
Proof.
  unfold Senv.equiv. intuition congruence.
Qed.

Lemma senv_preserved: Senv.equiv ge tge.
Proof.
  eapply senv_transitivity. { eapply (Genv.senv_match TRANSL). }
  eapply RTLpath.senv_preserved.
Qed.

Lemma function_ptr_preserved v f: Genv.find_funct_ptr ge v = Some f -> 
  exists tf, Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf.
Proof.
  intros; apply (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.


Lemma function_ptr_RTL_preserved v f: Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some f.
Proof.
  intros; exploit function_ptr_preserved; eauto.
  intros (tf & Htf & TRANS).
  exploit (Genv.find_funct_ptr_match (match_prog_RTL tprog)); eauto.
  intros (cunit & tf0 & X & Y & DUM); subst.
  unfold tge. rewrite X. 
  exploit transf_fundef_correct; eauto. 
  intuition subst; auto.
Qed.

Lemma find_function_preserved ros rs fd:
  RTL.find_function ge ros rs = Some fd -> RTL.find_function tge ros rs = Some fd.
Proof.
  intros H; assert (X: exists tfd, find_function tpge ros rs = Some tfd /\ fd = fundef_RTL tfd). 
  * destruct ros; simpl in * |- *.
    + intros; exploit (Genv.find_funct_match TRANSL); eauto.
      intros (cuint & tf & H1 & H2 & H3); subst; repeat econstructor; eauto.
      exploit transf_fundef_correct; eauto. 
      intuition auto.
    + rewrite <- (Genv.find_symbol_match TRANSL) in H.
    unfold tpge. destruct (Genv.find_symbol _ i); simpl; try congruence.
    exploit function_ptr_preserved; eauto.
    intros (tf & H1 & H2); subst; repeat econstructor; eauto.
    exploit transf_fundef_correct; eauto. 
    intuition auto.
 * destruct X as (tf & X1 & X2); subst.
   eapply find_function_RTL_match; eauto.
Qed.


Local Hint Resolve symbols_preserved senv_preserved: core.

Lemma transf_program_RTL_correct: 
  forward_simulation (RTL.semantics prog) (RTL.semantics (program_RTL tprog)).
Proof.
  eapply forward_simulation_step with (match_states:=fun (s1 s2:RTL.state) => s1=s2); simpl; eauto.
  - eapply senv_preserved.
  - (* initial states *)
    intros s1 INIT. destruct INIT as [b f m0 ge0 INIT SYMB PTR SIG]. eexists; intuition eauto.
    econstructor; eauto.
    + intros; eapply (Genv.init_mem_match (match_prog_RTL tprog)). apply (Genv.init_mem_match TRANSL); auto.
    + rewrite symbols_preserved. 
      replace (prog_main (program_RTL tprog)) with (prog_main prog).
      * eapply SYMB.
      * erewrite (match_program_main (match_prog_RTL tprog)). erewrite (match_program_main TRANSL); auto.
    + exploit function_ptr_RTL_preserved; eauto.
  - intros; subst; auto.
  - intros s t s2 STEP s1 H; subst.
    eexists; intuition.
    destruct STEP. 
    + (* Inop *) eapply exec_Inop; eauto.
    + (* Iop *) eapply exec_Iop; eauto.
      erewrite eval_operation_preserved; eauto.
    + (* Iload *) eapply exec_Iload; eauto. 
     erewrite eval_addressing_preserved; eauto.
    + (* Iload notrap1 *) eapply exec_Iload_notrap1; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Iload notrap2 *) eapply exec_Iload_notrap2; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Istore *) eapply exec_Istore; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Icall *)
        eapply RTL.exec_Icall; eauto.
        eapply find_function_preserved; eauto.
    + (* Itailcall *)
        eapply RTL.exec_Itailcall; eauto.
        eapply find_function_preserved; eauto.
    + (* Ibuiltin *)
      eapply RTL.exec_Ibuiltin; eauto.
      * eapply eval_builtin_args_preserved; eauto.
      * eapply external_call_symbols_preserved; eauto.
    + (* Icond *)
      eapply exec_Icond; eauto.
    + (* Ijumptable *)
      eapply RTL.exec_Ijumptable; eauto.
    + (* Ireturn *)
      eapply RTL.exec_Ireturn; eauto.
    + (* exec_function_internal *)
      eapply RTL.exec_function_internal; eauto.
    + (* exec_function_external *)
      eapply RTL.exec_function_external; eauto.
      eapply external_call_symbols_preserved; eauto.
    + (* exec_return *)
      eapply RTL.exec_return; eauto.
Qed.

Theorem transf_program_correct: 
  forward_simulation (RTL.semantics prog) (RTLpath.semantics tprog).
Proof.
  eapply compose_forward_simulations.
  + eapply transf_program_RTL_correct.
  + eapply RTLpath_complete.
Qed.


(* Properties used in hypothesis of [RTLpathLiveproofs.step_eqlive] theorem *)
Theorem all_fundef_liveness_ok b f:
  Genv.find_funct_ptr tpge b = Some f -> liveness_ok_fundef f.
Proof.
  unfold match_prog, match_program in TRANSL.
  unfold Genv.find_funct_ptr, tpge; simpl; intro X.
  destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence.
  destruct y as [tf0|]; try congruence.
  inversion X as [H1]. subst. clear X.
  remember (@Gfun fundef unit f) as f2.
  destruct H as [ctx' f1 f2 H0|]; try congruence.
  inversion Heqf2 as [H2]. subst; clear Heqf2.
  exploit transf_fundef_correct; eauto.
  intuition.
Qed.

End PRESERVATION.