From 59244394ae38e1b3241e945c28d0a122ec0714ef Mon Sep 17 00:00:00 2001 From: Dave Thaler Date: Mon, 20 Nov 2023 10:36:44 -0800 Subject: [PATCH] Add support for signed division and modulo instructions Fixes #523 Signed-off-by: Dave Thaler --- src/asm_ostream.cpp | 2 + src/asm_parse.cpp | 1 + src/asm_syntax.hpp | 5 +- src/asm_unmarshal.cpp | 14 +- src/assertions.cpp | 5 +- src/crab/ebpf_domain.cpp | 20 +- src/crab/interval.cpp | 51 ++- src/crab/interval.hpp | 10 +- src/crab/split_dbm.cpp | 4 +- src/test/test_yaml.cpp | 3 +- test-data/sdivmod.yaml | 571 ++++++++++++++++++++++++ test-data/{divmod.yaml => udivmod.yaml} | 0 12 files changed, 668 insertions(+), 18 deletions(-) create mode 100644 test-data/sdivmod.yaml rename test-data/{divmod.yaml => udivmod.yaml} (100%) diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp index 2ecdda978..43ff6491e 100644 --- a/src/asm_ostream.cpp +++ b/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 << "<<"; diff --git a/src/asm_parse.cpp b/src/asm_parse.cpp index 50d98f802..7ce6428ed 100644 --- a/src/asm_parse.cpp +++ b/src/asm_parse.cpp @@ -58,6 +58,7 @@ static const std::map 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 str_to_unop = { diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp index 09da5b6a4..4121bc9e0 100644 --- a/src/asm_syntax.hpp +++ b/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) diff --git a/src/asm_unmarshal.cpp b/src/asm_unmarshal.cpp index 4a9609d46..5cd3fdc99 100644 --- a/src/asm_unmarshal.cpp +++ b/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: diff --git a/src/assertions.cpp b/src/assertions.cpp index a76d5906d..4dd791470 100644 --- a/src/assertions.cpp +++ b/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(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}}}; } diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 072ffad67..62667c88e 100644 --- a/src/crab/ebpf_domain.cpp +++ b/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); diff --git a/src/crab/interval.cpp b/src/crab/interval.cpp index dd197e9ba..5aa333004 100644 --- a/src/crab/interval.cpp +++ b/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 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 diff --git a/src/crab/interval.hpp b/src/crab/interval.hpp index 5596d8d17..bf28cd2f5 100644 --- a/src/crab/interval.hpp +++ b/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; diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp index e6cce3021..8336ba40e 100644 --- a/src/crab/split_dbm.cpp +++ b/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; diff --git a/src/test/test_yaml.cpp b/src/test/test_yaml.cpp index e77f0ed05..44c89156f 100644 --- a/src/test/test_yaml.cpp +++ b/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") diff --git a/test-data/sdivmod.yaml b/test-data/sdivmod.yaml new file mode 100644 index 000000000..8da36fb5b --- /dev/null +++ b/test-data/sdivmod.yaml @@ -0,0 +1,571 @@ +# Copyright (c) Prevail Verifier contributors. +# SPDX-License-Identifier: MIT +--- +test-case: integer divided by non-integer + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.svalue=1", "r2.uvalue=1"] + +code: + : | + r1 s/= r2 + +post: + - r1.type=number + - r1.svalue=6 + - r1.uvalue=6 + - r2.svalue=1 + - r2.uvalue=1 + +messages: + - "0: Only numbers can be used as divisors (r2 != 0)" +--- +test-case: non-zero divided by zero immediate + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6"] + +code: + : | + r1 s/= 0 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 +--- +test-case: zero divided by zero immediate + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0"] + +code: + : | + r1 s/= 0 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 +--- +test-case: non-zero divided by zero register + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number", "r2.svalue=0", "r2.uvalue=0"] + +options: ["!allow_division_by_zero"] + +code: + : | + r1 s/= r2 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + - r2.svalue=0 + - r2.uvalue=0 + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: non-zero divided by zero register without warning + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number", "r2.svalue=0", "r2.uvalue=0"] + +code: + : | + r1 s/= r2 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + - r2.svalue=0 + - r2.uvalue=0 +--- +test-case: zero divided by zero register + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", + "r2.type=number", "r2.svalue=0", "r2.uvalue=0"] + +options: ["!allow_division_by_zero"] + +code: + : | + r1 s/= r2 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + - r2.svalue=0 + - r2.uvalue=0 + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: non-zero divided by possibly zero register + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number", "r2.svalue=[-5, 5]"] + +options: ["!allow_division_by_zero"] + +code: + : | + r1 s/= r2 ; this could divide by 0 + +post: + - r1.type=number + - r1.svalue=[-6, 6] + - r2.type=number + - r2.svalue=[-5, 5] + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: zero divided by possibly zero register + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", + "r2.type=number", "r2.svalue=[-5, 5]"] + +options: ["!allow_division_by_zero"] + +code: + : | + r1 s/= r2 ; this could divide by 0 but ok to set to 0 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + - r2.svalue=[-5, 5] + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: non-zero divided by possibly zero register 2 + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.svalue=r2.uvalue"] + +options: ["!allow_division_by_zero"] + +code: + : | + r1 s/= r2 ; this could divide by 0 + +post: + - r1.type=number + - r1.svalue=[0, 6] + - r1.uvalue=[0, 6] + - r1.svalue=r1.uvalue + - r2.type=number + - r2.svalue=[0, 5] + - r2.uvalue=[0, 5] + - r2.svalue=r2.uvalue + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: zero divided by possibly zero register 2 + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", + "r2.type=number", "r2.svalue=[-5, 0]"] + +code: + : | + r1 s/= r2 ; this could divide by 0 but ok to set to 0 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + - r2.svalue=[-5, 0] + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: non-zero divided by undefined value register + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number"] + +code: + : | + r1 s/= r2 ; this could divide by 0 + +post: + - r1.type=number + - r1.svalue=[-6, 6] + - r2.type=number + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: zero divided by undefined value register + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", + "r2.type=number"] + +code: + : | + r1 s/= r2 ; this could divide by 0 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: undefined value register divided by signed non-zero range + +pre: ["r1.type=number", "r1.svalue=[-9223372036854775808, -1]", + "r2.type=number"] + +code: + : | + r2 s/= r1 + +post: + - r1.type=number + - r1.svalue=[-9223372036854775808, -1] + - r2.type=number +--- +test-case: non-zero modulo zero immediate + +pre: ["r1.type=number", "r1.svalue=-6", "r1.uvalue=18446744073709551610"] + +code: + : | + r1 s%= 0 + +post: + - r1.type=number + - r1.svalue=-6 + - r1.uvalue=18446744073709551610 +--- +test-case: zero modulo zero immediate + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0"] + +code: + : | + r1 s%= 0 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 +--- +test-case: non-zero modulo zero register + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=-6", "r1.uvalue=18446744073709551610", + "r2.type=number", "r2.svalue=0", "r2.uvalue=0"] + +code: + : | + r1 s%= r2 + +post: + - r1.type=number + - r1.svalue=-6 + - r1.uvalue=18446744073709551610 + - r2.type=number + - r2.svalue=0 + - r2.uvalue=0 + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: non-zero modulo zero register without warning + +pre: ["r1.type=number", "r1.svalue=-6", "r1.uvalue=18446744073709551610", + "r2.type=number", "r2.svalue=0", "r2.uvalue=0"] + +code: + : | + r1 s%= r2 + +post: + - r1.type=number + - r1.svalue=-6 + - r1.uvalue=18446744073709551610 + - r2.type=number + - r2.svalue=0 + - r2.uvalue=0 +--- +test-case: zero modulo zero register + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", + "r2.type=number", "r2.svalue=0", "r2.uvalue=0"] + +code: + : | + r1 s%= r2 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + - r2.svalue=0 + - r2.uvalue=0 + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: non-zero modulo possibly zero register + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number", "r2.svalue=[-5, 5]"] + +code: + : | + r1 s%= r2 ; this could do modulo 0 so could set r1 = r2 + +post: + - r1.type=number + - r1.svalue=[0, 6] + - r1.uvalue=[0, 6] + - r1.svalue=r1.uvalue + - r2.type=number + - r2.svalue=[-5, 5] + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: zero modulo possibly zero register + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", + "r2.type=number", "r2.svalue=[-5, 5]"] + +code: + : | + r1 s%= r2 ; this could do modulo 0 so could set r1 = r2 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + - r2.svalue=[-5, 5] + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: non-zero modulo possibly zero register 2 + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number", "r2.svalue=[0, 5]", "r2.uvalue=[0, 5]", "r2.svalue=r2.uvalue"] + +code: + : | + r1 s%= r2 ; this could do modulo 0 so could set r1 = r2 + +post: + - r1.type=number + - r1.svalue=[0, 6] + - r1.uvalue=[0, 6] + - r1.svalue=r1.uvalue + - r2.type=number + - r2.svalue=[0, 5] + - r2.uvalue=[0, 5] + - r2.svalue=r2.uvalue + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: zero modulo possibly zero register 2 + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", + "r2.type=number", "r2.svalue=[-5, 0]"] + +code: + : | + r1 s%= r2 ; this could do modulo 0 so could set r1 = r2 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + - r2.svalue=[-5, 0] + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: non-zero modulo undefined value register + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number"] + +code: + : | + r1 s%= r2 ; this could be modulo 0 + +post: + - r1.type=number + - r1.svalue=[0, 6] + - r1.uvalue=[0, 6] + - r1.svalue=r1.uvalue + - r2.type=number + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: zero modulo undefined value register + +options: ["!allow_division_by_zero"] + +pre: ["r1.type=number", "r1.svalue=0", "r1.uvalue=0", + "r2.type=number"] + +code: + : | + r1 s%= r2 ; this could be modulo 0 + +post: + - r1.type=number + - r1.svalue=0 + - r1.uvalue=0 + - r2.type=number + +messages: + - "0: Possible division by zero (r2 != 0)" +--- +test-case: positive modulo positive range + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number", "r2.svalue=[1, 5]", "r2.uvalue=[1, 5]"] + +code: + : | + r1 s%= r2 + +post: + - r1.type=number + - r1.svalue=[0, 4] + - r1.uvalue=[0, 4] + - r1.svalue=r1.uvalue + - r2.type=number + - r2.svalue=[1, 5] + - r2.uvalue=[1, 5] +--- +test-case: negative modulo positive + +pre: ["r1.type=number", "r1.svalue=-13", "r1.uvalue=18446744073709551603"] + +code: + : | + r1 s%= 4 + +post: + - r1.type=number + - r1.svalue=-1 + - r1.uvalue=18446744073709551615 +--- +test-case: positive modulo negative + +pre: ["r1.type=number", "r1.svalue=13", "r1.uvalue=13"] + +code: + : | + r1 s%= -3 + +post: + - r1.type=number + - r1.svalue=1 + - r1.uvalue=1 +--- +test-case: positive modulo negative range + +pre: ["r1.type=number", "r1.svalue=13", "r1.uvalue=13", + "r2.type=number", "r2.svalue=[-3, -2]", "r2.uvalue=[18446744073709551613, 18446744073709551614]"] + +code: + : | + r1 s%= r2 + +post: + - r1.type=number + - r1.svalue=[0, 2] + - r1.uvalue=[0, 2] + - r1.svalue=r1.uvalue + - r2.type=number + - r2.svalue=[-3, -2] + - r2.uvalue=[18446744073709551613, 18446744073709551614] +--- +test-case: negative modulo negative + +pre: ["r1.type=number", "r1.svalue=-13", "r1.uvalue=18446744073709551603"] + +code: + : | + r1 s%= -3 + +post: + - r1.type=number + - r1.svalue=-1 + - r1.uvalue=18446744073709551615 +--- +test-case: negative modulo negative range + +pre: ["r1.type=number", "r1.svalue=-13", "r1.uvalue=18446744073709551603", + "r2.type=number", "r2.svalue=[-3, -2]", "r2.uvalue=[18446744073709551613, 18446744073709551614]"] + +code: + : | + r1 s%= r2 + +post: + - r1.type=number + - r1.svalue=[-2, 0] + - r2.type=number + - r2.svalue=[-3, -2] + - r2.uvalue=[18446744073709551613, 18446744073709551614] +--- +test-case: smaller modulo larger + +pre: ["r1.type=number", "r1.svalue=6", "r1.uvalue=6", + "r2.type=number", "r2.svalue=[7, 10]", "r2.uvalue=[7, 10]"] + +code: + : | + r1 s%= r2 + +post: + - r1.type=number + - r1.svalue=6 + - r1.uvalue=6 + - r2.type=number + - r2.svalue=[7, 10] + - r2.uvalue=[7, 10] diff --git a/test-data/divmod.yaml b/test-data/udivmod.yaml similarity index 100% rename from test-data/divmod.yaml rename to test-data/udivmod.yaml