Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 34 additions & 0 deletions codegen/masm/intrinsics/i64.masm
Original file line number Diff line number Diff line change
Expand Up @@ -253,6 +253,40 @@ pub proc checked_div # [b_lo, b_hi, a_lo, a_hi]
end
end

# Computes `a % b`, asserting that both inputs are valid i64 values (u32 limbs).
#
# Execution traps on division by zero, and on `i64::MIN % -1` (the underlying division overflows).
pub proc checked_mod # [b_lo, b_hi, a_lo, a_hi]

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should add type signatures to all new intrinsics

u32assertw

# Trap on i64::MIN % -1, since the underlying division overflows.
dup.1 dup.1 # [b_lo, b_hi, b_lo, b_hi, a_lo, a_hi]
push.NEG1_HI push.NEG1_LO exec.::miden::core::math::u64::eq # [b == -1, b_lo, b_hi, a_lo, a_hi]
dup.4 dup.4 # [a_lo, a_hi, b == -1, b_lo, b_hi, a_lo, a_hi]
push.MIN_HI push.MIN_LO exec.::miden::core::math::u64::eq # [a == MIN, b == -1, b_lo, b_hi, a_lo, a_hi]
and assertz # [b_lo, b_hi, a_lo, a_hi]

# The remainder takes the sign of the dividend `a`, so `is_signed_a` will be needed later.
dup.3 push.SIGN_BIT u32and push.SIGN_BIT eq # [is_a_signed, b_lo, b_hi, a_lo, a_hi]
movdn.4 # [b_lo, b_hi, a_lo, a_hi, is_a_signed]

# abs(a)
movup.3 movup.3 # [a_lo, a_hi, b_lo, b_hi, is_a_signed]
dup.4 movdn.2 # [a_lo, a_hi, is_a_signed, b_lo, b_hi, is_a_signed]
exec.cneg_u64 # [abs_a_lo, abs_a_hi, b_lo, b_hi, is_a_signed]

# abs(b)
movup.3 movup.3 # [b_lo, b_hi, abs_a_lo, abs_a_hi, is_a_signed]
dup.1 push.SIGN_BIT u32and push.SIGN_BIT eq # [is_b_signed, b_lo, b_hi, abs_a_lo, abs_a_hi, is_a_signed]
movdn.2 exec.cneg_u64 # [abs_b_lo, abs_b_hi, abs_a_lo, abs_a_hi, is_a_signed]

# r = abs(a) % abs(b); traps on division by zero.
exec.::miden::core::math::u64::mod # [r_lo, r_hi, is_a_signed]

# Apply the dividend's sign to the remainder.
exec.cneg_u64 # [result_lo, result_hi]
end

# Given two i64 values in two's complement representation, compare them,
# returning -1 if `a` < `b`, 0 if equal, and 1 if `a` > `b`.
pub proc icmp # [b_lo, b_hi, a_lo, a_hi]
Expand Down
6 changes: 4 additions & 2 deletions codegen/masm/src/emit/binary.rs
Original file line number Diff line number Diff line change
Expand Up @@ -654,8 +654,9 @@ impl OpEmitter<'_> {
assert_eq!(ty, rhs.ty(), "expected mod operands to be the same type");
match &ty {
Type::U64 => self.checked_mod_u64(span),
Type::I32 => self.checked_mod_i32(span),
Type::I64 => self.checked_mod_i64(span),
Type::U32 => self.checked_mod_u32(span),
Type::I32 => self.checked_mod_i32(span),
ty @ (Type::U16 | Type::U8) => {
self.checked_mod_uint(ty.size_in_bits() as u32, span);
}
Expand All @@ -678,8 +679,9 @@ impl OpEmitter<'_> {
self.push_immediate(imm, span);
self.checked_mod_u64(span);
}
Type::I32 => self.checked_mod_imm_i32(imm.as_i32().unwrap(), span),
Type::I64 => self.checked_mod_imm_i64(imm.as_i64().unwrap(), span),
Type::U32 => self.checked_mod_imm_u32(imm.as_u32().unwrap(), span),
Type::I32 => self.checked_mod_imm_i32(imm.as_i32().unwrap(), span),
ty @ (Type::U16 | Type::U8) => {
self.checked_mod_imm_uint(imm.as_u32().unwrap(), ty.size_in_bits() as u32, span);
}
Expand Down
18 changes: 18 additions & 0 deletions codegen/masm/src/emit/int64.rs
Original file line number Diff line number Diff line change
Expand Up @@ -713,6 +713,24 @@ impl OpEmitter<'_> {
self.raw_exec("::intrinsics::i64::checked_div", span);
}

/// Pops two i64 values off the stack, `b` and `a`, and performs `a % b`.
///
/// This operation is checked, so if the operands or result are not valid i64, execution traps.
pub fn checked_mod_i64(&mut self, span: SourceSpan) {
self.raw_exec("::intrinsics::i64::checked_mod", span);
}

/// Pops a i64 value off the stack, `a`, and performs `a % <imm>`.
///
/// This function will panic if the divisor is zero.
///
/// This operation is checked, so if the operand or result are not valid i64, execution traps.
pub fn checked_mod_imm_i64(&mut self, imm: i64, span: SourceSpan) {
assert_ne!(imm, 0, "division by zero is not allowed");
self.push_i64(imm, span);
self.raw_exec("::intrinsics::i64::checked_mod", span);
}

/// Pops two u64 values off the stack, `b` and `a`, and pushes the result of `a / b` on the
/// stack.
///
Expand Down
2 changes: 0 additions & 2 deletions tests/integration/src/end_to_end/arithmetic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -647,7 +647,6 @@ fn overflowing_rem_i32() {
}

#[test]
#[ignore = "https://github.com/0xMiden/compiler/issues/1000"]
fn overflowing_rem_i64() {
test_overflowing_arith(
i64::overflowing_rem,
Expand Down Expand Up @@ -868,7 +867,6 @@ fn checked_rem_i32() {
}

#[test]
#[ignore = "https://github.com/0xMiden/compiler/issues/1000"]
fn checked_rem_i64() {
test_checked_arith(i64::checked_rem, "checked_rem", NumericStrategy::rem_signed_checked());
}
Expand Down
24 changes: 24 additions & 0 deletions tests/integration/src/end_to_end/intrinsics/i64_arithmetic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -363,6 +363,30 @@ fn i64_checked_div() {
);
}

#[test]
fn i64_checked_mod() {
let proc_body = r#"
# Stack: [b_lo, b_hi, a_lo, a_hi]
exec.::intrinsics::i64::checked_mod
# Stack: [r_lo, r_hi]
"#;
test_i64_intrinsic(
proc_body,
NumericStrategy::<i64>::rem_signed_checked(),
binary_i64op_inputs_to_stack,
|(a, b): &(i64, i64)| {
if *b == 0 {
Err(TrapExpectation::DivideByZero)
} else if *a == i64::MIN && *b == -1 {

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

WebAssembly signed remainder is only undefined for a zero divisor; i64.rem_s(i64::MIN, -1) should return 0, not trap (WebAssembly numerics, irem_s).

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

i64.rem_s(i64::MIN, -1) should return 0, not trap

I think this means we have a bug in the lowering of Wasm's i64.rem_s which tests do not catch:

  • Wasm i64.rem_s is probably compiled to i64::checked_mod intrinsic
  • For (i64::MIN, -1) Wasm returns 0 but the intrinsic traps

The arith tests i64::checked_rem and i64::overflowing_rem do hit the intrinsic i64::checked_mod. Though when compiling i64::checked_rem, i64::overflowing_rem from Rust to Wasm, the generated Wasm handles edge cases explicitly, thus hiding the bug.

My plan is:

  • Add test(s) to check whether the i64.rem_s lowering is fine or not
  • Fix it if needed. Maybe by adding intrinsic i64::wrapping_mod and lowering i64.rem_s to that.

The same issue should then also exist for i32.rem_s and the i32::checked_mod intrinsic.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good!

Err(TrapExpectation::FailedAssertionOverflow)
} else {
Ok(vec![a.checked_rem(*b).unwrap()])
}
},
|stack: &[Felt]| decode_outputs_i64_only(stack, 1),
);
}

#[test]
fn i64_checked_shr() {
let proc_body = r#"
Expand Down
Loading