Refactoring in goto_symex

src/goto-symex/goto_symex_state.cpp

@@ -701,6 +701,9 @@ void goto_symex_statet::rename(
     }
   }
 
+  // expand struct and union tag types
+  type = ns.follow(type);
+
   if(type.id()==ID_array)
   {
     auto &array_type = to_array_type(type);
@@ -725,24 +728,6 @@ void goto_symex_statet::rename(
   {
     rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
   }
-  else if(type.id() == ID_symbol_type)
-  {
-    const symbolt &symbol = ns.lookup(to_symbol_type(type));
-    type = symbol.type;
-    rename(type, l1_identifier, ns, level);
-  }
-  else if(type.id() == ID_union_tag)
-  {
-    const symbolt &symbol = ns.lookup(to_union_tag_type(type));
-    type = symbol.type;
-    rename(type, l1_identifier, ns, level);
-  }
-  else if(type.id() == ID_struct_tag)
-  {
-    const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
-    type=symbol.type;
-    rename(type, l1_identifier, ns, level);
-  }
 
   if(level==L2 &&
      !l1_identifier.empty())

src/goto-symex/renaming_level.cpp

@@ -18,7 +18,7 @@ Author: Romain Brenguier, [email protected]
 #include "goto_symex_state.h"
 
 void symex_level0t::
-operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
+operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr) const
 {
   // already renamed?
   if(!ssa_expr.get_level_0().empty())
@@ -42,7 +42,7 @@ operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
   ssa_expr.set_level_0(thread_nr);
 }
 
-void symex_level1t::operator()(ssa_exprt &ssa_expr)
+void symex_level1t::operator()(ssa_exprt &ssa_expr) const
 {
   // already renamed?
   if(!ssa_expr.get_level_1().empty())

src/goto-symex/renaming_level.h

@@ -56,8 +56,8 @@ struct symex_renaming_levelt
 /// The renaming is built for one particular interleaving.
 struct symex_level0t : public symex_renaming_levelt
 {
-  void
-  operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr);
+  void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
+    const;
 
   symex_level0t() = default;
   ~symex_level0t() override = default;
@@ -68,7 +68,7 @@ struct symex_level0t : public symex_renaming_levelt
 /// This is to preserve locality in case of recursion
 struct symex_level1t : public symex_renaming_levelt
 {
-  void operator()(ssa_exprt &ssa_expr);
+  void operator()(ssa_exprt &ssa_expr) const;
 
   /// Insert the content of \p other into this renaming
   void restore_from(const current_namest &other);

src/goto-symex/symex_dead.cpp

@@ -32,12 +32,9 @@ void goto_symext::symex_dead(statet &state)
   // in case of pointers, put something into the value set
   if(code.symbol().type().id() == ID_pointer)
   {
-    exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns);
-
     exprt rhs;
-
-    if(failed.is_not_nil())
-      rhs = address_of_exprt(failed, to_pointer_type(code.symbol().type()));
+    if(auto failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns))
+      rhs = address_of_exprt(*failed, to_pointer_type(code.symbol().type()));
     else
       rhs=exprt(ID_invalid);
 

src/goto-symex/symex_decl.cpp

@@ -48,13 +48,9 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   // in case of pointers, put something into the value set
   if(expr.type().id() == ID_pointer)
   {
-    exprt failed=
-      get_failed_symbol(expr, ns);
-
     exprt rhs;
-
-    if(failed.is_not_nil())
-      rhs=address_of_exprt(failed, to_pointer_type(expr.type()));
+    if(auto failed = get_failed_symbol(expr, ns))
+      rhs = address_of_exprt(*failed, to_pointer_type(expr.type()));
     else
       rhs=exprt(ID_invalid);
 

src/goto-symex/symex_start_thread.cpp

@@ -68,10 +68,11 @@ void goto_symext::symex_start_thread(statet &state)
     lhs.set_level_0(t);
 
     // set up L1 name
-    if(!state.level1.current_names.insert(
-        std::make_pair(lhs.get_l1_object_identifier(),
-                       std::make_pair(lhs, 0))).second)
-      UNREACHABLE;
+    auto emplace_result = state.level1.current_names.emplace(
+      std::piecewise_construct,
+      std::forward_as_tuple(lhs.get_l1_object_identifier()),
+      std::forward_as_tuple(lhs, 0));
+    CHECK_RETURN(emplace_result.second);
     state.rename(lhs, ns, goto_symex_statet::L1);
     const irep_idt l1_name=lhs.get_l1_object_identifier();
     // store it

src/pointer-analysis/add_failed_symbols.cpp

@@ -89,17 +89,16 @@ void add_failed_symbols(symbol_table_baset &symbol_table)
 /// Get the failed-dereference symbol for the given symbol
 /// \param expr: symbol expression to get a failed symbol for
 /// \param ns: global namespace
-/// \return symbol expression for the failed-dereference symbol, or nil_exprt
-///   if none exists.
-exprt get_failed_symbol(
-  const symbol_exprt &expr,
-  const namespacet &ns)
+/// \return symbol expression for the failed-dereference symbol, or an empty
+///   optional if none exists.
+optionalt<symbol_exprt>
+get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
 {
   const symbolt &symbol=ns.lookup(expr);
   irep_idt failed_symbol_id=symbol.type.get(ID_C_failed_symbol);
 
   if(failed_symbol_id.empty())
-    return nil_exprt();
+    return {};
 
   const symbolt &failed_symbol=ns.lookup(failed_symbol_id);
 

src/pointer-analysis/add_failed_symbols.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H
 
 #include <util/irep.h>
+#include <util/optional.h>
 
 class symbol_table_baset;
 class symbolt;
@@ -27,8 +28,7 @@ void add_failed_symbol_if_needed(
 
 irep_idt failed_symbol_id(const irep_idt &identifier);
 
-exprt get_failed_symbol(
-  const symbol_exprt &expr,
-  const namespacet &ns);
+optionalt<symbol_exprt>
+get_failed_symbol(const symbol_exprt &expr, const namespacet &ns);
 
 #endif // CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H

src/pointer-analysis/value_set.cpp

@@ -1471,12 +1471,9 @@ void value_sett::apply_code_rec(
       (lhs_type.id() == ID_array && lhs_type.subtype().id() == ID_pointer))
     {
       // assign the address of the failed object
-      exprt failed=get_failed_symbol(to_symbol_expr(lhs), ns);
-
-      if(failed.is_not_nil())
+      if(auto failed = get_failed_symbol(to_symbol_expr(lhs), ns))
       {
-        address_of_exprt address_of_expr(
-          failed, to_pointer_type(lhs.type()));
+        address_of_exprt address_of_expr(*failed, to_pointer_type(lhs.type()));
         assign(lhs, address_of_expr, ns, false, false);
       }
       else