diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt index 4589f7a0998462..cb9dd344eec09a 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt @@ -38,6 +38,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi ProgramConversionContext { private val methods: MutableMap = SpecialKotlinFunctions.byName.toMutableMap() private val classes: MutableMap = mutableMapOf() + private val classDetails: MutableMap = mutableMapOf() private val properties: MutableMap = mutableMapOf() private val fields: MutableMap = mutableMapOf() @@ -67,7 +68,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi fields.values.distinctBy { it.name.mangled }.map { it.toViper() }, functions = SpecialFunctions.all, methods = SpecialMethods.all + methods.values.mapNotNull { it.viperMethod }.distinctBy { it.name.mangled }, - predicates = classes.values.flatMap { listOf(it.sharedPredicate, it.uniquePredicate) } + predicates = classDetails.values.flatMap { listOf(it.sharedPredicate, it.uniquePredicate) } ) fun registerForVerification(declaration: FirSimpleFunction) { @@ -113,38 +114,46 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi UserFunctionEmbedding(callable) } + /** + * Returns an embedding of the class type, with details set. + */ private fun embedClass(symbol: FirRegularClassSymbol): ClassTypeEmbedding { val className = symbol.classId.embedName() - return when (val existingEmbedding = classes[className]) { - null -> { - // The full class embedding is necessary to process the signatures of the properties of the class, since - // these take the class as a parameter. We thus do this in three phases: - // 1. Provide a class embedding in the `classes` map (necessary for embedType to not call this recursively). - // 2. Initialise the supertypes (including running this whole four-step process on each) - // 3. Initialise the fields - // 4. Process the properties of the class. - // - // With respect to the embedding, each phase is pure by itself, and only updates the class embedding at the end. - // This ensures the code never sees half-built supertype or field data. The phases can, however, modify the - // `ProgramConverter`. - - // Phase 1 - val newEmbedding = ClassTypeEmbedding(className, symbol.classKind == ClassKind.INTERFACE) - classes[className] = newEmbedding - - // Phase 2 - newEmbedding.initSuperTypes(symbol.resolvedSuperTypes.map(::embedType)) - - // Phase 3 - val properties = symbol.propertySymbols - newEmbedding.initFields(properties.mapNotNull { processBackingField(it, symbol) }.toMap()) - - // Phase 4 - properties.forEach { processProperty(it, newEmbedding) } - newEmbedding - } - else -> existingEmbedding + val embedding = classes.getOrPut(className) { + ClassTypeEmbedding(className, symbol.classKind == ClassKind.INTERFACE) } + if (embedding.hasDetails) return embedding + + classDetails[embedding]?.let { + embedding.initDetails(it) + return embedding + } + + val newDetails = ClassEmbeddingDetails(embedding) + classDetails[embedding] = newDetails + embedding.initDetails(newDetails) + + // The full class embedding is necessary to process the signatures of the properties of the class, since + // these take the class as a parameter. We thus do this in three phases: + // 1. Initialise the supertypes (including running this whole four-step process on each) + // 2. Initialise the fields + // 3. Process the properties of the class. + // + // With respect to the embedding, each phase is pure by itself, and only updates the class embedding at the end. + // This ensures the code never sees half-built supertype or field data. The phases can, however, modify the + // `ProgramConverter`. + + // Phase 1 + newDetails.initSuperTypes(symbol.resolvedSuperTypes.map(::embedType)) + + // Phase 2 + val properties = symbol.propertySymbols + newDetails.initFields(properties.mapNotNull { processBackingField(it, symbol) }.toMap()) + + // Phase 3 + properties.forEach { processProperty(it, newDetails) } + + return embedding } override fun embedType(type: ConeKotlinType): TypeEmbedding = when { @@ -203,7 +212,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi return constructedClassSymbol.propertySymbols.mapNotNull { propertySymbol -> propertySymbol.withConstructorParam { paramSymbol -> - constructedClass.findField(callableId.embedUnscopedPropertyName())?.let { paramSymbol to it } + constructedClass.details.findField(callableId.embedUnscopedPropertyName())?.let { paramSymbol to it } } }.toMap() } @@ -325,7 +334,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi * Note that the property either has associated Viper field (and then it is used to access the value) or not (in this case methods are used). * The field is only used for final properties with default getter and default setter (if any). */ - private fun processProperty(symbol: FirPropertySymbol, embedding: ClassTypeEmbedding) { + private fun processProperty(symbol: FirPropertySymbol, embedding: ClassEmbeddingDetails) { val unscopedName = symbol.callableId.embedUnscopedPropertyName() val backingField = embedding.findField(unscopedName) backingField?.let { fields.put(it.name, it) } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/domains/RuntimeTypeDomain.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/domains/RuntimeTypeDomain.kt index d2bb08a89cd6c8..3ab7906ee77917 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/domains/RuntimeTypeDomain.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/domains/RuntimeTypeDomain.kt @@ -410,7 +410,7 @@ class RuntimeTypeDomain(classes: List) : BuiltinDomain(RUNTI it.apply { injectionAxioms() } } classTypes.forEach { (typeEmbedding, typeFunction) -> - typeEmbedding.superTypes.forEach { + typeEmbedding.details.superTypes.forEach { classTypes[it]?.let { supertypeFunction -> axiom { typeFunction() subtype supertypeFunction() diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/ClassEmbeddingDetails.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/ClassEmbeddingDetails.kt new file mode 100644 index 00000000000000..901c9cb2fff371 --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/ClassEmbeddingDetails.kt @@ -0,0 +1,132 @@ +/* + * 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.names.ClassScope +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.PermExp +import org.jetbrains.kotlin.formver.viper.ast.Predicate +import org.jetbrains.kotlin.utils.addToStdlib.ifTrue + +class ClassEmbeddingDetails(val type: ClassTypeEmbedding) : TypeInvariantHolder { + private var _superTypes: List? = null + val superTypes: List + get() = _superTypes ?: error("Super types of ${type.className} have not been initialised yet.") + + private val classSuperTypes: List + get() = superTypes.filterIsInstance() + + fun initSuperTypes(newSuperTypes: List) { + check(_superTypes == null) { "Super types of ${type.className} are already initialised." } + _superTypes = newSuperTypes + } + + private var _fields: Map? = null + private var _sharedPredicate: Predicate? = null + private var _uniquePredicate: Predicate? = null + val fields: Map + get() = _fields ?: error("Fields of ${type.className} have not been initialised yet.") + val sharedPredicate: Predicate + get() = _sharedPredicate ?: error("Predicate of ${type.className} has not been initialised yet.") + val uniquePredicate: Predicate + get() = _uniquePredicate ?: error("Unique Predicate of ${type.className} has not been initialised yet.") + + fun initFields(newFields: Map) { + check(_fields == null) { "Fields of ${type.className} are already initialised." } + _fields = newFields + _sharedPredicate = ClassPredicateBuilder.build(this, type.name) { + forEachField { + if (isAlwaysReadable) { + addAccessPermissions(PermExp.WildcardPerm()) + forType { + addAccessToSharedPredicate() + includeSubTypeInvariants() + } + } + } + forEachSuperType { + addAccessToSharedPredicate() + } + } + _uniquePredicate = ClassPredicateBuilder.build(this, uniquePredicateName) { + forEachField { + if (isAlwaysReadable) { + addAccessPermissions(PermExp.WildcardPerm()) + } else { + addAccessPermissions(PermExp.FullPerm()) + } + forType { + addAccessToSharedPredicate() + if (isUnique) { + addAccessToUniquePredicate() + } + includeSubTypeInvariants() + } + } + forEachSuperType { + addAccessToUniquePredicate() + } + } + } + + private val uniquePredicateName = object : MangledName { + override val mangled: String = "Unique\$T_class_${type.className.mangled}" + } + + /** + * Find an embedding of a backing field by this name amongst the ancestors of this type. + * + * While in Kotlin only classes can have backing fields, and so searching interface supertypes is not strictly necessary, + * due to the way we handle list size we need to search all types. + */ + fun findField(name: SimpleKotlinName): FieldEmbedding? = fields[name] + + fun flatMapFields(action: (SimpleKotlinName, FieldEmbedding) -> List): List = + classSuperTypes.flatMap { it.details.flatMapFields(action) } + fields.flatMap { (name, field) -> action(name, field) } + + // We can't easily implement this by recursion on the supertype structure since some supertypes may be seen multiple times. + // TODO: figure out a nicer way to handle this. + override fun accessInvariants(): List = + flatMapUniqueFields { _, field -> field.accessInvariantsForParameter() } + + // Note: this function will replace accessInvariants when nested unfold will be implemented + override fun sharedPredicateAccessInvariant() = + PredicateAccessTypeInvariantEmbedding(type.name, PermExp.WildcardPerm()) + + override fun uniquePredicateAccessInvariant() = + 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 = sequence { + if (fieldName is ScopedKotlinName && fieldName.scope is ClassScope) { + if (fieldName.scope.className == type.className.name) { + yield(this@ClassEmbeddingDetails.type) + } else { + val sup = superTypes.firstOrNull { it is ClassTypeEmbedding && !it.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") + } + } + } else { + throw IllegalArgumentException("Cannot find hierarchy unfold path of a field with no class scope") + } + } + + fun flatMapUniqueFields(action: (SimpleKotlinName, FieldEmbedding) -> List): List { + val seenFields = mutableSetOf() + return flatMapFields { name, field -> + seenFields.add(name).ifTrue { + action(name, field) + } ?: listOf() + } + } + +} \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/ClassPredicateBuilder.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/ClassPredicateBuilder.kt index 8554ef4b595d15..cec0e8190fc93b 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/ClassPredicateBuilder.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/ClassPredicateBuilder.kt @@ -14,12 +14,15 @@ 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) +internal class ClassPredicateBuilder private constructor(private val details: ClassEmbeddingDetails) { + private val subject = PlaceholderVariableEmbedding(ClassPredicateSubjectName, details.type) private val body = mutableListOf() companion object { - fun build(classType: ClassTypeEmbedding, predicateName: MangledName, action: ClassPredicateBuilder.() -> Unit): Predicate { + fun build( + classType: ClassEmbeddingDetails, predicateName: MangledName, + action: ClassPredicateBuilder.() -> Unit, + ): Predicate { val builder = ClassPredicateBuilder(classType) builder.action() return Predicate( @@ -29,7 +32,7 @@ internal class ClassPredicateBuilder private constructor(private val type: Class } fun forEachField(action: FieldAssertionsBuilder.() -> Unit) = - type.fields.values + details.fields.values .filterIsInstance() .forEach { field -> val builder = FieldAssertionsBuilder(subject, field) @@ -38,7 +41,7 @@ internal class ClassPredicateBuilder private constructor(private val type: Class } fun forEachSuperType(action: TypeInvariantsBuilder.() -> Unit) = - type.superTypes.forEach { type -> + details.superTypes.forEach { type -> val builder = TypeInvariantsBuilder(type) builder.action() body.addAll(builder.toInvariantsList().fillHoles(subject)) diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt index 026185d31313d5..7a259140b67330 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt @@ -8,12 +8,12 @@ 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.* +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.names.SpecialName 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.utils.addToStdlib.ifTrue /** * Represents our representation of a Kotlin type. @@ -22,7 +22,7 @@ import org.jetbrains.kotlin.utils.addToStdlib.ifTrue * * All type embeddings must be `data` classes or objects! */ -interface TypeEmbedding { +interface TypeEmbedding : TypeInvariantHolder { /** * A Viper expression with the runtime representation of the type. * @@ -38,16 +38,6 @@ interface TypeEmbedding { */ val name: MangledName - /** - * Find an embedding of a backing field by this name amongst the ancestors of this type. - * - * While in Kotlin only classes can have backing fields, and so searching interface supertypes is not strictly necessary, - * due to the way we handle list size we need to search all types. - * - * Non-class types have no fields and so almost no types will implement this function. - */ - fun findField(name: SimpleKotlinName): FieldEmbedding? = null - /** * Perform an action on every field and collect the results. * @@ -56,21 +46,6 @@ interface TypeEmbedding { */ fun flatMapFields(action: (SimpleKotlinName, FieldEmbedding) -> List): List = listOf() - /** - * Invariants that provide access to a resource and thus behave linearly. - */ - fun accessInvariants(): List = emptyList() - - // Note: these functions will replace accessInvariants when nested unfold will be implemented - fun sharedPredicateAccessInvariant(): TypeInvariantEmbedding? = null - fun uniquePredicateAccessInvariant(): TypeInvariantEmbedding? = null - - /** - * Invariants that do not depend on the heap, and so do not need to be repeated - * once they have been established once. - */ - fun pureInvariants(): List = emptyList() - /** * Get a nullable version of this type embedding. * @@ -87,20 +62,6 @@ interface TypeEmbedding { get() = false } -fun TypeEmbedding.flatMapUniqueFields(action: (SimpleKotlinName, FieldEmbedding) -> List): List { - val seenFields = mutableSetOf() - return flatMapFields { name, field -> - seenFields.add(name).ifTrue { - action(name, field) - } ?: listOf() - } -} - -fun TypeEmbedding.mapNotNullUniqueFields(action: (SimpleKotlinName, FieldEmbedding) -> R?): List = - flatMapUniqueFields { name, field -> - action(name, field)?.let { listOf(it) } ?: emptyList() - } - data object UnitTypeEmbedding : TypeEmbedding { override val runtimeType = RuntimeTypeDomain.unitType() override val name = object : MangledName { @@ -133,7 +94,6 @@ data object IntTypeEmbedding : TypeEmbedding { } } - data object BooleanTypeEmbedding : TypeEmbedding { override val runtimeType = RuntimeTypeDomain.boolType() override val name = object : MangledName { @@ -185,113 +145,32 @@ data class FunctionTypeEmbedding(val signature: CallableSignatureData) : Unspeci } data class ClassTypeEmbedding(val className: ScopedKotlinName, val isInterface: Boolean) : TypeEmbedding { - private var _superTypes: List? = null - val superTypes: List - get() = _superTypes ?: error("Super types of $className have not been initialised yet.") - - private val classSuperTypes: List - get() = superTypes.filterIsInstance() + private var _details: ClassEmbeddingDetails? = null + val details: ClassEmbeddingDetails + get() = _details ?: error("Details of $className have not been initialised yet.") - fun initSuperTypes(newSuperTypes: List) { - check(_superTypes == null) { "Super types of $className are already initialised." } - _superTypes = newSuperTypes + fun initDetails(details: ClassEmbeddingDetails) { + require(_details == null) { "Class details already initialized" } + _details = details } - private var _fields: Map? = null - private var _sharedPredicate: Predicate? = null - private var _uniquePredicate: Predicate? = null - val fields: Map - get() = _fields ?: error("Fields of $className have not been initialised yet.") - val sharedPredicate: Predicate - get() = _sharedPredicate ?: error("Predicate of $className has not been initialised yet.") - val uniquePredicate: Predicate - get() = _uniquePredicate ?: error("Unique Predicate of $className has not been initialised yet.") - - fun initFields(newFields: Map) { - check(_fields == null) { "Fields of $className are already initialised." } - _fields = newFields - _sharedPredicate = ClassPredicateBuilder.build(this, name) { - forEachField { - if (isAlwaysReadable) { - addAccessPermissions(PermExp.WildcardPerm()) - forType { - addAccessToSharedPredicate() - includeSubTypeInvariants() - } - } - } - forEachSuperType { - addAccessToSharedPredicate() - } - } - _uniquePredicate = ClassPredicateBuilder.build(this, uniquePredicateName) { - forEachField { - if (isAlwaysReadable) { - addAccessPermissions(PermExp.WildcardPerm()) - } else { - addAccessPermissions(PermExp.FullPerm()) - } - forType { - addAccessToSharedPredicate() - if (isUnique) { - addAccessToUniquePredicate() - } - includeSubTypeInvariants() - } - } - forEachSuperType { - addAccessToUniquePredicate() - } - } - } + val hasDetails: Boolean + get() = _details != null // TODO: incorporate generic parameters. override val name = object : MangledName { override val mangled: String = "T_class_${className.mangled}" } - private val uniquePredicateName = object : MangledName { - override val mangled: String = "Unique\$T_class_${className.mangled}" - } - val runtimeTypeFunc = RuntimeTypeDomain.classTypeFunc(name) override val runtimeType: Exp = runtimeTypeFunc() - override fun findField(name: SimpleKotlinName): FieldEmbedding? = fields[name] - - override fun flatMapFields(action: (SimpleKotlinName, FieldEmbedding) -> List): List = - superTypes.flatMap { it.flatMapFields(action) } + fields.flatMap { (name, field) -> action(name, field) } - - // We can't easily implement this by recursion on the supertype structure since some supertypes may be seen multiple times. - // TODO: figure out a nicer way to handle this. - override fun accessInvariants(): List = - flatMapUniqueFields { _, field -> field.accessInvariantsForParameter() } + override fun accessInvariants(): List = details.accessInvariants() // Note: this function will replace accessInvariants when nested unfold will be implemented - override fun sharedPredicateAccessInvariant() = - PredicateAccessTypeInvariantEmbedding(name, PermExp.WildcardPerm()) - - override fun uniquePredicateAccessInvariant() = - 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 = sequence { - if (fieldName is ScopedKotlinName && fieldName.scope is ClassScope) { - if (fieldName.scope.className == className.name) { - yield(this@ClassTypeEmbedding) - } else { - val sup = superTypes.firstOrNull { it is ClassTypeEmbedding && !it.isInterface } - if (sup is ClassTypeEmbedding) { - yield(this@ClassTypeEmbedding) - yieldAll(sup.hierarchyUnfoldPath(fieldName)) - } else { - 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") - } - } + override fun sharedPredicateAccessInvariant() = details.sharedPredicateAccessInvariant() + + override fun uniquePredicateAccessInvariant() = details.uniquePredicateAccessInvariant() } @@ -313,7 +192,7 @@ private fun TypeEmbedding.isCollectionTypeNamed(name: String): Boolean = } fun TypeEmbedding.isInheritorOfCollectionTypeNamed(name: String): Boolean = - if (this !is ClassTypeEmbedding) false else isCollectionTypeNamed(name) || superTypes.any { + if (this !is ClassTypeEmbedding) false else isCollectionTypeNamed(name) || details.superTypes.any { it.isInheritorOfCollectionTypeNamed(name) } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeInvariantHolder.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeInvariantHolder.kt new file mode 100644 index 00000000000000..2bd42be68d3bd1 --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeInvariantHolder.kt @@ -0,0 +1,27 @@ +/* + * 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 + +/** + * Representation of an entity that, in Viper, should have invariants associated with it. + */ +interface TypeInvariantHolder { + /** + * Invariants that provide access to a resource and thus behave linearly. + */ + fun accessInvariants(): List = emptyList() + + // Note: these functions will replace accessInvariants when nested unfold will be implemented + fun sharedPredicateAccessInvariant(): TypeInvariantEmbedding? = null + fun uniquePredicateAccessInvariant(): TypeInvariantEmbedding? = null + + /** + * Invariants that do not depend on the heap, and so do not need to be repeated + * once they have been established once. + */ + fun pureInvariants(): List = emptyList() + +} \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ControlFlow.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ControlFlow.kt index 90fe0af19b5c11..069dfae63ddcda 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ControlFlow.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ControlFlow.kt @@ -15,7 +15,10 @@ import org.jetbrains.kotlin.formver.embeddings.expression.debug.* import org.jetbrains.kotlin.formver.linearization.LinearizationContext import org.jetbrains.kotlin.formver.linearization.addLabel import org.jetbrains.kotlin.formver.linearization.pureToViper -import org.jetbrains.kotlin.formver.viper.ast.* +import org.jetbrains.kotlin.formver.viper.ast.Exp +import org.jetbrains.kotlin.formver.viper.ast.Label +import org.jetbrains.kotlin.formver.viper.ast.PermExp +import org.jetbrains.kotlin.formver.viper.ast.Stmt // TODO: make a nice BlockBuilder interface. data class Block(val exps: List) : OptionalResultExpEmbedding { @@ -156,7 +159,7 @@ data class UnfoldingClassPredicateEmbedding(val predicated: VariableEmbedding, o } return Exp.Unfolding( Exp.PredicateAccess( - predicatedType.sharedPredicate.name, + predicatedType.details.sharedPredicate.name, listOf(predicated.pureToViper(false)), PermExp.WildcardPerm(), pos = ctx.source.asPosition, diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ExpEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ExpEmbedding.kt index 83e42c10bda804..a155ff3fb1ca32 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ExpEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ExpEmbedding.kt @@ -374,9 +374,9 @@ data class FieldAccess(val receiver: ExpEmbedding, val field: FieldEmbedding) : } private fun unfoldHierarchy(receiverWrapper: ExpEmbedding, ctx: LinearizationContext) { - val hierarchyPath = (receiver.type as? ClassTypeEmbedding)?.hierarchyUnfoldPath(field.name) + val hierarchyPath = (receiver.type as? ClassTypeEmbedding)?.details?.hierarchyUnfoldPath(field.name) hierarchyPath?.forEach { classType -> - val predAcc = classType.sharedPredicateAccessInvariant().fillHole(receiverWrapper) + val predAcc = classType.details.sharedPredicateAccessInvariant().fillHole(receiverWrapper) .pureToViper(toBuiltin = true, ctx.source) as? Exp.PredicateAccess predAcc?.let { ctx.addStatement { Stmt.Unfold(it) } } }