27778108035

Committed 07 Jun 2026 06:51PM UTC coverage: 86.386% (-2.5%) from 88.93%

Build # 27778108035

Build Type

push

github

Committed by

elazarg

Commit Message

Release v0.2.5

Bump project version to 0.2.5 and add a CHANGELOG entry covering ELF loader hardening, numeric-domain soundness fixes, and the writable helper output initialization documentation update since v0.2.4. Also updates the using_installed_package example version requirement.

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

Coverage Stats

9125 of 10563 relevant lines covered (86.39%)

6334294.72 hits per line

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

84.21

/src/string_constraints.hpp

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

#pragma once

#include <optional>
#include <set>
#include <string>
#include <vector>

#include "arith/linear_constraint.hpp"
#include "arith/variable.hpp"
#include "crab/interval.hpp"
#include "crab/type_encoding.hpp"
#include "crab_utils/debug.hpp"

namespace prevail {
struct StringInvariant {
    std::optional<std::set<std::string>> maybe_inv{};

    StringInvariant() = default;

    explicit StringInvariant(std::set<std::string> inv) : maybe_inv(std::move(inv)) {}

    StringInvariant(const StringInvariant& inv) = default;
    StringInvariant& operator=(const StringInvariant& inv) = default;
    StringInvariant(StringInvariant&& inv) = default;
    StringInvariant& operator=(StringInvariant&& inv) = default;

    [[nodiscard]]
    bool is_bottom() const {
        return !maybe_inv;
    }
    [[nodiscard]]
    bool empty() const {
        return maybe_inv && maybe_inv->empty();
    }

    static StringInvariant top() { return StringInvariant{{}}; }
    static StringInvariant bottom() { return StringInvariant{}; }

    [[nodiscard]]
    const std::set<std::string>& value() const {
        if (is_bottom()) {
            CRAB_ERROR("cannot iterate bottom");
        }
        return *maybe_inv;
    }

    StringInvariant operator-(const StringInvariant& b) const;
    StringInvariant operator+(const StringInvariant& b) const;

    bool operator==(const StringInvariant& other) const { return maybe_inv == other.maybe_inv; }

    [[nodiscard]]
    bool contains(const std::string& item) const {
        return value().contains(item);
    }

    friend std::ostream& operator<<(std::ostream&, const StringInvariant& inv);
};

struct TypeSetRestriction {
    Variable var;
    TypeSet types;
};

/// Parsed type equality: v1.type == v2.type.
struct TypeEquality {
    Variable v1;
    Variable v2;
};

/// All constraint kinds produced by parsing a `StringInvariant`. Consumed as a
/// single bundle by `EbpfDomain::from_constraints`. `numeric_ranges` carries
/// stack byte ranges that should be marked numeric in `ArrayDomain::num_bytes`
/// — distinct sub-domain from the other three, but always parsed and applied
/// alongside them.
struct ParsedConstraints {
    std::vector<TypeEquality> type_equalities;
    std::vector<TypeSetRestriction> type_restrictions;
    std::vector<LinearConstraint> value_csts;
    std::vector<Interval> numeric_ranges;
};
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3
4	#pragma once
5
6	#include <optional>
7	#include <set>
8	#include <string>
9	#include <vector>
10
11	#include "arith/linear_constraint.hpp"
12	#include "arith/variable.hpp"
13	#include "crab/interval.hpp"
14	#include "crab/type_encoding.hpp"
15	#include "crab_utils/debug.hpp"
16
17	namespace prevail {
18	struct StringInvariant {	4,139✔
19	std::optional<std::set<std::string>> maybe_inv{};
20
21	StringInvariant() = default;	954✔
22
23	explicit StringInvariant(std::set<std::string> inv) : maybe_inv(std::move(inv)) {}	7,715✔
24
25	StringInvariant(const StringInvariant& inv) = default;	4,693✔
26	StringInvariant& operator=(const StringInvariant& inv) = default;
27	StringInvariant(StringInvariant&& inv) = default;	5,803✔
28	StringInvariant& operator=(StringInvariant&& inv) = default;	94✔
29
30	[[nodiscard]]
31	bool is_bottom() const {	15,228✔
32	return !maybe_inv;	9,746✔
33	}
34	[[nodiscard]]
35	bool empty() const {	×
36	return maybe_inv && maybe_inv->empty();	×
37	}
38
39	static StringInvariant top() { return StringInvariant{{}}; }	1,546✔
40	static StringInvariant bottom() { return StringInvariant{}; }	458✔
41
42	[[nodiscard]]
43	const std::set<std::string>& value() const {	8,840✔
44	if (is_bottom()) {	8,840✔
45	CRAB_ERROR("cannot iterate bottom");	×
46	}
47	return *maybe_inv;	8,840✔
48	}
49
50	StringInvariant operator-(const StringInvariant& b) const;
51	StringInvariant operator+(const StringInvariant& b) const;
52
53	bool operator==(const StringInvariant& other) const { return maybe_inv == other.maybe_inv; }	2,235✔
54
55	[[nodiscard]]
56	bool contains(const std::string& item) const {	4,596✔
57	return value().contains(item);	4,596✔
58	}
59
60	friend std::ostream& operator<<(std::ostream&, const StringInvariant& inv);
61	};
62
63	struct TypeSetRestriction {
64	Variable var;
65	TypeSet types;
66	};
67
68	/// Parsed type equality: v1.type == v2.type.
69	struct TypeEquality {
70	Variable v1;
71	Variable v2;
72	};
73
74	/// All constraint kinds produced by parsing a `StringInvariant`. Consumed as a
75	/// single bundle by `EbpfDomain::from_constraints`. `numeric_ranges` carries
76	/// stack byte ranges that should be marked numeric in `ArrayDomain::num_bytes`
77	/// — distinct sub-domain from the other three, but always parsed and applied
78	/// alongside them.
79	struct ParsedConstraints {
80	std::vector<TypeEquality> type_equalities;
81	std::vector<TypeSetRestriction> type_restrictions;
82	std::vector<LinearConstraint> value_csts;
83	std::vector<Interval> numeric_ranges;
84	};
85	} // namespace prevail

Alan-Jowett / ebpf-verifier / 27778108035

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