diff --git a/liquidjava-example/pom.xml b/liquidjava-example/pom.xml index 0e1f5808..d029b288 100644 --- a/liquidjava-example/pom.xml +++ b/liquidjava-example/pom.xml @@ -1,50 +1,54 @@ - - - 4.0.0 - liquidjava-example - liquidjava-example - 0.0.1-SNAPSHOT - liquidjava-example - jar - - - - - org.apache.maven.plugins - maven-compiler-plugin - ${pVersion.compiler} - - 20 - 20 - - - - - - - UTF-8 - 20 - 20 - - 4.13.1 - 1.3.0 - - 3.8.0 - 2.22.1 - - - - - org.mdkt.compiler - InMemoryJavaCompiler - ${version.memcompiler} - - - io.github.liquid-java - liquidjava-api - 0.0.7 - - - + + + 4.0.0 + liquidjava-example + liquidjava-example + 0.0.1-SNAPSHOT + liquidjava-example + jar + + + + + org.apache.maven.plugins + maven-compiler-plugin + ${pVersion.compiler} + + 20 + 20 + + + testSuite/**/*Unresolved*.java + + + + + + + + UTF-8 + 20 + 20 + + 4.13.1 + 1.3.0 + + 3.8.0 + 2.22.1 + + + + + org.mdkt.compiler + InMemoryJavaCompiler + ${version.memcompiler} + + + io.github.liquid-java + liquidjava-api + 0.0.7 + + + diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedBinaryOperator.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedBinaryOperator.java new file mode 100644 index 00000000..14775088 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedBinaryOperator.java @@ -0,0 +1,59 @@ +package testSuite; + +import org.example.missing.Item; +import org.example.missing.Interrupts; + +import liquidjava.specification.Refinement; + +// Operations whose operand types cannot be resolved (classes not on the classpath) are unrefined (#388, #344) +@SuppressWarnings("unused") +public class CorrectUnresolvedBinaryOperator { + static boolean same(Item a, Item b) { + if (a.id() == b.id()) { + return true; + } + return false; + } + + static boolean comparedToConstant(Item p, int id) { + return p.getValue() == id; + } + + static void inLoop(Item embedding) { + for (int i = 0; i < embedding.length(); i++) { + } + } + + static void withKnownOperand(boolean someHandlerDefined) { + if (!someHandlerDefined || Interrupts.isInterruptsDisabled()) { + return; + } + } + + static boolean nested(Item x) { + return x.a() + 1 > 0; + } + + static String concatenation(Item i) { + return "Configuration is not an SQL config:" + i.name(); + } + + static void unknownVarNullCheck(Item x) { + var v = x.a(); + if (v == null) { + return; + } + } + + static void operatorAssignment(Item x) { + int c = 0; + c += x.a(); + } + + static void knownValuesStillUsed(Item x, int k) { + if (k > 0 && x.ok()) { + @Refinement("_ > 0") + int y = 1; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldDeclaringType.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldDeclaringType.java new file mode 100644 index 00000000..5ffb3609 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldDeclaringType.java @@ -0,0 +1,17 @@ +package testSuite; + +import org.example.missing.Config; + +// Fields whose declaring class cannot be resolved (#390) +@SuppressWarnings("unused") +public class CorrectUnresolvedFieldDeclaringType { + private static final int MIN_ADMIN_PASSWORD_LENGTH = 8; + + static boolean shortPassword(Config config) { + return config.httpAdminPassword.length() < MIN_ADMIN_PASSWORD_LENGTH; + } + + void undeclaredField(Exception e) { + log.error("get host name error:{}", e.getMessage()); // e.g., a field generated by Lombok + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedUnaryOperator.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedUnaryOperator.java new file mode 100644 index 00000000..6a1a83a7 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedUnaryOperator.java @@ -0,0 +1,22 @@ +package testSuite; + +import org.example.missing.Item; +import org.example.missing.Settings; + +// A negation of a call whose type cannot be resolved is an unknown boolean (#389) +@SuppressWarnings("unused") +public class CorrectUnresolvedUnaryOperator { + static void start(Settings settings) { + if (!settings.enabled()) { + return; + } + } + + static boolean negatedComparison(Item x) { + return !(x.a() == x.b()); + } + + static int negated(Item x) { + return -x.a(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectVarLocal.java b/liquidjava-example/src/main/java/testSuite/CorrectVarLocal.java new file mode 100644 index 00000000..1772fe3a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectVarLocal.java @@ -0,0 +1,28 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; + +// A var local has the static type of its initialiser (#344, #347) +@SuppressWarnings("unused") +@RefinementAlias("Port(int x) { 0 <= x && x <= 65535 }") +public class CorrectVarLocal { + static String name() { + return "x"; + } + + static void connect(@Refinement("Port(_)") int port) { + } + + static void nullCheck() { + var n = name(); + if (n == null) { + throw new IllegalArgumentException("no name"); + } + } + + static void refinedArgument() { + var port = 80; + connect(port); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectYieldRefinedConstructor.java b/liquidjava-example/src/main/java/testSuite/CorrectYieldRefinedConstructor.java new file mode 100644 index 00000000..5404e5f6 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectYieldRefinedConstructor.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +// Yielding a call to a refined constructor from a switch expression (#346) +@SuppressWarnings("unused") +public class CorrectYieldRefinedConstructor { + static class Conn { + public Conn(@Refinement("_ > 0") int port) { + } + } + + static Conn open(String scheme) { + return switch (scheme) { + case "tcp" -> { + yield new Conn(80); + } + default -> new Conn(1); + }; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedBinaryOperator.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedBinaryOperator.java new file mode 100644 index 00000000..f9415b3e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedBinaryOperator.java @@ -0,0 +1,18 @@ +package testSuite; + +import org.example.missing.Item; + +import liquidjava.specification.Refinement; + +// A violation under a comparison of values whose types cannot be resolved is still reported (#388) +@SuppressWarnings("unused") +public class ErrorUnresolvedBinaryOperator { + static void positive(@Refinement("_ > 0") int x) { + } + + static void comparison(Item a, Item b) { + if (a.id() == b.id()) { + positive(0); // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldDeclaringType.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldDeclaringType.java new file mode 100644 index 00000000..1f932c93 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldDeclaringType.java @@ -0,0 +1,18 @@ +package testSuite; + +import org.example.missing.Config; + +import liquidjava.specification.Refinement; + +// A violation next to a field whose declaring class cannot be resolved is still reported (#390) +@SuppressWarnings("unused") +public class ErrorUnresolvedFieldDeclaringType { + static void positive(@Refinement("_ > 0") int x) { + } + + static void field(Config config) { + if (config.httpAdminPassword.length() < 8) { + positive(-2); // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedOperationValue.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedOperationValue.java new file mode 100644 index 00000000..5d85250e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedOperationValue.java @@ -0,0 +1,14 @@ +package testSuite; + +import org.example.missing.Item; + +import liquidjava.specification.Refinement; + +// An operation whose operand types cannot be resolved has an unknown value (#388) +@SuppressWarnings("unused") +public class ErrorUnresolvedOperationValue { + static void unknownValue(Item x) { + @Refinement("_ > 0") + int y = x.a() + 1; // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedUnaryOperator.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedUnaryOperator.java new file mode 100644 index 00000000..1877cb30 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedUnaryOperator.java @@ -0,0 +1,18 @@ +package testSuite; + +import org.example.missing.Settings; + +import liquidjava.specification.Refinement; + +// A violation under a negation of a call whose type cannot be resolved is still reported (#389) +@SuppressWarnings("unused") +public class ErrorUnresolvedUnaryOperator { + static void positive(@Refinement("_ > 0") int x) { + } + + static void negation(Settings settings) { + if (!settings.enabled()) { + positive(-1); // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorVarLocal.java b/liquidjava-example/src/main/java/testSuite/ErrorVarLocal.java new file mode 100644 index 00000000..f23aff37 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorVarLocal.java @@ -0,0 +1,17 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; + +// The value of a var local is still checked against a refined parameter (#347) +@SuppressWarnings("unused") +@RefinementAlias("Port(int x) { 0 <= x && x <= 65535 }") +public class ErrorVarLocal { + static void connect(@Refinement("Port(_)") int port) { + } + + static void refinedArgument() { + var port = 70000; + connect(port); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorYieldRefinedConstructor.java b/liquidjava-example/src/main/java/testSuite/ErrorYieldRefinedConstructor.java new file mode 100644 index 00000000..d74bf552 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorYieldRefinedConstructor.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +// The arguments of a refined constructor yielded from a switch expression are checked (#346) +@SuppressWarnings("unused") +public class ErrorYieldRefinedConstructor { + static class Conn { + public Conn(@Refinement("_ > 0") int port) { + } + } + + static Conn open(String scheme) { + return switch (scheme) { + case "tcp" -> { + yield new Conn(-1); // Expect: Refinement Error + } + default -> new Conn(1); + }; + } +} 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 995c5927..0ed24307 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 @@ -335,7 +335,8 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { String targetName = fieldRead.getTarget().toString(); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), BuiltinFunctionPredicate.length(targetName, fieldRead))); - } else if (fieldRead.getVariable().getDeclaringType().getDeclaration() instanceof CtEnum) { + } else if (fieldRead.getVariable().getDeclaringType() != null + && fieldRead.getVariable().getDeclaringType().getDeclaration() instanceof CtEnum) { // only enums declared in the analyzed sources can be translated to SMT String target = fieldRead.getVariable().getDeclaringType().getSimpleName(); String enumLiteral = String.format(Formats.ENUM, target, fieldName); 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 8e387712..aa8d9d19 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 @@ -43,6 +43,7 @@ import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtType; import spoon.reflect.declaration.ParentNotInitializedException; +import spoon.reflect.reference.CtTypeReference; import spoon.reflect.reference.CtVariableReference; import spoon.support.reflect.code.CtIfImpl; @@ -74,6 +75,16 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr if (parent instanceof CtAnnotation) return; // Operations in annotations are not handled here + if (hasUnresolvedType(operator)) { + // an operand's type could not be resolved (e.g. its class is not on the classpath): the value of a + // comparison or logical operation is an unknown boolean, and any other operation is left unrefined + if (!isBooleanOperator(operator.getKind())) + return; + CtTypeReference booleanType = operator.getFactory().Type().booleanPrimitiveType(); + putBooleanRefinement(operator, parent, createFreshValue(operator, booleanType, new Predicate())); + return; + } + String type = operator.getType().getQualifiedName(); if (type.equals("java.lang.String")) return; @@ -93,10 +104,7 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr } List types = Arrays.asList(Types.IMPLEMENTED); if (type.contentEquals("boolean")) { - operator.putMetadata(Keys.REFINEMENT, oper); - if (parent instanceof CtLocalVariable || parent instanceof CtUnaryOperator - || parent instanceof CtReturn) - operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), oper)); + putBooleanRefinement(operator, parent, oper); } else if (types.contains(type)) { operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), oper)); } else { @@ -105,6 +113,34 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr // TODO ADD TYPES } + private static void putBooleanRefinement(CtBinaryOperator operator, CtElement parent, Predicate oper) { + operator.putMetadata(Keys.REFINEMENT, oper); + if (parent instanceof CtLocalVariable || parent instanceof CtUnaryOperator + || parent instanceof CtReturn) + operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), oper)); + } + + /** + * Whether the type of the operation, or of one of its operands (looking inside nested operations), could not be + * resolved, in which case Spoon leaves it unset + */ + private static boolean hasUnresolvedType(CtExpression e) { + if (e.getType() == null) + return true; + if (e instanceof CtBinaryOperator binop) + return hasUnresolvedType(binop.getLeftHandOperand()) || hasUnresolvedType(binop.getRightHandOperand()); + if (e instanceof CtUnaryOperator unop) + return hasUnresolvedType(unop.getOperand()); + return false; + } + + private static boolean isBooleanOperator(BinaryOperatorKind kind) { + return switch (kind) { + case EQ, NE, LT, LE, GT, GE, AND, OR, INSTANCEOF -> true; + default -> false; + }; + } + /** * Builds the refinement for a operator assignment. Java operator assignments such as {@code x += y} are modeled as * {@code x = x + y}; the returned predicate refines the assigned value as {@code _ == current(x) rhs}. @@ -114,6 +150,8 @@ public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperator String op = getOperatorFromKind(assignment.getKind()); if (op == null) // x |= y, x <<= n, ...: no counterpart in the integer logic, so the new value is unknown return new Predicate(); + if (hasUnresolvedType(assignment.getAssignment())) // the right-hand side has an unknown type + return new Predicate(); Predicate left = getCurrentVariableValue(assignedName); Predicate right = getOperatorAssignmentRefinement(assignment.getAssignment()); Predicate operation = Predicate.createOperation(left, op, right); @@ -165,6 +203,13 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro } } + CtTypeReference type = ex.getType(); + if (type == null) { + // the operand's type could not be resolved: a negation is still boolean, anything else is unrefined + if (operator.getKind() != UnaryOperatorKind.NOT) + return; + type = operator.getFactory().Type().booleanPrimitiveType(); + } Predicate metadata = rtc.getRefinement(ex); String newName = !name.equals(Formats.FRESH) ? String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()) @@ -176,7 +221,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro Predicate opS = unOp.substituteVariable(Keys.WILDCARD, newName); all = p instanceof CtIf ? opS : Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), opS); // TODO SEE IF () IN OPS IS NEEDED - rtc.getContext().addInstanceToContext(newName, ex.getType(), newMeta, operator); + rtc.getContext().addInstanceToContext(newName, type, newMeta, operator); operator.putMetadata(Keys.REFINEMENT, all); } @@ -424,9 +469,13 @@ private Predicate valueFromRefinement(CtExpression element, Predicate refinem } private Predicate createFreshValue(CtExpression element, Predicate refinement) { + return createFreshValue(element, element.getType(), refinement); + } + + private Predicate createFreshValue(CtExpression element, CtTypeReference type, Predicate refinement) { String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); Predicate freshRefinement = refinement.substituteVariable(Keys.WILDCARD, newName); - rtc.getContext().addVarToContext(newName, element.getType(), freshRefinement, element); + rtc.getContext().addVarToContext(newName, type, freshRefinement, element); return Predicate.createVar(newName); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 018287e4..cf3042ea 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -53,6 +53,8 @@ public static String qualifyName(String prefix, String name) { } public static String qualifyFieldName(CtFieldReference field) { + if (field.getDeclaringType() == null) // declaring class not resolved: matches no known field + return "this#" + field.getSimpleName(); return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); }