Embedding for `String`s #244

GrigoriiSolnyshkin · 2024-10-10T10:57:07Z

This pull request introduces embeddings for Kotlin types Char and String.
Chars are translated to Viper integers, whereas Strings are represented by viper sequences.

Note that String is a sequence of viper Ints rather than Refs as this approach should be more lightweight.

Operations implemented:

comparisons for characters
arithmetic for characters
operator get for strings
concatenation of strings
literals for char and strings

Apart from that, this PR

implements builder for registration of Kotlin function which we want to handle separately (and their implementation)
adds functions which are implemented by special ExpEmbeddings only sometimes (depending on the arguments passed)
implements builder for "operator" ExpEmbeddings

Overall, to add some operator on the primitive types it generally needs to be registered twice from now on (rather than thrice or more) and with some quite simple builders

jesyspa

Looks good! There are a few things where I feel like more clarity would help, and I wonder whether we could have fewer special cases.

jesyspa · 2024-10-11T08:08:24Z

...r.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbeddingBuilder.kt

+        val callableType = callableType ?: error("Signature not specified to buildExpEmbedding.")
+        val argumentTypes = callableType.formalArgTypes
+        val returnType = callableType.returnType
+        check(argumentTypes.size == 1 || argumentTypes.size == 2) { "Operator should take exactly two arguments." }


nit: error doesn't match with condition.

...formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbeddings.kt

jesyspa · 2024-10-11T08:11:28Z

...tion/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassEmbeddingDetails.kt

+}
+
+class StringEmbeddingDetails(type: ClassTypeEmbedding) : ClassEmbeddingDetails(type, false) {
+


nit: imho starting a class with an empty line like this looks sloppy, does the autoformatter not remove it?

jesyspa · 2024-10-11T08:13:32Z

...tion/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassEmbeddingDetails.kt

 import org.jetbrains.kotlin.utils.addToStdlib.ifTrue

-class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boolean) : TypeInvariantHolder {
+open class ClassEmbeddingDetails(val type: ClassTypeEmbedding, val isInterface: Boolean) : TypeInvariantHolder {


I am not sure that inheritance is a good idea here. While we are in a situation now where the special cases are all dijsoint, perhaps they could be given some other way, like via constructor parameters or using a method call?

We're redefining an implementation of one of the methods. It seems kind of like inheritance...
We could do sealed base and default / string implementation. Anyway, I don't like how I inherit from the extension function of some builder...

I think the key point is that you aren't really specialising the whole thing, so using composition (with something that might use inheritance itself) would feel more natural/clean to me.

jesyspa · 2024-10-11T08:14:41Z

...tion/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateBuilder.kt

@@ -41,6 +43,16 @@ internal class ClassPredicateBuilder private constructor(private val details: Cl
                body.addAll(builder.toAssertionsList())
            }

+    fun forFieldNamed(name: String, action: FieldAssertionsBuilder.() -> Unit) {
+        when (val field = details.fields[SimpleKotlinName(Name.identifier(name))]) {


Should it be an error if this is used with a non-user field embedding?

jesyspa · 2024-10-11T08:15:32Z

...ication/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassTypeEmbedding.kt

Does the string class need this amount of special treatment? I feel like it's a class like any other when it comes to RTTI

I guess we could do the same with String not being special here.
We could do the same with Booleans, Ints and Chars as well.
It may have some sense to reduce the amount of code we need to add a new primitive type.
On the other hand, it feels nice when these type embeddings have short beautiful names.
My thought regarding String was that it is treated somewhat special in Kotlin (having String literals etc.) and that is the main reason I decided to do it like this

jesyspa · 2024-10-11T08:21:16Z

...core/src/org/jetbrains/kotlin/formver/embeddings/callables/PartiallySpecialKotlinFunction.kt

+/**
+ * Functions that should sometimes be handled separately by our conversion depending on arguments they're called with.
+ */
+interface PartiallySpecialKotlinFunction : SeparatelyHandledKotlinFunction {


I don't quite understand the way this class is meant to be used. Do I understand correctly that baseEmbedding is the function that is called if no special case is triggered, and tryInsertCall is what decides whether the special behaviour should be used or not? Is this all being introduced only for the sake of StringPlusAnyFunction, or are there other cases?

jesyspa · 2024-10-11T08:21:40Z

.../formver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/SpecialKotlinFunction.kt

+import org.jetbrains.kotlin.formver.viper.MangledName
+
+
+interface SeparatelyHandledKotlinFunction : FunctionEmbedding {


Could you elaborate on what you mean by SeparatelyHandled? How is it different from Special?

jesyspa · 2024-10-11T08:23:24Z

.../formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbedding.kt

+import org.jetbrains.kotlin.formver.linearization.LinearizationContext
+import org.jetbrains.kotlin.formver.viper.ast.Exp
+
+interface InjectionBasedExpEmbedding : DirectResultExpEmbedding {


Could you elaborate on the sense in which it is InjectionBased? How should people understand the members?

jesyspa · 2024-10-11T08:24:50Z

.../formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/OperatorExpEmbedding.kt

+        builtinsOperation(inner.toViperBuiltinType(ctx), pos = ctx.source.asPosition, info = sourceRole.asInfo)
+}
+
+class OperatorExpEmbeddingTemplate(val type: TypeEmbedding, val refsOperation: InjectionImageFunction) {


When we pick an operator, it seems like we should already know whether it's binary or unary. Why allow for both types of calls on this type, instead of having two types?

jesyspa

LGTM, but please wait for Ilya's feedback.

jesyspa · 2024-10-24T08:31:43Z

...core/src/org/jetbrains/kotlin/formver/embeddings/callables/PartiallySpecialKotlinFunction.kt

+    val byName: Map<MangledName, FunctionEmbedding>
+        get() = buildList {


Please make this a function instead of a property with a getter.

jesyspa · 2024-10-24T13:16:40Z

...al-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt

@@ -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 {


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.

jesyspa · 2024-10-24T13:17:42Z

...al-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt

+                when {
+                    existing is PartiallySpecialKotlinFunction ->
+                        existing.also { it.initBaseEmbedding(userFunction) }
+                    else -> userFunction.also { methods[symbol.embedName(this)] = it }
+                }


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

jesyspa · 2024-10-24T13:19:13Z

...al-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt

-            val signature = embedFullSignature(symbol)
-            val callable = processCallable(symbol, signature)
-            UserFunctionEmbedding(callable)
+    override fun embedFunction(symbol: FirFunctionSymbol<*>): FunctionEmbedding {


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.

jesyspa · 2024-10-24T13:22:44Z

...ver.core/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunction.kt

+
+fun SpecialKotlinFunction.embedName(): ScopedKotlinName = callableId.embedFunctionName(callableType)
+
+object SpecialKotlinFunctions {


Please add a comment that explains that here we provide ExpEmbedding implementations of built-in Kotlin functions.

jesyspa · 2024-10-24T13:23:44Z

...e/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunctionBuilder.kt

+            name: String,
+            body: (List<ExpEmbedding>, StmtConversionContext) -> ExpEmbedding,
+        ) {
+


nit: unnecessary newline

jesyspa · 2024-10-24T13:24:54Z

...e/src/org/jetbrains/kotlin/formver/embeddings/callables/FullySpecialKotlinFunctionBuilder.kt

+            body: (List<ExpEmbedding>, StmtConversionContext) -> ExpEmbedding,
+        ) {
+
+            val newFunction = object : FullySpecialKotlinFunction {


At this point, should FullySpecialKotlinFunction not have an implementation which this thing passes all the data to, rather than creating a new object for each case? I'm not sure what the trade-offs are. (Maybe FullySpecialKotlinFunction should just be a class?)

jesyspa · 2024-10-24T13:26:24Z

...-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/Literal.kt

 }

-data object NullLit : PureExpEmbedding {
+data object NullLit : LiteralEmbedding {
+


nit: unnecessary newline

jesyspa · 2024-10-24T13:28:11Z

...ion/formver.core/src/org/jetbrains/kotlin/formver/embeddings/types/ClassPredicateEnhancer.kt

+sealed class ClassPredicateEnhancer {
+    internal abstract fun applyAdditionalAssertions(builder: ClassPredicateBuilder)
+}


Why not an interface?

GrigoriiSolnyshkin added 8 commits October 1, 2024 14:29

initial support for chars (no operators yet)

2b6eb83

builder for special kotlin function

732e313

Added builder for OperatorExpEmbeddings based on injections.

7af9a8e

Added implementation of ops with chars.

7ac7b17

Added string without ops.

18869c5

Added string without ops.

3f3e6d4

Added tests

0cf6d42

tests regenerated

1a1bb1c

GrigoriiSolnyshkin requested a review from jesyspa October 10, 2024 10:57

bug with partially special function detected and fixed

f2ca6ff

jesyspa reviewed Oct 11, 2024

View reviewed changes

GrigoriiSolnyshkin added 3 commits October 17, 2024 12:51

operators -> binary / unary operators

1f913d3

special functions hierarchy renamed and documented

ca786ff

make class embedding sealed

91c03b1

GrigoriiSolnyshkin requested a review from ligee October 18, 2024 07:45

GrigoriiSolnyshkin added 2 commits October 24, 2024 07:54

fixed bug with mutable static state

13aaa25

added enhancer for the predicates

99fbb1f

GrigoriiSolnyshkin requested a review from jesyspa October 24, 2024 07:45

jesyspa approved these changes Oct 24, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Embedding for `String`s #244

Embedding for `String`s #244

GrigoriiSolnyshkin commented Oct 10, 2024

jesyspa left a comment

jesyspa Oct 11, 2024

jesyspa Oct 11, 2024

jesyspa Oct 11, 2024

GrigoriiSolnyshkin Oct 17, 2024

jesyspa Oct 17, 2024

jesyspa Oct 11, 2024

jesyspa Oct 11, 2024

GrigoriiSolnyshkin Oct 17, 2024

jesyspa Oct 11, 2024

jesyspa Oct 11, 2024

jesyspa Oct 11, 2024

jesyspa Oct 11, 2024

jesyspa left a comment

jesyspa Oct 24, 2024

jesyspa Oct 24, 2024

jesyspa Oct 24, 2024

jesyspa Oct 24, 2024

jesyspa Oct 24, 2024

jesyspa Oct 24, 2024

jesyspa Oct 24, 2024

jesyspa Oct 24, 2024

jesyspa Oct 24, 2024

		}

		class StringEmbeddingDetails(type: ClassTypeEmbedding) : ClassEmbeddingDetails(type, false) {

		import org.jetbrains.kotlin.formver.viper.MangledName


		interface SeparatelyHandledKotlinFunction : FunctionEmbedding {

		val byName: Map<MangledName, FunctionEmbedding>
		get() = buildList {


		fun SpecialKotlinFunction.embedName(): ScopedKotlinName = callableId.embedFunctionName(callableType)

		object SpecialKotlinFunctions {

Embedding for Strings #244

Are you sure you want to change the base?

Embedding for Strings #244

Conversation

GrigoriiSolnyshkin commented Oct 10, 2024

jesyspa left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jesyspa left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Embedding for `String`s #244

Embedding for `String`s #244