Split l2_thread_write_encoding apart from write_is_shared

l2_thread_write_encoding both makes a quite complicated test regarding whether a write is to be
considered shared state, and also enacts some side-effects for both shared and non-shared state.
This splits part of its testing into write_is_shared.

No behavioural change.

Author: smowton

src/goto-symex/goto_symex_state.cpp

@@ -472,32 +472,47 @@ void goto_symex_statet::increase_generation_if_exists(const irep_idt identifier)
   current_names_iter->second.second = fresh_l2_name_provider(identifier);
 }
 
-/// thread encoding
-bool goto_symex_statet::l2_thread_write_encoding(
+goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared(
   const ssa_exprt &expr,
-  const namespacet &ns)
+  const namespacet &ns) const
 {
   if(!record_events)
-    return false;
+    return write_is_shared_resultt::NOT_SHARED;
 
-  // is it a shared object?
-  const irep_idt &obj_identifier=expr.get_object_name();
+  const irep_idt &obj_identifier = expr.get_object_name();
   if(
     obj_identifier == guard_identifier() ||
     (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier)))
   {
-    return false; // not shared
+    return write_is_shared_resultt::NOT_SHARED;
   }
 
-  // see whether we are within an atomic section
-  if(atomic_section_id!=0)
+  if(atomic_section_id != 0)
+    return write_is_shared_resultt::IN_ATOMIC_SECTION;
+
+  return write_is_shared_resultt::SHARED;
+}
+
+/// thread encoding
+bool goto_symex_statet::l2_thread_write_encoding(
+  const ssa_exprt &expr,
+  const namespacet &ns)
+{
+  switch(write_is_shared(expr, ns))
+  {
+  case write_is_shared_resultt::NOT_SHARED:
+    return false;
+  case write_is_shared_resultt::IN_ATOMIC_SECTION:
   {
-    ssa_exprt ssa_l1=expr;
+    ssa_exprt ssa_l1 = expr;
     ssa_l1.remove_level_2();
 
     written_in_atomic_section[ssa_l1].push_back(guard);
     return false;
   }
+  case write_is_shared_resultt::SHARED:
+    break;
+  }
 
   // record a shared write
   symex_target->shared_write(
@@ -507,7 +522,7 @@ bool goto_symex_statet::l2_thread_write_encoding(
     source);
 
   // do we have threads?
-  return threads.size()>1;
+  return threads.size() > 1;
 }
 
 template <levelt level>

src/goto-symex/goto_symex_state.h

@@ -181,8 +181,17 @@ class goto_symex_statet final : public goto_statet
 
   std::vector<threadt> threads;
 
+  enum class write_is_shared_resultt
+  {
+    NOT_SHARED,
+    IN_ATOMIC_SECTION,
+    SHARED
+  };
+
   bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
   bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
+  write_is_shared_resultt
+  write_is_shared(const ssa_exprt &expr, const namespacet &ns) const;
 
   bool record_events;