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

regression/symex-shortest-path/for-loop/main.c

@@ -0,0 +1,13 @@
+void main()
+{
+  int i,x,y=0,z=0;
+  for(i=0;i < 10;++i)
+  //while(1)
+  {
+    if(x)
+     y++;
+    else
+     z++;
+  }
+  assert(1);
+}

regression/symex-shortest-path/for-loop/test.desc

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

regression/symex-shortest-path/function_pointer1/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+void (*f_ptr)(void);
+
+int global;
+
+void f1(void)
+{
+  global=1;
+}
+
+void f2(void)
+{
+  global=2;
+}
+
+int main()
+{
+  int input;
+
+  f_ptr=f1;
+  f_ptr();
+//  assert(global==1);
+
+  f_ptr=f2;
+  f_ptr();
+//  assert(global==2);
+
+  f_ptr=input?f1:f2;
+  f_ptr();
+  assert(global==(input?1:2));
+}

regression/symex-shortest-path/function_pointer1/test.desc

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

regression/symex-shortest-path/insertion-sort-unsafe/main.c

@@ -0,0 +1,47 @@
+// This file contains modified code snippets from "Algorithms in C, Third Edition,
+// Parts 1-4," by Robert Sedgewick. The code is intentionally buggy!
+//
+// For the correct code, see https://www.cs.princeton.edu/~rs/Algs3.c1-4/code.txt
+
+#include <assert.h>
+
+#define N 5
+
+
+#ifdef ENABLE_KLEE
+#include <klee/klee.h>
+#endif
+
+typedef int Item;
+#define key(A) (A)
+#define less(A, B) (key(A) < key(B))
+#define exch(A, B) { Item t = A; A = B; B = t; }
+#define compexch(A, B) if (less(B, A)) exch(A, B)
+
+void insertion_sort(Item a[], int l, int r) {
+  int i;
+  for (i = l+1; i <= r; i++) compexch(a[l], a[i]);
+  for (i = l+2; i <= r; i++) {
+    int j = i; Item v = a[i];
+    while (0 < j && less(v, a[j-1])) {
+      a[j] = a[j]; j--;
+      //       ^ bug due to wrong index (it should be j-1)
+    }
+    a[j] = v;
+  }
+}
+
+// To find bug, let N >= 4.
+int main() {
+  int a[N];
+
+#ifdef ENABLE_KLEE
+  klee_make_symbolic(a, sizeof(a), "a");
+#endif
+
+  insertion_sort(a, 0, N-1);
+  for (unsigned i = 0; i < N - 1; i++)
+    assert(a[i] <= a[i+1]);
+
+  return 0;
+}

regression/symex-shortest-path/insertion-sort-unsafe/test.desc

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