diff options
| -rw-r--r-- | aarch64/Asm.v | 539 | ||||
| -rw-r--r-- | aarch64/Asmblock.v | 533 | ||||
| -rw-r--r-- | aarch64/Asmblockgen.v | 80 | ||||
| -rw-r--r-- | aarch64/Asmexpand.ml | 102 | ||||
| -rw-r--r-- | aarch64/Asmgen.v | 10 | ||||
| -rw-r--r-- | aarch64/Asmgenproof.v | 17 | ||||
| -rw-r--r-- | aarch64/OrigAsmgen.ml | 282 | ||||
| -rw-r--r-- | aarch64/TargetPrinter.ml | 8 | ||||
| -rw-r--r-- | aarch64/extractionMachdep.v | 2 | ||||
| -rw-r--r-- | extraction/extraction.v | 4 |
10 files changed, 964 insertions, 613 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 := diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 67ad2aa5..96162f9e 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -35,151 +35,11 @@ Require Import AST Integers Floats. Require Import Values Memory Events Globalenvs Smallstep. Require Import Locations Conventions. Require Stacklayout. -Require Import OptionMonad. +Require Import OptionMonad Asm. -(** * 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. *) +Local Open Scope option_monad_scope. -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). +(** * Abstract syntax *) (* First task: splitting the big [instruction] type below into CFI and basic instructions. Actually a finer splitting in order to regroup "similar" instructions could be much better for automation of the scheduler proof! @@ -688,272 +548,19 @@ Inductive instruction: Type := (** * 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 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. - (** See "Parameters" of the same names in Asm.v *) Record aarch64_linker: Type := { symbol_low: ident -> ptrofs -> val; symbol_high: ident -> ptrofs -> val }. +Definition genv := Genv.t fundef unit. + Section RELSEM. Variable lk: aarch64_linker. Variable ge: genv. - -(** 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. -Local Open Scope option_monad_scope. - -(* 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. - - (** Evaluating an addressing mode *) Definition eval_addressing (a: addressing) (rs: regset): val := @@ -980,66 +587,6 @@ Definition exec_store (chunk: memory_chunk) SOME m' <- Mem.storev chunk m (eval_addressing a rs) v IN Next rs m'. -(** 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 loads *) @@ -1892,76 +1439,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out 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). - - (** execution of the body of a bblock *) Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := match body with diff --git a/aarch64/Asmblockgen.v b/aarch64/Asmblockgen.v index 83f2b96b..66db0f5f 100644 --- a/aarch64/Asmblockgen.v +++ b/aarch64/Asmblockgen.v @@ -3,7 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Sylvain Boulmé Grenoble-INP, VERIMAG *) -(* Justus Fasse UGA, VERIMAG *) +(* Léo Gourdin UGA, VERIMAG *) (* Xavier Leroy INRIA Paris-Rocquencourt *) (* David Monniaux CNRS, VERIMAG *) (* Cyril Six Kalray *) @@ -19,14 +19,82 @@ Require Import Recdef Coqlib Zwf Zbits. Require Import Errors AST Integers Floats Op. -Require Import Locations Machblock Asmblock. +Require Import Locations Machblock Asm Asmblock. -(* STUB *) -Definition transf_function (f: Machblock.function) : res Asmblock.function := - Error (msg "Asmblockgen not yet implmented"). +Local Open Scope string_scope. +Local Open Scope list_scope. +Local Open Scope error_monad_scope. + +Program Definition single_basic (bi: basic): bblock := + {| header := nil; body:= bi::nil; exit := None |}. + +(* insert [bi] at the head of [k] *) +Program Definition insert_basic (bi: basic) (k:bblocks): bblocks := + match k with + | bb::k' => + match bb.(header) with + | nil => {| header := nil; body := bi :: (body bb); exit := exit bb |}::k' + | _ => (single_basic bi)::k + end + | _ => (single_basic bi)::k + end. + +Notation "bi ::b k" := (insert_basic bi k) (at level 49, right associativity). + +(* insert [ctl] at the head of [k] *) +Program Definition insert_ctl (ctl: control) (k:bblocks): bblocks := + {| header := nil; body := nil; exit := Some ctl |}::k. + +Notation "ctl ::c k" := (insert_ctl ctl k) (at level 49, right associativity). + + +(** Alignment check for symbols *) + +Parameter symbol_is_aligned : ident -> Z -> bool. +(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *) + +(***************************************************************************************) +(* STUB inspired from kvx/Asmblockgen.v and the reference aarch64/Asmgen.v (see below) *) + +Definition indexed_memory_access (insn: addressing -> basic) + (sz: Z) (base: iregsp) (ofs: ptrofs) (k: bblocks) : bblocks := + let ofs := Ptrofs.to_int64 ofs in + insn (ADimm base ofs) ::b k. (* STUB: change me ! See Asmgen below *) + + +Definition loadptr (base: iregsp) (ofs: ptrofs) (dst: ireg) (k: bblocks): bblocks := + indexed_memory_access (PLoad Pldrx dst) 8 base ofs k. + +Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: bblocks): bblocks := + indexed_memory_access (PStore Pstrx src) 8 base ofs k. + +(** Function epilogue *) + +Definition make_epilogue (f: Machblock.function) (k: bblocks) : bblocks := + (* 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) ::b k). + + +Program Definition transl_blocks (f: Machblock.function) (lmb: Machblock.code) (ep: bool): res bblocks := + OK (make_epilogue f ((Pret X0)::c nil)). (* STUB: TODO CHANGE ME ! *) + +(* Currently, we assume to be after the PseudoAsmblockproof.transf_program pass... *) +Program Definition make_prologue (f: Machblock.function) (k:bblocks) := + Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b + storeptr RA XSP f.(fn_retaddr_ofs) k. + +Definition transl_function (f: Machblock.function) : res Asmblock.function := + do lb <- transl_blocks f f.(Machblock.fn_code) true; + OK (mkfunction f.(Machblock.fn_sig) + (make_prologue f lb)). Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := - transf_partial_fundef transf_function f. + transf_partial_fundef transl_function f. (* TODO: do we need to check the size here ? (issue only in proofs) *) Definition transf_program (p: Machblock.program) : res Asmblock.program := transform_partial_program transf_fundef p. diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index b0787d0a..8e3c169a 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -34,13 +34,13 @@ let _m1 = Z.of_sint (-1) (* Emit instruction sequences that set or offset a register by a constant. *) let expand_loadimm32 (dst: ireg) n = - List.iter emit (Asmgen.loadimm32 dst n []) + List.iter emit (OrigAsmgen.loadimm32 dst n []) let expand_addimm64 (dst: iregsp) (src: iregsp) n = - List.iter emit (Asmgen.addimm64 dst src n []) + List.iter emit (OrigAsmgen.addimm64 dst src n []) let expand_storeptr (src: ireg) (base: iregsp) ofs = - List.iter emit (Asmgen.storeptr src base ofs []) + List.iter emit (OrigAsmgen.storeptr src base ofs []) (* Handling of varargs *) @@ -132,9 +132,9 @@ let expand_builtin_va_start r = let expand_annot_val kind txt targ args res = emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none)); match args, res with - | [BA(IR src)], BR(IR dst) -> - if dst <> src then emit (Pmov (RR1 dst, RR1 src)) - | [BA(FR src)], BR(FR dst) -> + | [BA(DR(IR' src))], BR(DR(IR' dst)) -> + if dst <> src then emit (Pmov (dst, src)) + | [BA(DR(FR' src))], BR(DR(FR' dst)) -> if dst <> src then emit (Pfmov (dst, src)) | _, _ -> raise (Error "ill-formed __builtin_annot_val") @@ -152,8 +152,8 @@ let offset_in_range ofs = let memcpy_small_arg sz arg tmp = match arg with - | BA (IR r) -> - (RR1 r, _0) + | BA (DR(IR' r)) -> + (r, _0) | BA_addrstack ofs -> if offset_in_range ofs && offset_in_range (Ptrofs.add ofs (Ptrofs.repr (Z.of_uint sz))) @@ -164,7 +164,7 @@ let memcpy_small_arg sz arg tmp = let expand_builtin_memcpy_small sz al src dst = let (tsrc, tdst) = - if dst <> BA (IR X17) then (X17, X29) else (X29, X17) in + if dst <> BA (DR(IR'(RR1 X17))) then (X17, X29) else (X29, X17) in let (rsrc, osrc) = memcpy_small_arg sz src tsrc in let (rdst, odst) = memcpy_small_arg sz dst tdst in let rec copy osrc odst sz = @@ -197,7 +197,7 @@ let expand_builtin_memcpy_small sz al src dst = let memcpy_big_arg arg tmp = match arg with - | BA (IR r) -> emit (Pmov(RR1 tmp, RR1 r)) + | BA (DR(IR' r)) -> emit (Pmov(RR1 tmp, r)) | BA_addrstack ofs -> expand_addimm64 (RR1 tmp) XSP ofs | _ -> assert false @@ -241,29 +241,29 @@ let expand_builtin_memcpy sz al args = let expand_builtin_vload_common chunk base ofs res = let addr = ADimm(base, ofs) in match chunk, res with - | Mint8unsigned, BR(IR res) -> + | Mint8unsigned, BR(DR(IR'(RR1 res))) -> emit (Pldrb(W, res, addr)) - | Mint8signed, BR(IR res) -> + | Mint8signed, BR(DR(IR'(RR1 res))) -> emit (Pldrsb(W, res, addr)) - | Mint16unsigned, BR(IR res) -> + | Mint16unsigned, BR(DR(IR'(RR1 res))) -> emit (Pldrh(W, res, addr)) - | Mint16signed, BR(IR res) -> + | Mint16signed, BR(DR(IR'(RR1 res))) -> emit (Pldrsh(W, res, addr)) - | Mint32, BR(IR res) -> + | Mint32, BR(DR(IR'(RR1 res))) -> emit (Pldrw(res, addr)) - | Mint64, BR(IR res) -> + | Mint64, BR(DR(IR'(RR1 res))) -> emit (Pldrx(res, addr)) - | Mfloat32, BR(FR res) -> + | Mfloat32, BR(DR(FR' res)) -> emit (Pldrs(res, addr)) - | Mfloat64, BR(FR res) -> + | Mfloat64, BR(DR(FR' res)) -> emit (Pldrd(res, addr)) | _ -> assert false let expand_builtin_vload chunk args res = match args with - | [BA(IR addr)] -> - expand_builtin_vload_common chunk (RR1 addr) _0 res + | [BA(DR(IR' addr))] -> + expand_builtin_vload_common chunk addr _0 res | [BA_addrstack ofs] -> if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then expand_builtin_vload_common chunk XSP ofs res @@ -271,11 +271,11 @@ let expand_builtin_vload chunk args res = expand_addimm64 (RR1 X16) XSP ofs; (* X16 <- SP + ofs *) expand_builtin_vload_common chunk (RR1 X16) _0 res end - | [BA_addptr(BA(IR addr), BA_long ofs)] -> + | [BA_addptr(BA(DR(IR' addr)), BA_long ofs)] -> if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then - expand_builtin_vload_common chunk (RR1 addr) ofs res + expand_builtin_vload_common chunk addr ofs res else begin - expand_addimm64 (RR1 X16) (RR1 addr) ofs; (* X16 <- addr + ofs *) + expand_addimm64 (RR1 X16) addr ofs; (* X16 <- addr + ofs *) expand_builtin_vload_common chunk (RR1 X16) _0 res end | _ -> @@ -284,25 +284,25 @@ let expand_builtin_vload chunk args res = let expand_builtin_vstore_common chunk base ofs src = let addr = ADimm(base, ofs) in match chunk, src with - | (Mint8signed | Mint8unsigned), BA(IR src) -> + | (Mint8signed | Mint8unsigned), BA(DR(IR'(RR1 src))) -> emit (Pstrb(src, addr)) - | (Mint16signed | Mint16unsigned), BA(IR src) -> + | (Mint16signed | Mint16unsigned), BA(DR(IR'(RR1 src))) -> emit (Pstrh(src, addr)) - | Mint32, BA(IR src) -> + | Mint32, BA(DR(IR'(RR1 src))) -> emit (Pstrw(src, addr)) - | Mint64, BA(IR src) -> + | Mint64, BA(DR(IR'(RR1 src))) -> emit (Pstrx(src, addr)) - | Mfloat32, BA(FR src) -> + | Mfloat32, BA(DR(FR' src)) -> emit (Pstrs(src, addr)) - | Mfloat64, BA(FR src) -> + | Mfloat64, BA(DR(FR' src)) -> emit (Pstrd(src, addr)) | _ -> assert false let expand_builtin_vstore chunk args = match args with - | [BA(IR addr); src] -> - expand_builtin_vstore_common chunk (RR1 addr) _0 src + | [BA(DR(IR' addr)); src] -> + expand_builtin_vstore_common chunk addr _0 src | [BA_addrstack ofs; src] -> if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then expand_builtin_vstore_common chunk XSP ofs src @@ -310,11 +310,11 @@ let expand_builtin_vstore chunk args = expand_addimm64 (RR1 X16) XSP ofs; (* X16 <- SP + ofs *) expand_builtin_vstore_common chunk (RR1 X16) _0 src end - | [BA_addptr(BA(IR addr), BA_long ofs); src] -> + | [BA_addptr(BA(DR(IR' addr)), BA_long ofs); src] -> if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then - expand_builtin_vstore_common chunk (RR1 addr) ofs src + expand_builtin_vstore_common chunk addr ofs src else begin - expand_addimm64 (RR1 X16) (RR1 addr) ofs; (* X16 <- addr + ofs *) + expand_addimm64 (RR1 X16) addr ofs; (* X16 <- addr + ofs *) expand_builtin_vstore_common chunk (RR1 X16) _0 src end | _ -> @@ -330,37 +330,37 @@ let expand_builtin_inline name args res = | "__builtin_nop", [], _ -> emit Pnop (* Byte swap *) - | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> + | ("__builtin_bswap" | "__builtin_bswap32"), [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) -> emit (Prev(W, res, a1)) - | "__builtin_bswap64", [BA(IR a1)], BR(IR res) -> + | "__builtin_bswap64", [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) -> emit (Prev(X, res, a1)) - | "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> + | "__builtin_bswap16", [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) -> emit (Prev16(W, res, a1)); emit (Pandimm(W, res, RR0 res, Z.of_uint 0xFFFF)) (* Count leading zeros and leading sign bits *) - | "__builtin_clz", [BA(IR a1)], BR(IR res) -> + | "__builtin_clz", [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) -> emit (Pclz(W, res, a1)) - | ("__builtin_clzl" | "__builtin_clzll"), [BA(IR a1)], BR(IR res) -> + | ("__builtin_clzl" | "__builtin_clzll"), [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) -> emit (Pclz(X, res, a1)) - | "__builtin_cls", [BA(IR a1)], BR(IR res) -> + | "__builtin_cls", [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) -> emit (Pcls(W, res, a1)) - | ("__builtin_clsl" | "__builtin_clsll"), [BA(IR a1)], BR(IR res) -> + | ("__builtin_clsl" | "__builtin_clsll"), [BA(DR(IR'(RR1 a1)))], BR(DR(IR'(RR1 res))) -> emit (Pcls(X, res, a1)) (* Float arithmetic *) - | "__builtin_fabs", [BA(FR a1)], BR(FR res) -> + | "__builtin_fabs", [BA(DR(FR' a1))], BR(DR(FR' res)) -> emit (Pfabs(D, res, a1)) - | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> + | "__builtin_fsqrt", [BA(DR(FR' a1))], BR(DR(FR' res)) -> emit (Pfsqrt(D, res, a1)) - | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> + | "__builtin_fmadd", [BA(DR(FR' a1)); BA(DR(FR' a2)); BA(DR(FR' a3))], BR(DR(FR' res)) -> emit (Pfmadd(D, res, a1, a2, a3)) - | "__builtin_fmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> + | "__builtin_fmsub", [BA(DR(FR' a1)); BA(DR(FR' a2)); BA(DR(FR' a3))], BR(DR(FR' res)) -> emit (Pfmsub(D, res, a1, a2, a3)) - | "__builtin_fnmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> + | "__builtin_fnmadd", [BA(DR(FR' a1)); BA(DR(FR' a2)); BA(DR(FR' a3))], BR(DR(FR' res)) -> emit (Pfnmadd(D, res, a1, a2, a3)) - | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> + | "__builtin_fnmsub", [BA(DR(FR' a1)); BA(DR(FR' a2)); BA(DR(FR' a3))], BR(DR(FR' res)) -> emit (Pfnmsub(D, res, a1, a2, a3)) (* Vararg *) - | "__builtin_va_start", [BA(IR a)], _ -> + | "__builtin_va_start", [BA(DR(IR'(RR1 a)))], _ -> expand_builtin_va_start a (* Catch-all *) | _ -> @@ -427,9 +427,9 @@ let float_reg_to_dwarf = function | D30 -> 94 | D31 -> 95 let preg_to_dwarf = function - | IR r -> int_reg_to_dwarf r - | FR r -> float_reg_to_dwarf r - | SP -> 31 + | DR(IR'(RR1 r)) -> int_reg_to_dwarf r + | DR(FR' r) -> float_reg_to_dwarf r + | DR(IR'(XSP)) -> 31 | _ -> assert false let expand_function id fn = diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 5dec10e9..af069929 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -28,19 +28,19 @@ Local Open Scope error_monad_scope. Module Asmblock_TRANSF. (* STUB *) -Definition ireg_of_preg (p : Asmblock.preg) : res ireg := +Definition ireg_of_preg (p : Asm.preg) : res ireg := match p with | DR (IR' (RR1 r)) => OK r | _ => Error (msg "Asmgen.ireg_of_preg") end. -Definition freg_of_preg (p : Asmblock.preg) : res freg := +Definition freg_of_preg (p : Asm.preg) : res freg := match p with | DR (FR' r) => OK r | _ => Error (msg "Asmgen.freg_of_preg") end. -Definition iregsp_of_preg (p : Asmblock.preg) : res iregsp := +Definition iregsp_of_preg (p : Asm.preg) : res iregsp := match p with | DR (IR' r) => OK r | _ => Error (msg "Asmgen.iregsp_of_preg") @@ -61,7 +61,7 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction := OK (Asm.Pfmovimmd rd' f) | PArith (PArithPP (Pmovk sz n pos) rd rs) => - if (Asmblock.preg_eq rd rs) then ( + if (Asm.preg_eq rd rs) then ( do rd' <- ireg_of_preg rd; OK (Asm.Pmovk sz rd' n pos) ) else @@ -359,4 +359,4 @@ Definition transf_program (p: Mach.program) : res Asm.program := let mbp := Machblockgen.transf_program p in do mbp' <- PseudoAsmblockproof.transf_program mbp; do abp <- Asmblockgen.transf_program mbp'; - Asmblock_TRANSF.transf_program abp. + Asmblock_TRANSF.transf_program abp.
\ No newline at end of file diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 0ea37a38..f469e437 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Léo Gourdin UGA, VERIMAG *) (* Justus Fasse UGA, VERIMAG *) (* Xavier Leroy INRIA Paris-Rocquencourt *) (* David Monniaux CNRS, VERIMAG *) @@ -17,7 +18,7 @@ Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. -Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock. +Require Import Op Locations Machblock Conventions PseudoAsmblock Asm Asmblock. Require Machblockgenproof Asmblockgenproof. Require Import Asmgen. Require Import Axioms. @@ -1862,8 +1863,8 @@ Qed. Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m (ATPC : rs PC = Vptr b ofs) (MATCHI : match_internal (size bb - 1) - {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} - {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}), + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}), _rs PC = Vptr b (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))). Proof. intros; inv MATCHI. rewrite <- AGPC; rewrite ATPC; unfold Val.offset_ptr; eauto. @@ -1874,8 +1875,8 @@ Lemma find_instr_ofs_somei: forall ofs bb f tc asmi rs m _rs _m (FIND_INSTR : Asm.find_instr (Ptrofs.unsigned ofs + (size bb - 1)) tc = Some (asmi)) (MATCHI : match_internal (size bb - 1) - {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} - {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}), + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}), Asm.find_instr (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) (Asm.fn_code {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}) = Some (asmi). @@ -1900,8 +1901,8 @@ Qed. Lemma eval_builtin_args_match: forall bb rs m _rs _m args vargs (MATCHI : match_internal (size bb - 1) - {| Asmblockgenproof.AB._rs := rs; Asmblockgenproof.AB._m := m |} - {| Asmblockgenproof.AB._rs := _rs; Asmblockgenproof.AB._m := _m |}) + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}) (EVAL : eval_builtin_args tge (fun r : dreg => rs r) (rs SP) m args vargs), eval_builtin_args tge _rs (_rs SP) _m (map (map_builtin_arg DR) args) vargs. Proof. @@ -2114,9 +2115,9 @@ Proof. erewrite !set_builtin_map_not_pc. rewrite HPC. eapply set_builtin_res_dont_move_pc_gen; intros. eapply set_buitin_res_sym; eauto. +Qed. - Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) diff --git a/aarch64/OrigAsmgen.ml b/aarch64/OrigAsmgen.ml new file mode 100644 index 00000000..1bbcf085 --- /dev/null +++ b/aarch64/OrigAsmgen.ml @@ -0,0 +1,282 @@ +(** File (more or less) extracted from the official aarch64/Asmgen.v of CompCert + +TODO: prune some definition in these files by reusing the ones of Asmblockgen that are identical... +e.g. all those which do not involve Asm.code + +**) + +open Asm +open BinInt +open BinNums +open Integers +open List0 +open Zbits + +module I = Integers.Int +module I64 = Integers.Int64 +module N = PeanoNat.Nat + +let s_ x = Datatypes.S x +let o_ = Datatypes.O + +module Automaton = + struct + type state = + | SA + | SB + | SC + | SD + | SE + | SF + | SG + | Sbad + + (** val start : state **) + + let start = + SA + + (** val next : state -> bool -> state **) + + let next s b = + match s with + | SA -> if b then SC else SB + | SB -> if b then SD else SB + | SC -> if b then SC else SE + | SD -> if b then SD else SF + | SE -> if b then SG else SE + | SF -> if b then Sbad else SF + | SG -> if b then SG else Sbad + | Sbad -> Sbad + + (** val accepting : state -> bool **) + + let accepting = function + | Sbad -> false + | _ -> true + + (** val run : nat -> state -> coq_Z -> bool **) + + let rec run len s x = + match len with + | Datatypes.O -> accepting s + | Datatypes.S len0 -> run len0 (next s (Z.odd x)) (Z.div2 x) + end + +(** val logical_imm_length : coq_Z -> bool -> nat **) + +let logical_imm_length x sixtyfour = + let test = fun n -> + Z.eqb (coq_Zzero_ext n x) (coq_Zzero_ext n (Z.shiftr x n)) + in + if (&&) sixtyfour + (Datatypes.negb + (test (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH)))))))) + then s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ + (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ + (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ + o_))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + else if Datatypes.negb (test (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH)))))) + then s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ + (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ o_))))))))))))))))))))))))))))))) + else if Datatypes.negb (test (Zpos (Coq_xO (Coq_xO (Coq_xO Coq_xH))))) + then s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ + o_))))))))))))))) + else if Datatypes.negb (test (Zpos (Coq_xO (Coq_xO Coq_xH)))) + then s_ (s_ (s_ (s_ (s_ (s_ (s_ (s_ o_))))))) + else if Datatypes.negb (test (Zpos (Coq_xO Coq_xH))) + then s_ (s_ (s_ (s_ o_))) + else s_ (s_ o_) + +(** val is_logical_imm32 : I.int -> bool **) + +let is_logical_imm32 x = + (&&) ((&&) (Datatypes.negb (I.eq x I.zero)) (Datatypes.negb (I.eq x I.mone))) + (Automaton.run (logical_imm_length (I.unsigned x) false) + Automaton.start (I.unsigned x)) + +(** val is_logical_imm64 : I64.int -> bool **) + +let is_logical_imm64 x = + (&&) ((&&) (Datatypes.negb (I64.eq x I64.zero)) (Datatypes.negb (I64.eq x I64.mone))) + (Automaton.run (logical_imm_length (I64.unsigned x) true) + Automaton.start (I64.unsigned x)) + +(** val is_arith_imm32 : I.int -> bool **) + +let is_arith_imm32 x = + (||) (I.eq x (I.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))) x)) + (I.eq x + (I.shl + (I.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))) + (I.shru x (I.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH))))))) + (I.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH))))))) + +(** val is_arith_imm64 : I64.int -> bool **) + +let is_arith_imm64 x = + (||) + (I64.eq x (I64.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))) x)) + (I64.eq x + (I64.shl + (I64.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))) + (I64.shru x (I64.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH))))))) + (I64.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH))))))) + +(** val decompose_int : nat -> coq_Z -> coq_Z -> (coq_Z * coq_Z) list **) + +let rec decompose_int n n0 p = + match n with + | Datatypes.O -> [] + | Datatypes.S n1 -> + let frag = + coq_Zzero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH))))) + (Z.shiftr n0 p) + in + if Z.eqb frag Z0 + then decompose_int n1 n0 + (Z.add p (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH)))))) + else (frag, + p) :: (decompose_int n1 + (Z.ldiff n0 + (Z.shiftl (Zpos (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI + (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI + (Coq_xI (Coq_xI (Coq_xI (Coq_xI Coq_xH)))))))))))))))) + p)) + (Z.add p (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xO Coq_xH))))))) + +(** val negate_decomposition : + (coq_Z * coq_Z) list -> (coq_Z * coq_Z) list **) + +let negate_decomposition l = + map (fun np -> + ((Z.coq_lxor (fst np) (Zpos (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI + (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI (Coq_xI + (Coq_xI (Coq_xI Coq_xH))))))))))))))))), (snd np))) l + +(** val loadimm_k : + isize -> ireg -> (coq_Z * coq_Z) list -> Asm.code -> Asm.code **) + +let loadimm_k sz rd l k = + fold_right (fun np k0 -> (Pmovk (sz, rd, (fst np), (snd np))) :: k0) k l + +(** val loadimm_z : + isize -> ireg -> (coq_Z * coq_Z) list -> Asm.code -> Asm.code **) + +let loadimm_z sz rd l k = + match l with + | [] -> (Pmovz (sz, rd, Z0, Z0)) :: k + | p :: l0 -> + let (n1, p1) = p in (Pmovz (sz, rd, n1, p1)) :: (loadimm_k sz rd l0 k) + +(** val loadimm_n : + isize -> ireg -> (coq_Z * coq_Z) list -> Asm.code -> Asm.code **) + +let loadimm_n sz rd l k = + match l with + | [] -> (Pmovn (sz, rd, Z0, Z0)) :: k + | p :: l0 -> + let (n1, p1) = p in + (Pmovn (sz, rd, n1, p1)) :: (loadimm_k sz rd (negate_decomposition l0) k) + +(** val loadimm : isize -> ireg -> coq_Z -> Asm.code -> Asm.code **) + +let loadimm sz rd n k = + let n0 = match sz with + | W -> s_ (s_ o_) + | X -> s_ (s_ (s_ (s_ o_))) in + let dz = decompose_int n0 n Z0 in + let dn = decompose_int n0 (Z.lnot n) Z0 in + if N.leb (Datatypes.length dz) (Datatypes.length dn) + then loadimm_z sz rd dz k + else loadimm_n sz rd dn k + +(** val loadimm32 : ireg -> I.int -> Asm.code -> Asm.code **) + +let loadimm32 rd n k = + if is_logical_imm32 n + then (Porrimm (W, rd, XZR, (I.unsigned n))) :: k + else loadimm W rd (I.unsigned n) k + +(** val loadimm64 : ireg -> I64.int -> Asm.code -> Asm.code **) + +let loadimm64 rd n k = + if is_logical_imm64 n + then (Porrimm (X, rd, XZR, (I64.unsigned n))) :: k + else loadimm X rd (I64.unsigned n) k + +(** val addimm_aux : + (iregsp -> iregsp -> coq_Z -> Asm.instruction) -> iregsp -> iregsp -> + coq_Z -> Asm.code -> Asm.instruction list **) + +let addimm_aux insn rd r1 n k = + let nlo = coq_Zzero_ext (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))) n in + let nhi = Z.sub n nlo in + if Z.eqb nhi Z0 + then (insn rd r1 nlo) :: k + else if Z.eqb nlo Z0 + then (insn rd r1 nhi) :: k + else (insn rd r1 nhi) :: ((insn rd rd nlo) :: k) + +(** val addimm32 : ireg -> ireg -> I.int -> Asm.code -> Asm.code **) + +let addimm32 rd r1 n k = + let m = I.neg n in + if I.eq n + (I.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xI Coq_xH))))) n) + then addimm_aux (fun x x0 x1 -> Paddimm (W, x, x0, x1)) (RR1 rd) (RR1 r1) + (I.unsigned n) k + else if I.eq m + (I.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xI Coq_xH))))) m) + then addimm_aux (fun x x0 x1 -> Psubimm (W, x, x0, x1)) (RR1 rd) (RR1 + r1) (I.unsigned m) k + else if I.lt n I.zero + then loadimm32 X16 m ((Psub (W, rd, (RR0 r1), X16, SOnone)) :: k) + else loadimm32 X16 n ((Padd (W, rd, (RR0 r1), X16, SOnone)) :: k) + +(** val addimm64 : iregsp -> iregsp -> I64.int -> Asm.code -> Asm.code **) + +let addimm64 rd r1 n k = + let m = I64.neg n in + if I64.eq n + (I64.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xI Coq_xH))))) n) + then addimm_aux (fun x x0 x1 -> Paddimm (X, x, x0, x1)) rd r1 + (I64.unsigned n) k + else if I64.eq m + (I64.zero_ext (Zpos (Coq_xO (Coq_xO (Coq_xO (Coq_xI Coq_xH))))) + m) + then addimm_aux (fun x x0 x1 -> Psubimm (X, x, x0, x1)) rd r1 + (I64.unsigned m) k + else if I64.lt n I64.zero + then loadimm64 X16 m ((Psubext (rd, r1, X16, (EOuxtx + I.zero))) :: k) + else loadimm64 X16 n ((Paddext (rd, r1, X16, (EOuxtx + I.zero))) :: k) + +(** val offset_representable : coq_Z -> I64.int -> bool **) + +let offset_representable sz ofs = + let isz = I64.repr sz in + (||) + (I64.eq ofs + (I64.sign_ext (Zpos (Coq_xI (Coq_xO (Coq_xO Coq_xH)))) ofs)) + ((&&) (I64.eq (I64.modu ofs isz) I64.zero) + (I64.ltu ofs + (I64.shl isz (I64.repr (Zpos (Coq_xO (Coq_xO (Coq_xI Coq_xH)))))))) + +(** val indexed_memory_access : + (Asm.addressing -> Asm.instruction) -> coq_Z -> iregsp -> Ptrofs.int -> + Asm.code -> Asm.instruction list **) + +let indexed_memory_access insn sz base ofs k = + let ofs0 = Ptrofs.to_int64 ofs in + if offset_representable sz ofs0 + then (insn (ADimm (base, ofs0))) :: k + else loadimm64 X16 ofs0 ((insn (ADreg (base, X16))) :: k) + +(** val storeptr : + ireg -> iregsp -> Ptrofs.int -> Asm.code -> Asm.instruction list **) + +let storeptr src base ofs k = + indexed_memory_access (fun x -> Pstrx (src, x)) (Zpos (Coq_xO (Coq_xO + (Coq_xO Coq_xH)))) base ofs k diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 8d74daf4..b1425d56 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -120,13 +120,13 @@ module Target : TARGET = output_string oc (match sz with D -> dreg_name r | S -> sreg_name r) let preg_asm oc ty = function - | IR r -> if ty = Tint then wreg oc r else xreg oc r - | FR r -> if ty = Tsingle then sreg oc r else dreg oc r + | DR (IR' (RR1 r)) -> if ty = Tint then wreg oc r else xreg oc r + | DR (FR' r) -> if ty = Tsingle then sreg oc r else dreg oc r | _ -> assert false let preg_annot = function - | IR r -> xreg_name r - | FR r -> dreg_name r + | DR (IR' (RR1 r)) -> xreg_name r + | DR (FR' r) -> dreg_name r | _ -> assert false (* Names of sections *) diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v index e82056e2..6815bc59 100644 --- a/aarch64/extractionMachdep.v +++ b/aarch64/extractionMachdep.v @@ -21,4 +21,4 @@ Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *) (* Asm *) Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false". -Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned". +Extract Constant Asmblockgen.symbol_is_aligned => "C2C.atom_is_aligned". diff --git a/extraction/extraction.v b/extraction/extraction.v index bd396cd8..5de66797 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -13,6 +13,7 @@ (* *) (* *********************************************************************) +Require Import ZArith PeanoNat. Require Coqlib. Require Wfsimpl. Require DecidableClass Decidableplus. @@ -218,7 +219,8 @@ Set Extraction AccessOpaque. Cd "extraction". -Separate Extraction +Separate Extraction + Z.ldiff Z.lnot Nat.leb CSE3analysis.internal_analysis CSE3analysis.eq_depends_on_mem Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state |