dafny-lang · keyboardDrummer · Aug 6, 2020 · Aug 6, 2020 · Aug 6, 2020 · Aug 6, 2020
diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml
@@ -9,6 +9,8 @@ on:
 jobs:
   build:
 
+    env:
+      MSBUILDSINGLELOADCONTEXT: 1 # Workaround for GitVersionTask issue: https://github.com/dotnet/sdk/issues/10878
     runs-on: ${{ matrix.os }}
 
     strategy:
@@ -22,33 +24,30 @@ jobs:
       uses: nuget/setup-nuget@v1
     - name: Manually sync certs
       run: cert-sync /etc/ssl/certs/ca-certificates.crt
-    - name: Add msbuild to PATH
-      if: matrix.os == 'windows-latest'
-      uses: microsoft/setup-msbuild@v1.0.0
-    - name: Checkout Boogie
-      uses: actions/checkout@v2
-      with:
-        repository: boogie-org/boogie
-        ref: v2.4.21
-        path: boogie
-    - name: Nuget Restore Boogie
-      run: nuget restore boogie/Source/Boogie.sln
-    - name: Build Boogie
-      run: msbuild boogie/Source/Boogie.sln
     - name: Checkout Dafny
       uses: actions/checkout@v2
       with:
+        submodules: recursive
         path: dafny
     - name: Get Z3
       if: matrix.os != 'windows-latest'
       run: |
         wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-ubuntu-14.04.zip
         unzip z3*.zip && rm *.zip
         cp -r z3* dafny/Binaries/z3
-    - name: Nuget Restore Dafny
-      run: nuget restore dafny/Source/Dafny.sln
+    - name: Enable Boogie's GitVersionTask dependency to build
+      # GitVersionTask does not work on headless git repositories
+      # GitVersionTask does not work on shallow git repositories
+      run: |
+        git checkout -b gitVersionTaskBranch 
+        git fetch --unshallow 
+      working-directory: dafny/Source/boogie
+    - name: Setup dotnet
+      uses: actions/setup-dotnet@v1
+      with:
+        dotnet-version: '3.1.x' # SDK Version to use; x will use the latest version of the 3.1 channel
     - name: Build Dafny
-      run: msbuild dafny/Source/Dafny.sln
+      run: dotnet build dafny/Source/Dafny.sln
     - uses: actions/setup-python@v1
     - name: Upgrade outdated pip
       run: python -m pip install --upgrade pip

diff --git a/.gitignore b/.gitignore
@@ -21,6 +21,7 @@ Binaries/DafnyServer.exe
 Binaries/DafnyRuntime.cs
 Binaries/export/
 Binaries/mono_crash*
+Binaries/*
 
 Package/
 

diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "Source/boogie"]
+	path = Source/boogie
+	url = https://github.com/boogie-org/boogie.git
diff --git a/Source/Dafny.sln b/Source/Dafny.sln
diff --git a/Source/Dafny/Compiler-Csharp.cs b/Source/Dafny/Compiler-Csharp.cs
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
@@ -10,7 +10,6 @@
 using Bpl = Microsoft.Boogie;
 using System.Reflection;
 using DafnyAssembly;
-using Mono.Cecil;
 
 namespace Microsoft.Dafny {
 
@@ -37,17 +36,20 @@ public DafnyFile(string filePath) {
       var extension = Path.GetExtension(filePath);
       if (extension != null) { extension = extension.ToLower(); }
 
+      if (!Path.IsPathRooted(filePath))
+        filePath = Path.GetFullPath(filePath);
+
       if (extension == ".dfy" || extension == ".dfyi") {
         isPrecompiled = false;
         SourceFileName = filePath;
       } else if (extension == ".dll") {
         isPrecompiled = true;
-        var asm = AssemblyDefinition.ReadAssembly(filePath);
+        var asm = Assembly.LoadFile(filePath);
         string sourceText = null;
         foreach (var adata in asm.CustomAttributes) {
           if (adata.Constructor.DeclaringType.Name == "DafnySourceAttribute") {
             foreach (var args in adata.ConstructorArguments) {
-              if (args.Type.FullName == "System.String") {
+              if (args.ArgumentType.FullName == "System.String") {
                 sourceText = (string)args.Value;
               }
             }

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
@@ -1,222 +1,26 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
-  <PropertyGroup>
-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
-    <ProductVersion>9.0.30729</ProductVersion>
-    <SchemaVersion>2.0</SchemaVersion>
-    <ProjectGuid>{FE44674A-1633-4917-99F4-57635E6FA740}</ProjectGuid>
-    <OutputType>Library</OutputType>
-    <AppDesignerFolder>Properties</AppDesignerFolder>
-    <RootNamespace>Microsoft.Dafny</RootNamespace>
-    <AssemblyName>DafnyPipeline</AssemblyName>
-    <TargetFrameworkVersion>v4.8</TargetFrameworkVersion>
-    <FileAlignment>512</FileAlignment>
-    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
-    <SignAssembly>true</SignAssembly>
-    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
-    <FileUpgradeFlags>
-    </FileUpgradeFlags>
-    <OldToolsVersion>3.5</OldToolsVersion>
-    <UpgradeBackupLocation />
-    <PublishUrl>publish\</PublishUrl>
-    <Install>true</Install>
-    <InstallFrom>Disk</InstallFrom>
-    <UpdateEnabled>false</UpdateEnabled>
-    <UpdateMode>Foreground</UpdateMode>
-    <UpdateInterval>7</UpdateInterval>
-    <UpdateIntervalUnits>Days</UpdateIntervalUnits>
-    <UpdatePeriodically>false</UpdatePeriodically>
-    <UpdateRequired>false</UpdateRequired>
-    <MapFileExtensions>true</MapFileExtensions>
-    <ApplicationRevision>0</ApplicationRevision>
-    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
-    <IsWebBootstrapper>false</IsWebBootstrapper>
-    <UseApplicationTrust>false</UseApplicationTrust>
-    <BootstrapperEnabled>true</BootstrapperEnabled>
-    <TargetFrameworkProfile>
-    </TargetFrameworkProfile>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
-    <DebugSymbols>true</DebugSymbols>
-    <DebugType>full</DebugType>
-    <Optimize>false</Optimize>
-    <OutputPath>bin\Debug\</OutputPath>
-    <DefineConstants>TRACE;DEBUG;NO_ENABLE_IRONDAFNY</DefineConstants>
-    <ErrorReport>prompt</ErrorReport>
-    <WarningLevel>4</WarningLevel>
-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
-    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
-    <CodeContractsCustomRewriterAssembly>
-    </CodeContractsCustomRewriterAssembly>
-    <CodeContractsCustomRewriterClass>
-    </CodeContractsCustomRewriterClass>
-    <CodeContractsLibPaths>
-    </CodeContractsLibPaths>
-    <CodeContractsExtraRewriteOptions>
-    </CodeContractsExtraRewriteOptions>
-    <CodeContractsExtraAnalysisOptions>
-    </CodeContractsExtraAnalysisOptions>
-    <CodeContractsBaseLineFile>
-    </CodeContractsBaseLineFile>
-    <CodeContractsRuntimeCheckingLevel>None</CodeContractsRuntimeCheckingLevel>
-    <CodeContractsReferenceAssembly>DoNotBuild</CodeContractsReferenceAssembly>
-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
-    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
-    <Prefer32Bit>false</Prefer32Bit>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
-    <DebugType>pdbonly</DebugType>
-    <Optimize>true</Optimize>
-    <OutputPath>bin\Release\</OutputPath>
-    <DefineConstants>TRACE;NO_ENABLE_IRONDAFNY</DefineConstants>
-    <ErrorReport>prompt</ErrorReport>
-    <WarningLevel>4</WarningLevel>
-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
-    <Prefer32Bit>false</Prefer32Bit>
-  </PropertyGroup>
-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
-    <DebugSymbols>true</DebugSymbols>
-    <OutputPath>bin\Checked\</OutputPath>
-    <DefineConstants>TRACE;DEBUG;NO_ENABLE_IRONDAFNY</DefineConstants>
-    <DebugType>full</DebugType>
-    <PlatformTarget>AnyCPU</PlatformTarget>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
-    <CodeContractsCustomRewriterAssembly />
-    <CodeContractsCustomRewriterClass />
-    <CodeContractsLibPaths />
-    <CodeContractsExtraRewriteOptions />
-    <CodeContractsExtraAnalysisOptions />
-    <CodeContractsBaseLineFile />
-    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
-    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
-    <Prefer32Bit>false</Prefer32Bit>
-  </PropertyGroup>
-  <ItemGroup>
-    <Reference Include="BoogieBasetypes">
-      <HintPath>..\..\..\boogie\Binaries\BoogieBasetypes.dll</HintPath>
-    </Reference>
-    <Reference Include="BoogieCore">
-      <HintPath>..\..\..\boogie\Binaries\BoogieCore.dll</HintPath>
-    </Reference>
-    <Reference Include="BoogieParserHelper">
-      <HintPath>..\..\..\boogie\Binaries\BoogieParserHelper.dll</HintPath>
-    </Reference>
-    <PackageReference Include="Mono.Cecil" Version="0.11.2" />
-    <Reference Include="System" />
-    <Reference Include="System.Core">
-      <RequiredTargetFramework>4.8</RequiredTargetFramework>
-    </Reference>
-    <Reference Include="System.Numerics" />
-  </ItemGroup>
-  <ItemGroup>
-    <Compile Include="Cloner.cs" />
-    <Compile Include="Compiler-Csharp.cs" />
-    <Compile Include="Compiler-go.cs" />
-    <Compile Include="Compiler-js.cs" />
-    <Compile Include="Compiler-cpp.cs" />
-    <Compile Include="Compiler-java.cs" />
-    <Compile Include="Reporting.cs" />
-    <Compile Include="Triggers\QuantifiersCollection.cs" />
-    <Compile Include="Triggers\QuantifierSplitter.cs" />
-    <Compile Include="Triggers\TriggerExtensions.cs" />
-    <Compile Include="Triggers\QuantifiersCollector.cs" />
-    <Compile Include="Triggers\TriggersCollector.cs" />
-    <Compile Include="Triggers\TriggerUtils.cs" />
-    <Compile Include="Util.cs" />
-    <Compile Include="Compiler.cs" />
-    <Compile Include="BigIntegerParser.cs" />
-    <Compile Include="DafnyAst.cs" />
-    <Compile Include="DafnyMain.cs" />
-    <Compile Include="DafnyOptions.cs" />
-    <Compile Include="Printer.cs" />
-    <Compile Include="RefinementTransformer.cs" />
-    <Compile Include="Resolver.cs" />
-    <Compile Include="Rewriter.cs" />
-    <Compile Include="SccGraph.cs" />
-    <Compile Include="Translator.cs" />
-    <Compile Include="..\version.cs" />
-  </ItemGroup>
-  <ItemGroup>
-    <Compile Include="cce.cs" />
-  </ItemGroup>
-  <ItemGroup>
-    <None Include="Dafny.atg" />
-  </ItemGroup>
-  <ItemGroup>
-    <Compile Include="Parser.cs" Visible="False" />
-    <Compile Include="Scanner.cs" Visible="False" />
-  </ItemGroup>
-  <ItemGroup>
-    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
-      <Visible>False</Visible>
-      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
-      <Install>false</Install>
-    </BootstrapperPackage>
-    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
-      <Visible>False</Visible>
-      <ProductName>.NET Framework 3.5 SP1</ProductName>
-      <Install>true</Install>
-    </BootstrapperPackage>
-    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
-      <Visible>False</Visible>
-      <ProductName>Windows Installer 3.1</ProductName>
-      <Install>true</Install>
-    </BootstrapperPackage>
-  </ItemGroup>
-  <ItemGroup>
-    <ProjectReference Include="..\DafnyRuntime\DafnyRuntime.csproj">
-      <Project>{3e2944e9-3e1d-4e03-a881-fb04a7a6ed67}</Project>
-      <Name>DafnyRuntime</Name>
-    </ProjectReference>
-  </ItemGroup>
-  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
-  <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
-       Other similar extension points exist, see Microsoft.Common.targets.
-  <Target Name="BeforeBuild">
-  </Target>
-  <Target Name="AfterBuild">
-  </Target>
-  -->
-  <PropertyGroup>
-    <CodeContractsInstallDir Condition="'$(CodeContractsInstallDir)'==''">C:\Program Files (x86)\Microsoft\Contracts\</CodeContractsInstallDir>
-  </PropertyGroup>
-  <Import Condition="'$(CodeContractsImported)' != 'true' AND '$(DontImportCodeContracts)' != 'true' AND Exists($(CodeContractsInstallDir))" Project="$(CodeContractsInstallDir)MsBuild\v14.0\Microsoft.CodeContracts.targets" />
+<Project Sdk="Microsoft.NET.Sdk">
+
+    <PropertyGroup>
+        <OutputType>Library</OutputType>
+        <AssemblyName>DafnyPipeline</AssemblyName>
+        <TargetFrameworks>netcoreapp3.1</TargetFrameworks>
+        <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
+        <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
+        <DefineConstants>TRACE</DefineConstants>
+        <PackageVersion>1.1.0</PackageVersion>
+    </PropertyGroup>
+
+    <ItemGroup>
+      <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
+      <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
+      <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
+    </ItemGroup>
+
+    <ItemGroup>
+      <ProjectReference Include="..\boogie\Source\Basetypes\Basetypes-NetCore.csproj" />
+      <ProjectReference Include="..\boogie\Source\Core\Core-NetCore.csproj" />
+      <ProjectReference Include="..\boogie\Source\ParserHelper\ParserHelper-NetCore.csproj" />
+      <ProjectReference Include="..\DafnyRuntime\DafnyRuntime.csproj" />
+    </ItemGroup>
+
 </Project>
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
@@ -7605,7 +7605,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu
 
           // Cannot use the datatype's formals, so we substitute the inferred type args:
           var su = new Dictionary<TypeParameter, Type>();
-          foreach (var p in dtv.Ctor.EnclosingDatatype.TypeArgs.Zip(dtv.InferredTypeArgs)) {
+          foreach (var p in LinqExtender.Zip(dtv.Ctor.EnclosingDatatype.TypeArgs, dtv.InferredTypeArgs)) {
             su[p.Item1] = p.Item2;
           }
           Type ty = Resolver.SubstType(formal.Type, su);
@@ -17549,11 +17549,11 @@ bool TrSplitExpr(Expression expr, List<SplitExprInfo/*!*/>/*!*/ splits, bool pos
     private bool CanSafelyInline(FunctionCallExpr fexp, Function f) {
       var visitor = new TriggersExplorer();
       visitor.Visit(f);
-      return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));
+      return LinqExtender.Zip(f.Formals, fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2));
     }
 
     // Using an empty set of old expressions is ok here; the only uses of the triggersCollector will be to check for trigger killers.
-    Triggers.TriggersCollector triggersCollector = new Triggers.TriggersCollector(new Dictionary<Expression, HashSet<OldExpr>>());
+    Triggers.TriggersCollector triggersCollector = new  Triggers.TriggersCollector(new Dictionary<Expression, HashSet<OldExpr>>());
 
     private bool CanSafelySubstitute(ISet<IVariable> protectedVariables, IVariable variable, Expression substitution) {
       return !(protectedVariables.Contains(variable) && triggersCollector.IsTriggerKiller(substitution));

diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs
@@ -89,7 +89,7 @@ public static List<A> Concat<A>(List<A> xs, List<A> ys) {
     }
 
     public static Dictionary<A,B> Dict<A,B>(IEnumerable<A> xs, IEnumerable<B> ys) {
-      return Dict<A,B>(xs.Zip(ys));
+      return Dict<A,B>(LinqExtender.Zip(xs, ys));
     }
 
     public static Dictionary<A,B> Dict<A,B>(IEnumerable<Tuple<A,B>> xys) {