From 85731bfc67fcc3a8d54db9b819de75f9e29d0815 Mon Sep 17 00:00:00 2001 From: GrigoriiSolnyshkin <89751176+GrigoriiSolnyshkin@users.noreply.github.com> Date: Mon, 15 Jul 2024 13:09:10 +0300 Subject: [PATCH] Generic Run Analogues (#218) With this pull request functions analogous to Kotlin `run` successfully compile to Viper if they're inline. For instance, call to ```inline fun T.copiedRun(block: T.() -> R): R = block()``` will be correctly inlined. Support for real stdlib `run` and other notable extension functions (`also`, `let` etc.) as well as the cases with multiple possible receivers will be implemented in future PRs. --- .../org/jetbrains/kotlin/formver/FirUtils.kt | 9 +- .../conversion/MethodConversionContext.kt | 1 + .../formver/conversion/MethodConverter.kt | 2 + .../formver/conversion/ParameterResolver.kt | 5 + .../formver/conversion/ProgramConverter.kt | 2 +- .../conversion/StmtConversionContext.kt | 5 +- .../conversion/StmtConversionVisitor.kt | 16 +- .../embeddings/callables/CallableEmbedding.kt | 8 +- .../callables/InlineNamedFunction.kt | 3 +- .../callables/SpecialKotlinFunction.kt | 23 - .../embeddings/expression/LambdaExp.kt | 15 +- .../custom_run_functions.fir.diag.txt | 507 ++++++++++++++++++ .../good_contracts/custom_run_functions.kt | 122 +++++ .../no_contracts/scope_functions.fir.diag.txt | 11 - .../no_contracts/scope_functions.kt | 8 - ...FormVerPluginDiagnosticsTestGenerated.java | 14 +- 16 files changed, 685 insertions(+), 66 deletions(-) create mode 100644 plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt create mode 100644 plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt delete mode 100644 plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.fir.diag.txt delete mode 100644 plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.kt diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/FirUtils.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/FirUtils.kt index b2b0bf815c42f..746c044827ac1 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/FirUtils.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/FirUtils.kt @@ -38,7 +38,14 @@ val FirPropertySymbol.isCustom: Boolean } val FirFunctionCall.functionCallArguments: List - 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 get() = this.resolvedContractDescription?.effects ?: emptyList() val KtSourceElement?.asPosition: Position diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt index eb9b86aba1449..d1cd8bdfe7c0f 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConversionContext.kt +++ b/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 withScopeImpl(scopeDepth: Int, action: () -> R): R fun addLoopIdentifier(labelName: String, index: Int) diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt index 3b116294ecf3a..d1d8a7236353a 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/MethodConverter.kt +++ b/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) diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt index 58cc203854146..e3e77c9a91873 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ParameterResolver.kt +++ b/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] } \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt index 4589f7a099846..4d7af58d59f33 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt @@ -373,7 +373,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) diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt index 66b4a831fabd3..afe2600881ce3 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionContext.kt +++ b/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( diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt index 5afde264ca712..356611e266728 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt +++ b/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() 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, @@ -271,9 +282,10 @@ object StmtConversionVisitor : FirVisitor() 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, diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/CallableEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/CallableEmbedding.kt index 2736f3707220c..d7cbcbba35abd 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/CallableEmbedding.kt +++ b/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, ctx: StmtConversionContext, -): ExpEmbedding { - return args.zip(formalArgTypes) - .map { (arg, type) -> arg.withType(type) } - .let { insertCallImpl(it, ctx) } - .withType(returnType) -} \ No newline at end of file +): ExpEmbedding = insertCallImpl(args, ctx) \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/InlineNamedFunction.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/InlineNamedFunction.kt index 6842789ef4ea1..bfbde320cee88 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/InlineNamedFunction.kt +++ b/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, 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) } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt index 1137f12ae0804..b80361853ce33 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt +++ b/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 = listOf("kotlin") - override val name: String = "run" - - override val receiverType: TypeEmbedding? = null - override val paramTypes: List = - listOf(FunctionTypeEmbedding(CallableSignatureData(null, emptyList(), NullableTypeEmbedding(AnyTypeEmbedding)))) - override val returnType: TypeEmbedding = NullableTypeEmbedding(AnyTypeEmbedding) - - override fun insertCallImpl( - args: List, - 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() } } \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt index 27686e692c7f2..950b47be1aac3 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt +++ b/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, 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 diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt new file mode 100644 index 0000000000000..f88f0476b7539 --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt @@ -0,0 +1,507 @@ +/custom_run_functions.kt:(1058,1064): info: Generated Viper text for useRun: +method global$fun_useRun$fun_take$$return$T_Boolean() returns (ret$0: Ref) + ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret$0), dom$RuntimeType$boolType()) + ensures dom$RuntimeType$boolFromRef(ret$0) == true +{ + var local0$one: Ref + var local0$two: Ref + var local0$three: Ref + var local0$genericResult: Ref + var anonymous$9: Ref + var ret$1: Ref + var anonymous$10: Ref + var ret$2: Ref + var anonymous$11: Ref + var ret$3: Ref + var anonymous$12: Ref + var ret$4: Ref + var anonymous$13: Ref + var ret$5: Ref + var anonymous$14: Ref + var ret$6: Ref + var local0$capturedResult: Ref + var anonymous$15: Ref + var ret$7: Ref + var anonymous$16: Ref + var ret$8: Ref + var anonymous$17: Ref + var ret$9: Ref + var anonymous$18: Ref + var ret$10: Ref + var anonymous$19: Ref + var ret$11: Ref + var anonymous$20: Ref + var ret$12: Ref + var local0$intResult: Ref + var anonymous$21: Ref + var ret$13: Ref + var ret$14: Ref + var anonymous$22: Ref + var ret$15: Ref + var ret$16: Ref + var anonymous$23: Ref + var ret$17: Ref + var ret$18: Ref + var local0$doubleIntRunResult: Ref + var anonymous$24: Ref + var ret$19: Ref + var anonymous$0: Ref + var ret$21: Ref + var anonymous$1: Ref + var ret$20: Ref + var local0$genericReceiverResult: Ref + var anonymous$25: Ref + var ret$22: Ref + var anonymous$2: Ref + var anonymous$26: Ref + var ret$23: Ref + var anonymous$27: Ref + var anonymous$28: Ref + var anonymous$29: Ref + var anonymous$30: Ref + var anonymous$31: Ref + var anonymous$32: Ref + var anonymous$33: Ref + var anonymous$34: Ref + var anonymous$35: Ref + var anonymous$36: Ref + local0$one := dom$RuntimeType$intToRef(1) + local0$two := dom$RuntimeType$intToRef(2) + local0$three := dom$RuntimeType$intToRef(3) + ret$2 := dom$RuntimeType$intToRef(1) + goto label$ret$2 + label label$ret$2 + anonymous$10 := ret$2 + ret$1 := anonymous$10 + goto label$ret$1 + label label$ret$1 + anonymous$9 := ret$1 + ret$4 := dom$RuntimeType$intToRef(2) + goto label$ret$4 + label label$ret$4 + anonymous$12 := ret$4 + ret$3 := anonymous$12 + goto label$ret$3 + label label$ret$3 + anonymous$11 := ret$3 + ret$6 := dom$RuntimeType$intToRef(3) + goto label$ret$6 + label label$ret$6 + anonymous$14 := ret$6 + ret$5 := anonymous$14 + goto label$ret$5 + label label$ret$5 + anonymous$13 := ret$5 + local0$genericResult := dom$RuntimeType$boolToRef(special$plusInts(anonymous$9, + anonymous$11) == + anonymous$13) + ret$8 := dom$RuntimeType$intToRef(1) + goto label$ret$8 + label label$ret$8 + anonymous$16 := ret$8 + ret$7 := anonymous$16 + goto label$ret$7 + label label$ret$7 + anonymous$15 := ret$7 + ret$10 := dom$RuntimeType$intToRef(2) + goto label$ret$10 + label label$ret$10 + anonymous$18 := ret$10 + ret$9 := anonymous$18 + goto label$ret$9 + label label$ret$9 + anonymous$17 := ret$9 + ret$12 := dom$RuntimeType$intToRef(3) + goto label$ret$12 + label label$ret$12 + anonymous$20 := ret$12 + ret$11 := anonymous$20 + goto label$ret$11 + label label$ret$11 + anonymous$19 := ret$11 + local0$capturedResult := dom$RuntimeType$boolToRef(special$plusInts(anonymous$15, + anonymous$17) == + anonymous$19) + ret$14 := dom$RuntimeType$intToRef(1) + goto label$ret$14 + label label$ret$14 + ret$13 := ret$14 + goto label$ret$13 + label label$ret$13 + anonymous$21 := ret$13 + ret$16 := dom$RuntimeType$intToRef(2) + goto label$ret$16 + label label$ret$16 + ret$15 := ret$16 + goto label$ret$15 + label label$ret$15 + anonymous$22 := ret$15 + ret$18 := dom$RuntimeType$intToRef(3) + goto label$ret$18 + label label$ret$18 + ret$17 := ret$18 + goto label$ret$17 + label label$ret$17 + anonymous$23 := ret$17 + local0$intResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$21) + + dom$RuntimeType$intFromRef(anonymous$22) == + dom$RuntimeType$intFromRef(anonymous$23)) + anonymous$0 := dom$RuntimeType$intToRef(1) + ret$20 := special$plusInts(anonymous$0, dom$RuntimeType$intToRef(1)) + goto label$ret$20 + label label$ret$20 + anonymous$1 := ret$20 + ret$21 := special$plusInts(anonymous$1, dom$RuntimeType$intToRef(1)) + goto label$ret$21 + label label$ret$21 + ret$19 := ret$21 + goto label$ret$19 + label label$ret$19 + anonymous$24 := ret$19 + local0$doubleIntRunResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$24) == + 3) + anonymous$2 := dom$RuntimeType$intToRef(1) + ret$23 := special$plusInts(anonymous$2, dom$RuntimeType$intToRef(2)) + goto label$ret$23 + label label$ret$23 + anonymous$26 := ret$23 + ret$22 := anonymous$26 + goto label$ret$22 + label label$ret$22 + anonymous$25 := ret$22 + local0$genericReceiverResult := dom$RuntimeType$boolToRef(anonymous$25 == + dom$RuntimeType$intToRef(3)) + if (dom$RuntimeType$boolFromRef(local0$intResult)) { + anonymous$36 := local0$genericResult + } else { + anonymous$36 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$36)) { + anonymous$35 := local0$capturedResult + } else { + anonymous$35 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$35)) { + var ret$24: Ref + var local24$result: Ref + var ret$25: Ref + ret$25 := special$plusInts(dom$RuntimeType$intToRef(1), dom$RuntimeType$intToRef(2)) + goto label$ret$25 + label label$ret$25 + local24$result := ret$25 + ret$24 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local24$result) == + 3) + goto label$ret$24 + label label$ret$24 + anonymous$34 := ret$24 + } else { + anonymous$34 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$34)) { + var anonymous$37: Ref + var ret$26: Ref + var local26$result: Ref + var ret$27: Ref + ret$27 := dom$RuntimeType$intToRef(4) + goto label$ret$27 + label label$ret$27 + local26$result := ret$27 + ret$26 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local26$result) == + 3) + goto label$ret$26 + label label$ret$26 + anonymous$37 := ret$26 + anonymous$33 := special$notBool(anonymous$37) + } else { + anonymous$33 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$33)) { + var ret$28: Ref + var local28$result: Ref + var ret$29: Ref + var anonymous$3: Ref + anonymous$3 := dom$RuntimeType$intToRef(1) + ret$29 := special$plusInts(anonymous$3, dom$RuntimeType$intToRef(2)) + goto label$ret$29 + label label$ret$29 + local28$result := ret$29 + ret$28 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local28$result) == + 3) + goto label$ret$28 + label label$ret$28 + anonymous$32 := ret$28 + } else { + anonymous$32 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$32)) { + var anonymous$38: Ref + var ret$30: Ref + var local30$result: Ref + var ret$31: Ref + var anonymous$4: Ref + anonymous$4 := dom$RuntimeType$intToRef(1) + ret$31 := anonymous$4 + goto label$ret$31 + label label$ret$31 + local30$result := ret$31 + ret$30 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local30$result) == + 3) + goto label$ret$30 + label label$ret$30 + anonymous$38 := ret$30 + anonymous$31 := special$notBool(anonymous$38) + } else { + anonymous$31 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$31)) { + var ret$32: Ref + var local32$result: Ref + var ret$33: Ref + var anonymous$5: Ref + anonymous$5 := dom$RuntimeType$intToRef(1) + ret$33 := special$plusInts(anonymous$5, dom$RuntimeType$intToRef(2)) + goto label$ret$33 + label label$ret$33 + local32$result := ret$33 + ret$32 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local32$result) == + 3) + goto label$ret$32 + label label$ret$32 + anonymous$30 := ret$32 + } else { + anonymous$30 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$30)) { + var ret$34: Ref + var local34$result: Ref + var ret$35: Ref + var anonymous$6: Ref + anonymous$6 := dom$RuntimeType$intToRef(1) + ret$35 := special$plusInts(anonymous$6, dom$RuntimeType$intToRef(2)) + goto label$ret$35 + label label$ret$35 + local34$result := ret$35 + ret$34 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local34$result) == + 3) + goto label$ret$34 + label label$ret$34 + anonymous$29 := ret$34 + } else { + anonymous$29 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$29)) { + var ret$36: Ref + var local36$result: Ref + var ret$38: Ref + var anonymous$8: Ref + var ret$37: Ref + var anonymous$7: Ref + anonymous$7 := dom$RuntimeType$intToRef(1) + ret$37 := special$plusInts(anonymous$7, dom$RuntimeType$intToRef(1)) + goto label$ret$37 + label label$ret$37 + anonymous$8 := ret$37 + ret$38 := special$plusInts(anonymous$8, dom$RuntimeType$intToRef(1)) + goto label$ret$38 + label label$ret$38 + local36$result := ret$38 + ret$36 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local36$result) == + 3) + goto label$ret$36 + label label$ret$36 + anonymous$28 := ret$36 + } else { + anonymous$28 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$28)) { + anonymous$27 := local0$doubleIntRunResult + } else { + anonymous$27 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$27)) { + ret$0 := local0$genericReceiverResult + } else { + ret$0 := dom$RuntimeType$boolToRef(false)} + goto label$ret$0 + label label$ret$0 +} + +/custom_run_functions.kt:(2226,2241): info: Generated Viper text for complexScenario: +method global$fun_complexScenario$fun_take$T_Boolean$return$T_Boolean(local$arg: Ref) + returns (ret$0: Ref) + ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret$0), dom$RuntimeType$boolType()) + ensures dom$RuntimeType$boolFromRef(ret$0) == true ==> + dom$RuntimeType$boolFromRef(local$arg) + ensures dom$RuntimeType$boolFromRef(ret$0) == false ==> + !dom$RuntimeType$boolFromRef(local$arg) +{ + var anonymous$5: Ref + var ret$1: Ref + inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(local$arg), dom$RuntimeType$boolType()) + if (dom$RuntimeType$boolFromRef(local$arg)) { + var anonymous$6: Ref + var ret$2: Ref + var anonymous$7: Ref + var ret$3: Ref + var local5$result: Ref + var ret$4: Ref + var anonymous$0: Ref + var anonymous$8: Ref + var ret$5: Ref + var anonymous$9: Ref + var ret$6: Ref + var ret$7: Ref + var ret$9: Ref + var anonymous$1: Ref + var ret$8: Ref + anonymous$0 := dom$RuntimeType$intToRef(1) + ret$8 := special$plusInts(anonymous$0, dom$RuntimeType$intToRef(1)) + goto label$ret$8 + label label$ret$8 + anonymous$1 := ret$8 + ret$9 := special$plusInts(anonymous$1, dom$RuntimeType$intToRef(1)) + goto label$ret$9 + label label$ret$9 + ret$7 := ret$9 + goto label$ret$7 + label label$ret$7 + ret$6 := ret$7 + goto label$ret$6 + label label$ret$6 + anonymous$9 := ret$6 + ret$5 := anonymous$9 + goto label$ret$5 + label label$ret$5 + anonymous$8 := ret$5 + ret$4 := anonymous$8 + goto label$ret$4 + label label$ret$4 + local5$result := ret$4 + ret$3 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local5$result) == + 3) + goto label$ret$3 + label label$ret$3 + anonymous$7 := ret$3 + ret$2 := anonymous$7 + goto label$ret$2 + label label$ret$2 + anonymous$6 := ret$2 + ret$1 := anonymous$6 + } else { + var anonymous$10: Ref + anonymous$10 := dom$RuntimeType$nullValue() + ret$1 := anonymous$10 + } + goto label$ret$1 + label label$ret$1 + anonymous$5 := ret$1 + if (anonymous$5 != dom$RuntimeType$nullValue()) { + ret$0 := anonymous$5 + } else { + var anonymous$11: Ref + var ret$10: Ref + var anonymous$12: Ref + var ret$11: Ref + var ret$12: Ref + var local15$result: Ref + var ret$13: Ref + var anonymous$2: Ref + var anonymous$13: Ref + var ret$14: Ref + var anonymous$14: Ref + var ret$15: Ref + var anonymous$15: Ref + var ret$16: Ref + var anonymous$3: Ref + var anonymous$16: Ref + var ret$17: Ref + var anonymous$17: Ref + var ret$18: Ref + var anonymous$4: Ref + var anonymous$18: Ref + var ret$19: Ref + anonymous$2 := dom$RuntimeType$intToRef(1) + anonymous$3 := special$plusInts(anonymous$2, dom$RuntimeType$intToRef(1)) + anonymous$4 := special$plusInts(anonymous$3, dom$RuntimeType$intToRef(1)) + ret$19 := special$plusInts(anonymous$4, dom$RuntimeType$intToRef(1)) + goto label$ret$19 + label label$ret$19 + anonymous$18 := ret$19 + ret$18 := anonymous$18 + goto label$ret$18 + label label$ret$18 + anonymous$17 := ret$18 + ret$17 := anonymous$17 + goto label$ret$17 + label label$ret$17 + anonymous$16 := ret$17 + ret$16 := anonymous$16 + goto label$ret$16 + label label$ret$16 + anonymous$15 := ret$16 + ret$15 := anonymous$15 + goto label$ret$15 + label label$ret$15 + anonymous$14 := ret$15 + ret$14 := anonymous$14 + goto label$ret$14 + label label$ret$14 + anonymous$13 := ret$14 + ret$13 := anonymous$13 + goto label$ret$13 + label label$ret$13 + local15$result := ret$13 + ret$12 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local15$result) == + 3) + goto label$ret$12 + label label$ret$12 + ret$11 := ret$12 + goto label$ret$11 + label label$ret$11 + anonymous$12 := ret$11 + ret$10 := anonymous$12 + goto label$ret$10 + label label$ret$10 + anonymous$11 := ret$10 + ret$0 := anonymous$11 + } + goto label$ret$0 + label label$ret$0 +} + +/custom_run_functions.kt:(3305,3320): info: Generated Viper text for testCustomClass: +field public$backing_field_member: Ref + +method class_CustomClass$constructor$fun_take$$return$T_class_global$class_CustomClass() + returns (ret: Ref) + ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret), dom$RuntimeType$T_class_global$class_CustomClass()) + ensures acc(T_class_global$class_CustomClass(ret), wildcard) + + +method global$fun_testCustomClass$fun_take$$return$T_Boolean() + returns (ret$0: Ref) + ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret$0), dom$RuntimeType$boolType()) + ensures dom$RuntimeType$boolFromRef(ret$0) == true +{ + var local0$custom: Ref + var anonymous$0: Ref + var ret$1: Ref + var anonymous$1: Ref + var ret$2: Ref + var anonymous$2: Ref + var ret$3: Ref + var anonymous$3: Ref + var ret$4: Ref + local0$custom := class_CustomClass$constructor$fun_take$$return$T_class_global$class_CustomClass() + unfold acc(T_class_global$class_CustomClass(local0$custom), wildcard) + ret$2 := local0$custom.public$backing_field_member + goto label$ret$2 + label label$ret$2 + anonymous$1 := ret$2 + ret$1 := anonymous$1 + goto label$ret$1 + label label$ret$1 + anonymous$0 := ret$1 + unfold acc(T_class_global$class_CustomClass(local0$custom), wildcard) + ret$4 := local0$custom.public$backing_field_member + goto label$ret$4 + label label$ret$4 + anonymous$3 := ret$4 + ret$3 := anonymous$3 + goto label$ret$3 + label label$ret$3 + anonymous$2 := ret$3 + ret$0 := dom$RuntimeType$boolToRef(anonymous$0 == anonymous$2) + goto label$ret$0 + label label$ret$0 +} diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt new file mode 100644 index 0000000000000..fa3c014af5bbe --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt @@ -0,0 +1,122 @@ +import kotlin.contracts.ExperimentalContracts +import kotlin.contracts.contract +import org.jetbrains.kotlin.formver.plugin.NeverConvert + +@NeverConvert +public inline fun copiedRun(block: () -> R): R = block() + +@NeverConvert +public inline fun T.copiedRun(block: T.() -> R): R = block() + +@NeverConvert +public inline fun intRun(block: () -> Int): Int = block() + +@NeverConvert +public inline fun equalsThree(block: () -> Int): Boolean { + val result = block() + return result == 3 +} + +@NeverConvert +public inline fun equalsThreeParametrized(block: (Int) -> Int): Boolean { + val result = block(1) + return result == 3 +} + +@NeverConvert +public inline fun equalsThreeExtension(block: Int.() -> Int): Boolean { + val result = 1.block() + return result == 3 +} + +@NeverConvert +public inline fun doubleEqualsThree(block: Int.() -> Int): Boolean { + val result = 1.block().block() + return result == 3 +} + +@NeverConvert +public inline fun Int.doubleIntRun(block: Int.() -> Int): Int = block().block() + +@OptIn(ExperimentalContracts::class) +public fun useRun(): Boolean { + contract { + returns(true) + } + val one = 1 + val two = 2 + val three = 3 + val genericResult = copiedRun { 1 } + copiedRun { 2 } == copiedRun { 3 } + val capturedResult = copiedRun { 1 } + copiedRun { 2 } == copiedRun { 3 } + val intResult = intRun { 1 } + intRun { 2 } == intRun { 3 } +// val stdlibResult = run { 1 } + run { 2 } == run { 3 } + val doubleIntRunResult = 1.doubleIntRun { plus(1) } == 3 + val genericReceiverResult = 1.copiedRun { plus(2) } == 3 + + return intResult + && genericResult +// && stdlibResult + && capturedResult + && equalsThree { 1 + 2 } + && !equalsThree { 4 } + && equalsThreeParametrized { it + 2 } + && !equalsThreeParametrized { arg -> arg } + && equalsThreeExtension { this + 2 } + && equalsThreeExtension { plus(2) } + && doubleEqualsThree { plus(1) } + && doubleIntRunResult + && genericReceiverResult +} + +@NeverConvert +public inline fun Boolean.ifTrue(block: () -> T?): T? = if (this) block() else null + +@OptIn(ExperimentalContracts::class) +public fun complexScenario(arg: Boolean): Boolean { + contract { + returns(true) implies arg + returns(false) implies !arg + } + + return arg.ifTrue { + equalsThreeParametrized { + it.copiedRun { + plus(1) // unused + plus(1) // unused + doubleIntRun { // receiver is `it` (== 1 in `equalsThreeParametrized`) + plus(1) // unused + plus(1) + } + } + } + } ?: copiedRun { // run with no receiver + equalsThreeExtension { + copiedRun { // run with receiver + plus(1).copiedRun { // receiver is `this` + plus(1).copiedRun { + plus(1) + } + } + } + } + } +} + +class CustomClass { + val member: Int = 42 + + @NeverConvert + inline fun memberRun(block: CustomClass.() -> T): T = block() +} + +@NeverConvert +inline fun CustomClass.extensionRun(block: CustomClass.() -> T): T = block() + +@OptIn(ExperimentalContracts::class) +fun testCustomClass(): Boolean { + contract { + returns(true) + } + val custom = CustomClass() + return custom.memberRun { member } == custom.extensionRun { member } +} \ No newline at end of file diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.fir.diag.txt deleted file mode 100644 index a24e0c4157820..0000000000000 --- a/plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.fir.diag.txt +++ /dev/null @@ -1,11 +0,0 @@ -/scope_functions.kt:(23,29): info: Generated Viper text for useRun: -method global$fun_useRun$fun_take$$return$T_Unit() returns (ret$0: Ref) - ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret$0), dom$RuntimeType$unitType()) -{ - var local0$x: Ref - var ret$1: Ref - ret$0 := dom$RuntimeType$unitValue() - local0$x := dom$RuntimeType$intToRef(0) - label label$ret$1 - label label$ret$0 -} diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.kt b/plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.kt deleted file mode 100644 index 475d4e7fd3b18..0000000000000 --- a/plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.kt +++ /dev/null @@ -1,8 +0,0 @@ -// NEVER_VALIDATE - -fun useRun() { - val x: Int - run { - x = 0 - } -} 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 1dff34739f3f4..4854b9eec27b5 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 @@ -6,8 +6,8 @@ package org.jetbrains.kotlin.formver.plugin.runners; import com.intellij.testFramework.TestDataPath; -import org.jetbrains.kotlin.test.TestMetadata; import org.jetbrains.kotlin.test.util.KtTestUtil; +import org.jetbrains.kotlin.test.TestMetadata; import org.junit.jupiter.api.Nested; import org.junit.jupiter.api.Test; @@ -127,6 +127,12 @@ public void testCustom_list() { runTest("plugins/formal-verification/testData/diagnostics/good_contracts/custom_list.kt"); } + @Test + @TestMetadata("custom_run_functions.kt") + public void testCustom_run_functions() { + runTest("plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt"); + } + @Test @TestMetadata("inline_correctness.kt") public void testInline_correctness() { @@ -227,12 +233,6 @@ public void testFunction_overloading() { runTest("plugins/formal-verification/testData/diagnostics/no_contracts/function_overloading.kt"); } - @Test - @TestMetadata("scope_functions.kt") - public void testScope_functions() { - runTest("plugins/formal-verification/testData/diagnostics/no_contracts/scope_functions.kt"); - } - @Test @TestMetadata("shadowing.kt") public void testShadowing() {