Enable marking if commands as {:allow_split} or not

Source/AbstractInterpretation/NativeLattice.cs

@@ -195,7 +195,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 +219,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 +230,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 +275,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 +294,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/LinearTypeChecker.cs

@@ -773,14 +773,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,73 @@ 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)
+      foreach (var block in impl.Blocks)
       {
-        if (b.TransferCmd is GotoCmd gotoCmd)
+        if (block.TransferCmd is not GotoCmd gotoCmd)
+        {
+          block.TransferCmd = new GotoCmd(block.TransferCmd.tok,
+            new List<Block> { returnCheckerBlock, returnBlock, noninterferenceCheckerBlock });
+        }
+        else
         {
           var targetBlocks = new List<Block>();
           var addEdge = false;
           foreach (var nextBlock in gotoCmd.LabelTargets)
           {
-            if (nextBlock.cmds.Count > 0)
+            if (nextBlock.Cmds.Count <= 0)
+            {
+              continue;
+            }
+
+            var cmd = nextBlock.Cmds[0];
+            if (cmd is not ParCallCmd parCallCmd)
             {
-              var cmd = nextBlock.cmds[0];
-              if (cmd is ParCallCmd parCallCmd)
+              continue;
+            }
+
+            foreach (var callCmd in parCallCmd.CallCmds)
+            {
+              if (!refinementBlocks.TryGetValue(callCmd, out var targetBlock))
               {
-                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;
+                continue;
               }
+
+              FixUpImplRefinementCheckingBlock(targetBlock,
+                CivlAttributes.IsCallMarked(callCmd)
+                  ? returnCheckerBlock
+                  : unchangedCheckerBlock);
+              targetBlocks.Add(targetBlock);
+              implRefinementCheckingBlocks.Add(targetBlock);
             }
+
+            addEdge = true;
           }
 
           gotoCmd.AddTargets(targetBlocks);
-          if (addEdge)
+          if (!addEdge)
           {
-            AddEdge(gotoCmd, noninterferenceCheckerBlock);
-            if (blocksInYieldingLoops.Contains(b))
-            {
-              AddEdge(gotoCmd, unchangedCheckerBlock);
-            }
-            else
-            {
-              b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
-              AddEdge(gotoCmd, refinementCheckerBlock);
-            }
+            continue;
+          }
+
+          AddEdge(gotoCmd, noninterferenceCheckerBlock);
+          if (blocksInYieldingLoops.Contains(block))
+          {
+            AddEdge(gotoCmd, unchangedCheckerBlock);
+          }
+          else
+          {
+            block.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
+            AddEdge(gotoCmd, refinementCheckerBlock);
           }
-        }
-        else
-        {
-          b.TransferCmd = new GotoCmd(b.TransferCmd.tok,
-            new List<Block> {returnCheckerBlock, returnBlock, noninterferenceCheckerBlock});
         }
       }
 
       // 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 +586,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 +722,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)

Source/Core/AST/AbsyQuant.cs

@@ -543,16 +543,6 @@ public static Expr FindExprAttribute(QKeyValue kv, string name)
       return null;
     }
 
-    // Return 'true' if {:name true} or {:name} is an attribute in 'kv'
-    public static bool FindBoolAttribute(QKeyValue kv, string name)
-    {
-      Contract.Requires(name != null);
-      kv = FindAttribute(kv, qkv => qkv.Key == name && (qkv.Params.Count == 0 ||
-                                    (qkv.Params.Count == 1 && qkv.Params[0] is LiteralExpr &&
-                                      ((LiteralExpr) qkv.Params[0]).IsTrue)));
-      return kv != null;
-    }
-
     public static int FindIntAttribute(QKeyValue kv, string name, int defl)
     {
       Contract.Requires(name != null);