Erasure tries to box call to label def

[gsps]

While migrating inox to Scala 3, I ran into runtime errors stemming from the following code, that has been worked around here: https://github.com/epfl-lara/inox/pull/71/commits/d68120a8b72ff273b2ff2b602a8be870e707de2c

Running the code without the workaround leads to

[error] Exception in thread "main" java.lang.VerifyError: Bad type on operand stack
[error] Exception Details:
[error]   Location:
[error]     inox/solvers/theories/ASCIIStringEncoder.transform$$anonfun$1(C)Lscala/collection/GenTraversableOnce; @352: invokespecial
[error]   Reason:
[error]     Type top (current frame, stack[1]) is not assignable to reference type
[error]   Current Frame:
[error]     bci: @352
[error]     flags: { }
[error]     locals: { integer, 'scala/Some', 'scala/collection/Seq', 'scala/Some', 'scala/collection/Seq', top, top, 'scala/collection/Seq' }
[error]     stack: { top, top, 'java/lang/String' }
[error]   Bytecode:
(...)
[error]   Stackmap Table:
[error]     full_frame(@153,{Integer,Top,Object[#263],Object[#345],Object[#263],Integer,Integer},{})
[error]     full_frame(@162,{},{Object[#403]})
[error]     full_frame(@165,{Integer,Top,Object[#263],Object[#345],Object[#263],Integer,Integer},{Object[#356]})
[error]     chop_frame(@168,2)
[error]     full_frame(@175,{Integer,Object[#345],Object[#263],Object[#345],Object[#263]},{Top,Top})
[error]     full_frame(@254,{Integer,Object[#345],Object[#263],Object[#345],Object[#263],Top,Top,Object[#263]},{Top,Top})
[error]     full_frame(@341,{Integer,Object[#345],Object[#263],Object[#345],Object[#263],Top,Top,Object[#263]},{Top,Top})
[error]     full_frame(@344,{Integer,Object[#345],Object[#263],Object[#345],Object[#263],Top,Top,Object[#263]},{Top,Top,Object[#175]})
[error]     full_frame(@347,{Integer,Top,Object[#263],Object[#345],Object[#263]},{Uninitialized[#168],Uninitialized[#168]})
[error]     full_frame(@352,{Integer,Object[#345],Object[#263],Object[#345],Object[#263],Top,Top,Object[#263]},{Top,Top,Object[#175]})
[error]     full_frame(@355,{Integer,Top,Object[#263],Object[#345],Object[#263]},{Top})
[error]     chop_frame(@358,1)
[error]     full_frame(@365,{},{Object[#403]})
[error]     full_frame(@368,{Integer,Top,Object[#263],Object[#345],Object[#263]},{Top})
[error]     chop_frame(@371,2)
[error]     full_frame(@378,{Integer,Top,Object[#263]},{Top,Top})
[error]     full_frame(@387,{},{Object[#403]})
[error]     full_frame(@390,{Integer,Top,Object[#263]},{Uninitialized[#371],Uninitialized[#371]})
[error]     full_frame(@393,{},{Object[#403]})
[error]     full_frame(@396,{Integer,Top,Object[#263],Object[#345],Object[#263]},{Top})
[error]     at inox.solvers.theories.ASCIIStringEncoder$.apply(ASCIIStringEncoder.scala:119)
[error]     at inox.solvers.theories.package$.Z3(package.scala:16)
[error]     at inox.solvers.SolverFactory$.getFromName(SolverFactory.scala:119)
[error]     at inox.solvers.SolverFactory$.apply(SolverFactory.scala:349)
[error]     at inox.solvers.SolverFactory$.apply(SolverFactory.scala:366)
[error]     at inox.package$$anon$3.createSolver(package.scala:77)
[error]     at inox.Semantics.getSolver$$anonfun$1(Semantics.scala:31)
[error]     at inox.utils.Cache.cached(Caches.scala:14)
[error]     at inox.Semantics.getSolver(Semantics.scala:31)

The underlying problem here is that dotc emits code trying to box a call to a label:

new scala.collection.immutable.StringOps(
  scala.collection.immutable.StringOps.evt2u$(case8(x31)))

where case8 is

def case8(case x34: Some): ErasedValueType(
  scala.collection.immutable.StringOps, String) = ...

I don't have a minimized test case unfortunately, but, as a starting point, this is how I reproduce it:

dotc  -deprecation -unchecked -feature -language:Scala2   -Xprint:erasure  -classpath /home/gs/epfl/D/inox-dotty/unmanaged/scalaz3-unix-64-2.12.jar:/home/gs/.ivy2/local/ch.epfl.lamp/scala-library/0.8.0-bin-SNAPSHOT/jars/scala-library.jar:/home/gs/.ivy2/local/ch.epfl.lamp/dotty-library_0.8/0.8.0-bin-SNAPSHOT/jars/dotty-library_0.8.jar:/home/gs/.ivy2/cache/org.scala-lang/scala-library/jars/scala-library-2.12.4.jar:/home/gs/.ivy2/cache/org.apache.commons/commons-lang3/jars/commons-lang3-3.4.jar:/home/gs/.ivy2/cache/org.scala-lang/scala-reflect/jars/scala-reflect-2.12.4.jar:/home/gs/.ivy2/cache/com.regblanc/scala-smtlib_2.12/jars/scala-smtlib_2.12-0.2.2-7-g00a9686.jar:/home/gs/.ivy2/cache/uuverifiers/princess_2.12/jars/princess_2.12-2016-12-26.jar:/home/gs/.ivy2/cache/uuverifiers/princess-parser_2.12/jars/princess-parser_2.12-2016-12-26.jar:/home/gs/.ivy2/cache/uuverifiers/princess-smt-parser_2.12/jars/princess-smt-parser_2.12-2016-12-26.jar:/home/gs/.ivy2/cache/org.scala-lang.modules/scala-parser-combinators_2.12/bundles/scala-parser-combinators_2.12-1.0.4.jar:/home/gs/.ivy2/cache/net.sf.squirrel-sql.thirdparty-non-maven/java-cup/jars/java-cup-0.11a.jar:/home/gs/epfl/D/inox-dotty/target/scala-0.8/classes/      /home/gs/epfl/D/inox-dotty/src/main/scala/inox/solvers/theories/ASCIIStringEncoder.scala

[smarter]

Minimal example:

case class Foo(str: String)

object Test {
  def test(x: Any): Unit = {
    val vc: Any = x match {
      case Foo("") =>
        42
      case _ =>
        10
    }
  }
}

After erasure we get:

        val vc: Object = 
          {
            case val x4: Object = x
            <label> def case6(): Int = 10
            if x4.isInstanceOf[Foo] then 
              {
                case val x5: Foo = x4.asInstanceOf[Foo]
                case val x6: Foo = Foo.unapply(x5)
                case val x7: String = x6._1()
                if "".==(x7) then scala.Int.box(42) else scala.Int.box(case6())
              }
             else scala.Int.box(case6())
          }

Notice the boxing around case6.

[smarter]

Fixing this will require special casing label defs in Erasure. In general, this also illustrates that many transformations are unsafe on label defs compared to defs. This isn't great since we expose label defs in Tasty and thus presumably in the macro API. This might be the tipping point for moving to Scala.js-like labeled blocks as advocated by @sjrd :).

[sjrd]

Ah ah! I will make my labeled blocks a reality. I will! 😛

[allanrenucci]

Notice the boxing around case6.

@smarter The expected type is Object, why is it an issue to box around case6?

[sjrd]

Hum, @smarter's minimal example does not seem to be a reproduction, indeed. With or without extends AnyVal, and also making sure to run it and hit all possible code paths in the match, both master and #4982 correctly compile and run:

case class Foo(str: String) extends AnyVal

object Test {
  def main(args: Array[String]): Unit = {
    test(Foo("one"))
    test(Foo(""))
    test("two")
  }

  def test(x: Any): Unit = {
    val vc: Any = x match {
      case Foo("") =>
        42
      case _ =>
        10
    }
    println(vc)
  }
}

result:

10
42
10

[sjrd]

OK this is an actual reproduction:

case class Foo(str: String) extends AnyVal

object Test {
  def main(args: Array[String]): Unit = {
    test(Foo("one"))
    test(Foo(""))
    test("two")
  }

  def test(x: Any): Unit = {
    val vc: Any = x match {
      case Foo("") =>
        Foo("42")
      case _ =>
        Foo("10")
    }
    println(vc)
  }
}

On master:

Exception in thread "main" java.lang.VerifyError: Bad type on operand stack
Exception Details:
  Location:
    Test$.test(Ljava/lang/Object;)V @108: invokespecial
  Reason:
    Type top (current frame, stack[1]) is not assignable to reference type
  Current Frame:
    bci: @108
    flags: { }
    locals: { 'Test$', 'java/lang/Object', top, 'java/lang/Object' }
    stack: { top, top, 'java/lang/String' }
  Bytecode:
    0x0000000: 2b4e 2dc1 0014 9900 512d c700 0701 a700
    0x0000010: 0a2d c000 14b6 0030 3a04 b200 1919 04b6
    0x0000020: 0033 3a05 b200 1919 05b6 0036 3a06 1228
    0x0000030: 1906 b600 3a99 0015 bb00 1459 b200 1912
    0x0000040: 3cb6 001f b700 22a7 000d bb00 1459 a700
    0x0000050: 1000 00bf a700 1bbb 0014 59a7 000e b200
    0x0000060: 1912 3eb6 001f a700 06a7 fff5 b700 224d
    0x0000070: b200 432c b600 46b1                    
  Stackmap Table:
    append_frame(@17,Top,Object[#4])
    same_locals_1_stack_item_frame(@24,Object[#75])
    append_frame(@74,Object[#75],Object[#75],Object[#75])
    full_frame(@81,{},{Object[#77]})
    full_frame(@84,{Object[#2],Object[#4],Top,Object[#4],Object[#75],Object[#75],Object[#75]},{Object[#20]})
    chop_frame(@87,3)
    full_frame(@94,{Object[#2],Object[#4],Top,Object[#4]},{Top,Top})
    full_frame(@105,{Object[#2],Object[#4],Top,Object[#4]},{Uninitialized[#87],Uninitialized[#87]})
    full_frame(@108,{Object[#2],Object[#4],Top,Object[#4]},{Top,Top,Object[#75]})
    same_locals_1_stack_item_frame(@111,Top)

        at Test.main(i4563.scala)

On #4982:

Foo(10)
Foo(42)
Foo(10)

[smarter]

@smarter The expected type is Object, why is it an issue to box around case6?

Because case6 is a labeldef which should always be a tailcall. Looks like it doesn't cause a miscompilation here, my bad.