Repository navigation
Read constant pointer offsets and slice lengths from the pointer - #4976
srivatsansamraj wants to merge 2 commits into
Conversation
|
@CYJ904 @Tianshu-Huang @wodex1nhaoIeng @acearyanarun for review. Kani built every constant slice and string from the whole constant it points into, so |
github-actions
Bot
added
Z-EndToEndBenchCI
1480260 to
83a492e
Compare
feliperodri
added
[C] Bug
There was a problem hiding this comment.
Warning
Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.
Copilot review overview
3 open issues
What changed in this PR
Fixes constant pointer codegen to respect the pointer’s own offset/length metadata (rather than the full allocation), preventing unsound proofs and compiler ICEs for subslices, substrings, element refs, and dangling empty slices/strings.
Changes:
- Read data offset (and fat-pointer length) from the constant pointer bytes in
codegen_const_ptr, and use the address directly when provenance is absent. - Adjust
&strhandling so only whole literals follow the literal extraction path; substrings are treated as non-literals. - Add regression tests and expected-failure outputs covering subslices/element refs, ZST slices, dangling empty slices/strings, and non-UTF8 backing bytes.
| File | Description |
|---|---|
| tests/kani/Slice/const_zst_slice.rs | Reproduces and guards against ZST-slice length computation ICEs. |
| tests/kani/Slice/const_subslice.rs | Validates correct offsets/lengths for subslices, substrings, and element references (incl. symbolic indexing). |
| tests/kani/Slice/const_str_non_utf8.rs | Ensures substring &str over valid UTF-8 region doesn’t decode whole non-UTF8 allocation (no ICE). |
| tests/kani/Slice/const_dangling_empty.rs | Confirms dangling empty slices/strings codegen uses the stored address when provenance is absent (no ICE). |
| tests/expected/const-subslice/main.rs | Expected-failure harnesses that must fail when subslices/refs are handled correctly. |
| tests/expected/const-subslice/expected | Pins the 6 expected failures for the above harnesses. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs | Core fix: derive offset/len from pointer bytes; handle no-provenance pointers; treat substrings as non-literals. |
Review effort: Lite
| let offset = alloc.read_partial_uint(0..pointer_size).unwrap(); | ||
| if self.use_fat_pointer_stable(inner_ty) { | ||
| let len = alloc.read_partial_uint(pointer_size..2 * pointer_size).unwrap(); |
There was a problem hiding this comment.
Done in fbebfa5ed: the reads name the constant's type when they fail.
| let Some(&(_, prov)) = alloc.provenance.ptrs.first() else { | ||
| // A pointer with no provenance (an empty slice or `&str` from a dangling | ||
| // pointer, for example) holds its address in the offset. | ||
| let data_expr = Expr::size_constant(offset, &self.symbol_table) | ||
| .cast_to(Type::unsigned_int(8).to_pointer()); | ||
| return slice_fat_ptr(typ, data_expr, len_expr, &self.symbol_table); | ||
| }; |
There was a problem hiding this comment.
Done in fbebfa5ed: more than one provenance entry is an assertion failure again, and none is still handled.
| let alloc_id = alloc.provenance.ptrs[0].1.0; | ||
| let typ = self.codegen_ty_stable(ty); | ||
| self.codegen_alloc_pointer(typ, alloc_id, ptr.0, loc) | ||
| self.codegen_alloc_pointer(typ, alloc_id, offset.try_into().unwrap(), loc) |
There was a problem hiding this comment.
Done in fbebfa5ed, with the offset and the type in the message.
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
The fix is right: a constant subslice now takes its offset and length from its own pointer, and the native-value tests show it.
Before merge:
- The old code asserted one provenance entry, and the new code takes
.first()and ignores the rest. Please keep an assert, or document why more than one can't occur. - Replace the
unwrap()calls withexpect(...)messages, as Copilot suggests, so a malformed constant gives a readable panic. auditfails. Please confirm it fails onmaintoo. Six jobs are cancelled. Please re-run them.- The branch is behind
main. Please update it.
`codegen_const_ptr` built a constant `&[T]` or `&str` from the start and the length of the whole allocation it points into, so a constant subslice such as `A.split_at(1).1` got the data and the length of `A` (model-checking#4971), and a constant empty slice with a dangling pointer, which has no provenance, hit an assertion in the compiler (model-checking#3021). A thin constant reference such as `&A[1]` read `A[0]` for the same reason: the offset it passed on was the pointer's position inside the constant, which is always 0. The offset, and a slice's length, are now read from the constant's own bytes, the address itself is used when there is no provenance, and a `&str` that is not a whole literal records nothing in `str_literals`, so `extract_const_message` cannot return the enclosing literal for it. The tests in `tests/kani/Slice/const_subslice.rs` check the native values of such subslices and references, also through a symbolic index that rustc cannot fold into a constant, `tests/expected/const-subslice` checks that the whole-allocation values now fail, `const_dangling_empty.rs` is the program from model-checking#3021, and `const_zst_slice.rs` and `const_str_non_utf8.rs` cover two compiler crashes in the same arms, for zero-sized elements and for a `&str` inside bytes that are not UTF-8.
Taking the first provenance entry would silently pick one buffer if a constant slice or string ever had more than one. Assert at most one, as before, now that a pointer with none is handled. The pointer reads also name the constant's type when they fail.
83a492e to
fbebfa5
Compare
|
@feliperodri rebased onto main, which reruns the cancelled jobs; the assert and the messages are in |
codegen_const_ptrbuilt a constant&[T]or&strfrom the start and the length of the whole allocation it points into. A constant subslice such asA.split_at(1).1therefore got the data and the length ofA, and Kani proved assertions about it that are false when the program runs (#4971). A constant empty slice with a dangling pointer has no provenance and hit the "Expected&[T]to point to a single buffer" assertion (#3021).While working on #4971, I noticed that a thin constant reference into another constant has the same problem: for
const R: &u8 = &A[1], Kani readA[0], because the offset it passed on was the pointer's position inside the constant, which is always 0. This PR fixes it as well.The offset, and a slice's length, are now read from the constant's own bytes, and the address itself is used when there is no provenance. A
&strthat is not a whole literal records nothing instr_literals; whole literals take the unchanged path. One visible change: a constant substring used as akani::assertmessage is now rejected like any other non-literal message, where before it printed the enclosing literal.tests/kani/Slice/const_subslice.rschecks the native values of subslices, substrings and element references, withu32elements so that a byte offset and an element index differ, and through a symbolic index that rustc cannot fold into a constant.tests/expected/const-subslicepins the six whole-allocation assertions as failures; all six verified onmain.const_dangling_empty.rsis the program from #3021.const_zst_slice.rsandconst_str_non_utf8.rscover two compiler crashes the same change removes.Not included: a constant slice that points into a
staticstill crashes the compiler, for a different reason.Resolves #4971
Resolves #3021
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.