Alan-Jowett / ebpf-verifier / 21765175576

coverage: 86.699% (-0.09%) from 86.792%
21765175576

push

github

web-flow 
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>

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

98.03
/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



PotentialFunction SplitDBM::pot_func(const std::vector<Weight>& p) {




1,874,106✔






10



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




692,291,255✔





11



}










12













13



SplitDBM::SplitDBM() {




2,377,374✔






14



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




2,377,374✔






15



    potential_.emplace_back(0);




2,377,374✔






16



}




2,377,374✔





17













18



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




99,402✔






19



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




99,402✔






20



    normalize();




99,402✔






21



}




99,402✔





22













23



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




263,340✔





24













25



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




35,085,176✔






26



    if (side == Side::LEFT) {




35,085,176✔






27



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




26,439,583✔





28



    } else {











29



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




17,492,019✔





30



    }










31



}










32












33



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











34



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




737,988✔






35



    if (side == Side::LEFT) {




737,988✔






36



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




565,014✔





37



    } else {











38



        g_.set_edge(0, bound_value, v);




361,312✔





39



    }











40



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




737,988✔






41



}




737,988✔





42













43



VertId SplitDBM::new_vertex() {




1,274,312✔






44



    const VertId vert = g_.new_vertex();




1,274,312✔






45



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




1,274,312✔






46



        potential_.emplace_back(0);




671,752✔





47



    } else {











48



        potential_[vert] = Weight(0);




602,560✔





49



    }











50



    return vert;




1,274,312✔





51



}










52













53



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




559,740✔





54













55



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




1,892✔





56













57



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




1,383,302✔






58



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




1,383,302✔





59



}










60













61



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




1,512,988✔






62



    if (side == Side::LEFT) {




1,512,988✔






63



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




771,762✔






64



            if (*w <= -new_bound) {




106,802✔






65



                return true;




42,189✔





66



            }










67



        }











68



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




687,384✔






69



        return repair_potential(v, 0);




687,384✔





70



    } else {











71



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




741,226✔






72



            if (*w <= new_bound) {




101,554✔






73



                return true;




31,121✔





74



            }










75



        }











76



        g_.set_edge(0, new_bound, v);




678,984✔






77



        return repair_potential(0, v);




678,984✔





78



    }










79



}










80













81



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




16,860✔






82



    g_.update_edge(src, k, dest);




16,860✔






83



    if (!repair_potential(src, dest)) {




16,860✔






84



        return false;




240✔





85



    }











86



    close_over_edge(g_, src, dest);




16,380✔






87



    return true;




16,380✔





88



}










89













90



void SplitDBM::close_after_bound_updates() { apply_delta(close_after_assign(*scratch_, g_, pot_func(potential_), 0)); }




2,235,582✔





91













92



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




1,768,363✔





93













94



void SplitDBM::close_after_assign_vertex(const VertId v) {




185,234✔






95



    apply_delta(close_after_assign(*scratch_, SubGraph(g_, 0), pot_func(potential_), v));




277,851✔






96



}




185,234✔





97













98



VertId SplitDBM::assign_vertex(const Weight& potential_value,




185,234✔





99



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










100



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










101



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











102



    const VertId vert = new_vertex();




185,234✔






103



    potential_[vert] = potential_value;




185,234✔





104













105



    EdgeVector delta;




185,234✔






106



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




185,234✔






107



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




372,118✔






108



        delta.emplace_back(vert, dest, w);




186,884✔





109



    }











110



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




372,116✔






111



        delta.emplace_back(src, vert, w);




186,882✔





112



    }











113



    apply_delta(delta);




185,234✔






114



    close_after_assign_vertex(vert);




185,234✔





115













116



    if (lb_edge) {




185,234✔






117



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




116,894✔





118



    }











119



    if (ub_edge) {




185,234✔






120



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




113,246✔





121



    }











122



    return vert;




185,234✔






123



}




185,234✔





124













125



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




140,952✔





126













127



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




375,496✔





128













129



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




794✔






NEW


130



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




×







131













132



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




1,450,343✔





133













134



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




99,188✔






135



    std::vector<VertId> result;




99,188✔






136



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




3,056,090✔






137



        if (v == 0) {




2,956,902✔






138



            continue;




99,188✔





139



        }











140



        if (!vertex_has_edges(v)) {




2,927,476✔






141



            result.push_back(v);




39,546✔





142



        }










143



    }











144



    return result;




99,188✔






NEW


145



}




×







146













147



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




4,668✔






148



    if (side == Side::LEFT) {




4,668✔






149



        const Weight edge_weight = -bound_value;




2,334✔






150



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




2,334✔






151



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




2,334✔






152



            return true;




2,304✔





153



        }











154



        g_.set_edge(v, edge_weight, 0);




30✔






155



        if (!repair_potential(v, 0)) {




30✔





156



            return false;










157



        }











158



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




96✔






159



            if (e.vert == 0) {




66✔






160



                continue;




30✔





161



            }











162



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




36✔






163



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




36✔






NEW


164



                return false;




×







165



            }











166



        }




66✔






167



    } else {




2,334✔






168



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




2,334✔






169



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




2,334✔






170



            return true;




2,330✔





171



        }











172



        g_.set_edge(0, bound_value, v);




4✔






173



        if (!repair_potential(0, v)) {




4✔





174



            return false;










175



        }











176



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




12✔






177



            if (e.vert == 0) {




8✔






178



                continue;




4✔





179



            }











180



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




4✔






181



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




4✔






NEW


182



                return false;




×







183



            }











184



        }




8✔





185



    }











186



    return true;




17✔





187



}










188













189



void SplitDBM::normalize() {




2,980,662✔






190



    if (unstable_.empty()) {




2,980,662✔






191



        return;




2,980,600✔





192



    }










193













194



    struct UnstableWrap {




31✔





195



        const VertSet& vs;











196



        explicit UnstableWrap(const VertSet& s) : vs(s) {}




62✔






197



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




168✔





198



    };










199













200



    const auto p = pot_func(potential_);




62✔






201



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




93✔






202



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




93✔





203













204



    unstable_.clear();




62✔






205



}




62✔





206













207



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




1,408✔





208












209



// =============================================================================










210



// SplitDBM static lattice method implementations










211



// =============================================================================










212













213



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




794✔






214



    const Graph& g = left.g_;




794✔






215



    const Graph& og = right.g_;




794✔





216













217



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




2,572✔






218



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




1,876✔






219



            continue;




48✔





220



        }










221













222



        const VertId x = perm[ox];




1,828✔






223



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




4,208✔






224



            const VertId oy = edge.vert;




2,478✔






225



            const VertId y = perm[oy];




2,478✔






226



            Weight ow = edge.val;




2,478✔





227













228



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




2,478✔






229



                if (*w <= ow) {




2,444✔






230



                    continue;




2,348✔





231



                }










232



            }










233













234



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




130✔






235



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




40✔






236



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




32✔






237



                        continue;




32✔





238



                    }










239



                }










240



            }











241



            return false;




98✔






242



        }




3,717✔





243



    }











244



    return true;




696✔





245



}










246













247



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




99,188✔






248



    const auto& perm_x = aligned.left_perm;




99,188✔






249



    const auto& perm_y = aligned.right_perm;




99,188✔






250



    const auto& left = aligned.left;




99,188✔






251



    const auto& right = aligned.right;




99,188✔






252



    const size_t sz = aligned.size();




99,188✔





253












254



    // Build potentials for the aligned vertices











255



    std::vector<Weight> pot_left, pot_right;




99,188✔






256



    pot_left.reserve(sz);




99,188✔






257



    pot_right.reserve(sz);




99,188✔






258



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




3,056,090✔






259



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




4,435,353✔






260



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




4,435,353✔





261



    }











262



    pot_left[0] = 0;




99,188✔






263



    pot_right[0] = 0;




99,188✔





264












265



    // Build aligned views of the graphs











266



    GraphPerm gx(perm_x, left.g_);




99,188✔






267



    GraphPerm gy(perm_y, right.g_);




99,188✔





268












269



    // Compute deferred relations: bounds from left applied to relations from right











270



    Graph g_deferred_right;




99,188✔






271



    g_deferred_right.growTo(sz);




99,188✔






272



    SubGraph gy_excl(gy, 0);




99,188✔






273



    for (VertId s : gy_excl.verts()) {




5,814,619✔






274



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




5,200,813✔






275



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




1,562,066✔






276



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




1,453,472✔






277



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




2,150,421✔





278



                }










279



            }










280



        }










281



    }










282












283



    // Apply deferred relations to right and re-close











284



    bool is_closed;




49,594✔






285



    Graph g_closed_left(graph_meet(gx, g_deferred_right, is_closed));




99,188✔






286



    if (!is_closed) {




99,188✔






287



        splitdbm::apply_delta(g_closed_left, close_after_meet(*scratch_, SubGraph(g_closed_left, 0), pot_func(pot_left),




99,188✔





288



                                                              gx, g_deferred_right));










289



    }










290












291



    // Compute deferred relations: bounds from right applied to relations from left











292



    Graph g_deferred_left;




99,188✔






293



    g_deferred_left.growTo(sz);




99,188✔






294



    SubGraph gx_excl(gx, 0);




99,188✔






295



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




5,814,619✔






296



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




5,391,625✔






297



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




1,689,274✔






298



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




1,581,088✔






299



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




2,341,962✔





300



                }










301



            }










302



        }










303



    }










304













305



    Graph g_closed_right(graph_meet(gy, g_deferred_left, is_closed));




99,188✔






306



    if (!is_closed) {




99,188✔






307



        splitdbm::apply_delta(g_closed_right, close_after_meet(*scratch_, SubGraph(g_closed_right, 0),




99,188✔






308



                                                               pot_func(pot_right), gy, g_deferred_left));




198,376✔





309



    }










310












311



    // Syntactic join of the closed graphs











312



    Graph result_g(graph_join(g_closed_left, g_closed_right));




99,188✔





313












314



    // Reapply missing independent relations











315



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




99,188✔






316



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




5,814,619✔






317



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




2,857,714✔






318



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




2,642,020✔






319



                if (*wx < *wy) {




2,638,608✔






320



                    ub_up.push_back(v);




19,824✔





321



                }











322



                if (*wy < *wx) {




2,638,608✔






323



                    ub_down.push_back(v);




34,236✔





324



                }










325



            }










326



        }











327



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




2,857,714✔






328



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




2,718,422✔






329



                if (*wx < *wy) {




2,715,196✔






330



                    lb_down.push_back(v);




15,204✔





331



                }











332



                if (*wy < *wx) {




2,715,196✔






333



                    lb_up.push_back(v);




34,404✔





334



                }










335



            }










336



        }










337



    }










338













339



    for (VertId s : lb_up) {




133,592✔






340



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




34,404✔






341



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




34,404✔






342



        for (VertId d : ub_up) {




82,544✔






343



            if (s != d) {




48,140✔






344



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




53,535✔





345



            }










346



        }











347



    }




34,404✔





348













349



    for (VertId s : lb_down) {




114,392✔






350



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




15,204✔






351



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




15,204✔






352



        for (VertId d : ub_down) {




55,260✔






353



            if (s != d) {




40,056✔






354



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




44,472✔





355



            }










356



        }











357



    }




15,204✔





358













359



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




198,376✔






360



}




198,376✔





361













362



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




168✔






363



    const auto& perm_left = aligned.left_perm;




168✔






364



    const auto& perm_right = aligned.right_perm;




168✔






365



    const auto& left = aligned.left;




168✔






366



    const auto& right = aligned.right;




168✔






367



    const size_t sz = aligned.size();




168✔





368












369



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











370



    std::vector<Weight> result_pot;




168✔






371



    result_pot.reserve(sz);




168✔






372



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




682✔






373



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




771✔





374



    }











375



    result_pot[0] = 0;




168✔





376












377



    // Build aligned views











378



    const GraphPerm gx(perm_left, left.g_);




168✔






379



    const GraphPerm gy(perm_right, right.g_);




168✔





380












381



    // Perform the widening











382



    VertSet result_unstable(left.unstable_);




168✔






383



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




168✔





384













385



    return SplitDBM(std::move(result_g), std::move(result_pot), std::move(result_unstable));




336✔






386



}




420✔





387













388



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




46✔






389



    const auto& perm_left = aligned.left_perm;




46✔






390



    const auto& perm_right = aligned.right_perm;




46✔






391



    const auto& left = aligned.left;




46✔






392



    const auto& right = aligned.right;




46✔





393












394



    // Build aligned views











395



    const GraphPerm gx(perm_left, left.g_);




46✔






396



    const GraphPerm gy(perm_right, right.g_);




46✔





397












398



    // Compute the syntactic meet of the aligned graphs











399



    bool is_closed{};




46✔






400



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




46✔





401












402



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











403



    auto& result_pot = aligned.initial_potentials;




46✔






404



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




46✔






NEW


405



        return std::nullopt; // Infeasible




×







406



    }










407













408



    if (!is_closed) {




46✔






409



        const auto potential_func = pot_func(result_pot);




46✔






410



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




46✔






411



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




46✔






412



    }




46✔





413













414



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




92✔






415



}




92✔





416












417



} // namespace splitdbm
























    

  • 

    •