From d5c95e0799e3b0541b07760178e68a1e72ee1b24 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sun, 21 Jun 2020 08:17:08 +0200 Subject: [WIP: Coq compilation broken] Stub for Asmgen --- aarch64/Asm.v | 530 ++++------------------------------------------------------ 1 file changed, 32 insertions(+), 498 deletions(-) (limited to 'aarch64/Asm.v') 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 -> -- cgit