Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
tautschnig wants to merge 1 commit into
base: main
Choose a base branch
from
Open

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

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
92 changes: 82 additions & 10 deletions ...main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,18 @@ private record LabelEntry(String javaLabel, String breakLabel, String continueLa
private final Deque<LabelEntry> labelStack = new ArrayDeque<>();
private String pendingLabel = null;

// Per-method parameter renames. Set at the start of
// visitMethodDef when a parameter name clashes with a
// Laurel-reserved identifier (currently only "result").
// Saved / restored per method visit (see visitMethodDef)
// so renames stay scoped to the method subtree. Read by
// the single-arg convertExpression / convertStatement
// overloads as the default renames map, so the rewrite
// propagates into precondition / postcondition /
// assertion / body translations without threading the
// map manually through every call site.
private Map<String, String> currentParamRenames = Map.of();

/** Check if a statement tree contains break or continue (at the current loop level). */
private boolean containsBreakOrContinue(JCTree.JCStatement stmt) {
boolean[] found = {false};
Expand Down Expand Up @@ -203,15 +215,23 @@ private String resolveContinueLabel(JCTree.JCContinue cont) {

@Override
public void visitMethodDef(JCTree.JCMethodDecl method) {
if ((method.mods.flags & Flags.STATIC) != 0) {
try {
translateStaticMethod(method);
} catch (JavaViolationException e) {
reporter.reportError(method, "translatorError", e.getMessage());
annotationCompiler.markSkipped(currentCompilationUnit, method);
// Save / restore the per-method rename state so it stays
// scoped to this method (and its nested declarations) and
// never leaks to sibling methods.
Map<String, String> previousParamRenames = currentParamRenames;
try {
if ((method.mods.flags & Flags.STATIC) != 0) {
try {
translateStaticMethod(method);
} catch (JavaViolationException e) {
reporter.reportError(method, "translatorError", e.getMessage());
annotationCompiler.markSkipped(currentCompilationUnit, method);
}
}
super.visitMethodDef(method);
} finally {
currentParamRenames = previousParamRenames;
}
super.visitMethodDef(method);
}

private void translateStaticMethod(JCTree.JCMethodDecl method) {
Expand All @@ -220,9 +240,34 @@ private void translateStaticMethod(JCTree.JCMethodDecl method) {
String methodName = qualifiedMethodName(method.sym);

List<Parameter> params = new ArrayList<>();
// When a user parameter is literally named "result"
// it would clash with Strata's reserved binding for
// the procedure return value (which the
// postcondition lambda also renames to). Rename
// the parameter to a fresh name and propagate the
// rewrite into all body / contract conversions
// via currentParamRenames (a visitor-scope field).
Set<String> existingParamNames = new HashSet<>();
for (var param : method.params) {
params.add(parameter(param.name.toString(), translateType(param.type)));
existingParamNames.add(param.name.toString());
}
Map<String, String> paramRenames = new HashMap<>();
for (var param : method.params) {
String pname = param.name.toString();
if (pname.equals("result")) {
// Pick a target that does not collide with any
// other parameter, so the rename cannot
// reintroduce the very clash we are avoiding.
String renamed = freshName("__user_result", existingParamNames);
paramRenames.put(pname, renamed);
pname = renamed;
}
Comment thread
tautschnig marked this conversation as resolved.
params.add(parameter(pname, translateType(param.type)));
}
// Map.copyOf is an immutable snapshot, so the per-method
// rename state cannot be mutated in place; visitMethodDef
// saves and restores this field around the subtree.
currentParamRenames = Map.copyOf(paramRenames);

Optional<ReturnType> retType = Optional.empty();
if (method.restype != null && method.restype.type != null
Expand All @@ -243,7 +288,14 @@ private void translateStaticMethod(JCTree.JCMethodDecl method) {
var postExpr = post.get();
if (postExpr instanceof JCTree.JCLambda lambda && lambda.params.size() == 1) {
var paramName = lambda.params.getFirst().name.toString();
var renames = Map.of(paramName, "result");
// result is Strata-canonical for return
// bindings. Combine the lambda-parameter
// rename with the user-parameter renames
// (e.g. when a parameter is named
// "result") so both rewrites apply
// inside the postcondition body.
Map<String, String> renames = new HashMap<>(paramRenames);
renames.put(paramName, "result");
ensures.add(ensuresClause(convertLambdaBody(lambda, renames), Optional.empty()));
} else {
ensures.add(ensuresClause(convertExpression(postExpr), Optional.empty()));
Expand Down Expand Up @@ -286,6 +338,22 @@ private void translateStaticMethod(JCTree.JCMethodDecl method) {
procedures.add(proc);
}

/// Returns `base` if it is not already present in `taken`,
/// otherwise appends the smallest positive integer suffix
/// that makes the name unique. Used to choose a rename
/// target for a user parameter named "result" that cannot
/// collide with another parameter in the same procedure.
private static String freshName(String base, Set<String> taken) {
if (!taken.contains(base)) {
return base;
}
int suffix = 1;
while (taken.contains(base + suffix)) {
suffix++;
}
return base + suffix;
}

private StmtExpr convertBlock(JCTree.JCBlock blk, Map<String, String> renames) {
List<StmtExpr> statements = new ArrayList<>();
for (var statement : blk.stats) {
Expand Down Expand Up @@ -450,7 +518,11 @@ yield withLoopLabels(forLoop.body, (breakLbl, continueLbl) -> {
}

private StmtExpr convertExpression(JCTree.JCExpression expr) {
return convertExpression(expr, Map.of());
// Use the per-method parameter renames so any
// user-parameter rewrite (e.g. "result" -> "__user_result")
// is applied transparently throughout the method's
// contracts and body.
return convertExpression(expr, currentParamRenames);

@fabiomadge fabiomadge Jun 9, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

}

private StmtExpr convertLambdaBody(JCTree.JCLambda lambda, Map<String, String> renames) {
Expand Down
Loading