What does "No overrides had any single concretely or symbolically failing preconditions" mean?

[nano-o]

When verifying a function while providing overrides, SAW sometimes fails with the error "No overrides had any single concretely or symbolically failing preconditions". It is not easy to figure out what this means.

After a discussion on Mattermost a while back, my working hypothesis is that the provided overrides each apply to some part of the symbolic state, but the symbolic state is not covered entirely by the provided overrides. I'm not sure this is accurate though.

Could someone help clarify this and come up with a more informative error message?

[robdockins]

Having briefly looked at the code that generates this message, I also am not entirely sure what situation can cause this to arise. We should refactor/better understand this code so that we can write a more sensible error message here.

[RyanGlScott]

I recently encountered this error message as well, and it took me an extremely long time to figure out what was happening. Here is a minimized example that triggers the error:

// bug.c
#include <stdint.h>

// Invariant: c != 0
void f(uint32_t c) {}

void g(uint32_t c) {
  f(c);
}

// bug.saw

let f_spec = do {
  c <- llvm_fresh_var "c" (llvm_int 32);
  llvm_precond {{ c != 0 }};

  llvm_execute_func [llvm_term c];
};

let g_spec = do {
  c <- llvm_fresh_var "c" (llvm_int 32);
  // llvm_precond {{ c != 0 }};

  llvm_execute_func [llvm_term c];
};

m <- llvm_load_module "bug.bc";
f_ov <- llvm_unsafe_assume_spec m "f" f_spec;
g_ov <- llvm_verify m "g" [f_ov] false g_spec z3;

$ clang-10 -g -emit-llvm bug.c -c
$ ~/Software/saw-0.9/bin/saw bug.saw

[19:51:05.375] Loading file "/home/rscott/Documents/Hacking/SAW/bug.saw"
[19:51:05.425] Assume override f
[19:51:05.426] Verifying g ...
[19:51:05.426] Simulating g ...
[19:51:05.426] Registering overrides for `f`
[19:51:05.426]   variant `Symbol "f"`
[19:51:05.426] Matching 1 overrides of  f ...
[19:51:05.426] Branching on 1 override variants of f ...
[19:51:05.426] Applied override! f
[19:51:05.427] Symbolic simulation completed with side conditions.
[19:51:05.427] Checking proof obligations g ...
[19:51:05.437] Subgoal failed: g safety assertion:
/home/rscott/Documents/Hacking/SAW/bug.saw:19:9: error: in overrideBranches
No override specification applies for f.
Arguments:
- symbolic integer:  width = 32
No overrides had any single concretely or symbolically failing preconditions.
Run SAW with --sim-verbose=3 to see a description of each override.

[19:51:05.437] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 257}
[19:51:05.438] ----------Counterexample----------
[19:51:05.438]   c: 0
[19:51:05.438] ----------------------------------
[19:51:05.438] Stack trace:
"llvm_verify" (/home/rscott/Documents/Hacking/SAW/bug.saw:19:9-19:20):
Proof failed.

The issue is that g_spec doesn't assert the precondition that c != 0, and commenting back in the relevant llvm_precond line in g_spec will make the proof succeed. I'm not quite sure why SAW claims there are no symbolically failing preconditions, since c != 0 definitely seems like it would qualify. (In my actual proof, I had two very similar fresh variables named c, except that the c that I was making an llvm_precond assertion about in g_spec was actually not the same c as what was being used in f_spec, which made this especially difficult to debug.)