diff options
| -rw-r--r-- | verilog/Archi.v | 21 | ||||
| -rw-r--r-- | verilog/Asm.v | 9 | ||||
| -rw-r--r-- | verilog/Asmexpand.ml | 59 | ||||
| -rw-r--r-- | verilog/Asmgen.v | 6 | ||||
| -rw-r--r-- | verilog/Builtins1.v | 17 | ||||
| -rw-r--r-- | verilog/CBuiltins.ml | 17 | ||||
| -rw-r--r-- | verilog/ConstpropOp.v | 5 | ||||
| -rw-r--r-- | verilog/ConstpropOp.vp | 5 | ||||
| -rw-r--r-- | verilog/ConstpropOpproof.v | 2 | ||||
| -rw-r--r-- | verilog/Conventions1.v | 221 | ||||
| -rw-r--r-- | verilog/Machregs.v | 6 | ||||
| -rw-r--r-- | verilog/NeedOp.v | 2 | ||||
| -rw-r--r-- | verilog/Op.v | 36 | ||||
| -rw-r--r-- | verilog/PrintOp.ml | 2 | ||||
| -rw-r--r-- | verilog/SelectOp.v | 6 | ||||
| -rw-r--r-- | verilog/SelectOp.vp | 6 | ||||
| -rw-r--r-- | verilog/SelectOpproof.v | 7 | ||||
| -rw-r--r-- | verilog/Stacklayout.v | 22 | ||||
| -rw-r--r-- | verilog/TargetPrinter.ml | 158 | ||||
| -rw-r--r-- | verilog/ValueAOp.v | 4 | ||||
| -rw-r--r-- | verilog/extractionMachdep.v | 29 |
21 files changed, 475 insertions, 165 deletions
diff --git a/verilog/Archi.v b/verilog/Archi.v index 8f1ccdef..f801110a 100644 --- a/verilog/Archi.v +++ b/verilog/Archi.v @@ -7,10 +7,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -29,7 +30,9 @@ Definition align_float64 := 4%Z. Definition splitlong := false. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. -Proof. discriminate. Qed. +Proof. + unfold splitlong. destruct ptr64; simpl; congruence. +Qed. Definition default_nan_64 := (true, iter_nat 51 _ xO xH). Definition default_nan_32 := (true, iter_nat 22 _ xO xH). @@ -56,8 +59,14 @@ Definition fma_invalid_mul_is_nan := false. Definition float_of_single_preserves_sNaN := false. +Definition float_conversion_default_nan := false. + +(** Which ABI to use. *) +Parameter win64: bool. (* Always false in 32 bits *) + Global Opaque ptr64 big_endian splitlong default_nan_64 choose_nan_64 default_nan_32 choose_nan_32 fma_order fma_invalid_mul_is_nan - float_of_single_preserves_sNaN. + float_of_single_preserves_sNaN + float_conversion_default_nan. diff --git a/verilog/Asm.v b/verilog/Asm.v index 64ae1c32..64a835e1 100644 --- a/verilog/Asm.v +++ b/verilog/Asm.v @@ -279,6 +279,7 @@ Inductive instruction: Type := | Pmaxsd (rd: freg) (r2: freg) | Pminsd (rd: freg) (r2: freg) | Pmovb_rm (rd: ireg) (a: addrmode) + | Pmovq_rf (rd: ireg) (r1: freg) | Pmovsq_mr (a: addrmode) (rs: freg) | Pmovsq_rm (rd: freg) (a: addrmode) | Pmovsb @@ -311,6 +312,7 @@ Module Pregmap := EMap(PregEq). Definition regset := Pregmap.t val. Definition genv := Genv.t fundef unit. +Declare Scope asm. 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. @@ -876,6 +878,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (compare_floats (rs r1) (rs r2) rs)) m | Pxorpd_f rd => Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m + | Pmaxsd rd r1 => + Next (nextinstr (rs#rd <- (Op.maxf rs#rd rs#r1))) m + | Pminsd rd r1 => + Next (nextinstr (rs#rd <- (Op.minf rs#rd rs#r1))) m (** Arithmetic operations over single-precision floats *) | Padds_ff rd r1 => Next (nextinstr (rs#rd <- (Val.addfs rs#rd rs#r1))) m @@ -995,9 +1001,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfnmsub132 _ _ _ | Pfnmsub213 _ _ _ | Pfnmsub231 _ _ _ - | Pmaxsd _ _ - | Pminsd _ _ | Pmovb_rm _ _ + | Pmovq_rf _ _ | Pmovsq_rm _ _ | Pmovsq_mr _ _ | Pmovsb diff --git a/verilog/Asmexpand.ml b/verilog/Asmexpand.ml index 1b3961e0..b76ad3a3 100644 --- a/verilog/Asmexpand.ml +++ b/verilog/Asmexpand.ml @@ -408,24 +408,6 @@ let expand_builtin_inline name args res = (* Float arithmetic *) | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> emit (Psqrtsd (res,a1)) - | "__builtin_fmax", [BA(FR a1); BA(FR a2)], BR(FR res) -> - if res = a1 then - emit (Pmaxsd (res,a2)) - else if res = a2 then - emit (Pmaxsd (res,a1)) - else begin - emit (Pmovsd_ff (res,a1)); - emit (Pmaxsd (res,a2)) - end - | "__builtin_fmin", [BA(FR a1); BA(FR a2)], BR(FR res) -> - if res = a1 then - emit (Pminsd (res,a2)) - else if res = a2 then - emit (Pminsd (res,a1)) - else begin - emit (Pmovsd_ff (res,a1)); - emit (Pminsd (res,a2)) - end | "__builtin_fmadd", _, _ -> expand_fma args res (fun r1 r2 r3 -> Pfmadd132(r1, r2, r3)) @@ -491,7 +473,8 @@ let expand_builtin_inline name args res = (* Vararg stuff *) | "__builtin_va_start", [BA(IR a)], _ -> assert (a = RDX); - if Archi.ptr64 then expand_builtin_va_start_elf64 a + if Archi.win64 then expand_builtin_va_start_win64 a + else if Archi.ptr64 then expand_builtin_va_start_elf64 a else expand_builtin_va_start_32 a (* Synchronization *) | "__builtin_membar", [], _ -> @@ -522,7 +505,14 @@ let fixup_funcall_elf64 sg = registers. *) -let copy_fregs_to_iregs args fr ir = +let rec copy_fregs_to_iregs args fr ir = + match (ir, fr, args) with + | (i1 :: ir, f1 :: fr, (Tfloat | Tsingle) :: args) -> + emit (Pmovq_rf (i1, f1)); + copy_fregs_to_iregs args fr ir + | (i1 :: ir, f1 :: fr, _ :: args) -> + copy_fregs_to_iregs args fr ir + | _ -> () let fixup_funcall_win64 sg = @@ -530,8 +520,10 @@ let fixup_funcall_win64 sg = copy_fregs_to_iregs sg.sig_args [XMM0; XMM1; XMM2; XMM3] [RCX; RDX; R8; R9] let fixup_funcall sg = - if Archi.ptr64 then - fixup_funcall_elf64 sg + if Archi.ptr64 + then if Archi.win64 + then fixup_funcall_win64 sg + else fixup_funcall_elf64 sg else () (* Expansion of instructions *) @@ -539,7 +531,23 @@ let fixup_funcall sg = let expand_instruction instr = match instr with | Pallocframe (sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin + if Archi.win64 then begin + let sz = sp_adjustment_win64 sz in + if is_current_function_variadic() then + (* Save parameters passed in registers in reserved stack area *) + emit (Pcall_s (intern_string "__compcert_va_saveregs", + {sig_args = []; sig_res = Tvoid; sig_cc = cc_default})); + (* Allocate frame *) + let sz' = Z.of_uint sz in + emit (Psubl_ri (RSP, sz')); + emit (Pcfi_adjust sz'); + (* Stack chaining *) + let addr1 = linear_addr RSP (Z.of_uint (sz + 8)) in + let addr2 = linear_addr RSP ofs_link in + emit_leaq RAX addr1; + emit (Pmovq_mr (addr2, RAX)); + current_function_stacksize := Int64.of_int (sz + 8) + end else if Archi.ptr64 then begin let (sz, save_regs) = sp_adjustment_elf64 sz in (* Allocate frame *) let sz' = Z.of_uint sz in @@ -572,7 +580,10 @@ let expand_instruction instr = PrintAsmaux.current_function_stacksize := Int32.of_int sz end | Pfreeframe(sz, ofs_ra, ofs_link) -> - if Archi.ptr64 then begin + if Archi.win64 then begin + let sz = sp_adjustment_win64 sz in + emit (Paddq_ri (RSP, Z.of_uint sz)) + end else if Archi.ptr64 then begin let (sz, _) = sp_adjustment_elf64 sz in emit (Paddq_ri (RSP, Z.of_uint sz)) end else begin diff --git a/verilog/Asmgen.v b/verilog/Asmgen.v index 73e3263e..f8d25a50 100644 --- a/verilog/Asmgen.v +++ b/verilog/Asmgen.v @@ -585,6 +585,12 @@ Definition transl_op | Odivf, a1 :: a2 :: nil => assertion (mreg_eq a1 res); do r <- freg_of res; do r2 <- freg_of a2; OK (Pdivd_ff r r2 :: k) + | Omaxf, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Pmaxsd r r2 :: k) + | Ominf, a1 :: a2 :: nil => + assertion (mreg_eq a1 res); + do r <- freg_of res; do r2 <- freg_of a2; OK (Pminsd r r2 :: k) | Onegfs, a1 :: nil => assertion (mreg_eq a1 res); do r <- freg_of res; OK (Pnegs r :: k) diff --git a/verilog/Builtins1.v b/verilog/Builtins1.v index f1d60961..7c77a488 100644 --- a/verilog/Builtins1.v +++ b/verilog/Builtins1.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -41,14 +42,14 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | BI_fmin => mkbuiltin_n2t Tfloat Tfloat Tfloat (fun f1 f2 => match Float.compare f1 f2 with - | Some Eq | Some Lt => f1 - | Some Gt | None => f2 + | Some Lt => f1 + | Some Eq | Some Gt | None => f2 end) | BI_fmax => mkbuiltin_n2t Tfloat Tfloat Tfloat (fun f1 f2 => match Float.compare f1 f2 with - | Some Eq | Some Gt => f1 - | Some Lt | None => f2 + | Some Gt => f1 + | Some Eq | Some Lt | None => f2 end) end. diff --git a/verilog/CBuiltins.ml b/verilog/CBuiltins.ml index 6820c089..a549cd25 100644 --- a/verilog/CBuiltins.ml +++ b/verilog/CBuiltins.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) @@ -19,8 +20,12 @@ open C let (va_list_type, va_list_scalar, size_va_list) = if Archi.ptr64 then - (* Actually a struct passed by reference; equivalent to 3 64-bit words *) - (TArray(TInt(IULong, []), Some 3L, []), false, 3*8) + if Archi.win64 then + (* Just a pointer *) + (TPtr(TVoid [], []), true, 8) + else + (* Actually a struct passed by reference; equivalent to 3 64-bit words *) + (TArray(TInt(IULong, []), Some 3L, []), false, 3*8) else (* Just a pointer *) (TPtr(TVoid [], []), true, 4) diff --git a/verilog/ConstpropOp.v b/verilog/ConstpropOp.v index 9b9c9711..c525c9c2 100644 --- a/verilog/ConstpropOp.v +++ b/verilog/ConstpropOp.v @@ -17,11 +17,10 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats. Require Import Op Registers. Require Import ValueDomain ValueAOp. +Require SelectOp. (** * Converting known values to constants *) -Parameter symbol_is_external: ident -> bool. (**r See [SelectOp] *) - Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a. Definition const_for_result (a: aval) : option operation := @@ -31,7 +30,7 @@ Definition const_for_result (a: aval) : option operation := | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None | Ptr(Gl id ofs) => - if symbol_is_external id then + if SelectOp.symbol_is_external id then if Ptrofs.eq ofs Ptrofs.zero then Some (Oindirectsymbol id) else None else Some (Olea_ptr (Aglobal id ofs)) diff --git a/verilog/ConstpropOp.vp b/verilog/ConstpropOp.vp index ada8d54a..dd4b839a 100644 --- a/verilog/ConstpropOp.vp +++ b/verilog/ConstpropOp.vp @@ -17,11 +17,10 @@ Require Import Coqlib Compopts. Require Import AST Integers Floats. Require Import Op Registers. Require Import ValueDomain ValueAOp. +Require SelectOp. (** * Converting known values to constants *) -Parameter symbol_is_external: ident -> bool. (**r See [SelectOp] *) - Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a. Definition const_for_result (a: aval) : option operation := @@ -31,7 +30,7 @@ Definition const_for_result (a: aval) : option operation := | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None | Ptr(Gl id ofs) => - if symbol_is_external id then + if SelectOp.symbol_is_external id then if Ptrofs.eq ofs Ptrofs.zero then Some (Oindirectsymbol id) else None else Some (Olea_ptr (Aglobal id ofs)) diff --git a/verilog/ConstpropOpproof.v b/verilog/ConstpropOpproof.v index c0bdaa76..09c6e91b 100644 --- a/verilog/ConstpropOpproof.v +++ b/verilog/ConstpropOpproof.v @@ -107,7 +107,7 @@ Proof. - (* pointer *) destruct p; try discriminate; SimplVM. + (* global *) - destruct (symbol_is_external id). + destruct (SelectOp.symbol_is_external id). * revert H2; predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero; intros EQ; inv EQ. exists (Genv.symbol_address ge id Ptrofs.zero); auto. * inv H2. exists (Genv.symbol_address ge id ofs); split. diff --git a/verilog/Conventions1.v b/verilog/Conventions1.v index 592acd72..abd22001 100644 --- a/verilog/Conventions1.v +++ b/verilog/Conventions1.v @@ -31,40 +31,44 @@ Definition is_callee_save (r: mreg) : bool := match r with | AX | CX | DX => false | BX | BP => true - | SI | DI => negb Archi.ptr64 (**r callee-save in 32 bits but not in 64 bits *) + | SI | DI => negb Archi.ptr64 || Archi.win64 (**r callee-save in ELF 64 bits *) | R8 | R9 | R10 | R11 => false | R12 | R13 | R14 | R15 => true | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => false - | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => false + | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Archi.win64 | FP0 => false end. Definition int_caller_save_regs := if Archi.ptr64 - then AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil + then if Archi.win64 + then AX :: CX :: DX :: R8 :: R9 :: R10 :: R11 :: nil + else AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil else AX :: CX :: DX :: nil. Definition float_caller_save_regs := if Archi.ptr64 - then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: - X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil + then if Archi.win64 + then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: nil + else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: + X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. Definition int_callee_save_regs := if Archi.ptr64 - then BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil + then if Archi.win64 + then BX :: SI :: DI :: BP :: R12 :: R13 :: R14 :: R15 :: nil + else BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil else BX :: SI :: DI :: BP :: nil. -Definition float_callee_save_regs : list mreg := nil. +Definition float_callee_save_regs := + if Archi.ptr64 && Archi.win64 + then X6 :: X7 :: X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil + else nil. Definition destroyed_at_call := List.filter (fun r => negb (is_callee_save r)) all_mregs. -Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) -Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) - -Definition callee_save_type := mreg_type. - Definition is_float_reg (r: mreg) := match r with | AX | BX | CX | DX | SI | DI | BP @@ -73,6 +77,28 @@ Definition is_float_reg (r: mreg) := | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 | FP0 => true end. +Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) +Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) + +Definition callee_save_type := mreg_type. + +(** How to use registers for register allocation. + We favor the use of caller-save registers, using callee-save registers + only when no caller-save is available. *) + +Record alloc_regs := mk_alloc_regs { + preferred_int_regs: list mreg; + remaining_int_regs: list mreg; + preferred_float_regs: list mreg; + remaining_float_regs: list mreg +}. + +Definition allocatable_registers (_: unit) := + {| preferred_int_regs := int_caller_save_regs; + remaining_int_regs := int_callee_save_regs; + preferred_float_regs := float_caller_save_regs; + remaining_float_regs := float_callee_save_regs |}. + (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -181,7 +207,7 @@ Fixpoint loc_arguments_32 :: loc_arguments_32 tys (ofs + typesize ty) end. -(** In the x86-64 ABI: +(** In the x86-64 ELF ABI: - The first 6 integer arguments are passed in registers [DI], [SI], [DX], [CX], [R8], [R9]. - The first 8 floating-point arguments are passed in registers [X0] to [X7]. - Extra arguments are passed on the stack, in [Outgoing] slots. @@ -189,26 +215,62 @@ Fixpoint loc_arguments_32 of data is used in a slot. *) -Definition int_param_regs := DI :: SI :: DX :: CX :: R8 :: R9 :: nil. -Definition float_param_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. +Definition int_param_regs_elf64 := DI :: SI :: DX :: CX :: R8 :: R9 :: nil. +Definition float_param_regs_elf64 := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. -Fixpoint loc_arguments_64 +Fixpoint loc_arguments_elf64 (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) := match tyl with | nil => nil | (Tint | Tlong | Tany32 | Tany64) as ty :: tys => - match list_nth_z int_param_regs ir with + match list_nth_z int_param_regs_elf64 ir with + | None => + One (S Outgoing ofs ty) :: loc_arguments_elf64 tys ir fr (ofs + 2) + | Some ireg => + One (R ireg) :: loc_arguments_elf64 tys (ir + 1) fr ofs + end + | (Tfloat | Tsingle) as ty :: tys => + match list_nth_z float_param_regs_elf64 fr with + | None => + One (S Outgoing ofs ty) :: loc_arguments_elf64 tys ir fr (ofs + 2) + | Some freg => + One (R freg) :: loc_arguments_elf64 tys ir (fr + 1) ofs + end + end. + +(** In the x86-64 Win64 ABI: +- The first 4 arguments are passed in registers [RCX], [RDX], [R8], and [R9] + (for integer arguments) and [X0] to [X3] (for floating-point arguments). + Each argument "burns" both an integer register and a FP integer. +- The first 8 floating-point arguments are passed in registers [X0] to [X7]. +- Extra arguments are passed on the stack, in [Outgoing] slots. + Consecutive stack slots are separated by 8 bytes, even if only 4 bytes + of data is used in a slot. +- Four 8-byte words are always reserved at the bottom of the outgoing area + so that the callee can use them to save the registers containing the + first four arguments. This is handled in the Stacking phase. +*) + +Definition int_param_regs_win64 := CX :: DX :: R8 :: R9 :: nil. +Definition float_param_regs_win64 := X0 :: X1 :: X2 :: X3 :: nil. + +Fixpoint loc_arguments_win64 + (tyl: list typ) (r ofs: Z) {struct tyl} : list (rpair loc) := + match tyl with + | nil => nil + | (Tint | Tlong | Tany32 | Tany64) as ty :: tys => + match list_nth_z int_param_regs_win64 r with | None => - One (S Outgoing ofs ty) :: loc_arguments_64 tys ir fr (ofs + 2) + One (S Outgoing ofs ty) :: loc_arguments_win64 tys r (ofs + 2) | Some ireg => - One (R ireg) :: loc_arguments_64 tys (ir + 1) fr ofs + One (R ireg) :: loc_arguments_win64 tys (r + 1) ofs end | (Tfloat | Tsingle) as ty :: tys => - match list_nth_z float_param_regs fr with + match list_nth_z float_param_regs_win64 r with | None => - One (S Outgoing ofs ty) :: loc_arguments_64 tys ir fr (ofs + 2) + One (S Outgoing ofs ty) :: loc_arguments_win64 tys r (ofs + 2) | Some freg => - One (R freg) :: loc_arguments_64 tys ir (fr + 1) ofs + One (R freg) :: loc_arguments_win64 tys (r + 1) ofs end end. @@ -217,7 +279,9 @@ Fixpoint loc_arguments_64 Definition loc_arguments (s: signature) : list (rpair loc) := if Archi.ptr64 - then loc_arguments_64 s.(sig_args) 0 0 0 + then if Archi.win64 + then loc_arguments_win64 s.(sig_args) 0 0 + else loc_arguments_elf64 s.(sig_args) 0 0 0 else loc_arguments_32 s.(sig_args) 0. (** Argument locations are either caller-save registers or [Outgoing] @@ -236,9 +300,16 @@ Definition loc_argument_32_charact (ofs: Z) (l: loc) : Prop := | _ => False end. -Definition loc_argument_64_charact (ofs: Z) (l: loc) : Prop := +Definition loc_argument_elf64_charact (ofs: Z) (l: loc) : Prop := + match l with + | R r => In r int_param_regs_elf64 \/ In r float_param_regs_elf64 + | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs') + | _ => False + end. + +Definition loc_argument_win64_charact (ofs: Z) (l: loc) : Prop := match l with - | R r => In r int_param_regs \/ In r float_param_regs + | R r => In r int_param_regs_win64 \/ In r float_param_regs_win64 | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs') | _ => False end. @@ -258,37 +329,75 @@ Proof. * destruct H; split; eapply X; eauto; lia. Qed. -Remark loc_arguments_64_charact: +Remark loc_arguments_elf64_charact: forall tyl ir fr ofs p, - In p (loc_arguments_64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_64_charact ofs) p. + In p (loc_arguments_elf64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_elf64_charact ofs) p. +Proof. + assert (X: forall ofs1 ofs2 l, loc_argument_elf64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_elf64_charact ofs1 l). + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_elf64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_elf64_charact ofs1) p). + { destruct p; simpl; intuition eauto. } + assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). + { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. } +Opaque list_nth_z. + induction tyl; simpl loc_arguments_elf64; intros. + elim H. + assert (A: forall ty, In p + match list_nth_z int_param_regs_elf64 ir with + | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl (ir + 1) fr ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_elf64 tyl ir fr (ofs + 2) + end -> + forall_rpair (loc_argument_elf64_charact ofs) p). + { intros. destruct (list_nth_z int_param_regs_elf64 ir) as [r|] eqn:E; destruct H1. + subst. left. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. lia. assumption. + eapply Y; eauto. lia. } + assert (B: forall ty, In p + match list_nth_z float_param_regs_elf64 fr with + | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl ir (fr + 1) ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_elf64 tyl ir fr (ofs + 2) + end -> + forall_rpair (loc_argument_elf64_charact ofs) p). + { intros. destruct (list_nth_z float_param_regs_elf64 fr) as [r|] eqn:E; destruct H1. + subst. right. eapply list_nth_z_in; eauto. + eapply IHtyl; eauto. + subst. split. lia. assumption. + eapply Y; eauto. lia. } + destruct a; eauto. +Qed. + +Remark loc_arguments_win64_charact: + forall tyl r ofs p, + In p (loc_arguments_win64 tyl r ofs) -> (2 | ofs) -> forall_rpair (loc_argument_win64_charact ofs) p. Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_64_charact ofs1 l). + assert (X: forall ofs1 ofs2 l, loc_argument_win64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_win64_charact ofs1 l). { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } - assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p). + assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_win64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_win64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. } Opaque list_nth_z. - induction tyl; simpl loc_arguments_64; intros. + induction tyl; simpl loc_arguments_win64; intros. elim H. assert (A: forall ty, In p - match list_nth_z int_param_regs ir with - | Some ireg => One (R ireg) :: loc_arguments_64 tyl (ir + 1) fr ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_64 tyl ir fr (ofs + 2) + match list_nth_z int_param_regs_win64 r with + | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_win64 tyl r (ofs + 2) end -> - forall_rpair (loc_argument_64_charact ofs) p). - { intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1. + forall_rpair (loc_argument_win64_charact ofs) p). + { intros. destruct (list_nth_z int_param_regs_win64 r) as [r'|] eqn:E; destruct H1. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. subst. split. lia. assumption. eapply Y; eauto. lia. } assert (B: forall ty, In p - match list_nth_z float_param_regs fr with - | Some ireg => One (R ireg) :: loc_arguments_64 tyl ir (fr + 1) ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_64 tyl ir fr (ofs + 2) + match list_nth_z float_param_regs_win64 r with + | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs + | None => One (S Outgoing ofs ty) :: loc_arguments_win64 tyl r (ofs + 2) end -> - forall_rpair (loc_argument_64_charact ofs) p). - { intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1. + forall_rpair (loc_argument_win64_charact ofs) p). + { intros. destruct (list_nth_z float_param_regs_win64 r) as [r'|] eqn:E; destruct H1. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. subst. split. lia. assumption. @@ -300,18 +409,30 @@ Lemma loc_arguments_acceptable: forall (s: signature) (p: rpair loc), In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. - unfold loc_arguments; intros. destruct Archi.ptr64 eqn:SF. -- (* 64 bits *) - assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF; decide_goal). - assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal. - assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l). - { unfold loc_argument_64_charact, loc_argument_acceptable. + unfold loc_arguments; intros. destruct Archi.ptr64 eqn:SF; [destruct Archi.win64 eqn:W64|]. +- (* WIN 64 bits *) + assert (A: forall r, In r int_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF; decide_goal). + assert (B: forall r, In r float_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; decide_goal). + assert (X: forall l, loc_argument_win64_charact 0 l -> loc_argument_acceptable l). + { unfold loc_argument_win64_charact, loc_argument_acceptable. + destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. + intros [C D]. split; auto. apply Z.divide_trans with 2; auto. + exists (2 / typealign ty); destruct ty; reflexivity. + } + exploit loc_arguments_win64_charact; eauto using Z.divide_0_r. + unfold forall_rpair; destruct p; intuition auto. +- (* ELF 64 bits *) + assert (A: forall r, In r int_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF, W64; decide_goal). + assert (B: forall r, In r float_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite W64; decide_goal). + assert (X: forall l, loc_argument_elf64_charact 0 l -> loc_argument_acceptable l). + { unfold loc_argument_elf64_charact, loc_argument_acceptable. destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto. intros [C D]. split; auto. apply Z.divide_trans with 2; auto. exists (2 / typealign ty); destruct ty; reflexivity. } - exploit loc_arguments_64_charact; eauto using Z.divide_0_r. + exploit loc_arguments_elf64_charact; eauto using Z.divide_0_r. unfold forall_rpair; destruct p; intuition auto. + - (* 32 bits *) assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l). { destruct l as [r | [] ofs ty]; simpl; intuition auto. rewrite H2; apply Z.divide_1_l. } @@ -319,15 +440,15 @@ Proof. unfold forall_rpair; destruct p; intuition auto. Qed. -Hint Resolve loc_arguments_acceptable: locs. +Global Hint Resolve loc_arguments_acceptable: locs. Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. - unfold loc_arguments; destruct Archi.ptr64; reflexivity. + unfold loc_arguments; destruct Archi.ptr64; auto; destruct Archi.win64; auto. Qed. -(** ** Normalization of function results *) +(** ** Normalization of function results and parameters *) (** In the x86 ABI, a return value of type "char" is returned in register AL, leaving the top 24 bits of EAX unspecified. diff --git a/verilog/Machregs.v b/verilog/Machregs.v index 6f3064b8..042248a8 100644 --- a/verilog/Machregs.v +++ b/verilog/Machregs.v @@ -57,9 +57,9 @@ Proof. intros. specialize (H r). InvBooleans. auto. Qed. -Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. +Global Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. -Instance Finite_mreg : Finite mreg := { +Global Instance Finite_mreg : Finite mreg := { Finite_elements := all_mregs; Finite_elements_spec := all_mregs_complete }. @@ -334,6 +334,8 @@ Definition two_address_op (op: operation) : bool := | Osubf => true | Omulf => true | Odivf => true + | Omaxf => true + | Ominf => true | Onegfs => true | Oabsfs => true | Oaddfs => true diff --git a/verilog/NeedOp.v b/verilog/NeedOp.v index 775a23db..9c7469e9 100644 --- a/verilog/NeedOp.v +++ b/verilog/NeedOp.v @@ -113,7 +113,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ororlimm _ => op1 (default nv) | Oleal addr => needs_of_addressing_64 addr nv | Onegf | Oabsf => op1 (default nv) - | Oaddf | Osubf | Omulf | Odivf => op2 (default nv) + | Oaddf | Osubf | Omulf | Odivf | Omaxf | Ominf => op2 (default nv) | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Osingleoffloat | Ofloatofsingle => op1 (default nv) diff --git a/verilog/Op.v b/verilog/Op.v index 16d75426..fde078dc 100644 --- a/verilog/Op.v +++ b/verilog/Op.v @@ -149,6 +149,8 @@ Inductive operation : Type := | Osubf (**r [rd = r1 - r2] *) | Omulf (**r [rd = r1 * r2] *) | Odivf (**r [rd = r1 / r2] *) + | Omaxf (**r [rd = max(r1,r2)] *) + | Ominf (**r [rd = min(r1,r2)] *) | Onegfs (**r [rd = - r1] *) | Oabsfs (**r [rd = abs(r1)] *) | Oaddfs (**r [rd = r1 + r2] *) @@ -198,6 +200,32 @@ Defined. Global Opaque eq_condition eq_addressing eq_operation. +(** Helper function for floating point maximum and minimum operation *) + +Definition float_max f1 f2 := + match Float.compare f1 f2 with + | Some Gt => f1 + | Some Eq | Some Lt| None => f2 + end. + +Definition maxf (v1 v2: val) : val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => Vfloat (float_max f1 f2) + | _, _ => Vundef + end. + +Definition float_min f1 f2 := + match Float.compare f1 f2 with + | Some Lt => f1 + | Some Eq | Some Gt| None => f2 + end. + +Definition minf (v1 v2: val) : val := + match v1, v2 with + | Vfloat f1, Vfloat f2 => Vfloat (float_min f1 f2) + | _, _ => Vundef + end. + (** In addressing modes, offsets are 32-bit signed integers, even in 64-bit mode. The following function checks that an addressing mode is valid, i.e. that the offsets are in range. @@ -392,6 +420,8 @@ Definition eval_operation | Osubf, v1::v2::nil => Some(Val.subf v1 v2) | Omulf, v1::v2::nil => Some(Val.mulf v1 v2) | Odivf, v1::v2::nil => Some(Val.divf v1 v2) + | Omaxf, v1::v2::nil => Some (maxf v1 v2) + | Ominf, v1::v2::nil => Some (minf v1 v2) | Onegfs, v1::nil => Some(Val.negfs v1) | Oabsfs, v1::nil => Some(Val.absfs v1) | Oaddfs, v1::v2::nil => Some(Val.addfs v1 v2) @@ -564,6 +594,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osubf => (Tfloat :: Tfloat :: nil, Tfloat) | Omulf => (Tfloat :: Tfloat :: nil, Tfloat) | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) + | Omaxf => (Tfloat :: Tfloat :: nil, Tfloat) + | Ominf => (Tfloat :: Tfloat :: nil, Tfloat) | Onegfs => (Tsingle :: nil, Tsingle) | Oabsfs => (Tsingle :: nil, Tsingle) | Oaddfs => (Tsingle :: Tsingle :: nil, Tsingle) @@ -722,6 +754,8 @@ Proof with (try exact I; try reflexivity). destruct v0; destruct v1... destruct v0; destruct v1... destruct v0; destruct v1... + destruct v0; destruct v1... + destruct v0; destruct v1... destruct v0... destruct v0... destruct v0; destruct v1... @@ -1290,6 +1324,8 @@ Proof. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. + inv H4; inv H2; simpl; auto. inv H4; simpl; auto. inv H4; simpl; auto. inv H4; inv H2; simpl; auto. diff --git a/verilog/PrintOp.ml b/verilog/PrintOp.ml index 6aa4d450..ac2e8f49 100644 --- a/verilog/PrintOp.ml +++ b/verilog/PrintOp.ml @@ -147,6 +147,8 @@ let print_operation reg pp = function | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2 | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2 | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2 + | Omaxf, [r1;r2] -> fprintf pp "max(%a, %a)" reg r1 reg r2 + | Ominf, [r1;r2] -> fprintf pp "min(%a, %a)" reg r1 reg r2 | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1 | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1 | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2 diff --git a/verilog/SelectOp.v b/verilog/SelectOp.v index d477d7bd..889e43ae 100644 --- a/verilog/SelectOp.v +++ b/verilog/SelectOp.v @@ -1546,4 +1546,8 @@ Definition builtin_arg (e: expr) := (** Platform-specific known builtins *) Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := - None. + match b, args with + | BI_fmax, e1 ::: e2 ::: Enil => Some (Eop Omaxf (e1 ::: e2 ::: Enil)) + | BI_fmin, e1 ::: e2 ::: Enil => Some (Eop Ominf (e1 ::: e2 ::: Enil)) + | _, _ => None + end. diff --git a/verilog/SelectOp.vp b/verilog/SelectOp.vp index 31be8c32..99496ba1 100644 --- a/verilog/SelectOp.vp +++ b/verilog/SelectOp.vp @@ -579,4 +579,8 @@ Nondetfunction builtin_arg (e: expr) := (** Platform-specific known builtins *) Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := - None. + match b, args with + | BI_fmax, e1 ::: e2 ::: Enil => Some (Eop Omaxf (e1 ::: e2 ::: Enil)) + | BI_fmin, e1 ::: e2 ::: Enil => Some (Eop Ominf (e1 ::: e2 ::: Enil)) + | _, _ => None + end. diff --git a/verilog/SelectOpproof.v b/verilog/SelectOpproof.v index d8ab32a4..61cbf72b 100644 --- a/verilog/SelectOpproof.v +++ b/verilog/SelectOpproof.v @@ -1021,7 +1021,12 @@ Theorem eval_platform_builtin: platform_builtin_sem bf vl = Some v -> exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. Proof. - intros. discriminate. + intros until le. intros SEL ARGS SEM. + destruct bf; try discriminate. + - inv ARGS; try discriminate. inv H0; try discriminate. inv H2; try discriminate. + inv SEL. inv SEM. exists (minf v1 v0); split; auto. EvalOp. + - inv ARGS; try discriminate. inv H0; try discriminate. inv H2; try discriminate. + inv SEL. inv SEM. exists (maxf v1 v0); split; auto. EvalOp. Qed. End CMCONSTR. diff --git a/verilog/Stacklayout.v b/verilog/Stacklayout.v index de2a6f10..002b86bf 100644 --- a/verilog/Stacklayout.v +++ b/verilog/Stacklayout.v @@ -15,11 +15,13 @@ Require Import Coqlib. Require Import AST Memory Separation. Require Import Bounds. +Require Archi. Local Open Scope sep_scope. (** The general shape of activation records is as follows, from bottom (lowest offsets) to top: +- For the Win64 ABI: 32 reserved bytes - Space for outgoing arguments to function calls. - Back link to parent frame - Saved values of integer callee-save registers used by the function. @@ -29,11 +31,11 @@ Local Open Scope sep_scope. - Return address. *) -Definition fe_ofs_arg := 0. +Definition fe_ofs_arg := if Archi.win64 then 32 else 0. Definition make_env (b: bounds) : frame_env := let w := if Archi.ptr64 then 8 else 4 in - let olink := align (4 * b.(bound_outgoing)) w in (* back link *) + let olink := align (fe_ofs_arg + 4 * b.(bound_outgoing)) w in (* back link *) let ocs := olink + w in (* callee-saves *) let ol := align (size_callee_save_area b ocs) 8 in (* locals *) let ostkdata := align (ol + 4 * b.(bound_local)) 8 in (* stack data *) @@ -61,7 +63,7 @@ Proof. Local Opaque Z.add Z.mul sepconj range. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). - set (olink := align (4 * b.(bound_outgoing)) w). + set (olink := align (fe_ofs_arg + 4 * b.(bound_outgoing)) w). set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). @@ -69,8 +71,9 @@ Local Opaque Z.add Z.mul sepconj range. replace (size_chunk Mptr) with w by (rewrite size_chunk_Mptr; auto). assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia). assert (0 <= 4 * b.(bound_outgoing)) by lia. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). assert (olink + w <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). @@ -87,7 +90,7 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap45. rewrite sep_swap34. (* Apply range_split and range_split2 repeatedly *) - unfold fe_ofs_arg. + apply range_drop_left with 0. lia. apply range_split_2. fold olink. lia. lia. apply range_split. lia. apply range_split_2. fold ol. lia. lia. @@ -105,15 +108,16 @@ Lemma frame_env_range: Proof. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). - set (olink := align (4 * b.(bound_outgoing)) w). + set (olink := align (fe_ofs_arg + 4 * b.(bound_outgoing)) w). set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + assert (0 <= fe_ofs_arg) by (unfold fe_ofs_arg; destruct Archi.win64; lia). assert (0 <= 4 * b.(bound_outgoing)) by lia. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (fe_ofs_arg + 4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). assert (olink + w <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). @@ -133,14 +137,14 @@ Lemma frame_env_aligned: Proof. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). - set (olink := align (4 * b.(bound_outgoing)) w). + set (olink := align (fe_ofs_arg + 4 * b.(bound_outgoing)) w). set (ocs := olink + w). set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). set (oretaddr := align (ostkdata + b.(bound_stack_data)) w). assert (0 < w) by (unfold w; destruct Archi.ptr64; lia). replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto). - split. apply Z.divide_0_r. + split. exists (fe_ofs_arg / 8). unfold fe_ofs_arg; destruct Archi.win64; reflexivity. split. apply align_divides; lia. split. apply align_divides; lia. split. apply align_divides; lia. diff --git a/verilog/TargetPrinter.ml b/verilog/TargetPrinter.ml index 8950b8ca..91e0b18e 100644 --- a/verilog/TargetPrinter.ml +++ b/verilog/TargetPrinter.ml @@ -95,9 +95,6 @@ let z oc n = output_string oc (Z.to_string n) let data_pointer = if Archi.ptr64 then ".quad" else ".long" -(* The comment deliminiter *) -let comment = "#" - (* Base-2 log of a Caml integer *) let rec log2 n = assert (n > 0); @@ -106,6 +103,7 @@ let rec log2 n = (* System dependent printer functions *) module type SYSTEM = sig + val comment: string val raw_symbol: out_channel -> string -> unit val symbol: out_channel -> P.t -> unit val label: out_channel -> int -> unit @@ -124,6 +122,9 @@ module type SYSTEM = module ELF_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + let raw_symbol oc s = fprintf oc "%s" s @@ -131,7 +132,30 @@ module ELF_System : SYSTEM = let label = elf_label - let name_of_section = fun _ -> assert false + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + variable_section ~sec:".data" ~bss:".bss" i + | Section_const i | Section_small_const i -> + variable_section + ~sec:".section .rodata" + ~reloc:".section .data.rel.ro,\"aw\",@progbits" + i + | Section_string sz -> + elf_mergeable_string_section sz ".section .rodata" + | Section_literal sz -> + elf_mergeable_literal_section sz ".section .rodata" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",\"a%s%s\",@progbits" + s (if wr then "w" else "") (if ex then "x" else "") + | Section_debug_info _ -> ".section .debug_info,\"\",@progbits" + | Section_debug_loc -> ".section .debug_loc,\"\",@progbits" + | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" + | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" + | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits" + | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" let stack_alignment = 16 @@ -162,6 +186,10 @@ module ELF_System : SYSTEM = module MacOS_System : SYSTEM = struct + (* The comment delimiter. + `##` instead of `#` to please the Clang assembler. *) + let comment = "##" + let raw_symbol oc s = fprintf oc "_%s" s @@ -171,7 +199,28 @@ module MacOS_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = fun _ -> assert false + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + variable_section ~sec:".data" i + | Section_const i | Section_small_const i -> + variable_section ~sec:".const" ~reloc:".const_data" i + | Section_string sz -> + macos_mergeable_string_section sz + | Section_literal sz -> + macos_mergeable_literal_section sz + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\", %s, %s" + (if wr then "__DATA" else "__TEXT") s + (if ex then "regular, pure_instructions" else "regular") + | Section_debug_info _ -> ".section __DWARF,__debug_info,regular,debug" + | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug" + | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" + | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" + | Section_debug_ranges -> ".section __DWARF,__debug_ranges,regular,debug" + | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" + | Section_ais_annotation -> assert false (* Not supported under MacOS *) let stack_alignment = 16 (* mandatory *) @@ -202,8 +251,13 @@ module MacOS_System : SYSTEM = module Cygwin_System : SYSTEM = struct + (* The comment delimiter *) + let comment = "#" + + let symbol_prefix = "" + let raw_symbol oc s = - fprintf oc "_%s" s + fprintf oc "%s%s" symbol_prefix s let symbol oc symb = raw_symbol oc (extern_atom symb) @@ -211,21 +265,53 @@ module Cygwin_System : SYSTEM = let label oc lbl = fprintf oc "L%d" lbl - let name_of_section = fun _ -> assert false - - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + variable_section ~sec:".data" ~bss:".bss" i + | Section_const i | Section_small_const i -> + variable_section ~sec:".section .rdata,\"dr\"" i + | Section_string _ -> ".section .rdata,\"dr\"" + | Section_literal _ -> ".section .rdata,\"dr\"" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section %s, \"%s\"\n" + s (if ex then "xr" else if wr then "d" else "dr") + | Section_debug_info _ -> ".section .debug_info,\"dr\"" + | Section_debug_loc -> ".section .debug_loc,\"dr\"" + | Section_debug_line _ -> ".section .debug_line,\"dr\"" + | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" + | Section_debug_ranges -> ".section .debug_ranges,\"dr\"" + | Section_debug_str-> assert false (* Should not be used *) + | Section_ais_annotation -> assert false (* Not supported for coff binaries *) + + let stack_alignment = 8 let print_align oc n = fprintf oc " .balign %d\n" n + let indirect_symbols : StringSet.t ref = ref StringSet.empty + let print_mov_rs oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd + assert Archi.ptr64; + let s = extern_atom id in + indirect_symbols := StringSet.add s !indirect_symbols; + fprintf oc " movq .refptr.%s(%%rip), %a\n" s ireg rd let print_fun_info _ _ = () let print_var_info _ _ = () - let print_epilogue _ = () + let declare_indirect_symbol oc s = + fprintf oc " .section .rdata$.refptr.%s, \"dr\"\n" s; + fprintf oc " .globl .refptr.%s\n" s; + fprintf oc " .linkonce discard\n"; + fprintf oc ".refptr.%s:\n" s; + fprintf oc " .quad %s\n" s + + let print_epilogue oc = + StringSet.iter (declare_indirect_symbol oc) !indirect_symbols; + indirect_symbols := StringSet.empty let print_comm_decl oc name sz al = fprintf oc " .comm %a, %s, %d\n" @@ -233,7 +319,8 @@ module Cygwin_System : SYSTEM = let print_lcomm_decl oc name sz al = fprintf oc " .lcomm %a, %s, %d\n" - symbol name (Z.to_string sz) (log2 al) + symbol name (Z.to_string sz) + (if Archi.ptr64 then al else log2 al) end @@ -345,7 +432,9 @@ module Target(System: SYSTEM):TARGET = | Pmovq_ri(rd, n) -> let n1 = camlint64_of_coqint n in let n2 = Int64.to_int32 n1 in - if n1 = Int64.of_int32 n2 then + if Int64.shift_right_logical n1 32 = Int64.zero then + fprintf oc " movl $%Ld, %a\n" n1 ireg32 rd + else if n1 = Int64.of_int32 n2 then fprintf oc " movq $%ld, %a\n" n2 ireg64 rd else fprintf oc " movabsq $%Ld, %a\n" n1 ireg64 rd @@ -654,7 +743,7 @@ module Target(System: SYSTEM):TARGET = | Pret -> if (not Archi.ptr64) && (!current_function_sig).sig_cc.cc_structret then begin - fprintf oc " movl 0(%%esp), %%eax\n"; + fprintf oc " movl 4(%%esp), %%eax\n"; fprintf oc " ret $4\n" end else begin fprintf oc " ret\n" @@ -714,6 +803,8 @@ module Target(System: SYSTEM):TARGET = fprintf oc " minsd %a, %a\n" freg a1 freg res | Pmovb_rm (rd,a) -> fprintf oc " movb %a, %a\n" addressing a ireg8 rd + | Pmovq_rf (rd, r1) -> + fprintf oc " movq %a, %a\n" freg r1 ireg64 rd | Pmovsq_mr(a, rs) -> fprintf oc " movq %a, %a\n" freg rs addressing a | Pmovsq_rm(rd, a) -> @@ -765,11 +856,6 @@ module Target(System: SYSTEM):TARGET = assert false end - let print_literal64 oc n lbl = - fprintf oc "%a: .quad 0x%Lx\n" label lbl n - let print_literal32 oc n lbl = - fprintf oc "%a: .long 0x%lx\n" label lbl n - let print_jumptable oc jmptbl = let print_jumptable (lbl, tbl) = let print_entry l = @@ -797,15 +883,6 @@ module Target(System: SYSTEM):TARGET = let name_of_section = name_of_section - let emit_constants oc lit = - if exists_constants () then begin - section oc lit; - print_align oc 8; - Hashtbl.iter (print_literal64 oc) literal64_labels; - Hashtbl.iter (print_literal32 oc) literal32_labels; - reset_literals () - end - let cfi_startproc = cfi_startproc let cfi_endproc = cfi_endproc @@ -815,11 +892,6 @@ module Target(System: SYSTEM):TARGET = let print_optional_fun_info _ = () - let get_section_names name = - match C2C.atom_sections name with - | [t;l;j] -> (t, l, j) - | _ -> (Section_text, Section_literal, Section_jumptable) - let print_fun_info = print_fun_info let print_var_info = print_var_info @@ -832,7 +904,23 @@ module Target(System: SYSTEM):TARGET = end let print_epilogue oc = - assert false + if !need_masks then begin + section oc (Section_literal 16); + print_align oc 16; + fprintf oc "%a: .quad 0x8000000000000000, 0\n" + raw_symbol "__negd_mask"; + fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n" + raw_symbol "__absd_mask"; + fprintf oc "%a: .long 0x80000000, 0, 0, 0\n" + raw_symbol "__negs_mask"; + fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" + raw_symbol "__abss_mask" + end; + System.print_epilogue oc; + if !Clflags.option_g then begin + Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); + section oc Section_text; + end let comment = comment @@ -847,7 +935,7 @@ end let sel_target () = let module S = (val (match Configuration.system with | "linux" | "bsd" -> (module ELF_System:SYSTEM) - | "macosx" -> (module MacOS_System:SYSTEM) + | "macos" -> (module MacOS_System:SYSTEM) | "cygwin" -> (module Cygwin_System:SYSTEM) | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in (module Target(S):TARGET) diff --git a/verilog/ValueAOp.v b/verilog/ValueAOp.v index d0b8427a..298a1a58 100644 --- a/verilog/ValueAOp.v +++ b/verilog/ValueAOp.v @@ -143,6 +143,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osubf, v1::v2::nil => subf v1 v2 | Omulf, v1::v2::nil => mulf v1 v2 | Odivf, v1::v2::nil => divf v1 v2 + | Omaxf, v1::v2::nil => binop_float float_max v1 v2 + | Ominf, v1::v2::nil => binop_float float_min v1 v2 | Onegfs, v1::nil => negfs v1 | Oabsfs, v1::nil => absfs v1 | Oaddfs, v1::v2::nil => addfs v1 v2 @@ -258,6 +260,8 @@ Proof. destruct (propagate_float_constants tt); constructor. eapply eval_static_addressing_32_sound; eauto. eapply eval_static_addressing_64_sound; eauto. + apply binop_float_sound; auto. + apply binop_float_sound; auto. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. apply select_sound; auto. eapply eval_static_condition_sound; eauto. Qed. diff --git a/verilog/extractionMachdep.v b/verilog/extractionMachdep.v index a29553e8..26a3f0a7 100644 --- a/verilog/extractionMachdep.v +++ b/verilog/extractionMachdep.v @@ -6,24 +6,29 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) (* Additional extraction directives specific to the x86-64 port *) -Require SelectOp ConstpropOp. +Require Archi SelectOp. -(* SelectOp *) - -Extract Constant SelectOp.symbol_is_external => - "fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id". +(* Archi *) -(* ConstpropOp *) +Extract Constant Archi.win64 => + "match Configuration.system with + | ""cygwin"" when ptr64 -> true + | _ -> false". -Extract Constant ConstpropOp.symbol_is_external => - "fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id". +(* SelectOp *) +Extract Constant SelectOp.symbol_is_external => + "match Configuration.system with + | ""macos"" -> C2C.atom_is_extern + | ""cygwin"" when Archi.ptr64 -> C2C.atom_is_extern + | _ -> (fun _ -> false)". |