Don't generate unnecessary fresh symbols for the GOTO trace #7021
Conversation
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
Codecov ReportBase: 78.26% // Head: 77.86% // Decreases project coverage by
Additional details and impacted files@@ Coverage Diff @@
## develop #7021 +/- ##
===========================================
- Coverage 78.26% 77.86% -0.40%
===========================================
Files 1642 1569 -73
Lines 189830 180969 -8861
===========================================
- Hits 148568 140913 -7655
+ Misses 41262 40056 -1206
Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here. ☔ View full report at Codecov. |
tautschnig
force-pushed
the
cleanup/no-unnecessry-fresh-symbols
branch
from
a0295ee to
537ebd6
Compare
tautschnig
requested review from
kroening,
martin-cs,
peterschrammel,
thomasspriggs,
NlightNFotis,
TGWDB and
romainbrenguier
as code owners
tautschnig
assigned kroening, peterschrammel, martin-cs, NlightNFotis, thomasspriggs and TGWDB
tautschnig
force-pushed
the
cleanup/no-unnecessry-fresh-symbols
branch
from
537ebd6 to
5d892f4
Compare
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Jul 22, 2022
Avoid creating equalities over the postponed bitvector when the object literals trivially aren't equal, and directly encode bitwise equality when the object literals are trivially equal (and stop searching for a matching object). In all other cases, avoid unnecessary Tseitin variables to encode the postponed bitvector equality. When running on various proofs done for AWS open-source projects, this changes the performance as follows (when comparing to diffblue#7021): with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26779.7 to 22409.9 seconds (4369.8 seconds speed-up); with Minisat, however, the hardest 49 proofs take 28616.7 instead of 28420.4 seconds (196.3 seconds slow-down). Across these benchmarks, 11.7% of variables and 12.8% of clauses are removed.
4 tasks
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Aug 11, 2022
This was previously disabled as it appeared to degrade performance. New benchmarking, however, suggests considerable performance improvement: When running on various proofs done for AWS open-source projects, this changes the performance as follows (when comparing to diffblue#7021): with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26779.7 to 24472.6 seconds (2307.1 seconds speed-up); with Minisat the hardest 49 proofs take 18541.2 instead of 28420.4 seconds (9879.2 seconds speed-up). Across these benchmarks, 1.0% of variables and 3.2% of clauses are removed.
4 tasks
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Aug 11, 2022
This was previously disabled as it appeared to degrade performance. New benchmarking, however, suggests considerable performance improvement: When running on various proofs done for AWS open-source projects, this changes the performance as follows (when comparing to diffblue#7021): with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26779.7 to 24472.6 seconds (2307.1 seconds speed-up); with Minisat the hardest 49 proofs take 18541.2 instead of 28420.4 seconds (9879.2 seconds speed-up). Across these benchmarks, 1.0% of variables and 3.2% of clauses are removed.
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Aug 12, 2022
Avoid creating equalities over the postponed bitvector when the object literals trivially aren't equal, and directly encode bitwise equality when the object literals are trivially equal (and stop searching for a matching object). In all other cases, avoid unnecessary Tseitin variables to encode the postponed bitvector equality. When running on various proofs done for AWS open-source projects, this changes the performance as follows (when comparing to diffblue#7021): with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26779.7 to 22409.9 seconds (4369.8 seconds speed-up); with Minisat, however, the hardest 49 proofs take 28616.7 instead of 28420.4 seconds (196.3 seconds slow-down). Across these benchmarks, 11.7% of variables and 12.8% of clauses are removed.
tautschnig
force-pushed
the
cleanup/no-unnecessry-fresh-symbols
branch
from
5d892f4 to
30c9bce
Compare
|
I love the performance graphs but please can we have the diagonal line so it is easy to see better / worse. |
martin-cs
approved these changes
Aug 13, 2022
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Aug 13, 2022
This was previously disabled as it appeared to degrade performance. New benchmarking, however, suggests considerable performance improvement: When running on various proofs done for AWS open-source projects, this changes the performance as follows (when comparing to diffblue#7021): with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26779.7 to 24472.6 seconds (2307.1 seconds speed-up); with Minisat the hardest 49 proofs take 18541.2 instead of 28420.4 seconds (9879.2 seconds speed-up). Across these benchmarks, 1.0% of variables and 3.2% of clauses are removed.
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Aug 14, 2022
This was previously disabled as it appeared to degrade performance. New benchmarking, however, suggests considerable performance improvement: When running on various proofs done for AWS open-source projects, this changes the performance as follows (when comparing to diffblue#7021): with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26779.7 to 24472.6 seconds (2307.1 seconds speed-up); with Minisat the hardest 49 proofs take 18541.2 instead of 28420.4 seconds (9879.2 seconds speed-up). Across these benchmarks, 1.0% of variables and 3.2% of clauses are removed. INCLUDE_REDUNDANT_CLAUSES is not enabled: while this would yield a further speed-up of 1080.4 seconds with CaDiCaL, it slows down Minisat by 4440.6 seconds on the above benchmark set.
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this pull request
Aug 14, 2022
This was previously disabled as it appeared to degrade performance. New benchmarking, however, suggests considerable performance improvement: When running on various proofs done for AWS open-source projects, this changes the performance as follows (when comparing to diffblue#7021): with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26779.7 to 24472.6 seconds (2307.1 seconds speed-up); with Minisat the hardest 49 proofs take 18541.2 instead of 28420.4 seconds (9879.2 seconds speed-up). Across these benchmarks, 1.0% of variables and 3.2% of clauses are removed. INCLUDE_REDUNDANT_CLAUSES is not enabled: while this would yield a further speed-up of 1080.4 seconds with CaDiCaL, it slows down Minisat by 4440.6 seconds on the above benchmark set.
|
This is not a good idea. I'd first like to understand how the speedup works. And then I'd like to push that change into the decision procedure. The user of the decision procedure (here symex) shouldn't have to care about encoding tricks that are this low level. |
tautschnig
force-pushed
the
cleanup/no-unnecessry-fresh-symbols
branch
2 times, most recently
from
57d6542 to
81afb57
Compare
tautschnig
changed the title
tautschnig
changed the title
tautschnig
changed the title
We can safely record the values of expressions by adding `expr == expr` as constraints in order to be able to fetch and display them in the GOTO trace. This was already being done for declarations. Introducing new symbols just adds unnecessary variables to the formula. When running on various proofs done for AWS open-source projects, this changes the performance as follows: with CaDiCaL as back-end, the total solver time for the hardest 46 proofs changes from 26546.5 to 26779.7 seconds (233.2 seconds slow-down); with Minisat, however, the hardest 49 proofs take 28420.4 instead of 32387.2 seconds (3966.8 seconds speed-up). Across these benchmarks, 1.7% of variables and 0.6% of clauses are removed.
tautschnig
force-pushed
the
cleanup/no-unnecessry-fresh-symbols
branch
from
81afb57 to
c7f67c6
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.
We can safely record the values of expressions by adding
expr == expras constraints in order to be able to fetch and display them in the GOTO
trace. This was already being done for declarations. Introducing new
symbols just adds unnecessary variables to the formula.
When running on various proofs done for AWS open-source projects, this
changes the performance as follows: with CaDiCaL as back-end, the total
solver time for the hardest 46 proofs changes from 26546.5 to 26779.7
seconds (233.2 seconds slow-down); with Minisat, however, the hardest 49
proofs take 28420.4 instead of 32387.2 seconds (3966.8 seconds
speed-up). Across these benchmarks, 1.7% of variables and 0.6% of
clauses are removed.