llvm_extract support for functions that call other functions

[brianhuffman]

Currently llvm_extract inlines all function calls into the top-level extracted function. This does not scale well for large programs with multiple levels of function calls.

Ideally it should be able to use an override-like mechanism to put defined constants in the place of function calls. It would also be nicer if it returned a single defined term with a function type, instead of an open term containing symbolic variables.

[TomMD]

One thing to consider during the crucible rewrite is handling undefined symbols. Currently SAW can't reason about code in the form:

extern int g(int x);
int f (int x)
{
    return g(x) - g(x);
}

For example, this code is identical to 0 (assuming no undefined behavior in g and it is pure). Reasonable uses exist that would be benefited by support for reasoning over incomplete declarations.

[brianhuffman]

@TomMD If you want to assume that g is pure with no undefined behavior, you could give a specification for g in terms of an uninterpreted function. Armed with such an override for g (which you'd have to assert without proof), you should be able to prove a spec for f that says the return value is 0.

EDIT: I should add that you can obtain an uninterpreted function of whatever type you want in saw-script like this:

sawscript> g <- fresh_symbolic "g" {| [32] -> [32] |}

[TomMD]

@brianhuffman But how can one extract the Term (via llvm_extract, llvm_symexec or otherwise) when the LLVMModule function refers to an undefined function? The naive application of any of the above functions results in an error, am I missing understanding of some significant functionality?

[atomb]

The original idea for llvm_extract was to support exactly this sort of use case, and the necessary plumbing just hasn't been put in place yet. The idea was that the LLVMSetup argument could configure more flexible inputs and outputs, and another list of overrides similar to the one in llvm_verify would allow for called functions to be interpreted in any way you like (including making their behavior completely uninterpreted). Doing this shouldn't be that hard (though I'd argue that we should just do something similar using Crucible, rather than continuing to add features to `llvm_extract). I think it would mostly require:

• Ensuring that the (existing) execution of the LLVMSetup argument makes sense in the context of what the rest of llvm_extract does.
• Adding a [LLVMMethodSpec] argument, and registering all of the elements as overrides (as done in llvm_verify).

The process might be slightly different for equivalent functionality using Crucible, but probably not in any fundamental way.

[atomb]

This is now done with crucible_llvm_compositional_extract.