• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

vbpf / ebpf-verifier / 12845504567

18 Jan 2025 04:08PM UTC coverage: 88.169% (-1.5%) from 89.646%
12845504567

push

github

web-flow
Handle upgrade from LCOV 1.15 to LCOV 2.0 (#826)

* Testing code coverage with a comment only change
* Workaround for failing code coverage
* Testing code coverage fix

Signed-off-by: Alan Jowett <alanjo@microsoft.com>

8481 of 9619 relevant lines covered (88.17%)

7430805.79 hits per line

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

96.86
/src/assertions.cpp
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 "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<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
    ValidAccess make_valid_access(const Reg reg, const int32_t offset = {}, const Value& width = Imm{0},
49,900✔
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,900✔
33
        return ValidAccess{depth, reg, offset, width, or_null, access_type};
49,900✔
34
    }
35

36
  public:
37
    explicit AssertExtractor(program_info info, std::optional<label_t> label)
341,156✔
38
        : info{std::move(info)}, current_label(label) {}
341,156✔
39

40
    vector<Assertion> operator()(const Undefined&) const {
4,960✔
41
        // assert(false);
42
        return {};
4,960✔
43
    }
44

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

47
    vector<Assertion> operator()(const LoadMapFd&) const { return {}; }
12,482✔
48

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

52
    vector<Assertion> operator()(const Exit&) const {
1,490✔
53
        vector<Assertion> res;
1,490✔
54
        if (current_label->stack_frame_prefix.empty()) {
1,490✔
55
            // Verify that Exit returns a number.
56
            res.emplace_back(TypeConstraint{Reg{R0_RETURN_VALUE}, TypeGroup::number});
1,384✔
57
        }
58
        return res;
1,490✔
59
    }
×
60

61
    vector<Assertion> operator()(const Call& call) const {
19,838✔
62
        vector<Assertion> res;
19,838✔
63
        std::optional<Reg> map_fd_reg;
19,838✔
64
        res.emplace_back(ValidCall{call.func, call.stack_frame_prefix});
19,838✔
65
        for (ArgSingle arg : call.singles) {
66,588✔
66
            switch (arg.kind) {
46,750✔
67
            case ArgSingle::Kind::ANYTHING:
13,328✔
68
                // avoid pointer leakage:
69
                if (!info.type.is_privileged) {
13,328✔
70
                    res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});
13,146✔
71
                }
72
                break;
6,664✔
73
            case ArgSingle::Kind::MAP_FD_PROGRAMS:
346✔
74
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd_programs});
346✔
75
                // Do not update map_fd_reg
76
                break;
346✔
77
            case ArgSingle::Kind::MAP_FD:
12,114✔
78
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd});
12,114✔
79
                map_fd_reg = arg.reg;
35,489✔
80
                break;
6,057✔
81
            case ArgSingle::Kind::PTR_TO_MAP_KEY:
15,796✔
82
            case ArgSingle::Kind::PTR_TO_MAP_VALUE:
7,898✔
83
                assert(map_fd_reg);
15,796✔
84
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});
15,796✔
85
                res.emplace_back(ValidMapKeyValue{arg.reg, *map_fd_reg, arg.kind == ArgSingle::Kind::PTR_TO_MAP_KEY});
15,796✔
86
                break;
15,796✔
87
            case ArgSingle::Kind::PTR_TO_CTX:
5,166✔
88
                for (const Assertion& a : zero_offset_ctx(arg.reg)) {
15,498✔
89
                    res.emplace_back(a);
10,332✔
90
                }
5,166✔
91
                break;
5,166✔
92
            }
93
        }
94
        for (ArgPair arg : call.pairs) {
24,190✔
95
            res.emplace_back(TypeConstraint{arg.size, TypeGroup::number});
4,352✔
96
            res.emplace_back(ValidSize{arg.size, arg.can_be_zero});
4,352✔
97
            switch (arg.kind) {
4,352✔
98
            case ArgPair::Kind::PTR_TO_READABLE_MEM_OR_NULL:
1,012✔
99
                res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem_or_num});
1,012✔
100
                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, true, AccessType::read));
1,518✔
101
                break;
1,012✔
102
            case ArgPair::Kind::PTR_TO_READABLE_MEM:
2,470✔
103
                /* pointer to valid memory (stack, packet, map value) */
104
                res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem});
2,470✔
105
                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::read));
3,702✔
106
                break;
2,470✔
107
            case ArgPair::Kind::PTR_TO_WRITABLE_MEM:
870✔
108
                // memory may be uninitialized, i.e. write only
109
                res.emplace_back(TypeConstraint{arg.mem, TypeGroup::mem});
870✔
110
                res.emplace_back(make_valid_access(arg.mem, 0, arg.size, false, AccessType::write));
1,302✔
111
                break;
870✔
112
            }
113
            // TODO: reg is constant (or maybe it's not important)
114
        }
115
        return res;
29,757✔
116
    }
×
117

118
    vector<Assertion> operator()(const CallLocal&) const { return {}; }
106✔
119

120
    vector<Assertion> operator()(const Callx& callx) const {
50✔
121
        vector<Assertion> res;
50✔
122
        res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});
50✔
123
        res.emplace_back(FuncConstraint{callx.func});
50✔
124
        return res;
50✔
125
    }
×
126

127
    [[nodiscard]]
128
    vector<Assertion> explicate(const Condition& cond) const {
25,582✔
129
        if (info.type.is_privileged) {
25,582✔
130
            return {};
164✔
131
        }
132
        vector<Assertion> res;
25,418✔
133
        if (const auto pimm = std::get_if<Imm>(&cond.right)) {
25,418✔
134
            if (pimm->v != 0) {
20,300✔
135
                // no need to check for valid access, it must be a number
136
                res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});
6,314✔
137
            } else {
138
                bool allow_pointers = false;
13,986✔
139

140
                switch (cond.op) {
13,986✔
141
                case Condition::Op::EQ: allow_pointers = true; break;
9,547✔
142
                case Condition::Op::NE: allow_pointers = true; break;
9,552✔
143
                case Condition::Op::SET: allow_pointers = true; break;
6,381✔
144
                case Condition::Op::NSET: allow_pointers = true; break;
6,381✔
145
                case Condition::Op::LT: allow_pointers = true; break;
6,394✔
146
                case Condition::Op::LE: allow_pointers = true; break;
6,381✔
147
                case Condition::Op::GT: allow_pointers = true; break;
6,393✔
148
                case Condition::Op::GE: allow_pointers = true; break;
6,382✔
149
                case Condition::Op::SLT: allow_pointers = false; break;
590✔
150
                case Condition::Op::SLE: allow_pointers = false; break;
3✔
151
                case Condition::Op::SGT: allow_pointers = false; break;
17✔
152
                case Condition::Op::SGE: allow_pointers = false; break;
4✔
153
                default: assert(!"unexpected condition");
6,993✔
154
                }
155

156
                // Only permit pointer comparisons if the operation is 64-bit.
157
                allow_pointers &= cond.is64;
13,986✔
158

159
                if (!allow_pointers) {
13,986✔
160
                    res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});
7,290✔
161
                }
162

163
                res.emplace_back(make_valid_access(cond.left));
20,979✔
164
                // OK - map_fd is just another pointer
165
                // Anything can be compared to 0
166
            }
167
        } else {
168
            const auto reg_right = get<Reg>(cond.right);
5,118✔
169
            res.emplace_back(make_valid_access(cond.left));
7,677✔
170
            res.emplace_back(make_valid_access(reg_right));
7,677✔
171
            if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {
5,118✔
172
                res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});
3,738✔
173
            }
174
            res.emplace_back(Comparable{.r1 = cond.left, .r2 = reg_right, .or_r2_is_number = false});
5,118✔
175
        }
176
        return res;
25,418✔
177
    }
25,418✔
178

179
    vector<Assertion> operator()(const Assume& ins) const {
50,802✔
180
        if (!ins.is_implicit) {
50,802✔
181
            return explicate(ins.cond);
350✔
182
        }
183
        return {};
50,452✔
184
    }
185

186
    vector<Assertion> operator()(const Jmp& ins) const {
29,740✔
187
        if (!ins.cond) {
29,740✔
188
            return {};
4,508✔
189
        }
190
        return explicate(*ins.cond);
25,232✔
191
    }
192

193
    vector<Assertion> operator()(const Mem& ins) const {
64,726✔
194
        vector<Assertion> res;
64,726✔
195
        const Reg basereg = ins.access.basereg;
64,726✔
196
        Imm width{gsl::narrow<uint32_t>(ins.access.width)};
64,726✔
197
        const int offset = ins.access.offset;
64,726✔
198
        if (basereg.v == R10_STACK_POINTER) {
64,726✔
199
            // We know we are accessing the stack.
200
            if (offset < -EBPF_SUBPROGRAM_STACK_SIZE || offset + static_cast<int>(width.v) > 0) {
43,812✔
201
                // This assertion will fail
202
                res.emplace_back(make_valid_access(basereg, offset, width, false,
3✔
203
                                                   ins.is_load ? AccessType::read : AccessType::write));
2✔
204
            } else if (ins.is_load) {
205
                // This assertion is not for bound checks but for reading initialized memory.
206
                // TODO: avoid load assertions: use post-assertion to check that the loaded value is initialized
207
                // res.emplace_back(make_valid_access(basereg, offset, width, false, AccessType::read));
208
            }
209
        } else {
210
            res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer});
20,914✔
211
            res.emplace_back(
31,371✔
212
                make_valid_access(basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write));
34,232✔
213
            if (!info.type.is_privileged && !ins.is_load) {
20,914✔
214
                if (const auto preg = std::get_if<Reg>(&ins.value)) {
5,708✔
215
                    if (width.v != 8) {
5,698✔
216
                        res.emplace_back(TypeConstraint{*preg, TypeGroup::number});
4,904✔
217
                    } else {
218
                        res.emplace_back(ValidStore{ins.access.basereg, *preg});
794✔
219
                    }
220
                }
221
            }
222
        }
223
        return res;
97,089✔
224
    }
×
225

226
    vector<Assertion> operator()(const Atomic& ins) const {
410✔
227

228
        return {
205✔
229
            Assertion{TypeConstraint{ins.valreg, TypeGroup::number}},
205✔
230
            Assertion{TypeConstraint{ins.access.basereg, TypeGroup::pointer}},
205✔
231
            Assertion{make_valid_access(ins.access.basereg, ins.access.offset,
615✔
232
                                        Imm{static_cast<uint32_t>(ins.access.width)}, false)},
205✔
233
        };
1,845✔
234
    }
820✔
235

236
    vector<Assertion> operator()(const Un& ins) const {
2,956✔
237
        return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
7,390✔
238
    }
2,956✔
239

240
    vector<Assertion> operator()(const Bin& ins) const {
153,328✔
241
        switch (ins.op) {
153,328✔
242
        case Bin::Op::MOV:
88,626✔
243
            if (const auto src = std::get_if<Reg>(&ins.v)) {
88,626✔
244
                if (!ins.is64) {
48,832✔
245
                    return {Assertion{TypeConstraint{*src, TypeGroup::number}}};
29,340✔
246
                }
247
            }
248
            return {};
76,890✔
249
        case Bin::Op::MOVSX8:
2,262✔
250
        case Bin::Op::MOVSX16:
1,131✔
251
        case Bin::Op::MOVSX32:
1,131✔
252
            if (const auto src = std::get_if<Reg>(&ins.v)) {
2,262✔
253
                return {Assertion{TypeConstraint{*src, TypeGroup::number}}};
5,655✔
254
            }
255
            return {};
×
256
        case Bin::Op::ADD: {
30,188✔
257
            if (const auto src = std::get_if<Reg>(&ins.v)) {
30,188✔
258
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}},
2,454✔
259
                        Assertion{TypeConstraint{*src, TypeGroup::ptr_or_num}}, Assertion{Addable{*src, ins.dst}},
2,454✔
260
                        Assertion{Addable{ins.dst, *src}}};
26,994✔
261
            }
262
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};
63,200✔
263
        }
264
        case Bin::Op::SUB: {
808✔
265
            if (const auto reg = std::get_if<Reg>(&ins.v)) {
808✔
266
                vector<Assertion> res;
780✔
267
                // disallow map-map since same type does not mean same offset
268
                // TODO: map identities
269
                res.emplace_back(TypeConstraint{ins.dst, TypeGroup::ptr_or_num});
780✔
270
                res.emplace_back(Comparable{.r1 = ins.dst, .r2 = *reg, .or_r2_is_number = true});
780✔
271
                return res;
780✔
272
            }
780✔
273
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};
70✔
274
        }
275
        case Bin::Op::UDIV:
2,498✔
276
        case Bin::Op::UMOD:
1,249✔
277
        case Bin::Op::SDIV:
1,249✔
278
        case Bin::Op::SMOD: {
1,249✔
279
            if (const auto src = std::get_if<Reg>(&ins.v)) {
2,498✔
280
                const bool is_signed = (ins.op == Bin::Op::SDIV || ins.op == Bin::Op::SMOD);
220✔
281
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},
110✔
282
                        Assertion{ValidDivisor{*src, is_signed}}};
770✔
283
            }
284
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
5,695✔
285
        }
286
        // For all other binary operations, the destination register must be a number and the source must either be an
287
        // immediate or a number.
288
        default:
28,946✔
289
            if (const auto src = std::get_if<Reg>(&ins.v)) {
28,946✔
290
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},
3,765✔
291
                        Assertion{TypeConstraint{*src, TypeGroup::number}}};
26,355✔
292
            } else {
293
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
53,540✔
294
            }
295
        }
296
        assert(false);
297
    }
75,658✔
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
vector<Assertion> get_assertions(Instruction ins, const program_info& info, const std::optional<label_t>& label) {
341,156✔
306
    return std::visit(AssertExtractor{info, label}, ins);
682,290✔
307
}
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2026 Coveralls, Inc