danmatichuk
commented
2 months ago This is subsumed by #435. We expect arbitrary values to instead be derived as (possibly uninterpreted) functions of global state, so that we can properly track references to these values between CFARs.
When a stub introduces an undefined value (i.e. number of bytes read from some source) it creates a fresh variable. If this variable ends up in the equivalence condition for a CFAR via propagation then the verifier gets stuck in an infinite loop trying to prove that the propagated condition implies the precondition for the subsequent CFAR. This is because each time the CFAR is analyzed the stub code is re-executed and a new fresh value is created with no relation to the old one. The result is an infinite loop where the same condition is repeatedly added with fresh variables.
To address this we need to add some scoping rules for these variables so they are consistent between stub executions. A condition which contains stub-generated variables can't be propagated (as they don't have any meaning before being introduced by the stub), which needs to be detected by the propagation logic (and should be considered a failure condition for an assertion: i.e. an assertion containing these free variables must be provable since it can't be propagated further to the entry point)