From 5089d4ac28259fb48ae7840aca4867f9afda336d Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 13 Jun 2019 16:43:11 +0200 Subject: [PATCH] Move optimization proofs repo to Solidity repo --- test/formal/README.md | 6 +++ test/formal/combine_div_shl_one_32.py | 27 +++++++++++ test/formal/combine_mul_shl_one_64.py | 33 +++++++++++++ test/formal/combine_shl_shr_by_constant_64.py | 44 ++++++++++++++++++ test/formal/combine_shr_shl_by_constant_64.py | 44 ++++++++++++++++++ test/formal/move_and_across_shl_128.py | 36 +++++++++++++++ test/formal/move_and_across_shr_128.py | 36 +++++++++++++++ test/formal/opcodes.py | 46 +++++++++++++++++++ test/formal/rule.py | 38 +++++++++++++++ test/formal/shl_workaround_8.py | 27 +++++++++++ 10 files changed, 337 insertions(+) create mode 100644 test/formal/README.md create mode 100644 test/formal/combine_div_shl_one_32.py create mode 100644 test/formal/combine_mul_shl_one_64.py create mode 100644 test/formal/combine_shl_shr_by_constant_64.py create mode 100644 test/formal/combine_shr_shl_by_constant_64.py create mode 100644 test/formal/move_and_across_shl_128.py create mode 100644 test/formal/move_and_across_shr_128.py create mode 100644 test/formal/opcodes.py create mode 100644 test/formal/rule.py create mode 100644 test/formal/shl_workaround_8.py diff --git a/test/formal/README.md b/test/formal/README.md new file mode 100644 index 000000000..83bd79e76 --- /dev/null +++ b/test/formal/README.md @@ -0,0 +1,6 @@ +The Solidity compiler implements several [optimization rules](https://github.com/ethereum/solidity/blob/develop/libevmasm/RuleList.h). + +This directory contains an effort to formally prove the correctness of those rules in: + +- HOL with [EthIsabelle](https://github.com/ekpyron/eth-isabelle) +- FOL with SMT solvers using [Integers and BitVectors](http://smtlib.cs.uiowa.edu/theories.shtml) diff --git a/test/formal/combine_div_shl_one_32.py b/test/formal/combine_div_shl_one_32.py new file mode 100644 index 000000000..23c65c8d7 --- /dev/null +++ b/test/formal/combine_div_shl_one_32.py @@ -0,0 +1,27 @@ +from rule import Rule +from opcodes import * + +""" +Rule: +DIV(X, SHL(Y, 1)) -> SHR(Y, X) +Requirements: +""" + +rule = Rule() + +n_bits = 32 + +# Input vars +X = BitVec('X', n_bits) +Y = BitVec('Y', n_bits) + +# Constants +ONE = BitVecVal(1, n_bits) + +# Non optimized result +nonopt = DIV(X, SHL(Y, ONE)) + +# Optimized result +opt = SHR(Y, X) + +rule.check(nonopt, opt) diff --git a/test/formal/combine_mul_shl_one_64.py b/test/formal/combine_mul_shl_one_64.py new file mode 100644 index 000000000..6f87cfcdb --- /dev/null +++ b/test/formal/combine_mul_shl_one_64.py @@ -0,0 +1,33 @@ +from rule import Rule +from opcodes import * + +""" +Rule: +MUL(X, SHL(Y, 1)) -> SHL(Y, X) +MUL(SHL(X, 1), Y) -> SHL(X, Y) +Requirements: +""" + +rule = Rule() + +n_bits = 64 + +# Input vars +X = BitVec('X', n_bits) +Y = BitVec('Y', n_bits) + +# Constants +ONE = BitVecVal(1, n_bits) + +# Requirements + +# Non optimized result +nonopt_1 = MUL(X, SHL(Y, ONE)) +nonopt_2 = MUL(SHL(X, ONE), Y) + +# Optimized result +opt_1 = SHL(Y, X) +opt_2 = SHL(X, Y) + +rule.check(nonopt_1, opt_1) +rule.check(nonopt_2, opt_2) diff --git a/test/formal/combine_shl_shr_by_constant_64.py b/test/formal/combine_shl_shr_by_constant_64.py new file mode 100644 index 000000000..fc7ec64e8 --- /dev/null +++ b/test/formal/combine_shl_shr_by_constant_64.py @@ -0,0 +1,44 @@ +from rule import Rule +from opcodes import * + +""" +Rule: +mask = shlWorkaround(u256(-1), unsigned(A.d())) >> unsigned(B.d()) +SHR(B, SHL(A, X)) -> AND(SH[L/R]([B - A / A - B], X), Mask) +Requirements: +A < BitWidth +B < BitWidth +""" + +rule = Rule() + +n_bits = 64 + +# Input vars +X = BitVec('X', n_bits) +A = BitVec('A', n_bits) +B = BitVec('B', n_bits) + +# Constants +BitWidth = BitVecVal(n_bits, n_bits) + +# Requirements +rule.require(ULT(A, BitWidth)) +rule.require(ULT(B, BitWidth)) + +# Non optimized result +nonopt = SHR(B, SHL(A, X)) + +# Optimized result +Mask = SHR(B, SHL(A, Int2BV(IntVal(-1), n_bits))) +opt = If( + UGT(A, B), + AND(SHL(A - B, X), Mask), + If( + UGT(B, A), + AND(SHR(B - A, X), Mask), + AND(X, Mask) + ) + ) + +rule.check(nonopt, opt) diff --git a/test/formal/combine_shr_shl_by_constant_64.py b/test/formal/combine_shr_shl_by_constant_64.py new file mode 100644 index 000000000..31aa60956 --- /dev/null +++ b/test/formal/combine_shr_shl_by_constant_64.py @@ -0,0 +1,44 @@ +from rule import Rule +from opcodes import * + +""" +Rule: +mask = shlWorkaround(u256(-1) >> unsigned(A.d()), unsigned(B.d())) +SHL(B, SHR(A, X)) -> AND(SH[L/R]([B - A / A - B], X), Mask) +Requirements: +A < BitWidth +B < BitWidth +""" + +rule = Rule() + +n_bits = 64 + +# Input vars +X = BitVec('X', n_bits) +A = BitVec('A', n_bits) +B = BitVec('B', n_bits) + +# Constants +BitWidth = BitVecVal(n_bits, n_bits) + +# Requirements +rule.require(ULT(A, BitWidth)) +rule.require(ULT(B, BitWidth)) + +# Non optimized result +nonopt = SHL(B, SHR(A, X)) + +# Optimized result +Mask = SHL(B, SHR(A, Int2BV(IntVal(-1), n_bits))) +opt = If( + UGT(A, B), + AND(SHR(a - b, x), Mask), + If( + UGT(B, A), + AND(SHL(B - A, X), Mask), + AND(X, Mask) + ) + ) + +rule.check(nonopt, opt) diff --git a/test/formal/move_and_across_shl_128.py b/test/formal/move_and_across_shl_128.py new file mode 100644 index 000000000..d3f5c3a66 --- /dev/null +++ b/test/formal/move_and_across_shl_128.py @@ -0,0 +1,36 @@ +from rule import Rule +from opcodes import * + +""" +Rule: +SHL(B, AND(X, A)) -> AND(SHL(B, X), A << B) +SHL(B, AND(A, X)) -> AND(SHL(B, X), A << B) +Requirements: +B < BitWidth +""" + +rule = Rule() + +n_bits = 128 + +# Input vars +X = BitVec('X', n_bits) +A = BitVec('A', n_bits) +B = BitVec('B', n_bits) + +# Constants +BitWidth = BitVecVal(n_bits, n_bits) + +# Requirements +rule.require(ULT(B, BitWidth)) + +# Non optimized result +nonopt_1 = SHL(B, AND(X, A)) +nonopt_2 = SHL(B, AND(A, X)) + +# Optimized result +Mask = SHL(B, A) +opt = AND(SHL(B, X), Mask) + +rule.check(nonopt_1, opt) +rule.check(nonopt_2, opt) diff --git a/test/formal/move_and_across_shr_128.py b/test/formal/move_and_across_shr_128.py new file mode 100644 index 000000000..df673ff59 --- /dev/null +++ b/test/formal/move_and_across_shr_128.py @@ -0,0 +1,36 @@ +from rule import Rule +from opcodes import * + +""" +Rule: +SHR(B, AND(X, A)) -> AND(SHR(B, X), A >> B) +SHR(B, AND(A, X)) -> AND(SHR(B, X), A >> B) +Requirements: +B < BitWidth +""" + +rule = Rule() + +n_bits = 128 + +# Input vars +X = BitVec('X', n_bits) +A = BitVec('A', n_bits) +B = BitVec('B', n_bits) + +# Constants +BitWidth = BitVecVal(n_bits, n_bits) + +# Requirements +rule.require(ULT(B, BitWidth)) + +# Non optimized result +nonopt_1 = SHR(B, AND(X, A)); +nonopt_2 = SHR(B, AND(A, X)); + +# Optimized result +Mask = SHR(B, A); +opt = AND(SHR(B, X), Mask); + +rule.check(nonopt_1, opt) +rule.check(nonopt_2, opt) diff --git a/test/formal/opcodes.py b/test/formal/opcodes.py new file mode 100644 index 000000000..faa9de1d9 --- /dev/null +++ b/test/formal/opcodes.py @@ -0,0 +1,46 @@ +from z3 import * + +def ADD(x, y): + return x + y + +def MUL(x, y): + return x * y + +def SUB(x, y): + return x - y + +def DIV(x, y): + return If(y == 0, 0, UDiv(x, y)) + +def SDIV(x, y): + return If(y == 0, 0, x / y) + +def MOD(x, y): + return If(y == 0, 0, URem(x, y)) + +def SMOD(x, y): + return If(y == 0, 0, x % y) + +def LT(x, y): + return ULT(x, y) + +def GT(x, y): + return UGT(x, y) + +def SLT(x, y): + return x < y + +def SGT(x, y): + return x > y + +def AND(x, y): + return x & y + +def SHL(x, y): + return y << x + +def SHR(x, y): + return LShR(y, x) + +def SAR(x, y): + return y >> x diff --git a/test/formal/rule.py b/test/formal/rule.py new file mode 100644 index 000000000..e434fcb3f --- /dev/null +++ b/test/formal/rule.py @@ -0,0 +1,38 @@ +from z3 import * + +class Rule: + def __init__(self): + self.requirements = [] + self.constraints = [] + self.solver = Solver() + self.setTimeout(60000) + + def setTimeout(self, _t): + self.solver.set("timeout", _t) + + def __lshift__(self, _c): + self.constraints.append(_c) + + def require(self, _r): + self.requirements.append(_r) + + def check(self, _nonopt, _opt): + self.solver.add(self.requirements) + result = self.solver.check() + + if result == unknown: + raise BaseException('Unable to satisfy requirements.') + elif result == unsat: + raise BaseException('Requirements are unsatisfiable.') + + self.solver.push() + self.solver.add(self.constraints) + self.solver.add(_nonopt != _opt) + + result = self.solver.check() + if result == unknown: + raise BaseException('Unable to prove rule.') + elif result == sat: + m = self.solver.model() + raise BaseException('Rule is incorrect.\nModel: ' + str(m)) + self.solver.pop() diff --git a/test/formal/shl_workaround_8.py b/test/formal/shl_workaround_8.py new file mode 100644 index 000000000..2ca711cdf --- /dev/null +++ b/test/formal/shl_workaround_8.py @@ -0,0 +1,27 @@ +from rule import Rule +from opcodes import * + +""" +Shift left workaround that Solidity implements +due to a bug in Boost. +""" + +rule = Rule() + +n_bits = 8 +bigint_bits = 16 + +# Input vars +X = BitVec('X', n_bits) +A = BitVec('A', n_bits) +B = BitVec('B', bigint_bits) + +# Compute workaround +workaround = Int2BV( + BV2Int( + (Int2BV(BV2Int(X), bigint_bits) << Int2BV(BV2Int(A), bigint_bits)) & + Int2BV(BV2Int(Int2BV(IntVal(-1), n_bits)), bigint_bits) + ), n_bits +) + +rule.check(workaround, SHL(A, X))