test/formal: Get rid of wildcard imports

test/formal/byte_big.py

@@ -1,5 +1,6 @@
+from opcodes import BYTE
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 byte(A, X) -> 0

test/formal/byte_equivalence.py

@@ -1,5 +1,6 @@
+from opcodes import BYTE
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, Concat, Extract
 
 """
 Checks that the byte opcode (implemented using shift) is equivalent to a

test/formal/checked_int_add.py

@@ -1,6 +1,7 @@
+from opcodes import AND, ISZERO, SGT, SLT, SUB
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVSignedMax, BVSignedMin, BVSignedUpCast
+from z3 import BitVec, BVAddNoOverflow, BVAddNoUnderflow, Not
 
 """
 Overflow checked signed integer addition.

test/formal/checked_int_div.py

@@ -1,6 +1,7 @@
+from opcodes import AND, EQ, SUB
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVSignedMin, BVSignedUpCast
+from z3 import BitVec, BVSDivNoOverflow, Not
 
 """
 Overflow checked signed integer division.

test/formal/checked_int_mul_16.py

@@ -1,6 +1,7 @@
+from opcodes import AND, DIV, GT, SDIV, SGT, SLT
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVSignedMax, BVSignedMin, BVSignedUpCast
+from z3 import BVMulNoOverflow, BVMulNoUnderflow, BitVec, Not, Or
 
 """
 Overflow checked signed integer multiplication.

test/formal/checked_int_sub.py

@@ -1,6 +1,7 @@
+from opcodes import AND, ADD, ISZERO, SLT, SGT
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVSignedMax, BVSignedMin, BVSignedUpCast
+from z3 import BitVec, BVSubNoOverflow, BVSubNoUnderflow, Not
 
 """
 Overflow checked signed integer subtraction.

test/formal/checked_uint_add.py

@@ -1,6 +1,7 @@
+from opcodes import GT, SUB
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVUnsignedMax, BVUnsignedUpCast
+from z3 import BitVec, BVAddNoOverflow, Not
 
 """
 Overflow checked unsigned integer addition.

test/formal/checked_uint_mul_16.py

@@ -1,6 +1,7 @@
+from opcodes import AND, ISZERO, GT, DIV
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVUnsignedUpCast, BVUnsignedMax
+from z3 import BitVec, Not, BVMulNoOverflow
 
 """
 Overflow checked unsigned integer multiplication.

test/formal/checked_uint_sub.py

@@ -1,6 +1,7 @@
+from opcodes import LT
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVUnsignedMax, BVUnsignedUpCast
+from z3 import BVSubNoUnderflow, BitVec, Not
 
 """
 Overflow checked unsigned integer subtraction.

test/formal/combine_byte_shl.py

@@ -1,5 +1,6 @@
+from opcodes import BYTE, SHL
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, ULE
 
 """
 byte(A, shl(B, X))

test/formal/combine_byte_shr_1.py

@@ -1,5 +1,6 @@
+from opcodes import BYTE, DIV, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, UGE, ULE, ULT
 
 """
 byte(A, shr(B, X))

test/formal/combine_byte_shr_2.py

@@ -1,5 +1,6 @@
+from opcodes import BYTE, SHR, DIV
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, ULT
 
 """
 byte(A, shr(B, X))

test/formal/combine_div_shl_one_32.py

@@ -1,5 +1,6 @@
+from opcodes import DIV, SHL, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rule:

test/formal/combine_mul_shl_one_64.py

@@ -1,5 +1,6 @@
+from opcodes import SHL, MUL
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rule:

test/formal/combine_shl_shr_by_constant_64.py

@@ -1,5 +1,6 @@
+from opcodes import AND, SHL, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, If, Int2BV, IntVal, UGT, ULT
 
 """
 Rule:

test/formal/combine_shr_shl_by_constant_64.py

@@ -1,5 +1,6 @@
+from opcodes import AND, SHL, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, If, Int2BV, IntVal, UGT, ULT
 
 """
 Rule:

test/formal/eq_sub.py

@@ -1,5 +1,6 @@
+from opcodes import EQ, ISZERO, SUB
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rule:

test/formal/exp_neg_one.py

@@ -1,6 +1,7 @@
+from opcodes import AND, ISZERO, MOD, SUB
 from rule import Rule
-from opcodes import *
-from util import *
+from util import BVUnsignedMax
+from z3 import BitVec, BitVecVal, If
 
 """
 Checking conversion of exp(-1, X) to sub(isZero(and(X, 1)), and(X, 1))

test/formal/exp_to_shl.py

@@ -1,6 +1,6 @@
+from opcodes import SHL
 from rule import Rule
-from opcodes import *
-from util import *
+from z3 import BitVec, If
 
 """
 Checking conversion of exp(2, X) to shl(X, 1)

test/formal/move_and_across_shl_128.py

@@ -1,5 +1,6 @@
+from opcodes import AND, SHL
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, ULT
 
 """
 Rule:

test/formal/move_and_across_shr_128.py

@@ -1,5 +1,6 @@
+from opcodes import AND, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, ULT
 
 """
 Rule:

test/formal/move_and_inside_or.py

@@ -1,5 +1,7 @@
+from opcodes import AND, OR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
+
 
 """
 Rule:

test/formal/opcodes.py

@@ -1,4 +1,4 @@
-from z3 import *
+from z3 import BitVecVal, BV2Int, If, LShR, UDiv, ULT, UGT, URem
 
 def ADD(x, y):
 	return x + y

test/formal/repeated_and.py

@@ -1,5 +1,6 @@
+from opcodes import AND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal
 
 """
 Rule:

test/formal/repeated_or.py

@@ -1,5 +1,6 @@
+from opcodes import OR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal
 
 """
 Rule:

test/formal/replace_mul_by_shift.py

@@ -1,5 +1,6 @@
+from opcodes import DIV, MUL, SHL, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rule:

test/formal/rule.py

@@ -1,6 +1,6 @@
 import sys
 
-from z3 import *
+from z3 import sat, Solver, unknown, unsat
 
 class Rule:
 	def __init__(self):

test/formal/shl_workaround_8.py

@@ -1,5 +1,6 @@
+from opcodes import SHL
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BV2Int, Int2BV, IntVal
 
 """
 Shift left workaround that Solidity implements

test/formal/signextend.py

@@ -1,5 +1,6 @@
+from opcodes import SIGNEXTEND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, If, UGE, ULT
 
 """
 Rule:

test/formal/signextend_and.py

@@ -1,5 +1,6 @@
+from opcodes import SIGNEXTEND, AND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, ULT
 
 """
 Rule:

test/formal/signextend_equivalence.py

@@ -1,5 +1,6 @@
+from opcodes import SIGNEXTEND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal, Extract, SignExt, UGT
 
 """
 Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract

test/formal/signextend_shl.py

@@ -1,5 +1,6 @@
+from opcodes import SHL, SIGNEXTEND
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, LShR, ULE
 
 """
 Rule:

test/formal/signextend_shr.py

@@ -1,5 +1,6 @@
+from opcodes import SIGNEXTEND, SAR, SHR
 from rule import Rule
-from opcodes import *
+from z3 import BitVec,  BitVecVal, ULE
 
 """
 Rule:

test/formal/sub_not_zero_x_to_not_x_256.py

@@ -1,5 +1,6 @@
+from opcodes import NOT, SUB
 from rule import Rule
-from opcodes import *
+from z3 import BitVec, BitVecVal
 
 """
 Rule:

test/formal/sub_sub.py

@@ -1,5 +1,6 @@
+from opcodes import ADD, SUB
 from rule import Rule
-from opcodes import *
+from z3 import BitVec
 
 """
 Rules:

test/formal/util.py

@@ -1,4 +1,4 @@
-from z3 import *
+from z3 import BitVecVal, Concat, If
 
 def BVUnsignedUpCast(x, n_bits):
 	assert x.size() <= n_bits