Handle quantifiers with statement expressions

[qinheping]

This pull request addresses the issue of handling quantifiers that contain statement expressions in CBMC. This fix ensures that CBMC can correctly process and verify programs that use quantifiers with statement expressions.

Changes

• goto_clean_expr.cpp: Added logic to handle quantifiers with statement expressions. This includes:
  • A new function find_base_symbol to identify the base symbol in an expression.
  • Modifications to clean_expr to handle quantifiers with statement expressions by converting them pure expressions.
• c_typecheck_expr.cpp: Updated to allow quantifiers with statement expressions.
• Tests: Introduced new tests to verify the correct handling of quantifiers with statement expressions. These tests ensure that CBMC can process and verify programs that use such quantifiers without errors.

Motivation and Context

Statement expressions may not contain side effects, and should be accepted as quantifier bodies when they don't.
Supporting quantifiers with statement expressions enhances CBMC's capability to handle a broader range of programs, e.g., GOTO program compiled from Rust MIR model-checking/kani#3737.

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

[kroening]

I am sure it makes sense to extend what's allowed in quantifiers. I am surprised by the choice of a (fragment) of statement expressions, which are a gcc extension at the C language level. In particular, note that this means you can't actually use these in Kani.

The examples suggest that you are perhaps looking for let expressions? These are unproblematic to use in quantifiers, and Kani can use these right away.

[qinheping]

In particular, note that this means you can't actually use these in Kani.

Kani is actually the motivation of support statement expressions in quantifiers. In Kani, we generate GOTO programs from Rust MIR. However, all Rust expressions will be compiled into a sequence of statements (including decl, assign, and conditional goto) in Rust MIR. We typically wrap all such statements into a closure function (in Rust) so that the evaluation of the Rust expressions becomes a single function call in GOTO. This approach doesn't work here because function calls are also side-effect expressions in GOTO. Therefore, we are considering inlining all function calls in MIR and generating a statement expression in GOTO from the inlined expression.

I don't think let-expressions are enough here because there will still be function calls or statement expressions in the where clauses of the let-expressions.

[kroening]

Kani is actually the motivation of support statement expressions in quantifiers. In Kani, we generate GOTO programs from Rust MIR. However, all Rust expressions will be compiled into a sequence of statements (including decl, assign, and conditional goto) in Rust MIR. We typically wrap all such statements into a closure function (in Rust) so that the evaluation of the Rust expressions becomes a single function call in GOTO. This approach doesn't work here because function calls are also side-effect expressions in GOTO. Therefore, we are considering inlining all function calls in MIR and generating a statement expression in GOTO from the inlined expression.

I don't think let-expressions are enough here because there will still be function calls or statement expressions in the where clauses of the let-expressions.

Ok, then how about defining the concept of a "pure" function, and then allowing those in quantifiers?

We need that in the front-end anyway, for C++'s constexpr.

[tautschnig]

A few initial comments, still need to work through the core piece of the implementation (see my "Note to self").

[tautschnig]

We need that in the front-end anyway, for C++'s constexpr.

But then constexpr has C++-standards-version-specific peculiarities, so a single definition might not work? I had pointed @qinheping to my constexpr implemention in #8386 as an initial guidance, though.

[qinheping]

Ok, then how about defining the concept of a "pure" function, and then allowing those in quantifiers?

In the design of this PR, no function calls are allowed in quantifiers.

[codecov]

Codecov Report

Attention: Patch coverage is 65.33333% with 52 lines in your changes missing coverage. Please review.

Project coverage is 79.17%. Comparing base (f55f636) to head (7969993).
Report is 4 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/ansi-c/goto-conversion/goto_clean_expr.cpp	64.58%	51 Missing ⚠️
src/ansi-c/c_typecheck_expr.cpp	83.33%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8605      +/-   ##
===========================================
- Coverage    79.63%   79.17%   -0.46%     
===========================================
  Files         1733     1733              
  Lines       197704   198973    +1269     
  Branches     17963    17967       +4     
===========================================
+ Hits        157438   157536      +98     
- Misses       40266    41437    +1171     

☔ 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.