Access-permissions on interfaces

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/ProgramConverter.kt

@@ -7,7 +7,6 @@ package org.jetbrains.kotlin.formver.core.conversion
 
 import org.jetbrains.kotlin.KtSourceElement
 import org.jetbrains.kotlin.descriptors.Visibilities
-import org.jetbrains.kotlin.descriptors.isInterface
 import org.jetbrains.kotlin.fir.FirSession
 import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction
 import org.jetbrains.kotlin.fir.declarations.processAllDeclarations
@@ -234,7 +233,6 @@ class ProgramConverter(
         val newDetails =
             ClassEmbeddingDetails(
                 embedding,
-                symbol.classKind.isInterface,
             )
         embedding.initDetails(newDetails)
 

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/types/ClassEmbeddingDetails.kt

@@ -16,7 +16,6 @@ import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
 
 class ClassEmbeddingDetails(
     val type: ClassTypeEmbedding,
-    val isInterface: Boolean,
 ) : TypeInvariantHolder {
     private var _superTypes: List<PretypeEmbedding>? = null
     val superTypes: List<PretypeEmbedding>
@@ -110,19 +109,26 @@ class ClassEmbeddingDetails(
 
     override fun subTypeInvariant(): TypeInvariantEmbedding = type.subTypeInvariant()
 
-    // Returns the sequence of classes in a hierarchy that need to be unfolded in order to access the given field
-    fun hierarchyPathTo(field: FieldEmbedding): Sequence<ClassTypeEmbedding> = sequence {
-        val className = field.containingClass?.name
-        require(className != null) { "Cannot find hierarchy unfold path of a field with no class information" }
-        if (className == type.name) {
-            yield([email protected])
-        } else {
-            val sup = classSuperTypes.firstOrNull { !it.details.isInterface }
-                ?: throw IllegalArgumentException("Reached top of the hierarchy without finding the field")
-
-            yield([email protected])
-            yieldAll(sup.details.hierarchyPathTo(field))
+    /**
+     * Returns the sequence of types to unfold to reach [target] from the current type.
+     * Returns an empty sequence if the current type already is [target].
+     * Throws if [target] is unreachable.
+     */
+    fun hierarchyPathTo(target: ClassTypeEmbedding): Sequence<ClassTypeEmbedding> =
+        pathToOrNull(target)?.asSequence()
+            ?: throw IllegalArgumentException("Could not find a path from ${type.name} to ${target.name} in the class hierarchy")
+
+    /**
+     * Returns the path of types to unfold from the current type to reach [target], or `null` if unreachable.
+     * An empty list means the current type IS the target.
+     */
+    private fun pathToOrNull(target: ClassTypeEmbedding): List<ClassTypeEmbedding>? {
+        if (type == target) return emptyList()
+        for (sup in classSuperTypes) {
+            val subPath = sup.details.pathToOrNull(target) ?: continue
+            return listOf(type) + subPath
         }
+        return null
     }
 
     fun <R> flatMapUniqueFields(action: (SimpleKotlinName, FieldEmbedding) -> List<R>): List<R> {

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/types/TypeEmbedding.kt

@@ -100,9 +100,13 @@ data class TypeEmbedding(val pretype: PretypeEmbedding, val flags: TypeEmbedding
     override val debugTreeView: TreeView
         get() = PlaintextLeaf(name.mangled)
 
-    fun hierarchyPathTo(field: FieldEmbedding): Sequence<ClassTypeEmbedding>? =
-        // TODO: Find a nicer solution to avoid this cast. It should really be: type.hierarchyPathTo(field)
-        (pretype as? ClassTypeEmbedding)?.details?.hierarchyPathTo(field)
+    fun hierarchyPathTo(field: FieldEmbedding): Sequence<ClassTypeEmbedding>? {
+        if (pretype !is ClassTypeEmbedding) return null
+        val target = requireNotNull(field.containingClass) {
+            "Cannot find hierarchy path of a field with no class information"
+        }
+        return pretype.details.hierarchyPathTo(target).plus(target)
+    }
 }
 
 data class TypeEmbeddingFlags(val nullable: Boolean) {

formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginNoVerificationDiagnosticsTestGenerated.java

@@ -238,6 +238,12 @@ public void testAllFilesPresentInPure_functions() {
         KtTestUtil.assertAllTestsPresentByMetadataWithExcluded(this.getClass(), new File("formver.compiler-plugin/testData/diagnostics/verification/pure_functions"), Pattern.compile("^(.+)\\.kt$"), null, true);
       }
 
+      @Test
+      @TestMetadata("heap_dependent_specifications.kt")
+      public void testHeap_dependent_specifications() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/pure_functions/heap_dependent_specifications.kt");
+      }
+
       @Test
       @TestMetadata("pure_function_rely_on_branch.kt")
       public void testPure_function_rely_on_branch() {