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 both 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,7 +387,7 @@ 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());
       }
     }
   }
@@ -403,19 +402,29 @@ bool code_contractst::apply_function_contract(
     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
+  // ASSIGNS clause should not refer to any quantified variables,
+  // and only refer to the common symbols to be replaced.
+  common_replace(assigns);
+
   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);
 
-  // Replace expressions in the contract components.
-  replace(assigns);
-  replace(requires);
-  replace(ensures);
+  // Add quantified variables in contracts to the symbol map
+  // and create replacement maps for ENSURES and REQUIRES,
+  // which independently extend common_replace.
+  {
+    replace_symbolt replace(common_replace);
+    code_contractst::add_quantified_variable(ensures, replace, mode);
+    replace(requires);
+  }
+  {
+    replace_symbolt replace(common_replace);
+    code_contractst::add_quantified_variable(requires, replace, mode);
+    replace(ensures);
+  }
 
   // Insert assertion of the precondition immediately before the call site.
   if(requires.is_not_nil())

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.