From c71fb76bb217f56b3a8a707998463ac8a6b18987 Mon Sep 17 00:00:00 2001 From: Daniel Kirchner Date: Fri, 14 Jun 2019 17:47:54 +0200 Subject: [PATCH] Proofs for the overflow and underflow conditions in checked arithmetic for Sol->Yul code generation. --- test/formal/checked_int_add.py | 39 +++++++++++++++++++++++++++ test/formal/checked_int_div.py | 35 +++++++++++++++++++++++++ test/formal/checked_int_mul_16.py | 42 ++++++++++++++++++++++++++++++ test/formal/checked_int_sub.py | 39 +++++++++++++++++++++++++++ test/formal/checked_uint_add.py | 35 +++++++++++++++++++++++++ test/formal/checked_uint_mul_16.py | 36 +++++++++++++++++++++++++ test/formal/checked_uint_sub.py | 35 +++++++++++++++++++++++++ test/formal/opcodes.py | 3 +++ test/formal/util.py | 27 +++++++++++++++++++ 9 files changed, 291 insertions(+) create mode 100644 test/formal/checked_int_add.py create mode 100644 test/formal/checked_int_div.py create mode 100644 test/formal/checked_int_mul_16.py create mode 100644 test/formal/checked_int_sub.py create mode 100644 test/formal/checked_uint_add.py create mode 100644 test/formal/checked_uint_mul_16.py create mode 100644 test/formal/checked_uint_sub.py create mode 100644 test/formal/util.py diff --git a/test/formal/checked_int_add.py b/test/formal/checked_int_add.py new file mode 100644 index 000000000..6e74944e2 --- /dev/null +++ b/test/formal/checked_int_add.py @@ -0,0 +1,39 @@ +from rule import Rule +from opcodes import * +from util import * + +""" +Overflow checked signed integer addition. +""" + +n_bits = 256 +type_bits = 8 + +while type_bits <= n_bits: + + rule = Rule() + + # Input vars + X_short = BitVec('X', type_bits) + Y_short = BitVec('Y', type_bits) + + # Z3's overflow and underflow conditions + actual_overflow = Not(BVAddNoOverflow(X_short, Y_short, True)) + actual_underflow = Not(BVAddNoUnderflow(X_short, Y_short)) + + # cast to full n_bits values + X = BVSignedUpCast(X_short, n_bits) + Y = BVSignedUpCast(Y_short, n_bits) + + # Constants + maxValue = BVSignedMax(type_bits, n_bits) + minValue = BVSignedMin(type_bits, n_bits) + + # Overflow and underflow checks in YulUtilFunction::overflowCheckedIntAddFunction + overflow_check = AND(ISZERO(SLT(X, 0)), SGT(Y, SUB(maxValue, X))) + underflow_check = AND(SLT(X, 0), SLT(Y, SUB(minValue, X))) + + rule.check(actual_overflow, overflow_check != 0) + rule.check(actual_underflow, underflow_check != 0) + + type_bits *= 2 diff --git a/test/formal/checked_int_div.py b/test/formal/checked_int_div.py new file mode 100644 index 000000000..2a36a9488 --- /dev/null +++ b/test/formal/checked_int_div.py @@ -0,0 +1,35 @@ +from rule import Rule +from opcodes import * +from util import * + +""" +Overflow checked signed integer division. +""" + +n_bits = 256 +type_bits = 8 + +while type_bits <= n_bits: + + rule = Rule() + + # Input vars + X_short = BitVec('X', type_bits) + Y_short = BitVec('Y', type_bits) + + # Z3's overflow conditions + actual_overflow = Not(BVSDivNoOverflow(X_short, Y_short)) + + # cast to full n_bits values + X = BVSignedUpCast(X_short, n_bits) + Y = BVSignedUpCast(Y_short, n_bits) + + # Constants + minValue = BVSignedMin(type_bits, n_bits) + + # Overflow check in YulUtilFunction::overflowCheckedIntDivFunction + overflow_check = AND(EQ(X, minValue), EQ(Y, SUB(0, 1))) + + rule.check(actual_overflow, overflow_check != 0) + + type_bits *= 2 diff --git a/test/formal/checked_int_mul_16.py b/test/formal/checked_int_mul_16.py new file mode 100644 index 000000000..cc8743b1d --- /dev/null +++ b/test/formal/checked_int_mul_16.py @@ -0,0 +1,42 @@ +from rule import Rule +from opcodes import * +from util import * + +""" +Overflow checked signed integer multiplication. +""" + +# Approximation with 16-bit base types. +n_bits = 16 +type_bits = 8 + +while type_bits <= n_bits: + + rule = Rule() + + # Input vars + X_short = BitVec('X', type_bits) + Y_short = BitVec('Y', type_bits) + + # Z3's overflow and underflow conditions + actual_overflow = Not(BVMulNoOverflow(X_short, Y_short, True)) + actual_underflow = Not(BVMulNoUnderflow(X_short, Y_short)) + + # cast to full n_bits values + X = BVSignedUpCast(X_short, n_bits) + Y = BVSignedUpCast(Y_short, n_bits) + + # Constants + maxValue = BVSignedMax(type_bits, n_bits) + minValue = BVSignedMin(type_bits, n_bits) + + # Overflow and underflow checks in YulUtilFunction::overflowCheckedIntMulFunction + overflow_check_1 = AND(AND(SGT(X, 0), SGT(Y, 0)), GT(X, DIV(maxValue, Y))) + underflow_check_1 = AND(AND(SGT(X, 0), SLT(Y, 0)), SLT(Y, SDIV(minValue, X))) + underflow_check_2 = AND(AND(SLT(X, 0), SGT(Y, 0)), SLT(X, SDIV(minValue, Y))) + overflow_check_2 = AND(AND(SLT(X, 0), SLT(Y, 0)), SLT(X, SDIV(maxValue, Y))) + + rule.check(actual_overflow, Or(overflow_check_1 != 0, overflow_check_2 != 0)) + rule.check(actual_underflow, Or(underflow_check_1 != 0, underflow_check_2 != 0)) + + type_bits *= 2 diff --git a/test/formal/checked_int_sub.py b/test/formal/checked_int_sub.py new file mode 100644 index 000000000..72a0a2109 --- /dev/null +++ b/test/formal/checked_int_sub.py @@ -0,0 +1,39 @@ +from rule import Rule +from opcodes import * +from util import * + +""" +Overflow checked signed integer subtraction. +""" + +n_bits = 256 +type_bits = 8 + +while type_bits <= n_bits: + + rule = Rule() + + # Input vars + X_short = BitVec('X', type_bits) + Y_short = BitVec('Y', type_bits) + + # Z3's overflow and underflow conditions + actual_overflow = Not(BVSubNoOverflow(X_short, Y_short)) + actual_underflow = Not(BVSubNoUnderflow(X_short, Y_short, True)) + + # cast to full n_bits values + X = BVSignedUpCast(X_short, n_bits) + Y = BVSignedUpCast(Y_short, n_bits) + + # Constants + maxValue = BVSignedMax(type_bits, n_bits) + minValue = BVSignedMin(type_bits, n_bits) + + # Overflow and underflow checks in YulUtilFunction::overflowCheckedIntSubFunction + underflow_check = AND(ISZERO(SLT(Y, 0)), SLT(X, ADD(minValue, Y))) + overflow_check = AND(SLT(Y, 0), SGT(X, ADD(maxValue, Y))) + + rule.check(actual_underflow, underflow_check != 0) + rule.check(actual_overflow, overflow_check != 0) + + type_bits *= 2 diff --git a/test/formal/checked_uint_add.py b/test/formal/checked_uint_add.py new file mode 100644 index 000000000..596fa04f0 --- /dev/null +++ b/test/formal/checked_uint_add.py @@ -0,0 +1,35 @@ +from rule import Rule +from opcodes import * +from util import * + +""" +Overflow checked unsigned integer addition. +""" + +n_bits = 256 +type_bits = 8 + +while type_bits <= n_bits: + + rule = Rule() + + # Input vars + X_short = BitVec('X', type_bits) + Y_short = BitVec('Y', type_bits) + + # Z3's overflow condition + actual_overflow = Not(BVAddNoOverflow(X_short, Y_short, False)) + + # cast to full n_bits values + X = BVUnsignedUpCast(X_short, n_bits) + Y = BVUnsignedUpCast(Y_short, n_bits) + + # Constants + maxValue = BVUnsignedMax(type_bits, n_bits) + + # Overflow check in YulUtilFunction::overflowCheckedIntAddFunction + overflow_check = GT(X, SUB(maxValue, Y)) + + rule.check(overflow_check != 0, actual_overflow) + + type_bits *= 2 diff --git a/test/formal/checked_uint_mul_16.py b/test/formal/checked_uint_mul_16.py new file mode 100644 index 000000000..6e8901799 --- /dev/null +++ b/test/formal/checked_uint_mul_16.py @@ -0,0 +1,36 @@ +from rule import Rule +from opcodes import * +from util import * + +""" +Overflow checked unsigned integer multiplication. +""" + +# Approximation with 16-bit base types. +n_bits = 16 +type_bits = 8 + +while type_bits <= n_bits: + + rule = Rule() + + # Input vars + X_short = BitVec('X', type_bits) + Y_short = BitVec('Y', type_bits) + + # Z3's overflow condition + actual_overflow = Not(BVMulNoOverflow(X_short, Y_short, False)) + + # cast to full n_bits values + X = BVUnsignedUpCast(X_short, n_bits) + Y = BVUnsignedUpCast(Y_short, n_bits) + + # Constants + maxValue = BVUnsignedMax(type_bits, n_bits) + + # Overflow check in YulUtilFunction::overflowCheckedIntMulFunction + overflow_check = AND(ISZERO(ISZERO(X)), GT(Y, DIV(maxValue, X))) + + rule.check(overflow_check != 0, actual_overflow) + + type_bits *= 2 diff --git a/test/formal/checked_uint_sub.py b/test/formal/checked_uint_sub.py new file mode 100644 index 000000000..b0f25b582 --- /dev/null +++ b/test/formal/checked_uint_sub.py @@ -0,0 +1,35 @@ +from rule import Rule +from opcodes import * +from util import * + +""" +Overflow checked unsigned integer subtraction. +""" + +n_bits = 256 +type_bits = 8 + +while type_bits <= n_bits: + + rule = Rule() + + # Input vars + X_short = BitVec('X', type_bits) + Y_short = BitVec('Y', type_bits) + + # Z3's overflow condition + actual_overflow = Not(BVSubNoUnderflow(X_short, Y_short, False)) + + # cast to full n_bits values + X = BVUnsignedUpCast(X_short, n_bits) + Y = BVUnsignedUpCast(Y_short, n_bits) + + # Constants + maxValue = BVUnsignedMax(type_bits, n_bits) + + # Overflow check in YulUtilFunction::overflowCheckedIntSubFunction + overflow_check = LT(X, Y) + + rule.check(overflow_check != 0, actual_overflow) + + type_bits *= 2 diff --git a/test/formal/opcodes.py b/test/formal/opcodes.py index ca6282f70..cdd60ddae 100644 --- a/test/formal/opcodes.py +++ b/test/formal/opcodes.py @@ -33,6 +33,9 @@ def SLT(x, y): def SGT(x, y): return If(x > y, BitVecVal(1, x.size()), BitVecVal(0, x.size())) +def EQ(x, y): + return If(x == y, BitVecVal(1, x.size()), BitVecVal(0, x.size())) + def ISZERO(x): return If(x == 0, BitVecVal(1, x.size()), BitVecVal(0, x.size())) diff --git a/test/formal/util.py b/test/formal/util.py new file mode 100644 index 000000000..ec98f9c81 --- /dev/null +++ b/test/formal/util.py @@ -0,0 +1,27 @@ +from z3 import * + +def BVUnsignedUpCast(x, n_bits): + assert(x.size() <= n_bits) + if x.size() < n_bits: + return Concat(BitVecVal(0, n_bits - x.size()), x) + else: + return x + +def BVUnsignedMax(type_bits, n_bits): + assert(type_bits <= n_bits) + return BitVecVal((1 << type_bits) - 1, n_bits) + +def BVSignedUpCast(x, n_bits): + assert(x.size() <= n_bits) + if x.size() < n_bits: + return Concat(If(x < 0, BitVecVal(-1, n_bits - x.size()), BitVecVal(0, n_bits - x.size())), x) + else: + return x + +def BVSignedMax(type_bits, n_bits): + assert(type_bits <= n_bits) + return BitVecVal((1 << (type_bits - 1)) - 1, n_bits) + +def BVSignedMin(type_bits, n_bits): + assert(type_bits <= n_bits) + return BitVecVal(-(1 << (type_bits - 1)), n_bits)