Add foundational support for class/record/sealed types

verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java

@@ -33,6 +33,12 @@ public class JavaToLaurelCompiler {
     private final VerifyAnnotationCompiler annotationCompiler;
     JCTree.JCCompilationUnit currentCompilationUnit;
 
+    /// Names of class/record/sealed types referenced as opaque Laurel
+    /// CompositeType sorts during translation. Each must be declared with
+    /// a compositeCommand so Strata's resolver can find the sort; insertion
+    /// order is preserved for deterministic output.
+    private final Set<String> referencedCompositeTypes = new LinkedHashSet<>();
+
     public JavaToLaurelCompiler(Context context) {
         lowerer = context.get(JavaLowerer.class);
         contractCompiler = MethodOrLoopContractCompiler.instance(context);
@@ -49,6 +55,7 @@ public AnalysisResult analyzeJavaCode(VerifierOptions verifierOptions, List<Java
 
         Map<URI, com.sun.tools.javac.util.Position.LineMap> lineMaps = new HashMap<>();
         boolean first = true;
+        Set<String> emittedCompositeTypes = new HashSet<>();
         for (var compilationUnit : loweredResult.parsed()) {
             if (lowerer.isContractSource(compilationUnit)) {
                 continue;
@@ -62,6 +69,15 @@ public AnalysisResult analyzeJavaCode(VerifierOptions verifierOptions, List<Java
                 commands.addAll(getPredefinedTypes());
                 first = false;
             }
+            // Declare each opaque composite sort referenced so far that has
+            // not been declared yet, before the procedures that use it, so
+            // Strata's resolver can find the sort.
+            for (var typeName : referencedCompositeTypes) {
+                if (emittedCompositeTypes.add(typeName)) {
+                    commands.add(compositeCommand(
+                            composite(typeName, Optional.empty(), List.of(), List.of())));
+                }
+            }
             for (var proc : visitor.procedures) {
                 commands.add(procedureCommand(proc));
             }
@@ -119,6 +135,27 @@ private static StmtExpr longLiteral(SourceRange sr, long val) {
     }
 
     private LaurelType translateType(com.sun.tools.javac.code.Type type) {
+        // Class / interface types (including sealed hierarchies and
+        // records): encode as an opaque Laurel CompositeType named
+        // after the source-side type. Strata treats unbound composite
+        // types as uninterpreted reference sorts, which is enough
+        // for parameter-position acceptance (e.g.
+        // `static void leftIdentityNone(PathLengthRange r)`).
+        // Body-level operations on the value (instanceof, pattern
+        // match, record-component reads, constructors) need
+        // additional translation that is NOT part of this commit;
+        // they will surface as separate convertExpression errors.
+        if (type instanceof com.sun.tools.javac.code.Type.ClassType classType) {
+            String name = classType.tsym.getQualifiedName().toString();
+            // Use the fully-qualified name (with the `$` nested-class
+            // separator normalised to `.`) as the CompositeType sort
+            // name. Keeping the package makes the name stable and
+            // collision-free across two same-named classes in
+            // different packages.
+            String sortName = name.replace('$', '.');
+            referencedCompositeTypes.add(sortName);
+            return compositeType(sortName);
+        }
         return switch (type.getTag()) {
             case INT -> compositeType("int32");
             case SHORT -> compositeType("int16");
@@ -131,7 +168,11 @@ private LaurelType translateType(com.sun.tools.javac.code.Type type) {
     }
 
     private static String qualifiedMethodName(Symbol.MethodSymbol sym) {
-        return sym.outermostClass().name + "_" + sym.name;
+        // Use the outermost class's fully-qualified (package-included) name,
+        // sanitised like the CompositeType sort names ('$' -> '.'), so two
+        // same-named classes in different packages don't produce colliding
+        // procedure names.
+        return sym.outermostClass().getQualifiedName().toString().replace('$', '.') + "_" + sym.name;
     }
 
     private class StaticMethodCollector extends TreeScanner {
@@ -570,6 +611,54 @@ yield call(toSourceRange(invocation),
                 // expression's type.
                 case JCTree.JCFieldAccess fa when fa.type.constValue() != null ->
                     convertConstantValue(toSourceRange(fa), fa.type.getTag(), fa.type.constValue());
+                case JCTree.JCNewClass newClass -> {
+                    // `new T(...)` for class / record types: produce
+                    // a Laurel `new_(T)` value of the matching
+                    // CompositeType. Constructor arguments are NOT
+                    // captured into the resulting value yet — that
+                    // would need a Laurel datatype declaration with
+                    // constructor args matching the source. For
+                    // verification of identity-style properties
+                    // that compare references (e.g. `cover(None, r)
+                    // == r`) the opaque value is sufficient. Body-
+                    // level inspection of record components will
+                    // still error until the datatype encoding
+                    // lands.
+                    SourceRange sr = toSourceRange(newClass);
+                    String name = newClass.type.tsym
+                            .getQualifiedName().toString()
+                            .replace('$', '.');
+                    // Declare the opaque composite sort even when the type
+                    // appears only here (in `new T(...)`) and never in a
+                    // type position, so the new_(T) value resolves.
+                    referencedCompositeTypes.add(name);
+                    // Translate each argument so unsupported argument
+                    // expressions still surface as errors, but DISCARD
+                    // the result: the opaque new_(T) value models only
+                    // the reference identity, not the constructor's
+                    // arguments or their side effects. Capturing those
+                    // needs a Laurel datatype encoding and expression
+                    // sequencing (let/temporaries), which is future
+                    // work.
+                    for (var arg : newClass.args) {
+                        convertExpression(arg, renames);
+                    }
+                    yield new_(sr, name);
+                }
+                case JCTree.JCInstanceOf instanceOf -> {
+                    // `r instanceof X`: the opaque-CompositeType
+                    // encoding carries no runtime tag, so the test
+                    // cannot be modelled precisely yet. Fail with a
+                    // clear, attributable error rather than emitting an
+                    // undeclared `instanceOf_<X>` predicate symbol
+                    // (which would surface only as a confusing
+                    // downstream "Resolution failed" message, and whose
+                    // simple-name form could even collide across
+                    // packages). A precise encoding needs a tagged
+                    // datatype representation; future work.
+                    throw new JavaViolationException(
+                        "instanceof on opaque reference types is not yet supported");
+                }
                 default -> throw new JavaViolationException("Unsupported expression: " + expr.getClass().getSimpleName());
             };
         }

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/records/AcceptClassParam.java

@@ -0,0 +1,16 @@
+package org.strata.jverify.verifier.tests.javasupport.records;
+
+import org.strata.jverify.testengine.JVerifyTest;
+
+/**
+ * A method with a class/record-typed parameter is accepted and verifies:
+ * the type is modelled as an opaque Laurel composite sort, which is now
+ * declared (via compositeCommand) so Strata's resolver can find it.
+ */
+@JVerifyTest(methodsVerified = 3, errorCount = 0)
+class AcceptClassParam {
+    record Point(int x, int y) {}
+
+    static void acceptParam(Point p) {
+    }
+}

verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/records/NewOnlyRecordType.java

@@ -0,0 +1,17 @@
+package org.strata.jverify.verifier.tests.javasupport.records;
+
+import org.strata.jverify.testengine.JVerifyTest;
+
+/**
+ * A record/class type used ONLY in `new T(...)` position (never in a type
+ * position such as a parameter, local, or return) must still have its opaque
+ * composite sort declared, so the `new_(T)` value resolves.
+ */
+@JVerifyTest(methodsVerified = 3, errorCount = 0)
+class NewOnlyRecordType {
+    record Q(int x) {}
+
+    static void make() {
+        new Q(1);
+    }
+}