package frama-c

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

Source file from_memory.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
(**************************************************************************)
(*                                                                        *)
(*  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 Locations
module Deps = Eva.Deps

module DepsOrUnassigned = struct
  include Eva.Assigns.DepsOrUnassigned

  let subst f d =
    match d with
    | DepsBottom -> DepsBottom
    | Unassigned -> Unassigned
    | AssignedFrom fd ->
      let fd' = f fd in
      if fd == fd' then d else AssignedFrom fd'
    | MaybeAssignedFrom fd ->
      let fd' = f fd in
      if fd == fd' then d else MaybeAssignedFrom fd'

  let compose d1 d2 =
    match d1, d2 with
    | DepsBottom, _ | _, DepsBottom ->
      DepsBottom (* could indicate dead code. Not used in practice anyway *)
    | Unassigned, _ -> d2
    | AssignedFrom _, _ -> d1
    | MaybeAssignedFrom _, Unassigned -> d1
    | MaybeAssignedFrom d1, MaybeAssignedFrom d2 ->
      MaybeAssignedFrom (Deps.join d1 d2)
    | MaybeAssignedFrom d1, AssignedFrom d2 ->
      AssignedFrom (Deps.join d1 d2)

  (* for backwards compatibility *)
  let pretty fmt fd =
    match fd with
    | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
    | Unassigned -> Format.pp_print_string fmt "(SELF)"
    | AssignedFrom d -> Zone.pretty fmt (Deps.to_zone d)
    | MaybeAssignedFrom d ->
      Format.fprintf fmt "%a (and SELF)" Zone.pretty (Deps.to_zone d)

  let pretty_precise fmt = function
    | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
    | Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
    | AssignedFrom fd -> Deps.pretty_precise fmt fd
    | MaybeAssignedFrom fd ->
      (* '(or UNASSIGNED)' would be a better pretty-printer, we use
         '(and SELF)' only for compatibility reasons *)
      Format.fprintf fmt "%a (and SELF)" Deps.pretty_precise fd
end

include Eva.Assigns.Memory

let bind_var vi v m =
  let z = Locations.zone_of_varinfo vi in
  add_binding ~exact:true m z v

let unbind_var vi m =
  remove_base (Base.of_varinfo vi) m

let map f = map (DepsOrUnassigned.subst f)

let is_unassigned m =
  LOffset.is_same_value m DepsOrUnassigned.Unassigned

(* Unassigned is a neutral value for compose, on both sides *)
let decide_compose m1 m2 =
  if m1 == m2 || is_unassigned m1 then LOffset.ReturnRight
  else if is_unassigned m2 then LOffset.ReturnLeft
  else LOffset.Recurse

let compose_map =
  let cache = Hptmap_sig.PersistentCache "From_memory.compose" in
  (* Partial application is important because of the cache. Idempotent,
     because [compose x x] is always equal to [x]. *)
  map2 ~cache ~symmetric:false ~idempotent:true ~empty_neutral:true
    decide_compose DepsOrUnassigned.compose

let compose m1 m2 = match m1, m2 with
  | Top, _ | _, Top -> Top
  | Map m1, Map m2 -> Map (compose_map m1 m2)
  | Bottom, (Map _ | Bottom) | Map _, Bottom -> Bottom


(* ----- Substitute --------------------------------------------------------- *)

(** Auxiliary function that substitutes the data right-hand part of a
    dependency by a pre-existing From state. The returned result is a Deps.t:
    the data part will be the data part of the complete result, the indirect
    part will be added to the indirect part of the final result. *)
(* This function iterates simultaneously on a From memory, and on a zone.
   It is cached. The definitions below are used to call the function that
   does the recursive descent. *)
let substitute_data_deps =
  (* Nothing left to substitute, return z unchanged *)
  let empty_right z = Deps.data z in
  (* Zone to substitute is empty *)
  let empty_left _ = Deps.bottom in
  (* [b] is in the zone and substituted. Rewrite appropriately *)
  let both b itvs offsm = find_precise_loffset offsm b itvs in
  let join = Deps.join in
  let empty = Deps.bottom in
  let cache = Hptmap_sig.PersistentCache "From_memory.substitute_data" in
  let f_map =
    Zone.fold2_join_heterogeneous
      ~cache ~empty_left ~empty_right ~both ~join ~empty
  in
  fun call_site_froms z ->
    match call_site_froms with
    | Bottom -> Deps.bottom
    | Top -> Deps.top
    | Map m ->
      try f_map z (shape m)
      with Abstract_interp.Error_Top -> Deps.top

(** Auxiliary function that substitutes the indirect right-hand part of a
    dependency by a pre-existing From state. The returned result is a zone,
    which will be added to the indirect part of the final result. *)
let substitute_indirect_deps =
  (* Nothing left to substitute, z is directly an indirect dependency *)
  let empty_right z = z in
  (* Zone to substitute is empty *)
  let empty_left _ = Zone.bottom in
  let both b itvs offsm =
    (* Both the found data and indirect dependencies are computed for indirect
       dependencies: merge to a single zone *)
    Deps.to_zone (find_precise_loffset offsm b itvs)
  in
  let join = Zone.join in
  let empty = Zone.bottom in
  let cache = Hptmap_sig.PersistentCache "From_memory.substitute_indirect" in
  let f_map =
    Zone.fold2_join_heterogeneous
      ~cache ~empty_left ~empty_right ~both ~join ~empty
  in
  fun call_site_froms z ->
    match call_site_froms with
    | Bottom -> Zone.bottom
    | Top -> Zone.top
    | Map m ->
      try f_map z (shape m)
      with Abstract_interp.Error_Top -> Zone.top

let substitute call_site_froms deps =
  let open Deps in
  let { data; indirect } = deps in
  (* depending directly on an indirect dependency -> indirect,
     depending indirectly on a direct dependency  -> indirect *)
  let dirdeps = substitute_data_deps call_site_froms data in
  let inddeps = substitute_indirect_deps call_site_froms indirect in
  let dir = dirdeps.data in
  let ind = Zone.(join dirdeps.indirect inddeps) in
  { data = dir; indirect = ind }


(* ----- Dependency of returned values -------------------------------------- *)

type return = Deps.t

let default_return = Deps.bottom

let top_return = Deps.top

let add_to_return ?start:(_start=0) ~size:_size ?(m=default_return) v =
  Deps.join m v
(*
    let start = Ival.of_int start in
    let itvs = Int_Intervals.from_ival_size start size in
    LOffset.add_iset ~exact:true itvs (DepsOrUnassigned.AssignedFrom v) m
*)

let top_return_size size =
  add_to_return ~size Deps.top

let collapse_return x = x


(* ----- Pretty-printing ---------------------------------------------------- *)

let () = imprecise_write_msg := "dependencies to update"

let pretty_skip = function
  | DepsOrUnassigned.DepsBottom -> true
  | DepsOrUnassigned.Unassigned -> true
  | DepsOrUnassigned.AssignedFrom _ -> false
  | DepsOrUnassigned.MaybeAssignedFrom _ -> false

let pretty =
  pretty_generic_printer
    ~skip_v:pretty_skip ~pretty_v:DepsOrUnassigned.pretty ~sep:"FROM" ()

let pretty_ind_data =
  pretty_generic_printer
    ~skip_v:pretty_skip ~pretty_v:DepsOrUnassigned.pretty_precise ~sep:"FROM"
    ()

(** same as pretty, but uses the type of the function to output more
    precise information.
    @raise Error if the given type is not a function type
*)
let pretty_with_type ~indirect typ fmt assigns =
  let Eva.Assigns.{ memory; return } = assigns in
  let (rt_typ,_,_,_) = Cil.splitFunctionType typ in
  if is_bottom memory
  then Format.fprintf fmt
      "@[NON TERMINATING - NO EFFECTS@]"
  else
    let map_pretty =
      if indirect
      then pretty_ind_data
      else pretty
    in
    if Cil.isVoidType rt_typ
    then begin
      if is_empty memory
      then Format.fprintf fmt "@[NO EFFECTS@]"
      else map_pretty fmt memory
    end
    else
      let pp_space fmt =
        if not (is_empty memory) then
          Format.fprintf fmt "@ "
      in
      Format.fprintf fmt "@[<v>%a%t@[\\result FROM @[%a@]@]@]"
        map_pretty memory pp_space
        (if indirect then Deps.pretty_precise else Deps.pretty) return

let pretty_with_type_indirect = pretty_with_type ~indirect:true
let pretty_with_type = pretty_with_type ~indirect:false
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