[claude-experiments] Add subtyping verification test probes

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

@@ -808,6 +808,76 @@ public void testStrings() {
       }
     }
 
+    @Nested
+    @TestMetadata("formver.compiler-plugin/testData/diagnostics/verification/subtyping")
+    @TestDataPath("$PROJECT_ROOT")
+    public class Subtyping {
+      @Test
+      @TestMetadata("abstract_class.kt")
+      public void testAbstract_class() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/abstract_class.kt");
+      }
+
+      @Test
+      public void testAllFilesPresentInSubtyping() {
+        KtTestUtil.assertAllTestsPresentByMetadataWithExcluded(this.getClass(), new File("formver.compiler-plugin/testData/diagnostics/verification/subtyping"), Pattern.compile("^(.+)\\.kt$"), null, true);
+      }
+
+      @Test
+      @TestMetadata("cast_verification.kt")
+      public void testCast_verification() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/cast_verification.kt");
+      }
+
+      @Test
+      @TestMetadata("class_hierarchy_basics.kt")
+      public void testClass_hierarchy_basics() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/class_hierarchy_basics.kt");
+      }
+
+      @Test
+      @TestMetadata("interface_verification.kt")
+      public void testInterface_verification() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/interface_verification.kt");
+      }
+
+      @Test
+      @TestMetadata("override_methods.kt")
+      public void testOverride_methods() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/override_methods.kt");
+      }
+
+      @Test
+      @TestMetadata("permissions_cast.kt")
+      public void testPermissions_cast() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/permissions_cast.kt");
+      }
+
+      @Test
+      @TestMetadata("permissions_double_predicate.kt")
+      public void testPermissions_double_predicate() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/permissions_double_predicate.kt");
+      }
+
+      @Test
+      @TestMetadata("permissions_unique.kt")
+      public void testPermissions_unique() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/permissions_unique.kt");
+      }
+
+      @Test
+      @TestMetadata("permissions_unique_subtype.kt")
+      public void testPermissions_unique_subtype() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/permissions_unique_subtype.kt");
+      }
+
+      @Test
+      @TestMetadata("smart_cast_class.kt")
+      public void testSmart_cast_class() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/subtyping/smart_cast_class.kt");
+      }
+    }
+
     @Nested
     @TestMetadata("formver.compiler-plugin/testData/diagnostics/verification/uniqueness")
     @TestDataPath("$PROJECT_ROOT")

formver.compiler-plugin/testData/diagnostics/verification/subtyping/abstract_class.fir.diag.txt

@@ -0,0 +1,27 @@
+/abstract_class.kt:(316,328): info: Generated Viper text for carIsVehicle:
+field bf$wheels: Ref
+
+method f$carIsVehicle$TF$T$Car$T$Boolean(p$c: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == true
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$c), df$rt$c$Car())
+  inhale acc(p$c$Car$shared(p$c), wildcard)
+  ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$c), df$rt$c$Vehicle()))
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/abstract_class.kt:(468,477): info: Generated Viper text for getWheels:
+field bf$wheels: Ref
+
+method f$getWheels$TF$T$Vehicle$T$Int(p$v: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$v), df$rt$c$Vehicle())
+  inhale acc(p$c$Vehicle$shared(p$v), wildcard)
+  unfold acc(p$c$Vehicle$shared(p$v), wildcard)
+  ret$0 := p$v.bf$wheels
+  goto lbl$ret$0
+  label lbl$ret$0
+}

formver.compiler-plugin/testData/diagnostics/verification/subtyping/abstract_class.kt

@@ -0,0 +1,24 @@
+@file:Suppress("USELESS_IS_CHECK")
+
+// ALWAYS_VALIDATE
+// Probe: abstract class subtyping verification
+
+import kotlin.contracts.ExperimentalContracts
+import kotlin.contracts.contract
+
+abstract class Vehicle(val wheels: Int)
+class Car : Vehicle(4)
+class Bicycle : Vehicle(2)
+
+@OptIn(ExperimentalContracts::class)
+fun <!VIPER_TEXT!>carIsVehicle<!>(c: Car): Boolean {
+    contract {
+        returns(true)
+    }
+    return c is Vehicle
+}
+
+// Access inherited field from abstract class
+fun <!VIPER_TEXT!>getWheels<!>(v: Vehicle): Int {
+    return v.wheels
+}

formver.compiler-plugin/testData/diagnostics/verification/subtyping/cast_verification.fir.diag.txt

@@ -0,0 +1,47 @@
+/cast_verification.kt:(303,325): info: Generated Viper text for safeCastPreservesValue:
+field bf$x: Ref
+
+field bf$y: Ref
+
+method f$safeCastPreservesValue$TF$T$Base$T$Int(p$b: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+{
+  var l0$d: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$c$Base())
+  inhale acc(p$c$Base$shared(p$b), wildcard)
+  if (df$rt$isSubtype(df$rt$typeOf(p$b), df$rt$c$Derived())) {
+    l0$d := p$b
+  } else {
+    l0$d := df$rt$nullValue()}
+  inhale df$rt$isSubtype(df$rt$typeOf(l0$d), df$rt$nullable(df$rt$c$Derived()))
+  inhale l0$d != df$rt$nullValue() ==>
+    acc(p$c$Derived$shared(l0$d), wildcard)
+  if (!(l0$d == df$rt$nullValue())) {
+    unfold acc(p$c$Derived$shared(l0$d), wildcard)
+    unfold acc(p$c$Base$shared(l0$d), wildcard)
+    ret$0 := l0$d.bf$x
+  } else {
+    unfold acc(p$c$Base$shared(p$b), wildcard)
+    ret$0 := p$b.bf$x
+  }
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/cast_verification.kt:(507,527): info: Generated Viper text for upcastAlwaysSucceeds:
+field bf$x: Ref
+
+field bf$y: Ref
+
+method f$upcastAlwaysSucceeds$TF$T$Derived$T$Boolean(p$d: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == true
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$d), df$rt$c$Derived())
+  inhale acc(p$c$Derived$shared(p$d), wildcard)
+  ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$d), df$rt$c$Base()))
+  goto lbl$ret$0
+  label lbl$ret$0
+}

formver.compiler-plugin/testData/diagnostics/verification/subtyping/cast_verification.kt

@@ -0,0 +1,25 @@
+@file:Suppress("USELESS_IS_CHECK")
+
+// ALWAYS_VALIDATE
+// Probe: cast operators in verification context
+
+import kotlin.contracts.ExperimentalContracts
+import kotlin.contracts.contract
+
+open class Base(val x: Int)
+class Derived(x: Int, val y: Int) : Base(x)
+
+// Safe cast returns null for wrong type
+fun <!VIPER_TEXT!>safeCastPreservesValue<!>(b: Base): Int {
+    val d = b as? Derived
+    return if (d != null) d.x else b.x
+}
+
+// Upcast should always succeed: verify Derived is Base
+@OptIn(ExperimentalContracts::class)
+fun <!VIPER_TEXT!>upcastAlwaysSucceeds<!>(d: Derived): Boolean {
+    contract {
+        returns(true)
+    }
+    return d is Base
+}

formver.compiler-plugin/testData/diagnostics/verification/subtyping/class_hierarchy_basics.fir.diag.txt

@@ -0,0 +1,45 @@
+/class_hierarchy_basics.kt:(180,191): info: Generated Viper text for takesAnimal:
+field bf$legs: Ref
+
+method f$takesAnimal$TF$T$Animal$T$Int(p$a: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$a), df$rt$c$Animal())
+  inhale acc(p$c$Animal$shared(p$a), wildcard)
+  unfold acc(p$c$Animal$shared(p$a), wildcard)
+  ret$0 := p$a.bf$legs
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/class_hierarchy_basics.kt:(222,237): info: Generated Viper text for passDogAsAnimal:
+field bf$legs: Ref
+
+method f$passDogAsAnimal$TF$T$Dog$T$Int(p$d: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$d), df$rt$c$Dog())
+  inhale acc(p$c$Dog$shared(p$d), wildcard)
+  ret$0 := f$takesAnimal$TF$T$Animal$T$Int(p$d)
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+method f$takesAnimal$TF$T$Animal$T$Int(p$a: Ref) returns (ret: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$intType())
+
+
+/class_hierarchy_basics.kt:(337,344): info: Generated Viper text for dogLegs:
+field bf$legs: Ref
+
+method f$dogLegs$TF$T$Dog$T$Int(p$d: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$d), df$rt$c$Dog())
+  inhale acc(p$c$Dog$shared(p$d), wildcard)
+  unfold acc(p$c$Dog$shared(p$d), wildcard)
+  unfold acc(p$c$Animal$shared(p$d), wildcard)
+  ret$0 := p$d.bf$legs
+  goto lbl$ret$0
+  label lbl$ret$0
+}

formver.compiler-plugin/testData/diagnostics/verification/subtyping/class_hierarchy_basics.kt

@@ -0,0 +1,17 @@
+// ALWAYS_VALIDATE
+// Probe: basic class hierarchy verification
+
+open class Animal(val legs: Int)
+class Dog(legs: Int) : Animal(legs)
+
+// Subtype passed to supertype parameter
+fun <!VIPER_TEXT!>takesAnimal<!>(a: Animal): Int = a.legs
+
+fun <!VIPER_TEXT!>passDogAsAnimal<!>(d: Dog): Int {
+    return takesAnimal(d)
+}
+
+// Field access on subtype returns inherited field
+fun <!VIPER_TEXT!>dogLegs<!>(d: Dog): Int {
+    return d.legs
+}

formver.compiler-plugin/testData/diagnostics/verification/subtyping/interface_verification.fir.diag.txt

@@ -0,0 +1,43 @@
+/interface_verification.kt:(422,435): info: Generated Viper text for getPersonName:
+field bf$age: Ref
+
+field bf$name: Ref
+
+method f$getPersonName$TF$T$Person$T$String(p$p: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$stringType())
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$p), df$rt$c$Person())
+  inhale acc(p$c$Person$shared(p$p), wildcard)
+  unfold acc(p$c$Person$shared(p$p), wildcard)
+  ret$0 := p$p.bf$name
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+method pg$public$age(this$dispatch: Ref) returns (ret: Ref)
+
+
+method pg$public$name(this$dispatch: Ref) returns (ret: Ref)
+
+
+/interface_verification.kt:(569,584): info: Generated Viper text for personIsHasName:
+field bf$age: Ref
+
+field bf$name: Ref
+
+method f$personIsHasName$TF$T$Person$T$Boolean(p$p: Ref)
+  returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == true
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$p), df$rt$c$Person())
+  inhale acc(p$c$Person$shared(p$p), wildcard)
+  ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$p), df$rt$c$HasName()))
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+method pg$public$age(this$dispatch: Ref) returns (ret: Ref)
+
+
+method pg$public$name(this$dispatch: Ref) returns (ret: Ref)

formver.compiler-plugin/testData/diagnostics/verification/subtyping/interface_verification.kt

@@ -0,0 +1,31 @@
+@file:Suppress("USELESS_IS_CHECK")
+
+// ALWAYS_VALIDATE
+// Probe: interface-based subtyping verification
+
+import kotlin.contracts.ExperimentalContracts
+import kotlin.contracts.contract
+
+interface HasName {
+    val name: String
+}
+
+interface HasAge {
+    val age: Int
+}
+
+class Person(override val name: String, override val age: Int) : HasName, HasAge
+
+// Verify accessing interface properties through implementing class
+fun <!VIPER_TEXT!>getPersonName<!>(p: Person): String {
+    return p.name
+}
+
+// Verify subtype relationship: Person is HasName
+@OptIn(ExperimentalContracts::class)
+fun <!VIPER_TEXT!>personIsHasName<!>(p: Person): Boolean {
+    contract {
+        returns(true)
+    }
+    return p is HasName
+}