Skip to content

Stop inheriting from std containers #919

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 14 commits into from
Aug 30, 2017
Merged
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
58 changes: 50 additions & 8 deletions src/analyses/goto_rw.h
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,14 @@ void goto_rw(const goto_functionst &goto_functions,
class range_domain_baset
{
public:
range_domain_baset()=default;

range_domain_baset(const range_domain_baset &rhs)=delete;
range_domain_baset &operator=(const range_domain_baset &rhs)=delete;

range_domain_baset(range_domain_baset &&rhs)=delete;
range_domain_baset &operator=(range_domain_baset &&rhs)=delete;

virtual ~range_domain_baset();

virtual void output(const namespacet &ns, std::ostream &out) const=0;
Expand All @@ -61,12 +69,29 @@ inline range_spect to_range_spect(const mp_integer &size)
}

// each element x represents a range of bits [x.first, x.second.first)
class range_domaint:
public range_domain_baset,
public std::list<std::pair<range_spect, range_spect> >
class range_domaint:public range_domain_baset
{
typedef std::list<std::pair<range_spect, range_spect>> sub_typet;
sub_typet data;

public:
virtual void output(const namespacet &ns, std::ostream &out) const;
void output(const namespacet &ns, std::ostream &out) const override;

// NOLINTNEXTLINE(readability/identifiers)
typedef sub_typet::iterator iterator;
// NOLINTNEXTLINE(readability/identifiers)
typedef sub_typet::const_iterator const_iterator;

iterator begin() { return data.begin(); }
const_iterator begin() const { return data.begin(); }
const_iterator cbegin() const { return data.begin(); }

iterator end() { return data.end(); }
const_iterator end() const { return data.end(); }
const_iterator cend() const { return data.end(); }

template <typename T>
void push_back(T &&v) { data.push_back(std::forward<T>(v)); }
};

class array_exprt;
Expand Down Expand Up @@ -257,12 +282,29 @@ class rw_range_set_value_sett:public rw_range_sett
const range_spect &size);
};

class guarded_range_domaint:
public range_domain_baset,
public std::multimap<range_spect, std::pair<range_spect, exprt> >
class guarded_range_domaint:public range_domain_baset
{
typedef std::multimap<range_spect, std::pair<range_spect, exprt>> sub_typet;
sub_typet data;

public:
virtual void output(const namespacet &ns, std::ostream &out) const;
virtual void output(const namespacet &ns, std::ostream &out) const override;

// NOLINTNEXTLINE(readability/identifiers)
typedef sub_typet::iterator iterator;
// NOLINTNEXTLINE(readability/identifiers)
typedef sub_typet::const_iterator const_iterator;

iterator begin() { return data.begin(); }
const_iterator begin() const { return data.begin(); }
const_iterator cbegin() const { return data.begin(); }

iterator end() { return data.end(); }
const_iterator end() const { return data.end(); }
const_iterator cend() const { return data.end(); }

template<typename T>
iterator insert(T &&v) { return data.insert(std::forward<T>(v)); }
};

class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
Expand Down
36 changes: 17 additions & 19 deletions src/analyses/local_bitvector_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -41,16 +41,16 @@ void local_bitvector_analysist::flagst::print(std::ostream &out) const
out << "+integer_address";
}

bool local_bitvector_analysist::loc_infot::merge(const loc_infot &src)
bool local_bitvector_analysist::merge(points_tot &a, points_tot &b)
{
bool result=false;

std::size_t max_index=
std::max(src.points_to.size(), points_to.size());
std::max(a.size(), b.size());

for(std::size_t i=0; i<max_index; i++)
{
if(points_to[i].merge(src.points_to[i]))
if(a[i].merge(b[i]))
result=true;
}

Expand All @@ -72,8 +72,8 @@ bool local_bitvector_analysist::is_tracked(const irep_idt &identifier)
void local_bitvector_analysist::assign_lhs(
const exprt &lhs,
const exprt &rhs,
const loc_infot &loc_info_src,
loc_infot &loc_info_dest)
points_tot &loc_info_src,
points_tot &loc_info_dest)
{
if(lhs.id()==ID_symbol)
{
Expand All @@ -83,7 +83,7 @@ void local_bitvector_analysist::assign_lhs(
{
unsigned dest_pointer=pointers.number(identifier);
flagst rhs_flags=get_rec(rhs, loc_info_src);
loc_info_dest.points_to[dest_pointer]=rhs_flags;
loc_info_dest[dest_pointer]=rhs_flags;
}
}
else if(lhs.id()==ID_dereference)
Expand Down Expand Up @@ -117,14 +117,12 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get(

assert(loc_it!=cfg.loc_map.end());

const loc_infot &loc_info_src=loc_infos[loc_it->second];

return get_rec(rhs, loc_info_src);
return get_rec(rhs, loc_infos[loc_it->second]);
}

local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
const exprt &rhs,
const loc_infot &loc_info_src)
points_tot &loc_info_src)
{
if(rhs.id()==ID_constant)
{
Expand All @@ -139,7 +137,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
if(is_tracked(identifier))
{
unsigned src_pointer=pointers.number(identifier);
return loc_info_src.points_to[src_pointer];
return loc_info_src[src_pointer];
}
else
return flagst::mk_unknown();
Expand Down Expand Up @@ -258,7 +256,7 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
// in the entry location.
for(const auto &local : locals.locals_map)
if(is_tracked(local.first))
loc_infos[0].points_to[pointers.number(local.first)]=flagst::mk_unknown();
loc_infos[0][pointers.number(local.first)]=flagst::mk_unknown();

while(!work_queue.empty())
{
Expand All @@ -267,8 +265,8 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
const goto_programt::instructiont &instruction=*node.t;
work_queue.pop();

const loc_infot &loc_info_src=loc_infos[loc_nr];
loc_infot loc_info_dest=loc_infos[loc_nr];
auto &loc_info_src=loc_infos[loc_nr];
auto loc_info_dest=loc_infos[loc_nr];

switch(instruction.type)
{
Expand Down Expand Up @@ -320,7 +318,7 @@ void local_bitvector_analysist::build(const goto_functiont &goto_function)
for(const auto &succ : node.successors)
{
assert(succ<loc_infos.size());
if(loc_infos[succ].merge(loc_info_dest))
if(merge(loc_infos[succ], (loc_info_dest)))
work_queue.push(succ);
}
}
Expand All @@ -337,14 +335,14 @@ void local_bitvector_analysist::output(
{
out << "**** " << i_it->source_location << "\n";

const loc_infot &loc_info=loc_infos[l];
const auto &loc_info=loc_infos[l];

for(points_tot::const_iterator
p_it=loc_info.points_to.begin();
p_it!=loc_info.points_to.end();
p_it=loc_info.begin();
p_it!=loc_info.end();
p_it++)
{
out << " " << pointers[p_it-loc_info.points_to.begin()]
out << " " << pointers[p_it-loc_info.begin()]
<< ": "
<< *p_it
<< "\n";
Expand Down
17 changes: 5 additions & 12 deletions src/analyses/local_bitvector_analysis.h
Original file line number Diff line number Diff line change
Expand Up @@ -186,27 +186,20 @@ class local_bitvector_analysist
// This is a vector, so it's fast.
typedef expanding_vectort<flagst> points_tot;

// the information tracked per program location
class loc_infot
{
public:
points_tot points_to;

bool merge(const loc_infot &src);
};
static bool merge(points_tot &a, points_tot &b);

typedef std::vector<loc_infot> loc_infost;
typedef std::vector<points_tot> loc_infost;
loc_infost loc_infos;

void assign_lhs(
const exprt &lhs,
const exprt &rhs,
const loc_infot &loc_info_src,
loc_infot &loc_info_dest);
points_tot &loc_info_src,
points_tot &loc_info_dest);

flagst get_rec(
const exprt &rhs,
const loc_infot &loc_info_src);
points_tot &loc_info_src);

bool is_tracked(const irep_idt &identifier);
};
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/wmm/cycle_collection.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ void event_grapht::graph_explorert::filter_thin_air(
{
std::set<critical_cyclet>::const_iterator next=it;
++next;
critical_cyclet::const_iterator e_it=it->begin();
auto e_it=it->begin();
/* is there an event in the cycle not in thin-air events? */
for(; e_it!=it->end(); ++e_it)
if(thin_air_events.find(*e_it)==thin_air_events.end())
Expand Down
45 changes: 23 additions & 22 deletions src/goto-instrument/wmm/data_dp.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ Date: 2012

#include "data_dp.h"

#include <util/invariant.h>
#include <util/message.h>

#include "abstract_event.h"
Expand All @@ -24,13 +25,13 @@ void data_dpt::dp_analysis(
const datat &write,
bool local_write)
{
const_iterator it;
data_typet::const_iterator it;

for(it=begin(); it!=end(); ++it)
for(it=data.cbegin(); it!=data.cend(); ++it)
{
if(local_read && it->id==read.id)
{
insert(
data.insert(
datat(
write.id,
(local_write?source_locationt():write.loc),
Expand All @@ -40,7 +41,7 @@ void data_dpt::dp_analysis(

if(local_write && it->id==write.id)
{
insert(
data.insert(
datat(
read.id,
(local_read?source_locationt():read.loc),
Expand All @@ -49,12 +50,12 @@ void data_dpt::dp_analysis(
}
}

if(it==end())
if(it==data.cend())
{
++class_nb;
insert(
data.insert(
datat(read.id, (local_read?source_locationt():read.loc), class_nb));
insert(
data.insert(
datat(write.id, (local_write?source_locationt():write.loc), class_nb));
}
}
Expand All @@ -71,11 +72,11 @@ void data_dpt::dp_analysis(
/// search in N^2
bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
{
for(const_iterator it1=begin(); it1!=end(); ++it1)
for(auto it1=data.cbegin(); it1!=data.cend(); ++it1)
{
const_iterator it2=it1;
auto it2=it1;
++it2;
if(it2==end())
if(it2==data.cend())
break;

if(e1.local)
Expand All @@ -89,7 +90,7 @@ bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
continue;
}

for(; it2!=end(); ++it2)
for(; it2!=data.cend(); ++it2)
{
if(e2.local)
{
Expand All @@ -116,42 +117,42 @@ bool data_dpt::dp(const abstract_eventt &e1, const abstract_eventt &e2) const
/// merge in N^3
void data_dpt::dp_merge()
{
if(size()<2)
if(data.size()<2)
return;

unsigned initial_size=size();
unsigned initial_size=data.size();

unsigned from=0;
unsigned to=0;

/* look for similar elements */
for(const_iterator it1=begin(); it1!=end(); ++it1)
for(auto it1=data.cbegin(); it1!=data.cend(); ++it1)
{
const_iterator it2=it1;
auto it2=it1;
++it2;
/* all ok -- ends */
if(it2==end())
if(it2==data.cend())
return;

for(; it2!=end(); ++it2)
for(; it2!=data.cend(); ++it2)
{
if(it1 == it2)
{
from=it2->eq_class;
to=it1->eq_class;
erase(it2);
data.erase(it2);
break;
}
}
}

/* merge */
for(iterator it3=begin(); it3!=end(); ++it3)
for(auto it3=data.begin(); it3!=data.end(); ++it3)
if(it3->eq_class==from)
it3->eq_class=to;

/* strictly monotonous => converges */
assert(initial_size>size());
INVARIANT(initial_size>data.size(), "strictly monotonous => converges");

/* repeat until classes are disjunct */
dp_merge();
Expand All @@ -160,10 +161,10 @@ void data_dpt::dp_merge()
void data_dpt::print(messaget &message)
{
#ifdef DEBUG
const_iterator it;
data_typet::const_iterator it;
std::map<unsigned, std::set<source_locationt> > classed;

for(it=begin(); it!=end(); ++it)
for(it=data.cbegin(); it!=data.cend(); ++it)
{
if(classed.find(it->eq_class)==classed.end())
{
Expand Down
6 changes: 4 additions & 2 deletions src/goto-instrument/wmm/data_dp.h
Original file line number Diff line number Diff line change
Expand Up @@ -48,11 +48,13 @@ struct datat
}
};

class data_dpt:public std::set<datat>
class data_dpt final
{
public:
typedef std::set<datat> data_typet;
data_typet data;
unsigned class_nb;

public:
/* add this dependency in the structure */
void dp_analysis(const abstract_eventt &read, const abstract_eventt &write);
void dp_analysis(
Expand Down
Loading