Do not sort operands as part of simplification [blocks: #3486] #1997
Conversation
tautschnig
requested review from
kroening,
peterschrammel and
smowton
as code owners
tautschnig
force-pushed
the
no-sort-operands
branch
from
1a6002c to
44cce54
Compare
|
Does it make a difference whether or not the number of operands is large? |
It's just the plain number of compare operations. 163M |
tautschnig
force-pushed
the
no-sort-operands
branch
from
44cce54 to
51fcd8c
Compare
tautschnig
added
Needs data
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 51fcd8c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106401199
tautschnig
changed the title
|
Combined with #1998 this increases the number of |
tautschnig
removed
the
Needs data
| @@ -119,30 +119,31 @@ static const struct saj_tablet &sort_and_join( | |||
| return saj_table[i]; | |||
| } | |||
|
|
|||
| bool sort_and_join(exprt &expr) | |||
There was a problem hiding this comment.
Because it no longer necessarily sorts! A person reading sort_and_join(x, false); might reasonably suppose that regardless of what that false means, x is certainly now sorted.
|
(but do still please rename |
tautschnig
force-pushed
the
no-sort-operands
branch
from
51fcd8c to
84baff9
Compare
Codecov Report
@@ Coverage Diff @@
## develop #1997 +/- ##
========================================
Coverage 69.64% 69.65%
========================================
Files 1248 1248
Lines 100911 100921 +10
========================================
+ Hits 70284 70292 +8
- Misses 30627 30629 +2
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
no-sort-operands
branch
from
84baff9 to
ec4c8ee
Compare
| \[main.NaN.15\] line \d+ NaN on - in mynan - \(float\)n: SUCCESS | ||
| \[main.NaN.16\] line \d+ NaN on \* in mynan \* \(float\)n: SUCCESS | ||
| \[main.NaN.17\] line \d+ NaN on / in mynan / \(float\)n: SUCCESS | ||
| \[main.NaN.6\] line \d+ NaN on \+ in myinf \+ -myinf: FAILURE |
There was a problem hiding this comment.
Actually; this raises an interesting question. Floating-point addition and multiplication are commutative but not associative. If seems like normalising / sorting these would be worth while.
There was a problem hiding this comment.
I'm not sure I am able to follow: why would sorting (which this PR largely disables) be particularly beneficial for those operations? We surely can selectively re-enable sorting, but I don't think I understand the rationale just yet.
There was a problem hiding this comment.
float a;
float b;
if (!isnan(a) && !isnan(b)) {
assert(a + b === b + a);
}
Normalising the order of commutative-but-not-associative operations means we can resolve this at simplification, rather than an expensive solver call. It is not a massively common case but it is very cheap to implement and IIRC is a huge speed up in this case. Note that this can be purely local as it is not associative.
There was a problem hiding this comment.
It seems we didn't actually simplify such expressions before as commutative-but-not-associative operations were exempt. I have now added 375f208 to take care of this, thank you very much for raising this!
tautschnig
force-pushed
the
no-sort-operands
branch
from
ec4c8ee to
72b4c1d
Compare
tautschnig
force-pushed
the
no-sort-operands
branch
from
d89f368 to
67294c2
Compare
tautschnig
force-pushed
the
no-sort-operands
branch
2 times, most recently
from
913d861 to
eae7a64
Compare
String refinement may or may not be successful (resulting in "ERROR" results rather than "FAILURE") when working on an unconstrained string (which the null dereference yields), depending on the models returned by the SAT solver.
Data for ReachSafety-BitVectors, the smallest of SV-COMP's categories, running for at most 600s per benchmark: 163M sort_operands calls, contributing to 1B irept::operator< calls, resulting in 4.5B irept::compare calls. None of these calls are actually necessary. As part of this work, also clean up naming of "sort_and_join" functions (as most of them don't actually sort or join, but instead just prepare for doing so).
tautschnig
force-pushed
the
no-sort-operands
branch
from
eae7a64 to
9e5434b
Compare
Testing floating-point equality is expensive, and thus warrants handling special cases (even if they might be rare) in the simplifier. This (simplistic) test would take 5 seconds with CaDiCaL as SAT back-end when not performing simplification.
Do-not-merge as above: this needs proper profiling to confirm the effect with data.