Pure contacts

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/ansi-c/c_typecheck_base.cpp

@@ -499,6 +499,48 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
   // mismatch.
 }
 
+/// Tries to match `symbol.value` as a code block containing a
+/// single call to `__CPROVER_pure_contract`.
+/// Adds a pragma "pure_contract" to the symbol and the
+/// `__CPROVER_pure_contract` call when successfull.
+void c_typecheck_baset::typecheck_pure_contract(symbolt &symbol)
+{
+  codet &code = to_code(symbol.value);
+  if(!can_cast_expr<code_blockt>(code))
+    return;
+
+  auto &statements = to_code_block(code).statements();
+
+  if(statements.size() != 1)
+    return;
+
+  auto &statement = statements.front();
+
+  if(!can_cast_expr<code_expressiont>(statement))
+    return;
+
+  auto &statement_expr = to_code_expression(statement).expression();
+
+  if(!can_cast_expr<side_effect_expr_function_callt>(statement_expr))
+    return;
+
+  auto &call_expr = to_side_effect_expr_function_call(statement_expr);
+
+  if(call_expr.arguments().size() != 0)
+    return;
+
+  auto &function = call_expr.function();
+
+  if(!can_cast_expr<symbol_exprt>(function))
+    return;
+  auto &symbol_expr = to_symbol_expr(function);
+  if(symbol_expr.get_identifier() == CPROVER_PREFIX "pure_contract")
+  {
+    symbol.location.add_pragma("pure_contract");
+    symbol_expr.add_source_location().add_pragma("pure_contract");
+  }
+}
+
 void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
 {
   if(symbol.value.id() != ID_code)
@@ -550,7 +592,8 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol)
     move_symbol(p_symbol, new_p_symbol);
   }
 
-  // typecheck the body code
+  typecheck_pure_contract(symbol);
+
   typecheck_code(to_code(symbol.value));
 
   // check the labels

src/ansi-c/c_typecheck_base.h

@@ -268,6 +268,8 @@ class c_typecheck_baset:
     symbolt &old_symbol, symbolt &new_symbol);
   void typecheck_function_body(symbolt &symbol);
 
+  void typecheck_pure_contract(symbolt &symbol);
+
   virtual void do_initializer(symbolt &symbol);
 
   static bool is_numeric_type(const typet &src)

src/ansi-c/c_typecheck_expr.cpp

@@ -1940,6 +1940,28 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
     if(entry!=asm_label_map.end())
       identifier=entry->second;
 
+    if(identifier == CPROVER_PREFIX "pure_contract")
+    {
+      const auto &loc = f_op.find_source_location();
+      bool usage_ok = false;
+
+      for(const auto &pragma : loc.get_pragmas())
+      {
+        const auto s = id2string(pragma.first);
+        if(!s.compare(0, 13, "pure_contract"))
+          usage_ok = true;
+      }
+
+      if(!usage_ok)
+      {
+        // throw an error otherwise
+        error().source_location = loc;
+        error() << "incorrect use of " << identifier
+                << ", function contains other instructions" << eom;
+        throw 0;
+      }
+    }
+
     if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
     {
       // This is an undeclared function.

src/ansi-c/cprover_builtin_headers.h

@@ -4,6 +4,7 @@ void __VERIFIER_assume(__CPROVER_bool assumption);
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
 void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);
 void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
+void __CPROVER_pure_contract();
 void __CPROVER_havoc_object(void *);
 void __CPROVER_havoc_slice(void *, __CPROVER_size_t);
 __CPROVER_bool __CPROVER_equal();

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)" \

src/goto-programs/builtin_functions.cpp

@@ -767,7 +767,16 @@ void goto_convertt::do_function_call_symbol(
     return;
   }
 
-  if(identifier == CPROVER_PREFIX "havoc_slice")
+  if(identifier == CPROVER_PREFIX "pure_contract")
+  {
+    const auto &loc = function.find_source_location();
+    goto_programt::targett t =
+      dest.add(goto_programt::make_assertion(false_exprt(), loc));
+    t->source_location_nonconst().set("user-provided", false);
+    t->source_location_nonconst().set_property_class(ID_pure_contract);
+    t->source_location_nonconst().set_comment("all calls replaced");
+  }
+  else if(identifier == CPROVER_PREFIX "havoc_slice")
   {
     do_havoc_slice(lhs, function, arguments, dest, mode);
   }

src/util/irep_ids.def

@@ -88,6 +88,7 @@ IREP_ID_ONE(assign_bitor)
 IREP_ID_ONE(assume)
 IREP_ID_ONE(assert)
 IREP_ID_ONE(assertion)
+IREP_ID_ONE(pure_contract)
 IREP_ID_ONE(precondition)
 IREP_ID_ONE(postcondition)
 IREP_ID_ONE(precondition_instance)