Sai/acc syntax addition

formver.annotations/src/org/jetbrains/kotlin/formver/plugin/Builtins.kt

@@ -27,6 +27,14 @@ fun <T> 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 <T> 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): Boolean =
+        throw FormverFunctionCalledInRuntimeException("acc")
 }

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

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/StmtConversionContext.kt

@@ -6,30 +6,66 @@
 package org.jetbrains.kotlin.formver.core.conversion
 
 import org.jetbrains.kotlin.fir.FirLabel
+import org.jetbrains.kotlin.fir.containingClassLookupTag
 import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction
+import org.jetbrains.kotlin.fir.declarations.FirValueParameter
+import org.jetbrains.kotlin.fir.declarations.hasAnnotation
 import org.jetbrains.kotlin.fir.declarations.utils.isFinal
 import org.jetbrains.kotlin.fir.expressions.*
 import org.jetbrains.kotlin.fir.references.symbol
 import org.jetbrains.kotlin.fir.symbols.impl.*
+import org.jetbrains.kotlin.fir.types.ConeCapturedType
+import org.jetbrains.kotlin.fir.types.ConeDefinitelyNotNullType
+import org.jetbrains.kotlin.fir.types.ConeFlexibleType
+import org.jetbrains.kotlin.fir.types.ConeIntegerConstantOperatorType
+import org.jetbrains.kotlin.fir.types.ConeIntegerLiteralConstantType
+import org.jetbrains.kotlin.fir.types.ConeIntersectionType
+import org.jetbrains.kotlin.fir.types.ConeLookupTagBasedType
+import org.jetbrains.kotlin.fir.types.ConeStubTypeForTypeVariableInSubtyping
+import org.jetbrains.kotlin.fir.types.ConeTypeVariableType
+import org.jetbrains.kotlin.fir.types.classId
 import org.jetbrains.kotlin.fir.types.isBoolean
+import org.jetbrains.kotlin.fir.types.isMarkedNullable
+import org.jetbrains.kotlin.fir.types.isMarkedOrFlexiblyNullable
+import org.jetbrains.kotlin.fir.types.lowerBoundIfFlexible
 import org.jetbrains.kotlin.fir.types.resolvedType
+import org.jetbrains.kotlin.fir.types.withNullability
 import org.jetbrains.kotlin.formver.common.SnaktInternalException
 import org.jetbrains.kotlin.formver.core.embeddings.FunctionBodyEmbedding
 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.FieldEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.properties.PropertyAccessEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.properties.UserFieldEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.properties.asPropertyAccess
+import org.jetbrains.kotlin.formver.core.embeddings.types.AnyTypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.BooleanTypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.CharTypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.ClassTypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.IntTypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.NothingTypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.PretypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.StringTypeEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbeddingFlags
+import org.jetbrains.kotlin.formver.core.embeddings.types.UnitTypeEmbedding
 import org.jetbrains.kotlin.formver.core.isCustom
 import org.jetbrains.kotlin.formver.core.isInvariantBuilderFunctionNamed
 import org.jetbrains.kotlin.formver.core.linearization.*
+import org.jetbrains.kotlin.formver.core.names.ScopedKotlinName
+import org.jetbrains.kotlin.formver.core.names.embedMemberPropertyName
+import org.jetbrains.kotlin.formver.core.names.embedName
 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.name.StandardClassIds
+import org.jetbrains.kotlin.text
 import org.jetbrains.kotlin.utils.addIfNotNull
 import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
 import org.jetbrains.kotlin.utils.filterIsInstanceAnd
@@ -235,6 +271,27 @@ fun StmtConversionContext.insertForAllFunctionCall(
     }
 }
 
+fun StmtConversionContext.insertAccFunctionCall(
+    field: FirPropertyAccessExpression,
+    perm: FirExpression,
+): 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).property.getter as BackingFieldGetter).field
+    val receiver = fieldAccess.receiver
+    val permExp = when(perm.source.text.toString()) {
+        "write" -> PermExp.WildcardPerm()
+        "read" -> PermExp.FullPerm()
+        else -> throw SnaktInternalException(symbol.source, "perm is not supported")
+    }
+    return withNoScope {
+        AccEmbedding(field, receiver, permExp)
+    }
+}
+
 fun StmtConversionContext.convertMethodWithBody(
     declaration: FirSimpleFunction,
     signature: FullNamedFunctionSignature,

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
@@ -286,17 +289,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
         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 +300,22 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
                     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
+            val permExpr = accLambda.arguments[1]
+            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(

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);

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, wildcard)
+  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)
+

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 <!VIPER_TEXT!>test_acc_precondition<!>(x: X) {
+    preconditions { acc(x.a, write) }
+    x.a = 123
+}