Wrap contract expressions in a lambda

This makes sure contracts are self-contained in that any parameter names
that may have only existed in the scope of a function declaration are
now bound variables.

Author: tautschnig

src/ansi-c/c_typecheck_base.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>
+#include <util/mathematical_expr.h>
 #include <util/std_types.h>
 
 #include "ansi_c_declaration.h"
@@ -745,7 +746,7 @@ void c_typecheck_baset::typecheck_declaration(
 
         // ensure parameter declarations are available for type checking to
         // succeed
-        std::vector<symbol_exprt> temporary_parameter_symbols;
+        binding_exprt::variablest temporary_parameter_symbols;
 
         const auto &return_type = code_type.return_type();
         if(return_type.id() != ID_empty)
@@ -780,16 +781,25 @@ void c_typecheck_baset::typecheck_declaration(
         {
           typecheck_spec_function_pointer_obeys_contract(expr);
           check_history_expr(expr);
+          lambda_exprt lambda{temporary_parameter_symbols, expr};
+          expr.swap(lambda);
         }
 
         for(auto &requires : code_type.requires())
         {
           typecheck_expr(requires);
           implicit_typecast_bool(requires);
           check_history_expr(requires);
+          lambda_exprt lambda{temporary_parameter_symbols, requires};
+          requires.swap(lambda);
         }
 
         typecheck_spec_assigns(code_type.assigns());
+        for(auto &assigns : code_type.assigns())
+        {
+          lambda_exprt lambda{temporary_parameter_symbols, assigns};
+          assigns.swap(lambda);
+        }
 
         for(auto &expr : code_type.ensures_contract())
         {
@@ -798,6 +808,8 @@ void c_typecheck_baset::typecheck_declaration(
             expr,
             ID_loop_entry,
             CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
+          lambda_exprt lambda{temporary_parameter_symbols, expr};
+          expr.swap(lambda);
         }
 
         for(auto &ensures : code_type.ensures())
@@ -808,6 +820,8 @@ void c_typecheck_baset::typecheck_declaration(
             ensures,
             ID_loop_entry,
             CPROVER_PREFIX "loop_entry is not allowed in postconditions.");
+          lambda_exprt lambda{temporary_parameter_symbols, ensures};
+          ensures.swap(lambda);
         }
 
         for(const auto &parameter_sym : temporary_parameter_symbols)

src/goto-instrument/contracts/contracts.cpp

@@ -25,7 +25,6 @@ Date: February 2016
 #include <util/message.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/replace_symbol.h>
 #include <util/std_code.h>
 
 #include <goto-programs/goto_inline.h>
@@ -777,15 +776,12 @@ void code_contractst::apply_function_contract(
   // Isolate each component of the contract.
   const auto &type = get_contract(target_function, ns);
   auto assigns_clause = type.assigns();
-  auto requires = conjunction(type.requires());
-  auto ensures = conjunction(type.ensures());
   auto requires_contract = type.requires_contract();
   auto ensures_contract = type.ensures_contract();
 
-  // Create a replace_symbolt object, for replacing expressions in the callee
+  // Prepare to instantiate expressions in the callee
   // with expressions from the call site (e.g. the return value).
-  // This object tracks replacements that are common to ENSURES and REQUIRES.
-  replace_symbolt common_replace;
+  exprt::operandst instantiation_values;
 
   // keep track of the call's return expression to make it nondet later
   optionalt<exprt> call_ret_opt = {};
@@ -804,17 +800,17 @@ void code_contractst::apply_function_contract(
       // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
       auto &lhs_expr = const_target->call_lhs();
       call_ret_opt = lhs_expr;
-      symbol_exprt ret_val(CPROVER_PREFIX "return_value", lhs_expr.type());
-      common_replace.insert(ret_val, lhs_expr);
+      instantiation_values.push_back(lhs_expr);
     }
     else
     {
       // If the function does return a value, but the return value is
       // disregarded, check if the postcondition includes the return value.
-      if(has_subexpr(ensures, [](const exprt &e) {
-           return e.id() == ID_symbol && to_symbol_expr(e).get_identifier() ==
-                                           CPROVER_PREFIX "return_value";
-         }))
+      if(std::any_of(
+           type.ensures().begin(), type.ensures().end(), [](const exprt &e) {
+             return has_symbol_expr(
+               to_lambda_expr(e).where(), CPROVER_PREFIX "return_value", true);
+           }))
       {
         // The postcondition does mention __CPROVER_return_value, so mint a
         // fresh variable to replace __CPROVER_return_value with.
@@ -827,28 +823,19 @@ void code_contractst::apply_function_contract(
           symbol_table.lookup_ref(target_function).mode,
           ns,
           symbol_table);
-        symbol_exprt ret_val(
-          CPROVER_PREFIX "return_value", function_type.return_type());
         auto fresh_sym_expr = fresh.symbol_expr();
-        common_replace.insert(ret_val, fresh_sym_expr);
         call_ret_opt = fresh_sym_expr;
+        instantiation_values.push_back(fresh_sym_expr);
       }
+      else
+        instantiation_values.push_back(nil_exprt{});
     }
   }
 
   // Replace formal parameters
   const auto &arguments = const_target->call_arguments();
-  auto a_it = arguments.begin();
-  for(auto p_it = type.parameters().begin();
-      p_it != type.parameters().end() && a_it != arguments.end();
-      ++p_it, ++a_it)
-  {
-    if(!p_it->get_identifier().empty())
-    {
-      symbol_exprt p(p_it->get_identifier(), p_it->type());
-      common_replace.insert(p, *a_it);
-    }
-  }
+  instantiation_values.insert(
+    instantiation_values.end(), arguments.begin(), arguments.end());
 
   const auto &mode = function_symbol.mode;
 
@@ -860,11 +847,17 @@ void code_contractst::apply_function_contract(
   is_fresh.add_memory_map_decl(new_program);
 
   // Insert assertion of the precondition immediately before the call site.
+  exprt::operandst requires_conjuncts;
+  for(const auto &r : type.requires())
+  {
+    requires_conjuncts.push_back(
+      to_lambda_expr(r).application(instantiation_values));
+  }
+  auto requires = conjunction(requires_conjuncts);
   if(!requires.is_true())
   {
     if(has_subexpr(requires, ID_exists) || has_subexpr(requires, ID_forall))
       add_quantified_variable(requires, mode);
-    common_replace(requires);
 
     goto_programt assertion;
     converter.goto_convert(code_assertt(requires), assertion, mode);
@@ -882,21 +875,27 @@ void code_contractst::apply_function_contract(
   for(auto &expr : requires_contract)
   {
     assert_function_pointer_obeys_contract(
-      to_function_pointer_obeys_contract_expr(expr),
+      to_function_pointer_obeys_contract_expr(
+        to_lambda_expr(expr).application(instantiation_values)),
       ID_precondition,
-      common_replace,
       mode,
       new_program);
   }
 
   // Gather all the instructions required to handle history variables
   // as well as the ensures clause
+  exprt::operandst ensures_conjuncts;
+  for(const auto &r : type.ensures())
+  {
+    ensures_conjuncts.push_back(
+      to_lambda_expr(r).application(instantiation_values));
+  }
+  auto ensures = conjunction(ensures_conjuncts);
   std::pair<goto_programt, goto_programt> ensures_pair;
   if(!ensures.is_false())
   {
     if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall))
       add_quantified_variable(ensures, mode);
-    common_replace(ensures);
 
     auto assumption = code_assumet(ensures);
     ensures_pair =
@@ -908,10 +907,9 @@ void code_contractst::apply_function_contract(
 
   // ASSIGNS clause should not refer to any quantified variables,
   // and only refer to the common symbols to be replaced.
-  exprt targets;
+  exprt::operandst targets;
   for(auto &target : assigns_clause)
-    targets.add_to_operands(std::move(target));
-  common_replace(targets);
+    targets.push_back(to_lambda_expr(target).application(instantiation_values));
 
   // Create a sequence of non-deterministic assignments ...
 
@@ -920,7 +918,7 @@ void code_contractst::apply_function_contract(
 
   havoc_assigns_clause_targetst havocker(
     target_function,
-    targets.operands(),
+    targets,
     goto_functions,
     location,
     symbol_table,
@@ -961,8 +959,8 @@ void code_contractst::apply_function_contract(
   for(auto &expr : ensures_contract)
   {
     assume_function_pointer_obeys_contract(
-      to_function_pointer_obeys_contract_expr(expr),
-      common_replace,
+      to_function_pointer_obeys_contract_expr(
+        to_lambda_expr(expr).application(instantiation_values)),
       mode,
       new_program);
   }
@@ -1399,7 +1397,6 @@ void code_contractst::enforce_contract(const irep_idt &function)
 void code_contractst::assert_function_pointer_obeys_contract(
   const function_pointer_obeys_contract_exprt &expr,
   const irep_idt &property_class,
-  const replace_symbolt &replace,
   const irep_idt &mode,
   goto_programt &dest)
 {
@@ -1411,9 +1408,8 @@ void code_contractst::assert_function_pointer_obeys_contract(
           << "' obeys contract '"
           << from_expr_using_mode(ns, mode, expr.contract()) << "'";
   loc.set_comment(comment.str());
-  exprt function_pointer(expr.function_pointer());
-  replace(function_pointer);
-  code_assertt assert_expr(equal_exprt{function_pointer, expr.contract()});
+  code_assertt assert_expr(
+    equal_exprt{expr.function_pointer(), expr.contract()});
   assert_expr.add_source_location() = loc;
   goto_programt instructions;
   converter.goto_convert(assert_expr, instructions, mode);
@@ -1422,7 +1418,6 @@ void code_contractst::assert_function_pointer_obeys_contract(
 
 void code_contractst::assume_function_pointer_obeys_contract(
   const function_pointer_obeys_contract_exprt &expr,
-  const replace_symbolt &replace,
   const irep_idt &mode,
   goto_programt &dest)
 {
@@ -1433,10 +1428,8 @@ void code_contractst::assume_function_pointer_obeys_contract(
           << "' obeys contract '"
           << from_expr_using_mode(ns, mode, expr.contract()) << "'";
   loc.set_comment(comment.str());
-  exprt function_pointer(expr.function_pointer());
-  replace(function_pointer);
-  dest.add(
-    goto_programt::make_assignment(function_pointer, expr.contract(), loc));
+  dest.add(goto_programt::make_assignment(
+    expr.function_pointer(), expr.contract(), loc));
 }
 
 void code_contractst::add_contract_check(
@@ -1448,8 +1441,6 @@ void code_contractst::add_contract_check(
 
   const auto &code_type = get_contract(wrapper_function, ns);
   auto assigns = code_type.assigns();
-  auto requires = conjunction(code_type.requires());
-  auto ensures = conjunction(code_type.ensures());
   auto requires_contract = code_type.requires_contract();
   auto ensures_contract = code_type.ensures_contract();
   // build:
@@ -1468,10 +1459,9 @@ void code_contractst::add_contract_check(
   const symbolt &function_symbol = ns.lookup(mangled_function);
   code_function_callt call(function_symbol.symbol_expr());
 
-  // Create a replace_symbolt object, for replacing expressions in the callee
+  // Prepare to instantiate expressions in the callee
   // with expressions from the call site (e.g. the return value).
-  // This object tracks replacements that are common to ENSURES and REQUIRES.
-  replace_symbolt common_replace;
+  exprt::operandst instantiation_values;
 
   const auto &source_location = function_symbol.location;
 
@@ -1490,8 +1480,7 @@ void code_contractst::add_contract_check(
     call.lhs() = r;
     return_stmt = code_returnt(r);
 
-    symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
-    common_replace.insert(ret_val, r);
+    instantiation_values.push_back(r);
   }
 
   // decl parameter1 ...
@@ -1516,18 +1505,24 @@ void code_contractst::add_contract_check(
 
     call.arguments().push_back(p);
 
-    common_replace.insert(parameter_symbol.symbol_expr(), p);
+    instantiation_values.push_back(p);
   }
 
   is_fresh_enforcet visitor(*this, log, wrapper_function);
   visitor.create_declarations();
   visitor.add_memory_map_decl(check);
   // Generate: assume(requires)
+  exprt::operandst requires_conjuncts;
+  for(const auto &r : code_type.requires())
+  {
+    requires_conjuncts.push_back(
+      to_lambda_expr(r).application(instantiation_values));
+  }
+  auto requires = conjunction(requires_conjuncts);
   if(!requires.is_false())
   {
     if(has_subexpr(requires, ID_exists) || has_subexpr(requires, ID_forall))
       add_quantified_variable(requires, function_symbol.mode);
-    common_replace(requires);
 
     goto_programt assumption;
     converter.goto_convert(
@@ -1540,11 +1535,17 @@ void code_contractst::add_contract_check(
   std::pair<goto_programt, goto_programt> ensures_pair;
 
   // Generate: copies for history variables
+  exprt::operandst ensures_conjuncts;
+  for(const auto &r : code_type.ensures())
+  {
+    ensures_conjuncts.push_back(
+      to_lambda_expr(r).application(instantiation_values));
+  }
+  auto ensures = conjunction(ensures_conjuncts);
   if(!ensures.is_true())
   {
     if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall))
       add_quantified_variable(ensures, function_symbol.mode);
-    common_replace(ensures);
 
     // get all the relevant instructions related to history variables
     auto assertion = code_assertt(ensures);
@@ -1567,8 +1568,8 @@ void code_contractst::add_contract_check(
   for(auto &expr : requires_contract)
   {
     assume_function_pointer_obeys_contract(
-      to_function_pointer_obeys_contract_expr(expr),
-      common_replace,
+      to_function_pointer_obeys_contract_expr(
+        to_lambda_expr(expr).application(instantiation_values)),
       function_symbol.mode,
       check);
   }
@@ -1586,9 +1587,9 @@ void code_contractst::add_contract_check(
   for(auto &expr : ensures_contract)
   {
     assert_function_pointer_obeys_contract(
-      to_function_pointer_obeys_contract_expr(expr),
+      to_function_pointer_obeys_contract_expr(
+        to_lambda_expr(expr).application(instantiation_values)),
       ID_postcondition,
-      common_replace,
       function_symbol.mode,
       check);
   }