mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Merge pull request #11833 from ethereum/enable-more-pylint-checks
Enable more pylint checks
This commit is contained in:
commit
ded3cb7ea5
@ -413,7 +413,7 @@ def commandline_parser() -> ArgumentParser:
|
|||||||
action='store_true',
|
action='store_true',
|
||||||
help="Immediately exit and print compiler output if the compiler exits with an error.",
|
help="Immediately exit and print compiler output if the compiler exits with an error.",
|
||||||
)
|
)
|
||||||
return parser;
|
return parser
|
||||||
|
|
||||||
|
|
||||||
if __name__ == "__main__":
|
if __name__ == "__main__":
|
||||||
|
@ -39,7 +39,7 @@ def colorize(left, right, id):
|
|||||||
reset = "\x1b[0m"
|
reset = "\x1b[0m"
|
||||||
colors = [red, yellow]
|
colors = [red, yellow]
|
||||||
color = colors[id % len(colors)]
|
color = colors[id % len(colors)]
|
||||||
function, arguments, results = parse_call(right)
|
function, _arguments, _results = parse_call(right)
|
||||||
left = left.replace("compileAndRun", color + "compileAndRun" + reset)
|
left = left.replace("compileAndRun", color + "compileAndRun" + reset)
|
||||||
right = right.replace("constructor", color + "constructor" + reset)
|
right = right.replace("constructor", color + "constructor" + reset)
|
||||||
if function:
|
if function:
|
||||||
@ -158,7 +158,7 @@ def main(argv):
|
|||||||
interactive = False
|
interactive = False
|
||||||
input_file = None
|
input_file = None
|
||||||
try:
|
try:
|
||||||
opts, args = getopt.getopt(argv, "if:")
|
opts, _args = getopt.getopt(argv, "if:")
|
||||||
except getopt.GetoptError:
|
except getopt.GetoptError:
|
||||||
print("./remove-testcases.py [-i] [-f <full path to SolidityEndToEndTest.cpp>]")
|
print("./remove-testcases.py [-i] [-f <full path to SolidityEndToEndTest.cpp>]")
|
||||||
sys.exit(1)
|
sys.exit(1)
|
||||||
|
@ -158,7 +158,7 @@ class TraceAnalyser:
|
|||||||
for trace_id, trace in enumerate(left.traces):
|
for trace_id, trace in enumerate(left.traces):
|
||||||
left_trace = trace
|
left_trace = trace
|
||||||
right_trace = right.traces[trace_id]
|
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):
|
if str(left_trace) != str(right_trace):
|
||||||
mismatch_info = " " + str(left_trace) + "\n"
|
mismatch_info = " " + str(left_trace) + "\n"
|
||||||
mismatch_info += " " + str(right_trace) + "\n"
|
mismatch_info += " " + str(right_trace) + "\n"
|
||||||
@ -179,7 +179,7 @@ def main(argv):
|
|||||||
extracted_tests_trace_file = None
|
extracted_tests_trace_file = None
|
||||||
end_to_end_trace_file = None
|
end_to_end_trace_file = None
|
||||||
try:
|
try:
|
||||||
opts, args = getopt.getopt(argv, "s:e:")
|
opts, _args = getopt.getopt(argv, "s:e:")
|
||||||
except getopt.GetoptError:
|
except getopt.GetoptError:
|
||||||
print("verify-testcases.py [-s <path to semantic-trace>] [-e <path to endToEndExtraction-trace>]")
|
print("verify-testcases.py [-s <path to semantic-trace>] [-e <path to endToEndExtraction-trace>]")
|
||||||
sys.exit(2)
|
sys.exit(2)
|
||||||
|
@ -261,9 +261,9 @@ def main(argv):
|
|||||||
no_confirm = False
|
no_confirm = False
|
||||||
examine_coverage = False
|
examine_coverage = False
|
||||||
next_id = 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":
|
if opt == "--check":
|
||||||
check = True
|
check = True
|
||||||
elif opt == "--fix":
|
elif opt == "--fix":
|
||||||
|
@ -49,9 +49,10 @@ def readDependencies(fname):
|
|||||||
if line[0] == '\t':
|
if line[0] == '\t':
|
||||||
library = line.split(' ', 1)[0][1:]
|
library = line.split(' ', 1)[0][1:]
|
||||||
if (library.startswith("/usr/local/lib") or
|
if (library.startswith("/usr/local/lib") or
|
||||||
library.startswith("/usr/local/opt") or
|
library.startswith("/usr/local/opt") or
|
||||||
library.startswith("/Users/")):
|
library.startswith("/Users/")
|
||||||
if (os.path.basename(library) != os.path.basename(fname)):
|
):
|
||||||
|
if os.path.basename(library) != os.path.basename(fname):
|
||||||
command = "install_name_tool -change " + \
|
command = "install_name_tool -change " + \
|
||||||
library + " @executable_path/./" + \
|
library + " @executable_path/./" + \
|
||||||
os.path.basename(library) + " " + fname
|
os.path.basename(library) + " " + fname
|
||||||
|
@ -20,7 +20,7 @@ repository. The changes are compared against ``origin/develop``.
|
|||||||
import subprocess
|
import subprocess
|
||||||
from pathlib import Path
|
from pathlib import Path
|
||||||
from enum import Enum
|
from enum import Enum
|
||||||
from parsec import *
|
from parsec import generate, ParseError, regex, string
|
||||||
from tabulate import tabulate
|
from tabulate import tabulate
|
||||||
|
|
||||||
class Kind(Enum):
|
class Kind(Enum):
|
||||||
@ -56,10 +56,10 @@ def diff_string() -> (Kind, Diff, int):
|
|||||||
-// gas irOptimized: 138070
|
-// gas irOptimized: 138070
|
||||||
|
|
||||||
"""
|
"""
|
||||||
diff_kind = yield (minus | plus)
|
diff_kind = yield minus | plus
|
||||||
yield comment
|
yield comment
|
||||||
yield space
|
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 colon
|
||||||
yield space
|
yield space
|
||||||
val = yield number()
|
val = yield number()
|
||||||
|
@ -6,7 +6,6 @@
|
|||||||
# into files for e.g. fuzz testing as
|
# into files for e.g. fuzz testing as
|
||||||
# scripts/isolate_tests.py test/libsolidity/*
|
# scripts/isolate_tests.py test/libsolidity/*
|
||||||
|
|
||||||
import sys
|
|
||||||
import re
|
import re
|
||||||
import os
|
import os
|
||||||
import hashlib
|
import hashlib
|
||||||
|
@ -9,7 +9,6 @@ from os import path, walk
|
|||||||
from sys import exit
|
from sys import exit
|
||||||
from textwrap import dedent
|
from textwrap import dedent
|
||||||
import subprocess
|
import subprocess
|
||||||
import sys
|
|
||||||
|
|
||||||
PROJECT_ROOT = path.dirname(path.dirname(path.realpath(__file__)))
|
PROJECT_ROOT = path.dirname(path.dirname(path.realpath(__file__)))
|
||||||
PYLINT_RCFILE = f"{PROJECT_ROOT}/scripts/pylintrc"
|
PYLINT_RCFILE = f"{PROJECT_ROOT}/scripts/pylintrc"
|
||||||
|
@ -24,24 +24,15 @@ disable=
|
|||||||
duplicate-code,
|
duplicate-code,
|
||||||
invalid-name,
|
invalid-name,
|
||||||
missing-docstring,
|
missing-docstring,
|
||||||
mixed-indentation,
|
|
||||||
no-else-return,
|
no-else-return,
|
||||||
no-self-use,
|
no-self-use,
|
||||||
pointless-string-statement,
|
pointless-string-statement,
|
||||||
redefined-builtin,
|
redefined-builtin,
|
||||||
redefined-outer-name,
|
redefined-outer-name,
|
||||||
singleton-comparison,
|
singleton-comparison,
|
||||||
superfluous-parens,
|
|
||||||
too-few-public-methods,
|
too-few-public-methods,
|
||||||
trailing-newlines,
|
too-many-public-methods,
|
||||||
undefined-variable,
|
ungrouped-imports
|
||||||
ungrouped-imports,
|
|
||||||
unnecessary-semicolon,
|
|
||||||
unused-import,
|
|
||||||
unused-variable,
|
|
||||||
unused-wildcard-import,
|
|
||||||
useless-object-inheritance,
|
|
||||||
wildcard-import
|
|
||||||
|
|
||||||
[BASIC]
|
[BASIC]
|
||||||
|
|
||||||
|
@ -11,7 +11,7 @@ import time
|
|||||||
|
|
||||||
DESCRIPTION = """Regressor is a tool to run regression tests in a CI env."""
|
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"""
|
"""Prints a dot every "interval" (default is 300) seconds"""
|
||||||
|
|
||||||
def __init__(self, interval=300):
|
def __init__(self, interval=300):
|
||||||
@ -30,7 +30,7 @@ class PrintDotsThread(object):
|
|||||||
print(".")
|
print(".")
|
||||||
time.sleep(self.interval)
|
time.sleep(self.interval)
|
||||||
|
|
||||||
class regressor():
|
class regressor:
|
||||||
_re_sanitizer_log = re.compile(r"""ERROR: (libFuzzer|UndefinedBehaviorSanitizer)""")
|
_re_sanitizer_log = re.compile(r"""ERROR: (libFuzzer|UndefinedBehaviorSanitizer)""")
|
||||||
|
|
||||||
def __init__(self, description, args):
|
def __init__(self, description, args):
|
||||||
|
@ -44,9 +44,7 @@ def writeSourceToFile(lines):
|
|||||||
os.system("mkdir -p " + filePath)
|
os.system("mkdir -p " + filePath)
|
||||||
with open(srcName, mode='a+', encoding='utf8', newline='') as f:
|
with open(srcName, mode='a+', encoding='utf8', newline='') as f:
|
||||||
createdSources.append(srcName)
|
createdSources.append(srcName)
|
||||||
i = 0
|
|
||||||
for idx, line in enumerate(lines[1:]):
|
for idx, line in enumerate(lines[1:]):
|
||||||
|
|
||||||
# write to file
|
# write to file
|
||||||
if line[:12] != "==== Source:":
|
if line[:12] != "==== Source:":
|
||||||
f.write(line)
|
f.write(line)
|
||||||
|
@ -7,7 +7,8 @@ import sys
|
|||||||
import re
|
import re
|
||||||
import os
|
import os
|
||||||
import hashlib
|
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):
|
def extract_test_cases(path):
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import BYTE
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec
|
||||||
|
|
||||||
"""
|
"""
|
||||||
byte(A, X) -> 0
|
byte(A, X) -> 0
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import BYTE
|
||||||
from rule import Rule
|
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
|
Checks that the byte opcode (implemented using shift) is equivalent to a
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
|
from opcodes import AND, ISZERO, SGT, SLT, SUB
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from util import BVSignedMax, BVSignedMin, BVSignedUpCast
|
||||||
from util import *
|
from z3 import BitVec, BVAddNoOverflow, BVAddNoUnderflow, Not
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Overflow checked signed integer addition.
|
Overflow checked signed integer addition.
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
|
from opcodes import AND, EQ, SUB
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from util import BVSignedMin, BVSignedUpCast
|
||||||
from util import *
|
from z3 import BitVec, BVSDivNoOverflow, Not
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Overflow checked signed integer division.
|
Overflow checked signed integer division.
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
|
from opcodes import AND, DIV, GT, SDIV, SGT, SLT
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from util import BVSignedMax, BVSignedMin, BVSignedUpCast
|
||||||
from util import *
|
from z3 import BVMulNoOverflow, BVMulNoUnderflow, BitVec, Not, Or
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Overflow checked signed integer multiplication.
|
Overflow checked signed integer multiplication.
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
|
from opcodes import AND, ADD, ISZERO, SLT, SGT
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from util import BVSignedMax, BVSignedMin, BVSignedUpCast
|
||||||
from util import *
|
from z3 import BitVec, BVSubNoOverflow, BVSubNoUnderflow, Not
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Overflow checked signed integer subtraction.
|
Overflow checked signed integer subtraction.
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
|
from opcodes import GT, SUB
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from util import BVUnsignedMax, BVUnsignedUpCast
|
||||||
from util import *
|
from z3 import BitVec, BVAddNoOverflow, Not
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Overflow checked unsigned integer addition.
|
Overflow checked unsigned integer addition.
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
|
from opcodes import AND, ISZERO, GT, DIV
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from util import BVUnsignedUpCast, BVUnsignedMax
|
||||||
from util import *
|
from z3 import BitVec, Not, BVMulNoOverflow
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Overflow checked unsigned integer multiplication.
|
Overflow checked unsigned integer multiplication.
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
|
from opcodes import LT
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from util import BVUnsignedMax, BVUnsignedUpCast
|
||||||
from util import *
|
from z3 import BVSubNoUnderflow, BitVec, Not
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Overflow checked unsigned integer subtraction.
|
Overflow checked unsigned integer subtraction.
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import BYTE, SHL
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, ULE
|
||||||
|
|
||||||
"""
|
"""
|
||||||
byte(A, shl(B, X))
|
byte(A, shl(B, X))
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import BYTE, DIV, SHR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, UGE, ULE, ULT
|
||||||
|
|
||||||
"""
|
"""
|
||||||
byte(A, shr(B, X))
|
byte(A, shr(B, X))
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import BYTE, SHR, DIV
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, ULT
|
||||||
|
|
||||||
"""
|
"""
|
||||||
byte(A, shr(B, X))
|
byte(A, shr(B, X))
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import DIV, SHL, SHR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import SHL, MUL
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import AND, SHL, SHR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal, If, Int2BV, IntVal, UGT, ULT
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import AND, SHL, SHR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal, If, Int2BV, IntVal, UGT, ULT
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import EQ, ISZERO, SUB
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,6 +1,7 @@
|
|||||||
|
from opcodes import AND, ISZERO, MOD, SUB
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from util import BVUnsignedMax
|
||||||
from util import *
|
from z3 import BitVec, BitVecVal, If
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Checking conversion of exp(-1, X) to sub(isZero(and(X, 1)), and(X, 1))
|
Checking conversion of exp(-1, X) to sub(isZero(and(X, 1)), and(X, 1))
|
||||||
|
@ -1,6 +1,6 @@
|
|||||||
|
from opcodes import SHL
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, If
|
||||||
from util import *
|
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Checking conversion of exp(2, X) to shl(X, 1)
|
Checking conversion of exp(2, X) to shl(X, 1)
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import AND, SHL
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal, ULT
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import AND, SHR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal, ULT
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
@ -25,12 +26,12 @@ BitWidth = BitVecVal(n_bits, n_bits)
|
|||||||
rule.require(ULT(B, BitWidth))
|
rule.require(ULT(B, BitWidth))
|
||||||
|
|
||||||
# Non optimized result
|
# Non optimized result
|
||||||
nonopt_1 = SHR(B, AND(X, A));
|
nonopt_1 = SHR(B, AND(X, A))
|
||||||
nonopt_2 = SHR(B, AND(A, X));
|
nonopt_2 = SHR(B, AND(A, X))
|
||||||
|
|
||||||
# Optimized result
|
# Optimized result
|
||||||
Mask = SHR(B, A);
|
Mask = SHR(B, A)
|
||||||
opt = AND(SHR(B, X), Mask);
|
opt = AND(SHR(B, X), Mask)
|
||||||
|
|
||||||
rule.check(nonopt_1, opt)
|
rule.check(nonopt_1, opt)
|
||||||
rule.check(nonopt_2, opt)
|
rule.check(nonopt_2, opt)
|
||||||
|
@ -1,5 +1,7 @@
|
|||||||
|
from opcodes import AND, OR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec
|
||||||
|
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
from z3 import *
|
from z3 import BitVecVal, BV2Int, If, LShR, UDiv, ULT, UGT, URem
|
||||||
|
|
||||||
def ADD(x, y):
|
def ADD(x, y):
|
||||||
return x + y
|
return x + y
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import AND
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import OR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import DIV, MUL, SHL, SHR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,6 +1,6 @@
|
|||||||
import sys
|
import sys
|
||||||
|
|
||||||
from z3 import *
|
from z3 import sat, Solver, unknown, unsat
|
||||||
|
|
||||||
class Rule:
|
class Rule:
|
||||||
def __init__(self):
|
def __init__(self):
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import SHL
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BV2Int, Int2BV, IntVal
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Shift left workaround that Solidity implements
|
Shift left workaround that Solidity implements
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import SIGNEXTEND
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal, If, UGE, ULT
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
@ -34,4 +35,3 @@ rule3.check(
|
|||||||
SIGNEXTEND(A, SIGNEXTEND(B, X)),
|
SIGNEXTEND(A, SIGNEXTEND(B, X)),
|
||||||
SIGNEXTEND(If(ULT(A, B), A, B), X)
|
SIGNEXTEND(If(ULT(A, B), A, B), X)
|
||||||
)
|
)
|
||||||
|
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import SIGNEXTEND, AND
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal, ULT
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import SIGNEXTEND
|
||||||
from rule import Rule
|
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
|
Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import SHL, SIGNEXTEND
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, LShR, ULE
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import SIGNEXTEND, SAR, SHR
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal, ULE
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
@ -28,4 +29,3 @@ rule.check(
|
|||||||
SIGNEXTEND(A, SHR(B, X)),
|
SIGNEXTEND(A, SHR(B, X)),
|
||||||
SAR(B, X)
|
SAR(B, X)
|
||||||
)
|
)
|
||||||
|
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import NOT, SUB
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec, BitVecVal
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rule:
|
Rule:
|
||||||
|
@ -1,5 +1,6 @@
|
|||||||
|
from opcodes import ADD, SUB
|
||||||
from rule import Rule
|
from rule import Rule
|
||||||
from opcodes import *
|
from z3 import BitVec
|
||||||
|
|
||||||
"""
|
"""
|
||||||
Rules:
|
Rules:
|
||||||
|
@ -1,27 +1,27 @@
|
|||||||
from z3 import *
|
from z3 import BitVecVal, Concat, If
|
||||||
|
|
||||||
def BVUnsignedUpCast(x, n_bits):
|
def BVUnsignedUpCast(x, n_bits):
|
||||||
assert(x.size() <= n_bits)
|
assert x.size() <= n_bits
|
||||||
if x.size() < n_bits:
|
if x.size() < n_bits:
|
||||||
return Concat(BitVecVal(0, n_bits - x.size()), x)
|
return Concat(BitVecVal(0, n_bits - x.size()), x)
|
||||||
else:
|
else:
|
||||||
return x
|
return x
|
||||||
|
|
||||||
def BVUnsignedMax(type_bits, n_bits):
|
def BVUnsignedMax(type_bits, n_bits):
|
||||||
assert(type_bits <= n_bits)
|
assert type_bits <= n_bits
|
||||||
return BitVecVal((1 << type_bits) - 1, n_bits)
|
return BitVecVal((1 << type_bits) - 1, n_bits)
|
||||||
|
|
||||||
def BVSignedUpCast(x, n_bits):
|
def BVSignedUpCast(x, n_bits):
|
||||||
assert(x.size() <= n_bits)
|
assert x.size() <= n_bits
|
||||||
if 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)
|
return Concat(If(x < 0, BitVecVal(-1, n_bits - x.size()), BitVecVal(0, n_bits - x.size())), x)
|
||||||
else:
|
else:
|
||||||
return x
|
return x
|
||||||
|
|
||||||
def BVSignedMax(type_bits, n_bits):
|
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)
|
return BitVecVal((1 << (type_bits - 1)) - 1, n_bits)
|
||||||
|
|
||||||
def BVSignedMin(type_bits, 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)
|
return BitVecVal(-(1 << (type_bits - 1)), n_bits)
|
||||||
|
Loading…
Reference in New Issue
Block a user