Source file toplevel.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
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
(** Toplevel abstraction
There are two main differences with domains. First, transfer functions are
indexed by paths to enable a faster access. Second, transfer functions are
not partial functions and return always a result.
*)
open Mopsa_utils
open Core.All
open Sig.Combiner.Domain
(** Signature of the toplevel abstraction *)
module type TOPLEVEL =
sig
(** {2 Abstraction header} *)
(** ********************** *)
type t
val bottom: t
val top: t
val is_bottom: t -> bool
(** {2 Lattice operators} *)
(** ********************* *)
val subset: (t, t) man -> t ctx -> t -> t -> bool
val join: (t, t) man -> t ctx -> t -> t -> t
val meet: (t, t) man -> t ctx -> t -> t -> t
val widen: (t, t) man -> t ctx -> t -> t -> t
val merge : t -> t * teffect -> t * teffect -> t
(** {2 Transfer functions} *)
(** ********************** *)
val init : program -> (t, t) man -> t flow
val exec : ?route:route -> stmt -> (t, t) man -> t flow -> t post
val eval : ?route:route -> ?translate:semantic -> ?translate_when:(semantic*(expr->bool)) list -> expr -> (t, t) man -> t flow -> t eval
val ask : ?route:route -> (t,'r) query -> (t, t) man -> t flow -> (t, 'r) cases
(** {2 Pretty printing} *)
(** ******************* *)
val print_state : ?route:route -> printer -> t -> unit
val print_expr : ?route:route -> (t,t) man -> t flow -> printer -> expr -> unit
(** Exceptions *)
exception SysBreak of t flow
exception GoBackward
end
(** {2 Domain encapsulation into an abstraction} *)
let debug fmt = Debug.debug ~channel:"framework.abstraction.toplevel" fmt
(** Encapsulate a domain into a top-level abstraction *)
module Make(Domain:DOMAIN_COMBINER) : TOPLEVEL with type t = Domain.t
=
struct
let () = debug "routing table:@,%a" pp_routing_table Domain.routing_table
(** {2 Abstraction header} *)
(** ********************** *)
type t = Domain.t
let bottom = Domain.bottom
let top = Domain.top
let is_bottom = Domain.is_bottom
(** {2 Lattice operators} *)
(** ********************* *)
let subset man ctx a a' =
Domain.subset man ctx (a,a) (a',a')
let join man ctx a a' =
Domain.join man ctx (a,a) (a',a')
let meet man ctx a a' =
Domain.meet man ctx (a,a) (a',a')
let widen man ctx a a' =
Domain.widen man ctx (a,a) (a',a')
let merge = Domain.merge
(** {2 Caches and route maps} *)
(** **************************** *)
module Cache = Core.Cache.Make(struct type t = Domain.t end)
(** Map giving transfer functions of each route *)
module RouteMap = MapExt.Make(struct
type t = route
let compare = compare_route
end)
(** {2 Initialization} *)
(** ****************** *)
let init prog man : Domain.t flow =
let ctx =
singleton_ctx
Context.callstack_ctx_key
Callstack.empty_callstack
in
let flow0 = Flow.singleton ctx T_cur man.lattice.top in
let res = Domain.init prog man flow0 in
let () = Hook.init () in
let ctx = Hook.init_active_hooks (Flow.get_ctx res) in
Flow.set_ctx ctx res
(** {2 Statement execution} *)
(** *********************** *)
(** Build the map of exec functions *)
let exec_map : (stmt -> (t,t) man -> t flow -> t post option) RouteMap.t =
let map = RouteMap.singleton toplevel (Domain.exec None) in
get_routes Domain.routing_table |>
List.fold_left (fun map route ->
if RouteMap.mem route map then
map
else
let domains = resolve_route route Domain.routing_table in
RouteMap.add route (Domain.exec (Some domains)) map
) map
(** Hooks should not be activated within hooks exec/eval.
The flag [inside_hook_flag] is set whenever the analyzer emits a hook
event, in order to prevent subsequent exec/eval (i.e. called inside
the hook) to emit hook events.
*)
let inside_hook_flag = ref false
let inside_hook () = !inside_hook_flag
let enter_hook () = assert(not (inside_hook())); inside_hook_flag := true
let exit_hook () = assert(inside_hook ()); inside_hook_flag := false
exception SysBreak of Domain.t flow
exception GoBackward
let exec ?(route = toplevel) (stmt: stmt) man (flow: Domain.t flow) : Domain.t post =
let flow =
if inside_hook () then
flow
else
let () = enter_hook() in
let x = Hook.on_before_exec route stmt man flow in
let () = exit_hook() in
match x with None -> flow | Some ctx -> Flow.set_ctx ctx flow
in
let fexec =
try RouteMap.find route exec_map
with Not_found -> Exceptions.panic_at stmt.srange "exec for %a not found" pp_route route
in
try
let post =
match skind stmt with
| S_breakpoint _ ->
Post.return flow
| _ ->
match Cache.exec fexec route stmt man flow with
| None ->
if Flow.is_bottom man.lattice flow
then Post.return flow
else
Exceptions.panic_at stmt.srange
"unable to analyze statement %a in %a"
pp_stmt stmt
pp_route route
| Some post ->
let not_handled = Cases.exists (fun c flow ->
match c with
| NotHandled ->
not (Flow.is_bottom man.lattice flow)
| _ -> false
) post
in
if not_handled then
Exceptions.panic_at stmt.srange
"unable to analyze statement %a in %a"
pp_stmt stmt
pp_route route
;
post
in
let clean_post = exec_cleaners man post in
let minimized_post = Post.remove_duplicates man.lattice clean_post in
if inside_hook () then
minimized_post
else
let () = enter_hook() in
let x = Hook.on_after_exec route stmt man flow minimized_post in
let () = exit_hook () in
match x with None -> minimized_post | Some ctx -> Cases.set_ctx ctx minimized_post
with
| Exceptions.Panic(msg, line) ->
Printexc.raise_with_backtrace
(Exceptions.PanicAtFrame(stmt.srange, (Flow.get_callstack flow),msg, line))
(Printexc.get_raw_backtrace())
| Exceptions.PanicAtLocation(range, msg, line) ->
Printexc.raise_with_backtrace
(Exceptions.PanicAtFrame(range, (Flow.get_callstack flow),msg, line))
(Printexc.get_raw_backtrace())
| Sys.Break -> raise (SysBreak flow)
| Apron.Manager.Error exc ->
Printexc.raise_with_backtrace
(Exceptions.PanicAtFrame(stmt.srange, (Flow.get_callstack flow), Format.asprintf "Apron.Manager.Error(%a)" Apron.Manager.print_exclog exc, ""))
(Printexc.get_raw_backtrace())
| e when (match e with Exit | Exceptions.PanicAtFrame _ | SysBreak _ | GoBackward -> false | _ -> true) ->
Printexc.raise_with_backtrace
(Exceptions.PanicAtFrame(stmt.srange, (Flow.get_callstack flow), Printexc.to_string e, ""))
(Printexc.get_raw_backtrace())
(** {2 Evaluation of expressions} *)
(** ***************************** *)
(** Build the map of [eval] functions *)
let eval_map : (expr -> (t,t) man -> t flow -> t eval option) RouteMap.t =
let map = RouteMap.singleton toplevel (Domain.eval None) in
get_routes Domain.routing_table |>
List.fold_left (fun map route ->
if RouteMap.mem route map then
map
else
let domains = resolve_route route Domain.routing_table in
RouteMap.add route (Domain.eval (Some domains)) map
) map
(** Get the actual route of the expression in case of a
variable, since variable can have an intrinsic semantic *)
let refine_route_with_var_semantic route e =
if compare_route route toplevel = 0 then
match ekind e with
| E_var (v,_) -> Semantic v.vsemantic
| _ -> route
else
route
(** Evaluate sub-nodes of an expression and rebuild it *)
let eval_sub_expressions ?(route=toplevel) exp man flow =
let parts, builder = structure_of_expr exp in
match parts with
| {exprs = []; stmts = []} ->
Eval.singleton exp flow
| {exprs; stmts = []} ->
Cases.bind_list exprs (man.eval ~route) flow
>>$ fun exprs flow ->
let semantics =
List.fold_left
(fun acc e ->
SemanticSet.union acc
(SemanticMap.bindings e.etrans |> List.map fst |> SemanticSet.of_list)
) SemanticSet.empty exprs in
let exprs =
List.map
(SemanticSet.fold
(fun s e ->
if SemanticMap.mem s e.etrans then e else { e with etrans = SemanticMap.add s e e.etrans }
) semantics
) exprs in
let exp = builder {exprs; stmts = []} in
let etrans =
SemanticSet.fold
(fun s etrans ->
let exprs =
List.fold_left
(fun acc e -> SemanticMap.find s e.etrans :: acc)
[] exprs in
let exp = builder {exprs = List.rev exprs; stmts=[]} in
SemanticMap.add s exp etrans
) semantics SemanticMap.empty in
Eval.singleton { exp with etrans } flow
| _ -> Eval.singleton exp flow
(** Evaluate not-handled cases *)
let eval_not_handled ?(route=toplevel) exp man evl =
let handled,not_handled = Cases.partition (fun c flow -> match c with NotHandled -> false | _ -> true) evl in
let not_handled_ret =
match not_handled with
| None -> None
| Some evl ->
let evl =
Eval.remove_duplicates man.lattice evl >>= fun _ flow ->
eval_sub_expressions ~route exp man flow
in
Some evl
in
OptionExt.neutral2 Cases.join handled not_handled_ret |>
OptionExt.none_to_exn
(** Evaluation of expressions. *)
let eval ?(route=toplevel) ?(translate=any_semantic) ?(translate_when=[]) exp man flow =
let semantic =
if not (is_any_semantic translate) then
translate
else
match List.find_opt (fun (s,f) -> f exp) translate_when with
| Some (s,_) -> s
| None -> any_semantic
in
let flow =
if inside_hook () then flow
else
let () = enter_hook() in
let x = Hook.on_before_eval route semantic exp man flow in
let () = exit_hook() in
match x with
| None -> flow
| Some ctx -> Flow.set_ctx ctx flow
in
let route = refine_route_with_var_semantic route exp in
let feval =
try Cache.eval (RouteMap.find route eval_map) route
with Not_found -> Exceptions.panic_at exp.erange "eval for %a not found" pp_route route
in
let evl =
match feval exp man flow with
| None -> eval_sub_expressions exp man flow
| Some evl -> eval_not_handled ~route exp man evl
in
let ret =
Cases.map_result
(fun exp' ->
if exp == exp'
then exp'
else
let exp'' = { exp' with
ehistory = exp :: exp'.ehistory } in
{ exp'' with
etrans =
SemanticMap.map
(fun e ->
{ e with ehistory = e.ehistory @ exp''.ehistory }
) exp''.etrans }
) evl
in
(** Return a translation if it was requested *)
let ret' =
if is_any_semantic semantic
then ret
else Cases.map_result (get_expr_translation semantic) ret
in
if inside_hook () then ret'
else
let () = enter_hook() in
let x = Hook.on_after_eval route semantic exp man flow ret' in
let () = exit_hook () in
match x with
| None -> ret'
| Some ctx -> Cases.set_ctx ctx ret'
(** {2 Handler of queries} *)
(** ********************** *)
let ask : type r. ?route:route -> (t,r) query -> (t,t) man -> t flow -> (t, r) cases =
fun ?(route=toplevel) query man flow ->
let domains = if compare_route route toplevel = 0 then None else Some (resolve_route route Domain.routing_table) in
match Domain.ask domains query man flow with
| None -> raise Not_found
| Some r -> r
(** {2 Pretty printer of states} *)
(** **************************** *)
(** Build the map of [print_state] functions *)
let print_state_map : (printer -> t -> unit) RouteMap.t =
let map = RouteMap.singleton toplevel (Domain.print_state None) in
get_routes Domain.routing_table |>
List.fold_left (fun map route ->
if RouteMap.mem route map then
map
else
let domains = resolve_route route Domain.routing_table in
RouteMap.add route (Domain.print_state (Some domains)) map
) map
(** Pretty print of states *)
let print_state ?(route=toplevel) printer a =
match RouteMap.find_opt route print_state_map with
| Some f ->
f printer a
| None ->
Exceptions.panic "pretty printer for %a not found" pp_route route
(** {2 Pretty printer of expressions} *)
(** ********************************* *)
(** Build the map of [print_expr] functions *)
let print_expr_map : ((t,t) man -> t flow -> printer -> expr -> unit) RouteMap.t =
let map = RouteMap.singleton toplevel (Domain.print_expr None) in
get_routes Domain.routing_table |>
List.fold_left (fun map route ->
if RouteMap.mem route map then
map
else
let domains = resolve_route route Domain.routing_table in
RouteMap.add route (Domain.print_expr (Some domains)) map
) map
(** Pretty print of expression values *)
let print_expr ?(route=toplevel) man flow printer exp =
if Print.mem_printed_expr printer exp then () else
let route = refine_route_with_var_semantic route exp in
match RouteMap.find_opt route print_expr_map with
| Some f ->
Print.add_printed_expr printer exp;
f man flow printer exp
| None ->
Exceptions.panic_at exp.erange "pretty printer for %a not found" pp_route route
end