This adds the ability for the equivalence analysis to "split" and independently analyze each binary (original vs patched), in order to collect any effects (observable and unobservable), while deferring any equivalence proofs.
This allows the verifier to continue in the presence of significant control flow differences, by splitting the analysis, collecting the result, and then later collecting the results and re-synchronizing.
During single-sided analysis, observable events are collected and any updated locations are considered to no longer be in the equivalence domain. When synchronizing, the two sequences of accumulated observable events are compared for equality, and the resulting equivalence domain is the intersection of the two domains (i.e. any locations modified by either program are no longer known to be equivalent).
The choice of where to split the analysis and where to re-synchronize is heuristic. Currently the verifier splits on any mismatched stub calls (i.e. when one program calls a stub and the other doesn't, or calls a different stub), and synchronizes when the function containing the call site is returned from.
This adds the ability for the equivalence analysis to "split" and independently analyze each binary (original vs patched), in order to collect any effects (observable and unobservable), while deferring any equivalence proofs. This allows the verifier to continue in the presence of significant control flow differences, by splitting the analysis, collecting the result, and then later collecting the results and re-synchronizing.
During single-sided analysis, observable events are collected and any updated locations are considered to no longer be in the equivalence domain. When synchronizing, the two sequences of accumulated observable events are compared for equality, and the resulting equivalence domain is the intersection of the two domains (i.e. any locations modified by either program are no longer known to be equivalent).
The choice of where to split the analysis and where to re-synchronize is heuristic. Currently the verifier splits on any mismatched stub calls (i.e. when one program calls a stub and the other doesn't, or calls a different stub), and synchronizes when the function containing the call site is returned from.