Semantic patch v1 rename skips calls inside class methods and writes a file that fails check #965

Summary

A schema-less (v1) rename of a function rewrites the declaration and the calls in top-level functions, but not the calls inside class methods. semaprax patch still exits 0, prints a new graph revision and writes the file, which then fails semaprax check with SPX-H003 unresolved function. semaprax impact with the same patch, and the same rename as a v2 patch, both refuse it with SPX-H003, so only the v1 patch path writes a broken file.

This issue is about the v1 write. The same traversal gap makes v2 refuse valid renames without writing; those cases are under "Further cases".

Environment

• Repository: github.com/wavect/semaprax at commit 2d215d3.
• Binary: target/debug/semaprax, built with cargo build --locked -p semaprax --bin semaprax, sha256 3eb5ebbf7f5cefa5a3be9b5c66032ffb0dbbda162f48cb015975721d636b8b2f. semaprax --version prints semaprax 0.9.0 (commit unknown).
• Host: macOS arm64, Darwin 27.2.0; rustc 1.98.1, cargo 1.98.1.

Fixture

module.spx:

module demo;

@id("demo.counter")
class Counter {
    @id("demo.counter.start")
    start: i64,

    @id("demo.counter.get")
    fn get(self: Counter) -> i64
{
        helper()
    }
}

@id("demo.helper")
fn helper() -> i64
{
    42
}

@id("demo.main")
fn main() -> i64
{
    let c = Counter { start: 1 };
    c.start + helper()
}

v1.spatch (the base is the revision that check prints for module.spx):

base sha256:c34f1c7b5ef3cc03951c92e3b2c5f6658b8582ed4486754faabeabba4cb17cd9
rename demo.helper to computed

v2.spatch is the same with schema semaprax.semantic-patch.v2 as its first line.

Steps and observed output

$ semaprax check module.spx; echo rc=$?
verified module.spx (sha256:c34f1c7b5ef3cc03951c92e3b2c5f6658b8582ed4486754faabeabba4cb17cd9)
rc=0

$ semaprax run module.spx; echo rc=$?
43
rc=0

$ semaprax impact module.spx v1.spatch; echo rc=$?
error[SPX-H003]: unresolved function `helper` at module.spx:11:9
rc=1

$ semaprax patch module.spx v2.spatch; echo rc=$?
error[SPX-H003]: unresolved function `helper` at module.spx:11:9
rc=1

The file is still unchanged; orig.spx is a copy of it. Then:

$ semaprax patch module.spx v1.spatch; echo rc=$?
applied semantic patch; graph is now sha256:de12804b51ccc2739ad1efa2876d305b924e6d0a183d5d57dcfc7e99d5926965
rc=0

$ diff -U0 --label orig.spx --label module.spx orig.spx module.spx; echo rc=$?
--- orig.spx
+++ module.spx
@@ -16 +16 @@
-fn helper() -> i64
+fn computed() -> i64
@@ -25 +25 @@
-    c.start + helper()
+    c.start + computed()
rc=1

$ semaprax check module.spx; echo rc=$?
error[SPX-H003]: unresolved function `helper` at module.spx:11:9
rc=1

$ semaprax run module.spx; echo rc=$?
error[SPX-H003]: unresolved function `helper` at module.spx:11:9
rc=1

Line 11 is still helper() inside Counter.get.

Expected behaviour

The v1 rename rewrites every reference, including the call in Counter.get, and the result passes check. If a reference form is not supported yet, the patch is refused and the file is left unchanged.

v1 is still a supported input: docs/SEMANTIC-PATCH-V2.md:8-10 says v2 adds operations "without changing schema-less v1 patches".

Where in the code

• src/patch.rs:2919-2946: function_name_positions, used by function rename at src/patch.rs:1424, collects call sites only from program.functions. Class methods live in TypeDeclarationKind::Class { fields, methods } (src/ast.rs:706-709), so it misses them.

• src/patch.rs:1339-1343: the original program is resolved with hir::resolve only for v2 and v3.

• src/patch.rs:1794-1807: a standalone v1 candidate gets verify::verify only. hir::resolve(&candidate), which reports SPX-H003, runs only under if let Some(before_resolved) = &before_resolved.

• src/impact.rs:195-198: impact resolves and validates both programs, which is why it rejects the same candidate.

• src/patch/source_index.rs:111-136: the v2 source index walks bodies and contracts only for top-level functions, so it also omits class method bodies and contracts. rename-member takes its sites from this index (src/patch.rs:1517-1521).

Further cases

The _v1 and _v2 patches are built like v1.spatch and v2.spatch, with the base that check prints. Each case exits 1 and leaves the file unchanged: nothing is corrupted, but a valid rename cannot be applied, and the v1 errors point at a line in the user's program.

inv.spx, a record invariant that calls the target (base sha256:7b76d8e6656ba6fc1cf2546d4f092873d239004cbdc9cd5ec6d159b058cbc73f):

module demo;

@id("demo.helper")
fn helper() -> i64
{
    1
}

@id("demo.seats")
record Seats {
    @id("demo.seats.limit")
    limit: i64,
}
    requires limit >= helper()

@id("demo.main")
fn main() -> i64
{
    let s = Seats { limit: 3 };
    s.limit
}

val.spx, the target passed as a function value (base sha256:d65bb4d46391f0f25b05a10d5c8e63b2ea7733a9f38650b51955f7636b1db057):

module demo;

@id("demo.helper")
fn helper(x: i64) -> i64
{
    x + 1
}

@id("demo.apply")
fn apply(f: fn(i64) -> i64, x: i64) -> i64
{
    f(x)
}

@id("demo.main")
fn main() -> i64
{
    apply(helper, 41)
}

$ semaprax patch inv.spx inv_v1.spatch; echo rc=$?
error[SPX-T203]: unknown function `helper` at inv.spx:14:23
  help: declare `helper` in this module, or in a project import it [...]
rc=1

$ semaprax patch inv.spx inv_v2.spatch; echo rc=$?
error[SPX-G108]: semantic patch source/HIR identity index is inconsistent
rc=1

$ semaprax patch val.spx val_v1.spatch; echo rc=$?
error[SPX-T202]: unknown value `helper` in `main` at val.spx:18:11
rc=1

$ semaprax patch val.spx val_v2.spatch; echo rc=$?
error[SPX-G108]: semantic patch source/HIR identity index is inconsistent
rc=1

v2 rename-member on a class field that a method reads, cls.spx (base sha256:de24679281acdf14dd449ca2b038b14d392afe1c4c4d390a172ec4c0cf3cf65e), patch line rename-member owner t.counter member t.counter.value to amount:

module t.cls;

@id("t.counter")
class Counter {
    @id("t.counter.value")
    value: i64,

    @id("t.counter.get")
    fn get(self: Counter) -> i64
{
        helper(self.value)
    }
}

@id("t.helper")
fn helper(x: i64) -> i64
{
    x + 1
}

@id("t.main")
fn main() -> i64
{
    let c = Counter { value: 41 };
    helper(c.value)
}

$ semaprax patch cls.spx mem.spatch; echo rc=$?
error[SPX-H001]: unresolved field `value` on `t.counter` at cls.spx:11:16
rc=1

Control: change only line 11, the method body, to 41 and use base sha256:5684c4265e7400b6e09c49fa6ed850df990c800618bfc38bc8323e20ba9b2abb in mem.spatch. Then patch exits 0, renames the field declaration, the constructor label and c.value, check exits 0 and run prints 42. main avoids method calls, which v2 refuses separately with SPX-G108.

A method requires helper() > 0 (body self.start) differs: v1 patch exits 0, the diff deletes that requires line, and check and run succeed. So a passing check does not show that method contracts were kept. That contract loss looks like a separate defect.

Suggested fix

One option: resolve standalone v1 candidates with hir::resolve before writing, so the unresolved call is refused. This fits inside CandidateValidation::Standalone, because project rename runs v1 with CandidateValidation::ProjectModule (src/patch.rs:965). Then extend function_name_positions and the v2 source index to class method bodies and contracts, and cover or refuse record invariants and function values. A regression test on module.spx can assert that line 11 becomes computed() and check passes.

Related

• [REF-12][P2] Represent semantic patch operations once and derive planner views #524 (closed) changed how semantic patch operations are represented; it did not change which declarations the rename traversal visits.

Not verified

• Class methods that call the target from ensures.
• Project mode (change preview and project rename); only single-file patch ran.
• Only the debug binary on macOS was used.

Written by an AI agent loop, lightly reviewed by a human. All commands were re-run at the commit above.