Unsound handling of mutability in llvm overrides

[brianhuffman]

Here's the example C file. Function foo takes a pointer that it just uses as scratch space, and then returns its second argument plus one. (It leaves a copy of the result x+1 in the scratch space.) Functions bar and baz are just wrappers around it.

#include <stdint.h>

uint64_t foo (uint64_t *p, uint64_t x) {
	*p = x;
	*p = *p + 1;
	return *p;
}

uint64_t bar (uint64_t *p, uint64_t x) {
	return foo(p, x);
}

uint64_t baz (uint64_t *p, uint64_t x) {
	return bar(p, x);
}

Now here's the saw-script:

bc <- llvm_load_module "invalid.bc";

let i64 = llvm_int 64;

foo_ov <-
  crucible_llvm_verify bc "foo" [] false
    do {
      p <- crucible_alloc i64;
      x <- crucible_fresh_var "x" i64;
      crucible_execute_func [p, crucible_term x];
      crucible_points_to p (crucible_term {{ x + 1 }});
      crucible_return (crucible_term {{ x + 1 }});
    }
    z3;

bar_ov <-
  crucible_llvm_verify bc "bar" [foo_ov] false
    do {
      p <- crucible_alloc_readonly i64;
      x <- crucible_fresh_var "x" i64;
      crucible_execute_func [p, crucible_term x];
      crucible_return (crucible_term {{ x + 1 }});
    }
    z3;

baz_ov <-
  crucible_llvm_verify bc "baz" [bar_ov] false
    do {
      p <- crucible_alloc i64;
      x <- crucible_fresh_var "x" i64;
      y <- crucible_fresh_var "y" i64;
      crucible_points_to p (crucible_term y);
      crucible_execute_func [p, crucible_term x];
      crucible_return (crucible_term {{ x + 1 }});
      crucible_points_to p (crucible_term y);
    }
    z3;

foo_ov is a complete and correct specification of what function foo does.

Then bar_ov cheats: It declares pointer p as read-only, even though function bar passes p to foo, which will write into it. But the verification of bar succeeds, and it uses foo_ov even though it shouldn't work because foo_ov should require its first argument to be a mutable pointer.

Finally, baz_ov completely breaks soundness, as it asserts that the final contents of the scratch buffer p will be unchanged. Using bar_ov as an override, the proof succeeds, but remove the override and the proof will fail as it should.