SYNTHESIZER: Add quick filter into goto-synthesizer #7973
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
qinheping
requested review from
tautschnig,
feliperodri and
remi-delmas-3000
as code owners
qinheping
added
aws
qinheping
force-pushed
the
features/quick-filter
branch
from
44e2221 to
fdaf2b5
Compare
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## develop #7973 +/- ##
=========================================
Coverage 79.09% 79.09%
=========================================
Files 1699 1701 +2
Lines 196503 196625 +122
=========================================
+ Hits 155419 155527 +108
- Misses 41084 41098 +14 ☔ View full report in Codecov by Sentry. |
qinheping
force-pushed
the
features/quick-filter
branch
2 times, most recently
from
c38511c to
052df4a
Compare
|
I also modify the benchmark |
tautschnig
approved these changes
Nov 17, 2023
Comment on lines
+304
to
+307
| // Typecast `result` to the type of `expr`. | ||
| auto tmp_expr = from_integer(result, expr.type()); | ||
| to_integer(tmp_expr, result); | ||
| return result; |
There was a problem hiding this comment.
This piece of code (repeated below) looks strange. Are you really just doing a modulo operation here?
There was a problem hiding this comment.
The result is the evaluation of expr. result may be larger than the max of the type of expr and hence overflow. So I use from_integer and to_integer here to typecast the result to the type of expr to avoid overflow.
src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp
Outdated
Show resolved
Hide resolved
qinheping
force-pushed
the
features/quick-filter
branch
from
052df4a to
c4da2a9
Compare
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`, 61 out of 67 bad candidates are ruled out be the quick filter.
qinheping
force-pushed
the
features/quick-filter
branch
from
c4da2a9 to
195a296
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.
The quick filter check if a candidate invariant (predicates of type
exprt) is consistent with the previous seen examples by evaluating the candidate on the examples (valuations of variables collected from CBMC trace). The idea is that the 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 significantly reduce the number of candidate sent to CBMC. As an example, in the benchmark
loop_contracts_synthesis_04, 60 out of 67 bad candidatesare ruled out be the quick filter.