package goblint

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

Source file sideWPointSelect.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
(** Strategies for widening leaf unknowns *)

open Batteries
open Goblint_constraint.ConstrSys
open Messages

module type S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  sig
    type data

    (** Create data required by this widening point selection strategy.
        The parameters are not necessarily used by all strategies.
        @param is_stable This callback should return whether an unknown is stable.
        @param add_infl  Allows the strategy to record additional influences.
                          This is mainly intended for strategies like unstable-self,
                          which records the influence of a side-effecting unknown x to the leaf y.
    *)
    val create_data: (S.v -> bool) -> (S.v -> S.v -> unit) -> data

    (** Notifies this strategy that a side-effect has occurred.
        This allows the strategy to adapt its internal data structure.
        @param data The internal state of this strategy
        @param x    The optional source of the side-effect
        @param y    The leaf receiving the side-effect
    *)
    val notify_side: data -> S.v option -> S.v -> unit

    (** Whether the destabilization of the side-effected var should record the destabilization
        of called variables and start variables. This information should be passed to [should_mark_wpoint]
        by the solver.
    *)
    val record_destabilized_vs: bool

    (** This strategy can decide to prevent widening.
        Note that, if this strategy does not veto, this does not mean that widening
        will necessarily be performed. Nor does a call to this function imply that
        the value of the leaf has grown.
        @param data      The internal state of this strategy
        @param called    Set of called unknowns
        @param old_sides Prior side-effects to leaf y
        @param x         Optional source of the side-effect
        @param y         Side-effected leaf y
        @return [true]: widening will not be applied; [false]: widening might be applied
    *)
    val veto_widen: data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool

    (** The value of the leaf has grown. Should it be marked a widening point?
        Widening points are widened when their value grows, unless vetoed.
        Even if this function is called, leaf y might already be a widening point
        from an earlier side-effect.
        @param data            The internal state of this strategy
        @param called          Set of called unknowns
        @param old_sides       Prior side-effects to leaf y
        @param x               Optional source of the side-effect
        @param y               Side-effected leaf y
        @param destabilized_vs Optional destabilization info, described in [record_destabilized_vs]
        @return [true]: mark as widening point; [false]: do not mark as widening point

    *)
    val should_mark_wpoint: data -> unit HM.t -> VS.t -> S.v option -> S.v -> bool option -> bool
  end

(** Any side-effect after the first one will be widened which will unnecessarily lose precision. *)
module Always : S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  struct
    type data = unit

    let create_data _ _ = ()
    let notify_side _ _ _ = ()
    let record_destabilized_vs = false
    let veto_widen _ _ _ _ _ = false
    let should_mark_wpoint _ _ _ _ _ _ = true
  end

(* On side-effect cycles, this should terminate via the outer `solver` loop. TODO check. *)
(** Never widen side-effects. *)
module Never : S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  struct
    type data = unit

    let create_data _ _ = ()
    let notify_side _ _ _ = ()
    let record_destabilized_vs = false
    let veto_widen _ _ _ _ _ = false
    let should_mark_wpoint _ _ _ _ _ _ = false
  end

(** Widening check happens by checking sides.
    Only widen if value increases and there has already been a side-effect from the same source *)
module SidesLocal : S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  struct
    type data = unit

    let create_data _ _ = ()
    let notify_side _ _ _ = ()
    let record_destabilized_vs = false
    let veto_widen state called old_sides x y =
      match x with
      | None -> false
      | Some x when VS.mem x old_sides -> false
      | _ -> true
    let should_mark_wpoint _ _ _ _ _ _ = true
  end

(** If there was already a `side x y d` from the same program point and now again, make y a widening point.
    Different from `Sides` in that it will not distinguish between side-effects from different contexts,
    only the program point matters. *)
module SidesPP : S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  struct
    type data = unit
    let create_data _ _ = ()
    let notify_side _ _ _ = ()
    let record_destabilized_vs = false
    let veto_widen state called old_sides x y = false
    let should_mark_wpoint state called old_sides x y _ = match x with
      | Some x ->
        let n = S.Var.node x in
        VS.exists (fun v -> Node.equal (S.Var.node v) n) old_sides
      | None -> false
      (* TODO: This is consistent with the previous implementation, but if multiple side-effects come in with x = None,
          the leaf will never be widened. This is different from SidesLocal *)
  end

(** If there already was a `side x y d` that changed rho[y] and now again, we make y a wpoint.
    x caused more than one update to y. >=3 partial context calls will be precise since sides come from different x. TODO this has 8 instead of 5 phases of `solver` for side_cycle.c *)
module Sides : S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  struct
    type data = unit

    let create_data _ _ = ()
    let notify_side _ _ _ = ()
    let record_destabilized_vs = false
    let veto_widen state called old_sides x y = false
    let should_mark_wpoint state called old_sides x y _ = match x with | Some(x) -> VS.mem x old_sides | None -> true
  end

(* TODO: The following two don't check if a vs got destabilized which may be a problem. *)

(* TODO test/remove. Check for which examples this is problematic! *)
(** Side to y destabilized itself via some infl-cycle. Records influences from unknowns to globals *)
module UnstableSelf : S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  struct
    type data = { is_stable: S.v -> bool; add_infl: S.v -> S.v -> unit }

    let create_data is_stable add_infl = { is_stable; add_infl }
    let notify_side data x y = (match x with None -> () | Some x -> data.add_infl x y)
    let record_destabilized_vs = false
    let veto_widen _ _ _ _ _ = false
    let should_mark_wpoint state called old_sides x y _ = not (state.is_stable y)
  end

(* TODO test/remove. *)
(** Widen if any called var (not just y) is no longer stable. Expensive! *)
module UnstableCalled : S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  struct
    type data = { is_stable: S.v -> bool }

    let create_data is_stable _ = { is_stable }
    let notify_side _ _ _ = ()
    let record_destabilized_vs = false
    let veto_widen state called old_sides y x = false
    let should_mark_wpoint state called old_sides y x _ = HM.exists (fun k _ -> not (state.is_stable k)) called (* this is very expensive since it iterates over called! see https://github.com/goblint/analyzer/issues/265#issuecomment-880748636 *)
  end

(** Destabilized a called or start var. Problem: two partial context calls will be precise, but third call will widen the state.
    If this side destabilized some of the initial unknowns vs, there may be a side-cycle between vs and we should make y a wpoint *)
module Cycle : S =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  functor (VS:Set.S with type elt = S.v) ->
  struct
    type data = unit

    let create_data _ _ = ()
    let notify_side _ _ _ = ()
    let record_destabilized_vs = true
    let veto_widen state called old_sides x y = false
    let should_mark_wpoint state called old_sides x y cycle =
      match cycle with
      | Some cycle ->
        if tracing && cycle then trace "side_widen" "cycle: should mark wpoint %a" S.Var.pretty_trace y;
        cycle
      | None ->
        failwith "destabilize_vs information not provided to side_widen cycle strategy";
  end

let choose_impl: unit -> (module S) = fun () ->
  let conf = GobConfig.get_string "solvers.td3.side_widen" in
  match conf with
  | "always" -> (module Always)
  | "never" -> (module Never)
  | "sides-local" -> (module SidesLocal)
  | "sides" -> (module Sides)
  | "sides-pp" -> (module SidesPP)
  | "unstable-self" -> (module UnstableSelf)
  | "unstable-called" -> (module UnstableCalled)
  | "cycle" -> (module Cycle)
  | _ -> failwith ("Unknown value '" ^ conf ^ "' for option solvers.td3.side_widen!")