From 4481325f18b29570eb128a66397856635bcf661f Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Thu, 5 Feb 2015 12:12:10 +0100
Subject: [PATCH] add support for bits operations
Adds a benchmark with many cool magic tricks with bits.
However, proving some of them is very costly and we
could potentially look at opportunities to make the proofs
go through faster.
---
.../scala/leon/codegen/CodeGeneration.scala | 34 ++++++
.../leon/evaluators/RecursiveEvaluator.scala | 42 +++++++
.../leon/frontends/scalac/ASTExtractors.scala | 7 ++
.../frontends/scalac/CodeExtraction.scala | 26 +++--
.../scala/leon/purescala/Extractors.scala | 7 ++
.../scala/leon/purescala/PrettyPrinter.scala | 6 +
src/main/scala/leon/purescala/Trees.scala | 22 ++++
.../leon/solvers/smtlib/SMTLIBTarget.scala | 8 ++
.../leon/solvers/z3/AbstractZ3Solver.scala | 7 ++
.../purescala/valid/BitsTricks.scala | 103 ++++++++++++++++++
.../evaluators/DefaultEvaluatorTests.scala | 25 +++++
testcases/verification/BitsTricks.scala | 103 ++++++++++++++++++
12 files changed, 378 insertions(+), 12 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/BitsTricks.scala
create mode 100644 testcases/verification/BitsTricks.scala
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index dbca0c5de..75e15d5ac 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -628,6 +628,40 @@ trait CodeGeneration {
mkExpr(e, ch)
ch << INEG
+ case BVNot(e) =>
+ mkExpr(e, ch)
+ mkExpr(IntLiteral(-1), ch)
+ ch << IXOR
+
+ case BVAnd(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IAND
+
+ case BVOr(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IOR
+
+ case BVXOr(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IXOR
+
+ case BVShiftLeft(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << ISHL
+
+ case BVLShiftRight(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IUSHR
+
+ case BVAShiftRight(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << ISHR
case ArrayLength(a) =>
mkExpr(a, ch)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 1d060afb6..c90f56768 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -264,6 +264,12 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case re => throw EvalError(typeErrorMsg(re, Int32Type))
}
+ case BVNot(ex) =>
+ e(ex) match {
+ case IntLiteral(i) => IntLiteral(~i)
+ case re => throw EvalError(typeErrorMsg(re, Int32Type))
+ }
+
case Times(l,r) =>
(e(l), e(r)) match {
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 * i2)
@@ -304,6 +310,42 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
+ case BVAnd(l,r) =>
+ (e(l), e(r)) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 & i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case BVOr(l,r) =>
+ (e(l), e(r)) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 | i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case BVXOr(l,r) =>
+ (e(l), e(r)) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 ^ i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case BVShiftLeft(l,r) =>
+ (e(l), e(r)) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 << i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case BVAShiftRight(l,r) =>
+ (e(l), e(r)) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 >> i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
+ case BVLShiftRight(l,r) =>
+ (e(l), e(r)) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 >>> i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
+ }
+
case LessThan(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 8f9f8b0b7..dfd099bcc 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -750,6 +750,13 @@ trait ASTExtractors {
}
}
+ object ExBVNot {
+ def unapply(tree: Select): Option[Tree] = tree match {
+ case Select(t, n) if (n == nme.UNARY_~ && hasIntType(t)) => Some(t)
+ case _ => None
+ }
+ }
+
object ExPatternMatching {
def unapply(tree: Match): Option[(Tree,List[CaseDef])] =
if(tree != null) Some((tree.selector, tree.cases)) else None
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 8b63ff731..df19be74d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1329,6 +1329,7 @@ trait CodeExtraction extends ASTExtractors {
case ExNot(e) => Not(extractTree(e))
case ExUMinus(e) => UMinus(extractTree(e))
case ExBVUMinus(e) => BVUMinus(extractTree(e))
+ case ExBVNot(e) => BVNot(extractTree(e))
case ExEquals(l, r) =>
val rl = extractTree(l)
@@ -1535,37 +1536,38 @@ trait CodeExtraction extends ASTExtractors {
LessThan(a1, a2)
case (IsTyped(a1, IntegerType), "<=", List(IsTyped(a2, IntegerType))) =>
LessEquals(a1, a2)
- case (IsTyped(a1, IntegerType), "<=", List(IsTyped(a2, IntegerType))) =>
- LessEquals(a1, a2)
// Int methods
case (IsTyped(a1, Int32Type), "+", List(IsTyped(a2, Int32Type))) =>
BVPlus(a1, a2)
-
case (IsTyped(a1, Int32Type), "-", List(IsTyped(a2, Int32Type))) =>
BVMinus(a1, a2)
-
case (IsTyped(a1, Int32Type), "*", List(IsTyped(a2, Int32Type))) =>
BVTimes(a1, a2)
-
case (IsTyped(a1, Int32Type), "%", List(IsTyped(a2, Int32Type))) =>
BVModulo(a1, a2)
-
case (IsTyped(a1, Int32Type), "/", List(IsTyped(a2, Int32Type))) =>
BVDivision(a1, a2)
+ case (IsTyped(a1, Int32Type), "|", List(IsTyped(a2, Int32Type))) =>
+ BVOr(a1, a2)
+ case (IsTyped(a1, Int32Type), "&", List(IsTyped(a2, Int32Type))) =>
+ BVAnd(a1, a2)
+ case (IsTyped(a1, Int32Type), "^", List(IsTyped(a2, Int32Type))) =>
+ BVXOr(a1, a2)
+ case (IsTyped(a1, Int32Type), "<<", List(IsTyped(a2, Int32Type))) =>
+ BVShiftLeft(a1, a2)
+ case (IsTyped(a1, Int32Type), ">>", List(IsTyped(a2, Int32Type))) =>
+ BVAShiftRight(a1, a2)
+ case (IsTyped(a1, Int32Type), ">>>", List(IsTyped(a2, Int32Type))) =>
+ BVLShiftRight(a1, a2)
+
case (IsTyped(a1, Int32Type), ">", List(IsTyped(a2, Int32Type))) =>
GreaterThan(a1, a2)
-
case (IsTyped(a1, Int32Type), ">=", List(IsTyped(a2, Int32Type))) =>
GreaterEquals(a1, a2)
-
case (IsTyped(a1, Int32Type), "<", List(IsTyped(a2, Int32Type))) =>
LessThan(a1, a2)
-
- case (IsTyped(a1, Int32Type), "<=", List(IsTyped(a2, Int32Type))) =>
- LessEquals(a1, a2)
-
case (IsTyped(a1, Int32Type), "<=", List(IsTyped(a2, Int32Type))) =>
LessEquals(a1, a2)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index a62521d84..52b434db6 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -19,6 +19,7 @@ object Extractors {
case Not(t) => Some((t,Not(_)))
case UMinus(t) => Some((t,UMinus))
case BVUMinus(t) => Some((t,BVUMinus))
+ case BVNot(t) => Some((t,BVNot))
case SetCardinality(t) => Some((t,SetCardinality))
case MultisetCardinality(t) => Some((t,MultisetCardinality))
case MultisetToSet(t) => Some((t,MultisetToSet))
@@ -57,6 +58,12 @@ object Extractors {
case BVTimes(t1,t2) => Some((t1,t2,BVTimes))
case BVDivision(t1,t2) => Some((t1,t2,BVDivision))
case BVModulo(t1,t2) => Some((t1,t2,BVModulo))
+ case BVAnd(t1,t2) => Some((t1,t2,BVAnd))
+ case BVOr(t1,t2) => Some((t1,t2,BVOr))
+ case BVXOr(t1,t2) => Some((t1,t2,BVXOr))
+ case BVShiftLeft(t1,t2) => Some((t1,t2,BVShiftLeft))
+ case BVAShiftRight(t1,t2) => Some((t1,t2,BVAShiftRight))
+ case BVLShiftRight(t1,t2) => Some((t1,t2,BVLShiftRight))
case ElementOfSet(t1,t2) => Some((t1,t2,ElementOfSet))
case SubsetOf(t1,t2) => Some((t1,t2,SubsetOf))
case SetIntersection(t1,t2) => Some((t1,t2,SetIntersection))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index baa1a2c20..1559634ed 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -348,6 +348,12 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case BVTimes(l,r) => optP { p"$l * $r" }
case BVDivision(l,r) => optP { p"$l / $r" }
case BVModulo(l,r) => optP { p"$l % $r" }
+ case BVAnd(l,r) => optP { p"$l & $r" }
+ case BVOr(l,r) => optP { p"$l | $r" }
+ case BVXOr(l,r) => optP { p"$l ^ $r" }
+ case BVShiftLeft(l,r) => optP { p"$l << $r" }
+ case BVAShiftRight(l,r) => optP { p"$l >> $r" }
+ case BVLShiftRight(l,r) => optP { p"$l >>> $r" }
case FiniteSet(rs) => p"{${rs.toSeq}}"
case FiniteMultiset(rs) => p"{|$rs|)"
case EmptyMultiset(_) => p"\u2205"
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index eeb15220f..60b6eb3fb 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -372,6 +372,28 @@ object Trees {
val getType = Int32Type
}
+ case class BVNot(expr: Expr) extends Expr {
+ val getType = Int32Type
+ }
+ case class BVAnd(lhs: Expr, rhs: Expr) extends Expr {
+ val getType = Int32Type
+ }
+ case class BVOr(lhs: Expr, rhs: Expr) extends Expr {
+ val getType = Int32Type
+ }
+ case class BVXOr(lhs: Expr, rhs: Expr) extends Expr {
+ val getType = Int32Type
+ }
+ case class BVShiftLeft(lhs: Expr, rhs: Expr) extends Expr {
+ val getType = Int32Type
+ }
+ case class BVAShiftRight(lhs: Expr, rhs: Expr) extends Expr {
+ val getType = Int32Type
+ }
+ case class BVLShiftRight(lhs: Expr, rhs: Expr) extends Expr {
+ val getType = Int32Type
+ }
+
case class IntToBigInt(expr: Expr) extends Expr {
val getType = Int32Type
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 98a129ce2..6cfa02774 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -442,6 +442,8 @@ trait SMTLIBTarget {
e match {
case (_: Not) => Core.Not(toSMT(u))
case (_: UMinus) => Ints.Neg(toSMT(u))
+ case (_: BVUMinus) => FixedSizeBitVectors.Neg(toSMT(u))
+ case (_: BVNot) => FixedSizeBitVectors.Not(toSMT(u))
case _ => reporter.fatalError("Unhandled unary "+e)
}
@@ -475,6 +477,12 @@ trait SMTLIBTarget {
case (_: BVTimes) => FixedSizeBitVectors.Mul(toSMT(a), toSMT(b))
case (_: BVDivision) => FixedSizeBitVectors.SDiv(toSMT(a), toSMT(b))
case (_: BVModulo) => FixedSizeBitVectors.SRem(toSMT(a), toSMT(b))
+ case (_: BVAnd) => FixedSizeBitVectors.And(toSMT(a), toSMT(b))
+ case (_: BVOr) => FixedSizeBitVectors.Or(toSMT(a), toSMT(b))
+ case (_: BVXOr) => FixedSizeBitVectors.XOr(toSMT(a), toSMT(b))
+ case (_: BVShiftLeft) => FixedSizeBitVectors.ShiftLeft(toSMT(a), toSMT(b))
+ case (_: BVAShiftRight) => FixedSizeBitVectors.AShiftRight(toSMT(a), toSMT(b))
+ case (_: BVLShiftRight) => FixedSizeBitVectors.LShiftRight(toSMT(a), toSMT(b))
case _ => reporter.fatalError("Unhandled binary "+e)
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index ab53266df..cb8954e29 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -582,6 +582,13 @@ trait AbstractZ3Solver
case BVDivision(l, r) => z3.mkBVSdiv(rec(l), rec(r))
case BVModulo(l, r) => z3.mkBVSrem(rec(l), rec(r))
case BVUMinus(e) => z3.mkBVNeg(rec(e))
+ case BVNot(e) => z3.mkBVNot(rec(e))
+ case BVAnd(l, r) => z3.mkBVAnd(rec(l), rec(r))
+ case BVOr(l, r) => z3.mkBVOr(rec(l), rec(r))
+ case BVXOr(l, r) => z3.mkBVXor(rec(l), rec(r))
+ case BVShiftLeft(l, r) => z3.mkBVShl(rec(l), rec(r))
+ case BVAShiftRight(l, r) => z3.mkBVAshr(rec(l), rec(r))
+ case BVLShiftRight(l, r) => z3.mkBVLshr(rec(l), rec(r))
case LessThan(l, r) => l.getType match {
case IntegerType => z3.mkLT(rec(l), rec(r))
case Int32Type => z3.mkBVSlt(rec(l), rec(r))
diff --git a/src/test/resources/regression/verification/purescala/valid/BitsTricks.scala b/src/test/resources/regression/verification/purescala/valid/BitsTricks.scala
new file mode 100644
index 000000000..561f38a19
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/BitsTricks.scala
@@ -0,0 +1,103 @@
+import leon.annotation._
+import leon.lang._
+
+object BitsTricks {
+
+ def bitAt(x: Int, n: Int): Boolean = {
+ require(n >= 0 && n < 32)
+ ((x >> n) & 1) == 1
+ }
+
+ def isEven(x: Int): Boolean = {
+ (x & 1) == 0
+ } ensuring(res => res == (x % 2 == 0))
+
+ def isNegative(x: Int): Boolean = {
+ (x >>> 31) == 1
+ } ensuring(b => b == x < 0)
+
+ def isBitNSet(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ (x & (1 << n))
+ }
+
+ def testBitSet1(): Int = {
+ isBitNSet(122, 3)
+ } ensuring(_ != 0)
+ def testBitSet2(): Int = {
+ isBitNSet(-33, 5)
+ } ensuring(_ == 0)
+
+ def setBitN(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ x | (1 << n)
+ } ensuring(res => isBitNSet(res, n) != 0)
+
+ def toggleBitN(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ x ^ (1 << n)
+ } ensuring(res =>
+ if(isBitNSet(x, n) != 0) isBitNSet(res, n) == 0
+ else isBitNSet(res, n) != 0)
+
+
+ def checkDoubleXor(x: Int, y: Int): Int = {
+ x ^ y ^ x
+ } ensuring(res => res == y)
+
+
+ def turnOffRightmostOneRec(x: Int, index: Int): Int = {
+ require(index >= 0 && index < 32)
+ if(bitAt(x, index)) toggleBitN(x, index)//(x ^ (1 << index))
+ else if(index == 31) x
+ else turnOffRightmostOneRec(x, index + 1)
+ }
+
+ /*
+ * loops forever on the proof
+ */
+ def turnOffRightmostOne(x: Int): Int = {
+ x & (x - 1)
+ } //ensuring(_ == turnOffRightmostOneRec(x, 0))
+
+ // 010100 -> 010111
+ def rightPropagateRightmostOne(x: Int): Int = {
+ x | (x - 1)
+ }
+
+ def property1(x: Int): Boolean = {
+ val y = rightPropagateRightmostOne(x)
+ y == rightPropagateRightmostOne(y)
+ } ensuring(b => b)
+
+ def isRotationLeft(x: Int, y: Int, n: Int, i: Int): Boolean = {
+ require(i >= 0 && i <= 32 && n >= 0 && n < 32)
+ if(i == 32)
+ true
+ else bitAt(x, i) == bitAt(y, (i + n) % 32) && isRotationLeft(x, y, n, i+1)
+ }
+
+ //rotateLeft proves in 1 minute (on very powerful computer)
+ def rotateLeft(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ val front = x >>> (32 - n)
+ (x << n) | front
+ } //ensuring(res => isRotationLeft(x, res, n, 0))
+
+ //careful with overflows, case definition, truncated
+ def safeMean(x: Int, y: Int): Int = {
+ if(x >= 0 && y <= 0 || x <= 0 && y >= 0) (x + y)/2
+ else if(x >= 0 && x <= y) x + (y - x)/2
+ else if(x >= 0 && y <= x) y + (x - y)/2
+ else if(x <= 0 && x <= y) y + (x - y)/2
+ else x + (y - x)/2
+ }
+
+ //proves in 45 seconds
+ def magicMean(x: Int, y: Int): Int = {
+ val t = (x&y)+((x^y) >> 1)
+ t + ((t >>> 31) & (x ^ y))
+ } //ensuring(res => res == safeMean(x, y))
+
+
+}
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index 7dd1b4742..fd0c09a2a 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -44,6 +44,31 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
expectSuccessful(defaultEvaluator.eval(BVTimes(IntLiteral(3), IntLiteral(3))), IntLiteral(9))
}
+ test("eval bitwise operations") {
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(3), IntLiteral(1))), IntLiteral(1))
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(3), IntLiteral(3))), IntLiteral(3))
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(5), IntLiteral(3))), IntLiteral(1))
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(5), IntLiteral(4))), IntLiteral(4))
+ expectSuccessful(defaultEvaluator.eval(BVAnd(IntLiteral(5), IntLiteral(2))), IntLiteral(0))
+
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(3), IntLiteral(1))), IntLiteral(3))
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(3), IntLiteral(3))), IntLiteral(3))
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(5), IntLiteral(3))), IntLiteral(7))
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(5), IntLiteral(4))), IntLiteral(5))
+ expectSuccessful(defaultEvaluator.eval(BVOr(IntLiteral(5), IntLiteral(2))), IntLiteral(7))
+
+ expectSuccessful(defaultEvaluator.eval(BVXOr(IntLiteral(3), IntLiteral(1))), IntLiteral(2))
+ expectSuccessful(defaultEvaluator.eval(BVXOr(IntLiteral(3), IntLiteral(3))), IntLiteral(0))
+
+ expectSuccessful(defaultEvaluator.eval(BVNot(IntLiteral(1))), IntLiteral(-2))
+
+ expectSuccessful(defaultEvaluator.eval(BVShiftLeft(IntLiteral(3), IntLiteral(1))), IntLiteral(6))
+ expectSuccessful(defaultEvaluator.eval(BVShiftLeft(IntLiteral(4), IntLiteral(2))), IntLiteral(16))
+
+ expectSuccessful(defaultEvaluator.eval(BVLShiftRight(IntLiteral(8), IntLiteral(1))), IntLiteral(4))
+ expectSuccessful(defaultEvaluator.eval(BVAShiftRight(IntLiteral(8), IntLiteral(1))), IntLiteral(4))
+ }
+
test("eval of simple arithmetic expressions") {
expectSuccessful(
defaultEvaluator.eval(Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(5))),
diff --git a/testcases/verification/BitsTricks.scala b/testcases/verification/BitsTricks.scala
new file mode 100644
index 000000000..993c7e515
--- /dev/null
+++ b/testcases/verification/BitsTricks.scala
@@ -0,0 +1,103 @@
+import leon.annotation._
+import leon.lang._
+
+object BitsTricks {
+
+ def bitAt(x: Int, n: Int): Boolean = {
+ require(n >= 0 && n < 32)
+ ((x >> n) & 1) == 1
+ }
+
+ def isEven(x: Int): Boolean = {
+ (x & 1) == 0
+ } ensuring(res => res == (x % 2 == 0))
+
+ def isNegative(x: Int): Boolean = {
+ (x >>> 31) == 1
+ } ensuring(b => b == x < 0)
+
+ def isBitNSet(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ (x & (1 << n))
+ }
+
+ def testBitSet1(): Int = {
+ isBitNSet(122, 3)
+ } ensuring(_ != 0)
+ def testBitSet2(): Int = {
+ isBitNSet(-33, 5)
+ } ensuring(_ == 0)
+
+ def setBitN(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ x | (1 << n)
+ } ensuring(res => isBitNSet(res, n) != 0)
+
+ def toggleBitN(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ x ^ (1 << n)
+ } ensuring(res =>
+ if(isBitNSet(x, n) != 0) isBitNSet(res, n) == 0
+ else isBitNSet(res, n) != 0)
+
+
+ def checkDoubleXor(x: Int, y: Int): Int = {
+ x ^ y ^ x
+ } ensuring(res => res == y)
+
+
+ def turnOffRightmostOneRec(x: Int, index: Int): Int = {
+ require(index >= 0 && index < 32)
+ if(bitAt(x, index)) toggleBitN(x, index)//(x ^ (1 << index))
+ else if(index == 31) x
+ else turnOffRightmostOneRec(x, index + 1)
+ }
+
+ /*
+ * loops forever on the proof
+ */
+ def turnOffRightmostOne(x: Int): Int = {
+ x & (x - 1)
+ } ensuring(_ == turnOffRightmostOneRec(x, 0))
+
+ // 010100 -> 010111
+ def rightPropagateRightmostOne(x: Int): Int = {
+ x | (x - 1)
+ }
+
+ def property1(x: Int): Boolean = {
+ val y = rightPropagateRightmostOne(x)
+ y == rightPropagateRightmostOne(y)
+ } ensuring(b => b)
+
+ def isRotationLeft(x: Int, y: Int, n: Int, i: Int): Boolean = {
+ require(i >= 0 && i <= 32 && n >= 0 && n < 32)
+ if(i == 32)
+ true
+ else bitAt(x, i) == bitAt(y, (i + n) % 32) && isRotationLeft(x, y, n, i+1)
+ }
+
+ //rotateLeft proves in 1 minute (on very powerful computer)
+ def rotateLeft(x: Int, n: Int): Int = {
+ require(n >= 0 && n < 32)
+ val front = x >>> (32 - n)
+ (x << n) | front
+ } ensuring(res => isRotationLeft(x, res, n, 0))
+
+ //careful with overflows, case definition, truncated
+ def safeMean(x: Int, y: Int): Int = {
+ if(x >= 0 && y <= 0 || x <= 0 && y >= 0) (x + y)/2
+ else if(x >= 0 && x <= y) x + (y - x)/2
+ else if(x >= 0 && y <= x) y + (x - y)/2
+ else if(x <= 0 && x <= y) y + (x - y)/2
+ else x + (y - x)/2
+ }
+
+ //proves in 45 seconds
+ def magicMean(x: Int, y: Int): Int = {
+ val t = (x&y)+((x^y) >> 1)
+ t + ((t >>> 31) & (x ^ y))
+ } ensuring(res => res == safeMean(x, y))
+
+
+}
--
GitLab