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

Alan-Jowett / ebpf-verifier / 21966302480

12 Feb 2026 10:13PM UTC coverage: 87.366% (+0.6%) from 86.783%
21966302480

Pull #161

github

web-flow
Merge 4c3f51414 into f1f1d42d7
Pull Request #161: Failure slice

518 of 660 new or added lines in 8 files covered. (78.48%)

9 existing lines in 2 files now uncovered.

10013 of 11461 relevant lines covered (87.37%)

2950767.02 hits per line

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

78.15
/src/result.cpp
1
// Copyright (c) Prevail Verifier contributors.
2
// SPDX-License-Identifier: MIT
3
#include <algorithm>
4
#include <map>
5
#include <ranges>
6
#include <regex>
7
#include <sstream>
8

9
#include "crab/ebpf_domain.hpp"
10
#include "ir/program.hpp"
11
#include "result.hpp"
12
#include "spec/ebpf_base.h"
13
#include "spec/vm_isa.hpp"
14

15
namespace prevail {
16

17
// Stream-local storage index for invariant filter
18
static int invariant_filter_index() {
24✔
19
    static const int index = std::ios_base::xalloc();
24✔
20
    return index;
24✔
21
}
22

23
const RelevantState* get_invariant_filter(std::ostream& os) {
12✔
24
    return static_cast<const RelevantState*>(os.pword(invariant_filter_index()));
12✔
25
}
26

27
std::ostream& operator<<(std::ostream& os, const invariant_filter& filter) {
12✔
28
    os.pword(invariant_filter_index()) = const_cast<void*>(static_cast<const void*>(filter.state));
12✔
29
    return os;
12✔
30
}
31

32
bool RelevantState::is_relevant_constraint(const std::string& constraint) const {
86✔
33
    // Extract the register or stack reference from the constraint
34
    // Constraints look like: "r1.type=number", "r2.svalue=[0, 100]", "s[4088...4095].type=ctx"
35
    // Relational constraints: "r1.svalue-r8.svalue<=-100", "r0.svalue=r3.svalue+2"
36
    // Also handle: "packet_size=54", "meta_offset=[-4098, 0]"
37

38
    // Check for ANY register mentioned in the constraint (not just at start)
39
    // This handles relational constraints like "r1.svalue-r8.svalue<=100"
40
    static const std::regex reg_pattern(R"(r(\d+)\.)");
86✔
41
    std::sregex_iterator it(constraint.begin(), constraint.end(), reg_pattern);
86✔
42
    std::sregex_iterator end;
86✔
43

44
    bool found_any_register = false;
86✔
45
    while (it != end) {
140✔
46
        found_any_register = true;
64✔
47
        const uint8_t reg_num = static_cast<uint8_t>(std::stoi((*it)[1].str()));
96✔
48
        if (registers.contains(Reg{reg_num})) {
64✔
49
            return true; // At least one relevant register is mentioned
5✔
50
        }
51
        ++it;
54✔
52
    }
53

54
    // If we found registers but none were relevant, skip this constraint
55
    if (found_any_register) {
76✔
56
        return false;
26✔
57
    }
58

59
    // Precompute absolute stack offsets once to avoid repeated conversion in loops
60
    std::vector<int64_t> abs_stack_offsets;
24✔
61
    abs_stack_offsets.reserve(stack_offsets.size());
24✔
62
    for (const auto& rel_offset : stack_offsets) {
24✔
NEW
63
        abs_stack_offsets.push_back(EBPF_TOTAL_STACK_SIZE + rel_offset);
×
64
    }
65

66
    // Check for stack range pattern: s[start...end]
67
    static const std::regex stack_range_pattern(R"(s\[(\d+)\.\.\.(\d+)\])");
24✔
68
    std::sregex_iterator stack_it(constraint.begin(), constraint.end(), stack_range_pattern);
24✔
69
    while (stack_it != end) {
36✔
70
        // Stack offsets in constraints are absolute (e.g., 4088...4095)
71
        // Our stack_offsets are relative to R10 (e.g., -8)
72
        const int64_t abs_start = std::stoll((*stack_it)[1].str());
18✔
73
        const int64_t abs_end = std::stoll((*stack_it)[2].str());
18✔
74
        for (const auto& abs_offset : abs_stack_offsets) {
12✔
NEW
75
            if (abs_offset >= abs_start && abs_offset <= abs_end) {
×
76
                return true; // Overlaps within the constraint range
12✔
77
            }
78
        }
79
        ++stack_it;
12✔
80
    }
81

82
    // Check for single-offset stack pattern: s[offset]
83
    static const std::regex stack_single_pattern(R"(s\[(\d+)\]\.)");
24✔
84
    std::sregex_iterator single_it(constraint.begin(), constraint.end(), stack_single_pattern);
24✔
85
    while (single_it != end) {
24✔
NEW
86
        const int64_t abs_pos = std::stoll((*single_it)[1].str());
×
NEW
87
        for (const auto& abs_offset : abs_stack_offsets) {
×
NEW
88
            if (abs_offset == abs_pos) {
×
89
                return true;
12✔
90
            }
91
        }
NEW
92
        ++single_it;
×
93
    }
94

95
    // Global constraints (packet_size, meta_offset) - always show for context
96
    if (constraint.starts_with("packet_size") || constraint.starts_with("meta_offset")) {
33✔
97
        return true;
9✔
98
    }
99

100
    // If we can't parse it, show it (conservative)
101
    return true;
6✔
102
}
110✔
103

UNCOV
104
bool AnalysisResult::is_valid_after(const Label& label, const StringInvariant& state) const {
×
105
    const EbpfDomain abstract_state =
106
        EbpfDomain::from_constraints(state.value(), thread_local_options.setup_constraints);
×
107
    return abstract_state <= invariants.at(label).post;
×
108
}
×
109

110
ObservationCheckResult AnalysisResult::check_observation_at_label(const Label& label, const InvariantPoint point,
12✔
111
                                                                  const StringInvariant& observation,
112
                                                                  const ObservationCheckMode mode) const {
113
    const auto it = invariants.find(label);
12✔
114
    if (it == invariants.end()) {
12✔
115
        return {.ok = false, .message = "No invariant available for label " + to_string(label)};
×
116
    }
117
    const auto& inv_pair = it->second;
12✔
118
    const EbpfDomain& abstract_state = (point == InvariantPoint::pre) ? inv_pair.pre : inv_pair.post;
12✔
119

120
    const EbpfDomain observed_state =
6✔
121
        observation.is_bottom()
12✔
122
            ? EbpfDomain::bottom()
12✔
123
            : EbpfDomain::from_constraints(observation.value(), thread_local_options.setup_constraints);
12✔
124

125
    if (observed_state.is_bottom()) {
12✔
126
        return {.ok = false, .message = "Observation constraints are unsatisfiable (domain is bottom)"};
2✔
127
    }
128

129
    if (abstract_state.is_bottom()) {
10✔
130
        return {.ok = false, .message = "Invariant at label is bottom (unreachable)"};
×
131
    }
132

133
    switch (mode) {
10✔
134
    case ObservationCheckMode::entailed:
4✔
135
        if (observed_state <= abstract_state) {
4✔
136
            return {.ok = true, .message = ""};
2✔
137
        }
138
        return {.ok = false, .message = "Invariant does not entail the observation (C ⊑ A is false)"};
2✔
139

140
    case ObservationCheckMode::consistent:
6✔
141
        // Default: consistency / satisfiability.
142
        if ((abstract_state & observed_state).is_bottom()) {
9✔
143
            return {.ok = false, .message = "Observation contradicts invariant (meet is bottom)"};
×
144
        }
145
        return {.ok = true, .message = ""};
6✔
146
    }
147

148
    return {.ok = false, .message = "Unsupported observation check mode"};
×
149
}
30✔
150

151
bool AnalysisResult::is_consistent_before(const Label& label, const StringInvariant& observation) const {
×
152
    return check_observation_at_label(label, InvariantPoint::pre, observation, ObservationCheckMode::consistent).ok;
×
153
}
154

155
bool AnalysisResult::is_consistent_after(const Label& label, const StringInvariant& observation) const {
×
156
    return check_observation_at_label(label, InvariantPoint::post, observation, ObservationCheckMode::consistent).ok;
×
157
}
158

159
StringInvariant AnalysisResult::invariant_at(const Label& label) const { return invariants.at(label).post.to_set(); }
1,400✔
160

161
std::optional<VerificationError> AnalysisResult::find_first_error() const {
1,400✔
162
    for (const auto& inv_pair : invariants | std::views::values) {
5,952✔
163
        if (inv_pair.pre.is_bottom()) {
4,866✔
164
            continue;
330✔
165
        }
166
        if (inv_pair.error) {
4,536✔
167
            return inv_pair.error;
314✔
168
        }
169
    }
170
    return {};
1,086✔
171
}
172

173
std::map<Label, std::vector<std::string>> AnalysisResult::find_unreachable(const Program& prog) const {
1,400✔
174
    std::map<Label, std::vector<std::string>> unreachable;
1,400✔
175
    for (const auto& [label, inv_pair] : invariants) {
6,828✔
176
        if (inv_pair.pre.is_bottom()) {
5,428✔
177
            continue;
810✔
178
        }
179
        if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {
7,332✔
180
            if (inv_pair.post.is_bottom() && !inv_pair.error) {
556✔
181
                const auto s = to_string(*passume);
182✔
182
                unreachable[label].emplace_back(to_string(label) + ": Code becomes unreachable (" + s + ")");
455✔
183
            }
182✔
184
        }
185
    }
186
    return unreachable;
1,400✔
187
}
×
188

189
/// Extract the registers and stack offsets read/written by an instruction.
190
/// Used to populate InstructionDeps during forward analysis.
191
InstructionDeps extract_instruction_deps(const Instruction& ins, const EbpfDomain& pre_state) {
460✔
192
    InstructionDeps deps;
460✔
193

194
    std::visit(
460✔
195
        [&](const auto& v) {
889✔
196
            using T = std::decay_t<decltype(v)>;
197

198
            if constexpr (std::is_same_v<T, Bin>) {
199
                // dst = dst op src (or dst = src for MOV)
200
                deps.regs_written.insert(v.dst);
152✔
201
                if (v.op != Bin::Op::MOV) {
152✔
202
                    // Non-MOV ops also read dst
203
                    deps.regs_read.insert(v.dst);
64✔
204
                }
205
                if (const auto* reg = std::get_if<Reg>(&v.v)) {
152✔
206
                    deps.regs_read.insert(*reg);
64✔
207
                }
208
            } else if constexpr (std::is_same_v<T, Un>) {
209
                // dst = op(dst)
NEW
210
                deps.regs_read.insert(v.dst);
×
NEW
211
                deps.regs_written.insert(v.dst);
×
212
            } else if constexpr (std::is_same_v<T, LoadMapFd> || std::is_same_v<T, LoadMapAddress>) {
213
                deps.regs_written.insert(v.dst);
20✔
214
            } else if constexpr (std::is_same_v<T, Mem>) {
215
                deps.regs_read.insert(v.access.basereg);
124✔
216
                if (v.is_load) {
124✔
217
                    // Load: value = *(basereg + offset)
218
                    if (const auto* dst_reg = std::get_if<Reg>(&v.value)) {
22✔
219
                        deps.regs_written.insert(*dst_reg);
22✔
220
                    }
221
                    // Track stack read if base is a stack pointer (R10 or derived)
222
                    if (v.access.basereg.v == R10_STACK_POINTER) {
22✔
223
                        deps.stack_read.insert(v.access.offset);
2✔
224
                    } else if (const auto stack_off = pre_state.get_stack_offset(v.access.basereg)) {
20✔
225
                        // basereg is a stack pointer with known offset from R10
226
                        // Compute the actual stack slot: stack_off is absolute (e.g., 4096),
227
                        // convert to relative from R10: relative = offset + (stack_off - EBPF_TOTAL_STACK_SIZE)
NEW
228
                        deps.stack_read.insert(v.access.offset + (*stack_off - EBPF_TOTAL_STACK_SIZE));
×
229
                    }
230
                } else {
231
                    // Store: *(basereg + offset) = value
232
                    if (const auto* src_reg = std::get_if<Reg>(&v.value)) {
102✔
233
                        deps.regs_read.insert(*src_reg);
102✔
234
                    }
235
                    // Track stack write if base is a stack pointer (R10 or derived)
236
                    if (v.access.basereg.v == R10_STACK_POINTER) {
102✔
237
                        deps.stack_written.insert(v.access.offset);
88✔
238
                    } else if (const auto stack_off = pre_state.get_stack_offset(v.access.basereg)) {
14✔
NEW
239
                        deps.stack_written.insert(v.access.offset + (*stack_off - EBPF_TOTAL_STACK_SIZE));
×
240
                    }
241
                }
242
            } else if constexpr (std::is_same_v<T, Atomic>) {
NEW
243
                deps.regs_read.insert(v.access.basereg);
×
NEW
244
                deps.regs_read.insert(v.valreg);
×
NEW
245
                if (v.fetch) {
×
NEW
246
                    deps.regs_written.insert(v.valreg);
×
247
                }
248
                // Track stack read/write if base is a stack pointer (R10 or derived)
NEW
249
                if (v.access.basereg.v == R10_STACK_POINTER) {
×
NEW
250
                    deps.stack_read.insert(v.access.offset);
×
NEW
251
                    deps.stack_written.insert(v.access.offset);
×
NEW
252
                } else if (const auto stack_off = pre_state.get_stack_offset(v.access.basereg)) {
×
NEW
253
                    const auto adjusted_off = v.access.offset + (*stack_off - EBPF_TOTAL_STACK_SIZE);
×
NEW
254
                    deps.stack_read.insert(adjusted_off);
×
NEW
255
                    deps.stack_written.insert(adjusted_off);
×
256
                }
257
            } else if constexpr (std::is_same_v<T, Call>) {
258
                // Calls read R1-R5 as arguments, write R0 as return value,
259
                // and clobber R1-R5 (caller-saved registers are killed).
260
                // Separate clobbers from writes so backward slicing can:
261
                // - Stop propagation for post-call uses of R1-R5 (they're killed)
262
                // - Still trace R1-R5 as read-deps when R0 is relevant-after (args affect return)
263
                for (uint8_t i = 1; i <= 5; ++i) {
132✔
264
                    deps.regs_read.insert(Reg{i});      // Arguments feed into return value
110✔
265
                    deps.regs_clobbered.insert(Reg{i}); // Killed after call
110✔
266
                }
267
                deps.regs_written.insert(Reg{0}); // Return value
22✔
268
            } else if constexpr (std::is_same_v<T, CallLocal>) {
269
                // Local (macro-inlined) calls:
270
                // - read R1-R5 as arguments
271
                // - write R0 as return value
272
                // - clobber R1-R5 (caller-saved)
273
                // - adjust frame pointer R10 (save/restore callee-saved regs)
NEW
274
                for (uint8_t i = 1; i <= 5; ++i) {
×
NEW
275
                    deps.regs_read.insert(Reg{i});      // Arguments
×
NEW
276
                    deps.regs_clobbered.insert(Reg{i}); // Killed after call
×
277
                }
NEW
278
                deps.regs_written.insert(Reg{0});  // Return value
×
NEW
279
                deps.regs_read.insert(Reg{10});    // Frame pointer read
×
NEW
280
                deps.regs_written.insert(Reg{10}); // Frame pointer adjusted
×
281
            } else if constexpr (std::is_same_v<T, Callx>) {
282
                // Indirect call: reads the function pointer and R1-R5,
283
                // writes R0, and clobbers R1-R5.
NEW
284
                deps.regs_read.insert(v.func);
×
NEW
285
                for (uint8_t i = 1; i <= 5; ++i) {
×
NEW
286
                    deps.regs_read.insert(Reg{i});      // Arguments
×
NEW
287
                    deps.regs_clobbered.insert(Reg{i}); // Killed after call
×
288
                }
NEW
289
                deps.regs_written.insert(Reg{0});
×
290
            } else if constexpr (std::is_same_v<T, Exit>) {
291
                deps.regs_read.insert(Reg{0}); // Return value
14✔
292
            } else if constexpr (std::is_same_v<T, Jmp>) {
293
                if (v.cond) {
46✔
294
                    deps.regs_read.insert(v.cond->left);
32✔
295
                    if (const auto* reg = std::get_if<Reg>(&v.cond->right)) {
32✔
296
                        deps.regs_read.insert(*reg);
2✔
297
                    }
298
                }
299
            } else if constexpr (std::is_same_v<T, Assume>) {
300
                deps.regs_read.insert(v.cond.left);
54✔
301
                if (const auto* reg = std::get_if<Reg>(&v.cond.right)) {
54✔
302
                    deps.regs_read.insert(*reg);
4✔
303
                }
304
            } else if constexpr (std::is_same_v<T, Packet>) {
NEW
305
                if (v.regoffset) {
×
NEW
306
                    deps.regs_read.insert(*v.regoffset);
×
307
                }
NEW
308
                deps.regs_written.insert(Reg{0}); // Result in R0
×
309
                // Packet also clobbers caller-saved registers R1-R5
NEW
310
                for (uint8_t i = 1; i <= 5; ++i) {
×
NEW
311
                    deps.regs_written.insert(Reg{i});
×
312
                }
313
            }
314
            // Undefined and IncrementLoopCounter have no register deps
315
        },
429✔
316
        ins);
317

318
    return deps;
460✔
NEW
319
}
×
320

321
/// Extract the registers referenced by an assertion.
322
/// Used to seed backward slicing from the point of failure.
323
std::set<Reg> extract_assertion_registers(const Assertion& assertion) {
32✔
324
    return std::visit(
16✔
325
        [](const auto& a) -> std::set<Reg> {
64✔
326
            using T = std::decay_t<decltype(a)>;
327

328
            if constexpr (std::is_same_v<T, Comparable>) {
329
                return {a.r1, a.r2};
4✔
330
            } else if constexpr (std::is_same_v<T, Addable>) {
NEW
331
                return {a.ptr, a.num};
×
332
            } else if constexpr (std::is_same_v<T, ValidDivisor>) {
333
                return {a.reg};
4✔
334
            } else if constexpr (std::is_same_v<T, ValidAccess>) {
335
                std::set<Reg> regs{a.reg};
3✔
336
                if (const auto* r = std::get_if<Reg>(&a.width)) {
2✔
NEW
337
                    regs.insert(*r);
×
338
                }
339
                return regs;
2✔
340
            } else if constexpr (std::is_same_v<T, ValidStore>) {
2✔
NEW
341
                return {a.mem, a.val};
×
342
            } else if constexpr (std::is_same_v<T, ValidSize>) {
NEW
343
                return {a.reg};
×
344
            } else if constexpr (std::is_same_v<T, ValidMapKeyValue>) {
345
                return {a.access_reg, a.map_fd_reg};
8✔
346
            } else if constexpr (std::is_same_v<T, ValidCall>) {
347
                // ValidCall checks function validity, no direct register deps
348
                return {};
4✔
349
            } else if constexpr (std::is_same_v<T, TypeConstraint>) {
350
                return {a.reg};
36✔
351
            } else if constexpr (std::is_same_v<T, FuncConstraint>) {
NEW
352
                return {a.reg};
×
353
            } else if constexpr (std::is_same_v<T, ZeroCtxOffset>) {
NEW
354
                return {a.reg};
×
355
            } else if constexpr (std::is_same_v<T, BoundedLoopCount>) {
356
                // Loop counter, not a register
NEW
357
                return {};
×
358
            }
359
            return {};
360
        },
361
        assertion);
36✔
362
}
363

364
std::vector<FailureSlice> AnalysisResult::compute_failure_slices(const Program& prog, const size_t max_steps,
14✔
365
                                                                 const size_t max_slices) const {
366
    std::vector<FailureSlice> slices;
14✔
367

368
    // Find all labels with errors
369
    for (const auto& [label, inv_pair] : invariants) {
296✔
370
        if (inv_pair.pre.is_bottom()) {
282✔
371
            continue; // Unreachable
272✔
372
        }
373
        if (!inv_pair.error) {
232✔
374
            continue; // No error here
222✔
375
        }
376

377
        // Check if we've reached the max slices limit
378
        if (max_slices > 0 && slices.size() >= max_slices) {
10✔
379
            break;
380
        }
381

382
        FailureSlice slice{
5✔
383
            .failing_label = label,
384
            .error = *inv_pair.error,
385
            .relevance = {},
386
        };
10✔
387

388
        // Seed relevant registers from the failed assertion.
389
        // Forward analysis records only the first assertion that fails at this label,
390
        // so we prefer to seed relevance from that single assertion to keep slices tight.
391
        // However, if the first assertion has no register dependencies, we fallback
392
        // to all assertions at this label to ensure we produce a usable slice.
393
        RelevantState initial_relevance;
10✔
394
        const auto& assertions = prog.assertions_at(label);
10✔
395
        if (!assertions.empty()) {
10✔
396
            // Try the first assertion (the failing one)
397
            for (const auto& reg : extract_assertion_registers(assertions[0])) {
18✔
398
                initial_relevance.registers.insert(reg);
8✔
399
            }
5✔
400
            // If first assertion has no registers, fallback to all assertions
401
            if (initial_relevance.registers.empty()) {
10✔
402
                for (const auto& assertion : assertions) {
16✔
403
                    for (const auto& reg : extract_assertion_registers(assertion)) {
30✔
404
                        initial_relevance.registers.insert(reg);
16✔
405
                    }
14✔
406
                }
407
            }
408
        }
409

410
        // Always include the failing label in the slice, even if no registers were extracted
411
        // (e.g., ValidCall, BoundedLoopCount assertions have no register deps)
412

413
        // `visited` tracks all explored labels for deduplication during backward traversal.
414
        // `slice_labels` tracks only labels that interact with relevant registers (the output slice).
415
        std::map<Label, RelevantState> visited;
10✔
416
        std::set<Label> conservative_visited; // Dedup for empty-relevance labels in conservative mode
10✔
417
        std::map<Label, RelevantState> slice_labels;
10✔
418

419
        // Worklist: (label, relevant_state_after_this_label)
420
        std::vector<std::pair<Label, RelevantState>> worklist;
10✔
421
        worklist.emplace_back(label, initial_relevance);
10✔
422

423
        // When the seed has no register/stack deps (e.g., BoundedLoopCount),
424
        // perform a conservative backward walk so the slice still shows the
425
        // loop structure and control flow leading to the failure.
426
        const bool conservative_mode = initial_relevance.registers.empty() && initial_relevance.stack_offsets.empty();
10✔
427

428
        size_t steps = 0;
10✔
429

430
        while (!worklist.empty() && steps < max_steps) {
108✔
431
            auto [current_label, relevant_after] = worklist.back();
98✔
432
            worklist.pop_back();
98✔
433

434
            // Skip if nothing is relevant — unless we're in conservative mode
435
            // (empty-seed assertions like BoundedLoopCount) or this is the failing label.
436
            if (!conservative_mode && current_label != label && relevant_after.registers.empty() &&
100✔
437
                relevant_after.stack_offsets.empty()) {
4✔
438
                continue;
4✔
439
            }
440

441
            // Merge with existing relevance at this label (for deduplication)
442
            auto& existing = visited[current_label];
94✔
443
            const size_t prev_size = existing.registers.size() + existing.stack_offsets.size();
94✔
444
            existing.registers.insert(relevant_after.registers.begin(), relevant_after.registers.end());
94✔
445
            existing.stack_offsets.insert(relevant_after.stack_offsets.begin(), relevant_after.stack_offsets.end());
94✔
446
            const size_t new_size = existing.registers.size() + existing.stack_offsets.size();
94✔
447

448
            // If no new relevance was added, skip (already processed with same or broader relevance).
449
            // In conservative mode with empty relevance, use a separate visited set for dedup.
450
            if (new_size == prev_size) {
94✔
451
                if (prev_size > 0) {
2✔
452
                    continue;
2✔
453
                }
454
                // Empty relevance (conservative mode): skip if we already visited this label
NEW
455
                if (!conservative_visited.insert(current_label).second) {
×
NEW
456
                    continue;
×
457
                }
458
            }
459

460
            // Compute what's relevant BEFORE this instruction using deps
461
            RelevantState relevant_before;
92✔
462
            const auto inv_it = invariants.find(current_label);
92✔
463
            if (inv_it != invariants.end() && inv_it->second.deps) {
92✔
464
                const auto& deps = *inv_it->second.deps;
92✔
465

466
                // Start with what's relevant after
467
                relevant_before = relevant_after;
92✔
468

469
                // Remove registers that are written by this instruction
470
                // (they weren't relevant before their definition)
471
                for (const auto& reg : deps.regs_written) {
158✔
472
                    relevant_before.registers.erase(reg);
66✔
473
                }
474

475
                // Remove registers that are clobbered (killed without reading).
476
                // These stop propagation for post-instruction uses but don't add read-deps.
477
                for (const auto& reg : deps.regs_clobbered) {
112✔
478
                    relevant_before.registers.erase(reg);
20✔
479
                }
480

481
                // Determine if this instruction contributes to the slice.
482
                // An instruction contributes when it writes to a relevant register/stack slot,
483
                // or when it is a control-flow decision (Jmp/Assume) that reads relevant registers.
484
                bool instruction_contributes = false;
92✔
485
                for (const auto& reg : deps.regs_written) {
112✔
486
                    if (relevant_after.registers.contains(reg)) {
66✔
487
                        instruction_contributes = true;
23✔
488
                        break;
23✔
489
                    }
490
                }
491
                for (const auto& offset : deps.stack_written) {
98✔
492
                    if (relevant_after.stack_offsets.contains(offset)) {
6✔
493
                        instruction_contributes = true;
494
                        break;
495
                    }
496
                }
497

498
                // Control-flow instructions (Jmp/Assume) that read relevant registers
499
                // contribute to the slice because they shape the path to the failure.
500
                if (!instruction_contributes) {
92✔
501
                    const auto& ins = prog.instruction_at(current_label);
46✔
502
                    if (std::holds_alternative<Jmp>(ins) || std::holds_alternative<Assume>(ins)) {
46✔
503
                        for (const auto& reg : deps.regs_read) {
30✔
504
                            if (relevant_after.registers.contains(reg)) {
20✔
505
                                instruction_contributes = true;
1✔
506
                                break;
1✔
507
                            }
508
                        }
509
                    }
510
                }
511

512
                // Immediate path guard: when the current label is a direct predecessor
513
                // of the failing label and is an Assume instruction, its condition
514
                // registers are causally relevant — they determine reachability.
515
                if (std::holds_alternative<Assume>(prog.instruction_at(current_label))) {
92✔
516
                    const auto& parents_of_fail = prog.cfg().parents_of(label);
6✔
517
                    if (std::find(parents_of_fail.begin(), parents_of_fail.end(), current_label) !=
6✔
518
                        parents_of_fail.end()) {
9✔
519
                        instruction_contributes = true;
47✔
520
                    }
521
                }
522

523
                // At the failing label, the assertion depends on registers the instruction
524
                // reads (e.g., base pointer r3 in a store). Since stores write to memory
525
                // not registers, instruction_contributes would be false without this.
526
                if (current_label == label) {
92✔
527
                    instruction_contributes = true;
10✔
528
                }
529

530
                // In conservative mode (empty seed, e.g., BoundedLoopCount), include all
531
                // reachable labels so the slice shows the loop structure and control flow.
532
                if (conservative_mode) {
92✔
533
                    instruction_contributes = true;
534
                }
535

536
                if (instruction_contributes) {
92✔
537
                    for (const auto& reg : deps.regs_read) {
114✔
538
                        relevant_before.registers.insert(reg);
58✔
539
                    }
540
                    for (const auto& offset : deps.stack_read) {
56✔
NEW
541
                        relevant_before.stack_offsets.insert(offset);
×
542
                    }
543
                    // Only include contributing labels in the output slice.
544
                    // Store relevant_before so pre-invariant filtering shows the
545
                    // instruction's read-deps (the true upstream dependencies).
546
                    slice_labels[current_label] = relevant_before;
56✔
547
                }
548

549
                // Remove stack locations that are written by this instruction,
550
                // but preserve offsets that are also read (read-modify-write, e.g., Atomic)
551
                for (const auto& offset : deps.stack_written) {
98✔
552
                    if (!deps.stack_read.contains(offset)) {
6✔
553
                        relevant_before.stack_offsets.erase(offset);
6✔
554
                    }
555
                }
556
            } else {
557
                // No deps available: conservatively treat this label as contributing
558
                // and propagate all current relevance to predecessors.
NEW
559
                relevant_before = relevant_after;
×
NEW
560
                slice_labels[current_label] = relevant_before;
×
561
            }
562

563
            // Add predecessors to worklist
564
            for (const auto& parent : prog.cfg().parents_of(current_label)) {
180✔
565
                worklist.emplace_back(parent, relevant_before);
88✔
566
            }
567

568
            ++steps;
92✔
569
        }
98✔
570

571
        // Expand join points: for any traversed label that is a join point
572
        // (≥2 predecessors) where at least one predecessor is already in the slice,
573
        // add the join-point label itself and all predecessors that have invariants.
574
        // This ensures the causal trace shows converging paths that cause precision loss.
575
        // Note: predecessors may not be in `visited` if the worklist budget was exhausted
576
        // before reaching them, so we check the invariant map directly.
577
        std::map<Label, RelevantState> join_expansion;
10✔
578
        for (const auto& [v_label, v_relevance] : visited) {
86✔
579
            const auto& parents = prog.cfg().parents_of(v_label);
76✔
580
            if (parents.size() < 2) {
76✔
581
                continue;
74✔
582
            }
583
            // Check that at least one predecessor is in the slice (this join is relevant)
584
            bool has_slice_parent = false;
2✔
585
            for (const auto& parent : parents) {
4✔
586
                if (slice_labels.contains(parent)) {
4✔
587
                    has_slice_parent = true;
1✔
588
                    break;
1✔
589
                }
590
            }
591
            if (!has_slice_parent) {
2✔
NEW
592
                continue;
×
593
            }
594
            // Include the join-point label itself so the printing code can display
595
            // per-predecessor state at this join.
596
            if (!slice_labels.contains(v_label)) {
2✔
NEW
597
                join_expansion[v_label] = v_relevance;
×
598
            }
599
            // Include all predecessors so the join display is complete.
600
            // Use visited relevance if available, otherwise use the join-point's relevance.
601
            for (const auto& parent : parents) {
6✔
602
                if (slice_labels.contains(parent) || join_expansion.contains(parent)) {
4✔
603
                    continue;
2✔
604
                }
605
                const auto& rel = visited.contains(parent) ? visited.at(parent) : v_relevance;
2✔
606
                join_expansion[parent] = rel;
2✔
607
            }
608
        }
609
        slice_labels.insert(join_expansion.begin(), join_expansion.end());
10✔
610

611
        // Build the slice from contributing labels only
612
        slice.relevance = std::move(slice_labels);
10✔
613
        slices.push_back(std::move(slice));
10✔
614
    }
10✔
615

616
    return slices;
14✔
NEW
617
}
×
618

619
} // namespace prevail
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