Merge pull request #10364 from ethereum/bytecode-comparison-with-model-checker-engine-none

Disable SMT checker instead of stripping SMT pragmas in bytecode comparison
This commit is contained in:
Alex Beregszaszi 2020-11-20 20:00:27 +00:00 committed by GitHub
commit 5b283f4a08
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 8 additions and 10 deletions

View File

@ -8,13 +8,10 @@ import json
SOLC_BIN = sys.argv[1]
REPORT_FILE = open("report.txt", mode="w", encoding='utf8', newline='\n')
def removeSMT(source):
return source.replace('pragma experimental SMTChecker;', '')
for optimize in [False, True]:
for f in sorted(glob.glob("*.sol")):
sources = {}
sources[f] = {'content': removeSMT(open(f, mode='r', encoding='utf8').read())}
sources[f] = {'content': open(f, mode='r', encoding='utf8').read()}
input_json = {
'language': 'Solidity',
'sources': sources,
@ -23,6 +20,9 @@ for optimize in [False, True]:
'enabled': optimize
},
'outputSelection': {'*': {'*': ['evm.bytecode.object', 'metadata']}}
},
'modelCheckerSettings': {
"engine": 'none'
}
}
args = [SOLC_BIN, '--standard-json']

View File

@ -57,11 +57,6 @@ var fs = require('fs')
var compiler = require('./solc-js/wrapper.js')(require('./solc-js/soljson.js'))
function removeSMT(source)
{
return source.replace('pragma experimental SMTChecker;', '');
}
for (var optimize of [false, true])
{
for (var filename of process.argv.slice(2))
@ -69,13 +64,16 @@ for (var optimize of [false, true])
if (filename !== undefined)
{
var inputs = {}
inputs[filename] = { content: removeSMT(fs.readFileSync(filename).toString()) }
inputs[filename] = { content: fs.readFileSync(filename).toString() }
var input = {
language: 'Solidity',
sources: inputs,
settings: {
optimizer: { enabled: optimize },
outputSelection: { '*': { '*': ['evm.bytecode.object', 'metadata'] } }
},
"modelCheckerSettings": {
"engine": "none"
}
}
var result = JSON.parse(compiler.compile(JSON.stringify(input)))