From b293a63bb8ee94868dc9f2f66a36ed64f266444f Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 25 Apr 2016 14:57:22 +0200
Subject: [PATCH] Small fix to termination checker for int32 termination
---
.../scala/leon/termination/Processor.scala | 11 ++-----
.../leon/termination/RelationComparator.scala | 9 ++++--
.../leon/termination/StructuralSize.scala | 30 ++++++++++++++-----
3 files changed, 31 insertions(+), 19 deletions(-)
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 6f998b0ed..024385ebf 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -27,15 +27,8 @@ trait Solvable extends Processor {
val modules: Strengthener with StructuralSize
- private val solver: SolverFactory[Solver] = {
- val program : Program = checker.program
- val context : LeonContext = checker.context
- val sizeModule : ModuleDef = ModuleDef(FreshIdentifier("$size"), modules.defs.toSeq, false)
- val sizeUnit : UnitDef = UnitDef(FreshIdentifier("$size"),Seq(sizeModule))
- val newProgram : Program = program.copy( units = sizeUnit :: program.units)
-
- SolverFactory.getFromSettings(context, newProgram).withTimeout(1.seconds)
- }
+ private val solver: SolverFactory[Solver] =
+ SolverFactory.getFromSettings(checker.context, checker.program).withTimeout(1.seconds)
type Solution = (Option[Boolean], Map[Identifier, Expr])
diff --git a/src/main/scala/leon/termination/RelationComparator.scala b/src/main/scala/leon/termination/RelationComparator.scala
index 0d72d5021..150759232 100644
--- a/src/main/scala/leon/termination/RelationComparator.scala
+++ b/src/main/scala/leon/termination/RelationComparator.scala
@@ -76,19 +76,22 @@ trait BVRelationComparator extends RelationComparator { self : StructuralSize =>
def isApplicableFor(p: Problem): Boolean = {
p.funDefs.forall(fd => fd.params.exists(valdef => valdef.getType == Int32Type))
}
-
+
def bvSize(e: Expr): Expr = FunctionInvocation(typedAbsIntFun, Seq(e))
+ /* Note: We swap the arguments to the `lexicographicDecreasing` call
+ * since bvSize maps into negative ints! (avoids -Integer.MIN_VALUE overflow) */
+
def sizeDecreasing(s10: Seq[Expr], s20: Seq[Expr]): Expr = {
val s1 = s10.filter(_.getType == Int32Type)
val s2 = s20.filter(_.getType == Int32Type)
- lexicographicDecreasing(s1, s2, strict = true, sizeOfOneExpr = bvSize)
+ lexicographicDecreasing(s2, s1, strict = true, sizeOfOneExpr = bvSize)
}
def softDecreasing(s10: Seq[Expr], s20: Seq[Expr]): Expr = {
val s1 = s10.filter(_.getType == Int32Type)
val s2 = s20.filter(_.getType == Int32Type)
- lexicographicDecreasing(s1, s2, strict = false, sizeOfOneExpr = bvSize)
+ lexicographicDecreasing(s2, s1, strict = false, sizeOfOneExpr = bvSize)
}
}
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 8d53f0c6f..9a1995365 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -14,8 +14,8 @@ import scala.collection.mutable.{Map => MutableMap}
trait StructuralSize {
- private val sizeCache : MutableMap[TypeTree, FunDef] = MutableMap.empty
-
+ private val sizeCache: MutableMap[TypeTree, FunDef] = MutableMap.empty
+
/* Absolute value for BigInt type
*
* def absBigInt(x: BigInt): BigInt = if (x >= 0) x else -x
@@ -31,7 +31,25 @@ trait StructuralSize {
absFun.typed
}
- /* Absolute value for Int (32 bit) type
+ /* Negative absolute value for Int type
+ *
+ * To avoid -Integer.MIN_VALUE overflow, we use negative absolute value
+ * for bitvector integers.
+ *
+ * def absInt(x: Int): Int = if (x >= 0) -x else x
+ */
+ val typedAbsIntFun: TypedFunDef = {
+ val x = FreshIdentifier("x", Int32Type, alwaysShowUniqueID = true)
+ val absFun = new FunDef(FreshIdentifier("absInt", alwaysShowUniqueID = true), Seq(), Seq(ValDef(x)), Int32Type)
+ absFun.body = Some(IfExpr(
+ GreaterEquals(Variable(x), IntLiteral(0)),
+ BVUMinus(Variable(x)),
+ Variable(x)
+ ))
+ absFun.typed
+ }
+
+ /* Absolute value for Int (32 bit) type into mathematical integers
*
* We use a recursive function here as the bv2int functionality provided
* through SMT solvers is waaaaay too slow. Recursivity requires the
@@ -45,7 +63,7 @@ trait StructuralSize {
* 1 + absInt(-(x + 1)) // avoids -Integer.MIN_VALUE overflow
* }) ensuring (_ >= 0)
*/
- def typedAbsIntFun: TypedFunDef = {
+ def typedAbsInt2IntegerFun: TypedFunDef = {
val x = FreshIdentifier("x", Int32Type, alwaysShowUniqueID = true)
val absFun = new FunDef(FreshIdentifier("absInt", alwaysShowUniqueID = true), Seq(), Seq(ValDef(x)), IntegerType)
absFun.body = Some(IfExpr(
@@ -107,7 +125,7 @@ trait StructuralSize {
case IntegerType =>
FunctionInvocation(typedAbsBigIntFun, Seq(expr))
case Int32Type =>
- FunctionInvocation(typedAbsIntFun, Seq(expr))
+ FunctionInvocation(typedAbsInt2IntegerFun, Seq(expr))
case _ => InfiniteIntegerLiteral(0)
}
}
@@ -129,6 +147,4 @@ trait StructuralSize {
greaterBecauseGreaterAtFirstDifferentPos
}
}
-
- def defs : Set[FunDef] = Set(sizeCache.values.toSeq : _*)
}
--
GitLab