When assessing whether A <= B, the poset's OrderedOrEqual has a passing
condition which permits A <= B, but is not sufficient to infer that A <= B.
This CL removes that incorrect passing condition.
Having identified that A and B are in the poset, the method will report that
A <= B if any of these three conditions are true:
(1) A and B are the same node in the poset.
- This means we know that A == B.
(2) There is a directed path, strict or not, from A -> B
- This means we know that, at least, A <= B, but A < B is possible.
(3) There is a directed path from B -> A, AND that path has no strict edges.
- This means we know that B <= A, but do not know that B < A.
In condition (3), we do not have enough information to say that A <= B, rather
we only know that B == A (which satisfies A <= B) is possible. The way I
understand it, a strict edge shows a known, strictly-ordered relation (<) but
the lack of a strict edge does not show the lack of a strictly-ordered relation.
The difference is highlighted by the example in #34802, where a bounds check is
incorrectly removed by prove, such that negative indexes into a slice
succeed:
n := make([]int, 1)
for i := -1; i <= 0; i++ {
fmt.Printf("i is %d\n", i)
n[i] = 1 // No Bounds check, program runs, assignment to n[-1] succeeds!!
}
When prove is checking the negative/failed branch from the bounds check at n[i],
in the signed domain we learn (0 > i || i >= len(n)). Because prove can't learn
the OR condition, we check whether we know that i is non-negative so we can
learn something, namely that i >= len(n). Prove uses the poset to check whether
we know that i is non-negative. At this point the poset holds the following
relations as a directed graph:
-1 <= i <= 0
-1 < 0
In poset.OrderedOrEqual, we are testing for 0 <= i. In this case, condition (3)
above is true because there is a non-strict path from i -> 0, and that path
does NOT have any strict edges. Because this condition is true, the poset
reports to prove that i is known to be >= 0. Knowing, incorrectly, that i >= 0,
prove learns from the failed bounds check that i >= len(n) in the signed domain.
When the slice, n, was created, prove learned that len(n) == 1. Because i is
also the induction variable for the loop, upon entering the loop, prove previously
learned that i is in [-1,0]. So when prove attempts to learn from the failed
bounds check, it finds the new fact, i > len(n), unsatisfiable given that it
previously learned that i <= 0 and len(n) = 1.
Fixes#34802
Change-Id: I235f4224bef97700c3aa5c01edcc595eb9f13afc
Reviewed-on: https://go-review.googlesource.com/c/go/+/200759
Run-TryBot: Zach Jones <zachj1@gmail.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Giovanni Bajo <rasky@develer.com>
Reviewed-by: Keith Randall <khr@golang.org>
Instead of returning an error, just panic: the function is
used only for debugging purposes anyway.
Change-Id: Ie81b2309daaf1efb9470992391534bce2141b3c2
Reviewed-on: https://go-review.googlesource.com/c/go/+/196779
Reviewed-by: David Chase <drchase@google.com>
In poset, all constants are always related to each other, so they
are part of the same DAG. Currently, it can be any of the DAGs in
the forest. Since we're about to start visiting that DAG for the
task of calculating bounds, make sure that it's conventionally
always the first, so that we don't need to search for it.
Change-Id: Ia7ca312b52336b4731b070d45cf0d768a0d6aeeb
Reviewed-on: https://go-review.googlesource.com/c/go/+/196599
Reviewed-by: David Chase <drchase@google.com>
The partially ordered set uses a method named 'dominates' to determine whether
two nodes are partially ordered. Dominates does a depth-first search of the
DAG, beginning at the source node, and returns true as soon as it finds a path
to the target node. In the context of the forest-of-DAGs that makes up the
poset, dominates is not necessarily checking dominance, but is checking
reachability. See the issue tracker for a more detailed discussion of the
difference.
Fortunately, reachability is logically correct everywhere dominates is currently
used in poset.go. Reachability within a DAG is sufficient to establish the
partial ordering (source < target).
This CL changes the name of the method (dominates -> reaches) and updates
all the comments in the file accordingly.
Fixes#33971.
Change-Id: Ia3a34f7b14b363801d75b05099cfc686035f7d96
Reviewed-on: https://go-review.googlesource.com/c/go/+/192617
Reviewed-by: Giovanni Bajo <rasky@develer.com>
Run-TryBot: Giovanni Bajo <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Go documentation style for boolean funcs is to say:
// Foo reports whether ...
func Foo() bool
(rather than "returns true if")
This CL also replaces 4 uses of "iff" with the same "reports whether"
wording, which doesn't lose any meaning, and will prevent people from
sending typo fixes when they don't realize it's "if and only if". In
the past I think we've had the typo CLs updated to just say "reports
whether". So do them all at once.
(Inspired by the addition of another "returns true if" in CL 146938
in fd_plan9.go)
Created with:
$ perl -i -npe 's/returns true if/reports whether/' $(git grep -l "returns true iff" | grep -v vendor)
$ perl -i -npe 's/returns true if/reports whether/' $(git grep -l "returns true if" | grep -v vendor)
Change-Id: Ided502237f5ab0d25cb625dbab12529c361a8b9f
Reviewed-on: https://go-review.googlesource.com/c/147037
Reviewed-by: Ian Lance Taylor <iant@golang.org>
In prove, reuse posets between different functions by storing them
in the per-worker cache.
Allocation count regression caused by prove improvements is down
from 5% to 3% after this CL.
Updates #25179
Change-Id: I6d14003109833d9b3ef5165fdea00aa9c9e952e8
Reviewed-on: https://go-review.googlesource.com/110455
Run-TryBot: Giovanni Bajo <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: David Chase <drchase@google.com>
prove uses the poset datastructure in a DFS walk, and always undoes
it back to its pristine status. Before this CL, poset's undo of
a new node creation didn't fully deallocate the node, which means
that at the end of prove there was still some allocated memory pending.
This was not a problem until now because the posets used by prove
were discarded after each function, but it would prevent recycling
them between functions (as a followup CL does).
Change-Id: I1c1c99c03fe19ad765395a43958cb256f686765a
Reviewed-on: https://go-review.googlesource.com/112976
Run-TryBot: Giovanni Bajo <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Josh Bleecher Snyder <josharian@gmail.com>
Reviewed-by: David Chase <drchase@google.com>
