diff --git a/formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Annotations.kt b/formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Annotations.kt index 9e106ef7..eaa6e73a 100644 --- a/formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Annotations.kt +++ b/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) diff --git a/formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/PluginAdditionalCheckers.kt b/formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/PluginAdditionalCheckers.kt index 23325c99..b9b56c63 100644 --- a/formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/PluginAdditionalCheckers.kt +++ b/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 - get() = setOf(ViperPoweredDeclarationChecker(session, config), UniqueDeclarationChecker(session, config)) + get() = setOf(ViperPoweredDeclarationChecker(session, config), UniquenessDeclarationChecker(session, config)) } } diff --git a/formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/UniqueDeclarationChecker.kt b/formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/UniquenessDeclarationChecker.kt similarity index 60% rename from formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/UniqueDeclarationChecker.kt rename to formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/UniquenessDeclarationChecker.kt index d91b4506..8df515de 100644 --- a/formver.compiler-plugin/plugin/src/org/jetbrains/kotlin/formver/plugin/compiler/UniqueDeclarationChecker.kt +++ b/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) } } + } \ No newline at end of file diff --git a/formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java b/formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java index 1e9080a7..861098ca 100644 --- a/formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java +++ b/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"); } } diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/annotations.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/annotations.kt index 405b42d2..89c8616b 100644 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/annotations.kt +++ b/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) {} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_local.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_local.fir.diag.txt new file mode 100644 index 00000000..328a2bbf --- /dev/null +++ b/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'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_local.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_local.kt new file mode 100644 index 00000000..f641df80 --- /dev/null +++ b/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(y) +} + +fun `assign borrowed`(@Borrowed x: Any) { + @Borrowed var y: Any + + y = x + + consume(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(y) +} + +// Var declarations + +fun `assign shared in declaration`(x: Any) { + var y = x + + consume(y) +} + +fun `assign borrowed in declaration`(@Borrowed x: Any) { + @Borrowed var y = x + + consume(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(y) +} + +fun `assign unique-borrowed in borrowed declaration`(@Unique @Borrowed x: Any) { + @Borrowed var y = x + + consume(y) +} + +fun `assign unique-borrowed in unique-borrowed declaration`(@Unique @Borrowed x: Any) { + @Unique @Borrowed var y = x + + consume(y) +} + +// Assignment chaining + +fun `chain shared assignments`(x: Any) { + var y: Any + var z: Any + + y = x + z = y + + consume(z) +} + +fun `chain borrowed assignments`(@Borrowed x: Any) { + @Borrowed var y: Any + @Borrowed var z: Any + + y = x + z = y + + consume(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(z) +} + +// Conditional assignments + +fun `assign unique or shared`(@Unique x: Any, y: Any) { + var z: Any; + + if (nondet()) { + z = x + } else { + z = y + } + + consume(z) +} + +// Looping assignments + +fun `assign unique to shared in loop`(@Unique x: Any, @Unique y: Any) { + @Unique var z: Any = y; + + while (nondet()) { + z = x + } + + consume(z) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_property.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_property.fir.diag.txt new file mode 100644 index 00000000..c453fad9 --- /dev/null +++ b/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'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_property.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_property.kt new file mode 100644 index 00000000..574be671 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/assign_property.kt @@ -0,0 +1,39 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A { + @Unique var x = Object() + @Unique var w = Object() +} + +class B { + @Unique var y = A() +} + +fun borrow(@Unique @Borrowed x: A) {} + +fun consume(@Unique a: Any) {} + +// Property assignments + +fun `assign shared to unique subproperty`(@Unique x: B, v: A): Unit { + x.y = v +} + +fun `assign borrowed to unique subproperty`(@Unique x: B, @Borrowed v: A): Unit { + x.y = v +} + +fun `assign unique to unique subproperty`(@Unique x: B, @Unique v: A): Unit { + x.y = v + + consume(x) +} + +fun `assign unique-borrowed to unique subproperty`(@Unique x: B, @Unique @Borrowed v: A): Unit { + x.y = v + + consume(x) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_local.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_local.fir.diag.txt new file mode 100644 index 00000000..0e631373 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_local.fir.diag.txt @@ -0,0 +1 @@ +/borrow_local.kt:(585,586): error: Argument uniqueness mismatch: expected 'shared local', actual 'moved'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_local.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_local.kt new file mode 100644 index 00000000..eaa28a8e --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_local.kt @@ -0,0 +1,49 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A() + +fun borrow(@Borrowed y: Any) {} + +fun consume(@Unique y: Any) {} + +fun share(y: Any) {} + +// Borrowing locals + +fun `borrow shared`(z: A) { + borrow(z) +} + +fun `borrow borrowed`(@Borrowed z: A) { + borrow(z) +} + +fun `borrow unique`(@Unique z: A) { + borrow(z) +} + +fun `borrow unique-borrowed`(@Borrowed @Unique z: A) { + borrow(z) +} + +// Borrowing local after consuming + +fun `borrow after consuming unique`(@Unique a: A) { + consume(a) + borrow(a) +} + +// Borrowing local after sharing + +fun `borrow after sharing shared`(a: A) { + share(a) + borrow(a) +} + +fun `borrow after sharing unique`(@Unique a: A) { + share(a) + borrow(a) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_property.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_property.fir.diag.txt new file mode 100644 index 00000000..1e3e0130 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_property.fir.diag.txt @@ -0,0 +1,3 @@ +/borrow_property.kt:(853,854): error: Argument uniqueness mismatch: partial type 'moved' is inconsistent with parent type 'unique global'. + +/borrow_property.kt:(931,932): error: Argument uniqueness mismatch: partial type 'shared global' is inconsistent with parent type 'unique global'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_property.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_property.kt new file mode 100644 index 00000000..ce55055b --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrow_property.kt @@ -0,0 +1,67 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A { + @Unique var x = Object() + @Unique var w = Object() +} + +class B { + @Unique var y = A() +} + +fun borrow(@Borrowed y: Any) {} + +fun consume(@Unique y: Any) {} + +fun share(a: Any) {} + +// Borrowing subproperties + +fun `borrow shared subproperty`(z: B) { + borrow(z.y) +} + +fun `borrow borrowed subproperty`(@Borrowed z: B) { + borrow(z.y) +} + +fun `borrow unique subproperty`(@Unique z: B) { + borrow(z.y) +} + +fun `borrow unique-borrowed subproperty`(@Borrowed @Unique z: B) { + borrow(z.y) +} + +fun `borrow multiple unique subproperties`(@Unique z: B) { + borrow(z.y.x) + borrow(z.y.w) +} + +// Borrowing partially-inconsistent subproperties + +fun `borrow partially moved`(@Unique z: B) { + consume(z.y) + borrow(z) +} + +fun `borrow partially shared`(@Unique z: B) { + share(z.y) + borrow(z) +} + +// Borrowing after assignment + +fun `borrow unique parent after assigning subproperty to unique`(@Unique x: B, @Unique v: A) { + x.y = v + borrow(x) +} + +fun `borrow unique parent twice after assigning subproperty to unique`(@Unique @Borrowed x: B, @Unique v: A) { + x.y = v + borrow(x) + borrow(x) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrowing.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrowing.fir.diag.txt deleted file mode 100644 index 4969038c..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrowing.fir.diag.txt +++ /dev/null @@ -1,3 +0,0 @@ -/borrowing.kt:(700,701): error: cannot pass borrowed value as non-borrowed - -/borrowing.kt:(783,784): error: cannot pass borrowed value as non-borrowed diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrowing.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrowing.kt deleted file mode 100644 index 6234078c..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/borrowing.kt +++ /dev/null @@ -1,40 +0,0 @@ -// UNIQUE_CHECK_ONLY - -import org.jetbrains.kotlin.formver.plugin.NeverConvert -import org.jetbrains.kotlin.formver.plugin.NeverVerify -import org.jetbrains.kotlin.formver.plugin.Unique -import org.jetbrains.kotlin.formver.plugin.Borrowed - -class A { - @Unique val x = 1 - @Unique val w = 2 -} - -class B { - @Unique val y = A() -} - -fun consumeInt(@Unique a: Int) {} -fun consumeA(@Unique a: A) {} -fun consumeB(@Unique a: B) {} - -fun makeIntoShared(a: A) {} - -fun sharedBorrowingA(@Borrowed y: A) {} - -fun borrowingB(@Borrowed @Unique z: B) { - sharedBorrowingA(z.y) -} - -fun valid_borrow(@Unique z: B) { - borrowingB(z) - consumeB(z) -} - -fun borrowedToNonBorrowed(@Borrowed @Unique z: B) { - consumeB(z) -} - -fun borrowedToNonBorrowedShared(@Borrowed @Unique y: A) { - makeIntoShared(y) -} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_local.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_local.fir.diag.txt new file mode 100644 index 00000000..16848d65 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_local.fir.diag.txt @@ -0,0 +1,13 @@ +/consume_local.kt:(309,310): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared global'. + +/consume_local.kt:(368,369): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared local'. + +/consume_local.kt:(497,498): error: Argument uniqueness mismatch: expected 'unique global', actual 'unique local'. + +/consume_local.kt:(613,614): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared global'. + +/consume_local.kt:(705,706): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared local'. + +/consume_local.kt:(996,997): error: Argument uniqueness mismatch: expected 'unique global', actual 'unique local'. + +/consume_local.kt:(1122,1123): error: Argument uniqueness mismatch: expected 'unique global', actual 'unique local'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_local.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_local.kt new file mode 100644 index 00000000..c77828e0 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_local.kt @@ -0,0 +1,62 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A() + +fun consume(@Unique a: Any) {} + +fun borrow(@Borrowed a: Any) {} + +fun borrowUnique(@Borrowed @Unique a: Any) {} + +// Consuming local + +fun `consume shared`(a: A) { + consume(a) +} + +fun `consume borrowed`(@Borrowed a: A) { + consume(a) +} + +fun `consume unique`(@Unique a: A) { + consume(a) +} + +fun `consume unique-borrowed`(@Unique @Borrowed a: A) { + consume(a) +} + +// Consuming local after borrowing + +fun `consume shared after borrowing it`(a: A) { + borrow(a) + consume(a) +} + +fun `consume borrowed after borrowing it`(@Borrowed a: A) { + borrow(a) + consume(a) +} + +fun `consume after borrowing unique`(@Unique a: A) { + borrow(a) + consume(a) +} + +fun `consume after borrowing unique as unique`(@Unique a: A) { + borrowUnique(a) + consume(a) +} + +fun `consume after borrowing unique-borrowed `(@Unique @Borrowed a: A) { + borrow(a) + consume(a) +} + +fun `consume after after borrowing unique-borrowed as unique`(@Unique @Borrowed a: A) { + borrowUnique(a) + consume(a) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_properties.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_properties.fir.diag.txt deleted file mode 100644 index 22705ef5..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_properties.fir.diag.txt +++ /dev/null @@ -1,5 +0,0 @@ -/consume_properties.kt:(550,551): error: cannot access expression as its uniqueness state is top - -/consume_properties.kt:(623,628): error: cannot access expression as its uniqueness state is top - -/consume_properties.kt:(709,712): error: expected unique value, got shared diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_properties.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_properties.kt deleted file mode 100644 index f685dcd5..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_properties.kt +++ /dev/null @@ -1,45 +0,0 @@ -// UNIQUE_CHECK_ONLY - -import org.jetbrains.kotlin.formver.plugin.NeverConvert -import org.jetbrains.kotlin.formver.plugin.NeverVerify -import org.jetbrains.kotlin.formver.plugin.Unique - -class A { - @Unique val x = 1 - @Unique val w = 2 -} - -class B { - @Unique val y = A() -} - -fun consumeInt(@Unique a: Int) {} -fun consumeA(@Unique a: A) {} -fun consumeB(@Unique a: B) {} - -fun makeIntoShared(a: A) {} - -fun valid_consume_all(@Unique z: B) { - consumeInt(z.y.x) - consumeInt(z.y.w) -} - -fun doubleConsume(@Unique a: A) { - consumeA(a) - consumeA(a) -} - -fun consumeParent(@Unique z: B) { - consumeA(z.y) - consumeInt(z.y.x) -} - -fun uniqueBecomeShared(@Unique z: B) { - makeIntoShared(z.y) - consumeA(z.y) -} - -fun uniqueBecomeSharedValid(@Unique z: B) { - makeIntoShared(z.y) - makeIntoShared(z.y) -} \ No newline at end of file diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_property.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_property.fir.diag.txt new file mode 100644 index 00000000..1288315e --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_property.fir.diag.txt @@ -0,0 +1,9 @@ +/consume_property.kt:(368,373): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared global'. + +/consume_property.kt:(443,448): error: Argument uniqueness mismatch: expected 'unique global', actual 'shared local'. + +/consume_property.kt:(604,609): error: Argument uniqueness mismatch: expected 'unique global', actual 'unique local'. + +/consume_property.kt:(841,842): error: Argument uniqueness mismatch: partial type 'moved' is inconsistent with parent type 'unique global'. + +/consume_property.kt:(921,922): error: Argument uniqueness mismatch: partial type 'shared global' is inconsistent with parent type 'unique global'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_property.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_property.kt new file mode 100644 index 00000000..37428e19 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/consume_property.kt @@ -0,0 +1,59 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A { + @Unique var x = Object() + @Unique var w = Object() +} + +class B { + @Unique var y = A() +} + +fun consume(@Unique a: Any) {} + +fun share(a: Any) {} + +// Consuming subproperties + +fun `consume shared subproperty`(z: B) { + consume(z.y.x) +} + +fun `consume borrowed subproperty`(@Borrowed z: B) { + consume(z.y.x) +} + +fun `consume unique subproperty`(@Unique z: B) { + consume(z.y.x) +} + +fun `consume unique-borrowed subproperty`(@Borrowed @Unique z: B) { + consume(z.y.x) +} + +fun `consume multiple unique subproperties`(@Unique z: B) { + consume(z.y.x) + consume(z.y.w) +} + +// Consuming partially-inconsistent subproperties + +fun `consume partially moved`(@Unique z: B) { + consume(z.y) + consume(z) +} + +fun `consume partially shared`(@Unique z: B) { + share(z.y) + consume(z) +} + +// Consuming subproperty after assignment + +fun `consume unique parent after assigning subproperty to unique`(@Unique x: B, @Unique y: A) { + x.y = y + consume(x.y) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/direct_pass_shared_to_unique.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/direct_pass_shared_to_unique.fir.diag.txt deleted file mode 100644 index 8e200d53..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/direct_pass_shared_to_unique.fir.diag.txt +++ /dev/null @@ -1 +0,0 @@ -/direct_pass_shared_to_unique.kt:(238,239): error: expected unique value, got shared diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/direct_pass_shared_to_unique.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/direct_pass_shared_to_unique.kt deleted file mode 100644 index 87f3b9d8..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/direct_pass_shared_to_unique.kt +++ /dev/null @@ -1,13 +0,0 @@ -// UNIQUE_CHECK_ONLY - -import org.jetbrains.kotlin.formver.plugin.NeverConvert -import org.jetbrains.kotlin.formver.plugin.NeverVerify -import org.jetbrains.kotlin.formver.plugin.Unique - -fun f(@Unique x: Int) { - -} - -fun use_f(y: Int) { - f(y) -} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/local_same_type.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/local_same_type.kt deleted file mode 100644 index 9c4fc74b..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/local_same_type.kt +++ /dev/null @@ -1,21 +0,0 @@ -// UNIQUE_CHECK_ONLY - -import org.jetbrains.kotlin.formver.plugin.NeverConvert -import org.jetbrains.kotlin.formver.plugin.NeverVerify -import org.jetbrains.kotlin.formver.plugin.Unique - -class A { - @Unique val x = 1 -} - -fun consumeInt(@Unique x: Int) {} - -fun moveSameTypedLocals(@Unique x: Int, @Unique y: Int) { - consumeInt(x) - consumeInt(y) -} - -fun moveSameTypedLocalMembers(@Unique x: A, @Unique y: A) { - consumeInt(x.x) - consumeInt(y.x) -} \ No newline at end of file diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/multi_level.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/multi_level.fir.diag.txt deleted file mode 100644 index e5279fff..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/multi_level.fir.diag.txt +++ /dev/null @@ -1 +0,0 @@ -/multi_level.kt:(393,398): error: expected unique value, got shared diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/multi_level.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/multi_level.kt deleted file mode 100644 index 8506ba62..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/multi_level.kt +++ /dev/null @@ -1,31 +0,0 @@ -// UNIQUE_CHECK_ONLY - -import org.jetbrains.kotlin.formver.plugin.NeverConvert -import org.jetbrains.kotlin.formver.plugin.NeverVerify -import org.jetbrains.kotlin.formver.plugin.Unique - -class A { - @Unique val x = 1 -} - -class B { - val y = A() -} - -@Unique val Int.f get() = 3 - -fun f(@Unique z: B) { - z.y.x -} - -fun g() { - 3.f -} - -fun g(@Unique x: Int) { - -} - -fun use_g(@Unique z: B) { - g(z.y.x) -} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partial_move.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partial_move.fir.diag.txt deleted file mode 100644 index f9d74b86..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partial_move.fir.diag.txt +++ /dev/null @@ -1 +0,0 @@ -/partial_move.kt:(340,341): error: a partially moved object cannot be passed as an argument diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partial_move.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partial_move.kt deleted file mode 100644 index 42bc6ced..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partial_move.kt +++ /dev/null @@ -1,20 +0,0 @@ -// UNIQUE_CHECK_ONLY - -import org.jetbrains.kotlin.formver.plugin.NeverConvert -import org.jetbrains.kotlin.formver.plugin.NeverVerify -import org.jetbrains.kotlin.formver.plugin.Unique - -class B - -class A( - @Unique val data: B, -) - -fun takesA(@Unique a: A) {} -fun dropB(@Unique b: B) {} - -fun test(@Unique a: A) { - dropB(a.data) - takesA(a) -} - diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partially_shared.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partially_shared.fir.diag.txt deleted file mode 100644 index 3c089ede..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partially_shared.fir.diag.txt +++ /dev/null @@ -1 +0,0 @@ -/partially_shared.kt:(338,339): error: cannot pass a partially shared argument diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partially_shared.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partially_shared.kt deleted file mode 100644 index 71e9705e..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/partially_shared.kt +++ /dev/null @@ -1,20 +0,0 @@ -// UNIQUE_CHECK_ONLY - -import org.jetbrains.kotlin.formver.plugin.NeverConvert -import org.jetbrains.kotlin.formver.plugin.NeverVerify -import org.jetbrains.kotlin.formver.plugin.Unique - -class B - -class A( - @Unique val data: B, -) - -fun consumeA(@Unique a: A) {} -fun shareB(b: B) {} - -fun test(@Unique a: A) { - shareB(a.data) - consumeA(a) -} - diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_local_argument.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_local_argument.fir.diag.txt new file mode 100644 index 00000000..bc97658b --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_local_argument.fir.diag.txt @@ -0,0 +1 @@ +/pass_local_argument.kt:(496,497): error: Argument uniqueness mismatch: expected 'unique global', actual 'moved'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_local_argument.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_local_argument.kt new file mode 100644 index 00000000..c5de2051 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_local_argument.kt @@ -0,0 +1,22 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +fun borrowBoth(@Borrowed a: Any, @Borrowed b: Any) {} + +fun consumeBoth(@Unique a: Any, @Unique b: Any) {} + +fun shareBoth(a: Any, b: Any) {} + +fun `pass shared twice to shareBoth`(a: Any) { + shareBoth(a, a) +} + +fun `pass borrowed twice to borrowBoth`(@Borrowed a: Any) { + borrowBoth(a, a) +} + +fun `pass unique twice to consumeBoth`(@Unique a: Any) { + consumeBoth(a, a) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_property_argument.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_property_argument.fir.diag.txt new file mode 100644 index 00000000..67895d1d --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_property_argument.fir.diag.txt @@ -0,0 +1 @@ +/pass_property_argument.kt:(655,656): error: Argument uniqueness mismatch: partial type 'moved' is inconsistent with parent type 'unique global'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_property_argument.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_property_argument.kt new file mode 100644 index 00000000..ea2e1123 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/pass_property_argument.kt @@ -0,0 +1,35 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A { + @Unique var x = Object() + @Unique var w = Object() +} + +class B { + @Unique var y = A() +} + +fun borrowBoth(@Borrowed a: Any, @Borrowed b: Any) {} + +fun consumeBoth(@Unique a: Any, @Unique b: Any) {} + +fun shareBoth(a: Any, b: Any) {} + +fun `pass shared subproperty and parent to shareBoth`(a: B) { + shareBoth(a.y, a) +} + +fun `pass borrowed subproperty and parent to borrowBoth`(@Borrowed a: B) { + borrowBoth(a.y, a) +} + +fun `pass unique subproperty and parent to consumeBoth`(@Unique a: B) { + consumeBoth(a.y, a) +} + +fun `pass unique-borrowed subproperty and parent to borrowBoth`(@Unique @Borrowed a: B) { + borrowBoth(a.y, a) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_local.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_local.fir.diag.txt new file mode 100644 index 00000000..ff990412 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_local.fir.diag.txt @@ -0,0 +1,3 @@ +/return_local.kt:(288,289): error: Return uniqueness mismatch: cannot return a 'shared local' value + +/return_local.kt:(425,426): error: Return uniqueness mismatch: cannot return a 'unique local' value diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_local.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_local.kt new file mode 100644 index 00000000..7345b386 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_local.kt @@ -0,0 +1,24 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +fun consume(@Unique a: Any) {} + +fun share(a: Any) {} + +fun `return shared`(a: Any): Any { + return a +} + +fun `return borrowed`(@Borrowed a: Any): Any { + return a +} + +fun `return unique`(@Unique a: Any): Any { + return a +} + +fun `return unique-borrowed`(@Unique @Borrowed a: Any): Any { + return a +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_property.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_property.fir.diag.txt new file mode 100644 index 00000000..67963a10 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_property.fir.diag.txt @@ -0,0 +1,3 @@ +/return_property.kt:(364,367): error: Return uniqueness mismatch: cannot return a 'shared local' value + +/return_property.kt:(525,528): error: Return uniqueness mismatch: cannot return a 'unique local' value diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_property.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_property.kt new file mode 100644 index 00000000..c3c6691c --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/return_property.kt @@ -0,0 +1,29 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A { + @Unique var x = Object() + @Unique var w = Object() +} + +class B { + @Unique var y = A() +} + +fun `return shared subproperty`(a: B): Any { + return a.y +} + +fun `return borrowed subproperty`(@Borrowed a: B): Any { + return a.y +} + +fun `return unique subproperty`(@Unique a: B): Any { + return a.y +} + +fun `return unique-borrowed subproperty`(@Unique @Borrowed a: B): Any { + return a.y +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_local.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_local.fir.diag.txt new file mode 100644 index 00000000..3266c704 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_local.fir.diag.txt @@ -0,0 +1,3 @@ +/share_local.kt:(269,270): error: Argument uniqueness mismatch: expected 'shared global', actual 'shared local'. + +/share_local.kt:(390,391): error: Argument uniqueness mismatch: expected 'shared global', actual 'unique local'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_local.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_local.kt new file mode 100644 index 00000000..ecb5e802 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_local.kt @@ -0,0 +1,26 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A() + +fun share(a: Any) {} + +// Sharing locals + +fun `share shared`(y: A) { + share(y) +} + +fun `share borrowed`(@Borrowed y: A) { + share(y) +} + +fun `share unique`(@Unique y: A) { + share(y) +} + +fun `share unique-borrowed`(@Borrowed @Unique y: A) { + share(y) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_properties.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_properties.fir.diag.txt new file mode 100644 index 00000000..1566a41a --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_properties.fir.diag.txt @@ -0,0 +1,9 @@ +/share_properties.kt:(433,438): error: Argument uniqueness mismatch: expected 'shared global', actual 'shared local'. + +/share_properties.kt:(586,591): error: Argument uniqueness mismatch: expected 'shared global', actual 'unique local'. + +/share_properties.kt:(808,809): error: Argument uniqueness mismatch: partial type 'moved' is inconsistent with parent type 'unique global'. + +/share_properties.kt:(884,885): error: Argument uniqueness mismatch: partial type 'shared global' is inconsistent with parent type 'unique global'. + +/share_properties.kt:(1018,1019): error: Assignment uniqueness mismatch: expected 'unique global', actual 'shared global'. diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_properties.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_properties.kt new file mode 100644 index 00000000..2d21c291 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/share_properties.kt @@ -0,0 +1,64 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class A { + @Unique var x = Object() + @Unique var w = Object() +} + +class B { + @Unique var y = A() +} + +fun consume(@Unique a: Any) {} + +fun share(a: Any) {} + +// Sharing subproperties + +fun `share shared subproperty`(z: B) { + share(z.y.x) +} + +fun `share borrowed subproperty`(@Borrowed z: B) { + share(z.y.x) +} + +fun `share unique subproperty`(@Unique z: B) { + share(z.y.x) +} + +fun `share unique-borrowed subproperty`(@Unique @Borrowed z: B) { + share(z.y.x) +} + +fun `share multiple unique subproperties`(@Unique z: B) { + share(z.y.x) + share(z.y.w) +} + +// Sharing partially-inconsistent properties + +fun `share partially moved`(@Unique z: B) { + consume(z.y) + share(z) +} + +fun `share partially shared`(@Unique z: B) { + share(z.y) + share(z) +} + +// Sharing subproperties after assignment + +fun `share subproperty after assigning it to shared`(@Unique x: B, v: A) { + x.y = v + share(x.y) +} + +fun `share subproperty after assigning it to unique`(@Unique x: B, @Unique v: A) { + x.y = v + share(x.y) +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/shared_to_shared.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/shared_to_shared.kt deleted file mode 100644 index eeaf009a..00000000 --- a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/shared_to_shared.kt +++ /dev/null @@ -1,13 +0,0 @@ -// UNIQUE_CHECK_ONLY - -import org.jetbrains.kotlin.formver.plugin.NeverConvert -import org.jetbrains.kotlin.formver.plugin.NeverVerify -import org.jetbrains.kotlin.formver.plugin.Unique - -fun f(x: Int) { - -} - -fun use_f(y: Int) { - f(y) -} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_local.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_local.fir.diag.txt new file mode 100644 index 00000000..df3bb84b --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_local.fir.diag.txt @@ -0,0 +1,3 @@ +/throw_local.kt:(232,233): error: Throw uniqueness mismatch: cannot throw a 'shared local' value + +/throw_local.kt:(367,368): error: Throw uniqueness mismatch: cannot throw a 'unique local' value diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_local.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_local.kt new file mode 100644 index 00000000..0c6cbd01 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_local.kt @@ -0,0 +1,20 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +fun `throw shared`(a: Throwable) { + throw a +} + +fun `throw borrowed`(@Borrowed a: Throwable) { + throw a +} + +fun `throw unique`(@Unique a: Throwable) { + throw a +} + +fun `throw unique-borrowed`(@Unique @Borrowed a: Throwable) { + throw a +} diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_property.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_property.fir.diag.txt new file mode 100644 index 00000000..85ef5e45 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_property.fir.diag.txt @@ -0,0 +1,3 @@ +/throw_property.kt:(287,290): error: Throw uniqueness mismatch: cannot throw a 'shared local' value + +/throw_property.kt:(434,437): error: Throw uniqueness mismatch: cannot throw a 'unique local' value diff --git a/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_property.kt b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_property.kt new file mode 100644 index 00000000..71bdf11a --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/uniqueness_checker/throw_property.kt @@ -0,0 +1,24 @@ +// UNIQUE_CHECK_ONLY + +import org.jetbrains.kotlin.formver.plugin.Borrowed +import org.jetbrains.kotlin.formver.plugin.Unique + +class B { + @Unique var y = Exception() +} + +fun `throw shared subproperty`(a: B) { + throw a.y +} + +fun `throw borrowed subproperty`(@Borrowed a: B) { + throw a.y +} + +fun `throw unique subproperty`(@Unique a: B) { + throw a.y +} + +fun `throw unique-borrowed subproperty`(@Unique @Borrowed a: B) { + throw a.y +} diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/ContextTrie.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/ContextTrie.kt deleted file mode 100644 index c3e8959f..00000000 --- a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/ContextTrie.kt +++ /dev/null @@ -1,44 +0,0 @@ -package org.jetbrains.kotlin.formver.uniqueness - -import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol -import org.jetbrains.kotlin.fir.symbols.impl.FirValueParameterSymbol - -class ContextTrie( - val parent: ContextTrie?, - val symbol: FirBasedSymbol<*>?, - val children: MutableMap, ContextTrie>, - override var level: UniqueLevel -) : UniquePathContext { - context(context: UniqueCheckerContext) override fun getOrPutPath(path: List>): ContextTrie { - if (path.isEmpty()) return this - - val (head, tail) = path.first() to path.drop(1) - val node = children.getOrPut(head) { - ContextTrie(this, head, mutableMapOf(), context.resolveUniqueAnnotation(head)) - } - return node.getOrPutPath(tail) - } - - private val localVariable: FirBasedSymbol<*>? - get() { - val local = parent?.localVariable ?: this.symbol - return local as? FirValueParameterSymbol - } - - context(context: UniqueCheckerContext) override val borrowingLevel: BorrowingLevel - get() = localVariable?.let { context.resolveBorrowingAnnotation(it) } ?: BorrowingLevel.Plain - - override val subtreeLUB: UniqueLevel - get() = listOfNotNull( - level, - children.values.maxOfOrNull { it.subtreeLUB }).max() - - override val pathToRootLUB: UniqueLevel - get() = listOfNotNull(parent?.pathToRootLUB, level).max() - - context(context: UniqueCheckerContext) override val hasChanges: Boolean - get() { - val changed = symbol?.let { level != context.resolveUniqueAnnotation(it) } ?: false - return changed || children.values.any { it.hasChanges } - } -} diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/DataFlowAnalyzer.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/DataFlowAnalyzer.kt new file mode 100644 index 00000000..8e6a807c --- /dev/null +++ b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/DataFlowAnalyzer.kt @@ -0,0 +1,167 @@ +/* + * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. + * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. + */ + +package org.jetbrains.kotlin.formver.uniqueness + +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.CFGNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.ControlFlowGraph + +/** + * Stores the flow facts before and after each CFG node. + * + * @param F the type of the flow object. + */ +class FlowFacts( + private val flowBefore: Map, F>, + private val flowAfter: Map, F> +) { + /** + * Returns the dataflow fact holding *before* the given [node] is executed. + */ + fun flowBefore(node: CFGNode<*>): F = + flowBefore[node] ?: throw IllegalArgumentException("No flow-before information for node: $node") + + /** + * Returns the dataflow fact holding *after* the given [node] is executed. + */ + fun flowAfter(node: CFGNode<*>): F = + flowAfter[node] ?: throw IllegalArgumentException("No flow-after information for node: $node") +} + +/** + * Directions for dataflow analysis. + */ +enum class FlowDirection { + FORWARD, + BACKWARD +} + +/** + * A generic, worklist-based dataflow analysis over [ControlFlowGraph]. + * + * @param F the type of the flow fact. + * @param direction whether the analysis propagates forward or backward along + * the CFG edges. + */ +abstract class DataFlowAnalyzer( + val direction: FlowDirection = FlowDirection.FORWARD, +) { + /** + * Returns the initial dataflow fact for the entry point of the analysis. + */ + abstract val initial: F + + /** + * Returns the initial flow fact for an intermediate point of the analysis. + */ + abstract val bottom: F + + /** + * Merges two flow facts at a join point. + * + * @param a the first flow fact. + * @param b the second flow fact. + * @return the joined flow fact. + */ + abstract fun join(a: F, b: F): F + + /** + * The transfer function. Given the dataflow fact [inFlow] arriving at [node], returns the fact that holds after + * [node]. + * + * @param node the CFG node to transfer. + * @param inFlow the incoming dataflow fact. + * @return the outgoing dataflow fact. + */ + abstract fun transfer(node: CFGNode<*>, inFlow: F): F + + /** + * Runs the worklist algorithm on [graph] and returns a [FlowFacts] containing the before/after facts for every + * node. + * + * @param graph the control flow graph to analyze. + * @return a [FlowFacts] containing the before/after facts for every node. + */ + fun analyze(graph: ControlFlowGraph): FlowFacts { + val nodes: List> = graph.nodes + val inFlow = mutableMapOf, F>() + val outFlow = mutableMapOf, F>() + val entryNode: CFGNode<*> + val predecessorsOf: (CFGNode<*>) -> List> + + when (direction) { + FlowDirection.FORWARD -> { + entryNode = nodes.first() + predecessorsOf = { node -> node.previousNodes } + } + FlowDirection.BACKWARD -> { + entryNode = nodes.last() + predecessorsOf = { node -> node.followingNodes } + } + } + + for (node in nodes) { + inFlow[node] = bottom + outFlow[node] = bottom + } + + inFlow[entryNode] = initial + outFlow[entryNode] = transfer(entryNode, initial) + + val worklist = ArrayDeque>() + val justAdded = mutableSetOf>() + + for (node in nodes) { + if (node !== entryNode) { + worklist.addLast(node) + justAdded.add(node) + } + } + + while (worklist.isNotEmpty()) { + val node = worklist.removeFirst() + justAdded.remove(node) + val predecessors = predecessorsOf(node) + + val joinedIn = if (predecessors.isEmpty()) { + bottom + } else { + predecessors + .map { outFlow[it] ?: bottom } + .reduce { result, flow -> join(result, flow) } + } + + inFlow[node] = joinedIn + val newOut = transfer(node, joinedIn) + + if (newOut != outFlow[node]) { + outFlow[node] = newOut + + val successors = when (direction) { + FlowDirection.FORWARD -> node.followingNodes + FlowDirection.BACKWARD -> node.previousNodes + } + + for (successor in successors) { + if (successor !in justAdded) { + worklist.addLast(successor) + justAdded.add(successor) + } + } + } + } + + return when (direction) { + FlowDirection.FORWARD -> FlowFacts( + flowBefore = inFlow.toMap(), + flowAfter = outFlow.toMap(), + ) + FlowDirection.BACKWARD -> FlowFacts( + flowBefore = outFlow.toMap(), + flowAfter = inFlow.toMap(), + ) + } + } +} diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/Path.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/Path.kt new file mode 100644 index 00000000..5737098b --- /dev/null +++ b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/Path.kt @@ -0,0 +1,90 @@ +/* + * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. + * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. + */ + +package org.jetbrains.kotlin.formver.uniqueness + +import org.jetbrains.kotlin.fir.FirElement +import org.jetbrains.kotlin.fir.declarations.FirProperty +import org.jetbrains.kotlin.fir.expressions.FirPropertyAccessExpression +import org.jetbrains.kotlin.fir.references.FirResolvedNamedReference +import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol +import org.jetbrains.kotlin.fir.visitors.FirVisitor + +typealias Path = List> + +/** + * A visitor for extracting an atomic receiving path from a [org.jetbrains.kotlin.fir.expressions.FirExpression]. + * + * This visitor differs from [ValuePathCollector] in that it only extracts the path of a receiver expression in an + * assignment, as opposed to the possible yielded paths. + */ +object ReceiverPathExtractor : FirVisitor() { + override fun visitElement( + element: FirElement, + data: Unit + ): Path? = null + + override fun visitResolvedNamedReference( + resolvedNamedReference: FirResolvedNamedReference, + data: Unit + ): Path = listOf(resolvedNamedReference.resolvedSymbol) + + override fun visitProperty( + property: FirProperty, + data: Unit + ): Path = listOf(property.symbol) + + override fun visitPropertyAccessExpression( + propertyAccessExpression: FirPropertyAccessExpression, + data: Unit + ): Path? { + val parent = propertyAccessExpression.explicitReceiver?.accept(this, data) ?: emptyList() + val callee = propertyAccessExpression.calleeReference.accept(this, data) ?: emptyList() + + if (parent.isEmpty() && callee.isEmpty()) { + return null + } else { + return parent + callee + } + } +} + +val FirElement.receiverPath + get() = accept(ReceiverPathExtractor, Unit) + +/** + * A visitor for collecting the paths that may be yielded by a [org.jetbrains.kotlin.fir.expressions.FirExpression]. + * + * This visitor differs from [ReceiverPathExtractor] in that it collects all paths that may be yielded by an expression. + * In the future this visitor will be expanded to handle more complex expressions such as `if` expressions, elvis + * operator, etc. + */ +object ValuePathCollector : FirVisitor, Unit>() { + override fun visitElement( + element: FirElement, + data: Unit + ): List = emptyList() + + override fun visitResolvedNamedReference( + resolvedNamedReference: FirResolvedNamedReference, + data: Unit + ): List = listOf(ReceiverPathExtractor.visitResolvedNamedReference(resolvedNamedReference, data)) + + override fun visitPropertyAccessExpression( + propertyAccessExpression: FirPropertyAccessExpression, + data: Unit + ): List { + val path = ReceiverPathExtractor.visitPropertyAccessExpression(propertyAccessExpression, data) + + if (path != null) { + return listOf(path) + } else { + return emptyList() + } + } +} + +val FirElement.valuePaths + get() = accept(ValuePathCollector, Unit) diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueCheckVisitor.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueCheckVisitor.kt deleted file mode 100644 index 15be3492..00000000 --- a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueCheckVisitor.kt +++ /dev/null @@ -1,166 +0,0 @@ -/* - * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. - * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. - */ - -package org.jetbrains.kotlin.formver.uniqueness - -import org.jetbrains.kotlin.fir.FirElement -import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction -import org.jetbrains.kotlin.fir.expressions.* -import org.jetbrains.kotlin.fir.references.FirResolvedNamedReference -import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol -import org.jetbrains.kotlin.fir.symbols.SymbolInternals -import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol -import org.jetbrains.kotlin.fir.visitors.FirVisitor - -object PathVisitor : FirVisitor>, Unit>() { - override fun visitElement(element: FirElement, data: Unit) = - throw IllegalStateException("LocalVariableVisitor should not be called on general FIR elements") - - override fun visitResolvedNamedReference( - resolvedNamedReference: FirResolvedNamedReference, data: Unit - ): List> = listOf(resolvedNamedReference.resolvedSymbol) - - override fun visitPropertyAccessExpression( - propertyAccessExpression: FirPropertyAccessExpression, data: Unit - ): List> { - val parent = propertyAccessExpression.explicitReceiver?.accept(this, data) ?: emptyList() - return parent + propertyAccessExpression.calleeReference.accept(this, data) - } -} - -/** - * Resolve the path of a property access expression. - * - * For example, `a.b.c.d` will be resolved to `local/a`, `A/b`, `B/c`, `C/d`. - */ -fun FirPropertyAccessExpression.resolvePath(): List> = accept(PathVisitor, Unit) - -object UniqueCheckVisitor : FirVisitor, UniqueCheckerContext>() { - override fun visitElement(element: FirElement, data: UniqueCheckerContext) = - throw IllegalStateException("UniqueCheckVisitor should not be called on general FIR elements") - - override fun visitSimpleFunction( - simpleFunction: FirSimpleFunction, data: UniqueCheckerContext - ): Pair { - simpleFunction.body?.accept(this, data) - // Function definition doesn't have to return a unique level - return Pair(UniqueLevel.Shared, null) - } - - override fun visitLiteralExpression( - literalExpression: FirLiteralExpression, data: UniqueCheckerContext - ): Pair = Pair(UniqueLevel.Unique, null) - - override fun visitPropertyAccessExpression( - propertyAccessExpression: FirPropertyAccessExpression, data: UniqueCheckerContext - ): Pair { - val path = propertyAccessExpression.resolvePath() - val last = data.getOrPutPath(path) - - return Pair(last.pathToRootLUB, last) - } - - override fun visitBlock(block: FirBlock, data: UniqueCheckerContext): Pair { - block.statements.forEach { statement -> - when (statement) { - is FirFunctionCall -> { - statement.accept(this, data) - } - } - } - return Pair(UniqueLevel.Shared, null) - } - - private fun verifyPassingRules( - functionCall: FirFunctionCall, - argument: FirExpression, - requirements: Pair, - actual: Pair, - pathContext: UniquePathContext?, - data: UniqueCheckerContext, - ) { - val (requiredUnique, requiredBorrowing) = requirements - val (argumentUnique, argumentBorrowing) = actual - - if (argumentUnique == UniqueLevel.Top) { - throw UniquenessCheckException( - argument.source, - "cannot access expression as its uniqueness state is top" - ) - } - - val argumentSubtreeLUB = pathContext?.subtreeLUB - if (argumentSubtreeLUB == UniqueLevel.Top) { - throw UniquenessCheckException( - argument.source, - "a partially moved object cannot be passed as an argument" - ) - } - - if (argumentBorrowing > requiredBorrowing) { - throw UniquenessCheckException( - argument.source, - "cannot pass borrowed value as non-borrowed" - ) - } - - if (requiredUnique == UniqueLevel.Unique) { - if (argumentUnique != UniqueLevel.Unique) { - throw UniquenessCheckException( - argument.source, - "expected unique value, got ${argumentUnique.toString().lowercase()}" - ) - } - - val subtreeChanged = with(data) { pathContext?.hasChanges ?: false } - if (subtreeChanged) { - throw UniquenessCheckException( - argument.source, - "cannot pass a partially shared argument" - ) - } - } - } - - @OptIn(SymbolInternals::class) - override fun visitFunctionCall( - functionCall: FirFunctionCall, data: UniqueCheckerContext - ): Pair { - // To keep it simple, assume a functionCall always return Shared for now - val symbol = functionCall.toResolvedCallableSymbol() - val params = (symbol as FirFunctionSymbol<*>).fir.valueParameters - val requiredUniqueLevels = params.map { data.resolveUniqueAnnotation(it) } - val paramBorrowingLevels = params.map { data.resolveBorrowingAnnotation(it) } - - val arguments = functionCall.arguments - arguments.forEachIndexed { index, argument -> - val requiredUnique = requiredUniqueLevels[index] - val paramBorrowing = paramBorrowingLevels[index] - - val (argumentUnique, pathContext) = argument.accept(this, data) - val argumentBorrowing = with(data) { pathContext?.borrowingLevel ?: BorrowingLevel.Plain } - verifyPassingRules( - functionCall, - argument, - requirements = Pair(requiredUnique, paramBorrowing), - actual = Pair(argumentUnique, argumentBorrowing), - pathContext, - data, - ) - - if (paramBorrowing != BorrowingLevel.Borrowed) { - when (requiredUnique) { - UniqueLevel.Unique -> pathContext?.level = UniqueLevel.Top - UniqueLevel.Shared -> pathContext?.level = UniqueLevel.Shared - else -> throw IllegalStateException("argument can't request unique level $requiredUnique") - } - } - } - - val callee = functionCall.toResolvedCallableSymbol()?.fir as FirSimpleFunction - return Pair(data.resolveUniqueAnnotation(callee), null) - } -} - diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueChecker.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueChecker.kt deleted file mode 100644 index c407f2c4..00000000 --- a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueChecker.kt +++ /dev/null @@ -1,46 +0,0 @@ -/* - * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. - * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. - */ - -package org.jetbrains.kotlin.formver.uniqueness - -import org.jetbrains.kotlin.fir.FirSession -import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol -import org.jetbrains.kotlin.fir.symbols.impl.FirValueParameterSymbol -import org.jetbrains.kotlin.formver.common.ErrorCollector -import org.jetbrains.kotlin.formver.common.PluginConfiguration -import org.jetbrains.kotlin.name.ClassId -import org.jetbrains.kotlin.name.FqName -import org.jetbrains.kotlin.name.Name - -class UniqueChecker( - override val session: FirSession, - override val config: PluginConfiguration, - override val errorCollector: ErrorCollector, -) : UniqueCheckerContext { - @Suppress("SameParameterValue") - private fun getAnnotationId(name: String): ClassId = - ClassId(FqName.fromSegments(listOf("org", "jetbrains", "kotlin", "formver", "plugin")), Name.identifier(name)) - - private val uniqueId: ClassId - get() = getAnnotationId("Unique") - - private val borrowingId: ClassId - get() = getAnnotationId("Borrowed") - - private val uniqueContext = ContextTrie(null, null, mutableMapOf(), UniqueLevel.Unique) - - override fun resolveUniqueAnnotation(declaration: HasAnnotation): UniqueLevel = - if (declaration.hasAnnotation(uniqueId, session)) UniqueLevel.Unique else UniqueLevel.Shared - - override fun resolveBorrowingAnnotation(declaration: HasAnnotation): BorrowingLevel = - if (declaration.hasAnnotation(borrowingId, session)) BorrowingLevel.Borrowed else BorrowingLevel.Plain - - override fun getOrPutPath(path: List>): UniquePathContext { - require(path.isNotEmpty()) { "Provided path is empty" } - require(path.first() is FirValueParameterSymbol) { "Provided path does not start with a local variable" } - - return uniqueContext.getOrPutPath(path) - } -} \ No newline at end of file diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueCheckerContext.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueCheckerContext.kt deleted file mode 100644 index 1cef8b2a..00000000 --- a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueCheckerContext.kt +++ /dev/null @@ -1,58 +0,0 @@ -/* - * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. - * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. - */ - -package org.jetbrains.kotlin.formver.uniqueness - -import org.jetbrains.kotlin.fir.FirAnnotationContainer -import org.jetbrains.kotlin.fir.FirSession -import org.jetbrains.kotlin.fir.declarations.hasAnnotation -import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol -import org.jetbrains.kotlin.formver.common.ErrorCollector -import org.jetbrains.kotlin.formver.common.PluginConfiguration -import org.jetbrains.kotlin.name.ClassId - -sealed interface HasAnnotation { - class Symbol(val symbol: FirBasedSymbol<*>) : HasAnnotation { - override fun hasAnnotation(id: ClassId, session: FirSession) = symbol.hasAnnotation(id, session) - } - - class AnnotationContainer(val container: FirAnnotationContainer) : HasAnnotation { - override fun hasAnnotation(id: ClassId, session: FirSession) = container.hasAnnotation(id, session) - } - - fun hasAnnotation(id: ClassId, session: FirSession): Boolean -} - -interface UniqueCheckerContext { - val config: PluginConfiguration - val errorCollector: ErrorCollector - val session: FirSession - - fun resolveUniqueAnnotation(declaration: HasAnnotation): UniqueLevel - fun resolveBorrowingAnnotation(declaration: HasAnnotation): BorrowingLevel - - /** - * Retrieves the [ContextTrie] node corresponding to the given path. - * If the path does not exist in the current context, inserts the necessary nodes. - * - * @param path A list of [FirBasedSymbol] items representing a sequence of symbols forming a path in code (`x.y.z -> [local/x, A/y, B/z]`). - * Note that the first element in the path must be a local symbol. - * @return The [ContextTrie] node at the end of the specified path. - * If intermediate nodes do not exist, they are created with unique levels extracted from annotations. - */ - fun getOrPutPath(path: List>): UniquePathContext -} - -fun UniqueCheckerContext.resolveUniqueAnnotation(declaration: FirBasedSymbol<*>): UniqueLevel = - resolveUniqueAnnotation(HasAnnotation.Symbol(declaration)) - -fun UniqueCheckerContext.resolveUniqueAnnotation(declaration: FirAnnotationContainer): UniqueLevel = - resolveUniqueAnnotation(HasAnnotation.AnnotationContainer(declaration)) - -fun UniqueCheckerContext.resolveBorrowingAnnotation(declaration: FirBasedSymbol<*>): BorrowingLevel = - resolveBorrowingAnnotation(HasAnnotation.Symbol(declaration)) - -fun UniqueCheckerContext.resolveBorrowingAnnotation(declaration: FirAnnotationContainer): BorrowingLevel = - resolveBorrowingAnnotation(HasAnnotation.AnnotationContainer(declaration)) \ No newline at end of file diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueLevel.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueLevel.kt deleted file mode 100644 index 0d024522..00000000 --- a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniqueLevel.kt +++ /dev/null @@ -1,17 +0,0 @@ -/* - * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. - * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. - */ - -package org.jetbrains.kotlin.formver.uniqueness - -enum class UniqueLevel { - Unique, - Shared, - Top, -} - -enum class BorrowingLevel { - Plain, - Borrowed, -} \ No newline at end of file diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquePathContext.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquePathContext.kt deleted file mode 100644 index d429d834..00000000 --- a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquePathContext.kt +++ /dev/null @@ -1,51 +0,0 @@ -package org.jetbrains.kotlin.formver.uniqueness - -import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol -import org.jetbrains.kotlin.formver.uniqueness.UniqueLevel.* - -/** - * Stores unique context for each path in a trie structure. - * - * Each path represents a sequence of symbols like x.y.z, where each node has a unique level annotation ([Unique]/[Shared]/[Top]) - * - * Example: - * ``` - * x.y.w => local/x --> A/y -> B/w -> .. - * ^ | - * x.z.w ======+ +-> A/z -> C/w -> ... - * ``` - */ -interface UniquePathContext { - var level: UniqueLevel - context(_: UniqueCheckerContext) val borrowingLevel: BorrowingLevel - - /** - * Retrieves the child node corresponding to the given path within the trie structure, - * or creates and inserts a new path if it does not already exist. - * This method uses the provided context to resolve unique annotations for new nodes. - * - * @param path A list of [FirBasedSymbol] items representing the path to traverse or create in the trie. - * Each symbol corresponds to a hierarchical level in the path. - * @return The [ContextTrie] node at the end of the given path, creating intermediate nodes as necessary. - */ - context(context: UniqueCheckerContext) fun getOrPutPath(path: List>): UniquePathContext - - /** - * Represents the least upper bound (LUB) of uniqueness levels for the subtree - * originating at this node in the trie structure. - */ - val subtreeLUB: UniqueLevel - - /** - * Represents the least upper bound (LUB) of uniqueness levels for the path from the current node - * to the root of the trie structure. - * - * For example, for the node representing `x.y.z`, this would return the LUB of `x.y.z`, `x.y` and `x` - */ - val pathToRootLUB: UniqueLevel - - /** - * Represents whether the subtree originating at this node in the trie has any changes - */ - context(_: UniqueCheckerContext) val hasChanges: Boolean -} \ No newline at end of file diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessCheckException.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessCheckException.kt index 8443628b..092f5cd6 100644 --- a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessCheckException.kt +++ b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessCheckException.kt @@ -1,3 +1,8 @@ +/* + * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. + * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. + */ + package org.jetbrains.kotlin.formver.uniqueness import org.jetbrains.kotlin.KtSourceElement diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessGraphAnalyzer.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessGraphAnalyzer.kt new file mode 100644 index 00000000..ad34d186 --- /dev/null +++ b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessGraphAnalyzer.kt @@ -0,0 +1,120 @@ +/* + * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. + * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. + */ + +package org.jetbrains.kotlin.formver.uniqueness + +import org.jetbrains.kotlin.fir.FirElement +import org.jetbrains.kotlin.fir.expressions.arguments +import org.jetbrains.kotlin.fir.expressions.toResolvedCallableSymbol +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.CFGNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.ControlFlowGraphVisitor +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.FunctionCallEnterNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.VariableAssignmentNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.VariableDeclarationNode +import org.jetbrains.kotlin.fir.symbols.SymbolInternals +import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol + +/** + * Visitor assigning uniqueness types to paths after the execution of a [CFGNode]. + * + * @param resolver The resolver used for fetching the default uniqueness type of parameter symbols. + */ +class UniquenessTypeAssigner( + private val resolver: UniquenessResolver +): ControlFlowGraphVisitor() { + override fun visitNode(node: CFGNode<*>, data: UniquenessTrie): UniquenessTrie = data + + private fun evaluateDefinition(receiver: FirElement, value: FirElement, data: UniquenessTrie): UniquenessTrie { + val result = data.copy() + val receiverPath = receiver.receiverPath + val valuePaths = value.valuePaths + + if (receiverPath != null) { + result[receiverPath] = resolver.resolveUniquenessType(receiverPath.last()) + } + + for (valuePath in valuePaths) { + val valueType = data[valuePath] + + if (valueType is UniquenessType.Active && valueType.uniqueLevel == UniqueLevel.Unique) { + result[valuePath] = UniquenessType.Moved + } + } + + return result + } + + override fun visitVariableDeclarationNode(node: VariableDeclarationNode, data: UniquenessTrie): UniquenessTrie { + val receiver = node.fir + val value = node.fir.initializer ?: return data + + return evaluateDefinition(receiver, value, data) + } + + override fun visitVariableAssignmentNode(node: VariableAssignmentNode, data: UniquenessTrie): UniquenessTrie { + val receiver = node.fir.lValue + val value = node.fir.rValue + + return evaluateDefinition(receiver, value, data) + } + + @OptIn(SymbolInternals::class) + override fun visitFunctionCallEnterNode(node: FunctionCallEnterNode, data: UniquenessTrie): UniquenessTrie { + val functionCall = node.fir + val callableSymbol = functionCall.toResolvedCallableSymbol() as? FirFunctionSymbol<*> + ?: throw IllegalStateException("Unable to resolve ${functionCall}") + val callableDeclaration = callableSymbol.fir + val result = data.copy() + + // TODO: If possible, it would be good to compute the outflow for the argument before reaching the + // [FunctionCallEnterNode]. This would allow us to provide more precise flow information to the checker. + // {@see UniquenessGraphChecker.visitFunctionCallEnterNode} + for ((argument, parameter) in functionCall.arguments.zip(callableDeclaration.valueParameters)) { + for (argumentPath in argument.valuePaths) { + val parameterType = resolver.resolveUniquenessType(parameter.symbol) + + if (parameterType.borrowLevel == BorrowLevel.Global) { + when (parameterType.uniqueLevel) { + UniqueLevel.Unique -> { + result[argumentPath] = UniquenessType.Moved + } + + UniqueLevel.Shared -> { + result[argumentPath] = UniquenessType.Active(UniqueLevel.Shared, BorrowLevel.Global) + } + } + } + } + } + + return result + } +} + +/** + * Analyzer inferring the uniqueness typing environment before and after the execution of each node. + * + * @param resolver The resolver used for fetching the default uniqueness type of some path. + * @param initial The initial uniqueness typing environment. + */ +class UniquenessGraphAnalyzer( + resolver: UniquenessResolver, + override val initial: UniquenessTrie +) : DataFlowAnalyzer(FlowDirection.FORWARD) { + val typeAssigner = UniquenessTypeAssigner(resolver) + + override val bottom: UniquenessTrie = UniquenessTrie(resolver) + + override fun join(a: UniquenessTrie, b: UniquenessTrie): UniquenessTrie { + val result = a.copy() + result.join(b) + + return result + } + + @OptIn(SymbolInternals::class) + override fun transfer(node: CFGNode<*>, inFlow: UniquenessTrie): UniquenessTrie = + node.accept(typeAssigner, inFlow) +} diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessGraphChecker.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessGraphChecker.kt new file mode 100644 index 00000000..8307c648 --- /dev/null +++ b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessGraphChecker.kt @@ -0,0 +1,236 @@ +/* + * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. + * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. + */ + +package org.jetbrains.kotlin.formver.uniqueness + +import org.jetbrains.kotlin.fir.FirElement +import org.jetbrains.kotlin.fir.FirSession +import org.jetbrains.kotlin.fir.expressions.FirExpression +import org.jetbrains.kotlin.fir.expressions.FirReturnExpression +import org.jetbrains.kotlin.fir.expressions.arguments +import org.jetbrains.kotlin.fir.expressions.toResolvedCallableSymbol +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.CFGNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.ControlFlowGraph +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.ControlFlowGraphVisitor +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.FunctionCallEnterNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.JumpNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.ThrowExceptionNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.VariableAssignmentNode +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.VariableDeclarationNode +import org.jetbrains.kotlin.fir.symbols.SymbolInternals +import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol +import org.jetbrains.kotlin.formver.common.ErrorCollector + +/** + * A visitor for checking uniqueness types in a [CFGNode]. + * + * @param resolver The resolver used for fetching the default uniqueness type of parameter symbols. + * @param errorCollector A collector for the checker's errors. + */ +class UniquenessTypeChecker( + val resolver: UniquenessResolver, + val errorCollector: ErrorCollector +) : ControlFlowGraphVisitor() { + override fun visitNode(node: CFGNode<*>, data: UniquenessTrie) {} + + private fun checkValueUsage( + value: FirExpression, + expectedType: UniquenessType.Active, + data: UniquenessTrie, + onError: (UniquenessType) -> Unit + ) { + for (valuePath in value.valuePaths) { + val valueData = data.ensure(valuePath) + val actualType = valueData.parentsJoin + + when (actualType) { + // TODO: Use errorCollector for errors, allowing to report more than one error per declaration. + is UniquenessType.Moved -> { + return onError(actualType) + } + + is UniquenessType.Active -> { + if (actualType.borrowLevel > expectedType.borrowLevel) { + return onError(actualType) + } + + if (actualType.uniqueLevel > expectedType.uniqueLevel) { + return onError(actualType) + } + } + } + } + } + + private fun checkDefinition( + receiver: FirElement, + value: FirExpression, + data: UniquenessTrie, + onError: (UniquenessType, UniquenessType) -> Unit + ) { + val receiverPath = receiver.receiverPath ?: return + val expectedType = resolver.resolveUniquenessType(receiverPath.last()) + checkValueUsage(value, expectedType, data) { actualType -> + onError(expectedType, actualType) + } + } + + override fun visitVariableDeclarationNode(node: VariableDeclarationNode, data: UniquenessTrie) { + val receiver = node.fir + val value = node.fir.initializer ?: return + checkDefinition(receiver, value, data) { expectedType, actualType -> + throw UniquenessCheckException( + value.source, + "Initializer uniqueness mismatch: expected '${expectedType}', actual '${actualType}'." + ) + } + } + + override fun visitVariableAssignmentNode(node: VariableAssignmentNode, data: UniquenessTrie) { + val receiver = node.fir.lValue + val value = node.fir.rValue + checkDefinition(receiver, value, data) { expectedType, actualType -> + throw UniquenessCheckException( + value.source, + "Assignment uniqueness mismatch: expected '${expectedType}', actual '${actualType}'." + ) + } + } + + private fun checkInvariance( + value: FirExpression, + data: UniquenessTrie, + onError: (UniquenessType, UniquenessType) -> Unit + ) { + for (valuePath in value.valuePaths) { + val valueType = data.ensure(valuePath).parentsJoin + val expectedType = resolver.resolveUniquenessType(valuePath.last()) + + if (valueType is UniquenessType.Active && + valueType.uniqueLevel == UniqueLevel.Unique && + !data.isInvariant(valuePath)) { + val valuePartialType = data.childrenJoin + + when (valuePartialType) { + is UniquenessType.Moved -> + return onError(valueType, valuePartialType) + + is UniquenessType.Active -> { + if (valuePartialType.uniqueLevel > expectedType.uniqueLevel) { + return onError(valueType, valuePartialType) + } + } + } + } + } + } + + @OptIn(SymbolInternals::class) + override fun visitFunctionCallEnterNode(node: FunctionCallEnterNode, data: UniquenessTrie) { + val functionCall = node.fir + val callableSymbol = functionCall.toResolvedCallableSymbol() as? FirFunctionSymbol<*> + ?: throw IllegalStateException("Unable to resolve ${functionCall}") + val callableDeclaration = callableSymbol.fir + var currentData = data + + for ((argument, parameter) in functionCall.arguments.zip(callableDeclaration.valueParameters)) { + val argumentPaths = argument.valuePaths + + for (argumentPath in argumentPaths) { + val parameterType = resolver.resolveUniquenessType(parameter.symbol) + checkValueUsage(argument, parameterType, currentData) { actualType -> + throw UniquenessCheckException( + argument.source, + "Argument uniqueness mismatch: expected '${parameterType}', actual '${actualType}'." + ) + } + checkInvariance(argument, currentData) { expectedType, partialType -> + throw UniquenessCheckException( + argument.source, + "Argument uniqueness mismatch: partial type '${partialType}' is inconsistent with parent type '${expectedType}'." + ) + } + + // TODO: Look into how to do this at the analyzer level. + // As of now the analysis can only provide us with the uniqueness `data` before and after the method + // call, but we would like to compute this data before and after each parameter reference. + // {@see UniquenessGraphAnalyzer.visitFunctionCallEnterNode} + if (parameterType.uniqueLevel == UniqueLevel.Unique) { + currentData = currentData.copy() + currentData[argumentPath] = UniquenessType.Moved + } + } + } + } + + private fun checkLeakedValue( + value: FirExpression, + data: UniquenessTrie, + onError: (UniquenessType) -> Unit + ) { + val valuePaths = value.valuePaths + + for (valuePath in valuePaths) { + // TODO: Determine whether this is the only we we should be able to access the type of something + val valueType = data.ensure(valuePath).parentsJoin + + when (valueType) { + is UniquenessType.Moved -> { + return onError(valueType) + } + + is UniquenessType.Active -> { + if (valueType.borrowLevel == BorrowLevel.Local) { + return onError(valueType) + } + } + } + } + } + + override fun visitJumpNode(node: JumpNode, data: UniquenessTrie) { + val returnExpression = node.fir as? FirReturnExpression ?: return + val value = returnExpression.result + + checkLeakedValue(value, data) { valueType -> + throw UniquenessCheckException( + value.source, + "Return uniqueness mismatch: cannot return a '${valueType}' value" + ) + } + } + + override fun visitThrowExceptionNode(node: ThrowExceptionNode, data: UniquenessTrie) { + val throwExpression = node.fir + val exception = throwExpression.exception + checkLeakedValue(exception, data) { valueType -> + throw UniquenessCheckException( + exception.source, + "Throw uniqueness mismatch: cannot throw a '${valueType}' value" + ) + } + } +} + +class UniquenessGraphChecker( + session: FirSession, + initial: UniquenessTrie, + errorCollector: ErrorCollector +) { + val resolver = UniquenessResolver(session) + + val analyzer = UniquenessGraphAnalyzer(resolver, initial) + + val typeChecker = UniquenessTypeChecker(resolver, errorCollector) + + fun check(graph: ControlFlowGraph) { + val facts = analyzer.analyze(graph) + + for (node in graph.nodes) { + val store = facts.flowBefore(node) + node.accept(typeChecker, store) + } + } +} \ No newline at end of file diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessResolver.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessResolver.kt new file mode 100644 index 00000000..a205ae52 --- /dev/null +++ b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessResolver.kt @@ -0,0 +1,52 @@ +/* + * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. + * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. + */ + +package org.jetbrains.kotlin.formver.uniqueness + +import org.jetbrains.kotlin.fir.FirSession +import org.jetbrains.kotlin.fir.declarations.hasAnnotation +import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol +import org.jetbrains.kotlin.name.ClassId +import org.jetbrains.kotlin.name.FqName +import org.jetbrains.kotlin.name.Name + +/** + * Resolves and determines the default uniqueness and borrowing levels of FIR symbols. + * + * @param session The FIR session used to access annotations and metadata associated with symbols. + */ +class UniquenessResolver( + val session: FirSession +) { + private fun getAnnotationId(name: String): ClassId = + ClassId( + FqName.fromSegments(listOf("org", "jetbrains", "kotlin", "formver", "plugin")), + Name.identifier(name) + ) + + private val uniqueId: ClassId + get() = getAnnotationId("Unique") + + private val borrowId: ClassId + get() = getAnnotationId("Borrowed") + + fun resolveUniqueLevel(symbol: FirBasedSymbol<*>): UniqueLevel = + if (symbol.hasAnnotation(uniqueId, session)) + UniqueLevel.Unique + else + UniqueLevel.Shared + + fun resolveBorrowLevel(symbol: FirBasedSymbol<*>): BorrowLevel = + if (symbol.hasAnnotation(borrowId, session)) + BorrowLevel.Local + else + BorrowLevel.Global + + fun resolveUniquenessType(symbol: FirBasedSymbol<*>): UniquenessType.Active = + UniquenessType.Active( + resolveUniqueLevel(symbol), + resolveBorrowLevel(symbol) + ) +} \ No newline at end of file diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessTrie.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessTrie.kt new file mode 100644 index 00000000..8c345882 --- /dev/null +++ b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessTrie.kt @@ -0,0 +1,195 @@ +/* + * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. + * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. + */ + +package org.jetbrains.kotlin.formver.uniqueness + +import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol + +/** + * Stores unique context for each path in a trie structure. + * + * Each path represents a sequence of symbols like x.y.z, where each node has a uniqueness type annotation + * + * Example: + * ``` + * x.y.w => local/x --> A/y -> B/w -> .. + * ^ | + * x.z.w ======+ +-> A/z -> C/w -> ... + * ``` + */ +class UniquenessTrie( + val resolver: UniquenessResolver, + var type: UniquenessType = UniquenessType.Active(UniqueLevel.Unique, BorrowLevel.Global), + private val children: MutableMap, UniquenessTrie> = mutableMapOf(), + private val parent: UniquenessTrie? = null +) { + /** + * Represents the least upper bound (LUB) of uniqueness levels for the path from the current node * to the root of + * the trie structure. + * + * For example, for the node representing `x.y.z`, this would return the LUB of `x.y.z`, `x.y` and `x`. + */ + val parentsJoin: UniquenessType + get() = + if (parent != null) + type.join(parent.parentsJoin) + else + type + + /** + * Represents the least upper bound (LUB) of uniqueness levels for the subtree * originating at this node in the + * trie structure. + */ + val childrenJoin: UniquenessType + get() = children.values.fold(type) { result, child -> + result.join(child.childrenJoin) + } + + private fun isInvariant(symbol: FirBasedSymbol<*>): Boolean { + val actual = type + val default = resolver.resolveUniquenessType(symbol) + + return actual == default && + children.all { (symbol, store) -> + store.isInvariant(symbol) + } + } + + /** + * @return true if the subpaths of `symbol` are invariant with respect to their default specification, `false` + * otherwise. + */ + fun isInvariant(path: Path): Boolean { + return path.isEmpty() || ensure(path).isInvariant(path.first()) + } + + /** + * Ensures that there is a `UniquenessTrie` associated with the specified path, creating one if it does not exist. + * + * @param path The path for which the uniqueness store is to be ensured. + * @return The `UniquenessTrie` root corresponding to the given path, creating and associating one if necessary. + */ + fun ensure(path: Path): UniquenessTrie { + if (path.isEmpty()) { + return this + } + + val head = path.first() + val child = children.computeIfAbsent(head) { + UniquenessTrie( + resolver = resolver, + type = resolver.resolveUniquenessType(head), + parent = this + ) + } + + return child.ensure(path.subList(1, path.size)) + } + + /** + * Retrieves the uniqueness type for a given path. + * + * @param path The path to retrieve the uniqueness type for. + * @return The uniqueness type for the given path, or null if not found. + */ + operator fun get(path: Path): UniquenessType = + ensure(path).type + + /** + * Aggregates the uniqueness types of multiple paths into a single type. + * + * @param paths The list of paths of which type should be aggregated. + * @return The aggregated uniqueness type. + */ + fun aggregate(paths: List): UniquenessType { + if (paths.isEmpty()) { + return UniquenessType.Active(UniqueLevel.Shared, BorrowLevel.Global) + } else { + return paths.fold( + UniquenessType.Active(UniqueLevel.Unique, BorrowLevel.Global) as UniquenessType + ) { result, path -> result.join(get(path)) } + } + } + + /** + * Sets the uniqueness type for a given path. + * + * @param path The path to set the uniqueness type for. + * @return The updated UniquenessStore. + */ + operator fun set(path: Path, value: UniquenessType) { + val store = ensure(path) + store.type = value + } + + private fun copyWithParent(newParent: UniquenessTrie?): UniquenessTrie { + val newNode = UniquenessTrie(resolver, type, mutableMapOf(), newParent) + + for ((key, child) in children) { + newNode.children[key] = child.copyWithParent(newNode) + } + + return newNode + } + + /** + * @return a deep copy of this UniquenessTrie. + */ + fun copy(): UniquenessTrie { + val newChildren = children.mapValuesTo(mutableMapOf()) { (_, child) -> + child.copyWithParent(this) + } + + return UniquenessTrie(resolver, type, newChildren, parent) + } + + /** + * In-place, pointwise join of two UniquenessTries. + * + * @param other The other UniquenessTrie to join with. + */ + fun join(other: UniquenessTrie) { + type = type.join(other.type) + + for ((key, otherChild) in other.children) { + val thisChild = children[key] + + if (thisChild != null) { + thisChild.join(otherChild) + } else { + children[key] = otherChild.copyWithParent(this) + } + } + } + + private fun toString(prefix: String): String { + val builder = StringBuilder() + val prefix = "$prefix : $type" + + for ((key, child) in children) { + builder.appendLine(child.toString("$prefix / $key")) + } + + return builder.toString() + } + + override fun toString(): String = + toString("root") + + override fun equals(other: Any?): Boolean { + return other is UniquenessTrie && + resolver == other.resolver && + children == other.children && + type == other.type + } + + override fun hashCode(): Int { + var result = resolver.hashCode() + result = 31 * result + type.hashCode() + result = 31 * result + children.hashCode() + + return result + } +} \ No newline at end of file diff --git a/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessType.kt b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessType.kt new file mode 100644 index 00000000..87e4b23a --- /dev/null +++ b/formver.compiler-plugin/uniqueness/src/org/jetbrains/kotlin/formver/uniqueness/UniquenessType.kt @@ -0,0 +1,59 @@ +/* + * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors. + * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file. + */ + +package org.jetbrains.kotlin.formver.uniqueness + +enum class UniqueLevel { + Unique, + Shared, +} + +enum class BorrowLevel { + Global, + Local +} + +sealed interface UniquenessType { + /** + * Corresponds to the TOP type + */ + object Moved : UniquenessType { + override fun toString() = "moved" + } + + /** + * Intermediate components of the lattice + */ + data class Active(val uniqueLevel: UniqueLevel, val borrowLevel: BorrowLevel) : UniquenessType { + override fun toString() = "${uniqueLevel.name.lowercase()} ${borrowLevel.name.lowercase()}" + } + + /** + * Join operation for the uniqueness type lattice. + * + * @param other The other type to join with. + * @return The result of the join operation. + */ + fun join(other: UniquenessType): UniquenessType { + if (this == other) { + return this + } + + when (this) { + is Moved -> return this + is Active -> { + when (other) { + is Moved -> return other + is Active -> { + return Active( + maxOf(uniqueLevel, other.uniqueLevel), + maxOf(borrowLevel, other.borrowLevel) + ) + } + } + } + } + } +} \ No newline at end of file