danmatichuk
commented
2 years ago Note: Revisit how variable bindings are handled when generating the post condition for each equivalence problem, as it's possible we're not handling symbolic pointers correctly in the equivalence domains.
In the strongest postcondition verifier, the widening loop currently computes the entire equivalence problem initially and then uses the counter-example to determine which machine locations can potentially diverge between the two programs.
In the worst possible case, the solver will only invalidate a single location on each iteration of the loop (i.e. the overall equivalence predicate is invalid because one location diverges, but the rest are still equal in the resulting model). This creates a lot of wasted effort, since we are providing the entire equivalence predicate (asserting that all memory locations are equal) to the solver each time.
As a potential optimization, we can instead iterate over the structured equivalence domain (which has an individual predicate asserting equality for each location) and independently ask the solver to widen for each location. The caveat here is that we are now necessarily invoking the solver once per location, but each query should be much smaller as it is only attempting to prove equality for one a single location.