From cba4dc2e6f1c7f803dad15603fbcfb3df076ed90 Mon Sep 17 00:00:00 2001 From: Ralf Vogler Date: Tue, 16 Jul 2019 16:46:47 +0200 Subject: [PATCH] add_infl x y for side x y to deal with cycles between globals MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TODO: this makes every y immediately a wpoint :( ~~~ globs.c int a, b; // globals, initial value 0 int main(){ /* 1 */ a = b+1; /* 2 */ b = a+1; } ~~~ Currently does not terminate with td3 b/c of how we do cycle detection in destabilize `./goblint -v --enable ana.int.interval --html --sets solver td3 --enable exp.earlyglobs globs.c` Terminates with td3 with space b/c the cycle is reduced? `./goblint -v --enable ana.int.interval --html --sets solver td3 --enable exp.earlyglobs globs.c --enable exp.solver.td3.space` Terminates with slr3t (b/c of prios) `./goblint -v --enable ana.int.interval --html --sets solver slr3t --enable exp.earlyglobs globs.c` Example for td3 w/o space: // solve 2 // eval 2 1 // infl 1 2 eval 1 b -> [0,0] infl b 1 side 1 a [1,1] -> [0,1] effects (1,a) destabilize ~side:a a // nothing to do yet eval 2 a -> [0,1] infl a 2 side 2 b [1,2] -> [0,2] effects (2,b) destabilize ~side:b b remove stable 1 destabilize ~side:b 1 remove stable 2 destabilize ~side:b 2 add wpoint b // since mem effects (2,b) // 1 and 2 are now not stable, and only b is a wpoint eval 1 b -> [0,2] infl b 1 side 1 a [1,3] -> [0,3] destabilize ~side:a a remove stable 2 destabilize ~side:a 2 eval 2 a -> [0,3] infl a 2 side 2 b [1,4] -> [0,∞] .. // b stable, but a will not become a wpoint and just keep increasing Change: 1. add `infl x y` for each `side x y` 2. make wpoint if `side-var=x` instead of `mem effects (x, side-var)` 3. also only widen for space if wpoint Problem: This makes every y immediately a wpoint :( The following should ideally not widen on g: ~~~ side.c int g; int main(){ /* 1 */ g = 1; /* 2 */ g = 2; /* 3 */ g = 3; } ~~~ --- src/solvers/td3.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 4a9f5ae8..62490c4e 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -35,7 +35,6 @@ module WP = let called = HM.create 10 in let rho = HM.create 10 in let wpoint = HM.create 10 in - let effects = HPM.create 10 in let cache_sizes = ref [] in let add_infl y x = @@ -45,7 +44,7 @@ module WP = let rec destabilize ?side x = if tracing then trace "sol2" "destabilize %a on %i\n" S.Var.pretty_trace x (S.Var.line_nr x); if HM.mem called x then assert (HM.find infl x = VS.empty); (* TODO if this is really true, we can remove the check below *) - Option.may (fun z -> if HPM.mem effects (x,z) then HM.replace wpoint z ()) side; + Option.may (fun z -> if S.Var.equal z x then HM.replace wpoint z ()) side; let w = HM.find_default infl x VS.empty in HM.replace infl x VS.empty; VS.iter (fun y -> @@ -117,7 +116,7 @@ module WP = tmp and side x y d = (* only to variables y w/o rhs *) if tracing then trace "sol2" "side to %a on %i (wpx: %b) ## value: %a\n" S.Var.pretty_trace y (S.Var.line_nr y) (HM.mem rho y) S.Dom.pretty d; - HPM.replace effects (x,y) (); + add_infl x y; if S.system y <> None then ( ignore @@ Pretty.printf "side-effect to unknown w/ rhs: %a, contrib: %a\n" S.Var.pretty_trace y S.Dom.pretty d; ); @@ -136,7 +135,7 @@ module WP = (* assert (S.Dom.leq old j); assert (S.Dom.leq old w); assert (S.Dom.leq j w); *) - HM.replace rho y ((if HM.mem wpoint y || space then S.Dom.widen old else identity) (S.Dom.join old d)); + HM.replace rho y ((if HM.mem wpoint y then S.Dom.widen old else identity) (S.Dom.join old d)); HM.replace stable y (); if HM.mem wpoint y then destabilize y (* we already are a wpoint, so no need to propagate it anymore *)