aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmexpand.ml
diff options
context:
space:
mode:
Diffstat (limited to 'arm/Asmexpand.ml')
-rw-r--r--arm/Asmexpand.ml37
1 files changed, 29 insertions, 8 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index d13015ff..2b19cbe8 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -106,7 +106,7 @@ let memcpy_small_arg sz arg tmp =
assert false
let expand_builtin_memcpy_small sz al src dst =
- let (tsrc, tdst) =
+ let (tsrc, tdst) =
if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
let (rdst, odst) = memcpy_small_arg sz dst tdst in
@@ -142,7 +142,7 @@ let memcpy_big_arg arg tmp =
let expand_builtin_memcpy_big sz al src dst =
assert (sz >= al);
assert (sz mod al = 0);
- let (s, d) =
+ let (s, d) =
if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
memcpy_big_arg src s;
memcpy_big_arg dst d;
@@ -377,7 +377,7 @@ let expand_instruction instr =
| Pbuiltin (ef,args,res) ->
begin match ef with
| EF_builtin (name,sg) ->
- expand_builtin_inline (extern_atom name) args res
+ expand_builtin_inline (camlstring_of_coqstring name) args res
| EF_vload chunk ->
expand_builtin_vload chunk args res
| EF_vstore chunk ->
@@ -395,17 +395,38 @@ let expand_instruction instr =
| _ ->
emit instr
-let expand_function fn =
+let int_reg_to_dwarf = function
+ | IR0 -> 0 | IR1 -> 1 | IR2 -> 2 | IR3 -> 3
+ | IR4 -> 4 | IR5 -> 5 | IR6 -> 6 | IR7 -> 7
+ | IR8 -> 8 | IR9 -> 9 | IR10 -> 10 | IR11 -> 11
+ | IR12 -> 12 | IR13 -> 13 | IR14 -> 14
+
+let float_reg_to_dwarf = function
+ | FR0 -> 64 | FR1 -> 65 | FR2 -> 66 | FR3 -> 67
+ | FR4 -> 68 | FR5 -> 69 | FR6 -> 70 | FR7 -> 71
+ | FR8 -> 72 | FR9 -> 73 | FR10 -> 74 | FR11 -> 75
+ | FR12 -> 76 | FR13 -> 77 | FR14 -> 78 | FR15 -> 79
+
+let preg_to_dwarf = function
+ | IR r -> int_reg_to_dwarf r
+ | FR r -> float_reg_to_dwarf r
+ | _ -> assert false
+
+
+let expand_function id fn =
try
set_current_function fn;
- List.iter expand_instruction fn.fn_code;
+ if !Clflags.option_g then
+ expand_debug id 13 preg_to_dwarf expand_instruction fn.fn_code
+ else
+ List.iter expand_instruction fn.fn_code;
Errors.OK (get_current_function ())
with Error s ->
Errors.Error (Errors.msg (coqstring_of_camlstring s))
-let expand_fundef = function
+let expand_fundef id = function
| Internal f ->
- begin match expand_function f with
+ begin match expand_function id f with
| Errors.OK tf -> Errors.OK (Internal tf)
| Errors.Error msg -> Errors.Error msg
end
@@ -413,4 +434,4 @@ let expand_fundef = function
Errors.OK (External ef)
let expand_program (p: Asm.program) : Asm.program Errors.res =
- AST.transform_partial_program expand_fundef p
+ AST.transform_partial_ident_program expand_fundef p