From 9cbeacb880699f9780ecac2d6f13018ac27e4bc1 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Fri, 18 Oct 2024 12:19:23 -0700 Subject: [PATCH 1/2] Emit warning if maximum number of iterations is reached. Signed-off-by: Alan Jowett --- src/asm_cfg.cpp | 10 +- src/asm_ostream.cpp | 4 + src/asm_syntax.hpp | 11 ++- src/assertions.cpp | 5 +- src/crab/cfg.hpp | 16 ++- src/crab/ebpf_domain.cpp | 11 ++- src/crab/ebpf_domain.hpp | 1 + src/crab/fwd_analyzer.cpp | 24 ++--- src/crab/fwd_analyzer.hpp | 2 +- src/crab/wto.hpp | 18 ++++ src/crab_verifier.cpp | 27 +++--- src/crab_verifier.hpp | 2 +- src/main/check.cpp | 4 +- src/test/test_verify.cpp | 6 +- test-data/loop.yaml | 199 +++++++++++++++++++++++++++++++++++++- 15 files changed, 297 insertions(+), 43 deletions(-) diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index e74606fdd..5e1eb4097 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -10,6 +10,7 @@ #include "asm_syntax.hpp" #include "crab/cfg.hpp" +#include "crab/wto.hpp" using std::optional; using std::set; @@ -359,10 +360,17 @@ std::map collect_stats(const cfg_t& cfg) { } cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bool simplify, - const bool must_have_exit) { + const bool check_for_termination, const bool must_have_exit) { // Convert the instruction sequence to a deterministic control-flow graph. cfg_t det_cfg = instruction_seq_to_cfg(prog, must_have_exit); + if (check_for_termination) { + wto_t wto(det_cfg); + wto.visit_loop_heads([&](const label_t& label) { + det_cfg.get_node(label).insert_front(IncrementLoopCounter{label}); + }); + } + // Annotate the CFG by adding in assertions before every memory instruction. explicate_assertions(det_cfg, info); diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp index 961d3b009..0e5a9722d 100644 --- a/src/asm_ostream.cpp +++ b/src/asm_ostream.cpp @@ -135,6 +135,10 @@ std::ostream& operator<<(std::ostream& os, ValidAccess const& a) { return os; } +std::ostream& operator<<(std::ostream& os, const BoundedLoopCount& a) { + return os << crab::variable_t::loop_counter(to_string(a.name)) << " < " << a.limit; +} + static crab::variable_t typereg(const Reg& r) { return crab::variable_t::reg(crab::data_kind_t::types, r.v); } std::ostream& operator<<(std::ostream& os, ValidSize const& a) { diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp index 7a58185ce..72c6b4e80 100644 --- a/src/asm_syntax.hpp +++ b/src/asm_syntax.hpp @@ -397,8 +397,17 @@ struct ZeroCtxOffset { constexpr bool operator==(const ZeroCtxOffset&) const = default; }; +struct BoundedLoopCount { + label_t name; + bool operator==(const BoundedLoopCount&) const = default; + // Maximum number of loop iterations allowed during verification. + // This prevents infinite loops while allowing reasonable bounded loops. + // When exceeded, verification fails as the loop might not terminate. + static constexpr int limit = 100000; +}; + using AssertionConstraint = std::variant; + ValidMapKeyValue, ValidCall, TypeConstraint, FuncConstraint, ZeroCtxOffset, BoundedLoopCount>; struct Assert { AssertionConstraint cst; diff --git a/src/assertions.cpp b/src/assertions.cpp index 7f7a171f9..854e9250c 100644 --- a/src/assertions.cpp +++ b/src/assertions.cpp @@ -47,9 +47,8 @@ class AssertExtractor { return {}; } - vector operator()(IncrementLoopCounter) const { - assert(false); - return {}; + vector operator()(IncrementLoopCounter& ipc) const { + return {{BoundedLoopCount{ipc.name}}}; } vector operator()(LoadMapFd const&) const { return {}; } diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp index d9527b2d2..5736e830b 100644 --- a/src/crab/cfg.hpp +++ b/src/crab/cfg.hpp @@ -65,6 +65,19 @@ class basic_block_t final { m_ts.push_back(arg); } + template + void insert_front(Args&&... args) { + assert(label() != label_t::entry); + assert(label() != label_t::exit); + m_ts.insert(m_ts.begin(), T{std::forward(args)...}); + } + + void insert_front(const Instruction& arg) { + assert(label() != label_t::entry); + assert(label() != label_t::exit); + m_ts.insert(m_ts.begin(), arg); + } + explicit basic_block_t(label_t _label) : m_label(_label) {} ~basic_block_t() = default; @@ -611,7 +624,8 @@ std::vector stats_headers(); std::map collect_stats(const cfg_t&); -cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, bool simplify, bool must_have_exit = true); +cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, bool simplify, bool check_for_termination, + bool must_have_exit = true); void explicate_assertions(cfg_t& cfg, const program_info& info); std::vector get_assertions(Instruction ins, const program_info& info, const std::optional& label); diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 21d7fd90c..7cbcee9dc 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -1435,6 +1435,14 @@ void ebpf_domain_t::operator()(const TypeConstraint& s) { } } +void ebpf_domain_t::operator()(const BoundedLoopCount& s) { + // Enforces an upper bound on loop iterations by checking that the loop counter + // does not exceed the specified limit + using namespace crab::dsl_syntax; + const auto counter = variable_t::loop_counter(to_string(s.name)); + require(m_inv, counter <= s.limit, "Loop counter is too large"); +} + void ebpf_domain_t::operator()(const FuncConstraint& s) { // Look up the helper function id. const reg_pack_t& reg = reg_pack(s.reg); @@ -2954,6 +2962,7 @@ extended_number ebpf_domain_t::get_loop_count_upper_bound() const { } void ebpf_domain_t::operator()(const IncrementLoopCounter& ins) { - this->add(variable_t::loop_counter(to_string(ins.name)), 1); + const auto counter = variable_t::loop_counter(to_string(ins.name)); + this->add(counter, 1); } } // namespace crab diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp index 486993b14..15ad4842e 100644 --- a/src/crab/ebpf_domain.hpp +++ b/src/crab/ebpf_domain.hpp @@ -78,6 +78,7 @@ class ebpf_domain_t final { void operator()(const ValidStore&); void operator()(const ZeroCtxOffset&); void operator()(const IncrementLoopCounter&); + void operator()(const BoundedLoopCount&); void initialize_loop_counter(const label_t& label); static ebpf_domain_t calculate_constant_limits(); diff --git a/src/crab/fwd_analyzer.cpp b/src/crab/fwd_analyzer.cpp index e0ccc0162..975128ae8 100644 --- a/src/crab/fwd_analyzer.cpp +++ b/src/crab/fwd_analyzer.cpp @@ -50,7 +50,7 @@ class member_component_visitor final { class interleaved_fwd_fixpoint_iterator_t final { using iterator = invariant_table_t::iterator; - cfg_t& _cfg; + const cfg_t& _cfg; wto_t _wto; invariant_table_t _pre, _post; @@ -68,7 +68,7 @@ class interleaved_fwd_fixpoint_iterator_t final { void set_pre(const label_t& label, const ebpf_domain_t& v) { _pre[label] = v; } void transform_to_post(const label_t& label, ebpf_domain_t pre) { - basic_block_t& bb = _cfg.get_node(label); + const basic_block_t& bb = _cfg.get_node(label); pre(bb); _post[label] = std::move(pre); } @@ -101,7 +101,7 @@ class interleaved_fwd_fixpoint_iterator_t final { } public: - explicit interleaved_fwd_fixpoint_iterator_t(cfg_t& cfg) : _cfg(cfg), _wto(cfg) { + explicit interleaved_fwd_fixpoint_iterator_t(const cfg_t& cfg) : _cfg(cfg), _wto(cfg) { for (const auto& label : _cfg.labels()) { _pre.emplace(label, ebpf_domain_t::bottom()); _post.emplace(label, ebpf_domain_t::bottom()); @@ -116,23 +116,17 @@ class interleaved_fwd_fixpoint_iterator_t final { void operator()(const std::shared_ptr& cycle); - friend std::pair run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv); + friend std::pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv); }; -std::pair run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv) { +std::pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv) { // Go over the CFG in weak topological order (accounting for loops). interleaved_fwd_fixpoint_iterator_t analyzer(cfg); if (thread_local_options.check_termination) { - std::vector cycle_heads; - for (auto& component : analyzer._wto) { - if (const auto pc = std::get_if>(&component)) { - cycle_heads.push_back((*pc)->head()); - } - } - for (const label_t& label : cycle_heads) { - entry_inv.initialize_loop_counter(label); - cfg.get_node(label).insert(IncrementLoopCounter{label}); - } + // Initialize loop counters for potential loop headers. + // This enables enforcement of upper bounds on loop iterations + // during program verification. + analyzer._wto.visit_loop_heads([&](const label_t& label) { entry_inv.initialize_loop_counter(label); }); } analyzer.set_pre(cfg.entry_label(), entry_inv); for (auto& component : analyzer._wto) { diff --git a/src/crab/fwd_analyzer.hpp b/src/crab/fwd_analyzer.hpp index 06ebc268a..3445e92fe 100644 --- a/src/crab/fwd_analyzer.hpp +++ b/src/crab/fwd_analyzer.hpp @@ -11,6 +11,6 @@ namespace crab { using invariant_table_t = std::map; -std::pair run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv); +std::pair run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv); } // namespace crab diff --git a/src/crab/wto.hpp b/src/crab/wto.hpp index a0ca2e4fa..4d489b17b 100644 --- a/src/crab/wto.hpp +++ b/src/crab/wto.hpp @@ -125,4 +125,22 @@ class wto_t final { friend std::ostream& operator<<(std::ostream& o, const wto_t& wto); const wto_nesting_t& nesting(const label_t& label); + + /** + * Visit the heads of all loops in the WTO. + * + * @tparam F A callable type with signature void(const label_t&). + * @param f The callable to be invoked for each loop head. + * + * The order in which the heads are visited is not specified. + */ + template + void visit_loop_heads(F&& f) const { + for (const auto& component : *this) { + if (const auto pc = std::get_if>(&component)) { + f((*pc)->head()); + } + } + } + }; diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index f1ceccd18..9f1c43f7e 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -56,11 +56,11 @@ struct checks_db final { checks_db() = default; }; -static checks_db generate_report(cfg_t& cfg, const crab::invariant_table_t& pre_invariants, +static checks_db generate_report(const cfg_t& cfg, const crab::invariant_table_t& pre_invariants, const crab::invariant_table_t& post_invariants) { checks_db m_db; for (const label_t& label : cfg.sorted_labels()) { - basic_block_t& bb = cfg.get_node(label); + const basic_block_t& bb = cfg.get_node(label); ebpf_domain_t from_inv(pre_invariants.at(label)); from_inv.set_require_check( [&m_db, label](auto& inv, const crab::linear_constraint_t& cst, const std::string& s) { @@ -95,8 +95,13 @@ static checks_db generate_report(cfg_t& cfg, const crab::invariant_table_t& pre_ } if (thread_local_options.check_termination) { - const auto last_inv = post_invariants.at(cfg.exit_label()); - m_db.max_loop_count = last_inv.get_loop_count_upper_bound(); + // Gather the upper bound of loop counts from post-invariants. + for (const auto [label, inv] : post_invariants) { + if (inv.is_bottom()) { + continue; + } + m_db.max_loop_count = std::max(m_db.max_loop_count, inv.get_loop_count_upper_bound()); + } } return m_db; } @@ -127,13 +132,9 @@ static void print_report(std::ostream& os, const checks_db& db, const Instructio } } os << "\n"; - const crab::number_t max_loop_count{100000}; - if (db.max_loop_count > max_loop_count) { - os << "Could not prove termination.\n"; - } } -static checks_db get_analysis_report(std::ostream& s, cfg_t& cfg, const crab::invariant_table_t& pre_invariants, +static checks_db get_analysis_report(std::ostream& s, const cfg_t& cfg, const crab::invariant_table_t& pre_invariants, const crab::invariant_table_t& post_invariants, const std::optional& prog = std::nullopt) { // Analyze the control-flow graph. @@ -161,7 +162,7 @@ static checks_db get_analysis_report(std::ostream& s, cfg_t& cfg, const crab::in return db; } -static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info, const ebpf_verifier_options_t* options, +static checks_db get_ebpf_report(std::ostream& s, const cfg_t& cfg, program_info info, const ebpf_verifier_options_t* options, const std::optional& prog = std::nullopt) { global_program_info = std::move(info); crab::domains::clear_global_state(); @@ -182,7 +183,7 @@ static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info, } /// Returned value is true if the program passes verification. -bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options, +bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options, ebpf_verifier_stats_t* stats) { if (options == nullptr) { options = &ebpf_verifier_default_options; @@ -219,7 +220,7 @@ std::tuple ebpf_analyze_program_for_test(std::ostream& o throw std::runtime_error("Entry invariant is inconsistent"); } try { - cfg_t cfg = prepare_cfg(prog, info, options.simplify, false); + const cfg_t cfg = prepare_cfg(prog, info, options.simplify, options.check_termination, false); auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_inv)); const checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants); print_report(os, report, prog, false); @@ -242,7 +243,7 @@ bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const pro // Convert the instruction sequence to a control-flow graph // in a "passive", non-deterministic form. - cfg_t cfg = prepare_cfg(prog, info, options->simplify); + const cfg_t cfg = prepare_cfg(prog, info, options->simplify, options->check_termination); std::optional prog_opt = std::nullopt; if (options->print_failures) { diff --git a/src/crab_verifier.hpp b/src/crab_verifier.hpp index 14eeb89a7..6694123c8 100644 --- a/src/crab_verifier.hpp +++ b/src/crab_verifier.hpp @@ -7,7 +7,7 @@ #include "spec_type_descriptors.hpp" #include "string_constraints.hpp" -bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options, +bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options, ebpf_verifier_stats_t* stats); bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const program_info& info, diff --git a/src/main/check.cpp b/src/main/check.cpp index a7cd49955..d8ace0ce5 100644 --- a/src/main/check.cpp +++ b/src/main/check.cpp @@ -250,7 +250,7 @@ int main(int argc, char** argv) { return !res; } else if (domain == "stats") { // Convert the instruction sequence to a control-flow graph. - cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.simplify); + const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.simplify, ebpf_verifier_options.check_termination); // Just print eBPF program stats. auto stats = collect_stats(cfg); @@ -264,7 +264,7 @@ int main(int argc, char** argv) { std::cout << "\n"; } else if (domain == "cfg") { // Convert the instruction sequence to a control-flow graph. - cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.simplify); + const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.simplify, ebpf_verifier_options.check_termination); std::cout << cfg; std::cout << "\n"; } else { diff --git a/src/test/test_verify.cpp b/src/test/test_verify.cpp index a8405e382..3cbe4fad5 100644 --- a/src/test/test_verify.cpp +++ b/src/test/test_verify.cpp @@ -586,7 +586,7 @@ TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/16") // False positive, unknown cause TEST_SECTION_FAIL("linux", "test_map_in_map_kern.o", "kprobe/sys_connect") -void test_analyze_thread(cfg_t* cfg, program_info* info, bool* res) { +void test_analyze_thread(const cfg_t* cfg, program_info* info, bool* res) { *res = run_ebpf_analysis(std::cout, *cfg, *info, nullptr, nullptr); } @@ -598,7 +598,7 @@ TEST_CASE("multithreading", "[verify][multithreading]") { auto prog_or_error1 = unmarshal(raw_prog1); auto prog1 = std::get_if(&prog_or_error1); REQUIRE(prog1 != nullptr); - cfg_t cfg1 = prepare_cfg(*prog1, raw_prog1.info, true); + const cfg_t cfg1 = prepare_cfg(*prog1, raw_prog1.info, true, true); auto raw_progs2 = read_elf("ebpf-samples/bpf_cilium_test/bpf_netdev.o", "2/2", nullptr, &g_ebpf_platform_linux); REQUIRE(raw_progs2.size() == 1); @@ -606,7 +606,7 @@ TEST_CASE("multithreading", "[verify][multithreading]") { auto prog_or_error2 = unmarshal(raw_prog2); auto prog2 = std::get_if(&prog_or_error2); REQUIRE(prog2 != nullptr); - cfg_t cfg2 = prepare_cfg(*prog2, raw_prog2.info, true); + const cfg_t cfg2 = prepare_cfg(*prog2, raw_prog2.info, true, true); bool res1, res2; std::thread a(test_analyze_thread, &cfg1, &raw_prog1.info, &res1); diff --git a/test-data/loop.yaml b/test-data/loop.yaml index 10e5fd116..a0f3d939a 100644 --- a/test-data/loop.yaml +++ b/test-data/loop.yaml @@ -186,7 +186,7 @@ post: - "pc[1]=[1, +oo]" messages: - - "Could not prove termination." + - "1: Loop counter is too large (pc[1] < 100000)" --- test-case: realistic forward loop @@ -266,3 +266,200 @@ post: - r4.uvalue-r2.svalue<=0 - r4.uvalue-r2.uvalue<=0 - r4.uvalue=[1, 255] + +--- +test-case: simple infinite loop, less than +options: ["termination"] + +pre: [] + +code: + : | + r0 = 0 + if r0 < 1 goto + exit + +post: [] + +messages: + - "1:2: Code is unreachable after 1:2" + - "0: Loop counter is too large (pc[0] < 100000)" +--- +test-case: simple infinite loop, less than or equal +options: ["termination"] + +pre: [] + +code: + : | + r0 = 0 + if r0 <= 1 goto + exit + +post: [] + +messages: + - "1:2: Code is unreachable after 1:2" + - "0: Loop counter is too large (pc[0] < 100000)" + +--- +test-case: simple infinite loop, equal +options: ["termination"] + +pre: [] + +code: + : | + r0 = 0 + if r0 == 0 goto + exit + +post: [] + +messages: + - "1:2: Code is unreachable after 1:2" + - "0: Loop counter is too large (pc[0] < 100000)" + +--- +test-case: simple infinite loop, greater than +options: ["termination"] + +pre: [] + +code: + : | + r0 = 1 + if r0 > 0 goto + exit + +post: [] + +messages: + - "1:2: Code is unreachable after 1:2" + - "0: Loop counter is too large (pc[0] < 100000)" + +--- +test-case: simple infinite loop, greater than or equal +options: ["termination"] + +pre: [] + +code: + : | + r0 = 1 + if r0 >= 0 goto + exit + +post: [] + +messages: + - "1:2: Code is unreachable after 1:2" + - "0: Loop counter is too large (pc[0] < 100000)" +--- +test-case: infinite loop with multiple exits +options: ["termination"] +pre: [] +code: + : | + r0 = 1 + if r0 > 0 goto + exit + : | + if r0 < 2 goto + exit +post: [] +messages: + - "1:2: Code is unreachable after 1:2" + - "3:4: Code is unreachable after 3:4" + - "0: Loop counter is too large (pc[0] < 100000)" + +--- +# Note: This test case terminates after 1000001 iterations, but the verifier assumes that the loop is infinite +# because it is greater than the default limit of 1000000 iterations. +test-case: very large loop > 1M iterations +options: ["termination"] +pre: [r0.type=number, r0.svalue=0, r0.uvalue=0] +code: + : | + r0 += 1 + if r0 < 1000001 goto + : | + exit +post: + - "pc[0]=1000001" + - "pc[0]=r0.svalue" + - "pc[0]=r0.uvalue" + - "r0.svalue=1000001" + - "r0.svalue=r0.uvalue" + - "r0.type=number" + - "r0.uvalue=1000001" +messages: + - "0: Loop counter is too large (pc[0] < 100000)" + +--- +test-case: possible infinite loop +options: ["termination"] + +pre: [r0.type=number] +code: + : | + if r0 > 0 goto + exit + +post: + - "pc[0]=[1, +oo]" + - "r0.svalue=0" + - "r0.uvalue=0" + - "r0.type=number" + +messages: + - "0: Loop counter is too large (pc[0] < 100000)" + +--- +# Check for case where there are backwards jumps that don't form a loop. +test-case: non-loop backwards jump +options: ["termination"] + +pre: [r0.type=number] +code: + : | + r0 = 1 + goto + : | + r0 += 1 + exit + : | + r0 += 1 + goto + +post: + - "r0.svalue=3" + - "r0.uvalue=3" + - "r0.type=number" + +messages: [] + +--- +# Nested loops with inner infinite loop +test-case: nested loops with inner infinite loop +options: ["termination"] + +pre: + - "r0.type=number" + - "r0.svalue=0" + - "r0.uvalue=0" +code: + : | + r0 += 1 + if r0 > 10 goto + : | + if r0 > 0 goto + : | + exit + +post: [] + +messages: + - "1:3: Code is unreachable after 1:3" + - "2: Loop counter is too large (pc[2] < 100000)" + - "2:3: Code is unreachable after 2:3" From f44316a8ccae93a883557a0509ac155eb0fca6c3 Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 6 Nov 2024 12:35:14 -0800 Subject: [PATCH 2/2] PR feedback Signed-off-by: Alan Jowett --- src/asm_cfg.cpp | 6 +++++- src/crab/cfg.hpp | 9 ++------- src/crab/fwd_analyzer.cpp | 3 ++- src/crab/wto.hpp | 3 +-- 4 files changed, 10 insertions(+), 11 deletions(-) diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index 5e1eb4097..46b3bef40 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -359,14 +359,18 @@ std::map collect_stats(const cfg_t& cfg) { return res; } +// ISSUE: 774 - Rationalize the list of bools being passed to prepare_cfg. cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bool simplify, const bool check_for_termination, const bool must_have_exit) { // Convert the instruction sequence to a deterministic control-flow graph. cfg_t det_cfg = instruction_seq_to_cfg(prog, must_have_exit); + // Detect loops using Weak Topological Ordering (WTO) and insert counters at loop entry points. WTO provides a + // hierarchical decomposition of the CFG that identifies all strongly connected components (cycles) and their entry + // points. These entry points serve as natural locations for loop counters that help verify program termination. if (check_for_termination) { wto_t wto(det_cfg); - wto.visit_loop_heads([&](const label_t& label) { + wto.for_each_loop_head([&](const label_t& label) { det_cfg.get_node(label).insert_front(IncrementLoopCounter{label}); }); } diff --git a/src/crab/cfg.hpp b/src/crab/cfg.hpp index 5736e830b..a3c177cec 100644 --- a/src/crab/cfg.hpp +++ b/src/crab/cfg.hpp @@ -65,13 +65,8 @@ class basic_block_t final { m_ts.push_back(arg); } - template - void insert_front(Args&&... args) { - assert(label() != label_t::entry); - assert(label() != label_t::exit); - m_ts.insert(m_ts.begin(), T{std::forward(args)...}); - } - + /// Insert an instruction at the front of the basic block. + /// @note Cannot modify entry or exit blocks. void insert_front(const Instruction& arg) { assert(label() != label_t::entry); assert(label() != label_t::exit); diff --git a/src/crab/fwd_analyzer.cpp b/src/crab/fwd_analyzer.cpp index 975128ae8..04c464524 100644 --- a/src/crab/fwd_analyzer.cpp +++ b/src/crab/fwd_analyzer.cpp @@ -126,7 +126,8 @@ std::pair run_forward_analyzer(const cfg_t // Initialize loop counters for potential loop headers. // This enables enforcement of upper bounds on loop iterations // during program verification. - analyzer._wto.visit_loop_heads([&](const label_t& label) { entry_inv.initialize_loop_counter(label); }); + // TODO: Consider making this an instruction instead of an explicit call. + analyzer._wto.for_each_loop_head([&](const label_t& label) { entry_inv.initialize_loop_counter(label); }); } analyzer.set_pre(cfg.entry_label(), entry_inv); for (auto& component : analyzer._wto) { diff --git a/src/crab/wto.hpp b/src/crab/wto.hpp index 4d489b17b..4521b2c5d 100644 --- a/src/crab/wto.hpp +++ b/src/crab/wto.hpp @@ -129,13 +129,12 @@ class wto_t final { /** * Visit the heads of all loops in the WTO. * - * @tparam F A callable type with signature void(const label_t&). * @param f The callable to be invoked for each loop head. * * The order in which the heads are visited is not specified. */ template - void visit_loop_heads(F&& f) const { + void for_each_loop_head(F&& f) const { for (const auto& component : *this) { if (const auto pc = std::get_if>(&component)) { f((*pc)->head());