Unify infrastructure for compositional verification

[atomb]

The implementations of compositional verification for Java and LLVM overlap to a very significant degree. We've put a good deal of effort into factoring out common code, with some success, but I expect there's more we can do. Reducing duplicate code would reduce the maintenance burden, and also reduce the cost of implementing compositional reasoning for new languages (such as Rust MIR or x86).

[brianhuffman]

Duplicate of #379?

[atomb]

This one is intended to be more general, though perhaps the initial description didn't convey that as well as it could. Whereas #379 is entirely about code duplication, this issue covers different approaches that may allow more sharing, as well. Even if #379 were resolved as well as possible, I think there are more improvements we could make to the overall architecture.

[kquick]

The Java support identified some LLVM-specific things that needed an equivalent implementation; the Rust work may help inform the right generalization (both improving and removing existing generalizations).

[atomb]

The Gillian system (Part 1, Part 2) may provide some inspiration about how to effectively decompose things in a language-independent way. I believe they were somewhat inspired by SAW in the way they approached the problem.