search

epfl-lara / inox

Solver for higher-order functional programs, used by Stainless
Apache License 2.0
88 stars 20 forks source link

Code explosion in mergeCalls #146

Closed jad-hamza closed 3 years ago

jad-hamza commented 3 years ago

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 ```scala 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 ```scala ¬(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 commented 3 years ago

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: https://github.com/epfl-lara/inox/blob/22de8d6b6af51fbe09bca2fc26dbdd596de8e3e8/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala#L370-L371 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 commented 3 years ago

Should liftCalls remain?

samarion commented 3 years ago

No, I think it shouldn't be necessary.