Features/quick filter fix bug vs2019 #3
Draft
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
Owner
qinheping
commented
Oct 21, 2023
qinheping
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
We do not currently have an implementation of calling conventions for any other platform. Fixes: diffblue#7934
When the `name` is not specified, the github UI uses the name of the first command as the step. This was misleading as it resulted in a 48 minute step titled "Run sudo apt-get update" which was also doing the build commands.
Given that the operation is taking the diff between function start and function end and applying it to a base, you would think that it should only have three domains. It previously had four and then copied the entire calling domain over the "this" domain, which was not otherwise used. This patch simplifies this and removes that oddity.
…e-way-merge Refactor/tidy up three way merge
…steps Add appropriate names to steps of code QL CI jobs
…yzer-config Restrict memory-analyzer build to Linux x86_64/i386
Collecting variables from trace will also collect those variables added during loop transformation, such as the car variables. Such variables should not appear in the loop contracts. This commit erases them from the terminals of the enumearting grammar used by the synthesizer.
…nals-in-synthesizer SYNTHESIZER: Use only symbols from the original goto as terminals
The function should scan all sub-expressions `it` of the given expression `expr` and check if `*it` has a given prefix.
The quick filter check if a candidate is consistent with the previous seen examples by evaluating the candidate on the examples. The idea is that quick filter is more efficient than CBMC for checking if a candidate is incorrect. So the synthesizer can use the quick filter to rule out incorrect candidates in an early stage before sending them to CBMC. In detail, we say a candidate is consistent with a positive (negative) example if the evaluation of the candidate on it is true (false). If a candidate is inconsistent with any example, it cannot be a valid loop invariant predicate. Examples are collected in the verification stage. In a CBMC trace, the valuations of variables upon the entry of the loop (loop_entry) must satisfy the loop invariants, so that they are positive examples. Oppositely, valuations of variables in the havoced iteration must not satisfy the loop invariants, so that they are negative examples. The quick filter sinificantly reduce the number of candidate sent to CBMC. As an example, in the benchmark `loop_contracts_synthesis_04`, 60 out of 67 bad candidates are ruled out be the quick filter.
qinheping
force-pushed
the
features/quick-filter-fix-bug-vs2019
branch
from
62e31b0
to
3fd1fbe
Compare
qinheping
force-pushed
the
features/quick-filter
branch
from
44e2221
to
fdaf2b5
Compare
qinheping
force-pushed
the
features/quick-filter-fix-bug-vs2019
branch
2 times, most recently
from
deead0a
to
ecfde8c
Compare
qinheping
force-pushed
the
features/quick-filter-fix-bug-vs2019
branch
from
ecfde8c
to
9cc2930
Compare
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.