Proper handling of globals in crucible_llvm_verify

[brianhuffman]

Currently, each run of the symbolic simulator in crucible_llvm_verify starts in a memory state where all declared globals are allocated and set to their initial values. This is fine for global constants, but is unsound for mutable global variables: Basically it's like having implicit, unchecked preconditions saying that when the function is called, all globals contain the same values they were initialized with.

We need to run the symbolic simulator with a different initial memory state: Constant globals should all be initialized to their values, but the memory locations for mutable globals should be empty. If a function reads from a global variable foo, then its spec must contain a statement crucible_points_to (crucible_global "foo") rhs in its preconditions in order for the simulation to succeed.

[robdockins]

As part of the LLVM module translation step, there is a special Crucible function generated that specifically sets up the globals with their initial values. This is included in the returned ModuleTranslation in the initMemoryCFG field. Currently, this function is called once when the LLVM module is first loaded (see load_crucible_llvm_module), and not actually at every verification (this is actually worse!).

To achieve what you want, the memory should be produced fresh each verification by calling Crucible.initializeMemory (which only allocates the globals, but does not set their values), but then do NOT call the initMemoryCFG Crucible function. Then, the values of globals will be set in the precondition block iff they are used in a points_to assertion, the same as any other memory.

Probably special support for const global values is warranted, and maybe also for fetching the initial value of globals so they can be mentioned in specifications.

[brianhuffman]

I tried using the result of Crucible.initializeMemory as the initial memory state for crucible_llvm_verify, but it is incredibly inconvenient not to have the values of constant globals available. Any C function that uses literal strings or other literal structured data is compiled to LLVM with constant globals with machine-generated names. I really don't want to have to mention these explicitly in my specs.

We need a variant of initMemoryCFG that initializes only the global constants. The resulting MemImpl could be saved and used as the starting point for every crucible_llvm_verify call.

[brianhuffman]

A related question: Would it make sense for the Crucible LLVM memory model to include a special read-only segment? It would be nice to have a way to ensure that the values of constant globals will never be overwritten at runtime.

[robdockins]

Yes, I think special handling for read-only values is a good idea. In particular, reads from read-only data should never alias with symbolic writes, so they can be made much more efficient.

[langston-barrett]

This has been partially addressed in master. It seems that global variables are indeed allocated but not initialized (what @brianhuffman suggests in the opening comment). However, the user experience is pretty poor, because the error message is long and doesn't say anything explicitly about globals (see #307 for the error message I encountered).

It would be nice to be able to say "this global variable should be initialized to what it is initialized to in the code" as @robdockins suggests. Even if the variable is mutable, this could be done in a _setup function so that the precondition is explicit.

[langston-barrett]

I was mistaken when I said that global values are not currently initialized. This is not currently implemented at all (all globals are allocated and initialized at the start of every verification), but I am working on the solution outlined above.

[langston-barrett]

This was fixed in #311

[langston-barrett]

While #311 improved the situation, it's still easy to create an unsound proof. In the following, the preconditions are met for the override for f (namely, glob is initialized). That override is then used for rewriting, but its side-effect on the value of glob is skipped. Thus, the proof for g succeeds, even though the spec is incorrect.

/*
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; clang_7" --run "clang -O0 -emit-llvm -c *.c"
  nix-shell --pure -p "with import (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/nixos-19.03.tar.gz) {}; llvm_7" --run "llvm-dis *.bc"
*/

int glob = 42;

int f(int x) {
  glob = 55;
  return x + x;
}

int g(int x) {
  f(x);
  return glob;
}

int main() {
  return g(5);
}

m <- llvm_load_module "test.bc";

let init_global name = do {
  crucible_points_to (crucible_global name) (crucible_global_initializer name);
};

let f_spec = do {
  init_global "glob";
  x <- crucible_fresh_var "x" (llvm_int 32);
  crucible_execute_func [crucible_term x];
  crucible_return (crucible_term {{ 2 * x : [32] }});
};

let g_spec = do {
  init_global "glob";
  x <- crucible_fresh_var "x" (llvm_int 32);
  crucible_execute_func [crucible_term x];
  crucible_return (crucible_term {{ 42 : [32] }});
};

f_spec <- crucible_llvm_verify m "f" [] false f_spec z3;
crucible_llvm_verify m "g" [f_spec] false g_spec z3;

One solution would be to require specifications for global variables to come in pairs, so that whenever you have a precondition specifying the value of a global variable, there is an implicit postcondition that it remains constant, unless you specify explicitly how it changes.

[atomb]

This happens to be true for all assignments that a function may make, not just those to globals. See #30. I think it's fine to release 0.3 without fixing that, but I want to fix it in time for 1.0.

[langston-barrett]

Yes, this seems like a special case of that issue. Let's continue the discussion there.