Unsoundness for LLVM overrides of functions that return NULL pointers

[brianhuffman]

Here's the C code:

#include <stdint.h>
#include <stdlib.h>

uint64_t *foo () {
	return NULL;
}

int bar () {
	return (foo() == NULL);
}

And the saw-script:

bc <- llvm_load_module "return_null.bc";

let i64 = llvm_int 64;

foo_ov <-
  crucible_llvm_verify bc "foo" [] false
    do {
      crucible_execute_func [];
      x <- crucible_alloc i64;
      crucible_return x;
    }
    z3;

bar_ov0 <-
  crucible_llvm_verify bc "bar" [foo_ov] false
    do {
      crucible_execute_func [];
      crucible_return (crucible_term {{ 0 : [32] }});
    }
    z3;

bar_ov1 <-
  crucible_llvm_verify bc "bar" [] false
    do {
      crucible_execute_func [];
      crucible_return (crucible_term {{ 1 : [32] }});
    }
    z3;

Note that we can prove either that bar always returns 0, or that bar always returns 1, depending on whether we use the override for foo. This is obviously unsound.

When checking the spec that we give here for foo (which has a crucible_alloc in the post-state section) saw ought to check that the returned pointer is actually non-NULL, because when we use the override saw always creates a fresh non-NULL pointer.

[brianhuffman]

This may have been fixed in 8610ae9.

[langston-barrett]

Closed via #750