Unsoundness for LLVM functions that return non-fresh pointers

[brianhuffman]

This is a similar bug to #640, but without using NULL.

Here's the C code:

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

uint64_t *foo (uint64_t *x) {
	return x;
}

int bar (uint64_t *x) {
	return (x == foo(x));
}

And here's the saw-script, which can prove both that bar always returns 0 and that bar always returns 1:

bc <- llvm_load_module "return_same.bc";

let i64 = llvm_int 64;

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

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

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

The problem is that the verification of foo should fail, as the spec says that the return value of foo should be a freshly-created pointer, while it has actually copied the pointer from an input argument. To be sound, we need to check that supposedly-fresh pointers are actually disjoint from all other pointers in scope.

[brianhuffman]

Here's another variation, using addresses of globals instead of pointers from input arguments.

Here's the C code:

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

uint64_t glob;

uint64_t *foo () {
	return &glob;
}

int bar () {
	return (&glob == foo());
}

and the saw-script, which again proves that bar returns 0 and returns 1:

bc <- llvm_load_module "return_global.bc";

let i64 = llvm_int 64;

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

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

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

[brianhuffman]

The second example here, involving globals, was fixed by PR #752 (4912fdd), which also fixed issue #642. We should still add a test for it, though.

The unsound example in the original post is still accepted by saw, however.

[brianhuffman]

The situation is a bit different if the global is declared const. In this case, saw will happily verify a spec saying that the return pointer is a fresh immutable pointer instead of a reference to the global:

const uint64_t glob;

const uint64_t *foo () {
	return &glob;
}

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

But in this case, verifying such a spec is not actually a problem, as our LLVM memory model explicitly allows immutable regions to alias each other and forbids comparing const pointers. So you can't actually do anything unsound with an override like this one.