diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala index 4556f7dd6507f9a8c8a745b0323dbbdb9cf0032b..c7382d167ccbf411a0531b2bfce2377e0b829da2 100644 --- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala +++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala @@ -219,7 +219,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T], // id => expr && ... && expr var guardedExprs = Map[Identifier, Seq[Expr]]() def storeGuarded(guardVar: Identifier, expr: Expr) : Unit = { - assert(expr.getType == BooleanType, expr.asString(Program.empty)(LeonContext.empty) + " is not of type Boolean." + ( + assert(expr.getType == BooleanType, expr.asString(Program.empty)(LeonContext.empty) + " is not of type Boolean. " + ( purescala.ExprOps.fold[String]{ (e, se) => s"$e is of type ${e.getType}" + se.map(child => "\n " + "\n".r.replaceAllIn(child, "\n ")).mkString }(expr) diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala index ace5274c20158105c6dd5d2160c00ff9de83d776..9f05589f069fbb16c564aabf4bb6219f614c606e 100644 --- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala +++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala @@ -217,7 +217,7 @@ object AntiAliasingPhase extends TransformationPhase { if(duplicatedParams.nonEmpty) ctx.reporter.fatalError(fi.getPos, "Illegal passing of aliased parameter: " + duplicatedParams.head) - val freshRes = FreshIdentifier("res", nfd.returnType) + val freshRes = FreshIdentifier("res", nfd.typed(fd.tps).returnType) val extractResults = Block( modifiedArgs.zipWithIndex.map(p => Assignment(p._1.id, TupleSelect(freshRes.toVariable, p._2 + 2))), diff --git a/testcases/verification/xlang/FunctionCaching.scala b/testcases/verification/xlang/FunctionCaching.scala index 0a7c477a67d188790f765934aabddfc903ef957e..75c73e822831a5d7da9a209f1964d36e10298359 100644 --- a/testcases/verification/xlang/FunctionCaching.scala +++ b/testcases/verification/xlang/FunctionCaching.scala @@ -3,40 +3,38 @@ import leon.collection._ object FunctionCaching { - case class Cache() { - var cached: Map[BigInt, BigInt] = Map() - //contains the set of elements where cache has been used - var cacheHit: Set[BigInt] = Set() - } + case class CachedFun[A,B](fun: (A) => B, var cached: Map[A, B], var cacheHit: Set[A]) { - def cachedFun(f: (BigInt) => BigInt, x: BigInt)(implicit cache: Cache) = { - cache.cached.get(x) match { - case None() => - val res = f(x) - cache.cached = cache.cached.updated(x, res) - res - case Some(cached) => - cache.cacheHit = cache.cacheHit ++ Set(x) - cached + def call(a: A): B = { + cached.get(a) match { + case None() => + val res = fun(a) + cached = cached.updated(a, res) + res + case Some(res) => + cacheHit = cacheHit ++ Set(a) + res + } } + } def funProperlyCached(x: BigInt, fun: (BigInt) => BigInt, trash: List[BigInt]): Boolean = { - implicit val cache = Cache() - val res1 = cachedFun(fun, x) - multipleCalls(trash, x, fun) - val res2 = cachedFun(fun, x) - res1 == res2 && cache.cacheHit.contains(x) + val cachedFun = CachedFun[BigInt, BigInt](fun, Map(), Set()) + val res1 = cachedFun.call(x) + multipleCalls(trash, cachedFun, x) + val res2 = cachedFun.call(x) + res1 == res2 && cachedFun.cacheHit.contains(x) } holds - def multipleCalls(args: List[BigInt], x: BigInt, fun: (BigInt) => BigInt)(implicit cache: Cache): Unit = { - require(cache.cached.isDefinedAt(x)) + def multipleCalls(args: List[BigInt], cachedFun: CachedFun[BigInt, BigInt], x: BigInt): Unit = { + require(cachedFun.cached.isDefinedAt(x)) args match { case Nil() => () case y::ys => - cachedFun(fun, y) - multipleCalls(ys, x, fun) + cachedFun.call(x) + multipleCalls(ys, cachedFun, x) } - } ensuring(_ => old(cache).cached.get(x) == cache.cached.get(x)) + } ensuring(_ => old(cachedFun).cached.get(x) == cachedFun.cached.get(x)) }