package frama-c

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

Source file defs.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
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

(** Find the statements that defines a given data at a program point,
 * ie. in each backward path starting from this point, find the statement
 * the the data has been assigned for the last time. *)

open Cil_datatype
open Cil_types

open Pdg_types

let debug1 fmt = Datascope.R.debug ~level:1 fmt

module Interproc =
  Datascope.R.True(struct
    let option_name = "-scope-defs-interproc"
    let help = "interprocedural defs computation"
  end)

module NSet = PdgTypes.Node.Set

let add_list_to_set l s = List.fold_left (fun r n -> NSet.add n r) s l


let _pp_list_node_underout prefix fmt =
  Pretty_utils.pp_list ~pre:(prefix ^^ " @[") ~suf:"@]@." ~sep:"@ "
    (fun fmt (n, undef) ->
       match undef with
       | None -> PdgTypes.Node.pretty fmt n
       | Some undef ->
         Format.fprintf fmt "%a {underout %a}"
           PdgTypes.Node.pretty n Locations.Zone.pretty undef)
    fmt

let _pp_set prefix fmt =
  Pretty_utils.pp_iter ~pre:(prefix ^^ " @[") ~suf:"@]@." ~sep:"@ "
    NSet.iter PdgTypes.Node.pretty fmt


(** The nodes [nodes] define the searched location [z]. If those nodes are calls
    to functions, go inside those calls, and find which nodes are relevant. *)
let rec add_callee_nodes z acc nodes =
  let new_nodes, acc = NSet.fold
      (fun node acc2 ->
         match Pdg.Api.node_key node with
         | PdgIndex.Key.SigCallKey (cid, PdgIndex.Signature.Out out_key) ->
           let callees = Eva.Results.callee (PdgIndex.Key.call_from_id cid) in
           List.fold_left (fun (new_nodes, acc) kf ->
               let callee_pdg = Pdg.Api.get kf in
               let outputs = match out_key with
                 | PdgIndex.Signature.OutLoc out ->
                   (* [out] might be an over-approximation of the location
                      we are searching for. We refine the search if needed. *)
                   let z = Locations.Zone.narrow out z in
                   fst (Pdg.Api.find_location_nodes_at_end callee_pdg z)
                 | PdgIndex.Signature.OutRet -> (* probably never occurs *)
                   fst (Pdg.Api.find_output_nodes callee_pdg out_key)
               in
               let outputs = List.map fst outputs in
               add_list_to_set outputs new_nodes, add_list_to_set outputs acc)
             acc2
             callees
         | _ -> acc2)
      nodes
      (NSet.empty, acc)
  in if NSet.is_empty new_nodes then acc else add_callee_nodes z acc new_nodes

(** [kf] doesn't define all the data that we are looking for: the [undef]
    zone must have been defined in its caller, let's find it. [z] is the
    initial zone that we are looking for, so that we do not look for more
    than it. *)
(* BYTODO: maybe [undef] could be used instead of [z] altogether *)
let rec add_caller_nodes z kf acc (undef, nodes) =
  let join_undef u u' = match u, u' with
    | _, None -> u
    | None, Some _ -> u'
    | Some z, Some z' -> Some (Locations.Zone.join z z')
  in
  let add_one_call_nodes pdg (acc_undef, acc) stmt =
    let acc_undef, acc = match undef with
      | None -> acc_undef, acc
      | Some undef ->
        let nodes_for_undef, undef' =
          Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before:true undef
        in
        let acc_undef = join_undef acc_undef undef' in
        let acc = add_list_to_set (List.map fst nodes_for_undef) acc in
        acc_undef, acc
    in
    let add_call_input_nodes node (acc_undef, acc) =
      match Pdg.Api.node_key node with
      | PdgIndex.Key.SigKey (PdgIndex.Signature.In in_key) ->
        begin match in_key with
          | PdgIndex.Signature.InCtrl ->
            (* We only look for the values *)
            acc_undef, acc
          | PdgIndex.Signature.InNum n_param ->
            let n = Pdg.Api.find_call_input_node pdg stmt n_param in
            acc_undef, NSet.add n acc
          | PdgIndex.Signature.InImpl z' ->
            let z = Locations.Zone.narrow z z' in
            let nodes, undef'= Pdg.Api.find_location_nodes_at_stmt
                pdg stmt ~before:true z
            in
            let acc_undef = join_undef acc_undef undef' in
            acc_undef, add_list_to_set (List.map fst nodes) acc
        end
      | _ -> acc_undef, acc
    in
    NSet.fold add_call_input_nodes nodes (acc_undef, acc)
  in
  let add_one_caller_nodes acc (kf, stmts) =
    let pdg = Pdg.Api.get kf in
    let acc_undef, caller_nodes =
      List.fold_left (add_one_call_nodes pdg) (None, NSet.empty) stmts
    in add_caller_nodes z kf (NSet.union caller_nodes acc) (acc_undef, caller_nodes)
  in List.fold_left add_one_caller_nodes acc (Eva.Results.callsites kf)

let compute_aux kf stmt zone =
  debug1 "[Defs.compute] for %a at sid:%d in '%a'@."
    Locations.Zone.pretty zone stmt.sid Kernel_function.pretty kf;
  try
    let pdg = Pdg.Api.get kf in
    let nodes, undef =
      Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before:true zone
    in
    let nodes = add_list_to_set (List.map fst nodes) NSet.empty  in
    let nodes =
      if Interproc.get () then
        begin
          let caller_nodes = add_caller_nodes zone kf nodes (undef, nodes) in
          add_callee_nodes zone caller_nodes caller_nodes
        end
      else nodes
    in
    Some (nodes, undef)
  with Pdg.Api.Bottom | Pdg.Api.Top | Not_found ->
    None

let compute kf stmt lval =
  let extract (nodes, undef) =
    let add_node node defs =
      match PdgIndex.Key.stmt (Pdg.Api.node_key node) with
      | None -> defs
      | Some s -> Stmt.Hptset.add s defs
    in
    (* select corresponding stmts *)
    let defs = NSet.fold add_node nodes Stmt.Hptset.empty in
    (defs, undef)
  in
  Eva.Analysis.compute ();
  let zone = Eva.Results.(before stmt |> eval_address lval |> as_zone) in
  compute_aux kf stmt zone |> Option.map extract

(* Variation of the function above. For each PDG node that has been found,
   we find whether it directly modifies [zone] through an affectation
   (statements [Set] or [Call (lv, _)], or if the change is indirect
   through the body of a call. *)
let compute_with_def_type_zone kf stmt zone =
  let extract (nodes, undef) =
    let add_node node acc =
      let change stmt (direct, indirect) =
        let (prev_d, pred_i) =
          try Stmt.Map.find stmt acc
          with Not_found -> (false, false)
        in
        let after = (direct || prev_d, indirect || pred_i) in
        Stmt.Map.add stmt after acc
      in
      match Pdg.Api.node_key node with
      | PdgIndex.Key.Stmt s -> change s (true, false)
      | PdgIndex.Key.CallStmt _ -> assert false
      | PdgIndex.Key.SigCallKey (s, sign) ->
        (match sign with
         | PdgIndex.Signature.Out (PdgIndex.Signature.OutRet) ->
           change s (true, false) (* defined by affectation in 'v = f()' *)
         | PdgIndex.Signature.In _ ->
           change s (true, false) (* defined by formal v in 'f(v)' *)
         | PdgIndex.Signature.Out (PdgIndex.Signature.OutLoc _) -> begin
             match s.skind with
             | Instr (Call (_, { enode = Lval (Var vi, NoOffset)}, _, _)
                     | Local_init (_, ConsInit(vi,_,_),_))
               when let kf = Globals.Functions.get vi in
                 Eva.Analysis.use_spec_instead_of_definition kf
               ->
               (* defined through a call, but function has no body *)
               change s (true, false)
             | _ ->
               (* defined within call to a function with a body*)
               change s (false, true)
           end
        )
      | PdgIndex.Key.SigKey _ -> acc
      | s -> Format.printf "## %a@." PdgIndex.Key.pretty s; acc
    in
    let stmts = NSet.fold add_node nodes Stmt.Map.empty in
    (stmts, undef)
  in
  Option.map extract (compute_aux kf stmt zone)

let compute_with_def_type kf stmt lval =
  Eva.Analysis.compute ();
  let zone =
    Eva.Results.(before stmt |> eval_address lval |> as_zone)
  in
  compute_with_def_type_zone kf stmt zone

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

let get_defs = compute

let get_defs_with_type = compute_with_def_type
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