Add support for anonymous nested statics #3953
Merged
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
rust-lang/rust#121644 added support for anonymous nested allocations to statics. This PR adds support for such statics to Kani.
The idea is to treat an anonymous
GlobalAlloc::Static
the same as we would treat aGlobalAlloc::Memory
, since an anonymous static is a nested memory allocation. To frame this change in terms of the tests:pointer_to_const_alloc.rs
contains a test for theGlobalAlloc::Memory
case, which we could already handle prior to this PR. The MIR looks like:meaning that
FOO
contains a pointer to the immutable allocation alloc3 (note thealloc3<imm>
, imm standing for "immutable").anon_static.rs
tests the code introduced in this PR. The MIR fromexample_1
looks almost identical:Note, however, that
alloc2
is mutable, and is thus an anonymous nested static rather than a constant allocation.But we can just call
codegen_const_allocation
anyway, since it ends up checking if the allocation is indeed constant before declaring the global variable in the symbol table:kani/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Line 556 in 319040b
Resolves #3904
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.