Fix support for with_exprt with more than 3 operands
#8668
Conversation
A `with_exprt` needs to have at least 3 operands, but can encode multiple updates when using more operands (where any further operands need to come in pairs of two: an index/member and a new value). We already support this in several places, but were still missing support in others. This led to wrong verification results in Kani as recent changes in CBMC make increasing use of the value set (which is among those fixed in this commit).
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
tautschnig
added
bugfix
soundness
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8668 +/- ##
===========================================
- Coverage 80.39% 80.39% -0.01%
===========================================
Files 1688 1688
Lines 207391 207414 +23
Branches 73 73
===========================================
+ Hits 166730 166746 +16
- Misses 40661 40668 +7 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
|
Test results for mlkem-native/main, mldsa-native/main and mldsa-native/remove_8617 are all good. |
| out << smt2_format(with_expr.old()) << ' '; | ||
| for(std::size_t i = 1; i < with_expr.operands().size(); i += 2) | ||
| { | ||
| out << smt2_format(with_expr.operands()[i]) << ' ' |
There was a problem hiding this comment.
This is code is never used so I don't know for sure, but which reason do you have to believe it does not?
There was a problem hiding this comment.
store appears to exist as a three-operand variant only: https://smt-lib.org/theories-ArraysEx.shtml
There was a problem hiding this comment.
Ah, sure, but note how the prior loop creates (store (store (store ... (lines 142 and 143).
| */ | ||
|
|
||
| if(value.id()==ID_with) | ||
| if(value.id() == ID_with && value.operands().size() == 3) |
There was a problem hiding this comment.
It may be worth considering to rewrite with expressions with >3 operands to the 3 operand variant.
There was a problem hiding this comment.
If we make the simplifier do this, we might as well refrain from constructing those in the first place? I'm actually inclined to create such a PR as an alternative to this one.
|
Replaced by #8674 |
|
Closing in favour of #8674. |
4 participants
A
with_exprtneeds to have at least 3 operands, but can encode multiple updates when using more operands (where any further operands need to come in pairs of two: an index/member and a new value). We already support this in several places, but were still missing support in others. This led to wrong verification results in Kani as recent changes in CBMC make increasing use of the value set (which is among those fixed in this commit).