|
3 | 3 |
|
4 | 4 | #include "concrete_rt.hpp"
|
5 | 5 | #include <cassert>
|
| 6 | +#include <cstdio> |
6 | 7 | #include <iterator>
|
7 | 8 | #include <memory>
|
| 9 | +#include <ostream> |
8 | 10 | #include <variant>
|
9 | 11 |
|
10 | 12 | class SymVal {
|
@@ -89,8 +91,29 @@ struct NodeBox {
|
89 | 91 | struct Node {
|
90 | 92 | virtual ~Node(){};
|
91 | 93 | virtual std::string to_string() = 0;
|
| 94 | + void to_graphviz(std::ostream &os) { |
| 95 | + os << "digraph G {\n"; |
| 96 | + os << " rankdir=TB;\n"; |
| 97 | + os << " node [shape=box, style=filled, fillcolor=lightblue];\n"; |
| 98 | + current_id = 0; |
| 99 | + generate_dot(os, -1, ""); |
| 100 | + |
| 101 | + os << "}\n"; |
| 102 | + } |
| 103 | + int get_next_id(int &id_counter) { return id_counter++; } |
| 104 | + virtual int generate_dot(std::ostream &os, int parent_dot_id, |
| 105 | + const std::string &edge_label) = 0; |
| 106 | + |
| 107 | +protected: |
| 108 | + // Counter for unique node IDs across the entire graph, only for generating |
| 109 | + // graphviz purpose |
| 110 | + static int current_id; |
92 | 111 | };
|
93 | 112 |
|
| 113 | +// TODO: use this header file in multiple compilation units will cause problems |
| 114 | +// during linking |
| 115 | +int Node::current_id = 0; |
| 116 | + |
94 | 117 | struct IfElseNode : Node {
|
95 | 118 | SymVal cond;
|
96 | 119 | std::unique_ptr<NodeBox> true_branch;
|
@@ -120,11 +143,56 @@ struct IfElseNode : Node {
|
120 | 143 | result += "}";
|
121 | 144 | return result;
|
122 | 145 | }
|
| 146 | + |
| 147 | + int generate_dot(std::ostream &os, int parent_dot_id, |
| 148 | + const std::string &edge_label) override { |
| 149 | + int current_node_dot_id = current_id; |
| 150 | + current_id += 1; |
| 151 | + |
| 152 | + os << " node" << current_node_dot_id << " [label=\"If\"," |
| 153 | + << "shape=diamond, fillcolor=lightyellow];\n"; |
| 154 | + |
| 155 | + // Draw edge from parent if this is not the root node |
| 156 | + if (parent_dot_id != -1) { |
| 157 | + os << " node" << parent_dot_id << " -> node" << current_node_dot_id; |
| 158 | + if (!edge_label.empty()) { |
| 159 | + os << " [label=\"" << edge_label << "\"]"; |
| 160 | + } |
| 161 | + os << ";\n"; |
| 162 | + } |
| 163 | + assert(true_branch != nullptr); |
| 164 | + assert(true_branch->node != nullptr); |
| 165 | + true_branch->node->generate_dot(os, current_node_dot_id, "true"); |
| 166 | + assert(false_branch != nullptr); |
| 167 | + assert(false_branch->node != nullptr); |
| 168 | + false_branch->node->generate_dot(os, current_node_dot_id, "false"); |
| 169 | + return current_node_dot_id; |
| 170 | + } |
123 | 171 | };
|
124 | 172 |
|
125 | 173 | struct UnExploredNode : Node {
|
126 | 174 | UnExploredNode() {}
|
127 | 175 | std::string to_string() override { return "UnexploredNode"; }
|
| 176 | + |
| 177 | +protected: |
| 178 | + int generate_dot(std::ostream &os, int parent_dot_id, |
| 179 | + const std::string &edge_label) override { |
| 180 | + int current_node_dot_id = current_id++; |
| 181 | + |
| 182 | + os << " node" << current_node_dot_id |
| 183 | + << " [label=\"Unexplored\", shape=octagon, style=filled, " |
| 184 | + "fillcolor=lightgrey];\n"; |
| 185 | + |
| 186 | + if (parent_dot_id != -1) { |
| 187 | + os << " node" << parent_dot_id << " -> node" << current_node_dot_id; |
| 188 | + if (!edge_label.empty()) { |
| 189 | + os << " [label=\"" << edge_label << "\"]"; |
| 190 | + } |
| 191 | + os << ";\n"; |
| 192 | + } |
| 193 | + |
| 194 | + return current_node_dot_id; |
| 195 | + } |
128 | 196 | };
|
129 | 197 |
|
130 | 198 | static UnExploredNode unexplored;
|
@@ -162,6 +230,11 @@ class ExploreTree_t {
|
162 | 230 | return std::monostate();
|
163 | 231 | }
|
164 | 232 |
|
| 233 | + std::monostate to_graphviz(std::ostream &os) { |
| 234 | + root->node->to_graphviz(os); |
| 235 | + return std::monostate(); |
| 236 | + } |
| 237 | + |
165 | 238 | private:
|
166 | 239 | std::unique_ptr<NodeBox> root;
|
167 | 240 | NodeBox *cursor;
|
|
0 commit comments