Traces article implementation

[sim642]

I'm opening this humongous draft pull request already now to have a place for keeping some notes on all the changes traces branch contains, including many general improvements etc.
Eventually these would get merged into master.

Overview of changes

1. Many implementations for privatization via exp.privatization option.
   1. The new default privatization is protection-read aka ProtectionBasedPriv with additional readable lockset check aka Protection-Based Reading with additional readable lockset check. The additional check is necessary to handle many of our regression tests.
   2. Regression tests which require more precise privatizations have // TODO comments to be useful with regression testing script.
   3. Privatization extracted and abstracted from base.ml to basePriv.ml.
   4. base analysis local domain has third privatization-dependent component (by @vesalvojdani).
   5. base analysis global domain is privatization-dependent.
   6. Add reason argument to sync transfer function to allow analyses choose if they want to do computations at every node, or only at some necessary places (like join).
2. Changes to mutex analysis.
   1. Write-based protecting locksets computed by mutex analysis (by @vesalvojdani).
   2. Number of new mutex-related queries needed by different privatizations.
3. Event system (ctx.emit and event transfer function) for deduplicating thread creation, lock, unlock and escape logic in different analyses.
   1. Use separate MCPSpec for analyses inside MCP.
   2. Replace ctx.split's explicit branch arguments with arbitrary events.
4. Comparison of privatization precisions with privPrecCompare.
   1. Based on dumping (marshalling) all read_global results via exp.priv-prec-dump option.
5. General improvements.
   1. Optimization of large CPAs that occur in some privatizations (issue Optimize large CPAs #164).
   2. Partial fix of path-sensitive thread creation (issue Make threadflag/thread analysis path-sensitive #148).
   3. Use right value of exp.earlyglobs already during global initialization.
   4. Move global invariant simulation in Control earlier to allow enter_with and otherstate to also sideg (issue Move extern inits, global inits and otherfuns spawning into constraint system #178).
   5. Add new sem (semantics) category of options for configuring what unknown functions etc may and may not do.
   6. Fix unknown functions not invalidating unprivatized globals.
   7. Fix Deadcode behavior of invariant on binary operators.
6. General utilities.
   1. AfterConfig module for running initialization things after config has been loaded.
   2. RichVarinfo module for abusing varinfos to represent richer data, particularly as global constraint variables.

Things broken

• OSEK regression tests fail with new privatizations. Defaulting to protection-vesal for them now, but old passes as well.
• Witness generation is untested after significant MapDomain interface changes from Optimize large CPAs #164. Domain tests fail for HoareMap.

[michael-schwarz]

In general, I'm very surprised by how modular the different privatisations turned out, that is a very nice touch!

[michael-schwarz]

Sorry, about the mess, I clicked on Close with comment instead of discarding my comment by mistake. 🙃

[michael-schwarz]

Is there still anything blocking us from merging?

[sim642]

Not from my side, so I suppose I'll do the merge?

Since nobody else would probably try or review this branch anyway, we won't find out about possible regressions until it's on master and everyone is using the changes.