package goblint

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

Source file td_simplified_ref.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
(** Top-down solver with side effects. Baseline for comparisons with td_parallel solvers     ([td_simplified_ref]).
    This is the same as ([td_simplified]), but it uses records for solver that instead of multiple hashmaps.
*)

open Batteries
open Goblint_constraint.ConstrSys
open Goblint_constraint.SolverTypes
open Messages

module M = Messages

module Base : GenericEqSolver =
  functor (S:EqConstrSys) ->
  functor (HM:Hashtbl.S with type key = S.v) ->
  struct
    open SolverBox.Warrow (S.Dom)
    include Generic.SolverStats (S) (HM)
    module VS = Set.Make (S.Var)

    type var_data = {
      infl: VS.t;
      value: S.Dom.t;
      wpoint: bool;
      stable: bool;
      called: bool;
    }

    let solve st vs =
      let (data : var_data ref HM.t) = HM.create 10 in

      let () = print_solver_stats := fun () ->
          Logs.debug "|data|=%d" (HM.length data);
      in

      let add_infl y x =
        if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
        let y_ref = HM.find data y in
        y_ref := { !y_ref with infl = VS.add x !y_ref.infl }
      in

      let init (x : S.v): var_data ref =
        let x_ref = HM.find_option data x in
        match x_ref with
        | Some r -> r
        | None ->
          begin
            new_var_event x;
            if tracing then trace "init" "init %a" S.Var.pretty_trace x;
            let data_x = ref { 
                infl = VS.empty;
                value = S.Dom.bot ();
                wpoint = false;
                stable = false;
                called = false 
              } in
            HM.replace data x data_x;
            data_x
          end
      in

      let eq x get set =
        if tracing then trace "eq" "eq %a" S.Var.pretty_trace x;
        match S.system x with
        | None -> S.Dom.bot ()
        | Some f -> f get set
      in

      let rec destabilize x =
        if tracing then trace "destab" "destabilize %a" S.Var.pretty_trace x;
        let x_ref = HM.find data x in
        let w = !x_ref.infl in
        x_ref := { !x_ref with infl = VS.empty };
        VS.iter (fun y ->
            if tracing then trace "destab" "stable remove %a" S.Var.pretty_trace y;
            let y_ref = HM.find data y in
            y_ref := { !y_ref with stable = false };
            destabilize y
          ) w
      in

      let rec query x y =
        let y_ref = init y in
        if tracing then trace "sol_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (!y_ref.stable) (!y_ref.called);
        get_var_event y;
        if not (!y_ref.called) then (
          if S.system y = None then (
            y_ref := { !y_ref with stable = true };
          ) else (
            y_ref := { !y_ref with called = true };
            if tracing then trace "iter" "iterate called from query";
            iterate y;
            y_ref := { !y_ref with called = false };)
        ) else (
          if tracing && not (!y_ref.wpoint) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y;
          y_ref := { !y_ref with wpoint = true };
        );
        let tmp = !y_ref.value in
        add_infl y x;
        if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp;
        tmp

      and side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *)
        assert (S.system y = None);
        let y_ref = init y in
        if tracing then trace "side" "side to %a (wpx: %b) from %a ## value: %a" S.Var.pretty_trace y (!y_ref.wpoint) S.Var.pretty_trace x S.Dom.pretty d;
        let widen a b =
          if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y;
          S.Dom.widen a (S.Dom.join a b)
        in
        let op a b = if !y_ref.wpoint then widen a b else S.Dom.join a b
        in
        let old = !y_ref.value in
        let tmp = op old d in
        y_ref := { !y_ref with stable = true };
        if not (S.Dom.leq tmp old) then (
          if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a: %a -> %a" S.Var.pretty_trace y (!y_ref.wpoint) S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp;
          y_ref := { !y_ref with value = tmp };
          destabilize y;
          (* make y a widening point. This will only matter for the next side _ y.  *)
          if tracing && not (!y_ref.wpoint) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y;
          y_ref := { !y_ref with wpoint = true };
        )

      and iterate x = (* ~(inner) solve in td3*)

        (* begining of iterate*)
        let x_ref = init x in
        if tracing then trace "iter" "iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (!x_ref.called) (!x_ref.stable) (!x_ref.wpoint);
        assert (S.system x <> None);
        if not (!x_ref.stable) then (
          x_ref := { !x_ref with stable = true };
          let wp = !x_ref.wpoint in (* if x becomes a wpoint during eq, checking this will delay widening until next iterate *)
          let eqd = eq x (query x) (side x) in (* d from equation/rhs *)
          let old = !x_ref.value in (* d from older iterate *)
          let wpd = (* d after widen/narrow (if wp) *)
            if not wp then eqd
            else (
              if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
              box old eqd)
          in
          if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( 
            (* old != wpd *)
            if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old);
            update_var_event x old wpd;
            x_ref := { !x_ref with value = wpd };
            destabilize x;
            if tracing then trace "iter" "iterate changed %a" S.Var.pretty_trace x;
            (iterate[@tailcall]) x
          ) else (
            (* old == wpd *)
            if not (!x_ref.stable) then ( 
              (* value unchanged, but not stable, i.e. destabilized itself during rhs *)
              if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
              (iterate[@tailcall]) x
            ) else (
              (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *)
              if tracing && (!x_ref.wpoint) then trace "wpoint" "iterate removing wpoint %a" S.Var.pretty_trace x;
              x_ref := { !x_ref with wpoint = false };
            )
          )
        )
      in

      let set_start (x,d) =
        let x_ref = init x in
        x_ref := { !x_ref with value = d; stable = true };
      in

      (* beginning of main solve *)
      start_event ();

      List.iter set_start st;

      List.iter (fun x -> ignore @@ init x) vs;
      (* If we have multiple start variables vs, we might solve v1, then while solving v2 we side some global which v1 depends on with a new value. Then v1 is no longer stable and we have to solve it again. *)
      let i = ref 0 in
      let rec solver () = (* as while loop in paper *)
        incr i;
        let unstable_vs = List.filter (neg (fun x -> !(HM.find data x).stable)) vs in
        if unstable_vs <> [] then (
          if Logs.Level.should_log Debug then (
            if !i = 1 then Logs.newline ();
            Logs.debug "Unstable solver start vars in %d. phase:" !i;
            List.iter (fun v -> Logs.debug "\t%a" S.Var.pretty_trace v) unstable_vs;
            Logs.newline ();
            flush_all ();
          );
          List.iter (fun x -> 
              let x_ref = HM.find data x in
              x_ref := { !x_ref with called = true };
              if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
              iterate x; 
              x_ref := { !x_ref with called = false } 
            ) unstable_vs;
          solver ();
        )
      in
      solver ();
      (* After termination, only those variables are stable which are
       * - reachable from any of the queried variables vs, or
       * - effected by side-effects and have no constraints on their own (this should be the case for all of our analyses). *)

      stop_event ();
      if Logs.Level.should_log Debug then (
        Logs.debug "Data after iterate completed";
        Logs.debug "|data|=%d" (HM.length data);
      );

      if GobConfig.get_bool "dbg.print_wpoints" then (
        Logs.newline ();
        Logs.debug "Widening points:";
        HM.filter (fun x_ref -> !x_ref.wpoint) data |> HM.iter (fun k x_ref ->
            Logs.debug "%a" S.Var.pretty_trace k)
      );

      HM.map (fun x x_ref -> !x_ref.value) data
  end

let () =
  Selector.add_solver ("td_simplified_ref", (module PostSolver.DemandEqIncrSolverFromEqSolver (Base)));
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