Skip to content

Commit a51c702

Browse files
committed
Streaming-convert one symbol at a time to Irep, to save memory (rust-lang#625)
1 parent a665585 commit a51c702

File tree

2 files changed

+30
-1
lines changed

2 files changed

+30
-1
lines changed

compiler/cbmc/src/irep/serialize.rs

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,35 @@ impl Serialize for SymbolTable {
5959
}
6060
}
6161

62+
// A direct serialization for the goto SymbolTable (contrasting to the irep SymbolTable just above).
63+
// This permits a "streaming optimization" where we reduce memory usage considerably by
64+
// only holding the irep conversion of one symbol in memory at a time.
65+
impl Serialize for crate::goto_program::SymbolTable {
66+
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
67+
where
68+
S: Serializer,
69+
{
70+
let mut obj = serializer.serialize_map(None)?;
71+
obj.serialize_entry("symbolTable", &StreamingSymbols(&self))?;
72+
obj.end()
73+
}
74+
}
75+
struct StreamingSymbols<'a>(&'a crate::goto_program::SymbolTable);
76+
impl<'a> Serialize for StreamingSymbols<'a> {
77+
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
78+
where
79+
S: Serializer,
80+
{
81+
let mm = self.0.machine_model();
82+
let mut obj = serializer.serialize_map(None)?;
83+
for (k, v) in self.0.iter() {
84+
// We're only storing the to_irep in RAM for one symbol at a time
85+
obj.serialize_entry(k, &v.to_irep(mm))?;
86+
}
87+
obj.end()
88+
}
89+
}
90+
6291
impl Serialize for Symbol {
6392
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
6493
where

compiler/rustc_codegen_rmc/src/compiler_interface.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ impl CodegenBackend for GotocCodegenBackend {
157157
if !sess.opts.debugging_opts.no_codegen && sess.opts.output_types.should_codegen() {
158158
// "path.o"
159159
let base_filename = outputs.path(OutputType::Object);
160-
write_file(&base_filename, "symtab.json", &result.symtab.to_irep());
160+
write_file(&base_filename, "symtab.json", &result.symtab);
161161
write_file(&base_filename, "type_map.json", &result.type_map);
162162
}
163163

0 commit comments

Comments
 (0)