diff options
-rw-r--r-- | Source/Concurrency/TypeCheck.cs | 1527 | ||||
-rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 731 | ||||
-rw-r--r-- | Source/Provers/SMTLib/SMTLibProcess.cs | 785 | ||||
-rw-r--r-- | Test/civl/chris3.bpl | 19 | ||||
-rw-r--r-- | Test/civl/chris3.bpl.expect | 2 |
5 files changed, 1557 insertions, 1507 deletions
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index c407a7b9..542d3515 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -1,757 +1,772 @@ -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; + } + 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; + } + if (availableUptoLayerNum <= createdAtLayerNum) + { + Error(proc, "Creation layer number must be less than the available upto layer number"); + 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)) + { + if (availableUptoLayerNum < createdAtLayerNum) + { + Error(proc, "Creation layer number must be no more than the available upto layer number"); + continue; + } + else + { + 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 4a1331c5..9fda36e7 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -1,388 +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) {
- prover.Kill();
- }
- }
-
- 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;
- try {
- prover.Kill();
- } catch {
- }
- 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..b415d3b9 --- /dev/null +++ b/Test/civl/chris3.bpl.expect @@ -0,0 +1,2 @@ +chris3.bpl(17,2): Error: The callee is not available in the caller procedure +1 type checking errors detected in chris3.bpl |