mir_fresh_expanded_value

This adds a `mir_fresh_expanded_value` command, which creates a MIR value
populated entirely 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 heavily inspired by the
`llvm_fresh_expanded_val` command in the LLVM backend.

This command will be important for the MIR user story going forward, as we will
impose an requirement that all mutable allocations in an override must be
explicitly set in the override's postconditions. The `mir_fresh_expanded_value`
command provides a convenient way to quickly generate values to set in the
postconditions.

At present, `mir_fresh_expanded_value` comes with the limitation that it does
not support reference types. This is not an inherent limitation, but it is one
that will require some additional work to lift. In particular, we will likely
need something like a `mir_fresh_ref` command (similar to LLVM's
`llvm_fresh_pointer` command) to make this work. We leave the task of
implementing `mir_fresh_ref` to a later patch.

This checks off one box in #1859.

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'