model-checking
Merge `cprover_bindings` serialization passes
Proposed change:
Based on discussion w/ @remi-delmas-3000, we think there's still a good potential for optimization in Kani's cprover_bindings code, specifically by combining the two serialization passes it currently uses.
Motivation:
To generate a goto binary from a goto_program::SymbolTable that our codegen produces, the meat of the logic is in the two following lines.
https://github.com/model-checking/kani/blob/4c18d036ac68620fc3a433444f8efad31f8579ba/cprover_bindings/src/irep/goto_binary_serde.rs#L104-L105
The first line recursively calls to_irep() on all of the nested elements of the goto_program::SymbolTable to convert it to a irep::SymbolTable. This new symbol table has the same semantic data but now just stores everything as nested Ireps (that are weakly typed and used in the goto binary format).
On the next line, we then traverse the newly created irep::SymbolTable to uniquely number structurally identical subtrees and write them all to a file.
It seems redundant to do all the work to generate a new irep::SymbolTable (e.g. memory allocation and deallocation for the underlying Vec<Irep>s) just to simply traverse it once and discard it. Instead, we could try traversing the goto_program::SymbolTable just once to both generate the weakly typed Ireps & uniquely number them for export.
