RMC compiles each Rust crate to a goto binary, and then uses the CBMC linker to link those binaries together. It is possible that the CBMC and Rust linkers may make different decisions, particularly in the case of either duplicated or missing symbols.
Likelihood:
We know of at least two regressions that fail due to missing functions at link time
We have a workaround for duplicated function symbols (due to inlining). This workaround appears to work for all known cases, but there may well be corner cases we have not yet encountered.
Linking is known to be broken in RMC in cases where one crate overrides another
Mitigation:
[x] Alarm on CBMC warnings.
Path to soundness:
[ ] Develop a formal model of Rust linking, and confirm that CBMC linking is compatible.
[ ] Add additional sanity checks to the CBMC linker.
RMC compiles each Rust crate to a goto binary, and then uses the CBMC linker to link those binaries together. It is possible that the CBMC and Rust linkers may make different decisions, particularly in the case of either duplicated or missing symbols.
Likelihood:
Mitigation:
Path to soundness:
Documentation: