package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2019 The MOPSA Project.                               *)
(*                                                                          *)
(* This program is free software: you can redistribute it and/or modify     *)
(* it under the terms of the GNU Lesser General Public License as published *)
(* by the Free Software Foundation, either version 3 of the License, or     *)
(* (at your option) any later version.                                      *)
(*                                                                          *)
(* This program is distributed in the hope that it will be useful,          *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of           *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the            *)
(* GNU Lesser General Public License for more details.                      *)
(*                                                                          *)
(* You should have received a copy of the GNU Lesser General Public License *)
(* along with this program.  If not, see <http://www.gnu.org/licenses/>.    *)
(*                                                                          *)
(****************************************************************************)

(** 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


(* {2 Scope definition} *)
(* ******************** *)

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

(* {2 Visitors} *)
(* ************ *)

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'