Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[SMTChecker] Solver option #11421

Merged
merged 1 commit into from
Jul 27, 2021
Merged

[SMTChecker] Solver option #11421

merged 1 commit into from
Jul 27, 2021

Conversation

leonardoalt
Copy link
Member

@leonardoalt leonardoalt commented May 20, 2021 •
edited
Loading

Depends on #11289

This PR introduces an option to allow the user to choose the solver they want to run. This is expected to not be used that much, but it's important for SMTChecker runs via the JS callback. That is needed, for example, to run the SMTChecker with other Horn solvers, for example Eldarica which I have been experimenting with.
In the current form, since we have static z3 inside soljson, z3 always runs and the CHC queries are not reported. After this PR, if the chosen solver is smtlib2, the queries will be output (for the callback) even if z3 is available statically. This is basically the goal here.

The refactoring of the solc-js SMTChecker tests ethereum/solc-js#524 depends on this PR, so we point to that PR here.

@leonardoalt leonardoalt mentioned this pull request May 21, 2021
Closed
@leonardoalt
Copy link
Member Author

This needs to install latest z3 binaries for CI when running t_ems_solcjs.

@leonardoalt leonardoalt force-pushed the smt_solver_option branch 2 times, most recently from 004e767 to 740ef2d Compare May 27, 2021 09:52
@leonardoalt
Copy link
Member Author

Need to install a newer z3

@leonardoalt leonardoalt marked this pull request as ready for review May 27, 2021 14:32
@leonardoalt
Copy link
Member Author

Latest development: all the code and tests are ready to be reviewed. The solc-js tests need a newer z3 binary installed to pass, since I changed the circleci script to install it but it's too old on Debian.

hrkrshnn
hrkrshnn reviewed May 31, 2021
View reviewed changes
Copy link
Member

@hrkrshnn hrkrshnn left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good. Did solc-js already support this smt2lib callback?

.circleci/config.yml Outdated
@@ -819,7 +819,7 @@ jobs:
name: Install test dependencies
command: |
apt-get update
apt-get install -qqy --no-install-recommends nodejs npm cvc4
apt-get install -qqy --no-install-recommends nodejs npm cvc4 z3
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why did you have to add z3 now?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

With the smt queries fixed, we can also run it via the solc-js callback by having a solver installed in the system. However, cvc4 does not have a Horn solver so the test is kinda null at the end. I installed z3 so that the solc-js smt callback tests can also run a Horn solver locally. This is still not enough because this installs z3 4.4 cus... Debian. Still have to find a solution to install the same z3 as our tests here

test/tools/fuzzer_common.cpp Outdated Show resolved Hide resolved
scripts/error_codes.py Outdated Show resolved Hide resolved
@leonardoalt
Copy link
Member Author

Looks good. Did solc-js already support this smt2lib callback?

@hrkrshnn Ah, forgot to answer this. Yea solc-js already supports this, but the queries themselves were broken before the last merged PR.

@leonardoalt leonardoalt force-pushed the smt_solver_option branch 3 times, most recently from f88f703 to 36dcdcc Compare June 1, 2021 10:11
@leonardoalt
Copy link
Member Author

I applied the review suggestions.

Open problems:

  • t_ems_solcjs: I changed the docker image so that the solcjs tests have a z3 binary in the system and use that for the tests, but doing so kills the job as z3 runs oom in one of the tests.
  • t_osx_cli: the CLI SMTChecker tests as they are require cvc4 to be available in the compiler (to try different solvers at different times), but installing cvc4 on osx seems to time out on circle CI. One option would be to make this work somehow, or to remove cvc4 from all CLI tests and remove the tests accordingly.

@leonardoalt leonardoalt force-pushed the smt_solver_option branch 2 times, most recently from 0b75703 to 66fa0fe Compare June 7, 2021 10:24
@github-actions
Copy link

github-actions bot commented Jun 7, 2021

solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-7 [solbuildpackpusher/solidity-buildpack-deps@sha256:745495fecc29a087bcd361b632b90501e6e4226049284b874360308e84c8eb0f].

@leonardoalt leonardoalt force-pushed the smt_solver_option branch 8 times, most recently from 7bea780 to fb86d72 Compare July 8, 2021 08:33
@github-actions
Copy link

solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-7 [solbuildpackpusher/solidity-buildpack-deps@sha256:0991e184e2f7e29cc7d4953184baf576f24ec9989295fc7cb47e065f3fdb5567].

cameel
cameel reviewed Jul 16, 2021
View reviewed changes
.circleci/config.yml Outdated Show resolved Hide resolved
docs/smtchecker.rst Outdated Show resolved Hide resolved
docs/smtchecker.rst Outdated Show resolved Hide resolved
docs/smtchecker.rst Outdated Show resolved Hide resolved
libsolidity/formal/ModelCheckerSettings.h Show resolved Hide resolved
test/cmdlineTests/standard_model_checker_solvers_cvc4/output.json Outdated Show resolved Hide resolved
test/externalTests/solc-js/solc-js.sh Outdated Show resolved Hide resolved
test/libsolidity/SMTCheckerTest.cpp Outdated Show resolved Hide resolved
test/libsolidity/SMTCheckerTest.cpp Outdated Show resolved Hide resolved
test/solc/CommandLineParser.cpp Show resolved Hide resolved
@leonardoalt leonardoalt force-pushed the smt_solver_option branch 4 times, most recently from f2619a3 to 0014237 Compare July 26, 2021 13:47
@leonardoalt
Copy link
Member Author

The solc-js tests with tests for external calls, invariants and loops look good, takes 4 min which is a good amount.

@leonardoalt
Copy link
Member Author

Can just squash everything at the end

cameel
cameel previously approved these changes Jul 27, 2021
View reviewed changes
Copy link
Member

@cameel cameel left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The only two remaining issues are the ignored error codes from cmdline tests (which might just be a problem unrelated to this PR) and the error message (which is just a minor thing) so I'm already marking it as approved regardless of how they're eventually resolved.

@leonardoalt
Copy link
Member Author

Changed the error message and squashed.

@leonardoalt leonardoalt merged commit 57092b2 into develop Jul 27, 2021
@cameel cameel mentioned this pull request Aug 6, 2021
Merged
@leonardoalt leonardoalt deleted the smt_solver_option branch May 12, 2022 08:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hrkrshnn hrkrshnn hrkrshnn left review comments

@cameel cameel cameel approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@leonardoalt @cameel @hrkrshnn