diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java index 4217ecf4..4cee020b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java @@ -14,10 +14,11 @@ public class ErrorEmitter { private int errorStatus; private HashMap map; - public ErrorEmitter() {} + public ErrorEmitter() { + } - public void addError( - String titleMessage, String msg, SourcePosition p, int errorStatus, HashMap map) { + public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus, + HashMap map) { this.titleMessage = titleMessage; fullMessage = msg; try { diff --git a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java index 8f92e0f0..f6681932 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java @@ -20,22 +20,13 @@ public class ErrorHandler { * @param expectedType * @param cSMT */ - public static void printError( - CtElement var, - Predicate expectedType, - Predicate cSMT, - HashMap map, - ErrorEmitter ee) { + public static void printError(CtElement var, Predicate expectedType, Predicate cSMT, + HashMap map, ErrorEmitter ee) { printError(var, null, expectedType, cSMT, map, ee); } - public static void printError( - CtElement var, - String moreInfo, - Predicate expectedType, - Predicate cSMT, - HashMap map, - ErrorEmitter errorl) { + public static void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT, + HashMap map, ErrorEmitter errorl) { String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" + // cSMT.toString(); @@ -44,7 +35,8 @@ public static void printError( // title StringBuilder sbtitle = new StringBuilder(); sbtitle.append("Failed to check refinement at: \n\n"); - if (moreInfo != null) sbtitle.append(moreInfo + "\n"); + if (moreInfo != null) + sbtitle.append(moreInfo + "\n"); sbtitle.append(var.toString()); // all message sb.append(sbtitle.toString() + "\n\n"); @@ -57,13 +49,8 @@ public static void printError( errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map); } - public static void printStateMismatch( - CtElement element, - String method, - VCImplication constraintForErrorMsg, - String states, - HashMap map, - ErrorEmitter errorl) { + public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg, + String states, HashMap map, ErrorEmitter errorl) { String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + "; // Found @@ -91,12 +78,8 @@ public static void printStateMismatch( errorl.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map); } - public static void printErrorUnknownVariable( - CtElement var, - String et, - String correctRefinement, - HashMap map, - ErrorEmitter errorl) { + public static void printErrorUnknownVariable(CtElement var, String et, String correctRefinement, + HashMap map, ErrorEmitter errorl) { String resumeMessage = "Encountered unknown variable"; @@ -114,13 +97,8 @@ public static void printErrorUnknownVariable( errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map); } - public static void printNotFound( - CtElement var, - Predicate constraint, - Predicate constraint2, - String msg, - HashMap map, - ErrorEmitter errorl) { + public static void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg, + HashMap map, ErrorEmitter errorl) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); @@ -136,12 +114,8 @@ public static void printNotFound( errorl.addError(msg, sb.toString(), var.getPosition(), 2, map); } - public static void printErrorArgs( - CtElement var, - Predicate expectedType, - String msg, - HashMap map, - ErrorEmitter errorl) { + public static void printErrorArgs(CtElement var, Predicate expectedType, String msg, + HashMap map, ErrorEmitter errorl) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); String title = "Error in ghost invocation: " + msg + "\n"; @@ -154,12 +128,8 @@ public static void printErrorArgs( errorl.addError(title, sb.toString(), var.getPosition(), 2, map); } - public static void printErrorTypeMismatch( - CtElement element, - Predicate expectedType, - String message, - HashMap map, - ErrorEmitter errorl) { + public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message, + HashMap map, ErrorEmitter errorl) { StringBuilder sb = new StringBuilder(); sb.append("______________________________________________________\n"); sb.append(message + "\n\n"); @@ -171,8 +141,8 @@ public static void printErrorTypeMismatch( errorl.addError(message, sb.toString(), element.getPosition(), 2, map); } - public static void printSameStateSetError( - CtElement element, Predicate p, String name, HashMap map, ErrorEmitter errorl) { + public static void printSameStateSetError(CtElement element, Predicate p, String name, + HashMap map, ErrorEmitter errorl) { String resume = "Error found multiple disjoint states from a State Set in a refinement"; StringBuilder sb = new StringBuilder(); @@ -249,7 +219,8 @@ public static void printSyntaxError(String msg, String ref, ErrorEmitter errorl) private static String printLine() { StringBuilder sb = new StringBuilder(); - for (int i = 0; i < 130; i++) sb.append("-"); // ----------- + for (int i = 0; i < 130; i++) + sb.append("-"); // ----------- return sb.toString(); } @@ -267,9 +238,7 @@ private static String printMap(HashMap map) { formatter.format(printLine() + "\n"); // data for (String s : map.keySet()) - formatter.format( - "| %-32s | %-60s | %-1s \n", - s, map.get(s).getText(), map.get(s).getSimplePosition()); + formatter.format("| %-32s | %-60s | %-1s \n", s, map.get(s).getText(), map.get(s).getSimplePosition()); // end formatter.format(printLine() + "\n\n"); String s = formatter.toString(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java index 9853681c..2e168f76 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java @@ -39,7 +39,8 @@ public void process(CtPackage pkg) { pkg.accept(new MethodsFirstChecker(c, factory, errorEmitter)); // double passing idea (instead of headers) pkg.accept(new RefinementTypeChecker(c, factory, errorEmitter)); - if (errorEmitter.foundError()) return; + if (errorEmitter.foundError()) + return; } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java index 00fb709a..eea4f6f6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java @@ -30,31 +30,32 @@ public String toString() { if (name != null && type != null) { String qualType = type.getQualifiedName(); String simpleType = qualType.contains(".") ? qualType.substring(qualType.lastIndexOf(".") + 1) : qualType; - return String.format( - "%-20s %s %s", - "∀" + name + ":" + simpleType + ",", - refinement.toString(), + return String.format("%-20s %s %s", "∀" + name + ":" + simpleType + ",", refinement.toString(), next != null ? " => \n" + next.toString() : ""); - } else return String.format("%-20s %s", "", refinement.toString()); + } else + return String.format("%-20s %s", "", refinement.toString()); } public Predicate toConjunctions() { Predicate c = new Predicate(); - if (name == null && type == null && next == null) return c; + if (name == null && type == null && next == null) + return c; c = auxConjunction(c); return c; } private Predicate auxConjunction(Predicate c) { Predicate t = Predicate.createConjunction(c, refinement); - if (next == null) return t; + if (next == null) + return t; t = next.auxConjunction(t); return t; } public VCImplication clone() { VCImplication vc = new VCImplication(this.name, this.type, this.refinement.clone()); - if (this.next != null) vc.next = this.next.clone(); + if (this.next != null) + vc.next = this.next.clone(); return vc; } } 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 50ca91a8..4e8b3987 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 @@ -33,8 +33,7 @@ public void visitCtClass(CtClass ctClass) { return; } - ctClass.getDeclaredFields().stream() - .filter(fld -> fld.getType().getQualifiedName().equals("int")) + 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)); 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 0c3b20ff..6b149ca9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/AliasWrapper.java @@ -64,8 +64,8 @@ public Predicate getPremises(List list, List newNames, CtElement List invocationPredicates = getPredicatesFromExpression(list, elem, ee); 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))); + prem = Predicate.createConjunction(prem, + Predicate.createEquals(Predicate.createVar(newNames.get(i)), invocationPredicates.get(i))); } return prem.clone(); } @@ -73,7 +73,8 @@ public Predicate getPremises(List list, List newNames, CtElement private List getPredicatesFromExpression(List list, CtElement elem, ErrorEmitter ee) throws ParsingException { List lp = new ArrayList<>(); - for (String e : list) lp.add(new Predicate(e, elem, ee)); + for (String e : list) + lp.add(new Predicate(e, elem, ee)); return lp; } 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 84f6645a..d604a00d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -36,7 +36,8 @@ private Context() { // SINGLETON public static Context getInstance() { - if (instance == null) instance = new Context(); + if (instance == null) + instance = new Context(); return instance; } @@ -62,13 +63,17 @@ public void reinitializeAllContext() { public void enterContext() { ctxVars.push(new ArrayList<>()); // make each variable enter context - for (RefinedVariable vi : getAllVariables()) if (vi instanceof Variable) ((Variable) vi).enterContext(); + for (RefinedVariable vi : getAllVariables()) + if (vi instanceof Variable) + ((Variable) vi).enterContext(); } public void exitContext() { ctxVars.pop(); // make each variable exit context - for (RefinedVariable vi : getAllVariables()) if (vi instanceof Variable) ((Variable) vi).exitContext(); + for (RefinedVariable vi : getAllVariables()) + if (vi instanceof Variable) + ((Variable) vi).exitContext(); } public int getCounter() { @@ -82,8 +87,10 @@ public Map> getContext() { ret.put(var.getName(), var.getType()); } } - for (RefinedVariable var : ctxSpecificVars) ret.put(var.getName(), var.getType()); - for (RefinedVariable var : ctxGlobalVars) ret.put(var.getName(), var.getType()); + for (RefinedVariable var : ctxSpecificVars) + ret.put(var.getName(), var.getType()); + for (RefinedVariable var : ctxGlobalVars) + ret.put(var.getName(), var.getType()); return ret; } @@ -108,8 +115,8 @@ public void addVarToContext(RefinedVariable var) { var.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); } - public RefinedVariable addVarToContext( - String simpleName, CtTypeReference type, Predicate c, CtElement placementInCode) { + public RefinedVariable addVarToContext(String simpleName, CtTypeReference type, Predicate c, + CtElement placementInCode) { RefinedVariable vi = new Variable(simpleName, type, c); vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode)); vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); @@ -117,16 +124,17 @@ public RefinedVariable addVarToContext( return vi; } - public RefinedVariable addInstanceToContext( - String simpleName, CtTypeReference type, Predicate c, CtElement placementInCode) { + public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference type, Predicate c, + CtElement placementInCode) { RefinedVariable vi = new VariableInstance(simpleName, type, c); vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode)); - if (!ctxSpecificVars.contains(vi)) addSpecificVariable(vi); + if (!ctxSpecificVars.contains(vi)) + addSpecificVariable(vi); return vi; } - public void addRefinementToVariableInContext( - String name, CtTypeReference type, Predicate et, CtElement placementInCode) { + public void addRefinementToVariableInContext(String name, CtTypeReference type, Predicate et, + CtElement placementInCode) { if (hasVariable(name)) { RefinedVariable vi = getVariableByName(name); vi.setRefinement(et); @@ -156,14 +164,17 @@ public Predicate getVariableRefinements(String varName) { public RefinedVariable getVariableByName(String name) { for (List l : ctxVars) { for (RefinedVariable var : l) { - if (var.getName().equals(name)) return var; + if (var.getName().equals(name)) + return var; } } for (RefinedVariable var : ctxSpecificVars) { - if (var.getName().equals(name)) return var; + if (var.getName().equals(name)) + return var; } for (RefinedVariable var : ctxGlobalVars) { - if (var.getName().equals(name)) return var; + if (var.getName().equals(name)) + return var; } return null; } @@ -200,10 +211,12 @@ public List getAllVariables() { public List getAllVariablesWithSupertypes() { List lvi = new ArrayList<>(); for (RefinedVariable rv : getAllVariables()) { - if (rv.getSuperTypes().size() > 0) lvi.add(rv); + if (rv.getSuperTypes().size() > 0) + lvi.add(rv); } for (RefinedVariable rv : ctxSpecificVars) { - if (rv.getSuperTypes().size() > 0) lvi.add(rv); + if (rv.getSuperTypes().size() > 0) + lvi.add(rv); } return lvi; } @@ -211,9 +224,9 @@ public List getAllVariablesWithSupertypes() { public void addRefinementInstanceToVariable(String name, String instanceName) { RefinedVariable vi1 = getVariableByName(name); RefinedVariable vi2 = getVariableByName(instanceName); - if (!hasVariable(name) - || !hasVariable(instanceName) - || !(vi1 instanceof Variable && vi2 instanceof VariableInstance)) return; + if (!hasVariable(name) || !hasVariable(instanceName) + || !(vi1 instanceof Variable && vi2 instanceof VariableInstance)) + return; ((Variable) vi1).addInstance((VariableInstance) vi2); ((VariableInstance) vi2).setParent((Variable) vi1); @@ -222,7 +235,8 @@ public void addRefinementInstanceToVariable(String name, String instanceName) { public Optional getLastVariableInstance(String name) { RefinedVariable rv = getVariableByName(name); - if (!hasVariable(name) || !(rv instanceof Variable)) return Optional.empty(); + if (!hasVariable(name) || !(rv instanceof Variable)) + return Optional.empty(); return ((Variable) rv).getLastInstance(); } @@ -236,23 +250,33 @@ public void addSpecificVariable(RefinedVariable vi) { // ---------------------- Variables - if information storing ---------------------- public void variablesSetBeforeIf() { - for (RefinedVariable vi : getAllVariables()) if (vi instanceof Variable) ((Variable) vi).saveInstanceBeforeIf(); + for (RefinedVariable vi : getAllVariables()) + if (vi instanceof Variable) + ((Variable) vi).saveInstanceBeforeIf(); } public void variablesSetThenIf() { - for (RefinedVariable vi : getAllVariables()) if (vi instanceof Variable) ((Variable) vi).saveInstanceThen(); + for (RefinedVariable vi : getAllVariables()) + if (vi instanceof Variable) + ((Variable) vi).saveInstanceThen(); } public void variablesSetElseIf() { - for (RefinedVariable vi : getAllVariables()) if (vi instanceof Variable) ((Variable) vi).saveInstanceElse(); + for (RefinedVariable vi : getAllVariables()) + if (vi instanceof Variable) + ((Variable) vi).saveInstanceElse(); } public void variablesNewIfCombination() { - for (RefinedVariable vi : getAllVariables()) if (vi instanceof Variable) ((Variable) vi).newIfCombination(); + for (RefinedVariable vi : getAllVariables()) + if (vi instanceof Variable) + ((Variable) vi).newIfCombination(); } public void variablesFinishIfCombination() { - for (RefinedVariable vi : getAllVariables()) if (vi instanceof Variable) ((Variable) vi).finishIfCombination(); + for (RefinedVariable vi : getAllVariables()) + if (vi instanceof Variable) + ((Variable) vi).finishIfCombination(); } public void variablesCombineFromIf(Predicate cond) { @@ -270,14 +294,14 @@ public void variablesCombineFromIf(Predicate cond) { // ---------------------- Functions ---------------------- public void addFunctionToContext(RefinedFunction f) { - if (!ctxFunctions.contains(f)) ctxFunctions.add(f); + if (!ctxFunctions.contains(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; + 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)) @@ -288,10 +312,9 @@ public RefinedFunction getFunction(String name, String target) { 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) - && fi.getArguments().size() == size) return fi; + if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target) + && fi.getArguments().size() == size) + return fi; } return null; } @@ -299,7 +322,8 @@ public RefinedFunction getFunction(String name, String target, int size) { public List getAllMethodsWithNameSize(String name, int size) { List l = new ArrayList<>(); for (RefinedFunction fi : ctxFunctions) { - if (fi.getName().equals(name) && fi.getArguments().size() == size) l.add(fi); + if (fi.getName().equals(name) && fi.getArguments().size() == size) + l.add(fi); } return l; } @@ -311,7 +335,8 @@ public void addGhostFunction(GhostFunction gh) { public boolean hasGhost(String name) { for (GhostFunction g : ghosts) { - if (g.getName().equals(name)) return true; + if (g.getName().equals(name)) + return true; } return false; } @@ -321,12 +346,14 @@ public List getGhosts() { } public void addGhostClass(String klass) { - if (!classStates.containsKey(klass)) classStates.put(klass, new ArrayList<>()); + if (!classStates.containsKey(klass)) + classStates.put(klass, new ArrayList<>()); } public void addToGhostClass(String klass, GhostState gs) { List l = classStates.get(klass); - if (!l.contains(gs)) l.add(gs); + if (!l.contains(gs)) + l.add(gs); } public List getGhostState(String s) { @@ -335,13 +362,15 @@ public List getGhostState(String s) { public List getGhostState() { List lgs = new ArrayList<>(); - for (List l : classStates.values()) lgs.addAll(l); + for (List l : classStates.values()) + lgs.addAll(l); return lgs; } // ---------------------- Alias ---------------------- public void addAlias(AliasWrapper aw) { - if (!alias.contains(aw)) alias.add(aw); + if (!alias.contains(aw)) + alias.add(aw); } public List getAlias() { @@ -352,7 +381,8 @@ public List getAlias() { public String toString() { StringBuilder sb = new StringBuilder(); sb.append("\n############Global Variables:############\n"); - for (RefinedVariable f : ctxGlobalVars) sb.append(f.toString()); + for (RefinedVariable f : ctxGlobalVars) + sb.append(f.toString()); sb.append("\n###########Variables############"); for (List l : ctxVars) { sb.append("{"); @@ -365,10 +395,12 @@ public String toString() { // for(RefinedFunction f : ctxGlobalFunctions) // sb.append(f.toString()); sb.append("\n############Functions:############\n"); - for (RefinedFunction f : ctxFunctions) sb.append(f.toString()); + for (RefinedFunction f : ctxFunctions) + sb.append(f.toString()); sb.append("\n############Ghost Functions:############\n"); - for (GhostFunction f : ghosts) sb.append(f.toString()); + for (GhostFunction f : ghosts) + sb.append(f.toString()); return sb.toString(); } 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 9a453e47..c81f5c12 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java @@ -24,13 +24,8 @@ public GhostFunction(GhostDTO f, Factory factory, String path, String klass) { } } - public GhostFunction( - String name, - List param_types, - CtTypeReference return_type, - Factory factory, - String path, - String klass) { + public GhostFunction(String name, List param_types, CtTypeReference return_type, Factory factory, + String path, String klass) { this.name = name; this.return_type = Utils.getType(return_type.toString().equals(klass) ? path : return_type.toString(), factory); this.param_types = new ArrayList<>(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java index 1788b5aa..6252c1c5 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostParentState.java @@ -9,13 +9,8 @@ public class GhostParentState extends GhostFunction { private ArrayList states; - public GhostParentState( - String name, - List params, - CtTypeReference ret, - Factory factory, - String qualifiedName, - String simpleName) { + public GhostParentState(String name, List params, CtTypeReference ret, Factory factory, + String qualifiedName, String simpleName) { super(name, params, ret, factory, qualifiedName, simpleName); states = new ArrayList<>(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java index 0343969a..795e9815 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java @@ -7,7 +7,8 @@ public class ObjectState { Predicate from; Predicate to; - public ObjectState() {} + public ObjectState() { + } public ObjectState(Predicate from, Predicate to) { this.from = from; 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 07887839..a597fe24 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Refined.java @@ -9,7 +9,8 @@ public abstract class Refined { private CtTypeReference type; // int private Predicate refinement; // 9 <= y && y <= 100 - public Refined() {} + public Refined() { + } public Refined(String name, CtTypeReference type, Predicate refinement) { this.name = name; @@ -38,7 +39,8 @@ public void setRefinement(Predicate c) { } public Predicate getRefinement() { - if (refinement != null) return refinement; + if (refinement != null) + return refinement; return new Predicate(); } @@ -63,16 +65,23 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; Refined other = (Refined) obj; if (name == null) { - if (other.name != null) return false; - } else if (!name.equals(other.name)) return false; + if (other.name != null) + return false; + } 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; + if (other.type != null) + return false; + } else if (!type.equals(other.type)) + return false; return true; } } 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 6c9d2fb9..7b70f473 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedFunction.java @@ -69,7 +69,8 @@ private Predicate getRenamedRefinements(Predicate place, Context context, CtElem public Predicate getAllRefinements() { Predicate c = new Predicate(); - for (RefinedVariable p : argRefinements) c = Predicate.createConjunction(c, p.getRefinement()); // joinArgs + for (RefinedVariable p : argRefinements) + c = Predicate.createConjunction(c, p.getRefinement()); // joinArgs c = Predicate.createConjunction(c, super.getRefinement()); // joinReturn return c; } @@ -117,13 +118,15 @@ public boolean hasStateChange() { public List getFromStates() { List lc = new ArrayList<>(); - for (ObjectState os : stateChange) lc.add(os.getFrom()); + for (ObjectState os : stateChange) + lc.add(os.getFrom()); return lc; } public List getToStates() { List lc = new ArrayList<>(); - for (ObjectState os : stateChange) lc.add(os.getTo()); + for (ObjectState os : stateChange) + lc.add(os.getTo()); return lc; } @@ -144,16 +147,23 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (!super.equals(obj)) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (!super.equals(obj)) + return false; + if (getClass() != obj.getClass()) + return false; RefinedFunction other = (RefinedFunction) obj; if (argRefinements == null) { - if (other.argRefinements != null) return false; - } else if (argRefinements.size() != other.argRefinements.size()) return false; + if (other.argRefinements != null) + return false; + } else if (argRefinements.size() != other.argRefinements.size()) + return false; if (targetClass == null) { - if (other.targetClass != null) return false; - } else if (!targetClass.equals(other.targetClass)) return false; + if (other.targetClass != null) + return false; + } else if (!targetClass.equals(other.targetClass)) + return false; return true; } } 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 5cc07a18..fe3abf11 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -18,7 +18,8 @@ public RefinedVariable(String name, CtTypeReference type, Predicate c) { public abstract Predicate getMainRefinement(); public void addSuperType(CtTypeReference t) { - if (!supertypes.contains(t)) supertypes.add(t); + if (!supertypes.contains(t)) + supertypes.add(t); } public List> getSuperTypes() { @@ -26,8 +27,11 @@ public List> getSuperTypes() { } public void addSuperTypes(CtTypeReference ts, Set> sts) { - if (ts != null && !supertypes.contains(ts)) supertypes.add(ts); - for (CtTypeReference ct : sts) if (ct != null && !supertypes.contains(ct)) supertypes.add(ct); + if (ts != null && !supertypes.contains(ts)) + supertypes.add(ts); + for (CtTypeReference ct : sts) + if (ct != null && !supertypes.contains(ct)) + supertypes.add(ct); } public void addPlacementInCode(PlacementInCode s) { @@ -48,13 +52,18 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (!super.equals(obj)) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (!super.equals(obj)) + return false; + if (getClass() != obj.getClass()) + return false; RefinedVariable other = (RefinedVariable) obj; if (supertypes == null) { - if (other.supertypes != null) return false; - } else if (!supertypes.equals(other.supertypes)) return false; + if (other.supertypes != null) + return false; + } else if (!supertypes.equals(other.supertypes)) + return false; return true; } } 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 f1511798..ff616db9 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java @@ -74,7 +74,8 @@ public void addInstance(VariableInstance vi) { } public void removeLastInstance() { - if (instances.size() > 0) instances.peek().remove(instances.size() - 1); + if (instances.size() > 0) + instances.peek().remove(instances.size() - 1); } public Optional getLastInstance() { @@ -93,11 +94,15 @@ public Optional getLastInstance() { } private void reloadFromBackup(Stack> backup) { - while (backup.size() > 0) instances.add(backup.pop()); + while (backup.size() > 0) + instances.add(backup.pop()); } public boolean hasInstance(VariableInstance vi) { - for (List lv : instances) for (VariableInstance v : lv) if (v.equals(vi)) return true; + for (List lv : instances) + for (VariableInstance v : lv) + if (v.equals(vi)) + return true; return false; } @@ -144,15 +149,16 @@ Optional getIfInstanceCombination(int counter, Predicate cond) if (!has(ifelseIndex)) { if (has(ifbeforeIndex) && has(ifthenIndex)) // value before if and inside then - ref = createITEConstraint(nName, cond, get(ifthenIndex), get(ifbeforeIndex)); + ref = createITEConstraint(nName, cond, get(ifthenIndex), get(ifbeforeIndex)); else if (!has(ifbeforeIndex)) // only value inside then - ref = createITEConstraint(nName, cond, get(ifthenIndex)); + ref = createITEConstraint(nName, cond, get(ifthenIndex)); } else { if (has(ifthenIndex)) // value in then and in else - ref = createITEConstraint(nName, cond, get(ifthenIndex), get(ifelseIndex)); + ref = createITEConstraint(nName, cond, get(ifthenIndex), get(ifelseIndex)); else if (has(ifbeforeIndex)) // value before and in else - ref = createITEConstraint(nName, cond, get(ifbeforeIndex), get(ifelseIndex)); - else ref = createITEConstraint(nName, cond.negate(), get(ifelseIndex)); + ref = createITEConstraint(nName, cond, get(ifbeforeIndex), get(ifelseIndex)); + else + ref = createITEConstraint(nName, cond.negate(), get(ifelseIndex)); } VariableInstance jointReturn = new VariableInstance(nName, super.getType(), ref, this); jointReturn.addPlacementInCode(getPlacementInCode()); 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 6aa92467..fe8de3c5 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 @@ -35,7 +35,8 @@ public void visitCtClass(CtClass ctClass) { @Override public void visitCtInterface(CtInterface intrface) { - if (errorEmitter.foundError()) return; + if (errorEmitter.foundError()) + return; Optional externalRefinements = getExternalRefinement(intrface); if (externalRefinements.isPresent()) { @@ -52,7 +53,8 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtField(CtField f) { - if (errorEmitter.foundError()) return; + if (errorEmitter.foundError()) + return; Optional oc; try { @@ -66,7 +68,8 @@ public void visitCtField(CtField f) { } public void visitCtMethod(CtMethod method) { - if (errorEmitter.foundError()) return; + if (errorEmitter.foundError()) + return; MethodsFunctionsChecker mfc = new MethodsFunctionsChecker(this); try { @@ -93,8 +96,8 @@ protected void getGhostFunction(String value, CtElement element) { } } catch (ParsingException e) { - ErrorHandler.printCostumeError( - element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter); + ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(), + errorEmitter); // e.printStackTrace(); } } @@ -106,8 +109,8 @@ protected Optional createStateGhost(int order, CtElement element) if (klass != null) { CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; List params = Arrays.asList(klass); - GhostFunction gh = new GhostFunction( - String.format("%s_state%d", klass.toLowerCase(), order), params, ret, factory, prefix, klass); + GhostFunction gh = new GhostFunction(String.format("%s_state%d", klass.toLowerCase(), order), params, ret, + factory, prefix, klass); return Optional.of(gh); } return Optional.empty(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 718685d5..b4224d3b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -27,24 +27,29 @@ public MethodsFirstChecker(Context c, Factory fac, ErrorEmitter errorEmitter) { @Override public void visitCtClass(CtClass ctClass) { - if (errorEmitter.foundError()) return; + if (errorEmitter.foundError()) + return; context.reinitializeContext(); - if (visitedClasses.contains(ctClass.getQualifiedName())) return; - else visitedClasses.add(ctClass.getQualifiedName()); + if (visitedClasses.contains(ctClass.getQualifiedName())) + return; + else + visitedClasses.add(ctClass.getQualifiedName()); // visitInterfaces if (!ctClass.getSuperInterfaces().isEmpty()) for (CtTypeReference t : ctClass.getSuperInterfaces()) { if (t.isInterface()) { CtType ct = t.getDeclaration(); - if (ct instanceof CtInterface) visitCtInterface((CtInterface) ct); + if (ct instanceof CtInterface) + visitCtInterface((CtInterface) ct); } } // visitSubclasses CtTypeReference sup = ctClass.getSuperclass(); if (sup != null && sup.isClass()) { CtType ct = sup.getDeclaration(); - if (ct instanceof CtClass) visitCtClass((CtClass) ct); + if (ct instanceof CtClass) + visitCtClass((CtClass) ct); } try { getRefinementFromAnnotation(ctClass); @@ -57,11 +62,15 @@ public void visitCtClass(CtClass ctClass) { @Override public void visitCtInterface(CtInterface intrface) { - if (errorEmitter.foundError()) return; + if (errorEmitter.foundError()) + return; - if (visitedClasses.contains(intrface.getQualifiedName())) return; - else visitedClasses.add(intrface.getQualifiedName()); - if (getExternalRefinement(intrface).isPresent()) return; + if (visitedClasses.contains(intrface.getQualifiedName())) + return; + else + visitedClasses.add(intrface.getQualifiedName()); + if (getExternalRefinement(intrface).isPresent()) + return; try { getRefinementFromAnnotation(intrface); @@ -74,7 +83,8 @@ public void visitCtInterface(CtInterface intrface) { @Override public void visitCtConstructor(CtConstructor c) { - if (errorEmitter.foundError()) return; + if (errorEmitter.foundError()) + return; context.enterContext(); try { @@ -88,7 +98,8 @@ public void visitCtConstructor(CtConstructor c) { } public void visitCtMethod(CtMethod method) { - if (errorEmitter.foundError()) return; + if (errorEmitter.foundError()) + return; context.enterContext(); try { 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 f2c4672d..b6bfaa12 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 @@ -130,8 +130,8 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { } catch (ParsingException e) { return; // error already in ErrorEmitter } - context.addVarToContext( - localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), localVariable); + context.addVarToContext(localVariable.getSimpleName(), localVariable.getType(), a.orElse(new Predicate()), + localVariable); } else { String varName = localVariable.getSimpleName(); CtExpression e = localVariable.getAssignment(); @@ -143,8 +143,8 @@ public void visitCtLocalVariable(CtLocalVariable localVariable) { context.addVarToContext(varName, localVariable.getType(), new Predicate(), e); try { - checkVariableRefinements( - refinementFound, varName, localVariable.getType(), localVariable, localVariable); + checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, + localVariable); } catch (ParsingException e1) { return; // error already in ErrorEmitter } @@ -199,8 +199,8 @@ public void visitCtThisAccess(CtThisAccess thisAccess) { String s = c.getSimpleName(); if (thisAccess.getParent() instanceof CtReturn) { String thisName = String.format(thisFormat, s); - thisAccess.putMetadata( - REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName))); + thisAccess.putMetadata(REFINE_KEY, + Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName))); } } @@ -261,17 +261,14 @@ public void visitCtLiteral(CtLiteral lit) { List types = Arrays.asList(implementedTypes); String type = lit.getType().getQualifiedName(); if (types.contains(type)) { - lit.putMetadata( - REFINE_KEY, - Predicate.createEquals( - Predicate.createVar(WILD_VAR), - Predicate.createLit(lit.getValue().toString(), type))); + lit.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR), + Predicate.createLit(lit.getValue().toString(), type))); } else if (lit.getType().getQualifiedName().contentEquals("java.lang.String")) { // Only taking care of strings inside refinements } else { - throw new NotImplementedException(String.format( - "Literal of type %s not implemented:", lit.getType().getQualifiedName())); + throw new NotImplementedException( + String.format("Literal of type %s not implemented:", lit.getType().getQualifiedName())); } } @@ -311,32 +308,24 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { String fieldName = fieldRead.getVariable().getSimpleName(); if (context.hasVariable(fieldName)) { RefinedVariable rv = context.getVariableByName(fieldName); - if (rv instanceof Variable - && ((Variable) rv).getLocation().isPresent() - && ((Variable) rv) - .getLocation() - .get() - .equals(fieldRead.getTarget().toString())) { + if (rv instanceof Variable && ((Variable) rv).getLocation().isPresent() + && ((Variable) rv).getLocation().get().equals(fieldRead.getTarget().toString())) { fieldRead.putMetadata(REFINE_KEY, context.getVariableRefinements(fieldName)); } else { - fieldRead.putMetadata( - REFINE_KEY, + fieldRead.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(fieldName))); } } else if (context.hasVariable(String.format(thisFormat, fieldName))) { String thisName = String.format(thisFormat, fieldName); - fieldRead.putMetadata( - REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName))); + fieldRead.putMetadata(REFINE_KEY, + Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(thisName))); } else if (fieldRead.getVariable().getSimpleName().equals("length")) { String targetName = fieldRead.getTarget().toString(); try { - fieldRead.putMetadata( - REFINE_KEY, - Predicate.createEquals( - Predicate.createVar(WILD_VAR), - BuiltinFunctionPredicate.builtin_length(targetName, fieldRead, getErrorEmitter()))); + fieldRead.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR), + BuiltinFunctionPredicate.builtin_length(targetName, fieldRead, getErrorEmitter()))); } catch (ParsingException e) { return; // error already in ErrorEmitter } @@ -433,8 +422,8 @@ public void visitCtIf(CtIf ifElement) { expRefs = new Predicate(); } - RefinedVariable freshRV = - context.addInstanceToContext(freshVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, exp); + RefinedVariable freshRV = context.addInstanceToContext(freshVarName, factory.Type().INTEGER_PRIMITIVE, expRefs, + exp); vcChecker.addPathVariable(freshRV); context.variablesNewIfCombination(); @@ -475,8 +464,8 @@ public void visitCtArrayWrite(CtArrayWrite arrayWrite) { CtExpression index = arrayWrite.getIndexExpression(); BuiltinFunctionPredicate fp; try { - fp = BuiltinFunctionPredicate.builtin_addToIndex( - arrayWrite.getTarget().toString(), index.toString(), WILD_VAR, arrayWrite, getErrorEmitter()); + fp = BuiltinFunctionPredicate.builtin_addToIndex(arrayWrite.getTarget().toString(), index.toString(), + WILD_VAR, arrayWrite, getErrorEmitter()); } catch (ParsingException e) { return; // error already in ErrorEmitter } @@ -491,8 +480,8 @@ public void visitCtConditional(CtConditional conditional) { super.visitCtConditional(conditional); Predicate cond = getRefinement(conditional.getCondition()); - Predicate c = Predicate.createITE( - cond, getRefinement(conditional.getThenExpression()), getRefinement(conditional.getElseExpression())); + Predicate c = Predicate.createITE(cond, getRefinement(conditional.getThenExpression()), + getRefinement(conditional.getElseExpression())); conditional.putMetadata(REFINE_KEY, c); } @@ -517,13 +506,8 @@ public void visitCtNewClass(CtNewClass newClass) { // ############################### Inner Visitors // ########################################## - private void checkAssignment( - String name, - CtTypeReference type, - CtExpression ex, - CtExpression assignment, - CtElement parentElem, - CtElement varDecl) { + private void checkAssignment(String name, CtTypeReference type, CtExpression ex, CtExpression assignment, + CtElement parentElem, CtElement varDecl) { getPutVariableMetadada(ex, name); Predicate refinementFound = getRefinement(assignment); @@ -596,8 +580,7 @@ private void getPutVariableMetadada(CtElement elem, String name) { Predicate cref = Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(name)); Optional ovi = context.getLastVariableInstance(name); if (ovi.isPresent()) { - cref = Predicate.createEquals( - Predicate.createVar(WILD_VAR), Predicate.createVar(ovi.get().getName())); + cref = Predicate.createEquals(Predicate.createVar(WILD_VAR), Predicate.createVar(ovi.get().getName())); } elem.putMetadata(REFINE_KEY, 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 b5708b2c..aeae4792 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 @@ -38,7 +38,7 @@ public abstract class TypeChecker extends CtScanner { public final String freshFormat = "#fresh_%d"; public final String instanceFormat = "#%s_%d"; public final String thisFormat = "this#%s"; - public String[] implementedTypes = {"boolean", "int", "short", "long", "float", "double"}; // TODO add + public String[] implementedTypes = { "boolean", "int", "short", "long", "float", "double" }; // TODO add // types e.g., "int[]" Context context; @@ -87,7 +87,8 @@ public Optional getRefinementFromAnnotation(CtElement element) throws } if (ref.isPresent()) { Predicate p = new Predicate(ref.get(), element, errorEmitter); - if (errorEmitter.foundError()) return Optional.empty(); + if (errorEmitter.foundError()) + return Optional.empty(); constr = Optional.of(p); } return constr; @@ -126,13 +127,12 @@ private void createStateSet(CtNewArray e, int set, CtElement element) { @SuppressWarnings("unchecked") CtLiteral s = (CtLiteral) ce; String f = s.getValue(); - GhostState gs = new GhostState( - f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE, g.getParentClassName()); + GhostState gs = new GhostState(f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE, + g.getParentClassName()); gs.setGhostParent(g); gs.setRefinement( /* new OperationPredicate(new InvocationPredicate(f, THIS), "<-->", */ - Predicate.createEquals( - ip, Predicate.createLit(Integer.toString(order), Utils.INT))); // open(THIS) + Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Utils.INT))); // open(THIS) // -> // state1(THIS) // == 1 @@ -151,11 +151,8 @@ private void createStateGhost(String string, CtAnnotation return; } if (gd.getParam_types().size() > 0) { - ErrorHandler.printCostumeError( - ann, - "Ghost States have the class as parameter " + "by default, no other parameters are allowed in '" - + string + "'", - errorEmitter); + ErrorHandler.printCostumeError(ann, "Ghost States have the class as parameter " + + "by default, no other parameters are allowed in '" + string + "'", errorEmitter); return; } // Set class as parameter of Ghost @@ -198,12 +195,8 @@ protected Optional createStateGhost(int order, CtElement element) CtTypeReference ret = factory.Type().INTEGER_PRIMITIVE; List params = Arrays.asList(klass.getSimpleName()); GhostFunction gh = new GhostFunction( - String.format("%s_state%d", klass.getSimpleName().toLowerCase(), order), - params, - ret, - factory, - klass.getQualifiedName(), - klass.getSimpleName()); + String.format("%s_state%d", klass.getSimpleName().toLowerCase(), order), params, ret, factory, + klass.getQualifiedName(), klass.getSimpleName()); return Optional.of(gh); } return Optional.empty(); @@ -218,8 +211,8 @@ protected void getGhostFunction(String value, CtElement element) { context.addGhostFunction(gh); } } catch (ParsingException e) { - ErrorHandler.printCostumeError( - element, "Could not parse the Ghost Function" + e.getMessage(), errorEmitter); + ErrorHandler.printCostumeError(element, "Could not parse the Ghost Function" + e.getMessage(), + errorEmitter); // e.printStackTrace(); return; } @@ -254,9 +247,7 @@ protected void handleAlias(String value, CtElement element) { Optional getExternalRefinement(CtInterface intrface) { Optional ref = Optional.empty(); for (CtAnnotation ann : intrface.getAnnotations()) - if (ann.getActualAnnotation() - .annotationType() - .getCanonicalName() + if (ann.getActualAnnotation().annotationType().getCanonicalName() .contentEquals("liquidjava.specification.ExternalRefinementsFor")) { @SuppressWarnings("unchecked") CtLiteral s = (CtLiteral) ann.getAllValues().get("value"); @@ -265,19 +256,20 @@ Optional getExternalRefinement(CtInterface intrface) { return ref; } - public void checkVariableRefinements( - Predicate refinementFound, String simpleName, CtTypeReference type, CtElement usage, CtElement variable) - throws ParsingException { + public void checkVariableRefinements(Predicate refinementFound, String simpleName, CtTypeReference type, + CtElement usage, CtElement variable) throws ParsingException { Optional expectedType = getRefinementFromAnnotation(variable); Predicate cEt; RefinedVariable mainRV = null; - if (context.hasVariable(simpleName)) mainRV = context.getVariableByName(simpleName); + 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 if (expectedType.isPresent()) + cEt = expectedType.get(); + else + cEt = new Predicate(); cEt = cEt.substituteVariable(WILD_VAR, simpleName); Predicate cet = cEt.substituteVariable(WILD_VAR, simpleName); @@ -289,7 +281,8 @@ public void checkVariableRefinements( // Substitute variable in verification RefinedVariable rv = context.addInstanceToContext(newName, type, correctNewRefinement, usage); - for (CtTypeReference t : mainRV.getSuperTypes()) rv.addSuperType(t); + for (CtTypeReference t : mainRV.getSuperTypes()) + rv.addSuperType(t); context.addRefinementInstanceToVariable(simpleName, newName); // smt check checkSMT(cEt, usage); // TODO CHANGE @@ -302,13 +295,13 @@ public void checkSMT(Predicate expectedType, CtElement element) { } public void checkStateSMT(Predicate prevState, Predicate expectedState, CtElement target, String string) { - vcChecker.processSubtyping( - prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, target, string, factory); + vcChecker.processSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, target, string, + factory); } public boolean checksStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p) { - return vcChecker.canProcessSubtyping( - prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, p, factory); + return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), WILD_VAR, THIS, p, + factory); } public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customeMessage) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeCheckingUtils.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeCheckingUtils.java index 6960bafa..ed839368 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 @@ -11,7 +11,8 @@ public static String getStringFromAnnotation(CtExpression ce) { if (ce instanceof CtLiteral) { CtLiteral cl = (CtLiteral) ce; CtTypeReference r = ce.getType(); - if (r.getSimpleName().equals("String")) return (String) cl.getValue(); + if (r.getSimpleName().equals("String")) + return (String) cl.getValue(); } else if (ce instanceof CtBinaryOperator) { CtBinaryOperator cbo = (CtBinaryOperator) ce; 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 97184968..0711807d 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 @@ -34,26 +34,20 @@ public VCChecker(ErrorEmitter errorEmitter) { this.errorEmitter = errorEmitter; } - public void processSubtyping( - Predicate expectedType, - List list, - String wild_var, - String this_var, - CtElement element, - Factory f) { + public void processSubtyping(Predicate expectedType, List list, String wild_var, String this_var, + CtElement element, Factory f) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); - if (expectedType.isBooleanTrue()) return; + if (expectedType.isBooleanTrue()) + return; HashMap map = new HashMap<>(); - String[] s = {wild_var, this_var}; - Predicate premisesBeforeChange = - joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); + String[] s = { wild_var, this_var }; + Predicate premisesBeforeChange = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); Predicate premises = new Predicate(); Predicate et = new Predicate(); try { - premises = premisesBeforeChange - .changeStatesToRefinements(list, s, errorEmitter) + premises = premisesBeforeChange.changeStatesToRefinements(list, s, errorEmitter) .changeAliasToRefinement(context, f); et = expectedType.changeStatesToRefinements(list, s, errorEmitter).changeAliasToRefinement(context, f); @@ -70,42 +64,30 @@ public void processSubtyping( } } - public void processSubtyping( - Predicate type, - Predicate expectedType, - List list, - String wild_var, - String this_var, - CtElement element, - String string, - Factory f) { + public void processSubtyping(Predicate type, Predicate expectedType, List list, String wild_var, + String this_var, CtElement element, String string, Factory f) { boolean b = canProcessSubtyping(type, expectedType, list, wild_var, this_var, element.getPosition(), f); - if (!b) printSubtypingError(element, expectedType, type, string); + if (!b) + printSubtypingError(element, expectedType, type, string); } - public boolean canProcessSubtyping( - Predicate type, - Predicate expectedType, - List list, - String wild_var, - String this_var, - SourcePosition p, - Factory f) { + public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List list, String wild_var, + String this_var, SourcePosition p, Factory f) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(type, lrv, mainVars); - if (expectedType.isBooleanTrue() && type.isBooleanTrue()) return true; + if (expectedType.isBooleanTrue() && type.isBooleanTrue()) + return true; // Predicate premises = joinPredicates(type, element, mainVars, lrv); HashMap map = new HashMap<>(); - String[] s = {wild_var, this_var}; + String[] s = { wild_var, this_var }; Predicate premises = new Predicate(); Predicate et = new Predicate(); try { premises = joinPredicates(expectedType, mainVars, lrv, map).toConjunctions(); - premises = Predicate.createConjunction(premises, type) - .changeStatesToRefinements(list, s, errorEmitter) + premises = Predicate.createConjunction(premises, type).changeStatesToRefinements(list, s, errorEmitter) .changeAliasToRefinement(context, f); et = expectedType.changeStatesToRefinements(list, s, errorEmitter).changeAliasToRefinement(context, f); } catch (Exception e) { @@ -118,11 +100,8 @@ public boolean canProcessSubtyping( return smtChecks(premises, et, p); } - private VCImplication joinPredicates( - Predicate expectedType, - List mainVars, - List vars, - HashMap map) { + private VCImplication joinPredicates(Predicate expectedType, List mainVars, + List vars, HashMap map) { VCImplication firstSi = null; VCImplication lastSi = null; @@ -181,18 +160,17 @@ private void gatherVariables(Predicate expectedType, List lrv, for (String s : expectedType.getVariableNames()) { if (context.hasVariable(s)) { RefinedVariable rv = context.getVariableByName(s); - if (!mainVars.contains(rv) && !lrv.contains(rv)) mainVars.add(rv); + if (!mainVars.contains(rv) && !lrv.contains(rv)) + mainVars.add(rv); List lm = getVariables(rv.getMainRefinement(), rv.getName()); addAllDifferent(lrv, lm, mainVars); } } } - private void addAllDifferent( - List toExpand, List from, List remove) { - from.stream() - .filter(rv -> !toExpand.contains(rv) && !remove.contains(rv)) - .forEach(toExpand::add); + 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); @@ -209,18 +187,16 @@ private List getVariables(Predicate c, String varName) { } private void getVariablesFromContext(List lvars, List allVars, String notAdd) { - lvars.stream() - .filter(name -> !name.equals(notAdd) && context.hasVariable(name)) - .map(context::getVariableByName) - .filter(rv -> !allVars.contains(rv)) - .forEach(rv -> { + lvars.stream().filter(name -> !name.equals(notAdd) && context.hasVariable(name)).map(context::getVariableByName) + .filter(rv -> !allVars.contains(rv)).forEach(rv -> { allVars.add(rv); recAuxGetVars(rv, allVars); }); } private void recAuxGetVars(RefinedVariable var, List newVars) { - if (!context.hasVariable(var.getName())) return; + if (!context.hasVariable(var.getName())) + return; Predicate c = var.getRefinement(); String varName = var.getName(); List l = c.getVariableNames(); @@ -281,10 +257,8 @@ 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)) + .collect(Collectors.toList()).forEach(pathVariables::remove); } private void printVCs(String string, String stringSMT, Predicate expectedType) { @@ -305,8 +279,8 @@ private HashMap createMap(CtElement element, Predicate return map; } - protected void printSubtypingError( - CtElement element, Predicate expectedType, Predicate foundType, String customeMsg) { + protected void printSubtypingError(CtElement element, Predicate expectedType, Predicate foundType, + String customeMsg) { List lrv = new ArrayList<>(), mainVars = new ArrayList<>(); gatherVariables(expectedType, lrv, mainVars); gatherVariables(foundType, lrv, mainVars); @@ -320,11 +294,7 @@ public void printSameStateError(CtElement element, Predicate expectedType, Strin ErrorHandler.printSameStateSetError(element, expectedType, klass, map, errorEmitter); } - private void printError( - Exception e, - Predicate premisesBeforeChange, - Predicate expectedType, - CtElement element, + private void printError(Exception e, Predicate premisesBeforeChange, Predicate expectedType, CtElement element, HashMap map) { String s = null; if (element instanceof CtInvocation) { @@ -355,12 +325,8 @@ private void printError( } } - private void printError( - Predicate premises, - Predicate expectedType, - CtElement element, - HashMap map, - String s) { + private void printError(Predicate premises, Predicate expectedType, CtElement element, + HashMap map, String s) { Predicate etMessageReady = expectedType; // substituteByMap(expectedType, map); Predicate cSMTMessageReady = premises; // substituteByMap(premises, map); ErrorHandler.printError(element, s, etMessageReady, cSMTMessageReady, map, errorEmitter); 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 bc55877a..93ae6503 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 @@ -60,17 +60,11 @@ public void getConstructorRefinements(CtConstructor c) throws ParsingExceptio public void getConstructorInvocationRefinements(CtConstructorCall ctConstructorCall) { CtExecutableReference exe = ctConstructorCall.getExecutable(); if (exe != null) { - RefinedFunction f = rtc.getContext() - .getFunction( - exe.getSimpleName(), - exe.getDeclaringType().getQualifiedName(), - ctConstructorCall.getArguments().size()); + RefinedFunction f = rtc.getContext().getFunction(exe.getSimpleName(), + exe.getDeclaringType().getQualifiedName(), ctConstructorCall.getArguments().size()); if (f != null) { - Map map = checkInvocationRefinements( - ctConstructorCall, - ctConstructorCall.getArguments(), - ctConstructorCall.getTarget(), - f.getName(), + Map map = checkInvocationRefinements(ctConstructorCall, + ctConstructorCall.getArguments(), ctConstructorCall.getTarget(), f.getName(), f.getTargetClass()); AuxStateHandler.constructorStateMetadata(rtc.REFINE_KEY, f, map, ctConstructorCall); } @@ -98,7 +92,8 @@ public void getMethodRefinements(CtMethod method) throws ParsingException auxGetMethodRefinements(method, f); AuxStateHandler.handleMethodState(method, f, rtc); - if (klass != null) AuxHierarchyRefinememtsPassage.checkFunctionInSupertypes(klass, method, f, rtc); + if (klass != null) + AuxHierarchyRefinememtsPassage.checkFunctionInSupertypes(klass, method, f, rtc); } public void getMethodRefinements(CtMethod method, String prefix) throws ParsingException { @@ -127,7 +122,8 @@ public void getMethodRefinements(CtMethod method, String prefix) throws P private void auxGetMethodRefinements(CtMethod method, RefinedFunction rf) throws ParsingException { // main cannot have refinement - for now - if (method.getSignature().equals("main(java.lang.String[])")) return; + if (method.getSignature().equals("main(java.lang.String[])")) + return; List> params = method.getParameters(); Predicate ref = handleFunctionRefinements(rf, method, params); method.putMetadata(rtc.REFINE_KEY, ref); @@ -152,10 +148,12 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, String paramName = param.getSimpleName(); Optional oc = rtc.getRefinementFromAnnotation(param); Predicate c = new Predicate(); - if (oc.isPresent()) c = oc.get().substituteVariable(rtc.WILD_VAR, paramName); + if (oc.isPresent()) + c = oc.get().substituteVariable(rtc.WILD_VAR, paramName); param.putMetadata(rtc.REFINE_KEY, c); RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param); - if (v instanceof Variable) f.addArgRefinements((Variable) v); + if (v instanceof Variable) + f.addArgRefinements((Variable) v); joint = Predicate.createConjunction(joint, c); } @@ -187,10 +185,11 @@ public void getReturnRefinements(CtReturn ret) { ret.getReturnedExpression().putMetadata(rtc.REFINE_KEY, new Predicate()); CtMethod method = ret.getParent(CtMethod.class); // check if method has refinements - if (rtc.getRefinement(method) == null) return; + if (rtc.getRefinement(method) == null) + return; if (method.getParent() instanceof CtClass) { - RefinedFunction fi = rtc.getContext() - .getFunction(method.getSimpleName(), ((CtClass) method.getParent()).getQualifiedName()); + RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(), + ((CtClass) method.getParent()).getQualifiedName()); List lv = fi.getArguments(); for (Variable v : lv) { @@ -201,13 +200,10 @@ public void getReturnRefinements(CtReturn ret) { String thisName = String.format(rtc.thisFormat, className); rtc.getContext().addInstanceToContext(thisName, c.getReference(), new Predicate(), ret); - String returnVarName = - String.format(retNameFormat, rtc.getContext().getCounter()); + String returnVarName = String.format(retNameFormat, rtc.getContext().getCounter()); Predicate cretRef = rtc.getRefinement(ret.getReturnedExpression()) - .substituteVariable(rtc.WILD_VAR, returnVarName) - .substituteVariable(rtc.THIS, returnVarName); - Predicate cexpectedType = fi.getRefReturn() - .substituteVariable(rtc.WILD_VAR, returnVarName) + .substituteVariable(rtc.WILD_VAR, returnVarName).substituteVariable(rtc.THIS, returnVarName); + Predicate cexpectedType = fi.getRefReturn().substituteVariable(rtc.WILD_VAR, returnVarName) .substituteVariable(rtc.THIS, returnVarName); rtc.getContext().addVarToContext(returnVarName, method.getType(), cretRef, ret); @@ -226,14 +222,15 @@ public void getInvocationRefinements(CtInvocation invocation) { CtExecutableReference cte = invocation.getExecutable(); - if (cte != null) searchMethodInLibrary(cte, invocation); + if (cte != null) + searchMethodInLibrary(cte, invocation); } else if (method.getParent() instanceof CtClass) { String ctype = ((CtClass) method.getParent()).getQualifiedName(); RefinedFunction f = rtc.getContext().getFunction(method.getSimpleName(), ctype); if (f != null) { // inside rtc.context - checkInvocationRefinements( - invocation, invocation.getArguments(), invocation.getTarget(), method.getSimpleName(), ctype); + checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), + method.getSimpleName(), ctype); } else { CtExecutable cet = invocation.getExecutable().getDeclaration(); @@ -272,18 +269,14 @@ private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation String prefix = ctype; String completeName = String.format("%s.%s", prefix, name); if (rtc.getContext().getFunction(completeName, ctype) != null) { - checkInvocationRefinements( - invocation, invocation.getArguments(), invocation.getTarget(), completeName, ctype); + checkInvocationRefinements(invocation, invocation.getArguments(), invocation.getTarget(), completeName, + ctype); } } } - private Map checkInvocationRefinements( - CtElement invocation, - List> arguments, - CtExpression target, - String methodName, - String className) { + private Map checkInvocationRefinements(CtElement invocation, List> arguments, + CtExpression target, String methodName, String className) { // -- Part 1: Check if the invocation is possible int si = arguments.size(); RefinedFunction f = rtc.getContext().getFunction(methodName, className, si); @@ -306,24 +299,22 @@ private Map checkInvocationRefinements( if (methodRef != null) { boolean equalsThis = methodRef.toString().equals("(_ == this)"); // TODO change for better List vars = methodRef.getVariableNames(); - for (String s : vars) if (map.containsKey(s)) methodRef = methodRef.substituteVariable(s, map.get(s)); + for (String s : vars) + if (map.containsKey(s)) + methodRef = methodRef.substituteVariable(s, map.get(s)); String varName = null; if (invocation.getMetadata(rtc.TARGET_KEY) != null) { VariableInstance vi = (VariableInstance) invocation.getMetadata(rtc.TARGET_KEY); methodRef = methodRef.substituteVariable(rtc.THIS, vi.getName()); Variable v = rtc.getContext().getVariableFromInstance(vi); - if (v != null) varName = v.getName(); + if (v != null) + varName = v.getName(); } - String viName = String.format( - rtc.instanceFormat, f.getName(), rtc.getContext().getCounter()); - VariableInstance vi = (VariableInstance) rtc.getContext() - .addInstanceToContext( - viName, - f.getType(), - methodRef.substituteVariable(rtc.WILD_VAR, viName), - invocation); // TODO REVER!! + String viName = String.format(rtc.instanceFormat, f.getName(), rtc.getContext().getCounter()); + VariableInstance vi = (VariableInstance) rtc.getContext().addInstanceToContext(viName, f.getType(), + methodRef.substituteVariable(rtc.WILD_VAR, viName), invocation); // TODO REVER!! if (varName != null && f.hasStateChange() && equalsThis) rtc.getContext().addRefinementInstanceToVariable(varName, viName); invocation.putMetadata(rtc.TARGET_KEY, vi); @@ -351,7 +342,7 @@ private Map mapInvocation(List> arguments, R .getLastVariableInstance(vr.getVariable().getSimpleName()); invStr = ovi.map(o -> o.getName()).orElse(vr.toString()); } else // create new variable with the argument refinement - invStr = createVariableRepresentingArgument(iArg, fArg); + invStr = createVariableRepresentingArgument(iArg, fArg); mapInvocation.put(fArg.getName(), invStr); } @@ -360,17 +351,17 @@ private Map mapInvocation(List> arguments, R private String createVariableRepresentingArgument(CtExpression iArg, Variable fArg) { Predicate met = (Predicate) iArg.getMetadata(rtc.REFINE_KEY); - if (met == null) met = new Predicate(); + if (met == null) + met = new Predicate(); if (!met.getVariableNames().contains(rtc.WILD_VAR)) met = Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), met); - String nVar = String.format( - rtc.instanceFormat, fArg.getName(), rtc.getContext().getCounter()); + String nVar = String.format(rtc.instanceFormat, fArg.getName(), rtc.getContext().getCounter()); rtc.getContext().addInstanceToContext(nVar, fArg.getType(), met.substituteVariable(rtc.WILD_VAR, nVar), iArg); return nVar; } - private void checkParameters( - CtElement invocation, List> arguments, RefinedFunction f, Map map) { + private void checkParameters(CtElement invocation, List> arguments, RefinedFunction f, + Map map) { List> invocationParams = arguments; List functionParams = f.getArguments(); for (int i = 0; i < invocationParams.size(); i++) { @@ -378,15 +369,17 @@ private void checkParameters( Predicate c = fArg.getMainRefinement(); 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)); + for (String s : vars) + if (map.containsKey(s)) + c = c.substituteVariable(s, map.get(s)); rtc.checkSMT(c, invocation); } } // IN CONSTRUCTION _ NOT USED @SuppressWarnings("unused") - private void applyRefinementsToArguments( - CtElement element, List> arguments, RefinedFunction f, Map map) { + private void applyRefinementsToArguments(CtElement element, List> arguments, RefinedFunction f, + Map map) { Context context = rtc.getContext(); List> invocationParams = arguments; List functionParams = f.getArguments(); @@ -424,11 +417,12 @@ public void loadFunctionInfo(CtExecutable method) { className = ((CtInterface) method.getParent()).getQualifiedName(); } if (className != null) { - RefinedFunction fi = getRefinementFunction( - method.getSimpleName(), className, method.getParameters().size()); + RefinedFunction fi = getRefinementFunction(method.getSimpleName(), className, + method.getParameters().size()); if (fi != null) { List lv = fi.getArguments(); - for (Variable v : lv) rtc.getContext().addVarToContext(v); + for (Variable v : lv) + rtc.getContext().addVarToContext(v); } else { assert false; // Method should already be in context. Should not arrive this point in 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 44b400de..3f31da92 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 @@ -62,7 +62,8 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws Pars Predicate oper; CtElement parent = operator.getParent(); - if (parent instanceof CtAnnotation) return; // Operations in annotations are not handled here + if (parent instanceof CtAnnotation) + return; // Operations in annotations are not handled here if (parent instanceof CtAssignment && ((CtAssignment) parent).getAssigned() instanceof CtVariableWrite) { @@ -81,8 +82,7 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws Pars List types = Arrays.asList(rtc.implementedTypes); if (type.contentEquals("boolean")) { operator.putMetadata(rtc.REFINE_KEY, oper); - if (parent instanceof CtLocalVariable - || parent instanceof CtUnaryOperator + if (parent instanceof CtLocalVariable || parent instanceof CtUnaryOperator || parent instanceof CtReturn) operator.putMetadata(rtc.REFINE_KEY, Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), oper)); } else if (types.contains(type)) { @@ -101,7 +101,7 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws Pars * * @throws ParsingException */ - @SuppressWarnings({"unchecked"}) + @SuppressWarnings({ "unchecked" }) public void getUnaryOpRefinements(CtUnaryOperator operator) throws ParsingException { CtExpression ex = (CtExpression) operator.getOperand(); String name = rtc.freshFormat; @@ -110,8 +110,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws Parsin CtVariableWrite w = (CtVariableWrite) ex; name = w.getVariable().getSimpleName(); all = getRefinementUnaryVariableWrite(ex, operator, w, name); - rtc.checkVariableRefinements( - all, name, w.getType(), operator, w.getVariable().getDeclaration()); + rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; } else if (ex instanceof CtVariableRead) { @@ -138,15 +137,18 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws Parsin String newName; if (!name.equals(rtc.freshFormat)) newName = String.format(rtc.instanceFormat, name, rtc.getContext().getCounter()); - else newName = String.format(name, rtc.getContext().getCounter()); + else + newName = String.format(name, rtc.getContext().getCounter()); Predicate newMeta = metadata.substituteVariable(rtc.WILD_VAR, newName); Predicate unOp = getOperatorFromKind(operator.getKind(), operator); CtElement p = operator.getParent(); Predicate opS = unOp.substituteVariable(rtc.WILD_VAR, newName); - if (p instanceof CtIf) all = opS; - else all = Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), opS); // TODO SEE IF () IN OPS IS NEEDED + if (p instanceof CtIf) + all = opS; + else + all = Predicate.createEquals(Predicate.createVar(rtc.WILD_VAR), opS); // TODO SEE IF () IN OPS IS NEEDED rtc.getContext().addInstanceToContext(newName, ex.getType(), newMeta, operator); operator.putMetadata(rtc.REFINE_KEY, all); @@ -182,19 +184,14 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtExpres * * @throws ParsingException */ - private Predicate getOperationRefinements( - CtBinaryOperator operator, CtVariableWrite parentVar, CtExpression element) - throws ParsingException { + private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariableWrite parentVar, + CtExpression element) throws ParsingException { if (element instanceof CtFieldRead) { CtFieldRead field = ((CtFieldRead) element); if (field.getVariable().getSimpleName().equals("length")) { String name = String.format(rtc.freshFormat, rtc.getContext().getCounter()); - rtc.getContext() - .addVarToContext( - name, - element.getType(), - rtc.getRefinement(element).substituteVariable(rtc.WILD_VAR, name), - field); + rtc.getContext().addVarToContext(name, element.getType(), + rtc.getRefinement(element).substituteVariable(rtc.WILD_VAR, name), field); return Predicate.createVar(name); } } @@ -202,7 +199,8 @@ private Predicate getOperationRefinements( if (element instanceof CtVariableRead) { CtVariableRead elemVar = (CtVariableRead) element; String elemName = elemVar.getVariable().getSimpleName(); - if (elemVar instanceof CtFieldRead) elemName = String.format(rtc.thisFormat, elemName); + if (elemVar instanceof CtFieldRead) + elemName = String.format(rtc.thisFormat, elemName); Predicate elem_ref = rtc.getContext().getVariableRefinements(elemName); String returnName = elemName; @@ -211,12 +209,11 @@ private Predicate getOperationRefinements( // No need for specific values if (parent != null && !(parent instanceof CtIfImpl)) { elem_ref = rtc.getRefinement(elemVar); - String newName = String.format( - rtc.instanceFormat, elemName, rtc.getContext().getCounter()); + String newName = String.format(rtc.instanceFormat, elemName, rtc.getContext().getCounter()); Predicate newElem_ref = elem_ref.substituteVariable(rtc.WILD_VAR, newName); // String newElem_ref = elem_ref.replace(rtc.WILD_VAR, newName); - RefinedVariable newVi = - rtc.getContext().addVarToContext(newName, elemVar.getType(), newElem_ref, elemVar); + RefinedVariable newVi = rtc.getContext().addVarToContext(newName, elemVar.getType(), newElem_ref, + elemVar); rtc.getContext().addSpecificVariable(newVi); returnName = newName; } @@ -235,11 +232,7 @@ private Predicate getOperationRefinements( } else if (element instanceof CtUnaryOperator) { Predicate a = (Predicate) element.getMetadata(rtc.REFINE_KEY); a = a.substituteVariable(rtc.WILD_VAR, ""); - String s = a.toString() - .replace("(", "") - .replace(")", "") - .replace("==", "") - .replace(" ", ""); // TODO + String s = a.toString().replace("(", "").replace(")", "").replace("==", "").replace(" ", ""); // TODO // IMPROVE return new Predicate(String.format("(%s)", s), element, rtc.getErrorEmitter()); @@ -251,7 +244,8 @@ private Predicate getOperationRefinements( CtInvocation inv = (CtInvocation) element; CtExecutable method = inv.getExecutable().getDeclaration(); - if (method == null) return getOperationRefinementFromExternalLib(inv, operator); + if (method == null) + return getOperationRefinementFromExternalLib(inv, operator); // Get function refinements with non_used variables String met = ((CtClass) method.getParent()).getQualifiedName(); // TODO check @@ -314,11 +308,9 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv, CtB * * @throws ParsingException */ - private Predicate getRefinementUnaryVariableWrite( - CtExpression ex, CtUnaryOperator operator, CtVariableWrite w, String name) - throws ParsingException { - String newName = - String.format(rtc.instanceFormat, name, rtc.getContext().getCounter()); + private Predicate getRefinementUnaryVariableWrite(CtExpression ex, CtUnaryOperator operator, + CtVariableWrite w, String name) throws ParsingException { + String newName = String.format(rtc.instanceFormat, name, rtc.getContext().getCounter()); CtVariable varDecl = w.getVariable().getDeclaration(); Predicate metadada = rtc.getContext().getVariableRefinements(varDecl.getSimpleName()); @@ -343,69 +335,69 @@ private Predicate getRefinementUnaryVariableWrite( */ private String getOperatorFromKind(BinaryOperatorKind kind) { switch (kind) { - case PLUS: - return Utils.PLUS; - case MINUS: - return Utils.MINUS; - case MUL: - return Utils.MUL; - case DIV: - return Utils.DIV; - case MOD: - return Utils.MOD; - - case AND: - return Utils.AND; - case OR: - return Utils.OR; - - case EQ: - return Utils.EQ; - case NE: - return Utils.NEQ; - case GE: - return Utils.GE; - case GT: - return Utils.GT; - case LE: - return Utils.LE; - case LT: - return Utils.LT; - default: - return null; - // TODO COMPLETE WITH MORE OPERANDS + case PLUS: + return Utils.PLUS; + case MINUS: + return Utils.MINUS; + case MUL: + return Utils.MUL; + case DIV: + return Utils.DIV; + case MOD: + return Utils.MOD; + + case AND: + return Utils.AND; + case OR: + return Utils.OR; + + case EQ: + return Utils.EQ; + case NE: + return Utils.NEQ; + case GE: + return Utils.GE; + case GT: + return Utils.GT; + case LE: + return Utils.LE; + case LT: + return Utils.LT; + default: + return null; + // TODO COMPLETE WITH MORE OPERANDS } } private Predicate getOperatorFromKind(UnaryOperatorKind kind, CtElement elem) throws ParsingException { String ret = null; switch (kind) { - case POSTINC: - ret = rtc.WILD_VAR + " + 1"; - break; - case POSTDEC: - ret = rtc.WILD_VAR + " - 1"; - break; - case PREINC: - ret = rtc.WILD_VAR + " + 1"; - break; - case PREDEC: - ret = rtc.WILD_VAR + " - 1"; - break; - case COMPL: - ret = "(32 & " + rtc.WILD_VAR + ")"; - break; - case NOT: - ret = "!" + rtc.WILD_VAR; - break; - case POS: - ret = "0 + " + rtc.WILD_VAR; - break; - case NEG: - ret = "-" + rtc.WILD_VAR; - break; - default: - throw new ParsingException(kind + "operation not supported"); + case POSTINC: + ret = rtc.WILD_VAR + " + 1"; + break; + case POSTDEC: + ret = rtc.WILD_VAR + " - 1"; + break; + case PREINC: + ret = rtc.WILD_VAR + " + 1"; + break; + case PREDEC: + ret = rtc.WILD_VAR + " - 1"; + break; + case COMPL: + ret = "(32 & " + rtc.WILD_VAR + ")"; + break; + case NOT: + ret = "!" + rtc.WILD_VAR; + break; + case POS: + ret = "0 + " + rtc.WILD_VAR; + break; + case NEG: + ret = "-" + rtc.WILD_VAR; + break; + default: + throw new ParsingException(kind + "operation not supported"); } return new Predicate(ret, elem, rtc.getErrorEmitter()); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java index 25ce7820..ead19e39 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java @@ -18,8 +18,8 @@ public class AuxHierarchyRefinememtsPassage { - public static void checkFunctionInSupertypes( - CtClass klass, CtMethod method, RefinedFunction f, TypeChecker tc) { + public static void checkFunctionInSupertypes(CtClass klass, CtMethod method, RefinedFunction f, + TypeChecker tc) { String name = method.getSimpleName(); int size = method.getParameters().size(); if (klass.getSuperInterfaces().size() > 0) { // implemented interfaces @@ -37,30 +37,25 @@ public static void checkFunctionInSupertypes( } } - static void transferRefinements( - RefinedFunction superFunction, RefinedFunction function, CtMethod method, TypeChecker tc) { + static void transferRefinements(RefinedFunction superFunction, RefinedFunction function, CtMethod method, + TypeChecker tc) { HashMap super2function = getParametersMap(superFunction, function, tc, method); transferReturnRefinement(superFunction, function, method, tc, super2function); transferArgumentsRefinements(superFunction, function, method, tc, super2function); transferStateRefinements(superFunction, function, method, tc); } - private static HashMap getParametersMap( - RefinedFunction superFunction, RefinedFunction function, TypeChecker tc, CtMethod method) { + private static HashMap getParametersMap(RefinedFunction superFunction, RefinedFunction function, + TypeChecker tc, CtMethod method) { List superArgs = superFunction.getArguments(); List fArgs = function.getArguments(); HashMap m = new HashMap(); for (int i = 0; i < fArgs.size(); i++) { - String newName = String.format( - tc.instanceFormat, fArgs.get(i).getName(), tc.getContext().getCounter()); + String newName = String.format(tc.instanceFormat, fArgs.get(i).getName(), tc.getContext().getCounter()); m.put(superArgs.get(i).getName(), newName); m.put(fArgs.get(i).getName(), newName); - RefinedVariable rv = tc.getContext() - .addVarToContext( - newName, - superArgs.get(i).getType(), - new Predicate(), - method.getParameters().get(i)); + RefinedVariable rv = tc.getContext().addVarToContext(newName, superArgs.get(i).getType(), new Predicate(), + method.getParameters().get(i)); for (CtTypeReference t : fArgs.get(i).getSuperTypes()) { rv.addSuperType(t); } @@ -68,12 +63,8 @@ private static HashMap getParametersMap( return m; } - static void transferArgumentsRefinements( - RefinedFunction superFunction, - RefinedFunction function, - CtMethod method, - TypeChecker tc, - HashMap super2function) { + static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedFunction function, + CtMethod method, TypeChecker tc, HashMap super2function) { List superArgs = superFunction.getArguments(); List args = function.getArguments(); List> params = method.getParameters(); @@ -91,21 +82,19 @@ static void transferArgumentsRefinements( boolean f = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition()); if (!f) { // ErrorPrinter.printError(method, argRef, superArgRef); - if (!tc.getErrorEmitter().foundError()) tc.createError(method, argRef, superArgRef, ""); + if (!tc.getErrorEmitter().foundError()) + tc.createError(method, argRef, superArgRef, ""); } } } } - static void transferReturnRefinement( - RefinedFunction superFunction, - RefinedFunction function, - CtMethod method, - TypeChecker tc, - HashMap super2function) { + static void transferReturnRefinement(RefinedFunction superFunction, RefinedFunction function, CtMethod method, + TypeChecker tc, HashMap super2function) { Predicate functionRef = function.getRefinement(); Predicate superRef = superFunction.getRefinement(); - if (functionRef.isBooleanTrue()) function.setRefinement(superRef); + if (functionRef.isBooleanTrue()) + function.setRefinement(superRef); else { String name = String.format(tc.freshFormat, tc.getContext().getCounter()); tc.getContext().addVarToContext(name, superFunction.getType(), new Predicate(), method); @@ -113,14 +102,12 @@ static void transferReturnRefinement( // functionRef) functionRef = functionRef.substituteVariable(tc.WILD_VAR, name); superRef = superRef.substituteVariable(tc.WILD_VAR, name); - for (String m : super2function.keySet()) superRef = superRef.substituteVariable(m, super2function.get(m)); + for (String m : super2function.keySet()) + superRef = superRef.substituteVariable(m, super2function.get(m)); for (String m : super2function.keySet()) functionRef = functionRef.substituteVariable(m, super2function.get(m)); - tc.checkStateSMT( - functionRef, - superRef, - method, + tc.checkStateSMT(functionRef, superRef, method, "Return Refinement of Subclass must be subtype of the Return Refinement of the" + " Superclass"); // boolean f = tc.checkStateSMT(functionRef, superRef, method); // if(!f) @@ -128,23 +115,24 @@ static void transferReturnRefinement( } } - static Optional functionInInterface( - CtClass klass, String simpleName, int size, TypeChecker tc) { + 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()) + List st = klass.getSuperInterfaces().stream().map(p -> p.getQualifiedName()) .collect(Collectors.toList()); for (RefinedFunction rf : lrf) { - if (st.contains(rf.getTargetClass())) return Optional.of(rf); // TODO only works for 1 interface + if (st.contains(rf.getTargetClass())) + return Optional.of(rf); // TODO only works for 1 interface } return Optional.empty(); } - private static void transferStateRefinements( - RefinedFunction superFunction, RefinedFunction subFunction, CtMethod method, TypeChecker tc) { + private static void transferStateRefinements(RefinedFunction superFunction, RefinedFunction subFunction, + CtMethod method, TypeChecker tc) { if (superFunction.hasStateChange()) { if (!subFunction.hasStateChange()) { - for (ObjectState o : superFunction.getAllStates()) subFunction.addStates(o.clone()); + for (ObjectState o : superFunction.getAllStates()) + subFunction.addStates(o.clone()); } else { List superStates = superFunction.getAllStates(); List subStates = subFunction.getAllStates(); @@ -152,24 +140,15 @@ private static void transferStateRefinements( ObjectState superState = superStates.get(i); ObjectState subState = subStates.get(i); - String thisName = - String.format(tc.freshFormat, tc.getContext().getCounter()); - createVariableInContext( - thisName, - tc, - subFunction, - superFunction, - method.getParameters().get(i)); + String thisName = String.format(tc.freshFormat, tc.getContext().getCounter()); + createVariableInContext(thisName, tc, subFunction, superFunction, method.getParameters().get(i)); Predicate superConst = matchVariableNames(tc.THIS, thisName, superState.getFrom()); - Predicate subConst = - matchVariableNames(tc.THIS, thisName, superFunction, subFunction, subState.getFrom()); + Predicate subConst = matchVariableNames(tc.THIS, thisName, superFunction, subFunction, + subState.getFrom()); // fromSup <: fromSub <==> fromSup is sub type and fromSub is expectedType - tc.checkStateSMT( - superConst, - subConst, - method, + tc.checkStateSMT(superConst, subConst, method, "FROM State from Superclass must be subtype of FROM State from Subclass"); // boolean correct = tc.checkStateSMT(superConst, subConst, method); // if(!correct) ErrorPrinter.printError(method, subState.getFrom(), @@ -178,10 +157,7 @@ private static void transferStateRefinements( superConst = matchVariableNames(tc.THIS, thisName, superState.getTo()); subConst = matchVariableNames(tc.THIS, thisName, superFunction, subFunction, subState.getTo()); // toSub <: toSup <==> ToSub is sub type and toSup is expectedType - tc.checkStateSMT( - subConst, - superConst, - method, + tc.checkStateSMT(subConst, superConst, method, "TO State from Subclass must be subtype of TO State from Superclass"); // boolean correct = tc.checkStateSMT(subConst, superConst, method); // if(!correct) ErrorPrinter.printError(method, subState.getTo(), @@ -191,18 +167,10 @@ private static void transferStateRefinements( } } - private static void createVariableInContext( - String thisName, - TypeChecker tc, - RefinedFunction subFunction, - RefinedFunction superFunction, - CtParameter ctParameter) { - RefinedVariable rv = tc.getContext() - .addVarToContext( - thisName, - Utils.getType(subFunction.getTargetClass(), tc.getFactory()), - new Predicate(), - ctParameter); + private static void createVariableInContext(String thisName, TypeChecker tc, RefinedFunction subFunction, + RefinedFunction superFunction, CtParameter ctParameter) { + 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 @@ -220,8 +188,8 @@ private static void createVariableInContext( * * @return */ - private static Predicate matchVariableNames( - String fromName, String thisName, RefinedFunction superFunction, RefinedFunction subFunction, Predicate c) { + private static Predicate matchVariableNames(String fromName, String thisName, RefinedFunction superFunction, + RefinedFunction subFunction, Predicate c) { Predicate nc = c.substituteVariable(fromName, thisName); List superArgs = superFunction.getArguments(); List subArgs = subFunction.getArguments(); 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 b9b6c6f9..f21329aa 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 @@ -27,7 +27,7 @@ public class AuxStateHandler { * * @throws ParsingException */ - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public static void handleConstructorState(CtConstructor c, RefinedFunction f, TypeChecker tc) throws ParsingException { List> an = getStateAnnotation(c); @@ -56,16 +56,16 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, * * @throws ParsingException */ - @SuppressWarnings({"rawtypes"}) - private static void setConstructorStates( - RefinedFunction f, List> anns, TypeChecker tc, CtElement element) - throws ParsingException { + @SuppressWarnings({ "rawtypes" }) + private static void setConstructorStates(RefinedFunction f, List> anns, + TypeChecker tc, CtElement element) throws ParsingException { List l = new ArrayList<>(); for (CtAnnotation an : anns) { Map m = an.getAllValues(); String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to")); ObjectState state = new ObjectState(); - if (to != null) state.setTo(new Predicate(to, element, tc.getErrorEmitter())); + if (to != null) + state.setTo(new Predicate(to, element, tc.getErrorEmitter())); l.add(state); } f.setAllStates(l); @@ -75,13 +75,13 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { String[] path = f.getTargetClass().split("\\."); String klass = path[path.length - 1]; - Predicate[] s = {Predicate.createVar(tc.THIS)}; + Predicate[] s = { Predicate.createVar(tc.THIS) }; Predicate c = new Predicate(); List sets = getDifferentSets(tc, klass); // ?? for (GhostFunction sg : sets) { if (sg.getReturnType().toString().equals("int")) { - Predicate p = Predicate.createEquals( - Predicate.createInvocation(sg.getName(), s), Predicate.createLit("0", Utils.INT)); + Predicate p = Predicate.createEquals(Predicate.createInvocation(sg.getName(), s), + Predicate.createLit("0", Utils.INT)); c = Predicate.createConjunction(c, p); } else { // TODO: Implement other stuff @@ -140,9 +140,8 @@ public static void handleMethodState(CtMethod method, RefinedFunction f, Type * * @throws ParsingException */ - private static void setFunctionStates( - RefinedFunction f, List> anns, TypeChecker tc, CtElement element) - throws ParsingException { + private static void setFunctionStates(RefinedFunction f, List> anns, + TypeChecker tc, CtElement element) throws ParsingException { List l = new ArrayList<>(); for (CtAnnotation an : anns) { l.add(getStates(an, f, tc, element)); @@ -150,10 +149,9 @@ private static void setFunctionStates( f.setAllStates(l); } - @SuppressWarnings({"rawtypes"}) - private static ObjectState getStates( - CtAnnotation ctAnnotation, RefinedFunction f, TypeChecker tc, CtElement e) - throws ParsingException { + @SuppressWarnings({ "rawtypes" }) + private static ObjectState getStates(CtAnnotation ctAnnotation, RefinedFunction f, + TypeChecker tc, CtElement e) throws ParsingException { Map m = ctAnnotation.getAllValues(); String from = TypeCheckingUtils.getStringFromAnnotation(m.get("from")); String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to")); @@ -178,15 +176,13 @@ private static ObjectState getStates( return state; } - private static Predicate createStatePredicate( - String value, /* RefinedFunction f */ String targetClass, TypeChecker tc, CtElement e, boolean isTo) - throws ParsingException { + private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass, + TypeChecker tc, CtElement e, boolean isTo) throws ParsingException { Predicate p = new Predicate(value, e, tc.getErrorEmitter()); String t = targetClass; // f.getTargetClass(); CtTypeReference r = tc.getFactory().Type().createReference(t); - String nameOld = - String.format(tc.instanceFormat, tc.THIS, tc.getContext().getCounter()); + String nameOld = String.format(tc.instanceFormat, tc.THIS, tc.getContext().getCounter()); String name = String.format(tc.instanceFormat, tc.THIS, tc.getContext().getCounter()); tc.getContext().addVarToContext(name, r, new Predicate(), e); tc.getContext().addVarToContext(nameOld, r, new Predicate(), e); @@ -250,8 +246,8 @@ private static Predicate addOldStates(Predicate p, Predicate th, List map, CtConstructorCall ctConstructorCall) { + public static void constructorStateMetadata(String refKey, RefinedFunction f, Map map, + CtConstructorCall ctConstructorCall) { List oc = f.getToStates(); if (oc.size() > 0) { // && !oc.get(0).isBooleanTrue()) // ctConstructorCall.putMetadata(stateKey, oc.get(0)); @@ -295,8 +291,8 @@ public static void addStateRefinements(TypeChecker tc, String varName, CtExpress * @param map * @param invocation */ - public static void checkTargetChanges( - TypeChecker tc, RefinedFunction f, CtExpression target2, Map map, CtElement invocation) { + public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpression target2, + Map map, CtElement invocation) { String parentTargetName = searchFistVariableTarget(tc, target2, invocation); VariableInstance target = getTarget(tc, invocation); if (target != null) { @@ -326,8 +322,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { return; } - String parentTargetName = - ((CtVariableRead) fw.getTarget()).getVariable().getSimpleName(); + String parentTargetName = ((CtVariableRead) fw.getTarget()).getVariable().getSimpleName(); Optional invocation_callee = tc.getContext().getLastVariableInstance(parentTargetName); if (!invocation_callee.isPresent()) { @@ -337,8 +332,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { VariableInstance vi = invocation_callee.get(); String instanceName = vi.getName(); - Predicate prevState = vi.getRefinement() - .substituteVariable(tc.WILD_VAR, instanceName) + Predicate prevState = vi.getRefinement().substituteVariable(tc.WILD_VAR, instanceName) .substituteVariable(parentTargetName, instanceName); // StateRefinement(from="true", to="n(this)=this#n") @@ -351,19 +345,17 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { stateChange.setFrom(fromPredicate); stateChange.setTo(toPredicate); } catch (ParsingException e) { - ErrorHandler.printCostumeError( - fw, - "ParsingException while constructing assignment update for `" + fw + "` in class `" - + fw.getVariable().getDeclaringType() + "` : " + e.getMessage(), - tc.getErrorEmitter()); + ErrorHandler + .printCostumeError(fw, + "ParsingException while constructing assignment update for `" + fw + "` in class `" + + fw.getVariable().getDeclaringType() + "` : " + e.getMessage(), + tc.getErrorEmitter()); return; } // replace "state(this)" to "state(whatever method is called from) and so on" - Predicate expectState = stateChange - .getFrom() - .substituteVariable(tc.THIS, instanceName) + Predicate expectState = stateChange.getFrom().substituteVariable(tc.THIS, instanceName) .changeOldMentions(vi.getName(), instanceName, tc.getErrorEmitter()); if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition @@ -374,18 +366,15 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { return; } - String newInstanceName = String.format( - tc.instanceFormat, parentTargetName, tc.getContext().getCounter()); - Predicate transitionedState = stateChange - .getTo() - .substituteVariable(tc.WILD_VAR, newInstanceName) + String newInstanceName = String.format(tc.instanceFormat, parentTargetName, tc.getContext().getCounter()); + Predicate transitionedState = stateChange.getTo().substituteVariable(tc.WILD_VAR, newInstanceName) .substituteVariable(tc.THIS, newInstanceName); transitionedState = checkOldMentions(transitionedState, instanceName, newInstanceName, tc); // update of stata of new instance of this#n#(whatever it was + 1) - VariableInstance vi2 = (VariableInstance) - tc.getContext().addInstanceToContext(newInstanceName, vi.getType(), vi.getRefinement(), fw); + VariableInstance vi2 = (VariableInstance) tc.getContext().addInstanceToContext(newInstanceName, vi.getType(), + vi.getRefinement(), fw); vi2.setRefinement(transitionedState); RefinedVariable rv = tc.getContext().getVariableByName(parentTargetName); @@ -413,19 +402,15 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) { * * @return */ - private static Predicate changeState( - TypeChecker tc, - VariableInstance vi, - /* RefinedFunction f */ List stateChanges, - String name, - Map map, + private static Predicate changeState(TypeChecker tc, VariableInstance vi, + /* RefinedFunction f */ List stateChanges, String name, Map map, CtElement invocation) { if (vi.getRefinement() == null) { return new Predicate(); } String instanceName = vi.getName(); - Predicate prevState = - vi.getRefinement().substituteVariable(tc.WILD_VAR, instanceName).substituteVariable(name, instanceName); + Predicate prevState = vi.getRefinement().substituteVariable(tc.WILD_VAR, instanceName).substituteVariable(name, + instanceName); // List stateChanges = f.getAllStates(); @@ -450,11 +435,8 @@ private static Predicate changeState( found = tc.checksStateSMT(prevCheck, expectState, invocation.getPosition()); if (found && stateChange.hasTo()) { - String newInstanceName = - String.format(tc.instanceFormat, name, tc.getContext().getCounter()); - Predicate transitionedState = stateChange - .getTo() - .substituteVariable(tc.WILD_VAR, newInstanceName) + String newInstanceName = String.format(tc.instanceFormat, name, tc.getContext().getCounter()); + Predicate transitionedState = stateChange.getTo().substituteVariable(tc.WILD_VAR, newInstanceName) .substituteVariable(tc.THIS, newInstanceName); for (String s : map.keySet()) { transitionedState = transitionedState.substituteVariable(s, map.get(s)); @@ -466,11 +448,8 @@ private static Predicate changeState( } } if (!found && !tc.getErrorEmitter().foundError()) { // Reaches the end of stateChange no matching states - String states = stateChanges.stream() - .filter(ObjectState::hasFrom) - .map(ObjectState::getFrom) - .map(Predicate::toString) - .collect(Collectors.joining(",")); + String states = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom) + .map(Predicate::toString).collect(Collectors.joining(",")); String simpleInvocation = invocation.toString(); // .getExecutable().toString(); tc.createStateMismatchError(invocation, simpleInvocation, prevState, states); @@ -499,8 +478,8 @@ private static Predicate changeVarsFields(Predicate pred, TypeChecker tc) { return noOld; } - private static Predicate checkOldMentions( - Predicate transitionedState, String instanceName, String newInstanceName, TypeChecker tc) { + private static Predicate checkOldMentions(Predicate transitionedState, String instanceName, String newInstanceName, + TypeChecker tc) { return transitionedState.changeOldMentions(instanceName, newInstanceName, tc.getErrorEmitter()); } @@ -514,18 +493,15 @@ private static Predicate checkOldMentions( * * @return */ - private static Predicate sameState( - TypeChecker tc, VariableInstance variableInstance, String name, CtElement invocation) { + private static Predicate sameState(TypeChecker tc, VariableInstance variableInstance, String name, + CtElement invocation) { // if(variableInstance.getState() != null) { if (variableInstance.getRefinement() != null) { - String newInstanceName = - String.format(tc.instanceFormat, name, tc.getContext().getCounter()); + String newInstanceName = String.format(tc.instanceFormat, name, tc.getContext().getCounter()); // Predicate c = // variableInstance.getState().substituteVariable(variableInstance.getName(), // newInstanceName); - Predicate c = variableInstance - .getRefinement() - .substituteVariable(tc.WILD_VAR, newInstanceName) + Predicate c = variableInstance.getRefinement().substituteVariable(tc.WILD_VAR, newInstanceName) .substituteVariable(variableInstance.getName(), newInstanceName); addInstanceWithState(tc, name, newInstanceName, variableInstance, c, invocation); @@ -546,15 +522,10 @@ private static Predicate sameState( * * @return */ - private static String addInstanceWithState( - TypeChecker tc, - String superName, - String name2, - VariableInstance prevInstance, - Predicate transitionedState, - CtElement invocation) { - VariableInstance vi2 = (VariableInstance) tc.getContext() - .addInstanceToContext(name2, prevInstance.getType(), prevInstance.getRefinement(), invocation); + private static String addInstanceWithState(TypeChecker tc, String superName, String name2, + VariableInstance prevInstance, Predicate transitionedState, CtElement invocation) { + VariableInstance vi2 = (VariableInstance) tc.getContext().addInstanceToContext(name2, prevInstance.getType(), + prevInstance.getRefinement(), invocation); // vi2.setState(transitionedState); vi2.setRefinement(transitionedState); RefinedVariable rv = tc.getContext().getVariableByName(superName); @@ -593,11 +564,9 @@ static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElem invocation.putMetadata(tc.TARGET_KEY, invocation_callee.get()); } else if (target2.getMetadata(tc.TARGET_KEY) == null) { RefinedVariable var = tc.getContext().getVariableByName(name); - String nName = - String.format(tc.instanceFormat, name, tc.getContext().getCounter()); - RefinedVariable rv = tc.getContext() - .addInstanceToContext( - nName, var.getType(), var.getRefinement().substituteVariable(name, nName), target2); + String nName = String.format(tc.instanceFormat, name, tc.getContext().getCounter()); + RefinedVariable rv = tc.getContext().addInstanceToContext(nName, var.getType(), + var.getRefinement().substituteVariable(name, nName), target2); tc.getContext().addRefinementInstanceToVariable(name, nName); invocation.putMetadata(tc.TARGET_KEY, rv); } @@ -622,11 +591,8 @@ static VariableInstance getTarget(TypeChecker tc, CtElement invocation) { } private static List> getStateAnnotation(CtElement element) { - return element.getAnnotations().stream() - .filter(ann -> ann.getActualAnnotation() - .annotationType() - .getCanonicalName() - .contentEquals("liquidjava.specification.StateRefinement")) + return element.getAnnotations().stream().filter(ann -> ann.getActualAnnotation().annotationType() + .getCanonicalName().contentEquals("liquidjava.specification.StateRefinement")) .collect(Collectors.toList()); // List> l = new ArrayList getVariableNames() { } public List getStateInvocations(List lgs) { - if (lgs == null) return new ArrayList<>(); + if (lgs == null) + return new ArrayList<>(); List all = lgs.stream().map(p -> p.getName()).collect(Collectors.toList()); List toAdd = new ArrayList<>(); exp.getStateInvocations(toAdd, all); List gh = new ArrayList<>(); for (String n : toAdd) { - for (GhostState g : lgs) if (g.getName().equals(n)) gh.add(g); + for (GhostState g : lgs) + if (g.getName().equals(n)) + gh.add(g); } return gh; @@ -145,12 +149,14 @@ private void expressionGetOldVariableNames(Expression exp, List ls) { if (fi.getName().equals(Utils.OLD)) { List le = fi.getArgs(); for (Expression e : le) { - if (e instanceof Var) ls.add(((Var) e).getName()); + if (e instanceof Var) + ls.add(((Var) e).getName()); } } } if (exp.hasChildren()) { - for (var ch : exp.getChildren()) expressionGetOldVariableNames(ch, ls); + for (var ch : exp.getChildren()) + expressionGetOldVariableNames(ch, ls); } } @@ -158,7 +164,7 @@ public Predicate changeStatesToRefinements(List ghostState, String[] Map nameRefinementMap = new HashMap<>(); for (GhostState gs : ghostState) if (gs.getRefinement() != null) // is a state and not a ghost state - nameRefinementMap.put(gs.getName(), innerParse(gs.getRefinement().toString(), ee)); + nameRefinementMap.put(gs.getName(), innerParse(gs.getRefinement().toString(), ee)); Expression e = exp.substituteState(nameRefinementMap, toChange); return new Predicate(e); @@ -201,13 +207,18 @@ public static Predicate createITE(Predicate c1, Predicate c2, Predicate c3) { public static Predicate createLit(String value, String type) { Expression ex; - if (type.equals(Utils.BOOLEAN)) ex = new LiteralBoolean(value); - else if (type.equals(Utils.INT)) ex = new LiteralInt(value); - else if (type.equals(Utils.DOUBLE)) ex = new LiteralReal(value); - else if (type.equals(Utils.SHORT)) ex = new LiteralInt(value); - else if (type.equals(Utils.LONG)) ex = new LiteralReal(value); + if (type.equals(Utils.BOOLEAN)) + ex = new LiteralBoolean(value); + else if (type.equals(Utils.INT)) + ex = new LiteralInt(value); + else if (type.equals(Utils.DOUBLE)) + ex = new LiteralReal(value); + else if (type.equals(Utils.SHORT)) + ex = new LiteralInt(value); + else if (type.equals(Utils.LONG)) + ex = new LiteralReal(value); else // if(type.equals(Utils.DOUBLE)) - ex = new LiteralReal(value); + ex = new LiteralReal(value); return new Predicate(ex); } @@ -221,7 +232,8 @@ public static Predicate createVar(String name) { public static Predicate createInvocation(String name, Predicate... Predicates) { List le = new ArrayList<>(); - for (Predicate c : Predicates) le.add(c.getExpression()); + for (Predicate c : Predicates) + le.add(c.getExpression()); return new Predicate(new FunctionInvocation(name, le)); } } 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 eea8c708..cdd89591 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 @@ -11,7 +11,8 @@ public class AliasInvocation extends Expression { public AliasInvocation(String name, List args) { this.name = name; - for (Expression e : args) addChild(e); + for (Expression e : args) + addChild(e); } public String getName() { @@ -38,18 +39,21 @@ public String toString() { @Override public void getVariableNames(List toAdd) { - for (Expression e : getArgs()) e.getVariableNames(toAdd); + for (Expression e : getArgs()) + e.getVariableNames(toAdd); } @Override public void getStateInvocations(List toAdd, List all) { - for (Expression e : getArgs()) e.getStateInvocations(toAdd, all); + for (Expression e : getArgs()) + e.getStateInvocations(toAdd, all); } @Override public Expression clone() { List le = new ArrayList<>(); - for (Expression e : getArgs()) le.add(e.clone()); + for (Expression e : getArgs()) + le.add(e.clone()); return new AliasInvocation(name, le); } @@ -69,16 +73,23 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; AliasInvocation other = (AliasInvocation) obj; if (getArgs() == null) { - if (other.getArgs() != null) return false; - } else if (!getArgs().equals(other.getArgs())) return false; + if (other.getArgs() != null) + return false; + } 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; + if (other.name != null) + return false; + } else if (!name.equals(other.name)) + return false; return true; } } 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 dc0c2f3a..ad7973cd 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 @@ -31,11 +31,7 @@ public boolean isLogicOperation() { } public boolean isBooleanOperation() { - return op.equals("==") - || op.equals("!=") - || op.equals(">=") - || op.equals(">") - || op.equals("<=") + return op.equals("==") || op.equals("!=") || op.equals(">=") || op.equals(">") || op.equals("<=") || op.equals("<"); } @@ -52,43 +48,42 @@ public Expr eval(TranslatorToZ3 ctx) throws Exception { private Expr evalBinaryOp(TranslatorToZ3 ctx, Expr e1, Expr e2) { switch (op) { - case "&&": - return ctx.makeAnd(e1, e2); - case "||": - return ctx.makeOr(e1, e2); - case "-->": - return ctx.makeImplies(e1, e2); - case "==": - return ctx.makeEquals(e1, e2); - case "!=": - return ctx.mkNot(ctx.makeEquals(e1, e2)); - case ">=": - return ctx.makeGtEq(e1, e2); - case ">": - return ctx.makeGt(e1, e2); - case "<=": - return ctx.makeLtEq(e1, e2); - case "<": - return ctx.makeLt(e1, e2); - case "+": - return ctx.makeAdd(e1, e2); - case "-": - return ctx.makeSub(e1, e2); - case "*": - return ctx.makeMul(e1, e2); - case "/": - return ctx.makeDiv(e1, e2); - case "%": - return ctx.makeMod(e1, e2); - default: // last case % - throw new RuntimeException("Operation " + op + "not supported by z3"); + case "&&": + return ctx.makeAnd(e1, e2); + case "||": + return ctx.makeOr(e1, e2); + case "-->": + return ctx.makeImplies(e1, e2); + case "==": + return ctx.makeEquals(e1, e2); + case "!=": + return ctx.mkNot(ctx.makeEquals(e1, e2)); + case ">=": + return ctx.makeGtEq(e1, e2); + case ">": + return ctx.makeGt(e1, e2); + case "<=": + return ctx.makeLtEq(e1, e2); + case "<": + return ctx.makeLt(e1, e2); + case "+": + return ctx.makeAdd(e1, e2); + case "-": + return ctx.makeSub(e1, e2); + case "*": + return ctx.makeMul(e1, e2); + case "/": + return ctx.makeDiv(e1, e2); + case "%": + return ctx.makeMod(e1, e2); + default: // last case % + throw new RuntimeException("Operation " + op + "not supported by z3"); } } @Override public String toString() { - return getFirstOperand().toString() + " " + op + " " - + getSecondOperand().toString(); + return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString(); } @Override @@ -105,23 +100,22 @@ public void getStateInvocations(List toAdd, List all) { @Override public Expression clone() { - return new BinaryExpression( - getFirstOperand().clone(), op, getSecondOperand().clone()); + return new BinaryExpression(getFirstOperand().clone(), op, getSecondOperand().clone()); } @Override public boolean isBooleanTrue() { switch (op) { - case "&&": - return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); - case "||": - return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); - case "-->": - return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); - case "==": - return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); - default: - return false; + case "&&": + return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); + case "||": + return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); + case "-->": + return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); + case "==": + return getFirstOperand().isBooleanTrue() && getSecondOperand().isBooleanTrue(); + default: + return false; } } @@ -129,29 +123,36 @@ public boolean isBooleanTrue() { public int hashCode() { final int prime = 31; int result = 1; - result = prime * result - + ((getFirstOperand() == null) ? 0 : getFirstOperand().hashCode()); - result = prime * result - + ((getSecondOperand() == null) ? 0 : getSecondOperand().hashCode()); + result = prime * result + ((getFirstOperand() == null) ? 0 : getFirstOperand().hashCode()); + result = prime * result + ((getSecondOperand() == null) ? 0 : getSecondOperand().hashCode()); result = prime * result + ((op == null) ? 0 : op.hashCode()); return result; } @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; BinaryExpression other = (BinaryExpression) obj; if (getFirstOperand() == null) { - if (other.getFirstOperand() != null) return false; - } else if (!getFirstOperand().equals(other.getFirstOperand())) return false; + if (other.getFirstOperand() != null) + return false; + } else if (!getFirstOperand().equals(other.getFirstOperand())) + return false; if (getSecondOperand() == null) { - if (other.getSecondOperand() != null) return false; - } else if (!getSecondOperand().equals(other.getSecondOperand())) return false; + if (other.getSecondOperand() != null) + return false; + } 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; + if (other.op != null) + return false; + } else if (!op.equals(other.op)) + return false; return true; } } 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 7a35f38d..49426ca2 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 @@ -56,7 +56,8 @@ public void setChild(int index, Expression element) { */ public Expression substitute(Expression from, Expression to) { Expression e = clone(); - if (this.equals(from)) e = to; + if (this.equals(from)) + e = to; e.auxSubstitute(from, to); return e; } @@ -65,7 +66,8 @@ private void auxSubstitute(Expression from, Expression to) { if (hasChildren()) { for (int i = 0; i < children.size(); i++) { Expression exp = children.get(i); - if (exp.equals(from)) setChild(i, to); + if (exp.equals(from)) + setChild(i, to); exp.auxSubstitute(from, to); } } @@ -117,9 +119,7 @@ private void auxSubstituteState(Map subMap, String[] toChang Expression exp = children.get(i); if (exp instanceof FunctionInvocation) { FunctionInvocation fi = (FunctionInvocation) exp; - if (subMap.containsKey(fi.name) - && fi.children.size() == 1 - && fi.children.get(0) instanceof Var) { // object + if (subMap.containsKey(fi.name) && fi.children.size() == 1 && fi.children.get(0) instanceof Var) { // object // state Var v = (Var) fi.children.get(0); Expression sub = subMap.get(fi.name).clone(); @@ -167,7 +167,8 @@ private void auxChangeAlias(Map alias, Context ctx, Factory f) for (int i = 0; i < children.size(); i++) { if (children.get(i) instanceof AliasInvocation) { AliasInvocation ai = (AliasInvocation) children.get(i); - if (!alias.containsKey(ai.name)) throw new Exception("Alias '" + ai.getName() + "' not found"); + if (!alias.containsKey(ai.name)) + throw new Exception("Alias '" + ai.getName() + "' not found"); AliasDTO dto = alias.get(ai.name); Expression sub = dto.getExpression().clone(); if (ai.hasChildren()) @@ -180,10 +181,7 @@ private void auxChangeAlias(Map alias, Context ctx, Factory f) if (!checks) throw new Exception( "Type Mismatch: Cannot substitute " + varExp + ":" + varType + " by " + aliasExp - + ":" - + TypeInfer.getType(ctx, f, aliasExp) - .get() - .getQualifiedName() + + ":" + TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName() + " in alias '" + ai.name + "'"); sub = sub.substitute(varExp, aliasExp); 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 2a520bd2..9e93690e 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 @@ -11,7 +11,8 @@ public class FunctionInvocation extends Expression { public FunctionInvocation(String name, List args) { this.name = name; - for (Expression e : args) addChild(e); + for (Expression e : args) + addChild(e); } public String getName() { @@ -43,19 +44,23 @@ public String toString() { @Override public void getVariableNames(List toAdd) { - for (Expression e : getArgs()) e.getVariableNames(toAdd); + for (Expression e : getArgs()) + e.getVariableNames(toAdd); } @Override public void getStateInvocations(List toAdd, List all) { - if (!toAdd.contains(name) && all.contains(name)) toAdd.add(name); - for (Expression e : getArgs()) e.getStateInvocations(toAdd, all); + if (!toAdd.contains(name) && all.contains(name)) + toAdd.add(name); + for (Expression e : getArgs()) + e.getStateInvocations(toAdd, all); } @Override public Expression clone() { List le = new ArrayList<>(); - for (Expression e : getArgs()) le.add(e.clone()); + for (Expression e : getArgs()) + le.add(e.clone()); return new FunctionInvocation(name, le); } @@ -65,9 +70,11 @@ public boolean isBooleanTrue() { } public boolean argumentsEqual(List parameters) { - if (parameters.size() != getArgs().size()) return false; + if (parameters.size() != getArgs().size()) + return false; for (int i = 0; i < getArgs().size(); i++) { - if (!parameters.get(i).equals(getArgs().get(i))) return false; + if (!parameters.get(i).equals(getArgs().get(i))) + return false; } return true; } @@ -83,16 +90,23 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; FunctionInvocation other = (FunctionInvocation) obj; if (getArgs() == null) { - if (other.getArgs() != null) return false; - } else if (!getArgs().equals(other.getArgs())) return false; + if (other.getArgs() != null) + return false; + } 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; + if (other.name != null) + return false; + } else if (!name.equals(other.name)) + return false; return true; } } 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 b09e794f..f7d7dcf3 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 @@ -47,20 +47,24 @@ public boolean isBooleanTrue() { public int hashCode() { final int prime = 31; int result = 1; - result = prime * result - + ((getExpression() == null) ? 0 : getExpression().hashCode()); + result = prime * result + ((getExpression() == null) ? 0 : getExpression().hashCode()); return result; } @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; GroupExpression other = (GroupExpression) obj; if (getExpression() == null) { - if (other.getExpression() != null) return false; - } else if (!getExpression().equals(other.getExpression())) return false; + if (other.getExpression() != null) + return false; + } else if (!getExpression().equals(other.getExpression())) + return false; return true; } } 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 0198e95f..4accd126 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 @@ -26,14 +26,12 @@ public Expression getElse() { @Override public Expr eval(TranslatorToZ3 ctx) throws Exception { - return ctx.makeIte( - getCondition().eval(ctx), getThen().eval(ctx), getElse().eval(ctx)); + return ctx.makeIte(getCondition().eval(ctx), getThen().eval(ctx), getElse().eval(ctx)); } @Override public String toString() { - return getCondition().toString() + "?" + getThen().toString() + ":" - + getElse().toString(); + return getCondition().toString() + "?" + getThen().toString() + ":" + getElse().toString(); } @Override @@ -57,9 +55,7 @@ public Expression clone() { @Override public boolean isBooleanTrue() { - return getCondition().isBooleanTrue() - && getThen().isBooleanTrue() - && getElse().isBooleanTrue(); + return getCondition().isBooleanTrue() && getThen().isBooleanTrue() && getElse().isBooleanTrue(); } @Override @@ -74,19 +70,28 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; Ite other = (Ite) obj; if (getCondition() == null) { - if (other.getCondition() != null) return false; - } else if (!getCondition().equals(other.getCondition())) return false; + if (other.getCondition() != null) + return false; + } else if (!getCondition().equals(other.getCondition())) + return false; if (getElse() == null) { - if (other.getElse() != null) return false; - } else if (!getElse().equals(other.getElse())) return false; + if (other.getElse() != null) + return false; + } 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; + if (other.getThen() != null) + return false; + } else if (!getThen().equals(other.getThen())) + return false; return true; } } 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 47c89a27..3d223697 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 @@ -55,11 +55,15 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; LiteralBoolean other = (LiteralBoolean) obj; - if (value != other.value) return false; + if (value != other.value) + return false; return true; } } 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 7ff89237..6a4e97f1 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 @@ -57,11 +57,15 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; LiteralInt other = (LiteralInt) obj; - if (value != other.value) return false; + if (value != other.value) + return false; return true; } } 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 90cb69cc..2ddc8430 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 @@ -59,11 +59,15 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; LiteralReal other = (LiteralReal) obj; - if (Double.doubleToLongBits(value) != Double.doubleToLongBits(other.value)) return false; + if (Double.doubleToLongBits(value) != Double.doubleToLongBits(other.value)) + return false; return true; } } 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 3223c1ca..eed7ec71 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 @@ -52,13 +52,18 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; LiteralString other = (LiteralString) obj; if (value == null) { - if (other.value != null) return false; - } else if (!value.equals(other.value)) return false; + if (other.value != null) + return false; + } else if (!value.equals(other.value)) + return false; return true; } } 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 6338f9d5..df5eb888 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 @@ -24,10 +24,10 @@ public String getOp() { @Override public Expr eval(TranslatorToZ3 ctx) throws Exception { switch (op) { - case "-": - return ctx.makeMinus(getExpression().eval(ctx)); - case "!": - return ctx.mkNot(getExpression().eval(ctx)); + case "-": + return ctx.makeMinus(getExpression().eval(ctx)); + case "!": + return ctx.mkNot(getExpression().eval(ctx)); } return null; } @@ -61,24 +61,30 @@ public boolean isBooleanTrue() { public int hashCode() { final int prime = 31; int result = 1; - result = prime * result - + ((getExpression() == null) ? 0 : getExpression().hashCode()); + result = prime * result + ((getExpression() == null) ? 0 : getExpression().hashCode()); result = prime * result + ((op == null) ? 0 : op.hashCode()); return result; } @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; UnaryExpression other = (UnaryExpression) obj; if (getExpression() == null) { - if (other.getExpression() != null) return false; - } else if (!getExpression().equals(other.getExpression())) return false; + if (other.getExpression() != null) + return false; + } 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; + if (other.op != null) + return false; + } else if (!op.equals(other.op)) + return false; return true; } } 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 3973fd22..2e5c3b1d 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 @@ -27,7 +27,8 @@ public String toString() { @Override public void getVariableNames(List toAdd) { - if (!toAdd.contains(name)) toAdd.add(name); + if (!toAdd.contains(name)) + toAdd.add(name); } @Override @@ -55,13 +56,18 @@ public int hashCode() { @Override public boolean equals(Object obj) { - if (this == obj) return true; - if (obj == null) return false; - if (getClass() != obj.getClass()) return false; + if (this == obj) + return true; + if (obj == null) + return false; + if (getClass() != obj.getClass()) + return false; Var other = (Var) obj; if (name == null) { - if (other.name != null) return false; - } else if (!name.equals(other.name)) return false; + if (other.name != null) + return false; + } else if (!name.equals(other.name)) + return false; return true; } } 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 f5635d0b..9f902fac 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 @@ -35,42 +35,58 @@ public static boolean checkCompatibleType(String type, Expression e, Context ctx } public static Optional> getType(Context ctx, Factory factory, Expression e) { - if (e instanceof LiteralString) return Optional.of(Utils.getType("String", factory)); - else if (e instanceof LiteralInt) return Optional.of(Utils.getType("int", factory)); - else if (e instanceof LiteralReal) return Optional.of(Utils.getType("double", factory)); - else if (e instanceof LiteralBoolean) return boolType(factory); - else if (e instanceof Var) return varType(ctx, factory, (Var) e); - else if (e instanceof UnaryExpression) return unaryType(ctx, factory, (UnaryExpression) e); - else if (e instanceof Ite) return boolType(factory); - else if (e instanceof BinaryExpression) return binaryType(ctx, factory, (BinaryExpression) e); - else if (e instanceof GroupExpression) return getType(ctx, factory, ((GroupExpression) e).getExpression()); - else if (e instanceof FunctionInvocation) return functionType(ctx, factory, (FunctionInvocation) e); - else if (e instanceof AliasInvocation) return boolType(factory); + if (e instanceof LiteralString) + return Optional.of(Utils.getType("String", factory)); + else if (e instanceof LiteralInt) + return Optional.of(Utils.getType("int", factory)); + else if (e instanceof LiteralReal) + return Optional.of(Utils.getType("double", factory)); + else if (e instanceof LiteralBoolean) + return boolType(factory); + else if (e instanceof Var) + return varType(ctx, factory, (Var) e); + else if (e instanceof UnaryExpression) + return unaryType(ctx, factory, (UnaryExpression) e); + else if (e instanceof Ite) + return boolType(factory); + else if (e instanceof BinaryExpression) + return binaryType(ctx, factory, (BinaryExpression) e); + else if (e instanceof GroupExpression) + return getType(ctx, factory, ((GroupExpression) e).getExpression()); + else if (e instanceof FunctionInvocation) + return functionType(ctx, factory, (FunctionInvocation) e); + else if (e instanceof AliasInvocation) + return boolType(factory); return Optional.empty(); } private static Optional> varType(Context ctx, Factory factory, Var v) { String name = v.getName(); - if (!ctx.hasVariable(name)) return Optional.empty(); + if (!ctx.hasVariable(name)) + return Optional.empty(); return Optional.of(ctx.getVariableByName(name).getType()); } private static Optional> unaryType(Context ctx, Factory factory, UnaryExpression e) { - if (e.getOp().equals("!")) return boolType(factory); + if (e.getOp().equals("!")) + return boolType(factory); return getType(ctx, factory, e.getExpression()); } private static Optional> binaryType(Context ctx, Factory factory, BinaryExpression e) { - if (e.isLogicOperation()) return boolType(factory); // &&, ||, --> + if (e.isLogicOperation()) + return boolType(factory); // &&, ||, --> else if (e.isBooleanOperation()) { // >, >=, <, <=, ==, != return boolType(factory); } else if (e.isArithmeticOperation()) { Optional> t1 = getType(ctx, factory, e.getFirstOperand()); Optional> t2 = getType(ctx, factory, e.getSecondOperand()); - if (!t1.isPresent() || !t2.isPresent()) return Optional.empty(); - if (t1.get().equals(t2.get())) return t1; + if (!t1.isPresent() || !t2.isPresent()) + return Optional.empty(); + if (t1.get().equals(t2.get())) + return t1; // TODO if the types are different ex: double, int throw new NotImplementedException( "To implement in TypeInfer: Binary type, arithmetic with different arg types"); @@ -79,9 +95,7 @@ else if (e.isBooleanOperation()) { // >, >=, <, <=, ==, != } private static Optional> functionType(Context ctx, Factory factory, FunctionInvocation e) { - Optional gh = ctx.getGhosts().stream() - .filter(g -> g.getName().equals(e.getName())) - .findAny(); + Optional gh = ctx.getGhosts().stream().filter(g -> g.getName().equals(e.getName())).findAny(); return gh.map(i -> i.getReturnType()); } 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 f48c3997..28c0dc82 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 @@ -23,19 +23,15 @@ public RJErrorListener() { } @Override - public void syntaxError( - Recognizer recognizer, - Object offendingSymbol, - int line, - int charPositionInLine, - String msg, - RecognitionException e) { + public void syntaxError(Recognizer recognizer, Object offendingSymbol, int line, int charPositionInLine, + String msg, RecognitionException e) { // Hint for == instead of = String hint = null; if (e instanceof LexerNoViableAltException) { LexerNoViableAltException l = (LexerNoViableAltException) e; char c = l.getInputStream().toString().charAt(charPositionInLine); - if (c == '=') hint = "Predicates must be compared with == instead of ="; + if (c == '=') + hint = "Predicates must be compared with == instead of ="; } errors++; String ms = "Error in " + msg + ", in the position " + charPositionInLine; @@ -43,22 +39,19 @@ public void syntaxError( } @Override - public void reportAmbiguity( - Parser recognizer, - DFA dfa, - int startIndex, - int stopIndex, - boolean exact, - BitSet ambigAlts, - ATNConfigSet configs) {} + public void reportAmbiguity(Parser recognizer, DFA dfa, int startIndex, int stopIndex, boolean exact, + BitSet ambigAlts, ATNConfigSet configs) { + } @Override - public void reportAttemptingFullContext( - Parser recognizer, DFA dfa, int startIndex, int stopIndex, BitSet conflictingAlts, ATNConfigSet configs) {} + public void reportAttemptingFullContext(Parser recognizer, DFA dfa, int startIndex, int stopIndex, + BitSet conflictingAlts, ATNConfigSet configs) { + } @Override - public void reportContextSensitivity( - Parser recognizer, DFA dfa, int startIndex, int stopIndex, int prediction, ATNConfigSet configs) {} + public void reportContextSensitivity(Parser recognizer, DFA dfa, int startIndex, int stopIndex, int prediction, + ATNConfigSet configs) { + } public int getErrors() { return errors; @@ -68,7 +61,8 @@ 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"); - for (String s : msgs) sb.append("* " + s + "\n"); + for (String s : msgs) + sb.append("* " + s + "\n"); return sb.toString(); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java index 28391f95..55daed4a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java @@ -34,13 +34,15 @@ public static Expression createAST(String toParse) throws ParsingException { public static GhostDTO getGhostDeclaration(String s) throws ParsingException { ParseTree rc = compile(s); GhostDTO g = GhostVisitor.getGhostDecl(rc); - if (g == null) throw new ParsingException(" The ghost should be in format ()"); + if (g == null) + throw new ParsingException(" The ghost should be in format ()"); return g; } public static AliasDTO getAliasDeclaration(String s) throws ParsingException { Optional os = getErrors(s); - if (os.isPresent()) throw new ParsingException(os.get()); + if (os.isPresent()) + throw new ParsingException(os.get()); CodePointCharStream input; input = CharStreams.fromString(s); RJErrorListener err = new RJErrorListener(); @@ -61,7 +63,8 @@ public static AliasDTO getAliasDeclaration(String s) throws ParsingException { private static ParseTree compile(String toParse) throws ParsingException { Optional s = getErrors(toParse); - if (s.isPresent()) throw new ParsingException(s.get()); + if (s.isPresent()) + throw new ParsingException(s.get()); CodePointCharStream input = CharStreams.fromString(toParse); RJErrorListener err = new RJErrorListener(); @@ -101,7 +104,8 @@ private static Optional getErrors(String toParse) { parser.removeErrorListeners(); parser.addErrorListener(err); parser.start(); // all consumed - if (err.getErrors() > 0) return Optional.of(err.getMessages()); + if (err.getErrors() > 0) + return Optional.of(err.getMessages()); return Optional.empty(); } } 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 218c4508..f0937af2 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 @@ -75,6 +75,7 @@ private void auxGetArgsDecl(ArgDeclIDContext argDeclID, List(type, name)); - if (argDeclID.argDeclID() != null) auxGetArgsDecl(argDeclID.argDeclID(), l); + if (argDeclID.argDeclID() != null) + auxGetArgsDecl(argDeclID.argDeclID(), 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 45d03b32..d647875a 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 @@ -56,52 +56,59 @@ public class CreateASTVisitor { public static Expression create(ParseTree rc) { - if (rc instanceof ProgContext) return progCreate((ProgContext) rc); - else if (rc instanceof StartContext) return startCreate(rc); - else if (rc instanceof PredContext) return predCreate(rc); - else if (rc instanceof ExpContext) return expCreate(rc); - else if (rc instanceof OperandContext) return operandCreate(rc); - else if (rc instanceof LiteralExpressionContext) return literalExpressionCreate(rc); - else if (rc instanceof FunctionCallContext) return functionCallCreate((FunctionCallContext) rc); - else if (rc instanceof LiteralContext) return literalCreate((LiteralContext) rc); + if (rc instanceof ProgContext) + return progCreate((ProgContext) rc); + else if (rc instanceof StartContext) + return startCreate(rc); + else if (rc instanceof PredContext) + return predCreate(rc); + else if (rc instanceof ExpContext) + return expCreate(rc); + else if (rc instanceof OperandContext) + return operandCreate(rc); + else if (rc instanceof LiteralExpressionContext) + return literalExpressionCreate(rc); + else if (rc instanceof FunctionCallContext) + return functionCallCreate((FunctionCallContext) rc); + else if (rc instanceof LiteralContext) + return literalCreate((LiteralContext) rc); return null; } private static Expression progCreate(ProgContext rc) { - if (rc.start() != null) return create(rc.start()); + if (rc.start() != null) + return create(rc.start()); return null; } private static Expression startCreate(ParseTree rc) { - if (rc instanceof StartPredContext) return create(((StartPredContext) rc).pred()); + if (rc instanceof StartPredContext) + return create(((StartPredContext) rc).pred()); // alias and ghost do not have evaluation return null; } private static Expression predCreate(ParseTree rc) { - if (rc instanceof PredGroupContext) return new GroupExpression(create(((PredGroupContext) rc).pred())); + if (rc instanceof PredGroupContext) + return new GroupExpression(create(((PredGroupContext) rc).pred())); else if (rc instanceof PredNegateContext) return new UnaryExpression("!", create(((PredNegateContext) rc).pred())); else if (rc instanceof PredLogicContext) - return new BinaryExpression( - create(((PredLogicContext) rc).pred(0)), - ((PredLogicContext) rc).LOGOP().getText(), - create(((PredLogicContext) rc).pred(1))); + return new BinaryExpression(create(((PredLogicContext) rc).pred(0)), + ((PredLogicContext) rc).LOGOP().getText(), create(((PredLogicContext) rc).pred(1))); else if (rc instanceof IteContext) - return new Ite( - create(((IteContext) rc).pred(0)), - create(((IteContext) rc).pred(1)), + return new Ite(create(((IteContext) rc).pred(0)), create(((IteContext) rc).pred(1)), create(((IteContext) rc).pred(2))); - else return create(((PredExpContext) rc).exp()); + else + return create(((PredExpContext) rc).exp()); } private static Expression expCreate(ParseTree rc) { - if (rc instanceof ExpGroupContext) return new GroupExpression(create(((ExpGroupContext) rc).exp())); + if (rc instanceof ExpGroupContext) + return new GroupExpression(create(((ExpGroupContext) rc).exp())); else if (rc instanceof ExpBoolContext) { - return new BinaryExpression( - create(((ExpBoolContext) rc).exp(0)), - ((ExpBoolContext) rc).BOOLOP().getText(), + return new BinaryExpression(create(((ExpBoolContext) rc).exp(0)), ((ExpBoolContext) rc).BOOLOP().getText(), create(((ExpBoolContext) rc).exp(1))); } else { ExpOperandContext eoc = (ExpOperandContext) rc; @@ -110,18 +117,20 @@ else if (rc instanceof ExpBoolContext) { } private static Expression operandCreate(ParseTree rc) { - if (rc instanceof OpLiteralContext) return create(((OpLiteralContext) rc).literalExpression()); + if (rc instanceof OpLiteralContext) + return create(((OpLiteralContext) rc).literalExpression()); else if (rc instanceof OpArithContext) - return new BinaryExpression( - create(((OpArithContext) rc).operand(0)), - ((OpArithContext) rc).ARITHOP().getText(), - create(((OpArithContext) rc).operand(1))); + return new BinaryExpression(create(((OpArithContext) rc).operand(0)), + ((OpArithContext) rc).ARITHOP().getText(), create(((OpArithContext) rc).operand(1))); else if (rc instanceof OpSubContext) - return new BinaryExpression( - create(((OpSubContext) rc).operand(0)), "-", create(((OpSubContext) rc).operand(1))); - else if (rc instanceof OpMinusContext) return new UnaryExpression("-", create(((OpMinusContext) rc).operand())); - else if (rc instanceof OpNotContext) return new UnaryExpression("!", create(((OpNotContext) rc).operand())); - else if (rc instanceof OpGroupContext) return new GroupExpression(create(((OpGroupContext) rc).operand())); + return new BinaryExpression(create(((OpSubContext) rc).operand(0)), "-", + create(((OpSubContext) rc).operand(1))); + else if (rc instanceof OpMinusContext) + return new UnaryExpression("-", create(((OpMinusContext) rc).operand())); + else if (rc instanceof OpNotContext) + return new UnaryExpression("!", create(((OpNotContext) rc).operand())); + else if (rc instanceof OpGroupContext) + return new GroupExpression(create(((OpGroupContext) rc).operand())); assert false; return null; } @@ -129,7 +138,8 @@ else if (rc instanceof OpSubContext) private static Expression literalExpressionCreate(ParseTree rc) { if (rc instanceof LitGroupContext) return new GroupExpression(create(((LitGroupContext) rc).literalExpression())); - else if (rc instanceof LitContext) return create(((LitContext) rc).literal()); + else if (rc instanceof LitContext) + return create(((LitContext) rc).literal()); else if (rc instanceof VarContext) { return new Var(((VarContext) rc).ID().getText()); } else if (rc instanceof TargetInvocationContext) { 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 5dcb259b..ac4c5495 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 @@ -18,19 +18,22 @@ public static GhostDTO getGhostDecl(ParseTree rc) { 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<>(); + if (ls == null) + ls = new ArrayList<>(); return new GhostDTO(name, ls, type); // return new Triple>>(type, name, args); } else if (rc.getChildCount() > 0) { int i = rc.getChildCount(); - if (i > 0) return getGhostDecl(rc.getChild(0)); + if (i > 0) + return getGhostDecl(rc.getChild(0)); } return null; } private static List> getArgsDecl(ArgDeclContext argDecl) { List> l = new ArrayList>(); - if (argDecl != null) auxGetArgsDecl(argDecl, l); + if (argDecl != null) + auxGetArgsDecl(argDecl, l); return l; } @@ -38,6 +41,7 @@ private static void auxGetArgsDecl(ArgDeclContext argDecl, List(type, name)); - if (argDecl.argDecl() != null) auxGetArgsDecl(argDecl.argDecl(), l); + if (argDecl.argDecl() != null) + auxGetArgsDecl(argDecl.argDecl(), l); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java index 9a4f92fd..621a2420 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java @@ -40,7 +40,8 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c) if (e.getLocalizedMessage().substring(0, 24).equals("Wrong number of argument") || e.getLocalizedMessage().substring(0, 13).equals("Sort mismatch")) throw new GhostFunctionError(e.getLocalizedMessage()); - else throw new Z3Exception(e.getLocalizedMessage()); + else + throw new Z3Exception(e.getLocalizedMessage()); } } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java index 7480bdbb..2cf2ca7a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java @@ -17,21 +17,23 @@ public class TranslatorContextToZ3 { - static void translateVariables( - Context z3, Map> ctx, Map> varTranslation) { + static void translateVariables(Context z3, Map> ctx, + Map> varTranslation) { - for (String name : ctx.keySet()) varTranslation.put(name, getExpr(z3, name, ctx.get(name))); + for (String name : ctx.keySet()) + varTranslation.put(name, getExpr(z3, name, ctx.get(name))); varTranslation.put("true", z3.mkBool(true)); varTranslation.put("false", z3.mkBool(false)); } - public static void storeVariablesSubtypes( - Context z3, List variables, Map>> varSuperTypes) { + public static void storeVariablesSubtypes(Context z3, List variables, + Map>> varSuperTypes) { for (RefinedVariable v : variables) { if (!v.getSuperTypes().isEmpty()) { ArrayList> a = new ArrayList<>(); - for (CtTypeReference ctr : v.getSuperTypes()) a.add(getExpr(z3, v.getName(), ctr)); + for (CtTypeReference ctr : v.getSuperTypes()) + a.add(getExpr(z3, v.getName(), ctr)); varSuperTypes.put(v.getName(), a); } } @@ -39,10 +41,14 @@ public static void storeVariablesSubtypes( private static Expr getExpr(Context z3, String name, CtTypeReference type) { String typeName = type.getQualifiedName(); - if (typeName.contentEquals("int")) return z3.mkIntConst(name); - else if (typeName.contentEquals("short")) return z3.mkIntConst(name); - else if (typeName.contentEquals("boolean")) return z3.mkBoolConst(name); - else if (typeName.contentEquals("long")) return z3.mkRealConst(name); + if (typeName.contentEquals("int")) + return z3.mkIntConst(name); + else if (typeName.contentEquals("short")) + return z3.mkIntConst(name); + else if (typeName.contentEquals("boolean")) + return z3.mkBoolConst(name); + else if (typeName.contentEquals("long")) + return z3.mkRealConst(name); else if (typeName.contentEquals("float")) { return (FPExpr) z3.mkConst(name, z3.mkFPSort64()); } else if (typeName.contentEquals("double")) { @@ -62,8 +68,8 @@ static void addAlias(Context z3, List alias, Map ghosts, Map> funcTranslation) { + public static void addGhostFunctions(Context z3, List ghosts, + Map> funcTranslation) { addBuiltinFunctions(z3, funcTranslation); if (!ghosts.isEmpty()) { for (GhostFunction gh : ghosts) { @@ -73,15 +79,12 @@ public static void addGhostFunctions( } private static void addBuiltinFunctions(Context z3, Map> funcTranslation) { - funcTranslation.put( - "length", - z3.mkFuncDecl("length", getSort(z3, "int[]"), getSort(z3, "int"))); // ERRRRRRRRRRRRO!!!!!!!!!!!!! + 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"); // TODO add built-in function - Sort[] s = Stream.of(getSort(z3, "int[]"), getSort(z3, "int"), getSort(z3, "int")) - .toArray(Sort[]::new); + 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"))); s = Stream.of(getSort(z3, "int[]"), getSort(z3, "int")).toArray(Sort[]::new); @@ -90,30 +93,30 @@ private static void addBuiltinFunctions(Context z3, Map> fun static Sort getSort(Context z3, String sort) { switch (sort) { - case "int": - return z3.getIntSort(); - case "boolean": - return z3.getBoolSort(); - case "long": - return z3.getRealSort(); - case "float": - return z3.mkFPSort32(); - case "double": - return z3.mkFPSortDouble(); - case "int[]": - return z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort()); - case "String": - return z3.getStringSort(); - case "void": - return z3.mkUninterpretedSort("void"); - // case "List":return z3.mkListSort(name, elemSort) - default: - return z3.mkUninterpretedSort(sort); + case "int": + return z3.getIntSort(); + case "boolean": + return z3.getBoolSort(); + case "long": + return z3.getRealSort(); + case "float": + return z3.mkFPSort32(); + case "double": + return z3.mkFPSortDouble(); + case "int[]": + return z3.mkArraySort(z3.mkIntSort(), z3.mkIntSort()); + case "String": + return z3.getStringSort(); + case "void": + return z3.mkUninterpretedSort("void"); + // case "List":return z3.mkListSort(name, elemSort) + default: + return z3.mkUninterpretedSort(sort); } } - public static void addGhostStates( - Context z3, List ghostState, Map> funcTranslation) { + public static void addGhostStates(Context z3, List ghostState, + Map> funcTranslation) { for (GhostState g : ghostState) { addGhostFunction(z3, g, funcTranslation); // if(g.getRefinement() != null) @@ -124,10 +127,7 @@ public static void addGhostStates( private static void addGhostFunction(Context z3, GhostFunction gh, Map> funcTranslation) { List> paramTypes = gh.getParametersTypes(); Sort ret = getSort(z3, gh.getReturnType().toString()); - Sort[] d = paramTypes.stream() - .map(t -> t.toString()) - .map(t -> getSort(z3, t)) - .toArray(Sort[]::new); + Sort[] d = paramTypes.stream().map(t -> t.toString()).map(t -> getSort(z3, t)).toArray(Sort[]::new); funcTranslation.put(gh.getName(), z3.mkFuncDecl(gh.getName(), d, ret)); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 69a727d7..1a373e7d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -71,10 +71,13 @@ public Expr makeBooleanLiteral(boolean value) { } private Expr getVariableTranslation(String name) throws Exception { - if (!varTranslation.containsKey(name)) throw new NotFoundError("Variable '" + name.toString() + "' not found"); + if (!varTranslation.containsKey(name)) + throw new NotFoundError("Variable '" + name.toString() + "' not found"); Expr e = varTranslation.get(name); - if (e == null) e = varTranslation.get(String.format("this#%s", name)); - if (e == null) throw new SyntaxException("Unknown variable:" + name); + if (e == null) + e = varTranslation.get(String.format("this#%s", name)); + if (e == null) + throw new SyntaxException("Unknown variable:" + name); return e; } @@ -83,10 +86,13 @@ public Expr makeVariable(String name) throws Exception { } public Expr makeFunctionInvocation(String name, Expr[] params) throws Exception { - if (name.equals("addToIndex")) return makeStore(name, params); - if (name.equals("getFromIndex")) return makeSelect(name, params); + if (name.equals("addToIndex")) + return makeStore(name, params); + if (name.equals("getFromIndex")) + return makeSelect(name, params); - if (!funcTranslation.containsKey(name)) throw new NotFoundError("Function '" + name + "' not found"); + if (!funcTranslation.containsKey(name)) + throw new NotFoundError("Function '" + name + "' not found"); FuncDecl fd = funcTranslation.get(name); Sort[] s = fd.getDomain(); @@ -95,7 +101,10 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws Exce if (!s[i].equals(param.getSort())) { // Look if the function type is a supertype of this List> le = varSuperTypes.get(param.toString().replace("|", "")); - if (le != null) for (Expr e : le) if (e.getSort().equals(s[i])) params[i] = e; + if (le != null) + for (Expr e : le) + if (e.getSort().equals(s[i])) + params[i] = e; } // System.out.println("Expected sort"+s[i]+"; Final sort->" // +params[i].toString() +":"+ @@ -105,13 +114,14 @@ public Expr makeFunctionInvocation(String name, Expr[] params) throws Exce return z3.mkApp(fd, params); } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) private Expr makeSelect(String name, Expr[] params) { - if (params.length == 2 && params[0] instanceof ArrayExpr) return z3.mkSelect((ArrayExpr) params[0], params[1]); + if (params.length == 2 && params[0] instanceof ArrayExpr) + return z3.mkSelect((ArrayExpr) params[0], params[1]); return null; } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) private Expr makeStore(String name, Expr[] params) { if (params.length == 3 && params[0] instanceof ArrayExpr) return z3.mkStore((ArrayExpr) params[0], params[1], params[2]); @@ -120,35 +130,40 @@ private Expr makeStore(String name, Expr[] params) { // #####################Boolean Operations##################### public Expr makeEquals(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPEq(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) + return z3.mkFPEq(toFP(e1), toFP(e2)); return z3.mkEq(e1, e2); } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeLt(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPLt(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) + return z3.mkFPLt(toFP(e1), toFP(e2)); return z3.mkLt((ArithExpr) e1, (ArithExpr) e2); } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeLtEq(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPLEq(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) + return z3.mkFPLEq(toFP(e1), toFP(e2)); return z3.mkLe((ArithExpr) e1, (ArithExpr) e2); } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeGt(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPGt(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) + return z3.mkFPGt(toFP(e1), toFP(e2)); return z3.mkGt((ArithExpr) e1, (ArithExpr) e2); } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeGtEq(Expr e1, Expr e2) { - if (e1 instanceof FPExpr || e2 instanceof FPExpr) return z3.mkFPGEq(toFP(e1), toFP(e2)); + if (e1 instanceof FPExpr || e2 instanceof FPExpr) + return z3.mkFPGEq(toFP(e1), toFP(e2)); return z3.mkGe((ArithExpr) e1, (ArithExpr) e2); } @@ -179,14 +194,15 @@ public Expr makeOr(Expr eval, Expr eval2) { // } // ##################### Unary Operations ##################### - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeMinus(Expr eval) { - if (eval instanceof FPExpr) return z3.mkFPNeg((FPExpr) eval); + if (eval instanceof FPExpr) + return z3.mkFPNeg((FPExpr) eval); return z3.mkUnaryMinus((ArithExpr) eval); } // #####################Arithmetic Operations##################### - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeAdd(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPAdd(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); @@ -194,7 +210,7 @@ public Expr makeAdd(Expr eval, Expr eval2) { return z3.mkAdd((ArithExpr) eval, (ArithExpr) eval2); } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeSub(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPSub(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); @@ -202,7 +218,7 @@ public Expr makeSub(Expr eval, Expr eval2) { return z3.mkSub((ArithExpr) eval, (ArithExpr) eval2); } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeMul(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPMul(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); @@ -210,7 +226,7 @@ public Expr makeMul(Expr eval, Expr eval2) { return z3.mkMul((ArithExpr) eval, (ArithExpr) eval2); } - @SuppressWarnings({"unchecked", "rawtypes"}) + @SuppressWarnings({ "unchecked", "rawtypes" }) public Expr makeDiv(Expr eval, Expr eval2) { if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPDiv(z3.mkFPRoundNearestTiesToEven(), toFP(eval), toFP(eval2)); @@ -219,7 +235,8 @@ public Expr makeDiv(Expr eval, Expr eval2) { } public Expr makeMod(Expr eval, Expr eval2) { - if (eval instanceof FPExpr || eval2 instanceof FPExpr) return z3.mkFPRem(toFP(eval), toFP(eval2)); + if (eval instanceof FPExpr || eval2 instanceof FPExpr) + return z3.mkFPRem(toFP(eval), toFP(eval2)); return z3.mkMod((IntExpr) eval, (IntExpr) eval2); } @@ -227,7 +244,8 @@ private FPExpr toFP(Expr e) { FPExpr f; if (e instanceof FPExpr) { f = (FPExpr) e; - } else if (e instanceof IntNum) f = z3.mkFP(((IntNum) e).getInt(), z3.mkFPSort64()); + } else if (e instanceof IntNum) + f = z3.mkFP(((IntNum) e).getInt(), z3.mkFPSort64()); else if (e instanceof IntExpr) { IntExpr ee = (IntExpr) e; RealExpr re = z3.mkInt2Real(ee); @@ -241,7 +259,8 @@ else if (e instanceof IntExpr) { } public Expr makeIte(Expr c, Expr t, Expr e) { - if (c instanceof BoolExpr) return z3.mkITE((BoolExpr) c, t, e); + if (c instanceof BoolExpr) + return z3.mkITE((BoolExpr) c, t, e); throw new RuntimeException("Condition is not a boolean expression"); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index a920c4f2..80a3ee43 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -37,21 +37,21 @@ public class Utils { public static CtTypeReference getType(String type, Factory factory) { // TODO complete switch (type) { - case INT: - return factory.Type().INTEGER_PRIMITIVE; - case DOUBLE: - return factory.Type().DOUBLE_PRIMITIVE; - case BOOLEAN: - return factory.Type().BOOLEAN_PRIMITIVE; - case INT_LIST: - return factory.createArrayReference(getType("int", factory)); - case STRING: - return factory.Type().STRING; - case LIST: - return factory.Type().LIST; - default: - // return factory.Type().OBJECT; - return factory.createReference(type); + case INT: + return factory.Type().INTEGER_PRIMITIVE; + case DOUBLE: + return factory.Type().DOUBLE_PRIMITIVE; + case BOOLEAN: + return factory.Type().BOOLEAN_PRIMITIVE; + case INT_LIST: + return factory.createArrayReference(getType("int", factory)); + case STRING: + return factory.Type().STRING; + case LIST: + return factory.Type().LIST; + default: + // return factory.Type().OBJECT; + return factory.createReference(type); } } } diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java index b63d20ed..223907e3 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestExamples.java @@ -27,8 +27,7 @@ public void testFile(final Path filePath) { String fileName = filePath.getFileName().toString(); // 1. Run the verifier on the file or package - ErrorEmitter errorEmitter = - CommandLineLauncher.launchTest(filePath.toAbsolutePath().toString()); + ErrorEmitter errorEmitter = CommandLineLauncher.launchTest(filePath.toAbsolutePath().toString()); // 2. Check if the file is correct or contains an error if ((fileName.startsWith("Correct") && errorEmitter.foundError()) @@ -54,18 +53,16 @@ public void testFile(final Path filePath) { * if an I/O error occurs or the path does not exist */ private static Stream fileNameSource() throws IOException { - return Files.find( - Paths.get("../liquidjava-example/src/main/java/testSuite/"), - Integer.MAX_VALUE, + return Files.find(Paths.get("../liquidjava-example/src/main/java/testSuite/"), Integer.MAX_VALUE, (filePath, fileAttr) -> { String name = filePath.getFileName().toString(); // 1. Files that start with "Correct" or "Error" - boolean isFileStartingWithCorrectOrError = - fileAttr.isRegularFile() && (name.startsWith("Correct") || name.startsWith("Error")); + boolean isFileStartingWithCorrectOrError = fileAttr.isRegularFile() + && (name.startsWith("Correct") || name.startsWith("Error")); // 2. Folders (directories) that contain "correct" or "error" - boolean isDirectoryWithCorrectOrError = - fileAttr.isDirectory() && (name.contains("correct") || name.contains("error")); + boolean isDirectoryWithCorrectOrError = fileAttr.isDirectory() + && (name.contains("correct") || name.contains("error")); // Return true if either condition matches return isFileStartingWithCorrectOrError || isDirectoryWithCorrectOrError;