diff --git a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java index 08162fe8..6a066f7b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java +++ b/liquidjava-verifier/src/main/java/liquidjava/api/CommandLineLauncher.java @@ -30,7 +30,9 @@ public static void main(String[] args) { launch(paths.toArray(new String[0])); // print diagnostics - System.out.println(diagnostics.getWarningOutput()); + if (diagnostics.foundWarning()) { + System.out.println(diagnostics.getWarningOutput()); + } if (diagnostics.foundError()) { System.out.println(diagnostics.getErrorOutput()); } else { @@ -50,7 +52,6 @@ public static void launch(String... paths) { } launcher.addInputResource(path); } - launcher.getEnvironment().setNoClasspath(true); launcher.getEnvironment().setComplianceLevel(8); launcher.run(); @@ -60,16 +61,9 @@ public static void launch(String... paths) { final RefinementProcessor processor = new RefinementProcessor(factory); processingManager.addProcessor(processor); - try { - // analyze all packages - CtPackage root = factory.Package().getRootPackage(); - if (root != null) - processingManager.process(root); - } catch (Exception e) { - e.printStackTrace(); - throw e; - } - - return; + // analyze all packages + CtPackage root = factory.Package().getRootPackage(); + if (root != null) + processingManager.process(root); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java index ff669fec..7b72d190 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java @@ -3,10 +3,7 @@ // ANSI color codes public class Colors { public static final String RESET = "\u001B[0m"; - public static final String BOLD = "\u001B[1m"; public static final String GREY = "\u001B[90m"; - public static final String RED = "\u001B[31m"; public static final String BOLD_RED = "\u001B[1;31m"; - public static final String YELLOW = "\u001B[33m"; public static final String BOLD_YELLOW = "\u001B[1;33m"; } \ No newline at end of file diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java index fc7c75f7..846f3dc6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/Diagnostics.java @@ -13,8 +13,8 @@ public class Diagnostics { private static final Diagnostics instance = new Diagnostics(); - private LinkedHashSet errors; - private LinkedHashSet warnings; + private final LinkedHashSet errors; + private final LinkedHashSet warnings; private Diagnostics() { this.errors = new LinkedHashSet<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java index 354e8680..3383f6bf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java @@ -2,59 +2,11 @@ import spoon.reflect.cu.SourcePosition; -public class ErrorPosition { - - private int lineStart; - private int colStart; - private int lineEnd; - private int colEnd; - - public ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) { - this.lineStart = lineStart; - this.colStart = colStart; - this.lineEnd = lineEnd; - this.colEnd = colEnd; - } - - public int getLineStart() { - return lineStart; - } - - public int getColStart() { - return colStart; - } - - public int getLineEnd() { - return lineEnd; - } - - public int getColEnd() { - return colEnd; - } +public record ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) { public static ErrorPosition fromSpoonPosition(SourcePosition pos) { if (pos == null || !pos.isValidPosition()) return null; return new ErrorPosition(pos.getLine(), pos.getColumn(), pos.getEndLine(), pos.getEndColumn()); } - - @Override - public boolean equals(Object obj) { - if (this == obj) - return true; - if (obj == null || getClass() != obj.getClass()) - return false; - ErrorPosition other = (ErrorPosition) obj; - return lineStart == other.lineStart && colStart == other.colStart && lineEnd == other.lineEnd - && colEnd == other.colEnd; - } - - @Override - public int hashCode() { - int result = lineStart; - result = 31 * result + colStart; - result = 31 * result + lineEnd; - result = 31 * result + colEnd; - return result; - } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index 9beaccfa..bf7df8b0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -8,12 +8,12 @@ public class LJDiagnostic extends RuntimeException { - private String title; - private String message; - private String details; - private String file; - private ErrorPosition position; - private String accentColor; + private final String title; + private final String message; + private final String details; + private final String file; + private final ErrorPosition position; + private final String accentColor; public LJDiagnostic(String title, String message, String details, SourcePosition pos, String accentColor) { this.title = title; @@ -65,7 +65,7 @@ public String toString() { // location if (file != null && position != null) { - sb.append("\n").append(file).append(":").append(position.getLineStart()).append(Colors.RESET).append("\n"); + sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n"); } return sb.toString(); @@ -83,12 +83,11 @@ public String getSnippet() { // before and after lines for context int contextBefore = 2; int contextAfter = 2; - int startLine = Math.max(1, position.getLineStart() - contextBefore); - int endLine = Math.min(lines.size(), position.getLineEnd() + contextAfter); + int startLine = Math.max(1, position.lineStart() - contextBefore); + int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter); // calculate padding for line numbers - int maxLineNum = endLine; - int padding = String.valueOf(maxLineNum).length(); + int padding = String.valueOf(endLine).length(); for (int i = startLine; i <= endLine; i++) { String lineNumStr = String.format("%" + padding + "d", i); @@ -98,9 +97,9 @@ public String getSnippet() { sb.append(Colors.GREY).append(lineNumStr).append(" | ").append(line).append(Colors.RESET).append("\n"); // add error markers on the line(s) with the error - if (i >= position.getLineStart() && i <= position.getLineEnd()) { - int colStart = (i == position.getLineStart()) ? position.getColStart() : 1; - int colEnd = (i == position.getLineEnd()) ? position.getColEnd() : line.length(); + if (i >= position.lineStart() && i <= position.lineEnd()) { + int colStart = (i == position.lineStart()) ? position.colStart() : 1; + int colEnd = (i == position.lineEnd()) ? position.colEnd() : line.length(); if (colStart > 0 && colEnd > 0) { // line number padding + " | " + column offset diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java index 73a933aa..1c063fa0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/GhostInvocationError.java @@ -11,7 +11,7 @@ */ public class GhostInvocationError extends LJError { - private String expected; + private final String expected; public GhostInvocationError(String message, SourcePosition pos, Expression expected, TranslationTable translationTable) { 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 8012928c..c94ef1ff 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java @@ -9,7 +9,7 @@ */ public class InvalidRefinementError extends LJError { - private String refinement; + private final String refinement; public InvalidRefinementError(CtElement element, String message, String refinement) { super("Invalid Refinement", message, "", element.getPosition(), null); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java index 446dea22..32a4e17d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/LJError.java @@ -10,7 +10,7 @@ */ public abstract class LJError extends LJDiagnostic { - private TranslationTable translationTable; + private final TranslationTable translationTable; public LJError(String title, String message, String details, SourcePosition pos, TranslationTable translationTable) { 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 72172934..87fd76e9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java @@ -12,8 +12,8 @@ */ public class RefinementError extends LJError { - private String expected; - private ValDerivationNode found; + private final String expected; + private final ValDerivationNode found; public RefinementError(CtElement element, Expression expected, ValDerivationNode found, TranslationTable translationTable) { 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 fd250e49..1fe85155 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateConflictError.java @@ -11,8 +11,8 @@ */ public class StateConflictError extends LJError { - private String state; - private String className; + private final String state; + private final String className; public StateConflictError(CtElement element, Expression state, String className, TranslationTable translationTable) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java index 1cf7101a..226e6ed5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/SyntaxError.java @@ -9,7 +9,7 @@ */ public class SyntaxError extends LJError { - private String refinement; + private final String refinement; public SyntaxError(String message, String refinement) { this(message, null, refinement); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java index 7fcbc468..e3d1c239 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalClassNotFoundWarning.java @@ -9,7 +9,7 @@ */ public class ExternalClassNotFoundWarning extends LJWarning { - private String className; + private final String className; public ExternalClassNotFoundWarning(CtElement element, String message, String className) { super(message, "", element.getPosition()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java index 4f90e994..26ad6f51 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/warnings/ExternalMethodNotFoundWarning.java @@ -9,8 +9,8 @@ */ public class ExternalMethodNotFoundWarning extends LJWarning { - private String methodName; - private String className; + private final String methodName; + private final String className; public ExternalMethodNotFoundWarning(CtElement element, String message, String details, String methodName, String className) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/TestInsideClasses.java b/liquidjava-verifier/src/main/java/liquidjava/processor/TestInsideClasses.java deleted file mode 100644 index 43fa8393..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/TestInsideClasses.java +++ /dev/null @@ -1,27 +0,0 @@ -package liquidjava.processor; - -import spoon.Launcher; - -public class TestInsideClasses { - public static void main(String[] args) { - - Launcher launcher = new Launcher(); - launcher.getEnvironment().setComplianceLevel(8); - launcher.run(); - - // final Factory factory = launcher.getFactory(); - // RefinedVariable vi2 = new Variable("a",factory.Type().INTEGER_PRIMITIVE, new Predicate("a > - // 0")); - // CtTypeReference intt = factory.Type().INTEGER_PRIMITIVE; - // List> l = new ArrayList<>(); - // l.add(intt); - // GhostState s = new GhostState("green", l, intt, "A"); - // GhostState ss = new GhostState("yellow", l, intt, "A"); - // GhostState sss = new GhostState("red", l, intt, "A"); - // List gh = new ArrayList<>(); - // gh.add(s);gh.add(ss);gh.add(sss); - // Predicate p = new Predicate("green(this) && red(this) == iio && u(3)"); - // System.out.println(p.getVariableNames()); - - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 35daad11..152488a8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -32,7 +32,7 @@ public String toString() { String qualType = type.getQualifiedName(); String simpleType = qualType.contains(".") ? Utils.getSimpleName(qualType) : qualType; return String.format("%-20s %s %s", "∀" + name + ":" + simpleType + ",", refinement.toString(), - next != null ? " => \n" + next.toString() : ""); + next != null ? " => \n" + next : ""); } else return String.format("%-20s %s", "", refinement.toString()); } 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 29600b36..10ad84e6 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,10 @@ public Factory getFactory() { public void visitCtClass(CtClass ctClass) { ctClass.getDeclaredFields().stream().filter(fld -> fld.getType().getQualifiedName().equals("int")) .forEach(fld -> { - CtTypeReference fld_type = fld.getType(); - CtAnnotation gen_ann = factory.createAnnotation(factory.createCtTypeReference(Ghost.class)); - gen_ann.addValue("value", fld_type.getSimpleName() + " " + fld.getSimpleName()); - ctClass.addAnnotation(gen_ann); + CtTypeReference fldType = fld.getType(); + CtAnnotation genAnn = factory.createAnnotation(factory.createCtTypeReference(Ghost.class)); + genAnn.addValue("value", fldType.getSimpleName() + " " + fld.getSimpleName()); + ctClass.addAnnotation(genAnn); }); super.visitCtClass(ctClass); 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 227db985..a9838440 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -1,32 +1,22 @@ package liquidjava.processor.context; import java.util.ArrayList; -import java.util.HashMap; 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.utils.Utils; -import spoon.reflect.declaration.CtElement; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; public class AliasWrapper { - private String name; - private List> varTypes; - private List varNames; - private Predicate expression; - // private Context context; - - private String newAliasFormat = "#alias_%s_%d"; + private final String name; + private final List> varTypes; + private final List varNames; + private final Predicate expression; - public AliasWrapper(AliasDTO a, Factory factory, String wILD_VAR, Context context2, String klass, String path) { + public AliasWrapper(AliasDTO a, Factory factory, String klass, String path) { name = a.getName(); expression = new Predicate(a.getExpression()); - varTypes = new ArrayList<>(); varNames = a.getVarNames(); for (String s : a.getVarTypes()) { @@ -48,69 +38,10 @@ public List getVarNames() { } public Predicate getClonedPredicate() { - return (Predicate) expression.clone(); - } - - public Expression getNewExpression(List newNames) { - Predicate expr = getClonedPredicate(); - for (int i = 0; i < newNames.size(); i++) { - expr = expr.substituteVariable(varNames.get(i), newNames.get(i)); - } - return expr.getExpression().clone(); - } - - 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++) { - prem = Predicate.createConjunction(prem, - Predicate.createEquals(Predicate.createVar(newNames.get(i)), invocationPredicates.get(i))); - } - return prem.clone(); - } - - private List getPredicatesFromExpression(List list, CtElement elem) throws LJError { - List lp = new ArrayList<>(); - for (String e : list) - lp.add(new Predicate(e, elem)); - - return lp; - } - - public List getNewVariables(Context context) { - List n = new ArrayList<>(); - for (int i = 0; i < varNames.size(); i++) - n.add(String.format(newAliasFormat, varNames.get(i), context.getCounter())); - return n; - } - - public Map> getTypes(List names) { - Map> m = new HashMap<>(); - for (int i = 0; i < names.size(); i++) { - m.put(names.get(i), varTypes.get(i)); - } - return m; + return expression.clone(); } public AliasDTO createAliasDTO() { return new AliasDTO(name, varTypes, varNames, expression.getExpression()); } - - // public Expression getSubstitutedExpression(List newNames) { - // return null; - // } - // - - // TypeKeyword tk; - // AliasName name; - // - // ParenthesisLeft pl; - // Type type; - // Var var; - // ParenthesisRight rl; - // - // BraceLeft bl; - // Expression e; - // BraceRight br; - } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index a09fb0e4..ca4d68e8 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -10,7 +10,7 @@ public class Context { private List ctxFunctions; private List ctxSpecificVars; - private List ctxGlobalVars; + private final List ctxGlobalVars; private List ghosts; private Map> classStates; @@ -24,9 +24,7 @@ private Context() { ctxVars.add(new ArrayList<>()); ctxFunctions = new ArrayList<>(); ctxSpecificVars = new ArrayList<>(); - // globals ctxGlobalVars = new ArrayList<>(); - // ctxGlobalFunctions = new ArrayList<>(); alias = new ArrayList<>(); ghosts = new ArrayList<>(); @@ -34,7 +32,6 @@ private Context() { counter = 0; } - // SINGLETON public static Context getInstance() { if (instance == null) instance = new Context(); @@ -44,11 +41,7 @@ public static Context getInstance() { public void reinitializeContext() { ctxVars = new Stack<>(); ctxVars.add(new ArrayList<>()); // global vars - // ctxFunctions = new ArrayList<>(); ctxSpecificVars = new ArrayList<>(); - // alias = new ArrayList<>(); - // ghosts = new ArrayList<>(); - // counter = 0; } public void reinitializeAllContext() { @@ -95,12 +88,6 @@ public Map> getContext() { } // ---------------------- Global variables ---------------------- - public void addGlobalVariableToContext(String simpleName, CtTypeReference type, Predicate c) { - RefinedVariable vi = new Variable(simpleName, type, c); - ctxGlobalVars.add(vi); - vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); - } - public void addGlobalVariableToContext(String simpleName, String location, CtTypeReference type, Predicate c) { RefinedVariable vi = new Variable(simpleName, location, type, c); vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); @@ -109,7 +96,6 @@ public void addGlobalVariableToContext(String simpleName, String location, CtTyp // ---------------------- Add variables and instances ---------------------- public void addVarToContext(RefinedVariable var) { - // if(!hasVariable(var.getName())) ctxVars.peek().add(var); CtTypeReference type = var.getType(); var.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); @@ -183,27 +169,15 @@ public boolean hasVariable(String name) { return getVariableByName(name) != null; } - public String allVariablesToString() { - StringBuilder sb = new StringBuilder(); - for (List l : ctxVars) { - for (RefinedVariable var : l) { - sb.append(var.toString() + "; "); - } - } - return sb.toString(); - } - /** * Lists all variables inside the stack * - * @return + * @return list of all variables */ public List getAllVariables() { List lvi = new ArrayList<>(); for (List l : ctxVars) { - for (RefinedVariable var : l) { - lvi.add(var); - } + lvi.addAll(l); } return lvi; } @@ -211,11 +185,11 @@ public List getAllVariables() { public List getAllVariablesWithSupertypes() { List lvi = new ArrayList<>(); for (RefinedVariable rv : getAllVariables()) { - if (rv.getSuperTypes().size() > 0) + if (!rv.getSuperTypes().isEmpty()) lvi.add(rv); } for (RefinedVariable rv : ctxSpecificVars) { - if (rv.getSuperTypes().size() > 0) + if (!rv.getSuperTypes().isEmpty()) lvi.add(rv); } return lvi; @@ -298,18 +272,6 @@ public void addFunctionToContext(RefinedFunction f) { ctxFunctions.add(f); } - public RefinedFunction getFunction(String name, String target) { - for (RefinedFunction fi : ctxFunctions) { - if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target)) - return fi; - } - // for(RefinedFunction fi: ctxGlobalFunctions) { - // if(fi.getName().equals(name) && fi.getTargetClass().equals(target)) - // return fi; - // } - return null; - } - public RefinedFunction getFunction(String name, String target, int size) { for (RefinedFunction fi : ctxFunctions) { if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target) @@ -333,14 +295,6 @@ public void addGhostFunction(GhostFunction gh) { ghosts.add(gh); } - public boolean hasGhost(String name) { - for (GhostFunction g : ghosts) { - if (g.matches(name)) - return true; - } - return false; - } - public List getGhosts() { return ghosts; } @@ -387,13 +341,10 @@ public String toString() { for (List l : ctxVars) { sb.append("{"); for (RefinedVariable var : l) { - sb.append(var.toString() + "; "); + sb.append(var.toString()).append("; "); } sb.append("}\n"); } - // sb.append("\n############Global Functions:############\n"); - // for(RefinedFunction f : ctxGlobalFunctions) - // sb.append(f.toString()); sb.append("\n############Functions:############\n"); for (RefinedFunction f : ctxFunctions) sb.append(f.toString()); @@ -406,10 +357,5 @@ public String toString() { public Variable getVariableFromInstance(VariableInstance vi) { return vi.getParent().orElse(null); - // for(List lv: ctxVars) - // for(RefinedVariable v: lv) - // if(v instanceof Variable && ((Variable)v).hasInstance(vi)) - // return (Variable)v; - // return null; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java index 769f4680..50a4f548 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java @@ -9,57 +9,55 @@ public class GhostFunction { - private String name; - private List> param_types; - private CtTypeReference return_type; - private String prefix; + private final String name; + private final List> paramTypes; + private final CtTypeReference returnType; + private final String prefix; public GhostFunction(GhostDTO f, Factory factory, String prefix) { String klass = this.getParentClassName(prefix); - this.name = f.getName(); - this.return_type = Utils.getType(f.getReturn_type().equals(klass) ? prefix : f.getReturn_type(), factory); - this.param_types = new ArrayList<>(); + this.name = f.name(); + this.returnType = Utils.getType(f.returnType().equals(klass) ? prefix : f.returnType(), factory); + this.paramTypes = new ArrayList<>(); this.prefix = prefix; - for (String t : f.getParam_types()) { - this.param_types.add(Utils.getType(t.equals(klass) ? prefix : t, factory)); + for (String t : f.paramTypes()) { + this.paramTypes.add(Utils.getType(t.equals(klass) ? prefix : t, factory)); } } - public GhostFunction(String name, List param_types, CtTypeReference return_type, Factory factory, + public GhostFunction(String name, List paramTypes, CtTypeReference returnType, Factory factory, String prefix) { String klass = this.getParentClassName(prefix); - String type = return_type.toString().equals(klass) ? prefix : return_type.toString(); + String type = returnType.toString().equals(klass) ? prefix : returnType.toString(); this.name = name; - this.return_type = Utils.getType(type, factory); - this.param_types = new ArrayList<>(); + this.returnType = Utils.getType(type, factory); + this.paramTypes = new ArrayList<>(); this.prefix = prefix; - for (int i = 0; i < param_types.size(); i++) { - String mType = param_types.get(i).toString(); - this.param_types.add(Utils.getType(mType.equals(klass) ? prefix : mType, factory)); + for (String mType : paramTypes) { + this.paramTypes.add(Utils.getType(mType.equals(klass) ? prefix : mType, factory)); } } - protected GhostFunction(String name, List> list, CtTypeReference return_type, String prefix) { + protected GhostFunction(String name, List> list, CtTypeReference returnType, String prefix) { this.name = name; - this.return_type = return_type; - this.param_types = new ArrayList<>(); - this.param_types = list; + this.returnType = returnType; + this.paramTypes = list; this.prefix = prefix; } public CtTypeReference getReturnType() { - return return_type; + return returnType; } public List> getParametersTypes() { - return param_types; + return paramTypes; } public String toString() { StringBuilder sb = new StringBuilder(); - sb.append("ghost " + return_type.toString() + " " + name + "("); - for (CtTypeReference t : param_types) { - sb.append(t.toString() + " ,"); + sb.append("ghost ").append(returnType.toString()).append(" ").append(name).append("("); + for (CtTypeReference t : paramTypes) { + sb.append(t.toString()).append(" ,"); } sb.delete(sb.length() - 2, sb.length()); sb.append(")"); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java deleted file mode 100644 index 64974bdf..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java +++ /dev/null @@ -1,28 +0,0 @@ -package liquidjava.processor.context; - -import java.util.ArrayList; -import java.util.List; -import spoon.reflect.factory.Factory; -import spoon.reflect.reference.CtTypeReference; - -public class GhostParentState extends GhostFunction { - - private ArrayList states; - - public GhostParentState(String name, List params, CtTypeReference ret, Factory factory, String prefix) { - super(name, params, ret, factory, prefix); - states = new ArrayList<>(); - } - - public void addState(GhostState s) { - states.add(s); - } - - public GhostState getFirstState() { - return states.get(0); - } - - public ArrayList getStates() { - return states; - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java index 3cdcacb7..121f0339 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java @@ -9,8 +9,8 @@ public class GhostState extends GhostFunction { private GhostFunction parent; private Predicate refinement; - public GhostState(String name, List> list, CtTypeReference return_type, String prefix) { - super(name, list, return_type, prefix); + public GhostState(String name, List> list, CtTypeReference returnType, String prefix) { + super(name, list, returnType, prefix); } public void setGhostParent(GhostFunction parent) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java index 2a8f90af..3400f5f7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java @@ -7,12 +7,12 @@ import spoon.reflect.declaration.CtElement; public class PlacementInCode { - private String text; - private SourcePosition position; + private final String text; + private final SourcePosition position; - private PlacementInCode(String t, SourcePosition s) { - this.text = t; - this.position = s; + private PlacementInCode(String text, SourcePosition pos) { + this.text = text; + this.position = pos; } public String getText() { @@ -23,24 +23,16 @@ public SourcePosition getPosition() { return position; } - public void setText(String text) { - this.text = text; - } - - public void setPosition(SourcePosition position) { - this.position = position; - } - public static PlacementInCode createPlacement(CtElement elem) { CtElement elemCopy = elem.clone(); // cleanup annotations - if (elem.getAnnotations().size() > 0) { + if (!elem.getAnnotations().isEmpty()) { for (CtAnnotation a : elem.getAnnotations()) { elemCopy.removeAnnotation(a); } } // cleanup comments - if (elem.getComments().size() > 0) { + if (!elem.getComments().isEmpty()) { for (CtComment a : elem.getComments()) { elemCopy.removeComment(a); } @@ -49,13 +41,6 @@ public static PlacementInCode createPlacement(CtElement elem) { return new PlacementInCode(elemText, elem.getPosition()); } - public String getSimplePosition() { - if (position.getFile() == null) { - return "No position provided. Possibly asking for generated code"; - } - return position.getFile().getName() + ":" + position.getLine() + ", " + position.getColumn(); - } - public String toString() { if (position.getFile() == null) { return "No position provided. Possibly asking for generated code"; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java index a597fe24..6028d521 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java @@ -78,10 +78,9 @@ public boolean equals(Object obj) { } else if (!name.equals(other.name)) return false; if (type == null) { - if (other.type != null) - return false; - } else if (!type.equals(other.type)) - return false; - return true; + return other.type == null; + } else { + return type.equals(other.type); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java index 807f4682..f1585cee 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java @@ -5,11 +5,10 @@ import java.util.Optional; import liquidjava.rj_language.Predicate; import spoon.reflect.declaration.CtElement; -import spoon.reflect.reference.CtTypeReference; public class RefinedFunction extends Refined { - private List argRefinements; + private final List argRefinements; private String targetClass; private List stateChange; private String signature; @@ -23,11 +22,6 @@ public List getArguments() { return argRefinements; } - public void addArgRefinements(String varName, CtTypeReference type, Predicate refinement) { - Variable v = new Variable(varName, type, refinement); - this.argRefinements.add(v); - } - public void addArgRefinements(Variable vi) { this.argRefinements.add(vi); } @@ -84,24 +78,9 @@ public Predicate getAllRefinements() { return c; } - /** - * Gives the Predicate for a certain parameter index and regards all the previous parameters' Predicates - * - * @param index - * - * @return - */ - public Predicate getRefinementsForParamIndex(int index) { - Predicate c = new Predicate(); - for (int i = 0; i <= index && i < argRefinements.size(); i++) - c = Predicate.createConjunction(c, argRefinements.get(i).getRefinement()); - return c; - } - public boolean allRefinementsTrue() { - boolean t = true; Predicate p = new Predicate(getRefReturn().getExpression()); - t = t && p.isBooleanTrue(); + boolean t = p.isBooleanTrue(); for (Variable v : argRefinements) { p = new Predicate(v.getRefinement().getExpression()); t = t && p.isBooleanTrue(); @@ -122,7 +101,7 @@ public void addStates(ObjectState e) { } public boolean hasStateChange() { - return stateChange.size() > 0; + return !stateChange.isEmpty(); } public List getFromStates() { @@ -149,7 +128,7 @@ public String toString() { public int hashCode() { final int prime = 31; int result = super.hashCode(); - result = prime * result + ((argRefinements == null) ? 0 : argRefinements.hashCode()); + result = prime * result + argRefinements.hashCode(); result = prime * result + ((targetClass == null) ? 0 : targetClass.hashCode()); result = prime * result + ((signature == null) ? 0 : signature.hashCode()); return result; @@ -164,10 +143,7 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; RefinedFunction other = (RefinedFunction) obj; - if (argRefinements == null) { - if (other.argRefinements != null) - return false; - } else if (!argRefinements.equals(other.argRefinements)) + if (!argRefinements.equals(other.argRefinements)) return false; if (targetClass == null) { if (other.targetClass != null) @@ -175,10 +151,9 @@ public boolean equals(Object obj) { } else if (!targetClass.equals(other.targetClass)) return false; if (signature == null) { - if (other.signature != null) - return false; - } else if (!signature.equals(other.signature)) - return false; - return true; + return other.signature == null; + } else { + return signature.equals(other.signature); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java index fe3abf11..534f8cfa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -7,7 +7,7 @@ import spoon.reflect.reference.CtTypeReference; public abstract class RefinedVariable extends Refined { - private List> supertypes; + private final List> supertypes; private PlacementInCode placementInCode; public RefinedVariable(String name, CtTypeReference type, Predicate c) { @@ -60,10 +60,9 @@ public boolean equals(Object obj) { return false; RefinedVariable other = (RefinedVariable) obj; if (supertypes == null) { - if (other.supertypes != null) - return false; - } else if (!supertypes.equals(other.supertypes)) - return false; - return true; + return other.supertypes == null; + } else { + return supertypes.equals(other.supertypes); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java index ff616db9..13f74cab 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java @@ -32,7 +32,7 @@ public Variable(String name, String location, CtTypeReference type, Predicate private void startVariables() { this.instances = new Stack<>(); - this.instances.push(new ArrayList()); + this.instances.push(new ArrayList<>()); ifCombiner = new Stack<>(); } @@ -73,16 +73,11 @@ public void addInstance(VariableInstance vi) { instances.peek().add(vi); } - public void removeLastInstance() { - if (instances.size() > 0) - instances.peek().remove(instances.size() - 1); - } - public Optional getLastInstance() { Stack> backup = new Stack<>(); - while (instances.size() > 0) { + while (!instances.isEmpty()) { List lvi = instances.peek(); - if (lvi.size() > 0) { // last list in stack has a value + if (!lvi.isEmpty()) { // last list in stack has a value reloadFromBackup(backup); return Optional.of(lvi.get(lvi.size() - 1)); } else { @@ -94,18 +89,10 @@ public Optional getLastInstance() { } private void reloadFromBackup(Stack> backup) { - while (backup.size() > 0) + while (!backup.isEmpty()) instances.add(backup.pop()); } - public boolean hasInstance(VariableInstance vi) { - for (List lv : instances) - for (VariableInstance v : lv) - if (v.equals(vi)) - return true; - return false; - } - // IFS public void newIfCombination() { ifCombiner.push(new Object[ifelseIndex + 1]); @@ -167,8 +154,7 @@ else if (has(ifbeforeIndex)) // value before and in else private boolean has(int index) { Object o = ifCombiner.peek()[index]; - boolean b = o != null && (o instanceof VariableInstance); - return b; + return (o instanceof VariableInstance); } private VariableInstance get(int index) { @@ -180,7 +166,7 @@ private VariableInstance get(int index) { * * @param nName * @param cond - * @param ifThen + * @param then * * @return */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java index 1a6daf4a..b4bebb0c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java @@ -6,7 +6,6 @@ public class VariableInstance extends RefinedVariable { - // private Predicate state; private Variable parent; public VariableInstance(String name, CtTypeReference type, Predicate c) { @@ -37,13 +36,4 @@ public void setParent(Variable p) { public Optional getParent() { return parent == null ? Optional.empty() : Optional.of(parent); } - - // public void setState(Predicate c) { - // state = c; - // } - // public Predicate getState() { - // return state; - // } - // - } 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 7b880475..ca120615 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/AliasDTO.java @@ -6,19 +6,20 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.rj_language.ast.Expression; import liquidjava.rj_language.parsing.RefinementsParser; +import spoon.reflect.declaration.CtTypeInformation; import spoon.reflect.reference.CtTypeReference; public class AliasDTO { - private String name; - private List varTypes; - private List varNames; + private final String name; + private final List varTypes; + private final List varNames; private Expression expression; private String ref; public AliasDTO(String name, List> varTypes, List varNames, Expression expression) { super(); this.name = name; - this.varTypes = varTypes.stream().map(m -> m.getQualifiedName()).collect(Collectors.toList()); + this.varTypes = varTypes.stream().map(CtTypeInformation::getQualifiedName).collect(Collectors.toList()); this.varNames = varNames; this.expression = expression; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java index 6dc9ea82..87dfb5cc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java @@ -2,28 +2,5 @@ import java.util.List; -public class GhostDTO { - - private String name; - private List param_types; - private String return_type; - - public GhostDTO(String name, List param_types, String return_type) { - super(); - this.name = name; - this.param_types = param_types; - this.return_type = return_type; - } - - public String getName() { - return name; - } - - public List getParam_types() { - return param_types; - } - - public String getReturn_type() { - return return_type; - } +public record GhostDTO(String name, List paramTypes, String returnType) { } 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 2321b1f6..bfbb8de3 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,6 +1,5 @@ package liquidjava.processor.refinement_checker; -import java.util.Arrays; import java.util.List; import java.util.Optional; @@ -27,7 +26,6 @@ public class ExternalRefinementTypeChecker extends TypeChecker { String prefix; - MethodsFunctionsChecker m; Diagnostics diagnostics = Diagnostics.getInstance(); public ExternalRefinementTypeChecker(Context context, Factory factory) { @@ -36,7 +34,6 @@ public ExternalRefinementTypeChecker(Context context, Factory factory) { @Override public void visitCtClass(CtClass ctClass) { - return; } @Override @@ -65,7 +62,7 @@ public void visitCtField(CtField f) { public void visitCtMethod(CtMethod method) { CtType targetType = factory.Type().createReference(prefix).getTypeDeclaration(); - if (targetType == null || !(targetType instanceof CtClass)) + if (!(targetType instanceof CtClass)) return; boolean isConstructor = method.getSimpleName().equals(targetType.getSimpleName()); @@ -99,7 +96,7 @@ public void visitCtMethod(CtMethod method) { protected void getGhostFunction(String value, CtElement element) throws LJError { GhostDTO f = RefinementsParser.getGhostDeclaration(value); - if (f != null && element.getParent() instanceof CtInterface) { + if (element.getParent() instanceof CtInterface) { GhostFunction gh = new GhostFunction(f, factory, prefix); context.addGhostFunction(gh); } @@ -110,7 +107,7 @@ protected Optional createStateGhost(int order, CtElement element) String klass = Utils.getSimpleName(prefix); if (klass != null) { CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; - List params = Arrays.asList(klass); + List params = List.of(klass); String name = String.format("state%d", order); GhostFunction gh = new GhostFunction(name, params, ret, factory, prefix); return Optional.of(gh); 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 d318f25e..43791ccd 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 @@ -47,7 +47,6 @@ public class RefinementTypeChecker extends TypeChecker { // This class should do the following: - // 1. Keep track of the context variable types // 2. Do type checking and inference @@ -189,8 +188,7 @@ public void visitCtAssignment(CtAssignment assignment) th String name = var.getSimpleName(); checkAssignment(name, varDecl.getType(), ex, assignment.getAssignment(), assignment, varDecl); - } else if (ex instanceof CtFieldWrite) { - CtFieldWrite fw = ((CtFieldWrite) ex); + } else if (ex instanceof CtFieldWrite fw) { CtFieldReference cr = fw.getVariable(); CtField f = fw.getVariable().getDeclaration(); String updatedVarName = String.format(Formats.THIS, cr.getSimpleName()); @@ -234,16 +232,12 @@ 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()) ); - String nname = String.format(Formats.THIS, f.getSimpleName()); + String name = String.format(Formats.THIS, f.getSimpleName()); Predicate ret = new Predicate(); if (c.isPresent()) { - ret = c.get().substituteVariable(Keys.WILDCARD, nname).substituteVariable(f.getSimpleName(), nname); + ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name); } - RefinedVariable v = context.addVarToContext(nname, f.getType(), ret, f); + RefinedVariable v = context.addVarToContext(name, f.getType(), ret, f); if (v instanceof Variable) { ((Variable) v).setLocation("this"); } @@ -274,9 +268,8 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { } else { fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); - // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE + // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE? } - super.visitCtFieldRead(fieldRead); } @@ -284,7 +277,7 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { public void visitCtVariableRead(CtVariableRead variableRead) { super.visitCtVariableRead(variableRead); CtVariable varDecl = variableRead.getVariable().getDeclaration(); - getPutVariableMetadada(variableRead, varDecl.getSimpleName()); + getPutVariableMetadata(variableRead, varDecl.getSimpleName()); } /** @@ -364,8 +357,7 @@ 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(index.toString(), Keys.WILDCARD, arrayWrite); arrayWrite.putMetadata(Keys.REFINEMENT, fp); } @@ -393,7 +385,7 @@ public void visitCtNewClass(CtNewClass newClass) { // ########################################## private void checkAssignment(String name, CtTypeReference type, CtExpression ex, CtExpression assignment, CtElement parentElem, CtElement varDecl) throws LJError { - getPutVariableMetadada(ex, name); + getPutVariableMetadata(ex, name); Predicate refinementFound = getRefinement(assignment); if (refinementFound == null) { @@ -452,18 +444,17 @@ private Predicate substituteAllVariablesForLastInstance(Predicate c) { // ########################################## /** - * @param + * Gets the variable refinement from the context and puts it as metadata in the element + * * @param elem * @param name - * Cannot be null */ - private void getPutVariableMetadada(CtElement elem, String name) { + private void getPutVariableMetadata(CtElement elem, String 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(Keys.WILDCARD), Predicate.createVar(ovi.get().getName())); } - 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 3608f23d..3b044848 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,7 @@ package liquidjava.processor.refinement_checker; import java.lang.annotation.Annotation; -import java.util.Arrays; +import java.util.Collections; import java.util.List; import java.util.Optional; @@ -66,7 +66,6 @@ public Optional getRefinementFromAnnotation(CtElement element) throws String an = ann.getActualAnnotation().annotationType().getCanonicalName(); if (an.contentEquals("liquidjava.specification.Refinement")) { String st = TypeCheckingUtils.getStringFromAnnotation(ann.getValue("value")); - // CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); ref = Optional.of(st); } else if (an.contentEquals("liquidjava.specification.RefinementPredicate")) { @@ -102,7 +101,7 @@ public void handleStateSetsFromAnnotation(CtElement element) throws LJError { } if (an.contentEquals("liquidjava.specification.Ghost")) { CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); - createStateGhost(s.getValue(), ann, an, element); + createStateGhost(s.getValue(), ann, element); } } } @@ -122,7 +121,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th } Optional og = createStateGhost(set, element); - if (!og.isPresent()) { + if (og.isEmpty()) { throw new RuntimeException("Error in creation of GhostFunction"); } GhostFunction g = og.get(); @@ -140,22 +139,18 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th GhostState gs = new GhostState(f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE, g.getPrefix()); gs.setGhostParent(g); - gs.setRefinement( - /* new OperationPredicate(new InvocationPredicate(f, THIS), "<-->", */ - Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); // open(THIS) - // -> - // state1(THIS) - // == 1 + gs.setRefinement(Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); + // open(THIS) -> state1(THIS) == 1 context.addToGhostClass(g.getParentClassName(), gs); } order++; } } - private void createStateGhost(String string, CtAnnotation ann, String an, CtElement element) + private void createStateGhost(String string, CtAnnotation ann, CtElement element) throws LJError { GhostDTO gd = RefinementsParser.getGhostDeclaration(string); - if (gd.getParam_types().size() > 0) { + if (!gd.paramTypes().isEmpty()) { throw new CustomError( "Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann); } @@ -163,10 +158,10 @@ private void createStateGhost(String string, CtAnnotation String qn = getQualifiedClassName(element); String sn = getSimpleClassName(element); context.addGhostClass(sn); - List> param = Arrays.asList(factory.Type().createReference(qn)); + List> param = Collections.singletonList(factory.Type().createReference(qn)); - CtTypeReference r = factory.Type().createReference(gd.getReturn_type()); - GhostState gs = new GhostState(gd.getName(), param, r, qn); + CtTypeReference r = factory.Type().createReference(gd.returnType()); + GhostState gs = new GhostState(gd.name(), param, r, qn); context.addToGhostClass(sn, gs); } @@ -197,7 +192,7 @@ protected Optional createStateGhost(int order, CtElement element) } if (klass != null) { CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; - List params = Arrays.asList(klass.getSimpleName()); + List params = Collections.singletonList(klass.getSimpleName()); String name = String.format("state%d", order); GhostFunction gh = new GhostFunction(name, params, ret, factory, klass.getQualifiedName()); return Optional.of(gh); @@ -207,8 +202,7 @@ protected Optional createStateGhost(int order, CtElement element) 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(); + if (element.getParent()instanceof CtClass klass) { GhostFunction gh = new GhostFunction(f, factory, klass.getQualifiedName()); context.addGhostFunction(gh); } @@ -233,7 +227,7 @@ protected void handleAlias(String value, CtElement element) throws LJError { throw new InvalidRefinementError(element, "Refinement alias must return a boolean expression", value); } - AliasWrapper aw = new AliasWrapper(a, factory, Keys.WILDCARD, context, klass, path); + AliasWrapper aw = new AliasWrapper(a, factory, klass, path); context.addAlias(aw); } } catch (SyntaxError e) { @@ -263,12 +257,11 @@ public void checkVariableRefinements(Predicate refinementFound, String simpleNam if (context.hasVariable(simpleName)) mainRV = context.getVariableByName(simpleName); - if (context.hasVariable(simpleName) && !context.getVariableByName(simpleName).getRefinement().isBooleanTrue()) + if (context.hasVariable(simpleName) && !context.getVariableByName(simpleName).getRefinement().isBooleanTrue()) { cEt = mainRV.getMainRefinement(); - else if (expectedType.isPresent()) - cEt = expectedType.get(); - else - cEt = new Predicate(); + } else { + cEt = expectedType.orElseGet(Predicate::new); + } cEt = cEt.substituteVariable(Keys.WILDCARD, simpleName); Predicate cet = cEt.substituteVariable(Keys.WILDCARD, simpleName); @@ -295,24 +288,23 @@ public void checkSMT(Predicate expectedType, CtElement element) throws LJError { public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String moreInfo) throws LJError { - vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, moreInfo, factory); + vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), target, factory); } 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) - throws LJError { - vcChecker.printSubtypingError(element, expectedType, foundType, customMessage); + public void createError(CtElement element, Predicate expectedType, Predicate foundType) throws LJError { + vcChecker.raiseSubtypingError(element, expectedType, foundType); } public void createSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { - vcChecker.printSameStateError(element, expectedType, klass); + vcChecker.raiseSameStateError(element, expectedType, klass); } public void createStateMismatchError(CtElement element, String method, Predicate found, Predicate[] expected) throws LJError { - vcChecker.printStateMismatchError(element, method, found, expected); + vcChecker.raiseStateMismatchError(element, method, found, expected); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeCheckingUtils.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeCheckingUtils.java index ed839368..5c5de261 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeCheckingUtils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeCheckingUtils.java @@ -8,14 +8,12 @@ public class TypeCheckingUtils { public static String getStringFromAnnotation(CtExpression ce) { - if (ce instanceof CtLiteral) { - CtLiteral cl = (CtLiteral) ce; + if (ce instanceof CtLiteral cl) { CtTypeReference r = ce.getType(); if (r.getSimpleName().equals("String")) return (String) cl.getValue(); - } else if (ce instanceof CtBinaryOperator) { - CtBinaryOperator cbo = (CtBinaryOperator) ce; + } else if (ce instanceof CtBinaryOperator cbo) { String l = getStringFromAnnotation(cbo.getLeftHandOperand()); String r = getStringFromAnnotation(cbo.getRightHandOperand()); return l + r; 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 5bae7e90..3636ff93 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 @@ -58,18 +58,18 @@ public void processSubtyping(Predicate expectedType, List list, CtEl } try { - smtChecking(premises, et, element.getPosition()); + smtChecking(premises, et); } catch (Exception e) { // To emit the message we use the constraints before the alias and state change - printError(e, premisesBeforeChange, expectedType, element, map); + raiseError(e, premisesBeforeChange, expectedType, element, map); } } public void processSubtyping(Predicate type, Predicate expectedType, List list, CtElement element, - String string, Factory f) throws LJError { + Factory f) throws LJError { boolean b = canProcessSubtyping(type, expectedType, list, element.getPosition(), f); if (!b) - printSubtypingError(element, expectedType, type, string); + raiseSubtypingError(element, expectedType, type); } public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List list, SourcePosition p, @@ -80,7 +80,6 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List< if (expectedType.isBooleanTrue() && type.isBooleanTrue()) return true; - // Predicate premises = joinPredicates(type, element, mainVars, lrv); TranslationTable map = new TranslationTable(); String[] s = { Keys.WILDCARD, Keys.THIS }; @@ -108,10 +107,6 @@ private List filterGhostStatesForVariables(List list, Li if (list.isEmpty()) return list; - // Collect all relevant qualified type names from involved variables and their supertypes - if (list == null || list.isEmpty()) - return list; - // Collect all relevant qualified type names (types + supertypes), keeping order and deduping Set allowedPrefixes = new java.util.LinkedHashSet<>(); Consumer collect = rv -> { @@ -171,13 +166,11 @@ private VCImplication joinPredicates(Predicate expectedType, List lrv, private void addAllDifferent(List toExpand, List from, List remove) { from.stream().filter(rv -> !toExpand.contains(rv) && !remove.contains(rv)).forEach(toExpand::add); - // for (RefinedVariable rv : from) { - // if (!toExpand.contains(rv) && !remove.contains(rv)) - // toExpand.add(rv); - // } } private List getVariables(Predicate c, String varName) { @@ -233,7 +222,7 @@ private void recAuxGetVars(RefinedVariable var, List newVars) { public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition p) throws LJError { try { - new SMTEvaluator().verifySubtype(found, expectedType, context, p); + new SMTEvaluator().verifySubtype(found, expectedType, context); } catch (TypeCheckError e) { return false; } catch (Exception e) { @@ -259,24 +248,10 @@ public boolean smtChecks(Predicate found, Predicate expectedType, SourcePosition * @param expectedType * */ - private void smtChecking(Predicate cSMT, Predicate expectedType, SourcePosition p) - throws TypeCheckError, Exception { - new SMTEvaluator().verifySubtype(cSMT, expectedType, context, p); + private void smtChecking(Predicate cSMT, Predicate expectedType) throws Exception { + new SMTEvaluator().verifySubtype(cSMT, expectedType, context); } - /** - * Change variables in constraint by their value expression in the map - * - * @param c - * @param map - * - * @return - */ - // 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); } @@ -286,13 +261,13 @@ public void removePathVariable(RefinedVariable rv) { } void removePathVariableThatIncludes(String otherVar) { - pathVariables.stream().filter(rv -> rv.getRefinement().getVariableNames().contains(otherVar)) - .collect(Collectors.toList()).forEach(pathVariables::remove); + pathVariables.stream().filter(rv -> rv.getRefinement().getVariableNames().contains(otherVar)).toList() + .forEach(pathVariables::remove); } // Errors--------------------------------------------------------------------------------------------------- - private TranslationTable createMap(CtElement element, Predicate expectedType) { + private TranslationTable createMap(Predicate expectedType) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); TranslationTable map = new TranslationTable(); @@ -300,8 +275,7 @@ private TranslationTable createMap(CtElement element, Predicate expectedType) { return map; } - protected void printSubtypingError(CtElement element, Predicate expectedType, Predicate foundType, String customMsg) - throws LJError { + protected void raiseSubtypingError(CtElement element, Predicate expectedType, Predicate foundType) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(foundType, lrv, mainVars); @@ -310,29 +284,23 @@ protected void printSubtypingError(CtElement element, Predicate expectedType, Pr throw new RefinementError(element, expectedType.getExpression(), premises.simplify(), map); } - public void printSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { - TranslationTable map = createMap(element, expectedType); + public void raiseSameStateError(CtElement element, Predicate expectedType, String klass) throws LJError { + TranslationTable map = createMap(expectedType); throw new StateConflictError(element, expectedType.getExpression(), klass, map); } - private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, + private void raiseError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, TranslationTable map) throws LJError { - LJError error = mapError(e, premisesBeforeChange, expectedType, element, map); - throw error; - } - - private LJError mapError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, - TranslationTable map) { if (e instanceof TypeCheckError) { - return new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map); + throw new RefinementError(element, expectedType.getExpression(), premisesBeforeChange.simplify(), map); } else if (e instanceof liquidjava.smt.errors.NotFoundError) { - return new NotFoundError(element, e.getMessage(), map); + throw new NotFoundError(element, e.getMessage(), map); } else { - return new CustomError(e.getMessage(), element); + throw new CustomError(e.getMessage(), element); } } - public void printStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) + public void raiseStateMismatchError(CtElement element, String method, Predicate found, Predicate[] states) throws LJError { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(found, lrv, mainVars); 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 1b642ee9..815e8e6c 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 @@ -1,18 +1,12 @@ package liquidjava.processor.refinement_checker.general_checkers; -import java.lang.annotation.Annotation; -import java.util.ArrayList; import java.util.HashMap; import java.util.List; 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; -import liquidjava.processor.context.Variable; -import liquidjava.processor.context.VariableInstance; +import liquidjava.processor.context.*; import liquidjava.processor.refinement_checker.TypeChecker; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; @@ -26,7 +20,6 @@ import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtVariableRead; -import spoon.reflect.declaration.CtAnnotation; import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtConstructor; import spoon.reflect.declaration.CtElement; @@ -39,7 +32,7 @@ public class MethodsFunctionsChecker { - private TypeChecker rtc; + private final TypeChecker rtc; public MethodsFunctionsChecker(TypeChecker rtc) { this.rtc = rtc; @@ -57,8 +50,7 @@ public void getConstructorRefinements(CtConstructor c) throws LJError { } else { f.setSignature(c.getSignature()); } - if (c.getParent() instanceof CtClass) { - CtClass klass = (CtClass) c.getParent(); + if (c.getParent()instanceof CtClass klass) { f.setClass(klass.getQualifiedName()); } rtc.getContext().addFunctionToContext(f); @@ -91,8 +83,7 @@ public void getMethodRefinements(CtMethod method) throws LJError { klass = (CtClass) method.getParent(); f.setClass(klass.getQualifiedName()); } - if (method.getParent() instanceof CtInterface) { - CtInterface inter = (CtInterface) method.getParent(); + if (method.getParent()instanceof CtInterface inter) { f.setClass(inter.getQualifiedName()); } String owner = f.getTargetClass(); @@ -147,7 +138,7 @@ private void auxGetMethodRefinements(CtMethod method, RefinedFunction rf) * Joins all the refinements from parameters and return * * @param f - * @param methodRef + * @param method * @param params * * @return Conjunction of all @@ -155,7 +146,6 @@ private void auxGetMethodRefinements(CtMethod method, RefinedFunction rf) private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, List> params) throws LJError { Predicate joint = new Predicate(); - for (CtParameter param : params) { String paramName = param.getSimpleName(); Optional oc = rtc.getRefinementFromAnnotation(param); @@ -168,26 +158,13 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, f.addArgRefinements((Variable) v); joint = Predicate.createConjunction(joint, c); } - Optional oret = rtc.getRefinementFromAnnotation(method); Predicate ret = oret.orElse(new Predicate()); ret = ret.substituteVariable("return", Keys.WILDCARD); f.setRefReturn(ret); - // rtc.context.addFunctionToContext(f); return Predicate.createConjunction(joint, ret); } - public List> getStateAnnotation(CtElement element) { - 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; - } - public void getReturnRefinements(CtReturn ret) throws LJError { CtClass c = ret.getParent(CtClass.class); String className = c.getSimpleName(); @@ -244,16 +221,6 @@ public void getInvocationRefinements(CtInvocation invocation) throws LJEr if (f != null) { // inside rtc.context checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), method.getSimpleName(), ctype); - - } else { - CtExecutable cet = invocation.getExecutable().getDeclaration(); - if (cet instanceof CtMethod) { - // CtMethod met = (CtMethod) cet; - // rtc.visitCtMethod(met); - // checkInvocationRefinements(invocation, method.getSimpleName()); - } - // rtc.visitCtMethod(method); - } } } @@ -344,7 +311,7 @@ private Map checkInvocationRefinements(CtElement invocation, Lis String viName = String.format(Formats.INSTANCE, f.getName(), rtc.getContext().getCounter()); VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(), - methodRef.substituteVariable(Keys.WILDCARD, viName), invocation); // TODO REVER!! + methodRef.substituteVariable(Keys.WILDCARD, viName), invocation); // TODO REVIEW!! if (varName != null && f.hasStateChange() && equalsThis) rtc.getContext().addRefinementInstanceToVariable(varName, viName); invocation.putMetadata(Keys.TARGET, vi); @@ -353,24 +320,19 @@ private Map checkInvocationRefinements(CtElement invocation, Lis return map; } - private Map mapInvocation(List> arguments, RefinedFunction f) { + private Map mapInvocation(List> arguments, RefinedFunction f) { Map mapInvocation = new HashMap<>(); - List> invocationParams = arguments; List functionParams = f.getArguments(); - for (int i = 0; i < invocationParams.size(); i++) { + for (int i = 0; i < arguments.size(); i++) { Variable fArg = functionParams.get(i); - CtExpression iArg = invocationParams.get(i); + CtExpression iArg = arguments.get(i); String invStr; - // if(iArg instanceof CtLiteral) - // invStr = iArg.toString(); - // else if (iArg instanceof CtFieldRead) { invStr = createVariableRepresentingArgument(iArg, fArg); - } else if (iArg instanceof CtVariableRead) { - CtVariableRead vr = (CtVariableRead) iArg; + } else if (iArg instanceof CtVariableRead vr) { Optional ovi = rtc.getContext() .getLastVariableInstance(vr.getVariable().getSimpleName()); - invStr = ovi.map(o -> o.getName()).orElse(vr.toString()); + invStr = ovi.map(Refined::getName).orElse(vr.toString()); } else // create new variable with the argument refinement invStr = createVariableRepresentingArgument(iArg, fArg); @@ -390,11 +352,10 @@ private String createVariableRepresentingArgument(CtExpression iArg, Variable return nVar; } - private void checkParameters(CtElement invocation, List> arguments, RefinedFunction f, + private void checkParameters(CtElement invocation, List> arguments, RefinedFunction f, Map map) throws LJError { - List> invocationParams = arguments; List functionParams = f.getArguments(); - for (int i = 0; i < invocationParams.size(); i++) { + for (int i = 0; i < arguments.size(); i++) { Variable fArg = functionParams.get(i); Predicate c = fArg.getMainRefinement(); c = c.substituteVariable(fArg.getName(), map.get(fArg.getName())); @@ -415,16 +376,14 @@ private void checkParameters(CtElement invocation, List> arg private void applyRefinementsToArguments(CtElement element, List> arguments, RefinedFunction f, Map map) { Context context = rtc.getContext(); - List> invocationParams = arguments; List functionParams = f.getArguments(); - for (int i = 0; i < invocationParams.size(); i++) { + for (int i = 0; i < arguments.size(); i++) { Variable fArg = functionParams.get(i); Predicate inferredRefinement = fArg.getRefinement(); - CtExpression e = invocationParams.get(i); - if (e instanceof CtVariableRead) { - CtVariableRead v = (CtVariableRead) e; + CtExpression e = arguments.get(i); + if (e instanceof CtVariableRead v) { String varName = v.getVariable().getSimpleName(); // TODO CHANGE RefinedVariable rv = context.getVariableByName(varName); String instanceName = String.format(Formats.INSTANCE, varName, context.getCounter()); @@ -433,13 +392,6 @@ private void applyRefinementsToArguments(CtElement element, List context.addInstanceToContext(instanceName, rv.getType(), inferredRefinement, element); context.addRefinementInstanceToVariable(varName, instanceName); } // TODO else's? - - // c = c.substituteVariable(fArg.getName(), map.get(fArg.getName())); - // List vars = c.getVariableNames(); - // for(String s: vars) - // if(map.containsKey(s)) - // c = c.substituteVariable(s, map.get(s)); - // rtc.checkSMT(c, invocation); } } 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 69dd190e..779d68a9 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 @@ -47,7 +47,7 @@ */ public class OperationsChecker { - private TypeChecker rtc; + private final TypeChecker rtc; public OperationsChecker(TypeChecker rtc) { this.rtc = rtc; @@ -69,17 +69,13 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr return; // Operations in annotations are not handled here if (parent instanceof CtAssignment - && ((CtAssignment) parent).getAssigned() instanceof CtVariableWrite) { - CtVariableWrite parentVar = (CtVariableWrite) ((CtAssignment) parent).getAssigned(); + && ((CtAssignment) parent).getAssigned()instanceof CtVariableWrite parentVar) { oper = getOperationRefinements(operator, parentVar, operator); } else { Predicate varLeft = getOperationRefinements(operator, left); Predicate varRight = getOperationRefinements(operator, right); oper = Predicate.createOperation(varLeft, getOperatorFromKind(operator.getKind()), varRight); - // new Predicate(String.format("(%s %s %s)", - // varLeft,,varRight)); - } String type = operator.getType().getQualifiedName(); List types = Arrays.asList(Types.IMPLEMENTED); @@ -109,15 +105,13 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro CtExpression ex = (CtExpression) operator.getOperand(); String name = Formats.FRESH; Predicate all; - if (ex instanceof CtVariableWrite) { - CtVariableWrite w = (CtVariableWrite) ex; + if (ex instanceof CtVariableWrite w) { name = w.getVariable().getSimpleName(); all = getRefinementUnaryVariableWrite(ex, operator, w, name); rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; - } else if (ex instanceof CtVariableRead) { - CtVariableRead var = (CtVariableRead) ex; + } else if (ex instanceof CtVariableRead var) { name = var.getVariable().getSimpleName(); // If the variable is the same, the refinements need to be changed try { @@ -137,20 +131,16 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro } Predicate metadata = rtc.getRefinement(ex); - String newName; - if (!name.equals(Formats.FRESH)) - newName = String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()); - else - newName = String.format(name, rtc.getContext().getCounter()); + String newName = !name.equals(Formats.FRESH) + ? String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()) + : String.format(name, rtc.getContext().getCounter()); Predicate newMeta = metadata.substituteVariable(Keys.WILDCARD, newName); Predicate unOp = getOperatorFromKind(operator.getKind(), operator); CtElement p = operator.getParent(); Predicate opS = unOp.substituteVariable(Keys.WILDCARD, newName); - if (p instanceof CtIf) - all = opS; - else - all = Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), opS); // TODO SEE IF () IN OPS IS NEEDED + all = p instanceof CtIf ? opS : Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), opS); + // TODO SEE IF () IN OPS IS NEEDED rtc.getContext().addInstanceToContext(newName, ex.getType(), newMeta, operator); operator.putMetadata(Keys.REFINEMENT, all); } @@ -182,8 +172,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtExpres */ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariableWrite parentVar, CtExpression element) throws LJError { - if (element instanceof CtFieldRead) { - CtFieldRead field = ((CtFieldRead) element); + if (element instanceof CtFieldRead field) { if (field.getVariable().getSimpleName().equals("length")) { String name = String.format(Formats.FRESH, rtc.getContext().getCounter()); rtc.getContext().addVarToContext(name, element.getType(), @@ -192,48 +181,41 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab } } - if (element instanceof CtVariableRead) { - CtVariableRead elemVar = (CtVariableRead) element; + if (element instanceof CtVariableRead elemVar) { String elemName = elemVar.getVariable().getSimpleName(); if (elemVar instanceof CtFieldRead) elemName = String.format(Formats.THIS, elemName); - Predicate elem_ref = rtc.getContext().getVariableRefinements(elemName); + Predicate elemRef = rtc.getContext().getVariableRefinements(elemName); String returnName = elemName; CtElement parent = operator.getParent(); // No need for specific values if (parent != null && !(parent instanceof CtIfImpl)) { - elem_ref = rtc.getRefinement(elemVar); + elemRef = rtc.getRefinement(elemVar); 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, + Predicate newElemRef = elemRef.substituteVariable(Keys.WILDCARD, newName); + RefinedVariable newVi = rtc.getContext().addVarToContext(newName, elemVar.getType(), newElemRef, elemVar); rtc.getContext().addSpecificVariable(newVi); returnName = newName; } - Predicate e = elem_ref.substituteVariable(Keys.WILDCARD, elemName); + Predicate e = elemRef.substituteVariable(Keys.WILDCARD, elemName); rtc.getContext().addVarToContext(elemName, elemVar.getType(), e, elemVar); return Predicate.createVar(returnName); - } else if (element instanceof CtBinaryOperator) { - CtBinaryOperator binop = (CtBinaryOperator) element; + } else if (element instanceof CtBinaryOperator binop) { Predicate right = getOperationRefinements(operator, parentVar, binop.getRightHandOperand()); Predicate left = getOperationRefinements(operator, parentVar, binop.getLeftHandOperand()); - return Predicate.createOperation(left, getOperatorFromKind(binop.getKind()), right); - // Predicate(left+" "+ getOperatorFromKind(binop.getKind()) +" "+ right); - } else if (element instanceof CtUnaryOperator) { Predicate a = (Predicate) element.getMetadata(Keys.REFINEMENT); a = a.substituteVariable(Keys.WILDCARD, ""); String s = a.toString().replace("(", "").replace(")", "").replace("==", "").replace(" ", ""); // TODO - // IMPROVE + // TODO: IMPROVE return new Predicate(String.format("(%s)", s), element); - } else if (element instanceof CtLiteral) { - CtLiteral l = (CtLiteral) element; + } else if (element instanceof CtLiteral l) { if (l.getType().getQualifiedName().equals("java.lang.String")) { // skip strings return new Predicate(); @@ -243,20 +225,19 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab return new Predicate(l.getValue().toString(), element); - } else if (element instanceof CtInvocation) { - CtInvocation inv = (CtInvocation) element; + } else if (element instanceof CtInvocation inv) { CtExecutable method = inv.getExecutable().getDeclaration(); if (method == null) - return getOperationRefinementFromExternalLib(inv, operator); + return getOperationRefinementFromExternalLib(inv); // Get function refinements with non_used variables String met = ((CtClass) method.getParent()).getQualifiedName(); // TODO check RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), met, inv.getArguments().size()); - Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!! + Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!! + // Substitute _ by the variable that we send String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); - innerRefs = innerRefs.substituteVariable(Keys.WILDCARD, newName); rtc.getContext().addVarToContext(newName, fi.getType(), innerRefs, inv); return new Predicate(newName, inv); // Return variable that represents the invocation @@ -265,8 +246,7 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab // TODO Maybe add cases } - private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtBinaryOperator operator) - throws LJError { + private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) throws LJError { CtExpression t = inv.getTarget(); if (t instanceof CtVariableRead) { @@ -280,11 +260,12 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtB String methodInClassName = typeNotParametrized + "." + simpleName; RefinedFunction fi = rtc.getContext().getFunction(methodInClassName, typeNotParametrized, inv.getArguments().size()); - Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVER!! + Predicate innerRefs = fi.getRenamedRefinements(rtc.getContext(), inv); // TODO REVIEW!! // Substitute _ by the variable that we send 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) { @@ -300,7 +281,7 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtB } /** - * Retrieves the refinements for the a variable write inside unary operation + * Retrieves the refinements for the variable write inside unary operation * * @param * @param ex @@ -333,7 +314,7 @@ private Predicate getRefinementUnaryVariableWrite(CtExpression ex, CtUnar * * @param kind * - * @return + * @return operator string */ private String getOperatorFromKind(BinaryOperatorKind kind) { return switch (kind) { @@ -356,15 +337,12 @@ private String getOperatorFromKind(BinaryOperatorKind kind) { private Predicate getOperatorFromKind(UnaryOperatorKind kind, CtElement elem) throws LJError { 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 POSTINC, PREINC -> Keys.WILDCARD + " + 1"; + case POSTDEC, 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 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 a1b5ae84..3fe01862 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 @@ -3,7 +3,6 @@ import java.util.HashMap; import java.util.List; import java.util.Optional; -import java.util.stream.Collectors; import liquidjava.diagnostics.errors.LJError; import liquidjava.processor.context.ObjectState; @@ -18,6 +17,7 @@ import spoon.reflect.declaration.CtClass; import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtParameter; +import spoon.reflect.declaration.CtTypeInformation; import spoon.reflect.reference.CtTypeReference; public class AuxHierarchyRefinementsPassage { @@ -26,11 +26,9 @@ public static void checkFunctionInSupertypes(CtClass klass, CtMethod m TypeChecker tc) throws LJError { String name = method.getSimpleName(); int size = method.getParameters().size(); - if (klass.getSuperInterfaces().size() > 0) { // implemented interfaces + if (!klass.getSuperInterfaces().isEmpty()) { // implemented interfaces Optional superFunction = functionInInterface(klass, name, size, tc); - if (superFunction.isPresent()) { - transferRefinements(superFunction.get(), f, method, tc); - } + superFunction.ifPresent(refinedFunction -> transferRefinements(refinedFunction, f, method, tc)); } if (klass.getSuperclass() != null) { // extended class CtTypeReference t = klass.getSuperclass(); @@ -85,7 +83,7 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF } else { boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); if (!ok) { - tc.createError(method, argRef, superArgRef, ""); + tc.createError(method, argRef, superArgRef); } } } @@ -117,8 +115,7 @@ static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunct static Optional functionInInterface(CtClass klass, String simpleName, int size, TypeChecker tc) { List lrf = tc.getContext().getAllMethodsWithNameSize(simpleName, size); - List st = klass.getSuperInterfaces().stream().map(p -> p.getQualifiedName()) - .collect(Collectors.toList()); + List st = klass.getSuperInterfaces().stream().map(CtTypeInformation::getQualifiedName).toList(); for (RefinedFunction rf : lrf) { if (st.contains(rf.getTargetClass())) return Optional.of(rf); // TODO only works for 1 interface @@ -142,16 +139,15 @@ private static void transferStateRefinements(RefinedFunction superFunction, Refi String thisName = String.format(Formats.FRESH, tc.getContext().getCounter()); createVariableInContext(thisName, tc, subFunction, superFunction, method.getParameters().get(i)); - Predicate superConst = matchVariableNames(Keys.THIS, thisName, superState.getFrom()); - Predicate subConst = matchVariableNames(Keys.THIS, thisName, superFunction, subFunction, - subState.getFrom()); + Predicate superConst = matchVariableNames(thisName, superState.getFrom()); + Predicate subConst = matchVariableNames(thisName, superFunction, subFunction, subState.getFrom()); // fromSup <: fromSub <==> fromSup is sub type and fromSub is expectedType tc.checkStateSMT(superConst, subConst, method, "FROM State from Superclass must be subtype of FROM State from Subclass"); - superConst = matchVariableNames(Keys.THIS, thisName, superState.getTo()); - subConst = matchVariableNames(Keys.THIS, thisName, superFunction, subFunction, subState.getTo()); + superConst = matchVariableNames(thisName, superState.getTo()); + subConst = matchVariableNames(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"); @@ -166,25 +162,22 @@ private static void createVariableInContext(String thisName, TypeChecker tc, Ref RefinedVariable rv = tc.getContext().addVarToContext(thisName, Utils.getType(subFunction.getTargetClass(), tc.getFactory()), new Predicate(), ctParameter); rv.addSuperType(Utils.getType(superFunction.getTargetClass(), tc.getFactory())); // TODO: change: this only - // works - // for one superclass - + // works for one superclass } /** * Changes all variable names in c to match the names of superFunction * - * @param fromName * @param thisName * @param superFunction * @param subFunction * @param c - * + * * @return */ - private static Predicate matchVariableNames(String fromName, String thisName, RefinedFunction superFunction, + private static Predicate matchVariableNames(String thisName, RefinedFunction superFunction, RefinedFunction subFunction, Predicate c) { - Predicate nc = c.substituteVariable(fromName, thisName); + Predicate nc = c.substituteVariable(Keys.THIS, thisName); List superArgs = superFunction.getArguments(); List subArgs = subFunction.getArguments(); for (int i = 0; i < subArgs.size(); i++) { @@ -193,7 +186,7 @@ private static Predicate matchVariableNames(String fromName, String thisName, Re return nc; } - private static Predicate matchVariableNames(String fromName, String thisName, Predicate c) { - return c.substituteVariable(fromName, thisName); + private static Predicate matchVariableNames(String thisName, Predicate c) { + return c.substituteVariable(Keys.THIS, thisName); } } 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 6d6de6d1..44164419 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 @@ -41,7 +41,7 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, throw new IllegalConstructorTransitionError(from); } } - setConstructorStates(f, an, tc, c); // f.setState(an, context.getGhosts(), c); + setConstructorStates(f, an, c); } else { setDefaultState(f, tc); } @@ -52,12 +52,11 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, * * @param f * @param anns - * @param tc * @param element */ @SuppressWarnings({ "rawtypes" }) private static void setConstructorStates(RefinedFunction f, List> anns, - TypeChecker tc, CtElement element) throws LJError { + CtElement element) throws LJError { List l = new ArrayList<>(); for (CtAnnotation an : anns) { Map m = an.getAllValues(); @@ -116,13 +115,11 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { private static List getDifferentSets(TypeChecker tc, String klassQualified) { List sets = new ArrayList<>(); List l = getGhostStatesFor(klassQualified, tc); - if (l != null) { - for (GhostState g : l) { - if (g.getParent() == null) { - sets.add(g); - } else if (!sets.contains(g.getParent())) { - sets.add(g.getParent()); - } + for (GhostState g : l) { + if (g.getParent() == null) { + sets.add(g); + } else if (!sets.contains(g.getParent())) { + sets.add(g.getParent()); } } return sets; @@ -141,8 +138,6 @@ public static void handleMethodState(CtMethod method, RefinedFunction f, Type if (!an.isEmpty()) { setFunctionStates(f, an, tc, method, prefix); } - // f.setState(an, context.getGhosts(), method); - } /** @@ -201,8 +196,8 @@ private static ObjectState getStates(CtAnnotation ctAnnota * * @return the created predicate */ - private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass, - TypeChecker tc, CtElement e, boolean isTo, String prefix) throws LJError { + private static Predicate createStatePredicate(String value, String targetClass, TypeChecker tc, CtElement e, + boolean isTo, String prefix) throws LJError { Predicate p = new Predicate(value, e, prefix); if (!p.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(e, "State refinement transition must be a boolean expression", value); @@ -239,11 +234,11 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) for (GhostState g : gs) { if (g.getParent() == null && sets.contains(g)) { sets.remove(g); - } else if (g.getParent() != null && sets.contains(g.getParent())) { + } else if (g.getParent() != null) { sets.remove(g.getParent()); } } - return addOldStates(p, Predicate.createVar(Keys.THIS), sets, tc); + return addOldStates(p, Predicate.createVar(Keys.THIS), sets); } /** @@ -286,11 +281,10 @@ private static List getGhostStatesFor(String qualifiedClass, TypeChe * @param p * @param th * @param sets - * @param tc - * + * * @return updated predicate */ - private static Predicate addOldStates(Predicate p, Predicate th, List sets, TypeChecker tc) { + private static Predicate addOldStates(Predicate p, Predicate th, List sets) { Predicate c = p; for (GhostFunction gf : sets) { Predicate eq = Predicate.createEquals( // gf.name == old(gf.name(this)) @@ -314,17 +308,13 @@ private static Predicate addOldStates(Predicate p, Predicate th, List map, CtConstructorCall ctConstructorCall) { List oc = f.getToStates(); - if (oc.size() > 0) { // && !oc.get(0).isBooleanTrue()) - // ctConstructorCall.putMetadata(stateKey, oc.get(0)); + if (!oc.isEmpty()) { Predicate c = oc.get(0); for (String k : map.keySet()) { c = c.substituteVariable(k, map.get(k)); } ctConstructorCall.putMetadata(refKey, c); - // add maping to oc.get(0)-HERE - } else if (oc.size() > 1) { - // TODO: Proper Exception - throw new RuntimeException("Constructor can only have one to state, not multiple."); + // add mapping to oc.get(0)-HERE } } @@ -352,16 +342,15 @@ public static void addStateRefinements(TypeChecker tc, String varName, CtExpress * @param tc * @param f * @param target2 - * @param target2 * @param map * @param invocation */ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpression target2, Map map, CtElement invocation) throws LJError { String parentTargetName = searchFistVariableTarget(tc, target2, invocation); - VariableInstance target = getTarget(tc, invocation); + VariableInstance target = getTarget(invocation); if (target != null) { - if (f.hasStateChange() && f.getFromStates().size() > 0) { + if (f.hasStateChange() && !f.getFromStates().isEmpty()) { changeState(tc, target, f.getAllStates(), parentTargetName, map, invocation); } if (!f.hasStateChange()) { @@ -394,20 +383,17 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L } String parentTargetName = ((CtVariableRead) fw.getTarget()).getVariable().getSimpleName(); - Optional invocation_callee = tc.getContext().getLastVariableInstance(parentTargetName); + Optional invocationCallee = tc.getContext().getLastVariableInstance(parentTargetName); - if (!invocation_callee.isPresent()) { + if (invocationCallee.isEmpty()) { return; } - VariableInstance vi = invocation_callee.get(); + VariableInstance vi = invocationCallee.get(); String instanceName = vi.getName(); Predicate prevState = vi.getRefinement().substituteVariable(Keys.WILDCARD, instanceName) .substituteVariable(parentTargetName, instanceName); - // StateRefinement(from="true", to="n(this)=this#n") - // ObjectState stateChange = getStates(ann, rf, tc, transitionMethod); - ObjectState stateChange = new ObjectState(); String prefix = field.getDeclaringType().getQualifiedName(); Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, prefix); @@ -429,7 +415,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L Predicate transitionedState = stateChange.getTo().substituteVariable(Keys.WILDCARD, newInstanceName) .substituteVariable(Keys.THIS, newInstanceName); - transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName, tc); + transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName); // update of stata of new instance of this#n#(whatever it was + 1) VariableInstance vi2 = (VariableInstance) tc.getContext().addInstanceToContext(newInstanceName, vi.getType(), @@ -458,24 +444,17 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L * @param name * @param map * @param invocation - * - * @return */ - private static Predicate changeState(TypeChecker tc, VariableInstance vi, - /* RefinedFunction f */ List stateChanges, String name, Map map, - CtElement invocation) throws LJError { + private static void changeState(TypeChecker tc, VariableInstance vi, List stateChanges, String name, + Map map, CtElement invocation) throws LJError { if (vi.getRefinement() == null) { - return new Predicate(); + return; } String instanceName = vi.getName(); Predicate prevState = vi.getRefinement().substituteVariable(Keys.WILDCARD, instanceName) .substituteVariable(name, instanceName); - // List stateChanges = f.getAllStates(); - boolean found = false; - // if(los.size() > 1) - // assertFalse("Change state only working for one method with one state",true); for (ObjectState stateChange : stateChanges) { // TODO: only working for 1 state annotation if (found) { break; @@ -500,10 +479,10 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, for (String s : map.keySet()) { transitionedState = transitionedState.substituteVariable(s, map.get(s)); } - transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName, tc); + transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName); // update of stata of new instance of this#n#(whatever it was + 1) addInstanceWithState(tc, name, newInstanceName, vi, transitionedState, invocation); - return transitionedState; + return; } } if (!found) { // Reaches the end of stateChange no matching states @@ -512,11 +491,10 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi, String simpleInvocation = invocation.toString(); tc.createStateMismatchError(invocation, simpleInvocation, prevState, states); } - return new Predicate(); } - private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName, - TypeChecker tc) { + private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, + String newInstanceName) { return transitionedState.changeOldMentions(instanceName, newInstanceName); } @@ -527,20 +505,16 @@ private static Predicate checkOldMentions(Predicate transitionedState, String in * @param variableInstance * @param name * @param invocation - * - * @return */ - private static Predicate sameState(TypeChecker tc, VariableInstance variableInstance, String name, - CtElement invocation) throws LJError { + private static void sameState(TypeChecker tc, VariableInstance variableInstance, String name, 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) .substituteVariable(variableInstance.getName(), newInstanceName); addInstanceWithState(tc, name, newInstanceName, variableInstance, c, invocation); - return c; } - return new Predicate(); } /** @@ -552,14 +526,11 @@ private static Predicate sameState(TypeChecker tc, VariableInstance variableInst * @param prevInstance * @param transitionedState * @param invocation - * - * @return */ - private static String addInstanceWithState(TypeChecker tc, String superName, String name2, + private static void addInstanceWithState(TypeChecker tc, String superName, String name2, VariableInstance prevInstance, Predicate transitionedState, CtElement invocation) throws LJError { VariableInstance vi2 = (VariableInstance) tc.getContext().addInstanceToContext(name2, prevInstance.getType(), prevInstance.getRefinement(), invocation); - // vi2.setState(transitionedState); vi2.setRefinement(transitionedState); Context ctx = tc.getContext(); if (ctx.hasVariable(superName)) { @@ -577,9 +548,7 @@ private static String addInstanceWithState(TypeChecker tc, String superName, Str tc.getContext().addRefinementInstanceToVariable(superName, name2); } } - invocation.putMetadata(Keys.TARGET, vi2); - return name2; } /** @@ -590,14 +559,13 @@ private static String addInstanceWithState(TypeChecker tc, String superName, Str * @return the name of the parent target */ static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElement invocation) { - if (target2 instanceof CtVariableRead) { + if (target2 instanceof CtVariableRead v) { // v--------- field read - // means invokation is in a form of `t.method(args)` - CtVariableRead v = (CtVariableRead) target2; + // means invocation is in a form of `t.method(args)` String name = v.getVariable().getSimpleName(); - Optional invocation_callee = tc.getContext().getLastVariableInstance(name); - if (invocation_callee.isPresent()) { - invocation.putMetadata(Keys.TARGET, invocation_callee.get()); + Optional invocationCallee = tc.getContext().getLastVariableInstance(name); + if (invocationCallee.isPresent()) { + invocation.putMetadata(Keys.TARGET, invocationCallee.get()); } else if (target2.getMetadata(Keys.TARGET) == null) { RefinedVariable var = tc.getContext().getVariableByName(name); String nName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter()); @@ -609,17 +577,17 @@ static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElem return name; } else if (target2.getMetadata(Keys.TARGET) != null) { - // invokation is in + // invocation is in // who did put the metadata here then? - VariableInstance target2_vi = (VariableInstance) target2.getMetadata(Keys.TARGET); - Optional v = target2_vi.getParent(); - invocation.putMetadata(Keys.TARGET, target2_vi); - return v.map(Refined::getName).orElse(target2_vi.getName()); + VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET); + Optional v = target2Vi.getParent(); + invocation.putMetadata(Keys.TARGET, target2Vi); + return v.map(Refined::getName).orElse(target2Vi.getName()); } return null; } - static VariableInstance getTarget(TypeChecker tc, CtElement invocation) { + static VariableInstance getTarget(CtElement invocation) { if (invocation.getMetadata(Keys.TARGET) != null) { return (VariableInstance) invocation.getMetadata(Keys.TARGET); } 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 be9db207..36dfc6aa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/BuiltinFunctionPredicate.java @@ -13,8 +13,7 @@ public static BuiltinFunctionPredicate length(String param, CtElement elem) thro return new BuiltinFunctionPredicate(elem, "length", param); } - public static BuiltinFunctionPredicate addToIndex(String array, String index, String value, CtElement elem) - throws LJError { + public static BuiltinFunctionPredicate addToIndex(String index, String value, CtElement elem) 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 6d10d4ec..ed490839 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -10,6 +10,7 @@ import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; +import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; import liquidjava.processor.facade.AliasDTO; import liquidjava.rj_language.ast.BinaryExpression; @@ -54,7 +55,6 @@ public Predicate() { * * @param ref * @param element - * @param e */ public Predicate(String ref, CtElement element) throws LJError { this(ref, element, element.getParent(CtType.class).getQualifiedName()); @@ -65,7 +65,6 @@ public Predicate(String ref, CtElement element) throws LJError { * * @param ref * @param element - * @param e * @param prefix */ public Predicate(String ref, CtElement element, String prefix) throws LJError { @@ -126,7 +125,7 @@ public List getVariableNames() { public List getStateInvocations(List lgs) { if (lgs == null) return new ArrayList<>(); - List all = lgs.stream().map(p -> p.getQualifiedName()).collect(Collectors.toList()); + List all = lgs.stream().map(GhostFunction::getQualifiedName).collect(Collectors.toList()); List toAdd = new ArrayList<>(); exp.getStateInvocations(toAdd, all); @@ -150,29 +149,6 @@ public Predicate changeOldMentions(String previousName, String newName) { return new Predicate(e); } - public List getOldVariableNames() { - List ls = new ArrayList<>(); - expressionGetOldVariableNames(this.exp, ls); - return ls; - } - - private void expressionGetOldVariableNames(Expression exp, List ls) { - if (exp instanceof FunctionInvocation) { - FunctionInvocation fi = (FunctionInvocation) exp; - if (fi.getName().equals(Keys.OLD)) { - List le = fi.getArgs(); - for (Expression e : le) { - if (e instanceof Var) - ls.add(((Var) e).getName()); - } - } - } - if (exp.hasChildren()) { - for (var ch : exp.getChildren()) - expressionGetOldVariableNames(ch, ls); - } - } - public Predicate changeStatesToRefinements(List ghostState, String[] toChange) throws LJError { Map nameRefinementMap = new HashMap<>(); for (GhostState gs : ghostState) { @@ -212,7 +188,7 @@ public ValDerivationNode simplify() { } private static boolean isBooleanLiteral(Expression expr, boolean value) { - return expr instanceof LiteralBoolean && ((LiteralBoolean) expr).isBooleanTrue() == value; + return expr instanceof LiteralBoolean && expr.isBooleanTrue() == value; } public static Predicate createConjunction(Predicate c1, Predicate c2) { @@ -228,19 +204,6 @@ public static Predicate createConjunction(Predicate c1, Predicate c2) { return new Predicate(new BinaryExpression(c1.getExpression(), Ops.AND, c2.getExpression())); } - public static Predicate createDisjunction(Predicate c1, Predicate c2) { - // simplification: (false || x) = x, (true || x) = true - if (isBooleanLiteral(c1.getExpression(), false)) - return c2; - if (isBooleanLiteral(c2.getExpression(), false)) - return c1; - if (isBooleanLiteral(c1.getExpression(), true)) - return c1; - if (isBooleanLiteral(c2.getExpression(), true)) - return c2; - 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(), Ops.EQ, c2.getExpression())); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java index 74e54cce..13b68ba1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java @@ -30,7 +30,7 @@ public T accept(ExpressionVisitor visitor) throws Exception { @Override public String toString() { - return name + "(" + getArgs().stream().map(p -> p.toString()).collect(Collectors.joining(", ")) + ")"; + return name + "(" + getArgs().stream().map(Expression::toString).collect(Collectors.joining(", ")) + ")"; } @Override @@ -88,10 +88,9 @@ public boolean equals(Object obj) { } else if (!getArgs().equals(other.getArgs())) return false; if (name == null) { - if (other.name != null) - return false; - } else if (!name.equals(other.name)) - return false; - return true; + return other.name == null; + } else { + return name.equals(other.name); + } } } 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 2cc30c6b..9e25e644 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 @@ -6,7 +6,7 @@ public class BinaryExpression extends Expression { - private String op; + private final String op; public BinaryExpression(Expression e1, String op, Expression e2) { this.op = op; @@ -109,10 +109,9 @@ public boolean equals(Object obj) { } else if (!getSecondOperand().equals(other.getSecondOperand())) return false; if (op == null) { - if (other.op != null) - return false; - } else if (!op.equals(other.op)) - return false; - return true; + return other.op == null; + } else { + return op.equals(other.op); + } } } 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 7a7bf0ab..48441251 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 @@ -51,7 +51,7 @@ public List getChildren() { } public boolean hasChildren() { - return children.size() > 0; + return !children.isEmpty(); } public void setChild(int index, Expression element) { @@ -114,15 +114,15 @@ private void auxSubstitute(Expression from, Expression to) { /** * Substitutes the function call with the given parameter to the expression e * - * @param s - * @param e + * @param functionName + * @param parameters + * @param sub */ public void substituteFunction(String functionName, List parameters, Expression sub) { if (hasChildren()) for (int i = 0; i < children.size(); i++) { Expression exp = children.get(i); - if (exp instanceof FunctionInvocation) { - FunctionInvocation fi = (FunctionInvocation) exp; + if (exp instanceof FunctionInvocation fi) { if (fi.name.equals(functionName) && fi.argumentsEqual(parameters)) { // substitute by sub in parent setChild(i, sub); @@ -134,14 +134,12 @@ public void substituteFunction(String functionName, List parameters, public Expression substituteState(Map subMap, String[] toChange) { Expression e = clone(); - if (this instanceof FunctionInvocation) { - FunctionInvocation fi = (FunctionInvocation) this; + if (this instanceof FunctionInvocation fi) { String key = fi.name; String simple = Utils.getSimpleName(key); boolean has = subMap.containsKey(key) || subMap.containsKey(simple); - if (has && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object + if (has && fi.children.size() == 1 && fi.children.get(0)instanceof Var v) { // object // state - Var v = (Var) fi.children.get(0); Expression sub = (subMap.containsKey(key) ? subMap.get(key) : subMap.get(simple)).clone(); for (String s : toChange) { sub = sub.substitute(new Var(s), v); @@ -158,14 +156,12 @@ private void auxSubstituteState(Map subMap, String[] toChang if (hasChildren()) { for (int i = 0; i < children.size(); i++) { Expression exp = children.get(i); - if (exp instanceof FunctionInvocation) { - FunctionInvocation fi = (FunctionInvocation) exp; + if (exp instanceof FunctionInvocation fi) { String key = fi.name; String simple = Utils.getSimpleName(key); boolean has = subMap.containsKey(key) || subMap.containsKey(simple); - if (has && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object + if (has && fi.children.size() == 1 && fi.children.get(0)instanceof Var v) { // object // state - Var v = (Var) fi.children.get(0); Expression sub = (subMap.containsKey(key) ? subMap.get(key) : subMap.get(simple)).clone(); for (String s : toChange) { sub = sub.substitute(new Var(s), v); @@ -181,8 +177,7 @@ private void auxSubstituteState(Map subMap, String[] toChang public Expression changeAlias(Map alias, Context ctx, Factory f) throws Exception { Expression e = clone(); - if (this instanceof AliasInvocation) { - AliasInvocation ai = (AliasInvocation) this; + if (this instanceof AliasInvocation ai) { if (alias.containsKey(ai.name)) { // object state AliasDTO dto = alias.get(ai.name); Expression sub = dto.getExpression().clone(); @@ -209,8 +204,7 @@ public Expression changeAlias(Map alias, Context ctx, Factory private void auxChangeAlias(Map alias, Context ctx, Factory f) throws Exception { if (hasChildren()) for (int i = 0; i < children.size(); i++) { - if (children.get(i) instanceof AliasInvocation) { - AliasInvocation ai = (AliasInvocation) children.get(i); + if (children.get(i)instanceof AliasInvocation ai) { if (!alias.containsKey(ai.name)) throw new Exception("Alias '" + ai.getName() + "' not found"); AliasDTO dto = alias.get(ai.name); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java index 44d91a75..f4dc3b9a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java @@ -36,7 +36,7 @@ public T accept(ExpressionVisitor visitor) throws Exception { @Override public String toString() { - return name + "(" + getArgs().stream().map(p -> p.toString()).collect(Collectors.joining(",")) + ")"; + return name + "(" + getArgs().stream().map(Expression::toString).collect(Collectors.joining(",")) + ")"; } @Override @@ -117,10 +117,9 @@ public boolean equals(Object obj) { } else if (!getArgs().equals(other.getArgs())) return false; if (name == null) { - if (other.name != null) - return false; - } else if (!name.equals(other.name)) - return false; - return true; + return other.name == null; + } else { + return name.equals(other.name); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java index f2517fb2..24e45fb4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java @@ -66,10 +66,9 @@ public boolean equals(Object obj) { return false; GroupExpression other = (GroupExpression) obj; if (getExpression() == null) { - if (other.getExpression() != null) - return false; - } else if (!getExpression().equals(other.getExpression())) - return false; - return true; + return other.getExpression() == null; + } else { + return getExpression().equals(other.getExpression()); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java index 6090c894..5b72ce6a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java @@ -94,10 +94,9 @@ public boolean equals(Object obj) { } else if (!getElse().equals(other.getElse())) return false; if (getThen() == null) { - if (other.getThen() != null) - return false; - } else if (!getThen().equals(other.getThen())) - return false; - return true; + return other.getThen() == null; + } else { + return getThen().equals(other.getThen()); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java index 85127fff..8da1091c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java @@ -33,7 +33,6 @@ public void getVariableNames(List toAdd) { @Override public void getStateInvocations(List toAdd, List all) { // end leaf - } @Override @@ -63,8 +62,6 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; LiteralBoolean other = (LiteralBoolean) obj; - if (value != other.value) - return false; - return true; + return value == other.value; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java index 582ecd92..993c177b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java @@ -6,7 +6,7 @@ public class LiteralInt extends Expression { - private int value; + private final int value; public LiteralInt(int v) { value = v; @@ -32,13 +32,11 @@ public int getValue() { @Override public void getVariableNames(List toAdd) { // end leaf - } @Override public void getStateInvocations(List toAdd, List all) { // end leaf - } @Override @@ -68,8 +66,6 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; LiteralInt other = (LiteralInt) obj; - if (value != other.value) - return false; - return true; + return value == other.value; } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java index c80bf750..7913438d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java @@ -6,7 +6,7 @@ public class LiteralReal extends Expression { - private double value; + private final double value; public LiteralReal(double v) { value = v; @@ -32,13 +32,11 @@ public double getValue() { @Override public void getVariableNames(List toAdd) { // end leaf - } @Override public void getStateInvocations(List toAdd, List all) { // end leaf - } @Override @@ -55,9 +53,7 @@ public boolean isBooleanTrue() { public int hashCode() { final int prime = 31; int result = 1; - long temp; - temp = Double.doubleToLongBits(value); - result = prime * result + (int) (temp ^ (temp >>> 32)); + result = prime * result + Double.hashCode(value); return result; } @@ -70,8 +66,6 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; LiteralReal other = (LiteralReal) obj; - if (Double.doubleToLongBits(value) != Double.doubleToLongBits(other.value)) - return false; - return true; + return Double.doubleToLongBits(value) == Double.doubleToLongBits(other.value); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java index 38577671..1382535c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java @@ -5,7 +5,8 @@ import liquidjava.rj_language.visitors.ExpressionVisitor; public class LiteralString extends Expression { - private String value; + + private final String value; public LiteralString(String v) { value = v; @@ -58,10 +59,9 @@ public boolean equals(Object obj) { return false; LiteralString other = (LiteralString) obj; if (value == null) { - if (other.value != null) - return false; - } else if (!value.equals(other.value)) - return false; - return true; + return other.value == null; + } else { + return value.equals(other.value); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java index 82218ec3..b805df84 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java @@ -6,7 +6,7 @@ public class UnaryExpression extends Expression { - private String op; + private final String op; public UnaryExpression(String op, Expression e) { this.op = op; @@ -80,10 +80,9 @@ public boolean equals(Object obj) { } else if (!getExpression().equals(other.getExpression())) return false; if (op == null) { - if (other.op != null) - return false; - } else if (!op.equals(other.op)) - return false; - return true; + return other.op == null; + } else { + return op.equals(other.op); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java index 2ab08d4f..e89365c6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java @@ -6,7 +6,7 @@ public class Var extends Expression { - private String name; + private final String name; public Var(String name) { this.name = name; @@ -64,10 +64,9 @@ public boolean equals(Object obj) { return false; Var other = (Var) obj; if (name == null) { - if (other.name != null) - return false; - } else if (!name.equals(other.name)) - return false; - return true; + return other.name == null; + } else { + return name.equals(other.name); + } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java index 4bcf17d4..764793e0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java @@ -22,12 +22,6 @@ public class TypeInfer { - public static boolean checkCompatibleType(Expression e1, Expression e2, Context ctx, Factory factory) { - Optional> t1 = getType(ctx, factory, e1); - Optional> t2 = getType(ctx, factory, e2); - return t1.isPresent() && t2.isPresent() && t1.get().equals(t2.get()); - } - public static boolean checkCompatibleType(String type, Expression e, Context ctx, Factory factory) { Optional> t1 = getType(ctx, factory, e); CtTypeReference t2 = Utils.getType(type, factory); @@ -44,7 +38,7 @@ else if (e instanceof LiteralReal) else if (e instanceof LiteralBoolean) return boolType(factory); else if (e instanceof Var) - return varType(ctx, factory, (Var) e); + return varType(ctx, (Var) e); else if (e instanceof UnaryExpression) return unaryType(ctx, factory, (UnaryExpression) e); else if (e instanceof Ite) @@ -54,14 +48,14 @@ else if (e instanceof BinaryExpression) else if (e instanceof GroupExpression) return getType(ctx, factory, ((GroupExpression) e).getExpression()); else if (e instanceof FunctionInvocation) - return functionType(ctx, factory, (FunctionInvocation) e); + return functionType(ctx, (FunctionInvocation) e); else if (e instanceof AliasInvocation) return boolType(factory); return Optional.empty(); } - private static Optional> varType(Context ctx, Factory factory, Var v) { + private static Optional> varType(Context ctx, Var v) { String name = v.getName(); if (!ctx.hasVariable(name)) return Optional.empty(); @@ -83,7 +77,7 @@ else if (e.isBooleanOperation()) { // >, >=, <, <=, ==, != } else if (e.isArithmeticOperation()) { Optional> t1 = getType(ctx, factory, e.getFirstOperand()); Optional> t2 = getType(ctx, factory, e.getSecondOperand()); - if (!t1.isPresent() || !t2.isPresent()) + if (t1.isEmpty() || t2.isEmpty()) return Optional.empty(); if (t1.get().equals(t2.get())) return t1; @@ -91,12 +85,12 @@ else if (e.isBooleanOperation()) { // >, >=, <, <=, ==, != throw new NotImplementedException( "To implement in TypeInfer: Binary type, arithmetic with different arg types"); } - return null; + return Optional.empty(); } - private static Optional> functionType(Context ctx, Factory factory, FunctionInvocation e) { + private static Optional> functionType(Context ctx, FunctionInvocation e) { Optional gh = ctx.getGhosts().stream().filter(g -> g.matches(e.getName())).findAny(); - return gh.map(i -> i.getReturnType()); + return gh.map(GhostFunction::getReturnType); } private static Optional> boolType(Factory factory) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java index 0d5fe242..b52f8eb7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantFolding.java @@ -26,8 +26,7 @@ public static ValDerivationNode fold(ValDerivationNode node) { if (exp instanceof UnaryExpression) return foldUnary(node); - if (exp instanceof GroupExpression) { - GroupExpression group = (GroupExpression) exp; + if (exp instanceof GroupExpression group) { if (group.getChildren().size() == 1) { return fold(new ValDerivationNode(group.getChildren().get(0), node.getOrigin())); } @@ -45,9 +44,8 @@ private static ValDerivationNode foldBinary(ValDerivationNode node) { // fold child nodes ValDerivationNode leftNode; ValDerivationNode rightNode; - if (parent instanceof BinaryDerivationNode) { + if (parent instanceof BinaryDerivationNode binaryOrigin) { // has origin (from constant propagation) - BinaryDerivationNode binaryOrigin = (BinaryDerivationNode) parent; leftNode = fold(binaryOrigin.getLeft()); rightNode = fold(binaryOrigin.getRight()); } else { @@ -129,8 +127,8 @@ else if ((left instanceof LiteralInt && right instanceof LiteralReal) } // bool and bool else if (left instanceof LiteralBoolean && right instanceof LiteralBoolean) { - boolean l = ((LiteralBoolean) left).isBooleanTrue(); - boolean r = ((LiteralBoolean) right).isBooleanTrue(); + boolean l = left.isBooleanTrue(); + boolean r = right.isBooleanTrue(); Expression res = switch (op) { case "&&" -> new LiteralBoolean(l && r); case "||" -> new LiteralBoolean(l || r); @@ -158,9 +156,8 @@ private static ValDerivationNode foldUnary(ValDerivationNode node) { // fold child node ValDerivationNode operandNode; - if (parent instanceof UnaryDerivationNode) { + if (parent instanceof UnaryDerivationNode unaryOrigin) { // has origin (from constant propagation) - UnaryDerivationNode unaryOrigin = (UnaryDerivationNode) parent; operandNode = fold(unaryOrigin.getOperand()); } else { // no origin @@ -173,7 +170,7 @@ private static ValDerivationNode foldUnary(ValDerivationNode node) { // unary not if ("!".equals(operator) && operand instanceof LiteralBoolean) { // !true => false, !false => true - boolean value = ((LiteralBoolean) operand).isBooleanTrue(); + boolean value = operand.isBooleanTrue(); Expression res = new LiteralBoolean(!value); return new ValDerivationNode(res, new UnaryDerivationNode(operandNode, operator)); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java index a72a9b33..5c74897f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ConstantPropagation.java @@ -30,8 +30,7 @@ public static ValDerivationNode propagate(Expression exp) { private static ValDerivationNode propagateRecursive(Expression exp, Map subs) { // substitute variable - if (exp instanceof Var) { - Var var = (Var) exp; + if (exp instanceof Var var) { String name = var.getName(); Expression value = subs.get(name); // substitution @@ -43,8 +42,7 @@ private static ValDerivationNode propagateRecursive(Expression exp, Map resolve(Expression exp) { // if the expression is just a single equality (not a conjunction) don't extract it // this avoids creating tautologies like "1 == 1" after substitution, which are then simplified to "true" - if (exp instanceof BinaryExpression) { - BinaryExpression be = (BinaryExpression) exp; + if (exp instanceof BinaryExpression be) { if ("==".equals(be.getOperator())) { return new HashMap<>(); } @@ -34,10 +33,9 @@ public static Map resolve(Expression exp) { * Modifies the given map in place */ private static void resolveRecursive(Expression exp, Map map) { - if (!(exp instanceof BinaryExpression)) + if (!(exp instanceof BinaryExpression be)) return; - BinaryExpression be = (BinaryExpression) exp; String op = be.getOperator(); if ("&&".equals(op)) { resolveRecursive(be.getFirstOperand(), map); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java index eeb6f21d..27629839 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java @@ -45,7 +45,7 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo if (exp instanceof LiteralReal) return new JsonPrimitive(((LiteralReal) exp).getValue()); if (exp instanceof LiteralBoolean) - return new JsonPrimitive(((LiteralBoolean) exp).isBooleanTrue()); + return new JsonPrimitive(exp.isBooleanTrue()); if (exp instanceof Var) return new JsonPrimitive(((Var) exp).getName()); return new JsonPrimitive(exp.toString()); diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RJErrorListener.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RJErrorListener.java index 28c0dc82..8720d439 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RJErrorListener.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RJErrorListener.java @@ -19,7 +19,7 @@ public class RJErrorListener implements ANTLRErrorListener { public RJErrorListener() { super(); errors = 0; - msgs = new ArrayList(); + msgs = new ArrayList<>(); } @Override @@ -27,8 +27,7 @@ public void syntaxError(Recognizer recognizer, Object offendingSymbol, int String msg, RecognitionException e) { // Hint for == instead of = String hint = null; - if (e instanceof LexerNoViableAltException) { - LexerNoViableAltException l = (LexerNoViableAltException) e; + if (e instanceof LexerNoViableAltException l) { char c = l.getInputStream().toString().charAt(charPositionInLine); if (c == '=') hint = "Predicates must be compared with == instead of ="; @@ -60,9 +59,10 @@ public int getErrors() { public String getMessages() { StringBuilder sb = new StringBuilder(); String pl = errors == 1 ? "" : "s"; - sb.append("Found ").append(errors).append(" error" + pl).append(", with the message" + pl + ":\n"); + sb.append("Found ").append(errors).append(" error").append(pl).append(", with the message").append(pl) + .append(":\n"); for (String s : msgs) - sb.append("* " + s + "\n"); + sb.append("* ").append(s).append("\n"); return sb.toString(); } } 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 fe0c7d2d..4237fc4b 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 @@ -6,7 +6,6 @@ import liquidjava.processor.facade.AliasDTO; import liquidjava.utils.Pair; import org.antlr.v4.runtime.CodePointCharStream; -import org.antlr.v4.runtime.TokenStreamRewriter; import org.antlr.v4.runtime.misc.Interval; import org.antlr.v4.runtime.tree.ParseTree; import rj.grammar.RJParser.AliasContext; @@ -14,7 +13,6 @@ import rj.grammar.RJParser.PredContext; public class AliasVisitor { - TokenStreamRewriter rewriter; CodePointCharStream input; public AliasVisitor(CodePointCharStream input) { @@ -29,14 +27,13 @@ public AliasVisitor(CodePointCharStream input) { * @return */ public AliasDTO getAlias(ParseTree rc) { - if (rc instanceof AliasContext) { - AliasContext ac = (AliasContext) rc; + if (rc instanceof AliasContext ac) { String name = ac.ID_UPPER().getText(); String ref = getText(ac.pred()); List> args = getArgsDecl(ac.argDeclID()); - List varNames = args.stream().map(p -> p.getSecond()).collect(Collectors.toList()); - List varTypes = args.stream().map(p -> p.getFirst()).collect(Collectors.toList()); + List varNames = args.stream().map(Pair::second).collect(Collectors.toList()); + List varTypes = args.stream().map(Pair::first).collect(Collectors.toList()); return new AliasDTO(name, varTypes, varNames, ref); } else if (rc.getChildCount() > 0) { @@ -63,7 +60,7 @@ private String getText(PredContext pred) { } private List> getArgsDecl(ArgDeclIDContext argDeclID) { - List> l = new ArrayList>(); + List> l = new ArrayList<>(); auxGetArgsDecl(argDeclID, l); return l; } 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 7eca4a33..96530499 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 @@ -198,6 +198,6 @@ else if (literalContext.INT() != null) return new LiteralInt(literalContext.INT().getText()); else if (literalContext.REAL() != null) return new LiteralReal(literalContext.REAL().getText()); - throw new NotImplementedException("Error got to unexistant literal."); + throw new NotImplementedException("Literal type not implemented"); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java index ac4c5495..6409740d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java @@ -12,16 +12,12 @@ public class GhostVisitor { public static GhostDTO getGhostDecl(ParseTree rc) { - if (rc instanceof GhostContext) { - GhostContext gc = (GhostContext) rc; + if (rc instanceof GhostContext gc) { String type = gc.type().getText(); String name = gc.ID().getText(); List> args = getArgsDecl(gc.argDecl()); - List ls = args.stream().map(m -> m.getFirst()).collect(Collectors.toList()); - if (ls == null) - ls = new ArrayList<>(); + List ls = args.stream().map(Pair::first).collect(Collectors.toList()); return new GhostDTO(name, ls, type); - // return new Triple>>(type, name, args); } else if (rc.getChildCount() > 0) { int i = rc.getChildCount(); if (i > 0) @@ -31,7 +27,7 @@ public static GhostDTO getGhostDecl(ParseTree rc) { } private static List> getArgsDecl(ArgDeclContext argDecl) { - List> l = new ArrayList>(); + List> l = new ArrayList<>(); if (argDecl != null) auxGetArgsDecl(argDecl, l); return l; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index 40c025b3..a11f0639 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -80,22 +80,22 @@ public Expr visitVar(Var var) throws Exception { } @Override - public Expr visitLiteralInt(LiteralInt lit) throws Exception { + public Expr visitLiteralInt(LiteralInt lit) { return ctx.makeIntegerLiteral(lit.getValue()); } @Override - public Expr visitLiteralBoolean(LiteralBoolean lit) throws Exception { + public Expr visitLiteralBoolean(LiteralBoolean lit) { return ctx.makeBooleanLiteral(lit.isBooleanTrue()); } @Override - public Expr visitLiteralReal(LiteralReal lit) throws Exception { + public Expr visitLiteralReal(LiteralReal lit) { return ctx.makeDoubleLiteral(lit.getValue()); } @Override - public Expr visitLiteralString(LiteralString lit) throws Exception { + public Expr visitLiteralString(LiteralString lit) { return ctx.makeString(lit.toString()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 6276a872..4bec8f9e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -9,18 +9,13 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Expression; import liquidjava.smt.errors.TypeCheckError; -import spoon.reflect.cu.SourcePosition; public class SMTEvaluator { - public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourcePosition pos) - throws TypeCheckError, Exception { + public void verifySubtype(Predicate subRef, Predicate supRef, Context c) throws Exception { // Creates a parser for our SMT-ready refinement language // Discharges the verification to z3 - Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate()); - // System.out.println("verification query: " + toVerify); // TODO remove - try { Expression exp = toVerify.getExpression(); Status s; @@ -28,14 +23,10 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c, SourceP ExpressionToZ3Visitor visitor = new ExpressionToZ3Visitor(tz3); Expr e = exp.accept(visitor); s = tz3.verifyExpression(e); - if (s.equals(Status.SATISFIABLE)) { - // System.out.println("result of SMT: Not Ok!"); throw new TypeCheckError(subRef + " not a subtype of " + supRef); } } - // System.out.println("result of SMT: Ok!"); - } catch (SyntaxException e1) { System.out.println("Could not parse: " + toVerify); e1.printStackTrace(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 36b167cc..c3fb32dc 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -51,7 +51,7 @@ private static Expr getExpr(Context z3, String name, CtTypeReference type) }; } - static void addAlias(Context z3, List alias, Map aliasTranslation) { + static void addAlias(List alias, Map aliasTranslation) { for (AliasWrapper a : alias) { aliasTranslation.put(a.getName(), a); } @@ -69,9 +69,8 @@ public static void addGhostFunctions(Context z3, List ghosts, private static void addBuiltinFunctions(Context z3, Map> funcTranslation) { funcTranslation.put("length", z3.mkFuncDecl("length", getSort(z3, "int[]"), getSort(z3, "int"))); // ERRRRRRRRRRRRO!!!!!!!!!!!!! - // System.out.println("\nWorks only for int[] now! Change in future. Ignore this - // message, it is a glorified - // todo"); + // Works only for int[] now! Change in the future + // Ignore this message, it is a glorified TODO // TODO add built-in function Sort[] s = Stream.of(getSort(z3, "int[]"), getSort(z3, "int"), getSort(z3, "int")).toArray(Sort[]::new); funcTranslation.put("addToIndex", z3.mkFuncDecl("addToIndex", s, getSort(z3, "void"))); @@ -90,7 +89,6 @@ static Sort getSort(Context z3, String sort) { 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); }; } @@ -99,15 +97,13 @@ public static void addGhostStates(Context z3, List ghostState, Map> funcTranslation) { for (GhostState g : ghostState) { addGhostFunction(z3, g, funcTranslation); - // if(g.getRefinement() != null) - // premisesToAdd.add(g.getRefinement().getExpression()); } } private static void addGhostFunction(Context z3, GhostFunction gh, Map> funcTranslation) { List> paramTypes = gh.getParametersTypes(); Sort ret = getSort(z3, gh.getReturnType().toString()); - Sort[] domain = paramTypes.stream().map(t -> t.toString()).map(t -> getSort(z3, t)).toArray(Sort[]::new); + Sort[] domain = paramTypes.stream().map(Object::toString).map(t -> getSort(z3, t)).toArray(Sort[]::new); String name = gh.getQualifiedName(); funcTranslation.put(name, z3.mkFuncDecl(name, domain, ret)); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 79eb58cd..7c091d2b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -24,33 +24,25 @@ public class TranslatorToZ3 implements AutoCloseable { - private com.microsoft.z3.Context z3 = new com.microsoft.z3.Context(); - private Map> varTranslation = new HashMap<>(); - private Map>> varSuperTypes = new HashMap<>(); - private Map aliasTranslation = new HashMap<>(); - private Map> funcTranslation = new HashMap<>(); + private final com.microsoft.z3.Context z3 = new com.microsoft.z3.Context(); + private final Map> varTranslation = new HashMap<>(); + private final Map>> varSuperTypes = new HashMap<>(); + private final Map aliasTranslation = new HashMap<>(); // this is not being used + private final Map> funcTranslation = new HashMap<>(); public TranslatorToZ3(liquidjava.processor.context.Context c) { TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation); TranslatorContextToZ3.storeVariablesSubtypes(z3, c.getAllVariablesWithSupertypes(), varSuperTypes); - TranslatorContextToZ3.addAlias(z3, c.getAlias(), aliasTranslation); + TranslatorContextToZ3.addAlias(c.getAlias(), aliasTranslation); TranslatorContextToZ3.addGhostFunctions(z3, c.getGhosts(), funcTranslation); TranslatorContextToZ3.addGhostStates(z3, c.getGhostState(), funcTranslation); } @SuppressWarnings("unchecked") - public Status verifyExpression(Expr e) throws Exception { + public Status verifyExpression(Expr e) { Solver s = z3.mkSolver(); - // s.add((BoolExpr) e.eval(this)); - // for(Expression ex: premisesToAdd) - // s.add((BoolExpr) ex.eval(this)); s.add((BoolExpr) e); - Status st = s.check(); - if (st.equals(Status.SATISFIABLE)) { - // Example of values - // System.out.println(s.getModel()); - } - return st; + return s.check(); } // #####################Literals and Variables##################### @@ -76,7 +68,7 @@ public Expr makeBooleanLiteral(boolean value) { private Expr getVariableTranslation(String name) throws Exception { if (!varTranslation.containsKey(name)) - throw new NotFoundError("Variable '" + name.toString() + "' not found"); + throw new NotFoundError("Variable '" + name + "' not found"); Expr e = varTranslation.get(name); if (e == null) e = varTranslation.get(String.format("this#%s", name)); @@ -91,9 +83,9 @@ public Expr makeVariable(String name) throws Exception { public Expr makeFunctionInvocation(String name, Expr[] params) throws Exception { if (name.equals("addToIndex")) - return makeStore(name, params); + return makeStore(params); if (name.equals("getFromIndex")) - return makeSelect(name, params); + return makeSelect(params); FuncDecl fd = funcTranslation.get(name); if (fd == null) fd = resolveFunctionDeclFallback(name, params); @@ -109,11 +101,7 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws Exce if (e.getSort().equals(s[i])) params[i] = e; } - // System.out.println("Expected sort"+s[i]+"; Final sort->" - // +params[i].toString() +":"+ - // params[i].getSort()); } - return z3.mkApp(fd, params); } @@ -149,14 +137,14 @@ private FuncDecl resolveFunctionDeclFallback(String name, Expr[] params) t } @SuppressWarnings({ "unchecked", "rawtypes" }) - private Expr makeSelect(String name, Expr[] params) { + private Expr makeSelect(Expr[] params) { if (params.length == 2 && params[0] instanceof ArrayExpr) return z3.mkSelect((ArrayExpr) params[0], params[1]); return null; } @SuppressWarnings({ "unchecked", "rawtypes" }) - private Expr makeStore(String name, Expr[] params) { + private Expr makeStore(Expr[] params) { if (params.length == 3 && params[0] instanceof ArrayExpr) return z3.mkStore((ArrayExpr) params[0], params[1], params[2]); return null; @@ -222,11 +210,6 @@ public Expr makeOr(Expr eval, Expr eval2) { return z3.mkOr((BoolExpr) eval, (BoolExpr) eval2); } - // public Expr makeIf(Expr eval, Expr eval2) { - // z3.mkI - // return z3.mkOr((BoolExpr) eval, (BoolExpr) eval2); - // } - // ##################### Unary Operations ##################### @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeMinus(Expr eval) { @@ -280,8 +263,7 @@ private FPExpr toFP(Expr e) { f = (FPExpr) e; } else if (e instanceof IntNum) f = z3.mkFP(((IntNum) e).getInt(), z3.mkFPSort64()); - else if (e instanceof IntExpr) { - IntExpr ee = (IntExpr) e; + else if (e instanceof IntExpr ee) { RealExpr re = z3.mkInt2Real(ee); f = z3.mkFPToFP(z3.mkFPRoundNearestTiesToEven(), re, z3.mkFPSort64()); } else if (e instanceof RealExpr) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Pair.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Pair.java index 699f80bf..708f4cba 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Pair.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Pair.java @@ -1,23 +1,4 @@ package liquidjava.utils; -public class Pair { - private K k; - private V v; - - public Pair(K k, V v) { - this.k = k; - this.v = v; - } - - public K getFirst() { - return k; - } - - public V getSecond() { - return v; - } - - public String toString() { - return "Pair [" + k.toString() + ", " + v.toString() + "]"; - } +public record Pair (K first, V second) { } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index b56a8cfd..275a5597 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -35,15 +35,11 @@ public static String qualifyName(String prefix, String name) { return String.format("%s.%s", prefix, name); } - public static String stripParens(String s) { - return s.startsWith("(") && s.endsWith(")") ? s.substring(1, s.length() - 1) : s; - } - public static SourcePosition getRefinementAnnotationPosition(CtElement element, String refinement) { return element.getAnnotations().stream().filter(a -> { String value = a.getValue("value").toString(); String unquoted = value.substring(1, value.length() - 1); return unquoted.equals(refinement); - }).findFirst().map(a -> a.getPosition()).orElse(element.getPosition()); + }).findFirst().map(CtElement::getPosition).orElse(element.getPosition()); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Patterns.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Patterns.java deleted file mode 100644 index 2bac52d7..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Patterns.java +++ /dev/null @@ -1,8 +0,0 @@ -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]+$"); -}