Add RTLTunnelingproof.v

1 files changed, 170 insertions, 0 deletions

diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v
new file mode 100644
index 00000000..57f14b9f
--- /dev/null
+++ b/backend/RTLTunnelingproof.v
@@ -0,0 +1,170 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 Events Globalenvs Smallstep.
+Require Import Op Locations RTL.
+Require Import RTLTunneling.
+Require Import Conventions1.
+
+Local Open Scope nat.
+
+(** 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` ?? *)
+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). eauto.
+  intros (cu & tf & A & B & C).
+  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_transf_partial TRANSL); eauto.
+Qed.
+
+Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  rewrite (Genv.find_symbol_match TRANSL). auto.
+Qed.
+
+Lemma sig_preserved:
+  forall f tf, tunnel_fundef f = OK tf -> funsig tf = funsig f.
+Proof.
+  intros. destruct f.
+  - simpl in H. monadInv H. (* rq: c'est une tactique maison... *)
+    unfold tunnel_function in EQ.
+    destruct (check_included _ _) as [_|] in EQ; try congruence.
+    monadInv EQ. auto.
+  - simpl in H. monadInv H. auto.
+Qed.
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof.
+  eapply (Genv.senv_match TRANSL). (* Il y a déjà une preuve, 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).
+
+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.
+  exploit function_ptr_translated; eauto.
+  intro Htf. destruct Htf as (tf & Htf & Hf).
+  exists (Callstate nil tf nil m0). split.
+  - econstructor.
+    + apply (Genv.init_mem_transf_partial TRANSL). auto.
+    + rewrite (match_program_main TRANSL).
+      rewrite symbols_preserved. eauto.
+    + apply Htf.
+    + rewrite <- H3. apply sig_preserved. apply Hf.
+  - constructor.
+    + constructor.
+    + apply Hf.
+    + constructor.
+    + 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.
+  intros s1 s2 r HM H1. inv H1. inv HM. inv STK. inv VAL. constructor.
+Qed.
+
+(* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *)
+
+(*
+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.
+  apply tunnel_step_correct.
+Qed.
+*)
+
+End PRESERVATION.