diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index d3822c3abed..7e542b52f28 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -467,9 +467,13 @@ static java_bytecode_convert_methodt::method_offsett get_common_dominator( dominator_analysis.cfg.entry_map.at(v->var.start_pc); const auto &this_var_doms= dominator_analysis.cfg[dominator_nodeidx].dominators; - for(const auto this_var_dom : this_var_doms) - if(this_var_dom<=first_pc) - candidate_dominators.push_back(this_var_dom); + this_var_doms.for_each( + [&candidate_dominators, first_pc]( + const java_bytecode_convert_methodt::method_offsett &this_var_dom) + { + if(this_var_dom <= first_pc) + candidate_dominators.push_back(this_var_dom); + }); } std::sort(candidate_dominators.begin(), candidate_dominators.end()); diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h index 6114ea90f82..3008fe8fa11 100644 --- a/src/analyses/cfg_dominators.h +++ b/src/analyses/cfg_dominators.h @@ -12,14 +12,17 @@ Author: Georg Weissenbacher, georg@weissenbacher.name #ifndef CPROVER_ANALYSES_CFG_DOMINATORS_H #define CPROVER_ANALYSES_CFG_DOMINATORS_H -#include -#include -#include -#include +#include +#include #include #include -#include + +#include +#include +#include +#include +#include /// Dominator graph. This computes a control-flow graph (see \ref cfgt) and /// decorates it with dominator sets per program point, following @@ -36,7 +39,97 @@ template class cfg_dominators_templatet { public: - typedef std::set target_sett; + /// Set of program points, backed by a copy-on-write sharing map so that + /// similar sets share most of their representation. Dominator sets of + /// adjacent program points typically differ in just a single element, so + /// the sharing keeps the total memory linear-ish in the program size, where + /// explicit per-node `std::set`s are worst-case quadratic (a straight-line + /// program of N instructions has dominator sets of total size N^2/2, which + /// for machine-generated functions with ~100k instructions exhausts tens of + /// gigabytes of memory). + class target_sett + { + public: + bool empty() const + { + return map.empty(); + } + + std::size_t size() const + { + return map.size(); + } + + std::size_t count(const T &t) const + { + return map.has_key(t) ? 1 : 0; + } + + void insert(const T &t) + { + if(!map.has_key(t)) + map.insert(t, unitt{}); + } + + /// Invoke \p f for each element of the set, in no particular order. + void for_each(std::function f) const + { + map.iterate([&f](const T &k, const unitt &) { f(k); }); + } + + /// Remove all elements that are not also contained in \p other, except + /// that \p keep is always retained. Return true if any element was + /// removed. The delta view used here only visits elements in subtrees + /// that are not shared between the two maps, so intersecting largely + /// overlapping sets is much cheaper than element-wise iteration. + bool intersect_with(const target_sett &other, const T &keep) + { + typename mapt::delta_viewt delta_view; + map.get_delta_view(other.map, delta_view, false); + + std::vector to_erase; + for(const auto &delta_item : delta_view) + { + if(!delta_item.is_in_both_maps() && !(delta_item.k == keep)) + to_erase.push_back(delta_item.k); + } + + for(const auto &item : to_erase) + map.erase(item); + + return !to_erase.empty(); + } + + protected: + struct unitt + { + }; + + struct target_hasht + { + /// Program-point hash: program points are either integral (e.g. Java + /// bytecode offsets) or iterator-like (e.g. goto-program targets), so + /// hash the value itself or the address of the object it refers to, + /// respectively. + template + typename std::enable_if::value, std::size_t>::type + operator()(const U &t) const + { + return std::hash{}(t); + } + + template + typename std::enable_if::value, std::size_t>::type + operator()(const U &t) const + { + return std::hash{}(&*t); + } + }; + + typedef sharing_mapt mapt; + + mapt map; + }; struct nodet { @@ -210,38 +303,7 @@ void cfg_dominators_templatet::fixedpoint(P &program) if(other.empty()) continue; - typename target_sett::const_iterator n_it=node.dominators.begin(); - typename target_sett::const_iterator o_it=other.begin(); - - // in-place intersection. not safe to use set_intersect - while(n_it!=node.dominators.end() && o_it!=other.end()) - { - if(*n_it==current) - ++n_it; - else if(typename P::target_less_than()(*n_it, *o_it)) - { - changed=true; - node.dominators.erase(n_it++); - } - else if(typename P::target_less_than()(*o_it, *n_it)) - ++o_it; - else - { - ++n_it; - ++o_it; - } - } - - while(n_it!=node.dominators.end()) - { - if(*n_it==current) - ++n_it; - else - { - changed=true; - node.dominators.erase(n_it++); - } - } + changed |= node.dominators.intersect_with(other, current); } if(changed) // fixed point for node reached? @@ -284,8 +346,17 @@ void cfg_dominators_templatet::output(std::ostream &out) const out << " post-dominated by "; else out << " dominated by "; + + std::vector sorted_dominators; + cfg[node.second].dominators.for_each([&sorted_dominators](const T &d) + { sorted_dominators.push_back(d); }); + std::sort( + sorted_dominators.begin(), + sorted_dominators.end(), + typename P::target_less_than{}); + bool first=true; - for(const auto &d : cfg[node.second].dominators) + for(const auto &d : sorted_dominators) { if(!first) out << ", "; diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index efb7c6ae8fc..dffa26d60bd 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -107,7 +107,7 @@ void dep_graph_domaint::control_dependencies( const cfg_post_dominatorst::cfgt::nodet &m_s= pd.cfg[edge.first]; - if(m_s.dominators.find(to)!=m_s.dominators.end()) + if(m_s.dominators.count(to) != 0) post_dom_one=true; else post_dom_all=false; diff --git a/src/analyses/sese_regions.cpp b/src/analyses/sese_regions.cpp index 240d5667845..d64a6f07d5a 100644 --- a/src/analyses/sese_regions.cpp +++ b/src/analyses/sese_regions.cpp @@ -146,10 +146,21 @@ void sese_region_analysist::compute_sese_regions( // but our current dominator analysis doesn't make it easy to determine an // immediate dominator. + // Iterate in a deterministic (location-number) order, since ties on the + // dominator-set size below are broken by iteration order. + std::vector sorted_postdoms; + instruction_postdoms.for_each( + [&sorted_postdoms](const goto_programt::const_targett &d) + { sorted_postdoms.push_back(d); }); + std::sort( + sorted_postdoms.begin(), + sorted_postdoms.end(), + goto_programt::target_less_than{}); + // Ideally I would use `std::optional` here, but it triggers a // GCC-5 bug. std::size_t closest_exit_index = dominators.cfg.size(); - for(const auto &possible_exit : instruction_postdoms) + for(const auto &possible_exit : sorted_postdoms) { const auto possible_exit_index = dominators.get_node_index(possible_exit); const auto &possible_exit_node = dominators.cfg[possible_exit_index]; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp index 80afe243632..8a18ed15ed2 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp @@ -272,7 +272,7 @@ void variable_sensitivity_dependence_domaint::control_dependencies( { const cfg_post_dominatorst::cfgt::nodet &m_s = pd.cfg[edge.first]; - if(m_s.dominators.find(to) != m_s.dominators.end()) + if(m_s.dominators.count(to) != 0) post_dom_one = true; else post_dom_all = false; diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 736864cdc9d..2e661ec2365 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -155,23 +155,31 @@ void full_slicert::add_jumps( // lex_succ goto_programt::const_targett nearest=lex_succ; std::size_t post_dom_size=0; - for(cfg_dominatorst::target_sett::const_iterator d_it = - j_PC_node.dominators.begin(); - d_it != j_PC_node.dominators.end(); - ++d_it) + // Iterate over the dominators in a deterministic (location-number) + // order, since ties on `post_dom_size` below are broken by iteration + // order. + std::vector sorted_dominators; + j_PC_node.dominators.for_each( + [&sorted_dominators](const goto_programt::const_targett &dominator) + { sorted_dominators.push_back(dominator); }); + std::sort( + sorted_dominators.begin(), + sorted_dominators.end(), + goto_programt::target_less_than{}); + for(const auto &dominator : sorted_dominators) { - const auto &node = cfg.get_node(*d_it); + const auto &node = cfg.get_node(dominator); if(node.node_required) { const irep_idt &id2 = node.function_id; INVARIANT(id==id2, "goto/jump expected to be within a single function"); - const auto &postdom_node = pd.get_node(*d_it); + const auto &postdom_node = pd.get_node(dominator); if(postdom_node.dominators.size() > post_dom_size) { - nearest=*d_it; + nearest = dominator; post_dom_size = postdom_node.dominators.size(); } }