Skip to content

irept deserialisation: avoid unnecessary construct/destruct #4163

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 12, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 10 additions & 7 deletions src/goto-programs/read_bin_goto_object.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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<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);
Expand Down Expand Up @@ -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<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(
Expand Down
54 changes: 32 additions & 22 deletions src/util/irep_serialization.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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()});
Expand All @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/util/irep_serialization.h
Original file line number Diff line number Diff line change
Expand Up @@ -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 &);
Expand All @@ -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