From ba4a00599d1a8e3ca37a9f1442a351b6057a9be9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 15 Jan 2019 16:53:57 +0000 Subject: [PATCH] irept deserialisation: avoid unnecessary construct/destruct Do not allocate empty irept elements to incrementally replace them, but instead construct them bottom-up. When running on SV-COMP's ReachSafety-ECA, these changes avoid 805,690,478 calls to irept::detach and 554,309,582 calls to irept::remove_ref in read_irep. In reference_convert, the number of irept::remove_ref calls is approximately halved (from 1,209,156,897 down to 637,698,242), and the number of irept copy constructor calls reduces from 302,984,665 to 56,124. --- src/goto-programs/read_bin_goto_object.cpp | 17 ++++--- src/util/irep_serialization.cpp | 54 +++++++++++++--------- src/util/irep_serialization.h | 4 +- 3 files changed, 44 insertions(+), 31 deletions(-) diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 76c47e6b00e..94f4c995935 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -35,9 +35,10 @@ static bool read_bin_goto_object_v5( { symbolt sym; - irepconverter.reference_convert(in, sym.type); - irepconverter.reference_convert(in, sym.value); - irepconverter.reference_convert(in, sym.location); + sym.type = static_cast(irepconverter.reference_convert(in)); + sym.value = static_cast(irepconverter.reference_convert(in)); + sym.location = static_cast( + irepconverter.reference_convert(in)); sym.name = irepconverter.read_string_ref(in); sym.module = irepconverter.read_string_ref(in); @@ -99,12 +100,14 @@ static bool read_bin_goto_object_v5( 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(irepconverter.reference_convert(in)); + instruction.source_location = static_cast( + 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(irepconverter.reference_convert(in)); instruction.target_number = irepconverter.read_gb_word(in); if(instruction.is_target() && rev_target_map.insert( diff --git a/src/util/irep_serialization.cpp b/src/util/irep_serialization.cpp index d3840505b2d..635eb4a2ca8 100644 --- a/src/util/irep_serialization.cpp +++ b/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) { - 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 diff --git a/src/util/irep_serialization.h b/src/util/irep_serialization.h index 5268325e2c3..275e9268ff5 100644 --- a/src/util/irep_serialization.h +++ b/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 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