Merge pull request #4302 from romainbrenguier/refactor/symex_call_stack2

tautschnig · web-flow · commit fc4b5cc7e82b · 2019-03-04T09:44:41.000Z
Extract call_stackt class from goto_symex_statet [depends-on: #4294]
diff --git a/jbmc/src/java_bytecode/java_bmc_util.cpp b/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)
diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp
@@ -24,8 +24,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 /// \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,
diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h
@@ -18,7 +18,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 #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,
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/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);
diff --git a/src/goto-checker/symex_bmc.cpp b/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);
diff --git a/src/goto-checker/symex_bmc.h b/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(
diff --git a/src/goto-symex/call_stack.h b/src/goto-symex/call_stack.h
@@ -0,0 +1,47 @@
+/*******************************************************************\
+
+Module: Symbolic Execution
+
+Author: Romain Brenguier, romain.brenguier@diffblue.com
+
+\*******************************************************************/
+
+#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
diff --git a/src/goto-symex/goto_symex.h b/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);
diff --git a/src/goto-symex/goto_symex_state.cpp b/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;
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/make_unique.h>
 #include <goto-programs/goto_function.h>
 
+#include "call_stack.h"
 #include "frame.h"
 #include "goto_state.h"
 #include "renaming_level.h"
@@ -126,18 +127,13 @@ class goto_symex_statet final : public goto_statet
   l1_typest l1_types;
 
 public:
-  // gotos
-  typedef std::list<goto_statet> goto_state_listt;
-
   // guards
   static irep_idt guard_identifier()
   {
     static irep_idt id = "goto_symex::\\guard";
     return id;
   }
 
-  typedef std::vector<framet> call_stackt;
-
   call_stackt &call_stack()
   {
     PRECONDITION(source.thread_nr < threads.size());
@@ -150,28 +146,6 @@ class goto_symex_statet final : public goto_statet
     return threads[source.thread_nr].call_stack;
   }
 
-  framet &top()
-  {
-    PRECONDITION(!call_stack().empty());
-    return call_stack().back();
-  }
-
-  const framet &top() const
-  {
-    PRECONDITION(!call_stack().empty());
-    return call_stack().back();
-  }
-
-  framet &new_frame()
-  {
-    call_stack().emplace_back(source);
-    return top();
-  }
-
-  void pop_frame() { call_stack().pop_back(); }
-
-  const framet &previous_frame() { return *(--(--call_stack().end())); }
-
   void print_backtrace(std::ostream &) const;
 
   // threads
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
@@ -65,7 +65,7 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code)
       assignment_type=symex_targett::assignment_typet::HIDDEN;
 
     // We hide if we are in a hidden function.
-    if(state.top().hidden_function)
+    if(state.call_stack().top().hidden_function)
       assignment_type=symex_targett::assignment_typet::HIDDEN;
 
     // We hide if we are executing a hidden instruction.
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
@@ -78,10 +78,9 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
 
   // we hide the declaration of auxiliary variables
   // and if the statement itself is hidden
-  bool hidden=
-    ns.lookup(expr.get_identifier()).is_auxiliary ||
-    state.top().hidden_function ||
-    state.source.pc->source_location.get_hide();
+  bool hidden = ns.lookup(expr.get_identifier()).is_auxiliary ||
+                state.call_stack().top().hidden_function ||
+                state.source.pc->source_location.get_hide();
 
   target.decl(
     state.guard.as_expr(),
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
@@ -124,7 +124,7 @@ void goto_symext::parameter_assignments(
       assignment_typet assignment_type;
 
       // We hide if we are in a hidden function.
-      if(state.top().hidden_function)
+      if(state.call_stack().top().hidden_function)
         assignment_type =
           symex_targett::assignment_typet::HIDDEN_ACTUAL_PARAMETER;
       else
@@ -243,10 +243,10 @@ void goto_symext::symex_function_call_code(
   if(emplace_safe_pointers_result.second)
     emplace_safe_pointers_result.first->second(goto_function.body);
 
-  const bool stop_recursing=get_unwind_recursion(
+  const bool stop_recursing = get_unwind_recursion(
     identifier,
     state.source.thread_nr,
-    state.top().loop_iterations[identifier].count);
+    state.call_stack().top().loop_iterations[identifier].count);
 
   // see if it's too much
   if(stop_recursing)
@@ -274,7 +274,8 @@ void goto_symext::symex_function_call_code(
     a = state.rename(std::move(a), ns);
 
   // we hide the call if the caller and callee are both hidden
-  const bool hidden = state.top().hidden_function && goto_function.is_hidden();
+  const bool hidden =
+    state.call_stack().top().hidden_function && goto_function.is_hidden();
 
   // record the call
   target.function_call(
@@ -302,7 +303,7 @@ void goto_symext::symex_function_call_code(
 
   // produce a new frame
   PRECONDITION(!state.call_stack().empty());
-  framet &frame = state.new_frame();
+  framet &frame = state.call_stack().new_frame(state.source);
 
   // preserve locality of local variables
   locality(identifier, state, goto_function, ns);
@@ -315,7 +316,7 @@ void goto_symext::symex_function_call_code(
   frame.function_identifier=identifier;
   frame.hidden_function=goto_function.is_hidden();
 
-  const framet &p_frame = state.previous_frame();
+  const framet &p_frame = state.call_stack().previous_frame();
   for(const auto &pair : p_frame.loop_iterations)
   {
     if(pair.second.is_recursion)
@@ -336,7 +337,7 @@ static void pop_frame(goto_symext::statet &state)
   PRECONDITION(!state.call_stack().empty());
 
   {
-    framet &frame = state.top();
+    const framet &frame = state.call_stack().top();
 
     // restore program counter
     symex_transition(state, frame.calling_location.pc, false);
@@ -365,13 +366,13 @@ static void pop_frame(goto_symext::statet &state)
     }
   }
 
-  state.pop_frame();
+  state.call_stack().pop();
 }
 
 /// do function call by inlining
 void goto_symext::symex_end_of_function(statet &state)
 {
-  const bool hidden = state.top().hidden_function;
+  const bool hidden = state.call_stack().top().hidden_function;
 
   // first record the return
   target.function_return(
@@ -397,7 +398,7 @@ static void locality(
 
   get_local_identifiers(goto_function, local_identifiers);
 
-  framet &frame = state.top();
+  framet &frame = state.call_stack().top();
 
   for(std::set<irep_idt>::const_iterator
       it=local_identifiers.begin();
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
@@ -25,7 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com
 void goto_symext::symex_goto(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
-  framet &frame = state.top();
 
   exprt new_guard = instruction.get_condition();
   clean_expr(new_guard, state, false);
@@ -80,7 +79,7 @@ void goto_symext::symex_goto(statet &state)
     const auto loop_id =
       goto_programt::loop_id(state.source.function_id, *state.source.pc);
 
-    unsigned &unwind = frame.loop_iterations[loop_id].count;
+    unsigned &unwind = state.call_stack().top().loop_iterations[loop_id].count;
     unwind++;
 
     if(should_stop_unwind(state.source, state.call_stack(), unwind))
@@ -210,7 +209,7 @@ void goto_symext::symex_goto(statet &state)
   // put a copy of the current state into the state-queue, to be used by
   // merge_gotos when we visit new_state_pc
   framet::goto_state_listt &goto_state_list =
-    state.top().goto_state_map[new_state_pc];
+    state.call_stack().top().goto_state_map[new_state_pc];
   goto_state_list.emplace_back(state);
 
   symex_transition(state, state_pc, backward);
@@ -288,7 +287,7 @@ void goto_symext::symex_goto(statet &state)
 
 void goto_symext::merge_gotos(statet &state)
 {
-  framet &frame = state.top();
+  framet &frame = state.call_stack().top();
 
   // first, see if this is a target at all
   auto state_map_it = frame.goto_state_map.find(state.source.pc);
@@ -563,7 +562,7 @@ void goto_symext::loop_bound_exceeded(
 
 bool goto_symext::should_stop_unwind(
   const symex_targett::sourcet &,
-  const goto_symex_statet::call_stackt &,
+  const call_stackt &,
   unsigned)
 {
   // by default, we keep going
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
@@ -53,7 +53,7 @@ void symex_transition(
     // 1. the transition from state.source.pc to "to" is not a backwards goto
     // or
     // 2. we are arriving from an outer loop
-    framet &frame = state.top();
+    framet &frame = state.call_stack().top();
     const goto_programt::instructiont &instruction=*to;
     for(const auto &i_e : instruction.incoming_edges)
       if(i_e->is_goto() && i_e->is_backwards_goto() &&
@@ -257,7 +257,7 @@ void goto_symext::symex_with_state(
   // as state.symbol_table might go out of scope
   reset_namespacet reset_ns(ns);
 
-  PRECONDITION(state.top().end_of_function->is_end_function());
+  PRECONDITION(state.call_stack().top().end_of_function->is_end_function());
 
   symex_threaded_step(state, get_goto_function);
   if(should_pause_symex)
@@ -323,9 +323,10 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
 
   goto_programt::const_targett limit =
     std::prev(start_function->body.instructions.end());
-  state->top().end_of_function = limit;
-  state->top().calling_location.pc = state->top().end_of_function;
-  state->top().hidden_function = start_function->is_hidden();
+  state->call_stack().top().end_of_function = limit;
+  state->call_stack().top().calling_location.pc =
+    state->call_stack().top().end_of_function;
+  state->call_stack().top().hidden_function = start_function->is_hidden();
 
   state->symex_target = &target;
 
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp

Original file line number	Diff line number	Diff line change
`@@ -105,7 +105,7 @@ void symex_bmct::merge_goto(goto_statet &&goto_state, statet &state)`
`105`	`105`
`106`	`106`	`bool symex_bmct::should_stop_unwind(`
`107`	`107`	`const symex_targett::sourcet &source,`
`108`		`- const goto_symex_statet::call_stackt &context,`
	`108`	`+ const call_stackt &context,`
`109`	`109`	`unsigned unwind)`
`110`	`110`	`{`
`111`	`111`	`const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc);`
Original file line number	Diff line number	Diff line change
`@@ -33,7 +33,7 @@ goto_symex_statet::goto_symex_statet(const symex_targett::sourcet &_source)`
`33`	`33`	`: goto_statet(_source), symex_target(nullptr), record_events(true), dirty()`
`34`	`34`	`{`
`35`	`35`	`threads.resize(1);`
`36`		`- new_frame();`
	`36`	`+ call_stack().new_frame(source);`
`37`	`37`	`}`
`38`	`38`
`39`	`39`	`goto_symex_statet::~goto_symex_statet()=default;`