Merge branch 'master' into fix-unary-minus

.github/workflows/msbuild.yml

@@ -34,6 +34,9 @@ jobs:
  - name: Restore tools
  working-directory: dafny
  run: dotnet tool restore
+ - name: Check whitespace and style
+ working-directory: dafny
+ run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
  - name: Get Boogie Version
  run: |
  sudo apt-get update
@@ -51,9 +54,6 @@ jobs:
  - name: Build Dafny with local Boogie
  working-directory: dafny
  run: dotnet build Source/Dafny.sln
- - name: Check whitespace and style
- working-directory: dafny
- run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyRuntime/DafnyRuntimeSystemModule.cs
  - name: Create NuGet package (just to make sure it works)
  run: dotnet pack --no-build dafny/Source/Dafny.sln
  - name: Check uniformity of integration tests that exercise backends

.pre-commit-config.yaml

@@ -4,5 +4,5 @@ repos:
  - id: dotnet-format
  name: dotnet-format
  language: system
- entry: dotnet tool run dotnet-format --folder -w --include
+ entry: dotnet format whitespace Source/Dafny.sln --include
  types_or: ["c#"]

Makefile

@@ -62,7 +62,7 @@ z3-ubuntu:
  chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 format:
- dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs
+ dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
 
 clean:
  (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)

Source/DafnyCore.Test/DafnyProjectTest.cs

@@ -1,6 +1,6 @@
 using Microsoft.Dafny;
 
-namespace DafnyCore.Test; 
+namespace DafnyCore.Test;
 
 public class DafnyProjectTest {
  [Fact]

Source/DafnyCore/AST/Members/Function.cs

@@ -28,6 +28,8 @@ public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFor
  k = WhatKind;
  }
 
+ // If this function is opaque due to the opaque keyword, include it.
+ k = (IsOpaque && !Attributes.Contains(Attributes, "opaque")) ? "opaque " + k : k;
  return HasStaticKeyword ? "static " + k : k;
  }
 

Source/DafnyCore/AST/Members/ICanAutoReveal.cs

@@ -1,4 +1,4 @@
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public interface ICanAutoRevealDependencies {
  public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, DafnyOptions Options, ErrorReporter Reporter);

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -79,6 +79,11 @@ public class CsharpCompiler : SinglePassCompiler {
  wr.WriteLine("using System;");
  wr.WriteLine("using System.Numerics;");
  wr.WriteLine("using System.Collections;");
+
+ if (Options.Get(CommonOptionBag.ExecutionCoverageReport) != null) {
+ wr.WriteLine("using System.IO;");
+ }
+
  if (program.Options.SystemModuleTranslationMode == CommonOptionBag.SystemModuleMode.OmitAllOtherModules) {
  wr.WriteLine("#endif");
  }
@@ -95,6 +100,9 @@ public class CsharpCompiler : SinglePassCompiler {
  EmitRuntimeSource("DafnyRuntimeCsharp", wr, false);
  }
 
+ if (Options.Get(CommonOptionBag.ExecutionCoverageReport) != null) {
+ EmitCoverageReportInstrumentation(program, wr);
+ }
  }
 
  /// <summary>
@@ -3435,5 +3443,30 @@ protected class ClassWriter : IClassWriter {
  TrStmt(recoveryBody, catchBlock);
  }
 
+ protected void EmitCoverageReportInstrumentation(Program program, ConcreteSyntaxTree wr) {
+ wr.WriteLine(@"
+namespace DafnyProfiling {
+ public class CodeCoverage {
+ static uint[] tallies;
+ static string talliesFileName;
+ public static void Setup(int size, string theTalliesFileName) {
+ tallies = new uint[size];
+ talliesFileName = theTalliesFileName;
+ }
+ public static void TearDown() {
+ using TextWriter talliesWriter = new StreamWriter(
+ new FileStream(talliesFileName, FileMode.Create));
+ for (var i = 0; i < tallies.Length; i++) {
+ talliesWriter.WriteLine(""{0}"", tallies[i]);
+ }
+ tallies = null;
+ }
+ public static bool Record(int id) {
+ tallies[id]++;
+ return true;
+ }
+ }
+}");
+ }
  }
 }

Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs

@@ -158,6 +158,10 @@ private class CSharpCompilationResult {
  return RunProcess(psi, outputWriter, errorWriter) == 0;
  }
 
+ public override void PopulateCoverageReport(CoverageReport coverageReport) {
+ compiler.Coverage.PopulateCoverageReport(coverageReport);
+ }
+
  public CsharpBackend(DafnyOptions options) : base(options) {
  }
 }

Source/DafnyCore/Compilers/CoverageInstrumenter.cs

@@ -1,18 +1,25 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.IO;
+using System.Linq;
 
 namespace Microsoft.Dafny.Compilers;
 
 public class CoverageInstrumenter {
  private readonly SinglePassCompiler compiler;
  private List<(IToken, string)>/*?*/ legend; // non-null implies options.CoverageLegendFile is non-null
+ private string talliesFilePath;
 
  public CoverageInstrumenter(SinglePassCompiler compiler) {
  this.compiler = compiler;
- if (compiler.Options?.CoverageLegendFile != null) {
+ if (compiler.Options?.CoverageLegendFile != null
+ || compiler.Options?.Get(CommonOptionBag.ExecutionCoverageReport) != null) {
  legend = new List<(IToken, string)>();
  }
+
+ if (compiler.Options?.Get(CommonOptionBag.ExecutionCoverageReport) != null) {
+ talliesFilePath = Path.GetTempFileName();
+ }
  }
 
  public bool IsRecording {
@@ -55,7 +62,11 @@ public class CoverageInstrumenter {
  public void EmitSetup(ConcreteSyntaxTree wr) {
  Contract.Requires(wr != null);
  if (legend != null) {
- wr.Write("DafnyProfiling.CodeCoverage.Setup({0})", legend.Count);
+ wr.Write("DafnyProfiling.CodeCoverage.Setup({0}", legend.Count);
+ if (talliesFilePath != null) {
+ wr.Write($", \"{talliesFilePath}\"");
+ }
+ wr.Write(")");
  compiler.EndStmt(wr);
  }
  }
@@ -69,7 +80,7 @@ public class CoverageInstrumenter {
  }
 
  public void WriteLegendFile() {
- if (legend != null) {
+ if (compiler.Options?.CoverageLegendFile != null) {
  var filename = compiler.Options.CoverageLegendFile;
  Contract.Assert(filename != null);
  TextWriter wr = filename == "-" ? compiler.Options.OutputWriter : new StreamWriter(new FileStream(Path.GetFullPath(filename), System.IO.FileMode.Create));
@@ -82,4 +93,20 @@ public class CoverageInstrumenter {
  legend = null;
  }
  }
+
+ public void PopulateCoverageReport(CoverageReport coverageReport) {
+ var coverageReportDir = compiler.Options?.Get(CommonOptionBag.ExecutionCoverageReport);
+ if (coverageReportDir != null) {
+ var tallies = File.ReadLines(talliesFilePath).Select(int.Parse).ToArray();
+ foreach (var ((token, _), tally) in legend.Zip(tallies)) {
+ var label = tally == 0 ? CoverageLabel.NotCovered : CoverageLabel.FullyCovered;
+ // For now we only identify branches at the line granularity,
+ // which matches what `dafny generate-tests ... --coverage-report` does as well.
+ var rangeToken = new RangeToken(new Token(token.line, 1), new Token(token.line + 1, 0));
+ rangeToken.Uri = token.Uri;
+ coverageReport.LabelCode(rangeToken, label);
+ }
+ }
+ }
+
 }

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -56,7 +56,8 @@ class CppCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.UnicodeChars,
  Feature.ConvertingValuesToStrings,
- Feature.BuiltinsInRuntime
+ Feature.BuiltinsInRuntime,
+ Feature.RuntimeCoverageReport
  };
 
  private List<DatatypeDecl> datatypeDecls = new();

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -91,7 +91,8 @@ class DafnyCompiler : SinglePassCompiler {
  Feature.SubtypeConstraintsInQuantifiers,
  Feature.TuplesWiderThan20,
  Feature.ForLoops,
- Feature.Traits
+ Feature.Traits,
+ Feature.RuntimeCoverageReport
  };
 
  private readonly List<string> Imports = new() { DafnyDefaultModule };

Source/DafnyCore/Compilers/Dafny/WrapException.cs

@@ -1,4 +1,4 @@
-namespace Microsoft.Dafny.Compilers; 
+namespace Microsoft.Dafny.Compilers;
 
 public class WrapException {
 

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Data.SqlTypes;
 using System.Diagnostics;
 using System.Diagnostics.Contracts;

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -27,7 +27,8 @@ class GoCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.ExternalConstructors,
  Feature.SubsetTypeTests,
- Feature.AllUnderscoreExternalModuleNames
+ Feature.AllUnderscoreExternalModuleNames,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -29,7 +29,8 @@ public class JavaCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.TuplesWiderThan20,
  Feature.ArraysWithMoreThan16Dims,
- Feature.ArrowsWithMoreThan16Arguments
+ Feature.ArrowsWithMoreThan16Arguments,
+ Feature.RuntimeCoverageReport,
  };
 
  const string DafnySetClass = "dafny.DafnySet";

Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs

@@ -26,7 +26,8 @@ class JavaScriptCompiler : SinglePassCompiler {
  Feature.MethodSynthesis,
  Feature.ExternalConstructors,
  Feature.SubsetTypeTests,
- Feature.SeparateCompilation
+ Feature.SeparateCompilation,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/Library/LibraryBackend.cs

@@ -6,7 +6,7 @@
 using System.Linq;
 using DafnyCore;
 
-namespace Microsoft.Dafny.Compilers; 
+namespace Microsoft.Dafny.Compilers;
 
 public class LibraryBackend : ExecutableBackend {
  public LibraryBackend(DafnyOptions options) : base(options) {
@@ -28,7 +28,8 @@ public class LibraryBackend : ExecutableBackend {
  public override bool SupportsInMemoryCompilation => false;
 
  public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
- Feature.LegacyCLI
+ Feature.LegacyCLI,
+ Feature.RuntimeCoverageReport
  };
 
  // Necessary since Compiler is null

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

@@ -34,7 +34,8 @@ class PythonCompiler : SinglePassCompiler {
 
  public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
  Feature.SubsetTypeTests,
- Feature.MethodSynthesis
+ Feature.MethodSynthesis,
+ Feature.RuntimeCoverageReport
  };
 
  public override string ModuleSeparator => "_";

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -5741,21 +5741,18 @@ private class ArrayLvalueImpl : ILvalue {
  IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false,
  bool isSubfiltering = false) {
  if (!boundVarType.Equals(collectionElementType, true) &&
- boundVarType.NormalizeExpand(true) is UserDefinedType
- {
+ boundVarType.NormalizeExpand(true) is UserDefinedType {
  TypeArgs: var typeArgs,
  ResolvedClass:
- SubsetTypeDecl
- {
+ SubsetTypeDecl {
  TypeArgs: var typeParametersArgs,
  Var: var variable,
  Constraint: var constraint
  }
  }) {
- if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType
- {
- ResolvedClass: SubsetTypeDecl
- } normalizedVariableType) {
+ if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType {
+ ResolvedClass: SubsetTypeDecl
+ } normalizedVariableType) {
  wr = MaybeInjectSubsetConstraint(boundVar, normalizedVariableType, collectionElementType,
  inLetExprBody, tok, wr, isReturning, elseReturnValue, true);
  }
@@ -6061,6 +6058,5 @@ private class ArrayLvalueImpl : ILvalue {
  }
 
  protected abstract void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr);
-
  }
 }

Source/DafnyCore/CoverageReport/CoverageReport.cs

@@ -5,13 +5,13 @@
 using System.Linq;
 using System.Threading;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public class CoverageReport {
 
  private static int nextUniqueId = 0;
 
- private readonly Dictionary<string, List<CoverageSpan>> labelsByFile;
+ private readonly Dictionary<Uri, List<CoverageSpan>> labelsByFile;
  public readonly string Name; // the name to assign to this coverage report
  public readonly string Units; // the units of coverage (plural). This will be written in the coverage report table.
  private readonly string suffix; // user-provided suffix to add to filenames that are part of this report
@@ -40,17 +40,17 @@ public class CoverageReport {
  /// Assign a coverage label to the code indicated by the <param name="span"></param> range token.
  /// </summary>
  public void LabelCode(RangeToken span, CoverageLabel label) {
- Contract.Assert(labelsByFile.ContainsKey(span.ActualFilename));
- var labeledFile = labelsByFile[span.ActualFilename];
+ Contract.Assert(labelsByFile.ContainsKey(span.Uri));
+ var labeledFile = labelsByFile[span.Uri];
  var coverageSpan = new CoverageSpan(span, label);
  labeledFile.Add(coverageSpan);
  }
 
- public IEnumerable<CoverageSpan> CoverageSpansForFile(string fileName) {
- return labelsByFile.GetOrDefault(fileName, () => new List<CoverageSpan>());
+ public IEnumerable<CoverageSpan> CoverageSpansForFile(Uri uri) {
+ return labelsByFile.GetOrDefault(uri, () => new List<CoverageSpan>());
  }
 
- public IEnumerable<string> AllFiles() {
+ public IEnumerable<Uri> AllFiles() {
  return labelsByFile.Keys;
  }
 
@@ -59,14 +59,14 @@ public class CoverageReport {
  }
 
  public void RegisterFile(Uri uri) {
- if (!labelsByFile.ContainsKey(uri.LocalPath)) {
- labelsByFile[uri.LocalPath] = new List<CoverageSpan>();
+ if (!labelsByFile.ContainsKey(uri)) {
+ labelsByFile[uri] = new List<CoverageSpan>();
  }
  }
 
  private void RegisterFiles(Node astNode) {
- if (astNode.StartToken.ActualFilename != null && !labelsByFile.ContainsKey(astNode.StartToken.ActualFilename)) {
- labelsByFile[astNode.StartToken.ActualFilename] = new();
+ if (astNode.StartToken.ActualFilename != null && !labelsByFile.ContainsKey(astNode.StartToken.Uri)) {
+ labelsByFile[astNode.StartToken.Uri] = new();
  }
 
  foreach (var declaration in astNode.Children.OfType<LiteralModuleDecl>()) {

Source/DafnyCore/CoverageReport/CoverageSpan.cs

@@ -2,7 +2,7 @@
 using System;
 using System.Diagnostics.Contracts;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public class CoverageSpan : IComparable<CoverageSpan> {
 

Source/DafnyCore/DafnyGeneratedFromDafny.sh

@@ -28,4 +28,4 @@ with open ('$output.cs', 'r' ) as f:
 with open('$output.cs', 'w') as w:
  w.write(content_new)
 "
-dotnet tool run dotnet-format -w --include $output.cs 
+dotnet format whitespace --include $output.cs