119 lines · cpp
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-exception6//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([&](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 hex40 attr = BitVectorAttr::get(&context, "#b01011010");41 ASSERT_EQ(attr.getValueAsString(), "#x5a");42 43 // A bit-width not divisible by 4 is always printed in binary44 // Also, make sure leading zeros are printed45 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([&](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([&](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 [&](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([&](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} // namespace119