Merge branch 'release-4.9.0' of https://github.com/dafny-lang/dafny i…

…nto release-4.9.0

RELEASE_NOTES.md

@@ -2,6 +2,28 @@
 
 See [docs/dev/news/](docs/dev/news/).
 
+# 4.9.0
+
+## New features
+
+- Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details. (https://github.com/dafny-lang/dafny/pull/5761)
+
+- By blocks ("... by { ... }") are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously `assert 3 / x == 1 by { assume x == 3; }` could still give a possible division by zero error, but now it won't. (https://github.com/dafny-lang/dafny/pull/5779)
+
+- Use --suggest-proof-refactoring to be alerted of function definitions, which have no contribution to a method's proof, and facts, which are only used once in a proof. (https://github.com/dafny-lang/dafny/pull/5812)
+
+- Support for [top-level @-attributes](https://dafny.org/latest/DafnyRef/DafnyRef#sec-at-attributes) (https://github.com/dafny-lang/dafny/pull/5825)
+
+## Bug fixes
+
+- Enable abstract imports to work well with match expression that occur in specifications (https://github.com/dafny-lang/dafny/pull/5808)
+
+- Fix a bug that prevented using reveal statement expressions in the body of a constant. (https://github.com/dafny-lang/dafny/pull/5823)
+
+- Improve performance of `dafny verify` for large applications, by removing memory leaks (https://github.com/dafny-lang/dafny/pull/5827)
+
+- Green gutter icons cover constants without RHS (https://github.com/dafny-lang/dafny/pull/5841)
+
 # 4.8.1
 
 ## New features

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -185,15 +185,10 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
     //   }
     // They aren't in any namespace to make them universally accessible.
     private void EmitFuncExtensions(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) {
-      // An extension for this arity will be provided in the Runtime which has to be linked.
-      var omitAritiesBefore16 = !Options.IncludeRuntime && Options.SystemModuleTranslationMode is not CommonOptionBag.SystemModuleMode.OmitAllOtherModules;
-      var name = omitAritiesBefore16 ? "FuncExtensionsAfterArity16" : "FuncExtensions";
-      var funcExtensions = wr.NewNamedBlock("public static class " + name);
+      var funcExtensions = wr.NewNamedBlock("internal static class FuncExtensions");
+      wr.WriteLine("// end of class FuncExtensions");
       foreach (var kv in systemModuleManager.ArrowTypeDecls) {
         int arity = kv.Key;
-        if (omitAritiesBefore16 && arity <= 16) {
-          continue;
-        }
 
         List<string> TypeParameterList(string prefix) {
           var l = arity switch {

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

@@ -3744,8 +3744,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         } else {
           error := Some("Unrecognized external file " + externalFile + ". External file must be *.rs files");
         }
-        var externMod := R.ExternMod(externalMod);
-        s := s + externMod.ToString("") + "\n";
+        if rootType.RootCrate? {
+          var externMod := R.ExternMod(externalMod);
+          s := s + externMod.ToString("") + "\n";
+        }
         externUseDecls := externUseDecls + [
           R.UseDecl(R.Use(R.PUB, R.crate.MSel(externalMod).MSel("*")))
         ];

Source/DafnyCore/DafnyGeneratedFromDafnyPost.py

@@ -67,6 +67,18 @@
 
     print(f"File generated: {file_path}")
 
+  # Special-case the FuncExtensions class, which isn't declared inside a namespace
+  func_extensions_pattern = re.compile(r'(internal\s+static\s+class\s+FuncExtensions\s*{[\s\S]*?}\s*//\s*end\s*of\s*class\s*FuncExtensions)')
+  match = func_extensions_pattern.search(content)
+  func_extensions_content = match[0]
+
+  file_content = f"{prelude}\n\n{func_extensions_content}"
+  file_path = f"{output}/FuncExtensions.cs"
+  with open(file_path, 'w') as file:
+    file.write(file_content)
+
+  print(f"File generated: {file_path}")
+
 # Now delete the file output.cs
 os.remove(output + '.cs')
 print("File deleted: " + output + '.cs')

Source/DafnyCore/GeneratedFromDafny/DCOMP.cs

@@ -6679,9 +6679,11 @@ public RAST._IExpr Error(Dafny.ISequence<Dafny.Rune> message, RAST._IExpr defaul
         } else {
           (this).error = Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Unrecognized external file "), _2_externalFile), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(". External file must be *.rs files")));
         }
-        RAST._IMod _4_externMod;
-        _4_externMod = RAST.Mod.create_ExternMod(_3_externalMod);
-        s = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(s, (_4_externMod)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
+        if (((this).rootType).is_RootCrate) {
+          RAST._IMod _4_externMod;
+          _4_externMod = RAST.Mod.create_ExternMod(_3_externalMod);
+          s = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(s, (_4_externMod)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
+        }
         _0_externUseDecls = Dafny.Sequence<RAST._IModDecl>.Concat(_0_externUseDecls, Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), ((RAST.__default.crate).MSel(_3_externalMod)).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("*"))))));
       }
       if (!(_0_externUseDecls).Equals(Dafny.Sequence<RAST._IModDecl>.FromElements())) {

Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs

@@ -0,0 +1,38 @@
+// 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
+
+internal static class FuncExtensions {
+  public static Func<U, UResult> DowncastClone<T, TResult, U, UResult>(this Func<T, TResult> F, Func<U, T> ArgConv, Func<TResult, UResult> ResConv) {
+    return arg => ResConv(F(ArgConv(arg)));
+  }
+  public static Func<UResult> DowncastClone<TResult, UResult>(this Func<TResult> F, Func<TResult, UResult> ResConv) {
+    return () => ResConv(F());
+  }
+  public static Func<U1, U2, UResult> DowncastClone<T1, T2, TResult, U1, U2, UResult>(this Func<T1, T2, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2)));
+  }
+  public static Func<U1, U2, U3, UResult> DowncastClone<T1, T2, T3, TResult, U1, U2, U3, UResult>(this Func<T1, T2, T3, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3)));
+  }
+  public static Func<U1, U2, U3, U4, UResult> DowncastClone<T1, T2, T3, T4, TResult, U1, U2, U3, U4, UResult>(this Func<T1, T2, T3, T4, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3, arg4) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4)));
+  }
+  public static Func<U1, U2, U3, U4, U5, U6, U7, UResult> DowncastClone<T1, T2, T3, T4, T5, T6, T7, TResult, U1, U2, U3, U4, U5, U6, U7, UResult>(this Func<T1, T2, T3, T4, T5, T6, T7, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<U5, T5> ArgConv5, Func<U6, T6> ArgConv6, Func<U7, T7> ArgConv7, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3, arg4, arg5, arg6, arg7) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5), ArgConv6(arg6), ArgConv7(arg7)));
+  }
+  public static Func<U1, U2, U3, U4, U5, UResult> DowncastClone<T1, T2, T3, T4, T5, TResult, U1, U2, U3, U4, U5, UResult>(this Func<T1, T2, T3, T4, T5, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<U5, T5> ArgConv5, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3, arg4, arg5) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5)));
+  }
+}
+// end of class FuncExtensions

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -650,7 +650,7 @@ private StmtList TrMethodContractWellformednessCheck(Method m, ExpressionTransla
         CheckWellformed(p, wfOptions, localVariables, builder, etran);
       }
 
-      if (!(m is TwoStateLemma)) {
+      if (m is not TwoStateLemma) {
         var modifies = m.Mod;
         var allowsAllocation = m.AllowsAllocation;
 
@@ -665,8 +665,16 @@ private StmtList TrMethodContractWellformednessCheck(Method m, ExpressionTransla
           outH.Add(new Boogie.IdentifierExpr(b.tok, b));
         }
         builder.Add(new Boogie.HavocCmd(m.tok, outH));
+        if (m is Constructor) {
+          var receiverType = ModuleResolver.GetReceiverType(m.tok, m);
+          var receiver = new Bpl.IdentifierExpr(m.tok, "this", TrType(receiverType));
+          var wh = BplAnd(
+            ReceiverNotNull(receiver),
+            GetWhereClause(m.tok, receiver, receiverType, etran, IsAllocType.ISALLOC));
+          builder.Add(TrAssumeCmd(m.tok, wh));
+        }
       }
-      // mark the end of the modifles/out-parameter havocking with a CaptureState; make its location be the first ensures clause, if any (and just
+      // mark the end of the modifies/out-parameter havocking with a CaptureState; make its location be the first ensures clause, if any (and just
       // omit the CaptureState if there's no ensures clause)
       if (m.Ens.Count != 0) {
         builder.AddCaptureState(m.Ens[0].E.tok, false, "post-state");

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -2828,10 +2828,9 @@ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, Me
 
         Bpl.Expr wh;
         var receiver = new Bpl.IdentifierExpr(tok, "this", TrType(receiverType));
-        if (m is Constructor && kind == MethodTranslationKind.Implementation) {
-          wh = BplAnd(
-            ReceiverNotNull(receiver),
-            GetWhereClause(tok, receiver, receiverType, etran, IsAllocType.NEVERALLOC));
+        if (m is Constructor && kind is MethodTranslationKind.Implementation or MethodTranslationKind.SpecWellformedness) {
+          // For constructors, the typical "where" condition is added in an assumption in the body, rather than in the parameter declaration itself
+          wh = null;
         } else {
           wh = BplAnd(
             ReceiverNotNull(receiver),

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs

@@ -754,20 +754,21 @@ private void SelectAllocateObject(IToken tok, Bpl.IdentifierExpr nw, Type type,
     Contract.Requires(type != null);
     Contract.Requires(builder != null);
     Contract.Requires(etran != null);
-    var udt = type as UserDefinedType;
-    if (udt != null && udt.ResolvedClass is NonNullTypeDecl) {
-      var nnt = (NonNullTypeDecl)udt.ResolvedClass;
+    if (type is UserDefinedType { ResolvedClass: NonNullTypeDecl nnt }) {
       type = nnt.RhsWithArgument(type.TypeArgs);
     }
+
     if (includeHavoc) {
       // havoc $nw;
       builder.Add(new Bpl.HavocCmd(tok, new List<Bpl.IdentifierExpr> { nw }));
-      // assume $nw != null && $Is($nw, type);
-      var nwNotNull = Bpl.Expr.Neq(nw, Predef.Null);
-      // drop the $Is conjunct if the type is "object", because "new object" allocates an object of an arbitrary type
-      var rightType = type.IsObjectQ ? Bpl.Expr.True : MkIs(nw, type);
-      builder.Add(TrAssumeCmd(tok, BplAnd(nwNotNull, rightType)));
     }
+
+    // assume $nw != null && $Is($nw, type);
+    var nwNotNull = Bpl.Expr.Neq(nw, Predef.Null);
+    // drop the $Is conjunct if the type is "object", because "new object" allocates an object of an arbitrary type
+    var rightType = type.IsObjectQ ? Bpl.Expr.True : MkIs(nw, type);
+    builder.Add(TrAssumeCmd(tok, BplAnd(nwNotNull, rightType)));
+
     // assume !$Heap[$nw, alloc];
     var notAlloc = Bpl.Expr.Not(etran.IsAlloced(tok, nw));
     builder.Add(TrAssumeCmd(tok, notAlloc));

Source/DafnyPipeline/DafnyPipeline.csproj

@@ -90,7 +90,7 @@
       <LinkBase>DafnyRuntimeJava</LinkBase>
       <CopyToOutputDirectory>Always</CopyToOutputDirectory>
     </EmbeddedResource>
-    <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJava\build\libs\DafnyRuntime-4.6.0.jar">
+    <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJava\build\libs\DafnyRuntime-4.9.0.jar">
       <LogicalName>DafnyRuntime.jar</LogicalName>
       <Link>DafnyRuntime.jar</Link>
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>

Source/DafnyRuntime/DafnyRuntime.csproj

@@ -46,7 +46,7 @@
     </Content>
   </ItemGroup>
   <PropertyGroup>
-    <DafnyRuntimeJar>DafnyRuntimeJava/build/libs/DafnyRuntime-4.6.0.jar</DafnyRuntimeJar>
+    <DafnyRuntimeJar>DafnyRuntimeJava/build/libs/DafnyRuntime-4.9.0.jar</DafnyRuntimeJar>
   </PropertyGroup>
   <Target Name="BuildDafnyRuntimeJar" AfterTargets="ResolveReferences" BeforeTargets="CoreCompile" Inputs="$(MSBuildProjectFile);@(DafnyRuntimeJavaInputFile)" Outputs="$(DafnyRuntimeJar)">
 

Source/DafnyRuntime/DafnyRuntimeJava/build.gradle

@@ -17,7 +17,7 @@ dependencies {
 }
 
 group = 'org.dafny'
-version = '4.6.0'
+version = '4.9.0'
 sourceCompatibility = '1.8'
 
 java {

Source/DafnyRuntime/DafnyRuntimeSystemModule.cs

@@ -503,7 +503,7 @@ public static T[] InitNewArray1<T>(T z, BigInteger size0) {
     }
   }
 } // end of namespace Dafny
-public static class FuncExtensions {
+internal static class FuncExtensions {
   public static Func<U, UResult> DowncastClone<T, TResult, U, UResult>(this Func<T, TResult> F, Func<U, T> ArgConv, Func<TResult, UResult> ResConv) {
     return arg => ResConv(F(ArgConv(arg)));
   }
@@ -556,6 +556,7 @@ public static Func<U1, U2, U3, U4, U5, U6, U7, U8, U9, U10, U11, U12, U13, U14,
     return (arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5), ArgConv6(arg6), ArgConv7(arg7), ArgConv8(arg8), ArgConv9(arg9), ArgConv10(arg10), ArgConv11(arg11), ArgConv12(arg12), ArgConv13(arg13), ArgConv14(arg14), ArgConv15(arg15), ArgConv16(arg16)));
   }
 }
+// end of class FuncExtensions
 #endif
 namespace _System {
 

Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy

@@ -752,7 +752,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivMod {
   }
 
   /* this is the same as writing x + (b/d) == x when b is less than d; this is true because (b/d) == 0 */
-  lemma LemmaDivMultiplesVanishFancy(x: int, b: int, d: int)
+  lemma {:vcs_split_on_every_assert} LemmaDivMultiplesVanishFancy(x: int, b: int, d: int)
     requires 0 < d
     requires 0 <= b < d
     ensures (d * x + b) / d == x

Source/Directory.Build.props

@@ -1,7 +1,7 @@
 <Project>
 
   <PropertyGroup>
-    <VersionPrefix>4.8.1</VersionPrefix>
+    <VersionPrefix>4.9.1</VersionPrefix>
     <NoWarn>1701;1702;VSTHRD200</NoWarn>
   </PropertyGroup>
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy

@@ -1,12 +1,16 @@
-// RUN: %baredafny translate rs --rust-module-name additional_module "%s"
+// RUN: %baredafny translate rs --rust-module-name additional_module "%S/more_dafny_extern.rs" "%s"
 // RUN: %exits-with -any %rm -f "%S/project_depending_on_dafny/src/additional_module.rs"
+// RUN: %exits-with -any %rm -f "%S/project_depending_on_dafny/src/more_dafny_extern.rs"
 // RUN: %mv "%S/more_dafny-rust/src/more_dafny.rs" "%S/project_depending_on_dafny/src/additional_module.rs"
+// RUN: %mv "%S/more_dafny-rust/src/more_dafny_extern.rs" "%S/project_depending_on_dafny/src/more_dafny_extern.rs"
 // RUN: "%S/project_depending_on_dafny/cargo" run > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module SubModule {
+  function {:axiom} {:extern "extern_dafny", "eight"} Eight(): (r: bv16) ensures r == 8
+
   function reverse(input: bv16): bv16 {
-    ((input & 0xFF) << 8) | ((input & 0xFF00) >> 8)
+    ((input & 0xFF) << Eight()) | ((input & 0xFF00) >> Eight())
   }
 }
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny_extern.rs

@@ -0,0 +1,5 @@
+pub mod extern_dafny {
+  pub fn eight() -> u16 {
+    8
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore

@@ -1,2 +1,3 @@
 src/additional_module.rs
+src/more_dafny_extern.rs
 target/

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs

@@ -1,4 +1,5 @@
 pub mod additional_module;
+pub mod more_dafny_extern;
 
 fn main() {
   let x = additional_module::_module::_default::reverse(10);

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/translation-records/InvalidFormat.dfy.expect

@@ -4,5 +4,5 @@ CLI: Error: malformed dtr file NoGood.dtr
 Translation was aborted because errors were found
 
 Dafny program verifier finished with 0 verified, 0 errors
-CLI: Error: cannot load WrongDafnyVersion.dtr: it was built with Dafny 10.6.0.0, which cannot be used by Dafny 4.8.1.0
+CLI: Error: cannot load WrongDafnyVersion.dtr: it was built with Dafny 10.6.0.0, which cannot be used by Dafny 4.9.0.0
 Translation was aborted because errors were found