Print simplified cfg

[elazarg]

This fixes #798 to re-introduce expected behavior for --simplify flag.

• Print "from" in addition to goto
• Split node printing into:
  -- print_label
  -- print_assertions
  -- print_instruction
  -- print_goto

Summary by CodeRabbit

• New Features

  • Introduced modular output functions for value_t and cfg_t, enhancing clarity in output processes.
  • Added new methods to cfg_t for printing various components, improving control flow graph representation.
  • Enhanced print_invariants method to support different output formats based on verbosity settings.

• Bug Fixes

  • Maintained consistent error handling in output functions.

• Refactor

  • Restructured output functions for better organization and maintainability.
  • Simplified the management of basic blocks within the control flow graph.

[coderabbitai]

Actionable comments posted: 3

🧹 Outside diff range comments (2)

src/asm_ostream.cpp (2)

Line range hint 101-117: Refactor duplicated code in print_goto and print_from functions.

The logic for printing comma-separated labels is duplicated. Extract this into a helper function.

+void print_label_list(std::ostream& o, const char* prefix, auto begin, auto end) {
+    if (begin != end) {
+        o << "  " << prefix;
+        while (begin != end) {
+            o << *begin;
+            ++begin;
+            if (begin == end) {
+                o << ";";
+            } else {
+                o << ",";
+            }
+        }
+    }
+    o << "\n";
+}

 void print_goto(std::ostream& o, const value_t& value) {
-    auto [it, et] = value.next_labels();
-    if (it != et) {
-        o << "  " << "goto ";
-        while (it != et) {
-            o << *it;
-            ++it;
-            if (it == et) {
-                o << ";";
-            } else {
-                o << ",";
-            }
-        }
-    }
-    o << "\n";
+    auto [begin, end] = value.next_labels();
+    print_label_list(o, "goto ", begin, end);
 }

 void print_from(std::ostream& o, const value_t& value) {
-    auto [it, et] = value.prev_labels();
-    if (it != et) {
-        o << "  " << "from ";
-        while (it != et) {
-            o << *it;
-            ++it;
-            if (it == et) {
-                o << ";";
-            } else {
-                o << ",";
-            }
-        }
-    }
-    o << "\n";
+    auto [begin, end] = value.prev_labels();
+    print_label_list(o, "from ", begin, end);
 }

Also applies to: 119-134

---

Line range hint 138-148: Maintain consistent formatting for edge information.

The edge information should follow the same indentation pattern as other parts of the output.

 std::ostream& operator<<(std::ostream& o, const cfg_t& cfg) {
     for (const label_t& label : cfg.sorted_labels()) {
         const auto& value = cfg.get_node(label);
         print_label(o, value);
         print_assertions(o, value);
         print_instruction(o, value);
-        o << "edges to:";
+        o << "  edges to:";
         for (const label_t& next_label : cfg.next_nodes(label)) {
             o << " " << next_label;
         }
         o << "\n";
     }
     return o;
 }

🧰 Tools

🪛 cppcheck (2.10-2)

[error] 134-134: Syntax Error

(internalAstError)

📜 Review details

Configuration used: CodeRabbit UI
Review profile: ASSERTIVE

📥 Commits

Reviewing files that changed from the base of the PR and between e4750ee and 5caf644.

📒 Files selected for processing (3)

• src/asm_ostream.cpp (2 hunks)
• src/crab/cfg.hpp (4 hunks)
• src/crab_verifier.cpp (1 hunks)

🧰 Additional context used

🪛 cppcheck (2.10-2)

src/asm_ostream.cpp

[error] 134-134: Syntax Error

(internalAstError)

🔇 Additional comments (2)

src/crab/cfg.hpp (2)

352-363: Const-qualified get_child and get_parent methods enhance const-correctness

Adding const versions of get_child and get_parent methods allows these functions to be used on const instances of cfg_t, improving the class's const-correctness.

---

386-387: Ensure C++20 support for operator<=> usage

The use of operator<=> (three-way comparison) in the basic_block_t class requires C++20 support. Verify that the project's build configuration enables C++20.

Run the following script to check if the project's build files specify C++20:

✅ Verification successful

C++20 support is properly configured in CMakeLists.txt

The project explicitly sets /std:c++20 compiler flag for MSVC, enabling C++20 features including the three-way comparison operator.

🏁 Scripts executed

The following scripts were executed for the analysis:

Script:

#!/bin/bash
# Description: Check if the project is configured to use C++20.

# Search for C++20 standard flags in build configuration files.
rg 'c\+\+20' -g '*CMakeLists.txt' -g '*.cmake' -g 'Makefile'

Length of output: 235

[coderabbitai]

🧹 Nitpick (assertive)

Include line information in simplified output

In the simplified output branch (lines 53-65), line information is not printed even when print_line_info is enabled. For consistency and to aid debugging, consider including line information in the simplified output.

Apply this diff to include line information:

+            LineInfoPrinter printer{os};
             for (const auto& bb : basic_block_t::collect_basic_blocks(cfg)) {
+                if (thread_local_options.verbosity_opts.print_line_info) {
+                    printer.print_line_info(bb.first_label());
+                }
                 os << "\nPre-invariant : " << invariants.at(bb.first_label()).pre << "\n";

Committable suggestion skipped: line range outside the PR's diff.

[coderabbitai]

Actionable comments posted: 4

🧹 Outside diff range comments (1)

src/crab/cfg.hpp (1)

Line range hint 426-451: Add documentation to basic_block_t constructors and methods

Providing documentation comments for the constructors and member functions like first_label() and last_label() would enhance code clarity and assist future maintainers.

📜 Review details

Configuration used: CodeRabbit UI
Review profile: ASSERTIVE

📥 Commits

Reviewing files that changed from the base of the PR and between 5caf644 and eff7e07.

📒 Files selected for processing (1)

• src/crab/cfg.hpp (4 hunks)

[coveralls]

coverage: 89.826% (-0.3%) from 90.143%
when pulling eff7e07 on simplify-print
into e4750ee on main.