Cache scanner after kompile and reuse during k-compile-search-pattern#2390
Merged
rv-jenkins merged 12 commits intomasterfrom Jan 11, 2022
Merged
Cache scanner after kompile and reuse during k-compile-search-pattern#2390rv-jenkins merged 12 commits intomasterfrom
kompile and reuse during k-compile-search-pattern#2390rv-jenkins merged 12 commits intomasterfrom
Conversation
added 10 commits
January 10, 2022 14:54
dwightguth
force-pushed
the
cache_scanner
branch
from
b209189 to
054220e
Compare
radumereuta
reviewed
Jan 11, 2022
Contributor
radumereuta
left a comment
radumereuta
left a comment
There was a problem hiding this comment.
Just one comment.
I'll let @SchmErik give the final approval
| return scanner; | ||
| } | ||
| public void setScanner(Scanner s) { | ||
| scanner = s; |
Contributor
There was a problem hiding this comment.
Everything here is indented by 4. This line is indented only by 2.
SchmErik
approved these changes
Jan 11, 2022
Contributor
SchmErik
left a comment
SchmErik
left a comment
There was a problem hiding this comment.
Looks good to me. I think this brings up a few questions about the code base but I'll ask them internally. @dwightguth I'll approve but please address @radumereuta before placing the automerge label
dwightguth
pushed a commit
that referenced
this pull request
Jan 21, 2022
…ern` (#2390) * fix bug where command line invocation was not printed with -v * delete dead code * code to serialize scanner * implement Comparable on TerminalLike * make tokens deterministic in numbering * implement code to deserialize scanner * add tests for bug * fix #2372 - false negative of invalid precedence error * fix bug involving syntax added by compiler to main module * fix precedence conflict in test * Fix indent Co-authored-by: rv-jenkins <admin@runtimeverification.com>
rv-jenkins
added a commit
that referenced
this pull request
Jan 25, 2022
* Cache scanner after `kompile` and reuse during `k-compile-search-pattern` (#2390) * fix bug where command line invocation was not printed with -v * delete dead code * code to serialize scanner * implement Comparable on TerminalLike * make tokens deterministic in numbering * implement code to deserialize scanner * add tests for bug * fix #2372 - false negative of invalid precedence error * fix bug involving syntax added by compiler to main module * fix precedence conflict in test * Fix indent Co-authored-by: rv-jenkins <admin@runtimeverification.com> * don't cache scanner in kprove Co-authored-by: rv-jenkins <admin@runtimeverification.com>
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
4 participants
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.
This PR will serialize the scanner during kompile and then reuse that scanner when compiling search patterns rather than having to recreate the scanner. This significantly brings down the time spent in
k-compile-search-patternwhen runningkrun --pattern.The reason this diff is so large is that we have to ensure that the set of tokens in kompile and k-compile-search-pattern are exactly identical and in the same order, thus necessitating some work to ensure that tokens in the scanner get emitted in a completely deterministic ordering.
I will make kprovex also use this scanner in a followup PR. Note, however, that this will not be possible if the specification has macros in it... If we decide to support this case, we will have to fall back on recreating the scanner in the prover if the user does this. Thoughts?
I also fix a couple other minor unrelated bugs, including:
krun -vprecattribute.