Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 7 additions & 3 deletions jbmc/src/java_bytecode/java_local_variable_table.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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());

Expand Down
149 changes: 110 additions & 39 deletions src/analyses/cfg_dominators.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,17 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
#ifndef CPROVER_ANALYSES_CFG_DOMINATORS_H
#define CPROVER_ANALYSES_CFG_DOMINATORS_H

#include <set>
#include <list>
#include <map>
#include <iosfwd>
#include <util/sharing_map.h>

#include <goto-programs/cfg.h>
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_program.h>
#include <goto-programs/cfg.h>

#include <algorithm>
#include <iosfwd>
#include <list>
#include <map>
#include <vector>
Comment on lines +21 to +25

/// Dominator graph. This computes a control-flow graph (see \ref cfgt) and
/// decorates it with dominator sets per program point, following
Expand All @@ -36,7 +39,97 @@ template <class P, class T, bool post_dom>
class cfg_dominators_templatet
{
public:
typedef std::set<T, typename P::target_less_than> 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<void(const T &)> 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<T> 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 U = T>
typename std::enable_if<std::is_integral<U>::value, std::size_t>::type
operator()(const U &t) const
{
return std::hash<U>{}(t);
}

template <typename U = T>
typename std::enable_if<!std::is_integral<U>::value, std::size_t>::type
operator()(const U &t) const
{
return std::hash<const void *>{}(&*t);
}
};

typedef sharing_mapt<T, unitt, false, target_hasht> mapt;

mapt map;
};

struct nodet
{
Expand Down Expand Up @@ -210,38 +303,7 @@ void cfg_dominators_templatet<P, T, post_dom>::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?
Expand Down Expand Up @@ -284,8 +346,17 @@ void cfg_dominators_templatet<P, T, post_dom>::output(std::ostream &out) const
out << " post-dominated by ";
else
out << " dominated by ";

std::vector<T> 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 << ", ";
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/dependence_graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
13 changes: 12 additions & 1 deletion src/analyses/sese_regions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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<goto_programt::const_targett> sorted_postdoms;
instruction_postdoms.for_each(
[&sorted_postdoms](const goto_programt::const_targett &d)
Comment on lines +149 to +153
{ sorted_postdoms.push_back(d); });
std::sort(
sorted_postdoms.begin(),
sorted_postdoms.end(),
goto_programt::target_less_than{});

// Ideally I would use `std::optional<std::size_t>` 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];
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
22 changes: 15 additions & 7 deletions src/goto-instrument/full_slicer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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<goto_programt::const_targett> sorted_dominators;
j_PC_node.dominators.for_each(
Comment on lines +158 to +162
[&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();
}
}
Expand Down
Loading