NULL-checking a pointer argument yields "Proof failed."

[ttaubert]

Assume a function that checks whether its pointer argument is NULL:

uint8_t test(uint8_t* a) {
    return a ? 0 : 1;
}

Now take a SAW script that proves it always returns 0 with a non-null argument:

llvm_verify m "test" [] do {
    llvm_ptr "a" (llvm_array 1 (llvm_int 8));
    a <- llvm_var "*a" (llvm_array 1 (llvm_int 8));
    llvm_return {{ 0:[8] }};
    llvm_verify_tactic abc;
};

This however returns "Proof failed.":

Loading module Cryptol
Loading file "test.saw"
When verifying @test:
Proof of return value failed.
Counterexample:
  lss__alloc0: 0
return value
Encountered:  1
Expected:     0
saw: user error (Proof failed.)

Adding llvm_assert_eq "*a" {{ [0:[8]] }}; to fix the input argument to a specific value doesn't help here either. The only way to make this work seems currently to remove the NULL-check.

[ttaubert]

It seems that there's a related bug with:

bool test(uint8_t* a, uint8_t* b) {
    return a == b;
}

Although (I assume) the simulator allocates two arrays when verifying, the function always returns true.

[atomb]

The issue going on here is that the return value from an allocation is currently just a free variable. There's no constraint that is isn't equal to some specific constant (say zero), or that it isn't equal to any other pointer. In the second example, it's not possible to prove that the function returns either true or false.

[atomb]

This is partly fixed. We now assume that pointers declared in a spec passed to llvm_verify are non-null. We don't yet assume that they point to non-overlapping regions of memory, however, so the second example will still fail to prove.

Note that this is a lack of completeness rather than a lack of soundness. We can't exploit this issue to prove a program correct that is not correct. But we may not be able to prove a correct program to be correct.

[TomMD]

Notice this issue appears in a different form with the crucible backend. I believe a faithful translation is:

load_crucible_llvm_module "test.bc";

crucible_llvm_verify "test" [] false
    do {
        aptr <- crucible_fresh_pointer (llvm_array 1 (llvm_int 8));
        a <- crucible_fresh_var "a" (llvm_array 1 (llvm_int 8));
        crucible_points_to aptr (crucible_term a);
        crucible_return (crucible_term {{ 0:[8]}});
        }
    do { abc; };

Which yields:

Loading module Cryptol
Loading file "/private/tmp/test.saw"
saw: user error ("crucible_llvm_verify" (/private/tmp/test.saw:3:1):
"crucible_points_to" (/private/tmp/test.saw:7:9):
typeOfSetupValue: Unresolved prestate variable:AllocIndex 0)

[brianhuffman]

With some small changes, the example works: Change crucible_fresh_pointer to crucible_alloc, and add a crucible_execute_func statement.

crucible_llvm_verify "test" [] false
    do {
        aptr <- crucible_alloc (llvm_array 1 (llvm_int 8));
        a <- crucible_fresh_var "a" (llvm_array 1 (llvm_int 8));
        crucible_points_to aptr (crucible_term a);
        crucible_execute_func [aptr];
        crucible_return (crucible_term {{ 0:[8]}});
        }
    do { abc; };

We seriously need to improve the error messages, though. SAW should inform the user that crucible_points_to cannot be used with a crucible_fresh_pointer-derived pointer on the lhs. Also SAW should report when the crucible_execute_func statement is missing.

[atomb]

The error messages are more informative now. Without the crucible_execute_func, we get:

Argument 0 unspecified when verifying "test"

And, before replacing crucible_fresh_pointer with crucible_alloc, we get:

[19:02:36.496] Loading file "/Users/atomb/galois/saw-script/misc/issue120/test.saw"
[19:02:36.581] Verifying test ...
[19:02:36.581] Simulating test ...
[19:02:36.583] Checking proof obligations test ...
[19:02:36.727] Subgoal failed: test safety assertion:
internal: error: in _SAW_verify_prestate
Memory store failed
Details:
  The region wasn't allocated, wasn't large enough, or was marked as readonly

[19:02:36.727] SolverStats {solverStatsSolvers = fromList ["SBV->Yices"], solverStatsGoalSize = 29}
[19:02:36.727] ----------Counterexample----------
[19:02:36.727] <<All settings of the symbolic variables constitute a counterexample>>
[19:02:36.727] ----------------------------------
[19:02:36.727] Stack trace:
"llvm_verify" (/Users/atomb/galois/saw-script/misc/issue120/test.saw:3:1-3:12):
Proof failed.