Avoid 'result' name clash when a user parameter is named result

[tautschnig]

Strata uses 'result' as the canonical binding for a procedure's return value in postcondition (ensures) clauses; JVerify's translator already renames the postcondition lambda's parameter to 'result' so the ensures expression refers to the return correctly. With BOTH the user parameter AND the renamed lambda variable mapped to 'result' in the same procedure scope, Strata complained:

(1:1-1:1): Error: Duplicate definition 'result'
is already defined in this scope

Fix: rename the user's parameter (only) when its name is exactly 'result'. The rename is applied to:

• The Laurel parameter declaration (so the procedure signature declares the renamed parameter instead of result).
• The current method's preconditions, postconditions, and body via a per-method currentParamRenames field on the StaticMethodCollector visitor that the single-arg convertExpression / convertStatement overloads consult. This avoids threading a renames Map through every recursive call site (~30+ locations in convertStatement alone).

Rename target: the base is '__user_result' (leading-underscore convention mirrors the JVerify shim's _jverify_old capture names, and it is obvious in raw_stdout / line-map diagnostics). Rather than trusting that base to be unique, freshName() checks it against the procedure's other parameter names and appends the smallest integer suffix needed, so the rename can never reintroduce the very duplicate-definition clash it avoids. (Residual: a body-local variable literally named '__user_result' is not yet considered; full identifier hygiene would require scanning the method body.)

Robustness of the visitor-scope field (per review feedback):

• currentParamRenames is declared private and holds an immutable Map.copyOf snapshot, so the per-method rename state cannot be mutated in place.
• visitMethodDef saves and restores the field in a try/finally, scoping renames to the method (and its nested declarations) and guaranteeing no state leaks to sibling methods.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Updates the Java→Laurel compiler to avoid identifier clashes when a Java method parameter is named result, ensuring contracts/body translation stays consistent.

Changes:

• Introduces a per-method rename map (currentParamRenames) to propagate parameter renames through conversions.
• Renames user parameters literally named result and applies that mapping across method translation.
• Merges user-parameter renames with postcondition-lambda renames so both rewrites apply in ensures.

---

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

[keyboardDrummer]

Shouldn't this be a fix in Laurel? To allow local variables to be named result ?

[tautschnig]

Shouldn't this be a fix in Laurel? To allow local variables to be named result ?

Quite possibly: yes - this was just the least intrusive way to work around an observed problem. Happy to work on the Laurel-side fix instead (once Strata's refactor is settled).

[fabiomadge]

The crash is real — on main, a method with a parameter named result plus a postcondition throws RuntimeException: Could not find line map for .../<unknown> (the same method with param y verifies). Rename direction is right.

But the fix is incomplete by one line, and a result-param method still can't verify. I dumped the Laurel for int identity(int result){ postcondition((int r)->r==result); return result; }:

• param -> __user_result ✓
• ensures: eq(result, __user_result) ✓
• body: return result — not renamed ✗

The postcondition pins the return to __user_result, but the body returns an unconstrained free var named result, so even this tautology fails (r == y with param y verifies). Cause: the fix updated the single-arg convertExpression to use currentParamRenames, but the single-arg convertStatement (which converts the method body) still passes Map.of(). One-line fix:

private StmtExpr convertStatement(JCTree.JCStatement statement) {
    return convertStatement(statement, currentParamRenames);   // was Map.of()
}

Verified locally: with that line, a result-param method verifies.

On tests: this PR adds none, and nothing existing covers it. AvoidNameCollisionsTest.differentReturnValueNames() tests result as a lambda parameter and as locals, but never as a method parameter — the one role that triggers this. And since the fix removes the crash, a "doesn't crash" test wouldn't catch the residual unprovability. Please add a test with a method that takes a result parameter and a postcondition that should hold, asserting it verifies (methodsVerified/errorCount), not just that it doesn't crash.

[fabiomadge]

This rewires single-arg convertExpression to currentParamRenames, but the parallel single-arg convertStatement (return convertStatement(statement, Map.of());) wasn't updated — and the method body is converted through it. So a renamed result param isn't rewritten in the body (return result stays result), leaving the return unconstrained and the postcondition unprovable. The same change is needed there.

[fabiomadge]

Shouldn't this be a fix in Laurel? To allow local variables to be named result?

Agree it's a Laurel scoping issue. When a procedure has a returnType but no explicit return param, Strata's ConcreteToAbstractTreeTranslator (~line 477) injects an output param literally named result into the procedure scope — so a user var/param named result collides ("Duplicate definition"). The robust fix is there: give the synthesized return binding a name users can't write. The front-end rename in this PR is a workaround.