mir_fresh_cryptol_var

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

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::a60250c8af2ca6f4"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::a60250c8af2ca6f4"}},"pos":"test.rs:2:5: 2:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::a60250c8af2ca6f4"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::a60250c8af2ca6f4"}]},"name":"test/bfa24f84::id_array","return_ty":"ty::Array::a60250c8af2ca6f4","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:6:5: 6:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}]},"name":"test/bfa24f84::id_tuple","return_ty":"ty::Tuple::f54c7b3282e27392","spread_arg":null},{"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":"_0","ty":"ty::u32"}},"pos":"test.rs:10:5: 10:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:11:2: 11:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/bfa24f84::id_u32","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/bfa24f84::id_array","kind":"Item","substs":[]},"name":"test/bfa24f84::id_array"},{"inst":{"def_id":"test/bfa24f84::id_tuple","kind":"Item","substs":[]},"name":"test/bfa24f84::id_tuple"},{"inst":{"def_id":"test/bfa24f84::id_u32","kind":"Item","substs":[]},"name":"test/bfa24f84::id_u32"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::a60250c8af2ca6f4","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"5"},"ty":"ty::usize"},"ty":"ty::u32"}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}}],"roots":["test/bfa24f84::id_array","test/bfa24f84::id_tuple","test/bfa24f84::id_u32"]}

intTests/test_mir_fresh_cryptol_var/test.rs

@@ -0,0 +1,11 @@
+pub fn id_array(x: [u32; 5]) -> [u32; 5] {
+    x
+}
+
+pub fn id_tuple(x: (u32, u32)) -> (u32, u32) {
+    x
+}
+
+pub fn id_u32(x: u32) -> u32 {
+    x
+}

intTests/test_mir_fresh_cryptol_var/test.saw

@@ -0,0 +1,15 @@
+enable_experimental;
+
+let id_spec cty = do {
+  x <- mir_fresh_cryptol_var "x" cty;
+
+  mir_execute_func [mir_term x];
+
+  mir_return (mir_term x);
+};
+
+m <- mir_load_module "test.linked-mir.json";
+
+mir_verify m "test::id_array" [] false (id_spec {| [5][32] |}) z3;
+mir_verify m "test::id_tuple" [] false (id_spec {| ([32], [32]) |}) z3;
+mir_verify m "test::id_u32" [] false (id_spec {| [32] |}) z3;

intTests/test_mir_fresh_cryptol_var/test.sh

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

src/SAWScript/Crucible/MIR/Builtins.hs

@@ -15,6 +15,7 @@ module SAWScript.Crucible.MIR.Builtins
   , mir_assert
   , mir_execute_func
   , mir_find_adt
+  , mir_fresh_cryptol_var
   , mir_fresh_expanded_value
   , mir_fresh_var
   , mir_load_module
@@ -221,6 +222,22 @@ mir_find_adt rm origName substs = do
   origDid <- findDefId crateDisambigs (Text.pack origName)
   findAdt col origDid (Mir.Substs substs)
 
+-- | Generate a fresh term of the given Cryptol type. The name will be used when
+-- pretty-printing the variable in debug output.
+mir_fresh_cryptol_var ::
+  Text ->
+  Cryptol.Schema ->
+  MIRSetupM TypedTerm
+mir_fresh_cryptol_var name s =
+  MIRSetupM $
+  do loc <- getW4Position "mir_fresh_var"
+     case s of
+       Cryptol.Forall [] [] ty ->
+         do sc <- lift $ lift getSharedContext
+            Setup.freshVariable sc name ty
+       _ ->
+         throwCrucibleSetup loc $ "Unsupported polymorphic Cryptol type schema: " ++ show s
+
 -- | Create a MIR value entirely populated with fresh symbolic variables.
 -- For compound types such as structs and arrays, this will explicitly set
 -- each field or element to contain a fresh symbolic variable. The Text

src/SAWScript/Interpreter.hs

@@ -3938,6 +3938,15 @@ primitives = Map.fromList
     , "be found in the MIRModule, this will raise an error."
     ]
 
+  , prim "mir_fresh_cryptol_var" "String -> Type -> MIRSetup Term"
+    (pureVal mir_fresh_cryptol_var)
+    Experimental
+    [ "Create a fresh symbolic variable of the given Cryptol type for use"
+    , "within a MIR specification. The given name is used only for"
+    , "pretty-printing. Unlike 'mir_fresh_var', this can be used when"
+    , "there isn't an appropriate MIR type, such as the Cryptol Array type."
+    ]
+
   , prim "mir_fresh_expanded_value" "String -> MIRType -> MIRSetup MIRValue"
     (pureVal mir_fresh_expanded_value)
     Experimental