Merge pull request #8430 from tautschnig/no-bound-var-rewrite

Contracts: remove bound-var-rewrite

Author: tautschnig

src/goto-instrument/contracts/contracts.cpp

@@ -68,10 +68,6 @@ void code_contractst::check_apply_loop_contracts(
   // at the start of and end of a loop body
   std::vector<symbol_exprt> old_decreases_vars, new_decreases_vars;
 
-  // replace bound variables by fresh instances
-  if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-    add_quantified_variable(symbol_table, invariant, mode);
-
   // instrument
   //
   //   ... preamble ...
@@ -571,13 +567,6 @@ static void generate_contract_constraints(
   goto_programt &program,
   const source_locationt &location)
 {
-  if(
-    has_subexpr(instantiated_clause, ID_exists) ||
-    has_subexpr(instantiated_clause, ID_forall))
-  {
-    add_quantified_variable(symbol_table, instantiated_clause, mode);
-  }
-
   goto_programt constraint;
   if(location.get_property_class() == ID_assume)
   {

src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp

@@ -235,9 +235,6 @@ dfcc_instrument_loopt::add_prehead_instructions(
   //   GOTO HEAD;
   // ```
 
-  // Replace bound variables by fresh instances in quantified formulas.
-  if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-    add_quantified_variable(symbol_table, invariant, language_mode);
   // initialize loop_entry history vars;
   auto replace_history_result = replace_history_loop_entry(
     symbol_table, invariant, loop_head_location, language_mode);
@@ -429,9 +426,6 @@ dfcc_instrument_loopt::add_step_instructions(
     dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
   {
     // Assume the loop invariant after havocing the state.
-    // Replace bound variables by fresh instances in quantified formulas.
-    if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-      add_quantified_variable(symbol_table, invariant, language_mode);
     code_assumet assumption{invariant};
     assumption.add_source_location() = loop_head_location;
     converter.goto_convert(assumption, step_instrs, language_mode);
@@ -513,9 +507,6 @@ void dfcc_instrument_loopt::add_body_instructions(
       id2string(check_location.get_function()) + "." +
       std::to_string(cbmc_loop_id));
     // Assume the loop invariant after havocing the state.
-    // Replace bound variables by fresh instances in quantified formulas.
-    if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-      add_quantified_variable(symbol_table, invariant, language_mode);
     code_assertt assertion{invariant};
     assertion.add_source_location() = check_location;
     converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);

src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.cpp

@@ -555,13 +555,6 @@ void dfcc_wrapper_programt::encode_requires_clauses()
   {
     exprt requires_lmbd =
       to_lambda_expr(r).application(contract_lambda_parameters);
-    requires_lmbd.add_source_location() = r.source_location();
-    if(
-      has_subexpr(requires_lmbd, ID_exists) ||
-      has_subexpr(requires_lmbd, ID_forall))
-      add_quantified_variable(
-        goto_model.symbol_table, requires_lmbd, language_mode);
-
     source_locationt sl(r.source_location());
     if(statement_type == ID_assert)
     {
@@ -609,9 +602,6 @@ void dfcc_wrapper_programt::encode_ensures_clauses()
                       .application(contract_lambda_parameters)
                       .with_source_location(e);
 
-    if(has_subexpr(ensures, ID_exists) || has_subexpr(ensures, ID_forall))
-      add_quantified_variable(goto_model.symbol_table, ensures, language_mode);
-
     // this also rewrites ID_old expressions to fresh variables
     generate_history_variables_initialization(
       goto_model.symbol_table, ensures, language_mode, history);

src/goto-instrument/contracts/utils.cpp

@@ -381,48 +381,6 @@ void widen_assigns(assignst &assigns, const namespacet &ns)
   assigns = result;
 }
 
-void add_quantified_variable(
-  symbol_table_baset &symbol_table,
-  exprt &expression,
-  const irep_idt &mode)
-{
-  auto visitor = [&symbol_table, &mode](exprt &expr) {
-    if(expr.id() != ID_exists && expr.id() != ID_forall)
-      return;
-    // When a quantifier expression is found, create a fresh symbol for each
-    // quantified variable and rewrite the expression to use those fresh
-    // symbols.
-    auto &quantifier_expression = to_quantifier_expr(expr);
-    std::vector<symbol_exprt> fresh_variables;
-    fresh_variables.reserve(quantifier_expression.variables().size());
-    for(const auto &quantified_variable : quantifier_expression.variables())
-    {
-      // 1. create fresh symbol
-      symbolt new_symbol = get_fresh_aux_symbol(
-        quantified_variable.type(),
-        id2string(quantified_variable.source_location().get_function()),
-        "tmp_cc",
-        quantified_variable.source_location(),
-        mode,
-        symbol_table);
-
-      // 2. add created fresh symbol to expression map
-      fresh_variables.push_back(new_symbol.symbol_expr());
-    }
-
-    // use fresh symbols
-    exprt where = quantifier_expression.instantiate(fresh_variables);
-
-    // recursively check for nested quantified formulae
-    add_quantified_variable(symbol_table, where, mode);
-
-    // replace previous variables and body
-    quantifier_expression.variables() = fresh_variables;
-    quantifier_expression.where() = std::move(where);
-  };
-  expression.visit_pre(visitor);
-}
-
 static void replace_history_parameter_rec(
   symbol_table_baset &symbol_table,
   exprt &expr,

src/goto-instrument/contracts/utils.h

@@ -232,15 +232,6 @@ void infer_loop_assigns(
 /// *(b+i) when `i` is a known constant, keep the expression in the result.
 void widen_assigns(assignst &assigns, const namespacet &ns);
 
-/// This function recursively searches \p expression to find nested or
-/// non-nested quantified expressions. When a quantified expression is found,
-/// a fresh quantified variable is added to the symbol table and \p expression
-/// is updated to use this fresh variable.
-void add_quantified_variable(
-  symbol_table_baset &symbol_table,
-  exprt &expression,
-  const irep_idt &mode);
-
 struct replace_history_parametert
 {
   exprt expression_after_replacement;