Formalization of SIGNEXTEND and rule proofs

Author: chriseth

test/formal/opcodes.py

@@ -64,3 +64,18 @@ def BYTE(i, x):
 		BitVecVal(0, x.size()),
 		(LShR(x, (x.size() - bit))) & 0xff
 	)
+
+def SIGNEXTEND(i, x):
+	bitBV = i * 8 + 7
+	bitInt = BV2Int(i) * 8 + 7
+	test = BitVecVal(1, x.size()) << bitBV
+	mask = test - 1
+	return If(
+		bitInt >= x.size(),
+		x,
+		If(
+			(x & test) == 0,
+			x & mask,
+			x | ~mask
+		)
+	)

test/formal/signextend.py

@@ -0,0 +1,37 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+1) SIGNEXTEND(A, X) -> X if A >= Pattern::WordSize / 8 - 1;
+
+2) SIGNEXTEND(X, SIGNEXTEND(X, Y)) -> SIGNEXTEND(X, Y)
+
+3) SIGNEXTEND(A, SIGNEXTEND(B, X)) -> SIGNEXTEND(min(A, B), X)
+"""
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule1 = Rule()
+# Requirements
+rule1.require(UGE(A, BitVecVal(n_bits // 8 - 1, n_bits)))
+rule1.check(SIGNEXTEND(A, X), X)
+
+rule2 = Rule()
+rule2.check(
+    SIGNEXTEND(X, SIGNEXTEND(X, Y)),
+    SIGNEXTEND(X, Y)
+)
+
+rule3 = Rule()
+rule3.check(
+    SIGNEXTEND(A, SIGNEXTEND(B, X)),
+    SIGNEXTEND(If(ULT(A, B), A, B), X)
+)
+

test/formal/signextend_and.py

@@ -0,0 +1,26 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+AND(A, SIGNEXTEND(B, X)) -> AND(A, X)
+given
+    B < WordSize / 8 - 1 AND
+    A & (1 << ((B + 1) * 8) - 1) == A
+"""
+
+n_bits = 128
+
+# Input vars
+X = BitVec('X', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule = Rule()
+# Requirements
+rule.require(ULT(B, BitVecVal(n_bits // 8 - 1, n_bits)))
+rule.require((A & ((BitVecVal(1, n_bits) << ((B + 1) * 8)) - 1)) == A)
+rule.check(
+    AND(A, SIGNEXTEND(B, X)),
+    AND(A, X)
+)

test/formal/signextend_shl.py

@@ -0,0 +1,25 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+SHL(A, SIGNEXTEND(B, X)) -> SIGNEXTEND((A >> 3) + B, SHL(A, X))
+given return A & 7 == 0  AND  A <= WordSize  AND  B <= WordSize / 8
+"""
+
+n_bits = 256
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule = Rule()
+rule.require(A & 7 == 0)
+rule.require(ULE(A, n_bits))
+rule.require(ULE(B, n_bits / 8))
+rule.check(
+    SHL(A, SIGNEXTEND(B, X)),
+    SIGNEXTEND(LShR(A, 3) + B, SHL(A, X))
+)

test/formal/signextend_shr.py

@@ -0,0 +1,31 @@
+from rule import Rule
+from opcodes import *
+
+"""
+Rule:
+SIGNEXTEND(A, SHR(B, X)) -> SAR(B, X)
+given
+    B % 8 == 0 AND
+    A <= WordSize AND
+    B <= wordSize AND
+    (WordSize - B) / 8 == A + 1
+"""
+
+n_bits = 256
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+B = BitVec('B', n_bits)
+
+rule = Rule()
+rule.require(B % 8 == 0)
+rule.require(ULE(A, n_bits))
+rule.require(ULE(B, n_bits))
+rule.require((BitVecVal(n_bits, n_bits) - B) / 8 == A + 1)
+rule.check(
+    SIGNEXTEND(A, SHR(B, X)),
+    SAR(B, X)
+)
+