Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Embedding for Strings #244

Open
wants to merge 14 commits into
base: formal-verification
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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))
}
}

Expand All @@ -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(
Expand All @@ -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(
Expand All @@ -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)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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.*
Expand All @@ -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
Expand All @@ -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<MangledName, FunctionEmbedding> = SpecialKotlinFunctions.byName.toMutableMap()
private val methods: MutableMap<MangledName, FunctionEmbedding> =
SpecialKotlinFunctions.byName.toMutableMap().also {
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not super important, but it's a bit weird that we are making a map, then turning it into a mutable map, and then mutating it again. If this is what we'll do with SpecialKotlinFunctions.byName anyway, maybe let's have it take a mutable map/mutable map builder? That would also make it clear it is stateless.

it.putAll(PartiallySpecialKotlinFunctions.byName)
}
private val classes: MutableMap<MangledName, ClassTypeEmbedding> = mutableMapOf()
private val properties: MutableMap<MangledName, PropertyEmbedding> = mutableMapOf()
private val fields: MutableSet<FieldEmbedding> = mutableSetOf()
Expand Down Expand Up @@ -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 {
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This code here seems to be the reason to have PartiallySpecialKotlinFunction. Let us imagine we decided to only use SpecialKotlinFunction, that would sometimes request an embedding. What piping are we missing for that? I assume ProgramConversionContext would have to be passed somewhere where it currently isn't.

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 }
}
Comment on lines +125 to +129
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: it's a bit strange to have when here when you use if above for almost the same check.

}
else -> existing
}
}

/**
* Returns an embedding of the class type, with details set.
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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()
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,23 @@ 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

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
Expand Down Expand Up @@ -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)
Expand All @@ -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)
)
}

Expand All @@ -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)))
)
}

Expand All @@ -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))
)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -85,6 +95,8 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
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)
}
Expand Down Expand Up @@ -180,20 +192,51 @@ object StmtConversionVisitor : FirVisitor<ExpEmbedding, StmtConversionContext>()
}
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}.")
}
}

private fun List<FirExpression>.withVarargsHandled(data: StmtConversionContext, function: FunctionEmbedding?) =
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)
Expand Down
Loading
Loading