Implement global widening delay

src/config/options.schema.json

@@ -1129,9 +1129,22 @@
             },
             "delay": {
               "title": "ana.widen.delay",
-              "description": "Delay widenings by count.",
-              "type": "integer",
-              "default": 0
+              "type": "object",
+              "properties": {
+                "local": {
+                  "title": "ana.widen.delay.local",
+                  "description": "Delay local widenings by count.",
+                  "type": "integer",
+                  "default": 0
+                },
+                "global": {
+                  "title": "ana.widen.delay.global",
+                  "description": "Delay global widenings by count.",
+                  "type": "integer",
+                  "default": 0
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false

src/framework/control.ml

@@ -25,7 +25,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       (module MCP.MCP2 : Spec)
       |> lift (get_int "ana.context.gas_value" >= 0) (module ContextGasLifter)
       |> lift true (module WidenContextLifterSide) (* option checked in functor *)
-      |> lift (get_int "ana.widen.delay" > 0) (module WideningDelay.Lifter)
+      |> lift (get_int "ana.widen.delay.local" > 0) (module WideningDelay.DLifter)
       (* hashcons before witness to reduce duplicates, because witness re-uses contexts in domain and requires tag for PathSensitive3 *)
       |> lift (get_bool "ana.opt.hashcons" || arg_enabled) (module HashconsContextLifter)
       |> lift arg_enabled (module HashconsLifter)
@@ -42,6 +42,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
       |> lift true (module LongjmpLifter)
       |> lift termination_enabled (module RecursionTermLifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
+      |> lift (get_int "ana.widen.delay.global" > 0) (module WideningDelay.GLifter)
     )
   in
   GobConfig.building_spec := false;

src/lifters/wideningDelay.ml

@@ -7,15 +7,21 @@ open Batteries
 open Lattice
 open Analyses
 
-module Dom (Base: S) =
+module LocalChainParams: Printable.ChainParams =
 struct
-  module ChainParams =
-  struct
-    let n () = GobConfig.get_int "ana.widen.delay"
-    let names = string_of_int
-  end
-  module Chain = Printable.Chain (ChainParams)
+  let n () = GobConfig.get_int "ana.widen.delay.local"
+  let names = string_of_int
+end
 
+module GlobalChainParams: Printable.ChainParams =
+struct
+  let n () = GobConfig.get_int "ana.widen.delay.global"
+  let names = string_of_int
+end
+
+module Dom (Base: S) (ChainParams: Printable.ChainParams) =
+struct
+  module Chain = Printable.Chain (ChainParams)
   include Printable.Prod (Base) (Chain)
 
   let bot () = (Base.bot (), 0)
@@ -41,11 +47,11 @@ struct
 end
 
 
-module Lifter (S: Spec): Spec =
+module DLifter (S: Spec): Spec =
 struct
   module D =
   struct
-    include Dom (S.D)
+    include Dom (S.D) (LocalChainParams)
 
     let printXml f (b, i) =
       BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" S.D.printXml b Chain.printXml i
@@ -108,4 +114,68 @@ struct
 
   let event ctx e octx =
     lift_fun ctx lift S.event ((|>) (conv octx) % (|>) e)
-end
+end
+
+module GLifter (S: Spec): Spec =
+struct
+  module D = S.D
+  module G =
+  struct
+    include Dom (S.G) (GlobalChainParams)
+
+    let printXml f (b, i) =
+      BatPrintf.fprintf f "%a<analysis name=\"widen-delay\">%a</analysis>" S.G.printXml b Chain.printXml i
+  end
+  module C = S.C
+  module V = S.V
+  module P = S.P
+
+  let name () = S.name () ^ " with widening delay"
+
+  type marshal = S.marshal
+  let init = S.init
+  let finalize = S.finalize
+
+  let startstate v = S.startstate v
+  let exitstate  v = S.exitstate  v
+  let morphstate v d = S.morphstate v d
+
+  let conv (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 global = (fun v -> fst (ctx.global v))
+             ; sideg = (fun v g -> ctx.sideg v (g, 0))
+    }
+
+  let context ctx fd d = S.context (conv ctx) fd d
+  let startcontext () = S.startcontext ()
+
+  let lift_fun ctx f g h =
+    f @@ h (g (conv ctx))
+
+  let lift d = d
+
+  let sync ctx reason = lift_fun ctx lift S.sync   ((|>) reason)
+  let query ctx (type a) (q: a Queries.t): a Queries.result = S.query (conv ctx) q
+  let assign ctx lv e = lift_fun ctx lift S.assign ((|>) e % (|>) lv)
+  let vdecl ctx v     = lift_fun ctx lift S.vdecl  ((|>) v)
+  let branch ctx e tv = lift_fun ctx lift S.branch ((|>) tv % (|>) e)
+  let body ctx f      = lift_fun ctx lift S.body   ((|>) f)
+  let return ctx r f  = lift_fun ctx lift S.return ((|>) f % (|>) r)
+  let asm ctx         = lift_fun ctx lift S.asm    identity
+  let skip ctx        = lift_fun ctx lift S.skip identity
+  let special ctx r f args = lift_fun ctx lift S.special ((|>) args % (|>) f % (|>) r)
+
+  let enter ctx r f args =
+    let liftmap = List.map (Tuple2.mapn lift) in
+    lift_fun ctx liftmap S.enter ((|>) args % (|>) f % (|>) r)
+  let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift S.combine_env (fun p -> p r fe f args fc es f_ask)
+  let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift S.combine_assign (fun p -> p r fe f args fc es f_ask)
+
+  let threadenter ctx ~multiple lval f args = lift_fun ctx (List.map lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
+  let threadspawn ctx ~multiple lval f args fctx = lift_fun ctx lift (S.threadspawn ~multiple) ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
+
+  let paths_as_set ctx =
+    lift_fun ctx Fun.id S.paths_as_set Fun.id
+
+  let event ctx e octx =
+    lift_fun ctx lift S.event ((|>) (conv octx) % (|>) e)
+end

tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c

@@ -1,4 +1,4 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay 1
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 1
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 int main() {

tests/regression/82-widen/02-mihaila-widen-fig7-delay.c

@@ -1,4 +1,4 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay 3
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 3
 // From "Widening as Abstract Domain", Fig. 7: https://doi.org/10.1007/978-3-642-38088-4_12
 // They claim delay 2 (https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf), we need 3 for some reason. Why?
 #include <goblint.h>

tests/regression/82-widen/03-mine14-delay.c

@@ -0,0 +1,35 @@
+// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid --enable ana.int.interval --set ana.widen.delay.local 100 --set ana.widen.delay.global 100
+// Fig 5a from Miné 2014
+#include <pthread.h>
+#include <stdio.h>
+#include <goblint.h>
+
+int x;
+pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int top;
+  while(top) {
+    pthread_mutex_lock(&mutex);
+    if(x<100) {
+      x++;
+    }
+    pthread_mutex_unlock(&mutex);
+  }
+  return NULL;
+}
+
+
+int main(void) {
+  int top, top2;
+
+
+  pthread_t id;
+  pthread_t id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex);
+  __goblint_check(x <= 100);
+  pthread_mutex_unlock(&mutex);
+  return 0;
+}