From b3922bc300fc5581bfcd807a783c377e2f24fc33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Kamil=20=C5=9Aliwak?= Date: Tue, 22 Dec 2020 07:46:31 +0100 Subject: [PATCH] prepare_report: Add command-line options for switching between SMT pragma stripping and only disabling the SMT checker --- scripts/bytecodecompare/prepare_report.js | 32 +++++++++++++--- scripts/bytecodecompare/prepare_report.py | 37 +++++++++++++------ .../test_bytecodecompare_prepare_report.py | 20 ++++++++-- 3 files changed, 69 insertions(+), 20 deletions(-) diff --git a/scripts/bytecodecompare/prepare_report.js b/scripts/bytecodecompare/prepare_report.js index 1d1b04060..1c5d55ec0 100755 --- a/scripts/bytecodecompare/prepare_report.js +++ b/scripts/bytecodecompare/prepare_report.js @@ -4,23 +4,45 @@ const fs = require('fs') const compiler = require('./solc-js/wrapper.js')(require('./solc-js/soljson.js')) + +function loadSource(sourceFileName, stripSMTPragmas) +{ + source = fs.readFileSync(sourceFileName).toString() + + if (stripSMTPragmas) + return source.replace('pragma experimental SMTChecker;', ''); + + return source +} + + +let stripSMTPragmas = false +let firstFileArgumentIndex = 2 + +if (process.argv.length >= 3 && process.argv[2] === '--strip-smt-pragmas') +{ + stripSMTPragmas = true + firstFileArgumentIndex = 3 +} + for (const optimize of [false, true]) { - for (const filename of process.argv.slice(2)) + for (const filename of process.argv.slice(firstFileArgumentIndex)) { if (filename !== undefined) { - const input = { + let input = { language: 'Solidity', sources: { - [filename]: {content: fs.readFileSync(filename).toString()} + [filename]: {content: loadSource(filename, stripSMTPragmas)} }, settings: { optimizer: {enabled: optimize}, - outputSelection: {'*': {'*': ['evm.bytecode.object', 'metadata']}}, - "modelChecker": {"engine": "none"} + outputSelection: {'*': {'*': ['evm.bytecode.object', 'metadata']}} } } + if (!stripSMTPragmas) + input['settings']['modelChecker'] = {engine: 'none'} const result = JSON.parse(compiler.compile(JSON.stringify(input))) diff --git a/scripts/bytecodecompare/prepare_report.py b/scripts/bytecodecompare/prepare_report.py index 1082d77fe..26cdf45e8 100755 --- a/scripts/bytecodecompare/prepare_report.py +++ b/scripts/bytecodecompare/prepare_report.py @@ -23,6 +23,12 @@ class CompilerInterface(Enum): STANDARD_JSON = 'standard-json' +class SMTUse(Enum): + PRESERVE = 'preserve' + DISABLE = 'disable' + STRIP_PRAGMAS = 'strip-pragmas' + + @dataclass(frozen=True) class ContractReport: contract_name: str @@ -54,10 +60,13 @@ class FileReport: return report -def load_source(path: Union[Path, str]) -> str: +def load_source(path: Union[Path, str], smt_use: SMTUse) -> str: with open(path, mode='r', encoding='utf8') as source_file: file_content = source_file.read() + if smt_use == SMTUse.STRIP_PRAGMAS: + return file_content.replace('pragma experimental SMTChecker;', '') + return file_content @@ -111,38 +120,42 @@ def parse_cli_output(source_file_name: Path, cli_output: str) -> FileReport: return file_report -def prepare_compiler_input(compiler_path: Path, source_file_name: Path, optimize: bool, interface: CompilerInterface) -> Tuple[List[str], str]: +def prepare_compiler_input(compiler_path: Path, source_file_name: Path, optimize: bool, interface: CompilerInterface, smt_use: SMTUse) -> Tuple[List[str], str]: if interface == CompilerInterface.STANDARD_JSON: json_input: dict = { 'language': 'Solidity', 'sources': { - str(source_file_name): {'content': load_source(source_file_name)} + str(source_file_name): {'content': load_source(source_file_name, smt_use)} }, 'settings': { 'optimizer': {'enabled': optimize}, 'outputSelection': {'*': {'*': ['evm.bytecode.object', 'metadata']}}, - 'modelChecker': {'engine': 'none'}, } } + if smt_use == SMTUse.DISABLE: + json_input['settings']['modelChecker'] = {'engine': 'none'} + command_line = [str(compiler_path), '--standard-json'] compiler_input = json.dumps(json_input) else: assert interface == CompilerInterface.CLI - compiler_options = [str(source_file_name), '--bin', '--metadata', '--model-checker-engine', 'none'] + compiler_options = [str(source_file_name), '--bin', '--metadata'] if optimize: compiler_options.append('--optimize') + if smt_use == SMTUse.DISABLE: + compiler_options += ['--model-checker-engine', 'none'] command_line = [str(compiler_path)] + compiler_options - compiler_input = load_source(source_file_name) + compiler_input = load_source(source_file_name, smt_use) return (command_line, compiler_input) -def run_compiler(compiler_path: Path, source_file_name: Path, optimize: bool, interface: CompilerInterface) -> FileReport: +def run_compiler(compiler_path: Path, source_file_name: Path, optimize: bool, interface: CompilerInterface, smt_use: SMTUse, tmp_dir: Path) -> FileReport: if interface == CompilerInterface.STANDARD_JSON: - (command_line, compiler_input) = prepare_compiler_input(compiler_path, Path(source_file_name).name, optimize, interface) + (command_line, compiler_input) = prepare_compiler_input(compiler_path, Path(source_file_name).name, optimize, interface, smt_use) process = subprocess.run( command_line, @@ -156,7 +169,7 @@ def run_compiler(compiler_path: Path, source_file_name: Path, optimize: bool, in assert interface == CompilerInterface.CLI assert tmp_dir is not None - (command_line, compiler_input) = prepare_compiler_input(compiler_path.absolute(), source_file_name.name, optimize, interface) + (command_line, compiler_input) = prepare_compiler_input(compiler_path.absolute(), source_file_name.name, optimize, interface, smt_use) # Create a copy that we can use directly with the CLI interface modified_source_path = tmp_dir / source_file_name.name @@ -173,13 +186,13 @@ def run_compiler(compiler_path: Path, source_file_name: Path, optimize: bool, in return parse_cli_output(Path(source_file_name), process.stdout) -def generate_report(source_file_names: List[str], compiler_path: Path, interface: CompilerInterface): +def generate_report(source_file_names: List[str], compiler_path: Path, interface: CompilerInterface, smt_use: SMTUse): with open('report.txt', mode='w', encoding='utf8', newline='\n') as report_file: for optimize in [False, True]: with TemporaryDirectory(prefix='prepare_report-') as tmp_dir: for source_file_name in sorted(source_file_names): try: - report = run_compiler(Path(compiler_path), Path(source_file_name), optimize, interface, Path(tmp_dir)) + report = run_compiler(Path(compiler_path), Path(source_file_name), optimize, interface, smt_use, Path(tmp_dir)) report_file.write(report.format_report()) except subprocess.CalledProcessError as exception: print(f"\n\nInterrupted by an exception while processing file '{source_file_name}' with optimize={optimize}\n", file=sys.stderr) @@ -200,6 +213,7 @@ def commandline_parser() -> ArgumentParser: parser = ArgumentParser(description=script_description) parser.add_argument(dest='compiler_path', help="Solidity compiler executable") parser.add_argument('--interface', dest='interface', default=CompilerInterface.STANDARD_JSON.value, choices=[c.value for c in CompilerInterface], help="Compiler interface to use.") + parser.add_argument('--smt-use', dest='smt_use', default=SMTUse.DISABLE.value, choices=[s.value for s in SMTUse], help="What to do about contracts that use the experimental SMT checker.") return parser; @@ -209,4 +223,5 @@ if __name__ == "__main__": glob("*.sol"), Path(options.compiler_path), CompilerInterface(options.interface), + SMTUse(options.smt_use), ) diff --git a/test/scripts/test_bytecodecompare_prepare_report.py b/test/scripts/test_bytecodecompare_prepare_report.py index 6589d7e74..077b50051 100644 --- a/test/scripts/test_bytecodecompare_prepare_report.py +++ b/test/scripts/test_bytecodecompare_prepare_report.py @@ -7,7 +7,7 @@ from textwrap import dedent from unittest_helpers import LIBSOLIDITY_TEST_DIR, load_fixture, load_libsolidity_test_case -from bytecodecompare.prepare_report import CompilerInterface, FileReport, ContractReport +from bytecodecompare.prepare_report import CompilerInterface, FileReport, ContractReport, SMTUse from bytecodecompare.prepare_report import load_source, parse_cli_output, parse_standard_json_output, prepare_compiler_input @@ -80,8 +80,18 @@ class TestPrepareReport(unittest.TestCase): def setUp(self): self.maxDiff = 10000 - def test_load_source(self): - self.assertEqual(load_source(SMT_SMOKE_TEST_SOL_PATH), SMT_SMOKE_TEST_SOL_CODE) + def test_load_source_should_strip_smt_pragmas_if_requested(self): + expected_file_content = dedent("""\ + + contract C { + } + """) + + self.assertEqual(load_source(SMT_SMOKE_TEST_SOL_PATH, SMTUse.STRIP_PRAGMAS), expected_file_content) + + def test_load_source_should_not_strip_smt_pragmas_if_not_requested(self): + self.assertEqual(load_source(SMT_SMOKE_TEST_SOL_PATH, SMTUse.DISABLE), SMT_SMOKE_TEST_SOL_CODE) + self.assertEqual(load_source(SMT_SMOKE_TEST_SOL_PATH, SMTUse.PRESERVE), SMT_SMOKE_TEST_SOL_CODE) def test_prepare_compiler_input_should_work_with_standard_json_interface(self): expected_compiler_input = { @@ -101,6 +111,7 @@ class TestPrepareReport(unittest.TestCase): SMT_SMOKE_TEST_SOL_PATH, optimize=True, interface=CompilerInterface.STANDARD_JSON, + smt_use=SMTUse.DISABLE ) self.assertEqual(command_line, ['solc', '--standard-json']) @@ -112,9 +123,10 @@ class TestPrepareReport(unittest.TestCase): SMT_SMOKE_TEST_SOL_PATH, optimize=True, interface=CompilerInterface.CLI, + smt_use=SMTUse.DISABLE ) - self.assertEqual(command_line, ['solc', str(SMT_SMOKE_TEST_SOL_PATH), '--bin', '--metadata', '--model-checker-engine', 'none', '--optimize']) + self.assertEqual(command_line, ['solc', str(SMT_SMOKE_TEST_SOL_PATH), '--bin', '--metadata', '--optimize', '--model-checker-engine', 'none']) self.assertEqual(compiler_input, SMT_SMOKE_TEST_SOL_CODE) def test_parse_standard_json_output(self):