Enable marking if commands as {:allow_split} or not

Source/AbstractInterpretation/NativeLattice.cs

@@ -185,8 +185,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       // We need to keep track of some information for each(some) block(s).  To do that efficiently,
       // we number the implementation's blocks sequentially, and then we can use arrays to store
       // the additional information.
-      var pre = new NativeLattice.Element[impl.Blocks
-        .Count]; // set to null if we never compute a join/widen at this block
+      var pre = new NativeLattice.Element[impl.Blocks.Count]; // set to null if we never compute a join/widen at this block
       var post = options.InstrumentInfer == CoreOptions.InstrumentationPlaces.Everywhere
         ? new NativeLattice.Element[impl.Blocks.Count]
         : null;
@@ -195,7 +194,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       int n = 0;
       foreach (var block in impl.Blocks)
       {
-        block.aiId = n;
+        block.AiId = n;
         // Note:  The forward analysis below will store lattice elements in pre[n] if pre[n] is non-null.
         // Thus, the assignment "pre[n] = bottom;" below must be done under the following condition:
         //    n == 0 || block.widenBlock
@@ -219,7 +218,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       {
         var workItem = workItems.Dequeue();
         var b = workItem.Item1;
-        var id = b.aiId;
+        var id = b.AiId;
         var e = workItem.Item2;
         if (pre[id] == null)
         {
@@ -230,7 +229,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
           // no change
           continue;
         }
-        else if (b.widenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
+        else if (b.WidenBlock && options.Ai.StepsBeforeWidening <= iterations[id])
         {
           e = lattice.Widen(pre[id], e);
           pre[id] = e;
@@ -275,8 +274,8 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.
 
       foreach (var b in impl.Blocks)
       {
-        var element = pre[b.aiId];
-        if (element != null && (b.widenBlock || options.InstrumentInfer ==
+        var element = pre[b.AiId];
+        if (element != null && (b.WidenBlock || options.InstrumentInfer ==
           CoreOptions.InstrumentationPlaces.Everywhere))
         {
           List<Cmd> newCommands = new List<Cmd>();
@@ -294,9 +293,9 @@ void Instrument(Implementation impl, NativeLattice.Element[] pre, NativeLattice.
 
           newCommands.Add(cmd);
           newCommands.AddRange(b.Cmds);
-          if (post != null && post[b.aiId] != null)
+          if (post != null && post[b.AiId] != null)
           {
-            inv = post[b.aiId].ToExpr(options);
+            inv = post[b.AiId].ToExpr(options);
             kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
             if (options.InstrumentWithAsserts)
             {

Source/AbstractInterpretation/Traverse.cs

@@ -54,7 +54,7 @@ static void Visit(Block b)
       {
         cce.BeginExpose(b);
         // we got here through a back-edge
-        b.widenBlock = true;
+        b.WidenBlock = true;
         cce.EndExpose();
       }
       else if (b.TraversingStatus == Block.VisitState.AlreadyVisited)
@@ -111,7 +111,7 @@ static void Visit(Block b)
     /// </summary>
     public static List<Block> ComputeLoopBodyFrom(Block block)
     {
-      Contract.Requires(block.widenBlock);
+      Contract.Requires(block.WidenBlock);
       Contract.Requires(block != null);
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
 

Source/Concurrency/CivlUtil.cs

@@ -307,14 +307,16 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars)
 
   public static class BlockHelper
   {
+    public static readonly IToken /*!*/ ReportedNoToken = new Token();
+
     public static Block Block(string label, List<Cmd> cmds)
     {
-      return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd);
+      return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd);
     }
 
     public static Block Block(string label, List<Cmd> cmds, List<Block> gotoTargets)
     {
-      return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
+      return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
     }
   }
 

Source/Concurrency/LinearPermissionInstrumentation.cs

@@ -61,18 +61,18 @@ public List<Cmd> DisjointnessAndWellFormedAssumeCmds(Absy absy, bool addGlobals)
     public void AddDisjointnessAndWellFormedAssumptions(Implementation impl)
     {
       // calls and parallel calls
-      foreach (var b in impl.Blocks)
+      foreach (var block in impl.Blocks)
       {
         var newCmds = new List<Cmd>();
-        foreach (var cmd in b.Cmds)
+        foreach (var cmd in block.Cmds)
         {
           newCmds.Add(cmd);
           if (cmd is ParCallCmd)
           {
             newCmds.AddRange(DisjointnessAndWellFormedAssumeCmds(cmd, true));
           }
         }
-        b.Cmds = newCmds;
+        block.Cmds = newCmds;
       }
 
       // loop headers

Source/Concurrency/LinearTypeChecker.cs

@@ -852,14 +852,14 @@ void ProcessIfCmd(IfCmd ifCmd)
                   {
                     checkingContext.Error(ifCmd.tok, "access to linear store not allowed");
                   }
-                  stmtLists.Push(ifCmd.thn);
-                  if (ifCmd.elseIf != null)
+                  stmtLists.Push(ifCmd.Thn);
+                  if (ifCmd.ElseIf != null)
                   {
-                    ProcessIfCmd(ifCmd.elseIf);
+                    ProcessIfCmd(ifCmd.ElseIf);
                   }
-                  else if (ifCmd.elseBlock != null)
+                  else if (ifCmd.ElseBlock != null)
                   {
-                    stmtLists.Push(ifCmd.elseBlock);
+                    stmtLists.Push(ifCmd.ElseBlock);
                   }
                 }
                 ProcessIfCmd(ifCmd);

Source/Concurrency/YieldingProcInstrumentation.cs

@@ -474,65 +474,61 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
 
       // add jumps to noninterferenceChecker, returnChecker, and refinementChecker blocks
       var implRefinementCheckingBlocks = new List<Block>();
-      foreach (var b in impl.Blocks)
-      {
-        if (b.TransferCmd is GotoCmd gotoCmd)
-        {
-          var targetBlocks = new List<Block>();
-          var addEdge = false;
-          foreach (var nextBlock in gotoCmd.LabelTargets)
-          {
-            if (nextBlock.cmds.Count > 0)
-            {
-              var cmd = nextBlock.cmds[0];
-              if (cmd is ParCallCmd parCallCmd)
-              {
-                foreach (var callCmd in parCallCmd.CallCmds)
-                {
-                  if (refinementBlocks.ContainsKey(callCmd))
-                  {
-                    var targetBlock = refinementBlocks[callCmd];
-                    FixUpImplRefinementCheckingBlock(targetBlock,
-                      CivlAttributes.IsCallMarked(callCmd)
-                        ? returnCheckerBlock
-                        : unchangedCheckerBlock);
-                    targetBlocks.Add(targetBlock);
-                    implRefinementCheckingBlocks.Add(targetBlock);
-                  }
-                }
-                addEdge = true;
-              }
-            }
+      foreach (var b in impl.Blocks) {
+        if (b.TransferCmd is not GotoCmd gotoCmd) {
+          b.TransferCmd = new GotoCmd(b.TransferCmd.tok,
+            new List<Block> { returnCheckerBlock, returnBlock, noninterferenceCheckerBlock });
+          continue;
+        }
+
+        var targetBlocks = new List<Block>();
+        var addEdge = false;
+        foreach (var nextBlock in gotoCmd.LabelTargets) {
+          if (nextBlock.Cmds.Count <= 0) {
+            continue;
           }
 
-          gotoCmd.AddTargets(targetBlocks);
-          if (addEdge)
-          {
-            AddEdge(gotoCmd, noninterferenceCheckerBlock);
-            if (blocksInYieldingLoops.Contains(b))
-            {
-              AddEdge(gotoCmd, unchangedCheckerBlock);
-            }
-            else
-            {
-              b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
-              AddEdge(gotoCmd, refinementCheckerBlock);
+          var cmd = nextBlock.Cmds[0];
+          if (cmd is not ParCallCmd parCallCmd) {
+            continue;
+          }
+
+          foreach (var callCmd in parCallCmd.CallCmds) {
+            if (!refinementBlocks.TryGetValue(callCmd, out var targetBlock)) {
+              continue;
             }
+
+            FixUpImplRefinementCheckingBlock(targetBlock,
+              CivlAttributes.IsCallMarked(callCmd)
+                ? returnCheckerBlock
+                : unchangedCheckerBlock);
+            targetBlocks.Add(targetBlock);
+            implRefinementCheckingBlocks.Add(targetBlock);
           }
+
+          addEdge = true;
         }
-        else
-        {
-          b.TransferCmd = new GotoCmd(b.TransferCmd.tok,
-            new List<Block> {returnCheckerBlock, returnBlock, noninterferenceCheckerBlock});
+
+        gotoCmd.AddTargets(targetBlocks);
+        if (!addEdge) {
+          continue;
+        }
+
+        AddEdge(gotoCmd, noninterferenceCheckerBlock);
+        if (blocksInYieldingLoops.Contains(b)) {
+          AddEdge(gotoCmd, unchangedCheckerBlock);
+        } else {
+          b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
+          AddEdge(gotoCmd, refinementCheckerBlock);
         }
       }
 
       // desugar ParCallCmd 
       foreach (Block b in impl.Blocks)
       {
-        if (b.cmds.Count > 0)
+        if (b.Cmds.Count > 0)
         {
-          var cmd = b.cmds[0];
+          var cmd = b.Cmds[0];
           if (cmd is ParCallCmd)
           {
             DesugarParCallCmdInBlock(b, blocksInYieldingLoops.Contains(b));
@@ -578,27 +574,27 @@ private void SplitBlocks(Implementation impl)
       {
         var currTransferCmd = b.TransferCmd;
         int labelCount = 0;
-        int lastSplitIndex = b.cmds.Count;
-        for (int i = b.cmds.Count - 1; i >= 0; i--)
+        int lastSplitIndex = b.Cmds.Count;
+        for (int i = b.Cmds.Count - 1; i >= 0; i--)
         {
           var split = false;
-          var cmd = b.cmds[i];
+          var cmd = b.Cmds[i];
           if (cmd is ParCallCmd)
           {
             split = true;
           }
 
           if (split)
           {
-            var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.cmds.GetRange(i, lastSplitIndex - i),
+            var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.Cmds.GetRange(i, lastSplitIndex - i),
               currTransferCmd);
             newBlocks.Add(newBlock);
             currTransferCmd = new GotoCmd(b.tok, new List<Block> {newBlock});
             lastSplitIndex = i;
           }
         }
 
-        b.cmds = b.cmds.GetRange(0, lastSplitIndex);
+        b.Cmds = b.Cmds.GetRange(0, lastSplitIndex);
         b.TransferCmd = currTransferCmd;
       }
 
@@ -714,8 +710,8 @@ private void DesugarParCallCmdInBlock(Block block, bool isBlockInYieldingLoop)
       newCmds.AddRange(CreateUpdatesToOldGlobalVars());
       newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars());
       newCmds.AddRange(CreateUpdatesToPermissionCollector(parCallCmd));
-      newCmds.AddRange(block.cmds.GetRange(1, block.cmds.Count - 1));
-      block.cmds = newCmds;
+      newCmds.AddRange(block.Cmds.GetRange(1, block.Cmds.Count - 1));
+      block.Cmds = newCmds;
     }
 
     private Formal ParCallDesugarFormal(Variable v, int count, bool incoming)

Source/Core/AST/Absy.cs

@@ -1300,7 +1300,7 @@ public override void Resolve(ResolutionContext rc)
 
     public void ResolveWhere(ResolutionContext rc)
     {
-      if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && this.TypedIdent.WhereExpr != null)
+      if (Attributes.FindBoolAttribute("assumption") && this.TypedIdent.WhereExpr != null)
       {
         rc.Error(tok, "assumption variable may not be declared with a where clause");
       }
@@ -1315,7 +1315,7 @@ public override void Typecheck(TypecheckingContext tc)
     {
       (this as ICarriesAttributes).TypecheckAttributes(tc);
       this.TypedIdent.Typecheck(tc);
-      if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && !this.TypedIdent.Type.IsBool)
+      if (Attributes.FindBoolAttribute("assumption") && !this.TypedIdent.Type.IsBool)
       {
         tc.Error(tok, "assumption variable must be of type 'bool'");
       }
@@ -2059,7 +2059,7 @@ public override void Emit(TokenTextWriter stream, int level)
 
       stream.Write(this, level, (AlwaysRevealed ? "revealed " : "") + "function ");
       EmitAttributes(stream);
-      if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline"))
+      if (Body != null && !Attributes.FindBoolAttribute("inline"))
       {
         Contract.Assert(DefinitionBody == null);
         // Boogie inlines any function whose .Body field is non-null.  The parser populates the .Body field
@@ -2069,7 +2069,7 @@ public override void Emit(TokenTextWriter stream, int level)
         stream.Write("{:inline} ");
       }
 
-      if (DefinitionBody != null && !QKeyValue.FindBoolAttribute(Attributes, "define"))
+      if (DefinitionBody != null && !Attributes.FindBoolAttribute("define"))
       {
         // Boogie defines any function whose .DefinitionBody field is non-null.  The parser populates the .DefinitionBody field
         // if the :define attribute is present, but if someone creates the Boogie file directly as an AST, then
@@ -2350,7 +2350,7 @@ public String ErrorMessage
 
     public bool CanAlwaysAssume()
     {
-      return Free && QKeyValue.FindBoolAttribute(Attributes, "always_assume");
+      return Free && Attributes.FindBoolAttribute("always_assume");
     }
 
 
@@ -2490,7 +2490,7 @@ public String ErrorMessage
 
     public bool CanAlwaysAssume ()
     {
-      return Free && QKeyValue.FindBoolAttribute(this.Attributes, "always_assume");
+      return Free && Attributes.FindBoolAttribute("always_assume");
     }
 
     public Ensures(IToken token, bool free, Expr condition, string comment, QKeyValue kv)