Skip to content
Snippets Groups Projects
Commit bbbc470b authored by Nicolas Voirol's avatar Nicolas Voirol Committed by Ravi
Browse files

Absolute value function for int32 types (termination)

parent 064fa2a0
No related branches found
No related tags found
No related merge requests found
...@@ -16,23 +16,51 @@ trait StructuralSize { ...@@ -16,23 +16,51 @@ trait StructuralSize {
private val sizeCache : MutableMap[TypeTree, FunDef] = MutableMap.empty private val sizeCache : MutableMap[TypeTree, FunDef] = MutableMap.empty
// function absBigInt(x: BigInt): BigInt = if (x >= 0) x else -x /* Absolute value for BigInt type
val typedAbsBigIntFun = makeAbsFun(IntegerType, "absBigInt", e => UMinus(e), InfiniteIntegerLiteral(0)) *
* def absBigInt(x: BigInt): BigInt = if (x >= 0) x else -x
// function absInt(x: Int): Int = if (x >= 0) x else -x */
val typedAbsIntFun = makeAbsFun(Int32Type, "absInt", e => BVUMinus(e), IntLiteral(0)) val typedAbsBigIntFun: TypedFunDef = {
val x = FreshIdentifier("x", IntegerType, alwaysShowUniqueID = true)
def makeAbsFun(tp: TypeTree, name: String, uminus: Expr => Expr, zero: Expr): TypedFunDef = { val absFun = new FunDef(FreshIdentifier("absBigInt", alwaysShowUniqueID = true), Seq(), Seq(ValDef(x)), IntegerType)
val x = FreshIdentifier("x", tp, alwaysShowUniqueID = true)
val absFun = new FunDef(FreshIdentifier(name, alwaysShowUniqueID = true), Seq(), Seq(ValDef(x)), tp)
absFun.body = Some(IfExpr( absFun.body = Some(IfExpr(
GreaterEquals(Variable(x), zero), GreaterEquals(Variable(x), InfiniteIntegerLiteral(0)),
Variable(x), Variable(x),
uminus(Variable(x)) UMinus(Variable(x))
)) ))
absFun.typed absFun.typed
} }
/* Absolute value for Int (32 bit) type
*
* We use a recursive function here as the bv2int functionality provided
* through SMT solvers is waaaaay too slow. Recursivity requires the
* postcondition for verification efforts to succeed.
*
* def absInt(x: Int): BigInt = (if (x == 0) {
* BigInt(0)
* } else if (x > 0) {
* 1 + absInt(x - 1)
* } else {
* 1 + absInt(-(x + 1)) // avoids -Integer.MIN_VALUE overflow
* }) ensuring (_ >= 0)
*/
def typedAbsIntFun: 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(
Equals(Variable(x), IntLiteral(0)),
InfiniteIntegerLiteral(0),
IfExpr(
GreaterThan(Variable(x), IntLiteral(0)),
Plus(InfiniteIntegerLiteral(1), FunctionInvocation(absFun.typed, Seq(BVMinus(Variable(x), IntLiteral(1))))),
Plus(InfiniteIntegerLiteral(1), FunctionInvocation(absFun.typed, Seq(BVUMinus(BVPlus(Variable(x), IntLiteral(1))))))
)))
val res = FreshIdentifier("res", IntegerType, alwaysShowUniqueID = true)
absFun.postcondition = Some(Lambda(Seq(ValDef(res)), GreaterEquals(Variable(res), InfiniteIntegerLiteral(0))))
absFun.typed
}
def size(expr: Expr) : Expr = { def size(expr: Expr) : Expr = {
def funDef(ct: ClassType, cases: ClassType => Seq[MatchCase]): FunDef = { def funDef(ct: ClassType, cases: ClassType => Seq[MatchCase]): FunDef = {
// we want to reuse generic size functions for sub-types // we want to reuse generic size functions for sub-types
...@@ -78,10 +106,8 @@ trait StructuralSize { ...@@ -78,10 +106,8 @@ trait StructuralSize {
}).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus) }).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus)
case IntegerType => case IntegerType =>
FunctionInvocation(typedAbsBigIntFun, Seq(expr)) FunctionInvocation(typedAbsBigIntFun, Seq(expr))
/*
case Int32Type => case Int32Type =>
FunctionInvocation(typedAbsIntFun, Seq(expr)) FunctionInvocation(typedAbsIntFun, Seq(expr))
*/
case _ => InfiniteIntegerLiteral(0) case _ => InfiniteIntegerLiteral(0)
} }
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment