package frama-c

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

Source file context.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
(**************************************************************************)
(*                                                                        *)
(*  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 Dive_types

module Graph = Dive_graph


module NodeRef = Datatype.Pair_with_collections
    (Node_kind) (Callstack)
    (struct let module_name = "Build.NodeRef" end)

module Index = Datatype.Int.Hashtbl
module NodeTable = FCHashtbl.Make (NodeRef)
module NodeSet = Graph.Node.Set
module BaseSet = Cil_datatype.Varinfo.Set

type element = Node of node | Edge of (node * dependency * node)

type t = {
  mutable graph: Graph.t;
  mutable vertex_table: node Index.t; (* node_key -> node *)
  mutable node_table: node NodeTable.t; (* node_kind * callstack -> node *)
  mutable unfolded_bases: BaseSet.t;
  mutable hidden_bases: BaseSet.t;
  mutable max_dep_fetch_count: int;
  mutable roots: NodeSet.t;
  mutable update_hook : element -> unit;
  mutable remove_hook : element -> unit;
  mutable clear_hook : unit -> unit;
}


(* --- initialization --- *)

let no_hook = fun _ -> ()

let create () =
  {
    graph = Graph.create ();
    vertex_table = Index.create 13;
    node_table = NodeTable.create 13;
    unfolded_bases = BaseSet.empty;
    hidden_bases = BaseSet.empty;
    max_dep_fetch_count = 10;
    roots = NodeSet.empty;
    update_hook = no_hook;
    remove_hook = no_hook;
    clear_hook = no_hook;
  }

let clear context =
  context.graph <- Graph.create ();
  context.vertex_table <- Index.create 13;
  context.node_table <- NodeTable.create 13;
  context.max_dep_fetch_count <- 10;
  context.roots <- NodeSet.empty;
  context.clear_hook ()


(* Hooks *)

let set_update_hook context f =
  context.update_hook <- f

let set_remove_hook context f =
  context.remove_hook <- f

let set_clear_hook context f =
  context.clear_hook <- f

let notify_node_update context node =
  context.update_hook (Node node)


(* --- Accessors --- *)

let get_graph context =
  context.graph

let find_node context node_key =
  Index.find context.vertex_table node_key

let get_max_dep_fetch_count context =
  context.max_dep_fetch_count


(* --- Roots --- *)

let get_roots context =
  NodeSet.elements context.roots

let update_roots context new_roots =
  let old_roots = context.roots in
  context.roots <- new_roots;
  let unset n =
    n.node_is_root <- false;
    context.update_hook (Node n);
  and set n =
    n.node_is_root <- true;
    context.update_hook (Node n);
  in
  NodeSet.iter unset old_roots;
  NodeSet.iter set new_roots

let set_unique_root context root =
  update_roots context (NodeSet.singleton root)

let add_root context root =
  update_roots context (NodeSet.add root context.roots)

let remove_root context root =
  update_roots context (NodeSet.remove root context.roots)


(* --- Folding --- *)

let is_folded context vi =
  not (BaseSet.mem vi context.unfolded_bases)

let fold context vi =
  context.unfolded_bases <- BaseSet.remove vi context.unfolded_bases

let unfold context vi =
  context.unfolded_bases <- BaseSet.add vi context.unfolded_bases


(* --- Base hiding --- *)

let is_hidden context node_kind =
  match Node_kind.get_base node_kind with
  | Some vi when BaseSet.mem vi context.hidden_bases -> true
  | _ -> false

let show context vi =
  context.hidden_bases <- BaseSet.add vi context.hidden_bases

let hide context vi =
  context.hidden_bases <- BaseSet.add vi context.hidden_bases


(* --- Building --- *)

let add_node context ~node_kind ~node_locality =
  let node_ref = (node_kind, node_locality.loc_callstack) in
  let add_new _ =
    let node = Graph.create_node context.graph ~node_kind ~node_locality in
    node.node_hidden <- is_hidden context node.node_kind;
    Index.add context.vertex_table node.node_key node;
    context.update_hook (Node node);
    node
  in
  NodeTable.memo context.node_table node_ref add_new

let remove_node context node =
  let node_ref = (node.node_kind, node.node_locality.loc_callstack) in
  let graph = context.graph in
  Graph.iter_succ (fun n -> n.node_writes_computation <- NotDone) graph node;
  Graph.iter_pred (fun n -> n.node_reads_computation <- NotDone) graph node;
  Graph.iter_succ_e (fun e -> context.remove_hook (Edge e)) graph node;
  Graph.iter_pred_e (fun e -> context.remove_hook (Edge e)) graph node;
  Graph.remove_node context.graph node;
  Index.remove context.vertex_table node.node_key;
  NodeTable.remove context.node_table node_ref;
  context.remove_hook (Node node)

let add_dep context ~origin ~kind src dest =
  let edge = Graph.create_dependency context.graph ~origin ~kind src dest in
  context.update_hook (Edge edge)

let remove_dep context edge =
  Graph.remove_dependency context.graph edge;
  context.remove_hook (Edge edge)

let remove_node_deps context node =
  Graph.iter_pred_e (remove_dep context) context.graph node

let update_node_values context node ~typ ~cvalue ~taint =
  Graph.update_node_values node ~typ ~cvalue ~taint;
  notify_node_update context node

let set_node_writes context node writes =
  node.node_writes <- List.sort_uniq Studia.Writes.compare writes;
  notify_node_update context node
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