[WIP: Coq compilation broken] Stub for Asmgen

1 files changed, 32 insertions, 498 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 47cd3051..0959d9ca 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -10,149 +10,28 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Abstract syntax and semantics for AArch64 assembly language *)
+(** Abstract syntax and semantics for AArch64 assembly language 
+
+
+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.
 Require Import AST Integers Floats.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Locations Conventions.
 Require Stacklayout.
+Require Import OptionMonad Asmblock.
 
 (** * 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.
-
-(** 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.
-
-(** We model the following registers of the ARM architecture. *)
-
-Inductive preg: Type :=
-  | IR: ireg -> preg   (**r 64- or 32-bit integer registers *)
-  | FR: freg -> preg   (**r double- or single-precision float registers *)
-  | CR: crbit -> preg  (**r bits in the condition register *)
-  | SP: preg           (**r register X31 used as stack pointer *)
-  | PC: preg.          (**r program counter *)
-
-Coercion IR: ireg >-> preg.
-Coercion FR: freg >-> preg.
-Coercion CR: crbit >-> preg.
-
-Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}.
-Proof. decide equality. apply ireg_eq. apply freg_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.
-
-Coercion preg_of_iregsp: iregsp >-> preg.
-
-(** 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 *)
@@ -307,65 +186,8 @@ Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
-
-(** * 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 ir0w (rs: regset) (r: ireg0) : val :=
-  match r with RR0 r => rs (IR r) | XZR => Vint Int.zero end.
-Definition ir0x (rs: regset) (r: ireg0) : val :=
-  match r with RR0 r => rs (IR r) | XZR => 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" := (ir0w a b) (at level 1, only parsing) : asm.
-Notation "a ### b" := (ir0x 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 two functions below axiomatize how the linker processes
   symbolic references [symbol + offset].  It computes the
   difference between the address and the PC, and splits it into:
@@ -385,6 +207,8 @@ Axiom symbol_high_low:
   forall (ge: genv) (id: ident) (ofs: ptrofs),
   Val.addl (symbol_high ge id ofs) (symbol_low ge id ofs) = Genv.symbol_address ge id ofs.
 
+(** * Operational semantics *)
+
 Section RELSEM.
 
 Variable ge: genv.
@@ -419,19 +243,6 @@ Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
       if is_label lbl instr then Some (pos + 1) else label_pos lbl (pos + 1) c'
   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. *)
-
-Inductive outcome: Type :=
-  | Next: regset -> mem -> outcome
-  | Stuck: outcome.
-
-(** Manipulations over the [PC] register: continuing with the next
-  instruction ([nextinstr]) or branching to a label ([goto_label]). *)
-
 Definition nextinstr (rs: regset) :=
   rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one).
 
@@ -445,88 +256,6 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
     end
   end.
 
-(** 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) (m: mem): option bool :=
-  match sz with
-  | W => Val.cmpu_bool (Mem.valid_pointer m) Ceq v (Vint Int.zero)
-  | X => Val.cmplu_bool (Mem.valid_pointer m) 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.
-
 (** Evaluating an addressing mode *)
 
 Definition eval_addressing (a: addressing) (rs: regset): val :=
@@ -557,130 +286,6 @@ Definition exec_store (chunk: memory_chunk)
   | Some m' => Next (nextinstr rs) m'
   end.
 
-(** Comparisons *)
-
-Definition compare_int (rs: regset) (v1 v2: val) (m: mem) :=
-  rs#CN <- (Val.negative (Val.sub v1 v2))
-    #CZ <- (Val.cmpu (Mem.valid_pointer m) Ceq v1 v2)
-    #CC <- (Val.cmpu (Mem.valid_pointer m) Cge v1 v2)
-    #CV <- (Val.sub_overflow v1 v2).
-
-Definition compare_long (rs: regset) (v1 v2: val) (m: mem) :=
-  rs#CN <- (Val.negativel (Val.subl v1 v2))
-    #CZ <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Ceq v1 v2))
-    #CC <- (Val.maketotal (Val.cmplu (Mem.valid_pointer m) 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.
-
-(** Execution of a single instruction [i] in initial state
-    [rs] and [m].  Return updated state.  For instructions
-    that correspond to actual AArch64 instructions, the cases are
-    straightforward transliterations of the informal descriptions
-    given in the ARMv8 reference manuals.  For pseudo-instructions,
-    refer to the informal descriptions given above.
-
-    Note that we set to [Vundef] the registers used as temporaries by
-    the expansions of the pseudo-instructions, so that the code we
-    generate cannot use those registers to hold values that must
-    survive the execution of the pseudo-instruction.
-*)
 
 Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
   match i with
@@ -704,13 +309,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pret r =>
       Next (rs#PC <- (rs#r)) m
   | Pcbnz sz r lbl =>
-      match eval_testzero sz rs#r m with
+      match eval_testzero sz rs#r with
       | Some true => Next (nextinstr rs) m
       | Some false => goto_label f lbl rs m
       | None => Stuck
       end
   | Pcbz sz r lbl =>
-      match eval_testzero sz rs#r m with
+      match eval_testzero sz rs#r with
       | Some true => goto_label f lbl rs m
       | Some false => Next (nextinstr rs) m
       | None => Stuck
@@ -778,13 +383,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Psubimm X rd r1 n =>
       Next (nextinstr (rs#rd <- (Val.subl rs#r1 (Vlong (Int64.repr n))))) m
   | Pcmpimm W r1 n =>
-      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.repr n)) m)) m
+      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.repr n)))) m
   | Pcmpimm X r1 n =>
-      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.repr n)) m)) m
+      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.repr n)))) m
   | Pcmnimm W r1 n =>
-      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.neg (Int.repr n))) m)) m
+      Next (nextinstr (compare_int rs rs#r1 (Vint (Int.neg (Int.repr n))))) m
   | Pcmnimm X r1 n =>
-      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.neg (Int64.repr n))) m)) m
+      Next (nextinstr (compare_long rs rs#r1 (Vlong (Int64.neg (Int64.repr n))))) m
   (** Move integer register *)
   | Pmov rd r1 =>
       Next (nextinstr (rs#rd <- (rs#r1))) m
@@ -802,9 +407,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Porrimm X rd r1 n =>
       Next (nextinstr (rs#rd <- (Val.orl rs###r1 (Vlong (Int64.repr n))))) m
   | Ptstimm W r1 n =>
-      Next (nextinstr (compare_int rs (Val.and rs#r1 (Vint (Int.repr n))) (Vint Int.zero) m)) m
+      Next (nextinstr (compare_int rs (Val.and rs#r1 (Vint (Int.repr n))) (Vint Int.zero))) m
   | Ptstimm X r1 n =>
-      Next (nextinstr (compare_long rs (Val.andl rs#r1 (Vlong (Int64.repr n))) (Vlong Int64.zero) m)) m
+      Next (nextinstr (compare_long rs (Val.andl rs#r1 (Vlong (Int64.repr n))) (Vlong Int64.zero))) m
   (** Move wide immediate *)
   | Pmovz W rd n pos =>
       Next (nextinstr (rs#rd <- (Vint (Int.repr (Z.shiftl n pos))))) m
@@ -850,22 +455,22 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Psub X rd r1 r2 s =>
       Next (nextinstr (rs#rd <- (Val.subl rs###r1 (eval_shift_op_long rs#r2 s)))) m
   | Pcmp W r1 r2 s =>
-      Next (nextinstr (compare_int rs rs##r1 (eval_shift_op_int rs#r2 s) m)) m
+      Next (nextinstr (compare_int rs rs##r1 (eval_shift_op_int rs#r2 s))) m
   | Pcmp X r1 r2 s =>
-      Next (nextinstr (compare_long rs rs###r1 (eval_shift_op_long rs#r2 s) m)) m
+      Next (nextinstr (compare_long rs rs###r1 (eval_shift_op_long rs#r2 s))) m
   | Pcmn W r1 r2 s =>
-      Next (nextinstr (compare_int rs rs##r1 (Val.neg (eval_shift_op_int rs#r2 s)) m)) m
+      Next (nextinstr (compare_int rs rs##r1 (Val.neg (eval_shift_op_int rs#r2 s)))) m
   | Pcmn X r1 r2 s =>
-      Next (nextinstr (compare_long rs rs###r1 (Val.negl (eval_shift_op_long rs#r2 s)) m)) m
+      Next (nextinstr (compare_long rs rs###r1 (Val.negl (eval_shift_op_long rs#r2 s)))) m
   (** Integer arithmetic, extending register *)
   | Paddext rd r1 r2 x =>
       Next (nextinstr (rs#rd <- (Val.addl rs#r1 (eval_extend rs#r2 x)))) m
   | Psubext rd r1 r2 x =>
       Next (nextinstr (rs#rd <- (Val.subl rs#r1 (eval_extend rs#r2 x)))) m
   | Pcmpext r1 r2 x =>
-      Next (nextinstr (compare_long rs rs#r1 (eval_extend rs#r2 x) m)) m
+      Next (nextinstr (compare_long rs rs#r1 (eval_extend rs#r2 x))) m
   | Pcmnext r1 r2 x =>
-      Next (nextinstr (compare_long rs rs#r1 (Val.negl (eval_extend rs#r2 x)) m)) m
+      Next (nextinstr (compare_long rs rs#r1 (Val.negl (eval_extend rs#r2 x)))) m
   (** Logical, shifted register *)
   | Pand W rd r1 r2 s =>
       Next (nextinstr (rs#rd <- (Val.and rs##r1 (eval_shift_op_int rs#r2 s)))) m
@@ -892,9 +497,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Porn X rd r1 r2 s =>
       Next (nextinstr (rs#rd <- (Val.orl rs###r1 (Val.notl (eval_shift_op_long rs#r2 s))))) m
   | Ptst W r1 r2 s =>
-      Next (nextinstr (compare_int rs (Val.and rs##r1 (eval_shift_op_int rs#r2 s)) (Vint Int.zero) m)) m
+      Next (nextinstr (compare_int rs (Val.and rs##r1 (eval_shift_op_int rs#r2 s)) (Vint Int.zero))) m
   | Ptst X r1 r2 s =>
-      Next (nextinstr (compare_long rs (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)) (Vlong Int64.zero) m)) m
+      Next (nextinstr (compare_long rs (Val.andl rs###r1 (eval_shift_op_long rs#r2 s)) (Vlong Int64.zero))) m
   (** Variable shifts *)
   | Pasrv W rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.shr rs#r1 rs#r2))) m
@@ -1118,80 +723,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Stuck
   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 preg_of (r: mreg) : preg :=
-  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.
-
-(** 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 instruction at [rs#PC]. *)
-
-Inductive state: Type :=
-  | State: regset -> mem -> state.
-
 Inductive step: state -> trace -> state -> Prop :=
   | exec_step_internal:
-      forall b ofs f i rs m rs' m',
+      forall b ofs (f:function) i rs m rs' m',
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
       find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some i ->