prepare_report: Add command-line options for switching between SMT pragma stripping and only disabling the SMT checker

scripts/bytecodecompare/prepare_report.js

@@ -4,23 +4,46 @@ 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)
+        // NOTE: replace() with string parameter replaces only the first occurrence.
+        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']}},
+                    outputSelection: {'*': {'*': ['evm.bytecode.object', 'metadata']}}
-                    "modelChecker": {"engine": "none"}
                 }
             }
+            if (!stripSMTPragmas)
+                input['settings']['modelChecker'] = {engine: 'none'}
 
             const result = JSON.parse(compiler.compile(JSON.stringify(input)))
 

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,12 +60,15 @@ class FileReport:
         return report
 
 
-def load_source(path: Union[Path, str]) -> str:
+def load_source(path: Union[Path, str], smt_use: SMTUse) -> str:
     # NOTE: newline='' disables newline conversion.
     # We want the file exactly as is because changing even a single byte in the source affects metadata.
     with open(path, mode='r', encoding='utf8', newline='') as source_file:
         file_content = source_file.read()
 
+    if smt_use == SMTUse.STRIP_PRAGMAS:
+        return file_content.replace('pragma experimental SMTChecker;', '', 1)
+
     return file_content
 
 
@@ -126,33 +135,37 @@ def prepare_compiler_input(
     compiler_path: Path,
     source_file_name: Path,
     optimize: bool,
-    interface: CompilerInterface
+    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)
 
@@ -162,6 +175,7 @@ def run_compiler(
     source_file_name: Path,
     optimize: bool,
     interface: CompilerInterface,
+    smt_use: SMTUse,
     tmp_dir: Path,
 ) -> FileReport:
 
@@ -170,7 +184,8 @@ def run_compiler(
             compiler_path,
             Path(source_file_name.name),
             optimize,
-            interface
+            interface,
+            smt_use,
         )
 
         process = subprocess.run(
@@ -190,7 +205,8 @@ def run_compiler(
             compiler_path.absolute(),
             Path(source_file_name.name),
             optimize,
-            interface
+            interface,
+            smt_use,
         )
 
         # Create a copy that we can use directly with the CLI interface
@@ -211,13 +227,20 @@ def run_compiler(
         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(compiler_path, Path(source_file_name), optimize, interface, Path(tmp_dir))
+                        report = run_compiler(
+                            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(
@@ -250,7 +273,14 @@ def commandline_parser() -> ArgumentParser:
         dest='interface',
         default=CompilerInterface.STANDARD_JSON.value,
         choices=[c.value for c in CompilerInterface],
-        help="Compiler interface to use."
+        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;
 
@@ -261,4 +291,5 @@ if __name__ == "__main__":
         glob("*.sol"),
         Path(options.compiler_path),
         CompilerInterface(options.interface),
+        SMTUse(options.smt_use),
     )

test/scripts/test_bytecodecompare_prepare_report.py

@@ -9,7 +9,7 @@ from unittest_helpers import FIXTURE_DIR, LIBSOLIDITY_TEST_DIR, load_fixture, lo
 
 # NOTE: This test file file only works with scripts/ added to PYTHONPATH so pylint can't find the imports
 # pragma pylint: disable=import-error
-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
 # pragma pylint: enable=import-error
 
@@ -98,48 +98,58 @@ class TestFileReport(PrepareReportTestBase):
 
 
 class TestLoadSource(PrepareReportTestBase):
-    def test_load_source(self):
+    def test_load_source_should_strip_smt_pragmas_if_requested(self):
-        self.assertEqual(load_source(SMT_SMOKE_TEST_SOL_PATH), SMT_SMOKE_TEST_SOL_CODE)
+        expected_file_content = (
-
-    def test_load_source_preserves_lf_newlines(self):
-        expected_output = (
-            "pragma experimental SMTChecker;\n"
             "\n"
             "contract C {\n"
             "}\n"
         )
 
-        self.assertEqual(load_source(SMT_CONTRACT_WITH_LF_NEWLINES_SOL_PATH), expected_output)
+        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_load_source_preserves_lf_newlines(self):
+        expected_output = (
+            "\n"
+            "\n"
+            "contract C {\n"
+            "}\n"
+        )
+
+        self.assertEqual(load_source(SMT_CONTRACT_WITH_LF_NEWLINES_SOL_PATH, SMTUse.STRIP_PRAGMAS), expected_output)
 
     def test_load_source_preserves_crlf_newlines(self):
         expected_output = (
-            "pragma experimental SMTChecker;\r\n"
+            "\r\n"
             "\r\n"
             "contract C {\r\n"
             "}\r\n"
         )
 
-        self.assertEqual(load_source(SMT_CONTRACT_WITH_CRLF_NEWLINES_SOL_PATH), expected_output)
+        self.assertEqual(load_source(SMT_CONTRACT_WITH_CRLF_NEWLINES_SOL_PATH, SMTUse.STRIP_PRAGMAS), expected_output)
 
     def test_load_source_preserves_cr_newlines(self):
         expected_output = (
-            "pragma experimental SMTChecker;\r"
+            "\r"
             "\r"
             "contract C {\r"
             "}\r"
         )
 
-        self.assertEqual(load_source(SMT_CONTRACT_WITH_CR_NEWLINES_SOL_PATH), expected_output)
+        self.assertEqual(load_source(SMT_CONTRACT_WITH_CR_NEWLINES_SOL_PATH, SMTUse.STRIP_PRAGMAS), expected_output)
 
     def test_load_source_preserves_mixed_newlines(self):
         expected_output = (
-            "pragma experimental SMTChecker;\n"
+            "\n"
             "\n"
             "contract C {\r"
             "}\r\n"
         )
 
-        self.assertEqual(load_source(SMT_CONTRACT_WITH_MIXED_NEWLINES_SOL_PATH), expected_output)
+        self.assertEqual(load_source(SMT_CONTRACT_WITH_MIXED_NEWLINES_SOL_PATH, SMTUse.STRIP_PRAGMAS), expected_output)
 
 
 class TestPrepareCompilerInput(PrepareReportTestBase):
@@ -161,6 +171,7 @@ class TestPrepareCompilerInput(PrepareReportTestBase):
             SMT_SMOKE_TEST_SOL_PATH,
             optimize=True,
             interface=CompilerInterface.STANDARD_JSON,
+            smt_use=SMTUse.DISABLE,
         )
 
         self.assertEqual(command_line, ['solc', '--standard-json'])
@@ -172,11 +183,12 @@ class TestPrepareCompilerInput(PrepareReportTestBase):
             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']
+            ['solc', str(SMT_SMOKE_TEST_SOL_PATH), '--bin', '--metadata', '--optimize', '--model-checker-engine', 'none']
         )
         self.assertEqual(compiler_input, SMT_SMOKE_TEST_SOL_CODE)
 
@@ -204,6 +216,7 @@ class TestPrepareCompilerInput(PrepareReportTestBase):
             SMT_CONTRACT_WITH_MIXED_NEWLINES_SOL_PATH,
             optimize=True,
             interface=CompilerInterface.STANDARD_JSON,
+            smt_use=SMTUse.DISABLE,
         )
 
         self.assertEqual(command_line, ['solc', '--standard-json'])
@@ -215,6 +228,7 @@ class TestPrepareCompilerInput(PrepareReportTestBase):
             SMT_CONTRACT_WITH_MIXED_NEWLINES_SOL_PATH,
             optimize=True,
             interface=CompilerInterface.CLI,
+            smt_use=SMTUse.DISABLE,
         )
 
         self.assertEqual(compiler_input, SMT_CONTRACT_WITH_MIXED_NEWLINES_SOL_CODE)