Skip to content

Restrict with_exprt to exactly three operands - #8674

Merged
tautschnig merged 2 commits into
diffblue:developfrom
tautschnig:three-operand-with
Jul 9, 2025
Merged

Restrict with_exprt to exactly three operands#8674
tautschnig merged 2 commits into
diffblue:developfrom
tautschnig:three-operand-with

Conversation

@tautschnig

@tautschnigtautschnig commented Jul 5, 2025

Copy link
Copy Markdown
Collaborator

We cannot build a C++ API for the previous >= 3, odd-number operand variant. Alas, we ended up with various places in the code base silently ignoring additional operands, which led to wrong verification results in Kani as recent changes in CBMC made increasing use of the value set (which is one of the places that silently ignored additional operands).

This is an alternative solution over #8668: #8668 does also fix the wrong verification results, but does not resolve original design problem. This PR now seeks to address both the bug and the design problem, and does so by largely just removing code.

Resolves: #7272

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a 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).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov

codecovBot commented Jul 5, 2025

Copy link
Copy Markdown

Codecov Report

Attention: Patch coverage is 92.38095% with 16 lines in your changes missing coverage. Please review.

Project coverage is 80.40%. Comparing base (e88ed5f) to head (fc5c5a0).
Report is 5 commits behind head on develop.

Files with missing linesPatch %Lines
src/goto-programs/graphml_witness.cpp0.00%12 Missing ⚠️
src/util/simplify_expr.cpp92.30%3 Missing ⚠️
...vers/smt2_incremental/encoding/struct_encoding.cpp87.50%1 Missing ⚠️
Additional details and impacted files
@@ Coverage Diff @@## develop #8674 +/- ##
===========================================
+ Coverage 80.39% 80.40% +0.01% 
===========================================
Files 1688 1688 Lines 207387 207380 -7 Branches 73 73 ===========================================
+ Hits 166728 166744 +16 + Misses 40659 40636 -23 

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@rod-chapman

Copy link
Copy Markdown
Collaborator

Test results for this branch running on mldsa-native/main are all good.

@rod-chapman

Copy link
Copy Markdown
Collaborator

Test results for this branch running on mlkem-native/main are all good.

@tautschnigtautschnig added bugfix soundness Soundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't. labels Jul 7, 2025
This is in preparation of moving to 3-operand with-expressions: without
intervening use of the simplifier some generated expressions could
become unnecessarily large.
We cannot build a C++ API for the previous >= 3, odd-number operand
variant. Alas, we ended up with various places in the code base silently
ignoring additional operands, which led to wrong verification results in
Kani as recent changes in CBMC made increasing use of the value set
(which is one of the places that silently ignored additional operands).
Resolves: diffblue#7272
@tautschnig
tautschnig merged commit ea7b092 into diffblue:developJul 9, 2025
@tautschnig
tautschnig deleted the three-operand-with branch July 9, 2025 18:38
tautschnig added a commit to tautschnig/cbmc that referenced this pull request Jul 9, 2025
This release addresses bugs in our handling of array-update ("with")
expressions (via diffblue#8674) and gaps in our C17/C23 support (via diffblue#8673).
@tautschnigtautschnig mentioned this pull request Jul 9, 2025
4 tasks
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bugfixsoundnessSoundness bug? Review and add "aws" if it is, or remove "soundness" if it isn't.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Construction of with expression in lowering/byte_operators.cpp does not match getters in with_exprt [rfc]

4 participants

@tautschnig@rod-chapman@kroening@peterschrammel