restauring Coq compilation with STUBS

1 files changed, 127 insertions, 0 deletions

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.
+