Add mir_mux_values command

Fixes #2000.

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -637,6 +637,7 @@ substMethodSpec sc sm ms = do
         MS.SetupUnion v _ _ -> case v of {}
         MS.SetupGlobal _ _ -> return sv
         MS.SetupGlobalInitializer _ _ -> return sv
+        MS.SetupMux b c t f -> MS.SetupMux b <$> goTypedTerm c <*> goSetupValue t <*> goSetupValue f
 
     goSetupCondition (MS.SetupCond_Equal loc sv1 sv2) =
         MS.SetupCond_Equal loc <$> goSetupValue sv1 <*> goSetupValue sv2

intTests/test2000/Makefile

@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json

intTests/test2000/test.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:6:8: 6:13","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"pos":"test.rs:6:8: 6:24","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"4294967295"},"ty":"ty::u32"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"Lt"}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"kind":"Move"},"discr_span":"test.rs:6:8: 6:24 !test.rs:6:8: 6:24","kind":"SwitchInt","pos":"test.rs:6:8: 6:24 !test.rs:6:8: 6:24","switch_ty":"ty::bool","targets":["bb3","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"test.rs:7:12: 7:17","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:7:12: 7:19","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _5 + const 1_u32`, which would overflow","pos":"test.rs:7:12: 7:19","target":"bb2"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"test.rs:7:12: 7:19","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Deinit","pos":"test.rs:7:9: 7:20"},{"kind":"Assign","lhs":{"data":[{"kind":"Downcast","variant":0},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::0d08cc03e8faa6eb"}},"pos":"test.rs:7:9: 7:20","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}}},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::0d08cc03e8faa6eb"}},"pos":"test.rs:7:9: 7:20","variant_index":0}],"terminator":{"kind":"Goto","pos":"test.rs:6:5: 10:6","target":"bb4"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Deinit","pos":"test.rs:9:9: 9:29"},{"kind":"SetDiscriminant","lvalue":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::0d08cc03e8faa6eb"}},"pos":"test.rs:9:9: 9:29","variant_index":1}],"terminator":{"kind":"Goto","pos":"test.rs:6:5: 10:6","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:11:2: 11:2"}},"blockid":"bb4"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::0d08cc03e8faa6eb"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Tuple::7063e33f0dbc8a58"}]},"name":"test/059ac093::increment","return_ty":"ty::Adt::0d08cc03e8faa6eb","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"0"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::0d08cc03e8faa6eb"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::1a1eab9d9d698a9d"},"kind":"Constant"},"kind":"Call","pos":"test.rs:14:5: 14:17"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:15:2: 15:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::0d08cc03e8faa6eb"}]},"name":"test/059ac093::f","return_ty":"ty::Adt::0d08cc03e8faa6eb","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"4294967295"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::0d08cc03e8faa6eb"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::1a1eab9d9d698a9d"},"kind":"Constant"},"kind":"Call","pos":"test.rs:18:5: 18:24"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:19:2: 19:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Adt::0d08cc03e8faa6eb"}]},"name":"test/059ac093::g","return_ty":"ty::Adt::0d08cc03e8faa6eb","spread_arg":null}],"adts":[{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"test/059ac093::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"test/059ac093::Error","orig_substs":[],"repr_transparent":false,"size":0,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"test/059ac093::Error::Overflow"}]},{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::result::Result::_adt8c4e4dad4cfdd737[0]","orig_def_id":"core/73237d41::result::Result","orig_substs":["ty::u32","ty::Adt::c843e4c253dfdd59"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[{"name":"core/73237d41::result::Result::Ok::0","ty":"ty::u32"}],"inhabited":true,"name":"core/73237d41::result::Result::Ok"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::result::Result::Err::0","ty":"ty::Adt::c843e4c253dfdd59"}],"inhabited":true,"name":"core/73237d41::result::Result::Err"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/059ac093::increment","kind":"Item","substs":[]},"name":"test/059ac093::increment"},{"inst":{"def_id":"test/059ac093::f","kind":"Item","substs":[]},"name":"test/059ac093::f"},{"inst":{"def_id":"test/059ac093::g","kind":"Item","substs":[]},"name":"test/059ac093::g"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Adt::c843e4c253dfdd59","ty":{"kind":"Adt","name":"test/059ac093::Error::_adtb7803c2264daf0ec[0]","orig_def_id":"test/059ac093::Error","substs":[]}},{"name":"ty::Adt::0d08cc03e8faa6eb","ty":{"kind":"Adt","name":"core/73237d41::result::Result::_adt8c4e4dad4cfdd737[0]","orig_def_id":"core/73237d41::result::Result","substs":["ty::u32","ty::Adt::c843e4c253dfdd59"]}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::7063e33f0dbc8a58","ty":{"kind":"Tuple","tys":["ty::u32","ty::bool"]}},{"name":"ty::FnDef::1a1eab9d9d698a9d","ty":{"defid":"test/059ac093::increment","kind":"FnDef"}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}}],"roots":["test/059ac093::increment","test/059ac093::f","test/059ac093::g"]}

intTests/test2000/test.rs

@@ -0,0 +1,19 @@
+pub enum Error {
+    Overflow,
+}
+
+pub fn increment(count: u32) -> Result<u32, Error> {
+    if count < u32::MAX {
+        Ok(count+1)
+    } else {
+        Err(Error::Overflow)
+    }
+}
+
+pub fn f() -> Result<u32, Error> {
+    increment(0)
+}
+
+pub fn g() -> Result<u32, Error> {
+    increment(u32::MAX)
+}

intTests/test2000/test.saw

@@ -0,0 +1,34 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+
+let error_adt = mir_find_adt m "test::Error" [];
+let result_adt = mir_find_adt m "core::result::Result" [mir_u32, mir_adt error_adt];
+
+let increment_spec = do {
+  count <- mir_fresh_var "count" mir_u32;
+
+  mir_execute_func [mir_term count];
+
+  let ok  = mir_enum_value result_adt "Ok" [mir_term {{ count + 1 }}];
+  let err = mir_enum_value result_adt "Err" [mir_enum_value error_adt "Overflow" []];
+  let res = mir_mux_values {{ count < (2^^32 - 1) }} ok err;
+  mir_return res;
+};
+
+increment_ov <- mir_verify m "test::increment" [] false increment_spec z3;
+
+let f_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_enum_value result_adt "Ok" [mir_term {{ 1 : [32] }}]);
+};
+
+let g_spec = do {
+  mir_execute_func [];
+
+  mir_return (mir_enum_value result_adt "Err" [mir_enum_value error_adt "Overflow" []]);
+};
+
+mir_verify m "test::f" [increment_ov] false f_spec z3;
+mir_verify m "test::g" [increment_ov] false g_spec z3;

intTests/test2000/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -52,6 +52,7 @@ module SAWScript.Crucible.Common.MethodSpec
   , XSetupCast
   , XSetupUnion
   , XSetupGlobalInitializer
+  , XSetupMux
 
   , SetupValue(..)
   , SetupValueHas
@@ -242,6 +243,15 @@ ppSetupValue setupval = case setupval of
         absurd empty
   SetupGlobal _ nm -> PP.pretty ("global(" ++ nm ++ ")")
   SetupGlobalInitializer _ nm -> PP.pretty ("global_initializer(" ++ nm ++ ")")
+  SetupMux x c t f ->
+    case (ext, x) of
+      (LLVMExt, empty) ->
+        absurd empty
+      (JVMExt, empty) ->
+        absurd empty
+      (MIRExt, ()) ->
+        PP.pretty "mux" <>
+        PP.parens (ppTypedTerm c <> PP.comma PP.<+> ppSetupValue t <> PP.comma PP.<+> ppSetupValue f)
   where
     ext :: SAWExt ext
     ext = sawExt @ext

src/SAWScript/Crucible/Common/Setup/Value.hs

@@ -48,6 +48,7 @@ module SAWScript.Crucible.Common.Setup.Value
   , XSetupCast
   , XSetupUnion
   , XSetupGlobalInitializer
+  , XSetupMux
 
   , SetupValue(..)
   , SetupValueHas
@@ -132,6 +133,7 @@ type family XSetupGlobal ext
 type family XSetupCast ext
 type family XSetupUnion ext
 type family XSetupGlobalInitializer ext
+type family XSetupMux ext
 
 -- | From the manual: \"The SetupValue type corresponds to values that can occur
 -- during symbolic execution, which includes both 'Term' values, pointers, and
@@ -162,6 +164,16 @@ data SetupValue ext where
   -- | This represents the value of a global's initializer.
   SetupGlobalInitializer ::
     XSetupGlobalInitializer ext -> String -> SetupValue ext
+  -- | A mux of two 'SetupValue's based on a boolean-typed 'TypedTerm'.
+  SetupMux ::
+    XSetupMux ext ->
+    TypedTerm
+      {- ^ The conditional expression. Must be of Cryptol type @Bit@. -} ->
+    SetupValue ext
+      {- ^ The value to use if the conditional expression is true. -} ->
+    SetupValue ext
+      {- ^ The value to use if the conditional expression is false. -} ->
+    SetupValue ext
 
 -- | This constraint can be solved for any ext so long as '()', 'Void', and any
 --   other types used in the right-hand sides of extension field
@@ -181,6 +193,7 @@ type SetupValueHas (c :: Type -> Constraint) ext =
   , c (XSetupUnion ext)
   , c (XSetupGlobal ext)
   , c (XSetupGlobalInitializer ext)
+  , c (XSetupMux ext)
   )
 
 deriving instance (SetupValueHas Show ext) => Show (SetupValue ext)

src/SAWScript/Crucible/JVM/Override.hs

@@ -942,6 +942,7 @@ instantiateSetupValue sc s v =
     MS.SetupCast empty _              -> absurd empty
     MS.SetupUnion empty _ _           -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
+    MS.SetupMux empty _ _ _           -> absurd empty
   where
     doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
 

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -149,6 +149,7 @@ typeOfSetupValue _cc env _nameEnv val =
     MS.SetupCast empty _              -> absurd empty
     MS.SetupUnion empty _ _           -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
+    MS.SetupMux empty _ _ _           -> absurd empty
 
 lookupAllocIndex :: Map AllocIndex a -> AllocIndex -> a
 lookupAllocIndex env i =
@@ -183,6 +184,7 @@ resolveSetupVal cc env _tyenv _nameEnv val =
     MS.SetupCast empty _              -> absurd empty
     MS.SetupUnion empty _ _           -> absurd empty
     MS.SetupGlobalInitializer empty _ -> absurd empty
+    MS.SetupMux empty _ _ _           -> absurd empty
   where
     sym = cc^.jccSym
 

src/SAWScript/Crucible/JVM/Setup/Value.hs

@@ -87,6 +87,7 @@ type instance MS.XSetupField CJ.JVM = Void
 type instance MS.XSetupCast CJ.JVM = Void
 type instance MS.XSetupUnion CJ.JVM = Void
 type instance MS.XSetupGlobalInitializer CJ.JVM = Void
+type instance MS.XSetupMux CJ.JVM = Void
 
 type JIdent = String -- FIXME(huffman): what to put here?
 

src/SAWScript/Crucible/LLVM/Override.hs

@@ -1021,6 +1021,7 @@ matchPointsTos opts sc cc spec prepost = go False []
         SetupNull _                -> Set.empty
         SetupGlobal _ _            -> Set.empty
         SetupGlobalInitializer _ _ -> Set.empty
+        SetupMux empty _ _ _       -> absurd empty
 
 
 ------------------------------------------------------------------------
@@ -1197,6 +1198,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
          matchArg opts sc cc cs prepost md (Crucible.LLVMValInt blk off') expectedTy v
 
     (_, _, SetupGlobalInitializer () _) -> resolveAndMatch
+    (_, _, SetupMux empty _ _ _)        -> absurd empty
 
     (Crucible.LLVMValInt blk off, _, _) ->
       case expected of
@@ -2283,6 +2285,7 @@ instantiateSetupValue sc s v =
     SetupNull{}              -> return v
     SetupGlobal{}            -> return v
     SetupGlobalInitializer{} -> return v
+    SetupMux empty _ _ _     -> absurd empty
     SetupEnum  empty         -> absurd empty
     SetupTuple empty _       -> absurd empty
     SetupSlice empty         -> absurd empty

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -555,6 +555,9 @@ typeOfSetupValue cc env nameEnv val =
                           ]
             Right memTy -> return memTy
         Nothing -> throwError $ "resolveSetupVal: global not found: " ++ name
+
+    SetupMux empty _ _ _ ->
+      absurd empty
   where
     lc = ccTypeCtx cc
     dl = Crucible.llvmDataLayout lc
@@ -682,6 +685,8 @@ resolveSetupVal cc mem env tyenv nameEnv val =
           fail $ "resolveSetupVal: global has no initializer: " ++ name
         Nothing ->
           fail $ "resolveSetupVal: global not found: " ++ name
+    SetupMux empty _ _ _ ->
+      absurd empty
 
 
 -- | Like 'resolveSetupVal', but specifically geared towards the needs of

src/SAWScript/Crucible/LLVM/Setup/Value.hs

@@ -132,6 +132,7 @@ type instance Setup.XSetupCast (LLVM _) = L.Type
 type instance Setup.XSetupUnion (LLVM _) = ()
 type instance Setup.XSetupGlobal (LLVM _) = ()
 type instance Setup.XSetupGlobalInitializer (LLVM _) = ()
+type instance Setup.XSetupMux (LLVM _) = Void
 
 type instance Setup.TypeName (LLVM arch) = CL.Ident
 type instance Setup.ExtType (LLVM arch) = CL.MemType

src/SAWScript/Crucible/MIR/Builtins.hs

@@ -31,6 +31,8 @@ module SAWScript.Crucible.MIR.Builtins
     -- ** MIR slices
   , mir_slice_value
   , mir_slice_range_value
+    -- ** MIR muxing
+  , mir_mux_values
     -- ** MIR types
   , mir_adt
   , mir_array
@@ -758,6 +760,17 @@ mir_slice_range_value ::
 mir_slice_range_value arrRef start end =
   MS.SetupSlice (MirSetupSliceRange arrRef start end)
 
+-----
+-- MIR muxing
+-----
+
+mir_mux_values ::
+  TypedTerm ->
+  MS.SetupValue MIR ->
+  MS.SetupValue MIR ->
+  MS.SetupValue MIR
+mir_mux_values = MS.SetupMux ()
+
 -----
 -- Mir.Types
 -----

src/SAWScript/Crucible/MIR/Override.hs

@@ -904,6 +904,10 @@ instantiateSetupValue sc s v =
     MS.SetupCast empty _              -> absurd empty
     MS.SetupUnion empty _ _           -> absurd empty
     MS.SetupGlobalInitializer _ _     -> return v
+    MS.SetupMux x c t f               -> MS.SetupMux x
+                                           <$> doTerm c
+                                           <*> instantiateSetupValue sc s t
+                                           <*> instantiateSetupValue sc s f
   where
     doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t
 
@@ -1260,6 +1264,13 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
       staticInitMirVal <- findStaticInitializer cc static
       pred_ <- liftIO $ equalValsPred cc staticInitMirVal actual
       addAssert pred_ md =<< notEq
+    (_, _, MS.SetupMux () c t f) -> do
+      cPred <- liftIO $ resolveBoolTerm sym (ttTerm c)
+      withConditionalPred cPred $
+        matchArg opts sc cc cs prepost md actual expectedTy t
+      cNegPred <- liftIO $ W4.notPred sym cPred
+      withConditionalPred cNegPred $
+        matchArg opts sc cc cs prepost md actual expectedTy f
 
     (_, _, MS.SetupNull empty)                -> absurd empty
     (_, _, MS.SetupCast empty _)              -> absurd empty
@@ -1372,6 +1383,7 @@ matchPointsTos opts sc cc spec prepost = go False []
         MS.SetupCast empty _              -> absurd empty
         MS.SetupUnion empty _ _           -> absurd empty
         MS.SetupNull empty                -> absurd empty
+        MS.SetupMux _ _ t f               -> setupVars t <> setupVars f
 
     -- Compute the set of variable identifiers in a 'MirSetupEnum'
     setupEnum :: MirSetupEnum -> Set AllocIndex