More relaxed aliasing checks for imperative programs

[jad-hamza]

No description provided.

[jad-hamza]

@samarion @vkuncak Is it ok to disable argument aliasing checks for pure functions?

[vkuncak]

How do you define pure? If they are not even subject to transformation then yes. Otherwise if they are only not writing, we need to check.

…

On Fri, Apr 9, 2021, 10:28 Jad Hamza ***@***.***> wrote: @samarion <https://github.com/samarion> @vkuncak <https://github.com/vkuncak> Is it ok to disable argument aliasing checks for pure functions? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#973 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA5CDN5QUOHAMFBCYXWJMHDTH23DZANCNFSM42SRCUKQ> .

[jad-hamza]

I'm not sure about the definition, at least being pure prevents from modifying arguments, but I don't know if local var's are allowed.

Otherwise if they are only not writing, we need to check.

Do you have an example of what can go wrong?

[vkuncak]

I don't, so you can go ahead and assume it is fine. Other effect analyses might declare this to be a no effect: ```scala def f(x, y)= oldx = x.f x.f = 42 assert(x.f == y.f) x.f = oldx ``` because x.f is restored at the end. But we should declare an effect here and thus it would not be pure (please check!), so it should be fine.

…

On Fri, Apr 9, 2021, 15:56 Jad Hamza ***@***.***> wrote: I'm not sure about the definition, at least being pure prevents from modifying arguments, but I don't know if local var's are allowed. Otherwise if they are only not writing, we need to check. Do you have an example of what can go wrong? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#973 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA5CDNYJNTAKLLWY2F5JJS3TH4BQ7ANCNFSM42SRCUKQ> .

[jad-hamza]

Right, your example makes sense, if this was allowed, we could assign x.f and y.f to different values and assert that they're different, which would go through while it shouldn't.

Fortunately this is rejected by the effects checker:

import stainless.annotation._

object Test {
  case class A(var x: BigInt)

  @pure
  def f(a: A) = {
    val oldX = a.x
    a.x = 0
    a.x = oldX
  }
}

with the error:

Functions marked @pure cannot have side-effects

stainless/core/src/main/scala/stainless/extraction/imperative/EffectsChecker.scala

Lines 238 to 242 in bfb5dba

	def checkPurity(fd: FunAbstraction): Unit = {
	val effs = effects(fd.fullBody)
	if ((fd.flags contains IsPure) && !effs.isEmpty)
	throw ImperativeEliminationException(fd, s"Functions marked @pure cannot have side-effects")