Make public backing fields explicitly unscoped. (#231)

Previously, we maintained scoping information in the name. This was a
bit messy; this PR changes the approach to not give them a scope at all.

We don't remove the special case on public scope yet, since that also
impacts public properties.

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

@@ -40,7 +40,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
     private val methods: MutableMap<MangledName, FunctionEmbedding> = SpecialKotlinFunctions.byName.toMutableMap()
     private val classes: MutableMap<MangledName, ClassTypeEmbedding> = mutableMapOf()
     private val properties: MutableMap<MangledName, PropertyEmbedding> = mutableMapOf()
-    private val fields: MutableMap<MangledName, FieldEmbedding> = mutableMapOf()
+    private val fields: MutableSet<FieldEmbedding> = mutableSetOf()
 
     // Cast is valid since we check that values are not null. We specify the type for `filterValues` explicitly to ensure there's no
     // loss of type information earlier.
@@ -65,7 +65,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
             // We need to deduplicate fields since public fields with the same name are represented differently
             // at `FieldEmbedding` level but map to the same Viper.
             fields = SpecialFields.all.map { it.toViper() } +
-                    fields.values.distinctBy { it.name.mangled }.map { it.toViper() },
+                    fields.distinctBy { it.name.mangled }.map { it.toViper() },
             functions = SpecialFunctions.all,
             methods = SpecialMethods.all + methods.values.mapNotNull { it.viperMethod }.distinctBy { it.name.mangled },
             predicates = classes.values.flatMap { listOf(it.details.sharedPredicate, it.details.uniquePredicate) }
@@ -314,7 +314,8 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
                 scopedName,
                 embedType(symbol.resolvedReturnType),
                 symbol,
-                symbol.isUnique(session)
+                symbol.isUnique(session),
+                embedding,
             )
         }
         return backingField?.let { unscopedName to it }
@@ -329,7 +330,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
     private fun processProperty(symbol: FirPropertySymbol, embedding: ClassEmbeddingDetails) {
         val unscopedName = symbol.callableId.embedUnscopedPropertyName()
         val backingField = embedding.findField(unscopedName)
-        backingField?.let { fields.put(it.name, it) }
+        backingField?.let { fields.add(it) }
         properties[symbol.embedMemberPropertyName()] = embedProperty(symbol, backingField)
     }
 

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

@@ -17,7 +17,6 @@ class BackingFieldGetter(val field: FieldEmbedding) : GetterEmbedding {
             FieldAccess(receiver, field).withAccessAndProvenInvariants()
         }
     }
-
 }
 
 class BackingFieldSetter(val field: FieldEmbedding) : SetterEmbedding {

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

@@ -6,10 +6,8 @@
 package org.jetbrains.kotlin.formver.embeddings
 
 import org.jetbrains.kotlin.formver.names.*
-import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
 import org.jetbrains.kotlin.formver.viper.ast.Predicate
-import org.jetbrains.kotlin.formver.viper.mangled
 import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
 
 class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boolean) : TypeInvariantHolder {
@@ -100,16 +98,16 @@ class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boole
         PredicateAccessTypeInvariantEmbedding(uniquePredicateName, PermExp.FullPerm())
 
     // Returns the sequence of classes in a hierarchy that need to be unfolded in order to access the given field
-    fun hierarchyUnfoldPath(fieldName: ScopedKotlinName): Sequence<ClassTypeEmbedding> = sequence {
-        val className = fieldName.scope.classNameIfAny
-        require(className != null) { "Cannot find hierarchy unfold path of a field with no class scope" }
-        if (className == type.className.name) {
+    fun hierarchyUnfoldPath(field: FieldEmbedding): Sequence<ClassTypeEmbedding> = sequence {
+        val className = field.containingClass?.className
+        require(className != null) { "Cannot find hierarchy unfold path of a field with no class information" }
+        if (className == type.className) {
             yield(this@ClassEmbeddingDetails.type)
         } else {
             val sup = superTypes.firstOrNull { it is ClassTypeEmbedding && !it.details.isInterface }
             if (sup is ClassTypeEmbedding) {
                 yield(this@ClassEmbeddingDetails.type)
-                yieldAll(sup.details.hierarchyUnfoldPath(fieldName))
+                yieldAll(sup.details.hierarchyUnfoldPath(field))
             } else {
                 throw IllegalArgumentException("Reached top of the hierarchy without finding the field")
             }

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

@@ -27,6 +27,8 @@ interface FieldEmbedding {
     // If true, it is necessary to unfold the predicate of the receiver before accessing the field
     val unfoldToAccess: Boolean
         get() = false
+    val containingClass: ClassTypeEmbedding?
+        get() = null
     val includeInShortDump: Boolean
     val symbol: FirPropertySymbol?
         get() = null
@@ -53,6 +55,7 @@ class UserFieldEmbedding(
     override val type: TypeEmbedding,
     override val symbol: FirPropertySymbol,
     override val isUnique: Boolean,
+    override val containingClass: ClassTypeEmbedding,
 ) : FieldEmbedding {
     override val viperType = Type.Ref
     override val accessPolicy: AccessPolicy = if (symbol.isVal) AccessPolicy.ALWAYS_READABLE else AccessPolicy.ALWAYS_INHALE_EXHALE

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

@@ -13,7 +13,6 @@ import org.jetbrains.kotlin.formver.embeddings.expression.debug.*
 import org.jetbrains.kotlin.formver.linearization.InhaleExhaleStmtModifier
 import org.jetbrains.kotlin.formver.linearization.LinearizationContext
 import org.jetbrains.kotlin.formver.linearization.pureToViper
-import org.jetbrains.kotlin.formver.names.ScopedKotlinName
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.Exp
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
@@ -376,7 +375,7 @@ data class FieldAccess(val receiver: ExpEmbedding, val field: FieldEmbedding) :
     }
 
     private fun unfoldHierarchy(receiverWrapper: ExpEmbedding, ctx: LinearizationContext) {
-        val hierarchyPath = (receiver.type as? ClassTypeEmbedding)?.details?.hierarchyUnfoldPath(field.name as ScopedKotlinName)
+        val hierarchyPath = (receiver.type as? ClassTypeEmbedding)?.details?.hierarchyUnfoldPath(field)
         hierarchyPath?.forEach { classType ->
             val predAcc = classType.sharedPredicateAccessInvariant().fillHole(receiverWrapper)
                 .pureToViper(toBuiltin = true, ctx.source) as? Exp.PredicateAccess

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

@@ -0,0 +1,21 @@
+/*
+ * Copyright 2010-2024 JetBrains s.r.o. and Kotlin Programming Language contributors.
+ * Use of this source code is governed by the Apache 2.0 license that can be found in the license/LICENSE.txt file.
+ */
+
+package org.jetbrains.kotlin.formver.names
+
+enum class MemberEmbeddingPolicy {
+    PRIVATE,
+    PUBLIC,
+    UNSCOPED,
+}
+
+fun alwaysScopedPolicy(isPrivate: Boolean): MemberEmbeddingPolicy =
+    if (isPrivate) MemberEmbeddingPolicy.PRIVATE else MemberEmbeddingPolicy.PUBLIC
+
+fun onlyPrivateScopedPolicy(isPrivate: Boolean): MemberEmbeddingPolicy =
+    if (isPrivate) MemberEmbeddingPolicy.PRIVATE else MemberEmbeddingPolicy.UNSCOPED
+
+val MemberEmbeddingPolicy.isScoped: Boolean
+    get() = this == MemberEmbeddingPolicy.PRIVATE || this == MemberEmbeddingPolicy.PUBLIC

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

@@ -9,7 +9,6 @@ import org.jetbrains.kotlin.descriptors.Visibilities
 import org.jetbrains.kotlin.fir.declarations.utils.visibility
 import org.jetbrains.kotlin.fir.symbols.impl.*
 import org.jetbrains.kotlin.formver.conversion.ProgramConversionContext
-import org.jetbrains.kotlin.formver.embeddings.ClassTypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
 import org.jetbrains.kotlin.name.CallableId
 import org.jetbrains.kotlin.name.ClassId
@@ -48,19 +47,28 @@ fun CallableId.embedExtensionSetterName(type: TypeEmbedding): ScopedKotlinName =
     ExtensionSetterKotlinName(callableName, type)
 }
 
-private fun CallableId.embedMemberPropertyNameBase(isPrivate: Boolean, withAction: (Name) -> KotlinName): ScopedKotlinName {
+private fun CallableId.embedMemberPropertyNameBase(scopePolicy: MemberEmbeddingPolicy, withAction: (Name) -> KotlinName): ScopedKotlinName {
     val id = classId ?: error("Embedding non-member property $callableName as a member.")
     return buildName {
-        embedScope(id)
-        if (isPrivate) privateScope() else publicScope()
+        if (scopePolicy.isScoped) {
+            embedScope(id)
+        }
+        when (scopePolicy) {
+            MemberEmbeddingPolicy.PUBLIC -> publicScope()
+            MemberEmbeddingPolicy.PRIVATE -> privateScope()
+            MemberEmbeddingPolicy.UNSCOPED -> fakeScope()
+        }
         withAction(callableName)
     }
 }
 
-fun CallableId.embedMemberPropertyName(isPrivate: Boolean) = embedMemberPropertyNameBase(isPrivate, ::PropertyKotlinName)
-fun CallableId.embedMemberGetterName(isPrivate: Boolean) = embedMemberPropertyNameBase(isPrivate, ::GetterKotlinName)
-fun CallableId.embedMemberSetterName(isPrivate: Boolean) = embedMemberPropertyNameBase(isPrivate, ::SetterKotlinName)
-fun CallableId.embedMemberBackingFieldName(isPrivate: Boolean) = embedMemberPropertyNameBase(isPrivate, ::BackingFieldKotlinName)
+fun CallableId.embedMemberPropertyName(isPrivate: Boolean) =
+    embedMemberPropertyNameBase(alwaysScopedPolicy(isPrivate), ::PropertyKotlinName)
+
+fun CallableId.embedMemberGetterName(isPrivate: Boolean) = embedMemberPropertyNameBase(alwaysScopedPolicy(isPrivate), ::GetterKotlinName)
+fun CallableId.embedMemberSetterName(isPrivate: Boolean) = embedMemberPropertyNameBase(alwaysScopedPolicy(isPrivate), ::SetterKotlinName)
+fun CallableId.embedMemberBackingFieldName(isPrivate: Boolean) =
+    embedMemberPropertyNameBase(onlyPrivateScopedPolicy(isPrivate), ::BackingFieldKotlinName)
 
 fun CallableId.embedUnscopedPropertyName(): SimpleKotlinName = SimpleKotlinName(callableName)
 fun CallableId.embedFunctionName(type: TypeEmbedding): ScopedKotlinName = buildName {

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

@@ -84,3 +84,11 @@ data class LocalScope(val level: Int) : NameScope {
     override val parent: NameScope? = null
     override val mangledScopeName = "l$level"
 }
+
+/**
+ * Scope to use in cases when we need a scoped name, but don't actually want to introduce one.
+ */
+data object FakeScope : NameScope {
+    override val parent: NameScope? = null
+    override val mangledScopeName: String? = null
+}

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

@@ -46,9 +46,14 @@ class ScopedKotlinNameBuilder {
     }
 
     fun localScope(level: Int) {
-        require (scope == null) { "Local scope cannot be nested." }
+        require(scope == null) { "Local scope cannot be nested." }
         scope = LocalScope(level)
     }
+
+    fun fakeScope() {
+        require(scope == null) { "Fake scope cannot be nested." }
+        scope = FakeScope
+    }
 }
 
 // TODO: generalise this to work for all names.

plugins/formal-verification/testData/diagnostics/bad_contracts/as_type_contract.fir.diag.txt

@@ -1,5 +1,5 @@
 /as_type_contract.kt:(150,154): info: Generated Viper text for getX:
-field bf$public$x: Ref
+field bf$x: Ref
 
 method f$getX$TF$T$Any(p$a: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
@@ -18,7 +18,7 @@ method f$getX$TF$T$Any(p$a: Ref) returns (ret$0: Ref)
   if (anon$0 != df$rt$nullValue()) {
     var anon$1: Ref
     unfold acc(p$c$IntHolder$shared(anon$0), wildcard)
-    anon$1 := anon$0.bf$public$x
+    anon$1 := anon$0.bf$x
     ret$0 := anon$1
   } else {
     ret$0 := df$rt$nullValue()}

plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt

@@ -67,7 +67,7 @@ method pg$public$length(this: Ref) returns (ret: Ref)
 /cond_effects.kt:(796,832): warning: Cannot verify that if a false value is returned then seq != null.
 
 /cond_effects.kt:(925,942): info: Generated Viper text for recursiveContract:
-field bf$public$length: Ref
+field bf$length: Ref
 
 method f$recursiveContract$TF$T$Int$Any(p$n: Ref, p$x: Ref)
   returns (ret$0: Ref)

plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt

@@ -1,5 +1,5 @@
 /is_type_contract.kt:(151,172): info: Generated Viper text for unverifiableTypeCheck:
-field bf$public$length: Ref
+field bf$length: Ref
 
 method f$unverifiableTypeCheck$TF$Int(p$x: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())

plugins/formal-verification/testData/diagnostics/good_contracts/as_type_contract.fir.diag.txt

@@ -32,7 +32,7 @@ method f$safeAsOperator$TF$T$c$Foo(p$foo: Ref) returns (ret$0: Ref)
 }
 
 /as_type_contract.kt:(504,508): info: Generated Viper text for getX:
-field bf$public$x: Ref
+field bf$x: Ref
 
 method f$getX$TF$T$Any(p$a: Ref) returns (ret$0: Ref)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
@@ -53,7 +53,7 @@ method f$getX$TF$T$Any(p$a: Ref) returns (ret$0: Ref)
   if (anon$0 != df$rt$nullValue()) {
     var anon$1: Ref
     unfold acc(p$c$IntHolder$shared(anon$0), wildcard)
-    anon$1 := anon$0.bf$public$x
+    anon$1 := anon$0.bf$x
     ret$0 := anon$1
   } else {
     ret$0 := df$rt$nullValue()}