Skip to content

verify: Treat the contract constructs by their meaning in Clang's own analyses - #37

Merged
SwayamInSync merged 13 commits into
mainfrom
fix/contract-node-sites
Oct 19, 2026
Merged

SwayamInSync merged 13 commits into
mainfrom
fix/contract-node-sites

Conversation

@SwayamInSync

@SwayamInSync SwayamInSync commented Oct 18, 2026 •

Copy link
Copy Markdown
Owner

Six switches over statement classes in Clang's own code did not list the contract classes (ForallExpr, ExistsExpr, ContractChooseExpr, OldExpr, ResultExpr, and the ghost statements), as the build warns (enumeration value 'ForallExprClass' not handled in switch). Three of them fell through to llvm_unreachable, which a release build compiles to undefined behavior, one let the analyzer drop the path, and one hid the constructs from libclang:

bool g = noexcept(cppverify::exists(k, 0, 3, k == 1));
  -> PLEASE submit a bug report ... (canThrow), or a hang
enum { Constant = cppverify::exists(k, 0, 3, k == 1) };   // -std=c++98
  -> PLEASE submit a bug report ... and a hang (CheckICE)
int after_ghost(int x) { cppverify::ghost { int g = x; } int *p = 0; return *p; }
  -> no warning from clang --analyze (the path ends at the ghost block)
int f(int n) cppverify::pre(cppverify::forall(k, 0, n, k >= 0)) { return n; }
  -> c-index-test shows no cursor for the precondition or its operands

Each site now handles the classes by their meaning: a contract expression is never evaluated, and ghost code emits no code.

  • Sema::canThrow: a contract expression or ghost statement cannot throw.
  • CheckICE (C++98 integral constant expressions): a contract expression is not one.
  • Expr::HasSideEffects: a contract expression has its operands' side effects, as if it were evaluated, which is what the fallthrough already computed; it is now listed with the other expressions that recurse.
  • The Itanium mangler: a contract expression in a mangled name is reported (cannot yet mangle ExistsExpr expression), as other expressions without a mangling are. Since verify: Compile contracts in templates, ignoring a template's contracts with a warning #28 one reaches it in a template's signature, and main mangles it to nothing: template <class T> void test(int (&)[sizeof(cppverify::exists(k, 0, 3, k == T()), T())]) instantiated for int is _Z4testIiEvRAszcmcvT__E_i, a comma (cm) with one operand, which neither llvm-cxxfilt nor c++filt accepts.
  • The CFG leaves out ghost code and contract statements, so the static analyzer, and the CFG-based warnings, continue past them; the analyzer lists the classes with those that never reach its evaluation loop.
  • libclang: a contract construct is an unexposed expression or statement, with its operands as children. It was CXCursor_NotImplemented, an invalid cursor that clients skip, and in a clause its operands went with it.

CI fails when the build log shows a switch over statement classes that misses one of them, so a new upstream switch cannot miss them silently.

Testing: Verify/contracts_in_clang_analyses.cpp checks noexcept on a contract expression (C++17), a contract expression in an integral constant expression (C++98), and the analyzer's null-dereference warnings after a ghost block and after cppverify::check, and the mangler's error for the template above. Each of its four runs fails on main (two by a crash and a hang, one by the missing warnings, one by the missing error). Removing the cases from canThrow, from CheckICE, or from the mangler, or the CFG's omission, fails it; removing them from the analyzer's switch does not, since the CFG never gives it those nodes. Index/cppverify-cursors.cpp checks the cursor of each construct and of its operands; it fails on main and without the libclang cases. The CI check matches the ten warnings of SemaExceptionSpec.cpp in each of two rebuilds of main's Sema, and none in a build of all of Clang on this branch (clang-test-depends, the target CI builds), which found the libclang site.

Checked on main together with the change of #38, for quantifiers in executable code, whose files are disjoint from these: in a build with assertions every Clang test passes (48,612), as do the Verify suite and the libclang and libIndex tests of the constructs; in a release build the Verify suite gives 417 passed, 1 unsupported. A verdict differential against main over the Verify sources, the new test left out since main hangs on it, changes only the new test of #38 and decode_uleb128_canonical (llvm_uleb128.cpp, with roundtrip_uleb128 after it), which timed out in main's run and verified here, as in another differential against main the same day; these changes do not reach the verifier's queries. No time changed.

Rebased onto main after #28, #32, and #34, with the mangler's test added: Verify suite 421 passed, 1 unsupported; in a build with assertions this test, CodeGenCXX/mangle-fail.cpp, Verify/template_contracts.cpp, and the libclang test pass.

@SwayamInSync
SwayamInSync force-pushed the fix/contract-node-sites branch from 19dda28 to 9c72d10 Compare October 18, 2026 14:19
@SwayamInSync
SwayamInSync merged commit 4209bc3 into main Oct 19, 2026
13 of 14 checks passed
@SwayamInSync
SwayamInSync deleted the fix/contract-node-sites branch October 19, 2026 06:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant