diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ContractDescriptionConversionVisitor.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ContractDescriptionConversionVisitor.kt index 7f323357b6b20..e501c56f322ad 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ContractDescriptionConversionVisitor.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ContractDescriptionConversionVisitor.kt @@ -16,6 +16,7 @@ import org.jetbrains.kotlin.formver.effects import org.jetbrains.kotlin.formver.embeddings.SourceRole import org.jetbrains.kotlin.formver.embeddings.callables.NamedFunctionSignature import org.jetbrains.kotlin.formver.embeddings.expression.* +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings data class ContractVisitorContext( val returnVariable: VariableEmbedding, @@ -92,8 +93,10 @@ class ContractDescriptionConversionVisitor( val lhsRole = left.sourceRole as SourceRole.Condition val rhsRole = right.sourceRole as SourceRole.Condition return when (binaryLogicExpression.kind) { - LogicOperationKind.AND -> And(left, right, SourceRole.Condition.Conjunction(lhsRole, rhsRole)) - LogicOperationKind.OR -> Or(left, right, SourceRole.Condition.Disjunction(lhsRole, rhsRole)) + LogicOperationKind.AND -> + OperatorExpEmbeddings.And(left, right, SourceRole.Condition.Conjunction(lhsRole, rhsRole)) + LogicOperationKind.OR -> + OperatorExpEmbeddings.Or(left, right, SourceRole.Condition.Disjunction(lhsRole, rhsRole)) } } @@ -102,7 +105,7 @@ class ContractDescriptionConversionVisitor( data: ContractVisitorContext, ): ExpEmbedding { val arg = logicalNot.arg.accept(this, data) - return Not(arg, SourceRole.Condition.Negation(arg.sourceRole as SourceRole.Condition)) + return OperatorExpEmbeddings.Not(arg, SourceRole.Condition.Negation(arg.sourceRole as SourceRole.Condition)) } override fun visitConditionalEffectDeclaration( @@ -113,7 +116,7 @@ class ContractDescriptionConversionVisitor( val cond = conditionalEffect.condition.accept(this, data) // The effect's source role it is guaranteed to be not null. The same goes for the condition's source role. val role = SourceRole.ConditionalEffect(effect.sourceRole as SourceRole.ReturnsEffect, cond.sourceRole as SourceRole.Condition) - return Implies(effect, cond, role) + return OperatorExpEmbeddings.Implies(effect, cond, role) } override fun visitCallsEffectDeclaration( @@ -131,7 +134,7 @@ class ContractDescriptionConversionVisitor( val argSymbol = isInstancePredicate.arg.getTargetParameter(data) val role = SourceRole.Condition.IsType(argSymbol, isInstancePredicate.type, isInstancePredicate.isNegated) return if (isInstancePredicate.isNegated) { - Not(Is(argVar, ctx.embedType(isInstancePredicate.type)), role) + OperatorExpEmbeddings.Not(Is(argVar, ctx.embedType(isInstancePredicate.type)), role) } else { Is(argVar, ctx.embedType(isInstancePredicate.type), role) } 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 e10470da6b1a2..372795e591b4e 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 @@ -8,6 +8,7 @@ package org.jetbrains.kotlin.formver.conversion import org.jetbrains.kotlin.KtSourceElement import org.jetbrains.kotlin.descriptors.ClassKind import org.jetbrains.kotlin.descriptors.Visibilities +import org.jetbrains.kotlin.descriptors.isInterface import org.jetbrains.kotlin.fir.FirSession import org.jetbrains.kotlin.fir.declarations.FirSimpleFunction import org.jetbrains.kotlin.fir.declarations.utils.* @@ -21,16 +22,7 @@ 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.embeddings.types.* import org.jetbrains.kotlin.formver.linearization.Linearizer import org.jetbrains.kotlin.formver.linearization.SeqnBuilder import org.jetbrains.kotlin.formver.linearization.SharedLinearizationState @@ -49,7 +41,10 @@ import org.jetbrains.kotlin.utils.addToStdlib.ifTrue */ class ProgramConverter(val session: FirSession, override val config: PluginConfiguration, override val errorCollector: ErrorCollector) : ProgramConversionContext { - private val methods: MutableMap = SpecialKotlinFunctions.byName.toMutableMap() + private val methods: MutableMap = + SpecialKotlinFunctions.byName.toMutableMap().also { + it.putAll(PartiallySpecialKotlinFunctions.byName) + } private val classes: MutableMap = mutableMapOf() private val properties: MutableMap = mutableMapOf() private val fields: MutableSet = mutableSetOf() @@ -119,12 +114,23 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi } } - override fun embedFunction(symbol: FirFunctionSymbol<*>): FunctionEmbedding = - methods.getOrPut(symbol.embedName(this)) { - val signature = embedFullSignature(symbol) - val callable = processCallable(symbol, signature) - UserFunctionEmbedding(callable) + override fun embedFunction(symbol: FirFunctionSymbol<*>): FunctionEmbedding { + return when (val existing = methods[symbol.embedName(this)]) { + null, is PartiallySpecialKotlinFunction -> { + if (existing is PartiallySpecialKotlinFunction && existing.baseEmbedding != null) + return existing + val signature = embedFullSignature(symbol) + val callable = processCallable(symbol, signature) + val userFunction = UserFunctionEmbedding(callable) + when { + existing is PartiallySpecialKotlinFunction -> + existing.also { it.initBaseEmbedding(userFunction) } + else -> userFunction.also { methods[symbol.embedName(this)] = it } + } + } + else -> existing } + } /** * Returns an embedding of the class type, with details set. @@ -138,7 +144,10 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi } if (embedding.hasDetails) return embedding - val newDetails = ClassEmbeddingDetails(embedding, symbol.classKind == ClassKind.INTERFACE) + val sharedPredicateEnhancer = embedding.isString.ifTrue { + StringSharedPredicateEnhancer + } + val newDetails = ClassEmbeddingDetails(embedding, symbol.classKind.isInterface, sharedPredicateEnhancer) embedding.initDetails(newDetails) // The full class embedding is necessary to process the signatures of the properties of the class, since @@ -289,7 +298,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi } } return if (invariants.isEmpty()) null - else UnfoldingClassPredicateEmbedding(returnVariable, invariants.toConjunction()) + else UnfoldingSharedClassPredicateEmbedding(returnVariable, invariants.toConjunction()) } override val declarationSource: KtSourceElement? = symbol.source @@ -409,6 +418,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi isNullable = true; any() } type.isUnit -> unit() + type.isChar -> char() type.isInt -> int() type.isBoolean -> boolean() type.isNothing -> nothing() diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StdLibConverter.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StdLibConverter.kt index 3808d5ebcf562..6713c730b4a58 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StdLibConverter.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StdLibConverter.kt @@ -8,6 +8,12 @@ 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.expression.OperatorExpEmbeddings.GeIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.GtIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.Implies +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.LeIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.Not +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.SubIntInt import org.jetbrains.kotlin.formver.embeddings.types.isInheritorOfCollectionTypeNamed import org.jetbrains.kotlin.formver.names.NameMatcher @@ -15,7 +21,10 @@ private fun VariableEmbedding.sameSize(): ExpEmbedding = EqCmp(FieldAccess(this, ListSizeFieldEmbedding), Old(FieldAccess(this, ListSizeFieldEmbedding))) private fun VariableEmbedding.increasedSize(amount: Int): ExpEmbedding = - EqCmp(FieldAccess(this, ListSizeFieldEmbedding), Add(Old(FieldAccess(this, ListSizeFieldEmbedding)), IntLit(amount))) + EqCmp( + FieldAccess(this, ListSizeFieldEmbedding), + OperatorExpEmbeddings.AddIntInt(Old(FieldAccess(this, ListSizeFieldEmbedding)), IntLit(amount)), + ) sealed interface StdLibReceiverInterface { fun match(function: NamedFunctionSignature): Boolean @@ -86,12 +95,12 @@ data object GetPrecondition : StdLibPrecondition { val receiver = function.dispatchReceiver!! val indexArg = function.formalArgs[1] return listOf( - GeCmp( + GeIntInt( indexArg, IntLit(0), SourceRole.ListElementAccessCheck(SourceRole.ListElementAccessCheck.AccessCheckType.LESS_THAN_ZERO) ), - GtCmp( + GtIntInt( FieldAccess(receiver, ListSizeFieldEmbedding), indexArg, SourceRole.ListElementAccessCheck(SourceRole.ListElementAccessCheck.AccessCheckType.GREATER_THAN_LIST_SIZE) @@ -109,9 +118,9 @@ data object SubListPrecondition : StdLibPrecondition { val fromIndexArg = function.formalArgs[1] val toIndexArg = function.formalArgs[2] return listOf( - LeCmp(fromIndexArg, toIndexArg, SourceRole.SubListCreation.CheckInSize), - GeCmp(fromIndexArg, IntLit(0), SourceRole.SubListCreation.CheckNegativeIndices), - LeCmp(toIndexArg, FieldAccess(receiver, ListSizeFieldEmbedding), SourceRole.SubListCreation.CheckInSize) + LeIntInt(fromIndexArg, toIndexArg, SourceRole.SubListCreation.CheckInSize), + GeIntInt(fromIndexArg, IntLit(0), SourceRole.SubListCreation.CheckNegativeIndices), + LeIntInt(toIndexArg, FieldAccess(receiver, ListSizeFieldEmbedding), SourceRole.SubListCreation.CheckInSize) ) } @@ -136,7 +145,7 @@ data object IsEmptyPostcondition : StdLibPostcondition { return listOf( receiver.sameSize(), Implies(returnVariable, EqCmp(FieldAccess(receiver, ListSizeFieldEmbedding), IntLit(0))), - Implies(Not(returnVariable), GtCmp(FieldAccess(receiver, ListSizeFieldEmbedding), IntLit(0))) + Implies(Not(returnVariable), GtIntInt(FieldAccess(receiver, ListSizeFieldEmbedding), IntLit(0))) ) } @@ -159,7 +168,7 @@ data object SubListPostcondition : StdLibPostcondition { val toIndexArg = function.formalArgs[2] return listOf( function.dispatchReceiver!!.sameSize(), - EqCmp(FieldAccess(returnVariable, ListSizeFieldEmbedding), Sub(toIndexArg, fromIndexArg)) + EqCmp(FieldAccess(returnVariable, ListSizeFieldEmbedding), SubIntInt(toIndexArg, fromIndexArg)) ) } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt index 0e2252c1df5a9..d844db7a1e12e 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/StmtConversionVisitor.kt @@ -24,10 +24,20 @@ import org.jetbrains.kotlin.formver.UnsupportedFeatureBehaviour import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding import org.jetbrains.kotlin.formver.embeddings.callables.FullNamedFunctionSignature import org.jetbrains.kotlin.formver.embeddings.callables.FunctionEmbedding -import org.jetbrains.kotlin.formver.embeddings.callables.SpecialVerifyFunction import org.jetbrains.kotlin.formver.embeddings.callables.insertCall +import org.jetbrains.kotlin.formver.embeddings.callables.isVerifyFunction import org.jetbrains.kotlin.formver.embeddings.expression.* +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.GeCharChar +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.GeIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.GtCharChar +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.GtIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.LeCharChar +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.LeIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.LtCharChar +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.LtIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.Not import org.jetbrains.kotlin.formver.embeddings.types.buildType +import org.jetbrains.kotlin.formver.embeddings.types.equalToType import org.jetbrains.kotlin.formver.functionCallArguments import org.jetbrains.kotlin.text import org.jetbrains.kotlin.types.ConstantValueKind @@ -85,6 +95,8 @@ object StmtConversionVisitor : FirVisitor() when (literalExpression.kind) { ConstantValueKind.Int -> IntLit((literalExpression.value as Long).toInt()) ConstantValueKind.Boolean -> BooleanLit(literalExpression.value as Boolean) + ConstantValueKind.Char -> CharLit(literalExpression.value as Char) + ConstantValueKind.String -> StringLit(literalExpression.value as String) ConstantValueKind.Null -> NullLit else -> handleUnimplementedElement("Constant Expression of type ${literalExpression.kind} is not yet implemented.", data) } @@ -180,12 +192,43 @@ object StmtConversionVisitor : FirVisitor() } val left = data.convert(dispatchReceiver) val right = data.convert(arg) - return when (comparisonExpression.operation) { - FirOperation.LT -> LtCmp(left, right) - FirOperation.LT_EQ -> LeCmp(left, right) - FirOperation.GT -> GtCmp(left, right) - FirOperation.GT_EQ -> GeCmp(left, right) - else -> throw IllegalArgumentException("expected comparison operation but found ${comparisonExpression.operation}") + + val functionSymbol = comparisonExpression.compareToCall.toResolvedCallableSymbol() + + val functionType = data.embedFunctionPretype(functionSymbol as FirFunctionSymbol) + + val comparisonTemplate = when { + functionType.formalArgTypes.all { it.equalToType { int() } } -> IntComparisonExpEmbeddingsTemplate + functionType.formalArgTypes.all { it.equalToType { char() } } -> CharComparisonExpEmbeddingsTemplate + else -> { + val result = data.convert(comparisonExpression.compareToCall) + return IntComparisonExpEmbeddingsTemplate.retrieve(comparisonExpression.operation)(result, IntLit(0)) + } + } + return comparisonTemplate.retrieve(comparisonExpression.operation)(left, right) + } + + private interface ComparisonExpEmbeddingsTemplate { + fun retrieve(operation: FirOperation): BinaryOperatorExpEmbeddingTemplate + } + + private object IntComparisonExpEmbeddingsTemplate : ComparisonExpEmbeddingsTemplate { + override fun retrieve(operation: FirOperation) = when (operation) { + FirOperation.LT -> LtIntInt + FirOperation.LT_EQ -> LeIntInt + FirOperation.GT -> GtIntInt + FirOperation.GT_EQ -> GeIntInt + else -> throw IllegalArgumentException("Expected comparison operation but found ${operation}.") + } + } + + private object CharComparisonExpEmbeddingsTemplate : ComparisonExpEmbeddingsTemplate { + override fun retrieve(operation: FirOperation) = when (operation) { + FirOperation.LT -> LtCharChar + FirOperation.LT_EQ -> LeCharChar + FirOperation.GT -> GtCharChar + FirOperation.GT_EQ -> GeCharChar + else -> throw IllegalArgumentException("Expected comparison operation but found ${operation}.") } } @@ -193,7 +236,7 @@ object StmtConversionVisitor : FirVisitor() flatMap { arg -> when (arg) { is FirVarargArgumentsExpression -> { - check(function is SpecialVerifyFunction) { + check(function != null && function.isVerifyFunction) { "vararg arguments are currently supported for `verify` function only" } arg.arguments.map(data::convert) 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 606e6dcccf092..c97a245be8afd 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 @@ -6,6 +6,7 @@ package org.jetbrains.kotlin.formver.domains import org.jetbrains.kotlin.formver.embeddings.types.ClassTypeEmbedding +import org.jetbrains.kotlin.formver.embeddings.types.embedClassTypeFunc import org.jetbrains.kotlin.formver.viper.MangledName import org.jetbrains.kotlin.formver.viper.ast.* import org.jetbrains.kotlin.formver.viper.mangled @@ -217,6 +218,13 @@ class RuntimeTypeDomain(classes: List) : BuiltinDomain(RUNTI fun createDomainFunc(funcName: String, args: List, type: Type, unique: Boolean = false) = DomainFunc(DomainFuncName(DomainName(RUNTIME_TYPE_DOMAIN_NAME), funcName), args, emptyList(), type, unique) + private fun createNewTypeDomainFunc(funcName: String) = createDomainFunc( + funcName, + emptyList(), + RuntimeType, + true, + ) + // variables for readability improving private val t = Var("t", RuntimeType) private val t1 = Var("t1", RuntimeType) @@ -240,12 +248,14 @@ class RuntimeTypeDomain(classes: List) : BuiltinDomain(RUNTI infix fun Exp.isOf(elemType: Exp) = isSubtype(typeOf(this), elemType) // built-in types function - val intType = createDomainFunc("intType", emptyList(), RuntimeType, true) - val boolType = createDomainFunc("boolType", emptyList(), RuntimeType, true) - val unitType = createDomainFunc("unitType", emptyList(), RuntimeType, true) - val nothingType = createDomainFunc("nothingType", emptyList(), RuntimeType, true) - val anyType = createDomainFunc("anyType", emptyList(), RuntimeType, true) - val functionType = createDomainFunc("functionType", emptyList(), RuntimeType, true) + val charType = createNewTypeDomainFunc("charType") + val intType = createNewTypeDomainFunc("intType") + val boolType = createNewTypeDomainFunc("boolType") + val unitType = createNewTypeDomainFunc("unitType") + val stringType = createNewTypeDomainFunc("stringType") + val nothingType = createNewTypeDomainFunc("nothingType") + val anyType = createNewTypeDomainFunc("anyType") + val functionType = createNewTypeDomainFunc("functionType") // for creation of user types fun classTypeFunc(name: MangledName) = createDomainFunc(name.mangled, emptyList(), RuntimeType, true) @@ -253,37 +263,10 @@ class RuntimeTypeDomain(classes: List) : BuiltinDomain(RUNTI // bijections to primitive types val intInjection = Injection("int", Type.Int, intType) val boolInjection = Injection("bool", Type.Bool, boolType) - val allInjections = listOf(intInjection, boolInjection) - + val charInjection = Injection("char", Type.Int, charType) + val stringInjection = Injection("string", Type.Seq(Type.Int), stringType) - // Ref translations of primitive operations - private val bothArgsInts = listOf(intInjection, intInjection) - private val bothArgsBools = listOf(boolInjection, boolInjection) - - val plusInts = InjectionImageFunction("plusInts", PlusInts, bothArgsInts, intInjection) - val minusInts = InjectionImageFunction("minusInts", MinusInts, bothArgsInts, intInjection) - val timesInts = InjectionImageFunction("timesInts", TimesInts, bothArgsInts, intInjection) - val divInts = InjectionImageFunction("divInts", DivInts, bothArgsInts, intInjection) { - precondition { - intInjection.fromRef(args[1]) ne 0.toExp() - } - } - val remInts = InjectionImageFunction("remInts", RemInts, bothArgsInts, intInjection) { - precondition { - intInjection.fromRef(args[1]) ne 0.toExp() - } - } - val gtInts = InjectionImageFunction("gtInts", GtInts, bothArgsInts, boolInjection) - val ltInts = InjectionImageFunction("ltInts", LtInts, bothArgsInts, boolInjection) - val geInts = InjectionImageFunction("geInts", GeInts, bothArgsInts, boolInjection) - val leInts = InjectionImageFunction("leInts", LeInts, bothArgsInts, boolInjection) - val notBool = InjectionImageFunction("notBool", NotBool, listOf(boolInjection), boolInjection) - val andBools = InjectionImageFunction("andBools", AndBools, bothArgsBools, boolInjection) - val orBools = InjectionImageFunction("orBools", OrBools, bothArgsBools, boolInjection) - val impliesBools = InjectionImageFunction("impliesBools", ImpliesBools, bothArgsBools, boolInjection) - val accompanyingFunctions: List = listOf( - plusInts, minusInts, timesInts, divInts, remInts, gtInts, ltInts, geInts, leInts, notBool, andBools, orBools, impliesBools - ) + val allInjections = listOf(intInjection, boolInjection, charInjection, stringInjection) // special values val nullValue = createDomainFunc("nullValue", emptyList(), Ref) @@ -291,9 +274,14 @@ class RuntimeTypeDomain(classes: List) : BuiltinDomain(RUNTI } - val classTypes = classes.associateWith { type -> type.runtimeTypeFunc } + val classTypes = classes.associateWith { type -> type.embedClassTypeFunc() } + val builtinTypes = listOf(intType, boolType, charType, unitType, nothingType, anyType, functionType, stringType) + + val nonNullableTypes = buildList { + addAll(builtinTypes) + addAll(classTypes.values) + }.distinctBy { it.name } - val nonNullableTypes = listOf(intType, boolType, unitType, nothingType, anyType, functionType) + classTypes.values override val functions: List = nonNullableTypes + listOf(nullValue, unitValue, isSubtype, typeOf, nullable) + allInjections.flatMap { listOf(it.toRef, it.fromRef) } @@ -420,4 +408,4 @@ class RuntimeTypeDomain(classes: List) : BuiltinDomain(RUNTI } } } -} +} \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/FieldEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/FieldEmbedding.kt index c13bc10387fda..9f90af0d29cb0 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/FieldEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/FieldEmbedding.kt @@ -9,8 +9,8 @@ import org.jetbrains.kotlin.fir.symbols.impl.FirPropertySymbol import org.jetbrains.kotlin.formver.conversion.AccessPolicy 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.expression.OperatorExpEmbeddings.GeIntInt import org.jetbrains.kotlin.formver.embeddings.types.ClassTypeEmbedding import org.jetbrains.kotlin.formver.embeddings.types.FieldAccessTypeInvariantEmbedding import org.jetbrains.kotlin.formver.embeddings.types.TypeInvariantEmbedding @@ -88,7 +88,7 @@ object ListSizeFieldEmbedding : FieldEmbedding { object NonNegativeSizeTypeInvariantEmbedding : TypeInvariantEmbedding { override fun fillHole(exp: ExpEmbedding): ExpEmbedding = - GeCmp(FieldAccess(exp, ListSizeFieldEmbedding), IntLit(0)) + GeIntInt(FieldAccess(exp, ListSizeFieldEmbedding), IntLit(0)) } } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunction.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunction.kt new file mode 100644 index 0000000000000..47966f0c6fe20 --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunction.kt @@ -0,0 +1,162 @@ +/* + * 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.embeddings.callables + +import org.jetbrains.kotlin.formver.embeddings.expression.* +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.AddCharInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.AddIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.AddStringString +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.DivIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.MulIntInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.Not +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.StringGet +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.SubCharChar +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.SubCharInt +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.SubIntInt +import org.jetbrains.kotlin.formver.embeddings.types.buildFunctionPretype +import org.jetbrains.kotlin.formver.names.* +import org.jetbrains.kotlin.formver.viper.MangledName +import org.jetbrains.kotlin.name.CallableId +import org.jetbrains.kotlin.name.FqName +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) + +object SpecialKotlinFunctions { + private val contractBuilderTypeName = buildName { + packageScope(listOf("kotlin", "contracts")) + ClassKotlinName(listOf("ContractBuilder")) + } + private val booleanArrayTypeName = buildName { + packageScope(listOf("kotlin")) + ClassKotlinName(listOf("BooleanArray")) + } + + val byName: Map = buildFullySpecialFunctions { + val intIntToIntType = buildFunctionPretype { + withDispatchReceiver { int() } + withParam { int() } + withReturnType { int() } + } + withCallableType(intIntToIntType) { + addFunction("kotlin", className = "Int", name = "plus") { args, _ -> + AddIntInt(args[0], args[1]) + } + addFunction("kotlin", className = "Int", name = "minus") { args, _ -> + SubIntInt(args[0], args[1]) + } + addFunction("kotlin", className = "Int", name = "times") { args, _ -> + MulIntInt(args[0], args[1]) + } + addFunction("kotlin", className = "Int", name = "div") { args, _ -> + blockOf( + InhaleDirect(NeCmp(args[1], IntLit(0))), + DivIntInt(args[0], args[1]), + ) + } + } + + val booleanToBooleanType = buildFunctionPretype { + withDispatchReceiver { boolean() } + withReturnType { boolean() } + } + + addFunction(booleanToBooleanType, "kotlin", className = "Boolean", name = "not") { args, _ -> + Not(args[0]) + } + + val verifyCallableType = buildFunctionPretype { + withParam { + klass { + withName(booleanArrayTypeName) + } + } + withReturnType { unit() } + } + addFunction(verifyCallableType, "org", "jetbrains", "kotlin", "formver", "plugin", name = "verify") { args, _ -> + args.map { Assert(it) }.toBlock() + } + + val contractCallableType = buildFunctionPretype { + withParam { + function { + withDispatchReceiver { + klass { + withName(contractBuilderTypeName) + } + } + withReturnType { unit() } + } + } + withReturnType { unit() } + } + + addFunction(contractCallableType, "kotlin", "contracts", name = "contract") { _, _ -> + UnitLit + } + + val charCharToIntType = buildFunctionPretype { + withDispatchReceiver { char() } + withParam { char() } + withReturnType { int() } + } + + addFunction(charCharToIntType, "kotlin", className = "Char", name = "minus") { args, _ -> + SubCharChar(args[0], args[1]) + } + + val charIntToCharType = buildFunctionPretype { + withDispatchReceiver { char() } + withParam { int() } + withReturnType { char() } + } + + withCallableType(charIntToCharType) { + addFunction("kotlin", className = "Char", name = "plus") { args, _ -> + AddCharInt(args[0], args[1]) + } + addFunction("kotlin", className = "Char", name = "minus") { args, _ -> + SubCharInt(args[0], args[1]) + } + } + + val stringIntToCharType = buildFunctionPretype { + withDispatchReceiver { string() } + withParam { int() } + withReturnType { char() } + } + + addFunction(stringIntToCharType, "kotlin", className = "String", name = "get") { args, _ -> + StringGet(args[0], args[1]) + } + + val stringStringToStringType = buildFunctionPretype { + withDispatchReceiver { string() } + withParam { string() } + withReturnType { string() } + } + + addFunction(stringStringToStringType, "kotlin", className = "String", name = "plus") { args, _ -> + AddStringString(args[0], args[1]) + } + } +} + +val FunctionEmbedding.isVerifyFunction: Boolean + get() = this is FullySpecialKotlinFunction && NameMatcher.matchClassScope(this.embedName()) { + ifPackageName("org", "jetbrains", "kotlin", "formver", "plugin") { + ifNoReceiver { + ifFunctionName("verify") { + return true + } + } + } + return false + } \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunctionBuilder.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunctionBuilder.kt new file mode 100644 index 0000000000000..300f89bd36125 --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunctionBuilder.kt @@ -0,0 +1,65 @@ +/* + * 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.callables + +import org.jetbrains.kotlin.formver.conversion.StmtConversionContext +import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding +import org.jetbrains.kotlin.formver.embeddings.types.FunctionTypeEmbedding +import org.jetbrains.kotlin.formver.viper.MangledName + +class FullySpecialKotlinFunctionBuilder { + private val byName = mutableMapOf() + + fun withCallableType( + callableType: FunctionTypeEmbedding, + functionsBlock: SpecialKotlinFunctionBuilderWithCallableType.() -> Unit, + ) { + val builderWithCallableType = SpecialKotlinFunctionBuilderWithCallableType(callableType) + + builderWithCallableType.functionsBlock() + } + + fun addFunction( + callableType: FunctionTypeEmbedding, + vararg packageName: String, + className: String? = null, + name: String, + body: (List, StmtConversionContext) -> ExpEmbedding, + ) { + withCallableType(callableType) { + addFunction(*packageName, className = className, name = name, body = body) + } + } + + inner class SpecialKotlinFunctionBuilderWithCallableType(private val callableType: FunctionTypeEmbedding) { + fun addFunction( + vararg packageName: String, + className: String? = null, + name: String, + body: (List, StmtConversionContext) -> ExpEmbedding, + ) { + + val newFunction = object : FullySpecialKotlinFunction { + override val name: String = name + override val packageName = packageName.toList() + override val callableType = this@SpecialKotlinFunctionBuilderWithCallableType.callableType + override val className = className + + override fun insertCall( + args: List, + ctx: StmtConversionContext, + ): ExpEmbedding = body(args, ctx) + } + newFunction.let { byName[it.embedName()] = it } + } + } + + fun complete(): Map = byName +} + +fun buildFullySpecialFunctions(functionsBlock: FullySpecialKotlinFunctionBuilder.() -> Unit): Map = + FullySpecialKotlinFunctionBuilder().apply(functionsBlock).complete() + diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/PartiallySpecialKotlinFunction.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/PartiallySpecialKotlinFunction.kt new file mode 100644 index 0000000000000..59bf8d8f48289 --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/PartiallySpecialKotlinFunction.kt @@ -0,0 +1,53 @@ +/* + * 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.callables + +import org.jetbrains.kotlin.formver.conversion.StmtConversionContext +import org.jetbrains.kotlin.formver.embeddings.expression.ExpEmbedding +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.AddStringString +import org.jetbrains.kotlin.formver.embeddings.types.buildFunctionPretype +import org.jetbrains.kotlin.formver.embeddings.types.equalToType +import org.jetbrains.kotlin.formver.embeddings.types.nullableAny +import org.jetbrains.kotlin.formver.viper.MangledName + +/** + * Base class for implementations of `PartiallySpecialKotlinFunction`s. + */ +abstract class AbstractPartiallySpecialKotlinFunction( + vararg packageName: String, + override val className: String? = null, + override val name: String, +) : PartiallySpecialKotlinFunction { + private var _baseEmbedding: FunctionEmbedding? = null + override val baseEmbedding + get() = _baseEmbedding + + override val packageName = packageName.toList() + + override fun initBaseEmbedding(embedding: FunctionEmbedding) { + check(_baseEmbedding == null) { "Base embedding for partially special function $name already initialized." } + _baseEmbedding = embedding + } +} + +class StringPlusAnyFunction : AbstractPartiallySpecialKotlinFunction("kotlin", className = "String", name = "plus") { + override fun tryInsertCall(args: List, ctx: StmtConversionContext): ExpEmbedding? = + if (args[1].type.equalToType { string() }) AddStringString(args[0], args[1]) else null + + override val callableType = buildFunctionPretype { + withDispatchReceiver { string() } + withParam { nullableAny() } + withReturnType { string() } + } +} + +object PartiallySpecialKotlinFunctions { + val byName: Map + get() = buildList { + add(StringPlusAnyFunction()) + }.associateBy { it.embedName() } +} + diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialFunctions.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialFunctions.kt index 8388470a7a4c6..f0be145f64bd1 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialFunctions.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialFunctions.kt @@ -5,9 +5,10 @@ package org.jetbrains.kotlin.formver.embeddings.callables -import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings object SpecialFunctions { - val all = RuntimeTypeDomain.accompanyingFunctions + val all + get() = OperatorExpEmbeddings.allTemplates.map { it.refsOperation } } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt index c3c2aa1cc3b73..83232a6bc905c 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt @@ -1,175 +1,55 @@ /* - * Copyright 2010-2023 JetBrains s.r.o. and Kotlin Programming Language contributors. + * 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.callables import org.jetbrains.kotlin.formver.conversion.StmtConversionContext -import org.jetbrains.kotlin.formver.embeddings.expression.* -import org.jetbrains.kotlin.formver.embeddings.types.FunctionTypeEmbedding -import org.jetbrains.kotlin.formver.embeddings.types.buildFunctionPretype -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.embeddings.expression.ExpEmbedding import org.jetbrains.kotlin.formver.viper.ast.Method -import org.jetbrains.kotlin.name.CallableId -import org.jetbrains.kotlin.name.FqName -import org.jetbrains.kotlin.name.Name /** - * Kotlin function that should be handled specially by our conversion. + * Some functions are handled specially by our conversion. + * This can be helpful when proving. For example, `Int.plus(Int)` will + * eventually be translated to native operator `+` in Viper. * - * This includes `contract` and operations on primitive types, where providing a full embedding into Viper - * offers more possibilities for reasoning about the code. + * In particular, that means that there won't be a call to the Viper method + * sometimes. */ interface SpecialKotlinFunction : FunctionEmbedding { val packageName: List val className: String? get() = null val name: String - override val viperMethod: Method? - get() = null -} - -val SpecialKotlinFunction.callableId: CallableId - get() = CallableId(FqName.fromSegments(packageName), className?.let { FqName(it) }, Name.identifier(name)) - -fun SpecialKotlinFunction.embedName(): ScopedKotlinName = callableId.embedFunctionName(callableType) - -object KotlinContractFunction : SpecialKotlinFunction { - override val packageName: List = listOf("kotlin", "contracts") - override val name: String = "contract" - - private val contractBuilderTypeName = buildName { - packageScope(packageName) - ClassKotlinName(listOf("ContractBuilder")) - } - - override val callableType: FunctionTypeEmbedding = buildFunctionPretype { - withParam { - function { - withDispatchReceiver { - klass { - withName(contractBuilderTypeName) - } - } - withReturnType { unit() } - } - } - withReturnType { unit() } - } - - override fun insertCall( - args: List, - ctx: StmtConversionContext, - ): ExpEmbedding = UnitLit -} - -abstract class KotlinIntSpecialFunction : SpecialKotlinFunction { - override val packageName: List = listOf("kotlin") - override val className: String? = "Int" - - override val callableType: FunctionTypeEmbedding = buildFunctionPretype { - withDispatchReceiver { int() } - withParam { int() } - withReturnType { int() } - } -} - -object KotlinIntPlusFunctionImplementation : KotlinIntSpecialFunction() { - override val name: String = "plus" - override fun insertCall( - args: List, - ctx: StmtConversionContext, - ): ExpEmbedding = - Add(args[0], args[1]) -} - -object KotlinIntMinusFunctionImplementation : KotlinIntSpecialFunction() { - override val name: String = "minus" - override fun insertCall( - args: List, - ctx: StmtConversionContext, - ): ExpEmbedding = - Sub(args[0], args[1]) } -object KotlinIntTimesFunctionImplementation : KotlinIntSpecialFunction() { - override val name: String = "times" - override fun insertCall( - args: List, - ctx: StmtConversionContext, - ): ExpEmbedding = - Mul(args[0], args[1]) -} - -object KotlinIntDivFunctionImplementation : KotlinIntSpecialFunction() { - override val name: String = "div" - override fun insertCall( - args: List, - ctx: StmtConversionContext, - // TODO: implement this properly, we don't want to evaluate args[1] twice. - ): ExpEmbedding = blockOf( - InhaleDirect(NeCmp(args[1], IntLit(0))), - Div(args[0], args[1]), - ) -} - -abstract class KotlinBooleanSpecialFunction : SpecialKotlinFunction { - override val packageName: List = listOf("kotlin") - override val className: String? = "Boolean" - - override val callableType: FunctionTypeEmbedding = buildFunctionPretype { - withDispatchReceiver { boolean() } - withReturnType { boolean() } - } -} - -object KotlinBooleanNotFunctionImplementation : KotlinBooleanSpecialFunction() { - override val name: String = "not" - override fun insertCall( - args: List, - ctx: StmtConversionContext, - ): ExpEmbedding = - Not(args[0]) +/** + * Kotlin function that will always be handled specially, like aforementioned `Int.plus(Int)`. + */ +interface FullySpecialKotlinFunction : SpecialKotlinFunction { + override val viperMethod: Method? + get() = null } /** - * Represents the `verify` function defined in `org.jetbrains.kotlin.formver.plugin`. + * Kotlin function that will sometimes be handled specially depending on arguments they're called with. + * + * This is useful in cases like `String.plus(Any)`. If `Any` turns out to be a `String` we can substitute + * sequence concatenation in Viper. Otherwise, we're forced to call an actual method (which is stored in `baseEmbedding`). + * + * Currently, `String.plus(Any)` is the sole case when we use this interface. */ -object SpecialVerifyFunction : SpecialKotlinFunction { - override val packageName: List = listOf("org", "jetbrains", "kotlin", "formver", "plugin") - override val name: String = "verify" - +interface PartiallySpecialKotlinFunction : SpecialKotlinFunction { + val baseEmbedding: FunctionEmbedding? + fun tryInsertCall(args: List, ctx: StmtConversionContext): ExpEmbedding? override fun insertCall(args: List, ctx: StmtConversionContext): ExpEmbedding { - return args.map { Assert(it) }.toBlock() + return tryInsertCall(args, ctx) ?: baseEmbedding?.insertCall(args, ctx) + ?: error("Base embedding for partially special function $name not specified") } - override val callableType: FunctionTypeEmbedding = buildFunctionPretype { - withParam { - klass { - withName( - buildName { - packageScope(listOf("kotlin")) - ClassKotlinName(listOf("BooleanArray")) - } - ) - } - } - withReturnType { unit() } - } -} + fun initBaseEmbedding(embedding: FunctionEmbedding) -object SpecialKotlinFunctions { - val byName = listOf( - SpecialVerifyFunction, - KotlinContractFunction, - KotlinIntPlusFunctionImplementation, - KotlinIntMinusFunctionImplementation, - KotlinIntTimesFunctionImplementation, - KotlinIntDivFunctionImplementation, - KotlinBooleanNotFunctionImplementation, - ).associateBy { it.embedName() } + override val viperMethod: Method? + get() = baseEmbedding?.viperMethod } \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Arithmetic.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Arithmetic.kt deleted file mode 100644 index 3fce49d2f79f3..0000000000000 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Arithmetic.kt +++ /dev/null @@ -1,50 +0,0 @@ -/* - * 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.embeddings.expression - -import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain -import org.jetbrains.kotlin.formver.embeddings.types.buildType - -sealed interface IntArithmeticExpression : OperationBaseExpEmbedding { - override val type - get() = buildType { int() } -} - -data class Add( - override val left: ExpEmbedding, - override val right: ExpEmbedding, -) : IntArithmeticExpression { - override val refsOperation = RuntimeTypeDomain.plusInts -} - -data class Sub( - override val left: ExpEmbedding, - override val right: ExpEmbedding, -) : IntArithmeticExpression { - override val refsOperation = RuntimeTypeDomain.minusInts -} - -data class Mul( - override val left: ExpEmbedding, - override val right: ExpEmbedding, -) : IntArithmeticExpression { - override val refsOperation = RuntimeTypeDomain.timesInts -} - -// TODO: handle separately, inhale rhs != 0 -data class Div( - override val left: ExpEmbedding, - override val right: ExpEmbedding, -) : IntArithmeticExpression { - override val refsOperation = RuntimeTypeDomain.divInts -} - -data class Mod( - override val left: ExpEmbedding, - override val right: ExpEmbedding, -) : IntArithmeticExpression { - override val refsOperation = RuntimeTypeDomain.remInts -} diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Boolean.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Boolean.kt deleted file mode 100644 index d3d00e1592327..0000000000000 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Boolean.kt +++ /dev/null @@ -1,60 +0,0 @@ -/* - * 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.embeddings.expression - -import org.jetbrains.kotlin.formver.asPosition -import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain -import org.jetbrains.kotlin.formver.embeddings.SourceRole -import org.jetbrains.kotlin.formver.embeddings.asInfo -import org.jetbrains.kotlin.formver.embeddings.types.buildType -import org.jetbrains.kotlin.formver.linearization.LinearizationContext -import org.jetbrains.kotlin.formver.viper.ast.Exp - -sealed interface BinaryBooleanExpression : OperationBaseExpEmbedding { - override val type - get() = buildType { boolean() } -} - -data class And( - override val left: ExpEmbedding, - override val right: ExpEmbedding, - override val sourceRole: SourceRole? = null, -) : BinaryBooleanExpression { - override val refsOperation - get() = RuntimeTypeDomain.andBools -} - -data class Or( - override val left: ExpEmbedding, - override val right: ExpEmbedding, - override val sourceRole: SourceRole? = null, -) : BinaryBooleanExpression { - override val refsOperation = RuntimeTypeDomain.orBools -} - -data class Implies( - override val left: ExpEmbedding, - override val right: ExpEmbedding, - override val sourceRole: SourceRole? = null, -) : BinaryBooleanExpression { - override val refsOperation = RuntimeTypeDomain.impliesBools -} - -data class Not( - override val inner: ExpEmbedding, - override val sourceRole: SourceRole? = null -) : UnaryDirectResultExpEmbedding { - override val type = buildType { boolean() } - override fun toViper(ctx: LinearizationContext) = - RuntimeTypeDomain.notBool(inner.toViper(ctx), pos = ctx.source.asPosition, info = sourceRole.asInfo) - - override fun toViperBuiltinType(ctx: LinearizationContext): Exp = - Exp.Not(inner.toViperBuiltinType(ctx), pos = ctx.source.asPosition, info = sourceRole.asInfo) -} - -fun List.toConjunction(): ExpEmbedding = - if (isEmpty()) BooleanLit(true) - else reduce { l, r -> And(l, r) } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Comparison.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Comparison.kt index 02421b2fd1d58..47f103f1733fd 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Comparison.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Comparison.kt @@ -47,43 +47,6 @@ sealed interface AnyComparisonExpression : BinaryDirectResultExpEmbedding { ) } -sealed interface IntComparisonExpression : OperationBaseExpEmbedding { - override val type - get() = buildType { boolean() } -} - -data class LtCmp( - override val left: ExpEmbedding, - override val right: ExpEmbedding, - override val sourceRole: SourceRole? = null, -) : IntComparisonExpression { - override val refsOperation: InjectionImageFunction = RuntimeTypeDomain.ltInts -} - -data class LeCmp( - override val left: ExpEmbedding, - override val right: ExpEmbedding, - override val sourceRole: SourceRole? = null, -) : IntComparisonExpression { - override val refsOperation: InjectionImageFunction = RuntimeTypeDomain.leInts -} - -data class GtCmp( - override val left: ExpEmbedding, - override val right: ExpEmbedding, - override val sourceRole: SourceRole? = null, -) : IntComparisonExpression { - override val refsOperation: InjectionImageFunction = RuntimeTypeDomain.gtInts -} - -data class GeCmp( - override val left: ExpEmbedding, - override val right: ExpEmbedding, - override val sourceRole: SourceRole? = null, -) : IntComparisonExpression { - override val refsOperation: InjectionImageFunction = RuntimeTypeDomain.geInts -} - data class EqCmp( override val left: ExpEmbedding, override val right: ExpEmbedding, 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 3b5251b21fd4f..fa50c9b97a388 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 @@ -162,7 +162,7 @@ data class NonDeterministically(val exp: ExpEmbedding) : UnitResultExpEmbedding, get() = listOf(exp) } -data class UnfoldingClassPredicateEmbedding(val predicated: VariableEmbedding, override val inner: ExpEmbedding) : +data class UnfoldingSharedClassPredicateEmbedding(val predicated: VariableEmbedding, override val inner: ExpEmbedding) : UnaryDirectResultExpEmbedding { override val type: TypeEmbedding = inner.type private fun toViperImpl(ctx: LinearizationContext, action: ExpEmbedding.() -> Exp): Exp { diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Literal.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Literal.kt index 8f214daffab20..223bdbabed0b7 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Literal.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Literal.kt @@ -13,58 +13,78 @@ import org.jetbrains.kotlin.formver.embeddings.asInfo import org.jetbrains.kotlin.formver.embeddings.expression.debug.PlaintextLeaf import org.jetbrains.kotlin.formver.embeddings.expression.debug.TreeView import org.jetbrains.kotlin.formver.embeddings.types.buildType +import org.jetbrains.kotlin.formver.embeddings.types.injection import org.jetbrains.kotlin.formver.linearization.LinearizationContext import org.jetbrains.kotlin.formver.viper.ast.Exp +import org.jetbrains.kotlin.formver.viper.ast.viperLiteral -data object UnitLit : UnitResultExpEmbedding { - // No operation: we just want to return unit. - override fun toViperSideEffects(ctx: LinearizationContext) = Unit +interface LiteralEmbedding : PureExpEmbedding { + val value: Any? - override val debugTreeView: TreeView - get() = PlaintextLeaf("Unit") -} + override val debugExtraSubtrees: List + get() = listOf(PlaintextLeaf(value.toString())) -data class IntLit(val value: Int) : PureExpEmbedding { - override val type = buildType { int() } override fun toViper(source: KtSourceElement?): Exp = - RuntimeTypeDomain.intInjection.toRef( - Exp.IntLit(value, source.asPosition, sourceRole.asInfo), + type.injection.toRef( + value.viperLiteral(source.asPosition, sourceRole.asInfo), pos = source.asPosition, - info = sourceRole.asInfo + info = sourceRole.asInfo, ) +} - override val debugName: String - get() = "Int" +data object UnitLit : LiteralEmbedding, UnitResultExpEmbedding { + override fun toViper(ctx: LinearizationContext): Exp = + super.toViper(ctx) - override val debugExtraSubtrees: List - get() = listOf(PlaintextLeaf(value.toString())) + override fun toViperUnusedResult(ctx: LinearizationContext) = + super.toViperUnusedResult(ctx) + + // No operation: we just want to return unit. + override fun toViperSideEffects(ctx: LinearizationContext) = Unit + + override val value = Unit +} + +data class IntLit(override val value: Int) : LiteralEmbedding { + override val type = buildType { int() } + + override val debugName = "Int" } -data class BooleanLit(val value: Boolean, override val sourceRole: SourceRole? = null) : PureExpEmbedding { +data class BooleanLit( + override val value: Boolean, + override val sourceRole: SourceRole? = null +) : LiteralEmbedding { + override val type = buildType { boolean() } - override fun toViper(source: KtSourceElement?): Exp = - RuntimeTypeDomain.boolInjection.toRef( - Exp.BoolLit(value, source.asPosition, sourceRole.asInfo), - pos = source.asPosition, - info = sourceRole.asInfo - ) - override val debugName: String - get() = "Boolean" + override val debugName = "Boolean" +} - override val debugExtraSubtrees: List - get() = listOf(PlaintextLeaf(value.toString())) +data class CharLit( + override val value: Char, +) : LiteralEmbedding { + override val type = buildType { char() } + + override val debugName: String = "Char" +} + +data class StringLit( + override val value: String, +) : LiteralEmbedding { + override val type = buildType { string() } + + override val debugName: String = "String" } -data object NullLit : PureExpEmbedding { +data object NullLit : LiteralEmbedding { + + override val value = null + override val type = buildType { isNullable = true; nothing() } override fun toViper(source: KtSourceElement?): Exp = RuntimeTypeDomain.nullValue(pos = source.asPosition) - override val debugName: String - get() = "Null" - - override val debugExtraSubtrees: List - get() = listOf(PlaintextLeaf("null")) + override val debugName = "Null" } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperationBase.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperationBase.kt deleted file mode 100644 index abf9bb8d6e35e..0000000000000 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperationBase.kt +++ /dev/null @@ -1,31 +0,0 @@ -/* - * 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.expression - -import org.jetbrains.kotlin.formver.asPosition -import org.jetbrains.kotlin.formver.domains.InjectionImageFunction -import org.jetbrains.kotlin.formver.embeddings.asInfo -import org.jetbrains.kotlin.formver.linearization.LinearizationContext -import org.jetbrains.kotlin.formver.viper.ast.Exp - -interface OperationBaseExpEmbedding : BinaryDirectResultExpEmbedding { - val refsOperation: InjectionImageFunction - val builtinsOperation - get() = refsOperation.original - - override fun toViper(ctx: LinearizationContext): Exp { - return refsOperation(left.toViper(ctx), right.toViper(ctx), pos = ctx.source.asPosition, info = sourceRole.asInfo) - } - - override fun toViperBuiltinType(ctx: LinearizationContext): Exp { - return builtinsOperation( - left.toViperBuiltinType(ctx), - right.toViperBuiltinType(ctx), - pos = ctx.source.asPosition, - info = sourceRole.asInfo - ) - } -} diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbedding.kt new file mode 100644 index 0000000000000..5c6ab1cfb3d1b --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbedding.kt @@ -0,0 +1,86 @@ +/* + * 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.expression + +import org.jetbrains.kotlin.formver.asPosition +import org.jetbrains.kotlin.formver.domains.InjectionImageFunction +import org.jetbrains.kotlin.formver.embeddings.SourceRole +import org.jetbrains.kotlin.formver.embeddings.asInfo +import org.jetbrains.kotlin.formver.embeddings.types.TypeEmbedding +import org.jetbrains.kotlin.formver.linearization.LinearizationContext +import org.jetbrains.kotlin.formver.viper.ast.Exp + +interface InjectionBasedExpEmbedding : DirectResultExpEmbedding { + val refsOperation: InjectionImageFunction + val builtinsOperation + get() = refsOperation.original +} + +interface BinaryOperatorExpEmbedding : BinaryDirectResultExpEmbedding, InjectionBasedExpEmbedding { + override fun toViper(ctx: LinearizationContext): Exp { + return refsOperation(left.toViper(ctx), right.toViper(ctx), pos = ctx.source.asPosition, info = sourceRole.asInfo) + } + + override fun toViperBuiltinType(ctx: LinearizationContext): Exp { + return builtinsOperation( + left.toViperBuiltinType(ctx), + right.toViperBuiltinType(ctx), + pos = ctx.source.asPosition, + info = sourceRole.asInfo + ) + } +} + +interface UnaryOperatorExpEmbedding : UnaryDirectResultExpEmbedding, InjectionBasedExpEmbedding { + override fun toViper(ctx: LinearizationContext) = + refsOperation(inner.toViper(ctx), pos = ctx.source.asPosition, info = sourceRole.asInfo) + + override fun toViperBuiltinType(ctx: LinearizationContext) = + builtinsOperation(inner.toViperBuiltinType(ctx), pos = ctx.source.asPosition, info = sourceRole.asInfo) +} + +sealed interface OperatorExpEmbeddingTemplate { + val type: TypeEmbedding + val refsOperation: InjectionImageFunction + + companion object { + fun create( + type: TypeEmbedding, + refsOperation: InjectionImageFunction, + ): OperatorExpEmbeddingTemplate? = when (refsOperation.formalArgs.size) { + 1 -> UnaryOperatorExpEmbeddingTemplate(type, refsOperation) + 2 -> BinaryOperatorExpEmbeddingTemplate(type, refsOperation) + else -> null + } + } +} + +class BinaryOperatorExpEmbeddingTemplate(override val type: TypeEmbedding, override val refsOperation: InjectionImageFunction) : + OperatorExpEmbeddingTemplate { + operator fun invoke(left: ExpEmbedding, right: ExpEmbedding, sourceRole: SourceRole? = null): BinaryOperatorExpEmbedding = + object : BinaryOperatorExpEmbedding { + override val refsOperation: InjectionImageFunction = this@BinaryOperatorExpEmbeddingTemplate.refsOperation + override val type = this@BinaryOperatorExpEmbeddingTemplate.type + override val left = left + override val right = right + override val sourceRole = sourceRole + } +} + +class UnaryOperatorExpEmbeddingTemplate(override val type: TypeEmbedding, override val refsOperation: InjectionImageFunction) : + OperatorExpEmbeddingTemplate { + operator fun invoke(inner: ExpEmbedding, sourceRole: SourceRole? = null): UnaryOperatorExpEmbedding = + object : UnaryOperatorExpEmbedding { + override val refsOperation: InjectionImageFunction = this@UnaryOperatorExpEmbeddingTemplate.refsOperation + override val type = this@UnaryOperatorExpEmbeddingTemplate.type + override val inner = inner + override val sourceRole = sourceRole + } +} + +fun List.toConjunction(): ExpEmbedding = + if (isEmpty()) BooleanLit(true) + else reduce { l, r -> OperatorExpEmbeddings.And(l, r) } diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbeddingBuilder.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbeddingBuilder.kt new file mode 100644 index 0000000000000..502c47ef2222d --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbeddingBuilder.kt @@ -0,0 +1,79 @@ +/* + * 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.expression + +import org.jetbrains.kotlin.formver.domains.FunctionBuilder +import org.jetbrains.kotlin.formver.domains.InjectionImageFunction +import org.jetbrains.kotlin.formver.embeddings.types.* +import org.jetbrains.kotlin.formver.viper.ast.* + + +class OperatorExpEmbeddingBuilder { + private var runtimeTypeFunctionName: String? = null + private var viperApplicable: Applicable? = null + private var callableType: FunctionTypeEmbedding? = null + private var additionalConditions: (FunctionBuilder.() -> Unit)? = null + + fun complete(): OperatorExpEmbeddingTemplate? { + val callableType = callableType ?: error("Signature not specified to buildExpEmbedding.") + val argumentTypes = callableType.formalArgTypes + val returnType = callableType.returnType + val refsOperation = InjectionImageFunction( + runtimeTypeFunctionName ?: error("No name specified for the underlying viper function."), + viperApplicable ?: error("No viper operator specified to build ExpEmbedding."), + argumentTypes.map { it.injection }, + returnType.injection, + additionalConditions ?: { } + ) + return OperatorExpEmbeddingTemplate.create(returnType, refsOperation) + } + + fun setName(name: String) { + check(runtimeTypeFunctionName == null) { "Name for underlying viper function is already set." } + runtimeTypeFunctionName = name + } + + fun setSignature(signature: FunctionTypeEmbedding) { + check(callableType == null) { "Signature to build ExpEmbedding is already set." } + callableType = signature + } + + fun withSignature(block: FunctionPretypeBuilder.() -> Unit) { + setSignature(buildFunctionPretype(block)) + } + + data class ViperCallData( + val args: List, + val pos: Position, + val info: Info, + val trafos: Trafos, + ) + + fun viperImplementation(block: ViperCallData.() -> Exp) { + check(viperApplicable == null) { "Viper implementation for OperatorExpEmbedding is already set." } + viperApplicable = object : Applicable { + override fun toFuncApp(args: List, pos: Position, info: Info, trafos: Trafos): Exp { + return ViperCallData(args, pos, info, trafos).block() + } + } + } + + fun additionalConditions(block: FunctionBuilder.() -> Unit) { + additionalConditions = block + } +} + +inline fun buildOperator(block: OperatorExpEmbeddingBuilder.() -> Unit) = + when (val completed = OperatorExpEmbeddingBuilder().apply(block).complete()) { + is T -> completed + else -> error("Attempt to create OperatorExpEmbedding with non-matching number of arguments.") + } + +fun buildUnaryOperator(block: OperatorExpEmbeddingBuilder.() -> Unit) = + buildOperator(block) + +fun buildBinaryOperator(block: OperatorExpEmbeddingBuilder.() -> Unit) = + buildOperator(block) diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbeddings.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbeddings.kt new file mode 100644 index 0000000000000..1ed1b65ce8c4e --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbeddings.kt @@ -0,0 +1,232 @@ +/* + * 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.expression + +import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain.Companion.intInjection +import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain.Companion.stringInjection +import org.jetbrains.kotlin.formver.embeddings.types.buildFunctionPretype +import org.jetbrains.kotlin.formver.viper.ast.* +import org.jetbrains.kotlin.formver.viper.ast.Exp.Companion.toConjunction + +object OperatorExpEmbeddings { + + private val intIntToIntType + get() = buildFunctionPretype { + withParam { int() } + withParam { int() } + withReturnType { int() } + } + + val AddIntInt = buildBinaryOperator { + setName("plusInts") + setSignature(intIntToIntType) + viperImplementation { Exp.Add(args[0], args[1], pos, info, trafos) } + } + + val SubIntInt = buildBinaryOperator { + setName("minusInts") + setSignature(intIntToIntType) + viperImplementation { Exp.Sub(args[0], args[1], pos, info, trafos) } + } + + val MulIntInt = buildBinaryOperator { + setName("timesInts") + setSignature(intIntToIntType) + viperImplementation { Exp.Mul(args[0], args[1], pos, info, trafos) } + } + + val DivIntInt = buildBinaryOperator { + setName("divInts") + setSignature(intIntToIntType) + viperImplementation { Exp.Div(args[0], args[1], pos, info, trafos) } + additionalConditions { + precondition { + intInjection.fromRef(args[1]) ne 0.toExp() + } + } + } + + val RemIntInt = buildBinaryOperator { + setName("remInts") + setSignature(intIntToIntType) + viperImplementation { Exp.Mod(args[0], args[1], pos, info, trafos) } + additionalConditions { + precondition { + intInjection.fromRef(args[1]) ne 0.toExp() + } + } + } + + private val intIntToBooleanType + get() = buildFunctionPretype { + withParam { int() } + withParam { int() } + withReturnType { boolean() } + } + + val LeIntInt = buildBinaryOperator { + setName("leInts") + setSignature(intIntToBooleanType) + viperImplementation { Exp.LeCmp(args[0], args[1], pos, info, trafos) } + } + + val LtIntInt = buildBinaryOperator { + setName("ltInts") + setSignature(intIntToBooleanType) + viperImplementation { Exp.LtCmp(args[0], args[1], pos, info, trafos) } + } + + val GeIntInt = buildBinaryOperator { + setName("geInts") + setSignature(intIntToBooleanType) + viperImplementation { Exp.GeCmp(args[0], args[1], pos, info, trafos) } + } + + val GtIntInt = buildBinaryOperator { + setName("gtInts") + setSignature(intIntToBooleanType) + viperImplementation { Exp.GtCmp(args[0], args[1], pos, info, trafos) } + } + + val Not = buildUnaryOperator { + setName("notBool") + withSignature { + withParam { boolean() } + withReturnType { boolean() } + } + viperImplementation { Exp.Not(args[0], pos, info, trafos) } + } + + private val booleanBooleanToBooleanType + get() = buildFunctionPretype { + withParam { boolean() } + withParam { boolean() } + withReturnType { boolean() } + } + + val And = buildBinaryOperator { + setName("andBools") + setSignature(booleanBooleanToBooleanType) + viperImplementation { Exp.And(args[0], args[1], pos, info, trafos) } + } + + val Or = buildBinaryOperator { + setName("orBools") + setSignature(booleanBooleanToBooleanType) + viperImplementation { Exp.Or(args[0], args[1], pos, info, trafos) } + } + + val Implies = buildBinaryOperator { + setName("impliesBools") + setSignature(booleanBooleanToBooleanType) + viperImplementation { Exp.Implies(args[0], args[1], pos, info, trafos) } + } + + val SubCharChar = buildBinaryOperator { + setName("subChars") + withSignature { + withParam { char() } + withParam { char() } + withReturnType { int() } + } + viperImplementation { Exp.Sub(args[0], args[1], pos, info, trafos) } + } + + private val charIntToCharType = buildFunctionPretype { + withParam { char() } + withParam { int() } + withReturnType { char() } + } + + val AddCharInt = buildBinaryOperator { + setName("addCharInt") + setSignature(charIntToCharType) + viperImplementation { Exp.Add(args[0], args[1], pos, info, trafos) } + } + + val SubCharInt = buildBinaryOperator { + setName("subCharInt") + setSignature(charIntToCharType) + viperImplementation { Exp.Sub(args[0], args[1], pos, info, trafos) } + } + + private val charCharToBooleanType = buildFunctionPretype { + withParam { char() } + withParam { char() } + withReturnType { boolean() } + } + + val GeCharChar = buildBinaryOperator { + setName("geChars") + setSignature(charCharToBooleanType) + viperImplementation { Exp.GeCmp(args[0], args[1], pos, info, trafos) } + } + + val GtCharChar = buildBinaryOperator { + setName("gtChars") + setSignature(charCharToBooleanType) + viperImplementation { Exp.GtCmp(args[0], args[1], pos, info, trafos) } + } + + val LeCharChar = buildBinaryOperator { + setName("leChars") + setSignature(charCharToBooleanType) + viperImplementation { Exp.LeCmp(args[0], args[1], pos, info, trafos) } + } + + val LtCharChar = buildBinaryOperator { + setName("ltChars") + setSignature(charCharToBooleanType) + viperImplementation { Exp.LtCmp(args[0], args[1], pos, info, trafos) } + } + + val StringLength = buildUnaryOperator { + setName("stringLength") + withSignature { + withParam { string() } + withReturnType { int() } + } + viperImplementation { Exp.SeqLength(args[0], pos, info, trafos) } + } + + val StringGet = buildBinaryOperator { + setName("stringGet") + withSignature { + withParam { string() } + withParam { int() } + withReturnType { char() } + } + viperImplementation { Exp.SeqIndex(args[0], args[1], pos, info, trafos) } + additionalConditions { + precondition { + listOf( + intInjection.fromRef(args[1]) ge 0.toExp(), + intInjection.fromRef(args[1]) lt Exp.SeqLength(stringInjection.fromRef(args[0])) + ).toConjunction() + } + } + } + + val AddStringString = buildBinaryOperator { + setName("addStrings") + withSignature { + withParam { string() } + withParam { string() } + withReturnType { string() } + } + viperImplementation { Exp.SeqAppend(args[0], args[1], pos, info, trafos) } + } + + val allTemplates + get() = listOf( + AddIntInt, SubIntInt, MulIntInt, DivIntInt, RemIntInt, + LeIntInt, GeIntInt, LtIntInt, GtIntInt, + Not, And, Or, Implies, + AddCharInt, SubCharChar, SubCharInt, + LeCharChar, GeCharChar, LtCharChar, GtCharChar, + StringLength, StringGet, AddStringString + ) +} diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassEmbeddingDetails.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassEmbeddingDetails.kt index 1fdaba69d024c..0dcf0e1361ebe 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassEmbeddingDetails.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassEmbeddingDetails.kt @@ -11,7 +11,12 @@ 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, val isInterface: Boolean) : TypeInvariantHolder { +class ClassEmbeddingDetails( + val type: ClassTypeEmbedding, + val isInterface: Boolean, + private val sharedPredicateEnhancer: ClassPredicateEnhancer? = null, + private val uniquePredicateEnhancer: ClassPredicateEnhancer? = null, +) : TypeInvariantHolder { private var _superTypes: List? = null val superTypes: List get() = _superTypes ?: error("Super types of ${type.name} have not been initialised yet.") @@ -37,7 +42,7 @@ class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boole fun initFields(newFields: Map) { check(_fields == null) { "Fields of ${type.name} are already initialised." } _fields = newFields - _sharedPredicate = ClassPredicateBuilder.Companion.build(this, sharedPredicateName) { + _sharedPredicate = ClassPredicateBuilder.build(this, sharedPredicateName) { forEachField { if (isAlwaysReadable) { addAccessPermissions(PermExp.WildcardPerm()) @@ -50,8 +55,9 @@ class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boole forEachSuperType { addAccessToSharedPredicate() } + sharedPredicateEnhancer?.applyAdditionalAssertions(this) } - _uniquePredicate = ClassPredicateBuilder.Companion.build(this, uniquePredicateName) { + _uniquePredicate = ClassPredicateBuilder.build(this, uniquePredicateName) { forEachField { if (isAlwaysReadable) { addAccessPermissions(PermExp.WildcardPerm()) @@ -69,6 +75,7 @@ class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boole forEachSuperType { addAccessToUniquePredicate() } + uniquePredicateEnhancer?.applyAdditionalAssertions(this) } } @@ -123,4 +130,4 @@ class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boole } ?: listOf() } } -} \ No newline at end of file +} diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateBuilder.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateBuilder.kt index d5f4513716ad9..4c4a1e90c672f 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateBuilder.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateBuilder.kt @@ -10,9 +10,11 @@ import org.jetbrains.kotlin.formver.embeddings.UserFieldEmbedding import org.jetbrains.kotlin.formver.embeddings.expression.* import org.jetbrains.kotlin.formver.linearization.pureToViper import org.jetbrains.kotlin.formver.names.DispatchReceiverName +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.name.Name import org.jetbrains.kotlin.utils.addIfNotNull internal class ClassPredicateBuilder private constructor(private val details: ClassEmbeddingDetails) { @@ -41,6 +43,16 @@ internal class ClassPredicateBuilder private constructor(private val details: Cl body.addAll(builder.toAssertionsList()) } + fun forUserFieldNamed(name: String, action: FieldAssertionsBuilder.() -> Unit) { + when (val field = details.fields[SimpleKotlinName(Name.identifier(name))]) { + is UserFieldEmbedding -> { + val builder = FieldAssertionsBuilder(subject, field) + builder.action() + body.addAll(builder.toAssertionsList()) + } + } + } + fun forEachSuperType(action: TypeInvariantsBuilder.() -> Unit) = details.superTypes.forEach { type -> val builder = TypeInvariantsBuilder(type.asTypeEmbedding()) @@ -64,6 +76,10 @@ class FieldAssertionsBuilder(private val subject: VariableEmbedding, private val fun addAccessPermissions(perm: PermExp) = assertions.add(FieldAccessTypeInvariantEmbedding(field, perm).fillHole(subject)) + + fun addEqualsGuarantee(block: ExpEmbedding.() -> ExpEmbedding) { + assertions.add(FieldEqualsInvariant(field, subject.block()).fillHole(subject)) + } } class TypeInvariantsBuilder(private val type: TypeEmbedding) { diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateEnhancer.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateEnhancer.kt new file mode 100644 index 0000000000000..1ec022444a07e --- /dev/null +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateEnhancer.kt @@ -0,0 +1,28 @@ +/* + * 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.types + +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.StringLength + +/** + * Sometimes we want to enhance a predicate with additional assertions. + * Hence, we introduce `ClassPredicateEnhancer`. + */ +sealed class ClassPredicateEnhancer { + internal abstract fun applyAdditionalAssertions(builder: ClassPredicateBuilder) +} + +data object StringSharedPredicateEnhancer : ClassPredicateEnhancer() { + override fun applyAdditionalAssertions(builder: ClassPredicateBuilder) { + builder.apply { + forUserFieldNamed("length") { + addEqualsGuarantee { + StringLength(this) + } + } + } + } +} diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassTypeEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassTypeEmbedding.kt index bb91f6a978e73..73628677fc51d 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassTypeEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassTypeEmbedding.kt @@ -8,6 +8,7 @@ package org.jetbrains.kotlin.formver.embeddings.types import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain import org.jetbrains.kotlin.formver.names.NameMatcher import org.jetbrains.kotlin.formver.names.ScopedKotlinName +import org.jetbrains.kotlin.formver.viper.ast.DomainFunc import org.jetbrains.kotlin.formver.viper.ast.Exp // TODO: incorporate generic parameters. @@ -24,8 +25,7 @@ data class ClassTypeEmbedding(override val name: ScopedKotlinName) : PretypeEmbe val hasDetails: Boolean get() = _details != null - val runtimeTypeFunc = RuntimeTypeDomain.Companion.classTypeFunc(name) - override val runtimeType: Exp = runtimeTypeFunc() + override val runtimeType: Exp = this.embedClassTypeFunc()() override fun accessInvariants(): List = details.accessInvariants() @@ -55,4 +55,18 @@ private fun PretypeEmbedding.isCollectionTypeNamed(name: String): Boolean { } return false } -} \ No newline at end of file +} + +val ClassTypeEmbedding.isString: Boolean + get() = NameMatcher.matchGlobalScope(name) { + ifPackageName("kotlin") { + ifClassName("String") { + return true + } + } + return false + } + +fun ClassTypeEmbedding.embedClassTypeFunc(): DomainFunc = + if (isString) RuntimeTypeDomain.stringType + else RuntimeTypeDomain.classTypeFunc(name) \ No newline at end of file diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/PretypeBuilder.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/PretypeBuilder.kt index 654054837fcff..784ab6a8b785c 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/PretypeBuilder.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/PretypeBuilder.kt @@ -40,6 +40,10 @@ object BooleanPretypeBuilder : PretypeBuilder { override fun complete() = BooleanTypeEmbedding } +object CharPretypeBuilder : PretypeBuilder { + override fun complete() = CharTypeEmbedding +} + class FunctionPretypeBuilder : PretypeBuilder { private val paramTypes = mutableListOf() private var extensionReceiverType: TypeEmbedding? = null diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/PretypeEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/PretypeEmbedding.kt index 089eb4390a0f7..a54e48465a42c 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/PretypeEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/PretypeEmbedding.kt @@ -58,5 +58,10 @@ data object BooleanTypeEmbedding : PretypeEmbedding { override val name = PretypeName("Boolean") } +data object CharTypeEmbedding : PretypeEmbedding { + override val runtimeType = RuntimeTypeDomain.charType() + override val name = PretypeName("Char") +} + fun PretypeEmbedding.asTypeEmbedding() = TypeEmbedding(this, TypeEmbeddingFlags(nullable = false)) diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeBuilder.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeBuilder.kt index 2e73f52297d4f..a8d1dba624d03 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeBuilder.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeBuilder.kt @@ -5,6 +5,9 @@ package org.jetbrains.kotlin.formver.embeddings.types +import org.jetbrains.kotlin.formver.names.ClassKotlinName +import org.jetbrains.kotlin.formver.names.buildName + /** * Builder for a `TypeEmbedding`. @@ -28,6 +31,14 @@ class TypeBuilder { fun any() = AnyPretypeBuilder fun int() = IntPretypeBuilder fun boolean() = BooleanPretypeBuilder + fun char() = CharPretypeBuilder + fun string() = klass { + withName(buildName { + packageScope(listOf("kotlin")) + ClassKotlinName(listOf("String")) + }) + } + fun function(init: FunctionPretypeBuilder.() -> Unit) = FunctionPretypeBuilder().also { it.init() } fun klass(init: ClassPretypeBuilder.() -> Unit) = ClassPretypeBuilder().also { it.init() } fun existing(embedding: PretypeEmbedding) = ExistingPretypeBuilder(embedding) diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeEmbedding.kt index ad34c2fc845e7..76a559f49428a 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeEmbedding.kt @@ -7,6 +7,7 @@ package org.jetbrains.kotlin.formver.embeddings.types import org.jetbrains.kotlin.formver.domains.Injection import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain +import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain.Companion.stringType import org.jetbrains.kotlin.formver.embeddings.expression.debug.PlaintextLeaf import org.jetbrains.kotlin.formver.embeddings.expression.debug.TreeView import org.jetbrains.kotlin.formver.names.* @@ -77,12 +78,19 @@ data class TypeEmbeddingFlags(val nullable: Boolean) { invariant?.let { adjustInvariant(it) } } -inline fun TypeEmbedding.injectionOr(default: () -> Injection): Injection { - if (flags.nullable) return default() +inline fun TypeEmbedding.injectionOr(default: (TypeEmbedding) -> Injection): Injection { + if (flags.nullable) return default(this) + if (equalToType { string() }) return RuntimeTypeDomain.stringInjection return when (this.pretype) { + CharTypeEmbedding -> RuntimeTypeDomain.charInjection IntTypeEmbedding -> RuntimeTypeDomain.intInjection BooleanTypeEmbedding -> RuntimeTypeDomain.boolInjection - else -> default() + else -> default(this) } } +val TypeEmbedding.injection + get() = injectionOr { + error("Type ${it.name} has no injection specified.") + } + diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeInvariantEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeInvariantEmbedding.kt index 0f26e84098f0f..0d34394192c26 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeInvariantEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/TypeInvariantEmbedding.kt @@ -7,6 +7,7 @@ package org.jetbrains.kotlin.formver.embeddings.types import org.jetbrains.kotlin.formver.embeddings.FieldEmbedding import org.jetbrains.kotlin.formver.embeddings.expression.* +import org.jetbrains.kotlin.formver.embeddings.expression.OperatorExpEmbeddings.Implies import org.jetbrains.kotlin.formver.viper.MangledName import org.jetbrains.kotlin.formver.viper.ast.PermExp @@ -35,6 +36,11 @@ data class IfNonNullInvariant(val invariant: TypeInvariantEmbedding) : TypeInvar Implies(NeCmp(exp, NullLit), invariant.fillHole(exp.withType(exp.type.getNonNullable()))) } +data class FieldEqualsInvariant(val field: FieldEmbedding, val comparedWith: ExpEmbedding) : TypeInvariantEmbedding { + override fun fillHole(exp: ExpEmbedding): ExpEmbedding = + EqCmp(PrimitiveFieldAccess(exp, field), comparedWith) +} + data class FieldAccessTypeInvariantEmbedding(val field: FieldEmbedding, val perm: PermExp) : TypeInvariantEmbedding { override fun fillHole(exp: ExpEmbedding): ExpEmbedding = FieldAccessPermissions(exp, field, perm) } diff --git a/plugins/formal-verification/formver.viper/src/org/jetbrains/kotlin/formver/viper/ast/Exp.kt b/plugins/formal-verification/formver.viper/src/org/jetbrains/kotlin/formver/viper/ast/Exp.kt index b2cd7ed9dae3e..173cac73f5da1 100644 --- a/plugins/formal-verification/formver.viper/src/org/jetbrains/kotlin/formver/viper/ast/Exp.kt +++ b/plugins/formal-verification/formver.viper/src/org/jetbrains/kotlin/formver/viper/ast/Exp.kt @@ -360,6 +360,114 @@ sealed interface Exp : IntoSilver { ) } + data class ExplicitSeq( + val args: List, + val pos: Position = Position.NoPosition, + val info: Info = Info.NoInfo, + val trafos: Trafos = Trafos.NoTrafos, + ) : Exp { + override fun toSilver(): viper.silver.ast.ExplicitSeq = + ExplicitSeq( + args.toSilver().toScalaSeq(), + pos.toSilver(), + info.toSilver(), + trafos.toSilver(), + ) + + override val type = Type.Seq(args.first().type) + } + + data class EmptySeq( + val elementType: Type, + val pos: Position = Position.NoPosition, + val info: Info = Info.NoInfo, + val trafos: Trafos = Trafos.NoTrafos, + ) : Exp { + override fun toSilver(): viper.silver.ast.EmptySeq = + viper.silver.ast.EmptySeq.apply( + elementType.toSilver(), + pos.toSilver(), + info.toSilver(), + trafos.toSilver(), + ) + + override val type = Type.Seq(elementType) + } + + data class SeqLength( + val seq: Exp, + val pos: Position = Position.NoPosition, + val info: Info = Info.NoInfo, + val trafos: Trafos = Trafos.NoTrafos, + ) : Exp { + override fun toSilver(): viper.silver.ast.SeqLength = + viper.silver.ast.SeqLength.apply( + seq.toSilver(), + pos.toSilver(), + info.toSilver(), + trafos.toSilver(), + ) + + override val type = Type.Int + } + + data class SeqTake( + val seq: Exp, + val idx: Exp, + val pos: Position = Position.NoPosition, + val info: Info = Info.NoInfo, + val trafos: Trafos = Trafos.NoTrafos, + ) : Exp { + override fun toSilver(): viper.silver.ast.SeqTake = + viper.silver.ast.SeqTake.apply( + seq.toSilver(), + idx.toSilver(), + pos.toSilver(), + info.toSilver(), + trafos.toSilver(), + ) + + override val type = seq.type + } + + data class SeqIndex( + val seq: Exp, + val idx: Exp, + val pos: Position = Position.NoPosition, + val info: Info = Info.NoInfo, + val trafos: Trafos = Trafos.NoTrafos, + ) : Exp { + override fun toSilver(): viper.silver.ast.SeqIndex = + viper.silver.ast.SeqIndex.apply( + seq.toSilver(), + idx.toSilver(), + pos.toSilver(), + info.toSilver(), + trafos.toSilver(), + ) + + override val type = Type.Int + } + + data class SeqAppend( + val left: Exp, + val right: Exp, + val pos: Position = Position.NoPosition, + val info: Info = Info.NoInfo, + val trafos: Trafos = Trafos.NoTrafos, + ) : Exp { + override fun toSilver(): viper.silver.ast.SeqAppend = + viper.silver.ast.SeqAppend.apply( + left.toSilver(), + right.toSilver(), + pos.toSilver(), + info.toSilver(), + trafos.toSilver(), + ) + + override val type = left.type + } + data class Old( val exp: Exp, val pos: Position = Position.NoPosition, @@ -556,3 +664,17 @@ infix fun Exp.implies(other: Exp) = Exp.Implies(this, other) fun Int.toExp() = Exp.IntLit(this) fun Boolean.toExp() = Exp.BoolLit(this) +fun Any?.viperLiteral( + pos: Position = Position.NoPosition, + info: Info = Info.NoInfo, + trafos: Trafos = Trafos.NoTrafos, +): Exp = when (this) { + null -> Exp.NullLit(pos, info, trafos) + is Int -> Exp.IntLit(this, pos, info, trafos) + is Boolean -> Exp.BoolLit(this, pos, info, trafos) + is Char -> Exp.IntLit(this.code, pos, info, trafos) + is String -> + if (isEmpty()) Exp.EmptySeq(Type.Int, pos, info, trafos) + else Exp.ExplicitSeq(map { it.viperLiteral(pos, info, trafos) }, pos, info, trafos) + else -> error("Literal type not known.") +} diff --git a/plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt index 49207968b42bf..7bd3c6c2bed11 100644 --- a/plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt +++ b/plugins/formal-verification/testData/diagnostics/bad_contracts/cond_effects.fir.diag.txt @@ -73,7 +73,7 @@ method f$recursiveContract$TF$T$Int$NT$Any(p$n: Ref, p$x: Ref) returns (ret$0: Ref) ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType()) ensures df$rt$boolFromRef(ret$0) == true ==> - df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$c$pkg$kotlin$String()) + df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$stringType()) { inhale df$rt$isSubtype(df$rt$typeOf(p$n), df$rt$intType()) inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$anyType())) diff --git a/plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt index 62695b8aa516c..c183022290a37 100644 --- a/plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt +++ b/plugins/formal-verification/testData/diagnostics/bad_contracts/is_type_contract.fir.diag.txt @@ -6,7 +6,7 @@ method f$unverifiableTypeCheck$TF$NT$Int(p$x: Ref) returns (ret$0: Ref) ensures true ==> df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$unitType()) { inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$intType())) - ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$c$pkg$kotlin$String())) + ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$stringType())) goto lbl$ret$0 label lbl$ret$0 } diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/full_viper_dump.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/full_viper_dump.fir.diag.txt index 96aec1dfae2e2..976d5c5c45237 100644 --- a/plugins/formal-verification/testData/diagnostics/no_contracts/full_viper_dump.fir.diag.txt +++ b/plugins/formal-verification/testData/diagnostics/no_contracts/full_viper_dump.fir.diag.txt @@ -5,6 +5,8 @@ domain d$rt { unique function df$rt$boolType(): d$rt + unique function df$rt$charType(): d$rt + unique function df$rt$unitType(): d$rt unique function df$rt$nothingType(): d$rt @@ -13,6 +15,8 @@ domain d$rt { unique function df$rt$functionType(): d$rt + unique function df$rt$stringType(): d$rt + unique function df$rt$c$Foo(): d$rt function df$rt$nullValue(): Ref @@ -33,6 +37,14 @@ domain d$rt { function df$rt$boolFromRef(r: Ref): Bool + function df$rt$charToRef(v: Int): Ref + + function df$rt$charFromRef(r: Ref): Int + + function df$rt$stringToRef(v: Seq[Int]): Ref + + function df$rt$stringFromRef(r: Ref): Seq[Int] + axiom rt$subtype_reflexive { (forall t: d$rt ::df$rt$isSubtype(t, t)) } @@ -83,6 +95,10 @@ domain d$rt { df$rt$isSubtype(df$rt$boolType(), df$rt$anyType()) } + axiom { + df$rt$isSubtype(df$rt$charType(), df$rt$anyType()) + } + axiom { df$rt$isSubtype(df$rt$unitType(), df$rt$anyType()) } @@ -99,6 +115,10 @@ domain d$rt { df$rt$isSubtype(df$rt$functionType(), df$rt$anyType()) } + axiom { + df$rt$isSubtype(df$rt$stringType(), df$rt$anyType()) + } + axiom { df$rt$isSubtype(df$rt$c$Foo(), df$rt$anyType()) } @@ -186,10 +206,60 @@ domain d$rt { df$rt$isSubtype(df$rt$typeOf(r), df$rt$boolType()) ==> df$rt$boolToRef(df$rt$boolFromRef(r)) == r) } + + axiom { + (forall v: Int :: + { df$rt$isSubtype(df$rt$typeOf(df$rt$charToRef(v)), df$rt$charType()) } + df$rt$isSubtype(df$rt$typeOf(df$rt$charToRef(v)), df$rt$charType())) + } + + axiom { + (forall v: Int :: + { df$rt$charFromRef(df$rt$charToRef(v)) } + df$rt$charFromRef(df$rt$charToRef(v)) == v) + } + + axiom { + (forall r: Ref :: + { df$rt$charToRef(df$rt$charFromRef(r)) } + df$rt$isSubtype(df$rt$typeOf(r), df$rt$charType()) ==> + df$rt$charToRef(df$rt$charFromRef(r)) == r) + } + + axiom { + (forall v: Seq[Int] :: + { df$rt$isSubtype(df$rt$typeOf(df$rt$stringToRef(v)), df$rt$stringType()) } + df$rt$isSubtype(df$rt$typeOf(df$rt$stringToRef(v)), df$rt$stringType())) + } + + axiom { + (forall v: Seq[Int] :: + { df$rt$stringFromRef(df$rt$stringToRef(v)) } + df$rt$stringFromRef(df$rt$stringToRef(v)) == v) + } + + axiom { + (forall r: Ref :: + { df$rt$stringToRef(df$rt$stringFromRef(r)) } + df$rt$isSubtype(df$rt$typeOf(r), df$rt$stringType()) ==> + df$rt$stringToRef(df$rt$stringFromRef(r)) == r) + } } field bf$x: Ref +function sp$addCharInt(arg1: Ref, arg2: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$charType()) + ensures df$rt$charFromRef(result) == + df$rt$charFromRef(arg1) + df$rt$intFromRef(arg2) + + +function sp$addStrings(arg1: Ref, arg2: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$stringType()) + ensures df$rt$stringFromRef(result) == + df$rt$stringFromRef(arg1) ++ df$rt$stringFromRef(arg2) + + function sp$andBools(arg1: Ref, arg2: Ref): Ref ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) ensures df$rt$boolFromRef(result) == @@ -203,12 +273,24 @@ function sp$divInts(arg1: Ref, arg2: Ref): Ref df$rt$intFromRef(arg1) / df$rt$intFromRef(arg2) +function sp$geChars(arg1: Ref, arg2: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) + ensures df$rt$boolFromRef(result) == + df$rt$charFromRef(arg1) >= df$rt$charFromRef(arg2) + + function sp$geInts(arg1: Ref, arg2: Ref): Ref ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) ensures df$rt$boolFromRef(result) == df$rt$intFromRef(arg1) >= df$rt$intFromRef(arg2) +function sp$gtChars(arg1: Ref, arg2: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) + ensures df$rt$boolFromRef(result) == + df$rt$charFromRef(arg1) > df$rt$charFromRef(arg2) + + function sp$gtInts(arg1: Ref, arg2: Ref): Ref ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) ensures df$rt$boolFromRef(result) == @@ -221,12 +303,24 @@ function sp$impliesBools(arg1: Ref, arg2: Ref): Ref (df$rt$boolFromRef(arg1) ==> df$rt$boolFromRef(arg2)) +function sp$leChars(arg1: Ref, arg2: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) + ensures df$rt$boolFromRef(result) == + df$rt$charFromRef(arg1) <= df$rt$charFromRef(arg2) + + function sp$leInts(arg1: Ref, arg2: Ref): Ref ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) ensures df$rt$boolFromRef(result) == df$rt$intFromRef(arg1) <= df$rt$intFromRef(arg2) +function sp$ltChars(arg1: Ref, arg2: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) + ensures df$rt$boolFromRef(result) == + df$rt$charFromRef(arg1) < df$rt$charFromRef(arg2) + + function sp$ltInts(arg1: Ref, arg2: Ref): Ref ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$boolType()) ensures df$rt$boolFromRef(result) == @@ -263,6 +357,31 @@ function sp$remInts(arg1: Ref, arg2: Ref): Ref df$rt$intFromRef(arg1) % df$rt$intFromRef(arg2) +function sp$stringGet(arg1: Ref, arg2: Ref): Ref + requires df$rt$intFromRef(arg2) >= 0 && + df$rt$intFromRef(arg2) < |df$rt$stringFromRef(arg1)| + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$charType()) + ensures df$rt$charFromRef(result) == + df$rt$stringFromRef(arg1)[df$rt$intFromRef(arg2)] + + +function sp$stringLength(arg1: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$intType()) + ensures df$rt$intFromRef(result) == |df$rt$stringFromRef(arg1)| + + +function sp$subCharInt(arg1: Ref, arg2: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$charType()) + ensures df$rt$charFromRef(result) == + df$rt$charFromRef(arg1) - df$rt$intFromRef(arg2) + + +function sp$subChars(arg1: Ref, arg2: Ref): Ref + ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$intType()) + ensures df$rt$intFromRef(result) == + df$rt$charFromRef(arg1) - df$rt$charFromRef(arg2) + + function sp$timesInts(arg1: Ref, arg2: Ref): Ref ensures df$rt$isSubtype(df$rt$typeOf(result), df$rt$intType()) ensures df$rt$intFromRef(result) == diff --git a/plugins/formal-verification/testData/diagnostics/verifies/contracts/is_type_contract.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/verifies/contracts/is_type_contract.fir.diag.txt index 82296a83f8f31..f4a07b84d8540 100644 --- a/plugins/formal-verification/testData/diagnostics/verifies/contracts/is_type_contract.fir.diag.txt +++ b/plugins/formal-verification/testData/diagnostics/verifies/contracts/is_type_contract.fir.diag.txt @@ -4,10 +4,10 @@ field bf$length: Ref method f$isString$TF$NT$Any(p$x: Ref) returns (ret$0: Ref) ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType()) ensures df$rt$boolFromRef(ret$0) == true ==> - df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$c$pkg$kotlin$String()) + df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$stringType()) { inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$anyType())) - ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$c$pkg$kotlin$String())) + ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$stringType())) goto lbl$ret$0 label lbl$ret$0 } @@ -21,10 +21,10 @@ field bf$length: Ref method f$isString$TF$T$Any(this$extension: Ref) returns (ret$0: Ref) ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType()) ensures df$rt$boolFromRef(ret$0) == true ==> - df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$c$pkg$kotlin$String()) + df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$stringType()) { inhale df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$anyType()) - ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$c$pkg$kotlin$String())) + ret$0 := df$rt$boolToRef(df$rt$isSubtype(df$rt$typeOf(this$extension), df$rt$stringType())) goto lbl$ret$0 label lbl$ret$0 } diff --git a/plugins/formal-verification/testData/diagnostics/verifies/properties_and_fields/private_properties.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/verifies/properties_and_fields/private_properties.fir.diag.txt index 0bde6fbc13fc1..56c03d746b079 100644 --- a/plugins/formal-verification/testData/diagnostics/verifies/properties_and_fields/private_properties.fir.diag.txt +++ b/plugins/formal-verification/testData/diagnostics/verifies/properties_and_fields/private_properties.fir.diag.txt @@ -26,7 +26,7 @@ field bf$c$B$private$field: Ref field bf$length: Ref method f$c$B$getStringField$TF$T$B(this$dispatch: Ref) returns (ret$0: Ref) - ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$c$pkg$kotlin$String()) + ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$stringType()) ensures acc(p$pkg$kotlin$c$String$shared(ret$0), wildcard) { inhale df$rt$isSubtype(df$rt$typeOf(this$dispatch), df$rt$c$B()) diff --git a/plugins/formal-verification/testData/diagnostics/verifies/string/chars.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/verifies/string/chars.fir.diag.txt new file mode 100644 index 0000000000000..427b595c0e6d9 --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/verifies/string/chars.fir.diag.txt @@ -0,0 +1,37 @@ +/chars.kt:(212,221): info: Generated Viper text for testChars: +field bf$char: Ref + +field bf$size: Ref + +method con$c$CharBox$T$Char(p$char: Ref) returns (ret: Ref) + ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$CharBox()) + ensures acc(p$c$CharBox$shared(ret), wildcard) + ensures acc(p$c$CharBox$unique(ret), write) + ensures (unfolding acc(p$c$CharBox$shared(ret), wildcard) in + df$rt$charFromRef(ret.bf$char) == df$rt$charFromRef(p$char)) + + +method f$testChars$TF$T$Char(p$c: Ref) returns (ret$0: Ref) + ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +{ + var l0$box: Ref + var l0$charA: Ref + var anon$0: Ref + var l0$charZ: Ref + inhale df$rt$isSubtype(df$rt$typeOf(p$c), df$rt$charType()) + l0$box := con$c$CharBox$T$Char(df$rt$charToRef(97)) + l0$charA := df$rt$charToRef(97) + unfold acc(p$c$CharBox$shared(l0$box), wildcard) + anon$0 := l0$box.bf$char + assert df$rt$charFromRef(l0$charA) == df$rt$charFromRef(anon$0) + l0$charZ := df$rt$charToRef(122) + assert df$rt$charFromRef(l0$charA) == df$rt$charFromRef(l0$charZ) - 25 + assert df$rt$charFromRef(l0$charA) - df$rt$charFromRef(l0$charZ) == -25 + assert df$rt$charFromRef(l0$charZ) == df$rt$charFromRef(l0$charA) + 25 + assert df$rt$charFromRef(l0$charA) <= df$rt$charFromRef(l0$charZ) + assert df$rt$charFromRef(l0$charA) < df$rt$charFromRef(l0$charZ) + assert df$rt$charFromRef(l0$charZ) > df$rt$charFromRef(l0$charA) + assert df$rt$charFromRef(l0$charZ) >= df$rt$charFromRef(l0$charZ) + label lbl$ret$0 + inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +} diff --git a/plugins/formal-verification/testData/diagnostics/verifies/string/chars.kt b/plugins/formal-verification/testData/diagnostics/verifies/string/chars.kt new file mode 100644 index 0000000000000..b9657ac1d2dd1 --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/verifies/string/chars.kt @@ -0,0 +1,24 @@ +import org.jetbrains.kotlin.formver.plugin.AlwaysVerify +import org.jetbrains.kotlin.formver.plugin.verify +import org.jetbrains.kotlin.formver.plugin.NeverConvert + +class CharBox(val char: Char) + +@AlwaysVerify +fun testChars(c: Char) { + val box = CharBox('a') + val charA = 'a' + verify(charA == box.char) + val charZ = 'z' + verify( + charA == charZ - 25, + charA - charZ == -25, + charZ == charA + 25, + ) + verify( + charA <= charZ, + (charA < charZ), + (charZ > charA), + charZ >= charZ, + ) +} \ No newline at end of file diff --git a/plugins/formal-verification/testData/diagnostics/verifies/string/strings.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/verifies/string/strings.fir.diag.txt new file mode 100644 index 0000000000000..2f1b96c400861 --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/verifies/string/strings.fir.diag.txt @@ -0,0 +1,345 @@ +/strings.kt:(237,245): info: Generated Viper text for testType: +field bf$length: Ref + +field bf$size: Ref + +field bf$str: Ref + +predicate p$c$StringBox$shared(this$dispatch: Ref) { + acc(this$dispatch.bf$str, wildcard) && + acc(p$pkg$kotlin$c$String$shared(this$dispatch.bf$str), wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$str), df$rt$stringType()) +} + +predicate p$c$StringBox$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$str, wildcard) && + acc(p$pkg$kotlin$c$String$shared(this$dispatch.bf$str), wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$str), df$rt$stringType()) +} + +predicate p$pkg$java_io$c$Serializable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$java_io$c$Serializable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$BooleanArray$shared(this$dispatch: Ref) { + acc(this$dispatch.bf$size, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$size), df$rt$intType()) && + acc(p$pkg$kotlin$c$Cloneable$shared(this$dispatch), wildcard) && + acc(p$pkg$java_io$c$Serializable$shared(this$dispatch), wildcard) +} + +predicate p$pkg$kotlin$c$BooleanArray$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$size, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$size), df$rt$intType()) && + acc(p$pkg$kotlin$c$Cloneable$unique(this$dispatch), write) && + acc(p$pkg$java_io$c$Serializable$unique(this$dispatch), write) +} + +predicate p$pkg$kotlin$c$CharSequence$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$CharSequence$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Cloneable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Cloneable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Comparable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Comparable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$String$shared(this$dispatch: Ref) { + acc(this$dispatch.bf$length, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$length), df$rt$intType()) && + acc(p$pkg$kotlin$c$Comparable$shared(this$dispatch), wildcard) && + acc(p$pkg$kotlin$c$CharSequence$shared(this$dispatch), wildcard) && + acc(p$pkg$java_io$c$Serializable$shared(this$dispatch), wildcard) && + df$rt$intFromRef(this$dispatch.bf$length) == + |df$rt$stringFromRef(this$dispatch)| +} + +predicate p$pkg$kotlin$c$String$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$length, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$length), df$rt$intType()) && + acc(p$pkg$kotlin$c$Comparable$unique(this$dispatch), write) && + acc(p$pkg$kotlin$c$CharSequence$unique(this$dispatch), write) && + acc(p$pkg$java_io$c$Serializable$unique(this$dispatch), write) +} + +method con$c$StringBox$T$String(p$str: Ref) returns (ret: Ref) + ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$StringBox()) + ensures acc(p$c$StringBox$shared(ret), wildcard) + ensures acc(p$c$StringBox$unique(ret), write) + ensures (unfolding acc(p$c$StringBox$shared(ret), wildcard) in + df$rt$stringFromRef(ret.bf$str) == df$rt$stringFromRef(p$str)) + + +method f$testType$TF$T$String(p$s: Ref) returns (ret$0: Ref) + ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +{ + var anon$0: Ref + var anon$1: Ref + var anon$2: Ref + var anon$3: Ref + inhale df$rt$isSubtype(df$rt$typeOf(p$s), df$rt$stringType()) + inhale acc(p$pkg$kotlin$c$String$shared(p$s), wildcard) + anon$1 := con$c$StringBox$T$String(p$s) + unfold acc(p$c$StringBox$shared(anon$1), wildcard) + anon$0 := anon$1.bf$str + assert df$rt$stringFromRef(anon$0) == df$rt$stringFromRef(p$s) + anon$3 := con$c$StringBox$T$String(df$rt$stringToRef(Seq(115, 116, 114))) + unfold acc(p$c$StringBox$shared(anon$3), wildcard) + anon$2 := anon$3.bf$str + assert df$rt$stringFromRef(anon$2) == Seq(115, 116, 114) + label lbl$ret$0 + inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +} + +method pg$public$length(this$dispatch: Ref) returns (ret: Ref) + + +/strings.kt:(368,383): info: Generated Viper text for testLengthField: +field bf$length: Ref + +field bf$size: Ref + +field bf$str: Ref + +predicate p$c$StringBox$shared(this$dispatch: Ref) { + acc(this$dispatch.bf$str, wildcard) && + acc(p$pkg$kotlin$c$String$shared(this$dispatch.bf$str), wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$str), df$rt$stringType()) +} + +predicate p$c$StringBox$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$str, wildcard) && + acc(p$pkg$kotlin$c$String$shared(this$dispatch.bf$str), wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$str), df$rt$stringType()) +} + +predicate p$pkg$java_io$c$Serializable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$java_io$c$Serializable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$BooleanArray$shared(this$dispatch: Ref) { + acc(this$dispatch.bf$size, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$size), df$rt$intType()) && + acc(p$pkg$kotlin$c$Cloneable$shared(this$dispatch), wildcard) && + acc(p$pkg$java_io$c$Serializable$shared(this$dispatch), wildcard) +} + +predicate p$pkg$kotlin$c$BooleanArray$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$size, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$size), df$rt$intType()) && + acc(p$pkg$kotlin$c$Cloneable$unique(this$dispatch), write) && + acc(p$pkg$java_io$c$Serializable$unique(this$dispatch), write) +} + +predicate p$pkg$kotlin$c$CharSequence$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$CharSequence$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Cloneable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Cloneable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Comparable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Comparable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$String$shared(this$dispatch: Ref) { + acc(this$dispatch.bf$length, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$length), df$rt$intType()) && + acc(p$pkg$kotlin$c$Comparable$shared(this$dispatch), wildcard) && + acc(p$pkg$kotlin$c$CharSequence$shared(this$dispatch), wildcard) && + acc(p$pkg$java_io$c$Serializable$shared(this$dispatch), wildcard) && + df$rt$intFromRef(this$dispatch.bf$length) == + |df$rt$stringFromRef(this$dispatch)| +} + +predicate p$pkg$kotlin$c$String$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$length, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$length), df$rt$intType()) && + acc(p$pkg$kotlin$c$Comparable$unique(this$dispatch), write) && + acc(p$pkg$kotlin$c$CharSequence$unique(this$dispatch), write) && + acc(p$pkg$java_io$c$Serializable$unique(this$dispatch), write) +} + +method con$c$StringBox$T$String(p$str: Ref) returns (ret: Ref) + ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$StringBox()) + ensures acc(p$c$StringBox$shared(ret), wildcard) + ensures acc(p$c$StringBox$unique(ret), write) + ensures (unfolding acc(p$c$StringBox$shared(ret), wildcard) in + df$rt$stringFromRef(ret.bf$str) == df$rt$stringFromRef(p$str)) + + +method f$testLengthField$TF$T$String(p$s: Ref) returns (ret$0: Ref) + ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +{ + var l0$len: Ref + var anon$0: Ref + var anon$1: Ref + var anon$2: Ref + inhale df$rt$isSubtype(df$rt$typeOf(p$s), df$rt$stringType()) + inhale acc(p$pkg$kotlin$c$String$shared(p$s), wildcard) + unfold acc(p$pkg$kotlin$c$String$shared(p$s), wildcard) + l0$len := p$s.bf$length + anon$2 := con$c$StringBox$T$String(df$rt$stringToRef(Seq(115, 116, 114))) + unfold acc(p$c$StringBox$shared(anon$2), wildcard) + anon$1 := anon$2.bf$str + unfold acc(p$pkg$kotlin$c$String$shared(anon$1), wildcard) + anon$0 := anon$1.bf$length + assert df$rt$intFromRef(anon$0) == 3 + label lbl$ret$0 + inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +} + +method pg$public$length(this$dispatch: Ref) returns (ret: Ref) + + +/strings.kt:(486,493): info: Generated Viper text for testOps: +field bf$length: Ref + +field bf$size: Ref + +predicate p$pkg$java_io$c$Serializable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$java_io$c$Serializable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$BooleanArray$shared(this$dispatch: Ref) { + acc(this$dispatch.bf$size, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$size), df$rt$intType()) && + acc(p$pkg$kotlin$c$Cloneable$shared(this$dispatch), wildcard) && + acc(p$pkg$java_io$c$Serializable$shared(this$dispatch), wildcard) +} + +predicate p$pkg$kotlin$c$BooleanArray$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$size, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$size), df$rt$intType()) && + acc(p$pkg$kotlin$c$Cloneable$unique(this$dispatch), write) && + acc(p$pkg$java_io$c$Serializable$unique(this$dispatch), write) +} + +predicate p$pkg$kotlin$c$CharSequence$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$CharSequence$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Cloneable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Cloneable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Comparable$shared(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$Comparable$unique(this$dispatch: Ref) { + true +} + +predicate p$pkg$kotlin$c$String$shared(this$dispatch: Ref) { + acc(this$dispatch.bf$length, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$length), df$rt$intType()) && + acc(p$pkg$kotlin$c$Comparable$shared(this$dispatch), wildcard) && + acc(p$pkg$kotlin$c$CharSequence$shared(this$dispatch), wildcard) && + acc(p$pkg$java_io$c$Serializable$shared(this$dispatch), wildcard) && + df$rt$intFromRef(this$dispatch.bf$length) == + |df$rt$stringFromRef(this$dispatch)| +} + +predicate p$pkg$kotlin$c$String$unique(this$dispatch: Ref) { + acc(this$dispatch.bf$length, wildcard) && + df$rt$isSubtype(df$rt$typeOf(this$dispatch.bf$length), df$rt$intType()) && + acc(p$pkg$kotlin$c$Comparable$unique(this$dispatch), write) && + acc(p$pkg$kotlin$c$CharSequence$unique(this$dispatch), write) && + acc(p$pkg$java_io$c$Serializable$unique(this$dispatch), write) +} + +method f$pkg$kotlin$c$String$plus$TF$T$String$NT$Any(this$dispatch: Ref, p$other: Ref) + returns (ret: Ref) + ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$stringType()) + ensures acc(p$pkg$kotlin$c$String$shared(ret), wildcard) + + +method f$testOps$TF$T$String(p$s: Ref) returns (ret$0: Ref) + ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +{ + var l0$c: Ref + var anon$0: Ref + var anon$1: Ref + var l0$str: Ref + var l0$helloWorld: Ref + inhale df$rt$isSubtype(df$rt$typeOf(p$s), df$rt$stringType()) + inhale acc(p$pkg$kotlin$c$String$shared(p$s), wildcard) + unfold acc(p$pkg$kotlin$c$String$shared(p$s), wildcard) + anon$0 := p$s.bf$length + if (df$rt$intFromRef(anon$0) > 0) { + l0$c := sp$stringGet(p$s, df$rt$intToRef(0)) + } else { + l0$c := df$rt$charToRef(97)} + if (df$rt$charFromRef(l0$c) == 97) { + anon$1 := df$rt$boolToRef(true) + } else { + var anon$2: Ref + unfold acc(p$pkg$kotlin$c$String$shared(p$s), wildcard) + anon$2 := p$s.bf$length + anon$1 := sp$gtInts(anon$2, df$rt$intToRef(0)) + } + assert df$rt$boolFromRef(anon$1) + l0$str := df$rt$stringToRef(Seq(97, 98, 97)) + assert df$rt$stringFromRef(l0$str)[0] == df$rt$stringFromRef(l0$str)[2] + assert !(df$rt$stringFromRef(l0$str)[1] == df$rt$stringFromRef(l0$str)[0]) + assert df$rt$stringFromRef(l0$str)[1] == 98 + assert Seq(75, 111, 116, 108, 105, 110) ++ Seq(46) ++ + Seq(83, 116, 114, 105, 110, 103) == + Seq(75, 111, 116, 108, 105, 110, 46, 83, 116, 114, 105, 110, 103) + l0$helloWorld := f$pkg$kotlin$c$String$plus$TF$T$String$NT$Any(df$rt$stringToRef(Seq(72, + 101, 108, 108, 111, 32, 87, 111, 114, 108, 100)), df$rt$charToRef(33)) + label lbl$ret$0 + inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType()) +} + +method pg$public$length(this$dispatch: Ref) returns (ret: Ref) + diff --git a/plugins/formal-verification/testData/diagnostics/verifies/string/strings.kt b/plugins/formal-verification/testData/diagnostics/verifies/string/strings.kt new file mode 100644 index 0000000000000..7fc6b851da79c --- /dev/null +++ b/plugins/formal-verification/testData/diagnostics/verifies/string/strings.kt @@ -0,0 +1,35 @@ +// RENDER_PREDICATES + +import org.jetbrains.kotlin.formver.plugin.AlwaysVerify +import org.jetbrains.kotlin.formver.plugin.verify +import org.jetbrains.kotlin.formver.plugin.NeverConvert + +class StringBox(val str: String) + +@AlwaysVerify +fun testType(s: String) { + verify( + StringBox(s).str == s, + StringBox("str").str == "str", + ) +} + +@AlwaysVerify +fun testLengthField(s: String) { + val len = s.length + verify(StringBox("str").str.length == 3) +} + +@AlwaysVerify +fun testOps(s: String) { + val c = if (s.length > 0) s[0] else 'a' + verify(c == 'a' || s.length > 0) + val str = "aba" + verify( + str[0] == str[2], + str[1] != str[0], + str[1] == 'b', + ) + verify("Kotlin" + "." + "String" == "Kotlin.String") + val helloWorld = "Hello World" + '!' +} \ No newline at end of file diff --git a/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java b/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java index f52e313f3aa42..497d01d7b1708 100644 --- a/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java +++ b/plugins/formal-verification/tests-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java @@ -640,5 +640,27 @@ public void testPrivate_properties() { runTest("plugins/formal-verification/testData/diagnostics/verifies/properties_and_fields/private_properties.kt"); } } + + @Nested + @TestMetadata("plugins/formal-verification/testData/diagnostics/verifies/string") + @TestDataPath("$PROJECT_ROOT") + public class String { + @Test + public void testAllFilesPresentInString() { + KtTestUtil.assertAllTestsPresentByMetadataWithExcluded(this.getClass(), new File("plugins/formal-verification/testData/diagnostics/verifies/string"), Pattern.compile("^(.+)\\.kt$"), null, true); + } + + @Test + @TestMetadata("chars.kt") + public void testChars() { + runTest("plugins/formal-verification/testData/diagnostics/verifies/string/chars.kt"); + } + + @Test + @TestMetadata("strings.kt") + public void testStrings() { + runTest("plugins/formal-verification/testData/diagnostics/verifies/string/strings.kt"); + } + } } }