Merge pull request #3445 from romainbrenguier/refactor/symex-part4

Goto symex state clean-up

Author: romainbrenguier

src/goto-symex/goto_symex_state.cpp

@@ -407,23 +407,20 @@ bool goto_symex_statet::l2_thread_read_encoding(
     guardt write_guard;
     write_guard.add(false_exprt());
 
-    written_in_atomic_sectiont::const_iterator a_s_writes=
-      written_in_atomic_section.find(ssa_l1);
+    const auto a_s_writes = written_in_atomic_section.find(ssa_l1);
     if(a_s_writes!=written_in_atomic_section.end())
     {
-      for(a_s_w_entryt::const_iterator it=a_s_writes->second.begin();
-          it!=a_s_writes->second.end();
-          ++it)
+      for(const auto &guard_in_list : a_s_writes->second)
       {
-        guardt g=*it;
+        guardt g = guard_in_list;
         g-=guard;
         if(g.is_true())
           // there has already been a write to l1_identifier within
           // this atomic section under the same guard, or a guard
           // that implies the current one
           return false;
 
-        write_guard|=*it;
+        write_guard |= guard_in_list;
       }
     }
 

src/goto-symex/goto_symex_state.h

@@ -173,47 +173,31 @@ class goto_symex_statet final
 
   // stack frames -- these are used for function calls and
   // for exceptions
-  class framet
+  struct framet
   {
-  public:
     // function calls
     irep_idt function_identifier;
     goto_state_mapt goto_state_map;
     symex_targett::sourcet calling_location;
 
     goto_programt::const_targett end_of_function;
-    exprt return_value;
-    bool hidden_function;
+    exprt return_value = nil_exprt();
+    bool hidden_function = false;
 
     symex_renaming_levelt::current_namest old_level1;
 
-    typedef std::set<irep_idt> local_objectst;
-    local_objectst local_objects;
-
-    framet():
-      return_value(nil_exprt()),
-      hidden_function(false)
-    {
-    }
+    std::set<irep_idt> local_objects;
 
     // exceptions
-    typedef std::map<irep_idt, goto_programt::targett> catch_mapt;
-    catch_mapt catch_map;
+    std::map<irep_idt, goto_programt::targett> catch_map;
 
     // loop and recursion unwinding
     struct loop_infot
     {
-      loop_infot():
-        count(0),
-        is_recursion(false)
-      {
-      }
-
-      unsigned count;
-      bool is_recursion;
+      unsigned count = 0;
+      bool is_recursion = false;
     };
-    typedef std::unordered_map<irep_idt, loop_infot> loop_iterationst;
-    loop_iterationst loop_iterations;
+    std::unordered_map<irep_idt, loop_infot> loop_iterations;
   };
 
   typedef std::vector<framet> call_stackt;
@@ -249,40 +233,27 @@ class goto_symex_statet final
   // threads
   unsigned atomic_section_id;
   typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;
-  typedef std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash>
-    read_in_atomic_sectiont;
   typedef std::list<guardt> a_s_w_entryt;
-  typedef std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
-    written_in_atomic_sectiont;
-  read_in_atomic_sectiont read_in_atomic_section;
-  written_in_atomic_sectiont written_in_atomic_section;
+  std::unordered_map<ssa_exprt, a_s_r_entryt, irep_hash> read_in_atomic_section;
+  std::unordered_map<ssa_exprt, a_s_w_entryt, irep_hash>
+    written_in_atomic_section;
 
   unsigned total_vccs, remaining_vccs;
 
-  class threadt
+  struct threadt
   {
-  public:
     goto_programt::const_targett pc;
     guardt guard;
     call_stackt call_stack;
     std::map<irep_idt, unsigned> function_frame;
-    unsigned atomic_section_id;
-
-    threadt():
-      atomic_section_id(0)
-    {
-    }
+    unsigned atomic_section_id = 0;
   };
 
-  typedef std::vector<threadt> threadst;
-  threadst threads;
+  std::vector<threadt> threads;
 
   bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
   bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
 
-  void populate_dirty_for_function(
-    const irep_idt &id, const goto_functiont &);
-
   bool record_events;
   incremental_dirtyt dirty;
 
@@ -294,7 +265,6 @@ class goto_symex_statet final
   /// \brief This state is saved, with the PC pointing to the next instruction
   /// of a GOTO
   bool has_saved_next_instruction;
-  bool saved_target_is_backwards;
 
 private:
   /// \brief Dangerous, do not use

src/goto-symex/symex_atomic_section.cpp

@@ -45,20 +45,16 @@ void goto_symext::symex_atomic_end(statet &state)
   const unsigned atomic_section_id=state.atomic_section_id;
   state.atomic_section_id=0;
 
-  for(goto_symex_statet::read_in_atomic_sectiont::const_iterator
-      r_it=state.read_in_atomic_section.begin();
-      r_it!=state.read_in_atomic_section.end();
-      ++r_it)
+  for(const auto &pair : state.read_in_atomic_section)
   {
-    ssa_exprt r=r_it->first;
-    r.set_level_2(r_it->second.first);
+    ssa_exprt r = pair.first;
+    r.set_level_2(pair.second.first);
 
     // guard is the disjunction over reads
-    PRECONDITION(!r_it->second.second.empty());
-    guardt read_guard(r_it->second.second.front());
-    for(std::list<guardt>::const_iterator
-        it=++(r_it->second.second.begin());
-        it!=r_it->second.second.end();
+    PRECONDITION(!pair.second.second.empty());
+    guardt read_guard(pair.second.second.front());
+    for(std::list<guardt>::const_iterator it = ++(pair.second.second.begin());
+        it != pair.second.second.end();
         ++it)
       read_guard|=*it;
     exprt read_guard_expr=read_guard.as_expr();
@@ -71,20 +67,16 @@ void goto_symext::symex_atomic_end(statet &state)
       state.source);
   }
 
-  for(goto_symex_statet::written_in_atomic_sectiont::const_iterator
-      w_it=state.written_in_atomic_section.begin();
-      w_it!=state.written_in_atomic_section.end();
-      ++w_it)
+  for(const auto &pair : state.written_in_atomic_section)
   {
-    ssa_exprt w=w_it->first;
+    ssa_exprt w = pair.first;
     w.set_level_2(state.level2.current_count(w.get_identifier()));
 
     // guard is the disjunction over writes
-    PRECONDITION(!w_it->second.empty());
-    guardt write_guard(w_it->second.front());
-    for(std::list<guardt>::const_iterator
-        it=++(w_it->second.begin());
-        it!=w_it->second.end();
+    PRECONDITION(!pair.second.empty());
+    guardt write_guard(pair.second.front());
+    for(std::list<guardt>::const_iterator it = ++(pair.second.begin());
+        it != pair.second.end();
         ++it)
       write_guard|=*it;
     exprt write_guard_expr=write_guard.as_expr();

src/goto-symex/symex_function_call.cpp

@@ -298,12 +298,11 @@ void goto_symext::symex_function_call_code(
   frame.hidden_function=goto_function.is_hidden();
 
   const goto_symex_statet::framet &p_frame=state.previous_frame();
-  for(goto_symex_statet::framet::loop_iterationst::const_iterator
-      it=p_frame.loop_iterations.begin();
-      it!=p_frame.loop_iterations.end();
-      ++it)
-    if(it->second.is_recursion)
-      frame.loop_iterations.insert(*it);
+  for(const auto &pair : p_frame.loop_iterations)
+  {
+    if(pair.second.is_recursion)
+      frame.loop_iterations.insert(pair);
+  }
 
   // increase unwinding counter
   frame.loop_iterations[identifier].is_recursion=true;

src/goto-symex/symex_goto.cpp

@@ -184,15 +184,13 @@ void goto_symext::symex_goto(statet &state)
     path_storaget::patht next_instruction(target, state);
     next_instruction.state.saved_target = state_pc;
     next_instruction.state.has_saved_next_instruction = true;
-    next_instruction.state.saved_target_is_backwards = backward;
 
     path_storaget::patht jump_target(target, state);
     jump_target.state.saved_target = new_state_pc;
     jump_target.state.has_saved_jump_target = true;
     // `forward` tells us where the branch we're _currently_ executing is
     // pointing to; this needs to be inverted for the branch that we're saving,
     // so let its truth value for `backwards` be the same as ours for `forward`.
-    jump_target.state.saved_target_is_backwards = !backward;
 
     log.debug() << "Saving next instruction '"
                 << next_instruction.state.saved_target->source_location << "'"