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..d9549f3b7ab9d --- /dev/null +++ b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt @@ -0,0 +1,161 @@ +/* + * 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.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 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, + setOf(this.context.resolveUniqueAnnotation(it)) + ) + } + 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 rhsUniqueLevel = data.getUniqueLevel(context.getTopExprPathUnique()) + return dataForNode.transformValues { it.put(lSymbol, rhsUniqueLevel) } + } + + override fun visitVariableAssignmentNode( + node: VariableAssignmentNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val dataForNode = visitNode(node, data) + val lSymbol = node.fir.lValue.toResolvedCallableSymbol(context.session) + val rhsUniqueLevel = data.getUniqueLevel(context.getTopExprPathUnique()) + return dataForNode.transformValues { it.put(lSymbol as FirVariableSymbol, rhsUniqueLevel) } + } + + @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 argUniqueLevel = this.context.resolveUniqueAnnotation(param) + 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}") + } + } + 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 + } + + @OptIn(SymbolInternals::class) + override fun visitFunctionCallExitNode( + node: FunctionCallExitNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val uniqueLevel = mutableSetOf() + val symbol = node.fir.calleeReference.symbol + if (symbol == null) { + uniqueLevel.add(UniqueLevel.Shared) + } else { + uniqueLevel.add(this.context.resolveUniqueAnnotation(symbol.fir)) + } + 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/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..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 @@ -7,11 +7,35 @@ 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 + +/** + * 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() interface UniqueCheckerContext { val config: PluginConfiguration val errorCollector: ErrorCollector 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/UniqueChecker.kt b/plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCheckerData.kt similarity index 77% 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..a3ca65a561d1c 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,12 +12,12 @@ 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)) @@ -31,4 +31,10 @@ class UniqueChecker( } 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 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"); + } } } }