package frama-c

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

Source file eval.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
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
(**************************************************************************)
(*                                                                        *)
(*  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

(** *)

(* -------------------------------------------------------------------------- *)
(**                       {2 Lattice structure }                              *)
(* -------------------------------------------------------------------------- *)

include Lattice_bounds
include Bottom.Operators


(* -------------------------------------------------------------------------- *)
(**                     {2 Types for the evaluations }                        *)
(* -------------------------------------------------------------------------- *)

(* Forward evaluation. *)
type 't with_alarms = 't * Alarmset.t
type 't evaluated = 't or_bottom with_alarms

(* This monad propagates the `Bottom value if needed and join the potential
   alarms returned during the evaluation. *)
let (>>=) (t, a) f = match t with
  | `Bottom  -> `Bottom, a
  | `Value t -> let t', a' = f t in t', Alarmset.combine a a'

(* Use this monad if the following function returns a simple value. *)
let (>>=:) (t, a) f = match t with
  | `Bottom  -> `Bottom, a
  | `Value t -> let t' = f t in `Value t', a

(* Use this monad if the following function returns no alarms. *)
let (>>=.) (t, a) f = match t with
  | `Bottom  -> `Bottom, a
  | `Value t -> let t' = f t in t', a

(* Backward evaluation. *)
type 'a reduced = [ `Bottom | `Unreduced | `Value of 'a ]

(* -------------------------------------------------------------------------- *)
(**                     {2 Cache for the evaluations }                        *)
(* -------------------------------------------------------------------------- *)

(* State of the reduction of an abstract value. *)
type reductness =
  | Unreduced  (* No reduction. *)
  | Reduced    (* A reduction has been performed for this expression. *)
  | Created    (* The abstract value has been created. *)
  | Dull       (* Reduction is pointless for this expression. *)

(* Right values with 'undefined' and 'escaping addresses' flags. *)
type 'a flagged_value = {
  v: 'a or_bottom;
  initialized: bool;
  escaping: bool;
}

module Flagged_Value = struct

  let bottom = {v = `Bottom; initialized=true; escaping=false; }
  let equal equal v1 v2  =
    Bottom.equal equal v1.v v2.v &&
    v1.initialized = v2.initialized && v1.escaping = v2.escaping
  let join join v1 v2 =
    { v = Bottom.join join v1.v v2.v;
      initialized = v1.initialized && v2.initialized;
      escaping = v1.escaping || v2.escaping }

  let pretty_flags fmt value = match value.initialized, value.escaping with
    | false, true  -> Format.pp_print_string fmt "UNINITIALIZED or ESCAPINGADDR"
    | false, false -> Format.pp_print_string fmt "UNINITIALIZED"
    | true, true   -> Format.pp_print_string fmt "ESCAPINGADDR"
    | true, false  -> Format.pp_print_string fmt "BOTTOM"

  let pretty pp fmt value = match value.v with
    | `Bottom -> pretty_flags fmt value
    | `Value v ->
      if value.initialized && not value.escaping
      then pp fmt v
      else Format.fprintf fmt "%a or %a" pp v pretty_flags value

end

(* Data record associated to each evaluated expression. *)
type ('a, 'origin) record_val = {
  value : 'a flagged_value;  (* The resulting abstract value *)
  origin: 'origin option;   (* The origin of the abstract value *)
  reductness : reductness;  (* The state of reduction. *)
  val_alarms : Alarmset.t   (* The emitted alarms during the evaluation. *)
}

(* Data record associated to each evaluated left-value. *)
type 'a record_loc = {
  loc: 'a;                  (* The location of the left-value. *)
  typ: typ;                 (* *)
  loc_alarms: Alarmset.t    (* The emitted alarms during the evaluation. *)
}

(* Results of an evaluation: the results of all intermediate calculation (the
    value of each expression and the location of each lvalue) are cached in a
    map. *)
module type Valuation = sig
  type t
  type value  (* Abstract value. *)
  type origin (* Origin of values. *)
  type loc    (* Abstract memory location. *)

  val empty : t
  val find : t -> exp -> (value, origin) record_val or_top
  val add : t -> exp -> (value, origin) record_val -> t
  val fold : (exp -> (value, origin) record_val -> 'a -> 'a) -> t -> 'a -> 'a
  val find_loc : t -> lval -> loc record_loc or_top
  val remove : t -> exp -> t
  val remove_loc : t -> lval -> t
end

(* Returns the list of the subexpressions of [expr] that contain [subexpr],
   without [subexpr] itself. *)
let compute_englobing_subexpr ~subexpr ~expr =
  let merge = Extlib.merge_opt (fun _ -> (@)) () in
  (* Returns [Some] of the list of subexpressions of [expr] that contain
     [subexpr], apart [subexpr] itself, or [None] if [subexpr] does not appear
     in [expr]. *)
  let rec compute expr =
    if Cil_datatype.ExpStructEq.equal expr subexpr
    then Some []
    else
      let sublist = match expr.enode with
        | UnOp (_, e, _)
        | CastE (_, e) ->
          compute e
        | BinOp (_, e1, e2, _) ->
          merge (compute e1) (compute e2)
        | Lval (host, offset) ->
          merge (compute_host host) (compute_offset offset)
        | _ -> None
      in
      Option.map (fun l -> expr :: l) sublist
  and compute_host = function
    | Var _ -> None
    | Mem e -> compute e
  and compute_offset offset = match offset with
    | NoOffset -> None
    | Field (_, offset) -> compute_offset offset
    | Index (index, offset) ->
      merge (compute index) (compute_offset offset)
  in
  Option.value ~default:[] (compute expr)

module Englobing =
  Datatype.Pair_with_collections (Cil_datatype.ExpStructEq) (Cil_datatype.ExpStructEq)
    (struct  let module_name = "Subexpressions" end)
module SubExprs = Datatype.List (Cil_datatype.Exp)

module EnglobingSubexpr =
  State_builder.Hashtbl (Englobing.Hashtbl) (SubExprs)
    (struct
      let name = "Value.Eval.Englobing_subexpressions"
      let size = 32
      let dependencies = [ Ast.self ]
    end)

let compute_englobing_subexpr ~subexpr ~expr=
  EnglobingSubexpr.memo
    (fun (expr, subexpr) -> compute_englobing_subexpr ~subexpr ~expr)
    (expr, subexpr)

module Clear_Valuation (Valuation : Valuation) = struct
  let clear_englobing_exprs valuation ~expr ~subexpr =
    let englobing = compute_englobing_subexpr ~subexpr ~expr in
    let remove valuation expr =
      let valuation = Valuation.remove valuation expr in
      match expr.enode with
      | Lval lval -> Valuation.remove_loc valuation lval
      | _ -> valuation
    in
    List.fold_left remove valuation englobing
end


(* -------------------------------------------------------------------------- *)
(**                        {2 Types of assignments }                          *)
(* -------------------------------------------------------------------------- *)

type 'loc left_value = {
  lval: lval;
  lloc: 'loc;
  ltyp: typ;
}

(* Assigned values. *)
type ('loc, 'value) assigned =
  | Assign of 'value
  | Copy of 'loc left_value * 'value flagged_value

let value_assigned = function
  | Assign v -> `Value v
  | Copy (_, copied) -> copied.v

type 'location logic_dependency =
  { term: identified_term;
    direct: bool;
    location: 'location option; }

type 'location logic_assign =
  | Assigns of identified_term * 'location logic_dependency list
  | Allocates of identified_term
  | Frees of identified_term

(* -------------------------------------------------------------------------- *)
(**                       {2 Interprocedural Analysis }                       *)
(* -------------------------------------------------------------------------- *)

type ('loc, 'value) argument = {
  formal: varinfo;
  concrete: exp;
  avalue: ('loc, 'value) assigned;
}

type ('loc, 'value) call = {
  kf: kernel_function;
  callstack: Callstack.t;
  arguments: ('loc, 'value) argument list;
  rest: (exp * ('loc, 'value) assigned) list;
  return: varinfo option;
}

type recursion = {
  depth: int;
  substitution: (varinfo * varinfo) list;
  base_substitution: Base.substitution;
  withdrawal: varinfo list;
  base_withdrawal: Base.Hptset.t;
}

type cacheable = Cacheable | NoCache | NoCacheCallers

(*
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