Skip to content

Use numeric limits instead of (unsigned)-1 #332

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.

Sign up for GitHub

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 3 commits into from
Jan 5, 2017
Merged

Use numeric limits instead of (unsigned)-1 #332

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
654e5ef
Added constant nil_target to identify an invalid location number
tautschnig Dec 15, 2016
2da51e7
Typedef wmm_grapht instead of repeating template instantiation
tautschnig Dec 15, 2016
4ee0c97
wmm/musketeer: Use wmm_grapht::node_indext instead of unsigned
tautschnig Dec 15, 2016
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
6 changes: 3 additions & 3 deletions src/goto-instrument/wmm/cycle_collection.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -393,7 +393,7 @@ bool event_grapht::graph_explorert::backtrack(
if(!get_com_only)
{
/* we first visit via po transition, if existing */
for(graph<abstract_eventt>::edgest::const_iterator
for(wmm_grapht::edgest::const_iterator
w_it=egraph.po_out(vertex).begin();
w_it!=egraph.po_out(vertex).end(); w_it++)
{
Expand Down Expand Up @@ -436,7 +436,7 @@ bool event_grapht::graph_explorert::backtrack(

if(!no_comm)
/* we then visit via com transitions, if existing */
for(graph<abstract_eventt>::edgest::const_iterator
for(wmm_grapht::edgest::const_iterator
w_it=egraph.com_out(vertex).begin();
w_it!=egraph.com_out(vertex).end(); w_it++)
{
Expand Down Expand Up @@ -568,7 +568,7 @@ bool event_grapht::graph_explorert::backtrack(
(!this_vertex.WRfence
&& egraph[point_stack.top()].operation==abstract_eventt::Write));

for(graph<abstract_eventt>::edgest::const_iterator w_it=
for(wmm_grapht::edgest::const_iterator w_it=
egraph.po_out(vertex).begin();
w_it!=egraph.po_out(vertex).end(); w_it++)
{
Expand Down
48 changes: 24 additions & 24 deletions src/goto-instrument/wmm/event_graph.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,15 +34,15 @@ Function: event_grapht::print_rec_graph

\*******************************************************************/

void event_grapht::print_rec_graph(std::ofstream& file, unsigned node_id,
std::set<unsigned>& visited)
void event_grapht::print_rec_graph(std::ofstream& file, event_idt node_id,
std::set<event_idt>& visited)
{
const abstract_eventt& node=operator[](node_id);
file << node_id << "[label=\"" << node << ", " << node.source_location <<
"\"];" << std::endl;
visited.insert(node_id);

for(graph<abstract_eventt>::edgest::const_iterator
for(wmm_grapht::edgest::const_iterator
it=po_out(node_id).begin();
it!=po_out(node_id).end(); ++it)
{
Expand All @@ -52,7 +52,7 @@ void event_grapht::print_rec_graph(std::ofstream& file, unsigned node_id,
print_rec_graph(file, it->first, visited);
}

for(graph<abstract_eventt>::edgest::const_iterator
for(wmm_grapht::edgest::const_iterator
it=com_out(node_id).begin();
it!=com_out(node_id).end(); ++it)
{
Expand All @@ -76,8 +76,8 @@ Function: event_grapht::print_graph

void event_grapht::print_graph() {
assert(po_order.size()>0);
std::set<unsigned> visited;
unsigned root=po_order.front();
std::set<event_idt> visited;
event_idt root=po_order.front();
std::ofstream file;
file.open("graph.dot");
file << "digraph G {" << std::endl;
Expand All @@ -99,8 +99,8 @@ Function: event_grapht::copy_segment

\*******************************************************************/

void event_grapht::explore_copy_segment(std::set<unsigned>& explored,
unsigned begin, unsigned end) const
void event_grapht::explore_copy_segment(std::set<event_idt>& explored,
event_idt begin, event_idt end) const
{
//std::cout << "explores " << begin << " against " << end << std::endl;
if(explored.find(begin)!=explored.end())
Expand All @@ -111,13 +111,13 @@ void event_grapht::explore_copy_segment(std::set<unsigned>& explored,
if(begin==end)
return;

for(graph<abstract_eventt>::edgest::const_iterator it=po_out(begin).begin();
for(wmm_grapht::edgest::const_iterator it=po_out(begin).begin();
it!=po_out(begin).end();
++it)
explore_copy_segment(explored, it->first, end);
}

unsigned event_grapht::copy_segment(unsigned begin, unsigned end)
event_idt event_grapht::copy_segment(event_idt begin, event_idt end)
{
const abstract_eventt& begin_event=operator[](begin);
const abstract_eventt& end_event=operator[](end);
Expand All @@ -137,25 +137,25 @@ unsigned event_grapht::copy_segment(unsigned begin, unsigned end)

message.status() << "tries to duplicate between " << begin_event.source_location
<< " and " << end_event.source_location << messaget::eom;
std::set<unsigned> covered;
std::set<event_idt> covered;

/* collects the nodes of the subgraph */
explore_copy_segment(covered, begin, end);

if(covered.size()==0)
return end;

// for(std::set<unsigned>::const_iterator it=covered.begin(); it!=covered.end(); ++it)
// for(std::set<event_idt>::const_iterator it=covered.begin(); it!=covered.end(); ++it)
// std::cout << "covered: " << *it << std::endl;

std::map<unsigned, unsigned> orig2copy;
std::map<event_idt, event_idt> orig2copy;

/* duplicates nodes */
for(std::set<unsigned>::const_iterator it=covered.begin();
for(std::set<event_idt>::const_iterator it=covered.begin();
it!=covered.end();
++it)
{
const unsigned new_node=add_node();
const event_idt new_node=add_node();
operator[](new_node)(operator[](*it));
orig2copy[*it]=new_node;
}
Expand All @@ -165,11 +165,11 @@ unsigned event_grapht::copy_segment(unsigned begin, unsigned end)
// (working on back-edges...)

/* replicates the po_s forward-edges -- O(#E^2) */
for(std::set<unsigned>::const_iterator it_i=covered.begin();
for(std::set<event_idt>::const_iterator it_i=covered.begin();
it_i!=covered.end();
++it_i)
{
for(std::set<unsigned>::const_iterator it_j=covered.begin();
for(std::set<event_idt>::const_iterator it_j=covered.begin();
it_j!=covered.end();
++it_j)
{
Expand All @@ -187,11 +187,11 @@ unsigned event_grapht::copy_segment(unsigned begin, unsigned end)

// TODO: to move to goto2graph, after po_s construction
/* replicates the cmp-edges -- O(#E x #G) */
for(std::set<unsigned>::const_iterator it_i=covered.begin();
for(std::set<event_idt>::const_iterator it_i=covered.begin();
it_i!=covered.end();
++it_i)
{
for(unsigned it_j=0;
for(event_idt it_j=0;
it_j<size();
++it_j)
{
Expand Down Expand Up @@ -547,8 +547,8 @@ bool event_grapht::critical_cyclet::is_unsafe(memory_modelt model, bool fast)
if(first.unsafe_pair(second,model)
&& (first.thread!=second.thread || egraph.are_po_ordered(back(),*s_it)))
{
std::list<unsigned>::const_iterator before_first;
std::list<unsigned>::const_iterator after_second;
std::list<event_idt>::const_iterator before_first;
std::list<event_idt>::const_iterator after_second;

before_first = end();
--before_first;
Expand Down Expand Up @@ -581,8 +581,8 @@ bool event_grapht::critical_cyclet::is_unsafe(memory_modelt model, bool fast)
if(first.unsafe_pair_lwfence(second,model)
&& (first.thread!=second.thread || egraph.are_po_ordered(back(),*s_it)))
{
std::list<unsigned>::const_iterator before_first;
std::list<unsigned>::const_iterator after_second;
std::list<event_idt>::const_iterator before_first;
std::list<event_idt>::const_iterator after_second;

before_first = end();
--before_first;
Expand Down Expand Up @@ -1332,7 +1332,7 @@ Function: event_grapht::critical_cyclet::hide_internals

void event_grapht::critical_cyclet::hide_internals(critical_cyclet& reduced) const
{
std::set<unsigned> reduced_evts;
std::set<event_idt> reduced_evts;
const_iterator first_it, prev_it=end();

/* finds an element first of its thread */
Expand Down
Loading