blob: bd76878110d62eca2bcc37060d11a7dec61fd14e (
plain)
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
open AST
open Camlcoq
open Diagnostics
open Memdata
open Printf
type t =
| Label of int
| String of string
| Symbol of ident
let offset ofs =
let ofs = camlint_of_coqint ofs in
if ofs = 0l then "" else sprintf " + %ld" ofs
let size_chunk c =
sprintf "%ld" (camlint_of_coqint (size_chunk c))
let addr_global id ofs =
let addr_o = "("
and addr_e = sprintf "%s)" (offset ofs) in
[String addr_o;Symbol id;String addr_e]
exception Bad_parameter of string
let warn_lval_arg pos arg =
match arg with
| BA_int _
| BA_long _
| BA_addrstack _
| BA_addrglobal _
| BA_splitlong _
| BA_addptr _ ->
let msg = sprintf "expected register or memory cell for parameter '%s', skipping generation of ais annotation" pos in
raise (Bad_parameter msg)
| BA_float _
| BA_single _ -> assert false (* Should never occur and be avoided in C2C *)
| _ -> ()
let ais_expr_arg pos preg_string sp_reg_name arg =
let preg reg = sprintf "reg(\"%s\")" (preg_string reg)
and sp = sprintf "reg(\"%s\")" sp_reg_name
and simple s = [String s]
in
let rec ais_arg = function
| BA x -> simple (preg x)
| BA_int n -> simple (sprintf "%ld" (camlint_of_coqint n))
| BA_long n -> simple (sprintf "%Ld" (camlint64_of_coqint n))
| BA_float _
| BA_single _ -> assert false (* Should never occur and be avoided in C2C *)
| BA_loadstack(chunk, ofs) ->
let loadstack = sprintf "mem(%s%s, %s)" sp
(offset ofs)
(size_chunk chunk) in
simple loadstack
| BA_addrstack ofs ->
let addrstack = sprintf "(%s%s)" sp (offset ofs) in
simple addrstack
| BA_loadglobal(chunk, id, ofs) ->
let mem_o = "mem("
and mem_e = sprintf "%s, %s)"
(offset ofs)
(size_chunk chunk) in
[String mem_o;Symbol id;String mem_e]
| BA_addrglobal(id, ofs) ->
addr_global id ofs
| BA_splitlong(hi, lo) ->
let arg1 = combine " * " (ais_arg hi) (simple "0x100000000") in
combine " + " arg1 (ais_arg lo)
| BA_addptr(a1, a2) ->
let a1 = ais_arg a1
and a2 = ais_arg a2 in
combine " + " a1 a2
and combine mid arg1 arg2 =
let op_br = simple "("
and mid = simple mid
and cl_br = simple ")" in
op_br@arg1@mid@arg2@cl_br in
ais_arg arg
let ais_annot_list: (t list) list ref = ref []
let get_ais_annots () =
let annots = !ais_annot_list in
ais_annot_list := [];
List.rev annots
let re_loc_param = Str.regexp "# file:\\([^ ]+\\) line:\\([^ ]+\\)"
let loc_of_txt txt =
try
let pos = String.index txt '\n' in
let txt = String.sub txt 0 (pos -1) in
if Str.string_partial_match re_loc_param txt 0 then
let file = Str.matched_group 1 txt
and line = int_of_string (Str.matched_group 2 txt) in
file,line
else
no_loc
with _ ->
no_loc
let re_ais_annot_param = Str.regexp "%%\\|%[el][0-9]+\\|%here\\|\007"
let ais_annot_txt warn lbl preg_string sp_reg_name txt args =
let fragment = function
| Str.Delim "%here" ->
[Label lbl]
| Str.Text s ->
[String s]
| Str.Delim "%%" ->
[String "%"]
| Str.Delim "\007" ->
[String "\007\000"]
| Str.Delim s ->
let typ = String.get s 1
and n = int_of_string (String.sub s 2 (String.length s - 2)) in
let arg = List.nth args (n-1) in
begin match typ with
| 'e' -> ais_expr_arg s preg_string sp_reg_name arg
| 'l' -> warn_lval_arg s arg; ais_expr_arg s preg_string sp_reg_name arg
| _ -> assert false
end
in
let annot =
try
List.concat (List.map fragment (Str.full_split re_ais_annot_param txt))
with
| Bad_parameter s ->
if warn then begin
let loc = loc_of_txt txt in
warning loc Wrong_ais_parameter "wrong ais parameter: %s" s
end;
[]
in
let rec merge acc = function
| [] -> acc
| (Label _ as lbl):: rest -> merge (lbl::acc) rest
| (Symbol _ as sym) :: rest -> merge (sym::acc) rest
| String s1 :: String s2 :: rest ->
merge acc (String (s1 ^ s2) :: rest)
| String s:: rest -> merge ((String s)::acc) rest
in
let rev_annot = match merge [] annot with
| [] -> []
| (String s)::rest -> (String (s^"\n"))::rest
| rest -> (String "\n")::rest in
List.rev rev_annot
let add_ais_annot lbl preg_string sp_reg_name txt args =
let annot = ais_annot_txt true lbl preg_string sp_reg_name txt args in
if annot <> [] then
ais_annot_list := (annot)::!ais_annot_list
let json_ais_annot preg_string sp_reg_name txt args =
let txt = ais_annot_txt false 0 preg_string sp_reg_name txt args in
let t_to_json = function
| Label _ -> String "%here"
| String s -> let buf = Buffer.create (String.length s) in
String.iter (fun c ->
begin match c with
| '\\' | '"' -> Buffer.add_char buf '\\'
| _ -> () end;
Buffer.add_char buf c) s;
String (Buffer.contents buf)
| Symbol s -> Symbol s in
(List.map t_to_json txt)
let validate_ais_annot env loc txt args =
let used_params = Array.make (List.length args) false in
let fragment arg =
match arg with
| Str.Delim "%here"
| Str.Text _
| Str.Delim "%%"
| Str.Delim "\007" -> ()
| Str.Delim s ->
let n = int_of_string (String.sub s 2 (String.length s - 2)) in
try
let arg = List.nth args (n-1) in
Array.set used_params (n-1) true;
if Cutil.is_float_type env arg.C.etyp then
error loc "floating point types for parameter '%s' are not supported in ais annotations" s
else if Cutil.is_volatile_variable env arg then begin
let arg =
match arg.C.edesc with
| C.EVar id -> id.C.name
| _ -> assert false
in
error loc "access to volatile variable '%s' for parameter '%s' is not supported in ais annotations" arg s
end
with _ ->
error loc "unknown parameter '%s'" s
in List.iter fragment (Str.full_split re_ais_annot_param txt);
Array.iteri (fun pos used -> if not used then warning loc Unused_ais_parameter "unused parameter %d of ais annotation" pos) used_params
|
