From 00554b4c0051a6083c764a54f2e44da090821f93 Mon Sep 17 00:00:00 2001
From: Komi Golov <anton.golov@jetbrains.com>
Date: Sat, 13 Jul 2024 14:16:38 +0200
Subject: [PATCH] Remove unused function TypeEmbeddings. (#226)

These were used for CallsInPlace; I thought they were still necessary
but I hadn't looked correctly.
---
 .../formver/embeddings/TypeEmbedding.kt       | 19 +++++--------------
 .../embeddings/callables/SpecialMethods.kt    | 17 +----------------
 .../embeddings/expression/ControlFlow.kt      | 19 ++++++-------------
 .../control_flow/loop_invariants.fir.diag.txt |  4 +---
 .../no_contracts/full_viper_dump.fir.diag.txt |  3 ---
 .../no_contracts/function_object.fir.diag.txt |  4 ----
 .../inlining/captured.fir.diag.txt            |  1 -
 7 files changed, 13 insertions(+), 54 deletions(-)

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 026185d31313d..aba29144c08cd 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt
@@ -8,7 +8,10 @@ package org.jetbrains.kotlin.formver.embeddings
 import org.jetbrains.kotlin.formver.domains.Injection
 import org.jetbrains.kotlin.formver.domains.RuntimeTypeDomain
 import org.jetbrains.kotlin.formver.embeddings.callables.CallableSignatureData
-import org.jetbrains.kotlin.formver.names.*
+import org.jetbrains.kotlin.formver.names.ClassScope
+import org.jetbrains.kotlin.formver.names.NameMatcher
+import org.jetbrains.kotlin.formver.names.ScopedKotlinName
+import org.jetbrains.kotlin.formver.names.SimpleKotlinName
 import org.jetbrains.kotlin.formver.viper.MangledName
 import org.jetbrains.kotlin.formver.viper.ast.Exp
 import org.jetbrains.kotlin.formver.viper.ast.PermExp
@@ -164,20 +167,8 @@ data class NullableTypeEmbedding(val elementType: TypeEmbedding) : TypeEmbedding
     override val isNullable = true
 }
 
-abstract class UnspecifiedFunctionTypeEmbedding : TypeEmbedding {
+data class FunctionTypeEmbedding(val signature: CallableSignatureData) : TypeEmbedding {
     override val runtimeType = RuntimeTypeDomain.functionType()
-}
-
-/**
- * Some of our older code requires specific type annotations for built-ins with function types.
- * However, we don't actually want to distinguish these builtins by type, so we introduce this
- * type embedding as a workaround.
- */
-data object LegacyUnspecifiedFunctionTypeEmbedding : UnspecifiedFunctionTypeEmbedding() {
-    override val name: MangledName = SpecialName("legacy_function_object_type")
-}
-
-data class FunctionTypeEmbedding(val signature: CallableSignatureData) : UnspecifiedFunctionTypeEmbedding() {
     override val name = object : MangledName {
         override val mangled: String =
             "fun_take\$${signature.formalArgTypes.joinToString("$") { it.name.mangled }}\$return\$${signature.returnType.name.mangled}"
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialMethods.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialMethods.kt
index 3025fd0b036e1..057a5e35bfd3a 100644
--- a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialMethods.kt
+++ b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialMethods.kt
@@ -5,23 +5,8 @@
 
 package org.jetbrains.kotlin.formver.embeddings.callables
 
-import org.jetbrains.kotlin.formver.embeddings.LegacyUnspecifiedFunctionTypeEmbedding
-import org.jetbrains.kotlin.formver.embeddings.expression.AnonymousVariableEmbedding
-import org.jetbrains.kotlin.formver.linearization.pureToViper
-import org.jetbrains.kotlin.formver.names.SpecialName
 import org.jetbrains.kotlin.formver.viper.ast.BuiltInMethod
-import org.jetbrains.kotlin.formver.viper.ast.Declaration
-import org.jetbrains.kotlin.formver.viper.ast.Exp
-
-object InvokeFunctionObjectMethod : BuiltInMethod(SpecialName("invoke_function_object")) {
-    private val thisArg = AnonymousVariableEmbedding(0, LegacyUnspecifiedFunctionTypeEmbedding)
-
-    override val formalArgs: List<Declaration.LocalVarDecl> = listOf(thisArg.toLocalVarDecl())
-    override val formalReturns: List<Declaration.LocalVarDecl> = listOf()
-    override val pres: List<Exp> = thisArg.accessInvariants().pureToViper(toBuiltin = true)
-    override val posts: List<Exp> = thisArg.allAccessInvariants().pureToViper(toBuiltin = true)
-}
 
 object SpecialMethods {
-    val all = listOf(InvokeFunctionObjectMethod)
+    val all: List<BuiltInMethod> = listOf()
 }
\ No newline at end of file
diff --git a/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ControlFlow.kt b/plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/ControlFlow.kt
index 90fe0af19b5c1..500f296f8c9e1 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
@@ -8,14 +8,16 @@ package org.jetbrains.kotlin.formver.embeddings.expression
 import org.jetbrains.kotlin.formver.asPosition
 import org.jetbrains.kotlin.formver.embeddings.*
 import org.jetbrains.kotlin.formver.embeddings.callables.FullNamedFunctionSignature
-import org.jetbrains.kotlin.formver.embeddings.callables.InvokeFunctionObjectMethod
 import org.jetbrains.kotlin.formver.embeddings.callables.NamedFunctionSignature
 import org.jetbrains.kotlin.formver.embeddings.callables.toMethodCall
 import org.jetbrains.kotlin.formver.embeddings.expression.debug.*
 import org.jetbrains.kotlin.formver.linearization.LinearizationContext
 import org.jetbrains.kotlin.formver.linearization.addLabel
 import org.jetbrains.kotlin.formver.linearization.pureToViper
-import org.jetbrains.kotlin.formver.viper.ast.*
+import org.jetbrains.kotlin.formver.viper.ast.Exp
+import org.jetbrains.kotlin.formver.viper.ast.Label
+import org.jetbrains.kotlin.formver.viper.ast.PermExp
+import org.jetbrains.kotlin.formver.viper.ast.Stmt
 
 // TODO: make a nice BlockBuilder interface.
 data class Block(val exps: List<ExpEmbedding>) : OptionalResultExpEmbedding {
@@ -207,17 +209,8 @@ data class InvokeFunctionObject(val receiver: ExpEmbedding, val args: List<ExpEm
     OnlyToViperExpEmbedding {
     override fun toViper(ctx: LinearizationContext): Exp {
         val variable = ctx.freshAnonVar(type)
-        ctx.addStatement {
-            val receiverViper = receiver.toViper(ctx)
-            for (arg in args) arg.toViperUnusedResult(ctx)
-            // NOTE: Since it is only relevant to update the number of times that a function object is called,
-            // the function call invocation is intentionally not assigned to the return variable
-            InvokeFunctionObjectMethod.toMethodCall(
-                listOf(receiverViper),
-                listOf(),
-                ctx.source.asPosition
-            )
-        }
+        receiver.toViperUnusedResult(ctx)
+        for (arg in args) arg.toViperUnusedResult(ctx)
         // TODO: figure out which exactly invariants we want here
         return variable.withAccessAndProvenInvariants().toViper(ctx)
     }
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop_invariants.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop_invariants.fir.diag.txt
index ca323fb0754ce..19f5a45726ef1 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop_invariants.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/control_flow/loop_invariants.fir.diag.txt
@@ -13,7 +13,6 @@ method global$fun_dynamicLambdaInvariant$fun_take$fun_take$$return$T_Int$return$
   {
     var anonymous$1: Ref
     var anonymous$2: Ref
-    special$invoke_function_object(local$f)
     anonymous$2 := anonymous$1
     inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(anonymous$2), dom$RuntimeType$intType())
     anonymous$0 := global$fun_returnsBoolean$fun_take$$return$T_Boolean()
@@ -44,7 +43,6 @@ method global$fun_functionAssignment$fun_take$fun_take$$return$T_Int$return$T_Un
   {
     var anonymous$1: Ref
     var anonymous$2: Ref
-    special$invoke_function_object(local0$g)
     anonymous$2 := anonymous$1
     inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(anonymous$2), dom$RuntimeType$intType())
     anonymous$0 := global$fun_returnsBoolean$fun_take$$return$T_Boolean()
@@ -81,7 +79,6 @@ method global$fun_conditionalFunctionAssignment$fun_take$T_Boolean$fun_take$$ret
   {
     var anonymous$1: Ref
     var anonymous$2: Ref
-    special$invoke_function_object(local0$g)
     anonymous$2 := anonymous$1
     inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(anonymous$2), dom$RuntimeType$intType())
     anonymous$0 := global$fun_returnsBoolean$fun_take$$return$T_Boolean()
@@ -93,3 +90,4 @@ method global$fun_conditionalFunctionAssignment$fun_take$T_Boolean$fun_take$$ret
 method global$fun_returnsBoolean$fun_take$$return$T_Boolean()
   returns (ret: Ref)
   ensures dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(ret), dom$RuntimeType$boolType())
+
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 98d59b2fb270f..6ef8b614e879e 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
@@ -317,9 +317,6 @@ method global$fun_f$fun_take$$return$T_Unit() returns (ret$0: Ref)
   label label$ret$0
 }
 
-method special$invoke_function_object(anonymous$0: Ref)
-
-
 /full_viper_dump.kt:(172,173): info: Generated ExpEmbedding for global$fun_f$fun_take$$return$T_Unit:
 Function(
     name = global$fun_f$fun_take$$return$T_Unit,
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/function_object.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/function_object.fir.diag.txt
index d18a5982282e8..1215ec66f59ba 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/function_object.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/function_object.fir.diag.txt
@@ -16,7 +16,6 @@ method global$fun_functionObjectCall$fun_take$fun_take$T_Boolean$T_Int$return$T_
   var anonymous$0: Ref
   var anonymous$1: Ref
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(local$g), dom$RuntimeType$functionType())
-  special$invoke_function_object(local$g)
   anonymous$1 := anonymous$0
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(anonymous$1), dom$RuntimeType$intType())
   ret$0 := anonymous$1
@@ -38,13 +37,10 @@ method global$fun_functionObjectNestedCall$fun_take$fun_take$T_Int$return$T_Int$
   var anonymous$5: Ref
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(local$f), dom$RuntimeType$functionType())
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(local$g), dom$RuntimeType$functionType())
-  special$invoke_function_object(local$g)
   anonymous$3 := anonymous$2
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(anonymous$3), dom$RuntimeType$intType())
-  special$invoke_function_object(local$f)
   anonymous$4 := anonymous$1
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(anonymous$4), dom$RuntimeType$intType())
-  special$invoke_function_object(local$f)
   anonymous$5 := anonymous$0
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(anonymous$5), dom$RuntimeType$intType())
   ret$0 := anonymous$5
diff --git a/plugins/formal-verification/testData/diagnostics/no_contracts/inlining/captured.fir.diag.txt b/plugins/formal-verification/testData/diagnostics/no_contracts/inlining/captured.fir.diag.txt
index 67faaa411b5df..8a6cbbe7212a4 100644
--- a/plugins/formal-verification/testData/diagnostics/no_contracts/inlining/captured.fir.diag.txt
+++ b/plugins/formal-verification/testData/diagnostics/no_contracts/inlining/captured.fir.diag.txt
@@ -10,7 +10,6 @@ method global$fun_captureArg$fun_take$fun_take$T_Int$return$T_Int$return$T_Int(l
   var anonymous$2: Ref
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(local$g), dom$RuntimeType$functionType())
   anonymous$0 := dom$RuntimeType$intToRef(0)
-  special$invoke_function_object(local$g)
   anonymous$2 := anonymous$1
   inhale dom$RuntimeType$isSubtype(dom$RuntimeType$typeOf(anonymous$2), dom$RuntimeType$intType())
   ret$2 := anonymous$2