diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 43e2ad1d59..533215375e 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1162,6 +1162,25 @@
"description": "Delay widenings using widening tokens.",
"type": "boolean",
"default": false
+ },
+ "delay": {
+ "title": "ana.widen.delay",
+ "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
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 0e4a8b1b5d..fb5de31714 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -26,6 +26,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
(module MCP.MCP2 : Spec)
|> lift (get_int "ana.context.gas_value" >= 0) (ContextGasLifter.get_gas_lifter ())
|> lift true (module WidenContextLifterSide) (* option checked in functor *)
+ |> 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 +43,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
|> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter)
|> lift true (module LongjmpLifter.Lifter)
|> lift termination_enabled (module RecursionTermLifter.Lifter) (* 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;
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 415fb21605..9aa1bb6a24 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -181,6 +181,7 @@ module SpecLifters = SpecLifters
module LongjmpLifter = LongjmpLifter
module RecursionTermLifter = RecursionTermLifter
module ContextGasLifter = ContextGasLifter
+module WideningDelay = WideningDelay
module WideningToken = WideningToken
module WideningTokenLifter = WideningTokenLifter
diff --git a/src/lifters/wideningDelay.ml b/src/lifters/wideningDelay.ml
new file mode 100644
index 0000000000..a47fd5c7a0
--- /dev/null
+++ b/src/lifters/wideningDelay.ml
@@ -0,0 +1,185 @@
+(** Standard widening delay with counters.
+
+ Abstract elements are paired with an integer counter, indicating how many times it has been widened.
+ Lifted abstract elements are only widened if the counter exceeds a predefined limit. *)
+
+open Batteries
+open Lattice
+open Analyses
+
+module LocalChainParams: Printable.ChainParams =
+struct
+ 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)
+ let is_bot (b, _) = Base.is_bot b
+ let top () = (Base.top (), ChainParams.n ())
+ let is_top (b, _) = Base.is_top b
+
+ let leq (b1, _) (b2, _) = Base.leq b1 b2
+
+ (** All operations keep maximal counter. *)
+ let join (b1, i1) (b2, i2) = (Base.join b1 b2, max i1 i2)
+ let meet (b1, i1) (b2, i2) = (Base.meet b1 b2, max i1 i2)
+ let widen (b1, i1) (b2, i2) =
+ let i' = max i1 i2 in
+ if i' < ChainParams.n () then
+ (Base.join b1 b2, i' + 1)
+ else
+ (Base.widen b1 b2, i') (* Don't increase beyond n, otherwise TD3 will not reach fixpoint w.r.t. equal. *)
+ let narrow (b1, i1) (b2, i2) = (Base.narrow b1 b2, max i1 i2)
+
+ let pretty_diff () ((b1, _), (b2, _)) =
+ Base.pretty_diff () (b1, b2) (* Counters cannot violate leq. *)
+end
+
+
+(** Lift {!S} to use widening delay for local states.
+
+ All transfer functions reset the counter to 0, so counting only happens between old and new values at a local unknown. *)
+module DLifter (S: Spec): Spec =
+struct
+ module D =
+ struct
+ include Dom (S.D) (LocalChainParams)
+
+ let printXml f (b, i) =
+ BatPrintf.fprintf f "%a%a" S.D.printXml b Chain.printXml i
+ 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 widening delay"
+
+ type marshal = S.marshal
+ let init = S.init
+ let finalize = S.finalize
+
+ let startstate v = (S.startstate v, 0)
+ let exitstate v = (S.exitstate v, 0)
+ let morphstate v (d, l) = (S.morphstate v d, l)
+
+ let conv (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, 0) es)
+ }
+
+ let context man fd (d, _) = S.context (conv man) fd d
+ let startcontext () = S.startcontext ()
+
+ let lift_fun man f g h =
+ f @@ h (g (conv man))
+
+ let lift d = (d, 0)
+
+ let sync man reason = lift_fun man lift S.sync ((|>) reason)
+ let query man (type a) (q: a Queries.t): a Queries.result = S.query (conv man) q
+ let assign man lv e = lift_fun man lift S.assign ((|>) e % (|>) lv)
+ let vdecl man v = lift_fun man lift S.vdecl ((|>) v)
+ let branch man e tv = lift_fun man lift S.branch ((|>) tv % (|>) e)
+ let body man f = lift_fun man lift S.body ((|>) f)
+ let return man r f = lift_fun man lift S.return ((|>) f % (|>) r)
+ let asm man = lift_fun man lift S.asm identity
+ let skip man = lift_fun man lift S.skip identity
+ let special man r f args = lift_fun man lift S.special ((|>) args % (|>) f % (|>) r)
+
+ let enter man r f args =
+ let liftmap = List.map (Tuple2.mapn lift) in
+ lift_fun man liftmap S.enter ((|>) args % (|>) f % (|>) r)
+ let combine_env man r fe f args fc es f_ask = lift_fun man lift S.combine_env (fun p -> p r fe f args fc (fst es) f_ask)
+ let combine_assign man r fe f args fc es f_ask = lift_fun man lift S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask)
+
+ let threadenter man ~multiple lval f args = lift_fun man (List.map lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
+ let threadspawn man ~multiple lval f args fman = lift_fun man lift (S.threadspawn ~multiple) ((|>) (conv fman) % (|>) args % (|>) f % (|>) lval)
+
+ let paths_as_set man =
+ let liftmap = List.map (fun x -> (x, snd man.local)) in
+ lift_fun man liftmap S.paths_as_set Fun.id
+
+ let event man e oman =
+ lift_fun man lift S.event ((|>) (conv oman) % (|>) e)
+end
+
+(** Lift {!S} to use widening delay for global unknowns. *)
+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%a" 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 (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 global = (fun v -> fst (man.global v))
+ ; sideg = (fun v g -> man.sideg v (g, 0))
+ }
+
+ let context man fd d = S.context (conv man) fd d
+ let startcontext () = S.startcontext ()
+
+ let lift_fun man f g h =
+ f @@ h (g (conv man))
+
+ let lift d = d
+
+ let sync man reason = lift_fun man lift S.sync ((|>) reason)
+ let query man (type a) (q: a Queries.t): a Queries.result = S.query (conv man) q
+ let assign man lv e = lift_fun man lift S.assign ((|>) e % (|>) lv)
+ let vdecl man v = lift_fun man lift S.vdecl ((|>) v)
+ let branch man e tv = lift_fun man lift S.branch ((|>) tv % (|>) e)
+ let body man f = lift_fun man lift S.body ((|>) f)
+ let return man r f = lift_fun man lift S.return ((|>) f % (|>) r)
+ let asm man = lift_fun man lift S.asm identity
+ let skip man = lift_fun man lift S.skip identity
+ let special man r f args = lift_fun man lift S.special ((|>) args % (|>) f % (|>) r)
+
+ let enter man r f args =
+ let liftmap = List.map (Tuple2.mapn lift) in
+ lift_fun man liftmap S.enter ((|>) args % (|>) f % (|>) r)
+ let combine_env man r fe f args fc es f_ask = lift_fun man lift S.combine_env (fun p -> p r fe f args fc es f_ask)
+ let combine_assign man r fe f args fc es f_ask = lift_fun man lift S.combine_assign (fun p -> p r fe f args fc es f_ask)
+
+ let threadenter man ~multiple lval f args = lift_fun man (List.map lift) (S.threadenter ~multiple) ((|>) args % (|>) f % (|>) lval)
+ let threadspawn man ~multiple lval f args fman = lift_fun man lift (S.threadspawn ~multiple) ((|>) (conv fman) % (|>) args % (|>) f % (|>) lval)
+
+ let paths_as_set man =
+ lift_fun man Fun.id S.paths_as_set Fun.id
+
+ let event man e oman =
+ lift_fun man lift S.event ((|>) (conv oman) % (|>) e)
+end
diff --git a/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c b/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
new file mode 100644
index 0000000000..d6fb982b82
--- /dev/null
+++ b/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
@@ -0,0 +1,14 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 1
+#include
+extern _Bool __VERIFIER_nondet_bool();
+int main() {
+ int v = 0;
+ while (__VERIFIER_nondet_bool() == 0) {
+ __goblint_check(0 <= v);
+ __goblint_check(v <= 1);
+ if (v == 0)
+ v = 1;
+ // ...
+ }
+ return 0;
+}
diff --git a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
new file mode 100644
index 0000000000..e0d908ff69
--- /dev/null
+++ b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
@@ -0,0 +1,24 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 1
+// From "Widening as Abstract Domain", Fig. 7: https://doi.org/10.1007/978-3-642-38088-4_12
+// Delay 1:
+// 0. {x -> [0,0], y -> [0,0]}
+// 1. {x -> [0,4], y -> [0,1]} (delay 0 would widen already here)
+// 2. {x -> [0,+inf], y -> [0,1]}
+// narrow: {x -> [0,103], y -> [0,1]}
+#include
+extern _Bool __VERIFIER_nondet_bool();
+
+int main() {
+ int x = 0;
+ int y = 0;
+ while (x < 100) {
+ __goblint_check(0 <= y);
+ __goblint_check(y <= 1);
+ if (__VERIFIER_nondet_bool())
+ y = 1;
+ x = x + 4;
+ }
+ __goblint_check(0 <= y);
+ __goblint_check(y <= 1);
+ return 0;
+}
diff --git a/tests/regression/82-widen/03-mihaila-widen-slide-delay.c b/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
new file mode 100644
index 0000000000..720bcb04d0
--- /dev/null
+++ b/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
@@ -0,0 +1,25 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --set ana.widen.delay.local 3
+// From "Widening as Abstract Domain" slides: https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf
+// They claim delay 2, we need 3:
+// 0. {x -> [0,0], y -> [0,0]}
+// 1. {x -> [0,4], y -> [0,0]}
+// 2. {x -> [0,8], y -> [0,0]}
+// 3. {x -> [0,12], y -> [0,1]} (delay 2 would widen already here)
+// 4. {x -> [0,+inf], y -> [0,1]}
+// narrow: {x -> [0,103], y -> [0,1]}
+#include
+
+int main() {
+ int x = 0;
+ int y = 0;
+ while (x < 100) {
+ __goblint_check(0 <= y);
+ __goblint_check(y <= 1);
+ if (x > 5)
+ y = 1;
+ x = x + 4;
+ }
+ __goblint_check(0 <= y);
+ __goblint_check(y <= 1);
+ return 0;
+}
diff --git a/tests/regression/82-widen/04-mine14-delay.c b/tests/regression/82-widen/04-mine14-delay.c
new file mode 100644
index 0000000000..433bd19d7e
--- /dev/null
+++ b/tests/regression/82-widen/04-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
+#include
+#include
+
+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;
+}