readonly

[weaversa]

Are crucible_alloc and crucible_alloc_readonly semantically equivalent when used after crucible_execute_func?

[brianhuffman]

I would expect them to behave differently, and there are certain contexts where you'd be able to tell the difference. Let's say you have an outer function that calls a function f, which returns a freshly-allocated pointer, and then that pointer is passed to another function g. If the spec for f uses alloc_readonly in the post-state section, and the spec for g says that the input pointer needs to be writable, then the verification should fail.

[brianhuffman]

Indeed, here's an example that demonstrates the difference:

#include <stdlib.h>

int *f () {
	int *p = malloc(sizeof(int));
	return p;
}

void g (int *p, int x) {
	*p = x;
}

int *foo (int x) {
	int *p = f();
	g(p, x);
	return p;
}

and the saw-script file:

bc <- llvm_load_module "issue689.bc";

let i32 = llvm_int 32;

f_ov <-
  llvm_verify bc "f" [] false
    do {
      llvm_execute_func [];
      p <- llvm_alloc_readonly i32;
      llvm_return p;
    } z3;

g_ov <-
  llvm_verify bc "g" [] false
    do {
      p <- llvm_alloc i32;
      x <- llvm_fresh_var "x" i32;
      llvm_execute_func [p, llvm_term x];
      llvm_points_to p (llvm_term x);
    } z3;

foo_ov <-
  llvm_verify bc "foo" [f_ov, g_ov] false
    do {
      x <- llvm_fresh_var "x" i32;
      llvm_execute_func [llvm_term x];
      p <- llvm_alloc_readonly i32;
      llvm_points_to p (llvm_term x);
      llvm_return p;
    } z3;

The verification of foo fails with a "No override specification applies for g" error message. But if you change the llvm_alloc_readonly in the spec for f to llvm_alloc, then it works just fine.

[brianhuffman]

Is there anything we should do before closing this? Perhaps we could add the above example as part of the integration test suite?