goto trace storage: use a list instead of a vector

goto traces consume a lot of memory, and re-allocating them for each
incremental addition of a goto trace does not seem to be a good
approach. This is at the expense of more costly indexed access, which
now requires iterator increments.

Author: tautschnig

src/goto-checker/goto_trace_storage.cpp

@@ -43,7 +43,7 @@ const goto_tracet &goto_trace_storaget::insert_all(goto_tracet &&trace)
   return traces.back();
 }
 
-const std::vector<goto_tracet> &goto_trace_storaget::all() const
+const std::list<goto_tracet> &goto_trace_storaget::all() const
 {
   return traces;
 }
@@ -53,8 +53,9 @@ operator[](const irep_idt &property_id) const
 {
   const auto trace_found = property_id_to_trace_index.find(property_id);
   PRECONDITION(trace_found != property_id_to_trace_index.end());
+  CHECK_RETURN(trace_found->second < traces.size());
 
-  return traces.at(trace_found->second);
+  return *(std::next(traces.begin(), trace_found->second));
 }
 
 const namespacet &goto_trace_storaget::get_namespace() const

src/goto-checker/goto_trace_storage.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-programs/goto_trace.h>
 
+#include <list>
+
 class goto_trace_storaget
 {
 public:
@@ -28,7 +30,7 @@ class goto_trace_storaget
   ///   are mapped to the given trace.
   const goto_tracet &insert_all(goto_tracet &&);
 
-  const std::vector<goto_tracet> &all() const;
+  const std::list<goto_tracet> &all() const;
   const goto_tracet &operator[](const irep_idt &property_id) const;
 
   const namespacet &get_namespace() const;
@@ -38,7 +40,7 @@ class goto_trace_storaget
   const namespacet &ns;
 
   /// stores the traces
-  std::vector<goto_tracet> traces;
+  std::list<goto_tracet> traces;
 
   // maps property ID to index in traces
   std::unordered_map<irep_idt, std::size_t> property_id_to_trace_index;