Merge branch 'fix-2852-soundness-compiler-lambda' of https://github.c…

…om/dafny-lang/dafny into fix-2852-soundness-compiler-lambda

RELEASE_NOTES.md

@@ -1,13 +1,15 @@
 # Upcoming
 
 - fix: Compiled lambdas now close only on non-ghost variables (https://github.com/dafny-lang/dafny/pull/2854)
+- fix: Crash in the LSP in some code that does not parse (https://github.com/dafny-lang/dafny/pull/2833)
 
 # 3.9.0
 
 - feat: Support for testing certain contracts at runtime with a new `/testContracts` flag (https://github.com/dafny-lang/dafny/pull/2712)
 - feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (https://github.com/dafny-lang/dafny/pull/2717)
 - feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq<string>)` (https://github.com/dafny-lang/dafny/pull/2594)
 - feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)
+- feat: Support arbitrary version of z3 for the language server. Dafny is still distributed with z3 4.8.5 and uses that version by default. (https://github.com/dafny-lang/dafny/pull/2820)
 - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)
 - fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668)
 - fix: Use the right comparison operators for bitvectors in Javascript (https://github.com/dafny-lang/dafny/pull/2716)

Source/DafnyCore/AST/Types.cs

@@ -2018,7 +2018,11 @@ public static string PrettyArrowTypeName(string arrow, List<Type> typeArgs, Type
     s += Util.Comma(typeArgs.Take(arity), arg => arg.TypeName(context, parseAble));
     if (domainNeedsParens) { s += ")"; }
     s += " " + arrow + " ";
-    s += (result ?? typeArgs.Last()).TypeName(context, parseAble);
+    if (result != null || typeArgs.Count >= 1) {
+      s += (result ?? typeArgs.Last()).TypeName(context, parseAble);
+    } else {
+      s += "<unable to infer result type>";
+    }
     return s;
   }
 

Source/DafnyCore/Dafny.atg

@@ -1,4 +1,5 @@
-/*-----------------------------------------------------------------------------
+/* (
+-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
 // Copyright by the contributors to the Dafny Project
@@ -96,7 +97,11 @@ void CheckDeclModifiers(ref DeclModifierData dmod, string declCaption, AllowedDe
   }
   if (dmod.IsGhost) {
     if ((allowed & AllowedDeclModifiers.AlreadyGhost) != 0) {
-      SemErr(dmod.GhostToken, $"{declCaption} cannot be declared 'ghost' (it is 'ghost' by default)");
+      if (declCaption.Contains("-by-method")) {
+        SemErr(dmod.GhostToken, $"{declCaption} has a ghost function body and a non-ghost method body; {declCaption} declaration does not use the 'ghost' keyword.");
+      } else {
+        SemErr(dmod.GhostToken, $"{declCaption} cannot be declared 'ghost' (it is 'ghost' by default)");
+      }
       dmod.IsGhost = false;
     } else if ((allowed & AllowedDeclModifiers.Ghost) == 0) {
       SemErr(dmod.GhostToken, $"{declCaption} cannot be declared 'ghost'");

Source/DafnyCore/DafnyOptions.cs

@@ -1239,8 +1239,9 @@ focal predicate P to P#[_k-1].
 
 /extractCounterexample
     If verification fails, report a detailed counterexample for the
-    first failing assertion. Requires specifying the /mv option as well
-    as /proverOpt:O:model_compress=false and
+    first failing assertion. Requires specifying the /mv:<file> option as well
+    as /proverOpt:O:model_compress=false (for z3 version < 4.8.7) or
+    /proverOpt:O:model.compact=false (for z3 version >= 4.8.7), and
     /proverOpt:O:model.completion=true.
 
 /countVerificationErrors:<n>

Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs

@@ -873,7 +873,10 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
       return result;
     }
 
-    private const string PleaseEnableModelCompressFalse = "Please enable /proverOpt:O:model_compress=false, otherwise you'll get unexpected values.";
+    private const string PleaseEnableModelCompressFalse =
+      "Please enable /proverOpt:O:model_compress=false (for z3 version < 4.8.7)" +
+      " or /proverOpt:O:model.compact=false (for z3 version >= 4.8.7)," +
+      " otherwise you'll get unexpected values.";
 
     /// <summary>
     /// Return the name of the field represented by the given element.

Source/DafnyLanguageServer/DafnyLanguageServer.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics;
+using System.Text.RegularExpressions;
 using Microsoft.Dafny.LanguageServer.Handlers;
 using Microsoft.Dafny.LanguageServer.Language;
 using Microsoft.Dafny.LanguageServer.Workspace;
@@ -14,7 +15,7 @@
 using System.Threading.Tasks;
 using Microsoft.Boogie.SMTLib;
 using Microsoft.Extensions.Options;
-using OmniSharp.Extensions.LanguageServer.Protocol.Window;
+using Action = System.Action;
 
 namespace Microsoft.Dafny.LanguageServer {
   public static class DafnyLanguageServer {
@@ -55,20 +56,61 @@ private static Task InitializeAsync(ILanguageServer server, InitializeParams req
       return Task.CompletedTask;
     }
 
+    private static readonly Regex Z3VersionRegex = new Regex(@"Z3 version (?<major>\d+)\.(?<minor>\d+)\.(?<patch>\d+)");
+
     private static void PublishSolverPath(ILanguageServer server) {
       var telemetryPublisher = server.GetRequiredService<ITelemetryPublisher>();
       string solverPath;
       try {
         var proverOptions = new SMTLibSolverOptions(DafnyOptions.O);
         proverOptions.Parse(DafnyOptions.O.ProverOptions);
         solverPath = proverOptions.ExecutablePath();
+        HandleZ3Version(telemetryPublisher, proverOptions);
       } catch (Exception e) {
         solverPath = $"Error while determining solver path: {e}";
       }
 
       telemetryPublisher.PublishSolverPath(solverPath);
     }
 
+    private static void HandleZ3Version(ITelemetryPublisher telemetryPublisher, SMTLibSolverOptions proverOptions) {
+      var z3Process = new ProcessStartInfo(proverOptions.ProverPath, "-version") {
+        CreateNoWindow = true,
+        RedirectStandardError = true,
+        RedirectStandardOutput = true,
+        RedirectStandardInput = true
+      };
+      var run = Process.Start(z3Process);
+      if (run == null) {
+        return;
+      }
+
+      var actualOutput = run.StandardOutput.ReadToEnd();
+      run.WaitForExit();
+      var versionMatch = Z3VersionRegex.Match(actualOutput);
+      if (!versionMatch.Success) {
+        // Might be another solver.
+        return;
+      }
+
+      telemetryPublisher.PublishZ3Version(versionMatch.Value);
+      var major = int.Parse(versionMatch.Groups["major"].Value);
+      var minor = int.Parse(versionMatch.Groups["minor"].Value);
+      var patch = int.Parse(versionMatch.Groups["patch"].Value);
+      if (major <= 4 && (major < 4 || minor <= 8) && (minor < 8 || patch <= 6)) {
+        return;
+      }
+
+      var toReplace = "O:model_compress=false";
+      var i = DafnyOptions.O.ProverOptions.IndexOf(toReplace);
+      if (i == -1) {
+        telemetryPublisher.PublishUnhandledException(new Exception($"Z3 version is > 4.8.6 but I did not find {toReplace} in the prover options:" + string.Join(" ", DafnyOptions.O.ProverOptions)));
+        return;
+      }
+
+      DafnyOptions.O.ProverOptions[i] = "O:model.compact=false";
+    }
+
     /// <summary>
     /// Load the plugins for the Dafny pipeline
     /// </summary>

Source/DafnyLanguageServer/Workspace/DocumentOptions.cs

@@ -28,7 +28,7 @@ static DocumentOptions() {
 
     public List<string> AugmentedProverOptions =>
       DafnyOptions.O.ProverOptions.Concat(new List<string>() {
-        "O:model_compress=false",
+        "O:model_compress=false", // Replaced by "O:model.compact=false" if z3's version is > 4.8.6
         "O:model.completion=true",
         "O:model_evaluator.completion=true"
       }).ToList();

Source/DafnyLanguageServer/Workspace/ITelemetryPublisher.cs

@@ -12,7 +12,8 @@ public interface ITelemetryPublisher {
     protected enum TelemetryEventKind {
       UpdateComplete,
       UnhandledException,
-      SolverPath
+      SolverPath,
+      Z3Version
     }
 
     /// <summary>
@@ -37,5 +38,9 @@ public void PublishUpdateComplete() {
     public void PublishSolverPath(string solverPath) {
       PublishTelemetry(TelemetryEventKind.SolverPath, solverPath);
     }
+
+    public void PublishZ3Version(string z3Version) {
+      PublishTelemetry(TelemetryEventKind.Z3Version, z3Version);
+    }
   }
 }

Test/dafny0/ParseErrors.dfy.expect

@@ -56,15 +56,15 @@ ParseErrors.dfy(220,2): Error: a module cannot be declared 'static'
 ParseErrors.dfy(226,2): Error: a datatype or codatatype cannot be declared 'ghost'
 ParseErrors.dfy(227,2): Error: a module cannot be declared 'ghost'
 ParseErrors.dfy(234,51): Error: a 'by method' implementation is not allowed on a twostate function
-ParseErrors.dfy(234,2): Error: a function-by-method cannot be declared 'ghost' (it is 'ghost' by default)
+ParseErrors.dfy(234,2): Error: a function-by-method has a ghost function body and a non-ghost method body; a function-by-method declaration does not use the 'ghost' keyword.
 ParseErrors.dfy(235,52): Error: a 'by method' implementation is not allowed on a twostate function
 ParseErrors.dfy(236,50): Error: a 'by method' implementation is not allowed on a twostate predicate
-ParseErrors.dfy(236,2): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default)
+ParseErrors.dfy(236,2): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword.
 ParseErrors.dfy(237,51): Error: a 'by method' implementation is not allowed on a twostate predicate
 ParseErrors.dfy(240,47): Error: a 'by method' implementation is not allowed on an extreme predicate
-ParseErrors.dfy(240,2): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default)
+ParseErrors.dfy(240,2): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword.
 ParseErrors.dfy(241,50): Error: a 'by method' implementation is not allowed on an extreme predicate
-ParseErrors.dfy(241,2): Error: a predicate-by-method cannot be declared 'ghost' (it is 'ghost' by default)
+ParseErrors.dfy(241,2): Error: a predicate-by-method has a ghost function body and a non-ghost method body; a predicate-by-method declaration does not use the 'ghost' keyword.
 ParseErrors.dfy(244,55): Error: a 'by method' implementation is not allowed on a twostate function
 ParseErrors.dfy(244,2): Error: a function-by-method cannot be declared 'abstract'
 ParseErrors.dfy(245,54): Error: a 'by method' implementation is not allowed on a twostate predicate