From 1effbea0f2548991721b90ce857a380f0cbc3cb5 Mon Sep 17 00:00:00 2001 From: Komi Golov Date: Wed, 10 Jul 2024 13:25:23 +0200 Subject: [PATCH] Remove dynamic invariants (#223) This was used for `callsInPlace` verification but is no longer necessary. --- .../kotlin/formver/conversion/ProgramConverter.kt | 1 - .../kotlin/formver/embeddings/TypeEmbedding.kt | 10 +--------- .../formver/embeddings/expression/VariableEmbedding.kt | 2 -- 3 files changed, 1 insertion(+), 12 deletions(-) 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 1b03c734ff585d..4589f7a0998462 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 @@ -257,7 +257,6 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi addIfNotNull(it.type.uniquePredicateAccessInvariant()?.fillHole(it)) } } - addAll(subSignature.params.flatMap { it.dynamicInvariants() }) addAll(returnVariable.pureInvariants()) addAll(returnVariable.provenInvariants()) addAll(returnVariable.allAccessInvariants()) diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt index 2b27e955f4da7f..026185d31313d5 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt @@ -71,15 +71,6 @@ interface TypeEmbedding { */ fun pureInvariants(): List = emptyList() - /** - * Invariants that should correlate the old and new value of a value of this type - * over a function call. When a caller gives away permissions to the callee, these - * dynamic invariants give properties about the modifications of the argument as - * part of the functions post conditions. - * This is exclusively necessary for CallsInPlace. - */ - fun dynamicInvariants(): List = emptyList() - /** * Get a nullable version of this type embedding. * @@ -158,6 +149,7 @@ data class NullableTypeEmbedding(val elementType: TypeEmbedding) : TypeEmbedding } override fun accessInvariants(): List = elementType.accessInvariants().map { IfNonNullInvariant(it) } + override fun pureInvariants(): List = elementType.pureInvariants().map { IfNonNullInvariant(it) } // Note: this function will replace accessInvariants when nested unfold will be implemented override fun sharedPredicateAccessInvariant(): TypeInvariantEmbedding? = diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/VariableEmbedding.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/VariableEmbedding.kt index 1b25351df0888c..cca8810a8ad30a 100644 --- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/VariableEmbedding.kt +++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/VariableEmbedding.kt @@ -51,8 +51,6 @@ sealed interface VariableEmbedding : PureExpEmbedding, PropertyAccessEmbedding { fun allAccessInvariants() = accessInvariants() + listOfNotNull(sharedPredicateAccessInvariant()) - fun dynamicInvariants(): List = type.dynamicInvariants().fillHoles(this) - override val debugTreeView: TreeView get() = NamedBranchingNode("Var", PlaintextLeaf(name.mangled)) }