Skip to content

Commit

Permalink
mir_fresh_cryptol_var
Browse files Browse the repository at this point in the history
This also adds some very rudimentary test cases. A more impressive test case
would involve ghost state, but we will need #1958 before we can write such a
test case.

Fixes #1970.
  • Loading branch information
RyanGlScott committed Nov 9, 2023
1 parent 8583a6d commit b2f1f7a
Show file tree
Hide file tree
Showing 7 changed files with 69 additions and 0 deletions.
13 changes: 13 additions & 0 deletions intTests/test_mir_fresh_cryptol_var/Makefile
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions intTests/test_mir_fresh_cryptol_var/test.linked-mir.json
Original file line number Diff line number Diff line change
@@ -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"]}
11 changes: 11 additions & 0 deletions intTests/test_mir_fresh_cryptol_var/test.rs
Original file line number Diff line number Diff line change
@@ -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
}
15 changes: 15 additions & 0 deletions intTests/test_mir_fresh_cryptol_var/test.saw
Original file line number Diff line number Diff line change
@@ -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;
3 changes: 3 additions & 0 deletions intTests/test_mir_fresh_cryptol_var/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
set -e

$SAW test.saw
17 changes: 17 additions & 0 deletions src/SAWScript/Crucible/MIR/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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_ghost_value
Expand Down Expand Up @@ -234,6 +235,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
Expand Down
9 changes: 9 additions & 0 deletions src/SAWScript/Interpreter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3957,6 +3957,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
Expand Down

0 comments on commit b2f1f7a

Please sign in to comment.