search

ethereum / solidity

Solidity, the Smart Contract Programming Language
https://soliditylang.org
GNU General Public License v3.0
22.67k stars 5.62k forks source link

SMTChecker: Upgrade CVC4 to cvc5 and switch from API to SMT-LIB2 interface #15078

Closed blishko closed 3 weeks ago

blishko commented 1 month ago

Instead of compiling solc itself with CVC4 support, it is now enough to have cvc5 executable on PATH when running the compiler. Instead of using API of CVC4, we now use SMT-LIB2 interface. That means we write the queries to temporary SMT-LIB2 files and call the solver process directly to run on the file.

Depends on https://github.com/ethereum/solidity/pull/15102

blishko commented 4 weeks ago

Very minor comments + let's update the changelog and remove references to CVC4 in cmake/toolchain and config.yml.

Added an entry to changelog and removed the missed references to CVC4. Thanks!

r0qs commented 3 weeks ago

Why don't we merge into develop?

Not sure if this was already answered, but the reason is because this PR relies on cvc5 being installed on the images used by the CI. Thus it depends on https://github.com/ethereum/solidity/pull/15102 being merged first.

blishko commented 3 weeks ago

Looks good to me, but I believe we also need to update solc-js. For instance, see: https://github.com/ethereum/solc-js/blob/fa19cf85208d24f10e29646f6e33b1ce23719341/smtsolver.ts#L21

Hmm, OK, yes, we should probably do that. Even though, it is probably an independent thing, if I understand it correctly, no?

r0qs commented 3 weeks ago

Looks good to me, but I believe we also need to update solc-js. For instance, see: https://github.com/ethereum/solc-js/blob/fa19cf85208d24f10e29646f6e33b1ce23719341/smtsolver.ts#L21

Hmm, OK, yes, we should probably do that. Even though, it is probably an independent thing, if I understand it correctly, no?

Yes, it is independent. I just wanted to highlight it here. It will just be a matter of changing the settings and the documentation. I tested solc-js with your branch, and it works fine. We might want to add some tests to solc-js for this, although we currently don't have CI tests for Z3 there either.