Generate triggers more conservatively #708
Merged
Conversation
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
…ate triggers if subset of operators is used where we know a trigger is valid or invalid. Do not generate triggers if operators are in neither of the valid/invalid sets.
…and disallowed (integer minus) in triggers.
pieter-bos
approved these changes
Oct 26, 2021
|
SonarCloud Quality Gate failed. |
|
There are some files that still have quite a few trigger warnings (kadane.java, set comprehension code generation, KeYAbruptTerminationChallenge.java, basic-examples.c, kernel-example-v3.pvl, forkjoininforloop.pvl, and max-sort.pvl), but these can be resolved in a new PR by actually adding the proper triggers. Some other files also have trigger warnings, but in those cases a trigger is not actually possible (i.e. (\forall int tid; f(tid - 1)). |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 ensures that triggers are only generated for expressions that use a subset of operators. For this subset of operators it is known for each operator if it is allowed to appear in a trigger or not. For example, + is not allowed in a trigger, but sequence size (
|xs|) is. If an operator is encountered that is not included in this subset, no trigger is generated for the nearest enclosing forall.This PR also includes a fix for including tuple notation in the syntax, which was also needed for Han's thesis.