Closed dylanmc closed 3 years ago
Do you get the same results if you use a solver other than abc
? What if you turn off path-sat?
EDIT: I see you answered the question about the solver. I'm still interested in the path-sat question. I suspect a configuration issue with your version of yices
on OSX.
How do I turn off path-sat?
The fourth boolean flag to crucible_llvm_verify
Aha. Doing that, I get the following with yices set as the solver:
saw zero-git.saw
[19:57:47.827] Loading file "...zero.saw"
[19:57:47.855] Verifying zero_spec ...
[19:57:47.856] Simulating zero_spec ...
[19:57:47.856] Checking proof obligations zero_spec ...
[19:57:47.870]
*** Data.SBV: fd:5: hGetLine: end of file:
***
*** Sent : (define-fun s1 () (_ BitVec 32) #x0000007b)
***
*** Executable: /Users/dylanjames/bin/yices-smt2
*** Options : --incremental
But with abc
or z3
as the solver, it works as expected. Hmmm.
What is your yices version? It should be 2.6.2.
It would be really nice to check the version of the solver and give more meaningful error messages if they are not in acceptable ranges. This is surprisingly hard to do!
Indeed my yices is 2.6.2. Also, the weirdness is with all three solvers is path-sat is true
, which is weird - I thought it was a safe default to be on.
Right now, the path satisfiability checking code for SAW always uses Yices, regardless of what solver you choose for the final proof steps. This really should be configureable, but currently is not.
As to the underlying problem... that is very strange. Does yices work for you at all if you invoke it manually?
It launches fine and gives me a prompt, but I don't know how to check health beyond that.
Also, when I choose yices
as the solver on a correct zero.c
, it works fine.
This program is simple enough it probably doesn't have to invoke the solver at all when the program is correct.
Try the following interaction:
$ yices-smt2 --incremental
(set-logic QF_AUF)
(push 1)
(assert false)
(check-sat)
unsat
(pop 1)
(check-sat)
sat
Well that's interesting:
% yices-smt2 --incremental
(set-logic QF_AUF)
(push 1)
(assert false)zsh: illegal hardware instruction yices-smt2 --incremental
I'll go download and reinstall yices.
Do you have an older mac? You might have to compile your own yices. The official yices builds assume some relatively new AVX instructions, I believe, and don't have fallback stubs.
Aha - that's it. I have a 2010 Mac Pro. Huh!
And with a freshly-built yices
for my ancient Xeon processors, it's working great. Thanks. I can imagine a small suite of saw scripts that verify health after installation. It's a tall stack of tools! I'll leave it to you what to do, and will close this.
Consider the following C code (
zero.c
):and the following saw code (
zero.saw
):On macOS,
saw zero.saw
succeeds without the injected bug, but if I remove the comments beforeif (*x != 123)
, rebuild thezero.bc
, and re-runsaw zero.saw
, I get the following on macOS:While the running the same command on Linux
saw
successfully yields the sought-after counterexample:The latter behavior is much preferable, IMO. If it matters, I'm creating the
zero.bc
from Linux, since my macOS clang is too new, but the successful verification suggests this is okay.Also, this odd macOS behavior exhibits whether I pass
abc
z3
oryices
as the prover.Version info on both macOS and Linux: