Regression tests for code contracts

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;
+}