Skip to content

Commit

Permalink
make wto const friendly
Browse files Browse the repository at this point in the history 
* mutable nesting field (cache)
* move is_component_member implementation to wto.cpp and simplify
* move class-static functions in fwd_analyzer.cpp to be file-static

Signed-off-by: Elazar Gershuni <[email protected]>
  • Loading branch information
@elazarg
elazarg committed Nov 26, 2024
1 parent 5195871 commit cb571ad
Show file tree
Hide file tree
Showing 3 changed files with 52 additions and 71 deletions.
90 changes: 26 additions & 64 deletions src/crab/fwd_analyzer.cpp
View file
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);
}
}

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

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

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

0 comments on commit cb571ad

Please sign in to comment.