Skip to content

Commit

Permalink
Add a builder for TypeEmbeddings (#229)
Browse files Browse the repository at this point in the history
Previously, we used the type embeddings directly in the code. This makes
changing their representation quite hard; this PR introduces a builder
that lets us hide the implementation details.

This isn't quite perfect; we sometimes still check what subtype a
particular embedding is. Getting rid of that entirely would be an even
bigger change, though.
  • Loading branch information
jesyspa authored Jul 26, 2024
1 parent d363387 commit e2cc67c
Show file tree
Hide file tree
Showing 17 changed files with 229 additions and 69 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,11 @@ 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) { ClassTypeEmbedding(className) }
val embedding = classes.getOrPut(className) {
buildType {
klass { withName(className) }
} as ClassTypeEmbedding
}
if (embedding.hasDetails) return embedding

val newDetails = ClassEmbeddingDetails(embedding, symbol.classKind == ClassKind.INTERFACE)
Expand Down Expand Up @@ -150,11 +154,11 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi

override fun embedType(type: ConeKotlinType): TypeEmbedding = when {
type is ConeErrorType -> error("Encountered an erroneous type: $type")
type is ConeTypeParameterType -> NullableTypeEmbedding(AnyTypeEmbedding)
type.isUnit -> UnitTypeEmbedding
type.isInt -> IntTypeEmbedding
type.isBoolean -> BooleanTypeEmbedding
type.isNothing -> NothingTypeEmbedding
type is ConeTypeParameterType -> buildType { isNullable = true; any() }
type.isUnit -> buildType { unit() }
type.isInt -> buildType { int() }
type.isBoolean -> buildType { boolean() }
type.isNothing -> buildType { nothing() }
type.isSomeFunctionType(session) -> {
val receiverType: TypeEmbedding? = type.receiverType(session)?.let { embedType(it) }
val paramTypes: List<TypeEmbedding> = type.valueParameterTypesWithoutReceivers(session).map(::embedType)
Expand All @@ -163,7 +167,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
FunctionTypeEmbedding(signature)
}
type.isNullable -> NullableTypeEmbedding(embedType(type.withNullability(ConeNullability.NOT_NULL, session.typeContext)))
type.isAny -> AnyTypeEmbedding
type.isAny -> buildType { any() }
type is ConeClassLikeType -> {
val classLikeSymbol = type.toClassSymbol(session)
if (classLikeSymbol is FirRegularClassSymbol) {
Expand Down Expand Up @@ -399,7 +403,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
throw NotImplementedError("The embedding for type $type is not yet implemented.")
UnsupportedFeatureBehaviour.ASSUME_UNREACHABLE -> {
errorCollector.addMinorError("Requested type $type, for which we do not yet have an embedding.")
UnitTypeEmbedding
buildType { unit() }
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,8 @@ import org.jetbrains.kotlin.fir.types.coneType
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.BooleanTypeEmbedding
import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
import org.jetbrains.kotlin.formver.embeddings.buildType
import org.jetbrains.kotlin.formver.embeddings.callables.FullNamedFunctionSignature
import org.jetbrains.kotlin.formver.embeddings.callables.insertCall
import org.jetbrains.kotlin.formver.embeddings.expression.*
Expand Down Expand Up @@ -99,7 +99,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
return if (branch.condition is FirElseIfTrueCondition) {
data.withNewScope { convert(branch.result) }
} else {
val cond = data.convert(branch.condition).withType(BooleanTypeEmbedding)
val cond = data.convert(branch.condition).withType { boolean() }
val thenExp = data.withNewScope { convert(branch.result) }
val elseExp = convertWhenBranches(whenBranches, type, data)
If(cond, thenExp, elseExp, type)
Expand Down Expand Up @@ -211,7 +211,7 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
}

override fun visitWhileLoop(whileLoop: FirWhileLoop, data: StmtConversionContext): ExpEmbedding {
val condition = data.convert(whileLoop.condition).withType(BooleanTypeEmbedding)
val condition = data.convert(whileLoop.condition).withType { boolean() }
val returnTarget = data.defaultResolvedReturnTarget
val invariants = when (val sig = data.signature) {
is FullNamedFunctionSignature -> sig.getPostconditions(returnTarget.variable)
Expand Down Expand Up @@ -274,8 +274,8 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
val left = data.convert(binaryLogicExpression.leftOperand)
val right = data.convert(binaryLogicExpression.rightOperand)
return when (binaryLogicExpression.kind) {
LogicOperationKind.AND -> If(left, right, BooleanLit(false), BooleanTypeEmbedding)
LogicOperationKind.OR -> If(left, BooleanLit(true), right, BooleanTypeEmbedding)
LogicOperationKind.AND -> If(left, right, BooleanLit(false), buildType { boolean() })
LogicOperationKind.OR -> If(left, BooleanLit(true), right, buildType { boolean() })
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,17 @@ package org.jetbrains.kotlin.formver.embeddings

import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol
import org.jetbrains.kotlin.formver.conversion.AccessPolicy
import org.jetbrains.kotlin.formver.embeddings.expression.*
import org.jetbrains.kotlin.formver.names.*
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.names.NameMatcher
import org.jetbrains.kotlin.formver.names.ScopedKotlinName
import org.jetbrains.kotlin.formver.names.SpecialName
import org.jetbrains.kotlin.formver.viper.MangledName
import org.jetbrains.kotlin.formver.viper.ast.*
import org.jetbrains.kotlin.formver.viper.ast.Field
import org.jetbrains.kotlin.formver.viper.ast.PermExp
import org.jetbrains.kotlin.formver.viper.ast.Type
import org.jetbrains.kotlin.utils.addToStdlib.ifTrue

/**
Expand Down Expand Up @@ -67,7 +74,7 @@ class UserFieldEmbedding(

object ListSizeFieldEmbedding : FieldEmbedding {
override val name = SpecialName("size")
override val type = IntTypeEmbedding
override val type = buildType { int() }
override val viperType = Type.Ref
override val accessPolicy = AccessPolicy.ALWAYS_WRITEABLE
override val includeInShortDump: Boolean = true
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
/*
* 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.embeddings

import org.jetbrains.kotlin.formver.embeddings.callables.CallableSignatureData
import org.jetbrains.kotlin.formver.names.ScopedKotlinName

/**
* We use "pretype" to refer to types that do not contain information on nullability or
* other flags.
*/
interface PretypeBuilder {
/**
* Turn the builder into a `TypeEmbedding`.
*
* We allow this deferral so that the build can be done in any order.
*/
fun complete(): TypeEmbedding
}

object UnitPretypeBuilder : PretypeBuilder {
override fun complete(): TypeEmbedding = UnitTypeEmbedding
}

object NothingPretypeBuilder : PretypeBuilder {
override fun complete(): TypeEmbedding = NothingTypeEmbedding
}

object AnyPretypeBuilder : PretypeBuilder {
override fun complete(): TypeEmbedding = AnyTypeEmbedding
}

object IntPretypeBuilder : PretypeBuilder {
override fun complete(): TypeEmbedding = IntTypeEmbedding
}

object BooleanPretypeBuilder : PretypeBuilder {
override fun complete(): TypeEmbedding = BooleanTypeEmbedding
}

class FunctionPretypeBuilder : PretypeBuilder {
private val paramTypes = mutableListOf<TypeEmbedding>()
private var receiverType: TypeEmbedding? = null
private var returnType: TypeEmbedding? = null

fun withParam(paramInit: TypeBuilder.() -> PretypeBuilder) {
paramTypes.add(buildType { paramInit() })
}

fun withReceiver(receiverInit: TypeBuilder.() -> PretypeBuilder) {
require(receiverType == null) { "Receiver already set" }
receiverType = buildType { receiverInit() }
}

fun withReturnType(returnTypeInit: TypeBuilder.() -> PretypeBuilder) {
require(returnType == null) { "Return type already set" }
returnType = buildType { returnTypeInit() }
}

override fun complete(): TypeEmbedding {
require(returnType != null) { "Return type not set" }
return FunctionTypeEmbedding(CallableSignatureData(receiverType, paramTypes, returnType!!))
}
}

class ClassPretypeBuilder : PretypeBuilder {
private var className: ScopedKotlinName? = null

fun withName(name: ScopedKotlinName) {
require(className == null) { "Class name already set" }
className = name
}

override fun complete(): TypeEmbedding {
require(className != null) { "Class name not set" }
return ClassTypeEmbedding(className!!)
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
/*
* 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.embeddings

/**
* Builder for a `TypeEmbedding`.
*
* We split most of the work into `PretypeBuilder`, which builds the type modulo nullability
* (and potentially other flags). As a result, the builder does not contain the full building
* state at any point, though a `TypeBuilder`, `PretypeBuilder` pair does.
*/
class TypeBuilder {
var isNullable = false

fun complete(init: TypeBuilder.() -> PretypeBuilder): TypeEmbedding = completeWithPretypeBuilder(init())

private fun completeWithPretypeBuilder(subBuilder: PretypeBuilder): TypeEmbedding {
val subResult = subBuilder.complete()
return if (isNullable) NullableTypeEmbedding(subResult) else subResult
}

fun unit() = UnitPretypeBuilder
fun nothing() = NothingPretypeBuilder
fun any() = AnyPretypeBuilder
fun int() = IntPretypeBuilder
fun boolean() = BooleanPretypeBuilder
fun function(init: FunctionPretypeBuilder.() -> Unit) = FunctionPretypeBuilder().also { it.init() }
fun klass(init: ClassPretypeBuilder.() -> Unit) = ClassPretypeBuilder().also { it.init() }
}

fun TypeBuilder.nullableAny(): AnyPretypeBuilder {
isNullable = true
return any()
}

fun buildType(init: TypeBuilder.() -> PretypeBuilder): TypeEmbedding = TypeBuilder().complete(init)

Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,6 @@ data object AnyTypeEmbedding : TypeEmbedding {
override val name = TypeName("Any")
}

data object NullableAnyTypeEmbedding : TypeEmbedding by NullableTypeEmbedding(AnyTypeEmbedding)

data object IntTypeEmbedding : TypeEmbedding {
override val runtimeType = RuntimeTypeDomain.intType()
override val name = TypeName("Int")
Expand All @@ -90,7 +88,6 @@ data object BooleanTypeEmbedding : TypeEmbedding {
override val name = TypeName("Boolean")
}


data class NullableTypeEmbedding(val elementType: TypeEmbedding) : TypeEmbedding {
override val runtimeType = RuntimeTypeDomain.nullable(elementType.runtimeType)
override val name = object : MangledName {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,13 @@ package org.jetbrains.kotlin.formver.embeddings.callables
import org.jetbrains.kotlin.KtSourceElement
import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol
import org.jetbrains.kotlin.formver.asPosition
import org.jetbrains.kotlin.formver.embeddings.NullableAnyTypeEmbedding
import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
import org.jetbrains.kotlin.formver.embeddings.UnitTypeEmbedding
import org.jetbrains.kotlin.formver.embeddings.expression.*
import org.jetbrains.kotlin.formver.embeddings.buildType
import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding
import org.jetbrains.kotlin.formver.embeddings.expression.FirVariableEmbedding
import org.jetbrains.kotlin.formver.embeddings.expression.PlaceholderVariableEmbedding
import org.jetbrains.kotlin.formver.embeddings.expression.VariableEmbedding
import org.jetbrains.kotlin.formver.embeddings.nullableAny
import org.jetbrains.kotlin.formver.linearization.pureToViper
import org.jetbrains.kotlin.formver.names.SetterValueName
import org.jetbrains.kotlin.formver.names.ThisReceiverName
Expand Down Expand Up @@ -47,23 +50,23 @@ abstract class PropertyAccessorFunctionSignature(
override fun getPreconditions(returnVariable: VariableEmbedding) = emptyList<ExpEmbedding>()
override fun getPostconditions(returnVariable: VariableEmbedding) = emptyList<ExpEmbedding>()
override val receiver: VariableEmbedding
get() = PlaceholderVariableEmbedding(ThisReceiverName, NullableAnyTypeEmbedding)
get() = PlaceholderVariableEmbedding(ThisReceiverName, buildType { nullableAny() })
override val declarationSource: KtSourceElement? = symbol.source
}

class GetterFunctionSignature(name: MangledName, symbol: FirPropertySymbol) :
PropertyAccessorFunctionSignature(name, symbol) {

override val params = emptyList<FirVariableEmbedding>()
override val returnType: TypeEmbedding = NullableAnyTypeEmbedding
override val returnType: TypeEmbedding = buildType { nullableAny() }
}

class SetterFunctionSignature(name: MangledName, symbol: FirPropertySymbol) :
PropertyAccessorFunctionSignature(name, symbol) {
override val params = listOf(
FirVariableEmbedding(SetterValueName, NullableAnyTypeEmbedding, symbol)
FirVariableEmbedding(SetterValueName, buildType { nullableAny() }, symbol)
)
override val returnType: TypeEmbedding = UnitTypeEmbedding
override val returnType: TypeEmbedding = buildType { unit() }
}


Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,14 @@
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.FunctionTypeEmbedding
import org.jetbrains.kotlin.formver.embeddings.TypeEmbedding
import org.jetbrains.kotlin.formver.embeddings.buildType
import org.jetbrains.kotlin.formver.embeddings.expression.*
import org.jetbrains.kotlin.formver.names.*
import org.jetbrains.kotlin.formver.names.ClassKotlinName
import org.jetbrains.kotlin.formver.names.ScopedKotlinName
import org.jetbrains.kotlin.formver.names.buildName
import org.jetbrains.kotlin.formver.names.embedFunctionName
import org.jetbrains.kotlin.formver.viper.ast.Method
import org.jetbrains.kotlin.name.CallableId
import org.jetbrains.kotlin.name.FqName
Expand Down Expand Up @@ -42,11 +47,19 @@ object KotlinContractFunction : SpecialKotlinFunction {
packageScope(packageName)
ClassKotlinName(listOf("ContractBuilder"))
}
private val contractBuilderType = ClassTypeEmbedding(contractBuilderTypeName)
override val receiverType: TypeEmbedding? = null
override val paramTypes: List<TypeEmbedding> =
listOf(FunctionTypeEmbedding(CallableSignatureData(contractBuilderType, listOf(), UnitTypeEmbedding)))
override val returnType: TypeEmbedding = UnitTypeEmbedding
listOf(buildType {
function {
withReceiver {
klass {
withName(contractBuilderTypeName)
}
}
withReturnType { unit() }
}
})
override val returnType: TypeEmbedding = buildType { unit() }

override fun insertCallImpl(
args: List<ExpEmbedding>,
Expand All @@ -58,9 +71,9 @@ abstract class KotlinIntSpecialFunction : SpecialKotlinFunction {
override val packageName: List<String> = listOf("kotlin")
override val className: String? = "Int"

override val receiverType: TypeEmbedding = IntTypeEmbedding
override val paramTypes: List<TypeEmbedding> = listOf(IntTypeEmbedding)
override val returnType: TypeEmbedding = IntTypeEmbedding
override val receiverType: TypeEmbedding = buildType { int() }
override val paramTypes: List<TypeEmbedding> = listOf(buildType { int() })
override val returnType: TypeEmbedding = buildType { int() }
}

object KotlinIntPlusFunctionImplementation : KotlinIntSpecialFunction() {
Expand Down Expand Up @@ -103,9 +116,9 @@ abstract class KotlinBooleanSpecialFunction : SpecialKotlinFunction {
override val packageName: List<String> = listOf("kotlin")
override val className: String? = "Boolean"

override val receiverType: TypeEmbedding = BooleanTypeEmbedding
override val receiverType: TypeEmbedding = buildType { boolean() }
override val paramTypes: List<TypeEmbedding> = emptyList()
override val returnType: TypeEmbedding = BooleanTypeEmbedding
override val returnType: TypeEmbedding = buildType { boolean() }
}

object KotlinBooleanNotFunctionImplementation : KotlinBooleanSpecialFunction() {
Expand All @@ -129,8 +142,8 @@ object SpecialVerifyFunction : SpecialKotlinFunction {
}

override val receiverType: TypeEmbedding? = null
override val paramTypes: List<TypeEmbedding> = listOf(BooleanTypeEmbedding)
override val returnType: TypeEmbedding = UnitTypeEmbedding
override val paramTypes: List<TypeEmbedding> = listOf(buildType { boolean() })
override val returnType: TypeEmbedding = buildType { unit() }
}

object SpecialKotlinFunctions {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,12 @@

package org.jetbrains.kotlin.formver.embeddings.expression

import org.jetbrains.kotlin.formver.asPosition
import org.jetbrains.kotlin.formver.domains.InjectionImageFunction
import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain
import org.jetbrains.kotlin.formver.embeddings.IntTypeEmbedding
import org.jetbrains.kotlin.formver.linearization.LinearizationContext
import org.jetbrains.kotlin.formver.embeddings.buildType

sealed interface IntArithmeticExpression : OperationBaseExpEmbedding {
override val type
get() = IntTypeEmbedding
get() = buildType { int() }
}

data class Add(
Expand Down
Loading

0 comments on commit e2cc67c

Please sign in to comment.