From 3aa8929e9769d5931621bfed1d5db7316a9e6959 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 14 Mar 2016 19:45:14 +0100
Subject: [PATCH] fix issue with generic function
---
.../solvers/templates/TemplateGenerator.scala | 2 +-
.../scala/leon/xlang/AntiAliasingPhase.scala | 2 +-
.../verification/xlang/FunctionCaching.scala | 46 +++++++++----------
3 files changed, 24 insertions(+), 26 deletions(-)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 4556f7dd6..c7382d167 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 ace5274c2..9f05589f0 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 0a7c477a6..75c73e822 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))
}
--
GitLab