Removing the PseudoAsm IR

7 files changed, 303 insertions, 46 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index f12e8922..5e41d96a 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -420,6 +420,22 @@ Fixpoint size_blocks (l: bblocks): Z :=
   end
   .
 
+Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0.
+Proof.
+  intros. destruct z; auto.
+  - contradict H. cbn. apply gt_irrefl.
+  - apply Zgt_pos_0.
+  - contradict H. cbn. apply gt_irrefl.
+Qed.
+
+Lemma size_positive (b:bblock): size b > 0.
+Proof.
+  unfold size. destruct b as [hd bdy ex cor]. cbn.
+  destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; cbn; omega);
+  unfold non_empty_bblockb in cor; simpl in cor.
+  inversion cor.
+Qed.
+
 Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index fbbf7507..d68cd7ac 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -160,6 +160,7 @@ Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity).
 (* NB: this notation helps the Coq typechecker to infer coercion [PArith] in [bcode] expressions *)
 (** Alignment check for symbols *)
 Notation "i ::bi k" := (cons (A:=basic) i k) (at level 49, right associativity).
+Notation "a @@ b" := (app a b) (at level 49, right associativity).
 
 (* The pop_bc and push_bc functions are used to adapt the output of some definitions
    in bblocks format and avoid some redefinitions. *)
@@ -1194,10 +1195,10 @@ Program Definition gen_bblocks (hd: list label) (c: bcode) (ctl: list instructio
 *)
 
 (* XXX: the simulation proof may be complex with this pattern. We may fix this later *)
-Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control) (k:bblocks): bblocks :=
+Program Definition cons_bblocks (ll: list label) (bdy: list basic) (ex: option control): bblocks :=
   match non_empty_bblockb bdy ex with
-  | true => {| header := ll; body:= bdy; exit := ex |}::k
-  | false => k
+  | true => {| header := ll; body:= bdy; exit := ex |} :: nil
+  | false => {| header := ll; body:= Pnop::nil; exit := None |} :: nil
   end.
 Obligation 1.
   rewrite <- Heq_anonymous. constructor.
@@ -1225,32 +1226,50 @@ Definition transl_exit (f: Machblock.function) (ext: option control_flow_inst) :
   | None => OK (nil, None)
   end.
 
-Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) (k:bblocks): res (list bblock) :=
+Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool) : res (list bblock) :=
   let stub := false in
   do (bdy, ex) <- transl_exit f fb.(Machblock.exit);
   do bdy' <- transl_basic_code f fb.(Machblock.body) ep bdy;
-  OK (cons_bblocks fb.(Machblock.header) bdy' ex k) 
+  OK (cons_bblocks fb.(Machblock.header) bdy' ex) 
   .
 
-Fixpoint transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=
+Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) :=
   match lmb with
   | nil => OK nil
   | mb :: lmb => 
+      do lb <- transl_block f mb (if Machblock.header mb then ep else false);
+      do lb' <- transl_blocks f lmb false;
+      OK (lb @@ lb')
+  end
+.
+
+(*   match lmb with
+  | nil => OK nil
+  | mb :: lmb => 
       do lb <- transl_blocks f lmb false;
       transl_block f mb (if Machblock.header mb then ep else false) lb
-  end.
+  end. *)
   (* OK (make_epilogue f ((Pret X0)::c nil))*)
 
-(* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *)
 Program Definition make_prologue (f:  Machblock.function) (k:bblocks) :=
-   Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
-   push_bc (storeptr_bc RA XSP f.(fn_retaddr_ofs) (pop_bc k)) k.
+  {| header := nil; body := Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::bi
+      storeptr_bc RA XSP f.(fn_retaddr_ofs) nil;
+      exit := None |} :: k.
+  
+(*    Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b
+   push_bc (storeptr_bc RA XSP f.(fn_retaddr_ofs) (pop_bc k)) k. *)
 
 Definition transl_function (f: Machblock.function) : res Asmblock.function :=
   do lb <- transl_blocks f f.(Machblock.fn_code) true;
   OK (mkfunction f.(Machblock.fn_sig)
         (make_prologue f lb)).
 
+Definition transf_function (f: Machblock.function) : res Asmblock.function :=
+  do tf <- transl_function f;
+  if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
+  then Error (msg "code size exceeded")
+  else OK tf.
+
 Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
   transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *)
 
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 41082772..bd96ff3b 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -5,8 +5,8 @@ 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.
+Require Import Op Locations Machblock Conventions Asmblock IterList.
+Require Import Asmblockgen Asmblockgenproof0.
 
 Module MB := Machblock.
 Module AB := Asmblock.
@@ -20,13 +20,8 @@ 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 lk: aarch64_linker.
 Variable prog: Machblock.program.
 Variable tprog: Asmblock.program.
@@ -38,15 +33,39 @@ Let tge := Genv.globalenv tprog.
 Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
   Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
 
-Lemma functions_bound_max_pos: forall fb f,
+(*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.
+Admitted.*)
+
+Lemma transf_function_no_overflow:
+  forall f tf,
+  transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned.
+Proof.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0.
+  omega.
+Qed.
 
+(** Existence of return addresses *)
+
+Lemma return_address_exists:
+  forall b f c, is_tail (b :: c) f.(MB.fn_code) ->
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros. eapply Asmblockgenproof0.return_address_exists; eauto.
+
+- intros. monadInv H0.
+  destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. monadInv EQ. simpl.
+  exists x; exists true; split; auto.
+  repeat constructor.
+- exact transf_function_no_overflow.
+Qed.
 
+Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := 
+  Asmblockgenproof0.return_address_offset.
 
 Lemma transf_program_correct:
-  forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics lk tprog).
+  forward_simulation (MB.semantics return_address_offset prog) (AB.semantics lk tprog).
 Admitted.
 
 End PRESERVATION.
diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
new file mode 100644
index 00000000..0187a494
--- /dev/null
+++ b/aarch64/Asmblockgenproof0.v
@@ -0,0 +1,214 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           Sylvain Boulmé     Grenoble-INP, 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.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+(** * "block" version of Asmgenproof0
+
+    This module is largely adapted from Asmgenproof0.v of the other backends
+    It needs to stand apart because of the block structure, and the distinction control/basic that there isn't in the other backends
+    It has similar definitions than Asmgenproof0, but adapted to this new structure *)
+
+Require Import Coqlib.
+Require Intv.
+Require Import AST.
+Require Import Errors.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Locations.
+Require Import Machblock.
+Require Import Asmblock.
+Require Import Asmblockgen.
+Require Import Conventions1.
+Require Import Axioms.
+Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
+Require Import Asmblockprops.
+
+Module MB:=Machblock.
+Module AB:=Asmblock.
+
+Inductive code_tail: Z -> bblocks -> bblocks -> Prop :=
+  | code_tail_0: forall c,
+      code_tail 0 c c
+  | code_tail_S: forall pos bi c1 c2,
+      code_tail pos c1 c2 ->
+      code_tail (pos + (size bi)) (bi :: c1) c2.
+      
+Lemma code_tail_pos:
+  forall pos c1 c2, code_tail pos c1 c2 -> pos >= 0.
+Proof.
+  induction 1. omega. generalize (size_positive bi); intros; omega.
+Qed.
+
+Lemma find_bblock_tail:
+  forall c1 bi c2 pos,
+  code_tail pos c1 (bi :: c2) ->
+  find_bblock pos c1 = Some bi.
+Proof.
+  induction c1; simpl; intros.
+  inversion H.  
+  destruct (zlt pos 0). generalize (code_tail_pos _ _ _ H); intro; omega.
+  destruct (zeq pos 0). subst pos.
+  inv H. auto. generalize (size_positive a) (code_tail_pos _ _ _ H4). intro; omega.
+  inv H. congruence. replace (pos0 + size a - size a) with pos0 by omega.
+  eauto.
+Qed.
+
+Local Hint Resolve code_tail_0 code_tail_S: core.
+
+Lemma code_tail_next:
+  forall fn ofs c0,
+  code_tail ofs fn c0 ->
+  forall bi c1, c0 = bi :: c1 -> code_tail (ofs + (size bi)) fn c1.
+Proof.
+  induction 1; intros.
+  - subst; eauto.
+  - replace (pos + size bi + size bi0) with ((pos + size bi0) + size bi); eauto.
+    omega.
+Qed.
+
+Lemma size_blocks_pos c: 0 <= size_blocks c.
+Proof.
+  induction c as [| a l ]; simpl; try omega.
+  generalize (size_positive a); omega.
+Qed.
+
+Remark code_tail_positive:
+  forall fn ofs c,
+  code_tail ofs fn c -> 0 <= ofs.
+Proof.
+  induction 1; intros; simpl.
+  - omega.
+  - generalize (size_positive bi). omega.
+Qed.
+
+Remark code_tail_size:
+  forall fn ofs c,
+  code_tail ofs fn c -> size_blocks fn = ofs + size_blocks c.
+Proof.
+  induction 1; intros; simpl; try omega.
+Qed.
+
+Remark code_tail_bounds fn ofs c:
+  code_tail ofs fn c -> 0 <= ofs <= size_blocks fn.
+Proof.
+  intro H; 
+  exploit code_tail_size; eauto.
+  generalize (code_tail_positive _ _ _ H), (size_blocks_pos c).
+  omega.
+Qed.
+
+Local Hint Resolve code_tail_next: core.
+
+Lemma code_tail_next_int:
+  forall fn ofs bi c,
+  size_blocks fn <= Ptrofs.max_unsigned ->
+  code_tail (Ptrofs.unsigned ofs) fn (bi :: c) ->
+  code_tail (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bi)))) fn c.
+Proof.
+  intros. 
+  exploit code_tail_size; eauto.
+  simpl; generalize (code_tail_positive _ _ _ H0), (size_positive bi), (size_blocks_pos c).
+  intros.
+  rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_repr.
+  - rewrite Ptrofs.unsigned_repr; eauto.
+    omega.
+  - rewrite Ptrofs.unsigned_repr; omega.
+Qed.
+
+(** Predictor for return addresses in generated Asm code.
+
+  The [return_address_offset] predicate defined here is used in the
+  semantics for Mach to determine the return addresses that are
+  stored in activation records. *)
+
+(** Consider a Mach function [f] and a sequence [c] of Mach instructions
+  representing the Mach code that remains to be executed after a
+  function call returns.  The predicate [return_address_offset f c ofs]
+  holds if [ofs] is the integer offset of the PPC instruction
+  following the call in the Asm code obtained by translating the
+  code of [f]. Graphically:
+<<
+     Mach function f    |--------- Mcall ---------|
+         Mach code c    |                |--------|
+                        |                 \        \
+                        |                  \        \
+                        |                   \        \
+     Asm code           |                    |--------|
+     Asm function       |------------- Pcall ---------|
+
+                        <-------- ofs ------->
+>>
+*)
+
+Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : Prop :=
+  forall tf  tc,
+  transf_function f = OK tf ->
+  transl_blocks f c false = OK tc ->
+  code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc.
+
+Lemma transl_blocks_tail:
+  forall f c1 c2, is_tail c1 c2 ->
+  forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 ->
+  exists tc1, exists ep1, transl_blocks f c1 ep1 = OK tc1 /\ is_tail tc1 tc2.
+Proof.
+  induction 1; simpl; intros.
+  exists tc2; exists ep2; split; auto with coqlib.
+  monadInv H0. exploit IHis_tail; eauto. intros (tc1 & ep1 & A & B).
+  exists tc1; exists ep1; split. auto.
+  eapply is_tail_trans with x0; eauto with coqlib.
+Qed.
+
+Lemma is_tail_code_tail:
+  forall c1 c2, is_tail c1 c2 -> exists ofs, code_tail ofs c2 c1.
+Proof.
+  induction 1; eauto.
+  destruct IHis_tail; eauto. 
+Qed.
+
+Section RETADDR_EXISTS.
+
+Hypothesis transf_function_inv:
+  forall f tf, transf_function f = OK tf ->
+  exists tc ep, transl_blocks f (Machblock.fn_code f) ep = OK tc /\ is_tail tc (fn_blocks tf).
+
+Hypothesis transf_function_len:
+  forall f tf, transf_function f = OK tf -> size_blocks (fn_blocks tf) <= Ptrofs.max_unsigned.
+
+
+Lemma return_address_exists:
+  forall b f c, is_tail (b :: c) f.(MB.fn_code) ->
+  exists ra, return_address_offset f c ra.
+Proof.
+  intros. destruct (transf_function f) as [tf|] eqn:TF.
+  + exploit transf_function_inv; eauto. intros (tc1 & ep1 & TR1 & TL1).
+    exploit transl_blocks_tail; eauto. intros (tc2 & ep2 & TR2 & TL2).
+    monadInv TR2.
+    assert (TL3: is_tail x0 (fn_blocks tf)).
+    { apply is_tail_trans with tc1; auto. 
+      apply is_tail_trans with (x++x0); auto. eapply is_tail_app.
+    }
+    exploit is_tail_code_tail. eexact TL3. intros [ofs CT].
+    exists (Ptrofs.repr ofs). red; intros.
+    rewrite Ptrofs.unsigned_repr. congruence.
+    exploit code_tail_bounds; eauto.
+    intros; apply transf_function_len in TF. omega.
+  + exists Ptrofs.zero; red; intros. congruence.
+Qed.
+
+End RETADDR_EXISTS.
\ No newline at end of file
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index f7ec07ae..cd9175cb 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -18,7 +18,7 @@
 Require Import Recdef Coqlib Zwf Zbits.
 Require Import Errors AST Integers Floats Op.
 Require Import Locations Compopts.
-Require Import Mach Asm Asmblock Asmblockgen Machblockgen PseudoAsmblock PseudoAsmblockproof PostpassScheduling.
+Require Import Mach Asm Asmblock Asmblockgen Machblockgen PostpassScheduling.
 
 
 Local Open Scope error_monad_scope.
@@ -450,7 +450,6 @@ 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';
+  do abp <- Asmblockgen.transf_program mbp;
   do abp' <- (time "PostpassScheduling total oracle+verification" PostpassScheduling.transf_program) abp;
   Asmblock_TRANSF.transf_program abp'.
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 793d94f9..690a54a2 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -18,7 +18,7 @@
 Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
-Require Import Op Locations Machblock Conventions PseudoAsmblock PseudoAsmblockproof Asm Asmblock.
+Require Import Op Locations Machblock Conventions Asm Asmblock.
 Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
 Require Import Asmgen.
 Require Import Axioms.
@@ -2281,7 +2281,6 @@ Local Open Scope linking_scope.
 
 Definition block_passes :=
       mkpass Machblockgenproof.match_prog
-  ::: mkpass PseudoAsmblockproof.match_prog
   ::: mkpass Asmblockgenproof.match_prog
   ::: mkpass PostpassSchedulingproof.match_prog
   ::: mkpass Asmblock_PRESERVATION.match_prog
@@ -2295,27 +2294,27 @@ 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. apply bind_inversion in H2. destruct H2. inversion_clear H.
+  inversion_clear H.
   unfold Compopts.time in *. 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 x1; split. apply PostpassSchedulingproof.transf_program_match; auto.
+  exists x; split. apply Asmblockgenproof.transf_program_match; auto.
+  exists x0; split. apply PostpassSchedulingproof.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).
+  Machblockgenproof.Mach_return_address_offset (Asmblockgenproof.return_address_offset).
 
 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.
+  intros; unfold return_address_offset; eapply Machblockgenproof.Mach_return_address_exists; eauto.
+  intros; eapply Asmblockgenproof.return_address_exists; eauto.
+Qed.
 
 Section PRESERVATION.
 
@@ -2329,28 +2328,19 @@ 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. inv H4. inv H.
+  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.
-    { intros.
-      unfold Genv.symbol_address.
-      erewrite <- PostpassSchedulingproof.symbols_preserved; eauto.
-      erewrite Asmblock_PRESERVATION.symbol_high_low; eauto.
-      reflexivity.
-     }
-  + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+  + apply Asmblockgenproof.transf_program_correct; eauto.
     { intros.
       unfold Genv.symbol_address.
       erewrite <- PostpassSchedulingproof.symbols_preserved; eauto.
       erewrite Asmblock_PRESERVATION.symbol_high_low; eauto.
       reflexivity.
     }
-    eapply compose_forward_simulations.
+  + eapply compose_forward_simulations.
     - apply PostpassSchedulingproof.transf_program_correct; eauto.
     - apply Asmblock_PRESERVATION.transf_program_correct; eauto.
 Qed.
diff --git a/configure b/configure
index 14c924d0..ae729e80 100755
--- a/configure
+++ b/configure
@@ -843,8 +843,8 @@ fi
 if [ "$arch" = "aarch64" ]; then # for aarch64 scheduling
 cat >> Makefile.config <<EOF
 ARCHDIRS=$arch
-BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v\\
-    Asmblock.v Asmblockgen.v Asmblockgenproof.v Asm.v Asmblockprops.v\\
+BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v \\
+    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof.v Asm.v Asmblockprops.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
     Asmblockdeps.v\\
     AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\