Extract call_stackt class from goto_symex_statet [depends-on: #4294]

jbmc/src/java_bytecode/java_bmc_util.cpp

@@ -28,7 +28,7 @@ void java_setup_symex(
     //  for some reason)
     symex.add_loop_unwind_handler(
       [&goto_model](
-        const goto_symex_statet::call_stackt &context,
+        const call_stackt &context,
         unsigned loop_num,
         unsigned unwind,
         unsigned &max_unwind)

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp

@@ -24,8 +24,7 @@ Author: Chris Smowton, [email protected]
 /// \param context: the current call stack
 /// \return the name of an enclosing function that may be defined on the
 ///   relevant enum type, or an empty string if we don't find one.
-static irep_idt
-find_enum_function_on_stack(const goto_symex_statet::call_stackt &context)
+static irep_idt find_enum_function_on_stack(const call_stackt &context)
 {
   static irep_idt reference_array_clone_id =
     "java::array[reference].clone:()Ljava/lang/Object;";
@@ -64,7 +63,7 @@ find_enum_function_on_stack(const goto_symex_statet::call_stackt &context)
 ///   unwind_count is <= the enumeration size, or unknown (defer / no decision)
 ///   otherwise.
 tvt java_enum_static_init_unwind_handler(
-  const goto_symex_statet::call_stackt &context,
+  const call_stackt &context,
   unsigned loop_number,
   unsigned unwind_count,
   unsigned &unwind_max,

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h

@@ -18,7 +18,7 @@ Author: Chris Smowton, [email protected]
 #include <util/threeval.h>
 
 tvt java_enum_static_init_unwind_handler(
-  const goto_symex_statet::call_stackt &context,
+  const call_stackt &context,
   unsigned loop_number,
   unsigned unwind_count,
   unsigned &unwind_max,

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -511,17 +511,17 @@ int jbmc_parse_optionst::doit()
   std::function<void(bmct &, const symbol_tablet &)> configure_bmc = nullptr;
   if(options.get_bool_option("java-unwind-enum-static"))
   {
-    configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) {
-      bmc.add_loop_unwind_handler(
-        [&symbol_table](
-          const goto_symex_statet::call_stackt &context,
-          unsigned loop_number,
-          unsigned unwind,
-          unsigned &max_unwind) {
+    configure_bmc =
+      [](bmct &bmc, const symbol_tablet &symbol_table) {
+        bmc.add_loop_unwind_handler([&symbol_table](
+                                      const call_stackt &context,
+                                      unsigned loop_number,
+                                      unsigned unwind,
+                                      unsigned &max_unwind) {
           return java_enum_static_init_unwind_handler(
             context, loop_number, unwind, max_unwind, symbol_table);
         });
-    };
+      };
   }
 
   object_factory_params.set(options);

src/goto-checker/symex_bmc.cpp

@@ -105,7 +105,7 @@ void symex_bmct::merge_goto(goto_statet &&goto_state, statet &state)
 
 bool symex_bmct::should_stop_unwind(
   const symex_targett::sourcet &source,
-  const goto_symex_statet::call_stackt &context,
+  const call_stackt &context,
   unsigned unwind)
 {
   const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc);

src/goto-checker/symex_bmc.h

@@ -42,7 +42,7 @@ class symex_bmct : public goto_symext
   /// enforced. They return true to halt unwinding, false to authorise
   /// unwinding, or Unknown to indicate they have no opinion.
   typedef std::function<
-    tvt(const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)>
+    tvt(const call_stackt &, unsigned, unsigned, unsigned &)>
     loop_unwind_handlert;
 
   /// Recursion unwind handlers take the function ID, the unwind count so far,
@@ -98,7 +98,7 @@ class symex_bmct : public goto_symext
 
   bool should_stop_unwind(
     const symex_targett::sourcet &source,
-    const goto_symex_statet::call_stackt &context,
+    const call_stackt &context,
     unsigned unwind) override;
 
   bool get_unwind_recursion(

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/call_stack.h

@@ -0,0 +1,47 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_SYMEX_CALL_STACK_H
+#define CPROVER_GOTO_SYMEX_CALL_STACK_H
+
+#include "frame.h"
+
+class call_stackt : public std::vector<framet>
+{
+public:
+  framet &top()
+  {
+    PRECONDITION(!empty());
+    return back();
+  }
+
+  const framet &top() const
+  {
+    PRECONDITION(!empty());
+    return back();
+  }
+
+  framet &new_frame(symex_targett::sourcet calling_location)
+  {
+    emplace_back(calling_location);
+    return back();
+  }
+
+  void pop()
+  {
+    PRECONDITION(!empty());
+    pop_back();
+  }
+
+  const framet &previous_frame()
+  {
+    return *(--(--end()));
+  }
+};
+
+#endif // CPROVER_GOTO_SYMEX_CALL_STACK_H

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.h

@@ -345,7 +345,7 @@ class goto_symext
   /// \return true indicates abort, with false we continue
   virtual bool should_stop_unwind(
     const symex_targett::sourcet &source,
-    const goto_symex_statet::call_stackt &context,
+    const call_stackt &context,
     unsigned unwind);
 
   virtual void loop_bound_exceeded(statet &state, const exprt &guard);

src/goto-symex/goto_symex_state.cpp

@@ -33,7 +33,7 @@ goto_symex_statet::goto_symex_statet(const symex_targett::sourcet &_source)
   : goto_statet(_source), symex_target(nullptr), record_events(true), dirty()
 {
   threads.resize(1);
-  new_frame();
+  call_stack().new_frame(source);
 }
 
 goto_symex_statet::~goto_symex_statet()=default;
@@ -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";
-  }
-}