Add a partial-skolemization (bound-variable renaming) module in goto-programs.

That allows us to do a bound-variables renaming early in `process-goto-programs`,
which then allows us to not have problems with clashing identifiers later on.

This performs only partial-skolemisation (doesn't eliminate the quantifier, but
renames the bound variables) because for the correct operation of VCCs we need
to preserve the exists statement.

Author: NlightNFotis

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

@@ -1,5 +1,5 @@
 CORE
-valid_index_range.c
+negated_exists.c
 --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$

src/goto-programs/Makefile

@@ -65,6 +65,7 @@ SRC = allocate_objects.cpp \
       show_goto_functions_xml.cpp \
       show_properties.cpp \
       show_symbol_table.cpp \
+      skolemization.cpp \
       slice_global_inits.cpp \
       string_abstraction.cpp \
       string_instrumentation.cpp \

src/goto-programs/process_goto_program.cpp

@@ -23,6 +23,7 @@ Author: Martin Brain, [email protected]
 #include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/rewrite_union.h>
+#include <goto-programs/skolemization.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
 
@@ -64,6 +65,8 @@ bool process_goto_program(
   if(options.get_bool_option("rewrite-union"))
     rewrite_union(goto_model);
 
+  rename_variables_in_existential_quantifiers(goto_model);
+
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
   goto_check(options, goto_model);

src/goto-programs/skolemization.cpp

@@ -0,0 +1,69 @@
+/// \file skolemization.h
+/// Rename variables in existentially quantified statements.
+/// Author: Diffblue Ltd.
+
+#include "skolemization.h"
+
+#include "goto_model.h"
+
+#include <ansi-c/expr2c.h>
+
+#include <util/expr_util.h>
+#include <util/fresh_symbol.h>
+#include <util/irep.h> // for id2string
+#include <util/mathematical_expr.h>
+
+void rename_variables_in_existential_quantifiers(goto_modelt &goto_model)
+{
+  for(auto &function : goto_model.goto_functions.function_map)
+  {
+    for(auto &instruction : function.second.body.instructions)
+    {
+      if(instruction.has_condition())
+      {
+        auto &cond = instruction.condition_nonconst();
+        recurse_on_condition(cond, goto_model);
+      }
+    }
+  }
+}
+
+void recurse_on_condition(exprt &cond, goto_modelt &model)
+{
+  // recurse on the condition's subexpressions first - that allows us
+  // to correctly identify the nodes we care about in a compound
+  // expression, for instance something like `1 == 1 && exists(i.i>=0 && i>1)`
+  for(exprt &subexpr : cond.operands())
+  {
+    recurse_on_condition(subexpr, model);
+  }
+
+  // if the expression we're in doesn't have any more operands,
+  // it means it's a leaf node, so we go ahead and process it.
+  rename_and_substitute(cond, model);
+}
+
+void rename_and_substitute(exprt &cond, goto_modelt &model)
+{
+  // perform the first part of skolemisation, by identifying an existentially
+  // quantified statement and substituting the variables with skolem constants.
+  if(can_cast_expr<exists_exprt>(cond))
+  {
+    quantifier_exprt &quantifier_expr = to_quantifier_expr(cond);
+    const auto &quantifier_sym = quantifier_expr.symbol();
+
+    const auto new_symbol = get_fresh_aux_symbol(
+      quantifier_sym.type(),
+      CPROVER_PREFIX,
+      id2string(
+        model.symbol_table.lookup(quantifier_sym.get_identifier())->base_name),
+      quantifier_expr.source_location(),
+      ID_C,
+      model.symbol_table);
+    const auto symbol_expr =
+      symbol_exprt(new_symbol.name, quantifier_sym.type());
+    const std::vector<exprt> new_sym_vec{symbol_expr};
+
+    cond = exists_exprt(symbol_expr, quantifier_expr.instantiate(new_sym_vec));
+  }
+}

src/goto-programs/skolemization.h

@@ -0,0 +1,30 @@
+/// \file skolemization.h
+/// Rename variables in existentially quantified statements.
+/// Author: Diffblue Ltd.
+
+#ifndef CPROVER_GOTO_PROGRAMS_SKOLEMIZATION_H
+#define CPROVER_GOTO_PROGRAMS_SKOLEMIZATION_H
+
+class exprt;
+class goto_modelt;
+
+/// Rename bound variables in existential quantifiers. This is the entry
+/// point to the module.
+/// \param goto_model The goto_model on which we operate. Needed
+///    for making changes to the symbol table at variable renaming time.
+void rename_variables_in_existential_quantifiers(goto_modelt &goto_model);
+
+/// Helper function that recurses over the condition expression of instructions.
+/// \param cond The condition on which we recurse over the operands (subexpressions).
+/// \param model The goto_model we are inserting the new symbol to.
+void recurse_on_condition(exprt &cond, goto_modelt &model);
+
+/// Helper function that does the actual renaming of the variables.
+/// This is called when we reach the atomic parts of the condition expression,
+/// to identify and rename the variables of any quantified statements that
+/// exist as part of the guard.
+/// \param cond The condition in which we are doing the renaming.
+/// \param model The goto_model we are inserting the new symbol to.
+void rename_and_substitute(exprt &cond, goto_modelt &model);
+
+#endif