Skip to content

Commit

Permalink
UB: Add verifier for ub.match
Browse files Browse the repository at this point in the history
  • Loading branch information
math-fehr committed Jan 16, 2025
1 parent d9670e3 commit 459f55f
Showing 1 changed file with 26 additions and 0 deletions.
26 changes: 26 additions & 0 deletions xdsl_smt/dialects/ub.py
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,32 @@ def __init__(self, value: SSAValue):
regions=[value_region, ub_region],
)

def verify_(self):
assert isattr(self.value.type, UBOrType[Attribute])
if self.value_region.blocks[0].arg_types != (self.value.type.type,):
raise ValueError(
"Value region must have exactly one argument of type "
f"{self.value.type.type}, got {self.value_region.blocks[0].args}"
)
if len(self.ub_region.blocks[0].args) != 0:
raise ValueError("UB region must have no arguments")
if not isinstance(term_val := self.value_region.blocks[0].last_op, YieldOp):
raise ValueError(
f"Value region must end with a 'ub.yield' op, got {term_val}"
)
if not isinstance(term_ub := self.ub_region.blocks[0].last_op, YieldOp):
raise ValueError(f"UB region must end with a 'ub.yield' op, got {term_ub}")
if self.result_types != term_val.operand_types:
raise ValueError(
"Yielded types in value region must match the result types, "
f"got {term_val.operand_types} and {self.result_types}"
)
if self.result_types != term_ub.operand_types:
raise ValueError(
"Yielded types in UB region must match the result types, "
f"got {term_ub.operand_types} and {self.result_types}"
)


@irdl_op_definition
class YieldOp(IRDLOperation):
Expand Down

0 comments on commit 459f55f

Please sign in to comment.