:s prover=abc not working

[jpziegler]

With a fresh abc build from Github:

Running with the sbv invocation seems to work fine. And it's in my path.

$ abc -S "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"
^C

But Cryptol (2.9.1 release in this case, but also in master) doesn't recognize it, even when it does recognize all the other solvers.

Cryptol> :s prover=abc
Warning: abc installation not found

Possibly relevant: in this case, both abc and Cryptol are built by me on CentOS 7, so if this error isn't occurring elsewhere, it may be a problem on my part. (I haven't tried building them elsewhere.)

[robdockins]

SBV sometimes reports this error if the version of the solver it finds is an incompatible version. FWIW, my current cryptol build seems to be working correctly with my local abc:

$ abc
UC Berkeley, ABC 1.01 (compiled Jun 22 2020 08:10:44)

[atomb]

This issue is showing up in the Docker builds, too. I've confirmed that abc can run on the command line inside the Docker container and has the same version (except for the "compiled" date), but :s prover=abc does not work.

[atomb]

Have you tried running sbvCheckSolverInstallation from the SBV library on that machine, @jpziegler? One hypothesis, based on a quick strace inside our Docker container for Cryptol, is that somehow a SIGCHLD is getting through and causing that function to return False. That function returns False if any exception arises during execution. It would be strange for that not to affect any of the other solvers, though.

[atomb]

I've confirmed that the Docker image I get when I build 2.9.0 and 2.9.1 locally has this problem, even though the images we uploaded to DockerHub for those versions do not have this problem. That holds true even if I restrict the abc checkout to use a version from when those DockerHub images were built. So I think some other dependency may have been updated since then and not have its version pinned.

[atomb]

I've experimented on a Linux machine with this a bit, and noticed that sbvCheckSolverInstallation returns False on any exception. Running the guts of that function, proveWith abc (\x -> sNot (sNot x) .== (x :: SBool)), directly in GHCi yields the following:

*** Exception:
*** Data.SBV: Failed to complete the call to ABC:
***
***
***    Stderr    : double free or corruption (out)
***    Exit code : ExitFailure (-6)
***    Executable: /home/vagrant/bin/abc
***    Options   : -S "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"
***
***    Hint      : Run with 'verbose=True' for further information

So it looks like this is ultimately a bug in ABC. When processing SMT-Lib files, it seems to do a double free, or something related, which triggers checks in GLIBC. Even so, we might be able to work around it.

[atomb]

This issue in the abc repository describes the problem in more detail, and even shows a way to work around it if you want to make a small change to the abc source code and recompile yourself: berkeley-abc/abc#107

[weaversa]

abc is fixed now. Would it be possible for you to reroll the 2.10.0 dockerhub image to include a working abc?

[atomb]

Done! It's on DockerHub now, and I've confirmed that :set prover=abc works with the uploaded image.