package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file recency.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
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2019 The MOPSA Project.                               *)
(*                                                                          *)
(* This program is free software: 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, either version 3 of the License, or     *)
(* (at your option) any later version.                                      *)
(*                                                                          *)
(* This program 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.                      *)
(*                                                                          *)
(* You should have received a copy of the GNU Lesser General Public License *)
(* along with this program.  If not, see <http://www.gnu.org/licenses/>.    *)
(*                                                                          *)
(****************************************************************************)


(** Abstraction of the heap *)


open Mopsa
open Sig.Abstraction.Domain
open Ast

module Pool =
  Framework.Lattices.Powerset.Make
    (struct
      type t = addr
      let compare = compare_addr
      let print = unformat pp_addr
    end)

type ('a,_) query +=
  | Q_alive_addresses : ('a,addr list) query
  | Q_alive_addresses_aspset : ('a,Pool.t) query
  | Q_allocated_addresses_aspset : ('a,Pool.t) query

let () =
  register_query {
    join = (
      let f : type a r. query_pool -> (a,r) query -> r -> r -> r =
        fun next query a b ->
          match query with
          | Q_alive_addresses -> List.sort_uniq compare_addr (a @ b)
          | Q_alive_addresses_aspset -> Pool.join a b
          | Q_allocated_addresses_aspset -> Pool.join a b
          | _ -> next.pool_join query a b
      in f
    );
    meet = (
      let f : type a r. query_pool -> (a,r) query -> r -> r -> r =
        fun next query a b ->
          match query with
          | Q_alive_addresses -> assert false
          | Q_alive_addresses_aspset -> Pool.meet a b
          | Q_allocated_addresses_aspset -> Pool.meet a b
          | _ -> next.pool_meet query a b
      in f
    );
  }

let name = "universal.heap.recency"

let opt_default_allocation_policy : string ref = ref "range_callstack"
let () = Policies.register_option opt_default_allocation_policy name "-default-alloc-pol" "by default"
           (fun _ ak -> (Policies.of_string !opt_default_allocation_policy) ak)

let gc_time = ref 0.
let gc_nb_collections = ref 0
let gc_nb_addr_collected = ref 0
let gc_max_heap_size = ref 0
(** {2 Domain definition} *)
(** ===================== *)

type stmt_kind +=
   | S_perform_gc

let () =
  register_stmt_with_visitor {
      compare = (fun next s1 s2 ->
        match skind s1, skind s2 with
        | _ -> next s1 s2);

      print = (fun default fmt stmt ->
        match skind stmt with
        | S_perform_gc -> Format.fprintf fmt "Abstract GC call"
        | _ -> default fmt stmt);

      visit = (fun default stmt ->
        match skind stmt with
        | S_perform_gc -> leaf stmt
        | _ -> default stmt);
    }



module Domain =
struct


  (** Domain header *)
  (** ============= *)

  type t = Pool.t

  include GenDomainId(struct
      type nonrec t = t
      let name = name
    end)

  let bottom = Pool.bottom

  let top = Pool.top

  let checks = []

  (** Lattice operators *)
  (** ================= *)

  let is_bottom _ = false

  let subset = Pool.subset

  let join = Pool.join

  let meet = Pool.meet

  let widen ctx = Pool.join

  let merge pre (a,e) (a',e') =
    assert false


  (** Initialization *)
  (** ============== *)

  let init prog man flow = set_env T_cur Pool.empty man flow |> Option.some


  (** Post-conditions *)
  (** *************** *)

  let is_recent addr = addr.addr_mode = STRONG

  let is_old addr = addr.addr_mode = WEAK

  let exec stmt man flow =
    let range = srange stmt in
    match skind stmt with
    (* 𝕊⟦ free(recent); ⟧ *)
    | S_free addr when is_recent addr ->
      let old = { addr with addr_mode = WEAK } in
      get_env T_cur man flow >>$? fun pool flow ->
      (* Inform domains to remove addr *)
      man.exec (mk_remove_addr addr stmt.srange) flow >>%? fun flow' ->
      if not (Pool.mem old pool) then
        (* only recent is present : remove it from the pool and return *)
        map_env T_cur (Pool.remove addr) man flow' |>
        OptionExt.return
      else
        (* old is present : expand it as the new recent *)
        man.exec (mk_expand_addr old [addr] stmt.srange) flow' |>
        OptionExt.return

    (* 𝕊⟦ free(old); ⟧ *)
    | S_free addr when is_old addr ->
       (* Inform domains to invalidate addr *)
       map_env T_cur (Pool.remove addr) man flow >>%? fun flow ->
       man.exec (mk_invalidate_addr addr stmt.srange) flow |>
       OptionExt.return

    | S_perform_gc ->
       let startt = Sys.time () in
       get_env T_cur man flow >>$? fun all flow ->
       let alive = ask_and_reduce man.ask Q_alive_addresses_aspset flow in
       let dead = Pool.diff all alive in
       debug "at %a, |dead| = %d@.dead = %a" pp_range range (Pool.cardinal dead) (format Pool.print) dead;
       let trange = tag_range range "agc" in
       (* let's free weak addresses first, and then the strong ones *)
       let dead_strong, dead_weak = Pool.partition (fun addr -> is_recent addr) dead in
       let post = Pool.fold (fun addr acc ->
                      debug "free %a" pp_addr addr;
                      acc >>% man.exec (mk_stmt (S_free addr) trange)) dead_weak (Post.return flow) in
       post >>% (fun flow ->
       let post = Pool.fold (fun addr acc ->
                      debug "free %a" pp_addr addr;
                      acc >>% man.exec (mk_stmt (S_free addr) trange)) dead_strong (Post.return flow) in
       let delta = Sys.time () -. startt in
       gc_time := !gc_time +. delta;
       incr gc_nb_collections;
       gc_nb_addr_collected := !gc_nb_addr_collected + (Pool.cardinal dead);
       gc_max_heap_size := max !gc_max_heap_size (Pool.cardinal all);
       post) |> OptionExt.return

    | _ -> None


  (** Evaluations *)
  (** *********** *)

  let eval expr man flow =
    let range = erange expr in
    match ekind expr with
    | E_alloc_addr(addr_kind, STRONG) ->
      get_env T_cur man flow >>$? fun pool flow ->

      let recent_addr = Policies.mk_addr addr_kind STRONG range (Flow.get_callstack flow) in

      if not (Pool.mem recent_addr pool) then
        (* first allocation at this site: just add the address to the pool and return it *)
        map_env T_cur (Pool.add recent_addr) man flow >>%? fun flow ->
        Eval.singleton (mk_addr recent_addr range) flow |>
        OptionExt.return
      else
        let old_addr = Policies.mk_addr addr_kind WEAK range (Flow.get_callstack flow) in
        if not (Pool.mem old_addr pool) then
          (* old address not present: rename the existing recent as old and return the new recent *)
          map_env T_cur (Pool.add old_addr) man flow >>%? fun flow ->
          man.exec (mk_rename_addr recent_addr old_addr range) flow >>%? fun flow ->
          Eval.singleton (mk_addr recent_addr range) flow |>
          OptionExt.return
        else
          (* old present : copy the content of the existing recent to old using `fold` statement *)
          man.exec (mk_fold_addr old_addr [recent_addr] range) flow >>%? fun flow ->
          Eval.singleton (mk_addr recent_addr range) flow |>
          OptionExt.return

    | E_alloc_addr(addr_kind, WEAK) ->
      get_env T_cur man flow >>$? fun pool flow ->
      let weak_addr = Policies.mk_addr addr_kind WEAK range (Flow.get_callstack flow) in

      let post =
        if Pool.mem weak_addr pool then
          Post.return flow
        else
          map_env T_cur (Pool.add weak_addr) man flow
      in
      post >>% Eval.singleton (mk_addr weak_addr range) |>
      OptionExt.return


    | _ -> None

  (** Queries *)
  (** ******* *)

  let ask : type r. ('a,r) query -> ('a, t) man -> 'a flow -> ('a, r) cases option =
    fun query man flow ->
    match query with
    | Q_allocated_addresses ->
      get_env T_cur man flow >>$? fun pool flow ->
      if Pool.is_top pool then Some (Cases.singleton [] flow)
      else Some (Cases.singleton (Pool.elements pool) flow)

    | Q_allocated_addresses_aspset ->
      Some (get_env T_cur man flow)

    | _ -> None


  (** Pretty printer *)
  (** ************** *)

  let print_state printer pool =
    pprint printer ~path:[Key "heap"]
      (pbox Pool.print pool)

  let print_expr man flow printer exp = ()


end


let () =
  register_standard_domain (module Domain)
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