diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-23 01:53:05 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-23 01:53:05 +0200 |
commit | 37ad0670e1dc02c47b4987c16602aadb462c44c2 (patch) | |
tree | 35f538126dc796187c869c9f3e2fd8993ec9e196 /aarch64/Asm.v | |
parent | 2ff831f62b8674e41dac82b4738199eaa4fb4011 (diff) | |
download | compcert-kvx-37ad0670e1dc02c47b4987c16602aadb462c44c2.tar.gz compcert-kvx-37ad0670e1dc02c47b4987c16602aadb462c44c2.zip |
aarch64 compiles again (but ccomp generates incorrect assembly)
Diffstat (limited to 'aarch64/Asm.v')
-rw-r--r-- | aarch64/Asm.v | 539 |
1 files changed, 530 insertions, 9 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 4de1a9d0..22ab0222 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -12,15 +12,10 @@ (** Abstract syntax and semantics for AArch64 assembly language - -W.r.t Asmblock, this is a "flat" syntax and semantics of "Aarch64" assembly: +W.r.t Asmblock, this is a "flat" syntax and semantics of "aarch64" assembly: - without the basic block structure - without the hierarchy of instructions. - -TODO: with respect to original file, remove parts of the syntax/semantics -that have been already defined in Asmblock. - *) Require Import Coqlib Zbits Maps. @@ -28,10 +23,152 @@ Require Import AST Integers Floats. Require Import Values Memory Events Globalenvs Smallstep. Require Import Locations Conventions. Require Stacklayout. -Require Import OptionMonad Asmblock. +Require Import OptionMonad. (** * Abstract syntax *) +(** Integer registers, floating-point registers. *) + +(** In assembly files, [Xn] denotes the full 64-bit register + and [Wn] the low 32 bits of [Xn]. *) + +Inductive ireg: Type := + | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 + | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 + | X16 | X17 | X18 | X19 | X20 | X21 | X22 | X23 + | X24 | X25 | X26 | X27 | X28 | X29 | X30. + +Inductive ireg0: Type := + | RR0 (r: ireg) | XZR. + +Inductive iregsp: Type := + | RR1 (r: ireg) | XSP. + +Coercion RR0: ireg >-> ireg0. +Coercion RR1: ireg >-> iregsp. + +Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Lemma iregsp_eq: forall (x y: iregsp), {x=y} + {x<>y}. +Proof. decide equality; apply ireg_eq. Defined. + +(** In assembly files, [Dn] denotes the low 64-bit of a vector register, + and [Sn] the low 32 bits. *) + +Inductive freg: Type := + | D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 + | D8 | D9 | D10 | D11 | D12 | D13 | D14 | D15 + | D16 | D17 | D18 | D19 | D20 | D21 | D22 | D23 + | D24 | D25 | D26 | D27 | D28 | D29 | D30 | D31. + +Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +(** Bits in the condition register. *) + +Inductive crbit: Type := + | CN: crbit (**r negative *) + | CZ: crbit (**r zero *) + | CC: crbit (**r carry *) + | CV: crbit. (**r overflow *) + +Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Inductive dreg : Type := + | IR': iregsp -> dreg (**r 64- or 32-bit integer registers *) + | FR': freg -> dreg. (**r double- or single-precision float registers *) + +(** We model the following registers of the ARM architecture. *) + +Inductive preg: Type := + | DR: dreg -> preg (** see dreg **) + | CR: crbit -> preg (**r bits in the condition register *) + | PC: preg. (**r program counter *) + +(* XXX: ireg no longer coerces to preg *) +Coercion IR': iregsp >-> dreg. +Coercion FR': freg >-> dreg. +Coercion DR: dreg >-> preg. +Definition SP:preg := XSP. +Coercion CR: crbit >-> preg. + +Lemma dreg_eq: forall (x y: dreg), {x=y} + {x<>y}. +Proof. decide equality. apply iregsp_eq. apply freg_eq. Defined. + +Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. +Proof. decide equality. apply dreg_eq. apply crbit_eq. Defined. + +Module PregEq. + Definition t := preg. + Definition eq := preg_eq. +End PregEq. + +Module Pregmap := EMap(PregEq). + +Definition preg_of_iregsp (r: iregsp) : preg := + match r with RR1 r => IR' r | XSP => SP end. + +(** Conventional name for return address ([RA]) *) + +Notation "'RA'" := X30 (only parsing) : asm. + +(** The instruction set. Most instructions correspond exactly to + actual AArch64 instructions. See the ARM reference manuals for more + details. Some instructions, described below, are + pseudo-instructions: they expand to canned instruction sequences + during the printing of the assembly code. *) + +Definition label := positive. + +Inductive isize: Type := + | W (**r 32-bit integer operation *) + | X. (**r 64-bit integer operation *) + +Inductive fsize: Type := + | S (**r 32-bit, single-precision FP operation *) + | D. (**r 64-bit, double-precision FP operation *) + +Inductive testcond : Type := + | TCeq: testcond (**r equal *) + | TCne: testcond (**r not equal *) + | TChs: testcond (**r unsigned higher or same *) + | TClo: testcond (**r unsigned lower *) + | TCmi: testcond (**r negative *) + | TCpl: testcond (**r positive *) + | TChi: testcond (**r unsigned higher *) + | TCls: testcond (**r unsigned lower or same *) + | TCge: testcond (**r signed greater or equal *) + | TClt: testcond (**r signed less than *) + | TCgt: testcond (**r signed greater *) + | TCle: testcond. (**r signed less than or equal *) + +Inductive addressing: Type := + | ADimm (base: iregsp) (n: int64) (**r base plus immediate offset *) + | ADreg (base: iregsp) (r: ireg) (**r base plus reg *) + | ADlsl (base: iregsp) (r: ireg) (n: int) (**r base plus reg LSL n *) + | ADsxt (base: iregsp) (r: ireg) (n: int) (**r base plus SIGN-EXT(reg) LSL n *) + | ADuxt (base: iregsp) (r: ireg) (n: int) (**r base plus ZERO-EXT(reg) LSL n *) + | ADadr (base: iregsp) (id: ident) (ofs: ptrofs) (**r base plus low address of [id + ofs] *) + | ADpostincr (base: iregsp) (n: int64). (**r base plus offset; base is updated after *) + +Inductive shift_op: Type := + | SOnone + | SOlsl (n: int) + | SOlsr (n: int) + | SOasr (n: int) + | SOror (n: int). + +Inductive extend_op: Type := + | EOsxtb (n: int) + | EOsxth (n: int) + | EOsxtw (n: int) + | EOuxtb (n: int) + | EOuxth (n: int) + | EOuxtw (n: int) + | EOuxtx (n: int). + Inductive instruction: Type := (** Branches *) | Pb (lbl: label) (**r branch *) @@ -209,9 +346,389 @@ Axiom symbol_high_low: (** * Operational semantics *) -Section RELSEM. -Variable ge: genv. +(** The semantics operates over a single mapping from registers + (type [preg]) to values. We maintain (but do not enforce) + the convention that integer registers are mapped to values of + type [Tint], float registers to values of type [Tfloat], + and condition bits to either [Vzero] or [Vone]. *) + +Definition regset := Pregmap.t val. + +(** The value of an [ireg0] is either the value of the integer register, + or 0. *) + +Definition ir0 (is:isize) (rs: regset) (r: ireg0) : val := + match r with RR0 r => rs (IR' r) | XZR => if is (* is W *) then Vint Int.zero else Vlong Int64.zero end. + +(** Concise notations for accessing and updating the values of registers. *) + +Notation "a # b" := (a b) (at level 1, only parsing) : asm. +Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. +Notation "a ## b" := (ir0 W a b) (at level 1, only parsing) : asm. +Notation "a ### b" := (ir0 X a b) (at level 1, only parsing) : asm. + +Open Scope asm. + +(** Undefining some registers *) + +Fixpoint undef_regs (l: list preg) (rs: regset) : regset := + match l with + | nil => rs + | r :: l' => undef_regs l' (rs#r <- Vundef) + end. + +(** Undefining the condition codes *) + +Definition undef_flags (rs: regset) : regset := + fun r => match r with CR _ => Vundef | _ => rs r end. + +(** Assigning a register pair *) + +Definition set_pair (p: rpair preg) (v: val) (rs: regset) : regset := + match p with + | One r => rs#r <- v + | Twolong rhi rlo => rs#rhi <- (Val.hiword v) #rlo <- (Val.loword v) + end. + +(** Assigning the result of a builtin *) + +Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := + match res with + | BR r => rs#r <- v + | BR_none => rs + | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs) + end. + +(** The semantics is purely small-step and defined as a function + from the current state (a register set + a memory state) + to either [Next rs' m'] where [rs'] and [m'] are the updated register + set and memory state after execution of the instruction at [rs#PC], + or [Stuck] if the processor is stuck. *) + +Record state: Type := State { _rs: regset; _m: mem }. +Definition outcome := option state. +Definition Next rs m: outcome := Some (State rs m). +Definition Stuck: outcome := None. + + +(* a few lemma on comparisons of unsigned (e.g. pointers) + +TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!) +*) + +Definition Val_cmpu_bool cmp v1 v2: option bool := + Val.cmpu_bool (fun _ _ => true) cmp v1 v2. + +Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: + (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b + -> (Val_cmpu_bool cmp v1 v2) = Some b. +Proof. + intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2). + +Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val): + Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2) + (Val_cmpu cmp v1 v2). +Proof. + unfold Val.cmpu, Val_cmpu. + remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. + destruct ob; simpl. + - erewrite Val_cmpu_bool_correct; eauto. + econstructor. + - econstructor. +Qed. + +Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val) + := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2). + +Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: + (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b + -> (Val_cmplu_bool cmp v1 v2) = Some b. +Proof. + intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto). +Qed. + +Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2). + +Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val): + Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2)) + (Val_cmplu cmp v1 v2). +Proof. + unfold Val.cmplu, Val_cmplu. + remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. + destruct ob as [b|]; simpl. + - erewrite Val_cmplu_bool_correct; eauto. + simpl. econstructor. + - econstructor. +Qed. + +(** Testing a condition *) + +Definition eval_testcond (c: testcond) (rs: regset) : option bool := + match c with + | TCeq => (**r equal *) + match rs#CZ with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + | TCne => (**r not equal *) + match rs#CZ with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TClo => (**r unsigned less than *) + match rs#CC with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TCls => (**r unsigned less or equal *) + match rs#CC, rs#CZ with + | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one) + | _, _ => None + end + | TChs => (**r unsigned greater or equal *) + match rs#CC with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + | TChi => (**r unsigned greater *) + match rs#CC, rs#CZ with + | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero) + | _, _ => None + end + | TClt => (**r signed less than *) + match rs#CV, rs#CN with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one) + | _, _ => None + end + | TCle => (**r signed less or equal *) + match rs#CV, rs#CN, rs#CZ with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one) + | _, _, _ => None + end + | TCge => (**r signed greater or equal *) + match rs#CV, rs#CN with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero) + | _, _ => None + end + | TCgt => (**r signed greater *) + match rs#CV, rs#CN, rs#CZ with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero) + | _, _, _ => None + end + | TCpl => (**r positive *) + match rs#CN with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TCmi => (**r negative *) + match rs#CN with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + end. + +(** Integer "is zero?" test *) + +Definition eval_testzero (sz: isize) (v: val): option bool := + match sz with + | W => Val_cmpu_bool Ceq v (Vint Int.zero) + | X => Val_cmplu_bool Ceq v (Vlong Int64.zero) + end. + +(** Integer "bit is set?" test *) + +Definition eval_testbit (sz: isize) (v: val) (n: int): option bool := + match sz with + | W => Val.cmp_bool Cne (Val.and v (Vint (Int.shl Int.one n))) (Vint Int.zero) + | X => Val.cmpl_bool Cne (Val.andl v (Vlong (Int64.shl' Int64.one n))) (Vlong Int64.zero) + end. + + +(** Comparisons *) + +Definition compare_int (rs: regset) (v1 v2: val) := + rs#CN <- (Val.negative (Val.sub v1 v2)) + #CZ <- (Val_cmpu Ceq v1 v2) + #CC <- (Val_cmpu Cge v1 v2) + #CV <- (Val.sub_overflow v1 v2). + +Definition compare_long (rs: regset) (v1 v2: val) := + rs#CN <- (Val.negativel (Val.subl v1 v2)) + #CZ <- (Val_cmplu Ceq v1 v2) + #CC <- (Val_cmplu Cge v1 v2) + #CV <- (Val.subl_overflow v1 v2). + +(** Semantics of [fcmp] instructions: +<< +== N=0 Z=1 C=1 V=0 +< N=1 Z=0 C=0 V=0 +> N=0 Z=0 C=1 V=0 +unord N=0 Z=0 C=1 V=1 +>> +*) + +Definition compare_float (rs: regset) (v1 v2: val) := + match v1, v2 with + | Vfloat f1, Vfloat f2 => + rs#CN <- (Val.of_bool (Float.cmp Clt f1 f2)) + #CZ <- (Val.of_bool (Float.cmp Ceq f1 f2)) + #CC <- (Val.of_bool (negb (Float.cmp Clt f1 f2))) + #CV <- (Val.of_bool (negb (Float.ordered f1 f2))) + | _, _ => + rs#CN <- Vundef + #CZ <- Vundef + #CC <- Vundef + #CV <- Vundef + end. + +Definition compare_single (rs: regset) (v1 v2: val) := + match v1, v2 with + | Vsingle f1, Vsingle f2 => + rs#CN <- (Val.of_bool (Float32.cmp Clt f1 f2)) + #CZ <- (Val.of_bool (Float32.cmp Ceq f1 f2)) + #CC <- (Val.of_bool (negb (Float32.cmp Clt f1 f2))) + #CV <- (Val.of_bool (negb (Float32.ordered f1 f2))) + | _, _ => + rs#CN <- Vundef + #CZ <- Vundef + #CC <- Vundef + #CV <- Vundef + end. + +(** Insertion of bits into an integer *) + +Definition insert_in_int (x: val) (y: Z) (pos: Z) (len: Z) : val := + match x with + | Vint n => Vint (Int.repr (Zinsert (Int.unsigned n) y pos len)) + | _ => Vundef + end. + +Definition insert_in_long (x: val) (y: Z) (pos: Z) (len: Z) : val := + match x with + | Vlong n => Vlong (Int64.repr (Zinsert (Int64.unsigned n) y pos len)) + | _ => Vundef + end. + +(** Evaluation of shifted operands *) + +Definition eval_shift_op_int (v: val) (s: shift_op): val := + match s with + | SOnone => v + | SOlsl n => Val.shl v (Vint n) + | SOlsr n => Val.shru v (Vint n) + | SOasr n => Val.shr v (Vint n) + | SOror n => Val.ror v (Vint n) + end. + +Definition eval_shift_op_long (v: val) (s: shift_op): val := + match s with + | SOnone => v + | SOlsl n => Val.shll v (Vint n) + | SOlsr n => Val.shrlu v (Vint n) + | SOasr n => Val.shrl v (Vint n) + | SOror n => Val.rorl v (Vint n) + end. + +(** Evaluation of sign- or zero- extended operands *) + +Definition eval_extend (v: val) (x: extend_op): val := + match x with + | EOsxtb n => Val.shll (Val.longofint (Val.sign_ext 8 v)) (Vint n) + | EOsxth n => Val.shll (Val.longofint (Val.sign_ext 16 v)) (Vint n) + | EOsxtw n => Val.shll (Val.longofint v) (Vint n) + | EOuxtb n => Val.shll (Val.longofintu (Val.zero_ext 8 v)) (Vint n) + | EOuxth n => Val.shll (Val.longofintu (Val.zero_ext 16 v)) (Vint n) + | EOuxtw n => Val.shll (Val.longofintu v) (Vint n) + | EOuxtx n => Val.shll v (Vint n) + end. + +(** Bit-level conversion from integers to FP numbers *) + +Definition float32_of_bits (v: val): val := + match v with + | Vint n => Vsingle (Float32.of_bits n) + | _ => Vundef + end. + +Definition float64_of_bits (v: val): val := + match v with + | Vlong n => Vfloat (Float.of_bits n) + | _ => Vundef + end. + + +(** Translation of the LTL/Linear/Mach view of machine registers + to the AArch64 view. Note that no LTL register maps to [X16], + [X18], nor [X30]. + [X18] is reserved as the platform register and never used by the + code generated by CompCert. + [X30] is used for the return address, and can also be used as temporary. + [X16] can be used as temporary. *) + +Definition dreg_of (r: mreg) : dreg := + match r with + | R0 => X0 | R1 => X1 | R2 => X2 | R3 => X3 + | R4 => X4 | R5 => X5 | R6 => X6 | R7 => X7 + | R8 => X8 | R9 => X9 | R10 => X10 | R11 => X11 + | R12 => X12 | R13 => X13 | R14 => X14 | R15 => X15 + | R17 => X17 | R19 => X19 + | R20 => X20 | R21 => X21 | R22 => X22 | R23 => X23 + | R24 => X24 | R25 => X25 | R26 => X26 | R27 => X27 + | R28 => X28 | R29 => X29 + | F0 => D0 | F1 => D1 | F2 => D2 | F3 => D3 + | F4 => D4 | F5 => D5 | F6 => D6 | F7 => D7 + | F8 => D8 | F9 => D9 | F10 => D10 | F11 => D11 + | F12 => D12 | F13 => D13 | F14 => D14 | F15 => D15 + | F16 => D16 | F17 => D17 | F18 => D18 | F19 => D19 + | F20 => D20 | F21 => D21 | F22 => D22 | F23 => D23 + | F24 => D24 | F25 => D25 | F26 => D26 | F27 => D27 + | F28 => D28 | F29 => D29 | F30 => D30 | F31 => D31 + end. + +Definition preg_of (r: mreg) : preg := + dreg_of r. + +(** Undefine all registers except SP and callee-save registers *) + +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => + if preg_eq r SP + || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) + then rs r + else Vundef. + +(** Extract the values of the arguments of an external call. + We exploit the calling conventions from module [Conventions], except that + we use AArch64 registers instead of locations. *) + +Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := + | extcall_arg_reg: forall r, + extcall_arg rs m (R r) (rs (preg_of r)) + | extcall_arg_stack: forall ofs ty bofs v, + bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> + Mem.loadv (chunk_of_type ty) m + (Val.offset_ptr rs#SP (Ptrofs.repr bofs)) = Some v -> + extcall_arg rs m (Locations.S Outgoing ofs ty) v. + +Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := + | extcall_arg_one: forall l v, + extcall_arg rs m l v -> + extcall_arg_pair rs m (One l) v + | extcall_arg_twolong: forall hi lo vhi vlo, + extcall_arg rs m hi vhi -> + extcall_arg rs m lo vlo -> + extcall_arg_pair rs m (Twolong hi lo) (Val.longofwords vhi vlo). + +Definition extcall_arguments + (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := + list_forall2 (extcall_arg_pair rs m) (loc_arguments sg) args. + +Definition loc_external_result (sg: signature) : rpair preg := + map_rpair preg_of (loc_result sg). (** Looking up instructions in a code sequence by position. *) @@ -256,6 +773,10 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := end end. +Section RELSEM. + +Variable ge: genv. + (** Evaluating an addressing mode *) Definition eval_addressing (a: addressing) (rs: regset): val := |