Unsound congruence domain arithmetic

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

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
@@ -336,8 +336,32 @@ 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 =
+    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 ->
+      let min_ik, max_ik = range ik in
+      let m_ikind = max_ik +: Z.one in
+      if Cil.isSigned ik then
+        let c = c1 -: c2 in
+        if c >=: min_ik && c <= max_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 ()
 
   let sub ?no_ov ik x y =
     let res = sub ?no_ov ik x y in
@@ -506,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

tests/regression/37-congruence/15-congruence-hardness-unsound-branches.c

@@ -0,0 +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 <goblint.h>
+
+main() {
+  int a;
+  unsigned c = 1;
+  if (a)
+    c = 4;
+
+  // 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;
+}

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;
+    // To produce the fixpoint not reached error, the following needed to be an assert:
+    assert(e == (unsigned int )c + d); //UNKNOWN
+
+    burgo = 23;
+  }
+
+  return (0);
+
+}

tests/regression/37-congruence/17-sub-congruence.c

@@ -0,0 +1,31 @@
+// PARAM: --enable ana.int.congruence --disable ana.int.bitfield --disable ana.int.enums  --disable ana.int.interval --disable ana.int.def_exc
+
+#include<limits.h>
+#include<goblint.h>
+
+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!
+
+  int ov2 = 0 - min;
+  __goblint_check(ov2 == INT_MAX); //UNKNOWN!
+
+  return (0);
+
+}