CONTRACTS: replace calls to pure contracts globally

Adds a CLI switch `--replace-pure-contracts` to goto-instrument to
replace calls to pure contracts globally when.

Author: Remi Delmas

doc/cprover-manual/contracts-functions.md

@@ -143,6 +143,27 @@ instruments the code to use the function contract in place of the function
 implementation wherever is invoked, and the third one runs CBMC to check the
 program using contracts.
 
+## Pure contracts
+
+A pure contract is a function definition equipped with a contract and
+for which the body consists of a single call to the function
+`__CPROVER_pure_contract`:
+
+```C
+ret_t foo(param_t params)
+__CPROVER_requires(R)
+__CPROVER_assigns(A)
+__CPROVER_ensures(E)
+{
+  __CPROVER_pure_contract();
+}
+```
+Using `__CPROVER_pure_contract();` in any other way results in a failed
+assertion.
+
+Calls to pure contracts are globally replaced by goto-instrument when the
+flag `--replace-pure-contracts` is specified on the command line.
+
 ## Additional Resources
 
 - [Requires \& Ensures Clauses](contracts-requires-and-ensures.md)

regression/contracts/pure-contracts/main-fail.c

@@ -0,0 +1,41 @@
+#include <stdlib.h>
+
+char nondet_char();
+
+char foo(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires(
+  0 < size  && size < __CPROVER_max_malloc_size && 
+  __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(arr[0],  arr[size-1])
+__CPROVER_ensures(
+  arr[0] == __CPROVER_return_value && arr[size-1] == __CPROVER_return_value)
+// clang-format on
+{
+  char retval = nondet_char();
+  arr[0] = retval;
+  arr[size - 1] = retval;
+  __CPROVER_pure_contract();
+  return retval;
+}
+
+char bar(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires(
+  0 < size  && size < __CPROVER_max_malloc_size && 
+  __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(arr[0],  arr[size-1])
+__CPROVER_ensures(
+  arr[0] == __CPROVER_return_value && arr[size-1] == __CPROVER_return_value)
+// clang-format on
+{
+  return foo(arr, size);
+}
+
+int main()
+{
+  size_t size;
+  char *arr;
+  bar(arr, size);
+  return 0;
+}

regression/contracts/pure-contracts/main.c

@@ -0,0 +1,36 @@
+#include <stdlib.h>
+
+char foo(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires(
+  0 < size && size < __CPROVER_max_malloc_size &&
+  __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(arr[0], arr[size - 1]) 
+__CPROVER_ensures(
+  arr[0] == __CPROVER_return_value && arr[size - 1] == __CPROVER_return_value)
+// clang-format on
+{
+  __CPROVER_pure_contract();
+}
+
+char bar(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires(
+  0 < size && size < __CPROVER_max_malloc_size &&
+  __CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(arr[0], arr[size - 1]) 
+__CPROVER_ensures(
+  arr[0] == __CPROVER_return_value && arr[size - 1] == __CPROVER_return_value)
+// clang-format on
+
+{
+  return foo(arr, size);
+}
+
+int main()
+{
+  size_t size;
+  char *arr;
+  bar(arr, size);
+  return 0;
+}

regression/contracts/pure-contracts/test-fail.desc

@@ -0,0 +1,11 @@
+CORE
+main-fail.c
+--replace-pure-contracts --enforce-contract bar
+^main-fail.c.* error: incorrect use of __CPROVER_pure_contract, function contains other instructions$
+^CONVERSION ERROR$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--
+--
+This test demonstrates that an improper use of __CPROVER_pure_contract 
+is detected and causes a conversion error.

regression/contracts/pure-contracts/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--replace-pure-contracts --enforce-contract bar
+^\[foo.pure_contract.\d+\] line \d+ all calls replaced: (UNREACHABLE|SUCCESS)$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test demonstrates that calls to functions tagged as pure contracts
+replaced by the contract when the command line switch --replace-pure-contracts
+is used. foo is a pure contract, bar has the same contract and calls foo.
+foo gets replaced in bar, and bar satisfies its contract.
+The assertion `foo.pure_contract` is UNREACHABLE or SUCCESS when
+all calls to foo have actually been replaced by foo's contract.

src/goto-instrument/contracts/contracts.cpp

@@ -133,6 +133,18 @@ class inlining_decoratort : public message_handlert
   }
 };
 
+bool code_contractst::is_pure_contract(const irep_idt &function_id)
+{
+  for(const auto &pragma : ns.lookup(function_id).location.get_pragmas())
+  {
+    const auto s = id2string(pragma.first);
+    if(!s.compare(0, 13, "pure_contract"))
+      return true;
+  }
+
+  return false;
+}
+
 void code_contractst::check_apply_loop_contracts(
   const irep_idt &function_name,
   goto_functionst::goto_functiont &goto_function,
@@ -1537,6 +1549,17 @@ void code_contractst::check_all_functions_found(
   }
 }
 
+void code_contractst::replace_pure_contracts()
+{
+  std::set<std::string> to_replace;
+  for(const auto &it : goto_functions.function_map)
+  {
+    if(is_pure_contract(it.first))
+      to_replace.insert(id2string(it.first));
+  }
+  replace_calls(to_replace);
+}
+
 void code_contractst::replace_calls(const std::set<std::string> &to_replace)
 {
   if(to_replace.empty())

src/goto-instrument/contracts/contracts.h

@@ -36,6 +36,12 @@ Date: February 2016
   " --apply-loop-contracts\n"                                                  \
   "                              check and use loop contracts when provided\n"
 
+#define FLAG_REPLACE_PURE_CONTRACTS "replace-pure-contracts"
+#define HELP_REPLACE_PURE_CONTRACTS                                            \
+  " --replace-pure-contracts\n"                                                \
+  "                              replace calls to all functions defined as "   \
+  "                              pure contracts with their contracts\n"
+
 #define FLAG_REPLACE_CALL "replace-call-with-contract"
 #define HELP_REPLACE_CALL                                                      \
   " --replace-call-with-contract <fun>\n"                                      \
@@ -62,6 +68,10 @@ class code_contractst
   {
   }
 
+  /// \brief Replace all calls to functions defined pure contracts by their
+  /// contracts
+  void replace_pure_contracts();
+
   /// Throws an exception if some function `functions` is found in the program.
   void check_all_functions_found(const std::set<std::string> &functions) const;
 
@@ -128,6 +138,10 @@ class code_contractst
 
   std::unordered_set<irep_idt> summarized;
 
+  /// \brief Returns true iff a function is a pure contract and must
+  /// automatically be replaced by its contract
+  bool is_pure_contract(const irep_idt &function_id);
+
   /// \brief Enforce contract of a single function
   void enforce_contract(const irep_idt &function);
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1133,7 +1133,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   if(
     cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) ||
-    cmdline.isset(FLAG_ENFORCE_CONTRACT))
+    cmdline.isset(FLAG_ENFORCE_CONTRACT) ||
+    cmdline.isset(FLAG_REPLACE_PURE_CONTRACTS))
   {
     do_indirect_call_and_rtti_removal();
     code_contractst contracts(goto_model, log);
@@ -1150,6 +1151,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     // first replacement then enforcement. We rely on contract replacement
     // and inlining of sub-function calls to properly annotate all
     // assignments.
+
+    if(cmdline.isset(FLAG_REPLACE_PURE_CONTRACTS))
+      contracts.replace_pure_contracts();
+
     contracts.replace_calls(to_replace);
     contracts.enforce_contracts(to_enforce);
 
@@ -1844,6 +1849,7 @@ void goto_instrument_parse_optionst::help()
     "Code contracts:\n"
     HELP_LOOP_CONTRACTS
     HELP_REPLACE_CALL
+    HELP_REPLACE_PURE_CONTRACTS
     HELP_ENFORCE_CONTRACT
     "\n"
     "Other options:\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -96,6 +96,7 @@ Author: Daniel Kroening, [email protected]
   "(horn)(skip-loops):(model-argc-argv):" \
   "(" FLAG_LOOP_CONTRACTS ")" \
   "(" FLAG_REPLACE_CALL "):" \
+  "(" FLAG_REPLACE_PURE_CONTRACTS ")" \
   "(" FLAG_ENFORCE_CONTRACT "):" \
   "(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \