Add an --assert-ensures check

regression/contracts/assert_ensures_01/main.c

@@ -0,0 +1,18 @@
+// This tests whether the flag --assert-ensures adds the assert of the
+// ensures statement after the call
+
+#include <assert.h>
+
+int min(int a, int b) __CPROVER_ensures(
+  __CPROVER_return_value <= a && __CPROVER_return_value <= b &&
+  (__CPROVER_return_value == a || __CPROVER_return_value == b))
+{
+  return 100;
+}
+
+int main()
+{
+  int x, y, z;
+  z = min(x, y);
+  return z;
+}

regression/contracts/assert_ensures_01/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--assert-ensures min
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

regression/contracts/assert_ensures_02/main.c

@@ -0,0 +1,21 @@
+// This tests whether --assert-ensures correctly handles function
+// calls in the contract
+
+#include <assert.h>
+
+int is_min(int min, int a, int b)
+{
+  return min <= a && min <= b && (min == a || min == b);
+}
+
+int min(int a, int b) __CPROVER_ensures(is_min(__CPROVER_return_value, a, b))
+{
+  return 100;
+}
+
+int main()
+{
+  int x, y, z;
+  z = min(x, y);
+  return z;
+}

regression/contracts/assert_ensures_02/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--assert-ensures min
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

src/goto-instrument/code_contracts.cpp

@@ -15,8 +15,10 @@ Date: February 2016
 
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
+#include <util/message.h>
 #include <util/replace_symbol.h>
 
+#include <goto-programs/goto_convert.h>
 #include <goto-programs/remove_skip.h>
 
 #include <analyses/local_may_alias.h>
@@ -30,12 +32,18 @@ class code_contractst
 public:
   code_contractst(
     symbol_tablet &_symbol_table,
-    goto_functionst &_goto_functions):
-      ns(_symbol_table),
+    goto_functionst &_goto_functions,
+    std::list<std::string> _functions_to_assert_ensures)
+    : ns(_symbol_table),
       symbol_table(_symbol_table),
       goto_functions(_goto_functions),
+      functions_to_assert_ensures(_functions_to_assert_ensures),
       temporary_counter(0)
   {
+    if(functions_to_assert_ensures.empty())
+      mode_assert_ensures = false;
+    else
+      mode_assert_ensures = true;
   }
 
   void operator()();
@@ -44,9 +52,12 @@ class code_contractst
   namespacet ns;
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
+  std::list<std::string> functions_to_assert_ensures;
 
   unsigned temporary_counter;
 
+  bool mode_assert_ensures;
+
   std::unordered_set<irep_idt> summarized;
 
   void code_contracts(goto_functionst::goto_functiont &goto_function);
@@ -55,6 +66,12 @@ class code_contractst
     goto_programt &goto_program,
     goto_programt::targett target);
 
+  void
+  assert_ensures_after_calls(goto_functionst::goto_functiont &goto_function);
+
+  void
+  assert_ensures(goto_programt &goto_program, goto_programt::targett target);
+
   void add_contract_check(
     const irep_idt &function,
     goto_programt &dest);
@@ -242,6 +259,70 @@ void code_contractst::code_contracts(
       apply_contract(goto_function.body, it);
 }
 
+void code_contractst::assert_ensures(
+  goto_programt &goto_program,
+  goto_programt::targett target)
+{
+  const code_function_callt &call = target->get_function_call();
+
+  // we don't handle function pointers
+  if(call.function().id() != ID_symbol)
+    return;
+
+  const irep_idt &function = to_symbol_expr(call.function()).get_identifier();
+  const symbolt &f_sym = ns.lookup(function);
+  const code_typet &type = to_code_type(f_sym.type);
+
+  exprt ensures = static_cast<const exprt &>(type.find(ID_C_spec_ensures));
+
+  // is there a contract?
+  if(ensures.is_nil())
+    return;
+
+  // replace formal parameters by arguments, replace return
+  replace_symbolt replace;
+
+  // TODO: return value could be nil
+  if(type.return_type() != empty_typet())
+  {
+    symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
+    replace.insert(ret_val, call.lhs());
+  }
+
+  // formal parameters
+  code_function_callt::argumentst::const_iterator a_it =
+    call.arguments().begin();
+  for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
+      p_it != type.parameters().end() && a_it != call.arguments().end();
+      ++p_it, ++a_it)
+    if(!p_it->get_identifier().empty())
+    {
+      symbol_exprt p(p_it->get_identifier(), p_it->type());
+      replace.insert(p, *a_it);
+    }
+
+  replace(ensures);
+
+  // assert the ensures part of the contract after the call
+  ++target;
+  code_assertt a(ensures);
+  goto_programt new_goto_program;
+  null_message_handlert message_handler;
+  // We first need to convert the expression to a goto_program
+  goto_convert(a, symbol_table, new_goto_program, message_handler, ID_C);
+
+  goto_program.insert_before_swap(target, new_goto_program);
+}
+
+void code_contractst::assert_ensures_after_calls(
+  goto_functionst::goto_functiont &goto_function)
+{
+  // look at all function calls
+  Forall_goto_program_instructions(it, goto_function.body)
+    if(it->is_function_call())
+      assert_ensures(goto_function.body, it);
+}
+
 const symbolt &code_contractst::new_tmp_symbol(
   const typet &type,
   const source_locationt &source_location,
@@ -372,23 +453,39 @@ void code_contractst::add_contract_check(
 
 void code_contractst::operator()()
 {
-  Forall_goto_functions(it, goto_functions)
-    code_contracts(it->second);
-
-  goto_functionst::function_mapt::iterator i_it=
-    goto_functions.function_map.find(INITIALIZE_FUNCTION);
-  assert(i_it!=goto_functions.function_map.end());
+  if(mode_assert_ensures)
+  {
+    Forall_goto_functions(it, goto_functions)
+      assert_ensures_after_calls(it->second);
+  }
+  else
+  {
+    Forall_goto_functions(it, goto_functions)
+      code_contracts(it->second);
 
-  for(const auto &contract : summarized)
-    add_contract_check(contract, i_it->second.body);
+    goto_functionst::function_mapt::iterator i_it =
+      goto_functions.function_map.find(INITIALIZE_FUNCTION);
+    INVARIANT(
+      i_it != goto_functions.function_map.end(),
+      "There must exist an INITIALIZE_FUNCTION");
 
-  // remove skips
-  remove_skip(i_it->second.body);
+    for(const auto &contract : summarized)
+      add_contract_check(contract, i_it->second.body);
 
+    // remove skips
+    remove_skip(i_it->second.body);
+  }
   goto_functions.update();
 }
 
+void assert_ensures(goto_modelt &goto_model, std::list<std::string> functions)
+{
+  code_contractst(
+    goto_model.symbol_table, goto_model.goto_functions, functions)();
+}
+
 void code_contracts(goto_modelt &goto_model)
 {
-  code_contractst(goto_model.symbol_table, goto_model.goto_functions)();
+  std::list<std::string> empty;
+  code_contractst(goto_model.symbol_table, goto_model.goto_functions, empty)();
 }

src/goto-instrument/code_contracts.h

@@ -14,8 +14,13 @@ Date: February 2016
 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
 #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H
 
+#include <list>
+#include <string>
+
 class goto_modelt;
 
 void code_contracts(goto_modelt &);
 
+void assert_ensures(goto_modelt &goto_model, std::list<std::string> functions);
+
 #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1088,6 +1088,22 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     code_contracts(goto_model);
   }
 
+  // assert the ensures part of the contract for the given functions
+  if(cmdline.isset("assert-ensures"))
+  {
+    log.status() << "Asserting code contract" << messaget::eom;
+    std::list<std::string> functions_to_assert_ensures =
+      cmdline.get_values("assert-ensures");
+    if(functions_to_assert_ensures.empty())
+    {
+      log.error()
+        << "At least one function name has to be given with --assert-ensures"
+        << messaget::eom;
+      throw 0;
+    }
+    assert_ensures(goto_model, functions_to_assert_ensures);
+  }
+
   // replace function pointers, if explicitly requested
   if(cmdline.isset("remove-function-pointers"))
   {
@@ -1643,6 +1659,7 @@ void goto_instrument_parse_optionst::help()
     " --nondet-static-exclude e    same as nondet-static except for the variable e\n" //NOLINT(*)
     "                              (use multiple times if required)\n"
     " --check-invariant function   instruments invariant checking function\n"
+    " --assert-ensures function    checks that function satisfies its contract ensures after each call\n" // NOLINT(*)
     " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
     " --splice-call caller,callee  prepends a call to callee in the body of caller\n"  // NOLINT(*)
     " --undefined-function-is-assume-false\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -94,7 +94,8 @@ Author: Daniel Kroening, [email protected]
   "(interpreter)(show-reaching-definitions)" \
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
-  "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
+  "(horn)(skip-loops):(apply-code-contracts)" \
+  "(assert-ensures):(model-argc-argv):" \
   "(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\