aarch64 compiles again (but ccomp generates incorrect assembly)

1 files changed, 74 insertions, 6 deletions

diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v
index 83f2b96b..66db0f5f 100644
--- a/aarch64/Asmblockgen.v
+++ b/aarch64/Asmblockgen.v
@@ -3,7 +3,7 @@
 (*             The Compcert verified compiler                  *)
 (*                                                             *)
 (*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
-(*           Justus Fasse       UGA, VERIMAG                   *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
 (*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
 (*           David Monniaux     CNRS, VERIMAG                  *)
 (*           Cyril Six          Kalray                         *)
@@ -19,14 +19,82 @@
 
 Require Import Recdef Coqlib Zwf Zbits.
 Require Import Errors AST Integers Floats Op.
-Require Import Locations Machblock Asmblock.
+Require Import Locations Machblock Asm Asmblock.
 
-(* STUB *)
-Definition transf_function (f: Machblock.function) : res Asmblock.function :=
-  Error (msg "Asmblockgen not yet implmented").
+Local Open Scope string_scope.
+Local Open Scope list_scope.
+Local Open Scope error_monad_scope.
+
+Program Definition single_basic (bi: basic): bblock :=
+  {| header := nil; body:= bi::nil; exit := None |}.
+
+(* insert [bi] at the head of [k] *)
+Program Definition insert_basic (bi: basic) (k:bblocks): bblocks :=
+  match k with
+  | bb::k' =>
+    match bb.(header) with
+    | nil => {| header := nil; body := bi :: (body bb); exit := exit bb |}::k'
+    | _ => (single_basic bi)::k
+    end
+  | _ => (single_basic bi)::k
+  end.
+
+Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity).
+
+(* insert [ctl] at the head of [k] *)
+Program Definition insert_ctl (ctl: control) (k:bblocks): bblocks :=
+  {| header := nil; body := nil; exit := Some ctl |}::k.
+
+Notation "ctl ::c k" := (insert_ctl ctl k) (at level 49, right associativity).
+
+
+(** Alignment check for symbols *)
+
+Parameter symbol_is_aligned : ident -> Z -> bool.
+(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)
+
+(***************************************************************************************)
+(* STUB inspired from kvx/Asmblockgen.v and the reference aarch64/Asmgen.v (see below) *)
+
+Definition indexed_memory_access (insn: addressing -> basic)
+                                 (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bblocks) : bblocks :=
+  let ofs := Ptrofs.to_int64 ofs in
+  insn (ADimm base ofs) ::b k. (* STUB: change me ! See Asmgen below *)
+
+
+Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks :=
+  indexed_memory_access (PLoad Pldrx dst) 8 base ofs k.
+
+Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bblocks): bblocks :=
+  indexed_memory_access (PStore Pstrx src) 8 base ofs k.
+
+(** Function epilogue *)
+
+Definition make_epilogue (f: Machblock.function) (k: bblocks) : bblocks :=
+  (* FIXME
+     Cannot be used because memcpy destroys X30;
+     issue being discussed with X. Leroy *)
+  (* if is_leaf_function f
+  then Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k
+  else*) loadptr XSP f.(fn_retaddr_ofs) RA
+         (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::b k).
+
+
+Program Definition transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks :=
+  OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *)
+
+(* 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
+   storeptr RA XSP f.(fn_retaddr_ofs) 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_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
-  transf_partial_fundef transf_function f.
+  transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *)
 
 Definition transf_program (p: Machblock.program) : res Asmblock.program :=
   transform_partial_program transf_fundef p.