MIR: relax requirement that slice backing allocations must be the same size when applying overrides

intTests/test2242_2243/Makefile

@@ -0,0 +1,5 @@
+all: ;
+clean:
+	sh ./test.sh clean
+
+.PHONY: all clean

intTests/test2301/.gitignore

@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff

intTests/test2301/Makefile

@@ -0,0 +1,5 @@
+all: ;
+clean:
+	sh ./test.sh clean
+
+.PHONY: all clean

intTests/test2620/.gitignore

@@ -0,0 +1,2 @@
+libtest.rlib
+libtest.mir

intTests/test2620/Makefile

@@ -0,0 +1,2 @@
+MIR_SRCS=test
+include ../support/mir-blobs.mk

intTests/test2620/test.linked-mir.json.FROM

@@ -0,0 +1,9 @@
+versions
+   rustc 1.91.0-nightly (02c7b1a7a 2025-09-13)
+   mir-json 0.1.0 (JSON schema version 9)
+   Rust toolchain nightly-2025-09-14
+   mir-json mtime: Mar 23 11:35:42 2026
+   mir-json version from cargo: mir-json v0.1.0
+   probable mir-json commit: 71700ee8a69e1b7d84f4eed7cbd43373b29d4373 from Tue Mar 17 13:41:39 2026 and/or Tue Mar 17 13:41:39 2026
+versions-notes
+   Generated by update-from.sh version 1

intTests/test2620/test.rs

@@ -0,0 +1,36 @@
+fn f(_: &[u8]) {}
+
+pub fn g(a: [u8; 2]) {
+    f(&a)
+}
+
+pub fn h(a: [u8; 5]) {
+    f(&a[0..2])
+}
+
+pub fn i(a: [u8; 5]) {
+    f(&a[3..5])
+}
+
+fn f_u32(_: &[u32]) {}
+
+pub fn h_u32(a: [u32; 5]) {
+    f_u32(&a[0..2])
+}
+
+// PRECONDITION: `a` must have at least two elements.
+fn tup(a: &[u8]) -> (u8, u8) {
+    (a[0], a[1])
+}
+
+pub fn g1(a: [u8; 5]) -> (u8, u8) {
+    tup(&a[0..2])
+}
+
+pub fn g2(a: [u8; 5]) -> (u8, u8) {
+    tup(&a)
+}
+
+pub fn g3(a: [u8; 5]) -> (u8, u8) {
+    tup(&a[1..3])
+}

intTests/test2620/test.saw

@@ -0,0 +1,76 @@
+enable_experimental;
+
+let f_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u8);
+    a_ref <- mir_ref_of (mir_term a_array);
+    mir_execute_func [mir_slice_value a_ref];
+};
+
+let f_spec_len3 = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 3 mir_u8);
+    a_ref <- mir_ref_of (mir_term a_array);
+    mir_execute_func [mir_slice_value a_ref];
+};
+
+let g_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u8);
+    mir_execute_func [mir_term a_array];
+};
+
+let h_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
+    mir_execute_func [mir_term a_array];
+};
+
+let i_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
+    mir_execute_func [mir_term a_array];
+};
+
+let f_u32_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u32);
+    a_ref <- mir_ref_of (mir_term a_array);
+    mir_execute_func [mir_slice_value a_ref];
+};
+
+let h_u32_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u32);
+    mir_execute_func [mir_term a_array];
+};
+
+m <- mir_load_module "test.linked-mir.json";
+
+f_ov <- mir_verify m "test::f" [] false f_spec z3;
+mir_verify m "test::g" [f_ov] false g_spec z3;
+mir_verify m "test::h" [f_ov] false h_spec z3;
+mir_verify m "test::i" [f_ov] false i_spec z3;
+f_u32_ov <- mir_verify m "test::f_u32" [] false f_u32_spec z3;
+mir_verify m "test::h_u32" [f_u32_ov] false h_u32_spec z3;
+f_ov_len3 <- mir_verify m "test::f" [] false f_spec_len3 z3;
+fails (mir_verify m "test::h" [f_ov_len3] false h_spec z3);
+
+let tup_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u8);
+    a_ref <- mir_ref_of (mir_term a_array);
+    mir_execute_func [mir_slice_value a_ref];
+    mir_return (mir_term {{ (a_array @ 0, a_array @ 1) }});
+};
+
+let g1_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
+    mir_execute_func [mir_term a_array];
+    mir_return (mir_term {{ (a_array @ 0, a_array @ 1) }});
+};
+
+let g3_spec = do {
+    a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
+    mir_execute_func [mir_term a_array];
+    mir_return (mir_term {{ (a_array @ 1, a_array @ 2) }});
+};
+
+tup_ov <- mir_verify m "test::tup" [] false tup_spec z3;
+mir_verify m "test::g1" [tup_ov] false g1_spec z3;
+mir_verify m "test::g2" [tup_ov] false g1_spec z3;
+
+mir_verify m "test::g3" [tup_ov] false g3_spec z3;
+fails (mir_verify m "test::g3" [tup_ov] false g1_spec z3);

intTests/test2620/test.sh

@@ -0,0 +1,3 @@
+#!/bin/sh
+SAW=${SAW:-saw}
+${SAW} test.saw

intTests/test2780/.gitignore

@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff

intTests/test2780/Makefile

@@ -0,0 +1,5 @@
+all: ;
+clean:
+	sh ./test.sh clean
+
+.PHONY: all clean

intTests/test2843/Makefile

@@ -0,0 +1,5 @@
+all: ;
+clean:
+	sh ./test.sh clean
+
+.PHONY: all clean

intTests/test2939/Makefile

@@ -0,0 +1,5 @@
+all: ;
+clean:
+	sh ./test.sh clean
+
+.PHONY: all clean

intTests/test_beta_reduce_term/.gitignore

@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff

intTests/test_sawcore_type_errors/.gitignore

@@ -0,0 +1,3 @@
+*.rawlog
+*.log
+*.diff

intTests/test_yosys_cells/.gitignore

@@ -0,0 +1,2 @@
+test.ys
+test.log

saw-central/src/SAWCentral/Crucible/MIR/Override.hs

@@ -1562,17 +1562,39 @@ matchArg opts sc cc cs prepost md = go False []
              Ctx.Empty Ctx.:> Crucible.RV actualArrRef Ctx.:> Crucible.RV actualStartSym <-
                liftIO $ Mir.mirRef_peelIndexMA bak iTypes actualSliceRef arrElemSize
 
+             Just actualStartBV <- pure $ W4.asBV actualStartSym
+             let actualStart :: Int
+                 actualStart = fromInteger $ BV.asUnsigned actualStartBV
+
+             let -- Read the full aggregate from the base array reference,
+                 -- split it at the actual start offset, resize to the
+                 -- expected slice length, and create a const reference
+                 -- containing only the correctly sliced elements.
+                 mkSlicedRef :: Int -> OverrideMatcher MIR w (Mir.MirReferenceMux Sym)
+                 mkSlicedRef expectedSliceLen = do
+                   globals <- OM $ use overrideGlobals
+                   fullAgg <- tryMirOperation $
+                     Mir.readMirRefMA bak globals iTypes Mir.MirAggregateRepr actualArrRef
+                   let off = fromIntegral actualStart * arrElemSize
+                   (_, rightAgg) <- case Mir.mirAggregate_split off fullAgg of
+                     Left err -> panic "matchArg" ["mirAggregate_split: " <> Text.pack err]
+                     Right result -> pure result
+                   let slicedAgg = Mir.resizeMirAggregate rightAgg
+                         (fromIntegral expectedSliceLen * arrElemSize)
+                   pure $ Mir.newConstMirRef sym Mir.MirAggregateRepr slicedAgg
+
              let -- Match the expected array reference value against the actual
                  -- array reference value.
-                 matchSlice :: Mir.Ty -> SetupValue -> OverrideMatcher MIR w ()
-                 matchSlice expectedArrRefTy expectedArrRef = do
+                 matchSlice :: Mir.MirReferenceMux Sym -> Mir.Ty -> SetupValue -> OverrideMatcher MIR w ()
+                 matchSlice actualArrRef' expectedArrRefTy expectedArrRef = do
                    arrLen <- arrRefTyLen expectedArrRefTy
                    let actualArrTy = Mir.TyArray actualElemTy arrLen
                    let actualArrTpr = Mir.MirAggregateRepr
                    let actualArrRefTy = Mir.TyRef actualArrTy actualMutbl
                    let actualArrRefShp = RefShape actualArrRefTy actualArrTy actualMutbl actualArrTpr
+
                    go inCast []
-                     (MIRVal actualArrRefShp actualArrRef)
+                     (MIRVal actualArrRefShp actualArrRef')
                      expectedArrRef
 
              actualSliceInfo <- sliceRefTyToSliceInfo actualSliceRefTy
@@ -1587,9 +1609,10 @@ matchArg opts sc cc cs prepost md = go False []
                  -- matches that of the actual slice reference value.
                  expectedArrRefTy <- typeOfSetupValue cc tyenv nameEnv expectedArrRef
                  expectedSliceLen <- arrRefTyLen expectedArrRefTy
-                 unless (expectedSliceLen == actualSliceLen) fail_
+                 unless (expectedSliceLen <= actualSliceLen) fail_
+                 slicedRef <- mkSlicedRef expectedSliceLen
                  -- Match the reference values.
-                 matchSlice expectedArrRefTy expectedArrRef
+                 matchSlice slicedRef expectedArrRefTy expectedArrRef
                MirSetupSliceRange expectedSliceInfo expectedArrRef expectedStart expectedEnd -> do
                  -- Check that both the expected and actual values are the same
                  -- sort of slice.
@@ -1602,16 +1625,10 @@ matchArg opts sc cc cs prepost md = go False []
                  -- underlying array, so there is no need to check it here.
                  expectedArrRefTy <- typeOfSetupValue cc tyenv nameEnv expectedArrRef
                  let expectedSliceLen = expectedEnd - expectedStart
-                 unless (expectedSliceLen == actualSliceLen) fail_
-                 -- Check that the starting indices into the expected and actual
-                 -- arrays are the same.
-                 case W4.asBV actualStartSym of
-                   Just actualStartBV
-                     | expectedStart == fromInteger (BV.asUnsigned actualStartBV) ->
-                       pure ()
-                   _ -> fail_
-                 -- Match the reference values.
-                 matchSlice expectedArrRefTy expectedArrRef
+                 unless (expectedSliceLen <= actualSliceLen) fail_
+                 -- Check that the start index matches.
+                 unless (expectedStart == actualStart) fail_
+                 matchSlice actualArrRef expectedArrRefTy expectedArrRef
 
         ([], MIRVal (RefShape (Mir.TyRef _ _) _ _ xTpr) x, MS.SetupGlobal () name) -> do
           static <- findStatic colState name