Merge branch 'master' into typerSniper-remove-preconditions-from-axioms

RustanLeino · Nov 20, 2021 · 5060983 · 5060983
2 parents a45dda4 + 6a39d5c
commit 5060983
Show file tree

Hide file tree

Showing 87 changed files with 3,082 additions and 991 deletions.
diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml
@@ -53,7 +53,6 @@ jobs:
 
   build:
     runs-on: ${{ matrix.os }}
-
     strategy:
       matrix:
         ## Windows jobs fail on some lit tests and sometimes fail even to
@@ -126,4 +125,9 @@ jobs:
         unzip dafny/Package/CI.zip -d unzippedRelease
     - name: Run integration tests
       run: |
-        XUNIT_SHARD=${{ matrix.shard }} XUNIT_SHARD_COUNT=5 DAFNY_RELEASE=$PWD/unzippedRelease/dafny dotnet test -v:n dafny/Source/IntegrationTests/IntegrationTests.csproj
+        XUNIT_SHARD=${{ matrix.shard }} XUNIT_SHARD_COUNT=5 DAFNY_RELEASE=$PWD/unzippedRelease/dafny dotnet test -v:n --logger trx dafny/Source/IntegrationTests/IntegrationTests.csproj
+    - uses: actions/upload-artifact@v2
+      if: always()
+      with:
+        name: integration-test-results-${{ matrix.os }}
+        path: dafny/Source/IntegrationTests/TestResults/*.trx
diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml
@@ -5,6 +5,7 @@ name: Test Release Downloads
 on:
   release:
     types: [ published ]
+  workflow_dispatch: // For manual testing through the Actions UI
 
 jobs:
   build:
@@ -16,14 +17,14 @@ jobs:
         os: [ ubuntu-latest, ubuntu-18.04, macos-latest, windows-latest ]
         include:
         - os:  'ubuntu-latest'
-          osn: 'ubuntu-18.04'
+          osn: 'ubuntu-16.04'
         - os:  'ubuntu-18.04'
-          osn: 'ubuntu-18.04'
+          osn: 'ubuntu-16.04'
         - os:  'macos-latest'
           osn: 'osx'
         - os:  'windows-latest'
           osn: 'win'
-          ver: '3.2.0'
+          ver: '3.3.0'
     # There is no hosted environment for Unbuntu 14.04 or for debian
 
     # Java is installed by default, but we need to select 1.8

diff --git a/.github/workflows/test-report.yml b/.github/workflows/test-report.yml
@@ -0,0 +1,29 @@
+name: 'Test Report'
+on:
+  workflow_run:
+    workflows: ['Run XUnit tests', 'Build and Test']
+    types:
+      - completed
+jobs:
+  report:
+    name: "Download and Publish Test Results"
+    needs: build
+    runs-on: ubuntu-latest
+    if: always()
+
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Download Artifacts
+        uses: actions/download-artifact@v2
+        with:
+          path: artifacts
+
+      - name: Publish Test Results
+        uses: dorny/test-reporter@v1
+        with:
+          name: Test Results
+          path: 'artifacts/**/*.trx'
+          reporter: dotnet-trx
diff --git a/.github/workflows/xunit-tests.yml b/.github/workflows/xunit-tests.yml
@@ -56,8 +56,13 @@ jobs:
     - name: Build
       run: dotnet build --no-restore ${{env.solutionPath}}
     - name: Run DafnyLanguageServer Tests
-      run: dotnet test --no-restore --verbosity normal Source/DafnyLanguageServer.Test
+      run: dotnet test --no-restore --verbosity normal --logger trx Source/DafnyLanguageServer.Test
     - name: Run DafnyPipeline Tests
-      run: dotnet test --no-restore --verbosity normal Source/DafnyPipeline.Test
+      run: dotnet test --no-restore --verbosity normal --logger trx Source/DafnyPipeline.Test
     - name: Run DafnyTestGeneration Tests
-      run: dotnet test --no-restore --verbosity normal Source/DafnyTestGeneration.Test
+      run: dotnet test --no-restore --verbosity normal --logger trx Source/DafnyTestGeneration.Test
+    - uses: actions/upload-artifact@v2
+      if: always()
+      with:
+        name: unit-test-results-${{ matrix.os }}
+        path: Source/*/TestResults/*.trx
diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs
@@ -4276,6 +4276,8 @@ public virtual List<Type> ParentTypes(List<Type> typeArgs) {
       Contract.Requires(this.TypeArgs.Count == typeArgs.Count);
       return new List<Type>();
     }
+
+    public bool AllowsAllocation => true;
   }
 
   public abstract class TopLevelDeclWithMembers : TopLevelDecl {
@@ -4850,6 +4852,7 @@ public interface ICallable : ICodeContext {
     /// the property will get the value "true".  This is so that a useful error message can be provided.
     /// </summary>
     bool InferredDecreases { get; set; }
+    bool AllowsAllocation { get; }
   }
 
   /// <summary>
@@ -4873,6 +4876,8 @@ public bool InferredDecreases {
       get => cwInner.InferredDecreases;
       set { cwInner.InferredDecreases = value; }
     }
+
+    public bool AllowsAllocation => cwInner.AllowsAllocation;
   }
 
   public class DontUseICallable : ICallable {
@@ -4891,6 +4896,7 @@ public bool InferredDecreases {
       get { throw new cce.UnreachableException(); }
       set { throw new cce.UnreachableException(); }
     }
+    public bool AllowsAllocation => throw new cce.UnreachableException();
   }
   /// <summary>
   /// An IMethodCodeContext is a Method or IteratorDecl.
@@ -4916,6 +4922,7 @@ public NoContext(ModuleDefinition module) {
     bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
     public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
     public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
+    public bool AllowsAllocation => true;
   }
 
   public class IteratorDecl : ClassDecl, IMethodCodeContext {
@@ -5403,6 +5410,7 @@ public bool InferredDecreases {
       get { throw new cce.UnreachableException(); }
       set { throw new cce.UnreachableException(); }
     }
+    public bool AllowsAllocation => true;
   }
 
   public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl {
@@ -6147,6 +6155,7 @@ public class Function : MemberDecl, TypeParameter.ParentType, ICallable {
     public Function OverriddenFunction;
     public Function Original => OverriddenFunction == null ? this : OverriddenFunction.Original;
     public override bool IsOverrideThatAddsBody => base.IsOverrideThatAddsBody && Body != null;
+    public bool AllowsAllocation => true;
 
     public bool containsQuantifier;
     public bool ContainsQuantifier {
@@ -6561,6 +6570,8 @@ bool ICallable.InferredDecreases {
       get { return _inferredDecr; }
     }
 
+    public virtual bool AllowsAllocation => true;
+
     ModuleDefinition ICodeContext.EnclosingModule {
       get {
         Contract.Assert(this.EnclosingClass != null);  // this getter is supposed to be called only after signature-resolution is complete
@@ -6590,7 +6601,7 @@ public BlockStmt Body {
       get {
         // Lemma from included files do not need to be resolved and translated
         // so we return emptyBody. This is to speed up resolvor and translator.
-        if (methodBody != null && (this is Lemma || this is TwoStateLemma) && this.tok is IncludeToken && !DafnyOptions.O.VerifyAllModules) {
+        if (methodBody != null && IsLemmaLike && this.tok is IncludeToken && !DafnyOptions.O.VerifyAllModules) {
           return Method.emptyBody;
         } else {
           return methodBody;
@@ -6601,6 +6612,8 @@ public BlockStmt Body {
       }
     }
 
+    public bool IsLemmaLike => this is Lemma || this is TwoStateLemma || this is ExtremeLemma || this is PrefixLemma;
+
     public BlockStmt BodyForRefinement {
       // For refinement, we still need to merge in the body
       // a lemma that is in the refinement base that is defined
@@ -6624,6 +6637,8 @@ public Lemma(IToken tok, string name,
                  Attributes attributes, IToken signatureEllipsis)
       : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
     }
+
+    public override bool AllowsAllocation => false;
   }
 
   public class TwoStateLemma : Method {
@@ -6649,6 +6664,8 @@ public TwoStateLemma(IToken tok, string name,
       Contract.Requires(ens != null);
       Contract.Requires(decreases != null);
     }
+
+    public override bool AllowsAllocation => false;
   }
 
   public class Constructor : Method {
@@ -6676,14 +6693,15 @@ public List<Statement> BodyProper {  // second part of Body's statements
       }
     }
     public Constructor(IToken tok, string name,
+                  bool isGhost,
                   List<TypeParameter> typeArgs,
                   List<Formal> ins,
                   List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
                   List<AttributedExpression> ens,
                   Specification<Expression> decreases,
                   DividedBlockStmt body,
                   Attributes attributes, IToken signatureEllipsis)
-      : base(tok, name, false, false, typeArgs, ins, new List<Formal>(), req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+      : base(tok, name, false, isGhost, typeArgs, ins, new List<Formal>(), req, mod, ens, decreases, body, attributes, signatureEllipsis) {
       Contract.Requires(tok != null);
       Contract.Requires(name != null);
       Contract.Requires(cce.NonNullElements(typeArgs));
@@ -6719,6 +6737,8 @@ public PrefixLemma(IToken tok, string name, bool hasStaticKeyword,
       K = k;
       ExtremeLemma = extremeLemma;
     }
+
+    public override bool AllowsAllocation => false;
   }
 
   public abstract class ExtremeLemma : Method {
@@ -6751,6 +6771,8 @@ public ExtremeLemma(IToken tok, string name,
       Contract.Requires(decreases != null);
       TypeOfK = typeOfK;
     }
+
+    public override bool AllowsAllocation => false;
   }
 
   public class LeastLemma : ExtremeLemma {

diff --git a/Source/Dafny/AST/Printer.cs b/Source/Dafny/AST/Printer.cs
@@ -933,7 +933,7 @@ public void PrintMethod(Method method, int indent, bool printSignatureOnly) {
         method is TwoStateLemma ? "twostate lemma" :
         "method";
       if (method.HasStaticKeyword) { k = "static " + k; }
-      if (method.IsGhost && !(method is Lemma) && !(method is PrefixLemma) && !(method is TwoStateLemma) && !(method is ExtremeLemma)) {
+      if (method.IsGhost && !method.IsLemmaLike) {
         k = "ghost " + k;
       }
       string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name;

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
@@ -798,7 +798,7 @@ public virtual Method CloneMethod(Method m) {
       BlockStmt body = CloneMethodBody(m);
 
       if (m is Constructor) {
-        return new Constructor(Tok(m.tok), m.Name, tps, ins,
+        return new Constructor(Tok(m.tok), m.Name, m.IsGhost, tps, ins,
           req, mod, ens, decreases, (DividedBlockStmt)body, CloneAttributes(m.Attributes), null);
       } else if (m is LeastLemma) {
         return new LeastLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, ((LeastLemma)m).TypeOfK, tps, ins, m.Outs.ConvertAll(CloneFormal),

diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs
@@ -2364,7 +2364,7 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod
 
     // ----- Target compilation and execution -------------------------------------------------------------
     private string ComputeExeName(string targetFilename) {
-      return Path.GetFileNameWithoutExtension(targetFilename) + ".exe";
+      return Path.ChangeExtension(Path.GetFullPath(targetFilename), "exe");
     }
 
     public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string/*?*/ targetFilename, ReadOnlyCollection<string> otherFileNames,
@@ -2373,15 +2373,14 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
       Contract.Assert(assemblyLocation != null);
       var codebase = System.IO.Path.GetDirectoryName(assemblyLocation);
       Contract.Assert(codebase != null);
-      var exeName = ComputeExeName(targetFilename);
       var warnings = "-Wall -Wextra -Wpedantic -Wno-unused-variable -Wno-deprecated-copy";
       if (!RuntimeInformation.IsOSPlatform(OSPlatform.Linux)) {
         warnings += " -Wno-unknown-warning-option";
       }
       if (RuntimeInformation.IsOSPlatform(OSPlatform.Linux)) {
         warnings += " -Wno-unused-but-set-variable";
       }
-      var args = warnings + $" -g -std=c++17 -I {codebase} -o {exeName} {targetFilename}";
+      var args = warnings + $" -g -std=c++17 -I {codebase} -o {ComputeExeName(targetFilename)} {targetFilename}";
       compilationResult = null;
       var psi = new ProcessStartInfo("g++", args) {
         CreateNoWindow = true,
@@ -2406,8 +2405,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
 
     public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection<string> otherFileNames,
       object compilationResult, TextWriter outputWriter) {
-      var exeName = ComputeExeName(targetFilename);
-      var psi = new ProcessStartInfo(exeName) {
+      var psi = new ProcessStartInfo(ComputeExeName(targetFilename)) {
         CreateNoWindow = true,
         UseShellExecute = false,
         RedirectStandardOutput = true,

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
@@ -1713,7 +1713,7 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
                                          SemErr(t, "constructors are allowed only in classes");
                                        }
                                        caption = "constructor";
-                                       allowed = AllowedDeclModifiers.None;
+                                       allowed = AllowedDeclModifiers.Ghost;
                                     .)
   )                                 (. keywordToken = t;
                                        CheckDeclModifiers(dmod, caption, allowed); .)
@@ -1731,7 +1731,7 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
     [ GenericParameters<typeArgs, false> ]
     [ KType<ref kType>              (. if (!(isGreatestLemma || isLeastLemma)) { SemErr(t, "type of _k can only be specified for least and greatest lemmas"); } .)
     ]
-    (. var isCompilable = (isPlainOlMethod && !dmod.IsGhost) || isConstructor; .)
+    (. var isCompilable = (isPlainOlMethod || isConstructor) && !dmod.IsGhost; .)
     Formals<true, isCompilable, isTwoStateLemma, ins>
     [ "returns"                                 (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
       Formals<false, isCompilable, false, outs>
@@ -1748,7 +1748,7 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
   ]
   (. IToken tok = id;
      if (isConstructor) {
-       m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,
+       m = new Constructor(tok, hasName ? id.val : "_ctor", dmod.IsGhost, typeArgs, ins,
                            req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), (DividedBlockStmt)body, attrs, signatureEllipsis);
      } else if (isLeastLemma) {
        m = new LeastLemma(tok, id.val, dmod.IsStatic, kType, typeArgs, ins, outs,