Split TypeEmbedding into a PretypeEmbedding and flags. (#241)

This makes it easier to uniformly track flags for our embeddings; in
Kotlin this is normally just nullability, but we also need to track
uniqueness and borrowing.

This PR just restructures the code, it doesn't add any new support for
unique/borrowing yet.

The PR does not attempt to fix the naming issues; it would be good to
structure naming better, but I'll do that in a follow-up PR.

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

@@ -9,7 +9,7 @@ import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirValueParameterSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol
-import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.callables.FunctionSignature
 import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
 import org.jetbrains.kotlin.formver.embeddings.expression.PlaceholderVariableEmbedding

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

@@ -13,11 +13,12 @@ import org.jetbrains.kotlin.fir.types.resolvedType
 import org.jetbrains.kotlin.formver.ErrorCollector
 import org.jetbrains.kotlin.formver.PluginConfiguration
 import org.jetbrains.kotlin.formver.embeddings.PropertyEmbedding
-import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.callables.FunctionEmbedding
 import org.jetbrains.kotlin.formver.embeddings.callables.FunctionSignature
 import org.jetbrains.kotlin.formver.embeddings.expression.AnonymousVariableEmbedding
 import org.jetbrains.kotlin.formver.embeddings.expression.VariableEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.FunctionTypeEmbedding
 import org.jetbrains.kotlin.formver.names.CatchLabelName
 import org.jetbrains.kotlin.formver.names.TryExitLabelName
 
@@ -36,7 +37,7 @@ interface ProgramConversionContext {
     fun embedFunction(symbol: FirFunctionSymbol<*>): FunctionEmbedding
     fun embedFunctionSignature(symbol: FirFunctionSymbol<*>): FunctionSignature
     fun embedType(type: ConeKotlinType): TypeEmbedding
-    fun embedType(symbol: FirFunctionSymbol<*>): TypeEmbedding
+    fun embedFunctionPretype(symbol: FirFunctionSymbol<*>): FunctionTypeEmbedding
     fun embedType(exp: FirExpression): TypeEmbedding = embedType(exp.resolvedType)
     fun embedProperty(symbol: FirPropertySymbol): PropertyEmbedding
 }

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

@@ -21,6 +21,16 @@ import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain
 import org.jetbrains.kotlin.formver.embeddings.*
 import org.jetbrains.kotlin.formver.embeddings.callables.*
 import org.jetbrains.kotlin.formver.embeddings.expression.*
+import org.jetbrains.kotlin.formver.embeddings.types.ClassEmbeddingDetails
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.ClassTypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.FunctionPretypeBuilder
+import org.jetbrains.kotlin.formver.embeddings.types.FunctionTypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.PretypeBuilder
+import org.jetbrains.kotlin.formver.embeddings.types.TypeBuilder
+import org.jetbrains.kotlin.formver.embeddings.types.buildClassPretype
+import org.jetbrains.kotlin.formver.embeddings.types.buildFunctionPretype
+import org.jetbrains.kotlin.formver.embeddings.types.buildType
 import org.jetbrains.kotlin.formver.linearization.Linearizer
 import org.jetbrains.kotlin.formver.linearization.SeqnBuilder
 import org.jetbrains.kotlin.formver.linearization.SharedLinearizationState
@@ -122,9 +132,9 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
     private fun embedClass(symbol: FirRegularClassSymbol): ClassTypeEmbedding {
         val className = symbol.classId.embedName()
         val embedding = classes.getOrPut(className) {
-            buildType {
-                klass { withName(className) }
-            } as ClassTypeEmbedding
+            buildClassPretype {
+                withName(className)
+            }
         }
         if (embedding.hasDetails) return embedding
 
@@ -142,7 +152,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
         // `ProgramConverter`.
 
         // Phase 1
-        newDetails.initSuperTypes(symbol.resolvedSuperTypes.map(::embedType))
+        newDetails.initSuperTypes(symbol.resolvedSuperTypes.map { embedType(it).pretype })
 
         // Phase 2
         val properties = symbol.propertySymbols
@@ -157,20 +167,8 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
     override fun embedType(type: ConeKotlinType): TypeEmbedding = buildType { embedTypeWithBuilder(type) }
 
     // Note: keep in mind that this function is necessary to resolve the name of the function!
-    override fun embedType(symbol: FirFunctionSymbol<*>): FunctionTypeEmbedding = buildFunctionType {
-        symbol.receiverType?.let {
-            withDispatchReceiver { embedTypeWithBuilder(it) }
-        }
-        symbol.extensionReceiverType?.let {
-            withExtensionReceiver { embedTypeWithBuilder(it) }
-        }
-        symbol.valueParameterSymbols.forEach { param ->
-            withParam {
-                embedTypeWithBuilder(param.resolvedReturnType)
-            }
-        }
-        withReturnType { embedTypeWithBuilder(symbol.resolvedReturnType) }
-        returnsUnique = symbol.isUnique(session) || symbol is FirConstructorSymbol
+    override fun embedFunctionPretype(symbol: FirFunctionSymbol<*>): FunctionTypeEmbedding = buildFunctionPretype {
+        embedFunctionPretypeWithBuilder(symbol)
     }
 
     override fun embedProperty(symbol: FirPropertySymbol): PropertyEmbedding = if (symbol.isExtension) {
@@ -210,7 +208,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
         val isExtensionReceiverUnique = symbol.receiverParameter?.isUnique(session) ?: false
         val isExtensionReceiverBorrowed = symbol.receiverParameter?.isBorrowed(session) ?: false
         return object : FunctionSignature {
-            override val type: FunctionTypeEmbedding = embedType(symbol)
+            override val callableType: FunctionTypeEmbedding = embedFunctionPretype(symbol)
 
             // TODO: figure out whether we want a symbol here and how to get it.
             override val dispatchReceiver = dispatchReceiverType?.let {
@@ -272,7 +270,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
                 addAll(returnVariable.pureInvariants())
                 addAll(returnVariable.provenInvariants())
                 addAll(returnVariable.allAccessInvariants())
-                if (subSignature.type.returnsUnique) {
+                if (subSignature.callableType.returnsUnique) {
                     addIfNotNull(returnVariable.uniquePredicateAccessInvariant())
                 }
                 addAll(contractVisitor.getPostconditions(ContractVisitorContext(returnVariable, symbol)))
@@ -384,7 +382,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
 
     private fun convertMethodWithBody(declaration: FirSimpleFunction, signature: FullNamedFunctionSignature): FunctionBodyEmbedding? {
         val firBody = declaration.body ?: return null
-        val returnTarget = returnTargetProducer.getFresh(signature.type.returnType)
+        val returnTarget = returnTargetProducer.getFresh(signature.callableType.returnType)
         val methodCtx =
             MethodConverter(
                 this,
@@ -436,6 +434,22 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
         else -> unimplementedTypeEmbedding(type)
     }
 
+    private fun FunctionPretypeBuilder.embedFunctionPretypeWithBuilder(symbol: FirFunctionSymbol<*>) {
+        symbol.receiverType?.let {
+            withDispatchReceiver { embedTypeWithBuilder(it) }
+        }
+        symbol.extensionReceiverType?.let {
+            withExtensionReceiver { embedTypeWithBuilder(it) }
+        }
+        symbol.valueParameterSymbols.forEach { param ->
+            withParam {
+                embedTypeWithBuilder(param.resolvedReturnType)
+            }
+        }
+        withReturnType { embedTypeWithBuilder(symbol.resolvedReturnType) }
+        returnsUnique = symbol.isUnique(session) || symbol is FirConstructorSymbol
+    }
+
     private fun TypeBuilder.unimplementedTypeEmbedding(type: ConeKotlinType): PretypeBuilder =
         when (config.behaviour) {
             UnsupportedFeatureBehaviour.THROW_EXCEPTION ->

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

@@ -8,7 +8,7 @@ package org.jetbrains.kotlin.formver.conversion
 import org.jetbrains.kotlin.fir.symbols.FirBasedSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol
-import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.expression.FirVariableEmbedding
 import org.jetbrains.kotlin.formver.embeddings.expression.VariableEmbedding
 import org.jetbrains.kotlin.formver.names.embedScopedLocalName

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

@@ -6,7 +6,7 @@
 package org.jetbrains.kotlin.formver.conversion
 
 import org.jetbrains.kotlin.formver.embeddings.FieldEmbedding
-import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.names.SpecialName
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.Type

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

@@ -8,6 +8,7 @@ package org.jetbrains.kotlin.formver.conversion
 import org.jetbrains.kotlin.formver.embeddings.*
 import org.jetbrains.kotlin.formver.embeddings.callables.NamedFunctionSignature
 import org.jetbrains.kotlin.formver.embeddings.expression.*
+import org.jetbrains.kotlin.formver.embeddings.types.isInheritorOfCollectionTypeNamed
 import org.jetbrains.kotlin.formver.names.NameMatcher
 
 private fun VariableEmbedding.sameSize(): ExpEmbedding =
@@ -23,7 +24,7 @@ sealed interface StdLibReceiverInterface {
 sealed interface PresentInterface : StdLibReceiverInterface {
     val interfaceName: String
     override fun match(function: NamedFunctionSignature): Boolean =
-        function.type.dispatchReceiverType?.isInheritorOfCollectionTypeNamed(interfaceName) ?: false
+        function.callableType.dispatchReceiverType?.pretype?.isInheritorOfCollectionTypeNamed(interfaceName) ?: false
 }
 
 data object CollectionInterface : PresentInterface {

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

@@ -17,6 +17,7 @@ import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirValueParameterSymbol
 import org.jetbrains.kotlin.fir.symbols.impl.FirVariableSymbol
 import org.jetbrains.kotlin.formver.embeddings.*
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.callables.FunctionSignature
 import org.jetbrains.kotlin.formver.embeddings.expression.*
 import org.jetbrains.kotlin.formver.isCustom
@@ -175,8 +176,8 @@ fun StmtConversionContext.insertInlineFunctionCall(
     parentCtx: MethodConversionContext? = null,
 ): ExpEmbedding {
     // TODO: It seems like it may be possible to avoid creating a local here, but it is not clear how.
-    val returnTarget = returnTargetProducer.getFresh(calleeSignature.type.returnType)
-    val (declarations, callArgs) = getInlineFunctionCallArgs(args, calleeSignature.type.formalArgTypes)
+    val returnTarget = returnTargetProducer.getFresh(calleeSignature.callableType.returnType)
+    val (declarations, callArgs) = getInlineFunctionCallArgs(args, calleeSignature.callableType.formalArgTypes)
     val subs = paramNames.zip(callArgs).toMap()
     val methodCtxFactory = MethodContextFactory(
         calleeSignature,

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

@@ -20,11 +20,11 @@ import org.jetbrains.kotlin.fir.types.isUnit
 import org.jetbrains.kotlin.fir.types.resolvedType
 import org.jetbrains.kotlin.fir.visitors.FirVisitor
 import org.jetbrains.kotlin.formver.UnsupportedFeatureBehaviour
-import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
-import org.jetbrains.kotlin.formver.embeddings.buildType
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.callables.FullNamedFunctionSignature
 import org.jetbrains.kotlin.formver.embeddings.callables.insertCall
 import org.jetbrains.kotlin.formver.embeddings.expression.*
+import org.jetbrains.kotlin.formver.embeddings.types.buildType
 import org.jetbrains.kotlin.formver.functionCallArguments
 import org.jetbrains.kotlin.text
 import org.jetbrains.kotlin.types.ConstantValueKind
@@ -88,7 +88,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
 
     override fun visitIntegerLiteralOperatorCall(
         integerLiteralOperatorCall: FirIntegerLiteralOperatorCall,
-        data: StmtConversionContext
+        data: StmtConversionContext,
     ): ExpEmbedding {
         return visitFunctionCall(integerLiteralOperatorCall, data)
     }
@@ -287,7 +287,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
 
     override fun visitBooleanOperatorExpression(
         booleanOperatorExpression: FirBooleanOperatorExpression,
-        data: StmtConversionContext
+        data: StmtConversionContext,
     ): ExpEmbedding {
         val left = data.convert(booleanOperatorExpression.leftOperand)
         val right = data.convert(booleanOperatorExpression.rightOperand)
@@ -327,7 +327,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
                 proven = true
                 access = true
             }
-            FirOperation.SAFE_AS -> SafeCast(argument, conversionType).withInvariants{
+            FirOperation.SAFE_AS -> SafeCast(argument, conversionType).withInvariants {
                 proven = true
                 access = true
             }

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

@@ -5,7 +5,7 @@
 
 package org.jetbrains.kotlin.formver.domains
 
-import org.jetbrains.kotlin.formver.embeddings.ClassTypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.ClassTypeEmbedding
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.*
 import org.jetbrains.kotlin.formver.viper.mangled

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

@@ -7,6 +7,7 @@ package org.jetbrains.kotlin.formver.embeddings
 
 import org.jetbrains.kotlin.formver.conversion.StmtConversionContext
 import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.embeddings.expression.withNewTypeInvariants
 
 // We assume that thanks to the checks done by the Kotlin compiler, a property with a

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

@@ -14,13 +14,13 @@ class CustomGetter(val getterMethod: CallableEmbedding) : GetterEmbedding {
     override fun getValue(
         receiver: ExpEmbedding,
         ctx: StmtConversionContext,
-    ): ExpEmbedding = getterMethod.insertCall(listOf(receiver), ctx, getterMethod.type.returnType)
+    ): ExpEmbedding = getterMethod.insertCall(listOf(receiver), ctx, getterMethod.callableType.returnType)
 }
 
 class CustomSetter(val setterMethod: CallableEmbedding) : SetterEmbedding {
     override fun setValue(
         receiver: ExpEmbedding,
         value: ExpEmbedding,
         ctx: StmtConversionContext,
-    ): ExpEmbedding = setterMethod.insertCall(listOf(receiver, value), ctx, setterMethod.type.returnType)
+    ): ExpEmbedding = setterMethod.insertCall(listOf(receiver, value), ctx, setterMethod.callableType.returnType)
 }

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

@@ -11,6 +11,12 @@ import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
 import org.jetbrains.kotlin.formver.embeddings.expression.FieldAccess
 import org.jetbrains.kotlin.formver.embeddings.expression.GeCmp
 import org.jetbrains.kotlin.formver.embeddings.expression.IntLit
+import org.jetbrains.kotlin.formver.embeddings.types.ClassTypeEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.FieldAccessTypeInvariantEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.TypeInvariantEmbedding
+import org.jetbrains.kotlin.formver.embeddings.types.buildType
+import org.jetbrains.kotlin.formver.embeddings.types.isCollectionInheritor
+import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.names.NameMatcher
 import org.jetbrains.kotlin.formver.names.ScopedKotlinName
 import org.jetbrains.kotlin.formver.names.SpecialName