SMTChecker: writeStateVars retains function->annotation().contract at CHC.cpp:1149 — sibling of PR #17151

Open
  • Is something wrong?
#17,173 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
2/5
Estimated time
1-3 hours
Newbie friendliness
55/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Tech stack
cpp
Domain
compilers

Research direction

Start in libsolidity/formal/CHC.cpp, in externalFunctionCallToTrustedCode: compare the pre-call readStateVars(*targetContract, ...) with the post-call writeStateVars(*function->annotation().contract, ...) near line 1149. Confirm the only remaining function->annotation().contract site with grep in libsolidity/formal/. Done means the write uses targetContract and an SMTChecker test for inherited external this calls still passes. The soundness impact is unverified, so check whether a test shows a difference.

Written by the indexing model from the issue text.

Description

Summary

PR #17151 (2026-10-27, 185246c4) explicitly passes targetContract to predicate(...) so SMTChecker accounts for inheritance across external this calls. The fix updated readStateVars at CHC.cpp:1109 (pre-call block in externalFunctionCallToTrustedCode) to use *targetContract instead of *function->annotation().contract.

The paired writeStateVars call in the post-call block of the same function (currently line 1149 on main) still uses the pre-fix pattern:

state().writeStateVars(*function->annotation().contract, contractAddressValue(_funCall));

grep -rn "function->annotation()\.contract" libsolidity/formal/ returns this as the only remaining instance in the whole directory. Every other site was updated by PR #17151.

Why it may matter

In externalFunctionCallToTrustedCode, state tracking becomes asymmetric for external this calls across inheritance:

  • pre-call readStateVars(*targetContract, ...) reads from the correct inherited contract
  • post-call writeStateVars(*function->annotation().contract, ...) writes to a potentially different contract scope

For the exact scenario PR #17151 flags (external this.foo() where foo is inherited), the read side was fixed but the write side was not — the SMT state model may track reads and writes on different contracts.

Caveats / honest state

  • Two attempted CHC assert-level repros on brew solc 0.8.38 (which pre-dates PR #17151) did not produce a demonstrable false-negative at the assertion level. The soundness consequence is theoretical from inspection; no observable mis-verification demonstrated so far.
  • Review-history scan via GitHub API: PR #17151 has 2 reviews, 0 inline comments, 0 issue comments — no reviewer dispatched this specific line, which supports oversight rather than an informed design decision.

Suggested fix (one-line symmetry)

state().writeStateVars(*targetContract, contractAddressValue(_funCall));

(Hoist the targetContract local above both the pre-call and post-call blocks so both sides use the resolved contract.)

References

  • Fix PR: #17151 (185246c4), merged 2026-10-27
  • Current main reference: libsolidity/formal/CHC.cpp:1149
  • Grep witness: single remaining function->annotation().contract callsite in libsolidity/formal/

Reporter: symposia-gi (General Imperative). Code-review observation only; no bounty claim.

Dominant language
C++
Stars
25.8k
Forks
6.2k
Avg merge
1d 22h
Merged PRs (30d)
43

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from argotorg/solidity

All issues in argotorg/solidity

Similar issues

More C++ issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.