factors out quantified variable handling. Handles both replace and enforce flags

Author: Aren Babikian

src/goto-instrument/code_contracts.cpp

@@ -163,6 +163,38 @@ bool code_contractst::has_contract(const irep_idt fun_name)
   return type.has_contract();
 }
 
+void code_contractst::add_quantified_variable(
+  exprt expression, replace_symbolt &replace, irep_idt mode)
+{
+  //If the expression is a quantified expression, this function adds
+  //the quantified variable to the symbol table and to the expression map
+
+  //TODO Currently only works if the contract contains only a single quantified formula
+  // i.e. (1) the top-level element is a quantifier formula
+  //and (2) there are no inner quantifier formulae
+  if(expression.id()==ID_exists || expression.id()==ID_forall)
+  {
+
+    //get quantified symbol
+    exprt tuple = expression.operands().front();
+    exprt quantified_variable = tuple.operands().front();
+    symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
+
+    //create fresh symbol
+    symbolt new_symbol = get_fresh_aux_symbol(
+      quantified_symbol.type(),
+      id2string(quantified_symbol.get_identifier()),
+      "tmp",
+      quantified_symbol.source_location(),
+      mode,
+      symbol_table);
+
+    // add created fresh symbol to expression map
+    symbol_exprt q(quantified_symbol.get_identifier(), quantified_symbol.type());
+    replace.insert(q, new_symbol.symbol_expr());
+  }
+}
+
 bool code_contractst::apply_function_contract(
   const irep_idt &function_id,
   goto_programt &goto_program,
@@ -243,26 +275,11 @@ bool code_contractst::apply_function_contract(
     }
   }
 
-  // Replace quantified variables
-  //TODO go at more depths
-  //TODO Generalize
-  if(ensures.id()==ID_exists || ensures.id()==ID_forall)
-  {
-    exprt tuple = ensures.operands().front();
-    exprt quantified_variable = tuple.operands().front();
-    symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable);
-
-    symbolt new_symbol = get_fresh_aux_symbol(
-      quantified_symbol.type(),
-      id2string(quantified_symbol.get_identifier()),
-      "tmp",
-      quantified_symbol.source_location(),
-      symbol_table.lookup_ref(function).mode,
-      symbol_table);
+  // 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);
 
-    symbol_exprt q(quantified_symbol.get_identifier(), quantified_symbol.type());
-    replace.insert(q, new_symbol.symbol_expr());
-  }
   // Replace expressions in the contract components.
   replace(assigns);
   replace(requires);
@@ -798,6 +815,10 @@ void code_contractst::add_contract_check(
     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);
+
   // assume(requires)
   if(requires.is_not_nil())
   {

src/goto-instrument/code_contracts.h

@@ -25,6 +25,8 @@ Date: February 2016
 #include <util/message.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
+#include <util/pointer_expr.h>
+#include <util/replace_symbol.h>
 
 class messaget;
 class assigns_clauset;
@@ -165,6 +167,19 @@ class code_contractst
 
   void
   add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest);
+
+  const symbolt &new_tmp_symbol(
+    const typet &type,
+    const source_locationt &source_location,
+    const irep_idt &function_id,
+    const irep_idt &mode);
+
+  //If the expression is a quantified expression, this function adds
+  //the quantified variable to the symbol table and to the expression map
+  void add_quantified_variable(
+    exprt expression, 
+    replace_symbolt &replace,
+    irep_idt mode);
 };
 
 #define FLAG_REPLACE_CALL "replace-call-with-contract"