Cannot replicate SMTChecker example output

engn33r commented 2 years ago

Page

https://docs.soliditylang.org/en/v0.8.14/smtchecker.html#assert

Abstract

I cannot replicate the SMTChecker assertion violation output in this example. I can replicate the SMTChecker output in all other examples so I know SMTChecker is working.

Contract code

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.8.0;

contract Max {
    function max(uint[] memory a) public pure returns (uint) {
        require(a.length >= 5);
        uint m = 0;
        for (uint i = 0; i < a.length; ++i)
            if (a[i] > m)
                m = a[i];

        for (uint i = 0; i < a.length; ++i)
            assert(m > a[i]);

        return m;
    }
}

Command I am using to run SMTChecker: solc Max.sol --model-checker-engine chc --model-checker-show-unproved --model-checker-timeout 0 --model-checker-targets "assert"

solc Version: 0.8.14+commit.80d49f37.Linux.g++ (with z3 dynamic library)

My output:

Warning: CHC: Error trying to invoke SMT solver.
  --> Max.sol:13:13:
   |
13 |             assert(m > a[i]);
   |             ^^^^^^^^^^^^^^^^

Warning: CHC: Assertion violation might happen here.
  --> Max.sol:13:13:
   |
13 |             assert(m > a[i]);
   |             ^^^^^^^^^^^^^^^^

Output shown in documentation:

Warning: CHC: Assertion violation happens here.
Counterexample:

a = [0, 0, 0, 0, 0]
 = 0

Transaction trace:
Test.constructor()
Test.max([0, 0, 0, 0, 0])
  --> max.sol:14:4:
   |
14 |            assert(m > a[i]);

Pull request

I have not identified the exact issue yet. If I change the --model-checker-engine argument to all, the BMC checker properly identifies the assertion violation with a counterexample, but the documentation shows the CHC checker should identify the assertion violation. If I change the assert comparison to less than or equals (assert(m >= a[i]); instead of assert(m > a[i]);), the contract compiles without issue and there are no warnings from SMTChecker.

leonardoalt commented 2 years ago

Hi @engn33r , thanks for the report! What's your z3 version? Can you try with a high timeout like 60000 (60s)?

engn33r commented 2 years ago

Thanks for the quick reply! I am using z3 version 4.8.12-1 on an Ubuntu-based system. I tried setting a higher timeout but the error message appears instantly with a zero or much higher timeout. I have seen SMTChecker take much longer when the timeout condition was involved.

I assume you're getting the expected output with the CHC checker? I find it odd that only the BMC checker identifies the assertion violation on my system.

Separate topic, but do you know if the solidity docker image has z3 to allow for SMTChecker to run from the image? If so, I can test this as an alternative.

leonardoalt commented 2 years ago

Yea the output is from CHC. BMC runs much faster but gives a lot of false positives.

The results can be quite sensitive to the z3 versions, a lot changes in between them. So I think if you use a newer z3 (4.8.14 for example) it should work. For instance, soljson.js that Remix uses has an embedded z3. If I run your example with pragma experimental SMTChecker; on Remix it actually gives the counterexample too.

I know Ubuntu ships z3 4.8.12, which is quite unfortunate since the latest is already 4.8.17. If you want a newer z3, Solidity also maintains a z3 package that has the lib and the binary. Just use the PPA https://launchpad.net/~ethereum/+archive/ubuntu/cpp-build-deps and install z3-static.

I'm not sure about the docker version having z3, but I suspect it doesn't.

engn33r commented 2 years ago

I tried uninstalling all other z3 packages/files and then installed z3-static from the ethereum ppa you linked to. I'm now getting a warning of Warning: z3 was selected as a Horn solver for CHC analysis but libz3.so.4.8 was not found. and can't get results for the other example files I've tested against. Did I go overboard in removing z3 files like libz3.so.4.8, or does solc have to be compiled from scratch when using a static z3 library which is my understanding from the docs? So far I've been using the solc-static-linux 0.8.14 binary from the releases page rather than compiling it.

I've tested remix with success, but a local setup would be nice to have.

leonardoalt commented 2 years ago

It doesn't have to be compiled, runtime libs should be enough. Can you check that you have libz3.so in some system default lib dir?

engn33r commented 2 years ago

As far as I can tell, solc is looking specifically for a file named libz3.so.4.8. I only had files named libz3.so and libz3.so.4 in default lib dirs, but manually copying the libz3.so.4 file to libz3.so.4.8 got SMTChecker working again. Based on some installs/reinstalls of individual z3 packages, the libz3-4 ubuntu package added libz3.so.4 while libz3-dev added libz3.so and libz3.so.4. I didn't see any dynamic z3 library added by installing z3-static from the ppa. I tried installing libz3-static-dev from the ppa instead z3-static, but I got the same error where solc warns libz3.so.4.8 was not found. and did not see any new libz3.so file added with either ppa package.

At this point, I'm aware that I can get the proper SMTChecker result for the original example I mentioned with remix. We can close the issue since that is resolved. But if you're willing to continue exploring the proper install process to get a local setup working, even offline (twitter link is in my profile), I would find it helpful. I haven't found clear instructions online for installing a newer z3 dynamic lib and have seen at least one case where solc was compiled from source with static linking to z3 to get SMTChecker working.

leonardoalt commented 2 years ago

We shouldn't rely on Remix here because it doesn't let you change the model checker parameters plus pragma smtchecker will be deprecated in solc 0.9.0. Let's try to get it fixed properly.

I've seen weird lib things happen before on Ubuntu, where the person had 4.8.12 installed and then had problems when installing the one from our PPA. A sane installation should end up with a libz3.so.4.8 in your system, because that's the ABI version. @Marenz you had problems with this recently, was it similar?

engn33r commented 2 years ago

Sounds good, I'd like to aim for outlining the installation steps for getting SMTChecker working on a *nix system. I'll stick to ubuntu for now but can test other distros once we have one set of setup instructions. I'll try using the ethereum z3 ppa on a fresh ubuntu docker image and/or ubuntu VM in case the other system I am using has some non-default configs.

engn33r commented 2 years ago

I tried installing the different packages on a clean ubuntu system. Here are the files/libraries that each package adds to the system.

Default ubuntu packages

libz3-dev adds: libz3.so and libz3.so.4 (additional source: https://ubuntu.pkgs.org/22.04/ubuntu-universe-amd64/libz3-dev_4.8.12-1_amd64.deb.html#howto)
libz3-4 adds: libz3.so.4 (additional source: https://ubuntu.pkgs.org/22.04/ubuntu-universe-amd64/libz3-4_4.8.12-1_amd64.deb.html#howto)

From ppa:ethereum/cpp-build-deps

z3-static adds: /usr/bin/z3
libz3-static-dev adds: .cmake and .h files to /usr/lib

Because I lack knowledge about z3, my questions are:

What package (on any *nix distro) installs a libz3.so.4.8 file to the system? I can look at the "preferred" package that provides this file to see if I can learn why ubuntu is different.
Since I copied the libz3.so.4 file to libz3.so.4.8 and got SMTChecker working on all but one of the examples I tested against (and I don't know if the error is due to the older z3 version 4.8.12 or a difference between libz3.so.4 and libz3.so.4.8), is there a major difference between those two files? If SMTChecker is hardcoded to require libz3.so.4.8, could SMTChecker add libz3.so.4 to the list of z3 libraries it can use?
Is there CI or other testing to confirm the ethereum ppa z3 packages provide a z3 dynamic library? Alternatively, I can look at the ppa z3 build script if it's public.

leonardoalt commented 2 years ago

Arch Linux for example installs
```
usr/lib/libz3.so
usr/lib/libz3.so.4.8
usr/lib/libz3.so.4.8.17.0
```
Now I'm not sure if the dynamic loading ever worked for us on Ubuntu... Trying to summon @ekpyron who may have an answer

The lib files with/without versions should be the same. In fact, usually they're just symbolic links to the full version one. On my system:

$ ls -l libz3.so*
lrwxrwxrwx 1 root root       12 May 12 23:08 libz3.so -> libz3.so.4.8
lrwxrwxrwx 1 root root       17 May 12 23:08 libz3.so.4.8 -> libz3.so.4.8.17.0
-rwxr-xr-x 1 root root 16090048 May 12 23:08 libz3.so.4.8.17.0

If SMTChecker is hardcoded to require libz3.so.4.8, could SMTChecker add libz3.so.4 to the list of z3 libraries it can use?

Not in a safe way. The minor (second) number of a version is the ABI series. This means that while SMTChecker supports the z3 4.8. interfaces, it cannot safely assume that it supports the z3 4.9. interfaces (which would be allowed for libz3.so.4) without any changes. In fact rather the opposite, if that number changes we probably need to adjust the API support.

Actually, it was probably my mistake, sorry about that. Our PPA provides a static z3 which is used by our CI to build a static solc + z3. By now I'm guessing the easiest way to have a newer z3 on Ubuntu is by building it yourself...

engn33r commented 2 years ago

I built z3 from source on ubuntu, but after running sudo make install, I got only one .so file added to the system, libz3.so, so it was effectively the same result as installing the ubuntu packages except for the version number. For one more data point, I installed z3-libs in a fedora container and I got the same result that you do for Arch, with libz3.so.4.8.17.0 and libz3.so.4.8 files added to the system. At this point I would suggest a note be added in the solidity docs stating that ubuntu is not supported for SMTChecker z3 dynamic library loading with a note that states the need for the libz3.so.4.8 library when using the dynamic z3 library option. I can make a PR in a few days unless you'd like to handle this.
Ok, this makes sense. Given I did get some results by copying the libz3.so.4 to libz3.so.4.8, I guess it may sometimes work but it is definitely not how things should work.
Understood, I'll decide whether it will be easier to use docker or a VM with another distro rather than building from source on ubuntu.

ekpyron commented 2 years ago

Interestingly, debian (and thereby ubuntu, since ubuntu uses debian packages) actually patches Z3 sources to adjust its SOVERSION: https://sources.debian.org/patches/z3/4.8.12-1/01-soname.patch/ That patch results in only libz3.so.4 being part of the debian/ubuntu z3 packages, while a regular install from z3 sources will install as libz3.so.4.8.

I'm not quite sure how you built z3 from source on ubuntu and only got libz3.so - I just tried in an ubuntu docker image and built and installed z3 as mkdir build && cmake .. && make && make install and got /usr/local/lib/libz3.so.4.8 as expected...

In any case, this indeed means that dynamic loading of Z3 will fail with the regular debian/ubuntu packages. I'm not quite sure why the debian package maintainers decided to apply this patch - but my guess would be that it is due to Z3 in the past not being particularly concerned with their so versions actually properly indicating binary compatibility (see https://github.com/Z3Prover/z3/issues/6030).

This is a bit unfortunate, though, since this means that we cannot rely on the z3 libraries getting uniform so versions across distributions - I'm not quite sure how best to deal with this...

engn33r commented 2 years ago

I see the Z3 issue linked above has been closed but I have not examined or tested the change myself. Could that resolve the issue on debian/ubuntu?

Another idea that avoids the dynamic z3 library loading is to publish a table that matches the solc release version with the corresponding z3 library version that the solc binary is compiled with. That way debian users can download a solc release version and then download a matching static z3 binary with the correct version. Even if this information about which solc version matches which z3 version is already available somewhere, it might be helpful to make it more easily accessible in the docs.

rori4 commented 1 year ago

I am having the same issue and first of all I don't seem to find a libz3.so.4xx folder in /usr/lib/ when installing z3 on Ubuntu 22.04.2 LTS

Searching the system with find /usr -name "libz3.so*" I got only those folders /usr/lib/x86_64-linux-gnu/libz3.so.4 /usr/lib/x86_64-linux-gnu/libz3.so

I've removed and installed z3 again with the following command sudo apt install z3 and the version is Z3 version 4.8.12 - 64 bit

solc version is 0.8.15 but I have tested a lot of different versions as well without any luck (tested all from 0.8.15 to 0.8.20)

Every time when I try different tests I get either: Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled. Install libz3.so.4.8 to enable Z3.

or

Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.

I've also tested the solc-macos on macOS and it works perfectly but as far as I understand it ships with z3 and on linux its dynamically loaded

EDIT: Ok re-reading again the answers above it seems that its unlikely to make it work on Ubuntu for now

EDIT2: Maybe it will be nice if there is a revision of adding optional builds with Z3 https://github.com/ethereum/solidity/issues/10420

Dynamically loading Z3 doesn't seem to work on Ubuntu

github-actions[bot] commented 1 year ago

This issue has been marked as stale due to inactivity for the last 90 days. It will be automatically closed in 7 days.

github-actions[bot] commented 1 year ago

Hi everyone! This issue has been automatically closed due to inactivity. If you think this issue is still relevant in the latest Solidity version and you have something to contribute, feel free to reopen. However, unless the issue is a concrete proposal that can be implemented, we recommend starting a language discussion on the forum instead.

engn33r commented 1 year ago

I tested the original issue I reported. I'm now getting the expected output as described in the docs. The z3 version I have installed is still 4.8.12-1. The only obvious differences I can think of since my original attempt are:

Installing solc from ppa instead of downloading a binary
Using solc 0.8.21 instead of an older version

No modifying of z3 files were needed to make it work this time. Something must have changed but I'm unsure what.

ethereum / solidity