diff --git a/scripts/bytecodecompare/prepare_report.py b/scripts/bytecodecompare/prepare_report.py index 33463f198..9d35b9988 100755 --- a/scripts/bytecodecompare/prepare_report.py +++ b/scripts/bytecodecompare/prepare_report.py @@ -413,7 +413,7 @@ def commandline_parser() -> ArgumentParser: action='store_true', help="Immediately exit and print compiler output if the compiler exits with an error.", ) - return parser; + return parser if __name__ == "__main__": diff --git a/scripts/endToEndExtraction/remove-testcases.py b/scripts/endToEndExtraction/remove-testcases.py index b1dc75b6c..28822e044 100755 --- a/scripts/endToEndExtraction/remove-testcases.py +++ b/scripts/endToEndExtraction/remove-testcases.py @@ -39,7 +39,7 @@ def colorize(left, right, id): reset = "\x1b[0m" colors = [red, yellow] color = colors[id % len(colors)] - function, arguments, results = parse_call(right) + function, _arguments, _results = parse_call(right) left = left.replace("compileAndRun", color + "compileAndRun" + reset) right = right.replace("constructor", color + "constructor" + reset) if function: @@ -158,7 +158,7 @@ def main(argv): interactive = False input_file = None try: - opts, args = getopt.getopt(argv, "if:") + opts, _args = getopt.getopt(argv, "if:") except getopt.GetoptError: print("./remove-testcases.py [-i] [-f ]") sys.exit(1) diff --git a/scripts/endToEndExtraction/verify-testcases.py b/scripts/endToEndExtraction/verify-testcases.py index c86a993dc..8e1c60a79 100755 --- a/scripts/endToEndExtraction/verify-testcases.py +++ b/scripts/endToEndExtraction/verify-testcases.py @@ -158,7 +158,7 @@ class TraceAnalyser: for trace_id, trace in enumerate(left.traces): left_trace = trace right_trace = right.traces[trace_id] - assert (left_trace.kind == right_trace.kind) + assert left_trace.kind == right_trace.kind if str(left_trace) != str(right_trace): mismatch_info = " " + str(left_trace) + "\n" mismatch_info += " " + str(right_trace) + "\n" @@ -179,7 +179,7 @@ def main(argv): extracted_tests_trace_file = None end_to_end_trace_file = None try: - opts, args = getopt.getopt(argv, "s:e:") + opts, _args = getopt.getopt(argv, "s:e:") except getopt.GetoptError: print("verify-testcases.py [-s ] [-e ]") sys.exit(2) diff --git a/scripts/error_codes.py b/scripts/error_codes.py index 8d919e41b..9290211a2 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -261,9 +261,9 @@ def main(argv): no_confirm = False examine_coverage = False next_id = False - opts, args = getopt.getopt(argv, "", ["check", "fix", "no-confirm", "examine-coverage", "next"]) + opts, _args = getopt.getopt(argv, "", ["check", "fix", "no-confirm", "examine-coverage", "next"]) - for opt, arg in opts: + for opt, _arg in opts: if opt == "--check": check = True elif opt == "--fix": diff --git a/scripts/fix_homebrew_paths_in_standalone_zip.py b/scripts/fix_homebrew_paths_in_standalone_zip.py index 95120f760..43f26795c 100755 --- a/scripts/fix_homebrew_paths_in_standalone_zip.py +++ b/scripts/fix_homebrew_paths_in_standalone_zip.py @@ -49,9 +49,10 @@ def readDependencies(fname): if line[0] == '\t': library = line.split(' ', 1)[0][1:] if (library.startswith("/usr/local/lib") or - library.startswith("/usr/local/opt") or - library.startswith("/Users/")): - if (os.path.basename(library) != os.path.basename(fname)): + library.startswith("/usr/local/opt") or + library.startswith("/Users/") + ): + if os.path.basename(library) != os.path.basename(fname): command = "install_name_tool -change " + \ library + " @executable_path/./" + \ os.path.basename(library) + " " + fname diff --git a/scripts/gas_diff_stats.py b/scripts/gas_diff_stats.py index 1e86e2836..5c7aa5338 100644 --- a/scripts/gas_diff_stats.py +++ b/scripts/gas_diff_stats.py @@ -20,7 +20,7 @@ repository. The changes are compared against ``origin/develop``. import subprocess from pathlib import Path from enum import Enum -from parsec import * +from parsec import generate, ParseError, regex, string from tabulate import tabulate class Kind(Enum): @@ -56,10 +56,10 @@ def diff_string() -> (Kind, Diff, int): -// gas irOptimized: 138070 """ - diff_kind = yield (minus | plus) + diff_kind = yield minus | plus yield comment yield space - codegen_kind = yield (gas_ir_optimized ^ gas_legacy_optimized ^ gas_legacy) + codegen_kind = yield gas_ir_optimized ^ gas_legacy_optimized ^ gas_legacy yield colon yield space val = yield number() diff --git a/scripts/isolate_tests.py b/scripts/isolate_tests.py index 93cf2755c..1e2170e82 100755 --- a/scripts/isolate_tests.py +++ b/scripts/isolate_tests.py @@ -6,7 +6,6 @@ # into files for e.g. fuzz testing as # scripts/isolate_tests.py test/libsolidity/* -import sys import re import os import hashlib diff --git a/scripts/pylint_all.py b/scripts/pylint_all.py index 7b8924b8a..8dbe6a7fc 100755 --- a/scripts/pylint_all.py +++ b/scripts/pylint_all.py @@ -9,7 +9,6 @@ from os import path, walk from sys import exit from textwrap import dedent import subprocess -import sys PROJECT_ROOT = path.dirname(path.dirname(path.realpath(__file__))) PYLINT_RCFILE = f"{PROJECT_ROOT}/scripts/pylintrc" diff --git a/scripts/pylintrc b/scripts/pylintrc index ed63c9256..50dbebee0 100644 --- a/scripts/pylintrc +++ b/scripts/pylintrc @@ -24,24 +24,15 @@ disable= duplicate-code, invalid-name, missing-docstring, - mixed-indentation, no-else-return, no-self-use, pointless-string-statement, redefined-builtin, redefined-outer-name, singleton-comparison, - superfluous-parens, too-few-public-methods, - trailing-newlines, - undefined-variable, - ungrouped-imports, - unnecessary-semicolon, - unused-import, - unused-variable, - unused-wildcard-import, - useless-object-inheritance, - wildcard-import + too-many-public-methods, + ungrouped-imports [BASIC] diff --git a/scripts/regressions.py b/scripts/regressions.py index 1efbb48b5..046044197 100755 --- a/scripts/regressions.py +++ b/scripts/regressions.py @@ -11,7 +11,7 @@ import time DESCRIPTION = """Regressor is a tool to run regression tests in a CI env.""" -class PrintDotsThread(object): +class PrintDotsThread: """Prints a dot every "interval" (default is 300) seconds""" def __init__(self, interval=300): @@ -30,7 +30,7 @@ class PrintDotsThread(object): print(".") time.sleep(self.interval) -class regressor(): +class regressor: _re_sanitizer_log = re.compile(r"""ERROR: (libFuzzer|UndefinedBehaviorSanitizer)""") def __init__(self, description, args): diff --git a/scripts/splitSources.py b/scripts/splitSources.py index 3d1c8ef45..181741f9c 100755 --- a/scripts/splitSources.py +++ b/scripts/splitSources.py @@ -44,9 +44,7 @@ def writeSourceToFile(lines): os.system("mkdir -p " + filePath) with open(srcName, mode='a+', encoding='utf8', newline='') as f: createdSources.append(srcName) - i = 0 for idx, line in enumerate(lines[1:]): - # write to file if line[:12] != "==== Source:": f.write(line) diff --git a/scripts/wasm-rebuild/docker-scripts/isolate_tests.py b/scripts/wasm-rebuild/docker-scripts/isolate_tests.py index 635ebcc31..c447c1e67 100755 --- a/scripts/wasm-rebuild/docker-scripts/isolate_tests.py +++ b/scripts/wasm-rebuild/docker-scripts/isolate_tests.py @@ -7,7 +7,8 @@ import sys import re import os import hashlib -from os.path import join, isfile +# Pylint for some reason insists that isfile() is unused +from os.path import join, isfile # pylint: disable=unused-import def extract_test_cases(path): diff --git a/test/formal/byte_big.py b/test/formal/byte_big.py index db11bc998..8e6dfd7ef 100644 --- a/test/formal/byte_big.py +++ b/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 diff --git a/test/formal/byte_equivalence.py b/test/formal/byte_equivalence.py index 0f3638424..c607eca4c 100644 --- a/test/formal/byte_equivalence.py +++ b/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 diff --git a/test/formal/checked_int_add.py b/test/formal/checked_int_add.py index 6e74944e2..43368a98d 100644 --- a/test/formal/checked_int_add.py +++ b/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. diff --git a/test/formal/checked_int_div.py b/test/formal/checked_int_div.py index 2a36a9488..4c9d4e829 100644 --- a/test/formal/checked_int_div.py +++ b/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. diff --git a/test/formal/checked_int_mul_16.py b/test/formal/checked_int_mul_16.py index cc8743b1d..b2f9eb852 100644 --- a/test/formal/checked_int_mul_16.py +++ b/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. diff --git a/test/formal/checked_int_sub.py b/test/formal/checked_int_sub.py index 72a0a2109..ed292bbe0 100644 --- a/test/formal/checked_int_sub.py +++ b/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. diff --git a/test/formal/checked_uint_add.py b/test/formal/checked_uint_add.py index 596fa04f0..e38b4dcdb 100644 --- a/test/formal/checked_uint_add.py +++ b/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. diff --git a/test/formal/checked_uint_mul_16.py b/test/formal/checked_uint_mul_16.py index 6e8901799..1c60de47b 100644 --- a/test/formal/checked_uint_mul_16.py +++ b/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. diff --git a/test/formal/checked_uint_sub.py b/test/formal/checked_uint_sub.py index b0f25b582..65bcf74a4 100644 --- a/test/formal/checked_uint_sub.py +++ b/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. diff --git a/test/formal/combine_byte_shl.py b/test/formal/combine_byte_shl.py index e2a6034ff..f492cc18f 100644 --- a/test/formal/combine_byte_shl.py +++ b/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)) diff --git a/test/formal/combine_byte_shr_1.py b/test/formal/combine_byte_shr_1.py index 4938e73f7..788319aa2 100644 --- a/test/formal/combine_byte_shr_1.py +++ b/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)) diff --git a/test/formal/combine_byte_shr_2.py b/test/formal/combine_byte_shr_2.py index 4f9be05a4..d969c301b 100644 --- a/test/formal/combine_byte_shr_2.py +++ b/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)) diff --git a/test/formal/combine_div_shl_one_32.py b/test/formal/combine_div_shl_one_32.py index 2ee7d2137..5cca7288b 100644 --- a/test/formal/combine_div_shl_one_32.py +++ b/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: diff --git a/test/formal/combine_mul_shl_one_64.py b/test/formal/combine_mul_shl_one_64.py index 44d031b98..169cc5be0 100644 --- a/test/formal/combine_mul_shl_one_64.py +++ b/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: diff --git a/test/formal/combine_shl_shr_by_constant_64.py b/test/formal/combine_shl_shr_by_constant_64.py index fc7ec64e8..4d8e6a1f8 100644 --- a/test/formal/combine_shl_shr_by_constant_64.py +++ b/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: diff --git a/test/formal/combine_shr_shl_by_constant_64.py b/test/formal/combine_shr_shl_by_constant_64.py index c011a2616..5bc852574 100644 --- a/test/formal/combine_shr_shl_by_constant_64.py +++ b/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: diff --git a/test/formal/eq_sub.py b/test/formal/eq_sub.py index bf7518acf..76808bc3b 100644 --- a/test/formal/eq_sub.py +++ b/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: diff --git a/test/formal/exp_neg_one.py b/test/formal/exp_neg_one.py index 88416496e..4dffb88b0 100644 --- a/test/formal/exp_neg_one.py +++ b/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)) diff --git a/test/formal/exp_to_shl.py b/test/formal/exp_to_shl.py index 064d1af3e..499cf7c2f 100644 --- a/test/formal/exp_to_shl.py +++ b/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) diff --git a/test/formal/move_and_across_shl_128.py b/test/formal/move_and_across_shl_128.py index d3f5c3a66..9e689b71e 100644 --- a/test/formal/move_and_across_shl_128.py +++ b/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: diff --git a/test/formal/move_and_across_shr_128.py b/test/formal/move_and_across_shr_128.py index df673ff59..592dc7742 100644 --- a/test/formal/move_and_across_shr_128.py +++ b/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: @@ -25,12 +26,12 @@ BitWidth = BitVecVal(n_bits, n_bits) rule.require(ULT(B, BitWidth)) # Non optimized result -nonopt_1 = SHR(B, AND(X, A)); -nonopt_2 = SHR(B, AND(A, X)); +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); +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/move_and_inside_or.py b/test/formal/move_and_inside_or.py index 09dc35c51..48ec20dba 100644 --- a/test/formal/move_and_inside_or.py +++ b/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: diff --git a/test/formal/opcodes.py b/test/formal/opcodes.py index 6098d01ed..103e57a14 100644 --- a/test/formal/opcodes.py +++ b/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 diff --git a/test/formal/repeated_and.py b/test/formal/repeated_and.py index 2e8431b3c..2376ca34f 100644 --- a/test/formal/repeated_and.py +++ b/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: diff --git a/test/formal/repeated_or.py b/test/formal/repeated_or.py index c1b2ebd09..ba18e39aa 100644 --- a/test/formal/repeated_or.py +++ b/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: diff --git a/test/formal/replace_mul_by_shift.py b/test/formal/replace_mul_by_shift.py index 5a2c2dc14..3805af0dc 100644 --- a/test/formal/replace_mul_by_shift.py +++ b/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: diff --git a/test/formal/rule.py b/test/formal/rule.py index 9327f7e5a..ac0f0c8a6 100644 --- a/test/formal/rule.py +++ b/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): diff --git a/test/formal/shl_workaround_8.py b/test/formal/shl_workaround_8.py index 2ca711cdf..19248574a 100644 --- a/test/formal/shl_workaround_8.py +++ b/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 diff --git a/test/formal/signextend.py b/test/formal/signextend.py index 32d374261..ed285345d 100644 --- a/test/formal/signextend.py +++ b/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: @@ -34,4 +35,3 @@ rule3.check( SIGNEXTEND(A, SIGNEXTEND(B, X)), SIGNEXTEND(If(ULT(A, B), A, B), X) ) - diff --git a/test/formal/signextend_and.py b/test/formal/signextend_and.py index ae2b4bd2c..91fc14349 100644 --- a/test/formal/signextend_and.py +++ b/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: diff --git a/test/formal/signextend_equivalence.py b/test/formal/signextend_equivalence.py index 1199fff47..3b8386e54 100644 --- a/test/formal/signextend_equivalence.py +++ b/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 diff --git a/test/formal/signextend_shl.py b/test/formal/signextend_shl.py index 608b10eec..18b1baea1 100644 --- a/test/formal/signextend_shl.py +++ b/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: diff --git a/test/formal/signextend_shr.py b/test/formal/signextend_shr.py index 4364e6a23..a763314cd 100644 --- a/test/formal/signextend_shr.py +++ b/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: @@ -28,4 +29,3 @@ rule.check( SIGNEXTEND(A, SHR(B, X)), SAR(B, X) ) - diff --git a/test/formal/sub_not_zero_x_to_not_x_256.py b/test/formal/sub_not_zero_x_to_not_x_256.py index eb3301100..d8f1282ec 100644 --- a/test/formal/sub_not_zero_x_to_not_x_256.py +++ b/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: diff --git a/test/formal/sub_sub.py b/test/formal/sub_sub.py index d6099c91f..643941085 100644 --- a/test/formal/sub_sub.py +++ b/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: diff --git a/test/formal/util.py b/test/formal/util.py index ec98f9c81..8d0debbef 100644 --- a/test/formal/util.py +++ b/test/formal/util.py @@ -1,27 +1,27 @@ -from z3 import * +from z3 import BitVecVal, Concat, If def BVUnsignedUpCast(x, n_bits): - assert(x.size() <= 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) + assert type_bits <= n_bits return BitVecVal((1 << type_bits) - 1, n_bits) def BVSignedUpCast(x, n_bits): - assert(x.size() <= 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) + 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) + assert type_bits <= n_bits return BitVecVal(-(1 << (type_bits - 1)), n_bits)