Refactor and cleanup

We do not need to do quantifier replacement within ASSIGNS annotation.
The replacement maps for ENSURES and REQUIRES clauses should also be
maintained independently.

Author: SaswatPadhi

src/goto-instrument/code_contracts.cpp

@@ -172,9 +172,9 @@ bool code_contractst::has_contract(const irep_idt fun_name)
 }
 
 void code_contractst::add_quantified_variable(
-  exprt expression,
+  const exprt &expression,
   replace_symbolt &replace,
-  irep_idt mode)
+  const irep_idt &mode)
 {
   if(expression.id() == ID_not || expression.id() == ID_typecast)
   {
@@ -213,15 +213,13 @@ void code_contractst::add_quantified_variable(
   else if(expression.id() == ID_exists || expression.id() == ID_forall)
   {
     // When a quantifier expression is found,
-    // 1. get quantified variables
+    // for each quantified variable ...
     const auto &quantifier_expression = to_quantifier_expr(expression);
-    const auto &quantified_variables = quantifier_expression.variables();
-    for(const auto &quantified_variable : quantified_variables)
+    for(const auto &quantified_variable : quantifier_expression.variables())
     {
-      // for each quantified variable...
       const auto &quantified_symbol = to_symbol_expr(quantified_variable);
 
-      // 1.1 create fresh symbol
+      // 1. create fresh symbol
       symbolt new_symbol = get_fresh_aux_symbol(
         quantified_symbol.type(),
         id2string(quantified_symbol.get_identifier()),
@@ -230,12 +228,12 @@ void code_contractst::add_quantified_variable(
         mode,
         symbol_table);
 
-      // 1.2 add created fresh symbol to expression map
+      // 2. add created fresh symbol to expression map
       symbol_exprt q(
         quantified_symbol.get_identifier(), quantified_symbol.type());
       replace.insert(q, new_symbol.symbol_expr());
 
-      // 1.3 recursively check for nested quantified formulae
+      // 3. recursively check for nested quantified formulae
       add_quantified_variable(quantifier_expression.where(), replace, mode);
     }
   }
@@ -356,7 +354,8 @@ bool code_contractst::apply_function_contract(
 
   // Create a replace_symbolt object, for replacing expressions in the callee
   // with expressions from the call site (e.g. the return value).
-  replace_symbolt replace;
+  // This object tracks replacements that are common to ENSURES and REQUIRES.
+  replace_symbolt common_replace;
   if(type.return_type() != empty_typet())
   {
     // Check whether the function's return value is not disregarded.
@@ -367,7 +366,7 @@ bool code_contractst::apply_function_contract(
       // rewrite calls to foo as follows:
       // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5)
       symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
-      replace.insert(ret_val, call.lhs());
+      common_replace.insert(ret_val, call.lhs());
     }
     else
     {
@@ -388,38 +387,37 @@ bool code_contractst::apply_function_contract(
           ns,
           symbol_table);
         symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type());
-        replace.insert(ret_val, fresh.symbol_expr());
+        common_replace.insert(ret_val, fresh.symbol_expr());
       }
     }
   }
 
   // Replace formal parameters
-  code_function_callt::argumentst::const_iterator a_it=
-    call.arguments().begin();
-  for(code_typet::parameterst::const_iterator p_it = type.parameters().begin();
+  auto a_it = call.arguments().begin();
+  for(auto 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);
+      common_replace.insert(p, *a_it);
     }
   }
 
-  // Add quantified variables in contracts to the symbol map
-  irep_idt mode = symbol_table.lookup_ref(function).mode;
-  code_contractst::add_quantified_variable(ensures, replace, mode);
-  code_contractst::add_quantified_variable(requires, replace, mode);
+  // ASSIGNS clause should not refer to any quantified variables,
+  // and only refer to the common symbols to be replaced.
+  common_replace(assigns);
 
-  // Replace expressions in the contract components.
-  replace(assigns);
-  replace(requires);
-  replace(ensures);
+  const auto &mode = symbol_table.lookup_ref(function).mode;
 
   // Insert assertion of the precondition immediately before the call site.
   if(requires.is_not_nil())
   {
+    replace_symbolt replace(common_replace);
+    code_contractst::add_quantified_variable(requires, replace, mode);
+    replace(requires);
+
     goto_programt assertion;
     converter.goto_convert(
       code_assertt(requires),
@@ -435,6 +433,10 @@ bool code_contractst::apply_function_contract(
   std::pair<goto_programt, goto_programt> ensures_pair;
   if(ensures.is_not_nil())
   {
+    replace_symbolt replace(common_replace);
+    code_contractst::add_quantified_variable(ensures, replace, mode);
+    replace(ensures);
+
     auto assumption = code_assumet(ensures);
     ensures_pair = create_ensures_instruction(
       assumption,
@@ -616,26 +618,22 @@ void code_contractst::instrument_call_statement(
 
   exprt called_assigns =
     to_code_with_contract_type(called_symbol.type).assigns();
-  if(!called_assigns.is_nil()) // Called function has assigns clause
-  {
-    replace_symbolt replace;
-    // Replace formal parameters
-    code_function_callt::argumentst::const_iterator a_it =
-      call.arguments().begin();
-    for(code_typet::parameterst::const_iterator p_it =
-          called_type.parameters().begin();
+  if(called_assigns.is_not_nil())
+  {
+    replace_symbolt replace_formal_params;
+    auto a_it = call.arguments().begin();
+    for(auto p_it = called_type.parameters().begin();
         p_it != called_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_formal_params.insert(p, *a_it);
       }
     }
-
-    replace(called_assigns);
+    replace_formal_params(called_assigns);
 
     // check compatibility of assigns clause with the called function
     assigns_clauset called_assigns_clause(
@@ -876,11 +874,12 @@ void code_contractst::add_contract_check(
   PRECONDITION(!dest.instructions.empty());
 
   const symbolt &function_symbol = ns.lookup(mangled_fun);
-  const auto &code_type = to_code_with_contract_type(function_symbol.type);
+  auto code_type = to_code_with_contract_type(function_symbol.type);
+
+  exprt &assigns = code_type.assigns();
+  exprt &requires = code_type.requires();
+  exprt &ensures = code_type.ensures();
 
-  const exprt &assigns = code_type.assigns();
-  const exprt &requires = code_type.requires();
-  const exprt &ensures = code_type.ensures();
   INVARIANT(
     ensures.is_not_nil() || assigns.is_not_nil(),
     "Code contract enforcement is trivial without an ensures or assigns "
@@ -905,7 +904,11 @@ void code_contractst::add_contract_check(
 
   // prepare function call including all declarations
   code_function_callt call(function_symbol.symbol_expr());
-  replace_symbolt replace;
+
+  // Create a replace_symbolt object, for replacing 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;
 
   // decl ret
   code_returnt return_stmt;
@@ -923,7 +926,7 @@ void code_contractst::add_contract_check(
     return_stmt = code_returnt(r);
 
     symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type());
-    replace.insert(ret_val, r);
+    common_replace.insert(ret_val, r);
   }
 
   // decl parameter1 ...
@@ -948,39 +951,40 @@ void code_contractst::add_contract_check(
 
     call.arguments().push_back(p);
 
-    replace.insert(parameter_symbol.symbol_expr(), p);
+    common_replace.insert(parameter_symbol.symbol_expr(), p);
   }
 
-  // Add quantified variables in contracts to the symbol map
-  code_contractst::add_quantified_variable(
-    ensures, replace, function_symbol.mode);
-  code_contractst::add_quantified_variable(
-    requires, replace, function_symbol.mode);
-
-  // rewrite any use of __CPROVER_return_value
-  exprt ensures_cond = ensures;
-  replace(ensures_cond);
-
-  // assume(requires)
+  // Generate: assume(requires)
   if(requires.is_not_nil())
   {
-    // rewrite any use of parameters
-    exprt requires_cond = requires;
-    replace(requires_cond);
+    // extend common_replace with quantified variables in REQUIRES,
+    // and then do the replacement
+    replace_symbolt replace(common_replace);
+    code_contractst::add_quantified_variable(
+      requires, replace, function_symbol.mode);
+    replace(requires);
 
     goto_programt assumption;
     converter.goto_convert(
-      code_assumet(requires_cond), assumption, function_symbol.mode);
+      code_assumet(requires), assumption, function_symbol.mode);
     check.destructive_append(assumption);
   }
 
   // Prepare the history variables handling
   std::pair<goto_programt, goto_programt> ensures_pair;
 
+  // Generate: copies for history variables
   if(ensures.is_not_nil())
   {
+    // extend common_replace with quantified variables in ENSURES,
+    // and then do the replacement
+    replace_symbolt replace(common_replace);
+    code_contractst::add_quantified_variable(
+      ensures, replace, function_symbol.mode);
+    replace(ensures);
+
     // get all the relevant instructions related to history variables
-    auto assertion = code_assertt(ensures_cond);
+    auto assertion = code_assertt(ensures);
     ensures_pair = create_ensures_instruction(
       assertion, ensures.source_location(), wrapper_fun, function_symbol.mode);
 
@@ -991,7 +995,7 @@ void code_contractst::add_contract_check(
   // ret=mangled_fun(parameter1, ...)
   check.add(goto_programt::make_function_call(call, skip->source_location));
 
-  // assert(ensures)
+  // Generate: assert(ensures)
   if(ensures.is_not_nil())
   {
     check.destructive_append(ensures_pair.first);

src/goto-instrument/code_contracts.h

@@ -185,9 +185,9 @@ class code_contractst
   /// the quantified variable is added to the symbol table
   /// and to the expression map.
   void add_quantified_variable(
-    exprt expression,
+    const exprt &expression,
     replace_symbolt &replace,
-    irep_idt mode);
+    const irep_idt &mode);
 
   /// This function recursively identifies the "old" expressions within expr
   /// and replaces them with correspoding history variables.

src/util/c_types.h

@@ -352,7 +352,10 @@ class code_with_contract_typet : public code_typet
 
   exprt &assigns()
   {
-    return static_cast<exprt &>(add(ID_C_spec_assigns));
+    auto &result = static_cast<exprt &>(add(ID_C_spec_assigns));
+    if(result.id().empty()) // not initialized?
+      result.make_nil();
+    return result;
   }
 
   const exprt &requires() const
@@ -362,7 +365,10 @@ class code_with_contract_typet : public code_typet
 
   exprt &requires()
   {
-    return static_cast<exprt &>(add(ID_C_spec_requires));
+    auto &result = static_cast<exprt &>(add(ID_C_spec_requires));
+    if(result.id().empty()) // not initialized?
+      result.make_nil();
+    return result;
   }
 
   const exprt &ensures() const
@@ -372,7 +378,10 @@ class code_with_contract_typet : public code_typet
 
   exprt &ensures()
   {
-    return static_cast<exprt &>(add(ID_C_spec_ensures));
+    auto &result = static_cast<exprt &>(add(ID_C_spec_ensures));
+    if(result.id().empty()) // not initialized?
+      result.make_nil();
+    return result;
   }
 };