From 9d7e2dc138c9f335b5f9adfd7dd7179b2a392455 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Tue, 10 Feb 2026 22:44:24 +0530 Subject: [PATCH 1/6] feat: implement support and restore test infrastructure --- .../src/main/java/testSuite/CorrectResult.java | 16 ++++++++++++++++ .../main/java/testSuite/ErrorResultVariable.java | 10 ++++++++++ 2 files changed, 26 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectResult.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorResultVariable.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectResult.java b/liquidjava-example/src/main/java/testSuite/CorrectResult.java new file mode 100644 index 00000000..db67c70c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectResult.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectResult { + + @Refinement("$result > 10") + public int getLargeNumber() { + return 15; + } + + @Refinement("$result == (a + b)") + public int sum(int a, int b) { + return a + b; + } +} \ No newline at end of file diff --git a/liquidjava-example/src/main/java/testSuite/ErrorResultVariable.java b/liquidjava-example/src/main/java/testSuite/ErrorResultVariable.java new file mode 100644 index 00000000..c37cade8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorResultVariable.java @@ -0,0 +1,10 @@ +// Not Found Error +package testSuite; +import liquidjava.specification.Refinement; + +public class ErrorResultVariable { + public void test() { + @Refinement("$result > 0") + int x = 10; + } +} \ No newline at end of file From e111574005e77d2ac889a11baa4e9085cdcee66b Mon Sep 17 00:00:00 2001 From: RajShivu Date: Tue, 10 Feb 2026 22:54:08 +0530 Subject: [PATCH 2/6] TestMultiple: restored original --- .../src/test/java/liquidjava/api/tests/TestMultiple.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java index 6e28cc67..e833d7ba 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java @@ -14,7 +14,7 @@ public void testMultipleErrorDirectory() { String path = "../liquidjava-example/src/main/java/testMultiple/errors"; CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(9, diagnostics.getErrors().size()); + assertEquals(9, diagnostics.getErrors().size());// 9 } @Test @@ -39,7 +39,7 @@ public void testMultipleDirectory() { CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(11, diagnostics.getErrors().size()); + assertEquals(11, diagnostics.getErrors().size());// 11 assertEquals(3, diagnostics.getWarnings().size()); } } \ No newline at end of file From ab4d6002495f85309cc2dcce372e33eacc651886 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Wed, 11 Feb 2026 08:35:48 +0530 Subject: [PATCH 3/6] Assert: checked assert validation tests --- .../general_checkers/MethodsFunctionsChecker.java | 8 ++++++++ .../src/test/java/liquidjava/api/tests/TestMultiple.java | 4 ++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 815e8e6c..6b5115a7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -161,6 +161,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, Optional oret = rtc.getRefinementFromAnnotation(method); Predicate ret = oret.orElse(new Predicate()); ret = ret.substituteVariable("return", Keys.WILDCARD); + ret = ret.substituteVariable("$result", Keys.WILDCARD);// added for refinement f.setRefReturn(ret); return Predicate.createConjunction(joint, ret); } @@ -180,6 +181,13 @@ public void getReturnRefinements(CtReturn ret) throws LJError { RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), ((CtClass) method.getParent()).getQualifiedName(), method.getParameters().size()); + if (fi == null) + return;// null check refinement + + if (fi.getRefReturn() == null) { + return; + } + List lv = fi.getArguments(); for (Variable v : lv) { rtc.getContext().addVarToContext(v); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java index e833d7ba..6e28cc67 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java @@ -14,7 +14,7 @@ public void testMultipleErrorDirectory() { String path = "../liquidjava-example/src/main/java/testMultiple/errors"; CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(9, diagnostics.getErrors().size());// 9 + assertEquals(9, diagnostics.getErrors().size()); } @Test @@ -39,7 +39,7 @@ public void testMultipleDirectory() { CommandLineLauncher.launch(path); Diagnostics diagnostics = Diagnostics.getInstance(); - assertEquals(11, diagnostics.getErrors().size());// 11 + assertEquals(11, diagnostics.getErrors().size()); assertEquals(3, diagnostics.getWarnings().size()); } } \ No newline at end of file From 58a547577f3bc7eff8b11f7883ccf86537747743 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Wed, 11 Feb 2026 21:32:48 +0530 Subject: [PATCH 4/6] Fix refinement handling in rj grammar --- liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index e34f40ad..07615f62 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -92,7 +92,7 @@ BOOL : 'true' | 'false'; ID_UPPER: ([A-Z][a-zA-Z0-9]*); OBJECT_TYPE: (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+); -ID : '#'*[a-zA-Z_][a-zA-Z0-9_#]*; +ID : '#'*('$')? [a-zA-Z_] [a-zA-Z0-9_#]* ; STRING : '"'(~["])*'"'; INT : (([0-9]+) | ([0-9]+('_'[0-9]+)*)); REAL : (([0-9]+('.'[0-9]+)?) | '.'[0-9]+); From a3bee27b2f4bea08335e70df34570dd117191f70 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Fri, 13 Feb 2026 20:31:59 +0530 Subject: [PATCH 5/6] Support as a restricted refinement variable --- liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 | 6 ++++-- .../rj_language/visitors/CreateASTVisitor.java | 12 +++++++++++- 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 index 07615f62..d52a7f92 100644 --- a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 +++ b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 @@ -36,6 +36,7 @@ operand: literalExpression: '(' literalExpression ')' #litGroup | literal #lit + | RESULT #result | ID #var | ID '.' functionCall #targetInvocation | functionCall #invocation @@ -91,8 +92,9 @@ ARITHOP : '+'|'*'|'/'|'%';//|'-'; BOOL : 'true' | 'false'; ID_UPPER: ([A-Z][a-zA-Z0-9]*); OBJECT_TYPE: - (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+); -ID : '#'*('$')? [a-zA-Z_] [a-zA-Z0-9_#]* ; + (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+); +RESULT : '$result'; +ID : '#'*[a-zA-Z_][a-zA-Z0-9_#]*; STRING : '"'(~["])*'"'; INT : (([0-9]+) | ([0-9]+('_'[0-9]+)*)); REAL : (([0-9]+('.'[0-9]+)?) | '.'[0-9]+); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 1bedda99..672fbc34 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -49,6 +49,7 @@ import rj.grammar.RJParser.PredLogicContext; import rj.grammar.RJParser.PredNegateContext; import rj.grammar.RJParser.ProgContext; +import rj.grammar.RJParser.ResultContext; import rj.grammar.RJParser.StartContext; import rj.grammar.RJParser.StartPredContext; import rj.grammar.RJParser.TargetInvocationContext; @@ -159,9 +160,18 @@ else if (rc instanceof VarContext) { } else if (rc instanceof TargetInvocationContext) { // TODO Finish Invocation with Target (a.len()) return null; - } else { + } + // else { + // return create(((InvocationContext) rc).functionCall()); + // } + else if (rc instanceof ResultContext) { + return new Var("$result"); + } else if (rc instanceof InvocationContext) { return create(((InvocationContext) rc).functionCall()); + } else { + throw new IllegalStateException("Unknown literalExpression: " + rc.getClass()); } + } private Expression functionCallCreate(FunctionCallContext rc) throws LJError { From 515ddf5e9972b3dd56df37913c524a5ec93243d0 Mon Sep 17 00:00:00 2001 From: RajShivu Date: Fri, 13 Feb 2026 21:55:23 +0530 Subject: [PATCH 6/6] Remove commented-out code from CreateASTVisitor --- .../liquidjava/rj_language/visitors/CreateASTVisitor.java | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 672fbc34..093b3df9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -160,11 +160,7 @@ else if (rc instanceof VarContext) { } else if (rc instanceof TargetInvocationContext) { // TODO Finish Invocation with Target (a.len()) return null; - } - // else { - // return create(((InvocationContext) rc).functionCall()); - // } - else if (rc instanceof ResultContext) { + } else if (rc instanceof ResultContext) { return new Var("$result"); } else if (rc instanceof InvocationContext) { return create(((InvocationContext) rc).functionCall());