Skip to content
Merged
Show file tree
Hide file tree
Changes from 34 commits
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
0083466
test
luisacicolini Apr 8, 2026
631d02c
or op
luisacicolini Apr 8, 2026
48ca02b
xor
luisacicolini Apr 8, 2026
1421b0a
mul
luisacicolini Apr 8, 2026
9b11b98
mul test
luisacicolini Apr 8, 2026
daaa670
mul tests
luisacicolini Apr 8, 2026
5e79b14
sdiv
luisacicolini Apr 8, 2026
66356a2
wip
luisacicolini Apr 8, 2026
f922a79
test
luisacicolini Apr 8, 2026
62649b9
urem
luisacicolini Apr 8, 2026
d31a3dc
fix
luisacicolini Apr 8, 2026
fc84815
fix
luisacicolini Apr 8, 2026
1054955
pattern
luisacicolini Apr 8, 2026
d0366e5
fix
luisacicolini Apr 8, 2026
b3d18d1
update files
luisacicolini Apr 8, 2026
aa6ab71
Merge branch 'luisa/isel-mul-div-rem' into luisa/isel-rem-urem
luisacicolini Apr 8, 2026
032709a
Apply suggestion from @luisacicolini
luisacicolini Apr 8, 2026
b6c973a
file
luisacicolini Apr 8, 2026
126d299
eof
luisacicolini Apr 8, 2026
cf1cafe
fix
luisacicolini Apr 8, 2026
3603763
Merge branch 'luisa/isel-mul-div-rem' into luisa/isel-rem-urem
luisacicolini Apr 8, 2026
fbc6973
wip
luisacicolini Apr 8, 2026
380f71c
merge
luisacicolini Apr 8, 2026
13bd022
wip
luisacicolini Apr 8, 2026
353516c
merge
luisacicolini Apr 9, 2026
949b3a3
sext
luisacicolini Apr 9, 2026
a9c30fe
trunc
luisacicolini Apr 9, 2026
2045058
fix
luisacicolini Apr 9, 2026
f6f3b7b
fix
luisacicolini Apr 9, 2026
22eec3c
test
luisacicolini Apr 9, 2026
d97f577
test
luisacicolini Apr 9, 2026
aa6ae01
invalid test
luisacicolini Apr 9, 2026
2ce8240
zext test
luisacicolini Apr 9, 2026
94a5318
test
luisacicolini Apr 9, 2026
e2f0c0e
fix
luisacicolini Apr 10, 2026
a3661ab
fix
luisacicolini Apr 10, 2026
179bf60
remove tests tested in verifier
luisacicolini Apr 10, 2026
3c790e3
fix tests
luisacicolini Apr 10, 2026
7b00b79
Merge remote-tracking branch 'origin' into luisa/isel-ext-trunc
luisacicolini Apr 10, 2026
98725af
fix
luisacicolini Apr 10, 2026
bc82076
fix
luisacicolini Apr 10, 2026
a7dc8ba
fix
luisacicolini Apr 10, 2026
939d543
remove check from pass bc done by verif
luisacicolini Apr 10, 2026
de130ea
fix test
luisacicolini Apr 10, 2026
9235224
test
luisacicolini Apr 10, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 28 additions & 0 deletions Test/Passes/InstructionSelection/RISCV64/sext.mlir
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
// RUN: veir-opt %s -p=isel-riscv64 | filecheck %s

"builtin.module"() ({
"func.func"() ({
^bb0(%a: i8, %b: i16, %c: i32, %d: i42):
%sexta = "llvm.sext"(%a) : (i8) -> i16
%sextb = "llvm.sext"(%b) : (i16) -> i32
%sextc = "llvm.sext"(%c) : (i32) -> i64
%sexdt = "llvm.sext"(%d) : (i42) -> i54

// CHECK: ^{{.*}}([[A:.*]] : i8, [[B:.*]] : i16, [[C:.*]] : i32, [[D:.*]] : i42):
// CHECK-NEXT: %[[E:.*]] = "builtin.unrealized_conversion_cast"([[A]]) : (i8) -> !reg
// CHECK-NEXT: %[[F:.*]] = "riscv.sextb"(%[[E]]) : (!reg) -> !reg
// CHECK-NEXT: %[[G:.*]] = "builtin.unrealized_conversion_cast"(%[[F]]) : (!reg) -> i16
// CHECK-NEXT: %[[H:.*]] = "builtin.unrealized_conversion_cast"([[B]]) : (i16) -> !reg
// CHECK-NEXT: %[[I:.*]] = "riscv.sexth"(%[[H]]) : (!reg) -> !reg
// CHECK-NEXT: %[[J:.*]] = "builtin.unrealized_conversion_cast"(%[[I]]) : (!reg) -> i32
// CHECK-NEXT: %[[K:.*]] = "builtin.unrealized_conversion_cast"([[C]]) : (i32) -> !reg
// CHECK-NEXT: %[[L:.*]] = "riscv.sextw"(%[[K]]) : (!reg) -> !reg
// CHECK-NEXT: %[[M:.*]] = "builtin.unrealized_conversion_cast"(%[[L]]) : (!reg) -> i64
// CHECK-NEXT: %[[N:.*]] = "builtin.unrealized_conversion_cast"([[D]]) : (i42) -> !reg
// CHECK-NEXT: %[[O:.*]] = "riscv.slli"(%[[N]]) <{"value" = 22 : i64}> : (!reg) -> !reg
// CHECK-NEXT: %[[P:.*]] = "riscv.srai"(%[[O]]) <{"value" = 22 : i64}> : (!reg) -> !reg
// CHECK-NEXT: %[[Q:.*]] = "builtin.unrealized_conversion_cast"(%[[P]]) : (!reg) -> i54

}) : () -> ()
}) : () -> ()

12 changes: 12 additions & 0 deletions Test/Passes/InstructionSelection/RISCV64/sext_invalid.mlir
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// RUN: veir-opt %s -p=isel-riscv64 | filecheck %s

"builtin.module"() ({
"func.func"() ({
^bb0(%a: i128, %b : i16):
%sexta = "llvm.sext"(%a) : (i128) -> i16
// CHECK: %{{.*}} = "llvm.sext"(%{{.*}}) : (i128) -> i16
%sextb = "llvm.sext"(%b) : (i16) -> i8
// CHECK: %{{.*}} = "llvm.sext"(%{{.*}}) : (i16) -> i8
}) : () -> ()
}) : () -> ()

23 changes: 23 additions & 0 deletions Test/Passes/InstructionSelection/RISCV64/trunc.mlir
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
// RUN: veir-opt %s -p=isel-riscv64 | filecheck %s

"builtin.module"() ({
"func.func"() ({
^bb0(%a: i8, %b: i16, %c: i32, %d: i42):
%trunca = "llvm.trunc"(%a) : (i8) -> i4
%truncb = "llvm.trunc"(%b) : (i16) -> i13
%truncc = "llvm.trunc"(%c) : (i32) -> i8
%sexdt = "llvm.trunc"(%d) : (i42) -> i37

// CHECK: ^{{.*}}([[A:.*]] : i8, [[B:.*]] : i16, [[C:.*]] : i32, [[D:.*]] : i42):
// CHECK-NEXT: %[[E:.*]] = "builtin.unrealized_conversion_cast"([[A]]) : (i8) -> !reg
// CHECK-NEXT: %[[F:.*]] = "builtin.unrealized_conversion_cast"(%[[E]]) : (!reg) -> i4
// CHECK-NEXT: %[[H:.*]] = "builtin.unrealized_conversion_cast"([[B]]) : (i16) -> !reg
// CHECK-NEXT: %[[I:.*]] = "builtin.unrealized_conversion_cast"(%[[H]]) : (!reg) -> i13
// CHECK-NEXT: %[[K:.*]] = "builtin.unrealized_conversion_cast"([[C]]) : (i32) -> !reg
// CHECK-NEXT: %[[L:.*]] = "builtin.unrealized_conversion_cast"(%[[K]]) : (!reg) -> i8
// CHECK-NEXT: %[[N:.*]] = "builtin.unrealized_conversion_cast"([[D]]) : (i42) -> !reg
// CHECK-NEXT: %[[Q:.*]] = "builtin.unrealized_conversion_cast"(%[[N]]) : (!reg) -> i37

}) : () -> ()
}) : () -> ()

12 changes: 12 additions & 0 deletions Test/Passes/InstructionSelection/RISCV64/trunc_invalid.mlir
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// RUN: veir-opt %s -p=isel-riscv64 | filecheck %s

"builtin.module"() ({
"func.func"() ({
^bb0(%a: i128, %b : i16):
%trunca = "llvm.trunc"(%a) : (i128) -> i16
// CHECK: %{{.*}} = "llvm.trunc"(%{{.*}}) : (i128) -> i16
%truncb = "llvm.trunc"(%b) : (i16) -> i32
// CHECK: %{{.*}} = "llvm.trunc"(%{{.*}}) : (i16) -> i32
}) : () -> ()
}) : () -> ()

28 changes: 28 additions & 0 deletions Test/Passes/InstructionSelection/RISCV64/zext.mlir
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
// RUN: veir-opt %s -p=isel-riscv64 | filecheck %s

"builtin.module"() ({
"func.func"() ({
^bb0(%a: i8, %b: i16, %c: i32, %d: i42):
%zexta = "llvm.zext"(%a) : (i8) -> i16
%zextb = "llvm.zext"(%b) : (i16) -> i32
%zextc = "llvm.zext"(%c) : (i32) -> i64
%sexdt = "llvm.zext"(%d) : (i42) -> i54

// CHECK: ^{{.*}}([[A:.*]] : i8, [[B:.*]] : i16, [[C:.*]] : i32, [[D:.*]] : i42):
// CHECK-NEXT: %[[E:.*]] = "builtin.unrealized_conversion_cast"([[A]]) : (i8) -> !reg
// CHECK-NEXT: %[[F:.*]] = "riscv.zextb"(%[[E]]) : (!reg) -> !reg
// CHECK-NEXT: %[[G:.*]] = "builtin.unrealized_conversion_cast"(%[[F]]) : (!reg) -> i16
// CHECK-NEXT: %[[H:.*]] = "builtin.unrealized_conversion_cast"([[B]]) : (i16) -> !reg
// CHECK-NEXT: %[[I:.*]] = "riscv.zexth"(%[[H]]) : (!reg) -> !reg
// CHECK-NEXT: %[[J:.*]] = "builtin.unrealized_conversion_cast"(%[[I]]) : (!reg) -> i32
// CHECK-NEXT: %[[K:.*]] = "builtin.unrealized_conversion_cast"([[C]]) : (i32) -> !reg
// CHECK-NEXT: %[[L:.*]] = "riscv.zextw"(%[[K]]) : (!reg) -> !reg
// CHECK-NEXT: %[[M:.*]] = "builtin.unrealized_conversion_cast"(%[[L]]) : (!reg) -> i64
// CHECK-NEXT: %[[N:.*]] = "builtin.unrealized_conversion_cast"([[D]]) : (i42) -> !reg
// CHECK-NEXT: %[[O:.*]] = "riscv.slli"(%[[N]]) <{"value" = 22 : i64}> : (!reg) -> !reg
// CHECK-NEXT: %[[P:.*]] = "riscv.srli"(%[[O]]) <{"value" = 22 : i64}> : (!reg) -> !reg
// CHECK-NEXT: %[[Q:.*]] = "builtin.unrealized_conversion_cast"(%[[P]]) : (!reg) -> i54

}) : () -> ()
}) : () -> ()

12 changes: 12 additions & 0 deletions Test/Passes/InstructionSelection/RISCV64/zext_invalid.mlir
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// RUN: veir-opt %s -p=isel-riscv64 | filecheck %s

"builtin.module"() ({
"func.func"() ({
^bb0(%a: i128, %b : i16):
%zexta = "llvm.zext"(%a) : (i128) -> i16
// CHECK: %{{.*}} = "llvm.zext"(%{{.*}}) : (i128) -> i16
%zextb = "llvm.zext"(%b) : (i16) -> i8
// CHECK: %{{.*}} = "llvm.zext"(%{{.*}}) : (i16) -> i8
}) : () -> ()
}) : () -> ()

138 changes: 137 additions & 1 deletion Veir/Passes/InstructionSelection/RISCV64.lean
Original file line number Diff line number Diff line change
Expand Up @@ -397,14 +397,150 @@ def urem (rewriter: PatternRewriter OpCode) (op: OperationPtr) :
#[] #[] () (some $ .before op) (by sorry) (by simp) (by simp) sorry
rewriter.replaceOp op castOp sorry sorry sorry

set_option warn.sorry false in
/--
llvm.sext %x i8 to iY -> riscv.sextb %x
llvm.sext %x i16 to iY -> riscv.sexth %x
llvm.sext %x i32 to iY -> riscv.sextw %x

For every other width:
llvm.sext %x iX to iY-> riscv.srai (riscv.slli %x (64 - X)) (64 - X)
-/
def sext (rewriter: PatternRewriter OpCode) (op: OperationPtr) :
Option (PatternRewriter OpCode) := do
let some (operand, _) := matchSext op rewriter.ctx | return rewriter
/- Only support extensions fron `iX` to `iY` where both `X < 64` and `Y < 64`. -/
let .integerType opType := (operand.getType! rewriter.ctx).val | return rewriter
if 64 < opType.bitwidth then return rewriter
let type := ((op.getResult 0).get! rewriter.ctx).type
let .integerType retType := type.val | rewriter
if 64 < retType.bitwidth then return rewriter
/- Instruction is illegal if return type is smaller than operand type.
TODO: this should be verified by `veir-opt` even before the pass starts. -/
if retType.bitwidth ≤ opType.bitwidth then return rewriter
/- First, cast the operand to registers -/
let (rewriter, opCastOp) ← rewriter.createOp .builtin_unrealized_conversion_cast #[RegisterType.mk] #[operand]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
dbg_trace "width = {opType.bitwidth}"
let (rewriter, retOp) ← match opType.bitwidth with
| 8 =>
let (rewriter, retOp) ← rewriter.createOp .riscv_sextb #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
pure (rewriter, retOp)
| 16 =>
let (rewriter, retOp) ← rewriter.createOp .riscv_sexth #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
pure (rewriter, retOp)
| 32 =>
let (rewriter, retOp) ← rewriter.createOp .riscv_sextw #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
dbg_trace "matched with width 32"
pure (rewriter, retOp)
| _ =>
let c := RISCVImmediateProperties.mk (IntegerAttr.mk (64 - opType.bitwidth) (IntegerType.mk 64))
let (rewriter, slliOp) ← rewriter.createOp .riscv_slli #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] c (some $ .before op) sorry (by simp) (by simp) sorry
let (rewriter, retOp) ← rewriter.createOp .riscv_srai #[RegisterType.mk] #[slliOp.getResult 0]
#[] #[] c (some $ .before op) sorry (by simp) (by simp) sorry
pure (rewriter, retOp)
/- Cast back result for type consistency-/
let (rewriter, castOp) ← rewriter.createOp .builtin_unrealized_conversion_cast #[type] #[retOp.getResult 0]
#[] #[] () (some $ .before op) (by sorry) (by simp) (by simp) sorry
rewriter.replaceOp op castOp sorry sorry sorry

set_option warn.sorry false in
/--
llvm.zext %x iX to iY where X ≤ 12 and X ≠ 8 -> riscv.andi %x (2 ^ X - 1)
e.g. llvm.zext %x i2 to iY -> riscv.andi %x 3
llvm.zext %x i3 to iY -> riscv.andi %x 7
...
llvm.zext %x i11 to iY -> riscv.andi %x 2047

llvm.zext %x i8 to iY -> riscv.sextb %x
llvm.zext %x i16 to iY -> riscv.zexth %x
llvm.zext %x i32 to iY -> riscv.zextw %x

For every other width:
llvm.zext %x iX to iY-> riscv.srli (riscv.slli %x (64 - X)) (64 - X)
-/
def zext (rewriter: PatternRewriter OpCode) (op: OperationPtr) :
Option (PatternRewriter OpCode) := do
let some (operand, _) := matchZext op rewriter.ctx | return rewriter
/- Only support extensions fron `iX` to `iY` where both `X < 64` and `Y < 64`. -/
let .integerType opType := (operand.getType! rewriter.ctx).val | return rewriter
if 64 < opType.bitwidth then return rewriter
let type := ((op.getResult 0).get! rewriter.ctx).type
let .integerType retType := type.val | rewriter
if 64 < retType.bitwidth then return rewriter
/- Instruction is illegal if return type is smaller than operand type.
TODO: this should be verified by `veir-opt` even before the pass starts. -/
if retType.bitwidth ≤ opType.bitwidth then return rewriter
/- First, cast the operand to registers -/
let (rewriter, opCastOp) ← rewriter.createOp .builtin_unrealized_conversion_cast #[RegisterType.mk] #[operand]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
let (rewriter, retOp) ← match opType.bitwidth with
| 8 =>
let (rewriter, retOp) ← rewriter.createOp .riscv_zextb #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
pure (rewriter, retOp)
| 16 =>
let (rewriter, retOp) ← rewriter.createOp .riscv_zexth #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
pure (rewriter, retOp)
| 32 =>
let (rewriter, retOp) ← rewriter.createOp .riscv_zextw #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
pure (rewriter, retOp)
| _ =>
if opType.bitwidth < 12 then
let c := RISCVImmediateProperties.mk (IntegerAttr.mk (2 ^ opType.bitwidth - 1) (IntegerType.mk 64))
let (rewriter, retOp) ← rewriter.createOp .riscv_andi #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] c (some $ .before op) sorry (by simp) (by simp) sorry
pure (rewriter, retOp)
else
let c := RISCVImmediateProperties.mk (IntegerAttr.mk (64 - opType.bitwidth) (IntegerType.mk 64))
let (rewriter, slliOp) ← rewriter.createOp .riscv_slli #[RegisterType.mk] #[opCastOp.getResult 0]
#[] #[] c (some $ .before op) sorry (by simp) (by simp) sorry
let (rewriter, retOp) ← rewriter.createOp .riscv_srli #[RegisterType.mk] #[slliOp.getResult 0]
#[] #[] c (some $ .before op) sorry (by simp) (by simp) sorry
pure (rewriter, retOp)
/- Cast back result for type consistency-/
let (rewriter, castOp) ← rewriter.createOp .builtin_unrealized_conversion_cast #[type] #[retOp.getResult 0]
#[] #[] () (some $ .before op) (by sorry) (by simp) (by simp) sorry
rewriter.replaceOp op castOp sorry sorry sorry

set_option warn.sorry false in
/--
llvm.trunc %x iX to iY -> builtin_unrealized_conversion_cast (!reg) : iY
-/
def trunc (rewriter: PatternRewriter OpCode) (op: OperationPtr) :
Option (PatternRewriter OpCode) := do
let some (operand, _) := matchTrunc op rewriter.ctx | return rewriter
/- Only support extensions fron `iX` to `iY` where both `X < 64` and `Y < 64`. -/
let .integerType opType := (operand.getType! rewriter.ctx).val | return rewriter
if 64 < opType.bitwidth then return rewriter
let type := ((op.getResult 0).get! rewriter.ctx).type
let .integerType retType := type.val | rewriter
if 64 < retType.bitwidth then return rewriter
/- Instruction is illegal if return type is smaller than operand type.
TODO: this should be verified by `veir-opt` even before the pass starts. -/
if opType.bitwidth ≤ retType.bitwidth then return rewriter
/- First, cast the operand to registers -/
let (rewriter, opCastOp) ← rewriter.createOp .builtin_unrealized_conversion_cast #[RegisterType.mk] #[operand]
#[] #[] () (some $ .before op) sorry (by simp) (by simp) sorry
/- Then, cast register to expected output width. -/
let (rewriter, castOp) ← rewriter.createOp .builtin_unrealized_conversion_cast #[type] #[opCastOp.getResult 0]
#[] #[] () (some $ .before op) (by sorry) (by simp) (by simp) sorry
rewriter.replaceOp op castOp sorry sorry sorry

/-! # Pass implementation -/

set_option warn.sorry false in
def ISelPass.impl (ctx : { ctx' : IRContext OpCode // ctx'.WellFormed }) (op : OperationPtr)
(_ : op.InBounds ctx.val) :
ExceptT String IO { ctx' : IRContext OpCode // ctx'.WellFormed } := do
let pattern := RewritePattern.GreedyRewritePattern #[constant, add, and, ashr, icmp, or, xor, mul,
sdiv, udiv, srem, urem]
sdiv, udiv, srem, urem, sext, zext, trunc]
match RewritePattern.applyInContext pattern ctx ctx.property.inBounds with
| none => throw "Error while applying pattern rewrites"
| some ctx => pure ⟨ctx, sorry⟩
Expand Down
12 changes: 12 additions & 0 deletions Veir/Passes/Matching.lean
Original file line number Diff line number Diff line change
Expand Up @@ -100,3 +100,15 @@ def matchSrem (op : OperationPtr) (ctx : IRContext OpCode) : Option (ValuePtr ×
def matchUrem (op : OperationPtr) (ctx : IRContext OpCode) : Option (ValuePtr × ValuePtr × propertiesOf .llvm_urem) := do
let (op, properties) ← matchOp op ctx .llvm_urem 2
return (op[0]!, op[1]!, properties)

def matchSext (op : OperationPtr) (ctx : IRContext OpCode) : Option (ValuePtr × propertiesOf .llvm_sext) := do
let (op, properties) ← matchOp op ctx .llvm_sext 1
return (op[0]!, properties)

def matchTrunc (op : OperationPtr) (ctx : IRContext OpCode) : Option (ValuePtr × propertiesOf .llvm_trunc) := do
let (op, properties) ← matchOp op ctx .llvm_trunc 1
return (op[0]!, properties)

def matchZext (op : OperationPtr) (ctx : IRContext OpCode) : Option (ValuePtr × propertiesOf .llvm_zext) := do
let (op, properties) ← matchOp op ctx .llvm_zext 1
return (op[0]!, properties)
Loading