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

@@ -319,8 +319,25 @@ 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 && 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

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