21886055111

Committed 10 Feb 2026 08:02PM UTC coverage: 86.783% (+0.08%) from 86.699%

Build # 21886055111

Build Type

push

github

Committed by

elazarg

Commit Message

Fix inverted is_stable predicate in close_after_widen

UnstableWrap::operator[] returned true for unstable vertices, but was
passed as the `is_stable` parameter to close_after_widen. This caused
Dijkstra recovery to run from stable vertices (no-op) instead of
unstable vertices, missing transitive edge tightenings after widening.

Negate the predicate so unstable vertices are correctly marked V_UNSTABLE
and recovery discovers shortest paths through them.

https://claude.ai/code/session_01XRADiTjoWyzfaoyhF2odaf
Signed-off-by: Claude Code <claude@anthropic.com>

Coverage Stats

33 of 34 new or added lines in 2 files covered. (97.06%)

9370 of 10797 relevant lines covered (86.78%)

3129617.71 hits per line

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

99.53

/src/test/test_join.cpp

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

#include "arith/dsl_syntax.hpp"
#include "crab/ebpf_domain.hpp"
#include "crab/splitdbm/split_dbm.hpp"

using namespace prevail;

static void require_join(const std::vector<LinearConstraint>& a_type_csts, const std::vector<LinearConstraint>& a_csts,
                         const std::vector<LinearConstraint>& b_type_csts, const std::vector<LinearConstraint>& b_csts,
                         const std::vector<LinearConstraint>& over_type_csts,
                         const std::vector<LinearConstraint>& over_csts) {
    using namespace dsl_syntax;
    EbpfDomain a = EbpfDomain::from_constraints(a_type_csts, a_csts);
    EbpfDomain b = EbpfDomain::from_constraints(b_type_csts, b_csts);
    EbpfDomain j = a | b;
    REQUIRE(a <= j);
    REQUIRE(b <= j);
    EbpfDomain over_approx = EbpfDomain::from_constraints(over_type_csts, over_csts);
    REQUIRE(j <= over_approx);
}

static const RegPack r0 = reg_pack(0);
static const Variable r0_type = reg_type(Reg{0});
static const RegPack r1 = reg_pack(1);
static const Variable r1_type = reg_type(Reg{1});
static const RegPack r2 = reg_pack(2);
static const Variable r2_type = reg_type(Reg{2});
static const RegPack r6 = reg_pack(6);
static const Variable r6_type = reg_type(Reg{6});
static const RegPack r7 = reg_pack(7);
static const Variable r7_type = reg_type(Reg{7});
static const RegPack r10 = reg_pack(10);
static const Variable r10_type = reg_type(Reg{10});

TEST_CASE("EbpfDomain basic join", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({}, {}, {}, {}, {}, {});
}

// 1) Type-only joins
TEST_CASE("join same precise type", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {}, {r0_type == T_NUM}, {}, {r0_type == T_NUM}, {});
}

TEST_CASE("join disjoint precise types widens to range", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_MAP}, {}, {r0_type == T_STACK}, {}, {r0_type >= T_MAP, r0_type <= T_STACK}, {});
}

TEST_CASE("join precise with top widens type range", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_MAP}, {}, {r0_type == T_NUM}, {}, {r0_type >= T_MAP, r0_type <= T_NUM}, {});
}

TEST_CASE("EbpfDomain disjoint value join", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {r0.svalue == 0}, {r0_type == T_NUM}, {r0.svalue == 5}, {r0_type == T_NUM},
                 {r0.svalue >= 0, r0.svalue <= 5});
}

TEST_CASE("join respects partial order", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {r0.svalue == 1}, {r0_type == T_NUM}, {r0.svalue == 2}, {r0_type == T_NUM},
                 {r0.svalue >= 1, r0.svalue <= 2});
}

// 2) Value constraints with same type
TEST_CASE("join keeps equal constants", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {r0.svalue == 7}, {r0_type == T_NUM}, {r0.svalue == 7}, {r0_type == T_NUM},
                 {r0.svalue == 7});
}

TEST_CASE("join convex hull of disjoint constants", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {r0.svalue == 1}, {r0_type == T_NUM}, {r0.svalue == 3}, {r0_type == T_NUM},
                 {r0.svalue >= 1, r0.svalue <= 3});
}

TEST_CASE("join overlapping intervals", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {r0.svalue >= 0, r0.svalue <= 5}, {r0_type == T_NUM},
                 {r0.svalue >= 3, r0.svalue <= 10}, {r0_type == T_NUM}, {r0.svalue >= 0, r0.svalue <= 10});
}

TEST_CASE("join with one top one constrained becomes top for value", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {r0.svalue >= -5, r0.svalue <= 5}, {r0_type == T_NUM}, {}, {r0_type == T_NUM}, {});
}

// 3) Same memory type, offsets
TEST_CASE("join same pointer type same offset", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_PACKET}, {r0.svalue == 123, r0.packet_offset == 4}, {r0_type == T_PACKET},
                 {r0.svalue == 123, r0.packet_offset == 4}, {r0_type == T_PACKET},
                 {r0.svalue == 123, r0.packet_offset == 4});
}

TEST_CASE("join ranges offsets for same pointer type", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_PACKET}, {r0.svalue == 1, r0.packet_offset == 0}, {r0_type == T_PACKET},
                 {r0.svalue == 3, r0.packet_offset == 4}, {r0_type == T_PACKET},
                 {r0.svalue >= 1, r0.svalue <= 3, r0.packet_offset >= 0, r0.packet_offset <= 4});
}

// 4) Different memory types keep per-type offsets
TEST_CASE("join keeps offsets across disjoint types", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r1_type == T_STACK}, {r1.svalue == 123, r1.stack_offset == 100}, {r1_type == T_PACKET},
                 {r1.svalue == 123, r1.packet_offset == 4}, {r1_type >= T_PACKET, r1_type <= T_STACK},
                 {r1.svalue == 123, r1.stack_offset == 100, r1.packet_offset == 4});
}

// 5) One branch pointer, other numeric
TEST_CASE("join widens type and preserves offset from one side", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_PACKET}, {r0.packet_offset == 8}, {r0_type == T_NUM}, {},
                 {r0_type >= T_NUM, r0_type <= T_PACKET}, {r0.packet_offset == 8});
}

TEST_CASE("join with matching map types", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_MAP}, {r0.svalue == 1}, {r0_type == T_MAP}, {r0.svalue == 3}, {r0_type == T_MAP},
                 {r0.svalue >= 1, r0.svalue <= 3});
}

TEST_CASE("join with matching memory types but different offsets", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_PACKET}, {r0.svalue == 1, r0.packet_offset == 0}, {r0_type == T_PACKET},
                 {r0.svalue == 3, r0.packet_offset == 4}, {r0_type == T_PACKET},
                 {r0.svalue >= 1, r0.svalue <= 3, r0.packet_offset >= 0, r0.packet_offset <= 4});
}

TEST_CASE("join with different types and unknown offsets", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_MAP}, {r0.svalue == 1}, {r0_type == T_STACK}, {r0.svalue == 2},
                 {r0_type <= T_STACK, r0_type >= T_MAP}, {r0.svalue >= 1, r0.svalue <= 2});
}

// 6) Shared memory offsets and sizes
TEST_CASE("join shared offsets and sizes", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_SHARED}, {r0.shared_offset == 16, r0.shared_region_size == 64}, {r0_type == T_SHARED},
                 {r0.shared_offset == 32, r0.shared_region_size == 64}, {r0_type == T_SHARED},
                 {r0.shared_offset >= 16, r0.shared_offset <= 32, r0.shared_region_size == 64});
}

TEST_CASE("join preserves shared offset across type widening", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_SHARED}, {r0.shared_offset == 0}, {r0_type == T_NUM}, {},
                 {r0_type >= T_NUM, r0_type <= T_SHARED}, {r0.shared_offset == 0});
}

// 7) Stack numeric size interactions
TEST_CASE("join stack offsets and numeric size", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_STACK}, {r0.stack_offset == 64, r0.stack_numeric_size == 8}, {r0_type == T_STACK},
                 {r0.stack_offset == 96, r0.stack_numeric_size == 8}, {r0_type == T_STACK},
                 {r0.stack_offset >= 64, r0.stack_offset <= 96, r0.stack_numeric_size == 8});
}

TEST_CASE("join preserves stack facts across type mismatch", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_STACK}, {r0.stack_offset == 64, r0.stack_numeric_size == 8}, {r0_type == T_NUM}, {},
                 {r0_type >= T_NUM, r0_type <= T_STACK}, {r0.stack_offset == 64, r0.stack_numeric_size == 8});
}

// 8) Context and map-related variables
TEST_CASE("join context offsets", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_CTX}, {r0.ctx_offset == 0}, {r0_type == T_CTX}, {r0.ctx_offset == 16},
                 {r0_type == T_CTX}, {r0.ctx_offset >= 0, r0.ctx_offset <= 16});
}

TEST_CASE("join map fd constants", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_MAP}, {r0.map_fd == 10}, {r0_type == T_MAP}, {r0.map_fd == 10}, {r0_type == T_MAP},
                 {r0.map_fd == 10});
}

TEST_CASE("join map vs non-map keeps map fd", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_MAP}, {r0.map_fd == 7}, {r0_type == T_NUM}, {}, {r0_type <= T_NUM, r0_type >= T_MAP},
                 {r0.map_fd == 7});
}

// 9) Top/Bottom edge behavior
TEST_CASE("join with bottom on one side returns other", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({}, {r2.svalue == 0, r2.svalue != 0}, {r0_type == T_NUM}, {r2.svalue == 5}, {r0_type == T_NUM},
                 {r2.svalue == 5});
}

// 10) Type range with value ranges
TEST_CASE("join of type ranges with value ranges", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type >= T_PACKET, r0_type <= T_SHARED}, {r0.svalue >= 0, r0.svalue <= 100},
                 {r0_type >= T_NUM, r0_type <= T_STACK}, {r0.svalue >= 50, r0.svalue <= 200},
                 {r0_type >= T_NUM, r0_type <= T_SHARED}, {r0.svalue >= 0, r0.svalue <= 200});
}

TEST_CASE("join regression from 74+103 to 104", "[join][lattice]") {
    using namespace dsl_syntax;
    // distillation of running:
    // ./check --no-simplify ebpf-samples/linux/test_map_in_map_kern.o kprobe/sys_connect - v

    require_join(
        {r0_type == T_MAP, r6_type == T_MAP, r7_type == T_NUM, r10_type == T_STACK},
        {
            r0.svalue == 0,
            r6.svalue == 0,
            r7.svalue == 0,
            r1.svalue == 153,
            r10.svalue >= 4096,
            r10.svalue <= 2147418112,
        },
        {r0_type == T_NUM, r6_type == T_NUM, r7_type == T_NUM, r10_type == T_STACK},
        {
            r7.svalue >= 1,
            r1.svalue == 146,
            r10.svalue >= 4096,
            r10.svalue <= 2147418112,
        },
        // Conservative overapproximation of correct join
        {r0_type >= T_MAP, r0_type <= T_NUM, r6_type >= T_MAP, r6_type <= T_NUM, r7_type == T_NUM, r10_type == T_STACK},
        {
            r7.svalue >= 0,
            r1.svalue >= 146,
            r1.svalue <= 153,
            r10.svalue >= 4096,
            r10.svalue <= 2147418112,
        });
}

// 11) Relational domain properties
TEST_CASE("join preserves equality relation across branches", "[join][lattice]") {
    using namespace dsl_syntax;
    // Both branches assert r0.svalue == r1.svalue with different constants; after join, equality should be preserved
    require_join(
        {r0_type == T_NUM, r1_type == T_NUM}, {eq(r0.svalue, r1.svalue), r0.svalue == 5, eq(r0.uvalue, r1.uvalue)},
        {r0_type == T_NUM, r1_type == T_NUM}, {eq(r0.svalue, r1.svalue), r0.svalue == 7, eq(r0.uvalue, r1.uvalue)},
        {r0_type == T_NUM, r1_type == T_NUM},
        {r0.svalue >= 5, r0.svalue <= 7, r1.svalue >= 5, r1.svalue <= 7, eq(r0.svalue, r1.svalue),
         eq(r0.uvalue, r1.uvalue)});
}

TEST_CASE("join drops opposing order relations but keeps per-var hulls", "[join][lattice]") {
    using namespace dsl_syntax;
    // One branch has r0.svalue <= r1.svalue, the other r1.svalue <= r0.svalue, on the same intervals.
    require_join({r0_type == T_NUM, r1_type == T_NUM},
                 {r0.svalue >= 0, r0.svalue <= 10, r1.svalue >= 5, r1.svalue <= 15, r0.svalue <= r1.svalue},
                 {r0_type == T_NUM, r1_type == T_NUM},
                 {r0.svalue >= 0, r0.svalue <= 10, r1.svalue >= 5, r1.svalue <= 15, r1.svalue <= r0.svalue},
                 {r0_type == T_NUM, r1_type == T_NUM},
                 {r0.svalue >= 0, r0.svalue <= 10, r1.svalue >= 5, r1.svalue <= 15});
}

// 12) svalue/uvalue interactions and implicit holes
TEST_CASE("join preserves svalue/uvalue-implied hole when both branches imply it", "[join][lattice]") {
    using namespace dsl_syntax;
    // Negative signed implies large unsigned (>= 2^63). Both branches keep this fact, join should too.
    const Number two63 = Number::max_int(64) + Number(1); // 2^63
    require_join({r0_type == T_NUM}, {r0.svalue <= -1, r0.uvalue >= two63}, {r0_type == T_NUM},
                 {r0.svalue <= -10, r0.uvalue >= two63}, {r0_type == T_NUM}, {r0.svalue <= -1, r0.uvalue >= two63});
}

TEST_CASE("join may lose hole if other branch allows small non-negative values", "[join][lattice]") {
    using namespace dsl_syntax;
    const Number two63 = Number::max_int(64) + Number(1); // 2^63
    // Branch A implies a hole around 0 (negative signed => u >= 2^63).
    // Branch B allows only small non-negative values.
    // The joined over-approx (convex hull on each dimension) can lose the hole.
    require_join({r0_type == T_NUM}, {r0.svalue <= -1, r0.uvalue >= two63}, {r0_type == T_NUM},
                 {r0.svalue >= 0, r0.svalue <= 100, r0.uvalue >= 0, r0.uvalue <= 100}, {r0_type == T_NUM}, {});
}

// 13) Algebraic laws: commutativity and idempotence
TEST_CASE("join is commutative and idempotent (domain-wide)", "[join][lattice]") {
    using namespace dsl_syntax;
    const std::vector TA{r0_type == T_PACKET};
    const std::vector A{r0.svalue >= 1, r0.svalue <= 3, r0.packet_offset == 4};

    // Idempotence
    require_join(TA, A, TA, A, TA, A);

    // Commutativity: A ⊔ B = B ⊔ A (same over-approx)
    const std::vector TB{r0_type == T_NUM};
    const std::vector B{r0.svalue >= 2, r0.svalue <= 5};
    const std::vector Tover{r0_type >= T_NUM, r0_type <= T_PACKET};
    const std::vector over{r0.svalue >= 1, r0.svalue <= 5, r0.packet_offset == 4};
    require_join(TA, A, TB, B, Tover, over);
    require_join(TB, B, TA, A, Tover, over);
}

// 14) Numeric value across pointer/num join (value facts should not leak to pointer case)
TEST_CASE("join does not conflate value facts across pointer/num", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {r0.svalue == 42}, {r0_type == T_PACKET}, {r0.packet_offset == 8},
                 {r0_type >= T_NUM, r0_type <= T_PACKET}, {r0.packet_offset == 8});
}

// 15) Extreme bounds (overflow safety of convex hull)
TEST_CASE("join convex hull with extreme 64-bit bounds", "[join][lattice]") {
    using namespace dsl_syntax;
    const Number min64 = Number::min_int(64);
    const Number max64 = Number::max_int(64);
    require_join({r0_type == T_NUM}, {r0.svalue >= min64, r0.svalue <= -1}, {r0_type == T_NUM},
                 {r0.svalue >= 1, r0.svalue <= max64}, {r0_type == T_NUM}, {r0.svalue >= min64, r0.svalue <= max64});
}

// 16) Disjoint intervals with a gap
TEST_CASE("join hull of disjoint intervals with gap", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_NUM}, {r0.svalue >= -10, r0.svalue <= -1}, {r0_type == T_NUM},
                 {r0.svalue >= 1, r0.svalue <= 10}, {r0_type == T_NUM}, {r0.svalue >= -10, r0.svalue <= 10});
}

// 17) Mixed per-type fields preserved under widening
TEST_CASE("join preserves multiple per-type fields across type widening", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_PACKET}, {r0.packet_offset == 8}, {r0_type == T_STACK}, {r0.stack_offset == 96},
                 {r0_type >= T_PACKET, r0_type <= T_STACK}, {r0.packet_offset == 8, r0.stack_offset == 96});
}

// 18) Map FD differing constants
TEST_CASE("join map fd differing constants forms hull", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_MAP}, {r0.map_fd == 7}, {r0_type == T_MAP}, {r0.map_fd == 9}, {r0_type == T_MAP},
                 {r0.map_fd >= 7, r0.map_fd <= 9});
}

// 19) Shared region size differing
TEST_CASE("join shared region size differing values", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join(
        {r0_type == T_SHARED}, {r0.shared_offset == 0, r0.shared_region_size == 64}, {r0_type == T_SHARED},
        {r0.shared_offset == 32, r0.shared_region_size == 128}, {r0_type == T_SHARED},
        {r0.shared_offset >= 0, r0.shared_offset <= 32, r0.shared_region_size >= 64, r0.shared_region_size <= 128});
}

// 20) Context fields vanish when resulting type excludes T_CTX
TEST_CASE("join does not retain ctx_offset if resulting type excludes T_CTX", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r0_type == T_CTX}, {r0.ctx_offset == 16}, {r0_type >= T_NUM, r0_type <= T_STACK}, {},
                 {r0_type >= T_NUM, r0_type <= T_STACK}, {});
}

// 21) Multi-register per-type field preservation under mixed joins
TEST_CASE("join preserves multi-register per-type field", "[join][lattice]") {
    using namespace dsl_syntax;
    require_join({r6_type == T_PACKET, r7_type == T_NUM}, {r6.packet_offset == 4},
                 {r6_type == T_NUM, r7_type == T_STACK}, {r7.stack_offset == 128},
                 {r6_type >= T_NUM, r6_type <= T_PACKET, r7_type >= T_NUM, r7_type <= T_STACK},
                 {r6.packet_offset == 4, r7.stack_offset == 128});
}

// 22) SplitDBM widen closure
TEST_CASE("close_after_widen recovers transitive edge through unstable vertex", "[widen][splitdbm]") {
    using namespace splitdbm;

    // Vertices: 0 (special zero vertex), 1, 2, 3.
    //
    // Left (closed) graph:
    //   Bounds: 0->v: 100, v->0: 0 for v in {1,2,3}
    //   Relations: 1->2: 5, 2->3: 5, 1->3: 10 (closure of 1->2->3)
    //
    // Right graph (same, except 1->3 is LOOSER: 12 instead of 10):
    //   Relations: 1->2: 5, 2->3: 5, 1->3: 12
    //
    // Widening keeps edges where right <= left, using left's weight:
    //   1->2: 5 (kept), 2->3: 5 (kept), 1->3: DROPPED (12 > 10)
    //
    // Vertex 1 becomes unstable (lost outgoing edge 1->3).
    //
    // close_after_widen should run Dijkstra recovery from unstable vertex 1
    // and discover the transitive path 1->2->3 = 5+5 = 10, adding edge 1->3: 10.

    auto make_graph = [](Weight w13) {
        Graph g;
        g.growTo(4);
        g.add_edge(0, Weight(100), 1);
        g.add_edge(1, Weight(0), 0);
        g.add_edge(0, Weight(100), 2);
        g.add_edge(2, Weight(0), 0);
        g.add_edge(0, Weight(100), 3);
        g.add_edge(3, Weight(0), 0);
        g.add_edge(1, Weight(5), 2);
        g.add_edge(2, Weight(5), 3);
        g.add_edge(1, w13, 3);
        return g;
    };

    std::vector<Weight> pot = {Weight(0), Weight(0), Weight(5), Weight(10)};

    SplitDBM left(make_graph(Weight(10)), std::vector<Weight>(pot), VertSet{});
    SplitDBM right(make_graph(Weight(12)), std::vector<Weight>(pot), VertSet{});

    AlignedPair aligned{
        .left = left,
        .right = right,
        .left_perm = {0, 1, 2, 3},
        .right_perm = {0, 1, 2, 3},
        .initial_potentials = std::vector<Weight>(pot),
    };

    SplitDBM result = SplitDBM::widen(aligned);
    const Graph& rg = result.graph();

    REQUIRE(rg.elem(1, 2));
    CHECK(rg.edge_val(1, 2) == Weight(5));

    REQUIRE(rg.elem(2, 3));
    CHECK(rg.edge_val(2, 3) == Weight(5));

    // The transitive edge 1->3 should be recovered via path 1->2->3 = 5+5 = 10.
    REQUIRE(rg.elem(1, 3));
    CHECK(rg.edge_val(1, 3) == Weight(10));
}

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <catch2/catch_all.hpp>
4
5	#include "arith/dsl_syntax.hpp"
6	#include "crab/ebpf_domain.hpp"
7	#include "crab/splitdbm/split_dbm.hpp"
8
9	using namespace prevail;
10
11	static void require_join(const std::vector<LinearConstraint>& a_type_csts, const std::vector<LinearConstraint>& a_csts,	84✔
12	const std::vector<LinearConstraint>& b_type_csts, const std::vector<LinearConstraint>& b_csts,
13	const std::vector<LinearConstraint>& over_type_csts,
14	const std::vector<LinearConstraint>& over_csts) {
15	using namespace dsl_syntax;	42✔
16	EbpfDomain a = EbpfDomain::from_constraints(a_type_csts, a_csts);	84✔
17	EbpfDomain b = EbpfDomain::from_constraints(b_type_csts, b_csts);	84✔
18	EbpfDomain j = a \| b;	84✔
19	REQUIRE(a <= j);	84✔
20	REQUIRE(b <= j);	84✔
21	EbpfDomain over_approx = EbpfDomain::from_constraints(over_type_csts, over_csts);	84✔
22	REQUIRE(j <= over_approx);	126✔
23	}	84✔
24
25	static const RegPack r0 = reg_pack(0);
26	static const Variable r0_type = reg_type(Reg{0});
27	static const RegPack r1 = reg_pack(1);
28	static const Variable r1_type = reg_type(Reg{1});
29	static const RegPack r2 = reg_pack(2);
30	static const Variable r2_type = reg_type(Reg{2});
31	static const RegPack r6 = reg_pack(6);
32	static const Variable r6_type = reg_type(Reg{6});
33	static const RegPack r7 = reg_pack(7);
34	static const Variable r7_type = reg_type(Reg{7});
35	static const RegPack r10 = reg_pack(10);
36	static const Variable r10_type = reg_type(Reg{10});
37
38	TEST_CASE("EbpfDomain basic join", "[join][lattice]") {	2✔
39	using namespace dsl_syntax;	1✔
40	require_join({}, {}, {}, {}, {}, {});	2✔
41	}	2✔
42
43	// 1) Type-only joins
44	TEST_CASE("join same precise type", "[join][lattice]") {	2✔
45	using namespace dsl_syntax;	1✔
46	require_join({r0_type == T_NUM}, {}, {r0_type == T_NUM}, {}, {r0_type == T_NUM}, {});	21✔
47	}	15✔
48
49	TEST_CASE("join disjoint precise types widens to range", "[join][lattice]") {	2✔
50	using namespace dsl_syntax;	1✔
51	require_join({r0_type == T_MAP}, {}, {r0_type == T_STACK}, {}, {r0_type >= T_MAP, r0_type <= T_STACK}, {});	23✔
52	}	18✔
53
54	TEST_CASE("join precise with top widens type range", "[join][lattice]") {	2✔
55	using namespace dsl_syntax;	1✔
56	require_join({r0_type == T_MAP}, {}, {r0_type == T_NUM}, {}, {r0_type >= T_MAP, r0_type <= T_NUM}, {});	23✔
57	}	18✔
58
59	TEST_CASE("EbpfDomain disjoint value join", "[join][lattice]") {	2✔
60	using namespace dsl_syntax;	1✔
61	require_join({r0_type == T_NUM}, {r0.svalue == 0}, {r0_type == T_NUM}, {r0.svalue == 5}, {r0_type == T_NUM},	37✔
62	{r0.svalue >= 0, r0.svalue <= 5});
63	}	33✔
64
65	TEST_CASE("join respects partial order", "[join][lattice]") {	2✔
66	using namespace dsl_syntax;	1✔
67	require_join({r0_type == T_NUM}, {r0.svalue == 1}, {r0_type == T_NUM}, {r0.svalue == 2}, {r0_type == T_NUM},	37✔
68	{r0.svalue >= 1, r0.svalue <= 2});
69	}	33✔
70
71	// 2) Value constraints with same type
72	TEST_CASE("join keeps equal constants", "[join][lattice]") {	2✔
73	using namespace dsl_syntax;	1✔
74	require_join({r0_type == T_NUM}, {r0.svalue == 7}, {r0_type == T_NUM}, {r0.svalue == 7}, {r0_type == T_NUM},	35✔
75	{r0.svalue == 7});
76	}	30✔
77
78	TEST_CASE("join convex hull of disjoint constants", "[join][lattice]") {	2✔
79	using namespace dsl_syntax;	1✔
80	require_join({r0_type == T_NUM}, {r0.svalue == 1}, {r0_type == T_NUM}, {r0.svalue == 3}, {r0_type == T_NUM},	37✔
81	{r0.svalue >= 1, r0.svalue <= 3});
82	}	33✔
83
84	TEST_CASE("join overlapping intervals", "[join][lattice]") {	2✔
85	using namespace dsl_syntax;	1✔
86	require_join({r0_type == T_NUM}, {r0.svalue >= 0, r0.svalue <= 5}, {r0_type == T_NUM},	41✔
87	{r0.svalue >= 3, r0.svalue <= 10}, {r0_type == T_NUM}, {r0.svalue >= 0, r0.svalue <= 10});
88	}	39✔
89
90	TEST_CASE("join with one top one constrained becomes top for value", "[join][lattice]") {	2✔
91	using namespace dsl_syntax;	1✔
92	require_join({r0_type == T_NUM}, {r0.svalue >= -5, r0.svalue <= 5}, {r0_type == T_NUM}, {}, {r0_type == T_NUM}, {});	28✔
93	}	23✔
94
95	// 3) Same memory type, offsets
96	TEST_CASE("join same pointer type same offset", "[join][lattice]") {	2✔
97	using namespace dsl_syntax;	1✔
98	require_join({r0_type == T_PACKET}, {r0.svalue == 123, r0.packet_offset == 4}, {r0_type == T_PACKET},	41✔
99	{r0.svalue == 123, r0.packet_offset == 4}, {r0_type == T_PACKET},
100	{r0.svalue == 123, r0.packet_offset == 4});
101	}	36✔
102
103	TEST_CASE("join ranges offsets for same pointer type", "[join][lattice]") {	2✔
104	using namespace dsl_syntax;	1✔
105	require_join({r0_type == T_PACKET}, {r0.svalue == 1, r0.packet_offset == 0}, {r0_type == T_PACKET},	45✔
106	{r0.svalue == 3, r0.packet_offset == 4}, {r0_type == T_PACKET},
107	{r0.svalue >= 1, r0.svalue <= 3, r0.packet_offset >= 0, r0.packet_offset <= 4});
108	}	42✔
109
110	// 4) Different memory types keep per-type offsets
111	TEST_CASE("join keeps offsets across disjoint types", "[join][lattice]") {	2✔
112	using namespace dsl_syntax;	1✔
113	require_join({r1_type == T_STACK}, {r1.svalue == 123, r1.stack_offset == 100}, {r1_type == T_PACKET},	45✔
114	{r1.svalue == 123, r1.packet_offset == 4}, {r1_type >= T_PACKET, r1_type <= T_STACK},
115	{r1.svalue == 123, r1.stack_offset == 100, r1.packet_offset == 4});
116	}	41✔
117
118	// 5) One branch pointer, other numeric
119	TEST_CASE("join widens type and preserves offset from one side", "[join][lattice]") {	2✔
120	using namespace dsl_syntax;	1✔
121	require_join({r0_type == T_PACKET}, {r0.packet_offset == 8}, {r0_type == T_NUM}, {},	32✔
122	{r0_type >= T_NUM, r0_type <= T_PACKET}, {r0.packet_offset == 8});
123	}	28✔
124
125	TEST_CASE("join with matching map types", "[join][lattice]") {	2✔
126	using namespace dsl_syntax;	1✔
127	require_join({r0_type == T_MAP}, {r0.svalue == 1}, {r0_type == T_MAP}, {r0.svalue == 3}, {r0_type == T_MAP},	37✔
128	{r0.svalue >= 1, r0.svalue <= 3});
129	}	33✔
130
131	TEST_CASE("join with matching memory types but different offsets", "[join][lattice]") {	2✔
132	using namespace dsl_syntax;	1✔
133	require_join({r0_type == T_PACKET}, {r0.svalue == 1, r0.packet_offset == 0}, {r0_type == T_PACKET},	45✔
134	{r0.svalue == 3, r0.packet_offset == 4}, {r0_type == T_PACKET},
135	{r0.svalue >= 1, r0.svalue <= 3, r0.packet_offset >= 0, r0.packet_offset <= 4});
136	}	42✔
137
138	TEST_CASE("join with different types and unknown offsets", "[join][lattice]") {	2✔
139	using namespace dsl_syntax;	1✔
140	require_join({r0_type == T_MAP}, {r0.svalue == 1}, {r0_type == T_STACK}, {r0.svalue == 2},	38✔
141	{r0_type <= T_STACK, r0_type >= T_MAP}, {r0.svalue >= 1, r0.svalue <= 2});
142	}	35✔
143
144	// 6) Shared memory offsets and sizes
145	TEST_CASE("join shared offsets and sizes", "[join][lattice]") {	2✔
146	using namespace dsl_syntax;	1✔
147	require_join({r0_type == T_SHARED}, {r0.shared_offset == 16, r0.shared_region_size == 64}, {r0_type == T_SHARED},	43✔
148	{r0.shared_offset == 32, r0.shared_region_size == 64}, {r0_type == T_SHARED},
149	{r0.shared_offset >= 16, r0.shared_offset <= 32, r0.shared_region_size == 64});
150	}	39✔
151
152	TEST_CASE("join preserves shared offset across type widening", "[join][lattice]") {	2✔
153	using namespace dsl_syntax;	1✔
154	require_join({r0_type == T_SHARED}, {r0.shared_offset == 0}, {r0_type == T_NUM}, {},	32✔
155	{r0_type >= T_NUM, r0_type <= T_SHARED}, {r0.shared_offset == 0});
156	}	28✔
157
158	// 7) Stack numeric size interactions
159	TEST_CASE("join stack offsets and numeric size", "[join][lattice]") {	2✔
160	using namespace dsl_syntax;	1✔
161	require_join({r0_type == T_STACK}, {r0.stack_offset == 64, r0.stack_numeric_size == 8}, {r0_type == T_STACK},	43✔
162	{r0.stack_offset == 96, r0.stack_numeric_size == 8}, {r0_type == T_STACK},
163	{r0.stack_offset >= 64, r0.stack_offset <= 96, r0.stack_numeric_size == 8});
164	}	39✔
165
166	TEST_CASE("join preserves stack facts across type mismatch", "[join][lattice]") {	2✔
167	using namespace dsl_syntax;	1✔
168	require_join({r0_type == T_STACK}, {r0.stack_offset == 64, r0.stack_numeric_size == 8}, {r0_type == T_NUM}, {},	36✔
169	{r0_type >= T_NUM, r0_type <= T_STACK}, {r0.stack_offset == 64, r0.stack_numeric_size == 8});
170	}	32✔
171
172	// 8) Context and map-related variables
173	TEST_CASE("join context offsets", "[join][lattice]") {	2✔
174	using namespace dsl_syntax;	1✔
175	require_join({r0_type == T_CTX}, {r0.ctx_offset == 0}, {r0_type == T_CTX}, {r0.ctx_offset == 16},	37✔
176	{r0_type == T_CTX}, {r0.ctx_offset >= 0, r0.ctx_offset <= 16});
177	}	33✔
178
179	TEST_CASE("join map fd constants", "[join][lattice]") {	2✔
180	using namespace dsl_syntax;	1✔
181	require_join({r0_type == T_MAP}, {r0.map_fd == 10}, {r0_type == T_MAP}, {r0.map_fd == 10}, {r0_type == T_MAP},	35✔
182	{r0.map_fd == 10});
183	}	30✔
184
185	TEST_CASE("join map vs non-map keeps map fd", "[join][lattice]") {	2✔
186	using namespace dsl_syntax;	1✔
187	require_join({r0_type == T_MAP}, {r0.map_fd == 7}, {r0_type == T_NUM}, {}, {r0_type <= T_NUM, r0_type >= T_MAP},	32✔
188	{r0.map_fd == 7});
189	}	27✔
190
191	// 9) Top/Bottom edge behavior
192	TEST_CASE("join with bottom on one side returns other", "[join][lattice]") {	2✔
193	using namespace dsl_syntax;	1✔
194	require_join({}, {r2.svalue == 0, r2.svalue != 0}, {r0_type == T_NUM}, {r2.svalue == 5}, {r0_type == T_NUM},	31✔
195	{r2.svalue == 5});
196	}	27✔
197
198	// 10) Type range with value ranges
199	TEST_CASE("join of type ranges with value ranges", "[join][lattice]") {	2✔
200	using namespace dsl_syntax;	1✔
201	require_join({r0_type >= T_PACKET, r0_type <= T_SHARED}, {r0.svalue >= 0, r0.svalue <= 100},	47✔
202	{r0_type >= T_NUM, r0_type <= T_STACK}, {r0.svalue >= 50, r0.svalue <= 200},
203	{r0_type >= T_NUM, r0_type <= T_SHARED}, {r0.svalue >= 0, r0.svalue <= 200});
204	}	48✔
205
206	TEST_CASE("join regression from 74+103 to 104", "[join][lattice]") {	2✔
207	using namespace dsl_syntax;	1✔
208	// distillation of running:
209	// ./check --no-simplify ebpf-samples/linux/test_map_in_map_kern.o kprobe/sys_connect - v
210
211	require_join(	81✔
212	{r0_type == T_MAP, r6_type == T_MAP, r7_type == T_NUM, r10_type == T_STACK},
213	{
214	r0.svalue == 0,
215	r6.svalue == 0,
216	r7.svalue == 0,
217	r1.svalue == 153,
218	r10.svalue >= 4096,
219	r10.svalue <= 2147418112,
220	},
221	{r0_type == T_NUM, r6_type == T_NUM, r7_type == T_NUM, r10_type == T_STACK},
222	{
223	r7.svalue >= 1,
224	r1.svalue == 146,
225	r10.svalue >= 4096,
226	r10.svalue <= 2147418112,
227	},
228	// Conservative overapproximation of correct join
229	{r0_type >= T_MAP, r0_type <= T_NUM, r6_type >= T_MAP, r6_type <= T_NUM, r7_type == T_NUM, r10_type == T_STACK},
230	{
231	r7.svalue >= 0,
232	r1.svalue >= 146,
233	r1.svalue <= 153,
234	r10.svalue >= 4096,
235	r10.svalue <= 2147418112,
236	});
237	}	84✔
238
239	// 11) Relational domain properties
240	TEST_CASE("join preserves equality relation across branches", "[join][lattice]") {	2✔
241	using namespace dsl_syntax;	1✔
242	// Both branches assert r0.svalue == r1.svalue with different constants; after join, equality should be preserved
243	require_join(	59✔
244	{r0_type == T_NUM, r1_type == T_NUM}, {eq(r0.svalue, r1.svalue), r0.svalue == 5, eq(r0.uvalue, r1.uvalue)},
245	{r0_type == T_NUM, r1_type == T_NUM}, {eq(r0.svalue, r1.svalue), r0.svalue == 7, eq(r0.uvalue, r1.uvalue)},
246	{r0_type == T_NUM, r1_type == T_NUM},
247	{r0.svalue >= 5, r0.svalue <= 7, r1.svalue >= 5, r1.svalue <= 7, eq(r0.svalue, r1.svalue),
248	eq(r0.uvalue, r1.uvalue)});
249	}	44✔
250
251	TEST_CASE("join drops opposing order relations but keeps per-var hulls", "[join][lattice]") {	2✔
252	using namespace dsl_syntax;	1✔
253	// One branch has r0.svalue <= r1.svalue, the other r1.svalue <= r0.svalue, on the same intervals.
254	require_join({r0_type == T_NUM, r1_type == T_NUM},	63✔
255	{r0.svalue >= 0, r0.svalue <= 10, r1.svalue >= 5, r1.svalue <= 15, r0.svalue <= r1.svalue},
256	{r0_type == T_NUM, r1_type == T_NUM},
257	{r0.svalue >= 0, r0.svalue <= 10, r1.svalue >= 5, r1.svalue <= 15, r1.svalue <= r0.svalue},
258	{r0_type == T_NUM, r1_type == T_NUM},
259	{r0.svalue >= 0, r0.svalue <= 10, r1.svalue >= 5, r1.svalue <= 15});
260	}	64✔
261
262	// 12) svalue/uvalue interactions and implicit holes
263	TEST_CASE("join preserves svalue/uvalue-implied hole when both branches imply it", "[join][lattice]") {	2✔
264	using namespace dsl_syntax;	1✔
265	// Negative signed implies large unsigned (>= 2^63). Both branches keep this fact, join should too.
266	const Number two63 = Number::max_int(64) + Number(1); // 2^63	3✔
267	require_join({r0_type == T_NUM}, {r0.svalue <= -1, r0.uvalue >= two63}, {r0_type == T_NUM},	38✔
268	{r0.svalue <= -10, r0.uvalue >= two63}, {r0_type == T_NUM}, {r0.svalue <= -1, r0.uvalue >= two63});
269	}	39✔
270
271	TEST_CASE("join may lose hole if other branch allows small non-negative values", "[join][lattice]") {	2✔
272	using namespace dsl_syntax;	1✔
273	const Number two63 = Number::max_int(64) + Number(1); // 2^63	3✔
274	// Branch A implies a hole around 0 (negative signed => u >= 2^63).
275	// Branch B allows only small non-negative values.
276	// The joined over-approx (convex hull on each dimension) can lose the hole.
277	require_join({r0_type == T_NUM}, {r0.svalue <= -1, r0.uvalue >= two63}, {r0_type == T_NUM},	39✔
278	{r0.svalue >= 0, r0.svalue <= 100, r0.uvalue >= 0, r0.uvalue <= 100}, {r0_type == T_NUM}, {});
279	}	37✔
280
281	// 13) Algebraic laws: commutativity and idempotence
282	TEST_CASE("join is commutative and idempotent (domain-wide)", "[join][lattice]") {	2✔
283	using namespace dsl_syntax;	1✔
284	const std::vector TA{r0_type == T_PACKET};	5✔
285	const std::vector A{r0.svalue >= 1, r0.svalue <= 3, r0.packet_offset == 4};	9✔
286
287	// Idempotence
288	require_join(TA, A, TA, A, TA, A);	2✔
289
290	// Commutativity: A ⊔ B = B ⊔ A (same over-approx)
291	const std::vector TB{r0_type == T_NUM};	5✔
292	const std::vector B{r0.svalue >= 2, r0.svalue <= 5};	7✔
293	const std::vector Tover{r0_type >= T_NUM, r0_type <= T_PACKET};	7✔
294	const std::vector over{r0.svalue >= 1, r0.svalue <= 5, r0.packet_offset == 4};	9✔
295	require_join(TA, A, TB, B, Tover, over);	2✔
296	require_join(TB, B, TA, A, Tover, over);	2✔
297	}	38✔
298
299	// 14) Numeric value across pointer/num join (value facts should not leak to pointer case)
300	TEST_CASE("join does not conflate value facts across pointer/num", "[join][lattice]") {	2✔
301	using namespace dsl_syntax;	1✔
302	require_join({r0_type == T_NUM}, {r0.svalue == 42}, {r0_type == T_PACKET}, {r0.packet_offset == 8},	37✔
303	{r0_type >= T_NUM, r0_type <= T_PACKET}, {r0.packet_offset == 8});
304	}	33✔
305
306	// 15) Extreme bounds (overflow safety of convex hull)
307	TEST_CASE("join convex hull with extreme 64-bit bounds", "[join][lattice]") {	2✔
308	using namespace dsl_syntax;	1✔
309	const Number min64 = Number::min_int(64);	2✔
310	const Number max64 = Number::max_int(64);	2✔
311	require_join({r0_type == T_NUM}, {r0.svalue >= min64, r0.svalue <= -1}, {r0_type == T_NUM},	41✔
312	{r0.svalue >= 1, r0.svalue <= max64}, {r0_type == T_NUM}, {r0.svalue >= min64, r0.svalue <= max64});
313	}	43✔
314
315	// 16) Disjoint intervals with a gap
316	TEST_CASE("join hull of disjoint intervals with gap", "[join][lattice]") {	2✔
317	using namespace dsl_syntax;	1✔
318	require_join({r0_type == T_NUM}, {r0.svalue >= -10, r0.svalue <= -1}, {r0_type == T_NUM},	41✔
319	{r0.svalue >= 1, r0.svalue <= 10}, {r0_type == T_NUM}, {r0.svalue >= -10, r0.svalue <= 10});
320	}	39✔
321
322	// 17) Mixed per-type fields preserved under widening
323	TEST_CASE("join preserves multiple per-type fields across type widening", "[join][lattice]") {	2✔
324	using namespace dsl_syntax;	1✔
325	require_join({r0_type == T_PACKET}, {r0.packet_offset == 8}, {r0_type == T_STACK}, {r0.stack_offset == 96},	39✔
326	{r0_type >= T_PACKET, r0_type <= T_STACK}, {r0.packet_offset == 8, r0.stack_offset == 96});
327	}	35✔
328
329	// 18) Map FD differing constants
330	TEST_CASE("join map fd differing constants forms hull", "[join][lattice]") {	2✔
331	using namespace dsl_syntax;	1✔
332	require_join({r0_type == T_MAP}, {r0.map_fd == 7}, {r0_type == T_MAP}, {r0.map_fd == 9}, {r0_type == T_MAP},	37✔
333	{r0.map_fd >= 7, r0.map_fd <= 9});
334	}	33✔
335
336	// 19) Shared region size differing
337	TEST_CASE("join shared region size differing values", "[join][lattice]") {	2✔
338	using namespace dsl_syntax;	1✔
339	require_join(	45✔
340	{r0_type == T_SHARED}, {r0.shared_offset == 0, r0.shared_region_size == 64}, {r0_type == T_SHARED},
341	{r0.shared_offset == 32, r0.shared_region_size == 128}, {r0_type == T_SHARED},
342	{r0.shared_offset >= 0, r0.shared_offset <= 32, r0.shared_region_size >= 64, r0.shared_region_size <= 128});
343	}	42✔
344
345	// 20) Context fields vanish when resulting type excludes T_CTX
346	TEST_CASE("join does not retain ctx_offset if resulting type excludes T_CTX", "[join][lattice]") {	2✔
347	using namespace dsl_syntax;	1✔
348	require_join({r0_type == T_CTX}, {r0.ctx_offset == 16}, {r0_type >= T_NUM, r0_type <= T_STACK}, {},	30✔
349	{r0_type >= T_NUM, r0_type <= T_STACK}, {});
350	}	26✔
351
352	// 21) Multi-register per-type field preservation under mixed joins
353	TEST_CASE("join preserves multi-register per-type field", "[join][lattice]") {	2✔
354	using namespace dsl_syntax;	1✔
355	require_join({r6_type == T_PACKET, r7_type == T_NUM}, {r6.packet_offset == 4},	47✔
356	{r6_type == T_NUM, r7_type == T_STACK}, {r7.stack_offset == 128},
357	{r6_type >= T_NUM, r6_type <= T_PACKET, r7_type >= T_NUM, r7_type <= T_STACK},
358	{r6.packet_offset == 4, r7.stack_offset == 128});
359	}	44✔
360
361	// 22) SplitDBM widen closure
362	TEST_CASE("close_after_widen recovers transitive edge through unstable vertex", "[widen][splitdbm]") {	2✔
363	using namespace splitdbm;	1✔
364
365	// Vertices: 0 (special zero vertex), 1, 2, 3.
366	//
367	// Left (closed) graph:
368	// Bounds: 0->v: 100, v->0: 0 for v in {1,2,3}
369	// Relations: 1->2: 5, 2->3: 5, 1->3: 10 (closure of 1->2->3)
370	//
371	// Right graph (same, except 1->3 is LOOSER: 12 instead of 10):
372	// Relations: 1->2: 5, 2->3: 5, 1->3: 12
373	//
374	// Widening keeps edges where right <= left, using left's weight:
375	// 1->2: 5 (kept), 2->3: 5 (kept), 1->3: DROPPED (12 > 10)
376	//
377	// Vertex 1 becomes unstable (lost outgoing edge 1->3).
378	//
379	// close_after_widen should run Dijkstra recovery from unstable vertex 1
380	// and discover the transitive path 1->2->3 = 5+5 = 10, adding edge 1->3: 10.
381
382	auto make_graph = [](Weight w13) {	5✔
383	Graph g;	4✔
384	g.growTo(4);	4✔
385	g.add_edge(0, Weight(100), 1);	4✔
386	g.add_edge(1, Weight(0), 0);	4✔
387	g.add_edge(0, Weight(100), 2);	4✔
388	g.add_edge(2, Weight(0), 0);	4✔
389	g.add_edge(0, Weight(100), 3);	4✔
390	g.add_edge(3, Weight(0), 0);	4✔
391	g.add_edge(1, Weight(5), 2);	4✔
392	g.add_edge(2, Weight(5), 3);	4✔
393	g.add_edge(1, w13, 3);	4✔
394	return g;	4✔
NEW 395	};	×
396
397	std::vector<Weight> pot = {Weight(0), Weight(0), Weight(5), Weight(10)};	12✔
398
399	SplitDBM left(make_graph(Weight(10)), std::vector<Weight>(pot), VertSet{});	3✔
400	SplitDBM right(make_graph(Weight(12)), std::vector<Weight>(pot), VertSet{});	3✔
401
402	AlignedPair aligned{	1✔
403	.left = left,
404	.right = right,
405	.left_perm = {0, 1, 2, 3},
406	.right_perm = {0, 1, 2, 3},
407	.initial_potentials = std::vector<Weight>(pot),
408	};	4✔
409
410	SplitDBM result = SplitDBM::widen(aligned);	2✔
411	const Graph& rg = result.graph();	2✔
412
413	REQUIRE(rg.elem(1, 2));	2✔
414	CHECK(rg.edge_val(1, 2) == Weight(5));	2✔
415
416	REQUIRE(rg.elem(2, 3));	2✔
417	CHECK(rg.edge_val(2, 3) == Weight(5));	2✔
418
419	// The transitive edge 1->3 should be recovered via path 1->2->3 = 5+5 = 10.
420	REQUIRE(rg.elem(1, 3));	2✔
421	CHECK(rg.edge_val(1, 3) == Weight(10));	2✔
422	}	2✔

Alan-Jowett / ebpf-verifier / 21886055111

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