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/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_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..7485a4df599 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -22,98 +22,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#include #include +#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 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; - - // 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