Skip to content

Remove unnecessary uses of irep_id_hash #2093

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
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
2 changes: 1 addition & 1 deletion src/analyses/call_graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ class function_indicest
call_grapht::directed_grapht &graph;

public:
std::unordered_map<irep_idt, node_indext, irep_id_hash> function_indices;
std::unordered_map<irep_idt, node_indext> function_indices;

explicit function_indicest(call_grapht::directed_grapht &graph):
graph(graph)
Expand Down
5 changes: 2 additions & 3 deletions src/analyses/call_graph.h
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ class call_grapht
friend class call_grapht;

/// Maps function names onto node indices
std::unordered_map<irep_idt, node_indext, irep_id_hash> nodes_by_name;
std::unordered_map<irep_idt, node_indext> nodes_by_name;

public:
/// Find the graph node by function name
Expand All @@ -124,8 +124,7 @@ class call_grapht
optionalt<node_indext> get_node_index(const irep_idt &function) const;

/// Type of the node name -> node index map.
typedef
std::unordered_map<irep_idt, node_indext, irep_id_hash> nodes_by_namet;
typedef std::unordered_map<irep_idt, node_indext> nodes_by_namet;

/// Get the node name -> node index map
/// \return node-by-name map
Expand Down
7 changes: 3 additions & 4 deletions src/analyses/dirty.h
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,6 @@ class dirtyt

public:
bool initialized;
typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
typedef goto_functionst::goto_functiont goto_functiont;

/// \post dirtyt objects that are created through this constructor are not
Expand Down Expand Up @@ -72,7 +71,7 @@ class dirtyt
return operator()(expr.get_identifier());
}

const id_sett &get_dirty_ids() const
const std::unordered_set<irep_idt> &get_dirty_ids() const
{
die_if_uninitialized();
return dirty;
Expand All @@ -97,7 +96,7 @@ class dirtyt
void build(const goto_functiont &goto_function);

// variables whose address is taken
id_sett dirty;
std::unordered_set<irep_idt> dirty;

void find_dirty(const exprt &expr);
void find_dirty_address_of(const exprt &expr);
Expand Down Expand Up @@ -131,7 +130,7 @@ class incremental_dirtyt

private:
dirtyt dirty;
std::unordered_set<irep_idt, irep_id_hash> dirty_processed_functions;
std::unordered_set<irep_idt> dirty_processed_functions;
};

#endif // CPROVER_ANALYSES_DIRTY_H
6 changes: 2 additions & 4 deletions src/analyses/invariant_propagation.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,7 @@ void invariant_propagationt::add_objects(
goto_program.get_decl_identifiers(locals);

// cache the list for the locals to speed things up
typedef std::unordered_map<irep_idt, object_listt, irep_id_hash>
object_cachet;
typedef std::unordered_map<irep_idt, object_listt> object_cachet;
object_cachet object_cache;

forall_goto_program_instructions(i_it, goto_program)
Expand Down Expand Up @@ -133,8 +132,7 @@ void invariant_propagationt::add_objects(
const goto_programt &goto_program=f_it->second.body;

// cache the list for the locals to speed things up
typedef std::unordered_map<irep_idt, object_listt, irep_id_hash>
object_cachet;
typedef std::unordered_map<irep_idt, object_listt> object_cachet;
object_cachet object_cache;

forall_goto_program_instructions(i_it, goto_program)
Expand Down
7 changes: 3 additions & 4 deletions src/analyses/reaching_definitions.h
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ class sparse_bitvector_analysist
protected:
typedef typename std::map<V, std::size_t> inner_mapt;
std::vector<typename inner_mapt::const_iterator> values;
std::unordered_map<irep_idt, inner_mapt, irep_id_hash> value_map;
std::unordered_map<irep_idt, inner_mapt> value_map;
};

struct reaching_definitiont
Expand Down Expand Up @@ -191,15 +191,14 @@ class rd_range_domaint:public ai_domain_baset
#ifdef USE_DSTRING
typedef std::map<irep_idt, values_innert> valuest;
#else
typedef std::unordered_map<irep_idt, values_innert, irep_id_hash> valuest;
typedef std::unordered_map<irep_idt, values_innert> valuest;
#endif
valuest values;

#ifdef USE_DSTRING
typedef std::map<irep_idt, ranges_at_loct> export_cachet;
#else
typedef std::unordered_map<irep_idt, ranges_at_loct, irep_id_hash>
export_cachet;
typedef std::unordered_map<irep_idt, ranges_at_loct> export_cachet;
#endif
mutable export_cachet export_cache;

Expand Down
3 changes: 1 addition & 2 deletions src/ansi-c/ansi_c_scope.h
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,7 @@ class ansi_c_scopet
public:
// This maps "scope names" (tag-X, label-X, X) to
// ansi_c_identifiert.
typedef std::unordered_map<irep_idt, ansi_c_identifiert, irep_id_hash>
name_mapt;
typedef std::unordered_map<irep_idt, ansi_c_identifiert> name_mapt;
name_mapt name_map;

std::string prefix;
Expand Down
4 changes: 2 additions & 2 deletions src/ansi-c/c_typecheck_base.h
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ class c_typecheck_baset:
const irep_idt mode;
symbolt current_symbol;

typedef std::unordered_map<irep_idt, typet, irep_id_hash> id_type_mapt;
typedef std::unordered_map<irep_idt, typet> id_type_mapt;
id_type_mapt parameter_map;

// overload to use language specific syntax
Expand Down Expand Up @@ -270,7 +270,7 @@ class c_typecheck_baset:
src.id()==ID_real;
}

typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> asm_label_mapt;
typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
asm_label_mapt asm_label_map;

void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_type.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -877,7 +877,7 @@ void c_typecheck_baset::typecheck_compound_body(
// scan for duplicate members

{
std::unordered_set<irep_idt, irep_id_hash> members;
std::unordered_set<irep_idt> members;

for(struct_union_typet::componentst::iterator
it=components.begin();
Expand Down
4 changes: 2 additions & 2 deletions src/ansi-c/expr2c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1688,8 +1688,8 @@ std::string expr2ct::convert_symbol(
dest=src.op0().get_string(ID_identifier);
else
{
std::unordered_map<irep_idt, irep_idt, irep_id_hash>::const_iterator
entry=shorthands.find(id);
std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
shorthands.find(id);
// we might be called from conversion of a type
if(entry==shorthands.end())
{
Expand Down
6 changes: 2 additions & 4 deletions src/ansi-c/expr2c_class.h
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,8 @@ class expr2ct

static std::string indent_str(unsigned indent);

std::unordered_map<irep_idt,
std::unordered_set<irep_idt, irep_id_hash>,
irep_id_hash> ns_collision;
std::unordered_map<irep_idt, irep_idt, irep_id_hash> shorthands;
std::unordered_map<irep_idt, std::unordered_set<irep_idt>> ns_collision;
std::unordered_map<irep_idt, irep_idt> shorthands;

unsigned sizeof_nesting;

Expand Down
3 changes: 1 addition & 2 deletions src/ansi-c/type2name.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,7 @@ Author: Daniel Kroening, [email protected]
#include <util/pointer_offset_size.h>
#include <util/invariant.h>

typedef std::unordered_map<irep_idt, std::pair<size_t, bool>, irep_id_hash>
symbol_numbert;
typedef std::unordered_map<irep_idt, std::pair<size_t, bool>> symbol_numbert;

static std::string type2name(
const typet &type,
Expand Down
4 changes: 2 additions & 2 deletions src/cbmc/symex_bmc.h
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ class symex_bmct: public goto_symext
unsigned max_unwind;
bool max_unwind_is_set;

typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> loop_limitst;
typedef std::unordered_map<irep_idt, unsigned> loop_limitst;
loop_limitst loop_limits;

typedef std::map<unsigned, loop_limitst> thread_loop_limitst;
Expand Down Expand Up @@ -147,7 +147,7 @@ class symex_bmct: public goto_symext

virtual void no_body(const irep_idt &identifier);

std::unordered_set<irep_idt, irep_id_hash> body_warnings;
std::unordered_set<irep_idt> body_warnings;

symex_coveraget symex_coverage;
};
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cpp_scopes.h
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ class cpp_scopest
}

// mapping from function/class/scope names to their cpp_idt
typedef std::unordered_map<irep_idt, cpp_idt *, irep_id_hash> id_mapt;
typedef std::unordered_map<irep_idt, cpp_idt *> id_mapt;
id_mapt id_map;

cpp_scopet *current_scope_ptr;
Expand Down
2 changes: 0 additions & 2 deletions src/cpp/expr2cpp.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,6 @@ class expr2cppt:public expr2ct
const typet &src,
const qualifierst &qualifiers,
const std::string &declarator) override;

typedef std::unordered_set<std::string, string_hash> id_sett;
};

std::string expr2cppt::convert_struct(
Expand Down
7 changes: 3 additions & 4 deletions src/goto-diff/goto_diff.h
Original file line number Diff line number Diff line change
Expand Up @@ -51,20 +51,19 @@ class goto_difft:public messaget
ui_message_handlert::uit ui;

unsigned total_functions_count;
typedef std::set<irep_idt> irep_id_sett;
irep_id_sett new_functions, modified_functions, deleted_functions;
std::set<irep_idt> new_functions, modified_functions, deleted_functions;

void output_function_group(
const std::string &group_name,
const irep_id_sett &function_group,
const std::set<irep_idt> &function_group,
const goto_modelt &goto_model) const;
void output_function(
const irep_idt &function_name,
const goto_modelt &goto_model) const;

void convert_function_group_json(
json_arrayt &result,
const irep_id_sett &function_group,
const std::set<irep_idt> &function_group,
const goto_modelt &goto_model) const;
void convert_function_json(
json_objectt &result,
Expand Down
4 changes: 2 additions & 2 deletions src/goto-diff/goto_diff_base.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ void goto_difft::output_functions() const
/// \param goto_model: the goto model
void goto_difft::output_function_group(
const std::string &group_name,
const irep_id_sett &function_group,
const std::set<irep_idt> &function_group,
const goto_modelt &goto_model) const
{
result() << group_name << ":\n";
Expand Down Expand Up @@ -113,7 +113,7 @@ void goto_difft::output_function(
/// \param goto_model: the goto model
void goto_difft::convert_function_group_json(
json_arrayt &result,
const irep_id_sett &function_group,
const std::set<irep_idt> &function_group,
const goto_modelt &goto_model) const
{
for(const auto &function_name : function_group)
Expand Down
9 changes: 3 additions & 6 deletions src/goto-instrument/code_contracts.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,7 @@ class code_contractst

unsigned temporary_counter;

typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
id_sett summarized;
std::unordered_set<irep_idt> summarized;

void code_contracts(goto_functionst::goto_functiont &goto_function);

Expand Down Expand Up @@ -389,10 +388,8 @@ void code_contractst::operator()()
goto_functions.function_map.find(CPROVER_PREFIX "initialize");
assert(i_it!=goto_functions.function_map.end());

for(id_sett::const_iterator it=summarized.begin();
it!=summarized.end();
++it)
add_contract_check(*it, i_it->second.body);
for(const auto &contract : summarized)
add_contract_check(contract, i_it->second.body);

// remove skips
remove_skip(i_it->second.body);
Expand Down
6 changes: 3 additions & 3 deletions src/goto-instrument/count_eloc.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,9 @@ Date: December 2012

#include <goto-programs/cfg.h>

typedef std::unordered_set<irep_idt, irep_id_hash> linest;
typedef std::unordered_map<irep_idt, linest, irep_id_hash> filest;
typedef std::unordered_map<irep_idt, filest, irep_id_hash> working_dirst;
typedef std::unordered_set<irep_idt> linest;
typedef std::unordered_map<irep_idt, linest> filest;
typedef std::unordered_map<irep_idt, filest> working_dirst;

static void collect_eloc(
const goto_modelt &goto_model,
Expand Down
2 changes: 1 addition & 1 deletion src/goto-instrument/cover_basic_blocks.h
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ class cover_basic_blocks_javat final : public cover_blocks_baset
// map block number to its location
std::vector<source_locationt> block_locations;
// map java indexes to block indexes
std::unordered_map<irep_idt, std::size_t, irep_id_hash> index_to_block;
std::unordered_map<irep_idt, std::size_t> index_to_block;

public:
explicit cover_basic_blocks_javat(const goto_programt &_goto_program);
Expand Down
26 changes: 13 additions & 13 deletions src/goto-instrument/dump_c.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ void dump_ct::operator()(std::ostream &os)
copied_symbol_table.add(symbol_pair.second);
}

typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> unique_tagst;
typedef std::unordered_map<irep_idt, unsigned> unique_tagst;
unique_tagst unique_tags;

// add tags to anonymous union/struct/enum,
Expand Down Expand Up @@ -613,7 +613,7 @@ void dump_ct::cleanup_decl(

tmp.add_instruction(END_FUNCTION);

std::unordered_set<irep_idt, irep_id_hash> typedef_names;
std::unordered_set<irep_idt> typedef_names;
for(const auto &td : typedef_map)
typedef_names.insert(td.first);

Expand All @@ -640,7 +640,7 @@ void dump_ct::cleanup_decl(
/// function declarations or struct definitions
void dump_ct::collect_typedefs(const typet &type, bool early)
{
std::unordered_set<irep_idt, irep_id_hash> deps;
std::unordered_set<irep_idt> deps;
collect_typedefs_rec(type, early, deps);
}

Expand All @@ -654,12 +654,12 @@ void dump_ct::collect_typedefs(const typet &type, bool early)
void dump_ct::collect_typedefs_rec(
const typet &type,
bool early,
std::unordered_set<irep_idt, irep_id_hash> &dependencies)
std::unordered_set<irep_idt> &dependencies)
{
if(system_symbols.is_type_internal(type, system_headers))
return;

std::unordered_set<irep_idt, irep_id_hash> local_deps;
std::unordered_set<irep_idt> local_deps;

if(type.id()==ID_code)
{
Expand Down Expand Up @@ -769,10 +769,9 @@ void dump_ct::dump_typedefs(std::ostream &os) const
// output
std::map<std::string, typedef_infot> to_insert;

typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
id_sett typedefs_done;
std::unordered_map<irep_idt, id_sett, irep_id_hash>
forward_deps, reverse_deps;
std::unordered_set<irep_idt> typedefs_done;
std::unordered_map<irep_idt, std::unordered_set<irep_idt>> forward_deps,
reverse_deps;

for(const auto &td : typedef_map)
if(!td.second.type_decl_str.empty())
Expand Down Expand Up @@ -805,8 +804,9 @@ void dump_ct::dump_typedefs(std::ostream &os) const
continue;

// reduce remaining dependencies
id_sett &r_deps=r_it->second;
for(id_sett::iterator it=r_deps.begin(); it!=r_deps.end(); ) // no ++it
std::unordered_set<irep_idt> &r_deps = r_it->second;
for(std::unordered_set<irep_idt>::iterator it = r_deps.begin();
it != r_deps.end();) // no ++it
{
auto f_it=forward_deps.find(*it);
if(f_it==forward_deps.end()) // might be done already
Expand All @@ -816,7 +816,7 @@ void dump_ct::dump_typedefs(std::ostream &os) const
}

// update dependencies
id_sett &f_deps=f_it->second;
std::unordered_set<irep_idt> &f_deps = f_it->second;
PRECONDITION(!f_deps.empty());
PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
f_deps.erase(t.typedef_name);
Expand Down Expand Up @@ -986,7 +986,7 @@ void dump_ct::convert_function_declaration(
code_blockt b;
std::list<irep_idt> type_decls, local_static;

std::unordered_set<irep_idt, irep_id_hash> typedef_names;
std::unordered_set<irep_idt> typedef_names;
for(const auto &td : typedef_map)
typedef_names.insert(td.first);

Expand Down
Loading