Treat operations and fields with unresolved types as unrefined (#388, #389, #390)

When a class is not on the classpath (the usual case when one file of a
project is verified), Spoon leaves the type of operations on its values,
and the declaring type of its fields, unset, and the verifier crashed on
them.

- A binary operation whose type, or the type of one of its operands, is
  unknown is now a fresh unknown boolean for comparisons and logical
  operators, and is left unrefined otherwise; an operator assignment with
  such a right-hand side gives the variable an unknown value.
- A negation of an operand with an unknown type is boolean; other unary
  operators on such operands are left unrefined.
- A field whose declaring type is unknown is qualified with its name only,
  so it matches no known field, and is not treated as an enum constant.

Unknown values carry no information, so a refinement that depends on them
is reported as not provable rather than accepted; violations next to them
are still reported (Error* fixtures). The example module excludes the
*Unresolved* test cases from javac, as they import missing classes on
purpose.

Fixes #388
Fixes #389
Fixes #390

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

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/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-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);