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

Shorten mangled names #227

Merged
merged 3 commits into from
Jul 24, 2024
Merged

Shorten mangled names #227

merged 3 commits into from
Jul 24, 2024

Conversation

jesyspa
Copy link
Owner

@jesyspa jesyspa commented Jul 12, 2024

Our current mangled names are inconveniently long. I'm working on making them shorter, but it's quite a bit of work; this should make things a bit easier to read without reworking too much.

Assigning both of you as reviewers so you can share your thoughts on the readability; there's no behavioural changes here.

@GrigoriiSolnyshkin
Copy link
Collaborator

By the way, there is a fun issue that I think we should consider at some point. Kotlin is actually allowed to generate properties with the same name in the same scope although the developer can't do it manually. For example, it desugars x++ to something like val <unary> = x; x = x + 1; <unary>. If there is two increments, two val <unary>s are generated.
Something similar happens when desugaring val (x, y) = ... (a fake property with some fixed name for (x, y) is generated) and when using _ as well.
Maybe it is worth to enumerate all the entities with a given name inside the scope.

Copy link
Collaborator

@GrigoriiSolnyshkin GrigoriiSolnyshkin left a comment

Choose a reason for hiding this comment

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

IMO abbreviations seem readable. I would probably stick with lowercase letters between $ because it would be easier to spot them.

In the future I suppose we should document when we use $ and _ as separators and maybe introduce some new ones (as well as some parentheses-like separators which we would use some complex names inside other names, e.g. functions).

@@ -179,8 +179,9 @@ data object LegacyUnspecifiedFunctionTypeEmbedding : UnspecifiedFunctionTypeEmbe

data class FunctionTypeEmbedding(val signature: CallableSignatureData) : UnspecifiedFunctionTypeEmbedding() {
override val name = object : MangledName {
// TODO: this can cause some number of collisions; fix it if it becomes an issue.
Copy link
Collaborator

Choose a reason for hiding this comment

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

I've come up with the following example:

fun foo(int: Int): Int { ... }
fun Int.foo(): Unit { ... }

It seems to be allowed because JVM signature includes return types.
A simpler sample

fun foo(int: Int): Int { ... }
fun foo(int: Int): Unit { ... }

is rejected on the FIR level.
A case like

fun foo(int: Int): Unit { ... }
fun Int.foo(): Unit { ... }

is prohibited on JVM (but seemingly allowed in FIR). As far as I understand this means that this check happens after our plugin.
Did you mean something else in this TODO?

Copy link
Owner Author

Choose a reason for hiding this comment

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

I was actually thinking something like fun foo(a: (Int) -> Unit) vs fun foo(a: () -> Unit, b: Int), but I didn't check.


For types:
* `C` for class
* `F` for function
Copy link
Collaborator

Choose a reason for hiding this comment

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

I would propose EF for extension functions to avoid some potential problems.

Copy link
Owner Author

Choose a reason for hiding this comment

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

We don't currently tag extension functions in any particular way. I'd also personally prefer putting that tag on the type of the parameter, not the function name itself.

override val mangled: String =
"fun_take\$${signature.formalArgTypes.joinToString("$") { it.name.mangled }}\$return\$${signature.returnType.name.mangled}"
"TF\$${signature.formalArgTypes.joinToString("$") { it.name.mangled }}"
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why do we want this TF if we already have F before in functions? It feels like after introduced abbreviations this T is less readable than take before.

Copy link
Owner Author

Choose a reason for hiding this comment

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

Because this is a type, so this makes it consistent with our other types like T_Int. That said, I'm not entirely happy with this either...

@jesyspa
Copy link
Owner Author

jesyspa commented Jul 13, 2024

IMO abbreviations seem readable. I would probably stick with lowercase letters between $ because it would be easier to spot them.

Hmm, that's an interesting one. I feel like the capital letters make it obvious that we're dealing with an abbreviation. But if we make the names more regular, that should be easier to tell anyway.

In the future I suppose we should document when we use $ and _ as separators and maybe introduce some new ones (as well as some parentheses-like separators which we would use some complex names inside other names, e.g. functions).

I agree. I think we use _ when possible because $ looks ugly, but _ can collide because it's allowed in Kotlin names. (On the other hand, so is $ if you escape the name... maybe we should just sanitize it from underscores and stick mostly to underscores?)

@jesyspa jesyspa force-pushed the shorten-names branch 3 times, most recently from cbd0a51 to e2553f7 Compare July 16, 2024 08:37
@GrigoriiSolnyshkin GrigoriiSolnyshkin self-requested a review July 17, 2024 06:49
Copy link
Collaborator

@GrigoriiSolnyshkin GrigoriiSolnyshkin left a comment

Choose a reason for hiding this comment

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

LGTM
I think it's worth to make issues regarding

  1. names of function types
  2. careful approach to separators
    though

@jesyspa
Copy link
Owner Author

jesyspa commented Jul 17, 2024

Discussed with Francesco: the way we handle predicate names (and class names in general) here is unfortunate. I'll figure out some better way before merging.

@jesyspa
Copy link
Owner Author

jesyspa commented Jul 17, 2024

I have some ideas on how to get things to work better, but they rely on names being a bit less ad-hoc, which is a bigger change. Still, I think it's worth doing. I'll try to get it done this week.

@jesyspa
Copy link
Owner Author

jesyspa commented Jul 19, 2024

I think I fixed the issue discussed with @francescoo22 , but now this is blocked on #230

jesyspa added 3 commits July 24, 2024 14:58
Our current mangled names are inconveniently long.  I'm working on
making them shorter, but it's quite a bit of work; this should make
things a bit easier to read without reworking too much.
@jesyspa jesyspa merged commit ce54ae9 into formal-verification Jul 24, 2024
1 check passed
@jesyspa jesyspa deleted the shorten-names branch July 24, 2024 13:11
jesyspa added a commit that referenced this pull request Jul 26, 2024
Our current mangled names are inconveniently long. I'm working on making
them shorter, but it's quite a bit of work; this should make things a
bit easier to read without reworking too much.

Assigning both of you as reviewers so you can share your thoughts on the
readability; there's no behavioural changes here.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants