Merge pull request #1955 from GaloisInc/T1859-mir_fresh_expanded_value

`mir_fresh_expanded_value`

doc/manual/manual.md

@@ -2650,6 +2650,19 @@ construct compound values:
 * `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given
   list of values as elements.
 
+To specify a compound value in which each element or field is symbolic, it
+would be possible, but tedious, to use a large number of `mir_fresh_var`
+invocations in conjunction with the commands above. However, the following
+function can simplify the common case where you want every element or field to
+have a fresh value:
+
+* `mir_fresh_expanded_value : String -> MIRType -> MIRSetup MIRValue`
+
+The `String` argument denotes a prefix to use when generating the names of
+fresh symbolic variables. The `MIRType` can be any type, with the exception of
+reference types (or compound types that contain references as elements or
+fields), which are not currently supported.
+
 ### MIR slices
 
 Slices are a unique form of compound type that is currently only used during

intTests/test_mir_fresh_expanded_value/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/test_mir_fresh_expanded_value/test.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::01bd9e2f4f30865e"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:6:20: 6:20"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/8e312bae::f","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:10:28: 10:28"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/8e312bae::h","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::cef0e4ed0a308aa2"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:8:26: 8:26"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/8e312bae::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::480389e29db14a3a"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:17:20: 17:20"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/8e312bae::i","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/8e312bae::S2::_adtb7803c2264daf0ec[0]","orig_def_id":"test/8e312bae::S2","orig_substs":[],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/8e312bae::S2::z","ty":"ty::u32"},{"name":"test/8e312bae::S2::w","ty":"ty::Ref::e028c0f25e8b6323"}],"inhabited":true,"name":"test/8e312bae::S2"}]},{"kind":{"kind":"Struct"},"name":"test/8e312bae::S1::_adtb7803c2264daf0ec[0]","orig_def_id":"test/8e312bae::S1","orig_substs":[],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/8e312bae::S1::x","ty":"ty::u32"},{"name":"test/8e312bae::S1::y","ty":"ty::u32"}],"inhabited":true,"name":"test/8e312bae::S1"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/8e312bae::f","kind":"Item","substs":[]},"name":"test/8e312bae::f"},{"inst":{"def_id":"test/8e312bae::h","kind":"Item","substs":[]},"name":"test/8e312bae::h"},{"inst":{"def_id":"test/8e312bae::g","kind":"Item","substs":[]},"name":"test/8e312bae::g"},{"inst":{"def_id":"test/8e312bae::i","kind":"Item","substs":[]},"name":"test/8e312bae::i"}],"tys":[{"name":"ty::Adt::01bd9e2f4f30865e","ty":{"kind":"Adt","name":"test/8e312bae::S1::_adtb7803c2264daf0ec[0]","orig_def_id":"test/8e312bae::S1","substs":[]}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::cef0e4ed0a308aa2","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"ty":"ty::u32"}},{"name":"ty::Adt::480389e29db14a3a","ty":{"kind":"Adt","name":"test/8e312bae::S2::_adtb7803c2264daf0ec[0]","orig_def_id":"test/8e312bae::S2","substs":[]}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}}],"roots":["test/8e312bae::f","test/8e312bae::g","test/8e312bae::h","test/8e312bae::i"]}

intTests/test_mir_fresh_expanded_value/test.rs

@@ -0,0 +1,17 @@
+pub struct S1 {
+    pub x: u32,
+    pub y: u32,
+}
+
+pub fn f(_s: S1) {}
+
+pub fn g(_a: [u32; 2]) {}
+
+pub fn h(_t: (u32, u32)) {}
+
+pub struct S2 {
+    pub z: u32,
+    pub w: &'static u32,
+}
+
+pub fn i(_s: S2) {}

intTests/test_mir_fresh_expanded_value/test.saw

@@ -0,0 +1,36 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+let s1_adt = mir_find_adt m "test::S1" [];
+let s2_adt = mir_find_adt m "test::S2" [];
+
+let f_spec = do {
+  s <- mir_fresh_expanded_value "s" (mir_adt s1_adt);
+
+  mir_execute_func [s];
+};
+
+let g_spec = do {
+  a <- mir_fresh_expanded_value "a" (mir_array 2 mir_u32);
+
+  mir_execute_func [a];
+};
+
+let h_spec = do {
+  t <- mir_fresh_expanded_value "t" (mir_tuple [mir_u32, mir_u32]);
+
+  mir_execute_func [t];
+};
+
+let i_spec = do {
+  s <- mir_fresh_expanded_value "s" (mir_adt s2_adt);
+
+  mir_execute_func [s];
+};
+
+mir_verify m "test::f" [] false f_spec z3;
+mir_verify m "test::g" [] false g_spec z3;
+mir_verify m "test::h" [] false h_spec z3;
+fails (
+  mir_verify m "test::i" [] false i_spec z3
+);

intTests/test_mir_fresh_expanded_value/test.sh

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

saw-remote-api/CHANGELOG.md

@@ -25,6 +25,11 @@
 * The API for `"struct"` `setup value`s now has a `"MIR ADT"` field. For
   MIR verification, this field is required. For LLVM and JVM verification,
   this field must be `null`, or else an error will be raised.
+* Add a `"fresh expanded"` `setup value` that denotes a value entirely
+  populated by fresh symbolic variables. For compound types such as structs or
+  arrays, this will explicitly set each field or element to contain a fresh
+  symbolic variable. This is currently only supported with LLVM and MIR
+  verification, and using this with JVM verification will raise an error.
 * Add `"slice"` and `"slice range"` `setup value`s representing slices in MIR
   verification. Attempting to use these in LLVM or JVM verification will raise
   an error.

saw-remote-api/python/CHANGELOG.md

@@ -31,6 +31,12 @@
 * Add a `proclaim_f` function. This behaves like the `proclaim` function, except
   that it takes a `cry_f`-style format string as an argument. That is,
   `proclaim_f(...)` is equivalent to `proclaim(cry_f(...))`.
+* Add a `fresh_expanded` function that creates a value entirely populated by
+  fresh symbolic variables. For compound types such as structs or arrays, this
+  will explicitly set each field or element to contain a fresh symbolic
+  variable. This function is currently only supported with LLVM and MIR
+  verification, and using this function with JVM verification will raise an
+  error.
 
 ## 1.0.1 -- YYYY-MM-DD
 

saw-remote-api/python/saw_client/crucible.py

@@ -213,6 +213,19 @@ def to_json(self) -> JSON:
         return {'setup value': 'field',
                 'base': self.base.to_json(), 'field': self.field_name}
 
+class FreshExpandedVal(SetupVal):
+    prefix: str
+    ty: Union['LLVMType', 'JVMType', 'MIRType']
+
+    def __init__(self, prefix : str, ty : Union['LLVMType', 'JVMType', 'MIRType']) -> None:
+        self.prefix = prefix
+        self.ty = ty
+
+    def to_json(self) -> JSON:
+        return {'setup value': 'fresh expanded',
+                'prefix': self.prefix,
+                'type': self.ty.to_json()}
+
 class GlobalInitializerVal(SetupVal):
     name : str
 
@@ -763,6 +776,18 @@ def field(base : SetupVal, field_name : str) -> SetupVal:
         raise ValueError('field expected a str, but got {field_name!r}')
     return FieldVal(base, field_name)
 
+def fresh_expanded(prefix: str, ty: Union['LLVMType', 'JVMType', 'MIRType']) -> SetupVal:
+    """Returns a value entirely populated with fresh symbolic variables (i.e.,
+    a ``FreshExpandedVal``). If ``ty`` is a compound type such as a struct or an
+    array, this will explicitly set each field or element to contain a fresh
+    symbolic variable. The ``prefix`` argument is used as a prefix in each of
+    the symbolic variables.
+
+    At present, this is only supported with LLVM and MIR verification. Using
+    this function with JVM verification will raise an error.
+    """
+    return FreshExpandedVal(prefix, ty)
+
 def global_initializer(name: str) -> SetupVal:
     """Returns the initializer value of a named global ``name`` (i.e., a ``GlobalInitializerVal``)."""
     if not isinstance(name, str):

saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value.linked-mir.json

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::280e5deae5669c6d"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value.rs:6:20: 6:20"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"mir_fresh_expanded_value/90f4371e::f","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::cef0e4ed0a308aa2"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value.rs:8:26: 8:26"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"mir_fresh_expanded_value/90f4371e::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value.rs:10:28: 10:28"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"mir_fresh_expanded_value/90f4371e::h","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::9419786252d2b491"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_fresh_expanded_value.rs:17:20: 17:20"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"mir_fresh_expanded_value/90f4371e::i","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"mir_fresh_expanded_value/90f4371e::S1::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_fresh_expanded_value/90f4371e::S1","orig_substs":[],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"mir_fresh_expanded_value/90f4371e::S1::x","ty":"ty::u32"},{"name":"mir_fresh_expanded_value/90f4371e::S1::y","ty":"ty::u32"}],"inhabited":true,"name":"mir_fresh_expanded_value/90f4371e::S1"}]},{"kind":{"kind":"Struct"},"name":"mir_fresh_expanded_value/90f4371e::S2::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_fresh_expanded_value/90f4371e::S2","orig_substs":[],"repr_transparent":false,"size":16,"variants":[{"ctor_kind":null,"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"mir_fresh_expanded_value/90f4371e::S2::z","ty":"ty::u32"},{"name":"mir_fresh_expanded_value/90f4371e::S2::w","ty":"ty::Ref::e028c0f25e8b6323"}],"inhabited":true,"name":"mir_fresh_expanded_value/90f4371e::S2"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_fresh_expanded_value/90f4371e::f","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value/90f4371e::f"},{"inst":{"def_id":"mir_fresh_expanded_value/90f4371e::g","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value/90f4371e::g"},{"inst":{"def_id":"mir_fresh_expanded_value/90f4371e::h","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value/90f4371e::h"},{"inst":{"def_id":"mir_fresh_expanded_value/90f4371e::i","kind":"Item","substs":[]},"name":"mir_fresh_expanded_value/90f4371e::i"}],"tys":[{"name":"ty::Adt::280e5deae5669c6d","ty":{"kind":"Adt","name":"mir_fresh_expanded_value/90f4371e::S1::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_fresh_expanded_value/90f4371e::S1","substs":[]}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::cef0e4ed0a308aa2","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"ty":"ty::u32"}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}},{"name":"ty::Adt::9419786252d2b491","ty":{"kind":"Adt","name":"mir_fresh_expanded_value/90f4371e::S2::_adtb7803c2264daf0ec[0]","orig_def_id":"mir_fresh_expanded_value/90f4371e::S2","substs":[]}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}}],"roots":["mir_fresh_expanded_value/90f4371e::f","mir_fresh_expanded_value/90f4371e::g","mir_fresh_expanded_value/90f4371e::h","mir_fresh_expanded_value/90f4371e::i"]}

saw-remote-api/python/tests/saw/test-files/mir_fresh_expanded_value.rs

@@ -0,0 +1,17 @@
+pub struct S1 {
+    pub x: u32,
+    pub y: u32,
+}
+
+pub fn f(_s: S1) {}
+
+pub fn g(_a: [u32; 2]) {}
+
+pub fn h(_t: (u32, u32)) {}
+
+pub struct S2 {
+    pub z: u32,
+    pub w: &'static u32,
+}
+
+pub fn i(_s: S2) {}

saw-remote-api/python/tests/saw/test_mir_fresh_expanded_value.py

@@ -0,0 +1,61 @@
+import unittest
+from pathlib import Path
+
+from saw_client import *
+from saw_client.crucible import fresh_expanded
+from saw_client.mir import Contract, MIRAdt, adt_ty, array_ty, tuple_ty, u32, void
+
+
+class FContract(Contract):
+    adt: MIRAdt
+
+    def __init__(self, adt: MIRAdt):
+        super().__init__()
+        self.adt = adt
+
+    def specification(self) -> None:
+        s = fresh_expanded('s', adt_ty(self.adt))
+
+        self.execute_func(s)
+
+        self.returns(void)
+
+
+class GContract(Contract):
+    def specification(self) -> None:
+        a = fresh_expanded('a', array_ty(2, u32))
+
+        self.execute_func(a)
+
+        self.returns(void)
+
+
+class HContract(Contract):
+    def specification(self) -> None:
+        t = fresh_expanded('t', tuple_ty(u32, u32))
+
+        self.execute_func(t)
+
+        self.returns(void)
+
+
+class MIRFreshExpandedValueTest(unittest.TestCase):
+    def test_mir_fresh_expanded_value(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        json_name = str(Path('tests', 'saw', 'test-files', 'mir_fresh_expanded_value.linked-mir.json'))
+        mod = mir_load_module(json_name)
+
+        s1_adt = mir_find_adt(mod, 'mir_fresh_expanded_value::S1')
+        f_result = mir_verify(mod, 'mir_fresh_expanded_value::f', FContract(s1_adt))
+        self.assertIs(f_result.is_success(), True)
+
+        g_result = mir_verify(mod, 'mir_fresh_expanded_value::g', GContract())
+        self.assertIs(g_result.is_success(), True)
+
+        h_result = mir_verify(mod, 'mir_fresh_expanded_value::h', HContract())
+        self.assertIs(h_result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()

saw-remote-api/src/SAWServer.hs

@@ -124,6 +124,7 @@ data CrucibleSetupVal ty e
   | GlobalLValue String
   | NamedValue ServerName
   | CryptolExpr e
+  | FreshExpandedValue Text ty
   deriving stock (Foldable, Functor, Traversable)
 
 data SetupStep ty

saw-remote-api/src/SAWServer/Data/SetupValue.hs

@@ -23,6 +23,7 @@ data SetupValTag
   | TagElemLValue
   | TagGlobalInit
   | TagGlobalLValue
+  | TagFreshExpandedValue
 
 instance FromJSON SetupValTag where
   parseJSON =
@@ -42,6 +43,7 @@ instance FromJSON SetupValTag where
       "element lvalue" -> pure TagElemLValue
       "global initializer" -> pure TagGlobalInit
       "global lvalue" -> pure TagGlobalLValue
+      "fresh expanded" -> pure TagFreshExpandedValue
       _ -> empty
 
 instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cryptolExpr) where
@@ -64,3 +66,4 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr
           TagElemLValue -> ElementLValue <$> o .: "base" <*> o .: "index"
           TagGlobalInit -> GlobalInitializer <$> o .: "name"
           TagGlobalLValue -> GlobalLValue <$> o .: "name"
+          TagFreshExpandedValue -> FreshExpandedValue <$> o .: "prefix" <*> o .: "type"

saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs

@@ -202,6 +202,8 @@ compileJVMContract fileReader bic cenv0 c =
       JVMSetupM $ fail "Global initializers unsupported in JVM API."
     getSetupVal _ (GlobalLValue _) =
       JVMSetupM $ fail "Global l-values unsupported in JVM API."
+    getSetupVal _ (FreshExpandedValue _ _) =
+      JVMSetupM $ fail "Fresh expanded values unsupported in JVM API."
 
 data JVMLoadClassParams
   = JVMLoadClassParams ServerName String

saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs

@@ -38,6 +38,7 @@ import SAWScript.Crucible.LLVM.Builtins
     , llvm_alloc_readonly
     , llvm_alloc_readonly_aligned
     , llvm_execute_func
+    , llvm_fresh_expanded_val
     , llvm_fresh_var
     , llvm_points_to_internal
     , llvm_points_to_bitfield
@@ -211,6 +212,9 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c =
       resolve env n >>= \case Val x -> return x
     getSetupVal (_, cenv) (CryptolExpr expr) =
       CMS.anySetupTerm <$> getTypedTerm cenv expr
+    getSetupVal _ (FreshExpandedValue _ ty) =
+      let ty' = llvmType ty in
+      llvm_fresh_expanded_val ty'
 
 data LLVMLoadModuleParams
   = LLVMLoadModuleParams ServerName FilePath

saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs

@@ -28,6 +28,7 @@ import SAWScript.Crucible.Common.Setup.Builtins (CheckPointsToType(..))
 import SAWScript.Crucible.MIR.Builtins
     ( mir_alloc,
       mir_alloc_mut,
+      mir_fresh_expanded_value,
       mir_fresh_var,
       mir_execute_func,
       mir_load_module,
@@ -202,6 +203,9 @@ compileMIRContract fileReader bic cenv0 sawenv c =
       pure $ MS.SetupGlobalInitializer () name
     getSetupVal _ (GlobalLValue name) =
       pure $ MS.SetupGlobal () name
+    getSetupVal _ (FreshExpandedValue pfx ty) =
+      let ty' = mirType sawenv ty in
+      mir_fresh_expanded_value pfx ty'
     getSetupVal env (SliceValue base) = do
       base' <- getSetupVal env base
       pure $ mir_slice_value base'