Checks non-nilness when indexing a pointer to an array - #1095
Merged
jcp19 merged 5 commits intoAug 27, 2026
Merged
Conversation
ArquintL
marked this pull request as draft
August 17, 2026 04:17
ArquintL
force-pushed
the
claude/soundness-nil-check-ptr-to-array
branch
2 times, most recently
from
August 17, 2026 06:25
702b67b to
1ade012
Compare
Indexing and slicing a pointer to an array implicitly dereference the
pointer ('p[i]' is shorthand for '(*p)[i]'), but the desugarer kept the
pointer as the direct base of the indexed or sliced expression. The
structural search for the outermost dereference of an L-value therefore
found no dereference and usages such as '&p[0]' or 'p[1:3]' generated
no nil-ness proof obligation at all, unlike the analogous field
accesses. The desugarer now makes the implicit dereference explicit
such that all further processing can uniformly treat the base as an
array; this also covers defined types whose underlying type is a
pointer to an array.
The added test cases document the different behavior of []byte and
*[N]byte, including that permission to the array does not (yet) entail
non-nilness of the pointer, in contrast to structs, since the
shared-array footprint consists of quantified permissions over embedded
locations rather than field permissions on the dereferenced pointer.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
In Go, indexing panics if the index is not within the length (only slicing is bounded by the capacity); this includes taking the address of an element. Previously, no bounds obligation was generated on this path: reads and writes are guarded by their permission footprints, which range over the in-bounds indices only, but taking the address of an element is encoded with total domain functions and, thus, verified unconditionally, e.g., for '&s[0]' with a possibly empty slice s. The obligation is emitted by safeReference for every indexed access of an array or a slice on the L-value's access path and, like the nil checks, applies only to actual code. In particular, the internal capacity-ranged footprint of 'make' and quantified permissions in specifications are unaffected. The conditions are emitted innermost-first, each guarded by the inner conditions, such that the well-definedness and the error of an outer condition can rely on the inner indices being in bounds. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Triggers are patterns that are never evaluated; wrapping them in the panic-absence checks' function applications would render them invalid as triggers. The exemption also applies to quantifiers in expression positions within actual code, e.g., in pure function bodies or ghost assignments. Furthermore, in Go, 'len' of an operand of array type is a constant and the operand is not evaluated; hence, neither the bounds of indices in the operand nor the non-nilness of a dereferenced pointer are checked. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The flag now gates both the nil-dereference checks and the index-bounds checks, i.e., the checks for the absence of runtime panics in general. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ases for nested indexed accesses The implication guarding an outer bounds condition was created with the indexed expression's plain meta information, such that the error lost the annotation identifying it as an index-bounds failure. The added test cases document the behavior of nested indexed accesses: computing the address of a nested element reads the inner slice header, which requires permission and, thus, an in-bounds inner index. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
ArquintL
force-pushed
the
claude/soundness-nil-check-ptr-to-array
branch
from
August 17, 2026 07:04
1ade012 to
c6691f0
Compare
ArquintL
marked this pull request as ready for review
August 17, 2026 07:09
jcp19
reviewed
Aug 25, 2026
Comment on lines
+90
to
+99
| // Unlike for structs, permission to the array does not (yet) entail that the pointer is | ||
| // non-nil: the shared-array footprint consists of quantified permissions over embedded | ||
| // locations rather than field permissions on the dereferenced pointer itself, so Viper's | ||
| // permission-implies-non-null reasoning does not apply. | ||
| requires acc(p) | ||
| func addrOfArrayElemWithPermission(p *[8]byte) (r *byte) { | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| r = &p[0] | ||
| return | ||
| } |
Contributor
There was a problem hiding this comment.
I don't understand this. What part of the encoding for array pointers would be to blame for this incompletenes?
Contributor
|
(This was merged automatically without my approval, we can continue the discussion about this PR in #1077) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Indexing a pointer to an array implicitly dereferences the pointer ('p[i]' is shorthand for '(*p)[i]'), but the desugarer does not introduce an explicit dereference node for it. Consequently, the structural search for the outermost dereference did not find any dereference and usages such as '&p[0]' generated no nil-ness proof obligation at all, unlike the analogous field accesses.
The added test cases document the different behavior of []byte and *[N]byte, including that permission to the array does not (yet) entail non-nilness of the pointer (cf.
addrOfArrayElemWithPermission), in contrast to structs, since the shared-array footprint consists of quantified permissions over embedded locations rather than field permissions on the dereferenced pointer.