-
Notifications
You must be signed in to change notification settings - Fork 64
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix convergence problem due to unbounded growing of assertion tree (#244
) This PR fixes the convergence issues causes by unbounded growing of assertion trees with assignments in a loop, such as in the simple example shown below. ``` func test() { a := &A{} for { a = a.f } } ``` Here, the assertion tree should look like `root -> varAssertionNode (a) -> fldAssertionNode (f)`. However, the assertion before was growing unboundedly (`root -> a -> f -> f -> f -> ...`) until the `stableRoundLimit` was hit. This simple function was taking 7 iterations to converge, while after the code change it now takes only 3 iterations to converge. Taking this opportunity, I have also added tests for testing fixpoint convergence. For this, I refactored existing infrastructure for anonymous functions and generalized it. Note: the goal of this PR is to improve performance only, and should not have any effect on the reported errors.
- Loading branch information
1 parent
fe712a8
commit 482b433
Showing
9 changed files
with
220 additions
and
74 deletions.
There are no files selected for viewing
This file contains 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 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 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 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 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 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 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 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
Oops, something went wrong.