CBMC GOTO binary serde and GOTO interpreter code reuse analysis

[remi-delmas-3000]

Motivation:
Designing and developing a standalone reference evaluator for GOTO that can load GOTO binaries can require to write a lot of code if written from scratch in a language like Rust.

With this task our goal is to understand what is in a GOTO binary, estimate the workload that would be needed to write a clean-slate implementation for GOTO binary serde and new interpreter by studying the existing C++ implementation.

Deliverables

• Tech report gathering key GOTO binary information and
• Decision to reuse none, some or all of the existing CBMC infrastructure for GOTO binary serialisation/deserialisation, GOTO interpreter.
• Decision to use Rust or not to write new reference evaluator.

[tedinski]

One possible requirement to consider is to support streaming serde of the contents of a goto binary.

Rust programs seem to frequently result in much larger (static) reachability graphs compared to C ones, and consequently we see real impact from memory consumption just in representing these in memory for some operations. Kani can pretty easily get symtab2gb to consume 10+GB of RAM. I assume this is the result of reading the whole json blob into memory, processing in memory, then construction of the whole goto binary in memory before writing.

While I think the goal is to get rid of symtab, if kani-compiler were constructing goto binaries directly, it would still directly benefit in peak memory consumption from being able to stream out the contents of a goto binary one symbol at a time, instead of having to construct the whole translation in-memory first.

Just a thought, I don't know if this will be in scope.