Skip to content
Snippets Groups Projects
Commit 4ccd7237 authored by xleroy's avatar xleroy
Browse files

Emit a few comments to help reading the generated asm

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1292 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 9976ed7a
No related branches found
No related tags found
No related merge requests found
...@@ -92,6 +92,11 @@ let label_high oc lbl = ...@@ -92,6 +92,11 @@ let label_high oc lbl =
| MacOS -> fprintf oc "ha16(L%d)" lbl | MacOS -> fprintf oc "ha16(L%d)" lbl
| Linux|Diab -> fprintf oc ".L%d@ha" lbl | Linux|Diab -> fprintf oc ".L%d@ha" lbl
let comment =
match target with
| MacOS|Linux -> ";"
| Diab -> "%"
let constant oc cst = let constant oc cst =
match cst with match cst with
| Cint n -> | Cint n ->
...@@ -118,7 +123,6 @@ let constant oc cst = ...@@ -118,7 +123,6 @@ let constant oc cst =
assert false assert false
end end
let num_crbit = function let num_crbit = function
| CRbit_0 -> 0 | CRbit_0 -> 0
| CRbit_1 -> 1 | CRbit_1 -> 1
...@@ -220,11 +224,12 @@ let is_builtin_function s = ...@@ -220,11 +224,12 @@ let is_builtin_function s =
Str.string_match re_builtin_function (extern_atom s) 0 Str.string_match re_builtin_function (extern_atom s) 0
let print_builtin_function oc s = let print_builtin_function oc s =
fprintf oc "%s begin %s\n" comment (extern_atom s);
(* int args: GPR3, GPR4 float args: FPR1, FPR2, FPR3 (* int args: GPR3, GPR4 float args: FPR1, FPR2, FPR3
int res: GPR3 float res: FPR1 int res: GPR3 float res: FPR1
Watch out for MacOSX/EABI incompatibility: functions that take Watch out for MacOSX/EABI incompatibility: functions that take
some floats then some ints. There are none here. *) some floats then some ints. There are none here. *)
match extern_atom s with begin match extern_atom s with
(* Volatile reads *) (* Volatile reads *)
| "__builtin_volatile_read_int8unsigned" -> | "__builtin_volatile_read_int8unsigned" ->
fprintf oc " lbz %a, 0(%a)\n" ireg GPR3 ireg GPR3 fprintf oc " lbz %a, 0(%a)\n" ireg GPR3 ireg GPR3
...@@ -305,6 +310,8 @@ let print_builtin_function oc s = ...@@ -305,6 +310,8 @@ let print_builtin_function oc s =
(* Catch-all *) (* Catch-all *)
| s -> | s ->
invalid_arg ("unrecognized builtin function " ^ s) invalid_arg ("unrecognized builtin function " ^ s)
end;
fprintf oc "%s end %s\n" comment (extern_atom s)
(* Printing of instructions *) (* Printing of instructions *)
...@@ -485,7 +492,8 @@ let print_instruction oc labels = function ...@@ -485,7 +492,8 @@ let print_instruction oc labels = function
let n = Int64.bits_of_float c in let n = Int64.bits_of_float c in
let nlo = Int64.to_int32 n let nlo = Int64.to_int32 n
and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo; fprintf oc "%a: .long 0x%lx, 0x%lx %s %.18g\n"
label lbl nhi nlo comment c;
section oc text section oc text
| Plfs(r1, c, r2) -> | Plfs(r1, c, r2) ->
fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2 fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2
...@@ -532,12 +540,9 @@ let print_instruction oc labels = function ...@@ -532,12 +540,9 @@ let print_instruction oc labels = function
fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c
| Prlwinm(r1, r2, c1, c2) -> | Prlwinm(r1, r2, c1, c2) ->
let (mb, me) = rolm_mask (camlint_of_coqint c2) in let (mb, me) = rolm_mask (camlint_of_coqint c2) in
fprintf oc " rlwinm %a, %a, %ld, %d, %d\n" fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n"
ireg r1 ireg r2 (camlint_of_coqint c1) mb me ireg r1 ireg r2 (camlint_of_coqint c1) mb me
(* comment (camlint_of_coqint c2)
fprintf oc " rlwinm %a, %a, %ld, 0x%lx\n"
ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2)
*)
| Pslw(r1, r2, r3) -> | Pslw(r1, r2, r3) ->
fprintf oc " slw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 fprintf oc " slw %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Psraw(r1, r2, r3) -> | Psraw(r1, r2, r3) ->
...@@ -772,13 +777,14 @@ let print_init oc = function ...@@ -772,13 +777,14 @@ let print_init oc = function
| Init_int32 n -> | Init_int32 n ->
fprintf oc " .long %ld\n" (camlint_of_coqint n) fprintf oc " .long %ld\n" (camlint_of_coqint n)
| Init_float32 n -> | Init_float32 n ->
fprintf oc " .long %ld\n" (Int32.bits_of_float n) fprintf oc " .long %ld %s %.18g\n" (Int32.bits_of_float n) comment n
| Init_float64 n -> | Init_float64 n ->
(* .quad not working on all versions of the MacOSX assembler *) (* .quad not working on all versions of the MacOSX assembler *)
let b = Int64.bits_of_float n in let b = Int64.bits_of_float n in
fprintf oc " .long %Ld, %Ld\n" fprintf oc " .long %Ld, %Ld %s %.18g\n"
(Int64.shift_right_logical b 32) (Int64.shift_right_logical b 32)
(Int64.logand b 0xFFFFFFFFL) (Int64.logand b 0xFFFFFFFFL)
comment n
| Init_space n -> | Init_space n ->
let n = camlint_of_z n in let n = camlint_of_z n in
if n > 0l then fprintf oc " .space %ld\n" n if n > 0l then fprintf oc " .space %ld\n" n
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment