added yield_assert attribute to allow less cumbersome factoring of yi…

…eld assertions to procedures

Source/Concurrency/CivlRefinement.cs

@@ -256,7 +256,7 @@ public override Ensures VisitEnsures(Ensures node)
  if (isAtomicSpecification || !civlTypeChecker.absyToLayerNums[node].Contains(layerNum))
  {
  ensures.Condition = Expr.True;
- ensures.Attributes = Concurrency.RemoveMoverAttribute(ensures.Attributes);
+ Concurrency.RemoveMoverAttribute(ensures);
  }
  return ensures;
  }

Source/Concurrency/CivlTypeChecker.cs

@@ -269,37 +269,37 @@ public class LayerEraser : ReadOnlyVisitor
  {
  public override Variable VisitVariable(Variable node)
  {
- node.Attributes = Concurrency.RemoveLayerAttribute(node.Attributes);
+ Concurrency.RemoveLayerAttribute(node);
  return base.VisitVariable(node);
  }
 
  public override Procedure VisitProcedure(Procedure node)
  {
- node.Attributes = Concurrency.RemoveLayerAttribute(node.Attributes);
+ Concurrency.RemoveLayerAttribute(node);
  return base.VisitProcedure(node);
  }
 
  public override Implementation VisitImplementation(Implementation node)
  {
- node.Attributes = Concurrency.RemoveLayerAttribute(node.Attributes);
+ Concurrency.RemoveLayerAttribute(node);
  return base.VisitImplementation(node);
  }
 
  public override Requires VisitRequires(Requires node)
  {
- node.Attributes = Concurrency.RemoveLayerAttribute(node.Attributes);
+ Concurrency.RemoveLayerAttribute(node);
  return base.VisitRequires(node);
  }
 
  public override Ensures VisitEnsures(Ensures node)
  {
- node.Attributes = Concurrency.RemoveLayerAttribute(node.Attributes);
+ Concurrency.RemoveLayerAttribute(node);
  return base.VisitEnsures(node);
  }
 
  public override Cmd VisitAssertCmd(AssertCmd node)
  {
- node.Attributes = Concurrency.RemoveLayerAttribute(node.Attributes);
+ Concurrency.RemoveLayerAttribute(node);
  return base.VisitAssertCmd(node);
  }
  }

Source/Concurrency/LinearSets.cs

@@ -12,13 +12,13 @@ public class LinearEraser : ReadOnlyVisitor
  {
  public override Variable VisitVariable(Variable node)
  {
- node.Attributes = Concurrency.RemoveLinearAttribute(node.Attributes);
+ Concurrency.RemoveLinearAttribute(node);
  return base.VisitVariable(node);
  }
 
  public override Function VisitFunction(Function node)
  {
- node.Attributes = Concurrency.RemoveLinearAttribute(node.Attributes);
+ Concurrency.RemoveLinearAttribute(node);
  return base.VisitFunction(node);
  }
  }

Source/Concurrency/Program.cs

@@ -38,41 +38,68 @@ public static void Transform(LinearTypeChecker linearTypeChecker, CivlTypeChecke
  }
  foreach (Declaration decl in decls)
  {
- decl.Attributes = RemoveYieldsAttribute(decl.Attributes);
+ RemoveYieldsAttribute(decl);
  }
  program.RemoveTopLevelDeclarations(x => originalDecls.Contains(x));
  program.AddTopLevelDeclarations(decls);
  }
 
- public static QKeyValue RemoveYieldsAttribute(QKeyValue iter)
+ public static bool RemoveAttribute(ICarriesAttributes obj, Func<QKeyValue, bool> cond)
  {
- if (iter == null) return null;
- iter.Next = RemoveYieldsAttribute(iter.Next);
- return (iter.Key == "yields") ? iter.Next : iter;
+ QKeyValue curr = obj.Attributes;
+ bool removed = false;
+
+ while (curr != null && cond (curr)) {
+ curr = curr.Next;
+ removed = true;
+ }
+ obj.Attributes = curr;
+ while (curr != null) {
+ QKeyValue next = curr.Next;
+ while (next != null && cond (next)) {
+ next = next.Next;
+ removed = true;
+ }
+ curr.Next = next;
+ curr = next;
+ }
+
+ return removed;
+ }
+
+ public static void RemoveYieldsAttribute(ICarriesAttributes obj)
+ {
+ RemoveAttribute(obj, kv => kv.Key == "yields");
  }
 
- public static QKeyValue RemoveMoverAttribute(QKeyValue iter)
+ public static void RemoveMoverAttribute(ICarriesAttributes obj)
  {
- if (iter == null) return null;
- iter.Next = RemoveMoverAttribute(iter.Next);
- if (iter.Key == "atomic" || iter.Key == "right" || iter.Key == "left" || iter.Key == "both")
- return iter.Next;
- else
- return iter;
+ RemoveAttribute (obj,
+ kv => kv.Key == "atomic" || kv.Key == "right" || kv.Key == "left" || kv.Key == "both");
  }
 
- public static QKeyValue RemoveLayerAttribute(QKeyValue iter)
+ public static void RemoveLayerAttribute(ICarriesAttributes obj)
  {
- if (iter == null) return null;
- iter.Next = RemoveLayerAttribute(iter.Next);
- return (iter.Key == "layer") ? iter.Next : iter;
+ RemoveAttribute(obj, kv => kv.Key == "layer");
  }
 
- public static QKeyValue RemoveLinearAttribute(QKeyValue iter)
+ public static void RemoveLinearAttribute(ICarriesAttributes obj)
  {
- if (iter == null) return null;
- iter.Next = RemoveLinearAttribute(iter.Next);
- return (iter.Key == "linear" || iter.Key == "linear_in" || iter.Key == "linear_out") ? iter.Next : iter;
+ RemoveAttribute(obj, 
+ kv => kv.Key == "linear" || kv.Key == "linear_in" || kv.Key == "linear_out");
+ }
+
+ public static void DesugarYieldAssert (Program program) {
+ foreach (var proc in program.Procedures) {
+ if (RemoveAttribute(proc, kv => kv.Key == "yield_assert")) {
+ proc.AddAttribute("yields");
+ foreach (var requires in proc.Requires) {
+ var ensures = new Ensures(false, requires.Condition);
+ ensures.Attributes = requires.Attributes;
+ proc.Ensures.Add(ensures);
+ }
+ }
+ }
  }
  }
 }

Source/ExecutionEngine/ExecutionEngine.cs

@@ -483,6 +483,8 @@ public static void ProcessFiles(List<string> fileNames, bool lookForSnapshots =
  PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false, true, CommandLineOptions.Clo.PrettyPrint);
  }
 
+ Concurrency.DesugarYieldAssert(program);
+
  LinearTypeChecker linearTypeChecker;
  CivlTypeChecker civlTypeChecker;
  PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1], out linearTypeChecker, out civlTypeChecker);

Util/Emacs/boogie-mode.el

@@ -44,8 +44,9 @@
  "async" "par"
  )) . font-lock-keyword-face)
  `(,(boogie-regexp-opt '(
- "layer" "yields" "linear" "linear_in" "linear_out"
+ "layer" "yields" "yield_assert"
  "atomic" "left" "right" "both"
+ "linear" "linear_in" "linear_out"
  "yield"
  )) . font-lock-preprocessor-face)
  `(,(boogie-regexp-opt '(