Merge branch 'master' into assignByFormatting

.gitignore

@@ -90,3 +90,4 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.csproj
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/PythonModule1
 /Source/DafnyCore/Prelude/DafnyPrelude.bpl
 /Source/DafnyCore/Prelude/Sequences.bpl
+/venv

Source/DafnyCore.Test/GeneratedDafnyTest.cs

@@ -6,7 +6,12 @@ namespace DafnyCore.Test;
 public class GeneratedDafnyTest {
   [Fact]
   public void TestDafnyCoverage() {
-    DafnyToRustCompilerCoverage.RASTCoverage.__default.TestExpr();
+    DafnyToRustCompilerCoverage.__default.TestIsCopy(); ;
+  }
+
+  [Fact]
+  public void TestRustASTCoverage() {
+    RASTCoverage.__default.TestExpr();
   }
 
   [Fact]

Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs

@@ -0,0 +1,32 @@
+// Dafny program the_program compiled into C#
+// To recompile, you will need the libraries
+//     System.Runtime.Numerics.dll System.Collections.Immutable.dll
+// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// Optionally, you may want to include compiler switches like
+//     /debug /nowarn:162,164,168,183,219,436,1717,1718
+
+using System;
+using System.Numerics;
+using System.Collections;
+#pragma warning disable CS0164 // This label has not been referenced
+#pragma warning disable CS0162 // Unreachable code detected
+#pragma warning disable CS1717 // Assignment made to same variable
+
+namespace DafnyToRustCompilerCoverage {
+
+  public partial class __default {
+    public static void TestIsCopy()
+    {
+      if (!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_Bool()))) {
+        throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(9,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+      if (!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_U128(true)))) {
+        throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(10,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+      if (!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_U128(false)))) {
+        throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(11,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+      if (!(!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_BigInt())))) {
+        throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(12,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+      if (!(!(Defs.__default.IsNewtypeCopy(DAST.NewtypeRange.create_NoRange())))) {
+        throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-coverage.dfy(13,4): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+    }
+  }
+} // end of namespace DafnyToRustCompilerCoverage

Source/DafnyCore/Backends/Dafny/AST.dfy

@@ -115,6 +115,15 @@ module {:extern "DAST"} DAST {
           this
       }
     }
+
+    predicate IsPrimitiveInt() {
+      match this {
+        case Primitive(Int) => true
+        case UserDefined(ResolvedType(_, _, SynonymType(typ), _, _, _)) =>
+          typ.IsPrimitiveInt()
+        case _ => false
+      }
+    }
   }
 
   datatype Variance =
@@ -130,10 +139,30 @@ module {:extern "DAST"} DAST {
 
   datatype Primitive = Int | Real | String | Bool | Char | Native
 
-  // USIZE is for whatever target considers that native arrays can be indexed with
+
   datatype NewtypeRange =
-    | U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | USIZE | BigInt
+    | U8(overflow: bool) // Whether arithmetic operations can overflow and wrap
+    | I8(overflow: bool)
+    | U16(overflow: bool)
+    | I16(overflow: bool)
+    | U32(overflow: bool)
+    | I32(overflow: bool)
+    | U64(overflow: bool)
+    | I64(overflow: bool)
+    | U128(overflow: bool)
+    | I128(overflow: bool)
+    | NativeArrayIndex
+    | BigInt
+    | Bool
     | NoRange
+  {
+    predicate CanOverflow() {
+      (U8? || I8? || U16? || I16? || U32? || I32? || U64? || I64? || U128? || I128?) && overflow
+    }
+    predicate HasArithmeticOperations() {
+      !Bool?// To change when newtypes will have sequences and sets as ranges.
+    }
+  }
 
   datatype Attribute = Attribute(name: string, args: seq<string>)
 
@@ -147,6 +176,7 @@ module {:extern "DAST"} DAST {
     | Class()
     | Datatype(variances: seq<Variance>)
     | Trait()
+    | SynonymType(baseType: Type)
     | Newtype(baseType: Type, range: NewtypeRange, erase: bool)
 
   datatype ResolvedType = ResolvedType(
@@ -190,7 +220,8 @@ module {:extern "DAST"} DAST {
     Newtype(
       name: Name, typeParams: seq<TypeArgDecl>, base: Type,
       range: NewtypeRange, constraint: Option<NewtypeConstraint>,
-      witnessStmts: seq<Statement>, witnessExpr: Option<Expression>, attributes: seq<Attribute>)
+      witnessStmts: seq<Statement>, witnessExpr: Option<Expression>, attributes: seq<Attribute>,
+      classItems: seq<ClassItem>)
 
   datatype NewtypeConstraint = NewtypeConstraint(variable: Formal, constraintStmts: seq<Statement>)
 
@@ -200,7 +231,7 @@ module {:extern "DAST"} DAST {
 
   datatype ClassItem = Method(Method)
 
-  datatype Field = Field(formal: Formal, isConstant: bool, defaultValue: Option<Expression>)
+  datatype Field = Field(formal: Formal, isConstant: bool, defaultValue: Option<Expression>, isStatic: bool)
 
   datatype Formal = Formal(name: VarName, typ: Type, attributes: seq<Attribute>)
 
@@ -250,13 +281,16 @@ module {:extern "DAST"} DAST {
 
   datatype CollKind = Seq | Array | Map
 
+  datatype TypedBinOp =
+    TypedBinOp(op: BinOp, leftType: Type, rightType: Type, resultType: Type)
+
   datatype BinOp =
     Eq(referential: bool) |
-    Div() | EuclidianDiv() |
+    Div(overflow: bool) | EuclidianDiv() |
     Mod() | EuclidianMod() |
     Lt() | // a <= b is !(b < a)
     LtChar() |
-    Plus() | Minus() | Times() |
+    Plus(overflow: bool) | Minus(overflow: bool) | Times(overflow: bool) |
     BitwiseAnd() | BitwiseOr() | BitwiseXor() |
     BitwiseShiftRight() | BitwiseShiftLeft() |
     And() | Or() |
@@ -295,7 +329,7 @@ module {:extern "DAST"} DAST {
     This() |
     Ite(cond: Expression, thn: Expression, els: Expression) |
     UnOp(unOp: UnaryOp, expr: Expression, format1: Format.UnaryOpFormat) |
-    BinOp(op: BinOp, left: Expression, right: Expression, format2: Format.BinaryOpFormat) |
+    BinOp(op: TypedBinOp, left: Expression, right: Expression, format2: Format.BinaryOpFormat) |
     ArrayLen(expr: Expression, exprType: Type, dim: nat, native: bool) |
     MapKeys(expr: Expression) |
     MapValues(expr: Expression) |
@@ -326,12 +360,15 @@ module {:extern "DAST"} DAST {
   // Since constant fields need to be set up in the constructor,
   // accessing constant fields is done in two ways:
   // - The internal field access (through the internal field that contains the value of the constant)
-  //   it's not initialized at the beginning of the constructor
+  //   it's not initialized at the beginning of the constructor.
   // - The external field access (through a function), which when accessed
-  //   must always be initialized
+  //   must always be initialized.
   // For Select expressions, it's important to know how the field is being accessed
   // For mutable fields, there is no wrapping function so only one way to access the mutable field
-  datatype FieldMutability = ConstantField | InternalClassConstantField  | ClassMutableField
+  datatype FieldMutability =
+    | ConstantField // Access a class constant field after initialization, or a datatype constant field
+    | InternalClassConstantFieldOrDatatypeDestructor // Access a class internal field before initialization, or a datatype destructor
+    | ClassMutableField
   datatype UnaryOp = Not | BitwiseNot | Cardinality
 
   datatype Literal =

Source/DafnyCore/Backends/Dafny/ASTBuilder.cs

@@ -39,9 +39,14 @@ public ModuleBuilder Module(string name, Sequence<Attribute> attributes, bool re
       return new ModuleBuilder(this, name, attributes, requiresExterns);
     }
 
-    static public Module UnsupportedToModule(string why) {
-      return new Module(Sequence<Rune>.UnicodeFromString(why), Sequence<Attribute>.FromElements((Attribute)Attribute.create_Attribute(
-          Sequence<Rune>.UnicodeFromString(why), Sequence<Sequence<Rune>>.Empty)), false,
+    public static Module UnsupportedToModule(string why) {
+      return new Module(
+        Sequence<Rune>.UnicodeFromString(why.Replace(".", ",")),
+        Sequence<Attribute>.FromElements(
+          (Attribute)Attribute.create_Attribute(
+            Sequence<Rune>.UnicodeFromString("extern"),
+          Sequence<Sequence<Rune>>.FromElements(
+            (Sequence<Rune>)Sequence<Rune>.UnicodeFromString(why)))), false,
         Std.Wrappers.Option<Sequence<ModuleItem>>.create_None());
     }
   }
@@ -133,8 +138,8 @@ public void AddMethod(DAST.Method item) {
       body.Add(item);
     }
 
-    public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      fields.Add((DAST.Field)DAST.Field.create_Field(item, isConstant, defaultValue));
+    public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue, bool isStatic) {
+      fields.Add((DAST.Field)DAST.Field.create_Field(item, isConstant, defaultValue, isStatic));
     }
 
     public object Finish() {
@@ -187,8 +192,8 @@ public void AddMethod(DAST.Method item) {
       body.Add(item);
     }
 
-    public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+    public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue, bool isStatic) {
+      this.parent.AddUnsupported("Field " + item.ToString());
     }
 
     public object Finish() {
@@ -223,6 +228,7 @@ class NewtypeBuilder : ClassLike {
     readonly List<DAST.Statement> witnessStmts;
     readonly DAST.Expression witness;
     private ISequence<_IAttribute> attributes;
+    private readonly List<DAST._IMethod> methods;
 
     public NewtypeBuilder(NewtypeContainer parent, string name, List<TypeArgDecl> typeParams,
       NewtypeRange newtypeRange, DAST.Type baseType, Option<DAST.NewtypeConstraint> constraint, List<DAST.Statement> statements,
@@ -237,14 +243,15 @@ public NewtypeBuilder(NewtypeContainer parent, string name, List<TypeArgDecl> ty
       this.witnessStmts = statements;
       this.witness = witness;
       this.attributes = attributes;
+      this.methods = new();
     }
 
     public void AddMethod(DAST.Method item) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      methods.Add(item);
     }
 
-    public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+    public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue, bool isStatic) {
+      parent.AddUnsupported("Datatype field " + item.ToString());
     }
 
     public object Finish() {
@@ -258,7 +265,8 @@ public object Finish() {
         this.witness == null
           ? Option<DAST._IExpression>.create_None()
           : Option<DAST._IExpression>.create_Some(this.witness),
-        attributes
+        attributes,
+        Sequence<DAST._IMethod>.FromArray(methods.ToArray())
       ));
       return parent;
     }
@@ -343,8 +351,8 @@ public void AddMethod(DAST.Method item) {
       body.Add(item);
     }
 
-    public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+    public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue, bool isStatic) {
+      parent.AddUnsupported("Datatype field " + item.ToString());
     }
 
     public object Finish() {
@@ -363,7 +371,7 @@ public object Finish() {
   interface ClassLike {
     void AddMethod(DAST.Method item);
 
-    void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue);
+    void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue, bool isStatic);
 
     public MethodBuilder Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction,
       ISequence<ISequence<Rune>> overridingPath,
@@ -676,6 +684,8 @@ class IfElseBuilder : ExprContainer, StatementContainer, BuildableStatement {
     readonly List<object> ifBody = new();
     readonly List<object> elseBody = new();
 
+    public object Condition => condition;
+
     public IfElseBuilder() { }
 
     public void AddExpr(DAST.Expression value) {
@@ -777,6 +787,7 @@ public void AddUnsupported(string why) {
   class WhileBuilder : ExprContainer, StatementContainer, BuildableStatement {
     object condition = null;
     readonly List<object> body = new();
+    public object Condition => condition;
 
     public void AddExpr(DAST.Expression value) {
       if (condition != null) {
@@ -1233,8 +1244,8 @@ ExprWrapper Wrapper(Func<DAST.Expression, DAST.Expression> wrapper) {
       return ret;
     }
 
-    BinOpBuilder BinOp(DAST.BinOp op) {
-      var ret = new BinOpBuilder(op);
+    BinOpBuilder BinOp(DAST.BinOp op, DAST.Type leftType, DAST.Type rightType, DAST.Type resType) {
+      var ret = new BinOpBuilder(op, leftType, rightType, resType);
       AddBuildable(ret);
       return ret;
     }
@@ -1385,9 +1396,10 @@ class BinOpBuilder : ExprContainer, BuildableExpr {
     readonly List<object> operands = new();
     private readonly string op;
 
-    public BinOpBuilder(DAST.BinOp op) {
+    public BinOpBuilder(DAST.BinOp op, DAST.Type leftType, DAST.Type rightType, DAST.Type resType) {
       this.internalBuilder = (DAST.Expression left, DAST.Expression right) =>
-        (DAST.Expression)DAST.Expression.create_BinOp(op, left, right, new BinaryOpFormat_NoFormat());
+        (DAST.Expression)DAST.Expression.create_BinOp(
+          DAST.TypedBinOp.create_TypedBinOp(op, leftType, rightType, resType), left, right, new BinaryOpFormat_NoFormat());
       this.op = op.ToString();
     }
 
@@ -1816,7 +1828,7 @@ public static DAST.Expression ToNativeUsize(int number) {
         DAST.ResolvedType.create_ResolvedType(
         Sequence<Sequence<Rune>>.FromElements((Sequence<Rune>)Sequence<Rune>.UnicodeFromString("usize")),
         Sequence<_IType>.Empty,
-        DAST.ResolvedTypeBase.create_Newtype(origType, DAST.NewtypeRange.create_USIZE(), true), Sequence<_IAttribute>.Empty,
+        DAST.ResolvedTypeBase.create_Newtype(origType, DAST.NewtypeRange.create_NativeArrayIndex(), true), Sequence<_IAttribute>.Empty,
         Sequence<Sequence<Rune>>.Empty, Sequence<_IType>.Empty)
       ));
     }