From 2917c923a2feba94038a97121f8546e920a1c70f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 12 Feb 2025 10:15:34 +0100 Subject: [PATCH] Enums: Take care in refinement that no new elements appear --- src/cdomain/value/cdomains/int/enumsDomain.ml | 16 +++++++++++++--- tests/regression/38-int-refinements/07-enums.c | 9 +++++++++ 2 files changed, 22 insertions(+), 3 deletions(-) create mode 100644 tests/regression/38-int-refinements/07-enums.c diff --git a/src/cdomain/value/cdomains/int/enumsDomain.ml b/src/cdomain/value/cdomains/int/enumsDomain.ml index d1020cfe2d..e530c16f89 100644 --- a/src/cdomain/value/cdomains/int/enumsDomain.ml +++ b/src/cdomain/value/cdomains/int/enumsDomain.ml @@ -349,6 +349,12 @@ module Enums : S with type int_t = Z.t = struct 10, QCheck.map pos (BISet.arbitrary ()); ] (* S TODO: decide frequencies *) + + (* One needs to be exceedingly careful here to not cause new elements to appear that are not originally tracked by the domain *) + (* to avoid breaking the termination guarantee that only constants from the program can appear in exclusion or inclusion sets here *) + (* What is generally safe is shrinking an inclusion set as no new elements appear here. *) + (* What is not safe is growing an exclusion set or switching from an exclusion set to an inclusion set *) + let refine_with_congruence ik a b = let contains c m x = if Z.equal m Z.zero then Z.equal c x else Z.equal (Z.rem (Z.sub x c) m) Z.zero in match a, b with @@ -356,11 +362,15 @@ module Enums : S with type int_t = Z.t = struct | Inc e, Some (c, m) -> Inc (BISet.filter (contains c m) e) | _ -> a - let refine_with_interval ik a b = a (* TODO: refine inclusion (exclusion?) set *) + let refine_with_interval ik a b = + match a, b with + | Inc _, None -> bot_of ik + | Inc e, Some (l, u) -> Inc (BISet.filter (value_in_range (l,u)) e) + | _ -> a let refine_with_excl_list ik a b = - match b with - | Some (ls, _) -> meet ik a (of_excl_list ik ls) (* TODO: refine with excl range? *) + match a, b with + | Inc _, Some (ls, _) -> meet ik a (of_excl_list ik ls) (* TODO: refine with excl range? *) | _ -> a let refine_with_incl_list ik a b = diff --git a/tests/regression/38-int-refinements/07-enums.c b/tests/regression/38-int-refinements/07-enums.c new file mode 100644 index 0000000000..76f0b9f950 --- /dev/null +++ b/tests/regression/38-int-refinements/07-enums.c @@ -0,0 +1,9 @@ +// PARAM: --set ana.int.refinement fixpoint --enable ana.int.def_exc --enable ana.int.enums --enable ana.int.interval --set sem.int.signed_overflow assume_none +// NOTIMEOUT: Used to not reach terminate (https://github.com/goblint/analyzer/issues/1671) and (https://github.com/goblint/analyzer/issues/1673) +int main() { + int count = 0; + while (1) { + count++; + count++; + } + }