diff --git a/Test/Passes/InstructionSelection/RISCV64/divpow2.mlir b/Test/Passes/InstructionSelection/RISCV64/divpow2.mlir new file mode 100644 index 000000000..d9ce0f6e0 --- /dev/null +++ b/Test/Passes/InstructionSelection/RISCV64/divpow2.mlir @@ -0,0 +1,122 @@ +// RUN: veir-opt %s -p=isel-sdag-riscv64 | filecheck %s + +"builtin.module"() ({ + // llvm.udiv x, 8 -> riscv.srli x, 3 + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = 8 : i64}> : () -> i64 + %r = "llvm.udiv"(%a, %c) : (i64, i64) -> i64 + // CHECK: %{{.*}} = "builtin.unrealized_conversion_cast"(%{{.*}}) : (i64) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.srli"(%{{.*}}) <{"value" = 3 : i64}> : (!riscv.reg) -> !riscv.reg + "func.return"(%r) : (i64) -> () + }) : () -> () + + // llvm.udiv x, 8 (i32) -> riscv.srliw x, 3 + "func.func"() <{function_type = (i32) -> i32}> ({ + ^bb(%a: i32): + %c = "llvm.mlir.constant"() <{value = 8 : i32}> : () -> i32 + %r = "llvm.udiv"(%a, %c) : (i32, i32) -> i32 + // CHECK: %{{.*}} = "riscv.srliw"(%{{.*}}) <{"value" = 3 : i64}> : (!riscv.reg) -> !riscv.reg + "func.return"(%r) : (i32) -> () + }) : () -> () + + // udiv by 2^63: its bit pattern (0x8000...0) is decoded as the negative decimal + // -9223372036854775808, but is still a valid *unsigned* power-of-two divisor. + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = -9223372036854775808 : i64}> : () -> i64 + %r = "llvm.udiv"(%a, %c) : (i64, i64) -> i64 + // CHECK: %{{.*}} = "riscv.srli"(%{{.*}}) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg + "func.return"(%r) : (i64) -> () + }) : () -> () + + // Regression: 0xC000000000000000 (decimal -4611686018427387904) has *two* bits + // set, so it is not a power of two -- even though its magnitude as a signed + // `Int` (2^62) would incorrectly look like one under a naive sign/magnitude + // check that didn't first reduce it mod 2^64. Must stay unselected. + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = -4611686018427387904 : i64}> : () -> i64 + %r = "llvm.udiv"(%a, %c) : (i64, i64) -> i64 + // CHECK: %{{.*}} = "llvm.udiv"(%{{.*}}, %{{.*}}) : (i64, i64) -> i64 + "func.return"(%r) : (i64) -> () + }) : () -> () + + // Not a power of two: left unselected here (the generic isel-riscv64 pass + // picks it up as a plain `riscv.divu`). + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = 6 : i64}> : () -> i64 + %r = "llvm.udiv"(%a, %c) : (i64, i64) -> i64 + // CHECK: %{{.*}} = "llvm.udiv"(%{{.*}}, %{{.*}}) : (i64, i64) -> i64 + "func.return"(%r) : (i64) -> () + }) : () -> () + + // llvm.sdiv exact x, 8 -> riscv.srai x, 3 (no negation needed) + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = 8 : i64}> : () -> i64 + %r = "llvm.sdiv"(%a, %c) <{exact}> : (i64, i64) -> i64 + // CHECK: %{{.*}} = "riscv.srai"(%{{.*}}) <{"value" = 3 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "builtin.unrealized_conversion_cast"(%{{.*}}) : (!riscv.reg) -> i64 + "func.return"(%r) : (i64) -> () + }) : () -> () + + // llvm.sdiv exact x, -8 -> riscv.srai x, 3, then negate via `sub 0, _`. + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = -8 : i64}> : () -> i64 + %r = "llvm.sdiv"(%a, %c) <{exact}> : (i64, i64) -> i64 + // CHECK: %{{.*}} = "riscv.srai"(%{{.*}}) <{"value" = 3 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.li"() <{"value" = 0 : i64}> : () -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.sub"(%{{.*}}, %{{.*}}) : (!riscv.reg, !riscv.reg) -> !riscv.reg + "func.return"(%r) : (i64) -> () + }) : () -> () + + // i32 exact variant. + "func.func"() <{function_type = (i32) -> i32}> ({ + ^bb(%a: i32): + %c = "llvm.mlir.constant"() <{value = 8 : i32}> : () -> i32 + %r = "llvm.sdiv"(%a, %c) <{exact}> : (i32, i32) -> i32 + // CHECK: %{{.*}} = "riscv.sraiw"(%{{.*}}) <{"value" = 3 : i64}> : (!riscv.reg) -> !riscv.reg + "func.return"(%r) : (i32) -> () + }) : () -> () + + // General (non-exact) llvm.sdiv x, 8 -> the biased 4-instruction sequence. + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = 8 : i64}> : () -> i64 + %r = "llvm.sdiv"(%a, %c) : (i64, i64) -> i64 + // CHECK: %{{.*}} = "riscv.srai"(%{{.*}}) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.srli"(%{{.*}}) <{"value" = 61 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.add"(%{{.*}}, %{{.*}}) : (!riscv.reg, !riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.srai"(%{{.*}}) <{"value" = 3 : i64}> : (!riscv.reg) -> !riscv.reg + "func.return"(%r) : (i64) -> () + }) : () -> () + + // General llvm.sdiv x, -8 -> the biased sequence plus a final negation. + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = -8 : i64}> : () -> i64 + %r = "llvm.sdiv"(%a, %c) : (i64, i64) -> i64 + // CHECK: %{{.*}} = "riscv.srai"(%{{.*}}) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.srli"(%{{.*}}) <{"value" = 61 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.add"(%{{.*}}, %{{.*}}) : (!riscv.reg, !riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.srai"(%{{.*}}) <{"value" = 3 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.li"() <{"value" = 0 : i64}> : () -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.sub"(%{{.*}}, %{{.*}}) : (!riscv.reg, !riscv.reg) -> !riscv.reg + "func.return"(%r) : (i64) -> () + }) : () -> () + + // i32 general variant. + "func.func"() <{function_type = (i32) -> i32}> ({ + ^bb(%a: i32): + %c = "llvm.mlir.constant"() <{value = 8 : i32}> : () -> i32 + %r = "llvm.sdiv"(%a, %c) : (i32, i32) -> i32 + // CHECK: %{{.*}} = "riscv.sraiw"(%{{.*}}) <{"value" = 31 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.srliw"(%{{.*}}) <{"value" = 29 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.addw"(%{{.*}}, %{{.*}}) : (!riscv.reg, !riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.sraiw"(%{{.*}}) <{"value" = 3 : i64}> : (!riscv.reg) -> !riscv.reg + "func.return"(%r) : (i32) -> () + }) : () -> () +}) : () -> () diff --git a/Test/Passes/InstructionSelection/RISCV64/fastntt.mlir b/Test/Passes/InstructionSelection/RISCV64/fastntt.mlir index 4bce5d882..e2080e55c 100644 --- a/Test/Passes/InstructionSelection/RISCV64/fastntt.mlir +++ b/Test/Passes/InstructionSelection/RISCV64/fastntt.mlir @@ -1,4 +1,4 @@ -// RUN: veir-opt %s -p=isel-br-riscv64,isel-riscv64,reconcile-cast,riscv-combine | filecheck %s +// RUN: veir-opt %s -p=isel-sdag-riscv64,isel-br-riscv64,isel-riscv64,reconcile-cast,riscv-combine,dce | filecheck %s "builtin.module"() ({ ^4(): @@ -118,146 +118,160 @@ // CHECK-NEXT: "llvm.module_flags"() {{.*}} : () -> () // CHECK-NEXT: "llvm.func"() <{{{.*}}"sym_name" = "fastNTT"{{.*}}}> ({ // CHECK-NEXT: ^[[bb7:[0-9]+]](%[[varg7_0:[a-zA-Z0-9_]+]] : !llvm.ptr, %[[varg7_1:[a-zA-Z0-9_]+]] : i64, %[[varg7_2:[a-zA-Z0-9_]+]] : i64, %[[varg7_3:[a-zA-Z0-9_]+]] : !llvm.ptr, %[[varg7_4:[a-zA-Z0-9_]+]] : i64, %[[varg7_5:[a-zA-Z0-9_]+]] : i64): -// CHECK-NEXT: %[[v374:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg -// CHECK-NEXT: %[[v370:[0-9]+]] = "riscv.li"() <{"value" = 2 : i64}> : () -> !riscv.reg -// CHECK-NEXT: %[[v368:[0-9]+]] = "riscv.li"() <{"value" = 1 : i64}> : () -> !riscv.reg -// CHECK-NEXT: %[[v363:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_4]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v375:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg -// CHECK-NEXT: %[[v366:[0-9]+]] = "riscv.sltu"(%[[v375]], %[[v363]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v367:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v366]]) : (!riscv.reg) -> i1 -// CHECK-NEXT: %[[v114:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v367]]) : (i1) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.bnez"(%[[v114]]) [^[[bb12:[0-9]+]], ^[[bb13:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () +// CHECK-NEXT: %[[v382:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg +// CHECK-NEXT: %[[v378:[0-9]+]] = "riscv.li"() <{"value" = 2 : i64}> : () -> !riscv.reg +// CHECK-NEXT: %[[v376:[0-9]+]] = "riscv.li"() <{"value" = 1 : i64}> : () -> !riscv.reg +// CHECK-NEXT: %[[v371:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_4]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v383:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg +// CHECK-NEXT: %[[v374:[0-9]+]] = "riscv.sltu"(%[[v383]], %[[v371]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v375:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v374]]) : (!riscv.reg) -> i1 +// CHECK-NEXT: %[[v174:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v375]]) : (i1) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.bnez"(%[[v174]]) [^[[bb12:[0-9]+]], ^[[bb13:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb12]](): -// CHECK-NEXT: %[[v118:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_1]]) : (i64) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v118]]) [^[[bb15:[0-9]+]]] : (!riscv.reg) -> () +// CHECK-NEXT: %[[v178:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_1]]) : (i64) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v178]]) [^[[bb15:[0-9]+]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb13]](): -// CHECK-NEXT: "riscv_cf.branch"(%[[v370]]) [^[[bb15]]] : (!riscv.reg) -> () +// CHECK-NEXT: "riscv_cf.branch"(%[[v378]]) [^[[bb15]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb15]](%[[varg15_0:[a-zA-Z0-9_]+]] : !riscv.reg): -// CHECK-NEXT: %[[v358:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_4]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v376:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg -// CHECK-NEXT: %[[v361:[0-9]+]] = "riscv.sltu"(%[[v376]], %[[v358]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v362:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v361]]) : (!riscv.reg) -> i1 -// CHECK-NEXT: %[[v122:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v362]]) : (i1) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.bnez"(%[[v122]]) [^[[bb19:[0-9]+]], ^[[bb20:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () +// CHECK-NEXT: %[[v366:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_4]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v384:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg +// CHECK-NEXT: %[[v369:[0-9]+]] = "riscv.sltu"(%[[v384]], %[[v366]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v370:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v369]]) : (!riscv.reg) -> i1 +// CHECK-NEXT: %[[v182:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v370]]) : (i1) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.bnez"(%[[v182]]) [^[[bb19:[0-9]+]], ^[[bb20:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb19]](): -// CHECK-NEXT: "riscv_cf.branch"(%[[v368]]) [^[[bb22:[0-9]+]]] : (!riscv.reg) -> () +// CHECK-NEXT: "riscv_cf.branch"(%[[v376]]) [^[[bb22:[0-9]+]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb20]](): -// CHECK-NEXT: %[[v354:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_5]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v356:[0-9]+]] = "riscv.div"(%[[v354]], %[[v370]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v356]]) [^[[bb22]]] : (!riscv.reg) -> () +// CHECK-NEXT: %[[v168:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_5]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v387:[0-9]+]] = "riscv.srli"(%[[v168]]) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v171:[0-9]+]] = "riscv.add"(%[[v168]], %[[v387]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v172:[0-9]+]] = "riscv.srai"(%[[v171]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v172]]) [^[[bb22]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb22]](%[[varg22_0:[a-zA-Z0-9_]+]] : !riscv.reg): -// CHECK-NEXT: %[[v350:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_1]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v352:[0-9]+]] = "riscv.div"(%[[v350]], %[[v370]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[varg22_0]], %[[v352]], %[[v374]], %[[varg15_0]]) [^[[bb27:[0-9]+]]] : (!riscv.reg, !riscv.reg, !riscv.reg, !riscv.reg) -> () +// CHECK-NEXT: %[[v162:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_1]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v388:[0-9]+]] = "riscv.srli"(%[[v162]]) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v165:[0-9]+]] = "riscv.add"(%[[v162]], %[[v388]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v166:[0-9]+]] = "riscv.srai"(%[[v165]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[varg22_0]], %[[v166]], %[[v382]], %[[varg15_0]]) [^[[bb27:[0-9]+]]] : (!riscv.reg, !riscv.reg, !riscv.reg, !riscv.reg) -> () // CHECK-NEXT: ^[[bb27]](%[[varg27_0:[a-zA-Z0-9_]+]] : !riscv.reg, %[[varg27_1:[a-zA-Z0-9_]+]] : !riscv.reg, %[[varg27_2:[a-zA-Z0-9_]+]] : !riscv.reg, %[[varg27_3:[a-zA-Z0-9_]+]] : !riscv.reg): -// CHECK-NEXT: %[[v150:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_1]]) : (i64) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v374]], %[[v150]]) [^[[bb29:[0-9]+]]] : (!riscv.reg, !riscv.reg) -> () +// CHECK-NEXT: %[[v210:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_1]]) : (i64) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v382]], %[[v210]]) [^[[bb29:[0-9]+]]] : (!riscv.reg, !riscv.reg) -> () // CHECK-NEXT: ^[[bb29]](%[[varg29_0:[a-zA-Z0-9_]+]] : !riscv.reg, %[[varg29_1:[a-zA-Z0-9_]+]] : !riscv.reg): -// CHECK-NEXT: %[[v348:[0-9]+]] = "riscv.slt"(%[[v368]], %[[varg29_1]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v349:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v348]]) : (!riscv.reg) -> i1 -// CHECK-NEXT: %[[v159:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v349]]) : (i1) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.bnez"(%[[v159]]) [^[[bb32:[0-9]+]], ^[[bb33:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () +// CHECK-NEXT: %[[v364:[0-9]+]] = "riscv.slt"(%[[v376]], %[[varg29_1]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v365:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v364]]) : (!riscv.reg) -> i1 +// CHECK-NEXT: %[[v219:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v365]]) : (i1) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.bnez"(%[[v219]]) [^[[bb32:[0-9]+]], ^[[bb33:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb32]](): -// CHECK-NEXT: %[[v344:[0-9]+]] = "riscv.sra"(%[[varg29_1]], %[[v368]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v340:[0-9]+]] = "riscv.add"(%[[v368]], %[[varg29_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v340]], %[[v344]]) [^[[bb29]]] : (!riscv.reg, !riscv.reg) -> () +// CHECK-NEXT: %[[v160:[0-9]+]] = "riscv.srai"(%[[varg29_1]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v157:[0-9]+]] = "riscv.addi"(%[[varg29_0]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v157]], %[[v160]]) [^[[bb29]]] : (!riscv.reg, !riscv.reg) -> () // CHECK-NEXT: ^[[bb33]](): -// CHECK-NEXT: %[[v336:[0-9]+]] = "riscv.slt"(%[[varg27_2]], %[[varg29_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v337:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v336]]) : (!riscv.reg) -> i1 -// CHECK-NEXT: %[[v168:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v337]]) : (i1) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.bnez"(%[[v168]]) [^[[bb39:[0-9]+]], ^[[bb40:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () +// CHECK-NEXT: %[[v360:[0-9]+]] = "riscv.slt"(%[[varg27_2]], %[[varg29_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v361:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v360]]) : (!riscv.reg) -> i1 +// CHECK-NEXT: %[[v228:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v361]]) : (i1) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.bnez"(%[[v228]]) [^[[bb39:[0-9]+]], ^[[bb40:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb39]](): -// CHECK-NEXT: "riscv_cf.branch"(%[[v374]]) [^[[bb42:[0-9]+]]] : (!riscv.reg) -> () +// CHECK-NEXT: "riscv_cf.branch"(%[[v382]]) [^[[bb42:[0-9]+]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb42]](%[[varg42_0:[a-zA-Z0-9_]+]] : !riscv.reg): -// CHECK-NEXT: %[[v330:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_1]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v332:[0-9]+]] = "riscv.div"(%[[v330]], %[[varg27_3]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v328:[0-9]+]] = "riscv.slt"(%[[varg42_0]], %[[v332]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v329:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v328]]) : (!riscv.reg) -> i1 -// CHECK-NEXT: %[[v176:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v329]]) : (i1) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.bnez"(%[[v176]]) [^[[bb46:[0-9]+]], ^[[bb47:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () +// CHECK-NEXT: %[[v354:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_1]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v356:[0-9]+]] = "riscv.div"(%[[v354]], %[[varg27_3]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v352:[0-9]+]] = "riscv.slt"(%[[varg42_0]], %[[v356]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v353:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v352]]) : (!riscv.reg) -> i1 +// CHECK-NEXT: %[[v236:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v353]]) : (i1) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.bnez"(%[[v236]]) [^[[bb46:[0-9]+]], ^[[bb47:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb46]](): -// CHECK-NEXT: "riscv_cf.branch"(%[[v374]]) [^[[bb49:[0-9]+]]] : (!riscv.reg) -> () +// CHECK-NEXT: "riscv_cf.branch"(%[[v382]]) [^[[bb49:[0-9]+]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb49]](%[[varg49_0:[a-zA-Z0-9_]+]] : !riscv.reg): -// CHECK-NEXT: %[[v324:[0-9]+]] = "riscv.div"(%[[varg27_3]], %[[v370]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v320:[0-9]+]] = "riscv.slt"(%[[varg49_0]], %[[v324]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v321:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v320]]) : (!riscv.reg) -> i1 -// CHECK-NEXT: %[[v183:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v321]]) : (i1) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.bnez"(%[[v183]]) [^[[bb53:[0-9]+]], ^[[bb54:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () +// CHECK-NEXT: %[[v389:[0-9]+]] = "riscv.srli"(%[[varg27_3]]) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v153:[0-9]+]] = "riscv.add"(%[[varg27_3]], %[[v389]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v154:[0-9]+]] = "riscv.srai"(%[[v153]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v348:[0-9]+]] = "riscv.slt"(%[[varg49_0]], %[[v154]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v349:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v348]]) : (!riscv.reg) -> i1 +// CHECK-NEXT: %[[v243:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v349]]) : (i1) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.bnez"(%[[v243]]) [^[[bb53:[0-9]+]], ^[[bb54:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb53]](): -// CHECK-NEXT: %[[v316:[0-9]+]] = "riscv.mul"(%[[varg27_3]], %[[varg42_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v312:[0-9]+]] = "riscv.add"(%[[varg49_0]], %[[v316]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v306:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_0]]) : (!llvm.ptr) -> !riscv.reg -// CHECK-NEXT: %[[v308:[0-9]+]] = "riscv.sh3add"(%[[v312]], %[[v306]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v304:[0-9]+]] = "riscv.ld"(%[[v308]]) <{"value" = 0 : i64}> : (!riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v301:[0-9]+]] = "riscv.div"(%[[varg27_3]], %[[v370]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v297:[0-9]+]] = "riscv.add"(%[[v301]], %[[v312]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v291:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_0]]) : (!llvm.ptr) -> !riscv.reg -// CHECK-NEXT: %[[v293:[0-9]+]] = "riscv.sh3add"(%[[v297]], %[[v291]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v289:[0-9]+]] = "riscv.ld"(%[[v293]]) <{"value" = 0 : i64}> : (!riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v286:[0-9]+]] = "riscv.mul"(%[[varg49_0]], %[[v370]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v282:[0-9]+]] = "riscv.add"(%[[v368]], %[[v286]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v278:[0-9]+]] = "riscv.mul"(%[[varg27_1]], %[[v282]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v272:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_3]]) : (!llvm.ptr) -> !riscv.reg -// CHECK-NEXT: %[[v274:[0-9]+]] = "riscv.sh3add"(%[[v278]], %[[v272]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v270:[0-9]+]] = "riscv.ld"(%[[v274]]) <{"value" = 0 : i64}> : (!riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v267:[0-9]+]] = "riscv.mul"(%[[v289]], %[[v270]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v262:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_2]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v263:[0-9]+]] = "riscv.rem"(%[[v267]], %[[v262]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v259:[0-9]+]] = "riscv.add"(%[[v263]], %[[v304]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v254:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_2]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v255:[0-9]+]] = "riscv.rem"(%[[v259]], %[[v254]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v251:[0-9]+]] = "riscv.sub"(%[[v304]], %[[v263]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v246:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_2]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v247:[0-9]+]] = "riscv.add"(%[[v246]], %[[v251]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v242:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_2]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v243:[0-9]+]] = "riscv.rem"(%[[v247]], %[[v242]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v237:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_0]]) : (!llvm.ptr) -> !riscv.reg -// CHECK-NEXT: %[[v239:[0-9]+]] = "riscv.sh3add"(%[[v312]], %[[v237]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv.sd"(%[[v239]], %[[v255]]) <{"value" = 0 : i64}> : (!riscv.reg, !riscv.reg) -> () -// CHECK-NEXT: %[[v230:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_0]]) : (!llvm.ptr) -> !riscv.reg -// CHECK-NEXT: %[[v232:[0-9]+]] = "riscv.sh3add"(%[[v297]], %[[v230]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv.sd"(%[[v232]], %[[v243]]) <{"value" = 0 : i64}> : (!riscv.reg, !riscv.reg) -> () +// CHECK-NEXT: %[[v344:[0-9]+]] = "riscv.mul"(%[[varg27_3]], %[[varg42_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v340:[0-9]+]] = "riscv.add"(%[[varg49_0]], %[[v344]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v334:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_0]]) : (!llvm.ptr) -> !riscv.reg +// CHECK-NEXT: %[[v336:[0-9]+]] = "riscv.sh3add"(%[[v340]], %[[v334]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v332:[0-9]+]] = "riscv.ld"(%[[v336]]) <{"value" = 0 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v390:[0-9]+]] = "riscv.srli"(%[[varg27_3]]) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v147:[0-9]+]] = "riscv.add"(%[[varg27_3]], %[[v390]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v148:[0-9]+]] = "riscv.srai"(%[[v147]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v329:[0-9]+]] = "riscv.add"(%[[v148]], %[[v340]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v323:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_0]]) : (!llvm.ptr) -> !riscv.reg +// CHECK-NEXT: %[[v325:[0-9]+]] = "riscv.sh3add"(%[[v329]], %[[v323]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v321:[0-9]+]] = "riscv.ld"(%[[v325]]) <{"value" = 0 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v318:[0-9]+]] = "riscv.mul"(%[[varg49_0]], %[[v378]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v142:[0-9]+]] = "riscv.addi"(%[[v318]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v314:[0-9]+]] = "riscv.mul"(%[[varg27_1]], %[[v142]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v308:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_3]]) : (!llvm.ptr) -> !riscv.reg +// CHECK-NEXT: %[[v310:[0-9]+]] = "riscv.sh3add"(%[[v314]], %[[v308]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v306:[0-9]+]] = "riscv.ld"(%[[v310]]) <{"value" = 0 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v303:[0-9]+]] = "riscv.mul"(%[[v321]], %[[v306]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v298:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_2]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v299:[0-9]+]] = "riscv.rem"(%[[v303]], %[[v298]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v295:[0-9]+]] = "riscv.add"(%[[v299]], %[[v332]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v290:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_2]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v291:[0-9]+]] = "riscv.rem"(%[[v295]], %[[v290]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v287:[0-9]+]] = "riscv.sub"(%[[v332]], %[[v299]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v282:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_2]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v283:[0-9]+]] = "riscv.add"(%[[v282]], %[[v287]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v278:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_2]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v279:[0-9]+]] = "riscv.rem"(%[[v283]], %[[v278]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v273:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_0]]) : (!llvm.ptr) -> !riscv.reg +// CHECK-NEXT: %[[v275:[0-9]+]] = "riscv.sh3add"(%[[v340]], %[[v273]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv.sd"(%[[v275]], %[[v291]]) <{"value" = 0 : i64}> : (!riscv.reg, !riscv.reg) -> () +// CHECK-NEXT: %[[v266:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_0]]) : (!llvm.ptr) -> !riscv.reg +// CHECK-NEXT: %[[v268:[0-9]+]] = "riscv.sh3add"(%[[v329]], %[[v266]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv.sd"(%[[v268]], %[[v279]]) <{"value" = 0 : i64}> : (!riscv.reg, !riscv.reg) -> () // CHECK-NEXT: "riscv_cf.branch"() [^[[bb80:[0-9]+]]] : () -> () // CHECK-NEXT: ^[[bb80]](): -// CHECK-NEXT: %[[v225:[0-9]+]] = "riscv.add"(%[[v368]], %[[varg49_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v225]]) [^[[bb49]]] : (!riscv.reg) -> () +// CHECK-NEXT: %[[v139:[0-9]+]] = "riscv.addi"(%[[varg49_0]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v139]]) [^[[bb49]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb54]](): // CHECK-NEXT: "riscv_cf.branch"() [^[[bb84:[0-9]+]]] : () -> () // CHECK-NEXT: ^[[bb84]](): -// CHECK-NEXT: %[[v221:[0-9]+]] = "riscv.add"(%[[v368]], %[[varg42_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v221]]) [^[[bb42]]] : (!riscv.reg) -> () +// CHECK-NEXT: %[[v136:[0-9]+]] = "riscv.addi"(%[[varg42_0]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v136]]) [^[[bb42]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb47]](): -// CHECK-NEXT: %[[v217:[0-9]+]] = "riscv.div"(%[[varg27_1]], %[[v370]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v210:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_4]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v377:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg -// CHECK-NEXT: %[[v213:[0-9]+]] = "riscv.sltu"(%[[v377]], %[[v210]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v214:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v213]]) : (!riscv.reg) -> i1 -// CHECK-NEXT: %[[v130:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v214]]) : (i1) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.bnez"(%[[v130]]) [^[[bb90:[0-9]+]], ^[[bb91:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () +// CHECK-NEXT: %[[v391:[0-9]+]] = "riscv.srli"(%[[varg27_1]]) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v132:[0-9]+]] = "riscv.add"(%[[varg27_1]], %[[v391]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v133:[0-9]+]] = "riscv.srai"(%[[v132]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v258:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_4]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v385:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg +// CHECK-NEXT: %[[v261:[0-9]+]] = "riscv.sltu"(%[[v385]], %[[v258]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v262:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v261]]) : (!riscv.reg) -> i1 +// CHECK-NEXT: %[[v190:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v262]]) : (i1) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.bnez"(%[[v190]]) [^[[bb90:[0-9]+]], ^[[bb91:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb90]](): -// CHECK-NEXT: %[[v208:[0-9]+]] = "riscv.div"(%[[varg27_3]], %[[v370]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v208]]) [^[[bb94:[0-9]+]]] : (!riscv.reg) -> () +// CHECK-NEXT: %[[v392:[0-9]+]] = "riscv.srli"(%[[varg27_3]]) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v126:[0-9]+]] = "riscv.add"(%[[varg27_3]], %[[v392]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v127:[0-9]+]] = "riscv.srai"(%[[v126]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v127]]) [^[[bb94:[0-9]+]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb91]](): -// CHECK-NEXT: %[[v204:[0-9]+]] = "riscv.add"(%[[varg27_3]], %[[varg27_3]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v204]]) [^[[bb94]]] : (!riscv.reg) -> () +// CHECK-NEXT: %[[v256:[0-9]+]] = "riscv.add"(%[[varg27_3]], %[[varg27_3]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v256]]) [^[[bb94]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb94]](%[[varg94_0:[a-zA-Z0-9_]+]] : !riscv.reg): -// CHECK-NEXT: %[[v197:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_4]]) : (i64) -> !riscv.reg -// CHECK-NEXT: %[[v378:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg -// CHECK-NEXT: %[[v200:[0-9]+]] = "riscv.sltu"(%[[v378]], %[[v197]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: %[[v201:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v200]]) : (!riscv.reg) -> i1 -// CHECK-NEXT: %[[v161:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v201]]) : (i1) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.bnez"(%[[v161]]) [^[[bb99:[0-9]+]], ^[[bb100:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () +// CHECK-NEXT: %[[v249:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[varg7_4]]) : (i64) -> !riscv.reg +// CHECK-NEXT: %[[v386:[0-9]+]] = "rv64.get_register"() : () -> !riscv.reg +// CHECK-NEXT: %[[v252:[0-9]+]] = "riscv.sltu"(%[[v386]], %[[v249]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v253:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v252]]) : (!riscv.reg) -> i1 +// CHECK-NEXT: %[[v221:[0-9]+]] = "builtin.unrealized_conversion_cast"(%[[v253]]) : (i1) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.bnez"(%[[v221]]) [^[[bb99:[0-9]+]], ^[[bb100:[0-9]+]]] <{"operandSegmentSizes" = array}> : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb99]](): -// CHECK-NEXT: %[[v195:[0-9]+]] = "riscv.add"(%[[varg27_0]], %[[varg27_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v195]]) [^[[bb103:[0-9]+]]] : (!riscv.reg) -> () +// CHECK-NEXT: %[[v247:[0-9]+]] = "riscv.add"(%[[varg27_0]], %[[varg27_0]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v247]]) [^[[bb103:[0-9]+]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb100]](): -// CHECK-NEXT: %[[v191:[0-9]+]] = "riscv.div"(%[[varg27_0]], %[[v370]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[v191]]) [^[[bb103]]] : (!riscv.reg) -> () +// CHECK-NEXT: %[[v393:[0-9]+]] = "riscv.srli"(%[[varg27_0]]) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v120:[0-9]+]] = "riscv.add"(%[[varg27_0]], %[[v393]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg +// CHECK-NEXT: %[[v121:[0-9]+]] = "riscv.srai"(%[[v120]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[v121]]) [^[[bb103]]] : (!riscv.reg) -> () // CHECK-NEXT: ^[[bb103]](%[[varg103_0:[a-zA-Z0-9_]+]] : !riscv.reg): // CHECK-NEXT: "riscv_cf.branch"() [^[[bb107:[0-9]+]]] : () -> () // CHECK-NEXT: ^[[bb107]](): -// CHECK-NEXT: %[[v187:[0-9]+]] = "riscv.add"(%[[v368]], %[[varg27_2]]) : (!riscv.reg, !riscv.reg) -> !riscv.reg -// CHECK-NEXT: "riscv_cf.branch"(%[[varg103_0]], %[[v217]], %[[v187]], %[[varg94_0]]) [^[[bb27]]] : (!riscv.reg, !riscv.reg, !riscv.reg, !riscv.reg) -> () +// CHECK-NEXT: %[[v115:[0-9]+]] = "riscv.addi"(%[[varg27_2]]) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg +// CHECK-NEXT: "riscv_cf.branch"(%[[varg103_0]], %[[v133]], %[[v115]], %[[varg94_0]]) [^[[bb27]]] : (!riscv.reg, !riscv.reg, !riscv.reg, !riscv.reg) -> () // CHECK-NEXT: ^[[bb40]](): // CHECK-NEXT: "llvm.return"() : () -> () // CHECK-NEXT: }) : () -> () diff --git a/Test/Passes/InstructionSelection/RISCV64/riscv_combine_srl_sra_signbit.mlir b/Test/Passes/InstructionSelection/RISCV64/riscv_combine_srl_sra_signbit.mlir new file mode 100644 index 000000000..c2eba9bd9 --- /dev/null +++ b/Test/Passes/InstructionSelection/RISCV64/riscv_combine_srl_sra_signbit.mlir @@ -0,0 +1,50 @@ +// RUN: veir-opt %s -p=riscv-combine | filecheck %s + +// `riscv.srli 63 (riscv.srai _ x) -> riscv.srli 63 x` (and the `i32` analogue at +// bit 31): an arithmetic right shift never changes the top bit, so a following +// logical shift by (width - 1), which keeps only that bit, doesn't care what the +// inner `srai`/`sraiw`'s own shift amount was. Mirrors LLVM's generic (division- +// agnostic) `DAGCombiner::visitSRL` rule `fold (srl (sra X, Y), 31) -> (srl X, 31)`. + +"builtin.module"() ({ + // riscv.srli 63 (riscv.srai 5 x) -> riscv.srli 63 x: the inner shift amount is + // discarded, and only the outer `srli 63` (renamed here, since a new op is + // created) survives. + "func.func"() <{function_type = (!riscv.reg) -> !riscv.reg}> ({ + ^bb(%x: !riscv.reg): + %sra = "riscv.srai"(%x) <{"value" = 5 : i64}> : (!riscv.reg) -> !riscv.reg + %srl = "riscv.srli"(%sra) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK: %{{.*}} = "riscv.srli"(%{{.*}}) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: "func.return"(%{{.*}}) : (!riscv.reg) -> () + "func.return"(%srl) : (!riscv.reg) -> () + }) : () -> () + + // i32 analogue: riscv.srliw 31 (riscv.sraiw 7 x) -> riscv.srliw 31 x. + "func.func"() <{function_type = (!riscv.reg) -> !riscv.reg}> ({ + ^bb(%x: !riscv.reg): + %sraw = "riscv.sraiw"(%x) <{"value" = 7 : i64}> : (!riscv.reg) -> !riscv.reg + %srlw = "riscv.srliw"(%sraw) <{"value" = 31 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK: %{{.*}} = "riscv.srliw"(%{{.*}}) <{"value" = 31 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: "func.return"(%{{.*}}) : (!riscv.reg) -> () + "func.return"(%srlw) : (!riscv.reg) -> () + }) : () -> () + + // Outer shift amount not (width - 1): the pattern must not fire, so both + // instructions survive. + "func.func"() <{function_type = (!riscv.reg) -> !riscv.reg}> ({ + ^bb(%x: !riscv.reg): + %sra = "riscv.srai"(%x) <{"value" = 5 : i64}> : (!riscv.reg) -> !riscv.reg + %srl = "riscv.srli"(%sra) <{"value" = 62 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK: %{{.*}} = "riscv.srai"(%{{.*}}) <{"value" = 5 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.srli"(%{{.*}}) <{"value" = 62 : i64}> : (!riscv.reg) -> !riscv.reg + "func.return"(%srl) : (!riscv.reg) -> () + }) : () -> () + + // No inner `srai`: not matched, `riscv.srli` is left as-is. + "func.func"() <{function_type = (!riscv.reg) -> !riscv.reg}> ({ + ^bb(%x: !riscv.reg): + %srl = "riscv.srli"(%x) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK: %{{.*}} = "riscv.srli"(%{{.*}}) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg + "func.return"(%srl) : (!riscv.reg) -> () + }) : () -> () +}) : () -> () diff --git a/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_by2.mlir b/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_by2.mlir new file mode 100644 index 000000000..c4330e92e --- /dev/null +++ b/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_by2.mlir @@ -0,0 +1,36 @@ +// RUN: veir-opt %s -p=isel-sdag-riscv64,riscv-combine | filecheck %s + +// `sdiv x, 2` is the one power-of-two divisor where `sdivPow2`'s general +// 4-instruction sequence shrinks to 3: the correction shift's amount `W - k` +// coincides with `W - 1` exactly when `k = 1`, so `riscv-combine`'s +// `srl_sra_signbit` folds away the sign-splat `srai`. This matches LLVM's actual +// `llc` output for `sdiv i64/i32 %a, 2` (and is *not* a `k = 1` special case in +// `sdivPow2` itself; the negative-divisor and non-eligible-`k` cases are covered +// directly in `riscv_combine_srl_sra_signbit.mlir`). + +"builtin.module"() ({ + // llvm.sdiv x, 2 -> riscv.srli 63 x / riscv.add x _ / riscv.srai 1 _ + // (no `riscv.srai 63` sign-splat survives). + "func.func"() <{function_type = (i64) -> i64}> ({ + ^bb(%a: i64): + %c = "llvm.mlir.constant"() <{value = 2 : i64}> : () -> i64 + %r = "llvm.sdiv"(%a, %c) : (i64, i64) -> i64 + // CHECK: %{{.*}} = "riscv.srli"(%{{.*}}) <{"value" = 63 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.add"(%{{.*}}, %{{.*}}) : (!riscv.reg, !riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.srai"(%{{.*}}) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NOT: "riscv.srai"(%{{.*}}) <{"value" = 63 : i64}> + "func.return"(%r) : (i64) -> () + }) : () -> () + + // i32 analogue: riscv.srliw 31 x / riscv.addw x _ / riscv.sraiw 1 _. + "func.func"() <{function_type = (i32) -> i32}> ({ + ^bb(%a: i32): + %c = "llvm.mlir.constant"() <{value = 2 : i32}> : () -> i32 + %r = "llvm.sdiv"(%a, %c) : (i32, i32) -> i32 + // CHECK: %{{.*}} = "riscv.srliw"(%{{.*}}) <{"value" = 31 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.addw"(%{{.*}}, %{{.*}}) : (!riscv.reg, !riscv.reg) -> !riscv.reg + // CHECK-NEXT: %{{.*}} = "riscv.sraiw"(%{{.*}}) <{"value" = 1 : i64}> : (!riscv.reg) -> !riscv.reg + // CHECK-NOT: "riscv.sraiw"(%{{.*}}) <{"value" = 31 : i64}> + "func.return"(%r) : (i32) -> () + }) : () -> () +}) : () -> () diff --git a/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_exact_exec.mlir b/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_exact_exec.mlir new file mode 100644 index 000000000..98c1d9623 --- /dev/null +++ b/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_exact_exec.mlir @@ -0,0 +1,23 @@ +// RUN: veir-interpret %s | filecheck %s --check-prefix=SRC +// RUN: veir-opt %s -p=canonicalize,instcombine,canonicalize,cse,dce,isel-br-riscv64,isel-sdag-riscv64,isel-riscv64,canonicalize,riscv-combine,reconcile-cast,dce > %t && veir-interpret %t | filecheck %s + +// Functional check for `sdivPow2Exact` (positive and negative divisor): evenly +// divisible signed division by a constant power of two, using the `exact` flag. +// Since the division is exact, the plain arithmetic-shift fast path agrees with +// full truncating division (no bias correction needed). + +"builtin.module"() ({ + "func.func"() <{sym_name = "main", function_type = () -> (i64, i64, i64)}> ({ + %pos = "llvm.mlir.constant"() <{value = 16 : i64}> : () -> i64 + %neg = "llvm.mlir.constant"() <{value = -16 : i64}> : () -> i64 + %div4 = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64 + %divneg4 = "llvm.mlir.constant"() <{value = -4 : i64}> : () -> i64 + %r0 = "llvm.sdiv"(%pos, %div4) <{exact}> : (i64, i64) -> i64 + %r1 = "llvm.sdiv"(%neg, %div4) <{exact}> : (i64, i64) -> i64 + %r2 = "llvm.sdiv"(%pos, %divneg4) <{exact}> : (i64, i64) -> i64 + "func.return"(%r0, %r1, %r2) : (i64, i64, i64) -> () + }) : () -> () +}) : () -> () + +// SRC: Program output: #[0x0000000000000004#64, 0xfffffffffffffffc#64, 0xfffffffffffffffc#64] +// CHECK: Program output: #[0x0000000000000004#64, 0xfffffffffffffffc#64, 0xfffffffffffffffc#64] diff --git a/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_exec.mlir b/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_exec.mlir new file mode 100644 index 000000000..ad60540da --- /dev/null +++ b/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_exec.mlir @@ -0,0 +1,25 @@ +// RUN: veir-interpret %s | filecheck %s --check-prefix=SRC +// RUN: veir-opt %s -p=canonicalize,instcombine,canonicalize,cse,dce,isel-br-riscv64,isel-sdag-riscv64,isel-riscv64,canonicalize,riscv-combine,reconcile-cast,dce > %t && veir-interpret %t | filecheck %s + +// Functional check for `sdivPow2` (general, non-`exact`, positive and negative +// divisor): truncating (round-toward-zero) division by a constant power of two. +// `-15 sdiv 4` exercises the bias correction (a plain arithmetic shift would give +// the floor, `-4`, instead of the truncated `-3`); the `y < 0` cases exercise the +// final negation. + +"builtin.module"() ({ + "func.func"() <{sym_name = "main", function_type = () -> (i64, i64, i64, i64)}> ({ + %pos = "llvm.mlir.constant"() <{value = 15 : i64}> : () -> i64 + %neg = "llvm.mlir.constant"() <{value = -15 : i64}> : () -> i64 + %div4 = "llvm.mlir.constant"() <{value = 4 : i64}> : () -> i64 + %divneg4 = "llvm.mlir.constant"() <{value = -4 : i64}> : () -> i64 + %r0 = "llvm.sdiv"(%pos, %div4) : (i64, i64) -> i64 + %r1 = "llvm.sdiv"(%neg, %div4) : (i64, i64) -> i64 + %r2 = "llvm.sdiv"(%pos, %divneg4) : (i64, i64) -> i64 + %r3 = "llvm.sdiv"(%neg, %divneg4) : (i64, i64) -> i64 + "func.return"(%r0, %r1, %r2, %r3) : (i64, i64, i64, i64) -> () + }) : () -> () +}) : () -> () + +// SRC: Program output: #[0x0000000000000003#64, 0xfffffffffffffffd#64, 0xfffffffffffffffd#64, 0x0000000000000003#64] +// CHECK: Program output: #[0x0000000000000003#64, 0xfffffffffffffffd#64, 0xfffffffffffffffd#64, 0x0000000000000003#64] diff --git a/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_i32_exec.mlir b/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_i32_exec.mlir new file mode 100644 index 000000000..8df546ebe --- /dev/null +++ b/Test/Passes/InstructionSelection/RISCV64/sdiv_pow2_i32_exec.mlir @@ -0,0 +1,18 @@ +// RUN: veir-interpret %s | filecheck %s --check-prefix=SRC +// RUN: veir-opt %s -p=canonicalize,instcombine,canonicalize,cse,dce,isel-br-riscv64,isel-sdag-riscv64,isel-riscv64,canonicalize,riscv-combine,reconcile-cast,dce > %t && veir-interpret %t | filecheck %s + +// `i32` analogue of sdiv_pow2_exec.mlir (`sdivwPow2`, general non-`exact` form). + +"builtin.module"() ({ + "func.func"() <{sym_name = "main", function_type = () -> (i32, i32)}> ({ + %neg = "llvm.mlir.constant"() <{value = -15 : i32}> : () -> i32 + %div4 = "llvm.mlir.constant"() <{value = 4 : i32}> : () -> i32 + %divneg4 = "llvm.mlir.constant"() <{value = -4 : i32}> : () -> i32 + %r0 = "llvm.sdiv"(%neg, %div4) : (i32, i32) -> i32 + %r1 = "llvm.sdiv"(%neg, %divneg4) : (i32, i32) -> i32 + "func.return"(%r0, %r1) : (i32, i32) -> () + }) : () -> () +}) : () -> () + +// SRC: Program output: #[0xfffffffd#32, 0x00000003#32] +// CHECK: Program output: #[0xfffffffd#32, 0x00000003#32] diff --git a/Test/Passes/InstructionSelection/RISCV64/udiv_pow2_exec.mlir b/Test/Passes/InstructionSelection/RISCV64/udiv_pow2_exec.mlir new file mode 100644 index 000000000..cc2880570 --- /dev/null +++ b/Test/Passes/InstructionSelection/RISCV64/udiv_pow2_exec.mlir @@ -0,0 +1,23 @@ +// RUN: veir-interpret %s | filecheck %s --check-prefix=SRC +// RUN: veir-opt %s -p=canonicalize,instcombine,canonicalize,cse,dce,isel-br-riscv64,isel-sdag-riscv64,isel-riscv64,canonicalize,riscv-combine,reconcile-cast,dce > %t && veir-interpret %t | filecheck %s + +// Functional check for `udivPow2`: unsigned division by a constant power of two, +// including the `2^63` boundary (whose bit pattern is decoded as a negative `Int` +// even though `udiv` treats it as unsigned -- see the regression case in +// divpow2.mlir). + +"builtin.module"() ({ + "func.func"() <{sym_name = "main", function_type = () -> (i64, i64)}> ({ + %a = "llvm.mlir.constant"() <{value = 37 : i64}> : () -> i64 + %b = "llvm.mlir.constant"() <{value = 8 : i64}> : () -> i64 + %r0 = "llvm.udiv"(%a, %b) : (i64, i64) -> i64 + // (2^63 + 5) udiv 2^63 = 1 + %c = "llvm.mlir.constant"() <{value = -9223372036854775803 : i64}> : () -> i64 + %d = "llvm.mlir.constant"() <{value = -9223372036854775808 : i64}> : () -> i64 + %r1 = "llvm.udiv"(%c, %d) : (i64, i64) -> i64 + "func.return"(%r0, %r1) : (i64, i64) -> () + }) : () -> () +}) : () -> () + +// SRC: Program output: #[0x0000000000000004#64, 0x0000000000000001#64] +// CHECK: Program output: #[0x0000000000000004#64, 0x0000000000000001#64] diff --git a/Test/Passes/InstructionSelection/RISCV64/udiv_pow2_i32_exec.mlir b/Test/Passes/InstructionSelection/RISCV64/udiv_pow2_i32_exec.mlir new file mode 100644 index 000000000..15750bcd9 --- /dev/null +++ b/Test/Passes/InstructionSelection/RISCV64/udiv_pow2_i32_exec.mlir @@ -0,0 +1,16 @@ +// RUN: veir-interpret %s | filecheck %s --check-prefix=SRC +// RUN: veir-opt %s -p=canonicalize,instcombine,canonicalize,cse,dce,isel-br-riscv64,isel-sdag-riscv64,isel-riscv64,canonicalize,riscv-combine,reconcile-cast,dce > %t && veir-interpret %t | filecheck %s + +// `i32` analogue of udiv_pow2_exec.mlir (`udivwPow2`). + +"builtin.module"() ({ + "func.func"() <{sym_name = "main", function_type = () -> i32}> ({ + %a = "llvm.mlir.constant"() <{value = 37 : i32}> : () -> i32 + %b = "llvm.mlir.constant"() <{value = 8 : i32}> : () -> i32 + %r = "llvm.udiv"(%a, %b) : (i32, i32) -> i32 + "func.return"(%r) : (i32) -> () + }) : () -> () +}) : () -> () + +// SRC: Program output: #[0x00000004#32] +// CHECK: Program output: #[0x00000004#32] diff --git a/Veir/Passes/InstructionSelection/Proofs.lean b/Veir/Passes/InstructionSelection/Proofs.lean index 6df5cf652..52d966090 100644 --- a/Veir/Passes/InstructionSelection/Proofs.lean +++ b/Veir/Passes/InstructionSelection/Proofs.lean @@ -317,6 +317,73 @@ theorem udiv_refinement {x y : LLVM.Int 64} : (Data.LLVM.Int.udiv x y) ⊒ (RISCV.Reg.toInt (Data.RISCV.divu (LLVM.Int.toReg y) (LLVM.Int.toReg x)) 64) := by veir_bv_decide +/-! ### `sdiv`/`udiv` by a constant power of two -/ + +set_option warn.sorry false in +/-- + `udiv x, 2^k` -> `riscv.srli x, k` (`udivPow2`). Mirrors `DAGCombiner::visitUDIVLike`'s + `fold (udiv x, (1 << c)) -> x >>u c` (via `BuildLogBase2`). + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L5430-L5440 +-/ +theorem udivPow2_refinement {x : LLVM.Int 64} (k : BitVec 6) : + (Data.LLVM.Int.udiv x (LLVM.Int.val ((1#64) <<< k))) ⊒ + (RISCV.Reg.toInt (Data.RISCV.srli k (LLVM.Int.toReg x)) 64) := by + sorry -- bv_decide needs a non-default timeout (120s) to close this goal + +set_option warn.sorry false in +/-- + `sdiv exact x, 2^k` -> `riscv.srai x, k` (`sdivPow2Exact`, positive divisor). + Since `exact` makes the source poison whenever `x` isn't a multiple of `2^k`, this + only has to hold when the arithmetic right shift and the truncating division + agree, i.e. when there is no fractional part to round differently. +-/ +theorem sdivPow2Exact_pos_refinement {x : LLVM.Int 64} (k : BitVec 6) (hk : k < 63) : + (Data.LLVM.Int.sdiv x (LLVM.Int.val ((1#64) <<< k)) true) ⊒ + (RISCV.Reg.toInt (Data.RISCV.srai k (LLVM.Int.toReg x)) 64) := by + sorry -- bv_decide needs a non-default timeout (120s) to close this goal + +set_option warn.sorry false in +/-- + `sdiv exact x, -2^k` -> `riscv.sub 0, (riscv.srai x, k)` (`sdivPow2Exact`, negative + divisor). No upper bound on `k` is needed here: `-2^63` (`k = 63`) is itself a + valid `i64` divisor. +-/ +theorem sdivPow2Exact_neg_refinement {x : LLVM.Int 64} (k : BitVec 6) : + (Data.LLVM.Int.sdiv x (LLVM.Int.val (-((1#64) <<< k))) true) ⊒ + (RISCV.Reg.toInt (Data.RISCV.neg (Data.RISCV.srai k (LLVM.Int.toReg x))) 64) := by + sorry -- bv_decide needs a non-default timeout (120s) to close this goal + +set_option warn.sorry false in +/-- + General (non-`exact`) `sdiv x, 2^k` -> the Hacker's-Delight bias/shift sequence + (`sdivPow2`, positive divisor): bias a negative dividend by `2^k - 1` before the + arithmetic shift, so truncation rounds toward zero. `k = 0` is excluded because the + correction shift `64 - k` would then need a full 64-bit shift, which has no legal + RISC-V immediate encoding (`sdiv x, ±1` never reaches instruction selection as + such: it is always simplified away first). +-/ +theorem sdivPow2_pos_refinement {x : LLVM.Int 64} (k : BitVec 6) (hk0 : 0 < k) (hk63 : k < 63) : + (Data.LLVM.Int.sdiv x (LLVM.Int.val ((1#64) <<< k)) false) ⊒ + (RISCV.Reg.toInt + (let sign := Data.RISCV.srai 63 (LLVM.Int.toReg x) + let corr := Data.RISCV.srli (64 - k) sign + let biased := Data.RISCV.add corr (LLVM.Int.toReg x) + Data.RISCV.srai k biased) 64) := by + sorry -- bv_decide needs a non-default timeout (300s) to close this goal + +set_option warn.sorry false in +/-- + Negative-divisor case of `sdivPow2_pos_refinement`: negate the biased-shift result. +-/ +theorem sdivPow2_neg_refinement {x : LLVM.Int 64} (k : BitVec 6) (hk0 : 0 < k) : + (Data.LLVM.Int.sdiv x (LLVM.Int.val (-((1#64) <<< k))) false) ⊒ + (RISCV.Reg.toInt + (let sign := Data.RISCV.srai 63 (LLVM.Int.toReg x) + let corr := Data.RISCV.srli (64 - k) sign + let biased := Data.RISCV.add corr (LLVM.Int.toReg x) + Data.RISCV.neg (Data.RISCV.srai k biased)) 64) := by + sorry -- bv_decide needs a non-default timeout (300s) to close this goal + /-- Prove the correctness of the `udiv` lowering pattern. -/ @@ -921,6 +988,51 @@ theorem udiv_refinement_32 {x y : LLVM.Int 32} : (RISCV.Reg.toInt (Data.RISCV.divuw (LLVM.Int.toReg y) (LLVM.Int.toReg x)) 32) := by veir_bv_decide +/-- `i32` analogue of `udivPow2_refinement` (`udivwPow2`). -/ +theorem udivwPow2_refinement {x : LLVM.Int 32} (k : BitVec 5) : + (Data.LLVM.Int.udiv x (LLVM.Int.val ((1#32) <<< k))) ⊒ + (RISCV.Reg.toInt (Data.RISCV.srliw k (LLVM.Int.toReg x)) 32) := by + veir_bv_decide + +set_option warn.sorry false in +/-- `i32` analogue of `sdivPow2Exact_pos_refinement` (`sdivwPow2Exact`, positive + divisor): a genuine positive `i32` divisor `2^k` needs `k < 31`. -/ +theorem sdivwPow2Exact_pos_refinement {x : LLVM.Int 32} (k : BitVec 5) (hk : k < 31) : + (Data.LLVM.Int.sdiv x (LLVM.Int.val ((1#32) <<< k)) true) ⊒ + (RISCV.Reg.toInt (Data.RISCV.sraiw k (LLVM.Int.toReg x)) 32) := by + sorry -- bv_decide times out with the default timeout on this goal + +set_option warn.sorry false in +/-- `i32` analogue of `sdivPow2Exact_neg_refinement` (`sdivwPow2Exact`, negative + divisor): `-2^31` (`k = 31`) is itself a valid `i32` divisor, so no upper bound + on `k` is needed. -/ +theorem sdivwPow2Exact_neg_refinement {x : LLVM.Int 32} (k : BitVec 5) : + (Data.LLVM.Int.sdiv x (LLVM.Int.val (-((1#32) <<< k))) true) ⊒ + (RISCV.Reg.toInt (Data.RISCV.negw (Data.RISCV.sraiw k (LLVM.Int.toReg x))) 32) := by + sorry -- bv_decide times out with the default timeout on this goal + +set_option warn.sorry false in +/-- `i32` analogue of `sdivPow2_pos_refinement` (`sdivwPow2`, positive divisor). -/ +theorem sdivwPow2_pos_refinement {x : LLVM.Int 32} (k : BitVec 5) (hk0 : 0 < k) (hk31 : k < 31) : + (Data.LLVM.Int.sdiv x (LLVM.Int.val ((1#32) <<< k)) false) ⊒ + (RISCV.Reg.toInt + (let sign := Data.RISCV.sraiw 31 (LLVM.Int.toReg x) + let corr := Data.RISCV.srliw (32 - k) sign + let biased := Data.RISCV.addw corr (LLVM.Int.toReg x) + Data.RISCV.sraiw k biased) 32) := by + sorry -- bv_decide needs a non-default timeout (300s) to close this goal + +set_option warn.sorry false in +/-- `i32` analogue of `sdivPow2_neg_refinement` (`sdivwPow2`, negative divisor). -/ +theorem sdivwPow2_neg_refinement {x : LLVM.Int 32} (k : BitVec 5) (hk0 : 0 < k) : + (Data.LLVM.Int.sdiv x (LLVM.Int.val (-((1#32) <<< k))) false) ⊒ + (RISCV.Reg.toInt + (let sign := Data.RISCV.sraiw 31 (LLVM.Int.toReg x) + let corr := Data.RISCV.srliw (32 - k) sign + let biased := Data.RISCV.addw corr (LLVM.Int.toReg x) + Data.RISCV.negw (Data.RISCV.sraiw k biased)) 32) := by + sorry -- bv_decide times out with the default timeout on this goal + theorem srem_refinement_32 {x y : LLVM.Int 32} : (Data.LLVM.Int.srem x y) ⊒ (RISCV.Reg.toInt (Data.RISCV.remw (LLVM.Int.toReg y) (LLVM.Int.toReg x)) 32) := by diff --git a/Veir/Passes/InstructionSelection/RISCV64Sdag.lean b/Veir/Passes/InstructionSelection/RISCV64Sdag.lean index 563565c54..f0afacc78 100644 --- a/Veir/Passes/InstructionSelection/RISCV64Sdag.lean +++ b/Veir/Passes/InstructionSelection/RISCV64Sdag.lean @@ -406,6 +406,161 @@ def sext_1 (rewriter : PatternRewriter OpCode) (op : OperationPtr) #[] #[] () (some $ .before op) return rewriter.replaceOp! op castOp +/-! ## Division by a constant power of two + + RISC-V has no divide-by-constant strength reduction in hardware, so a `udiv`/`sdiv` + by a constant power of two is turned into shifts here. This mirrors the + target-independent `DAGCombiner::visitUDIVLike` / `DAGCombiner::visitSDIVLike`: + RISC-V does not override this generic lowering with something target-specific + unless the `short-forward-branch-ialu` tuning feature is set (in which case + `RISCVTargetLowering::BuildSDIVPow2` instead emits a branchy `cmov` form), which we + do not model, so the sequences below are what a plain `-mtriple=riscv64` emits. + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L5270-L5285 +-/ + +/-- The `w`-bit unsigned magnitude of `v`, i.e. `v`'s bit pattern reduced mod `2^w`. + Needed because a `udiv` divisor whose top bit is set is decoded as a negative + `Int` (integer attributes carry no signedness), even though `udiv` treats the + bit pattern as unsigned. -/ +def unsignedMod (w : Nat) (v : Int) : Nat := (v % ((2 : Int) ^ w)).toNat + +/-- If `m` is a nonzero power of two, return its base-2 logarithm. -/ +def log2IfPow2 (m : Nat) : Option Nat := + if m == 0 || (m &&& (m - 1)) != 0 then none else some (Nat.log2 m) + +/-- If `|v|` is a nonzero power of two, return its base-2 logarithm together with + whether `v` is negative. Used for `sdiv`, whose divisor is signed, so `v` (as + decoded) already carries the correct sign. Mirrors `isDivisorPowerOfTwo`. + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L5270-L5285 -/ +def matchSignedPow2Divisor (v : Int) : Option (Nat × Bool) := do + let k ← log2IfPow2 v.natAbs + return (k, decide (v < 0)) + +/-- If the `w`-bit unsigned magnitude of `v` is a nonzero power of two, return its + base-2 logarithm. Used for `udiv`. -/ +def matchUnsignedPow2Divisor (w : Nat) (v : Int) : Option Nat := + log2IfPow2 (unsignedMod w v) + +/-- `udiv x, 2^k` -> `OP x, k`, where `OP` is `riscv.srli` (`width = 64`) or + `riscv.srliw` (`width = 32`, the `i32` analogue). Mirrors + `DAGCombiner::visitUDIVLike`'s `fold (udiv x, (1 << c)) -> x >>u c` (via + `BuildLogBase2`). + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L5430-L5440 -/ +def udivPow2Gen (dst : Riscv) (h : Riscv.propertiesOf dst = RISCVImmediateProperties) + (width : Nat) (rewriter : PatternRewriter OpCode) (op : OperationPtr) + (_ : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do + let some (lhs, rhs, _) := matchUdiv op rewriter.ctx | return rewriter + let .integerType t := ((op.getResult 0).get! rewriter.ctx.raw).type.val | return rewriter + if t.bitwidth ≠ width then return rewriter + let some imm := matchConstantIntVal rhs rewriter.ctx | return rewriter + let some k := matchUnsignedPow2Divisor width imm.value | return rewriter + let (rewriter, xReg) ← castToReg rewriter op lhs + let shamt := RISCVImmediateProperties.mk (IntegerAttr.mk k (IntegerType.mk 64)) + let (rewriter, shiftOp) := rewriter.createOp! (.riscv dst) #[RegisterType.mk] #[xReg] + #[] #[] (cast h.symm shamt) (some $ .before op) + replaceWithReg rewriter op (shiftOp.getResult 0) + +def udivPow2 := udivPow2Gen .srli rfl 64 +def udivwPow2 := udivPow2Gen .srliw rfl 32 + +/-- `riscv.sub 0, x` (`riscv.subw` at `i32`, selected via `negDst`): negates `x`. + Used to correct the quotient of a `sdiv`-by-power-of-two lowering when the + divisor is negative. -/ +def negateReg (negDst : Riscv) (h : Riscv.propertiesOf negDst = Unit) + (rewriter : PatternRewriter OpCode) (op : OperationPtr) (x : ValuePtr) : + PatternRewriter OpCode × OperationPtr := + let zero := RISCVImmediateProperties.mk (IntegerAttr.mk 0 (IntegerType.mk 64)) + let (rewriter, zeroOp) := rewriter.createOp! (.riscv .li) #[RegisterType.mk] #[] + #[] #[] zero (some $ .before op) + rewriter.createOp! (.riscv negDst) #[RegisterType.mk] #[zeroOp.getResult 0, x] + #[] #[] (cast h.symm ()) (some $ .before op) + +/-- `sdiv exact x, 2^k` -> `dst x, k` (`dst` = `riscv.srai`/`riscv.sraiw`); when the + divisor is negative, negate the shifted result via `negDst` + (`riscv.sub`/`riscv.subw`): `sdiv exact x, -2^k` -> `negDst 0, (dst x, k)`. + Mirrors `TargetLowering::BuildExactSDIV` (a plain arithmetic shift by the + trailing-zero count, times a ±1 "magic factor" that the surrounding combines + fold into a no-op or a negation). `DAGCombiner::visitSDIVLike` takes this path + instead of the general correction sequence below whenever the `exact` flag is + set, since it is cheaper. + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L5294-L5301 + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/TargetLowering.cpp#L6454-L6510 -/ +def sdivPow2ExactGen (dst : Riscv) (hDst : Riscv.propertiesOf dst = RISCVImmediateProperties) + (negDst : Riscv) (hNeg : Riscv.propertiesOf negDst = Unit) (width : Nat) + (rewriter : PatternRewriter OpCode) (op : OperationPtr) + (_ : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do + let some (lhs, rhs, props) := matchSdiv op rewriter.ctx | return rewriter + if ¬ props.exact then return rewriter + let .integerType t := ((op.getResult 0).get! rewriter.ctx.raw).type.val | return rewriter + if t.bitwidth ≠ width then return rewriter + let some imm := matchConstantIntVal rhs rewriter.ctx | return rewriter + let some (k, isNeg) := matchSignedPow2Divisor imm.value | return rewriter + let (rewriter, xReg) ← castToReg rewriter op lhs + let shamt := RISCVImmediateProperties.mk (IntegerAttr.mk k (IntegerType.mk 64)) + let (rewriter, sraOp) := rewriter.createOp! (.riscv dst) #[RegisterType.mk] #[xReg] + #[] #[] (cast hDst.symm shamt) (some $ .before op) + if ¬ isNeg then replaceWithReg rewriter op (sraOp.getResult 0) + else + let (rewriter, negOp) := negateReg negDst hNeg rewriter op (sraOp.getResult 0) + replaceWithReg rewriter op (negOp.getResult 0) + +def sdivPow2Exact := sdivPow2ExactGen .srai rfl .sub rfl 64 +def sdivwPow2Exact := sdivPow2ExactGen .sraiw rfl .subw rfl 32 + +/-- General `sdiv x, 2^k` (`exact` not set): bias negative dividends before + shifting so truncation rounds toward zero, then negate for a negative divisor: + ``` + sign := shiftDst x, (width - 1) -- splat the sign bit + corr := corrDst sign, (width - k) -- 2^k - 1 if x < 0, else 0 + biased := addDst x, corr + q := shiftDst biased, k + ``` + then `negDst 0, q` when the divisor is negative, where + `(shiftDst, corrDst, addDst, negDst)` is `(riscv.srai, riscv.srli, riscv.add, + riscv.sub)` at `width = 64` and the `w`-suffixed forms at `width = 32`. Mirrors + the generic `sra`/`srl`/`add` sequence built by `DAGCombiner::visitSDIVLike` + when the `exact` bit isn't set (Hacker's Delight §10-1); RISC-V's + `BuildSDIVPow2` only replaces this with a branchy `cmov` form under + `short-forward-branch-ialu` tuning, which we do not model, so this generic + sequence is what RV64 emits by default. + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L5294-L5345 + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/Target/RISCV/RISCVISelLowering.cpp#L27055-L27074 -/ +def sdivPow2Gen (shiftDst : Riscv) (hShift : Riscv.propertiesOf shiftDst = RISCVImmediateProperties) + (corrDst : Riscv) (hCorr : Riscv.propertiesOf corrDst = RISCVImmediateProperties) + (addDst : Riscv) (hAdd : Riscv.propertiesOf addDst = Unit) + (negDst : Riscv) (hNeg : Riscv.propertiesOf negDst = Unit) (width : Nat) + (rewriter : PatternRewriter OpCode) (op : OperationPtr) + (_ : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do + let some (lhs, rhs, props) := matchSdiv op rewriter.ctx | return rewriter + if props.exact then return rewriter + let .integerType t := ((op.getResult 0).get! rewriter.ctx.raw).type.val | return rewriter + if t.bitwidth ≠ width then return rewriter + let some imm := matchConstantIntVal rhs rewriter.ctx | return rewriter + let some (k, isNeg) := matchSignedPow2Divisor imm.value | return rewriter + /- `k = 0` (divisor ±1) would need a shift by the full register width, which has + no legal immediate encoding; middle-end optimizations always turn `sdiv x, ±1` + into `x`/`-x` well before instruction selection, so this case does not arise. -/ + if k = 0 then return rewriter + let (rewriter, xReg) ← castToReg rewriter op lhs + let shSign := RISCVImmediateProperties.mk (IntegerAttr.mk (width - 1) (IntegerType.mk 64)) + let (rewriter, signOp) := rewriter.createOp! (.riscv shiftDst) #[RegisterType.mk] #[xReg] + #[] #[] (cast hShift.symm shSign) (some $ .before op) + let shCorr := RISCVImmediateProperties.mk (IntegerAttr.mk (width - k) (IntegerType.mk 64)) + let (rewriter, corrOp) := rewriter.createOp! (.riscv corrDst) #[RegisterType.mk] #[signOp.getResult 0] + #[] #[] (cast hCorr.symm shCorr) (some $ .before op) + let (rewriter, biasedOp) := rewriter.createOp! (.riscv addDst) #[RegisterType.mk] + #[xReg, corrOp.getResult 0] #[] #[] (cast hAdd.symm ()) (some $ .before op) + let shQ := RISCVImmediateProperties.mk (IntegerAttr.mk k (IntegerType.mk 64)) + let (rewriter, qOp) := rewriter.createOp! (.riscv shiftDst) #[RegisterType.mk] #[biasedOp.getResult 0] + #[] #[] (cast hShift.symm shQ) (some $ .before op) + if ¬ isNeg then replaceWithReg rewriter op (qOp.getResult 0) + else + let (rewriter, negOp) := negateReg negDst hNeg rewriter op (qOp.getResult 0) + replaceWithReg rewriter op (negOp.getResult 0) + +def sdivPow2 := sdivPow2Gen .srai rfl .srli rfl .add rfl .sub rfl 64 +def sdivwPow2 := sdivPow2Gen .sraiw rfl .srliw rfl .addw rfl .subw rfl 32 + /-! # Pass implementation -/ def IselSDAG.impl (ctx : WfIRContext OpCode) (op : OperationPtr) (_ : op.InBounds ctx.raw) : @@ -413,11 +568,15 @@ def IselSDAG.impl (ctx : WfIRContext OpCode) (op : OperationPtr) (_ : op.InBound /- Order matters where patterns overlap: the more specific Zbs/Zba rules (`bexti`, `slliuw`) must precede the generic `andi`/`slli` forms they would otherwise be shadowed by. The `bseti`/`bclri`/`binvi` rules are mutually exclusive with - `ori`/`andi`/`xori` via their `!isInt<12>` guard, so their order is immaterial. -/ + `ori`/`andi`/`xori` via their `!isInt<12>` guard, so their order is immaterial. + `sdivPow2Exact`/`sdivwPow2Exact` are listed before `sdivPow2`/`sdivwPow2` to + mirror the priority LLVM gives the `exact`-flag fast path, though both sides + already guard on `exact`, so the two pairs are in fact mutually exclusive. -/ let pattern := RewritePattern.GreedyRewritePattern #[andn, orn, xnor, orcb, bexti, bseti, bclri, binvi, slliuw, addi, ori, andi, xori, slli, srli, srai, slti, - addiw, slliw, srliw, sraiw, roriw, roliw, zext_1, sext_1] + addiw, slliw, srliw, sraiw, roriw, roliw, zext_1, sext_1, + udivPow2, udivwPow2, sdivPow2Exact, sdivwPow2Exact, sdivPow2, sdivwPow2] match RewritePattern.applyInContext pattern ctx with | none => throw "Error while applying SDAG patterns" | some ctx => pure ctx diff --git a/Veir/Passes/RISCVCombines/Combine.lean b/Veir/Passes/RISCVCombines/Combine.lean index bb02409e2..d9b6697bb 100644 --- a/Veir/Passes/RISCVCombines/Combine.lean +++ b/Veir/Passes/RISCVCombines/Combine.lean @@ -27,6 +27,38 @@ def right_identity_zero_add (rewriter: PatternRewriter OpCode) (op: OperationPtr let rewriter := rewriter.replaceValue (op.getResult 0) lhs sorry sorry sorry rewriter.eraseOp op sorry sorry sorry +set_option warn.sorry false in +/-- `srlDst (width - 1) (sraDst _ x) -> srlDst (width - 1) x`, where `(srlDst, + sraDst)` is `(riscv.srli, riscv.srai)` at `width = 64` and `(riscv.srliw, + riscv.sraiw)` at `width = 32`: an arithmetic right shift never changes the top + bit, so a subsequent logical shift by `width - 1` (which keeps only that bit) + doesn't care what the `sra`'s own shift amount was. Mirrors LLVM's generic + (division-agnostic) `DAGCombiner::visitSRL` rule + `fold (srl (sra X, Y), 31) -> (srl X, 31)` (there `31` is `OpSizeInBits - 1`, + i.e. `63` at `i64`). This -- not a `k = 1` special case in the `sdiv` lowering + itself -- is what shortens `sdiv x, 2`'s codegen relative to the general + `sdiv x, 2^k` sequence: the correction shift's amount `W - k` only happens to + coincide with `W - 1` when `k = 1`. + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L11628-L11633 -/ +def srl_sra_signbitGen (srlDst : Riscv) (hSrl : Riscv.propertiesOf srlDst = RISCVImmediateProperties) + (sraDst : Riscv) (width : Nat) (rewriter : PatternRewriter OpCode) (op : OperationPtr) + (opInBounds : op.InBounds rewriter.ctx.raw) : Option (PatternRewriter OpCode) := do + let some (operands, outerImm) := matchOp op rewriter.ctx (.riscv srlDst) 1 | return rewriter + if (cast hSrl outerImm : RISCVImmediateProperties).value.value ≠ (width : Int) - 1 then + return rewriter + let some sraOp := getDefiningOp operands[0]! rewriter.ctx | return rewriter + let some (sraOperands, _) := matchOp sraOp rewriter.ctx (.riscv sraDst) 1 | return rewriter + let (rewriter, newOp) := rewriter.createOp! (.riscv srlDst) #[RegisterType.mk] #[sraOperands[0]!] + #[] #[] outerImm (some $ .before op) + let rewriter := rewriter.replaceValue (op.getResult 0) (newOp.getResult 0) sorry sorry sorry + rewriter.eraseOp op sorry sorry sorry + +def srl_sra_signbit := srl_sra_signbitGen .srli rfl .srai 64 + +/-- `i32` analogue of `srl_sra_signbit`: `riscv.srliw 31 (riscv.sraiw _ x) -> + riscv.srliw 31 x`. -/ +def srlw_sraw_signbit := srl_sra_signbitGen .srliw rfl .sraiw 32 + set_option warn.sorry false in /-- riscv.li 0 -> rv64.get_register (x0) @@ -52,7 +84,8 @@ def li_zero_to_x0 (rewriter: PatternRewriter OpCode) (op: OperationPtr) def Combine.impl (ctx : WfIRContext OpCode) (op : OperationPtr) (_ : op.InBounds ctx.raw) : ExceptT String IO (WfIRContext OpCode) := do - let patterns : Array (RewritePattern OpCode) := #[right_identity_zero_add, li_zero_to_x0] + let patterns : Array (RewritePattern OpCode) := + #[right_identity_zero_add, srl_sra_signbit, srlw_sraw_signbit, li_zero_to_x0] let pattern := RewritePattern.GreedyRewritePattern patterns match RewritePattern.applyInContext pattern ctx with | none => throw "Error while applying pattern rewrites" diff --git a/Veir/Passes/RISCVCombines/Proofs.lean b/Veir/Passes/RISCVCombines/Proofs.lean index 99cc503bc..e3a8c112c 100644 --- a/Veir/Passes/RISCVCombines/Proofs.lean +++ b/Veir/Passes/RISCVCombines/Proofs.lean @@ -16,4 +16,27 @@ theorem right_identity_zero_add: (RISCV.add lhs (Data.RISCV.li (BitVec.ofInt 64 0))) = lhs := by veir_bv_decide +/-- + Prove the correctness of the `srl_sra_signbit` combine, phrased directly on the + already-selected RISC-V register ops the combine rewrites: `riscv.srli 63 + (riscv.srai shamt x) = riscv.srli 63 x`. An arithmetic right shift by any amount + `shamt` never changes the top bit, so a subsequent logical shift by 63 (which + keeps only that bit) gives the same result as skipping the `srai` entirely. The + RISC-V ops are total, so this is an exact equality. Mirrors LLVM's generic + `DAGCombiner::visitSRL` rule `fold (srl (sra X, Y), 31) -> (srl X, 31)`. + https://github.com/llvm/llvm-project/blob/2e87cf8c2b8ec6453ccfa7e448d5b33f1d71a2ca/llvm/lib/CodeGen/SelectionDAG/DAGCombiner.cpp#L11628-L11633 +-/ +theorem srl_sra_signbit {x : Reg} {shamt : BitVec 6} : + RISCV.srli 63 (RISCV.srai shamt x) = RISCV.srli 63 x := by + veir_bv_decide + +/-- + Prove the correctness of the `srlw_sraw_signbit` combine (the `i32` analogue of + `srl_sra_signbit`, at bit 31): `riscv.srliw 31 (riscv.sraiw shamt x) = + riscv.srliw 31 x`. +-/ +theorem srlw_sraw_signbit {x : Reg} {shamt : BitVec 5} : + RISCV.srliw 31 (RISCV.sraiw shamt x) = RISCV.srliw 31 x := by + veir_bv_decide + end Veir.Data.RISCV