Use differential inlining to represent function calls

[danmatichuk]

Currently the equivalence of blocks containing function calls is proven compositionally, by performing three separate equivalence proofs for each function call site, computing intermediate equivalence relations for:

• before the function call
• the body of the called function,
• after the function call returns.

To propagate conditional equality, we need to be able to soundly represent a function call where some of the results are only conditionally equivalent. This can be represented here by inlining each function call as a family of uninterpreted functions: one for each modified location. Locations which are conditionally equivalent are inlined with a mux over this condition: either returning the "equal" uninterpreted function, or an "unequal" uninterpreted function.

Given this, we change the equivalence check for a function call to be as follows:

• Compute the (conditional) pre-domain from the call site of the function call, to the next return
• Compute a family of uninterpreted functions from the called function, given the above as the post-domain where:
  • locations in the post-domain yield equal uninterpreted functions for the original vs. patched programs
  • locations that are conditionally equivalent in the post-domain yield conditionally equivalent uninterpreted functions
  • modified locations outside the post-domain yield inequivalent uninterpreted functions
• Inline these uninterpreted functions in the calling function, and iterate.