Function contracts: add missing DECL/DEAD instructions for ignored_return_value variables introduced by contract replacement (these would previously appear as global variables).

Author: Remi Delmas

regression/contracts/assigns-replace-ignored-return-value/main.c

@@ -0,0 +1,37 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+int bar(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  return l + r;
+}
+
+int *baz(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    *__CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  int *res = malloc(sizeof(int));
+  *res = l + r;
+  return res;
+}
+
+int foo(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  bar(l, r);
+  bar(l, r);
+  baz(l, r);
+  baz(l, r);
+  return l + r;
+}
+
+int main()
+{
+  int l;
+  int r;
+  foo(l, r);
+  return 0;
+}

regression/contracts/assigns-replace-ignored-return-value/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^[.*] Check that .*ignored_return_value.* is assignable: FAILURE
+--
+This test checks that when replacing a call by a contract for a call that
+ignores the return value of the function, the temporary introduced to 
+receive the call result does not trigger errors with assigns clause Checking
+in the function under verification.

src/goto-instrument/contracts/contracts.cpp

@@ -672,6 +672,9 @@ bool code_contractst::apply_function_contract(
   // keep track of the call's return expression to make it nondet later
   optionalt<exprt> call_ret_opt = {};
 
+  // if true, the call return variable variable was created during replacement
+  bool call_ret_is_fresh_var = false;
+
   if(type.return_type() != empty_typet())
   {
     // Check whether the function's return value is not disregarded.
@@ -696,6 +699,7 @@ bool code_contractst::apply_function_contract(
       {
         // The postcondition does mention __CPROVER_return_value, so mint a
         // fresh variable to replace __CPROVER_return_value with.
+        call_ret_is_fresh_var = true;
         const symbolt &fresh = get_fresh_aux_symbol(
           type.return_type(),
           id2string(target_function),
@@ -803,6 +807,12 @@ bool code_contractst::apply_function_contract(
     auto &call_ret = call_ret_opt.value();
     auto &loc = call_ret.source_location();
     auto &type = call_ret.type();
+
+    // Declare if fresh
+    if(call_ret_is_fresh_var)
+      havoc_instructions.add(
+        goto_programt::make_decl(to_symbol_expr(call_ret), loc));
+
     side_effect_expr_nondett expr(type, location);
     auto target = havoc_instructions.add(
       goto_programt::make_assignment(call_ret, expr, loc));
@@ -819,6 +829,17 @@ bool code_contractst::apply_function_contract(
     is_fresh.update_ensures(ensures_pair.first);
     insert_before_swap_and_advance(function_body, target, ensures_pair.first);
   }
+
+  // Kill return value variable if fresh
+  if(call_ret_is_fresh_var)
+  {
+    function_body.output_instruction(ns, "", log.warning(), *target);
+    auto dead_inst =
+      goto_programt::make_dead(to_symbol_expr(call_ret_opt.value()), location);
+    function_body.insert_before_swap(target, dead_inst);
+    ++target;
+  }
+
   *target = goto_programt::make_skip();
 
   // Add this function to the set of replaced functions.