Merge pull request #4294 from romainbrenguier/refactor/goto_state

Move goto_statet and framet to their own files [blocks: #4302]

Author: tautschnig

src/goto-symex/Makefile

@@ -1,5 +1,6 @@
 SRC = auto_objects.cpp \
       build_goto_trace.cpp \
+      goto_state.cpp \
       goto_symex.cpp \
       goto_symex_state.cpp \
       memory_model.cpp \

src/goto-symex/frame.h

@@ -0,0 +1,54 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Class for stack frames
+
+#ifndef CPROVER_GOTO_SYMEX_FRAME_H
+#define CPROVER_GOTO_SYMEX_FRAME_H
+
+#include "goto_state.h"
+
+/// Stack frames -- these are used for function calls and for exceptions
+struct framet
+{
+  // gotos
+  using goto_state_listt = std::list<goto_statet>;
+
+  // function calls
+  irep_idt function_identifier;
+  std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
+  symex_targett::sourcet calling_location;
+
+  goto_programt::const_targett end_of_function;
+  exprt return_value = nil_exprt();
+  bool hidden_function = false;
+
+  symex_renaming_levelt::current_namest old_level1;
+
+  std::set<irep_idt> local_objects;
+
+  // exceptions
+  std::map<irep_idt, goto_programt::targett> catch_map;
+
+  // loop and recursion unwinding
+  struct loop_infot
+  {
+    unsigned count = 0;
+    bool is_recursion = false;
+  };
+
+  std::unordered_map<irep_idt, loop_infot> loop_iterations;
+
+  explicit framet(symex_targett::sourcet _calling_location)
+    : calling_location(std::move(_calling_location))
+  {
+  }
+};
+
+#endif // CPROVER_GOTO_SYMEX_FRAME_H

src/goto-symex/goto_state.cpp

@@ -0,0 +1,22 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#include "goto_state.h"
+
+#include <util/format_expr.h>
+
+/// Print the constant propagation map in a human-friendly format.
+/// This is primarily for use from the debugger; please don't delete me just
+/// because there aren't any current callers.
+void goto_statet::output_propagation_map(std::ostream &out)
+{
+  for(const auto &name_value : propagation)
+  {
+    out << name_value.first << " <- " << format(name_value.second) << "\n";
+  }
+}

src/goto-symex/goto_state.h

@@ -0,0 +1,70 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// goto_statet class definition
+
+#ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
+#define CPROVER_GOTO_SYMEX_GOTO_STATE_H
+
+#include <analyses/local_safe_pointers.h>
+#include <pointer-analysis/value_set.h>
+#include <util/guard.h>
+
+#include "renaming_level.h"
+#include "symex_target_equation.h"
+
+/// Container for data that varies per program point, e.g. the constant
+/// propagator state, when state needs to branch. This is copied out of
+/// goto_symex_statet at a control-flow fork and then back into it at a
+/// control-flow merge.
+class goto_statet
+{
+public:
+  /// Distance from entry
+  unsigned depth = 0;
+
+  symex_level2t level2;
+
+  /// Uses level 1 names, and is used to do dereferencing
+  value_sett value_set;
+
+  // A guard is a particular condition that has to pass for an instruction
+  // to be executed. The easiest example is an if/else: each instruction along
+  // the if branch will be guarded by the condition of the if (and if there
+  // is an else branch then instructions on it will be guarded by the negation
+  // of the condition of the if).
+  guardt guard{true_exprt{}};
+
+  symex_targett::sourcet source;
+
+  // Map L1 names to (L2) constants. Values will be evicted from this map
+  // when they become non-constant. This is used to propagate values that have
+  // been worked out to only have one possible value.
+  //
+  // "constants" can include symbols, but only in the context of an address-of
+  // op (i.e. &x can be propagated), and an address-taken thing should only be
+  // L1.
+  std::map<irep_idt, exprt> propagation;
+
+  void output_propagation_map(std::ostream &);
+
+  /// Threads
+  unsigned atomic_section_id = 0;
+
+  unsigned total_vccs = 0;
+  unsigned remaining_vccs = 0;
+
+  /// Constructors
+  explicit goto_statet(const class goto_symex_statet &s);
+  explicit goto_statet(const symex_targett::sourcet &_source) : source(_source)
+  {
+  }
+};
+
+#endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H

src/goto-symex/goto_symex_state.cpp

@@ -785,14 +785,3 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
         << frame.calling_location.pc->location_number << "\n";
   }
 }
-
-/// Print the constant propagation map in a human-friendly format.
-/// This is primarily for use from the debugger; please don't delete me just
-/// because there aren't any current callers.
-void goto_statet::output_propagation_map(std::ostream &out)
-{
-  for(const auto &name_value : propagation)
-  {
-    out << name_value.first << " <- " << format(name_value.second) << "\n";
-  }
-}

src/goto-symex/goto_symex_state.h

@@ -22,98 +22,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/ssa_expr.h>
 #include <util/make_unique.h>
-
-#include <pointer-analysis/value_set.h>
 #include <goto-programs/goto_function.h>
 
+#include "frame.h"
+#include "goto_state.h"
 #include "renaming_level.h"
 #include "symex_target_equation.h"
 
-/// Container for data that varies per program point, e.g. the constant
-/// propagator state, when state needs to branch. This is copied out of
-/// goto_symex_statet at a control-flow fork and then back into it at a
-/// control-flow merge.
-class goto_statet
-{
-public:
-  /// Distance from entry
-  unsigned depth = 0;
-
-  symex_level2t level2;
-
-  /// Uses level 1 names, and is used to do dereferencing
-  value_sett value_set;
-
-  // A guard is a particular condition that has to pass for an instruction
-  // to be executed. The easiest example is an if/else: each instruction along
-  // the if branch will be guarded by the condition of the if (and if there
-  // is an else branch then instructions on it will be guarded by the negation
-  // of the condition of the if).
-  guardt guard{true_exprt{}};
-
-  symex_targett::sourcet source;
-
-  // Map L1 names to (L2) constants. Values will be evicted from this map
-  // when they become non-constant. This is used to propagate values that have
-  // been worked out to only have one possible value.
-  //
-  // "constants" can include symbols, but only in the context of an address-of
-  // op (i.e. &x can be propagated), and an address-taken thing should only be
-  // L1.
-  std::map<irep_idt, exprt> propagation;
-
-  void output_propagation_map(std::ostream &);
-
-  /// Threads
-  unsigned atomic_section_id = 0;
-
-  unsigned total_vccs = 0;
-  unsigned remaining_vccs = 0;
-
-  /// Constructors
-  explicit goto_statet(const class goto_symex_statet &s);
-  explicit goto_statet(const symex_targett::sourcet &_source) : source(_source)
-  {
-  }
-};
-
-// stack frames -- these are used for function calls and
-// for exceptions
-struct framet
-{
-  // gotos
-  using goto_state_listt = std::list<goto_statet>;
-
-  // function calls
-  irep_idt function_identifier;
-  std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
-  symex_targett::sourcet calling_location;
-
-  goto_programt::const_targett end_of_function;
-  exprt return_value = nil_exprt();
-  bool hidden_function = false;
-
-  symex_renaming_levelt::current_namest old_level1;
-
-  std::set<irep_idt> local_objects;
-
-  // exceptions
-  std::map<irep_idt, goto_programt::targett> catch_map;
-
-  // loop and recursion unwinding
-  struct loop_infot
-  {
-    unsigned count = 0;
-    bool is_recursion = false;
-  };
-  std::unordered_map<irep_idt, loop_infot> loop_iterations;
-
-  explicit framet(symex_targett::sourcet _calling_location)
-    : calling_location(std::move(_calling_location))
-  {
-  }
-};
-
 /// \brief Central data structure: state.
 ///
 /// The state is a persistent data structure that symex maintains as it