diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 5f4e0969..c65d7551 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -256,6 +256,7 @@ 5.10.0 1.3.0 + 1.12.0 10.4.2 4.8.17 @@ -280,6 +281,11 @@ + + org.apache.commons + commons-text + ${version.commons-text} + org.junit.platform diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/NameSuggester.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/NameSuggester.java new file mode 100644 index 00000000..3c0daaf7 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/NameSuggester.java @@ -0,0 +1,54 @@ +package liquidjava.diagnostics; + +import java.util.Collection; +import java.util.Comparator; +import java.util.Locale; +import java.util.Optional; + +import org.apache.commons.text.similarity.JaroWinklerSimilarity; + +import liquidjava.utils.Utils; + +/** + * Finds the closest matching name among the elements available in the current context using Jaro-Winkler similarity + */ +public final class NameSuggester { + + private static final int MINIMUM_NAME_LENGTH = 3; + private static final double MINIMUM_SIMILARITY = 0.9; + private static final JaroWinklerSimilarity SIMILARITY = new JaroWinklerSimilarity(); + + private NameSuggester() { + } + + public static Optional findClosest(String name, Collection candidates) { + if (name == null || candidates == null || candidates.isEmpty()) + return Optional.empty(); + + String sourceName = getSourceName(name); + if (sourceName.length() < MINIMUM_NAME_LENGTH) + return Optional.empty(); // do not provide suggestions for very short names + + String normalizedSourceName = sourceName.toLowerCase(Locale.ROOT); + return candidates.stream().filter(candidate -> candidate != null).map(NameSuggester::getSourceName).distinct() + .filter(candidate -> candidate.length() >= MINIMUM_NAME_LENGTH && !candidate.equals(sourceName)) + .map(candidate -> new Match(candidate, + SIMILARITY.apply(normalizedSourceName, candidate.toLowerCase(Locale.ROOT)))) + .filter(match -> match.similarity() >= MINIMUM_SIMILARITY) + .max(Comparator.comparingDouble(Match::similarity).thenComparing(Match::name, + String.CASE_INSENSITIVE_ORDER.reversed())) + .map(Match::name); + } + + private static String getSourceName(String name) { + String simpleName = Utils.getSimpleName(name); + if (simpleName.startsWith("this#")) + return simpleName.substring("this#".length()); + if (simpleName.startsWith("#")) + return simpleName.substring(1).replaceFirst("_\\d+$", ""); + return simpleName; + } + + private record Match(String name, double similarity) { + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java index f354963f..f933c673 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/NotFoundError.java @@ -1,5 +1,9 @@ package liquidjava.diagnostics.errors; +import java.util.Collection; +import java.util.Locale; + +import liquidjava.diagnostics.NameSuggester; import liquidjava.diagnostics.TranslationTable; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; @@ -12,27 +16,40 @@ public class NotFoundError extends LJError { private final String name; - private final String kind; // "Variable" | "Ghost" | "Alias" + private final Kind kind; - public NotFoundError(String name, String kind) { - this(null, name, kind, null); + public NotFoundError(String name, Kind kind, Collection availableElements) { + this(null, name, kind, null, availableElements); } - public NotFoundError(SourcePosition position, String name, String kind) { - this(position, name, kind, null); + public NotFoundError(SourcePosition position, String name, Kind kind, Collection availableElements) { + this(position, name, kind, null, availableElements); } - public NotFoundError(SourcePosition position, String name, String kind, TranslationTable translationTable) { - super("Not Found Error", String.format("%s '%s' not found", kind, name), position, translationTable); + public NotFoundError(SourcePosition position, String name, Kind kind, TranslationTable translationTable, + Collection availableElements) { + super("Not Found Error", String.format("%s '%s' could not be found", kind, name), position, translationTable); this.name = Utils.getSimpleName(name); this.kind = kind; + NameSuggester.findClosest(name, availableElements) + .ifPresent(match -> setHint(String.format("Did you mean '%s'?", match))); } public String getName() { return name; } - public String getKind() { + public Kind getKind() { return kind; } + + public enum Kind { + VARIABLE, GHOST, ALIAS, CONSTANT; + + @Override + public String toString() { + String name = name().toLowerCase(Locale.ROOT); + return Character.toUpperCase(name.charAt(0)) + name.substring(1); + } + } } 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 c1d0dd87..6a5e3b38 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 @@ -206,9 +206,9 @@ private static ObjectState getStates(CtAnnotation ctAnnota */ private static Predicate createStatePredicate(String value, String targetClass, TypeChecker tc, CtElement e, boolean isTo, String prefix) throws LJError { + SourcePosition position = Utils.getLJAnnotationPosition(e, value); Predicate p = new Predicate(value, e, prefix); if (!p.getExpression().isBooleanExpression()) { - SourcePosition position = Utils.getLJAnnotationPosition(e, value); throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression", value); } @@ -233,11 +233,9 @@ private static Predicate createStatePredicate(String value, String targetClass, Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p; Predicate c = c1.substituteVariable(Keys.THIS, name); c = c.changeOldMentions(nameOld, name); - boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), e.getPosition(), true); - if (ok) { - SourcePosition pos = Utils.getLJAnnotationPosition(e, value); - tc.throwStateConflictError(pos, p); - } + boolean ok = tc.checkStateSMT(new Predicate(), c.negate(), position, true); + if (ok) + tc.throwStateConflictError(position, p); return c1; } 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 696ef5eb..2839babf 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -8,6 +8,7 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; +import liquidjava.diagnostics.errors.NotFoundError.Kind; import liquidjava.processor.context.AliasWrapper; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; @@ -100,7 +101,7 @@ private static Expression resolveStaticFinalConstants(Expression root, CtElement String hint = suggested != null ? "Add: import " + suggested + ";" : "Add an import for '" + en.getTypeName() + "' if it is a Java class with a static final field"; String name = en.getTypeName() + "." + en.getConstName(); - NotFoundError error = new NotFoundError(pos, name, "Constant"); + NotFoundError error = new NotFoundError(pos, name, Kind.CONSTANT, List.of()); error.setHint(hint); throw error; } 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 d33b4fce..f2502024 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 @@ -8,6 +8,7 @@ import liquidjava.diagnostics.errors.ArgumentMismatchError; import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; +import liquidjava.diagnostics.errors.NotFoundError.Kind; import liquidjava.processor.context.Context; import liquidjava.processor.context.GhostFunction; import liquidjava.processor.facade.AliasDTO; @@ -15,7 +16,6 @@ import liquidjava.rj_language.ast.typing.TypeInfer; import liquidjava.rj_language.visitors.ExpressionVisitor; import liquidjava.utils.Utils; -import liquidjava.utils.constants.Keys; import spoon.reflect.factory.Factory; import spoon.reflect.reference.CtTypeReference; @@ -199,34 +199,33 @@ private void auxSubstituteState(Map subMap, String[] toChang public Expression changeAlias(Map alias, Context ctx, Factory f) throws LJError { Expression e = clone(); if (this instanceof AliasInvocation ai) { - if (alias.containsKey(ai.name)) { // object state - AliasDTO dto = alias.get(ai.name); - // check argument count - if (children.size() != dto.getVarNames().size()) { + if (!alias.containsKey(ai.name)) + throw new NotFoundError(ai.getName(), Kind.ALIAS, alias.keySet()); + AliasDTO dto = alias.get(ai.name); + // check argument count + if (children.size() != dto.getVarNames().size()) { + String msg = String.format("Wrong number of arguments in alias invocation '%s': expected %d, got %d", + ai.name, dto.getVarNames().size(), children.size()); + throw new ArgumentMismatchError(msg); + } + Expression sub = dto.getExpression().clone(); + for (int i = 0; i < children.size(); i++) { + Expression varExp = new Var(dto.getVarNames().get(i)); + String varType = dto.getVarTypes().get(i); + Expression aliasExp = children.get(i); + + // check argument types + boolean compatible = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f); + if (!compatible) { String msg = String.format( - "Wrong number of arguments in alias invocation '%s': expected %d, got %d", ai.name, - dto.getVarNames().size(), children.size()); + "Argument '%s' and parameter '%s' of alias '%s' types are incompatible: expected %s, got %s", + aliasExp, dto.getVarNames().get(i), ai.name, varType, + TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName()); throw new ArgumentMismatchError(msg); } - Expression sub = dto.getExpression().clone(); - for (int i = 0; i < children.size(); i++) { - Expression varExp = new Var(dto.getVarNames().get(i)); - String varType = dto.getVarTypes().get(i); - Expression aliasExp = children.get(i); - - // check argument types - boolean compatible = TypeInfer.checkCompatibleType(varType, aliasExp, ctx, f); - if (!compatible) { - String msg = String.format( - "Argument '%s' and parameter '%s' of alias '%s' types are incompatible: expected %s, got %s", - aliasExp, dto.getVarNames().get(i), ai.name, varType, - TypeInfer.getType(ctx, f, aliasExp).get().getQualifiedName()); - throw new ArgumentMismatchError(msg); - } - sub = sub.substitute(varExp, aliasExp); - } - e = sub; + sub = sub.substitute(varExp, aliasExp); } + e = sub; } e.auxChangeAlias(alias, ctx, f); return e; @@ -237,7 +236,7 @@ private void auxChangeAlias(Map alias, Context ctx, Factory f) for (int i = 0; i < children.size(); i++) { if (children.get(i)instanceof AliasInvocation ai) { if (!alias.containsKey(ai.name)) - throw new NotFoundError(ai.getName(), Keys.ALIAS); + throw new NotFoundError(ai.getName(), Kind.ALIAS, alias.keySet()); AliasDTO dto = alias.get(ai.name); // check argument count if (ai.children.size() != dto.getVarNames().size()) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java index 8eb366ea..ab4adfff 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java @@ -23,11 +23,11 @@ import liquidjava.diagnostics.errors.LJError; import liquidjava.diagnostics.errors.NotFoundError; +import liquidjava.diagnostics.errors.NotFoundError.Kind; import liquidjava.processor.context.AliasWrapper; import liquidjava.utils.Pair; import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; -import liquidjava.utils.constants.Keys; import com.microsoft.z3.enumerations.Z3_sort_kind; import org.apache.commons.lang3.NotImplementedException; @@ -120,12 +120,12 @@ public Expr makeBooleanLiteral(boolean value) { private Expr getVariableTranslation(String name) throws LJError { if (!varTranslation.containsKey(name)) - throw new NotFoundError(name, Keys.VARIABLE); + throw new NotFoundError(name, Kind.VARIABLE, varTranslation.keySet()); Expr e = varTranslation.get(name); if (e == null) e = varTranslation.get(String.format("this#%s", name)); if (e == null) - throw new NotFoundError(name, Keys.VARIABLE); + throw new NotFoundError(name, Kind.VARIABLE, varTranslation.keySet()); return e; } @@ -213,7 +213,7 @@ private FuncDecl resolveFunctionDecl(String name, Expr[] params) throws LJ if (candidate != null) { return candidate; } - throw new NotFoundError(name, Keys.GHOST); + throw new NotFoundError(name, Kind.GHOST, funcTranslation.keySet()); } @SuppressWarnings({ "unchecked", "rawtypes" }) diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestNameSuggester.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestNameSuggester.java new file mode 100644 index 00000000..9cf2d6ce --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestNameSuggester.java @@ -0,0 +1,78 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import java.util.Arrays; +import java.util.List; + +import org.junit.jupiter.api.Test; + +import liquidjava.diagnostics.NameSuggester; + +class TestNameSuggester { + + @Test + void findsClosestName() { + assertEquals("amount", NameSuggester.findClosest("ammount", List.of("total", "amount")).orElseThrow()); + } + + @Test + void recognizesTransposedCharacters() { + assertEquals("length", NameSuggester.findClosest("lenght", List.of("length")).orElseThrow()); + } + + @Test + void normalizesQualifiedAndGeneratedNames() { + assertEquals("length", NameSuggester.findClosest("Example.lenght", List.of("Example.length")).orElseThrow()); + assertEquals("amount", NameSuggester.findClosest("ammount", List.of("#amount_12")).orElseThrow()); + assertEquals("value", NameSuggester.findClosest("valuee", List.of("this#value")).orElseThrow()); + } + + @Test + void doesNotSuggestUnrelatedOrVeryShortNames() { + assertTrue(NameSuggester.findClosest("counter", List.of("result", "value")).isEmpty()); + assertTrue(NameSuggester.findClosest("x", List.of("y")).isEmpty()); + } + + @Test + void handlesMissingAndEmptyInputs() { + assertTrue(NameSuggester.findClosest(null, List.of("value")).isEmpty()); + assertTrue(NameSuggester.findClosest("value", null).isEmpty()); + assertTrue(NameSuggester.findClosest("value", List.of()).isEmpty()); + assertTrue(NameSuggester.findClosest("", List.of("value")).isEmpty()); + } + + @Test + void ignoresNullBlankAndExactCandidates() { + assertEquals("amount", NameSuggester.findClosest("ammount", Arrays.asList(null, "", "amount")).orElseThrow()); + assertTrue(NameSuggester.findClosest("amount", List.of("amount")).isEmpty()); + assertTrue(NameSuggester.findClosest("amount", List.of("Example.amount", "#amount_1")).isEmpty()); + } + + @Test + void preservesCandidateCapitalization() { + assertEquals("Amount", NameSuggester.findClosest("amount", List.of("Amount")).orElseThrow()); + } + + @Test + void supportsNamesAtMinimumLength() { + assertEquals("size", NameSuggester.findClosest("siz", List.of("size")).orElseThrow()); + } + + @Test + void rejectsNamesJustBelowSimilarityThreshold() { + assertTrue(NameSuggester.findClosest("abc", List.of("abd")).isEmpty()); + } + + @Test + void prefersTheMostSimilarCandidate() { + assertEquals("availableValue", + NameSuggester.findClosest("availableValu", List.of("availableValues", "availableValue")).orElseThrow()); + } + + @Test + void breaksEquivalentMatchesAlphabetically() { + assertEquals("foobart", NameSuggester.findClosest("foobaru", List.of("foobarv", "foobart")).orElseThrow()); + } +}