Added an initial set of tests for contracts, which (expectedly) either fail or

will need to be redone once the new flags are added in.

Fixed test descriptions to put comments in the correct place and updated some
stylistic issues with test cases.

Enabled tests that work (if with different flag name) in the current state to
give a better sense of the initial state.

regression/Makefile

@@ -18,7 +18,8 @@ DIRS = cbmc \
        goto-cc-cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
-       systemc
+       systemc \
+       contracts \
        # Empty last line
 
 # Tests under goto-gcc cannot be run on Windows, so appveyor.yml unlinks

regression/contracts/CMakeLists.txt

@@ -0,0 +1,9 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)

regression/contracts/Makefile

@@ -0,0 +1,35 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
+test:
+	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+
+tests.log:
+	@../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/contracts/chain.sh

@@ -0,0 +1,38 @@
+#!/bin/bash
+
+set -e
+
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
+
+name=${*:$#}
+name=${name%.c}
+
+args=${*:5:$#-5}
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c"
+  mv "${name}.exe" "${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
+fi
+
+$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
+if [ ! -e "${name}-mod.gb" ] ; then
+  cp "$name.gb" "${name}-mod.gb"
+elif echo $args | grep -q -- "--dump-c" ; then
+  mv "${name}-mod.gb" "${name}-mod.c"
+
+  if [[ "${is_windows}" == "true" ]]; then
+    $goto_cc "${name}-mod.c"
+    mv "${name}-mod.exe" "${name}-mod.gb"
+  else
+    $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
+  fi
+
+  rm "${name}-mod.c"
+fi
+$goto_instrument --show-goto-functions "${name}-mod.gb"
+$cbmc "${name}-mod.gb"

regression/contracts/function_apply_01/main.c

@@ -0,0 +1,20 @@
+// function_apply_01
+
+// Note that this test is supposed to have an incorrect contract.
+// We verify that applying (without checking) the contract yields success,
+// and that checking the contract yields failure.
+
+#include <assert.h>
+
+int foo() 
+  __CPROVER_ensures(__CPROVER_return_value == 0)
+{
+  return 1;
+}
+
+int main()
+{
+  int x = foo();
+  assert(x == 0);
+  return 0;
+}

regression/contracts/function_apply_01/test.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Applying code contracts currently also checks them.

regression/contracts/function_check_01/main.c

@@ -0,0 +1,31 @@
+// function_check_01
+
+// This tests a simple example of a function with requires and
+// ensures which should both be satisfied.
+
+#include <assert.h>
+
+int min(int a, int b)
+  __CPROVER_requires(a >= 0 && b >= 0)
+  __CPROVER_ensures(__CPROVER_return_value <= a &&
+                    __CPROVER_return_value <= b &&
+                   (__CPROVER_return_value == a || __CPROVER_return_value == b)
+                   )
+{
+  if(a <= b)
+  {
+    return a;
+  }
+  else
+  {
+    return b;
+  }
+}
+
+int main()
+{
+  int x, y, z;
+  __CPROVER_assume(x >= 0 && y >= 0);
+  z = min(x, y);
+  assert(z <= x);
+}

regression/contracts/function_check_01/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.

regression/contracts/function_check_02/main.c

@@ -0,0 +1,24 @@
+// function_check_02
+
+// This test checks the use of quantifiers in ensures clauses.
+// A known bug (resolved in PR #2278) causes the use of quantifiers
+// in ensures to fail.
+
+int initialize(int *arr)
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i}
+  )
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  initialize(arr);
+}

regression/contracts/function_check_02/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Ensures statements currently do not allow quantified predicates unless the
+function has void return type.

regression/contracts/function_check_03/main.c

@@ -0,0 +1,26 @@
+// function_check_03
+
+// This extends function_check_02's test of quantifiers in ensures
+// and adds in a loop invariant which can be used to prove the ensures.
+// This currently fails because side-effect checking in loop invariants is
+// incorrect.
+
+void initialize(int *arr, int len)
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> arr[i] == i}
+  )
+{
+  for(int i = 0; i < len; i++)
+    __CPROVER_loop_invariant(
+      __CPROVER_forall {int j; (0 <= j && j < i) ==> arr[j] == j}
+    )
+  {
+    arr[i] = i;
+  }
+}
+
+int main()
+{
+  int arr[10];
+  initialize(arr, 10);
+}

regression/contracts/function_check_03/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariants currently do not support memory reads in at least some
+circumstances.

regression/contracts/function_check_04/main.c

@@ -0,0 +1,19 @@
+// function_check_04
+
+// Note that this test is supposed to have an incorrect contract.
+// We verify that checking this faulty contract (correctly) yields a failure.
+
+#include <assert.h>
+
+int foo() 
+  __CPROVER_ensures(__CPROVER_return_value == 0)
+{
+  return 1;
+}
+
+int main()
+{
+  int x = foo();
+  assert(x == 0);
+  return 0;
+}

regression/contracts/function_check_04/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^\[main.assertion.1\] assertion x == 0: SUCCESS$
+^\[foo.1\] : FAILURE$
+^VERIFICATION FAILED$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.

regression/contracts/function_check_05/main.c

@@ -0,0 +1,26 @@
+// function_check_05
+
+// This test checks that when a function call is replaced by an invariant,
+// it adequately havocs the locations modified by the function.
+// This test currently fails because the analysis of what is modified by
+// a function is flawed.
+
+#include <assert.h>
+
+int foo(int *x) 
+  __CPROVER_ensures(__CPROVER_return_value == 1)
+{
+  *x = 1;
+  return 1;
+}
+
+int main()
+{
+  int y = 0;  
+  int z = foo(&y);
+  // This assert should fail.
+  assert(y == 0);
+  // This one should succeed.
+  assert(z == 1);
+  return 0;
+}

regression/contracts/function_check_05/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^\[main.assertion.1\] assertion y == 0: FAILURE$
+^\[main.assertion.2\] assertion z == 1: SUCCESS$
+^\[foo.1\] : SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Contract checking does not properly havoc function calls.

regression/contracts/function_check_mem_01/main.c

@@ -0,0 +1,45 @@
+// function_check_mem_01
+
+// This test checks the use of pointer-related predicates in assumptions and
+// requires.
+// This test currently fails because of the lack of support for assuming
+// pointer predicates.
+
+#include <stddef.h>
+
+#define __CPROVER_VALID_MEM(ptr, size) \
+  __CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \
+  !__CPROVER_invalid_pointer((ptr)) && \
+  __CPROVER_POINTER_OBJECT((ptr)) != \
+  __CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \
+  __CPROVER_POINTER_OBJECT((ptr)) != \
+  __CPROVER_POINTER_OBJECT(__CPROVER_dead_object) && \
+  (__builtin_object_size((ptr), 1) >= (size) && \
+  __CPROVER_POINTER_OFFSET((ptr)) >= 0l || \
+   __CPROVER_DYNAMIC_OBJECT((ptr))) && \
+  (__CPROVER_POINTER_OFFSET((ptr)) >= 0 && \
+   __CPROVER_malloc_size >= (size) + __CPROVER_POINTER_OFFSET((ptr)) || \
+   __CPROVER_POINTER_OBJECT((ptr)) != \
+   __CPROVER_POINTER_OBJECT(__CPROVER_malloc_object))
+    
+typedef struct bar
+{
+  int x;
+  int y;
+  int z;
+} bar;
+
+void foo(bar *x)
+  __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
+{
+  x->x += 1;
+  return
+}
+
+int main()
+{
+  bar *y;
+  __CPROVER_assume(__CPROVER_VALID_MEM(y, sizeof(bar)));
+  y->x = 0;
+  return 0;
+}

regression/contracts/function_check_mem_01/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+CBMC currently does not support assumptions about pointers in the general way
+that other assumptions are supported.

regression/contracts/invar_check_01/main.c

@@ -0,0 +1,20 @@
+// invar_check_01
+
+// This test checks that a basic loop invariant can be proven and used in
+// combination with the negation of the loop guard to get a result.
+
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+  {
+    --r;
+  }
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts/invar_check_01/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.

regression/contracts/invar_check_02/main.c

@@ -0,0 +1,29 @@
+// invar_check_02
+
+// This test checks that loop invariants adequately handle continues.
+
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+  { 
+    --r;
+    if (r < 5)
+    {
+      continue;
+    }
+    else
+    {
+      --r;
+    }
+  }
+
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts/invar_check_02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.

regression/contracts/invar_check_03/main.c

@@ -0,0 +1,85 @@
+// invar_check_03
+
+// This test checks the use of loop invariants on a larger problem --- in this
+// case, the partition portion of quicksort, applied to a fixed-length array.
+// This serves as a stop-gap test until issues to do with quantifiers and
+// side-effects in loop invariants are fixed.
+
+#include <assert.h>
+
+void swap(int *a, int *b)
+{
+  *a ^= *b;
+  *b ^= *a;
+  *a ^= *b;
+}
+
+int main()
+{ 
+  int arr0, arr1, arr2, arr3, arr4;
+  arr0 = 1;
+  arr1 = 2;
+  arr2 = 0;
+  arr3 = 4;
+  arr4 = 3; 
+  int *arr[5] = {&arr0, &arr1, &arr2, &arr3, &arr4};
+  int pivot = 2;
+
+  int h = 5 - 1;
+  int l = 0;
+  int r = 1;
+  while(h > l)
+    __CPROVER_loop_invariant(
+      h >= l &&
+      0 <= l && l < 5 &&
+      0 <= h && h < 5 &&
+      l <= r && r <= h &&
+      (r == 0 ==> arr0 == pivot) &&
+      (r == 1 ==> arr1 == pivot) &&
+      (r == 2 ==> arr2 == pivot) &&
+      (r == 3 ==> arr3 == pivot) &&
+      (r == 4 ==> arr4 == pivot) &&
+      (0 < l ==> arr0 <= pivot) &&
+      (1 < l ==> arr1 <= pivot) &&
+      (2 < l ==> arr2 <= pivot) &&
+      (3 < l ==> arr3 <= pivot) &&
+      (4 < l ==> arr4 <= pivot) &&
+      (0 > h ==> arr0 >= pivot) &&
+      (1 > h ==> arr1 >= pivot) &&
+      (2 > h ==> arr2 >= pivot) &&
+      (3 > h ==> arr3 >= pivot) &&
+      (4 > h ==> arr4 >= pivot)
+    )
+  {
+    if(*(arr[h]) <= pivot && *(arr[l]) >= pivot) {
+      swap(arr[h], arr[l]);
+      if (r == h) {
+        r = l;
+        h--;
+      }
+      else if(r == l) {
+        r = h;
+        l++;
+      }
+    }
+    else if(*(arr[h]) <= pivot) {
+      l++;
+    }
+    else {
+      h--;
+    }
+  }
+  assert(0 <= r && r < 5);
+  assert(*(arr[r]) == pivot);
+  assert(0 < r ==> arr0 <= pivot);
+  assert(1 < r ==> arr1 <= pivot);
+  assert(2 < r ==> arr2 <= pivot);
+  assert(3 < r ==> arr3 <= pivot);
+  assert(4 < r ==> arr4 <= pivot);
+  assert(0 > r ==> arr0 >= pivot);
+  assert(1 > r ==> arr1 >= pivot);
+  assert(2 > r ==> arr2 >= pivot);
+  assert(3 > r ==> arr3 >= pivot);
+  assert(4 > r ==> arr4 >= pivot);
+  return r;
+}

regression/contracts/invar_check_03/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.

regression/contracts/invar_check_04/main.c

@@ -0,0 +1,30 @@
+// invar_check_04
+
+// This test checks the handling of break by loop invariants.
+// This test is expected to fail along the code path where r is even before
+// entering the loop.
+
+#include <assert.h>
+
+int main()
+{
+  int r;
+  __CPROVER_assume(r >= 0);
+
+  while(r>0)
+    __CPROVER_loop_invariant(r >= 0)
+  { 
+    --r;
+    if (r <= 1)
+    {
+      break;
+    }
+    else
+    {
+      --r;
+    }
+  }
+  assert(r == 0);
+
+  return 0;
+}

regression/contracts/invar_check_04/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--apply-code-contracts
+^\[main.1\] Loop invariant violated before entry: SUCCESS$
+^\[main.2\] Loop invariant not preserved: SUCCESS$
+^\[main.assertion.1\] assertion r == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+--check-code-contracts not implemented yet.
+--apply-code-contracts is the current name for the flag. This should be
+updated as the flag changes.

regression/contracts/invar_loop_constant/main.c

@@ -0,0 +1,25 @@
+// invar_loop_constant
+
+// This test checks to see whether loop invariant checking discards sufficiently
+// little information to be aware after the loop that s is necessarily 1.
+// This test currently fails due to excessive havocking in checking loop
+// invariants, but is not an obstacle to soundness of contract checking.
+
+#include <assert.h>
+
+int main()
+{
+  int r;
+  int s = 1;
+  __CPROVER_assume(r >= 0);
+  while(r > 0)
+    __CPROVER_loop_invariant(r >= 0)
+  {
+    s = 1;
+    r--;
+  }
+  assert(r == 0);
+  assert(s == 1);
+
+  return 0;
+}

regression/contracts/invar_loop_constant/test.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariant checking throws away more information than needed.

regression/contracts/quicksort_contracts_01/main.c

@@ -0,0 +1,112 @@
+// quicksort_contracts_01
+
+// This test checks the correctness of a quicksort implementation using explicit
+// ghost state.
+
+// This test currently fails for a variety of reasons, including:
+// (1) Lack of support for quantifiers in ensures statements.
+// (2) Lack of support for reading from memory in loop invariants (under some
+// circumstances)
+
+#include <assert.h>
+#include <stdlib.h>
+#include <string.h>
+
+void swap(int *a, int *b)
+{
+  *a ^= *b;
+  *b ^= *a;
+  *a ^= *b;
+}
+
+int partition(int arr_ghost[], int arr[], int len)
+  __CPROVER_requires(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> arr_ghost[i] == arr[i]} &&
+   len > 0 &&
+    1 == 1
+  )
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_exists {int j; 0 <= j && j < len && arr_ghost[i] == arr[j]}} &&
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_exists {int j; 0 <= j && j < len && arr[i] == arr_ghost[j]}} &&
+    0 <= __CPROVER_return_value && __CPROVER_return_value < len &&
+    __CPROVER_forall {int i; (0 <= i && i <= __CPROVER_return_value) ==> arr[i] <= arr[__CPROVER_return_value]} &&
+    __CPROVER_forall {int i; (__CPROVER_return_value <= i && i < len) ==> arr[__CPROVER_return_value] <= arr[i]} &&
+    1 == 1
+  )
+{
+  int h = len - 1;
+  int l = 0;
+
+  int pivot_idx = len / 2;
+  int pivot = arr[pivot_idx];
+
+  while(h > l)
+    __CPROVER_loop_invariant(
+        0 <= l && l <= pivot_idx && pivot_idx <= h && h < len &&
+      arr[pivot_idx] == pivot &&
+      __CPROVER_forall {int i; (0 <= i && i < l) ==> arr[i] <= pivot} &&
+      __CPROVER_forall {int i; (h < i && i < len) ==> pivot <= arr[i]} &&
+      1 == 1
+    )
+  {
+    if(arr[h] <= pivot && arr[l] >= pivot)
+    {
+      swap(arr + h, arr + l);
+      if(pivot_idx == h)
+      {
+        pivot_idx = l;
+        h--;
+      }
+      if(pivot_idx == l)
+      {
+        pivot_idx = h;
+        l++;
+      }
+    }
+    else if(arr[h] <= pivot)
+    {
+      l++;
+    }
+    else
+    {
+      h--;
+    }
+  }
+  return pivot_idx;
+}
+
+void quicksort(int arr_ghost[], int arr[], int len)
+  __CPROVER_requires(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> arr_ghost[i] == arr[i]} &&
+    1 == 1
+  )
+  __CPROVER_ensures(
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_exists {int j; 0 <= j && j < len && arr_ghost[i] == arr[j]}} &&
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_exists {int j; 0 <= j && j < len && arr[i] == arr_ghost[j]}} &&
+    __CPROVER_forall {int i; (0 <= i && i < len) ==> __CPROVER_forall {int j; (i <= j && j < len) ==> arr[i] <= arr[j]}} &&
+    1 == 1
+  )
+{
+  if(len <= 1)
+  {
+    return;
+  }
+  int *new_ghost = malloc(len * sizeof(int));
+  memcpy(new_ghost, arr, len * sizeof(int));
+
+  int pivot_idx = partition(new_ghost, arr, len);
+
+  memcpy(new_ghost, arr, len * sizeof(int));
+
+  quicksort(new_ghost, arr, pivot_idx);
+  quicksort(new_ghost, arr + pivot_idx + 1, len - pivot_idx - 1);
+
+  free(new_ghost);
+}
+
+int main()
+{
+  int arr[5] = {1, 2, 3, 0, 4};
+  int arr_ghost[5] = {1, 2, 3, 0, 4};
+  quicksort(arr_ghost, arr, 5);
+}

regression/contracts/quicksort_contracts_01/test.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+main.c
+--check-code-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Loop invariants are overzealous in deciding what counts as side effects.