KCFGStore for managing loading and storage of KCFG data

[ehildenb]

Related: runtimeverification/pyk#686

Currently in the KCFG class, we store a copy of the nodes on each of the edge types in the KCFG, which makes it very easy to select the source/target nodes for an edge without doing a second node lookup in the KCFG. The issue is that routines which modify nodes (such as (i) replace_node, which is broken runtimeverification/pyk#686, or (ii) if we switch to storing attributes directly on the node), don't also modify the given edges which contain the node as a source/target.

Another observation is that for any given node, it may have 0 or 1 successors, and that's it. We enforce this at the code level. So we can take advantage of this in our data-structures, by instead just having a single dictionary of _successors and _predecessors, where the _successors dictionary either has the entry with a single integer pointing at the target successor or nothing, and the precessors has a list of potential predecessors.

We could do one of two things:

• Change the way we store KCFGs in the following way:
  • New class KCFGStore, which has _nodes: dict[int, KCFG.Node], _constraints: dict[int, KInner], _csubsts: dict[int, CSubst]. These are the basic datas that are needed to reconstruct any edge in a KCFG.
  • Change the storage of nodes/edges in the KCFG class to be dictionaries that contain references to the given data components instead. For example, _covers becomes _dict[int, dict[int, int]], then when we are returning a Cover from KCFG.Cover, we lookup the relevant CSubst in KCFGStore._csubsts(...) and construct a KCFG.Cover directly at that moment.
  • Make sure there aren't any places outside of KCFG where the underlying datastructures are manipulated directly.

This would make it so that when we change a given node (adding a constraint, change attributes, simplify it, etc...), all the KCFG accessors will also be correctly updated. This change may also make it so we can more broadly apply things like the optimizer (runtimeverification/pyk#872) across all datastructures in the KCFGStore.

[ehildenb]

This came up because I was trying to make nodes store their attributes directly, and realized that I would suffer the same bug as replace_node if we do that.

[ehildenb]

For now, we make replace_node aware of the fact that it has to replace nodes on edges too: runtimeverification/pyk#920

[tothtamas28]

Another observation is that for any given node, it may have 0 or 1 successors, and that's it. We enforce this at the code level. So we can take advantage of this in our data-structures (...)

That would be a very nice change. And in general, the suggested refactoring makes sense to me.

Something that's related, I think we should extract a minimal, CRUD-like interface for KCFG-s, add tests for it, and implement more complex features (like shortest_path_between) in terms of it. That would greatly simplify KCFG implementation. Also, then we could implement multiple storage backends, and switch between them depending on the use case (e.g. faster vs more memory efficient).

In particular, we then could have a backend based on a relational database (the dicts with int keys already mimic that to some extent). We could start with something very lightweight like sqlite3. We do not need the whole KCFG in memory for most use cases, so that would solve memory issues for proofs on large KCFGs. Related: runtimeverification/pyk#79.