Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Print simplified cfg #799

Merged
merged 2 commits into from
Nov 23, 2024
Merged

Print simplified cfg #799

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5caf644
print simplified cfg
elazarg Nov 22, 2024
eff7e07
CR comment
elazarg Nov 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 31 additions & 7 deletions src/asm_ostream.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -87,14 +87,18 @@ void print_dot(const cfg_t& cfg, const std::string& outfile) {
print_dot(cfg, out);
}

std::ostream& operator<<(std::ostream& o, const value_t& value) {
o << value.label() << ":\n";
const auto ins = value.instruction();
for (const auto& pre : ins.preconditions) {
void print_label(std::ostream& o, const value_t& value) { o << value.label() << ":\n"; }

void print_assertions(std::ostream& o, const value_t& value) {
for (const auto& pre : value.instruction().preconditions) {
o << " "
<< "assert " << pre << ";\n";
}
o << " " << ins.cmd << ";\n";
}

void print_instruction(std::ostream& o, const value_t& value) { o << " " << value.instruction().cmd << ";\n"; }

void print_goto(std::ostream& o, const value_t& value) {
auto [it, et] = value.next_labels();
if (it != et) {
o << " "
Expand All @@ -110,12 +114,32 @@ std::ostream& operator<<(std::ostream& o, const value_t& value) {
}
}
o << "\n";
return o;
}

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";
}

std::ostream& operator<<(std::ostream& o, const cfg_t& cfg) {
for (const label_t& label : cfg.sorted_labels()) {
o << cfg.get_node(label);
const auto& value = cfg.get_node(label);
print_label(o, value);
print_assertions(o, value);
print_instruction(o, value);
o << "edges to:";
for (const label_t& next_label : cfg.next_nodes(label)) {
o << " " << next_label;
Expand Down
116 changes: 46 additions & 70 deletions src/crab/cfg.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,12 @@ class value_t final {
}
};

void print_label(std::ostream& o, const value_t& value);
void print_assertions(std::ostream& o, const value_t& value);
void print_instruction(std::ostream& o, const value_t& value);
void print_goto(std::ostream& o, const value_t& value);
void print_from(std::ostream& o, const value_t& value);
elazarg marked this conversation as resolved.
Show resolved Hide resolved

/// Control-Flow Graph
class cfg_t final {
public:
Expand Down Expand Up @@ -343,6 +349,18 @@ class cfg_t final {
return get_node(*rng.begin());
}

const value_t& get_child(const label_t& b) const {
assert(has_one_child(b));
const auto rng = next_nodes(b);
return get_node(*rng.begin());
}

const value_t& get_parent(const label_t& b) const {
assert(has_one_parent(b));
const auto rng = prev_nodes(b);
return get_node(*rng.begin());
}

elazarg marked this conversation as resolved.
Show resolved Hide resolved
private:
// Helpers
[[nodiscard]]
Expand All @@ -359,88 +377,66 @@ class cfg_t final {
};

class basic_block_t final {
friend class cfg_t;

public:
basic_block_t(const basic_block_t&) = delete;

using label_vec_t = std::set<label_t>;
using stmt_list_t = std::vector<GuardedInstruction*>;
using iterator = stmt_list_t::iterator;
using stmt_list_t = std::vector<label_t>;
using const_iterator = stmt_list_t::const_iterator;
using reverse_iterator = stmt_list_t::reverse_iterator;
using const_reverse_iterator = stmt_list_t::const_reverse_iterator;

private:
label_t m_label;
stmt_list_t m_ts;

public:
static std::map<label_t, basic_block_t> collect_basic_blocks(cfg_t& cfg) {
std::map<label_t, basic_block_t> res;
std::strong_ordering operator<=>(const basic_block_t& other) const { return first_label() <=> other.first_label(); }

elazarg marked this conversation as resolved.
Show resolved Hide resolved
static std::set<basic_block_t> collect_basic_blocks(const cfg_t& cfg) {
std::set<basic_block_t> res;

std::set worklist(cfg.label_begin(), cfg.label_end());
std::set<label_t> seen;
while (!worklist.empty()) {
label_t label = *worklist.begin();
const label_t label = *worklist.begin();
worklist.erase(label);
if (seen.contains(label)) {
continue;
}
seen.insert(label);

const value_t& value = cfg.get_node(label);
if (value.in_degree() == 1 && cfg.get_parent(label).out_degree() == 1) {
const value_t* current_value = &cfg.get_node(label);
if (current_value->in_degree() == 1 && cfg.get_parent(label).out_degree() == 1) {
continue;
}
res.emplace(label, label);
basic_block_t& bb = res.at(label);
while (value.out_degree() == 1) {
value_t& next_value = cfg.get_child(label);
basic_block_t bb{label};
while (current_value->out_degree() == 1) {
const value_t& next_value = cfg.get_child(bb.last_label());
const label_t& next_label = next_value.label();

if (&next_value == &value || next_value.in_degree() != 1) {
if (next_label == bb.first_label() || next_label == cfg.exit_label() || next_value.in_degree() != 1) {
break;
}
if (next_value.label() == cfg.exit_label()) {
break;
}
worklist.erase(next_value.label());

bb.m_ts.push_back(&next_value.instruction());
bb.m_ts.push_back(next_label);

worklist.erase(next_label);
seen.insert(next_label);

// delete next_bb entirely
// remove(next_value.label());
seen.insert(next_value.label());
current_value = &next_value;
}
res.emplace(std::move(bb));
elazarg marked this conversation as resolved.
Show resolved Hide resolved
}
return res;
}

void insert(GuardedInstruction* arg) {
assert(label() != label_t::entry);
assert(label() != label_t::exit);
m_ts.push_back(arg);
}
explicit basic_block_t(const label_t& first_label) : m_ts{first_label} {}
basic_block_t(basic_block_t&&) noexcept = default;
basic_block_t(const basic_block_t&) = default;

/// Insert a GuardedInstruction at the front of the basic block.
/// @note Cannot modify entry or exit blocks.
void insert_front(GuardedInstruction* arg) {
assert(label() != label_t::entry);
assert(label() != label_t::exit);
m_ts.insert(m_ts.begin(), arg);
[[nodiscard]]
label_t first_label() const {
return m_ts.at(0);
elazarg marked this conversation as resolved.
Show resolved Hide resolved
}

explicit basic_block_t(label_t _label) : m_label(std::move(_label)) {}

~basic_block_t() = default;

[[nodiscard]]
label_t label() const {
return m_label;
label_t last_label() const {
return m_ts.at(m_ts.size() - 1);
}

iterator begin() { return (m_ts.begin()); }
iterator end() { return (m_ts.end()); }
[[nodiscard]]
const_iterator begin() const {
return m_ts.begin();
Expand All @@ -450,35 +446,15 @@ class basic_block_t final {
return m_ts.end();
}

reverse_iterator rbegin() { return (m_ts.rbegin()); }
reverse_iterator rend() { return (m_ts.rend()); }
[[nodiscard]]
const_reverse_iterator rbegin() const {
return m_ts.rbegin();
}
[[nodiscard]]
const_reverse_iterator rend() const {
return m_ts.rend();
}

[[nodiscard]]
size_t size() const {
return gsl::narrow<size_t>(std::distance(begin(), end()));
}

// insert all statements of other at the back
void move_back(basic_block_t& other) {
m_ts.reserve(m_ts.size() + other.m_ts.size());
std::ranges::move(other.m_ts, std::back_inserter(m_ts));
return m_ts.size();
}

void swap_instructions(stmt_list_t& ts) { std::swap(m_ts, ts); }
};

void print_dot(const cfg_t& cfg, std::ostream& out);
void print_dot(const cfg_t& cfg, const std::string& outfile);

std::ostream& operator<<(std::ostream& o, const value_t& value);
std::ostream& operator<<(std::ostream& o, const cfg_t& cfg);

} // end namespace crab
Expand Down
34 changes: 27 additions & 7 deletions src/crab_verifier.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,13 +50,33 @@ bool Invariants::is_valid_after(const label_t& label, const string_invariant& st
}

void Invariants::print_invariants(std::ostream& os, const cfg_t& cfg) const {
LineInfoPrinter printer{os};
for (const label_t& label : cfg.sorted_labels()) {
printer.print_line_info(label);
const auto& inv_pair = invariants.at(label);
os << "\nPre-invariant : " << inv_pair.pre << "\n";
os << cfg.get_node(label);
os << "\nPost-invariant: " << inv_pair.post << "\n";
if (thread_local_options.verbosity_opts.simplify) {
for (const auto& bb : basic_block_t::collect_basic_blocks(cfg)) {
os << "\nPre-invariant : " << invariants.at(bb.first_label()).pre << "\n";
print_from(os, cfg.get_node(bb.first_label()));
print_label(os, cfg.get_node(bb.first_label()));
for (const auto& label : bb) {
const auto& value = cfg.get_node(label);
print_assertions(os, value);
print_instruction(os, value);
}
print_goto(os, cfg.get_node(bb.last_label()));
os << "\nPost-invariant: " << invariants.at(bb.last_label()).post << "\n";
}
Comment on lines +53 to +65
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🧹 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.

} else {
LineInfoPrinter printer{os};
for (const label_t& label : cfg.sorted_labels()) {
printer.print_line_info(label);
const auto& inv_pair = invariants.at(label);
os << "\nPre-invariant : " << inv_pair.pre << "\n";
const auto& value = cfg.get_node(label);
print_from(os, value);
print_label(os, value);
print_assertions(os, value);
print_instruction(os, value);
print_goto(os, value);
os << "\nPost-invariant: " << inv_pair.post << "\n";
}
}
os << "\n";
}
Expand Down
Loading