Record function argument evaluation order in configt::ansi_ct by tautschnig · Pull Request #9120 · diffblue/cbmc

tautschnig · 2026-07-19T10:43:58Z

As suggested by @kroening in #8991 (comment): record the target's function argument evaluation order as an architectural parameter in configt::ansi_ct — and use it during goto conversion.

The C and C++ standards leave the order of evaluation of function call arguments unspecified, but any given compiler/architecture combination uses a fixed order, observable when argument expressions have side effects. Empirically verified (test programs on native x86_64 and aarch64 hosts, cross-compilation + qemu-user, and Compiler Explorer for MSVC and gcc -mx32):

compiler	architectures	order
GCC 13	i386, x86_64, x32	right-to-left
GCC 13	arm64, arm (32-bit), riscv64, ppc64le, mips64el, s390x, sparc64	left-to-right
Clang 18	x86_64, arm64	left-to-right
MSVC v19.latest	x86, x64, arm64	right-to-left

Changes:

New architectural parameter configt::ansi_ct::argument_evaluation_order, set in each set_arch_spec_* function (matching the pattern of the other architectural parameters — important because goto-cc's -m16/-m32/-mthumb handling invokes those functions directly, bypassing set_arch) and re-derived when goto-cc switches the compiler flavour after configuring the architecture (goto-clang/goto-cl). Exposed as __CPROVER_architecture_argument_evaluation_order, and restored when loading goto binaries (tolerating older binaries that lack the symbol, following the precedent of the os entry).
Goto conversion now honours the parameter when lowering side effects in function call arguments, closing the long-standing // TODO: evaluation order in clean_expr. Previously arguments were always evaluated left-to-right, mis-modelling e.g. gcc on x86_64. All function-call lowering paths (subexpressions, plain assignment statements, do_function_call) share one helper, so the modelled order does not depend on the syntactic context of the call.
The pre-existing test Function_Eval_Order2, which documented the fixed left-to-right lowering, now pins an architecture where that order is real (--arch arm64); new regression tests cover both orders. These tests use preprocessed (.i) inputs so that no target-specific flags reach the native preprocessor on any CI host (pinning --arch with .c inputs breaks on the ARM runners, cf. the first CI iteration of this PR).
Unit tests cover the architecture/flavour matrix and the goto-binary restore path (both the symbol-present and the old-binary branch).
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.
n/a 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

Adds a new architectural configuration parameter to CBMC’s configt::ansi_ct to record the target/compiler’s function-argument evaluation order, persists it into the architecture symbols (__CPROVER_architecture_*) in goto binaries, and restores it when loading those binaries (with backward compatibility for older binaries).

Changes:

Introduce configt::ansi_ct::argument_evaluation_order and set it per architecture + compiler flavour (notably x86-family GCC/MSVC vs others).
Emit the parameter as __CPROVER_architecture_argument_evaluation_order in internal additions, and restore it from the symbol table when reading goto binaries.
Add unit + regression tests to validate the architecture/flavour matrix and symbol-table plumbing.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
`unit/util/argument_evaluation_order.cpp`	New unit test validating evaluation order across architecture/flavour combinations.
`unit/Makefile`	Adds the new unit test file to the unit build (Makefile path).
`src/util/config.h`	Defines the new `argument_evaluation_order` enum/field on `configt::ansi_ct`.
`src/util/config.cpp`	Sets defaults/overrides per arch; restores from symbol table if present.
`src/ansi-c/ansi_c_internal_additions.cpp`	Emits the new architecture symbol into the internal additions.
`regression/cbmc/architecture_argument_evaluation_order/test.desc`	Regression test ensuring the symbol appears in `--show-symbol-table`.
`regression/cbmc/architecture_argument_evaluation_order/main.c`	Minimal input program for the regression test.

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

codecov · 2026-07-19T11:40:54Z

Codecov Report

❌ Patch coverage is 85.36585% with 18 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.83%. Comparing base (ff8e112) to head (26c7414).

Files with missing lines	Patch %	Lines
src/util/config.cpp	67.34%	16 Missing ⚠️
src/ansi-c/ansi_c_internal_additions.cpp	66.66%	1 Missing ⚠️
src/goto-cc/ms_cl_mode.cpp	0.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9120      +/-   ##
===========================================
+ Coverage    80.77%   80.83%   +0.05%     
===========================================
  Files         1712     1715       +3     
  Lines       189833   189948     +115     
  Branches        73       73              
===========================================
+ Hits        153347   153537     +190     
+ Misses       36486    36411      -75

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

The C and C++ standards leave the order of evaluation of function call arguments unspecified, but any given compiler/architecture combination uses a fixed order, which is observable when argument expressions have side effects. Empirically (test programs on native and cross-compiled targets, and via Compiler Explorer): GCC evaluates right-to-left on the x86 family (i386, x86_64, x32) and left-to-right on all other architectures tested (arm64, arm, riscv64, ppc64le, mips64el, s390x, sparc64); Visual Studio evaluates right-to-left on all architectures tested (x86, x64, arm64); Clang evaluates left-to-right on all architectures tested (x86_64, arm64). Record this architectural parameter in configt::ansi_ct, setting it in each set_arch_spec_* function like the other architectural parameters (some of those functions are invoked directly by goto-cc's handling of -m16/-m32/-mthumb and friends, bypassing set_arch), and re-deriving it in goto-cc when the compiler flavour is switched after the architecture has been configured (goto-clang and goto-cl set the mode only after config.set). Expose it as __CPROVER_architecture_argument_evaluation_order, and restore it when loading goto binaries (tolerating older binaries that lack the symbol). Use the parameter during goto conversion when lowering side effects in function call arguments, which were previously always evaluated left-to-right, closing the 'TODO: evaluation order' in clean_expr. All lowering paths for function calls (subexpressions, plain assignment statements via convert_assign, and do_function_call) share a helper so that the modelled order does not depend on the syntactic context of the call. The pre-existing test Function_Eval_Order2, which documented the fixed left-to-right lowering, now pins an architecture that evaluates left-to-right; new regression tests check both evaluation orders and both lowering paths using preprocessed input files so that no target-specific flags reach the native preprocessor on any CI host. The practical relevance of this parameter was demonstrated while investigating cross-platform proof-time instability (issue diffblue#8991): Z3 built with GCC on x86_64 and aarch64 takes different solver paths on byte-identical input because AST node identifiers are assigned in argument evaluation order (fixed upstream in Z3Prover/z3#10165). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

rod-chapman · 2026-07-28T10:41:10Z

I have soundness concerns over this PR. Your assertion that "any given compiler/architecture combination uses a fixed order" is not correct as per my understanding of the ISO C standard, and the behaviour of optimizing compilers.

kroening · 2026-07-28T10:45:28Z

I have soundness concerns over this PR. Your assertion that "any given compiler/architecture combination uses a fixed order" is not correct as per my understanding of the ISO C standard, and the behaviour of optimizing compilers.

"any given" -> "any supported".

rod-chapman · 2026-07-28T11:05:53Z

What do you mean "supported"? That makes no sense to me. It doesn't matter if a compiler is "supported" or not... evaluation order of expressions is not predictable.

rod-chapman · 2026-07-28T11:26:10Z

For example:

#include <stdio.h>

int p = 5;

int f(int x)
{
  p = 0;
  return x / 2;
}

int main()
{
  int i = 10;
  int j = f(i) + i / p;
  printf("Final value of j is %d\n", j);
  return 0;
}

Running that on Graviton-4/Linux with gcc 13.3.0 yields unpredictable results:

ubuntu@ip-172-31-6-93:~$ gcc -o main -Wall  -O0 main.c
ubuntu@ip-172-31-6-93:~$ ./main
Final value of j is 5
ubuntu@ip-172-31-6-93:~$ gcc -o main -Wall  -O1 main.c
ubuntu@ip-172-31-6-93:~$ ./main
Final value of j is 5
ubuntu@ip-172-31-6-93:~$ gcc -o main -Wall  -O2 main.c
ubuntu@ip-172-31-6-93:~$ ./main
Trace/breakpoint trap (core dumped)
ubuntu@ip-172-31-6-93:~$ gcc -o main -Wall  -O3 main.c
ubuntu@ip-172-31-6-93:~$ ./main
Trace/breakpoint trap (core dumped)
ubuntu@ip-172-31-6-93:~$ gcc -o main -Wall  -Os main.c
ubuntu@ip-172-31-6-93:~$ ./main
Trace/breakpoint trap (core dumped)

rod-chapman · 2026-07-28T11:32:10Z

A naive reading of that code, and assuming R-to-L evaluation order, suggests that the final value of j is 7. If I add an assert, will CBMC prove that j == 7 just before the printf()? As you can see above, gcc disagrees.

rod-chapman · 2026-07-28T12:33:28Z

One more question: if I do nothing to my current set up, using no architecture-specific switches at all with CBMC, what does configt::ansi_ct::argument_evaluation_order get set to by default?

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 (all permutations for up to three blocks), so that order-dependent final states are explored rather than fixed; - fails closed with an explicit assertion when an expression contains more than three mutually unsequenced side-effect blocks. 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 diffblue#9120) remains the best model of what deployed compilers were observed to do, and the pre-diffblue#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 diffblue#9120, including both directions of the division-by-zero example and the two-writes example where the fixed order would wrongly prove an assertion. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

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 diffblue#9120) remains the best model of what deployed compilers were observed to do, and the pre-diffblue#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 diffblue#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. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig · 2026-08-05T13:26:42Z

#9152 is a follow-up seeking to address all the points raised by @rod-chapman to establish soundness in this regard.

Copilot AI review requested due to automatic review settings July 19, 2026 10:43

tautschnig requested review from kroening, peterschrammel and remi-delmas-3000 as code owners July 19, 2026 10:44

Copilot started reviewing on behalf of tautschnig July 19, 2026 10:44 View session

Copilot AI reviewed Jul 19, 2026

View reviewed changes

Comment thread unit/util/argument_evaluation_order.cpp Outdated

Comment thread src/util/config.h Outdated

tautschnig mentioned this pull request Jul 19, 2026

Cross-platform instability arising from default signedness of char in contracts library #8991

Open

tautschnig force-pushed the feature/argument-evaluation-order branch from d4e5cfe to 0a79951 Compare July 19, 2026 11:08

kroening approved these changes Jul 19, 2026

View reviewed changes

kroening assigned tautschnig Jul 19, 2026

tautschnig force-pushed the feature/argument-evaluation-order branch 5 times, most recently from ab66e45 to 04d1bb7 Compare July 19, 2026 19:26

tautschnig force-pushed the feature/argument-evaluation-order branch from 04d1bb7 to 26c7414 Compare July 19, 2026 19:27

tautschnig merged commit f71fdad into diffblue:develop Jul 19, 2026
42 of 43 checks passed

tautschnig deleted the feature/argument-evaluation-order branch July 19, 2026 21:02

tautschnig mentioned this pull request Aug 5, 2026

Add --evaluation-order-check for unspecified evaluation order #9152

Open

5 tasks

Navigation Menu

Uh oh!

Record function argument evaluation order in configt::ansi_ct - #9120

Record function argument evaluation order in configt::ansi_ct#9120
tautschnig merged 1 commit into
diffblue:developfrom
tautschnig:feature/argument-evaluation-order

tautschnig commented Jul 19, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

codecov Bot commented Jul 19, 2026 •

edited

Loading

Uh oh!

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

kroening commented Jul 28, 2026

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

tautschnig commented Aug 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

tautschnig commented Jul 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

codecov Bot commented Jul 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

kroening commented Jul 28, 2026

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

rod-chapman commented Jul 28, 2026

Uh oh!

tautschnig commented Aug 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

tautschnig commented Jul 19, 2026 •

edited

Loading

codecov Bot commented Jul 19, 2026 •

edited

Loading