14231336081

Committed 02 Apr 2025 11:08PM UTC coverage: 87.272% (-0.9%) from 88.177%

Build # 14231336081

Build Type

push

github

Committed by

web-flow

Commit Message

Propogate ebpf_verifier_options_t to thread_local_options (#856)

Signed-off-by: Alan Jowett <alanjo@microsoft.com>

Run Details

5 of 5 new or added lines in 2 files covered. (100.0%)

58 existing lines in 19 files now uncovered.

8324 of 9538 relevant lines covered (87.27%)

4881701.3 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

87.5

/src/crab/wto.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <ranges>

#include "wto.hpp"

// This file contains an iterative implementation of the recursive algorithm in
// Bourdoncle, "Efficient chaotic iteration strategies with widenings", 1993
// http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3574
// 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.

namespace crab {

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();
    if (this_size <= other_size) {
        // Can't be a superset.
        return false;
    }

    // Compare entries one at a time starting from the outermost
    // (i.e., end of the vectors).
    for (size_t index = 0; index < other_size; index++) {
        if (this->_heads[this_size - 1 - index] != nesting._heads[other_size - 1 - index]) {
            return false;
        }
    }
    return true;
}

enum class visit_task_type_t {
    PushSuccessors = 0,
    StartVisit = 1, // Start of the Visit() function defined in Figure 4 of the paper.
    ContinueVisit = 2,
};

struct visit_args_t {
    visit_task_type_t type;
    label_t vertex;
    wto_partition_t& partition;
    std::weak_ptr<wto_cycle_t> containing_cycle;

    visit_args_t(const visit_task_type_t t, label_t v, wto_partition_t& p, std::weak_ptr<wto_cycle_t> cc)
        : type(t), vertex(std::move(v)), partition(p), containing_cycle(std::move(cc)){};
};

struct wto_vertex_data_t {
    // Bourdoncle's thesis (reference [4]) is all in French but expands
    // DFN as "depth first number".
    int dfn{};
    int head_dfn{}; // Head value returned from Visit() in the paper.

    std::shared_ptr<wto_cycle_t> containing_cycle;
};
constexpr static int DFN_INF = std::numeric_limits<decltype(wto_vertex_data_t::dfn)>::max();

class wto_builder_t final {
    // Original control-flow graph.
    const cfg_t& _cfg;

    // The following members are named to match the names in the paper.
    std::map<label_t, wto_vertex_data_t> _vertex_data;
    int _num; // Highest DFN used so far.
    std::stack<label_t> _stack;

    std::stack<visit_args_t> _visit_stack;

    void push_successors(const label_t& vertex, wto_partition_t& partition,
                         const std::weak_ptr<wto_cycle_t>& containing_cycle);
    void start_visit(const label_t& vertex, wto_partition_t& partition,
                     const std::weak_ptr<wto_cycle_t>& containing_cycle);
    void continue_visit(const label_t& vertex, wto_partition_t& partition,
                        const std::weak_ptr<wto_cycle_t>& containing_cycle);

  public:
    wto_t wto;
    // Construct a Weak Topological Ordering from a control-flow graph using
    // the algorithm of figure 4 in the paper, where this constructor matches
    // what is shown there as the Partition function.
    explicit wto_builder_t(const cfg_t& cfg);
};

void wto_builder_t::push_successors(const label_t& vertex, wto_partition_t& partition,
                                    const std::weak_ptr<wto_cycle_t>& containing_cycle) {
    if (_vertex_data[vertex].dfn != 0) {
        // We found an alternate path to a node already visited, so nothing to do.
        return;
    }
    _vertex_data[vertex].dfn = ++_num;
    _stack.push(vertex);

    // Schedule the next task for this vertex once we're done with anything else.
    _visit_stack.emplace(visit_task_type_t::StartVisit, vertex, partition, containing_cycle);

    for (const label_t& succ : std::ranges::reverse_view(_cfg.children_of(vertex))) {
        if (_vertex_data[succ].dfn == 0) {
            _visit_stack.emplace(visit_task_type_t::PushSuccessors, succ, partition, containing_cycle);
        }
    }
}

void wto_builder_t::start_visit(const label_t& vertex, wto_partition_t& partition,
                                const std::weak_ptr<wto_cycle_t>& containing_cycle) {
    wto_vertex_data_t& vertex_data = _vertex_data[vertex];
    int head_dfn = vertex_data.dfn;
    bool loop = false;
    for (const label_t& succ : _cfg.children_of(vertex)) {
        const wto_vertex_data_t& data = _vertex_data[succ];
        int min_dfn = data.dfn;
        if (data.head_dfn != 0 && data.dfn != DFN_INF) {
            min_dfn = data.head_dfn;
        }
        if (min_dfn <= head_dfn) {
            head_dfn = min_dfn;
            loop = true;
        }
    }

    // Create a new cycle component inside the containing cycle.
    const auto cycle = std::make_shared<wto_cycle_t>(containing_cycle);

    if (head_dfn == vertex_data.dfn) {
        vertex_data.dfn = DFN_INF;
        label_t element = _stack.top();
        _stack.pop();
        if (loop) {
            while (element != vertex) {
                _vertex_data[element].dfn = 0;
                _vertex_data[element].head_dfn = 0;
                element = _stack.top();
                _stack.pop();
            }
            vertex_data.head_dfn = head_dfn;

            // Stash a reference to the cycle.
            _vertex_data[vertex].containing_cycle = cycle;

            // Schedule the next task for this vertex once we're done with anything else.
            _visit_stack.emplace(visit_task_type_t::ContinueVisit, vertex, partition, cycle);

            // Walk the control flow graph, adding nodes to this cycle.
            // This is the Component() function described in figure 4 of the paper.
            for (const label_t& succ : std::ranges::reverse_view(_cfg.children_of(vertex))) {
                if (_vertex_data.at(succ).dfn == 0) {
                    _visit_stack.emplace(visit_task_type_t::PushSuccessors, succ, cycle->_components, cycle);
                }
            }
            return;
        }
        // Insert a new vertex component vertex into the current partition.
        partition.emplace_back(vertex);

        // Remember that we put the vertex into the caller's cycle.
        wto._containing_cycle.emplace(vertex, containing_cycle);
    }
    vertex_data.head_dfn = head_dfn;
}

void wto_builder_t::continue_visit(const label_t& vertex, wto_partition_t& partition,
                                   const std::weak_ptr<wto_cycle_t>& containing_cycle) {
    // Add the vertex at the start of the cycle
    // (end of the vector which stores the cycle in reverse order).
    auto cycle = containing_cycle.lock();

    cycle->_components.push_back(vertex);

    // Insert the component into the current partition.
    partition.emplace_back(cycle);

    // Remember that we put the vertex into the new cycle.
    wto._containing_cycle.emplace(vertex, cycle);
}

wto_builder_t::wto_builder_t(const cfg_t& cfg) : _cfg(cfg) {
    // Create a map for holding a "depth-first number (DFN)" for each vertex.
    for (const label_t& label : cfg.labels()) {
        _vertex_data.emplace(label, 0);
    }

    // Initialize the DFN counter.
    _num = 0;

    // Push the entry vertex on the stack to process.
    _visit_stack.emplace(visit_args_t(visit_task_type_t::PushSuccessors, cfg.entry_label(), wto._components, {}));

    // Keep processing tasks until we're done.
    while (!_visit_stack.empty()) {
        visit_args_t args2 = _visit_stack.top();
        _visit_stack.pop();
        switch (args2.type) {
        case visit_task_type_t::PushSuccessors:
            push_successors(args2.vertex, args2.partition, args2.containing_cycle);
            break;
        case visit_task_type_t::StartVisit: start_visit(args2.vertex, args2.partition, args2.containing_cycle); break;
        case visit_task_type_t::ContinueVisit:
            continue_visit(args2.vertex, args2.partition, args2.containing_cycle);
            break;
        default: break;
        }
    }
}

class print_visitor {
    std::ostream& o;

  public:
    explicit print_visitor(std::ostream& o) : o(o) {}

    void operator()(const label_t& label) { o << label; }

    void operator()(const wto_cycle_t& cycle) {
        o << "( ";
        for (const auto& component : cycle) {
            std::visit(*this, component);
            o << " ";
        }
        o << ")";
    }

    void operator()(const std::shared_ptr<wto_cycle_t>& e) {
        if (e != nullptr) {
            (*this)(*e);
        }
    }

    void operator()(const wto_partition_t& partition) {
        for (const auto& p : std::ranges::reverse_view(partition)) {
            std::visit(*this, p);
            o << " ";
        }
    }

    // Output the nesting in order from outermost to innermost.
    void operator()(const wto_nesting_t& nesting) {
        for (const auto& _head : std::ranges::reverse_view(nesting._heads)) {
            o << _head << " ";
        }
    }
};

std::ostream& operator<<(std::ostream& o, const wto_t& wto) {
    print_visitor{o}(wto._components);
    return o << std::endl;
}

// Get the vertex at the head of the component containing a given
// label, as discussed in section 4.2 of the paper.  If the label
// 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) const {
    const auto it = _containing_cycle.find(label);
    if (it == _containing_cycle.end()) {
        // Label is not in any cycle.
        return {};
    }
    const std::shared_ptr<wto_cycle_t> cycle = it->second.lock();
    if (cycle == nullptr) {
        return {};
    }
    if (const label_t& first = cycle->head(); first != label) {
        // Return the head of the cycle the label is inside.
        return first;
    }

    // This label is already the head of a cycle, so get the cycle's parent.
    if (const auto parent = cycle->_containing_cycle.lock()) {
        return parent->head();
    }
    return {};
}

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) const {
    std::vector<label_t> heads;
    for (auto h = head(label); h; h = head(*h)) {
        heads.push_back(*h);
    }
    return heads;
}

// 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 {
    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.
        _nesting.emplace(label, collect_heads(label));
    }
    return _nesting.at(label);
}
} // namespace crab

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <ranges>
4
5	#include "wto.hpp"
6
7	// This file contains an iterative implementation of the recursive algorithm in
8	// Bourdoncle, "Efficient chaotic iteration strategies with widenings", 1993
9	// http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.3574
10	// where _visit_stack is roughly equivalent to a stack trace in the recursive algorithm.
11	// However, this scales much higher since it does not run out of stack memory.
12
13	namespace crab {
14
15	bool is_component_member(const label_t& label, const cycle_or_label& component) {	×
16	if (const auto plabel = std::get_if<label_t>(&component)) {	×
17	return *plabel == label;	×
18	}
19	const auto cycle = std::get<std::shared_ptr<wto_cycle_t>>(component);	×
20	if (cycle->head() == label) {	×
21	return true;
22	}
23	for (const auto& sub_component : *cycle) {	×
24	if (is_component_member(label, sub_component)) {	×
25	return true;	×
26	}
27	}
28	return false;
29	}	×
30
31	bool wto_nesting_t::operator>(const wto_nesting_t& nesting) const {	38✔
32	const size_t this_size = this->_heads.size();	38✔
33	const size_t other_size = nesting._heads.size();	38✔
34	if (this_size <= other_size) {	38✔
35	// Can't be a superset.
36	return false;
37	}
38
39	// Compare entries one at a time starting from the outermost
40	// (i.e., end of the vectors).
41	for (size_t index = 0; index < other_size; index++) {	19✔
42	if (this->_heads[this_size - 1 - index] != nesting._heads[other_size - 1 - index]) {	×
43	return false;
44	}
45	}
46	return true;
47	}
48
49	enum class visit_task_type_t {
50	PushSuccessors = 0,
51	StartVisit = 1, // Start of the Visit() function defined in Figure 4 of the paper.
52	ContinueVisit = 2,
53	};
54
55	struct visit_args_t {
56	visit_task_type_t type;
57	label_t vertex;
58	wto_partition_t& partition;
59	std::weak_ptr<wto_cycle_t> containing_cycle;
60
61	visit_args_t(const visit_task_type_t t, label_t v, wto_partition_t& p, std::weak_ptr<wto_cycle_t> cc)	341,487✔
62	: type(t), vertex(std::move(v)), partition(p), containing_cycle(std::move(cc)){};	341,487✔
63	};
64
UNCOV 65	struct wto_vertex_data_t {	×
66	// Bourdoncle's thesis (reference [4]) is all in French but expands
67	// DFN as "depth first number".
68	int dfn{};
69	int head_dfn{}; // Head value returned from Visit() in the paper.
70
71	std::shared_ptr<wto_cycle_t> containing_cycle;
72	};
73	constexpr static int DFN_INF = std::numeric_limits<decltype(wto_vertex_data_t::dfn)>::max();
74
75	class wto_builder_t final {
76	// Original control-flow graph.
77	const cfg_t& _cfg;
78
79	// The following members are named to match the names in the paper.
80	std::map<label_t, wto_vertex_data_t> _vertex_data;
81	int _num; // Highest DFN used so far.
82	std::stack<label_t> _stack;
83
84	std::stack<visit_args_t> _visit_stack;
85
86	void push_successors(const label_t& vertex, wto_partition_t& partition,
87	const std::weak_ptr<wto_cycle_t>& containing_cycle);
88	void start_visit(const label_t& vertex, wto_partition_t& partition,
89	const std::weak_ptr<wto_cycle_t>& containing_cycle);
90	void continue_visit(const label_t& vertex, wto_partition_t& partition,
91	const std::weak_ptr<wto_cycle_t>& containing_cycle);
92
93	public:
94	wto_t wto;
95	// Construct a Weak Topological Ordering from a control-flow graph using
96	// the algorithm of figure 4 in the paper, where this constructor matches
97	// what is shown there as the Partition function.
98	explicit wto_builder_t(const cfg_t& cfg);
99	};
100
101	void wto_builder_t::push_successors(const label_t& vertex, wto_partition_t& partition,	170,725✔
102	const std::weak_ptr<wto_cycle_t>& containing_cycle) {
103	if (_vertex_data[vertex].dfn != 0) {	170,725✔
104	// We found an alternate path to a node already visited, so nothing to do.
105	return;
106	}
107	_vertex_data[vertex].dfn = ++_num;	170,723✔
108	_stack.push(vertex);	170,723✔
109
110	// Schedule the next task for this vertex once we're done with anything else.
111	_visit_stack.emplace(visit_task_type_t::StartVisit, vertex, partition, containing_cycle);	170,723✔
112
113	for (const label_t& succ : std::ranges::reverse_view(_cfg.children_of(vertex))) {	352,858✔
114	if (_vertex_data[succ].dfn == 0) {	182,135✔
115	_visit_stack.emplace(visit_task_type_t::PushSuccessors, succ, partition, containing_cycle);	169,419✔
116	}
117	}
118	}
119
120	void wto_builder_t::start_visit(const label_t& vertex, wto_partition_t& partition,	170,723✔
121	const std::weak_ptr<wto_cycle_t>& containing_cycle) {
122	wto_vertex_data_t& vertex_data = _vertex_data[vertex];	170,723✔
123	int head_dfn = vertex_data.dfn;	170,723✔
124	bool loop = false;	170,723✔
125	for (const label_t& succ : _cfg.children_of(vertex)) {	352,858✔
126	const wto_vertex_data_t& data = _vertex_data[succ];	182,135✔
127	int min_dfn = data.dfn;	182,135✔
128	if (data.head_dfn != 0 && data.dfn != DFN_INF) {	182,135✔
129	min_dfn = data.head_dfn;	129✔
130	}
131	if (min_dfn <= head_dfn) {	182,135✔
132	head_dfn = min_dfn;	169✔
133	loop = true;	169✔
134	}
135	}
136
137	// Create a new cycle component inside the containing cycle.
138	const auto cycle = std::make_shared<wto_cycle_t>(containing_cycle);	170,723✔
139
140	if (head_dfn == vertex_data.dfn) {	170,723✔
141	vertex_data.dfn = DFN_INF;	170,596✔
142	label_t element = _stack.top();	170,596✔
143	_stack.pop();	170,596✔
144	if (loop) {	170,596✔
145	while (element != vertex) {	166✔
146	_vertex_data[element].dfn = 0;	127✔
147	_vertex_data[element].head_dfn = 0;	127✔
148	element = _stack.top();	127✔
149	_stack.pop();	127✔
150	}
151	vertex_data.head_dfn = head_dfn;	39✔
152
153	// Stash a reference to the cycle.
154	_vertex_data[vertex].containing_cycle = cycle;	39✔
155
156	// Schedule the next task for this vertex once we're done with anything else.
157	_visit_stack.emplace(visit_task_type_t::ContinueVisit, vertex, partition, cycle);	39✔
158
159	// Walk the control flow graph, adding nodes to this cycle.
160	// This is the Component() function described in figure 4 of the paper.
161	for (const label_t& succ : std::ranges::reverse_view(_cfg.children_of(vertex))) {	85✔
162	if (_vertex_data.at(succ).dfn == 0) {	46✔
163	_visit_stack.emplace(visit_task_type_t::PushSuccessors, succ, cycle->_components, cycle);	40✔
164	}
165	}
166	return;	39✔
167	}
168	// Insert a new vertex component vertex into the current partition.
169	partition.emplace_back(vertex);	170,557✔
170
171	// Remember that we put the vertex into the caller's cycle.
172	wto._containing_cycle.emplace(vertex, containing_cycle);	170,557✔
173	}	170,596✔
174	vertex_data.head_dfn = head_dfn;	170,684✔
175	}
176
177	void wto_builder_t::continue_visit(const label_t& vertex, wto_partition_t& partition,	39✔
178	const std::weak_ptr<wto_cycle_t>& containing_cycle) {
179	// Add the vertex at the start of the cycle
180	// (end of the vector which stores the cycle in reverse order).
181	auto cycle = containing_cycle.lock();	39✔
182
183	cycle->_components.push_back(vertex);	39✔
184
185	// Insert the component into the current partition.
186	partition.emplace_back(cycle);	39✔
187
188	// Remember that we put the vertex into the new cycle.
189	wto._containing_cycle.emplace(vertex, cycle);	39✔
190	}	39✔
191
192	wto_builder_t::wto_builder_t(const cfg_t& cfg) : _cfg(cfg) {	1,266✔
193	// Create a map for holding a "depth-first number (DFN)" for each vertex.
194	for (const label_t& label : cfg.labels()) {	172,031✔
195	_vertex_data.emplace(label, 0);	170,765✔
196	}
197
198	// Initialize the DFN counter.
199	_num = 0;	1,266✔
200
201	// Push the entry vertex on the stack to process.
202	_visit_stack.emplace(visit_args_t(visit_task_type_t::PushSuccessors, cfg.entry_label(), wto._components, {}));	2,532✔
203
204	// Keep processing tasks until we're done.
205	while (!_visit_stack.empty()) {	342,753✔
206	visit_args_t args2 = _visit_stack.top();	341,487✔
207	_visit_stack.pop();	341,487✔
208	switch (args2.type) {	341,487✔
209	case visit_task_type_t::PushSuccessors:	170,725✔
210	push_successors(args2.vertex, args2.partition, args2.containing_cycle);	170,725✔
211	break;
212	case visit_task_type_t::StartVisit: start_visit(args2.vertex, args2.partition, args2.containing_cycle); break;	170,723✔
213	case visit_task_type_t::ContinueVisit:	39✔
214	continue_visit(args2.vertex, args2.partition, args2.containing_cycle);	39✔
215	break;
216	default: break;
217	}
218	}	341,487✔
219	}	1,266✔
220
221	class print_visitor {
222	std::ostream& o;
223
224	public:
225	explicit print_visitor(std::ostream& o) : o(o) {}	3✔
226
227	void operator()(const label_t& label) { o << label; }	23✔
228
229	void operator()(const wto_cycle_t& cycle) {	4✔
230	o << "( ";	4✔
231	for (const auto& component : cycle) {	16✔
232	std::visit(*this, component);	12✔
233	o << " ";	12✔
234	}
235	o << ")";	4✔
236	}	4✔
237
238	void operator()(const std::shared_ptr<wto_cycle_t>& e) {	4✔
239	if (e != nullptr) {	4✔
240	(this)(e);	4✔
241	}
242	}
243
244	void operator()(const wto_partition_t& partition) {	3✔
245	for (const auto& p : std::ranges::reverse_view(partition)) {	18✔
246	std::visit(*this, p);	15✔
247	o << " ";	15✔
248	}
249	}	3✔
250
251	// Output the nesting in order from outermost to innermost.
252	void operator()(const wto_nesting_t& nesting) {
253	for (const auto& _head : std::ranges::reverse_view(nesting._heads)) {
254	o << _head << " ";
255	}
256	}
257	};
258
259	std::ostream& operator<<(std::ostream& o, const wto_t& wto) {	3✔
260	print_visitor{o}(wto._components);	3✔
261	return o << std::endl;	3✔
262	}
263
264	// Get the vertex at the head of the component containing a given
265	// label, as discussed in section 4.2 of the paper. If the label
266	// is itself a head of a component, we want the head of whatever
267	// contains that entire component. Returns nullopt if the label is
268	// not nested, i.e., the head is logically the entry point of the CFG.
269	std::optional<label_t> wto_t::head(const label_t& label) const {	76✔
270	const auto it = _containing_cycle.find(label);	76✔
271	if (it == _containing_cycle.end()) {	76✔
272	// Label is not in any cycle.
273	return {};	×
274	}
275	const std::shared_ptr<wto_cycle_t> cycle = it->second.lock();	76✔
276	if (cycle == nullptr) {	76✔
277	return {};	19✔
278	}
279	if (const label_t& first = cycle->head(); first != label) {	57✔
280	// Return the head of the cycle the label is inside.
281	return first;	19✔
282	}
283
284	// This label is already the head of a cycle, so get the cycle's parent.
285	if (const auto parent = cycle->_containing_cycle.lock()) {	38✔
286	return parent->head();	×
UNCOV 287	}	×
288	return {};	38✔
289	}	76✔
290
291	wto_t::wto_t(const cfg_t& cfg) : wto_t{std::move(wto_builder_t(cfg).wto)} {}	1,266✔
292
293	std::vector<label_t> wto_t::collect_heads(const label_t& label) const {	57✔
294	std::vector<label_t> heads;	57✔
295	for (auto h = head(label); h; h = head(*h)) {	152✔
296	heads.push_back(*h);	19✔
UNCOV 297	}	×
298	return heads;	57✔
299	}	×
300
301	// Compute the set of heads of the nested components containing a given label.
302	// See section 3.1 of the paper for discussion, which uses the notation w(c).
303	const wto_nesting_t& wto_t::nesting(const label_t& label) const {	57✔
304	if (!_nesting.contains(label)) {	57✔
305	// Not found in the cache yet, so construct the list of heads of the
306	// nested components containing the label, stored in reverse order.
307	_nesting.emplace(label, collect_heads(label));	57✔
308	}
309	return _nesting.at(label);	57✔
310	}
311	} // namespace crab

vbpf / ebpf-verifier / 14231336081

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous