Removing the PseudoAsm IR

1 files changed, 29 insertions, 10 deletions

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) *)