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
|
(* *********************************************************************)
(* *)
(* 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 =
let warn ty =
let msg = sprintf "expected register or memory cell but found %s for parameter '%s'" ty pos in
raise (Bad_parameter msg) in
match arg with
| BA_int _
| BA_long _ -> warn "constant"
| BA_float _
| BA_single _ -> assert false (* Should never occur and be avoided in C2C *)
| BA_addrstack ofs ->
warn "stack cell"
| BA_addrglobal(id, ofs) ->
warn "global address"
| BA_splitlong(hi, lo) ->
warn "register pair";
| BA_addptr(a1, a2) ->
warn "pointer computation"
| _ -> ()
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) ->
combine " * 0x100000000 + " hi lo
| BA_addptr(a1, a2) ->
combine " + " a1 a2
and combine mid arg1 arg2 =
let op_br = simple "("
and mid = simple mid
and cl_br = simple ")"
and arg1 = ais_arg arg1
and arg2 = ais_arg arg2 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][1-9][0-9]*\\|%here\\|\007"
let add_ais_annot 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 ->
let loc = loc_of_txt txt in
warning loc Wrong_ais_parameter "wrong ais parameter %s" s; []
in
let rec merge acc = function
| [] -> List.rev 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 annot = merge [] annot in
if annot <> [] then
ais_annot_list := (annot)::!ais_annot_list
let validate_ais_annot env loc txt args =
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
if Cutil.is_float_type env arg.C.etyp then
error loc "floating point types are not supported in ais annotations"
else if Cutil.is_volatile_variable env arg then
error loc "access to volatile variable '%a' is not supported in ais annotations" Cprint.exp (0,arg)
with _ ->
error loc "unknown parameter '%s'" s
in List.iter fragment (Str.full_split re_ais_annot_param txt)
|
