Move Name Resolution Logic Into Resolver

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

@@ -31,10 +31,10 @@ import org.jetbrains.kotlin.formver.core.embeddings.properties.*
 import org.jetbrains.kotlin.formver.core.embeddings.types.*
 import org.jetbrains.kotlin.formver.core.names.*
 import org.jetbrains.kotlin.formver.names.SimpleNameResolver
+import org.jetbrains.kotlin.formver.names.debugMangled
 import org.jetbrains.kotlin.formver.viper.SymbolicName
 import org.jetbrains.kotlin.formver.viper.ast.Method
 import org.jetbrains.kotlin.formver.viper.ast.Program
-import org.jetbrains.kotlin.formver.viper.debugMangled
 import org.jetbrains.kotlin.utils.addIfNotNull
 import org.jetbrains.kotlin.utils.addToStdlib.ifFalse
 import org.jetbrains.kotlin.utils.addToStdlib.ifTrue

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

@@ -7,12 +7,12 @@ package org.jetbrains.kotlin.formver.core.conversion
 
 import org.jetbrains.kotlin.formver.core.embeddings.properties.FieldEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbedding
-import org.jetbrains.kotlin.formver.core.names.SpecialName
+import org.jetbrains.kotlin.formver.core.names.SpecialFieldName
 import org.jetbrains.kotlin.formver.viper.SymbolicName
 import org.jetbrains.kotlin.formver.viper.ast.Type
 
 class SpecialField(baseName: String, override val type: TypeEmbedding, override val viperType: Type) : FieldEmbedding {
-    override val name: SymbolicName = SpecialName(baseName)
+    override val name: SymbolicName = SpecialFieldName(baseName)
     override val accessPolicy: AccessPolicy = AccessPolicy.ALWAYS_WRITEABLE
     override val includeInShortDump: Boolean = false
 }

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/domains/FunctionBuilder.kt

@@ -6,7 +6,7 @@
 package org.jetbrains.kotlin.formver.core.domains
 
 import org.jetbrains.kotlin.formver.core.names.PlaceholderArgumentName
-import org.jetbrains.kotlin.formver.core.names.SpecialName
+import org.jetbrains.kotlin.formver.viper.SymbolicName
 import org.jetbrains.kotlin.formver.viper.ast.BuiltinFunction
 import org.jetbrains.kotlin.formver.viper.ast.Exp
 import org.jetbrains.kotlin.formver.viper.ast.Type
@@ -38,10 +38,10 @@ class FunctionBuilder private constructor() {
         get() = Exp.Result(retType)
 
     companion object {
-        fun build(name: String, action: FunctionBuilder.() -> Unit): BuiltinFunction {
+        fun build(name: SymbolicName, action: FunctionBuilder.() -> Unit): BuiltinFunction {
             val builder = FunctionBuilder()
             builder.action()
-            return object : BuiltinFunction(SpecialName(name)) {
+            return object : BuiltinFunction(name) {
                 override val formalArgs = builder.formalArgs.map { it.decl() }
                 override val retType: Type = builder.retType
                 override val body = builder.functionBody

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/domains/Injection.kt

@@ -6,6 +6,7 @@
 package org.jetbrains.kotlin.formver.core.domains
 
 import org.jetbrains.kotlin.formver.core.domains.RuntimeTypeDomain.Companion.isOf
+import org.jetbrains.kotlin.formver.viper.SymbolicName
 import org.jetbrains.kotlin.formver.viper.ast.*
 import org.jetbrains.kotlin.formver.viper.ast.Function
 
@@ -98,7 +99,7 @@ val Injection?.viperType: Type
  * @param additionalConditions allows to add additional preconditions and/or postconditions
  */
 class InjectionImageFunction(
-    name: String,
+    name: SymbolicName,
     val original: Applicable,
     argsInjections: List<Injection>,
     resultInjection: Injection,

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/callables/FullySpecialKotlinFunction.kt

@@ -12,13 +12,13 @@ import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbedd
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.DivIntInt
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.Implies
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.MulIntInt
+import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.NegInt
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.Not
+import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.RemIntInt
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.StringGet
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.SubCharChar
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.SubCharInt
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.SubIntInt
-import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.RemIntInt
-import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.NegInt
 import org.jetbrains.kotlin.formver.core.embeddings.expression.UnitLit
 import org.jetbrains.kotlin.formver.core.embeddings.expression.toBlock
 import org.jetbrains.kotlin.formver.core.embeddings.types.buildFunctionPretype
@@ -33,7 +33,7 @@ import org.jetbrains.kotlin.name.Name
 val SpecialKotlinFunction.callableId: CallableId
     get() = CallableId(FqName.fromSegments(packageName), className?.let { FqName(it) }, Name.identifier(name))
 
-fun SpecialKotlinFunction.embedName(): ScopedKotlinName = callableId.embedFunctionName(callableType)
+fun SpecialKotlinFunction.embedName(): ScopedName = callableId.embedFunctionName(callableType)
 
 /**
  * We store here all the __Kotlin__ functions that need a (fully) special `ExpEmbedding`.

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/expression/ExpEmbedding.kt

@@ -21,12 +21,12 @@ import org.jetbrains.kotlin.formver.core.linearization.LinearizationContext
 import org.jetbrains.kotlin.formver.core.linearization.pureToViper
 import org.jetbrains.kotlin.formver.core.purity.PurityContext
 import org.jetbrains.kotlin.formver.names.SimpleNameResolver
+import org.jetbrains.kotlin.formver.names.debugMangled
 import org.jetbrains.kotlin.formver.viper.NameResolver
 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.formver.viper.ast.Stmt
-import org.jetbrains.kotlin.formver.viper.debugMangled
 import org.jetbrains.kotlin.formver.viper.mangled
 
 sealed interface ExpEmbedding : DebugPrintable {

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/expression/OperatorExpEmbeddingBuilder.kt

@@ -11,6 +11,8 @@ import org.jetbrains.kotlin.formver.core.embeddings.types.FunctionPretypeBuilder
 import org.jetbrains.kotlin.formver.core.embeddings.types.FunctionTypeEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.types.buildFunctionPretype
 import org.jetbrains.kotlin.formver.core.embeddings.types.injection
+import org.jetbrains.kotlin.formver.core.names.DomainAssociatedFuncName
+import org.jetbrains.kotlin.formver.viper.SymbolicName
 import org.jetbrains.kotlin.formver.viper.ast.*
 
 /**
@@ -20,7 +22,7 @@ import org.jetbrains.kotlin.formver.viper.ast.*
  * Then we should just set its signature (`(Int, Int) -> Int`) and Viper implementation (`Exp.Add`).
  */
 class OperatorExpEmbeddingBuilder {
-    private var runtimeTypeFunctionName: String? = null
+    private var runtimeTypeFunctionName: SymbolicName? = null
     private var viperApplicable: Applicable? = null
     private var callableType: FunctionTypeEmbedding? = null
     private var additionalConditions: (FunctionBuilder.() -> Unit)? = null
@@ -41,7 +43,7 @@ class OperatorExpEmbeddingBuilder {
 
     fun setName(name: String) {
         check(runtimeTypeFunctionName == null) { "Name for underlying viper function is already set." }
-        runtimeTypeFunctionName = name
+        runtimeTypeFunctionName = DomainAssociatedFuncName(name)
     }
 
     fun setSignature(signature: FunctionTypeEmbedding) {

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/properties/FieldEmbedding.kt

@@ -14,8 +14,8 @@ import org.jetbrains.kotlin.formver.core.embeddings.expression.IntLit
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings
 import org.jetbrains.kotlin.formver.core.embeddings.types.*
 import org.jetbrains.kotlin.formver.core.names.NameMatcher
-import org.jetbrains.kotlin.formver.core.names.ScopedKotlinName
-import org.jetbrains.kotlin.formver.core.names.SpecialName
+import org.jetbrains.kotlin.formver.core.names.ScopedName
+import org.jetbrains.kotlin.formver.core.names.SpecialFieldName
 import org.jetbrains.kotlin.formver.viper.SymbolicName
 import org.jetbrains.kotlin.formver.viper.ast.Field
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
@@ -55,7 +55,7 @@ interface FieldEmbedding {
 }
 
 class UserFieldEmbedding(
-    override val name: ScopedKotlinName,
+    override val name: ScopedName,
     override val type: TypeEmbedding,
     override val symbol: FirPropertySymbol,
     override val isUnique: Boolean,
@@ -80,7 +80,7 @@ class UserFieldEmbedding(
 
 
 object ListSizeFieldEmbedding : FieldEmbedding {
-    override val name = SpecialName("size")
+    override val name = SpecialFieldName("size")
     override val type = buildType { int() }
     override val viperType = Type.Ref
     override val accessPolicy = AccessPolicy.ALWAYS_WRITEABLE
@@ -94,7 +94,7 @@ object ListSizeFieldEmbedding : FieldEmbedding {
     }
 }
 
-fun ScopedKotlinName.specialEmbedding(embedding: ClassTypeEmbedding): FieldEmbedding? =
+fun ScopedName.specialEmbedding(embedding: ClassTypeEmbedding): FieldEmbedding? =
     NameMatcher.Companion.matchClassScope(this) {
         ifBackingFieldName("size") {
             return embedding.isCollectionInheritor.ifTrue {

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/types/ClassEmbeddingDetails.kt

@@ -6,8 +6,8 @@
 package org.jetbrains.kotlin.formver.core.embeddings.types
 
 import org.jetbrains.kotlin.formver.core.embeddings.properties.FieldEmbedding
-import org.jetbrains.kotlin.formver.core.names.PredicateKotlinName
-import org.jetbrains.kotlin.formver.core.names.ScopedKotlinName
+import org.jetbrains.kotlin.formver.core.names.PredicateName
+import org.jetbrains.kotlin.formver.core.names.ScopedName
 import org.jetbrains.kotlin.formver.core.names.SimpleKotlinName
 import org.jetbrains.kotlin.formver.core.names.asScope
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
@@ -78,8 +78,8 @@ class ClassEmbeddingDetails(
         }
     }
 
-    private val sharedPredicateName = ScopedKotlinName(type.name.asScope(), PredicateKotlinName("shared"))
-    private val uniquePredicateName = ScopedKotlinName(type.name.asScope(), PredicateKotlinName("unique"))
+    private val sharedPredicateName = ScopedName(type.name.asScope(), PredicateName("shared"))
+    private val uniquePredicateName = ScopedName(type.name.asScope(), PredicateName("unique"))
 
     /**
      * Find an embedding of a backing field by this name amongst the ancestors of this type.

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/types/ClassPredicateBuilder.kt

@@ -12,7 +12,6 @@ import org.jetbrains.kotlin.formver.core.linearization.pureToViper
 import org.jetbrains.kotlin.formver.core.names.DispatchReceiverName
 import org.jetbrains.kotlin.formver.core.names.SimpleKotlinName
 import org.jetbrains.kotlin.formver.viper.SymbolicName
-import org.jetbrains.kotlin.formver.viper.NameResolver
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
 import org.jetbrains.kotlin.formver.viper.ast.Predicate
 import org.jetbrains.kotlin.name.Name
@@ -71,10 +70,6 @@ class FieldAssertionsBuilder(private val subject: VariableEmbedding, private val
     val isAlwaysReadable = field.accessPolicy == AccessPolicy.ALWAYS_READABLE
     val isUnique = field.isUnique
 
-    context(nameResolver: NameResolver)
-    val nameAsString: String
-        get() = field.name.name.mangledBaseName
-
     fun forType(action: TypeInvariantsBuilder.() -> Unit) {
         val builder = TypeInvariantsBuilder(field.type)
         builder.action()

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/types/ClassTypeEmbedding.kt

@@ -10,13 +10,13 @@ import org.jetbrains.kotlin.formver.core.domains.RuntimeTypeDomain
 import org.jetbrains.kotlin.formver.core.embeddings.expression.ExpEmbedding
 import org.jetbrains.kotlin.formver.core.linearization.pureToViper
 import org.jetbrains.kotlin.formver.core.names.NameMatcher
-import org.jetbrains.kotlin.formver.core.names.ScopedKotlinName
+import org.jetbrains.kotlin.formver.core.names.ScopedName
+import org.jetbrains.kotlin.formver.names.debugMangled
 import org.jetbrains.kotlin.formver.viper.ast.DomainFunc
 import org.jetbrains.kotlin.formver.viper.ast.Exp
-import org.jetbrains.kotlin.formver.viper.debugMangled
 
 // TODO: incorporate generic parameters.
-data class ClassTypeEmbedding(override val name: ScopedKotlinName) : PretypeEmbedding {
+data class ClassTypeEmbedding(override val name: ScopedName) : PretypeEmbedding {
     private var _details: ClassEmbeddingDetails? = null
     val details: ClassEmbeddingDetails
         get() = _details ?: error("Details of $name have not been initialised yet.")

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/types/FunctionTypeEmbedding.kt

@@ -6,7 +6,9 @@
 package org.jetbrains.kotlin.formver.core.embeddings.types
 
 import org.jetbrains.kotlin.formver.core.domains.RuntimeTypeDomain
-import org.jetbrains.kotlin.formver.core.names.SetOfNames
+import org.jetbrains.kotlin.formver.core.names.FunctionTypeName
+import org.jetbrains.kotlin.formver.core.names.ListOfNames
+import org.jetbrains.kotlin.formver.core.names.NameOfType
 
 data class FunctionTypeEmbedding(
     val dispatchReceiverType: TypeEmbedding?,
@@ -17,7 +19,8 @@ data class FunctionTypeEmbedding(
 ) : PretypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.functionType()
 
-    override val name: SetOfNames = SetOfNames(formalArgTypes.map { it -> it.name } + listOf(returnType.name))
+    private val argsTypeNames = ListOfNames<NameOfType>(formalArgTypes.map { it.name })
+    override val name: FunctionTypeName = FunctionTypeName(argsTypeNames, returnType.name)
 
     /**
      * The flattened structure of the callable parameters: in case the callable has a receiver

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/types/PretypeBuilder.kt

@@ -5,7 +5,7 @@
 
 package org.jetbrains.kotlin.formver.core.embeddings.types
 
-import org.jetbrains.kotlin.formver.core.names.ScopedKotlinName
+import org.jetbrains.kotlin.formver.core.names.ScopedName
 
 /**
  * We use "pretype" to refer to types that do not contain information on nullability or
@@ -90,9 +90,9 @@ fun buildFunctionPretype(init: FunctionPretypeBuilder.() -> Unit): FunctionTypeE
     FunctionPretypeBuilder().apply(init).complete()
 
 class ClassPretypeBuilder : PretypeBuilder {
-    private var className: ScopedKotlinName? = null
+    private var className: ScopedName? = null
 
-    fun withName(name: ScopedKotlinName) {
+    fun withName(name: ScopedName) {
         require(className == null) { "Class name already set" }
         className = name
     }

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/types/TypeEmbedding.kt

@@ -14,7 +14,7 @@ import org.jetbrains.kotlin.formver.core.embeddings.expression.debug.PlaintextLe
 import org.jetbrains.kotlin.formver.core.embeddings.expression.debug.TreeView
 import org.jetbrains.kotlin.formver.core.embeddings.properties.FieldEmbedding
 import org.jetbrains.kotlin.formver.core.linearization.pureToViper
-import org.jetbrains.kotlin.formver.core.names.HavocKotlinName
+import org.jetbrains.kotlin.formver.core.names.HavocName
 import org.jetbrains.kotlin.formver.core.names.PlaceholderReturnVariableName
 import org.jetbrains.kotlin.formver.core.names.TypeName
 import org.jetbrains.kotlin.formver.viper.NameResolver
@@ -37,11 +37,11 @@ data class TypeEmbedding(val pretype: PretypeEmbedding, val flags: TypeEmbedding
      * It may at some point necessary to make a `TypeName` hierarchy of some sort to
      * represent these names, but we do it inline for now.
      */
-    val name: SymbolicName
+    val name: TypeName
         get() = TypeName(pretype, flags.nullable)
 
     val havocMethodName: SymbolicName by lazy {
-        HavocKotlinName(this)
+        HavocName(this)
     }
 
     val havocMethod: Method by lazy {

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/names/ClassScopeNameMatcher.kt

@@ -20,7 +20,7 @@ internal sealed class NameMatcher(val name: SymbolicName) {
         }
     }
 
-    protected val scopedName = name as? ScopedKotlinName
+    protected val scopedName = name as? ScopedName
     protected val packageName = scopedName?.scope?.packageNameIfAny
     protected abstract val className: ClassKotlinName?
 

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/names/FreshName.kt

@@ -0,0 +1,79 @@
+/*
+ * Copyright 2010-2023 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.core.names
+
+import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbedding
+import org.jetbrains.kotlin.formver.viper.NameType
+import org.jetbrains.kotlin.formver.viper.NameType.Label
+import org.jetbrains.kotlin.formver.viper.SymbolicName
+
+/* This file contains mangled names for constructs introduced during the conversion to Viper.
+ *
+ * See the NameEmbeddings file for guidelines on good name choices.
+ */
+
+
+sealed interface FreshName : SymbolicName
+
+abstract class TypedFreshName(override val mangledType: NameType, val baseName: String) : FreshName {
+}
+
+/**
+ * Representation for names not present in the original source,
+ * e.g. storage for the result of subexpressions.
+ */
+data class AnonymousName(val n: Int) : TypedFreshName(NameType.Base.Variable, "anon$$n")
+
+data class AnonymousBuiltinName(val n: Int) : TypedFreshName(NameType.Base.Variable, $$"anon$builtin$$$n")
+
+/**
+ * Name for return variable that should *only* be used in signatures of methods without a body.
+ */
+data object PlaceholderReturnVariableName : TypedFreshName(NameType.Base.Variable, "ret")
+
+data class ReturnVariableName(val n: Int) : TypedFreshName(NameType.Base.Variable, "ret$$n")
+
+/**
+ * Name for return variable that should *only* be used in signatures of pure functions
+ * This variable will be translated into the special result variable in Viper
+ */
+data object FunctionResultVariableName : TypedFreshName(NameType.Base.Variable, "result")
+
+data object DispatchReceiverName : TypedFreshName(NameType.Base.Variable, $$"this$dispatch")
+
+data object ExtensionReceiverName : TypedFreshName(NameType.Base.Variable, $$"this$extension")
+
+data class SpecialFieldName(val name: String) : TypedFreshName(NameType.Member.Property, name)
+
+
+abstract class NumberedLabelName(override val mangledType: NameType, originalN: Int) :
+    TypedFreshName(mangledType, originalN.toString())
+
+data class ReturnLabelName(val n: Int) : NumberedLabelName(Label.Return, n)
+data class BreakLabelName(val n: Int) : NumberedLabelName(Label.Break, n)
+data class ContinueLabelName(val n: Int) : NumberedLabelName(Label.Continue, n)
+data class CatchLabelName(val n: Int) : NumberedLabelName(Label.Catch, n)
+data class TryExitLabelName(val n: Int) : NumberedLabelName(Label.TryExit, n)
+
+
+data class DomainAssociatedFuncName(val name: String) : TypedFreshName(NameType.Base.DomainFunction, name)
+
+data class PlaceholderArgumentName(val n: Int) : TypedFreshName(NameType.Base.Variable, "arg$$n")
+
+data class DomainFuncParameterName(val name: String) : TypedFreshName(NameType.Base.Variable, name)
+
+data class SsaVariableName(val ssaIndex: Int, val baseName: SymbolicName) : FreshName {
+    override val mangledType: NameType
+        get() = NameType.Base.Variable
+
+}
+
+data class PredicateName(val name: String) : TypedFreshName(NameType.Base.Predicate, name)
+
+data class HavocName(val type: TypeEmbedding) : SymbolicName {
+    override val mangledType: NameType
+        get() = NameType.Base.Havoc
+}