refactored checking

microsoft · Nov 11, 2023 · a6cc486 · a6cc486
1 parent 4812d1c
commit a6cc486
Show file tree

Hide file tree

Showing 160 changed files with 7,677 additions and 90 deletions.
diff --git a/data/analysis/svcomp_dataset.ipynb b/data/analysis/svcomp_dataset.ipynb
@@ -2,7 +2,7 @@
  "cells": [
   {
    "cell_type": "code",
-   "execution_count": 69,
+   "execution_count": 1,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -14,7 +14,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 70,
+   "execution_count": 2,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -30,7 +30,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 72,
+   "execution_count": 3,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -46,7 +46,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 74,
+   "execution_count": 4,
    "metadata": {},
    "outputs": [
     {
@@ -55,7 +55,7 @@
        "544"
       ]
      },
-     "execution_count": 74,
+     "execution_count": 4,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -66,7 +66,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 76,
+   "execution_count": 5,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -77,7 +77,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 81,
+   "execution_count": 6,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -93,7 +93,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 85,
+   "execution_count": 7,
    "metadata": {},
    "outputs": [],
    "source": [
@@ -110,7 +110,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 86,
+   "execution_count": 8,
    "metadata": {},
    "outputs": [
     {
@@ -119,7 +119,7 @@
        "403"
       ]
      },
-     "execution_count": 86,
+     "execution_count": 8,
      "metadata": {},
      "output_type": "execute_result"
     }
@@ -128,6 +128,41 @@
     "len(final_positive_set)"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "ultimate_failure_file = open(\"ultimate_failed_benchmarks.txt\", \"r\", encoding=\"utf-8\").read().splitlines()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 12,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "ultimate_success = []\n",
+    "ultimate_failure = []\n",
+    "\n",
+    "for f in final_positive_set:\n",
+    "    if f in ultimate_failure_file:\n",
+    "        ultimate_failure.append(f)\n",
+    "    else:\n",
+    "        ultimate_success.append(f)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "with open(\"ultimate_success_benchmarks.txt\", \"w\", encoding='utf-8') as f:\n",
+    "    f.write(\"\\n\".join(ultimate_success))"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": 87,

diff --git a/data/analysis/ultimate_success_benchmarks.txt b/data/analysis/ultimate_success_benchmarks.txt
@@ -0,0 +1,170 @@
+../../sv-benchmarks/c/bitvector/gcd_4.c
+../../sv-benchmarks/c/bitvector/modulus-2.c
+../../sv-benchmarks/c/bitvector/soft_float_2a.c.cil.c
+../../sv-benchmarks/c/bitvector/soft_float_5a.c.cil.c
+../../sv-benchmarks/c/floats-cbmc-regression/float-div1.c
+../../sv-benchmarks/c/floats-cbmc-regression/float-no-simp2.c
+../../sv-benchmarks/c/floats-cbmc-regression/float-no-simp4.c
+../../sv-benchmarks/c/floats-cbmc-regression/float-no-simp6.c
+../../sv-benchmarks/c/floats-cbmc-regression/float-rounding1.c
+../../sv-benchmarks/c/floats-cbmc-regression/float-to-double1.c
+../../sv-benchmarks/c/floats-cbmc-regression/float-zero-sum1.c
+../../sv-benchmarks/c/floats-cbmc-regression/float14.c
+../../sv-benchmarks/c/floats-cbmc-regression/float19.c
+../../sv-benchmarks/c/floats-cbmc-regression/float20.c
+../../sv-benchmarks/c/floats-cbmc-regression/float21.c
+../../sv-benchmarks/c/floats-cbmc-regression/float3.c
+../../sv-benchmarks/c/floats-cbmc-regression/float4.c
+../../sv-benchmarks/c/floats-cbmc-regression/float8.c
+../../sv-benchmarks/c/floats-cbmc-regression/float_lib2.c
+../../sv-benchmarks/c/floats-esbmc-regression/trunc_nondet_2.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0250a.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0250b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0260.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0281.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0470.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0480.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0490a.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0490b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0730a.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0730b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0740.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0910b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0920a.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0920b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0931.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0960b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0970a.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0970b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_0981.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1032c.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1032d.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1052a.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1052b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1092c.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1092d.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1230.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1231b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1232a.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1250.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1251b.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1252a.c
+../../sv-benchmarks/c/float-newlib/double_req_bl_1300.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0250a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0250b.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0260.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0281.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0460.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0470.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0480.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0490a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0490b.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0710.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0730a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0730b.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0730c.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0740.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0910a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0910b.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0920a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0920b.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0931.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0960a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0960b.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0970a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0970b.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_0981.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_1072a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_1072b.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_1230.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_1231.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_1232a.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_1250.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_1251.c
+../../sv-benchmarks/c/float-newlib/float_req_bl_1252a.c
+../../sv-benchmarks/c/ldv-regression/test_cut_trace.i
+../../sv-benchmarks/c/ldv-sets/test_add-2.c
+../../sv-benchmarks/c/loops/trex01-2.c
+../../sv-benchmarks/c/loops/trex04.c
+../../sv-benchmarks/c/loops/trex04_abstracted.c
+../../sv-benchmarks/c/loops/while_infinite_loop_3.c
+../../sv-benchmarks/c/loop-acceleration/functions_1-1.c
+../../sv-benchmarks/c/loop-acceleration/nested_1-1.c
+../../sv-benchmarks/c/loop-invgen/SpamAssassin-loop.c
+../../sv-benchmarks/c/loop-invgen/apache-get-tag.c
+../../sv-benchmarks/c/loop-invgen/nest-if3.c
+../../sv-benchmarks/c/loops-crafted-1/loopv2.c
+../../sv-benchmarks/c/loops-crafted-1/nested5-1.c
+../../sv-benchmarks/c/loops-crafted-1/sum_by_3_abstracted.c
+../../sv-benchmarks/c/nla-digbench/cohendiv-ll.c
+../../sv-benchmarks/c/nla-digbench/fermat1-ll.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound10.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound100.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound20.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound5.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_unwindbound50.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound10.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound100.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound20.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound5.c
+../../sv-benchmarks/c/nla-digbench-scaling/cohendiv-ll_valuebound50.c
+../../sv-benchmarks/c/nla-digbench-scaling/dijkstra-u_unwindbound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/dijkstra-u_unwindbound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/dijkstra-u_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/dijkstra-u_valuebound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/divbin2_unwindbound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/divbin2_unwindbound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/divbin2_unwindbound5.c
+../../sv-benchmarks/c/nla-digbench-scaling/divbin2_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/divbin2_valuebound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/divbin_unwindbound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/divbin_unwindbound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/divbin_unwindbound5.c
+../../sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/egcd2-ll_valuebound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/egcd3-ll_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/egcd3-ll_valuebound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound10.c
+../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound100.c
+../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound20.c
+../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound5.c
+../../sv-benchmarks/c/nla-digbench-scaling/fermat1-ll_valuebound50.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard-ll_valuebound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound10.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound100.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound2.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound20.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound5.c
+../../sv-benchmarks/c/nla-digbench-scaling/hard2_valuebound50.c
+../../sv-benchmarks/c/nla-digbench-scaling/knuth_valuebound1.c
+../../sv-benchmarks/c/nla-digbench-scaling/knuth_valuebound2.c
+../../sv-benchmarks/c/recursive/Ackermann01-2.c
+../../sv-benchmarks/c/recursive/Ackermann03.c
+../../sv-benchmarks/c/recursive/Ackermann04.c
+../../sv-benchmarks/c/recursive/Addition01-2.c
+../../sv-benchmarks/c/recursive/Fibonacci01-1.c
+../../sv-benchmarks/c/recursive/Fibonacci02.c
+../../sv-benchmarks/c/recursive/Fibonacci03.c
+../../sv-benchmarks/c/recursive/McCarthy91-2.c
+../../sv-benchmarks/c/recursive/Primes.c
+../../sv-benchmarks/c/recursive/gcd01-1.c
+../../sv-benchmarks/c/recursive/recHanoi02-2.c
+../../sv-benchmarks/c/recursive/recHanoi03-2.c
+../../sv-benchmarks/c/recursive-simple/fibo_2calls_10-1.c
+../../sv-benchmarks/c/recursive-simple/id2_b2_o3.c
+../../sv-benchmarks/c/recursive-simple/id2_b3_o5.c
+../../sv-benchmarks/c/recursive-simple/id2_b5_o10.c
+../../sv-benchmarks/c/recursive-simple/id_b2_o3.c
+../../sv-benchmarks/c/recursive-simple/id_b3_o5-2.c
+../../sv-benchmarks/c/recursive-simple/id_b5_o10-2.c
+../../sv-benchmarks/c/recursive-simple/sum_non_eq-2.c
+../../sv-benchmarks/c/systemc/pc_sfifo_1.cil-2.c
+../../sv-benchmarks/c/systemc/pc_sfifo_2.cil-1.c
diff --git a/data/benchmarks/diffy_cav21_bench/brs1.c b/data/benchmarks/diffy_cav21_bench/brs1.c
@@ -0,0 +1,43 @@
+/*
+ * Benchmarks contributed by Divyesh Unadkat[1,2], Supratik Chakraborty[1], Ashutosh Gupta[1]
+ * [1] Indian Institute of Technology Bombay, Mumbai
+ * [2] TCS Innovation labs, Pune
+ *
+ */
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_assume(int);
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } }
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int main()
+{
+	N = __VERIFIER_nondet_int();
+	if(N <= 0) return 1;
+
+	int i;
+	int sum[1];
+	int a[N];
+
+	for(i=0; i<N; i++)
+	{
+		if(i%1==0) {
+			a[i] = 1;
+		} else {
+			a[i] = 0;
+		}
+	}
+
+	for(i=0; i<N; i++)
+	{
+		if(i==0) {
+			sum[0] = 0;
+		} else {
+			sum[0] = sum[0] + a[i];
+		}
+	}
+	__VERIFIER_assert(sum[0] <= N);
+	return 1;
+}
diff --git a/data/benchmarks/diffy_cav21_bench/brs2.c b/data/benchmarks/diffy_cav21_bench/brs2.c
@@ -0,0 +1,43 @@
+/*
+ * Benchmarks contributed by Divyesh Unadkat[1,2], Supratik Chakraborty[1], Ashutosh Gupta[1]
+ * [1] Indian Institute of Technology Bombay, Mumbai
+ * [2] TCS Innovation labs, Pune
+ *
+ */
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern void __VERIFIER_assume(int);
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } }
+extern int __VERIFIER_nondet_int(void);
+
+int N;
+
+int main()
+{
+	N = __VERIFIER_nondet_int();
+	if(N <= 0) return 1;
+
+	int i;
+	int sum[1];
+	int a[N];
+
+	for(i=0; i<N; i++)
+	{
+		if(i%2==0) {
+			a[i] = 2;
+		} else {
+			a[i] = 0;
+		}
+	}
+
+	for(i=0; i<N; i++)
+	{
+		if(i==0) {
+			sum[0] = 0;
+		} else {
+			sum[0] = sum[0] + a[i];
+		}
+	}
+	__VERIFIER_assert(sum[0] <= 2*N);
+	return 1;
+}