Enums: Take care in refinement that no new elements appear

Author: michael-schwarz

src/cdomain/value/cdomains/int/enumsDomain.ml

@@ -349,18 +349,28 @@ 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
     | Inc e, None -> bot_of ik
     | 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 =

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++;
+   }
+ }