Merge branch 'master' into testRemovingAdaptBoxAndResultDescription

.github/workflows/compfuzzci.yaml

@@ -0,0 +1,90 @@
+name: CompFuzzCI
+on:
+  pull_request:
+    branches:
+      - master
+    types: [opened, closed, synchronize, reopened]
+  issues:
+    branches:
+      - master
+    types: [opened, closed, reopened]
+
+jobs:
+  FuzzOnPR:
+    if: github.event_name == 'pull_request' && (github.event.action == 'opened' || github.event.action == 'reopened' || github.event.action == 'synchronize') && github.event.pull_request.base.ref == 'master'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'fuzz.yaml',
+                  ref: 'main',
+                  inputs: {
+                      commit: '${{ github.event.pull_request.head.sha }}',
+                      main_commit: '${{github.event.pull_request.base.sha}}',
+                      branch: '${{github.event.pull_request.head.ref}}',
+                      duration: '3600',
+                      instance: '5'
+                  }
+              })
+  UpdatePRClosed:
+    if: github.event_name == 'pull_request' && github.event.action == 'closed'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_pr_close.yaml',
+                  ref: 'main',
+                  inputs: {
+                      pr_number: '${{github.event.number}}'
+                  }
+              })
+  UpdateIssueOpened:
+    if: github.event_name == 'issues' && (github.event.action == 'opened' || github.event.action == 'reopened')  && github.event.pull_request.base.ref == 'master'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_issue_open.yaml',
+                  ref: 'main',
+                  inputs: {
+                      issue_number: '${{github.event.issue.number}}',
+                      issuer: '${{github.event.issue.user.login}}',
+                      commit: ${{ github.sha }}                
+                  }
+              })
+  UpdateIssueClosed:
+    if: github.event_name == 'issues' && github.event.action == 'closed'
+    runs-on: ubuntu-latest
+    steps:
+      - name: Trigger CompFuzzCI
+        uses: actions/github-script@v7
+        with:
+            github-token: ${{ secrets.COMPFUZZCI_PAT }}
+            script: |
+              await github.rest.actions.createWorkflowDispatch({
+                  owner: 'CompFuzzCI',
+                  repo: 'DafnyCompilerFuzzer',
+                  workflow_id: 'update_issue_close.yaml',
+                  ref: 'main',
+                  inputs: {
+                      issue_number: '${{github.event.issue.number}}'
+                  }
+              })

Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs

@@ -363,7 +363,7 @@ public void PrintStatement(Statement stmt, int indent) {
           wr.Write(" ");
         }
         PrintUpdateRHS(s, indent);
-        wr.Write(";");
+        PrintBy(s);
 
       } else if (stmt is CallStmt) {
         // Most calls are printed from their concrete syntax given in the input. However, recursive calls to
@@ -395,8 +395,7 @@ public void PrintStatement(Statement stmt, int indent) {
           wr.Write(" ");
           PrintUpdateRHS(s.Update, indent);
         }
-        wr.Write(";");
-
+        PrintBy(s.Update);
       } else if (stmt is VarDeclPattern) {
         var s = (VarDeclPattern)stmt;
         if (s.tok is AutoGeneratedToken) {
@@ -455,6 +454,20 @@ public void PrintStatement(Statement stmt, int indent) {
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected statement
       }
+
+      void PrintBy(ConcreteUpdateStatement statement) {
+        BlockStmt proof = statement switch {
+          UpdateStmt updateStmt => updateStmt.Proof,
+          AssignOrReturnStmt returnStmt => returnStmt.Proof,
+          _ => null
+        };
+        if (proof != null) {
+          wr.Write(" by ");
+          PrintStatement(proof, indent);
+        } else {
+          wr.Write(";");
+        }
+      }
     }
 
     private void PrintHideReveal(HideRevealStmt revealStmt) {

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -1,8 +1,11 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.Immutable;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using DafnyCore;
+using DafnyCore.Options;
 using Microsoft.Dafny.Auditor;
 using Microsoft.Dafny.Compilers;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -25,6 +28,18 @@ public enum ImplementationKind {
 public record Implements(ImplementationKind Kind, ModuleQualifiedId Target);
 
 public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable<ModuleDefinition>, IHasSymbolChildren {
+
+  public static readonly Option<bool> LegacyModuleNames = new("--legacy-module-names",
+    @"
+Generate module names in the older A_mB_mC style instead of the current A.B.C scheme".TrimStart()) {
+    IsHidden = true
+  };
+
+  static ModuleDefinition() {
+    DafnyOptions.RegisterLegacyUi(LegacyModuleNames, DafnyOptions.ParseBoolean, "Compilation options", legacyName: "legacyModuleNames", defaultValue: false);
+    OptionRegistry.RegisterOption(LegacyModuleNames, OptionScope.Translation);
+  }
+
   public IToken BodyStartTok = Token.NoToken;
   public IToken TokenWithTrailingDocString = Token.NoToken;
   public string DafnyName => NameNode.StartToken.val; // The (not-qualified) name as seen in Dafny source code
@@ -215,11 +230,15 @@ public string GetCompileName(DafnyOptions options) {
       if (IsBuiltinName) {
         compileName = Name;
       } else if (EnclosingModule is { TryToAvoidName: false }) {
-        // Include all names in the module tree path, to disambiguate when compiling
-        // a flat list of modules.
-        // Use an "underscore-escaped" character as a module name separator, since
-        // underscores are already used as escape characters in SanitizeName()
-        compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name);
+        if (options.Get(LegacyModuleNames)) {
+          compileName = SanitizedName;
+        } else {
+          // Include all names in the module tree path, to disambiguate when compiling
+          // a flat list of modules.
+          // Use an "underscore-escaped" character as a module name separator, since
+          // underscores are already used as escape characters in SanitizeName()
+          compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name);
+        }
       } else {
         compileName = NonglobalVariable.SanitizeName(Name);
       }

Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs

@@ -9,6 +9,7 @@ public class AssignOrReturnStmt : ConcreteUpdateStatement, ICloneable<AssignOrRe
   public readonly ExprRhs Rhs; // this is the unresolved RHS, and thus can also be a method call
   public readonly List<AssignmentRhs> Rhss;
   public readonly AttributedToken KeywordToken;
+  public readonly BlockStmt Proof;
   [FilledInDuringResolution] public readonly List<Statement> ResolvedStatements = new List<Statement>();
   public override IEnumerable<Statement> SubStatements => ResolvedStatements;
   public override IToken Tok {
@@ -22,7 +23,7 @@ public override IToken Tok {
     }
   }
 
-  public override IEnumerable<INode> Children => ResolvedStatements;
+  public override IEnumerable<INode> Children => ResolvedStatements.Concat(Proof?.Children ?? new List<INode>());
   public override IEnumerable<Statement> PreResolveSubStatements => Enumerable.Empty<Statement>();
 
   [ContractInvariantMethod]
@@ -43,13 +44,14 @@ public AssignOrReturnStmt(Cloner cloner, AssignOrReturnStmt original) : base(clo
     Rhs = (ExprRhs)cloner.CloneRHS(original.Rhs);
     Rhss = original.Rhss.ConvertAll(cloner.CloneRHS);
     KeywordToken = cloner.AttributedTok(original.KeywordToken);
+    Proof = cloner.CloneBlockStmt(original.Proof);
 
     if (cloner.CloneResolvedFields) {
       ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
     }
   }
 
-  public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs rhs, AttributedToken keywordToken, List<AssignmentRhs> rhss)
+  public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs rhs, AttributedToken keywordToken, List<AssignmentRhs> rhss, BlockStmt proof = null)
     : base(rangeToken, lhss) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(lhss != null);
@@ -59,6 +61,7 @@ public AssignOrReturnStmt(RangeToken rangeToken, List<Expression> lhss, ExprRhs
     Rhs = rhs;
     Rhss = rhss;
     KeywordToken = keywordToken;
+    Proof = proof;
   }
 
   public override IEnumerable<Expression> PreResolveSubExpressions {
@@ -190,6 +193,8 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
       return;
     }
 
+    ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext);
+
     Expression lhsExtract = null;
     if (expectExtract) {
       if (resolutionContext.CodeContext is Method caller && caller.Outs.Count == 0 && KeywordToken == null) {
@@ -285,7 +290,7 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract,
       }
     }
     // " temp, ... := MethodOrExpression, ...;"
-    UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2);
+    UpdateStmt up = new UpdateStmt(RangeToken, lhss2, rhss2, Proof);
     if (expectExtract) {
       up.OriginalInitialLhs = Lhss.Count == 0 ? null : Lhss[0];
     }

Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs

@@ -8,6 +8,7 @@ public class UpdateStmt : ConcreteUpdateStatement, ICloneable<UpdateStmt>, ICanR
   public readonly List<AssignmentRhs> Rhss;
   public readonly bool CanMutateKnownState;
   public Expression OriginalInitialLhs = null;
+  public readonly BlockStmt Proof;
 
   public override IToken Tok {
     get {
@@ -22,7 +23,7 @@ public override IToken Tok {
   }
 
   [FilledInDuringResolution] public List<Statement> ResolvedStatements;
-  public override IEnumerable<Statement> SubStatements => Children.OfType<Statement>();
+  public override IEnumerable<Statement> SubStatements => Children.OfType<Statement>().Concat(Proof != null ? Proof.SubStatements : new List<Statement>());
 
   public override IEnumerable<Expression> NonSpecificationSubExpressions =>
     ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : Enumerable.Empty<Expression>();
@@ -45,26 +46,29 @@ public UpdateStmt Clone(Cloner cloner) {
   public UpdateStmt(Cloner cloner, UpdateStmt original) : base(cloner, original) {
     Rhss = original.Rhss.Select(cloner.CloneRHS).ToList();
     CanMutateKnownState = original.CanMutateKnownState;
+    Proof = cloner.CloneBlockStmt(original.Proof);
     if (cloner.CloneResolvedFields) {
       ResolvedStatements = original.ResolvedStatements.Select(stmt => cloner.CloneStmt(stmt, false)).ToList();
     }
   }
 
-  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss)
+  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, BlockStmt proof = null)
     : base(rangeToken, lhss) {
     Contract.Requires(cce.NonNullElements(lhss));
     Contract.Requires(cce.NonNullElements(rhss));
     Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
     Rhss = rhss;
     CanMutateKnownState = false;
+    Proof = proof;
   }
-  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate)
+  public UpdateStmt(RangeToken rangeToken, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate, BlockStmt proof = null)
     : base(rangeToken, lhss) {
     Contract.Requires(cce.NonNullElements(lhss));
     Contract.Requires(cce.NonNullElements(rhss));
     Contract.Requires(lhss.Count != 0 || rhss.Count == 1);
     Rhss = rhss;
     CanMutateKnownState = mutate;
+    Proof = proof;
   }
 
   public override IEnumerable<Expression> PreResolveSubExpressions {
@@ -123,6 +127,9 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
       resolver.ResolveAttributes(rhs, resolutionContext);
     }
 
+    // resolve proof
+    ModuleResolver.ResolveByProof(resolver, Proof, resolutionContext);
+
     // figure out what kind of UpdateStmt this is
     if (firstEffectfulRhs == null) {
       if (Lhss.Count == 0) {
@@ -178,7 +185,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
         foreach (var ll in Lhss) {
           resolvedLhss.Add(ll.Resolved);
         }
-        CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok);
+        CallStmt a = new CallStmt(RangeToken, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok, Proof);
         a.OriginalInitialLhs = OriginalInitialLhs;
         ResolvedStatements.Add(a);
       }

Source/DafnyCore/AST/Statements/Methods/CallStmt.cs

@@ -25,11 +25,12 @@ void ObjectInvariant() {
   public readonly ActualBindings Bindings;
   public List<Expression> Args => Bindings.Arguments;
   public Expression OriginalInitialLhs = null;
+  public readonly BlockStmt Proof;
 
   public Expression Receiver { get { return MethodSelect.Obj; } }
   public Method Method { get { return (Method)MethodSelect.Member; } }
 
-  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, IToken overrideToken = null)
+  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, IToken overrideToken = null, BlockStmt proof = null)
     : base(rangeToken) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(cce.NonNullElements(lhs));
@@ -41,6 +42,7 @@ public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr me
     this.MethodSelect = memSel;
     this.overrideToken = overrideToken;
     this.Bindings = new ActualBindings(args);
+    Proof = proof;
   }
 
   public CallStmt Clone(Cloner cloner) {
@@ -52,14 +54,15 @@ public CallStmt(Cloner cloner, CallStmt original) : base(cloner, original) {
     Lhs = original.Lhs.Select(cloner.CloneExpr).ToList();
     Bindings = new ActualBindings(cloner, original.Bindings);
     overrideToken = original.overrideToken;
+    Proof = cloner.CloneBlockStmt(original.Proof);
   }
 
   /// <summary>
   /// This constructor is intended to be used when constructing a resolved CallStmt. The "args" are expected
   /// to be already resolved, and are all given positionally.
   /// </summary>
-  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args)
-    : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e))) {
+  public CallStmt(RangeToken rangeToken, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args, BlockStmt proof = null)
+    : this(rangeToken, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e)), proof: proof) {
     Bindings.AcceptArgumentExpressionsAsExactParameterList();
   }
 

Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs

@@ -89,16 +89,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co
 
     base.GenResolve(resolver, context);
 
-    if (Proof != null) {
-      // clear the labels for the duration of checking the proof body, because break statements are not allowed to leave a the proof body
-      var prevLblStmts = resolver.EnclosingStatementLabels;
-      var prevLoopStack = resolver.LoopStack;
-      resolver.EnclosingStatementLabels = new Scope<Statement>(resolver.Options);
-      resolver.LoopStack = new List<Statement>();
-      resolver.ResolveStatement(Proof, context);
-      resolver.EnclosingStatementLabels = prevLblStmts;
-      resolver.LoopStack = prevLoopStack;
-    }
+    ModuleResolver.ResolveByProof(resolver, Proof, context);
   }
 
   public bool HasAssertOnlyAttribute(out AssertOnlyKind assertOnlyKind) {