Return verifier stats to the calling application

For example so the caller can impose its own limit on max instructions to complete within. Signed-off-by: Dave Thaler <[email protected]>
dthaler · May 30, 2021 · d1411fa · d1411fa
1 parent 6efcb2a
commit d1411fa
Show file tree

Hide file tree

Showing 5 changed files with 35 additions and 11 deletions.
diff --git a/src/config.hpp b/src/config.hpp
@@ -15,4 +15,10 @@ struct ebpf_verifier_options_t {
     bool strict;
 };
 
+struct ebpf_verifier_stats_t {
+    int total_unreachable;
+    int total_warnings;
+    int max_instruction_count;
+};
+
 extern const ebpf_verifier_options_t ebpf_verifier_default_options;
diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp
@@ -395,10 +395,9 @@ class ebpf_domain_t final {
         }
     }
 
-    bool terminates() {
-        using namespace crab::dsl_syntax;
-        constexpr int max_instructions = 100000;
-        return m_inv.entail(variable_t::instruction_count() <= max_instructions);
+    int get_instruction_count_upper_bound() {
+        const auto& ub = m_inv[variable_t::instruction_count()].ub();
+        return (ub.is_finite() && ub.number().value().fits_sint()) ? (int)ub.number().value() : INT_MAX;
     }
 
     void operator()(Assume const& s) {

diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
@@ -33,6 +33,7 @@ struct checks_db final {
     std::map<label_t, std::vector<std::string>> m_db;
     int total_warnings{};
     int total_unreachable{};
+    int max_instruction_count{};
     std::set<label_t> maybe_nonterminating;
 
     void add(const label_t& label, const std::string& msg) {
@@ -91,12 +92,20 @@ static checks_db generate_report(std::ostream& s,
         });
 
         if (thread_local_options.check_termination) {
-            bool pre_join_terminates = false;
-            for (const label_t& prev_label : bb.prev_blocks_set())
-                pre_join_terminates |= preconditions.at(prev_label).terminates();
+            // Pinpoint the places where divergence might occur.
+            int min_instruction_count_upper_bound = INT_MAX;
+            for (const label_t& prev_label : bb.prev_blocks_set()) {
+                int instruction_count = preconditions.at(prev_label).get_instruction_count_upper_bound();
+                min_instruction_count_upper_bound = std::min(min_instruction_count_upper_bound, instruction_count);
+            }
 
-            if (pre_join_terminates && !from_inv.terminates())
+            constexpr int max_instructions = 100000;
+            int instruction_count_upper_bound = from_inv.get_instruction_count_upper_bound();
+            if ((min_instruction_count_upper_bound < max_instructions) &&
+                (instruction_count_upper_bound >= max_instructions))
                 m_db.add_nontermination(label);
+
+            m_db.max_instruction_count = std::max(m_db.max_instruction_count, instruction_count_upper_bound);
         }
 
         bool pre_bot = from_inv.is_bottom();
@@ -168,7 +177,7 @@ bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, program_info info, const ebp
 
 /// Returned value is true if the program passes verification.
 bool ebpf_verify_program(std::ostream& s, const InstructionSeq& prog, program_info info,
-                         const ebpf_verifier_options_t* options) {
+                         const ebpf_verifier_options_t* options, ebpf_verifier_stats_t* stats) {
     if (options == nullptr)
         options = &ebpf_verifier_default_options;
 
@@ -180,5 +189,10 @@ bool ebpf_verify_program(std::ostream& s, const InstructionSeq& prog, program_in
     if (options->print_failures) {
         print_report(s, report, prog);
     }
+    if (stats) {
+        stats->total_unreachable = report.total_unreachable;
+        stats->total_warnings = report.total_warnings;
+        stats->max_instruction_count = report.max_instruction_count;
+    }
     return (report.total_warnings == 0);
 }
diff --git a/src/crab_verifier.hpp b/src/crab_verifier.hpp
@@ -8,7 +8,8 @@
 
 bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, program_info info, const ebpf_verifier_options_t* options);
 
-bool ebpf_verify_program(std::ostream& s, const InstructionSeq& prog, program_info info, const ebpf_verifier_options_t* options);
+bool ebpf_verify_program(std::ostream& s, const InstructionSeq& prog, program_info info, const ebpf_verifier_options_t* options,
+    ebpf_verifier_stats_t* stats);
 
 int create_map_crab(const EbpfMapType& map_type, uint32_t key_size, uint32_t value_size, uint32_t max_entries, ebpf_verifier_options_t options);
 

diff --git a/src/main/check.cpp b/src/main/check.cpp
@@ -139,9 +139,13 @@ int main(int argc, char** argv) {
     }
 
     if (domain == "zoneCrab") {
+        ebpf_verifier_stats_t verifier_stats;
         const auto [res, seconds] = timed_execution([&] {
-            return ebpf_verify_program(std::cout, prog, raw_prog.info, &ebpf_verifier_options);
+            return ebpf_verify_program(std::cout, prog, raw_prog.info, &ebpf_verifier_options, &verifier_stats);
         });
+        if (ebpf_verifier_options.check_termination && (ebpf_verifier_options.print_failures || ebpf_verifier_options.print_invariants)) {
+            std::cout << "Program terminates within " << verifier_stats.max_instruction_count << " instructions\n";
+        }
         std::cout << res << "," << seconds << "," << resident_set_size_kb() << "\n";
         return !res;
     } else if (domain == "linux") {