Refactor skeleton / boilerplate generation

[chameco]

(Depends on GaloisInc/crucible#464.)

This PR improves the usability of SAWScript's LLVM boilerplate generation.

Previously, boilerplate generation was exposed through a function llvm_boilerplate, which emitted outlines of function specifications to a file, which could then be modified by hand. This approach was very "brittle": there was no way to generate specifications, tweak those specifications by hand, and then regenerate those specifications modulo the tweaks to reflect e.g. a code change. This was further exacerbated by the interface forcing the user to regenerate all specifications at once.

Here, we break the former boilerplate generation into two components:

• Skeleton generation, which provides a first-class SAWScript interface to infer the "skeleton" of a specification from an LLVM module, to modify that skeleton programatically, and to obtain a regular Crucible LLVM method spec from that skeleton.
• Boilerplate generation, which emits SAWScript textually. The emitted SAWScript now uses the skeleton generation interface described above.

Let's look at an example. Consider the following function:

void set(int *x, int y) {
    *x = y;
}

Previously, boilerplate generation would have produced a specification that looks like the following:

let set_setup = do {
  arg0_star <- crucible_fresh_var "x" (llvm_int 32);
  arg0 <- crucible_alloc (llvm_int 32);
  crucible_points_to arg0 (crucible_term arg0_star);
  arg1 <- crucible_fresh_var "y" (llvm_int 32);
  crucible_execute_func [arg0, crucible_term arg1];
};

Now, boilerplate generation will produce something like:

MODULE_SKEL <- module_skeleton MODULE;

set_skel <- function_skeleton MODULE_SKEL "set";
let set_spec = do {
  skeleton_globals_pre MODULE_SKEL;
  prestate <- skeleton_prestate set_skel;
  skeleton_exec prestate;
  poststate <- skeleton_poststate set_skel prestate;
  skeleton_globals_post MODULE_SKEL;
};

The intent here is that this boilerplate should never need to be regenerated.
Most of the work previously done to determine argument sizes, allocate and initialize arguments, etc. is now done by SAWScript at runtime, rather than by the boilerplate generation function as a separate step.
(Boilerplate generation now only handles things that are truly boilerplate, such as passing the correct overrides to crucible_llvm_verify.)

The skeleton generation interface allows adding additional preconditions or postconditions without constantly needing to copy these into new boilerplate. In the example above, we might add

  pre_y <- skeleton_arg prestate "y";
  post_x <- skeleton_arg poststate "x";
  crucible_postcond {{ (pre_y : [32]) == (post_x : [32]) }};

to the end of set_spec to assert that the value pointed to by x after executing set is equal to the initial value of y. set_spec will then work regardless of some small changes to set (e.g. changing int to long, or swapping the argument order).

[andreistefanescu]

This is a big change, looks good overall.

[chameco]

GaloisInc/crucible#464 has been merged, waiting on GaloisInc/macaw#157 to update deps/crucible and deps/macaw.

[kquick]

The excellent description of this PR is much appreciated!

[chameco]

The BIKE proofs are running out of memory on Travis and on Fryingpan. These were already "close to the edge" in terms of resource usage, so I suspect a recent Crucible change might have pushed them over.