Introduce DFA-based Uniqueness Checking

formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Annotations.kt

@@ -11,10 +11,10 @@ annotation class AlwaysVerify
 annotation class DumpExpEmbeddings
 
 // We annotate the function to indicate that the return value is unique
-@Target(AnnotationTarget.VALUE_PARAMETER, AnnotationTarget.FUNCTION, AnnotationTarget.PROPERTY)
+@Target(AnnotationTarget.LOCAL_VARIABLE, AnnotationTarget.VALUE_PARAMETER, AnnotationTarget.FUNCTION, AnnotationTarget.PROPERTY)
 annotation class Unique
 
-@Target(AnnotationTarget.VALUE_PARAMETER)
+@Target(AnnotationTarget.LOCAL_VARIABLE, AnnotationTarget.VALUE_PARAMETER)
 annotation class Borrowed
 
 @Target(AnnotationTarget.FUNCTION)

formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/PluginAdditionalCheckers.kt

@@ -21,7 +21,7 @@ class PluginAdditionalCheckers(session: FirSession, config: PluginConfiguration)
 
     override val declarationCheckers: DeclarationCheckers = object : DeclarationCheckers() {
         override val simpleFunctionCheckers: Set<FirSimpleFunctionChecker>
-            get() = setOf(ViperPoweredDeclarationChecker(session, config), UniqueDeclarationChecker(session, config))
+            get() = setOf(ViperPoweredDeclarationChecker(session, config), UniquenessDeclarationChecker(session, config))
     }
 }
 

formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/UniqueDeclarationChecker.kt → formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/UniquenessDeclarationChecker.kt

@@ -12,29 +12,36 @@ import org.jetbrains.kotlin.fir.analysis.checkers.MppCheckerKind
 import org.jetbrains.kotlin.fir.analysis.checkers.context.CheckerContext
 import org.jetbrains.kotlin.fir.analysis.checkers.declaration.FirSimpleFunctionChecker
 import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction
+import org.jetbrains.kotlin.fir.resolve.dfa.controlFlowGraph
 import org.jetbrains.kotlin.formver.common.ErrorCollector
 import org.jetbrains.kotlin.formver.common.PluginConfiguration
-import org.jetbrains.kotlin.formver.uniqueness.UniqueCheckVisitor
-import org.jetbrains.kotlin.formver.uniqueness.UniqueChecker
 import org.jetbrains.kotlin.formver.uniqueness.UniquenessCheckException
+import org.jetbrains.kotlin.formver.uniqueness.UniquenessGraphChecker
+import org.jetbrains.kotlin.formver.uniqueness.UniquenessResolver
+import org.jetbrains.kotlin.formver.uniqueness.UniquenessTrie
+
+class UniquenessDeclarationChecker(private val session: FirSession, private val config: PluginConfiguration) :
 
-class UniqueDeclarationChecker(private val session: FirSession, private val config: PluginConfiguration) :
     FirSimpleFunctionChecker(MppCheckerKind.Common) {
 
     context(context: CheckerContext, reporter: DiagnosticReporter)
     override fun check(declaration: FirSimpleFunction) {
         if (!config.checkUniqueness) return
-        val errorCollector = ErrorCollector()
+
         try {
-            val uniqueCheckerContext = UniqueChecker(session, config, errorCollector)
-            declaration.accept(UniqueCheckVisitor, uniqueCheckerContext)
-        }
-        catch (e: UniquenessCheckException) {
+            val errorCollector = ErrorCollector()
+            val graph = declaration.controlFlowGraphReference?.controlFlowGraph
+                ?: error("Control flow graph is null for declaration: ${declaration.name}")
+            val resolver = UniquenessResolver(session)
+            val initial = UniquenessTrie(resolver)
+            val graphChecker = UniquenessGraphChecker(session, initial, errorCollector)
+            graphChecker.check(graph)
+        } catch (e: UniquenessCheckException) {
             reporter.reportOn(e.source, PluginErrors.UNIQUENESS_VIOLATION, e.message)
-        }
-        catch (e: Exception) {
+        } catch (e: Exception) {
             val error = e.message ?: "No message provided"
             reporter.reportOn(declaration.source, PluginErrors.INTERNAL_ERROR, error)
         }
     }
+
 }

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

@@ -425,51 +425,87 @@ public void testAnnotations() {
     }
 
     @Test
-    @TestMetadata("borrowing.kt")
-    public void testBorrowing() {
-      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrowing.kt");
+    @TestMetadata("assign_local.kt")
+    public void testAssign_local() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_local.kt");
     }
 
     @Test
-    @TestMetadata("consume_properties.kt")
-    public void testConsume_properties() {
-      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_properties.kt");
+    @TestMetadata("assign_property.kt")
+    public void testAssign_property() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_property.kt");
     }
 
     @Test
-    @TestMetadata("direct_pass_shared_to_unique.kt")
-    public void testDirect_pass_shared_to_unique() {
-      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/direct_pass_shared_to_unique.kt");
+    @TestMetadata("borrow_local.kt")
+    public void testBorrow_local() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_local.kt");
     }
 
     @Test
-    @TestMetadata("local_same_type.kt")
-    public void testLocal_same_type() {
-      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/local_same_type.kt");
+    @TestMetadata("borrow_property.kt")
+    public void testBorrow_property() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_property.kt");
     }
 
     @Test
-    @TestMetadata("multi_level.kt")
-    public void testMulti_level() {
-      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/multi_level.kt");
+    @TestMetadata("consume_local.kt")
+    public void testConsume_local() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_local.kt");
     }
 
     @Test
-    @TestMetadata("partial_move.kt")
-    public void testPartial_move() {
-      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partial_move.kt");
+    @TestMetadata("consume_property.kt")
+    public void testConsume_property() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_property.kt");
     }
 
     @Test
-    @TestMetadata("partially_shared.kt")
-    public void testPartially_shared() {
-      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partially_shared.kt");
+    @TestMetadata("pass_local_argument.kt")
+    public void testPass_local_argument() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_local_argument.kt");
     }
 
     @Test
-    @TestMetadata("shared_to_shared.kt")
-    public void testShared_to_shared() {
-      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/shared_to_shared.kt");
+    @TestMetadata("pass_property_argument.kt")
+    public void testPass_property_argument() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_property_argument.kt");
+    }
+
+    @Test
+    @TestMetadata("return_local.kt")
+    public void testReturn_local() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_local.kt");
+    }
+
+    @Test
+    @TestMetadata("return_property.kt")
+    public void testReturn_property() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_property.kt");
+    }
+
+    @Test
+    @TestMetadata("share_local.kt")
+    public void testShare_local() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_local.kt");
+    }
+
+    @Test
+    @TestMetadata("share_properties.kt")
+    public void testShare_properties() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_properties.kt");
+    }
+
+    @Test
+    @TestMetadata("throw_local.kt")
+    public void testThrow_local() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_local.kt");
+    }
+
+    @Test
+    @TestMetadata("throw_property.kt")
+    public void testThrow_property() {
+      runTest("formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_property.kt");
     }
   }
 

formver.compiler-plugin/testData/diagnostics/uniqueness_checker/annotations.kt

@@ -1,11 +1,13 @@
 // UNIQUE_CHECK_ONLY
 
-import org.jetbrains.kotlin.formver.plugin.Unique
 import org.jetbrains.kotlin.formver.plugin.Borrowed
+import org.jetbrains.kotlin.formver.plugin.Unique
 
 class Box(@Unique val a: Any)
 
-fun f_unique(@Unique box: Box) {}
-fun f_borrowed(@Borrowed box: Box) {}
-fun f_unique_borrowed(@Unique @Borrowed box: Box) {}
+fun `unique parameter`(@Unique box: Box) {}
+
+fun `borrowed parameter`(@Borrowed box: Box) {}
+
+fun `unique borrowed parameter`(@Unique @Borrowed box: Box) {}
 

formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_local.fir.diag.txt

@@ -0,0 +1,25 @@
+/assign_local.kt:(290,291): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared global'.
+
+/assign_local.kt:(387,388): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared local'.
+
+/assign_local.kt:(598,599): error: Argument uniqueness mismatch: expected 'unique global', actual 'unique local'.
+
+/assign_local.kt:(697,698): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared global'.
+
+/assign_local.kt:(797,798): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared local'.
+
+/assign_local.kt:(991,992): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared global'.
+
+/assign_local.kt:(1115,1116): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared local'.
+
+/assign_local.kt:(1254,1255): error: Argument uniqueness mismatch: expected 'unique global', actual 'unique local'.
+
+/assign_local.kt:(1389,1390): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared global'.
+
+/assign_local.kt:(1532,1533): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared local'.
+
+/assign_local.kt:(1841,1842): error: Argument uniqueness mismatch: expected 'unique global', actual 'unique local'.
+
+/assign_local.kt:(2028,2029): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared global'.
+
+/assign_local.kt:(2194,2195): error: Assignment uniqueness mismatch: expected 'unique global', actual 'moved'.

formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_local.kt

@@ -0,0 +1,150 @@
+// UNIQUE_CHECK_ONLY
+
+import org.jetbrains.kotlin.formver.plugin.Borrowed
+import org.jetbrains.kotlin.formver.plugin.Unique
+
+fun nondet(): Boolean {
+    return false
+}
+
+fun consume(@Unique x: Any) {}
+
+// Var assignments
+
+fun `assign shared`(x: Any) {
+    var y: Any
+
+    y = x
+
+    consume(<!UNIQUENESS_VIOLATION!>y<!>)
+}
+
+fun `assign borrowed`(@Borrowed x: Any) {
+    @Borrowed var y: Any
+
+    y = x
+
+    consume(<!UNIQUENESS_VIOLATION!>y<!>)
+}
+
+fun `assign unique`(@Unique x: Any) {
+    @Unique var y: Any
+
+    y = x
+
+    consume(y)
+}
+
+fun `assign unique-borrowed`(@Unique @Borrowed x: Any) {
+    @Unique @Borrowed var y: Any
+
+    y = x
+
+    consume(<!UNIQUENESS_VIOLATION!>y<!>)
+}
+
+// Var declarations
+
+fun `assign shared in declaration`(x: Any) {
+    var y = x
+
+    consume(<!UNIQUENESS_VIOLATION!>y<!>)
+}
+
+fun `assign borrowed in declaration`(@Borrowed x: Any) {
+    @Borrowed var y = x
+
+    consume(<!UNIQUENESS_VIOLATION!>y<!>)
+}
+
+fun `assign unique in unique declaration`(@Unique x: Any) {
+    @Unique var y = x
+
+    consume(y)
+}
+
+fun `assign unique in shared declaration`(@Unique x: Any) {
+    var y = x
+
+    consume(<!UNIQUENESS_VIOLATION!>y<!>)
+}
+
+fun `assign unique-borrowed in borrowed declaration`(@Unique @Borrowed x: Any) {
+    @Borrowed var y = x
+
+    consume(<!UNIQUENESS_VIOLATION!>y<!>)
+}
+
+fun `assign unique-borrowed in unique-borrowed declaration`(@Unique @Borrowed x: Any) {
+    @Unique @Borrowed var y = x
+
+    consume(<!UNIQUENESS_VIOLATION!>y<!>)
+}
+
+// Assignment chaining
+
+fun `chain shared assignments`(x: Any) {
+    var y: Any
+    var z: Any
+
+    y = x
+    z = y
+
+    consume(<!UNIQUENESS_VIOLATION!>z<!>)
+}
+
+fun `chain borrowed assignments`(@Borrowed x: Any) {
+    @Borrowed var y: Any
+    @Borrowed var z: Any
+
+    y = x
+    z = y
+
+    consume(<!UNIQUENESS_VIOLATION!>z<!>)
+}
+
+fun `chain unique assignments`(@Unique x: Any) {
+    @Unique var y: Any
+    @Unique var z: Any
+
+    y = x
+    z = y
+
+    consume(z)
+}
+
+fun `chain unique-borrowed assignments`(@Unique @Borrowed x: Any) {
+    @Unique @Borrowed var y: Any
+    @Unique @Borrowed var z: Any
+
+    y = x
+    z = y
+
+    consume(<!UNIQUENESS_VIOLATION!>z<!>)
+}
+
+// Conditional assignments
+
+fun `assign unique or shared`(@Unique x: Any, y: Any) {
+    var z: Any;
+
+    if (nondet()) {
+        z = x
+    } else {
+        z = y
+    }
+
+    consume(<!UNIQUENESS_VIOLATION!>z<!>)
+}
+
+// Looping assignments
+
+fun `assign unique to shared in loop`(@Unique x: Any, @Unique y: Any) {
+    @Unique var z: Any = y;
+
+    while (nondet()) {
+        z = <!UNIQUENESS_VIOLATION!>x<!>
+    }
+
+    consume(z)
+}

formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_property.fir.diag.txt

@@ -0,0 +1,5 @@
+/assign_property.kt:(409,410): error: Assignment uniqueness mismatch: expected 'unique global', actual 'shared global'.
+
+/assign_property.kt:(506,507): error: Assignment uniqueness mismatch: expected 'unique global', actual 'shared local'.
+
+/assign_property.kt:(727,728): error: Assignment uniqueness mismatch: expected 'unique global', actual 'unique local'.