Add $result for Return Refinements

[rajshivu]

Updated CreateASTVisitor to map refinement variables '_' and 'return' to '$result' to prevent conflicts.
Verified by manual test in ReturnRefinementTest.java.

[rcosta358]

Hi @rajshivu,
This is not really what we were looking for. Your approach replaces the variables return and _ with $result, which is incorrect and causes the tests to fail.

To allow $result to represent return values of methods, you need to modify the grammar to allow identifiers to start with $, substitute the variable $result with _ (similarly to return), and finally add some tests to check if your implementation is correct.

[rcosta358]

Also, if you have any suggestions other than $result, which is not very idiomatic for Java, feel free to let us know!

[rajshivu]

Hi @rcosta358 ,
Thank you for the clarification - that makes sense. You’re right, my initial approach was too naive and incorrectly replaced return and _ directly with $result, which explains the failing tests.

Based on your feedback, I understand the correct direction is to:

1. Extend the grammar to allow identifiers starting with $.
2. Treat $result as a syntactic alias and internally substitute it with _ (similarly to how return is handled today).
3. Add proper tests to validate that $result, _, and return behave consistently.

I’ll update the implementation accordingly and push a revised PR.
Also, I agree that $result may not be the most idiomatic Java-style identifier — I’ll think about alternative suggestions and share them if I find a better fit.

Thanks again for the guidance, this was very helpful.

[rajshivu]

Fixed the handling of method return values in refinements:
Updated the grammar and AST visitor to allow $result to represent method return values, while still keeping _ as a valid alias.

Added a regression test ResultRefinementRegression.java to verify $result works correctly in refinements.
Ensured existing tests in TestMultiple.java pass with the new $result handling.

Hope This change resolves the issue where return was incorrectly treated as a variable and ensures $result can be safely used in refinement expressions.

[rcosta358]

Hey @rajshivu,
Almost there. Your implementation is not quite correct yet. Currently what you're doing is replacing all return and $result variables with _ in the CreateASTVisitor. That way, the following code passes, when it shouldn't:

void test() {
  @Refinement("$result > 0") // $result is replaced with `_`, which refers to `x`, so it passes
  int x = 1;
}

Actually, $result or return should only be allowed on refinements that target methods, such as:

@Refinement("$result > 0")
int test() {
  return 1;
}

So, we don't actually want to modify the CreateASTVisitor. Instead, we want to modify the MethodsFunctionsChecker. More specifically, the handleFunctionRefinements, and add an additional case for $result, similarly to return:

private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, List<CtParameter<?>> params) throws LJError {
  // ...
  ret = ret.substituteVariable("return", Keys.WILDCARD);
  ret = ret.substituteVariable("$result", Keys.WILDCARD); // ADD THIS
  f.setRefReturn(ret);
  // ...
}

Finally, please add tests to liquidjava-example/src/main/java/testSuite, not liquidjava-example/src/main/java/testMultiple. For tests that should pass, they must include "Correct" in their file name, whereas for tests that should fail, they should include "Error", along with the expected error in the first line of the file as a comment. To run the tests locally, you can run mvn test.

[rajshivu]

Hi @rcosta358 ,

Thanks for the clarification! Got it — I’ll revert the changes in CreateASTVisitor and TestMultiple, and instead implement $result handling in MethodsFunctionsChecker.handleFunctionRefinements as suggested. I’ll also move the regression tests to testSuite with the proper naming convention.

[alcides]

Hi @rajshivu, just out of curiosity, how would you pass a Turing test?

[rajshivu]

Hello @alcides , you caught me, I used a bit of AI to help polish my explanation and easy for understand, but I promise there's a real person behind the keyboard.

[rajshivu]

Hi @rcosta358 , I’ve pushed a fix for this issue in last commits,
Could you please pull the latest changes and verify if the solution works on your side?

[CatarinaGamboa]

Changing all IDs to allow for the $ will make it harder to pinpoint errors in other variables. Since the only thing we want is to allow $result as a possible var in the refinements we can add it to the place i pointed in the comments. Try the change and test it to see if it works

[CatarinaGamboa]

This is not a great idea to change all the IDs to allow the $. We can improve it by only allowing $result and only in the places it can appear (not when a ghost or state is created for example)

[rajshivu]

Hi @CatarinaGamboa , thanks for the clarification
I will work on it.

[rajshivu]

Hi @rcosta358 @CatarinaGamboa , I’ve pushed an updated fix.
$result is now handled as a dedicated literal in the grammar and mapped to a variable expression only in refinements, without changing global ID handling.
All tests are passing, could you please pull the latest changes and verify on your side?

[CatarinaGamboa]

Looks better! Merge main into this branch so there are no conflicts and then we fix the nitpick below. Then request a new review and maybe we'll merge it

[CatarinaGamboa]

dont leave commented code