Verify that next nodes have values with the right type.

PiperOrigin-RevId: 671933270
google · Sep 7, 2024 · 0e54fa0 · 0e54fa0
1 parent 27cd4eb
commit 0e54fa0
Show file tree

Hide file tree

Showing 3 changed files with 50 additions and 1 deletion.
diff --git 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
@@ -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<Next>(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<Next>(SourceInfo(), s.node(),
+                                     // This shouldn't verify!
+                                     lit0.node(), pred.node())
+                    .status());
+  EXPECT_THAT(pb.function()->MakeNode<Next>(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
@@ -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<Param>()));
-    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));
   }