Remove dependencies on GlobalInfo
We have a class util.globalinfo.GlobalInfo
that stores context information like the CFA and the CPAs in static state. This was necessary to add for serializing and deserializing objects like abstract states, which often contain data that cannot be (de-)serialized without access to certain context (like a solver context that is necessary for creating formula objects).
However, unfortunately other code has started to rely on this class as well. This will break as soon as more than one set of CPAs is used, e.g., when using more complex algorithms like a parallel portfolio, counterexample checks, etc. Even relying on the stored CFA is not safe because there are contexts where analyses run on different CFAs.
So we need to replace the following uses of GlobalInfo
with a different solution:
-
AppliedCustomInstructionParser.parseACIs
(ebc77548 (comment 652500546)) -
ARGBasedPartialReachedSetConstructionAlgorithm.getARGPass
(21fb4896 (comment 652502045)) -
TraceAbstractionTransferRelation.initializeComponentsOnce
(dceb7e1c (comment 652034317)) -
PredicateAbstractState.AbstractionState.getFormulaApproximation
(adb43d9c (comment 652105938))
In addition, we should make sure that future code does not start using GlobalInfo
again with the following changes:
-
Rename class and package to something that clearly indicates that it is only for serialization. -
Do not always fill GlobalInfo
with state and keep it forever, instead just register instances there immediately before they are needed (serialization) and remove their references afterwards. This also fixes the memory leak that is related to this class! -
Do not allow silently overwriting the state in this class. Instead, check that new instances can only be register while the current state is empty.