diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 07abf74f..caaa0692 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -11,7 +11,7 @@ io.github.liquid-java liquidjava-verifier - 0.0.14 + 0.0.15 liquidjava-verifier LiquidJava Verifier https://github.com/liquid-java/liquidjava diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java deleted file mode 100644 index 3383f6bf..00000000 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/ErrorPosition.java +++ /dev/null @@ -1,12 +0,0 @@ -package liquidjava.diagnostics; - -import spoon.reflect.cu.SourcePosition; - -public record ErrorPosition(int lineStart, int colStart, int lineEnd, int colEnd) { - - public static ErrorPosition fromSpoonPosition(SourcePosition pos) { - if (pos == null || !pos.isValidPosition()) - return null; - return new ErrorPosition(pos.getLine(), pos.getColumn(), pos.getEndLine(), pos.getEndColumn()); - } -} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java index d1a743dc..273e9a49 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java @@ -13,14 +13,14 @@ public class LJDiagnostic extends RuntimeException { private final String accentColor; private final String customMessage; private String file; - private ErrorPosition position; + private SourcePosition position; private static final String PIPE = " | "; public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) { this.title = title; this.message = message; this.file = (pos != null && pos.getFile() != null) ? pos.getFile().getPath() : null; - this.position = ErrorPosition.fromSpoonPosition(pos); + this.position = pos; this.accentColor = accentColor; this.customMessage = customMessage; } @@ -41,14 +41,14 @@ public String getDetails() { return ""; // to be overridden by subclasses } - public ErrorPosition getPosition() { + public SourcePosition getPosition() { return position; } public void setPosition(SourcePosition pos) { - if (pos == null) + if (pos == null || pos.getFile() == null) return; - this.position = ErrorPosition.fromSpoonPosition(pos); + this.position = pos; this.file = pos.getFile().getPath(); } @@ -82,7 +82,7 @@ public String toString() { // location if (file != null && position != null) { - sb.append("\n").append(file).append(":").append(position.lineStart()).append(Colors.RESET).append("\n"); + sb.append("\n").append(file).append(":").append(position.getLine()).append(Colors.RESET).append("\n"); } return sb.toString(); @@ -100,8 +100,8 @@ public String getSnippet() { // before and after lines for context int contextBefore = 2; int contextAfter = 2; - int startLine = Math.max(1, position.lineStart() - contextBefore); - int endLine = Math.min(lines.size(), position.lineEnd() + contextAfter); + int startLine = Math.max(1, position.getLine() - contextBefore); + int endLine = Math.min(lines.size(), position.getEndLine() + contextAfter); // calculate padding for line numbers int padding = String.valueOf(endLine).length(); @@ -115,9 +115,9 @@ public String getSnippet() { sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n"); // add error markers on the line(s) with the error - if (i >= position.lineStart() && i <= position.lineEnd()) { - int colStart = (i == position.lineStart()) ? position.colStart() : 1; - int colEnd = (i == position.lineEnd()) ? position.colEnd() : rawLine.length(); + if (i >= position.getLine() && i <= position.getEndLine()) { + int colStart = (i == position.getLine()) ? position.getColumn() : 1; + int colEnd = (i == position.getEndLine()) ? position.getEndColumn() : rawLine.length(); if (colStart > 0 && colEnd > 0) { int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars() 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 23176dfd..54c3ebff 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -104,32 +104,31 @@ 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 element) { RefinedVariable vi = new Variable(simpleName, type, c); - vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode)); + vi.setPlacementInCode(element); vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); addVarToContext(vi); return vi; } public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference type, Predicate c, - CtElement placementInCode) { + CtElement element) { RefinedVariable vi = new VariableInstance(simpleName, type, c); - vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode)); + vi.setPlacementInCode(element); if (!ctxInstanceVars.contains(vi)) addInstanceVariable(vi); return vi; } public void addRefinementToVariableInContext(String name, CtTypeReference type, Predicate et, - CtElement placementInCode) { + CtElement element) { if (hasVariable(name)) { RefinedVariable vi = getVariableByName(name); vi.setRefinement(et); - vi.addPlacementInCode(PlacementInCode.createPlacement(placementInCode)); + vi.setPlacementInCode(element); } else { - addVarToContext(name, type, et, placementInCode); + addVarToContext(name, type, et, element); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java index 0e4db162..f2274476 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -5,22 +5,22 @@ import java.util.Map; import java.util.Set; +import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtElement; -import spoon.reflect.declaration.CtExecutable; public class ContextHistory { private static ContextHistory instance; - private Map>> fileScopeVars; // file -> (scope -> variables in scope) - private Set instanceVars; - private Set globalVars; + private Map> fileScopes; + private Set localVars; private Set ghosts; private Set aliases; + private Set globalVars; private ContextHistory() { - fileScopeVars = new HashMap<>(); - instanceVars = new HashSet<>(); + fileScopes = new HashMap<>(); + localVars = new HashSet<>(); globalVars = new HashSet<>(); ghosts = new HashSet<>(); aliases = new HashSet<>(); @@ -33,48 +33,40 @@ public static ContextHistory getInstance() { } public void clearHistory() { - fileScopeVars.clear(); - instanceVars.clear(); + fileScopes.clear(); + localVars.clear(); globalVars.clear(); ghosts.clear(); aliases.clear(); } public void saveContext(CtElement element, Context context) { - SourcePosition pos = element.getPosition(); - if (pos == null || pos.getFile() == null) + String file = Utils.getFile(element); + if (file == null) return; - // add variables in scope for this position - String file = pos.getFile().getAbsolutePath(); + // add scope String scope = getScopePosition(element); - fileScopeVars.putIfAbsent(file, new HashMap<>()); - fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars())); + fileScopes.putIfAbsent(file, new HashSet<>()); + fileScopes.get(file).add(scope); - // add other elements in context - instanceVars.addAll(context.getCtxInstanceVars()); + // add variables, ghosts and aliases + localVars.addAll(context.getCtxVars()); + localVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); } - public String getScopePosition(CtElement element) { - SourcePosition pos = element.getPosition(); - SourcePosition innerPosition = pos; - if (element instanceof CtExecutable executable) { - if (executable.getBody() != null) - innerPosition = executable.getBody().getPosition(); - } - return String.format("%d:%d-%d:%d", innerPosition.getLine(), innerPosition.getColumn() + 1, pos.getEndLine(), - pos.getEndColumn()); - } - - public Map>> getFileScopeVars() { - return fileScopeVars; + private String getScopePosition(CtElement element) { + SourcePosition startPos = Utils.getRealPosition(element); + SourcePosition endPos = element.getPosition(); + return String.format("%d:%d-%d:%d", startPos.getLine(), startPos.getColumn(), endPos.getEndLine(), + endPos.getEndColumn() - 1); } - public Set getInstanceVars() { - return instanceVars; + public Set getLocalVars() { + return localVars; } public Set getGlobalVars() { @@ -88,4 +80,8 @@ public Set getGhosts() { public Set getAliases() { return aliases; } + + public Map> getFileScopes() { + return fileScopes; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java index 121f0339..bbc51f73 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java @@ -8,9 +8,12 @@ public class GhostState extends GhostFunction { private GhostFunction parent; private Predicate refinement; + private final String file; - public GhostState(String name, List> list, CtTypeReference returnType, String prefix) { + public GhostState(String name, List> list, CtTypeReference returnType, String prefix, + String file) { super(name, list, returnType, prefix); + this.file = file; } public void setGhostParent(GhostFunction parent) { @@ -28,4 +31,8 @@ public GhostFunction getParent() { public Predicate getRefinement() { return refinement; } + + public String getFile() { + return file; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java index 3400f5f7..d3014faa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java @@ -1,6 +1,8 @@ package liquidjava.processor.context; import java.lang.annotation.Annotation; + +import liquidjava.utils.Utils; import spoon.reflect.code.CtComment; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtAnnotation; @@ -9,10 +11,12 @@ public class PlacementInCode { private final String text; private final SourcePosition position; + private final SourcePosition annotationPosition; - private PlacementInCode(String text, SourcePosition pos) { + private PlacementInCode(String text, SourcePosition pos, SourcePosition annotationPosition) { this.text = text; this.position = pos; + this.annotationPosition = annotationPosition; } public String getText() { @@ -23,6 +27,10 @@ public SourcePosition getPosition() { return position; } + public SourcePosition getAnnotationPosition() { + return annotationPosition; + } + public static PlacementInCode createPlacement(CtElement elem) { CtElement elemCopy = elem.clone(); // cleanup annotations @@ -38,7 +46,8 @@ public static PlacementInCode createPlacement(CtElement elem) { } } String elemText = elemCopy.toString(); - return new PlacementInCode(elemText, elem.getPosition()); + SourcePosition annotationPosition = Utils.getFirstLJAnnotationPosition(elem); + return new PlacementInCode(elemText, elem.getPosition(), annotationPosition); } public String toString() { 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 534f8cfa..0a43939b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -4,6 +4,7 @@ import java.util.List; import java.util.Set; import liquidjava.rj_language.Predicate; +import spoon.reflect.declaration.CtElement; import spoon.reflect.reference.CtTypeReference; public abstract class RefinedVariable extends Refined { @@ -34,8 +35,12 @@ public void addSuperTypes(CtTypeReference ts, Set> sts) { supertypes.add(ct); } - public void addPlacementInCode(PlacementInCode s) { - placementInCode = s; + public void setPlacementInCode(CtElement element) { + placementInCode = PlacementInCode.createPlacement(element); + } + + public void setPlacementInScope(PlacementInCode placement) { + placementInCode = placement; } public PlacementInCode getPlacementInCode() { 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 13f74cab..8ea8f67e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java @@ -148,7 +148,7 @@ else if (has(ifbeforeIndex)) // value before and in else ref = createITEConstraint(nName, cond.negate(), get(ifelseIndex)); } VariableInstance jointReturn = new VariableInstance(nName, super.getType(), ref, this); - jointReturn.addPlacementInCode(getPlacementInCode()); + jointReturn.setPlacementInScope(getPlacementInCode()); return Optional.of(jointReturn); } 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 052c6754..20c6079f 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 @@ -12,7 +12,6 @@ import liquidjava.processor.facade.GhostDTO; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; import liquidjava.rj_language.Predicate; -import liquidjava.rj_language.parsing.RefinementsParser; import liquidjava.utils.Utils; import spoon.reflect.code.CtLiteral; import spoon.reflect.cu.SourcePosition; @@ -28,8 +27,8 @@ import spoon.reflect.reference.CtTypeReference; public class ExternalRefinementTypeChecker extends TypeChecker { - String prefix; - Diagnostics diagnostics = Diagnostics.getInstance(); + private String prefix; + private final Diagnostics diagnostics = Diagnostics.getInstance(); public ExternalRefinementTypeChecker(Context context, Factory factory) { super(context, factory); 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 d26cd25b..a91a4cb2 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 @@ -81,7 +81,7 @@ public Optional getRefinementFromAnnotation(CtElement element) throws if (ref.isPresent()) { Predicate p = new Predicate(ref.get(), element); if (!p.getExpression().isBooleanExpression()) { - SourcePosition position = Utils.getAnnotationPosition(element, ref.get()); + SourcePosition position = Utils.getLJAnnotationPosition(element, ref.get()); throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression", ref.get()); } @@ -152,7 +152,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th CtLiteral s = (CtLiteral) ce; String f = s.getValue(); GhostState gs = new GhostState(f, g.getParametersTypes(), factory.Type().BOOLEAN_PRIMITIVE, - g.getPrefix()); + g.getPrefix(), Utils.getFile(element)); gs.setGhostParent(g); gs.setRefinement(Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); // open(THIS) -> state1(THIS) == 1 @@ -189,7 +189,7 @@ private void createStateGhost(String string, CtElement element, SourcePosition p List> param = Collections.singletonList(factory.Type().createReference(qn)); CtTypeReference r = factory.Type().createReference(gd.returnType()); - GhostState gs = new GhostState(gd.name(), param, r, qn); + GhostState gs = new GhostState(gd.name(), param, r, qn, Utils.getFile(element)); context.addToGhostClass(sn, gs); } 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 61e2592c..446e36aa 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 @@ -209,7 +209,7 @@ private static Predicate createStatePredicate(String value, String targetClass, boolean isTo, String prefix) throws LJError { Predicate p = new Predicate(value, e, prefix); if (!p.getExpression().isBooleanExpression()) { - SourcePosition position = Utils.getAnnotationPosition(e, value); + SourcePosition position = Utils.getLJAnnotationPosition(e, value); throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression", value); } @@ -417,7 +417,7 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L .changeOldMentions(vi.getName(), instanceName); if (!tc.checkStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition - tc.throwStateRefinementError(fw.getPosition(), prevState, stateChange.getFrom(), stateChange.getMessage()); + tc.throwStateRefinementError(fw.getPosition(), prevState, expectState, stateChange.getMessage()); return; } @@ -465,6 +465,7 @@ private static void changeState(TypeChecker tc, VariableInstance vi, List msg != null && !msg.isBlank()).distinct().collect(Collectors.joining("\n")); - tc.throwStateRefinementError(invocation.getPosition(), prevState, expectedStatesDisjunction, message); + Predicate foundState = prevState.substituteVariable(instanceName, newInstanceName); + tc.throwStateRefinementError(invocation.getPosition(), foundState, expectedStatesDisjunction, message); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index cb3b0077..c91380ee 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -6,9 +6,7 @@ import java.util.Map; import java.util.stream.Collectors; -import liquidjava.diagnostics.errors.ArgumentMismatchError; import liquidjava.diagnostics.errors.LJError; -import liquidjava.diagnostics.errors.SyntaxError; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; @@ -88,7 +86,7 @@ protected Expression parse(String ref, CtElement element) throws LJError { return RefinementsParser.createAST(ref, prefix); } catch (LJError e) { // add location info to error - SourcePosition pos = Utils.getAnnotationPosition(element, ref); + SourcePosition pos = Utils.getLJAnnotationPosition(element, ref); e.setPosition(pos); throw e; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 96f32f66..ef50bf7c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -6,7 +6,6 @@ import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; -import com.microsoft.z3.FuncInterp; import com.microsoft.z3.IntExpr; import com.microsoft.z3.IntNum; import com.microsoft.z3.RealExpr; diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1e99e3f0..3924aefd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -5,9 +5,17 @@ import java.util.stream.Stream; import liquidjava.utils.constants.Types; +import spoon.reflect.code.CtBlock; +import spoon.reflect.code.CtFor; +import spoon.reflect.code.CtForEach; +import spoon.reflect.code.CtIf; +import spoon.reflect.code.CtTry; +import spoon.reflect.code.CtWhile; import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.CtAnnotation; +import spoon.reflect.declaration.CtConstructor; import spoon.reflect.declaration.CtElement; +import spoon.reflect.declaration.CtMethod; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; @@ -38,12 +46,29 @@ public static String qualifyName(String prefix, String name) { return String.format("%s.%s", prefix, name); } - public static SourcePosition getAnnotationPosition(CtElement element, String refinement) { + public static String getFile(CtElement element) { + SourcePosition pos = element.getPosition(); + if (pos == null || pos.getFile() == null) + return null; + + return pos.getFile().getAbsolutePath(); + } + + public static SourcePosition getLJAnnotationPosition(CtElement element, String refinement) { return element.getAnnotations().stream() .filter(a -> isLiquidJavaAnnotation(a) && hasRefinementValue(a, "\"" + refinement + "\"")).findFirst() .map(CtElement::getPosition).orElse(element.getPosition()); } + public static SourcePosition getFirstLJAnnotationPosition(CtElement element) { + return element.getAnnotations().stream().filter(Utils::isLiquidJavaAnnotation).map(CtElement::getPosition) + .min((p1, p2) -> { + if (p1.getLine() != p2.getLine()) + return Integer.compare(p1.getLine(), p2.getLine()); + return Integer.compare(p1.getColumn(), p2.getColumn()); + }).orElse(element.getPosition()); + } + private static boolean isLiquidJavaAnnotation(CtAnnotation annotation) { return annotation.getAnnotationType().getQualifiedName().startsWith("liquidjava.specification"); } @@ -52,4 +77,19 @@ private static boolean hasRefinementValue(CtAnnotation annotation, String ref Map values = annotation.getValues(); return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key)))); } + + public static SourcePosition getRealPosition(CtElement element) { + if (element instanceof CtBlock block) { + CtElement parent = block.getParent(); + if (parent instanceof CtIf ctIf) { + if (ctIf.getThenStatement() == element) { + return ctIf.getPosition(); + } + } else if (parent instanceof CtFor || parent instanceof CtForEach || parent instanceof CtWhile + || parent instanceof CtTry || parent instanceof CtMethod || parent instanceof CtConstructor) { + return parent.getPosition(); + } + } + return element.getPosition(); + } }