Enable marking if commands as {:allow_split} or not (#970)

### Changes
- Introduce the attribute `{:allow_split}` that can be placed on
`IfCmd`. When using `{:isolate "paths"}` only, branches with
`{:allow_split}` will trigger splitting of the VC.

### Testing
- Updated existing tests so they exercise the presence and absence of
`{:allow_split}`
- Added a test that combines `{:vcs_split_on_every_assert}` and explicit
returns.

Source/Concurrency/YieldingProcInstrumentation.cs

@@ -541,9 +541,7 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
       impl.Blocks.Add(unchangedCheckerBlock);
       impl.Blocks.Add(returnCheckerBlock);
       impl.Blocks.Add(returnBlock);
-      foreach (var block in implRefinementCheckingBlocks) {
-        impl.Blocks.Add(block);
-      }
+      impl.Blocks.AddRange(implRefinementCheckingBlocks);
       impl.Blocks.Insert(0, CreateInitialBlock(impl, preconditions));
     }
 
@@ -600,9 +598,7 @@ private void SplitBlocks(Implementation impl)
         b.TransferCmd = currTransferCmd;
       }
 
-      foreach (var newBlock in newBlocks) {
-        impl.Blocks.Add(newBlock);
-      }
+      impl.Blocks.AddRange(newBlocks);
     }
 
     private Block CreateNoninterferenceCheckerBlock()

Source/Core/AST/Absy.cs

@@ -2490,7 +2490,7 @@ public String ErrorMessage
 
     public bool CanAlwaysAssume ()
     {
-      return Free && this.Attributes.FindBoolAttribute("always_assume");
+      return Free && Attributes.FindBoolAttribute("always_assume");
     }
 
     public Ensures(IToken token, bool free, Expr condition, string comment, QKeyValue kv)

Source/Core/AST/Commands/AbsyCmd.cs

@@ -3,12 +3,9 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Diagnostics.Contracts;
-using Set = Microsoft.Boogie.GSet<object>;
 
 namespace Microsoft.Boogie
 {
-  //---------------------------------------------------------------------
-  // Commands
   [ContractClassFor(typeof(Cmd))]
   public abstract class CmdContracts : Cmd
   {
@@ -2088,8 +2085,7 @@ public override Absy StdDispatch(StandardVisitor visitor)
 
   public class ReturnExprCmd : ReturnCmd
   {
-    public Expr /*!*/
-      Expr;
+    public Expr /*!*/ Expr;
 
     [ContractInvariantMethod]
     void ObjectInvariant()
@@ -2214,21 +2210,4 @@ public override Absy StdDispatch(StandardVisitor visitor)
       return visitor.VisitHavocCmd(this);
     }
   }
-
-  //---------------------------------------------------------------------
-  // Transfer commands
-
-  [ContractClassFor(typeof(TransferCmd))]
-  public abstract class TransferCmdContracts : TransferCmd
-  {
-    public TransferCmdContracts() : base(null)
-    {
-    }
-
-    public override void Emit(TokenTextWriter stream, int level)
-    {
-      Contract.Requires(stream != null);
-      throw new NotImplementedException();
-    }
-  }
 }

Source/Core/AST/Commands/CallCmd.cs

@@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
         Contract.Assert(a != null);
         // These probably won't have IDs, but copy if they do.
         if (callId is not null) {
-          (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req,
+          a.CopyIdWithModificationsFrom(tok, req,
             id => new TrackedCallRequiresAssumed(callId, id));
         }
 

Source/Core/AST/GotoBoogie/Block.cs

@@ -7,11 +7,12 @@ namespace Microsoft.Boogie;
 
 public sealed class Block : Absy
 {
-  public string /*!*/ Label { get; set; } // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
+
+  public string Label { get; set; } // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
 
-  [Rep] 
-  [ElementsPeer] 
-  public List<Cmd> /*!*/ Cmds;
+  [Rep]
+  [ElementsPeer]
+  public List<Cmd> Cmds { get; set; }
 
   public IEnumerable<Block> Exits()
   {
@@ -23,8 +24,7 @@ public IEnumerable<Block> Exits()
   }
 
   [Rep] //PM: needed to verify Traverse.Visit
-  public TransferCmd
-    TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)
+  public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)
 
   public byte[] Checksum;
 
@@ -164,10 +164,10 @@ public override void Resolve(ResolutionContext rc)
 
   public override void Typecheck(TypecheckingContext tc)
   {
-    foreach (Cmd /*!*/ c in Cmds)
+    foreach (var /*!*/ cmd in Cmds)
     {
-      Contract.Assert(c != null);
-      c.Typecheck(tc);
+      Contract.Assert(cmd != null);
+      cmd.Typecheck(tc);
     }
 
     Contract.Assume(this.TransferCmd != null);

Source/Core/AST/GotoBoogie/GotoCmd.cs

@@ -5,7 +5,7 @@
 
 namespace Microsoft.Boogie;
 
-public class GotoCmd : TransferCmd
+public class GotoCmd : TransferCmd, ICarriesAttributes
 {
   [Rep] public List<string> LabelNames;
   [Rep] public List<Block> LabelTargets;
@@ -43,20 +43,20 @@ public GotoCmd(IToken /*!*/ tok, List<string> /*!*/ labels, List<Block> /*!*/ bl
     this.LabelTargets = blocks;
   }
 
-  public GotoCmd(IToken /*!*/ tok, List<Block> /*!*/ blockSeq)
+  public GotoCmd(IToken /*!*/ tok, List<Block> /*!*/ blocks)
     : base(tok)
   {
     //requires (blockSeq[i] != null ==> blockSeq[i].Label != null);
     Contract.Requires(tok != null);
-    Contract.Requires(blockSeq != null);
-    List<string> labelSeq = new List<string>();
-    for (int i = 0; i < blockSeq.Count; i++)
+    Contract.Requires(blocks != null);
+    var labels = new List<string>();
+    foreach (var block in blocks)
     {
-      labelSeq.Add(cce.NonNull(blockSeq[i]).Label);
+      labels.Add(block.Label);
     }
 
-    this.LabelNames = labelSeq;
-    this.LabelTargets = blockSeq;
+    this.LabelNames = labels;
+    this.LabelTargets = blocks;
   }
 
   public void RemoveTarget(Block b) {
@@ -91,6 +91,7 @@ public override void Emit(TokenTextWriter stream, int level)
     //Contract.Requires(stream != null);
     Contract.Assume(this.LabelNames != null);
     stream.Write(this, level, "goto ");
+    Attributes?.Emit(stream);
     if (stream.Options.PrintWithUniqueASTIds)
     {
       if (LabelTargets == null)

Source/Core/AST/GotoBoogie/TransferCmdContracts.cs

@@ -0,0 +1,18 @@
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+[ContractClassFor(typeof(TransferCmd))]
+public abstract class TransferCmdContracts : TransferCmd
+{
+  public TransferCmdContracts() : base(null)
+  {
+  }
+
+  public override void Emit(TokenTextWriter stream, int level)
+  {
+    Contract.Requires(stream != null);
+    throw new NotImplementedException();
+  }
+}

Source/Core/AST/QKeyValue.cs

@@ -48,14 +48,14 @@ void ObjectInvariant()
     Contract.Invariant(cce.NonNullElements(this._params));
   }
 
-  public QKeyValue(IToken tok, string key, IList<object /*!*/> /*!*/ parameters, QKeyValue next)
+  public QKeyValue(IToken tok, string key, IList<object /*!*/> /*!*/ parameters = null, QKeyValue next = null)
     : base(tok)
   {
     Contract.Requires(key != null);
     Contract.Requires(tok != null);
     Contract.Requires(cce.NonNullElements(parameters));
     Key = key;
-    this._params = new List<object>(parameters);
+    this._params = parameters == null ? new List<object>() : new List<object>(parameters);
     Next = next;
   }