cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Kamil Śliwak 2020-12-22 07:46:31 +01:00
parent d71de88bc1
commit b3922bc300
3 changed files with 69 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
scripts/bytecodecompare/prepare_report.js
View File

@ -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)))

37
scripts/bytecodecompare/prepare_report.py
View File

@ -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),
)

20
test/scripts/test_bytecodecompare_prepare_report.py
View File

@ -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):