Skip to content

Erasure tries to box call to label def #4563

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

Closed
gsps opened this issue May 22, 2018 · 7 comments · Fixed by #4982
Closed

Erasure tries to box call to label def #4563

gsps opened this issue May 22, 2018 · 7 comments · Fixed by #4982

Comments

@gsps
Copy link
Contributor

gsps commented May 22, 2018

While migrating inox to Scala 3, I ran into runtime errors stemming from the following code, that has been worked around here: epfl-lara/inox@d68120a

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
Copy link
Member

smarter commented May 22, 2018

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
Copy link
Member

smarter commented May 22, 2018

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
Copy link
Member

sjrd commented May 22, 2018

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

@allanrenucci
Copy link
Contributor

Notice the boxing around case6.

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

@sjrd
Copy link
Member

sjrd commented Aug 24, 2018

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
Copy link
Member

sjrd commented Aug 24, 2018

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
Copy link
Member

smarter commented Aug 24, 2018

@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.

sjrd added a commit to sjrd/dotty that referenced this issue Aug 24, 2018
sjrd added a commit to sjrd/dotty that referenced this issue Aug 24, 2018
sjrd added a commit to sjrd/dotty that referenced this issue Aug 24, 2018
sjrd added a commit to sjrd/dotty that referenced this issue Aug 26, 2018
A Labeled block is an expression tree of the form

  label[T]: {
    expr
  }

where `expr` must conform to the type `T`. In addition, within
`expr` (but nowhere else), return from the label is allowed:

  return[label] e

where `e` must conform to the type `T` as well.

If execution of `expr` completes normally (rather than throwing an
exception or returning, etc.), then the result of evaluating the
`Labeled` block is the result of `expr`. If a `return[label] e` is
reached, the execution of `expr` is interrupted, and the result of
evaluating the `Labeled` block is the result of evaluating the
argument `e`.

Implementation-wise, a `Labeled` block is represented as a `Tree`
with the shape:

  Labeled(Bind(labelName), expr)

where the `Bind` nodes holds the definition of the label symbol.
That symbol is a term symbol with the flag `Label` (but not
`Method`, unlike symbols for label-defs) and whose `info` is the
result type `T` of the labeled block.

We use those new `Labeled` blocks in `PatternMatcher`, instead of
label-defs. This is the first step towards completely removing
label-defs from the compiler.

This commit structurally fixes a few issues:

* It fixes scala#1313 through the `mergeTests` optimization.
* It fixes scala#4563 because Labeled blocks are erasure-friendly.
* It does a big step towards fixing the upstream test t10387: the
  compiler can get to the back-end on that test, but it produces
  too much bytecode for a single JVM method. We do add a sister
  test t10387b which works because optimizations can kick in.
sjrd added a commit to sjrd/dotty that referenced this issue Aug 26, 2018
A Labeled block is an expression tree of the form

  label[T]: {
    expr
  }

where `expr` must conform to the type `T`. In addition, within
`expr` (but nowhere else), return from the label is allowed:

  return[label] e

where `e` must conform to the type `T` as well.

If execution of `expr` completes normally (rather than throwing an
exception or returning, etc.), then the result of evaluating the
`Labeled` block is the result of `expr`. If a `return[label] e` is
reached, the execution of `expr` is interrupted, and the result of
evaluating the `Labeled` block is the result of evaluating the
argument `e`.

Implementation-wise, a `Labeled` block is represented as a `Tree`
with the shape:

  Labeled(Bind(labelName), expr)

where the `Bind` nodes holds the definition of the label symbol.
That symbol is a term symbol with the flag `Label` (but not
`Method`, unlike symbols for label-defs) and whose `info` is the
result type `T` of the labeled block.

We use those new `Labeled` blocks in `PatternMatcher`, instead of
label-defs. This is the first step towards completely removing
label-defs from the compiler.

This commit structurally fixes a few issues:

* It fixes scala#1313 through the `mergeTests` optimization.
* It fixes scala#4563 because Labeled blocks are erasure-friendly.
* It does a big step towards fixing the upstream test t10387: the
  compiler can get to the back-end on that test, but it produces
  too much bytecode for a single JVM method. We do add a sister
  test t10387b which works because optimizations can kick in.
sjrd added a commit to sjrd/dotty that referenced this issue Aug 27, 2018
A Labeled block is an expression tree of the form

  label[T]: {
    expr
  }

where `expr` must conform to the type `T`. In addition, within
`expr` (but nowhere else), return from the label is allowed:

  return[label] e

where `e` must conform to the type `T` as well.

If execution of `expr` completes normally (rather than throwing an
exception or returning, etc.), then the result of evaluating the
`Labeled` block is the result of `expr`. If a `return[label] e` is
reached, the execution of `expr` is interrupted, and the result of
evaluating the `Labeled` block is the result of evaluating the
argument `e`.

Implementation-wise, a `Labeled` block is represented as a `Tree`
with the shape:

  Labeled(Bind(labelName), expr)

where the `Bind` nodes holds the definition of the label symbol.
That symbol is a term symbol with the flag `Label` (but not
`Method`, unlike symbols for label-defs) and whose `info` is the
result type `T` of the labeled block.

We use those new `Labeled` blocks in `PatternMatcher`, instead of
label-defs. This is the first step towards completely removing
label-defs from the compiler.

This commit structurally fixes a few issues:

* It fixes scala#1313 through the `mergeTests` optimization.
* It fixes scala#4563 because Labeled blocks are erasure-friendly.
* It does a big step towards fixing the upstream test t10387: the
  compiler can get to the back-end on that test, but it produces
  too much bytecode for a single JVM method. We do add a sister
  test t10387b which works because optimizations can kick in.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants