Add goto-level loop-contract annotation

This commit allows us to parse and annotate loop contracts from JSON files to GOTO models.

We first parse the JSON file to get the configuration.

    Function configurations consist of function id (regex) and a list of loop-contract configurations.
    Loop-contract configurations consist of:
        Loop number of the loop we are annotating to.
        Loop invariants as strings.
        (optional) Loop assigns as strings.
        (optional) Loop decreases as strings.
        (optional) A symbol map that map symbol names in the loop contracts strings to their name in the symbol table of the goto model.

Loop contracts mangling consists of four steps.

    Construct a fake function with a fake loop that contains the loop contracts for parsing the contracts.
    Parse the fake function and extract the contracts as exprt.
    Substitute symbols in the extracted exprt with the symbols in the symbol table of the goto model according to the symbol map provided by the user.
    Typecheck all contract exprt.
    Annotate all contract exprt to the corresponding loop.

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\-contract\-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_contract_file.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--loop-contract-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 contract 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_contract_file.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--loop-contract-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 contract 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_contract_file.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--loop-contract-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 contract file.

regression/contracts-dfcc/loop_contracts_memcmp/main.c

@@ -0,0 +1,34 @@
+inline int memcmp(const void *s1, const void *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,9 @@
+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.

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_contract_file.desc

@@ -0,0 +1,10 @@
+CORE gcc-only
+main.c
+--loop-contract-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 contract file.

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_contract_file.desc

@@ -0,0 +1,17 @@
+CORE dfcc-only
+main.c
+--loop-contract-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 contract 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/contract_wrangler.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
       contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
       contracts/dynamic-frames/dfcc_contract_mode.cpp \