From 77287d8c9dc2785175d2db20ec4f7490df19fbe1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <MikaelMayer@users.noreply.github.com>
Date: Mon, 21 Oct 2024 18:05:45 -0500
Subject: [PATCH 1/2] Fix: Arrays can be printed and modify_field standalone
 (#5848)

### Description
A previous update forced the `T` under `Object<T>` to implement
`UpcastObject<dyn Any>` to be able to print it.
However, this trait was never implemented on objects. Arrays can be
converted to objects but it's not possible to cast them down to arrays
again, because arrays are traits in Rust (dynamic pointers).
Until we wrap arrays with a newtype to cast them back to a regular
struct, we can fix the Dafny runtime so that they are still printed as
"object"

Second, modify-field!() at the end of a block was triggering parsing
issues. I added a block wrapper in the macro to prevent that issue.

### How has this been tested?
Two tests added in the runtime.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---
 Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs | 17 +++++++++++++----
 .../DafnyRuntimeRust/src/tests/mod.rs           |  8 +++++++-
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
index aac8137d164..13745ff9c0b 100644
--- a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
+++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
@@ -3450,6 +3450,13 @@ impl <T: ?Sized + UpcastObject<dyn Any>> DafnyPrint for Object<T> {
         }
     }
 }
+
+impl <T: DafnyType> DafnyPrint for Object<[T]> {
+    fn fmt_print(&self, f: &mut Formatter<'_>, _in_seq: bool) -> std::fmt::Result {
+        write!(f, "<object>")
+    }
+}
+
 impl UpcastObject<dyn Any> for String {
     fn upcast(&self) -> Object<dyn Any> {
         // SAFETY: RC was just created
@@ -3642,9 +3649,11 @@ macro_rules! rd {
 #[macro_export]
 macro_rules! modify_field {
     ($pointer:expr, $rhs:expr) => {
-        let lhs = $pointer.get();
-        let rhs = $rhs;
-        unsafe {*lhs = rhs}
+        {
+            let lhs = $pointer.get();
+            let rhs = $rhs;
+            unsafe {*lhs = rhs}
+        }
     };
 }
 
@@ -4036,4 +4045,4 @@ impl<K: DafnyTypeEq, U: DafnyTypeEq> Map<K, U>
             Map::from_hashmap_owned(new_map)
         })
     }
-}
+}
\ No newline at end of file
diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
index 7b3efbce953..d287da43dde 100644
--- a/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
+++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
@@ -478,7 +478,9 @@ mod tests {
         assert_eq!(rd!(c).constant_plus_x(), int!(42));
         md!(c).increment_x();
         assert_eq!(rd!(c).constant_plus_x(), int!(43));
-        modify_field!(rd!(c).x,int!(40));
+        if true {
+          modify_field!(rd!(c).x,int!(40))
+        }
         assert_eq!(rd!(c).constant_plus_x(), int!(82));
         modify_field!(rd!(c).t,54);
         assert_eq!(read_field!(rd!(c).t), 54);
@@ -829,6 +831,7 @@ mod tests {
 
         let objects: Set<Object<dyn ::std::any::Any>> = crate::set!{y.clone(), cast_any_object!(x.clone())};
         assert_eq!(objects.cardinality_usize(), 1);
+        test_dafny_type(a.clone());
     }
 
     pub struct NodeRawMut {
@@ -890,6 +893,9 @@ mod tests {
     // Tests that we can compose Dafny types, like a sequence of maps
     fn _test<X: DafnyTypeEq, Y: DafnyType>(_input: Sequence<Map<X, Y>>) {
     }
+    // Tests that the input type is a DafnyType
+    fn test_dafny_type<X: DafnyType>(_input: X) {
+    }
 
     #[derive(Clone)]
     pub struct InternalOpaqueError {

From a38e8a4b20d5681cfcc4bf2902e5ac55d7baf3e4 Mon Sep 17 00:00:00 2001
From: Siva Somayyajula <ssomayya@cs.cmu.edu>
Date: Wed, 23 Oct 2024 13:50:16 -0400
Subject: [PATCH 2/2] Publishing nightly builds from 4.9 release branch (#5852)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

### Description
<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->
<!-- Is this a bug fix for an issue visible in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->

Does exactly what it says on the tin.

### How has this been tested?
<!-- Tests can be added to
`Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to
`Source/*.Test/…` and run with `dotnet test` -->

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Siva Somayyajula <somayyas@amazon.com>
---
 .github/workflows/nightly-build.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/nightly-build.yml b/.github/workflows/nightly-build.yml
index 311a0656713..9dafc3d3086 100644
--- a/.github/workflows/nightly-build.yml
+++ b/.github/workflows/nightly-build.yml
@@ -23,11 +23,11 @@ on:
   workflow_dispatch:
 
 jobs:
-  nightly-build-for-master:
+  nightly-build-for-4-9:
     if: github.repository_owner == 'dafny-lang'
     uses: ./.github/workflows/nightly-build-reusable.yml
     with:
-      ref: master
+      ref: 4.9
       publish-prerelease: true
     secrets:
       nuget_api_key: ${{ secrets.NUGET_API_KEY }}