Merge pull request #7534 from remi-delmas-3000/read-irep-ensure-named-sub-ordering

Restore named_sub map entries ordering when reading from a goto binary.

Author: tautschnig

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -18,6 +18,7 @@
 #include "abstract_environment.h"
 #include "context_abstract_object.h" // IWYU pragma: keep
 
+#include <algorithm>
 #include <numeric>
 
 static abstract_object_sett

src/cprover/generalization.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "solver.h"
 
+#include <algorithm>
 #include <iostream>
 #include <map>
 

src/cprover/inductiveness.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include "propagate.h"
 #include "solver.h"
 
+#include <algorithm>
 #include <iomanip>
 #include <iostream>
 

src/cprover/state_encoding.cpp

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 #include "state_encoding_targets.h"
 #include "variable_encoding.h"
 
+#include <algorithm>
 #include <iostream>
 
 class state_encodingt

src/goto-instrument/contracts/instrument_spec_assigns.h

@@ -21,6 +21,7 @@ Date: January 2022
 
 #include <goto-programs/goto_program.h>
 
+#include <algorithm>
 #include <unordered_map>
 #include <unordered_set>
 

src/goto-instrument/unwindset.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/abstract_goto_model.h>
 
+#include <algorithm>
 #include <fstream>
 
 void unwindsett::parse_unwind(const std::string &unwind)

src/solvers/flattening/boolbv_bitreverse.cpp

@@ -6,9 +6,11 @@ Author: Michael Tautschnig
 
 \*******************************************************************/
 
+#include <util/bitvector_expr.h>
+
 #include "boolbv.h"
 
-#include <util/bitvector_expr.h>
+#include <algorithm>
 
 bvt boolbvt::convert_bitreverse(const bitreverse_exprt &expr)
 {

src/solvers/flattening/boolbv_get.cpp

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 #include "boolbv.h"
 #include "boolbv_type.h"
 
+#include <algorithm>
+
 exprt boolbvt::get(const exprt &expr) const
 {
   if(expr.id()==ID_symbol ||

src/solvers/smt2_incremental/ast/smt_commands.cpp

@@ -4,6 +4,8 @@
 
 #include <util/range.h>
 
+#include <algorithm>
+
 // Define the irep_idts for commands.
 #define COMMAND_ID(the_id)                                                     \
   const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"};

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1,5 +1,4 @@
 // Author: Diffblue Ltd.
-
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
@@ -22,6 +21,7 @@
 #include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/theories/smt_core_theory.h>
 
+#include <algorithm>
 #include <functional>
 #include <numeric>
 

src/util/forward_list_as_map.h

@@ -34,7 +34,7 @@ class forward_list_as_mapt : public std::forward_list<std::pair<keyt, mappedt>>
   {
   }
 
-  void remove(const keyt &name)
+  void erase(const keyt &name)
   {
     const_iterator it = this->lower_bound(name);
 
@@ -94,6 +94,23 @@ class forward_list_as_mapt : public std::forward_list<std::pair<keyt, mappedt>>
     return it->second;
   }
 
+  mappedt &emplace(const keyt &name, const mappedt &irep)
+  {
+    iterator it = mutable_lower_bound(name);
+
+    if(it == this->end() || it->first != name)
+    {
+      iterator before = this->before_begin();
+      while(std::next(before) != it)
+        ++before;
+      it = this->emplace_after(before, name, irep);
+    }
+    else
+      it->second = irep;
+
+    return it->second;
+  }
+
   std::size_t size() const
   {
     return narrow<std::size_t>(std::distance(this->begin(), this->end()));

src/util/irep.cpp

@@ -94,12 +94,8 @@ void irept::set_size_t(const irep_idt &name, const std::size_t value)
 
 void irept::remove(const irep_idt &name)
 {
-#if NAMED_SUB_IS_FORWARD_LIST
-  return get_named_sub().remove(name);
-#else
   named_subt &s = get_named_sub();
   s.erase(name);
-#endif
 }
 
 const irept &irept::find(const irep_idt &name) const

src/util/irep_hash_container.cpp

@@ -55,12 +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
-#if NAMED_SUB_IS_FORWARD_LIST
-    const std::size_t named_sub_size =
-      std::distance(named_sub.begin(), named_sub.end());
-#else
     const std::size_t named_sub_size = named_sub.size();
-#endif
     packed.reserve(1 + 1 + sub.size() + 1 + named_sub_size * 2);
 
     packed.push_back(irep_id_hash()(irep.id()));

src/util/irep_serialization.cpp

@@ -75,31 +75,18 @@ irept irep_serializationt::read_irep(std::istream &in)
     sub.push_back(reference_convert(in));
   }
 
-#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);
-#if NAMED_SUB_IS_FORWARD_LIST
-    named_sub.emplace_after(before, id, reference_convert(in));
-    ++before;
-#else
     named_sub.emplace(id, reference_convert(in));
-#endif
   }
 
   while(in.peek()=='C')
   {
     in.get();
     irep_idt id = read_string_ref(in);
-#if NAMED_SUB_IS_FORWARD_LIST
-    named_sub.emplace_after(before, id, reference_convert(in));
-    ++before;
-#else
     named_sub.emplace(id, reference_convert(in));
-#endif
   }
 
   if(in.get()!=0)

src/util/lispirep.cpp

@@ -46,12 +46,7 @@ void irep2lisp(const irept &src, lispexprt &dest)
   dest.value.clear();
   dest.type=lispexprt::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
   const std::size_t named_sub_size = src.get_named_sub().size();
-#endif
   dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size);
 
   lispexprt id;

src/util/simplify_expr_int.cpp

@@ -25,6 +25,8 @@ Author: Daniel Kroening, [email protected]
 #include "simplify_utils.h"
 #include "std_expr.h"
 
+#include <algorithm>
+
 simplify_exprt::resultt<>
 simplify_exprt::simplify_bswap(const bswap_exprt &expr)
 {