From ff71e800b90f6aafc9b31f48e96a93d04ebbc1a0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 14 Nov 2025 14:09:18 +0000 Subject: [PATCH 01/16] Throw LJErrors --- .../liquidjava/diagnostics/LJDiagnostic.java | 2 +- .../errors/InvalidRefinementError.java | 1 - .../processor/context/AliasWrapper.java | 6 +- .../liquidjava/processor/facade/AliasDTO.java | 5 +- .../ExternalRefinementTypeChecker.java | 37 ++---- .../MethodsFirstChecker.java | 27 +---- .../RefinementTypeChecker.java | 93 +++------------ .../refinement_checker/TypeChecker.java | 72 +++++------ .../refinement_checker/VCChecker.java | 41 +++---- .../MethodsFunctionsChecker.java | 26 ++-- .../general_checkers/OperationsChecker.java | 32 ++--- .../AuxHierarchyRefinementsPassage.java | 12 +- .../object_checkers/AuxStateHandler.java | 112 ++++++++++-------- .../rj_language/BuiltinFunctionPredicate.java | 8 +- .../liquidjava/rj_language/Predicate.java | 31 ++--- .../rj_language/parsing/ParsingException.java | 8 -- .../parsing/RefinementsParser.java | 24 ++-- .../rj_language/visitors/AliasVisitor.java | 3 - .../visitors/CreateASTVisitor.java | 34 +++--- 19 files changed, 226 insertions(+), 348 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index db48c8a9..34b21f3d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -6,7 +6,7 @@ import spoon.reflect.cu.SourcePosition; -public class LJDiagnostic { +public class LJDiagnostic extends Exception { private String title; private String message; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java index 96cc272d..8012928c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -1,6 +1,5 @@ package liquidjava.diagnostics.errors; -import liquidjava.diagnostics.TranslationTable; import spoon.reflect.declaration.CtElement; /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java index fc8283d5..227db985 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -5,10 +5,10 @@ import java.util.List; import java.util.Map; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.utils.Utils; import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; @@ -59,7 +59,7 @@ public Expression getNewExpression(List newNames) { return expr.getExpression().clone(); } - public Predicate getPremises(List list, List newNames, CtElement elem) throws ParsingException { + public Predicate getPremises(List list, List newNames, CtElement elem) throws LJError { List invocationPredicates = getPredicatesFromExpression(list, elem); Predicate prem = new Predicate(); for (int i = 0; i < invocationPredicates.size(); i++) { @@ -69,7 +69,7 @@ public Predicate getPremises(List list, List newNames, CtElement return prem.clone(); } - private List getPredicatesFromExpression(List list, CtElement elem) throws ParsingException { + private List getPredicatesFromExpression(List list, CtElement elem) throws LJError { List lp = new ArrayList<>(); for (String e : list) lp.add(new Predicate(e, elem)); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java index 8737f572..7b880475 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java @@ -2,8 +2,9 @@ import java.util.List; import java.util.stream.Collectors; + +import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; import spoon.reflect.reference.CtTypeReference; @@ -32,7 +33,7 @@ public AliasDTO(String name2, List varTypes2, List varNames2, St // Parse the alias expression using the given the prefix to ensure ghost names are qualified consistently with // where the alias is declared or used - public void parse(String prefix) throws ParsingException { + public void parse(String prefix) throws LJError { if (ref != null) { this.expression = RefinementsParser.createAST(ref, prefix); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index ce05d7db..799dcd1a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -5,7 +5,7 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning; import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning; import liquidjava.processor.context.Context; @@ -13,7 +13,6 @@ import liquidjava.processor.facade.GhostDTO; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.Utils; import spoon.reflect.declaration.CtClass; @@ -52,11 +51,7 @@ public void visitCtInterface(CtInterface intrface) { diagnostics.add(new ExternalClassNotFoundWarning(intrface, message, prefix)); return; } - try { - getRefinementFromAnnotation(intrface); - } catch (ParsingException e) { - return; // error already reported - } + getRefinementFromAnnotation(intrface); handleStateSetsFromAnnotation(intrface); super.visitCtInterface(intrface); } @@ -70,8 +65,9 @@ public void visitCtField(CtField f) { Optional oc; try { oc = getRefinementFromAnnotation(f); - } catch (ParsingException e) { - return; // error already reported + } catch (LJError e) { + diagnostics.add(e); + return; } Predicate c = oc.orElse(new Predicate()); context.addGlobalVariableToContext(f.getSimpleName(), prefix, f.getType(), c); @@ -111,26 +107,15 @@ public void visitCtMethod(CtMethod method) { } } MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); - try { - mfc.getMethodRefinements(method, prefix); - } catch (ParsingException e) { - return; - } + mfc.getMethodRefinements(method, prefix); super.visitCtMethod(method); } - protected void getGhostFunction(String value, CtElement element) { - try { - // Optional ofd = - // RefinementParser.parseFunctionDecl(value); - GhostDTO f = RefinementsParser.getGhostDeclaration(value); - if (f != null && element.getParent() instanceof CtInterface) { - GhostFunction gh = new GhostFunction(f, factory, prefix); - context.addGhostFunction(gh); - } - - } catch (ParsingException e) { - diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), element)); + protected void getGhostFunction(String value, CtElement element) throws LJError { + GhostDTO f = RefinementsParser.getGhostDeclaration(value); + if (f != null && element.getParent() instanceof CtInterface) { + GhostFunction gh = new GhostFunction(f, factory, prefix); + context.addGhostFunction(gh); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index c4d97695..e3c5359d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -7,7 +7,6 @@ import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; -import liquidjava.rj_language.parsing.ParsingException; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtConstructor; import spoon.reflect.declaration.CtInterface; @@ -53,11 +52,7 @@ public void visitCtClass(CtClass ctClass) { if (ct instanceof CtClass) visitCtClass((CtClass) ct); } - try { - getRefinementFromAnnotation(ctClass); - } catch (ParsingException e) { - return; // error already reported - } + getRefinementFromAnnotation(ctClass); handleStateSetsFromAnnotation(ctClass); super.visitCtClass(ctClass); } @@ -74,11 +69,7 @@ public void visitCtInterface(CtInterface intrface) { if (getExternalRefinement(intrface).isPresent()) return; - try { - getRefinementFromAnnotation(intrface); - } catch (ParsingException e) { - return; // error already reported - } + getRefinementFromAnnotation(intrface); handleStateSetsFromAnnotation(intrface); super.visitCtInterface(intrface); } @@ -89,12 +80,8 @@ public void visitCtConstructor(CtConstructor c) { return; context.enterContext(); - try { - getRefinementFromAnnotation(c); - mfc.getConstructorRefinements(c); - } catch (ParsingException e) { - return; - } + getRefinementFromAnnotation(c); + mfc.getConstructorRefinements(c); super.visitCtConstructor(c); context.exitContext(); } @@ -104,11 +91,7 @@ public void visitCtMethod(CtMethod method) { return; context.enterContext(); - try { - mfc.getMethodRefinements(method); - } catch (ParsingException e) { - return; - } + mfc.getMethodRefinements(method); super.visitCtMethod(method); context.exitContext(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 6c20c816..fe73de81 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -7,13 +7,13 @@ import java.util.List; import java.util.Optional; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.processor.refinement_checker.general_checkers.OperationsChecker; import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.BuiltinFunctionPredicate; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Types; @@ -131,11 +131,7 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { // only declaration, no assignment if (localVariable.getAssignment() == null) { Optional a; - try { - a = getRefinementFromAnnotation(localVariable); - } catch (ParsingException e) { - return; // error already reported - } + a = getRefinementFromAnnotation(localVariable); context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), localVariable); } else { @@ -147,14 +143,7 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { refinementFound = new Predicate(); } context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); - - try { - checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, - localVariable); - } catch (ParsingException e1) { - return; // error already reported - } - + checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); AuxStateHandler.addStateRefinements(this, varName, e); } } @@ -169,12 +158,7 @@ public void visitCtNewArray(CtNewArray newArray) { List> l = newArray.getDimensionExpressions(); // TODO only working for 1 dimension for (CtExpression exp : l) { - Predicate c; - try { - c = getExpressionRefinements(exp); - } catch (ParsingException e) { - return; // error already reported - } + Predicate c = getExpressionRefinements(exp); String name = String.format(Formats.FRESH, context.getCounter()); if (c.getVariableNames().contains(Keys.WILDCARD)) { c = c.substituteVariable(Keys.WILDCARD, name); @@ -183,12 +167,9 @@ public void visitCtNewArray(CtNewArray newArray) { } context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp); Predicate ep; - try { - ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray), + ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray), Predicate.createVar(name)); - } catch (ParsingException e) { - return; // error already reported - } + newArray.putMetadata(Keys.REFINEMENT, ep); } } @@ -211,7 +192,7 @@ public void visitCtThisAccess(CtThisAccess thisAccess) { @SuppressWarnings("unchecked") @Override - public void visitCtAssignment(CtAssignment assignment) { + public void visitCtAssignment(CtAssignment assignment) throws LJError { if (diagnostics.foundError()) { return; } @@ -237,11 +218,6 @@ public void visitCtAssignment(CtAssignment assignment) { AuxStateHandler.updateGhostField(fw, this); } } - // if (ex instanceof CtArrayWrite) { - // Predicate c = getRefinement(ex); - // TODO continue - // c.substituteVariable(WILD_VAR, ); - // } } @Override @@ -286,12 +262,8 @@ public void visitCtField(CtField f) { } super.visitCtField(f); - Optional c; - try { - c = getRefinementFromAnnotation(f); - } catch (ParsingException e) { - return; // error already reported - } + Optional c = getRefinementFromAnnotation(f); + // context.addVarToContext(f.getSimpleName(), f.getType(), // c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new // Predicate()) ); @@ -330,12 +302,9 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { } else if (fieldRead.getVariable().getSimpleName().equals("length")) { String targetName = fieldRead.getTarget().toString(); - try { - fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), + fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), BuiltinFunctionPredicate.length(targetName, fieldRead))); - } catch (ParsingException e) { - return; // error already reported - } + } else { fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE @@ -363,13 +332,8 @@ public void visitCtBinaryOperator(CtBinaryOperator operator) { if (diagnostics.foundError()) { return; } - super.visitCtBinaryOperator(operator); - try { - otc.getBinaryOpRefinements(operator); - } catch (ParsingException e) { - return; // error already reported - } + otc.getBinaryOpRefinements(operator); } @Override @@ -379,11 +343,7 @@ public void visitCtUnaryOperator(CtUnaryOperator operator) { } super.visitCtUnaryOperator(operator); - try { - otc.getUnaryOpRefinements(operator); - } catch (ParsingException e) { - return; // error already reported - } + otc.getUnaryOpRefinements(operator); } public void visitCtInvocation(CtInvocation invocation) { @@ -412,13 +372,8 @@ public void visitCtIf(CtIf ifElement) { } CtExpression exp = ifElement.getCondition(); - - Predicate expRefs; - try { - expRefs = getExpressionRefinements(exp); - } catch (ParsingException e) { - return; // error already reported - } + Predicate expRefs = getExpressionRefinements(exp); + String freshVarName = String.format(Formats.FRESH, context.getCounter()); expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName); Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); @@ -469,13 +424,7 @@ public void visitCtArrayWrite(CtArrayWrite arrayWrite) { super.visitCtArrayWrite(arrayWrite); CtExpression index = arrayWrite.getIndexExpression(); - BuiltinFunctionPredicate fp; - try { - fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, - arrayWrite); - } catch (ParsingException e) { - return; // error already reported - } + BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, arrayWrite); arrayWrite.putMetadata(Keys.REFINEMENT, fp); } @@ -514,7 +463,7 @@ public void visitCtNewClass(CtNewClass newClass) { // ############################### Inner Visitors // ########################################## private void checkAssignment(String name, CtTypeReference type, CtExpression ex, CtExpression assignment, - CtElement parentElem, CtElement varDecl) { + CtElement parentElem, CtElement varDecl) throws LJError { getPutVariableMetadada(ex, name); Predicate refinementFound = getRefinement(assignment); @@ -531,14 +480,10 @@ private void checkAssignment(String name, CtTypeReference type, CtExpression< r.ifPresent(variableInstance -> vcChecker.removePathVariableThatIncludes(variableInstance.getName())); vcChecker.removePathVariableThatIncludes(name); // AQUI!! - try { - checkVariableRefinements(refinementFound, name, type, parentElem, varDecl); - } catch (ParsingException e) { - return; // error already reported - } + checkVariableRefinements(refinementFound, name, type, parentElem, varDecl); } - private Predicate getExpressionRefinements(CtExpression element) throws ParsingException { + private Predicate getExpressionRefinements(CtExpression element) throws LJError { if (element instanceof CtVariableRead) { // CtVariableRead elemVar = (CtVariableRead) element; return getRefinement(element); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 7b06b3c3..efc82261 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -9,6 +9,7 @@ import liquidjava.diagnostics.errors.CustomError; import liquidjava.diagnostics.errors.InvalidRefinementError; +import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -18,7 +19,6 @@ import liquidjava.processor.facade.AliasDTO; import liquidjava.processor.facade.GhostDTO; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; @@ -61,7 +61,7 @@ public Predicate getRefinement(CtElement elem) { return c == null ? new Predicate() : c; } - public Optional getRefinementFromAnnotation(CtElement element) throws ParsingException { + public Optional getRefinementFromAnnotation(CtElement element) throws LJError { Optional constr = Optional.empty(); Optional ref = Optional.empty(); for (CtAnnotation ann : element.getAnnotations()) { @@ -85,8 +85,8 @@ public Optional getRefinementFromAnnotation(CtElement element) throws // check if refinement is valid if (!p.getExpression().isBooleanExpression()) { - diagnostics.add(new InvalidRefinementError(element, "Refinement predicate must be a boolean expression", - ref.get())); + throw new InvalidRefinementError(element, "Refinement predicate must be a boolean expression", + ref.get()); } if (diagnostics.foundError()) return Optional.empty(); @@ -97,7 +97,7 @@ public Optional getRefinementFromAnnotation(CtElement element) throws } @SuppressWarnings("unchecked") - public void handleStateSetsFromAnnotation(CtElement element) { + public void handleStateSetsFromAnnotation(CtElement element) throws LJError { int set = 0; for (CtAnnotation ann : element.getAnnotations()) { String an = ann.getActualAnnotation().annotationType().getCanonicalName(); @@ -112,7 +112,7 @@ public void handleStateSetsFromAnnotation(CtElement element) { } } - private void createStateSet(CtNewArray e, int set, CtElement element) { + private void createStateSet(CtNewArray e, int set, CtElement element) throws LJError { // if any of the states starts with uppercase, throw error (reserved for alias) for (CtExpression ce : e.getElements()) { @@ -121,7 +121,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { CtLiteral s = (CtLiteral) ce; String f = s.getValue(); if (Character.isUpperCase(f.charAt(0))) { - diagnostics.add(new CustomError("State names must start with lowercase", s)); + throw new CustomError("State names must start with lowercase", s); } } } @@ -157,18 +157,11 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { } } - private void createStateGhost(String string, CtAnnotation ann, String an, CtElement element) { - GhostDTO gd = null; - try { - gd = RefinementsParser.getGhostDeclaration(string); - } catch (ParsingException e) { - diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), ann)); - return; - } + private void createStateGhost(String string, CtAnnotation ann, String an, CtElement element) throws LJError { + GhostDTO gd = RefinementsParser.getGhostDeclaration(string); if (gd.getParam_types().size() > 0) { - diagnostics.add(new CustomError( - "Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann)); - return; + throw new CustomError( + "Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann); } // Set class as parameter of Ghost String qn = getQualifiedClassName(element); @@ -216,22 +209,16 @@ protected Optional createStateGhost(int order, CtElement element) return Optional.empty(); } - protected void getGhostFunction(String value, CtElement element) { - try { - GhostDTO f = RefinementsParser.getGhostDeclaration(value); - if (f != null && element.getParent() instanceof CtClass) { - CtClass klass = (CtClass) element.getParent(); - GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName()); - context.addGhostFunction(gh); - } - } catch (ParsingException e) { - diagnostics.add(new CustomError("Could not parse the ghost function", e.getMessage(), element)); - // e.printStackTrace(); - return; + protected void getGhostFunction(String value, CtElement element) throws LJError { + GhostDTO f = RefinementsParser.getGhostDeclaration(value); + if (f != null && element.getParent() instanceof CtClass) { + CtClass klass = (CtClass) element.getParent(); + GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName()); + context.addGhostFunction(gh); } } - protected void handleAlias(String value, CtElement element) { + protected void handleAlias(String value, CtElement element) throws LJError { try { AliasDTO a = RefinementsParser.getAliasDeclaration(value); String klass = null; @@ -247,16 +234,15 @@ protected void handleAlias(String value, CtElement element) { a.parse(path); // refinement alias must return a boolean expression if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { - diagnostics.add(new InvalidRefinementError(element, - "Refinement alias must return a boolean expression", value)); - return; + throw new InvalidRefinementError(element, "Refinement alias must return a boolean expression", value); } AliasWrapper aw = new AliasWrapper(a, factory, Keys.WILDCARD, context, klass, path); context.addAlias(aw); } - } catch (ParsingException e) { + } catch (SyntaxError e) { + // add location info to error SourcePosition pos = Utils.getRefinementAnnotationPosition(element, value); - diagnostics.add(new SyntaxError(e.getMessage(), pos, value)); + throw new SyntaxError(e.getMessage(), pos, value); } } @@ -273,7 +259,7 @@ Optional getExternalRefinement(CtInterface intrface) { } public void checkVariableRefinements(Predicate refinementFound, String simpleName, CtTypeReference type, - CtElement usage, CtElement variable) throws ParsingException { + CtElement usage, CtElement variable) throws LJError { Optional expectedType = getRefinementFromAnnotation(variable); Predicate cEt; RefinedVariable mainRV = null; @@ -305,28 +291,28 @@ else if (expectedType.isPresent()) context.addRefinementToVariableInContext(simpleName, type, cet, usage); } - public void checkSMT(Predicate expectedType, CtElement element) { + public void checkSMT(Predicate expectedType, CtElement element) throws LJError { vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory); element.putMetadata(Keys.REFINEMENT, expectedType); } - public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) { + public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) throws LJError { vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, moreInfo, factory); } - public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) { + public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) throws LJError { return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); } - public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customMessage) { + public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customMessage) throws LJError { vcChecker.printSubtypingError(element, expectedType, foundType, customMessage); } - public void createSameStateError(CtElement element, Predicate expectedType, String klass) { + public void createSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { vcChecker.printSameStateError(element, expectedType, klass); } - public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) { + public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) throws LJError { vcChecker.printStateMismatchError(element, method, found, expected); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index b467a757..31fd9444 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -39,7 +39,7 @@ public VCChecker() { pathVariables = new Stack<>(); } - public void processSubtyping(Predicate expectedType, List list, CtElement element, Factory f) { + public void processSubtyping(Predicate expectedType, List list, CtElement element, Factory f) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); if (expectedType.isBooleanTrue()) @@ -53,11 +53,9 @@ public void processSubtyping(Predicate expectedType, List list, CtEl try { List filtered = filterGhostStatesForVariables(list, mainVars, lrv); premises = premisesBeforeChange.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); - et = expectedType.changeStatesToRefinements(filtered, s).changeAliasToRefinement(context, f); } catch (Exception e) { - diagnostics.add(new RefinementError(element, expectedType.getExpression(), premises.simplify(), map)); - return; + throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map); } try { @@ -69,14 +67,14 @@ public void processSubtyping(Predicate expectedType, List list, CtEl } public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, - String string, Factory f) { + String string, Factory f) throws LJError { boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); if (!b) printSubtypingError(element, expectedType, type, string); } public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List list, SourcePosition p, - Factory f) { + Factory f) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); @@ -234,24 +232,22 @@ private void recAuxGetVars(RefinedVariable var, List newVars) { getVariablesFromContext(l, newVars, varName); } - public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition p) { + public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition p) throws LJError { try { new SMTEvaluator().verifySubtype(found, expectedType, context, p); } catch (TypeCheckError e) { return false; } catch (Exception e) { String msg = e.getLocalizedMessage().toLowerCase(); - LJError error; if (msg.contains("wrong number of arguments")) { - error = new GhostInvocationError("Wrong number of arguments in ghost invocation", p, + throw new GhostInvocationError("Wrong number of arguments in ghost invocation", p, expectedType.getExpression(), null); } else if (msg.contains("sort mismatch")) { - error = new GhostInvocationError("Type mismatch in arguments of ghost invocation", p, + throw new GhostInvocationError("Type mismatch in arguments of ghost invocation", p, expectedType.getExpression(), null); } else { - error = new CustomError(e.getMessage(), p); + throw new CustomError(e.getMessage(), p); } - diagnostics.add(error); } return true; } @@ -262,9 +258,6 @@ public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition * * @param cSMT * @param expectedType - * - * @throws TypeCheckError - * @throws Exception * */ private void smtChecking(Predicate cSMT, Predicate expectedType, SourcePosition p) @@ -309,24 +302,24 @@ private TranslationTable createMap(CtElement element, Predicate expectedType) { } protected void printSubtypingError(CtElement element, Predicate expectedType, Predicate foundType, - String customMsg) { + String customMsg) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(foundType, lrv, mainVars); TranslationTable map = new TranslationTable(); Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - diagnostics.add(new RefinementError(element, expectedType.getExpression(), premises.simplify(), map)); + throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map); } - public void printSameStateError(CtElement element, Predicate expectedType, String klass) { + public void printSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { TranslationTable map = createMap(element, expectedType); - diagnostics.add(new StateConflictError(element, expectedType.getExpression(), klass, map)); + throw new StateConflictError(element, expectedType.getExpression(), klass, map); } private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, - TranslationTable map) { + TranslationTable map) throws LJError { LJError error = mapError(e, premisesBeforeChange, expectedType, element, map); - diagnostics.add(error); + throw error; } private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, @@ -340,13 +333,13 @@ private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate } } - public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) { + public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); VCImplication foundState = joinPredicates(found, mainVars, lrv, map); - diagnostics.add(new StateRefinementError(element, method, + throw new StateRefinementError(element, method, Arrays.stream(states).map(Predicate::getExpression).toArray(Expression[]::new), - foundState.toConjunctions().simplify().getValue(), map)); + foundState.toConjunctions().simplify().getValue(), map); } } 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 52fe40dc..1b642ee9 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 @@ -7,6 +7,7 @@ import java.util.Map; import java.util.Optional; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.Context; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.RefinedVariable; @@ -18,7 +19,6 @@ import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinementsPassage; import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.utils.Utils; import spoon.reflect.code.CtConstructorCall; import spoon.reflect.code.CtExpression; @@ -45,7 +45,7 @@ public MethodsFunctionsChecker(TypeChecker rtc) { this.rtc = rtc; } - public void getConstructorRefinements(CtConstructor c) throws ParsingException { + public void getConstructorRefinements(CtConstructor c) throws LJError { RefinedFunction f = new RefinedFunction(); f.setName(c.getSimpleName()); f.setType(c.getType()); @@ -65,7 +65,7 @@ public void getConstructorRefinements(CtConstructor c) throws ParsingExceptio AuxStateHandler.handleConstructorState(c, f, rtc); } - public void getConstructorInvocationRefinements(CtConstructorCall ctConstructorCall) { + public void getConstructorInvocationRefinements(CtConstructorCall ctConstructorCall) throws LJError { CtExecutableReference exe = ctConstructorCall.getExecutable(); if (exe != null) { RefinedFunction f = rtc.getContext().getFunction(exe.getSimpleName(), @@ -80,7 +80,7 @@ public void getConstructorInvocationRefinements(CtConstructorCall ctConstruct } // ################### VISIT METHOD ############################## - public void getMethodRefinements(CtMethod method) throws ParsingException { + public void getMethodRefinements(CtMethod method) throws LJError { RefinedFunction f = new RefinedFunction(); f.setName(method.getSimpleName().replaceAll("\\p{C}", "")); // remove any empty chars from string f.setType(method.getType()); @@ -110,7 +110,7 @@ public void getMethodRefinements(CtMethod method) throws ParsingException AuxHierarchyRefinementsPassage.checkFunctionInSupertypes(klass, method, f, rtc); } - public void getMethodRefinements(CtMethod method, String prefix) throws ParsingException { + public void getMethodRefinements(CtMethod method, String prefix) throws LJError { String constructorName = ""; String k = Utils.getSimpleName(prefix); @@ -134,7 +134,7 @@ public void getMethodRefinements(CtMethod method, String prefix) throws P } } - private void auxGetMethodRefinements(CtMethod method, RefinedFunction rf) throws ParsingException { + private void auxGetMethodRefinements(CtMethod method, RefinedFunction rf) throws LJError { // main cannot have refinement - for now if (method.getSignature().equals("main(java.lang.String[])")) return; @@ -151,11 +151,9 @@ private void auxGetMethodRefinements(CtMethod method, RefinedFunction rf) * @param params * * @return Conjunction of all - * - * @throws ParsingException */ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, List> params) - throws ParsingException { + throws LJError { Predicate joint = new Predicate(); for (CtParameter param : params) { @@ -190,7 +188,7 @@ public List> getStateAnnotation(CtElement ele return l; } - public void getReturnRefinements(CtReturn ret) { + public void getReturnRefinements(CtReturn ret) throws LJError { CtClass c = ret.getParent(CtClass.class); String className = c.getSimpleName(); if (ret.getReturnedExpression() != null) { @@ -230,7 +228,7 @@ public void getReturnRefinements(CtReturn ret) { // ############################### VISIT INVOCATION // ################################3 - public void getInvocationRefinements(CtInvocation invocation) { + public void getInvocationRefinements(CtInvocation invocation) throws LJError { CtExecutable method = invocation.getExecutable().getDeclaration(); if (method == null) { @@ -267,7 +265,7 @@ public RefinedFunction getRefinementFunction(String methodName, String className return f; } - private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation invocation) { + private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation invocation) throws LJError { CtTypeReference ctref = ctr.getDeclaringType(); if (ctref == null) { // Plan B: get us get the definition from the invocation. @@ -306,7 +304,7 @@ private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation } private Map checkInvocationRefinements(CtElement invocation, List> arguments, - CtExpression target, String methodName, String className) { + CtExpression target, String methodName, String className) throws LJError { // -- Part 1: Check if the invocation is possible int si = arguments.size(); RefinedFunction f = rtc.getContext().getFunction(methodName, className, si); @@ -393,7 +391,7 @@ private String createVariableRepresentingArgument(CtExpression iArg, Variable } private void checkParameters(CtElement invocation, List> arguments, RefinedFunction f, - Map map) { + Map map) throws LJError { List> invocationParams = arguments; List functionParams = f.getArguments(); for (int i = 0; i < invocationParams.size(); i++) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 0a93f1ac..6ef27a11 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -3,6 +3,9 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; + +import liquidjava.diagnostics.errors.CustomError; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.RefinedVariable; import liquidjava.processor.context.Variable; @@ -13,7 +16,6 @@ import liquidjava.utils.constants.Ops; import liquidjava.utils.constants.Types; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.parsing.ParsingException; import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtAssignment; @@ -56,10 +58,8 @@ public OperationsChecker(TypeChecker rtc) { * * @param * @param operator - * - * @throws ParsingException */ - public void getBinaryOpRefinements(CtBinaryOperator operator) throws ParsingException { + public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJError { CtExpression right = operator.getRightHandOperand(); CtExpression left = operator.getLeftHandOperand(); Predicate oper; @@ -103,11 +103,9 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws Pars * * @param * @param operator - * - * @throws ParsingException */ @SuppressWarnings({ "unchecked" }) - public void getUnaryOpRefinements(CtUnaryOperator operator) throws ParsingException { + public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJError { CtExpression ex = (CtExpression) operator.getOperand(); String name = Formats.FRESH; Predicate all; @@ -165,11 +163,9 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws Parsin * @param element * * @return String with the operation refinements - * - * @throws ParsingException */ private Predicate getOperationRefinements(CtBinaryOperator operator, CtExpression element) - throws ParsingException { + throws LJError { return getOperationRefinements(operator, null, element); } @@ -184,11 +180,9 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtExpres * CtExpression that represent an Binary Operation or one of the operands * * @return Predicate with the operation refinements - * - * @throws ParsingException */ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariableWrite parentVar, - CtExpression element) throws ParsingException { + CtExpression element) throws LJError { if (element instanceof CtFieldRead) { CtFieldRead field = ((CtFieldRead) element); if (field.getVariable().getSimpleName().equals("length")) { @@ -246,7 +240,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab return new Predicate(); } if (l.getValue() == null) - throw new ParsingException("Null literals are not supported"); + throw new CustomError("Null literals are not supported"); return new Predicate(l.getValue().toString(), element); @@ -273,7 +267,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab } private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtBinaryOperator operator) - throws ParsingException { + throws LJError { CtExpression t = inv.getTarget(); if (t instanceof CtVariableRead) { @@ -316,11 +310,9 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtB * @param name * * @return String with the refinements - * - * @throws ParsingException */ private Predicate getRefinementUnaryVariableWrite(CtExpression ex, CtUnaryOperator operator, - CtVariableWrite w, String name) throws ParsingException { + CtVariableWrite w, String name) throws LJError { String newName = String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()); CtVariable varDecl = w.getVariable().getDeclaration(); @@ -363,7 +355,7 @@ private String getOperatorFromKind(BinaryOperatorKind kind) { }; } - private Predicate getOperatorFromKind(UnaryOperatorKind kind, CtElement elem) throws ParsingException { + private Predicate getOperatorFromKind(UnaryOperatorKind kind, CtElement elem) throws LJError { String ret = switch (kind) { case POSTINC -> Keys.WILDCARD + " + 1"; case POSTDEC -> Keys.WILDCARD + " - 1"; @@ -373,7 +365,7 @@ private Predicate getOperatorFromKind(UnaryOperatorKind kind, CtElement elem) th case NOT -> "!" + Keys.WILDCARD; case POS -> "0 + " + Keys.WILDCARD; case NEG -> "-" + Keys.WILDCARD; - default -> throw new ParsingException(kind + "operation not supported"); + default -> throw new CustomError(kind + "operation not supported"); }; return new Predicate(ret, elem); }; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java index fc92e29a..a1b5ae84 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java @@ -4,6 +4,8 @@ import java.util.List; import java.util.Optional; import java.util.stream.Collectors; + +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.ObjectState; import liquidjava.processor.context.RefinedFunction; import liquidjava.processor.context.RefinedVariable; @@ -21,7 +23,7 @@ public class AuxHierarchyRefinementsPassage { public static void checkFunctionInSupertypes(CtClass klass, CtMethod method, RefinedFunction f, - TypeChecker tc) { + TypeChecker tc) throws LJError { String name = method.getSimpleName(); int size = method.getParameters().size(); if (klass.getSuperInterfaces().size() > 0) { // implemented interfaces @@ -40,7 +42,7 @@ public static void checkFunctionInSupertypes(CtClass klass, CtMethod m } static void transferRefinements(RefinedFunction superFunction, RefinedFunction function, CtMethod method, - TypeChecker tc) { + TypeChecker tc) throws LJError { HashMap super2function = getParametersMap(superFunction, function, tc, method); transferReturnRefinement(superFunction, function, method, tc, super2function); transferArgumentsRefinements(superFunction, function, method, tc, super2function); @@ -66,7 +68,7 @@ private static HashMap getParametersMap(RefinedFunction superFun } static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedFunction function, - CtMethod method, TypeChecker tc, HashMap super2function) { + CtMethod method, TypeChecker tc, HashMap super2function) throws LJError { List superArgs = superFunction.getArguments(); List args = function.getArguments(); List> params = method.getParameters(); @@ -90,7 +92,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF } static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunction function, CtMethod method, - TypeChecker tc, HashMap super2function) { + TypeChecker tc, HashMap super2function) throws LJError { Predicate functionRef = function.getRefinement(); Predicate superRef = superFunction.getRefinement(); if (functionRef.isBooleanTrue()) @@ -125,7 +127,7 @@ static Optional functionInInterface(CtClass klass, String si } private static void transferStateRefinements(RefinedFunction superFunction, RefinedFunction subFunction, - CtMethod method, TypeChecker tc) { + CtMethod method, TypeChecker tc) throws LJError { if (superFunction.hasStateChange()) { if (!subFunction.hasStateChange()) { for (ObjectState o : superFunction.getAllStates()) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index 9ec34087..f8faedad 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -1,19 +1,16 @@ package liquidjava.processor.refinement_checker.object_checkers; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.lang.annotation.Annotation; import java.util.*; import java.util.stream.Collectors; -import liquidjava.diagnostics.errors.CustomError; import liquidjava.diagnostics.errors.IllegalConstructorTransitionError; import liquidjava.diagnostics.errors.InvalidRefinementError; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.processor.refinement_checker.TypeCheckingUtils; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -32,20 +29,17 @@ public class AuxStateHandler { * @param c * @param f * @param tc - * - * @throws ParsingException */ @SuppressWarnings({ "unchecked", "rawtypes" }) public static void handleConstructorState(CtConstructor c, RefinedFunction f, TypeChecker tc) - throws ParsingException { + throws LJError { List> an = getStateAnnotation(c); if (!an.isEmpty()) { for (CtAnnotation a : an) { Map m = a.getAllValues(); CtLiteral from = (CtLiteral) m.get("from"); if (from != null) { - diagnostics.add(new IllegalConstructorTransitionError(from)); - return; + throw new IllegalConstructorTransitionError(from); } } setConstructorStates(f, an, tc, c); // f.setState(an, context.getGhosts(), c); @@ -61,12 +55,10 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, * @param anns * @param tc * @param element - * - * @throws ParsingException */ @SuppressWarnings({ "rawtypes" }) private static void setConstructorStates(RefinedFunction f, List> anns, - TypeChecker tc, CtElement element) throws ParsingException { + TypeChecker tc, CtElement element) throws LJError { List l = new ArrayList<>(); for (CtAnnotation an : anns) { Map m = an.getAllValues(); @@ -75,9 +67,7 @@ private static void setConstructorStates(RefinedFunction f, List getDifferentSets(TypeChecker tc, String klassQualified) { List sets = new ArrayList<>(); List l = getGhostStatesFor(klassQualified, tc); @@ -130,11 +131,9 @@ private static List getDifferentSets(TypeChecker tc, String klass * @param method * @param f * @param tc - * - * @throws ParsingException */ public static void handleMethodState(CtMethod method, RefinedFunction f, TypeChecker tc, String prefix) - throws ParsingException { + throws LJError { List> an = getStateAnnotation(method); if (!an.isEmpty()) { setFunctionStates(f, an, tc, method, prefix); @@ -150,11 +149,9 @@ public static void handleMethodState(CtMethod method, RefinedFunction f, Type * @param anns * @param tc * @param element - * - * @throws ParsingException */ private static void setFunctionStates(RefinedFunction f, List> anns, - TypeChecker tc, CtElement element, String prefix) throws ParsingException { + TypeChecker tc, CtElement element, String prefix) throws LJError { List l = new ArrayList<>(); for (CtAnnotation an : anns) { l.add(getStates(an, f, tc, element, prefix)); @@ -164,7 +161,7 @@ private static void setFunctionStates(RefinedFunction f, List ctAnnotation, RefinedFunction f, - TypeChecker tc, CtElement e, String prefix) throws ParsingException { + TypeChecker tc, CtElement e, String prefix) throws LJError { Map m = ctAnnotation.getAllValues(); String from = TypeCheckingUtils.getStringFromAnnotation(m.get("from")); String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to")); @@ -189,13 +186,21 @@ private static ObjectState getStates(CtAnnotation ctAnnota return state; } + /** + * Creates the predicate for state transition + * @param value + * @param targetClass + * @param tc + * @param e + * @param isTo + * @param prefix + * @return the created predicate + */ private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass, - TypeChecker tc, CtElement e, boolean isTo, String prefix) throws ParsingException { + TypeChecker tc, CtElement e, boolean isTo, String prefix) throws LJError { Predicate p = new Predicate(value, e, prefix); if (!p.getExpression().isBooleanExpression()) { - diagnostics.add( - new InvalidRefinementError(e, "State refinement transition must be a boolean expression", value)); - return new Predicate(); + throw new InvalidRefinementError(e, "State refinement transition must be a boolean expression", value); } CtTypeReference r = tc.getFactory().Type().createReference(targetClass); String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); @@ -214,6 +219,13 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f return c1; } + /** + * Gets the missing states in the predicate and adds equalities to old states + * @param t + * @param tc + * @param p + * @return the updated predicate + */ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) { List gs = p.getStateInvocations(getGhostStatesFor(t, tc)); List sets = getDifferentSets(tc, t); @@ -228,7 +240,10 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) } /** - * Collect ghost states for the given qualified class name and its immediate supertypes (superclass and interfaces). + * Collect ghost states for the given qualified class name and its immediate supertypes (superclass and interfaces) + * @param qualifiedClass + * @param tc + * @return list of ghost states */ private static List getGhostStatesFor(String qualifiedClass, TypeChecker tc) { // Keep order: class, then superclass, then interfaces; avoid duplicates @@ -256,15 +271,14 @@ private static List getGhostStatesFor(String qualifiedClass, TypeChe } /** - * Create predicate with the equalities with previous versions of the object e.g., ghostfunction1(this) == - * ghostfunction1(old(this)) - * + * Create predicate with the equalities with previous versions of the object + * e.g., ghostfunction1(this) == ghostfunction1(old(this)) * @param p * @param th * @param sets * @param tc * - * @return + * @return updated predicate */ private static Predicate addOldStates(Predicate p, Predicate th, List sets, TypeChecker tc) { Predicate c = p; @@ -333,7 +347,7 @@ public static void addStateRefinements(TypeChecker tc, String varName, CtExpress * @param invocation */ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpression target2, - Map map, CtElement invocation) { + Map map, CtElement invocation) throws LJError { String parentTargetName = searchFistVariableTarget(tc, target2, invocation); VariableInstance target = getTarget(tc, invocation); if (target != null) { @@ -346,7 +360,12 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre } } - public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { + /** + * Updates the ghost field after a write + * @param fw + * @param tc + */ + public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws LJError { CtField field = fw.getVariable().getDeclaration(); String updatedVarName = String.format(Formats.THIS, fw.getVariable().getSimpleName()); String targetClass = field.getDeclaringType().getQualifiedName(); @@ -379,18 +398,13 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { // ObjectState stateChange = getStates(ann, rf, tc, transitionMethod); ObjectState stateChange = new ObjectState(); - try { - String prefix = field.getDeclaringType().getQualifiedName(); - Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, - prefix); - Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix); - stateChange.setFrom(fromPredicate); - stateChange.setTo(toPredicate); - } catch (ParsingException e) { - String message = String.format("Parsing error while constructing assignment update for `%s`", fw); - diagnostics.add(new CustomError(message, e.getMessage(), field)); - return; - } + String prefix = field.getDeclaringType().getQualifiedName(); + Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, + prefix); + Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix); + stateChange.setFrom(fromPredicate); + stateChange.setTo(toPredicate); + // replace "state(this)" to "state(whatever method is called from) and so on" Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName) @@ -440,7 +454,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { */ private static Predicate changeState(TypeChecker tc, VariableInstance vi, /* RefinedFunction f */ List stateChanges, String name, Map map, - CtElement invocation) { + CtElement invocation) throws LJError { if (vi.getRefinement() == null) { return new Predicate(); } @@ -508,7 +522,7 @@ private static Predicate checkOldMentions(Predicate transitionedState, String in * @return */ private static Predicate sameState(TypeChecker tc, VariableInstance variableInstance, String name, - CtElement invocation) { + CtElement invocation) throws LJError { if (variableInstance.getRefinement() != null) { String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); Predicate c = variableInstance.getRefinement().substituteVariable(Keys.WILDCARD, newInstanceName) @@ -533,7 +547,7 @@ private static Predicate sameState(TypeChecker tc, VariableInstance variableInst * @return */ private static String addInstanceWithState(TypeChecker tc, String superName, String name2, - VariableInstance prevInstance, Predicate transitionedState, CtElement invocation) { + VariableInstance prevInstance, Predicate transitionedState, CtElement invocation) throws LJError { VariableInstance vi2 = (VariableInstance) tc.getContext().addInstanceToContext(name2, prevInstance.getType(), prevInstance.getRefinement(), invocation); // vi2.setState(transitionedState); @@ -564,7 +578,7 @@ private static String addInstanceWithState(TypeChecker tc, String superName, Str * * @param invocation * - * @return + * @return the name of the parent target */ static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElement invocation) { if (target2 instanceof CtVariableRead) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java index 61fe26e8..be9db207 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java @@ -1,20 +1,20 @@ package liquidjava.rj_language; -import liquidjava.rj_language.parsing.ParsingException; +import liquidjava.diagnostics.errors.LJError; import spoon.reflect.declaration.CtElement; public class BuiltinFunctionPredicate extends Predicate { - public BuiltinFunctionPredicate(CtElement elem, String functionName, String... params) throws ParsingException { + public BuiltinFunctionPredicate(CtElement elem, String functionName, String... params) throws LJError { super(functionName + "(" + getFormattedParams(params) + ")", elem); } - public static BuiltinFunctionPredicate length(String param, CtElement elem) throws ParsingException { + public static BuiltinFunctionPredicate length(String param, CtElement elem) throws LJError { return new BuiltinFunctionPredicate(elem, "length", param); } public static BuiltinFunctionPredicate addToIndex(String array, String index, String value, CtElement elem) - throws ParsingException { + throws LJError { return new BuiltinFunctionPredicate(elem, "addToIndex", index, value); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 7410b7bb..6d10d4ec 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -1,13 +1,12 @@ package liquidjava.rj_language; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.util.ArrayList; import java.util.HashMap; import java.util.List; import java.util.Map; import java.util.stream.Collectors; +import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; @@ -25,7 +24,6 @@ import liquidjava.rj_language.ast.Var; import liquidjava.rj_language.opt.derivation_node.ValDerivationNode; import liquidjava.rj_language.opt.ExpressionSimplifier; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.Utils; import liquidjava.utils.constants.Keys; @@ -57,10 +55,8 @@ public Predicate() { * @param ref * @param element * @param e - * - * @throws ParsingException */ - public Predicate(String ref, CtElement element) throws ParsingException { + public Predicate(String ref, CtElement element) throws LJError { this(ref, element, element.getParent(CtType.class).getQualifiedName()); } @@ -71,10 +67,8 @@ public Predicate(String ref, CtElement element) throws ParsingException { * @param element * @param e * @param prefix - * - * @throws ParsingException */ - public Predicate(String ref, CtElement element, String prefix) throws ParsingException { + public Predicate(String ref, CtElement element, String prefix) throws LJError { this.prefix = prefix; exp = parse(ref, element); if (!(exp instanceof GroupExpression)) { @@ -87,23 +81,18 @@ public Predicate(Expression e) { exp = e; } - protected Expression parse(String ref, CtElement element) throws ParsingException { + protected Expression parse(String ref, CtElement element) throws LJError { try { return RefinementsParser.createAST(ref, prefix); - } catch (ParsingException e) { + } catch (SyntaxError e) { + // add location info to error SourcePosition pos = Utils.getRefinementAnnotationPosition(element, ref); - diagnostics.add(new SyntaxError(e.getMessage(), pos, ref)); - throw e; + throw new SyntaxError(e.getMessage(), pos, ref); } } - protected Expression innerParse(String ref, String prefix) { - try { - return RefinementsParser.createAST(ref, prefix); - } catch (ParsingException e1) { - diagnostics.add(new SyntaxError(e1.getMessage(), ref)); - return null; - } + protected Expression innerParse(String ref, String prefix) throws LJError { + return RefinementsParser.createAST(ref, prefix); } public Predicate changeAliasToRefinement(Context context, Factory f) throws Exception { @@ -184,7 +173,7 @@ private void expressionGetOldVariableNames(Expression exp, List ls) { } } - public Predicate changeStatesToRefinements(List ghostState, String[] toChange) { + public Predicate changeStatesToRefinements(List ghostState, String[] toChange) throws LJError { Map nameRefinementMap = new HashMap<>(); for (GhostState gs : ghostState) { if (gs.getRefinement() != null) { // is a state and not a ghost state diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java deleted file mode 100644 index 7eae1e71..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/ParsingException.java +++ /dev/null @@ -1,8 +0,0 @@ -package liquidjava.rj_language.parsing; - -public class ParsingException extends Exception { - - public ParsingException(String errorMessage) { - super(errorMessage); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java index 572d5e71..8be9c387 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java @@ -1,6 +1,9 @@ package liquidjava.rj_language.parsing; import java.util.Optional; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.facade.AliasDTO; import liquidjava.processor.facade.GhostDTO; import liquidjava.rj_language.ast.Expression; @@ -17,7 +20,7 @@ public class RefinementsParser { - public static Expression createAST(String toParse, String prefix) throws ParsingException { + public static Expression createAST(String toParse, String prefix) throws LJError { ParseTree pt = compile(toParse); CreateASTVisitor visitor = new CreateASTVisitor(prefix); return visitor.create(pt); @@ -25,25 +28,20 @@ public static Expression createAST(String toParse, String prefix) throws Parsing /** * The triple information of the ghost declaration in the order > - * * @param s - * - * @return - * - * @throws ParsingException */ - public static GhostDTO getGhostDeclaration(String s) throws ParsingException { + public static GhostDTO getGhostDeclaration(String s) throws LJError { ParseTree rc = compile(s); GhostDTO g = GhostVisitor.getGhostDecl(rc); if (g == null) - throw new ParsingException("Ghost declarations should be in format ()"); + throw new SyntaxError("Ghost declarations should be in format ()", s); return g; } - public static AliasDTO getAliasDeclaration(String s) throws ParsingException { + public static AliasDTO getAliasDeclaration(String s) throws LJError { Optional os = getErrors(s); if (os.isPresent()) - throw new ParsingException(os.get()); + throw new SyntaxError(os.get(), s); CodePointCharStream input; input = CharStreams.fromString(s); RJErrorListener err = new RJErrorListener(); @@ -61,14 +59,14 @@ public static AliasDTO getAliasDeclaration(String s) throws ParsingException { AliasVisitor av = new AliasVisitor(input); AliasDTO alias = av.getAlias(rc); if (alias == null) - throw new ParsingException("Alias definitions should be in format () { }"); + throw new SyntaxError("Alias definitions should be in format () { }", s); return alias; } - private static ParseTree compile(String toParse) throws ParsingException { + private static ParseTree compile(String toParse) throws LJError { Optional s = getErrors(toParse); if (s.isPresent()) - throw new ParsingException(s.get()); + throw new SyntaxError(s.get(), toParse); CodePointCharStream input = CharStreams.fromString(toParse); RJErrorListener err = new RJErrorListener(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java index de155282..fe0c7d2d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/AliasVisitor.java @@ -4,7 +4,6 @@ import java.util.List; import java.util.stream.Collectors; import liquidjava.processor.facade.AliasDTO; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.utils.Pair; import org.antlr.v4.runtime.CodePointCharStream; import org.antlr.v4.runtime.TokenStreamRewriter; @@ -28,8 +27,6 @@ public AliasVisitor(CodePointCharStream input) { * @param rc * * @return - * - * @throws ParsingException */ public AliasDTO getAlias(ParseTree rc) { if (rc instanceof AliasContext) { 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 bef9525d..7eca4a33 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 @@ -2,6 +2,9 @@ import java.util.ArrayList; import java.util.List; + +import liquidjava.diagnostics.errors.LJError; +import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.rj_language.ast.AliasInvocation; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; @@ -14,7 +17,6 @@ import liquidjava.rj_language.ast.LiteralString; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; -import liquidjava.rj_language.parsing.ParsingException; import liquidjava.utils.Utils; import org.antlr.v4.runtime.tree.ParseTree; @@ -64,7 +66,7 @@ public CreateASTVisitor(String prefix) { this.prefix = prefix; } - public Expression create(ParseTree rc) throws ParsingException { + public Expression create(ParseTree rc) throws LJError { if (rc instanceof ProgContext) return progCreate((ProgContext) rc); else if (rc instanceof StartContext) @@ -85,20 +87,20 @@ else if (rc instanceof LiteralContext) return null; } - private Expression progCreate(ProgContext rc) throws ParsingException { + private Expression progCreate(ProgContext rc) throws LJError { if (rc.start() != null) return create(rc.start()); return null; } - private Expression startCreate(ParseTree rc) throws ParsingException { + private Expression startCreate(ParseTree rc) throws LJError { if (rc instanceof StartPredContext) return create(((StartPredContext) rc).pred()); // alias and ghost do not have evaluation return null; } - private Expression predCreate(ParseTree rc) throws ParsingException { + private Expression predCreate(ParseTree rc) throws LJError { if (rc instanceof PredGroupContext) return new GroupExpression(create(((PredGroupContext) rc).pred())); else if (rc instanceof PredNegateContext) @@ -113,7 +115,7 @@ else if (rc instanceof IteContext) return create(((PredExpContext) rc).exp()); } - private Expression expCreate(ParseTree rc) throws ParsingException { + private Expression expCreate(ParseTree rc) throws LJError { if (rc instanceof ExpGroupContext) return new GroupExpression(create(((ExpGroupContext) rc).exp())); else if (rc instanceof ExpBoolContext) { @@ -125,7 +127,7 @@ else if (rc instanceof ExpBoolContext) { } } - private Expression operandCreate(ParseTree rc) throws ParsingException { + private Expression operandCreate(ParseTree rc) throws LJError { if (rc instanceof OpLiteralContext) return create(((OpLiteralContext) rc).literalExpression()); else if (rc instanceof OpArithContext) @@ -144,7 +146,7 @@ else if (rc instanceof OpGroupContext) return null; } - private Expression literalExpressionCreate(ParseTree rc) throws ParsingException { + private Expression literalExpressionCreate(ParseTree rc) throws LJError { if (rc instanceof LitGroupContext) return new GroupExpression(create(((LitGroupContext) rc).literalExpression())); else if (rc instanceof LitContext) @@ -159,24 +161,26 @@ else if (rc instanceof VarContext) { } } - private Expression functionCallCreate(FunctionCallContext rc) throws ParsingException { + private Expression functionCallCreate(FunctionCallContext rc) throws LJError { if (rc.ghostCall() != null) { GhostCallContext gc = rc.ghostCall(); - String name = Utils.qualifyName(prefix, gc.ID().getText()); + String ref = gc.ID().getText(); + String name = Utils.qualifyName(prefix, ref); List args = getArgs(gc.args()); if (args.isEmpty()) - throw new ParsingException("Ghost call cannot have empty arguments"); + throw new SyntaxError("Ghost call cannot have empty arguments", ref); return new FunctionInvocation(name, args); } else { AliasCallContext gc = rc.aliasCall(); + String ref = gc.ID_UPPER().getText(); List args = getArgs(gc.args()); if (args.isEmpty()) - throw new ParsingException("Alias call cannot have empty arguments"); - return new AliasInvocation(gc.ID_UPPER().getText(), args); + throw new SyntaxError("Alias call cannot have empty arguments", ref); + return new AliasInvocation(ref, args); } } - private List getArgs(ArgsContext args) throws ParsingException { + private List getArgs(ArgsContext args) throws LJError { List le = new ArrayList<>(); if (args != null) for (PredContext oc : args.pred()) { @@ -185,7 +189,7 @@ private List getArgs(ArgsContext args) throws ParsingException { return le; } - private Expression literalCreate(LiteralContext literalContext) throws ParsingException { + private Expression literalCreate(LiteralContext literalContext) throws LJError { if (literalContext.BOOL() != null) return new LiteralBoolean(literalContext.BOOL().getText()); else if (literalContext.STRING() != null) From be1a0f2cb9a7cda629e828f73b898edb3fc3c222 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 14 Nov 2025 14:15:02 +0000 Subject: [PATCH 02/16] Remove Error Checks From Visitor Methods --- .../ann_generation/FieldGhostsGeneration.java | 4 - .../ExternalRefinementTypeChecker.java | 9 -- .../MethodsFirstChecker.java | 12 --- .../RefinementTypeChecker.java | 90 ------------------- 4 files changed, 115 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java index 12b6b49f..74f12868 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java @@ -28,10 +28,6 @@ public Factory getFactory() { @Override public void visitCtClass(CtClass ctClass) { - if (diagnostics.foundError()) { - return; - } - ctClass.getDeclaredFields().stream().filter(fld -> fld.getType().getQualifiedName().equals("int")) .forEach(fld -> { CtTypeReference fld_type = fld.getType(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 799dcd1a..1679010a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -40,9 +40,6 @@ public void visitCtClass(CtClass ctClass) { @Override public void visitCtInterface(CtInterface intrface) { - if (diagnostics.foundError()) - return; - Optional externalRefinements = getExternalRefinement(intrface); if (externalRefinements.isPresent()) { this.prefix = externalRefinements.get(); @@ -59,9 +56,6 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtField(CtField f) { - if (diagnostics.foundError()) - return; - Optional oc; try { oc = getRefinementFromAnnotation(f); @@ -75,9 +69,6 @@ public void visitCtField(CtField f) { } public void visitCtMethod(CtMethod method) { - if (diagnostics.foundError()) - return; - CtType targetType = factory.Type().createReference(prefix).getTypeDeclaration(); if (targetType == null || !(targetType instanceof CtClass)) return; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index e3c5359d..67b914f3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -28,9 +28,6 @@ public MethodsFirstChecker(Context context, Factory factory) { @Override public void visitCtClass(CtClass ctClass) { - if (diagnostics.foundError()) - return; - context.reinitializeContext(); if (visitedClasses.contains(ctClass.getQualifiedName())) return; @@ -59,9 +56,6 @@ public void visitCtClass(CtClass ctClass) { @Override public void visitCtInterface(CtInterface intrface) { - if (diagnostics.foundError()) - return; - if (visitedClasses.contains(intrface.getQualifiedName())) return; else @@ -76,9 +70,6 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtConstructor(CtConstructor c) { - if (diagnostics.foundError()) - return; - context.enterContext(); getRefinementFromAnnotation(c); mfc.getConstructorRefinements(c); @@ -87,9 +78,6 @@ public void visitCtConstructor(CtConstructor c) { } public void visitCtMethod(CtMethod method) { - if (diagnostics.foundError()) - return; - context.enterContext(); mfc.getMethodRefinements(method); super.visitCtMethod(method); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index fe73de81..9c2a1137 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -66,10 +66,6 @@ public RefinementTypeChecker(Context context, Factory factory) { @Override public void visitCtClass(CtClass ctClass) { - if (diagnostics.foundError()) { - return; - } - // System.out.println("CTCLASS:"+ctClass.getSimpleName()); context.reinitializeContext(); super.visitCtClass(ctClass); @@ -77,10 +73,6 @@ public void visitCtClass(CtClass ctClass) { @Override public void visitCtInterface(CtInterface intrface) { - if (diagnostics.foundError()) { - return; - } - // System.out.println("CT INTERFACE: " +intrface.getSimpleName()); if (getExternalRefinement(intrface).isPresent()) { return; @@ -90,18 +82,11 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtAnnotationType(CtAnnotationType annotationType) { - if (diagnostics.foundError()) { - return; - } super.visitCtAnnotationType(annotationType); } @Override public void visitCtConstructor(CtConstructor c) { - if (diagnostics.foundError()) { - return; - } - context.enterContext(); mfc.loadFunctionInfo(c); super.visitCtConstructor(c); @@ -109,10 +94,6 @@ public void visitCtConstructor(CtConstructor c) { } public void visitCtMethod(CtMethod method) { - if (diagnostics.foundError()) { - return; - } - context.enterContext(); if (!method.getSignature().equals("main(java.lang.String[])")) { mfc.loadFunctionInfo(method); @@ -123,10 +104,6 @@ public void visitCtMethod(CtMethod method) { @Override public void visitCtLocalVariable(CtLocalVariable localVariable) { - if (diagnostics.foundError()) { - return; - } - super.visitCtLocalVariable(localVariable); // only declaration, no assignment if (localVariable.getAssignment() == null) { @@ -150,10 +127,6 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { @Override public void visitCtNewArray(CtNewArray newArray) { - if (diagnostics.foundError()) { - return; - } - super.visitCtNewArray(newArray); List> l = newArray.getDimensionExpressions(); // TODO only working for 1 dimension @@ -176,10 +149,6 @@ public void visitCtNewArray(CtNewArray newArray) { @Override public void visitCtThisAccess(CtThisAccess thisAccess) { - if (diagnostics.foundError()) { - return; - } - super.visitCtThisAccess(thisAccess); CtClass c = thisAccess.getParent(CtClass.class); String s = c.getSimpleName(); @@ -193,10 +162,6 @@ public void visitCtThisAccess(CtThisAccess thisAccess) { @SuppressWarnings("unchecked") @Override public void visitCtAssignment(CtAssignment assignment) throws LJError { - if (diagnostics.foundError()) { - return; - } - super.visitCtAssignment(assignment); CtExpression ex = assignment.getAssigned(); @@ -222,10 +187,6 @@ public void visitCtAssignment(CtAssignment assignment) th @Override public void visitCtArrayRead(CtArrayRead arrayRead) { - if (diagnostics.foundError()) { - return; - } - super.visitCtArrayRead(arrayRead); String name = String.format(Formats.INSTANCE, "arrayAccess", context.getCounter()); context.addVarToContext(name, arrayRead.getType(), new Predicate(), arrayRead); @@ -235,10 +196,6 @@ public void visitCtArrayRead(CtArrayRead arrayRead) { @Override public void visitCtLiteral(CtLiteral lit) { - if (diagnostics.foundError()) { - return; - } - List types = Arrays.asList(Types.IMPLEMENTED); String type = lit.getType().getQualifiedName(); if (types.contains(type)) { @@ -257,10 +214,6 @@ public void visitCtLiteral(CtLiteral lit) { @Override public void visitCtField(CtField f) { - if (diagnostics.foundError()) { - return; - } - super.visitCtField(f); Optional c = getRefinementFromAnnotation(f); @@ -280,10 +233,6 @@ public void visitCtField(CtField f) { @Override public void visitCtFieldRead(CtFieldRead fieldRead) { - if (diagnostics.foundError()) { - return; - } - String fieldName = fieldRead.getVariable().getSimpleName(); if (context.hasVariable(fieldName)) { RefinedVariable rv = context.getVariableByName(fieldName); @@ -315,10 +264,6 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { @Override public void visitCtVariableRead(CtVariableRead variableRead) { - if (diagnostics.foundError()) { - return; - } - super.visitCtVariableRead(variableRead); CtVariable varDecl = variableRead.getVariable().getDeclaration(); getPutVariableMetadada(variableRead, varDecl.getSimpleName()); @@ -329,48 +274,29 @@ public void visitCtVariableRead(CtVariableRead variableRead) { */ @Override public void visitCtBinaryOperator(CtBinaryOperator operator) { - if (diagnostics.foundError()) { - return; - } super.visitCtBinaryOperator(operator); otc.getBinaryOpRefinements(operator); } @Override public void visitCtUnaryOperator(CtUnaryOperator operator) { - if (diagnostics.foundError()) { - return; - } - super.visitCtUnaryOperator(operator); otc.getUnaryOpRefinements(operator); } public void visitCtInvocation(CtInvocation invocation) { - if (diagnostics.foundError()) { - return; - } - super.visitCtInvocation(invocation); mfc.getInvocationRefinements(invocation); } @Override public void visitCtReturn(CtReturn ret) { - if (diagnostics.foundError()) { - return; - } - super.visitCtReturn(ret); mfc.getReturnRefinements(ret); } @Override public void visitCtIf(CtIf ifElement) { - if (diagnostics.foundError()) { - return; - } - CtExpression exp = ifElement.getCondition(); Predicate expRefs = getExpressionRefinements(exp); @@ -418,10 +344,6 @@ public void visitCtIf(CtIf ifElement) { @Override public void visitCtArrayWrite(CtArrayWrite arrayWrite) { - if (diagnostics.foundError()) { - return; - } - super.visitCtArrayWrite(arrayWrite); CtExpression index = arrayWrite.getIndexExpression(); BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, arrayWrite); @@ -430,10 +352,6 @@ public void visitCtArrayWrite(CtArrayWrite arrayWrite) { @Override public void visitCtConditional(CtConditional conditional) { - if (diagnostics.foundError()) { - return; - } - super.visitCtConditional(conditional); Predicate cond = getRefinement(conditional.getCondition()); Predicate c = Predicate.createITE(cond, getRefinement(conditional.getThenExpression()), @@ -443,20 +361,12 @@ public void visitCtConditional(CtConditional conditional) { @Override public void visitCtConstructorCall(CtConstructorCall ctConstructorCall) { - if (diagnostics.foundError()) { - return; - } - super.visitCtConstructorCall(ctConstructorCall); mfc.getConstructorInvocationRefinements(ctConstructorCall); } @Override public void visitCtNewClass(CtNewClass newClass) { - if (diagnostics.foundError()) { - return; - } - super.visitCtNewClass(newClass); } From cad6b1b24f8469c6e348eb15948fb5b80c98fb58 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 14 Nov 2025 14:26:03 +0000 Subject: [PATCH 03/16] Catch Errors in Visitors --- .../ExternalRefinementTypeChecker.java | 16 +- .../MethodsFirstChecker.java | 39 ++- .../RefinementTypeChecker.java | 247 +++++++++++------- 3 files changed, 195 insertions(+), 107 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 1679010a..090de6c8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -48,8 +48,13 @@ public void visitCtInterface(CtInterface intrface) { diagnostics.add(new ExternalClassNotFoundWarning(intrface, message, prefix)); return; } - getRefinementFromAnnotation(intrface); - handleStateSetsFromAnnotation(intrface); + try { + getRefinementFromAnnotation(intrface); + handleStateSetsFromAnnotation(intrface); + } catch (LJError e) { + diagnostics.add(e); + return; + } super.visitCtInterface(intrface); } } @@ -98,7 +103,12 @@ public void visitCtMethod(CtMethod method) { } } MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); - mfc.getMethodRefinements(method, prefix); + try { + mfc.getMethodRefinements(method, prefix); + } catch (LJError e) { + diagnostics.add(e); + return; + } super.visitCtMethod(method); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 67b914f3..55ce9c60 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -1,10 +1,11 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.util.ArrayList; import java.util.List; +import static liquidjava.diagnostics.Diagnostics.diagnostics; + +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import spoon.reflect.declaration.CtClass; @@ -49,8 +50,13 @@ public void visitCtClass(CtClass ctClass) { if (ct instanceof CtClass) visitCtClass((CtClass) ct); } - getRefinementFromAnnotation(ctClass); - handleStateSetsFromAnnotation(ctClass); + try { + getRefinementFromAnnotation(ctClass); + handleStateSetsFromAnnotation(ctClass); + } catch (LJError e) { + diagnostics.add(e); + return; + } super.visitCtClass(ctClass); } @@ -63,23 +69,38 @@ public void visitCtInterface(CtInterface intrface) { if (getExternalRefinement(intrface).isPresent()) return; - getRefinementFromAnnotation(intrface); - handleStateSetsFromAnnotation(intrface); + try { + getRefinementFromAnnotation(intrface); + handleStateSetsFromAnnotation(intrface); + } catch (LJError e) { + diagnostics.add(e); + return; + } super.visitCtInterface(intrface); } @Override public void visitCtConstructor(CtConstructor c) { context.enterContext(); - getRefinementFromAnnotation(c); - mfc.getConstructorRefinements(c); + try { + getRefinementFromAnnotation(c); + mfc.getConstructorRefinements(c); + } catch (LJError e) { + diagnostics.add(e); + return; + } super.visitCtConstructor(c); context.exitContext(); } public void visitCtMethod(CtMethod method) { context.enterContext(); - mfc.getMethodRefinements(method); + try { + mfc.getMethodRefinements(method); + } catch (LJError e) { + diagnostics.add(e); + return; + } super.visitCtMethod(method); context.exitContext(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 9c2a1137..0d12afa2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -105,45 +105,56 @@ public void visitCtMethod(CtMethod method) { @Override public void visitCtLocalVariable(CtLocalVariable localVariable) { super.visitCtLocalVariable(localVariable); - // only declaration, no assignment - if (localVariable.getAssignment() == null) { - Optional a; - a = getRefinementFromAnnotation(localVariable); - context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), - localVariable); - } else { - String varName = localVariable.getSimpleName(); - CtExpression e = localVariable.getAssignment(); - - Predicate refinementFound = getRefinement(e); - if (refinementFound == null) { - refinementFound = new Predicate(); + try { + // only declaration, no assignment + if (localVariable.getAssignment() == null) { + Optional a; + a = getRefinementFromAnnotation(localVariable); + context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), + localVariable); + } else { + String varName = localVariable.getSimpleName(); + CtExpression e = localVariable.getAssignment(); + + Predicate refinementFound = getRefinement(e); + if (refinementFound == null) { + refinementFound = new Predicate(); + } + context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); + checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); + AuxStateHandler.addStateRefinements(this, varName, e); } - context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); - checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); - AuxStateHandler.addStateRefinements(this, varName, e); + } catch (LJError e) { + diagnostics.add(e); + return; } } @Override public void visitCtNewArray(CtNewArray newArray) { super.visitCtNewArray(newArray); - List> l = newArray.getDimensionExpressions(); - // TODO only working for 1 dimension - for (CtExpression exp : l) { - Predicate c = getExpressionRefinements(exp); - String name = String.format(Formats.FRESH, context.getCounter()); - if (c.getVariableNames().contains(Keys.WILDCARD)) { - c = c.substituteVariable(Keys.WILDCARD, name); - } else { - c = Predicate.createEquals(Predicate.createVar(name), c); + + try { + List> l = newArray.getDimensionExpressions(); + // TODO only working for 1 dimension + for (CtExpression exp : l) { + Predicate c = getExpressionRefinements(exp); + String name = String.format(Formats.FRESH, context.getCounter()); + if (c.getVariableNames().contains(Keys.WILDCARD)) { + c = c.substituteVariable(Keys.WILDCARD, name); + } else { + c = Predicate.createEquals(Predicate.createVar(name), c); + } + context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp); + Predicate ep; + ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray), + Predicate.createVar(name)); + + newArray.putMetadata(Keys.REFINEMENT, ep); } - context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp); - Predicate ep; - ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray), - Predicate.createVar(name)); - - newArray.putMetadata(Keys.REFINEMENT, ep); + } catch (LJError e) { + diagnostics.add(e); + return; } } @@ -161,27 +172,31 @@ public void visitCtThisAccess(CtThisAccess thisAccess) { @SuppressWarnings("unchecked") @Override - public void visitCtAssignment(CtAssignment assignment) throws LJError { + public void visitCtAssignment(CtAssignment assignment) { super.visitCtAssignment(assignment); - CtExpression ex = assignment.getAssigned(); - - if (ex instanceof CtVariableWriteImpl) { - CtVariableReference var = ((CtVariableAccess) ex).getVariable(); - CtVariable varDecl = (CtVariable) var.getDeclaration(); - String name = var.getSimpleName(); - checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl); - - } else if (ex instanceof CtFieldWrite) { - CtFieldWrite fw = ((CtFieldWrite) ex); - CtFieldReference cr = fw.getVariable(); - CtField f = fw.getVariable().getDeclaration(); - String updatedVarName = String.format(Formats.THIS, cr.getSimpleName()); - checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f); - - // corresponding ghost function update - if (fw.getVariable().getType().toString().equals("int")) { - AuxStateHandler.updateGhostField(fw, this); + try { + CtExpression ex = assignment.getAssigned(); + if (ex instanceof CtVariableWriteImpl) { + CtVariableReference var = ((CtVariableAccess) ex).getVariable(); + CtVariable varDecl = (CtVariable) var.getDeclaration(); + String name = var.getSimpleName(); + checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl); + + } else if (ex instanceof CtFieldWrite) { + CtFieldWrite fw = ((CtFieldWrite) ex); + CtFieldReference cr = fw.getVariable(); + CtField f = fw.getVariable().getDeclaration(); + String updatedVarName = String.format(Formats.THIS, cr.getSimpleName()); + checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f); + + // corresponding ghost function update + if (fw.getVariable().getType().toString().equals("int")) { + AuxStateHandler.updateGhostField(fw, this); + } } + } catch (LJError e) { + diagnostics.add(e); + return; } } @@ -215,50 +230,55 @@ public void visitCtLiteral(CtLiteral lit) { @Override public void visitCtField(CtField f) { super.visitCtField(f); - Optional c = getRefinementFromAnnotation(f); - - // context.addVarToContext(f.getSimpleName(), f.getType(), - // c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new - // Predicate()) ); - String nname = String.format(Formats.THIS, f.getSimpleName()); - Predicate ret = new Predicate(); - if (c.isPresent()) { - ret = c.get().substituteVariable(Keys.WILDCARD, nname).substituteVariable(f.getSimpleName(), nname); - } - RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, f); - if (v instanceof Variable) { - ((Variable) v).setLocation("this"); + try { + Optional c = getRefinementFromAnnotation(f); + String name = String.format(Formats.THIS, f.getSimpleName()); + Predicate ret = new Predicate(); + if (c.isPresent()) { + ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name); + } + RefinedVariable v = context.addVarToContext(name, f.getType(), ret, f); + if (v instanceof Variable) { + ((Variable) v).setLocation("this"); + } + } catch (LJError e) { + diagnostics.add(e); + return; } } @Override public void visitCtFieldRead(CtFieldRead fieldRead) { - String fieldName = fieldRead.getVariable().getSimpleName(); - if (context.hasVariable(fieldName)) { - RefinedVariable rv = context.getVariableByName(fieldName); - if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent() - && ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) { - fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName)); - } else { + try { + String fieldName = fieldRead.getVariable().getSimpleName(); + if (context.hasVariable(fieldName)) { + RefinedVariable rv = context.getVariableByName(fieldName); + if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent() + && ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) { + fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName)); + } else { + fieldRead.putMetadata(Keys.REFINEMENT, + Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName))); + } + + } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) { + String thisName = String.format(Formats.THIS, fieldName); fieldRead.putMetadata(Keys.REFINEMENT, - Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName))); - } + Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); - } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) { - String thisName = String.format(Formats.THIS, fieldName); - fieldRead.putMetadata(Keys.REFINEMENT, - Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); - - } else if (fieldRead.getVariable().getSimpleName().equals("length")) { - String targetName = fieldRead.getTarget().toString(); - fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), - BuiltinFunctionPredicate.length(targetName, fieldRead))); - - } else { - fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); - // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE + } else if (fieldRead.getVariable().getSimpleName().equals("length")) { + String targetName = fieldRead.getTarget().toString(); + fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), + BuiltinFunctionPredicate.length(targetName, fieldRead))); + + } else { + fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); + // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE + } + } catch (LJError e) { + diagnostics.add(e); + return; } - super.visitCtFieldRead(fieldRead); } @@ -275,30 +295,57 @@ public void visitCtVariableRead(CtVariableRead variableRead) { @Override public void visitCtBinaryOperator(CtBinaryOperator operator) { super.visitCtBinaryOperator(operator); - otc.getBinaryOpRefinements(operator); + try { + otc.getBinaryOpRefinements(operator); + } catch (LJError e) { + diagnostics.add(e); + return; + } } @Override public void visitCtUnaryOperator(CtUnaryOperator operator) { super.visitCtUnaryOperator(operator); - otc.getUnaryOpRefinements(operator); + try { + otc.getUnaryOpRefinements(operator); + } catch (LJError e) { + diagnostics.add(e); + return; + } } public void visitCtInvocation(CtInvocation invocation) { super.visitCtInvocation(invocation); - mfc.getInvocationRefinements(invocation); + try { + mfc.getInvocationRefinements(invocation); + } catch (LJError e) { + diagnostics.add(e); + return; + } } @Override public void visitCtReturn(CtReturn ret) { super.visitCtReturn(ret); - mfc.getReturnRefinements(ret); + try { + mfc.getReturnRefinements(ret); + } catch (LJError e) { + diagnostics.add(e); + return; + } } @Override public void visitCtIf(CtIf ifElement) { CtExpression exp = ifElement.getCondition(); - Predicate expRefs = getExpressionRefinements(exp); + Predicate expRefs; + + try { + expRefs = getExpressionRefinements(exp); + } catch (LJError e) { + diagnostics.add(e); + return; + } String freshVarName = String.format(Formats.FRESH, context.getCounter()); expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName); @@ -345,9 +392,14 @@ public void visitCtIf(CtIf ifElement) { @Override public void visitCtArrayWrite(CtArrayWrite arrayWrite) { super.visitCtArrayWrite(arrayWrite); - CtExpression index = arrayWrite.getIndexExpression(); - BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, arrayWrite); - arrayWrite.putMetadata(Keys.REFINEMENT, fp); + try { + CtExpression index = arrayWrite.getIndexExpression(); + BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, arrayWrite); + arrayWrite.putMetadata(Keys.REFINEMENT, fp); + } catch (LJError e) { + diagnostics.add(e); + return; + } } @Override @@ -362,7 +414,12 @@ public void visitCtConditional(CtConditional conditional) { @Override public void visitCtConstructorCall(CtConstructorCall ctConstructorCall) { super.visitCtConstructorCall(ctConstructorCall); - mfc.getConstructorInvocationRefinements(ctConstructorCall); + try { + mfc.getConstructorInvocationRefinements(ctConstructorCall); + } catch (LJError e) { + diagnostics.add(e); + return; + } } @Override From efbf9c38d702ab872fbbb4f749f345d187b89d5e Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 14 Nov 2025 15:04:17 +0000 Subject: [PATCH 04/16] Revert "Catch Errors in Visitors" This reverts commit cad6b1b24f8469c6e348eb15948fb5b80c98fb58. --- .../ExternalRefinementTypeChecker.java | 16 +- .../MethodsFirstChecker.java | 39 +-- .../RefinementTypeChecker.java | 247 +++++++----------- 3 files changed, 107 insertions(+), 195 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 090de6c8..1679010a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -48,13 +48,8 @@ public void visitCtInterface(CtInterface intrface) { diagnostics.add(new ExternalClassNotFoundWarning(intrface, message, prefix)); return; } - try { - getRefinementFromAnnotation(intrface); - handleStateSetsFromAnnotation(intrface); - } catch (LJError e) { - diagnostics.add(e); - return; - } + getRefinementFromAnnotation(intrface); + handleStateSetsFromAnnotation(intrface); super.visitCtInterface(intrface); } } @@ -103,12 +98,7 @@ public void visitCtMethod(CtMethod method) { } } MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); - try { - mfc.getMethodRefinements(method, prefix); - } catch (LJError e) { - diagnostics.add(e); - return; - } + mfc.getMethodRefinements(method, prefix); super.visitCtMethod(method); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 55ce9c60..67b914f3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -1,11 +1,10 @@ package liquidjava.processor.refinement_checker; +import static liquidjava.diagnostics.Diagnostics.diagnostics; + import java.util.ArrayList; import java.util.List; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - -import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import spoon.reflect.declaration.CtClass; @@ -50,13 +49,8 @@ public void visitCtClass(CtClass ctClass) { if (ct instanceof CtClass) visitCtClass((CtClass) ct); } - try { - getRefinementFromAnnotation(ctClass); - handleStateSetsFromAnnotation(ctClass); - } catch (LJError e) { - diagnostics.add(e); - return; - } + getRefinementFromAnnotation(ctClass); + handleStateSetsFromAnnotation(ctClass); super.visitCtClass(ctClass); } @@ -69,38 +63,23 @@ public void visitCtInterface(CtInterface intrface) { if (getExternalRefinement(intrface).isPresent()) return; - try { - getRefinementFromAnnotation(intrface); - handleStateSetsFromAnnotation(intrface); - } catch (LJError e) { - diagnostics.add(e); - return; - } + getRefinementFromAnnotation(intrface); + handleStateSetsFromAnnotation(intrface); super.visitCtInterface(intrface); } @Override public void visitCtConstructor(CtConstructor c) { context.enterContext(); - try { - getRefinementFromAnnotation(c); - mfc.getConstructorRefinements(c); - } catch (LJError e) { - diagnostics.add(e); - return; - } + getRefinementFromAnnotation(c); + mfc.getConstructorRefinements(c); super.visitCtConstructor(c); context.exitContext(); } public void visitCtMethod(CtMethod method) { context.enterContext(); - try { - mfc.getMethodRefinements(method); - } catch (LJError e) { - diagnostics.add(e); - return; - } + mfc.getMethodRefinements(method); super.visitCtMethod(method); context.exitContext(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 0d12afa2..9c2a1137 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -105,56 +105,45 @@ public void visitCtMethod(CtMethod method) { @Override public void visitCtLocalVariable(CtLocalVariable localVariable) { super.visitCtLocalVariable(localVariable); - try { - // only declaration, no assignment - if (localVariable.getAssignment() == null) { - Optional a; - a = getRefinementFromAnnotation(localVariable); - context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), - localVariable); - } else { - String varName = localVariable.getSimpleName(); - CtExpression e = localVariable.getAssignment(); - - Predicate refinementFound = getRefinement(e); - if (refinementFound == null) { - refinementFound = new Predicate(); - } - context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); - checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); - AuxStateHandler.addStateRefinements(this, varName, e); + // only declaration, no assignment + if (localVariable.getAssignment() == null) { + Optional a; + a = getRefinementFromAnnotation(localVariable); + context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), + localVariable); + } else { + String varName = localVariable.getSimpleName(); + CtExpression e = localVariable.getAssignment(); + + Predicate refinementFound = getRefinement(e); + if (refinementFound == null) { + refinementFound = new Predicate(); } - } catch (LJError e) { - diagnostics.add(e); - return; + context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); + checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable); + AuxStateHandler.addStateRefinements(this, varName, e); } } @Override public void visitCtNewArray(CtNewArray newArray) { super.visitCtNewArray(newArray); - - try { - List> l = newArray.getDimensionExpressions(); - // TODO only working for 1 dimension - for (CtExpression exp : l) { - Predicate c = getExpressionRefinements(exp); - String name = String.format(Formats.FRESH, context.getCounter()); - if (c.getVariableNames().contains(Keys.WILDCARD)) { - c = c.substituteVariable(Keys.WILDCARD, name); - } else { - c = Predicate.createEquals(Predicate.createVar(name), c); - } - context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp); - Predicate ep; - ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray), - Predicate.createVar(name)); - - newArray.putMetadata(Keys.REFINEMENT, ep); + List> l = newArray.getDimensionExpressions(); + // TODO only working for 1 dimension + for (CtExpression exp : l) { + Predicate c = getExpressionRefinements(exp); + String name = String.format(Formats.FRESH, context.getCounter()); + if (c.getVariableNames().contains(Keys.WILDCARD)) { + c = c.substituteVariable(Keys.WILDCARD, name); + } else { + c = Predicate.createEquals(Predicate.createVar(name), c); } - } catch (LJError e) { - diagnostics.add(e); - return; + context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp); + Predicate ep; + ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray), + Predicate.createVar(name)); + + newArray.putMetadata(Keys.REFINEMENT, ep); } } @@ -172,31 +161,27 @@ public void visitCtThisAccess(CtThisAccess thisAccess) { @SuppressWarnings("unchecked") @Override - public void visitCtAssignment(CtAssignment assignment) { + public void visitCtAssignment(CtAssignment assignment) throws LJError { super.visitCtAssignment(assignment); - try { - CtExpression ex = assignment.getAssigned(); - if (ex instanceof CtVariableWriteImpl) { - CtVariableReference var = ((CtVariableAccess) ex).getVariable(); - CtVariable varDecl = (CtVariable) var.getDeclaration(); - String name = var.getSimpleName(); - checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl); - - } else if (ex instanceof CtFieldWrite) { - CtFieldWrite fw = ((CtFieldWrite) ex); - CtFieldReference cr = fw.getVariable(); - CtField f = fw.getVariable().getDeclaration(); - String updatedVarName = String.format(Formats.THIS, cr.getSimpleName()); - checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f); - - // corresponding ghost function update - if (fw.getVariable().getType().toString().equals("int")) { - AuxStateHandler.updateGhostField(fw, this); - } + CtExpression ex = assignment.getAssigned(); + + if (ex instanceof CtVariableWriteImpl) { + CtVariableReference var = ((CtVariableAccess) ex).getVariable(); + CtVariable varDecl = (CtVariable) var.getDeclaration(); + String name = var.getSimpleName(); + checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl); + + } else if (ex instanceof CtFieldWrite) { + CtFieldWrite fw = ((CtFieldWrite) ex); + CtFieldReference cr = fw.getVariable(); + CtField f = fw.getVariable().getDeclaration(); + String updatedVarName = String.format(Formats.THIS, cr.getSimpleName()); + checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f); + + // corresponding ghost function update + if (fw.getVariable().getType().toString().equals("int")) { + AuxStateHandler.updateGhostField(fw, this); } - } catch (LJError e) { - diagnostics.add(e); - return; } } @@ -230,55 +215,50 @@ public void visitCtLiteral(CtLiteral lit) { @Override public void visitCtField(CtField f) { super.visitCtField(f); - try { - Optional c = getRefinementFromAnnotation(f); - String name = String.format(Formats.THIS, f.getSimpleName()); - Predicate ret = new Predicate(); - if (c.isPresent()) { - ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name); - } - RefinedVariable v = context.addVarToContext(name, f.getType(), ret, f); - if (v instanceof Variable) { - ((Variable) v).setLocation("this"); - } - } catch (LJError e) { - diagnostics.add(e); - return; + Optional c = getRefinementFromAnnotation(f); + + // context.addVarToContext(f.getSimpleName(), f.getType(), + // c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new + // Predicate()) ); + String nname = String.format(Formats.THIS, f.getSimpleName()); + Predicate ret = new Predicate(); + if (c.isPresent()) { + ret = c.get().substituteVariable(Keys.WILDCARD, nname).substituteVariable(f.getSimpleName(), nname); + } + RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, f); + if (v instanceof Variable) { + ((Variable) v).setLocation("this"); } } @Override public void visitCtFieldRead(CtFieldRead fieldRead) { - try { - String fieldName = fieldRead.getVariable().getSimpleName(); - if (context.hasVariable(fieldName)) { - RefinedVariable rv = context.getVariableByName(fieldName); - if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent() - && ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) { - fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName)); - } else { - fieldRead.putMetadata(Keys.REFINEMENT, - Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName))); - } - - } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) { - String thisName = String.format(Formats.THIS, fieldName); - fieldRead.putMetadata(Keys.REFINEMENT, - Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); - - } else if (fieldRead.getVariable().getSimpleName().equals("length")) { - String targetName = fieldRead.getTarget().toString(); - fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), - BuiltinFunctionPredicate.length(targetName, fieldRead))); - + String fieldName = fieldRead.getVariable().getSimpleName(); + if (context.hasVariable(fieldName)) { + RefinedVariable rv = context.getVariableByName(fieldName); + if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent() + && ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) { + fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName)); } else { - fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); - // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE + fieldRead.putMetadata(Keys.REFINEMENT, + Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName))); } - } catch (LJError e) { - diagnostics.add(e); - return; + + } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) { + String thisName = String.format(Formats.THIS, fieldName); + fieldRead.putMetadata(Keys.REFINEMENT, + Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); + + } else if (fieldRead.getVariable().getSimpleName().equals("length")) { + String targetName = fieldRead.getTarget().toString(); + fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), + BuiltinFunctionPredicate.length(targetName, fieldRead))); + + } else { + fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); + // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE } + super.visitCtFieldRead(fieldRead); } @@ -295,57 +275,30 @@ public void visitCtVariableRead(CtVariableRead variableRead) { @Override public void visitCtBinaryOperator(CtBinaryOperator operator) { super.visitCtBinaryOperator(operator); - try { - otc.getBinaryOpRefinements(operator); - } catch (LJError e) { - diagnostics.add(e); - return; - } + otc.getBinaryOpRefinements(operator); } @Override public void visitCtUnaryOperator(CtUnaryOperator operator) { super.visitCtUnaryOperator(operator); - try { - otc.getUnaryOpRefinements(operator); - } catch (LJError e) { - diagnostics.add(e); - return; - } + otc.getUnaryOpRefinements(operator); } public void visitCtInvocation(CtInvocation invocation) { super.visitCtInvocation(invocation); - try { - mfc.getInvocationRefinements(invocation); - } catch (LJError e) { - diagnostics.add(e); - return; - } + mfc.getInvocationRefinements(invocation); } @Override public void visitCtReturn(CtReturn ret) { super.visitCtReturn(ret); - try { - mfc.getReturnRefinements(ret); - } catch (LJError e) { - diagnostics.add(e); - return; - } + mfc.getReturnRefinements(ret); } @Override public void visitCtIf(CtIf ifElement) { CtExpression exp = ifElement.getCondition(); - Predicate expRefs; - - try { - expRefs = getExpressionRefinements(exp); - } catch (LJError e) { - diagnostics.add(e); - return; - } + Predicate expRefs = getExpressionRefinements(exp); String freshVarName = String.format(Formats.FRESH, context.getCounter()); expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName); @@ -392,14 +345,9 @@ public void visitCtIf(CtIf ifElement) { @Override public void visitCtArrayWrite(CtArrayWrite arrayWrite) { super.visitCtArrayWrite(arrayWrite); - try { - CtExpression index = arrayWrite.getIndexExpression(); - BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, arrayWrite); - arrayWrite.putMetadata(Keys.REFINEMENT, fp); - } catch (LJError e) { - diagnostics.add(e); - return; - } + CtExpression index = arrayWrite.getIndexExpression(); + BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, arrayWrite); + arrayWrite.putMetadata(Keys.REFINEMENT, fp); } @Override @@ -414,12 +362,7 @@ public void visitCtConditional(CtConditional conditional) { @Override public void visitCtConstructorCall(CtConstructorCall ctConstructorCall) { super.visitCtConstructorCall(ctConstructorCall); - try { - mfc.getConstructorInvocationRefinements(ctConstructorCall); - } catch (LJError e) { - diagnostics.add(e); - return; - } + mfc.getConstructorInvocationRefinements(ctConstructorCall); } @Override From 77db4a40c86ed4eba6cef5254cf175617abb8e72 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 14 Nov 2025 17:46:14 +0000 Subject: [PATCH 05/16] Add Try Catch in Visitors --- .../test/currentlyTesting/SimpleTest.java | 13 ++++++-- .../liquidjava/diagnostics/LJDiagnostic.java | 2 +- .../MethodsFirstChecker.java | 8 ++++- .../RefinementTypeChecker.java | 30 ++++++++++++++++--- 4 files changed, 45 insertions(+), 8 deletions(-) diff --git a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java index 48999074..c6a44cf3 100644 --- a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java +++ b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java @@ -4,9 +4,18 @@ class SimpleTest { - @Refinement("return > 0") + + + public int test2() { + @Refinement("y > 0") + int y = -3; + return y; + } + public int test() { - return 10; + @Refinement("x > 0") + int x = -5; + return x; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 34b21f3d..cd4cd99f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -6,7 +6,7 @@ import spoon.reflect.cu.SourcePosition; -public class LJDiagnostic extends Exception { +public class LJDiagnostic extends RuntimeException { private String title; private String message; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 67b914f3..05ba44e0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -5,6 +5,7 @@ import java.util.ArrayList; import java.util.List; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import spoon.reflect.declaration.CtClass; @@ -51,7 +52,12 @@ public void visitCtClass(CtClass ctClass) { } getRefinementFromAnnotation(ctClass); handleStateSetsFromAnnotation(ctClass); - super.visitCtClass(ctClass); + try { + super.visitCtClass(ctClass); + } catch (LJError e) { + System.out.println("Error in class: " + ctClass.getSimpleName()); + diagnostics.add(e); + } } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 9c2a1137..d20d268c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -68,7 +68,14 @@ public RefinementTypeChecker(Context context, Factory factory) { public void visitCtClass(CtClass ctClass) { // System.out.println("CTCLASS:"+ctClass.getSimpleName()); context.reinitializeContext(); - super.visitCtClass(ctClass); + + try { + super.visitCtClass(ctClass); + } catch (LJError e) { + System.out.println("Error in class: " + ctClass.getSimpleName()); + diagnostics.add(e); + } + } @Override @@ -77,7 +84,12 @@ public void visitCtInterface(CtInterface intrface) { if (getExternalRefinement(intrface).isPresent()) { return; } - super.visitCtInterface(intrface); + try { + super.visitCtInterface(intrface); + } catch (LJError e) { + System.out.println("Error in interface: " + intrface.getSimpleName()); + diagnostics.add(e); + } } @Override @@ -89,7 +101,12 @@ public void visitCtAnnotationType(CtAnnotationType ann public void visitCtConstructor(CtConstructor c) { context.enterContext(); mfc.loadFunctionInfo(c); - super.visitCtConstructor(c); + try { + super.visitCtConstructor(c); + } catch (LJError e) { + System.out.println("Error in constructor: " + c.getSimpleName()); + diagnostics.add(e); + } context.exitContext(); } @@ -98,7 +115,12 @@ public void visitCtMethod(CtMethod method) { if (!method.getSignature().equals("main(java.lang.String[])")) { mfc.loadFunctionInfo(method); } - super.visitCtMethod(method); + try { + super.visitCtMethod(method); + } catch (LJError e) { + System.out.println("Error in method: " + method.getSimpleName()); + diagnostics.add(e); + } context.exitContext(); } From fe27fe6408ae439ce7acd4fdf2b88200b292b098 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 14 Nov 2025 23:19:48 +0000 Subject: [PATCH 06/16] Bug Fix --- .../test/currentlyTesting/SimpleTest.java | 110 +----------------- .../refinement_checker/TypeChecker.java | 3 - 2 files changed, 6 insertions(+), 107 deletions(-) diff --git a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java index c6a44cf3..2d828c30 100644 --- a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java +++ b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java @@ -4,111 +4,13 @@ class SimpleTest { - - - public int test2() { - @Refinement("y > 0") - int y = -3; - return y; + void test1() { + @Refinement("x > 0") + int x = -1; } - public int test() { - @Refinement("x > 0") - int x = -5; - return x; + void test2() { + @Refinement("y > 0") + int y = -2; } } - -// @RefinementAlias("Percentage(int x) { 0 <= x && x <= 100 }") -// @Refinement("Percentage(_)") -// public static int addBonus( -// @Refinement("Percentage(grade)") int grade, -// @Refinement("Percentage(bonus) && (bonus < grade)") -// int bonus) { -// -// if((grade + bonus) > 100) -// return 100; -// -// else -// return grade+bonus; -// } -// - -// @Refinement("_ > 10") -// int i = 10; - -// @Refinement("sum(_) > 30") -// Account a = new Account(50); -// a.deposit(60); - -// Account b = new Account(138); -// b = a.transferTo(b, 10); -// -// @Refinement("sum(_) == 148") -// Account c = b; - -// Order o = new Order(); -// -// Order f = o.addItem("shirt", 60).addGift(); -// .getNewOrderPayThis().addItem("t", 6).addItem("t", 1); -// o.addGift(); -// f.addItem("l", 1).pay(000).addGift().pay(000);//.addTransportCosts().sendToAddress("home"); - -// TrafficLight tl = new TrafficLight(); -// tl.transitionToAmber(); -// - -// TrafficLight tl2 = tl.getTrafficLightStartingRed(); -// tl2.transitionToFlashingAmber(); - -// tl.transitionToAmber(); -// tl.transitionToAmber(); - -// tl.passagersCross(); -// tl.intermitentMalfunction(); - -// tl.transitionToFlashingAmber(); - -// @Refinement("size(al) < 4") -// ArrayList al = new ArrayList(); -// al.add(1); -// al.add(1); -// al.get(2); - -// @Refinement("size(t) == 3") -// ArrayList t = al; - -// -// Order o = new Order(); -// o.addItem("shirt", 5) -// .addItem("shirt", 10) -// .addItem("h", 20) -// .addItem("h", 6); - -// InputStreamReader isr = new InputStreamReader(System.in); -// isr.read(); -// isr.read(); -// isr.read(); -// isr.close(); -// -// //... -// isr.read(); - -// @Refinement("_ > 0") -// public int fun (int[] arr) { -// return max(arr[0], 1); -// } -// - -// //@Refinement("_.length(x) >= 0") == -//// @Refinement("length(_, x) >= 0") -//// int[] a1 = new int[5]; -// K(.., ..) - -// } - -// See error NaN -// @Refinement("true") -// double b = 0/0; -// @Refinement("_ > 5") -// double c = b; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index efc82261..65776246 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -88,9 +88,6 @@ public Optional getRefinementFromAnnotation(CtElement element) throws throw new InvalidRefinementError(element, "Refinement predicate must be a boolean expression", ref.get()); } - if (diagnostics.foundError()) - return Optional.empty(); - constr = Optional.of(p); } return constr; From 47c48753074a0a6c5b2bcd69232499be99a982b6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 10:33:22 +0000 Subject: [PATCH 07/16] Refactor `Diagnostics` --- .../test/currentlyTesting/SimpleTest.java | 3 + .../liquidjava/api/CommandLineLauncher.java | 5 +- .../liquidjava/diagnostics/Diagnostics.java | 59 ++++++------------- .../liquidjava/diagnostics/LJDiagnostic.java | 1 - .../processor/RefinementProcessor.java | 15 ++++- .../ann_generation/FieldGhostsGeneration.java | 2 - .../ExternalRefinementTypeChecker.java | 13 ++-- .../MethodsFirstChecker.java | 10 +--- .../RefinementTypeChecker.java | 25 ++++---- .../refinement_checker/TypeChecker.java | 17 +++--- .../refinement_checker/VCChecker.java | 12 ++-- .../general_checkers/OperationsChecker.java | 3 +- .../object_checkers/AuxStateHandler.java | 25 +++++--- .../parsing/RefinementsParser.java | 1 + .../liquidjava/api/tests/TestExamples.java | 4 +- 15 files changed, 89 insertions(+), 106 deletions(-) diff --git a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java index 2d828c30..1d2feab6 100644 --- a/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java +++ b/liquidjava-example/src/main/java/test/currentlyTesting/SimpleTest.java @@ -12,5 +12,8 @@ void test1() { void test2() { @Refinement("y > 0") int y = -2; + + @Refinement("z > 0") + int z = 3; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index b1187271..ccf56c6a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -1,11 +1,10 @@ package liquidjava.api; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.io.File; import java.util.Arrays; import java.util.List; +import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.CustomError; import liquidjava.processor.RefinementProcessor; import spoon.Launcher; @@ -26,6 +25,7 @@ public static void main(String[] args) { } List paths = Arrays.asList(args); launch(paths.toArray(new String[0])); + Diagnostics diagnostics = Diagnostics.getInstance(); if (diagnostics.foundError()) { System.out.println(diagnostics.getErrorOutput()); } else { @@ -37,6 +37,7 @@ public static void main(String[] args) { public static void launch(String... paths) { System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", "")); + Diagnostics diagnostics = Diagnostics.getInstance(); Launcher launcher = new Launcher(); for (String path : paths) { if (!new File(path).exists()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java index dd69be2e..fc7c75f7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java @@ -1,6 +1,6 @@ package liquidjava.diagnostics; -import java.util.ArrayList; +import java.util.LinkedHashSet; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.warnings.LJWarning; @@ -11,24 +11,26 @@ * @see LJWarning */ public class Diagnostics { - public static final Diagnostics diagnostics = new Diagnostics(); + private static final Diagnostics instance = new Diagnostics(); - private ArrayList errors; - private ArrayList warnings; + private LinkedHashSet errors; + private LinkedHashSet warnings; private Diagnostics() { - this.errors = new ArrayList<>(); - this.warnings = new ArrayList<>(); + this.errors = new LinkedHashSet<>(); + this.warnings = new LinkedHashSet<>(); + } + + public static Diagnostics getInstance() { + return instance; } public void add(LJError error) { - if (!this.errors.contains(error)) - this.errors.add(error); + this.errors.add(error); } public void add(LJWarning warning) { - if (!this.warnings.contains(warning)) - this.warnings.add(warning); + this.warnings.add(warning); } public boolean foundError() { @@ -39,52 +41,25 @@ public boolean foundWarning() { return !this.warnings.isEmpty(); } - public ArrayList getErrors() { + public LinkedHashSet getErrors() { return this.errors; } - public ArrayList getWarnings() { + public LinkedHashSet getWarnings() { return this.warnings; } - public LJError getError() { - return foundError() ? this.errors.get(0) : null; - } - - public LJWarning getWarning() { - return foundWarning() ? this.warnings.get(0) : null; - } - public void clear() { this.errors.clear(); this.warnings.clear(); } public String getErrorOutput() { - StringBuilder sb = new StringBuilder(); - if (foundError()) { - for (LJError error : errors) { - sb.append(error.toString()).append("\n"); - } - } else { - if (foundWarning()) { - sb.append("Warnings:\n"); - for (LJWarning warning : warnings) { - sb.append(warning.getMessage()).append("\n"); - } - sb.append("Passed Verification!\n"); - } - } - return sb.toString(); + return String.join("\n", errors.stream().map(LJError::toString).toList()) + (errors.isEmpty() ? "" : "\n"); } public String getWarningOutput() { - StringBuilder sb = new StringBuilder(); - if (foundWarning()) { - for (LJWarning warning : warnings) { - sb.append(warning.toString()).append("\n"); - } - } - return sb.toString(); + return String.join("\n", warnings.stream().map(LJWarning::toString).toList()) + + (warnings.isEmpty() ? "" : "\n"); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index cd4cd99f..b7c43ee1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -113,7 +113,6 @@ public String getSnippet() { } return sb.toString(); } catch (Exception e) { - e.printStackTrace(); return null; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index 5254f494..99d14e49 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -3,6 +3,8 @@ import java.util.ArrayList; import java.util.List; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.ann_generation.FieldGhostsGeneration; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.ExternalRefinementTypeChecker; @@ -17,6 +19,7 @@ public class RefinementProcessor extends AbstractProcessor { List visitedPackages = new ArrayList<>(); Factory factory; + Diagnostics diagnostics = Diagnostics.getInstance(); public RefinementProcessor(Factory factory) { this.factory = factory; @@ -29,9 +32,15 @@ public void process(CtPackage pkg) { Context c = Context.getInstance(); c.reinitializeAllContext(); - pkg.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts - pkg.accept(new ExternalRefinementTypeChecker(c, factory)); - pkg.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers) + // we need to catch errors here + try { + pkg.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts + pkg.accept(new ExternalRefinementTypeChecker(c, factory)); + pkg.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers) + } catch (LJError e) { + diagnostics.add(e); + } + // here we catch the errors in the visitors pkg.accept(new RefinementTypeChecker(c, factory)); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java index 74f12868..29600b36 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java @@ -1,7 +1,5 @@ package liquidjava.processor.ann_generation; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import liquidjava.processor.context.Context; import liquidjava.specification.Ghost; import spoon.reflect.declaration.*; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 1679010a..2321b1f6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -1,10 +1,10 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.util.Arrays; import java.util.List; import java.util.Optional; + +import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning; import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning; @@ -28,6 +28,7 @@ public class ExternalRefinementTypeChecker extends TypeChecker { String prefix; MethodsFunctionsChecker m; + Diagnostics diagnostics = Diagnostics.getInstance(); public ExternalRefinementTypeChecker(Context context, Factory factory) { super(context, factory); @@ -56,13 +57,7 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtField(CtField f) { - Optional oc; - try { - oc = getRefinementFromAnnotation(f); - } catch (LJError e) { - diagnostics.add(e); - return; - } + Optional oc = getRefinementFromAnnotation(f); Predicate c = oc.orElse(new Predicate()); context.addGlobalVariableToContext(f.getSimpleName(), prefix, f.getType(), c); super.visitCtField(f); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 05ba44e0..bff427ec 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -1,11 +1,8 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.util.ArrayList; import java.util.List; -import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import spoon.reflect.declaration.CtClass; @@ -52,12 +49,7 @@ public void visitCtClass(CtClass ctClass) { } getRefinementFromAnnotation(ctClass); handleStateSetsFromAnnotation(ctClass); - try { - super.visitCtClass(ctClass); - } catch (LJError e) { - System.out.println("Error in class: " + ctClass.getSimpleName()); - diagnostics.add(e); - } + super.visitCtClass(ctClass); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index d20d268c..d318f25e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -1,12 +1,11 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.lang.annotation.Annotation; import java.util.Arrays; import java.util.List; import java.util.Optional; +import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; @@ -55,6 +54,7 @@ public class RefinementTypeChecker extends TypeChecker { // Auxiliary TypeCheckers OperationsChecker otc; MethodsFunctionsChecker mfc; + Diagnostics diagnostics = Diagnostics.getInstance(); public RefinementTypeChecker(Context context, Factory factory) { super(context, factory); @@ -72,10 +72,9 @@ public void visitCtClass(CtClass ctClass) { try { super.visitCtClass(ctClass); } catch (LJError e) { - System.out.println("Error in class: " + ctClass.getSimpleName()); diagnostics.add(e); } - + } @Override @@ -87,7 +86,6 @@ public void visitCtInterface(CtInterface intrface) { try { super.visitCtInterface(intrface); } catch (LJError e) { - System.out.println("Error in interface: " + intrface.getSimpleName()); diagnostics.add(e); } } @@ -104,7 +102,6 @@ public void visitCtConstructor(CtConstructor c) { try { super.visitCtConstructor(c); } catch (LJError e) { - System.out.println("Error in constructor: " + c.getSimpleName()); diagnostics.add(e); } context.exitContext(); @@ -118,7 +115,6 @@ public void visitCtMethod(CtMethod method) { try { super.visitCtMethod(method); } catch (LJError e) { - System.out.println("Error in method: " + method.getSimpleName()); diagnostics.add(e); } context.exitContext(); @@ -163,8 +159,8 @@ public void visitCtNewArray(CtNewArray newArray) { context.addVarToContext(name, factory.Type().INTEGER_PRIMITIVE, c, exp); Predicate ep; ep = Predicate.createEquals(BuiltinFunctionPredicate.length(Keys.WILDCARD, newArray), - Predicate.createVar(name)); - + Predicate.createVar(name)); + newArray.putMetadata(Keys.REFINEMENT, ep); } } @@ -238,7 +234,7 @@ public void visitCtLiteral(CtLiteral lit) { public void visitCtField(CtField f) { super.visitCtField(f); Optional c = getRefinementFromAnnotation(f); - + // context.addVarToContext(f.getSimpleName(), f.getType(), // c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new // Predicate()) ); @@ -274,8 +270,8 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { } else if (fieldRead.getVariable().getSimpleName().equals("length")) { String targetName = fieldRead.getTarget().toString(); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), - BuiltinFunctionPredicate.length(targetName, fieldRead))); - + BuiltinFunctionPredicate.length(targetName, fieldRead))); + } else { fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE @@ -321,7 +317,7 @@ public void visitCtReturn(CtReturn ret) { public void visitCtIf(CtIf ifElement) { CtExpression exp = ifElement.getCondition(); Predicate expRefs = getExpressionRefinements(exp); - + String freshVarName = String.format(Formats.FRESH, context.getCounter()); expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName); Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); @@ -368,7 +364,8 @@ public void visitCtIf(CtIf ifElement) { public void visitCtArrayWrite(CtArrayWrite arrayWrite) { super.visitCtArrayWrite(arrayWrite); CtExpression index = arrayWrite.getIndexExpression(); - BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), index.toString(), Keys.WILDCARD, arrayWrite); + BuiltinFunctionPredicate fp = BuiltinFunctionPredicate.addToIndex(arrayWrite.getTarget().toString(), + index.toString(), Keys.WILDCARD, arrayWrite); arrayWrite.putMetadata(Keys.REFINEMENT, fp); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java index 65776246..3608f23d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -1,7 +1,5 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.lang.annotation.Annotation; import java.util.Arrays; import java.util.List; @@ -154,7 +152,8 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th } } - private void createStateGhost(String string, CtAnnotation ann, String an, CtElement element) throws LJError { + private void createStateGhost(String string, CtAnnotation ann, String an, CtElement element) + throws LJError { GhostDTO gd = RefinementsParser.getGhostDeclaration(string); if (gd.getParam_types().size() > 0) { throw new CustomError( @@ -231,7 +230,8 @@ protected void handleAlias(String value, CtElement element) throws LJError { a.parse(path); // refinement alias must return a boolean expression if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) { - throw new InvalidRefinementError(element, "Refinement alias must return a boolean expression", value); + throw new InvalidRefinementError(element, "Refinement alias must return a boolean expression", + value); } AliasWrapper aw = new AliasWrapper(a, factory, Keys.WILDCARD, context, klass, path); context.addAlias(aw); @@ -293,7 +293,8 @@ public void checkSMT(Predicate expectedType, CtElement element) throws LJError { element.putMetadata(Keys.REFINEMENT, expectedType); } - public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) throws LJError { + public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) + throws LJError { vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, moreInfo, factory); } @@ -301,7 +302,8 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); } - public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customMessage) throws LJError { + public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customMessage) + throws LJError { vcChecker.printSubtypingError(element, expectedType, foundType, customMessage); } @@ -309,7 +311,8 @@ public void createSameStateError(CtElement element, Predicate expectedType, Stri vcChecker.printSameStateError(element, expectedType, klass); } - public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) throws LJError { + public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) + throws LJError { vcChecker.printStateMismatchError(element, method, found, expected); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java index 31fd9444..5bae7e90 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java @@ -1,7 +1,5 @@ package liquidjava.processor.refinement_checker; -import static liquidjava.diagnostics.Diagnostics.diagnostics; - import java.util.ArrayList; import java.util.Arrays; import java.util.List; @@ -39,7 +37,8 @@ public VCChecker() { pathVariables = new Stack<>(); } - public void processSubtyping(Predicate expectedType, List list, CtElement element, Factory f) throws LJError { + public void processSubtyping(Predicate expectedType, List list, CtElement element, Factory f) + throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); if (expectedType.isBooleanTrue()) @@ -301,8 +300,8 @@ private TranslationTable createMap(CtElement element, Predicate expectedType) { return map; } - protected void printSubtypingError(CtElement element, Predicate expectedType, Predicate foundType, - String customMsg) throws LJError { + protected void printSubtypingError(CtElement element, Predicate expectedType, Predicate foundType, String customMsg) + throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(foundType, lrv, mainVars); @@ -333,7 +332,8 @@ private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate } } - public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) throws LJError { + public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) + throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); TranslationTable map = new TranslationTable(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 6ef27a11..69dd190e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -164,8 +164,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro * * @return String with the operation refinements */ - private Predicate getOperationRefinements(CtBinaryOperator operator, CtExpression element) - throws LJError { + private Predicate getOperationRefinements(CtBinaryOperator operator, CtExpression element) throws LJError { return getOperationRefinements(operator, null, element); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index f8faedad..6d6de6d1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -31,8 +31,7 @@ public class AuxStateHandler { * @param tc */ @SuppressWarnings({ "unchecked", "rawtypes" }) - public static void handleConstructorState(CtConstructor c, RefinedFunction f, TypeChecker tc) - throws LJError { + public static void handleConstructorState(CtConstructor c, RefinedFunction f, TypeChecker tc) throws LJError { List> an = getStateAnnotation(c); if (!an.isEmpty()) { for (CtAnnotation a : an) { @@ -67,7 +66,8 @@ private static void setConstructorStates(RefinedFunction f, List getDifferentSets(TypeChecker tc, String klassQualified) { @@ -188,12 +191,14 @@ private static ObjectState getStates(CtAnnotation ctAnnota /** * Creates the predicate for state transition + * * @param value * @param targetClass * @param tc * @param e * @param isTo * @param prefix + * * @return the created predicate */ private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass, @@ -221,9 +226,11 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f /** * Gets the missing states in the predicate and adds equalities to old states + * * @param t * @param tc * @param p + * * @return the updated predicate */ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) { @@ -241,8 +248,10 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) /** * Collect ghost states for the given qualified class name and its immediate supertypes (superclass and interfaces) + * * @param qualifiedClass * @param tc + * * @return list of ghost states */ private static List getGhostStatesFor(String qualifiedClass, TypeChecker tc) { @@ -271,8 +280,9 @@ private static List getGhostStatesFor(String qualifiedClass, TypeChe } /** - * Create predicate with the equalities with previous versions of the object - * e.g., ghostfunction1(this) == ghostfunction1(old(this)) + * Create predicate with the equalities with previous versions of the object e.g., ghostfunction1(this) == + * ghostfunction1(old(this)) + * * @param p * @param th * @param sets @@ -362,6 +372,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre /** * Updates the ghost field after a write + * * @param fw * @param tc */ @@ -399,12 +410,10 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L ObjectState stateChange = new ObjectState(); String prefix = field.getDeclaringType().getQualifiedName(); - Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, - prefix); + Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, prefix); Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix); stateChange.setFrom(fromPredicate); stateChange.setTo(toPredicate); - // replace "state(this)" to "state(whatever method is called from) and so on" Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java index 8be9c387..2fd8e89f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java @@ -28,6 +28,7 @@ public static Expression createAST(String toParse, String prefix) throws LJError /** * The triple information of the ghost declaration in the order > + * * @param s */ public static GhostDTO getGhostDeclaration(String s) throws LJError { diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index b7f6d218..f0822bef 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -1,6 +1,5 @@ package liquidjava.api.tests; -import static liquidjava.diagnostics.Diagnostics.diagnostics; import static org.junit.Assert.fail; import java.io.IOException; @@ -9,6 +8,7 @@ import java.nio.file.Paths; import java.util.stream.Stream; import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; import org.junit.Test; import org.junit.jupiter.params.ParameterizedTest; @@ -16,6 +16,8 @@ public class TestExamples { + Diagnostics diagnostics = Diagnostics.getInstance(); + /** * Test the file at the given path by launching the verifier and checking for errors. The file/directory is expected * to be either correct or contain an error based on its name. From fdc1b61768b2b47e0eb6516269ca287beae15377 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 11:39:11 +0000 Subject: [PATCH 08/16] Fix --- .../main/java/liquidjava/processor/RefinementProcessor.java | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index 99d14e49..aa74251c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -32,16 +32,14 @@ public void process(CtPackage pkg) { Context c = Context.getInstance(); c.reinitializeAllContext(); - // we need to catch errors here try { pkg.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts pkg.accept(new ExternalRefinementTypeChecker(c, factory)); pkg.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers) + pkg.accept(new RefinementTypeChecker(c, factory)); } catch (LJError e) { diagnostics.add(e); } - // here we catch the errors in the visitors - pkg.accept(new RefinementTypeChecker(c, factory)); } } } From ab155638cca403cb650d7a2be0c595934b95386c Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 12:29:34 +0000 Subject: [PATCH 09/16] Fix Errors in Multiple Files Errors thrown stopped package traversal, so we need to catch them earlier to continue processing files in the same package. --- .../MethodsFirstChecker.java | 23 ++++++++++++++----- 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index bff427ec..ed2cbdc1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -3,6 +3,8 @@ import java.util.ArrayList; import java.util.List; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.Context; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import spoon.reflect.declaration.CtClass; @@ -17,6 +19,7 @@ public class MethodsFirstChecker extends TypeChecker { MethodsFunctionsChecker mfc; List visitedClasses; + Diagnostics diagnostics = Diagnostics.getInstance(); public MethodsFirstChecker(Context context, Factory factory) { super(context, factory); @@ -47,9 +50,13 @@ public void visitCtClass(CtClass ctClass) { if (ct instanceof CtClass) visitCtClass((CtClass) ct); } - getRefinementFromAnnotation(ctClass); - handleStateSetsFromAnnotation(ctClass); - super.visitCtClass(ctClass); + try { + getRefinementFromAnnotation(ctClass); + handleStateSetsFromAnnotation(ctClass); + super.visitCtClass(ctClass); + } catch (LJError e) { + diagnostics.add(e); + } } @Override @@ -61,9 +68,13 @@ public void visitCtInterface(CtInterface intrface) { if (getExternalRefinement(intrface).isPresent()) return; - getRefinementFromAnnotation(intrface); - handleStateSetsFromAnnotation(intrface); - super.visitCtInterface(intrface); + try { + getRefinementFromAnnotation(intrface); + handleStateSetsFromAnnotation(intrface); + super.visitCtInterface(intrface); + } catch (LJError e) { + diagnostics.add(e); + } } @Override From b2720df4764326d2f26cc56dd844f276f3ae9bf3 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 12:47:16 +0000 Subject: [PATCH 10/16] Separate Try-Catches in Class and Interface Visitors Wrap class annotation processing and child element visiting in separate try-catches so errors in one element don't prevent processing of sibling elements. --- .../refinement_checker/MethodsFirstChecker.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index ed2cbdc1..6a148725 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -50,9 +50,17 @@ public void visitCtClass(CtClass ctClass) { if (ct instanceof CtClass) visitCtClass((CtClass) ct); } + // first try-catch: process class-level annotations) + // errors here should not prevent visiting methods, constructors or fields of the class try { getRefinementFromAnnotation(ctClass); handleStateSetsFromAnnotation(ctClass); + } catch (LJError e) { + diagnostics.add(e); + } + // second try-catch: visit class children (methods, constructors, fields) + // errors from one child should not prevent visiting sibling elements + try { super.visitCtClass(ctClass); } catch (LJError e) { diagnostics.add(e); @@ -68,9 +76,17 @@ public void visitCtInterface(CtInterface intrface) { if (getExternalRefinement(intrface).isPresent()) return; + // first try-catch: process interface-level annotations + // errors here should not prevent visiting the interface's methods try { getRefinementFromAnnotation(intrface); handleStateSetsFromAnnotation(intrface); + } catch (LJError e) { + diagnostics.add(e); + } + // second try-catch: visit interface children (methods) + // errors from one child should not prevent visiting sibling methods + try { super.visitCtInterface(intrface); } catch (LJError e) { diagnostics.add(e); From 98568cb5dabc553b6246a80beff562211ac4da80 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 15:55:58 +0000 Subject: [PATCH 11/16] Minor Change --- .../src/main/java/liquidjava/api/CommandLineLauncher.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index ccf56c6a..bde73ab1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -38,6 +38,7 @@ public static void launch(String... paths) { System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", "")); Diagnostics diagnostics = Diagnostics.getInstance(); + diagnostics.clear(); Launcher launcher = new Launcher(); for (String path : paths) { if (!new File(path).exists()) { @@ -50,7 +51,6 @@ public static void launch(String... paths) { launcher.getEnvironment().setNoClasspath(true); launcher.getEnvironment().setComplianceLevel(8); launcher.run(); - diagnostics.clear(); final Factory factory = launcher.getFactory(); final ProcessingManager processingManager = new QueueProcessingManager(factory); From 9fbef6b05c3480412a1d164be724ba20dc46729b Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 16:01:39 +0000 Subject: [PATCH 12/16] Minor Changes --- .../src/main/java/liquidjava/api/CommandLineLauncher.java | 5 +++-- .../src/main/java/liquidjava/diagnostics/LJDiagnostic.java | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index bde73ab1..cd3486ff 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -14,6 +14,9 @@ import spoon.support.QueueProcessingManager; public class CommandLineLauncher { + + private static final Diagnostics diagnostics = Diagnostics.getInstance(); + public static void main(String[] args) { if (args.length == 0) { System.out.println("No input paths provided"); @@ -25,7 +28,6 @@ public static void main(String[] args) { } List paths = Arrays.asList(args); launch(paths.toArray(new String[0])); - Diagnostics diagnostics = Diagnostics.getInstance(); if (diagnostics.foundError()) { System.out.println(diagnostics.getErrorOutput()); } else { @@ -37,7 +39,6 @@ public static void main(String[] args) { public static void launch(String... paths) { System.out.println("Running LiquidJava on: " + Arrays.toString(paths).replaceAll("[\\[\\]]", "")); - Diagnostics diagnostics = Diagnostics.getInstance(); diagnostics.clear(); Launcher launcher = new Launcher(); for (String path : paths) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index b7c43ee1..965916c9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -49,7 +49,7 @@ public String toString() { StringBuilder sb = new StringBuilder(); // title - sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message) + sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message.toLowerCase()) .append("\n"); // snippet From 999eb53c1d9c4c720773e0f84b79ba520cb3ca51 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 16:48:23 +0000 Subject: [PATCH 13/16] Add Multiple Errors Test --- .../testMultiple/MultipleErrorsExample.java | 19 ++++++++ .../errors/CustomError.java | 2 +- .../errors/GhostInvocationError.java | 2 +- .../IllegalConstructorTransitionError.java | 2 +- .../errors/InvalidRefinementError.java | 2 +- .../errors/NotFoundError.java | 2 +- .../errors/RefinementError.java | 2 +- .../errors/StateConflictError.java | 2 +- .../errors/StateRefinementError.java | 2 +- .../errors/SyntaxError.java | 2 +- .../warnings/NonExistentClass.java | 2 +- .../warnings/NonExistentConstructor.java | 2 +- .../warnings/NonExistentMethod.java | 2 +- .../liquidjava/diagnostics/LJDiagnostic.java | 4 +- .../liquidjava/api/tests/TestMultiple.java | 45 +++++++++++++++++++ 15 files changed, 78 insertions(+), 14 deletions(-) create mode 100644 liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/CustomError.java (70%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/GhostInvocationError.java (82%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/IllegalConstructorTransitionError.java (86%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/InvalidRefinementError.java (80%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/NotFoundError.java (79%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/RefinementError.java (80%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/StateConflictError.java (87%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/StateRefinementError.java (91%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/errors/SyntaxError.java (79%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/warnings/NonExistentClass.java (78%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/warnings/NonExistentConstructor.java (91%) rename liquidjava-example/src/main/java/{testingInProgress/diagnostics => testMultiple}/warnings/NonExistentMethod.java (90%) create mode 100644 liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java diff --git a/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java b/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java new file mode 100644 index 00000000..48005140 --- /dev/null +++ b/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java @@ -0,0 +1,19 @@ +package testMultiple; + +import liquidjava.specification.Refinement; + +class MultipleErrorsExample { + + void test1() { + @Refinement("a > 0") + int a = -1; + } + + void test2() { + @Refinement("b > 0") + int b = -2; + + @Refinement("c > 0") + int c = 3; + } +} diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java b/liquidjava-example/src/main/java/testMultiple/errors/CustomError.java similarity index 70% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java rename to liquidjava-example/src/main/java/testMultiple/errors/CustomError.java index 953c56ef..7505005d 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/CustomError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/CustomError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.StateSet; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java b/liquidjava-example/src/main/java/testMultiple/errors/GhostInvocationError.java similarity index 82% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java rename to liquidjava-example/src/main/java/testMultiple/errors/GhostInvocationError.java index db4bcd57..831c6ca5 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/GhostInvocationError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.Ghost; import liquidjava.specification.StateRefinement; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java b/liquidjava-example/src/main/java/testMultiple/errors/IllegalConstructorTransitionError.java similarity index 86% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java rename to liquidjava-example/src/main/java/testMultiple/errors/IllegalConstructorTransitionError.java index dcfacf93..01134b29 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/IllegalConstructorTransitionError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/IllegalConstructorTransitionError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java b/liquidjava-example/src/main/java/testMultiple/errors/InvalidRefinementError.java similarity index 80% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java rename to liquidjava-example/src/main/java/testMultiple/errors/InvalidRefinementError.java index 92ed8dbd..e81cfdff 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/InvalidRefinementError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java b/liquidjava-example/src/main/java/testMultiple/errors/NotFoundError.java similarity index 79% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java rename to liquidjava-example/src/main/java/testMultiple/errors/NotFoundError.java index ff22cc9b..df3b7d93 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/NotFoundError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/NotFoundError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java b/liquidjava-example/src/main/java/testMultiple/errors/RefinementError.java similarity index 80% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java rename to liquidjava-example/src/main/java/testMultiple/errors/RefinementError.java index 25dac068..b6ab1682 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/RefinementError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/RefinementError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java b/liquidjava-example/src/main/java/testMultiple/errors/StateConflictError.java similarity index 87% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java rename to liquidjava-example/src/main/java/testMultiple/errors/StateConflictError.java index 9701ff05..66b8b9ae 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateConflictError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/StateConflictError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java b/liquidjava-example/src/main/java/testMultiple/errors/StateRefinementError.java similarity index 91% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java rename to liquidjava-example/src/main/java/testMultiple/errors/StateRefinementError.java index 6e4aa8fb..1187de24 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/StateRefinementError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/StateRefinementError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.StateRefinement; import liquidjava.specification.StateSet; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/SyntaxError.java b/liquidjava-example/src/main/java/testMultiple/errors/SyntaxError.java similarity index 79% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/SyntaxError.java rename to liquidjava-example/src/main/java/testMultiple/errors/SyntaxError.java index 87953608..082d25b8 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/errors/SyntaxError.java +++ b/liquidjava-example/src/main/java/testMultiple/errors/SyntaxError.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.errors; +package testMultiple.errors; import liquidjava.specification.Refinement; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentClass.java b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentClass.java similarity index 78% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentClass.java rename to liquidjava-example/src/main/java/testMultiple/warnings/NonExistentClass.java index f4eb3ebe..c1506822 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentClass.java +++ b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentClass.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.warnings; +package testMultiple.warnings; import liquidjava.specification.ExternalRefinementsFor; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentConstructor.java b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java similarity index 91% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentConstructor.java rename to liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java index c4a5f4d5..eae37e3c 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentConstructor.java +++ b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentConstructor.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.warnings; +package testMultiple.warnings; import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.RefinementPredicate; diff --git a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentMethod.java b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java similarity index 90% rename from liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentMethod.java rename to liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java index af7237f1..9d3d16e6 100644 --- a/liquidjava-example/src/main/java/testingInProgress/diagnostics/warnings/NonExistentMethod.java +++ b/liquidjava-example/src/main/java/testMultiple/warnings/NonExistentMethod.java @@ -1,4 +1,4 @@ -package testingInProgress.diagnostics.warnings; +package testMultiple.warnings; import liquidjava.specification.ExternalRefinementsFor; import liquidjava.specification.RefinementPredicate; diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 965916c9..9beaccfa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -49,8 +49,8 @@ public String toString() { StringBuilder sb = new StringBuilder(); // title - sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET).append(message.toLowerCase()) - .append("\n"); + sb.append("\n").append(accentColor).append(title).append(": ").append(Colors.RESET) + .append(message.toLowerCase()).append("\n"); // snippet String snippet = getSnippet(); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java new file mode 100644 index 00000000..6e28cc67 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java @@ -0,0 +1,45 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; + +public class TestMultiple { + + @Test + public void testMultipleErrorDirectory() { + String path = "../liquidjava-example/src/main/java/testMultiple/errors"; + CommandLineLauncher.launch(path); + Diagnostics diagnostics = Diagnostics.getInstance(); + assertEquals(9, diagnostics.getErrors().size()); + } + + @Test + public void testMultipleWarningDirectory() { + String path = "../liquidjava-example/src/main/java/testMultiple/warnings"; + CommandLineLauncher.launch(path); + Diagnostics diagnostics = Diagnostics.getInstance(); + assertEquals(3, diagnostics.getWarnings().size()); + } + + @Test + public void testMultipleErrorsSameFile() { + String path = "../liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java"; + CommandLineLauncher.launch(path); + Diagnostics diagnostics = Diagnostics.getInstance(); + assertEquals(2, diagnostics.getErrors().size()); + } + + @Test + public void testMultipleDirectory() { + String path = "../liquidjava-example/src/main/java/testMultiple"; + CommandLineLauncher.launch(path); + Diagnostics diagnostics = Diagnostics.getInstance(); + + assertEquals(11, diagnostics.getErrors().size()); + assertEquals(3, diagnostics.getWarnings().size()); + } +} \ No newline at end of file From 3d8b2dcdcb028b154fcc9382558afc785f2018fe Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 17:08:42 +0000 Subject: [PATCH 14/16] Fix Duplicate Visitor Passes (Claude) Changed from `pkg.accept()` to `pkg.getTypes().forEach()` in `RefinementProcessor` to prevent types in nested packages from being verified multiple times when `ProcessingManager` traverses the package hierarchy. --- .../java/liquidjava/api/CommandLineLauncher.java | 2 +- .../processor/RefinementProcessor.java | 16 ++++++++++++---- 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index cd3486ff..69814608 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -16,7 +16,7 @@ public class CommandLineLauncher { private static final Diagnostics diagnostics = Diagnostics.getInstance(); - + public static void main(String[] args) { if (args.length == 0) { System.out.println("No input paths provided"); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index aa74251c..ba8d268a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -33,10 +33,18 @@ public void process(CtPackage pkg) { c.reinitializeAllContext(); try { - pkg.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts - pkg.accept(new ExternalRefinementTypeChecker(c, factory)); - pkg.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers) - pkg.accept(new RefinementTypeChecker(c, factory)); + // process types in this package only, not sub-packages + // first pass: gather refinements + pkg.getTypes().forEach(type -> { + type.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts + type.accept(new ExternalRefinementTypeChecker(c, factory)); // process external refinements + type.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers) + }); + + // second pass: check refinements + pkg.getTypes().forEach(type -> { + type.accept(new RefinementTypeChecker(c, factory)); + }); } catch (LJError e) { diagnostics.add(e); } From 7b0ff3bfb9abf010cbf0f92d85ab80d661740e6f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 21:46:25 +0000 Subject: [PATCH 15/16] Always Print Warnings --- liquidjava-verifier/pom.xml | 2 +- .../src/main/java/liquidjava/api/CommandLineLauncher.java | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index e9727bff..5edca456 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.1 + 0.0.2 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 69814608..08162fe8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -28,10 +28,12 @@ public static void main(String[] args) { } List paths = Arrays.asList(args); launch(paths.toArray(new String[0])); + + // print diagnostics + System.out.println(diagnostics.getWarningOutput()); if (diagnostics.foundError()) { System.out.println(diagnostics.getErrorOutput()); } else { - System.out.println(diagnostics.getWarningOutput()); System.out.println("Correct! Passed Verification."); } } From 85527143a5b9e7cc6453b9a5e1783d8c97f1aaa3 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 15 Nov 2025 23:38:56 +0000 Subject: [PATCH 16/16] Update Test --- .../src/main/java/testMultiple/MultipleErrorsExample.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java b/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java index 48005140..a46cde56 100644 --- a/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java +++ b/liquidjava-example/src/main/java/testMultiple/MultipleErrorsExample.java @@ -14,6 +14,6 @@ void test2() { int b = -2; @Refinement("c > 0") - int c = 3; + int c = -3; } }