PR feedback

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>

Author: Alan Jowett

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);

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";

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<std::string>& constraints);