From fb3e0ea98f9392267089e9d2a6987af386d2a83a Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Tue, 15 Oct 2024 22:09:40 -0700 Subject: [PATCH] PR feedback Signed-off-by: Alan Jowett --- src/config.cpp | 2 +- src/crab_verifier.cpp | 32 ++++++++++++++++++-------------- src/crab_verifier.hpp | 2 ++ src/ebpf_yaml.cpp | 6 ++++-- test-data/add.yaml | 18 +++++++++--------- 5 files changed, 34 insertions(+), 26 deletions(-) diff --git a/src/config.cpp b/src/config.cpp index ea5e05117..f1f73b0ef 100644 --- a/src/config.cpp +++ b/src/config.cpp @@ -14,5 +14,5 @@ const ebpf_verifier_options_t ebpf_verifier_default_options = { .allow_division_by_zero = true, .setup_constraints = true, .big_endian = false, - .store_pre_invariants = false, + .store_pre_invariants = false, // Enable this to permit usage of the ebpf_check_constraints_at_label and ebpf_get_invariants_at_label functions. }; diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index 2f4625ec0..9e49c0b2b 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -162,7 +162,13 @@ static checks_db get_analysis_report(std::ostream& s, cfg_t& cfg, const crab::in return db; } -static thread_local std::optional save_pre_invariants = std::nullopt; +static thread_local std::optional saved_pre_invariants = std::nullopt; + +static void save_invariants_if_needed(const crab::invariant_table_t& pre_invariants) { + if (thread_local_options.store_pre_invariants) { + saved_pre_invariants = pre_invariants; + } +} static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info, const ebpf_verifier_options_t* options, const std::optional& prog = std::nullopt) { @@ -175,9 +181,7 @@ static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info, // Get dictionaries of pre-invariants and post-invariants for each basic block. ebpf_domain_t entry_dom = ebpf_domain_t::setup_entry(true); auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_dom)); - if (thread_local_options.store_pre_invariants) { - save_pre_invariants = pre_invariants; - } + save_invariants_if_needed(pre_invariants); return get_analysis_report(s, cfg, pre_invariants, post_invariants, prog); } catch (std::runtime_error& e) { // Convert verifier runtime_error exceptions to failure. @@ -227,9 +231,7 @@ std::tuple ebpf_analyze_program_for_test(std::ostream& o try { cfg_t cfg = prepare_cfg(prog, info, options.simplify, false); auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_inv)); - if (thread_local_options.store_pre_invariants) { - save_pre_invariants = pre_invariants; - } + save_invariants_if_needed(pre_invariants); const checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants); print_report(os, report, prog, false); @@ -276,21 +278,21 @@ void ebpf_verifier_clear_thread_local_state() { global_program_info.clear(); crab::domains::clear_thread_local_state(); crab::domains::SplitDBM::clear_thread_local_state(); - save_pre_invariants = std::nullopt; + saved_pre_invariants = std::nullopt; } bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label_string, const std::set& constraints) try { label_t label = label_t(label_string); - if (!save_pre_invariants.has_value()) { + if (!saved_pre_invariants.has_value()) { os << "No pre-invariants available\n"; return false; } - if (save_pre_invariants.value().find(label) == save_pre_invariants.value().end()) { + if (saved_pre_invariants.value().find(label) == saved_pre_invariants.value().end()) { os << "No pre-invariants available for label " << label << "\n"; return false; } - ebpf_domain_t from_inv(save_pre_invariants.value().at(label)); + ebpf_domain_t from_inv(saved_pre_invariants.value().at(label)); auto concrete_domain = ebpf_domain_t::from_constraints(constraints, false); if (concrete_domain.is_bottom()) { @@ -327,12 +329,14 @@ bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label_ std::set ebpf_get_invariants_at_label(const std::string& label) { + // If the label is malformed, throw an exception so the caller can handle it. label_t l = label_t(label); - if (!save_pre_invariants.has_value()) { + + if (!saved_pre_invariants.has_value()) { return {}; } - if (save_pre_invariants.value().find(l) == save_pre_invariants.value().end()) { + if (saved_pre_invariants.value().find(l) == saved_pre_invariants.value().end()) { return {}; } - return save_pre_invariants.value().at(l).to_set().value(); + return saved_pre_invariants.value().at(l).to_set().value(); } diff --git a/src/crab_verifier.hpp b/src/crab_verifier.hpp index bfb48a6b7..0e9bf109d 100644 --- a/src/crab_verifier.hpp +++ b/src/crab_verifier.hpp @@ -32,6 +32,8 @@ void ebpf_verifier_clear_thread_local_state(); * verifier constraints at the label. Requires the `store_pre_invariants` option to be set. * * Abstract constraints are computed by the verifier and stored if the `store_pre_invariants` option is set. + * These constraints represent the program state at a specific point in the control flow graph, + * as determined by the static analysis performed by the verifier. * * @param[in,out] os Print output to this stream. * @param[in] label The location in the CFG to check against. diff --git a/src/ebpf_yaml.cpp b/src/ebpf_yaml.cpp index 1cedf1583..4dbb3acd3 100644 --- a/src/ebpf_yaml.cpp +++ b/src/ebpf_yaml.cpp @@ -128,7 +128,7 @@ static std::set as_set_empty_default(const YAML::Node& optional_node) { } static std::map> parse_invariants_to_check(const YAML::Node& case_node) { - if (!case_node["invariants-to-check"].IsDefined()) { + if (!case_node["invariants-to-check"].IsDefined() || case_node["invariants-to-check"].IsNull()) { return {}; } @@ -278,12 +278,14 @@ std::optional run_yaml_test_case(TestCase test_case, bool debug) { std::set actual_messages = extract_messages(ss.str()); for (auto& [label, expected_invariant] : test_case.invariants_to_check) { + ss.str(""); + ss.clear(); if (!ebpf_check_constraints_at_label(ss, label, expected_invariant)) { // If debug is enabled, print the output of ebpf_check_constraints_at_label. if (debug) { std::cout << ss.str(); } - actual_messages.insert(label + ": Concrete invariants at do not match abstract invariants"); + actual_messages.insert(label + ": Concrete invariants do not match abstract invariants"); } } diff --git a/test-data/add.yaml b/test-data/add.yaml index 8e190fb72..790f271ef 100644 --- a/test-data/add.yaml +++ b/test-data/add.yaml @@ -189,19 +189,19 @@ code: r0 = r1 invariants-to-check: - 1: + 1: # After the first assignment, r1 should be 1. - r1.type=number - r1.svalue=1 - r1.uvalue=1 - 2: + 2: # After the second assignment, r2 should be 2. - r2.type=number - r2.svalue=2 - r2.uvalue=2 - 3: + 3: # After the addition, r1 should be 3. - r1.type=number - r1.svalue=3 - r1.uvalue=3 - -2: + -2: # After the last assignment, r0 should be 3. - r0.type=number - r0.svalue=3 - r0.uvalue=3 @@ -229,19 +229,19 @@ code: r0 = r1 invariants-to-check: - 1: + 1: # After the first assignment, r1 should be 1. - r1.type=number - r1.svalue=1 - r1.uvalue=1 - 2: + 2: # After the second assignment, r2 should be 2. - r2.type=number - r2.svalue=2 - r2.uvalue=2 - 3: + 3: # After the addition, r1 should be 3. Invalid invariant to test negative case. - r1.type=number - r1.svalue=2 - r1.uvalue=2 - -2: + -2: # After the last assignment, r0 should be 3. - r0.type=number - r0.svalue=3 - r0.uvalue=3 @@ -258,4 +258,4 @@ post: - r2.uvalue=2 messages: - - "3: Concrete invariants at do not match abstract invariants" + - "3: Concrete invariants do not match abstract invariants"