added implementation for distinguishing extension and dispatch (no de…

…ep recursive lookup)
jesyspa · Aug 5, 2024 · f77bb1d · f77bb1d
1 parent f0cfa46
commit f77bb1d
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 7 deletions.
diff --git a/...ation/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt b/...ation/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt
@@ -40,7 +40,7 @@ interface MethodConversionContext : ProgramConversionContext {
     fun resolveLocal(name: Name): VariableEmbedding
     fun registerLocalProperty(symbol: FirPropertySymbol)
     fun registerLocalVariable(symbol: FirVariableSymbol<*>)
-    fun resolveReceiver(): ExpEmbedding?
+    fun resolveReceiver(isExtension: Boolean): ExpEmbedding?
 
     fun <R> withScopeImpl(scopeDepth: Int, action: () -> R): R
     fun addLoopIdentifier(labelName: String, index: Int)

diff --git a/...-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt b/...-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt
@@ -62,7 +62,8 @@ class MethodConverter(
         paramResolver.tryResolveParameter(name) ?: parent?.resolveParameter(name)
         ?: throw IllegalArgumentException("Parameter $name not found in scope.")
 
-    override fun resolveReceiver(): ExpEmbedding? = paramResolver.tryResolveReceiver() ?: parent?.resolveReceiver()
+    override fun resolveReceiver(isExtension: Boolean): ExpEmbedding? =
+        paramResolver.tryResolveReceiver(isExtension) ?: parent?.resolveReceiver(isExtension)
 
     override val defaultResolvedReturnTarget = paramResolver.defaultResolvedReturnTarget
     override fun resolveNamedReturnTarget(sourceName: String): ReturnTarget? {

diff --git a/...erification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt b/...erification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt
@@ -19,7 +19,7 @@ import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
  */
 interface ParameterResolver {
     fun tryResolveParameter(name: Name): ExpEmbedding?
-    fun tryResolveReceiver(): ExpEmbedding?
+    fun tryResolveReceiver(isExtension: Boolean): ExpEmbedding?
 
     val sourceName: String?
     val defaultResolvedReturnTarget: ReturnTarget
@@ -36,7 +36,9 @@ class RootParameterResolver(
 ) : ParameterResolver {
     private val parameters = signature.params.associateBy { it.name }
     override fun tryResolveParameter(name: Name): ExpEmbedding? = parameters[name.embedParameterName()]
-    override fun tryResolveReceiver() = signature.run { dispatchReceiver ?: extensionReceiver }
+    override fun tryResolveReceiver(isExtension: Boolean) =
+        if (isExtension) signature.run { extensionReceiver }
+        else signature.run { dispatchReceiver }
 }
 
 class InlineParameterResolver(
@@ -45,5 +47,7 @@ class InlineParameterResolver(
     override val defaultResolvedReturnTarget: ReturnTarget,
 ) : ParameterResolver {
     override fun tryResolveParameter(name: Name): ExpEmbedding? = substitutions[name]
-    override fun tryResolveReceiver(): ExpEmbedding? = substitutions[ExtraSpecialNames.D_THIS] ?: substitutions[ExtraSpecialNames.E_THIS]
+    override fun tryResolveReceiver(isExtension: Boolean): ExpEmbedding? =
+        if (isExtension) substitutions[ExtraSpecialNames.E_THIS]
+        else substitutions[ExtraSpecialNames.D_THIS]
 }
diff --git a/...ication/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt b/...ication/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt
@@ -15,6 +15,7 @@ import org.jetbrains.kotlin.fir.expressions.impl.FirElseIfTrueCondition
 import org.jetbrains.kotlin.fir.references.FirThisReference
 import org.jetbrains.kotlin.fir.references.toResolvedSymbol
 import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol
+import org.jetbrains.kotlin.fir.symbols.impl.FirClassSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirFunctionSymbol
 import org.jetbrains.kotlin.fir.types.coneType
 import org.jetbrains.kotlin.fir.types.resolvedType
@@ -285,7 +286,12 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         thisReceiverExpression: FirThisReceiverExpression,
         data: StmtConversionContext,
     ): ExpEmbedding {
-        return data.resolveReceiver()
+        val isExtensionReceiver = when (thisReceiverExpression.calleeReference.boundSymbol) {
+            is FirClassSymbol<*> -> false
+            is FirFunctionSymbol<*> -> true
+            else -> error("Unsupported receiver expression type.")
+        }
+        return data.resolveReceiver(isExtensionReceiver)
             ?: throw IllegalArgumentException("Can't resolve the 'this' receiver since the function does not have one.")
     }
 

diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/multiple_receivers.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/multiple_receivers.kt
@@ -1,10 +1,16 @@
 import kotlin.contracts.ExperimentalContracts
 import kotlin.contracts.contract
 import org.jetbrains.kotlin.formver.plugin.AlwaysVerify
+import org.jetbrains.kotlin.formver.plugin.verify
 import org.jetbrains.kotlin.formver.plugin.NeverConvert
 
 class ClassWithExtension(val delta: Int) {
-    fun Int.<!VIPER_TEXT!>applyDelta<!>() = this + delta
+    @AlwaysVerify
+    fun Int.<!VIPER_TEXT!>applyDelta<!>() {
+        val withoutLabels = this + delta
+        val withLabels = this@ClassWithExtension.delta + this@applyDelta
+        verify(withoutLabels == withLabels)
+    }
     fun <!VIPER_TEXT!>returnDelta<!>() = delta
 }