Merge pull request #3947 from tautschnig/revert-symex-renaming

Revert symex renaming

Author: peterschrammel

regression/cbmc/vla1/main.c

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/fresh_symbol.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
@@ -609,25 +608,43 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
         throw 0;
       }
 
-      symbolt &new_symbol = get_fresh_aux_symbol(
-        size_type(),
-        id2string(current_symbol.name) + "$array_size",
-        id2string(current_symbol.base_name) + "$array_size",
-        size_source_location,
-        mode,
-        symbol_table);
+      // Need to pull out! We insert new symbol.
+      unsigned count = 0;
+      irep_idt temp_identifier;
+      std::string suffix;
+
+      do
+      {
+        suffix = "$array_size" + std::to_string(count);
+        temp_identifier = id2string(current_symbol.name) + suffix;
+        count++;
+      } while(symbol_table.symbols.find(temp_identifier) !=
+              symbol_table.symbols.end());
+
+      // add the symbol to symbol table
+      auxiliary_symbolt new_symbol;
+      new_symbol.name = temp_identifier;
+      new_symbol.pretty_name = id2string(current_symbol.pretty_name) + suffix;
+      new_symbol.base_name = id2string(current_symbol.base_name) + suffix;
+      new_symbol.type = size.type();
       new_symbol.type.set(ID_C_constant, true);
-      new_symbol.value = typecast_exprt::conditional_cast(size, size_type());
+      new_symbol.value = size;
+      new_symbol.location = size_source_location;
+      new_symbol.mode = mode;
+
+      symbol_table.add(new_symbol);
 
       // produce the code that declares and initializes the symbol
-      symbol_exprt symbol_expr = new_symbol.symbol_expr();
+      symbol_exprt symbol_expr;
+      symbol_expr.set_identifier(temp_identifier);
+      symbol_expr.type() = new_symbol.type;
 
       code_declt declaration(symbol_expr);
       declaration.add_source_location() = size_source_location;
 
       code_assignt assignment;
       assignment.lhs()=symbol_expr;
-      assignment.rhs() = new_symbol.value;
+      assignment.rhs() = size;
       assignment.add_source_location() = size_source_location;
 
       // store the code

regression/cbmc/vla1/program-only.desc

@@ -618,70 +618,12 @@ void goto_symex_statet::rename_address(
   }
 }
 
-/// Return true if, and only if, the \p type or one of its subtypes requires SSA
-/// renaming. Renaming is necessary when symbol expressions occur within the
-/// type, which is the case for arrays of non-constant size.
-static bool requires_renaming(const typet &type, const namespacet &ns)
-{
-  if(type.id() == ID_array)
-  {
-    const auto &array_type = to_array_type(type);
-    return requires_renaming(array_type.subtype(), ns) ||
-           !array_type.size().is_constant();
-  }
-  else if(
-    type.id() == ID_struct || type.id() == ID_union || type.id() == ID_class)
-  {
-    const struct_union_typet &s_u_type = to_struct_union_type(type);
-    const struct_union_typet::componentst &components = s_u_type.components();
-
-    for(auto &component : components)
-    {
-      // be careful, or it might get cyclic
-      if(
-        component.type().id() != ID_pointer &&
-        requires_renaming(component.type(), ns))
-      {
-        return true;
-      }
-    }
-
-    return false;
-  }
-  else if(type.id() == ID_pointer)
-  {
-    return requires_renaming(to_pointer_type(type).subtype(), ns);
-  }
-  else if(type.id() == ID_symbol_type)
-  {
-    const symbolt &symbol = ns.lookup(to_symbol_type(type));
-    return requires_renaming(symbol.type, ns);
-  }
-  else if(type.id() == ID_union_tag)
-  {
-    const symbolt &symbol = ns.lookup(to_union_tag_type(type));
-    return requires_renaming(symbol.type, ns);
-  }
-  else if(type.id() == ID_struct_tag)
-  {
-    const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
-    return requires_renaming(symbol.type, ns);
-  }
-
-  return false;
-}
-
 void goto_symex_statet::rename(
   typet &type,
   const irep_idt &l1_identifier,
   const namespacet &ns,
   levelt level)
 {
-  // check whether there are symbol expressions in the type; if not, there
-  // is no need to expand the struct/union tags in the type
-  if(!requires_renaming(type, ns))
-    return; // no action
-
   // rename all the symbols with their last known value
   // to the given level