Code explosion in mergeCalls

[jad-hamza]

cc: @samuelchassot

We found an example where the code simplification becomes very slow, probably due to a code explosion in mergeCalls:

// before mergeFunctions: 339 lines of code
// after liftCalls: 649 lines of code
// after mergeCalls: 30341 lines of code

Can be reproduced with the Stainless code below and the command:

stainless --watch File.scala --debug=solver,verification --functions=problem

Stainless code

import stainless.annotation._
import stainless.collection._
import stainless.equations._
import stainless.lang._
import stainless.proof.check
import scala.annotation.tailrec
import scala.collection.immutable

object MutableLongMap {

  private final val IndexMask: Int = 0x07ffffff // = Integer.MAX_VALUE/8
  private final val MissingBit = 0x80000000
  private final val VacantBit = 0x40000000
  private final val MissVacant = 0xc0000000
  private final val EntryNotFound = 0x20000000
  private final val MAX_ITER = 2048 // arbitrary

  @mutable
  case class LongMapLongV(
      var mask: Int = IndexMask,
      var extraKeys: Int = 0,
      var zeroValue: Long = 0,
      var minValue: Long = 0,
      var _size: Int = 0,
      var _keys: Array[Long] = Array.fill(IndexMask + 1)(0),
      var _values: Array[Long] = Array.fill(IndexMask + 1)(0),
      val defaultEntry: Long => Long = (x => 0),
      var repackingKeyCount: Int = 0
  ) {

    @inline
    def valid: Boolean = {
      mask == IndexMask &&
      _values.length == mask + 1 &&
      _keys.length == _values.length &&
      mask >= 0 &&
      _size >= 0 &&
      _size < mask + 1 &&
      size >= _size &&
      extraKeys >= 0 &&
      extraKeys <= 3 &&
      arrayCountValidKeysTailRec(_keys, 0, _keys.length) == _size

    }

    @inline
    def inRange(i: Int): Boolean = {
      i >= 0 && i < mask + 1
    }

    @inline
    def validKeyIndex(k: Long, i: Int): Boolean = {
      require(valid)
      if (inRange(i)) _keys(i) == k else false
    }

    @inline
    def validZeroKeyIndex(i: Int): Boolean = {
      require(valid && inRange(i))
      inRange(i) && _keys(i) == 0
    }

    def size: Int = {
      _size + (extraKeys + 1) / 2
    }

    def isEmpty: Boolean = {
      require(valid)
      _size == 0
    }.ensuring(_ => valid)

    private def toIndex(k: Long): Int = {
      require(valid)
      val h = ((k ^ (k >>> 32)) & 0xffffffffL).toInt
      val x = (h ^ (h >>> 16)) * 0x85ebca6b
      (x ^ (x >>> 13)) & mask
    }.ensuring(res => valid && res < _keys.length)

    @inline
    def getCurrentListMap(from: Int): ListMapLongKey[Long] = {
      require(valid && from >= 0 && from <= _keys.length)

      val res = if ((extraKeys & 1) != 0 && (extraKeys & 2) != 0) {
        (getCurrentListMapNoExtraKeys(from) + (0L, zeroValue)) + (Long.MinValue, minValue)
      } else if ((extraKeys & 1) != 0 && (extraKeys & 2) == 0) {
        getCurrentListMapNoExtraKeys(from) + (0L, zeroValue)
      } else if ((extraKeys & 2) != 0 && (extraKeys & 1) == 0) {
        getCurrentListMapNoExtraKeys(from) + (Long.MinValue, minValue)
      } else {
        getCurrentListMapNoExtraKeys(from)
      }
      if (from < _keys.length && validKeyInArray(_keys(from))) {
        ListMapLongKeyLemmas.addStillContains(getCurrentListMapNoExtraKeys(from), 0, zeroValue, _keys(from))
        ListMapLongKeyLemmas.addStillContains(getCurrentListMapNoExtraKeys(from), Long.MinValue, minValue, _keys(from))
        ListMapLongKeyLemmas.addApplyDifferent(getCurrentListMapNoExtraKeys(from), 0, zeroValue, _keys(from))
        ListMapLongKeyLemmas.addApplyDifferent(getCurrentListMapNoExtraKeys(from), Long.MinValue, minValue, _keys(from))
      }

      res

    }.ensuring(res =>
      valid &&
        (if (from < _keys.length && validKeyInArray(_keys(from))) res.contains(_keys(from)) && res(_keys(from)) == _values(from) else true) &&
        (if ((extraKeys & 1) != 0) res.contains(0) && res(0) == zeroValue else !res.contains(0)) &&
        (if ((extraKeys & 2) != 0) res.contains(Long.MinValue) && res(Long.MinValue) == minValue else !res.contains(Long.MinValue))
    )

    def getCurrentListMapNoExtraKeys(from: Int): ListMapLongKey[Long] = {
      require(valid && from >= 0 && from <= _keys.length)
      decreases(_keys.length + 1 -from)
      if (from >= _keys.length) {
        ListMapLongKey.empty[Long]
      } else if (validKeyInArray(_keys(from))) {
        ListMapLongKeyLemmas.addStillNotContains(getCurrentListMapNoExtraKeys(from + 1), _keys(from), _values(from), 0)

        getCurrentListMapNoExtraKeys(from + 1) + (_keys(from), _values(from))
      } else {
        getCurrentListMapNoExtraKeys(from + 1)
      }
    }.ensuring(res => valid &&
      !res.contains(0) && !res.contains(Long.MinValue) &&
        (if (from < _keys.length && validKeyInArray(_keys(from)))
           res.contains(_keys(from)) && res(_keys(from)) == _values(from)
         else if (from < _keys.length) res == getCurrentListMapNoExtraKeys(from + 1)
         else res.isEmpty)
    )

    @pure
    def problem(): Unit = {
      require(valid)
      val from = 0
      val res = getCurrentListMap(from)
    }.ensuring(_ => valid && (if ((extraKeys & 1) != 0) getCurrentListMap(0).contains(0) else !getCurrentListMap(0).contains(0)))

  }

  @extern
  def assume(b: Boolean): Unit = {}.ensuring(_ => b)

  @inline
  def validKeyInArray(l: Long): Boolean = {
    l != 0 && l != Long.MinValue
  }

  @tailrec
  @pure
  def arrayCountValidKeysTailRec(
      a: Array[Long],
      from: Int,
      to: Int
  ): Int = {
    require(
      from <= to && from >= 0 && to <= a.length && a.length < Integer.MAX_VALUE
    )
    decreases(a.length-from)
    if (from >= to) {
      0
    } else {
      if (validKeyInArray(a(from))) {
        1 + arrayCountValidKeysTailRec(a, from + 1, to)
      } else {
        arrayCountValidKeysTailRec(a, from + 1, to)
      }
    }
  }.ensuring(res => res >= 0 && res <= a.length - from)


}

case class ListMapLongKey[B](toList: List[(Long, B)]) {
  require(TupleListOps.isStrictlySorted(toList))

  @inline
  def isEmpty: Boolean = toList.isEmpty
  @inline
  def head: (Long, B) = {
    require(!isEmpty)
    toList.head
  }
  @inline
  def tail: ListMapLongKey[B] = {
    require(!isEmpty)
    ListMapLongKey(toList.tail)
  }

  @inlineOnce @extern
  def contains(key: Long): Boolean = {
    TupleListOps.containsKey(toList, key)

  }.ensuring(res => !res || this.get(key).isDefined)

  @inline
  def get(key: Long): Option[B] = {
    TupleListOps.getValueByKey(toList, key)
  }
  @inline
  def keysOf(value: B): List[Long] = {
    TupleListOps.getKeysOf(toList, value)
  }
  @inline
  def apply(key: Long): B = {
    require(contains(key))
    get(key).get
  }

  @inline
  def +(keyValue: (Long, B)): ListMapLongKey[B] = {

    val newList = TupleListOps.insertStrictlySorted(toList, keyValue._1, keyValue._2)

    ListMapLongKey(newList)

  }.ensuring(res => res.contains(keyValue._1) && res.get(keyValue._1) == Some(keyValue._2))

  // @inlineOnce
  def ++(keyValues: List[(Long, B)]): ListMapLongKey[B] = {
    decreases(keyValues)
    keyValues match {
      case Nil()                => this
      case Cons(keyValue, rest) => (this + keyValue) ++ rest
    }
  }
  // @inlineOnce
  def -(key: Long): ListMapLongKey[B] = {
    ListMapLongKey(TupleListOps.removeStrictlySorted(toList, key))
  }.ensuring(res => !res.contains(key))

  // @inlineOnce
  def --(keys: List[Long]): ListMapLongKey[B] = {
    decreases(keys)
    keys match {
    case Nil()           => this
    case Cons(key, rest) => (this - key) -- rest
  }
  }
  @inline
  def forall(p: ((Long, B)) => Boolean): Boolean = {
    toList.forall(p)
  }
}

object TupleListOps {

  @inline
  def invariantList[B](l: List[(Long, B)]): Boolean = {
    isStrictlySorted(l)
  }

  @extern
  def getKeysOf[B](l: List[(Long, B)], value: B): List[Long] = {
    require(invariantList(l))
    decreases(l)

    l match {
      case head :: tl if (head._2 == value) => {
        head._1 :: getKeysOf(tl, value)
      }
      case head :: tl if (head._2 != value) => {
        val r = getKeysOf(tl, value)
        getKeysOf(tl, value)
      }
      case Nil() => Nil[Long]()
    }

  }.ensuring(res => res.forall(getValueByKey(l, _) == Some(value)))

  def getValueByKey[B](l: List[(Long, B)], key: Long): Option[B] = {
    require(invariantList(l))
    decreases(l)

    l match {
      case head :: tl if (head._1 == key) => Some(head._2)
      case head :: tl if (head._1 != key) => getValueByKey(tl, key)
      case Nil()                          => None[B]
    }

  }

  def insertStrictlySorted[B](l: List[(Long, B)], newKey: Long, newValue: B): List[(Long, B)] = {
    require(invariantList(l))
    decreases(l)

    l match {
      case head :: tl if (head._1 < newKey)  => head :: insertStrictlySorted(tl, newKey, newValue)
      case head :: tl if (head._1 == newKey) => (newKey, newValue) :: tl
      case head :: tl if (head._1 > newKey)  => (newKey, newValue) :: head :: tl
      case Nil()                             => (newKey, newValue) :: Nil()
    }
  }.ensuring(res => invariantList(res) && containsKey(res, newKey) && res.contains((newKey, newValue)))

  def removeStrictlySorted[B](l: List[(Long, B)], key: Long): List[(Long, B)] = {
    require(invariantList(l))
    decreases(l)

    l match {
      case head :: tl if (head._1 == key) => tl
      case head :: tl if (head._1 != key) => head :: removeStrictlySorted(tl, key)
      case Nil()                          => Nil[(Long, B)]()
    }
  }.ensuring(res => invariantList(res) && !containsKey(res, key))


  def isStrictlySorted[B](l: List[(Long, B)]): Boolean = {
    decreases(l)
    l match {
      case Nil()                                     => true
      case Cons(_, Nil())                            => true
      case Cons(h1, Cons(h2, _)) if (h1._1 >= h2._1) => false
      case Cons(_, t)                                => isStrictlySorted(t)
    }
  }

  def containsKey[B](l: List[(Long, B)], key: Long): Boolean = {
    require(invariantList(l))
    decreases(l)
    l match {
      case head :: tl if(head._1 == key) => true
      case head :: tl if(head._1 > key) => false
      case head :: tl if(head._1 < key) => containsKey(tl, key)
      case Nil() => false

    }
  }
}

object ListMapLongKey {
  def empty[B]: ListMapLongKey[B] = ListMapLongKey[B](List.empty[(Long, B)])
}

object ListMapLongKeyLemmas {
  import ListSpecs._

  @opaque
  def addValidProp[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, a: Long, b: B): Unit = {
    require(lm.forall(p) && p(a, b))
    decreases(lm.toList.size)

    if (!lm.isEmpty)
      addValidProp(lm.tail, p, a, b)

  }.ensuring { _ =>
    val nlm = lm + (a, b)
    nlm.forall(p)
  }

  @opaque
  def removeValidProp[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, a: Long): Unit = {
    require(lm.forall(p))
    decreases(lm.toList.size)
    if (!lm.isEmpty)
      removeValidProp(lm.tail, p, a)

  }.ensuring { _ =>
    val nlm = lm - a
    nlm.forall(p)
  }

  @opaque
  def insertAllValidProp[B](lm: ListMapLongKey[B], kvs: List[(Long, B)], p: ((Long, B)) => Boolean): Unit = {
    require(lm.forall(p) && kvs.forall(p))
    decreases(kvs)

    if (!kvs.isEmpty) {
      addValidProp(lm, p, kvs.head._1, kvs.head._2)
      insertAllValidProp(lm + kvs.head, kvs.tail, p)
    }

  }.ensuring { _ =>
    val nlm = lm ++ kvs
    nlm.forall(p)
  }

  @opaque
  def removeAllValidProp[B](lm: ListMapLongKey[B], l: List[Long], p: ((Long, B)) => Boolean): Unit = {
    require(lm.forall(p))
    decreases(l)

    if (!l.isEmpty) {
      removeValidProp(lm, p, l.head)
      removeAllValidProp(lm - l.head, l.tail, p)
    }

  }.ensuring { _ =>
    val nlm = lm -- l
    nlm.forall(p)
  }

  @opaque @extern
  def addApplyDifferent[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
    require(lm.contains(a0) && a0 != a)

  }.ensuring(_ => (lm + (a -> b))(a0) == lm(a0))

  @opaque @extern
  def addStillContains[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
    require(lm.contains(a0))

  }.ensuring(_ => (lm + (a, b)).contains(a0))

  @opaque @extern
  def addStillNotContains[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
    require(!lm.contains(a0) && a != a0)

  }.ensuring(_ => !(lm + (a, b)).contains(a0))

  @opaque
  def applyForall[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, k: Long): Unit = {
    require(lm.forall(p) && lm.contains(k))
    decreases(lm.toList.size)

    if (!lm.isEmpty && lm.toList.head._1 != k)
      applyForall(lm.tail, p, k)

  }.ensuring(_ => p(k, lm(k)))

  @opaque
  def getForall[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, k: Long): Unit = {
    require(lm.forall(p))
    decreases(lm.toList.size)

    if (!lm.isEmpty && lm.toList.head._1 != k)
      getForall(lm.tail, p, k)

  }.ensuring(_ => lm.get(k).forall(v => p(k, v)))

  @opaque
  def uniqueImage[B](lm: ListMapLongKey[B], a: Long, b: B): Unit = {
    require(lm.toList.contains((a, b)))

  }.ensuring(_ => lm.get(a) == Some[B](b))

  @opaque
  def keysOfSound[B](lm: ListMapLongKey[B], value: B): Unit = {
  }.ensuring(_ => lm.keysOf(value).forall(key => lm.get(key) == Some[B](value)))
}

Expression before mergeFunctions

¬(thiss.mask ≠ IndexMask || thiss._values.size ≠ thiss.mask + 1 || thiss._keys.size ≠ thiss._values.size || thiss.mask < 0 || thiss._size < 0 || thiss._size >= thiss.mask + 1 || size(thiss) < thiss._size || thiss.extraKeys < 0 || thiss.extraKeys > 3 || arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) ≠ thiss._size || from ≠ 0 || res ≠ {
  val cond: Boolean = (thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0) && from <= thiss._keys.size
  val res: ListMapLongKey[Long] = {
    val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) ≠ 0) {
      val inlined: ListMapLongKey[Long] = {
        val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
        assume({
          val res: Boolean = choose((empty$140: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
          res
        } && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
        ListMapLongKey[Long](newList)
      }
      val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
      assume({
        val res: Boolean = choose((empty$141: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
        res
      } && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
      res
    } else if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) == 0) {
      val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
      val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
      assume({
        val res: Boolean = choose((empty$142: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
        res
      } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
      res
    } else if ((thiss.extraKeys & 2) ≠ 0 && (thiss.extraKeys & 1) == 0) {
      val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
      val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
      assume({
        val res: Boolean = choose((empty$143: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
        res
      } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
      res
    } else {
      getCurrentListMapNoExtraKeys(thiss, from)
    }
    val t: Unit = if (from < thiss._keys.size && {
      val l: Long = thiss._keys.arr(from)
      l ≠ 0.toLong && l ≠ -9223372036854775808
    }) {
      val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
      val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
      val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
      addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
    } else {
      ()
    }
    t
  }
  assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
    val l: Long = thiss._keys.arr(from)
    l ≠ 0.toLong && l ≠ -9223372036854775808
  }) || {
    val res: Boolean = choose((empty$144: Boolean) => true)
    assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
    res
  } && {
    val key: Long = thiss._keys.arr(from)
    val cond: Boolean = {
      val res: Boolean = choose((empty$145: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
      res
    }
    get[Long](getValueByKey[Long](res.toList, key))
  } == thiss._values.arr(from))) && (if ((thiss.extraKeys & 1) ≠ 0) {
    {
      val res: Boolean = choose((empty$146: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
      res
    } && {
      val key: Long = 0
      val cond: Boolean = {
        val res: Boolean = choose((empty$147: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss.zeroValue
  } else {
    val res: Boolean = choose((empty$148: Boolean) => true)
    ¬{
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
      res
    }
  })) && (if ((thiss.extraKeys & 2) ≠ 0) {
    {
      val res: Boolean = choose((empty$149: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
      res
    } && {
      val key: Long = -9223372036854775808
      val cond: Boolean = {
        val res: Boolean = choose((empty$150: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss.minValue
  } else {
    val res: Boolean = choose((empty$151: Boolean) => true)
    ¬{
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
      res
    }
  }))
  res
} || x$2 ≠ () || thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (if ((thiss.extraKeys & 1) ≠ 0) {
  val from: Int = 0
  val inlined: ListMapLongKey[Long] = {
    val t: Boolean = thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0
    val res: ListMapLongKey[Long] = {
      val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 2) ≠ 0) {
        val inlined: ListMapLongKey[Long] = {
          val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
          assume({
            val res: Boolean = choose((empty$152: Boolean) => true)
            assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
            res
          } && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
          ListMapLongKey[Long](newList)
        }
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
        assume({
          val res: Boolean = choose((empty$153: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
        res
      } else if ((thiss.extraKeys & 2) == 0) {
        val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
        assume({
          val res: Boolean = choose((empty$154: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
        res
      } else if (false) {
        val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
        assume({
          val res: Boolean = choose((empty$155: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
        res
      } else {
        getCurrentListMapNoExtraKeys(thiss, from)
      }
      val t: Unit = if (from < thiss._keys.size && {
        val l: Long = thiss._keys.arr(from)
        l ≠ 0.toLong && l ≠ -9223372036854775808
      }) {
        val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
        val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
        val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
        addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
      } else {
        ()
      }
      t
    }
    assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
      val l: Long = thiss._keys.arr(from)
      l ≠ 0.toLong && l ≠ -9223372036854775808
    }) || {
      val res: Boolean = choose((empty$156: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
      res
    } && {
      val key: Long = thiss._keys.arr(from)
      val cond: Boolean = {
        val res: Boolean = choose((empty$157: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss._values.arr(from))) && {
      val res: Boolean = choose((empty$158: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
      res
    } && {
      val key: Long = 0
      val cond: Boolean = {
        val res: Boolean = choose((empty$159: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss.zeroValue) && (if ((thiss.extraKeys & 2) ≠ 0) {
      {
        val res: Boolean = choose((empty$160: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
        res
      } && {
        val key: Long = -9223372036854775808
        val cond: Boolean = {
          val res: Boolean = choose((empty$161: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
          res
        }
        get[Long](getValueByKey[Long](res.toList, key))
      } == thiss.minValue
    } else {
      val res: Boolean = choose((empty$162: Boolean) => true)
      ¬{
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
        res
      }
    }))
    res
  }
  val res: Boolean = choose((empty$163: Boolean) => true)
  assume(¬res || isDefined[Long](getValueByKey[Long](inlined.toList, 0)))
  res
} else {
  val from: Int = 0
  val inlined: ListMapLongKey[Long] = {
    val t: Boolean = thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0
    val res: ListMapLongKey[Long] = {
      val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) ≠ 0) {
        val inlined: ListMapLongKey[Long] = {
          val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
          assume({
            val res: Boolean = choose((empty$164: Boolean) => true)
            assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
            res
          } && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
          ListMapLongKey[Long](newList)
        }
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
        assume({
          val res: Boolean = choose((empty$165: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
        res
      } else if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) == 0) {
        val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
        assume({
          val res: Boolean = choose((empty$166: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
        res
      } else if ((thiss.extraKeys & 2) ≠ 0 && (thiss.extraKeys & 1) == 0) {
        val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
        assume({
          val res: Boolean = choose((empty$167: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
        res
      } else {
        getCurrentListMapNoExtraKeys(thiss, from)
      }
      val t: Unit = if (from < thiss._keys.size && {
        val l: Long = thiss._keys.arr(from)
        l ≠ 0.toLong && l ≠ -9223372036854775808
      }) {
        val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
        val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
        val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
        addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
      } else {
        ()
      }
      t
    }
    assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
      val l: Long = thiss._keys.arr(from)
      l ≠ 0.toLong && l ≠ -9223372036854775808
    }) || {
      val res: Boolean = choose((empty$168: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
      res
    } && {
      val key: Long = thiss._keys.arr(from)
      val cond: Boolean = {
        val res: Boolean = choose((empty$169: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss._values.arr(from))) && (if ((thiss.extraKeys & 1) ≠ 0) {
      {
        val res: Boolean = choose((empty$170: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
        res
      } && {
        val key: Long = 0
        val cond: Boolean = {
          val res: Boolean = choose((empty$171: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
          res
        }
        get[Long](getValueByKey[Long](res.toList, key))
      } == thiss.zeroValue
    } else {
      val res: Boolean = choose((empty$172: Boolean) => true)
      ¬{
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
        res
      }
    })) && (if ((thiss.extraKeys & 2) ≠ 0) {
      {
        val res: Boolean = choose((empty$173: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
        res
      } && {
        val key: Long = -9223372036854775808
        val cond: Boolean = {
          val res: Boolean = choose((empty$174: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
          res
        }
        get[Long](getValueByKey[Long](res.toList, key))
      } == thiss.minValue
    } else {
      val res: Boolean = choose((empty$175: Boolean) => true)
      ¬{
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
        res
      }
    }))
    res
  }
  val res: Boolean = choose((empty$176: Boolean) => true)
  ¬{
    assume(¬res || isDefined[Long](getValueByKey[Long](inlined.toList, 0)))
    res
  }
}))

[samarion]

I mentioned this at some point (maybe to @gsps ?): we should be able to move the mergeCalls logic into the template generator which would make it much cleaner.

The idea is to change the IfExpr case in TemplateGenerator.mkExprClauses. We would change the following lines to call mkExprClauses recursively and then unify function calls which occur in both branches:

inox/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala

Lines 370 to 371 in 22de8d6

	val trec = rec(newBool1, thenn, pol)
	val erec = rec(newBool2, elze, pol)

would become

val (trec, tClauses) = mkExprClauses(newBool1, thenn, localSubst, pol)
val (erec, eClauses) = mkExprClauses(newBool2, elze, localSubst, pol)
builder ++= mergeCalls(pathVar, localSubst, tClauses, eClauses)

The new mergeCalls logic (inside TemplateGenerator.scala) would look something like this:

def mergeCalls(pathVar: Variable, condVar: Variable, substMap: Map[Variable, Encoded],
               thenClauses: TemplateClauses, elseClauses: TemplateClauses): TemplateClauses = {
  val builder = new Builder(pathVar, substMap)
  builder ++= thenClauses
  builder ++ elseClauses

  // Clear all guardedExprs in builder since we're going to transform them by merging calls.
  // The transformed guardedExprs will be added to builder at the end of the function.
  builder.guardedExprs = Map.empty

  def collectCalls(expr: Expr): Set[FunctionInvocation] =
    exprOps.collect { case fi: FunctionInvocation => Set(fi) case _ => Set.empty[FunctionInvocation] }(expr)
  def countCalls(expr: Expr): Int =
    exprOps.count { case fi: FunctionInvocation => 1 case _ => 0}(expr)
  def replaceCall(call: FunctionInvocation, newExpr: Expr)(e: Expr): Expr =
    exprOps.replace(Map(call, newExpr), e)

  def getCalls(guardedExprs: Map[Variable, Seq[Expr]]): Map[TypedFunDef, Seq[(FunctionInvocation, Set[Variable])]] =
    (for {(b, es) <- guardedExprs; e <- es; fi <- collectCalls(e)) yield (b -> fi))
    .groupBy(_._2)
    .mapValues(_.map(_._1).toSet)
    .toSeq
    .groupBy(_._1.tfd)
    .mapValues(_.toList.distinct.sortBy(p => countCalls(p._1)))  // place inner calls first
    .toMap

  var thenGuarded = thenClauses._4
  var elseGuarded = elseClauses._4

  val thenCalls = getCalls(thenGuarded)
  val elseCalls = getCalls(elseGuarded)

  // We sort common function calls in order to merge nested calls first.
  var toMerge = (thenCalls.keys() & elseCalls.keys())
    .flatMap(tfd => thenCalls(tfd) zip elseCalls(tfd))
    .toSeq
    .sortBy(p => countCalls(p._1._1) + countCalls(p._2._1))

  while (toMerge.nonEmpty) {
    val ((thenCall, thenBlockers), (elseCall, elseBlockers)) = toMerge.head
    toMerge = toMerge.tail

    val newExpr: Variable = Variable.fresh("call", thenCall.tfd.getType, true)
    builder.storeExpr(newExpr)

    val replaceThen = replaceCall(thenCall, newExpr) _
    val replaceElse = replaceCall(elseCall, newExpr) _

    thenGuarded = thenGuarded.mapValues(_.map(replaceThen)
    elseGuarded = elseGuarded.mapValues(_.map(replaceElse)
    toMerge = toMerge.map(p => (replaceThen(p._1), replaceElse(p._2))

    val newBlocker: Variable = Variable.fresh("bm", BooleanType(), true)
    // TODO: make this a method in Builder similar to storeCond
    builder.storeConds(thenBlockers ++ elseBlockers, newBlocker)
    builder.iff(orJoin((thenBlockers ++ elseBlockers).toSeq), newBlocker)

    val newArgs = (thenCall.args zip elseCall.args).map { case (thenArg, elseArg) =>
      val (newArg, argClauses) = mkExprClauses(newBlocker, IfExpr(condVar, thenArg, elseArg), builder.localSubst)
      builder ++= argClauses
      newArg
    }

    val newCall = thenCall.tfd.applied(newArgs)
    builder.storeGuarded(newBlocker, Equals(newExpr, newCall))
  }

  for ((b, es) <- thenGuarded; e <- es) builder.storeGuarded(b, e)
  for ((b, es) <- elseGuarded; e <- es) builder.storeGuarded(b, e)
  builder.result
}

[jad-hamza]

Should liftCalls remain?

[samarion]

No, I think it shouldn't be necessary.