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

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.

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.

r0qs · 2024-06-07T11:49:01Z

.circleci/config.yml

@@ -1104,7 +1104,7 @@ jobs:
    environment:
      <<: *base_ubuntu2204_large_env
      CMAKE_BUILD_TYPE: Debug
-      CMAKE_OPTIONS: -DCMAKE_CXX_STANDARD=20 -DUSE_CVC4=OFF


Wait, doesn't this mean that cvc5 will be used if found? Should this be the default behavior now in these images?

cvc5 will be used only in tests that explicitly request it.
It is now runtime dependency, not a compile-time dependency, as CVC4 was.

Not sure what you mean by default behaviour. As I understand it, default behaviour does not change.

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?

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 added 4 commits May 29, 2024 15:40

Split docker run command in Dockerfile.emscripten

0276f8c

Upgrade to cvc5 in buildpack-deps

8eabdd1

Bump docker image versions

2f0a799

Install cvc5 on OSX

4a27b84

r0qs mentioned this pull request May 29, 2024

Install cvc5 in buildpack-deps #15102

Open

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 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 added 3 commits June 6, 2024 13:04

Update CI images

a20bc83

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

nikola-matic 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

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

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

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

r0qs Jun 7, 2024

blishko Jun 7, 2024

blishko commented Jun 7, 2024

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

Are you sure you want to change the base?

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

Conversation

blishko commented May 6, 2024 • edited by r0qs

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

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

blishko commented Jun 7, 2024

blishko commented May 6, 2024 •

edited by r0qs

pgebal left a comment •

edited