From d8d665b8ba0c33a30960dd44085e055b8fcf81e5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 29 May 2024 13:35:26 +0300 Subject: [PATCH] Implement global widening delay --- src/config/options.schema.json | 19 +++- src/framework/control.ml | 3 +- src/lifters/wideningDelay.ml | 90 ++++++++++++++++--- .../82-widen/01-mine-tutorial-ex4.8-delay.c | 2 +- .../82-widen/02-mihaila-widen-fig7-delay.c | 2 +- tests/regression/82-widen/03-mine14-delay.c | 35 ++++++++ 6 files changed, 135 insertions(+), 16 deletions(-) create mode 100644 tests/regression/82-widen/03-mine14-delay.c diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 3c00660c81..bf2df2f20e 100644 --- a/src/config/options.schema.json +++ b/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 diff --git a/src/framework/control.ml b/src/framework/control.ml index dc1f480675..18130b1aed 100644 --- a/src/framework/control.ml +++ b/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; diff --git a/src/lifters/wideningDelay.ml b/src/lifters/wideningDelay.ml index cd17bebaf9..1cc8585935 100644 --- a/src/lifters/wideningDelay.ml +++ b/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%a" 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 \ No newline at end of file +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%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 (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 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 index 3b9e82b277..d6fb982b82 100644 --- a/tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c +++ b/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 extern _Bool __VERIFIER_nondet_bool(); int main() { diff --git a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c index e5890a80a2..375308851b 100644 --- a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c +++ b/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 diff --git a/tests/regression/82-widen/03-mine14-delay.c b/tests/regression/82-widen/03-mine14-delay.c new file mode 100644 index 0000000000..433bd19d7e --- /dev/null +++ b/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 +#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; +}