Alan-Jowett / ebpf-verifier / 22189862561

coverage: 88.157% (-0.1%) from 88.256%
22189862561

push

github

elazarg 
docs: track parity with Linux 6.18

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

10637 of 12066 relevant lines covered (88.16%)

774692.87 hits per line

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

97.05
/src/crab/splitdbm/split_dbm.cpp
1 
// Copyright (c) Prevail Verifier contributors.
2 
// SPDX-License-Identifier: Apache-2.0
3 









4



#include "crab/splitdbm/split_dbm.hpp"










5



#include "crab/splitdbm/definitions.hpp"










6












7



namespace splitdbm {










8












9



namespace {










10












11



// Compute deferred relations: bounds from bound_source applied to relations from rel_source.










12



Graph compute_deferred(const ReadableGraph auto& bound_source, ReadableGraph auto& rel_source, const size_t sz) {




99,620✔





13



    Graph deferred;




99,620✔





14



    deferred.growTo(sz);




99,620✔





15



    for (SubGraph rel_excl(rel_source, 0); VertId s : rel_excl.verts()) {




5,308,496✔





16



        for (VertId d : rel_excl.succs(s)) {




10,772,499✔





17



            if (auto ws = bound_source.lookup(s, 0)) {




3,709,082✔





18



                if (auto wd = bound_source.lookup(0, d)) {




3,491,828✔





19



                    deferred.add_edge(s, *ws + *wd, d);




3,451,124✔





20



                }










21



            }










22



        }










23



    }










24



    return deferred;




99,620✔





25



}




×







26












27



// Meet deferred relations into base graph and re-close.










28



Graph close_deferred(ScratchSpace& scratch, const ReadableGraph auto& base, const Graph& deferred,




99,620✔





29



                     const std::vector<Weight>& pot) {










30



    bool is_closed{};




99,620✔





31



    Graph closed(graph_meet(base, deferred, is_closed));




99,620✔





32



    if (!is_closed) {




99,620✔





33



        const auto p = [&pot](const VertId v) -> Weight { return pot[v]; };




14,446,224✔





34



        splitdbm::apply_delta(closed, close_after_meet(scratch, SubGraph(closed, 0), p, base, deferred));




149,430✔





35



    }










36



    return closed;




149,430✔





37



}




×







38












39



} // anonymous namespace










40












41



SplitDBM::SplitDBM() {




1,174,458✔





42



    g_.growTo(1); // Allocate the zero vertex




1,174,458✔





43



    potential_.emplace_back(0);




1,174,458✔





44



}




1,174,458✔





45












46



SplitDBM::SplitDBM(Graph&& g, std::vector<Weight>&& pot, VertSet&& unstable)




49,978✔





47



    : g_(std::move(g)), potential_(std::move(pot)), unstable_(std::move(unstable)) {




49,978✔





48



    normalize();




49,978✔





49



}




49,978✔





50












51



bool SplitDBM::is_top() const { return g_.is_empty(); }




155,110✔





52












53



prevail::ExtendedNumber SplitDBM::get_bound(const VertId v, const Side side) const {




2,119,874✔





54



    if (side == Side::LEFT) {




2,119,874✔





55



        return g_.elem(v, 0) ? -prevail::Number(g_.edge_val(v, 0)) : prevail::MINUS_INFINITY;




1,140,010✔





56



    } else {










57



        return g_.elem(0, v) ? prevail::Number(g_.edge_val(0, v)) : prevail::PLUS_INFINITY;




979,864✔





58



    }










59



}










60












61



// Callers must call normalize() after set_bound() to restore closure.










62



void SplitDBM::set_bound(const VertId v, const Side side, const Weight& bound_value) {




415,210✔





63



    if (side == Side::LEFT) {




415,210✔





64



        g_.set_edge(v, -bound_value, 0);




215,320✔





65



    } else {










66



        g_.set_edge(0, bound_value, v);




199,890✔





67



    }










68



    potential_[v] = potential_[0] + bound_value;




415,210✔





69



}




415,210✔





70












71



VertId SplitDBM::new_vertex() {




490,552✔





72



    const VertId vert = g_.new_vertex();




490,552✔





73



    if (vert >= potential_.size()) {




490,552✔





74



        potential_.emplace_back(0);




176,512✔





75



    } else {










76



        potential_[vert] = Weight(0);




314,040✔





77



    }










78



    return vert;




490,552✔





79



}










80












81



void SplitDBM::forget(const VertId v) { g_.forget(v); }




411,838✔





82












83



const Graph& SplitDBM::graph() const { return g_; }




970✔





84












85



bool SplitDBM::repair_potential(const VertId src, const VertId dest) {




216,008✔





86



    return splitdbm::repair_potential(*scratch_, g_, potential_, src, dest);




216,008✔





87



}










88












89



bool SplitDBM::update_bound_if_tighter(const VertId v, const Side side, const Weight& new_bound) {




258,960✔





90



    if (side == Side::LEFT) {




258,960✔





91



        if (const auto w = g_.lookup(v, 0)) {




142,974✔





92



            if (*w <= -new_bound) {




87,530✔





93



                return true;




24,736✔





94



            }










95



        }










96



        g_.set_edge(v, -new_bound, 0);




93,502✔





97



        return repair_potential(v, 0);




93,502✔





98



    } else {










99



        if (const auto w = g_.lookup(0, v)) {




115,986✔





100



            if (*w <= new_bound) {




87,894✔





101



                return true;




14,408✔





102



            }










103



        }










104



        g_.set_edge(0, new_bound, v);




87,170✔





105



        return repair_potential(0, v);




87,170✔





106



    }










107



}










108












109



bool SplitDBM::add_difference_constraint(const VertId src, const VertId dest, const Weight& k) {




35,268✔





110



    g_.update_edge(src, k, dest);




35,268✔





111



    if (!repair_potential(src, dest)) {




35,268✔





112



        return false;




8,760✔





113



    }










114



    close_over_edge(g_, src, dest);




17,748✔





115



    return true;




17,748✔





116



}










117












118



void SplitDBM::close_after_bound_updates() {




198,842✔





119



    apply_delta(close_after_assign(*scratch_, g_, [this](const VertId v) { return potential_[v]; }, 0));




103,309,003✔





120



}




198,842✔





121












122



void SplitDBM::apply_delta(const EdgeVector& delta) { splitdbm::apply_delta(g_, delta); }




463,374✔





123












124



void SplitDBM::close_after_assign_vertex(const VertId v) {




176,248✔





125



    apply_delta(close_after_assign(*scratch_, SubGraph(g_, 0), [this](const VertId u) { return potential_[u]; }, v));




274,578✔





126



}




176,248✔





127












128



VertId SplitDBM::assign_vertex(const Weight& potential_value,




176,248✔





129



                               const std::span<const std::pair<VertId, Weight>> diffs_from,










130



                               const std::span<const std::pair<VertId, Weight>> diffs_to,










131



                               const std::optional<Weight>& lb_edge, const std::optional<Weight>& ub_edge) {










132



    const VertId vert = new_vertex();




176,248✔





133



    potential_[vert] = potential_value;




176,248✔





134












135



    EdgeVector delta;




176,248✔





136



    delta.reserve(diffs_from.size() + diffs_to.size());




176,248✔





137



    for (const auto& [dest, w] : diffs_from) {




354,150✔





138



        delta.emplace_back(vert, dest, w);




177,902✔





139



    }










140



    for (const auto& [src, w] : diffs_to) {




354,148✔





141



        delta.emplace_back(src, vert, w);




177,900✔





142



    }










143



    apply_delta(delta);




176,248✔





144



    close_after_assign_vertex(vert);




176,248✔





145












146



    if (lb_edge) {




176,248✔





147



        g_.update_edge(vert, *lb_edge, 0);




108,020✔





148



    }










149



    if (ub_edge) {




176,248✔





150



        g_.update_edge(0, *ub_edge, vert);




104,336✔





151



    }










152



    return vert;




176,248✔





153



}




176,248✔





154












155



Weight SplitDBM::potential_at(const VertId v) const { return potential_[v]; }




132,744✔





156












157



Weight SplitDBM::potential_at_zero() const { return potential_[0]; }




358,162✔





158












159



std::size_t SplitDBM::graph_size() const { return g_.size(); }




406✔





160



std::size_t SplitDBM::num_edges() const { return g_.num_edges(); }




×







161












162



bool SplitDBM::vertex_has_edges(const VertId v) const { return g_.succs(v).size() > 0 || g_.preds(v).size() > 0; }




889,200✔





163












164



std::vector<VertId> SplitDBM::get_disconnected_vertices() const {




49,810✔





165



    std::vector<VertId> result;




49,810✔





166



    for (VertId v : g_.verts()) {




2,728,963✔





167



        if (v == 0) {




1,786,102✔





168



            continue;




49,810✔





169



        }










170



        if (!vertex_has_edges(v)) {




1,781,303✔





171



            result.push_back(v);




39,422✔





172



        }










173



    }










174



    return result;




49,810✔





175



}




×







176












177



bool SplitDBM::strengthen_bound(const VertId v, const Side side, const Weight& bound_value) {




588✔





178



    if (side == Side::LEFT) {




588✔





179



        const Weight edge_weight = -bound_value;




294✔





180



        const auto w = g_.lookup(v, 0);




294✔





181



        if (!w || edge_weight >= *w) {




294✔





182



            return true;




266✔





183



        }










184



        g_.set_edge(v, edge_weight, 0);




28✔





185



        if (!repair_potential(v, 0)) {




28✔





186



            return false;










187



        }










188



        for (const auto& e : g_.e_preds(v)) {




88✔





189



            if (e.vert == 0) {




60✔





190



                continue;




28✔





191



            }










192



            g_.update_edge(e.vert, e.val + edge_weight, 0);




32✔





193



            if (!repair_potential(e.vert, 0)) {




32✔





194



                return false;




×







195



            }










196



        }










197



    } else {










198



        const auto w = g_.lookup(0, v);




294✔





199



        if (!w || bound_value >= *w) {




294✔





200



            return true;




145✔





201



        }










202



        g_.set_edge(0, bound_value, v);




4✔





203



        if (!repair_potential(0, v)) {




4✔





204



            return false;










205



        }










206



        for (const auto& e : g_.e_succs(v)) {




12✔





207



            if (e.vert == 0) {




8✔





208



                continue;




4✔





209



            }










210



            g_.update_edge(0, e.val + bound_value, e.vert);




4✔





211



            if (!repair_potential(0, e.vert)) {




4✔





212



                return false;




×







213



            }










214



        }










215



    }










216



    return true;




16✔





217



}










218












219



void SplitDBM::normalize() {




1,125,260✔





220



    if (unstable_.empty()) {




1,125,260✔





221



        return;




1,125,180✔





222



    }










223












224



    // close_after_widen expects an is_stable predicate: returns true iff v is stable.










225



    // Vertices in unstable_ are NOT stable, so we negate the membership test.










226



    struct IsStable {




40✔





227



        const VertSet& unstable;










228



        explicit IsStable(const VertSet& s) : unstable(s) {}




80✔





229



        bool operator[](const VertId v) const { return !unstable.contains(v); }




268✔





230



    };










231












232



    const auto p = [this](const VertId v) { return potential_[v]; };




1,476✔





233



    apply_delta(close_after_widen(*scratch_, SubGraph(g_, 0), p, IsStable(unstable_)));




120✔





234



    apply_delta(close_after_assign(*scratch_, g_, p, 0));




120✔





235












236



    unstable_.clear();




80✔





237



}










238












239



void SplitDBM::clear_thread_local_state() { scratch_.clear(); }




1,442✔





240












241



bool SplitDBM::is_subsumed_by(const SplitDBM& left, const SplitDBM& right, const std::vector<VertId>& perm) {




406✔





242



    const Graph& g = left.g_;




406✔





243



    const Graph& og = right.g_;




406✔





244












245



    for (const VertId ox : og.verts()) {




1,795✔





246



        if (og.succs(ox).size() == 0) {




1,030✔





247



            continue;




50✔





248



        }










249












250



        const VertId x = perm[ox];




980✔





251



        for (const auto& edge : og.e_succs(ox)) {




2,624✔





252



            const VertId oy = edge.vert;




1,748✔





253



            const VertId y = perm[oy];




1,748✔





254



            Weight ow = edge.val;




1,748✔





255












256



            if (const auto w = g.lookup(x, y)) {




1,748✔





257



                if (*w <= ow) {




1,722✔





258



                    continue;




1,644✔





259



                }










260



            }










261












262



            if (const auto wx = g.lookup(x, 0)) {




128✔





263



                if (const auto wy = g.lookup(0, y)) {




28✔





264



                    if (*wx + *wy <= ow) {




24✔





265



                        continue;




24✔





266



                    }










267



                }










268



            }










269



            return false;




104✔





270



        }










271



    }










272



    return true;




302✔





273



}










274












275



SplitDBM SplitDBM::join(const AlignedPair& aligned) {




49,810✔





276



    const auto& perm_x = aligned.left_perm;




49,810✔





277



    const auto& perm_y = aligned.right_perm;




49,810✔





278



    const auto& left = aligned.left;




49,810✔





279



    const auto& right = aligned.right;




49,810✔





280



    const size_t sz = aligned.size();




49,810✔





281












282



    // Build potentials for the aligned vertices










283



    std::vector<Weight> pot_left, pot_right;




49,810✔





284



    pot_left.reserve(sz);




49,810✔





285



    pot_right.reserve(sz);




49,810✔





286



    for (size_t i = 0; i < sz; ++i) {




1,835,912✔





287



        pot_left.push_back(left.potential_[perm_x[i]] - left.potential_[0]);




1,786,102✔





288



        pot_right.push_back(right.potential_[perm_y[i]] - right.potential_[0]);




1,786,102✔





289



    }










290



    pot_left[0] = 0;




49,810✔





291



    pot_right[0] = 0;




49,810✔





292












293



    // Build aligned views of the graphs










294



    GraphPerm gx(perm_x, left.g_);




49,810✔





295



    GraphPerm gy(perm_y, right.g_);




49,810✔





296












297



    // Compute deferred relations and close










298



    auto g_deferred_right = compute_deferred(gx, gy, sz);




49,810✔





299



    auto g_closed_left = close_deferred(*scratch_, gx, g_deferred_right, pot_left);




49,810✔





300



    auto g_deferred_left = compute_deferred(gy, gx, sz);




49,810✔





301



    auto g_closed_right = close_deferred(*scratch_, gy, g_deferred_left, pot_right);




49,810✔





302












303



    // Syntactic join of the closed graphs










304



    Graph result_g(graph_join(g_closed_left, g_closed_right));




49,810✔





305












306



    // Reapply missing independent relations










307



    SubGraph gx_excl(gx, 0);




49,810✔





308



    std::vector<VertId> lb_up, lb_down, ub_up, ub_down;




49,810✔





309



    for (VertId v : gx_excl.verts()) {




2,654,248✔





310



        if (auto wx = gx.lookup(0, v)) {




1,736,292✔





311



            if (auto wy = gy.lookup(0, v)) {




1,520,464✔





312



                if (*wx < *wy) {




1,517,026✔





313



                    ub_up.push_back(v);




19,138✔





314



                }










315



                if (*wy < *wx) {




1,517,026✔





316



                    ub_down.push_back(v);




28,664✔





317



                }










318



            }










319



        }










320



        if (auto wx = gx.lookup(v, 0)) {




1,736,292✔





321



            if (auto wy = gy.lookup(v, 0)) {




1,597,334✔





322



                if (*wx < *wy) {




1,594,086✔





323



                    lb_down.push_back(v);




13,524✔





324



                }










325



                if (*wy < *wx) {




1,594,086✔





326



                    lb_up.push_back(v);




32,218✔





327



                }










328



            }










329



        }










330



    }










331












332



    for (VertId s : lb_up) {




82,028✔





333



        Weight left_lb = gx.edge_val(s, 0);




32,218✔





334



        Weight right_lb = gy.edge_val(s, 0);




32,218✔





335



        for (VertId d : ub_up) {




82,520✔





336



            if (s != d) {




50,302✔





337



                result_g.update_edge(s, std::max(left_lb + gx.edge_val(0, d), right_lb + gy.edge_val(0, d)), d);




49,079✔





338



            }










339



        }










340



    }










341












342



    for (VertId s : lb_down) {




63,334✔





343



        Weight left_lb = gx.edge_val(s, 0);




13,524✔





344



        Weight right_lb = gy.edge_val(s, 0);




13,524✔





345



        for (VertId d : ub_down) {




51,746✔





346



            if (s != d) {




38,222✔





347



                result_g.update_edge(s, std::max(left_lb + gx.edge_val(0, d), right_lb + gy.edge_val(0, d)), d);




33,170✔





348



            }










349



        }










350



    }










351












352



    return {std::move(result_g), std::move(pot_left), VertSet{}};




99,620✔





353



}




99,620✔





354












355



SplitDBM SplitDBM::widen(const AlignedPair& aligned) {




110✔





356



    const size_t sz = aligned.size();




110✔





357












358



    // Build potentials from left (widen uses left's potentials)










359



    std::vector<Weight> result_pot;




110✔





360



    result_pot.reserve(sz);




110✔





361



    for (size_t i = 0; i < sz; ++i) {




600✔





362



        result_pot.push_back(aligned.left.potential_[aligned.left_perm[i]] - aligned.left.potential_[0]);




490✔





363



    }










364



    result_pot[0] = 0;




110✔





365












366



    // Build aligned views










367



    const GraphPerm gx(aligned.left_perm, aligned.left.g_);




110✔





368



    const GraphPerm gy(aligned.right_perm, aligned.right.g_);




110✔





369












370



    // Perform the widening










371



    VertSet result_unstable(aligned.left.unstable_);




110✔





372



    Graph result_g(graph_widen(gx, gy, result_unstable));




110✔





373












374



    return {std::move(result_g), std::move(result_pot), std::move(result_unstable)};




220✔





375



}




275✔





376












377



std::optional<SplitDBM> SplitDBM::meet(AlignedPair& aligned) {




54✔





378



    // Build aligned views










379



    const GraphPerm gx(aligned.left_perm, aligned.left.g_);




54✔





380



    const GraphPerm gy(aligned.right_perm, aligned.right.g_);




54✔





381












382



    // Compute the syntactic meet of the aligned graphs










383



    bool is_closed{};




54✔





384



    Graph result_g(graph_meet(gx, gy, is_closed));




54✔





385












386



    // Select valid potentials using Bellman-Ford (updates initial_potentials in place)










387



    auto& result_pot = aligned.initial_potentials;




54✔





388



    if (!select_potentials(*scratch_, result_g, result_pot)) {




54✔





389



        return std::nullopt; // Infeasible




×







390



    }










391












392



    if (!is_closed) {




54✔





393



        const auto p = [&result_pot](const VertId v) { return result_pot[v]; };




38,184✔





394



        splitdbm::apply_delta(result_g, close_after_meet(*scratch_, SubGraph(result_g, 0), p, gx, gy));




54✔





395



        splitdbm::apply_delta(result_g, close_after_assign(*scratch_, result_g, p, 0));




81✔





396



    }










397












398



    return SplitDBM(std::move(result_g), std::move(result_pot), VertSet{});




108✔





399



}




108✔





400












401



} // namespace splitdbm
























    

  • 

    •