21765175576

Committed 06 Feb 2026 11:02AM UTC coverage: 86.699% (-0.09%) from 86.792%

Build # 21765175576

Build Type

push

github

Committed by

web-flow

Commit Message

SplitDBM as one-sided numerical domain (#985)


Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Run Details

1316 of 1401 new or added lines in 15 files covered. (93.93%)

136 existing lines in 4 files now uncovered.

9334 of 10766 relevant lines covered (86.7%)

3133567.38 hits per line

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

75.47

/src/result.cpp

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

#include "crab/ebpf_domain.hpp"
#include "ir/program.hpp"
#include "result.hpp"

namespace prevail {

bool AnalysisResult::is_valid_after(const Label& label, const StringInvariant& state) const {
    const EbpfDomain abstract_state =
        EbpfDomain::from_constraints(state.value(), thread_local_options.setup_constraints);
    return abstract_state <= invariants.at(label).post;
}

ObservationCheckResult AnalysisResult::check_observation_at_label(const Label& label, const InvariantPoint point,
                                                                  const StringInvariant& observation,
                                                                  const ObservationCheckMode mode) const {
    const auto it = invariants.find(label);
    if (it == invariants.end()) {
        return {.ok = false, .message = "No invariant available for label " + to_string(label)};
    }
    const auto& inv_pair = it->second;
    const EbpfDomain& abstract_state = (point == InvariantPoint::pre) ? inv_pair.pre : inv_pair.post;

    const EbpfDomain observed_state =
        observation.is_bottom()
            ? EbpfDomain::bottom()
            : EbpfDomain::from_constraints(observation.value(), thread_local_options.setup_constraints);

    if (observed_state.is_bottom()) {
        return {.ok = false, .message = "Observation constraints are unsatisfiable (domain is bottom)"};
    }

    if (abstract_state.is_bottom()) {
        return {.ok = false, .message = "Invariant at label is bottom (unreachable)"};
    }

    switch (mode) {
    case ObservationCheckMode::entailed:
        if (observed_state <= abstract_state) {
            return {.ok = true, .message = ""};
        }
        return {.ok = false, .message = "Invariant does not entail the observation (C ⊑ A is false)"};

    case ObservationCheckMode::consistent:
        // Default: consistency / satisfiability.
        if ((abstract_state & observed_state).is_bottom()) {
            return {.ok = false, .message = "Observation contradicts invariant (meet is bottom)"};
        }
        return {.ok = true, .message = ""};
    }

    return {.ok = false, .message = "Unsupported observation check mode"};
}

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

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

StringInvariant AnalysisResult::invariant_at(const Label& label) const { return invariants.at(label).post.to_set(); }

std::optional<VerificationError> AnalysisResult::find_first_error() const {
    for (const auto& inv_pair : invariants | std::views::values) {
        if (inv_pair.pre.is_bottom()) {
            continue;
        }
        if (inv_pair.error) {
            return inv_pair.error;
        }
    }
    return {};
}

std::map<Label, std::vector<std::string>> AnalysisResult::find_unreachable(const Program& prog) const {
    std::map<Label, std::vector<std::string>> unreachable;
    for (const auto& [label, inv_pair] : invariants) {
        if (inv_pair.pre.is_bottom()) {
            continue;
        }
        if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {
            if (inv_pair.post.is_bottom() && !inv_pair.error) {
                const auto s = to_string(*passume);
                unreachable[label].emplace_back(to_string(label) + ": Code becomes unreachable (" + s + ")");
            }
        }
    }
    return unreachable;
}

} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <map>
4	#include <ranges>
5	#include <sstream>
6
7	#include "crab/ebpf_domain.hpp"
8	#include "ir/program.hpp"
9	#include "result.hpp"
10
11	namespace prevail {
12
13	bool AnalysisResult::is_valid_after(const Label& label, const StringInvariant& state) const {	×
14	const EbpfDomain abstract_state =
15	EbpfDomain::from_constraints(state.value(), thread_local_options.setup_constraints);	×
16	return abstract_state <= invariants.at(label).post;	×
17	}	×
18
19	ObservationCheckResult AnalysisResult::check_observation_at_label(const Label& label, const InvariantPoint point,	12✔
20	const StringInvariant& observation,
21	const ObservationCheckMode mode) const {
22	const auto it = invariants.find(label);	12✔
23	if (it == invariants.end()) {	12✔
UNCOV 24	return {.ok = false, .message = "No invariant available for label " + to_string(label)};	×
25	}
26	const auto& inv_pair = it->second;	12✔
27	const EbpfDomain& abstract_state = (point == InvariantPoint::pre) ? inv_pair.pre : inv_pair.post;	12✔
28
29	const EbpfDomain observed_state =	6✔
30	observation.is_bottom()	12✔
31	? EbpfDomain::bottom()	12✔
32	: EbpfDomain::from_constraints(observation.value(), thread_local_options.setup_constraints);	12✔
33
34	if (observed_state.is_bottom()) {	12✔
35	return {.ok = false, .message = "Observation constraints are unsatisfiable (domain is bottom)"};	2✔
36	}
37
38	if (abstract_state.is_bottom()) {	10✔
UNCOV 39	return {.ok = false, .message = "Invariant at label is bottom (unreachable)"};	×
40	}
41
42	switch (mode) {	10✔
43	case ObservationCheckMode::entailed:	4✔
44	if (observed_state <= abstract_state) {	4✔
45	return {.ok = true, .message = ""};	2✔
46	}
47	return {.ok = false, .message = "Invariant does not entail the observation (C ⊑ A is false)"};	2✔
48
49	case ObservationCheckMode::consistent:	6✔
50	// Default: consistency / satisfiability.
51	if ((abstract_state & observed_state).is_bottom()) {	9✔
UNCOV 52	return {.ok = false, .message = "Observation contradicts invariant (meet is bottom)"};	×
53	}
54	return {.ok = true, .message = ""};	6✔
55	}
56
UNCOV 57	return {.ok = false, .message = "Unsupported observation check mode"};	×
58	}	30✔
59
UNCOV 60	bool AnalysisResult::is_consistent_before(const Label& label, const StringInvariant& observation) const {	×
UNCOV 61	return check_observation_at_label(label, InvariantPoint::pre, observation, ObservationCheckMode::consistent).ok;	×
62	}
63
UNCOV 64	bool AnalysisResult::is_consistent_after(const Label& label, const StringInvariant& observation) const {	×
UNCOV 65	return check_observation_at_label(label, InvariantPoint::post, observation, ObservationCheckMode::consistent).ok;	×
66	}
67
68	StringInvariant AnalysisResult::invariant_at(const Label& label) const { return invariants.at(label).post.to_set(); }	1,400✔
69
70	std::optional<VerificationError> AnalysisResult::find_first_error() const {	1,400✔
71	for (const auto& inv_pair : invariants \| std::views::values) {	5,952✔
72	if (inv_pair.pre.is_bottom()) {	4,866✔
73	continue;	330✔
74	}
75	if (inv_pair.error) {	4,536✔
76	return inv_pair.error;	314✔
77	}
78	}
79	return {};	1,086✔
80	}
81
82	std::map<Label, std::vector<std::string>> AnalysisResult::find_unreachable(const Program& prog) const {	1,400✔
83	std::map<Label, std::vector<std::string>> unreachable;	1,400✔
84	for (const auto& [label, inv_pair] : invariants) {	6,828✔
85	if (inv_pair.pre.is_bottom()) {	5,428✔
86	continue;	810✔
87	}
88	if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {	7,332✔
89	if (inv_pair.post.is_bottom() && !inv_pair.error) {	556✔
90	const auto s = to_string(*passume);	182✔
91	unreachable[label].emplace_back(to_string(label) + ": Code becomes unreachable (" + s + ")");	455✔
92	}	182✔
93	}
94	}
95	return unreachable;	1,400✔
UNCOV 96	}	×
97
98	} // namespace prevail

Alan-Jowett / ebpf-verifier / 21765175576

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