Merge pull request #3481 from thk123/refactor/remove-symex-magic-string

Don't use symex_dynamic:: magic string in multiple places

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/lispirep.h>
 #include <util/namespace.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/string_constant.h>
 #include <util/suffix.h>
@@ -1653,7 +1654,7 @@ std::string expr2ct::convert_symbol(
     dest=id2string(entry->second);
 
     #if 0
-    if(has_prefix(id2string(id), "symex_dynamic::dynamic_object"))
+    if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
     {
       if(sizeof_nesting++ == 0)
         dest+=" /*"+convert(src.type());

src/goto-instrument/race_check.cpp

@@ -18,6 +18,7 @@ Date: February 2006
 #include <goto-programs/remove_skip.h>
 
 #include <linking/static_lifetime_init.h>
+#include <util/pointer_predicates.h>
 
 #include "rw_set.h"
 
@@ -123,14 +124,13 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
 {
   const irep_idt &identifier=symbol_expr.get_identifier();
 
-  if(identifier==CPROVER_PREFIX "alloc" ||
-     identifier==CPROVER_PREFIX "alloc_size" ||
-     identifier=="stdin" ||
-     identifier=="stdout" ||
-     identifier=="stderr" ||
-     identifier=="sys_nerr" ||
-     has_prefix(id2string(identifier), "symex::invalid_object") ||
-     has_prefix(id2string(identifier), "symex_dynamic::dynamic_object"))
+  if(
+    identifier == CPROVER_PREFIX "alloc" ||
+    identifier == CPROVER_PREFIX "alloc_size" || identifier == "stdin" ||
+    identifier == "stdout" || identifier == "stderr" ||
+    identifier == "sys_nerr" ||
+    has_prefix(id2string(identifier), "symex::invalid_object") ||
+    has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
     return false; // no race check
 
   const symbolt &symbol=ns.lookup(identifier);

src/goto-symex/goto_symex_state.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/format.h>
 #include <util/format_expr.h>
 #include <util/invariant.h>
+#include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
 
@@ -178,7 +179,7 @@ void goto_symex_statet::assignment(
       || l1_identifier == guard_identifier()
       || ns.lookup(l1_identifier).is_shared()
       || has_prefix(id2string(l1_identifier), "symex::invalid_object")
-      || has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
+      || has_prefix(id2string(l1_identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object"));
 #endif
 
   // do the l2 renaming

src/goto-symex/symex_builtin_functions.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant_utils.h>
 #include <util/optional.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/string2int.h>
@@ -135,7 +136,8 @@ void goto_symext::symex_allocate(
 
       size_symbol.base_name=
         "dynamic_object_size"+std::to_string(dynamic_counter);
-      size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
+      size_symbol.name =
+        SYMEX_DYNAMIC_PREFIX + id2string(size_symbol.base_name);
       size_symbol.type=tmp_size.type();
       size_symbol.mode = mode;
       size_symbol.type.set(ID_C_constant, true);
@@ -154,7 +156,7 @@ void goto_symext::symex_allocate(
   symbolt value_symbol;
 
   value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
-  value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
+  value_symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(value_symbol.base_name);
   value_symbol.is_lvalue=true;
   value_symbol.type = *object_type;
   value_symbol.type.set(ID_C_dynamic, true);
@@ -405,7 +407,7 @@ void goto_symext::symex_cpp_new(
   symbol.base_name=
     do_array?"dynamic_"+count_string+"_array":
              "dynamic_"+count_string+"_value";
-  symbol.name="symex_dynamic::"+id2string(symbol.base_name);
+  symbol.name = SYMEX_DYNAMIC_PREFIX + id2string(symbol.base_name);
   symbol.is_lvalue=true;
   if(code.get(ID_statement)==ID_cpp_new_array ||
      code.get(ID_statement)==ID_cpp_new)

src/solvers/flattening/pointer_logic.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
+#include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
@@ -26,8 +27,9 @@ bool pointer_logict::is_dynamic_object(const exprt &expr) const
     return true;
 
   if(expr.id()==ID_symbol)
-    if(has_prefix(id2string(to_symbol_expr(expr).get_identifier()),
-                  "symex_dynamic::"))
+    if(has_prefix(
+         id2string(to_symbol_expr(expr).get_identifier()),
+         SYMEX_DYNAMIC_PREFIX))
       return true;
 
   return false;

src/util/pointer_predicates.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_POINTER_PREDICATES_H
 #define CPROVER_UTIL_POINTER_PREDICATES_H
 
+#define SYMEX_DYNAMIC_PREFIX "symex_dynamic::"
+
 class exprt;
 class namespacet;
 class typet;

src/util/simplify_expr_pointer.cpp

@@ -550,7 +550,7 @@ bool simplify_exprt::simplify_dynamic_object(exprt &expr)
       const irep_idt identifier=to_symbol_expr(op.op0()).get_identifier();
 
       // this is for the benefit of symex
-      expr.make_bool(has_prefix(id2string(identifier), "symex_dynamic::"));
+      expr.make_bool(has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX));
       return false;
     }
     else if(op.op0().id()==ID_string_constant)