diff --git a/xls/ir/BUILD b/xls/ir/BUILD index d7237abf20..31f4852481 100644 --- a/xls/ir/BUILD +++ b/xls/ir/BUILD @@ -941,10 +941,13 @@ cc_test( name = "verifier_test", srcs = ["verifier_test.cc"], deps = [ + ":bits", ":channel", ":function_builder", ":ir", ":ir_test_base", + ":source_location", + ":value", ":verifier", "//xls/common:xls_gunit_main", "//xls/common/status:matchers", diff --git a/xls/ir/verifier_test.cc b/xls/ir/verifier_test.cc index 230871131c..1649b81d8d 100644 --- a/xls/ir/verifier_test.cc +++ b/xls/ir/verifier_test.cc @@ -24,10 +24,14 @@ #include "absl/strings/substitute.h" #include "absl/types/span.h" #include "xls/common/status/matchers.h" +#include "xls/ir/bits.h" #include "xls/ir/channel.h" #include "xls/ir/function_builder.h" #include "xls/ir/ir_test_base.h" +#include "xls/ir/nodes.h" #include "xls/ir/package.h" +#include "xls/ir/source_location.h" +#include "xls/ir/value.h" namespace xls { namespace { @@ -617,5 +621,45 @@ TEST_F(VerifierTest, MismatchedInterfaceChannelFlowControl) { "channels with different flow control"))); } +TEST_F(VerifierTest, NextNodeWithWrongType) { + Package package("p"); + + ProcBuilder pb("p", &package, /*should_verify=*/false); + BValue s = pb.StateElement("s", Value(UBits(0, 32))); + BValue pred = pb.UGt(s, pb.Literal(UBits(10, 32))); + BValue lit0_width_1 = pb.Literal(UBits(0, 1)); + // Can't use pb.Next() because it checks the type without the verifier before + // making the node. + EXPECT_THAT(pb.function()->MakeNode(SourceInfo(), s.node(), + // This shouldn't verify! + lit0_width_1.node(), pred.node()), + StatusIs(absl::StatusCode::kInternal, + AllOf(HasSubstr("to have type bits[32]"), + HasSubstr("has type bits[1]")))); +} + +TEST_F(VerifierTest, NextNodeWithWrongTypePredicate) { + Package package("p"); + + ProcBuilder pb("p", &package, /*should_verify=*/false); + BValue s = pb.StateElement("s", Value(UBits(0, 32))); + BValue pred = pb.UGt(s, pb.Literal(UBits(10, 32))); + // This shouldn't verify! + BValue not_pred = pb.ZeroExtend(pb.Not(pred), 32); + BValue lit0 = pb.Literal(UBits(0, 32)); + BValue s_plus_one = pb.Add(s, pb.Literal(UBits(1, 32))); + // Can't use pb.Next() because it checks the type. + XLS_ASSERT_OK(pb.function() + ->MakeNode(SourceInfo(), s.node(), + // This shouldn't verify! + lit0.node(), pred.node()) + .status()); + EXPECT_THAT(pb.function()->MakeNode(SourceInfo(), s.node(), + s_plus_one.node(), not_pred.node()), + StatusIs(absl::StatusCode::kInternal, + AllOf(HasSubstr("to have bit count 1:"), + HasSubstr("had 32 bits")))); +} + } // namespace } // namespace xls diff --git a/xls/ir/verify_node.cc b/xls/ir/verify_node.cc index da3bd7cd30..300120ebb1 100644 --- a/xls/ir/verify_node.cc +++ b/xls/ir/verify_node.cc @@ -918,7 +918,9 @@ class NodeChecker : public DfsVisitor { Proc* proc = next->function_base()->AsProcOrDie(); XLS_ASSIGN_OR_RETURN(int64_t index, proc->GetStateParamIndex(next->param()->As())); - return ExpectOperandHasType(next, /*operand_no=*/0, + XLS_RETURN_IF_ERROR(ExpectOperandHasType(next, /*operand_no=*/0, + proc->GetStateElementType(index))); + return ExpectOperandHasType(next, /*operand_no=*/1, // value is operand 1 proc->GetStateElementType(index)); }