11674460316

Committed 04 Nov 2024 11:25PM UTC coverage: 90.541% (+0.05%) from 90.488%

Build # 11674460316

Build Type

push

github

Committed by

elazarg

Commit Message

revert to memcpy, add requires(trivially_copyable)

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

Run Details

2 of 2 new or added lines in 1 file covered. (100.0%)

76 existing lines in 3 files now uncovered.

8567 of 9462 relevant lines covered (90.54%)

8696209.32 hits per line

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

94.44

/src/assertions.cpp

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

#include <utility>
#include <vector>

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

using crab::TypeGroup;
using std::string;
using std::to_string;
using std::vector;

class AssertExtractor {
    program_info info;
    std::optional<label_t> current_label; ///< Pre-simplification label this assert is part of.

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

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

    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(program_info info, std::optional<label_t> label)
        : info{std::move(info)}, current_label(label) {}

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

    vector<Assert> operator()(Assert const&) const {
        assert(false);
        return {};
    }

    vector<Assert> operator()(IncrementLoopCounter) const {
        assert(false);
        return {};
    }

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

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

    vector<Assert> operator()(Exit const&) const {
        vector<Assert> 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<Assert> operator()(Call const& call) const {
        vector<Assert> 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 Assert& a : zero_offset_ctx(arg.reg)) {
                    res.emplace_back(a);
                }
                break;
            }
        }
        for (ArgPair arg : call.pairs) {
            res.emplace_back(TypeConstraint{arg.size, TypeGroup::number});
            res.emplace_back(ValidSize{arg.size, arg.can_be_zero});
            switch (arg.kind) {
            case ArgPair::Kind::PTR_TO_READABLE_MEM_OR_NULL:
                res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem_or_num});
                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, true, AccessType::read));
                break;
            case ArgPair::Kind::PTR_TO_READABLE_MEM:
                /* pointer to valid memory (stack, packet, map value) */
                res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem});
                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::read));
                break;
            case ArgPair::Kind::PTR_TO_WRITABLE_MEM:
                // memory may be uninitialized, i.e. write only
                res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem});
                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::write));
                break;
            }
            // TODO: reg is constant (or maybe it's not important)
        }
        return res;
    }

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

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

    [[nodiscard]]
    vector<Assert> explicate(const Condition& cond) const {
        if (info.type.is_privileged) {
            return {};
        }
        vector<Assert> 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<Assert> operator()(const Assume& ins) const { return explicate(ins.cond); }

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

    vector<Assert> operator()(const Mem& ins) const {
        vector<Assert> res;
        const Reg basereg = ins.access.basereg;
        Imm width{static_cast<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 {
            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<Assert> operator()(const Atomic& ins) const {

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

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

    vector<Assert> 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 {Assert{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 {Assert{TypeConstraint{*src, TypeGroup::number}}};
            }
            return {};
        case Bin::Op::ADD: {
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                return {Assert{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}},
                        Assert{TypeConstraint{*src, TypeGroup::ptr_or_num}}, Assert{Addable{*src, ins.dst}},
                        Assert{Addable{ins.dst, *src}}};
            }
            return {Assert{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};
        }
        case Bin::Op::SUB: {
            if (const auto reg = std::get_if<Reg>(&ins.v)) {
                vector<Assert> 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 {Assert{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 {Assert{TypeConstraint{ins.dst, TypeGroup::number}}, Assert{ValidDivisor{*src, is_signed}}};
            }
            return {Assert{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 {Assert{TypeConstraint{ins.dst, TypeGroup::number}},
                        Assert{TypeConstraint{*src, TypeGroup::number}}};
            } else {
                return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}};
            }
        }
        assert(false);
    }
};

vector<Assert> get_assertions(Instruction ins, const program_info& info, const std::optional<label_t>& label) {
    return std::visit(AssertExtractor{info, label}, ins);
}

/// 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.
void explicate_assertions(cfg_t& cfg, const program_info& info) {
    for (auto& [label, bb] : cfg) {
        (void)label; // unused
        vector<Instruction> insts;
        for (const auto& ins : vector<Instruction>(bb.begin(), bb.end())) {
            for (auto a : get_assertions(ins, info, bb.label())) {
                insts.emplace_back(a);
            }
            insts.push_back(ins);
        }
        bb.swap_instructions(insts);
    }
}

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <cinttypes>
4
5	#include <utility>
6	#include <vector>
7
8	#include "asm_syntax.hpp"
9	#include "crab/cfg.hpp"
10	#include "platform.hpp"
11
12	using crab::TypeGroup;
13	using std::string;
14	using std::to_string;
15	using std::vector;
16
17	class AssertExtractor {
18	program_info info;
19	std::optional<label_t> 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<Assert> zero_offset_ctx(const Reg reg) {	5,402✔
24	vector<Assert> 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	ValidAccess make_valid_access(const Reg reg, const int32_t offset = {}, const Value& width = Imm{0},	49,910✔
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;	49,910✔
33	return ValidAccess{depth, reg, offset, width, or_null, access_type};	49,910✔
34	}
35
36	public:
37	explicit AssertExtractor(program_info info, std::optional<label_t> label)	285,378✔
38	: info{std::move(info)}, current_label(label) {}	428,067✔
39
40	vector<Assert> operator()(Undefined const&) const {	×
UNCOV 41	assert(false);	×
42	return {};
43	}
44
45	vector<Assert> operator()(Assert const&) const {	×
UNCOV 46	assert(false);	×
47	return {};
48	}
49
UNCOV 50	vector<Assert> operator()(IncrementLoopCounter) const {	×
UNCOV 51	assert(false);	×
52	return {};
53	}
54
55	vector<Assert> operator()(LoadMapFd const&) const { return {}; }	12,482✔
56
57	/// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.
58	vector<Assert> operator()(Packet const&) const { return zero_offset_ctx({6}); }	236✔
59
60	vector<Assert> operator()(Exit const&) const {	1,498✔
61	vector<Assert> res;	1,498✔
62	if (current_label->stack_frame_prefix.empty()) {	1,498✔
63	// Verify that Exit returns a number.
64	res.emplace_back(TypeConstraint{Reg{R0_RETURN_VALUE}, TypeGroup::number});	1,410✔
65	}
66	return res;	1,498✔
UNCOV 67	}	×
68
69	vector<Assert> operator()(Call const& call) const {	19,838✔
70	vector<Assert> res;	19,838✔
71	std::optional<Reg> map_fd_reg;	19,838✔
72	res.emplace_back(ValidCall{call.func, call.stack_frame_prefix});	19,838✔
73	for (ArgSingle arg : call.singles) {	66,588✔
74	switch (arg.kind) {	46,750✔
75	case ArgSingle::Kind::ANYTHING:	13,328✔
76	// avoid pointer leakage:
77	if (!info.type.is_privileged) {	13,328✔
78	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});	13,146✔
79	}
80	break;	6,664✔
81	case ArgSingle::Kind::MAP_FD_PROGRAMS:	346✔
82	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd_programs});	346✔
83	// Do not update map_fd_reg
84	break;	346✔
85	case ArgSingle::Kind::MAP_FD:	12,114✔
86	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd});	12,114✔
87	map_fd_reg = arg.reg;	35,489✔
88	break;	6,057✔
89	case ArgSingle::Kind::PTR_TO_MAP_KEY:	15,796✔
90	case ArgSingle::Kind::PTR_TO_MAP_VALUE:	7,898✔
91	assert(map_fd_reg);	15,796✔
92	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});	15,796✔
93	res.emplace_back(ValidMapKeyValue{arg.reg, *map_fd_reg, arg.kind == ArgSingle::Kind::PTR_TO_MAP_KEY});	15,796✔
94	break;	15,796✔
95	case ArgSingle::Kind::PTR_TO_CTX:	5,166✔
96	for (const Assert& a : zero_offset_ctx(arg.reg)) {	15,498✔
97	res.emplace_back(a);	10,332✔
98	}	5,166✔
99	break;	5,166✔
100	}
101	}
102	for (ArgPair arg : call.pairs) {	24,190✔
103	res.emplace_back(TypeConstraint{arg.size, TypeGroup::number});	4,352✔
104	res.emplace_back(ValidSize{arg.size, arg.can_be_zero});	4,352✔
105	switch (arg.kind) {	4,352✔
106	case ArgPair::Kind::PTR_TO_READABLE_MEM_OR_NULL:	1,012✔
107	res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem_or_num});	1,012✔
108	res.emplace_back(make_valid_access(arg.mem, 0, arg.size, true, AccessType::read));	1,518✔
109	break;	1,012✔
110	case ArgPair::Kind::PTR_TO_READABLE_MEM:	2,470✔
111	/* pointer to valid memory (stack, packet, map value) */
112	res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem});	2,470✔
113	res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::read));	3,702✔
114	break;	2,470✔
115	case ArgPair::Kind::PTR_TO_WRITABLE_MEM:	870✔
116	// memory may be uninitialized, i.e. write only
117	res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem});	870✔
118	res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::write));	1,302✔
119	break;	870✔
120	}
121	// TODO: reg is constant (or maybe it's not important)
122	}
123	return res;	29,757✔
UNCOV 124	}	×
125
126	vector<Assert> operator()(CallLocal const& call) const { return {}; }	88✔
127
128	vector<Assert> operator()(Callx const& callx) const {	50✔
129	vector<Assert> res;	50✔
130	res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});	50✔
131	res.emplace_back(FuncConstraint{callx.func});	50✔
132	return res;	50✔
UNCOV 133	}	×
134
135	[[nodiscard]]
136	vector<Assert> explicate(const Condition& cond) const {	25,582✔
137	if (info.type.is_privileged) {	25,582✔
138	return {};	12,873✔
139	}
140	vector<Assert> res;	25,418✔
141	if (const auto pimm = std::get_if<Imm>(&cond.right)) {	25,418✔
142	if (pimm->v != 0) {	20,274✔
143	// no need to check for valid access, it must be a number
144	res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});	6,302✔
145	} else {
146	bool allow_pointers = false;	13,972✔
147
148	switch (cond.op) {	13,972✔
149	case Condition::Op::EQ: allow_pointers = true; break;	3,167✔
150	case Condition::Op::NE: allow_pointers = true; break;	3,172✔
151	case Condition::Op::SET: allow_pointers = true; break;	2✔
152	case Condition::Op::NSET: allow_pointers = true; break;	2✔
153	case Condition::Op::LT: allow_pointers = true; break;	15✔
154	case Condition::Op::LE: allow_pointers = true; break;	6✔
155	case Condition::Op::GT: allow_pointers = true; break;	8✔
156	case Condition::Op::GE: allow_pointers = true; break;
157	case Condition::Op::SLT: allow_pointers = false; break;	590✔
158	case Condition::Op::SLE: allow_pointers = false; break;	7✔
159	case Condition::Op::SGT: allow_pointers = false; break;	15✔
160	case Condition::Op::SGE: allow_pointers = false; break;	2✔
161	default: assert(!"unexpected condition");	6,986✔
162	}
163
164	// Only permit pointer comparisons if the operation is 64-bit.
165	allow_pointers &= cond.is64;	13,972✔
166
167	if (!allow_pointers) {	13,972✔
168	res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});	7,290✔
169	}
170
171	res.emplace_back(make_valid_access(cond.left));	20,958✔
172	// OK - map_fd is just another pointer
173	// Anything can be compared to 0
174	}
175	} else {
176	const auto reg_right = get<Reg>(cond.right);	5,144✔
177	res.emplace_back(make_valid_access(cond.left));	7,716✔
178	res.emplace_back(make_valid_access(reg_right));	7,716✔
179	if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {	5,144✔
180	res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});	3,738✔
181	}
182	res.emplace_back(Comparable{.r1 = cond.left, .r2 = reg_right, .or_r2_is_number = false});	5,144✔
183	}
184	return res;	25,418✔
185	}	25,418✔
186
187	vector<Assert> operator()(const Assume& ins) const { return explicate(ins.cond); }	350✔
188
189	vector<Assert> operator()(const Jmp& ins) const {	29,726✔
190	if (!ins.cond) {	29,726✔
191	return {};	4,494✔
192	}
193	return explicate(*ins.cond);	25,232✔
194	}
195
196	vector<Assert> operator()(const Mem& ins) const {	64,442✔
197	vector<Assert> res;	64,442✔
198	const Reg basereg = ins.access.basereg;	64,442✔
199	Imm width{static_cast<uint32_t>(ins.access.width)};	64,442✔
200	const int offset = ins.access.offset;	64,442✔
201	if (basereg.v == R10_STACK_POINTER) {	64,442✔
202	// We know we are accessing the stack.
203	if (offset < -EBPF_SUBPROGRAM_STACK_SIZE \|\| offset + static_cast<int>(width.v) > 0) {	43,576✔
204	// This assertion will fail
205	res.emplace_back(make_valid_access(basereg, offset, width, false,	33✔
206	ins.is_load ? AccessType::read : AccessType::write));	22✔
207	}
208	} else {
209	res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer});	20,866✔
210	res.emplace_back(	31,299✔
211	make_valid_access(basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write));	34,149✔
212	if (!info.type.is_privileged && !ins.is_load) {	20,866✔
213	if (const auto preg = std::get_if<Reg>(&ins.value)) {	5,686✔
214	if (width.v != 8) {	5,676✔
215	res.emplace_back(TypeConstraint{*preg, TypeGroup::number});	4,882✔
216	} else {
217	res.emplace_back(ValidStore{ins.access.basereg, *preg});	794✔
218	}
219	}
220	}
221	}
222	return res;	96,663✔
UNCOV 223	}	×
224
225	vector<Assert> operator()(const Atomic& ins) const {	410✔
226
227	return {	205✔
228	Assert{TypeConstraint{ins.valreg, TypeGroup::number}},	615✔
229	Assert{TypeConstraint{ins.access.basereg, TypeGroup::pointer}},	410✔
230	Assert{make_valid_access(ins.access.basereg, ins.access.offset,	615✔
231	Imm{static_cast<uint32_t>(ins.access.width)}, false)},	615✔
232	};	2,050✔
233	}
234
235	vector<Assert> operator()(const Un ins) const { return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}}; }	5,912✔
236
237	vector<Assert> operator()(const Bin& ins) const {	153,302✔
238	switch (ins.op) {	153,302✔
239	case Bin::Op::MOV:	88,626✔
240	if (const auto src = std::get_if<Reg>(&ins.v)) {	88,626✔
241	if (!ins.is64) {	48,832✔
242	return {Assert{TypeConstraint{*src, TypeGroup::number}}};	23,472✔
243	}
244	}
245	return {};	76,890✔
246	case Bin::Op::MOVSX8:	2,262✔
247	case Bin::Op::MOVSX16:	1,131✔
248	case Bin::Op::MOVSX32:	1,131✔
249	if (const auto src = std::get_if<Reg>(&ins.v)) {	2,262✔
250	return {Assert{TypeConstraint{*src, TypeGroup::number}}};	4,524✔
251	}
252	return {};	76,651✔
253	case Bin::Op::ADD: {	30,162✔
254	if (const auto src = std::get_if<Reg>(&ins.v)) {	30,162✔
255	return {Assert{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}},	2,443✔
256	Assert{TypeConstraint{src, TypeGroup::ptr_or_num}}, Assert{Addable{src, ins.dst}},	9,772✔
257	Assert{Addable{ins.dst, *src}}};	24,430✔
258	}
259	return {Assert{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};	50,552✔
260	}
261	case Bin::Op::SUB: {	808✔
262	if (const auto reg = std::get_if<Reg>(&ins.v)) {	808✔
263	vector<Assert> res;	780✔
264	// disallow map-map since same type does not mean same offset
265	// TODO: map identities
266	res.emplace_back(TypeConstraint{ins.dst, TypeGroup::ptr_or_num});	780✔
267	res.emplace_back(Comparable{.r1 = ins.dst, .r2 = *reg, .or_r2_is_number = true});	780✔
268	return res;	780✔
269	}	780✔
270	return {Assert{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};	56✔
271	}
272	case Bin::Op::UDIV:	2,498✔
273	case Bin::Op::UMOD:	1,249✔
274	case Bin::Op::SDIV:	1,249✔
275	case Bin::Op::SMOD: {	1,249✔
276	if (const auto src = std::get_if<Reg>(&ins.v)) {	2,498✔
277	const bool is_signed = (ins.op == Bin::Op::SDIV \|\| ins.op == Bin::Op::SMOD);	220✔
278	return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}, Assert{ValidDivisor{*src, is_signed}}};	660✔
279	}
280	return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}};	4,556✔
281	}
282	// For all other binary operations, the destination register must be a number and the source must either be an
283	// immediate or a number.
284	default:	28,946✔
285	if (const auto src = std::get_if<Reg>(&ins.v)) {	28,946✔
286	return {Assert{TypeConstraint{ins.dst, TypeGroup::number}},	3,765✔
287	Assert{TypeConstraint{*src, TypeGroup::number}}};	22,590✔
288	} else {
289	return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}};	42,832✔
290	}
291	}
292	assert(false);
293	}
294	};
295
296	vector<Assert> get_assertions(Instruction ins, const program_info& info, const std::optional<label_t>& label) {	285,378✔
297	return std::visit(AssertExtractor{info, label}, ins);	713,423✔
298	}
299
300	/// Annotate the CFG by adding explicit assertions for all the preconditions
301	/// of any instruction. For example, jump instructions are asserted not to
302	/// compare numbers and pointers, or pointers to potentially distinct memory
303	/// regions. The verifier will use these assertions to treat the program as
304	/// unsafe unless it can prove that the assertions can never fail.
305	void explicate_assertions(cfg_t& cfg, const program_info& info) {	2,452✔
306	for (auto& [label, bb] : cfg) {	292,690✔
307	(void)label; // unused	145,119✔
308	vector<Instruction> insts;	290,238✔
309	for (const auto& ins : vector<Instruction>(bb.begin(), bb.end())) {	575,572✔
310	for (auto a : get_assertions(ins, info, bb.label())) {	1,017,783✔
311	insts.emplace_back(a);	304,448✔
312	}	589,782✔
313	insts.push_back(ins);	285,334✔
314	}	290,238✔
315	bb.swap_instructions(insts);	290,238✔
316	}	290,238✔
317	}	2,452✔

vbpf / ebpf-verifier / 11674460316

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