The protection logging from apron analysis can be generalized into mutex analysis to compute, in traces paper notation, $G_m$-s from $\mathcal{M}[g]$-s. So far this information was just used for some benchmarking stats, but it's also useful for other things, e.g. witness invariants only about globals which are protected.

While moving this code, there are opportunities to also make other changes, to be discussed below.