Proper SMT CHC tests #524
Proper SMT CHC tests #524
Conversation
leonardoalt
force-pushed
the
smt_proper_tests
branch
from
2310e72 to
b85d230
Compare
leonardoalt
force-pushed
the
smt_proper_tests
branch
from
b85d230 to
234d815
Compare
| function expectErrors (expectations, errors, ignoreCex) { | ||
| if (errors.length !== expectations.length) { | ||
| return false; | ||
| function collectFiles (testdir) { |
There was a problem hiding this comment.
Just extracted from the main loop
| return sources; | ||
| } | ||
|
|
||
| function createTests (sources, st) { |
There was a problem hiding this comment.
Extracted from the main loop
| return solOutput.errors.filter(error => !error.message.includes('This is a pre-release')).map(error => error.message); | ||
| } | ||
|
|
||
| function expectStringErrors (a, b) { |
There was a problem hiding this comment.
These two functions have the same behavior as before and are only used by the first test.
|
I really don't understand this coverage tool. |
leonardoalt
force-pushed
the
smt_proper_tests
branch
from
234d815 to
a503e5a
Compare
leonardoalt
force-pushed
the
smt_proper_tests
branch
2 times, most recently
from
bd4d84d to
f2b9ac3
Compare
leonardoalt
force-pushed
the
smt_proper_tests
branch
from
f2b9ac3 to
9733e28
Compare
|
@leonardoalt Is this still work in progress or is it just waiting to be reviewed? |
|
Waiting to be reviewed |
smtsolver.js
Outdated
|
|
||
| var potentialSolvers = [ | ||
| { | ||
| name: 'z3', | ||
| params: '-smt2 rlimit=20000000 rewriter.pull_cheap_ite=true fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false' | ||
| params: '-smt2 timeout=' + timeout + ' rewriter.pull_cheap_ite=true fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false' |
There was a problem hiding this comment.
Why time limit and not resource limit?
Ah this is just so that both cvc4/z3 have the same limit.
| @@ -44,7 +45,9 @@ function solve (query) { | |||
| if ( | |||
| !solverOutput.startsWith('sat') && | |||
| !solverOutput.startsWith('unsat') && | |||
| !solverOutput.startsWith('unknown') | |||
| !solverOutput.startsWith('unknown') && | |||
| !solverOutput.startsWith('(error') && | |||
There was a problem hiding this comment.
ah, Eldarica outputs errors in some sort of smtlib sexpr, like (error something failed lalala) which is caught here
|
I suppose #565 needs to be merged first? |
|
Ah yes, this branch is all over the place. Will need to rethink it after the other one gets merged |
|
Closing cus need to rewrite it anyway. |
Depends on ethereum/solidity#11421
This PR adds proper SMTChecker tests. Currently, the SMTChecker tests are actually broken, many tests are ignored, and the smtlib version of the SMTCheckre encoding is not being tests at all.
The main
smtCheckerTestsin this code are mainly used by the Solidityt_ems_solcjsjob, which copies thesmtCheckerTestsinto thesolc-jstests and runstest/smtcallback.jsfrom this repo. It now requiressoljsonversion>=0.7.2because of the warning format.If
soljson < 0.8.5, it runs the staticz3insidesoljsonand compares that to the test expectation.Else, it runs /\ plus a local
z3binary using Solidity'ssmtlib2encoding, and compares all of them.The comparison now is much more precise than before: it compares each output location, which represents a property.
Note that safe properties are not reported, so if one solver reports a location and another doesn't, there's an inconsistency. The exception to this is when this inconsistency happens for the BMC engine, where one solver probably solved it safe with CHC, and another solver couldn't prove it safe with CHC, and reports an unsafe false positive via BMC.
The test only fails if there's a real inconsistency, as opposed to the stronger
soltest. I think that's fair since the JS/smtlib2 environment might give more nondeterministic answers compared to the embedded C++ z3.