diff options
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 589 |
1 files changed, 347 insertions, 242 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index b5f4c838..e5111220 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -10,13 +10,20 @@ (* *) (* *********************************************************************) -(** 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. + +*) 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. (** * Abstract syntax *) @@ -43,6 +50,9 @@ Coercion RR1: ireg >-> iregsp. Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. +Lemma iregsp_eq: forall (x y: iregsp), {x=y} + {x<>y}. +Proof. decide equality; apply ireg_eq. Defined. + (** In assembly files, [Dn] denotes the low 64-bit of a vector register, and [Sn] the low 32 bits. *) @@ -66,21 +76,29 @@ Inductive crbit: Type := Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. Proof. decide equality. Defined. +Inductive dreg : Type := + | IR: iregsp -> dreg (**r 64- or 32-bit integer registers *) + | FR: freg -> dreg. (**r double- or single-precision float registers *) + (** We model the following registers of the ARM architecture. *) Inductive preg: Type := - | 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. + | DR: dreg -> preg (** see dreg **) + | CR: crbit -> preg (**r bits in the condition register *) + | PC: preg. (**r program counter *) + +(* XXX: ireg no longer coerces to preg *) +Coercion IR: iregsp >-> dreg. +Coercion FR: freg >-> dreg. +Coercion DR: dreg >-> preg. +Definition SP:preg := XSP. Coercion CR: crbit >-> preg. +Lemma dreg_eq: forall (x y: dreg), {x=y} + {x<>y}. +Proof. decide equality. apply iregsp_eq. apply freg_eq. Defined. + Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined. +Proof. decide equality. apply dreg_eq. apply crbit_eq. Defined. Module PregEq. Definition t := preg. @@ -92,8 +110,6 @@ 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. @@ -177,14 +193,16 @@ Inductive instruction: Type := | Pldrsh (sz: isize) (rd: ireg) (a: addressing) (**r load int16, sign-extend *) | Pldrzw (rd: ireg) (a: addressing) (**r load int32, zero-extend to int64 *) | Pldrsw (rd: ireg) (a: addressing) (**r load int32, sign-extend to int64 *) - | Pldp (rd1 rd2: ireg) (a: addressing) (**r load two int64 *) + | Pldpw (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int32 *) + | Pldpx (rd1 rd2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two int64 *) | Pstrw (rs: ireg) (a: addressing) (**r store int32 *) | Pstrw_a (rs: ireg) (a: addressing) (**r store int32 as any32 *) | Pstrx (rs: ireg) (a: addressing) (**r store int64 *) | Pstrx_a (rs: ireg) (a: addressing) (**r store int64 as any64 *) | Pstrb (rs: ireg) (a: addressing) (**r store int8 *) | Pstrh (rs: ireg) (a: addressing) (**r store int16 *) - | Pstp (rs1 rs2: ireg) (a: addressing) (**r store two int64 *) + | Pstpw (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int32 *) + | Pstpx (rs1 rs2: ireg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two int64 *) (** Integer arithmetic, immediate *) | Paddimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z) (**r addition *) | Psubimm (sz: isize) (rd: iregsp) (r1: iregsp) (n: Z) (**r subtraction *) @@ -255,9 +273,13 @@ Inductive instruction: Type := | Pldrs (rd: freg) (a: addressing) (**r load float32 (single precision) *) | Pldrd (rd: freg) (a: addressing) (**r load float64 (double precision) *) | Pldrd_a (rd: freg) (a: addressing) (**r load float64 as any64 *) + | Pldps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two float32 *) + | Pldpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r load two float64 *) | Pstrs (rs: freg) (a: addressing) (**r store float32 *) | Pstrd (rs: freg) (a: addressing) (**r store float64 *) | Pstrd_a (rs: freg) (a: addressing) (**r store float64 as any64 *) + | Pstps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two float32 *) + | Pstpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two float64 *) (** Floating-point move *) | Pfmov (rd r1: freg) | Pfmovimms (rd: freg) (f: float32) (**r load float32 constant *) @@ -310,9 +332,30 @@ 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. +Definition genv := Genv.t fundef unit. + +(** 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: + - 12 low bits usable as an offset in an addressing mode; + - 21 high bits usable as argument to the ADRP instruction. + + In CompCert's model, we cannot really describe PC-relative addressing, + but we can claim that the address of [symbol + offset] decomposes + as the sum of + - a low part, usable as an offset in an addressing mode; + - a high part, usable as argument to the ADRP instruction. *) + +Parameter symbol_low: genv -> ident -> ptrofs -> val. +Parameter symbol_high: genv -> ident -> ptrofs -> val. + +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 *) + (** 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 @@ -320,22 +363,19 @@ Definition program := AST.program fundef unit. 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. +Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val := + match r with RR0 r => rs (IR r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end. (** Concise notations for accessing and updating the values of registers. *) Notation "a # b" := (a b) (at level 1, only parsing) : asm. Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. -Notation "a ## b" := (ir0w a b) (at level 1, only parsing) : asm. -Notation "a ### b" := (ir0x a b) (at level 1, only parsing) : asm. +Notation "a ## b" := (ir0 W a b) (at level 1, only parsing) : asm. +Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm. Open Scope asm. @@ -369,84 +409,16 @@ 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. -(** 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: - - 12 low bits usable as an offset in an addressing mode; - - 21 high bits usable as argument to the ADRP instruction. - - In CompCert's model, we cannot really describe PC-relative addressing, - but we can claim that the address of [symbol + offset] decomposes - as the sum of - - a low part, usable as an offset in an addressing mode; - - a high part, usable as argument to the ADRP instruction. *) - -Parameter symbol_low: genv -> ident -> ptrofs -> val. -Parameter symbol_high: genv -> ident -> ptrofs -> val. - -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. - -Section RELSEM. - -Variable ge: genv. - -(** Looking up instructions in a code sequence by position. *) - -Fixpoint find_instr (pos: Z) (c: code) {struct c} : option instruction := - match c with - | nil => None - | i :: il => if zeq pos 0 then Some i else find_instr (pos - 1) il - end. - -(** Position corresponding to a label *) - -Definition is_label (lbl: label) (instr: instruction) : bool := - match instr with - | Plabel lbl' => if peq lbl lbl' then true else false - | _ => false - end. - -Lemma is_label_correct: - forall lbl instr, - if is_label lbl instr then instr = Plabel lbl else instr <> Plabel lbl. -Proof. - intros. destruct instr; simpl; try discriminate. destruct (peq lbl lbl0); congruence. -Qed. - -Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z := - match c with - | nil => None - | instr :: c' => - 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). - -Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := - match label_pos lbl 0 (fn_code f) with - | None => Stuck - | Some pos => - match rs#PC with - | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m - | _ => Stuck - end - end. +Record state: Type := State { _rs: regset; _m: mem }. +Definition outcome := option state. +Definition Next rs m: outcome := Some (State rs m). +Definition Stuck: outcome := None. (** Testing a condition *) @@ -516,10 +488,10 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := (** Integer "is zero?" test *) -Definition eval_testzero (sz: isize) (v: val) (m: mem): option bool := +Definition eval_testzero (sz: isize) (v: val): 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) + | W => Val.mxcmpu_bool Ceq v (Vint Int.zero) + | X => Val.mxcmplu_bool Ceq v (Vlong Int64.zero) end. (** Integer "bit is set?" test *) @@ -530,48 +502,19 @@ Definition eval_testbit (sz: isize) (v: val) (n: int): option bool := | 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 := - match a with - | ADimm base n => Val.addl rs#base (Vlong n) - | ADreg base r => Val.addl rs#base rs#r - | ADlsl base r n => Val.addl rs#base (Val.shll rs#r (Vint n)) - | ADsxt base r n => Val.addl rs#base (Val.shll (Val.longofint rs#r) (Vint n)) - | ADuxt base r n => Val.addl rs#base (Val.shll (Val.longofintu rs#r) (Vint n)) - | ADadr base id ofs => Val.addl rs#base (symbol_low ge id ofs) - | ADpostincr base n => Vundef (* not modeled yet *) - end. - -(** Auxiliaries for memory accesses *) - -Definition exec_load (chunk: memory_chunk) (transf: val -> val) - (a: addressing) (r: preg) (rs: regset) (m: mem) := - match Mem.loadv chunk m (eval_addressing a rs) with - | None => Stuck - | Some v => Next (nextinstr (rs#r <- (transf v))) m - end. - -Definition exec_store (chunk: memory_chunk) - (a: addressing) (v: val) - (rs: regset) (m: mem) := - match Mem.storev chunk m (eval_addressing a rs) v with - | None => Stuck - | Some m' => Next (nextinstr rs) m' - end. (** Comparisons *) -Definition compare_int (rs: regset) (v1 v2: val) (m: mem) := +Definition compare_int (rs: regset) (v1 v2: val) := 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) + #CZ <- (Val.mxcmpu Ceq v1 v2) + #CC <- (Val.mxcmpu Cge v1 v2) #CV <- (Val.sub_overflow v1 v2). -Definition compare_long (rs: regset) (v1 v2: val) (m: mem) := +Definition compare_long (rs: regset) (v1 v2: val) := 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)) + #CZ <- (Val.mxcmplu Ceq v1 v2) + #CC <- (Val.mxcmplu Cge v1 v2) #CV <- (Val.subl_overflow v1 v2). (** Semantics of [fcmp] instructions: @@ -672,19 +615,230 @@ Definition float64_of_bits (v: val): val := | _ => 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. +(* Recognition of FP numbers that are supported by the fmov #imm instructions: + "a normalized binary floating point encoding with 1 sign bit, + 4 bits of fraction and a 3-bit exponent" *) +Definition is_immediate_float64 (f: float): bool := + let bits := Float.to_bits f in + let exp := + Int64.sub + (Int64.and (Int64.shr' bits (Int.repr 52)) + (Int64.repr 2047)) (Int64.repr 1023) in + let mant := + Int64.and bits (Int64.repr 4503599627370495) in + andb (Int64.cmp Cge exp (Int64.repr (-3))) + (andb (Int64.cmp Cle exp (Int64.repr 4)) + (Int64.eq + (Int64.and mant + (Int64.repr 4222124650659840)) mant)). + +Definition is_immediate_float32 (f: float32): bool := + let bits := Float32.to_bits f in + let exp := + Int.sub + (Int.and (Int.shr bits (Int.repr 23)) + (Int.repr 255)) (Int.repr 127) in + let mant := + Int.and bits (Int.repr 8388607) in + andb (Int.cmp Cge exp (Int.repr (-3))) + (andb (Int.cmp Cle exp (Int.repr 4)) + (Int.eq + (Int.and mant + (Int.repr 7864320)) mant)). + +(** Translation of the LTL/Linear/Mach view of machine registers + to the AArch64 view. Note that no LTL register maps to [X16], + [X18], nor [X30]. + [X18] is reserved as the platform register and never used by the + code generated by CompCert. + [X30] is used for the return address, and can also be used as temporary. + [X16] can be used as temporary. *) + +Definition dreg_of (r: mreg) : dreg := + match r with + | R0 => X0 | R1 => X1 | R2 => X2 | R3 => X3 + | R4 => X4 | R5 => X5 | R6 => X6 | R7 => X7 + | R8 => X8 | R9 => X9 | R10 => X10 | R11 => X11 + | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15 + | R17 => X17 | R19 => X19 + | R20 => X20 | R21 => X21 | R22 => X22 | R23 => X23 + | R24 => X24 | R25 => X25 | R26 => X26 | R27 => X27 + | R28 => X28 | R29 => X29 + | F0 => D0 | F1 => D1 | F2 => D2 | F3 => D3 + | F4 => D4 | F5 => D5 | F6 => D6 | F7 => D7 + | F8 => D8 | F9 => D9 | F10 => D10 | F11 => D11 + | F12 => D12 | F13 => D13 | F14 => D14 | F15 => D15 + | F16 => D16 | F17 => D17 | F18 => D18 | F19 => D19 + | F20 => D20 | F21 => D21 | F22 => D22 | F23 => D23 + | F24 => D24 | F25 => D25 | F26 => D26 | F27 => D27 + | F28 => D28 | F29 => D29 | F30 => D30 | F31 => D31 + end. + +Definition preg_of (r: mreg) : preg := + dreg_of r. + +(** Undefine all registers except SP and callee-save registers *) + +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => + if preg_eq r SP + || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) + then rs r + else Vundef. + +(** Extract the values of the arguments of an external call. + We exploit the calling conventions from module [Conventions], except that + we use AArch64 registers instead of locations. *) + +Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := + | extcall_arg_reg: forall r, + extcall_arg rs m (R r) (rs (preg_of r)) + | extcall_arg_stack: forall ofs ty bofs v, + bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> + Mem.loadv (chunk_of_type ty) m + (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v -> + extcall_arg rs m (Locations.S Outgoing ofs ty) v. + +Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := + | extcall_arg_one: forall l v, + extcall_arg rs m l v -> + extcall_arg_pair rs m (One l) v + | extcall_arg_twolong: forall hi lo vhi vlo, + extcall_arg rs m hi vhi -> + extcall_arg rs m lo vlo -> + extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo). + +Definition extcall_arguments + (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := + list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args. + +Definition loc_external_result (sg: signature) : rpair preg := + map_rpair preg_of (loc_result sg). + +(** Looking up instructions in a code sequence by position. *) + +Fixpoint find_instr (pos: Z) (c: code) {struct c} : option instruction := + match c with + | nil => None + | i :: il => if zeq pos 0 then Some i else find_instr (pos - 1) il + end. + +(** Position corresponding to a label *) + +Definition is_label (lbl: label) (instr: instruction) : bool := + match instr with + | Plabel lbl' => if peq lbl lbl' then true else false + | _ => false + end. + +Lemma is_label_correct: + forall lbl instr, + if is_label lbl instr then instr = Plabel lbl else instr <> Plabel lbl. +Proof. + intros. destruct instr; simpl; try discriminate. destruct (peq lbl lbl0); congruence. +Qed. + +Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z := + match c with + | nil => None + | instr :: c' => + if is_label lbl instr then Some pos else label_pos lbl (pos + 1) c' + end. + +Definition nextinstr (rs: regset) := + rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one). + +Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := + match label_pos lbl 0 (fn_code f) with + | None => Stuck + | Some pos => + match rs#PC with + | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m + | _ => Stuck + end + end. + +Section RELSEM. + +Variable ge: genv. + +(** Evaluating an addressing mode *) + +Definition eval_addressing (a: addressing) (rs: regset): val := + match a with + | ADimm base n => Val.addl rs#base (Vlong n) + | ADreg base r => Val.addl rs#base rs#r + | ADlsl base r n => Val.addl rs#base (Val.shll rs#r (Vint n)) + | ADsxt base r n => Val.addl rs#base (Val.shll (Val.longofint rs#r) (Vint n)) + | ADuxt base r n => Val.addl rs#base (Val.shll (Val.longofintu rs#r) (Vint n)) + | ADadr base id ofs => Val.addl rs#base (symbol_low ge id ofs) + | ADpostincr base n => Vundef + end. + +Definition is_pair_addressing_mode_correct (a: addressing): bool := + match a with + | ADimm _ _ => true + | _ => false + end. + +Definition get_offset_addr (a: addressing) (ofs: Z) : addressing := + match a with + | ADimm base n => (ADimm base (Int64.add n (Int64.repr ofs))) + | _ => a + end. + +(** Auxiliaries for memory accesses *) + +Definition exec_load (chunk: memory_chunk) (transf: val -> val) + (a: addressing) (r: preg) (rs: regset) (m: mem) := + match Mem.loadv chunk m (eval_addressing a rs) with + | None => Stuck + | Some v => Next (nextinstr (rs#r <- (transf v))) m + end. + +Definition exec_load_double (chk1 chk2: memory_chunk) (transf: val -> val) + (a: addressing) (rd1 rd2: preg) (rs: regset) (m: mem) := + if is_pair_addressing_mode_correct a then + let addr := (eval_addressing a rs) in + let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in + let addr' := (eval_addressing (get_offset_addr a ofs) rs) in + match Mem.loadv chk1 m addr with + | None => Stuck + | Some v1 => + match Mem.loadv chk2 m addr' with + | None => Stuck + | Some v2 => + Next (nextinstr ((rs#rd1 <- (transf v1))#rd2 <- (transf v2))) m + end + end + else Stuck. + +Definition exec_store (chunk: memory_chunk) + (a: addressing) (v: val) + (rs: regset) (m: mem) := + match Mem.storev chunk m (eval_addressing a rs) v with + | None => Stuck + | Some m' => Next (nextinstr rs) m' + end. + +Definition exec_store_double (chk1 chk2: memory_chunk) + (a: addressing) (v1 v2: val) + (rs: regset) (m: mem) := + if is_pair_addressing_mode_correct a then + let addr := (eval_addressing a rs) in + let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4 | _ => 8 end in + let addr' := (eval_addressing (get_offset_addr a ofs) rs) in + match Mem.storev chk1 m addr v1 with + | None => Stuck + | Some m' => match Mem.storev chk2 m' addr' v2 with + | None => Stuck + | Some m'' => Next (nextinstr rs) m'' + end + end + else Stuck. + Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := match i with (** Branches *) @@ -707,13 +861,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 @@ -781,13 +935,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 @@ -805,9 +959,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 @@ -853,22 +1007,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 @@ -895,9 +1049,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 @@ -969,10 +1123,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out (** Floating-point move *) | Pfmov rd r1 => Next (nextinstr (rs#rd <- (rs#r1))) m - | Pfmovimms rd f => - Next (nextinstr (rs#X16 <- Vundef #rd <- (Vsingle f))) m + | Pfmovimms rd f => + if is_immediate_float32 f then + Next (nextinstr (rs#rd <- (Vsingle f))) m + else + Next (nextinstr ((rs#rd <- (Vsingle f))#X16 <- Vundef)) m | Pfmovimmd rd f => - Next (nextinstr (rs#X16 <- Vundef #rd <- (Vfloat f))) m + if is_immediate_float64 f then + Next (nextinstr (rs#rd <- (Vfloat f))) m + else + Next (nextinstr ((rs#rd <- (Vfloat f))#X16 <- Vundef)) m | Pfmovi S rd r1 => Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m | Pfmovi D rd r1 => @@ -1102,10 +1262,27 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | _ => Stuck end | Pbuiltin ef args res => Stuck (**r treated specially below *) + (** loads and stores pairs int/int64 *) + | Pldpw rd1 rd2 chk1 chk2 a => + exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m + | Pldpx rd1 rd2 chk1 chk2 a => + exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m + | Pstpw rs1 rs2 chk1 chk2 a => + exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m + | Pstpx rs1 rs2 chk1 chk2 a => + exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m + (** loads and stores pairs floating-point *) + | Pldps rd1 rd2 chk1 chk2 a => + exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m + | Pldpd rd1 rd2 chk1 chk2 a => + exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m + | Pstps rs1 rs2 chk1 chk2 a => + exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m + | Pstpd rs1 rs2 chk1 chk2 a => + exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m + | Pnop => Next (nextinstr rs) m (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) - | Pldp _ _ _ - | Pstp _ _ _ | Pcls _ _ _ | Pclz _ _ _ | Prev _ _ _ @@ -1118,86 +1295,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfnmsub _ _ _ _ _ | Pfmax _ _ _ _ | Pfmin _ _ _ _ - | Pnop | Pcfi_adjust _ | Pcfi_rel_offset _ => 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 -> @@ -1212,7 +1317,7 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge vargs m t vres m' -> rs' = nextinstr (set_res res vres - (undef_regs (IR X16 :: IR X30 :: map preg_of (destroyed_by_builtin ef)) rs)) -> + (undef_regs (DR X16 :: DR X30 :: map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', @@ -1308,11 +1413,11 @@ Qed. Definition data_preg (r: preg) : bool := match r with - | IR X16 => false - | IR X30 => false - | IR _ => true - | FR _ => true + | DR (IR X16) => false + | DR (IR X30) => false + | DR (IR _) => true + | DR (FR _) => true | CR _ => false - | SP => true + (* | SP => true; subsumed by IR (iregsp) *) | PC => false end. |