summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2015-06-10 10:46:17 -0700
committerGravatar qadeer <qadeer@microsoft.com>2015-06-10 10:46:17 -0700
commit9c97c7c52776575485c3b131202addb1d864e3d9 (patch)
treeda29e22ba497d5bef18b1219f1a36f70dc22953d
parent47d48285c8ea7ab0c368c2594a4d8717a9361291 (diff)
fixed crash
Diffstat
-rw-r--r--Source/Concurrency/TypeCheck.cs1519
-rw-r--r--Source/Concurrency/YieldTypeChecker.cs731
-rw-r--r--Source/Provers/SMTLib/SMTLibProcess.cs794
-rw-r--r--Test/civl/chris3.bpl19
-rw-r--r--Test/civl/chris3.bpl.expect3
5 files changed, 1550 insertions, 1516 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index c407a7b9..793012e6 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -1,757 +1,764 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using Microsoft.Boogie;
-using System.Diagnostics.Contracts;
-using System.Diagnostics;
-
-namespace Microsoft.Boogie
-{
- public enum MoverType
- {
- Top,
- Atomic,
- Right,
- Left,
- Both
- }
-
- public class ActionInfo
- {
- public Procedure proc;
- public int createdAtLayerNum;
- public int availableUptoLayerNum;
- public bool hasImplementation;
- public bool isExtern;
-
- public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum)
- {
- this.proc = proc;
- this.createdAtLayerNum = createdAtLayerNum;
- this.availableUptoLayerNum = availableUptoLayerNum;
- this.hasImplementation = false;
- this.isExtern = QKeyValue.FindBoolAttribute(proc.Attributes, "extern");
- }
-
- public virtual bool IsRightMover
- {
- get { return true; }
- }
-
- public virtual bool IsLeftMover
- {
- get { return true; }
- }
- }
-
- public class AtomicActionInfo : ActionInfo
- {
- public Ensures ensures;
- public MoverType moverType;
- public List<AssertCmd> thisGate;
- public CodeExpr thisAction;
- public List<Variable> thisInParams;
- public List<Variable> thisOutParams;
- public List<AssertCmd> thatGate;
- public CodeExpr thatAction;
- public List<Variable> thatInParams;
- public List<Variable> thatOutParams;
- public HashSet<Variable> actionUsedGlobalVars;
- public HashSet<Variable> modifiedGlobalVars;
- public HashSet<Variable> gateUsedGlobalVars;
- public bool hasAssumeCmd;
-
- public bool CommutesWith(AtomicActionInfo actionInfo)
- {
- if (this.modifiedGlobalVars.Intersect(actionInfo.actionUsedGlobalVars).Count() > 0)
- return false;
- if (this.actionUsedGlobalVars.Intersect(actionInfo.modifiedGlobalVars).Count() > 0)
- return false;
- return true;
- }
-
- public override bool IsRightMover
- {
- get { return moverType == MoverType.Right || moverType == MoverType.Both; }
- }
-
- public override bool IsLeftMover
- {
- get { return moverType == MoverType.Left || moverType == MoverType.Both; }
- }
-
- public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int layerNum, int availableUptoLayerNum)
- : base(proc, layerNum, availableUptoLayerNum)
- {
- CodeExpr codeExpr = ensures.Condition as CodeExpr;
- this.ensures = ensures;
- this.moverType = moverType;
- this.thisGate = new List<AssertCmd>();
- this.thisAction = codeExpr;
- this.thisInParams = new List<Variable>();
- this.thisOutParams = new List<Variable>();
- this.thatGate = new List<AssertCmd>();
- this.thatInParams = new List<Variable>();
- this.thatOutParams = new List<Variable>();
- this.hasAssumeCmd = false;
-
- foreach (Block block in codeExpr.Blocks)
- {
- block.Cmds.ForEach(x => this.hasAssumeCmd = this.hasAssumeCmd || x is AssumeCmd);
- }
-
- var cmds = thisAction.Blocks[0].Cmds;
- for (int i = 0; i < cmds.Count; i++)
- {
- AssertCmd assertCmd = cmds[i] as AssertCmd;
- if (assertCmd == null) break;
- thisGate.Add(assertCmd);
- cmds[i] = new AssumeCmd(assertCmd.tok, Expr.True);
- }
-
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- foreach (Variable x in proc.InParams)
- {
- this.thisInParams.Add(x);
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes);
- this.thatInParams.Add(y);
- map[x] = Expr.Ident(y);
- }
- foreach (Variable x in proc.OutParams)
- {
- this.thisOutParams.Add(x);
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes);
- this.thatOutParams.Add(y);
- map[x] = Expr.Ident(y);
- }
- List<Variable> thatLocVars = new List<Variable>();
- foreach (Variable x in thisAction.LocVars)
- {
- Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
- map[x] = Expr.Ident(y);
- thatLocVars.Add(y);
- }
- Contract.Assume(proc.TypeParameters.Count == 0);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (AssertCmd assertCmd in thisGate)
- {
- thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
- }
- Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
- List<Block> thatBlocks = new List<Block>();
- foreach (Block block in thisAction.Blocks)
- {
- List<Cmd> otherCmds = new List<Cmd>();
- foreach (Cmd cmd in block.Cmds)
- {
- otherCmds.Add(Substituter.Apply(subst, cmd));
- }
- Block thatBlock = new Block();
- thatBlock.Cmds = otherCmds;
- thatBlock.Label = "that_" + block.Label;
- block.Label = "this_" + block.Label;
- thatBlocks.Add(thatBlock);
- blockMap[block] = thatBlock;
- if (block.TransferCmd is GotoCmd)
- {
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- for (int i = 0; i < gotoCmd.labelNames.Count; i++)
- {
- gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
- }
- }
- }
- foreach (Block block in thisAction.Blocks)
- {
- if (block.TransferCmd is ReturnExprCmd)
- {
- block.TransferCmd = new ReturnCmd(block.TransferCmd.tok);
- blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
- continue;
- }
- List<Block> thatGotoCmdLabelTargets = new List<Block>();
- List<string> thatGotoCmdLabelNames = new List<string>();
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- thatGotoCmdLabelTargets.Add(blockMap[target]);
- thatGotoCmdLabelNames.Add(blockMap[target].Label);
- }
- blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, thatGotoCmdLabelNames, thatGotoCmdLabelTargets);
- }
- this.thatAction = new CodeExpr(thatLocVars, thatBlocks);
-
- {
- VariableCollector collector = new VariableCollector();
- collector.Visit(codeExpr);
- this.actionUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
- }
-
- List<Variable> modifiedVars = new List<Variable>();
- foreach (Block block in codeExpr.Blocks)
- {
- block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars));
- }
- this.modifiedGlobalVars = new HashSet<Variable>(modifiedVars.Where(x => x is GlobalVariable));
-
- {
- VariableCollector collector = new VariableCollector();
- this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd));
- this.gateUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
- }
- }
- }
-
- public class SharedVariableInfo
- {
- public int introLayerNum;
- public int hideLayerNum;
-
- public SharedVariableInfo(int introLayerNum, int hideLayerNum)
- {
- this.introLayerNum = introLayerNum;
- this.hideLayerNum = hideLayerNum;
- }
- }
-
- public class LayerEraser : ReadOnlyVisitor
- {
- private QKeyValue RemoveLayerAttribute(QKeyValue iter)
- {
- if (iter == null) return null;
- iter.Next = RemoveLayerAttribute(iter.Next);
- return (iter.Key == "layer") ? iter.Next : iter;
- }
-
- public override Variable VisitVariable(Variable node)
- {
- node.Attributes = RemoveLayerAttribute(node.Attributes);
- return base.VisitVariable(node);
- }
-
- public override Procedure VisitProcedure(Procedure node)
- {
- node.Attributes = RemoveLayerAttribute(node.Attributes);
- return base.VisitProcedure(node);
- }
-
- public override Implementation VisitImplementation(Implementation node)
- {
- node.Attributes = RemoveLayerAttribute(node.Attributes);
- return base.VisitImplementation(node);
- }
-
- public override Requires VisitRequires(Requires node)
- {
- node.Attributes = RemoveLayerAttribute(node.Attributes);
- return base.VisitRequires(node);
- }
-
- public override Ensures VisitEnsures(Ensures node)
- {
- node.Attributes = RemoveLayerAttribute(node.Attributes);
- return base.VisitEnsures(node);
- }
-
- public override Cmd VisitAssertCmd(AssertCmd node)
- {
- node.Attributes = RemoveLayerAttribute(node.Attributes);
- return base.VisitAssertCmd(node);
- }
- }
-
- public class MoverTypeChecker : ReadOnlyVisitor
- {
- CheckingContext checkingContext;
- public int errorCount;
- public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;
- Procedure enclosingProc;
- Implementation enclosingImpl;
- public Dictionary<Procedure, ActionInfo> procToActionInfo;
- public Program program;
- bool canAccessSharedVars;
- bool canAccessGhostVars;
- int minLayerNum;
- int maxLayerNum;
- public Dictionary<Absy, HashSet<int>> absyToLayerNums;
- HashSet<Variable> ghostVars;
- public int leastUnimplementedLayerNum;
-
- private static List<int> FindLayers(QKeyValue kv)
- {
- HashSet<int> attrs = new HashSet<int>();
- for (; kv != null; kv = kv.Next)
- {
- if (kv.Key != "layer") continue;
- foreach (var o in kv.Params)
- {
- Expr e = o as Expr;
- if (e == null) continue;
- LiteralExpr l = e as LiteralExpr;
- if (l != null && l.isBigNum)
- attrs.Add(l.asBigNum.ToIntSafe);
- }
- }
- List<int> layers = attrs.ToList();
- layers.Sort();
- return layers;
- }
-
- private static MoverType GetMoverType(Ensures e)
- {
- if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
- return MoverType.Atomic;
- if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
- return MoverType.Right;
- if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
- return MoverType.Left;
- if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
- return MoverType.Both;
- return MoverType.Top;
- }
-
- public MoverTypeChecker(Program program)
- {
- this.ghostVars = new HashSet<Variable>();
- this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
- this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
- this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
- this.errorCount = 0;
- this.checkingContext = new CheckingContext(null);
- this.program = program;
- this.enclosingProc = null;
- this.enclosingImpl = null;
- this.canAccessSharedVars = false;
- this.canAccessGhostVars = false;
- this.minLayerNum = int.MaxValue;
- this.maxLayerNum = -1;
- this.leastUnimplementedLayerNum = int.MaxValue;
- foreach (var g in program.GlobalVariables)
- {
- List<int> layerNums = FindLayers(g.Attributes);
- if (layerNums.Count == 0)
- {
- // Cannot access atomic actions
- }
- else if (layerNums.Count == 1)
- {
- this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue);
- }
- else if (layerNums.Count == 2)
- {
- this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]);
- }
- else
- {
- Error(g, "Too many layer numbers");
- }
- }
- }
-
- private HashSet<int> allCreatedLayerNums;
- public IEnumerable<int> AllCreatedLayerNums
- {
- get
- {
- if (allCreatedLayerNums == null)
- {
- allCreatedLayerNums = new HashSet<int>();
- foreach (ActionInfo actionInfo in procToActionInfo.Values)
- {
- allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);
- }
- }
- return allCreatedLayerNums;
- }
- }
-
- public void TypeCheck()
- {
- foreach (var proc in program.Procedures)
- {
- if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
-
- int createdAtLayerNum; // must be initialized by the following code, otherwise it is an error
- int availableUptoLayerNum = int.MaxValue;
- List<int> attrs = FindLayers(proc.Attributes);
- if (attrs.Count == 1)
- {
- createdAtLayerNum = attrs[0];
- }
- else if (attrs.Count == 2)
- {
- createdAtLayerNum = attrs[0];
- availableUptoLayerNum = attrs[1];
- }
- else
- {
- Error(proc, "Incorrect number of layers");
- continue;
- }
- if (availableUptoLayerNum <= createdAtLayerNum)
- {
- Error(proc, "Creation layer number must be less than the available upto layer number");
- continue;
- }
- foreach (Ensures e in proc.Ensures)
- {
- MoverType moverType = GetMoverType(e);
- if (moverType == MoverType.Top) continue;
- CodeExpr codeExpr = e.Condition as CodeExpr;
- if (codeExpr == null)
- {
- Error(e, "An atomic action must be a CodeExpr");
- continue;
- }
- if (procToActionInfo.ContainsKey(proc))
- {
- Error(proc, "A procedure can have at most one atomic action");
- continue;
- }
-
- minLayerNum = int.MaxValue;
- maxLayerNum = -1;
- canAccessSharedVars = true;
- enclosingProc = proc;
- enclosingImpl = null;
- base.VisitEnsures(e);
- canAccessSharedVars = false;
- if (maxLayerNum > createdAtLayerNum)
- {
- Error(e, "A variable being accessed is introduced after this action is created");
- }
- else if (availableUptoLayerNum > minLayerNum)
- {
- Error(e, "A variable being accessed is hidden before this action becomes unavailable");
- }
- else
- {
- procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
- }
- }
- if (errorCount > 0) continue;
- if (!procToActionInfo.ContainsKey(proc))
- {
- procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum);
- }
- }
- if (errorCount > 0) return;
- foreach (var impl in program.Implementations)
- {
- if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
- procToActionInfo[impl.Proc].hasImplementation = true;
- }
- foreach (var proc in procToActionInfo.Keys)
- {
- ActionInfo actionInfo = procToActionInfo[proc];
- if (actionInfo.isExtern && actionInfo.hasImplementation)
- {
- Error(proc, "Extern procedure cannot have an implementation");
- continue;
- }
- if (actionInfo.isExtern || actionInfo.hasImplementation) continue;
- if (leastUnimplementedLayerNum == int.MaxValue)
- {
- leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;
- }
- else if (leastUnimplementedLayerNum != actionInfo.createdAtLayerNum)
- {
- Error(proc, "All unimplemented atomic actions must be created at the same layer");
- }
- }
- foreach (var g in this.globalVarToSharedVarInfo.Keys)
- {
- var info = globalVarToSharedVarInfo[g];
- if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))
- {
- Error(g, "Variable must be introduced with creation of some atomic action");
- }
- if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))
- {
- Error(g, "Variable must be hidden with creation of some atomic action");
- }
- }
- if (errorCount > 0) return;
- this.VisitProgram(program);
- foreach (Procedure proc in program.Procedures)
- {
- if (procToActionInfo.ContainsKey(proc)) continue;
- foreach (var ie in proc.Modifies)
- {
- if (!SharedVariables.Contains(ie.Decl)) continue;
- Error(proc, "A ghost procedure must not modify a global variable with layer annotation");
- }
- }
- if (errorCount > 0) return;
- YieldTypeChecker.PerformYieldSafeCheck(this);
- new LayerEraser().VisitProgram(program);
- }
-
- public IEnumerable<Variable> SharedVariables
- {
- get { return this.globalVarToSharedVarInfo.Keys; }
- }
-
- public override Implementation VisitImplementation(Implementation node)
- {
- if (!procToActionInfo.ContainsKey(node.Proc))
- {
- return node;
- }
- this.enclosingImpl = node;
- this.enclosingProc = null;
- ghostVars = new HashSet<Variable>();
- foreach (Variable v in node.LocVars)
- {
- if (QKeyValue.FindBoolAttribute(v.Attributes, "ghost"))
- {
- ghostVars.Add(v);
- }
- }
- return base.VisitImplementation(node);
- }
-
- public override Procedure VisitProcedure(Procedure node)
- {
- if (!procToActionInfo.ContainsKey(node))
- {
- return node;
- }
- this.enclosingProc = node;
- this.enclosingImpl = null;
- return base.VisitProcedure(node);
- }
-
- public override Cmd VisitCallCmd(CallCmd node)
- {
- int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
- if (procToActionInfo.ContainsKey(node.Proc))
- {
- ActionInfo actionInfo = procToActionInfo[node.Proc];
- if (node.IsAsync && actionInfo is AtomicActionInfo)
- {
- Error(node, "Target of async call cannot be an atomic action");
- }
- int calleeLayerNum = procToActionInfo[node.Proc].createdAtLayerNum;
- if (enclosingProcLayerNum < calleeLayerNum ||
- (enclosingProcLayerNum == calleeLayerNum && actionInfo is AtomicActionInfo))
- {
- Error(node, "The layer of the caller must be greater than the layer of the callee");
- }
- else if (enclosingProcLayerNum == calleeLayerNum && enclosingImpl.OutParams.Count > 0)
- {
- HashSet<Variable> outParams = new HashSet<Variable>(enclosingImpl.OutParams);
- foreach (var x in node.Outs)
- {
- if (x.Decl is GlobalVariable)
- {
- Error(node, "A global variable cannot be used as output argument for this call");
- }
- else if (outParams.Contains(x.Decl))
- {
- Error(node, "An output variable of the enclosing implementation cannot be used as output argument for this call");
- }
- }
- }
- if (actionInfo.availableUptoLayerNum < enclosingProcLayerNum)
- {
- Error(node, "The callee is not available in the caller procedure");
- }
- return base.VisitCallCmd(node);
- }
- else
- {
- foreach (var ie in node.Outs)
- {
- if (ghostVars.Contains(ie.Decl)) continue;
- Error(node, "The output of a ghost procedure must be assigned to a ghost variable");
- }
- bool savedCanAccessSharedVars = canAccessSharedVars;
- bool savedCanAccessAuxVars = canAccessGhostVars;
- canAccessSharedVars = true;
- canAccessGhostVars = true;
- var retVal = base.VisitCallCmd(node);
- canAccessSharedVars = savedCanAccessSharedVars;
- canAccessGhostVars = savedCanAccessAuxVars;
- return retVal;
- }
- }
-
- public override Cmd VisitParCallCmd(ParCallCmd node)
- {
- int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
- bool isLeftMover = true;
- bool isRightMover = true;
- int maxCalleeLayerNum = 0;
- int atomicActionCalleeLayerNum = 0;
- int numAtomicActions = 0;
- foreach (CallCmd iter in node.CallCmds)
- {
- ActionInfo actionInfo = procToActionInfo[iter.Proc];
- isLeftMover = isLeftMover && actionInfo.IsLeftMover;
- isRightMover = isRightMover && actionInfo.IsRightMover;
- if (actionInfo.createdAtLayerNum > maxCalleeLayerNum)
- {
- maxCalleeLayerNum = actionInfo.createdAtLayerNum;
- }
- if (actionInfo is AtomicActionInfo)
- {
- numAtomicActions++;
- if (atomicActionCalleeLayerNum == 0)
- {
- atomicActionCalleeLayerNum = actionInfo.createdAtLayerNum;
- }
- else if (atomicActionCalleeLayerNum != actionInfo.createdAtLayerNum)
- {
- Error(node, "All atomic actions must be introduced at the same layer");
- }
- }
- }
- if (numAtomicActions > 1 && !isLeftMover && !isRightMover)
- {
- Error(node, "The atomic actions in the parallel call must be all right movers or all left movers");
- }
- if (0 < atomicActionCalleeLayerNum && atomicActionCalleeLayerNum < maxCalleeLayerNum)
- {
- Error(node, "Atomic actions must be introduced at the highest layer");
- }
- return base.VisitParCallCmd(node);
- }
-
- public override Cmd VisitAssignCmd(AssignCmd node)
- {
- Contract.Ensures(Contract.Result<Cmd>() == node);
- for (int i = 0; i < node.Lhss.Count; ++i)
- {
- bool savedCanAccessSharedVars = canAccessSharedVars;
- bool savedCanAccessAuxVars = canAccessGhostVars;
- Variable v = node.Lhss[i].DeepAssignedVariable;
- if (v is LocalVariable && ghostVars.Contains(v))
- {
- canAccessSharedVars = true;
- canAccessGhostVars = true;
- }
- this.Visit(node.Lhss[i]);
- this.Visit(node.Rhss[i]);
- canAccessSharedVars = savedCanAccessSharedVars;
- canAccessGhostVars = savedCanAccessAuxVars;
- }
- return node;
- }
-
- public override Expr VisitIdentifierExpr(IdentifierExpr node)
- {
- if (node.Decl is GlobalVariable)
- {
- if (!canAccessSharedVars)
- {
- Error(node, "Shared variable can be accessed only in atomic actions or specifications");
- }
- else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl))
- {
- if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum)
- {
- minLayerNum = this.globalVarToSharedVarInfo[node.Decl].hideLayerNum;
- }
- if (this.globalVarToSharedVarInfo[node.Decl].introLayerNum > maxLayerNum)
- {
- maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum;
- }
- }
- else
- {
- Error(node, "Accessed shared variable must have layer annotation");
- }
- }
- else if (node.Decl is LocalVariable && ghostVars.Contains(node.Decl) && !canAccessGhostVars)
- {
- Error(node, "Ghost variable can be accessed only in assertions");
- }
-
- return base.VisitIdentifierExpr(node);
- }
-
- public override Ensures VisitEnsures(Ensures ensures)
- {
- minLayerNum = int.MaxValue;
- maxLayerNum = -1;
- canAccessSharedVars = true;
- Ensures ret = base.VisitEnsures(ensures);
- canAccessSharedVars = false;
- ActionInfo actionInfo = procToActionInfo[enclosingProc];
- AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
- if (atomicActionInfo != null && atomicActionInfo.ensures == ensures)
- {
- // This case has already been checked
- }
- else
- {
- CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum);
- }
- return ret;
- }
-
- public override Requires VisitRequires(Requires requires)
- {
- minLayerNum = int.MaxValue;
- maxLayerNum = -1;
- canAccessSharedVars = true;
- Requires ret = base.VisitRequires(requires);
- canAccessSharedVars = false;
- CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);
- return ret;
- }
-
- public override Cmd VisitAssertCmd(AssertCmd node)
- {
- if (enclosingImpl == null)
- return base.VisitAssertCmd(node);
- minLayerNum = int.MaxValue;
- maxLayerNum = -1;
- canAccessSharedVars = true;
- canAccessGhostVars = true;
- Cmd ret = base.VisitAssertCmd(node);
- canAccessGhostVars = false;
- canAccessSharedVars = false;
- CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);
- return ret;
- }
-
- private void CheckAndAddLayers(Absy node, QKeyValue attributes, int enclosingProcLayerNum)
- {
- List<int> attrs = FindLayers(attributes);
- if (attrs.Count == 0)
- {
- Error(node, "layer not present");
- return;
- }
- absyToLayerNums[node] = new HashSet<int>();
- foreach (int layerNum in attrs)
- {
- if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum))
- {
- Error(node, "Illegal layer number");
- }
- else if (layerNum > enclosingProcLayerNum)
- {
- Error(node, "The layer cannot be greater than the layer of enclosing procedure");
- }
- else if (maxLayerNum < layerNum && layerNum <= minLayerNum)
- {
- absyToLayerNums[node].Add(layerNum);
- }
- else
- {
- Error(node, string.Format("A variable being accessed in this specification is unavailable at layer {0}", layerNum));
- }
- }
- }
-
- public void Error(Absy node, string message)
- {
- checkingContext.Error(node, message);
- errorCount++;
- }
- }
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie
+{
+ public enum MoverType
+ {
+ Top,
+ Atomic,
+ Right,
+ Left,
+ Both
+ }
+
+ public class ActionInfo
+ {
+ public Procedure proc;
+ public int createdAtLayerNum;
+ public int availableUptoLayerNum;
+ public bool hasImplementation;
+ public bool isExtern;
+
+ public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum)
+ {
+ this.proc = proc;
+ this.createdAtLayerNum = createdAtLayerNum;
+ this.availableUptoLayerNum = availableUptoLayerNum;
+ this.hasImplementation = false;
+ this.isExtern = QKeyValue.FindBoolAttribute(proc.Attributes, "extern");
+ }
+
+ public virtual bool IsRightMover
+ {
+ get { return true; }
+ }
+
+ public virtual bool IsLeftMover
+ {
+ get { return true; }
+ }
+ }
+
+ public class AtomicActionInfo : ActionInfo
+ {
+ public Ensures ensures;
+ public MoverType moverType;
+ public List<AssertCmd> thisGate;
+ public CodeExpr thisAction;
+ public List<Variable> thisInParams;
+ public List<Variable> thisOutParams;
+ public List<AssertCmd> thatGate;
+ public CodeExpr thatAction;
+ public List<Variable> thatInParams;
+ public List<Variable> thatOutParams;
+ public HashSet<Variable> actionUsedGlobalVars;
+ public HashSet<Variable> modifiedGlobalVars;
+ public HashSet<Variable> gateUsedGlobalVars;
+ public bool hasAssumeCmd;
+
+ public bool CommutesWith(AtomicActionInfo actionInfo)
+ {
+ if (this.modifiedGlobalVars.Intersect(actionInfo.actionUsedGlobalVars).Count() > 0)
+ return false;
+ if (this.actionUsedGlobalVars.Intersect(actionInfo.modifiedGlobalVars).Count() > 0)
+ return false;
+ return true;
+ }
+
+ public override bool IsRightMover
+ {
+ get { return moverType == MoverType.Right || moverType == MoverType.Both; }
+ }
+
+ public override bool IsLeftMover
+ {
+ get { return moverType == MoverType.Left || moverType == MoverType.Both; }
+ }
+
+ public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int layerNum, int availableUptoLayerNum)
+ : base(proc, layerNum, availableUptoLayerNum)
+ {
+ CodeExpr codeExpr = ensures.Condition as CodeExpr;
+ this.ensures = ensures;
+ this.moverType = moverType;
+ this.thisGate = new List<AssertCmd>();
+ this.thisAction = codeExpr;
+ this.thisInParams = new List<Variable>();
+ this.thisOutParams = new List<Variable>();
+ this.thatGate = new List<AssertCmd>();
+ this.thatInParams = new List<Variable>();
+ this.thatOutParams = new List<Variable>();
+ this.hasAssumeCmd = false;
+
+ foreach (Block block in codeExpr.Blocks)
+ {
+ block.Cmds.ForEach(x => this.hasAssumeCmd = this.hasAssumeCmd || x is AssumeCmd);
+ }
+
+ var cmds = thisAction.Blocks[0].Cmds;
+ for (int i = 0; i < cmds.Count; i++)
+ {
+ AssertCmd assertCmd = cmds[i] as AssertCmd;
+ if (assertCmd == null) break;
+ thisGate.Add(assertCmd);
+ cmds[i] = new AssumeCmd(assertCmd.tok, Expr.True);
+ }
+
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ foreach (Variable x in proc.InParams)
+ {
+ this.thisInParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes);
+ this.thatInParams.Add(y);
+ map[x] = Expr.Ident(y);
+ }
+ foreach (Variable x in proc.OutParams)
+ {
+ this.thisOutParams.Add(x);
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes);
+ this.thatOutParams.Add(y);
+ map[x] = Expr.Ident(y);
+ }
+ List<Variable> thatLocVars = new List<Variable>();
+ foreach (Variable x in thisAction.LocVars)
+ {
+ Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);
+ map[x] = Expr.Ident(y);
+ thatLocVars.Add(y);
+ }
+ Contract.Assume(proc.TypeParameters.Count == 0);
+ Substitution subst = Substituter.SubstitutionFromHashtable(map);
+ foreach (AssertCmd assertCmd in thisGate)
+ {
+ thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd));
+ }
+ Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
+ List<Block> thatBlocks = new List<Block>();
+ foreach (Block block in thisAction.Blocks)
+ {
+ List<Cmd> otherCmds = new List<Cmd>();
+ foreach (Cmd cmd in block.Cmds)
+ {
+ otherCmds.Add(Substituter.Apply(subst, cmd));
+ }
+ Block thatBlock = new Block();
+ thatBlock.Cmds = otherCmds;
+ thatBlock.Label = "that_" + block.Label;
+ block.Label = "this_" + block.Label;
+ thatBlocks.Add(thatBlock);
+ blockMap[block] = thatBlock;
+ if (block.TransferCmd is GotoCmd)
+ {
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ for (int i = 0; i < gotoCmd.labelNames.Count; i++)
+ {
+ gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i];
+ }
+ }
+ }
+ foreach (Block block in thisAction.Blocks)
+ {
+ if (block.TransferCmd is ReturnExprCmd)
+ {
+ block.TransferCmd = new ReturnCmd(block.TransferCmd.tok);
+ blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok);
+ continue;
+ }
+ List<Block> thatGotoCmdLabelTargets = new List<Block>();
+ List<string> thatGotoCmdLabelNames = new List<string>();
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ foreach (Block target in gotoCmd.labelTargets)
+ {
+ thatGotoCmdLabelTargets.Add(blockMap[target]);
+ thatGotoCmdLabelNames.Add(blockMap[target].Label);
+ }
+ blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, thatGotoCmdLabelNames, thatGotoCmdLabelTargets);
+ }
+ this.thatAction = new CodeExpr(thatLocVars, thatBlocks);
+
+ {
+ VariableCollector collector = new VariableCollector();
+ collector.Visit(codeExpr);
+ this.actionUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
+ }
+
+ List<Variable> modifiedVars = new List<Variable>();
+ foreach (Block block in codeExpr.Blocks)
+ {
+ block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars));
+ }
+ this.modifiedGlobalVars = new HashSet<Variable>(modifiedVars.Where(x => x is GlobalVariable));
+
+ {
+ VariableCollector collector = new VariableCollector();
+ this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd));
+ this.gateUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
+ }
+ }
+ }
+
+ public class SharedVariableInfo
+ {
+ public int introLayerNum;
+ public int hideLayerNum;
+
+ public SharedVariableInfo(int introLayerNum, int hideLayerNum)
+ {
+ this.introLayerNum = introLayerNum;
+ this.hideLayerNum = hideLayerNum;
+ }
+ }
+
+ public class LayerEraser : ReadOnlyVisitor
+ {
+ private QKeyValue RemoveLayerAttribute(QKeyValue iter)
+ {
+ if (iter == null) return null;
+ iter.Next = RemoveLayerAttribute(iter.Next);
+ return (iter.Key == "layer") ? iter.Next : iter;
+ }
+
+ public override Variable VisitVariable(Variable node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitVariable(node);
+ }
+
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitProcedure(node);
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitImplementation(node);
+ }
+
+ public override Requires VisitRequires(Requires node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitRequires(node);
+ }
+
+ public override Ensures VisitEnsures(Ensures node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitEnsures(node);
+ }
+
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ node.Attributes = RemoveLayerAttribute(node.Attributes);
+ return base.VisitAssertCmd(node);
+ }
+ }
+
+ public class MoverTypeChecker : ReadOnlyVisitor
+ {
+ CheckingContext checkingContext;
+ public int errorCount;
+ public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;
+ Procedure enclosingProc;
+ Implementation enclosingImpl;
+ public Dictionary<Procedure, ActionInfo> procToActionInfo;
+ public Program program;
+ bool canAccessSharedVars;
+ bool canAccessGhostVars;
+ int minLayerNum;
+ int maxLayerNum;
+ public Dictionary<Absy, HashSet<int>> absyToLayerNums;
+ HashSet<Variable> ghostVars;
+ public int leastUnimplementedLayerNum;
+
+ private static List<int> FindLayers(QKeyValue kv)
+ {
+ List<int> layers = new List<int>();
+ for (; kv != null; kv = kv.Next)
+ {
+ if (kv.Key != "layer") continue;
+ foreach (var o in kv.Params)
+ {
+ Expr e = o as Expr;
+ if (e == null) return null;
+ LiteralExpr l = e as LiteralExpr;
+ if (l == null) return null;
+ if (!l.isBigNum) return null;
+ layers.Add(l.asBigNum.ToIntSafe);
+ }
+ }
+ return layers;
+ }
+
+ private static MoverType GetMoverType(Ensures e)
+ {
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
+ return MoverType.Atomic;
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
+ return MoverType.Right;
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
+ return MoverType.Left;
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
+ return MoverType.Both;
+ return MoverType.Top;
+ }
+
+ public MoverTypeChecker(Program program)
+ {
+ this.ghostVars = new HashSet<Variable>();
+ this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();
+ this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();
+ this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+ this.errorCount = 0;
+ this.checkingContext = new CheckingContext(null);
+ this.program = program;
+ this.enclosingProc = null;
+ this.enclosingImpl = null;
+ this.canAccessSharedVars = false;
+ this.canAccessGhostVars = false;
+ this.minLayerNum = int.MaxValue;
+ this.maxLayerNum = -1;
+ this.leastUnimplementedLayerNum = int.MaxValue;
+ foreach (var g in program.GlobalVariables)
+ {
+ List<int> layerNums = FindLayers(g.Attributes);
+ if (layerNums.Count == 0)
+ {
+ // Cannot access atomic actions
+ }
+ else if (layerNums.Count == 1)
+ {
+ this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue);
+ }
+ else if (layerNums.Count == 2)
+ {
+ this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]);
+ }
+ else
+ {
+ Error(g, "Too many layer numbers");
+ }
+ }
+ }
+
+ private HashSet<int> allCreatedLayerNums;
+ public IEnumerable<int> AllCreatedLayerNums
+ {
+ get
+ {
+ if (allCreatedLayerNums == null)
+ {
+ allCreatedLayerNums = new HashSet<int>();
+ foreach (ActionInfo actionInfo in procToActionInfo.Values)
+ {
+ allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);
+ }
+ }
+ return allCreatedLayerNums;
+ }
+ }
+
+ public void TypeCheck()
+ {
+ foreach (var proc in program.Procedures)
+ {
+ if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
+
+ int createdAtLayerNum; // must be initialized by the following code, otherwise it is an error
+ int availableUptoLayerNum = int.MaxValue;
+ List<int> attrs = FindLayers(proc.Attributes);
+ if (attrs.Count == 1)
+ {
+ createdAtLayerNum = attrs[0];
+ }
+ else if (attrs.Count == 2)
+ {
+ createdAtLayerNum = attrs[0];
+ availableUptoLayerNum = attrs[1];
+ }
+ else
+ {
+ Error(proc, "Incorrect number of layers");
+ continue;
+ }
+ if (availableUptoLayerNum <= createdAtLayerNum)
+ {
+ Error(proc, "Creation layer number must be less than the available upto layer number");
+ continue;
+ }
+ foreach (Ensures e in proc.Ensures)
+ {
+ MoverType moverType = GetMoverType(e);
+ if (moverType == MoverType.Top) continue;
+ CodeExpr codeExpr = e.Condition as CodeExpr;
+ if (codeExpr == null)
+ {
+ Error(e, "An atomic action must be a CodeExpr");
+ continue;
+ }
+ if (procToActionInfo.ContainsKey(proc))
+ {
+ Error(proc, "A procedure can have at most one atomic action");
+ continue;
+ }
+
+ minLayerNum = int.MaxValue;
+ maxLayerNum = -1;
+ canAccessSharedVars = true;
+ enclosingProc = proc;
+ enclosingImpl = null;
+ base.VisitEnsures(e);
+ canAccessSharedVars = false;
+ if (maxLayerNum > createdAtLayerNum)
+ {
+ Error(e, "A variable being accessed is introduced after this action is created");
+ }
+ else if (availableUptoLayerNum > minLayerNum)
+ {
+ Error(e, "A variable being accessed is hidden before this action becomes unavailable");
+ }
+ else
+ {
+ procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);
+ }
+ }
+ if (errorCount > 0) continue;
+ if (!procToActionInfo.ContainsKey(proc))
+ {
+ procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum);
+ }
+ }
+ if (errorCount > 0) return;
+ foreach (var impl in program.Implementations)
+ {
+ if (!procToActionInfo.ContainsKey(impl.Proc)) continue;
+ procToActionInfo[impl.Proc].hasImplementation = true;
+ }
+ foreach (var proc in procToActionInfo.Keys)
+ {
+ ActionInfo actionInfo = procToActionInfo[proc];
+ if (actionInfo.isExtern && actionInfo.hasImplementation)
+ {
+ Error(proc, "Extern procedure cannot have an implementation");
+ continue;
+ }
+ if (actionInfo.isExtern || actionInfo.hasImplementation) continue;
+ if (leastUnimplementedLayerNum == int.MaxValue)
+ {
+ leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;
+ }
+ else if (leastUnimplementedLayerNum != actionInfo.createdAtLayerNum)
+ {
+ Error(proc, "All unimplemented atomic actions must be created at the same layer");
+ }
+ }
+ foreach (var g in this.globalVarToSharedVarInfo.Keys)
+ {
+ var info = globalVarToSharedVarInfo[g];
+ if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))
+ {
+ Error(g, "Variable must be introduced with creation of some atomic action");
+ }
+ if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))
+ {
+ Error(g, "Variable must be hidden with creation of some atomic action");
+ }
+ }
+ if (errorCount > 0) return;
+ this.VisitProgram(program);
+ foreach (Procedure proc in program.Procedures)
+ {
+ if (procToActionInfo.ContainsKey(proc)) continue;
+ foreach (var ie in proc.Modifies)
+ {
+ if (!SharedVariables.Contains(ie.Decl)) continue;
+ Error(proc, "A ghost procedure must not modify a global variable with layer annotation");
+ }
+ }
+ if (errorCount > 0) return;
+ YieldTypeChecker.PerformYieldSafeCheck(this);
+ new LayerEraser().VisitProgram(program);
+ }
+
+ public IEnumerable<Variable> SharedVariables
+ {
+ get { return this.globalVarToSharedVarInfo.Keys; }
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ if (!procToActionInfo.ContainsKey(node.Proc))
+ {
+ return node;
+ }
+ this.enclosingImpl = node;
+ this.enclosingProc = null;
+ ghostVars = new HashSet<Variable>();
+ foreach (Variable v in node.LocVars)
+ {
+ if (QKeyValue.FindBoolAttribute(v.Attributes, "ghost"))
+ {
+ ghostVars.Add(v);
+ }
+ }
+ return base.VisitImplementation(node);
+ }
+
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ if (!procToActionInfo.ContainsKey(node))
+ {
+ return node;
+ }
+ this.enclosingProc = node;
+ this.enclosingImpl = null;
+ return base.VisitProcedure(node);
+ }
+
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
+ if (procToActionInfo.ContainsKey(node.Proc))
+ {
+ ActionInfo actionInfo = procToActionInfo[node.Proc];
+ if (node.IsAsync && actionInfo is AtomicActionInfo)
+ {
+ Error(node, "Target of async call cannot be an atomic action");
+ }
+ int calleeLayerNum = procToActionInfo[node.Proc].createdAtLayerNum;
+ if (enclosingProcLayerNum < calleeLayerNum ||
+ (enclosingProcLayerNum == calleeLayerNum && actionInfo is AtomicActionInfo))
+ {
+ Error(node, "The layer of the caller must be greater than the layer of the callee");
+ }
+ else if (enclosingProcLayerNum == calleeLayerNum && enclosingImpl.OutParams.Count > 0)
+ {
+ HashSet<Variable> outParams = new HashSet<Variable>(enclosingImpl.OutParams);
+ foreach (var x in node.Outs)
+ {
+ if (x.Decl is GlobalVariable)
+ {
+ Error(node, "A global variable cannot be used as output argument for this call");
+ }
+ else if (outParams.Contains(x.Decl))
+ {
+ Error(node, "An output variable of the enclosing implementation cannot be used as output argument for this call");
+ }
+ }
+ }
+ if (actionInfo.availableUptoLayerNum < enclosingProcLayerNum)
+ {
+ Error(node, "The callee is not available in the caller procedure");
+ }
+ return base.VisitCallCmd(node);
+ }
+ else
+ {
+ foreach (var ie in node.Outs)
+ {
+ if (ghostVars.Contains(ie.Decl)) continue;
+ Error(node, "The output of a ghost procedure must be assigned to a ghost variable");
+ }
+ bool savedCanAccessSharedVars = canAccessSharedVars;
+ bool savedCanAccessAuxVars = canAccessGhostVars;
+ canAccessSharedVars = true;
+ canAccessGhostVars = true;
+ var retVal = base.VisitCallCmd(node);
+ canAccessSharedVars = savedCanAccessSharedVars;
+ canAccessGhostVars = savedCanAccessAuxVars;
+ return retVal;
+ }
+ }
+
+ public override Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ int enclosingProcLayerNum = procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
+ bool isLeftMover = true;
+ bool isRightMover = true;
+ int maxCalleeLayerNum = 0;
+ int atomicActionCalleeLayerNum = 0;
+ int numAtomicActions = 0;
+ foreach (CallCmd iter in node.CallCmds)
+ {
+ ActionInfo actionInfo = procToActionInfo[iter.Proc];
+ isLeftMover = isLeftMover && actionInfo.IsLeftMover;
+ isRightMover = isRightMover && actionInfo.IsRightMover;
+ if (actionInfo.createdAtLayerNum > maxCalleeLayerNum)
+ {
+ maxCalleeLayerNum = actionInfo.createdAtLayerNum;
+ }
+ if (actionInfo is AtomicActionInfo)
+ {
+ numAtomicActions++;
+ if (atomicActionCalleeLayerNum == 0)
+ {
+ atomicActionCalleeLayerNum = actionInfo.createdAtLayerNum;
+ }
+ else if (atomicActionCalleeLayerNum != actionInfo.createdAtLayerNum)
+ {
+ Error(node, "All atomic actions must be introduced at the same layer");
+ }
+ }
+ }
+ if (numAtomicActions > 1 && !isLeftMover && !isRightMover)
+ {
+ Error(node, "The atomic actions in the parallel call must be all right movers or all left movers");
+ }
+ if (0 < atomicActionCalleeLayerNum && atomicActionCalleeLayerNum < maxCalleeLayerNum)
+ {
+ Error(node, "Atomic actions must be introduced at the highest layer");
+ }
+ return base.VisitParCallCmd(node);
+ }
+
+ public override Cmd VisitAssignCmd(AssignCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ for (int i = 0; i < node.Lhss.Count; ++i)
+ {
+ bool savedCanAccessSharedVars = canAccessSharedVars;
+ bool savedCanAccessAuxVars = canAccessGhostVars;
+ Variable v = node.Lhss[i].DeepAssignedVariable;
+ if (v is LocalVariable && ghostVars.Contains(v))
+ {
+ canAccessSharedVars = true;
+ canAccessGhostVars = true;
+ }
+ this.Visit(node.Lhss[i]);
+ this.Visit(node.Rhss[i]);
+ canAccessSharedVars = savedCanAccessSharedVars;
+ canAccessGhostVars = savedCanAccessAuxVars;
+ }
+ return node;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ if (node.Decl is GlobalVariable)
+ {
+ if (!canAccessSharedVars)
+ {
+ Error(node, "Shared variable can be accessed only in atomic actions or specifications");
+ }
+ else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl))
+ {
+ if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum)
+ {
+ minLayerNum = this.globalVarToSharedVarInfo[node.Decl].hideLayerNum;
+ }
+ if (this.globalVarToSharedVarInfo[node.Decl].introLayerNum > maxLayerNum)
+ {
+ maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum;
+ }
+ }
+ else
+ {
+ Error(node, "Accessed shared variable must have layer annotation");
+ }
+ }
+ else if (node.Decl is LocalVariable && ghostVars.Contains(node.Decl) && !canAccessGhostVars)
+ {
+ Error(node, "Ghost variable can be accessed only in assertions");
+ }
+
+ return base.VisitIdentifierExpr(node);
+ }
+
+ public override Ensures VisitEnsures(Ensures ensures)
+ {
+ minLayerNum = int.MaxValue;
+ maxLayerNum = -1;
+ canAccessSharedVars = true;
+ Ensures ret = base.VisitEnsures(ensures);
+ canAccessSharedVars = false;
+ ActionInfo actionInfo = procToActionInfo[enclosingProc];
+ AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+ if (atomicActionInfo != null && atomicActionInfo.ensures == ensures)
+ {
+ // This case has already been checked
+ }
+ else
+ {
+ CheckAndAddLayers(ensures, ensures.Attributes, actionInfo.createdAtLayerNum);
+ }
+ return ret;
+ }
+
+ public override Requires VisitRequires(Requires requires)
+ {
+ minLayerNum = int.MaxValue;
+ maxLayerNum = -1;
+ canAccessSharedVars = true;
+ Requires ret = base.VisitRequires(requires);
+ canAccessSharedVars = false;
+ CheckAndAddLayers(requires, requires.Attributes, procToActionInfo[enclosingProc].createdAtLayerNum);
+ return ret;
+ }
+
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ if (enclosingImpl == null)
+ return base.VisitAssertCmd(node);
+ minLayerNum = int.MaxValue;
+ maxLayerNum = -1;
+ canAccessSharedVars = true;
+ canAccessGhostVars = true;
+ Cmd ret = base.VisitAssertCmd(node);
+ canAccessGhostVars = false;
+ canAccessSharedVars = false;
+ CheckAndAddLayers(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].createdAtLayerNum);
+ return ret;
+ }
+
+ private List<int> RemoveDuplicatesAndSort(List<int> attrs)
+ {
+ HashSet<int> layerSet = new HashSet<int>(attrs);
+ List<int> layers = new List<int>(layerSet);
+ layers.Sort();
+ return layers;
+ }
+
+ private void CheckAndAddLayers(Absy node, QKeyValue attributes, int enclosingProcLayerNum)
+ {
+ List<int> attrs = RemoveDuplicatesAndSort(FindLayers(attributes));
+ if (attrs.Count == 0)
+ {
+ Error(node, "layer not present");
+ return;
+ }
+ absyToLayerNums[node] = new HashSet<int>();
+ foreach (int layerNum in attrs)
+ {
+ if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum))
+ {
+ Error(node, "Illegal layer number");
+ }
+ else if (layerNum > enclosingProcLayerNum)
+ {
+ Error(node, "The layer cannot be greater than the layer of enclosing procedure");
+ }
+ else if (maxLayerNum < layerNum && layerNum <= minLayerNum)
+ {
+ absyToLayerNums[node].Add(layerNum);
+ }
+ else
+ {
+ Error(node, string.Format("A variable being accessed in this specification is unavailable at layer {0}", layerNum));
+ }
+ }
+ }
+
+ public void Error(Absy node, string message)
+ {
+ checkingContext.Error(node, message);
+ errorCount++;
+ }
+ }
} \ No newline at end of file
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 95884626..a698c8fd 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -1,363 +1,368 @@
-using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using Microsoft.Boogie;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie.GraphUtil;
-using System.Diagnostics;
-
-namespace Microsoft.Boogie
-{
- class YieldTypeChecker
- {
- static List<Tuple<int, int, int>> ASpec;
- static List<Tuple<int, int, int>> BSpec;
- static List<Tuple<int, int, int>> CSpec;
- static YieldTypeChecker()
- {
- // initial: 0, final: 1
- ASpec = new List<Tuple<int,int,int>>();
- ASpec.Add(new Tuple<int, int, int>(0, 'Y', 1));
- ASpec.Add(new Tuple<int, int, int>(1, 'Y', 1));
- ASpec.Add(new Tuple<int, int, int>(1, 'B', 1));
- ASpec.Add(new Tuple<int, int, int>(1, 'R', 1));
- ASpec.Add(new Tuple<int, int, int>(1, 'L', 1));
- ASpec.Add(new Tuple<int, int, int>(1, 'A', 1));
- ASpec.Add(new Tuple<int, int, int>(0, 'P', 0));
- ASpec.Add(new Tuple<int, int, int>(1, 'P', 1));
-
- // initial: 1, final: 0
- BSpec = new List<Tuple<int, int, int>>();
- BSpec.Add(new Tuple<int, int, int>(1, 'Y', 0));
- BSpec.Add(new Tuple<int, int, int>(1, 'Y', 1));
- BSpec.Add(new Tuple<int, int, int>(1, 'B', 1));
- BSpec.Add(new Tuple<int, int, int>(1, 'R', 1));
- BSpec.Add(new Tuple<int, int, int>(1, 'L', 1));
- BSpec.Add(new Tuple<int, int, int>(1, 'A', 1));
- BSpec.Add(new Tuple<int, int, int>(0, 'P', 0));
- BSpec.Add(new Tuple<int, int, int>(1, 'P', 1));
-
- // initial: {0, 1}, final: {0, 1}
- CSpec = new List<Tuple<int,int,int>>();
- CSpec.Add(new Tuple<int, int, int>(0, 'B', 0));
- CSpec.Add(new Tuple<int, int, int>(0, 'R', 0));
- CSpec.Add(new Tuple<int, int, int>(0, 'Y', 0));
- CSpec.Add(new Tuple<int, int, int>(0, 'B', 1));
- CSpec.Add(new Tuple<int, int, int>(0, 'R', 1));
- CSpec.Add(new Tuple<int, int, int>(0, 'L', 1));
- CSpec.Add(new Tuple<int, int, int>(0, 'A', 1));
- CSpec.Add(new Tuple<int, int, int>(1, 'B', 1));
- CSpec.Add(new Tuple<int, int, int>(1, 'L', 1));
- CSpec.Add(new Tuple<int, int, int>(1, 'Y', 0));
- CSpec.Add(new Tuple<int, int, int>(0, 'P', 0));
- CSpec.Add(new Tuple<int, int, int>(1, 'P', 1));
- }
-
- private void IsYieldTypeSafe()
- {
- List<Tuple<int, int, int>> implEdges = new List<Tuple<int, int, int>>();
- foreach (Tuple<int, int> e in edgeLabels.Keys)
- {
- implEdges.Add(new Tuple<int, int, int>(e.Item1, edgeLabels[e], e.Item2));
- }
- //Console.WriteLine(PrintGraph(impl, implEdges, initialState, finalStates));
- ASpecCheck(implEdges);
- BSpecCheck(implEdges);
- CSpecCheck(implEdges);
- }
-
- private void ASpecCheck(List<Tuple<int, int, int>> implEdges)
- {
- Dictionary<int, HashSet<int>> initialConstraints = new Dictionary<int, HashSet<int>>();
- initialConstraints[initialState] = new HashSet<int>(new int[] { 0 });
- foreach (var finalState in finalStates)
- {
- initialConstraints[finalState] = new HashSet<int>(new int[] { 1 });
- }
- SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, ASpec, initialConstraints);
- Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
- if (simulationRelation[initialState].Count == 0)
- {
- moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));
- }
- }
-
- private void BSpecCheck(List<Tuple<int, int, int>> implEdges)
- {
- Dictionary<int, HashSet<int>> initialConstraints = new Dictionary<int, HashSet<int>>();
- initialConstraints[initialState] = new HashSet<int>(new int[] { 1 });
- foreach (var finalState in finalStates)
- {
- initialConstraints[finalState] = new HashSet<int>(new int[] { 0 });
- }
- SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, BSpec, initialConstraints);
- Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
- if (simulationRelation[initialState].Count == 0)
- {
- moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));
- }
- }
-
- private void CSpecCheck(List<Tuple<int, int, int>> implEdges)
- {
- Dictionary<int, HashSet<int>> initialConstraints = new Dictionary<int, HashSet<int>>();
- foreach (Block block in loopHeaders)
- {
- if (!IsTerminatingLoopHeader(block))
- {
- initialConstraints[absyToNode[block]] = new HashSet<int>(new int[] { 0 });
- }
- }
- SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, CSpec, initialConstraints);
- Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
- if (simulationRelation[initialState].Count == 0)
- {
- moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));
- }
- }
-
- private bool IsTerminatingLoopHeader(Block block)
- {
- foreach (Cmd cmd in block.Cmds)
- {
- AssertCmd assertCmd = cmd as AssertCmd;
- if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum))
- {
- return true;
- }
- }
- return false;
- }
-
- public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)
- {
- foreach (var impl in moverTypeChecker.program.Implementations)
- {
- if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
- impl.PruneUnreachableBlocks();
- Graph<Block> implGraph = Program.GraphFromImpl(impl);
- implGraph.ComputeLoops();
- int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
- foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
- {
- if (layerNum > specLayerNum) continue;
- YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);
- }
- }
- }
-
- int stateCounter;
- MoverTypeChecker moverTypeChecker;
- Implementation impl;
- int currLayerNum;
- Dictionary<Absy, int> absyToNode;
- Dictionary<int, Absy> nodeToAbsy;
- int initialState;
- HashSet<int> finalStates;
- Dictionary<Tuple<int, int>, int> edgeLabels;
- IEnumerable<Block> loopHeaders;
-
- private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
- {
- this.moverTypeChecker = moverTypeChecker;
- this.impl = impl;
- this.currLayerNum = currLayerNum;
- this.loopHeaders = loopHeaders;
- this.stateCounter = 0;
- this.absyToNode = new Dictionary<Absy, int>();
- this.initialState = 0;
- this.finalStates = new HashSet<int>();
- this.edgeLabels = new Dictionary<Tuple<int, int>, int>();
-
- foreach (Block block in impl.Blocks)
- {
- absyToNode[block] = stateCounter;
- stateCounter++;
- foreach (Cmd cmd in block.Cmds)
- {
- absyToNode[cmd] = stateCounter;
- stateCounter++;
- }
- absyToNode[block.TransferCmd] = stateCounter;
- stateCounter++;
- if (block.TransferCmd is ReturnCmd)
- {
- finalStates.Add(absyToNode[block.TransferCmd]);
- }
- }
- foreach (Block block in impl.Blocks)
- {
- Absy blockEntry = block.Cmds.Count == 0 ? (Absy)block.TransferCmd : (Absy)block.Cmds[0];
- edgeLabels[new Tuple<int, int>(absyToNode[block], absyToNode[blockEntry])] = 'P';
-
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- if (gotoCmd == null) continue;
- foreach (Block successor in gotoCmd.labelTargets)
- {
- edgeLabels[new Tuple<int, int>(absyToNode[gotoCmd], absyToNode[successor])] = 'P';
- }
- }
-
- this.nodeToAbsy = new Dictionary<int, Absy>();
- foreach (KeyValuePair<Absy, int> state in absyToNode)
- {
- this.nodeToAbsy[state.Value] = state.Key;
- }
-
- ComputeGraph();
- IsYieldTypeSafe();
- }
-
- private void ComputeGraph()
- {
- foreach (Block block in impl.Blocks)
- {
- for (int i = 0; i < block.Cmds.Count; i++)
- {
- Cmd cmd = block.Cmds[i];
- int curr = absyToNode[cmd];
- int next = (i + 1 == block.Cmds.Count) ? absyToNode[block.TransferCmd] : absyToNode[block.Cmds[i + 1]];
- Tuple<int, int> edge = new Tuple<int, int>(curr, next);
- if (cmd is CallCmd)
- {
- CallCmd callCmd = cmd as CallCmd;
- if (callCmd.IsAsync)
- {
- ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
- if (currLayerNum <= actionInfo.createdAtLayerNum)
- edgeLabels[edge] = 'L';
- else
- edgeLabels[edge] = 'B';
- }
- else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
- {
- edgeLabels[edge] = 'P';
- }
- else
- {
- MoverType moverType;
- ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
- if (actionInfo.createdAtLayerNum >= currLayerNum)
- {
- moverType = MoverType.Top;
- }
- else
- {
- AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
- if (atomicActionInfo == null)
- moverType = MoverType.Both;
- else
- moverType = atomicActionInfo.moverType;
- }
- switch (moverType)
- {
- case MoverType.Atomic:
- edgeLabels[edge] = 'A';
- break;
- case MoverType.Both:
- edgeLabels[edge] = 'B';
- break;
- case MoverType.Left:
- edgeLabels[edge] = 'L';
- break;
- case MoverType.Right:
- edgeLabels[edge] = 'R';
- break;
- case MoverType.Top:
- edgeLabels[edge] = 'Y';
- break;
- }
- }
- }
- else if (cmd is ParCallCmd)
- {
- ParCallCmd parCallCmd = cmd as ParCallCmd;
- bool isYield = false;
- bool isRightMover = true;
- bool isLeftMover = true;
- foreach (CallCmd callCmd in parCallCmd.CallCmds)
- {
- if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum)
- {
- isYield = true;
- }
- }
- if (isYield)
- {
- edgeLabels[edge] = 'Y';
- }
- else
- {
- foreach (CallCmd callCmd in parCallCmd.CallCmds)
- {
- ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
- isRightMover = isRightMover && actionInfo.IsRightMover;
- isLeftMover = isLeftMover && actionInfo.IsLeftMover;
- }
- if (isLeftMover && isRightMover)
- {
- edgeLabels[edge] = 'B';
- }
- else if (isLeftMover)
- {
- edgeLabels[edge] = 'L';
- }
- else if (isRightMover)
- {
- edgeLabels[edge] = 'R';
- }
- else
- {
- Debug.Assert(parCallCmd.CallCmds.Count == 1);
- edgeLabels[edge] = 'A';
- }
- }
- }
- else if (cmd is YieldCmd)
- {
- edgeLabels[edge] = 'Y';
- }
- else
- {
- edgeLabels[edge] = 'P';
- }
- }
- }
- }
-
- private static string PrintGraph(Implementation impl, List<Tuple<int, int, int>> edges, int initialState, HashSet<int> finalStates)
- {
- var s = new StringBuilder();
- s.AppendLine("\nImplementation " + impl.Proc.Name + " digraph G {");
- foreach (var e in edges)
- {
- string label = "P";
- switch (e.Item2)
- {
- case 'P': label = "P"; break;
- case 'Y': label = "Y"; break;
- case 'B': label = "B"; break;
- case 'R': label = "R"; break;
- case 'L': label = "L"; break;
- case 'A': label = "A"; break;
- default: Debug.Assert(false); break;
- }
- s.AppendLine(" \"" + e.Item1.ToString() + "\" -- " + label + " --> " + " \"" + e.Item3.ToString() + "\";");
- }
- s.AppendLine("}");
- s.AppendLine("Initial state: " + initialState);
- s.Append("Final states: ");
- bool first = true;
- foreach (int finalState in finalStates)
- {
- s.Append((first ? "" : ", ") + finalState);
- first = false;
- }
- s.AppendLine();
- return s.ToString();
- }
- }
-}
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie.AbstractInterpretation;
+using Microsoft.Boogie.GraphUtil;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie
+{
+ class YieldTypeChecker
+ {
+ static List<Tuple<int, int, int>> ASpec;
+ static List<Tuple<int, int, int>> BSpec;
+ static List<Tuple<int, int, int>> CSpec;
+ static YieldTypeChecker()
+ {
+ // initial: 0, final: 1
+ ASpec = new List<Tuple<int,int,int>>();
+ ASpec.Add(new Tuple<int, int, int>(0, 'Y', 1));
+ ASpec.Add(new Tuple<int, int, int>(1, 'Y', 1));
+ ASpec.Add(new Tuple<int, int, int>(1, 'B', 1));
+ ASpec.Add(new Tuple<int, int, int>(1, 'R', 1));
+ ASpec.Add(new Tuple<int, int, int>(1, 'L', 1));
+ ASpec.Add(new Tuple<int, int, int>(1, 'A', 1));
+ ASpec.Add(new Tuple<int, int, int>(0, 'P', 0));
+ ASpec.Add(new Tuple<int, int, int>(1, 'P', 1));
+
+ // initial: 1, final: 0
+ BSpec = new List<Tuple<int, int, int>>();
+ BSpec.Add(new Tuple<int, int, int>(1, 'Y', 0));
+ BSpec.Add(new Tuple<int, int, int>(1, 'Y', 1));
+ BSpec.Add(new Tuple<int, int, int>(1, 'B', 1));
+ BSpec.Add(new Tuple<int, int, int>(1, 'R', 1));
+ BSpec.Add(new Tuple<int, int, int>(1, 'L', 1));
+ BSpec.Add(new Tuple<int, int, int>(1, 'A', 1));
+ BSpec.Add(new Tuple<int, int, int>(0, 'P', 0));
+ BSpec.Add(new Tuple<int, int, int>(1, 'P', 1));
+
+ // initial: {0, 1}, final: {0, 1}
+ CSpec = new List<Tuple<int,int,int>>();
+ CSpec.Add(new Tuple<int, int, int>(0, 'B', 0));
+ CSpec.Add(new Tuple<int, int, int>(0, 'R', 0));
+ CSpec.Add(new Tuple<int, int, int>(0, 'Y', 0));
+ CSpec.Add(new Tuple<int, int, int>(0, 'B', 1));
+ CSpec.Add(new Tuple<int, int, int>(0, 'R', 1));
+ CSpec.Add(new Tuple<int, int, int>(0, 'L', 1));
+ CSpec.Add(new Tuple<int, int, int>(0, 'A', 1));
+ CSpec.Add(new Tuple<int, int, int>(1, 'B', 1));
+ CSpec.Add(new Tuple<int, int, int>(1, 'L', 1));
+ CSpec.Add(new Tuple<int, int, int>(1, 'Y', 0));
+ CSpec.Add(new Tuple<int, int, int>(0, 'P', 0));
+ CSpec.Add(new Tuple<int, int, int>(1, 'P', 1));
+ }
+
+ private void IsYieldTypeSafe()
+ {
+ List<Tuple<int, int, int>> implEdges = new List<Tuple<int, int, int>>();
+ foreach (Tuple<int, int> e in edgeLabels.Keys)
+ {
+ implEdges.Add(new Tuple<int, int, int>(e.Item1, edgeLabels[e], e.Item2));
+ }
+ //Console.WriteLine(PrintGraph(impl, implEdges, initialState, finalStates));
+ ASpecCheck(implEdges);
+ BSpecCheck(implEdges);
+ CSpecCheck(implEdges);
+ }
+
+ private void ASpecCheck(List<Tuple<int, int, int>> implEdges)
+ {
+ Dictionary<int, HashSet<int>> initialConstraints = new Dictionary<int, HashSet<int>>();
+ initialConstraints[initialState] = new HashSet<int>(new int[] { 0 });
+ foreach (var finalState in finalStates)
+ {
+ initialConstraints[finalState] = new HashSet<int>(new int[] { 1 });
+ }
+ SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, ASpec, initialConstraints);
+ Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
+ if (simulationRelation[initialState].Count == 0)
+ {
+ moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check A at layer {1}. An action must be preceded by a yield.\n", impl.Name, currLayerNum));
+ }
+ }
+
+ private void BSpecCheck(List<Tuple<int, int, int>> implEdges)
+ {
+ Dictionary<int, HashSet<int>> initialConstraints = new Dictionary<int, HashSet<int>>();
+ initialConstraints[initialState] = new HashSet<int>(new int[] { 1 });
+ foreach (var finalState in finalStates)
+ {
+ initialConstraints[finalState] = new HashSet<int>(new int[] { 0 });
+ }
+ SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, BSpec, initialConstraints);
+ Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
+ if (simulationRelation[initialState].Count == 0)
+ {
+ moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check B at layer {1}. An action must be succeeded by a yield.\n", impl.Name, currLayerNum));
+ }
+ }
+
+ private void CSpecCheck(List<Tuple<int, int, int>> implEdges)
+ {
+ Dictionary<int, HashSet<int>> initialConstraints = new Dictionary<int, HashSet<int>>();
+ foreach (Block block in loopHeaders)
+ {
+ if (!IsTerminatingLoopHeader(block))
+ {
+ initialConstraints[absyToNode[block]] = new HashSet<int>(new int[] { 0 });
+ }
+ }
+ SimulationRelation<int, int, int> x = new SimulationRelation<int, int, int>(implEdges, CSpec, initialConstraints);
+ Dictionary<int, HashSet<int>> simulationRelation = x.ComputeSimulationRelation();
+ if (simulationRelation[initialState].Count == 0)
+ {
+ moverTypeChecker.Error(impl, string.Format("Implementation {0} fails simulation check C at layer {1}. Transactions must be separated by a yield.\n", impl.Name, currLayerNum));
+ }
+ }
+
+ private bool IsTerminatingLoopHeader(Block block)
+ {
+ foreach (Cmd cmd in block.Cmds)
+ {
+ AssertCmd assertCmd = cmd as AssertCmd;
+ if (assertCmd != null && QKeyValue.FindBoolAttribute(assertCmd.Attributes, "terminates") && moverTypeChecker.absyToLayerNums[assertCmd].Contains(currLayerNum))
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)
+ {
+ foreach (var impl in moverTypeChecker.program.Implementations)
+ {
+ if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;
+ impl.PruneUnreachableBlocks();
+ Graph<Block> implGraph = Program.GraphFromImpl(impl);
+ implGraph.ComputeLoops();
+ int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;
+ foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
+ {
+ if (layerNum > specLayerNum) continue;
+ YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);
+ }
+ }
+ }
+
+ int stateCounter;
+ MoverTypeChecker moverTypeChecker;
+ Implementation impl;
+ int currLayerNum;
+ Dictionary<Absy, int> absyToNode;
+ Dictionary<int, Absy> nodeToAbsy;
+ int initialState;
+ HashSet<int> finalStates;
+ Dictionary<Tuple<int, int>, int> edgeLabels;
+ IEnumerable<Block> loopHeaders;
+
+ private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable<Block> loopHeaders)
+ {
+ this.moverTypeChecker = moverTypeChecker;
+ this.impl = impl;
+ this.currLayerNum = currLayerNum;
+ this.loopHeaders = loopHeaders;
+ this.stateCounter = 0;
+ this.absyToNode = new Dictionary<Absy, int>();
+ this.initialState = 0;
+ this.finalStates = new HashSet<int>();
+ this.edgeLabels = new Dictionary<Tuple<int, int>, int>();
+
+ foreach (Block block in impl.Blocks)
+ {
+ absyToNode[block] = stateCounter;
+ stateCounter++;
+ foreach (Cmd cmd in block.Cmds)
+ {
+ absyToNode[cmd] = stateCounter;
+ stateCounter++;
+ }
+ absyToNode[block.TransferCmd] = stateCounter;
+ stateCounter++;
+ if (block.TransferCmd is ReturnCmd)
+ {
+ finalStates.Add(absyToNode[block.TransferCmd]);
+ }
+ }
+ foreach (Block block in impl.Blocks)
+ {
+ Absy blockEntry = block.Cmds.Count == 0 ? (Absy)block.TransferCmd : (Absy)block.Cmds[0];
+ edgeLabels[new Tuple<int, int>(absyToNode[block], absyToNode[blockEntry])] = 'P';
+
+ GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
+ if (gotoCmd == null) continue;
+ foreach (Block successor in gotoCmd.labelTargets)
+ {
+ edgeLabels[new Tuple<int, int>(absyToNode[gotoCmd], absyToNode[successor])] = 'P';
+ }
+ }
+
+ this.nodeToAbsy = new Dictionary<int, Absy>();
+ foreach (KeyValuePair<Absy, int> state in absyToNode)
+ {
+ this.nodeToAbsy[state.Value] = state.Key;
+ }
+
+ ComputeGraph();
+ IsYieldTypeSafe();
+ }
+
+ private void ComputeGraph()
+ {
+ foreach (Block block in impl.Blocks)
+ {
+ for (int i = 0; i < block.Cmds.Count; i++)
+ {
+ Cmd cmd = block.Cmds[i];
+ int curr = absyToNode[cmd];
+ int next = (i + 1 == block.Cmds.Count) ? absyToNode[block.TransferCmd] : absyToNode[block.Cmds[i + 1]];
+ Tuple<int, int> edge = new Tuple<int, int>(curr, next);
+ if (cmd is CallCmd)
+ {
+ CallCmd callCmd = cmd as CallCmd;
+ if (callCmd.IsAsync)
+ {
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+ if (currLayerNum <= actionInfo.createdAtLayerNum)
+ edgeLabels[edge] = 'L';
+ else
+ edgeLabels[edge] = 'B';
+ }
+ else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
+ {
+ edgeLabels[edge] = 'P';
+ }
+ else
+ {
+ MoverType moverType;
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+ if (actionInfo.createdAtLayerNum >= currLayerNum)
+ {
+ moverType = MoverType.Top;
+ }
+ else
+ {
+ AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+ if (atomicActionInfo == null)
+ moverType = MoverType.Both;
+ else
+ moverType = atomicActionInfo.moverType;
+ }
+ switch (moverType)
+ {
+ case MoverType.Atomic:
+ edgeLabels[edge] = 'A';
+ break;
+ case MoverType.Both:
+ edgeLabels[edge] = 'B';
+ break;
+ case MoverType.Left:
+ edgeLabels[edge] = 'L';
+ break;
+ case MoverType.Right:
+ edgeLabels[edge] = 'R';
+ break;
+ case MoverType.Top:
+ edgeLabels[edge] = 'Y';
+ break;
+ }
+ }
+ }
+ else if (cmd is ParCallCmd)
+ {
+ ParCallCmd parCallCmd = cmd as ParCallCmd;
+ bool isYield = false;
+ bool isRightMover = true;
+ bool isLeftMover = true;
+ foreach (CallCmd callCmd in parCallCmd.CallCmds)
+ {
+ if (moverTypeChecker.procToActionInfo[callCmd.Proc].createdAtLayerNum >= currLayerNum)
+ {
+ isYield = true;
+ }
+ }
+ if (isYield)
+ {
+ edgeLabels[edge] = 'Y';
+ }
+ else
+ {
+ int numAtomicActions = 0;
+ foreach (CallCmd callCmd in parCallCmd.CallCmds)
+ {
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+ isRightMover = isRightMover && actionInfo.IsRightMover;
+ isLeftMover = isLeftMover && actionInfo.IsLeftMover;
+ if (actionInfo is AtomicActionInfo)
+ {
+ numAtomicActions++;
+ }
+ }
+ if (isLeftMover && isRightMover)
+ {
+ edgeLabels[edge] = 'B';
+ }
+ else if (isLeftMover)
+ {
+ edgeLabels[edge] = 'L';
+ }
+ else if (isRightMover)
+ {
+ edgeLabels[edge] = 'R';
+ }
+ else
+ {
+ Debug.Assert(numAtomicActions == 1);
+ edgeLabels[edge] = 'A';
+ }
+ }
+ }
+ else if (cmd is YieldCmd)
+ {
+ edgeLabels[edge] = 'Y';
+ }
+ else
+ {
+ edgeLabels[edge] = 'P';
+ }
+ }
+ }
+ }
+
+ private static string PrintGraph(Implementation impl, List<Tuple<int, int, int>> edges, int initialState, HashSet<int> finalStates)
+ {
+ var s = new StringBuilder();
+ s.AppendLine("\nImplementation " + impl.Proc.Name + " digraph G {");
+ foreach (var e in edges)
+ {
+ string label = "P";
+ switch (e.Item2)
+ {
+ case 'P': label = "P"; break;
+ case 'Y': label = "Y"; break;
+ case 'B': label = "B"; break;
+ case 'R': label = "R"; break;
+ case 'L': label = "L"; break;
+ case 'A': label = "A"; break;
+ default: Debug.Assert(false); break;
+ }
+ s.AppendLine(" \"" + e.Item1.ToString() + "\" -- " + label + " --> " + " \"" + e.Item3.ToString() + "\";");
+ }
+ s.AppendLine("}");
+ s.AppendLine("Initial state: " + initialState);
+ s.Append("Final states: ");
+ bool first = true;
+ foreach (int finalState in finalStates)
+ {
+ s.Append((first ? "" : ", ") + finalState);
+ first = false;
+ }
+ s.AppendLine();
+ return s.ToString();
+ }
+ }
+}
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 7776f4de..9fda36e7 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -1,397 +1,397 @@
-//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics;
-using System.IO;
-using System.Threading;
-using System.Diagnostics.Contracts;
-
-namespace Microsoft.Boogie.SMTLib
-{
- public class SMTLibProcess
- {
- readonly Process prover;
- readonly Inspector inspector;
- readonly SMTLibProverOptions options;
- readonly Queue<string> proverOutput = new Queue<string>();
- readonly Queue<string> proverErrors = new Queue<string>();
- readonly TextWriter toProver;
- readonly int smtProcessId;
- static int smtProcessIdSeq = 0;
- ConsoleCancelEventHandler cancelEvent;
- public bool NeedsRestart;
-
- public static ProcessStartInfo ComputerProcessStartInfo(string executable, string options)
- {
- return new ProcessStartInfo(executable, options)
- {
- CreateNoWindow = true,
- UseShellExecute = false,
- RedirectStandardInput = true,
- RedirectStandardOutput = true,
- RedirectStandardError = true
- };
- }
-
- public SMTLibProcess(ProcessStartInfo psi, SMTLibProverOptions options)
- {
- this.options = options;
- this.smtProcessId = smtProcessIdSeq++;
-
- if (options.Inspector != null) {
- this.inspector = new Inspector(options);
- }
-
- foreach (var arg in options.SolverArguments)
- psi.Arguments += " " + arg;
-
- if (cancelEvent == null && CommandLineOptions.Clo.RunningBoogieFromCommandLine) {
- cancelEvent = new ConsoleCancelEventHandler(ControlCHandler);
- Console.CancelKeyPress += cancelEvent;
- }
-
- if (options.Verbosity >= 1) {
- Console.WriteLine("[SMT-{0}] Starting {1} {2}", smtProcessId, psi.FileName, psi.Arguments);
- }
-
-
- try {
- prover = new Process();
- prover.StartInfo = psi;
- prover.ErrorDataReceived += prover_ErrorDataReceived;
- prover.OutputDataReceived += prover_OutputDataReceived;
- prover.Start();
- toProver = prover.StandardInput;
- prover.BeginErrorReadLine();
- prover.BeginOutputReadLine();
- } catch (System.ComponentModel.Win32Exception e) {
- throw new ProverException(string.Format("Unable to start the process {0}: {1}", psi.FileName, e.Message));
- }
- }
-
- [NoDefaultContract] // important, since we have no idea what state the object might be in when this handler is invoked
- void ControlCHandler(object o, ConsoleCancelEventArgs a)
- {
- if (prover != null) {
- TerminateProver();
- }
- }
-
- private void TerminateProver(Int32 timeout = 2000) {
- try {
- // Let the prover know that we're done sending input.
- prover.StandardInput.Close();
-
- // Give it a chance to exit cleanly (e.g. to flush buffers)
- if (!prover.WaitForExit(timeout)) {
- prover.Kill();
- }
- } catch { /* Swallow errors */ }
- }
-
- public void Send(string cmd)
- {
- if (options.Verbosity >= 2) {
- var log = cmd;
- if (log.Length > 50)
- log = log.Substring(0, 50) + "...";
- log = log.Replace("\r", "").Replace("\n", " ");
- Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
- }
- toProver.WriteLine(cmd);
- }
-
- // this is less than perfect; (echo ...) would be better
- public void Ping()
- {
- Send("(get-info :name)");
- }
-
- public bool IsPong(SExpr sx)
- {
- return sx != null && sx.Name == ":name";
- }
-
- public void PingPong()
- {
- Ping();
- while (true) {
- var sx = GetProverResponse();
- if (sx == null) {
- this.NeedsRestart = true;
- HandleError("Prover died");
- return;
- }
-
- if (IsPong(sx))
- return;
- else
- HandleError("Invalid PING response from the prover: " + sx.ToString());
- }
- }
-
- internal Inspector Inspector
- {
- get { return inspector; }
- }
-
- public SExpr GetProverResponse()
- {
- toProver.Flush();
-
- while (true) {
- var exprs = ParseSExprs(true).ToArray();
- Contract.Assert(exprs.Length <= 1);
- if (exprs.Length == 0)
- return null;
- var resp = exprs[0];
- if (resp.Name == "error") {
- if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId)
- HandleError(resp.Arguments[0].Name);
- else
- HandleError(resp.ToString());
- } else if (resp.Name == "progress") {
- if (inspector != null) {
- var sb = new StringBuilder();
- foreach (var a in resp.Arguments) {
- if (a.Name == "labels") {
- sb.Append("STATS LABELS");
- foreach (var x in a.Arguments)
- sb.Append(" ").Append(x.Name);
- } else if (a.Name.StartsWith(":")) {
- sb.Append("STATS NAMED_VALUES ").Append(a.Name);
- foreach (var x in a.Arguments)
- sb.Append(" ").Append(x.Name);
- } else {
- continue;
- }
- inspector.StatsLine(sb.ToString());
- sb.Clear();
- }
- }
- } else if (resp.Name == "unsupported") {
- // Skip -- this may be a benign "unsupported" from a previous command.
- // Of course, this is suboptimal. We should really be using
- // print-success to identify the errant command and determine whether
- // the response is benign.
- } else {
- return resp;
- }
- }
- }
-
- public static System.TimeSpan TotalUserTime = System.TimeSpan.Zero;
-
- public void Close()
- {
- TotalUserTime += prover.UserProcessorTime;
- TerminateProver();
- DisposeProver();
- }
-
- public event Action<string> ErrorHandler;
- int errorCnt;
-
- private void HandleError(string msg)
- {
- if (options.Verbosity >= 2)
- Console.WriteLine("[SMT-ERR-{0}] Handling error: {1}", smtProcessId, msg);
- if (ErrorHandler != null)
- ErrorHandler(msg);
- }
-
- #region SExpr parsing
- int linePos;
- string currLine;
- char SkipWs()
- {
- while (true) {
- if (currLine == null) {
- currLine = ReadProver();
- if (currLine == null)
- return '\0';
- }
-
-
- while (linePos < currLine.Length && char.IsWhiteSpace(currLine[linePos]))
- linePos++;
-
- if (linePos < currLine.Length && currLine[linePos] != ';')
- return currLine[linePos];
- else {
- currLine = null;
- linePos = 0;
- }
- }
- }
-
- void Shift()
- {
- linePos++;
- }
-
- string ParseId()
- {
- var sb = new StringBuilder();
-
- var beg = SkipWs();
-
- var quoted = beg == '"' || beg == '|';
- if (quoted)
- Shift();
- while (true) {
- if (linePos >= currLine.Length) {
- if (quoted) {
- sb.Append("\n");
- currLine = ReadProver();
- linePos = 0;
- if (currLine == null)
- break;
- } else break;
- }
-
- var c = currLine[linePos++];
- if (quoted && c == beg)
- break;
- if (!quoted && (char.IsWhiteSpace(c) || c == '(' || c == ')')) {
- linePos--;
- break;
- }
- if (quoted && c == '\\' && linePos < currLine.Length && currLine[linePos] == '"') {
- sb.Append('"');
- linePos++;
- continue;
- }
- sb.Append(c);
- }
-
- return sb.ToString();
- }
-
- void ParseError(string msg)
- {
- HandleError("Error parsing prover output: " + msg);
- }
-
- IEnumerable<SExpr> ParseSExprs(bool top)
- {
- while (true) {
- var c = SkipWs();
- if (c == '\0')
- break;
-
- if (c == ')') {
- if (top)
- ParseError("stray ')'");
- break;
- }
-
- string id;
-
- if (c == '(') {
- Shift();
- c = SkipWs();
- if (c == '\0') {
- ParseError("expecting something after '('");
- break;
- } else if (c == '(') {
- id = "";
- } else {
- id = ParseId();
- }
-
- var args = ParseSExprs(false).ToArray();
-
- c = SkipWs();
- if (c == ')') {
- Shift();
- } else {
- ParseError("unclosed '(" + id + "'");
- }
- yield return new SExpr(id, args);
- } else {
- id = ParseId();
- yield return new SExpr(id);
- }
-
- if (top) break;
- }
- }
- #endregion
-
- #region handling input from the prover
- string ReadProver()
- {
- string error = null;
- while (true) {
- if (error != null) {
- HandleError(error);
- errorCnt++;
- error = null;
- }
-
- lock (this) {
- while (proverOutput.Count == 0 && proverErrors.Count == 0 && !prover.HasExited) {
- Monitor.Wait(this, 100);
- }
-
- if (proverErrors.Count > 0) {
- error = proverErrors.Dequeue();
- continue;
- }
-
- if (proverOutput.Count > 0) {
- return proverOutput.Dequeue();
- }
-
- if (prover.HasExited) {
- DisposeProver();
- return null;
- }
- }
- }
- }
-
- void DisposeProver()
- {
- if (cancelEvent != null) {
- Console.CancelKeyPress -= cancelEvent;
- cancelEvent = null;
- }
- }
-
- void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)
- {
- lock (this) {
- if (e.Data != null) {
- if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) {
- Console.WriteLine("[SMT-OUT-{0}] {1}", smtProcessId, e.Data);
- }
- proverOutput.Enqueue(e.Data);
- Monitor.Pulse(this);
- }
- }
- }
-
- void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e)
- {
- lock (this) {
- if (e.Data != null) {
- if (options.Verbosity >= 1)
- Console.WriteLine("[SMT-ERR-{0}] {1}", smtProcessId, e.Data);
- proverErrors.Enqueue(e.Data);
- Monitor.Pulse(this);
- }
- }
- }
- #endregion
- }
-}
-
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using System.IO;
+using System.Threading;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie.SMTLib
+{
+ public class SMTLibProcess
+ {
+ readonly Process prover;
+ readonly Inspector inspector;
+ readonly SMTLibProverOptions options;
+ readonly Queue<string> proverOutput = new Queue<string>();
+ readonly Queue<string> proverErrors = new Queue<string>();
+ readonly TextWriter toProver;
+ readonly int smtProcessId;
+ static int smtProcessIdSeq = 0;
+ ConsoleCancelEventHandler cancelEvent;
+ public bool NeedsRestart;
+
+ public static ProcessStartInfo ComputerProcessStartInfo(string executable, string options)
+ {
+ return new ProcessStartInfo(executable, options)
+ {
+ CreateNoWindow = true,
+ UseShellExecute = false,
+ RedirectStandardInput = true,
+ RedirectStandardOutput = true,
+ RedirectStandardError = true
+ };
+ }
+
+ public SMTLibProcess(ProcessStartInfo psi, SMTLibProverOptions options)
+ {
+ this.options = options;
+ this.smtProcessId = smtProcessIdSeq++;
+
+ if (options.Inspector != null) {
+ this.inspector = new Inspector(options);
+ }
+
+ foreach (var arg in options.SolverArguments)
+ psi.Arguments += " " + arg;
+
+ if (cancelEvent == null && CommandLineOptions.Clo.RunningBoogieFromCommandLine) {
+ cancelEvent = new ConsoleCancelEventHandler(ControlCHandler);
+ Console.CancelKeyPress += cancelEvent;
+ }
+
+ if (options.Verbosity >= 1) {
+ Console.WriteLine("[SMT-{0}] Starting {1} {2}", smtProcessId, psi.FileName, psi.Arguments);
+ }
+
+
+ try {
+ prover = new Process();
+ prover.StartInfo = psi;
+ prover.ErrorDataReceived += prover_ErrorDataReceived;
+ prover.OutputDataReceived += prover_OutputDataReceived;
+ prover.Start();
+ toProver = prover.StandardInput;
+ prover.BeginErrorReadLine();
+ prover.BeginOutputReadLine();
+ } catch (System.ComponentModel.Win32Exception e) {
+ throw new ProverException(string.Format("Unable to start the process {0}: {1}", psi.FileName, e.Message));
+ }
+ }
+
+ [NoDefaultContract] // important, since we have no idea what state the object might be in when this handler is invoked
+ void ControlCHandler(object o, ConsoleCancelEventArgs a)
+ {
+ if (prover != null) {
+ TerminateProver();
+ }
+ }
+
+ private void TerminateProver(Int32 timeout = 2000) {
+ try {
+ // Let the prover know that we're done sending input.
+ prover.StandardInput.Close();
+
+ // Give it a chance to exit cleanly (e.g. to flush buffers)
+ if (!prover.WaitForExit(timeout)) {
+ prover.Kill();
+ }
+ } catch { /* Swallow errors */ }
+ }
+
+ public void Send(string cmd)
+ {
+ if (options.Verbosity >= 2) {
+ var log = cmd;
+ if (log.Length > 50)
+ log = log.Substring(0, 50) + "...";
+ log = log.Replace("\r", "").Replace("\n", " ");
+ Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
+ }
+ toProver.WriteLine(cmd);
+ }
+
+ // this is less than perfect; (echo ...) would be better
+ public void Ping()
+ {
+ Send("(get-info :name)");
+ }
+
+ public bool IsPong(SExpr sx)
+ {
+ return sx != null && sx.Name == ":name";
+ }
+
+ public void PingPong()
+ {
+ Ping();
+ while (true) {
+ var sx = GetProverResponse();
+ if (sx == null) {
+ this.NeedsRestart = true;
+ HandleError("Prover died");
+ return;
+ }
+
+ if (IsPong(sx))
+ return;
+ else
+ HandleError("Invalid PING response from the prover: " + sx.ToString());
+ }
+ }
+
+ internal Inspector Inspector
+ {
+ get { return inspector; }
+ }
+
+ public SExpr GetProverResponse()
+ {
+ toProver.Flush();
+
+ while (true) {
+ var exprs = ParseSExprs(true).ToArray();
+ Contract.Assert(exprs.Length <= 1);
+ if (exprs.Length == 0)
+ return null;
+ var resp = exprs[0];
+ if (resp.Name == "error") {
+ if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId)
+ HandleError(resp.Arguments[0].Name);
+ else
+ HandleError(resp.ToString());
+ } else if (resp.Name == "progress") {
+ if (inspector != null) {
+ var sb = new StringBuilder();
+ foreach (var a in resp.Arguments) {
+ if (a.Name == "labels") {
+ sb.Append("STATS LABELS");
+ foreach (var x in a.Arguments)
+ sb.Append(" ").Append(x.Name);
+ } else if (a.Name.StartsWith(":")) {
+ sb.Append("STATS NAMED_VALUES ").Append(a.Name);
+ foreach (var x in a.Arguments)
+ sb.Append(" ").Append(x.Name);
+ } else {
+ continue;
+ }
+ inspector.StatsLine(sb.ToString());
+ sb.Clear();
+ }
+ }
+ } else if (resp.Name == "unsupported") {
+ // Skip -- this may be a benign "unsupported" from a previous command.
+ // Of course, this is suboptimal. We should really be using
+ // print-success to identify the errant command and determine whether
+ // the response is benign.
+ } else {
+ return resp;
+ }
+ }
+ }
+
+ public static System.TimeSpan TotalUserTime = System.TimeSpan.Zero;
+
+ public void Close()
+ {
+ TotalUserTime += prover.UserProcessorTime;
+ TerminateProver();
+ DisposeProver();
+ }
+
+ public event Action<string> ErrorHandler;
+ int errorCnt;
+
+ private void HandleError(string msg)
+ {
+ if (options.Verbosity >= 2)
+ Console.WriteLine("[SMT-ERR-{0}] Handling error: {1}", smtProcessId, msg);
+ if (ErrorHandler != null)
+ ErrorHandler(msg);
+ }
+
+ #region SExpr parsing
+ int linePos;
+ string currLine;
+ char SkipWs()
+ {
+ while (true) {
+ if (currLine == null) {
+ currLine = ReadProver();
+ if (currLine == null)
+ return '\0';
+ }
+
+
+ while (linePos < currLine.Length && char.IsWhiteSpace(currLine[linePos]))
+ linePos++;
+
+ if (linePos < currLine.Length && currLine[linePos] != ';')
+ return currLine[linePos];
+ else {
+ currLine = null;
+ linePos = 0;
+ }
+ }
+ }
+
+ void Shift()
+ {
+ linePos++;
+ }
+
+ string ParseId()
+ {
+ var sb = new StringBuilder();
+
+ var beg = SkipWs();
+
+ var quoted = beg == '"' || beg == '|';
+ if (quoted)
+ Shift();
+ while (true) {
+ if (linePos >= currLine.Length) {
+ if (quoted) {
+ sb.Append("\n");
+ currLine = ReadProver();
+ linePos = 0;
+ if (currLine == null)
+ break;
+ } else break;
+ }
+
+ var c = currLine[linePos++];
+ if (quoted && c == beg)
+ break;
+ if (!quoted && (char.IsWhiteSpace(c) || c == '(' || c == ')')) {
+ linePos--;
+ break;
+ }
+ if (quoted && c == '\\' && linePos < currLine.Length && currLine[linePos] == '"') {
+ sb.Append('"');
+ linePos++;
+ continue;
+ }
+ sb.Append(c);
+ }
+
+ return sb.ToString();
+ }
+
+ void ParseError(string msg)
+ {
+ HandleError("Error parsing prover output: " + msg);
+ }
+
+ IEnumerable<SExpr> ParseSExprs(bool top)
+ {
+ while (true) {
+ var c = SkipWs();
+ if (c == '\0')
+ break;
+
+ if (c == ')') {
+ if (top)
+ ParseError("stray ')'");
+ break;
+ }
+
+ string id;
+
+ if (c == '(') {
+ Shift();
+ c = SkipWs();
+ if (c == '\0') {
+ ParseError("expecting something after '('");
+ break;
+ } else if (c == '(') {
+ id = "";
+ } else {
+ id = ParseId();
+ }
+
+ var args = ParseSExprs(false).ToArray();
+
+ c = SkipWs();
+ if (c == ')') {
+ Shift();
+ } else {
+ ParseError("unclosed '(" + id + "'");
+ }
+ yield return new SExpr(id, args);
+ } else {
+ id = ParseId();
+ yield return new SExpr(id);
+ }
+
+ if (top) break;
+ }
+ }
+ #endregion
+
+ #region handling input from the prover
+ string ReadProver()
+ {
+ string error = null;
+ while (true) {
+ if (error != null) {
+ HandleError(error);
+ errorCnt++;
+ error = null;
+ }
+
+ lock (this) {
+ while (proverOutput.Count == 0 && proverErrors.Count == 0 && !prover.HasExited) {
+ Monitor.Wait(this, 100);
+ }
+
+ if (proverErrors.Count > 0) {
+ error = proverErrors.Dequeue();
+ continue;
+ }
+
+ if (proverOutput.Count > 0) {
+ return proverOutput.Dequeue();
+ }
+
+ if (prover.HasExited) {
+ DisposeProver();
+ return null;
+ }
+ }
+ }
+ }
+
+ void DisposeProver()
+ {
+ if (cancelEvent != null) {
+ Console.CancelKeyPress -= cancelEvent;
+ cancelEvent = null;
+ }
+ }
+
+ void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)
+ {
+ lock (this) {
+ if (e.Data != null) {
+ if (options.Verbosity >= 2 || (options.Verbosity >= 1 && !e.Data.StartsWith("(:name "))) {
+ Console.WriteLine("[SMT-OUT-{0}] {1}", smtProcessId, e.Data);
+ }
+ proverOutput.Enqueue(e.Data);
+ Monitor.Pulse(this);
+ }
+ }
+ }
+
+ void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e)
+ {
+ lock (this) {
+ if (e.Data != null) {
+ if (options.Verbosity >= 1)
+ Console.WriteLine("[SMT-ERR-{0}] {1}", smtProcessId, e.Data);
+ proverErrors.Enqueue(e.Data);
+ Monitor.Pulse(this);
+ }
+ }
+ }
+ #endregion
+ }
+}
+
diff --git a/Test/civl/chris3.bpl b/Test/civl/chris3.bpl
new file mode 100644
index 00000000..5cbc000a
--- /dev/null
+++ b/Test/civl/chris3.bpl
@@ -0,0 +1,19 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure{:yields}{:layer 94,94} H()
+{
+ yield;
+}
+
+procedure{:yields}{:layer 94,95} A()
+ ensures{:atomic} |{ A: return true; }|;
+{
+ yield;
+}
+
+procedure{:yields}{:layer 95,95} P()
+{
+ yield;
+ par A() | H();
+ yield;
+}
diff --git a/Test/civl/chris3.bpl.expect b/Test/civl/chris3.bpl.expect
new file mode 100644
index 00000000..c8b2ab00
--- /dev/null
+++ b/Test/civl/chris3.bpl.expect
@@ -0,0 +1,3 @@
+chris3.bpl(3,33): Error: Creation layer number must be less than the available upto layer number
+chris3.bpl(14,33): Error: Creation layer number must be less than the available upto layer number
+2 type checking errors detected in chris3.bpl
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 22:56:35 +0000