From ba8bbe2d24ecf83615d1a5cd53e092a78c81a2fd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 11 Feb 2018 16:31:40 +0000 Subject: [PATCH 1/3] expand goto_programt and goto_functionst templates The goto_program_template and the goto_functions_template each only have one instance, but make it much harder to read the code. --- src/analyses/constant_propagator.cpp | 2 + src/analyses/custom_bitvector_analysis.cpp | 2 + src/analyses/goto_check.cpp | 2 + src/analyses/goto_rw.cpp | 2 + src/analyses/interval_domain.cpp | 1 + src/cbmc/bmc_cover.cpp | 3 + src/cbmc/symex_coverage.cpp | 2 + src/goto-instrument/call_sequences.cpp | 2 + .../cover_instrument_condition.cpp | 2 + .../cover_instrument_decision.cpp | 2 + src/goto-instrument/cover_instrument_mcdc.cpp | 2 + .../cover_instrument_other.cpp | 2 + src/goto-instrument/dot.cpp | 2 + src/goto-instrument/wmm/goto2graph.cpp | 2 +- src/goto-programs/builtin_functions.cpp | 4 +- src/goto-programs/goto_functions.cpp | 64 +- src/goto-programs/goto_functions.h | 170 +++- src/goto-programs/goto_functions_template.h | 264 ------ src/goto-programs/goto_inline_class.cpp | 2 + src/goto-programs/goto_program.cpp | 149 +++- src/goto-programs/goto_program.h | 674 +++++++++++++- src/goto-programs/goto_program_template.cpp | 2 +- src/goto-programs/goto_program_template.h | 841 ------------------ src/goto-programs/graphml_witness.cpp | 4 +- src/goto-programs/interpreter_evaluate.cpp | 2 + src/goto-programs/lazy_goto_functions_map.h | 11 +- src/goto-programs/lazy_goto_model.h | 2 +- src/pointer-analysis/value_set.cpp | 3 +- unit/goto-programs/goto_trace_output.cpp | 2 +- 29 files changed, 1074 insertions(+), 1148 deletions(-) delete mode 100644 src/goto-programs/goto_functions_template.h delete mode 100644 src/goto-programs/goto_program_template.h diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index fa410762bf2..8a18888fbcf 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -20,6 +20,8 @@ Author: Peter Schrammel #include #include +#include + void constant_propagator_domaint::assign_rec( valuest &values, const exprt &lhs, diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index ae452b36002..be96ce1e2c2 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include void custom_bitvector_domaint::set_bit( diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index d88035159b9..344f4a85ed1 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -28,6 +28,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "local_bitvector_analysis.h" class goto_checkt diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index e965337a31c..be0f162c539 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -23,6 +23,8 @@ Date: April 2010 #include #include +#include + #include #include diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 1b237c31f1f..bdf1ccec09a 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifdef DEBUG #include +#include #endif #include diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 2afc70a59d8..d43e7ac9d8b 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "bmc.h" #include +#include #include #include @@ -25,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "bv_cbmc.h" class bmc_covert: diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index c6a9e3cd419..43f431a5ae8 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/src/cbmc/symex_coverage.cpp @@ -23,6 +23,8 @@ Date: March 2016 #include #include +#include + #include #include diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index cc16768f870..c188828768b 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -22,6 +22,8 @@ Date: April 2013 #include +#include + void show_call_sequences( const irep_idt &caller, const goto_programt &goto_program) diff --git a/src/goto-instrument/cover_instrument_condition.cpp b/src/goto-instrument/cover_instrument_condition.cpp index d5b3778d649..1bc3b2769b1 100644 --- a/src/goto-instrument/cover_instrument_condition.cpp +++ b/src/goto-instrument/cover_instrument_condition.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening #include "cover_instrument.h" +#include + #include "cover_util.h" void cover_condition_instrumentert::instrument( diff --git a/src/goto-instrument/cover_instrument_decision.cpp b/src/goto-instrument/cover_instrument_decision.cpp index 9c5fc59074d..122e05046e3 100644 --- a/src/goto-instrument/cover_instrument_decision.cpp +++ b/src/goto-instrument/cover_instrument_decision.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening #include "cover_instrument.h" +#include + #include "cover_util.h" void cover_decision_instrumentert::instrument( diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp index a708583c559..e06508d84d8 100644 --- a/src/goto-instrument/cover_instrument_mcdc.cpp +++ b/src/goto-instrument/cover_instrument_mcdc.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening #include "cover_instrument.h" +#include + #include #include "cover_util.h" diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp index d2f37d598e7..bc97a809da9 100644 --- a/src/goto-instrument/cover_instrument_other.cpp +++ b/src/goto-instrument/cover_instrument_other.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening #include "cover_instrument.h" +#include + #include "cover_util.h" void cover_path_instrumentert::instrument( diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index d011c10914a..84f5cf6c907 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -15,6 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #define DOTGRAPHSETTINGS "color=black;" \ "orientation=portrait;" \ "fontsize=20;"\ diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 09afe5d1836..13587974058 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -1301,7 +1301,7 @@ bool instrumentert::is_cfg_spurious(const event_grapht::critical_cyclet &cyc) /* now test whether this part of the code can exist */ goto_functionst::function_mapt map; - goto_function_templatet one_interleaving; + goto_functiont one_interleaving; one_interleaving.body.copy_from(interleaving); map.insert(std::make_pair( goto_functionst::entry_point(), diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index e4c6fb3849c..60fe569f845 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include #include @@ -29,9 +30,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include +#include + #include "format_strings.h" #include "class_identifier.h" diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index 9c14c8bc6bc..44d9d31d6b7 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -13,8 +13,70 @@ Date: June 2003 #include "goto_functions.h" +void goto_functionst::output( + const namespacet &ns, + std::ostream &out) const +{ + for(const auto &fun : function_map) + { + if(fun.second.body_available()) + { + out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; + + const symbolt &symbol=ns.lookup(fun.first); + out << symbol.display_name() << " /* " << symbol.name << " */\n"; + fun.second.body.output(ns, symbol.name, out); + + out << std::flush; + } + } +} + +void goto_functionst::compute_location_numbers() +{ + unused_location_number = 0; + for(auto &func : function_map) + { + // Side-effect: bumps unused_location_number. + func.second.body.compute_location_numbers(unused_location_number); + } +} + +void goto_functionst::compute_location_numbers( + goto_programt &program) +{ + // Renumber just this single function. Use fresh numbers in case it has + // grown since it was last numbered. + program.compute_location_numbers(unused_location_number); +} + +void goto_functionst::compute_incoming_edges() +{ + for(auto &func : function_map) + { + func.second.body.compute_incoming_edges(); + } +} + +void goto_functionst::compute_target_numbers() +{ + for(auto &func : function_map) + { + func.second.body.compute_target_numbers(); + } +} + +void goto_functionst::compute_loop_numbers() +{ + for(auto &func : function_map) + { + func.second.body.compute_loop_numbers(); + } +} + + void get_local_identifiers( - const goto_function_templatet &goto_function, + const goto_functiont &goto_function, std::set &dest) { goto_function.body.get_decl_identifiers(dest); diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index 7fc9f70628a..12b6b8c98be 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -15,12 +15,115 @@ Date: June 2003 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H #include "goto_program.h" -#include "goto_functions_template.h" -class goto_functionst:public goto_functions_templatet +#include +#include + +#include +#include +#include + +class goto_functiont { public: - goto_functionst()=default; + goto_programt body; + code_typet type; + + typedef std::vector parameter_identifierst; + parameter_identifierst parameter_identifiers; + + bool body_available() const + { + return !body.instructions.empty(); + } + + bool is_inlined() const + { + return type.get_bool(ID_C_inlined); + } + + bool is_hidden() const + { + return type.get_bool(ID_C_hide); + } + + void make_hidden() + { + type.set(ID_C_hide, true); + } + + goto_functiont() + { + } + + void clear() + { + body.clear(); + type.clear(); + parameter_identifiers.clear(); + } + + /// update the function member in each instruction + /// \param function_id: the `function_id` used for assigning empty function + /// members + void update_instructions_function(const irep_idt &function_id) + { + body.update_instructions_function(function_id); + } + + void swap(goto_functiont &other) + { + body.swap(other.body); + type.swap(other.type); + parameter_identifiers.swap(other.parameter_identifiers); + } + + void copy_from(const goto_functiont &other) + { + body.copy_from(other.body); + type=other.type; + parameter_identifiers=other.parameter_identifiers; + } + + goto_functiont(const goto_functiont &)=delete; + goto_functiont &operator=(const goto_functiont &)=delete; + + goto_functiont(goto_functiont &&other): + body(std::move(other.body)), + type(std::move(other.type)), + parameter_identifiers(std::move(other.parameter_identifiers)) + { + } + + goto_functiont &operator=(goto_functiont &&other) + { + body=std::move(other.body); + type=std::move(other.type); + parameter_identifiers=std::move(other.parameter_identifiers); + return *this; + } +}; + +class goto_functionst +{ +public: + using goto_functiont=::goto_functiont; + typedef std::map function_mapt; + function_mapt function_map; + +private: + /// A location number such that numbers in the interval + /// [unused_location_number, MAX_UINT] are all unused. There might still be + /// unused numbers below this. + /// If numbering a new function or renumbering a function, starting from this + /// number is safe. + unsigned unused_location_number; + +public: + goto_functionst(): + unused_location_number(0) + { + } // Copying is unavailable as base class copy is deleted // MSVC is unable to automatically determine this @@ -34,15 +137,70 @@ class goto_functionst:public goto_functions_templatet // under "Defaulted and Deleted Functions") goto_functionst(goto_functionst &&other): - goto_functions_templatet(std::move(other)) + function_map(std::move(other.function_map)), + unused_location_number(other.unused_location_number) { } goto_functionst &operator=(goto_functionst &&other) { - goto_functions_templatet::operator=(std::move(other)); + function_map=std::move(other.function_map); + unused_location_number=other.unused_location_number; return *this; } + + void unload(const irep_idt &name) { function_map.erase(name); } + + void clear() + { + function_map.clear(); + } + + void output( + const namespacet &ns, + std::ostream &out) const; + + void compute_location_numbers(); + void compute_location_numbers(goto_programt &); + void compute_loop_numbers(); + void compute_target_numbers(); + void compute_incoming_edges(); + + /// update the function member in each instruction by setting it to + /// the goto function's identifier + void update_instructions_function() + { + for(auto &func : function_map) + { + func.second.update_instructions_function(func.first); + } + } + + void update() + { + compute_incoming_edges(); + compute_target_numbers(); + compute_location_numbers(); + compute_loop_numbers(); + update_instructions_function(); + } + + static inline irep_idt entry_point() + { + // do not confuse with C's "int main()" + return CPROVER_PREFIX "_start"; + } + + void swap(goto_functionst &other) + { + function_map.swap(other.function_map); + } + + void copy_from(const goto_functionst &other) + { + for(const auto &fun : other.function_map) + function_map[fun.first].copy_from(fun.second); + } }; #define Forall_goto_functions(it, functions) \ @@ -56,7 +214,7 @@ class goto_functionst:public goto_functions_templatet it!=(functions).function_map.end(); it++) void get_local_identifiers( - const goto_function_templatet &goto_function, + const goto_functiont &, std::set &dest); #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h deleted file mode 100644 index 08dc0494252..00000000000 --- a/src/goto-programs/goto_functions_template.h +++ /dev/null @@ -1,264 +0,0 @@ -/*******************************************************************\ - -Module: Goto Programs with Functions - -Author: Daniel Kroening - -Date: June 2003 - -\*******************************************************************/ - -/// \file -/// Goto Programs with Functions - -#ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H -#define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H - -#include -#include - -#include -#include -#include - -template -class goto_function_templatet -{ -public: - bodyT body; - code_typet type; - - typedef std::vector parameter_identifierst; - parameter_identifierst parameter_identifiers; - - bool body_available() const - { - return !body.instructions.empty(); - } - - bool is_inlined() const - { - return type.get_bool(ID_C_inlined); - } - - bool is_hidden() const - { - return type.get_bool(ID_C_hide); - } - - void make_hidden() - { - type.set(ID_C_hide, true); - } - - goto_function_templatet() - { - } - - void clear() - { - body.clear(); - type.clear(); - parameter_identifiers.clear(); - } - - /// update the function member in each instruction - /// \param function_id: the `function_id` used for assigning empty function - /// members - void update_instructions_function(const irep_idt &function_id) - { - body.update_instructions_function(function_id); - } - - void swap(goto_function_templatet &other) - { - body.swap(other.body); - type.swap(other.type); - parameter_identifiers.swap(other.parameter_identifiers); - } - - void copy_from(const goto_function_templatet &other) - { - body.copy_from(other.body); - type=other.type; - parameter_identifiers=other.parameter_identifiers; - } - - goto_function_templatet(const goto_function_templatet &)=delete; - goto_function_templatet &operator=(const goto_function_templatet &)=delete; - - goto_function_templatet(goto_function_templatet &&other): - body(std::move(other.body)), - type(std::move(other.type)), - parameter_identifiers(std::move(other.parameter_identifiers)) - { - } - - goto_function_templatet &operator=(goto_function_templatet &&other) - { - body=std::move(other.body); - type=std::move(other.type); - parameter_identifiers=std::move(other.parameter_identifiers); - return *this; - } -}; - -template -class goto_functions_templatet -{ -public: - typedef goto_function_templatet goto_functiont; - typedef std::map function_mapt; - function_mapt function_map; - -private: - /// A location number such that numbers in the interval - /// [unused_location_number, MAX_UINT] are all unused. There might still be - /// unused numbers below this. - /// If numbering a new function or renumbering a function, starting from this - /// number is safe. - unsigned unused_location_number; - -public: - goto_functions_templatet(): - unused_location_number(0) - { - } - - goto_functions_templatet(const goto_functions_templatet &)=delete; - goto_functions_templatet &operator=(const goto_functions_templatet &)=delete; - - goto_functions_templatet(goto_functions_templatet &&other): - function_map(std::move(other.function_map)), - unused_location_number(other.unused_location_number) - { - } - - goto_functions_templatet &operator=(goto_functions_templatet &&other) - { - function_map=std::move(other.function_map); - return *this; - } - - void unload(const irep_idt &name) { function_map.erase(name); } - - void clear() - { - function_map.clear(); - } - - void output( - const namespacet &ns, - std::ostream &out) const; - - void compute_location_numbers(); - void compute_location_numbers(goto_programt &); - void compute_loop_numbers(); - void compute_target_numbers(); - void compute_incoming_edges(); - - /// update the function member in each instruction by setting it to - /// the goto function's identifier - void update_instructions_function() - { - for(auto &func : function_map) - { - func.second.update_instructions_function(func.first); - } - } - - void update() - { - compute_incoming_edges(); - compute_target_numbers(); - compute_location_numbers(); - compute_loop_numbers(); - update_instructions_function(); - } - - static inline irep_idt entry_point() - { - // do not confuse with C's "int main()" - return CPROVER_PREFIX "_start"; - } - - void swap(goto_functions_templatet &other) - { - function_map.swap(other.function_map); - } - - void copy_from(const goto_functions_templatet &other) - { - for(const auto &fun : other.function_map) - function_map[fun.first].copy_from(fun.second); - } -}; - -template -void goto_functions_templatet::output( - const namespacet &ns, - std::ostream &out) const -{ - for(const auto &fun : function_map) - { - if(fun.second.body_available()) - { - out << "^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n"; - - const symbolt &symbol=ns.lookup(fun.first); - out << symbol.display_name() << " /* " << symbol.name << " */\n"; - fun.second.body.output(ns, symbol.name, out); - - out << std::flush; - } - } -} - -template -void goto_functions_templatet::compute_location_numbers() -{ - unused_location_number = 0; - for(auto &func : function_map) - { - // Side-effect: bumps unused_location_number. - func.second.body.compute_location_numbers(unused_location_number); - } -} - -template -void goto_functions_templatet::compute_location_numbers( - goto_programt &program) -{ - // Renumber just this single function. Use fresh numbers in case it has - // grown since it was last numbered. - program.compute_location_numbers(unused_location_number); -} - -template -void goto_functions_templatet::compute_incoming_edges() -{ - for(auto &func : function_map) - { - func.second.body.compute_incoming_edges(); - } -} - -template -void goto_functions_templatet::compute_target_numbers() -{ - for(auto &func : function_map) - { - func.second.body.compute_target_numbers(); - } -} - -template -void goto_functions_templatet::compute_loop_numbers() -{ - for(auto &func : function_map) - { - func.second.body.compute_loop_numbers(); - } -} - -#endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_TEMPLATE_H diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index ee89b365ec6..d24f5257ef4 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -25,6 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "remove_skip.h" #include "goto_inline.h" diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 00e7a5ff49d..f253c9ba1d2 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_program.h" #include +#include #include @@ -34,7 +35,7 @@ std::ostream &goto_programt::output_instruction( const namespacet &ns, const irep_idt &identifier, std::ostream &out, - const goto_program_templatet::instructiont &instruction) const + const instructiont &instruction) const { out << " // " << instruction.location_number << " "; @@ -482,3 +483,149 @@ std::string as_string( throw "unknown statement"; } } + +void goto_programt::compute_loop_numbers() +{ + unsigned nr=0; + for(auto &i : instructions) + if(i.is_backwards_goto()) + i.loop_number=nr++; +} + +void goto_programt::update() +{ + compute_incoming_edges(); + compute_target_numbers(); + compute_location_numbers(); + compute_loop_numbers(); +} + +std::ostream &goto_programt::output( + const namespacet &ns, + const irep_idt &identifier, + std::ostream &out) const +{ + // output program + + for(const auto &instruction : instructions) + output_instruction(ns, identifier, out, instruction); + + return out; +} + +void goto_programt::compute_target_numbers() +{ + // reset marking + + for(auto &i : instructions) + i.target_number=instructiont::nil_target; + + // mark the goto targets + + for(const auto &i : instructions) + { + for(const auto &t : i.targets) + { + if(t!=instructions.end()) + t->target_number=0; + } + } + + // number the targets properly + unsigned cnt=0; + + for(auto &i : instructions) + { + if(i.is_target()) + { + i.target_number=++cnt; + assert(i.target_number!=0); + } + } + + // check the targets! + // (this is a consistency check only) + + for(const auto &i : instructions) + { + for(const auto &t : i.targets) + { + if(t!=instructions.end()) + { + assert(t->target_number!=0); + assert(t->target_number!=instructiont::nil_target); + } + } + } +} + +void goto_programt::copy_from(const goto_programt &src) +{ + // Definitions for mapping between the two programs + typedef std::map targets_mappingt; + targets_mappingt targets_mapping; + + clear(); + + // Loop over program - 1st time collects targets and copy + + for(instructionst::const_iterator + it=src.instructions.begin(); + it!=src.instructions.end(); + ++it) + { + auto new_instruction=add_instruction(); + targets_mapping[it]=new_instruction; + *new_instruction=*it; + } + + // Loop over program - 2nd time updates targets + + for(auto &i : instructions) + { + for(auto &t : i.targets) + { + targets_mappingt::iterator + m_target_it=targets_mapping.find(t); + + if(m_target_it==targets_mapping.end()) + throw "copy_from: target not found"; + + t=m_target_it->second; + } + } + + compute_incoming_edges(); + compute_target_numbers(); +} + +// number them +bool goto_programt::has_assertion() const +{ + for(const auto &i : instructions) + if(i.is_assert() && !i.guard.is_true()) + return true; + + return false; +} + +void goto_programt::compute_incoming_edges() +{ + for(auto &i : instructions) + { + i.incoming_edges.clear(); + } + + for(instructionst::iterator + it=instructions.begin(); + it!=instructions.end(); + ++it) + { + for(const auto &s : get_successors(it)) + { + if(s!=instructions.end()) + s->incoming_edges.insert(it); + } + } +} + diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 4ef4262a0d1..ad5d2d6254f 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -12,28 +12,65 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H +#include +#include #include +#include +#include +#include +#include +#include +#include +#include +#include #include -#include "goto_program_template.h" - -/*! \brief A specialization of goto_program_templatet over - goto programs in which instructions have codet type. -*/ -class goto_programt:public goto_program_templatet +/// The type of an instruction in a GOTO program. +enum goto_program_instruction_typet { -public: - std::ostream &output_instruction( - const class namespacet &ns, - const irep_idt &identifier, - std::ostream &out, - const instructiont &instruction) const override; + NO_INSTRUCTION_TYPE=0, + GOTO=1, // branch, possibly guarded + ASSUME=2, // non-failing guarded self loop + ASSERT=3, // assertions + OTHER=4, // anything else + SKIP=5, // just advance the PC + START_THREAD=6, // spawns an asynchronous thread + END_THREAD=7, // end the current thread + LOCATION=8, // semantically like SKIP + END_FUNCTION=9, // exit point of a function + ATOMIC_BEGIN=10, // marks a block without interleavings + ATOMIC_END=11, // end of a block without interleavings + RETURN=12, // set function return value (no control-flow change) + ASSIGN=13, // assignment lhs:=rhs + DECL=14, // declare a local variable + DEAD=15, // marks the end-of-live of a local variable + FUNCTION_CALL=16, // call a function + THROW=17, // throw an exception + CATCH=18 // push, pop or enter an exception handler +}; - goto_programt() { } +std::ostream &operator<<(std::ostream &, goto_program_instruction_typet); - // Copying is unavailable as base class copy is deleted - // MSVC is unable to automatically determine this +/// A generic container class for the GOTO intermediate representation of one +/// function. +/// +/// A function is represented by a std::list of instructions. Execution starts +/// in the first instruction of the list. Then, the execution of the i-th +/// instruction is followed by the execution of the (i+1)-th instruction unless +/// instruction i jumps to some other instruction in the list. See the internal +/// class instructiont for additional details +/// +/// Although it is straightforward to compute the control flow graph (CFG) of a +/// function from the list of instructions and the goto target locations in +/// instructions, the GOTO intermediate representation is _not_ regarded as the +/// CFG of a function. See instead the class cfg_baset, which is based on grapht +/// and allows for easier implementation of generic graph algorithms (e.g., +/// dominator analysis). +class goto_programt +{ +public: + /// Copying is deleted as this class contains pointers that cannot be copied goto_programt(const goto_programt &)=delete; goto_programt &operator=(const goto_programt &)=delete; @@ -44,21 +81,617 @@ class goto_programt:public goto_program_templatet // under "Defaulted and Deleted Functions") goto_programt(goto_programt &&other): - goto_program_templatet(std::move(other)) + instructions(std::move(other.instructions)) { } goto_programt &operator=(goto_programt &&other) { - goto_program_templatet::operator=(std::move(other)); + instructions=std::move(other.instructions); return *this; } - // get the variables in decl statements + /// This class represents an instruction in the GOTO intermediate + /// representation. Three fields are key: + /// + /// - type: an enum value describing the action performed by this instruction + /// - guard: an (arbitrarily complex) expression (usually an \ref exprt) of + /// Boolean type + /// - code: a code statement (usually a \ref codet) + /// + /// The meaning of an instruction node depends on the `type` field. Different + /// kinds of instructions make use of the fields `guard` and `code` for + /// different purposes. We list below, using a mixture of pseudo code and + /// plain English, the meaning of different kinds of instructions. + /// We use `guard`, `code`, and `targets` to mean the value of the + /// respective fields in this class: + /// + /// - GOTO: + /// if `guard` then goto `targets` + /// - RETURN: + /// Set the value returned by `code` (which shall be either nil or an + /// instance of code_returnt) and then jump to the end of the function. + /// - DECL: + /// Introduces a symbol denoted by the field `code` (an instance of + /// code_declt), the life-time of which is bounded by a corresponding DEAD + /// instruction. + /// - FUNCTION_CALL: + /// Invoke the function denoted by field `code` (an instance of + /// code_function_callt). + /// - ASSIGN: + /// Update the left-hand side of `code` (an instance of code_assignt) to + /// the value of the right-hand side. + /// - OTHER: + /// Execute the `code` (an instance of codet of kind ID_fence, ID_printf, + /// ID_array_copy, ID_array_set, ID_input, ID_output, ...). + /// - ASSUME: + /// Wait for `guard` to evaluate to true. + /// - ASSERT: + /// Using ASSERT instructions is the one and only way to express + /// properties to be verified. Execution paths abort if `guard` evaluates + /// to false. + /// - SKIP, LOCATION: + /// No-op. + /// - ATOMIC_BEGIN, ATOMIC_END: + /// When a thread executes ATOMIC_BEGIN, no thread other will be able to + /// execute any instruction until the same thread executes ATOMIC_END. + /// - END_FUNCTION: + /// Can only occur as the last instruction of the list. + /// - START_THREAD: + /// Create a new thread and run the code of this function starting from + /// targets[0]. Quite often the instruction pointed by targets[0] will be + /// just a FUNCTION_CALL, followed by an END_THREAD. + /// - END_THREAD: + /// Terminate the calling thread. + /// - THROW: + /// throw `exception1`, ..., `exceptionN` + /// where the list of exceptions is extracted from the `code` field + /// - CATCH, when code.find(ID_exception_list) is non-empty: + /// Establishes that from here to the next occurrence of CATCH with an + /// empty list (see below) if + /// - `exception1` is thrown, then goto `target1`, + /// - ... + /// - `exceptionN` is thrown, then goto `targetN`. + /// The list of exceptions is obtained from the `code` field and the list + /// of targets from the `targets` field. + /// - CATCH, when empty code.find(ID_exception_list) is empty: + /// clears all the catch clauses established as per the above in this + /// function? + class instructiont final + { + public: + codet code; + + /// The function this instruction belongs to + irep_idt function; + + /// The location of the instruction in the source file + source_locationt source_location; + + /// What kind of instruction? + goto_program_instruction_typet type; + + /// Guard for gotos, assume, assert + exprt guard; + + // The below will eventually become a single target only. + /// The target for gotos and for start_thread nodes + typedef std::list::iterator targett; + typedef std::list::const_iterator const_targett; + typedef std::list targetst; + typedef std::list const_targetst; + + /// The list of successor instructions + targetst targets; + + /// Returns the first (and only) successor for the usual case of a single + /// target + targett get_target() const + { + assert(targets.size()==1); + return targets.front(); + } + + /// Sets the first (and only) successor for the usual case of a single + /// target + void set_target(targett t) + { + targets.clear(); + targets.push_back(t); + } + + bool has_target() const + { + return !targets.empty(); + } + + /// Goto target labels + typedef std::list labelst; + labelst labels; + + // will go away + std::set incoming_edges; + + /// Is this node a branch target? + bool is_target() const + { return target_number!=nil_target; } + + /// Clear the node + void clear(goto_program_instruction_typet _type) + { + type=_type; + targets.clear(); + guard=true_exprt(); + code.make_nil(); + } + + void make_goto() { clear(GOTO); } + void make_return() { clear(RETURN); } + void make_skip() { clear(SKIP); } + void make_location(const source_locationt &l) + { clear(LOCATION); source_location=l; } + void make_throw() { clear(THROW); } + void make_catch() { clear(CATCH); } + void make_assertion(const exprt &g) { clear(ASSERT); guard=g; } + void make_assumption(const exprt &g) { clear(ASSUME); guard=g; } + void make_assignment() { clear(ASSIGN); } + void make_other(const codet &_code) { clear(OTHER); code=_code; } + void make_decl() { clear(DECL); } + void make_dead() { clear(DEAD); } + void make_atomic_begin() { clear(ATOMIC_BEGIN); } + void make_atomic_end() { clear(ATOMIC_END); } + void make_end_function() { clear(END_FUNCTION); } + + void make_goto(targett _target) + { + make_goto(); + targets.push_back(_target); + } + + void make_goto(targett _target, const exprt &g) + { + make_goto(_target); + guard=g; + } + + void make_assignment(const codet &_code) + { + clear(ASSIGN); + code=_code; + } + + void make_decl(const codet &_code) + { + clear(DECL); + code=_code; + } + + void make_function_call(const codet &_code) + { + clear(FUNCTION_CALL); + code=_code; + } + + bool is_goto () const { return type==GOTO; } + bool is_return () const { return type==RETURN; } + bool is_assign () const { return type==ASSIGN; } + bool is_function_call() const { return type==FUNCTION_CALL; } + bool is_throw () const { return type==THROW; } + bool is_catch () const { return type==CATCH; } + bool is_skip () const { return type==SKIP; } + bool is_location () const { return type==LOCATION; } + bool is_other () const { return type==OTHER; } + bool is_decl () const { return type==DECL; } + bool is_dead () const { return type==DEAD; } + bool is_assume () const { return type==ASSUME; } + bool is_assert () const { return type==ASSERT; } + bool is_atomic_begin () const { return type==ATOMIC_BEGIN; } + bool is_atomic_end () const { return type==ATOMIC_END; } + bool is_start_thread () const { return type==START_THREAD; } + bool is_end_thread () const { return type==END_THREAD; } + bool is_end_function () const { return type==END_FUNCTION; } + + instructiont(): + instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit) + { + } + + explicit instructiont(goto_program_instruction_typet _type): + source_location(static_cast(get_nil_irep())), + type(_type), + guard(true_exprt()), + location_number(0), + loop_number(0), + target_number(nil_target) + { + } + + /// Swap two instructions + void swap(instructiont &instruction) + { + using std::swap; + swap(instruction.code, code); + swap(instruction.source_location, source_location); + swap(instruction.type, type); + swap(instruction.guard, guard); + swap(instruction.targets, targets); + swap(instruction.function, function); + } + + #if (defined _MSC_VER && _MSC_VER <= 1800) + // Visual Studio <= 2013 does not support constexpr, making + // numeric_limits::max() unviable for a static const member + static const unsigned nil_target= + static_cast(-1); + #else + /// Uniquely identify an invalid target or location + static const unsigned nil_target= + std::numeric_limits::max(); + #endif + + /// A globally unique number to identify a program location. + /// It's guaranteed to be ordered in program order within + /// one goto_program. + unsigned location_number; + + /// Number unique per function to identify loops + unsigned loop_number; + + /// A number to identify branch targets. + /// This is \ref nil_target if it's not a target. + unsigned target_number; + + /// Returns true if the instruction is a backwards branch. + bool is_backwards_goto() const + { + if(!is_goto()) + return false; + + for(const auto &t : targets) + if(t->location_number<=location_number) + return true; + + return false; + } + + std::string to_string() const + { + std::ostringstream instruction_id_builder; + instruction_id_builder << type; + return instruction_id_builder.str(); + } + }; + + // Never try to change this to vector-we mutate the list while iterating + typedef std::list instructionst; + + typedef instructionst::iterator targett; + typedef instructionst::const_iterator const_targett; + typedef std::list targetst; + typedef std::list const_targetst; + + /// The list of instructions in the goto program + instructionst instructions; + + /// Convert a const_targett to a targett - use with care and avoid + /// whenever possible + targett const_cast_target(const_targett t) + { + return instructions.erase(t, t); + } + + /// Dummy for templates with possible const contexts + const_targett const_cast_target(const_targett t) const + { + return t; + } + + static const irep_idt get_function_id( + const_targett l) + { + while(!l->is_end_function()) + ++l; + + return l->function; + } + + static const irep_idt get_function_id( + const goto_programt &p) + { + assert(!p.empty()); + + return get_function_id(--p.instructions.end()); + } + + template + std::list get_successors(Target target) const; + + void compute_incoming_edges(); + + /// Insertion that preserves jumps to "target". + void insert_before_swap(targett target) + { + assert(target!=instructions.end()); + const auto next=std::next(target); + instructions.insert(next, instructiont())->swap(*target); + } + + /// Insertion that preserves jumps to "target". + /// The instruction is destroyed. + void insert_before_swap(targett target, instructiont &instruction) + { + insert_before_swap(target); + target->swap(instruction); + } + + /// Insertion that preserves jumps to "target". + /// The program p is destroyed. + void insert_before_swap( + targett target, + goto_programt &p) + { + assert(target!=instructions.end()); + if(p.instructions.empty()) + return; + insert_before_swap(target, p.instructions.front()); + auto next=std::next(target); + p.instructions.erase(p.instructions.begin()); + instructions.splice(next, p.instructions); + } + + /// Insertion before the given target + /// \return newly inserted location + targett insert_before(const_targett target) + { + return instructions.insert(target, instructiont()); + } + + /// Insertion after the given target + /// \return newly inserted location + targett insert_after(const_targett target) + { + return instructions.insert(std::next(target), instructiont()); + } + + /// Appends the given program, which is destroyed + void destructive_append(goto_programt &p) + { + instructions.splice(instructions.end(), + p.instructions); + // BUG: The iterators to p-instructions are invalidated! + } + + /// Inserts the given program at the given location. + /// The program is destroyed. + void destructive_insert( + const_targett target, + goto_programt &p) + { + instructions.splice(target, p.instructions); + // BUG: The iterators to p-instructions are invalidated! + } + + /// Adds an instruction at the end. + /// \return The newly added instruction. + targett add_instruction() + { + instructions.push_back(instructiont()); + return --instructions.end(); + } + + /// Adds an instruction of given type at the end. + /// \return The newly added instruction. + targett add_instruction(goto_program_instruction_typet type) + { + instructions.push_back(instructiont(type)); + return --instructions.end(); + } + + /// Output goto program to given stream + std::ostream &output( + const namespacet &ns, + const irep_idt &identifier, + std::ostream &out) const; + + /// Output goto-program to given stream + std::ostream &output(std::ostream &out) const + { + return output(namespacet(symbol_tablet()), "", out); + } + + /// Output a single instruction + std::ostream &output_instruction( + const namespacet &ns, + const irep_idt &identifier, + std::ostream &out, + const instructionst::value_type &it) const; + + /// Compute the target numbers + void compute_target_numbers(); + + /// Compute location numbers + void compute_location_numbers(unsigned &nr) + { + for(auto &i : instructions) + { + INVARIANT( + nr != std::numeric_limits::max(), + "Too many location numbers assigned"); + i.location_number=nr++; + } + } + + /// Sets the `function` member of each instruction if not yet set + /// Note that a goto program need not be a goto function and therefore, + /// we cannot do this in update(), but only at the level of + /// of goto_functionst where goto programs are guaranteed to be + /// named functions. + void update_instructions_function(const irep_idt &function_id) + { + for(auto &instruction : instructions) + { + if(instruction.function.empty()) + { + instruction.function = function_id; + } + } + } + + /// Compute location numbers + void compute_location_numbers() + { + unsigned nr=0; + compute_location_numbers(nr); + } + + /// Compute loop numbers + void compute_loop_numbers(); + + /// Update all indices + void update(); + + /// Human-readable loop name + static irep_idt loop_id(const instructiont &instruction) + { + return id2string(instruction.function)+"."+ + std::to_string(instruction.loop_number); + } + + /// Is the program empty? + bool empty() const + { + return instructions.empty(); + } + + /// Constructor + goto_programt() + { + } + + ~goto_programt() + { + } + + /// Swap the goto program + void swap(goto_programt &program) + { + program.instructions.swap(instructions); + } + + /// Clear the goto program + void clear() + { + instructions.clear(); + } + + targett get_end_function() + { + assert(!instructions.empty()); + const auto end_function=std::prev(instructions.end()); + assert(end_function->is_end_function()); + return end_function; + } + + /// Copy a full goto program, preserving targets + void copy_from(const goto_programt &src); + + /// Does the goto program have an assertion? + bool has_assertion() const; + typedef std::set decl_identifierst; + /// get the variables in decl statements void get_decl_identifiers(decl_identifierst &decl_identifiers) const; }; +template +std::list goto_programt::get_successors( + Target target) const +{ + if(target==instructions.end()) + return std::list(); + + const auto next=std::next(target); + + const instructiont &i=*target; + + if(i.is_goto()) + { + std::list successors(i.targets.begin(), i.targets.end()); + + if(!i.guard.is_true() && next!=instructions.end()) + successors.push_back(next); + + return successors; + } + + if(i.is_start_thread()) + { + std::list successors(i.targets.begin(), i.targets.end()); + + if(next!=instructions.end()) + successors.push_back(next); + + return successors; + } + + if(i.is_end_thread()) + { + // no successors + return std::list(); + } + + if(i.is_throw()) + { + // the successors are non-obvious + return std::list(); + } + + if(i.is_assume()) + { + return + !i.guard.is_false() && next!=instructions.end() ? + std::list{next} : + std::list(); + } + + if(next!=instructions.end()) + { + return std::list{next}; + } + + return std::list(); +} + +inline bool order_const_target( + const goto_programt::const_targett i1, + const goto_programt::const_targett i2) +{ + const goto_programt::instructiont &_i1=*i1; + const goto_programt::instructiont &_i2=*i2; + return &_i1<&_i2; +} + +struct const_target_hash +{ + std::size_t operator()( + const goto_programt::const_targett t) const + { + using hash_typet = decltype(&(*t)); + return std::hash{}(&(*t)); + } +}; + +/// Functor to check whether iterators from different collections point at the +/// same object. +struct pointee_address_equalt +{ + template + bool operator()(const A &a, const B &b) const + { + return &(*a) == &(*b); + } +}; + #define forall_goto_program_instructions(it, program) \ for(goto_programt::instructionst::const_iterator \ it=(program).instructions.begin(); \ @@ -73,7 +706,7 @@ inline bool operator<( const goto_programt::const_targett &i1, const goto_programt::const_targett &i2) { - return order_const_target(i1, i2); + return order_const_target(i1, i2); } inline bool operator<( @@ -83,9 +716,6 @@ inline bool operator<( return &(*i1)<&(*i2); } -// NOLINTNEXTLINE(readability/identifiers) -typedef struct const_target_hash_templatet const_target_hash; - std::list objects_read(const goto_programt::instructiont &); std::list objects_written(const goto_programt::instructiont &); diff --git a/src/goto-programs/goto_program_template.cpp b/src/goto-programs/goto_program_template.cpp index 89b310c8d01..53dfafaf32a 100644 --- a/src/goto-programs/goto_program_template.cpp +++ b/src/goto-programs/goto_program_template.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Goto Program Template -#include "goto_program_template.h" +#include "goto_program.h" #include diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h deleted file mode 100644 index 852e380bc4a..00000000000 --- a/src/goto-programs/goto_program_template.h +++ /dev/null @@ -1,841 +0,0 @@ -/*******************************************************************\ - -Module: Goto Program Template - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Goto Program Template - -#ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H -#define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H - -#include -#include -#include -#include -#include -#include -#include - -#include -#include -#include -#include -#include - -/// The type of an instruction in a GOTO program. -enum goto_program_instruction_typet -{ - NO_INSTRUCTION_TYPE=0, - GOTO=1, // branch, possibly guarded - ASSUME=2, // non-failing guarded self loop - ASSERT=3, // assertions - OTHER=4, // anything else - SKIP=5, // just advance the PC - START_THREAD=6, // spawns an asynchronous thread - END_THREAD=7, // end the current thread - LOCATION=8, // semantically like SKIP - END_FUNCTION=9, // exit point of a function - ATOMIC_BEGIN=10, // marks a block without interleavings - ATOMIC_END=11, // end of a block without interleavings - RETURN=12, // set function return value (no control-flow change) - ASSIGN=13, // assignment lhs:=rhs - DECL=14, // declare a local variable - DEAD=15, // marks the end-of-live of a local variable - FUNCTION_CALL=16, // call a function - THROW=17, // throw an exception - CATCH=18 // push, pop or enter an exception handler -}; - -std::ostream &operator<<(std::ostream &, goto_program_instruction_typet); - -/// A generic container class for the GOTO intermediate representation of one -/// function. -/// -/// A function is represented by a std::list of instructions. Execution starts -/// in the first instruction of the list. Then, the execution of the i-th -/// instruction is followed by the execution of the (i+1)-th instruction unless -/// instruction i jumps to some other instruction in the list. See the internal -/// class instructiont for additional details -/// -/// Although it is straightforward to compute the control flow graph (CFG) of a -/// function from the list of instructions and the goto target locations in -/// instructions, the GOTO intermediate representation is _not_ regarded as the -/// CFG of a function. See instead the class cfg_baset, which is based on grapht -/// and allows for easier implementation of generic graph algorithms (e.g., -/// dominator analysis). -template -class goto_program_templatet -{ -public: - /// Copying is deleted as this class contains pointers that cannot be copied - goto_program_templatet(const goto_program_templatet &)=delete; - goto_program_templatet &operator=(const goto_program_templatet &)=delete; - - // Move operations need to be explicitly enabled as they are deleted with the - // copy operations - // default for move operations isn't available on Windows yet, so define - // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx - // under "Defaulted and Deleted Functions") - - goto_program_templatet(goto_program_templatet &&other): - instructions(std::move(other.instructions)) - { - } - - goto_program_templatet &operator=(goto_program_templatet &&other) - { - instructions=std::move(other.instructions); - return *this; - } - - /// This class represents an instruction in the GOTO intermediate - /// representation. Three fields are key: - /// - /// - type: an enum value describing the action performed by this instruction - /// - guard: an (arbitrarily complex) expression (usually an \ref exprt) of - /// Boolean type - /// - code: a code statement (usually a \ref codet) - /// - /// The meaning of an instruction node depends on the `type` field. Different - /// kinds of instructions make use of the fields `guard` and `code` for - /// different purposes. We list below, using a mixture of pseudo code and - /// plain English, the meaning of different kinds of instructions. - /// We use `guard`, `code`, and `targets` to mean the value of the - /// respective fields in this class: - /// - /// - GOTO: - /// if `guard` then goto `targets` - /// - RETURN: - /// Set the value returned by `code` (which shall be either nil or an - /// instance of code_returnt) and then jump to the end of the function. - /// - DECL: - /// Introduces a symbol denoted by the field `code` (an instance of - /// code_declt), the life-time of which is bounded by a corresponding DEAD - /// instruction. - /// - FUNCTION_CALL: - /// Invoke the function denoted by field `code` (an instance of - /// code_function_callt). - /// - ASSIGN: - /// Update the left-hand side of `code` (an instance of code_assignt) to - /// the value of the right-hand side. - /// - OTHER: - /// Execute the `code` (an instance of codet of kind ID_fence, ID_printf, - /// ID_array_copy, ID_array_set, ID_input, ID_output, ...). - /// - ASSUME: - /// Wait for `guard` to evaluate to true. - /// - ASSERT: - /// Using ASSERT instructions is the one and only way to express - /// properties to be verified. Execution paths abort if `guard` evaluates - /// to false. - /// - SKIP, LOCATION: - /// No-op. - /// - ATOMIC_BEGIN, ATOMIC_END: - /// When a thread executes ATOMIC_BEGIN, no thread other will be able to - /// execute any instruction until the same thread executes ATOMIC_END. - /// - END_FUNCTION: - /// Can only occur as the last instruction of the list. - /// - START_THREAD: - /// Create a new thread and run the code of this function starting from - /// targets[0]. Quite often the instruction pointed by targets[0] will be - /// just a FUNCTION_CALL, followed by an END_THREAD. - /// - END_THREAD: - /// Terminate the calling thread. - /// - THROW: - /// throw `exception1`, ..., `exceptionN` - /// where the list of exceptions is extracted from the `code` field - /// - CATCH, when code.find(ID_exception_list) is non-empty: - /// Establishes that from here to the next occurrence of CATCH with an - /// empty list (see below) if - /// - `exception1` is thrown, then goto `target1`, - /// - ... - /// - `exceptionN` is thrown, then goto `targetN`. - /// The list of exceptions is obtained from the `code` field and the list - /// of targets from the `targets` field. - /// - CATCH, when empty code.find(ID_exception_list) is empty: - /// clears all the catch clauses established as per the above in this - /// function? - class instructiont - { - public: - codeT code; - - /// The function this instruction belongs to - irep_idt function; - - /// The location of the instruction in the source file - source_locationt source_location; - - /// What kind of instruction? - goto_program_instruction_typet type; - - /// Guard for gotos, assume, assert - guardT guard; - - // The below will eventually become a single target only. - /// The target for gotos and for start_thread nodes - typedef typename std::list::iterator targett; - typedef typename std::list::const_iterator const_targett; - typedef std::list targetst; - typedef std::list const_targetst; - - /// The list of successor instructions - targetst targets; - - /// Returns the first (and only) successor for the usual case of a single - /// target - targett get_target() const - { - assert(targets.size()==1); - return targets.front(); - } - - /// Sets the first (and only) successor for the usual case of a single - /// target - void set_target(targett t) - { - targets.clear(); - targets.push_back(t); - } - - bool has_target() const - { - return !targets.empty(); - } - - /// Goto target labels - typedef std::list labelst; - labelst labels; - - // will go away - std::set incoming_edges; - - /// Is this node a branch target? - bool is_target() const - { return target_number!=nil_target; } - - /// Clear the node - void clear(goto_program_instruction_typet _type) - { - type=_type; - targets.clear(); - guard=true_exprt(); - code.make_nil(); - } - - void make_goto() { clear(GOTO); } - void make_return() { clear(RETURN); } - void make_skip() { clear(SKIP); } - void make_location(const source_locationt &l) - { clear(LOCATION); source_location=l; } - void make_throw() { clear(THROW); } - void make_catch() { clear(CATCH); } - void make_assertion(const guardT &g) { clear(ASSERT); guard=g; } - void make_assumption(const guardT &g) { clear(ASSUME); guard=g; } - void make_assignment() { clear(ASSIGN); } - void make_other(const codeT &_code) { clear(OTHER); code=_code; } - void make_decl() { clear(DECL); } - void make_dead() { clear(DEAD); } - void make_atomic_begin() { clear(ATOMIC_BEGIN); } - void make_atomic_end() { clear(ATOMIC_END); } - void make_end_function() { clear(END_FUNCTION); } - - void make_goto(targett _target) - { - make_goto(); - targets.push_back(_target); - } - - void make_goto(targett _target, const guardT &g) - { - make_goto(_target); - guard=g; - } - - void make_assignment(const codeT &_code) - { - clear(ASSIGN); - code=_code; - } - - void make_decl(const codeT &_code) - { - clear(DECL); - code=_code; - } - - void make_function_call(const codeT &_code) - { - clear(FUNCTION_CALL); - code=_code; - } - - bool is_goto () const { return type==GOTO; } - bool is_return () const { return type==RETURN; } - bool is_assign () const { return type==ASSIGN; } - bool is_function_call() const { return type==FUNCTION_CALL; } - bool is_throw () const { return type==THROW; } - bool is_catch () const { return type==CATCH; } - bool is_skip () const { return type==SKIP; } - bool is_location () const { return type==LOCATION; } - bool is_other () const { return type==OTHER; } - bool is_decl () const { return type==DECL; } - bool is_dead () const { return type==DEAD; } - bool is_assume () const { return type==ASSUME; } - bool is_assert () const { return type==ASSERT; } - bool is_atomic_begin () const { return type==ATOMIC_BEGIN; } - bool is_atomic_end () const { return type==ATOMIC_END; } - bool is_start_thread () const { return type==START_THREAD; } - bool is_end_thread () const { return type==END_THREAD; } - bool is_end_function () const { return type==END_FUNCTION; } - - instructiont(): - instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit) - { - } - - explicit instructiont(goto_program_instruction_typet _type): - source_location(static_cast(get_nil_irep())), - type(_type), - guard(true_exprt()), - location_number(0), - loop_number(0), - target_number(nil_target) - { - } - - /// Swap two instructions - void swap(instructiont &instruction) - { - using std::swap; - swap(instruction.code, code); - swap(instruction.source_location, source_location); - swap(instruction.type, type); - swap(instruction.guard, guard); - swap(instruction.targets, targets); - swap(instruction.function, function); - } - - #if (defined _MSC_VER && _MSC_VER <= 1800) - // Visual Studio <= 2013 does not support constexpr, making - // numeric_limits::max() unviable for a static const member - static const unsigned nil_target= - static_cast(-1); - #else - /// Uniquely identify an invalid target or location - static const unsigned nil_target= - std::numeric_limits::max(); - #endif - - /// A globally unique number to identify a program location. - /// It's guaranteed to be ordered in program order within - /// one goto_program. - unsigned location_number; - - /// Number unique per function to identify loops - unsigned loop_number; - - /// A number to identify branch targets. - /// This is \ref nil_target if it's not a target. - unsigned target_number; - - /// Returns true if the instruction is a backwards branch. - bool is_backwards_goto() const - { - if(!is_goto()) - return false; - - for(const auto &t : targets) - if(t->location_number<=location_number) - return true; - - return false; - } - - std::string to_string() const - { - std::ostringstream instruction_id_builder; - instruction_id_builder << type; - return instruction_id_builder.str(); - } - }; - - // Never try to change this to vector-we mutate the list while iterating - typedef std::list instructionst; - - typedef typename instructionst::iterator targett; - typedef typename instructionst::const_iterator const_targett; - typedef typename std::list targetst; - typedef typename std::list const_targetst; - - /// The list of instructions in the goto program - instructionst instructions; - - /// Convert a const_targett to a targett - use with care and avoid - /// whenever possible - targett const_cast_target(const_targett t) - { - return instructions.erase(t, t); - } - - /// Dummy for templates with possible const contexts - const_targett const_cast_target(const_targett t) const - { - return t; - } - - static const irep_idt get_function_id( - const goto_program_templatet &p) - { - PRECONDITION(!p.empty()); - - return p.instructions.back().function; - } - - template - std::list get_successors(Target target) const; - - void compute_incoming_edges(); - - /// Insertion that preserves jumps to "target". - void insert_before_swap(targett target) - { - assert(target!=instructions.end()); - const auto next=std::next(target); - instructions.insert(next, instructiont())->swap(*target); - } - - /// Insertion that preserves jumps to "target". - /// The instruction is destroyed. - void insert_before_swap(targett target, instructiont &instruction) - { - insert_before_swap(target); - target->swap(instruction); - } - - /// Insertion that preserves jumps to "target". - /// The program p is destroyed. - void insert_before_swap( - targett target, - goto_program_templatet &p) - { - assert(target!=instructions.end()); - if(p.instructions.empty()) - return; - insert_before_swap(target, p.instructions.front()); - auto next=std::next(target); - p.instructions.erase(p.instructions.begin()); - instructions.splice(next, p.instructions); - } - - /// Insertion before the given target - /// \return newly inserted location - targett insert_before(const_targett target) - { - return instructions.insert(target, instructiont()); - } - - /// Insertion after the given target - /// \return newly inserted location - targett insert_after(const_targett target) - { - return instructions.insert(std::next(target), instructiont()); - } - - /// Appends the given program, which is destroyed - void destructive_append(goto_program_templatet &p) - { - instructions.splice(instructions.end(), - p.instructions); - // BUG: The iterators to p-instructions are invalidated! - } - - /// Inserts the given program at the given location. - /// The program is destroyed. - void destructive_insert( - const_targett target, - goto_program_templatet &p) - { - instructions.splice(target, p.instructions); - // BUG: The iterators to p-instructions are invalidated! - } - - /// Adds an instruction at the end. - /// \return The newly added instruction. - targett add_instruction() - { - instructions.push_back(instructiont()); - return --instructions.end(); - } - - /// Adds an instruction of given type at the end. - /// \return The newly added instruction. - targett add_instruction(goto_program_instruction_typet type) - { - instructions.push_back(instructiont(type)); - return --instructions.end(); - } - - /// Output goto program to given stream - std::ostream &output( - const namespacet &ns, - const irep_idt &identifier, - std::ostream &out) const; - - /// Output goto-program to given stream - std::ostream &output(std::ostream &out) const - { - return output(namespacet(symbol_tablet()), "", out); - } - - /// Output a single instruction - virtual std::ostream &output_instruction( - const namespacet &ns, - const irep_idt &identifier, - std::ostream &out, - const typename instructionst::value_type &it) const = 0; - - /// Compute the target numbers - void compute_target_numbers(); - - /// Compute location numbers - void compute_location_numbers(unsigned &nr) - { - for(auto &i : instructions) - { - INVARIANT( - nr != std::numeric_limits::max(), - "Too many location numbers assigned"); - i.location_number=nr++; - } - } - - /// Sets the `function` member of each instruction if not yet set - /// Note that a goto program need not be a goto function and therefore, - /// we cannot do this in update(), but only at the level of - /// of goto_functionst where goto programs are guaranteed to be - /// named functions. - void update_instructions_function(const irep_idt &function_id) - { - for(auto &instruction : instructions) - { - if(instruction.function.empty()) - { - instruction.function = function_id; - } - } - } - - /// Compute location numbers - void compute_location_numbers() - { - unsigned nr=0; - compute_location_numbers(nr); - } - - /// Compute loop numbers - void compute_loop_numbers(); - - /// Update all indices - void update(); - - /// Human-readable loop name - static irep_idt loop_id(const instructiont &instruction) - { - return id2string(instruction.function)+"."+ - std::to_string(instruction.loop_number); - } - - /// Is the program empty? - bool empty() const - { - return instructions.empty(); - } - - /// Constructor - goto_program_templatet() - { - } - - virtual ~goto_program_templatet() - { - } - - /// Swap the goto program - void swap(goto_program_templatet &program) - { - program.instructions.swap(instructions); - } - - /// Clear the goto program - void clear() - { - instructions.clear(); - } - - targett get_end_function() - { - assert(!instructions.empty()); - const auto end_function=std::prev(instructions.end()); - assert(end_function->is_end_function()); - return end_function; - } - - /// Copy a full goto program, preserving targets - void copy_from(const goto_program_templatet &src); - - /// Does the goto program have an assertion? - bool has_assertion() const; -}; - -template -void goto_program_templatet::compute_loop_numbers() -{ - unsigned nr=0; - for(auto &i : instructions) - if(i.is_backwards_goto()) - i.loop_number=nr++; -} - -template -template -std::list goto_program_templatet::get_successors( - Target target) const -{ - if(target==instructions.end()) - return std::list(); - - const auto next=std::next(target); - - const instructiont &i=*target; - - if(i.is_goto()) - { - std::list successors(i.targets.begin(), i.targets.end()); - - if(!i.guard.is_true() && next!=instructions.end()) - successors.push_back(next); - - return successors; - } - - if(i.is_start_thread()) - { - std::list successors(i.targets.begin(), i.targets.end()); - - if(next!=instructions.end()) - successors.push_back(next); - - return successors; - } - - if(i.is_end_thread()) - { - // no successors - return std::list(); - } - - if(i.is_throw()) - { - // the successors are non-obvious - return std::list(); - } - - if(i.is_assume()) - { - return - !i.guard.is_false() && next!=instructions.end() ? - std::list{next} : - std::list(); - } - - if(next!=instructions.end()) - { - return std::list{next}; - } - - return std::list(); -} - -#include -#include - -template -void goto_program_templatet::update() -{ - compute_incoming_edges(); - compute_target_numbers(); - compute_location_numbers(); -} - -template -std::ostream &goto_program_templatet::output( - const namespacet &ns, - const irep_idt &identifier, - std::ostream &out) const -{ - // output program - - for(const auto &instruction : instructions) - output_instruction(ns, identifier, out, instruction); - - return out; -} - -template -void goto_program_templatet::compute_target_numbers() -{ - // reset marking - - for(auto &i : instructions) - i.target_number=instructiont::nil_target; - - // mark the goto targets - - for(const auto &i : instructions) - { - for(const auto &t : i.targets) - { - if(t!=instructions.end()) - t->target_number=0; - } - } - - // number the targets properly - unsigned cnt=0; - - for(auto &i : instructions) - { - if(i.is_target()) - { - i.target_number=++cnt; - assert(i.target_number!=0); - } - } - - // check the targets! - // (this is a consistency check only) - - for(const auto &i : instructions) - { - for(const auto &t : i.targets) - { - if(t!=instructions.end()) - { - assert(t->target_number!=0); - assert(t->target_number!=instructiont::nil_target); - } - } - } -} - -template -void goto_program_templatet::copy_from( - const goto_program_templatet &src) -{ - // Definitions for mapping between the two programs - typedef std::map targets_mappingt; - targets_mappingt targets_mapping; - - clear(); - - // Loop over program - 1st time collects targets and copy - - for(typename instructionst::const_iterator - it=src.instructions.begin(); - it!=src.instructions.end(); - ++it) - { - auto new_instruction=add_instruction(); - targets_mapping[it]=new_instruction; - *new_instruction=*it; - } - - // Loop over program - 2nd time updates targets - - for(auto &i : instructions) - { - for(auto &t : i.targets) - { - typename targets_mappingt::iterator - m_target_it=targets_mapping.find(t); - - if(m_target_it==targets_mapping.end()) - throw "copy_from: target not found"; - - t=m_target_it->second; - } - } - - compute_incoming_edges(); - compute_target_numbers(); -} - -// number them -template -bool goto_program_templatet::has_assertion() const -{ - for(const auto &i : instructions) - if(i.is_assert() && !i.guard.is_true()) - return true; - - return false; -} - -template -void goto_program_templatet::compute_incoming_edges() -{ - for(auto &i : instructions) - { - i.incoming_edges.clear(); - } - - for(typename instructionst::iterator - it=instructions.begin(); - it!=instructions.end(); - ++it) - { - for(const auto &s : get_successors(it)) - { - if(s!=instructions.end()) - s->incoming_edges.insert(it); - } - } -} - -template -inline bool order_const_target( - const typename goto_program_templatet::const_targett i1, - const typename goto_program_templatet::const_targett i2) -{ - const typename goto_program_templatet::instructiont &_i1=*i1; - const typename goto_program_templatet::instructiont &_i2=*i2; - return &_i1<&_i2; -} - -template -struct const_target_hash_templatet -{ - std::size_t operator()( - const typename goto_program_templatet::const_targett t) const - { - using hash_typet = decltype(&(*t)); - return std::hash{}(&(*t)); - } -}; - -/// Functor to check whether iterators from different collections point at the -/// same object. -struct pointee_address_equalt -{ - template - bool operator()(const A &a, const B &b) const - { - return &(*a) == &(*b); - } -}; - -#endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_TEMPLATE_H diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index e316b00ccba..0a089fc30c5 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -18,7 +18,9 @@ Author: Daniel Kroening #include #include -#include +#include + +#include "goto_program.h" void graphml_witnesst::remove_l0_l1(exprt &expr) { diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index b1c87a48039..43b291fa983 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + /// Reads a memory address and loads it into the `dest` variable. /// Marks cell as `READ_BEFORE_WRITTEN` if cell has never been written. void interpretert::read( diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index b2cc0b2e75a..a49772c859a 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -25,19 +25,18 @@ /// each program, in sequence, after it is converted. /// 3. Analyses will then access functions using the `at` function /// \tparam bodyt: The type of the function bodies, usually goto_programt -template class lazy_goto_functions_mapt final { public: // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL typedef irep_idt key_type; // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL - typedef goto_function_templatet &mapped_type; + typedef goto_functiont &mapped_type; /// The type of elements returned by const members // NOLINTNEXTLINE(readability/identifiers) - name matches mapped_type - typedef const goto_function_templatet &const_mapped_type; + typedef const goto_functiont &const_mapped_type; // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL - typedef std::pair> value_type; + typedef std::pair value_type; // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL typedef value_type &reference; // NOLINTNEXTLINE(readability/identifiers) - name matches those used in STL @@ -57,7 +56,7 @@ class lazy_goto_functions_mapt final post_process_functiont; private: - typedef std::map> underlying_mapt; + typedef std::map underlying_mapt; underlying_mapt &goto_functions; /// Names of functions that are already fully available in the programt state. /// \remarks These functions do not need processing before being returned @@ -151,7 +150,7 @@ class lazy_goto_functions_mapt final const key_type &name, symbol_table_baset &function_symbol_table) const { - typename underlying_mapt::iterator it=goto_functions.find(name); + underlying_mapt::iterator it=goto_functions.find(name); if(it!=goto_functions.end()) return *it; // Fill in symbol table entry body if not already done diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index 4419d994846..3888fda1d10 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -110,7 +110,7 @@ class lazy_goto_modelt : public can_produce_functiont symbol_tablet &symbol_table; private: - const lazy_goto_functions_mapt goto_functions; + const lazy_goto_functions_mapt goto_functions; language_filest language_files; // Function/module processing functions diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index b096016117d..2c5af45d24e 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -26,8 +26,9 @@ Author: Daniel Kroening, kroening@kroening.com #include -#ifdef DEBUG #include + +#ifdef DEBUG #include #endif diff --git a/unit/goto-programs/goto_trace_output.cpp b/unit/goto-programs/goto_trace_output.cpp index 2e9d43df63c..30eefe549a2 100644 --- a/unit/goto-programs/goto_trace_output.cpp +++ b/unit/goto-programs/goto_trace_output.cpp @@ -7,7 +7,7 @@ \*******************************************************************/ #include -#include +#include #include #include From 9c12abbc57cb39c2b8e14087a8bf6fe071de6597 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 19 Feb 2018 16:32:43 +0000 Subject: [PATCH 2/3] make linter happy --- src/goto-programs/goto_program.cpp | 17 +++++++++++------ src/goto-programs/goto_program.h | 14 ++++++++------ 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index f253c9ba1d2..a69432ce316 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -163,7 +163,8 @@ std::ostream &goto_programt::output_instruction( unsigned i=0; const irept::subt &exception_list= instruction.code.find(ID_exception_list).get_sub(); - assert(instruction.targets.size()==exception_list.size()); + DATA_INVARIANT(instruction.targets.size()==exception_list.size(), + "size of target list"); for(instructiont::targetst::const_iterator gt_it=instruction.targets.begin(); gt_it!=instruction.targets.end(); @@ -220,8 +221,10 @@ void goto_programt::get_decl_identifiers( { if(it->is_decl()) { - assert(it->code.get_statement()==ID_decl); - assert(it->code.operands().size()==1); + DATA_INVARIANT(it->code.get_statement()==ID_decl, + "declaration statements"); + DATA_INVARIANT(it->code.operands().size()==1, + "operand of declaration statement"); const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0()); decl_identifiers.insert(symbol_expr.get_identifier()); } @@ -539,7 +542,7 @@ void goto_programt::compute_target_numbers() if(i.is_target()) { i.target_number=++cnt; - assert(i.target_number!=0); + DATA_INVARIANT(i.target_number!=0, "target numbers"); } } @@ -552,8 +555,10 @@ void goto_programt::compute_target_numbers() { if(t!=instructions.end()) { - assert(t->target_number!=0); - assert(t->target_number!=instructiont::nil_target); + DATA_INVARIANT(t->target_number!=0, + "target numbers"); + DATA_INVARIANT(t->target_number!=instructiont::nil_target, + "target numbers"); } } } diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index ad5d2d6254f..ebb77a46eae 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -188,7 +188,7 @@ class goto_programt /// target targett get_target() const { - assert(targets.size()==1); + PRECONDITION(targets.size()==1); return targets.front(); } @@ -398,7 +398,7 @@ class goto_programt static const irep_idt get_function_id( const goto_programt &p) { - assert(!p.empty()); + PRECONDITION(!p.empty()); return get_function_id(--p.instructions.end()); } @@ -411,7 +411,7 @@ class goto_programt /// Insertion that preserves jumps to "target". void insert_before_swap(targett target) { - assert(target!=instructions.end()); + PRECONDITION(target!=instructions.end()); const auto next=std::next(target); instructions.insert(next, instructiont())->swap(*target); } @@ -430,7 +430,7 @@ class goto_programt targett target, goto_programt &p) { - assert(target!=instructions.end()); + PRECONDITION(target!=instructions.end()); if(p.instructions.empty()) return; insert_before_swap(target, p.instructions.front()); @@ -586,9 +586,10 @@ class goto_programt targett get_end_function() { - assert(!instructions.empty()); + PRECONDITION(!instructions.empty()); const auto end_function=std::prev(instructions.end()); - assert(end_function->is_end_function()); + DATA_INVARIANT(end_function->is_end_function(), + "goto program ends on END_FUNCTION"); return end_function; } @@ -671,6 +672,7 @@ inline bool order_const_target( return &_i1<&_i2; } +// NOLINTNEXTLINE(readability/identifiers) struct const_target_hash { std::size_t operator()( From d82c58601d885afb2318b10424582b0c85272491 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 20 Feb 2018 10:14:52 +0000 Subject: [PATCH 3/3] missing header for std::time_t --- src/cbmc/symex_coverage.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index 43f431a5ae8..fec36dd1f5f 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/src/cbmc/symex_coverage.cpp @@ -13,6 +13,7 @@ Date: March 2016 #include "symex_coverage.h" +#include #include #include #include