Merge branch 'master' into deprecateUnicodeChar

dafny-lang · Apr 18, 2024 · eea5913 · eea5913
2 parents 87dcec4 + 0ca6ae9
commit eea5913
Show file tree

Hide file tree

Showing 15 changed files with 58 additions and 22 deletions.
diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs
@@ -57,7 +57,7 @@ public class Token : IToken {
 
   public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normally null at the end of parsing
   public static readonly Token NoToken = new();
-  public static readonly Token Cli = new();
+  public static readonly Token Cli = new(1, 1);
   public Token() : this(0, 0) { }
 
   public Token(int linenum, int colnum) {

diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
@@ -1725,7 +1725,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
           } else if (ArrowType.IsTotalArrowTypeName(td.Name)) {
             var rangeDefaultValue = TypeInitializationValue(udt.TypeArgs.Last(), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
             // return the lambda expression ((Ty0 x0, Ty1 x1, Ty2 x2) => rangeDefaultValue)
-            var arguments = Util.Comma(udt.TypeArgs.Count - 1, i => $"{TypeName(udt.TypeArgs[i], wr, udt.tok)} x{i}");
+            var arguments = Util.Comma(udt.TypeArgs.Count - 1, i => $"{TypeName(udt.TypeArgs[i], wr, udt.tok)} {idGenerator.FreshId("x")}");
             return $"(({arguments}) => {rangeDefaultValue})";
           } else if (((NonNullTypeDecl)td).Class is ArrayClassDecl arrayClass) {
             // non-null array type; we know how to initialize them

diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
@@ -3202,7 +3202,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
           } else if (ArrowType.IsTotalArrowTypeName(td.Name)) {
             var rangeDefaultValue = TypeInitializationValue(udt.TypeArgs.Last(), wr, tok, usePlaceboValue, constructTypeParameterDefaultsFromTypeDescriptors);
             // return the lambda expression ((Ty0 x0, Ty1 x1, Ty2 x2) -> rangeDefaultValue)
-            return $"(({Util.Comma(udt.TypeArgs.Count - 1, i => $"{BoxedTypeName(udt.TypeArgs[i], wr, udt.tok)} x{i}")}) -> {rangeDefaultValue})";
+            return $"(({Util.Comma(udt.TypeArgs.Count - 1, i => $"{BoxedTypeName(udt.TypeArgs[i], wr, udt.tok)} {idGenerator.FreshId("x")}")}) -> {rangeDefaultValue})";
           } else if (((NonNullTypeDecl)td).Class is ArrayClassDecl arrayClass) {
             // non-null array type; we know how to initialize them
             var elType = udt.TypeArgs[0];

diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
@@ -742,7 +742,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
                     var rangeDefaultValue = TypeInitializationValue(udt.TypeArgs.Last(), wr, tok, usePlaceboValue,
                       constructTypeParameterDefaultsFromTypeDescriptors);
                     // The final TypeArg contains the result type
-                    var arguments = udt.TypeArgs.SkipLast(1).Comma((_, i) => $"x{i}");
+                    var arguments = udt.TypeArgs.SkipLast(1).Comma((_, i) => idGenerator.FreshId("x"));
                     return $"(lambda {arguments}: {rangeDefaultValue})";
                   default:
                     return TypeInitializationValue(td.RhsWithArgument(udt.TypeArgs), wr, tok, usePlaceboValue,

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
@@ -188,10 +188,10 @@ public override bool Parse(string[] arguments) {
 
       try {
         if (i >= arguments.Length) {
-          return BaseParse(arguments);
+          return BaseParse(arguments, true);
         }
         MainArgs = arguments.Skip(i + 1).ToList();
-        return BaseParse(arguments.Take(i).ToArray());
+        return BaseParse(arguments.Take(i).ToArray(), true);
       } catch (Exception e) {
         ErrorWriter.WriteLine("Invalid filename: " + e.Message);
         return false;
@@ -222,7 +222,7 @@ public override void Error(string message, params string[] args) {
     /// Customized version of Microsoft.Boogie.CommandLineOptions.Parse
     /// Needed because the Boogie version writes to Console.Error
     /// </summary>
-    private bool BaseParse(string[] args) {
+    public bool BaseParse(string[] args, bool allowFile) {
       Environment = Environment + "Command Line Options: " + string.Join(" ", args);
       args = cce.NonNull<string[]>((string[])args.Clone());
       Bpl.CommandLineParseState state;
@@ -249,8 +249,10 @@ private bool BaseParse(string[] args) {
               UnknownSwitch(state);
             }
           }
-        } else {
+        } else if (allowFile) {
           AddFile(file, state);
+        } else {
+          state.Error($"Boogie option '{state.s}' must start with - or /");
         }
       }
       if (state.EncounteredErrors) {

diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs
@@ -99,7 +99,7 @@ static BoogieOptionBag() {
     DafnyOptions.RegisterLegacyBinding(BoogieArguments, (o, boogieOptions) => {
       var splitOptions = boogieOptions.SelectMany(SplitArguments).ToArray();
       if (splitOptions.Any()) {
-        o.Parse(splitOptions.ToArray());
+        o.BaseParse(splitOptions.ToArray(), false);
       }
     });
     DafnyOptions.RegisterLegacyBinding(Cores,

diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs
@@ -147,8 +147,6 @@ private async Task<IReadOnlyList<DafnyFile>> DetermineRootFiles() {
         $"command-line argument '{shortPath}' is neither a recognized option nor a Dafny input file (.dfy, .doo, or .toml).");
       if (file != null) {
         result.Add(file);
-      } else {
-        return result;
       }
     }
     if (Options.UseStdin) {
@@ -224,7 +222,7 @@ private async Task<IReadOnlyList<DafnyFile>> DetermineRootFiles() {
       transformedProgram = await documentLoader.ParseAsync(this, cancellationSource.Token);
       transformedProgram.HasParseErrors = HasErrors;
 
-      var cloner = new Cloner(true, false);
+      var cloner = new Cloner(true);
       programAfterParsing = new Program(cloner, transformedProgram);
 
       updates.OnNext(new FinishedParsing(programAfterParsing, GetDiagnosticsCopyAndClear()));

diff --git a/Source/DafnyDriver/Commands/ServerCommand.cs b/Source/DafnyDriver/Commands/ServerCommand.cs
@@ -23,6 +23,7 @@ static ServerCommand() {
       LanguageServer.VerifySnapshots,
       DafnyLangSymbolResolver.UseCaching,
       ProjectManager.UpdateThrottling,
+      ProjectManager.ReuseSolvers,
       LegacySignatureAndCompletionTable.MigrateSignatureAndCompletionTable
     );
   }

diff --git a/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyTextDocumentHandler.cs
@@ -31,7 +31,8 @@ namespace Microsoft.Dafny.LanguageServer.Handlers {
   /// break the background processing if used.
   /// </remarks>
   public class DafnyTextDocumentHandler : TextDocumentSyncHandlerBase {
-    private const string LanguageId = "dafny";
+    private const string DafnyLanguage = "dafny";
+    private const string DafnyProjectLanguage = "dafnyProject";
 
     private readonly ILogger logger;
     private readonly IProjectDatabase projects;
@@ -50,13 +51,13 @@ public DafnyTextDocumentHandler(
 
     protected override TextDocumentSyncRegistrationOptions CreateRegistrationOptions(SynchronizationCapability capability, ClientCapabilities clientCapabilities) {
       return new TextDocumentSyncRegistrationOptions {
-        DocumentSelector = DocumentSelector.ForLanguage(LanguageId),
+        DocumentSelector = DocumentSelector.ForLanguage(new[] { DafnyLanguage, DafnyProjectLanguage }),
         Change = TextDocumentSyncKind.Incremental
       };
     }
 
     public override TextDocumentAttributes GetTextDocumentAttributes(DocumentUri uri) {
-      return new TextDocumentAttributes(uri, LanguageId);
+      return new TextDocumentAttributes(uri, uri.Path.EndsWith(DafnyProject.FileName) ? DafnyProjectLanguage : DafnyLanguage);
     }
 
     public override async Task<Unit> Handle(DidOpenTextDocumentParams notification, CancellationToken cancellationToken) {

diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs
@@ -46,6 +46,11 @@ public class ProjectManager : IDisposable {
     ArgumentHelpName = "event"
   };
 
+  public static readonly Option<bool> ReuseSolvers = new("--reuse-solvers",
+    @"(experimental) Reuse solver for different verification of different document versions. Reduces verification latency but may reduce reliability of verification.".TrimStart()) {
+    ArgumentHelpName = "event"
+  };
+
   private readonly CreateMigrator createMigrator;
   public DafnyProject Project { get; }
 
@@ -55,6 +60,9 @@ public class ProjectManager : IDisposable {
   private readonly EventLoopScheduler ideStateUpdateScheduler = new();
   private readonly ILogger<ProjectManager> logger;
 
+  private readonly VerificationResultCache cache;
+  private readonly CustomStackSizePoolTaskScheduler scheduler;
+
   /// <summary>
   /// The version of this project.
   /// Is incremented when any file in the project is updated.
@@ -73,7 +81,7 @@ public class ProjectManager : IDisposable {
   private readonly DafnyOptions options;
   private readonly DafnyOptions serverOptions;
   private readonly CreateCompilation createCompilation;
-  private readonly ExecutionEngine boogieEngine;
+  private ExecutionEngine? boogieEngine;
   private readonly IFileSystem fileSystem;
   private readonly TelemetryPublisherBase telemetryPublisher;
   private readonly IProjectDatabase projectDatabase;
@@ -104,13 +112,14 @@ public ProjectManager(
 
     options = DetermineProjectOptions(project, serverOptions);
     options.Printer = new OutputLogger(logger);
-    boogieEngine = new ExecutionEngine(options, cache, scheduler);
+    this.cache = cache;
+    this.scheduler = scheduler;
     var compilationInput = new CompilationInput(options, version, Project);
     var initialIdeState = IdeState.InitialIdeState(compilationInput);
     latestIdeState = initialIdeState;
 
     observer = createIdeStateObserver(initialIdeState);
-    Compilation = createCompilation(boogieEngine, compilationInput);
+    Compilation = this.createCompilation(GetBoogie(), compilationInput);
 
     observerSubscription = Disposable.Empty;
   }
@@ -135,7 +144,7 @@ private void StartNewCompilation(Uri triggeringFile, DidChangeTextDocumentParams
 
     Compilation.Dispose();
     var input = new CompilationInput(options, version, Project);
-    Compilation = createCompilation(boogieEngine, input);
+    Compilation = createCompilation(GetBoogie(), input);
     var migratedUpdates = GetStates(Compilation);
     states = new ReplaySubject<IdeState>(1);
     var statesSubscription = observerSubscription =
@@ -155,6 +164,16 @@ private void StartNewCompilation(Uri triggeringFile, DidChangeTextDocumentParams
     TriggerVerificationForFile(triggeringFile);
   }
 
+  private ExecutionEngine GetBoogie() {
+    if (options.Get(ReuseSolvers)) {
+      boogieEngine ??= new ExecutionEngine(options, cache, scheduler);
+    } else {
+      boogieEngine?.Dispose();
+      boogieEngine = new ExecutionEngine(options, cache, scheduler);
+    }
+    return boogieEngine;
+  }
+
   private void UpdateRecentChanges(DidChangeTextDocumentParams changes, Migrator? migrator) {
     lock (RecentChanges) {
       var newChanges = changes.ContentChanges.Where(c => c.Range != null).
@@ -354,7 +373,7 @@ public void OpenDocument(Uri uri, bool triggerCompilation) {
   }
 
   public void Dispose() {
-    boogieEngine.Dispose();
+    boogieEngine?.Dispose();
     Compilation.Dispose();
     observerSubscription.Dispose();
     // Dispose the update scheduler after the observer subscription, to prevent accessing a disposed object.

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/fileThroughBoogie.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/fileThroughBoogie.dfy
@@ -0,0 +1,4 @@
+// RUN: %verify --boogie "noDashAtStart" %s 2> %t
+// RUN: %diff "%s.expect" "%t"
+
+method Foo() { }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/fileThroughBoogie.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/fileThroughBoogie.dfy.expect
@@ -0,0 +1,2 @@
+dafny: Error: Boogie option 'noDashAtStart' must start with - or /
+Use /help for available options
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/DuplicateArrowNames.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/DuplicateArrowNames.dfy
@@ -0,0 +1,8 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment
+
+// Previously, this would lead to duplicate variable names in Java, C#,
+// and Python.
+method Main() {
+  var f: nat -> nat -> bool;
+  print f(0)(1), "\n";
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/DuplicateArrowNames.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/DuplicateArrowNames.dfy.expect
@@ -0,0 +1 @@
+false
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafnydoc/doc1/TestDafnyDoc.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafnydoc/doc1/TestDafnyDoc.dfy
@@ -1,6 +1,6 @@
 // RUN: %baredafny doc --use-basename-for-filename "%s" > "%t"
-// RUN: %diff ./docs/index.html "%S"/docs-expected/index.html
-// RUN: %diff ./docs/TestModule_214638566.html "%S"/docs-expected/TestModule_214638566.html
+// RUN: %diff "%S"/docs-expected/index.html ./docs/index.html 
+// RUN: %diff "%S"/docs-expected/TestModule_214638566.html ./docs/TestModule_214638566.html 
 
 /** Test module. More about this test module. */
 module {:options "--function-syntax:4"} TestModule {