Isolate paths (dafny-lang#5832)

Requires Boogie boogie-org/boogie#970

### Changes
- Allows using `{:isolate "paths"}` on `assert`, `return` and `continue`
statements.

### Out of scope
- `{:isolate "paths"}` for implicit assertions
- Custom syntax for {:isolate}, possibly in combination with "by
clauses"

### Testing
- Added the CLI test `isolatePaths.dfy`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Source/DafnyCore/AST/Statements/ControlFlow/BreakStmt.cs

@@ -31,8 +31,8 @@ public BreakStmt(Cloner cloner, BreakStmt original) : base(cloner, original) {
     }
   }
 
-  public BreakStmt(RangeToken rangeToken, IToken targetLabel, bool isContinue)
-    : base(rangeToken) {
+  public BreakStmt(RangeToken rangeToken, IToken targetLabel, bool isContinue, Attributes attributes = null)
+    : base(rangeToken, attributes) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(targetLabel != null);
     this.TargetLabel = targetLabel;
@@ -43,8 +43,8 @@ public BreakStmt(RangeToken rangeToken, IToken targetLabel, bool isContinue)
   /// For "isContinue == false", represents the statement "break ^breakAndContinueCount ;".
   /// For "isContinue == true", represents the statement "break ^(breakAndContinueCount - 1) continue;".
   /// </summary>
-  public BreakStmt(RangeToken rangeToken, int breakAndContinueCount, bool isContinue)
-    : base(rangeToken) {
+  public BreakStmt(RangeToken rangeToken, int breakAndContinueCount, bool isContinue, Attributes attributes = null)
+    : base(rangeToken, attributes) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(1 <= breakAndContinueCount);
     this.BreakAndContinueCount = breakAndContinueCount;

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

@@ -19,8 +19,8 @@ protected ProduceStmt(Cloner cloner, ProduceStmt original) : base(cloner, origin
     }
   }
 
-  public ProduceStmt(RangeToken rangeToken, List<AssignmentRhs> rhss)
-    : base(rangeToken) {
+  protected ProduceStmt(RangeToken rangeToken, List<AssignmentRhs> rhss, Attributes attributes)
+    : base(rangeToken, attributes) {
     this.Rhss = rhss;
     HiddenUpdate = null;
   }

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

@@ -14,8 +14,8 @@ public ReturnStmt(Cloner cloner, ReturnStmt original) : base(cloner, original) {
     ReverifyPost = original.ReverifyPost;
   }
 
-  public ReturnStmt(RangeToken rangeToken, List<AssignmentRhs> rhss)
-    : base(rangeToken, rhss) {
+  public ReturnStmt(RangeToken rangeToken, List<AssignmentRhs> rhss, Attributes attributes = null)
+    : base(rangeToken, rhss, attributes) {
     Contract.Requires(rangeToken != null);
   }
 }

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

@@ -11,7 +11,7 @@ public YieldStmt(Cloner cloner, YieldStmt original) : base(cloner, original) {
   }
 
   public YieldStmt(RangeToken rangeToken, List<AssignmentRhs> rhss)
-    : base(rangeToken, rhss) {
+    : base(rangeToken, rhss, null) {
   }
 
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {

Source/DafnyCore/AST/Statements/Statement.cs

@@ -12,15 +12,7 @@ public abstract class Statement : RangeNode, IAttributeBearingDeclaration {
   public int ScopeDepth { get; set; }
   public LList<Label> Labels;  // mutable during resolution
 
-  private Attributes attributes;
-  public Attributes Attributes {
-    get {
-      return attributes;
-    }
-    set {
-      attributes = value;
-    }
-  }
+  public Attributes Attributes { get; set; }
   string IAttributeBearingDeclaration.WhatKind => "statement";
 
   [ContractInvariantMethod]
@@ -36,7 +28,7 @@ public virtual void GenResolve(INewOrOldResolver resolver, ResolutionContext res
 
   protected Statement(Cloner cloner, Statement original) : base(cloner.Tok(original.RangeToken)) {
     cloner.AddStatementClone(original, this);
-    this.attributes = cloner.CloneAttributes(original.Attributes);
+    this.Attributes = cloner.CloneAttributes(original.Attributes);
 
     if (cloner.CloneResolvedFields) {
       IsGhost = original.IsGhost;
@@ -45,7 +37,7 @@ protected Statement(Cloner cloner, Statement original) : base(cloner.Tok(origina
   }
 
   protected Statement(RangeToken rangeToken, Attributes attrs) : base(rangeToken) {
-    this.attributes = attrs;
+    this.Attributes = attrs;
   }
 
   protected Statement(RangeToken rangeToken)

Source/DafnyCore/AST/Tokens.cs

@@ -1,6 +1,5 @@
 
 using System;
-using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Text;
@@ -160,6 +159,7 @@ public Uri Uri {
   public bool IsValid {
     get { return WrappedToken.IsValid; }
   }
+
   public int kind {
     get { return WrappedToken.kind; }
     set { WrappedToken.kind = value; }

Source/DafnyCore/CompileNestedMatch/MatchAst.cs

@@ -107,7 +107,7 @@ public IEnumerable<IHasNavigationToken> GetReferences() {
   }
 }
 
-interface IMatch {
+public interface IMatch {
   IEnumerable<MatchCase> Cases { get; }
   Expression Source { get; }
   List<DatatypeCtor> MissingCases { get; }

Source/DafnyCore/Dafny.atg

@@ -2264,8 +2264,10 @@ BreakStmt<out Statement/*!*/ s>
      IToken start = Token.NoToken;
      IToken label = null;
      int breakAndContinueCount = 1;
+     Attributes attributes = null;
   .)
   ( "continue"              (. start = t; isContinue = true; .)
+    [ Attribute<ref attributes> ]
     [ LabelName<out label> ]
   | "break"                 (. start = t; .)
     ( LabelName<out label>
@@ -2280,7 +2282,7 @@ BreakStmt<out Statement/*!*/ s>
   (. Contract.Assert(label == null || breakAndContinueCount == 1);
      s = label != null ?
        new BreakStmt(new RangeToken(start, t), label, isContinue) :
-       new BreakStmt(new RangeToken(start, t), breakAndContinueCount, isContinue);
+       new BreakStmt(new RangeToken(start, t), breakAndContinueCount, isContinue, attributes);
   .)
   .
 
@@ -2291,14 +2293,16 @@ ReturnStmt<out Statement/*!*/ s>
          IToken returnTok = t;
          List<AssignmentRhs> rhss = null;
          AssignmentRhs r;
+         Attributes attributes = null;
        .)
+  [ Attribute<ref attributes> ]
   [ Rhs<out r>                       (. rhss = new List<AssignmentRhs>();
                                         rhss.Add(r);
                                      .)
     { "," Rhs<out r>                 (. rhss.Add(r); .)
     }
   ]
-  ";"                                (. s = new ReturnStmt(new RangeToken(returnTok, t), rhss);
+  ";"                                (. s = new ReturnStmt(new RangeToken(returnTok, t), rhss, attributes);
                                      .)
   .
 

Source/DafnyCore/DafnyCore.csproj

@@ -34,7 +34,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.3.3" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.4.1" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyCore/Options/BoogieOptionBag.cs

@@ -142,7 +142,6 @@ static BoogieOptionBag() {
     DafnyOptions.RegisterLegacyBinding(VerificationErrorLimit, (options, value) => { options.ErrorLimit = value; });
     DafnyOptions.RegisterLegacyBinding(IsolateAssertions, (o, v) => o.VcsSplitOnEveryAssert = v);
 
-
     OptionRegistry.RegisterGlobalOption(BoogieArguments, OptionCompatibility.CheckOptionMatches);
     OptionRegistry.RegisterGlobalOption(NoVerify, OptionCompatibility.OptionLibraryImpliesLocalError);
     OptionRegistry.RegisterOption(HiddenNoVerify, OptionScope.Cli);

Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs

@@ -893,6 +893,8 @@ public static IToken ToDafnyToken(bool reportRanges, Bpl.IToken boogieToken) {
         return null;
       } else if (boogieToken is IToken dafnyToken) {
         return dafnyToken;
+      } else if (boogieToken is VCGeneration.TokenWrapper tokenWrapper) {
+        return ToDafnyToken(reportRanges, tokenWrapper.Inner);
       } else if (boogieToken == Boogie.Token.NoToken) {
         return Token.NoToken;
       } else {

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -1939,6 +1939,7 @@ public static bool RewriteInExpr(Expression s, bool aggressive) {
 
       private static readonly HashSet<string> NullaryAttributesToCopy = new(new[] {
         "focus",
+        "isolate",
         "ignore",
         "selective_checking",
         "split",
@@ -1965,6 +1966,7 @@ public static bool RewriteInExpr(Expression s, bool aggressive) {
 
       private static readonly HashSet<string> StringAttributesToCopy = new(new[] {
         "captureState",
+        "isolate",
         "error"
       });
 
@@ -1999,7 +2001,7 @@ private QKeyValue TrStringAttribute(string name, Expression arg, QKeyValue rest)
           : rest;
       }
 
-      public QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute) {
+      public QKeyValue TrAttributes(Attributes attrs, string skipThisAttribute = null) {
         QKeyValue kv = null;
         var hasNewTimeLimit = Attributes.Contains(attrs, "_timeLimit");
         var hasNewRLimit = Attributes.Contains(attrs, "_rlimit");

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -11,6 +11,7 @@
 using System.Numerics;
 using System.Diagnostics.Contracts;
 using DafnyCore.Verifier;
+using DafnyCore.Verifier.Statements;
 using Bpl = Microsoft.Boogie;
 using Microsoft.Boogie;
 using Std.Wrappers;
@@ -261,13 +262,12 @@ public void CheckWellformed(Expression expr, WFOptions wfOptions, Variables loca
     /// <summary>
     /// Adds to "builder" code that checks the well-formedness of "expr".  Any local variables introduced
     /// in this code are added to "locals".
-    /// If "result" is non-null, then after checking the well-formedness of "expr", the generated code will
-    /// assume the equivalent of "result == expr".
     /// See class WFOptions for descriptions of the specified options.
     /// </summary>
     public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
       Variables locals, BoogieStmtListBuilder builder, ExpressionTranslator etran,
       AddResultCommands addResultCommands) {
+
       var origOptions = wfOptions;
       if (wfOptions.LValueContext) {
         // Turn off LValueContext for any recursive call
@@ -1313,7 +1313,7 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) {
             break;
           }
         case MatchExpr matchExpr:
-          MatchStatementVerifier.TrMatchExpr(this, matchExpr, wfOptions, locals, builder, etran, addResultCommands);
+          MatchStmtVerifier.TrMatchExpr(this, matchExpr, wfOptions, locals, builder, etran, addResultCommands);
           addResultCommands = null;
           break;
         case DatatypeUpdateExpr updateExpr: {

Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs

@@ -152,8 +152,8 @@ Bpl.Expr GetField(MemberSelectExpr fse) {
     void AddWellformednessCheck(ConstantField decl) {
       Contract.Requires(decl != null);
       Contract.Requires(sink != null && Predef != null);
-      Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null);
-      Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null);
+      Contract.Requires(currentModule == null && codeContext == null && IsAllocContext == null && fuelContext == null);
+      Contract.Ensures(currentModule == null && codeContext == null && IsAllocContext == null && fuelContext == null);
 
       proofDependencies.SetCurrentDefinition(MethodVerboseName(decl.FullDafnyName, MethodTranslationKind.SpecWellformedness), null);
       if (!InVerificationScope(decl)) {
@@ -209,7 +209,7 @@ void AddWellformednessCheck(ConstantField decl) {
       var builder = new BoogieStmtListBuilder(this, options, new BodyTranslationContext(false));
       builder.Add(new CommentCmd($"AddWellformednessCheck for {decl.WhatKind} {decl}"));
       builder.AddCaptureState(decl.tok, false, "initial state");
-      isAllocContext = new IsAllocContext(options, true);
+      IsAllocContext = new IsAllocContext(options, true);
 
       DefineFrame(decl.tok, etran.ReadsFrame(decl.tok), new List<FrameExpression>(), builder, locals, null);
 
@@ -229,7 +229,7 @@ void AddWellformednessCheck(ConstantField decl) {
 
       Contract.Assert(currentModule == decl.EnclosingModule);
       Contract.Assert(codeContext == decl);
-      isAllocContext = null;
+      IsAllocContext = null;
       fuelContext = null;
       Reset();
     }

Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs

@@ -37,7 +37,7 @@ void AddIteratorSpecAndBody(IteratorDecl iter) {
 
       FuelContext oldFuelContext = this.fuelContext;
       this.fuelContext = FuelSetting.NewFuelContext(iter);
-      isAllocContext = new IsAllocContext(options, false);
+      IsAllocContext = new IsAllocContext(options, false);
 
       // wellformedness check for method specification
       Bpl.Procedure proc = AddIteratorProc(iter, MethodTranslationKind.SpecWellformedness);
@@ -53,7 +53,7 @@ void AddIteratorSpecAndBody(IteratorDecl iter) {
         AddIteratorImpl(iter, proc);
       }
       this.fuelContext = oldFuelContext;
-      isAllocContext = null;
+      IsAllocContext = null;
     }
 
 

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -41,7 +41,7 @@ void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods, bool inc
       }
 
       foreach (MemberDecl member in c.Members.FindAll(VisibleInScope)) {
-        Contract.Assert(isAllocContext == null);
+        Contract.Assert(IsAllocContext == null);
         CurrentDeclaration = member;
         if (!filterOnlyMembers || member.HasUserAttribute("only", out _)) {
           SetAssertionOnlyFilter(member);
@@ -143,7 +143,7 @@ private void AddIsAndIsAllocForReferenceType(ClassLikeDecl c) {
     void AddFunction_Top(Function f, bool includeAllMethods) {
       FuelContext oldFuelContext = this.fuelContext;
       this.fuelContext = FuelSetting.NewFuelContext(f);
-      isAllocContext = new IsAllocContext(options, true);
+      IsAllocContext = new IsAllocContext(options, true);
 
       AddClassMember_Function(f);
 
@@ -161,7 +161,7 @@ void AddFunction_Top(Function f, bool includeAllMethods) {
       }
 
       this.fuelContext = oldFuelContext;
-      isAllocContext = null;
+      IsAllocContext = null;
     }
 
     void AddMethod_Top(Method m, bool isByMethod, bool includeAllMethods) {
@@ -528,13 +528,13 @@ private void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc
       Contract.Requires(proc != null);
       Contract.Requires(sink != null && Predef != null);
       Contract.Requires(wellformednessProc || m.Body != null);
-      Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null);
-      Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null);
+      Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && IsAllocContext == null);
+      Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && IsAllocContext == null);
 
       proofDependencies.SetCurrentDefinition(proc.VerboseName, m);
       currentModule = m.EnclosingClass.EnclosingModuleDefinition;
       codeContext = m;
-      isAllocContext = new IsAllocContext(options, m.IsGhost);
+      IsAllocContext = new IsAllocContext(options, m.IsGhost);
 
       List<Variable> inParams = Boogie.Formal.StripWhereClauses(proc.InParams);
       List<Variable> outParams = Boogie.Formal.StripWhereClauses(proc.OutParams);
@@ -579,7 +579,7 @@ private void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc
         }
       }
 
-      isAllocContext = null;
+      IsAllocContext = null;
       Reset();
     }
 
@@ -819,13 +819,13 @@ private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) {
       Contract.Requires(m.Ins.Count == m.OverriddenMethod.Ins.Count);
       Contract.Requires(m.Outs.Count == m.OverriddenMethod.Outs.Count);
       //Contract.Requires(wellformednessProc || m.Body != null);
-      Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null);
-      Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null);
+      Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && IsAllocContext == null);
+      Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && IsAllocContext == null);
 
       proofDependencies.SetCurrentDefinition(proc.VerboseName, m);
       currentModule = m.EnclosingClass.EnclosingModuleDefinition;
       codeContext = m;
-      isAllocContext = new IsAllocContext(options, m.IsGhost);
+      IsAllocContext = new IsAllocContext(options, m.IsGhost);
 
       List<Variable> inParams = Boogie.Formal.StripWhereClauses(proc.InParams);
       List<Variable> outParams = Boogie.Formal.StripWhereClauses(proc.OutParams);
@@ -893,7 +893,7 @@ private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) {
         }
       }
 
-      isAllocContext = null;
+      IsAllocContext = null;
       Reset();
     }
 
@@ -917,8 +917,8 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       Contract.Requires(sink != null && Predef != null);
       Contract.Requires(f.OverriddenFunction != null);
       Contract.Requires(f.Ins.Count == f.OverriddenFunction.Ins.Count);
-      Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext != null);
-      Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext != null);
+      Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && IsAllocContext != null);
+      Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && IsAllocContext != null);
 
       proofDependencies.SetCurrentDefinition(MethodVerboseName(f.FullDafnyName, MethodTranslationKind.OverrideCheck), f);
       #region first procedure, no impl yet
@@ -1688,15 +1688,15 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
       Contract.Requires(m != null);
       Contract.Requires(m.EnclosingClass != null);
       Contract.Requires(Predef != null);
-      Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null);
-      Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null);
+      Contract.Requires(currentModule == null && codeContext == null && IsAllocContext == null);
+      Contract.Ensures(currentModule == null && codeContext == null && IsAllocContext == null);
       Contract.Ensures(Contract.Result<Boogie.Procedure>() != null);
       Contract.Assert(VisibleInScope(m));
 
       proofDependencies.SetCurrentDefinition(MethodVerboseName(m.FullDafnyName, kind), m);
       currentModule = m.EnclosingClass.EnclosingModuleDefinition;
       codeContext = m;
-      isAllocContext = new IsAllocContext(options, m.IsGhost);
+      IsAllocContext = new IsAllocContext(options, m.IsGhost);
       Boogie.Expr prevHeap = null;
       Boogie.Expr currHeap = null;
       var ordinaryEtran = new ExpressionTranslator(this, Predef, m.tok, m);
@@ -1732,7 +1732,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) {
 
       currentModule = null;
       codeContext = null;
-      isAllocContext = null;
+      IsAllocContext = null;
 
       return proc;