Description of changes:

A PR introducing a --gen-c-runnable flag which produces a runnable C program from the compiled goto program. The existing --gen-c flag acts as a starting point, but there are a few issues listed in #237 that prevent the generated C file from compiling.

The change introduces a generic visitor pattern for transforming Stmts, Exprs, and Types, which is then used to create a transformer over symbol tables. We then create an implementation for transforming identifiers in the symbol table to valid C identifiers.

To signify whether we want the original symbol table or the transformed names one, we pass a different backend ("gotoc" vs "genc") to the rmc-rustc command. We then do some post-processing to add in some CBMC-specific special functions/macros.

Resolved issues:

Partially resolves #237 (possibly fully after more changes.)

Call-outs:

Todo:

• Generate nondet_<k>() functions from a sample trace.
• Add definition for overflow
• Add definition for byte_extract_little_endian
• Fix field access in src/test/cbmc/FatPointers/boxtrait.c
• Set up distinct flags for readable and runnable gen-c
• Figure out testing strategy
• Documentation
• Clean up commits

Testing:

• How is this change tested? Existing regression suite.

• Is this a refactor change? No.

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.