Skip to content

Commit

Permalink
move printing code to asm_ostream.cpp and unify
Browse files Browse the repository at this point in the history 
Signed-off-by: Elazar Gershuni <[email protected]>
  • Loading branch information
@elazarg
elazarg committed Nov 24, 2024
1 parent e9d9933 commit d82d43f
Show file tree
Hide file tree
Showing 6 changed files with 109 additions and 117 deletions.
2 changes: 1 addition & 1 deletion src/asm_cfg.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -281,7 +281,7 @@ std::set<basic_block_t> basic_block_t::collect_basic_blocks(const cfg_t& cfg, co
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) {
if (seen.contains(next_label) || next_label == cfg.exit_label() || next_value.in_degree() != 1) {
break;
}

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
2 changes: 1 addition & 1 deletion src/crab/cfg.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -419,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
91 changes: 0 additions & 91 deletions src/crab_verifier.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,48 +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 bool simplify) const {
LineInfoPrinter printer{os};
for (const auto& bb : basic_block_t::collect_basic_blocks(cfg, simplify)) {
os << "\nPre-invariant : " << invariants.at(bb.first_label()).pre << "\n";
const crab::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 crab::value_t& node = cfg.get_node(label);
print_assertions(os, node);
print_instruction(os, node);
}
print_goto(os, cfg.get_node(bb.last_label()));
os << "\nPost-invariant: " << invariants.at(bb.last_label()).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 @@ -100,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
43 changes: 35 additions & 8 deletions src/crab_verifier.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,13 +14,39 @@ class Report final {
friend class Invariants;

public:
void print_reachability(std::ostream& os) const;
void print_warnings(std::ostream& os) const;
void print_all_messages(std::ostream& os) const;
std::set<std::string> all_messages() const;
std::set<std::string> reachability_set() const;
std::set<std::string> warning_set() const;
bool verified() const;
friend void print_reachability(std::ostream& os, const Report& report);
friend void print_warnings(std::ostream& os, const Report& report);
friend void print_all_messages(std::ostream& os, const Report& report);

std::set<std::string> 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> 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> 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 verified() const { return warnings.empty(); }
};

class Invariants final {
Expand All @@ -32,7 +58,6 @@ class Invariants final {
Invariants(const Invariants& invariants) = default;

bool is_valid_after(const label_t& label, const string_invariant& state) const;
void print_invariants(std::ostream& os, const cfg_t& cfg, bool simplify) const;

string_invariant invariant_at(const label_t& label) const;

Expand All @@ -41,6 +66,8 @@ class Invariants final {
int max_loop_count() const;
bool verified(const cfg_t& cfg) const;
Report check_assertions(const cfg_t& cfg) const;

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

Invariants analyze(const cfg_t& cfg);
Expand Down
9 changes: 4 additions & 5 deletions src/main/check.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -238,25 +238,24 @@ int main(int argc, char** argv) {
if (domain == "zoneCrab" || domain == "cfg") {
// Convert the instruction sequence to a control-flow graph.
try {
const auto verbosity = ebpf_verifier_options.verbosity_opts;
const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.cfg_opts);
if (domain == "cfg") {
std::cout << cfg;
std::cout << "\n";
print_cfg(std::cout, cfg, verbosity.simplify);
return 0;
}
const auto begin = std::chrono::steady_clock::now();
auto invariants = analyze(cfg);
const auto end = std::chrono::steady_clock::now();
const auto seconds = std::chrono::duration<double>(end - begin).count();
const auto verbosity = ebpf_verifier_options.verbosity_opts;
if (verbosity.print_invariants) {
invariants.print_invariants(std::cout, cfg, verbosity.simplify);
print_invariants(std::cout, cfg, verbosity.simplify, invariants);
}

bool pass;
if (verbosity.print_failures) {
auto report = invariants.check_assertions(cfg);
report.print_warnings(std::cout);
print_warnings(std::cout, report);
pass = report.verified();
} else {
pass = invariants.verified(cfg);
Expand Down

0 comments on commit d82d43f

Please sign in to comment.