Fixed a test case

dnezam · Sep 21, 2024 · 57a27a2 · 57a27a2
1 parent f1be5cb
commit 57a27a2
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 7 deletions.
diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
@@ -3150,7 +3150,9 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           case _ => enclosingType
         };
         if (forTrait) {
-          var selfFormal := if m.wasFunction then R.Formal.selfBorrowed else R.Formal.selfBorrowedMut;
+          // Mutability is required when not using raw pointers, even for functione, because
+          // --release optimisations sometimes removes the code to increment the reference counting on upcasting
+          var selfFormal := if m.wasFunction && ObjectType.RawPointers? then R.Formal.selfBorrowed else R.Formal.selfBorrowedMut;
           params := [selfFormal] + params;
         } else {
           var tpe := GenType(instanceType, GenTypeContext.default());
@@ -3161,7 +3163,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             // For raw pointers, no borrowing is necessary, because it implements the Copy type
           } else if selfId == "self" {
             if tpe.IsObjectOrPointer() { // For classes and traits
-              if m.wasFunction {
+              if m.wasFunction && ObjectType.RawPointers? {
                 tpe := R.SelfBorrowed;
               } else {
                 tpe := R.SelfBorrowedMut;
@@ -5202,10 +5204,15 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
               var onExpr, recOwnership, recIdents;
               if base.Trait? || base.Class? {
                 onExpr, recOwnership, recIdents := GenExpr(on, selfIdent, env, OwnershipOwned);
-                onExpr := read_macro.Apply1(onExpr);
+                if ObjectType.RawPointers? {
+                  onExpr := read_macro.Apply1(onExpr);
+                } else {
+                  onExpr := modify_macro.Apply1(onExpr);
+                }
                 readIdents := readIdents + recIdents;
               } else {
-                onExpr, recOwnership, recIdents := GenExpr(on, selfIdent, env, OwnershipBorrowed);
+                var expectedOnOwnership := if ObjectType.RawPointers? then OwnershipBorrowed else OwnershipBorrowedMut;
+                onExpr, recOwnership, recIdents := GenExpr(on, selfIdent, env, expectedOnOwnership);
                 readIdents := readIdents + recIdents;
               }
               r := fullPath.ApplyType(onTypeExprs).FSel(escapeName(name.name)).ApplyType(typeExprs).Apply([onExpr] + argExprs);
@@ -5225,7 +5232,11 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
                       case CallName(_, Some(tpe), _, _, _) =>
                         var typ := GenType(tpe, GenTypeContext.default());
                         if typ.IsObjectOrPointer() {
-                          onExpr := read_macro.Apply1(onExpr);
+                          if ObjectType.RawPointers? {
+                            onExpr := read_macro.Apply1(onExpr);
+                          } else {
+                            onExpr := modify_macro.Apply1(onExpr);
+                          }
                         }
                       case _ =>
                     }

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/externalclasses.rs
@@ -28,7 +28,7 @@ pub mod External {
 
       impl crate::External::Class::Container::GetValueHolder
         for ExternalPartialClass {
-        fn GetValue(&self) -> dafny_runtime::DafnyInt {
+        fn GetValue(&mut self) -> dafny_runtime::DafnyInt {
           ::dafny_runtime::int!(2)
         }
       }
@@ -97,7 +97,7 @@ pub mod ExternModuleWithOneClassToImport {
   }
   impl crate::ExternModuleWithOneClassToImport::TraitDefinedInModule
     for NonShareableBox {
-    fn Get(&self) -> ::dafny_runtime::DafnyString {
+    fn Get(&mut self) -> ::dafny_runtime::DafnyString {
       self.s.clone()
     }
     fn Put(&mut self, c: &::dafny_runtime::DafnyString) {