macOS saw "resource vanished (Broken pipe)" on failed verification

[dylanmc]

Consider the following C code (zero.c):

#include <stdint.h>
#include <stddef.h>
#include <stdbool.h>

void zero_ptr(uint32_t *x) {
//    if (*x != 123)  // <- injectable bug
      *x = 0;
}

bool zero_spec(uint32_t x) {
    zero_ptr(&x);
    return (x == 0);
}

and the following saw code (zero.saw):

swapmod <- llvm_load_module "zero.bc";

let zero_is_ok = do {
    x <- crucible_fresh_var "x" (llvm_int 32);
    crucible_execute_func [crucible_term x];
    crucible_return ( crucible_term {{ 1 : [1] }});
};

crucible_llvm_verify swapmod "zero_spec" [] true zero_is_ok abc;

On macOS, saw zero.saw succeeds without the injected bug, but if I remove the comments before if (*x != 123), rebuild the zero.bc, and re-run saw zero.saw, I get the following on macOS:

% saw zero.saw 

[19:38:26.457] Loading file "...zero-git.saw"
[19:38:26.485] Verifying zero_spec ...
[19:38:26.486] Simulating zero_spec ...
[19:38:26.495] fd:4: hFlush: resource vanished (Broken pipe)

While the running the same command on Linux saw successfully yields the sought-after counterexample:

% saw zero.saw 

[19:38:19.771] Loading file "...zero-git.saw"
[19:38:19.792] Verifying zero_spec ...
[19:38:19.793] Simulating zero_spec ...
[19:38:19.798] Checking proof obligations zero_spec ...
[19:38:19.846] Subgoal failed: zero_spec safety assertion:
Literal equality postcondition
Expected term: let { x@1 = Cryptol.TCNum 1
    }
 in Cryptol.ecNumber x@1
      (Prelude.Vec 1 Prelude.Bool)
      (Cryptol.PLiteralSeqBool x@1)
Actual term:   Prelude.ite
  (Prelude.bitvector 1)
  (Prelude.and
     (Prelude.bvEq 32
        (Prelude.bvNat 32 123)
        x)
     (Prelude.not
        (Prelude.bvEq 32
           (Prelude.bvNat 32 0)
           x)))
  (Prelude.bvNat 1 0)
  (Prelude.bvNat 1 1)

in _SAW_verify_prestate at /vagrant/zero-git.saw:9:1

[19:38:19.851] SolverStats {solverStatsSolvers = fromList ["ABC"], solverStatsGoalSize = 52}
[19:38:19.851] ----------Counterexample----------
[19:38:19.851]   x: 123
[19:38:19.852] ----------------------------------
[19:38:19.852] Stack trace:
"crucible_llvm_verify" (/vagrant/zero-git.saw:9:1-9:21):
Proof failed.

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 or yices as the prover.

Version info on both macOS and Linux:

 ┏━━━┓━━━┓━┓━┓━┓
 ┃ ━━┓ ╻ ┃ ┃ ┃ ┃
 ┣━━ ┃ ╻ ┃┓ ╻ ┏┛
 ┗━━━┛━┛━┛┗━┛━┛ version 0.6 (9403144-dirty)

[robdockins]

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.

[dylanmc]

How do I turn off path-sat?

[robdockins]

The fourth boolean flag to crucible_llvm_verify

[dylanmc]

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.

[robdockins]

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!

[dylanmc]

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.

[robdockins]

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?

[dylanmc]

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.

[robdockins]

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

[dylanmc]

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.

[robdockins]

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.

[dylanmc]

Aha - that's it. I have a 2010 Mac Pro. Huh!

[dylanmc]

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.