Adding/extending support for ssa_exprt

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6377 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/goto-programs/graphml_goto_trace.cpp

@@ -12,8 +12,7 @@ Author: Daniel Kroening
 #include <util/i2string.h>
 #include <util/arith_tools.h>
 #include <util/prefix.h>
-
-#include <goto-symex/ssa_expr.h>
+#include <util/ssa_expr.h>
 
 #include "graphml_goto_trace.h"
 

src/goto-symex/Makefile

@@ -4,7 +4,7 @@ SRC = symex_target.cpp symex_target_equation.cpp goto_symex.cpp \
       symex_goto.cpp symex_builtin_functions.cpp slice.cpp symex_other.cpp \
       slice_by_trace.cpp symex_decl.cpp symex_dead.cpp rewrite_union.cpp \
       precondition.cpp postcondition.cpp symex_clean_expr.cpp \
-      symex_dereference_state.cpp auto_objects.cpp ssa_expr.cpp \
+      symex_dereference_state.cpp auto_objects.cpp \
       symex_catch.cpp symex_start_thread.cpp symex_assign.cpp \
       symex_throw.cpp symex_atomic_section.cpp memory_model.cpp \
       memory_model_sc.cpp partial_order_concurrency.cpp \

src/pointer-analysis/value_set_dereference.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/options.h>
 #include <util/pointer_predicates.h>
 #include <util/byte_operators.h>
+#include <util/ssa_expr.h>
 
 #include <ansi-c/c_types.h>
 #include <ansi-c/c_typecast.h>
@@ -651,6 +652,8 @@ void value_set_dereferencet::valid_check(
   else if(symbol_expr.id()==ID_symbol)
   {
     const irep_idt identifier=
+      is_ssa_expr(symbol_expr)?
+      to_ssa_expr(symbol_expr).get_object_name():
       to_symbol_expr(symbol_expr).get_identifier();
 
     const symbolt &symbol=ns.lookup(identifier);

src/util/Makefile

@@ -21,7 +21,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \
       bv_arithmetic.cpp tempdir.cpp tempfile.cpp timer.cpp unicode.cpp \
       irep_ids.cpp byte_operators.cpp string2int.cpp file_util.cpp \
       memory_info.cpp pipe_stream.cpp irep_hash.cpp endianness_map.cpp \
-      vtable.cpp 
+      vtable.cpp ssa_expr.cpp
 
 INCLUDES= -I ..
 

src/util/array_name.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 #include "expr.h"
 #include "namespace.h"
 #include "symbol.h"
+#include "ssa_expr.h"
 
 /*******************************************************************\
 
@@ -34,6 +35,12 @@ std::string array_name(
 
     return array_name(ns, expr.op0())+"[]";
   }
+  else if(is_ssa_expr(expr))
+  {
+    const symbolt &symbol=
+      ns.lookup(to_ssa_expr(expr).get_object_name());
+    return "array `"+id2string(symbol.base_name)+"'";
+  }
   else if(expr.id()==ID_symbol)
   {
     const symbolt &symbol=ns.lookup(expr);

src/util/pointer_offset_size.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include "simplify_expr.h"
 #include "namespace.h"
 #include "symbol.h"
+#include "ssa_expr.h"
 
 #include "pointer_offset_size.h"
 
@@ -499,7 +500,13 @@ mp_integer compute_pointer_offset(
   const namespacet &ns)
 {
   if(expr.id()==ID_symbol)
-    return 0;
+  {
+    if(is_ssa_expr(expr))
+      return compute_pointer_offset(
+        to_ssa_expr(expr).get_original_expr(), ns);
+    else
+      return 0;
+  }
   else if(expr.id()==ID_index)
   {
     assert(expr.operands().size()==2);

src/goto-symex/ssa_expr.cpp renamed to src/util/ssa_expr.cpp

@@ -44,13 +44,34 @@ class ssa_exprt:public symbol_exprt
     return to_symbol_expr(ode.root_object()).get_identifier();
   }
 
+  inline const ssa_exprt get_l1_object() const
+  {
+    object_descriptor_exprt ode;
+    ode.object()=get_original_expr();
+
+    ssa_exprt root(ode.root_object());
+    root.set(ID_L0, get(ID_L0));
+    root.set(ID_L1, get(ID_L1));
+    root.update_identifier();
+
+    return root;
+  }
+
   inline const irep_idt get_l1_object_identifier() const
   {
-    return build_identifier(
-             get_original_expr(),
-             get_level_0(),
-             get_level_1(),
-             irep_idt()); // intentionally blank
+    #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;
+    #endif
   }
 
   inline const irep_idt get_original_name() const