:s prover=any problems

[weaversa]

I really like the idea of :s prover=any, but when one SMT solver segfaults (usually CVC4) when trying to prove a property using :s prover=any, unknown is returned rather than waiting for one of the other solvers to return.

I suggest ignoring the segfaulting solvers, especially those necessary for Cryptol to run as we can't not have them in our path. Giving the result of the first successful solver, if any.

It would also be nice to know which solver(s) segfaulted, and which solver returned the result. I see now that this information is available via :s debug=on

[weaversa]

Here is an example from the DES.cry in the examples directory:

DES> :s prover=cvc4
DES> :prove \k -> \p -> DES.decrypt k (DES.encrypt k p) == p
*** An error occurred.
***  Failed to start the external solver: fd:5: hFlush: resource vanished (Broken pipe)
***  Make sure you can start "/opt/local/bin/cvc4"
***  from the command line without issues.
DES> :s prover=abc
DES> :prove \k -> \p -> DES.decrypt k (DES.encrypt k p) == p
Q.E.D.
DES> :s prover=any
DES> :prove \k -> \p -> DES.decrypt k (DES.encrypt k p) == p
*** An error occurred.
***  Failed to start the external solver: fd:5: hFlush: resource vanished (Broken pipe)
***  Make sure you can start "/opt/local/bin/cvc4"
***  from the command line without issues.

[weaversa]

@LeventErkok is this an SBV thing rather than a Cryptol thing?

[LeventErkok]

My guess is actually that it's a CVC4 thing.

Can you generate the SMT-File in offline mode from Cryptol, and feed it directly to CVC4? I'm guessing you'll see CVC4 choking on it.

When prover "any" is chosen, SBV runs all the provers and gets the result of the first. But strictly speaking, it gets the result of the first one to say something. Even if what they say is "I segfaulted." I'm not sure if there's a portable/reliable way to detect that and wait for one that produces a real result; @acfoltzer might have a better idea on how to go about that.

[acfoltzer]

Do the tools have any standards about which exit codes they return? CVC4 at least returns exit code 0 for both sat and unsat results when reading from a script, while @weaversa's example returns exit code 134 (this might be platform-dependent actually). Maybe SBV could check for non-zero exit codes and ignore/report errors for those results while letting the other solvers continue?

[acfoltzer]

Also feel free to keep talking about this here, but I'm going to close it as a Cryptol issue because it's on the SBV side.

[LeventErkok]

When you get a seg-fault (which I thought was the case here), I don't think there's an exit-code associated, is there?

On Mon, Mar 16, 2015 at 11:32 AM, Adam C. Foltzer notifications@github.com wrote:

Closed #187 https://github.com/GaloisInc/cryptol/issues/187.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/187#event-255906542.

[weaversa]

seg-faults give some standard non-zero exit code like 11 or 139, depending on OS and type of fault.

[LeventErkok]

I honestly am not sure what the right behavior should be here. I don't want to over-engineer the code so we can handle all sorts of situations on all platforms; whatever solution we come up with it'll be problematic on some other platform.

Also, perhaps this is the right thing to do as you'd like to know if one of your solvers actually choked? If SBV silently ignored it, you can go without noticing a solver falling into the cracks for long periods of time.

Perhaps the best thing to do is to extract the SMTLib file in off-line mode, and directly send it to the CVC4 folks. I'm sure they'd love to see it, and it'd be the "right" thing to do anyways.

[acfoltzer]

My recommendation would be to ignore any solver that returns a non-zero exit code, maybe printing something to stderr and saving the SMTLIB to a temp directory for ease of bug reporting. That's not too platform-dependent, but should prevent buggy solvers from bringing down a whole run.

[LeventErkok]

Alas some solvers actually use non-zero exit codes to indicate SAT/UNSAT/UNKNOWN. (I know CVC4 and Boolector does, perhaps others.) SBV actually has code to deal with that. See here: https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Provers/CVC4.hs#L73

Your idea still has some merit; after solver specific exit-code mangling, we can require the exit code to be a "Successfully completed one." Perhaps proveWithall/satWithAll takes an extra argument to tell it how to behave for non-successful exit codes. Whatever works the best for you and @weaversa. Patches are welcome!

[acfoltzer]

According to that link, CVC4 (thankfully) no longer does this. Maybe we can prod the Boolector folks to get on board with reasonable exit code behavior as well?

[LeventErkok]

Ah; most excellent!

I'll scour the code tonight to see what other provers do this and perhaps @weaversa can twist some arms..

On Tue, Mar 17, 2015 at 11:01 AM, Adam C. Foltzer notifications@github.com wrote:

According to that link, CVC4 (thankfully) no longer does this. Maybe we can prod the Boolector folks to get on board with reasonable exit code behavior as well?

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/187#issuecomment-82500695.

[weaversa]

boolector exit codes:

#define BOOLECTOR_UNKNOWN 0
#define BOOLECTOR_SAT 10
#define BOOLECTOR_UNSAT 20

[weaversa]

cvc4 and abc return 0 on all 3.

[weaversa]

yices-smt returns 0 as well.

[LeventErkok]

@weaversa Thanks Sean.. I wonder if Boolector folks can be convinced to follow the crowd. Here's the relevant remark from CVC4 folks: http://cvc4.cs.nyu.edu/wiki/User_Manual#Exit_status

[weaversa]

I can't get cryptol to notice z3. What version is supported? I have tried z3 v. 4.0 from homebrew/science/z3

[LeventErkok]

that's way too old. try this one: http://z3.codeplex.com/downloads/get/1436284

On Tue, Mar 17, 2015 at 11:39 AM, weaversa notifications@github.com wrote:

I can't get cryptol to notice z3. What version is supported? I have tried z3 v. 4.0 from homebrew/science/z3

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/187#issuecomment-82517081.

[weaversa]

Great! Works!

z3 also exits 0.

[weaversa]

mathsat from here: http://mathsat.fbk.eu/download.html causes Cryptol> :s prover=mathsat to hang.

[weaversa]

The command issued is: mathsat -input=smt2, but mathsat doesn't seem to accept the flag. Removing the flag -input=smt2 fixes the problem for me.

And, exits with 0 for SAT and UNSAT.

[LeventErkok]

my mathsat version is probably way too old.. I'll upgrade when I get home and fix SBV accordingly. In the meantime SBV_MATHSAT_OPTIONS should do the trick.

On Tue, Mar 17, 2015 at 11:56 AM, weaversa notifications@github.com wrote:

The command issued is: mathsat -input=smt2, but mathsat doesn't seem to accept the flag. Removing the flag -input=smt2 fixes the problem for me.

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/cryptol/issues/187#issuecomment-82527746.

[LeventErkok]

@weaversa Unfortunately the most recent MathSAT seems to have flushing issues; i.e., it's not -input=smt2 that needs to change. (I'm assuming you conducted your test over the command line?) It works when used from the terminal since all terminal connections are unbuffered, but not from SBV which uses a bi-directional unix pipe.

Unfortunately MathSAT isn't open-source and there does not seem to be a bug/issue tracker.. I did send a note to them to see if we can get a resolution. So; do not upgrade to MathSAT 5.3.4 just yet if you want to use it from Cryptol; though I suspect this is not a big deal.