Generic Run Analogues

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/FirUtils.kt

@@ -32,7 +32,14 @@ val FirPropertySymbol.isCustom: Boolean
     }
 
 val FirFunctionCall.functionCallArguments: List<FirExpression>
-    get() = listOfNotNull(dispatchReceiver) + argumentList.arguments
+    get() {
+        val receiverArg = when {
+            dispatchReceiver != null -> dispatchReceiver
+            extensionReceiver != null -> extensionReceiver
+            else -> null
+        }
+        return listOfNotNull(receiverArg) + argumentList.arguments
+    }
 val FirFunctionSymbol<*>.effects: List<FirEffectDeclaration>
     get() = this.resolvedContractDescription?.effects ?: emptyList()
 val KtSourceElement?.asPosition: Position

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt

@@ -40,6 +40,7 @@ interface MethodConversionContext : ProgramConversionContext {
     fun resolveLocal(name: Name): VariableEmbedding
     fun registerLocalProperty(symbol: FirPropertySymbol)
     fun registerLocalVariable(symbol: FirVariableSymbol<*>)
+    fun resolveReceiver(): ExpEmbedding?
 
     fun <R> withScopeImpl(scopeDepth: Int, action: () -> R): R
     fun addLoopIdentifier(labelName: String, index: Int)

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt

@@ -62,6 +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 val defaultResolvedReturnTarget = paramResolver.defaultResolvedReturnTarget
     override fun resolveNamedReturnTarget(sourceName: String): ReturnTarget? {
         return paramResolver.resolveNamedReturnTarget(sourceName) ?: parent?.resolveNamedReturnTarget(sourceName)

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt

@@ -9,6 +9,7 @@ import org.jetbrains.kotlin.formver.embeddings.callables.FunctionSignature
 import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
 import org.jetbrains.kotlin.formver.names.embedParameterName
 import org.jetbrains.kotlin.name.Name
+import org.jetbrains.kotlin.name.SpecialNames
 import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
 
 /**
@@ -18,6 +19,7 @@ import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
  */
 interface ParameterResolver {
     fun tryResolveParameter(name: Name): ExpEmbedding?
+    fun tryResolveReceiver(): ExpEmbedding?
 
     val sourceName: String?
     val defaultResolvedReturnTarget: ReturnTarget
@@ -33,7 +35,9 @@ class RootParameterResolver(
     override val defaultResolvedReturnTarget: ReturnTarget,
 ) : ParameterResolver {
     private val parameters = signature.params.associateBy { it.name }
+    private val receiver = signature.receiver
     override fun tryResolveParameter(name: Name): ExpEmbedding? = parameters[name.embedParameterName()]
+    override fun tryResolveReceiver() = receiver
 }
 
 class InlineParameterResolver(
@@ -42,4 +46,5 @@ class InlineParameterResolver(
     override val defaultResolvedReturnTarget: ReturnTarget,
 ) : ParameterResolver {
     override fun tryResolveParameter(name: Name): ExpEmbedding? = substitutions[name]
+    override fun tryResolveReceiver(): ExpEmbedding? = substitutions[SpecialNames.THIS]
 }

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt

@@ -357,7 +357,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
                 this,
                 signature,
                 RootParameterResolver(this, signature, signature.sourceName, returnTarget),
-                scopeIndexProducer.getFresh(),
+                scopeDepth = scopeIndexProducer.getFresh(),
             )
         val stmtCtx = StmtConverter(methodCtx)
         val body = stmtCtx.convert(firBody)

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt

@@ -130,7 +130,8 @@ fun StmtConversionContext.embedPropertyAccess(accessExpression: FirPropertyAcces
                 else -> embedLocalProperty(calleeSymbol)
             }
         }
-        else -> error("Property access symbol $calleeSymbol has unsupported type.")
+        else ->
+            error("Property access symbol $calleeSymbol has unsupported type.")
     }
 
 fun StmtConversionContext.getInlineFunctionCallArgs(
@@ -165,7 +166,7 @@ fun StmtConversionContext.insertInlineFunctionCall(
     val methodCtxFactory = MethodContextFactory(
         calleeSignature,
         InlineParameterResolver(subs, returnTargetName, returnTarget),
-        parentCtx,
+        parent = parentCtx,
     )
     return withMethodCtx(methodCtxFactory) {
         Block(

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt

@@ -8,8 +8,11 @@ package org.jetbrains.kotlin.formver.conversion
 import org.jetbrains.kotlin.contracts.description.LogicOperationKind
 import org.jetbrains.kotlin.fir.FirElement
 import org.jetbrains.kotlin.fir.declarations.FirProperty
+import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction
+import org.jetbrains.kotlin.fir.declarations.evaluateAs
 import org.jetbrains.kotlin.fir.expressions.*
 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.FirFunctionSymbol
@@ -23,6 +26,7 @@ import org.jetbrains.kotlin.formver.embeddings.callables.FullNamedFunctionSignat
 import org.jetbrains.kotlin.formver.embeddings.callables.insertCall
 import org.jetbrains.kotlin.formver.embeddings.expression.*
 import org.jetbrains.kotlin.formver.functionCallArguments
+import org.jetbrains.kotlin.name.Name
 import org.jetbrains.kotlin.text
 import org.jetbrains.kotlin.types.ConstantValueKind
 
@@ -70,6 +74,13 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
             else -> handleUnimplementedElement("Constant Expression of type ${constExpression.kind} is not yet implemented.", data)
         }
 
+    override fun visitIntegerLiteralOperatorCall(
+        integerLiteralOperatorCall: FirIntegerLiteralOperatorCall,
+        data: StmtConversionContext
+    ): ExpEmbedding {
+        return visitFunctionCall(integerLiteralOperatorCall, data)
+    }
+
     override fun visitWhenSubjectExpression(
         whenSubjectExpression: FirWhenSubjectExpression,
         data: StmtConversionContext,
@@ -119,6 +130,11 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         return propertyAccess.getValue(data)
     }
 
+    override fun visitSimpleFunction(simpleFunction: FirSimpleFunction, data: StmtConversionContext): ExpEmbedding {
+        data.embedFunctionSignature(simpleFunction.symbol)
+        return UnitLit
+    }
+
     override fun visitEqualityOperatorCall(
         equalityOperatorCall: FirEqualityOperatorCall,
         data: StmtConversionContext,
@@ -271,9 +287,10 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
     override fun visitThisReceiverExpression(
         thisReceiverExpression: FirThisReceiverExpression,
         data: StmtConversionContext,
-    ): ExpEmbedding =
-        data.signature.receiver
+    ): ExpEmbedding {
+        return data.resolveReceiver()
             ?: throw IllegalArgumentException("Can't resolve the 'this' receiver since the function does not have one.")
+    }
 
     override fun visitTypeOperatorCall(
         typeOperatorCall: FirTypeOperatorCall,
@@ -284,7 +301,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         return when (typeOperatorCall.operation) {
             FirOperation.IS -> Is(argument, conversionType)
             FirOperation.NOT_IS -> Not(Is(argument, conversionType))
-            FirOperation.AS -> Cast(argument, conversionType).withAccessAndProvenInvariants()
+            FirOperation.AS -> argument.withNewTypeAccessAndProvenInvariants(conversionType)
             FirOperation.SAFE_AS -> SafeCast(argument, conversionType).withAccessAndProvenInvariants()
             else -> handleUnimplementedElement("Can't embed type operator ${typeOperatorCall.operation}.", data)
         }

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/CallableEmbedding.kt

@@ -7,7 +7,6 @@ package org.jetbrains.kotlin.formver.embeddings.callables
 
 import org.jetbrains.kotlin.formver.conversion.StmtConversionContext
 import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
-import org.jetbrains.kotlin.formver.embeddings.expression.withType
 
 /**
  * Kotlin entity that can be called.
@@ -21,9 +20,4 @@ interface CallableEmbedding : CallableSignature {
 fun CallableEmbedding.insertCall(
     args: List<ExpEmbedding>,
     ctx: StmtConversionContext,
-): ExpEmbedding {
-    return args.zip(formalArgTypes)
-        .map { (arg, type) -> arg.withType(type) }
-        .let { insertCallImpl(it, ctx) }
-        .withType(returnType)
-}
+): ExpEmbedding = insertCallImpl(args, ctx)

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/InlineNamedFunction.kt

@@ -11,6 +11,7 @@ import org.jetbrains.kotlin.formver.conversion.StmtConversionContext
 import org.jetbrains.kotlin.formver.conversion.insertInlineFunctionCall
 import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
+import org.jetbrains.kotlin.name.SpecialNames
 
 class InlineNamedFunction(
     val signature: FullNamedFunctionSignature,
@@ -21,7 +22,7 @@ class InlineNamedFunction(
         args: List<ExpEmbedding>,
         ctx: StmtConversionContext,
     ): ExpEmbedding {
-        val paramNames = symbol.valueParameterSymbols.map { it.name }
+        val paramNames = listOfNotNull(receiver?.let { SpecialNames.THIS }) + symbol.valueParameterSymbols.map { it.name }
         return ctx.insertInlineFunctionCall(signature, paramNames, args, firBody, signature.sourceName)
     }
 

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt

@@ -117,28 +117,6 @@ object KotlinBooleanNotFunctionImplementation : KotlinBooleanSpecialFunction() {
         Not(args[0])
 }
 
-object KotlinRunSpecialFunction : SpecialKotlinFunction {
-    override val packageName: List<String> = listOf("kotlin")
-    override val name: String = "run"
-
-    override val receiverType: TypeEmbedding? = null
-    override val paramTypes: List<TypeEmbedding> =
-        listOf(FunctionTypeEmbedding(CallableSignatureData(null, emptyList(), NullableTypeEmbedding(AnyTypeEmbedding))))
-    override val returnType: TypeEmbedding = NullableTypeEmbedding(AnyTypeEmbedding)
-
-    override fun insertCallImpl(
-        args: List<ExpEmbedding>,
-        ctx: StmtConversionContext,
-    ): ExpEmbedding {
-        val lambda = when (val arg = args[0].ignoringCastsAndMetaNodes()) {
-            is LambdaExp -> arg
-            else -> error("kotlin.run must be called with a lambda argument at the moment")
-        }
-
-        return lambda.insertCallImpl(listOf(), ctx)
-    }
-}
-
 /**
  * Represents the `verify` function defined in `org.jetbrains.kotlin.formver.plugin`.
  */
@@ -164,6 +142,5 @@ object SpecialKotlinFunctions {
         KotlinIntTimesFunctionImplementation,
         KotlinIntDivFunctionImplementation,
         KotlinBooleanNotFunctionImplementation,
-        KotlinRunSpecialFunction,
     ).associateBy { it.embedName() }
 }

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt

@@ -17,6 +17,7 @@ import org.jetbrains.kotlin.formver.embeddings.callables.asData
 import org.jetbrains.kotlin.formver.embeddings.expression.debug.PlaintextLeaf
 import org.jetbrains.kotlin.formver.embeddings.expression.debug.TreeView
 import org.jetbrains.kotlin.formver.linearization.LinearizationContext
+import org.jetbrains.kotlin.name.SpecialNames
 
 class LambdaExp(
     val signature: FunctionSignature,
@@ -34,9 +35,17 @@ class LambdaExp(
         args: List<ExpEmbedding>,
         ctx: StmtConversionContext,
     ): ExpEmbedding {
-        val inlineBody = function.body ?: throw IllegalArgumentException("Lambda $function has a null body")
-        val paramNames = function.valueParameters.map { it.name }
-        return ctx.insertInlineFunctionCall(signature, paramNames, args, inlineBody, ctx.signature.sourceName, parentCtx)
+        val inlineBody = function.body ?: throw IllegalArgumentException("Lambda $function has a null body.")
+        val nonReceiverParamNames = function.valueParameters.map { it.name }
+        val receiverParamNames = if (function.receiverParameter != null) listOf(SpecialNames.THIS) else emptyList()
+        return ctx.insertInlineFunctionCall(
+            signature,
+            receiverParamNames + nonReceiverParamNames,
+            args,
+            inlineBody,
+            ctx.signature.sourceName,
+            parentCtx,
+        )
     }
 
     override val debugTreeView: TreeView