diff options
| -rwxr-xr-x | configure | 16 | ||||
| -rw-r--r-- | ia32/Asm.v | 2 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 8 | ||||
| -rw-r--r-- | ia32/Machregs.v | 2 | ||||
| -rw-r--r-- | ia32/TargetPrinter.ml | 69 | ||||
| -rw-r--r-- | runtime/x86_64/vararg.S | 2 |
6 files changed, 68 insertions, 31 deletions
@@ -340,6 +340,22 @@ if test "$arch" = "ia32" -a "$model" = "64"; then struct_return="ref" # to check! system="linux" ;; + macosx) + # kernel major versions count upwards from 4 for OSX 10.0 to 15 for OSX 10.11 + kernel_major=`uname -r | cut -d "." -f 1` + + abi="macosx" + casm="${toolprefix}gcc" + casm_options="-arch x86_64 -c" + cc="${toolprefix}gcc -arch x86_64" + clinker="${toolprefix}gcc" + cprepro="${toolprefix}gcc" + cprepro_options="-std=c99 -arch x86_64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' -E" + libmath="" + struct_passing="ref-callee" # wrong! + struct_return="ref" # to check! + system="macosx" + ;; *) echo "Error: invalid eabi/system '$target' for architecture X86_64." 1>&2 echo "$usage" 1>&2 @@ -913,7 +913,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Vint n => match list_nth_z tbl (Int.unsigned n) with | None => Stuck - | Some lbl => goto_label f lbl rs m + | Some lbl => goto_label f lbl (rs #RAX <- Vundef #RDX <- Vundef) m end | _ => Stuck end diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 79602e52..e56dc429 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -779,16 +779,18 @@ Opaque loadind. inv AT. monadInv H6. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H5); intro NOOV. - exploit find_label_goto_label; eauto. + set (rs1 := rs0 #RAX <- Vundef #RDX <- Vundef). + exploit (find_label_goto_label f tf lbl rs1); eauto. intros [tc' [rs' [A [B C]]]]. exploit ireg_val; eauto. rewrite H. intros LD; inv LD. left; econstructor; split. apply plus_one. econstructor; eauto. eapply find_instr_tail; eauto. - simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eauto. + simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. Transparent destroyed_by_jumptable. - simpl. eapply agree_exten; eauto. intros. rewrite C; auto with asmgen. + apply agree_undef_regs with rs0; auto. + simpl; intros. destruct H8. rewrite C by auto with asmgen. unfold rs1; Simplifs. congruence. - (* Mreturn *) diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 034fa4bb..c3cdaefb 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -157,7 +157,7 @@ Definition destroyed_by_cond (cond: condition): list mreg := nil. Definition destroyed_by_jumptable: list mreg := - nil. + AX :: DX :: nil. Fixpoint destroyed_by_clobber (cl: list string): list mreg := match cl with diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index bd872f1e..33d47830 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -71,10 +71,8 @@ let z oc n = output_string oc (Z.to_string n) (* 32/64 bit dependencies *) -let size_pointer = if Archi.ptr64 then 8 else 4 let data_pointer = if Archi.ptr64 then ".quad" else ".long" - (* The comment deliminiter *) let comment = "#" @@ -292,7 +290,7 @@ module Target(System: SYSTEM):TARGET = let section oc sec = fprintf oc " %s\n" (name_of_section sec) -(* Emit a align directive *) +(* For "abs" and "neg" FP operations *) let need_masks = ref false @@ -301,15 +299,13 @@ module Target(System: SYSTEM):TARGET = let print_file_line oc file line = print_file_line oc comment file line -(* Built-in functions *) +(* In 64-bit mode use RIP-relative addressing to designate labels *) -(* Built-ins. They come in two flavors: - - annotation statements: take their arguments in registers or stack - locations; generate no code; - - inlined by the compiler: take their arguments in arbitrary - registers; preserve all registers except RCX, RDX, XMM6 and XMM7. *) + let rip_rel = + if Archi.ptr64 then "(%rip)" else "" -(* Hack for large 64-bit immediates *) +(* Large 64-bit immediates (bigger than a 32-bit signed integer) are + not supported by the processor. Turn them into memory operands. *) let intconst64 oc n = let n1 = camlint64_of_coqint n in @@ -324,6 +320,8 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%a(%%rip)" label lbl end + + (* Printing of instructions *) (* Reminder on AT&T syntax: op source, dest *) @@ -366,7 +364,9 @@ module Target(System: SYSTEM):TARGET = | Pmovsd_fi(rd, n) -> let b = camlint64_of_coqint (Floats.Float.to_bits n) in let lbl = new_label() in - fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat n); + fprintf oc " movsd %a%s, %a %s %.18g\n" + label lbl rip_rel + freg rd comment (camlfloat_of_coqfloat n); float64_literals := (lbl, b) :: !float64_literals | Pmovsd_fm(rd, a) | Pmovsd_fm_a(rd, a) -> fprintf oc " movsd %a, %a\n" addressing a freg rd @@ -375,7 +375,9 @@ module Target(System: SYSTEM):TARGET = | Pmovss_fi(rd, n) -> let b = camlint_of_coqint (Floats.Float32.to_bits n) in let lbl = new_label() in - fprintf oc " movss %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat32 n); + fprintf oc " movss %a%s, %a %s %.18g\n" + label lbl rip_rel + freg rd comment (camlfloat_of_coqfloat32 n); float32_literals := (lbl, b) :: !float32_literals | Pmovss_fm(rd, a) -> fprintf oc " movss %a, %a\n" addressing a freg rd @@ -576,10 +578,12 @@ module Target(System: SYSTEM):TARGET = fprintf oc " divsd %a, %a\n" freg r1 freg rd | Pnegd (rd) -> need_masks := true; - fprintf oc " xorpd %a, %a\n" raw_symbol "__negd_mask" freg rd + fprintf oc " xorpd %a%s, %a\n" + raw_symbol "__negd_mask" rip_rel freg rd | Pabsd (rd) -> need_masks := true; - fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg rd + fprintf oc " andpd %a%s, %a\n" + raw_symbol "__absd_mask" rip_rel freg rd | Pcomisd_ff(r1, r2) -> fprintf oc " comisd %a, %a\n" freg r2 freg r1 | Pxorpd_f (rd) -> @@ -594,10 +598,12 @@ module Target(System: SYSTEM):TARGET = fprintf oc " divss %a, %a\n" freg r1 freg rd | Pnegs (rd) -> need_masks := true; - fprintf oc " xorpd %a, %a\n" raw_symbol "__negs_mask" freg rd + fprintf oc " xorpd %a%s, %a\n" + raw_symbol "__negs_mask" rip_rel freg rd | Pabss (rd) -> need_masks := true; - fprintf oc " andpd %a, %a\n" raw_symbol "__abss_mask" freg rd + fprintf oc " andpd %a%s, %a\n" + raw_symbol "__abss_mask" rip_rel freg rd | Pcomiss_ff(r1, r2) -> fprintf oc " comiss %a, %a\n" freg r2 freg r1 | Pxorps_f (rd) -> @@ -620,8 +626,17 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%a:\n" label l' | Pjmptbl(r, tbl) -> let l = new_label() in - fprintf oc " jmp *%a(, %a, %d)\n" label l ireg r size_pointer; - jumptables := (l, tbl) :: !jumptables + jumptables := (l, tbl) :: !jumptables; + if Archi.ptr64 then begin + let (tmp1, tmp2) = + if r = RAX then (RDX, RAX) else (RAX, RDX) in + fprintf oc " leaq %a(%%rip), %a\n" label l ireg tmp1; + fprintf oc " movslq (%a, %a, 4), %a\n" ireg tmp1 ireg r ireg tmp2; + fprintf oc " addq %a, %a\n" ireg tmp2 ireg tmp1; + fprintf oc " jmp *%a\n" ireg tmp1 + end else begin + fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r + end | Pcall_s(f, sg) -> fprintf oc " call %a\n" symbol f; if (not Archi.ptr64) && sg.sig_cc.cc_structret then @@ -741,16 +756,20 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%a: .long 0x%lx\n" label lbl n let print_jumptable oc jmptbl = - let print_jumptable oc (lbl, tbl) = + let print_jumptable (lbl, tbl) = + let print_entry l = + if Archi.ptr64 then + fprintf oc " .long %a - %a\n" label (transl_label l) label lbl + else + fprintf oc " .long %a\n" label (transl_label l) + in fprintf oc "%a:" label lbl; - List.iter - (fun l -> fprintf oc " %s %a\n" - data_pointer label (transl_label l)) - tbl in + List.iter print_entry tbl + in if !jumptables <> [] then begin section oc jmptbl; - print_align oc size_pointer; - List.iter (print_jumptable oc) !jumptables; + print_align oc 4; + List.iter print_jumptable !jumptables; jumptables := [] end diff --git a/runtime/x86_64/vararg.S b/runtime/x86_64/vararg.S index 3e645474..9c0d787b 100644 --- a/runtime/x86_64/vararg.S +++ b/runtime/x86_64/vararg.S @@ -117,7 +117,7 @@ FUNCTION(__compcert_va_float64) ENDFUNCTION(__compcert_va_float64) FUNCTION(__compcert_va_composite) - jmp __compcert_va_int64 // by-ref convention, FIXME + jmp GLOB(__compcert_va_int64) // by-ref convention, FIXME ENDFUNCTION(__compcert_va_composite) // Save integer and FP registers at beginning of vararg function |