Skip to content

Commit 245ad31

Browse files
authored
chore(rust): get latest fixes for dafny-runtime-rust (#1924)
1 parent 58b39a7 commit 245ad31

File tree

3 files changed

+36
-12
lines changed

3 files changed

+36
-12
lines changed

releases/rust/db_esdk/dafny_runtime_rust/Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "dafny-runtime"
3-
version = "0.3.0"
3+
version = "0.3.1"
44
edition = "2021"
55
keywords = ["dafny"]
66
license = "ISC AND (Apache-2.0 OR ISC)"

releases/rust/db_esdk/dafny_runtime_rust/src/lib.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3304,10 +3304,11 @@ impl<T: ?Sized> Object<T> {
33043304
// SAFETY: Not guaranteed unfortunately. But looking at the sources of from_raw as of today 10/24/2024
33053305
// it will will correctly rebuilt the Rc
33063306
let rebuilt = ::std::hint::black_box(unsafe { Rc::from_raw(pt) });
3307-
let previous_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt));
3307+
let _previous_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt));
33083308
::std::hint::black_box(increment_strong_count(pt));
3309-
let new_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt));
3310-
assert_eq!(new_strong_count, previous_strong_count + 1); // Will panic if not
3309+
let _new_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt));
3310+
#[cfg(not(feature = "sync"))]
3311+
assert_eq!(_new_strong_count, _previous_strong_count + 1); // Will panic if not. Asserted only in sequential mode
33113312
Object(Some(rebuilt))
33123313
}
33133314
}

releases/rust/db_esdk/dafny_runtime_rust/src/tests/mod.rs

Lines changed: 31 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@
44
#[cfg(test)]
55
mod tests {
66
use crate::*;
7+
#[cfg(feature = "sync")]
8+
use std::thread;
79

810
#[test]
911
fn test_int() {
@@ -40,22 +42,22 @@ mod tests {
4042
let b_copy_3 = b.clone();
4143
let a_copy_4 = a.clone();
4244
let b_copy_4 = b.clone();
43-
let handle_ab = std::thread::spawn(move || {
45+
let handle_ab = thread::spawn(move || {
4446
let a_plus_b = a_copy_1.concat(&b_copy_1);
4547
let a_plus_b_vec = a_plus_b.to_array();
4648
a_plus_b_vec
4749
});
48-
let handle_ba = std::thread::spawn(move || {
50+
let handle_ba = thread::spawn(move || {
4951
let b_plus_a = b_copy_2.concat(&a_copy_2);
5052
let b_plus_a_vec = b_plus_a.to_array();
5153
b_plus_a_vec
5254
});
53-
let handle_ab_2 = std::thread::spawn(move || {
55+
let handle_ab_2 = thread::spawn(move || {
5456
let a_plus_b = a_copy_3.concat(&b_copy_3);
5557
let a_plus_b_vec = a_plus_b.to_array();
5658
a_plus_b_vec
5759
});
58-
let handle_ba_2 = std::thread::spawn(move || {
60+
let handle_ba_2 = thread::spawn(move || {
5961
let b_plus_a = b_copy_4.concat(&a_copy_4);
6062
let b_plus_a_vec = b_plus_a.to_array();
6163
b_plus_a_vec
@@ -1293,9 +1295,30 @@ mod tests {
12931295
let c3 = c;
12941296
assert_eq!(c3, c2);
12951297
}
1296-
/*impl GeneralTrait for Rc<ADatatype> {
1297-
fn _clone(&self) -> Box<dyn GeneralTrait> {
1298-
Box::new(self.as_ref().clone())
1298+
1299+
#[cfg(feature = "sync")]
1300+
#[test]
1301+
fn test_object_share_async() {
1302+
let obj = ClassWrapper::constructor_object(53);
1303+
let objClone = obj.clone();
1304+
1305+
let handle: thread::JoinHandle<i32> = thread::spawn(move || {
1306+
// Thread code here
1307+
let mut result: *const ClassWrapper<i32> = objClone.as_ref();
1308+
for _i in 0..10000 {
1309+
let obj2 = Object::from_ref(objClone.as_ref());
1310+
result = obj2.as_ref() as *const ClassWrapper<i32>;
1311+
}
1312+
result as i32
1313+
});
1314+
let mut result: *const ClassWrapper<i32> = obj.as_ref();
1315+
for _i in 0..10000 {
1316+
let obj2 = Object::from_ref(obj.as_ref());
1317+
result = obj2.as_ref() as *const ClassWrapper<i32>;
12991318
}
1300-
}*/
1319+
1320+
// Wait for thread to finish
1321+
assert_eq!(handle.join().unwrap(), result as i32);
1322+
assert_eq!(result as i32, obj.as_ref() as *const ClassWrapper<i32> as i32);
1323+
}
13011324
}

0 commit comments

Comments
 (0)