Implement lookahead widening

src/common/framework/analysisState.ml

@@ -36,3 +36,5 @@ let postsolving = ref false
 
 (* None if verification is disabled, Some true if verification succeeded, Some false if verification failed *)
 let verified : bool option ref = ref None
+
+let widening = ref false

src/config/options.schema.json

@@ -1126,6 +1126,12 @@
               "description": "Delay widenings using widening tokens.",
               "type": "boolean",
               "default": false
+            },
+            "lookahead": {
+              "title": "ana.widen.lookahead",
+              "description": "Use lookahead widening.",
+              "type": "boolean",
+              "default": false
             }
           },
           "additionalProperties": false

src/framework/control.ml

@@ -36,6 +36,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift (get_int "dbg.limit.widen" > 0) (module LimitLifter)
       |> lift (get_bool "ana.opt.equal" && not (get_bool "ana.opt.hashcons")) (module OptEqual)
       |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
+      |> lift (get_bool "ana.widen.lookahead") (module LookaheadWidening.Lifter)
       (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
          Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
       |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)

src/goblint_lib.ml

@@ -171,6 +171,16 @@ module AbortUnless = AbortUnless
 module PtranalAnalysis = PtranalAnalysis
 
 
+(** {1 Analysis lifters}
+
+    Transformations of analyses into extended analyses. *)
+
+module WideningTokens = WideningTokens
+module LookaheadWidening = LookaheadWidening
+
+module WitnessConstraints = WitnessConstraints
+
+
 (** {1 Domains}
 
     Domains used by analysis specifications and constraint systems are {{!Lattice.S} lattices}.
@@ -326,7 +336,6 @@ module WitnessUtil = WitnessUtil
     Automaton-based GraphML witnesses used in SV-COMP. *)
 
 module MyARG = MyARG
-module WitnessConstraints = WitnessConstraints
 module ArgTools = ArgTools
 module Witness = Witness
 module Graphml = Graphml
@@ -337,7 +346,6 @@ module Graphml = Graphml
 
 module YamlWitness = YamlWitness
 module YamlWitnessType = YamlWitnessType
-module WideningTokens = WideningTokens
 
 (** {3 Violation}
 

src/lifters/lookaheadWidening.ml

@@ -0,0 +1,130 @@
+(** Lookahead widening.
+
+    @see <https://doi.org/10.1007/11817963_41> Gopan, D., Reps, T. Lookahead Widening. *)
+
+open Batteries
+open Lattice
+open Analyses
+
+module Dom (Base: S) =
+struct
+  include Printable.Prod (Base) (Base)
+
+  let bot () = (Base.bot (), Base.bot ())
+  let is_bot (m, p) = Base.is_bot m
+  let top () = (Base.top (), Base.top ())
+  let is_top (m, p) = Base.is_top m && Base.is_top p
+
+  let leq (m1, p1) (m2, p2) = Base.leq m1 m2 && (not (Base.equal m1 m2) || Base.leq p1 p2)
+
+  let op_scheme mop pop (m1, p1) (m2, p2) = (mop m1 m2, pop p1 p2)
+  let join x y =
+    if !AnalysisState.widening then
+      y
+    else
+      op_scheme Base.join Base.join x y
+  let meet = op_scheme Base.meet Base.meet (** TODO: Might not be correct *)
+  let widen ((m1, p1) as x) ((m2, p2) as y) =
+    if leq y x then
+      x
+    else if Base.leq p2 p1 then
+      (p2, p2)
+    else
+      op_scheme Base.join (fun p1 p2 ->
+          if Base.leq p2 p1 then
+            p1
+          else
+            Base.widen p1 (Base.join p1 p2)
+        ) x y
+  let narrow = op_scheme Base.narrow Base.narrow (** TODO: Might not be correct *)
+
+  let pretty_diff () ((m1, p1), (m2, p2)) =
+    if Base.leq m1 m2 then
+      Base.pretty_diff () (p1, p2)
+    else
+      Base.pretty_diff () (m1, m2)
+end
+
+
+module Lifter (S: Spec): Spec =
+struct
+  module D =
+  struct
+    include Dom (S.D)
+
+    let printXml f (m, p) =
+      BatPrintf.fprintf f "%a%a" S.D.printXml m S.D.printXml p
+  end
+  module G = S.G
+  module C = S.C
+  module V = S.V
+  module P =
+  struct
+    include S.P
+    let of_elt (x, _) = of_elt x
+  end
+
+  let name () = S.name () ^ " with lookahead widening"
+
+  type marshal = S.marshal
+  let init = S.init
+  let finalize = S.finalize
+
+  let startstate v = (S.startstate v, S.startstate v)
+  let exitstate  v = (S.exitstate  v, S.exitstate  v)
+  let morphstate v (m, p) = (S.morphstate v m, S.morphstate v p)
+
+  let convm (ctx: (D.t, G.t, C.t, V.t) ctx): (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
+    { ctx with local = fst ctx.local
+             ; split = (fun d es -> ctx.split (d, snd ctx.local) es)
+    }
+  let convp (ctx: (D.t, G.t, C.t, V.t) ctx): (S.D.t, S.G.t, S.C.t, S.V.t) ctx =
+    { ctx with local = snd ctx.local
+             ; split = (fun d es -> ctx.split (fst ctx.local, d) es)
+    }
+
+  let context ctx fd (m, _) = S.context (convm ctx) fd m
+  let startcontext () = S.startcontext ()
+
+  let lift_fun (ctx: (D.t, G.t, C.t, V.t) ctx) g h =
+    let main = h (g (convm ctx)) in
+    if S.D.is_bot main then D.bot () else
+      (main, h (g (convp ctx)))
+  let lift_fun' (ctx: (D.t, G.t, C.t, V.t) ctx) g h =
+    let main = h (g (convm ctx)) in
+    (main, h (g (convp ctx)))
+  let lift_fun2 (ctx: (D.t, G.t, C.t, V.t) ctx) g h1 h2 =
+    let main = h1 (g (convm ctx)) in
+    if S.D.is_bot main then D.bot () else
+      (main, h2 (g (convp ctx)))
+
+  let sync ctx reason = lift_fun ctx S.sync   ((|>) reason)
+  let query ctx (type a) (q: a Queries.t): a Queries.result = S.query (convm ctx) q
+  let assign ctx lv e = lift_fun ctx S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v     = lift_fun ctx S.vdecl  ((|>) v)
+  let branch ctx e tv = lift_fun ctx S.branch ((|>) tv % (|>) e)
+  let body ctx f      = lift_fun ctx S.body   ((|>) f)
+  let return ctx r f  = lift_fun ctx S.return ((|>) f % (|>) r)
+  let asm ctx         = lift_fun ctx S.asm    identity
+  let skip ctx        = lift_fun ctx S.skip identity
+  let special ctx r f args = lift_fun ctx S.special ((|>) args % (|>) f % (|>) r)
+
+  let enter ctx r f args =
+    let (l1, l2) = lift_fun' ctx S.enter ((|>) args % (|>) f % (|>) r) in
+    List.map2 (fun (m1, m2) (p1, p2) -> ((m1, p1), (m2, p2))) l1 l2
+  let combine_env ctx r fe f args fc es f_ask = lift_fun ctx S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
+  let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
+
+  let threadenter ctx ~multiple lval f args =
+    let (l1, l2) = lift_fun' ctx (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) in
+    List.combine l1 l2
+  let threadspawn ctx ~multiple lval f args fctx =
+    lift_fun2 ctx (S.threadspawn ~multiple) ((|>) (convm fctx) % (|>) args % (|>) f % (|>) lval) ((|>) (convp fctx) % (|>) args % (|>) f % (|>) lval)
+
+  let paths_as_set ctx =
+    let (l1, l2) = lift_fun' ctx S.paths_as_set Fun.id in
+    List.combine l1 l2
+
+  let event ctx e octx =
+    lift_fun2 ctx S.event ((|>) (convm octx) % (|>) e) ((|>) (convp octx) % (|>) e)
+end

src/solver/td3.ml

@@ -323,7 +323,11 @@ module Base =
             if not wp then eqd
             else if term then
               match phase with
-              | Widen -> S.Dom.widen old (S.Dom.join old eqd)
+              | Widen ->
+                AnalysisState.widening := true;
+                let r = S.Dom.widen old (S.Dom.join old eqd) in
+                AnalysisState.widening := false;
+                r
               | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *)
               | Narrow ->
                 (* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *) *)

tests/regression/82-widen/10-gopan-reps-fig1-std.c

@@ -0,0 +1,29 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none
+// From "Lookahead Widening", Fig. 1: https://doi.org/10.1007/11817963_41
+// Checks that require no narrowing or lookahead
+#include <goblint.h>
+
+int main() {
+  int x, y;
+  x = 0;
+  y = 0;
+  while (1) {
+    // n_1
+    __goblint_check(y <= x);
+    if (x <= 50)
+      y++;
+    else
+      y--;
+    if (y < 0)
+      break;
+    x++;
+    // n_6
+    __goblint_check(x >= 0);
+    __goblint_check(y >= 0);
+    __goblint_check(y <= x);
+  }
+  // n_x
+  __goblint_check(y <= -1);
+  __goblint_check(x >= y - 1);
+  return 0;
+}

tests/regression/82-widen/11-gopan-reps-fig1-narrow.c

@@ -0,0 +1,32 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none
+// From "Lookahead Widening", Fig. 1: https://doi.org/10.1007/11817963_41
+// Checks that also require narrowing, but no lookahead
+#include <goblint.h>
+
+int main() {
+  int x, y;
+  x = 0;
+  y = 0;
+  while (1) {
+    // n_1
+    __goblint_check(x >= 0); // TODO (needs narrow)
+    __goblint_check(y >= 0); // TODO (needs narrow)
+    __goblint_check(y <= x);
+    if (x <= 50)
+      y++;
+    else
+      y--;
+    if (y < 0)
+      break;
+    x++;
+    // n_6
+    __goblint_check(x >= 1); // TODO (needs narrow)
+    __goblint_check(y >= 0);
+    __goblint_check(y <= x);
+    __goblint_check(51 * y >= 51 - 2 * (x - 1)); // TODO (needs narrow)
+  }
+  // n_x
+  __goblint_check(x >= 51); // TODO (needs narrow)
+  __goblint_check(y == -1); // TODO (needs narrow)
+  return 0;
+}

tests/regression/82-widen/12-gopan-reps-fig1-lookahead.c

@@ -0,0 +1,39 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none --enable ana.widen.lookahead
+// From "Lookahead Widening", Fig. 1: https://doi.org/10.1007/11817963_41
+// Checks that also require lookahead, but no narrowing
+#include <goblint.h>
+
+int main() {
+  int x, y;
+  x = 0;
+  y = 0;
+  while (1) {
+    // n_1
+    __goblint_check(x >= 0); // needs lookahead
+    __goblint_check(x <= 102); // needs lookahead
+    __goblint_check(y >= 0); // needs lookahead
+    __goblint_check(y <= 51); // needs lookahead
+    __goblint_check(y <= x);
+    __goblint_check(x + y <= 102); // needs lookahead
+    if (x <= 50)
+      y++;
+    else
+      y--;
+    if (y < 0)
+      break;
+    x++;
+    // n_6
+    __goblint_check(x >= 1); // needs lookahead
+    __goblint_check(x <= 102); // needs lookahead
+    __goblint_check(y >= 0);
+    __goblint_check(y <= 51); // needs lookahead
+    __goblint_check(y <= x);
+    __goblint_check(x + y <= 102); // needs lookahead
+    __goblint_check(51 * y >= 51 - 2 * (x - 1)); // needs lookahead
+  }
+  // n_x
+  __goblint_check(x >= 51); // needs lookahead
+  __goblint_check(x <= 102); // needs lookahead
+  __goblint_check(y == -1); // needs lookahead
+  return 0;
+}