diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index 91d5b40a21..2a041b829f 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -685,14 +685,14 @@ regToSetup bak p eval shp rv = go shp rv msbPrePost p . seVars %= Set.insert (Some var) liftIO $ MS.SetupTerm <$> eval btpr expr go (TupleShape _ _ flds) rvs = MS.SetupStruct () <$> goFields flds rvs - go (ArrayShape _ _ shp) vec = do + go (ArrayShape _ elemTy shp) vec = do svs <- case vec of MirVector_Vector v -> mapM (go shp) (toList v) MirVector_PartialVector v -> forM (toList v) $ \p -> do rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p go shp rv MirVector_Array _ -> error $ "regToSetup: MirVector_Array NYI" - return $ MS.SetupArray () svs + return $ MS.SetupArray elemTy svs go (StructShape _ _ flds) (AnyValue tpr rvs) | Just Refl <- testEquality tpr shpTpr = MS.SetupStruct () <$> goFields flds rvs diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index 22dea6d78c..c89164423e 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -391,7 +391,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv show (W4.printSymExpr val)) "" go (TupleShape _ _ flds) rvs (MS.SetupStruct () svs) = goFields flds rvs svs - go (ArrayShape _ _ shp) vec (MS.SetupArray () svs) = case vec of + go (ArrayShape _ _ shp) vec (MS.SetupArray _ svs) = case vec of MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 97c24ec515..02cec02a93 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -2621,6 +2621,13 @@ the value of an array element. * `jvm_field_is : JVMValue -> String -> JVMValue -> JVMSetup ()` specifies the name of an object field. +In the experimental MIR verification implementation, the following functions +construct compound values: + +* `mir_array_value : MIRType -> [SetupValue] -> SetupValue` constructs an array + of the given type whose elements consist of the given values. Supplying the + element type is necessary to support length-0 arrays. + ### Bitfields SAW has experimental support for specifying `struct`s with bitfields, such as diff --git a/intTests/test_mir_verify_arrays/Makefile b/intTests/test_mir_verify_arrays/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_verify_arrays/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 diff --git a/intTests/test_mir_verify_arrays/test.linked-mir.json b/intTests/test_mir_verify_arrays/test.linked-mir.json new file mode 100644 index 0000000000..dfa30b36fd --- /dev/null +++ b/intTests/test_mir_verify_arrays/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::81835db4e9facbc9"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"pos":"test.rs:2:7: 2:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:2:5: 2:29","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::81835db4e9facbc9"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:2:5: 2:29","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"}},"pos":"test.rs:2:26: 2:27","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:2:23: 2:28","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::81835db4e9facbc9"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"test.rs:2:23: 2:28","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:2:5: 2:29"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/20eb85f3::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"test.rs:10:30: 10:31","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:10:30: 10:31"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"test/20eb85f3::h::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":true,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::2b5f0dde3662ce8b"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:16:2: 16:2"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::c637e0515abd45e8"}]},"name":"test/20eb85f3::i","return_ty":"ty::Array::c637e0515abd45e8","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"test.rs:5:24: 5:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:5:24: 5:25"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"test/20eb85f3::g::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::555de431791d484a"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"}},"pos":"test.rs:6:8: 6:9","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:6:5: 6:15","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::555de431791d484a"}}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:6:5: 6:15","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"}},"pos":"test.rs:7:15: 7:16","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:7:13: 7:33","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::555de431791d484a"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"test.rs:7:13: 7:33","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::953fce25114368d0"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"test.rs:7:13: 7:33"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"}},"pos":"test.rs:7:8: 7:9","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:7:5: 7:33","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::555de431791d484a"}}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::Ref::953fce25114368d0"}},"pos":"test.rs:7:5: 7:33","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:8:2: 8:2"}},"blockid":"bb1"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"},{"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":"Not"},"name":"_5","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::Ref::953fce25114368d0"}]},"name":"test/20eb85f3::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"test.rs:1:20: 1:21","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:20: 1:21"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"test/20eb85f3::f::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"test.rs:14:20: 14:21","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:14:20: 14:21"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"test/20eb85f3::i::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"test.rs:14:33: 14:34","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:14:33: 14:34"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"test/20eb85f3::i::{constant#1}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:11:6: 11:9","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/20eb85f35364dfc9::{{alloc}}[0]","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:11:6: 11:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:11:6: 11:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:11:11: 11:14","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"test/20eb85f35364dfc9::{{alloc}}[1]","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"test.rs:11:11: 11:14","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::81835db4e9facbc9"}},"pos":"test.rs:11:5: 11:15","rhs":{"akind":{"kind":"Array","ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Aggregate","ops":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"}]}}],"terminator":{"kind":"Return","pos":"test.rs:12:2: 12:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::81835db4e9facbc9"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"test/20eb85f3::h","return_ty":"ty::Array::81835db4e9facbc9","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:13: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1163:10: 1163:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}]},"name":"core/73237d41::num::{impl#9}::wrapping_add","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[{"kind":"constant","mutable":false,"name":"test/20eb85f35364dfc9::{{alloc}}[0]","rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},{"kind":"constant","mutable":false,"name":"test/20eb85f35364dfc9::{{alloc}}[1]","rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"}],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/20eb85f3::f","kind":"Item","substs":[]},"name":"test/20eb85f3::f"},{"inst":{"def_id":"test/20eb85f3::h::{constant#0}","kind":"Item","substs":[]},"name":"test/20eb85f3::h::{constant#0}"},{"inst":{"def_id":"test/20eb85f3::i","kind":"Item","substs":[]},"name":"test/20eb85f3::i"},{"inst":{"def_id":"test/20eb85f3::g::{constant#0}","kind":"Item","substs":[]},"name":"test/20eb85f3::g::{constant#0}"},{"inst":{"def_id":"test/20eb85f3::g","kind":"Item","substs":[]},"name":"test/20eb85f3::g"},{"inst":{"def_id":"test/20eb85f3::f::{constant#0}","kind":"Item","substs":[]},"name":"test/20eb85f3::f::{constant#0}"},{"inst":{"def_id":"test/20eb85f3::i::{constant#0}","kind":"Item","substs":[]},"name":"test/20eb85f3::i::{constant#0}"},{"inst":{"def_id":"test/20eb85f3::i::{constant#1}","kind":"Item","substs":[]},"name":"test/20eb85f3::i::{constant#1}"},{"inst":{"def_id":"test/20eb85f3::h","kind":"Item","substs":[]},"name":"test/20eb85f3::h"},{"inst":{"def_id":"core/73237d41::num::{impl#9}::wrapping_add","kind":"Item","substs":[]},"name":"core/73237d41::num::{impl#9}::wrapping_add"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::81835db4e9facbc9","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"ty":"ty::Ref::e028c0f25e8b6323"}},{"name":"ty::FnDef::f55acdef755f1aaa","ty":{"defid":"core/73237d41::num::{impl#9}::wrapping_add","kind":"FnDef"}},{"name":"ty::Array::2b5f0dde3662ce8b","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"ty":"ty::u32"}},{"name":"ty::u64","ty":{"kind":"Uint","uintkind":{"kind":"U64"}}},{"name":"ty::Array::c637e0515abd45e8","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"ty":"ty::u64"}},{"name":"ty::Ref::953fce25114368d0","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"name":"ty::Array::555de431791d484a","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"ty":"ty::Ref::953fce25114368d0"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}}],"roots":["test/20eb85f3::f","test/20eb85f3::f::{constant#0}","test/20eb85f3::g","test/20eb85f3::g::{constant#0}","test/20eb85f3::h","test/20eb85f3::h::{constant#0}","test/20eb85f3::i","test/20eb85f3::i::{constant#0}","test/20eb85f3::i::{constant#1}"]} \ No newline at end of file diff --git a/intTests/test_mir_verify_arrays/test.rs b/intTests/test_mir_verify_arrays/test.rs new file mode 100644 index 0000000000..a3f8985e86 --- /dev/null +++ b/intTests/test_mir_verify_arrays/test.rs @@ -0,0 +1,16 @@ +pub fn f(x: [&u32; 2]) -> u32 { + x[0].wrapping_add(*x[1]) +} + +pub fn g(x: [&mut u32; 2]) { + *x[0] = 42; + *x[1] = x[1].wrapping_add(1); +} + +pub fn h() -> [&'static u32; 2] { + [&27, &42] +} + +pub fn i(_x: [u32; 0]) -> [u64; 0] { + [] +} diff --git a/intTests/test_mir_verify_arrays/test.saw b/intTests/test_mir_verify_arrays/test.saw new file mode 100644 index 0000000000..8f743c3261 --- /dev/null +++ b/intTests/test_mir_verify_arrays/test.saw @@ -0,0 +1,80 @@ +enable_experimental; + +let f_spec = do { + x0_ref <- mir_alloc mir_u32; + x0 <- mir_fresh_var "x0" mir_u32; + mir_points_to x0_ref (mir_term x0); + + x1_ref <- mir_alloc mir_u32; + x1 <- mir_fresh_var "x1" mir_u32; + mir_points_to x1_ref (mir_term x1); + + let x = mir_array_value (mir_ref mir_u32) [x0_ref, x1_ref]; + + mir_execute_func [x]; + + mir_return (mir_term {{ x0 + x1 }}); +}; + +let g_spec = do { + x0_ref <- mir_alloc_mut mir_u32; + + x1_ref <- mir_alloc_mut mir_u32; + x1 <- mir_fresh_var "x1" mir_u32; + mir_points_to x1_ref (mir_term x1); + + let x = mir_array_value (mir_ref_mut mir_u32) [x0_ref, x1_ref]; + + mir_execute_func [x]; + + mir_points_to x0_ref (mir_term {{ 42 : [32] }}); + mir_points_to x1_ref (mir_term {{ x1 + 1 }}); +}; + +let h_spec = do { + mir_execute_func []; + + x0_ref <- mir_alloc mir_u32; + mir_points_to x0_ref (mir_term {{ 27 : [32] }}); + + x1_ref <- mir_alloc mir_u32; + mir_points_to x1_ref (mir_term {{ 42 : [32] }}); + + let x = mir_array_value (mir_ref mir_u32) [x0_ref, x1_ref]; + mir_return x; +}; + +let i_spec = do { + let x = mir_term {{ [] : [0][32] }}; + mir_execute_func [x]; + + mir_return (mir_array_value mir_u64 []); +}; + +let i_spec_bad1 = do { + let x = mir_term {{ [42] : [1][32] }}; + mir_execute_func [x]; + + mir_return (mir_array_value mir_u64 []); +}; + +let i_spec_bad2 = do { + let x = mir_term {{ [] : [0][32] }}; + mir_execute_func [x]; + + mir_return (mir_array_value mir_u64 [mir_term {{ 42 : [64] }}]); +}; + +m <- mir_load_module "test.linked-mir.json"; + +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; +mir_verify m "test::i" [] false i_spec z3; + +fails ( + mir_verify m "test::i" [] false i_spec_bad1 z3 +); +fails ( + mir_verify m "test::i" [] false i_spec_bad2 z3 +); diff --git a/intTests/test_mir_verify_arrays/test.sh b/intTests/test_mir_verify_arrays/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_verify_arrays/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/CHANGELOG.md b/saw-remote-api/CHANGELOG.md index 2fb5ef4838..90fc120547 100644 --- a/saw-remote-api/CHANGELOG.md +++ b/saw-remote-api/CHANGELOG.md @@ -13,6 +13,10 @@ how SAW's MIR verification support works in general, see the `mir_*` commands documented in the [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md). +* The API for `"array"` `setup value`s now has an `"element type"` field. For + LLVM verification, this field is optional. For MIR verification, this field + is required if the `"elements"` value is empty and optional if the + `"elements"` value is non-empty. ## 1.0.0 -- 2023-06-26 diff --git a/saw-remote-api/python/CHANGELOG.md b/saw-remote-api/python/CHANGELOG.md index 6944dd7692..7aa8094779 100644 --- a/saw-remote-api/python/CHANGELOG.md +++ b/saw-remote-api/python/CHANGELOG.md @@ -12,6 +12,9 @@ For more information about how SAW's MIR verification support works in general, see the `mir_*` commands documented in the [SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md). +* The `array()` function now takes an additional `element_type` argument, which + defaults to `None`. If constructing a MIR array with no elements, then the + `element_type` must be specified. Otherwise, this argument is optional. ## 1.0.1 -- YYYY-MM-DD diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py index f4c18dfaa5..04f1393969 100644 --- a/saw-remote-api/python/saw_client/crucible.py +++ b/saw-remote-api/python/saw_client/crucible.py @@ -197,13 +197,23 @@ def to_json(self) -> JSON: return {'setup value': 'null'} class ArrayVal(SetupVal): + element_type : Union['LLVMType', 'JVMType', 'MIRType', None] elements : List[SetupVal] - def __init__(self, elements : List[SetupVal]) -> None: + def __init__(self, + element_type : Union['LLVMType', 'JVMType', 'MIRType', None], + elements : List[SetupVal]) -> None: + self.element_type = element_type self.elements = elements def to_json(self) -> JSON: + element_type_json: Optional[Any] + if self.element_type is None: + element_type_json = None + else: + element_type_json = self.element_type.to_json() return {'setup value': 'array', + 'element type' : element_type_json, 'elements': [element.to_json() for element in self.elements]} name_regexp = re.compile('^(?P.*[^0-9])?(?P[0-9]+)?$') @@ -668,16 +678,18 @@ def cry_f(s : str) -> CryptolTerm: """ return CryptolTerm(to_cryptol_str_customf(s, frames=1)) -def array(*elements: SetupVal) -> SetupVal: +def array(*elements: SetupVal, element_type: Union['LLVMType', 'JVMType', 'MIRType', None] = None) -> SetupVal: """Returns an array with the provided ``elements`` (i.e., an ``ArrayVal``). + If returning an empty MIR array, you are required to explicitly supply + an ``element_type``; otherwise, the ``element_type`` argument is optional. - N.B., one or more ``elements`` must be provided.""" # FIXME why? document this here when we figure it out. - if len(elements) == 0: - raise ValueError('An array must be constructed with one or more elements') + If returning an LLVM array, then one or more ``elements`` must be provided.""" # FIXME why? document this here when we figure it out. + if isinstance(element_type, LLVMType) and len(elements) == 0: + raise ValueError('An LLVM array must be constructed with one or more elements') for e in elements: if not isinstance(e, SetupVal): raise ValueError('array expected a SetupVal, but got {e!r}') - return ArrayVal(list(elements)) + return ArrayVal(element_type, list(elements)) def elem(base: SetupVal, index: int) -> SetupVal: """Returns the value of the array element at position ``index`` in ``base`` (i.e., an ``ElemVal``). diff --git a/saw-remote-api/python/tests/saw/test-files/mir_arrays.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/mir_arrays.linked-mir.json new file mode 100644 index 0000000000..b3c9e14aac --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_arrays.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::555de431791d484a"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"}},"pos":"mir_arrays.rs:6:8: 6:9","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"}},"pos":"mir_arrays.rs:6:5: 6:15","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::555de431791d484a"}}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"}},"pos":"mir_arrays.rs:6:5: 6:15","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"}},"pos":"mir_arrays.rs:7:15: 7:16","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::953fce25114368d0"}},"pos":"mir_arrays.rs:7:13: 7:33","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::555de431791d484a"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"mir_arrays.rs:7:13: 7:33","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::953fce25114368d0"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_arrays.rs:7:13: 7:33"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"}},"pos":"mir_arrays.rs:7:8: 7:9","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::Ref::953fce25114368d0"}},"pos":"mir_arrays.rs:7:5: 7:33","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::555de431791d484a"}}}},{"kind":"Assign","lhs":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::Ref::953fce25114368d0"}},"pos":"mir_arrays.rs:7:5: 7:33","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"mir_arrays.rs:8:2: 8:2"}},"blockid":"bb1"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::usize"},{"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":"Not"},"name":"_5","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_6","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::Ref::953fce25114368d0"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::Ref::953fce25114368d0"}]},"name":"mir_arrays/62f09145::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":true,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::2b5f0dde3662ce8b"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_arrays.rs:16:2: 16:2"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::c637e0515abd45e8"}]},"name":"mir_arrays/62f09145::i","return_ty":"ty::Array::c637e0515abd45e8","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"mir_arrays.rs:14:33: 14:34","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_arrays.rs:14:33: 14:34"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"mir_arrays/62f09145::i::{constant#1}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::81835db4e9facbc9"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}},"pos":"mir_arrays.rs:2:7: 2:8","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_arrays.rs:2:5: 2:29","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::81835db4e9facbc9"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"mir_arrays.rs:2:5: 2:29","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"}},"pos":"mir_arrays.rs:2:26: 2:27","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"1"},"ty":"ty::usize"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_arrays.rs:2:23: 2:28","rhs":{"kind":"CopyForDeref","place":{"data":[{"kind":"Index","op":{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"}}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::81835db4e9facbc9"}}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"mir_arrays.rs:2:23: 2:28","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Deref"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::f55acdef755f1aaa"},"kind":"Constant"},"kind":"Call","pos":"mir_arrays.rs:2:5: 2:29"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"mir_arrays.rs:3:2: 3:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_5","ty":"ty::usize"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"mir_arrays/62f09145::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"mir_arrays.rs:10:30: 10:31","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_arrays.rs:10:30: 10:31"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"mir_arrays/62f09145::h::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"mir_arrays.rs:1:20: 1:21","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_arrays.rs:1:20: 1:21"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"mir_arrays/62f09145::f::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_arrays.rs:11:6: 11:9","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_arrays/62f09145c10d242b::{{alloc}}[0]","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_arrays.rs:11:6: 11:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_arrays.rs:11:6: 11:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_arrays.rs:11:11: 11:14","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"def_id":"mir_arrays/62f09145c10d242b::{{alloc}}[1]","kind":"static_ref"},"ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Constant"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}},"pos":"mir_arrays.rs:11:11: 11:14","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::81835db4e9facbc9"}},"pos":"mir_arrays.rs:11:5: 11:15","rhs":{"akind":{"kind":"Array","ty":"ty::Ref::e028c0f25e8b6323"},"kind":"Aggregate","ops":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"},{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"}},"kind":"Move"}]}}],"terminator":{"kind":"Return","pos":"mir_arrays.rs:12:2: 12:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::81835db4e9facbc9"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::Ref::e028c0f25e8b6323"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::Ref::e028c0f25e8b6323"}]},"name":"mir_arrays/62f09145::h","return_ty":"ty::Array::81835db4e9facbc9","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"mir_arrays.rs:5:24: 5:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_arrays.rs:5:24: 5:25"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"mir_arrays/62f09145::g::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"mir_arrays.rs:14:20: 14:21","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"mir_arrays.rs:14:20: 14:21"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"mir_arrays/62f09145::i::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:38: 1162:42 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"StorageLive","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","slvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:44: 1162:47 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:13: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"kind":"BinaryOp","op":{"kind":"Add"}}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},{"kind":"StorageDead","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1162:47: 1162:48 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101","sdvar":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}}],"terminator":{"kind":"Return","pos":"/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/uint_macros.rs:1163:10: 1163:10 !/rustc/5e37043d63bfe2f3be8fa5a05b07d6c0dad5775d/library/core/src/num/mod.rs:921:5: 922:101"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}]},"name":"core/73237d41::num::{impl#9}::wrapping_add","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[{"kind":"constant","mutable":false,"name":"mir_arrays/62f09145c10d242b::{{alloc}}[0]","rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},{"kind":"constant","mutable":false,"name":"mir_arrays/62f09145c10d242b::{{alloc}}[1]","rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"}],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"mir_arrays/62f09145::g","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::g"},{"inst":{"def_id":"mir_arrays/62f09145::i","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::i"},{"inst":{"def_id":"mir_arrays/62f09145::i::{constant#1}","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::i::{constant#1}"},{"inst":{"def_id":"mir_arrays/62f09145::f","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::f"},{"inst":{"def_id":"mir_arrays/62f09145::h::{constant#0}","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::h::{constant#0}"},{"inst":{"def_id":"mir_arrays/62f09145::f::{constant#0}","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::f::{constant#0}"},{"inst":{"def_id":"mir_arrays/62f09145::h","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::h"},{"inst":{"def_id":"mir_arrays/62f09145::g::{constant#0}","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::g::{constant#0}"},{"inst":{"def_id":"mir_arrays/62f09145::i::{constant#0}","kind":"Item","substs":[]},"name":"mir_arrays/62f09145::i::{constant#0}"},{"inst":{"def_id":"core/73237d41::num::{impl#9}::wrapping_add","kind":"Item","substs":[]},"name":"core/73237d41::num::{impl#9}::wrapping_add"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Ref::953fce25114368d0","ty":{"kind":"Ref","mutability":{"kind":"Mut"},"ty":"ty::u32"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::Array::555de431791d484a","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"ty":"ty::Ref::953fce25114368d0"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::f55acdef755f1aaa","ty":{"defid":"core/73237d41::num::{impl#9}::wrapping_add","kind":"FnDef"}},{"name":"ty::Array::2b5f0dde3662ce8b","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"ty":"ty::u32"}},{"name":"ty::u64","ty":{"kind":"Uint","uintkind":{"kind":"U64"}}},{"name":"ty::Array::c637e0515abd45e8","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"0"},"ty":"ty::usize"},"ty":"ty::u64"}},{"name":"ty::Ref::e028c0f25e8b6323","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::u32"}},{"name":"ty::Array::81835db4e9facbc9","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"2"},"ty":"ty::usize"},"ty":"ty::Ref::e028c0f25e8b6323"}}],"roots":["mir_arrays/62f09145::f","mir_arrays/62f09145::f::{constant#0}","mir_arrays/62f09145::g","mir_arrays/62f09145::g::{constant#0}","mir_arrays/62f09145::h","mir_arrays/62f09145::h::{constant#0}","mir_arrays/62f09145::i","mir_arrays/62f09145::i::{constant#0}","mir_arrays/62f09145::i::{constant#1}"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/mir_arrays.rs b/saw-remote-api/python/tests/saw/test-files/mir_arrays.rs new file mode 100644 index 0000000000..a3f8985e86 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/mir_arrays.rs @@ -0,0 +1,16 @@ +pub fn f(x: [&u32; 2]) -> u32 { + x[0].wrapping_add(*x[1]) +} + +pub fn g(x: [&mut u32; 2]) { + *x[0] = 42; + *x[1] = x[1].wrapping_add(1); +} + +pub fn h() -> [&'static u32; 2] { + [&27, &42] +} + +pub fn i(_x: [u32; 0]) -> [u64; 0] { + [] +} diff --git a/saw-remote-api/python/tests/saw/test_mir_arrays.py b/saw-remote-api/python/tests/saw/test_mir_arrays.py new file mode 100644 index 0000000000..8ca6f7861d --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_mir_arrays.py @@ -0,0 +1,82 @@ +import unittest +from pathlib import Path + +from saw_client import * +from saw_client.crucible import array, cry, cry_f +from saw_client.mir import Contract, FreshVar, MIRType, SetupVal, u32, u64, void + + +def ref_to_fresh(c : Contract, ty : MIRType, name : Optional[str] = None, + read_only : bool = False) -> Tuple[FreshVar, SetupVal]: + """Add to ``Contract`` ``c`` an allocation of a reference of type ``ty`` initialized to an unknown fresh value. + If ``read_only == True`` then the allocated memory is immutable. + + :returns A fresh variable bound to the reference's initial value and the newly allocated reference. (The fresh + variable will be assigned ``name`` if provided/available.)""" + var = c.fresh_var(ty, name) + ptr = c.alloc(ty, points_to = var, read_only = read_only) + return (var, ptr) + + +class FContract(Contract): + def specification(self) -> None: + (x0, x0_p) = ref_to_fresh(self, u32, "x0", read_only = True) + (x1, x1_p) = ref_to_fresh(self, u32, "x1", read_only = True) + x = array(x0_p, x1_p) + + self.execute_func(x) + + self.returns_f('{x0} + {x1}') + + +class GContract(Contract): + def specification(self) -> None: + x0_p = self.alloc(u32) + (x1, x1_p) = ref_to_fresh(self, u32, "x1") + x = array(x0_p, x1_p) + + self.execute_func(x) + + self.points_to(x0_p, cry_f('42 : [32]')) + self.points_to(x1_p, cry_f('{x1} + 1')) + self.returns(void) + + +class HContract(Contract): + def specification(self) -> None: + self.execute_func() + + x0_ptr = self.alloc(u32, points_to = cry_f('27 : [32]'), read_only = True) + x1_ptr = self.alloc(u32, points_to = cry_f('42 : [32]'), read_only = True) + self.returns(array(x0_ptr, x1_ptr)) + + +class IContract(Contract): + def specification(self) -> None: + self.execute_func(cry_f('[] : [0][32]')) + + self.returns(array(element_type = u64)) + + +class MIRArraysTest(unittest.TestCase): + def test_mir_points_to(self): + connect(reset_server=True) + if __name__ == "__main__": view(LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'mir_arrays.linked-mir.json')) + mod = mir_load_module(json_name) + + f_result = mir_verify(mod, 'mir_arrays::f', FContract()) + self.assertIs(f_result.is_success(), True) + + g_result = mir_verify(mod, 'mir_arrays::g', GContract()) + self.assertIs(g_result.is_success(), True) + + h_result = mir_verify(mod, 'mir_arrays::h', HContract()) + self.assertIs(h_result.is_success(), True) + + i_result = mir_verify(mod, 'mir_arrays::i', IContract()) + self.assertIs(i_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 8a8e79f4dd..a3200fb6de 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -106,7 +106,7 @@ instance Show SAWTask where data CrucibleSetupVal ty e = NullValue - | ArrayValue [CrucibleSetupVal ty e] + | ArrayValue (Maybe ty) [CrucibleSetupVal ty e] | TupleValue [CrucibleSetupVal ty e] -- | RecordValue [(String, CrucibleSetupVal e)] | FieldLValue (CrucibleSetupVal ty e) String diff --git a/saw-remote-api/src/SAWServer/Data/SetupValue.hs b/saw-remote-api/src/SAWServer/Data/SetupValue.hs index ff973feb34..c924fda107 100644 --- a/saw-remote-api/src/SAWServer/Data/SetupValue.hs +++ b/saw-remote-api/src/SAWServer/Data/SetupValue.hs @@ -4,7 +4,7 @@ module SAWServer.Data.SetupValue (CrucibleSetupVal) where import Control.Applicative -import Data.Aeson (FromJSON(..), withObject, withText, (.:)) +import Data.Aeson (FromJSON(..), withObject, withText, (.:), (.:?)) import SAWServer @@ -47,7 +47,7 @@ instance (FromJSON ty, FromJSON cryptolExpr) => FromJSON (CrucibleSetupVal ty cr TagNamedValue -> NamedValue <$> o .: "name" TagNullValue -> pure NullValue TagCryptol -> CryptolExpr <$> o .: "expression" - TagArrayValue -> ArrayValue <$> o .: "elements" + TagArrayValue -> ArrayValue <$> o .:? "element type" <*> o .: "elements" TagTupleValue -> TupleValue <$> o .: "elements" TagFieldLValue -> FieldLValue <$> o .: "base" <*> o .: "field" TagCastLValue -> CastLValue <$> o .: "base" <*> o .: "type" diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index 8811524901..925655df86 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -180,7 +180,7 @@ compileJVMContract fileReader bic cenv0 c = resolve env n >>= \case Val x -> return x getSetupVal (_, cenv) (CryptolExpr expr) = MS.SetupTerm <$> getTypedTerm cenv expr - getSetupVal _ (ArrayValue _) = + getSetupVal _ (ArrayValue _ _) = JVMSetupM $ fail "Array setup values unsupported in JVM API." getSetupVal _ (TupleValue _) = JVMSetupM $ fail "Tuple setup values unsupported in JVM API." diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 8eab0dd225..4de73bf090 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -176,7 +176,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c = CrucibleSetupVal JSONLLVMType (P.Expr P.PName) -> LLVMCrucibleSetupM (CMS.AllLLVM MS.SetupValue) getSetupVal _ NullValue = LLVMCrucibleSetupM $ return CMS.anySetupNull - getSetupVal env (ArrayValue elts) = + getSetupVal env (ArrayValue _ elts) = do elts' <- mapM (getSetupVal env) elts LLVMCrucibleSetupM $ return $ CMS.anySetupArray elts' getSetupVal env (TupleValue elts) = diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index 891d17f9a8..6c762033d1 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -10,8 +10,9 @@ module SAWServer.MIRCrucibleSetup ) where import Control.Exception (throw) -import Control.Lens ( view ) +import Control.Lens ( (^.), view ) import Control.Monad.IO.Class ( MonadIO(liftIO) ) +import Control.Monad.State ( MonadState(..) ) import Data.Aeson ( FromJSON(..), withObject, (.:) ) import Data.ByteString (ByteString) import Data.Map (Map) @@ -21,7 +22,8 @@ import Mir.Intrinsics (MIR) import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) -import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import qualified SAWScript.Crucible.Common.Setup.Type as MS import SAWScript.Crucible.Common.Setup.Builtins (CheckPointsToType(..)) import SAWScript.Crucible.MIR.Builtins ( mir_alloc, @@ -33,6 +35,7 @@ import SAWScript.Crucible.MIR.Builtins mir_postcond, mir_precond, mir_return ) +import SAWScript.Crucible.MIR.ResolveSetupValue (typeOfSetupValue) import SAWScript.Value (BuiltinContext, MIRSetupM(..), biSharedContext) import qualified Verifier.SAW.CryptolEnv as CEnv import Verifier.SAW.CryptolEnv (CryptolEnv) @@ -61,7 +64,7 @@ import SAWServer.OK ( OK, ok ) import SAWServer.TopLevel ( tl ) import SAWServer.TrackFile ( trackFile ) -newtype ServerSetupVal = Val (SetupValue MIR) +newtype ServerSetupVal = Val (MS.SetupValue MIR) compileMIRContract :: (FilePath -> IO ByteString) -> @@ -159,9 +162,24 @@ compileMIRContract fileReader bic cenv0 c = MS.SetupTerm <$> getTypedTerm cenv expr getSetupVal _ NullValue = MIRSetupM $ fail "Null setup values unsupported in the MIR API." - getSetupVal env (ArrayValue elts) = - do elts' <- mapM (getSetupVal env) elts - MIRSetupM $ return $ MS.SetupArray () elts' + getSetupVal env (ArrayValue mbEltTy elts) = + case (mbEltTy, elts) of + (Nothing, []) -> + MIRSetupM $ fail "Empty MIR array with unknown element type." + (Just eltTy, []) -> + return $ MS.SetupArray (mirType eltTy) [] + (_, elt:eltss) -> + do st <- MIRSetupM get + let cc = st ^. MS.csCrucibleContext + let mspec = st ^. MS.csMethodSpec + let allocEnv = MS.csAllocations mspec + let nameEnv = MS.csTypeNames mspec + elt' <- getSetupVal env elt + eltss' <- mapM (getSetupVal env) eltss + ty' <- case mbEltTy of + Just eltTy -> pure $ mirType eltTy + Nothing -> MIRSetupM $ typeOfSetupValue cc allocEnv nameEnv elt' + return $ MS.SetupArray ty' (elt':eltss') getSetupVal _ (TupleValue _) = MIRSetupM $ fail "Tuple setup values unsupported in the MIR API." getSetupVal _ (FieldLValue _ _) = diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index 0b23c3de0a..f0fc0fba28 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -182,7 +182,7 @@ instantiateSetupValue sc s v = MS.SetupNull empty -> absurd empty MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct _ _ -> return v - MS.SetupArray _ _ -> return v + MS.SetupArray elemTy vs -> MS.SetupArray elemTy <$> mapM (instantiateSetupValue sc s) vs MS.SetupElem _ _ _ -> return v MS.SetupField _ _ _ -> return v MS.SetupCast empty _ -> absurd empty @@ -301,23 +301,37 @@ matchArg opts sc cc cs prepost md actual expectedTy expected@(MS.SetupTerm expec realTerm <- valueToSC sym md failMsg tval actual matchTerm sc cc md prepost realTerm (ttTerm expectedTT) -matchArg opts sc cc cs _prepost md actual@(MIRVal (RefShape _refTy pointeeTy mutbl tpr) ref) expectedTy setupval = - case setupval of - MS.SetupVar var -> +matchArg opts sc cc cs prepost md actual expectedTy expected = + mccWithBackend cc $ \bak -> do + let sym = backendGetSym bak + case (actual, expectedTy, expected) of + (MIRVal (RefShape _refTy pointeeTy mutbl tpr) ref, _, MS.SetupVar var) -> do assignVar cc md var (Some (MirPointer tpr mutbl pointeeTy ref)) - MS.SetupNull empty -> absurd empty - MS.SetupGlobal empty _ -> absurd empty - MS.SetupCast empty _ -> absurd empty - MS.SetupUnion empty _ _ -> absurd empty - MS.SetupGlobalInitializer empty _ -> absurd empty - - _ -> failure (cs ^. MS.csLoc) =<< - mkStructuralMismatch opts cc sc cs actual setupval expectedTy - -matchArg opts sc cc cs _prepost md actual expectedTy expected = - failure (MS.conditionLoc md) =<< - mkStructuralMismatch opts cc sc cs actual expected expectedTy + -- match arrays point-wise + (MIRVal (ArrayShape _ _ elemShp) xs, Mir.TyArray y _len, MS.SetupArray _elemTy zs) + | Mir.MirVector_Vector xs' <- xs + , V.length xs' == length zs -> + sequence_ + [ matchArg opts sc cc cs prepost md (MIRVal elemShp x) y z + | (x, z) <- zip (V.toList xs') zs ] + + | Mir.MirVector_PartialVector xs' <- xs + , V.length xs' == length zs -> + do xs'' <- liftIO $ + traverse (readMaybeType sym "vector element" (shapeType elemShp)) xs' + sequence_ + [ matchArg opts sc cc cs prepost md (MIRVal elemShp x) y z + | (x, z) <- zip (V.toList xs'') zs ] + + (_, _, MS.SetupNull empty) -> absurd empty + (_, _, MS.SetupGlobal empty _) -> absurd empty + (_, _, MS.SetupCast empty _) -> absurd empty + (_, _, MS.SetupUnion empty _ _) -> absurd empty + (_, _, MS.SetupGlobalInitializer empty _) -> absurd empty + + _ -> failure (MS.conditionLoc md) =<< + mkStructuralMismatch opts cc sc cs actual expected expectedTy -- | For each points-to statement read the memory value through the -- given pointer (lhs) and match the value against the given pattern diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index 5daca1d080..5ddf1b6a21 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -120,11 +120,12 @@ typeOfSetupValue _mcc env _nameEnv val = Right mirTy -> return mirTy TypedTermSchema s -> X.throwM (MIRPolymorphicType s) tp -> X.throwM (MIRInvalidTypedTerm tp) + MS.SetupArray elemTy vs -> + pure $ Mir.TyArray elemTy (length vs) MS.SetupNull empty -> absurd empty MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct _ _ -> panic "typeOfSetupValue" ["structs not yet implemented"] - MS.SetupArray _ _ -> panic "typeOfSetupValue" ["arrays not yet implemented"] MS.SetupElem _ _ _ -> panic "typeOfSetupValue" ["elems not yet implemented"] MS.SetupField _ _ _ -> panic "typeOfSetupValue" ["fields not yet implemented"] MS.SetupCast empty _ -> absurd empty @@ -161,18 +162,13 @@ resolveSetupVal mcc env tyenv nameEnv val = MS.SetupNull empty -> absurd empty MS.SetupGlobal empty _ -> absurd empty MS.SetupStruct _ _ -> panic "resolveSetupValue" ["structs not yet implemented"] - MS.SetupArray () [] -> fail "resolveSetupVal: invalid empty array" - MS.SetupArray () vs -> do + MS.SetupArray elemTy vs -> do vals <- V.mapM (resolveSetupVal mcc env tyenv nameEnv) (V.fromList vs) Some (shp :: TypeShape tp) <- - case V.head vals of - MIRVal shp _ -> pure (Some shp) + pure $ tyToShape col elemTy - let mirTy :: Mir.Ty - mirTy = shapeMirTy shp - - vals' :: Vector (RegValue Sym tp) + let vals' :: Vector (RegValue Sym tp) vals' = V.map (\(MIRVal shp' val') -> case W4.testEquality shp shp' of Just Refl -> val' @@ -182,13 +178,15 @@ resolveSetupVal mcc env tyenv nameEnv val = , show shp' ]) vals - return $ MIRVal (ArrayShape (Mir.TyArray mirTy (V.length vals)) mirTy shp) + return $ MIRVal (ArrayShape (Mir.TyArray elemTy (V.length vals)) elemTy shp) (Mir.MirVector_Vector vals') MS.SetupElem _ _ _ -> panic "resolveSetupValue" ["elems not yet implemented"] MS.SetupField _ _ _ -> panic "resolveSetupValue" ["fields not yet implemented"] MS.SetupCast empty _ -> absurd empty MS.SetupUnion empty _ _ -> absurd empty MS.SetupGlobalInitializer empty _ -> absurd empty + where + col = mcc ^. mccRustModule . Mir.rmCS . Mir.collection resolveTypedTerm :: MIRCrucibleContext -> diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index c935340da2..211d82d2f2 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -61,7 +61,8 @@ import qualified SAWScript.Crucible.Common.Setup.Value as MS type instance MS.XSetupNull MIR = Void type instance MS.XSetupGlobal MIR = Void type instance MS.XSetupStruct MIR = () -type instance MS.XSetupArray MIR = () +-- The 'M.Ty' represents the type of array elements. +type instance MS.XSetupArray MIR = M.Ty type instance MS.XSetupElem MIR = () type instance MS.XSetupField MIR = () type instance MS.XSetupCast MIR = Void diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 898ed9eac5..9ccc5a5842 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -93,6 +93,7 @@ import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW -- Crucible import qualified Lang.Crucible.JVM as CJ import Mir.Intrinsics (MIR) +import qualified Mir.Mir as Mir import qualified SAWScript.Crucible.Common as CC import qualified SAWScript.Crucible.Common.MethodSpec as CMS import qualified SAWScript.Crucible.JVM.BuiltinsJVM as CJ @@ -3857,6 +3858,13 @@ primitives = Map.fromList , "verified is expected to perform the allocation." ] + , prim "mir_array_value" "MIRType -> [MIRValue] -> MIRValue" + (pureVal (CMS.SetupArray :: Mir.Ty -> [CMS.SetupValue MIR] -> CMS.SetupValue MIR)) + Experimental + [ "Create a SetupValue representing an array of the given type, with the" + , "given list of values as elements." + ] + , prim "mir_assert" "Term -> MIRSetup ()" (pureVal mir_assert) Experimental