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

93.94

/src/crab_utils/num_extended.hpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: Apache-2.0

#pragma once

#include <optional>
#include <utility>

#include "crab_utils/num_big.hpp"
#include "crab_utils/stats.hpp"

namespace crab {

class extended_number final {
    bool _is_infinite;
    number_t _n;

    extended_number(const bool is_infinite, const number_t& n) : _is_infinite(is_infinite), _n(n) {
        if (is_infinite) {
            if (n > 0) {
                _n = 1;
            } else {
                _n = -1;
            }
        }
    }

  public:
    static extended_number plus_infinity() { return extended_number(true, 1); }

    static extended_number minus_infinity() { return extended_number(true, -1); }

    explicit extended_number(const std::string& s) : _n(1) {
        if (s == "+oo") {
            _is_infinite = true;
        } else if (s == "-oo") {
            _is_infinite = true;
            _n = -1;
        } else {
            _is_infinite = false;
            _n = number_t(s);
        }
    }

    extended_number(number_t n) : _is_infinite(false), _n(std::move(n)) {}
    extended_number(std::integral auto n) : _is_infinite(false), _n{n} {}

    extended_number(const extended_number& o) = default;

    extended_number(extended_number&&) noexcept = default;

    template <std::integral T>
    T narrow() const {
        if (_is_infinite) {
            CRAB_ERROR("Bound: cannot narrow infinite value");
        }
        return _n.narrow<T>();
    }

    template <is_enum T>
    T narrow() const {
        return static_cast<T>(narrow<std::underlying_type_t<T>>());
    }

    extended_number& operator=(extended_number&&) noexcept = default;

    extended_number& operator=(const extended_number& o) {
        if (this != &o) {
            _is_infinite = o._is_infinite;
            _n = o._n;
        }
        return *this;
    }

    [[nodiscard]]
    bool is_infinite() const {
        return _is_infinite;
    }

    [[nodiscard]]
    bool is_finite() const {
        return !_is_infinite;
    }

    [[nodiscard]]
    bool is_plus_infinity() const {
        return (is_infinite() && _n > 0);
    }

    [[nodiscard]]
    bool is_minus_infinity() const {
        return (is_infinite() && _n < 0);
    }

    extended_number operator-() const { return extended_number(_is_infinite, -_n); }

    extended_number operator+(const extended_number& x) const {
        if (is_finite()) {
            if (x.is_finite()) {
                return extended_number(_n + x._n);
            }
            return x;
        }
        if (x.is_finite() || x._n == _n) {
            return *this;
        }
        CRAB_ERROR("Bound: undefined operation -oo + +oo");
    }

    extended_number& operator+=(const extended_number& x) { return operator=(operator+(x)); }

    extended_number operator-(const extended_number& x) const { return operator+(x.operator-()); }

    extended_number& operator-=(const extended_number& x) { return operator=(operator-(x)); }

    extended_number operator*(const extended_number& x) const {
        if (x._n == 0) {
            return x;
        } else if (_n == 0) {
            return *this;
        } else {
            return extended_number(_is_infinite || x._is_infinite, _n * x._n);
        }
    }

    extended_number& operator*=(const extended_number& x) { return operator=(operator*(x)); }

  private:
    extended_number AbsDiv(const extended_number& x, extended_number (*f)(number_t, number_t)) const {
        if (x._n == 0) {
            CRAB_ERROR("Bound: division by zero");
        }
        if (x.is_infinite()) {
            if (is_infinite()) {
                CRAB_ERROR("Bound: inf / inf");
            }
            return number_t{0};
        }
        if (is_infinite()) {
            return *this;
        }
        return f(_n, x._n);
    }

  public:
    extended_number operator/(const extended_number& x) const {
        return AbsDiv(x, [](number_t dividend, number_t divisor) { return extended_number{dividend / divisor}; });
    }

    extended_number operator%(const extended_number& x) const {
        return AbsDiv(x, [](number_t dividend, number_t divisor) { return extended_number{dividend % divisor}; });
    }

    [[nodiscard]]
    extended_number udiv(const extended_number& x) const {
        using M = uint64_t;
        return AbsDiv(x, [](number_t dividend, number_t divisor) {
            dividend = dividend >= 0 ? dividend : number_t{dividend.cast_to<M>()};
            divisor = divisor >= 0 ? divisor : number_t{divisor.cast_to<M>()};
            return extended_number{dividend / divisor};
        });
    }

    [[nodiscard]]
    extended_number urem(const extended_number& x) const {
        using M = uint64_t;
        return AbsDiv(x, [](number_t dividend, number_t divisor) {
            dividend = dividend >= 0 ? dividend : number_t{dividend.cast_to<M>()};
            divisor = divisor >= 0 ? divisor : number_t{divisor.cast_to<M>()};
            return extended_number{dividend % divisor};
        });
    }

    extended_number& operator/=(const extended_number& x) { return operator=(operator/(x)); }

    bool operator<(const extended_number& x) const { return !operator>=(x); }

    bool operator>(const extended_number& x) const { return !operator<=(x); }

    bool operator==(const extended_number& x) const { return (_is_infinite == x._is_infinite && _n == x._n); }

    bool operator!=(const extended_number& x) const { return !operator==(x); }

    [[nodiscard]]
    number_t sign_extend(const int width) const {
        if (is_infinite()) {
            CRAB_ERROR("Bound: infinity cannot be sign_extended");
        }
        return _n.sign_extend(width);
    }

    [[nodiscard]]
    number_t zero_extend(const int width) const {
        if (is_infinite()) {
            CRAB_ERROR("Bound: infinity cannot be zero_extended");
        }
        return _n.zero_extend(width);
    }

    /*        operator<= and operator>= use a somewhat optimized implementation.
     *        results include up to 20% improvements in performance in the octagon domain
     *        over a more naive implementation.
     */
    bool operator<=(const extended_number& x) const {
        if (_is_infinite xor x._is_infinite) {
            if (_is_infinite) {
                return _n < 0;
            }
            return x._n > 0;
        }
        return _n <= x._n;
    }

    bool operator>=(const extended_number& x) const {
        if (_is_infinite xor x._is_infinite) {
            if (_is_infinite) {
                return _n > 0;
            }
            return x._n < 0;
        }
        return _n >= x._n;
    }

    [[nodiscard]]
    extended_number abs() const {
        if (operator>=(number_t{0})) {
            return *this;
        } else {
            return operator-();
        }
    }

    [[nodiscard]]
    std::optional<number_t> number() const {
        if (is_infinite()) {
            return {};
        } else {
            return {_n};
        }
    }

    friend std::ostream& operator<<(std::ostream& o, const extended_number& b) {
        if (b.is_plus_infinity()) {
            o << "+oo";
        } else if (b.is_minus_infinity()) {
            o << "-oo";
        } else {
            o << b._n;
        }
        return o;
    }

}; // class extended_number

} // namespace crab

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: Apache-2.0
3
4	#pragma once
5
6	#include <optional>
7	#include <utility>
8
9	#include "crab_utils/num_big.hpp"
10	#include "crab_utils/stats.hpp"
11
12	namespace crab {
13
14	class extended_number final {	194,966,417✔
15	bool _is_infinite;
16	number_t _n;
17
18	extended_number(const bool is_infinite, const number_t& n) : _is_infinite(is_infinite), _n(n) {	174,933,806✔
19	if (is_infinite) {	174,933,806✔
20	if (n > 0) {	126,610,436✔
21	_n = 1;	63,339,449✔
22	} else {
23	_n = -1;	63,270,987✔
24	}
25	}
26	}	174,933,806✔
27
28	public:
29	static extended_number plus_infinity() { return extended_number(true, 1); }	48,052,375✔
30
31	static extended_number minus_infinity() { return extended_number(true, -1); }	48,052,330✔
32
33	explicit extended_number(const std::string& s) : _n(1) {
34	if (s == "+oo") {
35	_is_infinite = true;
36	} else if (s == "-oo") {
37	_is_infinite = true;
38	_n = -1;
39	} else {
40	_is_infinite = false;
41	_n = number_t(s);
42	}
43	}
44
45	extended_number(number_t n) : _is_infinite(false), _n(std::move(n)) {}	199,139,419✔
46	extended_number(std::integral auto n) : _is_infinite(false), _n{n} {}	2,803,472✔
47
48	extended_number(const extended_number& o) = default;	255,911,989✔
49
50	extended_number(extended_number&&) noexcept = default;
51
52	template <std::integral T>
53	T narrow() const {	266,992✔
54	if (_is_infinite) {	266,992✔
55	CRAB_ERROR("Bound: cannot narrow infinite value");	×
56	}
57	return _n.narrow<T>();	266,992✔
58	}
59
60	template <is_enum T>
61	T narrow() const {
62	return static_cast<T>(narrow<std::underlying_type_t<T>>());
63	}
64
65	extended_number& operator=(extended_number&&) noexcept = default;	27,018,921✔
66
67	extended_number& operator=(const extended_number& o) {	56,764,272✔
68	if (this != &o) {	56,764,272✔
69	_is_infinite = o._is_infinite;	56,764,272✔
70	_n = o._n;	56,764,272✔
71	}
72	return *this;	42,573,202✔
73	}
74
75	[[nodiscard]]
76	bool is_infinite() const {	13,680,503✔
77	return _is_infinite;	10,816,916✔
78	}
79
80	[[nodiscard]]
81	bool is_finite() const {	118,788,906✔
82	return !_is_infinite;	118,788,906✔
83	}
84
85	[[nodiscard]]
86	bool is_plus_infinity() const {	4,104✔
87	return (is_infinite() && _n > 0);	4,122✔
88	}
89
90	[[nodiscard]]
91	bool is_minus_infinity() const {	4,072✔
92	return (is_infinite() && _n < 0);	4,074✔
93	}
94
95	extended_number operator-() const { return extended_number(_is_infinite, -_n); }	1,612,071✔
96
97	extended_number operator+(const extended_number& x) const {	58,148,510✔
98	if (is_finite()) {	58,148,510✔
99	if (x.is_finite()) {	58,015,888✔
100	return extended_number(_n + x._n);	40,175,426✔
101	}
102	return x;	31,232,270✔
103	}
104	if (x.is_finite() \|\| x._n == _n) {	132,622✔
105	return *this;	132,622✔
106	}
107	CRAB_ERROR("Bound: undefined operation -oo + +oo");	×
108	}
109
110	extended_number& operator+=(const extended_number& x) { return operator=(operator+(x)); }
111
112	extended_number operator-(const extended_number& x) const { return operator+(x.operator-()); }	1,612,056✔
113
114	extended_number& operator-=(const extended_number& x) { return operator=(operator-(x)); }
115
116	extended_number operator*(const extended_number& x) const {	112,018,464✔
117	if (x._n == 0) {	112,018,464✔
118	return x;	2,229,080✔
119	} else if (_n == 0) {	109,789,384✔
120	return *this;	92✔
121	} else {
122	return extended_number(_is_infinite \|\| x._is_infinite, _n * x._n);	164,683,946✔
123	}
124	}
125
126	extended_number& operator=(const extended_number& x) { return operator=(operator(x)); }
127
128	private:
129	extended_number AbsDiv(const extended_number& x, extended_number (*f)(number_t, number_t)) const {	6,636✔
130	if (x._n == 0) {	6,636✔
131	CRAB_ERROR("Bound: division by zero");	×
132	}
133	if (x.is_infinite()) {	6,636✔
134	if (is_infinite()) {	64✔
135	CRAB_ERROR("Bound: inf / inf");	×
136	}
137	return number_t{0};	64✔
138	}
139	if (is_infinite()) {	6,572✔
140	return *this;	582✔
141	}
142	return f(_n, x._n);	8,985✔
143	}
144
145	public:
146	extended_number operator/(const extended_number& x) const {	1,912✔
147	return AbsDiv(x, [](number_t dividend, number_t divisor) { return extended_number{dividend / divisor}; });	5,043✔
148	}
149
150	extended_number operator%(const extended_number& x) const {
151	return AbsDiv(x, [](number_t dividend, number_t divisor) { return extended_number{dividend % divisor}; });
152	}
153
154	[[nodiscard]]
155	extended_number udiv(const extended_number& x) const {	4,681✔
156	using M = uint64_t;	2,362✔
157	return AbsDiv(x, [](number_t dividend, number_t divisor) {	6,985✔
158	dividend = dividend >= 0 ? dividend : number_t{dividend.cast_to<M>()};	6,783✔
159	divisor = divisor >= 0 ? divisor : number_t{divisor.cast_to<M>()};	6,783✔
160	return extended_number{dividend / divisor};	6,783✔
161	});	6,957✔
162	}
163
164	[[nodiscard]]
165	extended_number urem(const extended_number& x) const {
166	using M = uint64_t;
167	return AbsDiv(x, [](number_t dividend, number_t divisor) {
168	dividend = dividend >= 0 ? dividend : number_t{dividend.cast_to<M>()};
169	divisor = divisor >= 0 ? divisor : number_t{divisor.cast_to<M>()};
170	return extended_number{dividend % divisor};
171	});
172	}
173
174	extended_number& operator/=(const extended_number& x) { return operator=(operator/(x)); }
175
176	bool operator<(const extended_number& x) const { return !operator>=(x); }	114,069,004✔
177
178	bool operator>(const extended_number& x) const { return !operator<=(x); }	328,092,917✔
179
180	bool operator==(const extended_number& x) const { return (_is_infinite == x._is_infinite && _n == x._n); }	3,713,072✔
181
182	bool operator!=(const extended_number& x) const { return !operator==(x); }
183
184	[[nodiscard]]
185	number_t sign_extend(const int width) const {	97,828✔
186	if (is_infinite()) {	97,828✔
NEW 187	CRAB_ERROR("Bound: infinity cannot be sign_extended");	×
188	}
189	return _n.sign_extend(width);	97,828✔
190	}
191
192	[[nodiscard]]
193	number_t zero_extend(const int width) const {	186,204✔
194	if (is_infinite()) {	186,204✔
NEW 195	CRAB_ERROR("Bound: infinity cannot be zero_extended");	×
196	}
197	return _n.zero_extend(width);	186,204✔
198	}
199
200	/* operator<= and operator>= use a somewhat optimized implementation.
201	* results include up to 20% improvements in performance in the octagon domain
202	* over a more naive implementation.
203	*/
204	bool operator<=(const extended_number& x) const {	372,922,429✔
205	if (_is_infinite xor x._is_infinite) {	372,922,429✔
206	if (_is_infinite) {	24,917,671✔
207	return _n < 0;	12,445,318✔
208	}
209	return x._n > 0;	12,472,353✔
210	}
211	return _n <= x._n;	348,004,758✔
212	}
213
214	bool operator>=(const extended_number& x) const {	114,470,358✔
215	if (_is_infinite xor x._is_infinite) {	114,470,358✔
216	if (_is_infinite) {	67,688✔
217	return _n > 0;	65,488✔
218	}
219	return x._n < 0;	2,200✔
220	}
221	return _n >= x._n;	114,402,670✔
222	}
223
224	[[nodiscard]]
225	extended_number abs() const {
226	if (operator>=(number_t{0})) {
227	return *this;
228	} else {
229	return operator-();
230	}
231	}
232
233	[[nodiscard]]
234	std::optional<number_t> number() const {	6,562,157✔
235	if (is_infinite()) {	6,186,060✔
236	return {};	1,658,078✔
237	} else {
238	return {_n};	4,904,079✔
239	}
240	}
241
242	friend std::ostream& operator<<(std::ostream& o, const extended_number& b) {	4,104✔
243	if (b.is_plus_infinity()) {	4,104✔
244	o << "+oo";	32✔
245	} else if (b.is_minus_infinity()) {	4,072✔
246	o << "-oo";	4✔
247	} else {
248	o << b._n;	4,068✔
249	}
250	return o;	4,104✔
251	}
252
253	}; // class extended_number
254
255	} // 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