diff --git a/scripts/test-incremental.sh b/scripts/test-incremental.sh index 29198669ac..fa95f25f42 100755 --- a/scripts/test-incremental.sh +++ b/scripts/test-incremental.sh @@ -19,7 +19,7 @@ patch -p0 -b <$patch ./goblint --conf $conf $args --enable incremental.load --set save_run $base/$test-incrementalrun $source &> $base/$test.after.incr.log ./goblint --conf $conf $args --enable incremental.only-rename --set save_run $base/$test-originalrun $source &> $base/$test.after.scratch.log -./goblint --conf $conf --enable solverdiffs --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source +./goblint --conf $conf --disable dbg.compare_runs.glob --enable solverdiffs --compare_runs $base/$test-originalrun $base/$test-incrementalrun $source patch -p0 -b -R <$patch rm -r $base/$test-originalrun $base/$test-incrementalrun diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index a646d9d3a1..88b3dfec18 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -25,6 +25,7 @@ struct module V = struct include Printable.Either (V0) (CilType.Varinfo) + let name () = "access" (* HACK: incremental accesses rely on this! *) let access x = `Left x let vars x = `Right x end diff --git a/src/cdomains/basetype.ml b/src/cdomains/basetype.ml index 4db41612cf..bfe3a592d2 100644 --- a/src/cdomains/basetype.ml +++ b/src/cdomains/basetype.ml @@ -40,8 +40,6 @@ struct | _ -> Local let name () = "variables" let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape (show x)) - let var_id _ = "globals" - let node _ = MyCFG.Function Cil.dummyFunDec let arbitrary () = MyCheck.Arbitrary.varinfo end diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index b71371e051..5183113cf0 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -71,7 +71,7 @@ struct let contexts x = `Right x (* from Basetype.Variables *) - let var_id _ = "globals" + let var_id = show (* HACK: incremental accesses rely on this! *) let node _ = MyCFG.Function Cil.dummyFunDec let pretty_trace = pretty end diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml index 4b6e016f03..9080dbaffc 100644 --- a/src/solvers/postSolver.ml +++ b/src/solvers/postSolver.ml @@ -72,8 +72,11 @@ module Verify: F = struct include Unit (S) (VH) + let accs = VH.create 123 + let init () = - Goblintutil.verified := Some true + Goblintutil.verified := Some true; + VH.clear accs let complain_constraint x ~lhs ~rhs = Goblintutil.verified := Some false; @@ -84,8 +87,18 @@ module Verify: F = ignore (Pretty.printf "Fixpoint not reached at %a\nOrigin: %a\n @[Solver computed:\n%a\nSide-effect:\n%a\nDifference: %a\n@]" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty lhs S.Dom.pretty rhs S.Dom.pretty_diff (rhs, lhs)) let one_side ~vh ~x ~y ~d = - let y_lhs = try VH.find vh y with Not_found -> S.Dom.bot () in - if not (S.Dom.leq d y_lhs) then + (* HACK: incremental accesses insanity! *) + (* ignore (Pretty.printf "one_side %s: %a\n" (S.Var.var_id y) S.Dom.pretty d); *) + let is_acc = String.starts_with (S.Var.var_id y) "access:" in + let y_lhs = + if is_acc && not (VH.mem accs y) then ( + VH.replace accs y (); + S.Dom.bot () + ) + else + try VH.find vh y with Not_found -> S.Dom.bot () + in + if not is_acc && not (S.Dom.leq d y_lhs) then complain_side x y ~lhs:y_lhs ~rhs:d else VH.replace vh y (S.Dom.join y_lhs d) (* HACK: allow warnings/accesses to be added *) diff --git a/tests/incremental/11-restart/12-mutex-simple.c b/tests/incremental/11-restart/12-mutex-simple.c new file mode 100644 index 0000000000..82c1642a93 --- /dev/null +++ b/tests/incremental/11-restart/12-mutex-simple.c @@ -0,0 +1,23 @@ +#include +#include + +int myglobal; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + myglobal=myglobal+1; // RACE! + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&mutex2); + myglobal=myglobal+1; // RACE! + pthread_mutex_unlock(&mutex2); + pthread_join (id, NULL); + return 0; +} diff --git a/tests/incremental/11-restart/12-mutex-simple.json b/tests/incremental/11-restart/12-mutex-simple.json new file mode 100644 index 0000000000..daff0678ce --- /dev/null +++ b/tests/incremental/11-restart/12-mutex-simple.json @@ -0,0 +1,9 @@ +{ + "incremental": { + "restart": { + "sided": { + "enabled": false + } + } + } +} \ No newline at end of file diff --git a/tests/incremental/11-restart/12-mutex-simple.patch b/tests/incremental/11-restart/12-mutex-simple.patch new file mode 100644 index 0000000000..14913c581d --- /dev/null +++ b/tests/incremental/11-restart/12-mutex-simple.patch @@ -0,0 +1,24 @@ +--- tests/incremental/11-restart/12-mutex-simple.c ++++ tests/incremental/11-restart/12-mutex-simple.c +@@ -7,7 +7,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + + void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); +- myglobal=myglobal+1; // RACE! ++ myglobal=myglobal+1; // NORACE + pthread_mutex_unlock(&mutex1); + return NULL; + } +@@ -15,9 +15,9 @@ void *t_fun(void *arg) { + int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); +- pthread_mutex_lock(&mutex2); +- myglobal=myglobal+1; // RACE! +- pthread_mutex_unlock(&mutex2); ++ pthread_mutex_lock(&mutex1); ++ myglobal=myglobal+1; // NORACE ++ pthread_mutex_unlock(&mutex1); + pthread_join (id, NULL); + return 0; + }