-
Notifications
You must be signed in to change notification settings - Fork 0
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
Improving type guarantees when invoking #233
Improving type guarantees when invoking #233
Conversation
if (argWithInvariants is VariableEmbedding) null to argWithInvariants | ||
else declareAnonVar(callType, argWithInvariants).let { | ||
it to it.variable | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
My impression was that we already make copies of values passed to inlined functions; otherwise the following code is not translated correctly:
class X(var a: Int)
fun f(x: X) : Int = x.a.run { x.a += 1; it }
This isn't an idiomatic example, of course, but do we miscompile it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hm, I added a couple of tests now that check we don't evaluate receiver twice. I'm not able to find any other copies when passing arguments. Anyway this part is just slightly changed logic of what was in this file before.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think I'll try to experiment without this piece of code and report what happens.
fun TypeEmbedding.subTypeInvariant(): SubTypeInvariantEmbedding? = equals(buildType { nullableAny() }).ifFalse { | ||
SubTypeInvariantEmbedding(this) | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this special case really worth it? I guess it reduces the number of inhales we do, but it may be hard to find why nullable any behaves differently. Perhaps with the type decomposition redesign we can do something nicer.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nah, I think it has some sense to introduce this optimization eventually. Particularly because it can enable further optimizations (like .simplified
). But I don't think it should be done like this anyway.
09f5168
to
870e059
Compare
if (returnTarget.variable.type.equalsToType { unit() }) { | ||
returnTarget.variable.withInvariants { proven = true }.toViperUnusedResult(linearizer) | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This code is a bit hard to read because there's no verb: I'm guessing withInvariants
produces an ExpEmbedding
that inhales the invariants?
@@ -39,6 +39,8 @@ fun TypeBuilder.nullableAny(): AnyPretypeBuilder { | |||
|
|||
fun buildType(init: TypeBuilder.() -> PretypeBuilder): TypeEmbedding = TypeBuilder().complete(init) | |||
|
|||
fun TypeEmbedding.equalsToType(init: TypeBuilder.() -> PretypeBuilder) = equals(buildType { init() }) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
nit: equalToType
or equalsType
With this pull request necessary casts are added when calling and returning from lambdas and functions (inline and non-inline).
Before code like
wouldn't work: we only knew that the object returned from
id
had typeAny?
. Therefore, we make casts when entering (inline calls) and returning (from any calls) to keepTypeEmbedding
consistent with kotlin types (this is also needed to correctly represent==
calls etc.)