package frama-c

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

Source file callwise.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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_datatype


module Tbl =
  Cil_state_builder.Kinstr_hashtbl
    (Function_Froms)
    (struct
      let name = "Callwise dependencies"
      let size = 17
      let dependencies = [ Eva.Analysis.self ]
    end)
let () = From_parameters.ForceCallDeps.set_output_dependencies [Tbl.self]

let merge_call_froms table callsite froms =
  try
    let current = Kinstr.Hashtbl.find table callsite in
    let new_froms = Function_Froms.join froms current in
    Kinstr.Hashtbl.replace table callsite new_froms
  with Not_found ->
    Kinstr.Hashtbl.add table callsite froms

(** State for the analysis of one function call *)
type from_state = {
  current_function: Kernel_function.t (** Function being analyzed *);
  value_initial_state: Cvalue.Model.t (** State of Eva at the beginning of
                                          the call *);
  table_for_calls: Function_Froms.t Kinstr.Hashtbl.t
(** State of the From plugin for each statement containing a function call
    in the body of [current_function]. Updated incrementally each time
    Value analyses such a statement *);
}

(** The state of the callwise From analysis. Only the top of this callstack
    is accessed. New calls are pushed on the stack when Value starts the
    analysis of a function, and popped when the analysis finishes. This
    stack is manually synchronized with Value's callstack. *)
let call_froms_stack : from_state list ref = ref []

let record_callwise_dependencies_in_db call_site froms =
  try
    let previous = Tbl.find call_site in
    Tbl.replace call_site (Function_Froms.join previous froms)
  with Not_found -> Tbl.add call_site froms

let call_for_individual_froms callstack _kf call_type value_initial_state =
  if From_parameters.ForceCallDeps.get () then begin
    let current_function, call_site = List.hd callstack in
    let register_from froms =
      record_callwise_dependencies_in_db call_site froms;
      match !call_froms_stack with
      | { table_for_calls } :: _ ->
        merge_call_froms table_for_calls call_site froms;
      | [] ->
        (* Empty call stack: this is the main entry point with no call site. *)
        assert (call_site = Cil_types.Kglobal);
    in
    let compute_from_behaviors bhv =
      let assigns = Ast_info.merge_assigns bhv in
      let froms =
        From_compute.compute_using_prototype_for_state
          value_initial_state current_function assigns
      in
      register_from froms
    in
    match call_type with
    | `Def | `Memexec ->
      let table_for_calls = Kinstr.Hashtbl.create 7 in
      call_froms_stack :=
        { current_function; value_initial_state; table_for_calls } ::
        !call_froms_stack
    | `Builtin (Some (result,_)) ->
      register_from result
    | `Builtin None ->
      let behaviors =
        Eva.Logic_inout.valid_behaviors current_function value_initial_state
      in
      compute_from_behaviors behaviors
    | `Spec spec ->
      compute_from_behaviors spec.Cil_types.spec_behavior
  end

let end_record call_stack froms =
  let (current_function_value, call_site) = List.hd call_stack in
  record_callwise_dependencies_in_db call_site froms;
  (* pop + record in top of stack the froms of function that just finished *)
  match !call_froms_stack with
  | {current_function} :: ({table_for_calls = table} :: _ as tail) ->
    if current_function_value != current_function then
      From_parameters.fatal "calldeps %a != %a@."
        Kernel_function.pretty current_function
        Kernel_function.pretty current_function_value;
    call_froms_stack := tail;
    merge_call_froms table call_site froms

  | _ ->  (* the entry point, probably *)
    Tbl.mark_as_computed ();
    call_froms_stack := []


module MemExec =
  State_builder.Hashtbl
    (Datatype.Int.Hashtbl)
    (Function_Froms)
    (struct
      let size = 17
      let dependencies = [Tbl.self]
      let name = "From.Callwise.MemExec"
    end)

let compute_call_from_value_states current_function states =
  let module To_Use = struct
    let get_from_call _f callsite =
      let { table_for_calls } = List.hd !call_froms_stack in
      try Kinstr.Hashtbl.find table_for_calls (Cil_types.Kstmt callsite)
      with Not_found -> raise From_compute.Call_did_not_take_place

    let stmt_request stmt =
      Eva.Results.in_cvalue_state
        (try Stmt.Hashtbl.find states stmt
         with Not_found -> Cvalue.Model.bottom)

    let keep_base kf base =
      let fundec = Kernel_function.get_definition kf in
      not (Base.is_formal_or_local base fundec)

    let cleanup_and_save _kf froms = froms
  end
  in
  let module Callwise_Froms = From_compute.Make(To_Use) in
  Callwise_Froms.compute_and_return current_function


let record_for_individual_froms callstack cur_kf value_res =
  if From_parameters.ForceCallDeps.get () then begin
    let froms = match value_res with
      | Eva.Cvalue_callbacks.Store ({before_stmts}, memexec_counter) ->
        let froms =
          if Eva.Analysis.save_results cur_kf
          then compute_call_from_value_states cur_kf (Lazy.force before_stmts)
          else Function_Froms.top
        in
        let pre_state = match !call_froms_stack with
          | [] -> assert false
          | { value_initial_state } :: _ -> value_initial_state
        in
        if From_parameters.VerifyAssigns.get () then
          Eva.Logic_inout.verify_assigns cur_kf ~pre:pre_state froms;
        MemExec.replace memexec_counter froms;
        froms

      | Reuse counter ->
        MemExec.find counter
    in
    end_record callstack froms

  end


(* Register our callbacks inside the value analysis *)
let () =
  Eva.Cvalue_callbacks.register_call_hook call_for_individual_froms;
  Eva.Cvalue_callbacks.register_call_results_hook record_for_individual_froms

let iter = Tbl.iter
let find = Tbl.find

let compute_all_calldeps () =
  if not (Tbl.is_computed ()) then begin
    if Eva.Analysis.is_computed () then
      Project.clear
        ~selection:(State_selection.with_dependencies Eva.Analysis.self)
        ();
    Eva.Analysis.compute ()
  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