Add support for signed division and modulo instructions

src/asm_ostream.cpp

@@ -60,7 +60,9 @@ std::ostream& operator<<(std::ostream& os, Bin::Op op) {
     case Op::SUB: return os << "-";
     case Op::MUL: return os << "*";
     case Op::UDIV: return os << "/";
+    case Op::SDIV: return os << "s/";
     case Op::UMOD: return os << "%";
+    case Op::SMOD: return os << "s%";
     case Op::OR: return os << "|";
     case Op::AND: return os << "&";
     case Op::LSH: return os << "<<";

src/asm_parse.cpp

@@ -58,6 +58,7 @@ static const std::map<std::string, Bin::Op> str_to_binop = {
     {"", Bin::Op::MOV},   {"+", Bin::Op::ADD},  {"-", Bin::Op::SUB},    {"*", Bin::Op::MUL},
     {"/", Bin::Op::UDIV}, {"%", Bin::Op::UMOD}, {"|", Bin::Op::OR},     {"&", Bin::Op::AND},
     {"<<", Bin::Op::LSH}, {">>", Bin::Op::RSH}, {"s>>", Bin::Op::ARSH}, {"^", Bin::Op::XOR},
+    {"s/", Bin::Op::SDIV}, {"s%", Bin::Op::SMOD},
 };
 
 static const std::map<std::string, Un::Op> str_to_unop = {

src/asm_syntax.hpp

@@ -85,6 +85,8 @@ struct Bin {
         RSH,
         ARSH,
         XOR,
+        SDIV,
+        SMOD,
     };
 
     Op op;
@@ -262,6 +264,7 @@ struct Addable {
 // Condition check whether a register contains a non-zero number.
 struct ValidDivisor {
     Reg reg;
+    bool is_signed{};
 };
 
 enum class AccessType {
@@ -380,7 +383,7 @@ DECLARE_EQ2(TypeConstraint, reg, types)
 DECLARE_EQ2(ValidSize, reg, can_be_zero)
 DECLARE_EQ2(Comparable, r1, r2)
 DECLARE_EQ2(Addable, ptr, num)
-DECLARE_EQ1(ValidDivisor, reg)
+DECLARE_EQ2(ValidDivisor, reg, is_signed)
 DECLARE_EQ2(ValidStore, mem, val)
 DECLARE_EQ5(ValidAccess, reg, offset, width, or_null, access_type)
 DECLARE_EQ3(ValidMapKeyValue, access_reg, map_fd_reg, key)

src/asm_unmarshal.cpp

@@ -91,13 +91,23 @@ struct Unmarshaller {
         case INST_ALU_OP_ADD: return Bin::Op::ADD;
         case INST_ALU_OP_SUB: return Bin::Op::SUB;
         case INST_ALU_OP_MUL: return Bin::Op::MUL;
-        case INST_ALU_OP_DIV: return Bin::Op::UDIV;
+        case INST_ALU_OP_DIV:
+            switch (inst.offset) {
+            case 0: return Bin::Op::UDIV;
+            case 1: return Bin::Op::SDIV;
+            default: throw InvalidInstruction{pc, "invalid ALU op 0x30"};
+            }
         case INST_ALU_OP_OR: return Bin::Op::OR;
         case INST_ALU_OP_AND: return Bin::Op::AND;
         case INST_ALU_OP_LSH: return Bin::Op::LSH;
         case INST_ALU_OP_RSH: return Bin::Op::RSH;
         case INST_ALU_OP_NEG: return Un::Op::NEG;
-        case INST_ALU_OP_MOD: return Bin::Op::UMOD;
+        case INST_ALU_OP_MOD:
+            switch (inst.offset) {
+            case 0: return Bin::Op::UMOD;
+            case 1: return Bin::Op::SMOD;
+            default: throw InvalidInstruction{pc, "invalid ALU op 0x90"};
+            }
         case INST_ALU_OP_XOR: return Bin::Op::XOR;
         case INST_ALU_OP_MOV: return Bin::Op::MOV;
         case INST_ALU_OP_ARSH:

src/assertions.cpp

@@ -209,9 +209,12 @@ class AssertExtractor {
             }
         case Bin::Op::UDIV:
         case Bin::Op::UMOD:
+        case Bin::Op::SDIV:
+        case Bin::Op::SMOD:
             if (std::holds_alternative<Reg>(ins.v)) {
                 auto src = reg(ins.v);
-                return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}, Assert{ValidDivisor{src}}};
+                bool is_signed = (ins.op == Bin::Op::SDIV || ins.op == Bin::Op::SMOD);
+                return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}, Assert{ValidDivisor{src, is_signed}}};
             } else {
                 return {Assert{TypeConstraint{ins.dst, TypeGroup::number}}};
             }

src/crab/ebpf_domain.cpp

@@ -1527,8 +1527,8 @@ void ebpf_domain_t::operator()(const ValidDivisor& s) {
     if (!type_inv.implies_type(m_inv, type_is_pointer(reg), type_is_number(s.reg)))
         require(m_inv, linear_constraint_t::FALSE(), "Only numbers can be used as divisors");
     if (!thread_local_options.allow_division_by_zero) {
-        // Division is an unsigned operation. There are no eBPF instructions for signed division.
-        require(m_inv, reg.uvalue != 0, "Possible division by zero");
+        auto v = s.is_signed ? reg.svalue : reg.uvalue;
+        require(m_inv, v != 0, "Possible division by zero");
     }
 }
 
@@ -2435,6 +2435,14 @@ void ebpf_domain_t::operator()(const Bin& bin) {
             urem(dst.svalue, dst.uvalue, imm, finite_width);
             havoc_offsets(bin.dst);
             break;
+        case Bin::Op::SDIV:
+            sdiv(dst.svalue, dst.uvalue, imm, finite_width);
+            havoc_offsets(bin.dst);
+            break;
+        case Bin::Op::SMOD:
+            srem(dst.svalue, dst.uvalue, imm, finite_width);
+            havoc_offsets(bin.dst);
+            break;
         case Bin::Op::OR:
             bitwise_or(dst.svalue, dst.uvalue, imm);
             havoc_offsets(bin.dst);
@@ -2581,6 +2589,14 @@ void ebpf_domain_t::operator()(const Bin& bin) {
             urem(dst.svalue, dst.uvalue, src.uvalue, finite_width);
             havoc_offsets(bin.dst);
             break;
+        case Bin::Op::SDIV:
+            sdiv(dst.svalue, dst.uvalue, src.svalue, finite_width);
+            havoc_offsets(bin.dst);
+            break;
+        case Bin::Op::SMOD:
+            srem(dst.svalue, dst.uvalue, src.svalue, finite_width);
+            havoc_offsets(bin.dst);
+            break;
         case Bin::Op::OR:
             bitwise_or(dst.svalue, dst.uvalue, src.uvalue, finite_width);
             havoc_offsets(bin.dst);

src/crab/interval.cpp

@@ -51,7 +51,54 @@ interval_t interval_t::operator/(const interval_t& x) const {
     }
 }
 
-// Unsigned division
+// Signed division.
+interval_t interval_t::SDiv(const interval_t& x) const {
+    if (is_bottom() || x.is_bottom()) {
+        return bottom();
+    } else {
+        // Divisor is a singleton:
+        //   the linear interval solver can perform many divisions where
+        //   the divisor is a singleton interval. We optimize for this case.
+        std::optional<number_t> n = x.singleton();
+        if (n && n->fits_cast_to_int64()) {
+            number_t c{n->cast_to_sint64()};
+            if (c == 1) {
+                return *this;
+            } else if (c != 0) {
+                return interval_t(_lb / bound_t{c}, _ub / bound_t{c});
+            } else {
+                // The eBPF ISA defines division by 0 as resulting in 0.
+                return interval_t(number_t(0));
+            }
+        }
+        // Divisor is not a singleton
+        using z_interval = interval_t;
+        if (x[0]) {
+            // The divisor contains 0.
+            z_interval l(x._lb, z_bound(-1));
+            z_interval u(z_bound(1), x._ub);
+            return (SDiv(l) | SDiv(u) | z_interval(number_t(0)));
+        } else if (operator[](0)) {
+            // The dividend contains 0.
+            z_interval l(_lb, z_bound(-1));
+            z_interval u(z_bound(1), _ub);
+            return (l.SDiv(x) | u.SDiv(x) | z_interval(number_t(0)));
+        } else {
+            // Neither the dividend nor the divisor contains 0
+            z_interval a =
+                (_ub < number_t{0})
+                    ? (*this + ((x._ub < number_t{0}) ? (x + z_interval(number_t(1))) : (z_interval(number_t(1)) - x)))
+                    : *this;
+            bound_t ll = a._lb / x._lb;
+            bound_t lu = a._lb / x._ub;
+            bound_t ul = a._ub / x._lb;
+            bound_t uu = a._ub / x._ub;
+            return interval_t(bound_t::min(ll, lu, ul, uu), bound_t::max(ll, lu, ul, uu));
+        }
+    }
+}
+
+// Unsigned division.
 interval_t interval_t::UDiv(const interval_t& x) const {
     if (is_bottom() || x.is_bottom()) {
         return bottom();
@@ -97,7 +144,7 @@ interval_t interval_t::UDiv(const interval_t& x) const {
     }
 }
 
-// Signed remainder (modulo). eBPF has no instruction for this.
+// Signed remainder (modulo).
 interval_t interval_t::SRem(const interval_t& x) const {
     // note that the sign of the divisor does not matter
 

src/crab/interval.hpp

@@ -121,13 +121,7 @@ class bound_t final {
         } else if (is_finite() && x.is_finite()) {
             return bound_t(false, _n / x._n);
         } else if (is_finite() && x.is_infinite()) {
-            if (_n > 0) {
-                return x;
-            } else if (_n == 0) {
-                return *this;
-            } else {
-                return x.operator-();
-            }
+            return number_t{0};
         } else if (is_infinite() && x.is_finite()) {
             if (x._n > 0) {
                 return *this;
@@ -423,6 +417,8 @@ class interval_t final {
 
     // division and remainder operations
 
+    [[nodiscard]] interval_t SDiv(const interval_t& x) const;
+
     [[nodiscard]] interval_t UDiv(const interval_t& x) const;
 
     [[nodiscard]] interval_t SRem(const interval_t& x) const;

src/crab/split_dbm.cpp

@@ -951,7 +951,7 @@ void SplitDBM::apply(arith_binop_t op, variable_t x, variable_t y, variable_t z,
     case arith_binop_t::SUB: assign(x, linear_expression_t(y).subtract(z)); break;
     // For the rest of operations, we fall back on intervals.
     case arith_binop_t::MUL: set(x, get_interval(y, finite_width) * get_interval(z, finite_width)); break;
-    case arith_binop_t::SDIV: set(x, get_interval(y, finite_width) / get_interval(z, finite_width)); break;
+    case arith_binop_t::SDIV: set(x, get_interval(y, finite_width).SDiv(get_interval(z, finite_width))); break;
     case arith_binop_t::UDIV: set(x, get_interval(y, finite_width).UDiv(get_interval(z, finite_width))); break;
     case arith_binop_t::SREM: set(x, get_interval(y, finite_width).SRem(get_interval(z, finite_width))); break;
     case arith_binop_t::UREM: set(x, get_interval(y, finite_width).URem(get_interval(z, finite_width))); break;
@@ -969,7 +969,7 @@ void SplitDBM::apply(arith_binop_t op, variable_t x, variable_t y, const number_
     case arith_binop_t::SUB: assign(x, linear_expression_t(y).subtract(k)); break;
     case arith_binop_t::MUL: assign(x, linear_expression_t(k, y)); break;
     // For the rest of operations, we fall back on intervals.
-    case arith_binop_t::SDIV: set(x, get_interval(y, finite_width) / interval_t(k)); break;
+    case arith_binop_t::SDIV: set(x, get_interval(y, finite_width).SDiv(interval_t(k))); break;
     case arith_binop_t::UDIV: set(x, get_interval(y, finite_width).UDiv(interval_t(k))); break;
     case arith_binop_t::SREM: set(x, get_interval(y, finite_width).SRem(interval_t(k))); break;
     case arith_binop_t::UREM: set(x, get_interval(y, finite_width).URem(interval_t(k))); break;

src/test/test_yaml.cpp

@@ -23,7 +23,8 @@ YAML_CASE("test-data/add.yaml")
 YAML_CASE("test-data/assign.yaml")
 YAML_CASE("test-data/bitop.yaml")
 YAML_CASE("test-data/call.yaml")
-YAML_CASE("test-data/divmod.yaml")
+YAML_CASE("test-data/udivmod.yaml")
+YAML_CASE("test-data/sdivmod.yaml")
 YAML_CASE("test-data/full64.yaml")
 YAML_CASE("test-data/jump.yaml")
 YAML_CASE("test-data/loop.yaml")