Shorten mangled names and make type/scope/name distinction explicit

Our current mangled names are inconveniently long.  I'm working on
making them shorter, but it's quite a bit of work; this should make
things a bit easier to read without reworking too much.

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

@@ -25,6 +25,7 @@ import org.jetbrains.kotlin.formver.linearization.SharedLinearizationState
 import org.jetbrains.kotlin.formver.names.*
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.Program
+import org.jetbrains.kotlin.formver.viper.mangled
 import org.jetbrains.kotlin.utils.addIfNotNull
 import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
 

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/domains/RuntimeTypeDomain.kt

@@ -8,9 +8,10 @@ package org.jetbrains.kotlin.formver.domains
 import org.jetbrains.kotlin.formver.embeddings.ClassTypeEmbedding
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.*
+import org.jetbrains.kotlin.formver.viper.mangled
 
 
-const val RUNTIME_TYPE_DOMAIN_NAME = "RuntimeType"
+const val RUNTIME_TYPE_DOMAIN_NAME = "RT"
 
 
 /**

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

@@ -8,14 +8,14 @@ package org.jetbrains.kotlin.formver.embeddings
 import org.jetbrains.kotlin.formver.conversion.AccessPolicy
 import org.jetbrains.kotlin.formver.embeddings.expression.*
 import org.jetbrains.kotlin.formver.linearization.pureToViper
-import org.jetbrains.kotlin.formver.names.ClassPredicateSubjectName
+import org.jetbrains.kotlin.formver.names.ThisReceiverName
 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.utils.addIfNotNull
 
 internal class ClassPredicateBuilder private constructor(private val type: ClassTypeEmbedding) {
-    private val subject = PlaceholderVariableEmbedding(ClassPredicateSubjectName, type)
+    private val subject = PlaceholderVariableEmbedding(ThisReceiverName, type)
     private val body = mutableListOf<ExpEmbedding>()
 
     companion object {

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

@@ -8,14 +8,13 @@ package org.jetbrains.kotlin.formver.embeddings
 import org.jetbrains.kotlin.formver.domains.Injection
 import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain
 import org.jetbrains.kotlin.formver.embeddings.callables.CallableSignatureData
-import org.jetbrains.kotlin.formver.names.ClassScope
+import org.jetbrains.kotlin.formver.names.*
 import org.jetbrains.kotlin.formver.names.NameMatcher
-import org.jetbrains.kotlin.formver.names.ScopedKotlinName
-import org.jetbrains.kotlin.formver.names.SimpleKotlinName
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.Exp
 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
 
 /**
@@ -106,49 +105,42 @@ fun <R> TypeEmbedding.mapNotNullUniqueFields(action: (SimpleKotlinName, FieldEmb
 
 data object UnitTypeEmbedding : TypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.unitType()
-    override val name = object : MangledName {
-        override val mangled: String = "T_Unit"
-    }
+    override val name = TypeName("Unit")
 }
 
 data object NothingTypeEmbedding : TypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.nothingType()
-    override val name = object : MangledName {
-        override val mangled: String = "T_Nothing"
-    }
+    override val name = TypeName("Nothing")
 
     override fun pureInvariants(): List<TypeInvariantEmbedding> = listOf(FalseTypeInvariant)
 }
 
 data object AnyTypeEmbedding : TypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.anyType()
-    override val name = object : MangledName {
-        override val mangled: String = "T_Any"
-    }
+    override val name = TypeName("Any")
 }
 
 data object NullableAnyTypeEmbedding : TypeEmbedding by NullableTypeEmbedding(AnyTypeEmbedding)
 
 data object IntTypeEmbedding : TypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.intType()
-    override val name = object : MangledName {
-        override val mangled: String = "T_Int"
-    }
+    override val name = TypeName("Int")
 }
 
 
 data object BooleanTypeEmbedding : TypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.boolType()
-    override val name = object : MangledName {
-        override val mangled: String = "T_Boolean"
-    }
+    override val name = TypeName("Boolean")
 }
 
 
 data class NullableTypeEmbedding(val elementType: TypeEmbedding) : TypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.nullable(elementType.runtimeType)
     override val name = object : MangledName {
-        override val mangled: String = "N" + elementType.name.mangled
+        override val mangledScope: String?
+            get() = elementType.name.mangledScope?.let { "N$it" }
+        override val mangledBaseName: String
+            get() = elementType.name.mangledBaseName
     }
 
     override fun accessInvariants(): List<TypeInvariantEmbedding> = elementType.accessInvariants().map { IfNonNullInvariant(it) }
@@ -170,8 +162,11 @@ data class NullableTypeEmbedding(val elementType: TypeEmbedding) : TypeEmbedding
 data class FunctionTypeEmbedding(val signature: CallableSignatureData) : TypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.functionType()
     override val name = object : MangledName {
-        override val mangled: String =
-            "fun_take\$${signature.formalArgTypes.joinToString("$") { it.name.mangled }}\$return\$${signature.returnType.name.mangled}"
+        // TODO: this can cause some number of collisions; fix it if it becomes an issue.
+        override val mangledBaseName: String =
+            signature.formalArgTypes.joinToString("$") { it.name.mangled }
+        override val mangledType: String
+            get() = "TF"
     }
 }
 
@@ -237,12 +232,13 @@ data class ClassTypeEmbedding(val className: ScopedKotlinName, val isInterface:
     }
 
     // TODO: incorporate generic parameters.
-    override val name = object : MangledName {
-        override val mangled: String = "T_class_${className.mangled}"
-    }
+    override val name = TypeName("class_${className.mangled}")
 
     private val uniquePredicateName = object : MangledName {
-        override val mangled: String = "Unique\$T_class_${className.mangled}"
+        override val mangledType: String
+            get() = "U"
+        override val mangledBaseName: String
+            get() = name.mangled
     }
 
     val runtimeTypeFunc = RuntimeTypeDomain.classTypeFunc(name)

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

@@ -17,6 +17,7 @@ import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.Exp
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
 import org.jetbrains.kotlin.formver.viper.ast.Stmt
+import org.jetbrains.kotlin.formver.viper.mangled
 
 sealed interface ExpEmbedding {
     val type: TypeEmbedding

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

@@ -17,6 +17,7 @@ import org.jetbrains.kotlin.formver.embeddings.expression.debug.TreeView
 import org.jetbrains.kotlin.formver.names.AnonymousName
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.*
+import org.jetbrains.kotlin.formver.viper.mangled
 
 sealed interface VariableEmbedding : PureExpEmbedding, PropertyAccessEmbedding {
     val name: MangledName

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

@@ -10,6 +10,7 @@ import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.callables.NamedFunctionSignature
 import org.jetbrains.kotlin.formver.viper.ast.Label
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
+import org.jetbrains.kotlin.formver.viper.mangled
 
 val Label.debugTreeView: TreeView
     get() = PlaintextLeaf(name.mangled)

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

@@ -17,51 +17,56 @@ import org.jetbrains.kotlin.formver.viper.MangledName
  * e.g. storage for the result of subexpressions.
  */
 data class AnonymousName(val n: Int) : MangledName {
-    override val mangled: String
-        get() = "anonymous\$$n"
+    override val mangledType: String
+        get() = "a"
+    override val mangledBaseName: String
+        get() = n.toString()
 }
 
 /**
  * Name for return variable that should *only* be used in signatures of methods without a body.
  */
 data object PlaceholderReturnVariableName : MangledName {
-    override val mangled: String
+    override val mangledBaseName: String
         get() = "ret"
 }
 
 data class ReturnVariableName(val n: Int) : MangledName {
-    override val mangled: String
-        get() = "ret\$$n"
+    override val mangledType: String
+        get() = "r"
+    override val mangledBaseName: String
+        get() = n.toString()
 }
 
 data object ThisReceiverName : MangledName {
-    override val mangled: String
+    override val mangledBaseName: String
         get() = "this"
 }
 
 data object SetterValueName : MangledName {
-    override val mangled = "value"
+    override val mangledBaseName: String
+        get() = "value"
 }
 
-abstract class SpecialNameBase(name: String) : MangledName {
-    override val mangled: String = "special\$$name"
+data class SpecialName(override val mangledBaseName: String) : MangledName {
+    override val mangledType: String
+        get() = "sp"
 }
 
-data class SpecialName(val name: String) : SpecialNameBase(name)
-data object GetterFunctionSubjectName : SpecialNameBase("get\$function\$subject")
-data object ClassPredicateSubjectName : SpecialNameBase("class\$predicate\$subject")
-
-data class GetterFunctionName(val className: MangledName, val fieldName: MangledName) : MangledName {
-    override val mangled: String
-        get() = "${className.mangled}\$get\$${fieldName.mangled}"
-}
-
-abstract class NumberedLabelName(kind: String, n: Int) : MangledName {
-    override val mangled = "label\$$kind\$$n"
+abstract class NumberedLabelName(override val mangledScope: String, n: Int) : MangledName {
+    override val mangledType: String
+        get() = "lbl"
+    override val mangledBaseName: String = n.toString()
 }
 
 data class ReturnLabelName(val scopeDepth: Int) : NumberedLabelName("ret", scopeDepth)
 data class BreakLabelName(val n: Int) : NumberedLabelName("break", n)
 data class ContinueLabelName(val n: Int) : NumberedLabelName("continue", n)
 data class CatchLabelName(val n: Int) : NumberedLabelName("catch", n)
 data class TryExitLabelName(val n: Int) : NumberedLabelName("try_exit", n)
+
+data class TypeName(override val mangledBaseName: String) : MangledName {
+    override val mangledType: String
+        get() = "T"
+}
+

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

@@ -5,8 +5,10 @@
 
 package org.jetbrains.kotlin.formver.names
 
+import org.jetbrains.kotlin.formver.embeddings.ClassTypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
 import org.jetbrains.kotlin.formver.viper.MangledName
+import org.jetbrains.kotlin.formver.viper.mangled
 import org.jetbrains.kotlin.name.FqName
 import org.jetbrains.kotlin.name.Name
 
@@ -19,44 +21,46 @@ import org.jetbrains.kotlin.name.Name
 sealed interface KotlinName : MangledName
 
 data class SimpleKotlinName(val name: Name) : KotlinName {
-    override val mangled: String = name.asStringStripSpecialMarkers()
+    override val mangledBaseName: String = name.asStringStripSpecialMarkers()
 }
 
-abstract class PrefixedKotlinName(prefix: String, name: Name) : KotlinName {
-    override val mangled: String = "${prefix}_${name.asStringStripSpecialMarkers()}"
+abstract class TypedKotlinName(override val mangledType: String, name: Name) : KotlinName {
+    override val mangledBaseName: String = name.asStringStripSpecialMarkers()
 }
 
-abstract class PrefixedKotlinNameWithType(prefix: String, name: Name, type: TypeEmbedding) : KotlinName {
-    override val mangled: String = "${prefix}_${name.asStringStripSpecialMarkers()}\$${type.name.mangled}"
+abstract class TypedKotlinNameWithType(override val mangledType: String, name: Name, type: TypeEmbedding) : KotlinName {
+    override val mangledBaseName: String = "${name.asStringStripSpecialMarkers()}\$${type.name.mangled}"
 }
 
-data class FunctionKotlinName(val name: Name, val type: TypeEmbedding) : PrefixedKotlinNameWithType("fun", name, type)
+data class FunctionKotlinName(val name: Name, val type: TypeEmbedding) : TypedKotlinNameWithType("f", name, type)
 
 /**
  * This name will never occur in the viper output, but rather is used to lookup properties.
  */
-data class PropertyKotlinName(val name: Name) : PrefixedKotlinName("property_property", name)
-data class BackingFieldKotlinName(val name: Name) : PrefixedKotlinName("backing_field", name)
-data class GetterKotlinName(val name: Name) : PrefixedKotlinName("property_getter", name)
-data class SetterKotlinName(val name: Name) : PrefixedKotlinName("property_setter", name)
-data class ExtensionSetterKotlinName(val name: Name, val type: TypeEmbedding) : PrefixedKotlinNameWithType(
-    "ext_setter",
+data class PropertyKotlinName(val name: Name) : TypedKotlinName("pp", name)
+data class BackingFieldKotlinName(val name: Name) : TypedKotlinName("bf", name)
+data class GetterKotlinName(val name: Name) : TypedKotlinName("pg", name)
+data class SetterKotlinName(val name: Name) : TypedKotlinName("ps", name)
+data class ExtensionSetterKotlinName(val name: Name, val type: TypeEmbedding) : TypedKotlinNameWithType(
+    "es",
     name, type
 )
 
-data class ExtensionGetterKotlinName(val name: Name, val type: TypeEmbedding) : PrefixedKotlinNameWithType
-    (
-    "ext_getter",
-    name, type
-)
+data class ExtensionGetterKotlinName(val name: Name, val type: TypeEmbedding) : TypedKotlinNameWithType
+    ("es", name, type)
 
 data class ClassKotlinName(val name: FqName) : KotlinName {
-    override val mangled: String = "class_${name.asViperString()}"
+    override val mangledType: String
+        get() = "c"
+    override val mangledBaseName: String = name.asViperString()
 
     constructor(classSegments: List<String>) : this(FqName.fromSegments(classSegments))
 }
 
 data class ConstructorKotlinName(val type: TypeEmbedding) : KotlinName {
-    override val mangled: String = "constructor\$${type.name.mangled}"
+    override val mangledType: String
+        get() = "con"
+    override val mangledBaseName: String
+        get() = type.name.mangledBaseName
 }
 

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

@@ -9,6 +9,7 @@ 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

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/names/NameMangling.md

@@ -0,0 +1,41 @@
+# Name mangling
+
+There are two hard problems in computer science:
+cache invalidation, naming, and off-by-one errors.
+
+When translating Kotlin to Viper, we need to pick distinct names for objects.
+Viper is significantly less forgiving than Kotlin when it comes to shadowing,
+so we aim to pick unique names globally.
+
+We do this by scoping and typing the names:
+* Names are given a scope corresponding (roughly) to their scope in the original
+  Kotlin program.
+* Names are given a type based on the kind of thing they refer to.
+
+Since this typically makes names long, we use abbreviations, or omit the type
+and/or scope for the most common cases.
+
+For scopes:
+* `pkg` for package
+* `g` for global
+* `p` for parameter
+* `ln` for local, where `n` is the number of the scope.
+
+For types:
+* `c` for class
+* `f` for function
+* `d` for domain
+* `l` for label
+* `a` for anonymous value
+* `con` for constructor
+* `pp` for property (internal use only)
+* `bf` for backing field
+* `pg` for property getter
+* `ps` for property setter
+* `eg` for extension getter
+* `es` for extension setter
+
+There are still holdover (longer) names.
+
+Ideally, we would like this system to be modular and configurable, dropping
+prefixes when they are unused, etc.  However, that is WIP.