Merge branch 'master' into github-issue-511

.github/workflows/integration-tests-reusable.yml

@@ -95,7 +95,7 @@ jobs:
       run: python -m pip install --upgrade pip
     - name: Install lit
       run: pip install lit OutputCheck pyyaml
-    - uses: actions/setup-node@v3
+    - uses: actions/setup-node@v4
     - run: npm install bignumber.js
     - name: Checkout Dafny
       uses: actions/checkout@v4

.github/workflows/publish-release-reusable.yml

@@ -67,7 +67,7 @@ jobs:
       with:
         java-version: 18
         distribution: corretto
-    - uses: actions/setup-node@v3
+    - uses: actions/setup-node@v4
     - run: npm install bignumber.js
     - name: Set up Python
       uses: actions/setup-python@v4

.github/workflows/standard-libraries.yml

@@ -19,7 +19,7 @@ jobs:
 
     steps:
       - name: Checkout Dafny
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           submodules: true
       - name: Set up JDK 18

.gitignore

@@ -39,7 +39,6 @@ Source/DafnyCore/Scanner.cs.old
 
 Source/DafnyRuntime/MSBuild_Logs/
 TestResults/
-Test/.lit_test_times.txt
 
 Docs/OnlineTutorial/DocumentationTransducer.exe
 Docs/OnlineTutorial/DocumentationTransducer.pdb
@@ -74,4 +73,3 @@ docs/dev/*.fix
 docs/dev/*.feat
 docs/dev/*.break
 
-

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -3,7 +3,6 @@
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
-using System.Reflection;
 using System.Text;
 using System.Threading;
 using Microsoft.Extensions.Logging;
@@ -61,11 +60,11 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
 
       var parseResult = ParseFileWithErrorHandling(
         errorReporter.Options,
+        dafnyFile.IsPrerefined,
         dafnyFile.GetContent,
         dafnyFile.Origin,
         dafnyFile.Uri,
-        cancellationToken
-      );
+        cancellationToken);
       if (parseResult.ErrorReporter.ErrorCount != 0) {
         logger.LogDebug($"encountered {parseResult.ErrorReporter.ErrorCount} errors while parsing {dafnyFile.Uri}");
       }
@@ -98,12 +97,13 @@ public virtual Program ParseFiles(string programName, IReadOnlyList<DafnyFile> f
   }
 
   private DfyParseResult ParseFileWithErrorHandling(DafnyOptions options,
+    bool parseAsDooFile,
     Func<TextReader> getContent,
     IToken origin,
     Uri uri,
     CancellationToken cancellationToken) {
     try {
-      return ParseFile(options, getContent, uri, cancellationToken);
+      return ParseFile(options, parseAsDooFile, getContent, uri, cancellationToken);
     } catch (IOException e) {
       if (origin == null) {
         throw;
@@ -227,11 +227,11 @@ CancellationToken cancellationToken
       cancellationToken.ThrowIfCancellationRequested();
       var parseIncludeResult = ParseFileWithErrorHandling(
         errorReporter.Options,
+        top.IsPrerefined,
         top.GetContent,
         top.Origin,
         top.Uri,
-        cancellationToken
-      );
+        cancellationToken);
       result.Add(parseIncludeResult);
 
       foreach (var include in parseIncludeResult.Module.Includes) {
@@ -262,12 +262,12 @@ private DafnyFile IncludeToDafnyFile(SystemModuleManager systemModuleManager, Er
   /// Returns the number of parsing errors encountered.
   /// Note: first initialize the Scanner.
   ///</summary>
-  protected virtual DfyParseResult ParseFile(DafnyOptions options, Func<TextReader> getReader,
+  protected virtual DfyParseResult ParseFile(DafnyOptions options, bool parseAsDooFile, Func<TextReader> getReader,
     Uri uri, CancellationToken cancellationToken) /* throws System.IO.IOException */ {
     Contract.Requires(uri != null);
     using var reader = getReader();
     var text = SourcePreprocessor.ProcessDirectives(reader, new List<string>());
-    return ParseFile(options, text, uri, cancellationToken);
+    return ParseFile(options, parseAsDooFile, text, uri, cancellationToken);
   }
 
   ///<summary>
@@ -276,9 +276,9 @@ protected virtual DfyParseResult ParseFile(DafnyOptions options, Func<TextReader
   /// Returns the number of parsing errors encountered.
   /// Note: first initialize the Scanner with the given Errors sink.
   ///</summary>
-  private static DfyParseResult ParseFile(DafnyOptions options, string /*!*/ s, Uri /*!*/ uri, CancellationToken cancellationToken) {
+  private static DfyParseResult ParseFile(DafnyOptions options, bool parseAsDooFile, string /*!*/ content, Uri /*!*/ uri, CancellationToken cancellationToken) {
     var batchErrorReporter = new BatchErrorReporter(options);
-    Parser parser = SetupParser(s, uri, batchErrorReporter, cancellationToken);
+    Parser parser = SetupParser(parseAsDooFile, content, uri, batchErrorReporter, cancellationToken);
     parser.Parse();
 
     if (parser.theModule.DefaultClass.Members.Count == 0 && parser.theModule.Includes.Count == 0 && !parser.theModule.SourceDecls.Any()
@@ -289,7 +289,8 @@ private static DfyParseResult ParseFile(DafnyOptions options, string /*!*/ s, Ur
     return new DfyParseResult(batchErrorReporter, parser.theModule, parser.SystemModuleModifiers);
   }
 
-  private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, ErrorReporter /*!*/ errorReporter, CancellationToken cancellationToken) {
+  private static Parser SetupParser(bool parseAsDooFile, string s /*!*/, Uri uri /*!*/,
+    ErrorReporter errorReporter /*!*/, CancellationToken cancellationToken) {
     Contract.Requires(s != null);
     Contract.Requires(uri != null);
     System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle);
@@ -303,7 +304,7 @@ private static Parser SetupParser(string /*!*/ s, Uri /*!*/ uri, ErrorReporter /
     var errors = new Errors(errorReporter);
 
     var scanner = new Scanner(ms, errors, uri, firstToken: firstToken);
-    return new Parser(errorReporter.Options, scanner, errors, cancellationToken);
+    return new Parser(errorReporter.Options, parseAsDooFile, scanner, errors, cancellationToken);
   }
 
   public Program Parse(string source, Uri uri, ErrorReporter reporter) {

Source/DafnyCore/AST/Members/Function.cs

@@ -247,7 +247,7 @@ public Function(RangeToken range, Name name, bool hasStaticKeyword, bool isGhost
     this.ByMethodTok = byMethodTok;
     this.ByMethodBody = byMethodBody;
     this.SignatureEllipsis = signatureEllipsis;
-    this.IsOpaque = isOpaque;
+    this.IsOpaque = isOpaque || Attributes.Contains(attributes, "opaque");
 
     if (attributes != null) {
       List<Expression> args = Attributes.FindExpressions(attributes, "fuel");

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -597,14 +597,15 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke
       Contract.Requires(tok != null);
       Contract.Requires(wr != null);
 
-      return DatatypeWrapperEraser.SimplifyType(Options, type, true) switch {
+      var simplifiedType = DatatypeWrapperEraser.SimplifyType(Options, type, true);
+      return simplifiedType switch {
         var x when x.IsBuiltinArrowType => $"{DafnyDefaults}.pointer",
         // unresolved proxy; just treat as bool, since no particular type information is apparently needed for this type
         BoolType or TypeProxy => $"{DafnyDefaults}.bool",
         CharType => UnicodeCharEnabled ? $"{DafnyDefaults}.codepoint" : $"{DafnyDefaults}.char",
         IntType or BitvectorType => $"{DafnyDefaults}.int",
         RealType => $"{DafnyDefaults}.real",
-        SeqType or SetType or MultiSetType or MapType => CollectionTypeDescriptor(),
+        SeqType or SetType or MultiSetType or MapType => TypeHelperName(simplifiedType.NormalizeExpandKeepConstraints()),
         UserDefinedType udt => udt.ResolvedClass switch {
           TypeParameter tp => TypeParameterDescriptor(tp),
           ClassLikeDecl or NonNullTypeDecl => $"{DafnyDefaults}.pointer",
@@ -615,10 +616,6 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke
         _ => throw new cce.UnreachableException()
       };
 
-      string CollectionTypeDescriptor() {
-        return TypeHelperName(type.NormalizeExpandKeepConstraints());
-      }
-
       string TypeParameterDescriptor(TypeParameter typeParameter) {
         if ((thisContext != null && typeParameter.Parent is TopLevelDeclWithMembers and not TraitDecl) || typeParameter.Parent is IteratorDecl) {
           return $"self.{typeParameter.GetCompileName(Options)}";

Source/DafnyCore/Dafny.atg

@@ -21,6 +21,7 @@ using System.CommandLine;
 using static Microsoft.Dafny.ParseErrors;
 COMPILER Dafny
 /*--------------------------------------------------------------------------*/
+readonly bool parseAsDooFile;
 readonly Expression/*!*/ dummyExpr;
 readonly AssignmentRhs/*!*/ dummyRhs;
 readonly FrameExpression/*!*/ dummyFrameExpr;
@@ -178,10 +179,11 @@ public void ApplyOptionsFromAttributes(Attributes attrs) {
   }
 }
 
-public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, CancellationToken cancellationToken)
+public Parser(DafnyOptions options, bool parseAsDooFile, Scanner/*!*/ scanner, Errors/*!*/ errors, CancellationToken cancellationToken)
   : this(scanner, errors, cancellationToken)  // the real work
 {
   // initialize readonly fields
+  this.parseAsDooFile = parseAsDooFile;
   dummyExpr = new LiteralExpr(Token.NoToken);
   dummyRhs = new ExprRhs(dummyExpr);
   dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
@@ -442,7 +444,7 @@ string UnwildIdent(IToken x, bool allowWildcardId) {
   if (x.val.StartsWith("_")) {
     if (allowWildcardId && x.val.Length == 1) {
       return "_v" + anonymousIds++;
-    } else {
+    } else if (!parseAsDooFile) {
       SemErr(ErrorId.p_no_leading_underscore, x, "cannot declare identifier beginning with underscore");
     }
   }
@@ -5308,7 +5310,7 @@ Name<out Name name>
 // Identifier, disallowing leading underscores
 NoUSIdent<out IToken/*!*/ x>
 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
-  Ident<out x>     (. if (x.val.StartsWith("_")) {
+  Ident<out x>     (. if (x.val.StartsWith("_") && !parseAsDooFile) {
                         SemErr(ErrorId.p_no_leading_underscore_2, x, 
                           "cannot declare identifier beginning with underscore");
                       }

Source/DafnyCore/DafnyFile.cs

@@ -16,6 +16,7 @@ public class DafnyFile {
   public string BaseName { get; private set; }
   public bool IsPreverified { get; set; }
   public bool IsPrecompiled { get; set; }
+  public bool IsPrerefined { get; private set; }
   public Func<TextReader> GetContent { get; set; }
   public Uri Uri { get; }
   [CanBeNull] public IToken Origin { get; }
@@ -102,6 +103,7 @@ public DafnyFile(DafnyOptions options, Uri uri, [CanBeNull] IToken origin = null
       // the DooFile class should encapsulate the serialization logic better
       // and expose a Program instead of the program text.
       GetContent = () => new StringReader(dooFile.ProgramText);
+      IsPrerefined = true;
     } else if (Extension == ".dll") {
       IsPreverified = true;
       // Technically only for C#, this is for backwards compatability

Source/DafnyCore/ProofDependencyWarnings.cs

@@ -16,7 +16,8 @@ public static void WarnAboutSuspiciousDependencies(DafnyOptions dafnyOptions, Er
     }
   }
 
-  public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter, ProofDependencyManager depManager, DafnyConsolePrinter.ImplementationLogEntry logEntry, DafnyConsolePrinter.VerificationResultLogEntry result) {
+  public static void WarnAboutSuspiciousDependenciesForImplementation(DafnyOptions dafnyOptions, ErrorReporter reporter,
+    ProofDependencyManager depManager, DafnyConsolePrinter.ImplementationLogEntry logEntry, DafnyConsolePrinter.VerificationResultLogEntry result) {
     if (result.Outcome != ConditionGeneration.Outcome.Correct) {
       return;
     }

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -315,7 +315,7 @@ public void ResolveAttributes(IAttributeBearingDeclaration attributeHost, Resolu
         if (attr.Args != null) {
           foreach (var arg in attr.Args) {
             Contract.Assert(arg != null);
-            if (!(Attributes.Contains(attributeHost.Attributes, "opaque_reveal") && attr.Name == "fuel" && arg is NameSegment)) {
+            if (!(Attributes.Contains(attributeHost.Attributes, "opaque_reveal") && attr.Name is "revealedFunction" && arg is NameSegment)) {
               ResolveExpression(arg, resolutionContext);
             } else {
               ResolveRevealLemmaAttribute(arg);

Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs

@@ -69,9 +69,7 @@ protected void AnnotateRevealFunction(Method lemma, Function f) {
     rr.Type = new ArrowType(f.tok, args, new IntType());
     nameSegment.ResolvedExpression = rr;
     nameSegment.Type = rr.Type;
-    LiteralExpr low = new LiteralExpr(f.tok, 1);
-    LiteralExpr hi = new LiteralExpr(f.tok, 2);
-    lemma.Attributes = new Attributes("fuel", new List<Expression>() { nameSegment, low, hi }, lemma.Attributes);
+    lemma.Attributes = new Attributes("revealedFunction", new List<Expression>() { nameSegment }, lemma.Attributes);
   }
 
 
@@ -99,10 +97,8 @@ private bool ShouldBeRevealed(MemberDecl member) {
   }
   private void GenerateRevealLemma(MemberDecl m, List<MemberDecl> newDecls) {
     if (m is Function f) {
-      // mark the opaque function with {:fuel 0, 0}
-      var amount = new LiteralExpr(m.tok, 0);
-      m.Attributes = new Attributes("fuel", new List<Expression>() { amount, amount }, m.Attributes);
 
+      // TODO: The following comment will need to be updated.
       // That is, given:
       //   function {:opaque} foo(x:int, y:int) : int
       //     requires 0 <= x < 5;

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -1918,6 +1918,7 @@ public Boogie.QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute)
               || attr.Name == "timeLimitMultiplier"  // This is a Dafny-specific attribute
               || (attr.Name == "timeLimit" && hasNewTimeLimit)
               || (attr.Name == "rlimit" && hasNewRLimit)
+              || (attr.Name == "revealedFunction")
           ) {
             continue;
           }

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -1724,25 +1724,12 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
 
         // add the fuel assumption for the reveal method of a opaque method
         if (IsOpaqueRevealLemma(m)) {
-          List<Expression> args = Attributes.FindExpressions(m.Attributes, "fuel");
+          List<Expression> args = Attributes.FindExpressions(m.Attributes, "revealedFunction");
           if (args != null) {
             MemberSelectExpr selectExpr = args[0].Resolved as MemberSelectExpr;
             if (selectExpr != null) {
               Function f = selectExpr.Member as Function;
-              FuelConstant fuelConstant = this.functionFuel.Find(x => x.f == f);
-              if (fuelConstant != null) {
-                Boogie.Expr startFuel = fuelConstant.startFuel;
-                Boogie.Expr startFuelAssert = fuelConstant.startFuelAssert;
-                Boogie.Expr moreFuel_expr = fuelConstant.MoreFuel(sink, predef, f.IdGenerator);
-                Boogie.Expr layer = etran.layerInterCluster.LayerN(1, moreFuel_expr);
-                Boogie.Expr layerAssert = etran.layerInterCluster.LayerN(2, moreFuel_expr);
-
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuel, layer), null, null, null));
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(startFuelAssert, layerAssert), null, null, null));
-                AddEnsures(ens, Ensures(m.tok, true, GetRevealConstant(f), null, null, null));
-
-                AddEnsures(ens, Ensures(m.tok, true, Boogie.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, moreFuel_expr), moreFuel_expr), null, null, "Shortcut to LZ"));
-              }
+              AddEnsures(ens, Ensures(m.tok, true, GetRevealConstant(f), null, null, null));
             }
           }
         }