package frama-c

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

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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  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, version 2.1.                                              *)
(*                                                                        *)
(*  It 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.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Locations

(* Computation of over-approximated operational inputs:
   An accurate computation of these inputs needs the computation of
   under-approximated outputs.
*)

type t = Inout_type.t = {
  over_inputs: Locations.Zone.t;
  over_inputs_if_termination: Locations.Zone.t;
  over_logic_inputs: Locations.Zone.t;
  (* [over_logic_inputs] is used internally by Eva to make memexec consider also
     the logic inputs of the function. Computed in [transfer_annotations]. *)
  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;
}

(* [_if_termination] fields of the type above, which are the one propagated by
   the dataflow analysis of this module. It is meaningless to store the other
   ones, as they come from branches that are by construction not propagated
   until the end by the dataflow. *)
type compute_t = {
  over_inputs_d : Zone.t ;
  under_outputs_d : Zone.t;
  over_outputs_d: Zone.t;
}

(* Initial value for the computation *)
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)

(* This code evaluates an assigns, computing in particular a sound approximation
   of sure outputs. For an assigns [locs_out \from locs_from], the process
   is the following:
   - evaluate locs_out to locations; discard those that are not exact, as
     we cannot guarantee that they are always assigned
   - evaluate locs_from, as a zone (no need for locations)
   - compute the difference between the out and the froms, ie remove the
     zones that are such that [z \from z] holds

   (Note: large parts of this code are inspired/redundant with
   [assigns_to_zone_foobar_state] in Value/register.ml)
*)
let eval_assigns kf state assigns =
  let treat_one_zone acc (out, froms as asgn) = (* treat a single assign *)
    (* Return a list of independent output zones, plus a zone indicating
       that the zone has been overwritten in a sure way *)
    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
    (* Compute all inputs as a zone *)
    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
    (* Fuse all outputs. An output is sure if it was certainly
       overwritten (i.e. is in the left part of an assign clause,
       and if it is not amongst its from.) *)
    (* Note: here we remove an overapproximation from an
       underapproximation to get an underapproximation, which is not
       the usual direction. It works here because diff on non-top zones is
       an exact operation. *)
    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

(* Results of this module, consolidated by functions. Formals and locals
   are stored *)
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

(* Results of an an entire call, represented by a pair (stmt, kernel_function).
*)
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 (* Debug: Callwise or functionwise *)
    val _kf: kernel_function (* Debug: Function being analyzed *)
    val kf_pre_state: Cvalue.Model.t (* Memory pre-state of the function. *)
    val stmt_state: stmt -> Cvalue.Model.t (* Memory state at the given stmt *)
    val stmt_request: stmt -> Eva.Results.request (* Request at the given stmt *)
    val at_call: stmt -> kernel_function -> Inout_type.t (* Results of the
                                                            analysis for the given call. Must not contain locals or formals *)
  end) = struct

  (* We want to compute the in/out for all terminating and
     non-terminating points of the function. This is not immediate
     with a dataflow, as all (1) infinite loops, (2) branches that call a non
     terminating function, or (3) branches that fail, will not appear in the
     final state. Hence, we two use auxiliary variables into which we add
     all partial results. *)
  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;
  ;;

  (* Store the 'non-termination' information of a function subcall into
     the current call. [under_outputs] are the current call sure 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

  (* Transfer function on expression. *)
  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}

  (* Initialized const variables should be included as outputs of the function,
     so [for_writing] must be false for local initializations. It should be
     true for all other instructions. *)
  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
        (* There is only one modified zone. So, this is an exact output.
           Add it into the under-approximated outputs. *)
        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
    (* Join the inputs of [args] and of the function expression. *)
    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 =
      (* Treatment for the possible assignment of the call result *)
      (match dest with
       | None -> result
       | Some lv -> add_out ~for_writing request lv Zone.bottom result)
    in result

  (* Propagate all zones in predicates for the given statement, only in the case
     of assertions and loop-invariants. For the time being, we do not treat
     terminating and non-terminating points of the function differently. *)
  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 ->
               (* To be sound, we should perform a join with the top zone here.
                  We do nothing instead because the latter behavior would
                  directly disable memexec. *)
               ()
             | Some p_zone -> store_non_terminating_logic_inputs p_zone
           end
         | _ -> ())
      stmt

  (* Transfer function on instructions. *)
  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) ->
          (* Avoid folding implicit zero-initializer of large arrays. *)
          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
            (* If the implicit zero-initializers hade been skipped, add the
               zone of the array as outputs. It is exactly the written zone for
               arrays of scalar elements. Nothing is read by zero-initializers,
               so the inputs are empty. *)
            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
  ;;

  (* transfer_guard: gets the state obtained after evaluating the
     condition, and split the state according to the truth value of
     the condition. In this case, we just make sure that dead
     edges get bottom, instead of the input state. *)
  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 (* TODO: a float condition is true iff != 0.0 *)
    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 extract_inout_from_froms 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) =
        (* Skip zones fully unassigned, they are not really port of the
           dependencies, but just present in the offsetmap to avoid "holes" *)
        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 =
    (* Global callwise table *)
    let prev =
      try CallwiseResults.find call
      with Not_found -> Inout_type.bottom
    in
    CallwiseResults.replace call (Inout_type.join v prev);
    (* Global, kf-indexed, table *)
    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, [] ->  (* the entry point *)
      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

        (* Returns the [kf] pre-state with respect to the single [call_stack]. *)
        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


  (* Register our callbacks inside the value analysis *)

  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


(* Functionwise version of the computations. *)
module FunctionWise = struct

  (* Stack of function being processed *)
  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 (*TODO*) (*{
                                              Inout_type.over_inputs_if_termination = empty.over_inputs_d ;
                                              under_outputs_if_termination = empty.under_outputs_d;
                                              over_inputs = empty.over_inputs_d;
                                              over_outputs = empty.over_outputs_d;
                                              over_outputs_if_termination = empty.over_outputs_d;
                                              }*)

  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 (* The results may have been computed by the call
                                to Eva.Analysis.compute *)
       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
OCaml

Innovation. Community. Security.