Skip to content

Commit

Permalink
Fix: Arrays can be printed and modify_field standalone (#5848)
Browse files Browse the repository at this point in the history
### 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>
  • Loading branch information
MikaelMayer authored Oct 21, 2024
1 parent 7538a93 commit 77287d8
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 5 deletions.
17 changes: 13 additions & 4 deletions Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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}
}
};
}

Expand Down Expand Up @@ -4036,4 +4045,4 @@ impl<K: DafnyTypeEq, U: DafnyTypeEq> Map<K, U>
Map::from_hashmap_owned(new_map)
})
}
}
}
8 changes: 7 additions & 1 deletion Source/DafnyRuntime/DafnyRuntimeRust/src/tests/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down

0 comments on commit 77287d8

Please sign in to comment.