Treat operations and fields with unresolved types as unrefined

liquidjava-example/pom.xml

@@ -1,50 +1,54 @@
-<project xmlns="http://maven.apache.org/POM/4.0.0"
-	xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
-	xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 https://maven.apache.org/xsd/maven-4.0.0.xsd">
-
-	<modelVersion>4.0.0</modelVersion>
-	<groupId>liquidjava-example</groupId>
-	<artifactId>liquidjava-example</artifactId>
-	<version>0.0.1-SNAPSHOT</version>
-	<name>liquidjava-example</name>
-	<packaging>jar</packaging>
-
-	<build>
-		<plugins>
-			<plugin>
-				<groupId>org.apache.maven.plugins</groupId>
-				<artifactId>maven-compiler-plugin</artifactId>
-				<version>${pVersion.compiler}</version>
-				<configuration>
-					<source>20</source>
-					<target>20</target>
-				</configuration>
-			</plugin>
-		</plugins>
-	</build>
-
-	<properties>
-		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
-		<maven.compiler.source>20</maven.compiler.source>
-		<maven.compiler.target>20</maven.compiler.target>
-		<!-- versions -->
-		<version.junit>4.13.1</version.junit>
-		<version.memcompiler>1.3.0</version.memcompiler>
-		<!-- plugin versions -->
-		<pVersion.compiler>3.8.0</pVersion.compiler>
-		<pVersion.surefire>2.22.1</pVersion.surefire>
-	</properties>
-
-	<dependencies>
-		<dependency>
-			<groupId>org.mdkt.compiler</groupId>
-			<artifactId>InMemoryJavaCompiler</artifactId>
-			<version>${version.memcompiler}</version>
-		</dependency>
-		<dependency>
-			<groupId>io.github.liquid-java</groupId>
-			<artifactId>liquidjava-api</artifactId>
-			<version>0.0.7</version>
-		</dependency>
-	</dependencies>
-</project>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+	xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+	xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 https://maven.apache.org/xsd/maven-4.0.0.xsd">
+
+	<modelVersion>4.0.0</modelVersion>
+	<groupId>liquidjava-example</groupId>
+	<artifactId>liquidjava-example</artifactId>
+	<version>0.0.1-SNAPSHOT</version>
+	<name>liquidjava-example</name>
+	<packaging>jar</packaging>
+
+	<build>
+		<plugins>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-compiler-plugin</artifactId>
+				<version>${pVersion.compiler}</version>
+				<configuration>
+					<source>20</source>
+					<target>20</target>
+					<excludes>
+						<!-- test cases that use classes missing from the classpath on purpose -->
+						<exclude>testSuite/**/*Unresolved*.java</exclude>
+					</excludes>
+				</configuration>
+			</plugin>
+		</plugins>
+	</build>
+
+	<properties>
+		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
+		<maven.compiler.source>20</maven.compiler.source>
+		<maven.compiler.target>20</maven.compiler.target>
+		<!-- versions -->
+		<version.junit>4.13.1</version.junit>
+		<version.memcompiler>1.3.0</version.memcompiler>
+		<!-- plugin versions -->
+		<pVersion.compiler>3.8.0</pVersion.compiler>
+		<pVersion.surefire>2.22.1</pVersion.surefire>
+	</properties>
+
+	<dependencies>
+		<dependency>
+			<groupId>org.mdkt.compiler</groupId>
+			<artifactId>InMemoryJavaCompiler</artifactId>
+			<version>${version.memcompiler}</version>
+		</dependency>
+		<dependency>
+			<groupId>io.github.liquid-java</groupId>
+			<artifactId>liquidjava-api</artifactId>
+			<version>0.0.7</version>
+		</dependency>
+	</dependencies>
+</project>

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;
+        }
+    }
+}

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
+    }
+}

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();
+    }
+}

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);
+    }
+}

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);
+        };
+    }
+}

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
+        }
+    }
+}

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
+        }
+    }
+}

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
+    }
+}

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
+        }
+    }
+}

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
+    }
+}

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);
+        };
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

@@ -335,7 +335,8 @@ public <T> void visitCtFieldRead(CtFieldRead<T> 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);