restauring Coq compilation with STUBS

3 files changed, 189 insertions, 2 deletions

diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index bcd4495f..0e90cbf5 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -1,3 +1,50 @@
+(** Correctness proof for aarch64/Asmblock generation: main proof. 
+CURRENTLY A STUB !
+*)
+
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock IterList.
+Require Import PseudoAsmblockproof Asmblockgen.
+
+Module MB := Machblock.
+Module AB := Asmblock.
+
+Definition match_prog (p: MB.program) (tp: AB.program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. eapply match_transform_partial_program; eauto.
+Qed.
+
+Parameter next: MB.function -> Z -> Z.
+
+Section PRESERVATION.
+
+Lemma next_progress: forall (f:MB.function) (pos:Z), (pos < (next f pos))%Z.
+Admitted.
+
+Variable prog: Machblock.program.
+Variable tprog: Asmblock.program.
+Hypothesis TRANSF: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_bound_max_pos: forall fb f,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  (max_pos next f) <= Ptrofs.max_unsigned.
+Admitted.
+
+Lemma transf_program_correct:
+  forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics tprog).
+Admitted.
+
+End PRESERVATION.
+
+
 (* ORIGINAL aarch64/Asmgenproof file that needs to be adapted
 
 (* *********************************************************************)
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index f81f37d6..b0fec14b 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -16,11 +16,16 @@
 
 Require Import Recdef Coqlib Zwf Zbits.
 Require Import Errors AST Integers Floats Op.
-Require Import Locations Asmblock Asm.
+Require Import Locations Compopts.
+Require Import Mach Asm Asmblock Asmblockgen Machblockgen PseudoAsmblock PseudoAsmblockproof.
+
+
+Local Open Scope error_monad_scope.
 
 (** * Translation from Asmblock to assembly language 
-      Inspired from the KVX backend. *)
+      Inspired from the KVX backend (see kvx/Asm.v and kvx/Asmgen.v) *)
 
+Module Asmblock_TRANSF.
 (* STUB *)
 
 Definition transf_function (f: Asmblock.function) : res Asm.function :=
@@ -31,3 +36,11 @@ Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef :=
 
 Definition transf_program (p: Asmblock.program) : res Asm.program :=
   transform_partial_program transf_fundef p.
+
+End Asmblock_TRANSF.
+
+Definition transf_program (p: Mach.program) : res Asm.program :=
+  let mbp := Machblockgen.transf_program p in
+  do mbp' <- PseudoAsmblockproof.transf_program mbp;
+  do abp <- Asmblockgen.transf_program mbp';
+  Asmblock_TRANSF.transf_program abp.
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index e69de29b..b9f931c0 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -0,0 +1,127 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Justus Fasse       UGA, VERIMAG                   *)
+(*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*           Cyril Six          Kalray                         *)
+(*                                                             *)
+(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock.
+Require Machblockgenproof Asmblockgenproof.
+Require Import Asmgen.
+
+
+Module Asmblock_PRESERVATION.
+
+Import Asmblock_TRANSF.
+
+Definition match_prog (p: Asmblock.program) (tp: Asm.program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. eapply match_transform_partial_program; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variable prog: Asmblock.program.
+Variable tprog: Asm.program.
+Hypothesis TRANSF: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma transf_program_correct:
+  forward_simulation (Asmblock.semantics prog) (Asm.semantics tprog).
+Admitted. (* TODO *)
+
+End PRESERVATION.
+
+End Asmblock_PRESERVATION.
+
+
+Local Open Scope linking_scope.
+
+Definition block_passes :=
+      mkpass Machblockgenproof.match_prog
+  ::: mkpass PseudoAsmblockproof.match_prog
+  ::: mkpass Asmblockgenproof.match_prog
+  ::: mkpass Asmblock_PRESERVATION.match_prog
+  ::: pass_nil _.
+
+Definition match_prog := pass_match (compose_passes block_passes).
+
+Lemma transf_program_match:
+  forall p tp, Asmgen.transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros p tp H.
+  unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
+  inversion_clear H. apply bind_inversion in H1. destruct H1.
+  inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
+  unfold match_prog; simpl.
+  exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
+  exists x; split. apply PseudoAsmblockproof.transf_program_match; auto.
+  exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
+  exists tp; split. apply Asmblock_PRESERVATION.transf_program_match; auto. auto.
+Qed.
+
+(** Return Address Offset *)
+
+Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
+  Machblockgenproof.Mach_return_address_offset (PseudoAsmblockproof.rao Asmblockgenproof.next).
+
+Lemma return_address_exists:
+  forall f sg ros c, is_tail (Mach.Mcall sg ros :: c) f.(Mach.fn_code) ->
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros; eapply Machblockgenproof.Mach_return_address_exists; eauto.
+Admitted.
+
+Section PRESERVATION.
+
+Variable prog: Mach.program.
+Variable tprog: Asm.program.
+Hypothesis TRANSF: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Theorem transf_program_correct:
+  forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
+Proof.
+  unfold match_prog in TRANSF. simpl in TRANSF.
+  inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
+  eapply compose_forward_simulations.
+  { exploit Machblockgenproof.transf_program_correct; eauto. }
+  eapply compose_forward_simulations.
+  + apply PseudoAsmblockproof.transf_program_correct; eauto.
+    - intros; apply Asmblockgenproof.next_progress.
+    - intros; eapply Asmblockgenproof.functions_bound_max_pos; eauto.
+  + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+    apply Asmblock_PRESERVATION.transf_program_correct. eauto.
+Qed.
+
+End PRESERVATION.
+
+Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes).
+
+(*******************************************)
+(* Stub actually needed by driver/Compiler *)
+
+Module Asmgenproof0.
+
+Definition return_address_offset := return_address_offset.
+
+End Asmgenproof0.
+