Unassume witness invariants during solving

bench/zarith/benchZarith.ml

@@ -0,0 +1,50 @@
+(** Benchmark calculation of powers of 2 with Zarith.
+    Originally for https://github.com/goblint/cil/pull/115.
+
+    dune exec bench/zarith/benchZarith.exe -- -a *)
+
+open Benchmark
+open Benchmark.Tree
+
+
+let () =
+  let pow2_pow n = Big_int_Z.power_int_positive_int 2 n in
+  let pow2_lsl n = Big_int_Z.shift_left_big_int Big_int_Z.unit_big_int n in
+
+
+  register (
+    "pow2" @>>> [
+      "8" @> lazy (
+        let arg = 8 in
+        throughputN 1 [
+          ("pow", pow2_pow, arg);
+          ("lsl", pow2_lsl, arg);
+        ]
+      );
+      "16" @> lazy (
+        let arg = 16 in
+        throughputN 1 [
+          ("pow", pow2_pow, arg);
+          ("lsl", pow2_lsl, arg);
+        ]
+      );
+      "32" @> lazy (
+        let arg = 32 in
+        throughputN 1 [
+          ("pow", pow2_pow, arg);
+          ("lsl", pow2_lsl, arg);
+        ]
+      );
+      "64" @> lazy (
+        let arg = 64 in
+        throughputN 1 [
+          ("pow", pow2_pow, arg);
+          ("lsl", pow2_lsl, arg);
+        ]
+      );
+    ]
+  )
+
+
+let () =
+  run_global ()

bench/zarith/dune

@@ -0,0 +1,4 @@
+(executable
+ (name benchZarith)
+ (optional) ; TODO: for some reason this doesn't work: `dune build` still tries to compile if benchmark missing (https://github.com/ocaml/dune/issues/4065)
+ (libraries benchmark zarith))

conf/bench-yaml-validate.json

@@ -0,0 +1,76 @@
+{
+  "ana": {
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "activated": [
+      "expRelation",
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "escape",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "mallocWrapper",
+      "mhp",
+      "assert",
+      "unassume"
+    ],
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    },
+    "widen": {
+      "tokens": true
+    }
+  },
+  "witness": {
+    "enabled": false,
+    "invariant": {
+      "loop-head": true,
+      "after-lock": true,
+      "other": false
+    }
+  },
+  "sem": {
+    "unknown_function": {
+      "invalidate": {
+        "globals": false
+      },
+      "spawn": true
+    },
+    "builtin_unreachable": {
+      "dead_code": true
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    }
+  },
+  "pre": {
+    "cppflags": [
+      "-DGOBLINT_NO_PTHREAD_ONCE",
+      "-DGOBLINT_NO_QSORT",
+      "-DGOBLINT_NO_BSEARCH"
+    ]
+  }
+}

conf/bench-yaml.json

@@ -0,0 +1,78 @@
+{
+  "ana": {
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "activated": [
+      "expRelation",
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "escape",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "mallocWrapper",
+      "mhp",
+      "assert"
+    ],
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    }
+  },
+  "witness": {
+    "enabled": false,
+    "yaml": {
+      "enabled": true
+    },
+    "invariant": {
+      "exact": false,
+      "exclude-vars": [
+        "tmp\\(___[0-9]+\\)?",
+        "cond",
+        "RETURN"
+      ]
+    }
+  },
+  "sem": {
+    "unknown_function": {
+      "invalidate": {
+        "globals": false
+      },
+      "spawn": true
+    },
+    "builtin_unreachable": {
+      "dead_code": true
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    }
+  },
+  "pre": {
+    "cppflags": [
+      "-DGOBLINT_NO_PTHREAD_ONCE",
+      "-DGOBLINT_NO_QSORT",
+      "-DGOBLINT_NO_BSEARCH"
+    ]
+  }
+}

conf/svcomp-yaml-validate.json

@@ -0,0 +1,82 @@
+{
+  "ana": {
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "escape",
+      "expRelation",
+      "mhp",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "unassume"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    },
+    "widen": {
+      "tokens": true
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "witness": {
+    "enabled": false,
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false
+    }
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    }
+  }
+}

conf/svcomp-yaml.json

@@ -0,0 +1,89 @@
+{
+  "ana": {
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "escape",
+      "expRelation",
+      "mhp",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "witness": {
+    "enabled": false,
+    "yaml": {
+      "enabled": true
+    },
+    "invariant": {
+      "exact": false,
+      "exclude-vars": [
+        "tmp\\(___[0-9]+\\)?",
+        "cond",
+        "RETURN",
+        "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+        ".*____CPAchecker_TMP_[0-9]+",
+        "__VERIFIER_assert__cond",
+        "__ksymtab_.*",
+        "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+      ]
+    }
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    }
+  }
+}