package frama-c

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

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

open Pdg_types
open PdgIndex

type data_info = ((PdgTypes.Node.t * Locations.Zone.t option) list
                  * Locations.Zone.t option) option

type ctrl_info = PdgTypes.Node.t list

type decl_info = PdgTypes.Node.t list

let zone_info_nodes pdg data_info =
  let add_info_nodes pdg (nodes_acc, undef_acc) info =
    let stmt = info.Logic_deps.ki in
    let before = info.Logic_deps.before in
    let zone = info.Logic_deps.zone in
    Pdg_parameters.debug ~level:2 "[pdg:annotation] need %a %s stmt %d@."
      Locations.Zone.pretty zone
      (if before then "before" else "after") stmt.sid;
    let nodes, undef_loc =
      Sets.find_location_nodes_at_stmt pdg stmt ~before zone
    in
    let undef_acc = match undef_acc, undef_loc with
      | None, _ -> undef_loc
      | _, None -> undef_acc
      | Some z1, Some z2 -> Some (Locations.Zone.join z1 z2)
    in
    (nodes @ nodes_acc, undef_acc)
  in match data_info with
  | None -> None (* To_zone.xxx didn't manage to compute the zone *)
  | Some data_info ->
    let data_dpds = ([], None) in
    let data_dpds =
      List.fold_left (add_info_nodes pdg) data_dpds data_info
    in Some data_dpds

let get_decl_nodes pdg decl_info =
  let add_decl_nodes decl_var nodes_acc =
    let node = Sets.find_decl_var_node pdg decl_var in
    node::nodes_acc
  in
  Varinfo.Set.fold add_decl_nodes decl_info []

let find_nodes_for_function_contract pdg f_interpret =
  let kf =  PdgTypes.Pdg.get_kf pdg in
  let (data_info, decl_label_info) = f_interpret kf in
  let data_dpds = zone_info_nodes pdg data_info in
  let decl_nodes = (* No way to get stmt from labels of at construct into function contracts *)
    get_decl_nodes pdg decl_label_info.Logic_deps.var
  in
  decl_nodes, data_dpds

let find_fun_precond_nodes (pdg:PdgTypes.Pdg.t) p =
  let f_interpret kf =
    let f_ctx = Logic_deps.mk_ctx_func_contract ~before:true kf in
    Logic_deps.from_pred p f_ctx
  in find_nodes_for_function_contract pdg f_interpret

let find_fun_postcond_nodes pdg p =
  let f_interpret kf =
    let f_ctx = Logic_deps.mk_ctx_func_contract ~before:false kf in
    Logic_deps.from_pred p f_ctx
  in let nodes,deps = find_nodes_for_function_contract pdg f_interpret
  in let nodes =
       (* find is \result is used in p, and if it is the case,
        * add the node [Sets.find_output_node pdg]
        * to the returned list of nodes.
       *)
       if Logic_deps.to_result_from_pred p then
         (Sets.find_output_node pdg)::nodes
       else nodes
  in nodes,deps

let find_fun_variant_nodes pdg t =
  let f_interpret kf =
    let f_ctx = Logic_deps.mk_ctx_func_contract ~before:true kf in
    Logic_deps.from_term t f_ctx
  in find_nodes_for_function_contract pdg f_interpret

let find_code_annot_nodes pdg stmt annot =
  Pdg_parameters.debug "[pdg:annotation] CodeAnnot-%d stmt %d : %a @."
    annot.annot_id stmt.sid
    Printer.pp_code_annotation annot;
  if Eva.Results.is_reachable stmt then
    begin
      let kf =  PdgTypes.Pdg.get_kf pdg in
      let (data_info, decl_label_info), slices =
        Logic_deps.from_stmt_annot annot (stmt, kf)
      in
      let data_dpds = zone_info_nodes pdg data_info in
      let decl_nodes = get_decl_nodes pdg decl_label_info.Logic_deps.var in
      let labels = decl_label_info.Logic_deps.lbl in
      let stmt_key = Key.stmt_key stmt in
      let stmt_node = match stmt_key with
        | Key.Stmt _ -> Sets.find_stmt_node pdg stmt
        | Key.CallStmt _ -> Sets.find_call_ctrl_node pdg stmt
        | _ -> assert false
      in
      let ctrl_dpds = Sets.direct_ctrl_dpds pdg stmt_node in
      let add_stmt_nodes s acc =
        try Sets.find_stmt_and_blocks_nodes pdg s @ acc
        with Not_found -> acc
      in
      (* can safely ignore slices.ctrl
       * because we already have the ctrl dpds from the stmt node. *)
      let stmt_slices = slices.Logic_deps.stmt in
      let ctrl_dpds = Stmt.Set.fold add_stmt_nodes stmt_slices ctrl_dpds in
      let add_label_nodes l acc = match l with
        | StmtLabel stmt ->
          (* TODO: we could be more precise here if we knew which label
           * is really useful... *)
          let add acc l =
            try (Sets.find_label_node pdg !stmt l)::acc
            with Not_found -> acc
          in List.fold_left add acc (!stmt).labels
        | FormalLabel _ | BuiltinLabel _ -> acc
      in
      let ctrl_dpds = Logic_label.Set.fold add_label_nodes labels ctrl_dpds in
      if Pdg_parameters.debug_atleast 2 then begin
        let p fmt (n,z) = match z with
          | None -> PdgTypes.Node.pretty fmt n
          | Some z -> Format.fprintf fmt "%a(%a)"
                        PdgTypes.Node.pretty n Locations.Zone.pretty z
        in
        let pl fmt l = List.iter (fun n -> Format.fprintf fmt " %a" p n) l in
        Pdg_parameters.debug " ctrl nodes = %a"
          PdgTypes.Node.pretty_list ctrl_dpds;
        Pdg_parameters.debug " decl nodes = %a"
          PdgTypes.Node.pretty_list decl_nodes;
        match data_dpds with
        | None ->
          Pdg_parameters.debug " data nodes = None (failed to compute)"
        | Some (data_nodes, data_undef) ->
          begin
            Pdg_parameters.debug " data nodes = %a" pl data_nodes;
            match data_undef with
            | None -> ()
            | Some data_undef ->
              Pdg_parameters.debug " data undef = %a"
                Locations.Zone.pretty data_undef;
          end
      end;
      ctrl_dpds, decl_nodes, data_dpds
    end
  else begin
    Pdg_parameters.debug ~level:2
      "[pdg:annotation] CodeAnnot-%d : unreachable stmt ! @."
      annot.annot_id;
    raise Not_found (* unreachable statement *)
  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