Source file operational_inputs.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
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
open Cil_types
open Locations
type t = Inout_type.t = {
over_inputs: Locations.Zone.t;
over_inputs_if_termination: Locations.Zone.t;
over_logic_inputs: Locations.Zone.t;
under_outputs_if_termination: Locations.Zone.t;
over_outputs: Locations.Zone.t;
over_outputs_if_termination: Locations.Zone.t;
}
let top = {
over_inputs = Zone.top;
over_inputs_if_termination = Zone.top;
over_logic_inputs = Zone.top;
under_outputs_if_termination = Zone.bottom;
over_outputs = Zone.top;
over_outputs_if_termination = Zone.top;
}
type compute_t = {
over_inputs_d : Zone.t ;
under_outputs_d : Zone.t;
over_outputs_d: Zone.t;
}
let empty = {
over_inputs_d = Zone.bottom;
under_outputs_d = Zone.bottom;
over_outputs_d = Zone.bottom;
}
let bottom = {
over_inputs_d = Zone.bottom;
under_outputs_d = Zone.top;
over_outputs_d = Zone.bottom;
}
let equal ct1 ct2 =
Zone.equal ct1.over_inputs_d ct2.over_inputs_d &&
Zone.equal ct1.under_outputs_d ct2.under_outputs_d &&
Zone.equal ct1.over_outputs_d ct2.over_outputs_d
let join c1 c2 = {
over_inputs_d = Zone.join c1.over_inputs_d c2.over_inputs_d;
under_outputs_d = Zone.meet c1.under_outputs_d c2.under_outputs_d;
over_outputs_d = Zone.join c1.over_outputs_d c2.over_outputs_d;
}
let is_included c1 c2 =
Zone.is_included c1.over_inputs_d c2.over_inputs_d &&
Zone.is_included c2.under_outputs_d c1.under_outputs_d &&
Zone.is_included c1.over_outputs_d c2.over_outputs_d
let join_and_is_included smaller larger =
let join = join smaller larger in
join, equal join larger
;;
let externalize_zone ~with_formals kf =
Zone.filter_base
(Eva.Logic_inout.accept_base ~formals:with_formals ~locals:false kf)
let eval_assigns kf state assigns =
let treat_one_zone acc (out, froms as asgn) =
let clean_deps =
Locations.Zone.filter_base
(function
| Base.Var (v, _) | Base.Allocated (v, _, _) ->
not (Kernel_function.is_formal v kf)
| Base.CLogic_Var _ | Base.Null | Base.String _ -> true)
in
let out_term = out.it_content in
let outputs_under, outputs_over, deps =
if Logic_const.(is_result out_term || is_exit_status out_term)
then (Zone.bottom, Zone.bottom, Zone.bottom)
else
let output =
Eva.Logic_inout.tlval_to_zones Assigns state Write out_term
in
match output with
| Some output -> output.under, output.over, clean_deps output.deps
| None ->
Inout_parameters.warning ~current:true ~once:true
"failed to interpret assigns clause '%a'" Printer.pp_term out_term;
(Zone.bottom, Zone.top, Zone.top)
in
let inputs =
match froms with
| FromAny -> Zone.top
| From l ->
let aux acc { it_content = from } =
let inputs = Eva.Logic_inout.tlval_to_zones Assigns state Read from in
match inputs with
| Some inputs ->
let acc = Zone.join (clean_deps inputs.deps) acc in
Zone.join inputs.over acc
| _ ->
Inout_parameters.warning ~current:true ~once:true
"failed to interpret inputs in assigns clause '%a'"
Printer.pp_from asgn;
Zone.top
in
List.fold_left aux deps l
in
let sure_out =
Zone.(if equal top inputs then bottom else diff outputs_under inputs)
in
{
under_outputs_d = Zone.link acc.under_outputs_d sure_out;
over_inputs_d = Zone.join acc.over_inputs_d inputs;
over_outputs_d = Zone.join acc.over_outputs_d outputs_over;
}
in
match assigns with
| WritesAny ->
Inout_parameters.warning "@[no assigns clauses for@ function %a.@]@ \
Results will be imprecise."
Kernel_function.pretty kf;
top
| Writes l ->
let init = { bottom with under_outputs_d = Zone.bottom } in
let r = List.fold_left treat_one_zone init l in {
over_inputs = r.over_inputs_d;
over_logic_inputs = r.over_inputs_d;
over_inputs_if_termination = r.over_inputs_d;
under_outputs_if_termination = r.under_outputs_d;
over_outputs = r.over_outputs_d;
over_outputs_if_termination = r.over_outputs_d;
}
let compute_using_spec state kf =
let behaviors = Eva.Logic_inout.valid_behaviors kf state in
let assigns = Ast_info.merge_assigns behaviors in
eval_assigns kf state assigns
let compute_using_prototype ?stmt kf =
let state = Cumulative_analysis.specialize_state_on_call ?stmt kf in
compute_using_spec state kf
module Internals =
Kernel_function.Make_Table(Inout_type)
(struct
let name = "Inout.Operational_inputs.Internals"
let dependencies = [ Eva.Analysis.self ]
let size = 17
end)
module Callsite =
Datatype.Pair_with_collections (Kernel_function) (Cil_datatype.Kinstr)
module CallsiteHash = Callsite.Hashtbl
module CallwiseResults =
State_builder.Hashtbl
(Callsite.Hashtbl)
(Inout_type)
(struct
let size = 17
let dependencies = [Internals.self]
let name = "Inout.Operational_inputs.CallwiseResults"
end)
module Computer(Fenv:Dataflows.FUNCTION_ENV)(X:sig
val _version: string
val _kf: kernel_function
val kf_pre_state: Cvalue.Model.t
val stmt_state: stmt -> Cvalue.Model.t
val stmt_request: stmt -> Eva.Results.request
val at_call: stmt -> kernel_function -> Inout_type.t
end) = struct
let non_terminating_inputs = ref Zone.bottom
let non_terminating_outputs = ref Zone.bottom
let non_terminating_logic_inputs = ref Zone.bottom
let store_non_terminating_inputs inputs =
non_terminating_inputs := Zone.join !non_terminating_inputs inputs;
;;
let store_non_terminating_logic_inputs logic_inputs =
non_terminating_logic_inputs :=
Zone.join !non_terminating_logic_inputs logic_inputs
let store_non_terminating_outputs outputs =
non_terminating_outputs := Zone.join !non_terminating_outputs outputs;
;;
let store_non_terminating_subcall under_outputs subcall =
store_non_terminating_inputs (Zone.diff subcall.over_inputs under_outputs);
store_non_terminating_outputs subcall.over_outputs;
;;
let catenate c1 c2 =
let inputs = Zone.diff c2.over_inputs_d c1.under_outputs_d in
store_non_terminating_inputs inputs;
{ over_inputs_d = Zone.join c1.over_inputs_d inputs;
under_outputs_d = Zone.link c1.under_outputs_d c2.under_outputs_d;
over_outputs_d = Zone.join c1.over_outputs_d c2.over_outputs_d;
}
type t = compute_t
let pretty fmt x =
Format.fprintf fmt
"@[Over-approximated operational inputs: %a@]@\n\
@[Under-approximated operational outputs: %a@]"
Zone.pretty x.over_inputs_d
Zone.pretty x.under_outputs_d
let bottom = bottom
let join_and_is_included = join_and_is_included
let join = join
let is_included = is_included
let transfer_exp s exp data =
let request = X.stmt_request s in
let inputs = Eva.Results.expr_deps exp request in
let new_inputs = Zone.diff inputs data.under_outputs_d in
store_non_terminating_inputs new_inputs;
{data with over_inputs_d = Zone.join data.over_inputs_d new_inputs}
let add_out ~for_writing request lv deps data =
let lv_address = Eva.Results.eval_address ~for_writing lv request in
let new_outs = Eva.Results.as_zone lv_address in
let exact = Eva.Results.is_singleton lv_address in
store_non_terminating_outputs new_outs;
let lv_deps = Eva.Results.address_deps lv request in
let deps = Zone.join lv_deps deps in
let new_inputs = Zone.diff deps data.under_outputs_d in
store_non_terminating_inputs new_inputs;
let new_sure_outs =
if exact then
Zone.link data.under_outputs_d new_outs
else data.under_outputs_d
in
{ under_outputs_d = new_sure_outs;
over_inputs_d = Zone.join data.over_inputs_d new_inputs;
over_outputs_d = Zone.join data.over_outputs_d new_outs }
let transfer_call ~for_writing s dest f args _loc data =
let request = X.stmt_request s in
let eval_deps acc e = Zone.join acc (Eva.Results.expr_deps e request) in
let f_args_inputs = List.fold_left eval_deps Zone.bottom (f :: args) in
let data =
catenate
data
{ over_inputs_d = f_args_inputs ;
under_outputs_d = Zone.bottom;
over_outputs_d = Zone.bottom; }
in
let called = Eva.Results.(eval_callee f request |> default []) in
let for_functions =
List.fold_left
(fun acc kf ->
let res = X.at_call s kf in
store_non_terminating_subcall data.over_outputs_d res;
let for_function = {
over_inputs_d = res.over_inputs_if_termination;
under_outputs_d = res.under_outputs_if_termination;
over_outputs_d = res.over_outputs_if_termination;
} in
join for_function acc)
bottom
called
in
let result = catenate data for_functions in
let result =
(match dest with
| None -> result
| Some lv -> add_out ~for_writing request lv Zone.bottom result)
in result
let transfer_annotations stmt =
Annotations.iter_code_annot
(fun _ ca ->
match ca.annot_content with
| AAssert (_, p)
| AInvariant (_, true, p) ->
begin
let pre = X.kf_pre_state
and here = X.stmt_state stmt in
let deps =
Eva.Logic_inout.predicate_deps ~pre ~here p.tp_statement
in
match deps with
| None ->
()
| Some p_zone -> store_non_terminating_logic_inputs p_zone
end
| _ -> ())
stmt
let transfer_instr stmt (i: instr) (data: t) =
match i with
| Set (lv, exp, _) ->
let request = X.stmt_request stmt in
let e_inputs = Eva.Results.expr_deps exp request in
add_out ~for_writing:true request lv e_inputs data
| Local_init (v, AssignInit i, _) ->
let request = X.stmt_request stmt in
let rec aux lv i acc =
match i with
| SingleInit e ->
let e_inputs = Eva.Results.expr_deps e request in
add_out ~for_writing:false request lv e_inputs acc
| CompoundInit(ct, initl) ->
let implicit = Cumulative_analysis.fold_implicit_initializer ct in
let doinit o i _ data = aux (Cil.addOffsetLval o lv) i data in
let data = Cil.foldLeftCompound ~implicit ~doinit ~ct ~initl ~acc in
if implicit then data else
add_out ~for_writing:false request lv Zone.bottom acc
in
aux (Cil.var v) i data
| Call (lvaloption,funcexp,argl,loc) ->
transfer_call ~for_writing:true stmt lvaloption funcexp argl loc data
| Local_init(v, ConsInit(f, args, kind), loc) ->
let transfer = transfer_call ~for_writing:false stmt in
Cil.treat_constructor_as_func transfer v f args kind loc data
| Asm _ | Code_annot _ | Skip _ -> data
;;
let transfer_guard stmt e t =
let request = X.stmt_request stmt in
let v_e = Eva.Results.(eval_exp e request |> as_cvalue) in
let t1 = Ast_types.unroll (Cil.typeOf e) in
let do_then, do_else =
if Ast_types.is_integral t1 || Ast_types.is_ptr t1
then Cvalue.V.contains_non_zero v_e,
Cvalue.V.contains_zero v_e
else true, true
in
(if do_then then t else bottom),
(if do_else then t else bottom)
;;
let return_data = ref bottom;;
let transfer_stmt s data =
let map_on_all_succs new_data = List.map (fun x -> (x,new_data)) s.succs in
match s.skind with
| Instr i -> map_on_all_succs (transfer_instr s i data)
| If(exp,_,_,_) ->
let data = transfer_exp s exp data in
Dataflows.transfer_if_from_guard transfer_guard s data
| Switch(exp,_,_,_) ->
let data = transfer_exp s exp data in
Dataflows.transfer_switch_from_guard transfer_guard s data
| Return(Some exp,_) -> return_data := transfer_exp s exp data;
assert (s.succs == []); []
| Return(None,_) -> return_data := data;
assert (s.succs == []); []
| Throw _ | TryCatch _ ->
Inout_parameters.fatal "Exception node in the AST"
| UnspecifiedSequence _ | Loop _ | Block _
| Goto _ | Break _ | Continue _
| TryExcept _ | TryFinally _
-> map_on_all_succs data
;;
let transfer_stmt s data =
if Cvalue.Model.is_reachable (X.stmt_state s)
then begin
transfer_annotations s;
transfer_stmt s data
end
else []
;;
let init = [(Kernel_function.find_first_stmt Fenv.kf), empty];;
let end_dataflow () =
let res_if_termination = !return_data in {
over_inputs_if_termination = res_if_termination.over_inputs_d;
under_outputs_if_termination = res_if_termination.under_outputs_d ;
over_outputs_if_termination = res_if_termination.over_outputs_d;
over_inputs =
Zone.join !non_terminating_inputs res_if_termination.over_inputs_d;
over_logic_inputs = !non_terminating_logic_inputs;
over_outputs =
Zone.join !non_terminating_outputs res_if_termination.over_outputs_d;
}
end
let externalize ~with_formals kf v =
let filter = externalize_zone ~with_formals kf in
Inout_type.map filter v
let compute_externals_using_prototype ?stmt kf =
let internals = compute_using_prototype ?stmt kf in
externalize ~with_formals:false kf internals
let ref_get_internal = ref (fun _kf : t -> assert false)
let get_internal_aux ?stmt kf =
match stmt with
| None -> !ref_get_internal kf
| Some stmt ->
try CallwiseResults.find (kf, Kstmt stmt)
with Not_found ->
if Eva.Analysis.use_spec_instead_of_definition kf then
compute_using_prototype ~stmt kf
else !ref_get_internal kf
let ref_get_external = ref (fun _kf : t -> assert false)
let get_external_aux ?stmt kf =
match stmt with
| None -> !ref_get_external kf
| Some stmt ->
try
let internals = CallwiseResults.find (kf, Kstmt stmt) in
externalize ~with_formals:false kf internals
with Not_found ->
if Eva.Analysis.use_spec_instead_of_definition kf then
let r = compute_externals_using_prototype ~stmt kf in
CallwiseResults.add (kf, Kstmt stmt) r;
r
else !ref_get_external kf
let assigns =
let Eva.Assigns.{ return = deps_return; memory = deps_table } = assigns in
let in_return = Eva.Deps.to_zone deps_return in
let in_, out_ =
match deps_table with
| Top -> Zone.top, Zone.top
| Bottom -> Zone.bottom, Zone.bottom
| Map m ->
let aux_from out in_ (acc_in,acc_out as acc) =
match (in_ : Eva.Assigns.DepsOrUnassigned.t) with
| Unassigned -> acc
| AssignedFrom in_ | MaybeAssignedFrom in_ ->
Zone.join acc_in (Eva.Deps.to_zone in_),
Zone.join acc_out out
in
Eva.Assigns.Memory.fold aux_from m (Zone.bottom, Zone.bottom)
in
(Zone.join in_return in_), out_
[@@@ warning "-60"]
module Callwise = struct
module Record_Inout_Callbacks = Hook.Build (struct type t = Inout_type.t end)
let merge_call_in_local_table call local_table v =
let prev =
try CallsiteHash.find local_table call
with Not_found -> Inout_type.bottom
in
let joined = Inout_type.join v prev in
CallsiteHash.replace local_table call joined
let merge_call_in_global_tables (kf, _ as call) v =
let prev =
try CallwiseResults.find call
with Not_found -> Inout_type.bottom
in
CallwiseResults.replace call (Inout_type.join v prev);
let prev =
try Internals.find kf
with Not_found -> Inout_type.bottom
in
Internals.replace kf (Inout_type.join v prev);
;;
let call_inout_stack = ref []
let call_for_callwise_inout _callstack kf _state = function
| `Body ->
let table_current_function = CallsiteHash.create 7 in
call_inout_stack := (kf, table_current_function) :: !call_inout_stack
| `Reuse | `Spec | `Builtin -> ()
let pop_local_table kf =
match !call_inout_stack with
| (kf', table) :: tail ->
if not (Kernel_function.equal kf kf') then
Inout_parameters.fatal "callwise inout: %a != %a@."
Kernel_function.pretty kf Kernel_function.pretty kf';
CallsiteHash.iter merge_call_in_global_tables table;
call_inout_stack := tail;
| [] -> Inout_parameters.fatal "callwise: internal stack is empty"
let end_record callstack kf inout =
Record_Inout_Callbacks.apply inout;
let callsite = Eva.Callstack.top_callsite callstack in
match callsite, !call_inout_stack with
| Kstmt _, (_caller, table) :: _ ->
merge_call_in_local_table (kf, callsite) table inout;
| Kglobal, [] ->
merge_call_in_global_tables (kf, callsite) inout;
CallwiseResults.mark_as_computed ()
| _ ->
Inout_parameters.fatal
"callwise: internal stack is inconsistent with Eva callstack"
module MemExec =
State_builder.Hashtbl
(Datatype.Int.Hashtbl)
(Inout_type)
(struct
let size = 17
let dependencies = [Internals.self]
let name = "Operational_inputs.MemExec"
end)
let compute_call_from_value_states kf call_stack states =
let module Fenv = (val Dataflows.function_env kf: Dataflows.FUNCTION_ENV) in
let module Computer = Computer(Fenv)(
struct
let _version = "callwise"
let _kf = kf
let kf_pre_state =
Eva.Results.(at_start_of kf |> in_callstack call_stack |>
get_cvalue_model)
let stmt_state stmt =
try Cil_datatype.Stmt.Hashtbl.find states stmt
with Not_found -> Cvalue.Model.bottom
let stmt_request stmt = Eva.Results.in_cvalue_state (stmt_state stmt)
let at_call stmt kf =
let _cur_kf, table = List.hd !call_inout_stack in
try
let with_internals = CallsiteHash.find table (kf, Kstmt stmt) in
let filter =
match kf.fundec with
| Definition (fundec, _) ->
(fun b -> not (Base.is_formal_or_local b fundec))
| _ ->
let vi_kf = Kernel_function.get_vi kf in
(fun b -> not (Base.is_formal_of_prototype b vi_kf))
in
Inout_type.map (Zone.filter_base filter) with_internals
with Not_found -> Inout_type.bottom
end) in
let module [@warning "-60"] Compute =
Dataflows.Simple_forward (Fenv) (Computer)
in
Computer.end_dataflow ()
let record_for_callwise_inout callstack kf pre_state value_res =
let inout =
match value_res with
| `Body (Eva.Cvalue_callbacks.{before_stmts}, memexec_counter) ->
let inout =
if Eva.Analysis.save_results kf
then
let cvalue_states = Lazy.force before_stmts in
compute_call_from_value_states kf callstack cvalue_states
else top
in
MemExec.replace memexec_counter inout;
pop_local_table kf;
inout
| `Reuse counter -> MemExec.find counter
| `Spec _states
| `Builtin (_states, None) -> compute_using_spec pre_state kf
| `Builtin (_states, Some (froms,sure_out)) ->
let in_, out_ = extract_inout_from_froms froms in
{
over_inputs_if_termination = in_;
over_inputs = in_;
over_logic_inputs = Zone.bottom;
over_outputs_if_termination = out_ ;
over_outputs = out_;
under_outputs_if_termination = sure_out;
}
in
end_record callstack kf inout
let () =
Eva.Cvalue_callbacks.register_call_results_hook record_for_callwise_inout;
Eva.Cvalue_callbacks.register_call_hook call_for_callwise_inout
let _register_call_hook =
Dynamic.register
~comment:"Registers a function to be applied on the inputs/outputs \
computed for each function call."
~plugin:Inout_parameters.name
"register_call_hook"
Datatype.(func (func Inout_type.ty unit) unit)
Record_Inout_Callbacks.extend_once
end
module FunctionWise = struct
let call_stack : kernel_function Stack.t = Stack.create ()
let compute_internal_using_cfg kf =
try
let module Fenv =
(val Dataflows.function_env kf: Dataflows.FUNCTION_ENV)
in
let module Computer = Computer(Fenv)(struct
let _version = "functionwise"
let _kf = kf
let kf_pre_state = Eva.Results.(at_start_of kf |> get_cvalue_model)
let stmt_state s = Eva.Results.(before s |> get_cvalue_model)
let stmt_request s = Eva.Results.before s
let at_call stmt kf = get_external_aux ~stmt kf
end) in
Stack.iter (fun g -> if kf == g then raise Exit) call_stack;
Stack.push kf call_stack;
let module [@warning "-60"] Compute =
Dataflows.Simple_forward (Fenv) (Computer)
in
let result = Computer.end_dataflow () in
ignore (Stack.pop call_stack);
result
with Exit -> Inout_type.bottom
let compute_internal_using_cfg kf =
if not (Eva.Analysis.save_results kf) then
top
else begin
Inout_parameters.feedback ~level:2 "computing for function %a%s"
Kernel_function.pretty kf
(let s = ref "" in
Stack.iter
(fun kf -> s := !s^" <-"^
(Format.asprintf "%a" Kernel_function.pretty kf))
call_stack;
!s);
let r = compute_internal_using_cfg kf in
Inout_parameters.feedback ~level:2 "done for function %a"
Kernel_function.pretty kf;
r
end
end
let get_internal =
Internals.memo
(fun kf ->
Eva.Analysis.compute ();
try Internals.find kf
with
| Not_found ->
if Eva.Analysis.use_spec_instead_of_definition kf then
compute_using_prototype kf
else
FunctionWise.compute_internal_using_cfg kf
)
let raw_externals ~with_formals kf =
let filter = externalize ~with_formals kf in
filter (get_internal kf)
module Externals =
Kernel_function.Make_Table(Inout_type)
(struct
let name = "External inouts full"
let dependencies = [ Internals.self ]
let size = 17
end)
let get_external = Externals.memo (raw_externals ~with_formals:false)
let compute kf = ignore (get_external kf)
module Externals_With_Formals =
Kernel_function.Make_Table(Inout_type)
(struct
let name = "Inout.Operational_inputs.Externals_With_Formals"
let dependencies = [ Internals.self ]
let size = 17
end)
let get_external_with_formals =
Externals_With_Formals.memo (raw_externals ~with_formals:true)
let pretty_operational_inputs_internal fmt kf =
Format.fprintf fmt "@[InOut (internal) for function %a:@\n%a@]@\n"
Kernel_function.pretty kf
Inout_type.pretty_operational_inputs (get_internal kf)
let pretty_operational_inputs_external fmt kf =
Format.fprintf fmt "@[InOut for function %a:@\n%a@]@\n"
Kernel_function.pretty kf
Inout_type.pretty_operational_inputs (get_external kf)
let pretty_operational_inputs_external_with_formals fmt kf =
Format.fprintf fmt "@[InOut (with formals) for function %a:@\n%a@]@\n"
Kernel_function.pretty kf
Inout_type.pretty_operational_inputs (get_external_with_formals kf)
let pretty fmt x =
Format.fprintf fmt "@[<v>";
Format.fprintf fmt "@[<v 2>Operational inputs:@ @[<hov>%a@]@]@ "
Locations.Zone.pretty (x.Inout_type.over_inputs);
Format.fprintf fmt "@[<v 2>Operational inputs on termination:@ @[<hov>%a@]@]@ "
Locations.Zone.pretty (x.Inout_type.over_inputs_if_termination);
Format.fprintf fmt "@[<v 2>Sure outputs:@ @[<hov>%a@]@]"
Locations.Zone.pretty (x.Inout_type.under_outputs_if_termination);
Format.fprintf fmt "@]"
let get_internal_precise = get_internal_aux
let () =
ref_get_internal := get_internal;
ref_get_external := get_external