Merge pull request #4163 from tautschnig/irept-deserialisation

irept deserialisation: avoid unnecessary construct/destruct

Author: tautschnig

src/goto-programs/read_bin_goto_object.cpp

@@ -36,9 +36,10 @@ static bool read_bin_goto_object(
   {
     symbolt sym;
 
-    irepconverter.reference_convert(in, sym.type);
-    irepconverter.reference_convert(in, sym.value);
-    irepconverter.reference_convert(in, sym.location);
+    sym.type = static_cast<const typet &>(irepconverter.reference_convert(in));
+    sym.value = static_cast<const exprt &>(irepconverter.reference_convert(in));
+    sym.location = static_cast<const source_locationt &>(
+      irepconverter.reference_convert(in));
 
     sym.name = irepconverter.read_string_ref(in);
     sym.module = irepconverter.read_string_ref(in);
@@ -100,12 +101,14 @@ static bool read_bin_goto_object(
       goto_programt::targett itarget = f.body.add_instruction();
       goto_programt::instructiont &instruction=*itarget;
 
-      irepconverter.reference_convert(in, instruction.code);
-      irepconverter.reference_convert(in, instruction.source_location);
+      instruction.code =
+        static_cast<const codet &>(irepconverter.reference_convert(in));
+      instruction.source_location = static_cast<const source_locationt &>(
+        irepconverter.reference_convert(in));
       instruction.type = (goto_program_instruction_typet)
                               irepconverter.read_gb_word(in);
-      instruction.guard.make_nil();
-      irepconverter.reference_convert(in, instruction.guard);
+      instruction.guard =
+        static_cast<const exprt &>(irepconverter.reference_convert(in));
       instruction.target_number = irepconverter.read_gb_word(in);
       if(instruction.is_target() &&
          rev_target_map.insert(

src/util/irep_serialization.cpp

@@ -41,20 +41,15 @@ void irep_serializationt::write_irep(
   out.put(0); // terminator
 }
 
-void irep_serializationt::reference_convert(
-  std::istream &in,
-  irept &irep)
+const irept &irep_serializationt::reference_convert(std::istream &in)
 {
   std::size_t id=read_gb_word(in);
 
-  if(id<ireps_container.ireps_on_read.size() &&
-     ireps_container.ireps_on_read[id].first)
-  {
-    irep=ireps_container.ireps_on_read[id].second;
-  }
-  else
+  if(
+    id >= ireps_container.ireps_on_read.size() ||
+    !ireps_container.ireps_on_read[id].first)
   {
-    read_irep(in, irep);
+    irept irep = read_irep(in);
 
     if(id >= ireps_container.ireps_on_read.size())
       ireps_container.ireps_on_read.resize(1 + id * 2, {false, get_nil_irep()});
@@ -63,42 +58,57 @@ void irep_serializationt::reference_convert(
     if(ireps_container.ireps_on_read[id].first)
       throw deserialization_exceptiont("irep id read twice.");
 
-    ireps_container.ireps_on_read[id] = {true, irep};
+    ireps_container.ireps_on_read[id] = {true, std::move(irep)};
   }
+
+  return ireps_container.ireps_on_read[id].second;
 }
 
-void irep_serializationt::read_irep(
-  std::istream &in,
-  irept &irep)
+irept irep_serializationt::read_irep(std::istream &in)
 {
-  irep.clear();
-  irep.id(read_string_ref(in));
+  irep_idt id = read_string_ref(in);
+  irept::subt sub;
+  irept::named_subt named_sub;
 
   while(in.peek()=='S')
   {
     in.get();
-    irep.get_sub().push_back(irept());
-    reference_convert(in, irep.get_sub().back());
+    sub.push_back(reference_convert(in));
   }
 
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  irept::named_subt::iterator before = named_sub.before_begin();
+#endif
   while(in.peek()=='N')
   {
     in.get();
-    irept &r=irep.add(read_string_ref(in));
-    reference_convert(in, r);
+    irep_idt id = read_string_ref(in);
+#ifdef 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();
-    irept &r=irep.add(read_string_ref(in));
-    reference_convert(in, r);
+    irep_idt id = read_string_ref(in);
+#ifdef 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)
   {
     throw deserialization_exceptiont("irep not terminated");
   }
+
+  return irept(std::move(id), std::move(named_sub), std::move(sub));
 }
 
 /// Serialize an irept

src/util/irep_serialization.h

@@ -61,7 +61,7 @@ class irep_serializationt
     clear();
   };
 
-  void reference_convert(std::istream &, irept &irep);
+  const irept &reference_convert(std::istream &);
   void reference_convert(const irept &irep, std::ostream &);
 
   irep_idt read_string_ref(std::istream &);
@@ -77,7 +77,7 @@ class irep_serializationt
   std::vector<char> read_buffer;
 
   void write_irep(std::ostream &, const irept &irep);
-  void read_irep(std::istream &, irept &irep);
+  irept read_irep(std::istream &);
 };
 
 #endif // CPROVER_UTIL_IREP_SERIALIZATION_H