From 8f2142f84db5a9abc112dbdb5748d0b941eca7a2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 15:56:27 +0000 Subject: [PATCH 1/4] Code Refactoring --- .../liquidjava/diagnostics/ErrorHandler.java | 15 +- .../liquidjava/diagnostics/LJDiagnostics.java | 24 +++ .../diagnostics/errors/RefinementError.java | 2 +- .../errors/StateConflictError.java | 2 +- .../RefinementTypeChecker.java | 70 ++++---- .../refinement_checker/TypeChecker.java | 44 ++--- .../refinement_checker/VCChecker.java | 61 ++++--- .../MethodsFunctionsChecker.java | 60 +++---- .../general_checkers/OperationsChecker.java | 156 +++++++----------- .../AuxHierarchyRefinememtsPassage.java | 20 ++- .../object_checkers/AuxStateHandler.java | 95 +++++------ .../liquidjava/rj_language/Predicate.java | 35 ++-- .../rj_language/ast/BinaryExpression.java | 16 +- .../liquidjava/smt/TranslatorContextToZ3.java | 60 +++---- .../java/liquidjava/smt/TranslatorToZ3.java | 1 + .../src/main/java/liquidjava/utils/Utils.java | 59 ++----- .../liquidjava/utils/constants/Formats.java | 8 + .../java/liquidjava/utils/constants/Keys.java | 9 + .../java/liquidjava/utils/constants/Ops.java | 17 ++ .../liquidjava/utils/constants/Patterns.java | 8 + .../liquidjava/utils/constants/Types.java | 15 ++ 21 files changed, 368 insertions(+), 409 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/constants/Ops.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/constants/Patterns.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/utils/constants/Types.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java index af45af24..39452f90 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorHandler.java @@ -3,6 +3,7 @@ import java.util.Formatter; import java.util.HashMap; import java.util.Locale; + import liquidjava.processor.VCImplication; import liquidjava.processor.context.PlacementInCode; import liquidjava.rj_language.Predicate; @@ -11,20 +12,6 @@ public class ErrorHandler { - /** - * Prints the error message - * - * @param - * @param var - * @param s - * @param expectedType - * @param cSMT - */ - public static void printError(CtElement var, Predicate expectedType, Predicate cSMT, - HashMap map, ErrorEmitter ee) { - printError(var, null, expectedType, cSMT, map, ee); - } - public static void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT, HashMap map, ErrorEmitter ee) { String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" + diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java index 624ffe65..02a6d315 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostics.java @@ -7,6 +7,12 @@ import liquidjava.diagnostics.warnings.LJWarning; import liquidjava.processor.context.PlacementInCode; +/** + * Singleton class to store diagnostics information (errors, warnings, translation map) during the verification process + * + * @see LJError + * @see LJWarning + */ public class LJDiagnostics { private static LJDiagnostics instance; @@ -26,6 +32,24 @@ public static LJDiagnostics getInstance() { return instance; } + public static LJDiagnostics add(LJError error) { + LJDiagnostics instance = getInstance(); + instance.addError(error); + return instance; + } + + public static LJDiagnostics add(LJWarning warning) { + LJDiagnostics instance = getInstance(); + instance.addWarning(warning); + return instance; + } + + public static LJDiagnostics add(HashMap map) { + LJDiagnostics instance = getInstance(); + instance.setTranslationMap(map); + return instance; + } + public void addError(LJError error) { this.errors.add(error); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java index 051e5d95..fc4b31f1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -16,7 +16,7 @@ public class RefinementError extends LJError { private ValDerivationNode found; public RefinementError(CtElement element, Predicate expected, ValDerivationNode found) { - super("Refinement Error", "Predicate refinement violation", element); + super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected), element); this.expected = expected; this.found = found; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index 0a9ec435..23ac0812 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -14,7 +14,7 @@ public class StateConflictError extends LJError { private String className; public StateConflictError(CtElement element, Predicate predicate, String className) { - super("State Conflict Error", "Found multiple disjoint states from a StateSet in refinement", element); + super("State Conflict Error", "Found multiple disjoint states in state transition", element); this.predicate = predicate; this.className = className; } 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 ef6f2c55..ae3b77f4 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 @@ -13,7 +13,9 @@ import liquidjava.rj_language.BuiltinFunctionPredicate; 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; +import liquidjava.utils.constants.Types; import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.CtArrayRead; @@ -172,9 +174,9 @@ public void visitCtNewArray(CtNewArray newArray) { } catch (ParsingException e) { return; // error already in ErrorEmitter } - String name = String.format(freshFormat, context.getCounter()); - if (c.getVariableNames().contains(WILD_VAR)) { - c = c.substituteVariable(WILD_VAR, name); + String name = String.format(Formats.RET, context.getCounter()); + if (c.getVariableNames().contains(Keys.WILDCARD)) { + c = c.substituteVariable(Keys.WILDCARD, name); } else { c = Predicate.createEquals(Predicate.createVar(name), c); } @@ -182,12 +184,12 @@ public void visitCtNewArray(CtNewArray newArray) { Predicate ep; try { ep = Predicate.createEquals( - BuiltinFunctionPredicate.builtin_length(WILD_VAR, newArray, getErrorEmitter()), + BuiltinFunctionPredicate.builtin_length(Keys.WILDCARD, newArray, getErrorEmitter()), Predicate.createVar(name)); } catch (ParsingException e) { return; // error already in ErrorEmitter } - newArray.putMetadata(REFINE_KEY, ep); + newArray.putMetadata(Keys.REFINEMENT, ep); } } @@ -201,9 +203,9 @@ public void visitCtThisAccess(CtThisAccess thisAccess) { CtClass c = thisAccess.getParent(CtClass.class); String s = c.getSimpleName(); if (thisAccess.getParent() instanceof CtReturn) { - String thisName = String.format(thisFormat, s); - thisAccess.putMetadata(REFINE_KEY, - Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName))); + String thisName = String.format(Formats.THIS, s); + thisAccess.putMetadata(Keys.REFINEMENT, + Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); } } @@ -227,7 +229,7 @@ public void visitCtAssignment(CtAssignment assignment) { CtFieldWrite fw = ((CtFieldWrite) ex); CtFieldReference cr = fw.getVariable(); CtField f = fw.getVariable().getDeclaration(); - String updatedVarName = String.format(thisFormat, cr.getSimpleName()); + String updatedVarName = String.format(Formats.THIS, cr.getSimpleName()); checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f); // corresponding ghost function update @@ -249,9 +251,9 @@ public void visitCtArrayRead(CtArrayRead arrayRead) { } super.visitCtArrayRead(arrayRead); - String name = String.format(instanceFormat, "arrayAccess", context.getCounter()); + String name = String.format(Formats.INSTANCE, "arrayAccess", context.getCounter()); context.addVarToContext(name, arrayRead.getType(), new Predicate(), arrayRead); - arrayRead.putMetadata(REFINE_KEY, Predicate.createVar(name)); + arrayRead.putMetadata(Keys.REFINEMENT, Predicate.createVar(name)); // TODO predicate for now is always TRUE } @@ -261,15 +263,15 @@ public void visitCtLiteral(CtLiteral lit) { return; } - List types = Arrays.asList(implementedTypes); + List types = Arrays.asList(Types.IMPLEMENTED); String type = lit.getType().getQualifiedName(); if (types.contains(type)) { - lit.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR), + lit.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createLit(lit.getValue().toString(), type))); } else if (lit.getType().getQualifiedName().equals("java.lang.String")) { // Only taking care of strings inside refinements - } else if (type.equals(Utils.NULL_TYPE)) { + } else if (type.equals(Types.NULL)) { // Skip null literals } else { throw new NotImplementedException( @@ -293,10 +295,10 @@ public void visitCtField(CtField f) { // context.addVarToContext(f.getSimpleName(), f.getType(), // c.map( i -> i.substituteVariable(WILD_VAR, f.getSimpleName()).orElse(new // Predicate()) ); - String nname = String.format(thisFormat, f.getSimpleName()); + String nname = String.format(Formats.THIS, f.getSimpleName()); Predicate ret = new Predicate(); if (c.isPresent()) { - ret = c.get().substituteVariable(WILD_VAR, nname).substituteVariable(f.getSimpleName(), nname); + ret = c.get().substituteVariable(Keys.WILDCARD, nname).substituteVariable(f.getSimpleName(), nname); } RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, f); if (v instanceof Variable) { @@ -315,27 +317,27 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { RefinedVariable rv = context.getVariableByName(fieldName); if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent() && ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) { - fieldRead.putMetadata(REFINE_KEY, context.getVariableRefinements(fieldName)); + fieldRead.putMetadata(Keys.REFINEMENT, context.getVariableRefinements(fieldName)); } else { - fieldRead.putMetadata(REFINE_KEY, - Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(fieldName))); + fieldRead.putMetadata(Keys.REFINEMENT, + Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName))); } - } else if (context.hasVariable(String.format(thisFormat, fieldName))) { - String thisName = String.format(thisFormat, fieldName); - fieldRead.putMetadata(REFINE_KEY, - Predicate.createEquals(Predicate.createVar(WILD_VAR), 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(); try { - fieldRead.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR), + fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), BuiltinFunctionPredicate.builtin_length(targetName, fieldRead, getErrorEmitter()))); } catch (ParsingException e) { return; // error already in ErrorEmitter } } else { - fieldRead.putMetadata(REFINE_KEY, new Predicate()); + fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE } @@ -417,8 +419,8 @@ public void visitCtIf(CtIf ifElement) { } catch (ParsingException e) { return; // error already in ErrorEmitter } - String freshVarName = String.format(freshFormat, context.getCounter()); - expRefs = expRefs.substituteVariable(WILD_VAR, freshVarName); + String freshVarName = String.format(Formats.FRESH, context.getCounter()); + expRefs = expRefs.substituteVariable(Keys.WILDCARD, freshVarName); Predicate lastExpRefs = substituteAllVariablesForLastInstance(expRefs); expRefs = Predicate.createConjunction(expRefs, lastExpRefs); @@ -470,11 +472,11 @@ public void visitCtArrayWrite(CtArrayWrite arrayWrite) { BuiltinFunctionPredicate fp; try { fp = BuiltinFunctionPredicate.builtin_addToIndex(arrayWrite.getTarget().toString(), index.toString(), - WILD_VAR, arrayWrite, getErrorEmitter()); + Keys.WILDCARD, arrayWrite, getErrorEmitter()); } catch (ParsingException e) { return; // error already in ErrorEmitter } - arrayWrite.putMetadata(REFINE_KEY, fp); + arrayWrite.putMetadata(Keys.REFINEMENT, fp); } @Override @@ -487,7 +489,7 @@ public void visitCtConditional(CtConditional conditional) { Predicate cond = getRefinement(conditional.getCondition()); Predicate c = Predicate.createITE(cond, getRefinement(conditional.getThenExpression()), getRefinement(conditional.getElseExpression())); - conditional.putMetadata(REFINE_KEY, c); + conditional.putMetadata(Keys.REFINEMENT, c); } @Override @@ -582,12 +584,12 @@ private Predicate substituteAllVariablesForLastInstance(Predicate c) { * Cannot be null */ private void getPutVariableMetadada(CtElement elem, String name) { - Predicate cref = Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(name)); + Predicate cref = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(name)); Optional ovi = context.getLastVariableInstance(name); if (ovi.isPresent()) { - cref = Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(ovi.get().getName())); + cref = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(ovi.get().getName())); } - elem.putMetadata(REFINE_KEY, cref); + elem.putMetadata(Keys.REFINEMENT, cref); } } 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 159195c8..375bff40 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 @@ -17,7 +17,9 @@ 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; +import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Types; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtLiteral; import spoon.reflect.code.CtNewArray; @@ -31,16 +33,6 @@ import spoon.reflect.visitor.CtScanner; public abstract class TypeChecker extends CtScanner { - public final String REFINE_KEY = "refinement"; - public final String TARGET_KEY = "target"; - // public final String STATE_KEY = "state"; - public final String THIS = "this"; - public final String WILD_VAR = "_"; - public final String freshFormat = "#fresh_%d"; - public final String instanceFormat = "#%s_%d"; - public final String thisFormat = "this#%s"; - public String[] implementedTypes = { "boolean", "int", "short", "long", "float", "double" }; // TODO add - // types e.g., "int[]" Context context; Factory factory; @@ -63,7 +55,7 @@ public Factory getFactory() { } public Predicate getRefinement(CtElement elem) { - Predicate c = (Predicate) elem.getMetadata(REFINE_KEY); + Predicate c = (Predicate) elem.getMetadata(Keys.REFINEMENT); return c == null ? new Predicate() : c; } @@ -142,7 +134,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { context.addGhostClass(g.getParentClassName()); List> ls = e.getElements(); - Predicate ip = Predicate.createInvocation(g.getName(), Predicate.createVar(THIS)); + Predicate ip = Predicate.createInvocation(g.getName(), Predicate.createVar(Keys.WILDCARD)); int order = 0; for (CtExpression ce : ls) { if (ce instanceof CtLiteral) { @@ -154,7 +146,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { gs.setGhostParent(g); gs.setRefinement( /* new OperationPredicate(new InvocationPredicate(f, THIS), "<-->", */ - Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Utils.INT))); // open(THIS) + Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); // open(THIS) // -> // state1(THIS) // == 1 @@ -258,7 +250,7 @@ protected void handleAlias(String value, CtElement element) { errorEmitter); return; } - AliasWrapper aw = new AliasWrapper(a, factory, WILD_VAR, context, klass, path); + AliasWrapper aw = new AliasWrapper(a, factory, Keys.WILDCARD, context, klass, path); context.addAlias(aw); } } catch (ParsingException e) { @@ -295,12 +287,12 @@ else if (expectedType.isPresent()) else cEt = new Predicate(); - cEt = cEt.substituteVariable(WILD_VAR, simpleName); - Predicate cet = cEt.substituteVariable(WILD_VAR, simpleName); + cEt = cEt.substituteVariable(Keys.WILDCARD, simpleName); + Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName); - String newName = String.format(instanceFormat, simpleName, context.getCounter()); - Predicate correctNewRefinement = refinementFound.substituteVariable(WILD_VAR, newName); - correctNewRefinement = correctNewRefinement.substituteVariable(THIS, newName); + String newName = String.format(Formats.INSTANCE, simpleName, context.getCounter()); + Predicate correctNewRefinement = refinementFound.substituteVariable(Keys.WILDCARD, newName); + correctNewRefinement = correctNewRefinement.substituteVariable(Keys.THIS, newName); cEt = cEt.substituteVariable(simpleName, newName); // Substitute variable in verification @@ -314,18 +306,16 @@ else if (expectedType.isPresent()) } public void checkSMT(Predicate expectedType, CtElement element) { - vcChecker.processSubtyping(expectedType, context.getGhostState(), WILD_VAR, THIS, element, factory); - element.putMetadata(REFINE_KEY, expectedType); + vcChecker.processSubtyping(expectedType, context.getGhostState(), element, factory); + element.putMetadata(Keys.REFINEMENT, expectedType); } - public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String string) { - vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, target, string, - factory); + public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) { + vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, moreInfo, factory); } public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) { - return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, p, - factory); + return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory); } public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customeMessage) { 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 fcded1ce..b23200a9 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 @@ -6,7 +6,6 @@ import java.util.Set; import java.util.Stack; import java.util.function.Consumer; -import java.util.regex.Pattern; import java.util.stream.Collectors; import liquidjava.diagnostics.ErrorEmitter; @@ -19,6 +18,7 @@ import liquidjava.smt.SMTEvaluator; import liquidjava.smt.TypeCheckError; import liquidjava.smt.TypeMismatchError; +import liquidjava.utils.constants.Keys; import spoon.reflect.code.CtInvocation; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; @@ -29,8 +29,6 @@ public class VCChecker { private final Context context; private final List pathVariables; private final ErrorEmitter errorEmitter; - Pattern thisPattern = Pattern.compile("#this_\\d+"); - Pattern instancePattern = Pattern.compile("^#(.+)_[0-9]+$"); public VCChecker(ErrorEmitter errorEmitter) { context = Context.getInstance(); @@ -38,15 +36,14 @@ public VCChecker(ErrorEmitter errorEmitter) { this.errorEmitter = errorEmitter; } - public void processSubtyping(Predicate expectedType, List list, String wild_var, String this_var, - CtElement element, Factory f) { + public void processSubtyping(Predicate expectedType, List list, CtElement element, Factory f) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); if (expectedType.isBooleanTrue()) return; HashMap map = new HashMap<>(); - String[] s = { wild_var, this_var }; + String[] s = { Keys.WILDCARD, Keys.THIS }; Predicate premisesBeforeChange = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); Predicate premises = new Predicate(); Predicate et = new Predicate(); @@ -56,8 +53,8 @@ public void processSubtyping(Predicate expectedType, List list, Stri .changeAliasToRefinement(context, f); et = expectedType.changeStatesToRefinements(filtered, s, errorEmitter).changeAliasToRefinement(context, f); - } catch (Exception e1) { - printError(premises, expectedType, element, map, e1.getMessage()); + } catch (Exception e) { + ErrorHandler.printError(element, e.getMessage(), expectedType, premises, map, errorEmitter); return; } @@ -69,15 +66,15 @@ public void processSubtyping(Predicate expectedType, List list, Stri } } - public void processSubtyping(Predicate type, Predicate expectedType, List list, String wild_var, - String this_var, CtElement element, String string, Factory f) { - boolean b = canProcessSubtyping(type, expectedType, list, wild_var, this_var, element.getPosition(), f); + public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, + String string, Factory f) { + 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, String wild_var, - String this_var, SourcePosition p, Factory f) { + public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List list, SourcePosition p, + Factory f) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); @@ -86,7 +83,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< // Predicate premises = joinPredicates(type, element, mainVars, lrv); HashMap map = new HashMap<>(); - String[] s = { wild_var, this_var }; + String[] s = { Keys.WILDCARD, Keys.THIS }; Predicate premises = new Predicate(); Predicate et = new Predicate(); @@ -289,11 +286,10 @@ private void smtChecking(Predicate cSMT, Predicate expectedType) * * @return */ - @SuppressWarnings("unused") - private Predicate substituteByMap(Predicate c, HashMap map) { - map.keySet().forEach(s -> c.substituteVariable(s, map.get(s))); - return c; - } + // private Predicate substituteByMap(Predicate c, HashMap map) { + // map.keySet().forEach(s -> c.substituteVariable(s, map.get(s))); + // return c; + // } public void addPathVariable(RefinedVariable rv) { pathVariables.add(rv); @@ -308,12 +304,12 @@ void removePathVariableThatIncludes(String otherVar) { .collect(Collectors.toList()).forEach(pathVariables::remove); } - private void printVCs(String string, String stringSMT, Predicate expectedType) { - System.out.println("\n----------------------------VC--------------------------------\n"); - System.out.println(string); - System.out.println("\nSMT subtyping:" + stringSMT + " <: " + expectedType.toString()); - System.out.println("--------------------------------------------------------------"); - } + // private void printVCs(String string, String stringSMT, Predicate expectedType) { + // System.out.println("\n----------------------------VC--------------------------------\n"); + // System.out.println(string); + // System.out.println("\nSMT subtyping:" + stringSMT + " <: " + expectedType.toString()); + // System.out.println("--------------------------------------------------------------"); + // } // Print // Errors--------------------------------------------------------------------------------------------------- @@ -333,7 +329,8 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr gatherVariables(foundType, lrv, mainVars); HashMap map = new HashMap<>(); Predicate premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - printError(premises, expectedType, element, map, customeMsg); + + ErrorHandler.printError(element, customeMsg, expectedType, premises, map, errorEmitter); } public void printSameStateError(CtElement element, Predicate expectedType, String klass) { @@ -372,12 +369,12 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e } } - private void printError(Predicate premises, Predicate expectedType, CtElement element, - HashMap map, String s) { - Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map); - Predicate cSMTMessageReady = premises; // substituteByMap(premises, map); - ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); - } + // private void printError(Predicate premises, Predicate expectedType, CtElement element, + // HashMap map, String s) { + // Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map); + // Predicate cSMTMessageReady = premises; // substituteByMap(premises, map); + // ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); + // } public void printStateMismatchError(CtElement element, String method, Predicate c, String states) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); 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 4c35c931..c729b2ce 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 @@ -13,6 +13,8 @@ import liquidjava.processor.context.Variable; import liquidjava.processor.context.VariableInstance; import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.utils.constants.Formats; +import liquidjava.utils.constants.Keys; import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinememtsPassage; import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler; import liquidjava.rj_language.Predicate; @@ -39,8 +41,6 @@ public class MethodsFunctionsChecker { private TypeChecker rtc; - private static String retNameFormat = "#ret_%d"; - public MethodsFunctionsChecker(TypeChecker rtc) { this.rtc = rtc; } @@ -74,7 +74,7 @@ public void getConstructorInvocationRefinements(CtConstructorCall ctConstruct Map map = checkInvocationRefinements(ctConstructorCall, ctConstructorCall.getArguments(), ctConstructorCall.getTarget(), f.getName(), f.getTargetClass()); - AuxStateHandler.constructorStateMetadata(rtc.REFINE_KEY, f, map, ctConstructorCall); + AuxStateHandler.constructorStateMetadata(Keys.REFINEMENT, f, map, ctConstructorCall); } } } @@ -140,7 +140,7 @@ private void auxGetMethodRefinements(CtMethod method, RefinedFunction rf) return; List> params = method.getParameters(); Predicate ref = handleFunctionRefinements(rf, method, params); - method.putMetadata(rtc.REFINE_KEY, ref); + method.putMetadata(Keys.REFINEMENT, ref); } /** @@ -163,8 +163,8 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, Optional oc = rtc.getRefinementFromAnnotation(param); Predicate c = new Predicate(); if (oc.isPresent()) - c = oc.get().substituteVariable(rtc.WILD_VAR, paramName); - param.putMetadata(rtc.REFINE_KEY, c); + c = oc.get().substituteVariable(Keys.WILDCARD, paramName); + param.putMetadata(Keys.REFINEMENT, c); RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param); if (v instanceof Variable) f.addArgRefinements((Variable) v); @@ -173,7 +173,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, Optional oret = rtc.getRefinementFromAnnotation(method); Predicate ret = oret.orElse(new Predicate()); - ret = ret.substituteVariable("return", rtc.WILD_VAR); + ret = ret.substituteVariable("return", Keys.WILDCARD); f.setRefReturn(ret); // rtc.context.addFunctionToContext(f); return Predicate.createConjunction(joint, ret); @@ -196,7 +196,7 @@ public void getReturnRefinements(CtReturn ret) { if (ret.getReturnedExpression() != null) { // check if there are refinements if (rtc.getRefinement(ret.getReturnedExpression()) == null) - ret.getReturnedExpression().putMetadata(rtc.REFINE_KEY, new Predicate()); + ret.getReturnedExpression().putMetadata(Keys.REFINEMENT, new Predicate()); CtMethod method = ret.getParent(CtMethod.class); // check if method has refinements if (rtc.getRefinement(method) == null) @@ -211,14 +211,14 @@ public void getReturnRefinements(CtReturn ret) { } // Both return and the method have metadata - String thisName = String.format(rtc.thisFormat, className); + String thisName = String.format(Formats.THIS, className); rtc.getContext().addInstanceToContext(thisName, c.getReference(), new Predicate(), ret); - String returnVarName = String.format(retNameFormat, rtc.getContext().getCounter()); + String returnVarName = String.format(Formats.RET, rtc.getContext().getCounter()); Predicate cretRef = rtc.getRefinement(ret.getReturnedExpression()) - .substituteVariable(rtc.WILD_VAR, returnVarName).substituteVariable(rtc.THIS, returnVarName); - Predicate cexpectedType = fi.getRefReturn().substituteVariable(rtc.WILD_VAR, returnVarName) - .substituteVariable(rtc.THIS, returnVarName); + .substituteVariable(Keys.WILDCARD, returnVarName).substituteVariable(Keys.THIS, returnVarName); + Predicate cexpectedType = fi.getRefReturn().substituteVariable(Keys.WILDCARD, returnVarName) + .substituteVariable(Keys.THIS, returnVarName); rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret); rtc.checkSMT(cexpectedType, ret); @@ -318,7 +318,7 @@ private Map checkInvocationRefinements(CtElement invocation, Lis AuxStateHandler.checkTargetChanges(rtc, f, target, map, invocation); } if (f.allRefinementsTrue()) { - invocation.putMetadata(rtc.REFINE_KEY, new Predicate()); + invocation.putMetadata(Keys.REFINEMENT, new Predicate()); return map; } @@ -336,21 +336,21 @@ private Map checkInvocationRefinements(CtElement invocation, Lis methodRef = methodRef.substituteVariable(s, map.get(s)); String varName = null; - if (invocation.getMetadata(rtc.TARGET_KEY) != null) { - VariableInstance vi = (VariableInstance) invocation.getMetadata(rtc.TARGET_KEY); - methodRef = methodRef.substituteVariable(rtc.THIS, vi.getName()); + if (invocation.getMetadata(Keys.TARGET) != null) { + VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET); + methodRef = methodRef.substituteVariable(Keys.THIS, vi.getName()); Variable v = rtc.getContext().getVariableFromInstance(vi); if (v != null) varName = v.getName(); } - String viName = String.format(rtc.instanceFormat, f.getName(), rtc.getContext().getCounter()); + String viName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter()); VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(), - methodRef.substituteVariable(rtc.WILD_VAR, viName), invocation); // TODO REVER!! + methodRef.substituteVariable(Keys.WILDCARD, viName), invocation); // TODO REVER!! if (varName != null && f.hasStateChange() && equalsThis) rtc.getContext().addRefinementInstanceToVariable(varName, viName); - invocation.putMetadata(rtc.TARGET_KEY, vi); - invocation.putMetadata(rtc.REFINE_KEY, methodRef); + invocation.putMetadata(Keys.TARGET, vi); + invocation.putMetadata(Keys.REFINEMENT, methodRef); } return map; } @@ -382,13 +382,13 @@ private Map mapInvocation(List> arguments, R } private String createVariableRepresentingArgument(CtExpression iArg, Variable fArg) { - Predicate met = (Predicate) iArg.getMetadata(rtc.REFINE_KEY); + Predicate met = (Predicate) iArg.getMetadata(Keys.REFINEMENT); if (met == null) met = new Predicate(); - if (!met.getVariableNames().contains(rtc.WILD_VAR)) - met = Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), met); - String nVar = String.format(rtc.instanceFormat, fArg.getName(), rtc.getContext().getCounter()); - rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(rtc.WILD_VAR, nVar), iArg); + if (!met.getVariableNames().contains(Keys.WILDCARD)) + met = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), met); + String nVar = String.format(Formats.INSTANCE, fArg.getName(), rtc.getContext().getCounter()); + rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(Keys.WILDCARD, nVar), iArg); return nVar; } @@ -404,9 +404,9 @@ private void checkParameters(CtElement invocation, List> arg for (String s : vars) if (map.containsKey(s)) c = c.substituteVariable(s, map.get(s)); - if (invocation.getMetadata(rtc.TARGET_KEY) != null) { - VariableInstance vi = (VariableInstance) invocation.getMetadata(rtc.TARGET_KEY); - c = c.substituteVariable(rtc.THIS, vi.getName()); + if (invocation.getMetadata(Keys.TARGET) != null) { + VariableInstance vi = (VariableInstance) invocation.getMetadata(Keys.TARGET); + c = c.substituteVariable(Keys.THIS, vi.getName()); } rtc.checkSMT(c, invocation); } @@ -429,7 +429,7 @@ private void applyRefinementsToArguments(CtElement element, List CtVariableRead v = (CtVariableRead) e; String varName = v.getVariable().getSimpleName(); // TODO CHANGE RefinedVariable rv = context.getVariableByName(varName); - String instanceName = String.format(rtc.instanceFormat, varName, context.getCounter()); + String instanceName = String.format(Formats.INSTANCE, varName, context.getCounter()); inferredRefinement = inferredRefinement.substituteVariable(fArg.getName(), instanceName); context.addInstanceToContext(instanceName, rv.getType(), inferredRefinement, element); 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 bfdfa173..1c518e5c 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 @@ -8,9 +8,12 @@ import liquidjava.processor.context.Variable; import liquidjava.processor.context.VariableInstance; import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.utils.constants.Formats; +import liquidjava.utils.constants.Keys; +import liquidjava.utils.constants.Ops; +import liquidjava.utils.constants.Types; import liquidjava.rj_language.Predicate; import liquidjava.rj_language.parsing.ParsingException; -import liquidjava.utils.Utils; import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtAssignment; @@ -79,14 +82,14 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws Pars } String type = operator.getType().getQualifiedName(); - List types = Arrays.asList(rtc.implementedTypes); + List types = Arrays.asList(Types.IMPLEMENTED); if (type.contentEquals("boolean")) { - operator.putMetadata(rtc.REFINE_KEY, oper); + operator.putMetadata(Keys.REFINEMENT, oper); if (parent instanceof CtLocalVariable || parent instanceof CtUnaryOperator || parent instanceof CtReturn) - operator.putMetadata(rtc.REFINE_KEY, Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), oper)); + operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), oper)); } else if (types.contains(type)) { - operator.putMetadata(rtc.REFINE_KEY, Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), oper)); + operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), oper)); } else if (type.equals("java.lang.String")) { // skip strings } else { @@ -106,7 +109,7 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws Pars @SuppressWarnings({ "unchecked" }) public void getUnaryOpRefinements(CtUnaryOperator operator) throws ParsingException { CtExpression ex = (CtExpression) operator.getOperand(); - String name = rtc.freshFormat; + String name = Formats.FRESH; Predicate all; if (ex instanceof CtVariableWrite) { CtVariableWrite w = (CtVariableWrite) ex; @@ -126,7 +129,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws Parsin String parentName = w.getVariable().getSimpleName(); if (name.equals(parentName)) { all = getRefinementUnaryVariableWrite(ex, operator, w, name); - operator.putMetadata(rtc.REFINE_KEY, all); + operator.putMetadata(Keys.REFINEMENT, all); return; } } @@ -137,23 +140,21 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws Parsin Predicate metadata = rtc.getRefinement(ex); String newName; - if (!name.equals(rtc.freshFormat)) - newName = String.format(rtc.instanceFormat, name, rtc.getContext().getCounter()); + if (!name.equals(Formats.FRESH)) + newName = String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()); else newName = String.format(name, rtc.getContext().getCounter()); - Predicate newMeta = metadata.substituteVariable(rtc.WILD_VAR, newName); + Predicate newMeta = metadata.substituteVariable(Keys.WILDCARD, newName); Predicate unOp = getOperatorFromKind(operator.getKind(), operator); CtElement p = operator.getParent(); - Predicate opS = unOp.substituteVariable(rtc.WILD_VAR, newName); - + Predicate opS = unOp.substituteVariable(Keys.WILDCARD, newName); if (p instanceof CtIf) all = opS; else - all = Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), opS); // TODO SEE IF () IN OPS IS NEEDED - + all = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), opS); // TODO SEE IF () IN OPS IS NEEDED rtc.getContext().addInstanceToContext(newName, ex.getType(), newMeta, operator); - operator.putMetadata(rtc.REFINE_KEY, all); + operator.putMetadata(Keys.REFINEMENT, all); } /** @@ -191,9 +192,9 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab if (element instanceof CtFieldRead) { CtFieldRead field = ((CtFieldRead) element); if (field.getVariable().getSimpleName().equals("length")) { - String name = String.format(rtc.freshFormat, rtc.getContext().getCounter()); + String name = String.format(Formats.FRESH, rtc.getContext().getCounter()); rtc.getContext().addVarToContext(name, element.getType(), - rtc.getRefinement(element).substituteVariable(rtc.WILD_VAR, name), field); + rtc.getRefinement(element).substituteVariable(Keys.WILDCARD, name), field); return Predicate.createVar(name); } } @@ -202,7 +203,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab CtVariableRead elemVar = (CtVariableRead) element; String elemName = elemVar.getVariable().getSimpleName(); if (elemVar instanceof CtFieldRead) - elemName = String.format(rtc.thisFormat, elemName); + elemName = String.format(Formats.THIS, elemName); Predicate elem_ref = rtc.getContext().getVariableRefinements(elemName); String returnName = elemName; @@ -211,8 +212,8 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab // No need for specific values if (parent != null && !(parent instanceof CtIfImpl)) { elem_ref = rtc.getRefinement(elemVar); - String newName = String.format(rtc.instanceFormat, elemName, rtc.getContext().getCounter()); - Predicate newElem_ref = elem_ref.substituteVariable(rtc.WILD_VAR, newName); + String newName = String.format(Formats.INSTANCE, elemName, rtc.getContext().getCounter()); + Predicate newElem_ref = elem_ref.substituteVariable(Keys.WILDCARD, newName); // String newElem_ref = elem_ref.replace(rtc.WILD_VAR, newName); RefinedVariable newVi = rtc.getContext().addVarToContext(newName, elemVar.getType(), newElem_ref, elemVar); @@ -220,7 +221,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab returnName = newName; } - Predicate e = elem_ref.substituteVariable(rtc.WILD_VAR, elemName); + Predicate e = elem_ref.substituteVariable(Keys.WILDCARD, elemName); rtc.getContext().addVarToContext(elemName, elemVar.getType(), e, elemVar); return Predicate.createVar(returnName); } else if (element instanceof CtBinaryOperator) { @@ -232,8 +233,8 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab // Predicate(left+" "+ getOperatorFromKind(binop.getKind()) +" "+ right); } else if (element instanceof CtUnaryOperator) { - Predicate a = (Predicate) element.getMetadata(rtc.REFINE_KEY); - a = a.substituteVariable(rtc.WILD_VAR, ""); + Predicate a = (Predicate) element.getMetadata(Keys.REFINEMENT); + a = a.substituteVariable(Keys.WILDCARD, ""); String s = a.toString().replace("(", "").replace(")", "").replace("==", "").replace(" ", ""); // TODO // IMPROVE return new Predicate(String.format("(%s)", s), element, rtc.getErrorEmitter()); @@ -258,9 +259,9 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size()); Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!! // Substitute _ by the variable that we send - String newName = String.format(rtc.freshFormat, rtc.getContext().getCounter()); + String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); - innerRefs = innerRefs.substituteVariable(rtc.WILD_VAR, newName); + innerRefs = innerRefs.substituteVariable(Keys.WILDCARD, newName); rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv); return new Predicate(newName, inv, rtc.getErrorEmitter()); // Return variable that represents the invocation } @@ -286,14 +287,14 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtB Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!! // Substitute _ by the variable that we send - String newName = String.format(rtc.freshFormat, rtc.getContext().getCounter()); - innerRefs = innerRefs.substituteVariable(rtc.WILD_VAR, newName); + String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); + innerRefs = innerRefs.substituteVariable(Keys.WILDCARD, newName); // change this for the current instance RefinedVariable r = rtc.getContext().getVariableByName(v.getSimpleName()); if (r instanceof Variable) { Optional ovi = ((Variable) r).getLastInstance(); if (ovi.isPresent()) - innerRefs = innerRefs.substituteVariable(rtc.THIS, ovi.get().getName()); + innerRefs = innerRefs.substituteVariable(Keys.THIS, ovi.get().getName()); } rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv); @@ -317,17 +318,17 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtB */ private Predicate getRefinementUnaryVariableWrite(CtExpression ex, CtUnaryOperator operator, CtVariableWrite w, String name) throws ParsingException { - String newName = String.format(rtc.instanceFormat, name, rtc.getContext().getCounter()); + String newName = String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()); CtVariable varDecl = w.getVariable().getDeclaration(); Predicate metadada = rtc.getContext().getVariableRefinements(varDecl.getSimpleName()); - metadada = metadada.substituteVariable(rtc.WILD_VAR, newName); + metadada = metadada.substituteVariable(Keys.WILDCARD, newName); metadada = metadada.substituteVariable(name, newName); - Predicate c = getOperatorFromKind(operator.getKind(), ex).substituteVariable(rtc.WILD_VAR, newName); + Predicate c = getOperatorFromKind(operator.getKind(), ex).substituteVariable(Keys.WILDCARD, newName); rtc.getContext().addVarToContext(newName, w.getType(), metadada, w); - return Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), c); + return Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), c); } // ############################### Operations Auxiliaries @@ -341,71 +342,36 @@ private Predicate getRefinementUnaryVariableWrite(CtExpression ex, CtUnar * @return */ private String getOperatorFromKind(BinaryOperatorKind kind) { - switch (kind) { - case PLUS: - return Utils.PLUS; - case MINUS: - return Utils.MINUS; - case MUL: - return Utils.MUL; - case DIV: - return Utils.DIV; - case MOD: - return Utils.MOD; - - case AND: - return Utils.AND; - case OR: - return Utils.OR; - - case EQ: - return Utils.EQ; - case NE: - return Utils.NEQ; - case GE: - return Utils.GE; - case GT: - return Utils.GT; - case LE: - return Utils.LE; - case LT: - return Utils.LT; - default: - return null; - // TODO COMPLETE WITH MORE OPERANDS - } + return switch (kind) { + case PLUS -> Ops.PLUS; + case MINUS -> Ops.MINUS; + case MUL -> Ops.MUL; + case DIV -> Ops.DIV; + case MOD -> Ops.MOD; + case AND -> Ops.AND; + case OR -> Ops.OR; + case EQ -> Ops.EQ; + case NE -> Ops.NEQ; + case GE -> Ops.GE; + case GT -> Ops.GT; + case LE -> Ops.LE; + case LT -> Ops.LT; + default -> null; + }; } private Predicate getOperatorFromKind(UnaryOperatorKind kind, CtElement elem) throws ParsingException { - String ret = null; - switch (kind) { - case POSTINC: - ret = rtc.WILD_VAR + " + 1"; - break; - case POSTDEC: - ret = rtc.WILD_VAR + " - 1"; - break; - case PREINC: - ret = rtc.WILD_VAR + " + 1"; - break; - case PREDEC: - ret = rtc.WILD_VAR + " - 1"; - break; - case COMPL: - ret = "(32 & " + rtc.WILD_VAR + ")"; - break; - case NOT: - ret = "!" + rtc.WILD_VAR; - break; - case POS: - ret = "0 + " + rtc.WILD_VAR; - break; - case NEG: - ret = "-" + rtc.WILD_VAR; - break; - default: - throw new ParsingException(kind + "operation not supported"); - } + String ret = switch (kind) { + case POSTINC -> Keys.WILDCARD + " + 1"; + case POSTDEC -> Keys.WILDCARD + " - 1"; + case PREINC -> Keys.WILDCARD + " + 1"; + case PREDEC -> Keys.WILDCARD + " - 1"; + case COMPL -> "(32 & " + Keys.WILDCARD + ")"; + case NOT -> "!" + Keys.WILDCARD; + case POS -> "0 + " + Keys.WILDCARD; + case NEG -> "-" + Keys.WILDCARD; + default -> throw new ParsingException(kind + "operation not supported"); + }; return new Predicate(ret, elem, rtc.getErrorEmitter()); - } + }; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java index ead19e39..04c0c14f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java @@ -11,6 +11,8 @@ import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.rj_language.Predicate; import liquidjava.utils.Utils; +import liquidjava.utils.constants.Formats; +import liquidjava.utils.constants.Keys; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtParameter; @@ -51,7 +53,7 @@ private static HashMap getParametersMap(RefinedFunction superFun List fArgs = function.getArguments(); HashMap m = new HashMap(); for (int i = 0; i < fArgs.size(); i++) { - String newName = String.format(tc.instanceFormat, fArgs.get(i).getName(), tc.getContext().getCounter()); + String newName = String.format(Formats.INSTANCE, fArgs.get(i).getName(), tc.getContext().getCounter()); m.put(superArgs.get(i).getName(), newName); m.put(fArgs.get(i).getName(), newName); RefinedVariable rv = tc.getContext().addVarToContext(newName, superArgs.get(i).getType(), new Predicate(), @@ -96,12 +98,12 @@ static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunct if (functionRef.isBooleanTrue()) function.setRefinement(superRef); else { - String name = String.format(tc.freshFormat, tc.getContext().getCounter()); + String name = String.format(Formats.FRESH, tc.getContext().getCounter()); tc.getContext().addVarToContext(name, superFunction.getType(), new Predicate(), method); // functionRef might be stronger than superRef -> check (superRef <: // functionRef) - functionRef = functionRef.substituteVariable(tc.WILD_VAR, name); - superRef = superRef.substituteVariable(tc.WILD_VAR, name); + functionRef = functionRef.substituteVariable(Keys.WILDCARD, name); + superRef = superRef.substituteVariable(Keys.WILDCARD, name); for (String m : super2function.keySet()) superRef = superRef.substituteVariable(m, super2function.get(m)); for (String m : super2function.keySet()) @@ -140,11 +142,11 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi ObjectState superState = superStates.get(i); ObjectState subState = subStates.get(i); - String thisName = String.format(tc.freshFormat, tc.getContext().getCounter()); + String thisName = String.format(Formats.FRESH, tc.getContext().getCounter()); createVariableInContext(thisName, tc, subFunction, superFunction, method.getParameters().get(i)); - Predicate superConst = matchVariableNames(tc.THIS, thisName, superState.getFrom()); - Predicate subConst = matchVariableNames(tc.THIS, thisName, superFunction, subFunction, + Predicate superConst = matchVariableNames(Keys.THIS, thisName, superState.getFrom()); + Predicate subConst = matchVariableNames(Keys.THIS, thisName, superFunction, subFunction, subState.getFrom()); // fromSup <: fromSub <==> fromSup is sub type and fromSub is expectedType @@ -154,8 +156,8 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi // if(!correct) ErrorPrinter.printError(method, subState.getFrom(), // superState.getFrom()); - superConst = matchVariableNames(tc.THIS, thisName, superState.getTo()); - subConst = matchVariableNames(tc.THIS, thisName, superFunction, subFunction, subState.getTo()); + superConst = matchVariableNames(Keys.THIS, thisName, superState.getTo()); + subConst = matchVariableNames(Keys.THIS, thisName, superFunction, subFunction, subState.getTo()); // toSub <: toSup <==> ToSub is sub type and toSup is expectedType tc.checkStateSMT(subConst, superConst, method, "TO State from Subclass must be subtype of TO State from Superclass"); 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 7198bf9b..77dbaaec 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 @@ -11,6 +11,9 @@ 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; +import liquidjava.utils.constants.Types; import spoon.reflect.code.*; import spoon.reflect.declaration.*; import spoon.reflect.reference.CtTypeReference; @@ -81,15 +84,15 @@ private static void setConstructorStates(RefinedFunction f, List sets = getDifferentSets(tc, klass); // ?? for (GhostFunction sg : sets) { String retType = sg.getReturnType().toString(); Predicate typePredicate = switch (retType) { - case "int" -> Predicate.createLit("0", Utils.INT); - case "boolean" -> Predicate.createLit("false", Utils.BOOLEAN); - case "double" -> Predicate.createLit("0.0", Utils.DOUBLE); + case "int" -> Predicate.createLit("0", Types.INT); + case "boolean" -> Predicate.createLit("false", Types.BOOLEAN); + case "double" -> Predicate.createLit("0.0", Types.DOUBLE); default -> throw new RuntimeException("Ghost not implemented for type " + retType); }; Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getQualifiedName(), s), typePredicate); @@ -191,14 +194,14 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f String t = targetClass; // f.getTargetClass(); CtTypeReference r = tc.getFactory().Type().createReference(t); - String nameOld = String.format(tc.instanceFormat, tc.THIS, tc.getContext().getCounter()); - String name = String.format(tc.instanceFormat, tc.THIS, tc.getContext().getCounter()); + String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); + String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter()); tc.getContext().addVarToContext(name, r, new Predicate(), e); tc.getContext().addVarToContext(nameOld, r, new Predicate(), e); // TODO REVIEW!! // what is it for? Predicate c1 = isTo ? getMissingStates(t, tc, p) : p; - Predicate c = c1.substituteVariable(tc.THIS, name); + Predicate c = c1.substituteVariable(Keys.THIS, name); c = c.changeOldMentions(nameOld, name, tc.getErrorEmitter()); boolean b = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition()); if (b && !tc.getErrorEmitter().foundError()) { @@ -218,7 +221,7 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) sets.remove(g.getParent()); } } - return addOldStates(p, Predicate.createVar(tc.THIS), sets, tc); + return addOldStates(p, Predicate.createVar(Keys.THIS), sets, tc); } /** @@ -265,7 +268,7 @@ private static Predicate addOldStates(Predicate p, Predicate th, List e) { Optional ovi = tc.getContext().getLastVariableInstance(varName); - if (ovi.isPresent() && e.getMetadata(tc.REFINE_KEY) != null) { + if (ovi.isPresent() && e.getMetadata(Keys.REFINEMENT) != null) { VariableInstance vi = ovi.get(); - Predicate c = (Predicate) e.getMetadata(tc.REFINE_KEY); - c = c.substituteVariable(tc.THIS, vi.getName()).substituteVariable(tc.WILD_VAR, vi.getName()); + Predicate c = (Predicate) e.getMetadata(Keys.REFINEMENT); + c = c.substituteVariable(Keys.THIS, vi.getName()).substituteVariable(Keys.WILDCARD, vi.getName()); vi.setRefinement(c); } } @@ -342,7 +345,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { CtField field = fw.getVariable().getDeclaration(); - String updatedVarName = String.format(tc.thisFormat, fw.getVariable().getSimpleName()); + String updatedVarName = String.format(Formats.THIS, fw.getVariable().getSimpleName()); String targetClass = field.getDeclaringType().getQualifiedName(); // state transition annotation construction @@ -366,7 +369,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { VariableInstance vi = invocation_callee.get(); String instanceName = vi.getName(); - Predicate prevState = vi.getRefinement().substituteVariable(tc.WILD_VAR, instanceName) + Predicate prevState = vi.getRefinement().substituteVariable(Keys.WILDCARD, instanceName) .substituteVariable(parentTargetName, instanceName); // StateRefinement(from="true", to="n(this)=this#n") @@ -391,7 +394,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { } // replace "state(this)" to "state(whatever method is called from) and so on" - Predicate expectState = stateChange.getFrom().substituteVariable(tc.THIS, instanceName) + Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName) .changeOldMentions(vi.getName(), instanceName, tc.getErrorEmitter()); if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition @@ -402,9 +405,9 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { return; } - String newInstanceName = String.format(tc.instanceFormat, parentTargetName, tc.getContext().getCounter()); - Predicate transitionedState = stateChange.getTo().substituteVariable(tc.WILD_VAR, newInstanceName) - .substituteVariable(tc.THIS, newInstanceName); + String newInstanceName = String.format(Formats.INSTANCE, parentTargetName, tc.getContext().getCounter()); + Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName) + .substituteVariable(Keys.THIS, newInstanceName); transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName, tc); // update of stata of new instance of this#n#(whatever it was + 1) @@ -445,8 +448,8 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, return new Predicate(); } String instanceName = vi.getName(); - Predicate prevState = vi.getRefinement().substituteVariable(tc.WILD_VAR, instanceName).substituteVariable(name, - instanceName); + Predicate prevState = vi.getRefinement().substituteVariable(Keys.WILDCARD, instanceName) + .substituteVariable(name, instanceName); // List stateChanges = f.getAllStates(); @@ -461,7 +464,7 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, continue; } // replace "state(this)" to "state(whatever method is called from) and so on" - Predicate expectState = stateChange.getFrom().substituteVariable(tc.THIS, instanceName); + Predicate expectState = stateChange.getFrom().substituteVariable(Keys.THIS, instanceName); Predicate prevCheck = prevState; for (String s : map.keySet()) { // substituting function variables into annotation if there are any prevCheck = prevCheck.substituteVariable(s, map.get(s)); @@ -471,9 +474,9 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, found = tc.checksStateSMT(prevCheck, expectState, invocation.getPosition()); if (found && stateChange.hasTo()) { - String newInstanceName = String.format(tc.instanceFormat, name, tc.getContext().getCounter()); - Predicate transitionedState = stateChange.getTo().substituteVariable(tc.WILD_VAR, newInstanceName) - .substituteVariable(tc.THIS, newInstanceName); + String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); + Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName) + .substituteVariable(Keys.THIS, newInstanceName); for (String s : map.keySet()) { transitionedState = transitionedState.substituteVariable(s, map.get(s)); } @@ -503,16 +506,16 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, * * @return */ - private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) { - Predicate noOld = pred; - List listVarsInOld = pred.getOldVariableNames(); - for (String varInOld : listVarsInOld) { - Optional ovi = tc.getContext().getLastVariableInstance(varInOld); - if (ovi.isPresent()) - noOld = noOld.changeOldMentions(varInOld, ovi.get().getName(), tc.getErrorEmitter()); - } - return noOld; - } + // private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) { + // Predicate noOld = pred; + // List listVarsInOld = pred.getOldVariableNames(); + // for (String varInOld : listVarsInOld) { + // Optional ovi = tc.getContext().getLastVariableInstance(varInOld); + // if (ovi.isPresent()) + // noOld = noOld.changeOldMentions(varInOld, ovi.get().getName(), tc.getErrorEmitter()); + // } + // return noOld; + // } private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName, TypeChecker tc) { @@ -533,11 +536,11 @@ private static Predicate sameState(TypeChecker tc, VariableInstance variableInst CtElement invocation) { // if(variableInstance.getState() != null) { if (variableInstance.getRefinement() != null) { - String newInstanceName = String.format(tc.instanceFormat, name, tc.getContext().getCounter()); + String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); // Predicate c = // variableInstance.getState().substituteVariable(variableInstance.getName(), // newInstanceName); - Predicate c = variableInstance.getRefinement().substituteVariable(tc.WILD_VAR, newInstanceName) + Predicate c = variableInstance.getRefinement().substituteVariable(Keys.WILDCARD, newInstanceName) .substituteVariable(variableInstance.getName(), newInstanceName); addInstanceWithState(tc, name, newInstanceName, variableInstance, c, invocation); @@ -581,7 +584,7 @@ private static String addInstanceWithState(TypeChecker tc, String superName, Str } } - invocation.putMetadata(tc.TARGET_KEY, vi2); + invocation.putMetadata(Keys.TARGET, vi2); return name2; } @@ -600,31 +603,31 @@ static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElem String name = v.getVariable().getSimpleName(); Optional invocation_callee = tc.getContext().getLastVariableInstance(name); if (invocation_callee.isPresent()) { - invocation.putMetadata(tc.TARGET_KEY, invocation_callee.get()); - } else if (target2.getMetadata(tc.TARGET_KEY) == null) { + invocation.putMetadata(Keys.TARGET, invocation_callee.get()); + } else if (target2.getMetadata(Keys.TARGET) == null) { RefinedVariable var = tc.getContext().getVariableByName(name); - String nName = String.format(tc.instanceFormat, name, tc.getContext().getCounter()); + String nName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); RefinedVariable rv = tc.getContext().addInstanceToContext(nName, var.getType(), var.getRefinement().substituteVariable(name, nName), target2); tc.getContext().addRefinementInstanceToVariable(name, nName); - invocation.putMetadata(tc.TARGET_KEY, rv); + invocation.putMetadata(Keys.TARGET, rv); } return name; - } else if (target2.getMetadata(tc.TARGET_KEY) != null) { + } else if (target2.getMetadata(Keys.TARGET) != null) { // invokation is in // who did put the metadata here then? - VariableInstance target2_vi = (VariableInstance) target2.getMetadata(tc.TARGET_KEY); + VariableInstance target2_vi = (VariableInstance) target2.getMetadata(Keys.TARGET); Optional v = target2_vi.getParent(); - invocation.putMetadata(tc.TARGET_KEY, target2_vi); + invocation.putMetadata(Keys.TARGET, target2_vi); return v.map(Refined::getName).orElse(target2_vi.getName()); } return null; } static VariableInstance getTarget(TypeChecker tc, CtElement invocation) { - if (invocation.getMetadata(tc.TARGET_KEY) != null) { - return (VariableInstance) invocation.getMetadata(tc.TARGET_KEY); + if (invocation.getMetadata(Keys.TARGET) != null) { + return (VariableInstance) invocation.getMetadata(Keys.TARGET); } return null; } 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 1f476f15..8456aee1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -22,12 +22,14 @@ import liquidjava.rj_language.ast.LiteralReal; import liquidjava.rj_language.ast.UnaryExpression; import liquidjava.rj_language.ast.Var; -import liquidjava.rj_language.opt.derivation_node.DerivationNode; 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; +import liquidjava.utils.constants.Ops; +import liquidjava.utils.constants.Types; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtType; import spoon.reflect.factory.Factory; @@ -155,7 +157,7 @@ public Predicate changeOldMentions(String previousName, String newName, ErrorEmi Expression prev = createVar(previousName).getExpression(); List le = new ArrayList<>(); le.add(createVar(newName).getExpression()); - e.substituteFunction(Utils.OLD, le, prev); + e.substituteFunction(Keys.OLD, le, prev); return new Predicate(e); } @@ -168,7 +170,7 @@ public List getOldVariableNames() { private void expressionGetOldVariableNames(Expression exp, List ls) { if (exp instanceof FunctionInvocation) { FunctionInvocation fi = (FunctionInvocation) exp; - if (fi.getName().equals(Utils.OLD)) { + if (fi.getName().equals(Keys.OLD)) { List le = fi.getArgs(); for (Expression e : le) { if (e instanceof Var) @@ -221,15 +223,15 @@ public ValDerivationNode simplify() { } public static Predicate createConjunction(Predicate c1, Predicate c2) { - return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression())); + return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression())); } public static Predicate createDisjunction(Predicate c1, Predicate c2) { - return new Predicate(new BinaryExpression(c1.getExpression(), Utils.OR, c2.getExpression())); + return new Predicate(new BinaryExpression(c1.getExpression(), Ops.OR, c2.getExpression())); } public static Predicate createEquals(Predicate c1, Predicate c2) { - return new Predicate(new BinaryExpression(c1.getExpression(), Utils.EQ, c2.getExpression())); + return new Predicate(new BinaryExpression(c1.getExpression(), Ops.EQ, c2.getExpression())); } public static Predicate createITE(Predicate c1, Predicate c2, Predicate c3) { @@ -237,20 +239,13 @@ public static Predicate createITE(Predicate c1, Predicate c2, Predicate c3) { } public static Predicate createLit(String value, String type) { - Expression ex; - if (type.equals(Utils.BOOLEAN)) - ex = new LiteralBoolean(value); - else if (type.equals(Utils.INT)) - ex = new LiteralInt(value); - else if (type.equals(Utils.DOUBLE)) - ex = new LiteralReal(value); - else if (type.equals(Utils.SHORT)) - ex = new LiteralInt(value); - else if (type.equals(Utils.LONG)) - ex = new LiteralReal(value); - else // if(type.equals(Utils.DOUBLE)) - ex = new LiteralReal(value); - return new Predicate(ex); + Expression exp = switch (type) { + case Types.BOOLEAN -> new LiteralBoolean(value); + case Types.INT, Types.SHORT -> new LiteralInt(value); + case Types.DOUBLE, Types.LONG -> new LiteralReal(value); + default -> new LiteralReal(value); + }; + return new Predicate(exp); } public static Predicate createOperation(Predicate c1, String op, Predicate c2) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java index 899b2367..5e07cd03 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java @@ -68,18 +68,10 @@ public Expression clone() { @Override public boolean isBooleanTrue() { - switch (op) { - case "&&": - return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); - case "||": - return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); - case "-->": - return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); - case "==": - return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); - default: - return false; - } + return switch (op) { + case "&&", "||", "-->", "==" -> getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); + default -> false; + }; } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 5c5539d2..36b167cc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -41,25 +41,14 @@ public static void storeVariablesSubtypes(Context z3, List vari private static Expr getExpr(Context z3, String name, CtTypeReference type) { String typeName = type.getQualifiedName(); - if (typeName.contentEquals("int")) - return z3.mkIntConst(name); - else if (typeName.contentEquals("short")) - return z3.mkIntConst(name); - else if (typeName.contentEquals("boolean")) - return z3.mkBoolConst(name); - else if (typeName.contentEquals("long")) - return z3.mkRealConst(name); - else if (typeName.contentEquals("float")) { - return (FPExpr) z3.mkConst(name, z3.mkFPSort64()); - } else if (typeName.contentEquals("double")) { - return (FPExpr) z3.mkConst(name, z3.mkFPSort64()); - } else if (typeName.contentEquals("int[]")) { - return z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); - } else { - Sort nSort = z3.mkUninterpretedSort(typeName); - return z3.mkConst(name, nSort); - // System.out.println("Add new type: "+typeName); - } + return switch (typeName) { + case "int", "short" -> z3.mkIntConst(name); + case "boolean" -> z3.mkBoolConst(name); + case "long" -> z3.mkRealConst(name); + case "float", "double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64()); + case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort()); + default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName)); + }; } static void addAlias(Context z3, List alias, Map aliasTranslation) { @@ -92,27 +81,18 @@ private static void addBuiltinFunctions(Context z3, Map> fun } static Sort getSort(Context z3, String sort) { - switch (sort) { - case "int": - return z3.getIntSort(); - case "boolean": - return z3.getBoolSort(); - case "long": - return z3.getRealSort(); - case "float": - return z3.mkFPSort32(); - case "double": - return z3.mkFPSortDouble(); - case "int[]": - return z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort()); - case "String": - return z3.getStringSort(); - case "void": - return z3.mkUninterpretedSort("void"); - // case "List":return z3.mkListSort(name, elemSort) - default: - return z3.mkUninterpretedSort(sort); - } + return switch (sort) { + case "int" -> z3.getIntSort(); + case "boolean" -> z3.getBoolSort(); + case "long" -> z3.getRealSort(); + case "float" -> z3.mkFPSort32(); + case "double" -> z3.mkFPSortDouble(); + case "int[]" -> z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort()); + case "String" -> z3.getStringSort(); + case "void" -> z3.mkUninterpretedSort("void"); + // case "List" -> z3.mkListSort(name, elemSort); + default -> z3.mkUninterpretedSort(sort); + }; } public static void addGhostStates(Context z3, List ghostState, diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index b4219d2a..ed0db04e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -37,6 +37,7 @@ public TranslatorToZ3(liquidjava.processor.context.Context c) { TranslatorContextToZ3.addGhostStates(z3, c.getGhostState(), funcTranslation); } + @SuppressWarnings("unchecked") public Status verifyExpression(Expr e) throws Exception { Solver s = z3.mkSolver(); // s.add((BoolExpr) e.eval(this)); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 6c204258..089c28d7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -2,62 +2,25 @@ import java.util.Set; +import liquidjava.utils.constants.Types; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; public class Utils { - public static final String AND = "&&"; - public static final String OR = "||"; - - public static final String EQ = "=="; - public static final String NEQ = "!="; - public static final String GT = ">"; - public static final String GE = ">="; - public static final String LT = "<"; - public static final String LE = "<="; - - public static final String PLUS = "+"; - public static final String MINUS = "-"; - public static final String MUL = "*"; - public static final String DIV = "/"; - public static final String MOD = "%"; - - public static final String WILD_VAR = "_"; - public static final String OLD = "old"; - - public static final String INT = "int"; - public static final String DOUBLE = "double"; - public static final String STRING = "String"; - public static final String BOOLEAN = "boolean"; - public static final String INT_LIST = "int[]"; - public static final String LIST = "List"; - public static final String SHORT = "short"; - public static final String LONG = "long"; - public static final String FLOAT = "float"; - public static final String NULL_TYPE = ""; - private static final Set DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex"); public static CtTypeReference getType(String type, Factory factory) { - // TODO complete - switch (type) { - case INT: - return factory.Type().INTEGER_PRIMITIVE; - case DOUBLE: - return factory.Type().DOUBLE_PRIMITIVE; - case BOOLEAN: - return factory.Type().BOOLEAN_PRIMITIVE; - case INT_LIST: - return factory.createArrayReference(getType("int", factory)); - case STRING: - return factory.Type().STRING; - case LIST: - return factory.Type().LIST; - default: - // return factory.Type().OBJECT; - return factory.createReference(type); - } + // TODO: complete with other types + return switch (type) { + case Types.INT -> factory.Type().INTEGER_PRIMITIVE; + case Types.DOUBLE -> factory.Type().DOUBLE_PRIMITIVE; + case Types.BOOLEAN -> factory.Type().BOOLEAN_PRIMITIVE; + case Types.INT_LIST -> factory.createArrayReference(getType("int", factory)); + case Types.STRING -> factory.Type().STRING; + case Types.LIST -> factory.Type().LIST; + default -> factory.createReference(type); + }; } public static String getSimpleName(String name) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java new file mode 100644 index 00000000..f3ae77f0 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java @@ -0,0 +1,8 @@ +package liquidjava.utils.constants; + +public final class Formats { + public static final String FRESH = "#fresh_%d"; + public static final String INSTANCE = "#%s_%d"; + public static final String THIS = "this#%s"; + public static final String RET = "#ret_%d"; +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java new file mode 100644 index 00000000..790845fa --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Keys.java @@ -0,0 +1,9 @@ +package liquidjava.utils.constants; + +public final class Keys { + public static final String REFINEMENT = "refinement"; + public static final String TARGET = "target"; + public static final String THIS = "this"; + public static final String WILDCARD = "_"; + public static final String OLD = "old"; +} \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Ops.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Ops.java new file mode 100644 index 00000000..82312a35 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Ops.java @@ -0,0 +1,17 @@ +package liquidjava.utils.constants; + +public class Ops { + public static final String AND = "&&"; + public static final String OR = "||"; + public static final String EQ = "=="; + public static final String NEQ = "!="; + public static final String GT = ">"; + public static final String GE = ">="; + public static final String LT = "<"; + public static final String LE = "<="; + public static final String PLUS = "+"; + public static final String MINUS = "-"; + public static final String MUL = "*"; + public static final String DIV = "/"; + public static final String MOD = "%"; +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Patterns.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Patterns.java new file mode 100644 index 00000000..2bac52d7 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Patterns.java @@ -0,0 +1,8 @@ +package liquidjava.utils.constants; + +import java.util.regex.Pattern; + +public final class Patterns { + public static final Pattern THIS = Pattern.compile("#this_\\d+"); + public static final Pattern INSTANCE = Pattern.compile("^#(.+)_[0-9]+$"); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Types.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Types.java new file mode 100644 index 00000000..39472de2 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Types.java @@ -0,0 +1,15 @@ +package liquidjava.utils.constants; + +public class Types { + public static final String INT = "int"; + public static final String DOUBLE = "double"; + public static final String STRING = "String"; + public static final String BOOLEAN = "boolean"; + public static final String INT_LIST = "int[]"; + public static final String LIST = "List"; + public static final String SHORT = "short"; + public static final String LONG = "long"; + public static final String FLOAT = "float"; + public static final String NULL = ""; + public static final String[] IMPLEMENTED = { "boolean", "int", "short", "long", "float", "double" }; +} \ No newline at end of file From 194f7dd9669ffcf1f64773ea1a89f2f3a1b7fa16 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 19:08:11 +0000 Subject: [PATCH 2/4] Minor Fix --- .../main/java/liquidjava/rj_language/ast/Expression.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java index 56912642..37e3343e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java @@ -180,9 +180,9 @@ public Expression changeAlias(Map alias, Context ctx, Factory String varType = dto.getVarTypes().get(i); Expression aliasExp = children.get(i); - boolean checks = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f); - if (!checks) - throw new Exception("Type Mismatch: Cannoy substitute " + aliasExp + " : " + boolean compatible = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f); + if (!compatible) + throw new Exception("Type Mismatch: Cannot substitute " + aliasExp + " : " + TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName() + " by " + varExp + " : " + TypeInfer.getType(ctx, f, varExp).get().getQualifiedName()); From 07ca3f08ff1d5e68e6139a5a406f6503c7da3c25 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 9 Nov 2025 20:39:59 +0000 Subject: [PATCH 3/4] Fix NullPointerException in `OperationsChecker` --- .../refinement_checker/general_checkers/OperationsChecker.java | 3 +++ 1 file changed, 3 insertions(+) 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 1c518e5c..a4adf7c7 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 @@ -245,6 +245,9 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab // skip strings return new Predicate(); } + if (l.getValue() == null) + throw new ParsingException("Null literals are not supported"); + return new Predicate(l.getValue().toString(), element, rtc.getErrorEmitter()); } else if (element instanceof CtInvocation) { From 5472ca716321b5412f03125a90ee585b21dfdbc2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 10 Nov 2025 15:27:32 +0000 Subject: [PATCH 4/4] Requested Changes --- .../errors/StateConflictError.java | 4 ++- .../RefinementTypeChecker.java | 2 +- .../refinement_checker/VCChecker.java | 15 --------- .../object_checkers/AuxStateHandler.java | 33 ------------------- .../liquidjava/rj_language/Predicate.java | 4 +-- 5 files changed, 6 insertions(+), 52 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java index 23ac0812..1f714cb2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -14,7 +14,9 @@ public class StateConflictError extends LJError { private String className; public StateConflictError(CtElement element, Predicate predicate, String className) { - super("State Conflict Error", "Found multiple disjoint states in state transition", element); + super("State Conflict Error", + "Found multiple disjoint states in state transition — State transition can only go to one state of each state set", + element); this.predicate = predicate; this.className = className; } 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 ae3b77f4..53b65116 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 @@ -174,7 +174,7 @@ public void visitCtNewArray(CtNewArray newArray) { } catch (ParsingException e) { return; // error already in ErrorEmitter } - String name = String.format(Formats.RET, context.getCounter()); + String name = String.format(Formats.FRESH, context.getCounter()); if (c.getVariableNames().contains(Keys.WILDCARD)) { c = c.substituteVariable(Keys.WILDCARD, name); } else { 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 b23200a9..cba055bc 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 @@ -304,14 +304,6 @@ void removePathVariableThatIncludes(String otherVar) { .collect(Collectors.toList()).forEach(pathVariables::remove); } - // private void printVCs(String string, String stringSMT, Predicate expectedType) { - // System.out.println("\n----------------------------VC--------------------------------\n"); - // System.out.println(string); - // System.out.println("\nSMT subtyping:" + stringSMT + " <: " + expectedType.toString()); - // System.out.println("--------------------------------------------------------------"); - // } - - // Print // Errors--------------------------------------------------------------------------------------------------- private HashMap createMap(CtElement element, Predicate expectedType) { @@ -369,13 +361,6 @@ private void printError(Exception e, Predicate premisesBeforeChange, Predicate e } } - // private void printError(Predicate premises, Predicate expectedType, CtElement element, - // HashMap map, String s) { - // Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map); - // Predicate cSMTMessageReady = premises; // substituteByMap(premises, map); - // ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); - // } - public void printStateMismatchError(CtElement element, String method, Predicate c, String states) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(c, lrv, mainVars); 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 77dbaaec..1d52caa9 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 @@ -498,25 +498,6 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, return new Predicate(); } - /** - * Method prepared to change all old vars in a predicate, however it has not been needed yet - * - * @param pred - * @param tc - * - * @return - */ - // private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) { - // Predicate noOld = pred; - // List listVarsInOld = pred.getOldVariableNames(); - // for (String varInOld : listVarsInOld) { - // Optional ovi = tc.getContext().getLastVariableInstance(varInOld); - // if (ovi.isPresent()) - // noOld = noOld.changeOldMentions(varInOld, ovi.get().getName(), tc.getErrorEmitter()); - // } - // return noOld; - // } - private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName, TypeChecker tc) { return transitionedState.changeOldMentions(instanceName, newInstanceName, tc.getErrorEmitter()); @@ -534,12 +515,8 @@ private static Predicate checkOldMentions(Predicate transitionedState, String in */ private static Predicate sameState(TypeChecker tc, VariableInstance variableInstance, String name, CtElement invocation) { - // if(variableInstance.getState() != null) { if (variableInstance.getRefinement() != null) { String newInstanceName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); - // Predicate c = - // variableInstance.getState().substituteVariable(variableInstance.getName(), - // newInstanceName); Predicate c = variableInstance.getRefinement().substituteVariable(Keys.WILDCARD, newInstanceName) .substituteVariable(variableInstance.getName(), newInstanceName); @@ -636,15 +613,5 @@ private static List> getStateAnnotation(CtEle return element.getAnnotations().stream().filter(ann -> ann.getActualAnnotation().annotationType() .getCanonicalName().contentEquals("liquidjava.specification.StateRefinement")) .collect(Collectors.toList()); - - // List> l = new ArrayList>(); - // for (CtAnnotation ann : element.getAnnotations()) { - // String an = ann.getActualAnnotation().annotationType().getCanonicalName(); - // if (an.contentEquals("liquidjava.specification.StateRefinement")) { - // l.add(ann); - // } - // } - // return l; } } \ No newline at end of file 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 8456aee1..cb17f5ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -242,8 +242,8 @@ public static Predicate createLit(String value, String type) { Expression exp = switch (type) { case Types.BOOLEAN -> new LiteralBoolean(value); case Types.INT, Types.SHORT -> new LiteralInt(value); - case Types.DOUBLE, Types.LONG -> new LiteralReal(value); - default -> new LiteralReal(value); + case Types.DOUBLE, Types.LONG, Types.FLOAT -> new LiteralReal(value); + default -> throw new IllegalArgumentException("Unsupported literal type: " + type); }; return new Predicate(exp); }