Skip to content

cfgt: index entry-map by instruction location number, not the instruction itself #5049

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
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
3 changes: 3 additions & 0 deletions src/goto-instrument/dump_c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -663,6 +663,9 @@ void dump_ct::cleanup_decl(

tmp.add(goto_programt::make_end_function());

// goto_program2codet requires valid location numbers:
tmp.update();

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems like it might fix an obscure bug or two...

std::unordered_set<irep_idt> typedef_names;
for(const auto &td : typedef_map)
typedef_names.insert(td.first);
Expand Down
17 changes: 17 additions & 0 deletions src/goto-instrument/goto_instrument_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -692,6 +692,10 @@ int goto_instrument_parse_optionst::doit()
// applied
restore_returns(goto_model);

// dump_c (actually goto_program2code) requires valid instruction
// location numbers:
goto_model.goto_functions.update();

if(cmdline.args.size()==2)
{
#ifdef _MSC_VER
Expand Down Expand Up @@ -1520,6 +1524,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
do_indirect_call_and_rtti_removal();

log.status() << "Performing a reachability slice" << messaget::eom;

// reachability_slicer requires that the model has unique location numbers:
goto_model.goto_functions.update();

if(cmdline.isset("property"))
reachability_slicer(goto_model, cmdline.get_values("property"));
else
Expand All @@ -1546,7 +1554,11 @@ void goto_instrument_parse_optionst::instrument_goto_program()
if(cmdline.isset("property"))
property_slicer(goto_model, cmdline.get_values("property"));
else
{
// full_slicer requires that the model has unique location numbers:
goto_model.goto_functions.update();
full_slicer(goto_model);
}
}

// splice option
Expand All @@ -1567,6 +1579,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
{
do_indirect_call_and_rtti_removal();

// reachability_slicer requires that the model has unique location numbers:
goto_model.goto_functions.update();

log.status() << "Slicing away initializations of unused global variables"
<< messaget::eom;
slice_global_inits(goto_model);
Expand Down Expand Up @@ -1595,6 +1610,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()

aggressive_slicer.doit();

goto_model.goto_functions.update();

log.status() << "Performing a reachability slice" << messaget::eom;
if(cmdline.isset("property"))
reachability_slicer(goto_model, cmdline.get_values("property"));
Expand Down
62 changes: 57 additions & 5 deletions src/goto-programs/cfg.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,9 @@ Author: Daniel Kroening, [email protected]
#ifndef CPROVER_GOTO_PROGRAMS_CFG_H
#define CPROVER_GOTO_PROGRAMS_CFG_H

#include <util/std_expr.h>
#include <util/dense_integer_map.h>
#include <util/graph.h>
#include <util/std_expr.h>

#include "goto_functions.h"

Expand All @@ -31,6 +32,29 @@ struct cfg_base_nodet:public graph_nodet<empty_edget>, public T
I PC;
};

/// Functor to convert cfg nodes into dense integers, used by \ref cfg_baset.
/// Default implementation: the identity function.
template <class T>
class cfg_instruction_to_dense_integert
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This could do with some unit tests.

{
public:
std::size_t operator()(T &&t) const
{
return std::forward<T>(identity_functort{}(t));
}
};

/// GOTO-instruction to location number functor.
template <>
class cfg_instruction_to_dense_integert<goto_programt::const_targett>
{
public:
std::size_t operator()(const goto_programt::const_targett &t) const
{
return t->location_number;
}
};

/// A multi-procedural control flow graph (CFG) whose nodes store references to
/// instructions in a GOTO program.
///
Expand Down Expand Up @@ -69,7 +93,11 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >

class entry_mapt final
{
typedef std::map<goto_programt::const_targett, entryt> data_typet;
typedef dense_integer_mapt<
goto_programt::const_targett,
entryt,
cfg_instruction_to_dense_integert<goto_programt::const_targett>>
data_typet;
data_typet data;

public:
Expand Down Expand Up @@ -114,6 +142,12 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
{
return data.at(t);
}

template <class Iter>
void setup_for_keys(Iter begin, Iter end)
{
data.setup_for_keys(begin, end);
}
};
entry_mapt entry_map;

Expand Down Expand Up @@ -173,12 +207,30 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
void operator()(
const goto_functionst &goto_functions)
{
std::vector<goto_programt::const_targett> possible_keys;
for(const auto &id_and_function : goto_functions.function_map)
{
const auto &instructions = id_and_function.second.body.instructions;
possible_keys.reserve(
possible_keys.size() +
std::distance(instructions.begin(), instructions.end()));
for(auto it = instructions.begin(); it != instructions.end(); ++it)
possible_keys.push_back(it);
}
entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
compute_edges(goto_functions);
}

void operator()(P &goto_program)
{
goto_functionst goto_functions;
std::vector<goto_programt::const_targett> possible_keys;
const auto &instructions = goto_program.instructions;
possible_keys.reserve(
std::distance(instructions.begin(), instructions.end()));
for(auto it = instructions.begin(); it != instructions.end(); ++it)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why std::distance? On a list that's linear.
.size() is constant since C++11.

possible_keys.push_back(it);
entry_map.setup_for_keys(possible_keys.begin(), possible_keys.end());
compute_edges(goto_functions, goto_program);
}

Expand All @@ -187,19 +239,19 @@ class cfg_baset:public grapht< cfg_base_nodet<T, I> >
/// in that particular case you should just use `cfg.get_node(i)`). Storing
/// node indices saves a map lookup, so it can be worthwhile when you expect
/// to repeatedly look up the same program point.
entryt get_node_index(const I &program_point) const
entryt get_node_index(const goto_programt::const_targett &program_point) const
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could use pass-by-value 🍐

{
return entry_map.at(program_point);
}

/// Get the CFG graph node relating to \p program_point.
nodet &get_node(const I &program_point)
nodet &get_node(const goto_programt::const_targett &program_point)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🍐

{
return (*this)[get_node_index(program_point)];
}

/// Get the CFG graph node relating to \p program_point.
const nodet &get_node(const I &program_point) const
const nodet &get_node(const goto_programt::const_targett &program_point) const
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🍐

{
return (*this)[get_node_index(program_point)];
}
Expand Down
Loading