/* Copyright 2009-2015 EPFL, Lausanne */ 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, indexFromLeft: Int): Int = { require(0 <= indexFromLeft && indexFromLeft < 32) if(bitAt(x, 31 - indexFromLeft)) toggleBitN(x, 31 - indexFromLeft)//(x ^ (1 << (31 - indexFromLeft))) else if(indexFromLeft == 0) x else turnOffRightmostOneRec(x, indexFromLeft - 1) } // proves in 10s def turnOffRightmostOne(x: Int): Int = { x & (x - 1) } //ensuring(_ == turnOffRightmostOneRec(x, 31)) // 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(0 <= i && i < 32 && 0 <= n && n < 32) val isOk = bitAt(x, i) == bitAt(y, (i + n) % 32) if (i == 0) isOk else isOk && 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, 31)) //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)) }