Feat: Ability to emit sync-compatible Rust code.

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy

@@ -236,6 +236,7 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
   datatype PointerType = Raw | RcMut
   datatype CharType = UTF16 | UTF32
   datatype RootType = RootCrate | RootPath(moduleName: string)
+  datatype SyncType = NoSync | Sync
 
   datatype GenTypeContext =
     GenTypeContext(forTraitParents: bool)
@@ -594,6 +595,8 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
   }
 
   function CoerceImpl(
+    rc: R.Type -> R.Type,
+    rcNew: R.Expr -> R.Expr,
     rTypeParamsDecls: seq<R.TypeParamDecl>,
     datatypeName: string,
     datatypeType: R.Type,
@@ -614,15 +617,15 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
              "coerce", rCoerceTypeParams,
              coerceArguments,
              Some(
-               R.Rc(
+               rc(
                  R.ImplType(
                    R.FnType(
                      [datatypeType],
                      R.TypeApp(R.TIdentifier(datatypeName), coerceTypes))))),
              Some(
-               R.RcNew(R.Lambda([R.Formal("this", R.SelfOwned)],
-                                Some(R.TypeApp(R.TIdentifier(datatypeName), coerceTypes)),
-                                coerceImplBody)))))]
+               rcNew(R.Lambda([R.Formal("this", R.SelfOwned)],
+                              Some(R.TypeApp(R.TIdentifier(datatypeName), coerceTypes)),
+                              coerceImplBody)))))]
       ))
   }
 

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy

@@ -77,7 +77,7 @@ module FactorPathsOptimizationTest {
                 "dummy", std_any_Any.AsType(),
                 StmtExpr(
                   DeclareVar(
-                    MUT, "doit", Some(std_rc_Rc.AsType().Apply1(TIdentifier("unknown"))),
+                    MUT, "doit", Some(RcType.Apply1(TIdentifier("unknown"))),
                     Some(
                       Identifier("something").ApplyType(
                         [ DynType(std_default_Default.AsType())
@@ -95,7 +95,7 @@ module FactorPathsOptimizationTest {
         NoDoc, NoAttr,
         "onemodule", [
           UseDecl(Use(PUB, std_any_Any)),
-          UseDecl(Use(PUB, std_rc_Rc)),
+          UseDecl(Use(PUB, RcPath)),
           UseDecl(Use(PUB, std_default_Default)),
           UseDecl(Use(PUB, dafny_runtime.MSel("rd"))),
           UseDecl(Use(PUB, dafny_runtime.MSel("DafnyString"))),

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-rast.dfy

@@ -608,8 +608,10 @@ module RAST
   const SelfBorrowedMut := BorrowedMut(SelfOwned)
 
   const RcPath := std.MSel("rc").MSel("Rc")
+  const ArcPath := std.MSel("sync").MSel("Arc")
 
   const RcType := RcPath.AsType()
+  const ArcType := ArcPath.AsType()
 
   const ObjectPath: Path := dafny_runtime.MSel("Object")
 
@@ -629,9 +631,6 @@ module RAST
     PtrPath.AsType().Apply([underlying])
   }
 
-  function Rc(underlying: Type): Type {
-    TypeApp(RcType, [underlying])
-  }
   function RefCell(underlying: Type): Type {
     TypeApp(RefcellType, [underlying])
   }
@@ -822,7 +821,7 @@ module RAST
       || (TMetaData? && (copySemantics || display.CanReadWithoutClone()))
     }
     predicate IsRcOrBorrowedRc() {
-      (TypeApp? && baseName == RcType) ||
+      IsRc() ||
       (Borrowed? && underlying.IsRcOrBorrowedRc()) ||
       (TSynonym? && base.IsRcOrBorrowedRc())
     }
@@ -1054,7 +1053,7 @@ module RAST
     }
 
     predicate IsRc() {
-      this.TypeApp? && this.baseName == RcType && |arguments| == 1
+      TypeApp? && (baseName == RcType || baseName == ArcType) && |arguments| == 1
     }
     function RcUnderlying(): Type
       requires IsRc()
@@ -1083,6 +1082,8 @@ module RAST
   const Eq := std.MSel("cmp").MSel("Eq").AsType()
   const Hash := std.MSel("hash").MSel("Hash").AsType()
   const DafnyInt := dafny_runtime.MSel("DafnyInt").AsType()
+  const SyncType := std.MSel("marker").MSel("Sync").AsType()
+  const SendType := std.MSel("marker").MSel("Send").AsType()
 
   function SystemTuple(elements: seq<Expr>): Expr {
     var size := Strings.OfNat(|elements|);
@@ -1889,18 +1890,8 @@ module RAST
     MaybePlaceboPath.FSel("from").Apply1(underlying)
   }
 
-  const std_rc := std.MSel("rc")
-
-  const std_rc_Rc := std_rc.MSel("Rc")
-
-  const std_rc_Rc_new := std_rc_Rc.FSel("new")
-
   const std_default_Default_default := std_default_Default.FSel("default").Apply0()
 
-  function RcNew(underlying: Expr): Expr {
-    Call(std_rc_Rc_new, [underlying])
-  }
-
   function IntoUsize(underlying: Expr): Expr {
     dafny_runtime.MSel("DafnyUsize").FSel("into_usize").Apply1(underlying)
   }

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy

@@ -19,6 +19,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
     const charType: CharType
     const pointerType: PointerType
     const rootType: RootType
+    const syncType: SyncType
 
     const thisFile: R.Path := if rootType.RootCrate? then R.crate else R.crate.MSel(rootType.moduleName)
     const DafnyChar := if charType.UTF32? then "DafnyChar" else "DafnyCharUTF16"
@@ -59,15 +60,28 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
     const downcast :=
       if pointerType.Raw? then "cast!" else "cast_object!"
 
+    const rcPath := if syncType.NoSync? then R.RcPath else R.ArcPath
+    const rcType := rcPath.AsType()
+    const rcExpr := rcPath.AsExpr()
+
+    const rc := (underlying: R.Type) => rcType.Apply([underlying])
+    const rcNew := (underlying: R.Expr) => rcExpr.FSel("new").Apply([underlying])
+    const SyncSendType := R.IntersectionType(R.SyncType, R.SendType)
+    const AnyTrait := if syncType.NoSync? then
+                        R.dafny_runtime.MSel("Any").AsType()
+                      else
+                        R.IntersectionType(R.dafny_runtime.MSel("Any").AsType(), SyncSendType)
+    const DynAny := R.dafny_runtime.MSel("DynAny").AsType()
 
     var error: Option<string>
 
     var optimizations: seq<R.Mod -> R.Mod>
 
-    constructor(charType: CharType, pointerType: PointerType, rootType: RootType) {
+    constructor(charType: CharType, pointerType: PointerType, rootType: RootType, syncType: SyncType) {
       this.charType := charType;
       this.pointerType := pointerType;
       this.rootType := rootType;
+      this.syncType := syncType;
       this.error := None; // If error, then the generated code contains <i>Unsupported: .*</i>
       this.optimizations := [
         ExpressionOptimization.apply,
@@ -479,13 +493,13 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           R.ImplDecl(
             R.ImplFor(
               rTypeParamsDecls,
-              R.dafny_runtime.MSel(Upcast).AsType().Apply([R.DynType(R.AnyTrait)]),
+              R.dafny_runtime.MSel(Upcast).AsType().Apply([DynAny]),
               R.TypeApp(genSelfPath, rTypeParams),
               [
                 R.ImplMemberMacro(
                   R.dafny_runtime
                   .MSel(UpcastFnMacro).AsExpr()
-                  .Apply1(R.ExprFromType(R.DynType(R.AnyTrait))))
+                  .Apply1(R.ExprFromType(DynAny)))
               ]
             )
           )
@@ -884,7 +898,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         if |ctor.args| == 0 {
           var instantiation := R.StructBuild(R.Identifier(datatypeName).FSel(escapeName(ctor.name)), []);
           if IsRcWrapped(c.attributes) {
-            instantiation := R.RcNew(instantiation);
+            instantiation := rcNew(instantiation);
           }
           singletonConstructors := singletonConstructors + [
             instantiation
@@ -1048,7 +1062,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           coerceArguments := coerceArguments + [
             R.Formal(
               coerceFormal,
-              R.Rc(R.IntersectionType(R.ImplType(R.FnType([rTypeArg], rCoerceType)), R.StaticTrait)))
+              rc(R.IntersectionType(R.ImplType(R.FnType([rTypeArg], rCoerceType)), R.StaticTrait)))
           ];
         }
         if |unusedTypeParams| > 0 {
@@ -1225,14 +1239,14 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           R.Identifier("this"),
           coerceImplBodyCases);
         s := s + [
-          CoerceImpl(rTypeParamsDecls, datatypeName, datatypeType, rCoerceTypeParams, coerceArguments, coerceTypes, coerceImplBody)
+          CoerceImpl(rc, rcNew, rTypeParamsDecls, datatypeName, datatypeType, rCoerceTypeParams, coerceArguments, coerceTypes, coerceImplBody)
         ];
       }
 
       if |singletonConstructors| == |c.ctors| {
         var instantiationType :=
           if IsRcWrapped(c.attributes) then
-            R.Rc(datatypeType)
+            rc(datatypeType)
           else
             datatypeType;
         s := s + [
@@ -1388,7 +1402,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             }
             case Datatype(_) => {
               if IsRcWrapped(resolved.attributes) {
-                s := R.Rc(s);
+                s := rc(s);
               }
             }
             case Trait(GeneralTrait()) => {
@@ -1398,7 +1412,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             }
             case Trait(ObjectTrait()) => {
               if resolved.path == [Ident.Ident(Name("_System")), Ident.Ident(Name("object"))] {
-                s := R.AnyTrait;
+                s := AnyTrait;
               }
               if !genTypeContext.forTraitParents {
                 s := Object(R.DynType(s));
@@ -1424,7 +1438,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           }
         }
         case Object() => {
-          s := R.AnyTrait;
+          s := AnyTrait;
           if !genTypeContext.forTraitParents {
             s := Object(R.DynType(s));
           }
@@ -1491,8 +1505,12 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           }
 
           var resultType := GenType(result, GenTypeContext.default());
+          var fnType := R.DynType(R.FnType(argTypes, resultType));
+          if syncType.Sync? {
+            fnType := R.IntersectionType(fnType, SyncSendType);
+          }
           s :=
-            R.Rc(R.DynType(R.FnType(argTypes, resultType)));
+            rc(fnType);
         }
         case TypeArg(Ident(name)) => s := R.TIdentifier(escapeName(name));
         case Primitive(p) => {
@@ -1608,7 +1626,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             } else { // For Rc-defined datatypes
               if enclosingType.UserDefined? && enclosingType.resolved.kind.Datatype?
                  && IsRcWrapped(enclosingType.resolved.attributes) {
-                tpe := R.Borrowed(R.Rc(R.SelfOwned));
+                tpe := R.Borrowed(rc(R.SelfOwned));
               } else if enclosingType.UserDefined? && enclosingType.resolved.kind.Newtype?
                         && IsNewtypeCopy(enclosingType.resolved.kind.range) {
                 tpe := R.TMetaData(
@@ -2736,7 +2754,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
       assert !IsNewtype(fromTpe);
       match (fromTpe, toTpe) {
         case (Primitive(Int), Primitive(Real)) => {
-          r := R.RcNew(R.dafny_runtime.MSel("BigRational").AsExpr().FSel("from_integer").Apply1(r));
+          r := rcNew(R.dafny_runtime.MSel("BigRational").AsExpr().FSel("from_integer").Apply1(r));
           r, resultingOwnership := FromOwned(r, expectedOwnership);
         }
         case (Primitive(Real), Primitive(Int)) => {
@@ -3328,7 +3346,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           }
           r := R.StructBuild(r, assignments);
           if IsRcWrapped(datatypeType.attributes) {
-            r := R.RcNew(r);
+            r := rcNew(r);
           }
           r, resultingOwnership := FromOwned(r, expectedOwnership);
           return;
@@ -3578,7 +3596,6 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         case SelectFn(on, field, isDatatype, isStatic, isConstant, arguments) => {
           // Transforms a function member into a lambda
           var onExpr, onOwned, recIdents := GenExpr(on, selfIdent, env, OwnershipBorrowed);
-          var onString := onExpr.ToString(IND);
 
           var lEnv := env;
           var args := [];
@@ -3591,11 +3608,17 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             parameters := parameters + [R.Formal(name, bTy)];
             args := args + [(name, ty)];
           }
-          var body :=
-            if isStatic then
-              onExpr.FSel(escapeVar(field))
-            else
-              R.Identifier("callTarget").Sel(escapeVar(field));
+          var body;
+          if isStatic {
+            body := onExpr.FSel(escapeVar(field));
+          } else {
+            body := R.Identifier("callTarget");
+            if !isDatatype {
+              body := read_macro.Apply1(body);
+            }
+            body := body.Sel(escapeVar(field));
+          }
+
           if isConstant {
             body := body.Apply0();
           }
@@ -3628,10 +3651,13 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           }
 
           var typeShape := R.DynType(R.FnType(typeShapeArgs, R.TIdentifier("_")));
+          if syncType.Sync? {
+            typeShape := R.IntersectionType(typeShape, SyncSendType);
+          }
 
           r := R.TypeAscription(
-            R.std_rc_Rc_new.Apply1(r),
-            R.std_rc_Rc.AsType().Apply([typeShape]));
+            rcNew(r),
+            rc(typeShape));
           r, resultingOwnership := FromOwned(r, expectedOwnership);
           readIdents := recIdents;
           return;
@@ -3832,7 +3858,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           var retTypeGen := GenType(retType, GenTypeContext.default());
           r := R.Block(
             allReadCloned.Then(
-              R.RcNew(
+              rcNew(
                 R.Lambda(params, Some(retTypeGen), R.Block(recursiveGen))
               )
             ));