diff options
-rw-r--r-- | aarch64/Asm.v | 530 | ||||
-rw-r--r-- | aarch64/Asmblock.v | 14 | ||||
-rw-r--r-- | aarch64/Asmblockgen.v | 1197 | ||||
-rw-r--r-- | aarch64/Asmblockgenproof.v | 1104 | ||||
-rw-r--r-- | aarch64/Asmblockgenproof1.v (renamed from aarch64/Asmgenproof1.v) | 3 | ||||
-rw-r--r-- | aarch64/Asmgen.v | 1185 | ||||
-rw-r--r-- | aarch64/Asmgenproof.v | 1101 | ||||
-rwxr-xr-x | configure | 4 |
8 files changed, 2370 insertions, 2768 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 -> diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 71c0dba3..d52f3c24 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -475,11 +475,6 @@ Inductive instruction: Type := | Pcfi_adjust (ofs: int) (**r .cfi_adjust debug directive *) | Pcfi_rel_offset (ofs: int) (**r .cfi_rel_offset debug directive *) . - -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. *) @@ -541,6 +536,15 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) end. + +(** FIXME: not clear howto deal with these axioms in Asmblock. + The dependency over genv will get us in troubles... + +TODO: The solution is probably to put [symbol_low] and [symbol_high] [symbol_high_low] with any dependency on "ge" +as an hypothesis in RELSEM section. + +*) + (** 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: diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v new file mode 100644 index 00000000..83f2b96b --- /dev/null +++ b/aarch64/Asmblockgen.v @@ -0,0 +1,1197 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Justus Fasse UGA, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +(** * Translation from Machblock to AArch64 assembly block language (Asmblock) + Inspired from the Mach->Asm pass of original Leroy's backend, but adapted to the block structure like the KVX backend. *) + +Require Import Recdef Coqlib Zwf Zbits. +Require Import Errors AST Integers Floats Op. +Require Import Locations Machblock Asmblock. + +(* STUB *) +Definition transf_function (f: Machblock.function) : res Asmblock.function := + Error (msg "Asmblockgen not yet implmented"). + +Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := + transf_partial_fundef transf_function f. + +Definition transf_program (p: Machblock.program) : res Asmblock.program := + transform_partial_program transf_fundef p. + +(* ORIGINAL aarch64/Asmgen file that needs to be adapted + +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and INRIA Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Translation from Mach to AArch64. *) + +Require Import Recdef Coqlib Zwf Zbits. +Require Import Errors AST Integers Floats Op. +Require Import Locations Mach Asm. + +Local Open Scope string_scope. +Local Open Scope list_scope. +Local Open Scope error_monad_scope. + +(** Alignment check for symbols *) + +Parameter symbol_is_aligned : ident -> Z -> bool. +(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) + +(** Extracting integer or float registers. *) + +Definition ireg_of (r: mreg) : res ireg := + match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end. + +Definition freg_of (r: mreg) : res freg := + match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end. + +(** Recognition of immediate arguments for logical integer operations.*) + +(** Valid immediate arguments are repetitions of a bit pattern [B] + of length [e] = 2, 4, 8, 16, 32 or 64. + The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*] + but must not be all zeros or all ones. *) + +(** The following automaton recognizes [0*1*0*|1*0*1*]. +<< + 0 1 0 + / \ / \ / \ + \ / \ / \ / + -0--> [B] --1--> [D] --0--> [F] + / + [A] + \ + -1--> [C] --0--> [E] --1--> [G] + / \ / \ / \ + \ / \ / \ / + 1 0 1 +>> +*) + +Module Automaton. + +Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad. + +Definition start := SA. + +Definition next (s: state) (b: bool) := + match s, b with + | SA,false => SB | SA,true => SC + | SB,false => SB | SB,true => SD + | SC,false => SE | SC,true => SC + | SD,false => SF | SD,true => SD + | SE,false => SE | SE,true => SG + | SF,false => SF | SF,true => Sbad + | SG,false => Sbad | SG,true => SG + | Sbad,_ => Sbad + end. + +Definition accepting (s: state) := + match s with + | SA | SB | SC | SD | SE | SF | SG => true + | Sbad => false + end. + +Fixpoint run (len: nat) (s: state) (x: Z) : bool := + match len with + | Datatypes.O => accepting s + | Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x) + end. + +End Automaton. + +(** The following function determines the candidate length [e], + ensuring that [x] is a repetition [BB...B] + of a bit pattern [B] of length [e]. *) + +Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat := + (** [test n] checks that the low [2n] bits of [x] are of the + form [BB], that is, two occurrences of the same [n] bits *) + let test (n: Z) : bool := + Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in + (** If [test n] fails, we know that the candidate length [e] is + at least [2n]. Hence we test with decreasing values of [n]: + 32, 16, 8, 4, 2. *) + if sixtyfour && negb (test 32) then 64%nat + else if negb (test 16) then 32%nat + else if negb (test 8) then 16%nat + else if negb (test 4) then 8%nat + else if negb (test 2) then 4%nat + else 2%nat. + +(** A valid logical immediate is +- neither [0] nor [-1]; +- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e] +- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*]. +*) + +Definition is_logical_imm32 (x: int) : bool := + negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) && + Automaton.run (logical_imm_length (Int.unsigned x) false) + Automaton.start (Int.unsigned x). + +Definition is_logical_imm64 (x: int64) : bool := + negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) && + Automaton.run (logical_imm_length (Int64.unsigned x) true) + Automaton.start (Int64.unsigned x). + +(** Arithmetic immediates are 12-bit unsigned numbers, possibly shifted left 12 bits *) + +Definition is_arith_imm32 (x: int) : bool := + Int.eq x (Int.zero_ext 12 x) + || Int.eq x (Int.shl (Int.zero_ext 12 (Int.shru x (Int.repr 12))) (Int.repr 12)). + +Definition is_arith_imm64 (x: int64) : bool := + Int64.eq x (Int64.zero_ext 12 x) + || Int64.eq x (Int64.shl (Int64.zero_ext 12 (Int64.shru x (Int64.repr 12))) (Int64.repr 12)). + +(** Decompose integer literals into 16-bit fragments *) + +Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) := + match N with + | Datatypes.O => nil + | Datatypes.S N => + let frag := Zzero_ext 16 (Z.shiftr n p) in + if Z.eqb frag 0 then + decompose_int N n (p + 16) + else + (frag, p) :: decompose_int N (Z.ldiff n (Z.shiftl 65535 p)) (p + 16) + end. + +Definition negate_decomposition (l: list (Z * Z)) := + List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l. + +Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := + List.fold_right (fun np k => Pmovk sz rd (fst np) (snd np) :: k) k l. + +Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := + match l with + | nil => Pmovz sz rd 0 0 :: k + | (n1, p1) :: l => Pmovz sz rd n1 p1 :: loadimm_k sz rd l k + end. + +Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := + match l with + | nil => Pmovn sz rd 0 0 :: k + | (n1, p1) :: l => Pmovn sz rd n1 p1 :: loadimm_k sz rd (negate_decomposition l) k + end. + +Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: code) : code := + let N := match sz with W => 2%nat | X => 4%nat end in + let dz := decompose_int N n 0 in + let dn := decompose_int N (Z.lnot n) 0 in + if Nat.leb (List.length dz) (List.length dn) + then loadimm_z sz rd dz k + else loadimm_n sz rd dn k. + +Definition loadimm32 (rd: ireg) (n: int) (k: code) : code := + if is_logical_imm32 n + then Porrimm W rd XZR (Int.unsigned n) :: k + else loadimm W rd (Int.unsigned n) k. + +Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code := + if is_logical_imm64 n + then Porrimm X rd XZR (Int64.unsigned n) :: k + else loadimm X rd (Int64.unsigned n) k. + +(** Add immediate *) + +Definition addimm_aux (insn: iregsp -> iregsp -> Z -> instruction) + (rd r1: iregsp) (n: Z) (k: code) := + let nlo := Zzero_ext 12 n in + let nhi := n - nlo in + if Z.eqb nhi 0 then + insn rd r1 nlo :: k + else if Z.eqb nlo 0 then + insn rd r1 nhi :: k + else + insn rd r1 nhi :: insn rd rd nlo :: k. + +Definition addimm32 (rd r1: ireg) (n: int) (k: code) : code := + let m := Int.neg n in + if Int.eq n (Int.zero_ext 24 n) then + addimm_aux (Paddimm W) rd r1 (Int.unsigned n) k + else if Int.eq m (Int.zero_ext 24 m) then + addimm_aux (Psubimm W) rd r1 (Int.unsigned m) k + else if Int.lt n Int.zero then + loadimm32 X16 m (Psub W rd r1 X16 SOnone :: k) + else + loadimm32 X16 n (Padd W rd r1 X16 SOnone :: k). + +Definition addimm64 (rd r1: iregsp) (n: int64) (k: code) : code := + let m := Int64.neg n in + if Int64.eq n (Int64.zero_ext 24 n) then + addimm_aux (Paddimm X) rd r1 (Int64.unsigned n) k + else if Int64.eq m (Int64.zero_ext 24 m) then + addimm_aux (Psubimm X) rd r1 (Int64.unsigned m) k + else if Int64.lt n Int64.zero then + loadimm64 X16 m (Psubext rd r1 X16 (EOuxtx Int.zero) :: k) + else + loadimm64 X16 n (Paddext rd r1 X16 (EOuxtx Int.zero) :: k). + +(** Logical immediate *) + +Definition logicalimm32 + (insn1: ireg -> ireg0 -> Z -> instruction) + (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction) + (rd r1: ireg) (n: int) (k: code) : code := + if is_logical_imm32 n + then insn1 rd r1 (Int.unsigned n) :: k + else loadimm32 X16 n (insn2 rd r1 X16 SOnone :: k). + +Definition logicalimm64 + (insn1: ireg -> ireg0 -> Z -> instruction) + (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction) + (rd r1: ireg) (n: int64) (k: code) : code := + if is_logical_imm64 n + then insn1 rd r1 (Int64.unsigned n) :: k + else loadimm64 X16 n (insn2 rd r1 X16 SOnone :: k). + +(** Sign- or zero-extended arithmetic *) + +Definition transl_extension (ex: extension) (a: int) : extend_op := + match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end. + +Definition move_extended_base + (rd: ireg) (r1: ireg) (ex: extension) (k: code) : code := + match ex with + | Xsgn32 => Pcvtsw2x rd r1 :: k + | Xuns32 => Pcvtuw2x rd r1 :: k + end. + +Definition move_extended + (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: code) : code := + if Int.eq a Int.zero then + move_extended_base rd r1 ex k + else + move_extended_base rd r1 ex (Padd X rd XZR rd (SOlsl a) :: k). + +Definition arith_extended + (insnX: iregsp -> iregsp -> ireg -> extend_op -> instruction) + (insnS: ireg -> ireg0 -> ireg -> shift_op -> instruction) + (rd r1 r2: ireg) (ex: extension) (a: int) (k: code) : code := + if Int.ltu a (Int.repr 5) then + insnX rd r1 r2 (transl_extension ex a) :: k + else + move_extended_base X16 r2 ex (insnS rd r1 X16 (SOlsl a) :: k). + +(** Extended right shift *) + +Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code := + if Int.eq n Int.zero then + Pmov rd r1 :: k + else if Int.eq n Int.one then + Padd W X16 r1 r1 (SOlsr (Int.repr 31)) :: + Porr W rd XZR X16 (SOasr n) :: k + else + Porr W X16 XZR r1 (SOasr (Int.repr 31)) :: + Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) :: + Porr W rd XZR X16 (SOasr n) :: k. + +Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code := + if Int.eq n Int.zero then + Pmov rd r1 :: k + else if Int.eq n Int.one then + Padd X X16 r1 r1 (SOlsr (Int.repr 63)) :: + Porr X rd XZR X16 (SOasr n) :: k + else + Porr X X16 XZR r1 (SOasr (Int.repr 63)) :: + Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) :: + Porr X rd XZR X16 (SOasr n) :: k. + +(** Load the address [id + ofs] in [rd] *) + +Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: code) : code := + if Archi.pic_code tt then + if Ptrofs.eq ofs Ptrofs.zero then + Ploadsymbol rd id :: k + else + Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k + else + Padrp rd id ofs :: Paddadr rd rd id ofs :: k. + +(** Translate a shifted operand *) + +Definition transl_shift (s: Op.shift) (a: int): Asm.shift_op := + match s with + | Slsl => SOlsl a + | Slsr => SOlsr a + | Sasr => SOasr a + | Sror => SOror a + end. + +(** Translation of a condition. Prepends to [k] the instructions + that evaluate the condition and leave its boolean result in one of + the bits of the condition register. The bit in question is + determined by the [crbit_for_cond] function. *) + +Definition transl_cond + (cond: condition) (args: list mreg) (k: code) := + match cond, args with + | (Ccomp c | Ccompu c), a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp W r1 r2 SOnone :: k) + | (Ccompshift c s a | Ccompushift c s a), a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp W r1 r2 (transl_shift s a) :: k) + | (Ccompimm c n | Ccompuimm c n), a1 :: nil => + do r1 <- ireg_of a1; + OK (if is_arith_imm32 n then + Pcmpimm W r1 (Int.unsigned n) :: k + else if is_arith_imm32 (Int.neg n) then + Pcmnimm W r1 (Int.unsigned (Int.neg n)) :: k + else + loadimm32 X16 n (Pcmp W r1 X16 SOnone :: k)) + | (Cmaskzero n | Cmasknotzero n), a1 :: nil => + do r1 <- ireg_of a1; + OK (if is_logical_imm32 n then + Ptstimm W r1 (Int.unsigned n) :: k + else + loadimm32 X16 n (Ptst W r1 X16 SOnone :: k)) + | (Ccompl c | Ccomplu c), a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp X r1 r2 SOnone :: k) + | (Ccomplshift c s a | Ccomplushift c s a), a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pcmp X r1 r2 (transl_shift s a) :: k) + | (Ccomplimm c n | Ccompluimm c n), a1 :: nil => + do r1 <- ireg_of a1; + OK (if is_arith_imm64 n then + Pcmpimm X r1 (Int64.unsigned n) :: k + else if is_arith_imm64 (Int64.neg n) then + Pcmnimm X r1 (Int64.unsigned (Int64.neg n)) :: k + else + loadimm64 X16 n (Pcmp X r1 X16 SOnone :: k)) + | (Cmasklzero n | Cmasklnotzero n), a1 :: nil => + do r1 <- ireg_of a1; + OK (if is_logical_imm64 n then + Ptstimm X r1 (Int64.unsigned n) :: k + else + loadimm64 X16 n (Ptst X r1 X16 SOnone :: k)) + | Ccompf cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmp D r1 r2 :: k) + | Cnotcompf cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmp D r1 r2 :: k) + | Ccompfzero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmp0 D r1 :: k) + | Cnotcompfzero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmp0 D r1 :: k) + | Ccompfs cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmp S r1 r2 :: k) + | Cnotcompfs cmp, a1 :: a2 :: nil => + do r1 <- freg_of a1; do r2 <- freg_of a2; + OK (Pfcmp S r1 r2 :: k) + | Ccompfszero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmp0 S r1 :: k) + | Cnotcompfszero cmp, a1 :: nil => + do r1 <- freg_of a1; + OK (Pfcmp0 S r1 :: k) + | _, _ => + Error(msg "Asmgen.transl_cond") + end. + +Definition cond_for_signed_cmp (cmp: comparison) := + match cmp with + | Ceq => TCeq + | Cne => TCne + | Clt => TClt + | Cle => TCle + | Cgt => TCgt + | Cge => TCge + end. + +Definition cond_for_unsigned_cmp (cmp: comparison) := + match cmp with + | Ceq => TCeq + | Cne => TCne + | Clt => TClo + | Cle => TCls + | Cgt => TChi + | Cge => TChs + end. + +Definition cond_for_float_cmp (cmp: comparison) := + match cmp with + | Ceq => TCeq + | Cne => TCne + | Clt => TCmi + | Cle => TCls + | Cgt => TCgt + | Cge => TCge + end. + +Definition cond_for_float_not_cmp (cmp: comparison) := + match cmp with + | Ceq => TCne + | Cne => TCeq + | Clt => TCpl + | Cle => TChi + | Cgt => TCle + | Cge => TClt + end. + +Definition cond_for_cond (cond: condition) := + match cond with + | Ccomp cmp => cond_for_signed_cmp cmp + | Ccompu cmp => cond_for_unsigned_cmp cmp + | Ccompshift cmp s a => cond_for_signed_cmp cmp + | Ccompushift cmp s a => cond_for_unsigned_cmp cmp + | Ccompimm cmp n => cond_for_signed_cmp cmp + | Ccompuimm cmp n => cond_for_unsigned_cmp cmp + | Cmaskzero n => TCeq + | Cmasknotzero n => TCne + | Ccompl cmp => cond_for_signed_cmp cmp + | Ccomplu cmp => cond_for_unsigned_cmp cmp + | Ccomplshift cmp s a => cond_for_signed_cmp cmp + | Ccomplushift cmp s a => cond_for_unsigned_cmp cmp + | Ccomplimm cmp n => cond_for_signed_cmp cmp + | Ccompluimm cmp n => cond_for_unsigned_cmp cmp + | Cmasklzero n => TCeq + | Cmasklnotzero n => TCne + | Ccompf cmp => cond_for_float_cmp cmp + | Cnotcompf cmp => cond_for_float_not_cmp cmp + | Ccompfzero cmp => cond_for_float_cmp cmp + | Cnotcompfzero cmp => cond_for_float_not_cmp cmp + | Ccompfs cmp => cond_for_float_cmp cmp + | Cnotcompfs cmp => cond_for_float_not_cmp cmp + | Ccompfszero cmp => cond_for_float_cmp cmp + | Cnotcompfszero cmp => cond_for_float_not_cmp cmp + end. + +(** Translation of a conditional branch. Prepends to [k] the instructions + that evaluate the condition and ranch to [lbl] if it holds. + We recognize some conditional branches that can be implemented + without setting then testing condition flags. *) + +Definition transl_cond_branch_default + (c: condition) (args: list mreg) (lbl: label) (k: code) := + transl_cond c args (Pbc (cond_for_cond c) lbl :: k). + +Definition transl_cond_branch + (c: condition) (args: list mreg) (lbl: label) (k: code) := + match args, c with + | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) => + if Int.eq n Int.zero + then (do r1 <- ireg_of a1; OK (Pcbnz W r1 lbl :: k)) + else transl_cond_branch_default c args lbl k + | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) => + if Int.eq n Int.zero + then (do r1 <- ireg_of a1; OK (Pcbz W r1 lbl :: k)) + else transl_cond_branch_default c args lbl k + | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) => + if Int64.eq n Int64.zero + then (do r1 <- ireg_of a1; OK (Pcbnz X r1 lbl :: k)) + else transl_cond_branch_default c args lbl k + | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) => + if Int64.eq n Int64.zero + then (do r1 <- ireg_of a1; OK (Pcbz X r1 lbl :: k)) + else transl_cond_branch_default c args lbl k + | a1 :: nil, Cmaskzero n => + match Int.is_power2 n with + | Some bit => do r1 <- ireg_of a1; OK (Ptbz W r1 bit lbl :: k) + | None => transl_cond_branch_default c args lbl k + end + | a1 :: nil, Cmasknotzero n => + match Int.is_power2 n with + | Some bit => do r1 <- ireg_of a1; OK (Ptbnz W r1 bit lbl :: k) + | None => transl_cond_branch_default c args lbl k + end + | a1 :: nil, Cmasklzero n => + match Int64.is_power2' n with + | Some bit => do r1 <- ireg_of a1; OK (Ptbz X r1 bit lbl :: k) + | None => transl_cond_branch_default c args lbl k + end + | a1 :: nil, Cmasklnotzero n => + match Int64.is_power2' n with + | Some bit => do r1 <- ireg_of a1; OK (Ptbnz X r1 bit lbl :: k) + | None => transl_cond_branch_default c args lbl k + end + | _, _ => + transl_cond_branch_default c args lbl k + end. + +(** Translation of the arithmetic operation [res <- op(args)]. + The corresponding instructions are prepended to [k]. *) + +Definition transl_op + (op: operation) (args: list mreg) (res: mreg) (k: code) := + match op, args with + | Omove, a1 :: nil => + match preg_of res, preg_of a1 with + | IR r, IR a => OK (Pmov r a :: k) + | FR r, FR a => OK (Pfmov r a :: k) + | _ , _ => Error(msg "Asmgen.Omove") + end + | Ointconst n, nil => + do rd <- ireg_of res; + OK (loadimm32 rd n k) + | Olongconst n, nil => + do rd <- ireg_of res; + OK (loadimm64 rd n k) + | Ofloatconst f, nil => + do rd <- freg_of res; + OK (if Float.eq_dec f Float.zero + then Pfmovi D rd XZR :: k + else Pfmovimmd rd f :: k) + | Osingleconst f, nil => + do rd <- freg_of res; + OK (if Float32.eq_dec f Float32.zero + then Pfmovi S rd XZR :: k + else Pfmovimms rd f :: k) + | Oaddrsymbol id ofs, nil => + do rd <- ireg_of res; + OK (loadsymbol rd id ofs k) + | Oaddrstack ofs, nil => + do rd <- ireg_of res; + OK (addimm64 rd XSP (Ptrofs.to_int64 ofs) k) +(** 32-bit integer arithmetic *) + | Oshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porr W rd XZR r1 (transl_shift s a) :: k) + | Oadd, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd W rd r1 r2 SOnone :: k) + | Oaddshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd W rd r1 r2 (transl_shift s a) :: k) + | Oaddimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (addimm32 rd r1 n k) + | Oneg, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psub W rd XZR r1 SOnone :: k) + | Onegshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psub W rd XZR r1 (transl_shift s a) :: k) + | Osub, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub W rd r1 r2 SOnone :: k) + | Osubshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub W rd r1 r2 (transl_shift s a) :: k) + | Omul, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmadd W rd r1 r2 XZR :: k) + | Omuladd, a1 :: a2 :: a3 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (Pmadd W rd r2 r3 r1 :: k) + | Omulsub, a1 :: a2 :: a3 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (Pmsub W rd r2 r3 r1 :: k) + | Odiv, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psdiv W rd r1 r2 :: k) + | Odivu, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pudiv W rd r1 r2 :: k) + | Oand, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand W rd r1 r2 SOnone :: k) + | Oandshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand W rd r1 r2 (transl_shift s a) :: k) + | Oandimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm32 (Pandimm W) (Pand W) rd r1 n k) + | Oor, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr W rd r1 r2 SOnone :: k) + | Oorshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr W rd r1 r2 (transl_shift s a) :: k) + | Oorimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm32 (Porrimm W) (Porr W) rd r1 n k) + | Oxor, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor W rd r1 r2 SOnone :: k) + | Oxorshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor W rd r1 r2 (transl_shift s a) :: k) + | Oxorimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm32 (Peorimm W) (Peor W) rd r1 n k) + | Onot, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porn W rd XZR r1 SOnone :: k) + | Onotshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porn W rd XZR r1 (transl_shift s a) :: k) + | Obic, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic W rd r1 r2 SOnone :: k) + | Obicshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic W rd r1 r2 (transl_shift s a) :: k) + | Oorn, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porn W rd r1 r2 SOnone :: k) + | Oornshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porn W rd r1 r2 (transl_shift s a) :: k) + | Oeqv, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peon W rd r1 r2 SOnone :: k) + | Oeqvshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peon W rd r1 r2 (transl_shift s a) :: k) + | Oshl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Plslv W rd r1 r2 :: k) + | Oshr, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pasrv W rd r1 r2 :: k) + | Oshru, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Plsrv W rd r1 r2 :: k) + | Oshrximm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (shrx32 rd r1 n k) + | Ozext s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfiz W rd r1 Int.zero s :: k) + | Osext s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfiz W rd r1 Int.zero s :: k) + | Oshlzext s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) + | Oshlsext s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) + | Ozextshr a s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) + | Osextshr a s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) +(** 64-bit integer arithmetic *) + | Oshiftl s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porr X rd XZR r1 (transl_shift s a) :: k) + | Oextend x a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (move_extended rd r1 x a k) + (* [Omakelong] and [Ohighlong] should not occur *) + | Olowlong, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + assertion (ireg_eq rd r1); + OK (Pcvtx2w rd :: k) + | Oaddl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd X rd r1 r2 SOnone :: k) + | Oaddlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Padd X rd r1 r2 (transl_shift s a) :: k) + | Oaddlext x a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (arith_extended Paddext (Padd X) rd r1 r2 x a k) + | Oaddlimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (addimm64 rd r1 n k) + | Onegl, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psub X rd XZR r1 SOnone :: k) + | Oneglshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psub X rd XZR r1 (transl_shift s a) :: k) + | Osubl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub X rd r1 r2 SOnone :: k) + | Osublshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psub X rd r1 r2 (transl_shift s a) :: k) + | Osublext x a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (arith_extended Psubext (Psub X) rd r1 r2 x a k) + | Omull, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pmadd X rd r1 r2 XZR :: k) + | Omulladd, a1 :: a2 :: a3 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (Pmadd X rd r2 r3 r1 :: k) + | Omullsub, a1 :: a2 :: a3 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; + OK (Pmsub X rd r2 r3 r1 :: k) + | Omullhs, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psmulh rd r1 r2 :: k) + | Omullhu, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pumulh rd r1 r2 :: k) + | Odivl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Psdiv X rd r1 r2 :: k) + | Odivlu, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pudiv X rd r1 r2 :: k) + | Oandl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand X rd r1 r2 SOnone :: k) + | Oandlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pand X rd r1 r2 (transl_shift s a) :: k) + | Oandlimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm64 (Pandimm X) (Pand X) rd r1 n k) + | Oorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr X rd r1 r2 SOnone :: k) + | Oorlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porr X rd r1 r2 (transl_shift s a) :: k) + | Oorlimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm64 (Porrimm X) (Porr X) rd r1 n k) + | Oxorl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor X rd r1 r2 SOnone :: k) + | Oxorlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peor X rd r1 r2 (transl_shift s a) :: k) + | Oxorlimm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (logicalimm64 (Peorimm X) (Peor X) rd r1 n k) + | Onotl, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porn X rd XZR r1 SOnone :: k) + | Onotlshift s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Porn X rd XZR r1 (transl_shift s a) :: k) + | Obicl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic X rd r1 r2 SOnone :: k) + | Obiclshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pbic X rd r1 r2 (transl_shift s a) :: k) + | Oornl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porn X rd r1 r2 SOnone :: k) + | Oornlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Porn X rd r1 r2 (transl_shift s a) :: k) + | Oeqvl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peon X rd r1 r2 SOnone :: k) + | Oeqvlshift s a, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Peon X rd r1 r2 (transl_shift s a) :: k) + | Oshll, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Plslv X rd r1 r2 :: k) + | Oshrl, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Pasrv X rd r1 r2 :: k) + | Oshrlu, a1 :: a2 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (Plsrv X rd r1 r2 :: k) + | Oshrlximm n, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (shrx64 rd r1 n k) + | Ozextl s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfiz X rd r1 Int.zero s :: k) + | Osextl s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfiz X rd r1 Int.zero s :: k) + | Oshllzext s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) + | Oshllsext s a, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) + | Ozextshrl a s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Pubfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) + | Osextshrl a s, a1 :: nil => + do rd <- ireg_of res; do r1 <- ireg_of a1; + OK (Psbfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) +(** 64-bit floating-point arithmetic *) + | Onegf, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfneg D rd rs :: k) + | Oabsf, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfabs D rd rs :: k) + | Oaddf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfadd D rd rs1 rs2 :: k) + | Osubf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfsub D rd rs1 rs2 :: k) + | Omulf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmul D rd rs1 rs2 :: k) + | Odivf, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfdiv D rd rs1 rs2 :: k) +(** 32-bit floating-point arithmetic *) + | Onegfs, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfneg S rd rs :: k) + | Oabsfs, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfabs S rd rs :: k) + | Oaddfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfadd S rd rs1 rs2 :: k) + | Osubfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfsub S rd rs1 rs2 :: k) + | Omulfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfmul S rd rs1 rs2 :: k) + | Odivfs, a1 :: a2 :: nil => + do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; + OK (Pfdiv S rd rs1 rs2 :: k) + | Osingleoffloat, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfcvtsd rd rs :: k) + | Ofloatofsingle, a1 :: nil => + do rd <- freg_of res; do rs <- freg_of a1; + OK (Pfcvtds rd rs :: k) +(** Conversions between int and float *) + | Ointoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzs W D rd rs :: k) + | Ointuoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzu W D rd rs :: k) + | Ofloatofint, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pscvtf D W rd rs :: k) + | Ofloatofintu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pucvtf D W rd rs :: k) + | Ointofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzs W S rd rs :: k) + | Ointuofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzu W S rd rs :: k) + | Osingleofint, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pscvtf S W rd rs :: k) + | Osingleofintu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pucvtf S W rd rs :: k) + | Olongoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzs X D rd rs :: k) + | Olonguoffloat, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzu X D rd rs :: k) + | Ofloatoflong, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pscvtf D X rd rs :: k) + | Ofloatoflongu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pucvtf D X rd rs :: k) + | Olongofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzs X S rd rs :: k) + | Olonguofsingle, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfcvtzu X S rd rs :: k) + | Osingleoflong, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pscvtf S X rd rs :: k) + | Osingleoflongu, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pucvtf S X rd rs :: k) +(** Boolean tests *) + | Ocmp c, _ => + do rd <- ireg_of res; + transl_cond c args (Pcset rd (cond_for_cond c) :: k) +(** Conditional move *) + | Osel cmp ty, a1 :: a2 :: args => + match preg_of res with + | IR r => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) :: k) + | FR r => + do r1 <- freg_of a1; do r2 <- freg_of a2; + transl_cond cmp args (Pfsel r r1 r2 (cond_for_cond cmp) :: k) + | _ => + Error(msg "Asmgen.Osel") + end + | _, _ => + Error(msg "Asmgen.transl_op") + end. + +(** Translation of addressing modes *) + +Definition offset_representable (sz: Z) (ofs: int64) : bool := + let isz := Int64.repr sz in + (** either unscaled 9-bit signed *) + Int64.eq ofs (Int64.sign_ext 9 ofs) || + (** or scaled 12-bit unsigned *) + (Int64.eq (Int64.modu ofs isz) Int64.zero + && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))). + +Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) + (insn: Asm.addressing -> instruction) (k: code) : res code := + match addr, args with + | Aindexed ofs, a1 :: nil => + do r1 <- ireg_of a1; + if offset_representable sz ofs then + OK (insn (ADimm r1 ofs) :: k) + else + OK (loadimm64 X16 ofs (insn (ADreg r1 X16) :: k)) + | Aindexed2, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (insn (ADreg r1 r2) :: k) + | Aindexed2shift a, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + if Int.eq a Int.zero then + OK (insn (ADreg r1 r2) :: k) + else if Int.eq (Int.shl Int.one a) (Int.repr sz) then + OK (insn (ADlsl r1 r2 a) :: k) + else + OK (Padd X X16 r1 r2 (SOlsl a) :: insn (ADimm X16 Int64.zero) :: k) + | Aindexed2ext x a, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then + OK (insn (match x with Xsgn32 => ADsxt r1 r2 a + | Xuns32 => ADuxt r1 r2 a end) :: k) + else + OK (arith_extended Paddext (Padd X) X16 r1 r2 x a + (insn (ADimm X16 Int64.zero) :: k)) + | Aglobal id ofs, nil => + assertion (negb (Archi.pic_code tt)); + if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz + then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k) + else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k)) + | Ainstack ofs, nil => + let ofs := Ptrofs.to_int64 ofs in + if offset_representable sz ofs then + OK (insn (ADimm XSP ofs) :: k) + else + OK (loadimm64 X16 ofs (insn (ADreg XSP X16) :: k)) + | _, _ => + Error(msg "Asmgen.transl_addressing") + end. + +(** Translation of loads and stores *) + +Definition transl_load (trap: trapping_mode) + (chunk: memory_chunk) (addr: Op.addressing) + (args: list mreg) (dst: mreg) (k: code) : res code := + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64") + | TRAP => + match chunk with + | Mint8unsigned => + do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrb W rd) k + | Mint8signed => + do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrsb W rd) k + | Mint16unsigned => + do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrh W rd) k + | Mint16signed => + do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrsh W rd) k + | Mint32 => + do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw rd) k + | Mint64 => + do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx rd) k + | Mfloat32 => + do rd <- freg_of dst; transl_addressing 4 addr args (Pldrs rd) k + | Mfloat64 => + do rd <- freg_of dst; transl_addressing 8 addr args (Pldrd rd) k + | Many32 => + do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw_a rd) k + | Many64 => + do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx_a rd) k + end + end. + +Definition transl_store (chunk: memory_chunk) (addr: Op.addressing) + (args: list mreg) (src: mreg) (k: code) : res code := + match chunk with + | Mint8unsigned | Mint8signed => + do r1 <- ireg_of src; transl_addressing 1 addr args (Pstrb r1) k + | Mint16unsigned | Mint16signed => + do r1 <- ireg_of src; transl_addressing 2 addr args (Pstrh r1) k + | Mint32 => + do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw r1) k + | Mint64 => + do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx r1) k + | Mfloat32 => + do r1 <- freg_of src; transl_addressing 4 addr args (Pstrs r1) k + | Mfloat64 => + do r1 <- freg_of src; transl_addressing 8 addr args (Pstrd r1) k + | Many32 => + do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw_a r1) k + | Many64 => + do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx_a r1) k + end. + +(** Register-indexed loads and stores *) + +Definition indexed_memory_access (insn: Asm.addressing -> instruction) + (sz: Z) (base: iregsp) (ofs: ptrofs) (k: code) := + let ofs := Ptrofs.to_int64 ofs in + if offset_representable sz ofs + then insn (ADimm base ofs) :: k + else loadimm64 X16 ofs (insn (ADreg base X16) :: k). + +Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := + match ty, preg_of dst with + | Tint, IR rd => OK (indexed_memory_access (Pldrw rd) 4 base ofs k) + | Tlong, IR rd => OK (indexed_memory_access (Pldrx rd) 8 base ofs k) + | Tsingle, FR rd => OK (indexed_memory_access (Pldrs rd) 4 base ofs k) + | Tfloat, FR rd => OK (indexed_memory_access (Pldrd rd) 8 base ofs k) + | Tany32, IR rd => OK (indexed_memory_access (Pldrw_a rd) 4 base ofs k) + | Tany64, IR rd => OK (indexed_memory_access (Pldrx_a rd) 8 base ofs k) + | Tany64, FR rd => OK (indexed_memory_access (Pldrd_a rd) 8 base ofs k) + | _, _ => Error (msg "Asmgen.loadind") + end. + +Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: code) := + match ty, preg_of src with + | Tint, IR rd => OK (indexed_memory_access (Pstrw rd) 4 base ofs k) + | Tlong, IR rd => OK (indexed_memory_access (Pstrx rd) 8 base ofs k) + | Tsingle, FR rd => OK (indexed_memory_access (Pstrs rd) 4 base ofs k) + | Tfloat, FR rd => OK (indexed_memory_access (Pstrd rd) 8 base ofs k) + | Tany32, IR rd => OK (indexed_memory_access (Pstrw_a rd) 4 base ofs k) + | Tany64, IR rd => OK (indexed_memory_access (Pstrx_a rd) 8 base ofs k) + | Tany64, FR rd => OK (indexed_memory_access (Pstrd_a rd) 8 base ofs k) + | _, _ => Error (msg "Asmgen.storeind") + end. + +Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: code) := + indexed_memory_access (Pldrx dst) 8 base ofs k. + +Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) := + indexed_memory_access (Pstrx src) 8 base ofs k. + +(** Function epilogue *) + +Definition make_epilogue (f: Mach.function) (k: code) := + (* 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) :: k). + +(** Translation of a Mach instruction. *) + +Definition transl_instr (f: Mach.function) (i: Mach.instruction) + (r29_is_parent: bool) (k: code) : res code := + match i with + | Mgetstack ofs ty dst => + loadind XSP ofs ty dst k + | Msetstack src ofs ty => + storeind src XSP ofs ty k + | Mgetparam ofs ty dst => + (* load via the frame pointer if it is valid *) + do c <- loadind X29 ofs ty dst k; + OK (if r29_is_parent then c else loadptr XSP f.(fn_link_ofs) X29 c) + | Mop op args res => + transl_op op args res k + | Mload trap chunk addr args dst => + transl_load trap chunk addr args dst k + | Mstore chunk addr args src => + transl_store chunk addr args src k + | Mcall sig (inl r) => + do r1 <- ireg_of r; OK (Pblr r1 sig :: k) + | Mcall sig (inr symb) => + OK (Pbl symb sig :: k) + | Mtailcall sig (inl r) => + do r1 <- ireg_of r; + OK (make_epilogue f (Pbr r1 sig :: k)) + | Mtailcall sig (inr symb) => + OK (make_epilogue f (Pbs symb sig :: k)) + | Mbuiltin ef args res => + OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) + | Mlabel lbl => + OK (Plabel lbl :: k) + | Mgoto lbl => + OK (Pb lbl :: k) + | Mcond cond args lbl => + transl_cond_branch cond args lbl k + | Mjumptable arg tbl => + do r <- ireg_of arg; + OK (Pbtbl r tbl :: k) + | Mreturn => + OK (make_epilogue f (Pret RA :: k)) + end. + +(** Translation of a code sequence *) + +Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := + match i with + | Msetstack src ofs ty => before + | Mgetparam ofs ty dst => negb (mreg_eq dst R29) + | Mop op args res => before && negb (mreg_eq res R29) + | _ => false + end. + +(** This is the naive definition that we no longer use because it + is not tail-recursive. It is kept as specification. *) + +Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := + match il with + | nil => OK nil + | i1 :: il' => + do k <- transl_code f il' (it1_is_parent it1p i1); + transl_instr f i1 it1p k + end. + +(** This is an equivalent definition in continuation-passing style + that runs in constant stack space. *) + +Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction) + (it1p: bool) (k: code -> res code) := + match il with + | nil => k nil + | i1 :: il' => + transl_code_rec f il' (it1_is_parent it1p i1) + (fun c1 => do c2 <- transl_instr f i1 it1p c1; k c2) + end. + +Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := + transl_code_rec f il it1p (fun c => OK c). + +(** Translation of a whole function. Note that we must check + that the generated code contains less than [2^32] instructions, + otherwise the offset part of the [PC] code pointer could wrap + around, leading to incorrect executions. *) + +Definition transl_function (f: Mach.function) := + do c <- transl_code' f f.(Mach.fn_code) true; + OK (mkfunction f.(Mach.fn_sig) + (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: + storeptr RA XSP f.(fn_retaddr_ofs) c)). + +*)
\ No newline at end of file diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v new file mode 100644 index 00000000..bcd4495f --- /dev/null +++ b/aarch64/Asmblockgenproof.v @@ -0,0 +1,1104 @@ +(* ORIGINAL aarch64/Asmgenproof file that needs to be adapted + +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, Collège de France and INRIA Paris *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness proof for AArch64 code generation. *) + +Require Import Coqlib Errors. +Require Import Integers Floats AST Linking. +Require Import Values Memory Events Globalenvs Smallstep. +Require Import Op Locations Mach Conventions Asm. +Require Import Asmgen Asmgenproof0 Asmgenproof1. + +Definition match_prog (p: Mach.program) (tp: Asm.program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall p tp, transf_program p = OK tp -> match_prog p tp. +Proof. + intros. eapply match_transform_partial_program; eauto. +Qed. + +Section PRESERVATION. + +Variable prog: Mach.program. +Variable tprog: Asm.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSF). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). + +Lemma functions_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial TRANSF). + +Lemma functions_transl: + forall fb f tf, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transf_function f = OK tf -> + Genv.find_funct_ptr tge fb = Some (Internal tf). +Proof. + intros. exploit functions_translated; eauto. intros [tf' [A B]]. + monadInv B. rewrite H0 in EQ; inv EQ; auto. +Qed. + +(** * Properties of control flow *) + +Lemma transf_function_no_overflow: + forall f tf, + transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. +Proof. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. + omega. +Qed. + +Lemma exec_straight_exec: + forall fb f c ep tf tc c' rs m rs' m', + transl_code_at_pc ge (rs PC) fb f c ep tf tc -> + exec_straight tge tf tc rs m c' rs' m' -> + plus step tge (State rs m) E0 (State rs' m'). +Proof. + intros. inv H. + eapply exec_straight_steps_1; eauto. + eapply transf_function_no_overflow; eauto. + eapply functions_transl; eauto. +Qed. + +Lemma exec_straight_at: + forall fb f c ep tf tc c' ep' tc' rs m rs' m', + transl_code_at_pc ge (rs PC) fb f c ep tf tc -> + transl_code f c' ep' = OK tc' -> + exec_straight tge tf tc rs m tc' rs' m' -> + transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'. +Proof. + intros. inv H. + exploit exec_straight_steps_2; eauto. + eapply transf_function_no_overflow; eauto. + eapply functions_transl; eauto. + intros [ofs' [PC' CT']]. + rewrite PC'. constructor; auto. +Qed. + +(** The following lemmas show that the translation from Mach to Asm + preserves labels, in the sense that the following diagram commutes: +<< + translation + Mach code ------------------------ Asm instr sequence + | | + | Mach.find_label lbl find_label lbl | + | | + v v + Mach code tail ------------------- Asm instr seq tail + translation +>> + The proof demands many boring lemmas showing that Asm constructor + functions do not introduce new labels. +*) + +Section TRANSL_LABEL. + +Remark loadimm_z_label: forall sz rd l k, tail_nolabel k (loadimm_z sz rd l k). +Proof. + intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel. + induction l as [ | [n p] l]; simpl; TailNoLabel. +Qed. + +Remark loadimm_n_label: forall sz rd l k, tail_nolabel k (loadimm_n sz rd l k). +Proof. + intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel. + induction l as [ | [n p] l]; simpl; TailNoLabel. +Qed. + +Remark loadimm_label: forall sz rd n k, tail_nolabel k (loadimm sz rd n k). +Proof. + unfold loadimm; intros. destruct Nat.leb; [apply loadimm_z_label|apply loadimm_n_label]. +Qed. +Hint Resolve loadimm_label: labels. + +Remark loadimm32_label: forall r n k, tail_nolabel k (loadimm32 r n k). +Proof. + unfold loadimm32; intros. destruct (is_logical_imm32 n); TailNoLabel. +Qed. +Hint Resolve loadimm32_label: labels. + +Remark loadimm64_label: forall r n k, tail_nolabel k (loadimm64 r n k). +Proof. + unfold loadimm64; intros. destruct (is_logical_imm64 n); TailNoLabel. +Qed. +Hint Resolve loadimm64_label: labels. + +Remark addimm_aux: forall insn rd r1 n k, + (forall rd r1 n, nolabel (insn rd r1 n)) -> + tail_nolabel k (addimm_aux insn rd r1 n k). +Proof. + unfold addimm_aux; intros. + destruct Z.eqb. TailNoLabel. destruct Z.eqb; TailNoLabel. +Qed. + +Remark addimm32_label: forall rd r1 n k, tail_nolabel k (addimm32 rd r1 n k). +Proof. + unfold addimm32; intros. + destruct Int.eq. apply addimm_aux; intros; red; auto. + destruct Int.eq. apply addimm_aux; intros; red; auto. + destruct Int.lt; eapply tail_nolabel_trans; TailNoLabel. +Qed. +Hint Resolve addimm32_label: labels. + +Remark addimm64_label: forall rd r1 n k, tail_nolabel k (addimm64 rd r1 n k). +Proof. + unfold addimm64; intros. + destruct Int64.eq. apply addimm_aux; intros; red; auto. + destruct Int64.eq. apply addimm_aux; intros; red; auto. + destruct Int64.lt; eapply tail_nolabel_trans; TailNoLabel. +Qed. +Hint Resolve addimm64_label: labels. + +Remark logicalimm32_label: forall insn1 insn2 rd r1 n k, + (forall rd r1 n, nolabel (insn1 rd r1 n)) -> + (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) -> + tail_nolabel k (logicalimm32 insn1 insn2 rd r1 n k). +Proof. + unfold logicalimm32; intros. + destruct (is_logical_imm32 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +Qed. + +Remark logicalimm64_label: forall insn1 insn2 rd r1 n k, + (forall rd r1 n, nolabel (insn1 rd r1 n)) -> + (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) -> + tail_nolabel k (logicalimm64 insn1 insn2 rd r1 n k). +Proof. + unfold logicalimm64; intros. + destruct (is_logical_imm64 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +Qed. + +Remark move_extended_label: forall rd r1 ex a k, tail_nolabel k (move_extended rd r1 ex a k). +Proof. + unfold move_extended, move_extended_base; intros. destruct Int.eq, ex; TailNoLabel. +Qed. +Hint Resolve move_extended_label: labels. + +Remark arith_extended_label: forall insnX insnS rd r1 r2 ex a k, + (forall rd r1 r2 x, nolabel (insnX rd r1 r2 x)) -> + (forall rd r1 r2 s, nolabel (insnS rd r1 r2 s)) -> + tail_nolabel k (arith_extended insnX insnS rd r1 r2 ex a k). +Proof. + unfold arith_extended; intros. destruct Int.ltu. + TailNoLabel. + destruct ex; simpl; TailNoLabel. +Qed. + +Remark loadsymbol_label: forall r id ofs k, tail_nolabel k (loadsymbol r id ofs k). +Proof. + intros; unfold loadsymbol. + destruct (Archi.pic_code tt); TailNoLabel. destruct Ptrofs.eq; TailNoLabel. +Qed. +Hint Resolve loadsymbol_label: labels. + +Remark transl_cond_label: forall cond args k c, + transl_cond cond args k = OK c -> tail_nolabel k c. +Proof. + unfold transl_cond; intros; destruct cond; TailNoLabel. +- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. +Qed. + +Remark transl_cond_branch_default_label: forall cond args lbl k c, + transl_cond_branch_default cond args lbl k = OK c -> tail_nolabel k c. +Proof. + unfold transl_cond_branch_default; intros. + eapply tail_nolabel_trans; [eapply transl_cond_label;eauto|TailNoLabel]. +Qed. +Hint Resolve transl_cond_branch_default_label: labels. + +Remark transl_cond_branch_label: forall cond args lbl k c, + transl_cond_branch cond args lbl k = OK c -> tail_nolabel k c. +Proof. + unfold transl_cond_branch; intros; destruct args; TailNoLabel; destruct cond; TailNoLabel. +- destruct c0; TailNoLabel. +- destruct c0; TailNoLabel. +- destruct (Int.is_power2 n); TailNoLabel. +- destruct (Int.is_power2 n); TailNoLabel. +- destruct c0; TailNoLabel. +- destruct c0; TailNoLabel. +- destruct (Int64.is_power2' n); TailNoLabel. +- destruct (Int64.is_power2' n); TailNoLabel. +Qed. + +Remark transl_op_label: + forall op args r k c, + transl_op op args r k = OK c -> tail_nolabel k c. +Proof. + unfold transl_op; intros; destruct op; TailNoLabel. +- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. +- destruct (Float.eq_dec n Float.zero); TailNoLabel. +- destruct (Float32.eq_dec n Float32.zero); TailNoLabel. +- apply logicalimm32_label; unfold nolabel; auto. +- apply logicalimm32_label; unfold nolabel; auto. +- apply logicalimm32_label; unfold nolabel; auto. +- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. +- apply arith_extended_label; unfold nolabel; auto. +- apply arith_extended_label; unfold nolabel; auto. +- apply logicalimm64_label; unfold nolabel; auto. +- apply logicalimm64_label; unfold nolabel; auto. +- apply logicalimm64_label; unfold nolabel; auto. +- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. +- eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. +- destruct (preg_of r); try discriminate; TailNoLabel; + (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]). +Qed. + +Remark transl_addressing_label: + forall sz addr args insn k c, + transl_addressing sz addr args insn k = OK c -> + (forall ad, nolabel (insn ad)) -> + tail_nolabel k c. +Proof. + unfold transl_addressing; intros; destruct addr; TailNoLabel; + eapply tail_nolabel_trans; TailNoLabel. + eapply tail_nolabel_trans. apply arith_extended_label; unfold nolabel; auto. TailNoLabel. +Qed. + +Remark transl_load_label: + forall trap chunk addr args dst k c, + transl_load trap chunk addr args dst k = OK c -> tail_nolabel k c. +Proof. + unfold transl_load; intros; destruct trap; try discriminate; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto. +Qed. + +Remark transl_store_label: + forall chunk addr args src k c, + transl_store chunk addr args src k = OK c -> tail_nolabel k c. +Proof. + unfold transl_store; intros; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto. +Qed. + +Remark indexed_memory_access_label: + forall insn sz base ofs k, + (forall ad, nolabel (insn ad)) -> + tail_nolabel k (indexed_memory_access insn sz base ofs k). +Proof. + unfold indexed_memory_access; intros. destruct offset_representable. + TailNoLabel. + eapply tail_nolabel_trans; TailNoLabel. +Qed. + +Remark loadind_label: + forall base ofs ty dst k c, + loadind base ofs ty dst k = OK c -> tail_nolabel k c. +Proof. + unfold loadind; intros. + destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I. +Qed. + +Remark storeind_label: + forall src base ofs ty k c, + storeind src base ofs ty k = OK c -> tail_nolabel k c. +Proof. + unfold storeind; intros. + destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I. +Qed. + +Remark loadptr_label: + forall base ofs dst k, tail_nolabel k (loadptr base ofs dst k). +Proof. + intros. apply indexed_memory_access_label. unfold nolabel; auto. +Qed. + +Remark storeptr_label: + forall src base ofs k, tail_nolabel k (storeptr src base ofs k). +Proof. + intros. apply indexed_memory_access_label. unfold nolabel; auto. +Qed. + +Remark make_epilogue_label: + forall f k, tail_nolabel k (make_epilogue f k). +Proof. + unfold make_epilogue; intros. + (* FIXME destruct is_leaf_function. + { TailNoLabel. } *) + eapply tail_nolabel_trans. + apply loadptr_label. + TailNoLabel. +Qed. + +Lemma transl_instr_label: + forall f i ep k c, + transl_instr f i ep k = OK c -> + match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end. +Proof. + unfold transl_instr; intros; destruct i; TailNoLabel. +- eapply loadind_label; eauto. +- eapply storeind_label; eauto. +- destruct ep. eapply loadind_label; eauto. + eapply tail_nolabel_trans. apply loadptr_label. eapply loadind_label; eauto. +- eapply transl_op_label; eauto. +- eapply transl_load_label; eauto. +- eapply transl_store_label; eauto. +- destruct s0; monadInv H; TailNoLabel. +- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]). +- eapply transl_cond_branch_label; eauto. +- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]. +Qed. + +Lemma transl_instr_label': + forall lbl f i ep k c, + transl_instr f i ep k = OK c -> + find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. +Proof. + intros. exploit transl_instr_label; eauto. + destruct i; try (intros [A B]; apply B). + intros. subst c. simpl. auto. +Qed. + +Lemma transl_code_label: + forall lbl f c ep tc, + transl_code f c ep = OK tc -> + match Mach.find_label lbl c with + | None => find_label lbl tc = None + | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc' + end. +Proof. + induction c; simpl; intros. + inv H. auto. + monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0). + generalize (Mach.is_label_correct lbl a). + destruct (Mach.is_label lbl a); intros. + subst a. simpl in EQ. exists x; auto. + eapply IHc; eauto. +Qed. + +Lemma transl_find_label: + forall lbl f tf, + transf_function f = OK tf -> + match Mach.find_label lbl f.(Mach.fn_code) with + | None => find_label lbl tf.(fn_code) = None + | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc + end. +Proof. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. + monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. + simpl. destruct (storeptr_label X30 XSP (fn_retaddr_ofs f) x) as [A B]; rewrite B. + eapply transl_code_label; eauto. +Qed. + +End TRANSL_LABEL. + +(** A valid branch in a piece of Mach code translates to a valid ``go to'' + transition in the generated Asm code. *) + +Lemma find_label_goto_label: + forall f tf lbl rs m c' b ofs, + Genv.find_funct_ptr ge b = Some (Internal f) -> + transf_function f = OK tf -> + rs PC = Vptr b ofs -> + Mach.find_label lbl f.(Mach.fn_code) = Some c' -> + exists tc', exists rs', + goto_label tf lbl rs m = Next rs' m + /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' + /\ forall r, r <> PC -> rs'#r = rs#r. +Proof. + intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. + intros [tc [A B]]. + exploit label_pos_code_tail; eauto. instantiate (1 := 0). + intros [pos' [P [Q R]]]. + exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))). + split. unfold goto_label. rewrite P. rewrite H1. auto. + split. rewrite Pregmap.gss. constructor; auto. + rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. + auto. omega. + generalize (transf_function_no_overflow _ _ H0). omega. + intros. apply Pregmap.gso; auto. +Qed. + +(** Existence of return addresses *) + +Lemma return_address_exists: + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> + exists ra, return_address_offset f c ra. +Proof. + intros. eapply Asmgenproof0.return_address_exists; eauto. +- intros. exploit transl_instr_label; eauto. + destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. +- intros. monadInv H0. + destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. + rewrite transl_code'_transl_code in EQ0. + exists x; exists true; split; auto. unfold fn_code. + constructor. apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) x). +- exact transf_function_no_overflow. +Qed. + +(** * Proof of semantic preservation *) + +(** Semantic preservation is proved using simulation diagrams + of the following form. +<< + st1 --------------- st2 + | | + t| *|t + | | + v v + st1'--------------- st2' +>> + The invariant is the [match_states] predicate below, which includes: +- The Asm code pointed by the PC register is the translation of + the current Mach code sequence. +- Mach register values and Asm register values agree. +*) + +Inductive match_states: Mach.state -> Asm.state -> Prop := + | match_states_intro: + forall s fb sp c ep ms m m' rs f tf tc + (STACKS: match_stack ge s) + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) + (MEXT: Mem.extends m m') + (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) + (AG: agree ms sp rs) + (DXP: ep = true -> rs#X29 = parent_sp s) + (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s), + match_states (Mach.State s fb sp c ms m) + (Asm.State rs m') + | match_states_call: + forall s fb ms m m' rs + (STACKS: match_stack ge s) + (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = Vptr fb Ptrofs.zero) + (ATLR: rs RA = parent_ra s), + match_states (Mach.Callstate s fb ms m) + (Asm.State rs m') + | match_states_return: + forall s ms m m' rs + (STACKS: match_stack ge s) + (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = parent_ra s), + match_states (Mach.Returnstate s ms m) + (Asm.State rs m'). + +Lemma exec_straight_steps: + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2, + match_stack ge s -> + Mem.extends m2 m2' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> + (forall k c (TR: transl_instr f i ep k = OK c), + exists rs2, + exec_straight tge tf c rs1 m1' k rs2 m2' + /\ agree ms2 sp rs2 + /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s) + /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> + exists st', + plus step tge (State rs1 m1') E0 st' /\ + match_states (Mach.State s fb sp c ms2 m2) st'. +Proof. + intros. inversion H2. subst. monadInv H7. + exploit H3; eauto. intros [rs2 [A [B [C D]]]]. + exists (State rs2 m2'); split. + - eapply exec_straight_exec; eauto. + - econstructor; eauto. eapply exec_straight_at; eauto. +Qed. + +Lemma exec_straight_steps_goto: + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', + match_stack ge s -> + Mem.extends m2 m2' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + Mach.find_label lbl f.(Mach.fn_code) = Some c' -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> + it1_is_parent ep i = false -> + (forall k c (TR: transl_instr f i ep k = OK c), + exists jmp, exists k', exists rs2, + exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' + /\ agree ms2 sp rs2 + /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' + /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> + exists st', + plus step tge (State rs1 m1') E0 st' /\ + match_states (Mach.State s fb sp c' ms2 m2) st'. +Proof. + intros. inversion H3. subst. monadInv H9. + exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]]. + generalize (functions_transl _ _ _ H7 H8); intro FN. + generalize (transf_function_no_overflow _ _ H8); intro NOOV. + exploit exec_straight_steps_2; eauto. + intros [ofs' [PC2 CT2]]. + exploit find_label_goto_label; eauto. + intros [tc' [rs3 [GOTO [AT' OTH]]]]. + exists (State rs3 m2'); split. + eapply plus_right'. + eapply exec_straight_steps_1; eauto. + econstructor; eauto. + eapply find_instr_tail. eauto. + rewrite C. eexact GOTO. + traceEq. + econstructor; eauto. + apply agree_exten with rs2; auto with asmgen. + congruence. + rewrite OTH by congruence; auto. +Qed. + +Lemma exec_straight_opt_steps_goto: + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', + match_stack ge s -> + Mem.extends m2 m2' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + Mach.find_label lbl f.(Mach.fn_code) = Some c' -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> + it1_is_parent ep i = false -> + (forall k c (TR: transl_instr f i ep k = OK c), + exists jmp, exists k', exists rs2, + exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2' + /\ agree ms2 sp rs2 + /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' + /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> + exists st', + plus step tge (State rs1 m1') E0 st' /\ + match_states (Mach.State s fb sp c' ms2 m2) st'. +Proof. + intros. inversion H3. subst. monadInv H9. + exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]]. + generalize (functions_transl _ _ _ H7 H8); intro FN. + generalize (transf_function_no_overflow _ _ H8); intro NOOV. + inv A. +- exploit find_label_goto_label; eauto. + intros [tc' [rs3 [GOTO [AT' OTH]]]]. + exists (State rs3 m2'); split. + apply plus_one. econstructor; eauto. + eapply find_instr_tail. eauto. + rewrite C. eexact GOTO. + econstructor; eauto. + apply agree_exten with rs2; auto with asmgen. + congruence. + rewrite OTH by congruence; auto. +- exploit exec_straight_steps_2; eauto. + intros [ofs' [PC2 CT2]]. + exploit find_label_goto_label; eauto. + intros [tc' [rs3 [GOTO [AT' OTH]]]]. + exists (State rs3 m2'); split. + eapply plus_right'. + eapply exec_straight_steps_1; eauto. + econstructor; eauto. + eapply find_instr_tail. eauto. + rewrite C. eexact GOTO. + traceEq. + econstructor; eauto. + apply agree_exten with rs2; auto with asmgen. + congruence. + rewrite OTH by congruence; auto. +Qed. + +(** We need to show that, in the simulation diagram, we cannot + take infinitely many Mach transitions that correspond to zero + transitions on the Asm side. Actually, all Mach transitions + correspond to at least one Asm transition, except the + transition from [Machsem.Returnstate] to [Machsem.State]. + So, the following integer measure will suffice to rule out + the unwanted behaviour. *) + +Definition measure (s: Mach.state) : nat := + match s with + | Mach.State _ _ _ _ _ _ => 0%nat + | Mach.Callstate _ _ _ _ => 0%nat + | Mach.Returnstate _ _ _ => 1%nat + end. + +Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r. +Proof. + intros. change (IR X29) with (preg_of R29). red; intros. + exploit preg_of_injective; eauto. intros; subst r; discriminate. +Qed. + +Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP. +Proof. + intros. eapply sp_val; eauto. +Qed. + +(** This is the simulation diagram. We prove it by case analysis on the Mach transition. *) + +Theorem step_simulation: + forall S1 t S2, Mach.step return_address_offset ge S1 t S2 -> + forall S1' (MS: match_states S1 S1') (WF: wf_state ge S1), + (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. +Proof. + induction 1; intros; inv MS. + +- (* Mlabel *) + left; eapply exec_straight_steps; eauto; intros. + monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split. { apply agree_nextinstr; auto. } + split. { simpl; congruence. } + rewrite nextinstr_inv by congruence; assumption. + +- (* Mgetstack *) + unfold load_stack in H. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + left; eapply exec_straight_steps; eauto. intros. simpl in TR. + exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]]. + exists rs'; split. eauto. + split. { eapply agree_set_mreg; eauto with asmgen. congruence. } + split. { simpl; congruence. } + rewrite S. assumption. + +- (* Msetstack *) + unfold store_stack in H. + assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto). + exploit Mem.storev_extends; eauto. intros [m2' [A B]]. + left; eapply exec_straight_steps; eauto. + rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. + exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]]. + exists rs'; split. eauto. + split. eapply agree_undef_regs; eauto with asmgen. + simpl; intros. + split. rewrite Q; auto with asmgen. + rewrite R. assumption. + +- (* Mgetparam *) + assert (f0 = f) by congruence; subst f0. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact H0. auto. + intros [parent' [A B]]. rewrite (sp_val' _ _ _ AG) in A. + exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. + exploit Mem.loadv_extends. eauto. eexact H1. auto. + intros [v' [C D]]. +Opaque loadind. + left; eapply exec_straight_steps; eauto; intros. monadInv TR. + destruct ep. +(* X30 contains parent *) + exploit loadind_correct. eexact EQ. + instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence. + intros [rs1 [P [Q [R S]]]]. + exists rs1; split. eauto. + split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. + simpl; split; intros. + { rewrite R; auto with asmgen. + apply preg_of_not_X29; auto. + } + { rewrite S; auto. } + +(* X30 does not contain parent *) + exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]]. + exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence. + intros [rs2 [S [T [U V]]]]. + exists rs2; split. eapply exec_straight_trans; eauto. + split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. + instantiate (1 := rs1#X29 <- (rs2#X29)). intros. + rewrite Pregmap.gso; auto with asmgen. + congruence. + intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen. + split; simpl; intros. rewrite U; auto with asmgen. + apply preg_of_not_X29; auto. + rewrite V. rewrite R by congruence. auto. + +- (* Mop *) + assert (eval_operation tge sp op (map rs args) m = Some v). + { rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. } + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. + intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. + left; eapply exec_straight_steps; eauto; intros. simpl in TR. + exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]]. + exists rs2; split. eauto. split. + apply agree_set_undef_mreg with rs0; auto. + apply Val.lessdef_trans with v'; auto. + split; simpl; intros. InvBooleans. + rewrite R; auto. apply preg_of_not_X29; auto. +Local Transparent destroyed_by_op. + destruct op; try exact I; simpl; congruence. + rewrite S. + auto. +- (* Mload *) + destruct trap. + { + assert (Op.eval_addressing tge sp addr (map rs args) = Some a). + { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. } + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. + left; eapply exec_straight_steps; eauto; intros. simpl in TR. + exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]]. + exists rs2; split. eauto. + split. eapply agree_set_undef_mreg; eauto. congruence. + split. simpl; congruence. + rewrite S. assumption. + } + + (* Mload notrap1 *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + +- (* Mload notrap *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + +- (* Mload notrap *) + inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. + +- (* Mstore *) + assert (Op.eval_addressing tge sp addr (map rs args) = Some a). + { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. } + exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. + intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. + assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto). + exploit Mem.storev_extends; eauto. intros [m2' [C D]]. + left; eapply exec_straight_steps; eauto. + intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]]. + exists rs2; split. eauto. + split. eapply agree_undef_regs; eauto with asmgen. + split. simpl; congruence. + rewrite R. assumption. + +- (* Mcall *) + assert (f0 = f) by congruence. subst f0. + inv AT. + assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). + { eapply transf_function_no_overflow; eauto. } + destruct ros as [rf|fid]; simpl in H; monadInv H5. ++ (* Indirect call *) + assert (rs rf = Vptr f' Ptrofs.zero). + { destruct (rs rf); try discriminate. + revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } + assert (rs0 x0 = Vptr f' Ptrofs.zero). + { exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. } + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). + { econstructor; eauto. } + exploit return_address_offset_correct; eauto. intros; subst ra. + left; econstructor; split. + apply plus_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. eauto. + econstructor; eauto. + econstructor; eauto. + eapply agree_sp_def; eauto. + simpl. eapply agree_exten; eauto. intros. Simpl. + Simpl. rewrite <- H2. auto. ++ (* Direct call *) + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). + econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. + left; econstructor; split. + apply plus_one. eapply exec_step_internal. eauto. + eapply functions_transl; eauto. eapply find_instr_tail; eauto. + simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto. + econstructor; eauto. + econstructor; eauto. + eapply agree_sp_def; eauto. + simpl. eapply agree_exten; eauto. intros. Simpl. + Simpl. rewrite <- H2. auto. + +- (* Mtailcall *) + assert (f0 = f) by congruence. subst f0. + inversion AT; subst. + assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). + { eapply transf_function_no_overflow; eauto. } + exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. + destruct ros as [rf|fid]; simpl in H; monadInv H7. ++ (* Indirect call *) + assert (rs rf = Vptr f' Ptrofs.zero). + { destruct (rs rf); try discriminate. + revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } + assert (rs0 x0 = Vptr f' Ptrofs.zero). + { exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. } + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_steps_2; eauto using functions_transl. + intros (ofs' & P & Q). + left; econstructor; split. + (* execution *) + eapply plus_right'. eapply exec_straight_exec; eauto. + econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. + simpl. reflexivity. + traceEq. + (* match states *) + econstructor; eauto. + apply agree_set_other; auto with asmgen. + Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. ++ (* Direct call *) + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_steps_2; eauto using functions_transl. + intros (ofs' & P & Q). + left; econstructor; split. + (* execution *) + eapply plus_right'. eapply exec_straight_exec; eauto. + econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. + simpl. reflexivity. + traceEq. + (* match states *) + econstructor; eauto. + apply agree_set_other; auto with asmgen. + Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. + +- (* Mbuiltin *) + inv AT. monadInv H4. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H3); intro NOOV. + exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [A [B [C D]]]]]. + left. econstructor; split. apply plus_one. + eapply exec_step_builtin. eauto. eauto. + eapply find_instr_tail; eauto. + erewrite <- sp_val by eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + eauto. + econstructor; eauto. + instantiate (2 := tf); instantiate (1 := x). + unfold nextinstr. rewrite Pregmap.gss. + rewrite set_res_other. rewrite undef_regs_other_2. + rewrite <- H1. simpl. econstructor; eauto. + eapply code_tail_next_int; eauto. + rewrite preg_notin_charact. intros. auto with asmgen. + auto with asmgen. + apply agree_nextinstr. eapply agree_set_res; auto. + eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. + congruence. + + Simpl. + rewrite set_res_other by trivial. + rewrite undef_regs_other. + assumption. + intro. + rewrite in_map_iff. + intros (x0 & PREG & IN). + subst r'. + intro. + apply (preg_of_not_RA x0). + congruence. + +- (* Mgoto *) + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H4. + exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. + left; exists (State rs' m'); split. + apply plus_one. econstructor; eauto. + eapply functions_transl; eauto. + eapply find_instr_tail; eauto. + simpl; eauto. + econstructor; eauto. + eapply agree_exten; eauto with asmgen. + congruence. + + rewrite INV by congruence. + assumption. + +- (* Mcond true *) + assert (f0 = f) by congruence. subst f0. + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. + left; eapply exec_straight_opt_steps_goto; eauto. + intros. simpl in TR. + exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). + exists jmp; exists k; exists rs'. + split. eexact A. + split. apply agree_exten with rs0; auto with asmgen. + split. + exact B. + rewrite D. exact LEAF. + +- (* Mcond false *) + exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. + left; eapply exec_straight_steps; eauto. intros. simpl in TR. + exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). + econstructor; split. + eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto. + split. apply agree_exten with rs0; auto. intros. Simpl. + split. + simpl; congruence. + Simpl. rewrite D. + exact LEAF. + +- (* Mjumptable *) + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H6. + exploit functions_transl; eauto. intro FN. + generalize (transf_function_no_overflow _ _ H5); intro NOOV. + exploit find_label_goto_label. eauto. eauto. + instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef). + Simpl. eauto. + eauto. + intros [tc' [rs' [A [B C]]]]. + exploit ireg_val; eauto. rewrite H. intros LD; inv LD. + left; econstructor; split. + apply plus_one. econstructor; eauto. + eapply find_instr_tail; eauto. + simpl. Simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. + econstructor; eauto. + eapply agree_undef_regs; eauto. + simpl. intros. rewrite C; auto with asmgen. Simpl. + congruence. + + rewrite C by congruence. + repeat rewrite Pregmap.gso by congruence. + assumption. + +- (* Mreturn *) + assert (f0 = f) by congruence. subst f0. + inversion AT; subst. simpl in H6; monadInv H6. + assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_steps_2; eauto using functions_transl. + intros (ofs' & P & Q). + left; econstructor; split. + (* execution *) + eapply plus_right'. eapply exec_straight_exec; eauto. + econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. + simpl. reflexivity. + traceEq. + (* match states *) + econstructor; eauto. + apply agree_set_other; auto with asmgen. + +- (* internal function *) + + exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. + generalize EQ; intros EQ'. monadInv EQ'. + destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. + unfold store_stack in *. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. + intros [m1' [C D]]. + exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. + intros [m2' [F G]]. + simpl chunk_of_type in F. + exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. + intros [m3' [P Q]]. + change (chunk_of_type Tptr) with Mint64 in *. + (* Execution of function prologue *) + monadInv EQ0. rewrite transl_code'_transl_code in EQ1. + set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: + storeptr RA XSP (fn_retaddr_ofs f) x0) in *. + set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. + set (rs2 := nextinstr (rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef)). + exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2). + simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. + change (rs2 X2) with sp. eexact P. + simpl; congruence. congruence. + intros (rs3 & U & V & W). + assert (EXEC_PROLOGUE: + exec_straight tge tf + tf.(fn_code) rs0 m' + x0 rs3 m3'). + { change (fn_code tf) with tfbody; unfold tfbody. + apply exec_straight_step with rs2 m2'. + unfold exec_instr. rewrite C. fold sp. + rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity. + reflexivity. + eexact U. } + exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. + intros (ofs' & X & Y). + left; exists (State rs3 m3'); split. + eapply exec_straight_steps_1; eauto. omega. constructor. + econstructor; eauto. + rewrite X; econstructor; eauto. + apply agree_exten with rs2; eauto with asmgen. + unfold rs2. + apply agree_nextinstr. apply agree_set_other; auto with asmgen. + apply agree_change_sp with (parent_sp s). + apply agree_undef_regs with rs0. auto. +Local Transparent destroyed_at_function_entry. simpl. + simpl; intros; Simpl. + unfold sp; congruence. + intros. rewrite V by auto with asmgen. reflexivity. + + rewrite W. + unfold rs2. + Simpl. + +- (* external function *) + exploit functions_translated; eauto. + intros [tf [A B]]. simpl in B. inv B. + exploit extcall_arguments_match; eauto. + intros [args' [C D]]. + exploit external_call_mem_extends; eauto. + intros [res' [m2' [P [Q [R S]]]]]. + left; econstructor; split. + apply plus_one. eapply exec_step_external; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + econstructor; eauto. + unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. + apply agree_undef_caller_save_regs; auto. + +- (* return *) + inv STACKS. simpl in *. + right. split. omega. split. auto. + rewrite <- ATPC in H5. + econstructor; eauto. congruence. + inv WF. + inv STACK. + inv H1. + congruence. +Qed. + +Lemma transf_initial_states: + forall st1, Mach.initial_state prog st1 -> + exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inversion H. unfold ge0 in *. + econstructor; split. + econstructor. + eapply (Genv.init_mem_transf_partial TRANSF); eauto. + replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero) + with (Vptr fb Ptrofs.zero). + econstructor; eauto. + constructor. + apply Mem.extends_refl. + split. auto. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. + intros. rewrite Regmap.gi. auto. + unfold Genv.symbol_address. + rewrite (match_program_main TRANSF). + rewrite symbols_preserved. + unfold ge; rewrite H1. auto. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r. +Proof. + intros. inv H0. inv H. constructor. assumption. + compute in H1. inv H1. + generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto. +Qed. + +Theorem transf_program_correct: + forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). +Proof. + eapply forward_simulation_star with (measure := measure) + (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1). + - apply senv_preserved. + - simpl; intros. exploit transf_initial_states; eauto. + intros (s2 & A & B). + exists s2; intuition auto. apply wf_initial; auto. + - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto. + - simpl; intros. destruct H0 as [MS WF]. + exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ]. + + left; exists s2'; intuition auto. eapply wf_step; eauto. + + right; intuition auto. eapply wf_step; eauto. +Qed. + +End PRESERVATION. +*)
\ No newline at end of file diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmblockgenproof1.v index 0e36bd05..b42309bc 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmblockgenproof1.v @@ -1,3 +1,5 @@ +(* ORIGINAL aarch64/Asmgenproof1 file that needs to be adapted + (* *********************************************************************) (* *) (* The Compcert verified compiler *) @@ -2136,3 +2138,4 @@ Proof. Qed. End CONSTRUCTORS. +*)
\ No newline at end of file diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 024c9a17..f81f37d6 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -1,1172 +1,33 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, Collège de France and INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Translation from Mach to AArch64. *) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Justus Fasse UGA, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Recdef Coqlib Zwf Zbits. Require Import Errors AST Integers Floats Op. -Require Import Locations Mach Asm. - -Local Open Scope string_scope. -Local Open Scope list_scope. -Local Open Scope error_monad_scope. - -(** Alignment check for symbols *) - -Parameter symbol_is_aligned : ident -> Z -> bool. -(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) - -(** Extracting integer or float registers. *) - -Definition ireg_of (r: mreg) : res ireg := - match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end. - -Definition freg_of (r: mreg) : res freg := - match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end. - -(** Recognition of immediate arguments for logical integer operations.*) - -(** Valid immediate arguments are repetitions of a bit pattern [B] - of length [e] = 2, 4, 8, 16, 32 or 64. - The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*] - but must not be all zeros or all ones. *) - -(** The following automaton recognizes [0*1*0*|1*0*1*]. -<< - 0 1 0 - / \ / \ / \ - \ / \ / \ / - -0--> [B] --1--> [D] --0--> [F] - / - [A] - \ - -1--> [C] --0--> [E] --1--> [G] - / \ / \ / \ - \ / \ / \ / - 1 0 1 ->> -*) - -Module Automaton. - -Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad. - -Definition start := SA. - -Definition next (s: state) (b: bool) := - match s, b with - | SA,false => SB | SA,true => SC - | SB,false => SB | SB,true => SD - | SC,false => SE | SC,true => SC - | SD,false => SF | SD,true => SD - | SE,false => SE | SE,true => SG - | SF,false => SF | SF,true => Sbad - | SG,false => Sbad | SG,true => SG - | Sbad,_ => Sbad - end. - -Definition accepting (s: state) := - match s with - | SA | SB | SC | SD | SE | SF | SG => true - | Sbad => false - end. - -Fixpoint run (len: nat) (s: state) (x: Z) : bool := - match len with - | Datatypes.O => accepting s - | Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x) - end. - -End Automaton. - -(** The following function determines the candidate length [e], - ensuring that [x] is a repetition [BB...B] - of a bit pattern [B] of length [e]. *) - -Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat := - (** [test n] checks that the low [2n] bits of [x] are of the - form [BB], that is, two occurrences of the same [n] bits *) - let test (n: Z) : bool := - Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in - (** If [test n] fails, we know that the candidate length [e] is - at least [2n]. Hence we test with decreasing values of [n]: - 32, 16, 8, 4, 2. *) - if sixtyfour && negb (test 32) then 64%nat - else if negb (test 16) then 32%nat - else if negb (test 8) then 16%nat - else if negb (test 4) then 8%nat - else if negb (test 2) then 4%nat - else 2%nat. - -(** A valid logical immediate is -- neither [0] nor [-1]; -- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e] -- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*]. -*) - -Definition is_logical_imm32 (x: int) : bool := - negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) && - Automaton.run (logical_imm_length (Int.unsigned x) false) - Automaton.start (Int.unsigned x). - -Definition is_logical_imm64 (x: int64) : bool := - negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) && - Automaton.run (logical_imm_length (Int64.unsigned x) true) - Automaton.start (Int64.unsigned x). - -(** Arithmetic immediates are 12-bit unsigned numbers, possibly shifted left 12 bits *) - -Definition is_arith_imm32 (x: int) : bool := - Int.eq x (Int.zero_ext 12 x) - || Int.eq x (Int.shl (Int.zero_ext 12 (Int.shru x (Int.repr 12))) (Int.repr 12)). - -Definition is_arith_imm64 (x: int64) : bool := - Int64.eq x (Int64.zero_ext 12 x) - || Int64.eq x (Int64.shl (Int64.zero_ext 12 (Int64.shru x (Int64.repr 12))) (Int64.repr 12)). - -(** Decompose integer literals into 16-bit fragments *) - -Fixpoint decompose_int (N: nat) (n p: Z) {struct N} : list (Z * Z) := - match N with - | Datatypes.O => nil - | Datatypes.S N => - let frag := Zzero_ext 16 (Z.shiftr n p) in - if Z.eqb frag 0 then - decompose_int N n (p + 16) - else - (frag, p) :: decompose_int N (Z.ldiff n (Z.shiftl 65535 p)) (p + 16) - end. - -Definition negate_decomposition (l: list (Z * Z)) := - List.map (fun np => (Z.lxor (fst np) 65535, snd np)) l. - -Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := - List.fold_right (fun np k => Pmovk sz rd (fst np) (snd np) :: k) k l. - -Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := - match l with - | nil => Pmovz sz rd 0 0 :: k - | (n1, p1) :: l => Pmovz sz rd n1 p1 :: loadimm_k sz rd l k - end. - -Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code := - match l with - | nil => Pmovn sz rd 0 0 :: k - | (n1, p1) :: l => Pmovn sz rd n1 p1 :: loadimm_k sz rd (negate_decomposition l) k - end. - -Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: code) : code := - let N := match sz with W => 2%nat | X => 4%nat end in - let dz := decompose_int N n 0 in - let dn := decompose_int N (Z.lnot n) 0 in - if Nat.leb (List.length dz) (List.length dn) - then loadimm_z sz rd dz k - else loadimm_n sz rd dn k. - -Definition loadimm32 (rd: ireg) (n: int) (k: code) : code := - if is_logical_imm32 n - then Porrimm W rd XZR (Int.unsigned n) :: k - else loadimm W rd (Int.unsigned n) k. - -Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code := - if is_logical_imm64 n - then Porrimm X rd XZR (Int64.unsigned n) :: k - else loadimm X rd (Int64.unsigned n) k. - -(** Add immediate *) - -Definition addimm_aux (insn: iregsp -> iregsp -> Z -> instruction) - (rd r1: iregsp) (n: Z) (k: code) := - let nlo := Zzero_ext 12 n in - let nhi := n - nlo in - if Z.eqb nhi 0 then - insn rd r1 nlo :: k - else if Z.eqb nlo 0 then - insn rd r1 nhi :: k - else - insn rd r1 nhi :: insn rd rd nlo :: k. - -Definition addimm32 (rd r1: ireg) (n: int) (k: code) : code := - let m := Int.neg n in - if Int.eq n (Int.zero_ext 24 n) then - addimm_aux (Paddimm W) rd r1 (Int.unsigned n) k - else if Int.eq m (Int.zero_ext 24 m) then - addimm_aux (Psubimm W) rd r1 (Int.unsigned m) k - else if Int.lt n Int.zero then - loadimm32 X16 m (Psub W rd r1 X16 SOnone :: k) - else - loadimm32 X16 n (Padd W rd r1 X16 SOnone :: k). - -Definition addimm64 (rd r1: iregsp) (n: int64) (k: code) : code := - let m := Int64.neg n in - if Int64.eq n (Int64.zero_ext 24 n) then - addimm_aux (Paddimm X) rd r1 (Int64.unsigned n) k - else if Int64.eq m (Int64.zero_ext 24 m) then - addimm_aux (Psubimm X) rd r1 (Int64.unsigned m) k - else if Int64.lt n Int64.zero then - loadimm64 X16 m (Psubext rd r1 X16 (EOuxtx Int.zero) :: k) - else - loadimm64 X16 n (Paddext rd r1 X16 (EOuxtx Int.zero) :: k). - -(** Logical immediate *) - -Definition logicalimm32 - (insn1: ireg -> ireg0 -> Z -> instruction) - (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction) - (rd r1: ireg) (n: int) (k: code) : code := - if is_logical_imm32 n - then insn1 rd r1 (Int.unsigned n) :: k - else loadimm32 X16 n (insn2 rd r1 X16 SOnone :: k). - -Definition logicalimm64 - (insn1: ireg -> ireg0 -> Z -> instruction) - (insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction) - (rd r1: ireg) (n: int64) (k: code) : code := - if is_logical_imm64 n - then insn1 rd r1 (Int64.unsigned n) :: k - else loadimm64 X16 n (insn2 rd r1 X16 SOnone :: k). - -(** Sign- or zero-extended arithmetic *) - -Definition transl_extension (ex: extension) (a: int) : extend_op := - match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end. - -Definition move_extended_base - (rd: ireg) (r1: ireg) (ex: extension) (k: code) : code := - match ex with - | Xsgn32 => Pcvtsw2x rd r1 :: k - | Xuns32 => Pcvtuw2x rd r1 :: k - end. - -Definition move_extended - (rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: code) : code := - if Int.eq a Int.zero then - move_extended_base rd r1 ex k - else - move_extended_base rd r1 ex (Padd X rd XZR rd (SOlsl a) :: k). - -Definition arith_extended - (insnX: iregsp -> iregsp -> ireg -> extend_op -> instruction) - (insnS: ireg -> ireg0 -> ireg -> shift_op -> instruction) - (rd r1 r2: ireg) (ex: extension) (a: int) (k: code) : code := - if Int.ltu a (Int.repr 5) then - insnX rd r1 r2 (transl_extension ex a) :: k - else - move_extended_base X16 r2 ex (insnS rd r1 X16 (SOlsl a) :: k). - -(** Extended right shift *) - -Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code := - if Int.eq n Int.zero then - Pmov rd r1 :: k - else if Int.eq n Int.one then - Padd W X16 r1 r1 (SOlsr (Int.repr 31)) :: - Porr W rd XZR X16 (SOasr n) :: k - else - Porr W X16 XZR r1 (SOasr (Int.repr 31)) :: - Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) :: - Porr W rd XZR X16 (SOasr n) :: k. - -Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code := - if Int.eq n Int.zero then - Pmov rd r1 :: k - else if Int.eq n Int.one then - Padd X X16 r1 r1 (SOlsr (Int.repr 63)) :: - Porr X rd XZR X16 (SOasr n) :: k - else - Porr X X16 XZR r1 (SOasr (Int.repr 63)) :: - Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) :: - Porr X rd XZR X16 (SOasr n) :: k. - -(** Load the address [id + ofs] in [rd] *) - -Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: code) : code := - if Archi.pic_code tt then - if Ptrofs.eq ofs Ptrofs.zero then - Ploadsymbol rd id :: k - else - Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k - else - Padrp rd id ofs :: Paddadr rd rd id ofs :: k. - -(** Translate a shifted operand *) - -Definition transl_shift (s: Op.shift) (a: int): Asm.shift_op := - match s with - | Slsl => SOlsl a - | Slsr => SOlsr a - | Sasr => SOasr a - | Sror => SOror a - end. - -(** Translation of a condition. Prepends to [k] the instructions - that evaluate the condition and leave its boolean result in one of - the bits of the condition register. The bit in question is - determined by the [crbit_for_cond] function. *) - -Definition transl_cond - (cond: condition) (args: list mreg) (k: code) := - match cond, args with - | (Ccomp c | Ccompu c), a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pcmp W r1 r2 SOnone :: k) - | (Ccompshift c s a | Ccompushift c s a), a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pcmp W r1 r2 (transl_shift s a) :: k) - | (Ccompimm c n | Ccompuimm c n), a1 :: nil => - do r1 <- ireg_of a1; - OK (if is_arith_imm32 n then - Pcmpimm W r1 (Int.unsigned n) :: k - else if is_arith_imm32 (Int.neg n) then - Pcmnimm W r1 (Int.unsigned (Int.neg n)) :: k - else - loadimm32 X16 n (Pcmp W r1 X16 SOnone :: k)) - | (Cmaskzero n | Cmasknotzero n), a1 :: nil => - do r1 <- ireg_of a1; - OK (if is_logical_imm32 n then - Ptstimm W r1 (Int.unsigned n) :: k - else - loadimm32 X16 n (Ptst W r1 X16 SOnone :: k)) - | (Ccompl c | Ccomplu c), a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pcmp X r1 r2 SOnone :: k) - | (Ccomplshift c s a | Ccomplushift c s a), a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pcmp X r1 r2 (transl_shift s a) :: k) - | (Ccomplimm c n | Ccompluimm c n), a1 :: nil => - do r1 <- ireg_of a1; - OK (if is_arith_imm64 n then - Pcmpimm X r1 (Int64.unsigned n) :: k - else if is_arith_imm64 (Int64.neg n) then - Pcmnimm X r1 (Int64.unsigned (Int64.neg n)) :: k - else - loadimm64 X16 n (Pcmp X r1 X16 SOnone :: k)) - | (Cmasklzero n | Cmasklnotzero n), a1 :: nil => - do r1 <- ireg_of a1; - OK (if is_logical_imm64 n then - Ptstimm X r1 (Int64.unsigned n) :: k - else - loadimm64 X16 n (Ptst X r1 X16 SOnone :: k)) - | Ccompf cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmp D r1 r2 :: k) - | Cnotcompf cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmp D r1 r2 :: k) - | Ccompfzero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmp0 D r1 :: k) - | Cnotcompfzero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmp0 D r1 :: k) - | Ccompfs cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmp S r1 r2 :: k) - | Cnotcompfs cmp, a1 :: a2 :: nil => - do r1 <- freg_of a1; do r2 <- freg_of a2; - OK (Pfcmp S r1 r2 :: k) - | Ccompfszero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmp0 S r1 :: k) - | Cnotcompfszero cmp, a1 :: nil => - do r1 <- freg_of a1; - OK (Pfcmp0 S r1 :: k) - | _, _ => - Error(msg "Asmgen.transl_cond") - end. - -Definition cond_for_signed_cmp (cmp: comparison) := - match cmp with - | Ceq => TCeq - | Cne => TCne - | Clt => TClt - | Cle => TCle - | Cgt => TCgt - | Cge => TCge - end. - -Definition cond_for_unsigned_cmp (cmp: comparison) := - match cmp with - | Ceq => TCeq - | Cne => TCne - | Clt => TClo - | Cle => TCls - | Cgt => TChi - | Cge => TChs - end. - -Definition cond_for_float_cmp (cmp: comparison) := - match cmp with - | Ceq => TCeq - | Cne => TCne - | Clt => TCmi - | Cle => TCls - | Cgt => TCgt - | Cge => TCge - end. - -Definition cond_for_float_not_cmp (cmp: comparison) := - match cmp with - | Ceq => TCne - | Cne => TCeq - | Clt => TCpl - | Cle => TChi - | Cgt => TCle - | Cge => TClt - end. - -Definition cond_for_cond (cond: condition) := - match cond with - | Ccomp cmp => cond_for_signed_cmp cmp - | Ccompu cmp => cond_for_unsigned_cmp cmp - | Ccompshift cmp s a => cond_for_signed_cmp cmp - | Ccompushift cmp s a => cond_for_unsigned_cmp cmp - | Ccompimm cmp n => cond_for_signed_cmp cmp - | Ccompuimm cmp n => cond_for_unsigned_cmp cmp - | Cmaskzero n => TCeq - | Cmasknotzero n => TCne - | Ccompl cmp => cond_for_signed_cmp cmp - | Ccomplu cmp => cond_for_unsigned_cmp cmp - | Ccomplshift cmp s a => cond_for_signed_cmp cmp - | Ccomplushift cmp s a => cond_for_unsigned_cmp cmp - | Ccomplimm cmp n => cond_for_signed_cmp cmp - | Ccompluimm cmp n => cond_for_unsigned_cmp cmp - | Cmasklzero n => TCeq - | Cmasklnotzero n => TCne - | Ccompf cmp => cond_for_float_cmp cmp - | Cnotcompf cmp => cond_for_float_not_cmp cmp - | Ccompfzero cmp => cond_for_float_cmp cmp - | Cnotcompfzero cmp => cond_for_float_not_cmp cmp - | Ccompfs cmp => cond_for_float_cmp cmp - | Cnotcompfs cmp => cond_for_float_not_cmp cmp - | Ccompfszero cmp => cond_for_float_cmp cmp - | Cnotcompfszero cmp => cond_for_float_not_cmp cmp - end. - -(** Translation of a conditional branch. Prepends to [k] the instructions - that evaluate the condition and ranch to [lbl] if it holds. - We recognize some conditional branches that can be implemented - without setting then testing condition flags. *) - -Definition transl_cond_branch_default - (c: condition) (args: list mreg) (lbl: label) (k: code) := - transl_cond c args (Pbc (cond_for_cond c) lbl :: k). - -Definition transl_cond_branch - (c: condition) (args: list mreg) (lbl: label) (k: code) := - match args, c with - | a1 :: nil, (Ccompimm Cne n | Ccompuimm Cne n) => - if Int.eq n Int.zero - then (do r1 <- ireg_of a1; OK (Pcbnz W r1 lbl :: k)) - else transl_cond_branch_default c args lbl k - | a1 :: nil, (Ccompimm Ceq n | Ccompuimm Ceq n) => - if Int.eq n Int.zero - then (do r1 <- ireg_of a1; OK (Pcbz W r1 lbl :: k)) - else transl_cond_branch_default c args lbl k - | a1 :: nil, (Ccomplimm Cne n | Ccompluimm Cne n) => - if Int64.eq n Int64.zero - then (do r1 <- ireg_of a1; OK (Pcbnz X r1 lbl :: k)) - else transl_cond_branch_default c args lbl k - | a1 :: nil, (Ccomplimm Ceq n | Ccompluimm Ceq n) => - if Int64.eq n Int64.zero - then (do r1 <- ireg_of a1; OK (Pcbz X r1 lbl :: k)) - else transl_cond_branch_default c args lbl k - | a1 :: nil, Cmaskzero n => - match Int.is_power2 n with - | Some bit => do r1 <- ireg_of a1; OK (Ptbz W r1 bit lbl :: k) - | None => transl_cond_branch_default c args lbl k - end - | a1 :: nil, Cmasknotzero n => - match Int.is_power2 n with - | Some bit => do r1 <- ireg_of a1; OK (Ptbnz W r1 bit lbl :: k) - | None => transl_cond_branch_default c args lbl k - end - | a1 :: nil, Cmasklzero n => - match Int64.is_power2' n with - | Some bit => do r1 <- ireg_of a1; OK (Ptbz X r1 bit lbl :: k) - | None => transl_cond_branch_default c args lbl k - end - | a1 :: nil, Cmasklnotzero n => - match Int64.is_power2' n with - | Some bit => do r1 <- ireg_of a1; OK (Ptbnz X r1 bit lbl :: k) - | None => transl_cond_branch_default c args lbl k - end - | _, _ => - transl_cond_branch_default c args lbl k - end. - -(** Translation of the arithmetic operation [res <- op(args)]. - The corresponding instructions are prepended to [k]. *) - -Definition transl_op - (op: operation) (args: list mreg) (res: mreg) (k: code) := - match op, args with - | Omove, a1 :: nil => - match preg_of res, preg_of a1 with - | IR r, IR a => OK (Pmov r a :: k) - | FR r, FR a => OK (Pfmov r a :: k) - | _ , _ => Error(msg "Asmgen.Omove") - end - | Ointconst n, nil => - do rd <- ireg_of res; - OK (loadimm32 rd n k) - | Olongconst n, nil => - do rd <- ireg_of res; - OK (loadimm64 rd n k) - | Ofloatconst f, nil => - do rd <- freg_of res; - OK (if Float.eq_dec f Float.zero - then Pfmovi D rd XZR :: k - else Pfmovimmd rd f :: k) - | Osingleconst f, nil => - do rd <- freg_of res; - OK (if Float32.eq_dec f Float32.zero - then Pfmovi S rd XZR :: k - else Pfmovimms rd f :: k) - | Oaddrsymbol id ofs, nil => - do rd <- ireg_of res; - OK (loadsymbol rd id ofs k) - | Oaddrstack ofs, nil => - do rd <- ireg_of res; - OK (addimm64 rd XSP (Ptrofs.to_int64 ofs) k) -(** 32-bit integer arithmetic *) - | Oshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porr W rd XZR r1 (transl_shift s a) :: k) - | Oadd, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Padd W rd r1 r2 SOnone :: k) - | Oaddshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Padd W rd r1 r2 (transl_shift s a) :: k) - | Oaddimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (addimm32 rd r1 n k) - | Oneg, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psub W rd XZR r1 SOnone :: k) - | Onegshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psub W rd XZR r1 (transl_shift s a) :: k) - | Osub, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psub W rd r1 r2 SOnone :: k) - | Osubshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psub W rd r1 r2 (transl_shift s a) :: k) - | Omul, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pmadd W rd r1 r2 XZR :: k) - | Omuladd, a1 :: a2 :: a3 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; - OK (Pmadd W rd r2 r3 r1 :: k) - | Omulsub, a1 :: a2 :: a3 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; - OK (Pmsub W rd r2 r3 r1 :: k) - | Odiv, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psdiv W rd r1 r2 :: k) - | Odivu, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pudiv W rd r1 r2 :: k) - | Oand, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pand W rd r1 r2 SOnone :: k) - | Oandshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pand W rd r1 r2 (transl_shift s a) :: k) - | Oandimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (logicalimm32 (Pandimm W) (Pand W) rd r1 n k) - | Oor, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porr W rd r1 r2 SOnone :: k) - | Oorshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porr W rd r1 r2 (transl_shift s a) :: k) - | Oorimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (logicalimm32 (Porrimm W) (Porr W) rd r1 n k) - | Oxor, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peor W rd r1 r2 SOnone :: k) - | Oxorshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peor W rd r1 r2 (transl_shift s a) :: k) - | Oxorimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (logicalimm32 (Peorimm W) (Peor W) rd r1 n k) - | Onot, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porn W rd XZR r1 SOnone :: k) - | Onotshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porn W rd XZR r1 (transl_shift s a) :: k) - | Obic, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pbic W rd r1 r2 SOnone :: k) - | Obicshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pbic W rd r1 r2 (transl_shift s a) :: k) - | Oorn, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porn W rd r1 r2 SOnone :: k) - | Oornshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porn W rd r1 r2 (transl_shift s a) :: k) - | Oeqv, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peon W rd r1 r2 SOnone :: k) - | Oeqvshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peon W rd r1 r2 (transl_shift s a) :: k) - | Oshl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Plslv W rd r1 r2 :: k) - | Oshr, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pasrv W rd r1 r2 :: k) - | Oshru, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Plsrv W rd r1 r2 :: k) - | Oshrximm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (shrx32 rd r1 n k) - | Ozext s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfiz W rd r1 Int.zero s :: k) - | Osext s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfiz W rd r1 Int.zero s :: k) - | Oshlzext s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) - | Oshlsext s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfiz W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) - | Ozextshr a s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) - | Osextshr a s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfx W rd r1 a (Z.min s (Int.zwordsize - Int.unsigned a)) :: k) -(** 64-bit integer arithmetic *) - | Oshiftl s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porr X rd XZR r1 (transl_shift s a) :: k) - | Oextend x a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (move_extended rd r1 x a k) - (* [Omakelong] and [Ohighlong] should not occur *) - | Olowlong, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - assertion (ireg_eq rd r1); - OK (Pcvtx2w rd :: k) - | Oaddl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Padd X rd r1 r2 SOnone :: k) - | Oaddlshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Padd X rd r1 r2 (transl_shift s a) :: k) - | Oaddlext x a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (arith_extended Paddext (Padd X) rd r1 r2 x a k) - | Oaddlimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (addimm64 rd r1 n k) - | Onegl, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psub X rd XZR r1 SOnone :: k) - | Oneglshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psub X rd XZR r1 (transl_shift s a) :: k) - | Osubl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psub X rd r1 r2 SOnone :: k) - | Osublshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psub X rd r1 r2 (transl_shift s a) :: k) - | Osublext x a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (arith_extended Psubext (Psub X) rd r1 r2 x a k) - | Omull, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pmadd X rd r1 r2 XZR :: k) - | Omulladd, a1 :: a2 :: a3 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; - OK (Pmadd X rd r2 r3 r1 :: k) - | Omullsub, a1 :: a2 :: a3 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; - OK (Pmsub X rd r2 r3 r1 :: k) - | Omullhs, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psmulh rd r1 r2 :: k) - | Omullhu, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pumulh rd r1 r2 :: k) - | Odivl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Psdiv X rd r1 r2 :: k) - | Odivlu, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pudiv X rd r1 r2 :: k) - | Oandl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pand X rd r1 r2 SOnone :: k) - | Oandlshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pand X rd r1 r2 (transl_shift s a) :: k) - | Oandlimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (logicalimm64 (Pandimm X) (Pand X) rd r1 n k) - | Oorl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porr X rd r1 r2 SOnone :: k) - | Oorlshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porr X rd r1 r2 (transl_shift s a) :: k) - | Oorlimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (logicalimm64 (Porrimm X) (Porr X) rd r1 n k) - | Oxorl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peor X rd r1 r2 SOnone :: k) - | Oxorlshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peor X rd r1 r2 (transl_shift s a) :: k) - | Oxorlimm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (logicalimm64 (Peorimm X) (Peor X) rd r1 n k) - | Onotl, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porn X rd XZR r1 SOnone :: k) - | Onotlshift s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Porn X rd XZR r1 (transl_shift s a) :: k) - | Obicl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pbic X rd r1 r2 SOnone :: k) - | Obiclshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pbic X rd r1 r2 (transl_shift s a) :: k) - | Oornl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porn X rd r1 r2 SOnone :: k) - | Oornlshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Porn X rd r1 r2 (transl_shift s a) :: k) - | Oeqvl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peon X rd r1 r2 SOnone :: k) - | Oeqvlshift s a, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Peon X rd r1 r2 (transl_shift s a) :: k) - | Oshll, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Plslv X rd r1 r2 :: k) - | Oshrl, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Pasrv X rd r1 r2 :: k) - | Oshrlu, a1 :: a2 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (Plsrv X rd r1 r2 :: k) - | Oshrlximm n, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (shrx64 rd r1 n k) - | Ozextl s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfiz X rd r1 Int.zero s :: k) - | Osextl s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfiz X rd r1 Int.zero s :: k) - | Oshllzext s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) - | Oshllsext s a, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfiz X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) - | Ozextshrl a s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Pubfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) - | Osextshrl a s, a1 :: nil => - do rd <- ireg_of res; do r1 <- ireg_of a1; - OK (Psbfx X rd r1 a (Z.min s (Int64.zwordsize - Int.unsigned a)) :: k) -(** 64-bit floating-point arithmetic *) - | Onegf, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfneg D rd rs :: k) - | Oabsf, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfabs D rd rs :: k) - | Oaddf, a1 :: a2 :: nil => - do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; - OK (Pfadd D rd rs1 rs2 :: k) - | Osubf, a1 :: a2 :: nil => - do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; - OK (Pfsub D rd rs1 rs2 :: k) - | Omulf, a1 :: a2 :: nil => - do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; - OK (Pfmul D rd rs1 rs2 :: k) - | Odivf, a1 :: a2 :: nil => - do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; - OK (Pfdiv D rd rs1 rs2 :: k) -(** 32-bit floating-point arithmetic *) - | Onegfs, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfneg S rd rs :: k) - | Oabsfs, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfabs S rd rs :: k) - | Oaddfs, a1 :: a2 :: nil => - do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; - OK (Pfadd S rd rs1 rs2 :: k) - | Osubfs, a1 :: a2 :: nil => - do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; - OK (Pfsub S rd rs1 rs2 :: k) - | Omulfs, a1 :: a2 :: nil => - do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; - OK (Pfmul S rd rs1 rs2 :: k) - | Odivfs, a1 :: a2 :: nil => - do rd <- freg_of res; do rs1 <- freg_of a1; do rs2 <- freg_of a2; - OK (Pfdiv S rd rs1 rs2 :: k) - | Osingleoffloat, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfcvtsd rd rs :: k) - | Ofloatofsingle, a1 :: nil => - do rd <- freg_of res; do rs <- freg_of a1; - OK (Pfcvtds rd rs :: k) -(** Conversions between int and float *) - | Ointoffloat, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzs W D rd rs :: k) - | Ointuoffloat, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzu W D rd rs :: k) - | Ofloatofint, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pscvtf D W rd rs :: k) - | Ofloatofintu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pucvtf D W rd rs :: k) - | Ointofsingle, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzs W S rd rs :: k) - | Ointuofsingle, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzu W S rd rs :: k) - | Osingleofint, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pscvtf S W rd rs :: k) - | Osingleofintu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pucvtf S W rd rs :: k) - | Olongoffloat, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzs X D rd rs :: k) - | Olonguoffloat, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzu X D rd rs :: k) - | Ofloatoflong, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pscvtf D X rd rs :: k) - | Ofloatoflongu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pucvtf D X rd rs :: k) - | Olongofsingle, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzs X S rd rs :: k) - | Olonguofsingle, a1 :: nil => - do rd <- ireg_of res; do rs <- freg_of a1; - OK (Pfcvtzu X S rd rs :: k) - | Osingleoflong, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pscvtf S X rd rs :: k) - | Osingleoflongu, a1 :: nil => - do rd <- freg_of res; do rs <- ireg_of a1; - OK (Pucvtf S X rd rs :: k) -(** Boolean tests *) - | Ocmp c, _ => - do rd <- ireg_of res; - transl_cond c args (Pcset rd (cond_for_cond c) :: k) -(** Conditional move *) - | Osel cmp ty, a1 :: a2 :: args => - match preg_of res with - | IR r => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - transl_cond cmp args (Pcsel r r1 r2 (cond_for_cond cmp) :: k) - | FR r => - do r1 <- freg_of a1; do r2 <- freg_of a2; - transl_cond cmp args (Pfsel r r1 r2 (cond_for_cond cmp) :: k) - | _ => - Error(msg "Asmgen.Osel") - end - | _, _ => - Error(msg "Asmgen.transl_op") - end. - -(** Translation of addressing modes *) - -Definition offset_representable (sz: Z) (ofs: int64) : bool := - let isz := Int64.repr sz in - (** either unscaled 9-bit signed *) - Int64.eq ofs (Int64.sign_ext 9 ofs) || - (** or scaled 12-bit unsigned *) - (Int64.eq (Int64.modu ofs isz) Int64.zero - && Int64.ltu ofs (Int64.shl isz (Int64.repr 12))). - -Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) - (insn: Asm.addressing -> instruction) (k: code) : res code := - match addr, args with - | Aindexed ofs, a1 :: nil => - do r1 <- ireg_of a1; - if offset_representable sz ofs then - OK (insn (ADimm r1 ofs) :: k) - else - OK (loadimm64 X16 ofs (insn (ADreg r1 X16) :: k)) - | Aindexed2, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (insn (ADreg r1 r2) :: k) - | Aindexed2shift a, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - if Int.eq a Int.zero then - OK (insn (ADreg r1 r2) :: k) - else if Int.eq (Int.shl Int.one a) (Int.repr sz) then - OK (insn (ADlsl r1 r2 a) :: k) - else - OK (Padd X X16 r1 r2 (SOlsl a) :: insn (ADimm X16 Int64.zero) :: k) - | Aindexed2ext x a, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then - OK (insn (match x with Xsgn32 => ADsxt r1 r2 a - | Xuns32 => ADuxt r1 r2 a end) :: k) - else - OK (arith_extended Paddext (Padd X) X16 r1 r2 x a - (insn (ADimm X16 Int64.zero) :: k)) - | Aglobal id ofs, nil => - assertion (negb (Archi.pic_code tt)); - if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz - then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k) - else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k)) - | Ainstack ofs, nil => - let ofs := Ptrofs.to_int64 ofs in - if offset_representable sz ofs then - OK (insn (ADimm XSP ofs) :: k) - else - OK (loadimm64 X16 ofs (insn (ADreg XSP X16) :: k)) - | _, _ => - Error(msg "Asmgen.transl_addressing") - end. - -(** Translation of loads and stores *) - -Definition transl_load (trap: trapping_mode) - (chunk: memory_chunk) (addr: Op.addressing) - (args: list mreg) (dst: mreg) (k: code) : res code := - match trap with - | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on aarch64") - | TRAP => - match chunk with - | Mint8unsigned => - do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrb W rd) k - | Mint8signed => - do rd <- ireg_of dst; transl_addressing 1 addr args (Pldrsb W rd) k - | Mint16unsigned => - do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrh W rd) k - | Mint16signed => - do rd <- ireg_of dst; transl_addressing 2 addr args (Pldrsh W rd) k - | Mint32 => - do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw rd) k - | Mint64 => - do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx rd) k - | Mfloat32 => - do rd <- freg_of dst; transl_addressing 4 addr args (Pldrs rd) k - | Mfloat64 => - do rd <- freg_of dst; transl_addressing 8 addr args (Pldrd rd) k - | Many32 => - do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw_a rd) k - | Many64 => - do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx_a rd) k - end - end. - -Definition transl_store (chunk: memory_chunk) (addr: Op.addressing) - (args: list mreg) (src: mreg) (k: code) : res code := - match chunk with - | Mint8unsigned | Mint8signed => - do r1 <- ireg_of src; transl_addressing 1 addr args (Pstrb r1) k - | Mint16unsigned | Mint16signed => - do r1 <- ireg_of src; transl_addressing 2 addr args (Pstrh r1) k - | Mint32 => - do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw r1) k - | Mint64 => - do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx r1) k - | Mfloat32 => - do r1 <- freg_of src; transl_addressing 4 addr args (Pstrs r1) k - | Mfloat64 => - do r1 <- freg_of src; transl_addressing 8 addr args (Pstrd r1) k - | Many32 => - do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw_a r1) k - | Many64 => - do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx_a r1) k - end. - -(** Register-indexed loads and stores *) - -Definition indexed_memory_access (insn: Asm.addressing -> instruction) - (sz: Z) (base: iregsp) (ofs: ptrofs) (k: code) := - let ofs := Ptrofs.to_int64 ofs in - if offset_representable sz ofs - then insn (ADimm base ofs) :: k - else loadimm64 X16 ofs (insn (ADreg base X16) :: k). - -Definition loadind (base: iregsp) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := - match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access (Pldrw rd) 4 base ofs k) - | Tlong, IR rd => OK (indexed_memory_access (Pldrx rd) 8 base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access (Pldrs rd) 4 base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access (Pldrd rd) 8 base ofs k) - | Tany32, IR rd => OK (indexed_memory_access (Pldrw_a rd) 4 base ofs k) - | Tany64, IR rd => OK (indexed_memory_access (Pldrx_a rd) 8 base ofs k) - | Tany64, FR rd => OK (indexed_memory_access (Pldrd_a rd) 8 base ofs k) - | _, _ => Error (msg "Asmgen.loadind") - end. - -Definition storeind (src: mreg) (base: iregsp) (ofs: ptrofs) (ty: typ) (k: code) := - match ty, preg_of src with - | Tint, IR rd => OK (indexed_memory_access (Pstrw rd) 4 base ofs k) - | Tlong, IR rd => OK (indexed_memory_access (Pstrx rd) 8 base ofs k) - | Tsingle, FR rd => OK (indexed_memory_access (Pstrs rd) 4 base ofs k) - | Tfloat, FR rd => OK (indexed_memory_access (Pstrd rd) 8 base ofs k) - | Tany32, IR rd => OK (indexed_memory_access (Pstrw_a rd) 4 base ofs k) - | Tany64, IR rd => OK (indexed_memory_access (Pstrx_a rd) 8 base ofs k) - | Tany64, FR rd => OK (indexed_memory_access (Pstrd_a rd) 8 base ofs k) - | _, _ => Error (msg "Asmgen.storeind") - end. - -Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: code) := - indexed_memory_access (Pldrx dst) 8 base ofs k. - -Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) := - indexed_memory_access (Pstrx src) 8 base ofs k. - -(** Function epilogue *) - -Definition make_epilogue (f: Mach.function) (k: code) := - (* 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) :: k). - -(** Translation of a Mach instruction. *) - -Definition transl_instr (f: Mach.function) (i: Mach.instruction) - (r29_is_parent: bool) (k: code) : res code := - match i with - | Mgetstack ofs ty dst => - loadind XSP ofs ty dst k - | Msetstack src ofs ty => - storeind src XSP ofs ty k - | Mgetparam ofs ty dst => - (* load via the frame pointer if it is valid *) - do c <- loadind X29 ofs ty dst k; - OK (if r29_is_parent then c else loadptr XSP f.(fn_link_ofs) X29 c) - | Mop op args res => - transl_op op args res k - | Mload trap chunk addr args dst => - transl_load trap chunk addr args dst k - | Mstore chunk addr args src => - transl_store chunk addr args src k - | Mcall sig (inl r) => - do r1 <- ireg_of r; OK (Pblr r1 sig :: k) - | Mcall sig (inr symb) => - OK (Pbl symb sig :: k) - | Mtailcall sig (inl r) => - do r1 <- ireg_of r; - OK (make_epilogue f (Pbr r1 sig :: k)) - | Mtailcall sig (inr symb) => - OK (make_epilogue f (Pbs symb sig :: k)) - | Mbuiltin ef args res => - OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k) - | Mlabel lbl => - OK (Plabel lbl :: k) - | Mgoto lbl => - OK (Pb lbl :: k) - | Mcond cond args lbl => - transl_cond_branch cond args lbl k - | Mjumptable arg tbl => - do r <- ireg_of arg; - OK (Pbtbl r tbl :: k) - | Mreturn => - OK (make_epilogue f (Pret RA :: k)) - end. - -(** Translation of a code sequence *) - -Definition it1_is_parent (before: bool) (i: Mach.instruction) : bool := - match i with - | Msetstack src ofs ty => before - | Mgetparam ofs ty dst => negb (mreg_eq dst R29) - | Mop op args res => before && negb (mreg_eq res R29) - | _ => false - end. - -(** This is the naive definition that we no longer use because it - is not tail-recursive. It is kept as specification. *) - -Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := - match il with - | nil => OK nil - | i1 :: il' => - do k <- transl_code f il' (it1_is_parent it1p i1); - transl_instr f i1 it1p k - end. - -(** This is an equivalent definition in continuation-passing style - that runs in constant stack space. *) - -Fixpoint transl_code_rec (f: Mach.function) (il: list Mach.instruction) - (it1p: bool) (k: code -> res code) := - match il with - | nil => k nil - | i1 :: il' => - transl_code_rec f il' (it1_is_parent it1p i1) - (fun c1 => do c2 <- transl_instr f i1 it1p c1; k c2) - end. - -Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bool) := - transl_code_rec f il it1p (fun c => OK c). +Require Import Locations Asmblock Asm. -(** Translation of a whole function. Note that we must check - that the generated code contains less than [2^32] instructions, - otherwise the offset part of the [PC] code pointer could wrap - around, leading to incorrect executions. *) +(** * Translation from Asmblock to assembly language + Inspired from the KVX backend. *) -Definition transl_function (f: Mach.function) := - do c <- transl_code' f f.(Mach.fn_code) true; - OK (mkfunction f.(Mach.fn_sig) - (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) :: - storeptr RA XSP f.(fn_retaddr_ofs) c)). +(* STUB *) -Definition transf_function (f: Mach.function) : res Asm.function := - do tf <- transl_function f; - if zlt Ptrofs.max_unsigned (list_length_z tf.(fn_code)) - then Error (msg "code size exceeded") - else OK tf. +Definition transf_function (f: Asmblock.function) : res Asm.function := + Error (msg "Asmgen not yet implmented"). -Definition transf_fundef (f: Mach.fundef) : res Asm.fundef := +Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef := transf_partial_fundef transf_function f. -Definition transf_program (p: Mach.program) : res Asm.program := +Definition transf_program (p: Asmblock.program) : res Asm.program := transform_partial_program transf_fundef p. diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 6831509f..e69de29b 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1,1101 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, Collège de France and INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for AArch64 code generation. *) - -Require Import Coqlib Errors. -Require Import Integers Floats AST Linking. -Require Import Values Memory Events Globalenvs Smallstep. -Require Import Op Locations Mach Conventions Asm. -Require Import Asmgen Asmgenproof0 Asmgenproof1. - -Definition match_prog (p: Mach.program) (tp: Asm.program) := - match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. - -Lemma transf_program_match: - forall p tp, transf_program p = OK tp -> match_prog p tp. -Proof. - intros. eapply match_transform_partial_program; eauto. -Qed. - -Section PRESERVATION. - -Variable prog: Mach.program. -Variable tprog: Asm.program. -Hypothesis TRANSF: match_prog prog tprog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof (Genv.find_symbol_match TRANSF). - -Lemma senv_preserved: - Senv.equiv ge tge. -Proof (Genv.senv_match TRANSF). - -Lemma functions_translated: - forall b f, - Genv.find_funct_ptr ge b = Some f -> - exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial TRANSF). - -Lemma functions_transl: - forall fb f tf, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - transf_function f = OK tf -> - Genv.find_funct_ptr tge fb = Some (Internal tf). -Proof. - intros. exploit functions_translated; eauto. intros [tf' [A B]]. - monadInv B. rewrite H0 in EQ; inv EQ; auto. -Qed. - -(** * Properties of control flow *) - -Lemma transf_function_no_overflow: - forall f tf, - transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. -Proof. - intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - omega. -Qed. - -Lemma exec_straight_exec: - forall fb f c ep tf tc c' rs m rs' m', - transl_code_at_pc ge (rs PC) fb f c ep tf tc -> - exec_straight tge tf tc rs m c' rs' m' -> - plus step tge (State rs m) E0 (State rs' m'). -Proof. - intros. inv H. - eapply exec_straight_steps_1; eauto. - eapply transf_function_no_overflow; eauto. - eapply functions_transl; eauto. -Qed. - -Lemma exec_straight_at: - forall fb f c ep tf tc c' ep' tc' rs m rs' m', - transl_code_at_pc ge (rs PC) fb f c ep tf tc -> - transl_code f c' ep' = OK tc' -> - exec_straight tge tf tc rs m tc' rs' m' -> - transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'. -Proof. - intros. inv H. - exploit exec_straight_steps_2; eauto. - eapply transf_function_no_overflow; eauto. - eapply functions_transl; eauto. - intros [ofs' [PC' CT']]. - rewrite PC'. constructor; auto. -Qed. - -(** The following lemmas show that the translation from Mach to Asm - preserves labels, in the sense that the following diagram commutes: -<< - translation - Mach code ------------------------ Asm instr sequence - | | - | Mach.find_label lbl find_label lbl | - | | - v v - Mach code tail ------------------- Asm instr seq tail - translation ->> - The proof demands many boring lemmas showing that Asm constructor - functions do not introduce new labels. -*) - -Section TRANSL_LABEL. - -Remark loadimm_z_label: forall sz rd l k, tail_nolabel k (loadimm_z sz rd l k). -Proof. - intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel. - induction l as [ | [n p] l]; simpl; TailNoLabel. -Qed. - -Remark loadimm_n_label: forall sz rd l k, tail_nolabel k (loadimm_n sz rd l k). -Proof. - intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel. - induction l as [ | [n p] l]; simpl; TailNoLabel. -Qed. - -Remark loadimm_label: forall sz rd n k, tail_nolabel k (loadimm sz rd n k). -Proof. - unfold loadimm; intros. destruct Nat.leb; [apply loadimm_z_label|apply loadimm_n_label]. -Qed. -Hint Resolve loadimm_label: labels. - -Remark loadimm32_label: forall r n k, tail_nolabel k (loadimm32 r n k). -Proof. - unfold loadimm32; intros. destruct (is_logical_imm32 n); TailNoLabel. -Qed. -Hint Resolve loadimm32_label: labels. - -Remark loadimm64_label: forall r n k, tail_nolabel k (loadimm64 r n k). -Proof. - unfold loadimm64; intros. destruct (is_logical_imm64 n); TailNoLabel. -Qed. -Hint Resolve loadimm64_label: labels. - -Remark addimm_aux: forall insn rd r1 n k, - (forall rd r1 n, nolabel (insn rd r1 n)) -> - tail_nolabel k (addimm_aux insn rd r1 n k). -Proof. - unfold addimm_aux; intros. - destruct Z.eqb. TailNoLabel. destruct Z.eqb; TailNoLabel. -Qed. - -Remark addimm32_label: forall rd r1 n k, tail_nolabel k (addimm32 rd r1 n k). -Proof. - unfold addimm32; intros. - destruct Int.eq. apply addimm_aux; intros; red; auto. - destruct Int.eq. apply addimm_aux; intros; red; auto. - destruct Int.lt; eapply tail_nolabel_trans; TailNoLabel. -Qed. -Hint Resolve addimm32_label: labels. - -Remark addimm64_label: forall rd r1 n k, tail_nolabel k (addimm64 rd r1 n k). -Proof. - unfold addimm64; intros. - destruct Int64.eq. apply addimm_aux; intros; red; auto. - destruct Int64.eq. apply addimm_aux; intros; red; auto. - destruct Int64.lt; eapply tail_nolabel_trans; TailNoLabel. -Qed. -Hint Resolve addimm64_label: labels. - -Remark logicalimm32_label: forall insn1 insn2 rd r1 n k, - (forall rd r1 n, nolabel (insn1 rd r1 n)) -> - (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) -> - tail_nolabel k (logicalimm32 insn1 insn2 rd r1 n k). -Proof. - unfold logicalimm32; intros. - destruct (is_logical_imm32 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -Qed. - -Remark logicalimm64_label: forall insn1 insn2 rd r1 n k, - (forall rd r1 n, nolabel (insn1 rd r1 n)) -> - (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) -> - tail_nolabel k (logicalimm64 insn1 insn2 rd r1 n k). -Proof. - unfold logicalimm64; intros. - destruct (is_logical_imm64 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -Qed. - -Remark move_extended_label: forall rd r1 ex a k, tail_nolabel k (move_extended rd r1 ex a k). -Proof. - unfold move_extended, move_extended_base; intros. destruct Int.eq, ex; TailNoLabel. -Qed. -Hint Resolve move_extended_label: labels. - -Remark arith_extended_label: forall insnX insnS rd r1 r2 ex a k, - (forall rd r1 r2 x, nolabel (insnX rd r1 r2 x)) -> - (forall rd r1 r2 s, nolabel (insnS rd r1 r2 s)) -> - tail_nolabel k (arith_extended insnX insnS rd r1 r2 ex a k). -Proof. - unfold arith_extended; intros. destruct Int.ltu. - TailNoLabel. - destruct ex; simpl; TailNoLabel. -Qed. - -Remark loadsymbol_label: forall r id ofs k, tail_nolabel k (loadsymbol r id ofs k). -Proof. - intros; unfold loadsymbol. - destruct (Archi.pic_code tt); TailNoLabel. destruct Ptrofs.eq; TailNoLabel. -Qed. -Hint Resolve loadsymbol_label: labels. - -Remark transl_cond_label: forall cond args k c, - transl_cond cond args k = OK c -> tail_nolabel k c. -Proof. - unfold transl_cond; intros; destruct cond; TailNoLabel. -- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -Qed. - -Remark transl_cond_branch_default_label: forall cond args lbl k c, - transl_cond_branch_default cond args lbl k = OK c -> tail_nolabel k c. -Proof. - unfold transl_cond_branch_default; intros. - eapply tail_nolabel_trans; [eapply transl_cond_label;eauto|TailNoLabel]. -Qed. -Hint Resolve transl_cond_branch_default_label: labels. - -Remark transl_cond_branch_label: forall cond args lbl k c, - transl_cond_branch cond args lbl k = OK c -> tail_nolabel k c. -Proof. - unfold transl_cond_branch; intros; destruct args; TailNoLabel; destruct cond; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct (Int.is_power2 n); TailNoLabel. -- destruct (Int.is_power2 n); TailNoLabel. -- destruct c0; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct (Int64.is_power2' n); TailNoLabel. -- destruct (Int64.is_power2' n); TailNoLabel. -Qed. - -Remark transl_op_label: - forall op args r k c, - transl_op op args r k = OK c -> tail_nolabel k c. -Proof. - unfold transl_op; intros; destruct op; TailNoLabel. -- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. -- destruct (Float.eq_dec n Float.zero); TailNoLabel. -- destruct (Float32.eq_dec n Float32.zero); TailNoLabel. -- apply logicalimm32_label; unfold nolabel; auto. -- apply logicalimm32_label; unfold nolabel; auto. -- apply logicalimm32_label; unfold nolabel; auto. -- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. -- apply arith_extended_label; unfold nolabel; auto. -- apply arith_extended_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. -- eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. -- destruct (preg_of r); try discriminate; TailNoLabel; - (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]). -Qed. - -Remark transl_addressing_label: - forall sz addr args insn k c, - transl_addressing sz addr args insn k = OK c -> - (forall ad, nolabel (insn ad)) -> - tail_nolabel k c. -Proof. - unfold transl_addressing; intros; destruct addr; TailNoLabel; - eapply tail_nolabel_trans; TailNoLabel. - eapply tail_nolabel_trans. apply arith_extended_label; unfold nolabel; auto. TailNoLabel. -Qed. - -Remark transl_load_label: - forall trap chunk addr args dst k c, - transl_load trap chunk addr args dst k = OK c -> tail_nolabel k c. -Proof. - unfold transl_load; intros; destruct trap; try discriminate; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto. -Qed. - -Remark transl_store_label: - forall chunk addr args src k c, - transl_store chunk addr args src k = OK c -> tail_nolabel k c. -Proof. - unfold transl_store; intros; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto. -Qed. - -Remark indexed_memory_access_label: - forall insn sz base ofs k, - (forall ad, nolabel (insn ad)) -> - tail_nolabel k (indexed_memory_access insn sz base ofs k). -Proof. - unfold indexed_memory_access; intros. destruct offset_representable. - TailNoLabel. - eapply tail_nolabel_trans; TailNoLabel. -Qed. - -Remark loadind_label: - forall base ofs ty dst k c, - loadind base ofs ty dst k = OK c -> tail_nolabel k c. -Proof. - unfold loadind; intros. - destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I. -Qed. - -Remark storeind_label: - forall src base ofs ty k c, - storeind src base ofs ty k = OK c -> tail_nolabel k c. -Proof. - unfold storeind; intros. - destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I. -Qed. - -Remark loadptr_label: - forall base ofs dst k, tail_nolabel k (loadptr base ofs dst k). -Proof. - intros. apply indexed_memory_access_label. unfold nolabel; auto. -Qed. - -Remark storeptr_label: - forall src base ofs k, tail_nolabel k (storeptr src base ofs k). -Proof. - intros. apply indexed_memory_access_label. unfold nolabel; auto. -Qed. - -Remark make_epilogue_label: - forall f k, tail_nolabel k (make_epilogue f k). -Proof. - unfold make_epilogue; intros. - (* FIXME destruct is_leaf_function. - { TailNoLabel. } *) - eapply tail_nolabel_trans. - apply loadptr_label. - TailNoLabel. -Qed. - -Lemma transl_instr_label: - forall f i ep k c, - transl_instr f i ep k = OK c -> - match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end. -Proof. - unfold transl_instr; intros; destruct i; TailNoLabel. -- eapply loadind_label; eauto. -- eapply storeind_label; eauto. -- destruct ep. eapply loadind_label; eauto. - eapply tail_nolabel_trans. apply loadptr_label. eapply loadind_label; eauto. -- eapply transl_op_label; eauto. -- eapply transl_load_label; eauto. -- eapply transl_store_label; eauto. -- destruct s0; monadInv H; TailNoLabel. -- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]). -- eapply transl_cond_branch_label; eauto. -- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]. -Qed. - -Lemma transl_instr_label': - forall lbl f i ep k c, - transl_instr f i ep k = OK c -> - find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. -Proof. - intros. exploit transl_instr_label; eauto. - destruct i; try (intros [A B]; apply B). - intros. subst c. simpl. auto. -Qed. - -Lemma transl_code_label: - forall lbl f c ep tc, - transl_code f c ep = OK tc -> - match Mach.find_label lbl c with - | None => find_label lbl tc = None - | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc' - end. -Proof. - induction c; simpl; intros. - inv H. auto. - monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0). - generalize (Mach.is_label_correct lbl a). - destruct (Mach.is_label lbl a); intros. - subst a. simpl in EQ. exists x; auto. - eapply IHc; eauto. -Qed. - -Lemma transl_find_label: - forall lbl f tf, - transf_function f = OK tf -> - match Mach.find_label lbl f.(Mach.fn_code) with - | None => find_label lbl tf.(fn_code) = None - | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc - end. -Proof. - intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. - simpl. destruct (storeptr_label X30 XSP (fn_retaddr_ofs f) x) as [A B]; rewrite B. - eapply transl_code_label; eauto. -Qed. - -End TRANSL_LABEL. - -(** A valid branch in a piece of Mach code translates to a valid ``go to'' - transition in the generated Asm code. *) - -Lemma find_label_goto_label: - forall f tf lbl rs m c' b ofs, - Genv.find_funct_ptr ge b = Some (Internal f) -> - transf_function f = OK tf -> - rs PC = Vptr b ofs -> - Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - exists tc', exists rs', - goto_label tf lbl rs m = Next rs' m - /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' - /\ forall r, r <> PC -> rs'#r = rs#r. -Proof. - intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. - intros [tc [A B]]. - exploit label_pos_code_tail; eauto. instantiate (1 := 0). - intros [pos' [P [Q R]]]. - exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))). - split. unfold goto_label. rewrite P. rewrite H1. auto. - split. rewrite Pregmap.gss. constructor; auto. - rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. - intros. apply Pregmap.gso; auto. -Qed. - -(** Existence of return addresses *) - -Lemma return_address_exists: - forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> - exists ra, return_address_offset f c ra. -Proof. - intros. eapply Asmgenproof0.return_address_exists; eauto. -- intros. exploit transl_instr_label; eauto. - destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. -- intros. monadInv H0. - destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. - rewrite transl_code'_transl_code in EQ0. - exists x; exists true; split; auto. unfold fn_code. - constructor. apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) x). -- exact transf_function_no_overflow. -Qed. - -(** * Proof of semantic preservation *) - -(** Semantic preservation is proved using simulation diagrams - of the following form. -<< - st1 --------------- st2 - | | - t| *|t - | | - v v - st1'--------------- st2' ->> - The invariant is the [match_states] predicate below, which includes: -- The Asm code pointed by the PC register is the translation of - the current Mach code sequence. -- Mach register values and Asm register values agree. -*) - -Inductive match_states: Mach.state -> Asm.state -> Prop := - | match_states_intro: - forall s fb sp c ep ms m m' rs f tf tc - (STACKS: match_stack ge s) - (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) - (MEXT: Mem.extends m m') - (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) - (AG: agree ms sp rs) - (DXP: ep = true -> rs#X29 = parent_sp s) - (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s), - match_states (Mach.State s fb sp c ms m) - (Asm.State rs m') - | match_states_call: - forall s fb ms m m' rs - (STACKS: match_stack ge s) - (MEXT: Mem.extends m m') - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = Vptr fb Ptrofs.zero) - (ATLR: rs RA = parent_ra s), - match_states (Mach.Callstate s fb ms m) - (Asm.State rs m') - | match_states_return: - forall s ms m m' rs - (STACKS: match_stack ge s) - (MEXT: Mem.extends m m') - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = parent_ra s), - match_states (Mach.Returnstate s ms m) - (Asm.State rs m'). - -Lemma exec_straight_steps: - forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2, - match_stack ge s -> - Mem.extends m2 m2' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - (forall k c (TR: transl_instr f i ep k = OK c), - exists rs2, - exec_straight tge tf c rs1 m1' k rs2 m2' - /\ agree ms2 sp rs2 - /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s) - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c ms2 m2) st'. -Proof. - intros. inversion H2. subst. monadInv H7. - exploit H3; eauto. intros [rs2 [A [B [C D]]]]. - exists (State rs2 m2'); split. - - eapply exec_straight_exec; eauto. - - econstructor; eauto. eapply exec_straight_at; eauto. -Qed. - -Lemma exec_straight_steps_goto: - forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', - match_stack ge s -> - Mem.extends m2 m2' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - it1_is_parent ep i = false -> - (forall k c (TR: transl_instr f i ep k = OK c), - exists jmp, exists k', exists rs2, - exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' - /\ agree ms2 sp rs2 - /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c' ms2 m2) st'. -Proof. - intros. inversion H3. subst. monadInv H9. - exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]]. - generalize (functions_transl _ _ _ H7 H8); intro FN. - generalize (transf_function_no_overflow _ _ H8); intro NOOV. - exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. - econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - traceEq. - econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. -Qed. - -Lemma exec_straight_opt_steps_goto: - forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', - match_stack ge s -> - Mem.extends m2 m2' -> - Genv.find_funct_ptr ge fb = Some (Internal f) -> - Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - it1_is_parent ep i = false -> - (forall k c (TR: transl_instr f i ep k = OK c), - exists jmp, exists k', exists rs2, - exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2' - /\ agree ms2 sp rs2 - /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c' ms2 m2) st'. -Proof. - intros. inversion H3. subst. monadInv H9. - exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]]. - generalize (functions_transl _ _ _ H7 H8); intro FN. - generalize (transf_function_no_overflow _ _ H8); intro NOOV. - inv A. -- exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - apply plus_one. econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. -- exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. - econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - traceEq. - econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. -Qed. - -(** We need to show that, in the simulation diagram, we cannot - take infinitely many Mach transitions that correspond to zero - transitions on the Asm side. Actually, all Mach transitions - correspond to at least one Asm transition, except the - transition from [Machsem.Returnstate] to [Machsem.State]. - So, the following integer measure will suffice to rule out - the unwanted behaviour. *) - -Definition measure (s: Mach.state) : nat := - match s with - | Mach.State _ _ _ _ _ _ => 0%nat - | Mach.Callstate _ _ _ _ => 0%nat - | Mach.Returnstate _ _ _ => 1%nat - end. - -Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r. -Proof. - intros. change (IR X29) with (preg_of R29). red; intros. - exploit preg_of_injective; eauto. intros; subst r; discriminate. -Qed. - -Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP. -Proof. - intros. eapply sp_val; eauto. -Qed. - -(** This is the simulation diagram. We prove it by case analysis on the Mach transition. *) - -Theorem step_simulation: - forall S1 t S2, Mach.step return_address_offset ge S1 t S2 -> - forall S1' (MS: match_states S1 S1') (WF: wf_state ge S1), - (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') - \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. -Proof. - induction 1; intros; inv MS. - -- (* Mlabel *) - left; eapply exec_straight_steps; eauto; intros. - monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. { apply agree_nextinstr; auto. } - split. { simpl; congruence. } - rewrite nextinstr_inv by congruence; assumption. - -- (* Mgetstack *) - unfold load_stack in H. - exploit Mem.loadv_extends; eauto. intros [v' [A B]]. - rewrite (sp_val _ _ _ AG) in A. - left; eapply exec_straight_steps; eauto. intros. simpl in TR. - exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]]. - exists rs'; split. eauto. - split. { eapply agree_set_mreg; eauto with asmgen. congruence. } - split. { simpl; congruence. } - rewrite S. assumption. - -- (* Msetstack *) - unfold store_stack in H. - assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto). - exploit Mem.storev_extends; eauto. intros [m2' [A B]]. - left; eapply exec_straight_steps; eauto. - rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. - exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]]. - exists rs'; split. eauto. - split. eapply agree_undef_regs; eauto with asmgen. - simpl; intros. - split. rewrite Q; auto with asmgen. - rewrite R. assumption. - -- (* Mgetparam *) - assert (f0 = f) by congruence; subst f0. - unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. auto. - intros [parent' [A B]]. rewrite (sp_val' _ _ _ AG) in A. - exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. - exploit Mem.loadv_extends. eauto. eexact H1. auto. - intros [v' [C D]]. -Opaque loadind. - left; eapply exec_straight_steps; eauto; intros. monadInv TR. - destruct ep. -(* X30 contains parent *) - exploit loadind_correct. eexact EQ. - instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence. - intros [rs1 [P [Q [R S]]]]. - exists rs1; split. eauto. - split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. - simpl; split; intros. - { rewrite R; auto with asmgen. - apply preg_of_not_X29; auto. - } - { rewrite S; auto. } - -(* X30 does not contain parent *) - exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]]. - exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence. - intros [rs2 [S [T [U V]]]]. - exists rs2; split. eapply exec_straight_trans; eauto. - split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. - instantiate (1 := rs1#X29 <- (rs2#X29)). intros. - rewrite Pregmap.gso; auto with asmgen. - congruence. - intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen. - split; simpl; intros. rewrite U; auto with asmgen. - apply preg_of_not_X29; auto. - rewrite V. rewrite R by congruence. auto. - -- (* Mop *) - assert (eval_operation tge sp op (map rs args) m = Some v). - { rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. } - exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. - intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. - left; eapply exec_straight_steps; eauto; intros. simpl in TR. - exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]]. - exists rs2; split. eauto. split. - apply agree_set_undef_mreg with rs0; auto. - apply Val.lessdef_trans with v'; auto. - split; simpl; intros. InvBooleans. - rewrite R; auto. apply preg_of_not_X29; auto. -Local Transparent destroyed_by_op. - destruct op; try exact I; simpl; congruence. - rewrite S. - auto. -- (* Mload *) - destruct trap. - { - assert (Op.eval_addressing tge sp addr (map rs args) = Some a). - { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. } - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. - intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. - exploit Mem.loadv_extends; eauto. intros [v' [C D]]. - left; eapply exec_straight_steps; eauto; intros. simpl in TR. - exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]]. - exists rs2; split. eauto. - split. eapply agree_set_undef_mreg; eauto. congruence. - split. simpl; congruence. - rewrite S. assumption. - } - - (* Mload notrap1 *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mload notrap *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mload notrap *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mstore *) - assert (Op.eval_addressing tge sp addr (map rs args) = Some a). - { rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. } - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. - intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. - assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto). - exploit Mem.storev_extends; eauto. intros [m2' [C D]]. - left; eapply exec_straight_steps; eauto. - intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]]. - exists rs2; split. eauto. - split. eapply agree_undef_regs; eauto with asmgen. - split. simpl; congruence. - rewrite R. assumption. - -- (* Mcall *) - assert (f0 = f) by congruence. subst f0. - inv AT. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - { eapply transf_function_no_overflow; eauto. } - destruct ros as [rf|fid]; simpl in H; monadInv H5. -+ (* Indirect call *) - assert (rs rf = Vptr f' Ptrofs.zero). - { destruct (rs rf); try discriminate. - revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } - assert (rs0 x0 = Vptr f' Ptrofs.zero). - { exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. } - generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). - { econstructor; eauto. } - exploit return_address_offset_correct; eauto. intros; subst ra. - left; econstructor; split. - apply plus_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. eauto. - econstructor; eauto. - econstructor; eauto. - eapply agree_sp_def; eauto. - simpl. eapply agree_exten; eauto. intros. Simpl. - Simpl. rewrite <- H2. auto. -+ (* Direct call *) - generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). - econstructor; eauto. - exploit return_address_offset_correct; eauto. intros; subst ra. - left; econstructor; split. - apply plus_one. eapply exec_step_internal. eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto. - econstructor; eauto. - econstructor; eauto. - eapply agree_sp_def; eauto. - simpl. eapply agree_exten; eauto. intros. Simpl. - Simpl. rewrite <- H2. auto. - -- (* Mtailcall *) - assert (f0 = f) by congruence. subst f0. - inversion AT; subst. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - { eapply transf_function_no_overflow; eauto. } - exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. - destruct ros as [rf|fid]; simpl in H; monadInv H7. -+ (* Indirect call *) - assert (rs rf = Vptr f' Ptrofs.zero). - { destruct (rs rf); try discriminate. - revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } - assert (rs0 x0 = Vptr f' Ptrofs.zero). - { exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. } - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. - Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. -+ (* Direct call *) - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. - Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - -- (* Mbuiltin *) - inv AT. monadInv H4. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit builtin_args_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. - intros [vres' [m2' [A [B [C D]]]]]. - left. econstructor; split. apply plus_one. - eapply exec_step_builtin. eauto. eauto. - eapply find_instr_tail; eauto. - erewrite <- sp_val by eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - eauto. - econstructor; eauto. - instantiate (2 := tf); instantiate (1 := x). - unfold nextinstr. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. - rewrite <- H1. simpl. econstructor; eauto. - eapply code_tail_next_int; eauto. - rewrite preg_notin_charact. intros. auto with asmgen. - auto with asmgen. - apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. - congruence. - - Simpl. - rewrite set_res_other by trivial. - rewrite undef_regs_other. - assumption. - intro. - rewrite in_map_iff. - intros (x0 & PREG & IN). - subst r'. - intro. - apply (preg_of_not_RA x0). - congruence. - -- (* Mgoto *) - assert (f0 = f) by congruence. subst f0. - inv AT. monadInv H4. - exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. - left; exists (State rs' m'); split. - apply plus_one. econstructor; eauto. - eapply functions_transl; eauto. - eapply find_instr_tail; eauto. - simpl; eauto. - econstructor; eauto. - eapply agree_exten; eauto with asmgen. - congruence. - - rewrite INV by congruence. - assumption. - -- (* Mcond true *) - assert (f0 = f) by congruence. subst f0. - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. - left; eapply exec_straight_opt_steps_goto; eauto. - intros. simpl in TR. - exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). - exists jmp; exists k; exists rs'. - split. eexact A. - split. apply agree_exten with rs0; auto with asmgen. - split. - exact B. - rewrite D. exact LEAF. - -- (* Mcond false *) - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. - left; eapply exec_straight_steps; eauto. intros. simpl in TR. - exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). - econstructor; split. - eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto. - split. apply agree_exten with rs0; auto. intros. Simpl. - split. - simpl; congruence. - Simpl. rewrite D. - exact LEAF. - -- (* Mjumptable *) - assert (f0 = f) by congruence. subst f0. - inv AT. monadInv H6. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H5); intro NOOV. - exploit find_label_goto_label. eauto. eauto. - instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef). - Simpl. eauto. - eauto. - intros [tc' [rs' [A [B C]]]]. - exploit ireg_val; eauto. rewrite H. intros LD; inv LD. - left; econstructor; split. - apply plus_one. econstructor; eauto. - eapply find_instr_tail; eauto. - simpl. Simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. - econstructor; eauto. - eapply agree_undef_regs; eauto. - simpl. intros. rewrite C; auto with asmgen. Simpl. - congruence. - - rewrite C by congruence. - repeat rewrite Pregmap.gso by congruence. - assumption. - -- (* Mreturn *) - assert (f0 = f) by congruence. subst f0. - inversion AT; subst. simpl in H6; monadInv H6. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - eapply transf_function_no_overflow; eauto. - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. - -- (* internal function *) - - exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. - generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. - unfold store_stack in *. - exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. - intros [m1' [C D]]. - exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. - intros [m2' [F G]]. - simpl chunk_of_type in F. - exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. - intros [m3' [P Q]]. - change (chunk_of_type Tptr) with Mint64 in *. - (* Execution of function prologue *) - monadInv EQ0. rewrite transl_code'_transl_code in EQ1. - set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: - storeptr RA XSP (fn_retaddr_ofs f) x0) in *. - set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. - set (rs2 := nextinstr (rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef)). - exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2). - simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. - change (rs2 X2) with sp. eexact P. - simpl; congruence. congruence. - intros (rs3 & U & V & W). - assert (EXEC_PROLOGUE: - exec_straight tge tf - tf.(fn_code) rs0 m' - x0 rs3 m3'). - { change (fn_code tf) with tfbody; unfold tfbody. - apply exec_straight_step with rs2 m2'. - unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity. - reflexivity. - eexact U. } - exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. - intros (ofs' & X & Y). - left; exists (State rs3 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. - econstructor; eauto. - rewrite X; econstructor; eauto. - apply agree_exten with rs2; eauto with asmgen. - unfold rs2. - apply agree_nextinstr. apply agree_set_other; auto with asmgen. - apply agree_change_sp with (parent_sp s). - apply agree_undef_regs with rs0. auto. -Local Transparent destroyed_at_function_entry. simpl. - simpl; intros; Simpl. - unfold sp; congruence. - intros. rewrite V by auto with asmgen. reflexivity. - - rewrite W. - unfold rs2. - Simpl. - -- (* external function *) - exploit functions_translated; eauto. - intros [tf [A B]]. simpl in B. inv B. - exploit extcall_arguments_match; eauto. - intros [args' [C D]]. - exploit external_call_mem_extends; eauto. - intros [res' [m2' [P [Q [R S]]]]]. - left; econstructor; split. - apply plus_one. eapply exec_step_external; eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - econstructor; eauto. - unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. - apply agree_undef_caller_save_regs; auto. - -- (* return *) - inv STACKS. simpl in *. - right. split. omega. split. auto. - rewrite <- ATPC in H5. - econstructor; eauto. congruence. - inv WF. - inv STACK. - inv H1. - congruence. -Qed. - -Lemma transf_initial_states: - forall st1, Mach.initial_state prog st1 -> - exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. -Proof. - intros. inversion H. unfold ge0 in *. - econstructor; split. - econstructor. - eapply (Genv.init_mem_transf_partial TRANSF); eauto. - replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero) - with (Vptr fb Ptrofs.zero). - econstructor; eauto. - constructor. - apply Mem.extends_refl. - split. auto. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. - intros. rewrite Regmap.gi. auto. - unfold Genv.symbol_address. - rewrite (match_program_main TRANSF). - rewrite symbols_preserved. - unfold ge; rewrite H1. auto. -Qed. - -Lemma transf_final_states: - forall st1 st2 r, - match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r. -Proof. - intros. inv H0. inv H. constructor. assumption. - compute in H1. inv H1. - generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto. -Qed. - -Theorem transf_program_correct: - forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). -Proof. - eapply forward_simulation_star with (measure := measure) - (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1). - - apply senv_preserved. - - simpl; intros. exploit transf_initial_states; eauto. - intros (s2 & A & B). - exists s2; intuition auto. apply wf_initial; auto. - - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto. - - simpl; intros. destruct H0 as [MS WF]. - exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ]. - + left; exists s2'; intuition auto. eapply wf_step; eauto. - + right; intuition auto. eapply wf_step; eauto. -Qed. - -End PRESERVATION. @@ -847,8 +847,8 @@ ARCHDIRS=$arch kvx/lib kvx/abstractbb kvx/abstractbb/Impure BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v OptionMonad.v IterList.v PseudoAsmblock.v PseudoAsmblockproof.v ForwardSimulationBlock.v\\ AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\ ImpConfig.v ImpCore.v ImpExtern.v ImpHCons.v ImpIO.v ImpLoops.v ImpMonads.v ImpPrelude.v\\ - Asmblock.v\\ - Asmgenproof0.v Asmgenproof1.v Asmgenproof.v # TODO: CHANGE THIS + Asmblock.v Asmblockgen.v\\ + Asmgenproof.v # TODO: CHANGE THIS EOF fi |