narrow to constant bounds once (#479)

Signed-off-by: Elazar Gershuni <[email protected]>

CMakeLists.txt

@@ -80,10 +80,8 @@ file(GLOB LIB_SRC
 file(GLOB ALL_TEST
         "./src/test/test.cpp"
         "./src/test/test_conformance.cpp"
-        "./src/test/test_loop.cpp"
         "./src/test/test_marshal.cpp"
         "./src/test/test_print.cpp"
-        "./src/test/test_termination.cpp"
         "./src/test/test_verify.cpp"
         "./src/test/test_wto.cpp"
         "./src/test/test_yaml.cpp"

src/asm_marshal.cpp

@@ -229,6 +229,10 @@ struct MarshalVisitor {
             .offset = static_cast<int16_t>(b.access.offset),
             .imm = 0}};
     }
+
+    vector<ebpf_inst> operator()(IncrementLoopCounter const& ins) {
+        return {};
+    }
 };
 
 vector<ebpf_inst> marshal(const Instruction& ins, pc_t pc) { return std::visit(MarshalVisitor{label_to_offset(pc)}, ins); }

src/asm_ostream.cpp

@@ -329,6 +329,9 @@ struct InstructionPrinterVisitor {
         os_ << "assert " << a.cst;
     }
 
+    void operator()(IncrementLoopCounter const& a) {
+        os_ << crab::variable_t::instruction_count(to_string(a.name)) << "++";
+    }
 };
 
 string to_string(label_t const& label) {

src/asm_ostream.hpp

@@ -48,5 +48,6 @@ inline std::ostream& operator<<(std::ostream& os, Mem const& a) { return os << (
 inline std::ostream& operator<<(std::ostream& os, LockAdd const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Assume const& a) { return os << (Instruction)a; }
 inline std::ostream& operator<<(std::ostream& os, Assert const& a) { return os << (Instruction)a; }
+inline std::ostream& operator<<(std::ostream& os, IncrementLoopCounter const& a) { return os << (Instruction)a; }
 std::ostream& operator<<(std::ostream& os, AssertionConstraint const& a);
 std::string to_string(AssertionConstraint const& constraint);

src/asm_syntax.hpp

@@ -309,7 +309,11 @@ struct Assert {
     Assert(AssertionConstraint cst): cst(cst) { }
 };
 
-using Instruction = std::variant<Undefined, Bin, Un, LoadMapFd, Call, Exit, Jmp, Mem, Packet, LockAdd, Assume, Assert>;
+struct IncrementLoopCounter {
+    label_t name;
+};
+
+using Instruction = std::variant<Undefined, Bin, Un, LoadMapFd, Call, Exit, Jmp, Mem, Packet, LockAdd, Assume, Assert, IncrementLoopCounter>;
 
 using LabeledInstruction = std::tuple<label_t, Instruction, std::optional<btf_line_info_t>>;
 using InstructionSeq = std::vector<LabeledInstruction>;
@@ -382,6 +386,7 @@ DECLARE_EQ5(ValidAccess, reg, offset, width, or_null, access_type)
 DECLARE_EQ3(ValidMapKeyValue, access_reg, map_fd_reg, key)
 DECLARE_EQ1(ZeroCtxOffset, reg)
 DECLARE_EQ1(Assert, cst)
+DECLARE_EQ1(IncrementLoopCounter, name)
 
 }
 

src/assertions.cpp

@@ -38,6 +38,8 @@ class AssertExtractor {
 
     vector<Assert> operator()(Assert const& ins) const { assert(false); return {}; }
 
+    vector<Assert> operator()(IncrementLoopCounter ins) const { assert(false); return {}; }
+
     vector<Assert> operator()(LoadMapFd const& ins) const { return {}; }
 
     /// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.

src/crab/ebpf_domain.cpp

@@ -909,8 +909,39 @@ ebpf_domain_t ebpf_domain_t::operator&(const ebpf_domain_t& other) const {
     return ebpf_domain_t(m_inv & other.m_inv, stack & other.stack);
 }
 
-ebpf_domain_t ebpf_domain_t::widen(const ebpf_domain_t& other) {
-    return ebpf_domain_t(m_inv.widen(other.m_inv), stack | other.stack);
+ebpf_domain_t ebpf_domain_t::calculate_constant_limits() {
+    ebpf_domain_t inv;
+    using namespace crab::dsl_syntax;
+    for (int i : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}) {
+        auto r = reg_pack(i);
+        inv += r.svalue <= std::numeric_limits<int32_t>::max();
+        inv += r.svalue >= std::numeric_limits<int32_t>::min();
+        inv += r.uvalue <= std::numeric_limits<uint32_t>::max();
+        inv += r.uvalue >= 0;
+        inv += r.stack_offset <= EBPF_STACK_SIZE;
+        inv += r.stack_offset >= 0;
+        inv += r.shared_offset <= r.shared_region_size;
+        inv += r.shared_offset >= 0;
+        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()) {
+                inv += counter <= std::numeric_limits<int32_t>::max();
+                inv += counter >= 0;
+                inv += counter <= r.svalue;
+            }
+        }
+    }
+    return inv;
+}
+
+static const ebpf_domain_t constant_limits = ebpf_domain_t::calculate_constant_limits();
+
+ebpf_domain_t ebpf_domain_t::widen(const ebpf_domain_t& other, bool to_constants) {
+    ebpf_domain_t res{m_inv.widen(other.m_inv), stack | other.stack};
+    if (to_constants)
+        return res & constant_limits;
+    return res;
 }
 
 ebpf_domain_t ebpf_domain_t::narrow(const ebpf_domain_t& other) {
@@ -1333,19 +1364,10 @@ void ebpf_domain_t::overflow_unsigned(NumAbsDomain& inv, variable_t lhs, int fin
     overflow_bounds(inv, lhs, span, finite_width, false);
 }
 
-void ebpf_domain_t::operator()(const basic_block_t& bb, bool check_termination) {
+void ebpf_domain_t::operator()(const basic_block_t& bb) {
     for (const Instruction& statement : bb) {
         std::visit(*this, statement);
     }
-    if (check_termination) {
-        // +1 to avoid being tricked by empty loops
-        add(variable_t::instruction_count(), crab::number_t((unsigned)bb.size() + 1));
-    }
-}
-
-bound_t ebpf_domain_t::get_instruction_count_upper_bound() {
-    const auto& ub = m_inv[variable_t::instruction_count()].ub();
-    return ub;
 }
 
 void ebpf_domain_t::check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb,
@@ -2681,7 +2703,7 @@ void ebpf_domain_t::initialize_packet(ebpf_domain_t& inv) {
 ebpf_domain_t ebpf_domain_t::from_constraints(const std::set<std::string>& constraints, bool setup_constraints) {
     ebpf_domain_t inv;
     if (setup_constraints) {
-        inv = ebpf_domain_t::setup_entry(false, false);
+        inv = ebpf_domain_t::setup_entry(false);
     }
     auto numeric_ranges = std::vector<crab::interval_t>();
     for (const auto& cst : parse_linear_constraints(constraints, numeric_ranges)) {
@@ -2696,7 +2718,7 @@ ebpf_domain_t ebpf_domain_t::from_constraints(const std::set<std::string>& const
     return inv;
 }
 
-ebpf_domain_t ebpf_domain_t::setup_entry(bool check_termination, bool init_r1) {
+ebpf_domain_t ebpf_domain_t::setup_entry(bool init_r1) {
     using namespace crab::dsl_syntax;
 
     ebpf_domain_t inv;
@@ -2719,10 +2741,21 @@ ebpf_domain_t ebpf_domain_t::setup_entry(bool check_termination, bool init_r1) {
     }
 
     initialize_packet(inv);
-    if (check_termination) {
-        inv.assign(variable_t::instruction_count(), 0);
-    }
     return inv;
 }
 
+void ebpf_domain_t::initialize_instruction_count(const label_t label) {
+    m_inv.assign(variable_t::instruction_count(to_string(label)), 0);
+}
+
+bound_t ebpf_domain_t::get_instruction_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());
+    return ub;
+}
+
+void ebpf_domain_t::operator()(const IncrementLoopCounter& ins) {
+    this->add(variable_t::instruction_count(to_string(ins.name)), 1);
+}
 } // namespace crab

src/crab/ebpf_domain.hpp

@@ -41,20 +41,20 @@ class ebpf_domain_t final {
     ebpf_domain_t operator|(const ebpf_domain_t& other) const&;
     ebpf_domain_t operator|(const ebpf_domain_t& other) &&;
     ebpf_domain_t operator&(const ebpf_domain_t& other) const;
-    ebpf_domain_t widen(const ebpf_domain_t& other);
+    ebpf_domain_t widen(const ebpf_domain_t& other, bool to_constants);
     ebpf_domain_t widening_thresholds(const ebpf_domain_t& other, const crab::iterators::thresholds_t& ts);
     ebpf_domain_t narrow(const ebpf_domain_t& other);
 
     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();
-    static ebpf_domain_t setup_entry(bool check_termination, bool init_r1);
+    static ebpf_domain_t setup_entry(bool init_r1);
 
     static ebpf_domain_t from_constraints(const std::set<std::string>& constraints, bool setup_constraints);
     string_invariant to_set();
 
     // abstract transformers
-    void operator()(const basic_block_t& bb, bool check_termination);
+    void operator()(const basic_block_t& bb);
 
     void operator()(const Addable&);
     void operator()(const Assert&);
@@ -77,7 +77,10 @@ class ebpf_domain_t final {
     void operator()(const ValidSize&);
     void operator()(const ValidStore&);
     void operator()(const ZeroCtxOffset&);
+    void operator()(const IncrementLoopCounter&);
 
+    void initialize_instruction_count(label_t label);
+    static ebpf_domain_t calculate_constant_limits();
   private:
     // private generic domain functions
     void operator+=(const linear_constraint_t& cst);

src/crab/fwd_analyzer.cpp

@@ -48,44 +48,37 @@ class interleaved_fwd_fixpoint_iterator_t final {
     wto_t _wto;
     invariant_table_t _pre, _post;
 
-    /// number of iterations until triggering widening
-    const unsigned int _widening_delay{1};
-
     /// number of narrowing iterations. If the narrowing operator is
     /// indeed a narrowing operator this parameter is not
     /// needed. However, there are abstract domains for which an actual
     /// narrowing operation is not available so we must enforce
     /// termination.
-    const unsigned int _descending_iterations;
+    static constexpr unsigned int _descending_iterations = 2000000;
 
     /// Used to skip the analysis until _entry is found
     bool _skip{true};
 
-    /// Whether the domain tracks instruction count; the invariants are somewhat easier to read without it
-    /// Generally corresponds to the check_termination flag in ebpf_verifier_options_t
-    const bool check_termination;
-
   private:
-    inline void set_pre(const label_t& label, const ebpf_domain_t& v) { _pre[label] = v; }
+    void set_pre(const label_t& label, const ebpf_domain_t& v) { _pre[label] = v; }
 
-    inline void transform_to_post(const label_t& label, ebpf_domain_t pre) {
+    void transform_to_post(const label_t& label, ebpf_domain_t pre) {
         basic_block_t& bb = _cfg.get_node(label);
-        pre(bb, check_termination);
+        pre(bb);
         _post[label] = std::move(pre);
     }
 
-    [[nodiscard]]
-    ebpf_domain_t extrapolate(const label_t& node, unsigned int iteration, ebpf_domain_t before,
-                              const ebpf_domain_t& after) const {
-        if (iteration <= _widening_delay) {
+    [[nodiscard]] static ebpf_domain_t extrapolate(ebpf_domain_t before, const ebpf_domain_t& after,
+                                                   unsigned int iteration) {
+        /// number of iterations until triggering widening
+        constexpr auto _widening_delay = 2;
+
+        if (iteration < _widening_delay) {
             return before | after;
-        } else {
-            return before.widen(after);
         }
+        return before.widen(after, iteration == _widening_delay);
     }
 
-    static ebpf_domain_t refine(const label_t& node, unsigned int iteration, ebpf_domain_t before,
-                                const ebpf_domain_t& after) {
+    static ebpf_domain_t refine(ebpf_domain_t before, const ebpf_domain_t& after, unsigned int iteration) {
         if (iteration == 1) {
             return before & after;
         } else {
@@ -102,8 +95,7 @@ class interleaved_fwd_fixpoint_iterator_t final {
     }
 
   public:
-    explicit interleaved_fwd_fixpoint_iterator_t(cfg_t& cfg, unsigned int descending_iterations, bool check_termination)
-        : _cfg(cfg), _wto(cfg), _descending_iterations(descending_iterations), check_termination(check_termination) {
+    explicit interleaved_fwd_fixpoint_iterator_t(cfg_t& cfg) : _cfg(cfg), _wto(cfg) {
         for (const auto& label : _cfg.labels()) {
             _pre.emplace(label, ebpf_domain_t::bottom());
             _post.emplace(label, ebpf_domain_t::bottom());
@@ -114,17 +106,28 @@ class interleaved_fwd_fixpoint_iterator_t final {
 
     ebpf_domain_t get_post(const label_t& node) { return _post.at(node); }
 
-    void operator()(const label_t& vertex);
+    void operator()(const label_t& node);
 
     void operator()(std::shared_ptr<wto_cycle_t>& cycle);
 
-    friend std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, const ebpf_domain_t& entry_inv, bool check_termination);
+    friend std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv);
 };
 
-std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, const ebpf_domain_t& entry_inv, bool check_termination) {
+std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv) {
     // Go over the CFG in weak topological order (accounting for loops).
-    constexpr unsigned int descending_iterations = 2000000;
-    interleaved_fwd_fixpoint_iterator_t analyzer(cfg, descending_iterations, check_termination);
+    interleaved_fwd_fixpoint_iterator_t analyzer(cfg);
+    if (thread_local_options.check_termination) {
+        std::vector<label_t> cycle_heads;
+        for (auto& component : analyzer._wto) {
+            if (std::holds_alternative<std::shared_ptr<wto_cycle_t>>(*component)) {
+                cycle_heads.push_back(std::get<std::shared_ptr<wto_cycle_t>>(*component)->head());
+            }
+        }
+        for (const label_t& label : cycle_heads) {
+            entry_inv.initialize_instruction_count(label);
+            cfg.get_node(label).insert(IncrementLoopCounter{label});
+        }
+    }
     analyzer.set_pre(cfg.entry_label(), entry_inv);
     for (auto& component : analyzer._wto) {
         std::visit(analyzer, *component);
@@ -164,61 +167,56 @@ void interleaved_fwd_fixpoint_iterator_t::operator()(std::shared_ptr<wto_cycle_t
         }
     }
 
-    ebpf_domain_t pre = ebpf_domain_t::bottom();
+    ebpf_domain_t invariant = ebpf_domain_t::bottom();
     if (entry_in_this_cycle) {
-        pre = get_pre(_cfg.entry_label());
+        invariant = get_pre(_cfg.entry_label());
     } else {
         wto_nesting_t cycle_nesting = _wto.nesting(head);
         for (const label_t& prev : _cfg.prev_nodes(head)) {
             if (!(_wto.nesting(prev) > cycle_nesting)) {
-                pre |= get_post(prev);
+                invariant |= get_post(prev);
             }
         }
     }
 
     for (unsigned int iteration = 1;; ++iteration) {
         // Increasing iteration sequence with widening
-        set_pre(head, pre);
-        transform_to_post(head, pre);
+        set_pre(head, invariant);
+        transform_to_post(head, invariant);
         for (auto& component : *cycle) {
             wto_component_t c = *component;
             if (!std::holds_alternative<label_t>(c) || (std::get<label_t>(c) != head))
                 std::visit(*this, *component);
         }
         ebpf_domain_t new_pre = join_all_prevs(head);
-        if (new_pre <= pre) {
+        if (new_pre <= invariant) {
             // Post-fixpoint reached
             set_pre(head, new_pre);
-            pre = std::move(new_pre);
+            invariant = std::move(new_pre);
             break;
         } else {
-            pre = extrapolate(head, iteration, pre, new_pre);
+            invariant = extrapolate(invariant, new_pre, iteration);
         }
     }
 
-    if (this->_descending_iterations == 0) {
-        // no narrowing
-        return;
-    }
-
     for (unsigned int iteration = 1;; ++iteration) {
         // Decreasing iteration sequence with narrowing
-        transform_to_post(head, pre);
+        transform_to_post(head, invariant);
 
         for (auto& component : *cycle) {
             wto_component_t c = *component;
             if (!std::holds_alternative<label_t>(c) || (std::get<label_t>(c) != head))
                 std::visit(*this, *component);
         }
         ebpf_domain_t new_pre = join_all_prevs(head);
-        if (pre <= new_pre) {
+        if (invariant <= new_pre) {
             // No more refinement possible(pre == new_pre)
             break;
         } else {
             if (iteration > _descending_iterations)
                 break;
-            pre = refine(head, iteration, pre, new_pre);
-            set_pre(head, pre);
+            invariant = refine(invariant, new_pre, iteration);
+            set_pre(head, invariant);
         }
     }
 }

src/crab/fwd_analyzer.hpp

@@ -13,7 +13,6 @@ namespace crab {
 
 using invariant_table_t = std::map<label_t, ebpf_domain_t>;
 
-std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, const ebpf_domain_t& entry_inv,
-                                                                     bool check_termination);
+std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(cfg_t& cfg, ebpf_domain_t entry_inv);
 
 } // namespace crab