Fix incompleteness with nil checking change
#1077
There are no files selected for viewing
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
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,48 @@ | ||
| // Any copyright is dedicated to the Public Domain. | ||
| // http://creativecommons.org/publicdomain/zero/1.0/ | ||
|
|
||
| package issue491_4 | ||
|
|
||
| // Tests that usages of L-values that cannot panic due to a nil dereference | ||
| // do not generate nil-ness proof obligations. Earlier versions of the nil | ||
| // checks asserted non-nilness of the address of the entire L-value, which | ||
| // the verifier often cannot prove for compound locations such as elements | ||
| // of a resliced slice (see the comments in PR #531). | ||
|
ArquintL marked this conversation as resolved.
|
||
|
|
||
| requires 8 <= len(raw) | ||
| preserves forall i int :: { &raw[i] } 0 <= i && i < len(raw) ==> acc(&raw[i]) | ||
| func DecodeFromBytes(raw []byte) { | ||
| assert forall i int :: 0 <= i && i < len(raw[2:4]) ==> | ||
| &raw[2:4][i] == &raw[2 + i] | ||
| } | ||
|
|
||
| requires len(s) == 2 | ||
| requires acc(&s[0]) && acc(&s[1]) | ||
| func reslicedElemAddr(s []int) { | ||
| assert &s[1:2][0] == &s[1] | ||
| } | ||
|
|
||
| type Pair struct { | ||
| x int | ||
| y int | ||
| } | ||
|
|
||
| // Taking the address of a field only requires the dereferenced pointer to be non-nil. | ||
| requires p != nil | ||
| func addrOfField(p *Pair) (r *int) { | ||
| r = &p.x | ||
| return | ||
| } | ||
|
|
||
| requires acc(p) | ||
| func addrOfFieldWithPermission(p *Pair) (r *int) { | ||
| r = &p.x | ||
| return | ||
| } | ||
|
|
||
| // Without any of the two preconditions, the obligation is reported. | ||
| func addrOfFieldOfNil(p *Pair) (r *int) { | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| r = &p.x | ||
| return | ||
| } | ||
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,66 @@ | ||
| // Any copyright is dedicated to the Public Domain. | ||
| // http://creativecommons.org/publicdomain/zero/1.0/ | ||
|
|
||
| package issue491_5 | ||
|
|
||
| // Tests that nil-dereference checks are not emitted in specifications and | ||
| // intrinsically ghost statements: these are never executed and thus cannot | ||
| // panic. There, an L-value rooted in a nil pointer denotes an unconstrained | ||
| // value, and the permission system prevents deriving facts about actual | ||
| // memory from it. | ||
|
|
||
| type Base struct { | ||
| numINF int | ||
| } | ||
|
|
||
| pred (b *Base) BaseMem() { | ||
| acc(&b.numINF) | ||
| } | ||
|
|
||
| type Raw struct { | ||
| Base | ||
| raw []byte | ||
| } | ||
|
|
||
| // The first conjunct calls a predicate on an embedded field, i.e., takes | ||
| // &r.Base before any permission is available. This must not generate a | ||
| // nil-ness proof obligation: a nil-receiver instance of this predicate can | ||
| // never be folded. | ||
| pred (r *Raw) Mem() { | ||
| r.Base.BaseMem() && acc(&r.raw) | ||
| } | ||
|
|
||
| // Bodies of pure functions are checked, as a pure function that is not ghost is | ||
| // executable. Here, unfolding the predicate provides the permission that entails | ||
| // that r is non-nil, so taking &r.Base is safe. | ||
| ghost | ||
| requires r.Mem() | ||
| pure func (r *Raw) numINFs() int { | ||
| return unfolding r.Mem() in unfolding r.Base.BaseMem() in r.Base.numINF | ||
| } | ||
|
|
||
| // Without such a permission, the obligation of a pure function that is not ghost | ||
| // is reported. | ||
| pure func addrOfBase(r *Raw) (res *Base) { | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| return &r.Base | ||
| } | ||
|
|
||
| requires r != nil | ||
| pure func addrOfBaseNonNil(r *Raw) (res *Base) { | ||
| return &r.Base | ||
| } | ||
|
|
||
| func test1() { | ||
| var x *[10]int | ||
| // no error: ghost statements are never executed and thus cannot panic; | ||
| // len(*x) denotes an unconstrained (but well-defined) value | ||
| assert len(*x) == len(*x) | ||
| } | ||
|
|
||
| func test2(r *Raw) { | ||
| // taking a reference in actual code is still checked | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| b := &r.Base | ||
| _ = b | ||
| } |
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,113 @@ | ||
| // Any copyright is dedicated to the Public Domain. | ||
| // http://creativecommons.org/publicdomain/zero/1.0/ | ||
|
|
||
| package issue491_6 | ||
|
|
||
| // Tests that usages of long L-value chains are rejected when they may dereference nil. | ||
| // | ||
| // Every dereference along a chain must be safe, but only the outermost one gives rise to a | ||
| // nil-ness proof obligation. The pointers dereferenced before it are read out of memory to | ||
| // form the chain, and reading them requires permission to the corresponding fields, which | ||
| // entails that they are non-nil; the outermost dereference is the only one without such a | ||
| // witness, as the memory it refers to is not necessarily read. | ||
| // | ||
| // Consequently, the two mechanisms reject with different errors, as documented per test | ||
| // below: an unsafe outermost dereference fails the nil check, whereas an unsafe dereference | ||
| // earlier in the chain fails to obtain the permission needed to read the pointer following | ||
| // it. Both reject the program, but only the former mentions nil. | ||
|
|
||
| type LList struct { | ||
| Val int | ||
| Next *LList | ||
| } | ||
|
|
||
| pred P(l *LList) { acc(&l.Val) } | ||
|
|
||
| // In the three tests below, every pointer up to the outermost dereference is owned, so the | ||
| // chain is read safely, and only the pointer of the outermost dereference is unconstrained: | ||
| // the permission to the field behind it is wrapped in a predicate, which does not entail | ||
| // that the pointer is non-nil. These are the cases that the nil check rejects, and they | ||
| // fail with a nil error at increasing depths. | ||
| requires acc(&l.Next) && P(l.Next) | ||
| func chain1(l *LList) (r *int) { | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| r = &l.Next.Val | ||
| return | ||
| } | ||
|
|
||
| requires acc(&l.Next) && acc(&l.Next.Next) && P(l.Next.Next) | ||
| func chain2(l *LList) (r *int) { | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| r = &l.Next.Next.Val | ||
| return | ||
| } | ||
|
|
||
| requires acc(&l.Next) && acc(&l.Next.Next) && acc(&l.Next.Next.Next) | ||
| requires P(l.Next.Next.Next) | ||
| func chain3(l *LList) (r *int) { | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| r = &l.Next.Next.Next.Val | ||
| return | ||
| } | ||
|
|
||
| // Nothing constrains l.Next.Next here, so the dereference in the middle of the chain may | ||
| // be unsafe. It is rejected, but by the permission required to read l.Next.Next.Next out | ||
| // of memory, and thus with a permission error instead of a nil error: holding that | ||
| // permission is what would have entailed that l.Next.Next is non-nil. | ||
| requires acc(&l.Next) && acc(&l.Next.Next) | ||
| func middleOfChain(l *LList) (r *int) { | ||
| //:: ExpectedOutput(assignment_error:permission_error) | ||
| r = &l.Next.Next.Next.Val | ||
| return | ||
| } | ||
|
|
||
| // Reading through a chain is rejected for the same reason. Here the permission that is | ||
| // missing is the one for the field that is read, l.Next.Next.Next.Val. | ||
| requires acc(&l.Next) && acc(&l.Next.Next) && acc(&l.Next.Next.Next) | ||
| func readChain(l *LList) (v int) { | ||
| //:: ExpectedOutput(assignment_error:permission_error) | ||
| v = l.Next.Next.Next.Val | ||
| return | ||
| } | ||
|
|
||
| // The base of an index expression is not always a location: a slice expression is not one. | ||
| // An L-value whose base is a slice expression has no outermost dereference of its own, but | ||
| // slicing an array pointer does dereference it, and that dereference is checked when the | ||
| // slice expression itself is encoded. | ||
| func sliceOfArrayPointer(p *[10]int) (r *int) { | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| r = &p[0:5][0] | ||
| return | ||
| } | ||
|
|
||
| preserves p != nil ==> acc(p) | ||
| func readSliceOfArrayPointer(p *[10]int) (v int) { | ||
| //:: ExpectedOutput(load_error:receiver_is_nil_error) | ||
| v = p[0:5][0] | ||
| return | ||
| } | ||
|
|
||
| // A slice value carries its own backing array, so slicing and indexing it dereferences | ||
| // nothing and no obligation is generated. | ||
| requires len(s) > 3 && acc(&s[2]) | ||
| func sliceOfSliceValue(s []int) (r *int) { | ||
| r = &s[2:4][0] | ||
| return | ||
| } | ||
|
|
||
| // With permissions to every link, all dereferences are witnessed and the chain verifies. | ||
| // These cases guard against the checks becoming vacuous: they must keep verifying, so that | ||
| // a change that rejects them shows up here rather than as an incompleteness in a client. | ||
| requires acc(&l.Next) && acc(&l.Next.Next) && acc(&l.Next.Next.Next) | ||
| requires acc(&l.Next.Next.Next.Val) | ||
| func chainOk(l *LList) (r *int) { | ||
| r = &l.Next.Next.Next.Val | ||
| return | ||
| } | ||
|
|
||
| // Assigning through a long chain is safe once every link is owned. | ||
| requires acc(&l.Next) && acc(&l.Next.Next) && acc(&l.Next.Next.Next) | ||
| requires acc(&l.Next.Next.Next.Val) | ||
| func assignChainOk(l *LList) { | ||
| l.Next.Next.Next.Val = 42 | ||
| } |
Oops, something went wrong.
Oops, something went wrong.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
what's the "root"?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This was a stale comment; It's the outermost dereference, i.e. the last one evaluated (for l.next.val, the dereference of l.next) — what outermostDeref returns. Reworded.