Skip to content

Commit f710af5

Browse files
MCJOHN974MCJOHN974
authored
Merge pull request bytecodealliance#126 from near/viktar/remu
zkasm: remu
2 parents ab7d7bf + 0c5b1bc commit f710af5

35 files changed

+1294
-39
lines changed

‎cranelift/codegen/src/isa/zkasm/inst.isle

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,16 @@
7474
(rs1 Reg)
7575
(rs2 Reg))
7676

77+
(URemArith
78+
(rd WritableReg)
79+
(rs1 Reg)
80+
(rs2 Reg))
81+
82+
(URemArith32
83+
(rd WritableReg)
84+
(rs1 Reg)
85+
(rs2 Reg))
86+
7787
(Ineg
7888
(rd WritableReg)
7989
(rs1 Reg))
@@ -735,6 +745,12 @@
735745
(_ Unit (emit (MInst.RemArith32 dst rs1 rs2))))
736746
dst))
737747

748+
(decl zk_remu_32 (XReg XReg) XReg)
749+
(rule (zk_remu_32 rs1 rs2)
750+
(let ((dst WritableXReg (temp_writable_xreg))
751+
(_ Unit (emit (MInst.URemArith32 dst rs1 rs2))))
752+
dst))
753+
738754
;; Helper for emitting the `mulh` ("Multiply High Signed Signed") instruction.
739755
;; rd ← (sext(rs1) × sext(rs2)) » xlen
740756
(decl rv_mulh (XReg XReg) XReg)
@@ -763,6 +779,12 @@
763779
(_ Unit (emit (MInst.RemArith dst rs1 rs2))))
764780
dst))
765781

782+
(decl zk_remu (XReg XReg) XReg)
783+
(rule (zk_remu rs1 rs2)
784+
(let ((dst WritableXReg (temp_writable_xreg))
785+
(_ Unit (emit (MInst.URemArith dst rs1 rs2))))
786+
dst))
787+
766788
;; Helper for emitting the `divu` ("Divide Unsigned") instruction.
767789
;; rd ← rs1 ÷ rs2
768790
(decl rv_divu (XReg XReg) XReg)

‎cranelift/codegen/src/isa/zkasm/inst/emit.rs

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -736,6 +736,61 @@ impl MachInstEmit for Inst {
736736
put_string("${E % B} => C\n", sink);
737737
put_string("E:ARITH\n", sink);
738738
}
739+
&Inst::URemArith32 { rd, rs1, rs2 } => {
740+
let rs1 = allocs.next(rs1);
741+
let rs2 = allocs.next(rs2);
742+
debug_assert_eq!(rs1, a0());
743+
debug_assert_eq!(rs2, e0());
744+
let rd = allocs.next_writable(rd);
745+
746+
// A % B => E
747+
748+
put_string("A :MSTORE(SP)\n", sink); // SP contains op1
749+
750+
// op2 / 2 ** 32 => A
751+
put_string("0 => D\n", sink);
752+
put_string("0 => C\n", sink);
753+
put_string("4294967296n => B\n", sink);
754+
put_string("${E / B} => A\n", sink);
755+
put_string("E:ARITH\n", sink);
756+
757+
put_string("A :MSTORE(SP + 1)\n", sink); // SP + 1 contains op2 / 2 ** 32
758+
759+
// op1 => E
760+
put_string("$ => E :MLOAD(SP)\n", sink);
761+
762+
// op1 / 2 ** 32 => A
763+
put_string("${E / B} => A\n", sink);
764+
put_string("E:ARITH\n", sink);
765+
766+
put_string("A => E\n", sink);
767+
put_string("$ => B :MLOAD(SP + 1)\n", sink);
768+
769+
// now E = op1 / 2**32, B = op2 / 2**32
770+
put_string("${E / B} => A\n", sink);
771+
put_string("${E % B} => C\n", sink);
772+
put_string("E:ARITH\n", sink);
773+
774+
// now C = res / 2 ** 32
775+
put_string("C => A\n", sink);
776+
put_string("4294967296n => B\n", sink);
777+
778+
put_string("0 => D\n", sink);
779+
put_string("0 => C\n", sink);
780+
put_string("${A * B} => E :ARITH\n", sink);
781+
// now E = res
782+
}
783+
&Inst::URemArith { rd, rs1, rs2 } => {
784+
let rs1 = allocs.next(rs1);
785+
let rs2 = allocs.next(rs2);
786+
debug_assert_eq!(rs1, e0());
787+
debug_assert_eq!(rs2, b0());
788+
let rd = allocs.next_writable(rd);
789+
put_string("0 => D\n", sink);
790+
put_string("${E / B} => A\n", sink);
791+
put_string("${E % B} => C\n", sink);
792+
put_string("E:ARITH\n", sink);
793+
}
739794
&Inst::AluRRR {
740795
alu_op,
741796
rd,

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

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -346,6 +346,26 @@ fn zkasm_get_operands<F: Fn(VReg) -> VReg>(inst: &Inst, collector: &mut OperandC
346346
collector.reg_clobbers(clobbered);
347347
collector.reg_fixed_def(rd, a0());
348348
}
349+
&Inst::URemArith { rd, rs1, rs2, .. } => {
350+
collector.reg_fixed_use(rs1, e0());
351+
collector.reg_fixed_use(rs2, b0());
352+
let mut clobbered = PRegSet::empty();
353+
clobbered.add(a0().to_real_reg().unwrap().into());
354+
clobbered.add(d0().to_real_reg().unwrap().into());
355+
collector.reg_clobbers(clobbered);
356+
collector.reg_fixed_def(rd, c0());
357+
}
358+
&Inst::URemArith32 { rd, rs1, rs2, .. } => {
359+
collector.reg_fixed_use(rs1, a0());
360+
collector.reg_fixed_use(rs2, e0());
361+
let mut clobbered = PRegSet::empty();
362+
clobbered.add(a0().to_real_reg().unwrap().into());
363+
clobbered.add(b0().to_real_reg().unwrap().into());
364+
clobbered.add(c0().to_real_reg().unwrap().into());
365+
clobbered.add(d0().to_real_reg().unwrap().into());
366+
collector.reg_clobbers(clobbered);
367+
collector.reg_fixed_def(rd, e0());
368+
}
349369
&Inst::RemArith { rd, rs1, rs2, .. } => {
350370
collector.reg_fixed_use(rs1, e0());
351371
collector.reg_fixed_use(rs2, b0());
@@ -1089,6 +1109,21 @@ impl Inst {
10891109
let rd_s = format_reg(rd.to_reg(), allocs);
10901110
format!("RemArith32 rd = {}, rs1 = {}, rs2 = {}", rd_s, rs1_s, rs2_s)
10911111
}
1112+
&Inst::URemArith { rd, rs1, rs2 } => {
1113+
let rs1_s = format_reg(rs1, allocs);
1114+
let rs2_s = format_reg(rs2, allocs);
1115+
let rd_s = format_reg(rd.to_reg(), allocs);
1116+
format!("URemArith rd = {}, rs1 = {}, rs2 = {}", rd_s, rs1_s, rs2_s)
1117+
}
1118+
&Inst::URemArith32 { rd, rs1, rs2 } => {
1119+
let rs1_s = format_reg(rs1, allocs);
1120+
let rs2_s = format_reg(rs2, allocs);
1121+
let rd_s = format_reg(rd.to_reg(), allocs);
1122+
format!(
1123+
"URemArith32 rd = {}, rs1 = {}, rs2 = {}",
1124+
rd_s, rs1_s, rs2_s
1125+
)
1126+
}
10921127
Inst::AddImm32 { rd, src1, src2 } => {
10931128
let rd = format_reg(rd.to_reg(), allocs);
10941129
format!("{src1} + {src2} => {rd};")

‎cranelift/codegen/src/isa/zkasm/lower.isle

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -123,16 +123,11 @@
123123
(rule (lower (has_type $I32 (srem x y)))
124124
(zk_rem_32 x y))
125125

126-
(rule (lower (has_type $I32 (urem x y)))
127-
(let
128-
((y2 XReg (zext y $I32 $I64))
129-
(_ InstOutput (gen_div_by_zero y2)))
130-
(rv_remuw x y2)))
131-
132126
(rule (lower (has_type $I64 (urem x y)))
133-
(let
134-
((_ InstOutput (gen_div_by_zero y)))
135-
(rv_remu x y)))
127+
(zk_remu x y))
128+
129+
(rule (lower (has_type $I32 (urem x y)))
130+
(zk_remu_32 x y))
136131

137132
;;;; Rules for `and` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
138133
(rule 0 (lower (has_type (ty_int ty) (band x y)))

‎cranelift/zkasm_data/spectest/i32/generated/rem_u_1.zkasm

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
start:
2+
zkPC + 2 => RR
3+
:JMP(function_1)
4+
:JMP(finalizeExecution)
5+
function_1:
6+
SP + 1 => SP
7+
RR :MSTORE(SP - 1)
8+
SP + 4 => SP
9+
C :MSTORE(SP - 1)
10+
D :MSTORE(SP - 2)
11+
E :MSTORE(SP - 3)
12+
B :MSTORE(SP - 4)
13+
4294967296n => A
14+
4294967296n => E
15+
A :MSTORE(SP)
16+
0 => D
17+
0 => C
18+
4294967296n => B
19+
${E / B} => A
20+
E:ARITH
21+
A :MSTORE(SP + 1)
22+
$ => E :MLOAD(SP)
23+
${E / B} => A
24+
E:ARITH
25+
A => E
26+
$ => B :MLOAD(SP + 1)
27+
${E / B} => A
28+
${E % B} => C
29+
E:ARITH
30+
C => A
31+
4294967296n => B
32+
0 => D
33+
0 => C
34+
${A * B} => E :ARITH
35+
E => A
36+
0n => B
37+
B :ASSERT
38+
$ => C :MLOAD(SP - 1)
39+
$ => D :MLOAD(SP - 2)
40+
$ => E :MLOAD(SP - 3)
41+
$ => B :MLOAD(SP - 4)
42+
SP - 4 => SP
43+
$ => RR :MLOAD(SP - 1)
44+
SP - 1 => SP
45+
:JMP(RR)
46+
finalizeExecution:
47+
${beforeLast()} :JMPN(finalizeExecution)
48+
:JMP(start)
49+
INCLUDE "helpers/2-exp.zkasm"

‎cranelift/zkasm_data/spectest/i32/generated/rem_u_10.zkasm

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
start:
2+
zkPC + 2 => RR
3+
:JMP(function_1)
4+
:JMP(finalizeExecution)
5+
function_1:
6+
SP + 1 => SP
7+
RR :MSTORE(SP - 1)
8+
SP + 4 => SP
9+
C :MSTORE(SP - 1)
10+
D :MSTORE(SP - 2)
11+
E :MSTORE(SP - 3)
12+
B :MSTORE(SP - 4)
13+
21474836480n => A
14+
18446744065119617024n => E
15+
A :MSTORE(SP)
16+
0 => D
17+
0 => C
18+
4294967296n => B
19+
${E / B} => A
20+
E:ARITH
21+
A :MSTORE(SP + 1)
22+
$ => E :MLOAD(SP)
23+
${E / B} => A
24+
E:ARITH
25+
A => E
26+
$ => B :MLOAD(SP + 1)
27+
${E / B} => A
28+
${E % B} => C
29+
E:ARITH
30+
C => A
31+
4294967296n => B
32+
0 => D
33+
0 => C
34+
${A * B} => E :ARITH
35+
E => A
36+
21474836480n => B
37+
B :ASSERT
38+
$ => C :MLOAD(SP - 1)
39+
$ => D :MLOAD(SP - 2)
40+
$ => E :MLOAD(SP - 3)
41+
$ => B :MLOAD(SP - 4)
42+
SP - 4 => SP
43+
$ => RR :MLOAD(SP - 1)
44+
SP - 1 => SP
45+
:JMP(RR)
46+
finalizeExecution:
47+
${beforeLast()} :JMPN(finalizeExecution)
48+
:JMP(start)
49+
INCLUDE "helpers/2-exp.zkasm"

‎cranelift/zkasm_data/spectest/i32/generated/rem_u_11.zkasm

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
start:
2+
zkPC + 2 => RR
3+
:JMP(function_1)
4+
:JMP(finalizeExecution)
5+
function_1:
6+
SP + 1 => SP
7+
RR :MSTORE(SP - 1)
8+
SP + 4 => SP
9+
C :MSTORE(SP - 1)
10+
D :MSTORE(SP - 2)
11+
E :MSTORE(SP - 3)
12+
B :MSTORE(SP - 4)
13+
18446744052234715136n => A
14+
18446744065119617024n => E
15+
A :MSTORE(SP)
16+
0 => D
17+
0 => C
18+
4294967296n => B
19+
${E / B} => A
20+
E:ARITH
21+
A :MSTORE(SP + 1)
22+
$ => E :MLOAD(SP)
23+
${E / B} => A
24+
E:ARITH
25+
A => E
26+
$ => B :MLOAD(SP + 1)
27+
${E / B} => A
28+
${E % B} => C
29+
E:ARITH
30+
C => A
31+
4294967296n => B
32+
0 => D
33+
0 => C
34+
${A * B} => E :ARITH
35+
E => A
36+
18446744052234715136n => B
37+
B :ASSERT
38+
$ => C :MLOAD(SP - 1)
39+
$ => D :MLOAD(SP - 2)
40+
$ => E :MLOAD(SP - 3)
41+
$ => B :MLOAD(SP - 4)
42+
SP - 4 => SP
43+
$ => RR :MLOAD(SP - 1)
44+
SP - 1 => SP
45+
:JMP(RR)
46+
finalizeExecution:
47+
${beforeLast()} :JMPN(finalizeExecution)
48+
:JMP(start)
49+
INCLUDE "helpers/2-exp.zkasm"

‎cranelift/zkasm_data/spectest/i32/generated/rem_u_12.zkasm

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
start:
2+
zkPC + 2 => RR
3+
:JMP(function_1)
4+
:JMP(finalizeExecution)
5+
function_1:
6+
SP + 1 => SP
7+
RR :MSTORE(SP - 1)
8+
SP + 4 => SP
9+
C :MSTORE(SP - 1)
10+
D :MSTORE(SP - 2)
11+
E :MSTORE(SP - 3)
12+
B :MSTORE(SP - 4)
13+
30064771072n => A
14+
12884901888n => E
15+
A :MSTORE(SP)
16+
0 => D
17+
0 => C
18+
4294967296n => B
19+
${E / B} => A
20+
E:ARITH
21+
A :MSTORE(SP + 1)
22+
$ => E :MLOAD(SP)
23+
${E / B} => A
24+
E:ARITH
25+
A => E
26+
$ => B :MLOAD(SP + 1)
27+
${E / B} => A
28+
${E % B} => C
29+
E:ARITH
30+
C => A
31+
4294967296n => B
32+
0 => D
33+
0 => C
34+
${A * B} => E :ARITH
35+
E => A
36+
4294967296n => B
37+
B :ASSERT
38+
$ => C :MLOAD(SP - 1)
39+
$ => D :MLOAD(SP - 2)
40+
$ => E :MLOAD(SP - 3)
41+
$ => B :MLOAD(SP - 4)
42+
SP - 4 => SP
43+
$ => RR :MLOAD(SP - 1)
44+
SP - 1 => SP
45+
:JMP(RR)
46+
finalizeExecution:
47+
${beforeLast()} :JMPN(finalizeExecution)
48+
:JMP(start)
49+
INCLUDE "helpers/2-exp.zkasm"

0 commit comments

Comments
 (0)