From 67734e425160c5e10734bbb39ba8855f77f01b8c Mon Sep 17 00:00:00 2001 From: qadeer Date: Mon, 16 Dec 2013 12:32:55 -0800 Subject: added syntax for par call and ParCallCmd --- Source/Concurrency/LinearSets.cs | 119 +++++--- Source/Concurrency/MoverCheck.cs | 2 + Source/Concurrency/OwickiGries.cs | 136 +++++----- Source/Concurrency/TypeCheck.cs | 66 ++++- Source/Core/AbsyCmd.cs | 150 +++++++---- Source/Core/BoogiePL.atg | 36 ++- Source/Core/DeadVarElim.cs | 42 ++- Source/Core/Duplicator.cs | 11 +- Source/Core/Parser.cs | 434 ++++++++++++++++-------------- Source/Core/ResolutionContext.cs | 2 - Source/Core/Scanner.cs | 104 +++---- Source/Core/StandardVisitor.cs | 11 + Source/ExecutionEngine/ExecutionEngine.cs | 2 +- Source/VCExpr/Boogie2VCExpr.cs | 6 + Test/linear/Answer | 8 +- Test/linear/typecheck.bpl | 6 +- Test/og/DeviceCache.bpl | 4 +- Test/og/DeviceCacheWithBuffer.bpl | 4 +- Test/og/parallel1.bpl | 2 +- Test/og/parallel2.bpl | 4 +- Test/og/parallel3.bpl | 2 +- Test/og/parallel4.bpl | 2 +- Test/og/parallel5.bpl | 4 +- Test/og/parallel7.bpl | 2 +- Test/og/ticket.bpl | 124 +++++++++ 25 files changed, 812 insertions(+), 471 deletions(-) create mode 100644 Test/og/ticket.bpl diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index 576d6163..d0ee04b3 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -41,7 +41,6 @@ namespace Microsoft.Boogie this.errorCount = 0; this.checkingContext = new CheckingContext(null); this.domainNameToType = new Dictionary(); - this.parallelCallInvars = new HashSet(); this.availableLinearVars = new Dictionary>(); this.inoutParamToDomainName = new Dictionary(); this.varToDomainName = new Dictionary(); @@ -113,12 +112,12 @@ namespace Microsoft.Boogie { foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(end)) { - Error(b, string.Format("Global variable {0} must be available at a return", g.Name)); + Error(b.TransferCmd, string.Format("Global variable {0} must be available at a return", g.Name)); } foreach (Variable v in node.OutParams) { if (FindDomainName(v) == null || end.Contains(v)) continue; - Error(b, string.Format("Output variable {0} must be available at a return", v.Name)); + Error(b.TransferCmd, string.Format("Output variable {0} must be available at a return", v.Name)); } continue; } @@ -175,10 +174,37 @@ namespace Microsoft.Boogie { foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start)) { - Error(b, string.Format("Global variable {0} must be available at a call", g.Name)); - } + Error(cmd, string.Format("Global variable {0} must be available at a call", g.Name)); + } CallCmd callCmd = (CallCmd)cmd; - while (callCmd != null) + for (int i = 0; i < callCmd.Proc.InParams.Count; i++) + { + if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue; + IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr; + if (start.Contains(ie.Decl)) + { + start.Remove(ie.Decl); + } + else + { + Error(ie, "unavailable source for a linear read"); + } + } + availableLinearVars[callCmd] = new HashSet(start); + foreach (IdentifierExpr ie in callCmd.Outs) + { + if (FindDomainName(ie.Decl) == null) continue; + start.Add(ie.Decl); + } + } + else if (cmd is ParCallCmd) + { + foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start)) + { + Error(cmd, string.Format("Global variable {0} must be available at a call", g.Name)); + } + ParCallCmd parCallCmd = (ParCallCmd)cmd; + foreach (CallCmd callCmd in parCallCmd.CallCmds) { for (int i = 0; i < callCmd.Proc.InParams.Count; i++) { @@ -193,23 +219,20 @@ namespace Microsoft.Boogie Error(ie, "unavailable source for a linear read"); } } - callCmd = callCmd.InParallelWith; } - callCmd = (CallCmd)cmd; - availableLinearVars[callCmd] = new HashSet(start); - while (callCmd != null) + availableLinearVars[parCallCmd] = new HashSet(start); + foreach (CallCmd callCmd in parCallCmd.CallCmds) { foreach (IdentifierExpr ie in callCmd.Outs) { if (FindDomainName(ie.Decl) == null) continue; start.Add(ie.Decl); } - callCmd = callCmd.InParallelWith; } } else if (cmd is HavocCmd) { - HavocCmd havocCmd = (HavocCmd) cmd; + HavocCmd havocCmd = (HavocCmd)cmd; foreach (IdentifierExpr ie in havocCmd.Vars) { if (FindDomainName(ie.Decl) == null) continue; @@ -220,7 +243,7 @@ namespace Microsoft.Boogie { foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start)) { - Error(b, string.Format("Global variable {0} must be available at a yield", g.Name)); + Error(cmd, string.Format("Global variable {0} must be available at a yield", g.Name)); } availableLinearVars[cmd] = new HashSet(start); } @@ -311,7 +334,6 @@ namespace Microsoft.Boogie } return base.VisitAssignCmd(node); } - HashSet parallelCallInvars; public override Cmd VisitCallCmd(CallCmd node) { HashSet inVars = new HashSet(); @@ -337,18 +359,17 @@ namespace Microsoft.Boogie Error(node, "The domains of formal and actual parameters must be the same"); continue; } - if (parallelCallInvars.Contains(actual.Decl)) + if (actual.Decl is GlobalVariable) { - Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name)); + Error(node, "Only local linear variable can be an actual input parameter of a procedure call"); continue; } - if (actual.Decl is GlobalVariable) + if (inVars.Contains(actual.Decl)) { - Error(node, "Only local linear variable can be an actual input parameter of a procedure call"); + Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name)); continue; } inVars.Add(actual.Decl); - parallelCallInvars.Add(actual.Decl); } for (int i = 0; i < node.Proc.OutParams.Count; i++) { @@ -373,17 +394,31 @@ namespace Microsoft.Boogie continue; } } - if (node.InParallelWith != null) - { - VisitCallCmd(node.InParallelWith); - } - foreach (Variable v in inVars) + return base.VisitCallCmd(node); + } + public override Cmd VisitParCallCmd(ParCallCmd node) + { + HashSet parallelCallInvars = new HashSet(); + foreach (CallCmd callCmd in node.CallCmds) { - parallelCallInvars.Remove(v); + for (int i = 0; i < callCmd.Proc.InParams.Count; i++) + { + Variable formal = callCmd.Proc.InParams[i]; + string domainName = FindDomainName(formal); + if (domainName == null) continue; + IdentifierExpr actual = callCmd.Ins[i] as IdentifierExpr; + if (parallelCallInvars.Contains(actual.Decl)) + { + Error(node, string.Format("Linear variable {0} can occur only once as an input parameter of a parallel call", actual.Decl.Name)); + } + else + { + parallelCallInvars.Add(actual.Decl); + } + } } - return base.VisitCallCmd(node); + return base.VisitParCallCmd(node); } - private void AddDisjointnessExpr(List newCmds, Absy absy, Dictionary domainNameToInputVar) { Dictionary> domainNameToScope = new Dictionary>(); @@ -444,21 +479,6 @@ namespace Microsoft.Boogie callCmd.Ins.Add(expr); } } - else if (callCmd.InParallelWith != null) - { - while (callCmd != null) - { - foreach (var domainName in linearDomains.Keys) - { - var domain = linearDomains[domainName]; - var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - callCmd.Ins.Add(expr); - } - callCmd = callCmd.InParallelWith; - } - } else { Dictionary domainNameToExpr = new Dictionary(); @@ -483,6 +503,21 @@ namespace Microsoft.Boogie } } } + else if (cmd is ParCallCmd) + { + ParCallCmd parCallCmd = (ParCallCmd)cmd; + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + foreach (var domainName in linearDomains.Keys) + { + var domain = linearDomains[domainName]; + var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List { Expr.False }); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + callCmd.Ins.Add(expr); + } + } + } else if (cmd is YieldCmd) { AddDisjointnessExpr(newCmds, cmd, domainNameToInputVar); diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 53d61ba5..2b6b406a 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -21,6 +21,7 @@ namespace Microsoft.Boogie public Procedure proc; public MoverType moverType; public int phaseNum; + public HashSet callerPhaseNums; public List thisGate; public CodeExpr thisAction; public List thisInParams; @@ -45,6 +46,7 @@ namespace Microsoft.Boogie this.proc = proc; this.moverType = moverType; this.phaseNum = phaseNum; + this.callerPhaseNums = new HashSet(); this.thisGate = new List(); this.thisAction = codeExpr; this.thisInParams = new List(); diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 7125bfcd..561d9a53 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -130,18 +130,16 @@ namespace Microsoft.Boogie } } - public Procedure DesugarParallelCallCmd(CallCmd callCmd, out List ins, out List outs) + public void DesugarParallelCallCmd(List newCmds, ParCallCmd parCallCmd) { List parallelCalleeNames = new List(); - CallCmd iter = callCmd; - ins = new List(); - outs = new List(); - while (iter != null) + List ins = new List(); + List outs = new List(); + foreach (CallCmd callCmd in parCallCmd.CallCmds) { - parallelCalleeNames.Add(iter.Proc.Name); - ins.AddRange(iter.Ins); - outs.AddRange(iter.Outs); - iter = iter.InParallelWith; + parallelCalleeNames.Add(callCmd.Proc.Name); + ins.AddRange(callCmd.Ins); + outs.AddRange(callCmd.Outs); } parallelCalleeNames.Sort(); string procName = "og"; @@ -149,47 +147,52 @@ namespace Microsoft.Boogie { procName = procName + "_" + calleeName; } + Procedure proc; if (asyncAndParallelCallDesugarings.ContainsKey(procName)) - return asyncAndParallelCallDesugarings[procName]; - - List inParams = new List(); - List outParams = new List(); - List requiresSeq = new List(); - List ensuresSeq = new List(); - int count = 0; - while (callCmd != null) { - Dictionary map = new Dictionary(); - foreach (Variable x in callCmd.Proc.InParams) - { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true); - inParams.Add(y); - map[x] = new IdentifierExpr(Token.NoToken, y); - } - foreach (Variable x in callCmd.Proc.OutParams) - { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), false); - outParams.Add(y); - map[x] = new IdentifierExpr(Token.NoToken, y); - } - Contract.Assume(callCmd.Proc.TypeParameters.Count == 0); - Substitution subst = Substituter.SubstitutionFromHashtable(map); - foreach (Requires req in callCmd.Proc.Requires) + proc = asyncAndParallelCallDesugarings[procName]; + } + else + { + List inParams = new List(); + List outParams = new List(); + List requiresSeq = new List(); + List ensuresSeq = new List(); + int count = 0; + foreach (CallCmd callCmd in parCallCmd.CallCmds) { - requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition))); + Dictionary map = new Dictionary(); + foreach (Variable x in callCmd.Proc.InParams) + { + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true); + inParams.Add(y); + map[x] = new IdentifierExpr(Token.NoToken, y); + } + foreach (Variable x in callCmd.Proc.OutParams) + { + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), false); + outParams.Add(y); + map[x] = new IdentifierExpr(Token.NoToken, y); + } + Contract.Assume(callCmd.Proc.TypeParameters.Count == 0); + Substitution subst = Substituter.SubstitutionFromHashtable(map); + foreach (Requires req in callCmd.Proc.Requires) + { + requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition))); + } + foreach (Ensures ens in callCmd.Proc.Ensures) + { + ensuresSeq.Add(new Ensures(ens.Free, Substituter.Apply(subst, ens.Condition))); + } + count++; } - foreach (Ensures ens in callCmd.Proc.Ensures) - { - ensuresSeq.Add(new Ensures(ens.Free, Substituter.Apply(subst, ens.Condition))); - } - count++; - callCmd = callCmd.InParallelWith; + proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, new List(), ensuresSeq); + proc.AddAttribute("yields"); + asyncAndParallelCallDesugarings[procName] = proc; } - - Procedure proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, new List(), ensuresSeq); - proc.AddAttribute("yields"); - asyncAndParallelCallDesugarings[procName] = proc; - return proc; + CallCmd dummyCallCmd = new CallCmd(Token.NoToken, proc.Name, ins, outs); + dummyCallCmd.Proc = proc; + newCmds.Add(dummyCallCmd); } private void CreateYieldCheckerImpl(DeclWithFormals decl, List> yields, Dictionary map) @@ -301,9 +304,11 @@ namespace Microsoft.Boogie { if (cmd is YieldCmd) return true; + if (cmd is ParCallCmd) + return true; CallCmd callCmd = cmd as CallCmd; if (callCmd == null) continue; - if (callCmd.IsAsync || callCmd.InParallelWith != null || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) + if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) return true; } } @@ -407,24 +412,15 @@ namespace Microsoft.Boogie cmds.Add(pcmd); } } - CallCmd callCmd = cmd as CallCmd; - if (callCmd != null) + + if (cmd is CallCmd) { - if (callCmd.InParallelWith != null || callCmd.IsAsync || - QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) + CallCmd callCmd = cmd as CallCmd; + if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) { AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); } - if (callCmd.InParallelWith != null) - { - List ins; - List outs; - Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs); - CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs); - dummyCallCmd.Proc = dummyParallelCallDesugaring; - newCmds.Add(dummyCallCmd); - } - else if (callCmd.IsAsync) + if (callCmd.IsAsync) { if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name)) { @@ -439,8 +435,7 @@ namespace Microsoft.Boogie { newCmds.Add(callCmd); } - if (callCmd.InParallelWith != null || callCmd.IsAsync || - QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) + if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) { HashSet availableLinearVars = new HashSet(linearTypeChecker.availableLinearVars[callCmd]); foreach (IdentifierExpr ie in callCmd.Outs) @@ -452,6 +447,23 @@ namespace Microsoft.Boogie AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); } } + else if (cmd is ParCallCmd) + { + ParCallCmd parCallCmd = cmd as ParCallCmd; + AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); + DesugarParallelCallCmd(newCmds, parCallCmd); + HashSet availableLinearVars = new HashSet(linearTypeChecker.availableLinearVars[parCallCmd]); + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + foreach (IdentifierExpr ie in callCmd.Outs) + { + if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue; + availableLinearVars.Add(ie.Decl); + } + } + Dictionary domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } else { newCmds.Add(cmd); diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index d4df34b8..41fb9480 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -21,7 +21,7 @@ namespace Microsoft.Boogie HashSet globalVariables; bool globalVarAccessAllowed; bool visitingAssertion; - int phaseNumEnclosingProc; + int enclosingProcPhaseNum; public Dictionary procToActionInfo; public Program program; @@ -64,7 +64,7 @@ namespace Microsoft.Boogie this.checkingContext = new CheckingContext(null); this.program = program; this.visitingAssertion = false; - this.phaseNumEnclosingProc = int.MaxValue; + this.enclosingProcPhaseNum = int.MaxValue; } public override Block VisitBlock(Block node) { @@ -83,27 +83,71 @@ namespace Microsoft.Boogie } public override Implementation VisitImplementation(Implementation node) { - phaseNumEnclosingProc = FindPhaseNumber(node.Proc); + enclosingProcPhaseNum = FindPhaseNumber(node.Proc); return base.VisitImplementation(node); } public override Procedure VisitProcedure(Procedure node) { - phaseNumEnclosingProc = FindPhaseNumber(node); + enclosingProcPhaseNum = FindPhaseNumber(node); return base.VisitProcedure(node); } public override Cmd VisitCallCmd(CallCmd node) { globalVarAccessAllowed = false; - if (!node.IsAsync && node.InParallelWith == null) { + if (enclosingProcPhaseNum == int.MaxValue) + return base.VisitCallCmd(node); + if (!node.IsAsync) + { int calleePhaseNum = FindPhaseNumber(node.Proc); - if (!(calleePhaseNum == int.MaxValue || phaseNumEnclosingProc > calleePhaseNum)) + if (enclosingProcPhaseNum > calleePhaseNum) + { + procToActionInfo[node.Proc].callerPhaseNums.Add(enclosingProcPhaseNum); + } + else { - Error(node, "The phase of the caller procedure must be greater than the phase of the callee"); + Error(node, "The phase of the caller procedure must be greater than the phase of the callee"); } } return base.VisitCallCmd(node); } + public override Cmd VisitParCallCmd(ParCallCmd node) + { + globalVarAccessAllowed = false; + foreach (CallCmd callCmd in node.CallCmds) + { + base.VisitCallCmd(callCmd); + } + + if (enclosingProcPhaseNum == int.MaxValue) + return node; + + int maxCalleePhaseNum = 0; + foreach (CallCmd iter in node.CallCmds) + { + int calleePhaseNum = FindPhaseNumber(iter.Proc); + if (calleePhaseNum < maxCalleePhaseNum) + maxCalleePhaseNum = calleePhaseNum; + } + + if (enclosingProcPhaseNum > maxCalleePhaseNum) + { + bool isLeftMover = true; + bool isRightMover = true; + foreach (CallCmd iter in node.CallCmds) + { + ActionInfo actionInfo = procToActionInfo[iter.Proc]; + isLeftMover = isLeftMover && actionInfo.IsLeftMover; + isRightMover = isRightMover && actionInfo.IsRightMover; + actionInfo.callerPhaseNums.Add(enclosingProcPhaseNum); + } + if (!isLeftMover && !isRightMover) + { + Error(node, "The procedures in the parallel call must be all right mover or all left mover"); + } + } + return node; + } public override YieldCmd VisitYieldCmd(YieldCmd node) { globalVarAccessAllowed = true; @@ -120,7 +164,7 @@ namespace Microsoft.Boogie public override Ensures VisitEnsures(Ensures ensures) { int phaseNum = QKeyValue.FindIntAttribute(ensures.Attributes, "phase", 0); - if (phaseNum > phaseNumEnclosingProc) + if (phaseNum > enclosingProcPhaseNum) { Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure"); } @@ -132,7 +176,7 @@ namespace Microsoft.Boogie public override Requires VisitRequires(Requires requires) { int phaseNum = QKeyValue.FindIntAttribute(requires.Attributes, "phase", 0); - if (phaseNum > phaseNumEnclosingProc) + if (phaseNum > enclosingProcPhaseNum) { Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure"); } @@ -144,7 +188,7 @@ namespace Microsoft.Boogie public override Cmd VisitAssertCmd(AssertCmd node) { int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", 0); - if (phaseNum > phaseNumEnclosingProc) + if (phaseNum > enclosingProcPhaseNum) { Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure"); } @@ -156,7 +200,7 @@ namespace Microsoft.Boogie public override Cmd VisitAssumeCmd(AssumeCmd node) { int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", 0); - if (phaseNum > phaseNumEnclosingProc) + if (phaseNum > enclosingProcPhaseNum) { Error(node, "The phase of assume cannot be greater than the phase of enclosing procedure"); } diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 9afa4f45..65e91db5 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1727,8 +1727,100 @@ namespace Microsoft.Boogie { } } + public class ParCallCmd : CallCommonality, IPotentialErrorNode + { + public List CallCmds; + public ParCallCmd(IToken tok, List callCmds) + : base(tok, null) + { + this.CallCmds = callCmds; + } + public ParCallCmd(IToken tok, List callCmds, QKeyValue kv) + : base(tok, kv) + { + this.CallCmds = callCmds; + } + protected override Cmd ComputeDesugaring() + { + throw new NotImplementedException(); + } + private object errorData; + public object ErrorData + { + get + { + return errorData; + } + set + { + errorData = value; + } + } + public override void Resolve(ResolutionContext rc) + { + ResolveAttributes(Attributes, rc); + foreach (CallCmd callCmd in CallCmds) + { + callCmd.Resolve(rc); + } + HashSet parallelCallLhss = new HashSet(); + foreach (CallCmd callCmd in CallCmds) + { + foreach (IdentifierExpr ie in callCmd.Outs) + { + if (parallelCallLhss.Contains(ie.Decl)) + { + rc.Error(this, "left-hand side of parallel call command contains variable twice: {0}", ie.Name); + } + else + { + parallelCallLhss.Add(ie.Decl); + } + } + } + } + public override void Typecheck(TypecheckingContext tc) + { + TypecheckAttributes(Attributes, tc); + if (!CommandLineOptions.Clo.DoModSetAnalysis) + { + if (!tc.Yields) + { + tc.Error(this, "enclosing procedure of a parallel call must yield"); + } + foreach (CallCmd callCmd in CallCmds) + { + if (!QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields")) + { + tc.Error(callCmd, "target procedure of a parallel call must yield"); + } + if (!QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "stable")) + { + tc.Error(callCmd, "target procedure of a parallel call must be stable"); + } + } + } + foreach (CallCmd callCmd in CallCmds) + { + callCmd.Typecheck(tc); + } + } + public override void AddAssignedVariables(List vars) + { + foreach (CallCmd callCmd in CallCmds) + { + callCmd.AddAssignedVariables(vars); + } + } + public override Absy StdDispatch(StandardVisitor visitor) + { + //Contract.Requires(visitor != null); + Contract.Ensures(Contract.Result() != null); + return visitor.VisitParCallCmd(this); + } + } + public class CallCmd : CallCommonality, IPotentialErrorNode { - public CallCmd InParallelWith { get; private set; } public string/*!*/ callee { get; private set; } public Procedure Proc; @@ -1793,18 +1885,6 @@ namespace Microsoft.Boogie { this.IsAsync = IsAsync; } - public CallCmd(IToken tok, string callee, List ins, List outs, QKeyValue kv, CallCmd inParallelWith) - : base(tok, kv) - { - Contract.Requires(outs != null); - Contract.Requires(ins != null); - Contract.Requires(callee != null); - Contract.Requires(tok != null); - this.callee = callee; - this.Ins = ins; - this.Outs = outs; - this.InParallelWith = inParallelWith; - } public override void Emit(TokenTextWriter stream, int level) { //Contract.Requires(stream != null); stream.Write(this, level, ""); @@ -1860,28 +1940,19 @@ namespace Microsoft.Boogie { e.Resolve(rc); } } - Set/**/ actualOuts = new Set/**/ (Outs.Count); + HashSet actualOuts = new HashSet(); foreach (IdentifierExpr ide in Outs) { if (ide != null) { ide.Resolve(rc); if (ide.Decl != null) { - if (/* actualOuts[ide.Decl] */ rc.parallelCallLhss.Contains(ide.Decl)) { + if (actualOuts.Contains(ide.Decl)) { rc.Error(this, "left-hand side of call command contains variable twice: {0}", ide.Name); } else { actualOuts.Add(ide.Decl); - rc.parallelCallLhss.Add(ide.Decl); } } } } - if (InParallelWith != null) - { - InParallelWith.Resolve(rc); - } - foreach (Variable v in actualOuts) - { - rc.parallelCallLhss.Remove(v); - } if (Proc == null) return; @@ -1907,11 +1978,6 @@ namespace Microsoft.Boogie { rc.Error(this.tok, "a procedure called asynchronously can have no output parameters"); return; } - if (InParallelWith != null) - { - rc.Error(this.tok, "an asynchronous procedure call cannot be parallel"); - return; - } } // Check that type parameters can be determined using the given @@ -2009,30 +2075,20 @@ namespace Microsoft.Boogie { TypeParameters = SimpleTypeParamInstantiation.From(Proc.TypeParameters, actualTypeParams); - if (!CommandLineOptions.Clo.DoModSetAnalysis && (IsAsync || InParallelWith != null)) + if (!CommandLineOptions.Clo.DoModSetAnalysis && IsAsync) { if (!tc.Yields) { - tc.Error(this, "enclosing procedure of a parallel or async call must yield"); + tc.Error(this, "enclosing procedure of an async call must yield"); } - var curr = this; - while (curr != null) + if (!QKeyValue.FindBoolAttribute(Proc.Attributes, "yields")) { - if (!QKeyValue.FindBoolAttribute(curr.Proc.Attributes, "yields")) - { - tc.Error(curr, "target procedure of a parallel or async call must yield"); - } - if (!QKeyValue.FindBoolAttribute(curr.Proc.Attributes, "stable")) - { - tc.Error(curr, "target procedure of a parallel or async call must be stable"); - } - curr = curr.InParallelWith; + tc.Error(this, "target procedure of an async call must yield"); + } + if (!QKeyValue.FindBoolAttribute(Proc.Attributes, "stable")) + { + tc.Error(this, "target procedure of an async call must be stable"); } - } - - if (InParallelWith != null) - { - InParallelWith.Typecheck(tc); } } diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index a8ba40ff..42bb7b34 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -4,7 +4,6 @@ //--------------------------------------------------------------------------*/ /*using System;*/ -using PureCollections; using System.Collections; using System.Collections.Generic; using System.IO; @@ -305,20 +304,20 @@ Type ( TypeAtom | - Ident (. List/*!*/ args = new List (); .) + Ident (. List/*!*/ args = new List (); .) [ TypeArgs ] (. ty = new UnresolvedTypeIdentifier (tok, tok.val, args); .) | MapType ) . -TypeArgs<.List/*!*/ ts.> +TypeArgs<.List/*!*/ ts.> = (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .) ( TypeAtom (. ts.Add(ty); .) [ TypeArgs ] | - Ident (. List/*!*/ args = new List (); + Ident (. List/*!*/ args = new List (); ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); .) [ TypeArgs ] | @@ -342,7 +341,7 @@ TypeAtom MapType = (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null; IToken/*!*/ nnTok; - List/*!*/ arguments = new List(); + List/*!*/ arguments = new List(); Bpl.Type/*!*/ result; List/*!*/ typeParameters = new List(); .) @@ -369,7 +368,7 @@ TypeParams<.out IToken/*!*/ tok, out List/*!*/ typeParams.> .) . -Types<.List/*!*/ ts.> +Types<.List/*!*/ ts.> = (. Contract.Requires(ts != null); Bpl.Type/*!*/ ty; .) Type (. ts.Add(ty); .) { "," Type (. ts.Add(ty); .) @@ -864,6 +863,7 @@ LabelOrCmd c = new HavocCmd(x,ids); .) | CallCmd ";" (. c = cn; .) + | ParCallCmd (. c = cn; .) | "yield" (. x = t; .) ";" (. c = new YieldCmd(x); .) ) @@ -935,18 +935,32 @@ CallCmd ] "call" (. x = t; .) { Attribute } - CallParams (. .) - { "|" CallParams (. .) + CallParams (. .) + . + +ParCallCmd += (. Contract.Ensures(Contract.ValueAtReturn(out d) != null); + IToken x; + QKeyValue kv = null; + Cmd c = null; + List callCmds = new List(); + .) + "par" (. x = t; .) + { Attribute } + CallParams (. callCmds.Add((CallCmd)c); .) + { "|" CallParams (. callCmds.Add((CallCmd)c); .) } + ";" (. d = new ParCallCmd(x, callCmds, kv); .) . -CallParams +CallParams = (. List ids = new List(); List es = new List(); Expr en; IToken first; IToken p; + c = null; .) Ident ( "(" @@ -954,7 +968,7 @@ CallParams { "," Expression (. es.Add(en); .) } ] - ")" (. c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .) + ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .) | (. ids.Add(new IdentifierExpr(first, first.val)); .) [ "," Ident (. ids.Add(new IdentifierExpr(p, p.val)); .) @@ -966,7 +980,7 @@ CallParams { "," Expression (. es.Add(en); .) } ] - ")" (. c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .) + ")" (. c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; .) ) . diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 06ef2c27..59f03aac 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -199,9 +199,8 @@ namespace Microsoft.Boogie { Cmd ret = base.VisitCallCmd(callCmd); foreach (IdentifierExpr ie in callCmd.Outs) { - if(ie != null) ProcessVariable(ie.Decl); + if (ie != null) ProcessVariable(ie.Decl); } - Procedure callee = callCmd.Proc; if (callee == null) return ret; @@ -210,28 +209,43 @@ namespace Microsoft.Boogie { ProcessVariable(var); } } - if (!yieldingProcs.Contains(enclosingProc) && - (yieldingProcs.Contains(callCmd.Proc) || callCmd.IsAsync || callCmd.InParallelWith != null)) + if (!yieldingProcs.Contains(enclosingProc) && (yieldingProcs.Contains(callCmd.Proc) || callCmd.IsAsync)) { yieldingProcs.Add(enclosingProc); moreProcessingRequired = true; } - if (callCmd.IsAsync || callCmd.InParallelWith != null) + if (callCmd.IsAsync) { - var curr = callCmd; - while (curr != null) + asyncAndParallelCallTargetProcs.Add(callCmd.Proc); + if (!yieldingProcs.Contains(callCmd.Proc)) { - asyncAndParallelCallTargetProcs.Add(curr.Proc); - if (!yieldingProcs.Contains(curr.Proc)) - { - yieldingProcs.Add(curr.Proc); - moreProcessingRequired = true; - } - curr = curr.InParallelWith; + yieldingProcs.Add(callCmd.Proc); + moreProcessingRequired = true; } } return ret; } + public override Cmd VisitParCallCmd(ParCallCmd node) + { + //Contract.Requires(callCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitParCallCmd(node); + if (!yieldingProcs.Contains(enclosingProc)) + { + yieldingProcs.Add(enclosingProc); + moreProcessingRequired = true; + } + foreach (CallCmd callCmd in node.CallCmds) + { + asyncAndParallelCallTargetProcs.Add(callCmd.Proc); + if (!yieldingProcs.Contains(callCmd.Proc)) + { + yieldingProcs.Add(callCmd.Proc); + moreProcessingRequired = true; + } + } + return ret; + } private static void ProcessVariable(Variable var) { Procedure/*!*/ localProc = cce.NonNull(enclosingProc); if (var == null) diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 402ea7dc..056a47f9 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -107,12 +107,21 @@ namespace Microsoft.Boogie { public override Cmd VisitCallCmd(CallCmd node) { //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); - CallCmd/*!*/ clone = (CallCmd)node.Clone(); + CallCmd clone = (CallCmd)node.Clone(); Contract.Assert(clone != null); clone.Ins = new List(clone.Ins); clone.Outs = new List(clone.Outs); return base.VisitCallCmd(clone); } + public override Cmd VisitParCallCmd(ParCallCmd node) + { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + ParCallCmd clone = (ParCallCmd)node.Clone(); + Contract.Assert(clone != null); + clone.CallCmds = new List(node.CallCmds); + return base.VisitParCallCmd(clone); + } public override Choice VisitChoice(Choice node) { //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 310e3cc0..6c70fca4 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -12,8 +12,6 @@ using Bpl = Microsoft.Boogie; using System; using System.Diagnostics.Contracts; -namespace Microsoft.Boogie { - public class Parser { @@ -24,7 +22,7 @@ public class Parser { public const int _string = 4; public const int _decimal = 5; public const int _float = 6; - public const int maxT = 95; + public const int maxT = 96; const bool T = true; const bool x = false; @@ -362,7 +360,7 @@ private class BvBounds : Expr { Get(); Type(out retTy); retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); - } else SynErr(96); + } else SynErr(97); if (la.kind == 27) { Get(); Expression(out tmp); @@ -370,7 +368,7 @@ private class BvBounds : Expr { Expect(28); } else if (la.kind == 8) { Get(); - } else SynErr(97); + } else SynErr(98); if (retTyd == null) { // construct a dummy type for the case of syntax error retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int)); @@ -493,7 +491,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors); - } else SynErr(98); + } else SynErr(99); proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); } @@ -598,14 +596,14 @@ private class BvBounds : Expr { TypeAtom(out ty); } else if (la.kind == 1) { Ident(out tok); - List/*!*/ args = new List (); + List/*!*/ args = new List (); if (StartOf(6)) { TypeArgs(args); } ty = new UnresolvedTypeIdentifier (tok, tok.val, args); } else if (la.kind == 17 || la.kind == 19) { MapType(out ty); - } else SynErr(99); + } else SynErr(100); } void AttributesIdsTypeWhere(bool allowAttributes, bool allowWhereClauses, string context, System.Action action ) { @@ -646,7 +644,7 @@ private class BvBounds : Expr { void Expression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; ImpliesExpression(false, out e0); - while (la.kind == 54 || la.kind == 55) { + while (la.kind == 55 || la.kind == 56) { EquivOp(); x = t; ImpliesExpression(false, out e1); @@ -669,7 +667,7 @@ private class BvBounds : Expr { Get(); Type(out ty); Expect(10); - } else SynErr(100); + } else SynErr(101); } void Ident(out IToken/*!*/ x) { @@ -681,7 +679,7 @@ private class BvBounds : Expr { } - void TypeArgs(List/*!*/ ts) { + void TypeArgs(List/*!*/ ts) { Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; if (StartOf(5)) { TypeAtom(out ty); @@ -691,7 +689,7 @@ private class BvBounds : Expr { } } else if (la.kind == 1) { Ident(out tok); - List/*!*/ args = new List (); + List/*!*/ args = new List (); ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); if (StartOf(6)) { TypeArgs(ts); @@ -699,13 +697,13 @@ private class BvBounds : Expr { } else if (la.kind == 17 || la.kind == 19) { MapType(out ty); ts.Add(ty); - } else SynErr(101); + } else SynErr(102); } void MapType(out Bpl.Type/*!*/ ty) { Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null; IToken/*!*/ nnTok; - List/*!*/ arguments = new List(); + List/*!*/ arguments = new List(); Bpl.Type/*!*/ result; List/*!*/ typeParameters = new List(); @@ -737,7 +735,7 @@ private class BvBounds : Expr { } - void Types(List/*!*/ ts) { + void Types(List/*!*/ ts) { Contract.Requires(ts != null); Bpl.Type/*!*/ ty; Type(out ty); ts.Add(ty); @@ -884,7 +882,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { SpecPrePost(true, pre, post); } else if (la.kind == 36 || la.kind == 37) { SpecPrePost(false, pre, post); - } else SynErr(102); + } else SynErr(103); } void ImplBody(out List/*!*/ locals, out StmtList/*!*/ stmtList) { @@ -916,7 +914,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Proposition(out e); Expect(8); post.Add(new Ensures(tok, free, e, null, kv)); - } else SynErr(103); + } else SynErr(104); } void StmtList(out StmtList/*!*/ stmtList) { @@ -1043,6 +1041,11 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { c = cn; break; } + case 53: { + ParCallCmd(out cn); + c = cn; + break; + } case 49: { Get(); x = t; @@ -1050,7 +1053,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { c = new YieldCmd(x); break; } - default: SynErr(104); break; + default: SynErr(105); break; } } @@ -1067,7 +1070,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 45) { BreakCmd(out bcmd); ec = bcmd; - } else SynErr(105); + } else SynErr(106); } void TransferCmd(out TransferCmd/*!*/ tc) { @@ -1087,7 +1090,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 39) { Get(); tc = new ReturnCmd(t); - } else SynErr(106); + } else SynErr(107); Expect(8); } @@ -1112,7 +1115,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Get(); StmtList(out els); elseOption = els; - } else SynErr(107); + } else SynErr(108); } ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); } @@ -1175,7 +1178,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (StartOf(9)) { Expression(out ee); e = ee; - } else SynErr(108); + } else SynErr(109); Expect(10); } @@ -1222,7 +1225,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } Expect(8); c = new AssignCmd(x, lhss, rhss); - } else SynErr(109); + } else SynErr(110); } void CallCmd(out Cmd c) { @@ -1246,13 +1249,31 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { while (la.kind == 27) { Attribute(ref kv); } - CallParams(isAsync, isFree, kv, x, ref c); + CallParams(isAsync, isFree, kv, x, out c); - while (la.kind == 53) { + } + + void ParCallCmd(out Cmd d) { + Contract.Ensures(Contract.ValueAtReturn(out d) != null); + IToken x; + QKeyValue kv = null; + Cmd c = null; + List callCmds = new List(); + + Expect(53); + x = t; + while (la.kind == 27) { + Attribute(ref kv); + } + CallParams(false, false, kv, x, out c); + callCmds.Add((CallCmd)c); + while (la.kind == 54) { Get(); - CallParams(isAsync, isFree, kv, x, ref c); - + CallParams(false, false, kv, x, out c); + callCmds.Add((CallCmd)c); } + Expect(8); + d = new ParCallCmd(x, callCmds, kv); } void MapAssignIndex(out IToken/*!*/ x, out List/*!*/ indexes) { @@ -1273,12 +1294,13 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Expect(18); } - void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, ref Cmd c) { + void CallParams(bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c) { List ids = new List(); List es = new List(); Expr en; IToken first; IToken p; + c = null; Ident(out first); if (la.kind == 9) { @@ -1293,7 +1315,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } } Expect(10); - c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; + c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; } else if (la.kind == 12 || la.kind == 50) { ids.Add(new IdentifierExpr(first, first.val)); if (la.kind == 12) { @@ -1319,8 +1341,8 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } } Expect(10); - c = new CallCmd(x, first.val, es, ids, kv, (CallCmd) c); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; - } else SynErr(110); + c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; + } else SynErr(111); } void Expressions(out List/*!*/ es) { @@ -1338,7 +1360,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; LogicalExpression(out e0); if (StartOf(10)) { - if (la.kind == 56 || la.kind == 57) { + if (la.kind == 57 || la.kind == 58) { ImpliesOp(); x = t; ImpliesExpression(true, out e1); @@ -1350,7 +1372,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { x = t; LogicalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 58 || la.kind == 59) { + while (la.kind == 59 || la.kind == 60) { ExpliesOp(); x = t; LogicalExpression(out e1); @@ -1361,23 +1383,23 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void EquivOp() { - if (la.kind == 54) { + if (la.kind == 55) { Get(); - } else if (la.kind == 55) { + } else if (la.kind == 56) { Get(); - } else SynErr(111); + } else SynErr(112); } void LogicalExpression(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; RelationalExpression(out e0); if (StartOf(11)) { - if (la.kind == 60 || la.kind == 61) { + if (la.kind == 61 || la.kind == 62) { AndOp(); x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 60 || la.kind == 61) { + while (la.kind == 61 || la.kind == 62) { AndOp(); x = t; RelationalExpression(out e1); @@ -1388,7 +1410,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { x = t; RelationalExpression(out e1); e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 62 || la.kind == 63) { + while (la.kind == 63 || la.kind == 64) { OrOp(); x = t; RelationalExpression(out e1); @@ -1399,19 +1421,19 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void ImpliesOp() { - if (la.kind == 56) { + if (la.kind == 57) { Get(); - } else if (la.kind == 57) { + } else if (la.kind == 58) { Get(); - } else SynErr(112); + } else SynErr(113); } void ExpliesOp() { - if (la.kind == 58) { + if (la.kind == 59) { Get(); - } else if (la.kind == 59) { + } else if (la.kind == 60) { Get(); - } else SynErr(113); + } else SynErr(114); } void RelationalExpression(out Expr/*!*/ e0) { @@ -1425,25 +1447,25 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void AndOp() { - if (la.kind == 60) { + if (la.kind == 61) { Get(); - } else if (la.kind == 61) { + } else if (la.kind == 62) { Get(); - } else SynErr(114); + } else SynErr(115); } void OrOp() { - if (la.kind == 62) { + if (la.kind == 63) { Get(); - } else if (la.kind == 63) { + } else if (la.kind == 64) { Get(); - } else SynErr(115); + } else SynErr(116); } void BvTerm(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; Term(out e0); - while (la.kind == 72) { + while (la.kind == 73) { Get(); x = t; Term(out e1); @@ -1454,7 +1476,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; switch (la.kind) { - case 64: { + case 65: { Get(); x = t; op=BinaryOperator.Opcode.Eq; break; @@ -1469,49 +1491,49 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { x = t; op=BinaryOperator.Opcode.Gt; break; } - case 65: { + case 66: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 66: { + case 67: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - case 67: { + case 68: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 68: { + case 69: { Get(); x = t; op=BinaryOperator.Opcode.Subtype; break; } - case 69: { + case 70: { Get(); x = t; op=BinaryOperator.Opcode.Neq; break; } - case 70: { + case 71: { Get(); x = t; op=BinaryOperator.Opcode.Le; break; } - case 71: { + case 72: { Get(); x = t; op=BinaryOperator.Opcode.Ge; break; } - default: SynErr(116); break; + default: SynErr(117); break; } } void Term(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; Factor(out e0); - while (la.kind == 73 || la.kind == 74) { + while (la.kind == 74 || la.kind == 75) { AddOp(out x, out op); Factor(out e1); e0 = Expr.Binary(x, op, e0, e1); @@ -1530,19 +1552,19 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) { Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 73) { + if (la.kind == 74) { Get(); x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 74) { + } else if (la.kind == 75) { Get(); x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(117); + } else SynErr(118); } void Power(out Expr/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; UnaryExpression(out e0); - if (la.kind == 78) { + if (la.kind == 79) { Get(); x = t; Power(out e1); @@ -1555,43 +1577,43 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { if (la.kind == 44) { Get(); x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 75) { + } else if (la.kind == 76) { Get(); x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 76) { + } else if (la.kind == 77) { Get(); x = t; op=BinaryOperator.Opcode.Mod; - } else if (la.kind == 77) { + } else if (la.kind == 78) { Get(); x = t; op=BinaryOperator.Opcode.RealDiv; - } else SynErr(118); + } else SynErr(119); } void UnaryExpression(out Expr/*!*/ e) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; - if (la.kind == 74) { + if (la.kind == 75) { Get(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); - } else if (la.kind == 79 || la.kind == 80) { + } else if (la.kind == 80 || la.kind == 81) { NegOp(); x = t; UnaryExpression(out e); e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); } else if (StartOf(14)) { CoercionExpression(out e); - } else SynErr(119); + } else SynErr(120); } void NegOp() { - if (la.kind == 79) { + if (la.kind == 80) { Get(); - } else if (la.kind == 80) { + } else if (la.kind == 81) { Get(); - } else SynErr(120); + } else SynErr(121); } void CoercionExpression(out Expr/*!*/ e) { @@ -1615,7 +1637,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum); } - } else SynErr(121); + } else SynErr(122); } } @@ -1696,12 +1718,12 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { List/*!*/ blocks; switch (la.kind) { - case 81: { + case 82: { Get(); e = new LiteralExpr(t, false); break; } - case 82: { + case 83: { Get(); e = new LiteralExpr(t, true); break; @@ -1731,12 +1753,12 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { e = new NAryExpr(x, new FunctionCall(id), es); } else if (la.kind == 10) { e = new NAryExpr(x, new FunctionCall(id), new List()); - } else SynErr(122); + } else SynErr(123); Expect(10); } break; } - case 83: { + case 84: { Get(); x = t; Expect(9); @@ -1770,19 +1792,19 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { if (e is BvBounds) this.SemErr("parentheses around bitvector bounds " + "are not allowed"); - } else if (la.kind == 87 || la.kind == 88) { + } else if (la.kind == 88 || la.kind == 89) { Forall(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ForallExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 89 || la.kind == 90) { + } else if (la.kind == 90 || la.kind == 91) { Exists(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); if (typeParams.Count + ds.Count > 0) e = new ExistsExpr(x, typeParams, ds, kv, trig, e); - } else if (la.kind == 91 || la.kind == 92) { + } else if (la.kind == 92 || la.kind == 93) { Lambda(); x = t; QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e); @@ -1790,7 +1812,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { SemErr("triggers not allowed in lambda expressions"); if (typeParams.Count + ds.Count > 0) e = new LambdaExpr(x, typeParams, ds, kv, e); - } else SynErr(123); + } else SynErr(124); Expect(10); break; } @@ -1798,12 +1820,12 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { IfThenElseExpression(out e); break; } - case 84: { + case 85: { CodeExpression(out locals, out blocks); e = new CodeExpr(locals, blocks); break; } - default: SynErr(124); break; + default: SynErr(125); break; } } @@ -1815,7 +1837,7 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } else if (la.kind == 6) { Get(); s = t.val; - } else SynErr(125); + } else SynErr(126); try { n = BigDec.FromString(s); } catch (FormatException) { @@ -1842,11 +1864,11 @@ out List/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { } void Forall() { - if (la.kind == 87) { + if (la.kind == 88) { Get(); - } else if (la.kind == 88) { + } else if (la.kind == 89) { Get(); - } else SynErr(126); + } else SynErr(127); } void QuantifierBody(IToken/*!*/ q, out List/*!*/ typeParams, out List/*!*/ ds, @@ -1864,7 +1886,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } } else if (la.kind == 1 || la.kind == 27) { BoundVars(q, out ds); - } else SynErr(127); + } else SynErr(128); QSep(); while (la.kind == 27) { AttributeOrTrigger(ref kv, ref trig); @@ -1873,19 +1895,19 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } void Exists() { - if (la.kind == 89) { + if (la.kind == 90) { Get(); - } else if (la.kind == 90) { + } else if (la.kind == 91) { Get(); - } else SynErr(128); + } else SynErr(129); } void Lambda() { - if (la.kind == 91) { + if (la.kind == 92) { Get(); - } else if (la.kind == 92) { + } else if (la.kind == 93) { Get(); - } else SynErr(129); + } else SynErr(130); } void IfThenElseExpression(out Expr/*!*/ e) { @@ -1896,7 +1918,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Expect(40); tok = t; Expression(out e0); - Expect(86); + Expect(87); Expression(out e1); Expect(41); Expression(out e2); @@ -1907,7 +1929,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List(); Block/*!*/ b; blocks = new List(); - Expect(84); + Expect(85); while (la.kind == 7) { LocalVars(locals); } @@ -1917,7 +1939,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { SpecBlock(out b); blocks.Add(b); } - Expect(85); + Expect(86); } void SpecBlock(out Block/*!*/ b) { @@ -1955,7 +1977,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Get(); Expression(out e); b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(130); + } else SynErr(131); Expect(8); } @@ -2012,7 +2034,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { trig.AddLast(new Trigger(tok, true, es, null)); } - } else SynErr(131); + } else SynErr(132); Expect(28); } @@ -2027,15 +2049,15 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } else if (StartOf(9)) { Expression(out e); o = e; - } else SynErr(132); + } else SynErr(133); } void QSep() { - if (la.kind == 93) { + if (la.kind == 94) { Get(); - } else if (la.kind == 94) { + } else if (la.kind == 95) { Get(); - } else SynErr(133); + } else SynErr(134); } @@ -2051,23 +2073,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { } static readonly bool[,]/*!*/ set = { - {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x} + {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x}, + {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x} }; } // end Parser @@ -2145,87 +2167,88 @@ public class Errors { case 50: s = "\":=\" expected"; break; case 51: s = "\"async\" expected"; break; case 52: s = "\"call\" expected"; break; - case 53: s = "\"|\" expected"; break; - case 54: s = "\"<==>\" expected"; break; - case 55: s = "\"\\u21d4\" expected"; break; - case 56: s = "\"==>\" expected"; break; - case 57: s = "\"\\u21d2\" expected"; break; - case 58: s = "\"<==\" expected"; break; - case 59: s = "\"\\u21d0\" expected"; break; - case 60: s = "\"&&\" expected"; break; - case 61: s = "\"\\u2227\" expected"; break; - case 62: s = "\"||\" expected"; break; - case 63: s = "\"\\u2228\" expected"; break; - case 64: s = "\"==\" expected"; break; - case 65: s = "\"<=\" expected"; break; - case 66: s = "\">=\" expected"; break; - case 67: s = "\"!=\" expected"; break; - case 68: s = "\"<:\" expected"; break; - case 69: s = "\"\\u2260\" expected"; break; - case 70: s = "\"\\u2264\" expected"; break; - case 71: s = "\"\\u2265\" expected"; break; - case 72: s = "\"++\" expected"; break; - case 73: s = "\"+\" expected"; break; - case 74: s = "\"-\" expected"; break; - case 75: s = "\"div\" expected"; break; - case 76: s = "\"mod\" expected"; break; - case 77: s = "\"/\" expected"; break; - case 78: s = "\"**\" expected"; break; - case 79: s = "\"!\" expected"; break; - case 80: s = "\"\\u00ac\" expected"; break; - case 81: s = "\"false\" expected"; break; - case 82: s = "\"true\" expected"; break; - case 83: s = "\"old\" expected"; break; - case 84: s = "\"|{\" expected"; break; - case 85: s = "\"}|\" expected"; break; - case 86: s = "\"then\" expected"; break; - case 87: s = "\"forall\" expected"; break; - case 88: s = "\"\\u2200\" expected"; break; - case 89: s = "\"exists\" expected"; break; - case 90: s = "\"\\u2203\" expected"; break; - case 91: s = "\"lambda\" expected"; break; - case 92: s = "\"\\u03bb\" expected"; break; - case 93: s = "\"::\" expected"; break; - case 94: s = "\"\\u2022\" expected"; break; - case 95: s = "??? expected"; break; - case 96: s = "invalid Function"; break; + case 53: s = "\"par\" expected"; break; + case 54: s = "\"|\" expected"; break; + case 55: s = "\"<==>\" expected"; break; + case 56: s = "\"\\u21d4\" expected"; break; + case 57: s = "\"==>\" expected"; break; + case 58: s = "\"\\u21d2\" expected"; break; + case 59: s = "\"<==\" expected"; break; + case 60: s = "\"\\u21d0\" expected"; break; + case 61: s = "\"&&\" expected"; break; + case 62: s = "\"\\u2227\" expected"; break; + case 63: s = "\"||\" expected"; break; + case 64: s = "\"\\u2228\" expected"; break; + case 65: s = "\"==\" expected"; break; + case 66: s = "\"<=\" expected"; break; + case 67: s = "\">=\" expected"; break; + case 68: s = "\"!=\" expected"; break; + case 69: s = "\"<:\" expected"; break; + case 70: s = "\"\\u2260\" expected"; break; + case 71: s = "\"\\u2264\" expected"; break; + case 72: s = "\"\\u2265\" expected"; break; + case 73: s = "\"++\" expected"; break; + case 74: s = "\"+\" expected"; break; + case 75: s = "\"-\" expected"; break; + case 76: s = "\"div\" expected"; break; + case 77: s = "\"mod\" expected"; break; + case 78: s = "\"/\" expected"; break; + case 79: s = "\"**\" expected"; break; + case 80: s = "\"!\" expected"; break; + case 81: s = "\"\\u00ac\" expected"; break; + case 82: s = "\"false\" expected"; break; + case 83: s = "\"true\" expected"; break; + case 84: s = "\"old\" expected"; break; + case 85: s = "\"|{\" expected"; break; + case 86: s = "\"}|\" expected"; break; + case 87: s = "\"then\" expected"; break; + case 88: s = "\"forall\" expected"; break; + case 89: s = "\"\\u2200\" expected"; break; + case 90: s = "\"exists\" expected"; break; + case 91: s = "\"\\u2203\" expected"; break; + case 92: s = "\"lambda\" expected"; break; + case 93: s = "\"\\u03bb\" expected"; break; + case 94: s = "\"::\" expected"; break; + case 95: s = "\"\\u2022\" expected"; break; + case 96: s = "??? expected"; break; case 97: s = "invalid Function"; break; - case 98: s = "invalid Procedure"; break; - case 99: s = "invalid Type"; break; - case 100: s = "invalid TypeAtom"; break; - case 101: s = "invalid TypeArgs"; break; - case 102: s = "invalid Spec"; break; - case 103: s = "invalid SpecPrePost"; break; - case 104: s = "invalid LabelOrCmd"; break; - case 105: s = "invalid StructuredCmd"; break; - case 106: s = "invalid TransferCmd"; break; - case 107: s = "invalid IfCmd"; break; - case 108: s = "invalid Guard"; break; - case 109: s = "invalid LabelOrAssign"; break; - case 110: s = "invalid CallParams"; break; - case 111: s = "invalid EquivOp"; break; - case 112: s = "invalid ImpliesOp"; break; - case 113: s = "invalid ExpliesOp"; break; - case 114: s = "invalid AndOp"; break; - case 115: s = "invalid OrOp"; break; - case 116: s = "invalid RelOp"; break; - case 117: s = "invalid AddOp"; break; - case 118: s = "invalid MulOp"; break; - case 119: s = "invalid UnaryExpression"; break; - case 120: s = "invalid NegOp"; break; - case 121: s = "invalid CoercionExpression"; break; - case 122: s = "invalid AtomExpression"; break; + case 98: s = "invalid Function"; break; + case 99: s = "invalid Procedure"; break; + case 100: s = "invalid Type"; break; + case 101: s = "invalid TypeAtom"; break; + case 102: s = "invalid TypeArgs"; break; + case 103: s = "invalid Spec"; break; + case 104: s = "invalid SpecPrePost"; break; + case 105: s = "invalid LabelOrCmd"; break; + case 106: s = "invalid StructuredCmd"; break; + case 107: s = "invalid TransferCmd"; break; + case 108: s = "invalid IfCmd"; break; + case 109: s = "invalid Guard"; break; + case 110: s = "invalid LabelOrAssign"; break; + case 111: s = "invalid CallParams"; break; + case 112: s = "invalid EquivOp"; break; + case 113: s = "invalid ImpliesOp"; break; + case 114: s = "invalid ExpliesOp"; break; + case 115: s = "invalid AndOp"; break; + case 116: s = "invalid OrOp"; break; + case 117: s = "invalid RelOp"; break; + case 118: s = "invalid AddOp"; break; + case 119: s = "invalid MulOp"; break; + case 120: s = "invalid UnaryExpression"; break; + case 121: s = "invalid NegOp"; break; + case 122: s = "invalid CoercionExpression"; break; case 123: s = "invalid AtomExpression"; break; case 124: s = "invalid AtomExpression"; break; - case 125: s = "invalid Dec"; break; - case 126: s = "invalid Forall"; break; - case 127: s = "invalid QuantifierBody"; break; - case 128: s = "invalid Exists"; break; - case 129: s = "invalid Lambda"; break; - case 130: s = "invalid SpecBlock"; break; - case 131: s = "invalid AttributeOrTrigger"; break; - case 132: s = "invalid AttributeParameter"; break; - case 133: s = "invalid QSep"; break; + case 125: s = "invalid AtomExpression"; break; + case 126: s = "invalid Dec"; break; + case 127: s = "invalid Forall"; break; + case 128: s = "invalid QuantifierBody"; break; + case 129: s = "invalid Exists"; break; + case 130: s = "invalid Lambda"; break; + case 131: s = "invalid SpecBlock"; break; + case 132: s = "invalid AttributeOrTrigger"; break; + case 133: s = "invalid AttributeParameter"; break; + case 134: s = "invalid QSep"; break; default: s = "error " + n; break; } @@ -2244,12 +2267,6 @@ public class Errors { count++; } - public void Warning(IToken/*!*/ tok, string/*!*/ msg) { // warnings - Contract.Requires(tok != null); - Contract.Requires(msg != null); - Warning(tok.filename, tok.line, tok.col, msg); - } - public virtual void Warning(string filename, int line, int col, string msg) { Contract.Requires(msg != null); errorStream.WriteLine(warningMsgFormat, filename, line, col, msg); @@ -2262,4 +2279,3 @@ public class FatalError: Exception { } -} \ No newline at end of file diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index dcc9e346..65bc3461 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -552,8 +552,6 @@ namespace Microsoft.Boogie { cce.EndExpose(); } } - - public HashSet parallelCallLhss = new HashSet(); } public class TypecheckingContext : CheckingContext { diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index fded8dea..f0c9063d 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -8,7 +8,7 @@ using System.Diagnostics.Contracts; using Microsoft.Boogie; -namespace Microsoft.Boogie { + //----------------------------------------------------------------------------------- // Buffer @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner { const char EOL = '\n'; const int eofSym = 0; /* pdt */ - const int maxT = 95; - const int noSym = 95; + const int maxT = 96; + const int noSym = 96; [ContractInvariantMethod] @@ -520,15 +520,16 @@ public class Scanner { case "yield": t.kind = 49; break; case "async": t.kind = 51; break; case "call": t.kind = 52; break; - case "div": t.kind = 75; break; - case "mod": t.kind = 76; break; - case "false": t.kind = 81; break; - case "true": t.kind = 82; break; - case "old": t.kind = 83; break; - case "then": t.kind = 86; break; - case "forall": t.kind = 87; break; - case "exists": t.kind = 89; break; - case "lambda": t.kind = 91; break; + case "par": t.kind = 53; break; + case "div": t.kind = 76; break; + case "mod": t.kind = 77; break; + case "false": t.kind = 82; break; + case "true": t.kind = 83; break; + case "old": t.kind = 84; break; + case "then": t.kind = 87; break; + case "forall": t.kind = 88; break; + case "exists": t.kind = 90; break; + case "lambda": t.kind = 92; break; default: break; } } @@ -650,62 +651,62 @@ public class Scanner { case 26: {t.kind = 50; break;} case 27: - {t.kind = 54; break;} - case 28: {t.kind = 55; break;} - case 29: + case 28: {t.kind = 56; break;} - case 30: + case 29: {t.kind = 57; break;} + case 30: + {t.kind = 58; break;} case 31: - {t.kind = 59; break;} + {t.kind = 60; break;} case 32: if (ch == '&') {AddCh(); goto case 33;} else {goto case 0;} case 33: - {t.kind = 60; break;} - case 34: {t.kind = 61; break;} - case 35: + case 34: {t.kind = 62; break;} - case 36: + case 35: {t.kind = 63; break;} + case 36: + {t.kind = 64; break;} case 37: - {t.kind = 66; break;} - case 38: {t.kind = 67; break;} - case 39: + case 38: {t.kind = 68; break;} - case 40: + case 39: {t.kind = 69; break;} - case 41: + case 40: {t.kind = 70; break;} - case 42: + case 41: {t.kind = 71; break;} - case 43: + case 42: {t.kind = 72; break;} + case 43: + {t.kind = 73; break;} case 44: - {t.kind = 74; break;} + {t.kind = 75; break;} case 45: - {t.kind = 77; break;} - case 46: {t.kind = 78; break;} + case 46: + {t.kind = 79; break;} case 47: - {t.kind = 80; break;} + {t.kind = 81; break;} case 48: - {t.kind = 84; break;} - case 49: {t.kind = 85; break;} + case 49: + {t.kind = 86; break;} case 50: - {t.kind = 88; break;} + {t.kind = 89; break;} case 51: - {t.kind = 90; break;} + {t.kind = 91; break;} case 52: - {t.kind = 92; break;} - case 53: {t.kind = 93; break;} - case 54: + case 53: {t.kind = 94; break;} + case 54: + {t.kind = 95; break;} case 55: recEnd = pos; recKind = 11; if (ch == '=') {AddCh(); goto case 26;} @@ -733,30 +734,30 @@ public class Scanner { if (ch == '*') {AddCh(); goto case 46;} else {t.kind = 44; break;} case 61: - recEnd = pos; recKind = 53; + recEnd = pos; recKind = 54; if (ch == '|') {AddCh(); goto case 35;} else if (ch == '{') {AddCh(); goto case 48;} - else {t.kind = 53; break;} + else {t.kind = 54; break;} case 62: - recEnd = pos; recKind = 79; + recEnd = pos; recKind = 80; if (ch == '=') {AddCh(); goto case 38;} - else {t.kind = 79; break;} + else {t.kind = 80; break;} case 63: - recEnd = pos; recKind = 73; + recEnd = pos; recKind = 74; if (ch == '+') {AddCh(); goto case 43;} - else {t.kind = 73; break;} + else {t.kind = 74; break;} case 64: - recEnd = pos; recKind = 65; + recEnd = pos; recKind = 66; if (ch == '=') {AddCh(); goto case 66;} - else {t.kind = 65; break;} + else {t.kind = 66; break;} case 65: - recEnd = pos; recKind = 64; + recEnd = pos; recKind = 65; if (ch == '>') {AddCh(); goto case 29;} - else {t.kind = 64; break;} + else {t.kind = 65; break;} case 66: - recEnd = pos; recKind = 58; + recEnd = pos; recKind = 59; if (ch == '>') {AddCh(); goto case 27;} - else {t.kind = 58; break;} + else {t.kind = 59; break;} } t.val = new String(tval, 0, tlen); @@ -802,4 +803,3 @@ public class Scanner { public delegate void ErrorProc(int n, string filename, int line, int col); -} \ No newline at end of file diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 556676da..cd59638b 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -174,6 +174,17 @@ namespace Microsoft.Boogie { node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(node.Outs[i])); return node; } + public virtual Cmd VisitParCallCmd(ParCallCmd node) + { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + for (int i = 0; i < node.CallCmds.Count; i++) + { + if (node.CallCmds[i] != null) + node.CallCmds[i] = (CallCmd)this.VisitCallCmd(node.CallCmds[i]); + } + return node; + } public virtual List VisitCmdSeq(List cmdSeq) { Contract.Requires(cmdSeq != null); Contract.Ensures(Contract.Result>() != null); diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 80e91e22..e7b55dc4 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -596,7 +596,7 @@ namespace Microsoft.Boogie try { var defines = new List() { "FILE_" + fileId }; - errorCount = BoogiePL.Parser.Parse(bplFileName, defines, out programSnippet); + errorCount = Parser.Parse(bplFileName, defines, out programSnippet); if (programSnippet == null || errorCount != 0) { Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName); diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index a6b01760..bd8e7c79 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -679,6 +679,12 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false); throw new cce.UnreachableException(); } + public override Cmd VisitParCallCmd(ParCallCmd node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + Contract.Assert(false); + throw new cce.UnreachableException(); + } public override List VisitCmdSeq(List cmdSeq) { //Contract.Requires(cmdSeq != null); Contract.Ensures(Contract.Result>() != null); diff --git a/Test/linear/Answer b/Test/linear/Answer index 9ba244e5..2934d690 100644 --- a/Test/linear/Answer +++ b/Test/linear/Answer @@ -12,11 +12,11 @@ typecheck.bpl(51,4): Error: Only variable can be passed to linear parameter b typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same typecheck.bpl(57,4): Error: Only a linear argument can be passed to linear parameter a -typecheck.bpl(61,4): Error: Linear variable a can occur only once as an input parameter -typecheck.bpl(66,6): Error: Output variable d must be available at a return -typecheck.bpl(75,4): Error: Global variable g must be available at a return +typecheck.bpl(61,4): Error: Linear variable a can occur only once as an input parameter of a parallel call +typecheck.bpl(67,0): Error: Output variable d must be available at a return +typecheck.bpl(76,0): Error: Global variable g must be available at a return typecheck.bpl(81,7): Error: unavailable source for a linear read -typecheck.bpl(81,4): Error: Output variable r must be available at a return +typecheck.bpl(82,0): Error: Output variable r must be available at a return 17 type checking errors detected in typecheck.bpl -------------------- list.bpl -------------------- diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index 973a1c88..187b3ff8 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -58,7 +58,7 @@ procedure {:yields} D() call c, x := E(a, x); - call a := F(a) | x := F(a); + par a := F(a) | x := F(a); } procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X) @@ -92,12 +92,12 @@ procedure {:yields} {:stable} J() procedure {:yields} P1({:linear ""} x:int) returns({:linear ""} x':int) { - call x' := I(x) | J(); + par x' := I(x) | J(); call x' := I(x'); } procedure {:yields} P2({:linear ""} x:int) returns({:linear ""} x':int) { call x' := I(x); - call x' := I(x') | J(); + par x' := I(x') | J(); } diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index 413db4ca..ede0a31e 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -87,7 +87,7 @@ ensures 0 <= bytesRead && bytesRead <= size; } READ_DEVICE: - call Skip() | tid := YieldToWriteCache(tid); + par Skip() | tid := YieldToWriteCache(tid); call tid := WriteCache(tid, start + size); call tid := acquire(tid); call tid, tmp := ReadNewsize(tid); @@ -95,7 +95,7 @@ READ_DEVICE: call tid := release(tid); COPY_TO_BUFFER: - call Skip() | YieldToReadCache(); + par Skip() | YieldToReadCache(); call ReadCache(start, bytesRead); } diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl index 0ab2beec..fa2cc611 100644 --- a/Test/og/DeviceCacheWithBuffer.bpl +++ b/Test/og/DeviceCacheWithBuffer.bpl @@ -93,7 +93,7 @@ ensures (forall i: int :: 0 <= i && i < bytesRead ==> buffer[i] == device[start+ } READ_DEVICE: - call Skip() | tid := YieldToWriteCache(tid); + par Skip() | tid := YieldToWriteCache(tid); call tid := WriteCache(tid, start + size); call tid := acquire(tid); call tid, tmp := ReadNewsize(tid); @@ -101,7 +101,7 @@ READ_DEVICE: call tid := release(tid); COPY_TO_BUFFER: - call Skip() | YieldToReadCache(); + par Skip() | YieldToReadCache(); call buffer := ReadCache(start, bytesRead); } diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl index ecddc9fc..fc33d6cc 100644 --- a/Test/og/parallel1.bpl +++ b/Test/og/parallel1.bpl @@ -25,6 +25,6 @@ procedure {:entrypoint} {:yields} Main() { while (true) { - call PB() | PC() | PD(); + par PB() | PC() | PD(); } } diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index b963fe72..6cc85131 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -8,8 +8,8 @@ procedure {:entrypoint} {:yields} main() var {:linear "tid"} j: int; call i := Allocate(); call j := Allocate(); - call i := t(i) | j := t(j); - call i := u(i) | j := u(j); + par i := t(i) | j := t(j); + par i := u(i) | j := u(j); } procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int) diff --git a/Test/og/parallel3.bpl b/Test/og/parallel3.bpl index f34efc6d..4c47adf7 100644 --- a/Test/og/parallel3.bpl +++ b/Test/og/parallel3.bpl @@ -1,6 +1,6 @@ procedure {:entrypoint} {:yields} main() { - call A() | B(); + par A() | B(); } procedure {:yields} {:stable} A() {} diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl index c07975ca..22e7173f 100644 --- a/Test/og/parallel4.bpl +++ b/Test/og/parallel4.bpl @@ -8,7 +8,7 @@ procedure {:entrypoint} {:yields} main() var {:linear "tid"} j: int; call i := Allocate(); call j := Allocate(); - call i := t(i) | j := t(j); + par i := t(i) | j := t(j); } procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int) diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl index eda8ef44..34bb82a9 100644 --- a/Test/og/parallel5.bpl +++ b/Test/og/parallel5.bpl @@ -8,8 +8,8 @@ procedure {:entrypoint} {:yields} main() var {:linear "tid"} j: int; call i := Allocate(); call j := Allocate(); - call i := t(i) | j := Yield(j); - call i := u(i) | j := u(j); + par i := t(i) | j := Yield(j); + par i := u(i) | j := u(j); } procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int) diff --git a/Test/og/parallel7.bpl b/Test/og/parallel7.bpl index 7a4018df..b66b9ee5 100644 --- a/Test/og/parallel7.bpl +++ b/Test/og/parallel7.bpl @@ -1,3 +1,3 @@ procedure {:yields} {:stable} A(); procedure {:yields} {:stable} B(); -procedure {:yields} C() { call A() | B(); } +procedure {:yields} C() { par A() | B(); } diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl new file mode 100644 index 00000000..d620abf3 --- /dev/null +++ b/Test/og/ticket.bpl @@ -0,0 +1,124 @@ +function RightOpen(n: int) : [int]bool; +function RightClosed(n: int) : [int]bool; + +type X; +function {:builtin "MapConst"} mapconstbool(bool): [X]bool; +const nil: X; +var t: int; +var s: int; +var cs: X; +var T: [int]bool; + +procedure Allocate({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X); +ensures xl != nil; + +function Inv1(tickets: [int]bool, ticket: int): (bool) +{ + tickets == RightOpen(ticket) +} + +function Inv2(tickets: [int]bool, ticket: int, lock: X): (bool) +{ + if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket) +} + +procedure {:yields} {:entrypoint} main({:linear "tid"} xls':[X]bool) +requires xls' == mapconstbool(true); +{ + var {:linear "tid"} tid: X; + var {:linear "tid"} xls: [X]bool; + + call xls := Init(xls'); + + while (*) + invariant {:phase 1} Inv1(T, t); + invariant {:phase 2} Inv2(T, s, cs); + { + call xls, tid := Allocate(xls); + async call Customer(tid); + } +} + +procedure {:yields} {:stable} Customer({:linear "tid"} tid': X) +requires {:phase 1} Inv1(T, t); +requires {:phase 2} tid' != nil && Inv2(T, s, cs); +{ + var {:linear "tid"} tid: X; + tid := tid'; + + while (*) + invariant {:phase 1} Inv1(T, t); + invariant {:phase 2} tid != nil && Inv2(T, s, cs); + { + par Skip() | Yield0() | Yield1() | Yield2(); + call tid := Enter(tid); + par Skip() | Yield0() | Yield1(); + call tid := Leave(tid); + par Skip() | Yield0() | Yield1() | Yield2(); + } +} + +procedure {:yields} Enter({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X) +requires {:phase 1} Inv1(T, t); +ensures {:phase 1} Inv1(T,t); +requires {:phase 2} tid' != nil && Inv2(T, s, cs); +ensures {:phase 2} tid != nil && Inv2(T, s, cs); +ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|; +{ + var m: int; + tid := tid'; + + par Skip() | Yield0() | Yield1(); + call tid, m := GetTicketAbstract(tid); + par Skip() | Yield0(); + call tid := WaitAndEnter(tid, m); + par Skip() | Yield0() | Yield1(); +} + +procedure {:yields} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int) +requires {:phase 1} Inv1(T, t); +ensures {:phase 1} Inv1(T, t); +ensures {:right 1} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|; +{ + tid := tid'; + + par Skip() | Yield0(); + call tid, m := GetTicket(tid); + par Skip() | Yield0(); +} + +procedure {:yields} {:stable} Yield2() +{ +} + +procedure {:yields} {:stable} Yield1() +requires {:phase 2} Inv2(T, s, cs); +ensures {:phase 2} Inv2(T, s, cs); +ensures {:both 2} |{ A: return true; }|; +{ +} + +procedure {:yields} {:stable} Yield0() +requires {:phase 1} Inv1(T, t); +ensures {:phase 1} Inv1(T,t); +ensures {:both 1} |{ A: return true; }|; +{ +} + +procedure {:yields} {:stable} Skip() +ensures {:both 0} |{ A: return true; }|; +{ +} + +procedure {:yields} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool); +ensures {:both 0} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|; + +procedure {:yields} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int); +ensures {:atomic 0} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|; + +procedure {:yields} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X); +ensures {:atomic 0} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|; + +procedure {:yields} Leave({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X); +ensures {:atomic 0} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|; + -- cgit v1.2.3