From dfaf8a901a8783a52a57bf3e2de34f80445824ea Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Oct 2024 11:18:32 +0300 Subject: [PATCH 01/13] Add creduce script for both branches dead --- scripts/creduce/branches.sh | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100755 scripts/creduce/branches.sh diff --git a/scripts/creduce/branches.sh b/scripts/creduce/branches.sh new file mode 100755 index 0000000000..d509a19576 --- /dev/null +++ b/scripts/creduce/branches.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +set -e + +gcc -c -Werror=implicit-function-declaration ./bad.c + +GOBLINTDIR="/home/simmo/dev/goblint/sv-comp/goblint" +OPTS="--conf $GOBLINTDIR/conf/svcomp.json --set ana.specification $GOBLINTDIR/../sv-benchmarks/c/properties/unreach-call.prp bad.c --enable pre.enabled" +LOG="goblint.log" + +$GOBLINTDIR/goblint $OPTS -v &> $LOG + +grep -F "Both branches dead" $LOG From 36525a96746c47129b0fff7262aff5ab41fc3e39 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 1 Oct 2024 11:18:46 +0300 Subject: [PATCH 02/13] Add reduced congruence both branches dead test --- .../15-congruence-hardness-unsound-branches.c | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c diff --git a/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c b/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c new file mode 100644 index 0000000000..9105e2bf94 --- /dev/null +++ b/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c @@ -0,0 +1,11 @@ +// PARAM: --enable ana.int.congruence --enable ana.int.interval +// reduced (via creduce and manually) from sv-benchmarks/c/hardness-nfm22/hardness_codestructure_dependencies_file-70.c + +main() { + int a; + unsigned c = 1; + if (a) + c = 4; + if (c + (c + 2)) // NOWARN + a = 1; +} From 74f3649eb3deaa2f863fa003bda50b0ac4abc7fe Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 12 Feb 2025 18:57:08 +0100 Subject: [PATCH 03/13] Congruence sub: handle treatment of sub by computing congruence class with which to add. --- src/cdomain/value/cdomains/int/congruenceDomain.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml index 003e33a624..dd2a437a2c 100644 --- a/src/cdomain/value/cdomains/int/congruenceDomain.ml +++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml @@ -319,8 +319,13 @@ struct pretty res ; res - let sub ?(no_ov=false) ik x y = add ~no_ov ik x (neg ~no_ov ik y) - + let sub ?(no_ov=false) ik x y = + match y with + | None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))) + | Some (c, m) -> + let m = m -: c in + let y = Some (c, m) in + add ~no_ov ik x y let sub ?no_ov ik x y = let res = sub ?no_ov ik x y in From 5f1b020f7d6a762ed2f4e89e1c99b6383b6570e7 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 13 Feb 2025 09:56:01 +0100 Subject: [PATCH 04/13] Congruence bug in subtraction: Fix testcase such that it still catches bug, but goes through when it is fixed. --- .../15-congruence-hardness-unsound-branches.c | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c b/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c index 9105e2bf94..7d6ee81e0f 100644 --- a/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c +++ b/tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c @@ -1,11 +1,21 @@ // PARAM: --enable ana.int.congruence --enable ana.int.interval // reduced (via creduce and manually) from sv-benchmarks/c/hardness-nfm22/hardness_codestructure_dependencies_file-70.c +#include + main() { int a; unsigned c = 1; if (a) c = 4; - if (c + (c + 2)) // NOWARN + + // The following condition evaluated to "both branches dead", due to a bug in the congruence domain. + // --- Even though the condition is true the concrete. + if (c + (c + 2)) a = 1; + + // Check that this is reachable. + // That is, check that not both branches of previous condition are dead. + __goblint_check(1); + return 0; } From 98977b10fbbc1cfad79ae981ce16dd12536bf165 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 11:56:34 +0100 Subject: [PATCH 05/13] CongruenceDomain.sub: Handle case when second operand of subtraction is precisely known. --- src/cdomain/value/cdomains/int/congruenceDomain.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml index dd2a437a2c..5cbeffff21 100644 --- a/src/cdomain/value/cdomains/int/congruenceDomain.ml +++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml @@ -323,8 +323,17 @@ struct match y with | None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))) | Some (c, m) -> - let m = m -: c in - let y = Some (c, m) in + let y = + if m =: Z.zero then + if no_ov then + let c = Z.neg c in + Some (c, m) + else + top_of ik + else + let m = m -: c in + Some (c, m) + in add ~no_ov ik x y let sub ?no_ov ik x y = From 829b2bd5b0f63fb0955d5dcbd3bf7e51a7be5441 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 14:52:20 +0100 Subject: [PATCH 06/13] CongruenceDomain: Implement sub idependently of add. --- .../value/cdomains/int/congruenceDomain.ml | 33 ++++++++++--------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml index 5cbeffff21..f0cb8256a9 100644 --- a/src/cdomain/value/cdomains/int/congruenceDomain.ml +++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml @@ -320,21 +320,24 @@ struct res let sub ?(no_ov=false) ik x y = - match y with - | None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))) - | Some (c, m) -> - let y = - if m =: Z.zero then - if no_ov then - let c = Z.neg c in - Some (c, m) - else - top_of ik - else - let m = m -: c in - Some (c, m) - in - add ~no_ov ik x y + let no_ov_case (c1, m1) (c2, m2) = + c1 -: c2, Z.gcd m1 m2 + in + match (x, y) with + | None, None -> bot () + | None, _ + | _, None -> + raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))) + | Some a, Some b when no_ov -> + normalize ik (Some (no_ov_case a b)) + | Some (c1, m1), Some (c2, m2) when m1 =: Z.zero && m2 =: Z.zero && not (Cil.isSigned ik) -> + let _, max_ik = range ik in + let m_ikind = max_ik +: Z.one in + let c = (c1 -: c2 +: m_ikind) %: m_ikind in + Some(c, Z.zero) + | Some a, Some b when not (Cil.isSigned ik) -> + handle_overflow ik (no_ov_case a b) + | _ -> top () let sub ?no_ov ik x y = let res = sub ?no_ov ik x y in From 96bb532c64b0265464fe09d63325e85432ef4227 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 16:45:38 +0100 Subject: [PATCH 07/13] Add test case for unreached fixpoint due to bug in congruences showing with refinement. This is a minimized test case developped in #1671. Co-authored-by: Michael Schwarz --- .../37-congruence/16-refinement-fixpoint.c | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/regression/37-congruence/16-refinement-fixpoint.c diff --git a/tests/regression/37-congruence/16-refinement-fixpoint.c b/tests/regression/37-congruence/16-refinement-fixpoint.c new file mode 100644 index 0000000000..1cdeb7c888 --- /dev/null +++ b/tests/regression/37-congruence/16-refinement-fixpoint.c @@ -0,0 +1,24 @@ +// PARAM: --enable ana.int.bitfield --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval --set ana.int.refinement fixpoint +// FIXPOINT +int main(void) +{ + unsigned int c = 3; + unsigned int d = 6; + unsigned int e = 9; + int burgo; + + while (1) { + c ++; + + d += 2U; + + e += 3U; + + assert(e == (unsigned int )c + d); + + burgo = 23; + } + + return (0); + +} \ No newline at end of file From 958b827704d3d44d2d1d575f69175a4ece78fb61 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 16:58:34 +0100 Subject: [PATCH 08/13] Add test for sub operation for congruence. --- .../37-congruence/17-sub-congruence.c | 28 +++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 tests/regression/37-congruence/17-sub-congruence.c diff --git a/tests/regression/37-congruence/17-sub-congruence.c b/tests/regression/37-congruence/17-sub-congruence.c new file mode 100644 index 0000000000..e51cf217e2 --- /dev/null +++ b/tests/regression/37-congruence/17-sub-congruence.c @@ -0,0 +1,28 @@ +// PARAM: --enable ana.int.congruence --disable ana.int.bitfield --disable ana.int.enums --disable ana.int.interval --disable ana.int.def_exc + +#include +#include + +int main(void) +{ + unsigned x = 0; + unsigned y = 1; + + unsigned int z = x - y; + __goblint_check(UINT_MAX == z); + + int a = 1; + int b = 2; + + int c = a - b; + + __goblint_check(c == -1); + + int min = INT_MIN; + int ov = min - 1; + + __goblint_check(ov == INT_MAX); //UNKNOWN! + + return (0); + +} \ No newline at end of file From b84844b47205bdc0a80f254d3222acb78f4ff082 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 16:59:54 +0100 Subject: [PATCH 09/13] CongruenceDomain.sub: Handle case precisely where two signed numbers are subtracted and do not produce an overflow. --- .../value/cdomains/int/congruenceDomain.ml | 37 +++++++++++-------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml index df30290f9e..c30d6b6d18 100644 --- a/src/cdomain/value/cdomains/int/congruenceDomain.ml +++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml @@ -139,21 +139,21 @@ struct let of_congruence ik (c,m) = normalize ik @@ Some(c,m) - let of_bitfield ik (z,o) = + let of_bitfield ik (z,o) = match BitfieldDomain.Bitfield.to_int (z,o) with | Some x -> normalize ik (Some (x, Z.zero)) | _ -> (* get posiiton of first top bit *) - let tl_zeros = Z.trailing_zeros (Z.logand z o) in - let ik_bits = Size.bit ik in - let m = if tl_zeros > ik_bits then Z.one else Z.pow Z.one tl_zeros in - let c = Z.logand o (m -: Z.one) in + let tl_zeros = Z.trailing_zeros (Z.logand z o) in + let ik_bits = Size.bit ik in + let m = if tl_zeros > ik_bits then Z.one else Z.pow Z.one tl_zeros in + let c = Z.logand o (m -: Z.one) in normalize ik (Some (c, m)) - let to_bitfield ik x = - let x = normalize ik x in - match x with - | None -> (Z.zero, Z.zero) + let to_bitfield ik x = + let x = normalize ik x in + match x with + | None -> (Z.zero, Z.zero) | Some (c,m) -> BitfieldDomain.Bitfield.of_congruence ik (c,m) let maximal t = match t with @@ -347,11 +347,18 @@ struct raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))) | Some a, Some b when no_ov -> normalize ik (Some (no_ov_case a b)) - | Some (c1, m1), Some (c2, m2) when m1 =: Z.zero && m2 =: Z.zero && not (Cil.isSigned ik) -> - let _, max_ik = range ik in + | Some (c1, m1), Some (c2, m2) when m1 =: Z.zero && m2 =: Z.zero -> + let min_ik, max_ik = range ik in let m_ikind = max_ik +: Z.one in - let c = (c1 -: c2 +: m_ikind) %: m_ikind in - Some(c, Z.zero) + if Cil.isSigned ik then + let c = c1 -: c2 in + if c >=: min_ik then + Some (c, Z.zero) + else + top_of ik + else + let c = (c1 -: c2 +: m_ikind) %: m_ikind in + Some (c, Z.zero) | Some a, Some b when not (Cil.isSigned ik) -> handle_overflow ik (no_ov_case a b) | _ -> top () @@ -523,8 +530,8 @@ struct let refine_with_congruence ik a b = meet ik a b - let refine_with_bitfield ik a (z,o) = - let a = normalize ik a in + let refine_with_bitfield ik a (z,o) = + let a = normalize ik a in meet ik a (of_bitfield ik (z,o)) let refine_with_excl_list ik a b = a From f947dcc79f7b607b168b7a2c6b206bcdfb2d6e29 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 17:04:14 +0100 Subject: [PATCH 10/13] Add unknown annotation to assert in test case. --- tests/regression/37-congruence/16-refinement-fixpoint.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/37-congruence/16-refinement-fixpoint.c b/tests/regression/37-congruence/16-refinement-fixpoint.c index 1cdeb7c888..83e79b2287 100644 --- a/tests/regression/37-congruence/16-refinement-fixpoint.c +++ b/tests/regression/37-congruence/16-refinement-fixpoint.c @@ -14,7 +14,7 @@ int main(void) e += 3U; - assert(e == (unsigned int )c + d); + assert(e == (unsigned int )c + d); //UNKNOWN burgo = 23; } From 7a3d072455c4a15ce2f15ff08e99251e9ad4b37b Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 17:08:57 +0100 Subject: [PATCH 11/13] Add comment to test that assert was required to expose fixpoint error. We could not reproduce the error with branching or goblint_check. --- tests/regression/37-congruence/16-refinement-fixpoint.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/37-congruence/16-refinement-fixpoint.c b/tests/regression/37-congruence/16-refinement-fixpoint.c index 83e79b2287..07c7372056 100644 --- a/tests/regression/37-congruence/16-refinement-fixpoint.c +++ b/tests/regression/37-congruence/16-refinement-fixpoint.c @@ -13,7 +13,7 @@ int main(void) d += 2U; e += 3U; - + // To produce the fixpoint not reached error, the following needed to be an assert: assert(e == (unsigned int )c + d); //UNKNOWN burgo = 23; From 3c27e68a8f2f13669cb5f97d7b28e12d298e44f1 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 17:14:33 +0100 Subject: [PATCH 12/13] Congruences: Add testing for overflow in subtraction where result it too large. --- tests/regression/37-congruence/17-sub-congruence.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/tests/regression/37-congruence/17-sub-congruence.c b/tests/regression/37-congruence/17-sub-congruence.c index e51cf217e2..393b60826d 100644 --- a/tests/regression/37-congruence/17-sub-congruence.c +++ b/tests/regression/37-congruence/17-sub-congruence.c @@ -23,6 +23,9 @@ int main(void) __goblint_check(ov == INT_MAX); //UNKNOWN! + int ov2 = 0 - min; + __goblint_check(ov2 == INT_MAX); //UNKNOWN! + return (0); } \ No newline at end of file From a1963daf63f373218d35dc68a50bbfa2d6008e7e Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 24 Feb 2025 17:19:37 +0100 Subject: [PATCH 13/13] Congruencedomain.sub: Check also for upper bound overflow for signed --- src/cdomain/value/cdomains/int/congruenceDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml index c30d6b6d18..63a3271e33 100644 --- a/src/cdomain/value/cdomains/int/congruenceDomain.ml +++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml @@ -352,7 +352,7 @@ struct let m_ikind = max_ik +: Z.one in if Cil.isSigned ik then let c = c1 -: c2 in - if c >=: min_ik then + if c >=: min_ik && c <= max_ik then Some (c, Z.zero) else top_of ik