diff --git a/cranelift/codegen/src/isa/zkasm/inst.isle b/cranelift/codegen/src/isa/zkasm/inst.isle index c11e1bcbccd1..bbd9d26f6f3e 100644 --- a/cranelift/codegen/src/isa/zkasm/inst.isle +++ b/cranelift/codegen/src/isa/zkasm/inst.isle @@ -40,6 +40,12 @@ (rs1 Reg) (rs2 Reg)) + ;;Division via Arith + (DivArith + (rd WritableReg) + (rs1 Reg) + (rs2 Reg)) + ;; An load (Load (rd WritableReg) @@ -327,13 +333,11 @@ (Mulh) (Mulhsu) (Mulhu) - (Div) (DivU) (Rem) (RemU) ;; RV64M Standard Extension (in addition to RV32M) - (Divw) (Divuw) (Remw) (Remuw) @@ -697,9 +701,11 @@ ;; Helper for emitting the `div` instruction. ;; rd ← rs1 ÷ rs2 -(decl rv_div (XReg XReg) XReg) -(rule (rv_div rs1 rs2) - (alu_rrr (AluOPRRR.Div) rs1 rs2)) +(decl zk_div (XReg XReg) XReg) +(rule (zk_div rs1 rs2) + (let ((dst WritableXReg (temp_writable_xreg)) + (_ Unit (emit (MInst.DivArith dst rs1 rs2)))) + dst)) ;; Helper for emitting the `divu` ("Divide Unsigned") instruction. ;; rd ← rs1 ÷ rs2 @@ -724,13 +730,6 @@ ;; RV64M Extension ;; TODO: Enable these instructions only when we have the M extension - -;; Helper for emitting the `divw` ("Divide Word") instruction. -;; rd ← sext32(rs1) ÷ sext32(rs2) -(decl rv_divw (XReg XReg) XReg) -(rule (rv_divw rs1 rs2) - (alu_rrr (AluOPRRR.Divw) rs1 rs2)) - ;; Helper for emitting the `divuw` ("Divide Unsigned Word") instruction. ;; rd ← uext32(rs1) ÷ uext32(rs2) (decl rv_divuw (XReg XReg) XReg) diff --git a/cranelift/codegen/src/isa/zkasm/inst/args.rs b/cranelift/codegen/src/isa/zkasm/inst/args.rs index bf3efdfb0454..056fe1e95515 100644 --- a/cranelift/codegen/src/isa/zkasm/inst/args.rs +++ b/cranelift/codegen/src/isa/zkasm/inst/args.rs @@ -331,11 +331,9 @@ impl AluOPRRR { Self::Mulh => "mulh", Self::Mulhsu => "mulhsu", Self::Mulhu => "mulhu", - Self::Div => "div", Self::DivU => "divu", Self::Rem => "rem", Self::RemU => "remu", - Self::Divw => "divw", Self::Divuw => "divuw", Self::Remw => "remw", Self::Remuw => "remuw", @@ -393,11 +391,9 @@ impl AluOPRRR { AluOPRRR::Mulh => 0b001, AluOPRRR::Mulhsu => 0b010, AluOPRRR::Mulhu => 0b011, - AluOPRRR::Div => 0b100, AluOPRRR::DivU => 0b101, AluOPRRR::Rem => 0b110, AluOPRRR::RemU => 0b111, - AluOPRRR::Divw => 0b100, AluOPRRR::Divuw => 0b101, AluOPRRR::Remw => 0b110, AluOPRRR::Remuw => 0b111, @@ -463,12 +459,11 @@ impl AluOPRRR { AluOPRRR::Mulh | AluOPRRR::Mulhsu | AluOPRRR::Mulhu - | AluOPRRR::Div | AluOPRRR::DivU | AluOPRRR::Rem | AluOPRRR::RemU => 0b0110011, - AluOPRRR::Divw | AluOPRRR::Divuw | AluOPRRR::Remw | AluOPRRR::Remuw => 0b0111011, + AluOPRRR::Divuw | AluOPRRR::Remw | AluOPRRR::Remuw => 0b0111011, AluOPRRR::Adduw => 0b0111011, AluOPRRR::Andn @@ -524,12 +519,10 @@ impl AluOPRRR { AluOPRRR::Mulh => 0b0000001, AluOPRRR::Mulhsu => 0b0000001, AluOPRRR::Mulhu => 0b0000001, - AluOPRRR::Div => 0b0000001, AluOPRRR::DivU => 0b0000001, AluOPRRR::Rem => 0b0000001, AluOPRRR::RemU => 0b0000001, - AluOPRRR::Divw => 0b0000001, AluOPRRR::Divuw => 0b0000001, AluOPRRR::Remw => 0b0000001, AluOPRRR::Remuw => 0b0000001, diff --git a/cranelift/codegen/src/isa/zkasm/inst/emit.rs b/cranelift/codegen/src/isa/zkasm/inst/emit.rs index e61299c188cc..aa83b8b4b949 100644 --- a/cranelift/codegen/src/isa/zkasm/inst/emit.rs +++ b/cranelift/codegen/src/isa/zkasm/inst/emit.rs @@ -3,7 +3,7 @@ use crate::binemit::StackMap; use crate::ir::{self, RelSourceLoc, TrapCode}; use crate::isa::zkasm::inst::*; -use crate::machinst::{AllocationConsumer, Reg, Writable}; +use crate::machinst::{reg, AllocationConsumer, Reg, Writable}; use crate::trace; use cranelift_control::ControlPlane; use cranelift_entity::EntityRef; @@ -481,6 +481,19 @@ impl MachInstEmit for Inst { sink, ); } + &Inst::DivArith { rd, rs1, rs2 } => { + let rs1 = allocs.next(rs1); + let rs2 = allocs.next(rs2); + debug_assert_eq!(rs1, e0()); + debug_assert_eq!(rs2, b0()); + let rd = allocs.next_writable(rd); + // Same as in MulArith about D register + put_string("0 => D\n", sink); + put_string("0 => C\n", sink); + put_string("$${var _divArith = E / B}\n", sink); + put_string("${_divArith} => A\n", sink); + put_string("E:ARITH\n", sink); + } &Inst::AluRRR { alu_op, rd, diff --git a/cranelift/codegen/src/isa/zkasm/inst/mod.rs b/cranelift/codegen/src/isa/zkasm/inst/mod.rs index 95267ba87502..6ec1357eb469 100644 --- a/cranelift/codegen/src/isa/zkasm/inst/mod.rs +++ b/cranelift/codegen/src/isa/zkasm/inst/mod.rs @@ -279,6 +279,15 @@ fn zkasm_get_operands VReg>(inst: &Inst, collector: &mut OperandC collector.reg_clobbers(clobbered); collector.reg_def(rd); } + &Inst::DivArith { rd, rs1, rs2, .. } => { + collector.reg_fixed_use(rs1, e0()); + collector.reg_fixed_use(rs2, b0()); + let mut clobbered = PRegSet::empty(); + clobbered.add(c0().to_real_reg().unwrap().into()); + clobbered.add(d0().to_real_reg().unwrap().into()); + collector.reg_clobbers(clobbered); + collector.reg_fixed_def(rd, a0()); + } &Inst::Load { rd, from, .. } => { if let Some(r) = from.get_allocatable_register() { collector.reg_use(r); @@ -971,6 +980,12 @@ impl Inst { let rd_s = format_reg(rd.to_reg(), allocs); format!("MulArith rd = {}, rs1 = {}, rs2 = {}", rd_s, rs1_s, rs2_s) } + &Inst::DivArith { rd, rs1, rs2 } => { + let rs1_s = format_reg(rs1, allocs); + let rs2_s = format_reg(rs2, allocs); + let rd_s = format_reg(rd.to_reg(), allocs); + format!("DivArith rd = {}, rs1 = {}, rs2 = {}", rd_s, rs1_s, rs2_s) + } Inst::AddImm32 { rd, src1, src2 } => { let rd = format_reg(rd.to_reg(), allocs); format!("{src1} + {src2} => {rd};") diff --git a/cranelift/codegen/src/isa/zkasm/inst/regs.rs b/cranelift/codegen/src/isa/zkasm/inst/regs.rs index a10a5bcbb5ed..9363480313c1 100644 --- a/cranelift/codegen/src/isa/zkasm/inst/regs.rs +++ b/cranelift/codegen/src/isa/zkasm/inst/regs.rs @@ -31,6 +31,10 @@ pub fn d0() -> Reg { x_reg(6) } +pub fn e0() -> Reg { + x_reg(7) +} + #[inline] pub fn writable_a0() -> Writable { Writable::from_reg(a0()) diff --git a/cranelift/codegen/src/isa/zkasm/lower.isle b/cranelift/codegen/src/isa/zkasm/lower.isle index c2e96cab3ff7..3ac6e53f091f 100644 --- a/cranelift/codegen/src/isa/zkasm/lower.isle +++ b/cranelift/codegen/src/isa/zkasm/lower.isle @@ -116,19 +116,8 @@ (_ InstOutput (gen_div_by_zero y2))) (rv_divuw (zext x ty $I64) y2))) -; (rule -1 (lower (has_type (fits_in_32 ty) (sdiv x y))) -; (let -; ((a XReg (sext x ty $I64)) -; (b XReg (sext y ty $I64)) -; (_ InstOutput (gen_div_overflow a b ty)) -; (_ InstOutput (gen_div_by_zero b))) -; (rv_divw a b))) -; -; (rule (lower (has_type $I64 (sdiv x y))) -; (let -; ((_ InstOutput (gen_div_overflow x y $I64)) -; (_ InstOutput (gen_div_by_zero y)) ) -; (rv_div x y))) +(rule (lower (sdiv x y)) + (zk_div x y)) (rule (lower (has_type $I64 (udiv x y))) (let diff --git a/cranelift/filetests/src/test_zkasm.rs b/cranelift/filetests/src/test_zkasm.rs index 38c9b6e4a634..7624d7fb9166 100644 --- a/cranelift/filetests/src/test_zkasm.rs +++ b/cranelift/filetests/src/test_zkasm.rs @@ -203,5 +203,7 @@ mod tests { xor, and, or, + div, + i64_div, } } diff --git a/cranelift/zkasm_data/div.wat b/cranelift/zkasm_data/div.wat new file mode 100644 index 000000000000..4d38ac1c4899 --- /dev/null +++ b/cranelift/zkasm_data/div.wat @@ -0,0 +1,9 @@ +(module + (import "env" "assert_eq" (func $assert_eq (param i32) (param i32))) + (func $main + i32.const 1999999999 + i32.const 64516129 + i32.div_s + i32.const 31 + call $assert_eq) + (start $main)) diff --git a/cranelift/zkasm_data/generated/div.zkasm b/cranelift/zkasm_data/generated/div.zkasm new file mode 100644 index 000000000000..434feb1c1703 --- /dev/null +++ b/cranelift/zkasm_data/generated/div.zkasm @@ -0,0 +1,32 @@ +start: + zkPC + 2 => RR + :JMP(function_1) + :JMP(finalizeExecution) +function_1: + SP + 1 => SP + RR :MSTORE(SP - 1) + SP + 4 => SP + C :MSTORE(SP - 1) + D :MSTORE(SP - 2) + E :MSTORE(SP - 3) + B :MSTORE(SP - 4) + 1999999999 => E + 64516129 => B + 0 => D + 0 => C + $${var _divArith = E / B} + ${_divArith} => A + E:ARITH + 31 => B + B :ASSERT + $ => C :MLOAD(SP - 1) + $ => D :MLOAD(SP - 2) + $ => E :MLOAD(SP - 3) + $ => B :MLOAD(SP - 4) + SP - 4 => SP + $ => RR :MLOAD(SP - 1) + SP - 1 => SP + :JMP(RR) +finalizeExecution: + ${beforeLast()} :JMPN(finalizeExecution) + :JMP(start) \ No newline at end of file diff --git a/cranelift/zkasm_data/generated/i64_div.zkasm b/cranelift/zkasm_data/generated/i64_div.zkasm new file mode 100644 index 000000000000..4a6e68980614 --- /dev/null +++ b/cranelift/zkasm_data/generated/i64_div.zkasm @@ -0,0 +1,44 @@ +start: + zkPC + 2 => RR + :JMP(function_1) + :JMP(finalizeExecution) +function_1: + SP + 1 => SP + RR :MSTORE(SP - 1) + SP + 4 => SP + C :MSTORE(SP - 1) + D :MSTORE(SP - 2) + E :MSTORE(SP - 3) + B :MSTORE(SP - 4) + 214748364 => A + A => E + 107374183 => A + 2 => B + 0 => D + 0 => C + $${var _mulArith = A * B} + ${_mulArith} => B :ARITH + E => A + 0 => D + 0 => C + $${var _mulArith = A * B} + ${_mulArith} => E :ARITH + 214748364 => B + 0 => D + 0 => C + $${var _divArith = E / B} + ${_divArith} => A + E:ARITH + 214748366 => B + B :ASSERT + $ => C :MLOAD(SP - 1) + $ => D :MLOAD(SP - 2) + $ => E :MLOAD(SP - 3) + $ => B :MLOAD(SP - 4) + SP - 4 => SP + $ => RR :MLOAD(SP - 1) + SP - 1 => SP + :JMP(RR) +finalizeExecution: + ${beforeLast()} :JMPN(finalizeExecution) + :JMP(start) \ No newline at end of file diff --git a/cranelift/zkasm_data/i64_div.wat b/cranelift/zkasm_data/i64_div.wat new file mode 100644 index 000000000000..3b88d9b60c09 --- /dev/null +++ b/cranelift/zkasm_data/i64_div.wat @@ -0,0 +1,13 @@ +(module + (import "env" "assert_eq" (func $assert_eq (param i64) (param i64))) + (func $main + i64.const 214748364 + i64.const 107374183 + i64.const 2 + i64.mul + i64.mul + i64.const 214748364 + i64.div_s + i64.const 214748366 + call $assert_eq) + (start $main))