Set up a scheme for solver version constraints

[langston-barrett]

I experienced a cryptic error message when using Yices 2.6.0 that went away when I installed Yices 2.6.1. We should probably fail early and notify users that this version is necessary.

[kquick]

Do you happen to have the error handy?

[langston-barrett]

@kquick The error came from here:

user error ("verify" (/home/siddharthist/code/fizz-hkdf/main.saw:122:21-122:27):
"crucible_llvm_verify" (/home/siddharthist/code/fizz-hkdf/base.saw:24:34-24:54):
Could not parse acknowledgement result.
*** Exception: Parse exception: Failed reading: empty
)

[langston-barrett]

Looks like using SBV's getInfo would be the best way to figure out what version we're using. Perhaps we can solve this issue with a slightly more generic ability for SAW to impose bounds on the versions for each solver.

[langston-barrett]

I misspoke above: the error comes not from our use of Yices via SBV, but from What4. See the PR linked just above this comment.

[kquick]

Can we extend this easily to versioning for other solvers? For example, we recently discovered an issue that Z3 v4.7.1 works fine for, but which causes Z3 to not terminate for v4.8.1-v4.8.4, so we might want to set some restrictions there as well.

Also, we may want to have some way to override these limits, either via cmdline or configuration file. For example, if the Z3 issue is due to a bug that gets fixed (hypothetically) in 4.8.5, we would want to be able to tell people to update their configuration file to specify "z3-no-allow-versions: 4.8.1--4.8.4" or something like that so that they could use 4.8.5 without requiring a full release from us. If something like this is not trivial to add (e.g. would require adding general configuration file support) then we should discuss further and perhaps handle via a separate feature branch.

[langston-barrett]

@kquick See the PR linked above. I believe the solution I'm looking at there would support your Z3 use case (specifically, for SMTLib2 solvers, it allows setting a key/value mapping of solvers with min/max version bounds).

It would be great to have a Crucible/SAW configuration file to put such options in :-) But right now I don't think that exists. I'd be supportive of adding one.

[atomb]

It occurs to me that, at the moment, SAW is currently hard-coded to use Yices through What4 for path satisfiability checking, and that this is the only place that shows up. I'm somewhat inclined to add a simple test within SAW for Yices versions, and to otherwise leave a more correct fix for this issue for later releases.

[langston-barrett]

@atomb That sounds fine to me, I think a generic solution would take a bit longer than I'd like to spend at the moment.

[atomb]

A fix for this from the SAW perspective is in place in PR #460. I'm going to leave this issue open to track creation of a more generic solution but remove the 0.3 milestone.

[sauclovian-g]

The topic of solver versions and version constraints came up again this week because of some z3 regressions, so maybe it's time we did something about this.