POC: Make ensuring inline

[mbovel]

No description provided.

[mbovel]

This PR makes ensuring inline:

extension [A](x: A)
  @library inline def ensuring(@ghost inline cond: A => Boolean, inline msg: String = ""): A = x

Therefore when compiling:

def f(x: Int): Int = {
 require(x >= 0)
 val res = if x == Integer.MAX_VALUE then x else x + 1
 res
}.ensuring(_ > 0)

After inlining we get:

def f(x: Int): Int = {
 val x$1: Int = {
   require(x.>=(0))
   val res: Int = if x.==(Integer.MAX_VALUE) then x else x.+(1)
   res:Int
 }
 x$1:Int
}

Note how the x argument to ensuring is lifted to a val x$1. A challenge is to "unlift" it. That's what I am trying to do in ExInlinedCall.

From my understanding, val x$1 is an inline argument proxy, and is generated in Dotty's Inliner.paramBindingDef.

I would therefore expect InlineProxy flag to be set on val x$1: https://github.com/scala/scala3/blob/20e6f11f4fe47982259eba949eea78d65765142f/compiler/src/dotty/tools/dotc/inlines/Inliner.scala#L224. But it is always false for some reasons, even at phase inlining (core.Contexts.atPhase(dottyCtx.base.inliningPhase)). I don't understand why. In the meantime, I just used the Synthetic flag instead; this work but is an over-approximation.

[mbovel]

7224d8c partially fixes extraction of nested inlined ensuring, such that:

import stainless.lang.StaticChecks.*

case class FileInputStream() {
  def tryReadByte(isOpen: Boolean): Int = {
    require(isOpen)
    def impl(): Int = {
      require(isOpen)
      0
    }.ensuring(_ => isOpen)
    impl()
  }.ensuring(_ => isOpen)
}

is extracted to:

case class FileInputStream {
  @method(FileInputStream)
  def tryReadByte(isOpen: Boolean): Int = {
    require(@ghost isOpen)
    @final
    def impl: Int = {
      require(@ghost isOpen)
      0
    }.ensuring {
      (_$1: Int) => @ghost isOpen
    }
    impl
  }.ensuring {
    (_$2: Int) => @ghost isOpen
  }
}

[mbovel]

I found that Inlined.call is frozen in time: https://github.com/scala/scala3/blob/7573951106ceeee2d5bb532cff2cf9b657e23635/compiler/src/dotty/tools/dotc/ast/Trees.scala#L1570-L1571. The tree of the call is preserved, but never processed by tree maps. This is a problem: we can't use it like a normal tree.

[mbovel]

After discussing with @samuelchassot, I think a better approach than trying to "de-inline" calls to StaticChecks methods could be to not inline them in the first place when running Stainless. I think this could be done easily by adding a Dotty phase in the Stainless pipeline that would remove inline modifiers on certain methods.