aboutsummaryrefslogtreecommitdiffstats
path: root/x86
diff options
context:
space:
mode:
Diffstat (limited to 'x86')
-rw-r--r--x86/AsmToJSON.ml2
-rw-r--r--x86/AsmToJSON.mli2
-rw-r--r--x86/Asmexpand.ml8
-rw-r--r--x86/Asmgenproof.v2
-rw-r--r--x86/CBuiltins.ml8
-rw-r--r--x86/Conventions1.v20
-rw-r--r--x86/Machregs.v2
-rw-r--r--x86/Op.v2
-rw-r--r--x86/Stacklayout.v2
-rw-r--r--x86/TargetPrinter.ml93
10 files changed, 104 insertions, 37 deletions
diff --git a/x86/AsmToJSON.ml b/x86/AsmToJSON.ml
index ca18999a..8488bfde 100644
--- a/x86/AsmToJSON.ml
+++ b/x86/AsmToJSON.ml
@@ -15,3 +15,5 @@
(* Dummy function *)
let pp_program pp prog =
Format.fprintf pp "null"
+
+let pp_mnemonics pp = ()
diff --git a/x86/AsmToJSON.mli b/x86/AsmToJSON.mli
index e4d9c39a..058a4e83 100644
--- a/x86/AsmToJSON.mli
+++ b/x86/AsmToJSON.mli
@@ -11,3 +11,5 @@
(* *********************************************************************)
val pp_program: Format.formatter -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit
+
+val pp_mnemonics: Format.formatter -> unit
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 1b716165..9927d2fb 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -81,8 +81,8 @@ let sp_adjustment_64 sz =
(* Handling of annotations *)
-let expand_annot_val txt targ args res =
- emit (Pbuiltin (EF_annot(txt,[targ]), args, BR_none));
+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_rr (dst,src))
@@ -537,8 +537,8 @@ let expand_instruction instr =
expand_builtin_vstore chunk args
| EF_memcpy(sz, al) ->
expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
- | EF_annot_val(txt, targ) ->
- expand_annot_val txt targ args res
+ | EF_annot_val(kind,txt, targ) ->
+ expand_annot_val kind txt targ args res
| EF_annot _ | EF_debug _ | EF_inline_asm _ ->
emit instr
| _ ->
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index 6caf4531..38816fd2 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -825,7 +825,7 @@ Transparent destroyed_by_jumptable.
destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inv EQ1.
monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
unfold store_stack in *.
- exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
+ exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
intros [m1' [C D]].
exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto.
intros [m2' [F G]].
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index 09303223..69a2eb64 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -31,14 +31,8 @@ let builtins = {
];
Builtins.functions = [
(* Integer arithmetic *)
- "__builtin_bswap",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
"__builtin_bswap64",
(TInt(IULongLong, []), [TInt(IULongLong, [])], false);
- "__builtin_bswap32",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap16",
- (TInt(IUShort, []), [TInt(IUShort, [])], false);
"__builtin_clz",
(TInt(IInt, []), [TInt(IUInt, [])], false);
"__builtin_clzl",
@@ -52,8 +46,6 @@ let builtins = {
"__builtin_ctzll",
(TInt(IInt, []), [TInt(IULongLong, [])], false);
(* Float arithmetic *)
- "__builtin_fsqrt",
- (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
"__builtin_fmax",
(TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
"__builtin_fmin",
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index ecfb85bf..646c4afb 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -299,7 +299,7 @@ Proof.
assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_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 Zdivide_refl. }
+ { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. }
Opaque list_nth_z.
induction tyl; simpl loc_arguments_64; intros.
elim H.
@@ -339,10 +339,10 @@ Proof.
assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l).
{ unfold loc_argument_64_charact, loc_argument_acceptable.
destruct l as [r | [] ofs ty]; auto. intros [C|C]; auto.
- intros [C D]. split; auto. apply Zdivide_trans with 2; 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 Zdivide_0.
+ exploit loc_arguments_64_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).
@@ -360,7 +360,7 @@ Remark size_arguments_32_above:
Proof.
induction tyl; simpl; intros.
omega.
- apply Zle_trans with (ofs0 + typesize a); auto.
+ apply Z.le_trans with (ofs0 + typesize a); auto.
generalize (typesize_pos a); omega.
Qed.
@@ -376,21 +376,21 @@ Proof.
| None => size_arguments_64 tyl ir fr (ofs0 + 2)
end).
{ destruct (list_nth_z int_param_regs ir); eauto.
- apply Zle_trans with (ofs0 + 2); auto. omega. }
+ apply Z.le_trans with (ofs0 + 2); auto. omega. }
assert (B: ofs0 <=
match list_nth_z float_param_regs fr with
| Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
| None => size_arguments_64 tyl ir fr (ofs0 + 2)
end).
{ destruct (list_nth_z float_param_regs fr); eauto.
- apply Zle_trans with (ofs0 + 2); auto. omega. }
+ apply Z.le_trans with (ofs0 + 2); auto. omega. }
destruct a; auto.
Qed.
Lemma size_arguments_above:
forall s, size_arguments s >= 0.
Proof.
- intros; unfold size_arguments. apply Zle_ge.
+ intros; unfold size_arguments. apply Z.le_ge.
destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above].
Qed.
@@ -402,7 +402,7 @@ Proof.
induction tyl as [ | t l]; simpl; intros x IN.
- contradiction.
- rewrite in_app_iff in IN; destruct IN as [IN|IN].
-+ apply Zle_trans with (x + typesize t); [|apply size_arguments_32_above].
++ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above].
Ltac decomp :=
match goal with
| [ H: _ \/ _ |- _ ] => destruct H; decomp
@@ -437,7 +437,7 @@ Proof.
{ intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0.
- discriminate.
- eapply IHtyl; eauto.
- - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
+ - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
- eapply IHtyl; eauto. }
assert (B: forall ty0,
In (S Outgoing ofs ty) (regs_of_rpairs
@@ -454,7 +454,7 @@ Proof.
{ intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0.
- discriminate.
- eapply IHtyl; eauto.
- - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
+ - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
- eapply IHtyl; eauto. }
destruct a; eauto.
Qed.
diff --git a/x86/Machregs.v b/x86/Machregs.v
index 5d1b4515..bdf492ed 100644
--- a/x86/Machregs.v
+++ b/x86/Machregs.v
@@ -361,7 +361,7 @@ Definition builtin_constraints (ef: external_function) :
| EF_vload _ => OK_addressing :: nil
| EF_vstore _ => OK_addressing :: OK_default :: nil
| EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil
- | EF_annot txt targs => map (fun _ => OK_all) targs
+ | EF_annot kind txt targs => map (fun _ => OK_all) targs
| EF_debug kind txt targs => map (fun _ => OK_all) targs
| _ => nil
end.
diff --git a/x86/Op.v b/x86/Op.v
index 136c900b..02b04574 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1311,7 +1311,7 @@ Remark weak_valid_pointer_no_overflow_extends:
Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
Proof.
- intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2.
+ intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2.
Qed.
Remark valid_different_pointers_extends:
diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v
index 22c68099..d375febf 100644
--- a/x86/Stacklayout.v
+++ b/x86/Stacklayout.v
@@ -140,7 +140,7 @@ Proof.
set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto).
- split. apply Zdivide_0.
+ split. apply Z.divide_0_r.
split. apply align_divides; omega.
split. apply align_divides; omega.
split. apply align_divides; omega.
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 4a576df3..c19359fa 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -66,6 +66,11 @@ let preg oc = function
| FR r -> freg oc r
| _ -> assert false
+let preg_annot = function
+ | IR r -> if Archi.ptr64 then int64_reg_name r else int32_reg_name r
+ | FR r -> float_reg_name r
+ | _ -> assert false
+
let z oc n = output_string oc (Z.to_string n)
(* 32/64 bit dependencies *)
@@ -75,6 +80,11 @@ 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);
+ if n = 1 then 0 else 1 + log2 (n lsr 1)
+
(* System dependend printer functions *)
module type SYSTEM =
sig
@@ -121,6 +131,7 @@ module ELF_System : SYSTEM =
| 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
@@ -179,15 +190,11 @@ module MacOS_System : SYSTEM =
| 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 *)
- (* Base-2 log of a Caml integer *)
- let rec log2 n =
- assert (n > 0);
- if n = 1 then 0 else 1 + log2 (n lsr 1)
-
let print_align oc n =
fprintf oc " .align %d\n" (log2 n)
@@ -228,6 +235,63 @@ module MacOS_System : SYSTEM =
end
+(* Printer functions for Cygwin *)
+module Cygwin_System : SYSTEM =
+ struct
+
+ let raw_symbol oc s =
+ fprintf oc "_%s" s
+
+ let symbol oc symb =
+ raw_symbol oc (extern_atom symb)
+
+ let label oc lbl =
+ fprintf oc "L%d" lbl
+
+ let name_of_section = function
+ | Section_text -> ".text"
+ | Section_data i | Section_small_data i ->
+ if i then ".data" else "COMM"
+ | Section_const i | Section_small_const i ->
+ if i then ".section .rdata,\"dr\"" else "COMM"
+ | 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 (* minimum is 4, 8 is better for perfs *)
+
+ let print_align oc n =
+ fprintf oc " .balign %d\n" n
+
+ let print_mov_rs oc rd id =
+ fprintf oc " movl $%a, %a\n" symbol id ireg rd
+
+ let print_fun_info _ _ = ()
+
+ let print_var_info _ _ = ()
+
+ let print_epilogue _ = ()
+
+ let print_comm_decl oc name sz al =
+ fprintf oc " .comm %a, %s, %d\n"
+ symbol name (Z.to_string sz) (log2 al)
+
+ let print_lcomm_decl oc name sz al =
+ fprintf oc " .lcomm %a, %s, %d\n"
+ symbol name (Z.to_string sz) (log2 al)
+
+ end
+
module Target(System: SYSTEM):TARGET =
struct
@@ -735,11 +799,18 @@ module Target(System: SYSTEM):TARGET =
assert false
| Pbuiltin(ef, args, res) ->
begin match ef with
- | EF_annot(txt, targs) ->
- fprintf oc "%s annotation: " comment;
- print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args
+ | EF_annot(kind,txt, targs) ->
+ let annot =
+ begin match (P.to_int kind) with
+ | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args
+ | 2 -> let lbl = new_label () in
+ fprintf oc "%a: " label lbl;
+ ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args
+ | _ -> assert false
+ end in
+ fprintf oc "%s annotation: %S\n" comment annot
| EF_debug(kind, txt, targs) ->
- print_debug_info comment print_file_line preg "%esp" oc
+ print_debug_info comment print_file_line preg_annot "%esp" oc
(P.to_int kind) (extern_atom txt) args
| EF_inline_asm(txt, sg, clob) ->
fprintf oc "%s begin inline assembly\n\t" comment;
@@ -875,8 +946,8 @@ end
let sel_target () =
let module S = (val (match Configuration.system with
+ | "linux" | "bsd" -> (module ELF_System:SYSTEM)
| "macosx" -> (module MacOS_System:SYSTEM)
- | "linux"
- | "bsd" -> (module ELF_System:SYSTEM)
+ | "cygwin" -> (module Cygwin_System:SYSTEM)
| _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in
(module Target(S):TARGET)
generated by cgit (git 2.34.1) at 2024-06-29 14:06:24 +0000