package frama-c

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

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

module EdgeLabel = Abstract_state.EdgeLabel

(** Points-to graphs datastructure. *)
module G = Abstract_state.G

type v = G.V.t

let vid = Abstract_state.vid

module LSet = Abstract_state.LSet
module VarSet = Abstract_state.VarSet

module Abstract_state = Abstract_state

let check_computed () =
  if not (Analysis.is_computed ())
  then
    Options.abort "Static analysis must be called before any function of the API can be called"

let get_of_stmt ~stmt empty (get : Abstract_state.t -> 'a) =
  check_computed ();
  match Analysis.get_state_before_stmt stmt with
  | None -> empty
  | Some state -> get state

let lset ~stmt get_set = get_of_stmt ~stmt LSet.empty get_set
let vars ~stmt get_set = get_of_stmt ~stmt VarSet.empty get_set
let get_list ~stmt get = get_of_stmt ~stmt [] get

module Statement = struct
  let points_to_vars ~stmt lv = vars ~stmt (Abstract_state.points_to_vars lv)
  let points_to_lvals ~stmt lv = lset ~stmt (Abstract_state.points_to_lvals lv)
  let alias_sets_vars ~stmt = get_list ~stmt Abstract_state.alias_sets_vars
  let alias_sets_lvals ~stmt = get_list ~stmt Abstract_state.alias_sets_lvals
  let alias_vars ~stmt lv = vars ~stmt (Abstract_state.alias_vars lv)
  let alias_lvals ~stmt lv = lset ~stmt (Abstract_state.alias_lvals lv)
  let aliases = alias_lvals (* deprecated *)

  let new_aliases_lvals ~stmt lv =
    let get_set state =
      let new_state = Analysis.do_stmt state stmt in
      Abstract_state.alias_lvals lv new_state
    in
    lset ~stmt:stmt get_set

  let new_aliases_vars ~stmt lv =
    let get_set state =
      let new_state = Analysis.do_stmt state stmt in
      Abstract_state.alias_vars lv new_state
    in
    vars ~stmt:stmt get_set

  let are_aliased ~stmt (lv1: lval) (lv2:lval) : bool =
    (* TODO: more efficient algorithm: do they share a successor? *)
    LSet.mem lv2 @@ aliases ~stmt lv1
end

let points_to_set_stmt _kf stmt = Statement.points_to_lvals ~stmt

let aliases_stmt _kf stmt = Statement.aliases ~stmt

module Function = struct
  let return_stmt kf =
    if Kernel_function.has_definition kf
    then Kernel_function.find_return kf
    else Options.abort "function %a has no definition" Kernel_function.pretty kf

  let points_to_vars ~kf = Statement.points_to_vars ~stmt:(return_stmt kf)
  let points_to_lvals ~kf = Statement.points_to_lvals ~stmt:(return_stmt kf)
  let alias_sets_vars ~kf = Statement.alias_sets_vars ~stmt:(return_stmt kf)
  let alias_sets_lvals ~kf = Statement.alias_sets_lvals ~stmt:(return_stmt kf)
  let alias_vars ~kf = Statement.alias_vars ~stmt:(return_stmt kf)
  let alias_lvals ~kf = Statement.alias_lvals ~stmt:(return_stmt kf)
  let aliases = alias_lvals (* deprecated *)
  let are_aliased ~kf = Statement.are_aliased ~stmt:(return_stmt kf)

  let fundec_stmts ~kf lv =
    if Kernel_function.has_definition kf
    then
      List.map
        (fun stmt -> stmt, Statement.new_aliases_lvals ~stmt lv)
        (Kernel_function.get_definition kf).sallstmts
    else
      Options.abort "fundec_stmts: function %a has no definition" Kernel_function.pretty kf
end

let points_to_set_kf kf = Function.points_to_lvals ~kf

let aliases_kf kf = Function.aliases ~kf

let fundec_stmts kf = Function.fundec_stmts ~kf


let fold_points_to_set f_fold acc kf s lv =
  LSet.fold (fun e a -> f_fold a e) (points_to_set_stmt kf s lv) acc

let fold_aliases_stmt f_fold acc kf s lv =
  LSet.fold (fun e a -> f_fold a e) (aliases_stmt kf s lv) acc

let fold_new_aliases_stmt f_fold acc _kf s lv =
  LSet.fold (fun e a -> f_fold a e) (Statement.new_aliases_lvals ~stmt:s lv) acc

let fold_points_to_set_kf (f_fold: 'a -> lval -> 'a) (acc: 'a) (kf:kernel_function) (lv:lval) : 'a =
  LSet.fold (fun e a -> f_fold a e) (points_to_set_kf kf lv) acc

let fold_aliases_kf (f_fold : 'a -> lval -> 'a) (acc : 'a) kf lv : 'a =
  LSet.fold (fun e a -> f_fold a e) (aliases_kf kf lv) acc

let fold_fundec_stmts (f_fold: 'a -> stmt -> lval -> 'a) (acc: 'a) (kf:kernel_function) (lv:lval) : 'a =
  List.fold_left
    (fun acc (s, set) ->
       LSet.fold (fun lv a -> f_fold a s lv) set acc
    )
    acc
    (fundec_stmts kf lv)

let are_aliased (_kf: kernel_function) stmt = Statement.are_aliased ~stmt

let fold_vertex (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (_kf: kernel_function) (s:stmt) (lv: lval) : 'a =
  check_computed ();
  match Analysis.get_state_before_stmt s with
    None -> acc
  | Some state ->
    let v : G.V.t = Abstract_state.find_vertex lv state in
    let set_aliases = Abstract_state.find_synonyms lv state in
    LSet.fold (fun lv a -> f_fold a v lv) set_aliases acc

let fold_vertex_closure  (f_fold : 'a -> G.V.t -> lval -> 'a) (acc: 'a) (_kf: kernel_function)  (s:stmt) (lv: lval) : 'a =
  check_computed ();
  match Analysis.get_state_before_stmt s with
    None -> acc
  | Some state ->
    let list_closure : (G.V.t * LSet.t) list = Abstract_state.find_transitive_closure lv state in
    List.fold_left
      (fun acc (i,s) -> LSet.fold (fun lv a -> f_fold a i lv) s acc)
      acc
      list_closure

let get_state_before_stmt _kf =
  Analysis.get_state_before_stmt

let call_function a f res args =
  match Analysis.get_summary f with
    None -> None
  | Some su -> Some(Abstract_state.call a res args su)

let simplify_lval = Simplified.Lval.simplify
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