Expose check_renaming utility function

In the process it is moved (without change) to renaming_level.h/cpp,
alongside the similarly-structured get_original_name functions.

Author: smowton

src/goto-symex/goto_symex_state.cpp

@@ -48,90 +48,6 @@ goto_symex_statet::goto_symex_statet(
 
 goto_symex_statet::~goto_symex_statet()=default;
 
-/// Check that \p expr is correctly renamed to level 2 and return true in case
-/// an error is detected.
-static bool check_renaming(const exprt &expr);
-
-static bool check_renaming(const typet &type)
-{
-  if(type.id()==ID_array)
-    return check_renaming(to_array_type(type).size());
-  else if(type.id() == ID_struct || type.id() == ID_union)
-  {
-    for(const auto &c : to_struct_union_type(type).components())
-      if(check_renaming(c.type()))
-        return true;
-  }
-  else if(type.has_subtype())
-    return check_renaming(to_type_with_subtype(type).subtype());
-
-  return false;
-}
-
-static bool check_renaming_l1(const exprt &expr)
-{
-  if(check_renaming(expr.type()))
-    return true;
-
-  if(expr.id()==ID_symbol)
-  {
-    const auto &type = expr.type();
-    if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
-    if(!to_ssa_expr(expr).get_level_2().empty())
-      return true;
-    if(to_ssa_expr(expr).get_original_expr().type() != type)
-      return true;
-  }
-  else
-  {
-    forall_operands(it, expr)
-      if(check_renaming_l1(*it))
-        return true;
-  }
-
-  return false;
-}
-
-static bool check_renaming(const exprt &expr)
-{
-  if(check_renaming(expr.type()))
-    return true;
-
-  if(
-    expr.id() == ID_address_of &&
-    to_address_of_expr(expr).object().id() == ID_symbol)
-  {
-    return check_renaming_l1(to_address_of_expr(expr).object());
-  }
-  else if(
-    expr.id() == ID_address_of &&
-    to_address_of_expr(expr).object().id() == ID_index)
-  {
-    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
-    return check_renaming_l1(index_expr.array()) ||
-           check_renaming(index_expr.index());
-  }
-  else if(expr.id()==ID_symbol)
-  {
-    const auto &type = expr.type();
-    if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
-    if(to_ssa_expr(expr).get_level_2().empty())
-      return true;
-    if(to_ssa_expr(expr).get_original_expr().type() != type)
-      return true;
-  }
-  else
-  {
-    forall_operands(it, expr)
-      if(check_renaming(*it))
-        return true;
-  }
-
-  return false;
-}
-
 template <>
 renamedt<ssa_exprt, L0>
 goto_symex_statet::set_indices<L0>(ssa_exprt ssa_expr, const namespacet &ns)

src/goto-symex/renaming_level.cpp

@@ -205,3 +205,83 @@ typet get_original_name(typet type)
   }
   return type;
 }
+
+bool check_renaming(const typet &type)
+{
+  if(type.id() == ID_array)
+    return check_renaming(to_array_type(type).size());
+  else if(type.id() == ID_struct || type.id() == ID_union)
+  {
+    for(const auto &c : to_struct_union_type(type).components())
+      if(check_renaming(c.type()))
+        return true;
+  }
+  else if(type.has_subtype())
+    return check_renaming(to_type_with_subtype(type).subtype());
+
+  return false;
+}
+
+bool check_renaming_l1(const exprt &expr)
+{
+  if(check_renaming(expr.type()))
+    return true;
+
+  if(expr.id() == ID_symbol)
+  {
+    const auto &type = expr.type();
+    if(!expr.get_bool(ID_C_SSA_symbol))
+      return type.id() != ID_code && type.id() != ID_mathematical_function;
+    if(!to_ssa_expr(expr).get_level_2().empty())
+      return true;
+    if(to_ssa_expr(expr).get_original_expr().type() != type)
+      return true;
+  }
+  else
+  {
+    forall_operands(it, expr)
+      if(check_renaming_l1(*it))
+        return true;
+  }
+
+  return false;
+}
+
+bool check_renaming(const exprt &expr)
+{
+  if(check_renaming(expr.type()))
+    return true;
+
+  if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_symbol)
+  {
+    return check_renaming_l1(to_address_of_expr(expr).object());
+  }
+  else if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_index)
+  {
+    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
+    return check_renaming_l1(index_expr.array()) ||
+           check_renaming(index_expr.index());
+  }
+  else if(expr.id() == ID_symbol)
+  {
+    const auto &type = expr.type();
+    if(!expr.get_bool(ID_C_SSA_symbol))
+      return type.id() != ID_code && type.id() != ID_mathematical_function;
+    if(to_ssa_expr(expr).get_level_2().empty())
+      return true;
+    if(to_ssa_expr(expr).get_original_expr().type() != type)
+      return true;
+  }
+  else
+  {
+    forall_operands(it, expr)
+      if(check_renaming(*it))
+        return true;
+  }
+
+  return false;
+}

src/goto-symex/renaming_level.h

@@ -103,4 +103,16 @@ exprt get_original_name(exprt expr);
 /// Undo all levels of renaming
 typet get_original_name(typet type);
 
+/// Check that \p expr is correctly renamed to level 2 and return true in case
+/// an error is detected.
+bool check_renaming(const exprt &expr);
+
+/// Check that \p expr is correctly renamed to level 1 and return true in case
+/// an error is detected.
+bool check_renaming_l1(const exprt &expr);
+
+/// Check that \p type is correctly renamed to level 2 and return true in case
+/// an error is detected.
+bool check_renaming(const typet &type);
+
 #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H