Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit d6204e0c authored by Léo Gourdin's avatar Léo Gourdin
Browse files

fix aarch64 merge?

parent 7cc2810b
......@@ -76,6 +76,8 @@ build_aarch64:
script:
- ./config_aarch64.sh
- make -j "$NJOBS"
- export LD_LIBRARY_PATH=/usr/aarch64-linux-gnu/lib
- sudo ln -s /usr/aarch64-linux-gnu/lib/ld-linux-aarch64.so.1 /lib
- make -C test CCOMPOPTS='-static' SIMU='qemu-aarch64' EXECUTE='qemu-aarch64' all test
- ulimit -s65536 && make -C test/monniaux/yarpgen TARGET_CC='aarch64-linux-gnu-gcc' EXECUTE='qemu-aarch64' CCOMPOPTS='-static' TARGET_CFLAGS='-static'
rules:
......
......@@ -87,14 +87,12 @@ Global Opaque ptr64 big_endian splitlong
(** Which ABI to implement *)
<<<<<<< HEAD
Parameter pic_code: unit -> bool.
Definition has_notrap_loads := false.
=======
Inductive abi_kind: Type :=
| AAPCS64 (**r ARM's standard as used in Linux and other ELF platforms *)
| Apple. (**r the variant used in macOS and iOS *)
Parameter abi: abi_kind.
>>>>>>> master
......@@ -17,121 +17,8 @@
Require Import Recdef Coqlib Zwf Zbits.
Require Import Errors AST Integers Floats Op.
<<<<<<< HEAD
Require Import Locations Compopts.
Require Import Mach Asm Asmblock Asmblockgen Machblockgen PostpassScheduling.
=======
Require Import Locations Mach Asm.
Require SelectOp.
Local Open Scope string_scope.
Local Open Scope list_scope.
Local Open Scope error_monad_scope.
(** Alignment check for symbols *)
Parameter symbol_is_aligned : ident -> Z -> bool.
(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)
(** Extracting integer or float registers. *)
Definition ireg_of (r: mreg) : res ireg :=
match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end.
Definition freg_of (r: mreg) : res freg :=
match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end.
(** Recognition of immediate arguments for logical integer operations.*)
(** Valid immediate arguments are repetitions of a bit pattern [B]
of length [e] = 2, 4, 8, 16, 32 or 64.
The bit pattern [B] must be of the form [0*1*0*] or [1*0*1*]
but must not be all zeros or all ones. *)
(** The following automaton recognizes [0*1*0*|1*0*1*].
<<
0 1 0
/ \ / \ / \
\ / \ / \ /
-0--> [B] --1--> [D] --0--> [F]
/
[A]
\
-1--> [C] --0--> [E] --1--> [G]
/ \ / \ / \
\ / \ / \ /
1 0 1
>>
*)
Module Automaton.
Inductive state : Type := SA | SB | SC | SD | SE | SF | SG | Sbad.
Definition start := SA.
Definition next (s: state) (b: bool) :=
match s, b with
| SA,false => SB | SA,true => SC
| SB,false => SB | SB,true => SD
| SC,false => SE | SC,true => SC
| SD,false => SF | SD,true => SD
| SE,false => SE | SE,true => SG
| SF,false => SF | SF,true => Sbad
| SG,false => Sbad | SG,true => SG
| Sbad,_ => Sbad
end.
Definition accepting (s: state) :=
match s with
| SA | SB | SC | SD | SE | SF | SG => true
| Sbad => false
end.
Fixpoint run (len: nat) (s: state) (x: Z) : bool :=
match len with
| Datatypes.O => accepting s
| Datatypes.S len => run len (next s (Z.odd x)) (Z.div2 x)
end.
End Automaton.
(** The following function determines the candidate length [e],
ensuring that [x] is a repetition [BB...B]
of a bit pattern [B] of length [e]. *)
Definition logical_imm_length (x: Z) (sixtyfour: bool) : nat :=
(** [test n] checks that the low [2n] bits of [x] are of the
form [BB], that is, two occurrences of the same [n] bits *)
let test (n: Z) : bool :=
Z.eqb (Zzero_ext n x) (Zzero_ext n (Z.shiftr x n)) in
(** If [test n] fails, we know that the candidate length [e] is
at least [2n]. Hence we test with decreasing values of [n]:
32, 16, 8, 4, 2. *)
if sixtyfour && negb (test 32) then 64%nat
else if negb (test 16) then 32%nat
else if negb (test 8) then 16%nat
else if negb (test 4) then 8%nat
else if negb (test 2) then 4%nat
else 2%nat.
(** A valid logical immediate is
- neither [0] nor [-1];
- composed of a repetition [BBBBB] of a bit-pattern [B] of length [e]
- the low [e] bits of the number, that is, [B], match [0*1*0*] or [1*0*1*].
*)
Definition is_logical_imm32 (x: int) : bool :=
negb (Int.eq x Int.zero) && negb (Int.eq x Int.mone) &&
Automaton.run (logical_imm_length (Int.unsigned x) false)
Automaton.start (Int.unsigned x).
Definition is_logical_imm64 (x: int64) : bool :=
negb (Int64.eq x Int64.zero) && negb (Int64.eq x Int64.mone) &&
Automaton.run (logical_imm_length (Int64.unsigned x) true)
Automaton.start (Int64.unsigned x).
>>>>>>> master
Local Open Scope error_monad_scope.
......@@ -194,86 +81,7 @@ Definition addimm64 (rd r1: iregsp) (n: int64) (k: code) : code :=
else if Int64.eq m (Int64.zero_ext 24 m) then
addimm_aux (Asm.Psubimm X) rd r1 (Int64.unsigned m) k
else if Int64.lt n Int64.zero then
<<<<<<< HEAD
loadimm64 X16 m (Asm.Psubext rd r1 X16 (EOuxtx Int.zero) :: k)
=======
loadimm64 X16 m (Psubext rd r1 X16 (EOuxtx Int.zero) :: k)
else
loadimm64 X16 n (Paddext rd r1 X16 (EOuxtx Int.zero) :: k).
(** Logical immediate *)
Definition logicalimm32
(insn1: ireg -> ireg0 -> Z -> instruction)
(insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction)
(rd r1: ireg) (n: int) (k: code) : code :=
if is_logical_imm32 n
then insn1 rd r1 (Int.unsigned n) :: k
else loadimm32 X16 n (insn2 rd r1 X16 SOnone :: k).
Definition logicalimm64
(insn1: ireg -> ireg0 -> Z -> instruction)
(insn2: ireg -> ireg0 -> ireg -> shift_op -> instruction)
(rd r1: ireg) (n: int64) (k: code) : code :=
if is_logical_imm64 n
then insn1 rd r1 (Int64.unsigned n) :: k
else loadimm64 X16 n (insn2 rd r1 X16 SOnone :: k).
(** Sign- or zero-extended arithmetic *)
Definition transl_extension (ex: extension) (a: int) : extend_op :=
match ex with Xsgn32 => EOsxtw a | Xuns32 => EOuxtw a end.
Definition move_extended_base
(rd: ireg) (r1: ireg) (ex: extension) (k: code) : code :=
match ex with
| Xsgn32 => Pcvtsw2x rd r1 :: k
| Xuns32 => Pcvtuw2x rd r1 :: k
end.
Definition move_extended
(rd: ireg) (r1: ireg) (ex: extension) (a: int) (k: code) : code :=
if Int.eq a Int.zero then
move_extended_base rd r1 ex k
else
move_extended_base rd r1 ex (Padd X rd XZR rd (SOlsl a) :: k).
Definition arith_extended
(insnX: iregsp -> iregsp -> ireg -> extend_op -> instruction)
(insnS: ireg -> ireg0 -> ireg -> shift_op -> instruction)
(rd r1 r2: ireg) (ex: extension) (a: int) (k: code) : code :=
if Int.ltu a (Int.repr 5) then
insnX rd r1 r2 (transl_extension ex a) :: k
else
move_extended_base X16 r2 ex (insnS rd r1 X16 (SOlsl a) :: k).
(** Extended right shift *)
Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code :=
if Int.eq n Int.zero then
Pmov rd r1 :: k
else
Porr W X16 XZR r1 (SOasr (Int.repr 31)) ::
Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) ::
Porr W rd XZR X16 (SOasr n) :: k.
Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code :=
if Int.eq n Int.zero then
Pmov rd r1 :: k
else
Porr X X16 XZR r1 (SOasr (Int.repr 63)) ::
Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) ::
Porr X rd XZR X16 (SOasr n) :: k.
(** Load the address [id + ofs] in [rd] *)
Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: code) : code :=
if SelectOp.symbol_is_relocatable id then
if Ptrofs.eq ofs Ptrofs.zero then
Ploadsymbol rd id :: k
else
Ploadsymbol rd id :: addimm64 rd rd (Ptrofs.to_int64 ofs) k
>>>>>>> master
else
loadimm64 X16 n (Asm.Paddext rd r1 X16 (EOuxtx Int.zero) :: k).
......@@ -565,7 +373,6 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
| Pnop => OK (Asm.Pnop)
end.
<<<<<<< HEAD
Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction :=
match cfi with
| Pb l => Asm.Pb l
......@@ -580,59 +387,6 @@ Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction
| Ptbnz sz r n lbl => Asm.Ptbnz sz r n lbl
| Ptbz sz r n lbl => Asm.Ptbz sz r n lbl
| Pbtbl r1 tbl => Asm.Pbtbl r1 tbl
=======
(** Translation of addressing modes *)
Definition offset_representable (sz: Z) (ofs: int64) : bool :=
let isz := Int64.repr sz in
(** either unscaled 9-bit signed *)
Int64.eq ofs (Int64.sign_ext 9 ofs) ||
(** or scaled 12-bit unsigned *)
(Int64.eq (Int64.modu ofs isz) Int64.zero
&& Int64.ltu ofs (Int64.shl isz (Int64.repr 12))).
Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
(insn: Asm.addressing -> instruction) (k: code) : res code :=
match addr, args with
| Aindexed ofs, a1 :: nil =>
do r1 <- ireg_of a1;
if offset_representable sz ofs then
OK (insn (ADimm r1 ofs) :: k)
else
OK (loadimm64 X16 ofs (insn (ADreg r1 X16) :: k))
| Aindexed2, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (insn (ADreg r1 r2) :: k)
| Aindexed2shift a, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
if Int.eq a Int.zero then
OK (insn (ADreg r1 r2) :: k)
else if Int.eq (Int.shl Int.one a) (Int.repr sz) then
OK (insn (ADlsl r1 r2 a) :: k)
else
OK (Padd X X16 r1 r2 (SOlsl a) :: insn (ADimm X16 Int64.zero) :: k)
| Aindexed2ext x a, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
if Int.eq a Int.zero || Int.eq (Int.shl Int.one a) (Int.repr sz) then
OK (insn (match x with Xsgn32 => ADsxt r1 r2 a
| Xuns32 => ADuxt r1 r2 a end) :: k)
else
OK (arith_extended Paddext (Padd X) X16 r1 r2 x a
(insn (ADimm X16 Int64.zero) :: k))
| Aglobal id ofs, nil =>
assertion (negb (SelectOp.symbol_is_relocatable id));
if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k)
else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k))
| Ainstack ofs, nil =>
let ofs := Ptrofs.to_int64 ofs in
if offset_representable sz ofs then
OK (insn (ADimm XSP ofs) :: k)
else
OK (loadimm64 X16 ofs (insn (ADreg XSP X16) :: k))
| _, _ =>
Error(msg "Asmgen.transl_addressing")
>>>>>>> master
end.
Definition control_to_instruction (c: control) :=
......
......@@ -21,28 +21,6 @@ open AisAnnot
open PrintAsmaux
open Fileinfo
<<<<<<< HEAD
(* Module containing the printing functions *)
module Target (*: TARGET*) =
=======
(* 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"
*)
let is_immediate_float64 bits =
let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
let is_immediate_float32 bits =
let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
let mant = Int32.logand bits 0x7F_FFFFl in
exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
(* Naming and printing registers *)
let intsz oc (sz, n) =
match sz with X -> coqint64 oc n | W -> coqint oc n
......@@ -112,14 +90,14 @@ let freg oc (sz, r) =
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
| _ -> assert false
| 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
| _ -> assert false
| DR (IR (RR1 r)) -> xreg_name r
| DR (FR r) -> dreg_name r
| _ -> assert false
(* Base-2 log of a Caml integer *)
let rec log2 n =
......@@ -147,7 +125,6 @@ module type SYSTEM =
end
module ELF_System : SYSTEM =
>>>>>>> master
struct
let comment = "//"
let raw_symbol = output_string
......@@ -161,105 +138,18 @@ module ELF_System : SYSTEM =
let label_low oc lbl =
fprintf oc "#:lo12:%a" elf_label lbl
<<<<<<< HEAD
let print_label oc lbl = label oc (transl_label lbl)
let load_symbol_address oc rd id =
fprintf oc " adrp %a, :got:%a\n" xreg rd symbol id;
fprintf oc " ldr %a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id
let intsz oc (sz, n) =
match sz with X -> coqint64 oc n | W -> coqint oc n
let xreg_name = function
| X0 -> "x0" | X1 -> "x1" | X2 -> "x2" | X3 -> "x3"
| X4 -> "x4" | X5 -> "x5" | X6 -> "x6" | X7 -> "x7"
| X8 -> "x8" | X9 -> "x9" | X10 -> "x10" | X11 -> "x11"
| X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15"
| X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19"
| X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23"
| X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27"
| X28 -> "x28" | X29 -> "x29" | X30 -> "x30"
let wreg_name = function
| X0 -> "w0" | X1 -> "w1" | X2 -> "w2" | X3 -> "w3"
| X4 -> "w4" | X5 -> "w5" | X6 -> "w6" | X7 -> "w7"
| X8 -> "w8" | X9 -> "w9" | X10 -> "w10" | X11 -> "w11"
| X12 -> "w12" | X13 -> "w13" | X14 -> "w14" | X15 -> "w15"
| X16 -> "w16" | X17 -> "w17" | X18 -> "w18" | X19 -> "w19"
| X20 -> "w20" | X21 -> "w21" | X22 -> "w22" | X23 -> "w23"
| X24 -> "w24" | X25 -> "w25" | X26 -> "w26" | X27 -> "w27"
| X28 -> "w28" | X29 -> "w29" | X30 -> "w30"
let xreg0_name = function RR0 r -> xreg_name r | XZR -> "xzr"
let wreg0_name = function RR0 r -> wreg_name r | XZR -> "wzr"
let xregsp_name = function RR1 r -> xreg_name r | XSP -> "sp"
let wregsp_name = function RR1 r -> wreg_name r | XSP -> "wsp"
let dreg_name = function
| D0 -> "d0" | D1 -> "d1" | D2 -> "d2" | D3 -> "d3"
| D4 -> "d4" | D5 -> "d5" | D6 -> "d6" | D7 -> "d7"
| D8 -> "d8" | D9 -> "d9" | D10 -> "d10" | D11 -> "d11"
| D12 -> "d12" | D13 -> "d13" | D14 -> "d14" | D15 -> "d15"
| D16 -> "d16" | D17 -> "d17" | D18 -> "d18" | D19 -> "d19"
| D20 -> "d20" | D21 -> "d21" | D22 -> "d22" | D23 -> "d23"
| D24 -> "d24" | D25 -> "d25" | D26 -> "d26" | D27 -> "d27"
| D28 -> "d28" | D29 -> "d29" | D30 -> "d30" | D31 -> "d31"
let sreg_name = function
| D0 -> "s0" | D1 -> "s1" | D2 -> "s2" | D3 -> "s3"
| D4 -> "s4" | D5 -> "s5" | D6 -> "s6" | D7 -> "s7"
| D8 -> "s8" | D9 -> "s9" | D10 -> "s10" | D11 -> "s11"
| D12 -> "s12" | D13 -> "s13" | D14 -> "s14" | D15 -> "s15"
| D16 -> "s16" | D17 -> "s17" | D18 -> "s18" | D19 -> "s19"
| D20 -> "s20" | D21 -> "s21" | D22 -> "s22" | D23 -> "s23"
| D24 -> "s24" | D25 -> "s25" | D26 -> "s26" | D27 -> "s27"
| D28 -> "s28" | D29 -> "s29" | D30 -> "s30" | D31 -> "s31"
let xreg oc r = output_string oc (xreg_name r)
let wreg oc r = output_string oc (wreg_name r)
let ireg oc (sz, r) =
output_string oc (match sz with X -> xreg_name r | W -> wreg_name r)
let xreg0 oc r = output_string oc (xreg0_name r)
let wreg0 oc r = output_string oc (wreg0_name r)
let ireg0 oc (sz, r) =
output_string oc (match sz with X -> xreg0_name r | W -> wreg0_name r)
let xregsp oc r = output_string oc (xregsp_name r)
let iregsp oc (sz, r) =
output_string oc (match sz with X -> xregsp_name r | W -> wregsp_name r)
let dreg oc r = output_string oc (dreg_name r)
let sreg oc r = output_string oc (sreg_name r)
let freg oc (sz, r) =
output_string oc (match sz with D -> dreg_name r | S -> sreg_name r)
let preg_asm oc ty = function
| 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
| DR (IR (RR1 r)) -> xreg_name r
| DR (FR r) -> dreg_name r
| _ -> assert false
(* Names of sections *)
(* Names of sections *)
let name_of_section = function
| Section_text -> ".text"
| Section_data(i, true) ->
failwith "_Thread_local unsupported on this platform"
| Section_data(i, false) | Section_small_data i ->
if i then ".data" else common_section ()
=======
let load_symbol_address oc rd id =
fprintf oc " adrp %a, :got:%a\n" xreg rd symbol id;
fprintf oc " ldr %a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id
let name_of_section = function
| Section_text -> ".text"
| Section_data i | Section_small_data i ->
variable_section ~sec:".data" ~bss:".bss" i
>>>>>>> master
| Section_const i | Section_small_const i ->
variable_section ~sec:".section .rodata" i
| Section_string -> ".section .rodata"
......@@ -320,7 +210,9 @@ module MacOS_System : SYSTEM =
let name_of_section = function
| Section_text -> ".text"
| Section_data i | Section_small_data i ->
| Section_data(i, true) ->
failwith "_Thread_local unsupported on this platform"
| Section_data(i, false) | Section_small_data i ->
variable_section ~sec:".data" i
| Section_const i | Section_small_const i ->
variable_section ~sec:".const" ~reloc:".const_data" i
......
......@@ -19,6 +19,9 @@ Require Archi Asm Asmgen SelectOp.
(* Archi *)
Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *)
Extract Constant Archi.abi =>
"match Configuration.abi with
| ""apple"" -> Apple
......@@ -35,11 +38,4 @@ Extract Constant SelectOp.symbol_is_relocatable =>
Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false".
Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false".
<<<<<<< HEAD
Extract Constant Asmblockgen.symbol_is_aligned => "C2C.atom_is_aligned".
=======
(* Asmgen *)
Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned".
>>>>>>> master
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment