Added support for Kotlin objects

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

@@ -8,18 +8,22 @@ package org.jetbrains.kotlin.formver.core.conversion
 import org.jetbrains.kotlin.KtSourceElement
 import org.jetbrains.kotlin.descriptors.Visibilities
 import org.jetbrains.kotlin.descriptors.isInterface
+import org.jetbrains.kotlin.descriptors.isObject
+import org.jetbrains.kotlin.fir.FirElement
 import org.jetbrains.kotlin.fir.FirSession
 import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction
 import org.jetbrains.kotlin.fir.declarations.processAllDeclarations
 import org.jetbrains.kotlin.fir.declarations.utils.correspondingValueParameterFromPrimaryConstructor
 import org.jetbrains.kotlin.fir.declarations.utils.hasBackingField
 import org.jetbrains.kotlin.fir.declarations.utils.isFinal
 import org.jetbrains.kotlin.fir.declarations.utils.visibility
+import org.jetbrains.kotlin.fir.expressions.FirResolvedQualifier
 import org.jetbrains.kotlin.fir.resolve.toClassSymbol
 import org.jetbrains.kotlin.fir.resolve.toRegularClassSymbol
 import org.jetbrains.kotlin.fir.symbols.SymbolInternals
 import org.jetbrains.kotlin.fir.symbols.impl.*
 import org.jetbrains.kotlin.fir.types.*
+import org.jetbrains.kotlin.fir.visitors.FirVisitorVoid
 import org.jetbrains.kotlin.formver.common.ErrorCollector
 import org.jetbrains.kotlin.formver.common.PluginConfiguration
 import org.jetbrains.kotlin.formver.common.UnsupportedFeatureBehaviour
@@ -235,6 +239,7 @@ class ProgramConverter(
             ClassEmbeddingDetails(
                 embedding,
                 symbol.classKind.isInterface,
+                symbol.classKind.isObject,
             )
         embedding.initDetails(newDetails)
 
@@ -409,16 +414,31 @@ class ProgramConverter(
             ).statementCtxt()
         }
 
+        // Holds all objects referenced by the function
+        val referencedObjects = collectReferencedObjects(body)
+
         return object : FullNamedFunctionSignature, NamedFunctionSignature by subSignature {
             override fun getPreconditions() = buildList {
                 subSignature.formalArgs.forEach {
                     addAll(it.pureInvariants())
                     addAll(it.accessInvariants())
                     addAll(it.provenInvariants())
+                    addIfNotNull(it.sharedPredicateAccessInvariant())
                     if (it.isUnique) {
                         addIfNotNull(it.type.uniquePredicateAccessInvariant()?.fillHole(it))
                     }
                 }
+                // If a function references a singleton object, it must hold read permissions to this object.
+                // As objects are not created using a constructor that emits this permission, we must request it
+                // in the pres.
+                for (objectSymbol in referencedObjects) {
+                    val classTypeEmbedding = this@ProgramConverter.embedClass(objectSymbol)
+                    val objectLit = ObjectLit(
+                        TypeEmbedding(classTypeEmbedding, TypeEmbeddingFlags(nullable = false)),
+                        classTypeEmbedding.embedObjectValueFunc(),
+                    )
+                    addIfNotNull(classTypeEmbedding.sharedPredicateAccessInvariant().fillHole(objectLit))
+                }
                 addAll(subSignature.stdLibPreconditions())
                 // We create a separate context to embed the preconditions here.
                 // Hence, some parts of FIR are translated later than the other and less explicitly.
@@ -469,6 +489,27 @@ class ProgramConverter(
         }
     }
 
+    /** Collects all distinct object class symbols referenced by traversing the FIR AST again.
+     *  TODO: Check if the second tree traversal can be avoided */
+    private fun collectReferencedObjects(element: FirElement?): List<FirRegularClassSymbol> {
+        if (element == null) return emptyList()
+        val objects = mutableSetOf<FirRegularClassSymbol>()
+        element.acceptChildren(object : FirVisitorVoid() {
+            override fun visitElement(element: FirElement) {
+                element.acceptChildren(this)
+            }
+
+            override fun visitResolvedQualifier(resolvedQualifier: FirResolvedQualifier) {
+                resolvedQualifier.acceptChildren(this)
+                val classSymbol = resolvedQualifier.symbol as? FirRegularClassSymbol ?: return
+                if (classSymbol.classKind.isObject) {
+                    objects.add(classSymbol)
+                }
+            }
+        })
+        return objects.toList()
+    }
+
     private val FirFunctionSymbol<*>.containingPropertyOrSelf
         get() = when (this) {
             is FirPropertyAccessorSymbol -> propertySymbol

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

@@ -7,6 +7,7 @@ package org.jetbrains.kotlin.formver.core.conversion
 
 import org.jetbrains.kotlin.KtSourceElement
 import org.jetbrains.kotlin.contracts.description.LogicOperationKind
+import org.jetbrains.kotlin.descriptors.isObject
 import org.jetbrains.kotlin.fir.FirElement
 import org.jetbrains.kotlin.fir.declarations.FirProperty
 import org.jetbrains.kotlin.fir.expressions.*
@@ -37,7 +38,10 @@ import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbedd
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.LtIntInt
 import org.jetbrains.kotlin.formver.core.embeddings.expression.OperatorExpEmbeddings.Not
 import org.jetbrains.kotlin.formver.core.embeddings.toLink
+import org.jetbrains.kotlin.formver.core.embeddings.types.ClassTypeEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbedding
+import org.jetbrains.kotlin.formver.core.embeddings.types.embedClassTypeFunc
+import org.jetbrains.kotlin.formver.core.embeddings.types.embedObjectValueFunc
 import org.jetbrains.kotlin.formver.core.embeddings.types.equalToType
 import org.jetbrains.kotlin.formver.core.functionCallArguments
 import org.jetbrains.kotlin.formver.core.isInvariantBuilderFunctionNamed
@@ -81,12 +85,19 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
     override fun visitResolvedQualifier(
         resolvedQualifier: FirResolvedQualifier, data: StmtConversionContext
     ): ExpEmbedding {
-        if (!resolvedQualifier.resolvedType.isUnit) {
-            throw SnaktInternalException(
-                resolvedQualifier.source, "Only `Unit` is supported among resolved qualifiers currently."
-            )
+        if (resolvedQualifier.resolvedType.isUnit) {
+            return UnitLit
         }
-        return UnitLit
+        val classSymbol = resolvedQualifier.symbol as? FirClassSymbol<*>
+        if (classSymbol != null && classSymbol.classKind.isObject) {
+            val type = data.embedType(resolvedQualifier.resolvedType)
+            // TODO: Is there a better way to do this? E.g. by not selecting the domain function here
+            val classTypeEmbedding = type.pretype as? ClassTypeEmbedding ?:
+                throw SnaktInternalException(resolvedQualifier.source, "Object type must be an class")
+            return ObjectLit(type, classTypeEmbedding.embedObjectValueFunc())
+        }
+
+        throw SnaktInternalException(resolvedQualifier.source, "Unsupported reference used as resolved quantifier.")
     }
 
     override fun visitBlock(block: FirBlock, data: StmtConversionContext): ExpEmbedding =

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

@@ -7,6 +7,7 @@ package org.jetbrains.kotlin.formver.core.domains
 
 import org.jetbrains.kotlin.formver.core.embeddings.types.ClassTypeEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.types.embedClassTypeFunc
+import org.jetbrains.kotlin.formver.core.embeddings.types.embedObjectValueFunc
 import org.jetbrains.kotlin.formver.viper.SymbolicName
 import org.jetbrains.kotlin.formver.viper.ast.*
 
@@ -268,6 +269,10 @@ class RuntimeTypeDomain(val classes: List<ClassTypeEmbedding>) : BuiltinDomain(R
         // for creation of user types
         fun classTypeFunc(name: SymbolicName) = createDomainFunc(name, emptyList(), RuntimeType, true)
 
+        // value functions for object, which are later axiomatized to be unique
+        fun objectValueFunc(name: SymbolicName) = createDomainFunc(name, emptyList(), Ref)
+
+
         // bijections to primitive types
         val intInjection = Injection("int", Type.Int, intType)
         val boolInjection = Injection("bool", Type.Bool, boolType)
@@ -281,6 +286,8 @@ class RuntimeTypeDomain(val classes: List<ClassTypeEmbedding>) : BuiltinDomain(R
     }
 
     val classTypes: Map<ClassTypeEmbedding, DomainFunc> = classes.associateWith { it.embedClassTypeFunc() }
+    private val objectClasses: List<ClassTypeEmbedding> = classes.filter { it.hasDetails && it.details.isObject }
+    val objectClassesWithValueFunc: Map<ClassTypeEmbedding, DomainFunc> = objectClasses.associateWith { it.embedObjectValueFunc() }
     val builtinTypes: List<DomainFunc> =
         listOf(intType, boolType, charType, unitType, nothingType, anyType, functionType, stringType)
     val nonNullableTypes: List<DomainFunc> = buildList {
@@ -289,7 +296,7 @@ class RuntimeTypeDomain(val classes: List<ClassTypeEmbedding>) : BuiltinDomain(R
     }.distinctBy { it.name }
     override val functions: List<DomainFunc> = nonNullableTypes + listOf(
         nullValue, unitValue, isSubtype, typeOf, nullable
-    ) + allInjections.flatMap { listOf(it.toRef, it.fromRef) }
+    ) + allInjections.flatMap { listOf(it.toRef, it.fromRef) } + objectClassesWithValueFunc.values
     override val axioms: List<DomainAxiom> = AxiomListBuilder.build(this) {
         axiom("subtype_reflexive") {
             Exp.forall(t) { t -> t subtype t }
@@ -411,5 +418,20 @@ class RuntimeTypeDomain(val classes: List<ClassTypeEmbedding>) : BuiltinDomain(R
                 }
             }
         }
+        // Create type and uniqueness axioms for object types
+        objectClassesWithValueFunc.forEach { (typeEmbedding, valueFunction) ->
+            val typeFunction = classTypes[typeEmbedding]!!
+            axiom {
+                valueFunction() isOf typeFunction()
+            }
+            axiom {
+                Exp.forall(r) { r ->
+                    assumption {
+                        simpleTrigger { r isOf typeFunction() }
+                    }
+                    r eq valueFunction()
+                }
+            }
+        }
     }
 }

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

@@ -115,13 +115,12 @@ fun FullNamedFunctionSignature.toViperFunction(
             "Postcondition tries to acquire permissions, which is not allowed in a function"
         )
     }
-    val preconditions = formalArgs.mapNotNull { it.sharedPredicateAccessInvariant() } + getPreconditions()
     return UserFunction(
         name,
         formalArgs.map { it.toLocalVarDecl() },
         // TODO: Be explicit about the return types of functions instead of boxing them into a Ref
         Type.Ref,
-        preconditions.pureToViper(toBuiltin = true),
+        getPreconditions().pureToViper(toBuiltin = true),
         postconditions.pureToViper(toBuiltin = true),
         body,
         declarationSource.asPosition

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

@@ -13,8 +13,10 @@ import org.jetbrains.kotlin.formver.core.embeddings.callables.NamedFunctionSigna
 import org.jetbrains.kotlin.formver.core.embeddings.callables.toFuncApp
 import org.jetbrains.kotlin.formver.core.embeddings.callables.toMethodCall
 import org.jetbrains.kotlin.formver.core.embeddings.expression.debug.*
+import org.jetbrains.kotlin.formver.core.embeddings.types.ClassTypeEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.types.buildType
+import org.jetbrains.kotlin.formver.core.embeddings.types.predicateAccess
 import org.jetbrains.kotlin.formver.core.linearization.LinearizationContext
 import org.jetbrains.kotlin.formver.core.linearization.addLabel
 import org.jetbrains.kotlin.formver.core.linearization.freshAnonVar
@@ -191,11 +193,31 @@ data class NonDeterministically(val exp: ExpEmbedding) : UnitResultExpEmbedding,
     override fun <R> accept(v: ExpVisitor<R>): R = v.visitNonDeterministically(this)
 }
 
+/** Unfolds every predicate in the subtyping hierarchy between the actual type and the expected supertype */
+private fun unfoldSubtypePredicatesForArgs(
+    args: List<ExpEmbedding>,
+    formalArgs: List<VariableEmbedding>,
+    ctx: LinearizationContext,
+) {
+    args.zip(formalArgs).forEach { (arg, param) ->
+        val innerPretype = arg.ignoringCastsAndMetaNodes().type.pretype
+        val paramPretype = param.type.pretype
+        if (innerPretype is ClassTypeEmbedding && paramPretype is ClassTypeEmbedding) {
+            val path = innerPretype.details.supertypePathTo(paramPretype) ?: return@forEach
+            for (step in path) { // unfold for each type in hierarchy
+                val predAcc = step.predicateAccess(arg, ctx.source)
+                ctx.addStatement { Stmt.Unfold(predAcc, ctx.source.asPosition) }
+            }
+        }
+    }
+}
+
 // Note: this is always a *real* Viper method call.
 data class MethodCall(val method: NamedFunctionSignature, val args: List<ExpEmbedding>) : StoredResultExpEmbedding {
     override val type: TypeEmbedding = method.callableType.returnType
 
     override fun toViperStoringIn(result: VariableEmbedding, ctx: LinearizationContext) {
+        unfoldSubtypePredicatesForArgs(args, method.formalArgs, ctx)
         ctx.addStatement {
             method.toMethodCall(
                 args.map { it.toViper(ctx) },
@@ -224,10 +246,13 @@ data class FunctionCall(val function: NamedFunctionSignature, val args: List<Exp
     override val subexpressions: List<ExpEmbedding>
         get() = args
 
-    override fun toViper(ctx: LinearizationContext): Exp = function.toFuncApp(
-        args.map { it.toViper(ctx) },
-        ctx.source.asPosition
-    )
+    override fun toViper(ctx: LinearizationContext): Exp {
+        unfoldSubtypePredicatesForArgs(args, function.formalArgs, ctx) // unfold before function call
+        return function.toFuncApp(
+            args.map { it.toViper(ctx) },
+            ctx.source.asPosition
+        )
+    }
 
     override fun <R> accept(v: ExpVisitor<R>): R =
         v.visitFunctionCall(this)
@@ -276,13 +301,6 @@ data class FunctionExp(
     override val type: TypeEmbedding = body.type
 
     override fun toViperMaybeStoringIn(result: VariableEmbedding?, ctx: LinearizationContext) {
-        signature?.formalArgs?.forEach { arg ->
-            // Ideally, we would want to assume these rather than inhale them to prevent inconsistencies with
-            // permissions. Unfortunately, Silicon for some reason does not allow Assumes.
-            listOfNotNull(arg.sharedPredicateAccessInvariant()).forEach { invariant ->
-                ctx.addStatement { Stmt.Inhale(invariant.toViperBuiltinType(ctx), ctx.source.asPosition) }
-            }
-        }
         body.toViperMaybeStoringIn(result, ctx)
         ctx.addLabel(returnLabel.toViper(ctx))
     }

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

@@ -12,12 +12,15 @@ import org.jetbrains.kotlin.formver.core.embeddings.SourceRole
 import org.jetbrains.kotlin.formver.core.embeddings.asInfo
 import org.jetbrains.kotlin.formver.core.embeddings.expression.debug.PlaintextLeaf
 import org.jetbrains.kotlin.formver.core.embeddings.expression.debug.TreeView
+import org.jetbrains.kotlin.formver.core.embeddings.types.TypeEmbedding
 import org.jetbrains.kotlin.formver.core.embeddings.types.buildType
 import org.jetbrains.kotlin.formver.core.embeddings.types.injection
 import org.jetbrains.kotlin.formver.core.linearization.LinearizationContext
 import org.jetbrains.kotlin.formver.viper.NameResolver
+import org.jetbrains.kotlin.formver.viper.ast.DomainFunc
 import org.jetbrains.kotlin.formver.viper.ast.Exp
 import org.jetbrains.kotlin.formver.viper.ast.viperLiteral
+import viper.silicon.state.terms.DomainFun
 
 interface LiteralEmbedding : NullaryDirectResultExpEmbedding {
     val value: Any?
@@ -93,3 +96,19 @@ data object NullLit : LiteralEmbedding {
     override val debugName = "Null"
 }
 
+/**
+ * Resembles a Kotlin object
+ *  Requires the object's type embedding and a domain function returning its unique reference
+ */
+data class ObjectLit(
+    override val type: TypeEmbedding,
+    val valueFunc: DomainFunc
+) : NullaryDirectResultExpEmbedding {
+    override val debugName = "ObjectLit"
+
+    override fun toViper(ctx: LinearizationContext): Exp =
+        valueFunc(pos = ctx.source.asPosition)
+
+    override fun <R> accept(v: ExpVisitor<R>): R =
+        v.visitDefault(this)
+}

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

@@ -17,6 +17,7 @@ import org.jetbrains.kotlin.utils.addToStdlib.ifTrue
 class ClassEmbeddingDetails(
     val type: ClassTypeEmbedding,
     val isInterface: Boolean,
+    val isObject: Boolean,
 ) : TypeInvariantHolder {
     private var _superTypes: List<PretypeEmbedding>? = null
     val superTypes: List<PretypeEmbedding>
@@ -110,6 +111,16 @@ class ClassEmbeddingDetails(
 
     override fun subTypeInvariant(): TypeInvariantEmbedding = type.subTypeInvariant()
 
+    /** Constructs a list resembling the full subtyping relations between the current class and some supertype */
+    fun supertypePathTo(target: ClassTypeEmbedding): List<ClassTypeEmbedding>? {
+        if (type == target) return emptyList()
+        for (sup in classSuperTypes) {
+            val subPath = sup.details.supertypePathTo(target)
+            if (subPath != null) return listOf(type) + subPath
+        }
+        return null
+    }
+
     // Returns the sequence of classes in a hierarchy that need to be unfolded in order to access the given field
     fun hierarchyPathTo(field: FieldEmbedding): Sequence<ClassTypeEmbedding> = sequence {
         val className = field.containingClass?.name

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

@@ -10,6 +10,7 @@ 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.ObjectValueName
 import org.jetbrains.kotlin.formver.core.names.ScopedKotlinName
 import org.jetbrains.kotlin.formver.viper.ast.DomainFunc
 import org.jetbrains.kotlin.formver.viper.ast.Exp
@@ -63,6 +64,10 @@ private fun PretypeEmbedding.isCollectionTypeNamed(name: String): Boolean {
 
 fun ClassTypeEmbedding.embedClassTypeFunc(): DomainFunc = RuntimeTypeDomain.classTypeFunc(name)
 
+fun ClassTypeEmbedding.embedObjectValueFunc(): DomainFunc = RuntimeTypeDomain.objectValueFunc(
+    ObjectValueName(name)
+)
+
 fun ClassTypeEmbedding.predicateAccess(
     receiver: ExpEmbedding,
     source: KtSourceElement?

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/linearization/Linearizer.kt

@@ -70,6 +70,17 @@ data class Linearizer(
         val lhsViper = lhs.toViper(this)
         val rhsViper = rhs.withType(lhs.type).toViper(this)
         addStatement { Stmt.assign(lhsViper, rhsViper, source.asPosition) }
+        // Unfold the subtype's shared predicate hierarchy so the supertype's shared predicate becomes available
+        val innerPretype = rhs.ignoringCastsAndMetaNodes().type.pretype
+        val lhsPretype = lhs.type.pretype
+        if (innerPretype is ClassTypeEmbedding && lhsPretype is ClassTypeEmbedding) { // Only for class-like objects
+            val path = innerPretype.details.supertypePathTo(lhsPretype) ?: return
+            val lhsWrapper = ExpWrapper(lhsViper, rhs.ignoringCastsAndMetaNodes().type)
+            for (step in path) {
+                val predAcc = step.predicateAccess(lhsWrapper, source)
+                addStatement { Stmt.Unfold(predAcc, source.asPosition) }
+            }
+        }
     }
 
     override fun addReturn(returnExp: ExpEmbedding, target: ReturnTarget) {

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

@@ -82,6 +82,14 @@ data class ConstructorKotlinName(val type: FunctionTypeEmbedding) : KotlinName {
         get() = type.name.mangledBaseName
 }
 
+data class ObjectValueName(val className: SymbolicName) : KotlinName {
+    context(nameResolver: NameResolver)
+    override val mangledBaseName: String
+        get() = "${className.mangledBaseName}${SEPARATOR}value"
+    override val mangledType: String
+        get() = className.mangledType ?: ""
+}
+
 // It's a bit of a hack to make this as KotlinName, it should really just be any old name, but right now our scoped
 // names are KotlinNames and changing that could be messy.
 data class PredicateKotlinName(val name: String) : KotlinName {