Code re-organizations prepping for KCFG refactors

[ehildenb]

Part of #471, #413

As I was working towards the goal of better BMC prover visualization, it's clear we need:

• Proof specific viewers,
• Fixing the BMC checker off-by-one-error, and
• Trimming of the structure stored in the KCFG (removing the notion of target, expanded).

This makes the first least controversial steps towards those changes, including:

• Method KCFG.replace_node now replaces the node in place, so that the node identifier doesn't change. This is possible now because the node identifier is not tied to the contents of the node, and makes tracking things like init/target/terminal/bounded sets externally in the *Proof classes more feasible even if nodes are being simplified for example.
• The notion of a unique target and init is added to the APRProof class, in preparation for removing the target notion from KCFG.
  • Add fields target and init to APRProof state, which explicitly call out the unique init/target states.
  • Move KCFGExplore.target_subsume => APRProver._check_subsumed, which makes use of the explicitly called out init/target states.
  • Moves KCFG.path_constraints => APRProof.path_constraints, because it relies on a unique target node.
• The notion of stuck nodes is moved into APRProof state as terminal nodes.
  • The field _terminal_nodes is added to APRProof state.
  • APRProver._check_terminal directly manipulates this set instead of stuck/expanded set.
  • The notion of APRProof.terminal is added, which returns the set of nodes in the APRProof._terminal_nodes set.
  • The notion of APRProof.pending is added, which returns the set of KCFG.frontier nodes that are not in the proofs terminal_nodes set.
  • The APRProof.terminal and APRProof.pending sets are used for determining APRProof.status.
  • The APRBMCProof.bounded set is added, which similarly tracks the bounded set of nodes directly. This is used in computing APRBMCProof.pending and APRBMCProof.status.
• Methods APRProof.from_claim and APRBMCProof.from_claim_with_bmc_depth are added for reading these proof types directly from claims (and tests are updated appropriately).
• Method APRBMCProof.dict is refactored to use APRProof.dict directly first, then add the needed information to it.
• Methods KCFG.node_attrs => KCFGShow.node_attrs and KCFG.node_short_info => KCFGShow.node_short_info are moved to localize them to use site.
• Adds Proof.json as shortcut for json.dumps(Proof.dict).
• For each of the integration/kcfg tests that do APRProofs, adds logging at info level for the generated KCFG, to make debugging them easier by just throwing a flag.

[tothtamas28]

The notion of stuck nodes is moved into APRProof state as terminal nodes

Do you also plan to remove stuck from KCFG? It is reachability information that I think should be stored there. Proof classes can interpret that information accordingly.

The notion of a unique target and init is added to the APRProof class, in preparation for removing the target notion from KCFG.

Subsumption into the target will still be retained in the KCFG though, right?

[ehildenb]

After discussion, we'll be removing the notion of expanded, in favor of an explicit stuck set (to mark that the backend has attempted symbolic execution from that node and it will not be able to make progress). But target will be removed.