From 938bfd15dbd13b2d8eaf5f6a0cb5b895173ffa09 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 9 Jun 2015 01:03:32 -0700 Subject: Stop truncating the prover logs As it stands, Boogie abruptly aborts the prover by calling Kill() on the associated process after receiving responses to all of its queries. In most cases this is fine, but in general this is pretty bad: it yields to all sorts of output corruption when user-supplied options require z3 to write output to an auxiliary file (say, using /z3opt:TRACE=true). This explains why VCC's Axiom Profiler often complains about a missing [eof] after running Boogie with /z3opt:TRACE=true. This patch fixes it by only falling back to Kill if the process seems to have become unresponsive. That is, it starts by cleanly closing the process input, which signals the end of the interactive session. It then waits for a clean exit for 2s, and only after that does it resort to calling Kill(). I've striven for minimal modifications to the logic, so the patch still universally swallows errors that might occur while closing the underlying stream, and still calls Kill() (I wouldn't be against Boogie just hanging if z3 hangs too). On my tests, z3 exits cleanly pretty much instantly after input is closed anyway, so I don't expect the timeout to fire often (which would be one more reason to actually remove that timeout, and condition Boogie's exit on that of z3 IMO). --- Source/Provers/SMTLib/SMTLibProcess.cs | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) (limited to 'Source/Provers') diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 4a1331c5..7776f4de 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -80,10 +80,22 @@ namespace Microsoft.Boogie.SMTLib void ControlCHandler(object o, ConsoleCancelEventArgs a) { if (prover != null) { - prover.Kill(); + 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) { @@ -180,10 +192,7 @@ namespace Microsoft.Boogie.SMTLib public void Close() { TotalUserTime += prover.UserProcessorTime; - try { - prover.Kill(); - } catch { - } + TerminateProver(); DisposeProver(); } -- cgit v1.2.3 From 9c97c7c52776575485c3b131202addb1d864e3d9 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 10 Jun 2015 10:46:17 -0700 Subject: fixed crash --- Source/Concurrency/TypeCheck.cs | 1519 ++++++++++++++++---------------- Source/Concurrency/YieldTypeChecker.cs | 731 +++++++-------- Source/Provers/SMTLib/SMTLibProcess.cs | 794 ++++++++--------- Test/civl/chris3.bpl | 19 + Test/civl/chris3.bpl.expect | 3 + 5 files changed, 1550 insertions(+), 1516 deletions(-) create mode 100644 Test/civl/chris3.bpl create mode 100644 Test/civl/chris3.bpl.expect (limited to 'Source/Provers') 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 thisGate; - public CodeExpr thisAction; - public List thisInParams; - public List thisOutParams; - public List thatGate; - public CodeExpr thatAction; - public List thatInParams; - public List thatOutParams; - public HashSet actionUsedGlobalVars; - public HashSet modifiedGlobalVars; - public HashSet 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(); - this.thisAction = codeExpr; - this.thisInParams = new List(); - this.thisOutParams = new List(); - this.thatGate = new List(); - this.thatInParams = new List(); - this.thatOutParams = new List(); - 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 map = new Dictionary(); - 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 thatLocVars = new List(); - 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 blockMap = new Dictionary(); - List thatBlocks = new List(); - foreach (Block block in thisAction.Blocks) - { - List otherCmds = new List(); - 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 thatGotoCmdLabelTargets = new List(); - List thatGotoCmdLabelNames = new List(); - 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(collector.usedVars.Where(x => x is GlobalVariable)); - } - - List modifiedVars = new List(); - foreach (Block block in codeExpr.Blocks) - { - block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars)); - } - this.modifiedGlobalVars = new HashSet(modifiedVars.Where(x => x is GlobalVariable)); - - { - VariableCollector collector = new VariableCollector(); - this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd)); - this.gateUsedGlobalVars = new HashSet(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 globalVarToSharedVarInfo; - Procedure enclosingProc; - Implementation enclosingImpl; - public Dictionary procToActionInfo; - public Program program; - bool canAccessSharedVars; - bool canAccessGhostVars; - int minLayerNum; - int maxLayerNum; - public Dictionary> absyToLayerNums; - HashSet ghostVars; - public int leastUnimplementedLayerNum; - - private static List FindLayers(QKeyValue kv) - { - HashSet attrs = new HashSet(); - 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 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(); - this.absyToLayerNums = new Dictionary>(); - this.globalVarToSharedVarInfo = new Dictionary(); - this.procToActionInfo = new Dictionary(); - 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 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 allCreatedLayerNums; - public IEnumerable AllCreatedLayerNums - { - get - { - if (allCreatedLayerNums == null) - { - allCreatedLayerNums = new HashSet(); - 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 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 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(); - 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 outParams = new HashSet(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() == 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 attrs = FindLayers(attributes); - if (attrs.Count == 0) - { - Error(node, "layer not present"); - return; - } - absyToLayerNums[node] = new HashSet(); - 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 thisGate; + public CodeExpr thisAction; + public List thisInParams; + public List thisOutParams; + public List thatGate; + public CodeExpr thatAction; + public List thatInParams; + public List thatOutParams; + public HashSet actionUsedGlobalVars; + public HashSet modifiedGlobalVars; + public HashSet 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(); + this.thisAction = codeExpr; + this.thisInParams = new List(); + this.thisOutParams = new List(); + this.thatGate = new List(); + this.thatInParams = new List(); + this.thatOutParams = new List(); + 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 map = new Dictionary(); + 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 thatLocVars = new List(); + 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 blockMap = new Dictionary(); + List thatBlocks = new List(); + foreach (Block block in thisAction.Blocks) + { + List otherCmds = new List(); + 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 thatGotoCmdLabelTargets = new List(); + List thatGotoCmdLabelNames = new List(); + 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(collector.usedVars.Where(x => x is GlobalVariable)); + } + + List modifiedVars = new List(); + foreach (Block block in codeExpr.Blocks) + { + block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars)); + } + this.modifiedGlobalVars = new HashSet(modifiedVars.Where(x => x is GlobalVariable)); + + { + VariableCollector collector = new VariableCollector(); + this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd)); + this.gateUsedGlobalVars = new HashSet(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 globalVarToSharedVarInfo; + Procedure enclosingProc; + Implementation enclosingImpl; + public Dictionary procToActionInfo; + public Program program; + bool canAccessSharedVars; + bool canAccessGhostVars; + int minLayerNum; + int maxLayerNum; + public Dictionary> absyToLayerNums; + HashSet ghostVars; + public int leastUnimplementedLayerNum; + + private static List FindLayers(QKeyValue kv) + { + List layers = new List(); + 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(); + this.absyToLayerNums = new Dictionary>(); + this.globalVarToSharedVarInfo = new Dictionary(); + this.procToActionInfo = new Dictionary(); + 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 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 allCreatedLayerNums; + public IEnumerable AllCreatedLayerNums + { + get + { + if (allCreatedLayerNums == null) + { + allCreatedLayerNums = new HashSet(); + 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 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 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(); + 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 outParams = new HashSet(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() == 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 RemoveDuplicatesAndSort(List attrs) + { + HashSet layerSet = new HashSet(attrs); + List layers = new List(layerSet); + layers.Sort(); + return layers; + } + + private void CheckAndAddLayers(Absy node, QKeyValue attributes, int enclosingProcLayerNum) + { + List attrs = RemoveDuplicatesAndSort(FindLayers(attributes)); + if (attrs.Count == 0) + { + Error(node, "layer not present"); + return; + } + absyToLayerNums[node] = new HashSet(); + 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> ASpec; - static List> BSpec; - static List> CSpec; - static YieldTypeChecker() - { - // initial: 0, final: 1 - ASpec = new List>(); - ASpec.Add(new Tuple(0, 'Y', 1)); - ASpec.Add(new Tuple(1, 'Y', 1)); - ASpec.Add(new Tuple(1, 'B', 1)); - ASpec.Add(new Tuple(1, 'R', 1)); - ASpec.Add(new Tuple(1, 'L', 1)); - ASpec.Add(new Tuple(1, 'A', 1)); - ASpec.Add(new Tuple(0, 'P', 0)); - ASpec.Add(new Tuple(1, 'P', 1)); - - // initial: 1, final: 0 - BSpec = new List>(); - BSpec.Add(new Tuple(1, 'Y', 0)); - BSpec.Add(new Tuple(1, 'Y', 1)); - BSpec.Add(new Tuple(1, 'B', 1)); - BSpec.Add(new Tuple(1, 'R', 1)); - BSpec.Add(new Tuple(1, 'L', 1)); - BSpec.Add(new Tuple(1, 'A', 1)); - BSpec.Add(new Tuple(0, 'P', 0)); - BSpec.Add(new Tuple(1, 'P', 1)); - - // initial: {0, 1}, final: {0, 1} - CSpec = new List>(); - CSpec.Add(new Tuple(0, 'B', 0)); - CSpec.Add(new Tuple(0, 'R', 0)); - CSpec.Add(new Tuple(0, 'Y', 0)); - CSpec.Add(new Tuple(0, 'B', 1)); - CSpec.Add(new Tuple(0, 'R', 1)); - CSpec.Add(new Tuple(0, 'L', 1)); - CSpec.Add(new Tuple(0, 'A', 1)); - CSpec.Add(new Tuple(1, 'B', 1)); - CSpec.Add(new Tuple(1, 'L', 1)); - CSpec.Add(new Tuple(1, 'Y', 0)); - CSpec.Add(new Tuple(0, 'P', 0)); - CSpec.Add(new Tuple(1, 'P', 1)); - } - - private void IsYieldTypeSafe() - { - List> implEdges = new List>(); - foreach (Tuple e in edgeLabels.Keys) - { - implEdges.Add(new Tuple(e.Item1, edgeLabels[e], e.Item2)); - } - //Console.WriteLine(PrintGraph(impl, implEdges, initialState, finalStates)); - ASpecCheck(implEdges); - BSpecCheck(implEdges); - CSpecCheck(implEdges); - } - - private void ASpecCheck(List> implEdges) - { - Dictionary> initialConstraints = new Dictionary>(); - initialConstraints[initialState] = new HashSet(new int[] { 0 }); - foreach (var finalState in finalStates) - { - initialConstraints[finalState] = new HashSet(new int[] { 1 }); - } - SimulationRelation x = new SimulationRelation(implEdges, ASpec, initialConstraints); - Dictionary> 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> implEdges) - { - Dictionary> initialConstraints = new Dictionary>(); - initialConstraints[initialState] = new HashSet(new int[] { 1 }); - foreach (var finalState in finalStates) - { - initialConstraints[finalState] = new HashSet(new int[] { 0 }); - } - SimulationRelation x = new SimulationRelation(implEdges, BSpec, initialConstraints); - Dictionary> 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> implEdges) - { - Dictionary> initialConstraints = new Dictionary>(); - foreach (Block block in loopHeaders) - { - if (!IsTerminatingLoopHeader(block)) - { - initialConstraints[absyToNode[block]] = new HashSet(new int[] { 0 }); - } - } - SimulationRelation x = new SimulationRelation(implEdges, CSpec, initialConstraints); - Dictionary> 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 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 absyToNode; - Dictionary nodeToAbsy; - int initialState; - HashSet finalStates; - Dictionary, int> edgeLabels; - IEnumerable loopHeaders; - - private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable loopHeaders) - { - this.moverTypeChecker = moverTypeChecker; - this.impl = impl; - this.currLayerNum = currLayerNum; - this.loopHeaders = loopHeaders; - this.stateCounter = 0; - this.absyToNode = new Dictionary(); - this.initialState = 0; - this.finalStates = new HashSet(); - this.edgeLabels = new Dictionary, 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(absyToNode[block], absyToNode[blockEntry])] = 'P'; - - GotoCmd gotoCmd = block.TransferCmd as GotoCmd; - if (gotoCmd == null) continue; - foreach (Block successor in gotoCmd.labelTargets) - { - edgeLabels[new Tuple(absyToNode[gotoCmd], absyToNode[successor])] = 'P'; - } - } - - this.nodeToAbsy = new Dictionary(); - foreach (KeyValuePair 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 edge = new Tuple(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> edges, int initialState, HashSet 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> ASpec; + static List> BSpec; + static List> CSpec; + static YieldTypeChecker() + { + // initial: 0, final: 1 + ASpec = new List>(); + ASpec.Add(new Tuple(0, 'Y', 1)); + ASpec.Add(new Tuple(1, 'Y', 1)); + ASpec.Add(new Tuple(1, 'B', 1)); + ASpec.Add(new Tuple(1, 'R', 1)); + ASpec.Add(new Tuple(1, 'L', 1)); + ASpec.Add(new Tuple(1, 'A', 1)); + ASpec.Add(new Tuple(0, 'P', 0)); + ASpec.Add(new Tuple(1, 'P', 1)); + + // initial: 1, final: 0 + BSpec = new List>(); + BSpec.Add(new Tuple(1, 'Y', 0)); + BSpec.Add(new Tuple(1, 'Y', 1)); + BSpec.Add(new Tuple(1, 'B', 1)); + BSpec.Add(new Tuple(1, 'R', 1)); + BSpec.Add(new Tuple(1, 'L', 1)); + BSpec.Add(new Tuple(1, 'A', 1)); + BSpec.Add(new Tuple(0, 'P', 0)); + BSpec.Add(new Tuple(1, 'P', 1)); + + // initial: {0, 1}, final: {0, 1} + CSpec = new List>(); + CSpec.Add(new Tuple(0, 'B', 0)); + CSpec.Add(new Tuple(0, 'R', 0)); + CSpec.Add(new Tuple(0, 'Y', 0)); + CSpec.Add(new Tuple(0, 'B', 1)); + CSpec.Add(new Tuple(0, 'R', 1)); + CSpec.Add(new Tuple(0, 'L', 1)); + CSpec.Add(new Tuple(0, 'A', 1)); + CSpec.Add(new Tuple(1, 'B', 1)); + CSpec.Add(new Tuple(1, 'L', 1)); + CSpec.Add(new Tuple(1, 'Y', 0)); + CSpec.Add(new Tuple(0, 'P', 0)); + CSpec.Add(new Tuple(1, 'P', 1)); + } + + private void IsYieldTypeSafe() + { + List> implEdges = new List>(); + foreach (Tuple e in edgeLabels.Keys) + { + implEdges.Add(new Tuple(e.Item1, edgeLabels[e], e.Item2)); + } + //Console.WriteLine(PrintGraph(impl, implEdges, initialState, finalStates)); + ASpecCheck(implEdges); + BSpecCheck(implEdges); + CSpecCheck(implEdges); + } + + private void ASpecCheck(List> implEdges) + { + Dictionary> initialConstraints = new Dictionary>(); + initialConstraints[initialState] = new HashSet(new int[] { 0 }); + foreach (var finalState in finalStates) + { + initialConstraints[finalState] = new HashSet(new int[] { 1 }); + } + SimulationRelation x = new SimulationRelation(implEdges, ASpec, initialConstraints); + Dictionary> 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> implEdges) + { + Dictionary> initialConstraints = new Dictionary>(); + initialConstraints[initialState] = new HashSet(new int[] { 1 }); + foreach (var finalState in finalStates) + { + initialConstraints[finalState] = new HashSet(new int[] { 0 }); + } + SimulationRelation x = new SimulationRelation(implEdges, BSpec, initialConstraints); + Dictionary> 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> implEdges) + { + Dictionary> initialConstraints = new Dictionary>(); + foreach (Block block in loopHeaders) + { + if (!IsTerminatingLoopHeader(block)) + { + initialConstraints[absyToNode[block]] = new HashSet(new int[] { 0 }); + } + } + SimulationRelation x = new SimulationRelation(implEdges, CSpec, initialConstraints); + Dictionary> 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 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 absyToNode; + Dictionary nodeToAbsy; + int initialState; + HashSet finalStates; + Dictionary, int> edgeLabels; + IEnumerable loopHeaders; + + private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currLayerNum, IEnumerable loopHeaders) + { + this.moverTypeChecker = moverTypeChecker; + this.impl = impl; + this.currLayerNum = currLayerNum; + this.loopHeaders = loopHeaders; + this.stateCounter = 0; + this.absyToNode = new Dictionary(); + this.initialState = 0; + this.finalStates = new HashSet(); + this.edgeLabels = new Dictionary, 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(absyToNode[block], absyToNode[blockEntry])] = 'P'; + + GotoCmd gotoCmd = block.TransferCmd as GotoCmd; + if (gotoCmd == null) continue; + foreach (Block successor in gotoCmd.labelTargets) + { + edgeLabels[new Tuple(absyToNode[gotoCmd], absyToNode[successor])] = 'P'; + } + } + + this.nodeToAbsy = new Dictionary(); + foreach (KeyValuePair 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 edge = new Tuple(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> edges, int initialState, HashSet 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 proverOutput = new Queue(); - readonly Queue proverErrors = new Queue(); - 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 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 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 proverOutput = new Queue(); + readonly Queue proverErrors = new Queue(); + 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 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 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 -- cgit v1.2.3