From 2871dee9698ce500f1f75cb59c0aeacc6f9f2de4 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 18 Sep 2024 14:06:10 -0500 Subject: [PATCH 1/3] Chore: refactor macro types This refactoring makes it possible to distinguish runtime types (in $crate) from any other type. I reviewed all the types one by one to ensure types not in the runtime have absolute paths. It will make maintenance easier. --- .../DafnyRuntime/DafnyRuntimeRust/src/lib.rs | 36 +++++++++---------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs index 2aaa1e80efe..eb18d07a321 100644 --- a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs +++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs @@ -322,7 +322,7 @@ impl AsRef for DafnyInt { #[macro_export] macro_rules! truncate { ($x:expr, $t:ty) => { - <$crate::DafnyInt as $crate::Into<$t>>::into($x) + <$crate::DafnyInt as ::std::convert::Into<$t>>::into($x) }; } @@ -594,10 +594,10 @@ impl DafnyInt { macro_rules! impl_dafnyint_from { () => {}; ($type:ident) => { - impl $crate::From<$type> for $crate::DafnyInt { + impl ::std::convert::From<$type> for $crate::DafnyInt { fn from(n: $type) -> Self { $crate::DafnyInt { - data: $crate::Rc::new(n.into()), + data: ::std::rc::Rc::new(n.into()), } } } @@ -1990,7 +1990,7 @@ impl DafnyPrint for LazyFieldWrapper { // Convert the DafnyPrint above into a macro so that we can create it for functions of any input arity macro_rules! dafny_print_function { ($($n:tt)*) => { - impl $crate::DafnyPrint for $crate::Rc B> { + impl $crate::DafnyPrint for ::std::rc::Rc B> { fn fmt_print(&self, f: &mut ::std::fmt::Formatter<'_>, _in_seq: bool) -> ::std::fmt::Result { write!(f, "") } @@ -2557,14 +2557,14 @@ macro_rules! ARRAY_GETTER_LENGTH { #[macro_export] macro_rules! array { ($($x:expr), *) => { - $crate::array::from_native($crate::Box::new([$($x), *])) + $crate::array::from_native(::std::boxed::Box::new([$($x), *])) } } macro_rules! ARRAY_INIT { {$length: ident, $inner: expr} => { $crate::array::initialize_box_usize($length, { - $crate::Rc::new(move |_| { $inner }) + ::std::rc::Rc::new(move |_| { $inner }) }) } } @@ -2579,10 +2579,10 @@ macro_rules! ARRAY_INIT_INNER { // Box<[Box<[Box<[T]>]>]> macro_rules! ARRAY_DATA_TYPE { ($length:ident) => { - $crate::Box<[T]> + ::std::boxed::Box<[T]> }; ($length:ident, $($rest_length:ident),+) => { - $crate::Box<[ARRAY_DATA_TYPE!($($rest_length),+)]> + ::std::boxed::Box<[ARRAY_DATA_TYPE!($($rest_length),+)]> }; } @@ -2606,8 +2606,8 @@ macro_rules! ARRAY_METHODS { pub fn placebos_box_usize( $length0: usize, $($length: usize),+ - ) -> $crate::Box<$ArrayType<$crate::MaybeUninit>> { - $crate::Box::new($ArrayType { + ) -> ::std::boxed::Box<$ArrayType<$crate::MaybeUninit>> { + ::std::boxed::Box::new($ArrayType { $($length: $length),+, data: INIT_ARRAY_DATA!($ArrayType, $length0, $($length),+), }) @@ -2676,7 +2676,7 @@ macro_rules! ARRAY_TO_VEC_LOOP { }; (@inner $self: ident, $outerTmp: ident, $data: expr $(, $rest_length_usize: ident)*) => { { - let mut tmp = $crate::Vec::new(); + let mut tmp = ::std::vec::Vec::new(); ARRAY_TO_VEC_LOOP!(@for $self, tmp, $data $(, $rest_length_usize)*); $outerTmp.push(tmp); } @@ -2684,7 +2684,7 @@ macro_rules! ARRAY_TO_VEC_LOOP { ($self: ident, $data: expr $(, $rest_length_usize: ident)*) => { { - let mut tmp = $crate::Vec::new(); + let mut tmp = ::std::vec::Vec::new(); ARRAY_TO_VEC_LOOP!(@for $self, tmp, $data $(, $rest_length_usize)*); tmp } @@ -2693,10 +2693,10 @@ macro_rules! ARRAY_TO_VEC_LOOP { macro_rules! ARRAY_TO_VEC_TYPE { ($length0: ident) => { - $crate::Vec + ::std::vec::Vec }; ($length0: ident $(, $res_length: ident)*) => { - $crate::Vec + ::std::vec::Vec } } @@ -2751,7 +2751,7 @@ macro_rules! ARRAY_DEF { $(($length, $length_usize)), + } } - impl $ArrayType { + impl $ArrayType { ARRAY_TO_VEC_WRAPPER!{ $(($length, $length_usize)), + } @@ -3111,7 +3111,7 @@ macro_rules! is_object { #[macro_export] macro_rules! cast_any { ($raw:expr) => { - $crate::Upcast::::upcast($crate::read!($raw)) + $crate::Upcast::::upcast($crate::read!($raw)) }; } // cast_any_object is meant to be used on references only, to convert any references (classes or traits)* @@ -3119,7 +3119,7 @@ macro_rules! cast_any { #[macro_export] macro_rules! cast_any_object { ($obj:expr) => { - $crate::UpcastObject::::upcast($crate::md!($obj)) + $crate::UpcastObject::::upcast($crate::md!($obj)) }; } @@ -3555,7 +3555,7 @@ macro_rules! rd { #[macro_export] macro_rules! refcount { ($x:expr) => { - $crate::Rc::strong_count(unsafe { $crate::rcmut::as_rc($x.0.as_ref().unwrap()) }) + ::std::rc::Rc::strong_count(unsafe { $crate::rcmut::as_rc($x.0.as_ref().unwrap()) }) }; } From 3ea9b6bc43501430a07073c4345dff178c795e22 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 18 Sep 2024 14:07:01 -0500 Subject: [PATCH 2/3] Removed warning --- Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs index 1cfcdff8943..2d61e01e680 100644 --- a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs +++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs @@ -853,9 +853,7 @@ mod tests { let o: Object = Object::new(s); let n: Object = upcast_object::()(o); let x = cast_object!(n, InternalOpaqueError); - let s2 = unsafe { - crate::dafny_runtime_conversions::object::dafny_class_to_struct(x) - }; + let s2 = crate::dafny_runtime_conversions::object::dafny_class_to_struct(x); assert_eq!(s2.message, "Hello, World!"); } } From c9fdfba62e19c5bca5b4cd37a74faeb33c48faa0 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 18 Sep 2024 15:19:24 -0500 Subject: [PATCH 3/3] Added smoke tests --- .../DafnyRuntimeRustTest/.gitignore | 1 + .../DafnyRuntimeRustTest/Cargo.lock | 133 ++++++++++++++++++ .../DafnyRuntimeRustTest/Cargo.toml | 7 + .../DafnyRuntimeRustTest/src/main.rs | 39 +++++ Source/DafnyRuntime/DafnyRuntimeRust/Makefile | 3 +- 5 files changed, 182 insertions(+), 1 deletion(-) create mode 100644 Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/.gitignore create mode 100644 Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.lock create mode 100644 Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.toml create mode 100644 Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/src/main.rs diff --git a/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/.gitignore b/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/.gitignore new file mode 100644 index 00000000000..9f970225adb --- /dev/null +++ b/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/.gitignore @@ -0,0 +1 @@ +target/ \ No newline at end of file diff --git a/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.lock b/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.lock new file mode 100644 index 00000000000..c1b0654506e --- /dev/null +++ b/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.lock @@ -0,0 +1,133 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "DafnyRuntimeRustTest" +version = "0.1.0" +dependencies = [ + "dafny_runtime", +] + +[[package]] +name = "as-any" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5b8a30a44e99a1c83ccb2a6298c563c888952a1c9134953db26876528f84c93a" + +[[package]] +name = "autocfg" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" + +[[package]] +name = "dafny_runtime" +version = "0.1.0" +dependencies = [ + "as-any", + "itertools", + "num", + "once_cell", + "paste", +] + +[[package]] +name = "either" +version = "1.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" + +[[package]] +name = "itertools" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" +dependencies = [ + "either", +] + +[[package]] +name = "num" +version = "0.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "35bd024e8b2ff75562e5f34e7f4905839deb4b22955ef5e73d2fea1b9813cb23" +dependencies = [ + "num-bigint", + "num-complex", + "num-integer", + "num-iter", + "num-rational", + "num-traits", +] + +[[package]] +name = "num-bigint" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" +dependencies = [ + "num-integer", + "num-traits", +] + +[[package]] +name = "num-complex" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "73f88a1307638156682bada9d7604135552957b7818057dcef22705b4d509495" +dependencies = [ + "num-traits", +] + +[[package]] +name = "num-integer" +version = "0.1.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" +dependencies = [ + "num-traits", +] + +[[package]] +name = "num-iter" +version = "0.1.45" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1429034a0490724d0075ebb2bc9e875d6503c3cf69e235a8941aa757d83ef5bf" +dependencies = [ + "autocfg", + "num-integer", + "num-traits", +] + +[[package]] +name = "num-rational" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f83d14da390562dca69fc84082e73e548e1ad308d24accdedd2720017cb37824" +dependencies = [ + "num-bigint", + "num-integer", + "num-traits", +] + +[[package]] +name = "num-traits" +version = "0.2.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" +dependencies = [ + "autocfg", +] + +[[package]] +name = "once_cell" +version = "1.19.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" + +[[package]] +name = "paste" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" diff --git a/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.toml b/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.toml new file mode 100644 index 00000000000..f8825f708b1 --- /dev/null +++ b/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "DafnyRuntimeRustTest" +version = "0.1.0" +edition = "2021" + +[dependencies] +dafny_runtime = {path= "../../DafnyRuntime/DafnyRuntimeRust"} \ No newline at end of file diff --git a/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/src/main.rs b/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/src/main.rs new file mode 100644 index 00000000000..87396df3fcf --- /dev/null +++ b/Source/DafnyRuntime.Tests/DafnyRuntimeRustTest/src/main.rs @@ -0,0 +1,39 @@ +use dafny_runtime::{Upcast, UpcastObject}; + + + +struct SmokeStruct { + pub i: i32, +} +pub struct OtherSmokeStruct(pub i32); + +impl UpcastObject for SmokeStruct { + dafny_runtime::UpcastObjectFn!(dyn ::std::any::Any); +} +impl Upcast for SmokeStruct { + dafny_runtime::UpcastFn!(dyn ::std::any::Any); +} + +#[test] +fn smoke_test() { + let mut x = ::dafny_runtime::dafny_runtime_conversions::object::boxed_struct_to_dafny_class(Box::new(SmokeStruct{i: 3})); + assert_eq!(::dafny_runtime::refcount!(x), 1); + let y = ::dafny_runtime::cast_any_object!(x); + assert_eq!(::dafny_runtime::refcount!(x), 2); + assert!(::dafny_runtime::is_object!(y, SmokeStruct)); + assert!(!::dafny_runtime::is_object!(y, OtherSmokeStruct)); + assert_eq!(::dafny_runtime::rd!(x).i, 3); + x = ::dafny_runtime::cast_object!(y, SmokeStruct); + assert_eq!(::dafny_runtime::rd!(x).i, 3); + let mut x = ::dafny_runtime::dafny_runtime_conversions::ptr::boxed_struct_to_dafny_class(Box::new(SmokeStruct{i: 3})); + let y = ::dafny_runtime::cast_any!(x); + assert!(::dafny_runtime::is!(y, SmokeStruct)); + assert!(!::dafny_runtime::is!(y, OtherSmokeStruct)); + assert_eq!(::dafny_runtime::read!(x).i, 3); + x = ::dafny_runtime::cast!(y, SmokeStruct); + assert_eq!(::dafny_runtime::read!(x).i, 3); + let z = ::dafny_runtime::truncate!(::dafny_runtime::int!(3), usize); + let a = ::dafny_runtime::array!(1, 2, 3); + assert_eq!(z, 3); + assert_eq!(::dafny_runtime::read!(a)[2], 3); +} diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/Makefile b/Source/DafnyRuntime/DafnyRuntimeRust/Makefile index 27cf8fe9d6a..f3b72d92998 100644 --- a/Source/DafnyRuntime/DafnyRuntimeRust/Makefile +++ b/Source/DafnyRuntime/DafnyRuntimeRust/Makefile @@ -18,4 +18,5 @@ update-system-module: build-system-module cp $(GENERATED_SYSTEM_MODULE_SOURCE) $(GENERATED_SYSTEM_MODULE_TARGET) test: - cargo test \ No newline at end of file + cargo test + (cd ../../DafnyRuntime.Tests/DafnyRuntimeRustTest; cargo test) \ No newline at end of file