Zero alloc bounded join of witnesses#1472
Closed
gretay-js wants to merge 4 commits intooxcaml:mainfrom
Closed
Conversation
no functionality change
I'm not sure the dots worth the extra memory overhead
Contributor
Author
|
In terms of build performance and memory overhead, this PR won't have noticeable effect in a large code base. The bound will only trigger on large functions that have lots of allocations (more than the bound) and are annotated with |
Contributor
Author
|
closing as very very outdated, will open a new PR after this is reworked to handle fixpoint. |
3 tasks
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
1 participant
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.
On top of #1471. Only last two commits are new. Best review commit by commit.
The analysis keeps track of all witness instructions that lead to
Topat function entry, even if the flag-checkmach-details-cutoff nlimits the number of witnesses to be included in error message to somen > 0. This PR usesnas the apper bound on the size of the set of witnesses to be propagated.There are two commits. The first is a simple change to
jointo implement the above functionality.The second commit is refactoring of
Witnesses.ttype to keep track of whether join was in fact bounded or not, and propagate this information to function entry. This information is then used to print "..." at the end of error messages so the user knows when list of witnesses is partial. I am not entirely sure that the "dots" are worth the extra memory overhead of boolean field to track them. I'd be fine without it but wanted to get feedback first, or maybe there is a cheaper way to track it. I thought about tracking it per function but it breaks the abstractions.