path: root/backend/RTLTunnelingproof.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*          TODO: Proper author information                            *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Correctness proof for the branch tunneling optimization for RTL. *)
(* This is a port of Tunnelingproof.v, the same optimisation for LTL. *)

Require Import Coqlib Maps Errors.
Require Import AST Linking.
Require Import Values Memory Registers Events Globalenvs Smallstep.
Require Import Op Locations RTL.
Require Import RTLTunneling.
Require Import Conventions1.

Local Open Scope nat.

(**) Definition check_included_spec (c:code) (td:UF) (ok: option instruction) :=
  ok <> None -> forall pc, c!pc = None -> td!pc = None.

Lemma check_included_correct (td:UF) (c:code):
  check_included_spec c td (check_included td c).
Proof.
  apply PTree_Properties.fold_rec with (P:=check_included_spec c); unfold check_included_spec.
  - intros m m' oi EQ IND N pc. rewrite <- EQ. apply IND. apply N.
  - intros N pc. rewrite PTree.gempty. auto.
  - intros m oi pc v N S IND. destruct oi.
    + intros. rewrite PTree.gsspec. destruct (peq _ _); try congruence. apply IND. congruence. apply H0.
    + contradiction.
Qed.

(**) Inductive target_bounds (target: node -> node) (bound: node -> nat) (pc: node) : option instruction -> Prop :=
  | TB_default (TB: target pc = pc) oi:
      target_bounds target bound pc oi
  | TB_nop s
      (EQ: target pc = target s)
      (DEC: bound s < bound pc):
      target_bounds target bound pc (Some (Inop s))
  | TB_cond cond args ifso ifnot info
      (EQSO: target pc = target ifso)
      (EQNOT: target pc = target ifnot)
      (DECSO: bound ifso < bound pc)
      (DECNOT: bound ifnot < bound pc):
      target_bounds target bound pc (Some (Icond cond args ifso ifnot info))
.
Local Hint Resolve TB_default: core.

Lemma target_None (td: UF) (pc: node): td!pc = None -> td pc = pc.
Proof.
  unfold target, get. intro EQ. rewrite EQ. auto.
Qed.
Local Hint Resolve target_None Z.abs_nonneg: core.

Lemma get_nonneg td pc t d: get td pc = (t,d) -> (0 <= d)%Z.
Proof.
  unfold get. destruct td!pc as [(tpc,dpc)|]; intro H; inv H; lia.
Qed.
Local Hint Resolve get_nonneg: core.

(**) Definition bound (td: UF) (pc: node) := Z.to_nat (snd (get td pc)).


(* TODO: à réécrire proprement *)
Lemma check_instr_correct (td: UF) (pc: node) (i: instruction):
  check_instr td pc i = OK tt ->
  target_bounds (target td) (bound td) pc (Some i).
Proof.
  unfold check_instr. destruct (td!pc) as [(tpc,dpc)|] eqn:EQ.
  assert (DPC: snd (get td pc) = Z.abs dpc). { unfold get. rewrite EQ. auto. }
  - destruct i; try congruence.
    + destruct (get td n) as (ts,ds) eqn:EQs.
      destruct (peq _ _); try congruence.
      destruct (zlt _ _); try congruence. intros _.
      apply TB_nop. replace (td pc) with tpc.
      unfold target. rewrite EQs. auto.
      unfold target. unfold get. rewrite EQ. auto.
      unfold bound. rewrite DPC. rewrite EQs; simpl. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n ts. apply EQs.
    + destruct (get td n) as (tso,dso) eqn:EQSO.
      destruct (get td n0) as (tnot,dnot) eqn:EQNOT.
      intro H.
      repeat ((destruct (peq _ _) in H || destruct (zlt _ _) in H); try congruence).
      apply TB_cond; subst.
      * unfold target. replace (fst (get td pc)) with tnot. rewrite EQSO. auto.
        unfold get. rewrite EQ. auto.
      * unfold target. replace (fst (get td pc)) with tnot. rewrite EQNOT. auto.
        unfold get. rewrite EQ. auto.
      * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n tnot. rewrite EQSO. auto. rewrite EQSO. auto.
      * unfold bound. rewrite DPC. apply Z2Nat.inj_lt; try lia. apply get_nonneg with td n0 tnot. rewrite EQNOT; auto. rewrite EQNOT; auto.
  - intros _. apply TB_default. unfold target. unfold get. rewrite EQ. auto.
Qed.

Definition check_code_spec (td:UF) (c:code) (ok: res unit) :=
   ok = OK tt -> forall pc i, c!pc = Some i -> target_bounds (target td) (bound td) pc (Some i).

Lemma check_code_correct (td:UF) c:
   check_code_spec td c (check_code td c).
Proof.
  unfold check_code. apply PTree_Properties.fold_rec; unfold check_code_spec.
  - intros. rewrite <- H in H2. apply H0; auto.
  - intros. rewrite PTree.gempty in H0. congruence.
  - intros m [[]|e] pc i N S IND; simpl; try congruence.
    intros H pc0 i0. rewrite PTree.gsspec. destruct (peq _ _).
    subst. intro. inv H0. apply check_instr_correct. apply H.
    auto.
Qed.

Theorem branch_target_bounds:
  forall f tf pc,
  tunnel_function f = OK tf ->
  target_bounds (branch_target f) (bound (branch_target f)) pc (f.(fn_code)!pc).
Proof.
(* ~old
  intros t tf pc. unfold tunnel_function.
  destruct (check_included _ _) eqn:HI; try congruence.
  destruct (check_code _ _) eqn: HC.
  - intros _. destruct ((fn_code t) ! pc) eqn:EQ.
    + exploit check_code_correct; eauto.
    replace tt with u. auto. {destruct u; auto. }
    + exploit check_included_correct; eauto. rewrite HI. congruence.
    intro. apply TB_default. unfold target. unfold get. rewrite H. debug auto.
  - simpl. congruence.
*)

  intros. unfold tunnel_function in H.
  destruct (check_included _ _) eqn:EQinc; try congruence.
  monadInv H. rename EQ into EQcode.
  destruct (_ ! _) eqn:EQ.
  - exploit check_code_correct. destruct x. apply EQcode. apply EQ. auto.
  - exploit check_included_correct.
    rewrite EQinc. congruence.
    apply EQ.
    intro. apply TB_default. apply target_None. apply H.
Qed.

(** Preservation of semantics *)

Definition match_prog (p tp: program) :=
  match_program (fun _ f tf => tunnel_fundef f = OK tf) eq p tp.
  (* rq: `(fun _ ...)` est la fonction pour matcher des fonctions
   *     `eq` la fonction pour matcher les variables ? (`varinfo` dans la def)
   *     `p` et `tp` sont les programmes donc on doit dire s'ils match
   *)



Section PRESERVATION.


Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog. (* rq: on suppose que les programmes match *)
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

(* rq: pour les deux lemmes suivants, j'ai recopié les preuves, mais je ne les comprends pas du tout... D'où vient `exploit` ?? *)
(* rq: `exploit` vient de Coqlib! Mais je comprends pas encore vraiment ce qui se passe... *)
Lemma functions_translated:
  forall (v: val) (f: fundef),
  Genv.find_funct ge v = Some f ->
  exists tf, tunnel_fundef f = OK tf /\ Genv.find_funct tge v = Some tf.
Proof.
  intros.
  exploit (Genv.find_funct_match TRANSL). apply H.
  intros (cu & tf & A & B & C).
  (* exists tf. split. apply B. apply A. *)
  (* rq: on peut remplacer les `split` et `apply` par `eauto`, et ne pas spécifier le
   * `exists`, avec un `eexists` *)
  eexists. eauto.
  (* rq: Je ne comprends pas à quoi sert le `intuition`... *)
  (* repeat eexists; intuition eauto. *)
Qed.

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  exists tf,
  Genv.find_funct_ptr tge v = Some tf /\ tunnel_fundef f = OK tf.
Proof.
  intros. exploit (Genv.find_funct_ptr_match TRANSL).
  - apply H.
  - intros (cu & tf & A & B & C). exists tf. split. apply A. apply B.
Qed.

Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  apply (Genv.find_symbol_match TRANSL).
  (* rq: ici pas de `exploit` mais un `apply` parce que `Genv.find_symbol_match
   * prouve vraiment pile ce qu'on veut *)
Qed.

Lemma sig_preserved:
  forall f tf, tunnel_fundef f = OK tf -> funsig tf = funsig f.
Proof.
  intros. destruct f; simpl in H.
  -
    (*
    unfold bind in H.
    destruct (tunnel_function _) as [x|] eqn:EQ; try congruence.
    inversion H.
    unfold tunnel_function in EQ.
    destruct (check_included _ _) in EQ; try congruence.
    unfold bind in EQ. destruct (check_code _ _) in EQ; try congruence. inversion EQ. auto.
    *)

    monadInv H. (* rq: c'est une tactique maison... *)
    unfold tunnel_function in EQ.
    destruct (check_included _ _) in EQ; try congruence.
    monadInv EQ. auto.
  - monadInv H. auto.
Qed.

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof.
  eapply (Genv.senv_match TRANSL). (* Il y a déjà une preuve de cette propriété très exactement, je ne vais pas réinventer la roue ici *)
Qed.

(* TODO: vérifier s'il faut faire quelque chose avec le `res` ? *)
Inductive match_stackframes: stackframe -> stackframe -> Prop :=
  | match_stackframes_intro:
      forall res f tf sp pc rs trs
      (TF: tunnel_function f = OK tf)
      (RS: Registers.regs_lessdef rs trs),
      match_stackframes
        (Stackframe res f sp pc rs)
        (Stackframe res tf sp (branch_target f pc) trs).

(* rq: `match_states s1 s2` correspond à s1 ~ s2 *)
Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
      forall s ts f tf sp pc rs trs m tm
      (STK: list_forall2 match_stackframes s ts)
      (TF: tunnel_function f = OK tf)
      (RS: Registers.regs_lessdef rs trs)
      (MEM: Mem.extends m tm),
      match_states
        (State s f sp pc rs m)
        (State ts tf sp (branch_target f pc) trs tm)
  | match_states_call:
      forall s ts f tf a ta m tm
      (STK: list_forall2 match_stackframes s ts)
      (TF: tunnel_fundef f = OK tf)
      (ARGS: list_forall2 Val.lessdef a ta)
      (MEM: Mem.extends m tm),
      match_states
        (Callstate s f a m)
        (Callstate ts tf ta tm)
  | match_states_return:
      forall s ts v tv m tm
      (STK: list_forall2 match_stackframes s ts)
      (VAL: Val.lessdef v tv)
      (MEM: Mem.extends m tm),
      match_states
        (Returnstate s v m)
        (Returnstate ts tv tm).

(* TODO: il faut définir une bonne mesure *)
(* (**) Definition measure (st: state) : nat :=
  match st with
  | State s f sp pc rs m =>
      match (fn_code f)!pc with
      | Some (Inop pc') => (bound (branch_target f) pc') * 2 + 1
      | Some (Icond _ _ ifso ifnot _) => (max
                                    (bound (branch_target f) ifso)
                                    (bound (branch_target f) ifnot)
                                  ) * 2 + 1
      | Some _ => (bound (branch_target f) pc) * 2
      | None => 0
      end
  | Callstate s f v m => 0
  | Returnstate s v m => 0
  end.
*)

Definition measure (st: state): nat :=
  match st with
  | State s f sp pc rs m => bound (branch_target f) pc
  | Callstate s f v m => 0
  | Returnstate s v m => 0
  end.


(* rq: sans les lemmes définis au-dessus je ne vois pas trop comment j'aurais
 * fait... ni comment j'aurais eu l'idée d'en faire des lemmes ? *)
(**) Lemma transf_initial_states:
  forall s1: state, initial_state prog s1 ->
  exists s2: state, initial_state tprog s2 /\ match_states s1 s2.
Proof.
  intros. inversion H as [b f m0 ge0 MEM SYM PTR SIG CALL].
  exploit function_ptr_translated.
  - apply PTR.
  - intros (tf & TPTR & TUN).
    exists (Callstate nil tf nil m0). split.
    + apply initial_state_intro with b.
      * apply (Genv.init_mem_match TRANSL). apply MEM.
      * rewrite (match_program_main TRANSL).
        rewrite symbols_preserved. apply SYM.
      * apply TPTR.
      * rewrite <- SIG. apply sig_preserved. apply TUN.
    + apply match_states_call.
      * apply list_forall2_nil.
      * apply TUN.
      * apply list_forall2_nil.
      * apply Mem.extends_refl.
Qed.

(**) Lemma transf_final_states:
  forall (s1 : state)
  (s2 : state) (r : Integers.Int.int),
  match_states s1 s2 ->
  final_state s1 r ->
  final_state s2 r.
Proof.
  (* rq: `inv` au lieu de `inversion` fait beaucoup de nettoyage dans les
   * hypothèses, mais je sais pas trop ce que ça fait exactement *)
  intros. inv H0. inv H. inv VAL. inversion STK. apply final_state_intro.
Qed.

Lemma tunnel_function_unfold:
  forall f tf pc,
  tunnel_function f = OK tf ->
  (fn_code tf) ! pc =
  option_map (tunnel_instr (branch_target f)) (fn_code f) ! pc.
Proof.
  intros f tf pc.
  unfold tunnel_function.
  destruct (check_included _ _) eqn:EQinc; try congruence.
  destruct (check_code _ _) eqn:EQcode; simpl; try congruence.
  intro. inv H. simpl. rewrite PTree.gmap1. reflexivity.
Qed.

Lemma reglist_lessdef:
  forall (rs trs: Registers.Regmap.t val) (args: list Registers.reg),
  regs_lessdef rs trs -> Val.lessdef_list (rs##args) (trs##args).
Proof.
  intros. induction args; simpl; constructor.
  apply H. apply IHargs.
Qed.

(* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *)
Lemma tunnel_step_correct:
  forall st1 t st2, step ge st1 t st2 ->
  forall st1' (MS: match_states st1 st1'),
  (exists st2', step tge st1' t st2' /\ match_states st2 st2')
  \/ (measure st2 < measure st1 /\ t = E0 /\ match_states st2 st1')%nat.
Proof.
  intros st1 t st2 H. induction H; intros; try (inv MS).
  - (* Inop *)
    exploit branch_target_bounds. apply TF.
    rewrite H. intro. inv H0.
    + (* TB_default *)
      rewrite TB. left. eexists. split.
      * apply exec_Inop. rewrite (tunnel_function_unfold f tf pc). rewrite H. simpl. eauto. apply TF.
      * constructor; try assumption.
    + (* TB_nop *)
      simpl. right. repeat split. apply DEC.
      rewrite EQ. apply match_states_intro; assumption.
  - (* Iop *)
    exploit eval_operation_lessdef; try eassumption.
    apply reglist_lessdef. apply RS.
    intros (tv & EVAL & LD).
    left; eexists; split.
    + eapply exec_Iop with (v:=tv).
      assert ((fn_code tf) ! pc = Some (Iop op args res (branch_target f pc'))).
      rewrite (tunnel_function_unfold f tf pc); eauto.
      rewrite H. simpl. reflexivity.
      (* TODO: refaire ça joliment *)
      assert (target_bounds (branch_target f) (bound (branch_target f)) pc (fn_code f)! pc).
      apply (branch_target_bounds) with tf. apply TF.
      inv H2. rewrite TB. apply H1. rewrite H in H4. congruence.
      rewrite H in H4. congruence.
      rewrite <- EVAL. apply eval_operation_preserved. apply symbols_preserved.
    + apply match_states_intro; eauto. apply set_reg_lessdef. apply LD. apply RS.
  - (* Iload *)


Qed.


Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTL.semantics tprog).
Proof.
  eapply forward_simulation_opt.
  apply senv_preserved.
  apply transf_initial_states.
  apply transf_final_states.
  exact tunnel_step_correct.
Qed.

End PRESERVATION.