Use std::forward_list instead of std::map in irept by default

This reduces the size of an irept by 5 pointers (i.e., 40 bytes on
64-bit systems). On SV-COMP's ReachSafety-ECA with this change we can
perform 3819.81 symex_step calls per second, compared to 2752.28 calls
per second with the std::map configuration. The performance improvements
are spread across various `irept`-related operations.

Author: tautschnig

.travis.yml

@@ -182,7 +182,7 @@ jobs:
         - WITH_MEMORY_ANALYZER=1
       script: echo "Not running any tests for a debug build."
 
-    # cmake build using g++-7, enable NAMED_SUB_IS_FORWARD_LIST
+    # cmake build using g++-7, disable NAMED_SUB_IS_FORWARD_LIST
     - stage: Test different OS/CXX/Flags
       os: linux
       sudo: false
@@ -205,7 +205,7 @@ jobs:
       install:
         - ccache -z
         - ccache --max-size=1G
-        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST' '-DWITH_MEMORY_ANALYZER=On'
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_CXX_FLAGS=-DNAMED_SUB_IS_FORWARD_LIST=0' '-DWITH_MEMORY_ANALYZER=On'
         - git submodule update --init --recursive
         - cmake --build build -- -j4
       script: (cd build; bin/unit "[core][irept]")

src/util/irep.cpp

@@ -92,7 +92,7 @@ void irept::set(const irep_namet &name, const long long value)
 
 void irept::remove(const irep_namet &name)
 {
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   return get_named_sub().remove(name);
 #else
   named_subt &s = get_named_sub();
@@ -120,7 +120,7 @@ irept &irept::add(const irep_namet &name, irept irep)
 {
   named_subt &s = get_named_sub();
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   return s.add(name, std::move(irep));
 #else
   std::pair<named_subt::iterator, bool> entry = s.emplace(

src/util/irep.h

@@ -20,9 +20,11 @@ Author: Daniel Kroening, [email protected]
 #ifndef HASH_CODE
 #  define HASH_CODE 1
 #endif
-// #define NAMED_SUB_IS_FORWARD_LIST
+#ifndef NAMED_SUB_IS_FORWARD_LIST
+#  define NAMED_SUB_IS_FORWARD_LIST 1
+#endif
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
 #  include "forward_list_as_map.h"
 #else
 #include <map>
@@ -386,7 +388,7 @@ class irept
   : public non_sharing_treet<
       irept,
 #endif
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
       forward_list_as_mapt<irep_namet, irept>>
 #else
       std::map<irep_namet, irept>>

src/util/irep_hash_container.cpp

@@ -55,7 +55,7 @@ void irep_hash_container_baset::pack(
   {
     // we pack: the irep id, the sub size, the subs, the named-sub size, and
     // each of the named subs with their ids
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     const std::size_t named_sub_size =
       std::distance(named_sub.begin(), named_sub.end());
 #else

src/util/irep_serialization.cpp

@@ -76,14 +76,14 @@ irept irep_serializationt::read_irep(std::istream &in)
     sub.push_back(reference_convert(in));
   }
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   irept::named_subt::iterator before = named_sub.before_begin();
 #endif
   while(in.peek()=='N')
   {
     in.get();
     irep_idt id = read_string_ref(in);
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     named_sub.emplace_after(before, id, reference_convert(in));
     ++before;
 #else
@@ -95,7 +95,7 @@ irept irep_serializationt::read_irep(std::istream &in)
   {
     in.get();
     irep_idt id = read_string_ref(in);
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     named_sub.emplace_after(before, id, reference_convert(in));
     ++before;
 #else

src/util/lispirep.cpp

@@ -46,7 +46,7 @@ void irep2lisp(const irept &src, lispexprt &dest)
   dest.value.clear();
   dest.type=lispexprt::List;
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   const std::size_t named_sub_size =
     std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
 #else

src/util/merge_irep.cpp

@@ -46,7 +46,7 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const
 
   if(sub.size()!=o_sub.size())
     return false;
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   if(
     std::distance(named_sub.begin(), named_sub.end()) !=
     std::distance(o_named_sub.begin(), o_named_sub.end()))
@@ -105,12 +105,12 @@ const merged_irept &merged_irepst::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   irept::named_subt::iterator before = dest_named_sub.before_begin();
 #endif
   forall_named_irep(it, src_named_sub)
   {
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     dest_named_sub.emplace_after(
       before, it->first, merged(it->second)); // recursive call
     ++before;
@@ -209,12 +209,12 @@ const irept &merge_full_irept::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
   irept::named_subt::iterator before = dest_named_sub.before_begin();
 #endif
   forall_named_irep(it, src_named_sub)
   {
-#ifdef NAMED_SUB_IS_FORWARD_LIST
+#if NAMED_SUB_IS_FORWARD_LIST
     dest_named_sub.emplace_after(
       before, it->first, merged(it->second)); // recursive call
     ++before;

src/util/type.h

@@ -32,7 +32,8 @@ class typet:public irept
 
   explicit typet(const irep_idt &_id):irept(_id) { }
 
-#if defined(__clang__) || !defined(__GNUC__) || __GNUC__ >= 6
+  // the STL implementation shipped with GCC 5 is broken
+#if !defined(__GLIBCXX__) || __GLIBCXX__ >= 20181026
   typet(irep_idt _id, typet _subtype)
     : irept(std::move(_id), {}, {std::move(_subtype)})
   {

unit/util/irep.cpp

@@ -35,7 +35,7 @@ SCENARIO("irept_memory", "[core][utils][irept]")
       REQUIRE(sizeof(std::vector<int>) == 3 * sizeof(void *));
 #endif
 
-#ifndef NAMED_SUB_IS_FORWARD_LIST
+#if !NAMED_SUB_IS_FORWARD_LIST
       const std::size_t named_size = sizeof(std::map<int, int>);
 #  ifndef _GLIBCXX_DEBUG
 #    ifdef __APPLE__