diff --git a/compiler/cbmc/src/irep/serialize.rs b/compiler/cbmc/src/irep/serialize.rs index 3a4e295b81472..a87bebac171d1 100644 --- a/compiler/cbmc/src/irep/serialize.rs +++ b/compiler/cbmc/src/irep/serialize.rs @@ -59,6 +59,35 @@ impl Serialize for SymbolTable { } } +// A direct serialization for the goto SymbolTable (contrasting to the irep SymbolTable just above). +// This permits a "streaming optimization" where we reduce memory usage considerably by +// only holding the irep conversion of one symbol in memory at a time. +impl Serialize for crate::goto_program::SymbolTable { + fn serialize(&self, serializer: S) -> Result + where + S: Serializer, + { + let mut obj = serializer.serialize_map(None)?; + obj.serialize_entry("symbolTable", &StreamingSymbols(&self))?; + obj.end() + } +} +struct StreamingSymbols<'a>(&'a crate::goto_program::SymbolTable); +impl<'a> Serialize for StreamingSymbols<'a> { + fn serialize(&self, serializer: S) -> Result + where + S: Serializer, + { + let mm = self.0.machine_model(); + let mut obj = serializer.serialize_map(None)?; + for (k, v) in self.0.iter() { + // We're only storing the to_irep in RAM for one symbol at a time + obj.serialize_entry(k, &v.to_irep(mm))?; + } + obj.end() + } +} + impl Serialize for Symbol { fn serialize(&self, serializer: S) -> Result where diff --git a/compiler/rustc_codegen_rmc/src/compiler_interface.rs b/compiler/rustc_codegen_rmc/src/compiler_interface.rs index 358c6e2a977ff..4fa3cff51d349 100644 --- a/compiler/rustc_codegen_rmc/src/compiler_interface.rs +++ b/compiler/rustc_codegen_rmc/src/compiler_interface.rs @@ -157,7 +157,7 @@ impl CodegenBackend for GotocCodegenBackend { if !sess.opts.debugging_opts.no_codegen && sess.opts.output_types.should_codegen() { // "path.o" let base_filename = outputs.path(OutputType::Object); - write_file(&base_filename, "symtab.json", &result.symtab.to_irep()); + write_file(&base_filename, "symtab.json", &result.symtab); write_file(&base_filename, "type_map.json", &result.type_map); }