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.

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

[SMT] Add bv2int op #8049

Merged
merged 5 commits into from
Jan 10, 2025
Merged

[SMT] Add bv2int op #8049

merged 5 commits into from
Jan 10, 2025

Conversation

TaoBi22
Copy link
Contributor

@TaoBi22 TaoBi22 commented Jan 9, 2025

Adds an operation to convert between SMT bitvectors and SMT integers. As discussed further in #8041, support for these operations varies between solvers - technically this one is outlined in the SMTLIB spec but AFAIU only to describe the semantics of other operations, rather than as something solvers are expected to implement, so I've made ExportSMTLIB error out on this one too since it's not really part of the spec for the language itself.

@TaoBi22 TaoBi22 requested a review from maerhart as a code owner January 9, 2025 15:45
include/circt/Dialect/SMT/SMTBitVectorOps.td Outdated Show resolved Hide resolved
include/circt/Dialect/SMT/SMTBitVectorOps.td Outdated Show resolved Hide resolved
include/circt/Dialect/SMT/SMTBitVectorOps.td Outdated Show resolved Hide resolved
include/circt/Dialect/SMT/SMTBitVectorOps.td Outdated Show resolved Hide resolved
include/circt/Dialect/SMT/SMTBitVectorOps.td Outdated Show resolved Hide resolved
include/circt/Dialect/SMT/SMTBitVectorOps.td Outdated Show resolved Hide resolved
integration_test/Dialect/SMT/basic.mlir Outdated Show resolved Hide resolved
lib/Target/ExportSMTLIB/ExportSMTLIB.cpp Outdated Show resolved Hide resolved
@TaoBi22 TaoBi22 merged commit c49c1c3 into llvm:main Jan 10, 2025
4 checks passed
lib/Dialect/SMT/CMakeLists.txt Show resolved Hide resolved
lib/Dialect/SMT/SMTOps.cpp Show resolved Hide resolved
Comment on lines +605 to 608
if (isa<smt::Int2BVOp, BV2IntOp>(op))
return op->emitError("operation not supported for SMTLIB emission");

return success();
Copy link
Member

Choose a reason for hiding this comment

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

I think just

  return op->emitError("operation not supported for SMTLIB emission");

should work instead of

    if (isa<smt::Int2BVOp, BV2IntOp>(op))
      return op->emitError("operation not supported for SMTLIB emission");

    return success();

to generically emit this error if we add new operations that we don't explicitly add support for in ExportSMTLIB (i.e., should be more robust)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Ah I see, sorry for the misunderstanding before!

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Just checked and this actually breaks all the ExportSMTLIB tests - I'm not super clear on the Visitor infrastructure so I'm not sure why yet, but from a brief scan it looks like getting rid of the condition causes the error to throw on the first non-ConstantLike op the export pass encounters.

include/circt/Dialect/SMT/SMTBitVectorOps.td Show resolved Hide resolved
include/circt/Dialect/SMT/SMTBitVectorOps.td Show resolved Hide resolved
@TaoBi22
Copy link
Contributor Author

TaoBi22 commented Jan 10, 2025

I'll push fixes to main, thanks!

TaoBi22 added a commit to TaoBi22/circt that referenced this pull request Jan 10, 2025
TaoBi22 added a commit that referenced this pull request Jan 10, 2025
TaoBi22 added a commit that referenced this pull request Jan 10, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants