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

Cleanup wto parts in fwd_analyzer #807

Merged
merged 1 commit into from
Nov 27, 2024
+52 −71
Merged

Cleanup wto parts in fwd_analyzer #807

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
90 changes: 26 additions & 64 deletions src/crab/fwd_analyzer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,43 +13,9 @@

namespace crab {

// Simple visitor to check if node is a member of the wto component.
class member_component_visitor final {
label_t _node;
bool _found;

public:
explicit member_component_visitor(const label_t& node) : _node(node), _found(false) {}

void operator()(const label_t& vertex) {
if (!_found) {
_found = (vertex == _node);
}
}

void operator()(const std::shared_ptr<wto_cycle_t>& c) {
if (!_found) {
_found = (c->head() == _node);
if (!_found) {
for (const auto& component : *c) {
if (_found) {
break;
}
std::visit(*this, component);
}
}
}
}

[[nodiscard]]
bool is_member() const {
return _found;
}
};

class interleaved_fwd_fixpoint_iterator_t final {
const cfg_t& _cfg;
wto_t _wto;
const wto_t _wto;
invariant_table_t _inv;

/// number of narrowing iterations. If the narrowing operator is
Expand All @@ -62,12 +28,11 @@ class interleaved_fwd_fixpoint_iterator_t final {
/// Used to skip the analysis until _entry is found
bool _skip{true};

private:
void set_pre(const label_t& label, const ebpf_domain_t& v) { _inv.at(label).pre = v; }

ebpf_domain_t get_pre(const label_t& node) { return _inv.at(node).pre; }
ebpf_domain_t get_pre(const label_t& node) const { return _inv.at(node).pre; }

ebpf_domain_t get_post(const label_t& node) { return _inv.at(node).post; }
ebpf_domain_t get_post(const label_t& node) const { return _inv.at(node).post; }

void transform_to_post(const label_t& label, ebpf_domain_t pre) {
const GuardedInstruction& ins = _cfg.at(label);
Expand All @@ -83,27 +48,7 @@ class interleaved_fwd_fixpoint_iterator_t final {
_inv.at(label).post = std::move(pre);
}

[[nodiscard]]
static ebpf_domain_t extrapolate(const ebpf_domain_t& before, const ebpf_domain_t& after,
const unsigned int iteration) {
/// number of iterations until triggering widening
constexpr auto _widening_delay = 2;

if (iteration < _widening_delay) {
return before | after;
}
return before.widen(after, iteration == _widening_delay);
}

static ebpf_domain_t refine(const ebpf_domain_t& before, const ebpf_domain_t& after, const unsigned int iteration) {
if (iteration == 1) {
return before & after;
} else {
return before.narrow(after);
}
}

ebpf_domain_t join_all_prevs(const label_t& node) {
ebpf_domain_t join_all_prevs(const label_t& node) const {
if (node == _cfg.entry_label()) {
return get_pre(node);
}
Expand All @@ -114,13 +59,13 @@ class interleaved_fwd_fixpoint_iterator_t final {
return res;
}

public:
explicit interleaved_fwd_fixpoint_iterator_t(const cfg_t& cfg) : _cfg(cfg), _wto(cfg) {
for (const auto& label : _cfg.labels()) {
_inv.emplace(label, invariant_map_pair{ebpf_domain_t::bottom(), ebpf_domain_t::bottom()});
}
}

public:
void operator()(const label_t& node);

void operator()(const std::shared_ptr<wto_cycle_t>& cycle);
Expand All @@ -146,6 +91,25 @@ invariant_table_t run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv
return std::move(analyzer._inv);
}

static ebpf_domain_t extrapolate(const ebpf_domain_t& before, const ebpf_domain_t& after,
const unsigned int iteration) {
/// number of iterations until triggering widening
constexpr auto _widening_delay = 2;

if (iteration < _widening_delay) {
return before | after;
}
return before.widen(after, iteration == _widening_delay);
}

static ebpf_domain_t refine(const ebpf_domain_t& before, const ebpf_domain_t& after, const unsigned int iteration) {
if (iteration == 1) {
return before & after;
} else {
return before.narrow(after);
}
}

elazarg marked this conversation as resolved.
Show resolved Hide resolved
void interleaved_fwd_fixpoint_iterator_t::operator()(const label_t& node) {
/** decide whether skip vertex or not **/
if (_skip && node == _cfg.entry_label()) {
Expand All @@ -167,11 +131,9 @@ void interleaved_fwd_fixpoint_iterator_t::operator()(const std::shared_ptr<wto_c
/** decide whether to skip cycle or not **/
bool entry_in_this_cycle = false;
if (_skip) {
// We only skip the analysis of cycle if _entry is not a
// We only skip the analysis of cycle if entry_label is not a
// component of it, included nested components.
member_component_visitor vis(_cfg.entry_label());
vis(cycle);
entry_in_this_cycle = vis.is_member();
entry_in_this_cycle = is_component_member(_cfg.entry_label(), cycle);
_skip = !entry_in_this_cycle;
if (_skip) {
return;
Expand Down
22 changes: 19 additions & 3 deletions src/crab/wto.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,22 @@
// where _visit_stack is roughly equivalent to a stack trace in the recursive algorithm.
// However, this scales much higher since it does not run out of stack memory.

bool is_component_member(const label_t& label, const cycle_or_label& component) {
if (const auto plabel = std::get_if<label_t>(&component)) {
return *plabel == label;
}
const auto cycle = std::get<std::shared_ptr<wto_cycle_t>>(component);
if (cycle->head() == label) {
return true;
}
for (const auto& sub_component : *cycle) {
if (is_component_member(label, sub_component)) {
return true;
}
}
return false;
}
elazarg marked this conversation as resolved.
Show resolved Hide resolved

bool wto_nesting_t::operator>(const wto_nesting_t& nesting) const {
const size_t this_size = this->_heads.size();
const size_t other_size = nesting._heads.size();
Expand Down Expand Up @@ -249,7 +265,7 @@ std::ostream& operator<<(std::ostream& o, const wto_t& wto) {
// is itself a head of a component, we want the head of whatever
// contains that entire component. Returns nullopt if the label is
// not nested, i.e., the head is logically the entry point of the CFG.
std::optional<label_t> wto_t::head(const label_t& label) {
std::optional<label_t> wto_t::head(const label_t& label) const {
const auto it = _containing_cycle.find(label);
if (it == _containing_cycle.end()) {
// Label is not in any cycle.
Expand All @@ -273,7 +289,7 @@ std::optional<label_t> wto_t::head(const label_t& label) {

wto_t::wto_t(const cfg_t& cfg) : wto_t{std::move(wto_builder_t(cfg).wto)} {}

std::vector<label_t> wto_t::collect_heads(const label_t& label) {
std::vector<label_t> wto_t::collect_heads(const label_t& label) const {
std::vector<label_t> heads;
for (auto h = head(label); h; h = head(*h)) {
heads.push_back(*h);
Expand All @@ -283,7 +299,7 @@ std::vector<label_t> wto_t::collect_heads(const label_t& label) {

// Compute the set of heads of the nested components containing a given label.
// See section 3.1 of the paper for discussion, which uses the notation w(c).
const wto_nesting_t& wto_t::nesting(const label_t& label) {
const wto_nesting_t& wto_t::nesting(const label_t& label) const {
if (!_nesting.contains(label)) {
// Not found in the cache yet, so construct the list of heads of the
// nested components containing the label, stored in reverse order.
Expand Down
11 changes: 7 additions & 4 deletions src/crab/wto.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,9 @@ class wto_cycle_t final {
}
};

// Check if node is a member of the wto component.
bool is_component_member(const label_t& label, const cycle_or_label& component);

class wto_t final {
// Top level components, in reverse order.
wto_partition_t _components;
Expand All @@ -102,10 +105,10 @@ class wto_t final {
// Table mapping label to the list of heads of cycles containing the label.
// This is an on-demand cache, since for most vertices the nesting is never
// looked at so we only create a wto_nesting_t for cases we actually need it.
std::map<label_t, wto_nesting_t> _nesting;
mutable std::map<label_t, wto_nesting_t> _nesting;

std::vector<label_t> collect_heads(const label_t& label);
std::optional<label_t> head(const label_t& label);
std::vector<label_t> collect_heads(const label_t& label) const;
std::optional<label_t> head(const label_t& label) const;

wto_t() = default;
friend class wto_builder_t;
Expand All @@ -124,7 +127,7 @@ class wto_t final {
}

friend std::ostream& operator<<(std::ostream& o, const wto_t& wto);
const wto_nesting_t& nesting(const label_t& label);
const wto_nesting_t& nesting(const label_t& label) const;
elazarg marked this conversation as resolved.
Show resolved Hide resolved

/**
* Visit the heads of all loops in the WTO.
Expand Down