diff --git a/formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Builtins.kt b/formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Builtins.kt index e6ed125c3..a445af9fd 100644 --- a/formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Builtins.kt +++ b/formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Builtins.kt @@ -27,6 +27,14 @@ fun postconditions(@Suppress("UNUSED_PARAMETER") body: InvariantBuilder.(T) * This class is designed as a receiver for lambda blocks of `loopInvariants`, `preconditions` and `postconditions`. */ class InvariantBuilder { + + class Permission + + val read : Permission + get() = throw FormverFunctionCalledInRuntimeException("read.get") + val write : Permission + get() = throw FormverFunctionCalledInRuntimeException("write.get") + fun forAll(@Suppress("UNUSED_PARAMETER") body: (T) -> Unit): Boolean = throw FormverFunctionCalledInRuntimeException("forAll") @@ -37,4 +45,7 @@ class InvariantBuilder { */ fun triggers(@Suppress("UNUSED_PARAMETER") vararg expressions: Any?): Unit = throw FormverFunctionCalledInRuntimeException("triggers") + + fun acc(@Suppress("UNUSED_PARAMETER") path: Any?, permission: Permission? = null): Boolean = + throw FormverFunctionCalledInRuntimeException("acc") } diff --git a/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/FormverFirBlock.kt b/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/FormverFirBlock.kt index bcadac5e4..efa271204 100644 --- a/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/FormverFirBlock.kt +++ b/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/FormverFirBlock.kt @@ -22,6 +22,13 @@ fun FirStatement.extractFormverFirBlock(predicate: FirFunctionSymbol<*>.() -> Bo return formverInvariantsArgument.anonymousFunction } +fun FirStatement.extractFormverFirStmt(predicate: FirFunctionSymbol<*>.() -> Boolean): FirFunctionCall? { + if (this !is FirFunctionCall) return null + val firFunction = toResolvedCallableSymbol() as? FirFunctionSymbol<*> ?: return null + if (!predicate(firFunction)) return null + return this +} + fun extractLoopInvariants(parentBlock: FirBlock): FirBlock? { val firstStmt = parentBlock.statements.firstOrNull() ?: return null return firstStmt.extractFormverFirBlock { isFormverFunctionNamed("loopInvariants") }?.body diff --git a/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionContext.kt b/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionContext.kt index 00319503c..3a7aa95f9 100644 --- a/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionContext.kt +++ b/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionContext.kt @@ -19,6 +19,7 @@ import org.jetbrains.kotlin.formver.core.embeddings.LabelEmbedding import org.jetbrains.kotlin.formver.core.embeddings.callables.FullNamedFunctionSignature import org.jetbrains.kotlin.formver.core.embeddings.callables.FunctionSignature import org.jetbrains.kotlin.formver.core.embeddings.expression.* +import org.jetbrains.kotlin.formver.core.embeddings.properties.BackingFieldGetter import org.jetbrains.kotlin.formver.core.embeddings.properties.ClassPropertyAccess import org.jetbrains.kotlin.formver.core.embeddings.properties.PropertyAccessEmbedding import org.jetbrains.kotlin.formver.core.embeddings.properties.asPropertyAccess @@ -30,6 +31,7 @@ import org.jetbrains.kotlin.formver.core.purity.checkValidity import org.jetbrains.kotlin.formver.core.purity.isPure import org.jetbrains.kotlin.formver.viper.SymbolicName import org.jetbrains.kotlin.formver.viper.ast.Exp +import org.jetbrains.kotlin.formver.viper.ast.PermExp import org.jetbrains.kotlin.utils.addIfNotNull import org.jetbrains.kotlin.utils.addToStdlib.ifTrue import org.jetbrains.kotlin.utils.filterIsInstanceAnd @@ -235,6 +237,28 @@ fun StmtConversionContext.insertForAllFunctionCall( } } +fun StmtConversionContext.insertAccFunctionCall( + field: FirPropertyAccessExpression, + perm: PermExp, +): ExpEmbedding { + val symbol = field.calleeReference.symbol as? FirPropertySymbol ?: throw SnaktInternalException( + field.source, + "acc requires a property access like x.a" + ) + val fieldAccess = embedPropertyAccess(field) + val field = ((fieldAccess as? ClassPropertyAccess ?: throw SnaktInternalException( + field.source, + "could not embed as class property" + )).property.getter as? BackingFieldGetter ?: throw SnaktInternalException( + field.source, + "could not get property access like x.a" + )).field + val receiver = fieldAccess.receiver + return withNoScope { + AccEmbedding(receiver, field, perm) + } +} + fun StmtConversionContext.convertMethodWithBody( declaration: FirSimpleFunction, signature: FullNamedFunctionSignature, diff --git a/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionVisitor.kt b/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionVisitor.kt index 649474f6a..b0051c366 100644 --- a/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionVisitor.kt +++ b/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionVisitor.kt @@ -5,10 +5,12 @@ package org.jetbrains.kotlin.formver.core.conversion +import org.checkerframework.common.aliasing.qual.Unique import org.jetbrains.kotlin.KtSourceElement 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.hasAnnotation import org.jetbrains.kotlin.fir.expressions.* import org.jetbrains.kotlin.fir.expressions.impl.FirElseIfTrueCondition import org.jetbrains.kotlin.fir.expressions.impl.FirUnitExpression @@ -21,6 +23,7 @@ import org.jetbrains.kotlin.fir.types.resolvedType import org.jetbrains.kotlin.fir.visitors.FirVisitor import org.jetbrains.kotlin.formver.common.SnaktInternalException import org.jetbrains.kotlin.formver.common.UnsupportedFeatureBehaviour +import org.jetbrains.kotlin.formver.core.annotationId import org.jetbrains.kotlin.formver.core.embeddings.LabelLink import org.jetbrains.kotlin.formver.core.embeddings.callables.CallableEmbedding import org.jetbrains.kotlin.formver.core.embeddings.callables.FunctionEmbedding @@ -41,6 +44,7 @@ import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbedding import org.jetbrains.kotlin.formver.core.embeddings.types.equalToType import org.jetbrains.kotlin.formver.core.functionCallArguments import org.jetbrains.kotlin.formver.core.isInvariantBuilderFunctionNamed +import org.jetbrains.kotlin.formver.viper.ast.PermExp import org.jetbrains.kotlin.text import org.jetbrains.kotlin.types.ConstantValueKind import org.jetbrains.kotlin.utils.addIfNotNull @@ -286,17 +290,7 @@ object StmtConversionVisitor : FirVisitor() val symbol = functionCall.toResolvedCallableSymbol() as? FirFunctionSymbol<*> ?: throw NotImplementedError("Only functions are expected as callables of function calls, got ${functionCall.toResolvedCallableSymbol()}") - when (val forAllLambda = functionCall.extractFormverFirBlock { isInvariantBuilderFunctionNamed("forAll") }) { - null -> { - val callee = data.embedAnyFunction(symbol) - return callee.insertCall( - functionCall.functionCallArguments.withVarargsHandled(data, callee), - data, - data.embedType(functionCall.resolvedType), - ) - } - - else -> { + functionCall.extractFormverFirBlock { isInvariantBuilderFunctionNamed("forAll") }?.let { forAllLambda -> if (!data.isValidForForAllBlock) throw SnaktInternalException( forAllLambda.source, "`forAll` scope is only allowed inside one of the `loopInvariants`, `preconditions` or `postconditions`." @@ -307,8 +301,29 @@ object StmtConversionVisitor : FirVisitor() forAllLambda.body?.source, "Lambda body should be accessible in `forAll` function call." ) return data.insertForAllFunctionCall(forAllArg.symbol, forAllBody) + } + + functionCall.extractFormverFirStmt { isInvariantBuilderFunctionNamed("acc") }?.let { + accLambda -> + //acc is only allowed to be used in the same context as forAll + if (!data.isValidForForAllBlock) throw SnaktInternalException( + accLambda.source, + "`acc` scope is only allowed inside one of the `loopInvariants`, `preconditions` or `postconditions`." + ) + val fieldExpr = accLambda.arguments[0] as? FirPropertyAccessExpression ?: throw SnaktInternalException( + accLambda.source, + "must be a property access expression." + ) + val permExpr = when(accLambda.arguments.getOrNull(1)?.source?.text?.toString() ?: "") { + "write" -> PermExp.WildcardPerm() + "read", "" -> PermExp.FullPerm() + else -> throw SnaktInternalException(symbol.source, "perm is not supported") } + return data.insertAccFunctionCall(fieldExpr, permExpr) } + + val callee = data.embedAnyFunction(symbol) + return callee.insertCall( functionCall.functionCallArguments.withVarargsHandled(data, callee), data, data.embedType(functionCall.resolvedType), ) } override fun visitImplicitInvokeCall( diff --git a/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/expression/AccEmbedding.kt b/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/expression/AccEmbedding.kt index e8d9619b2..fd3dee84d 100644 --- a/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/expression/AccEmbedding.kt +++ b/formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/expression/AccEmbedding.kt @@ -5,12 +5,10 @@ package org.jetbrains.kotlin.formver.core.embeddings.expression -import org.jetbrains.kotlin.backend.jvm.AccessType import org.jetbrains.kotlin.formver.core.asPosition import org.jetbrains.kotlin.formver.core.embeddings.ExpVisitor import org.jetbrains.kotlin.formver.core.embeddings.asInfo import org.jetbrains.kotlin.formver.core.embeddings.properties.FieldEmbedding -import org.jetbrains.kotlin.formver.core.embeddings.types.FieldAccessTypeInvariantEmbedding import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbedding import org.jetbrains.kotlin.formver.core.embeddings.types.buildType import org.jetbrains.kotlin.formver.core.linearization.LinearizationContext @@ -18,13 +16,13 @@ import org.jetbrains.kotlin.formver.viper.ast.Exp import org.jetbrains.kotlin.formver.viper.ast.PermExp class AccEmbedding( + val receiver: ExpEmbedding, val field: FieldEmbedding, - val access: ExpEmbedding, val perm: PermExp, ) : OnlyToBuiltinTypeExpEmbedding { override fun toViperBuiltinType(ctx: LinearizationContext): Exp { val field = Exp.FieldAccess( - access.toViper(ctx), + receiver.toViper(ctx), field.toViper(), ctx.source.asPosition, ) @@ -36,7 +34,7 @@ class AccEmbedding( ) } - override val subexpressions: List = listOf(access) + override val subexpressions: List = listOf(receiver) override val type: TypeEmbedding get() = buildType { boolean() } diff --git a/formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java b/formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java index 2e17f758d..2794e7f36 100644 --- a/formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java +++ b/formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java @@ -94,6 +94,12 @@ public void testShadowing() { @TestMetadata("formver.compiler-plugin/testData/diagnostics/conversion/classes") @TestDataPath("$PROJECT_ROOT") public class Classes { + @Test + @TestMetadata("acc_precondition.kt") + public void testAcc_precondition() { + runTest("formver.compiler-plugin/testData/diagnostics/conversion/classes/acc_precondition.kt"); + } + @Test public void testAllFilesPresentInClasses() { KtTestUtil.assertAllTestsPresentByMetadataWithExcluded(this.getClass(), new File("formver.compiler-plugin/testData/diagnostics/conversion/classes"), Pattern.compile("^(.+)\\.kt$"), null, true); diff --git a/formver.compiler-plugin/testData/diagnostics/conversion/classes/acc_precondition.fir.diag.txt b/formver.compiler-plugin/testData/diagnostics/conversion/classes/acc_precondition.fir.diag.txt new file mode 100644 index 000000000..6862e170b --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/conversion/classes/acc_precondition.fir.diag.txt @@ -0,0 +1,36 @@ +/acc_precondition.kt:(127,148): info: Generated Viper text for test_acc_precondition: +field bf$a: Ref + +predicate p$c$X$shared(this$dispatch: Ref) { + true +} + +predicate p$c$X$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$a, write) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$a), df$rt$anyType()) +} + +predicate p$pkg$org_jetbrains_kotlin_formver_plugin$c$InvariantBuilder$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$org_jetbrains_kotlin_formver_plugin$c$InvariantBuilder$unique(this$dispatch: Ref) { + true +} + +method f$test_acc_precondition$TF$T$X(p$x: Ref) returns (ret$0: Ref) + requires acc(p$x.bf$a, write) + ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +{ + inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$c$X()) + inhale acc(p$c$X$shared(p$x), wildcard) + p$x.bf$a := df$rt$intToRef(123) + label lbl$ret$0 + inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +} + +method pg$public$read(this$dispatch: Ref) returns (ret: Ref) + + +method pg$public$write(this$dispatch: Ref) returns (ret: Ref) + diff --git a/formver.compiler-plugin/testData/diagnostics/conversion/classes/acc_precondition.kt b/formver.compiler-plugin/testData/diagnostics/conversion/classes/acc_precondition.kt new file mode 100644 index 000000000..1abdaf9e2 --- /dev/null +++ b/formver.compiler-plugin/testData/diagnostics/conversion/classes/acc_precondition.kt @@ -0,0 +1,10 @@ +// RENDER_PREDICATES +// NEVER_VALIDATE + +import org.jetbrains.kotlin.formver.plugin.* + +class X(@property:Manual var a: Any) +fun test_acc_precondition(x: X) { + preconditions { acc(x.a) } + x.a = 123 +}