Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement delayed widening #1483

Open
wants to merge 14 commits into
base: master
Choose a base branch
from
Open
19 changes: 19 additions & 0 deletions src/config/options.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 2 additions & 0 deletions src/framework/control.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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;
Expand Down
1 change: 1 addition & 0 deletions src/goblint_lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
185 changes: 185 additions & 0 deletions src/lifters/wideningDelay.ml
Original file line number Diff line number Diff line change
@@ -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<analysis name=\"widen-delay\">%a</analysis>" 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<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 (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
14 changes: 14 additions & 0 deletions tests/regression/82-widen/01-mine-tutorial-ex4.8-delay.c
Original file line number Diff line number Diff line change
@@ -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 <goblint.h>
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;
}
24 changes: 24 additions & 0 deletions tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
Original file line number Diff line number Diff line change
@@ -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 <goblint.h>
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;
}
25 changes: 25 additions & 0 deletions tests/regression/82-widen/03-mihaila-widen-slide-delay.c
Original file line number Diff line number Diff line change
@@ -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 <goblint.h>

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;
}
35 changes: 35 additions & 0 deletions tests/regression/82-widen/04-mine14-delay.c
Original file line number Diff line number Diff line change
@@ -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;
}
Loading