aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmexpand.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-09 11:06:24 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-09 11:06:24 +0200
commit0ffd562ae1941e37471ac0c2b8f93bed1de26441 (patch)
tree2ac8382fa3a37568f32d27dbc3291c8cd97f13e2 /arm/Asmexpand.ml
parentf0a5038b4e4220300637d3e9e918d9ec31623108 (diff)
downloadcompcert-kvx-0ffd562ae1941e37471ac0c2b8f93bed1de26441.tar.gz
compcert-kvx-0ffd562ae1941e37471ac0c2b8f93bed1de26441.zip
Filled in the rest of the funciton needed for thte debug info under arm.
The name_of_section function no returns the correct name for the debug sections, the prologue and epilogue directives are added and the labels for the live ranges are introduced in the Asmexpand pass.
Diffstat (limited to 'arm/Asmexpand.ml')
-rw-r--r--arm/Asmexpand.ml50
1 files changed, 46 insertions, 4 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index da08bf7c..b5bbc664 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -395,17 +395,59 @@ 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_int = function
+ | IR r -> int_reg_to_dwarf r
+ | FR r -> float_reg_to_dwarf r
+ | _ -> assert false
+
+let translate_annot annot =
+ let rec aux = function
+ | BA x -> Some (13,BA (preg_to_dwarf_int x))
+ | BA_int _
+ | BA_long _
+ | BA_float _
+ | BA_single _
+ | BA_loadglobal _
+ | BA_addrglobal _
+ | BA_loadstack _ -> None
+ | BA_addrstack ofs -> Some (13,BA_addrstack ofs)
+ | BA_splitlong (hi,lo) ->
+ begin
+ match (aux hi,aux lo) with
+ | Some (_,hi) ,Some (_,lo) -> Some (13,BA_splitlong (hi,lo))
+ | _,_ -> None
+ end in
+ (match annot with
+ | [] -> None
+ | a::_ -> aux a)
+
+
+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 translate_annot 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