Infinite loop in InnerClasses

[jad-hamza]

I'm getting an infinite loop on this example during phase InnerClasses. @romac Maybe you know why?

stainless -XX:MaxJavaStackTraceDepth=1000000 File.scala --debug=trees,stack --batched

object Main {

  def twoOrders() = {
    val order1 = new TotalOrder[Int] {
      override def leq(x: Int, y: Int): Boolean = x <= y
    }
    val order2 = new TotalOrder[Short] {
      override def leq(x: Short, y: Short): Boolean = x <= y
    }
  }
}

trait TotalOrder[A] {
  def leq(x: A, y: A): Boolean
}

The symbols are:

[ Debug  ] Symbols before InnerClasses
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] @abstract
[ Debug  ] @method(TotalOrder)
[ Debug  ] def leq(x: A, y: A): Boolean = <empty tree>[Boolean]
[ Debug  ] 
[ Debug  ] def twoOrders: Unit = {
[ Debug  ]   val order1: TotalOrder[Int] = {
[ Debug  ]     case class $anon extends TotalOrder[Int] {
[ Debug  ]       
[ Debug  ]     
[ Debug  ]       @method($anon)
[ Debug  ]       def leq(x: Int, y: Int): Boolean = x <= y
[ Debug  ]     }
[ Debug  ]     $anon()
[ Debug  ]   }
[ Debug  ]   val order2: TotalOrder[Short] = {
[ Debug  ]     case class $anon extends TotalOrder[Short] {
[ Debug  ]       
[ Debug  ]     
[ Debug  ]       @method($anon)
[ Debug  ]       def leq(x: Short, y: Short): Boolean = x.toInt <= y.toInt
[ Debug  ]     }
[ Debug  ]     $anon()
[ Debug  ]   }
[ Debug  ]   ()
[ Debug  ] }
[ Debug  ] 
[ Debug  ] -------------Classes-------------
[ Debug  ] @abstract
[ Debug  ] abstract class TotalOrder[A]

And the loop happens when calling preMap: https://github.com/epfl-lara/stainless/blob/58d12a902aa90df7d4595995963535c6e13f71de/core/src/main/scala/stainless/extraction/innerclasses/InnerClasses.scala#L406

The loop is in rec in Inox (loops on this): https://github.com/epfl-lara/inox/blob/93503b1f7cffd68ae44483cdc2170cafba38eaa4/src/main/scala/inox/ast/GenTreeOps.scala#L284

// premap
val order1: TotalOrder[Int] = {
  case class $anon extends TotalOrder[Int] {

    @method($anon)
    def leq(x: Int, y: Int): Boolean = x <= y
  }
  $anon()
}
true

// rec
val order1: TotalOrder[Int] = {
  case class $anon extends TotalOrder[Int] {

    @method($anon)
    def leq(x: Int, y: Int): Boolean = x <= y
  }
  $anon()
}
true

// rec
case class $anon extends TotalOrder[Int] {

  @method($anon)
  def leq(x: Int, y: Int): Boolean = x <= y
}
$anon()

// rec
$anon()

// rec
this

// rec
this

// rec
this

// rec
this
[...] // continues with this

[jad-hamza]

More debugging:

• The tree on which rec loops is: this[$anon] (of class stainless.extraction.methods.Trees$This)
• The function given to preMap https://github.com/epfl-lara/stainless/blob/58d12a902aa90df7d4595995963535c6e13f71de/core/src/main/scala/stainless/extraction/innerclasses/InnerClasses.scala#L415 returns Some(this[$anon].outer$anon)
• So newV on https://github.com/epfl-lara/inox/blob/93503b1f7cffd68ae44483cdc2170cafba38eaa4/src/main/scala/inox/ast/GenTreeOps.scala#L286 is equal to this[$anon].outer$anon
• We then deconstruct newV, one of the children is this[$anon] and we recurse on that expression on line https://github.com/epfl-lara/inox/blob/93503b1f7cffd68ae44483cdc2170cafba38eaa4/src/main/scala/inox/ast/GenTreeOps.scala#L302

The comments suggest that preMap shouldn't diverge when applyRec is false https://github.com/epfl-lara/inox/blob/93503b1f7cffd68ae44483cdc2170cafba38eaa4/src/main/scala/inox/ast/GenTreeOps.scala#L150

[samarion]

Hmm, that comment isn't accurate. preMap can diverge if the output wraps the input (as in your example).

Maybe we should be using postMap?

[romac]

Maybe we should be using postMap?

That's what I would try as well. I am not sure why we even use preMap here.

[jad-hamza]

Thanks to both for having a look! I switched to postMap and the loop is gone :)

But, for the same example, there is another loop:

The trees with unique identifiers before entering the phase:

[ Debug  ] Symbols before PartialFunctions
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] @abstract
[ Debug  ] @method(TotalOrder$0)
[ Debug  ] def leq$2(x$130: A$117, y$31: A$117): Boolean = <empty tree>[Boolean]
[ Debug  ] 
[ Debug  ] def twoOrders$0: Unit = {
[ Debug  ]   val order1$1: TotalOrder$0[Int] = {
[ Debug  ]     case class $anon$0 extends TotalOrder$0[Int] {
[ Debug  ]       @method($anon$0)
[ Debug  ]       def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
[ Debug  ]     }
[ Debug  ]     $anon$0()
[ Debug  ]   }
[ Debug  ]   val order2$1: TotalOrder$0[Short] = {
[ Debug  ]     case class $anon$1 extends TotalOrder$0[Short] {
[ Debug  ]       @method($anon$1)
[ Debug  ]       def leq$1(x$129: Short, y$30: Short): Boolean = x$129.toInt <= y$30.toInt
[ Debug  ]     }
[ Debug  ]     $anon$1()
[ Debug  ]   }
[ Debug  ]   ()
[ Debug  ] }

The loop goes through transform(e: Expr, ctx: Context) and through the call to transform(fd: FunDef, ctx: Context) on a method of subst.methods (https://github.com/epfl-lara/stainless/blob/f6ecb80598ef0e077aeaae02929ce0523ccc7dc4/core/src/main/scala/stainless/extraction/innerclasses/InnerClasses.scala#L249)

There are methods with an id of the form inv$n being created indefinitely for $anon$0 (and they contain $anon$0 inside):

// transform
val order2$1: TotalOrder$0[Short] = {
  case class $anon$1 extends TotalOrder$0[Short] {
    @method($anon$1)
    def leq$1(x$129: Short, y$30: Short): Boolean = x$129.toInt <= y$30.toInt
  }
  $anon$1()
}
()

// transform
case class $anon$1 extends TotalOrder$0[Short] {
  @method($anon$1)
  def leq$1(x$129: Short, y$30: Short): Boolean = x$129.toInt <= y$30.toInt
}
$anon$1()

// transform a method in subst.methods
@invariant
@method($anon$1)
def inv$7: Boolean = {
  val order1$1: TotalOrder$0[Int] = {
    case class $anon$0 extends TotalOrder$0[Int] {
      @method($anon$0)
      def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
    }
    $anon$0()
  }
  true
}

// transform
val order1$1: TotalOrder$0[Int] = {
  case class $anon$0 extends TotalOrder$0[Int] {
    @method($anon$0)
    def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
  }
  $anon$0()
}
true

// transform
case class $anon$0 extends TotalOrder$0[Int] {
  @method($anon$0)
  def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
}
$anon$0()

// transform a method in subst.methods
@invariant
@method($anon$0)
def inv$8: Boolean = {
  val order1$1: TotalOrder$0[Int] = {
    case class $anon$0 extends TotalOrder$0[Int] {
      @method($anon$0)
      def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
    }
    $anon$0(this[$anon$1])
  }
  true
}

// transform
val order1$1: TotalOrder$0[Int] = {
  case class $anon$0 extends TotalOrder$0[Int] {
    @method($anon$0)
    def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
  }
  $anon$0(this[$anon$1])
}
true

// transform
case class $anon$0 extends TotalOrder$0[Int] {
  @method($anon$0)
  def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
}
$anon$0(this[$anon$1])

// transform a method in subst.methods
@invariant
@method($anon$0)
def inv$9: Boolean = {
  val order1$1: TotalOrder$0[Int] = {
    case class $anon$0 extends TotalOrder$0[Int] {
      @method($anon$0)
      def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
    }
    $anon$0(this[$anon$0])
  }
  true
}

// transform
val order1$1: TotalOrder$0[Int] = {
  case class $anon$0 extends TotalOrder$0[Int] {
    @method($anon$0)
    def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
  }
  $anon$0(this[$anon$0])
}
true

// transform
case class $anon$0 extends TotalOrder$0[Int] {
  @method($anon$0)
  def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
}
$anon$0(this[$anon$0])

// transform a method in subst.methods
@invariant
@method($anon$0)
def inv$10: Boolean = {
  val order1$1: TotalOrder$0[Int] = {
    case class $anon$0 extends TotalOrder$0[Int] {
      @method($anon$0)
      def leq$0(x$128: Int, y$29: Int): Boolean = x$128 <= y$29
    }
    $anon$0(this[$anon$0])
  }
  true
}

// and so on