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/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..2ea6444b 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,31 +44,42 @@ 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(), + return String.format("%d:%d-%d:%d", annPosition.getLine(), annPosition.getColumn() + 1, pos.getEndLine(), pos.getEndColumn()); } @@ -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"); }