13958948275

Committed 19 Mar 2025 11:53PM UTC coverage: 88.194% (-0.5%) from 88.66%

Build # 13958948275

Build Type

push

github

Committed by

web-flow

Commit Message

Finite domain (#849)

* Move arithmetic and bit operations functions to finite_domain.cpp
* Remove operator-= (now havoc) and operator+= (now add_constraint)
* Abort early when registers are not usable; clear type variable instead of explicitly assigning T_UNINIT. Update YAML tests accordingly
---------
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

847 of 898 new or added lines in 11 files covered. (94.32%)

57 existing lines in 8 files now uncovered.

8628 of 9783 relevant lines covered (88.19%)

9034663.84 hits per line

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

52.5

/src/crab/bitset_domain.cpp

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include "bitset_domain.hpp"
4	#include <ostream>
5
UNCOV 6	std::ostream& operator<<(std::ostream& o, const bitset_domain_t& b) {	×
UNCOV 7	o << "Numbers -> {";	×
UNCOV 8	bool first = true;	×
UNCOV 9	for (int i = -EBPF_TOTAL_STACK_SIZE; i < 0; i++) {	×
UNCOV 10	if (b.non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + i]) {	×
UNCOV 11	continue;	×
12	}
UNCOV 13	if (!first) {	×
UNCOV 14	o << ", ";	×
15	}
UNCOV 16	first = false;	×
UNCOV 17	o << "[" << EBPF_TOTAL_STACK_SIZE + i;	×
UNCOV 18	int j = i + 1;	×
UNCOV 19	for (; j < 0; j++) {	×
UNCOV 20	if (b.non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + j]) {	×
21	break;
22	}
23	}
UNCOV 24	if (j > i + 1) {	×
UNCOV 25	o << "..." << EBPF_TOTAL_STACK_SIZE + j - 1;	×
26	}
UNCOV 27	o << "]";	×
UNCOV 28	i = j;	×
29	}
UNCOV 30	o << "}";	×
UNCOV 31	return o;	×
32	}
33
34	string_invariant bitset_domain_t::to_set() const {	1,386✔
35	if (this->is_bottom()) {	1,386✔
36	return string_invariant::bottom();
37	}
38	if (this->is_top()) {	1,386✔
39	return string_invariant::top();	1,232✔
40	}
41
42	std::set<std::string> result;	154✔
43	for (int i = -EBPF_TOTAL_STACK_SIZE; i < 0; i++) {	629,628✔
44	if (non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + i]) {	629,474✔
45	continue;	629,320✔
46	}
47	std::string value = "s[" + std::to_string(EBPF_TOTAL_STACK_SIZE + i);	154✔
48	int j = i + 1;	154✔
49	for (; j < 0; j++) {	1,310✔
50	if (non_numerical_bytes[EBPF_TOTAL_STACK_SIZE + j]) {	1,310✔
51	break;	77✔
52	}
53	}
54	if (j > i + 1) {	154✔
55	value += "..." + std::to_string(EBPF_TOTAL_STACK_SIZE + j - 1);	222✔
56	}
57	value += "].type=number";	154✔
58	result.insert(value);	154✔
59	i = j;	154✔
60	}	154✔
61	return string_invariant{result};	154✔
62	}	154✔

vbpf / ebpf-verifier / 13958948275

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