Regression tests for symex shortest path search heuristics

This is all the regression tests from regression/symex that only have one property, and all the regression tests from regression/symex-infeasibility that the default symex search heuristic (dfs) can complete in a reasonable amount of time.

Author: polgreen

regression/symex-shortest-path/Makefile

@@ -0,0 +1,22 @@
+default: tests.log
+
+test:
+	@../test.pl -c "../../../src/symex/symex --shortest-path"
+	@../test.pl -c "../../../src/symex/symex --shortest-path --randomize"
+
+tests.log: ../test.pl
+	@../test.pl -c "../../../src/symex/symex --shortest-path"
+	@../test.pl -c "../../../src/symex/symex --shortest-path --randomize"
+
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/symex-shortest-path/bst-safe/main.c

@@ -0,0 +1,101 @@
+// This file contains code snippets from "Algorithms in C, Third Edition,
+// Parts 1-4," by Robert Sedgewick.
+//
+// See https://www.cs.princeton.edu/~rs/Algs3.c1-4/code.txt
+
+#include <stdlib.h>
+#include <assert.h>
+
+#define N 1000
+
+
+#ifdef ENABLE_KLEE
+#include <klee/klee.h>
+#endif
+
+typedef int Key;
+typedef int Item;
+
+#define eq(A, B) (!less(A, B) && !less(B, A))
+#define key(A) (A)
+#define less(A, B) (key(A) < key(B))
+#define NULLitem 0
+
+struct STnode;
+typedef struct STnode* link;
+
+struct STnode { Item item; link l, r; int n; };
+static link head, z;
+
+static link NEW(Item item, link l, link r, int n) {
+  link x = malloc(sizeof *x);
+  x->item = item; x->l = l; x->r = r; x->n = n;
+  return x;
+}
+
+void STinit() {
+  head = (z = NEW(NULLitem, 0, 0, 0));
+}
+
+int STcount() { return head->n; }
+
+static link insertR(link h, Item item) {
+  Key v = key(item), t = key(h->item);
+  if (h == z) return NEW(item, z, z, 1);
+
+  if (less(v, t))
+    h->l = insertR(h->l, item);
+  else
+    h->r = insertR(h->r, item);
+
+  (h->n)++; return h;
+}
+
+void STinsert(Item item) { head = insertR(head, item); }
+
+static void sortR(link h, void (*visit)(Item)) {
+  if (h == z) return;
+  sortR(h->l, visit);
+  visit(h->item);
+  sortR(h->r, visit);
+}
+
+void STsort(void (*visit)(Item)) { sortR(head, visit); }
+
+
+static Item a[N];
+static unsigned k = 0;
+void sorter(Item item) {
+  a[k++] = item;
+}
+
+#ifdef ENABLE_CPROVER
+int nondet_int();
+#endif
+
+// Unwind N+1 times
+int main() {
+#ifdef ENABLE_KLEE
+  klee_make_symbolic(a, sizeof(a), "a");
+#endif
+
+  STinit();
+
+  for (unsigned i = 0; i < N; i++) {
+#ifdef ENABLE_CPROVER
+    STinsert(nondet_int());
+#elif ENABLE_KLEE
+    STinsert(a[i]);
+    a[i] = NULLitem;
+#endif
+  }
+
+  STsort(sorter);
+
+#ifndef FORCE_BRANCH
+  for (unsigned i = 0; i < N - 1; i++)
+    assert(a[i] <= a[i+1]);
+#endif
+
+  return 0;
+}

regression/symex-shortest-path/bst-safe/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-shortest-path/concrete-sum-unsafe/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+#define N 40000
+
+int main(void) {
+  unsigned n = 1;
+  unsigned sum = 0;
+
+  while (n <= N)
+  {
+    sum = sum + n;
+    n = n + 1;
+  }
+
+  assert(sum != ((N * (N + 1)) / 2));
+
+  return 0;
+}

regression/symex-shortest-path/concrete-sum-unsafe/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/symex-shortest-path/concrete-sum/concrete-sum-unsafe.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main(void) {
+  unsigned n = 1;
+  unsigned sum = 0;
+
+  while (n <= N)
+  {
+    sum = sum + n;
+    n = n + 1;
+  }
+
+  assert(sum != ((N * (N + 1)) / 2));
+
+  return 0;
+}

regression/symex-shortest-path/concrete-sum/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+#define N 40000
+
+// conservatively safe for N <= 46340
+int main(void) {
+  unsigned n = 1;
+  unsigned sum = 0;
+
+  while (n <= N)
+  {
+    sum = sum + n;
+    n = n + 1;
+  }
+
+//#ifndef FORCE_BRANCH
+  assert(sum == ((N * (N + 1)) / 2));
+//#endif
+
+  return 0;
+}

regression/symex-shortest-path/concrete-sum/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/symex-shortest-path/counter-unsafe/main.c

@@ -0,0 +1,39 @@
+// Similar to SV-COMP'14 (loops/count_up_down_false.c) except
+// that we use explicit signedness constraints to support
+// benchmarks with tools that are not bit precise.
+
+#include <assert.h>
+
+#define N 10
+#define ENABLE_CPROVER
+
+#ifdef ENABLE_KLEE
+#include <klee/klee.h>
+#endif
+
+#ifdef ENABLE_CPROVER
+int nondet_int();
+#endif
+
+// It suffices to unwind N times
+int main() {
+#ifdef ENABLE_CPROVER
+  int n = nondet_int();
+  __CPROVER_assume(0 <= n && n < N);
+#elif ENABLE_KLEE
+  int n;
+  klee_make_symbolic(&n, sizeof(n), "n");
+  if (0 > n)
+    return 0;
+  if (n >= N)
+    return 0;
+#endif
+
+  int x = n, y = 0;
+  while (x > 0) {
+    x = x - 1;
+    y = y + 1;
+  }
+  assert(0 <= y && y != n);
+  return 0;
+}

regression/symex-shortest-path/counter-unsafe/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+--
+^warning: ignoring