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..affc6ae9 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) 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..c6e6fd46 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.addPlacementInCode(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.addPlacementInCode(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.addPlacementInCode(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..0aa1a9a7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/ContextHistory.java @@ -5,24 +5,27 @@ 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; +import spoon.reflect.declaration.CtParameter; public class ContextHistory { private static ContextHistory instance; private Map>> fileScopeVars; // file -> (scope -> variables in scope) + private Map> ghosts; // file -> ghosts + + // globals + private Set aliases; private Set instanceVars; private Set globalVars; - private Set ghosts; - private Set aliases; private ContextHistory() { fileScopeVars = new HashMap<>(); instanceVars = new HashSet<>(); globalVars = new HashSet<>(); - ghosts = new HashSet<>(); + ghosts = new HashMap<>(); aliases = new HashSet<>(); } @@ -41,32 +44,43 @@ public void clearHistory() { } public void saveContext(CtElement element, Context context) { - SourcePosition pos = element.getPosition(); - if (pos == null || pos.getFile() == null) + String file = getFile(element); + if (file == null) return; - // add variables in scope for this position - String file = pos.getFile().getAbsolutePath(); + // add variables in scope String scope = getScopePosition(element); fileScopeVars.putIfAbsent(file, new HashMap<>()); fileScopeVars.get(file).put(scope, new HashSet<>(context.getCtxVars())); - // add other elements in context + // add other elements in context (except ghosts) instanceVars.addAll(context.getCtxInstanceVars()); globalVars.addAll(context.getCtxGlobalVars()); - ghosts.addAll(context.getGhostStates()); aliases.addAll(context.getAliases()); } + public void saveGhost(CtElement element, GhostState ghost) { + String file = getFile(element); + if (file == null) + return; + ghosts.putIfAbsent(file, new HashSet<>()); + ghosts.get(file).add(ghost); + } + + private String getFile(CtElement element) { + SourcePosition pos = element.getPosition(); + if (pos == null || pos.getFile() == null) + return null; + + return pos.getFile().getAbsolutePath(); + } + public String getScopePosition(CtElement element) { + CtElement startElement = element instanceof CtParameter ? element.getParent() : element; + SourcePosition annPosition = Utils.getFirstLJAnnotationPosition(startElement); 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()); + return String.format("%d:%d-%d:%d", annPosition.getLine() - 1, annPosition.getColumn() - 1, + pos.getEndLine() - 1, pos.getEndColumn() - 1); } public Map>> getFileScopeVars() { @@ -81,7 +95,7 @@ public Set getGlobalVars() { return globalVars; } - public Set getGhosts() { + public Map> getGhosts() { return ghosts; } 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..7a04abde 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java @@ -4,15 +4,21 @@ import java.util.List; import java.util.Set; import liquidjava.rj_language.Predicate; +import liquidjava.utils.Utils; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.declaration.CtElement; import spoon.reflect.reference.CtTypeReference; public abstract class RefinedVariable extends Refined { private final List> supertypes; private PlacementInCode placementInCode; + private boolean isParameter; + private SourcePosition annPosition; public RefinedVariable(String name, CtTypeReference type, Predicate c) { super(name, type, c); supertypes = new ArrayList<>(); + isParameter = false; } public abstract Predicate getMainRefinement(); @@ -34,14 +40,23 @@ public void addSuperTypes(CtTypeReference ts, Set> sts) { supertypes.add(ct); } - public void addPlacementInCode(PlacementInCode s) { - placementInCode = s; + public void addPlacementInCode(CtElement element) { + placementInCode = PlacementInCode.createPlacement(element); + annPosition = Utils.getFirstLJAnnotationPosition(element); + } + + public void addPlacementInCode(PlacementInCode placement) { + placementInCode = placement; } public PlacementInCode getPlacementInCode() { return placementInCode; } + public SourcePosition getAnnPosition() { + return annPosition; + } + @Override public int hashCode() { final int prime = 31; @@ -65,4 +80,12 @@ public boolean equals(Object obj) { return supertypes.equals(other.supertypes); } } + + public void setIsParameter(boolean b) { + isParameter = b; + } + + public boolean isParameter() { + return isParameter; + } } 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..87384e44 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 @@ -8,6 +8,7 @@ import liquidjava.diagnostics.warnings.ExternalClassNotFoundWarning; import liquidjava.diagnostics.warnings.ExternalMethodNotFoundWarning; import liquidjava.processor.context.Context; +import liquidjava.processor.context.ContextHistory; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.GhostDTO; import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker; @@ -28,8 +29,9 @@ 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(); + private final ContextHistory contextHistory = ContextHistory.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..296e4334 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java @@ -9,6 +9,7 @@ import liquidjava.diagnostics.errors.*; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; +import liquidjava.processor.context.ContextHistory; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.context.GhostState; import liquidjava.processor.context.RefinedVariable; @@ -40,6 +41,7 @@ public abstract class TypeChecker extends CtScanner { protected final Context context; protected final Factory factory; protected final VCChecker vcChecker; + private final ContextHistory contextHistory = ContextHistory.getInstance(); public TypeChecker(Context context, Factory factory) { this.context = context; @@ -81,7 +83,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()); } @@ -157,6 +159,7 @@ private void createStateSet(CtNewArray e, int set, CtElement element) th gs.setRefinement(Predicate.createEquals(ip, Predicate.createLit(Integer.toString(order), Types.INT))); // open(THIS) -> state1(THIS) == 1 context.addToGhostClass(g.getParentClassName(), gs); + contextHistory.saveGhost(element, gs); } order++; } @@ -191,6 +194,7 @@ private void createStateGhost(String string, CtElement element, SourcePosition p CtTypeReference r = factory.Type().createReference(gd.returnType()); GhostState gs = new GhostState(gd.name(), param, r, qn); context.addToGhostClass(sn, gs); + contextHistory.saveGhost(element, gs); } protected String getQualifiedClassName(CtElement element) { 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 af16bf92..1f1decda 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 @@ -154,6 +154,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method, c = oc.get().substituteVariable(Keys.WILDCARD, paramName); param.putMetadata(Keys.REFINEMENT, c); RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param); + v.setIsParameter(true); rtc.getMessageFromAnnotation(param).ifPresent(v::setMessage); if (v instanceof Variable) f.addArgRefinements((Variable) v); 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..cb70c2e9 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); } 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..f6931b52 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -88,7 +88,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/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 1e99e3f0..3119151f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -38,12 +38,21 @@ 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 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"); }