From deac4407cacb45efa56adf912bd9db32235984f5 Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Fri, 4 Jun 2021 17:49:38 +0200 Subject: Add RTLTunnelingproof.v --- Makefile | 2 +- backend/RTLTunnelingproof.v | 170 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 171 insertions(+), 1 deletion(-) create mode 100644 backend/RTLTunnelingproof.v diff --git a/Makefile b/Makefile index 0556a93c..4900b165 100644 --- a/Makefile +++ b/Makefile @@ -144,7 +144,7 @@ BACKEND=\ Allnontrap.v Allnontrapproof.v \ Allocation.v Allocationproof.v \ Tunneling.v Tunnelingproof.v \ - RTLTunneling.v \ + RTLTunneling.v RTLTunnelingproof.v \ Linear.v Lineartyping.v \ Linearize.v Linearizeproof.v \ CleanupLabels.v CleanupLabelsproof.v \ 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. -- cgit