WIP: use lambda for code contracts

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"
@@ -743,56 +744,60 @@ void c_typecheck_baset::typecheck_declaration(
         code_with_contract_typet code_type =
           to_code_with_contract_type(new_symbol.type);
 
-        // ensure parameter declarations are in the symbol table
-        std::vector<irep_idt> temporary_parameter_symbols;
+        // ensure parameter declarations are available for type checking to
+        // succeed
+        binding_exprt::variablest temporary_parameter_symbols;
+
+        const auto &return_type = code_type.return_type();
+        if(return_type.id() != ID_empty)
+        {
+          parameter_map[CPROVER_PREFIX "return_value"] = return_type;
+          temporary_parameter_symbols.emplace_back(CPROVER_PREFIX "return_value", return_type);
+        }
+
+        std::size_t anon_counter = 0;
         for(auto &p : code_type.parameters())
         {
+          // may be anonymous
           if(p.get_base_name().empty())
-            continue;
+            p.set_base_name("#anon" + std::to_string(anon_counter++));
 
           // produce identifier
-          irep_idt base_name = p.get_base_name();
+          const irep_idt &base_name = p.get_base_name();
           irep_idt parameter_identifier =
             id2string(identifier) + "::" + id2string(base_name);
 
           p.set_identifier(parameter_identifier);
 
-          if(
-            symbol_table.symbols.find(parameter_identifier) ==
-            symbol_table.symbols.end())
-          {
-            parameter_symbolt p_symbol;
-
-            p_symbol.type = p.type();
-            p_symbol.name = parameter_identifier;
-            p_symbol.base_name = base_name;
-            p_symbol.location = p.source_location();
-
-            symbolt *new_p_symbol;
-            move_symbol(p_symbol, new_p_symbol);
-
-            temporary_parameter_symbols.push_back(parameter_identifier);
-          }
+          PRECONDITION(
+            parameter_map.find(parameter_identifier) == parameter_map.end());
+          parameter_map[parameter_identifier] = p.type();
+          temporary_parameter_symbols.emplace_back(parameter_identifier, p.type());
         }
 
         for(auto &expr : code_type.requires_contract())
         {
           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());
-
-        const auto &return_type = code_type.return_type();
-        if(return_type.id() != ID_empty)
-          parameter_map[CPROVER_PREFIX "return_value"] = return_type;
+        for(auto &assigns : code_type.assigns())
+        {
+          lambda_exprt lambda{temporary_parameter_symbols, assigns};
+          assigns.swap(lambda);
+        }
 
         for(auto &expr : code_type.ensures_contract())
         {
@@ -801,6 +806,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())
@@ -811,10 +818,12 @@ 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);
         }
 
-        if(return_type.id() != ID_empty)
-          parameter_map.erase(CPROVER_PREFIX "return_value");
+        for(const auto &parameter_sym : temporary_parameter_symbols)
+          parameter_map.erase(parameter_sym.get_identifier());
 
         // create a contract symbol
         symbolt contract;
@@ -844,11 +853,6 @@ void c_typecheck_baset::typecheck_declaration(
         new_symbol.type.remove(ID_C_spec_ensures_contract);
         new_symbol.type.remove(ID_C_spec_requires);
         new_symbol.type.remove(ID_C_spec_requires_contract);
-
-        // remove parameter declarations if those were only added for type
-        // checking the contract
-        for(const auto &parameter_id : temporary_parameter_symbols)
-          symbol_table.remove(parameter_id);
       }
     }
   }

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,8 +800,7 @@ 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
     {
@@ -827,28 +822,16 @@ 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);
       }
     }
   }
 
   // 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 +843,16 @@ 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 +870,25 @@ 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 =
@@ -961,8 +953,7 @@ 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 +1390,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 +1401,7 @@ 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 +1410,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 +1420,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));
+    goto_programt::make_assignment(expr.function_pointer(), expr.contract(), loc));
 }
 
 void code_contractst::add_contract_check(
@@ -1448,8 +1433,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:
@@ -1473,10 +1456,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;
 
   // decl ret
   optionalt<code_returnt> return_stmt;
@@ -1493,8 +1475,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 ...
@@ -1519,18 +1500,23 @@ 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(
@@ -1543,11 +1529,16 @@ 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);
@@ -1570,8 +1561,7 @@ 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);
   }
@@ -1589,9 +1579,8 @@ 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);
   }