Feat: Dafny-to-Rust code indentation and identifiers (#4974)

# Improvements of the DAST to Rust code generator:

* The code generator emits a Rust-like AST that is then formatted with
proper indentation
* Ensured Rust-like identifiers in Dafny stay the same in Rust (like
"one_variable")
* Added Initial implementation of sequences and maps in the
DafnyRuntimeRust, following the implementation of the Go
* Added module to perform conversions from and to Dafny types to and
from native types

# Code enhancement

* Added support for using the standard library's Option type rather than
the hard-coded Optional type.

# Tests

* Added proof that the identifier mapping is fully reversible and won't
conflict with other internal constructs
* Added a Rust test module for the DafnyRuntimeRust and wrote tests for
testing the encoding Dafny/Rust

# Tooling improvement

- The makefile now works even if there is a space in the path
- `make dfydev` does not perform verification and formatting of the
resulting C# file, but `make dfyprod` does it. Both build Dafny
afterwards
' `make dfydevinit` and `make dfyprodinit` only perform the conversion
from dafny files to C# files, without rebuilding Dafny.
 


<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>

Makefile

@@ -1,4 +1,4 @@
-DIR=$(dir $(realpath $(firstword $(MAKEFILE_LIST))))
+DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))
 
 default: exe
 
@@ -7,9 +7,20 @@ all: exe refman
 exe:
  (cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
 
-dfydev:
- (cd ${DIR}/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
- (cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
+dfyprodformat:
+ (cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .)
+
+dfyprodinit: 
+ (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
+
+dfyprod: dfyprodformat dfyprodinit
+ (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
+
+dfydevinit:
+ (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify --no-format)
+
+dfydev: dfydevinit
+ (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
 
 boogie: ${DIR}/boogie/Binaries/Boogie.exe
 
@@ -29,7 +40,7 @@ refman-release: exe
  make -C ${DIR}/docs/DafnyRef release
 
 z3-mac:
- mkdir -p ${DIR}Binaries/z3/bin
+ mkdir -p ${DIR}/Binaries/z3/bin
  wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
  unzip z3-4.12.1-x64-macos-11-bin.zip
  rm z3-4.12.1-x64-macos-11-bin.zip
@@ -40,7 +51,7 @@ z3-mac:
  chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 z3-mac-arm:
- mkdir -p ${DIR}Binaries/z3/bin
+ mkdir -p ${DIR}/Binaries/z3/bin
  wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip
  unzip z3-4.12.1-arm64-macos-11-bin.zip
  rm z3-4.12.1-arm64-macos-11-bin.zip
@@ -51,7 +62,7 @@ z3-mac-arm:
  chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 z3-ubuntu:
- mkdir -p ${DIR}Binaries/z3/bin
+ mkdir -p ${DIR}/Binaries/z3/bin
  wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
  unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
  rm z3-4.12.1-x64-ubuntu-20.04-bin.zip

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -1,7 +1,14 @@
 module {:extern "DAST"} DAST {
+ import opened Std.Wrappers
+
  datatype Module = Module(name: string, isExtern: bool, body: seq<ModuleItem>)
 
- datatype ModuleItem = Module(Module) | Class(Class) | Trait(Trait) | Newtype(Newtype) | Datatype(Datatype)
+ datatype ModuleItem =
+ | Module(Module)
+ | Class(Class)
+ | Trait(Trait)
+ | Newtype(Newtype)
+ | Datatype(Datatype)
 
  datatype Type =
  Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) |
@@ -30,29 +37,27 @@ module {:extern "DAST"} DAST {
 
  datatype DatatypeCtor = DatatypeCtor(name: string, args: seq<Formal>, hasAnyArgs: bool /* includes ghost */)
 
- datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Optional<Expression>)
+ datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)
 
  datatype ClassItem = Method(Method)
 
- datatype Field = Field(formal: Formal, defaultValue: Optional<Expression>)
+ datatype Field = Field(formal: Formal, defaultValue: Option<Expression>)
 
  datatype Formal = Formal(name: string, typ: Type)
 
- datatype Method = Method(isStatic: bool, hasBody: bool, overridingPath: Optional<seq<Ident>>, name: string, typeParams: seq<Type>, params: seq<Formal>, body: seq<Statement>, outTypes: seq<Type>, outVars: Optional<seq<Ident>>)
-
- datatype Optional<T> = Some(T) | None
+ datatype Method = Method(isStatic: bool, hasBody: bool, overridingPath: Option<seq<Ident>>, name: string, typeParams: seq<Type>, params: seq<Formal>, body: seq<Statement>, outTypes: seq<Type>, outVars: Option<seq<Ident>>)
 
  datatype Statement =
- DeclareVar(name: string, typ: Type, maybeValue: Optional<Expression>) |
+ DeclareVar(name: string, typ: Type, maybeValue: Option<Expression>) |
  Assign(lhs: AssignLhs, value: Expression) |
  If(cond: Expression, thn: seq<Statement>, els: seq<Statement>) |
  Labeled(lbl: string, body: seq<Statement>) |
  While(cond: Expression, body: seq<Statement>) |
  Foreach(boundName: string, boundType: Type, over: Expression, body: seq<Statement>) |
- Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Optional<seq<Ident>>) |
+ Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
  Return(expr: Expression) |
  EarlyReturn() |
- Break(toLabel: Optional<string>) |
+ Break(toLabel: Option<string>) |
  TailRecursive(body: seq<Statement>) |
  JumpTailCallStart() |
  Halt() |
@@ -70,9 +75,9 @@ module {:extern "DAST"} DAST {
  Neq(referential: bool, nullable: bool) |
  Div() | EuclidianDiv() |
  Mod() | EuclidianMod() |
- Implies() |
+ Implies() | // TODO: REplace by Not Or
  In() |
- NotIn() |
+ NotIn() | // TODO: Replace by Not In
  SetDifference() |
  Concat() |
  Passthrough(string)
@@ -98,7 +103,7 @@ module {:extern "DAST"} DAST {
  Select(expr: Expression, field: string, isConstant: bool, onDatatype: bool) |
  SelectFn(expr: Expression, field: string, onDatatype: bool, isStatic: bool, arity: nat) |
  Index(expr: Expression, collKind: CollKind, indices: seq<Expression>) |
- IndexRange(expr: Expression, isArray: bool, low: Optional<Expression>, high: Optional<Expression>) |
+ IndexRange(expr: Expression, isArray: bool, low: Option<Expression>, high: Option<Expression>) |
  TupleSelect(expr: Expression, index: nat) |
  Call(on: Expression, name: Ident, typeArgs: seq<Type>, args: seq<Expression>) |
  Lambda(params: seq<Formal>, retType: Type, body: seq<Statement>) |

Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs

@@ -2,7 +2,9 @@
 using System.Collections.Generic;
 using Dafny;
 using DAST;
+using Microsoft.CodeAnalysis;
 using Microsoft.Dafny.Compilers;
+using Std.Wrappers;
 
 namespace Microsoft.Dafny.Compilers {
 
@@ -97,7 +99,7 @@ public void AddMethod(DAST.Method item) {
  body.Add(item);
  }
 
- public void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue) {
+ public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
  fields.Add((DAST.Field)DAST.Field.create_Field(item, defaultValue));
  }
 
@@ -146,7 +148,7 @@ public void AddMethod(DAST.Method item) {
  body.Add(item);
  }
 
- public void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue) {
+ public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
  throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
  }
 
@@ -189,7 +191,7 @@ public void AddMethod(DAST.Method item) {
  throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
  }
 
- public void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue) {
+ public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
  throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
  }
 
@@ -199,7 +201,7 @@ public object Finish() {
  Sequence<DAST.Type>.FromArray(this.typeParams.ToArray()),
  this.baseType,
  Sequence<DAST.Statement>.FromArray(this.witnessStmts.ToArray()),
- this.witness == null ? Optional<DAST._IExpression>.create_None() : Optional<DAST._IExpression>.create_Some(this.witness)
+ this.witness == null ? Option<DAST._IExpression>.create_None() : Option<DAST._IExpression>.create_Some(this.witness)
  ));
  return parent;
  }
@@ -235,7 +237,7 @@ public void AddMethod(DAST.Method item) {
  body.Add(item);
  }
 
- public void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue) {
+ public void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue) {
  throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
  }
 
@@ -255,7 +257,7 @@ public object Finish() {
  interface ClassLike {
  void AddMethod(DAST.Method item);
 
- void AddField(DAST.Formal item, _IOptional<DAST._IExpression> defaultValue);
+ void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue);
 
  public MethodBuilder Method(
  bool isStatic, bool hasBody,
@@ -324,13 +326,13 @@ public DAST.Method Build() {
  return (DAST.Method)DAST.Method.create(
  isStatic,
  hasBody,
- overridingPath != null ? Optional<ISequence<ISequence<Rune>>>.create_Some(overridingPath) : Optional<ISequence<ISequence<Rune>>>.create_None(),
+ overridingPath != null ? Option<ISequence<ISequence<Rune>>>.create_Some(overridingPath) : Option<ISequence<ISequence<Rune>>>.create_None(),
  Sequence<Rune>.UnicodeFromString(this.name),
  Sequence<DAST.Type>.FromArray(typeArgs.ToArray()),
  Sequence<DAST.Formal>.FromArray(params_.ToArray()),
  Sequence<DAST.Statement>.FromArray(builtStatements.ToArray()),
  Sequence<DAST.Type>.FromArray(outTypes.ToArray()),
- outVars != null ? Optional<ISequence<ISequence<Rune>>>.create_Some(Sequence<ISequence<Rune>>.FromArray(outVars.ToArray())) : Optional<ISequence<ISequence<Rune>>>.create_None()
+ outVars != null ? Option<ISequence<ISequence<Rune>>>.create_Some(Sequence<ISequence<Rune>>.FromArray(outVars.ToArray())) : Option<ISequence<ISequence<Rune>>>.create_None()
  );
  }
  }
@@ -473,11 +475,11 @@ public void AddBuildable(BuildableExpr value) {
 
  public DAST.Statement Build() {
  if (this.value == null) {
- return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, DAST.Optional<DAST._IExpression>.create_None());
+ return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, Option<DAST._IExpression>.create_None());
  } else {
  var builtValue = new List<DAST.Expression>();
  ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
- return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, DAST.Optional<DAST._IExpression>.create_Some(builtValue[0]));
+ return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence<Rune>.UnicodeFromString(name), type, Option<DAST._IExpression>.create_Some(builtValue[0]));
  }
  }
  }
@@ -820,7 +822,7 @@ public DAST.Statement Build() {
  Sequence<Rune>.UnicodeFromString(name),
  Sequence<DAST.Type>.FromArray(typeArgs.ToArray()),
  Sequence<DAST.Expression>.FromArray(builtArgs.ToArray()),
- outs == null ? DAST.Optional<ISequence<ISequence<Rune>>>.create_None() : DAST.Optional<ISequence<ISequence<Rune>>>.create_Some(Sequence<ISequence<Rune>>.FromArray(outs.ToArray()))
+ outs == null ? Option<ISequence<ISequence<Rune>>>.create_None() : Option<ISequence<ISequence<Rune>>>.create_Some(Sequence<ISequence<Rune>>.FromArray(outs.ToArray()))
  );
  }
  }

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -7,6 +7,7 @@
 using Microsoft.BaseTypes;
 using System.Linq;
 using System.Diagnostics.Contracts;
+using Std.Wrappers;
 
 namespace Microsoft.Dafny.Compilers {
 
@@ -519,7 +520,7 @@ public ConcreteSyntaxTree CreateGetterSetter(string name, Type resultType, IToke
 
  public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, bool isConst, Type type,
  IToken tok, string rhs, Field field) {
- _IOptional<DAST._IExpression> rhsExpr = null;
+ _IOption<DAST._IExpression> rhsExpr = null;
  if (rhs != null) {
  rhsExpr = compiler.bufferedInitializationValue;
  compiler.bufferedInitializationValue = null;
@@ -528,7 +529,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic,
  throw new InvalidOperationException();
  }
  } else {
- rhsExpr = Optional<DAST._IExpression>.create_None();
+ rhsExpr = Option<DAST._IExpression>.create_None();
  }
 
  builder.AddField((DAST.Formal)DAST.Formal.create_Formal(
@@ -571,7 +572,7 @@ protected override void EmitReturnExpr(string returnExpr, ConcreteSyntaxTree wr)
 
  if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
  var returnBuilder = stmtContainer.Builder.Return();
- returnBuilder.AddExpr((DAST.Expression)rhsValue.dtor_Some_a0);
+ returnBuilder.AddExpr((DAST.Expression)rhsValue.dtor_value);
  } else {
  throw new InvalidOperationException();
  }
@@ -615,7 +616,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok,
 
  // sometimes, the compiler generates the initial value before the declaration,
  // so we buffer it here
- _IOptional<DAST._IExpression> bufferedInitializationValue = null;
+ _IOption<DAST._IExpression> bufferedInitializationValue = null;
 
  protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok,
  bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
@@ -624,38 +625,38 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
  } else {
  type = type.NormalizeExpandKeepConstraints();
  if (usePlaceboValue) {
- bufferedInitializationValue = Optional<DAST._IExpression>.create_None();
+ bufferedInitializationValue = Option<DAST._IExpression>.create_None();
  } else {
  if (type.AsNewtype != null && type.AsNewtype.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
  var buf = new ExprBuffer(null);
  EmitExpr(type.AsNewtype.Witness, false, new BuilderSyntaxTree<ExprContainer>(buf), null);
- bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(buf.Finish());
+ bufferedInitializationValue = Option<DAST._IExpression>.create_Some(buf.Finish());
  } else if (type.AsSubsetType != null && type.AsSubsetType.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
  var buf = new ExprBuffer(null);
  EmitExpr(type.AsSubsetType.Witness, false, new BuilderSyntaxTree<ExprContainer>(buf), null);
- bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(buf.Finish());
+ bufferedInitializationValue = Option<DAST._IExpression>.create_Some(buf.Finish());
  } else if (type.AsDatatype != null && type.AsDatatype.Ctors.Count == 1 && type.AsDatatype.Ctors[0].EnclosingDatatype is TupleTypeDecl tupleDecl) {
  var elems = new List<DAST._IExpression>();
  for (var i = 0; i < tupleDecl.Ctors[0].Formals.Count; i++) {
  if (!tupleDecl.Ctors[0].Formals[i].IsGhost) {
  TypeInitializationValue(type.TypeArgs[i], wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
- elems.Add(bufferedInitializationValue.dtor_Some_a0);
+ elems.Add(bufferedInitializationValue.dtor_value);
  bufferedInitializationValue = null;
  }
  }
 
  if (elems.Count == 1) {
- bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(elems[0]);
+ bufferedInitializationValue = Option<DAST._IExpression>.create_Some(elems[0]);
  } else {
- bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(
+ bufferedInitializationValue = Option<DAST._IExpression>.create_Some(
  DAST.Expression.create_Tuple(Sequence<DAST._IExpression>.FromArray(elems.ToArray()))
  );
  }
  } else if (type.IsArrowType) {
  throwGeneralUnsupported();
  throw new InvalidOperationException();
  } else {
- bufferedInitializationValue = Optional<DAST._IExpression>.create_Some(
+ bufferedInitializationValue = Option<DAST._IExpression>.create_Some(
  DAST.Expression.create_InitializationValue(GenType(type))
  );
  }
@@ -958,7 +959,7 @@ protected override ConcreteSyntaxTree CreateLabeledCode(string label, bool creat
  protected override void EmitBreak(string label, ConcreteSyntaxTree wr) {
  if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
  stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_Break(
- label == null ? Optional<ISequence<Rune>>.create_None() : Optional<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString("goto_" + label))
+ label == null ? Option<ISequence<Rune>>.create_None() : Option<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString("goto_" + label))
  ));
  } else {
  throw new InvalidOperationException();
@@ -968,7 +969,7 @@ protected override void EmitBreak(string label, ConcreteSyntaxTree wr) {
  protected override void EmitContinue(string label, ConcreteSyntaxTree wr) {
  if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
  stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_Break(
- Optional<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString("continue_" + label))
+ Option<ISequence<Rune>>.create_Some(Sequence<Rune>.UnicodeFromString("continue_" + label))
  ));
  } else {
  throw new InvalidOperationException();
@@ -1781,8 +1782,8 @@ protected override void EmitSeqSelectRange(Expression source, Expression lo, Exp
  builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_IndexRange(
  sourceExpr,
  fromArray,
- loExpr != null ? Optional<DAST._IExpression>.create_Some(loExpr) : Optional<DAST._IExpression>.create_None(),
- hiExpr != null ? Optional<DAST._IExpression>.create_Some(hiExpr) : Optional<DAST._IExpression>.create_None()
+ loExpr != null ? Option<DAST._IExpression>.create_Some(loExpr) : Option<DAST._IExpression>.create_None(),
+ hiExpr != null ? Option<DAST._IExpression>.create_Some(hiExpr) : Option<DAST._IExpression>.create_None()
  ));
  } else {
  throw new InvalidOperationException();