Conditions are not properly propagated backwards across control flow desync/sync points #448
Comments
danmatichuk
added a commit
that referenced
this issue
Sep 11, 2024
this ensures that the domain is computed under the strongest possible set of assumptions, as well as ensuring that assertions are necessarily propagated NB: this breaks challenge 10 and target 7, since it fixes #447 but not #448 (i.e. desync points are now properly re-queued for analysis during propagation, but the generated assertions are incorrect)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When an assertion is introduced after the sync point following desync/sync analysis, it may need to be propagated back through one or both of the single-sided analyses in order to be proven. Currently when propagating through a sync point we duplicate the assertion and try to propagate it separately through both of the single-sided analyses. This is incorrect and will almost necessarily introduce unprovable assertions, as it results in introducing unbounded symbolic terms (i.e. the variables representing the undefined state of the opposite program state during a single-sided analysis step).
This issue was hiding behind #447, which caused these unprovable assertions to be undetected.
The text was updated successfully, but these errors were encountered: