Add --evaluation-order-check for unspecified evaluation order

[tautschnig]

The C and C++ standards leave the evaluation order within expressions largely open: the operands of most operators and the arguments of a function call are evaluated in an unspecified order (C11 6.5p3, 6.5.2.2p10), and per C11 3.4.4 that choice need not be consistent between two instances in one program, so the order observed for a given compiler is not a guarantee. Function executions do not interleave with other evaluations (they are indeterminately sequenced), and unsequenced conflicting accesses to the same scalar object in open code are undefined behaviour outright (C11 6.5p2).

Goto conversion, like other verifiers that lower expressions to statement sequences, picks one evaluation order per expression. That is sound if and only if the expression's value and effect are independent of the orders the standard permits; when they are not, verification against the single modelled order can miss behaviours of a conforming compiler. For example, in

int b = 0;
int f(void) { b = 1; return 0; }
... a / b + f() ...

goto conversion hoists f's side effects before the division, so the division by zero that occurs when a compiler evaluates a / b first (gcc does, on several architectures) goes unnoticed.

The new option --evaluation-order-check makes this sound: whenever the lowering of a full expression involves side effects next to sibling sub-evaluations, goto conversion now

• snapshots the value of each side-effect-free sibling operand in the state before any of the side effects, and asserts after each side-effect block that the value is unchanged; the assertions fail exactly when a permitted evaluation order can observe a different value, and evaluating the operands in the pre-state also applies the enabled undefined-behaviour checks (division by zero, overflow, pointer checks) to that state;
• executes the side-effect blocks of sibling operands, which are mutually independent by construction, in a nondeterministically chosen order, using round-based scheduling (each round executes one not-yet-executed block selected by an unconstrained choice), which covers all k! orders of k blocks while emitting only k copies of each block, so no bound on the number of unsequenced side effects is needed.

When all emitted evaluation-order assertions hold, the expression's value and the resulting state are the same under every evaluation order the standard permits at the granularity of sibling operands, and the fixed lowering order is a complete model. Known limitations, by design of this first version: unsequenced conflicts between an assignment's left-hand side and its right-hand side (i = i++ + 1) are not detected (the lhs is lowered separately); interleavings within one operand's evaluation relative to its siblings are only explored at operand granularity; reads of aggregate-typed operands are not snapshotted.

The check is off by default: the fixed per-target evaluation order (introduced for function-call arguments in #9120) remains the best model of what deployed compilers were observed to do, and the pre-#9120 behaviour was equally a single fixed order. The comment documenting configt::ansi_ct::argument_evaluation_order is reworded to make explicit that the recorded orders are observations, not guarantees, and to point to the new option.

The regression tests double as documentation of the semantics discussed in the review of #9120, including both directions of the division-by-zero example and the two-writes example where the fixed order would wrongly prove an assertion. The previously FUTURE tests Eval_Order2 and Function_Eval_Order1, which documented the aspiration of modelling evaluation-order nondeterminism, are promoted to CORE using the new option.

• 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).
• 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.

[Copilot]

Pull request overview

This PR adds a new --evaluation-order-check mode to C/C++ goto-conversion to detect when a single fixed lowering order is unsound because expression values/effects depend on evaluation orders left unspecified by the language standards. It does so by snapshotting side-effect-free sibling reads and by exploring permutations of sibling side-effect blocks via nondeterministic scheduling, and it adds regression tests that document the expected semantics.

Changes:

• Introduce config.ansi_c.evaluation_order_check and a --evaluation-order-check command-line option.
• Extend goto-conversion expression cleaning to (a) snapshot candidate reads and assert invariance, and (b) schedule side-effect blocks in nondeterministic round-based order.
• Add/promote regression tests covering order-dependent reads/writes and division-by-zero cases, and promote previously FUTURE tests to CORE under the new option.

Reviewed changes

Copilot reviewed 22 out of 22 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/util/config.h	Adds help/option wiring for --evaluation-order-check and stores the config flag in configt::ansi_ct.
src/util/config.cpp	Parses --evaluation-order-check into config.ansi_c.evaluation_order_check.
src/ansi-c/goto-conversion/module_dependencies.txt	Adds langapi dependency for language_util usage in new diagnostics/comments.
src/ansi-c/goto-conversion/goto_convert_class.h	Adds clean_expr_depth tracking and declares the new helper to emit checked/scheduled blocks.
src/ansi-c/goto-conversion/goto_clean_expr.cpp	Implements snapshot-candidate detection, depth tracking, operand-wise cleaning, and nondeterministic scheduling + boundary assertions.
regression/cbmc/Function_Eval_Order1/test.desc	Promotes test to CORE and runs it under --evaluation-order-check to demonstrate refuted assertions under differing orders.
regression/cbmc/Eval_Order2/test.desc	Promotes test to CORE and runs it under --evaluation-order-check to demonstrate detected order dependence.
regression/cbmc/evaluation_order_check/test.desc	New CORE test driver covering division-by-zero + evaluation-order dependence scenario.
regression/cbmc/evaluation_order_check/unsequenced_increment.desc	New CORE test showing evaluation-order dependence for an unsequenced increment/read pattern.
regression/cbmc/evaluation_order_check/unsequenced_increment.c	Test program for unsequenced increment/read case.
regression/cbmc/evaluation_order_check/pure_calls.desc	New CORE test asserting no evaluation-order properties are generated in an order-independent case.
regression/cbmc/evaluation_order_check/pure_calls.c	Test program for order-independent calls.
regression/cbmc/evaluation_order_check/four_independent_writes.desc	New CORE test for commutative independent side effects across 4 operands.
regression/cbmc/evaluation_order_check/four_independent_writes.c	Test program for four independent writes case.
regression/cbmc/evaluation_order_check/four_conflicting_writes.desc	New CORE test demonstrating differing results across 24 possible orders.
regression/cbmc/evaluation_order_check/four_conflicting_writes.c	Test program for four conflicting writes case.
regression/cbmc/evaluation_order_check/division_before_call.desc	New CORE test demonstrating missed div-by-zero without the check and detected dependence with it.
regression/cbmc/evaluation_order_check/division_before_call.c	Test program for division-before-call scenario.
regression/cbmc/evaluation_order_check/division_before_call_no_check.desc	New CORE test documenting baseline (unchecked) behavior.
regression/cbmc/evaluation_order_check/division_after_call.c	Test program for division-after-call scenario driven by evaluation_order_check/test.desc.
regression/cbmc/evaluation_order_check/conflicting_writes.desc	New CORE test showing refutation when side effects don’t commute.
regression/cbmc/evaluation_order_check/conflicting_writes.c	Test program for conflicting writes case.

Suppressed comments (1)

src/ansi-c/goto-conversion/goto_clean_expr.cpp:1128

• After widening choice_symbol, the per-arm guard still compares against from_integer(i, unsignedbv_typet{8}), which will truncate for i >= 256. This should use the same choice_type as the choice variable.

      const and_exprt guard{
        equal_exprt{
          choice_symbol.symbol_expr(), from_integer(i, unsignedbv_typet{8})},
        not_exprt{done_flags[i]}};

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[rod-chapman]

Could I also have a --no-function-side-effects flag that would simply reject functions that have any side-effect when called in the context of an expression? (so... void functions can have side-effects when called as part of a statment are OK). That's how Frama-C and SPARK/Ada do it.

[kroening]

Could I also have a --no-function-side-effects flag that would simply reject functions that have any side-effect when called in the context of an expression? (so... void functions can have side-effects when called as part of a statment are OK). That's how Frama-C and SPARK/Ada do it.

This would render a large chunk of the standard C library unusable?

[codecov]

Codecov Report

❌ Patch coverage is 94.24460% with 8 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.85%. Comparing base (a777c7b) to head (e55aaf5).
⚠️ Report is 2 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/ansi-c/goto-conversion/goto_clean_expr.cpp	94.20%	8 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9152      +/-   ##
===========================================
+ Coverage    80.83%   80.85%   +0.01%     
===========================================
  Files         1715     1715              
  Lines       189989   190127     +138     
  Branches        73       73              
===========================================
+ Hits        153576   153720     +144     
+ Misses       36413    36407       -6     

☔ View full report in Codecov by Harness.
📢 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]

Fair point - I think Frama-C allows allows non-overlapping side-effects in simple cases where there are no binary operators in the expression, so things like

e = memset_s(&dest, 4, &src, 4);

is OK, but

e = memset_s(&e, 4, &src, 4);

is rejected.

[rod-chapman]

I am pleased to report that both mlkem-native and mldsa-native proofs are all OK for all parameter sets, with --evaluation-order-check added to their Makefile.common