CBMC has a strict typing semantics: each type must be identified by a unique name. Structurally identical types are not considered identical for CBMC purposes: you must transition between them using an explicit byte_extract. We currently get the names for Rust types using the Rust pretty-printer. For the most part, this works well. However, in some cases the pretty printer elides necessary data, for e.g. replacing [i32; 8] with [i32, _]. This can spuriously cause structurally identical types to appear to differ; more worryingly, it can also cause unexpected type aliasing if both [i32; 8] and [i32; 4] are reduced to [i32, _].
Likelihood:
This issue does not occur on most codebases. However, there are known failing regression tests in the RMC test suite where this issue does occur.
Mitigation:
- We have special cased pretty-printing of array types to avoid the problem described above
- More generally, the GOTO type-checker we implemented has been very effective in catching these cases, and raising a warning to the user.
Path to soundness:
Replace the default Rust pretty-printer with a scheme that is guaranteed to produce canonical names.
Documentation:
CBMC has a strict typing semantics: each type must be identified by a unique name. Structurally identical types are not considered identical for CBMC purposes: you must transition between them using an explicit byte_extract. We currently get the names for Rust types using the Rust pretty-printer. For the most part, this works well. However, in some cases the pretty printer elides necessary data, for e.g. replacing
[i32; 8]with[i32, _]. This can spuriously cause structurally identical types to appear to differ; more worryingly, it can also cause unexpected type aliasing if both[i32; 8]and[i32; 4]are reduced to[i32, _].Likelihood:
This issue does not occur on most codebases. However, there are known failing regression tests in the RMC test suite where this issue does occur.
Mitigation:
Path to soundness:
Replace the default Rust pretty-printer with a scheme that is guaranteed to produce canonical names.
Documentation: