PR feedback

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

Author: Alan Jowett

src/asm_parse.hpp

@@ -18,6 +18,10 @@ Instruction parse_instruction(const std::string& line, const std::map<std::strin
  * @param[out] numeric_ranges A vector of numeric ranges that are extracted from the constraints.
  *
  * @return A vector of crab::linear_constraint_t
+ * Example of string constraints include:
+ * r0.type=number
+ * r0.uvalue=5
+ * r0.svalue=5
  */
 std::vector<crab::linear_constraint_t> parse_linear_constraints(const std::set<std::string>& constraints,
                                                           std::vector<crab::interval_t>& numeric_ranges);

src/asm_syntax.hpp

@@ -23,6 +23,19 @@ struct label_t {
     explicit label_t(const int index, const int to = -1, std::string stack_frame_prefix = {}) noexcept
         : from(index), to(to), stack_frame_prefix(std::move(stack_frame_prefix)) {}
 
+    /**
+     * @brief Construct a new label t object from a string.
+     *
+     * @param[in] string_label The string representation of the label.
+     *
+     * @throw std::invalid_argument The label format is invalid.
+     * @throw std::out_of_range The label value causes numeric overflow.
+     *
+     * 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.
+     */
     explicit label_t(std::string_view string_label) {
         auto pos = string_label.find(STACK_FRAME_DELIMITER);
         if (pos != std::string_view::npos) {

src/config.cpp

@@ -14,5 +14,7 @@ const ebpf_verifier_options_t ebpf_verifier_default_options = {
     .allow_division_by_zero = true,
     .setup_constraints = true,
     .big_endian = false,
-    .store_pre_invariants = false, // Enable this to permit usage of the ebpf_check_constraints_at_label and ebpf_get_invariants_at_label functions.
+    .store_pre_invariants = false, // When enabled, stores pre-invariants to support ebpf_check_constraints_at_label and
+                                   // ebpf_get_invariants_at_label. Disabled by default to avoid memory overhead when
+                                   // these functions are not used.
 };

src/crab_verifier.cpp

@@ -282,49 +282,51 @@ void ebpf_verifier_clear_thread_local_state() {
 }
 
 bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label_string,
-                                     const std::set<std::string>& constraints) try {
-    label_t label = label_t(label_string);
-    if (!saved_pre_invariants.has_value()) {
-        os << "No pre-invariants available\n";
-        return false;
-    }
-    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(saved_pre_invariants.value().at(label));
-    auto concrete_domain = ebpf_domain_t::from_constraints(constraints, false);
+                                     const std::set<std::string>& constraints) {
+    try {
+        label_t label = label_t(label_string);
+        if (!saved_pre_invariants.has_value()) {
+            os << "No pre-invariants available\n";
+            return false;
+        }
+        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(saved_pre_invariants.value().at(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 << concrete_domain << "\n";
+            return 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 << concrete_domain << "\n";
-        return false;
-    }
+        if (from_inv.is_bottom()) {
+            os << "The abstract state is unreachable\n";
+            os << from_inv << "\n";
+            return false;
+        }
 
-    if (from_inv.is_bottom()) {
-        os << "The abstract state is unreachable\n";
-        os << from_inv << "\n";
-        return false;
-    }
+        if ((from_inv & concrete_domain).is_bottom()) {
+            os << "Concrete state does not match invariant\n";
 
-    if ((from_inv & concrete_domain).is_bottom()) {
-        os << "Concrete state does not match invariant\n";
+            // Print the concrete state
+            os << "--- Concrete state ---\n";
+            os << concrete_domain << "\n";
 
-        // Print the concrete state
-        os << "--- Concrete state ---\n";
-        os << concrete_domain << "\n";
+            os << "--- Abstract state ---\n";
+            os << from_inv << "\n";
 
-        os << "--- Abstract state ---\n";
-        os << from_inv << "\n";
+            return false;
+        }
 
+        return true;
+    } catch (std::exception& e) {
+        os << "Error occurred while checking constraints: " << e.what() << "\n";
         return false;
     }
-
-    return true;
-} catch (std::exception& e) {
-    os << "Error occurred while checking constraints: " << e.what() << "\n";
-    return false;
 }
 
 std::set<std::string> ebpf_get_invariants_at_label(const std::string& label)

src/crab_verifier.hpp

@@ -43,8 +43,8 @@ void ebpf_verifier_clear_thread_local_state();
  * @param[in,out] os Print output to this stream.
  * @param[in] label The location in the CFG to check against.
  * @param[in] constraints The concrete state to check.
- * @return true The state is valid.
- * @return false The state is invalid.
+ * @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
  */