package frama-c

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

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

(** DataState is associated with a program point
    and provide the dependencies for the data,
    ie. it stores for each location the nodes of the pdg where its value
    was last defined.
*)

let dkey = Pdg_parameters.register_category "state"

module P = Pdg_parameters

open Pdg_types
open PdgTypes

exception Cannot_fold

let make loc_info under_outputs =
  { loc_info = loc_info; under_outputs = under_outputs }

let empty = make LocInfo.empty Locations.Zone.bottom
(* Convention: bottom is used for statements that are not reachable,
   and for calls that never terminate. In this case, the second field
   must be ignored *)
let bottom = make LocInfo.bottom Locations.Zone.bottom

let pretty fmt state =
  Format.fprintf fmt "state = %a@.with under_outputs = %a@."
    LocInfo.pretty state.loc_info
    Locations.Zone.pretty state.under_outputs

let add_loc_node state ~exact loc node =
  P.debug ~dkey ~level:2 "add_loc_node (%s) : node %a -> %a@."
    (if exact then "exact" else "merge")
    PdgTypes.Node.pretty node
    Locations.Zone.pretty loc ;
  if LocInfo.is_bottom state.loc_info then
    (* Do not add anything to a bottom state (which comes from an unreachable
       statement *)
    state
  else
    let new_info = NodeSetLattice.inject_singleton node in
    let new_loc_info =
      LocInfo.add_binding ~exact state.loc_info loc new_info in
    let new_outputs = (* Zone.link in the under-approx version of Zone.join *)
      if exact then Locations.Zone.link state.under_outputs loc
      else state.under_outputs
    in
    P.debug ~dkey ~level:2 "add_loc_node -> %a" pretty state;
    make new_loc_info new_outputs

(** this one is very similar to [add_loc_node] except that
 * we want to accumulate the nodes (exact = false) but nonetheless
 * define under_outputs like (exact = true) *)
let add_init_state_input state loc node =
  match loc with
  | Locations.Zone.Top(_p,_o) ->
    (* don't add top because it loses everything*)
    state
  | _ ->
    let new_info = NodeSetLattice.inject_singleton node in
    let new_loc_info =
      LocInfo.add_binding ~exact:false state.loc_info loc new_info
    in
    let new_outputs = Locations.Zone.link state.under_outputs loc in
    make new_loc_info new_outputs

let test_and_merge ~old new_ =
  if LocInfo.is_included new_.loc_info old.loc_info
  && Locations.Zone.is_included old.under_outputs new_.under_outputs
  then (false, old)
  else
    (* Catch Bottom states, as under_outputs get a special value *)
  if LocInfo.is_bottom old.loc_info then true, new_
  else if LocInfo.is_bottom new_.loc_info then true, old
  else
    let new_loc_info = LocInfo.join old.loc_info new_.loc_info in
    let new_outputs =
      Locations.Zone.meet old.under_outputs new_.under_outputs
    in
    let new_state =
      { loc_info = new_loc_info ; under_outputs = new_outputs }
    in
    true, new_state

(** returns pairs of (n, z_opt) where n is a node that computes a part of [loc]
 * and z is the intersection between [loc] and the zone computed by the node.
 * @raise Cannot_fold if the state is top (TODO : something better ?)
 * *)
let get_loc_nodes_and_part state loc =
  let process z nodes acc =
    if Locations.Zone.intersects z loc then
      let z =
        if Locations.Zone.equal loc z
        then Some loc
        (* Be careful not ot put None here, because if we have n_1 : (s1 =
           s2) and then n_2 : (s1.b = 3) the state looks like :
           s1.a -> n_1; s1.b -> n_2 ; s1.c -> n_1.  And if we
           look for s1.a in that state, we get n_1 but this node
           represent more that s1.a even if it is so in the
           state...  *)
        else Some (Locations.Zone.narrow z loc) in
      let add n acc =
        P.debug ~dkey ~level:2 "get_loc_nodes ->  %a@."
          PdgTypes.Node.pretty_with_part (n,z);
        (n,z)::acc
      in
      NodeSetLattice.fold add nodes acc
    else
      acc
  in
  match state.loc_info with
  | LocInfo.Top -> raise Cannot_fold
  | LocInfo.Bottom -> []
  | LocInfo.Map m -> LocInfo.fold process m []

(** @raise Cannot_fold (see [get_loc_nodes_and_part]) *)
let get_loc_nodes state loc =
  P.debug ~dkey ~level:2 "get_loc_nodes %a@.            in %a@."
    Locations.Zone.pretty loc pretty state ;
  if Locations.Zone.equal loc Locations.Zone.bottom
  then  [], None (* nothing to do *)
  else
    let nodes = get_loc_nodes_and_part state loc in
    let undef_zone = Locations.Zone.diff loc state.under_outputs in
    P.debug ~dkey ~level:2 "get_loc_nodes -> undef = %a@."
      Locations.Zone.pretty undef_zone;
    let undef_zone =
      if (Locations.Zone.equal undef_zone Locations.Zone.bottom) then None
      else Some undef_zone
    in
    nodes, undef_zone

open Cil_datatype

type states = PdgTypes.data_state Stmt.Hashtbl.t

(* Slightly ugly, but should not be a problem unless the sid counter wraps *)
let stmt_init = List.hd Stmt.reprs
let stmt_last = { stmt_init with Cil_types.sid = stmt_init.Cil_types.sid - 1 }

let store_init_state states state = Stmt.Hashtbl.add states stmt_init state
let store_last_state states state = Stmt.Hashtbl.add states stmt_last state

let get_init_state states = Stmt.Hashtbl.find states stmt_init
let get_last_state states = Stmt.Hashtbl.find states stmt_last
let get_stmt_state states stmt = Stmt.Hashtbl.find states stmt
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