From 24bbdeae979ee54515f672df4b3f0913eddb56fc Mon Sep 17 00:00:00 2001 From: Alan Jowett Date: Wed, 30 Oct 2024 14:34:52 -0700 Subject: [PATCH] PR feedback Signed-off-by: Alan Jowett --- src/asm_syntax.hpp | 9 ++++++++- src/crab_verifier.cpp | 4 +--- src/crab_verifier.hpp | 5 +++-- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp index 2d704fd3d..c8ca67001 100644 --- a/src/asm_syntax.hpp +++ b/src/asm_syntax.hpp @@ -27,14 +27,21 @@ struct label_t { * @brief Construct a new label t object from a string. * * @param[in] string_label The string representation of the label. + * @return None (constructor) * * @throw std::invalid_argument The label format is invalid. * @throw std::out_of_range The label value causes numeric overflow. * + * Format: [prefix/]from[:to] + * - prefix: Optional stack frame prefix + * - from: Source instruction number + * - to: Optional jump target (-1 means next instruction) + * * Example labels: * "2:-1" - a label which falls through to the next instruction. * "2:5" - a label which jumps to instruction 5. - * "2:-1/5:-1" - a label which falls through to the next instruction, with a stack frame prefix denoting where the label was called. + * "2:-1/5:-1" - a label which falls through to the next instruction, with a stack frame prefix denoting where the + * label was called. */ explicit label_t(std::string_view string_label) { auto pos = string_label.find(STACK_FRAME_DELIMITER); diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index 6e4c8efcc..f9433990c 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -297,12 +297,10 @@ bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label_ auto concrete_domain = ebpf_domain_t::from_constraints(constraints, false); if (concrete_domain.is_bottom()) { - os << "The provided constraints are unsatisfiable (concrete domain is bottom)\n"; - os << "Concrete constraints are self-contradictory\n"; + os << "The provided constraints are unsatisfiable and self-contradictory (concrete domain is bottom)\n"; os << concrete_domain << "\n"; return false; } - if (from_inv.is_bottom()) { os << "The abstract state is unreachable\n"; os << from_inv << "\n"; diff --git a/src/crab_verifier.hpp b/src/crab_verifier.hpp index faaf5d457..bd0055c8c 100644 --- a/src/crab_verifier.hpp +++ b/src/crab_verifier.hpp @@ -45,8 +45,9 @@ void ebpf_verifier_clear_thread_local_state(); * @param[in] constraints The concrete state to check. * @retval true The state is valid. * @retval false The state is invalid. - * @throw std::invalid_argument The label format is invalid - * @throw std::out_of_range The label value causes numeric overflow + * + * Note: + * This can also return false if the label is not found in the CFG or if the label is malformed. */ bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label, const std::set& constraints);