feat(lint): add write-after-write

[mablr]

Description

Closes OSS-84

Add write-after-write lint.

Detects redundant consecutive storage writes to the same variable where the first value is overwritten before being read, wasting an SSTORE.

PR Checklist

• Added Tests
• Added Documentation
• Breaking changes

[figtracer]

correctness

[mattsse]

Requesting changes for a few correctness gaps in write-after-write.

P2: Binary and Ternary are walked linearly here: write_after_write.rs#L204-L215. This can false-positive across &&/|| short-circuiting and ternary arms, and conflicts with the docs' “flat sequence” scope: book#L16-L20. Suggest treating conditional/short-circuit expression boundaries like branches: process condition reads, then clear or analyze each reachable arm with separate pending state.

P2: The lint only implements check_function: write_after_write.rs#L22-L33, so modifier bodies are not analyzed even though placeholder handling exists: write_after_write.rs#L114-L117. Suggest adding modifier-body traversal or removing/de-scoping placeholder logic and tests until modifiers are actually checked.

P3: Calls clear pending without first walking the callee/args: write_after_write.rs#L171-L174, write_after_write.rs#L216-L218. Solidity evaluates call arguments before the call, so nested overwrites in args are missed. Suggest walking callee/arguments first, then clearing pending before modeling the call itself.

[grandizzy]

A few things worth addressing before merge, mostly around the data-flow precision in check_stmt / collect_reads:

Real false positives from nested terminators

check_block only stops when the immediate statement is Return | Revert | Break | Continue. Terminators inside nested blocks/branches don't propagate, so unreachable code is still treated as live and the first write gets flagged:

{ return; }
x = 1;
x = 2;                       // unreachable, but x = 1 will be flagged

if (c) return; else revert E();
x = 1;
x = 2;                       // unreachable on both paths, but x = 1 will be flagged

while (c) {
    { break; }
    x = 1;
    x = 2;                   // unreachable after break in this iteration
}

Fix: thread a small Flow { Continue, StopCurrentBlock } through check_stmt / check_block. Block / UncheckedBlock propagate from children; If returns StopCurrentBlock only if both branches stop; Loop always returns Continue (zero-iteration possible).

Inline assembly handling

The match on StmtKind isn't exhaustive without an Assembly / Yul arm. Either solar's pinned HIR has no such variant (in which case fine), or it does and it's silently ignored — which would be unsound, since inline assembly can sload / sstore / call / revert any storage:

x = 1;
assembly { /* may read or overwrite x.slot */ }
x = 2;                       // currently x = 1 likely flagged — unsound

Safe behavior is pending.clear() for the assembly statement. Worth confirming against solar's actual StmtKind enum and adding a fixture.

Tuple diagnostic span is misleading

(x, y) = (1, 2);
x = v;

emits one warning pointing at the whole tuple statement, but only the x slot is dead — y may be live. process_assignment_lhs should pass the component span (e.span) instead of the outer assign_span so the warning points at x specifically.

Likely false negatives worth fixtures (or documenting)

These are the conservative-clear trade-offs; mostly defensible, but should at least be visible as tests:

• Branch-local dead writes: x = 1; if (c) { y = 2; } x = v; — x = 1 dead on both paths, missed (outer pending cleared on If).
• Both branches assign: if (c) x = 1; else x = 2; x = 3; — both branch writes dead, missed.
• Short-circuit / ternary in RHS: x = 1; bool b = a && b2; x = 2; and x = 1; uint256 z = c ? 7 : 8; x = 2; — x = 1 lost because collect_reads's && / || / Ternary arms unconditionally pending.clear() even when the surrounding context doesn't read x.
• Pure / view / builtin calls: x = 1; pureFn(); x = 2; or any abi.encode(...) — all calls clear pending. Defensible for reentrancy, but loses many obviously-safe cases.
• do { x = 2; } while (c); after x = 1 — body executes ≥ 1, but loops always wipe pending.
• Modifier arguments: writes in f() m(x = 1) live on func.modifiers, not func.body, and aren't analyzed.

Minor soundness / style notes

• process_assignment_lhs for tuple LHS uses the same assign_span for every component, so two same-statement WAW reports point to identical spans and are hard to distinguish.
• The Loop(block, _) second field is LoopSource (init/cond/update are desugared into the loop block in HIR) — so that's fine, not a bug.
• DeclMulti with state-var LHS isn't a real concern: (uint a, x) = … shows up as a tuple Assign, which is handled.
• x = f(); x = v; where f() may revert is sound — on success the first is dead, on revert the second never runs.
• emit E(x) correctly doesn't clear pending; reads in args are removed by collect_reads.

Suggested additional fixtures

// Currently FP (or will be after fix) — unreachable code should not flag
function nestedReturn() public {
    { return; }
    x = 1;
    x = 2;
}

function bothBranchesExit(bool c) public {
    if (c) return; else revert();
    x = 1;
    x = 2;
}

function nestedBreak(bool c) public {
    while (c) {
        { break; }
        x = 1;
        x = 2;
    }
}

// Inline assembly — verify soundness
function asmReadsX() public {
    x = 1;
    assembly { let v := sload(0) }
    x = 2;
}

// UX: span should point at the `x` component, not the whole tuple
function tuplePartial(uint256 v) public {
    (x, y) = (1, 2);
    x = v;
}

// Known FNs — document as limitations
function branchMiss(bool c, uint256 v) public {
    x = 1;
    if (c) { y = 2; }
    x = v;
}
function shortCircuitMiss(bool a, bool b) public {
    x = 1;
    bool z = a && b;
    x = 2;
}
function pureCallMiss() public {
    x = 1;
    abi.encode(uint256(0));
    x = 2;
}

Minimal fix suggestion

The three items above (Flow propagation through nested terminators, explicit assembly handling, component-level tuple spans) close the real soundness / UX issues with little added complexity. The conservative-clear false negatives can be left as-is — but adding fixtures for them makes the design intent visible to future maintainers.

[mablr]

@grandizzy I fixed your findings in 06e3f72.