1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Util functions used for the expansion of built-ins and some
pseudo-instructions *)
open Asm
open AST
open Camlcoq
(* Buffering the expanded code *)
let current_code = ref ([]: instruction list)
let emit i = current_code := i :: !current_code
(* Generation of fresh labels *)
let dummy_function = { fn_code = []; fn_sig = signature_main }
let current_function = ref dummy_function
let next_label = ref (None: label option)
let new_label () =
let lbl =
match !next_label with
| Some l -> l
| None ->
(* on-demand computation of the next available label *)
List.fold_left
(fun next instr ->
match instr with
| Plabel l -> if P.lt l next then next else P.succ l
| _ -> next)
P.one (!current_function).fn_code
in
next_label := Some (P.succ lbl);
lbl
let set_current_function f =
current_function := f; next_label := None; current_code := []
let get_current_function () =
let c = List.rev !current_code in
let fn = !current_function in
set_current_function dummy_function;
{fn with fn_code = c}
(* Expand function for debug information *)
let expand_scope id lbl oldscopes newscopes =
let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes
and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in
List.iter (fun i -> Debug.open_scope id i lbl) opening;
List.iter (fun i -> Debug.close_scope id i lbl) closing
let expand_debug id annot simple l =
let get_lbl = function
| None ->
let lbl = new_label () in
emit (Plabel lbl);
lbl
| Some lbl -> lbl in
let rec aux lbl scopes = function
| [] -> let lbl = get_lbl lbl in
Debug.function_end id lbl
| (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
let kind = (P.to_int kind) in
begin
match kind with
| 1->
emit i;aux lbl scopes rest
| 2 ->
aux lbl scopes rest
| 3 ->
begin
match annot args with
| Some a ->
let lbl = get_lbl lbl in
Debug.start_live_range (id,txt) lbl a;
aux (Some lbl) scopes rest
| None -> aux lbl scopes rest
end
| 4 ->
let lbl = get_lbl lbl in
Debug.end_live_range (id,txt) lbl;
aux (Some lbl) scopes rest
| 5 ->
begin
match annot args with
| Some a->
Debug.stack_variable (id,txt) a;
aux lbl scopes rest
| _ -> aux lbl scopes rest
end
| 6 ->
let lbl = get_lbl lbl in
let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in
expand_scope id lbl scopes scopes';
aux (Some lbl) scopes' rest
| _ ->
aux None scopes rest
end
| i::rest -> simple i; aux None scopes rest in
(* We need to move all closing debug annotations before the last real statement *)
let rec move_debug acc bcc = function
| (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest ->
let kind = (P.to_int kind) in
if kind = 1 then
move_debug acc (i::bcc) rest (* Do not move debug line *)
else
move_debug (i::acc) bcc rest (* Move the debug annotations forward *)
| b::rest -> List.rev ((List.rev (b::bcc)@List.rev acc)@rest) (* We found the first non debug location *)
| [] -> List.rev acc (* This actually can never happen *) in
aux None [] (move_debug [] [] (List.rev l))
|
