From 24760f564f94ea2ecbd903ed169f0a6a97ae6293 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 10 Apr 2024 12:24:55 +0200 Subject: [PATCH 01/11] Use range in `of_interval` --- src/cdomain/value/cdomains/intDomain.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 6c67279044..ffd68a458c 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2074,7 +2074,14 @@ struct | _ -> None let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L)) - let of_interval ?(suppress_ovwarn=false) ik (x,y) = if Z.compare x y = 0 then of_int ik x else top_of ik + let of_interval ?(suppress_ovwarn=false) ik (x,y) = + if Z.compare x y = 0 then + of_int ik x + else + let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in + let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in + let ex = if Z.geq x Z.zero || Z.leq y Z.zero then S.singleton Z.zero else S.empty () in + (`Excluded (ex, r)) let starting ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero > 0 then not_zero ikind else top_of ikind let ending ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero < 0 then not_zero ikind else top_of ikind From b3a33c3eb1f98d3d599b0c90c7d899369c20163b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 11 Apr 2024 11:21:26 +0200 Subject: [PATCH 02/11] Fix stupid mistake --- src/cdomain/value/cdomains/intDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index ffd68a458c..2dc6fcdbdc 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2080,7 +2080,7 @@ struct else let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in - let ex = if Z.geq x Z.zero || Z.leq y Z.zero then S.singleton Z.zero else S.empty () in + let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in (`Excluded (ex, r)) let starting ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero > 0 then not_zero ikind else top_of ikind From bb4c7ff132d515b80194c8a7fbb6c7cd47b6986b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 11 Apr 2024 11:22:24 +0200 Subject: [PATCH 03/11] Apply norm --- src/cdomain/value/cdomains/intDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 2dc6fcdbdc..5de5726442 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2081,7 +2081,7 @@ struct let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in - (`Excluded (ex, r)) + norm ik @@ (`Excluded (ex, r)) let starting ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero > 0 then not_zero ikind else top_of ikind let ending ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero < 0 then not_zero ikind else top_of ikind From b094bbf13d6f8d1c4beb1b033b4576d9840201bd Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 11 Apr 2024 11:24:18 +0200 Subject: [PATCH 04/11] Pass overflow flag --- src/cdomain/value/cdomains/intDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 5de5726442..1168a06653 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2079,7 +2079,7 @@ struct of_int ik x else let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in - let r = R.join (R.of_interval range_ikind a) (R.of_interval range_ikind b) in + let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval range_ikind b) in let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in norm ik @@ (`Excluded (ex, r)) From a5d8723d989b2eb5d7b99f7164545bc64072f213 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Apr 2024 14:04:55 +0200 Subject: [PATCH 05/11] Use ranges in starting & ending --- src/cdomain/value/cdomains/intDomain.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 1168a06653..778c138d5e 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2083,8 +2083,13 @@ struct let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in norm ik @@ (`Excluded (ex, r)) - let starting ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero > 0 then not_zero ikind else top_of ikind - let ending ?(suppress_ovwarn=false) ikind x = if Z.compare x Z.zero < 0 then not_zero ikind else top_of ikind + let starting ?(suppress_ovwarn=false) ikind x = + let _,u_ik = Size.range ikind in + of_interval ~suppress_ovwarn ikind (x, u_ik) + + let ending ?(suppress_ovwarn=false) ikind x = + let l_ik,_ = Size.range ikind in + of_interval ~suppress_ovwarn ikind (l_ik, x) let of_excl_list t l = let r = size t in (* elements in l are excluded from the full range of t! *) From 86a4cc7173495fa2c0a6baebb3e765afc95f2ed9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Apr 2024 15:26:49 +0200 Subject: [PATCH 06/11] Add test --- tests/regression/01-cpa/75-refine-def-exc.c | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/regression/01-cpa/75-refine-def-exc.c diff --git a/tests/regression/01-cpa/75-refine-def-exc.c b/tests/regression/01-cpa/75-refine-def-exc.c new file mode 100644 index 0000000000..85af0a8f02 --- /dev/null +++ b/tests/regression/01-cpa/75-refine-def-exc.c @@ -0,0 +1,16 @@ +//PARAM: +#include +#include +#include + +int main () { + // Needs to be unsigned as we create ranges corresponding to types and ending for signed + // means we have int as there are no types containing only negative numbers + unsigned int r; + + if(r < 1024) { + __goblint_check(r <= 32768); + } + + return 0; +} From a5df5e44fda09d602c4a7c2c84ae9e313fc12978 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Apr 2024 15:49:23 +0200 Subject: [PATCH 07/11] Enums: `of_interval`, `starting`, `ending` like in DefExc --- src/cdomain/value/cdomains/intDomain.ml | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 778c138d5e..7b650282b4 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2503,7 +2503,14 @@ module Enums : S with type int_t = Z.t = struct let of_int ikind x = cast_to ikind (Inc (BISet.singleton x)) - let of_interval ?(suppress_ovwarn=false) ik (x,y) = if x = y then of_int ik x else top_of ik + let of_interval ?(suppress_ovwarn=false) ik (x, y) = + if Z.compare x y = 0 then + of_int ik x + else + let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in + let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval range_ikind b) in + let ex = if Z.gt x Z.zero || Z.lt y Z.zero then BISet.singleton Z.zero else BISet.empty () in + norm ik @@ (Exc (ex, r)) let join ik = curry @@ function | Inc x, Inc y -> Inc (BISet.union x y) @@ -2638,8 +2645,13 @@ module Enums : S with type int_t = Z.t = struct let is_excl_list = BatOption.is_some % to_excl_list let to_incl_list = function Inc s when not (BISet.is_empty s) -> Some (BISet.elements s) | _ -> None - let starting ?(suppress_ovwarn=false) ikind x = top_of ikind - let ending ?(suppress_ovwarn=false) ikind x = top_of ikind + let starting ?(suppress_ovwarn=false) ikind x = + let _,u_ik = Size.range ikind in + of_interval ~suppress_ovwarn ikind (x, u_ik) + + let ending ?(suppress_ovwarn=false) ikind x = + let l_ik,_ = Size.range ikind in + of_interval ~suppress_ovwarn ikind (l_ik, x) let c_lognot ik x = if is_bot x From cd50f0cbc5be0150345339f79d4303ba924ad47b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 12 Apr 2024 16:15:11 +0200 Subject: [PATCH 08/11] Forgot promote --- tests/regression/cfg/foo.t/run.t | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t index 6dcb21863e..9ef307b1d9 100644 --- a/tests/regression/cfg/foo.t/run.t +++ b/tests/regression/cfg/foo.t/run.t @@ -67,7 +67,7 @@ total lines: 6 [Warning][Deadcode][CWE-571] condition 'a > 0' (possibly inserted by CIL) is always true (foo.c:3:10-3:20) [Info][Witness] witness generation summary: - total generation entries: 13 + total generation entries: 15 $ yamlWitnessStrip < witness.yml - entry_type: loop_invariant @@ -125,6 +125,17 @@ string: 1 <= a type: assertion format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 7 + column: 2 + function: main + location_invariant: + string: 0 <= a + type: assertion + format: C - entry_type: location_invariant location: file_name: foo.c @@ -213,3 +224,14 @@ string: 1 <= a type: assertion format: C + - entry_type: location_invariant + location: + file_name: foo.c + file_hash: $FILE_HASH + line: 4 + column: 4 + function: main + location_invariant: + string: 0 <= a + type: assertion + format: C From 79ba3981e76c31a3f25cfc5a1572cf30f9b5ae0d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 15 Apr 2024 10:51:07 +0200 Subject: [PATCH 09/11] 01/75: Make more explicit that `DefExc` is tested Co-authored-by: Simmo Saan --- tests/regression/01-cpa/75-refine-def-exc.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/01-cpa/75-refine-def-exc.c b/tests/regression/01-cpa/75-refine-def-exc.c index 85af0a8f02..244ec986b1 100644 --- a/tests/regression/01-cpa/75-refine-def-exc.c +++ b/tests/regression/01-cpa/75-refine-def-exc.c @@ -1,4 +1,4 @@ -//PARAM: +//PARAM: --enable ana.int.def_exc --disable ana.int.interval #include #include #include From 2f4f50daf8eb09d7c610bbc8950543b6275e870a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 15 Apr 2024 10:51:41 +0200 Subject: [PATCH 10/11] Pass `~suppress_ovwarn` to both `of_interval` calls Co-authored-by: Simmo Saan --- src/cdomain/value/cdomains/intDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 7b650282b4..2010731585 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2079,7 +2079,7 @@ struct of_int ik x else let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in - let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval range_ikind b) in + let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval ~suppress_ovwarn range_ikind b) in let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else S.empty () in norm ik @@ (`Excluded (ex, r)) From 4b0b7c39b10a654793a29041171d190d34fe26c7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 15 Apr 2024 10:51:51 +0200 Subject: [PATCH 11/11] Pass `~suppress_ovwarn` to both `of_interval` calls Co-authored-by: Simmo Saan --- src/cdomain/value/cdomains/intDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml index 2010731585..0a850b03a3 100644 --- a/src/cdomain/value/cdomains/intDomain.ml +++ b/src/cdomain/value/cdomains/intDomain.ml @@ -2508,7 +2508,7 @@ module Enums : S with type int_t = Z.t = struct of_int ik x else let a, b = Size.min_range_sign_agnostic x, Size.min_range_sign_agnostic y in - let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval range_ikind b) in + let r = R.join (R.of_interval ~suppress_ovwarn range_ikind a) (R.of_interval ~suppress_ovwarn range_ikind b) in let ex = if Z.gt x Z.zero || Z.lt y Z.zero then BISet.singleton Z.zero else BISet.empty () in norm ik @@ (Exc (ex, r))