Implement lookahead widening

src/cdomain/value/cdomains/arrayDomain.ml

@@ -720,6 +720,7 @@ struct
     smart_op (Val.smart_join x1_eval_int x2_eval_int) length x1 x2 x1_eval_int x2_eval_int
 
   let smart_widen_with_length length x1_eval_int x2_eval_int x1 x2  =
+    let x2 = smart_join_with_length length x1_eval_int x2_eval_int x1 x2 in (* TODO: figure out why smart_op requires joined second argument when widening *)
     smart_op (Val.smart_widen x1_eval_int x2_eval_int) length x1 x2 x1_eval_int x2_eval_int
 
   let smart_leq_with_length length x1_eval_int x2_eval_int x1 x2 =

src/config/options.schema.json

@@ -1229,6 +1229,12 @@
                 }
               },
               "additionalProperties": false
+            },
+            "lookahead": {
+              "title": "ana.widen.lookahead",
+              "description": "Use lookahead widening.",
+              "type": "boolean",
+              "default": false
             }
           },
           "additionalProperties": false

src/framework/control.ml

@@ -40,6 +40,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift (get_bool "dbg.slice.on") (module LevelSliceLifter)
       |> lift (get_bool "ana.opt.equal" && not hashcons_enabled) (module OptEqual)
       |> lift hashcons_enabled (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 WideningTokenLifter.Lifter)

src/goblint_lib.ml

@@ -206,6 +206,7 @@ module ContextGasLifter = ContextGasLifter
 module WideningDelay = WideningDelay
 module WideningToken = WideningToken
 module WideningTokenLifter = WideningTokenLifter
+module LookaheadWidening = LookaheadWidening
 
 
 (** {1 Domains}

src/lifters/lookaheadWidening.ml

@@ -0,0 +1,144 @@
+(** 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
+  module Main =
+  struct
+    include Base
+    let name () = "main"
+  end
+  module Pilot =
+  struct
+    include Base
+    let name () = "pilot"
+  end
+  include Printable.Prod (Main) (Pilot)
+
+  let bot () = (Main.bot (), Pilot.bot ())
+  let is_bot (m, p) = Main.is_bot m
+  let top () = (Main.top (), Pilot.top ())
+  let is_top (m, p) = Main.is_top m && Pilot.is_top p
+
+  let leq (m1, p1) (m2, p2) = Main.leq m1 m2 && (not (Main.equal m1 m2) || Pilot.leq p1 p2)
+
+  let op_scheme mop pop (m1, p1) (m2, p2) = (mop m1 m2, pop p1 p2)
+  let join x y = op_scheme Main.join Pilot.join x y
+  let meet = op_scheme Main.meet Pilot.meet (** TODO: Might not be correct *)
+  let widen ((m1, p1) as x) ((m2, p2) as y) =
+    if leq y x then
+      x
+    else if Pilot.leq p2 p1 then
+      (p2, p2)
+    else
+      op_scheme Main.join (fun p1 p2 ->
+          if Pilot.leq p2 p1 then
+            p1 (* ensure stable widening *) (* TODO: is this necessary for us? *)
+          else
+            Pilot.widen p1 p2
+        ) x y
+  let narrow = op_scheme Main.narrow Pilot.narrow (** TODO: Might not be correct *)
+
+  let pretty_diff () ((m1, p1), (m2, p2)) =
+    if Main.leq m1 m2 then
+      Pilot.pretty_diff () (p1, p2)
+    else
+      Main.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 (man: (D.t, G.t, C.t, V.t) man): (S.D.t, S.G.t, S.C.t, S.V.t) man =
+    { man with local = fst man.local
+             ; split = (fun d es -> man.split (d, snd man.local) es)
+    }
+  let convp (man: (D.t, G.t, C.t, V.t) man): (S.D.t, S.G.t, S.C.t, S.V.t) man =
+    { man with local = snd man.local
+             ; split = (fun d es -> man.split (fst man.local, d) es)
+    }
+
+  let context man fd (m, _) = S.context (convm man) fd m
+  let startcontext () = S.startcontext ()
+
+  let lift_fun (man: (D.t, G.t, C.t, V.t) man) g h =
+    let main = h (g (convm man)) in
+    if S.D.is_bot main then D.bot () else
+      let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+      (main, h (g (convp man)))
+  let lift_fun' (man: (D.t, G.t, C.t, V.t) man) g h =
+    let main = h (g (convm man)) in
+    let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+    (main, h (g (convp man)))
+  let lift_fun2 (man: (D.t, G.t, C.t, V.t) man) g h1 h2 =
+    let main = h1 (g (convm man)) in
+    if S.D.is_bot main then D.bot () else
+      let@ () = GobRef.wrap AnalysisState.executing_speculative_computations true in
+      (main, h2 (g (convp man)))
+
+  let sync man reason = lift_fun man S.sync   ((|>) reason)
+  let query man (type a) (q: a Queries.t): a Queries.result = S.query (convm man) q
+  let assign man lv e = lift_fun man S.assign ((|>) e % (|>) lv)
+  let vdecl man v     = lift_fun man S.vdecl  ((|>) v)
+  let branch man e tv = lift_fun man S.branch ((|>) tv % (|>) e)
+  let body man f      = lift_fun man S.body   ((|>) f)
+  let return man r f  = lift_fun man S.return ((|>) f % (|>) r)
+  let asm man         = lift_fun man S.asm    identity
+  let skip man        = lift_fun man S.skip identity
+  let special man r f args = lift_fun man S.special ((|>) args % (|>) f % (|>) r)
+
+  let enter man r f args =
+    M.tracel "LA" "enter: %a" D.pretty man.local;
+    let (l1, l2) = lift_fun' man S.enter ((|>) args % (|>) f % (|>) r) in
+    M.tracel "LA" "enter l1: %a" (Pretty.d_list "\n" D.pretty) l1;
+    M.tracel "LA" "enter l2: %a" (Pretty.d_list "\n" D.pretty) l2;
+    List.map2 (fun (m1, m2) (p1, p2) -> ((m1, p1), (m2, p2))) l1 l2
+  let combine_env man r fe f args fc es f_ask =
+    lift_fun2 man S.combine_env (fun p -> p r fe f args fc (fst es) f_ask) (fun p -> p r fe f args fc (snd es) f_ask)
+  let combine_assign man r fe f args fc es f_ask =
+    lift_fun2 man S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask) (fun p -> p r fe f args fc (snd es) f_ask)
+
+  let threadenter man ~multiple lval f args =
+    let (l1, l2) = lift_fun' man (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval) in
+    List.combine l1 l2
+  let threadspawn man ~multiple lval f args fman =
+    lift_fun2 man (S.threadspawn ~multiple) ((|>) (convm fman) % (|>) args % (|>) f % (|>) lval) ((|>) (convp fman) % (|>) args % (|>) f % (|>) lval)
+
+  let paths_as_set man =
+    let (l1, l2) = lift_fun' man S.paths_as_set Fun.id in
+    List.combine l1 l2
+
+  let event man e oman =
+    lift_fun2 man S.event ((|>) (convm oman) % (|>) e) ((|>) (convp oman) % (|>) e)
+end

tests/regression/82-widen/14-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/15-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/16-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;
+}