From 1116ef622f21fb53e82780317c19088c9bad25de Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 24 Sep 2023 14:22:35 +0200 Subject: [PATCH 1/2] No shortcut `meet` and `narrow` w/ int refinement --- src/domains/lattice.ml | 9 +++++++-- .../regression/38-int-refinements/06-narrow.c | 18 ++++++++++++++++++ 2 files changed, 25 insertions(+), 2 deletions(-) create mode 100644 tests/regression/38-int-refinements/06-narrow.c diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml index 4cdaa8fb9f..841d1d61b7 100644 --- a/src/domains/lattice.ml +++ b/src/domains/lattice.ml @@ -151,10 +151,15 @@ end module HConsed (Base:S) = struct include Printable.HConsed (Base) + + (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues *) + (* see https://github.com/goblint/analyzer/issues/1005 *) + let int_refine_active = GobConfig.get_string "ana.int.refinement" <> "never" + let lift_f2 f x y = f (unlift x) (unlift y) - let narrow x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y) + let narrow x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y) let widen x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.widen x y) - let meet x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y) + let meet x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y) let join x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.join x y) let leq x y = (x.BatHashcons.tag == y.BatHashcons.tag) || lift_f2 Base.leq x y let is_top = lift_f Base.is_top diff --git a/tests/regression/38-int-refinements/06-narrow.c b/tests/regression/38-int-refinements/06-narrow.c new file mode 100644 index 0000000000..513e9dde60 --- /dev/null +++ b/tests/regression/38-int-refinements/06-narrow.c @@ -0,0 +1,18 @@ +// PARAM: --set ana.int.refinement fixpoint --enable ana.int.interval +// FIXPOINT +#include + +int g = 0; + +void main() +{ + int i = 0; + while (1) { + i++; + for (int j=0; j < 10; j++) { + if (i > 100) g = 1; + } + if (i>9) i=0; + } + return; +} From 2f691be58f2367cdf2f8fb51e7fcf947b0571df3 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 24 Sep 2023 14:23:42 +0200 Subject: [PATCH 2/2] Make comment a bit longer --- src/domains/lattice.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml index 841d1d61b7..3e1207b8b1 100644 --- a/src/domains/lattice.ml +++ b/src/domains/lattice.ml @@ -152,7 +152,7 @@ module HConsed (Base:S) = struct include Printable.HConsed (Base) - (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues *) + (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *) (* see https://github.com/goblint/analyzer/issues/1005 *) let int_refine_active = GobConfig.get_string "ana.int.refinement" <> "never"