Merge pull request #396 from smowton/fix_ssa_l1_ids

Keep SSA L1 IDs as an attribute

Author: Daniel Kroening

src/util/irep_ids.txt

@@ -693,6 +693,7 @@ C_full_identifier #full_identifier
 L0
 L1
 L2
+L1_object_identifier
 already_typechecked
 C_va_arg_type #va_arg_type
 smt2_symbol

src/util/ssa_expr.cpp

@@ -30,21 +30,22 @@ static void build_ssa_identifier_rec(
   const irep_idt &l0,
   const irep_idt &l1,
   const irep_idt &l2,
-  std::ostream &os)
+  std::ostream &os,
+  std::ostream &l1_object_os)
 {
   if(expr.id()==ID_member)
   {
     const member_exprt &member=to_member_expr(expr);
 
-    build_ssa_identifier_rec(member.struct_op(), l0, l1, l2, os);
+    build_ssa_identifier_rec(member.struct_op(), l0, l1, l2, os, l1_object_os);
 
     os << '.' << member.get_component_name();
   }
   else if(expr.id()==ID_index)
   {
     const index_exprt &index=to_index_expr(expr);
 
-    build_ssa_identifier_rec(index.array(), l0, l1, l2, os);
+    build_ssa_identifier_rec(index.array(), l0, l1, l2, os, l1_object_os);
 
     mp_integer idx;
     if(to_integer(to_constant_expr(index.index()), idx))
@@ -54,13 +55,21 @@ static void build_ssa_identifier_rec(
   }
   else if(expr.id()==ID_symbol)
   {
-    os << to_symbol_expr(expr).get_identifier();
+    auto symid=to_symbol_expr(expr).get_identifier();
+    os << symid;
+    l1_object_os << symid;
 
     if(!l0.empty())
+    {
       os << '!' << l0;
+      l1_object_os << '!' << l0;
+    }
 
     if(!l1.empty())
+    {
       os << '@' << l1;
+      l1_object_os << '@' << l1;
+    }
 
     if(!l2.empty())
       os << '#' << l2;
@@ -81,15 +90,16 @@ Function: ssa_exprt::build_identifier
 
 \*******************************************************************/
 
-irep_idt ssa_exprt::build_identifier(
+std::pair<irep_idt, irep_idt> ssa_exprt::build_identifier(
   const exprt &expr,
   const irep_idt &l0,
   const irep_idt &l1,
   const irep_idt &l2)
 {
   std::ostringstream oss;
+  std::ostringstream l1_object_oss;
 
-  build_ssa_identifier_rec(expr, l0, l1, l2, oss);
+  build_ssa_identifier_rec(expr, l0, l1, l2, oss, l1_object_oss);
 
-  return oss.str();
+  return std::make_pair(irep_idt(oss.str()), irep_idt(l1_object_oss.str()));
 }

src/util/ssa_expr.h

@@ -67,15 +67,9 @@ class ssa_exprt:public symbol_exprt
     #if 0
     return get_l1_object().get_identifier();
     #else
-    // the above is the clean version, this is the fast one, making
-    // use of internal knowledge about identifier names
-    std::string l1_o_id=id2string(get_identifier());
-    std::string::size_type fs_suffix=l1_o_id.find_first_of(".[#");
-
-    if(fs_suffix!=std::string::npos)
-      l1_o_id.resize(fs_suffix);
-
-    return l1_o_id;
+    // the above is the clean version, this is the fast one, using
+    // an identifier cached during build_identifier
+    return get(ID_L1_object_identifier);
     #endif
   }
 
@@ -130,10 +124,12 @@ class ssa_exprt:public symbol_exprt
     const irep_idt &l1=get_level_1();
     const irep_idt &l2=get_level_2();
 
-    set_identifier(build_identifier(get_original_expr(), l0, l1, l2));
+    auto idpair=build_identifier(get_original_expr(), l0, l1, l2);
+    set_identifier(idpair.first);
+    set(ID_L1_object_identifier, idpair.second);
   }
 
-  static irep_idt build_identifier(
+  static std::pair<irep_idt, irep_idt> build_identifier(
     const exprt &src,
     const irep_idt &l0,
     const irep_idt &l1,