Skip to content

Commit

Permalink
Restructure scoping definitions to be more structured.
Browse files Browse the repository at this point in the history
Previously, scopes were just arbitrary names.  This imposes the kind of
hierarchical structure on scopes that we will want to use for optimising
mangled name length.
  • Loading branch information
jesyspa committed Jul 19, 2024
1 parent bf8db14 commit f391ca1
Show file tree
Hide file tree
Showing 10 changed files with 208 additions and 81 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ package org.jetbrains.kotlin.formver.embeddings
import org.jetbrains.kotlin.formver.names.ClassScope
import org.jetbrains.kotlin.formver.names.ScopedKotlinName
import org.jetbrains.kotlin.formver.names.SimpleKotlinName
import org.jetbrains.kotlin.formver.names.classNameIfAny
import org.jetbrains.kotlin.formver.viper.MangledName
import org.jetbrains.kotlin.formver.viper.ast.PermExp
import org.jetbrains.kotlin.formver.viper.ast.Predicate
Expand Down Expand Up @@ -102,21 +103,19 @@ 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: MangledName): Sequence<ClassTypeEmbedding> = sequence {
if (fieldName is ScopedKotlinName && fieldName.scope is ClassScope) {
if (fieldName.scope.className == type.className.name) {
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) {
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))
} else {
val sup = superTypes.firstOrNull { it is ClassTypeEmbedding && !it.details.isInterface }
if (sup is ClassTypeEmbedding) {
yield(this@ClassEmbeddingDetails.type)
yieldAll(sup.details.hierarchyUnfoldPath(fieldName))
} else {
throw IllegalArgumentException("Reached top of the hierarchy without finding the field")
}
throw IllegalArgumentException("Reached top of the hierarchy without finding the field")
}
} else {
throw IllegalArgumentException("Cannot find hierarchy unfold path of a field with no class scope")
}
}

Expand All @@ -128,5 +127,4 @@ class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boole
} ?: listOf()
}
}

}
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,7 @@ package org.jetbrains.kotlin.formver.embeddings.callables
import org.jetbrains.kotlin.formver.conversion.StmtConversionContext
import org.jetbrains.kotlin.formver.embeddings.*
import org.jetbrains.kotlin.formver.embeddings.expression.*
import org.jetbrains.kotlin.formver.names.ClassKotlinName
import org.jetbrains.kotlin.formver.names.GlobalScope
import org.jetbrains.kotlin.formver.names.ScopedKotlinName
import org.jetbrains.kotlin.formver.names.embedFunctionName
import org.jetbrains.kotlin.formver.names.*
import org.jetbrains.kotlin.formver.viper.ast.Method
import org.jetbrains.kotlin.name.CallableId
import org.jetbrains.kotlin.name.FqName
Expand Down Expand Up @@ -41,8 +38,12 @@ object KotlinContractFunction : SpecialKotlinFunction {
override val packageName: List<String> = listOf("kotlin", "contracts")
override val name: String = "contract"

private val contractBuilderType =
ClassTypeEmbedding(ScopedKotlinName(GlobalScope(packageName), ClassKotlinName(listOf("ContractBuilder"))))
private val contractBuilderTypeName = buildName {
packageScope(packageName)
globalScope()
ClassKotlinName(listOf("ContractBuilder"))
}
private val contractBuilderType = ClassTypeEmbedding(contractBuilderTypeName)
override val receiverType: TypeEmbedding? = null
override val paramTypes: List<TypeEmbedding> =
listOf(FunctionTypeEmbedding(CallableSignatureData(contractBuilderType, listOf(), UnitTypeEmbedding)))
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ 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
Expand Down Expand Up @@ -374,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)
val hierarchyPath = (receiver.type as? ClassTypeEmbedding)?.details?.hierarchyUnfoldPath(field.name as ScopedKotlinName)
hierarchyPath?.forEach { classType ->
val predAcc = classType.sharedPredicateAccessInvariant().fillHole(receiverWrapper)
.pureToViper(toBuiltin = true, ctx.source) as? Exp.PredicateAccess
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ internal sealed class NameMatcher(val name: MangledName) {
}

protected val scopedName = name as? ScopedKotlinName
protected val packageName = (scopedName?.scope as? PackagePrefixScope)?.packageName
protected val packageName = scopedName?.scope?.packageNameIfAny
protected abstract val className: ClassKotlinName?

inline fun ifPackageName(vararg segments: String, action: NameMatcher.() -> Unit) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,27 +20,44 @@ import org.jetbrains.kotlin.name.Name
* If there is a risk of collision, add a prefix.
*/

fun ClassId.embedLocalName(): ClassKotlinName = ClassKotlinName(relativeClassName)

fun CallableId.embedScopeName(): NameScope =
when (val id = this.classId) {
null -> GlobalScope(packageName)
else -> DefaultClassScope(packageName, ClassKotlinName(id.relativeClassName))
fun ScopedKotlinNameBuilder.embedScope(id: CallableId) {
packageScope(id.packageName)
when (val classId = id.classId) {
null -> globalScope()
else -> classScope(classId.embedLocalName())
}
}

fun ScopedKotlinNameBuilder.embedScope(id: ClassId) {
packageScope(id.packageFqName)
classScope(id.embedLocalName())
}

fun ClassId.embedName(): ScopedKotlinName = ScopedKotlinName(GlobalScope(packageFqName), ClassKotlinName(relativeClassName))
fun CallableId.embedExtensionGetterName(type: TypeEmbedding): ScopedKotlinName =
ScopedKotlinName(embedScopeName(), ExtensionGetterKotlinName(callableName, type))
fun ClassId.embedName(): ScopedKotlinName = buildName {
packageScope(packageFqName)
globalScope()
embedLocalName()
}

fun CallableId.embedExtensionSetterName(type: TypeEmbedding): ScopedKotlinName =
ScopedKotlinName(embedScopeName(), ExtensionSetterKotlinName(callableName, type))
fun CallableId.embedExtensionGetterName(type: TypeEmbedding): ScopedKotlinName = buildName {
embedScope(this@embedExtensionGetterName)
ExtensionGetterKotlinName(callableName, type)
}

fun CallableId.embedExtensionSetterName(type: TypeEmbedding): ScopedKotlinName = buildName {
embedScope(this@embedExtensionSetterName)
ExtensionSetterKotlinName(callableName, type)
}

private fun CallableId.embedMemberPropertyNameBase(isPrivate: Boolean, withAction: (Name) -> KotlinName): ScopedKotlinName {
val id = classId ?: error("Embedding non-member property $callableName as a member.")
val className = ClassKotlinName(id.relativeClassName)
val scope =
if (isPrivate) PrivateClassScope(packageName, className)
else PublicClassScope(packageName, className)
return ScopedKotlinName(scope, withAction(callableName))
return buildName {
embedScope(id)
if (isPrivate) privateScope() else publicScope()
withAction(callableName)
}
}

fun CallableId.embedMemberPropertyName(isPrivate: Boolean) = embedMemberPropertyNameBase(isPrivate, ::PropertyKotlinName)
Expand All @@ -49,13 +66,22 @@ fun CallableId.embedMemberSetterName(isPrivate: Boolean) = embedMemberPropertyNa
fun CallableId.embedMemberBackingFieldName(isPrivate: Boolean) = embedMemberPropertyNameBase(isPrivate, ::BackingFieldKotlinName)

fun CallableId.embedUnscopedPropertyName(): SimpleKotlinName = SimpleKotlinName(callableName)
fun CallableId.embedFunctionName(type: TypeEmbedding): ScopedKotlinName =
ScopedKotlinName(embedScopeName(), FunctionKotlinName(callableName, type))
fun CallableId.embedFunctionName(type: TypeEmbedding): ScopedKotlinName = buildName {
embedScope(this@embedFunctionName)
FunctionKotlinName(callableName, type)
}

fun Name.embedScopedLocalName(scope: Int) = buildName {
localScope(scope)
SimpleKotlinName(this@embedScopedLocalName)
}

fun Name.embedScopedLocalName(scope: Int) = ScopedKotlinName(LocalScope(scope), SimpleKotlinName(this))
fun Name.embedParameterName() = ScopedKotlinName(ParameterScope, SimpleKotlinName(this))
fun Name.embedParameterName() = buildName {
parameterScope()
SimpleKotlinName(this@embedParameterName)
}

fun FirValueParameterSymbol.embedName(): ScopedKotlinName = ScopedKotlinName(ParameterScope, SimpleKotlinName(name))
fun FirValueParameterSymbol.embedName(): ScopedKotlinName = name.embedParameterName()

fun FirPropertySymbol.embedGetterName(ctx: ProgramConversionContext): ScopedKotlinName = when (isExtension) {
true -> callableId.embedExtensionGetterName(ctx.embedType(getterSymbol!!))
Expand All @@ -71,8 +97,10 @@ fun FirPropertySymbol.embedMemberPropertyName() = callableId.embedMemberProperty
Visibilities.isPrivate(this.visibility)
)

fun FirConstructorSymbol.embedName(ctx: ProgramConversionContext): ScopedKotlinName =
ScopedKotlinName(callableId.embedScopeName(), ConstructorKotlinName(ctx.embedType(this)))
fun FirConstructorSymbol.embedName(ctx: ProgramConversionContext): ScopedKotlinName = buildName {
embedScope(callableId)
ConstructorKotlinName(ctx.embedType(this@embedName))
}

fun FirFunctionSymbol<*>.embedName(ctx: ProgramConversionContext): ScopedKotlinName = when (this) {
is FirPropertyAccessorSymbol -> if (isGetter) propertySymbol.embedGetterName(ctx) else propertySymbol.embedSetterName(ctx)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,51 +7,87 @@ package org.jetbrains.kotlin.formver.names

import org.jetbrains.kotlin.formver.viper.MangledName
import org.jetbrains.kotlin.name.FqName
import org.jetbrains.kotlin.utils.addToStdlib.ifFalse
import org.jetbrains.kotlin.utils.addToStdlib.ifTrue

sealed interface NameScope : MangledName
sealed interface NameScope {
val parent: NameScope?
val mangledScopeName: String?

sealed interface PackagePrefixScope : NameScope {
val packageName: FqName
val suffix: String
override val mangled: String
get() = if (packageName.isRoot) {
suffix
} else {
"pkg\$${packageName.asViperString()}\$$suffix"
}
// Determines whether the parent should be part of the name.
// This is a hack required by how we deal with public names.
// We use only accessible scopes when generating the names, but all scopes when doing lookups
// for things like package and class names.
val parentAccessible: Boolean
get() = true
}

data class GlobalScope(override val packageName: FqName) : PackagePrefixScope {
override val suffix = "global"
// Includes the scope itself.
val NameScope.parentScopes: Sequence<NameScope>
get() = sequence {
if (parentAccessible) parent?.parentScopes?.let { yieldAll(it) }
yield(this@parentScopes)
}

constructor(segments: List<String>) : this(FqName.fromSegments(segments))
val NameScope.allParentScopes: Sequence<NameScope>
get() = sequence {
parent?.parentScopes?.let { yieldAll(it) }
yield(this@allParentScopes)
}

val NameScope.fullMangledName: String?
get() {
val scopes = parentScopes.mapNotNull { it.mangledScopeName }.toList()
return if (scopes.isEmpty()) null else scopes.joinToString("$")
}

val NameScope.packageNameIfAny: FqName?
get() = allParentScopes.filterIsInstance<PackageScope>().firstOrNull()?.packageName

val NameScope.classNameIfAny: ClassKotlinName?
get() = allParentScopes.filterIsInstance<ClassScope>().firstOrNull()?.className

data class PackageScope(val packageName: FqName) : NameScope {
override val parent = null

override val mangledScopeName: String?
get() = packageName.isRoot.ifFalse { "pkg\$${packageName.asViperString()}" }
}

sealed interface ClassScope : PackagePrefixScope {
val className: ClassKotlinName
// This is really just package scope, here for backwards compatibility.
data class GlobalScope(override val parent: NameScope) : NameScope {
override val mangledScopeName: String
get() = "global"
}

data class DefaultClassScope(override val packageName: FqName, override val className: ClassKotlinName, ) : ClassScope {
override val suffix = className.mangled
data class ClassScope(override val parent: NameScope, val className: ClassKotlinName) : NameScope {
override val mangledScopeName: String
get() = className.mangled
}

/**
* We do not want to mangle field names with class and package, hence introducing
* this special `NameScope`. Note that it still needs package and class for other purposes.
*/
data class PublicClassScope(override val packageName: FqName, override val className: ClassKotlinName) : ClassScope {
override val suffix = className.mangled + "_public"
override val mangled = "public"
data class PublicScope(override val parent: NameScope) : NameScope {
override val mangledScopeName: String
get() = "public"
override val parentAccessible: Boolean
get() = false
}

data class PrivateClassScope(override val packageName: FqName, override val className: ClassKotlinName) : ClassScope {
override val suffix = className.mangled + "_private"
data class PrivateScope(override val parent: NameScope) : NameScope {
override val mangledScopeName: String
get() = "private"
}

data object ParameterScope : NameScope {
override val mangled = "local"
override val parent: NameScope? = null
override val mangledScopeName: String
get() = "local"
}

data class LocalScope(val level: Int) : NameScope {
override val mangled = "local$level"
override val parent: NameScope? = null
override val mangledScopeName = "local$level"
}
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,9 @@ import org.jetbrains.kotlin.name.FqName
/**
* Name of a Kotlin entity in the original program in a specified scope and optionally distinguished by type.
*/
data class ScopedKotlinName(val scope: NameScope, val name: KotlinName) : MangledName {
data class ScopedKotlinName(val scope: NameScope, val name: KotlinName) : KotlinName {
override val mangled: String
get() = listOf(scope.mangled, name.mangled).joinToString("$")
get() = listOf(scope.fullMangledName, name.mangled).joinToString("$")
}

fun FqName.asViperString() = asString().replace('.', '$')
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
/*
* 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

import org.jetbrains.kotlin.name.FqName

class ScopedKotlinNameBuilder {
private var scope: NameScope? = null

fun complete(name: KotlinName): ScopedKotlinName {
require(scope != null) { "No scope specified "}
return ScopedKotlinName(scope!!, name)
}

fun packageScope(packageName: FqName) {
require (scope == null) { "Invalid scope combination: package after $scope" }
scope = PackageScope(packageName)
}

fun packageScope(packageName: List<String>) {
require (scope == null) { "Invalid scope combination: package after $scope" }
scope = PackageScope(FqName.fromSegments(packageName))
}

fun globalScope() {
require (scope != null) { "Global scope cannot be top-level" }
scope = GlobalScope(scope!!)
}

fun classScope(className: ClassKotlinName) {
require (scope != null) { "Public class scope cannot be top-level" }
scope = ClassScope(scope!!, className)
}

fun publicScope() {
require(scope != null) { "Public class scope cannot be top-level" }
scope = PublicScope(scope!!)
}

fun privateScope() {
require(scope != null) { "Private class scope cannot be top-level" }
scope = PrivateScope(scope!!)
}

fun parameterScope() {
require(scope == null) { "Parameter scope cannot be nested." }
scope = ParameterScope
}

fun localScope(level: Int) {
require (scope == null) { "Local scope cannot be nested." }
scope = LocalScope(level)
}
}

// TODO: generalise this to work for all names.
fun buildName(init: ScopedKotlinNameBuilder.() -> KotlinName): ScopedKotlinName =
ScopedKotlinNameBuilder().let {
it.complete(it.init())
}
Loading

0 comments on commit f391ca1

Please sign in to comment.