Add static module for top-level Control Spec context

[sim642]

This adds the static Analyses.ControlSpecC module, which corresponds to the context of the entire top-level Spec. This allows individual analyses to actually use ctx.control_context, get a result of meaningful type and use them (opaquely) inside its own domains and global constraint variables.

Previously this was problematic in multiple ways:

1. ARINC analysis (and its extraction) unsafely get (or really reconstruct) the corresponding base analysis context and use its hash to identify the context:
   

   analyzer/src/analyses/arinc.ml

   Lines 253 to 255 in 1dcd967

   	let base_context = BaseMain.context_cpa f @@ Obj.obj @@ ctx.presub "base" in
   	let context_hash = Hashtbl.hash (base_context, ctx.local.pid) in
   	{ ctx.local with ctx = Ctx.of_int (Int64.of_int context_hash) }

   
   This in itself is prone to two problems:
   1. Hashes may collide.
   2. Other analyses other than base may also have context components.
2. To avoid the aforementioned problems, a safe way is to implement a Spec functor instead, which wraps the entire combined analysis and can thus directly access its C module. The GraphML witness generation takes this route.
   Implementing such an analysis as a functor is inconvenient and composes poorly with other analyses.

[jerhard]

Currently, neither ControlSpecC nor the already existing control_context seem to be used, or am I missing something?

[michael-schwarz]

This should be used by #220 (or the ARINC analyses, but I'll open a PR to drop them tomorrow).

[sim642]

Currently, neither ControlSpecC nor the already existing control_context seem to be used, or am I missing something?

That's correct. I initially tried to use this for #796 in order to track constraint variables where a witness hint was already used, but that didn't work as well as I had hoped (not the fault of this PR).

I also thought whether I could reimplement WitnessConstraints lifter as an analysis instead using this PR, but that also doesn't work out, because that also records dependencies between paths, which this cannot really handle.

So there's no immediate need for this unless we plan to refactor #220 to use this.

[sim642]

Since unassuming once turned out to be a futile idea according to GobCon discussions, this will not be used by #796.

However, since #812 removes ctx.presub but its replacement #220 currently would require it, this will be necessary for #811. Thus this will be needed. At minimum #220 could then be refactored to just use ControlSpecC.hash instead of base context hash. A further improvement could then replace hashes with the real things via this module.