Scope work to produce goto instead of irep

[celinval]

Currently, the kani-compiler creates a CBMC symbol table and serializes it into a JSON file. We use symtab2gb to convert those files into a goto binary. This process is slow and it tends to consume a lot of memory depending on the size of the model. This has been a major bottleneck for compilation times. It tends to dominate the time spending in the compiler, and it can take much longer than the actual verification.

One possibility would be to change the compiler to produce a GOTO binary instead of the symbol table JSON.

[celinval]

Here are a few notes on my findings so far. Thanks @remi-delmas-3000 for your help:

• The goto binary is currently on version 5. The version 4 is well documented here and it seems to be independent on the C++ structures.
• The goto structure contains a symbol table and a list of instructions for each function that was compiled.
• The list of instructions in the goto is a lower representation from the function body from the symbol table.
  • Some of the lowering work that symtab2gb performs is not required, since we don't use the higher level constructs, such as loop constructs.
  • In other cases, e.g. builtin functions, we would need to expand them in the Kani compiler.
• It's not clear to me yet if the symbol table inside the goto is just a copy of the original symbol table or if it is a trimmed version that doesn't contain function body.
• The symbol table serialization done as part of the goto serialization seems to be able to handle all constructs that we use today. More details on that format is documented here.

For us to create GOTO directly, we would need to do the following:

1. Generate each function body in the goto instructions format. This can be done either by post-process the function body from the symbol table we generate or by generating the expected format directly from MIR.
2. Implement the irep and the goto serialization in Rust or wait for an API to build and serialize GOTO structures (see Step 4 from Proposal of Interface between Kani/CProver tools diffblue/cbmc#7042).

One intermediate step that we could take to reduce the cost of calling symtab2gb is to see if we can add an option that reads from a serialized irep using the same serialization mechanism as it's done as part of the goto serialization.

[tedinski]

The list of instructions in the goto is a lower representation from the function body from the symbol table.
Some of the lowering work that symtab2gb performs is not required, since we don't use the higher level constructs, such as loop constructs.

In case it might be helpful here, Sacha achieved pretty good coverage of irep stmts and the list he had to handle (i.e. was emitted by kani-compiler) is here: https://github.com/giltho/Kanillian/blob/master/kanillian/lib/goto_program/expr_and_stmt.ml#L358-L381

One thing I never figured out what was goes on with "stmt-exprs". It kinda seemed like they were left intact as high-level stmt constructs, but that does not make sense to me, and I never investigated far enough to figure it out.

[celinval]

Interesting... it looks like we would still need to lower switch statements. Thanks @tedinski