Fix misleading instruction_count message

Since PR #479, PREVAIL now computes a loop iteration count,
not an instruction_count, so update messages and symbols names
accordingly.

Fixes #542

Signed-off-by: Dave Thaler <[email protected]>

src/asm_ostream.cpp

@@ -338,7 +338,7 @@ struct InstructionPrinterVisitor {
     }
 
     void operator()(IncrementLoopCounter const& a) {
-        os_ << crab::variable_t::instruction_count(to_string(a.name)) << "++";
+        os_ << crab::variable_t::loop_counter(to_string(a.name)) << "++";
     }
 };
 

src/config.hpp

@@ -25,7 +25,7 @@ struct ebpf_verifier_options_t {
 struct ebpf_verifier_stats_t {
     int total_unreachable;
     int total_warnings;
-    int max_instruction_count;
+    int max_loop_count;
 };
 
 extern const ebpf_verifier_options_t ebpf_verifier_default_options;

src/crab/ebpf_domain.cpp

@@ -925,7 +925,7 @@ ebpf_domain_t ebpf_domain_t::calculate_constant_limits() {
         inv += r.packet_offset <= variable_t::packet_size();
         inv += r.packet_offset >= 0;
         if (thread_local_options.check_termination) {
-            for (variable_t counter : variable_t::get_instruction_counters()) {
+            for (variable_t counter : variable_t::get_loop_counters()) {
                 inv += counter <= std::numeric_limits<int32_t>::max();
                 inv += counter >= 0;
                 inv += counter <= r.svalue;
@@ -2828,18 +2828,18 @@ ebpf_domain_t ebpf_domain_t::setup_entry(bool init_r1) {
     return inv;
 }
 
-void ebpf_domain_t::initialize_instruction_count(const label_t label) {
-    m_inv.assign(variable_t::instruction_count(to_string(label)), 0);
+void ebpf_domain_t::initialize_loop_counter(const label_t label) {
+    m_inv.assign(variable_t::loop_counter(to_string(label)), 0);
 }
 
-bound_t ebpf_domain_t::get_instruction_count_upper_bound() {
+bound_t ebpf_domain_t::get_loop_count_upper_bound() {
     crab::bound_t ub{number_t{0}};
-    for (variable_t counter : variable_t::get_instruction_counters())
-        ub += std::max(ub, m_inv[counter].ub());
+    for (variable_t counter : variable_t::get_loop_counters())
+        ub = std::max(ub, m_inv[counter].ub());
     return ub;
 }
 
 void ebpf_domain_t::operator()(const IncrementLoopCounter& ins) {
-    this->add(variable_t::instruction_count(to_string(ins.name)), 1);
+    this->add(variable_t::loop_counter(to_string(ins.name)), 1);
 }
 } // namespace crab

src/crab/ebpf_domain.hpp

@@ -47,7 +47,7 @@ class ebpf_domain_t final {
 
     typedef bool check_require_func_t(NumAbsDomain&, const linear_constraint_t&, std::string);
     void set_require_check(std::function<check_require_func_t> f);
-    bound_t get_instruction_count_upper_bound();
+    bound_t get_loop_count_upper_bound();
     static ebpf_domain_t setup_entry(bool init_r1);
 
     static ebpf_domain_t from_constraints(const std::set<std::string>& constraints, bool setup_constraints);
@@ -79,7 +79,7 @@ class ebpf_domain_t final {
     void operator()(const ZeroCtxOffset&);
     void operator()(const IncrementLoopCounter&);
 
-    void initialize_instruction_count(label_t label);
+    void initialize_loop_counter(label_t label);
     static ebpf_domain_t calculate_constant_limits();
   private:
     // private generic domain functions

src/crab/fwd_analyzer.cpp

@@ -124,7 +124,7 @@ std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg,
             }
         }
         for (const label_t& label : cycle_heads) {
-            entry_inv.initialize_instruction_count(label);
+            entry_inv.initialize_loop_counter(label);
             cfg.get_node(label).insert(IncrementLoopCounter{label});
         }
     }

src/crab/var_factory.cpp

@@ -88,7 +88,7 @@ variable_t variable_t::kind_var(data_kind_t kind, variable_t type_variable) {
 
 variable_t variable_t::meta_offset() { return make("meta_offset"); }
 variable_t variable_t::packet_size() { return make("packet_size"); }
-variable_t variable_t::instruction_count(const std::string& label) { return make("pc[" + label + "]"); }
+variable_t variable_t::loop_counter(const std::string& label) { return make("pc[" + label + "]"); }
 
 static bool ends_with(const std::string& str, const std::string& suffix)
 {
@@ -108,7 +108,7 @@ bool variable_t::is_in_stack() const {
     return this->name()[0] == 's';
 }
 
-std::vector<variable_t> variable_t::get_instruction_counters() {
+std::vector<variable_t> variable_t::get_loop_counters() {
     std::vector<variable_t> res;
     for (const std::string& name: *names) {
         if (name.find("pc") == 0)

src/crab/variable.hpp

@@ -75,8 +75,8 @@ class variable_t final {
     static variable_t kind_var(data_kind_t kind, variable_t type_variable);
     static variable_t meta_offset();
     static variable_t packet_size();
-    static std::vector<variable_t> get_instruction_counters();
-    static variable_t instruction_count(const std::string& label);
+    static std::vector<variable_t> get_loop_counters();
+    static variable_t loop_counter(const std::string& label);
     [[nodiscard]] bool is_in_stack() const;
 
     struct Hasher {

src/crab_verifier.cpp

@@ -31,7 +31,7 @@ struct checks_db final {
     std::map<label_t, std::vector<std::string>> m_db{};
     int total_warnings{};
     int total_unreachable{};
-    crab::bound_t max_instruction_count{crab::number_t{0}};
+    crab::bound_t max_loop_count{crab::number_t{0}};
 
     void add(const label_t& label, const std::string& msg) { m_db[label].emplace_back(msg); }
 
@@ -45,8 +45,8 @@ struct checks_db final {
         total_unreachable++;
     }
 
-    [[nodiscard]] int get_max_instruction_count() const {
-        auto m = this->max_instruction_count.number();
+    [[nodiscard]] int get_max_loop_count() const {
+        auto m = this->max_loop_count.number();
         if (m && m->fits_sint32())
             return m->cast_to_sint32();
         else
@@ -94,7 +94,7 @@ static checks_db generate_report(cfg_t& cfg, crab::invariant_table_t& pre_invari
 
     if (thread_local_options.check_termination) {
         auto last_inv = post_invariants.at(cfg.exit_label());
-        m_db.max_instruction_count = last_inv.get_instruction_count_upper_bound();
+        m_db.max_loop_count = last_inv.get_loop_count_upper_bound();
     }
     return m_db;
 }
@@ -122,8 +122,8 @@ static void print_report(std::ostream& os, const checks_db& db, const Instructio
         }
     }
     os << "\n";
-    crab::number_t max_instructions{100000};
-    if (db.max_instruction_count > max_instructions) {
+    crab::number_t max_loop_count{100000};
+    if (db.max_loop_count > max_loop_count) {
         os << "Could not prove termination.\n";
     }
 }
@@ -171,7 +171,7 @@ bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, const program_info& info, co
     if (stats) {
         stats->total_unreachable = report.total_unreachable;
         stats->total_warnings = report.total_warnings;
-        stats->max_instruction_count = report.get_max_instruction_count();
+        stats->max_loop_count = report.get_max_loop_count();
     }
     return (report.total_warnings == 0);
 }
@@ -224,7 +224,7 @@ bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const pro
     if (stats) {
         stats->total_unreachable = report.total_unreachable;
         stats->total_warnings = report.total_warnings;
-        stats->max_instruction_count = report.get_max_instruction_count();
+        stats->max_loop_count = report.get_max_loop_count();
     }
     return (report.total_warnings == 0);
 }

src/main/check.cpp

@@ -161,8 +161,8 @@ int main(int argc, char** argv) {
         const auto [res, seconds] = timed_execution([&] {
             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";
+        if (res && ebpf_verifier_options.check_termination && (ebpf_verifier_options.print_failures || ebpf_verifier_options.print_invariants)) {
+            std::cout << "Program terminates within " << verifier_stats.max_loop_count << " loop iterations\n";
         }
         std::cout << res << "," << seconds << "," << resident_set_size_kb() << "\n";
         return !res;