APRProof specific proof state visualization #489

ehildenb · 2023-06-12T21:22:52Z

Fixes: #413

This PR introduces proof-specific viewers, and does a few refactors to make that possible:

Helpers are added to KCFG for turning into modules, including:
- KCFG.Split.covers which returns each individual split as a reverse cover.
- KCFG.NDBranch.edges, which returns each non-deterministic step as an edge.
- KCFG.Edge.to_rule, which converts an edge into a K rule (or claim).
Small refactorings to KCFGShow structure:
- KCFGShow.dot returns a Digraph directly (for further manipulation) instead of a list of str.
- KCFGShow.to_module which returns a KFlatModule is factored out and used directly in KCFGShow.show.
- Helper methods embedded in other methods in KCFGShow are factored out directly to staticmethods of KCFGShow so they can be reused easily.
- We just treat stuck as a node attribute now, printed at the beginning of a node, instead of printing it a second time following a node too.
The way that KCFGShow calculates node attributes is adjusted and factor out.
- A new class NodePrinter is factored out, which by default just uses the attributes the KCFG knows about for printing out nodes.
- That class is extended by APRProofNodePrinter and APRBMCProofNodePrinter, which add the additional information about the nodes pending,terminal,bounded state. If a node is terminal or bounded, then the stuck attribute is no longer printed for less confusion.
- KCFGShow now takes an optional *NodePrinter as an argument (or builds on itself), so instantiating that class is how you can customize how nodes are displayed in text.
- The tests are adapted to use the more specific *NodePrinter classes, and the output checked that the more specific node information is indeed being included.
Adds helper predicates APRProof.is_{pending,terminal} and APRProof.is_bounded, which should behave better in case there are qualified node ids passed in.

…Show

… rules from KCFG edges

…e APR*Proof.is_* predicates directly

… APR*ProofNodePrinter classes

ehildenb · 2023-06-14T20:43:56Z

Running bmc-loop-symbolic-1 test with log level set to INFO now prints out something looking like this for BMC depth-bounded nodes:

You can see that it includes the bounded label in that node, and the stuck is not there anymore, which is less confusing.

In addition, for a node that is terminal, we similarly remove the stuck attribute at print time, for less confusion:

src/pyk/kcfg/kcfg.py

tothtamas28 · 2023-06-15T10:15:01Z

src/tests/unit/test_kcfg.py

        '┃  ┣━━┓\n'
        '┃  ┃  │\n'
-        '┃  ┃  └─ \033[1m24 (frontier, leaf)\033[0m\n'
+        '┃  ┃  └─ 24 (frontier, leaf)\n'


id-s are no longer bold, is this deliberate?

Yes, I removed the bolding.

…ment

Following #489, it turns out that KEVM's TUI is broken because it relies on the old way of doing Node printing. This makes a new `APRProofViewer` class, which largely inherits from `KCFGViewer`, but adjusts it to handle the more spceific node viewers. I have tested this with both KEVM+Foundry and raw KEVM specs, and it seems to work. --------- Co-authored-by: devops <[email protected]>

Following runtimeverification/pyk#489, it turns out that KEVM's TUI is broken because it relies on the old way of doing Node printing. This makes a new `APRProofViewer` class, which largely inherits from `KCFGViewer`, but adjusts it to handle the more spceific node viewers. I have tested this with both KEVM+Foundry and raw KEVM specs, and it seems to work. --------- Co-authored-by: devops <[email protected]>

) Fixes: #413 This PR introduces proof-specific viewers, and does a few refactors to make that possible: - Helpers are added to `KCFG` for turning into modules, including: - `KCFG.Split.covers` which returns each individual split as a reverse cover. - `KCFG.NDBranch.edges`, which returns each non-deterministic step as an edge. - `KCFG.Edge.to_rule`, which converts an edge into a K rule (or claim). - Small refactorings to `KCFGShow` structure: - `KCFGShow.dot` returns a `Digraph` directly (for further manipulation) instead of a list of `str`. - `KCFGShow.to_module` which returns a `KFlatModule` is factored out and used directly in `KCFGShow.show`. - Helper methods embedded in other methods in `KCFGShow` are factored out directly to staticmethods of `KCFGShow` so they can be reused easily. - We just treat `stuck` as a node attribute now, printed at the beginning of a node, instead of printing it a second time following a node too. - The way that `KCFGShow` calculates node attributes is adjusted and factor out. - A new class `NodePrinter` is factored out, which by default just uses the attributes the `KCFG` knows about for printing out nodes. - That class is extended by `APRProofNodePrinter` and `APRBMCProofNodePrinter`, which add the additional information about the nodes `pending,terminal,bounded` state. If a node is `terminal` or `bounded`, then the `stuck` attribute is no longer printed for less confusion. - `KCFGShow` now takes an optional `*NodePrinter` as an argument (or builds on itself), so instantiating that class is how you can customize how nodes are displayed in text. - The tests are adapted to use the more specific `*NodePrinter` classes, and the output checked that the more specific node information is indeed being included. - Adds helper predicates `APRProof.is_{pending,terminal}` and `APRProof.is_bounded`, which should behave better in case there are qualified node ids passed in. --------- Co-authored-by: devops <[email protected]>

…tion/pyk#507) Following runtimeverification/pyk#489, it turns out that KEVM's TUI is broken because it relies on the old way of doing Node printing. This makes a new `APRProofViewer` class, which largely inherits from `KCFGViewer`, but adjusts it to handle the more spceific node viewers. I have tested this with both KEVM+Foundry and raw KEVM specs, and it seems to work. --------- Co-authored-by: devops <[email protected]>

) Fixes: #413 This PR introduces proof-specific viewers, and does a few refactors to make that possible: - Helpers are added to `KCFG` for turning into modules, including: - `KCFG.Split.covers` which returns each individual split as a reverse cover. - `KCFG.NDBranch.edges`, which returns each non-deterministic step as an edge. - `KCFG.Edge.to_rule`, which converts an edge into a K rule (or claim). - Small refactorings to `KCFGShow` structure: - `KCFGShow.dot` returns a `Digraph` directly (for further manipulation) instead of a list of `str`. - `KCFGShow.to_module` which returns a `KFlatModule` is factored out and used directly in `KCFGShow.show`. - Helper methods embedded in other methods in `KCFGShow` are factored out directly to staticmethods of `KCFGShow` so they can be reused easily. - We just treat `stuck` as a node attribute now, printed at the beginning of a node, instead of printing it a second time following a node too. - The way that `KCFGShow` calculates node attributes is adjusted and factor out. - A new class `NodePrinter` is factored out, which by default just uses the attributes the `KCFG` knows about for printing out nodes. - That class is extended by `APRProofNodePrinter` and `APRBMCProofNodePrinter`, which add the additional information about the nodes `pending,terminal,bounded` state. If a node is `terminal` or `bounded`, then the `stuck` attribute is no longer printed for less confusion. - `KCFGShow` now takes an optional `*NodePrinter` as an argument (or builds on itself), so instantiating that class is how you can customize how nodes are displayed in text. - The tests are adapted to use the more specific `*NodePrinter` classes, and the output checked that the more specific node information is indeed being included. - Adds helper predicates `APRProof.is_{pending,terminal}` and `APRProof.is_bounded`, which should behave better in case there are qualified node ids passed in. --------- Co-authored-by: devops <[email protected]>

…tion/pyk#507) Following runtimeverification/pyk#489, it turns out that KEVM's TUI is broken because it relies on the old way of doing Node printing. This makes a new `APRProofViewer` class, which largely inherits from `KCFGViewer`, but adjusts it to handle the more spceific node viewers. I have tested this with both KEVM+Foundry and raw KEVM specs, and it seems to work. --------- Co-authored-by: devops <[email protected]>

) Fixes: #413 This PR introduces proof-specific viewers, and does a few refactors to make that possible: - Helpers are added to `KCFG` for turning into modules, including: - `KCFG.Split.covers` which returns each individual split as a reverse cover. - `KCFG.NDBranch.edges`, which returns each non-deterministic step as an edge. - `KCFG.Edge.to_rule`, which converts an edge into a K rule (or claim). - Small refactorings to `KCFGShow` structure: - `KCFGShow.dot` returns a `Digraph` directly (for further manipulation) instead of a list of `str`. - `KCFGShow.to_module` which returns a `KFlatModule` is factored out and used directly in `KCFGShow.show`. - Helper methods embedded in other methods in `KCFGShow` are factored out directly to staticmethods of `KCFGShow` so they can be reused easily. - We just treat `stuck` as a node attribute now, printed at the beginning of a node, instead of printing it a second time following a node too. - The way that `KCFGShow` calculates node attributes is adjusted and factor out. - A new class `NodePrinter` is factored out, which by default just uses the attributes the `KCFG` knows about for printing out nodes. - That class is extended by `APRProofNodePrinter` and `APRBMCProofNodePrinter`, which add the additional information about the nodes `pending,terminal,bounded` state. If a node is `terminal` or `bounded`, then the `stuck` attribute is no longer printed for less confusion. - `KCFGShow` now takes an optional `*NodePrinter` as an argument (or builds on itself), so instantiating that class is how you can customize how nodes are displayed in text. - The tests are adapted to use the more specific `*NodePrinter` classes, and the output checked that the more specific node information is indeed being included. - Adds helper predicates `APRProof.is_{pending,terminal}` and `APRProof.is_bounded`, which should behave better in case there are qualified node ids passed in. --------- Co-authored-by: devops <[email protected]>

…tion/pyk#507) Following runtimeverification/pyk#489, it turns out that KEVM's TUI is broken because it relies on the old way of doing Node printing. This makes a new `APRProofViewer` class, which largely inherits from `KCFGViewer`, but adjusts it to handle the more spceific node viewers. I have tested this with both KEVM+Foundry and raw KEVM specs, and it seems to work. --------- Co-authored-by: devops <[email protected]>

) Fixes: #413 This PR introduces proof-specific viewers, and does a few refactors to make that possible: - Helpers are added to `KCFG` for turning into modules, including: - `KCFG.Split.covers` which returns each individual split as a reverse cover. - `KCFG.NDBranch.edges`, which returns each non-deterministic step as an edge. - `KCFG.Edge.to_rule`, which converts an edge into a K rule (or claim). - Small refactorings to `KCFGShow` structure: - `KCFGShow.dot` returns a `Digraph` directly (for further manipulation) instead of a list of `str`. - `KCFGShow.to_module` which returns a `KFlatModule` is factored out and used directly in `KCFGShow.show`. - Helper methods embedded in other methods in `KCFGShow` are factored out directly to staticmethods of `KCFGShow` so they can be reused easily. - We just treat `stuck` as a node attribute now, printed at the beginning of a node, instead of printing it a second time following a node too. - The way that `KCFGShow` calculates node attributes is adjusted and factor out. - A new class `NodePrinter` is factored out, which by default just uses the attributes the `KCFG` knows about for printing out nodes. - That class is extended by `APRProofNodePrinter` and `APRBMCProofNodePrinter`, which add the additional information about the nodes `pending,terminal,bounded` state. If a node is `terminal` or `bounded`, then the `stuck` attribute is no longer printed for less confusion. - `KCFGShow` now takes an optional `*NodePrinter` as an argument (or builds on itself), so instantiating that class is how you can customize how nodes are displayed in text. - The tests are adapted to use the more specific `*NodePrinter` classes, and the output checked that the more specific node information is indeed being included. - Adds helper predicates `APRProof.is_{pending,terminal}` and `APRProof.is_bounded`, which should behave better in case there are qualified node ids passed in. --------- Co-authored-by: devops <[email protected]>

…tion/pyk#507) Following runtimeverification/pyk#489, it turns out that KEVM's TUI is broken because it relies on the old way of doing Node printing. This makes a new `APRProofViewer` class, which largely inherits from `KCFGViewer`, but adjusts it to handle the more spceific node viewers. I have tested this with both KEVM+Foundry and raw KEVM specs, and it seems to work. --------- Co-authored-by: devops <[email protected]>

ehildenb added 9 commits June 12, 2023 21:20

kcfg/show: return Digraph directly from KCFGShow.dot

e3a8407

kcfg/show: factor out common helper methods to static methods in KCFG…

11b0c71

…Show

kcfg/show: factor out KCFGShow.to_module from KCFGShow.show

9e972eb

proof/show: implement proof-specific APRProofShow

f5bdb3c

kcfg/show: factor out staticmethod KCFGShow.to_rule

1ddac0e

kcfg/show: allow passing in custom node descriptors for pretty printing

5172d31

proof/show: adding pending/terminal descriptors to nodes in APRProofShow

9d9b28e

kcfg/show, proof/show: thread through node_descriptors to more methods

f4627f6

Merge f4627f6 into 7bb5b66

0dd021c

ehildenb self-assigned this Jun 12, 2023

rv-auditor and others added 15 commits June 12, 2023 21:24

Set Version: 0.1.328

84e85eb

kcfg/show: thread through node_descriptors from _print_node

f6554a2

kcfg/kcfg: add KCFG.Split.covers and KCFG.NDBranch.edges helper methods

96cdf53

kcfg/kcfg: add KCFG.Edge.to_rule for a simple default way of building…

39dcbee

… rules from KCFG edges

kcfg/show: use KCFG.Edge.to_rule in KCFGShow.to_module

d3f5091

pyk/kcfg, src/tests: factor out NodePrinter class from KCFGShow

4e396f6

proof/show: simplify APRProofShow by using APRProofNodePrinter instead

ca9b1d8

proof/show: add APRBMCProofNodePrinter too

3aa8bbd

kcfg/show: no need to print stuck attribute twice

9491ecd

proof/reachability: add APR*Proof.is_* predicates for testing nodes

2ef0942

proof/show: correctly initialize APR*ProofNodePrinter classes, and us…

2665eae

…e APR*Proof.is_* predicates directly

src/tests/integration/kcfg: migrate tests over to using more specific…

ec93de4

… APR*ProofNodePrinter classes

Merge remote-tracking branch 'upstream/master' into proof-viewers

070725f

Merge 070725f into 400fc7e

0718fad

Set Version: 0.1.333

ddd584e

proof/show: remove stuck attribute for terminal/bounded nodes

5fd404c

ehildenb marked this pull request as ready for review June 14, 2023 20:52

ehildenb requested review from nwatson22 and tothtamas28 June 14, 2023 20:52

ehildenb changed the title ~~APRProof specific viewer~~ APRProof specific proof visualization Jun 14, 2023

ehildenb changed the title ~~APRProof specific proof visualization~~ APRProof specific proof state visualization Jun 14, 2023

nwatson22 approved these changes Jun 14, 2023

View reviewed changes

src/pyk/kcfg/kcfg.py Outdated Show resolved Hide resolved

tothtamas28 approved these changes Jun 15, 2023

View reviewed changes

ehildenb and others added 4 commits June 15, 2023 20:01

Merge remote-tracking branch 'upstream/master' into proof-viewers

72f1a2f

kcfg/{kcfg,show}: KCFG.Edge.to_rule does not need KDefinition as argu…

62faa2c

…ment

Merge 62faa2c into 2443106

9a5fc14

Set Version: 0.1.335

e8f561a

ehildenb added the automerge label Jun 15, 2023

rv-jenkins merged commit 9720f2c into master Jun 15, 2023

rv-jenkins deleted the proof-viewers branch June 15, 2023 20:25

This was referenced Jun 20, 2023

Update dependency: deps/pyk_release runtimeverification/evm-semantics#1903

Merged

Implement APRProofViewer as an APRProof specific TUI #507

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

APRProof specific proof state visualization #489

APRProof specific proof state visualization #489

Uh oh!

ehildenb commented Jun 12, 2023 •

edited

Loading

Uh oh!

ehildenb commented Jun 14, 2023 •

edited

Loading

Uh oh!

Uh oh!

tothtamas28 Jun 15, 2023

Uh oh!

ehildenb Jun 15, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

APRProof specific proof state visualization #489

APRProof specific proof state visualization #489

Uh oh!

Conversation

ehildenb commented Jun 12, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ehildenb commented Jun 14, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

tothtamas28 Jun 15, 2023

Choose a reason for hiding this comment

Uh oh!

ehildenb Jun 15, 2023

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

ehildenb commented Jun 12, 2023 •

edited

Loading

ehildenb commented Jun 14, 2023 •

edited

Loading