diff options
| -rw-r--r-- | Source/Concurrency/LinearSets.cs | 119 | ||||
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 2 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 136 | ||||
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 66 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 150 | ||||
| -rw-r--r-- | Source/Core/BoogiePL.atg | 36 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.cs | 42 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 11 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 434 | ||||
| -rw-r--r-- | Source/Core/ResolutionContext.cs | 2 | ||||
| -rw-r--r-- | Source/Core/Scanner.cs | 104 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 11 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 6 | ||||
| -rw-r--r-- | Test/linear/Answer | 8 | ||||
| -rw-r--r-- | Test/linear/typecheck.bpl | 6 | ||||
| -rw-r--r-- | Test/og/DeviceCache.bpl | 4 | ||||
| -rw-r--r-- | Test/og/DeviceCacheWithBuffer.bpl | 4 | ||||
| -rw-r--r-- | Test/og/parallel1.bpl | 2 | ||||
| -rw-r--r-- | Test/og/parallel2.bpl | 4 | ||||
| -rw-r--r-- | Test/og/parallel3.bpl | 2 | ||||
| -rw-r--r-- | Test/og/parallel4.bpl | 2 | ||||
| -rw-r--r-- | Test/og/parallel5.bpl | 4 | ||||
| -rw-r--r-- | Test/og/parallel7.bpl | 2 | ||||
| -rw-r--r-- | Test/og/ticket.bpl | 124 |
25 files changed, 812 insertions, 471 deletions
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<string, Type>();
- this.parallelCallInvars = new HashSet<Variable>();
this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();
this.inoutParamToDomainName = new Dictionary<Variable, string>();
this.varToDomainName = new Dictionary<Variable, string>();
@@ -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<Variable>(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<Variable>(start);
- while (callCmd != null)
+ availableLinearVars[parCallCmd] = new HashSet<Variable>(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<Variable>(start);
}
@@ -311,7 +334,6 @@ namespace Microsoft.Boogie }
return base.VisitAssignCmd(node);
}
- HashSet<Variable> parallelCallInvars;
public override Cmd VisitCallCmd(CallCmd node)
{
HashSet<Variable> inVars = new HashSet<Variable>();
@@ -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<Variable> parallelCallInvars = new HashSet<Variable>();
+ 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<Cmd> newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
@@ -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> { Expr.False });
- expr.Resolve(new ResolutionContext(null));
- expr.Typecheck(new TypecheckingContext(null));
- callCmd.Ins.Add(expr);
- }
- callCmd = callCmd.InParallelWith;
- }
- }
else
{
Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
@@ -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> { 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<int> callerPhaseNums;
public List<AssertCmd> thisGate;
public CodeExpr thisAction;
public List<Variable> thisInParams;
@@ -45,6 +46,7 @@ namespace Microsoft.Boogie this.proc = proc;
this.moverType = moverType;
this.phaseNum = phaseNum;
+ this.callerPhaseNums = new HashSet<int>();
this.thisGate = new List<AssertCmd>();
this.thisAction = codeExpr;
this.thisInParams = new List<Variable>();
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<Expr> ins, out List<IdentifierExpr> outs)
+ public void DesugarParallelCallCmd(List<Cmd> newCmds, ParCallCmd parCallCmd)
{
List<string> parallelCalleeNames = new List<string>();
- CallCmd iter = callCmd;
- ins = new List<Expr>();
- outs = new List<IdentifierExpr>();
- while (iter != null)
+ List<Expr> ins = new List<Expr>();
+ List<IdentifierExpr> outs = new List<IdentifierExpr>();
+ 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<Variable> inParams = new List<Variable>();
- List<Variable> outParams = new List<Variable>();
- List<Requires> requiresSeq = new List<Requires>();
- List<Ensures> ensuresSeq = new List<Ensures>();
- int count = 0;
- while (callCmd != null)
{
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- 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<Variable> inParams = new List<Variable>();
+ List<Variable> outParams = new List<Variable>();
+ List<Requires> requiresSeq = new List<Requires>();
+ List<Ensures> ensuresSeq = new List<Ensures>();
+ int count = 0;
+ foreach (CallCmd callCmd in parCallCmd.CallCmds)
{
- requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition)));
+ Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
+ 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<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);
+ proc.AddAttribute("yields");
+ asyncAndParallelCallDesugarings[procName] = proc;
}
-
- Procedure proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), 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<List<Cmd>> yields, Dictionary<Variable, Expr> 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<Expr> ins;
- List<IdentifierExpr> 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<Variable> availableLinearVars = new HashSet<Variable>(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<Variable> availableLinearVars = new HashSet<Variable>(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<string, Expr> 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<Variable> globalVariables;
bool globalVarAccessAllowed;
bool visitingAssertion;
- int phaseNumEnclosingProc;
+ int enclosingProcPhaseNum;
public Dictionary<Procedure, ActionInfo> 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<CallCmd> CallCmds;
+ public ParCallCmd(IToken tok, List<CallCmd> callCmds)
+ : base(tok, null)
+ {
+ this.CallCmds = callCmds;
+ }
+ public ParCallCmd(IToken tok, List<CallCmd> 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<Variable> parallelCallLhss = new HashSet<Variable>();
+ 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<Variable> vars)
+ {
+ foreach (CallCmd callCmd in CallCmds)
+ {
+ callCmd.AddAssignedVariables(vars);
+ }
+ }
+ public override Absy StdDispatch(StandardVisitor visitor)
+ {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != 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<Expr> ins, List<IdentifierExpr> 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/*<Variable>*/ actualOuts = new Set/*<Variable>*/ (Outs.Count);
+ HashSet<Variable> actualOuts = new HashSet<Variable>();
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<out Bpl.Type/*!*/ ty> (
TypeAtom<out ty>
|
- Ident<out tok> (. List<Type>/*!*/ args = new List<Type> (); .)
+ Ident<out tok> (. List<Bpl.Type>/*!*/ args = new List<Bpl.Type> (); .)
[ TypeArgs<args> ] (. ty = new UnresolvedTypeIdentifier (tok, tok.val, args); .)
|
MapType<out ty>
)
.
-TypeArgs<.List<Type>/*!*/ ts.>
+TypeArgs<.List<Bpl.Type>/*!*/ ts.>
= (.Contract.Requires(ts != null); IToken/*!*/ tok; Bpl.Type/*!*/ ty; .)
(
TypeAtom<out ty> (. ts.Add(ty); .)
[ TypeArgs<ts> ]
|
- Ident<out tok> (. List<Type>/*!*/ args = new List<Type> ();
+ Ident<out tok> (. List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); .)
[ TypeArgs<ts> ]
|
@@ -342,7 +341,7 @@ TypeAtom<out Bpl.Type/*!*/ ty> MapType<out Bpl.Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken tok = null;
IToken/*!*/ nnTok;
- List<Type>/*!*/ arguments = new List<Type>();
+ List<Bpl.Type>/*!*/ arguments = new List<Bpl.Type>();
Bpl.Type/*!*/ result;
List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>();
.)
@@ -369,7 +368,7 @@ TypeParams<.out IToken/*!*/ tok, out List<TypeVariable>/*!*/ typeParams.> .)
.
-Types<.List<Type>/*!*/ ts.>
+Types<.List<Bpl.Type>/*!*/ ts.>
= (. Contract.Requires(ts != null); Bpl.Type/*!*/ ty; .)
Type<out ty> (. ts.Add(ty); .)
{ "," Type<out ty> (. ts.Add(ty); .)
@@ -864,6 +863,7 @@ LabelOrCmd<out Cmd c, out IToken label> c = new HavocCmd(x,ids);
.)
| CallCmd<out cn> ";" (. c = cn; .)
+ | ParCallCmd<out cn> (. c = cn; .)
| "yield" (. x = t; .)
";" (. c = new YieldCmd(x); .)
)
@@ -935,18 +935,32 @@ CallCmd<out Cmd c> ]
"call" (. x = t; .)
{ Attribute<ref kv> }
- CallParams<isAsync, isFree, kv, x, ref c> (. .)
- { "|" CallParams<isAsync, isFree, kv, x, ref c> (. .)
+ CallParams<isAsync, isFree, kv, x, out c> (. .)
+ .
+
+ParCallCmd<out Cmd d>
+= (. Contract.Ensures(Contract.ValueAtReturn(out d) != null);
+ IToken x;
+ QKeyValue kv = null;
+ Cmd c = null;
+ List<CallCmd> callCmds = new List<CallCmd>();
+ .)
+ "par" (. x = t; .)
+ { Attribute<ref kv> }
+ CallParams<false, false, kv, x, out c> (. callCmds.Add((CallCmd)c); .)
+ { "|" CallParams<false, false, kv, x, out c> (. callCmds.Add((CallCmd)c); .)
}
+ ";" (. d = new ParCallCmd(x, callCmds, kv); .)
.
-CallParams<bool isAsync, bool isFree, QKeyValue kv, IToken x, ref Cmd c>
+CallParams<bool isAsync, bool isFree, QKeyValue kv, IToken x, out Cmd c>
= (.
List<IdentifierExpr> ids = new List<IdentifierExpr>();
List<Expr> es = new List<Expr>();
Expr en;
IToken first;
IToken p;
+ c = null;
.)
Ident<out first>
( "("
@@ -954,7 +968,7 @@ CallParams<bool isAsync, bool isFree, QKeyValue kv, IToken x, ref Cmd c> { "," Expression<out en> (. 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<out p> (. ids.Add(new IdentifierExpr(p, p.val)); .)
@@ -966,7 +980,7 @@ CallParams<bool isAsync, bool isFree, QKeyValue kv, IToken x, ref Cmd c> { "," Expression<out en> (. 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<Cmd>() != 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<Cmd>() != null);
- CallCmd/*!*/ clone = (CallCmd)node.Clone();
+ CallCmd clone = (CallCmd)node.Clone();
Contract.Assert(clone != null);
clone.Ins = new List<Expr>(clone.Ins);
clone.Outs = new List<IdentifierExpr>(clone.Outs);
return base.VisitCallCmd(clone);
}
+ public override Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ ParCallCmd clone = (ParCallCmd)node.Clone();
+ Contract.Assert(clone != null);
+ clone.CallCmds = new List<CallCmd>(node.CallCmds);
+ return base.VisitParCallCmd(clone);
+ }
public override Choice VisitChoice(Choice node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<Choice>() != 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<Type>/*!*/ args = new List<Type> ();
+ List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
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<TypedIdent, QKeyValue> 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<Type>/*!*/ ts) {
+ void TypeArgs(List<Bpl.Type>/*!*/ 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<Type>/*!*/ args = new List<Type> ();
+ List<Bpl.Type>/*!*/ args = new List<Bpl.Type> ();
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<Type>/*!*/ arguments = new List<Type>();
+ List<Bpl.Type>/*!*/ arguments = new List<Bpl.Type>();
Bpl.Type/*!*/ result;
List<TypeVariable>/*!*/ typeParameters = new List<TypeVariable>();
@@ -737,7 +735,7 @@ private class BvBounds : Expr { }
- void Types(List<Type>/*!*/ ts) {
+ void Types(List<Bpl.Type>/*!*/ ts) {
Contract.Requires(ts != null); Bpl.Type/*!*/ ty;
Type(out ty);
ts.Add(ty);
@@ -884,7 +882,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
@@ -916,7 +914,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { c = new YieldCmd(x);
break;
}
- default: SynErr(104); break;
+ default: SynErr(105); break;
}
}
@@ -1067,7 +1070,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<CallCmd> callCmds = new List<CallCmd>();
+
+ 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<Expr/*!*/>/*!*/ indexes) {
@@ -1273,12 +1294,13 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<IdentifierExpr> ids = new List<IdentifierExpr>();
List<Expr> es = new List<Expr>();
Expr en;
IToken first;
IToken p;
+ c = null;
Ident(out first);
if (la.kind == 9) {
@@ -1293,7 +1315,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Expr>/*!*/ es) {
@@ -1338,7 +1360,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(121);
+ } else SynErr(122);
}
}
@@ -1696,12 +1718,12 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { List<Block/*!*/>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Expr>());
- } else SynErr(122);
+ } else SynErr(123);
Expect(10);
}
break;
}
- case 83: {
+ case 84: {
Get();
x = t;
Expect(9);
@@ -1770,19 +1792,19 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<Variable>/*!*/ ins, out List<Variable>/*!*/ 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<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ 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<Variable>(); Block/*!*/ b;
blocks = new List<Block/*!*/>();
- 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<Variable> parallelCallLhss = new HashSet<Variable>();
}
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<Cmd>() != 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<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
Contract.Requires(cmdSeq != null);
Contract.Ensures(Contract.Result<List<Cmd>>() != 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<string>() { "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<Cmd>() != null);
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
//Contract.Requires(cmdSeq != null);
Contract.Ensures(Contract.Result<List<Cmd>>() != 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; }|;
+
|