From 7f8903e3db0497d520b826eaf5ed7d00b0e7dc02 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 28 Feb 2019 08:51:12 +0000 Subject: [PATCH 1/6] Move goto_statet definition to its own file Having one class per header file makes it easier to navigate the code and find what we want. --- src/goto-symex/Makefile | 1 + src/goto-symex/goto_state.cpp | 22 +++++++++ src/goto-symex/goto_state.h | 70 +++++++++++++++++++++++++++++ src/goto-symex/goto_symex_state.cpp | 11 ----- src/goto-symex/goto_symex_state.h | 51 +-------------------- 5 files changed, 94 insertions(+), 61 deletions(-) create mode 100644 src/goto-symex/goto_state.cpp create mode 100644 src/goto-symex/goto_state.h diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile index b406da78aa8..18b2f028009 100644 --- a/src/goto-symex/Makefile +++ b/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 \ diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp new file mode 100644 index 00000000000..8326d9915a4 --- /dev/null +++ b/src/goto-symex/goto_state.cpp @@ -0,0 +1,22 @@ +/*******************************************************************\ + +Module: Symbolic Execution + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include "goto_state.h" + +#include + +/// 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"; + } +} diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h new file mode 100644 index 00000000000..c34c7df98da --- /dev/null +++ b/src/goto-symex/goto_state.h @@ -0,0 +1,70 @@ +/*******************************************************************\ + +Module: Symbolic Execution + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +/// \file +/// goto_statet class definition + +#ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H +#define CPROVER_GOTO_SYMEX_GOTO_STATE_H + +#include +#include +#include + +#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 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 diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 939c2bbc341..02ff884e118 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/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"; - } -} diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index a438c6d0872..e693aa784c8 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -22,61 +22,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#include #include +#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 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 From 3bce5c287fde48ce3d359731f8879698505d1c90 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 28 Feb 2019 09:18:36 +0000 Subject: [PATCH 2/6] Move framet class to its own file Having one class per file makes it easier to navigate the code and find what you want. --- src/goto-symex/frame.h | 54 +++++++++++++++++++++++++++++++ src/goto-symex/goto_symex_state.h | 38 +--------------------- 2 files changed, 55 insertions(+), 37 deletions(-) create mode 100644 src/goto-symex/frame.h diff --git a/src/goto-symex/frame.h b/src/goto-symex/frame.h new file mode 100644 index 00000000000..cab5914dbf8 --- /dev/null +++ b/src/goto-symex/frame.h @@ -0,0 +1,54 @@ +/*******************************************************************\ + +Module: Symbolic Execution + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +/// \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; + + // function calls + irep_idt function_identifier; + std::map 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 local_objects; + + // exceptions + std::map catch_map; + + // loop and recursion unwinding + struct loop_infot + { + unsigned count = 0; + bool is_recursion = false; + }; + + std::unordered_map loop_iterations; + + explicit framet(symex_targett::sourcet _calling_location) + : calling_location(std::move(_calling_location)) + { + } +}; + +#endif // CPROVER_GOTO_SYMEX_FRAME_H diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index e693aa784c8..7485a4df599 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -24,47 +24,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "frame.h" #include "goto_state.h" #include "renaming_level.h" #include "symex_target_equation.h" -// stack frames -- these are used for function calls and -// for exceptions -struct framet -{ - // gotos - using goto_state_listt = std::list; - - // function calls - irep_idt function_identifier; - std::map 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 local_objects; - - // exceptions - std::map catch_map; - - // loop and recursion unwinding - struct loop_infot - { - unsigned count = 0; - bool is_recursion = false; - }; - std::unordered_map 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 From 3ea80c0d41cf20c188b363cf2d1afdb3bed0960a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 28 Feb 2019 11:30:25 +0000 Subject: [PATCH 3/6] New class for call_stack Extract a call_stackt class from goto_symex_statet to declutter the class definition. This makes some calls a bit more verbose, but can be clearer. For instance, it is not obvious what `top()` represent in the context of goto_symex_state, whereas `call_stack().top()` is more explicit. --- jbmc/src/java_bytecode/java_bmc_util.cpp | 2 +- .../java_enum_static_init_unwind_handler.cpp | 5 +- .../java_enum_static_init_unwind_handler.h | 2 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 2 +- src/goto-checker/symex_bmc.cpp | 2 +- src/goto-checker/symex_bmc.h | 4 +- src/goto-symex/call_stack.h | 46 +++++++++++++++++++ src/goto-symex/goto_symex.h | 2 +- src/goto-symex/goto_symex_state.cpp | 2 +- src/goto-symex/goto_symex_state.h | 25 +--------- src/goto-symex/symex_assign.cpp | 2 +- src/goto-symex/symex_decl.cpp | 7 ++- src/goto-symex/symex_function_call.cpp | 21 +++++---- src/goto-symex/symex_goto.cpp | 9 ++-- src/goto-symex/symex_main.cpp | 11 +++-- src/goto-symex/symex_start_thread.cpp | 4 +- 16 files changed, 84 insertions(+), 62 deletions(-) create mode 100644 src/goto-symex/call_stack.h diff --git a/jbmc/src/java_bytecode/java_bmc_util.cpp b/jbmc/src/java_bytecode/java_bmc_util.cpp index 99a9312ec52..fff94bc9a37 100644 --- 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 index c8e5669be68..bbdc9c92532 100644 --- 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 index 586fbf98c25..89c08dda7b8 100644 --- 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 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 index a50627f88f3..30d076a78de 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -514,7 +514,7 @@ int jbmc_parse_optionst::doit() configure_bmc = [](bmct &bmc, const symbol_tablet &symbol_table) { bmc.add_loop_unwind_handler( [&symbol_table]( - const goto_symex_statet::call_stackt &context, + const call_stackt &context, unsigned loop_number, unsigned unwind, unsigned &max_unwind) { diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index 2acf7de98fe..7252e23e69b 100644 --- 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 index 618a529d7a5..5e322d53090 100644 --- 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 new file mode 100644 index 00000000000..c766272e013 --- /dev/null +++ b/src/goto-symex/call_stack.h @@ -0,0 +1,46 @@ +/*******************************************************************\ + +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 +{ +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() + { + 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 index c1d0ee5b382..a4c68471a7f 100644 --- 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 index 02ff884e118..9c8d826d641 100644 --- 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 index 7485a4df599..c6506c874b8 100644 --- 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 #include +#include "call_stack.h" #include "frame.h" #include "goto_state.h" #include "renaming_level.h" @@ -136,8 +137,6 @@ class goto_symex_statet final : public goto_statet return id; } - typedef std::vector call_stackt; - call_stackt &call_stack() { PRECONDITION(source.thread_nr < threads.size()); @@ -150,28 +149,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 index d078c2502f0..f9a87afbef8 100644 --- 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 index 9055ece53fb..e29a6d33da5 100644 --- 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 index d695db2f44b..add84eae5ba 100644 --- 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::const_iterator it=local_identifiers.begin(); diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 7f147a860a2..e569bda6d8a 100644 --- 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 index 1c80b87c141..82233ed2406 100644 --- 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::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 = ⌖ diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index bdfd028abf5..8253890b9c6 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -42,7 +42,7 @@ void goto_symext::symex_start_thread(statet &state) statet::threadt &new_thread=state.threads.back(); new_thread.pc=thread_target; new_thread.guard=state.guard; - new_thread.call_stack.push_back(state.top()); + new_thread.call_stack.push_back(state.call_stack().top()); new_thread.call_stack.back().local_objects.clear(); new_thread.call_stack.back().goto_state_map.clear(); #if 0 @@ -50,7 +50,7 @@ void goto_symext::symex_start_thread(statet &state) #endif // create a copy of the local variables for the new thread - framet &frame = state.top(); + framet &frame = state.call_stack().top(); for(auto c_it = state.level2.current_names.begin(); c_it != state.level2.current_names.end(); From b620c5769f023811e9a404653d0fe2ff413b36cd Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 28 Feb 2019 13:57:47 +0000 Subject: [PATCH 4/6] Remove unused typedef --- src/goto-symex/goto_symex_state.h | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index c6506c874b8..cf73640bba7 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -127,9 +127,6 @@ class goto_symex_statet final : public goto_statet l1_typest l1_types; public: - // gotos - typedef std::list goto_state_listt; - // guards static irep_idt guard_identifier() { From 1ab1fff0b739c1bcf1b7c414833a2582a00568bc Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 1 Mar 2019 08:49:32 +0000 Subject: [PATCH 5/6] Apply clang-format suggestions No functional change --- jbmc/src/jbmc/jbmc_parse_options.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 30d076a78de..b7f56a06f56 100644 --- 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 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 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); From 52eb5c7c03e244f7360d7f316357205fa893baba Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 1 Mar 2019 08:52:16 +0000 Subject: [PATCH 6/6] Add precondition on call_stackt::pop Guarantee that it is never called on an empty stack. --- src/goto-symex/call_stack.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/goto-symex/call_stack.h b/src/goto-symex/call_stack.h index c766272e013..9aeaf46458d 100644 --- a/src/goto-symex/call_stack.h +++ b/src/goto-symex/call_stack.h @@ -34,6 +34,7 @@ class call_stackt : public std::vector void pop() { + PRECONDITION(!empty()); pop_back(); }