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

Split class details into separate object. #224

Merged
merged 2 commits into from
Jul 17, 2024
Merged

Conversation

jesyspa
Copy link
Owner

@jesyspa jesyspa commented Jul 11, 2024

Right now, details like supertypes and properties are all included in the ClassTypeEmbedding. This is unfortunate, because these are data classes, and this breaks the equality definition on them. With this commit, all the mutable data is split off into a separate object. The class type embeddings still aren't quite interchangable, since some may be missing this details object, but at least it's much easier to detect now.

Right now, details like supertypes and properties are all included in
the `ClassTypeEmbedding`.  This is unfortunate, because these are data
classes, and this breaks the equality definition on them.  With this
commit, all the mutable data is split off into a separate object.  The
class type embeddings still aren't quite interchangable, since some may
be missing this `details` object, but at least it's much easier to
detect now.
@@ -38,6 +38,7 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
ProgramConversionContext {
private val methods: MutableMap<MangledName, FunctionEmbedding> = SpecialKotlinFunctions.byName.toMutableMap()
private val classes: MutableMap<MangledName, ClassTypeEmbedding> = mutableMapOf()
private val classDetails: MutableMap<ClassTypeEmbedding, ClassEmbeddingDetails> = mutableMapOf()
Copy link
Collaborator

Choose a reason for hiding this comment

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

Do we actually need classDetails when we have details property in every ClassTypeEmbedding?

Copy link
Collaborator

Choose a reason for hiding this comment

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

I guess there're issues with the initialization order, but I don't quite get them.

Copy link
Owner Author

Choose a reason for hiding this comment

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

The relevant situation here is when you get a class embedding but don't have associated details. I guess in that case we could trust that the copy in classes does have an embedding, though... I'll think about it.

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 ended up removing this map, thanks for the suggestion :)

}
else -> existingEmbedding
val embedding = classes.getOrPut(className) {
ClassTypeEmbedding(className, symbol.classKind == ClassKind.INTERFACE)
}
Copy link
Collaborator

Choose a reason for hiding this comment

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

Intuitively isInterface should be included in details. Did you leave it as is because the situation is much simpler in this case?

Copy link
Owner Author

Choose a reason for hiding this comment

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

Thanks, that's a fair point. I left it because it was in the constructor arguments in ClassTypeEmbedding, but that's not really a good way to do it.

hierarchyPath?.forEach { classType ->
val predAcc = classType.sharedPredicateAccessInvariant().fillHole(receiverWrapper)
val predAcc = classType.details.sharedPredicateAccessInvariant().fillHole(receiverWrapper)
Copy link
Collaborator

Choose a reason for hiding this comment

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

Hmm, I think .details can be omitted here since you've overridden this method anyway.
In general, should we hide those .details calls under some extension functions of TypeEmbedding?

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'm not sure TypeEmbedding is the best place; I'd prefer us to fail explicitly when we need a ClassTypeEmbedding but have something else. We could make functions that forward things to details, but I'm not sure there's much benefit; details is not meant to be private, and being aware you're using the details can be seen as a plus.

@jesyspa jesyspa merged commit bf8db14 into formal-verification Jul 17, 2024
1 check passed
@jesyspa jesyspa deleted the class-split branch July 17, 2024 13:13
jesyspa added a commit that referenced this pull request Jul 26, 2024
Right now, details like supertypes and properties are all included in
the `ClassTypeEmbedding`. This is unfortunate, because these are data
classes, and this breaks the equality definition on them. With this
commit, all the mutable data is split off into a separate object. The
class type embeddings still aren't quite interchangable, since some may
be missing this `details` object, but at least it's much easier to
detect now.
Eric-Song-Nop pushed a commit that referenced this pull request Jul 30, 2024
Right now, details like supertypes and properties are all included in
the `ClassTypeEmbedding`. This is unfortunate, because these are data
classes, and this breaks the equality definition on them. With this
commit, all the mutable data is split off into a separate object. The
class type embeddings still aren't quite interchangable, since some may
be missing this `details` object, but at least it's much easier to
detect now.
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.

2 participants