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,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

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