Source file scoping.ml
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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
(** Resolve variables scope and give unique identifiers accordingly. *)
open Mopsa_utils
open Location
open Cst
let debug fmt = Debug.debug ~channel:"c_stubs_parser.passes.scoping" fmt
module Scope =
struct
include SetExt.Make(struct type t = var let compare v1 v2 = compare v1.vname v2.vname end)
let uid_counter = ref 100000
let create v t s =
incr uid_counter;
let v' = {
vname = v.vname;
vuid = !uid_counter;
vlocal = true;
vrange = v.vrange;
vtyp = t;
} in
let s' = remove v' s |>
add v'
in
v', s'
let resolve v s =
match find_opt v s with
| None -> v
| Some vv -> vv
end
let rec visit_list f l scope =
match l with
| [] -> [], scope
| hd :: tl ->
let hd', scope' = f hd scope in
let tl', scope'' = visit_list f tl scope' in
hd' :: tl', scope''
let visit_option f o scope =
match o with
| None -> None, scope
| Some x ->
let x, scope = f x scope in
Some x, scope
let rec visit_expr (e:expr with_range) scope =
bind_pair_range e @@ fun expr ->
match expr with
| E_top _ | E_int _ | E_float _ | E_invalid
| E_string _ | E_char _ | E_return ->
expr, scope
| E_var v ->
E_var (Scope.resolve v scope), scope
| E_unop(op, e) ->
let e, scope = visit_expr e scope in
E_unop(op, e), scope
| E_binop (op, e1, e2) ->
let e1, scope = visit_expr e1 scope in
let e2, scope = visit_expr e2 scope in
E_binop (op, e1, e2), scope
| E_addr_of e ->
let e, scope = visit_expr e scope in
E_addr_of e, scope
| E_deref e ->
let e, scope = visit_expr e scope in
E_deref e, scope
| E_cast (t, e) ->
let e, scope = visit_expr e scope in
E_cast (t, e), scope
| E_subscript (a, i) ->
let a, scope = visit_expr a scope in
let i, scope = visit_expr i scope in
E_subscript (a, i), scope
| E_member (s, f) ->
let s, scope = visit_expr s scope in
E_member (s, f), scope
| E_arrow (p, f) ->
let p, scope = visit_expr p scope in
E_arrow (p, f), scope
| E_conditional (c, e1, e2) ->
let c, scope = visit_expr c scope in
let e1, scope = visit_expr e1 scope in
let e2, scope = visit_expr e2 scope in
E_conditional (c, e1, e2), scope
| E_builtin_call (f, args) ->
let args, scope = visit_list visit_expr args scope in
E_builtin_call (f, args), scope
| E_sizeof_type t ->
E_sizeof_type t, scope
| E_sizeof_expr e ->
let e, scope = visit_expr e scope in
E_sizeof_expr e, scope
| E_raise msg ->
E_raise msg, scope
let visit_interval i scope =
let lb, scope = visit_expr i.itv_lb scope in
let ub, scope = visit_expr i.itv_ub scope in
let i = { i with
itv_lb = lb;
itv_ub = ub; } in
i, scope
let visit_set (set:set) scope =
match set with
| S_interval itv ->
let itv, scope = visit_interval itv scope in
S_interval itv, scope
| S_resource r -> S_resource r, scope
let rec visit_formula (f:formula with_range) scope =
bind_pair_range f @@ fun formula ->
match formula with
| F_expr e ->
let e, scope = visit_expr e scope in
F_expr e, scope
| F_bool _ -> formula, scope
| F_binop (op, f1, f2) ->
let f1, scope = visit_formula f1 scope in
let f2, scope = visit_formula f2 scope in
F_binop (op, f1, f2), scope
| F_not f ->
let f, scope = visit_formula f scope in
F_not f, scope
| F_forall (v, t, s, f) ->
let v, scope' = Scope.create v t scope in
let f, scope' = visit_formula f scope' in
let s, _ = visit_set s scope in
F_forall (v, t, s, f), scope
| F_exists (v, t, s, f) ->
let v, scope' = Scope.create v t scope in
let f, scope' = visit_formula f scope' in
let s, _ = visit_set s scope in
F_exists (v, t, s, f), scope
| F_in (e, s) ->
let e, scope = visit_expr e scope in
let s, scope = visit_set s scope in
F_in (e, s), scope
| F_otherwise (f, e) ->
let f, scope = visit_formula f scope in
let e, scope = visit_expr e scope in
F_otherwise (f, e), scope
| F_if (cond, fthen, felse) ->
let cond, scope = visit_formula cond scope in
let fthen, scope = visit_formula fthen scope in
let felse, scope = visit_formula felse scope in
F_if (cond, fthen, felse), scope
let visit_requires requires scope =
bind_pair_range requires @@ fun requires ->
visit_formula requires scope
let visit_assumes assumes scope =
bind_pair_range assumes @@ fun assumes ->
visit_formula assumes scope
let visit_ensures ensures scope =
bind_pair_range ensures @@ fun ensures ->
visit_formula ensures scope
let visit_assigns assigns scope =
bind_pair_range assigns @@ fun assigns ->
let assign_target, scope = visit_expr assigns.assign_target scope in
let assign_offset, scope = visit_list visit_interval assigns.assign_offset scope in
{ assign_target; assign_offset }, scope
let visit_free free scope =
bind_pair_range free @@ fun free ->
visit_expr free scope
let visit_local_value lv scope =
match lv with
| L_new rc -> lv, scope
| L_call (f, args) ->
let f = bind_range f @@ fun ff -> Scope.resolve ff scope in
let args, scope = visit_list visit_expr args scope in
L_call (f, args), scope
let visit_local local scope =
bind_pair_range local @@ fun local ->
let lval, scope = visit_local_value local.lval scope in
let lvar, scope = Scope.create local.lvar local.ltyp scope in
{ lvar; ltyp = local.ltyp; lval }, scope
let visit_leaf leaf scope =
match leaf with
| S_local local ->
let local, scope = visit_local local scope in
S_local local, scope
| S_assumes assumes ->
let assumes, scope = visit_assumes assumes scope in
S_assumes assumes, scope
| S_requires requires ->
let requires, scope = visit_requires requires scope in
S_requires requires, scope
| S_assigns assigns ->
let assigns, scope = visit_assigns assigns scope in
S_assigns assigns, scope
| S_ensures ensures ->
let ensures, scope = visit_ensures ensures scope in
S_ensures ensures, scope
| S_free free ->
let free, scope = visit_free free scope in
S_free free, scope
| S_message msg ->
S_message msg, scope
let visit_case case scope =
bind_pair_range case @@ fun case ->
let body, scope' = visit_list visit_leaf case.case_body scope in
let case = {
case_label = case.case_label;
case_body = body;
}
in
case, scope
let visit_section sect scope =
match sect with
| S_leaf leaf ->
let leaf, scope = visit_leaf leaf scope in
S_leaf leaf, scope
| S_case case ->
let case, scope = visit_case case scope in
S_case case, scope
(** {2 Entry point} *)
(** *************** *)
let doit (stub: stub) : stub =
bind_range stub @@ fun sections ->
let scope = Scope.empty in
let stub', _ = visit_list visit_section sections scope in
stub'