PR feedback

Signed-off-by: Alan Jowett <[email protected]>

Author: Alan-Jowett

Diff for: src/crab/ebpf_transformer.cpp

@@ -942,10 +942,10 @@ void ebpf_transformer::forget_packet_pointers() {
     dom.initialize_packet();
 }
 
-static void overflow_bounds(NumAbsDomain& inv, variable_t lhs, number_t span, int finite_width, bool issigned) {
+static void overflow_bounds(NumAbsDomain& inv, variable_t lhs, int finite_width, bool issigned) {
     using namespace crab::dsl_syntax;
     auto interval = inv[lhs];
-    if (interval.ub() - interval.lb() >= span) {
+    if (interval.size() >= interval_t::unsigned_int(finite_width).size()) {
         // Interval covers the full space.
         inv -= lhs;
         return;
@@ -980,21 +980,11 @@ static void overflow_bounds(NumAbsDomain& inv, variable_t lhs, number_t span, in
 }
 
 static void overflow_signed(NumAbsDomain& inv, const variable_t lhs, const int finite_width) {
-    const auto span{finite_width == 64   ? number_t{std::numeric_limits<uint64_t>::max()}
-                    : finite_width == 32 ? number_t{std::numeric_limits<uint32_t>::max()}
-                    : finite_width == 16 ? number_t{std::numeric_limits<uint16_t>::max()}
-                    : finite_width == 8  ? number_t{std::numeric_limits<uint8_t>::max()}
-                                         : throw std::exception()};
-    overflow_bounds(inv, lhs, span, finite_width, true);
+    overflow_bounds(inv, lhs, finite_width, true);
 }
 
 static void overflow_unsigned(NumAbsDomain& inv, const variable_t lhs, const int finite_width) {
-    const auto span{finite_width == 64   ? number_t{std::numeric_limits<uint64_t>::max()}
-                    : finite_width == 32 ? number_t{std::numeric_limits<uint32_t>::max()}
-                    : finite_width == 16 ? number_t{std::numeric_limits<uint16_t>::max()}
-                    : finite_width == 8  ? number_t{std::numeric_limits<uint8_t>::max()}
-                                         : throw std::exception()};
-    overflow_bounds(inv, lhs, span, finite_width, false);
+    overflow_bounds(inv, lhs, finite_width, false);
 }
 static void apply_signed(NumAbsDomain& inv, const binop_t& op, const variable_t xs, const variable_t xu,
                          const variable_t y, const number_t& z, const int finite_width) {
@@ -1550,13 +1540,11 @@ void ebpf_transformer::do_store_stack(NumAbsDomain& inv, const linear_expression
     } else {
         if ((width == 1 || width == 2 || width == 4) && type_inv.get_type(m_inv, val_type) == T_NUM) {
             // Keep track of numbers on the stack that might be used as array indices.
-            auto stack_svalue = stack.store(inv, data_kind_t::svalues, addr, width, val_svalue);
-            auto stack_uvalue = stack.store(inv, data_kind_t::uvalues, addr, width, val_uvalue);
-            if (stack_svalue.has_value()) {
+            if (const auto stack_svalue = stack.store(inv, data_kind_t::svalues, addr, width, val_svalue)) {
                 inv.assign(stack_svalue, val_svalue);
                 overflow_signed(inv, *stack_svalue, width * 8);
             }
-            if (stack_uvalue.has_value()) {
+            if (const auto stack_uvalue = stack.store(inv, data_kind_t::uvalues, addr, width, val_uvalue)) {
                 inv.assign(stack_uvalue, val_uvalue);
                 overflow_unsigned(inv, *stack_uvalue, width * 8);
             }