chore: updates for latest dafny-rust - Sync and Send (#772)

Author: ajewellamz

.github/actions/build_dafny_from_source/action.yml

@@ -1,67 +1,56 @@
-#
-# This local action builds Dafny from source
-# rather than using the setup-dafny-action.
-# Currently it's only used to test Rust support
-# against a feature branch of Dafny.
-#
-
 name: "Build Dafny from source"
-description: "Drop-in replacement for setup-dafny-action that builds the given branch of Dafny from source"
+description: "Builds the given branch of Dafny from source"
 inputs:
-  dafny:
-    description: "The Dafny branch to use"
+  dafny-version:
+    description: "Dafny version to build from source"
+    required: true
+    type: string
+  ref:
+    description: "The Dafny branch, tag or SHA to build"
     required: true
     type: string
 runs:
   using: "composite"
   steps:
+    - uses: actions/setup-java@v3
+      with:
+        distribution: "corretto"
+        java-version: "17"
+
     - name: Checkout Dafny
       uses: actions/checkout@v4
       with:
         repository: dafny-lang/dafny
         path: dafny
-        ref: ${{ inputs.dafny }}
-
-    - name: Load Z3
-      shell: bash
-      run: |
-        sudo apt-get update && sudo apt-get install -qq libarchive-tools
-        mkdir -p dafny/Binaries/z3/bin
-        wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
-        mv z3-4.12.1 dafny/Binaries/z3/bin/
-        chmod +x dafny/Binaries/z3/bin/z3-4.12.1
-        mkdir -p unzippedRelease/dafny/z3/bin
-        ln dafny/Binaries/z3/bin/z3-4.12.1 unzippedRelease/dafny/z3/bin/z3-4.12.1
+        ref: ${{ inputs.ref }}
 
-    - name: Setup dotnet
-      uses: actions/setup-dotnet@v4
+    - name: Setup Z3
+      uses: cda-tum/setup-[email protected]
       with:
-        dotnet-version: 6.0.x
+        version: 4.12.1
 
     - name: Build Dafny
       shell: bash
       run: |
-        dotnet build dafny/Source/Dafny.sln
+        make -C dafny exe
 
-    - name: Add dafny to PATH
+    - name: Add dafny to PATH (non-Windows)
+      if: runner.os != 'Windows'
       shell: bash
       run: |
         echo ${{ github.workspace }}/dafny/Scripts >> $GITHUB_PATH
+    - name: Add dafny to PATH (Windows)
+      if: runner.os == 'Windows'
+      shell: pwsh
+      run: |
+        Add-Content $env:GITHUB_PATH "${{ github.workspace }}/dafny/Scripts"
 
-    # Hard-coding this for now since it's a pain to extract from an arbitrary branch
     - name: Export DAFNY_VERSION
       shell: bash
       run: |
-        echo "DAFNY_VERSION=4.7.0" >> $GITHUB_ENV
+        echo "DAFNY_VERSION=${{ inputs.dafny-version }}" >> $GITHUB_ENV
 
-    # update the copy of the Rust runtime we have inside TestModels
-    # (since it's not published yet)
-    # TODO: Temporarily not doing this because we need a targeted fix to the runtime,
-    # but can't pick it up by moving to a newer Dafny commit because that would pull in
-    # other breaking changes.
-
-#    - name: Update dafny_runtime_rust
-#      shell: bash
-#      run: |
-#        rm -rf TestModels/dafny-dependencies/dafny_runtime_rust
-#        cp -r dafny/Source/DafnyRuntime/DafnyRuntimeRust TestModels/dafny-dependencies/dafny_runtime_rust
+    - name: Install reportgenerator
+      shell: bash
+      run: |
+        dotnet tool install -g dafny-reportgenerator --version 1.*

.github/workflows/pull.yml

@@ -53,7 +53,7 @@ jobs:
         # Rust code generation is under development and depends on pending changes to the
         # Dafny Rust code generation, so we test on a specific unreleased commit instead.
         dafny-version:
-          - d07403b6d6606257e1b5aada4d0156901f4a17de
+          - nightly-2025-01-30-7db1e5f
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}

.github/workflows/push.yml

@@ -55,7 +55,7 @@ jobs:
         # Rust code generation is under development and depends on pending changes to the
         # Dafny Rust code generation, so we test on a specific unreleased commit instead.
         dafny-version:
-          - 5f2330113320f2af0476473fd267b5b547f94cba
+          - nightly-2025-01-30-7db1e5f
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}

.github/workflows/test_models_rust_tests.yml

@@ -51,10 +51,10 @@ jobs:
         with:
           submodules: recursive
 
-      - name: Setup Dafny (build from source)
-        uses: ./.github/actions/build_dafny_from_source
+      - name: Setup Dafny
+        uses: dafny-lang/[email protected]
         with:
-          dafny: ${{ inputs.dafny }}
+          dafny-version: ${{ inputs.dafny }}
 
       - name: Set up Rust
         uses: actions-rust-lang/setup-rust-toolchain@v1

SmithyDafnyMakefile.mk

@@ -631,7 +631,7 @@ _mv_implementation_rust:
 # Pre-process the Dafny-generated Rust code to remove them.
 	sed -i -e 's/[[:space:]]*$$//' runtimes/rust/src/implementation_from_dafny.rs 
 	rm -f runtimes/rust/src/implementation_from_dafny.rs-e
-#	rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs
+	rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs
 	rm -rf implementation_from_dafny-rust
 
 build_rust:
@@ -643,6 +643,11 @@ test_rust:
 	cd runtimes/rust; \
 	cargo test --release -- --nocapture
 
+test_rust_debug:
+	rustc --version
+	cd runtimes/rust; \
+	cargo test -- --nocapture
+
 ########################## Cleanup targets
 
 _clean:

TestModels/dafny-dependencies/dafny_runtime_rust/Cargo.toml

@@ -9,4 +9,7 @@ num = "0.4"
 itertools = "0.11.0"
 
 [features]
+# Use `dafny translate rs --rust-sync --include-runtime file.dfy`
+# to compile to code where values can be sent safely through threads
+# This will include the runtime with the sync feature
 sync = []

TestModels/dafny-dependencies/dafny_runtime_rust/src/lib.rs

@@ -56,6 +56,9 @@ pub use ::std::cell::UnsafeCell;
 pub struct UnsafeCell<T: ?Sized> {
     data: ::std::cell::UnsafeCell<T>, // UnsafeCell for interior mutability
 }
+// SAFETY: UnsafeCell is not possibly sync normally.
+// However, we use it only for raw pointers, and fields and access to read and write
+// to fields will be subject to mutexes in any cases.
 #[cfg(feature = "sync")]
 unsafe impl<T: ?Sized> Sync for UnsafeCell<T> where T: Send {}
 #[cfg(feature = "sync")]
@@ -740,10 +743,10 @@ where
         values: Rc<Vec<T>>,
     },
     ConcatSequence {
-        left: Rc<UnsafeCell<Sequence<T>>>,
-        right: Rc<UnsafeCell<Sequence<T>>>,
+        left: Rc<RefCell<Sequence<T>>>,
+        right: Rc<RefCell<Sequence<T>>>,
         length: SizeT,
-        boxed: Rc<RefCell<Option<Rc<Vec<T>>>>>,
+        cache: Rc<RefCell<Option<Rc<Vec<T>>>>>,
     },
 }
 
@@ -800,12 +803,12 @@ where
             values: Rc::new(values),
         }
     }
-    pub fn new_concat_sequence(left: &Sequence<T>, right: &Sequence<T>) -> Sequence<T> {
+    pub(crate) fn new_concat_sequence(left: &Sequence<T>, right: &Sequence<T>) -> Sequence<T> {
         Sequence::ConcatSequence {
-            left: Rc::new(UnsafeCell::new(left.clone())),
-            right: Rc::new(UnsafeCell::new(right.clone())),
+            left: Rc::new(RefCell::new(left.clone())),
+            right: Rc::new(RefCell::new(right.clone())),
             length: left.cardinality_usize() + right.cardinality_usize(),
-            boxed: Rc::new(RefCell::new(None)),
+            cache: Rc::new(RefCell::new(None)),
         }
     }
     pub fn to_array(&self) -> Rc<Vec<T>> {
@@ -818,40 +821,49 @@ where
             }
             Sequence::ConcatSequence {
                 length,
-                boxed,
+                cache,
                 left,
                 right,
             } => {
                 #[cfg(feature = "sync")]
-                let into_boxed = boxed.as_ref();
-                #[cfg(feature = "sync")]
-                let into_boxed_borrowed = into_boxed;
-                #[cfg(feature = "sync")]
-                let mut guard = into_boxed_borrowed.lock().unwrap();
-                #[cfg(feature = "sync")]
-                let borrowed: Option<&Rc<Vec<T>>> = guard.as_ref();
+                {
+                    let guard = cache.as_ref().lock().unwrap();
+                    let cache_borrow: Option<&Rc<Vec<T>>> = guard.as_ref();
+                    if let Some(cache) = cache_borrow {
+                        return Rc::clone(cache);
+                    }
+                }
 
                 #[cfg(not(feature = "sync"))]
-                let into_boxed = boxed.as_ref().clone();
-                #[cfg(not(feature = "sync"))]
-                let into_boxed_borrowed = into_boxed.borrow();
-                #[cfg(not(feature = "sync"))]
-                let borrowed: Option<&Rc<Vec<T>>> = into_boxed_borrowed.as_ref();
-                if let Some(cache) = borrowed.as_ref() {
-                    return Rc::clone(cache);
+                {
+                    let cache_opened = cache.as_ref().clone();
+                    let cache_opened_borrowed = cache_opened.borrow();
+                    let cache_borrow: Option<&Rc<Vec<T>>> = cache_opened_borrowed.as_ref();
+                    if let Some(cache) = cache_borrow {
+                        return Rc::clone(cache);
+                    }
                 }
                 // Let's create an array of size length and fill it up recursively
                 // We don't materialize nested arrays because most of the time they are forgotten
                 let mut array: Vec<T> = Vec::with_capacity(*length);
-                Sequence::<T>::append_recursive_safe(&mut array, &borrowed, left, right);
+                Sequence::<T>::append_recursive_safe(&mut array, &None, left, right);
                 let result = Rc::new(array);
-                let mutable_left: *mut Sequence<T> = left.get();
-                let mutable_right: *mut Sequence<T> = right.get();
-                // safety: Once the array is computed, left and right won't ever be read again.
-                unsafe { *mutable_left = seq!() };
-                unsafe { *mutable_right = seq!() };
                 #[cfg(not(feature = "sync"))]
-                let mut guard = boxed.borrow_mut();
+                {
+                    *left.borrow_mut() = seq!();
+                    *right.borrow_mut() = seq!();
+                }
+                #[cfg(feature = "sync")]
+                {
+                    let mut left_guard = left.as_ref().lock().unwrap();
+                    let mut right_guard = right.as_ref().lock().unwrap();
+                    *left_guard = seq!();
+                    *right_guard = seq!();
+                }
+                #[cfg(not(feature = "sync"))]
+                let mut guard = cache.borrow_mut();
+                #[cfg(feature = "sync")]
+                let mut guard = cache.as_ref().lock().unwrap();
                 *guard = Some(result.clone());
                 result
             }
@@ -860,19 +872,28 @@ where
 
     pub fn append_recursive_safe(
         array: &mut Vec<T>,
-        borrowed: &Option<&Rc<Vec<T>>>,
-        left: &Rc<UnsafeCell<Sequence<T>>>,
-        right: &Rc<UnsafeCell<Sequence<T>>>,
+        cache_borrow: &Option<&Rc<Vec<T>>>,
+        left: &Rc<RefCell<Sequence<T>>>,
+        right: &Rc<RefCell<Sequence<T>>>,
     ) {
-        if let Some(values) = borrowed.as_ref() {
+        if let Some(values) = cache_borrow.as_ref() {
             for value in values.iter() {
                 array.push(value.clone());
             }
             return;
         }
-        // safety: When a concat is initialized, the left and right are well defined
-        Sequence::<T>::append_recursive(array, unsafe { &mut *left.get() });
-        Sequence::<T>::append_recursive(array, unsafe { &mut *right.get() });
+        #[cfg(not(feature = "sync"))]
+        {
+            Sequence::<T>::append_recursive(array, &left.as_ref().borrow());
+            Sequence::<T>::append_recursive(array, &right.as_ref().borrow());
+        }
+        #[cfg(feature = "sync")]
+        {
+            let left_guard = left.as_ref().lock().unwrap();
+            let right_guard = right.as_ref().lock().unwrap();
+            Sequence::<T>::append_recursive(array, &left_guard);
+            Sequence::<T>::append_recursive(array, &right_guard);
+        }
     }
 
     pub fn append_recursive(array: &mut Vec<T>, this: &Sequence<T>) {
@@ -885,7 +906,7 @@ where
                 }
             }
             Sequence::ConcatSequence {
-                boxed, left, right, ..
+                cache: boxed, left, right, ..
             } =>
             // Let's create an array of size length and fill it up recursively
             {
@@ -904,20 +925,11 @@ where
                 let into_boxed_borrowed = into_boxed.borrow();
                 #[cfg(not(feature = "sync"))]
                 let borrowed: Option<&Rc<Vec<T>>> = into_boxed_borrowed.as_ref();
-                if let Some(values) = borrowed.as_ref() {
-                    for value in values.iter() {
-                        array.push(value.clone());
-                    }
-                    return;
-                }
-                // safety: When a concat is initialized, the left and right are well defined
-                Sequence::<T>::append_recursive(array, unsafe { &mut *left.get() });
-                Sequence::<T>::append_recursive(array, unsafe { &mut *right.get() });
+                Self::append_recursive_safe(array, &borrowed, left, right);
             }
         }
     }
-    /// Returns the cardinality of this [`Sequence<T>`].
-    // The cardinality returns the length of the sequence
+    /// Returns the cardinality or length of this [`Sequence<T>`].
     pub fn cardinality_usize(&self) -> SizeT {
         match self {
             Sequence::ArraySequence { values, .. } =>
@@ -1917,14 +1929,6 @@ pub fn dafny_rational_to_int(r: &BigRational) -> BigInt {
     euclidian_division(r.numer().clone(), r.denom().clone())
 }
 
-pub fn nullable_referential_equality<T: ?Sized>(left: Option<Rc<T>>, right: Option<Rc<T>>) -> bool {
-    match (left, right) {
-        (Some(l), Some(r)) => Rc::ptr_eq(&l, &r),
-        (None, None) => true,
-        _ => false,
-    }
-}
-
 pub fn euclidian_division<A: Signed + Zero + One + Clone + PartialEq>(a: A, b: A) -> A {
     if !a.is_negative() {
         if !b.is_negative() {
@@ -2131,16 +2135,6 @@ impl<T: DafnyPrint> Display for DafnyPrintWrapper<&T> {
     }
 }
 
-// from gazebo
-#[inline]
-pub unsafe fn transmute_unchecked<A, B>(x: A) -> B {
-    assert_eq!(std::mem::size_of::<A>(), std::mem::size_of::<B>());
-    debug_assert_eq!(0, (&x as *const A).align_offset(std::mem::align_of::<B>()));
-    let b = std::ptr::read(&x as *const A as *const B);
-    std::mem::forget(x);
-    b
-}
-
 pub trait DafnyPrint {
     fn fmt_print(&self, f: &mut Formatter<'_>, in_seq: bool) -> std::fmt::Result;
 
@@ -3237,7 +3231,6 @@ macro_rules! cast_any_object {
     };
 }
 
-
 // When initializing an uninitialized field for the first time,
 // we ensure we don't drop the previous content
 // This is problematic if the same field is overwritten multiple times
@@ -3665,7 +3658,9 @@ pub struct AllocationTracker {
 }
 
 #[cfg(feature = "sync")]
-pub fn allocate_object_track<T: 'static + Sync + Send>(allocation_tracker: &mut AllocationTracker) -> Object<T> {
+pub fn allocate_object_track<T: 'static + Sync + Send>(
+    allocation_tracker: &mut AllocationTracker,
+) -> Object<T> {
     let res = allocate_object::<T>();
     allocation_tracker
         .allocations