Skip to content

Commit

Permalink
Remove unused function TypeEmbeddings. (#226)
Browse files Browse the repository at this point in the history
These were used for CallsInPlace; I thought they were still necessary
but I hadn't looked correctly.
  • Loading branch information
jesyspa committed Jul 26, 2024
1 parent 8ca3f8f commit 00554b4
Show file tree
Hide file tree
Showing 7 changed files with 13 additions and 54 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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}"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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()
}
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand All @@ -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())

Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 00554b4

Please sign in to comment.