From 6462da4e8f25ce5df951635828901ad0180e9958 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Wed, 20 Mar 2019 12:00:16 +0100
Subject: Integrating Asmvliw.v in the proof chain

---
 mppa_k1c/Asm.v                     |  6 +++---
 mppa_k1c/Asmvliw.v                 |  5 ++---
 mppa_k1c/PostpassSchedulingproof.v | 34 ++++++++++++++++++++++++----------
 3 files changed, 29 insertions(+), 16 deletions(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 31bc855d..0d4906b9 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -30,7 +30,7 @@ Require Import Smallstep.
 Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
-Require Import Asmblock.
+Require Import Asmvliw.
 Require Import Linking.
 Require Import Errors.
 
@@ -416,7 +416,7 @@ Definition program_proj (p: program) : Asmblock.program :=
 
 End RELSEM.
 
-Definition semantics (p: program) := Asmblock.semantics (program_proj p).
+Definition semantics (p: program) := Asmvliw.semantics (program_proj p).
 
 (** Determinacy of the [Asm] semantics. *)
 
@@ -547,7 +547,7 @@ Proof (Genv.senv_match TRANSF).
 
 
 Theorem transf_program_correct:
-  forward_simulation (Asmblock.semantics prog) (semantics tprog).
+  forward_simulation (Asmvliw.semantics prog) (semantics tprog).
 Proof.
   pose proof (match_program_transf prog tprog TRANSF) as TR.
   subst. unfold semantics. rewrite transf_program_proj.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 5b58118b..36c68acd 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -31,7 +31,8 @@ Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
-Require Import Asmblock.
+Require Export Asmblock.
+Require Import Sorting.Permutation.
 
 Local Open Scope asm.
 
@@ -236,8 +237,6 @@ Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m:
 Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
   parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs m.
 
-Require Import Sorting.Permutation.
-
 Definition parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
    exists bdy1 bdy2, Permutation (bdy1++bdy2) (body b) /\ 
       o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m with
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 7d6d9a7a..6fff3117 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -237,7 +237,7 @@ Proof.
   rewrite <- Zplus_mod. auto.
 Qed.
 
-Section PRESERVATION.
+Section PRESERVATION_ASMBLOCK.
 
 Variables prog tprog: program.
 Hypothesis TRANSL: match_prog prog tprog.
@@ -668,23 +668,37 @@ Proof.
   - apply transf_step_correct.
 Qed.
 
-(* TODO:
+End PRESERVATION_ASMBLOCK.
+
 Require Import Asmvliw.
 
-Theorem transf_program_correct: 
+Section PRESERVATION_ASMVLIW.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Theorem transf_program_correct_Asmvliw: 
   forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog).
 Proof.
-  eapply forward_simulation_one_one. (* FIXME *)
 Admitted.
 
-Theorem transf_program_correct: 
-  forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog).
-Proof.
-  eapply forward_simulation_compose. (* FIXME *)
-Admitted.
+End PRESERVATION_ASMVLIW.
 
-*)
+Section PRESERVATION.
 
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
 
+Theorem transf_program_correct: 
+  forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog).
+Proof.
+  eapply compose_forward_simulations.
+  eapply transf_program_correct_Asmblock; eauto.
+  eapply transf_program_correct_Asmvliw; eauto.
+Qed.
 
 End PRESERVATION.
-- 
cgit