Signed division via Arith (#54)

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)

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,

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,

cranelift/codegen/src/isa/zkasm/inst/mod.rs

@@ -279,6 +279,15 @@ fn zkasm_get_operands<F: Fn(VReg) -> 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};")

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<Reg> {
     Writable::from_reg(a0())

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

cranelift/filetests/src/test_zkasm.rs

@@ -203,5 +203,7 @@ mod tests {
         xor,
         and,
         or,
+        div,
+        i64_div,
     }
 }

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))

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)

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)

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))