13955273819

Committed 19 Mar 2025 07:38PM UTC coverage: 88.66% (+0.5%) from 88.134%

Build # 13955273819

Build Type

push

github

Committed by

web-flow

Commit Message

Fix sign extension (#850)

* fix sign extension
* add exhaustive tests for sign extension of <=3 bits
* fix interval::size()
* streamline bit/width operations

---------
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

203 of 214 new or added lines in 9 files covered. (94.86%)

9 existing lines in 5 files now uncovered.

8639 of 9744 relevant lines covered (88.66%)

8977818.22 hits per line

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

84.96

/src/crab/add_bottom.hpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#pragma once

#include <optional>

#include "crab/split_dbm.hpp"
#include "string_constraints.hpp"

namespace crab {

namespace domains {

class AddBottom final {
    using T = SplitDBM;
    std::optional<T> dom{};
    AddBottom() {}

  public:
    explicit AddBottom(auto&& _dom) : dom{std::forward<decltype(_dom)>(_dom)} {}
    AddBottom(const AddBottom& other) = default;
    AddBottom(AddBottom& other) = default;
    AddBottom(AddBottom&& other) = default;

    AddBottom& operator=(const AddBottom& o) = default;
    AddBottom& operator=(AddBottom&& o) = default;

    void set_to_top() {
        if (dom) {
            dom->set_to_top();
        } else {
            dom = T::top();
        }
    }

    void set_to_bottom() { dom = {}; }

    [[nodiscard]]
    bool is_bottom() const {
        return !dom;
    }

    static AddBottom top() { return AddBottom(T::top()); }

    static AddBottom bottom() { return AddBottom(); }

    [[nodiscard]]
    bool is_top() const {
        return dom && dom->is_top();
    }

    bool operator<=(const AddBottom& o) const {
        if (!dom) {
            return true;
        }
        if (!o.dom) {
            return false;
        }
        return *dom <= *o.dom;
    }

    void operator|=(const AddBottom& o) {
        if (!o.dom) {
            return;
        }
        if (!dom) {
            dom = *o.dom;
            return;
        }
        (*dom) |= *o.dom;
    }

    void operator|=(AddBottom&& o) {
        if (!o.dom) {
            return;
        }
        if (!dom) {
            dom = std::move(o.dom);
            return;
        }
        *dom |= std::move(*o.dom);
    }

    template <typename Left, typename Right>
    friend AddBottom operator|(Left&& left, Right&& right) {
        using LDOM = decltype(*std::forward<Left>(left).dom);
        using RDOM = decltype(*std::forward<Right>(right).dom);
        if (!left.dom) {
            return std::forward<Right>(right);
        }
        if (!right.dom) {
            return std::forward<Left>(left);
        }
        return AddBottom(std::forward<LDOM>(*left.dom) | std::forward<RDOM>(*right.dom));
    }

    [[nodiscard]]
    AddBottom widen(const AddBottom& o) const {
        if (!dom) {
            return o;
        }
        if (!o.dom) {
            return *this;
        }
        return AddBottom(dom->widen(*o.dom));
    }

    AddBottom operator&(const AddBottom& o) const {
        if (!dom || !o.dom) {
            return bottom();
        }
        if (auto res = (*dom).meet(*o.dom)) {
            return AddBottom(*res);
        }
        return bottom();
    }

    [[nodiscard]]
    AddBottom narrow(const AddBottom& o) const {
        if (!dom || !o.dom) {
            return bottom();
        }
        return AddBottom(dom->narrow(*o.dom));
    }

    [[nodiscard]]
    AddBottom when(const linear_constraint_t& cst) const {
        if (dom) {
            AddBottom result(*dom);
            if (!result.dom->add_constraint(cst)) {
                result.dom = {};
            }
            return result;
        }
        return bottom();
    }

    void operator-=(variable_t v) {
        if (dom) {
            (*dom) -= v;
        }
    }

    void assign(std::optional<variable_t> x, const linear_expression_t& e) {
        if (x) {
            assign(*x, e);
        }
    }

    template <typename V>
    void assign(variable_t x, const V& value) {
        if (dom) {
            // XXX: maybe needs to return false when becomes bottom
            // is this possible?
            dom->assign(x, value);
        }
    };

    template <typename Op, typename Left, typename Right>
    void apply(Op op, variable_t x, const Left& left, const Right& right, int finite_width) {
        if (dom) {
            dom->apply(op, x, left, right, finite_width);
        }
    }

    void operator+=(const linear_constraint_t& cst) {
        if (dom) {
            if (!dom->add_constraint(cst)) {
                dom = {};
            }
        }
    }

    [[nodiscard]]
    interval_t eval_interval(const linear_expression_t& e) const {
        if (dom) {
            return dom->eval_interval(e);
        }
        return interval_t::bottom();
    }

    interval_t operator[](variable_t x) const {
        if (dom) {
            return (*dom)[x];
        }
        return interval_t::bottom();
    }

    void set(variable_t x, const interval_t& intv) {
        if (intv.is_bottom()) {
            dom = {};
        } else if (dom) {
            dom->set(x, intv);
        }
    }

    // Return true if inv intersects with cst.
    [[nodiscard]]
    bool intersect(const linear_constraint_t& cst) const {
        if (dom) {
            return dom->intersect(cst);
        }
        return false;
    }

    // Return true if entails rhs.
    [[nodiscard]]
    bool entail(const linear_constraint_t& cst) const {
        if (dom) {
            return dom->entail(cst);
        }
        return true;
    }

    friend std::ostream& operator<<(std::ostream& o, const AddBottom& dom) {
        if (dom.dom) {
            return o << *dom.dom;
        }
        return o << "_|_";
    }

    [[nodiscard]]
    string_invariant to_set() const {
        if (dom) {
            return dom->to_set();
        }
        return string_invariant::bottom();
    }
}; // class AddBottom

} // namespace domains
} // namespace crab

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#pragma once
4
5	#include <optional>
6
7	#include "crab/split_dbm.hpp"
8	#include "string_constraints.hpp"
9
10	namespace crab {
11
12	namespace domains {
13
14	class AddBottom final {	1,097,894✔
15	using T = SplitDBM;
16	std::optional<T> dom{};
17	AddBottom() {}	118,596✔
18
19	public:
20	explicit AddBottom(auto&& _dom) : dom{std::forward<decltype(_dom)>(_dom)} {}	1,021,226✔
21	AddBottom(const AddBottom& other) = default;	533,223✔
22	AddBottom(AddBottom& other) = default;	×
23	AddBottom(AddBottom&& other) = default;	794,625✔
24
25	AddBottom& operator=(const AddBottom& o) = default;	166,946✔
26	AddBottom& operator=(AddBottom&& o) = default;	449,482✔
27
28	void set_to_top() {	60✔
29	if (dom) {	60✔
30	dom->set_to_top();	60✔
31	} else {
32	dom = T::top();	×
33	}
34	}	60✔
35
36	void set_to_bottom() { dom = {}; }	1,011,328✔
37
38	[[nodiscard]]
39	bool is_bottom() const {	1,689,812✔
40	return !dom;	1,188,803✔
41	}
42
43	static AddBottom top() { return AddBottom(T::top()); }	1,522,020✔
44
45	static AddBottom bottom() { return AddBottom(); }	118,596✔
46
47	[[nodiscard]]
48	bool is_top() const {	×
49	return dom && dom->is_top();	×
50	}
51
52	bool operator<=(const AddBottom& o) const {	198✔
53	if (!dom) {	198✔
54	return true;
55	}
56	if (!o.dom) {	198✔
57	return false;
58	}
59	return dom <= o.dom;	198✔
60	}
61
62	void operator\|=(const AddBottom& o) {
63	if (!o.dom) {
64	return;
65	}
66	if (!dom) {
67	dom = *o.dom;
68	return;
69	}
70	(dom) \|= o.dom;
71	}
72
73	void operator\|=(AddBottom&& o) {	141,532✔
74	if (!o.dom) {	141,532✔
75	return;	241✔
76	}
77	if (!dom) {	141,050✔
78	dom = std::move(o.dom);	118,118✔
79	return;	118,118✔
80	}
81	dom \|= std::move(o.dom);	22,932✔
82	}
83
84	template <typename Left, typename Right>
85	friend AddBottom operator\|(Left&& left, Right&& right) {	38✔
86	using LDOM = decltype(*std::forward<Left>(left).dom);
87	using RDOM = decltype(*std::forward<Right>(right).dom);
88	if (!left.dom) {	38✔
89	return std::forward<Right>(right);	×
90	}
91	if (!right.dom) {	38✔
92	return std::forward<Left>(left);	×
93	}
94	return AddBottom(std::forward<LDOM>(left.dom) \| std::forward<RDOM>(right.dom));	57✔
95	}
96
97	[[nodiscard]]
98	AddBottom widen(const AddBottom& o) const {	84✔
99	if (!dom) {	84✔
100	return o;	×
101	}
102	if (!o.dom) {	84✔
103	return *this;	×
104	}
105	return AddBottom(dom->widen(*o.dom));	126✔
106	}
107
108	AddBottom operator&(const AddBottom& o) const {	38✔
109	if (!dom \|\| !o.dom) {	38✔
110	return bottom();	×
111	}
112	if (auto res = (dom).meet(o.dom)) {	38✔
113	return AddBottom(*res);	38✔
114	}	38✔
115	return bottom();	×
116	}
117
118	[[nodiscard]]
119	AddBottom narrow(const AddBottom& o) const {	×
120	if (!dom \|\| !o.dom) {	×
121	return bottom();	×
122	}
123	return AddBottom(dom->narrow(*o.dom));	×
124	}
125
126	[[nodiscard]]
127	AddBottom when(const linear_constraint_t& cst) const {	6,386✔
128	if (dom) {	6,386✔
129	AddBottom result(*dom);	6,386✔
130	if (!result.dom->add_constraint(cst)) {	6,386✔
131	result.dom = {};	5,152✔
132	}
133	return result;	6,386✔
134	}	6,386✔
135	return bottom();	×
136	}	2,576✔
137
138	void operator-=(variable_t v) {	3,237,085✔
139	if (dom) {	3,237,085✔
140	(*dom) -= v;	3,237,037✔
141	}
142	}	3,237,085✔
143
144	void assign(std::optional<variable_t> x, const linear_expression_t& e) {	95,356✔
145	if (x) {	95,356✔
146	assign(*x, e);	143,031✔
147	}
148	}	95,356✔
149
150	template <typename V>
151	void assign(variable_t x, const V& value) {	627,742✔
152	if (dom) {	627,742✔
153	// XXX: maybe needs to return false when becomes bottom
154	// is this possible?
155	dom->assign(x, value);	627,718✔
156	}
157	};	313,872✔
158
159	template <typename Op, typename Left, typename Right>
160	void apply(Op op, variable_t x, const Left& left, const Right& right, int finite_width) {	134,388✔
161	if (dom) {	134,388✔
162	dom->apply(op, x, left, right, finite_width);	134,364✔
163	}
164	}	134,388✔
165
166	void operator+=(const linear_constraint_t& cst) {	225,312✔
167	if (dom) {	225,312✔
168	if (!dom->add_constraint(cst)) {	225,120✔
169	dom = {};	1,096✔
170	}
171	}
172	}	225,312✔
173
174	[[nodiscard]]
175	interval_t eval_interval(const linear_expression_t& e) const {	28,119,422✔
176	if (dom) {	28,119,422✔
177	return dom->eval_interval(e);	28,119,246✔
178	}
179	return interval_t::bottom();	176✔
180	}
181
182	interval_t operator[](variable_t x) const {	364,892✔
183	if (dom) {	364,892✔
184	return (*dom)[x];	364,844✔
185	}
186	return interval_t::bottom();	48✔
187	}
188
189	void set(variable_t x, const interval_t& intv) {	658,510✔
190	if (intv.is_bottom()) {	658,510✔
UNCOV 191	dom = {};	×
192	} else if (dom) {	658,510✔
193	dom->set(x, intv);	658,510✔
194	}
195	}	658,510✔
196
197	// Return true if inv intersects with cst.
198	[[nodiscard]]
199	bool intersect(const linear_constraint_t& cst) const {	1,724,030✔
200	if (dom) {	1,724,030✔
201	return dom->intersect(cst);	1,724,030✔
202	}
203	return false;
204	}
205
206	// Return true if entails rhs.
207	[[nodiscard]]
208	bool entail(const linear_constraint_t& cst) const {	209,070✔
209	if (dom) {	209,070✔
210	return dom->entail(cst);	200,766✔
211	}
212	return true;	4,152✔
213	}
214
215	friend std::ostream& operator<<(std::ostream& o, const AddBottom& dom) {	16✔
216	if (dom.dom) {	16✔
217	return o << *dom.dom;	16✔
218	}
219	return o << "_\|_";	×
220	}
221
222	[[nodiscard]]
223	string_invariant to_set() const {	1,386✔
224	if (dom) {	1,386✔
225	return dom->to_set();	1,188✔
226	}
227	return string_invariant::bottom();	198✔
228	}
229	}; // class AddBottom
230
231	} // namespace domains
232	} // namespace crab

vbpf / ebpf-verifier / 13955273819

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