Skip to content

Commit

Permalink
Feat: Ability to emit sync-compatible Rust code. (#6040)
Browse files Browse the repository at this point in the history 
Fixes #5969 
### What was changed?

- I added a new Rust-specific option `--rust-sync`, set to `false` by
default. When turned on, all the generated code uses `std::sync::Arc`
instead of `std::rc::Rc`. Nothing else is normally needed for generated
code.
- The option `--include-runtime=true` now emits the runtime when
translating to Rust.
- I added a new feature for the dafny runtime which is `feature =
"sync"`, enabling or disabling some functions via `#[cfg(feature =
"sync")]` and `#[cfg(not(feature = "sync"))]`. Regular tests don't use
this feature.
- I ran `cargo fmt` on the runtime.

### How has this been tested?
- A test `comp/rust/arc/tokiouser.dfy` uses this option and the runtime
with the sync feature, compiled with `--rust-sync`


<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: Andrew Jewell <[email protected]>
  • Loading branch information
@MikaelMayer @ajewellamz
MikaelMayer and ajewellamz authored Jan 24, 2025
1 parent 76a7caa commit 18c538a
Show file tree
Hide file tree
Showing 21 changed files with 1,506 additions and 1,052 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs
View file

Large diffs are not rendered by default.

11 changes: 7 additions & 4 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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,
Expand All @@ -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)))))]
))
}

Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-path-simplification.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand All @@ -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"))),
Expand Down
21 changes: 6 additions & 15 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-rast.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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")

Expand All @@ -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])
}
Expand Down Expand Up @@ -822,7 +821,7 @@ module RAST
|| (TMetaData? && (copySemantics || display.CanReadWithoutClone()))
}
predicate IsRcOrBorrowedRc() {
(TypeApp? && baseName == RcType) ||
IsRc() ||
(Borrowed? && underlying.IsRcOrBorrowedRc()) ||
(TSynonym? && base.IsRcOrBorrowedRc())
}
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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|);
Expand Down Expand Up @@ -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)
}
Expand Down
72 changes: 49 additions & 23 deletions Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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)))
]
)
)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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 + [
Expand Down Expand Up @@ -1388,7 +1402,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
}
case Datatype(_) => {
if IsRcWrapped(resolved.attributes) {
s := R.Rc(s);
s := rc(s);
}
}
case Trait(GeneralTrait()) => {
Expand All @@ -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));
Expand All @@ -1424,7 +1438,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
}
}
case Object() => {
s := R.AnyTrait;
s := AnyTrait;
if !genTypeContext.forTraitParents {
s := Object(R.DynType(s));
}
Expand Down Expand Up @@ -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) => {
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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)) => {
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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 := [];
Expand All @@ -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();
}
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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))
)
));
Expand Down
Loading

0 comments on commit 18c538a

Please sign in to comment.