Merge pull request #3116 from tautschnig/cleanup-irep-serialization

Cleanup irep serialization

Author: tautschnig

src/util/irep_serialization.cpp

@@ -62,7 +62,15 @@ void irep_serializationt::reference_convert(
   else
   {
     read_irep(in, irep);
-    insert_on_read(id, irep);
+
+    if(id >= ireps_container.ireps_on_read.size())
+      ireps_container.ireps_on_read.resize(1 + id * 2, {false, get_nil_irep()});
+
+    // guard against self-referencing ireps
+    if(ireps_container.ireps_on_read[id].first)
+      throw deserialization_exceptiont("irep id read twice.");
+
+    ireps_container.ireps_on_read[id] = {true, irep};
   }
 }
 
@@ -100,72 +108,29 @@ void irep_serializationt::read_irep(
   }
 }
 
+/// Serialize an irept
+/// \param irep: source irept to serialize
+/// \param out: target output stream
 void irep_serializationt::reference_convert(
   const irept &irep,
   std::ostream &out)
 {
   std::size_t h=ireps_container.irep_full_hash_container.number(irep);
 
-  // should be merged with insert
-  ireps_containert::ireps_on_writet::const_iterator fi=
-    ireps_container.ireps_on_write.find(h);
+  const auto res = ireps_container.ireps_on_write.insert(
+    {h, ireps_container.ireps_on_write.size()});
 
-  if(fi==ireps_container.ireps_on_write.end())
-  {
-    size_t id=insert_on_write(h);
-    write_gb_word(out, id);
+  write_gb_word(out, res.first->second);
+  if(res.second)
     write_irep(out, irep);
-  }
-  else
-  {
-    write_gb_word(out, fi->second);
-  }
-}
-
-/// inserts an irep into the hashtable
-/// \par parameters: a size_t and an irep
-/// \return true on success, false otherwise
-std::size_t irep_serializationt::insert_on_write(std::size_t h)
-{
-  std::pair<ireps_containert::ireps_on_writet::const_iterator, bool> res=
-    ireps_container.ireps_on_write.insert(
-      std::make_pair(h, ireps_container.ireps_on_write.size()));
-
-  if(!res.second)
-    return ireps_container.ireps_on_write.size();
-  else
-    return res.first->second;
 }
 
-/// inserts an irep into the hashtable, but only the id-hashtable (only to be
-/// used upon reading ireps from a file)
-/// \par parameters: a size_t and an irep
-/// \return true on success, false otherwise
-std::size_t irep_serializationt::insert_on_read(
-  std::size_t id,
-  const irept &i)
-{
-  if(id>=ireps_container.ireps_on_read.size())
-    ireps_container.ireps_on_read.resize(1+id*2,
-      std::pair<bool, irept>(false, get_nil_irep()));
-
-  if(ireps_container.ireps_on_read[id].first)
-    throw deserialization_exceptiont("irep id read twice.");
-  else
-  {
-    ireps_container.ireps_on_read[id]=
-      std::pair<bool, irept>(true, i);
-  }
-
-  return id;
-}
-
-/// outputs 4 characters for a long, most-significant byte first
-/// \par parameters: an output stream and a number
-/// \return nothing
+/// Write 7 bits of `u` each time, least-significant byte first, until we have
+/// zero.
+/// \param out: target stream
+/// \param u: number to write
 void write_gb_word(std::ostream &out, std::size_t u)
 {
-  // we write 7 bits each time, until we have zero
 
   while(true)
   {
@@ -182,9 +147,9 @@ void write_gb_word(std::ostream &out, std::size_t u)
   }
 }
 
-/// reads 4 characters and builds a long int from them
-/// \par parameters: a stream
-/// \return a long
+/// Interpret a stream of byte as a 7-bit encoded unsigned number.
+/// \param in: input stream
+/// \return decoded number
 std::size_t irep_serializationt::read_gb_word(std::istream &in)
 {
   std::size_t res=0;
@@ -193,19 +158,25 @@ std::size_t irep_serializationt::read_gb_word(std::istream &in)
 
   while(in.good())
   {
+    if(shift_distance >= sizeof(res) * 8)
+      throw deserialization_exceptiont("input number too large");
+
     unsigned char ch=static_cast<unsigned char>(in.get());
     res|=(size_t(ch&0x7f))<<shift_distance;
     shift_distance+=7;
     if((ch&0x80)==0)
       break;
   }
 
+  if(!in.good())
+    throw deserialization_exceptiont("unexpected end of input stream");
+
   return res;
 }
 
 /// outputs the string and then a zero byte.
-/// \par parameters: an output stream and a string
-/// \return nothing
+/// \param out: output stream
+/// \param s: string to output
 void write_gb_string(std::ostream &out, const std::string &s)
 {
   for(std::string::const_iterator it=s.begin();
@@ -221,7 +192,7 @@ void write_gb_string(std::ostream &out, const std::string &s)
 }
 
 /// reads a string from the stream
-/// \par parameters: a stream
+/// \param in: input stream
 /// \return a string
 irep_idt irep_serializationt::read_gb_string(std::istream &in)
 {
@@ -244,9 +215,9 @@ irep_idt irep_serializationt::read_gb_string(std::istream &in)
   return irep_idt(std::string(read_buffer.data(), length));
 }
 
-/// outputs the string reference
-/// \par parameters: an output stream and a string
-/// \return nothing
+/// Output a string and maintain a reference to it
+/// \param out: output stream
+/// \param s: string to output
 void irep_serializationt::write_string_ref(
   std::ostream &out,
   const irep_idt &s)
@@ -265,8 +236,8 @@ void irep_serializationt::write_string_ref(
   }
 }
 
-/// reads a string reference from the stream
-/// \par parameters: a stream
+/// Read a string reference from the stream
+/// \param in: input stream
 /// \return a string
 irep_idt irep_serializationt::read_string_ref(std::istream &in)
 {
@@ -276,15 +247,12 @@ irep_idt irep_serializationt::read_string_ref(std::istream &in)
     ireps_container.string_rev_map.resize(1+id*2,
       std::pair<bool, irep_idt>(false, irep_idt()));
 
-  if(ireps_container.string_rev_map[id].first)
-  {
-    return ireps_container.string_rev_map[id].second;
-  }
-  else
+  if(!ireps_container.string_rev_map[id].first)
   {
     irep_idt s=read_gb_string(in);
     ireps_container.string_rev_map[id]=
       std::pair<bool, irep_idt>(true, s);
-    return ireps_container.string_rev_map[id].second;
   }
+
+  return ireps_container.string_rev_map[id].second;
 }

src/util/irep_serialization.h

@@ -61,9 +61,6 @@ class irep_serializationt
     clear();
   };
 
-  std::size_t insert_on_write(std::size_t h);
-  std::size_t insert_on_read(std::size_t id, const irept &);
-
   void reference_convert(std::istream &, irept &irep);
   void reference_convert(const irept &irep, std::ostream &);