18658728485

Committed 18 Oct 2025 05:56PM UTC coverage: 88.47% (+0.4%) from 88.11%

Build # 18658728485

Build Type

push

github

Committed by

elazarg

Commit Message

Bump external/bpf_conformance from `8f3c2fe` to `6fa6a20`

Bumps [external/bpf_conformance](https://github.com/Alan-Jowett/bpf_conformance) from `8f3c2fe` to `6fa6a20`.
- [Release notes](https://github.com/Alan-Jowett/bpf_conformance/releases)
- [Commits](https://github.com/Alan-Jowett/bpf_conformance/compare/8f3c2fe88...<a class=hub.com/Alan-Jowett/ebpf-verifier/commit/6fa6a20ac6fd3612ea9338312a67408687b9f06b">6fa6a20ac)

---
updated-dependencies:
- dependency-name: external/bpf_conformance
  dependency-version: 6fa6a20ac6fd3612ea9338312a67408687b9f06b
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>

Run Details

8954 of 10121 relevant lines covered (88.47%)

18293099.16 hits per line

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

96.74

/src/assertions.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <cassert>
#include <cinttypes>
#include <utility>
#include <vector>

#include "asm_syntax.hpp"
#include "cfg/cfg.hpp"
#include "platform.hpp"

using std::string;
using std::to_string;
using std::vector;

namespace prevail {
class AssertExtractor {
    ProgramInfo info;
    std::optional<Label> current_label; ///< Pre-simplification label this assert is part of.

    static Imm imm(const Value& v) { return std::get<Imm>(v); }

    static vector<Assertion> zero_offset_ctx(const Reg reg) {
        vector<Assertion> res;
        res.emplace_back(TypeConstraint{reg, TypeGroup::ctx});
        res.emplace_back(ZeroCtxOffset{reg});
        return res;
    }

    [[nodiscard]]
    ValidAccess make_valid_access(const Reg reg, const int32_t offset = {}, const Value& width = Imm{0},
                                  const bool or_null = {}, const AccessType access_type = {}) const {
        const int depth = current_label.has_value() ? current_label.value().call_stack_depth() : 1;
        return ValidAccess{depth, reg, offset, width, or_null, access_type};
    }

  public:
    explicit AssertExtractor(ProgramInfo info, std::optional<Label> label)
        : info{std::move(info)}, current_label(std::move(label)) {}

    vector<Assertion> operator()(const Undefined&) const {
        // assert(false);
        return {};
    }

    vector<Assertion> operator()(const IncrementLoopCounter& ipc) const { return {{BoundedLoopCount{ipc.name}}}; }

    vector<Assertion> operator()(const LoadMapFd&) const { return {}; }
    vector<Assertion> operator()(const LoadMapAddress&) const { return {}; }

    /// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.
    vector<Assertion> operator()(const Packet&) const { return zero_offset_ctx({6}); }

    vector<Assertion> operator()(const Exit&) const {
        vector<Assertion> res;
        if (current_label->stack_frame_prefix.empty()) {
            // Verify that Exit returns a number.
            res.emplace_back(TypeConstraint{Reg{R0_RETURN_VALUE}, TypeGroup::number});
        }
        return res;
    }

    vector<Assertion> operator()(const Call& call) const {
        vector<Assertion> res;
        std::optional<Reg> map_fd_reg;
        res.emplace_back(ValidCall{call.func, call.stack_frame_prefix});
        for (ArgSingle arg : call.singles) {
            switch (arg.kind) {
            case ArgSingle::Kind::ANYTHING:
                // avoid pointer leakage:
                if (!info.type.is_privileged) {
                    res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});
                }
                break;
            case ArgSingle::Kind::MAP_FD_PROGRAMS:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd_programs});
                // Do not update map_fd_reg
                break;
            case ArgSingle::Kind::MAP_FD:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd});
                map_fd_reg = arg.reg;
                break;
            case ArgSingle::Kind::PTR_TO_MAP_KEY:
            case ArgSingle::Kind::PTR_TO_MAP_VALUE:
                assert(map_fd_reg);
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});
                res.emplace_back(ValidMapKeyValue{arg.reg, *map_fd_reg, arg.kind == ArgSingle::Kind::PTR_TO_MAP_KEY});
                break;
            case ArgSingle::Kind::PTR_TO_CTX:
                for (const Assertion& a : zero_offset_ctx(arg.reg)) {
                    res.emplace_back(a);
                }
                break;
            }
        }
        for (ArgPair arg : call.pairs) {
            const auto group = arg.or_null ? TypeGroup::mem_or_num : TypeGroup::mem;
            const auto access_type =
                arg.kind == ArgPair::Kind::PTR_TO_READABLE_MEM ? AccessType::read : AccessType::write;
            res.emplace_back(TypeConstraint{arg.size, TypeGroup::number});
            res.emplace_back(ValidSize{arg.size, arg.can_be_zero});
            res.emplace_back(TypeConstraint{arg.mem, group});
            res.emplace_back(make_valid_access(arg.mem, 0, arg.size, arg.or_null, access_type));
            // TODO: reg is constant (or maybe it's not important)
        }
        return res;
    }

    vector<Assertion> operator()(const CallLocal&) const { return {}; }

    vector<Assertion> operator()(const Callx& callx) const {
        vector<Assertion> res;
        res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});
        res.emplace_back(FuncConstraint{callx.func});
        return res;
    }

    [[nodiscard]]
    vector<Assertion> explicate(const Condition& cond) const {
        if (info.type.is_privileged) {
            return {};
        }
        vector<Assertion> res;
        if (const auto pimm = std::get_if<Imm>(&cond.right)) {
            if (pimm->v != 0) {
                // no need to check for valid access, it must be a number
                res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});
            } else {
                bool allow_pointers = false;

                switch (cond.op) {
                case Condition::Op::EQ: allow_pointers = true; break;
                case Condition::Op::NE: allow_pointers = true; break;
                case Condition::Op::SET: allow_pointers = true; break;
                case Condition::Op::NSET: allow_pointers = true; break;
                case Condition::Op::LT: allow_pointers = true; break;
                case Condition::Op::LE: allow_pointers = true; break;
                case Condition::Op::GT: allow_pointers = true; break;
                case Condition::Op::GE: allow_pointers = true; break;
                case Condition::Op::SLT: allow_pointers = false; break;
                case Condition::Op::SLE: allow_pointers = false; break;
                case Condition::Op::SGT: allow_pointers = false; break;
                case Condition::Op::SGE: allow_pointers = false; break;
                default: assert(!"unexpected condition");
                }

                // Only permit pointer comparisons if the operation is 64-bit.
                allow_pointers &= cond.is64;

                if (!allow_pointers) {
                    res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});
                }

                res.emplace_back(make_valid_access(cond.left));
                // OK - map_fd is just another pointer
                // Anything can be compared to 0
            }
        } else {
            const auto reg_right = get<Reg>(cond.right);
            res.emplace_back(make_valid_access(cond.left));
            res.emplace_back(make_valid_access(reg_right));
            if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {
                res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});
            }
            res.emplace_back(Comparable{.r1 = cond.left, .r2 = reg_right, .or_r2_is_number = false});
        }
        return res;
    }

    vector<Assertion> operator()(const Assume& ins) const {
        if (!ins.is_implicit) {
            return explicate(ins.cond);
        }
        return {};
    }

    vector<Assertion> operator()(const Jmp& ins) const {
        if (!ins.cond) {
            return {};
        }
        return explicate(*ins.cond);
    }

    vector<Assertion> operator()(const Mem& ins) const {
        vector<Assertion> res;
        const Reg basereg = ins.access.basereg;
        Imm width{gsl::narrow<uint32_t>(ins.access.width)};
        const int offset = ins.access.offset;
        if (basereg.v == R10_STACK_POINTER) {
            // We know we are accessing the stack.
            if (offset < -EBPF_SUBPROGRAM_STACK_SIZE || offset + static_cast<int>(width.v) > 0) {
                // This assertion will fail
                res.emplace_back(make_valid_access(basereg, offset, width, false,
                                                   ins.is_load ? AccessType::read : AccessType::write));
            } else if (ins.is_load) {
                // This assertion is not for bound checks but for reading initialized memory.
                // TODO: avoid load assertions: use post-assertion to check that the loaded value is initialized
                // res.emplace_back(make_valid_access(basereg, offset, width, false, AccessType::read));
            }
        } else {
            res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer});
            res.emplace_back(
                make_valid_access(basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write));
            if (!info.type.is_privileged && !ins.is_load) {
                if (const auto preg = std::get_if<Reg>(&ins.value)) {
                    if (width.v != 8) {
                        res.emplace_back(TypeConstraint{*preg, TypeGroup::number});
                    } else {
                        res.emplace_back(ValidStore{ins.access.basereg, *preg});
                    }
                }
            }
        }
        return res;
    }

    vector<Assertion> operator()(const Atomic& ins) const {

        return {
            Assertion{TypeConstraint{ins.valreg, TypeGroup::number}},
            Assertion{TypeConstraint{ins.access.basereg, TypeGroup::pointer}},
            Assertion{make_valid_access(ins.access.basereg, ins.access.offset,
                                        Imm{static_cast<uint32_t>(ins.access.width)}, false)},
        };
    }

    vector<Assertion> operator()(const Un& ins) const {
        return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
    }

    vector<Assertion> operator()(const Bin& ins) const {
        switch (ins.op) {
        case Bin::Op::MOV:
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                if (!ins.is64) {
                    return {Assertion{TypeConstraint{*src, TypeGroup::number}}};
                }
            }
            return {};
        case Bin::Op::MOVSX8:
        case Bin::Op::MOVSX16:
        case Bin::Op::MOVSX32:
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                return {Assertion{TypeConstraint{*src, TypeGroup::number}}};
            }
            return {};
        case Bin::Op::ADD: {
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}},
                        Assertion{TypeConstraint{*src, TypeGroup::ptr_or_num}}, Assertion{Addable{*src, ins.dst}},
                        Assertion{Addable{ins.dst, *src}}};
            }
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};
        }
        case Bin::Op::SUB: {
            if (const auto reg = std::get_if<Reg>(&ins.v)) {
                vector<Assertion> res;
                // disallow map-map since same type does not mean same offset
                // TODO: map identities
                res.emplace_back(TypeConstraint{ins.dst, TypeGroup::ptr_or_num});
                res.emplace_back(Comparable{.r1 = ins.dst, .r2 = *reg, .or_r2_is_number = true});
                return res;
            }
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};
        }
        case Bin::Op::UDIV:
        case Bin::Op::UMOD:
        case Bin::Op::SDIV:
        case Bin::Op::SMOD: {
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                const bool is_signed = (ins.op == Bin::Op::SDIV || ins.op == Bin::Op::SMOD);
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},
                        Assertion{ValidDivisor{*src, is_signed}}};
            }
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
        }
            // For all other binary operations, the destination register must be a number and the source must either be
            // an immediate or a number.
        default:
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},
                        Assertion{TypeConstraint{*src, TypeGroup::number}}};
            } else {
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
            }
        }
        assert(false);
    }
};

/// Annotate the CFG by adding explicit assertions for all the preconditions
/// of any instruction. For example, jump instructions are asserted not to
/// compare numbers and pointers, or pointers to potentially distinct memory
/// regions. The verifier will use these assertions to treat the program as
/// unsafe unless it can prove that the assertions can never fail.
vector<Assertion> get_assertions(Instruction ins, const ProgramInfo& info, const std::optional<Label>& label) {
    return std::visit(AssertExtractor{info, label}, ins);
}
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <cassert>
4	#include <cinttypes>
5	#include <utility>
6	#include <vector>
7
8	#include "asm_syntax.hpp"
9	#include "cfg/cfg.hpp"
10	#include "platform.hpp"
11
12	using std::string;
13	using std::to_string;
14	using std::vector;
15
16	namespace prevail {
17	class AssertExtractor {
18	ProgramInfo info;
19	std::optional<Label> current_label; ///< Pre-simplification label this assert is part of.
20
21	static Imm imm(const Value& v) { return std::get<Imm>(v); }
22
23	static vector<Assertion> zero_offset_ctx(const Reg reg) {	5,402✔
24	vector<Assertion> res;	5,402✔
25	res.emplace_back(TypeConstraint{reg, TypeGroup::ctx});	5,402✔
26	res.emplace_back(ZeroCtxOffset{reg});	5,402✔
27	return res;	5,402✔
28	}	×
29
30	[[nodiscard]]
31	ValidAccess make_valid_access(const Reg reg, const int32_t offset = {}, const Value& width = Imm{0},	49,916✔
32	const bool or_null = {}, const AccessType access_type = {}) const {
33	const int depth = current_label.has_value() ? current_label.value().call_stack_depth() : 1;	49,916✔
34	return ValidAccess{depth, reg, offset, width, or_null, access_type};	49,916✔
35	}
36
37	public:
38	explicit AssertExtractor(ProgramInfo info, std::optional<Label> label)	341,244✔
39	: info{std::move(info)}, current_label(std::move(label)) {}	341,244✔
40
41	vector<Assertion> operator()(const Undefined&) const {	4,992✔
42	// assert(false);
43	return {};	4,992✔
44	}
45
46	vector<Assertion> operator()(const IncrementLoopCounter& ipc) const { return {{BoundedLoopCount{ipc.name}}}; }	128✔
47
48	vector<Assertion> operator()(const LoadMapFd&) const { return {}; }	12,484✔
49	vector<Assertion> operator()(const LoadMapAddress&) const { return {}; }	10✔
50
51	/// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.
52	vector<Assertion> operator()(const Packet&) const { return zero_offset_ctx({6}); }	236✔
53
54	vector<Assertion> operator()(const Exit&) const {	1,492✔
55	vector<Assertion> res;	1,492✔
56	if (current_label->stack_frame_prefix.empty()) {	1,492✔
57	// Verify that Exit returns a number.
58	res.emplace_back(TypeConstraint{Reg{R0_RETURN_VALUE}, TypeGroup::number});	1,388✔
59	}
60	return res;	1,492✔
61	}	×
62
63	vector<Assertion> operator()(const Call& call) const {	19,834✔
64	vector<Assertion> res;	19,834✔
65	std::optional<Reg> map_fd_reg;	19,834✔
66	res.emplace_back(ValidCall{call.func, call.stack_frame_prefix});	19,834✔
67	for (ArgSingle arg : call.singles) {	66,576✔
68	switch (arg.kind) {	46,742✔
69	case ArgSingle::Kind::ANYTHING:	13,328✔
70	// avoid pointer leakage:
71	if (!info.type.is_privileged) {	13,328✔
72	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});	13,146✔
73	}
74	break;	6,664✔
75	case ArgSingle::Kind::MAP_FD_PROGRAMS:	346✔
76	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd_programs});	346✔
77	// Do not update map_fd_reg
78	break;	346✔
79	case ArgSingle::Kind::MAP_FD:	12,110✔
80	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd});	12,110✔
81	map_fd_reg = arg.reg;	35,481✔
82	break;	6,055✔
83	case ArgSingle::Kind::PTR_TO_MAP_KEY:	15,792✔
84	case ArgSingle::Kind::PTR_TO_MAP_VALUE:	7,896✔
85	assert(map_fd_reg);	15,792✔
86	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});	15,792✔
87	res.emplace_back(ValidMapKeyValue{arg.reg, *map_fd_reg, arg.kind == ArgSingle::Kind::PTR_TO_MAP_KEY});	15,792✔
88	break;	15,792✔
89	case ArgSingle::Kind::PTR_TO_CTX:	5,166✔
90	for (const Assertion& a : zero_offset_ctx(arg.reg)) {	15,498✔
91	res.emplace_back(a);	10,332✔
92	}	5,166✔
93	break;	5,166✔
94	}
95	}
96	for (ArgPair arg : call.pairs) {	24,186✔
97	const auto group = arg.or_null ? TypeGroup::mem_or_num : TypeGroup::mem;	4,352✔
98	const auto access_type =	6,528✔
99	arg.kind == ArgPair::Kind::PTR_TO_READABLE_MEM ? AccessType::read : AccessType::write;	4,352✔
100	res.emplace_back(TypeConstraint{arg.size, TypeGroup::number});	4,352✔
101	res.emplace_back(ValidSize{arg.size, arg.can_be_zero});	4,352✔
102	res.emplace_back(TypeConstraint{arg.mem, group});	4,352✔
103	res.emplace_back(make_valid_access(arg.mem, 0, arg.size, arg.or_null, access_type));	6,522✔
104	// TODO: reg is constant (or maybe it's not important)
105	}
106	return res;	29,751✔
107	}	×
108
109	vector<Assertion> operator()(const CallLocal&) const { return {}; }	104✔
110
111	vector<Assertion> operator()(const Callx& callx) const {	48✔
112	vector<Assertion> res;	48✔
113	res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});	48✔
114	res.emplace_back(FuncConstraint{callx.func});	48✔
115	return res;	48✔
116	}	×
117
118	[[nodiscard]]
119	vector<Assertion> explicate(const Condition& cond) const {	25,572✔
120	if (info.type.is_privileged) {	25,572✔
121	return {};	164✔
122	}
123	vector<Assertion> res;	25,408✔
124	if (const auto pimm = std::get_if<Imm>(&cond.right)) {	25,408✔
125	if (pimm->v != 0) {	20,298✔
126	// no need to check for valid access, it must be a number
127	res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});	6,312✔
128	} else {
129	bool allow_pointers = false;	13,986✔
130
131	switch (cond.op) {	13,986✔
132	case Condition::Op::EQ: allow_pointers = true; break;	9,547✔
133	case Condition::Op::NE: allow_pointers = true; break;	9,552✔
134	case Condition::Op::SET: allow_pointers = true; break;	6,381✔
135	case Condition::Op::NSET: allow_pointers = true; break;	6,381✔
136	case Condition::Op::LT: allow_pointers = true; break;	6,394✔
137	case Condition::Op::LE: allow_pointers = true; break;	6,381✔
138	case Condition::Op::GT: allow_pointers = true; break;	6,393✔
139	case Condition::Op::GE: allow_pointers = true; break;	6,382✔
140	case Condition::Op::SLT: allow_pointers = false; break;	590✔
141	case Condition::Op::SLE: allow_pointers = false; break;	3✔
142	case Condition::Op::SGT: allow_pointers = false; break;	17✔
143	case Condition::Op::SGE: allow_pointers = false; break;	4✔
144	default: assert(!"unexpected condition");	6,993✔
145	}
146
147	// Only permit pointer comparisons if the operation is 64-bit.
148	allow_pointers &= cond.is64;	13,986✔
149
150	if (!allow_pointers) {	13,986✔
151	res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});	7,290✔
152	}
153
154	res.emplace_back(make_valid_access(cond.left));	20,979✔
155	// OK - map_fd is just another pointer
156	// Anything can be compared to 0
157	}
158	} else {
159	const auto reg_right = get<Reg>(cond.right);	5,110✔
160	res.emplace_back(make_valid_access(cond.left));	7,665✔
161	res.emplace_back(make_valid_access(reg_right));	7,665✔
162	if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {	5,110✔
163	res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});	3,732✔
164	}
165	res.emplace_back(Comparable{.r1 = cond.left, .r2 = reg_right, .or_r2_is_number = false});	5,110✔
166	}
167	return res;	25,408✔
168	}	25,408✔
169
170	vector<Assertion> operator()(const Assume& ins) const {	50,792✔
171	if (!ins.is_implicit) {	50,792✔
172	return explicate(ins.cond);	340✔
173	}
174	return {};	50,452✔
175	}
176
177	vector<Assertion> operator()(const Jmp& ins) const {	29,740✔
178	if (!ins.cond) {	29,740✔
179	return {};	4,508✔
180	}
181	return explicate(*ins.cond);	25,232✔
182	}
183
184	vector<Assertion> operator()(const Mem& ins) const {	64,764✔
185	vector<Assertion> res;	64,764✔
186	const Reg basereg = ins.access.basereg;	64,764✔
187	Imm width{gsl::narrow<uint32_t>(ins.access.width)};	64,764✔
188	const int offset = ins.access.offset;	64,764✔
189	if (basereg.v == R10_STACK_POINTER) {	64,764✔
190	// We know we are accessing the stack.
191	if (offset < -EBPF_SUBPROGRAM_STACK_SIZE \|\| offset + static_cast<int>(width.v) > 0) {	43,822✔
192	// This assertion will fail
193	res.emplace_back(make_valid_access(basereg, offset, width, false,	3✔
194	ins.is_load ? AccessType::read : AccessType::write));	2✔
195	} else if (ins.is_load) {
196	// This assertion is not for bound checks but for reading initialized memory.
197	// TODO: avoid load assertions: use post-assertion to check that the loaded value is initialized
198	// res.emplace_back(make_valid_access(basereg, offset, width, false, AccessType::read));
199	}
200	} else {
201	res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer});	20,942✔
202	res.emplace_back(	31,413✔
203	make_valid_access(basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write));	34,279✔
204	if (!info.type.is_privileged && !ins.is_load) {	20,942✔
205	if (const auto preg = std::get_if<Reg>(&ins.value)) {	5,718✔
206	if (width.v != 8) {	5,708✔
207	res.emplace_back(TypeConstraint{*preg, TypeGroup::number});	4,910✔
208	} else {
209	res.emplace_back(ValidStore{ins.access.basereg, *preg});	798✔
210	}
211	}
212	}
213	}
214	return res;	97,146✔
215	}	×
216
217	vector<Assertion> operator()(const Atomic& ins) const {	414✔
218
219	return {	207✔
220	Assertion{TypeConstraint{ins.valreg, TypeGroup::number}},	207✔
221	Assertion{TypeConstraint{ins.access.basereg, TypeGroup::pointer}},	207✔
222	Assertion{make_valid_access(ins.access.basereg, ins.access.offset,	621✔
223	Imm{static_cast<uint32_t>(ins.access.width)}, false)},	207✔
224	};	1,863✔
225	}	828✔
226
227	vector<Assertion> operator()(const Un& ins) const {	2,960✔
228	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	7,400✔
229	}	2,960✔
230
231	vector<Assertion> operator()(const Bin& ins) const {	153,342✔
232	switch (ins.op) {	153,342✔
233	case Bin::Op::MOV:	88,640✔
234	if (const auto src = std::get_if<Reg>(&ins.v)) {	88,640✔
235	if (!ins.is64) {	48,836✔
236	return {Assertion{TypeConstraint{*src, TypeGroup::number}}};	29,340✔
237	}
238	}
239	return {};	76,904✔
240	case Bin::Op::MOVSX8:	2,262✔
241	case Bin::Op::MOVSX16:	1,131✔
242	case Bin::Op::MOVSX32:	1,131✔
243	if (const auto src = std::get_if<Reg>(&ins.v)) {	2,262✔
244	return {Assertion{TypeConstraint{*src, TypeGroup::number}}};	5,655✔
245	}
246	return {};	×
247	case Bin::Op::ADD: {	30,188✔
248	if (const auto src = std::get_if<Reg>(&ins.v)) {	30,188✔
249	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}},	2,454✔
250	Assertion{TypeConstraint{src, TypeGroup::ptr_or_num}}, Assertion{Addable{src, ins.dst}},	2,454✔
251	Assertion{Addable{ins.dst, *src}}};	26,994✔
252	}
253	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};	63,200✔
254	}
255	case Bin::Op::SUB: {	810✔
256	if (const auto reg = std::get_if<Reg>(&ins.v)) {	810✔
257	vector<Assertion> res;	782✔
258	// disallow map-map since same type does not mean same offset
259	// TODO: map identities
260	res.emplace_back(TypeConstraint{ins.dst, TypeGroup::ptr_or_num});	782✔
261	res.emplace_back(Comparable{.r1 = ins.dst, .r2 = *reg, .or_r2_is_number = true});	782✔
262	return res;	782✔
263	}	782✔
264	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};	70✔
265	}
266	case Bin::Op::UDIV:	2,498✔
267	case Bin::Op::UMOD:	1,249✔
268	case Bin::Op::SDIV:	1,249✔
269	case Bin::Op::SMOD: {	1,249✔
270	if (const auto src = std::get_if<Reg>(&ins.v)) {	2,498✔
271	const bool is_signed = (ins.op == Bin::Op::SDIV \|\| ins.op == Bin::Op::SMOD);	220✔
272	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},	110✔
273	Assertion{ValidDivisor{*src, is_signed}}};	770✔
274	}
275	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	5,695✔
276	}
277	// For all other binary operations, the destination register must be a number and the source must either be
278	// an immediate or a number.
279	default:	28,944✔
280	if (const auto src = std::get_if<Reg>(&ins.v)) {	28,944✔
281	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},	3,764✔
282	Assertion{TypeConstraint{*src, TypeGroup::number}}};	26,348✔
283	} else {
284	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	53,540✔
285	}
286	}
287	assert(false);
288	}	75,656✔
289	};
290
291	/// Annotate the CFG by adding explicit assertions for all the preconditions
292	/// of any instruction. For example, jump instructions are asserted not to
293	/// compare numbers and pointers, or pointers to potentially distinct memory
294	/// regions. The verifier will use these assertions to treat the program as
295	/// unsafe unless it can prove that the assertions can never fail.
296	vector<Assertion> get_assertions(Instruction ins, const ProgramInfo& info, const std::optional<Label>& label) {	341,244✔
297	return std::visit(AssertExtractor{info, label}, ins);	853,089✔
298	}
299	} // namespace prevail

Alan-Jowett / ebpf-verifier / 18658728485

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