1//===- AttributeTest.cpp - SMT attribute unit tests -----------------------===//
2//
3// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4// See https://llvm.org/LICENSE.txt for license information.
5// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6//
7//===----------------------------------------------------------------------===//
8
9#include "mlir/Dialect/SMT/IR/SMTAttributes.h"
10#include "mlir/Dialect/SMT/IR/SMTDialect.h"
11#include "mlir/Dialect/SMT/IR/SMTTypes.h"
12#include "gtest/gtest.h"
13
14using namespace mlir;
15using namespace smt;
16
17namespace {
18
19TEST(BitVectorAttrTest, MinBitWidth) {
20 MLIRContext context;
21 context.loadDialect<SMTDialect>();
22 Location loc(UnknownLoc::get(&context));
23
24 auto attr = BitVectorAttr::getChecked(loc, &context, UINT64_C(0), 0U);
25 ASSERT_EQ(attr, BitVectorAttr());
26 context.getDiagEngine().registerHandler(handler: [&](Diagnostic &diag) {
27 ASSERT_EQ(diag.str(), "bit-width must be at least 1, but got 0");
28 });
29}
30
31TEST(BitVectorAttrTest, ParserAndPrinterCorrect) {
32 MLIRContext context;
33 context.loadDialect<SMTDialect>();
34
35 auto attr = BitVectorAttr::get(&context, "#b1010");
36 ASSERT_EQ(attr.getValue(), APInt(4, 10));
37 ASSERT_EQ(attr.getType(), BitVectorType::get(&context, 4));
38
39 // A bit-width divisible by 4 is always printed in hex
40 attr = BitVectorAttr::get(&context, "#b01011010");
41 ASSERT_EQ(attr.getValueAsString(), "#x5a");
42
43 // A bit-width not divisible by 4 is always printed in binary
44 // Also, make sure leading zeros are printed
45 attr = BitVectorAttr::get(&context, "#b0101101");
46 ASSERT_EQ(attr.getValueAsString(), "#b0101101");
47
48 attr = BitVectorAttr::get(&context, "#x3c");
49 ASSERT_EQ(attr.getValueAsString(), "#x3c");
50
51 attr = BitVectorAttr::get(&context, "#x03c");
52 ASSERT_EQ(attr.getValueAsString(), "#x03c");
53}
54
55TEST(BitVectorAttrTest, ExpectedOneDigit) {
56 MLIRContext context;
57 context.loadDialect<SMTDialect>();
58 Location loc(UnknownLoc::get(&context));
59
60 auto attr =
61 BitVectorAttr::getChecked(loc, &context, static_cast<StringRef>("#b"));
62 ASSERT_EQ(attr, BitVectorAttr());
63 context.getDiagEngine().registerHandler(handler: [&](Diagnostic &diag) {
64 ASSERT_EQ(diag.str(), "expected at least one digit");
65 });
66}
67
68TEST(BitVectorAttrTest, ExpectedBOrX) {
69 MLIRContext context;
70 context.loadDialect<SMTDialect>();
71 Location loc(UnknownLoc::get(&context));
72
73 auto attr =
74 BitVectorAttr::getChecked(loc, &context, static_cast<StringRef>("#c0"));
75 ASSERT_EQ(attr, BitVectorAttr());
76 context.getDiagEngine().registerHandler(handler: [&](Diagnostic &diag) {
77 ASSERT_EQ(diag.str(), "expected either 'b' or 'x'");
78 });
79}
80
81TEST(BitVectorAttrTest, ExpectedHashtag) {
82 MLIRContext context;
83 context.loadDialect<SMTDialect>();
84 Location loc(UnknownLoc::get(&context));
85
86 auto attr =
87 BitVectorAttr::getChecked(loc, &context, static_cast<StringRef>("b0"));
88 ASSERT_EQ(attr, BitVectorAttr());
89 context.getDiagEngine().registerHandler(
90 handler: [&](Diagnostic &diag) { ASSERT_EQ(diag.str(), "expected '#'"); });
91}
92
93TEST(BitVectorAttrTest, OutOfRange) {
94 MLIRContext context;
95 context.loadDialect<SMTDialect>();
96 Location loc(UnknownLoc::get(&context));
97
98 auto attr1 = BitVectorAttr::getChecked(loc, &context, UINT64_C(2), 1U);
99 auto attr63 =
100 BitVectorAttr::getChecked(loc, &context, UINT64_C(3) << 62, 63U);
101 ASSERT_EQ(attr1, BitVectorAttr());
102 ASSERT_EQ(attr63, BitVectorAttr());
103 context.getDiagEngine().registerHandler(handler: [&](Diagnostic &diag) {
104 ASSERT_EQ(diag.str(),
105 "value does not fit in a bit-vector of desired width");
106 });
107}
108
109TEST(BitVectorAttrTest, GetUInt64Max) {
110 MLIRContext context;
111 context.loadDialect<SMTDialect>();
112 auto attr64 = BitVectorAttr::get(&context, UINT64_MAX, 64);
113 auto attr65 = BitVectorAttr::get(&context, UINT64_MAX, 65);
114 ASSERT_EQ(attr64.getValue(), APInt::getAllOnes(64));
115 ASSERT_EQ(attr65.getValue(), APInt::getAllOnes(64).zext(65));
116}
117
118} // namespace
119

source code of mlir/unittests/Dialect/SMT/AttributeTest.cpp