Fix Z3 translation of ArraySlice and add fuzzing infrastructure.

xls/solvers/BUILD

@@ -158,10 +158,17 @@ cc_test(
         ":z3_ir_equivalence_testutils",
         "//xls/common:xls_gunit_main",
         "//xls/common/status:matchers",
+        "//xls/common/status:ret_check",
+        "//xls/interpreter:ir_interpreter",
         "//xls/ir",
+        "//xls/ir:bits",
+        "//xls/ir:events",
         "//xls/ir:function_builder",
         "//xls/ir:ir_test_base",
         "//xls/ir:value",
+        "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/status",
+        "@com_google_absl//absl/types:span",
         "@googletest//:gtest",
     ],
 )
@@ -211,11 +218,18 @@ cc_test(
         ":z3_ir_translator_matchers",
         ":z3_utils",
         "//xls/common:xls_gunit_main",
+        "//xls/common/fuzzing:fuzztest",
         "//xls/common/status:matchers",
+        "//xls/common/status:ret_check",
+        "//xls/common/status:status_macros",
+        "//xls/data_structures:inline_bitmap",
+        "//xls/data_structures:leaf_type_tree",
+        "//xls/fuzzer/ir_fuzzer:ir_fuzz_domain",
         "//xls/interpreter:ir_interpreter",
         "//xls/ir",
         "//xls/ir:bits",
         "//xls/ir:bits_ops",
+        "//xls/ir:events",
         "//xls/ir:format_preference",
         "//xls/ir:function_builder",
         "//xls/ir:ir_parser",
@@ -224,8 +238,18 @@ cc_test(
         "//xls/ir:source_location",
         "//xls/ir:value",
         "//xls/ir:value_builder",
+        "//xls/ir:value_flattening",
+        "//xls/ir:value_utils",
+        "//xls/passes:dfe_pass",
+        "//xls/passes:inlining_pass",
+        "//xls/passes:optimization_pass",
+        "//xls/passes:pass_base",
+        "@com_google_absl//absl/algorithm:container",
         "@com_google_absl//absl/cleanup",
         "@com_google_absl//absl/container:flat_hash_map",
+        "@com_google_absl//absl/container:flat_hash_set",
+        "@com_google_absl//absl/log",
+        "@com_google_absl//absl/log:check",
         "@com_google_absl//absl/status",
         "@com_google_absl//absl/status:status_matchers",
         "@com_google_absl//absl/strings",

xls/solvers/z3_ir_equivalence_testutils_test.cc

@@ -14,8 +14,17 @@
 
 #include "xls/solvers/z3_ir_equivalence_testutils.h"
 
+#include <cstdint>
+
 #include "gtest/gtest.h"
+#include "absl/container/flat_hash_map.h"
+#include "absl/status/status.h"
+#include "absl/types/span.h"
 #include "xls/common/status/matchers.h"
+#include "xls/common/status/ret_check.h"
+#include "xls/interpreter/ir_interpreter.h"
+#include "xls/ir/bits.h"
+#include "xls/ir/events.h"
 #include "xls/ir/function_builder.h"
 #include "xls/ir/ir_test_base.h"
 #include "xls/ir/nodes.h"
@@ -42,5 +51,47 @@ TEST_F(Z3IrEquivalenceTestutilsTest, EquivWithAssert) {
   XLS_ASSERT_OK(f->RemoveNode(add.node()));
 }
 
+class FunctionInterpreter : public IrInterpreter {
+ public:
+  using IrInterpreter::IrInterpreter;
+  absl::Status HandleParam(Param* param) override {
+    XLS_RET_CHECK(HasResult(param)) << param;
+    return absl::OkStatus();
+  }
+};
+
+TEST_F(Z3IrEquivalenceTestutilsTest, EquivArraySlice) {
+  auto p = CreatePackage();
+  FunctionBuilder fb(TestName(), p.get());
+  BValue x = fb.Param("x", p->GetArrayType(2, p->GetBitsType(4)));
+  BValue y = fb.Param("y", p->GetBitsType(4));
+  BValue eq_0 = fb.Eq(y, fb.Literal(UBits(0, 4)));
+  fb.ArrayIndex(x, {fb.Literal(UBits(0, 4))});
+  BValue element_1 = fb.ArrayIndex(x, {fb.Literal(UBits(1, 4))});
+  BValue end = fb.Array({element_1, element_1}, element_1.GetType());
+  BValue transformed = fb.Select(eq_0, /*on_true=*/x, /*on_false=*/end);
+  BValue res = fb.ArraySlice(x, y, 2);
+  XLS_ASSERT_OK_AND_ASSIGN(Function * f, fb.Build());
+  ScopedVerifyEquivalence sve(f);
+  // Exhaustively check all inputs for equivalence.
+  for (uint64_t x0 = 0; x0 < 16; ++x0) {
+    for (uint64_t x1 = 0; x1 < 16; ++x1) {
+      for (uint64_t y0 = 0; y0 < 16; ++y0) {
+        InterpreterEvents events;
+        XLS_ASSERT_OK_AND_ASSIGN(Value x_val, Value::UBitsArray({x0, x1}, 4));
+        absl::flat_hash_map<Node*, Value> node_values{
+            {x.node(), x_val}, {y.node(), Value(UBits(y0, 4))}};
+        FunctionInterpreter interp(&node_values, &events);
+        XLS_ASSERT_OK(f->Accept(&interp));
+        EXPECT_EQ(node_values.at(res.node()),
+                  node_values.at(transformed.node()))
+            << " @ [" << x0 << ", " << x1 << "], " << y;
+      }
+    }
+  }
+  XLS_ASSERT_OK(
+      res.node()->ReplaceImplicitUsesWith(transformed.node()).status());
+}
+
 }  // namespace
 }  // namespace xls::solvers::z3

xls/solvers/z3_ir_translator.cc

@@ -926,13 +926,21 @@ absl::Status IrTranslator::HandleArraySlice(ArraySlice* array_slice) {
   Z3_ast start_ast = GetValue(array_slice->start());
   ArrayType* input_type = array_slice->array()->GetType()->AsArrayOrDie();
   ArrayType result_type(array_slice->width(), input_type->element_type());
-  Z3_ast formatted_start_ast =
-      GetAsFormattedArrayIndex(ctx_, start_ast, input_type);
-
+  int64_t min_offset_bits = Bits::MinBitCountUnsigned(array_slice->width());
+  // Make sure we don't overflow.
+  int64_t offset_width =
+      1 + std::max<int64_t>(
+              min_offset_bits,
+              Z3_get_bv_sort_size(ctx_, Z3_get_sort(ctx_, start_ast)));
+  Z3_sort index_sort = Z3_mk_bv_sort(ctx_, offset_width);
+  Z3_ast start_ext = Z3_mk_zero_ext(
+      ctx_,
+      offset_width - Z3_get_bv_sort_size(ctx_, Z3_get_sort(ctx_, start_ast)),
+      start_ast);
   std::vector<Z3_ast> elements;
   for (uint64_t i = 0; i < array_slice->width(); ++i) {
-    Z3_ast i_ast = GetAsFormattedArrayIndex(ctx_, i, input_type);
-    Z3_ast index_ast = Z3_mk_bvadd(ctx_, i_ast, formatted_start_ast);
+    Z3_ast i_ast = Z3_mk_int64(ctx_, i, index_sort);
+    Z3_ast index_ast = Z3_mk_bvadd(ctx_, start_ext, i_ast);
     elements.push_back(GetArrayElement(input_type, array_ast, index_ast));
   }