From 14ec23f8e7f2925ef82f19c8fe50e285d6a89361 Mon Sep 17 00:00:00 2001 From: Graham Date: Thu, 11 Jul 2024 17:06:25 -0400 Subject: [PATCH] Improved cozy-viz README --- cozy-viz/README.md | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/cozy-viz/README.md b/cozy-viz/README.md index 4114b71..9ee0ade 100644 --- a/cozy-viz/README.md +++ b/cozy-viz/README.md @@ -88,3 +88,47 @@ The available tools are: To compare a different set of branches, click a new terminal node in the left pane. This will highlight a new set of compatible branches on the right, and you can select one of those as above. + +### Refining The View + +The initial view presented by dragging in a trace is fully expanded: each basic +block along each execution path is a node, all basic blocks are displayed, and +all nodes with special features are highlighted. This can be a lot of +information to deal with. To refine the view, you can use some of the menu +options at the top of the cozy-viz interface. The available menu options are: + +1. File: this contains options for saving the trace you're currently viewing as + a file. This can be useful if you've summoned the visualizer from a script + with a preloaded trace, and it turns out you'd like to save that trace. It + also contains an option for creating a *report* - see below. +2. View: this contains options for toggling the visibility of the different + kinds of special nodes: errors, [failed + post-conditions](https://draperlaboratory.github.io/cozy/autoapi/cozy/directive/index.html#cozy.directive.Postcondition), [failed asserts](https://draperlaboratory.github.io/cozy/autoapi/cozy/directive/index.html#cozy.directive.Assert), + nodes containing syscalls, and nodes containing simulated procedure calls. + View also includes options for changing the "granularity" of the view, + either by merging sequences of nodes in which the constraints on input don't + change, or merging all sequences of nodes where no forking occurs. +3. Prune: this lets you toggle different "prunings", which remove branchings + that aren't interestingly different from any of their compatible partners. + Options include pruning branches that don't differ from their partners in + memory contents, register contents, input constraints, stdout, or branches + whose stdout contents satisfy some regex also satisfied by all their partners. +4. Layout: this lets you change the way the symbolic execution is laid out, + displaying it as a CFG using one of several graph-layout + algorithms. Note that while the symbolic execution is laid out as a CFG, it + won't be possible to select or compare pairs of branches in the ordinary + way, since the CFG obscures which sequences of nodes are branches in the + symbolic execution. +5. Search: this lets you highlight sets of nodes whose stdout matches a certain + regex. + +### Report Generation + +The "Report" option under the file menu will open a report in a new window, +based on whatever branches are visible (not pruned) at the time that the report +window is opened. For each visible branch in the left pane, the report will +contain a text field where notes about that branch and its partners can be +recorded. Branches can be checked off as "reviewed" by clicking the checkboxes +within the report. Reviewed branches will show an × in their final node, and +can be hidden from view using one of the pruning options under the "prune" menu. +Once a report is completed, it can be printed as a PDF.