Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Generic integer semantics #51

Open
wants to merge 5 commits into
base: main
Choose a base branch
from
Open

Generic integer semantics #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
a506334
Parametric int semantics
qaco Dec 12, 2024
847e122
First pass on reviews
qaco Dec 16, 2024
eac26c9
Simple equality in the refinement
qaco Dec 16, 2024
b609f81
Make pyright happy
qaco Dec 16, 2024
455f697
Hide unused return values
qaco Dec 16, 2024
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
6 changes: 3 additions & 3 deletions tests/filecheck/lower-memory-to-array/lower-get-fresh-id.mlir
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,9 @@
%block_id2, %memory3 = memory.get_fresh_block_id %memory2
%block_id3, %memory4 = memory.get_fresh_block_id %memory3

// CHECK: %block_id1 = "smt.int.constant"() {"value" = 0 : i64} : () -> !smt.int.int
// CHECK-NEXT: %block_id2 = "smt.int.constant"() {"value" = 1 : i64} : () -> !smt.int.int
// CHECK-NEXT: %block_id3 = "smt.int.constant"() {"value" = 2 : i64} : () -> !smt.int.int
// CHECK: %block_id1 = "smt.int.constant"() {"value" = 0 : ui128} : () -> !smt.int.int
// CHECK-NEXT: %block_id2 = "smt.int.constant"() {"value" = 1 : ui128} : () -> !smt.int.int
// CHECK-NEXT: %block_id3 = "smt.int.constant"() {"value" = 2 : ui128} : () -> !smt.int.int
Comment on lines -10 to +12
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll fix this in another PR, but actually we have the IntAttr attribute that can represent arbitrary bitwidth integers, it's probably better suited here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh ok nice



"test.op"(%block_id1, %block_id2, %block_id3, %memory4) : (!memory.block_id, !memory.block_id, !memory.block_id, !memory.memory) -> ()
18 changes: 11 additions & 7 deletions xdsl_smt/dialects/smt_int_dialect.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,11 @@
SMTLibSort,
SMTConversionCtx,
)
from .smt_dialect import BoolType
from xdsl.ir import SSAValue, Operation
from xdsl_smt.dialects import smt_dialect as smt
from xdsl.dialects.builtin import Signedness

LARGE_ENOUGH_INT_TYPE = IntegerType(128, Signedness.UNSIGNED)

_OpT = TypeVar("_OpT", bound=Operation)

Expand Down Expand Up @@ -58,16 +62,16 @@ def __init__(self, lhs: SSAValue, rhs: SSAValue):


class BinaryPredIntOp(IRDLOperation, Pure):
res: OpResult = result_def(BoolType)
res: OpResult = result_def(smt.BoolType)
lhs: Operand = operand_def(SMTIntType)
rhs: Operand = operand_def(SMTIntType)

def __init__(self, lhs: SSAValue, rhs: SSAValue):
super().__init__(result_types=[BoolType()], operands=[lhs, rhs])
super().__init__(result_types=[smt.BoolType()], operands=[lhs, rhs])

@classmethod
def get(cls: type[_BPOpT], lhs: SSAValue, rhs: SSAValue) -> _BPOpT:
return cls.create(result_types=[BoolType()], operands=[lhs, rhs])
return cls.create(result_types=[smt.BoolType()], operands=[lhs, rhs])


_UOpT = TypeVar("_UOpT", bound="UnaryIntOp")
Expand All @@ -91,11 +95,11 @@ class ConstantOp(IRDLOperation, Pure, SMTLibOp):
res: OpResult = result_def(SMTIntType)
value: IntegerAttr[IntegerType] = attr_def(IntegerAttr)

def __init__(self, value: int):
value_type = IntegerType(64)
def __init__(self, value: int | IntegerAttr[IntegerType]):
assert isinstance(value, int)
super().__init__(
result_types=[SMTIntType()],
attributes={"value": IntegerAttr(value, value_type)},
attributes={"value": IntegerAttr(value, LARGE_ENOUGH_INT_TYPE)},
)

def print_expr_to_smtlib(self, stream: IO[str], ctx: SMTConversionCtx):
Expand Down
38 changes: 13 additions & 25 deletions xdsl_smt/passes/load_parametric_int_semantics.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,35 +2,23 @@
from xdsl.passes import ModulePass
from xdsl.context import MLContext
from xdsl.dialects.builtin import ModuleOp
from xdsl.dialects import arith
from xdsl.dialects.builtin import IntegerType
from xdsl_smt.passes.lower_to_smt.smt_lowerer import SMTLowerer
from xdsl_smt.dialects import smt_int_dialect as smt_int
from xdsl_smt.semantics.arith_int_semantics import (
IntIntegerTypeSemantics,
IntConstantSemantics,
IntCmpiSemantics,
get_binary_ef_semantics,
get_div_semantics,
)
from xdsl_smt.semantics.generic_integer_proxy import IntegerProxy
from xdsl_smt.passes.lower_to_smt.smt_lowerer_loaders import load_int_semantics
from xdsl.pattern_rewriter import PatternRewriter


@dataclass(frozen=True)
class LoadIntSemanticsPass(ModulePass):
name = "load-int-semantics"

def apply(self, ctx: MLContext, op: ModuleOp) -> None:
semantics = {
arith.Constant: IntConstantSemantics(),
arith.Addi: get_binary_ef_semantics(smt_int.AddOp)(),
arith.Subi: get_binary_ef_semantics(smt_int.SubOp)(),
arith.Muli: get_binary_ef_semantics(smt_int.MulOp)(),
arith.Cmpi: IntCmpiSemantics(),
arith.DivUI: get_div_semantics(smt_int.DivOp)(),
arith.RemUI: get_div_semantics(smt_int.ModOp)(),
}
SMTLowerer.op_semantics = {**SMTLowerer.op_semantics, **semantics}
types = {
IntegerType: IntIntegerTypeSemantics(),
}
SMTLowerer.type_lowerers = {**SMTLowerer.type_lowerers, **types}
if op.body.first_block is None:
return
assert op.body.first_block
if op.body.first_block.first_op:
return
assert op.body.first_block.first_op
rewriter = PatternRewriter(op.body.first_block.first_op)
integer_proxy = IntegerProxy()
integer_proxy.build_pow2(rewriter)
load_int_semantics(integer_proxy)
44 changes: 42 additions & 2 deletions xdsl_smt/passes/lower_to_smt/smt_lowerer_loaders.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,17 @@
from xdsl.ir import Operation
from xdsl_smt.semantics.semantics import OperationSemantics
from xdsl.ir import Attribute, Operation
from xdsl.dialects import arith
from xdsl_smt.semantics.generic_integer_proxy import IntegerProxy
from xdsl_smt.semantics.arith_int_semantics import (
IntConstantSemantics,
get_binary_ef_semantics,
IntSelectSemantics,
IntCmpiSemantics,
IntAndISemantics,
get_div_semantics,
IntIntegerTypeSemantics,
IntIntegerAttrSemantics,
)
from xdsl_smt.semantics.semantics import OperationSemantics, AttributeSemantics
from xdsl_smt.dialects.transfer import (
AbstractValueType,
TransIntegerType,
Expand All @@ -23,6 +35,7 @@
func_to_smt_patterns,
transfer_to_smt_patterns,
)
from xdsl_smt.dialects import smt_int_dialect as smt_int


def load_vanilla_semantics_with_transfer(transfer_width: int):
Expand Down Expand Up @@ -60,3 +73,30 @@ def load_transfer_type_lowerer(transfer_width: int):
def load_dynamic_semantics(semantics: dict[type[Operation], OperationSemantics]):
SMTLowerer.dynamic_semantics_enabled = True
SMTLowerer.op_semantics = {**SMTLowerer.op_semantics, **semantics}


def load_int_semantics(integer_proxy: IntegerProxy):
semantics = {
arith.Constant: IntConstantSemantics(integer_proxy),
arith.Select: IntSelectSemantics(integer_proxy),
arith.Addi: get_binary_ef_semantics(smt_int.AddOp)(integer_proxy),
arith.Subi: get_binary_ef_semantics(smt_int.SubOp)(integer_proxy),
arith.Muli: get_binary_ef_semantics(smt_int.MulOp)(integer_proxy),
arith.Cmpi: IntCmpiSemantics(integer_proxy),
arith.AndI: IntAndISemantics(integer_proxy),
arith.DivUI: get_div_semantics(smt_int.DivOp)(integer_proxy),
arith.RemUI: get_div_semantics(smt_int.ModOp)(integer_proxy),
}
SMTLowerer.op_semantics = {**SMTLowerer.op_semantics, **semantics}
types = {
TransIntegerType: IntIntegerTypeSemantics(integer_proxy),
IntegerType: IntIntegerTypeSemantics(integer_proxy),
}
SMTLowerer.type_lowerers = {**SMTLowerer.type_lowerers, **types}
attribute_semantics: dict[type[Attribute], AttributeSemantics] = {
IntegerAttr: IntIntegerAttrSemantics()
}
SMTLowerer.attribute_semantics = {
**SMTLowerer.attribute_semantics,
**attribute_semantics,
}
Loading
Loading