21993000823

Committed 13 Feb 2026 01:02PM UTC coverage: 86.313% (-0.5%) from 86.783%

Build # 21993000823

Build Type

push

github

Committed by

web-flow

Commit Message

ISA feature support matrix and precise rejection semantics (#999)

* ISA feature support matrix and precise rejection semantics

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

Run Details

282 of 380 new or added lines in 14 files covered. (74.21%)

3 existing lines in 3 files now uncovered.

9535 of 11047 relevant lines covered (86.31%)

3060772.25 hits per line

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

92.55

/src/ir/assertions.cpp

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

#include "ir/syntax.hpp"
#include "platform.hpp"

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

namespace prevail {
class AssertExtractor {
    const ProgramInfo& info;
    const 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, const bool or_null) {
        vector<Assertion> res;
        res.emplace_back(TypeConstraint{reg, or_null ? TypeGroup::ctx_or_num : TypeGroup::ctx});
        res.emplace_back(ZeroCtxOffset{reg, or_null});
        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(const ProgramInfo& info, const std::optional<Label>& label)
        : info{info}, current_label{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 {}; }
    // Rejected before assertion extraction by cfg_builder::check_instruction_feature_support.
    vector<Assertion> operator()(const LoadPseudo&) const {
        assert(false && "LoadPseudo should be rejected before assertion extraction");
        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}, false); }

    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_STACK:
                res.emplace_back(TypeConstraint{arg.reg, arg.or_null ? TypeGroup::stack_or_num : TypeGroup::stack});
                // TODO: check 0 when null
                break;
            case ArgSingle::Kind::PTR_TO_CTX:
                for (const Assertion& a : zero_offset_ctx(arg.reg, arg.or_null)) {
                    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;
    }

    // Rejected before assertion extraction by cfg_builder::check_instruction_feature_support.
    vector<Assertion> operator()(const CallBtf&) const {
        assert(false && "CallBtf should be rejected before assertion extraction");
        return {};
    }

    [[nodiscard]]
    vector<Assertion> explicate(const Condition& cond) const {
        vector<Assertion> res;
        if (info.type.is_privileged) {
            return 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)) {
                // disallow map-map since same type does not mean same offset
                // TODO: map identities
                return {TypeConstraint{ins.dst, TypeGroup::ptr_or_num},
                        Comparable{.r1 = ins.dst, .r2 = *reg, .or_r2_is_number = true}};
            }
            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(const 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 "ir/syntax.hpp"
9	#include "platform.hpp"
10
11	using std::string;
12	using std::to_string;
13	using std::vector;
14
15	namespace prevail {
16	class AssertExtractor {
17	const ProgramInfo& info;
18	const std::optional<Label>& current_label; ///< Pre-simplification label this assert is part of.
19
20	static Imm imm(const Value& v) { return std::get<Imm>(v); }
21
22	static vector<Assertion> zero_offset_ctx(const Reg reg, const bool or_null) {	6,036✔
23	vector<Assertion> res;	6,036✔
24	res.emplace_back(TypeConstraint{reg, or_null ? TypeGroup::ctx_or_num : TypeGroup::ctx});	9,030✔
25	res.emplace_back(ZeroCtxOffset{reg, or_null});	6,036✔
26	return res;	6,036✔
27	}	×
28
29	[[nodiscard]]
30	ValidAccess make_valid_access(const Reg reg, const int32_t offset = {}, const Value& width = Imm{0},	58,830✔
31	const bool or_null = {}, const AccessType access_type = {}) const {
32	const int depth = current_label.has_value() ? current_label.value().call_stack_depth() : 1;	58,830✔
33	return ValidAccess{depth, reg, offset, width, or_null, access_type};	58,830✔
34	}
35
36	public:
37	explicit AssertExtractor(const ProgramInfo& info, const std::optional<Label>& label)	390,318✔
38	: info{info}, current_label{label} {}	390,318✔
39
40	vector<Assertion> operator()(const Undefined&) const {	5,508✔
41	// assert(false);
42	return {};	5,508✔
43	}
44
45	vector<Assertion> operator()(const IncrementLoopCounter& ipc) const { return {{BoundedLoopCount{ipc.name}}}; }	128✔
46
47	vector<Assertion> operator()(const LoadMapFd&) const { return {}; }	13,632✔
48	vector<Assertion> operator()(const LoadMapAddress&) const { return {}; }	424✔
49	// Rejected before assertion extraction by cfg_builder::check_instruction_feature_support.
NEW 50	vector<Assertion> operator()(const LoadPseudo&) const {	×
NEW 51	assert(false && "LoadPseudo should be rejected before assertion extraction");	×
52	return {};
53	}
54
55	/// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.
56	vector<Assertion> operator()(const Packet&) const { return zero_offset_ctx({6}, false); }	236✔
57
58	vector<Assertion> operator()(const Exit&) const {	1,892✔
59	vector<Assertion> res;	1,892✔
60	if (current_label->stack_frame_prefix.empty()) {	1,892✔
61	// Verify that Exit returns a number.
62	res.emplace_back(TypeConstraint{Reg{R0_RETURN_VALUE}, TypeGroup::number});	1,786✔
63	}
64	return res;	1,892✔
65	}	×
66
67	vector<Assertion> operator()(const Call& call) const {	21,534✔
68	vector<Assertion> res;	21,534✔
69	std::optional<Reg> map_fd_reg;	21,534✔
70	res.emplace_back(ValidCall{call.func, call.stack_frame_prefix});	21,534✔
71	for (ArgSingle arg : call.singles) {	72,018✔
72	switch (arg.kind) {	50,484✔
73	case ArgSingle::Kind::ANYTHING:	14,142✔
74	// avoid pointer leakage:
75	if (!info.type.is_privileged) {	14,142✔
76	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});	13,954✔
77	}
78	break;	7,071✔
79	case ArgSingle::Kind::MAP_FD_PROGRAMS:	500✔
80	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd_programs});	500✔
81	// Do not update map_fd_reg
82	break;	500✔
83	case ArgSingle::Kind::MAP_FD:	13,092✔
84	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd});	13,092✔
85	map_fd_reg = arg.reg;	38,334✔
86	break;	6,546✔
87	case ArgSingle::Kind::PTR_TO_MAP_KEY:	16,950✔
88	case ArgSingle::Kind::PTR_TO_MAP_VALUE:	8,475✔
89	assert(map_fd_reg);	16,950✔
90	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});	16,950✔
91	res.emplace_back(ValidMapKeyValue{arg.reg, *map_fd_reg, arg.kind == ArgSingle::Kind::PTR_TO_MAP_KEY});	16,950✔
92	break;	16,950✔
93	case ArgSingle::Kind::PTR_TO_STACK:	×
94	res.emplace_back(TypeConstraint{arg.reg, arg.or_null ? TypeGroup::stack_or_num : TypeGroup::stack});	×
95	// TODO: check 0 when null
96	break;	×
97	case ArgSingle::Kind::PTR_TO_CTX:	5,800✔
98	for (const Assertion& a : zero_offset_ctx(arg.reg, arg.or_null)) {	17,400✔
99	res.emplace_back(a);	11,600✔
100	}	5,800✔
101	break;	5,800✔
102	}
103	}
104	for (ArgPair arg : call.pairs) {	26,252✔
105	const auto group = arg.or_null ? TypeGroup::mem_or_num : TypeGroup::mem;	4,718✔
106	const auto access_type =	7,077✔
107	arg.kind == ArgPair::Kind::PTR_TO_READABLE_MEM ? AccessType::read : AccessType::write;	4,718✔
108	res.emplace_back(TypeConstraint{arg.size, TypeGroup::number});	4,718✔
109	res.emplace_back(ValidSize{arg.size, arg.can_be_zero});	4,718✔
110	res.emplace_back(TypeConstraint{arg.mem, group});	4,718✔
111	res.emplace_back(make_valid_access(arg.mem, 0, arg.size, arg.or_null, access_type));	7,071✔
112	// TODO: reg is constant (or maybe it's not important)
113	}
114	return res;	32,301✔
115	}	×
116
117	vector<Assertion> operator()(const CallLocal&) const { return {}; }	106✔
118
119	vector<Assertion> operator()(const Callx& callx) const {	48✔
120	vector<Assertion> res;	48✔
121	res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});	48✔
122	res.emplace_back(FuncConstraint{callx.func});	48✔
123	return res;	48✔
124	}	×
125
126	// Rejected before assertion extraction by cfg_builder::check_instruction_feature_support.
NEW 127	vector<Assertion> operator()(const CallBtf&) const {	×
NEW 128	assert(false && "CallBtf should be rejected before assertion extraction");	×
129	return {};
130	}
131
132	[[nodiscard]]
133	vector<Assertion> explicate(const Condition& cond) const {	30,388✔
134	vector<Assertion> res;	30,388✔
135	if (info.type.is_privileged) {	30,388✔
136	return res;	85✔
137	}
138	if (const auto pimm = std::get_if<Imm>(&cond.right)) {	30,218✔
139	if (pimm->v != 0) {	24,450✔
140	// no need to check for valid access, it must be a number
141	res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});	8,176✔
142	} else {
143	bool allow_pointers = false;	16,274✔
144
145	switch (cond.op) {	16,274✔
146	case Condition::Op::EQ: allow_pointers = true; break;	11,127✔
147	case Condition::Op::NE: allow_pointers = true; break;	10,779✔
148	case Condition::Op::SET: allow_pointers = true; break;	7,317✔
149	case Condition::Op::NSET: allow_pointers = true; break;	7,317✔
150	case Condition::Op::LT: allow_pointers = true; break;	7,330✔
151	case Condition::Op::LE: allow_pointers = true; break;	7,317✔
152	case Condition::Op::GT: allow_pointers = true; break;	7,329✔
153	case Condition::Op::GE: allow_pointers = true; break;	7,319✔
154	case Condition::Op::SLT: allow_pointers = false; break;	796✔
155	case Condition::Op::SLE: allow_pointers = false; break;	4✔
156	case Condition::Op::SGT: allow_pointers = false; break;	18✔
157	case Condition::Op::SGE: allow_pointers = false; break;	4✔
158	default: assert(!"unexpected condition");	8,137✔
159	}
160
161	// Only permit pointer comparisons if the operation is 64-bit.
162	allow_pointers &= cond.is64;	16,274✔
163
164	if (!allow_pointers) {	16,274✔
165	res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});	8,746✔
166	}
167
168	res.emplace_back(make_valid_access(cond.left));	24,411✔
169	// OK - map_fd is just another pointer
170	// Anything can be compared to 0
171	}
172	} else {
173	const auto reg_right = get<Reg>(cond.right);	5,768✔
174	res.emplace_back(make_valid_access(cond.left));	8,652✔
175	res.emplace_back(make_valid_access(reg_right));	8,652✔
176	if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {	5,768✔
177	res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});	4,092✔
178	}
179	res.emplace_back(Comparable{.r1 = cond.left, .r2 = reg_right, .or_r2_is_number = false});	5,768✔
180	}
181	return res;	15,109✔
182	}	×
183
184	vector<Assertion> operator()(const Assume& ins) const {	60,400✔
185	if (!ins.is_implicit) {	60,400✔
186	return explicate(ins.cond);	340✔
187	}
188	return {};	60,060✔
189	}
190
191	vector<Assertion> operator()(const Jmp& ins) const {	35,620✔
192	if (!ins.cond) {	35,620✔
193	return {};	5,572✔
194	}
195	return explicate(*ins.cond);	30,048✔
196	}
197
198	vector<Assertion> operator()(const Mem& ins) const {	76,798✔
199	vector<Assertion> res;	76,798✔
200	const Reg basereg = ins.access.basereg;	76,798✔
201	Imm width{gsl::narrow<uint32_t>(ins.access.width)};	76,798✔
202	const int offset = ins.access.offset;	76,798✔
203	if (basereg.v == R10_STACK_POINTER) {	76,798✔
204	// We know we are accessing the stack.
205	if (offset < -EBPF_SUBPROGRAM_STACK_SIZE \|\| offset + static_cast<int>(width.v) > 0) {	51,036✔
206	// This assertion will fail
207	res.emplace_back(make_valid_access(basereg, offset, width, false,	3✔
208	ins.is_load ? AccessType::read : AccessType::write));	2✔
209	} else if (ins.is_load) {
210	// This assertion is not for bound checks but for reading initialized memory.
211	// TODO: avoid load assertions: use post-assertion to check that the loaded value is initialized
212	// res.emplace_back(make_valid_access(basereg, offset, width, false, AccessType::read));
213	}
214	} else {
215	res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer});	25,762✔
216	res.emplace_back(	38,643✔
217	make_valid_access(basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write));	42,141✔
218	if (!info.type.is_privileged && !ins.is_load) {	25,762✔
219	if (const auto preg = std::get_if<Reg>(&ins.value)) {	6,982✔
220	if (width.v != 8) {	6,972✔
221	res.emplace_back(TypeConstraint{*preg, TypeGroup::number});	5,870✔
222	} else {
223	res.emplace_back(ValidStore{ins.access.basereg, *preg});	1,102✔
224	}
225	}
226	}
227	}
228	return res;	115,197✔
229	}	×
230
231	vector<Assertion> operator()(const Atomic& ins) const {	538✔
232
233	return {	269✔
234	Assertion{TypeConstraint{ins.valreg, TypeGroup::number}},	269✔
235	Assertion{TypeConstraint{ins.access.basereg, TypeGroup::pointer}},	269✔
236	Assertion{make_valid_access(ins.access.basereg, ins.access.offset,	807✔
237	Imm{static_cast<uint32_t>(ins.access.width)}, false)},	269✔
238	};	2,421✔
239	}	1,076✔
240
241	vector<Assertion> operator()(const Un& ins) const {	3,156✔
242	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	7,890✔
243	}	3,156✔
244
245	vector<Assertion> operator()(const Bin& ins) const {	170,394✔
246	switch (ins.op) {	170,394✔
247	case Bin::Op::MOV:	99,056✔
248	if (const auto src = std::get_if<Reg>(&ins.v)) {	99,056✔
249	if (!ins.is64) {	53,114✔
250	return {Assertion{TypeConstraint{*src, TypeGroup::number}}};	33,055✔
251	}
252	}
253	return {};	85,834✔
254	case Bin::Op::MOVSX8:	2,274✔
255	case Bin::Op::MOVSX16:	1,137✔
256	case Bin::Op::MOVSX32:	1,137✔
257	if (const auto src = std::get_if<Reg>(&ins.v)) {	2,274✔
258	return {Assertion{TypeConstraint{*src, TypeGroup::number}}};	5,685✔
259	}
260	return {};	×
261	case Bin::Op::ADD: {	32,820✔
262	if (const auto src = std::get_if<Reg>(&ins.v)) {	32,820✔
263	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}},	2,653✔
264	Assertion{TypeConstraint{src, TypeGroup::ptr_or_num}}, Assertion{Addable{src, ins.dst}},	2,653✔
265	Assertion{Addable{ins.dst, *src}}};	29,183✔
266	}
267	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};	68,785✔
268	}
269	case Bin::Op::SUB: {	858✔
270	if (const auto reg = std::get_if<Reg>(&ins.v)) {	858✔
271	// disallow map-map since same type does not mean same offset
272	// TODO: map identities
273	return {TypeConstraint{ins.dst, TypeGroup::ptr_or_num},	413✔
274	Comparable{.r1 = ins.dst, .r2 = *reg, .or_r2_is_number = true}};	2,891✔
275	}
276	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};	80✔
277	}
278	case Bin::Op::UDIV:	2,632✔
279	case Bin::Op::UMOD:	1,316✔
280	case Bin::Op::SDIV:	1,316✔
281	case Bin::Op::SMOD: {	1,316✔
282	if (const auto src = std::get_if<Reg>(&ins.v)) {	2,632✔
283	const bool is_signed = (ins.op == Bin::Op::SDIV \|\| ins.op == Bin::Op::SMOD);	274✔
284	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},	137✔
285	Assertion{ValidDivisor{*src, is_signed}}};	959✔
286	}
287	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	5,895✔
288	}
289	// For all other binary operations, the destination register must be a number and the source must either be
290	// an immediate or a number.
291	default:	32,754✔
292	if (const auto src = std::get_if<Reg>(&ins.v)) {	32,754✔
293	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},	4,365✔
294	Assertion{TypeConstraint{*src, TypeGroup::number}}};	30,555✔
295	} else {
296	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	60,060✔
297	}
298	}
299	assert(false);
300	}	84,560✔
301	};
302
303	/// Annotate the CFG by adding explicit assertions for all the preconditions
304	/// of any instruction. For example, jump instructions are asserted not to
305	/// compare numbers and pointers, or pointers to potentially distinct memory
306	/// regions. The verifier will use these assertions to treat the program as
307	/// unsafe unless it can prove that the assertions can never fail.
308	vector<Assertion> get_assertions(const Instruction& ins, const ProgramInfo& info, const std::optional<Label>& label) {	390,318✔
309	return std::visit(AssertExtractor{info, label}, ins);	390,318✔
310	}
311	} // namespace prevail

Alan-Jowett / ebpf-verifier / 21993000823

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