Merge pull request #7788 from qinheping/features/goto-level-loop-cont…

…racts

CONTRACTS: Add goto-level loop-contract annotation

doc/man/goto-instrument.1

@@ -1010,6 +1010,9 @@ check and use loop contracts when provided
 \fB\-loop\-contracts\-no\-unwind\fR
 do not unwind transformed loops
 .TP
+\fB\-loop\-contracts\-file\fR \fIfile\fR
+annotate loop contracts from the file to the goto program
+.TP
 \fB\-\-replace\-call\-with\-contract\fR \fIfun\fR
 replace calls to \fIfun\fR with \fIfun\fR's contract
 .TP

regression/contracts-dfcc/CMakeLists.txt

@@ -14,12 +14,12 @@ endif()
 
 
 add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} true"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} true" ${gcc_only}
 )
 
 add_test_pl_profile(
     "contracts-non-dfcc"
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} false"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows} false" ${gcc_only}
     "-C;-X;dfcc-only;-s;non-dfcc"
     "CORE"
 )

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test.json

@@ -0,0 +1,15 @@
+{
+    "functions": [
+      {
+        "foo": [
+            {
+              "loop_id": "0",
+              "assigns": "i",
+              "invariants": "0 <= i && i <= 10",
+              "decreases": "i",
+              "symbol_map": "i,foo::1::1::i"
+            }
+          ]
+      }
+    ]
+  }

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/test_contracts_file.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--loop-contracts-file test.json --dfcc main --apply-loop-contracts
+^\[foo.assigns.\d+\] .* Check that nondet_var is assignable: FAILURE$
+^\[foo.assigns.\d+\] .* Check that __VERIFIER_var is assignable: FAILURE$
+^\[foo.assigns.\d+\] .* Check that __CPROVER_var is assignable: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that program variables with special name prefixes
+__CPROVER_, __VERIFIER, or nondet do not escape assigns clause checking.
+Using loop contracts from the contracts file.

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test.json

@@ -0,0 +1,18 @@
+{
+    "functions": [
+      {
+        "foo": [
+            {
+              "loop_id": "0",
+              "assigns": "i,nondet_var, __VERIFIER_var, __CPROVER_var",
+              "invariants": "0 <= i && i <= 10",
+              "decreases": "i",
+              "symbol_map": "i,foo::1::1::i;
+                            nondet_var,foo::1::nondet_var;
+                            __VERIFIER_var, foo::1::__VERIFIER_var;
+                            __CPROVER_var,foo::1::__CPROVER_var"
+            }
+          ]
+      }
+    ]
+  }

regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/test_contracts_file.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--loop-contracts-file test.json --dfcc main --apply-loop-contracts
+^\[foo.assigns.\d+\] .* Check that nondet_var is assignable: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that __VERIFIER_var is assignable: SUCCESS$
+^\[foo.assigns.\d+\] .* Check that __CPROVER_var is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that when program variables names have special prefixes
+__CPROVER_, __VERIFIER, or nondet, adding them to the write set makes them
+assignable.
+Using loop contracts from the contracts file.

regression/contracts-dfcc/history-index/test.json

@@ -0,0 +1,13 @@
+{
+    "functions": [
+      {
+        "main": [
+            {
+              "loop_id": "0",
+              "invariants": "x[0] == __CPROVER_loop_entry(x[0])",
+              "symbol_map": "x,main::1::x"
+            }
+          ]
+      }
+    ]
+  }

regression/contracts-dfcc/history-index/test_contracts_file.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--loop-contracts-file test.json --dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^Tracking history of index expressions is not supported yet\.
+--
+This test checks that `ID_index` expressions are allowed within history variables.
+Using loop contracts from the contracts file.

regression/contracts-dfcc/loop_contracts_file_fail/main.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  foo();
+}
+
+void foo()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+
+  b->data[5] = 0;
+  for(unsigned i = 0; i < SIZE; i++)
+  // clang-format off
+  // clang-format on
+  {
+    b->data[i] = 1;
+  }
+}
+
+void foo1()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+
+  b->data[5] = 0;
+  for(unsigned i = 0; i < SIZE; i++)
+  // clang-format off
+  // clang-format on
+  {
+    b->data[i] = 1;
+  }
+}

regression/contracts-dfcc/loop_contracts_file_fail/test_matching_more_than_one_function.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--loop-contracts-file test_matching_more_than_one_function.json --dfcc main --apply-loop-contracts
+^function regex .* matches more than one function
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+This test checks that loop contracts wrangler correctly error out
+when there is more than one matched function.

regression/contracts-dfcc/loop_contracts_file_fail/test_matching_more_than_one_function.json

@@ -0,0 +1,13 @@
+{
+    "functions": [
+      {
+        "foo.*": [
+            {
+              "loop_id": "0",
+              "invariants": "i <= 8",
+              "symbol_map": "i, foo::1::1::i"
+            }
+          ]
+      }
+    ]
+  }

regression/contracts-dfcc/loop_contracts_file_fail/test_matching_no_function.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--loop-contracts-file test_matching_no_function.json --dfcc main --apply-loop-contracts
+^function .* matches no function
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+This test checks that loop contracts wrangler correctly error out
+when there is no matched function.

regression/contracts-dfcc/loop_contracts_file_fail/test_matching_no_function.json

@@ -0,0 +1,13 @@
+{
+    "functions": [
+      {
+        "bar": [
+            {
+              "loop_id": "0",
+              "invariants": "i <= 8",
+              "symbol_map": "i, foo::1::1::i"
+            }
+          ]
+      }
+    ]
+  }

regression/contracts-dfcc/loop_contracts_memcmp/main.c

@@ -0,0 +1,34 @@
+inline int memcmp(const char *s1, const char *s2, unsigned n)
+{
+  int res = 0;
+  const unsigned char *sc1 = s1, *sc2 = s2;
+  for(; n != 0; n--)
+    // clang-format off
+    __CPROVER_loop_invariant(n <= __CPROVER_loop_entry(n))
+    __CPROVER_loop_invariant(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))
+    __CPROVER_loop_invariant(__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))
+    __CPROVER_loop_invariant(sc1 <= s1 + __CPROVER_loop_entry(n))
+    __CPROVER_loop_invariant(sc2 <= s2 + __CPROVER_loop_entry(n))
+    __CPROVER_loop_invariant(res == 0)
+    __CPROVER_loop_invariant(sc1 -(const unsigned char*)s1 == sc2 -(const unsigned char*)s2
+      &&  sc1 -(const unsigned char*)s1== __CPROVER_loop_entry(n) - n)
+    // clang-format on
+    {
+      res = (*sc1++) - (*sc2++);
+      long d1 = sc1 - (const unsigned char *)s1;
+      long d2 = sc2 - (const unsigned char *)s2;
+      if(res != 0)
+        return res;
+    }
+  return res;
+}
+
+int main()
+{
+  unsigned SIZE;
+  __CPROVER_assume(1 < SIZE && SIZE < 65536);
+  unsigned char *a = malloc(SIZE);
+  unsigned char *b = malloc(SIZE);
+  memcpy(b, a, SIZE);
+  assert(memcmp(a, b, SIZE) == 0);
+}

regression/contracts-dfcc/loop_contracts_memcmp/test.desc

@@ -0,0 +1,13 @@
+CORE gcc-only
+main.c
+--dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that loop contracts work correctly on memcmp.
+This test fails the CI job check-vs-2019-cmake-build-and-test with
+the following error.
+`Function '_errno' must exist in the model.`
+

regression/contracts-dfcc/loop_contracts_memcmp/test.json

@@ -0,0 +1,19 @@
+{
+    "functions": [
+      {
+        "memcmp": [
+            {
+              "loop_id": "0",
+              "invariants": "(n <= __CPROVER_loop_entry(n))&&(__CPROVER_same_object(sc1, __CPROVER_loop_entry(sc1)))&&
+                            (__CPROVER_same_object(sc2, __CPROVER_loop_entry(sc2)))&&
+                            (sc1 <= s1 + __CPROVER_loop_entry(n))&&
+                            (sc2 <= s2 + __CPROVER_loop_entry(n))&&
+                            (res == 0)&&
+                            (sc1 -(const unsigned char*)s1 == sc2 -(const unsigned char*)s2
+                            &&  sc1 -(const unsigned char*)s1== __CPROVER_loop_entry(n) - n)",
+              "symbol_map": "n,memcmp::n; sc1,memcmp::1::sc1; sc2,memcmp::1::sc2; res,memcmp::1::res; s1, memcmp::s1; s2, memcmp::s2"
+            }
+          ]
+      }
+    ]
+  }

regression/contracts-dfcc/loop_contracts_memcmp/test_contracts_file.desc

@@ -0,0 +1,13 @@
+CORE gcc-only
+main.c
+--loop-contracts-file test.json --dfcc main --apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that loop contracts work correctly on memcmp.
+Using loop contracts from the contracts file.
+This test fails the CI job check-vs-2019-cmake-build-and-test with
+the following error.
+`Function '_errno' must exist in the model.`

regression/contracts-dfcc/variant_multi_instruction_loop_head/test.json

@@ -0,0 +1,14 @@
+{
+    "functions": [
+      {
+        "main": [
+            {
+              "loop_id": "0",
+              "invariants": "0 <= *y && *y <= 10",
+              "decreases": "10-x",
+              "symbol_map": "y,main::1::y;x,main::1::x"
+            }
+          ]
+      }
+    ]
+  }

regression/contracts-dfcc/variant_multi_instruction_loop_head/test_contracts_file.desc

@@ -0,0 +1,17 @@
+CORE dfcc-only
+main.c
+--loop-contracts-file test.json --dfcc main --apply-loop-contracts
+^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$
+^\[main.assigns.\d+\] line \d+ Check that x is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that decreases clause is properly initialized
+when the loop head and loop invariant compilation emit several goto instructions.
+Using loop contracts from the contracts file.

src/ansi-c/c_typecheck_base.h

@@ -65,6 +65,7 @@ class c_typecheck_baset:
 
   virtual void typecheck()=0;
   virtual void typecheck_expr(exprt &expr);
+  virtual void typecheck_spec_assigns(exprt::operandst &targets);
 
 protected:
   symbol_table_baset &symbol_table;
@@ -160,7 +161,6 @@ class c_typecheck_baset:
   /// is found in expr.
   virtual void check_was_freed(const exprt &expr, std::string &clause_type);
 
-  virtual void typecheck_spec_assigns(exprt::operandst &targets);
   virtual void typecheck_spec_frees(exprt::operandst &targets);
   virtual void typecheck_conditional_targets(
     exprt::operandst &targets,

src/goto-instrument/Makefile

@@ -17,6 +17,7 @@ SRC = accelerate/accelerate.cpp \
       branch.cpp \
       call_sequences.cpp \
       contracts/contracts.cpp \
+      contracts/contracts_wrangler.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
       contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
       contracts/dynamic-frames/dfcc_contract_mode.cpp \

src/goto-instrument/contracts/contracts.h

@@ -40,6 +40,11 @@ Date: February 2016
   " --loop-contracts-no-unwind\n"                                              \
   "                              do not unwind transformed loops\n"
 
+#define FLAG_LOOP_CONTRACTS_FILE "loop-contracts-file"
+#define HELP_LOOP_CONTRACTS_FILE                                               \
+  " --loop-contracts-file <file>\n"                                            \
+  "                              parse and annotate loop contracts from files\n"
+
 #define FLAG_REPLACE_CALL "replace-call-with-contract"
 #define HELP_REPLACE_CALL                                                      \
   " --replace-call-with-contract <function>[/contract]\n"                      \