From 48aec2853a9c527da7eabd9c660811df90b3a881 Mon Sep 17 00:00:00 2001 From: Grigorii Solnyshkin Date: Mon, 24 Jun 2024 08:47:44 +0300 Subject: [PATCH 1/8] receiver for innermost lambda --- .../conversion/MethodConversionContext.kt | 1 + .../formver/conversion/MethodConverter.kt | 2 + .../formver/conversion/ParameterResolver.kt | 5 ++ .../formver/conversion/ProgramConverter.kt | 2 +- .../conversion/StmtConversionContext.kt | 2 +- .../conversion/StmtConversionVisitor.kt | 23 ++++- .../embeddings/callables/CallableEmbedding.kt | 7 +- .../embeddings/expression/LambdaExp.kt | 16 +++- .../good_contracts/generics.fir.diag.txt | 86 +++++++++++++++++++ .../diagnostics/good_contracts/generics.kt | 51 +++++++++++ ...FormVerPluginDiagnosticsTestGenerated.java | 6 ++ 11 files changed, 187 insertions(+), 14 deletions(-) create mode 100644 plugins/formal-verification/testData/diagnostics/good_contracts/generics.fir.diag.txt create mode 100644 plugins/formal-verification/testData/diagnostics/good_contracts/generics.kt 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 ed61dfe32038d..14c82284cf9f6 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 @@ -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) 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..69245e8368ee3 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 @@ -165,7 +165,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..dcab7c94af434 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, @@ -119,6 +130,11 @@ object StmtConversionVisitor : FirVisitor() 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() 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() 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) } 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..822cae2fd62ab 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 @@ -21,9 +21,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/expression/LambdaExp.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/LambdaExp.kt index 27686e692c7f2..ec63f2c4af61e 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,8 @@ 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.Name +import org.jetbrains.kotlin.name.SpecialNames class LambdaExp( val signature: FunctionSignature, @@ -34,9 +36,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/generics.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/generics.fir.diag.txt new file mode 100644 index 0000000000000..373a74b04ed80 --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/generics.fir.diag.txt @@ -0,0 +1,86 @@ +/generics.kt:(378,384): 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$genericResult: 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 + var anonymous$4: Ref + var ret$5: Ref + var anonymous$5: Ref + var ret$6: Ref + var local0$intResult: Ref + var anonymous$6: Ref + var ret$7: Ref + var ret$8: Ref + var anonymous$7: Ref + var ret$9: Ref + var ret$10: Ref + var anonymous$8: Ref + var ret$11: Ref + var ret$12: Ref + ret$2 := dom$RuntimeType$intToRef(1) + 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 + ret$4 := dom$RuntimeType$intToRef(2) + 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$6 := dom$RuntimeType$intToRef(3) + goto label$ret$6 + label label$ret$6 + anonymous$5 := ret$6 + ret$5 := anonymous$5 + goto label$ret$5 + label label$ret$5 + anonymous$4 := ret$5 + local0$genericResult := dom$RuntimeType$boolToRef(special$plusInts(anonymous$0, + anonymous$2) == + anonymous$4) + ret$8 := dom$RuntimeType$intToRef(1) + goto label$ret$8 + label label$ret$8 + ret$7 := ret$8 + goto label$ret$7 + label label$ret$7 + anonymous$6 := ret$7 + ret$10 := dom$RuntimeType$intToRef(2) + goto label$ret$10 + label label$ret$10 + ret$9 := ret$10 + goto label$ret$9 + label label$ret$9 + anonymous$7 := ret$9 + ret$12 := dom$RuntimeType$intToRef(3) + goto label$ret$12 + label label$ret$12 + ret$11 := ret$12 + goto label$ret$11 + label label$ret$11 + anonymous$8 := ret$11 + local0$intResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$6) + + dom$RuntimeType$intFromRef(anonymous$7) == + dom$RuntimeType$intFromRef(anonymous$8)) + if (dom$RuntimeType$boolFromRef(local0$intResult)) { + ret$0 := local0$genericResult + } else { + ret$0 := dom$RuntimeType$boolToRef(false)} + goto label$ret$0 + label label$ret$0 +} diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/generics.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/generics.kt new file mode 100644 index 0000000000000..446d6c0b786eb --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/generics.kt @@ -0,0 +1,51 @@ +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 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 +} + +@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 intResult = intRun { 1 } + intRun { 2 } == intRun { 3 } + val stdlibResult = run { 1 } + run { 2 } == run { 3 } + val capturedResult = run { one } + run { two } == run { three } + return intResult + && genericResult + && stdlibResult + && capturedResult + && equalsThree { 1 + 2 } + && !equalsThree { 4 } + && equalsThreeParametrized { it + 2 } + && !equalsThreeParametrized { arg -> arg } + && equalsThreeExtension { this + 2 } + && equalsThreeExtension { plus(2) } +} 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 6969336476faf..15764ad0ce9c2 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 @@ -127,6 +127,12 @@ public void testCustom_list() { runTest("plugins/formal-verification/testData/diagnostics/good_contracts/custom_list.kt"); } + @Test + @TestMetadata("generics.kt") + public void testGenerics() { + runTest("plugins/formal-verification/testData/diagnostics/good_contracts/generics.kt"); + } + @Test @TestMetadata("inline_correctness.kt") public void testInline_correctness() { From c9acc3a5f0c324b81b644ba8267e4dd1a088a62b Mon Sep 17 00:00:00 2001 From: Grigorii Solnyshkin Date: Mon, 24 Jun 2024 09:11:05 +0300 Subject: [PATCH 2/8] tests updated and renamed --- .../good_contracts/generics.fir.diag.txt | 86 ------ .../lambdas_receivers.fir.diag.txt | 254 ++++++++++++++++++ .../{generics.kt => lambdas_receivers.kt} | 0 ...FormVerPluginDiagnosticsTestGenerated.java | 12 +- 4 files changed, 260 insertions(+), 92 deletions(-) delete mode 100644 plugins/formal-verification/testData/diagnostics/good_contracts/generics.fir.diag.txt create mode 100644 plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.fir.diag.txt rename plugins/formal-verification/testData/diagnostics/good_contracts/{generics.kt => lambdas_receivers.kt} (100%) diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/generics.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/generics.fir.diag.txt deleted file mode 100644 index 373a74b04ed80..0000000000000 --- a/plugins/formal-verification/testData/diagnostics/good_contracts/generics.fir.diag.txt +++ /dev/null @@ -1,86 +0,0 @@ -/generics.kt:(378,384): 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$genericResult: 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 - var anonymous$4: Ref - var ret$5: Ref - var anonymous$5: Ref - var ret$6: Ref - var local0$intResult: Ref - var anonymous$6: Ref - var ret$7: Ref - var ret$8: Ref - var anonymous$7: Ref - var ret$9: Ref - var ret$10: Ref - var anonymous$8: Ref - var ret$11: Ref - var ret$12: Ref - ret$2 := dom$RuntimeType$intToRef(1) - 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 - ret$4 := dom$RuntimeType$intToRef(2) - 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$6 := dom$RuntimeType$intToRef(3) - goto label$ret$6 - label label$ret$6 - anonymous$5 := ret$6 - ret$5 := anonymous$5 - goto label$ret$5 - label label$ret$5 - anonymous$4 := ret$5 - local0$genericResult := dom$RuntimeType$boolToRef(special$plusInts(anonymous$0, - anonymous$2) == - anonymous$4) - ret$8 := dom$RuntimeType$intToRef(1) - goto label$ret$8 - label label$ret$8 - ret$7 := ret$8 - goto label$ret$7 - label label$ret$7 - anonymous$6 := ret$7 - ret$10 := dom$RuntimeType$intToRef(2) - goto label$ret$10 - label label$ret$10 - ret$9 := ret$10 - goto label$ret$9 - label label$ret$9 - anonymous$7 := ret$9 - ret$12 := dom$RuntimeType$intToRef(3) - goto label$ret$12 - label label$ret$12 - ret$11 := ret$12 - goto label$ret$11 - label label$ret$11 - anonymous$8 := ret$11 - local0$intResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$6) + - dom$RuntimeType$intFromRef(anonymous$7) == - dom$RuntimeType$intFromRef(anonymous$8)) - if (dom$RuntimeType$boolFromRef(local0$intResult)) { - ret$0 := local0$genericResult - } else { - ret$0 := dom$RuntimeType$boolToRef(false)} - goto label$ret$0 - label label$ret$0 -} diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.fir.diag.txt new file mode 100644 index 0000000000000..ff2a771faf9a4 --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.fir.diag.txt @@ -0,0 +1,254 @@ +/lambdas_receivers.kt:(736,742): 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$4: Ref + var ret$1: Ref + var anonymous$5: Ref + var ret$2: Ref + var anonymous$6: Ref + var ret$3: Ref + var anonymous$7: Ref + var ret$4: Ref + var anonymous$8: Ref + var ret$5: Ref + var anonymous$9: Ref + var ret$6: Ref + var local0$intResult: Ref + var anonymous$10: Ref + var ret$7: Ref + var ret$8: Ref + var anonymous$11: Ref + var ret$9: Ref + var ret$10: Ref + var anonymous$12: Ref + var ret$11: Ref + var ret$12: Ref + var local0$stdlibResult: Ref + var anonymous$13: Ref + var ret$13: Ref + var anonymous$14: Ref + var ret$14: Ref + var anonymous$15: Ref + var ret$15: Ref + var local0$capturedResult: Ref + var anonymous$16: Ref + var ret$16: Ref + var anonymous$17: Ref + var ret$17: Ref + var anonymous$18: Ref + var ret$18: Ref + var anonymous$19: Ref + var anonymous$20: Ref + var anonymous$21: Ref + var anonymous$22: Ref + var anonymous$23: Ref + var anonymous$24: Ref + var anonymous$25: Ref + var anonymous$26: 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$5 := ret$2 + ret$1 := anonymous$5 + goto label$ret$1 + label label$ret$1 + anonymous$4 := ret$1 + ret$4 := dom$RuntimeType$intToRef(2) + goto label$ret$4 + label label$ret$4 + anonymous$7 := ret$4 + ret$3 := anonymous$7 + goto label$ret$3 + label label$ret$3 + anonymous$6 := ret$3 + ret$6 := dom$RuntimeType$intToRef(3) + 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 + local0$genericResult := dom$RuntimeType$boolToRef(special$plusInts(anonymous$4, + anonymous$6) == + anonymous$8) + ret$8 := dom$RuntimeType$intToRef(1) + goto label$ret$8 + label label$ret$8 + ret$7 := ret$8 + goto label$ret$7 + label label$ret$7 + anonymous$10 := ret$7 + ret$10 := dom$RuntimeType$intToRef(2) + goto label$ret$10 + label label$ret$10 + ret$9 := ret$10 + goto label$ret$9 + label label$ret$9 + anonymous$11 := ret$9 + ret$12 := dom$RuntimeType$intToRef(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 + local0$intResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$10) + + dom$RuntimeType$intFromRef(anonymous$11) == + dom$RuntimeType$intFromRef(anonymous$12)) + ret$13 := dom$RuntimeType$intToRef(1) + goto label$ret$13 + label label$ret$13 + anonymous$13 := ret$13 + ret$14 := dom$RuntimeType$intToRef(2) + goto label$ret$14 + label label$ret$14 + anonymous$14 := ret$14 + ret$15 := dom$RuntimeType$intToRef(3) + goto label$ret$15 + label label$ret$15 + anonymous$15 := ret$15 + local0$stdlibResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$13) + + dom$RuntimeType$intFromRef(anonymous$14) == + dom$RuntimeType$intFromRef(anonymous$15)) + ret$16 := local0$one + goto label$ret$16 + label label$ret$16 + anonymous$16 := ret$16 + ret$17 := local0$two + goto label$ret$17 + label label$ret$17 + anonymous$17 := ret$17 + ret$18 := local0$three + goto label$ret$18 + label label$ret$18 + anonymous$18 := ret$18 + local0$capturedResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$16) + + dom$RuntimeType$intFromRef(anonymous$17) == + dom$RuntimeType$intFromRef(anonymous$18)) + if (dom$RuntimeType$boolFromRef(local0$intResult)) { + anonymous$26 := local0$genericResult + } else { + anonymous$26 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$26)) { + anonymous$25 := local0$stdlibResult + } else { + anonymous$25 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$25)) { + anonymous$24 := local0$capturedResult + } else { + anonymous$24 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$24)) { + var ret$19: Ref + var local19$result: Ref + var ret$20: Ref + ret$20 := special$plusInts(dom$RuntimeType$intToRef(1), dom$RuntimeType$intToRef(2)) + goto label$ret$20 + label label$ret$20 + local19$result := ret$20 + ret$19 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local19$result) == + 3) + goto label$ret$19 + label label$ret$19 + anonymous$23 := ret$19 + } else { + anonymous$23 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$23)) { + var anonymous$27: Ref + var ret$21: Ref + var local21$result: Ref + var ret$22: Ref + ret$22 := dom$RuntimeType$intToRef(4) + goto label$ret$22 + label label$ret$22 + local21$result := ret$22 + ret$21 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local21$result) == + 3) + goto label$ret$21 + label label$ret$21 + anonymous$27 := ret$21 + anonymous$22 := special$notBool(anonymous$27) + } else { + anonymous$22 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$22)) { + var ret$23: Ref + var local23$result: Ref + var ret$24: Ref + var anonymous$0: Ref + anonymous$0 := dom$RuntimeType$intToRef(1) + ret$24 := special$plusInts(anonymous$0, dom$RuntimeType$intToRef(2)) + goto label$ret$24 + label label$ret$24 + local23$result := ret$24 + ret$23 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local23$result) == + 3) + goto label$ret$23 + label label$ret$23 + anonymous$21 := ret$23 + } else { + anonymous$21 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$21)) { + var anonymous$28: Ref + var ret$25: Ref + var local25$result: Ref + var ret$26: Ref + var anonymous$1: Ref + anonymous$1 := dom$RuntimeType$intToRef(1) + ret$26 := anonymous$1 + goto label$ret$26 + label label$ret$26 + local25$result := ret$26 + ret$25 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local25$result) == + 3) + goto label$ret$25 + label label$ret$25 + anonymous$28 := ret$25 + anonymous$20 := special$notBool(anonymous$28) + } else { + anonymous$20 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$20)) { + var ret$27: Ref + var local27$result: Ref + var ret$28: Ref + var anonymous$2: Ref + anonymous$2 := dom$RuntimeType$intToRef(1) + ret$28 := special$plusInts(anonymous$2, dom$RuntimeType$intToRef(2)) + goto label$ret$28 + label label$ret$28 + local27$result := ret$28 + ret$27 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local27$result) == + 3) + goto label$ret$27 + label label$ret$27 + anonymous$19 := ret$27 + } else { + anonymous$19 := dom$RuntimeType$boolToRef(false)} + if (dom$RuntimeType$boolFromRef(anonymous$19)) { + var ret$29: Ref + var local29$result: Ref + var ret$30: Ref + var anonymous$3: Ref + anonymous$3 := dom$RuntimeType$intToRef(1) + ret$30 := special$plusInts(anonymous$3, dom$RuntimeType$intToRef(2)) + goto label$ret$30 + label label$ret$30 + local29$result := ret$30 + ret$29 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local29$result) == + 3) + goto label$ret$29 + label label$ret$29 + ret$0 := ret$29 + } else { + ret$0 := dom$RuntimeType$boolToRef(false)} + goto label$ret$0 + label label$ret$0 +} diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/generics.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt similarity index 100% rename from plugins/formal-verification/testData/diagnostics/good_contracts/generics.kt rename to plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt 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 15764ad0ce9c2..07f353f6afda6 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 @@ -127,12 +127,6 @@ public void testCustom_list() { runTest("plugins/formal-verification/testData/diagnostics/good_contracts/custom_list.kt"); } - @Test - @TestMetadata("generics.kt") - public void testGenerics() { - runTest("plugins/formal-verification/testData/diagnostics/good_contracts/generics.kt"); - } - @Test @TestMetadata("inline_correctness.kt") public void testInline_correctness() { @@ -145,6 +139,12 @@ public void testIs_type_contract() { runTest("plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.kt"); } + @Test + @TestMetadata("lambdas_receivers.kt") + public void testLambdas_receivers() { + runTest("plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt"); + } + @Test @TestMetadata("list.kt") public void testList() { From eea3f05bfe8a00edef95701de27b3d6ded805681 Mon Sep 17 00:00:00 2001 From: Grigorii Solnyshkin Date: Wed, 26 Jun 2024 09:17:46 +0300 Subject: [PATCH 3/8] fixed fir function in utils to adjust for extensions --- .../src/org/jetbrains/kotlin/formver/FirUtils.kt | 9 ++++++++- .../embeddings/callables/InlineNamedFunction.kt | 3 ++- .../diagnostics/good_contracts/lambdas_receivers.kt | 12 ++++++++++++ 3 files changed, 22 insertions(+), 2 deletions(-) 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 e085ebe07877e..b35c49ca56d5c 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 @@ -32,7 +32,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/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/testData/diagnostics/good_contracts/lambdas_receivers.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt index 446d6c0b786eb..f6cfd11afc7f4 100644 --- a/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt @@ -26,6 +26,15 @@ public inline fun equalsThreeExtension(block: Int.() -> Int): Boolean { 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 { @@ -38,6 +47,7 @@ public fun useRun(): Boolean { val intResult = intRun { 1 } + intRun { 2 } == intRun { 3 } val stdlibResult = run { 1 } + run { 2 } == run { 3 } val capturedResult = run { one } + run { two } == run { three } + val doubleIntRunResult = 1.doubleIntRun { plus(1) } == 3 return intResult && genericResult && stdlibResult @@ -48,4 +58,6 @@ public fun useRun(): Boolean { && !equalsThreeParametrized { arg -> arg } && equalsThreeExtension { this + 2 } && equalsThreeExtension { plus(2) } + && doubleEqualsThree { plus(1) } + && doubleIntRunResult } From 5bc58afe64359ac9078ab51794604b46a73fd521 Mon Sep 17 00:00:00 2001 From: Grigorii Solnyshkin Date: Wed, 26 Jun 2024 15:46:19 +0300 Subject: [PATCH 4/8] turned off support for kotlin.run + added complex testcase --- .../conversion/StmtConversionContext.kt | 3 +- .../embeddings/callables/CallableEmbedding.kt | 1 - .../callables/SpecialKotlinFunction.kt | 23 --------- .../embeddings/expression/LambdaExp.kt | 1 - .../good_contracts/lambdas_receivers.kt | 48 +++++++++++++++++-- 5 files changed, 47 insertions(+), 29 deletions(-) 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 69245e8368ee3..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( 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 822cae2fd62ab..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. 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 ec63f2c4af61e..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,7 +17,6 @@ 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.Name import org.jetbrains.kotlin.name.SpecialNames class LambdaExp( diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt index f6cfd11afc7f4..e4c7fcde464d7 100644 --- a/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt @@ -1,3 +1,5 @@ +// USE_STDLIB + import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract import org.jetbrains.kotlin.formver.plugin.NeverConvert @@ -5,6 +7,9 @@ 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() @@ -44,13 +49,15 @@ public fun useRun(): Boolean { 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 capturedResult = run { one } + run { two } == run { three } +// 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 +// && stdlibResult && capturedResult && equalsThree { 1 + 2 } && !equalsThree { 4 } @@ -60,4 +67,39 @@ public fun useRun(): Boolean { && 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) + } + } + } + } + } +} \ No newline at end of file From c0df963a283152456fa50de7a63dcbd63ea1e274 Mon Sep 17 00:00:00 2001 From: Grigorii Solnyshkin Date: Wed, 26 Jun 2024 15:59:12 +0300 Subject: [PATCH 5/8] tests updated --- .../custom_run_functions.fir.diag.txt | 460 ++++++++++++++++++ ...s_receivers.kt => custom_run_functions.kt} | 0 .../lambdas_receivers.fir.diag.txt | 254 ---------- .../no_contracts/scope_functions.fir.diag.txt | 11 - .../no_contracts/scope_functions.kt | 8 - ...FormVerPluginDiagnosticsTestGenerated.java | 20 +- 6 files changed, 467 insertions(+), 286 deletions(-) create mode 100644 plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt rename plugins/formal-verification/testData/diagnostics/good_contracts/{lambdas_receivers.kt => custom_run_functions.kt} (100%) delete mode 100644 plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.fir.diag.txt 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/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..776484fbc1277 --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.fir.diag.txt @@ -0,0 +1,460 @@ +/custom_run_functions.kt:(1073,1079): 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:(2241,2256): 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 +} diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt similarity index 100% rename from plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt rename to plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt diff --git a/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.fir.diag.txt deleted file mode 100644 index ff2a771faf9a4..0000000000000 --- a/plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.fir.diag.txt +++ /dev/null @@ -1,254 +0,0 @@ -/lambdas_receivers.kt:(736,742): 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$4: Ref - var ret$1: Ref - var anonymous$5: Ref - var ret$2: Ref - var anonymous$6: Ref - var ret$3: Ref - var anonymous$7: Ref - var ret$4: Ref - var anonymous$8: Ref - var ret$5: Ref - var anonymous$9: Ref - var ret$6: Ref - var local0$intResult: Ref - var anonymous$10: Ref - var ret$7: Ref - var ret$8: Ref - var anonymous$11: Ref - var ret$9: Ref - var ret$10: Ref - var anonymous$12: Ref - var ret$11: Ref - var ret$12: Ref - var local0$stdlibResult: Ref - var anonymous$13: Ref - var ret$13: Ref - var anonymous$14: Ref - var ret$14: Ref - var anonymous$15: Ref - var ret$15: Ref - var local0$capturedResult: Ref - var anonymous$16: Ref - var ret$16: Ref - var anonymous$17: Ref - var ret$17: Ref - var anonymous$18: Ref - var ret$18: Ref - var anonymous$19: Ref - var anonymous$20: Ref - var anonymous$21: Ref - var anonymous$22: Ref - var anonymous$23: Ref - var anonymous$24: Ref - var anonymous$25: Ref - var anonymous$26: 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$5 := ret$2 - ret$1 := anonymous$5 - goto label$ret$1 - label label$ret$1 - anonymous$4 := ret$1 - ret$4 := dom$RuntimeType$intToRef(2) - goto label$ret$4 - label label$ret$4 - anonymous$7 := ret$4 - ret$3 := anonymous$7 - goto label$ret$3 - label label$ret$3 - anonymous$6 := ret$3 - ret$6 := dom$RuntimeType$intToRef(3) - 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 - local0$genericResult := dom$RuntimeType$boolToRef(special$plusInts(anonymous$4, - anonymous$6) == - anonymous$8) - ret$8 := dom$RuntimeType$intToRef(1) - goto label$ret$8 - label label$ret$8 - ret$7 := ret$8 - goto label$ret$7 - label label$ret$7 - anonymous$10 := ret$7 - ret$10 := dom$RuntimeType$intToRef(2) - goto label$ret$10 - label label$ret$10 - ret$9 := ret$10 - goto label$ret$9 - label label$ret$9 - anonymous$11 := ret$9 - ret$12 := dom$RuntimeType$intToRef(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 - local0$intResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$10) + - dom$RuntimeType$intFromRef(anonymous$11) == - dom$RuntimeType$intFromRef(anonymous$12)) - ret$13 := dom$RuntimeType$intToRef(1) - goto label$ret$13 - label label$ret$13 - anonymous$13 := ret$13 - ret$14 := dom$RuntimeType$intToRef(2) - goto label$ret$14 - label label$ret$14 - anonymous$14 := ret$14 - ret$15 := dom$RuntimeType$intToRef(3) - goto label$ret$15 - label label$ret$15 - anonymous$15 := ret$15 - local0$stdlibResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$13) + - dom$RuntimeType$intFromRef(anonymous$14) == - dom$RuntimeType$intFromRef(anonymous$15)) - ret$16 := local0$one - goto label$ret$16 - label label$ret$16 - anonymous$16 := ret$16 - ret$17 := local0$two - goto label$ret$17 - label label$ret$17 - anonymous$17 := ret$17 - ret$18 := local0$three - goto label$ret$18 - label label$ret$18 - anonymous$18 := ret$18 - local0$capturedResult := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(anonymous$16) + - dom$RuntimeType$intFromRef(anonymous$17) == - dom$RuntimeType$intFromRef(anonymous$18)) - if (dom$RuntimeType$boolFromRef(local0$intResult)) { - anonymous$26 := local0$genericResult - } else { - anonymous$26 := dom$RuntimeType$boolToRef(false)} - if (dom$RuntimeType$boolFromRef(anonymous$26)) { - anonymous$25 := local0$stdlibResult - } else { - anonymous$25 := dom$RuntimeType$boolToRef(false)} - if (dom$RuntimeType$boolFromRef(anonymous$25)) { - anonymous$24 := local0$capturedResult - } else { - anonymous$24 := dom$RuntimeType$boolToRef(false)} - if (dom$RuntimeType$boolFromRef(anonymous$24)) { - var ret$19: Ref - var local19$result: Ref - var ret$20: Ref - ret$20 := special$plusInts(dom$RuntimeType$intToRef(1), dom$RuntimeType$intToRef(2)) - goto label$ret$20 - label label$ret$20 - local19$result := ret$20 - ret$19 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local19$result) == - 3) - goto label$ret$19 - label label$ret$19 - anonymous$23 := ret$19 - } else { - anonymous$23 := dom$RuntimeType$boolToRef(false)} - if (dom$RuntimeType$boolFromRef(anonymous$23)) { - var anonymous$27: Ref - var ret$21: Ref - var local21$result: Ref - var ret$22: Ref - ret$22 := dom$RuntimeType$intToRef(4) - goto label$ret$22 - label label$ret$22 - local21$result := ret$22 - ret$21 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local21$result) == - 3) - goto label$ret$21 - label label$ret$21 - anonymous$27 := ret$21 - anonymous$22 := special$notBool(anonymous$27) - } else { - anonymous$22 := dom$RuntimeType$boolToRef(false)} - if (dom$RuntimeType$boolFromRef(anonymous$22)) { - var ret$23: Ref - var local23$result: Ref - var ret$24: Ref - var anonymous$0: Ref - anonymous$0 := dom$RuntimeType$intToRef(1) - ret$24 := special$plusInts(anonymous$0, dom$RuntimeType$intToRef(2)) - goto label$ret$24 - label label$ret$24 - local23$result := ret$24 - ret$23 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local23$result) == - 3) - goto label$ret$23 - label label$ret$23 - anonymous$21 := ret$23 - } else { - anonymous$21 := dom$RuntimeType$boolToRef(false)} - if (dom$RuntimeType$boolFromRef(anonymous$21)) { - var anonymous$28: Ref - var ret$25: Ref - var local25$result: Ref - var ret$26: Ref - var anonymous$1: Ref - anonymous$1 := dom$RuntimeType$intToRef(1) - ret$26 := anonymous$1 - goto label$ret$26 - label label$ret$26 - local25$result := ret$26 - ret$25 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local25$result) == - 3) - goto label$ret$25 - label label$ret$25 - anonymous$28 := ret$25 - anonymous$20 := special$notBool(anonymous$28) - } else { - anonymous$20 := dom$RuntimeType$boolToRef(false)} - if (dom$RuntimeType$boolFromRef(anonymous$20)) { - var ret$27: Ref - var local27$result: Ref - var ret$28: Ref - var anonymous$2: Ref - anonymous$2 := dom$RuntimeType$intToRef(1) - ret$28 := special$plusInts(anonymous$2, dom$RuntimeType$intToRef(2)) - goto label$ret$28 - label label$ret$28 - local27$result := ret$28 - ret$27 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local27$result) == - 3) - goto label$ret$27 - label label$ret$27 - anonymous$19 := ret$27 - } else { - anonymous$19 := dom$RuntimeType$boolToRef(false)} - if (dom$RuntimeType$boolFromRef(anonymous$19)) { - var ret$29: Ref - var local29$result: Ref - var ret$30: Ref - var anonymous$3: Ref - anonymous$3 := dom$RuntimeType$intToRef(1) - ret$30 := special$plusInts(anonymous$3, dom$RuntimeType$intToRef(2)) - goto label$ret$30 - label label$ret$30 - local29$result := ret$30 - ret$29 := dom$RuntimeType$boolToRef(dom$RuntimeType$intFromRef(local29$result) == - 3) - goto label$ret$29 - label label$ret$29 - ret$0 := ret$29 - } else { - ret$0 := dom$RuntimeType$boolToRef(false)} - goto label$ret$0 - label label$ret$0 -} 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 07f353f6afda6..c3673b1158992 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() { @@ -139,12 +145,6 @@ public void testIs_type_contract() { runTest("plugins/formal-verification/testData/diagnostics/good_contracts/is_type_contract.kt"); } - @Test - @TestMetadata("lambdas_receivers.kt") - public void testLambdas_receivers() { - runTest("plugins/formal-verification/testData/diagnostics/good_contracts/lambdas_receivers.kt"); - } - @Test @TestMetadata("list.kt") public void testList() { @@ -233,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() { From 917e9d2fc23d72e6de18ae81b2e02f4e984c3940 Mon Sep 17 00:00:00 2001 From: Grigorii Solnyshkin Date: Mon, 1 Jul 2024 10:17:31 +0300 Subject: [PATCH 6/8] added test wih backing field --- .../custom_run_functions.fir.diag.txt | 51 ++++++++++++++++++- .../good_contracts/custom_run_functions.kt | 21 +++++++- 2 files changed, 68 insertions(+), 4 deletions(-) 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 index 776484fbc1277..f88f0476b7539 100644 --- 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 @@ -1,4 +1,4 @@ -/custom_run_functions.kt:(1073,1079): info: Generated Viper text for useRun: +/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 @@ -316,7 +316,7 @@ method global$fun_useRun$fun_take$$return$T_Boolean() returns (ret$0: Ref) label label$ret$0 } -/custom_run_functions.kt:(2241,2256): info: Generated Viper text for complexScenario: +/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()) @@ -458,3 +458,50 @@ method global$fun_complexScenario$fun_take$T_Boolean$return$T_Boolean(local$arg: 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 index e4c7fcde464d7..fa3c014af5bbe 100644 --- a/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt +++ b/plugins/formal-verification/testData/diagnostics/good_contracts/custom_run_functions.kt @@ -1,5 +1,3 @@ -// USE_STDLIB - import kotlin.contracts.ExperimentalContracts import kotlin.contracts.contract import org.jetbrains.kotlin.formver.plugin.NeverConvert @@ -102,4 +100,23 @@ public fun complexScenario(arg: Boolean): Boolean { } } } +} + +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 From e5df0b51e061f5d0e2ab99d9d7746c3788945417 Mon Sep 17 00:00:00 2001 From: Grigorii Solnyshkin Date: Mon, 1 Jul 2024 16:00:21 +0300 Subject: [PATCH 7/8] implementation of FIR as reverted --- .../kotlin/formver/conversion/StmtConversionVisitor.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 dcab7c94af434..55ea2a5194c06 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 @@ -301,7 +301,7 @@ object StmtConversionVisitor : FirVisitor() return when (typeOperatorCall.operation) { FirOperation.IS -> Is(argument, conversionType) FirOperation.NOT_IS -> Not(Is(argument, conversionType)) - FirOperation.AS -> argument.withNewTypeAccessAndProvenInvariants(conversionType) + FirOperation.AS -> Cast(argument, conversionType).withAccessAndProvenInvariants() FirOperation.SAFE_AS -> SafeCast(argument, conversionType).withAccessAndProvenInvariants() else -> handleUnimplementedElement("Can't embed type operator ${typeOperatorCall.operation}.", data) } From d24e305ce07f96b9176503c2411c38ecd9fd9378 Mon Sep 17 00:00:00 2001 From: Grigorii Solnyshkin Date: Mon, 8 Jul 2024 08:23:33 +0300 Subject: [PATCH 8/8] removed unrelated simple function declaration visit implementation --- .../kotlin/formver/conversion/StmtConversionVisitor.kt | 5 ----- 1 file changed, 5 deletions(-) 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 55ea2a5194c06..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 @@ -130,11 +130,6 @@ object StmtConversionVisitor : FirVisitor() 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,