package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file cumulative_analysis.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    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 Visitor

(* To avoid a performance issue, do not fold implicit zero-initializers of large
   arrays. For arrays of scalar elements, the outputs of an initializer is
   exactly the zone covered by the array. For arrays containing structs with
   padding bits, this is an over-approximation, so we prefer folding the
   initializer if the array is not too big (the 100 cells limit is arbitrary).
   We still need to fold the explicit initializers to collect the inputs. *)
let fold_implicit_initializer typ =
  not
    (Cil.isArrayType typ &&
     (Cil.isArithmeticOrPointerType (Cil.typeOf_array_elem typ)
      || Ast_info.array_size typ > (Integer.of_int 100)))

let specialize_state_on_call ?stmt kf =
  match stmt with
  | None -> Eva.Results.(at_start_of kf |> get_cvalue_model)
  | Some stmt ->
    let filter = fun cs -> match Eva.Callstack.top_callsite cs with
      | Kstmt s -> Cil_datatype.Stmt.equal s stmt
      | Kglobal -> false
    in
    Eva.Results.(at_start_of kf |> filter_callstack filter |> get_cvalue_model)

class virtual ['a] cumulative_visitor = object
  inherit frama_c_inplace as self

  method specialize_state_on_call kf =
    specialize_state_on_call ?stmt:self#current_stmt kf

  method virtual compute_kf: kernel_function -> 'a

end

class type virtual ['a] cumulative_class = object
  inherit ['a] cumulative_visitor

  method bottom: 'a

  method result: 'a
  method join: 'a -> unit

  method compute_funspec : kernel_function -> 'a

  method clean_kf_result: kernel_function -> 'a -> 'a
end


module Make (X:
             sig
               val analysis_name: string

               type t
               module T: Datatype.S with type t = t

               class virtual do_it: [t] cumulative_class
             end) =
struct

  module Memo =
    Kernel_function.Make_Table(X.T)
      (struct
        let name = "Inout.Cumulative_analysis.Memo(" ^ X.analysis_name ^ ")"
        let dependencies = [ Eva.Analysis.self ]
        let size = 97
      end)

  class do_it_cached call_stack = object(self)
    inherit X.do_it

    (* The cycle variable holds the list of functions that are
       involved in a cycle. As long as it is not empty, we known that
       the results we are computing are not complete, and we do not memorize
       them *)
    val mutable cycle = Kernel_function.Hptset.empty
    method private add_cycle s = cycle <- Kernel_function.Hptset.union s cycle
    method cycle = cycle

    (* Computation using the body of a kernel function. The result is
       automatically cached by the function if possible *)
    method private compute_kf_with_def kf =
      let f = Kernel_function.get_definition kf in
      if List.exists (Kernel_function.equal kf) call_stack then (
        self#add_cycle (Kernel_function.Hptset.singleton kf);
        self#bottom
      )
      else
        let computer = new do_it_cached (kf :: call_stack) in
        ignore (visitFramacFunction (computer:>frama_c_visitor) f);
        (* Results on all the statements of the function *)
        let v = computer#result in
        let v = computer#clean_kf_result kf v in
        (* recursive calls detected during analysis of the statements*)
        let cycle_aux = Kernel_function.Hptset.remove kf computer#cycle in
        self#add_cycle cycle_aux;
        if Kernel_function.Hptset.is_empty cycle then (
          (* No recursive calls, our results are correct *)
          Inout_parameters.debug "Caching %s result for %a"
            X.analysis_name Kernel_function.pretty kf;
          Memo.add kf v;
        ) else
          Inout_parameters.debug
            "Not caching %s result for %a because of cycle"
            X.analysis_name Kernel_function.pretty kf;
        v

    (* Computation and caching for a kernel function, using its spec *)
    method private compute_kf_with_spec_generic kf =
      try Memo.find kf
      with Not_found ->
        let r_glob = self#compute_funspec kf in
        let r_glob = self#clean_kf_result kf r_glob in
        Memo.add kf r_glob;
        r_glob

    method compute_kf kf =
      if Eva.Analysis.use_spec_instead_of_definition kf then
        (* If only a declaration is available, or we are instructed to use
           the spec, do so. If a current stmt is available (most of the times),
           do not cache the results. Maybe [compute_funspec] will be able
           to deliver a more precise result on this given statement *)
        match self#current_stmt with
        | None -> self#compute_kf_with_spec_generic kf
        | Some _stmt -> self#compute_funspec kf
      else
        try Memo.find kf
        with Not_found -> self#compute_kf_with_def kf
  end

  let statement stmt =
    let computer = new do_it_cached [] in
    ignore (visitFramacStmt (computer:>frama_c_visitor) stmt);
    assert (Kernel_function.Hptset.is_empty computer#cycle);
    computer#result

  let expr stmt e =
    let computer = new do_it_cached [] in
    computer#push_stmt stmt;
    ignore (visitFramacExpr (computer:>frama_c_visitor) e);
    assert (Kernel_function.Hptset.is_empty computer#cycle);
    computer#result

  let kernel_function kf =
    let computer = new do_it_cached [] in
    computer#join (computer#compute_kf kf);
    assert (Kernel_function.Hptset.is_empty computer#cycle);
    computer#result

end

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct