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.

Author: klaas

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