diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index d8fe147d67..3bf81b1ba1 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -559,6 +559,19 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct let to_int (x1, x2) = if Ints_t.equal x1 x2 then Some x1 else None + + let upper_threshold u max_ik = + let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in + let u = Ints_t.to_bigint u in + let max_ik' = Ints_t.to_bigint max_ik in + let t = List.find_opt (fun x -> Z.compare u x <= 0 && Z.compare x max_ik' <= 0) ts in + BatOption.map_default Ints_t.of_bigint max_ik t + let lower_threshold l min_ik = + let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in + let l = Ints_t.to_bigint l in + let min_ik' = Ints_t.to_bigint min_ik in + let t = List.find_opt (fun x -> Z.compare l x >= 0 && Z.compare x min_ik' >= 0) ts in + BatOption.map_default Ints_t.of_bigint min_ik t end module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option = @@ -668,22 +681,16 @@ struct | Some (l0,u0), Some (l1,u1) -> let (min_ik, max_ik) = range ik in let threshold = get_interval_threshold_widening () in - let upper_threshold u = - let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in - let u = Ints_t.to_bigint u in - let t = List.find_opt (fun x -> Z.compare u x <= 0) ts in - BatOption.map_default Ints_t.of_bigint max_ik t + let l2 = + if Ints_t.compare l0 l1 = 0 then l0 + else if threshold then IArith.lower_threshold l1 min_ik + else min_ik in - let lower_threshold l = - let ts = if get_interval_threshold_widening_constants () = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in - let l = Ints_t.to_bigint l in - let t = List.find_opt (fun x -> Z.compare l x >= 0) ts in - BatOption.map_default Ints_t.of_bigint min_ik t + let u2 = + if Ints_t.compare u0 u1 = 0 then u0 + else if threshold then IArith.upper_threshold u1 max_ik + else max_ik in - let lt = if threshold then lower_threshold l1 else min_ik in - let l2 = if Ints_t.compare l0 l1 = 0 then l0 else Ints_t.min l1 (Ints_t.max lt min_ik) in - let ut = if threshold then upper_threshold u1 else max_ik in - let u2 = if Ints_t.compare u0 u1 = 0 then u0 else Ints_t.max u1 (Ints_t.min ut max_ik) in norm ik @@ Some (l2,u2) |> fst let widen ik x y = let r = widen ik x y in @@ -1394,18 +1401,8 @@ struct let widen ik xs ys = let (min_ik,max_ik) = range ik in let threshold = get_bool "ana.int.interval_threshold_widening" in - let upper_threshold (_,u) = - let ts = if GobConfig.get_string "ana.int.interval_threshold_widening_constants" = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in - let u = Ints_t.to_bigint u in - let t = List.find_opt (fun x -> Z.compare u x <= 0) ts in - BatOption.map_default Ints_t.of_bigint max_ik t - in - let lower_threshold (l,_) = - let ts = if GobConfig.get_string "ana.int.interval_threshold_widening_constants" = "comparisons" then WideningThresholds.lower_thresholds () else ResettableLazy.force widening_thresholds_desc in - let l = Ints_t.to_bigint l in - let t = List.find_opt (fun x -> Z.compare l x >= 0) ts in - BatOption.map_default Ints_t.of_bigint min_ik t - in + let upper_threshold (_,u) = IArith.upper_threshold u max_ik in + let lower_threshold (l,_) = IArith.lower_threshold l min_ik in (*obtain partitioning of xs intervals according to the ys interval that includes them*) let rec interval_sets_to_partitions (ik: ikind) (acc : (int_t * int_t) option) (xs: t) (ys: t)= match xs,ys with diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml index 288d8f9337..e697b022eb 100644 --- a/tests/unit/cdomains/intDomainTest.ml +++ b/tests/unit/cdomains/intDomainTest.ml @@ -198,22 +198,35 @@ let test_ex_set _ = assert_equal (Some true) (T.to_bool tex10); assert_equal None (T.to_bool tex1) -module Interval = +module IntervalTest (I : IntDomain.SOverflow with type int_t = Z.t) = struct - module I = IntDomain.SOverflowUnlifter(IntDomain.Interval) + module I = IntDomain.SOverflowUnlifter (I) + let ik = Cil.IInt + let i65536 = I.of_interval ik (Z.zero, of_int 65536) + let i65537 = I.of_interval ik (Z.zero, of_int 65537) + let imax = I.of_interval ik (Z.zero, of_int 2147483647) let assert_equal x y = assert_equal ~cmp:I.equal ~printer:I.show x y let test_interval_rem _ = - let ik = Cil.IInt in assert_equal (I.of_int ik Z.zero) (I.rem ik (I.of_int ik Z.minus_one) (I.of_int ik Z.one)) + let test_interval_widen _ = + GobConfig.set_bool "ana.int.interval_threshold_widening" true; + GobConfig.set_string "ana.int.interval_threshold_widening_constants" "comparisons"; + assert_equal imax (I.widen ik i65536 i65537); + assert_equal imax (I.widen ik i65536 imax) + let test () = [ "test_interval_rem" >:: test_interval_rem; + "test_interval_widen" >:: test_interval_widen; ] end +module Interval = IntervalTest (IntDomain.Interval) +module IntervalSet = IntervalTest (IntDomain.IntervalSet) + module Congruence = struct module C = IntDomain.Congruence @@ -291,6 +304,7 @@ let test () = "test_meet" >:: test_meet; "test_excl_list">:: test_ex_set; "interval" >::: Interval.test (); + "intervalSet" >::: IntervalSet.test (); "congruence" >::: Congruence.test (); "intDomTuple" >::: IntDomTuple.test (); ]