revisit warn-unused and check-value analyses

[ivg]

The #1075 PR highlighted some fundamental problems with our warn-unused/must-check-value analyses that we need to revisit once #1075 is merged.

Problem 1: analyses summaries should not rely on observations

When we summarize the run of a machine or a system we shall not use observations to post the summary results as during summarization the observations are usually blocked (or it they not, then the summarization procedure may trigger its own observation that will kill it in an asynchronous manner).

This is not a fundamental problem but a technical one. It, however, limits the flexibility of Primus, so we might reconsider some of our design decisions, e.g., by playing with the clock interface. (We can move clock to a different component and enable/disable them).

Problem 2: taint-finalize shall not be used for may analysis

Or, more general, microexecution is bad for may analyses. If we have a program property that is computed as may analysis (i.e., the property holds if it holds on at least one path), then in order to prove that the property doesn't hold we need to wait until all paths converge and the we can summarize. Compare it with UAF/DF which is must analysis, i.e., where the security property must hold on all paths, so once we find at least one counterexample we can immediately report it.

Currently, we use Taint analysis with its GC to find unused/unchecked values. We, hower, rely on the taint-finalize observation which is path-specific, therefore if a taint is finalized in a given path, it doesn't mean that we don't have any other machines where it is still live. That means that we need to revisit the taint analysis on the next iteration and implement the taint-liveness analysis on the global level.