Feat: Rust operators (#5390)

UPDATE: The commit
8661eb0
fixed the previous nightly issue that multi-compiler tests on Windows
were taking 15x longer.
UPDATE: That works only for the ResolvedDesugaredExecutableDafny
compiler. Enabling the Dafny-to-Rust compiler again triggers that 15x
slowdown. **Do not merge yet**

### Description
This PR implements most immutable types in Dafny (Sequence, Set,
Multiset, Map) and implements most if not all operators on them. It also
sets an architecture that can now be relied on.
List of features in this PR:
- More comprehensive Rust AST, precedence and associativity to render
parentheses
- The Rust compiler no longer crash when not in /runAllTests, but emits
invalid code. It makes it possible to see which features are missing by
searching for `<i>` in the generated code.
- Made verification of GenExpr less brittle
- Previous PR review comments
- Ability to use shadowed identifiers to avoid numbers in names. Rust
has the same rules as Dafny for shadowing, and I will continue to
monitor cases where semantics might differ.
- `make pr` now prepares a codebase for a (regenerates everything and
reformats everything in the correct order).

### How has this been tested?
I added an integration test for compiling Dafny to Rust, and I added
unit tests for the runtime in Rust
*All tests for each compiler now have a `.rs.check` if they fail.*.

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

.github/workflows/msbuild.yml

@@ -37,7 +37,7 @@ jobs:
  run: dotnet tool restore
  - name: Check whitespace and style
  working-directory: dafny
- run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
+ run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
  - name: Get Boogie Version
  run: |
  sudo apt-get update

.pre-commit-config.yaml

@@ -4,5 +4,5 @@ repos:
  - id: dotnet-format
  name: dotnet-format
  language: system
- entry: dotnet format whitespace Source/Dafny.sln --include
+ entry: dotnet format whitespace Source/Dafny.sln -v:d --include 
  types_or: ["c#"]

Makefile

@@ -7,20 +7,18 @@ all: exe refman
 exe:
  (cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
 
-dfyprodformat:
+format-dfy:
  (cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .)
 
-dfyprodinit: 
+dfy-to-cs: 
  (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
 
-dfyprod: dfyprodformat dfyprodinit
- (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
+dfy-to-cs-exe: dfy-to-cs exe
 
-dfydevinit:
- (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify --no-format)
+dfy-to-cs-noverify:
+ (cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify)
 
-dfydev: dfydevinit
- (cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
+dfy-to-cs-noverify-exe: dfy-to-cs-noverify exe
 
 boogie: ${DIR}/boogie/Binaries/Boogie.exe
 
@@ -73,7 +71,7 @@ z3-ubuntu:
  chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 format:
- dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
+ dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
 
 clean:
  (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
@@ -84,3 +82,11 @@ clean:
  make -C ${DIR}/docs/DafnyRef clean
  (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
  echo Source/*/bin Source/*/obj
+
+# `make pr` will bring you in a state suitable for submitting a PR
+# - Builds the Dafny executable
+# - Use the build to convert core .dfy files to .cs
+# - Rebuilds the Dafny executable with this .cs files
+# - Apply dafny format on all dfy files
+# - Apply dotnet format on all cs files except the generated ones
+pr: exe dfy-to-cs-exe format-dfy format

Source/DafnyCore.Test/GeneratedDafnyTest.cs

@@ -0,0 +1,11 @@
+using System.Collections.Concurrent;
+using Microsoft.Dafny;
+
+namespace DafnyCore.Test;
+
+public class GeneratedDafnyTest {
+ [Fact]
+ public void TestDafnyGeneratedCode() {
+ DafnyToRustCompilerCoverage.RASTCoverage.__default.TestExpr();
+ }
+}

Source/DafnyCore/AST/Expressions/Variables/IVariable.cs

@@ -24,6 +24,10 @@ public interface IVariable : ISymbol {
  string SanitizedName {
  get;
  }
+ string SanitizedNameShadowable { // A name suitable for compilation, but without the unique identifier.
+ // Useful to generate readable identifiers in the generated source code.
+ get;
+ }
  string CompileName {
  get;
  }

Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs

@@ -41,6 +41,13 @@ public abstract class IVariableContracts : TokenNode, IVariable {
  throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
  }
  }
+
+ public string SanitizedNameShadowable {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ throw new NotImplementedException(); // this getter implementation is here only so that the Ensures contract can be given here
+ }
+ }
  public string CompileName {
  get {
  Contract.Ensures(Contract.Result<string>() != null);

Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs

@@ -74,9 +74,14 @@ public abstract class NonglobalVariable : TokenNode, IVariable {
  }
  }
 
+ private string sanitizedNameShadowable;
+
+ public virtual string SanitizedNameShadowable =>
+ sanitizedNameShadowable ??= SanitizeName(Name);
+
  private string sanitizedName;
  public virtual string SanitizedName =>
- sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizeName(Name)}";
+ sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
 
  protected string compileName;
  public virtual string CompileName =>

Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs

@@ -68,9 +68,15 @@ public LocalVariable(RangeToken rangeToken, string name, Type type, bool isGhost
  return uniqueName ??= generator.FreshId(Name + "#");
  }
 
+ private string sanitizedNameShadowable;
+
+ public string SanitizedNameShadowable =>
+ sanitizedNameShadowable ??= NonglobalVariable.SanitizeName(Name);
+
  private string sanitizedName;
+
  public string SanitizedName =>
- sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{NonglobalVariable.SanitizeName(Name)}";
+ sanitizedName ??= $"_{IVariable.CompileNameIdGenerator.FreshNumericId()}_{SanitizedNameShadowable}";
 
  string compileName;
  public string CompileName =>

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -174,7 +174,7 @@ public class NativeType {
  public readonly BigInteger LowerBound;
  public readonly BigInteger UpperBound;
  public readonly int Bitwidth; // for unassigned types, this shows the number of bits in the type; else is 0
- public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long }
+ public enum Selection { Byte, SByte, UShort, Short, UInt, Int, Number, ULong, Long, UDoubleLong, DoubleLong }
  public readonly Selection Sel;
  public NativeType(string Name, BigInteger LowerBound, BigInteger UpperBound, int bitwidth, Selection sel) {
  Contract.Requires(Name != null);

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -3422,15 +3422,16 @@ protected class ClassWriter : IClassWriter {
  return termLeftWriter;
  }
 
- protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) {
+ protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName,
+ ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) {
  if (ct is SetType) {
  var typeName = TypeName(ct.Arg, wr, tok);
- return string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})");
+ wr.Write(string.Format($"{DafnySetClass}<{typeName}>.FromCollection({collName})"));
  } else if (ct is MapType) {
  var mt = (MapType)ct;
  var domtypeName = TypeName(mt.Domain, wr, tok);
  var rantypeName = TypeName(mt.Range, wr, tok);
- return $"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})";
+ wr.Write($"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})");
  } else {
  Contract.Assume(false); // unexpected collection type
  throw new cce.UnreachableException(); // please compiler

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

@@ -2455,9 +2455,10 @@ protected class ClassWriter : IClassWriter {
  throw new UnsupportedFeatureException(tok, Feature.MapComprehensions);
  }
 
- protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) {
+ protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName,
+ ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmt) {
  // collections are built in place
- return collName;
+ wr.Write(collName);
  }
 
  protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBody, string type,

Source/DafnyCore/Backends/Dafny/AST.dfy

@@ -1,3 +1,22 @@
+module {:extern "DAST.Format"} DAST.Format
+ /* Cues about how to format different AST elements if necessary,
+ e.g. to generate idiomatic code when needed. */
+{
+ // Dafny AST compilation tenets:
+ // - The Compiled Dafny AST should be minimal
+ // - The generated code should look idiomatic and close to the original Dafny file if possible
+ // Since the two might conflict, the second one is taken care of by adding formatting information
+
+ datatype UnaryOpFormat =
+ | NoFormat
+ | CombineFormat
+ datatype BinaryOpFormat =
+ | NoFormat
+ | ImpliesFormat
+ | EquivalenceFormat
+ | ReverseFormat
+}
+
 module {:extern "DAST"} DAST {
  import opened Std.Wrappers
 
@@ -19,13 +38,22 @@ module {:extern "DAST"} DAST {
  Set(element: Type) |
  Multiset(element: Type) |
  Map(key: Type, value: Type) |
+ SetBuilder(element: Type) |
+ MapBuilder(key: Type, value: Type) |
  Arrow(args: seq<Type>, result: Type) |
  Primitive(Primitive) | Passthrough(string) |
  TypeArg(Ident)
 
  datatype Primitive = Int | Real | String | Bool | Char
 
- datatype ResolvedType = Datatype(path: seq<Ident>) | Trait(path: seq<Ident>) | Newtype(Type)
+ datatype NewtypeRange =
+ | U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | BigInt
+ | NoRange
+
+ datatype ResolvedType =
+ | Datatype(path: seq<Ident>)
+ | Trait(path: seq<Ident>)
+ | Newtype(baseType: Type, range: NewtypeRange, erase: bool)
 
  datatype Ident = Ident(id: string)
 
@@ -37,7 +65,7 @@ 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: Option<Expression>)
+ datatype Newtype = Newtype(name: string, typeParams: seq<Type>, base: Type, range: NewtypeRange, witnessStmts: seq<Statement>, witnessExpr: Option<Expression>)
 
  datatype ClassItem = Method(Method)
 
@@ -47,14 +75,18 @@ module {:extern "DAST"} DAST {
 
  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 CallName =
+ Name(name: string) |
+ MapBuilderAdd | MapBuilderBuild | SetBuilderAdd | SetBuilderBuild
+
  datatype Statement =
  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: Option<seq<Ident>>) |
+ Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>, outs: Option<seq<Ident>>) |
  Return(expr: Expression) |
  EarlyReturn() |
  Break(toLabel: Option<string>) |
@@ -72,13 +104,21 @@ module {:extern "DAST"} DAST {
 
  datatype BinOp =
  Eq(referential: bool, nullable: bool) |
- Neq(referential: bool, nullable: bool) |
  Div() | EuclidianDiv() |
  Mod() | EuclidianMod() |
- Implies() | // TODO: REplace by Not Or
+ Lt() | // a <= b is !(b < a)
+ LtChar() |
+ Plus() | Minus() | Times() |
+ BitwiseAnd() | BitwiseOr() | BitwiseXor() |
+ BitwiseShiftRight() | BitwiseShiftLeft() |
+ And() | Or() |
  In() |
- NotIn() | // TODO: Replace by Not In
- SetDifference() |
+ SeqProperPrefix() | SeqPrefix() |
+ SetMerge() | SetSubtraction() | SetIntersection() |
+ Subset() | ProperSubset() | SetDisjoint() |
+ MapMerge() | MapSubtraction() |
+ MultisetMerge() | MultisetSubtraction() | MultisetIntersection() |
+ Submultiset() | ProperSubmultiset() | MultisetDisjoint() |
  Concat() |
  Passthrough(string)
 
@@ -94,18 +134,26 @@ module {:extern "DAST"} DAST {
  SeqConstruct(length: Expression, elem: Expression) |
  SeqValue(elements: seq<Expression>, typ: Type) |
  SetValue(elements: seq<Expression>) |
+ MultisetValue(elements: seq<Expression>) |
  MapValue(mapElems: seq<(Expression, Expression)>) |
+ MapBuilder(keyType: Type, valueType: Type) |
+ SeqUpdate(expr: Expression, indexExpr: Expression, value: Expression) |
+ MapUpdate(expr: Expression, indexExpr: Expression, value: Expression) |
+ SetBuilder(elemType: Type) |
+ ToMultiset(Expression) |
  This() |
  Ite(cond: Expression, thn: Expression, els: Expression) |
- UnOp(unOp: UnaryOp, expr: Expression) |
- BinOp(op: BinOp, left: Expression, right: Expression) |
+ UnOp(unOp: UnaryOp, expr: Expression, format1: Format.UnaryOpFormat) |
+ BinOp(op: BinOp, left: Expression, right: Expression, format2: Format.BinaryOpFormat) |
  ArrayLen(expr: Expression, dim: nat) |
+ MapKeys(expr: Expression) |
+ MapValues(expr: Expression) |
  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: Option<Expression>, high: Option<Expression>) |
  TupleSelect(expr: Expression, index: nat) |
- Call(on: Expression, name: Ident, typeArgs: seq<Type>, args: seq<Expression>) |
+ Call(on: Expression, callName: CallName, typeArgs: seq<Type>, args: seq<Expression>) |
  Lambda(params: seq<Formal>, retType: Type, body: seq<Statement>) |
  BetaRedex(values: seq<(Formal, Expression)>, retType: Type, expr: Expression) |
  IIFE(name: Ident, typ: Type, value: Expression, iifeBody: Expression) |