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

blishko · 2024-05-06T17:06:02Z

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 #15102

ekpyron · 2024-06-03T12:47:25Z

CMakeLists.txt

+find_program(CVC5_PATH cvc5)
+if (CVC5_PATH)
+  add_compile_definitions(CVC5_PATH=${CVC5_PATH})
+  message("cvc5 SMT solver found. This enables optional SMT checking with cvc5.")
 endif()


I was about to say that this is bad, since if you then use CVC5_PATH somewhere, it'll get the path hardcoded - but you actually don't use it anywhere, right :-)? So the add_compile_definitions is superfluous anyways?

Should we even have any kind of cmake logic here? I've not looked at the rest of the PR yet, but I'd guess that CVC5 is purely a runtime dependency with the change, so we don't need to do anything special at cmake configure time, do we?

That's a good point. I thought we need to give some sort of a message at configuration time, but most likely we don't.
Yes, cvc5 is now a runtime dependency. It works the same way as Eldarica, so basically the executable must be present in PATH.

I'll remove this cmake logic.

I am wondering about the message below, which warns if Z3 nor CVC4 (now cvc5) is not enabled/has not been found.

Should there be any information/warning at cmake configure time about available solvers?

nikola-matic

I've re-run the failing windows bytecode builds since they were failing (network err).

nikola-matic · 2024-06-04T08:08:05Z

libsmtutil/CHCSmtLib2Interface.h

@@ -79,17 +78,19 @@ class CHCSmtLib2Interface: public CHCSolverInterface
 	/// Translates CHC solver response with a model to our representation of invariants. Returns None on error.
 	std::optional<smtutil::Expression> invariantsFromSolverResponse(std::string const& response) const;

+	/// Hook to setup external solver call
+	virtual void setupSmtCallback() {}


Should probably smtAssert(false) here.

We cannot do that yet, because --model-checker-solvers smtlib2 is a valid option now, and it will instantiate this base class.
What will happen is that it will try to call SMTCommand, but that will do nothing.

I think eventually we should just drop smtlib2 as a possible choice for the solver (once also z3 migrates to the new usage).

libsmtutil/SMTPortfolio.cpp

nikola-matic · 2024-06-04T08:24:38Z

libsolidity/formal/EldaricaCHCSmtLib2Interface.h

+protected:
+	void setupSmtCallback() override;
+
+	bool m_computeInvariants;


This can be private, no?

Change to private both in EldaricaCHCSmtLib2Inteface and in Cvc5SmtLib2Interface.

pgebal

Why don't we merge into develop?

There are still some references to CVC4 in config.yml and in some files cmake/toolchains dir. Search for CVC4 in all files in the repo.

pgebal

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

libsolidity/formal/Cvc5SMTLib2Interface.cpp

libsolidity/formal/EldaricaCHCSmtLib2Interface.cpp

pgebal · 2024-06-05T09:42:55Z

libsolidity/interface/SMTSolverCommand.cpp

+	else
+	{
+		m_arguments.push_back("--rlimit");
+		m_arguments.push_back(std::to_string(12000));


Optionally we could define 12000 as a named constant so it's not buried here.

Where do you suggest to put the constant?

I admit I don't know what's the best place. First I thought about using #define, but I've learned it's not recommended. We can leave it like it is now.

blishko · 2024-06-05T10:22:23Z

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!

Changelog.md

r0qs

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

r0qs · 2024-06-07T11:20:13Z

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 #15102 being merged first.

.circleci/config.yml

blishko · 2024-06-07T14:30:37Z

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 · 2024-06-10T11:19:27Z

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.

The base branch was changed.

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.

We are using SMTCommand inside UniversalCallback to call external solvers on queries produced my our engines. Previous mechanism set the external solver once during initialization and it was not possible to change it later. This meant, that it would not be possible to use, e.g., Eldarica and cvc5 at the same time. Here we move the proper setup for SMTCommand just before we call it. This setup is customized by subclasses of (CHC)SmtLib2Interface, which call corresponding external solvers.

blishko force-pushed the smt-cvc4-switch branch 2 times, most recently from efbf366 to 06f5be1 Compare May 8, 2024 15:07

blishko force-pushed the smt-cvc4-switch branch from 06f5be1 to d68a87e Compare May 15, 2024 17:11

blishko changed the title ~~SMTChecker: Switch CVC4 from API to SMT-LIB2 interface~~ SMTChecker: Upgrade CVC4 to cvc5 and switch from API to SMT-LIB2 interface May 15, 2024

blishko force-pushed the smt-cvc4-switch branch 4 times, most recently from dbe0d74 to e2de0dd Compare May 15, 2024 19:02

r0qs added has dependencies The PR depends on other PRs that must be merged first smt labels May 22, 2024

r0qs mentioned this pull request May 29, 2024

Install cvc5 in buildpack-deps #15102

Merged

blishko force-pushed the smt-cvc4-switch branch from e2de0dd to 81f5d22 Compare May 29, 2024 17:50

blishko changed the base branch from develop to install-cvc5 May 29, 2024 17:51

blishko marked this pull request as ready for review May 29, 2024 17:57

blishko force-pushed the smt-cvc4-switch branch 3 times, most recently from 06653aa to 012532d Compare June 3, 2024 06:43

ekpyron reviewed Jun 3, 2024

View reviewed changes

nikola-matic self-requested a review June 3, 2024 13:29

blishko force-pushed the smt-cvc4-switch branch from 012532d to 6ef4abc Compare June 3, 2024 16:36

nikola-matic reviewed Jun 4, 2024

View reviewed changes

blishko force-pushed the smt-cvc4-switch branch from 6ef4abc to e7edbe1 Compare June 4, 2024 12:18

pgebal self-requested a review June 4, 2024 15:27

pgebal reviewed Jun 5, 2024

View reviewed changes

pgebal requested changes Jun 5, 2024

View reviewed changes

blishko force-pushed the smt-cvc4-switch branch from e7edbe1 to 9ad7f1d Compare June 5, 2024 10:21

pgebal previously approved these changes Jun 5, 2024

View reviewed changes

nikola-matic reviewed Jun 6, 2024

View reviewed changes

Changelog.md Show resolved Hide resolved

blishko force-pushed the smt-cvc4-switch branch from 9ad7f1d to 1735786 Compare June 6, 2024 11:05

nikola-matic previously approved these changes Jun 6, 2024

View reviewed changes

r0qs force-pushed the install-cvc5 branch from 4a27b84 to 128b172 Compare June 6, 2024 15:56

r0qs reviewed Jun 7, 2024

View reviewed changes

.circleci/config.yml Show resolved Hide resolved

r0qs mentioned this pull request Jun 10, 2024

Update cvc4 to cvc5 ethereum/solc-js#741

Merged

Base automatically changed from install-cvc5 to develop June 11, 2024 06:51

blishko added 3 commits June 11, 2024 08:52

Update CI images

025f9a2

blishko force-pushed the smt-cvc4-switch branch from 1735786 to 20ae0f2 Compare June 11, 2024 06:53

nikola-matic approved these changes Jun 11, 2024

View reviewed changes

blishko enabled auto-merge June 11, 2024 07:27

blishko merged commit 07f25f5 into develop Jun 11, 2024
72 checks passed

blishko deleted the smt-cvc4-switch branch June 11, 2024 07:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

blishko commented May 6, 2024 •

edited by r0qs

Loading

ekpyron Jun 3, 2024

blishko Jun 3, 2024

blishko Jun 3, 2024

nikola-matic left a comment

nikola-matic Jun 4, 2024

blishko Jun 4, 2024

nikola-matic Jun 4, 2024

blishko Jun 4, 2024

pgebal left a comment

pgebal left a comment •

edited

Loading

pgebal Jun 5, 2024

blishko Jun 5, 2024

pgebal Jun 5, 2024

blishko commented Jun 5, 2024

r0qs left a comment

r0qs commented Jun 7, 2024

blishko commented Jun 7, 2024

r0qs commented Jun 10, 2024 •

edited

Loading

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

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

Conversation

blishko commented May 6, 2024 • edited by r0qs Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikola-matic left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pgebal left a comment

Choose a reason for hiding this comment

pgebal left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

blishko commented Jun 5, 2024

r0qs left a comment

Choose a reason for hiding this comment

r0qs commented Jun 7, 2024

blishko commented Jun 7, 2024

r0qs commented Jun 10, 2024 • edited Loading

blishko commented May 6, 2024 •

edited by r0qs

Loading

pgebal left a comment •

edited

Loading

r0qs commented Jun 10, 2024 •

edited

Loading