From 37ad0670e1dc02c47b4987c16602aadb462c44c2 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Fri, 23 Oct 2020 01:53:05 +0200
Subject: aarch64 compiles again (but ccomp generates incorrect assembly)

---
 aarch64/Asm.v               | 539 +++++++++++++++++++++++++++++++++++++++++++-
 aarch64/Asmblock.v          | 533 +------------------------------------------
 aarch64/Asmblockgen.v       |  80 ++++++-
 aarch64/Asmexpand.ml        | 102 ++++-----
 aarch64/Asmgen.v            |  10 +-
 aarch64/Asmgenproof.v       |  17 +-
 aarch64/OrigAsmgen.ml       | 282 +++++++++++++++++++++++
 aarch64/TargetPrinter.ml    |   8 +-
 aarch64/extractionMachdep.v |   2 +-
 extraction/extraction.v     |   4 +-
 10 files changed, 964 insertions(+), 613 deletions(-)
 create mode 100644 aarch64/OrigAsmgen.ml

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 4de1a9d0..22ab0222 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -12,15 +12,10 @@
 
 (** Abstract syntax and semantics for AArch64 assembly language 
 
-
-W.r.t Asmblock, this is a "flat" syntax and semantics of "Aarch64" assembly:
+W.r.t Asmblock, this is a "flat" syntax and semantics of "aarch64" assembly:
   - without the basic block structure
   - without the hierarchy of instructions.
 
-
-TODO: with respect to original file, remove parts of the syntax/semantics 
-that have been already defined in Asmblock.
-
 *)
 
 Require Import Coqlib Zbits Maps.
@@ -28,10 +23,152 @@ Require Import AST Integers Floats.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Locations Conventions.
 Require Stacklayout.
-Require Import OptionMonad Asmblock.
+Require Import OptionMonad.
 
 (** * Abstract syntax *)
 
+(** Integer registers, floating-point registers. *)
+
+(** In assembly files, [Xn] denotes the full 64-bit register
+    and [Wn] the low 32 bits of [Xn]. *)
+
+Inductive ireg: Type :=
+  | X0  | X1  | X2  | X3  | X4  | X5  |  X6  | X7
+  | X8  | X9  | X10 | X11 | X12 | X13 |  X14 | X15
+  | X16 | X17 | X18 | X19 | X20 | X21 |  X22 | X23
+  | X24 | X25 | X26 | X27 | X28 | X29 |  X30.
+
+Inductive ireg0: Type :=
+  | RR0 (r: ireg) | XZR.
+
+Inductive iregsp: Type :=
+  | RR1 (r: ireg) | XSP.
+
+Coercion RR0: ireg >-> ireg0.
+Coercion RR1: ireg >-> iregsp.
+
+Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+Lemma iregsp_eq: forall (x y: iregsp), {x=y} + {x<>y}.
+Proof. decide equality; apply ireg_eq. Defined.
+
+(** In assembly files, [Dn] denotes the low 64-bit of a vector register,
+    and [Sn] the low 32 bits. *)
+
+Inductive freg: Type :=
+  | D0  | D1  | D2  | D3  | D4  | D5  |  D6  | D7
+  | D8  | D9  | D10 | D11 | D12 | D13 |  D14 | D15
+  | D16 | D17 | D18 | D19 | D20 | D21 |  D22 | D23
+  | D24 | D25 | D26 | D27 | D28 | D29 |  D30 | D31.
+
+Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+(** Bits in the condition register. *)
+
+Inductive crbit: Type :=
+  | CN: crbit    (**r negative *)
+  | CZ: crbit    (**r zero *)
+  | CC: crbit    (**r carry *)
+  | CV: crbit.   (**r overflow *)
+
+Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
+Inductive dreg : Type :=
+  | IR': iregsp -> dreg  (**r 64- or 32-bit integer registers *)
+  | FR': freg -> dreg.   (**r double- or single-precision float registers *)
+
+(** We model the following registers of the ARM architecture. *)
+
+Inductive preg: Type :=
+  | DR: dreg -> preg     (** see dreg **)
+  | CR: crbit -> preg    (**r bits in the condition register *)
+  | PC: preg.            (**r program counter *)
+
+(* XXX: ireg no longer coerces to preg *)
+Coercion IR': iregsp >-> dreg.
+Coercion FR': freg >-> dreg.
+Coercion DR: dreg >-> preg.
+Definition SP:preg := XSP.
+Coercion CR: crbit >-> preg.
+
+Lemma dreg_eq: forall (x y: dreg), {x=y} + {x<>y}.
+Proof. decide equality. apply iregsp_eq. apply freg_eq. Defined.
+
+Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
+Proof. decide equality. apply dreg_eq. apply crbit_eq. Defined.
+
+Module PregEq.
+  Definition t := preg.
+  Definition eq := preg_eq.
+End PregEq.
+
+Module Pregmap := EMap(PregEq).
+
+Definition preg_of_iregsp (r: iregsp) : preg :=
+  match r with RR1 r => IR' r | XSP => SP end.
+
+(** Conventional name for return address ([RA]) *)
+
+Notation "'RA'" := X30 (only parsing) : asm.
+
+(** The instruction set.  Most instructions correspond exactly to
+  actual AArch64 instructions. See the ARM reference manuals for more
+  details.  Some instructions, described below, are
+  pseudo-instructions: they expand to canned instruction sequences
+  during the printing of the assembly code.  *)
+
+Definition label := positive.
+
+Inductive isize: Type :=
+  | W                                                (**r 32-bit integer operation *)
+  | X.                                               (**r 64-bit integer operation *)
+
+Inductive fsize: Type :=
+  | S                                                (**r 32-bit, single-precision FP operation *)
+  | D.                                               (**r 64-bit, double-precision FP operation *)
+
+Inductive testcond : Type :=
+  | TCeq: testcond    (**r equal *)
+  | TCne: testcond    (**r not equal *)
+  | TChs: testcond    (**r unsigned higher or same *)
+  | TClo: testcond    (**r unsigned lower *)
+  | TCmi: testcond    (**r negative *)
+  | TCpl: testcond    (**r positive *)
+  | TChi: testcond    (**r unsigned higher *)
+  | TCls: testcond    (**r unsigned lower or same *)
+  | TCge: testcond    (**r signed greater or equal *)
+  | TClt: testcond    (**r signed less than *)
+  | TCgt: testcond    (**r signed greater *)
+  | TCle: testcond.   (**r signed less than or equal *)
+
+Inductive addressing: Type :=
+  | ADimm (base: iregsp) (n: int64)                  (**r base plus immediate offset *)
+  | ADreg (base: iregsp) (r: ireg)                   (**r base plus reg *)
+  | ADlsl (base: iregsp) (r: ireg) (n: int)          (**r base plus reg LSL n *)
+  | ADsxt (base: iregsp) (r: ireg) (n: int)          (**r base plus SIGN-EXT(reg) LSL n *)
+  | ADuxt (base: iregsp) (r: ireg) (n: int)          (**r base plus ZERO-EXT(reg) LSL n *)
+  | ADadr (base: iregsp) (id: ident) (ofs: ptrofs)   (**r base plus low address of [id + ofs] *)
+  | ADpostincr (base: iregsp) (n: int64).            (**r base plus offset; base is updated after *)
+
+Inductive shift_op: Type :=
+  | SOnone
+  | SOlsl (n: int)
+  | SOlsr (n: int)
+  | SOasr (n: int)
+  | SOror (n: int).
+
+Inductive extend_op: Type :=
+  | EOsxtb (n: int)
+  | EOsxth (n: int)
+  | EOsxtw (n: int)
+  | EOuxtb (n: int)
+  | EOuxth (n: int)
+  | EOuxtw (n: int)
+  | EOuxtx (n: int).
+
 Inductive instruction: Type :=
   (** Branches *)
   | Pb (lbl: label)                                                   (**r branch *)
@@ -209,9 +346,389 @@ Axiom symbol_high_low:
 
 (** * Operational semantics *)
 
-Section RELSEM.
 
-Variable ge: genv.
+(** The semantics operates over a single mapping from registers
+  (type [preg]) to values.  We maintain (but do not enforce)
+  the convention that integer registers are mapped to values of
+  type [Tint], float registers to values of type [Tfloat],
+  and condition bits to either [Vzero] or [Vone]. *)
+
+Definition regset := Pregmap.t val.
+
+(** The value of an [ireg0] is either the value of the integer register,
+    or 0. *)
+
+Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val :=
+  match r with RR0 r => rs (IR' r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end.
+
+(** Concise notations for accessing and updating the values of registers. *)
+
+Notation "a # b" := (a b) (at level 1, only parsing) : asm.
+Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
+Notation "a ## b" := (ir0 W a b) (at level 1, only parsing) : asm.
+Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm.
+
+Open Scope asm.
+
+(** Undefining some registers *)
+
+Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
+  match l with
+  | nil => rs
+  | r :: l' => undef_regs l' (rs#r <- Vundef)
+  end.
+
+(** Undefining the condition codes *)
+
+Definition undef_flags (rs: regset) : regset :=
+  fun r => match r with CR _ => Vundef | _ => rs r end.
+
+(** Assigning a register pair *)
+
+Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
+  match p with
+  | One r => rs#r <- v
+  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
+  end.
+
+(** Assigning the result of a builtin *)
+
+Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
+  match res with
+  | BR r => rs#r <- v
+  | BR_none => rs
+  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  end.
+
+(** The semantics is purely small-step and defined as a function
+  from the current state (a register set + a memory state)
+  to either [Next rs' m'] where [rs'] and [m'] are the updated register
+  set and memory state after execution of the instruction at [rs#PC],
+  or [Stuck] if the processor is stuck. *)
+
+Record state: Type := State { _rs: regset; _m: mem }.
+Definition outcome := option state.
+Definition Next rs m: outcome := Some (State rs m).
+Definition Stuck: outcome := None.
+
+
+(* a few lemma on comparisons of unsigned (e.g. pointers)
+
+TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!)
+*)
+
+Definition Val_cmpu_bool cmp v1 v2: option bool :=
+  Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
+
+Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
+   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
+   -> (Val_cmpu_bool cmp v1 v2) = Some b.
+Proof.
+  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
+
+Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
+   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
+               (Val_cmpu cmp v1 v2).
+Proof.
+  unfold Val.cmpu, Val_cmpu.
+  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
+  destruct ob; simpl.
+  - erewrite Val_cmpu_bool_correct; eauto.
+    econstructor.
+  - econstructor.
+Qed.
+
+Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
+ := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).
+
+Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
+   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
+   -> (Val_cmplu_bool cmp v1 v2) = Some b.
+Proof.
+  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
+Qed.
+
+Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
+
+Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
+   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
+               (Val_cmplu cmp v1 v2).
+Proof.
+  unfold Val.cmplu, Val_cmplu.
+  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
+  destruct ob as [b|]; simpl.
+  - erewrite Val_cmplu_bool_correct; eauto.
+    simpl. econstructor.
+  - econstructor.
+Qed.
+
+(** Testing a condition *)
+
+Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
+  match c with
+  | TCeq =>                             (**r equal *)
+      match rs#CZ with
+      | Vint n => Some (Int.eq n Int.one)
+      | _ => None
+      end
+  | TCne =>                             (**r not equal *)
+      match rs#CZ with
+      | Vint n => Some (Int.eq n Int.zero)
+      | _ => None
+      end
+  | TClo =>                             (**r unsigned less than  *)
+      match rs#CC with
+      | Vint n => Some (Int.eq n Int.zero)
+      | _ => None
+      end
+  | TCls =>                             (**r unsigned less or equal *)
+      match rs#CC, rs#CZ with
+      | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one)
+      | _, _ => None
+      end
+  | TChs =>                             (**r unsigned greater or equal *)
+      match rs#CC with
+      | Vint n => Some (Int.eq n Int.one)
+      | _ => None
+      end
+  | TChi =>                             (**r unsigned greater *)
+      match rs#CC, rs#CZ with
+      | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero)
+      | _, _ => None
+      end
+  | TClt =>                             (**r signed less than *)
+      match rs#CV, rs#CN with
+      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one)
+      | _, _ => None
+      end
+  | TCle =>                             (**r signed less or equal *)
+      match rs#CV, rs#CN, rs#CZ with
+      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one)
+      | _, _, _ => None
+      end
+  | TCge =>                             (**r signed greater or equal *)
+      match rs#CV, rs#CN with
+      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero)
+      | _, _ => None
+      end
+  | TCgt =>                             (**r signed greater *)
+      match rs#CV, rs#CN, rs#CZ with
+      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero)
+      | _, _, _ => None
+      end
+  | TCpl =>                             (**r positive *)
+      match rs#CN with
+      | Vint n => Some (Int.eq n Int.zero)
+      | _ => None
+      end
+  | TCmi =>                             (**r negative *)
+      match rs#CN with
+      | Vint n => Some (Int.eq n Int.one)
+      | _ => None
+      end
+  end.
+
+(** Integer "is zero?" test *)
+
+Definition eval_testzero (sz: isize) (v: val): option bool :=
+  match sz with
+  | W => Val_cmpu_bool Ceq v (Vint Int.zero)
+  | X => Val_cmplu_bool Ceq v (Vlong Int64.zero)
+  end.
+
+(** Integer "bit is set?" test *)
+
+Definition eval_testbit (sz: isize) (v: val) (n: int): option bool :=
+  match sz with
+  | W => Val.cmp_bool Cne (Val.and v (Vint (Int.shl Int.one n))) (Vint Int.zero)
+  | X => Val.cmpl_bool Cne (Val.andl v (Vlong (Int64.shl' Int64.one n))) (Vlong Int64.zero)
+  end.
+
+
+(** Comparisons *)
+
+Definition compare_int (rs: regset) (v1 v2: val) :=
+  rs#CN <- (Val.negative (Val.sub v1 v2))
+    #CZ <- (Val_cmpu Ceq v1 v2)
+    #CC <- (Val_cmpu Cge v1 v2)
+    #CV <- (Val.sub_overflow v1 v2).
+
+Definition compare_long (rs: regset) (v1 v2: val) :=
+  rs#CN <- (Val.negativel (Val.subl v1 v2))
+    #CZ <- (Val_cmplu Ceq v1 v2)
+    #CC <- (Val_cmplu Cge v1 v2)
+    #CV <- (Val.subl_overflow v1 v2).
+
+(** Semantics of [fcmp] instructions:
+<<
+==	N=0 Z=1 C=1 V=0
+<	N=1 Z=0 C=0 V=0
+>	N=0 Z=0 C=1 V=0
+unord	N=0 Z=0 C=1 V=1
+>>
+*)
+
+Definition compare_float (rs: regset) (v1 v2: val) :=
+  match v1, v2 with
+  | Vfloat f1, Vfloat f2 =>
+      rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2))
+        #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2))
+        #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2)))
+        #CV <- (Val.of_bool (negb (Float.ordered f1 f2)))
+  | _, _ =>
+      rs#CN <- Vundef
+        #CZ <- Vundef
+        #CC <- Vundef
+        #CV <- Vundef
+  end.
+
+Definition compare_single (rs: regset) (v1 v2: val) :=
+  match v1, v2 with
+  | Vsingle f1, Vsingle f2 =>
+      rs#CN <- (Val.of_bool (Float32.cmp Clt f1 f2))
+        #CZ <- (Val.of_bool (Float32.cmp Ceq f1 f2))
+        #CC <- (Val.of_bool (negb (Float32.cmp Clt f1 f2)))
+        #CV <- (Val.of_bool (negb (Float32.ordered f1 f2)))
+  | _, _ =>
+      rs#CN <- Vundef
+        #CZ <- Vundef
+        #CC <- Vundef
+        #CV <- Vundef
+  end.
+
+(** Insertion of bits into an integer *)
+
+Definition insert_in_int (x: val) (y: Z) (pos: Z) (len: Z) : val :=
+  match x with
+  | Vint n => Vint (Int.repr (Zinsert (Int.unsigned n) y pos len))
+  | _ => Vundef
+  end.
+
+Definition insert_in_long (x: val) (y: Z) (pos: Z) (len: Z) : val :=
+  match x with
+  | Vlong n => Vlong (Int64.repr (Zinsert (Int64.unsigned n) y pos len))
+  | _ => Vundef
+  end.
+
+(** Evaluation of shifted operands *)
+
+Definition eval_shift_op_int (v: val) (s: shift_op): val :=
+  match s with
+  | SOnone => v
+  | SOlsl n => Val.shl v (Vint n)
+  | SOlsr n => Val.shru v (Vint n)
+  | SOasr n => Val.shr v (Vint n)
+  | SOror n => Val.ror v (Vint n)
+  end.
+
+Definition eval_shift_op_long (v: val) (s: shift_op): val :=
+  match s with
+  | SOnone => v
+  | SOlsl n => Val.shll v (Vint n)
+  | SOlsr n => Val.shrlu v (Vint n)
+  | SOasr n => Val.shrl v (Vint n)
+  | SOror n => Val.rorl v (Vint n)
+  end.
+
+(** Evaluation of sign- or zero- extended operands *)
+
+Definition eval_extend (v: val) (x: extend_op): val :=
+  match x with
+  | EOsxtb n => Val.shll (Val.longofint (Val.sign_ext 8 v)) (Vint n)
+  | EOsxth n => Val.shll (Val.longofint (Val.sign_ext 16 v)) (Vint n)
+  | EOsxtw n => Val.shll (Val.longofint v) (Vint n)
+  | EOuxtb n => Val.shll (Val.longofintu (Val.zero_ext 8 v)) (Vint n)
+  | EOuxth n => Val.shll (Val.longofintu (Val.zero_ext 16 v)) (Vint n)
+  | EOuxtw n => Val.shll (Val.longofintu v) (Vint n)
+  | EOuxtx n => Val.shll v (Vint n)
+  end.
+
+(** Bit-level conversion from integers to FP numbers *)
+
+Definition float32_of_bits (v: val): val :=
+  match v with
+  | Vint n => Vsingle (Float32.of_bits n)
+  | _ => Vundef
+  end.
+
+Definition float64_of_bits (v: val): val :=
+  match v with
+  | Vlong n => Vfloat (Float.of_bits n)
+  | _ => Vundef
+  end.
+
+
+(** Translation of the LTL/Linear/Mach view of machine registers
+  to the AArch64 view.  Note that no LTL register maps to [X16],
+  [X18], nor [X30].
+  [X18] is reserved as the platform register and never used by the
+  code generated by CompCert.
+  [X30] is used for the return address, and can also be used as temporary.
+  [X16] can be used as temporary. *)
+
+Definition dreg_of (r: mreg) : dreg :=
+  match r with
+  | R0 => X0   | R1 => X1   | R2 => X2   | R3 => X3
+  | R4 => X4   | R5 => X5   | R6 => X6   | R7 => X7
+  | R8 => X8   | R9 => X9   | R10 => X10 | R11 => X11
+  | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15
+  | R17 => X17 | R19 => X19
+  | R20 => X20 | R21 => X21 | R22 => X22 | R23 => X23
+  | R24 => X24 | R25 => X25 | R26 => X26 | R27 => X27
+  | R28 => X28 | R29 => X29
+  | F0 => D0   | F1 => D1   | F2 => D2   | F3 => D3
+  | F4 => D4   | F5 => D5   | F6 => D6   | F7 => D7
+  | F8 => D8   | F9 => D9   | F10 => D10 | F11 => D11
+  | F12 => D12 | F13 => D13 | F14 => D14 | F15 => D15
+  | F16 => D16 | F17 => D17 | F18 => D18 | F19 => D19
+  | F20 => D20 | F21 => D21 | F22 => D22 | F23 => D23
+  | F24 => D24 | F25 => D25 | F26 => D26 | F27 => D27
+  | F28 => D28 | F29 => D29 | F30 => D30 | F31 => D31
+  end.
+
+Definition preg_of (r: mreg) : preg :=
+  dreg_of r.
+
+(** Undefine all registers except SP and callee-save registers *)
+
+Definition undef_caller_save_regs (rs: regset) : regset :=
+  fun r =>
+    if preg_eq r SP
+    || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs))
+    then rs r
+    else Vundef.
+
+(** Extract the values of the arguments of an external call.
+    We exploit the calling conventions from module [Conventions], except that
+    we use AArch64 registers instead of locations. *)
+
+Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
+  | extcall_arg_reg: forall r,
+      extcall_arg rs m (R r) (rs (preg_of r))
+  | extcall_arg_stack: forall ofs ty bofs v,
+      bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
+      Mem.loadv (chunk_of_type ty) m
+                (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v ->
+      extcall_arg rs m (Locations.S Outgoing ofs ty) v.
+
+Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
+  | extcall_arg_one: forall l v,
+      extcall_arg rs m l v ->
+      extcall_arg_pair rs m (One l) v
+  | extcall_arg_twolong: forall hi lo vhi vlo,
+      extcall_arg rs m hi vhi ->
+      extcall_arg rs m lo vlo ->
+      extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).
+
+Definition extcall_arguments
+    (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
+  list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
+
+Definition loc_external_result (sg: signature) : rpair preg :=
+  map_rpair preg_of (loc_result sg).
 
 (** Looking up instructions in a code sequence by position. *)
 
@@ -256,6 +773,10 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
     end
   end.
 
+Section RELSEM.
+
+Variable ge: genv.
+
 (** Evaluating an addressing mode *)
 
 Definition eval_addressing (a: addressing) (rs: regset): val :=
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 67ad2aa5..96162f9e 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -35,151 +35,11 @@ Require Import AST Integers Floats.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Locations Conventions.
 Require Stacklayout.
-Require Import OptionMonad.
+Require Import OptionMonad Asm.
 
-(** * Abstract syntax *)
-
-(** Integer registers, floating-point registers. *)
-
-(** In assembly files, [Xn] denotes the full 64-bit register
-    and [Wn] the low 32 bits of [Xn]. *)
-
-Inductive ireg: Type :=
-  | X0  | X1  | X2  | X3  | X4  | X5  |  X6  | X7
-  | X8  | X9  | X10 | X11 | X12 | X13 |  X14 | X15
-  | X16 | X17 | X18 | X19 | X20 | X21 |  X22 | X23
-  | X24 | X25 | X26 | X27 | X28 | X29 |  X30.
-
-Inductive ireg0: Type :=
-  | RR0 (r: ireg) | XZR.
-
-Inductive iregsp: Type :=
-  | RR1 (r: ireg) | XSP.
-
-Coercion RR0: ireg >-> ireg0.
-Coercion RR1: ireg >-> iregsp.
-
-Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}.
-Proof. decide equality. Defined.
-
-Lemma iregsp_eq: forall (x y: iregsp), {x=y} + {x<>y}.
-Proof. decide equality; apply ireg_eq. Defined.
-
-(** In assembly files, [Dn] denotes the low 64-bit of a vector register,
-    and [Sn] the low 32 bits. *)
+Local Open Scope option_monad_scope.
 
-Inductive freg: Type :=
-  | D0  | D1  | D2  | D3  | D4  | D5  |  D6  | D7
-  | D8  | D9  | D10 | D11 | D12 | D13 |  D14 | D15
-  | D16 | D17 | D18 | D19 | D20 | D21 |  D22 | D23
-  | D24 | D25 | D26 | D27 | D28 | D29 |  D30 | D31.
-
-Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}.
-Proof. decide equality. Defined.
-
-(** Bits in the condition register. *)
-
-Inductive crbit: Type :=
-  | CN: crbit    (**r negative *)
-  | CZ: crbit    (**r zero *)
-  | CC: crbit    (**r carry *)
-  | CV: crbit.   (**r overflow *)
-
-Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}.
-Proof. decide equality. Defined.
-
-Inductive dreg : Type :=
-  | IR': iregsp -> dreg  (**r 64- or 32-bit integer registers *)
-  | FR': freg -> dreg.   (**r double- or single-precision float registers *)
-
-(** We model the following registers of the ARM architecture. *)
-
-Inductive preg: Type :=
-  | DR: dreg -> preg     (** see dreg **)
-  | CR: crbit -> preg    (**r bits in the condition register *)
-  | PC: preg.            (**r program counter *)
-
-(* XXX: ireg no longer coerces to preg *)
-Coercion IR': iregsp >-> dreg.
-Coercion FR': freg >-> dreg.
-Coercion DR: dreg >-> preg.
-Definition SP:preg := XSP.
-Coercion CR: crbit >-> preg.
-
-Lemma dreg_eq: forall (x y: dreg), {x=y} + {x<>y}.
-Proof. decide equality. apply iregsp_eq. apply freg_eq. Defined.
-
-Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply dreg_eq. apply crbit_eq. Defined.
-
-Module PregEq.
-  Definition t := preg.
-  Definition eq := preg_eq.
-End PregEq.
-
-Module Pregmap := EMap(PregEq).
-
-Definition preg_of_iregsp (r: iregsp) : preg :=
-  match r with RR1 r => IR' r | XSP => SP end.
-
-(** Conventional name for return address ([RA]) *)
-
-Notation "'RA'" := X30 (only parsing) : asm.
-
-(** The instruction set.  Most instructions correspond exactly to
-  actual AArch64 instructions. See the ARM reference manuals for more
-  details.  Some instructions, described below, are
-  pseudo-instructions: they expand to canned instruction sequences
-  during the printing of the assembly code.  *)
-
-Definition label := positive.
-
-Inductive isize: Type :=
-  | W                                                (**r 32-bit integer operation *)
-  | X.                                               (**r 64-bit integer operation *)
-
-Inductive fsize: Type :=
-  | S                                                (**r 32-bit, single-precision FP operation *)
-  | D.                                               (**r 64-bit, double-precision FP operation *)
-
-Inductive testcond : Type :=
-  | TCeq: testcond    (**r equal *)
-  | TCne: testcond    (**r not equal *)
-  | TChs: testcond    (**r unsigned higher or same *)
-  | TClo: testcond    (**r unsigned lower *)
-  | TCmi: testcond    (**r negative *)
-  | TCpl: testcond    (**r positive *)
-  | TChi: testcond    (**r unsigned higher *)
-  | TCls: testcond    (**r unsigned lower or same *)
-  | TCge: testcond    (**r signed greater or equal *)
-  | TClt: testcond    (**r signed less than *)
-  | TCgt: testcond    (**r signed greater *)
-  | TCle: testcond.   (**r signed less than or equal *)
-
-Inductive addressing: Type :=
-  | ADimm (base: iregsp) (n: int64)                  (**r base plus immediate offset *)
-  | ADreg (base: iregsp) (r: ireg)                   (**r base plus reg *)
-  | ADlsl (base: iregsp) (r: ireg) (n: int)          (**r base plus reg LSL n *)
-  | ADsxt (base: iregsp) (r: ireg) (n: int)          (**r base plus SIGN-EXT(reg) LSL n *)
-  | ADuxt (base: iregsp) (r: ireg) (n: int)          (**r base plus ZERO-EXT(reg) LSL n *)
-  | ADadr (base: iregsp) (id: ident) (ofs: ptrofs)   (**r base plus low address of [id + ofs] *)
-  | ADpostincr (base: iregsp) (n: int64).            (**r base plus offset; base is updated after *)
-
-Inductive shift_op: Type :=
-  | SOnone
-  | SOlsl (n: int)
-  | SOlsr (n: int)
-  | SOasr (n: int)
-  | SOror (n: int).
-
-Inductive extend_op: Type :=
-  | EOsxtb (n: int)
-  | EOsxth (n: int)
-  | EOsxtw (n: int)
-  | EOuxtb (n: int)
-  | EOuxth (n: int)
-  | EOuxtw (n: int)
-  | EOuxtx (n: int).
+(** * Abstract syntax *)
 
 (* First task: splitting the big [instruction] type below into CFI and basic instructions.
    Actually a finer splitting in order to regroup "similar" instructions could be much better for automation of the scheduler proof!
@@ -688,272 +548,19 @@ Inductive instruction: Type :=
 
 (** * Operational semantics *)
 
-(** The semantics operates over a single mapping from registers
-  (type [preg]) to values.  We maintain (but do not enforce)
-  the convention that integer registers are mapped to values of
-  type [Tint], float registers to values of type [Tfloat],
-  and condition bits to either [Vzero] or [Vone]. *)
-
-Definition regset := Pregmap.t val.
-Definition genv := Genv.t fundef unit.
-
-(** The value of an [ireg0] is either the value of the integer register,
-    or 0. *)
-
-Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val :=
-  match r with RR0 r => rs (IR' r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end.
-
-(** Concise notations for accessing and updating the values of registers. *)
-
-Notation "a # b" := (a b) (at level 1, only parsing) : asm.
-Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm.
-Notation "a ## b" := (ir0 W a b) (at level 1, only parsing) : asm.
-Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm.
-
-Open Scope asm.
-
-(** Undefining some registers *)
-
-Fixpoint undef_regs (l: list preg) (rs: regset) : regset :=
-  match l with
-  | nil => rs
-  | r :: l' => undef_regs l' (rs#r <- Vundef)
-  end.
-
-(** Undefining the condition codes *)
-
-Definition undef_flags (rs: regset) : regset :=
-  fun r => match r with CR _ => Vundef | _ => rs r end.
-
-(** Assigning a register pair *)
-
-Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset :=
-  match p with
-  | One r => rs#r <- v
-  | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v)
-  end.
-
-(** Assigning the result of a builtin *)
-
-Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
-  match res with
-  | BR r => rs#r <- v
-  | BR_none => rs
-  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
-  end.
-
 (** See "Parameters" of the same names in Asm.v *)
 Record aarch64_linker: Type := {
   symbol_low: ident -> ptrofs -> val;
   symbol_high: ident -> ptrofs -> val
 }.
 
+Definition genv := Genv.t fundef unit.
+
 Section RELSEM.
 
 Variable lk: aarch64_linker.
 Variable ge: genv.
 
-
-(** The semantics is purely small-step and defined as a function
-  from the current state (a register set + a memory state)
-  to either [Next rs' m'] where [rs'] and [m'] are the updated register
-  set and memory state after execution of the instruction at [rs#PC],
-  or [Stuck] if the processor is stuck. *)
-
-Record state: Type := State { _rs: regset; _m: mem }.
-Definition outcome := option state.
-Definition Next rs m: outcome := Some (State rs m).
-Definition Stuck: outcome := None.
-Local Open Scope option_monad_scope.
-
-(* a few lemma on comparisons of unsigned (e.g. pointers)
-
-TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!)
-*)
-
-Definition Val_cmpu_bool cmp v1 v2: option bool :=
-  Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
-
-Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmpu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
-
-Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
-               (Val_cmpu cmp v1 v2).
-Proof.
-  unfold Val.cmpu, Val_cmpu.
-  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob; simpl.
-  - erewrite Val_cmpu_bool_correct; eauto.
-    econstructor.
-  - econstructor.
-Qed.
-
-Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
- := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).
-
-Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmplu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
-
-Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
-               (Val_cmplu cmp v1 v2).
-Proof.
-  unfold Val.cmplu, Val_cmplu.
-  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob as [b|]; simpl.
-  - erewrite Val_cmplu_bool_correct; eauto.
-    simpl. econstructor.
-  - econstructor.
-Qed.
-
-(** Testing a condition *)
-
-Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
-  match c with
-  | TCeq =>                             (**r equal *)
-      match rs#CZ with
-      | Vint n => Some (Int.eq n Int.one)
-      | _ => None
-      end
-  | TCne =>                             (**r not equal *)
-      match rs#CZ with
-      | Vint n => Some (Int.eq n Int.zero)
-      | _ => None
-      end
-  | TClo =>                             (**r unsigned less than  *)
-      match rs#CC with
-      | Vint n => Some (Int.eq n Int.zero)
-      | _ => None
-      end
-  | TCls =>                             (**r unsigned less or equal *)
-      match rs#CC, rs#CZ with
-      | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one)
-      | _, _ => None
-      end
-  | TChs =>                             (**r unsigned greater or equal *)
-      match rs#CC with
-      | Vint n => Some (Int.eq n Int.one)
-      | _ => None
-      end
-  | TChi =>                             (**r unsigned greater *)
-      match rs#CC, rs#CZ with
-      | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero)
-      | _, _ => None
-      end
-  | TClt =>                             (**r signed less than *)
-      match rs#CV, rs#CN with
-      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one)
-      | _, _ => None
-      end
-  | TCle =>                             (**r signed less or equal *)
-      match rs#CV, rs#CN, rs#CZ with
-      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one)
-      | _, _, _ => None
-      end
-  | TCge =>                             (**r signed greater or equal *)
-      match rs#CV, rs#CN with
-      | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero)
-      | _, _ => None
-      end
-  | TCgt =>                             (**r signed greater *)
-      match rs#CV, rs#CN, rs#CZ with
-      | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero)
-      | _, _, _ => None
-      end
-  | TCpl =>                             (**r positive *)
-      match rs#CN with
-      | Vint n => Some (Int.eq n Int.zero)
-      | _ => None
-      end
-  | TCmi =>                             (**r negative *)
-      match rs#CN with
-      | Vint n => Some (Int.eq n Int.one)
-      | _ => None
-      end
-  end.
-
-(** Integer "is zero?" test *)
-
-Definition eval_testzero (sz: isize) (v: val): option bool :=
-  match sz with
-  | W => Val_cmpu_bool Ceq v (Vint Int.zero)
-  | X => Val_cmplu_bool Ceq v (Vlong Int64.zero)
-  end.
-
-(** Integer "bit is set?" test *)
-
-Definition eval_testbit (sz: isize) (v: val) (n: int): option bool :=
-  match sz with
-  | W => Val.cmp_bool Cne (Val.and v (Vint (Int.shl Int.one n))) (Vint Int.zero)
-  | X => Val.cmpl_bool Cne (Val.andl v (Vlong (Int64.shl' Int64.one n))) (Vlong Int64.zero)
-  end.
-
-
-(** Comparisons *)
-
-Definition compare_int (rs: regset) (v1 v2: val) :=
-  rs#CN <- (Val.negative (Val.sub v1 v2))
-    #CZ <- (Val_cmpu Ceq v1 v2)
-    #CC <- (Val_cmpu Cge v1 v2)
-    #CV <- (Val.sub_overflow v1 v2).
-
-Definition compare_long (rs: regset) (v1 v2: val) :=
-  rs#CN <- (Val.negativel (Val.subl v1 v2))
-    #CZ <- (Val_cmplu Ceq v1 v2)
-    #CC <- (Val_cmplu Cge v1 v2)
-    #CV <- (Val.subl_overflow v1 v2).
-
-(** Semantics of [fcmp] instructions:
-<<
-==	N=0 Z=1 C=1 V=0
-<	N=1 Z=0 C=0 V=0
->	N=0 Z=0 C=1 V=0
-unord	N=0 Z=0 C=1 V=1
->>
-*)
-
-Definition compare_float (rs: regset) (v1 v2: val) :=
-  match v1, v2 with
-  | Vfloat f1, Vfloat f2 =>
-      rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2))
-        #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2))
-        #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2)))
-        #CV <- (Val.of_bool (negb (Float.ordered f1 f2)))
-  | _, _ =>
-      rs#CN <- Vundef
-        #CZ <- Vundef
-        #CC <- Vundef
-        #CV <- Vundef
-  end.
-
-Definition compare_single (rs: regset) (v1 v2: val) :=
-  match v1, v2 with
-  | Vsingle f1, Vsingle f2 =>
-      rs#CN <- (Val.of_bool (Float32.cmp Clt f1 f2))
-        #CZ <- (Val.of_bool (Float32.cmp Ceq f1 f2))
-        #CC <- (Val.of_bool (negb (Float32.cmp Clt f1 f2)))
-        #CV <- (Val.of_bool (negb (Float32.ordered f1 f2)))
-  | _, _ =>
-      rs#CN <- Vundef
-        #CZ <- Vundef
-        #CC <- Vundef
-        #CV <- Vundef
-  end.
-
-
 (** Evaluating an addressing mode *)
 
 Definition eval_addressing (a: addressing) (rs: regset): val :=
@@ -980,66 +587,6 @@ Definition exec_store (chunk: memory_chunk)
   SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN
   Next rs m'.
 
-(** Insertion of bits into an integer *)
-
-Definition insert_in_int (x: val) (y: Z) (pos: Z) (len: Z) : val :=
-  match x with
-  | Vint n => Vint (Int.repr (Zinsert (Int.unsigned n) y pos len))
-  | _ => Vundef
-  end.
-
-Definition insert_in_long (x: val) (y: Z) (pos: Z) (len: Z) : val :=
-  match x with
-  | Vlong n => Vlong (Int64.repr (Zinsert (Int64.unsigned n) y pos len))
-  | _ => Vundef
-  end.
-
-(** Evaluation of shifted operands *)
-
-Definition eval_shift_op_int (v: val) (s: shift_op): val :=
-  match s with
-  | SOnone => v
-  | SOlsl n => Val.shl v (Vint n)
-  | SOlsr n => Val.shru v (Vint n)
-  | SOasr n => Val.shr v (Vint n)
-  | SOror n => Val.ror v (Vint n)
-  end.
-
-Definition eval_shift_op_long (v: val) (s: shift_op): val :=
-  match s with
-  | SOnone => v
-  | SOlsl n => Val.shll v (Vint n)
-  | SOlsr n => Val.shrlu v (Vint n)
-  | SOasr n => Val.shrl v (Vint n)
-  | SOror n => Val.rorl v (Vint n)
-  end.
-
-(** Evaluation of sign- or zero- extended operands *)
-
-Definition eval_extend (v: val) (x: extend_op): val :=
-  match x with
-  | EOsxtb n => Val.shll (Val.longofint (Val.sign_ext 8 v)) (Vint n)
-  | EOsxth n => Val.shll (Val.longofint (Val.sign_ext 16 v)) (Vint n)
-  | EOsxtw n => Val.shll (Val.longofint v) (Vint n)
-  | EOuxtb n => Val.shll (Val.longofintu (Val.zero_ext 8 v)) (Vint n)
-  | EOuxth n => Val.shll (Val.longofintu (Val.zero_ext 16 v)) (Vint n)
-  | EOuxtw n => Val.shll (Val.longofintu v) (Vint n)
-  | EOuxtx n => Val.shll v (Vint n)
-  end.
-
-(** Bit-level conversion from integers to FP numbers *)
-
-Definition float32_of_bits (v: val): val :=
-  match v with
-  | Vint n => Vsingle (Float32.of_bits n)
-  | _ => Vundef
-  end.
-
-Definition float64_of_bits (v: val): val :=
-  match v with
-  | Vlong n => Vfloat (Float.of_bits n)
-  | _ => Vundef
-  end.
 
 (** execution of loads
 *)
@@ -1892,76 +1439,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   end.
 *)
 
-(** Translation of the LTL/Linear/Mach view of machine registers
-  to the AArch64 view.  Note that no LTL register maps to [X16],
-  [X18], nor [X30].
-  [X18] is reserved as the platform register and never used by the
-  code generated by CompCert.
-  [X30] is used for the return address, and can also be used as temporary.
-  [X16] can be used as temporary. *)
-
-Definition dreg_of (r: mreg) : dreg :=
-  match r with
-  | R0 => X0   | R1 => X1   | R2 => X2   | R3 => X3
-  | R4 => X4   | R5 => X5   | R6 => X6   | R7 => X7
-  | R8 => X8   | R9 => X9   | R10 => X10 | R11 => X11
-  | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15
-  | R17 => X17 | R19 => X19
-  | R20 => X20 | R21 => X21 | R22 => X22 | R23 => X23
-  | R24 => X24 | R25 => X25 | R26 => X26 | R27 => X27
-  | R28 => X28 | R29 => X29
-  | F0 => D0   | F1 => D1   | F2 => D2   | F3 => D3
-  | F4 => D4   | F5 => D5   | F6 => D6   | F7 => D7
-  | F8 => D8   | F9 => D9   | F10 => D10 | F11 => D11
-  | F12 => D12 | F13 => D13 | F14 => D14 | F15 => D15
-  | F16 => D16 | F17 => D17 | F18 => D18 | F19 => D19
-  | F20 => D20 | F21 => D21 | F22 => D22 | F23 => D23
-  | F24 => D24 | F25 => D25 | F26 => D26 | F27 => D27
-  | F28 => D28 | F29 => D29 | F30 => D30 | F31 => D31
-  end.
-
-Definition preg_of (r: mreg) : preg :=
-  dreg_of r.
-
-(** Undefine all registers except SP and callee-save registers *)
-
-Definition undef_caller_save_regs (rs: regset) : regset :=
-  fun r =>
-    if preg_eq r SP
-    || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs))
-    then rs r
-    else Vundef.
-
-(** Extract the values of the arguments of an external call.
-    We exploit the calling conventions from module [Conventions], except that
-    we use AArch64 registers instead of locations. *)
-
-Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
-  | extcall_arg_reg: forall r,
-      extcall_arg rs m (R r) (rs (preg_of r))
-  | extcall_arg_stack: forall ofs ty bofs v,
-      bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
-      Mem.loadv (chunk_of_type ty) m
-                (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v ->
-      extcall_arg rs m (Locations.S Outgoing ofs ty) v.
-
-Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
-  | extcall_arg_one: forall l v,
-      extcall_arg rs m l v ->
-      extcall_arg_pair rs m (One l) v
-  | extcall_arg_twolong: forall hi lo vhi vlo,
-      extcall_arg rs m hi vhi ->
-      extcall_arg rs m lo vlo ->
-      extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo).
-
-Definition extcall_arguments
-    (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop :=
-  list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args.
-
-Definition loc_external_result (sg: signature) : rpair preg :=
-  map_rpair preg_of (loc_result sg).
-
-
 (**  execution of the body of a bblock *)
 Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome :=
   match body with
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.
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index b0787d0a..8e3c169a 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -34,13 +34,13 @@ let _m1 = Z.of_sint (-1)
 (* Emit instruction sequences that set or offset a register by a constant. *)
 
 let expand_loadimm32 (dst: ireg) n =
-  List.iter emit (Asmgen.loadimm32 dst n [])
+  List.iter emit (OrigAsmgen.loadimm32 dst n [])
 
 let expand_addimm64 (dst: iregsp) (src: iregsp) n =
-  List.iter emit (Asmgen.addimm64 dst src n [])
+  List.iter emit (OrigAsmgen.addimm64 dst src n [])
 
 let expand_storeptr (src: ireg) (base: iregsp) ofs =
-  List.iter emit (Asmgen.storeptr src base ofs [])
+  List.iter emit (OrigAsmgen.storeptr src base ofs [])
 
 (* Handling of varargs *)
 
@@ -132,9 +132,9 @@ let expand_builtin_va_start r =
 let expand_annot_val kind txt targ args res =
   emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none));
   match args, res with
-  | [BA(IR src)], BR(IR dst) ->
-     if dst <> src then emit (Pmov (RR1 dst, RR1 src))
-  | [BA(FR src)], BR(FR dst) ->
+  | [BA(DR(IR' src))], BR(DR(IR' dst)) ->
+     if dst <> src then emit (Pmov (dst, src))
+  | [BA(DR(FR' src))], BR(DR(FR' dst)) ->
      if dst <> src then emit (Pfmov (dst, src))
   | _, _ ->
      raise (Error "ill-formed __builtin_annot_val")
@@ -152,8 +152,8 @@ let offset_in_range ofs =
   
 let memcpy_small_arg sz arg tmp =
   match arg with
-  | BA (IR r) ->
-      (RR1 r, _0)
+  | BA (DR(IR' r)) ->
+      (r, _0)
   | BA_addrstack ofs ->
       if offset_in_range ofs
       && offset_in_range (Ptrofs.add ofs (Ptrofs.repr (Z.of_uint sz)))
@@ -164,7 +164,7 @@ let memcpy_small_arg sz arg tmp =
 
 let expand_builtin_memcpy_small sz al src dst =
   let (tsrc, tdst) =
-    if dst <> BA (IR X17) then (X17, X29) else (X29, X17) in
+    if dst <> BA (DR(IR'(RR1 X17))) then (X17, X29) else (X29, X17) in
   let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
   let (rdst, odst) = memcpy_small_arg sz dst tdst in
   let rec copy osrc odst sz =
@@ -197,7 +197,7 @@ let expand_builtin_memcpy_small sz al src dst =
 
 let memcpy_big_arg arg tmp =
   match arg with
-  | BA (IR r) -> emit (Pmov(RR1 tmp, RR1 r))
+  | BA (DR(IR' r)) -> emit (Pmov(RR1 tmp, r))
   | BA_addrstack ofs -> expand_addimm64 (RR1 tmp) XSP ofs
   | _ -> assert false
 
@@ -241,29 +241,29 @@ let expand_builtin_memcpy  sz al args =
 let expand_builtin_vload_common chunk base ofs res =
   let addr = ADimm(base, ofs) in
   match chunk, res with
-  | Mint8unsigned, BR(IR res) ->
+  | Mint8unsigned, BR(DR(IR'(RR1 res))) ->
      emit (Pldrb(W, res, addr))
-  | Mint8signed, BR(IR res) ->
+  | Mint8signed, BR(DR(IR'(RR1 res))) ->
      emit (Pldrsb(W, res, addr))
-  | Mint16unsigned, BR(IR res) ->
+  | Mint16unsigned, BR(DR(IR'(RR1 res))) ->
      emit (Pldrh(W, res, addr))
-  | Mint16signed, BR(IR res) ->
+  | Mint16signed, BR(DR(IR'(RR1 res))) ->
      emit (Pldrsh(W, res, addr))
-  | Mint32, BR(IR res) ->
+  | Mint32, BR(DR(IR'(RR1 res))) ->
      emit (Pldrw(res, addr))
-  | Mint64, BR(IR res) ->
+  | Mint64, BR(DR(IR'(RR1 res))) ->
      emit (Pldrx(res, addr))
-  | Mfloat32, BR(FR res) ->
+  | Mfloat32, BR(DR(FR' res)) ->
      emit (Pldrs(res, addr))
-  | Mfloat64, BR(FR res) ->
+  | Mfloat64, BR(DR(FR' res)) ->
      emit (Pldrd(res, addr))
   | _ ->
      assert false
 
 let expand_builtin_vload chunk args res =
   match args with
-  | [BA(IR addr)] ->
-      expand_builtin_vload_common chunk (RR1 addr) _0 res
+  | [BA(DR(IR' addr))] ->
+      expand_builtin_vload_common chunk addr _0 res
   | [BA_addrstack ofs] ->
       if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
         expand_builtin_vload_common chunk XSP ofs res
@@ -271,11 +271,11 @@ let expand_builtin_vload chunk args res =
         expand_addimm64 (RR1 X16) XSP ofs; (* X16 <- SP + ofs *)
         expand_builtin_vload_common chunk (RR1 X16) _0 res
       end
-  | [BA_addptr(BA(IR addr), BA_long ofs)] ->
+  | [BA_addptr(BA(DR(IR' addr)), BA_long ofs)] ->
       if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
-        expand_builtin_vload_common chunk (RR1 addr) ofs res
+        expand_builtin_vload_common chunk addr ofs res
       else begin
-        expand_addimm64 (RR1 X16) (RR1 addr) ofs; (* X16 <- addr + ofs *)
+        expand_addimm64 (RR1 X16) addr ofs; (* X16 <- addr + ofs *)
         expand_builtin_vload_common chunk (RR1 X16) _0 res
       end
   | _ ->
@@ -284,25 +284,25 @@ let expand_builtin_vload chunk args res =
 let expand_builtin_vstore_common chunk base ofs src =
   let addr = ADimm(base, ofs) in
   match chunk, src with
-  | (Mint8signed | Mint8unsigned), BA(IR src) ->
+  | (Mint8signed | Mint8unsigned), BA(DR(IR'(RR1 src))) ->
      emit (Pstrb(src, addr))
-  | (Mint16signed | Mint16unsigned), BA(IR src) ->
+  | (Mint16signed | Mint16unsigned), BA(DR(IR'(RR1 src))) ->
      emit (Pstrh(src, addr))
-  | Mint32, BA(IR src) ->
+  | Mint32, BA(DR(IR'(RR1 src))) ->
      emit (Pstrw(src, addr))
-  | Mint64, BA(IR src) ->
+  | Mint64, BA(DR(IR'(RR1 src))) ->
      emit (Pstrx(src, addr))
-  | Mfloat32, BA(FR src) ->
+  | Mfloat32, BA(DR(FR' src)) ->
      emit (Pstrs(src, addr))
-  | Mfloat64, BA(FR src) ->
+  | Mfloat64, BA(DR(FR' src)) ->
      emit (Pstrd(src, addr))
   | _ ->
      assert false
 
 let expand_builtin_vstore chunk args =
   match args with
-  | [BA(IR addr); src] ->
-      expand_builtin_vstore_common chunk (RR1 addr) _0 src
+  | [BA(DR(IR' addr)); src] ->
+      expand_builtin_vstore_common chunk addr _0 src
   | [BA_addrstack ofs; src] ->
       if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
         expand_builtin_vstore_common chunk XSP ofs src
@@ -310,11 +310,11 @@ let expand_builtin_vstore chunk args =
         expand_addimm64 (RR1 X16) XSP ofs; (* X16 <- SP + ofs *)
         expand_builtin_vstore_common chunk (RR1 X16) _0 src
       end
-  | [BA_addptr(BA(IR addr), BA_long ofs); src] ->
+  | [BA_addptr(BA(DR(IR' addr)), BA_long ofs); src] ->
       if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
-        expand_builtin_vstore_common chunk (RR1 addr) ofs src
+        expand_builtin_vstore_common chunk addr ofs src
       else begin
-        expand_addimm64 (RR1 X16) (RR1 addr) ofs; (* X16 <- addr + ofs *)
+        expand_addimm64 (RR1 X16) addr ofs; (* X16 <- addr + ofs *)
         expand_builtin_vstore_common chunk (RR1 X16) _0 src
       end
   | _ ->
@@ -330,37 +330,37 @@ let expand_builtin_inline name args res =
   | "__builtin_nop", [], _ ->
      emit Pnop
   (* Byte swap *)
-  | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
+  | ("__builtin_bswap" | "__builtin_bswap32"), [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) ->
      emit (Prev(W, res, a1))
-  | "__builtin_bswap64", [BA(IR a1)], BR(IR res) ->
+  | "__builtin_bswap64", [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) ->
      emit (Prev(X, res, a1))
-  | "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
+  | "__builtin_bswap16", [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) ->
      emit (Prev16(W, res, a1));
      emit (Pandimm(W, res, RR0 res, Z.of_uint 0xFFFF))
   (* Count leading zeros and leading sign bits *)
-  | "__builtin_clz",  [BA(IR a1)], BR(IR res) ->
+  | "__builtin_clz",  [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) ->
      emit (Pclz(W, res, a1))
-  | ("__builtin_clzl" | "__builtin_clzll"),  [BA(IR a1)], BR(IR res) ->
+  | ("__builtin_clzl" | "__builtin_clzll"),  [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) ->
      emit (Pclz(X, res, a1)) 
-  | "__builtin_cls",  [BA(IR a1)], BR(IR res) ->
+  | "__builtin_cls",  [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) ->
      emit (Pcls(W, res, a1))
-  | ("__builtin_clsl" | "__builtin_clsll"),  [BA(IR a1)], BR(IR res) ->
+  | ("__builtin_clsl" | "__builtin_clsll"),  [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) ->
      emit (Pcls(X, res, a1))
  (* Float arithmetic *)
-  | "__builtin_fabs",  [BA(FR a1)], BR(FR res) ->
+  | "__builtin_fabs",  [BA(DR(FR' a1))], BR(DR(FR' res)) ->
      emit (Pfabs(D, res, a1))
-  | "__builtin_fsqrt",  [BA(FR a1)], BR(FR res) ->
+  | "__builtin_fsqrt",  [BA(DR(FR' a1))], BR(DR(FR' res)) ->
      emit (Pfsqrt(D, res, a1))
-  | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
+  | "__builtin_fmadd", [BA(DR(FR' a1)); BA(DR(FR' a2)); BA(DR(FR' a3))], BR(DR(FR' res)) ->
       emit (Pfmadd(D, res, a1, a2, a3))
-  | "__builtin_fmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
+  | "__builtin_fmsub", [BA(DR(FR' a1)); BA(DR(FR' a2)); BA(DR(FR' a3))], BR(DR(FR' res)) ->
       emit (Pfmsub(D, res, a1, a2, a3))
-  | "__builtin_fnmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
+  | "__builtin_fnmadd", [BA(DR(FR' a1)); BA(DR(FR' a2)); BA(DR(FR' a3))], BR(DR(FR' res)) ->
       emit (Pfnmadd(D, res, a1, a2, a3))
-  | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
+  | "__builtin_fnmsub", [BA(DR(FR' a1)); BA(DR(FR' a2)); BA(DR(FR' a3))], BR(DR(FR' res)) ->
       emit (Pfnmsub(D, res, a1, a2, a3))
   (* Vararg *)
-  | "__builtin_va_start", [BA(IR a)], _ ->
+  | "__builtin_va_start", [BA(DR(IR'(RR1 a)))], _ ->
       expand_builtin_va_start a
   (* Catch-all *)
   | _ ->
@@ -427,9 +427,9 @@ let float_reg_to_dwarf = function
   | D30 -> 94 | D31 -> 95
 
 let preg_to_dwarf = function
-   | IR r -> int_reg_to_dwarf r
-   | FR r -> float_reg_to_dwarf r
-   | SP -> 31
+   | DR(IR'(RR1 r)) -> int_reg_to_dwarf r
+   | DR(FR' r) -> float_reg_to_dwarf r
+   | DR(IR'(XSP)) -> 31
    | _ -> assert false
 
 let expand_function id fn =
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index 5dec10e9..af069929 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -28,19 +28,19 @@ Local Open Scope error_monad_scope.
 Module Asmblock_TRANSF.
 (* STUB *)
 
-Definition ireg_of_preg (p : Asmblock.preg) : res ireg :=
+Definition ireg_of_preg (p : Asm.preg) : res ireg :=
   match p with
   | DR (IR' (RR1 r)) => OK r
   | _ => Error (msg "Asmgen.ireg_of_preg")
   end.
 
-Definition freg_of_preg (p : Asmblock.preg) : res freg :=
+Definition freg_of_preg (p : Asm.preg) : res freg :=
   match p with
   | DR (FR' r) => OK r
   | _ => Error (msg "Asmgen.freg_of_preg")
   end.
 
-Definition iregsp_of_preg (p : Asmblock.preg) : res iregsp :=
+Definition iregsp_of_preg (p : Asm.preg) : res iregsp :=
   match p with
   | DR (IR' r) => OK r
   | _ => Error (msg "Asmgen.iregsp_of_preg")
@@ -61,7 +61,7 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
                                             OK (Asm.Pfmovimmd rd' f)
 
   | PArith (PArithPP (Pmovk sz n pos) rd rs) =>
-    if (Asmblock.preg_eq rd rs) then (
+    if (Asm.preg_eq rd rs) then (
       do rd' <- ireg_of_preg rd;
       OK (Asm.Pmovk sz rd' n pos)
     ) else
@@ -359,4 +359,4 @@ 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.
+  Asmblock_TRANSF.transf_program abp.
\ No newline at end of file
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 0ea37a38..f469e437 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -3,6 +3,7 @@
 (*             The Compcert verified compiler                  *)
 (*                                                             *)
 (*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
+(*           Léo Gourdin        UGA, VERIMAG                   *)
 (*           Justus Fasse       UGA, VERIMAG                   *)
 (*           Xavier Leroy       INRIA Paris-Rocquencourt       *)
 (*           David Monniaux     CNRS, VERIMAG                  *)
@@ -17,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 Asmblock.
+Require Import Op Locations Machblock Conventions PseudoAsmblock Asm Asmblock.
 Require Machblockgenproof Asmblockgenproof.
 Require Import Asmgen.
 Require Import Axioms.
@@ -1862,8 +1863,8 @@ Qed.
 Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m
   (ATPC : rs PC = Vptr b ofs)
   (MATCHI : match_internal (size bb - 1)
-            {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |}
-            {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}),
+            {| _rs := rs; _m := m |}
+            {| _rs := _rs; _m := _m |}),
   _rs PC = Vptr b (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))).
 Proof.
   intros; inv MATCHI. rewrite <- AGPC; rewrite ATPC; unfold Val.offset_ptr; eauto.
@@ -1874,8 +1875,8 @@ Lemma find_instr_ofs_somei: forall ofs bb f tc asmi rs m _rs _m
   (FIND_INSTR : Asm.find_instr (Ptrofs.unsigned ofs + (size bb - 1)) tc =
                 Some (asmi))
   (MATCHI : match_internal (size bb - 1)
-            {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |}
-            {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}),
+            {| _rs := rs; _m := m |}
+            {| _rs := _rs; _m := _m |}),
   Asm.find_instr (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
     (Asm.fn_code {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}) =
   Some (asmi).
@@ -1900,8 +1901,8 @@ Qed.
 
 Lemma eval_builtin_args_match: forall bb rs m _rs _m args vargs
   (MATCHI : match_internal (size bb - 1)
-            {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |}
-            {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |})
+            {| _rs := rs; _m := m |}
+            {| _rs := _rs; _m := _m |})
   (EVAL : eval_builtin_args tge (fun r : dreg => rs r) (rs SP) m args vargs),
   eval_builtin_args tge _rs (_rs SP) _m (map (map_builtin_arg DR) args) vargs.
 Proof.
@@ -2114,9 +2115,9 @@ Proof.
      erewrite !set_builtin_map_not_pc. rewrite HPC.
      eapply set_builtin_res_dont_move_pc_gen; intros.
      eapply set_buitin_res_sym; eauto.
+Qed.
 
 
-  
 Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
diff --git a/aarch64/OrigAsmgen.ml b/aarch64/OrigAsmgen.ml
new file mode 100644
index 00000000..1bbcf085
--- /dev/null
+++ b/aarch64/OrigAsmgen.ml
@@ -0,0 +1,282 @@
+(** File (more or less) extracted from the official aarch64/Asmgen.v of CompCert 
+
+TODO: prune some definition in these files by reusing the ones of Asmblockgen that are identical...
+e.g. all those which do not involve Asm.code
+
+**)
+
+open Asm
+open BinInt
+open BinNums
+open Integers
+open List0
+open Zbits
+
+module I = Integers.Int
+module I64 = Integers.Int64
+module N = PeanoNat.Nat
+   
+let s_ x = Datatypes.S x
+let o_ = Datatypes.O
+
+module Automaton =
+ struct
+  type state =
+  | SA
+  | SB
+  | SC
+  | SD
+  | SE
+  | SF
+  | SG
+  | Sbad
+
+  (** val start : state **)
+
+  let start =
+    SA
+
+  (** val next : state -> bool -> state **)
+
+  let next s b =
+    match s with
+    | SA -> if b then SC else SB
+    | SB -> if b then SD else SB
+    | SC -> if b then SC else SE
+    | SD -> if b then SD else SF
+    | SE -> if b then SG else SE
+    | SF -> if b then Sbad else SF
+    | SG -> if b then SG else Sbad
+    | Sbad -> Sbad
+
+  (** val accepting : state -> bool **)
+
+  let accepting = function
+  | Sbad -> false
+  | _ -> true
+
+  (** val run : nat -> state -> coq_Z -> bool **)
+
+  let rec run len s x =
+    match len with
+    | Datatypes.O -> accepting s
+    | Datatypes.S len0 -> run len0 (next s (Z.odd x)) (Z.div2 x)
+ end
+
+(** val logical_imm_length : coq_Z -> bool -> nat **)
+
+let logical_imm_length x sixtyfour =
+  let test = fun n ->
+    Z.eqb (coq_Zzero_ext n x) (coq_Zzero_ext n (Z.shiftr x n))
+  in
+  if (&&) sixtyfour
+       (Datatypes.negb
+         (test (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH))))))))
+  then s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_
+         (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_
+         (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_
+         o_)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+  else if Datatypes.negb (test (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH))))))
+       then s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_
+              (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ o_)))))))))))))))))))))))))))))))
+       else if Datatypes.negb (test (Zpos (Coq_xO (Coq_xO (Coq_xO Coq_xH)))))
+            then s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_
+                   o_)))))))))))))))
+            else if Datatypes.negb (test (Zpos (Coq_xO (Coq_xO Coq_xH))))
+                 then s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ o_)))))))
+                 else if Datatypes.negb (test (Zpos (Coq_xO Coq_xH)))
+                      then s_ (s_ (s_ (s_ o_)))
+                      else s_ (s_ o_)
+
+(** val is_logical_imm32 : I.int -> bool **)
+
+let is_logical_imm32 x =
+  (&&) ((&&) (Datatypes.negb (I.eq x I.zero)) (Datatypes.negb (I.eq x I.mone)))
+    (Automaton.run (logical_imm_length (I.unsigned x) false)
+      Automaton.start (I.unsigned x))
+
+(** val is_logical_imm64 : I64.int -> bool **)
+
+let is_logical_imm64 x =
+  (&&) ((&&) (Datatypes.negb (I64.eq x I64.zero)) (Datatypes.negb (I64.eq x I64.mone)))
+    (Automaton.run (logical_imm_length (I64.unsigned x) true)
+      Automaton.start (I64.unsigned x))
+
+(** val is_arith_imm32 : I.int -> bool **)
+
+let is_arith_imm32 x =
+  (||) (I.eq x (I.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))) x))
+    (I.eq x
+      (I.shl
+        (I.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH))))
+          (I.shru x (I.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))))))
+        (I.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))))))
+
+(** val is_arith_imm64 : I64.int -> bool **)
+
+let is_arith_imm64 x =
+  (||)
+    (I64.eq x (I64.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))) x))
+    (I64.eq x
+      (I64.shl
+        (I64.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH))))
+          (I64.shru x (I64.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))))))
+        (I64.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))))))
+
+(** val decompose_int : nat -> coq_Z -> coq_Z -> (coq_Z * coq_Z) list **)
+
+let rec decompose_int n n0 p =
+  match n with
+  | Datatypes.O -> []
+  | Datatypes.S n1 ->
+    let frag =
+      coq_Zzero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH)))))
+        (Z.shiftr n0 p)
+    in
+    if Z.eqb frag Z0
+    then decompose_int n1 n0
+           (Z.add p (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH))))))
+    else (frag,
+           p) :: (decompose_int n1
+                   (Z.ldiff n0
+                     (Z.shiftl (Zpos (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI
+                       (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI
+                       (Coq_xI (Coq_xI (Coq_xI (Coq_xI Coq_xH))))))))))))))))
+                       p))
+                   (Z.add p (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH)))))))
+
+(** val negate_decomposition :
+    (coq_Z * coq_Z) list -> (coq_Z * coq_Z) list **)
+
+let negate_decomposition l =
+  map (fun np ->
+    ((Z.coq_lxor (fst np) (Zpos (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI
+       (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI
+       (Coq_xI (Coq_xI Coq_xH))))))))))))))))), (snd np))) l
+
+(** val loadimm_k :
+    isize -> ireg -> (coq_Z * coq_Z) list -> Asm.code -> Asm.code **)
+
+let loadimm_k sz rd l k =
+  fold_right (fun np k0 -> (Pmovk (sz, rd, (fst np), (snd np))) :: k0) k l
+
+(** val loadimm_z :
+    isize -> ireg -> (coq_Z * coq_Z) list -> Asm.code -> Asm.code **)
+
+let loadimm_z sz rd l k =
+  match l with
+  | [] -> (Pmovz (sz, rd, Z0, Z0)) :: k
+  | p :: l0 ->
+    let (n1, p1) = p in (Pmovz (sz, rd, n1, p1)) :: (loadimm_k sz rd l0 k)
+
+(** val loadimm_n :
+    isize -> ireg -> (coq_Z * coq_Z) list -> Asm.code -> Asm.code **)
+
+let loadimm_n sz rd l k =
+  match l with
+  | [] -> (Pmovn (sz, rd, Z0, Z0)) :: k
+  | p :: l0 ->
+    let (n1, p1) = p in
+    (Pmovn (sz, rd, n1, p1)) :: (loadimm_k sz rd (negate_decomposition l0) k)
+
+(** val loadimm : isize -> ireg -> coq_Z -> Asm.code -> Asm.code **)
+
+let loadimm sz rd n k =
+  let n0 = match sz with
+           | W -> s_ (s_ o_)
+           | X -> s_ (s_ (s_ (s_ o_))) in
+  let dz = decompose_int n0 n Z0 in
+  let dn = decompose_int n0 (Z.lnot n) Z0 in
+  if N.leb (Datatypes.length dz) (Datatypes.length dn)
+  then loadimm_z sz rd dz k
+  else loadimm_n sz rd dn k
+
+(** val loadimm32 : ireg -> I.int -> Asm.code -> Asm.code **)
+
+let loadimm32 rd n k =
+  if is_logical_imm32 n
+  then (Porrimm (W, rd, XZR, (I.unsigned n))) :: k
+  else loadimm W rd (I.unsigned n) k
+
+(** val loadimm64 : ireg -> I64.int -> Asm.code -> Asm.code **)
+
+let loadimm64 rd n k =
+  if is_logical_imm64 n
+  then (Porrimm (X, rd, XZR, (I64.unsigned n))) :: k
+  else loadimm X rd (I64.unsigned n) k
+
+(** val addimm_aux :
+    (iregsp -> iregsp -> coq_Z -> Asm.instruction) -> iregsp -> iregsp ->
+    coq_Z -> Asm.code -> Asm.instruction list **)
+
+let addimm_aux insn rd r1 n k =
+  let nlo = coq_Zzero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))) n in
+  let nhi = Z.sub n nlo in
+  if Z.eqb nhi Z0
+  then (insn rd r1 nlo) :: k
+  else if Z.eqb nlo Z0
+       then (insn rd r1 nhi) :: k
+       else (insn rd r1 nhi) :: ((insn rd rd nlo) :: k)
+
+(** val addimm32 : ireg -> ireg -> I.int -> Asm.code -> Asm.code **)
+
+let addimm32 rd r1 n k =
+  let m = I.neg n in
+  if I.eq n
+       (I.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xI Coq_xH))))) n)
+  then addimm_aux (fun x x0 x1 -> Paddimm (W, x, x0, x1)) (RR1 rd) (RR1 r1)
+         (I.unsigned n) k
+  else if I.eq m
+            (I.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xI Coq_xH))))) m)
+       then addimm_aux (fun x x0 x1 -> Psubimm (W, x, x0, x1)) (RR1 rd) (RR1
+              r1) (I.unsigned m) k
+       else if I.lt n I.zero
+            then loadimm32 X16 m ((Psub (W, rd, (RR0 r1), X16, SOnone)) :: k)
+            else loadimm32 X16 n ((Padd (W, rd, (RR0 r1), X16, SOnone)) :: k)
+
+(** val addimm64 : iregsp -> iregsp -> I64.int -> Asm.code -> Asm.code **)
+
+let addimm64 rd r1 n k =
+  let m = I64.neg n in
+  if I64.eq n
+       (I64.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xI Coq_xH))))) n)
+  then addimm_aux (fun x x0 x1 -> Paddimm (X, x, x0, x1)) rd r1
+         (I64.unsigned n) k
+  else if I64.eq m
+            (I64.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xI Coq_xH)))))
+              m)
+       then addimm_aux (fun x x0 x1 -> Psubimm (X, x, x0, x1)) rd r1
+              (I64.unsigned m) k
+       else if I64.lt n I64.zero
+            then loadimm64 X16 m ((Psubext (rd, r1, X16, (EOuxtx
+                   I.zero))) :: k)
+            else loadimm64 X16 n ((Paddext (rd, r1, X16, (EOuxtx
+                   I.zero))) :: k)
+
+(** val offset_representable : coq_Z -> I64.int -> bool **)
+
+let offset_representable sz ofs =
+  let isz = I64.repr sz in
+  (||)
+    (I64.eq ofs
+      (I64.sign_ext (Zpos (Coq_xI (Coq_xO (Coq_xO Coq_xH)))) ofs))
+    ((&&) (I64.eq (I64.modu ofs isz) I64.zero)
+      (I64.ltu ofs
+        (I64.shl isz (I64.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH))))))))
+  
+(** val indexed_memory_access :
+    (Asm.addressing -> Asm.instruction) -> coq_Z -> iregsp -> Ptrofs.int ->
+    Asm.code -> Asm.instruction list **)
+
+let indexed_memory_access insn sz base ofs k =
+  let ofs0 = Ptrofs.to_int64 ofs in
+  if offset_representable sz ofs0
+  then (insn (ADimm (base, ofs0))) :: k
+  else loadimm64 X16 ofs0 ((insn (ADreg (base, X16))) :: k)
+
+(** val storeptr :
+    ireg -> iregsp -> Ptrofs.int -> Asm.code -> Asm.instruction list **)
+
+let storeptr src base ofs k =
+  indexed_memory_access (fun x -> Pstrx (src, x)) (Zpos (Coq_xO (Coq_xO
+    (Coq_xO Coq_xH)))) base ofs k
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index 8d74daf4..b1425d56 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -120,13 +120,13 @@ module Target : TARGET =
       output_string oc (match sz with D -> dreg_name r | S -> sreg_name r)
 
     let preg_asm oc ty = function
-      | IR r -> if ty = Tint then wreg oc r else xreg oc r
-      | FR r -> if ty = Tsingle then sreg oc r else dreg oc r
+      | DR (IR' (RR1 r)) -> if ty = Tint then wreg oc r else xreg oc r
+      | DR (FR' r) -> if ty = Tsingle then sreg oc r else dreg oc r
       | _    -> assert false
 
     let preg_annot = function
-      | IR r -> xreg_name r
-      | FR r -> dreg_name r
+      | DR (IR' (RR1 r)) -> xreg_name r
+      | DR (FR' r) -> dreg_name r
       | _ -> assert false
 
 (* Names of sections *)
diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index e82056e2..6815bc59 100644
--- a/aarch64/extractionMachdep.v
+++ b/aarch64/extractionMachdep.v
@@ -21,4 +21,4 @@ Extract Constant Archi.pic_code => "fun () -> false".  (* for the time being *)
 (* Asm *)
 Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false".
 Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false".
-Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned".
+Extract Constant Asmblockgen.symbol_is_aligned => "C2C.atom_is_aligned".
diff --git a/extraction/extraction.v b/extraction/extraction.v
index bd396cd8..5de66797 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -13,6 +13,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require Import ZArith PeanoNat.
 Require Coqlib.
 Require Wfsimpl.
 Require DecidableClass Decidableplus.
@@ -218,7 +219,8 @@ Set Extraction AccessOpaque.
 
 Cd "extraction".
 
-Separate Extraction
+Separate Extraction 
+   Z.ldiff Z.lnot Nat.leb
    CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
-- 
cgit