Merge pull request #4017 from tautschnig/single-guard

Store goto_symex::\guard in a single place [blocks: #3619]

Author: tautschnig

src/goto-symex/auto_objects.cpp

@@ -87,7 +87,7 @@ void goto_symext::trigger_auto_object(
     const ssa_exprt &ssa_expr=to_ssa_expr(expr);
     const irep_idt &obj_identifier=ssa_expr.get_object_name();
 
-    if(obj_identifier!="goto_symex::\\guard")
+    if(obj_identifier != statet::guard_identifier())
     {
       const symbolt &symbol=
         ns.lookup(obj_identifier);

src/goto-symex/goto_symex.h

@@ -84,7 +84,6 @@ class goto_symext
       target(_target),
       atomic_section_counter(0),
       log(mh),
-      guard_identifier("goto_symex::\\guard"),
       path_storage(path_storage),
       path_segment_vccs(0),
       _total_vccs(std::numeric_limits<unsigned>::max()),
@@ -238,10 +237,6 @@ class goto_symext
     guardt &,
     bool keep_array);
 
-  // guards
-
-  const irep_idt guard_identifier;
-
   virtual void symex_goto(statet &);
   virtual void symex_start_thread(statet &);
   virtual void symex_atomic_begin(statet &);

src/goto-symex/goto_symex_state.cpp

@@ -180,7 +180,7 @@ void goto_symex_statet::assignment(
 
 #if 0
   PRECONDITION(l1_identifier != get_original_name(l1_identifier)
-      || l1_identifier=="goto_symex::\\guard"
+      || 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"));
@@ -372,9 +372,11 @@ bool goto_symex_statet::l2_thread_read_encoding(
   // is it a shared object?
   const irep_idt &obj_identifier=expr.get_object_name();
   if(
-    obj_identifier == "goto_symex::\\guard" ||
+    obj_identifier == guard_identifier() ||
     (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
+  {
     return false;
+  }
 
   ssa_exprt ssa_l1=expr;
   ssa_l1.remove_level_2();
@@ -508,9 +510,11 @@ bool goto_symex_statet::l2_thread_write_encoding(
   // is it a shared object?
   const irep_idt &obj_identifier=expr.get_object_name();
   if(
-    obj_identifier == "goto_symex::\\guard" ||
+    obj_identifier == guard_identifier() ||
     (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
+  {
     return false; // not shared
+  }
 
   // see whether we are within an atomic section
   if(atomic_section_id!=0)

src/goto-symex/goto_symex_state.h

@@ -220,6 +220,13 @@ class goto_symex_statet final
   typedef std::map<goto_programt::const_targett, goto_state_listt>
     goto_state_mapt;
 
+  // guards
+  static irep_idt guard_identifier()
+  {
+    static irep_idt id = "goto_symex::\\guard";
+    return id;
+  }
+
   // stack frames -- these are used for function calls and
   // for exceptions
   struct framet

src/goto-symex/renaming_level.cpp

@@ -15,6 +15,8 @@ Author: Romain Brenguier, [email protected]
 #include <util/ssa_expr.h>
 #include <util/symbol.h>
 
+#include "goto_symex_state.h"
+
 void symex_level0t::
 operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
 {
@@ -25,7 +27,7 @@ operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
   const irep_idt &obj_identifier = ssa_expr.get_object_name();
 
   // guards are not L0-renamed
-  if(obj_identifier == "goto_symex::\\guard")
+  if(obj_identifier == goto_symex_statet::guard_identifier())
     return;
 
   const symbolt *s;

src/goto-symex/symex_goto.cpp

@@ -243,8 +243,8 @@ void goto_symext::symex_goto(statet &state)
     }
     else
     {
-      symbol_exprt guard_symbol_expr=
-        symbol_exprt(guard_identifier, bool_typet());
+      symbol_exprt guard_symbol_expr =
+        symbol_exprt(statet::guard_identifier(), bool_typet());
       exprt new_rhs = boolean_negate(new_guard);
 
       ssa_exprt new_lhs(guard_symbol_expr);
@@ -394,7 +394,6 @@ static void for_each2(
 /// \param [in, out] dest_state: second state
 /// \param ns: namespace
 /// \param diff_guard: difference between the guards of the two states
-/// \param guard_identifier: prefix used for goto symex guards
 /// \param [out] log: logger for debug messages
 /// \param do_simplify: should the right-hand-side of the assignment that is
 ///   added to the target be simplified
@@ -408,7 +407,6 @@ static void merge_names(
   goto_symext::statet &dest_state,
   const namespacet &ns,
   const guardt &diff_guard,
-  const irep_idt &guard_identifier,
   messaget &log,
   const bool do_simplify,
   symex_target_equationt &target,
@@ -419,7 +417,7 @@ static void merge_names(
   const irep_idt l1_identifier = ssa.get_identifier();
   const irep_idt &obj_identifier = ssa.get_object_name();
 
-  if(obj_identifier == guard_identifier)
+  if(obj_identifier == goto_symext::statet::guard_identifier())
     return; // just a guard, don't bother
 
   if(goto_count == dest_count)
@@ -544,7 +542,6 @@ void goto_symext::phi_function(
         dest_state,
         ns,
         diff_guard,
-        guard_identifier,
         log,
         symex_config.simplify_opt,
         target,