From e4fc535fb1259ce5170b26d9c3c0a65d1c2ff1df Mon Sep 17 00:00:00 2001 From: Yifan Song Date: Tue, 30 Jul 2024 15:12:14 +0200 Subject: [PATCH 1/7] Basic cfa checker for assignment and function call --- .../formver/UniqueDeclarationChecker.kt | 7 +- .../formver.uniqueness/build.gradle.kts | 1 + .../org/jetbrains/kotlin/formver/UniqueCFA.kt | 171 ++++++++++++++++++ .../kotlin/formver/UniqueCheckVisitor.kt | 68 ------- .../kotlin/formver/UniqueCheckerContext.kt | 10 + ...{UniqueChecker.kt => UniqueCheckerData.kt} | 8 +- .../direct_pass_shared_to_unique.fir.diag.txt | 2 +- .../good_unique/unique_to_unique.kt | 13 ++ ...FormVerPluginDiagnosticsTestGenerated.java | 6 + 9 files changed, 211 insertions(+), 75 deletions(-) create mode 100644 plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt delete mode 100644 plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckVisitor.kt rename plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/{UniqueChecker.kt => UniqueCheckerData.kt} (86%) create mode 100644 plugins/formal-verification/testData/diagnostics/uniqueness/good_unique/unique_to_unique.kt diff --git a/plugins/formal-verification/formver.plugin/src/org/jetbrains/kotlin/formver/UniqueDeclarationChecker.kt b/plugins/formal-verification/formver.plugin/src/org/jetbrains/kotlin/formver/UniqueDeclarationChecker.kt index ce77204a4a7c8..f136c01a7ffb6 100644 --- a/plugins/formal-verification/formver.plugin/src/org/jetbrains/kotlin/formver/UniqueDeclarationChecker.kt +++ b/plugins/formal-verification/formver.plugin/src/org/jetbrains/kotlin/formver/UniqueDeclarationChecker.kt @@ -12,6 +12,8 @@ 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.text class UniqueDeclarationChecker(private val session: FirSession, private val config: PluginConfiguration) : FirSimpleFunctionChecker(MppCheckerKind.Common) { @@ -20,9 +22,10 @@ class UniqueDeclarationChecker(private val session: FirSession, private val conf if (!config.checkUniqueness) return val errorCollector = ErrorCollector() try { - val uniqueCheckerContext = UniqueChecker(session, config, errorCollector) - declaration.accept(UniquenessCheckExceptionWrapper, uniqueCheckerContext) + val cfaChecker = UniqueCFA(UniqueCheckerData(session, config, errorCollector)) + declaration.controlFlowGraphReference?.controlFlowGraph?.let { cfaChecker.analyze(it, reporter, context) } } catch (e: Exception) { + errorCollector.addErrorInfo("... while checking uniqueness level for ${declaration.source.text}") val error = errorCollector.formatErrorWithInfos(e.message ?: "No message provided") reporter.reportOn(declaration.source, PluginErrors.UNIQUENESS_VIOLATION, error, context) } diff --git a/plugins/formal-verification/formver.uniqueness/build.gradle.kts b/plugins/formal-verification/formver.uniqueness/build.gradle.kts index b4b92e9a76dfa..958468ee0561e 100644 --- a/plugins/formal-verification/formver.uniqueness/build.gradle.kts +++ b/plugins/formal-verification/formver.uniqueness/build.gradle.kts @@ -5,6 +5,7 @@ plugins { dependencies { compileOnly(project(":kotlin-formver-compiler-plugin.common")) + compileOnly(project(":compiler:fir:checkers")) compileOnly(project(":compiler:fir:cones")) compileOnly(project(":compiler:fir:tree")) compileOnly(project(":compiler:fir:plugin-utils")) diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt new file mode 100644 index 0000000000000..f8f23f0e3b2fb --- /dev/null +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt @@ -0,0 +1,171 @@ +/* + * 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 + +import org.jetbrains.kotlin.diagnostics.DiagnosticReporter +import org.jetbrains.kotlin.fir.analysis.cfa.util.* +import org.jetbrains.kotlin.fir.analysis.checkers.MppCheckerKind +import org.jetbrains.kotlin.fir.analysis.checkers.cfa.FirControlFlowChecker +import org.jetbrains.kotlin.fir.analysis.checkers.context.CheckerContext +import org.jetbrains.kotlin.fir.declarations.FirVariable +import org.jetbrains.kotlin.fir.declarations.hasAnnotation +import org.jetbrains.kotlin.fir.expressions.toResolvedCallableSymbol +import org.jetbrains.kotlin.fir.references.symbol +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.* +import org.jetbrains.kotlin.fir.symbols.SymbolInternals +import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol +import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol +import org.jetbrains.kotlin.text +import org.jetbrains.kotlin.utils.addToStdlib.popLast + +class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker(MppCheckerKind.Common) { + override fun analyze(graph: ControlFlowGraph, reporter: DiagnosticReporter, context: CheckerContext) { + graph.traverseToFixedPoint(UniqueInfoCollector(this.data)) + } + + private class UniqueInfoCollector(private val context: UniqueCheckerContext) : + PathAwareControlFlowGraphVisitor, Set>() { + + override fun mergeInfo( + a: ControlFlowInfo, Set>, + b: ControlFlowInfo, Set>, + node: CFGNode<*>, + ): ControlFlowInfo, Set> { + // TODO: No implemented yet, for now just return from one branch + return a + } + + override fun visitEdge( + from: CFGNode<*>, + to: CFGNode<*>, + metadata: Edge, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val dataForEdge = super.visitEdge(from, to, metadata, data) + return dataForEdge + } + + override fun visitNode( + node: CFGNode<*>, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + if (node is EnterNodeMarker) { + context.uniqueStack.add(ArrayDeque()) + } else if (node is ExitNodeMarker) { + context.uniqueStack.popLast().lastOrNull()?.let { context.uniqueStack.last().add(it) } + } + return data + } + + override fun visitFunctionEnterNode( + node: FunctionEnterNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val dataForNode = visitNode(node, data) + val declaration = node.fir + + // construct context and start control flow analysis + if (declaration.receiverParameter != null) { + TODO("Ignore receiver for now, not sure how to convert it into property symbol yet") + } + val valueParameters = + declaration.valueParameters.associate { + Pair, Set>( + it.symbol, + if (it.hasAnnotation(this.context.uniqueId, this.context.session)) { + setOf(UniqueLevel.Unique) + } else { + setOf(UniqueLevel.Shared) + } + ) + }.toMap() + return dataForNode.transformValues { it.putAll(valueParameters) } + } + + override fun visitVariableDeclarationNode( + node: VariableDeclarationNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val dataForNode = visitNode(node, data) + val lSymbol = node.fir.symbol + if (node.fir.initializer == null) { + return dataForNode.transformValues { it.put(lSymbol, setOf(UniqueLevel.Shared)) } + } + val rhsUnique = when (val last = context.uniqueStack.last().last()) { + is Level -> last.level + is Path -> dataForNode[NormalPath]?.get(last.symbol) ?: setOf(UniqueLevel.Shared) + } + return dataForNode.transformValues { it.put(lSymbol, rhsUnique) } + } + + override fun visitVariableAssignmentNode( + node: VariableAssignmentNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val dataForNode = visitNode(node, data) + val lSymbol = node.fir.lValue.toResolvedCallableSymbol(context.session) + val rhsUnique = when (val last = context.uniqueStack.last().last()) { + is Level -> last.level + is Path -> dataForNode[NormalPath]?.get(last.symbol) ?: setOf(UniqueLevel.Shared) + } + return dataForNode.transformValues { it.put(lSymbol as FirVariableSymbol, rhsUnique) } + } + + @OptIn(SymbolInternals::class) + override fun visitFunctionCallArgumentsExitNode( + node: FunctionCallArgumentsExitNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + // TODO: this is where function call parameter checking should happen + // Here do not call visitNode + val params = (node.fir.toResolvedCallableSymbol() as FirFunctionSymbol<*>).fir.valueParameters + val argumentAliasOrUnique: MutableList = mutableListOf() + for (i in params.indices) { + argumentAliasOrUnique.add(context.uniqueStack.last().popLast()) + } + // FIXME: might not get annotation in this way + params.zip(argumentAliasOrUnique).forEach { (param, varUnique) -> + val argShouldUnique = param.hasAnnotation(context.uniqueId, context.session) + val passedUnique: Set = when (varUnique) { + is Path -> data[NormalPath]?.get(varUnique.symbol) ?: setOf(UniqueLevel.Shared) + is Level -> varUnique.level + } + // TODO: more general comparison + if (argShouldUnique && passedUnique.any { it != UniqueLevel.Unique }) { + throw IllegalArgumentException("uniqueness level not match ${param.source.text}") + } + } + return data + } + + override fun visitQualifiedAccessNode( + node: QualifiedAccessNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val dataForNode = visitNode(node, data) + val callee = node.fir.calleeReference.symbol as FirVariableSymbol + context.uniqueStack.last().add(Path(callee)) + return dataForNode + } + + override fun visitFunctionCallExitNode( + node: FunctionCallExitNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val uniqueLevel = mutableSetOf() + // FIXME: might not be able to get the annotation for function declaration in this way + if (node.fir.hasAnnotation(this.context.uniqueId, this.context.session)) { + uniqueLevel.add(UniqueLevel.Unique) + } else { + uniqueLevel.add(UniqueLevel.Shared) + } + context.uniqueStack.last().add(Level(uniqueLevel)) + + // Function call does not change context + return data + } + } +} \ No newline at end of file diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckVisitor.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckVisitor.kt deleted file mode 100644 index fa88fd8772971..0000000000000 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckVisitor.kt +++ /dev/null @@ -1,68 +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 - -import org.jetbrains.kotlin.fir.FirElement -import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction -import org.jetbrains.kotlin.fir.expressions.FirBlock -import org.jetbrains.kotlin.fir.expressions.FirFunctionCall -import org.jetbrains.kotlin.fir.expressions.arguments -import org.jetbrains.kotlin.fir.expressions.toResolvedCallableSymbol -import org.jetbrains.kotlin.fir.symbols.SymbolInternals -import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol -import org.jetbrains.kotlin.fir.visitors.FirVisitor -import org.jetbrains.kotlin.text - -object UniqueCheckVisitor : FirVisitor() { - override fun visitElement(element: FirElement, data: UniqueCheckerContext): UniqueLevel = UniqueLevel.Shared - - override fun visitSimpleFunction(simpleFunction: FirSimpleFunction, data: UniqueCheckerContext): UniqueLevel { - simpleFunction.body?.accept(this, data) - // Function definition don't have to return a unique level - return UniqueLevel.Shared - } - - override fun visitBlock(block: FirBlock, data: UniqueCheckerContext): UniqueLevel { - block.statements.forEach { statement -> - when (statement) { - is FirFunctionCall -> { - statement.accept(this, data) - } - } - } - return UniqueLevel.Shared - } - - @OptIn(SymbolInternals::class) - override fun visitFunctionCall(functionCall: FirFunctionCall, data: UniqueCheckerContext): UniqueLevel { - // To keep is 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) } - // Skip merge of context for now - val arguments = functionCall.arguments - arguments.forEachIndexed { index, argument -> - val requiredUnique = requiredUniqueLevels[index] - if (requiredUnique == UniqueLevel.Unique && visitExpression(argument, data) == UniqueLevel.Shared) { - throw IllegalArgumentException("uniqueness level not match ${argument.source.text}") - } - } - - val callee = functionCall.toResolvedCallableSymbol()?.fir as FirSimpleFunction - return data.resolveUniqueAnnotation(callee) - } -} - -object UniquenessCheckExceptionWrapper : FirVisitor() { - override fun visitElement(element: FirElement, data: UniqueCheckerContext): UniqueLevel { - try { - return element.accept(UniqueCheckVisitor, data) - } catch (e: Exception) { - data.errorCollector.addErrorInfo("... while checking uniqueness level for ${element.source.text}") - throw e - } - } -} diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt index ec2b90bb059ab..90cca32e58d61 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt @@ -7,11 +7,21 @@ package org.jetbrains.kotlin.formver import org.jetbrains.kotlin.fir.FirSession import org.jetbrains.kotlin.fir.declarations.FirDeclaration +import org.jetbrains.kotlin.fir.declarations.FirVariable +import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol +import org.jetbrains.kotlin.name.ClassId + +// TODO: find a better name for it +sealed class PathUnique +data class Path(val symbol: FirVariableSymbol) : PathUnique() +data class Level(val level: Set) : PathUnique() interface UniqueCheckerContext { val config: PluginConfiguration val errorCollector: ErrorCollector val session: FirSession + val uniqueId: ClassId + val uniqueStack: ArrayDeque> fun resolveUniqueAnnotation(declaration: FirDeclaration): UniqueLevel } diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueChecker.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt similarity index 86% rename from plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueChecker.kt rename to plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt index 6a71bd78d4ee2..566f80d62a1ec 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueChecker.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt @@ -12,17 +12,17 @@ import org.jetbrains.kotlin.name.ClassId import org.jetbrains.kotlin.name.FqName import org.jetbrains.kotlin.name.Name -class UniqueChecker( +class UniqueCheckerData( override val session: FirSession, override val config: PluginConfiguration, override val errorCollector: ErrorCollector, -) : - UniqueCheckerContext { + override val uniqueStack: ArrayDeque> = ArrayDeque(), +) : UniqueCheckerContext { private fun getAnnotationId(name: String): ClassId = ClassId(FqName.fromSegments(listOf("org", "jetbrains", "kotlin", "formver", "plugin")), Name.identifier(name)) - private val uniqueId: ClassId + override val uniqueId: ClassId get() = getAnnotationId("Unique") override fun resolveUniqueAnnotation(declaration: FirDeclaration): UniqueLevel { diff --git a/plugins/formal-verification/testData/diagnostics/uniqueness/bad_unique/direct_pass_shared_to_unique.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/uniqueness/bad_unique/direct_pass_shared_to_unique.fir.diag.txt index 2e796f38b091f..9a91f4bdf2249 100644 --- a/plugins/formal-verification/testData/diagnostics/uniqueness/bad_unique/direct_pass_shared_to_unique.fir.diag.txt +++ b/plugins/formal-verification/testData/diagnostics/uniqueness/bad_unique/direct_pass_shared_to_unique.fir.diag.txt @@ -1,4 +1,4 @@ -/direct_pass_shared_to_unique.kt:(212,242): error: uniqueness level not match y +/direct_pass_shared_to_unique.kt:(212,242): error: uniqueness level not match @Unique x: Int ... while checking uniqueness level for fun use_f(y: Int) { f(y) } diff --git a/plugins/formal-verification/testData/diagnostics/uniqueness/good_unique/unique_to_unique.kt b/plugins/formal-verification/testData/diagnostics/uniqueness/good_unique/unique_to_unique.kt new file mode 100644 index 0000000000000..7f68c169a056a --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/uniqueness/good_unique/unique_to_unique.kt @@ -0,0 +1,13 @@ +// 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(@Unique y: Int) { + f(y) +} diff --git a/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java b/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java index 4854b9eec27b5..25ccc49ed82f3 100644 --- a/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java +++ b/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java @@ -557,6 +557,12 @@ public void testAllFilesPresentInGood_unique() { public void testShared_to_shared() { runTest("plugins/formal-verification/testData/diagnostics/uniqueness/good_unique/shared_to_shared.kt"); } + + @Test + @TestMetadata("unique_to_unique.kt") + public void testUnique_to_unique() { + runTest("plugins/formal-verification/testData/diagnostics/uniqueness/good_unique/unique_to_unique.kt"); + } } } } From 13e8a4e93dd2b800b08e4ba6466972c8e5c0cab8 Mon Sep 17 00:00:00 2001 From: Yifan Song Date: Mon, 5 Aug 2024 17:18:19 +0200 Subject: [PATCH 2/7] Remove duplicate visitEdge --- .../src/org/jetbrains/kotlin/formver/UniqueCFA.kt | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt index f8f23f0e3b2fb..6031d44d64e63 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt @@ -38,16 +38,6 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( return a } - override fun visitEdge( - from: CFGNode<*>, - to: CFGNode<*>, - metadata: Edge, - data: PathAwareControlFlowInfo, Set>, - ): PathAwareControlFlowInfo, Set> { - val dataForEdge = super.visitEdge(from, to, metadata, data) - return dataForEdge - } - override fun visitNode( node: CFGNode<*>, data: PathAwareControlFlowInfo, Set>, From 58e51b35556fa473c7af7c589f7131a32caf7aa2 Mon Sep 17 00:00:00 2001 From: Yifan Song Date: Mon, 5 Aug 2024 17:25:38 +0200 Subject: [PATCH 3/7] Comment for PathUnique --- .../org/jetbrains/kotlin/formver/UniqueCheckerContext.kt | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt index 90cca32e58d61..b9fcc39d335c3 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt @@ -11,7 +11,11 @@ import org.jetbrains.kotlin.fir.declarations.FirVariable import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol import org.jetbrains.kotlin.name.ClassId -// TODO: find a better name for it +/** + * An enum for either a variable or a unique level + * [Path] denotes a possible variable, while [Level] is for a unique level + * This type is used for the stack for control-flow visitor + */ sealed class PathUnique data class Path(val symbol: FirVariableSymbol) : PathUnique() data class Level(val level: Set) : PathUnique() From a3644a04984726bf8163a05e69c17b3f3d7752fe Mon Sep 17 00:00:00 2001 From: Yifan Song Date: Mon, 5 Aug 2024 17:33:24 +0200 Subject: [PATCH 4/7] Use resolve uniqueness level for all annotations --- .../org/jetbrains/kotlin/formver/UniqueCFA.kt | 19 ++++++++----------- .../kotlin/formver/UniqueCheckerContext.kt | 1 - .../kotlin/formver/UniqueCheckerData.kt | 2 +- 3 files changed, 9 insertions(+), 13 deletions(-) diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt index 6031d44d64e63..1b4cc8da58d15 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt @@ -65,11 +65,7 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( declaration.valueParameters.associate { Pair, Set>( it.symbol, - if (it.hasAnnotation(this.context.uniqueId, this.context.session)) { - setOf(UniqueLevel.Unique) - } else { - setOf(UniqueLevel.Shared) - } + setOf(this.context.resolveUniqueAnnotation(it)) ) }.toMap() return dataForNode.transformValues { it.putAll(valueParameters) } @@ -118,13 +114,13 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( } // FIXME: might not get annotation in this way params.zip(argumentAliasOrUnique).forEach { (param, varUnique) -> - val argShouldUnique = param.hasAnnotation(context.uniqueId, context.session) + val argUniqueLevel = this.context.resolveUniqueAnnotation(param) val passedUnique: Set = when (varUnique) { is Path -> data[NormalPath]?.get(varUnique.symbol) ?: setOf(UniqueLevel.Shared) is Level -> varUnique.level } // TODO: more general comparison - if (argShouldUnique && passedUnique.any { it != UniqueLevel.Unique }) { + if (argUniqueLevel == UniqueLevel.Unique && passedUnique.any { it != UniqueLevel.Unique }) { throw IllegalArgumentException("uniqueness level not match ${param.source.text}") } } @@ -141,16 +137,17 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( return dataForNode } + @OptIn(SymbolInternals::class) override fun visitFunctionCallExitNode( node: FunctionCallExitNode, data: PathAwareControlFlowInfo, Set>, ): PathAwareControlFlowInfo, Set> { val uniqueLevel = mutableSetOf() - // FIXME: might not be able to get the annotation for function declaration in this way - if (node.fir.hasAnnotation(this.context.uniqueId, this.context.session)) { - uniqueLevel.add(UniqueLevel.Unique) - } else { + val symbol = node.fir.calleeReference.symbol + if (symbol == null) { uniqueLevel.add(UniqueLevel.Shared) + } else { + uniqueLevel.add(this.context.resolveUniqueAnnotation(symbol.fir)) } context.uniqueStack.last().add(Level(uniqueLevel)) diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt index b9fcc39d335c3..42e46b87b4685 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt @@ -24,7 +24,6 @@ interface UniqueCheckerContext { val config: PluginConfiguration val errorCollector: ErrorCollector val session: FirSession - val uniqueId: ClassId val uniqueStack: ArrayDeque> fun resolveUniqueAnnotation(declaration: FirDeclaration): UniqueLevel diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt index 566f80d62a1ec..9e65a0929fafa 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt @@ -22,7 +22,7 @@ class UniqueCheckerData( private fun getAnnotationId(name: String): ClassId = ClassId(FqName.fromSegments(listOf("org", "jetbrains", "kotlin", "formver", "plugin")), Name.identifier(name)) - override val uniqueId: ClassId + private val uniqueId: ClassId get() = getAnnotationId("Unique") override fun resolveUniqueAnnotation(declaration: FirDeclaration): UniqueLevel { From 63da938b9583f333951f505d996df9178bd6a67b Mon Sep 17 00:00:00 2001 From: Yifan Song Date: Mon, 5 Aug 2024 17:34:00 +0200 Subject: [PATCH 5/7] remove unused import --- .../src/org/jetbrains/kotlin/formver/UniqueCFA.kt | 1 - .../src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt | 1 - 2 files changed, 2 deletions(-) diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt index 1b4cc8da58d15..43bbd4f8bebff 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt @@ -11,7 +11,6 @@ import org.jetbrains.kotlin.fir.analysis.checkers.MppCheckerKind import org.jetbrains.kotlin.fir.analysis.checkers.cfa.FirControlFlowChecker import org.jetbrains.kotlin.fir.analysis.checkers.context.CheckerContext import org.jetbrains.kotlin.fir.declarations.FirVariable -import org.jetbrains.kotlin.fir.declarations.hasAnnotation import org.jetbrains.kotlin.fir.expressions.toResolvedCallableSymbol import org.jetbrains.kotlin.fir.references.symbol import org.jetbrains.kotlin.fir.resolve.dfa.cfg.* diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt index 42e46b87b4685..e5149d437a7c7 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt @@ -9,7 +9,6 @@ import org.jetbrains.kotlin.fir.FirSession import org.jetbrains.kotlin.fir.declarations.FirDeclaration import org.jetbrains.kotlin.fir.declarations.FirVariable import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol -import org.jetbrains.kotlin.name.ClassId /** * An enum for either a variable or a unique level From 569a5ea9d3d270c4bc30aa129e3ec3ef437f2337 Mon Sep 17 00:00:00 2001 From: Yifan Song Date: Mon, 5 Aug 2024 17:38:35 +0200 Subject: [PATCH 6/7] Removed redundant toMap after associate --- .../src/org/jetbrains/kotlin/formver/UniqueCFA.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt index 43bbd4f8bebff..a0d435c736935 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt @@ -66,7 +66,7 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( it.symbol, setOf(this.context.resolveUniqueAnnotation(it)) ) - }.toMap() + } return dataForNode.transformValues { it.putAll(valueParameters) } } From ab3c1ca69f59000c6f63a596ed4d0934f77b97f8 Mon Sep 17 00:00:00 2001 From: Yifan Song Date: Mon, 5 Aug 2024 19:35:31 +0200 Subject: [PATCH 7/7] Helper functions to access stack and info --- .../org/jetbrains/kotlin/formver/UniqueCFA.kt | 34 +++++++++++-------- .../kotlin/formver/UniqueCheckerContext.kt | 12 +++++++ .../kotlin/formver/UniqueCheckerData.kt | 6 ++++ 3 files changed, 37 insertions(+), 15 deletions(-) diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt index a0d435c736935..d9549f3b7ab9d 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt @@ -79,11 +79,8 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( if (node.fir.initializer == null) { return dataForNode.transformValues { it.put(lSymbol, setOf(UniqueLevel.Shared)) } } - val rhsUnique = when (val last = context.uniqueStack.last().last()) { - is Level -> last.level - is Path -> dataForNode[NormalPath]?.get(last.symbol) ?: setOf(UniqueLevel.Shared) - } - return dataForNode.transformValues { it.put(lSymbol, rhsUnique) } + val rhsUniqueLevel = data.getUniqueLevel(context.getTopExprPathUnique()) + return dataForNode.transformValues { it.put(lSymbol, rhsUniqueLevel) } } override fun visitVariableAssignmentNode( @@ -92,11 +89,8 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( ): PathAwareControlFlowInfo, Set> { val dataForNode = visitNode(node, data) val lSymbol = node.fir.lValue.toResolvedCallableSymbol(context.session) - val rhsUnique = when (val last = context.uniqueStack.last().last()) { - is Level -> last.level - is Path -> dataForNode[NormalPath]?.get(last.symbol) ?: setOf(UniqueLevel.Shared) - } - return dataForNode.transformValues { it.put(lSymbol as FirVariableSymbol, rhsUnique) } + val rhsUniqueLevel = data.getUniqueLevel(context.getTopExprPathUnique()) + return dataForNode.transformValues { it.put(lSymbol as FirVariableSymbol, rhsUniqueLevel) } } @OptIn(SymbolInternals::class) @@ -114,10 +108,7 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( // FIXME: might not get annotation in this way params.zip(argumentAliasOrUnique).forEach { (param, varUnique) -> val argUniqueLevel = this.context.resolveUniqueAnnotation(param) - val passedUnique: Set = when (varUnique) { - is Path -> data[NormalPath]?.get(varUnique.symbol) ?: setOf(UniqueLevel.Shared) - is Level -> varUnique.level - } + val passedUnique: Set = data.getUniqueLevel(varUnique) // TODO: more general comparison if (argUniqueLevel == UniqueLevel.Unique && passedUnique.any { it != UniqueLevel.Unique }) { throw IllegalArgumentException("uniqueness level not match ${param.source.text}") @@ -148,10 +139,23 @@ class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker( } else { uniqueLevel.add(this.context.resolveUniqueAnnotation(symbol.fir)) } - context.uniqueStack.last().add(Level(uniqueLevel)) + context.pushExprPathUnique(Level(uniqueLevel)) // Function call does not change context return data } + + fun PathAwareControlFlowInfo, Set>.getUniqueLevel(pathUnique: PathUnique?): Set = + when (pathUnique) { + is Path -> this.getPathUniqueOrShared(pathUnique.symbol) + is Level -> pathUnique.level + else -> setOf(UniqueLevel.Shared) + } + + fun PathAwareControlFlowInfo, Set>.getPathUniqueOrShared( + symbol: FirVariableSymbol, + ): Set { + return this[NormalPath]?.get(symbol) ?: setOf(UniqueLevel.Shared) + } } } \ No newline at end of file diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt index e5149d437a7c7..824e20ea4719b 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerContext.kt @@ -25,5 +25,17 @@ interface UniqueCheckerContext { val session: FirSession val uniqueStack: ArrayDeque> + /** + * Resolve the annotation for borrow and uniqueness + */ fun resolveUniqueAnnotation(declaration: FirDeclaration): UniqueLevel + + /** + * Pushes the alias or unique level of the last expression onto the top of last stack. + * + * @param pathUnique the unique path to be added to the stack + */ + fun pushExprPathUnique(pathUnique: PathUnique) + + fun getTopExprPathUnique(): PathUnique? } diff --git a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt index 9e65a0929fafa..a3ca65a561d1c 100644 --- a/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt @@ -31,4 +31,10 @@ class UniqueCheckerData( } return UniqueLevel.Shared } + + override fun pushExprPathUnique(pathUnique: PathUnique) { + this.uniqueStack.last().add(pathUnique) + } + + override fun getTopExprPathUnique(): PathUnique? = this.uniqueStack.last().lastOrNull() } \ No newline at end of file