From 71915600f5563f0877de21aa66b0678f4a8d18c5 Mon Sep 17 00:00:00 2001 From: Yifan Song Date: Thu, 25 Jul 2024 19:55:07 +0200 Subject: [PATCH] More on uniqueness context checking --- .../formver/UniqueDeclarationChecker.kt | 46 ++++++- .../org/jetbrains/kotlin/formver/UniqueCFA.kt | 117 ++++++++++++------ .../kotlin/formver/UniqueCheckerContext.kt | 5 +- .../kotlin/formver/UniqueCheckerData.kt | 12 +- 4 files changed, 129 insertions(+), 51 deletions(-) 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 918cb1f266f94..af1e942b5ebbc 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,7 @@ 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.cfg.* import org.jetbrains.kotlin.fir.resolve.dfa.controlFlowGraph class UniqueDeclarationChecker(private val session: FirSession, private val config: PluginConfiguration) : @@ -21,7 +22,8 @@ class UniqueDeclarationChecker(private val session: FirSession, private val conf if (!config.checkUniqueness) return val errorCollector = ErrorCollector() try { - val uniqueCheckerContext = UniqueCheckerData(session, config, errorCollector) + val assignArgumentPos = declaration.controlFlowGraphReference?.controlFlowGraph?.usedForAssignOrCall() ?: emptyMap() + val uniqueCheckerContext = UniqueCheckerData(session, config, errorCollector, assignArgumentPos = assignArgumentPos) val cfaChecker = UniqueCFA(uniqueCheckerContext) declaration.controlFlowGraphReference?.controlFlowGraph?.let { cfaChecker.analyze(it, reporter, context) } @@ -30,4 +32,46 @@ class UniqueDeclarationChecker(private val session: FirSession, private val conf reporter.reportOn(declaration.source, PluginErrors.UNIQUENESS_VIOLATION, error, context) } } + + // This function resolve nodes use as arguments or rhs for assignments + // When an node is used in this case, we need to track alias or uniqueness level information in this.data + private fun ControlFlowGraph.usedForAssignOrCall(): Map, CFGNode<*>> { + val result: MutableMap, CFGNode<*>> = mutableMapOf() + + fun resolveArgument(node: CFGNode<*>): CFGNode<*> { + var curNode: CFGNode<*> = node + var exitNode = node + while (exitNode !is FunctionCallArgumentsExitNode) { + if (exitNode.previousNodes.isEmpty()) { + TODO("Throw correctly") + } + exitNode = exitNode.previousNodes[0] + if (exitNode.owner != node.owner) return exitNode + } + while (true) { + if (curNode.previousNodes.isEmpty()) { + TODO("Throw correctly") + } + curNode = curNode.previousNodes[0] + if (curNode is ExitNodeMarker && curNode is FunctionCallArgumentsExitNode) + curNode = resolveArgument(curNode) + else if (curNode is EnterNodeMarker) break + else result[curNode] = exitNode + } + return curNode + } + + for (node in nodes) { + if (node is FunctionCallArgumentsExitNode) { + resolveArgument(node) + } + if (node is VariableDeclarationNode || node is VariableAssignmentNode) { + if (node.previousNodes.isEmpty()) { + TODO("Throw correctly") + } + result[node.previousNodes[0]] = node + } + } + return result + } } \ No newline at end of file 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 15618c12e6dd5..a171ee3912817 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 @@ -14,47 +14,43 @@ 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.FirResolvedNamedReference import org.jetbrains.kotlin.fir.references.symbol import org.jetbrains.kotlin.fir.resolve.dfa.cfg.* import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol -sealed class LastOrPath { - data object LastNode : LastOrPath() - data class Path(val path: FirVariableSymbol) : LastOrPath() -} - -class UniqueCFA(private val data: UniqueCheckerData) : FirControlFlowChecker(MppCheckerKind.Common) { +class UniqueCFA(private val data: UniqueCheckerContext) : FirControlFlowChecker(MppCheckerKind.Common) { override fun analyze(graph: ControlFlowGraph, reporter: DiagnosticReporter, context: CheckerContext) { graph.traverseToFixedPoint(UniqueInfoCollector(data)) } - private class UniqueInfoCollector(private val data: UniqueCheckerData) : - PathAwareControlFlowGraphVisitor>() { + private class UniqueInfoCollector(private val data: UniqueCheckerContext) : + PathAwareControlFlowGraphVisitor, Set>() { + override fun mergeInfo( - a: ControlFlowInfo>, - b: ControlFlowInfo>, + a: ControlFlowInfo, Set>, + b: ControlFlowInfo, Set>, node: CFGNode<*>, - ): ControlFlowInfo> { + ): ControlFlowInfo, Set> { // TODO: No implemented yet, for now just return from one branch return a } - override fun visitNode( - node: CFGNode<*>, - data: PathAwareControlFlowInfo>, - ): PathAwareControlFlowInfo> { - // Check if node is a FirVariable - - // TODO: I should remove something here - val dataForNode = data.transformValues { it.remove(LastOrPath.LastNode) } - return super.visitNode(node, dataForNode) + 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 visitFunctionEnterNode( node: FunctionEnterNode, - data: PathAwareControlFlowInfo>, - ): PathAwareControlFlowInfo> { + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { val declaration = node.fir // construct context and start control flow analysis @@ -64,8 +60,8 @@ class UniqueCFA(private val data: UniqueCheckerData) : FirControlFlowChecker(Mpp } val valueParameters = declaration.valueParameters.associate { - Pair>( - LastOrPath.Path(it.symbol), + Pair, Set>( + it.symbol, if (it.hasAnnotation(this.data.uniqueId, this.data.session)) { setOf(UniqueLevel.Unique) } else { @@ -73,32 +69,75 @@ class UniqueCFA(private val data: UniqueCheckerData) : FirControlFlowChecker(Mpp } ) }.toPersistentMap() - return super.visitFunctionEnterNode(node, persistentMapOf(Pair(NormalPath, valueParameters))) + return persistentMapOf(Pair(NormalPath, valueParameters)) } override fun visitVariableDeclarationNode( node: VariableDeclarationNode, - data: PathAwareControlFlowInfo>, - ): PathAwareControlFlowInfo> { - val dataForNode = super.visitVariableDeclarationNode(node, data) + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val dataForNode = data val lSymbol = node.fir.symbol - val rhsUniqueLevel = data[NormalPath]?.get(LastOrPath.LastNode) ?: setOf(UniqueLevel.Shared) - val temp = dataForNode.transformValues { it.put(LastOrPath.Path(lSymbol), rhsUniqueLevel) } - .transformValues { it.remove(LastOrPath.LastNode) } - return temp + if (this.data.nodeUniqueLevel.contains(node)) { + val nodeUniqueLevel = this.data.nodeUniqueLevel[node] ?: emptyMap() + if (nodeUniqueLevel.isEmpty() || nodeUniqueLevel.all { (_, k) -> k.isEmpty() }) { + return dataForNode.transformValues { it.put(lSymbol, setOf(UniqueLevel.Shared)) } + } + return dataForNode.transformValues { it.put(lSymbol, nodeUniqueLevel.firstNotNullOf { (_, v) -> v }) } + } else { + return dataForNode.transformValues { it.put(lSymbol, setOf(UniqueLevel.Shared)) } + } + } + + override fun visitVariableAssignmentNode( + node: VariableAssignmentNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + // FIXME: this function might be totally wrong, variable assignment might be totally different from variable declaration + val dataForNode = data + val lSymbol = node.fir.lValue.toResolvedCallableSymbol(this.data.session) as FirVariableSymbol + if (this.data.nodeUniqueLevel.contains(node)) { + val nodeUniqueLevel = this.data.nodeUniqueLevel[node] ?: emptyMap() + if (nodeUniqueLevel.isEmpty() || nodeUniqueLevel.all { (_, k) -> k.isEmpty() }) { + return dataForNode.transformValues { it.put(lSymbol, setOf(UniqueLevel.Shared)) } + } + return dataForNode.transformValues { it.put(lSymbol, nodeUniqueLevel.firstNotNullOf { (_, v) -> v }) } + } else { + return dataForNode.transformValues { it.put(lSymbol, setOf(UniqueLevel.Shared)) } + } + } + + override fun visitFunctionCallArgumentsExitNode( + node: FunctionCallArgumentsExitNode, + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + // TODO: this is where function call parameter checking should happen + if (this.data.nodeUniqueLevel.contains(node)) { + println("$node: ${this.data.nodeUniqueLevel[node]}") + } + return data } override fun visitQualifiedAccessNode( node: QualifiedAccessNode, - data: PathAwareControlFlowInfo> - ): PathAwareControlFlowInfo> { - val dataForNode = visitNode(node, data) - if (node.fir.calleeReference is FirResolvedNamedReference) { + data: PathAwareControlFlowInfo, Set>, + ): PathAwareControlFlowInfo, Set> { + val dataForNode = data + if (node.fir.calleeReference is FirResolvedNamedReference && this.data.assignArgumentPos.contains(node)) { + // When accessed node is used for assignment and is a path + // When accessed node is a unique variable need to change its uniqueness level to Top + // In all cases store the unique level + val usePos: CFGNode<*> = this.data.assignArgumentPos[node]!! val callee = node.fir.calleeReference.symbol as FirVariableSymbol - val rhsUniqueLevel = data[NormalPath]?.get(LastOrPath.Path(callee)) ?: setOf(UniqueLevel.Shared) - return data.transformValues { it.put(LastOrPath.LastNode, rhsUniqueLevel) } + val rhsUniqueLevel = data[NormalPath]?.get(callee) ?: setOf(UniqueLevel.Shared) + if (this.data.nodeUniqueLevel[usePos].isNullOrEmpty()) { + this.data.nodeUniqueLevel[usePos] = mapOf(node to rhsUniqueLevel).toMutableMap() + } else { + this.data.nodeUniqueLevel[usePos]?.set(node, rhsUniqueLevel) + } + return dataForNode } - return super.visitQualifiedAccessNode(node, data) + return dataForNode } } } \ 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 f6ea7d0e1b965..0af0e46b83d74 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,6 +7,7 @@ package org.jetbrains.kotlin.formver import org.jetbrains.kotlin.fir.FirSession import org.jetbrains.kotlin.fir.declarations.FirDeclaration +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.CFGNode import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol import org.jetbrains.kotlin.name.ClassId @@ -15,8 +16,8 @@ interface UniqueCheckerContext { val errorCollector: ErrorCollector val session: FirSession val uniqueId: ClassId + val nodeUniqueLevel: MutableMap, MutableMap, Set>> + val assignArgumentPos: Map, CFGNode<*>> fun resolveUniqueAnnotation(declaration: FirDeclaration): UniqueLevel - fun getPathUniqueLevel(path: FirPropertySymbol): Set - fun setPathUniqueLevel(path: FirPropertySymbol, level: 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 acda9310e6dfc..30dc6c3d08e7e 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 @@ -8,6 +8,7 @@ package org.jetbrains.kotlin.formver import org.jetbrains.kotlin.fir.FirSession import org.jetbrains.kotlin.fir.declarations.FirDeclaration import org.jetbrains.kotlin.fir.declarations.hasAnnotation +import org.jetbrains.kotlin.fir.resolve.dfa.cfg.CFGNode import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol import org.jetbrains.kotlin.name.ClassId import org.jetbrains.kotlin.name.FqName @@ -17,7 +18,8 @@ class UniqueCheckerData( override val session: FirSession, override val config: PluginConfiguration, override val errorCollector: ErrorCollector, - public val pathUniqueTable: MutableMap> = mutableMapOf(), + override val nodeUniqueLevel: MutableMap, MutableMap, Set>> = mutableMapOf(), + override val assignArgumentPos: Map, CFGNode<*>> ) : UniqueCheckerContext { private fun getAnnotationId(name: String): ClassId = @@ -32,12 +34,4 @@ class UniqueCheckerData( } return UniqueLevel.Shared } - - override fun getPathUniqueLevel(path: FirPropertySymbol): Set { - return this.pathUniqueTable[path] ?: setOf(UniqueLevel.Shared) - } - - override fun setPathUniqueLevel(path: FirPropertySymbol, level: UniqueLevel) { - this.pathUniqueTable[path] = setOf(level) - } } \ No newline at end of file