Skip to content

Commit

Permalink
Uniform printing of simplified vs non-simplified (#805)
Browse files Browse the repository at this point in the history 
* Unified printing for simplify vs no-simplify
* Do not print entry and exit.
* Move printing code to asm_ostream.cpp and unify with cfg printing. 
* Pass simplify flag to collect_basic_blocks, and collect trivial ones if false.

Signed-off-by: Elazar Gershuni <[email protected]>
  • Loading branch information
@elazarg
elazarg authored Nov 24, 2024
1 parent 3d61f28 commit e09c6a7
Show file tree
Hide file tree
Showing 6 changed files with 163 additions and 170 deletions.
51 changes: 51 additions & 0 deletions src/asm_cfg.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -250,6 +250,57 @@ cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const pr
return cfg;
}

std::set<basic_block_t> basic_block_t::collect_basic_blocks(const cfg_t& cfg, const bool simplify) {
if (!simplify) {
std::set<basic_block_t> res;
for (const label_t& label : cfg.labels()) {
if (label != cfg.entry_label() && label != cfg.exit_label()) {
res.insert(basic_block_t{label});
}
}
return res;
}

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

const value_t* current_value = &cfg.get_node(label);
if (current_value->in_degree() == 1 && cfg.get_parent(label).out_degree() == 1) {
continue;
}
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 (seen.contains(next_label) || next_label == cfg.exit_label() || next_value.in_degree() != 1) {
break;
}

if (bb.first_label() == cfg.entry_label()) {
// Entry instruction is Undefined. We want to start with 0
bb.m_ts.clear();
}
bb.m_ts.push_back(next_label);

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

current_value = &next_value;
}
res.emplace(std::move(bb));
}
return res;
}

template <typename T>
static vector<label_t> unique(const std::pair<T, T>& be) {
vector<label_t> res;
Expand Down
79 changes: 68 additions & 11 deletions src/asm_ostream.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,12 @@

#include "asm_syntax.hpp"
#include "crab/cfg.hpp"
#include "crab/fwd_analyzer.hpp"
#include "crab/interval.hpp"
#include "crab/type_encoding.hpp"
#include "crab/variable.hpp"
#include "crab_utils/num_big.hpp"
#include "crab_verifier.hpp"
#include "helpers.hpp"
#include "platform.hpp"
#include "spec_type_descriptors.hpp"
Expand All @@ -21,6 +23,23 @@ using std::optional;
using std::string;
using std::vector;

struct LineInfoPrinter {
std::ostream& os;
std::string previous_source_line;

void print_line_info(const label_t& label) {
if (thread_local_options.verbosity_opts.print_line_info) {
const auto& line_info_map = thread_local_program_info.get().line_info;
const auto& line_info = line_info_map.find(label.from);
// Print line info only once.
if (line_info != line_info_map.end() && line_info->second.source_line != previous_source_line) {
os << "\n" << line_info->second << "\n";
previous_source_line = line_info->second.source_line;
}
}
}
};

namespace crab {

std::string number_t::to_string() const { return _n.str(); }
Expand Down Expand Up @@ -134,23 +153,61 @@ void print_from(std::ostream& o, const value_t& value) {
o << "\n";
}

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:";
for (const label_t& next_label : cfg.next_nodes(label)) {
o << " " << next_label;
static void print_cfg(std::ostream& os, const cfg_t& cfg, const bool simplify, const invariant_table_t* invariants) {
LineInfoPrinter printer{os};
for (const auto& bb : basic_block_t::collect_basic_blocks(cfg, simplify)) {
if (invariants) {
os << "\nPre-invariant : " << invariants->at(bb.first_label()).pre << "\n";
}
const value_t& first_node = cfg.get_node(bb.first_label());
print_from(os, first_node);
print_label(os, first_node);
for (const label_t& label : bb) {
printer.print_line_info(label);
const value_t& node = cfg.get_node(label);
print_assertions(os, node);
print_instruction(os, node);
}
print_goto(os, cfg.get_node(bb.last_label()));
if (invariants) {
os << "\nPost-invariant: " << invariants->at(bb.last_label()).post << "\n";
}
o << "\n";
}
return o;
os << "\n";
}
void print_cfg(std::ostream& os, const cfg_t& cfg, const bool simplify) { print_cfg(os, cfg, simplify, nullptr); }

} // namespace crab

void print_reachability(std::ostream& os, const Report& report) {
for (const auto& [label, notes] : report.reachability) {
for (const auto& msg : notes) {
os << label << ": " << msg << "\n";
}
}
os << "\n";
}

void print_warnings(std::ostream& os, const Report& report) {
LineInfoPrinter printer{os};
for (const auto& [label, warnings] : report.warnings) {
for (const auto& msg : warnings) {
printer.print_line_info(label);
os << label << ": " << msg << "\n";
}
}
os << "\n";
}

void print_all_messages(std::ostream& os, const Report& report) {
print_reachability(os, report);
print_warnings(os, report);
}

void print_invariants(std::ostream& os, const cfg_t& cfg, const bool simplify, const Invariants& invariants) {
print_cfg(os, cfg, simplify, &invariants.invariants);
}

namespace asm_syntax {
std::ostream& operator<<(std::ostream& os, const ArgSingle::Kind kind) {
switch (kind) {
Expand Down
40 changes: 2 additions & 38 deletions src/crab/cfg.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -385,43 +385,7 @@ class basic_block_t final {
public:
std::strong_ordering operator<=>(const basic_block_t& other) const { return first_label() <=> other.first_label(); }

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()) {
const label_t label = *worklist.begin();
worklist.erase(label);
if (seen.contains(label)) {
continue;
}
seen.insert(label);

const value_t* current_value = &cfg.get_node(label);
if (current_value->in_degree() == 1 && cfg.get_parent(label).out_degree() == 1) {
continue;
}
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_label == bb.first_label() || next_label == cfg.exit_label() || next_value.in_degree() != 1) {
break;
}

bb.m_ts.push_back(next_label);

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

current_value = &next_value;
}
res.emplace(std::move(bb));
}
return res;
}
static std::set<basic_block_t> collect_basic_blocks(const cfg_t& cfg, bool simplify);

explicit basic_block_t(const label_t& first_label) : m_ts{first_label} {}
basic_block_t(basic_block_t&&) noexcept = default;
Expand Down Expand Up @@ -455,7 +419,7 @@ class basic_block_t final {
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 cfg_t& cfg);
void print_cfg(std::ostream& os, const cfg_t& cfg, bool simplify);

} // end namespace crab

Expand Down
104 changes: 0 additions & 104 deletions src/crab_verifier.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,61 +26,12 @@ thread_local crab::lazy_allocator<program_info> thread_local_program_info;
thread_local ebpf_verifier_options_t thread_local_options;
void ebpf_verifier_clear_before_analysis();

struct LineInfoPrinter {
std::ostream& os;
std::string previous_source_line;

void print_line_info(const label_t& label) {
if (thread_local_options.verbosity_opts.print_line_info) {
const auto& line_info_map = thread_local_program_info.get().line_info;
const auto& line_info = line_info_map.find(label.from);
// Print line info only once.
if (line_info != line_info_map.end() && line_info->second.source_line != previous_source_line) {
os << "\n" << line_info->second << "\n";
previous_source_line = line_info->second.source_line;
}
}
}
};

bool Invariants::is_valid_after(const label_t& label, const string_invariant& state) const {
const ebpf_domain_t abstract_state =
ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);
return abstract_state <= invariants.at(label).post;
}

void Invariants::print_invariants(std::ostream& os, const cfg_t& cfg) const {
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";
}
} 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";
}

string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); }

crab::interval_t Invariants::exit_value() const { return invariants.at(label_t::exit).post.get_r0(); }
Expand Down Expand Up @@ -113,61 +64,6 @@ Invariants analyze(const cfg_t& cfg, const string_invariant& entry_invariant) {
ebpf_domain_t::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));
}

void Report::print_reachability(std::ostream& os) const {
for (const auto& [label, notes] : reachability) {
for (const auto& msg : notes) {
os << label << ": " << msg << "\n";
}
}
os << "\n";
}

void Report::print_warnings(std::ostream& os) const {
LineInfoPrinter printer{os};
for (const auto& [label, warnings] : warnings) {
for (const auto& msg : warnings) {
printer.print_line_info(label);
os << label << ": " << msg << "\n";
}
}
os << "\n";
}

void Report::print_all_messages(std::ostream& os) const {
print_reachability(os);
print_warnings(os);
}

std::set<std::string> Report::all_messages() const {
std::set<std::string> result = warning_set();
for (const auto& note : reachability_set()) {
result.insert(note);
}
return result;
}

std::set<std::string> Report::reachability_set() const {
std::set<std::string> result;
for (const auto& [label, warnings] : reachability) {
for (const auto& msg : warnings) {
result.insert(to_string(label) + ": " + msg);
}
}
return result;
}

std::set<std::string> Report::warning_set() const {
std::set<std::string> result;
for (const auto& [label, warnings] : warnings) {
for (const auto& msg : warnings) {
result.insert(to_string(label) + ": " + msg);
}
}
return result;
}

bool Report::verified() const { return warnings.empty(); }

bool Invariants::verified(const cfg_t& cfg) const {
for (const auto& [label, inv_pair] : invariants) {
if (inv_pair.pre.is_bottom()) {
Expand Down
Loading

0 comments on commit e09c6a7

Please sign in to comment.