Skip to content

Replace uses of scala.collection.mutable.HashMap#getOrElseUpdate with getOrElse + manual update

Viktor Kuncak requested to merge github/fork/romac/fix-freshen-locals into master

Created by: romac

The issue is due to scala.collection.mutable.HashMap#getOrElseUpdate being broken[1, 2] in Scala v2.11.9 - v2.12.7.

This sometimes resulted in ill-formed code, such as in the following example surfaced in epfl-lara/stainless#433:

BEFORE FRESHENING:

val A$103: (Object$0) => Boolean = (x$186: Object$0) => x$186 is Integer$0
val thiss$7: { x$245: Object$0 | @unchecked isMonoid$0(x$245, A$103) } = thiss$12
val x$178: { x$247: Object$0 | @unchecked A$103(x$247) } = Integer$0(x$180)
val y$17: { x$248: Object$0 | @unchecked A$103(x$248) } = Integer$0(y$19)
val z$10: { x$249: Object$0 | @unchecked A$103(x$249) } = Integer$0(z$12)
@unchecked (append$2(A$103, thiss$7, x$178, append$2(A$103, thiss$7, y$17, z$10)) == append$2(A$103, thiss$7, append$2(A$103, thiss$7, x$178, y$17), z$10))

AFTER FRESHENING:

val A$108: (Object$0) => Boolean = (x$345: Object$0) => x$345 is Integer$0
val thiss$13: { x$346: Object$0 | @unchecked isMonoid$0(x$346, A$108) } = thiss$12
val x$348: { x$347: Object$0 | @unchecked A$108(x$347) } = Integer$0(x$180)
val y$22: { x$349: Object$0 | @unchecked A$108(x$349) } = Integer$0(y$19)
val z$14: { x$350: Object$0 | @unchecked A$108(x$350) } = Integer$0(z$12)
@unchecked (append$2(A$108, thiss$13, x$348, append$2(A$108, thiss$13, y$22, z$15)) == append$2(A$108, thiss$13, append$2(A$108, thiss$13, x$348, y$22), z$15))

Note that z$10 has been freshened twice above: once to z$14, and then again to z$15.

  • [1] scala/bug#10703
  • [2] retronym/scala@5af85b5

Merge request reports