From bc91973016414796a3a45eece7841e9bc41e66d9 Mon Sep 17 00:00:00 2001 From: Elazar Gershuni Date: Mon, 2 Dec 2024 19:45:04 +0200 Subject: [PATCH] specialize GraphOps * only include graph_ops.hpp from split_dbm.cpp * pass function to Heap, remove type parameter * use inline thread_local static members * add WeightIndexable concept, preparing switch from template to a function (using operator() instead of operator[]) * inline classes dedicated to operator overloading * add consts Signed-off-by: Elazar Gershuni --- src/crab/split_dbm.cpp | 47 +++++---- src/crab/split_dbm.hpp | 7 +- src/crab_utils/graph_ops.hpp | 188 ++++++++++++++--------------------- src/crab_utils/heap.hpp | 14 +-- src/main/linux_verifier.cpp | 2 +- 5 files changed, 113 insertions(+), 145 deletions(-) diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp index 29d61a222..dc449c5ba 100644 --- a/src/crab/split_dbm.cpp +++ b/src/crab/split_dbm.cpp @@ -6,6 +6,7 @@ #include "crab/split_dbm.hpp" #include "crab_utils/debug.hpp" +#include "crab_utils/graph_ops.hpp" #include "crab_utils/stats.hpp" #include "string_constraints.hpp" #include "type_encoding.hpp" @@ -278,9 +279,9 @@ bool SplitDBM::add_linear_leq(const linear_expression_t& exp) { if (!repair_potential(src, dest)) { return false; } - GrOps::close_over_edge(g, src, dest); + GraphOps::close_over_edge(g, src, dest); } - GrOps::apply_delta(g, GrOps::close_after_assign(g, potential, 0)); + GraphOps::apply_delta(g, GraphOps::close_after_assign(g, potential, 0)); normalize(); return true; } @@ -501,9 +502,9 @@ SplitDBM SplitDBM::operator|(const SplitDBM& o) const& { } // Apply the deferred relations, and re-close. bool is_closed; - graph_t g_rx(GrOps::meet(gx, g_ix_ry, is_closed)); + graph_t g_rx(GraphOps::meet(gx, g_ix_ry, is_closed)); if (!is_closed) { - GrOps::apply_delta(g_rx, GrOps::close_after_meet(SubGraph(g_rx, 0), pot_rx, gx, g_ix_ry)); + GraphOps::apply_delta(g_rx, GraphOps::close_after_meet(SubGraph(g_rx, 0), pot_rx, gx, g_ix_ry)); } graph_t g_rx_iy; @@ -522,14 +523,14 @@ SplitDBM SplitDBM::operator|(const SplitDBM& o) const& { } } // Similarly, should use a SubGraph view. - graph_t g_ry(GrOps::meet(gy, g_rx_iy, is_closed)); + graph_t g_ry(GraphOps::meet(gy, g_rx_iy, is_closed)); if (!is_closed) { - GrOps::apply_delta(g_ry, GrOps::close_after_meet(SubGraph(g_ry, 0), pot_ry, gy, g_rx_iy)); + GraphOps::apply_delta(g_ry, GraphOps::close_after_meet(SubGraph(g_ry, 0), pot_ry, gy, g_rx_iy)); } // We now have the relevant set of relations. Because g_rx and g_ry are closed, // the result is also closed. - graph_t join_g(GrOps::join(g_rx, g_ry)); + graph_t join_g(GraphOps::join(g_rx, g_ry)); // Now reapply the missing independent relations. // Need to derive vert_ids from lb_up/lb_down, and make sure the vertices exist @@ -646,7 +647,7 @@ SplitDBM SplitDBM::widen(const SplitDBM& o) const { // Now perform the widening vert_set_t widen_unstable(unstable); - graph_t widen_g(GrOps::widen(gx, gy, widen_unstable)); + graph_t widen_g(GraphOps::widen(gx, gy, widen_unstable)); SplitDBM res(std::move(out_vmap), std::move(out_revmap), std::move(widen_g), std::move(widen_pot), std::move(widen_unstable)); @@ -717,23 +718,23 @@ std::optional SplitDBM::meet(const SplitDBM& o) const { GraphPerm gy(perm_y, o.g); // Compute the syntactic meet of the permuted graphs. - bool is_closed; - graph_t meet_g(GrOps::meet(gx, gy, is_closed)); + bool is_closed{}; + graph_t meet_g(GraphOps::meet(gx, gy, is_closed)); // Compute updated potentials on the zero-enriched graph // vector meet_pi(meet_g.size()); // We've warm-started pi with the operand potentials - if (!GrOps::select_potentials(meet_g, meet_pi)) { + if (!GraphOps::select_potentials(meet_g, meet_pi)) { // Potentials cannot be selected -- state is infeasible. return {}; } if (!is_closed) { - GrOps::apply_delta(meet_g, GrOps::close_after_meet(SubGraph(meet_g, 0), meet_pi, gx, gy)); + GraphOps::apply_delta(meet_g, GraphOps::close_after_meet(SubGraph(meet_g, 0), meet_pi, gx, gy)); // Recover updated LBs and UBs.< - GrOps::apply_delta(meet_g, GrOps::close_after_assign(meet_g, meet_pi, 0)); + GraphOps::apply_delta(meet_g, GraphOps::close_after_assign(meet_g, meet_pi, 0)); } SplitDBM res(std::move(meet_verts), std::move(meet_rev), std::move(meet_g), std::move(meet_pi), vert_set_t()); CRAB_LOG("zones-split", std::cout << "Result meet:\n" << res << "\n"); @@ -878,7 +879,7 @@ void SplitDBM::assign(variable_t lhs, const linear_expression_t& e) { } { - edge_vector delta; + GraphOps::edge_vector delta; for (const auto& [var, n] : diffs_lb) { delta.emplace_back(vert, get_vert(var), -n); } @@ -888,9 +889,9 @@ void SplitDBM::assign(variable_t lhs, const linear_expression_t& e) { } // apply_delta should be safe here, as x has no edges in G. - GrOps::apply_delta(g, delta); + GraphOps::apply_delta(g, delta); } - GrOps::apply_delta(g, GrOps::close_after_assign(SubGraph(g, 0), potential, vert)); + GraphOps::apply_delta(g, GraphOps::close_after_assign(SubGraph(g, 0), potential, vert)); if (lb_w) { g.update_edge(vert, *lb_w, 0); @@ -926,6 +927,12 @@ class vert_set_wrap_t { const SplitDBM::vert_set_t& vs; }; +bool SplitDBM::repair_potential(vert_id src, vert_id dest) { + return GraphOps::repair_potential(g, potential, src, dest); +} + +void SplitDBM::clear_thread_local_state() { GraphOps::clear_thread_local_state(); } + void SplitDBM::normalize() { CrabStats::count("SplitDBM.count.normalize"); ScopedCrabStats __st__("SplitDBM.normalize"); @@ -936,12 +943,12 @@ void SplitDBM::normalize() { return; } - edge_vector delta; - // GrOps::close_after_widen(g, potential, vert_set_wrap_t(unstable), delta); + GraphOps::edge_vector delta; + // GraphOps::close_after_widen(g, potential, vert_set_wrap_t(unstable), delta); // GKG: Check - GrOps::apply_delta(g, GrOps::close_after_widen(SubGraph(g, 0), potential, vert_set_wrap_t(unstable))); + GraphOps::apply_delta(g, GraphOps::close_after_widen(SubGraph(g, 0), potential, vert_set_wrap_t(unstable))); // Retrieve variable bounds - GrOps::apply_delta(g, GrOps::close_after_assign(g, potential, 0)); + GraphOps::apply_delta(g, GraphOps::close_after_assign(g, potential, 0)); unstable.clear(); } diff --git a/src/crab/split_dbm.hpp b/src/crab/split_dbm.hpp index 8ec93be2c..f508dea79 100644 --- a/src/crab/split_dbm.hpp +++ b/src/crab/split_dbm.hpp @@ -31,7 +31,6 @@ #include "crab/variable.hpp" #include "crab_utils/adapt_sgraph.hpp" #include "crab_utils/debug.hpp" -#include "crab_utils/graph_ops.hpp" #include "crab_utils/num_big.hpp" #include "crab_utils/num_safeint.hpp" #include "crab_utils/stats.hpp" @@ -57,8 +56,6 @@ class SplitDBM final { using variable_vector_t = std::vector; using rev_map_t = std::vector>; - using GrOps = GraphOps; - using edge_vector = GrOps::edge_vector; // < , k> == x - y <= k. using diffcst_t = std::pair, Weight>; using vert_set_t = std::unordered_set; @@ -129,7 +126,7 @@ class SplitDBM final { interval_t get_interval(variable_t x, int finite_width) const; // Restore potential after an edge addition - bool repair_potential(vert_id src, vert_id dest) { return GrOps::repair_potential(g, potential, src, dest); } + bool repair_potential(vert_id src, vert_id dest); void normalize(); @@ -304,7 +301,7 @@ class SplitDBM final { string_invariant to_set() const; public: - static void clear_thread_local_state() { GraphOps::clear_thread_local_state(); } + static void clear_thread_local_state(); }; // class SplitDBM } // namespace domains diff --git a/src/crab_utils/graph_ops.hpp b/src/crab_utils/graph_ops.hpp index 931a1694f..8c26d0935 100644 --- a/src/crab_utils/graph_ops.hpp +++ b/src/crab_utils/graph_ops.hpp @@ -6,7 +6,9 @@ #include #include +#include +#include "crab_utils/adapt_sgraph.hpp" #include "crab_utils/heap.hpp" #include "crab_utils/lazy_allocator.hpp" #include "crab_utils/num_safety.hpp" @@ -482,30 +484,25 @@ class GraphRev { G& g; }; -// Comparator for use with min-heaps. -template -class DistComp { - public: - explicit DistComp(V& _A) : A(_A) {} - bool operator()(int x, int y) const { return A[x] < A[y]; } - V& A; +// temporary concept: indexable +// TODO: replace everywhere with simple callable +template +concept WeightIndexable = requires(T t, AdaptGraph::vert_id v) { + { t[v] } -> std::convertible_to; }; // GKG - What's the best way to split this out? -template class GraphOps { public: - using Weight = typename Gr::Weight; // The following code assumes vert_id is an integer. - using graph_t = Gr; + using graph_t = AdaptGraph; + using Weight = typename graph_t::Weight; using vert_id = typename graph_t::vert_id; + using WeightVector = std::vector; using mut_val_ref_t = typename graph_t::mut_val_ref_t; using edge_vector = std::vector>; - using WtComp = DistComp>; - using WtHeap = Heap; - using edge_ref = std::tuple; //=========================================== @@ -517,27 +514,26 @@ class GraphOps { enum SMarkT { V_UNSTABLE = 0, V_STABLE = 1 }; // Whether a vertex is in the current SCC/queue for Bellman-Ford. enum QMarkT { BF_NONE = 0, BF_SCC = 1, BF_QUEUED = 2 }; - // =========================================== + // Scratch space needed by the graph algorithms. // Should really switch to some kind of arena allocator, rather // than having all these static structures. - // =========================================== - static thread_local lazy_allocator> edge_marks; + static inline thread_local lazy_allocator> edge_marks; // Used for Bellman-Ford queueing - static thread_local lazy_allocator> dual_queue; - static thread_local lazy_allocator> vert_marks; - static thread_local size_t scratch_sz; + static inline thread_local lazy_allocator> dual_queue; + static inline thread_local lazy_allocator> vert_marks; + static inline thread_local size_t scratch_sz; // For locality, should combine dists & dist_ts. // Weight must have an empty constructor, but does _not_ need a top or infty element. // dist_ts tells us which distances are current, and ts_idx prevents wraparound problems, // in the unlikely circumstance that we have more than 2^sizeof(uint) iterations. - static thread_local lazy_allocator> dists; - static thread_local lazy_allocator> dists_alt; - static thread_local lazy_allocator> dist_ts; - static thread_local unsigned int ts; - static thread_local unsigned int ts_idx; + static inline thread_local lazy_allocator> dists; + static inline thread_local lazy_allocator> dists_alt; + static inline thread_local lazy_allocator> dist_ts; + static inline thread_local unsigned int ts; + static inline thread_local unsigned int ts_idx; static void clear_thread_local_state() { dists.clear(); @@ -582,15 +578,15 @@ class GraphOps { static graph_t join(auto& l, auto& r) { // For the join, potentials are preserved assert(l.size() == r.size()); - size_t sz = l.size(); + const size_t sz = l.size(); graph_t g; g.growTo(sz); mut_val_ref_t wr; - for (vert_id s : l.verts()) { + for (const vert_id s : l.verts()) { for (const auto e : l.e_succs(s)) { - vert_id d = e.vert; + const vert_id d = e.vert; if (r.lookup(s, d, &wr)) { g.add_edge(s, std::max(e.val, static_cast(wr)), d); } @@ -622,12 +618,12 @@ class GraphOps { static graph_t widen(const auto& l, const auto& r, std::unordered_set& unstable) { assert(l.size() == r.size()); - size_t sz = l.size(); + const size_t sz = l.size(); graph_t g; g.growTo(sz); - for (vert_id s : r.verts()) { + for (const vert_id s : r.verts()) { for (const auto e : r.e_succs(s)) { - vert_id d = e.vert; + const vert_id d = e.vert; if (auto wl = l.lookup(s, d)) { if (e.val <= *wl) { g.add_edge(s, *wl, d); @@ -636,7 +632,7 @@ class GraphOps { } // Check if this vertex is stable - for (vert_id d : l.succs(s)) { + for (const vert_id d : l.succs(s)) { if (!g.elem(s, d)) { unstable.insert(s); break; @@ -660,7 +656,7 @@ class GraphOps { stack.push_back(v); // Consider successors of v - for (vert_id w : x.succs(v)) { + for (const vert_id w : x.succs(v)) { if (!vert_marks->at(w)) { strong_connect(x, stack, index, w, sccs); dual_queue->at(v) = std::min(dual_queue->at(v), dual_queue->at(w)); @@ -706,8 +702,8 @@ class GraphOps { // Run Bellman-Ford to compute a valid model of a set of difference constraints. // Returns false if there is some negative cycle. - static bool select_potentials(const auto& g, auto& potentials) { - size_t sz = g.size(); + static bool select_potentials(const auto& g, WeightVector& potentials) { + const size_t sz = g.size(); assert(potentials.size() >= sz); grow_scratch(sz); @@ -726,7 +722,7 @@ class GraphOps { // Run Bellman-ford on each SCC. // Current implementation returns sccs in reverse topological order. - for (std::vector& scc : sccs) { + for (const std::vector& scc : sccs) { auto qhead = dual_queue->begin(); auto qtail = qhead; @@ -789,12 +785,12 @@ class GraphOps { return true; } - template - static edge_vector close_after_meet(const G& g, const P& pots, const G1& l, const G2& r) { + template + static edge_vector close_after_meet(const G& g, const WeightIndexable auto& pots, const G1& l, const G2& r) { // We assume the syntactic meet has already been computed, and potentials have been initialized. // We just want to restore closure. assert(l.size() == r.size()); - size_t sz = l.size(); + const size_t sz = l.size(); grow_scratch(sz); std::vector> colour_succs(2 * sz); @@ -803,13 +799,13 @@ class GraphOps { for (vert_id s : g.verts()) { for (const auto e : g.e_succs(s)) { unsigned char mark = 0; - vert_id d = e.vert; - if (auto w = l.lookup(s, d)) { + const vert_id d = e.vert; + if (const auto w = l.lookup(s, d)) { if (*w == e.val) { mark |= E_LEFT; } } - if (auto w = r.lookup(s, d)) { + if (const auto w = r.lookup(s, d)) { if (*w == e.val) { mark |= E_RIGHT; } @@ -849,12 +845,15 @@ class GraphOps { } } + static bool dists_compare(int x, int y) { return (*dists)[x] < (*dists)[y]; } + // P is some vector-alike holding a valid system of potentials. // Don't need to clear/initialize - template - static void chrome_dijkstra(const G& g, const P& p, std::vector>& colour_succs, vert_id src, + template + static void chrome_dijkstra(const G& g, const WeightIndexable auto& p, + std::vector>& colour_succs, vert_id src, std::vector>& out) { - size_t sz = g.size(); + const size_t sz = g.size(); if (sz == 0) { return; } @@ -867,11 +866,10 @@ class GraphOps { dists->at(src) = Weight(0); dist_ts->at(src) = ts; - WtComp comp(*dists); - WtHeap heap(comp); + Heap heap(dists_compare); for (const auto e : g.e_succs(src)) { - vert_id dest = e.vert; + const vert_id dest = e.vert; dists->at(dest) = p[src] + e.val - p[dest]; dist_ts->at(dest) = ts; @@ -880,11 +878,11 @@ class GraphOps { } while (!heap.empty()) { - int es = heap.removeMin(); - Weight es_cost = dists->at(es) + p[es]; // If it's on the queue, distance is not infinite. - Weight es_val = es_cost - p[src]; + const int es = heap.removeMin(); + const Weight es_cost = dists->at(es) + p[es]; // If it's on the queue, distance is not infinite. { - auto w = g.lookup(src, es); + const Weight es_val = es_cost - p[src]; + const auto w = g.lookup(src, es); if (!w || *w > es_val) { out.emplace_back(es, es_val); } @@ -895,10 +893,10 @@ class GraphOps { } // Pick the appropriate set of successors - std::vector& es_succs = + const std::vector& es_succs = (vert_marks->at(es) == E_LEFT) ? colour_succs[2 * es + 1] : colour_succs[2 * es]; for (vert_id ed : es_succs) { - Weight v = es_cost + g.edge_val(es, ed) - p[ed]; + const Weight v = es_cost + g.edge_val(es, ed) - p[ed]; if (dist_ts->at(ed) != ts || v < dists->at(ed)) { dists->at(ed) = v; dist_ts->at(ed) = ts; @@ -918,8 +916,8 @@ class GraphOps { // Run Dijkstra's algorithm, but similar to the chromatic algorithm, avoid expanding anything that _was_ stable. // GKG: Factor out common elements of this & the previous algorithm. - template - static void dijkstra_recover(const G& g, const P& p, const S& is_stable, vert_id src, + template + static void dijkstra_recover(const G& g, const WeightIndexable auto& p, const S& is_stable, vert_id src, std::vector>& out) { const size_t sz = g.size(); if (sz == 0) { @@ -938,11 +936,10 @@ class GraphOps { dists->at(src) = Weight(0); dist_ts->at(src) = ts; - WtComp comp(*dists); - WtHeap heap(comp); + Heap heap(dists_compare); for (const auto e : g.e_succs(src)) { - vert_id dest = e.vert; + const vert_id dest = e.vert; dists->at(dest) = p[src] + e.val - p[dest]; dist_ts->at(dest) = ts; @@ -951,10 +948,10 @@ class GraphOps { } while (!heap.empty()) { - int es = heap.removeMin(); - Weight es_cost = dists->at(es) + p[es]; // If it's on the queue, distance is not infinite. - Weight es_val = es_cost - p[src]; + const int es = heap.removeMin(); + const Weight es_cost = dists->at(es) + p[es]; // If it's on the queue, distance is not infinite. { + Weight es_val = es_cost - p[src]; auto w = g.lookup(src, es); if (!w || *w > es_val) { out.emplace_back(es, es_val); @@ -964,12 +961,12 @@ class GraphOps { continue; } - char es_mark = is_stable[es] ? V_STABLE : V_UNSTABLE; + const char es_mark = is_stable[es] ? V_STABLE : V_UNSTABLE; // Pick the appropriate set of successors for (const auto e : g.e_succs(es)) { - vert_id ed = e.vert; - Weight v = es_cost + e.val - p[ed]; + const vert_id ed = e.vert; + const Weight v = es_cost + e.val - p[ed]; if (dist_ts->at(ed) != ts || v < dists->at(ed)) { dists->at(ed) = v; dist_ts->at(ed) = ts; @@ -987,8 +984,8 @@ class GraphOps { } } - template - static bool repair_potential(const G& g, P& p, vert_id ii, vert_id jj) { + template + static bool repair_potential(const G& g, WeightVector& p, vert_id ii, vert_id jj) { // Ensure there's enough scratch space. const size_t sz = g.size(); // assert(src < (int) sz && dest < (int) sz); @@ -1004,8 +1001,7 @@ class GraphOps { return true; } - WtComp comp(*dists); - WtHeap heap(comp); + Heap heap(dists_compare); heap.insert(jj); @@ -1040,8 +1036,8 @@ class GraphOps { return true; } - template - static edge_vector close_after_widen(const G& g, const P& p, const V& is_stable) { + template + static edge_vector close_after_widen(const G& g, const WeightIndexable auto& p, const V& is_stable) { const size_t sz = g.size(); grow_scratch(sz); // assert(orig.size() == sz); @@ -1065,24 +1061,10 @@ class GraphOps { return delta; } - // Used for sorting successors of some vertex by increasing slack. - // operator() may only be called on vertices for which dists is initialized. - template - struct AdjCmp { - bool operator()(vert_id d1, vert_id d2) const { return dists->at(d1) - p[d1] < dists->at(d2) - p[d2]; } - const P& p; - }; - - template - struct NegP { - Weight operator[](vert_id v) const { return -(p[v]); } - const P& p; - }; - // Compute the transitive closure of edges reachable from v, assuming // (1) the subgraph G \ {v} is closed, and // (2) P is a valid model of G. - static void close_after_assign_fwd(const auto& g, const auto& p, vert_id v, + static void close_after_assign_fwd(const auto& g, const WeightIndexable auto& p, vert_id v, std::vector>& aux) { // Initialize the queue and distances. for (vert_id u : g.verts()) { @@ -1103,7 +1085,8 @@ class GraphOps { } // Sort the immediate edges by increasing slack. - std::sort(adj_head, adj_tail, AdjCmp{p}); + std::sort(adj_head, adj_tail, + [&p](vert_id d1, vert_id d2) { return dists->at(d1) - p[d1] < dists->at(d2) - p[d2]; }); auto reach_tail = adj_tail; for (; adj_head < adj_tail; ++adj_head) { @@ -1195,7 +1178,8 @@ class GraphOps { // Closure is now updated. } - static edge_vector close_after_assign(const auto& g, const auto& p, vert_id v) { + template + static edge_vector close_after_assign(const auto& g, const P& p, vert_id v) { const size_t sz = g.size(); grow_scratch(sz); edge_vector delta; @@ -1209,6 +1193,11 @@ class GraphOps { { std::vector> aux; GraphRev g_rev{g}; + + struct NegP { + Weight operator[](vert_id v) const { return -(p[v]); } + const P& p; + }; close_after_assign_fwd(g_rev, NegP{p}, v, aux); for (const auto& [vid, wt] : aux) { delta.emplace_back(vid, v, wt); @@ -1218,29 +1207,4 @@ class GraphOps { } }; -// Static data allocation -template -thread_local lazy_allocator> GraphOps::edge_marks; - -// Used for Bellman-Ford queueing -template -thread_local lazy_allocator::vert_id>> GraphOps::dual_queue; - -template -thread_local lazy_allocator> GraphOps::vert_marks; - -template -thread_local size_t GraphOps::scratch_sz = 0; - -template -thread_local lazy_allocator> GraphOps::dists; -template -thread_local lazy_allocator> GraphOps::dists_alt; -template -thread_local lazy_allocator> GraphOps::dist_ts; -template -thread_local unsigned int GraphOps::ts = 0; -template -thread_local unsigned int GraphOps::ts_idx = 0; - } // namespace crab diff --git a/src/crab_utils/heap.hpp b/src/crab_utils/heap.hpp index c9df640b5..dd86dda82 100644 --- a/src/crab_utils/heap.hpp +++ b/src/crab_utils/heap.hpp @@ -27,11 +27,10 @@ namespace crab { // A heap implementation with support for decrease/increase key. // @tparam Comp a predicate that compares two integers. -template Comparator> class Heap { - Comparator lt; - std::vector heap; // heap of ints - std::vector indices; // int -> index in heap + std::function lt; // + std::vector heap; // heap of ints + std::vector indices; // int -> index in heap // Index "traversal" functions static int left(const int i) { return i * 2 + 1; } @@ -49,7 +48,8 @@ class Heap { indices[x] = i; } - void percolateDown(int i) { + void percolateDown() { + int i = 0; const int x = heap[i]; const int size = heap.size(); while (left(i) < size) { @@ -74,7 +74,7 @@ class Heap { } public: - explicit Heap(const Comparator& c) : lt(c) {} + explicit Heap(const std::function& lt) : lt{lt} {} [[nodiscard]] int size() const { @@ -117,7 +117,7 @@ class Heap { indices[x] = -1; heap.pop_back(); if (heap.size() > 1) { - percolateDown(0); + percolateDown(); } return x; } diff --git a/src/main/linux_verifier.cpp b/src/main/linux_verifier.cpp index b1807b287..4ef3ab63e 100644 --- a/src/main/linux_verifier.cpp +++ b/src/main/linux_verifier.cpp @@ -2,10 +2,10 @@ // SPDX-License-Identifier: MIT #if __linux__ +#include #include #include #include -#include #include "config.hpp" #include "linux_verifier.hpp"