From 9d74cbd5433a8e62df93ac90e86c0c8b00bc58b1 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 24 Aug 2023 17:08:53 -0400 Subject: [PATCH] mir_array_value This adds support for a `mir_array_value` function in the MIR backend, which allows constructing array `SetupValue`s. This largely behaves like `llvm_array_value`s in the LLVM backend, but with the following differences: * Unlike in the LLVM backend, MIR arrays can have length 0. To account for this possibility, `mir_array_value` has a `MIRType` argument to ensure that SAW can always infer the type of the array, even if there are no element values from which to infer the type. Similarly, the SAW remote API's `array()` function now has an optional `element_type` kwarg that can be used to specify the element type in the event that there are no element values. * Because only the MIR backend makes use of the element type, this is encoded in the `XSetupArray` extension field. This checks off one box in #1859. --- doc/manual/manual.md | 7 ++ intTests/test_mir_verify_arrays/Makefile | 13 +++ .../test.linked-mir.json | 1 + intTests/test_mir_verify_arrays/test.rs | 16 ++++ intTests/test_mir_verify_arrays/test.saw | 80 ++++++++++++++++++ intTests/test_mir_verify_arrays/test.sh | 3 + saw-remote-api/CHANGELOG.md | 4 + saw-remote-api/python/CHANGELOG.md | 3 + saw-remote-api/python/saw_client/crucible.py | 24 ++++-- .../saw/test-files/mir_arrays.linked-mir.json | 1 + .../python/tests/saw/test-files/mir_arrays.rs | 16 ++++ .../python/tests/saw/test_mir_arrays.py | 82 +++++++++++++++++++ saw-remote-api/src/SAWServer.hs | 2 +- .../src/SAWServer/Data/SetupValue.hs | 4 +- .../src/SAWServer/JVMCrucibleSetup.hs | 2 +- .../src/SAWServer/LLVMCrucibleSetup.hs | 2 +- .../src/SAWServer/MIRCrucibleSetup.hs | 30 +++++-- src/SAWScript/Crucible/MIR/Override.hs | 46 +++++++---- .../Crucible/MIR/ResolveSetupValue.hs | 18 ++-- src/SAWScript/Crucible/MIR/Setup/Value.hs | 3 +- src/SAWScript/Interpreter.hs | 8 ++ 21 files changed, 321 insertions(+), 44 deletions(-) create mode 100644 intTests/test_mir_verify_arrays/Makefile create mode 100644 intTests/test_mir_verify_arrays/test.linked-mir.json create mode 100644 intTests/test_mir_verify_arrays/test.rs create mode 100644 intTests/test_mir_verify_arrays/test.saw create mode 100755 intTests/test_mir_verify_arrays/test.sh create mode 100644 saw-remote-api/python/tests/saw/test-files/mir_arrays.linked-mir.json create mode 100644 saw-remote-api/python/tests/saw/test-files/mir_arrays.rs create mode 100644 saw-remote-api/python/tests/saw/test_mir_arrays.py 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