Move all the various id_sett typedefs into irep.h

Call them unordered_id_sett to reflect the fact that these are unordered sets

Author: NathanJPhillips

src/analyses/dirty.h

@@ -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
@@ -72,7 +71,7 @@ class dirtyt
     return operator()(expr.get_identifier());
   }
 
-  const id_sett &get_dirty_ids() const
+  const unordered_id_sett &get_dirty_ids() const
   {
     die_if_uninitialized();
     return dirty;
@@ -97,7 +96,7 @@ class dirtyt
   void build(const goto_functiont &goto_function);
 
   // variables whose address is taken
-  id_sett dirty;
+  unordered_id_sett dirty;
 
   void find_dirty(const exprt &expr);
   void find_dirty_address_of(const exprt &expr);

src/goto-instrument/code_contracts.cpp

@@ -45,8 +45,7 @@ class code_contractst
 
   unsigned temporary_counter;
 
-  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
-  id_sett summarized;
+  unordered_id_sett summarized;
 
   void code_contracts(goto_functionst::goto_functiont &goto_function);
 
@@ -389,8 +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();
+  for(unordered_id_sett::const_iterator it = summarized.begin();
+      it != summarized.end();
       ++it)
     add_contract_check(*it, i_it->second.body);
 

src/goto-instrument/dump_c.cpp

@@ -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;
+  unordered_id_sett typedefs_done;
+  std::unordered_map<irep_idt, unordered_id_sett, irep_id_hash> forward_deps,
+    reverse_deps;
 
   for(const auto &td : typedef_map)
     if(!td.second.type_decl_str.empty())
@@ -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
+    unordered_id_sett &r_deps = r_it->second;
+    for(unordered_id_sett::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
@@ -816,7 +816,7 @@ void dump_ct::dump_typedefs(std::ostream &os) const
       }
 
       // update dependencies
-      id_sett &f_deps=f_it->second;
+      unordered_id_sett &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);

src/goto-instrument/goto_program2code.h

@@ -20,7 +20,6 @@ Author: Daniel Kroening, [email protected]
 class goto_program2codet
 {
   typedef std::list<irep_idt> id_listt;
-  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
   typedef std::map<goto_programt::const_targett, goto_programt::const_targett>
     loopt;
   typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> dead_mapt;
@@ -47,23 +46,23 @@ class goto_program2codet
 
 public:
   goto_program2codet(
-      const irep_idt &identifier,
-      const goto_programt &_goto_program,
-      symbol_tablet &_symbol_table,
-      code_blockt &_dest,
-      id_listt &_local_static,
-      id_listt &_type_names,
-      const id_sett &_typedef_names,
-      std::set<std::string> &_system_headers):
-    func_name(identifier),
-    goto_program(_goto_program),
-    symbol_table(_symbol_table),
-    ns(_symbol_table),
-    toplevel_block(_dest),
-    local_static(_local_static),
-    type_names(_type_names),
-    typedef_names(_typedef_names),
-    system_headers(_system_headers)
+    const irep_idt &identifier,
+    const goto_programt &_goto_program,
+    symbol_tablet &_symbol_table,
+    code_blockt &_dest,
+    id_listt &_local_static,
+    id_listt &_type_names,
+    const unordered_id_sett &_typedef_names,
+    std::set<std::string> &_system_headers)
+    : func_name(identifier),
+      goto_program(_goto_program),
+      symbol_table(_symbol_table),
+      ns(_symbol_table),
+      toplevel_block(_dest),
+      local_static(_local_static),
+      type_names(_type_names),
+      typedef_names(_typedef_names),
+      system_headers(_system_headers)
   {
     assert(local_static.empty());
 
@@ -84,18 +83,18 @@ class goto_program2codet
   code_blockt &toplevel_block;
   id_listt &local_static;
   id_listt &type_names;
-  const id_sett &typedef_names;
+  const unordered_id_sett &typedef_names;
   std::set<std::string> &system_headers;
   std::unordered_set<exprt, irep_hash> va_list_expr;
 
   natural_loopst loops;
   loopt loop_map;
-  id_sett labels_in_use;
+  unordered_id_sett labels_in_use;
   dead_mapt dead_map;
   loop_last_stackt loop_last_stack;
-  id_sett local_static_set;
-  id_sett type_names_set;
-  id_sett const_removed;
+  unordered_id_sett local_static_set;
+  unordered_id_sett type_names_set;
+  unordered_id_sett const_removed;
 
   void build_loop_map();
   void build_dead_map();

src/goto-programs/link_goto_model.cpp

@@ -158,8 +158,7 @@ void link_goto_model(
   goto_modelt &src,
   message_handlert &message_handler)
 {
-  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
-  id_sett weak_symbols;
+  unordered_id_sett weak_symbols;
 
   for(const auto &symbol_pair : dest.symbol_table.symbols)
   {

src/java_bytecode/java_bytecode_language.cpp

@@ -819,7 +819,7 @@ const select_pointer_typet &
 /// \return Populates `methods` with the complete list of lazy methods that are
 ///   available to convert (those which are valid parameters for
 ///   `convert_lazy_method`)
-void java_bytecode_languaget::methods_provided(id_sett &methods) const
+void java_bytecode_languaget::methods_provided(unordered_id_sett &methods) const
 {
   // Add all string solver methods to map
   string_preprocess.get_all_function_names(methods);

src/java_bytecode/java_bytecode_language.h

@@ -135,7 +135,7 @@ class java_bytecode_languaget:public languaget
   std::set<std::string> extensions() const override;
 
   void modules_provided(std::set<std::string> &modules) override;
-  virtual void methods_provided(id_sett &methods) const override;
+  virtual void methods_provided(unordered_id_sett &methods) const override;
   virtual void convert_lazy_method(
     const irep_idt &function_id,
     symbol_table_baset &symbol_table) override;

src/java_bytecode/java_string_library_preprocess.cpp

@@ -1827,7 +1827,7 @@ void add_keys_to_container(const TMap &map, TContainer &container)
 }
 
 void java_string_library_preprocesst::get_all_function_names(
-  id_sett &methods) const
+  unordered_id_sett &methods) const
 {
   for(const id_mapt *map : id_maps)
     add_keys_to_container(*map, methods);

src/java_bytecode/java_string_library_preprocess.h

@@ -31,8 +31,6 @@ Date:   March 2017
 // Arbitrary limit of 10 arguments for the number of arguments to String.format
 #define MAX_FORMAT_ARGS 10
 
-typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
-
 class java_string_library_preprocesst:public messaget
 {
 public:
@@ -48,7 +46,7 @@ class java_string_library_preprocesst:public messaget
   void initialize_refined_string_type();
 
   bool implements_function(const irep_idt &function_id) const;
-  void get_all_function_names(id_sett &methods) const;
+  void get_all_function_names(unordered_id_sett &methods) const;
 
   exprt
   code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table);

src/langapi/language.h

@@ -23,8 +23,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/system_library_symbols.h>
 
-typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
-
 class symbol_tablet;
 class symbol_table_baset;
 class exprt;
@@ -79,7 +77,7 @@ class languaget:public messaget
 
   // add lazy functions provided to set
 
-  virtual void methods_provided(id_sett &methods) const
+  virtual void methods_provided(unordered_id_sett &methods) const
   { }
 
   // populate a lazy method

src/langapi/language_file.cpp

@@ -144,7 +144,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
       // register lazy methods.
       // TODO: learn about modules and generalise this
       // to module-providing languages if required.
-      id_sett lazy_method_ids;
+      unordered_id_sett lazy_method_ids;
       file.second.language->methods_provided(lazy_method_ids);
       for(const auto &id : lazy_method_ids)
         lazy_method_map[id]=&file.second;

src/langapi/language_file.h

@@ -83,7 +83,7 @@ class language_filest:public messaget
   {
     // Clear relevant entries from lazy_method_map
     language_filet *language_file = &file_map.at(filename);
-    id_sett files_methods;
+    unordered_id_sett files_methods;
     for(const std::pair<irep_idt, language_filet *> &method : lazy_method_map)
     {
       if(method.second == language_file)

src/linking/linking.cpp

@@ -1162,7 +1162,7 @@ bool linkingt::needs_renaming_type(
   return true; // different
 }
 
-void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed)
+void linkingt::do_type_dependencies(unordered_id_sett &needs_to_be_renamed)
 {
   // Any type that uses a symbol that will be renamed also
   // needs to be renamed, and so on, until saturation.
@@ -1186,9 +1186,8 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed)
 
   std::stack<irep_idt> queue;
 
-  for(id_sett::const_iterator
-      d_it=needs_to_be_renamed.begin();
-      d_it!=needs_to_be_renamed.end();
+  for(unordered_id_sett::const_iterator d_it = needs_to_be_renamed.begin();
+      d_it != needs_to_be_renamed.end();
       d_it++)
     queue.push(*d_it);
 
@@ -1197,11 +1196,9 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed)
     irep_idt id=queue.top();
     queue.pop();
 
-    const id_sett &u=used_by[id];
+    const unordered_id_sett &u = used_by[id];
 
-    for(id_sett::const_iterator
-        d_it=u.begin();
-        d_it!=u.end();
+    for(unordered_id_sett::const_iterator d_it = u.begin(); d_it != u.end();
         d_it++)
       if(needs_to_be_renamed.insert(*d_it).second)
       {
@@ -1214,7 +1211,7 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed)
   }
 }
 
-void linkingt::rename_symbols(const id_sett &needs_to_be_renamed)
+void linkingt::rename_symbols(const unordered_id_sett &needs_to_be_renamed)
 {
   namespacet src_ns(src_symbol_table);
 
@@ -1258,7 +1255,7 @@ void linkingt::copy_symbols()
   }
 
   // Move over all the non-colliding ones
-  id_sett collisions;
+  unordered_id_sett collisions;
 
   for(const auto &named_symbol : src_symbols)
   {
@@ -1313,7 +1310,7 @@ void linkingt::typecheck()
 
   // PHASE 1: identify symbols to be renamed
 
-  id_sett needs_to_be_renamed;
+  unordered_id_sett needs_to_be_renamed;
 
   for(const auto &symbol_pair : src_symbol_table.symbols)
   {

src/linking/linking_class.h

@@ -38,8 +38,6 @@ class linkingt:public typecheckt
   replace_symbolt object_type_updates;
 
 protected:
-  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
-
   bool needs_renaming_type(
     const symbolt &old_symbol,
     const symbolt &new_symbol);
@@ -58,9 +56,9 @@ class linkingt:public typecheckt
       return needs_renaming_non_type(old_symbol, new_symbol);
   }
 
-  void do_type_dependencies(id_sett &);
+  void do_type_dependencies(unordered_id_sett &);
 
-  void rename_symbols(const id_sett &needs_to_be_renamed);
+  void rename_symbols(const unordered_id_sett &needs_to_be_renamed);
   void copy_symbols();
 
   void duplicate_non_type_symbol(
@@ -94,8 +92,8 @@ class linkingt:public typecheckt
     const symbolt &old_symbol;
     const symbolt &new_symbol;
     bool set_to_new;
-    id_sett o_symbols;
-    id_sett n_symbols;
+    unordered_id_sett o_symbols;
+    unordered_id_sett n_symbols;
   };
 
   bool adjust_object_type_rec(
@@ -173,12 +171,13 @@ class linkingt:public typecheckt
   namespacet ns;
 
   // X -> Y iff Y uses X for new symbol type IDs X and Y
-  typedef std::unordered_map<irep_idt, id_sett, irep_id_hash> used_byt;
+  typedef std::unordered_map<irep_idt, unordered_id_sett, irep_id_hash>
+    used_byt;
 
   irep_idt rename(irep_idt);
 
   // the new IDs created by renaming
-  id_sett renamed_ids;
+  unordered_id_sett renamed_ids;
 };
 
 #endif // CPROVER_LINKING_LINKING_CLASS_H

src/util/irep.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 #include <cassert>
 #include <iosfwd>
+#include <unordered_set>
 
 #include "irep_ids.h"
 
@@ -44,6 +45,8 @@ typedef std::string irep_namet;
 typedef string_hash irep_id_hash;
 #endif
 
+typedef std::unordered_set<irep_idt, irep_id_hash> unordered_id_sett;
+
 inline const std::string &id2string(const irep_idt &d)
 {
   #ifdef USE_DSTRING