From 25595a7b34b70011dcb77aae277ee1cdb8920c60 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 28 May 2021 14:28:56 +0200
Subject: splitting BTL by introducing BTLmatchRTL

reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof
sharing is done in BTLmatchRTL
---
 scheduling/BTLtoRTLproof.v | 42 +++++-------------------------------------
 1 file changed, 5 insertions(+), 37 deletions(-)

(limited to 'scheduling/BTLtoRTLproof.v')

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 46f360c5..765f9cad 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -1,31 +1,12 @@
 Require Import Coqlib Maps.
 Require Import AST Integers Values Events Memory Globalenvs Smallstep.
-Require Import RTL Op Registers OptionMonad BTL.
+Require Import RTL Op Registers OptionMonad.
 
 Require Import Errors Linking BTLtoRTL.
 
 Require Import Linking.
 
-Record match_function dupmap f f': Prop := {
-  dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f');
-  dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f');
-  preserv_fnsig: fn_sig f = RTL.fn_sig f';
-  preserv_fnparams: fn_params f = RTL.fn_params f';
-  preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f'
-}.
-
-Inductive match_fundef: fundef -> RTL.fundef -> Prop :=
-  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
-  | match_External ef: match_fundef (External ef) (External ef).
-
-Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop :=
-  | match_stackframe_intro 
-      dupmap res f sp pc rs f' pc'
-      (TRANSF: match_function dupmap f f')
-      (DUPLIC: dupmap!pc = Some pc')
-      : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs).
-
-Inductive match_states: state -> RTL.state -> Prop :=
+Inductive match_states: BTL.state -> RTL.state -> Prop :=
   | match_states_intro 
       dupmap st f sp pc rs m st' f' pc'
       (STACKS: list_forall2 match_stackframes st st')
@@ -43,26 +24,13 @@ Inductive match_states: state -> RTL.state -> Prop :=
       : match_states (Returnstate st v m) (RTL.Returnstate st' v m)
    .
 
-Lemma verify_function_correct dupmap f f' tt:
-  verify_function dupmap f f' = OK tt ->
-  fn_sig f = RTL.fn_sig f' ->
-  fn_params f = RTL.fn_params f' ->
-  fn_stacksize f = RTL.fn_stacksize f' ->
-  match_function dupmap f f'.
-Proof.
-  unfold verify_function; intro VERIF. monadInv VERIF.
-  constructor; eauto.
-  - eapply verify_cfg_correct; eauto.
-  - eapply verify_is_copy_correct; eauto.
-Qed.
-
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
-Proof. Admitted. (*
+Proof.
   unfold transf_function; unfold bind. repeat autodestruct.
   intros H _ _ X. inversion X; subst; clear X.
   eexists; eapply verify_function_correct; simpl; eauto.
-                    Qed.*)
+Qed.
 
 Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
@@ -402,7 +370,7 @@ Proof.
 Qed.
 
 Theorem transf_program_correct_cfg:
-  forward_simulation (BTL.cfgsem prog) (RTL.semantics tprog).
+  forward_simulation (BTLmatchRTL.cfgsem prog) (RTL.semantics tprog).
 Proof.
   eapply forward_simulation_plus with match_states.
   - eapply senv_preserved.
-- 
cgit