diff options
author | 2013-10-09 22:20:01 +0100 | |
---|---|---|
committer | 2013-10-09 22:20:01 +0100 | |
commit | 37a8b374462a3f41d43546da75ae540cc75a329d (patch) | |
tree | 8f3ae7b0f2d58855971e499f2891fe72045551ec /Source/Core | |
parent | e3e9aff76e22d05cdb3c558c8106d4a201aa0141 (diff) | |
parent | 225f211c0b94ad3d13dee857596f322b666fe259 (diff) |
Merge
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/Absy.cs | 7 | ||||
-rw-r--r-- | Source/Core/DeadVarElim.cs | 7 | ||||
-rw-r--r-- | Source/Core/Inline.cs | 1 | ||||
-rw-r--r-- | Source/Core/LinearSets.cs | 108 | ||||
-rw-r--r-- | Source/Core/OwickiGries.cs | 37 |
5 files changed, 99 insertions, 61 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 009fb071..33c4e91a 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2354,9 +2354,10 @@ namespace Microsoft.Boogie { public override void Typecheck(TypecheckingContext tc) {
//Contract.Requires(tc != null);
bool isAtomicSpecification =
- QKeyValue.FindIntAttribute(this.Attributes, "atomic", -1) != -1 ||
- QKeyValue.FindIntAttribute(this.Attributes, "rightmover", -1) != -1 ||
- QKeyValue.FindIntAttribute(this.Attributes, "leftmover", -1) != -1;
+ QKeyValue.FindBoolAttribute(this.Attributes, "atomic") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "right") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "left") ||
+ QKeyValue.FindBoolAttribute(this.Attributes, "both");
bool oldYields = tc.Yields;
tc.Yields = isAtomicSpecification;
this.Condition.Typecheck(tc);
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index f3056e4f..cb6ce689 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -42,6 +42,7 @@ namespace Microsoft.Boogie { static Procedure enclosingProc;
static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;
static HashSet<Procedure> yieldingProcs;
+ static HashSet<Procedure> asyncAndParallelCallTargetProcs;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));
@@ -69,6 +70,7 @@ namespace Microsoft.Boogie { modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();
yieldingProcs = new HashSet<Procedure>();
+ asyncAndParallelCallTargetProcs = new HashSet<Procedure>();
HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();
foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
@@ -118,6 +120,10 @@ namespace Microsoft.Boogie { {
x.AddAttribute("yields");
}
+ if (asyncAndParallelCallTargetProcs.Contains(x) && !QKeyValue.FindBoolAttribute(x.Attributes, "stable"))
+ {
+ x.AddAttribute("stable");
+ }
}
if (false /*CommandLineOptions.Clo.Trace*/) {
@@ -209,6 +215,7 @@ namespace Microsoft.Boogie { var curr = callCmd;
while (curr != null)
{
+ asyncAndParallelCallTargetProcs.Add(curr.Proc);
if (!yieldingProcs.Contains(curr.Proc))
{
yieldingProcs.Add(curr.Proc);
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 61b3a322..ad9ecef0 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -50,6 +50,7 @@ namespace Microsoft.Boogie { Inliner codeExprInliner = new Inliner(program, inlineCallback, CommandLineOptions.Clo.InlineDepth);
codeExprInliner.newLocalVars = new List<Variable>(node.LocVars);
codeExprInliner.newModifies = new List<IdentifierExpr>();
+ codeExprInliner.inlinedProcLblMap = this.inlinedProcLblMap;
List<Block> newCodeExprBlocks = codeExprInliner.DoInlineBlocks(node.Blocks, ref inlinedSomething);
return new CodeExpr(codeExprInliner.newLocalVars, newCodeExprBlocks);
}
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 5769cbdf..3a9de5fb 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -9,16 +9,16 @@ namespace Microsoft.Boogie {
public class LinearEraser : StandardVisitor
{
- private QKeyValue Remove(QKeyValue iter)
+ private QKeyValue RemoveLinearAttribute(QKeyValue iter)
{
if (iter == null) return null;
- iter.Next = Remove(iter.Next);
+ iter.Next = RemoveLinearAttribute(iter.Next);
return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next;
}
public override Variable VisitVariable(Variable node)
{
- node.Attributes = Remove(node.Attributes);
+ node.Attributes = RemoveLinearAttribute(node.Attributes);
return base.VisitVariable(node);
}
}
@@ -29,9 +29,10 @@ namespace Microsoft.Boogie public int errorCount;
public CheckingContext checkingContext;
public Dictionary<string, Type> domainNameToType;
- public Dictionary<Absy, HashSet<Variable>> availableLocalLinearVars;
+ public Dictionary<Absy, HashSet<Variable>> availableLinearVars;
public Dictionary<Variable, string> inoutParamToDomainName;
public Dictionary<Variable, string> varToDomainName;
+ public Dictionary<Variable, string> globalVarToDomainName;
public Dictionary<string, LinearDomain> linearDomains;
public LinearTypechecker(Program program)
@@ -41,7 +42,7 @@ namespace Microsoft.Boogie this.checkingContext = new CheckingContext(null);
this.domainNameToType = new Dictionary<string, Type>();
this.parallelCallInvars = new HashSet<Variable>();
- this.availableLocalLinearVars = new Dictionary<Absy, HashSet<Variable>>();
+ this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();
this.inoutParamToDomainName = new Dictionary<Variable, string>();
this.varToDomainName = new Dictionary<Variable, string>();
this.linearDomains = new Dictionary<string, LinearDomain>();
@@ -59,9 +60,22 @@ namespace Microsoft.Boogie checkingContext.Error(node, message);
errorCount++;
}
+ public override Program VisitProgram(Program node)
+ {
+ globalVarToDomainName = new Dictionary<Variable, string>();
+ foreach (GlobalVariable g in program.GlobalVariables())
+ {
+ string domainName = FindDomainName(g);
+ if (domainName != null)
+ {
+ globalVarToDomainName[g] = domainName;
+ }
+ }
+ return base.VisitProgram(node);
+ }
public override Implementation VisitImplementation(Implementation node)
{
- HashSet<Variable> start = new HashSet<Variable>();
+ HashSet<Variable> start = new HashSet<Variable>(globalVarToDomainName.Keys);
for (int i = 0; i < node.InParams.Count; i++)
{
string domainName = FindDomainName(node.Proc.InParams[i]);
@@ -87,7 +101,7 @@ namespace Microsoft.Boogie Stack<Block> dfsStack = new Stack<Block>();
HashSet<Block> dfsStackAsSet = new HashSet<Block>();
- availableLocalLinearVars[node.Blocks[0]] = start;
+ availableLinearVars[node.Blocks[0]] = start;
dfsStack.Push(node.Blocks[0]);
dfsStackAsSet.Add(node.Blocks[0]);
while (dfsStack.Count > 0)
@@ -97,27 +111,31 @@ namespace Microsoft.Boogie HashSet<Variable> end = PropagateAvailableLinearVarsAcrossBlock(b);
if (b.TransferCmd is ReturnCmd)
{
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(end))
+ {
+ Error(b, 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, "output variable must be available at a return");
+ Error(b, string.Format("Output variable {0} must be available at a return", v.Name));
}
+ continue;
}
- if (b.TransferCmd is ReturnCmd) continue;
GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
foreach (Block target in gotoCmd.labelTargets)
{
- if (!availableLocalLinearVars.ContainsKey(target))
+ if (!availableLinearVars.ContainsKey(target))
{
- availableLocalLinearVars[target] = new HashSet<Variable>(end);
+ availableLinearVars[target] = new HashSet<Variable>(end);
dfsStack.Push(target);
dfsStackAsSet.Add(target);
}
else
{
- var savedAvailableVars = new HashSet<Variable>(availableLocalLinearVars[target]);
- availableLocalLinearVars[target].IntersectWith(end);
- if (savedAvailableVars.IsProperSupersetOf(availableLocalLinearVars[target]) && !dfsStackAsSet.Contains(target))
+ var savedAvailableVars = new HashSet<Variable>(availableLinearVars[target]);
+ availableLinearVars[target].IntersectWith(end);
+ if (savedAvailableVars.IsProperSupersetOf(availableLinearVars[target]) && !dfsStackAsSet.Contains(target))
{
dfsStack.Push(target);
dfsStackAsSet.Add(target);
@@ -128,7 +146,7 @@ namespace Microsoft.Boogie return impl;
}
private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b) {
- HashSet<Variable> start = new HashSet<Variable>(availableLocalLinearVars[b]);
+ HashSet<Variable> start = new HashSet<Variable>(availableLinearVars[b]);
foreach (Cmd cmd in b.Cmds)
{
if (cmd is AssignCmd)
@@ -155,6 +173,10 @@ namespace Microsoft.Boogie }
else if (cmd is CallCmd)
{
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))
+ {
+ Error(b, string.Format("Global variable {0} must be available at a call", g.Name));
+ }
CallCmd callCmd = (CallCmd)cmd;
while (callCmd != null)
{
@@ -174,7 +196,7 @@ namespace Microsoft.Boogie callCmd = callCmd.InParallelWith;
}
callCmd = (CallCmd)cmd;
- availableLocalLinearVars[callCmd] = new HashSet<Variable>(start);
+ availableLinearVars[callCmd] = new HashSet<Variable>(start);
while (callCmd != null)
{
foreach (IdentifierExpr ie in callCmd.Outs)
@@ -196,13 +218,19 @@ namespace Microsoft.Boogie }
else if (cmd is YieldCmd)
{
- availableLocalLinearVars[cmd] = new HashSet<Variable>(start);
+ foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))
+ {
+ Error(b, string.Format("Global variable {0} must be available at a yield", g.Name));
+ }
+ availableLinearVars[cmd] = new HashSet<Variable>(start);
}
}
return start;
}
public string FindDomainName(Variable v)
{
+ if (globalVarToDomainName.ContainsKey(v))
+ return globalVarToDomainName[v];
if (inoutParamToDomainName.ContainsKey(v))
return inoutParamToDomainName[v];
return QKeyValue.FindStringAttribute(v.Attributes, "linear");
@@ -233,7 +261,7 @@ namespace Microsoft.Boogie }
if (domainNameToType.ContainsKey(domainName) && !domainNameToType[domainName].Equals(type))
{
- Error(node, "a linear domain must be consistently attached to variables of a particular type");
+ Error(node, string.Format("Linear domain {0} must be consistently attached to variables of one type", domainName));
}
else
{
@@ -248,44 +276,35 @@ namespace Microsoft.Boogie for (int i = 0; i < node.Lhss.Count; i++)
{
AssignLhs lhs = node.Lhss[i];
- string domainName = FindDomainName(lhs.DeepAssignedVariable);
+ Variable lhsVar = lhs.DeepAssignedVariable;
+ string domainName = FindDomainName(lhsVar);
if (domainName == null) continue;
SimpleAssignLhs salhs = lhs as SimpleAssignLhs;
if (salhs == null)
{
- Error(node, "Only simple assignment allowed on linear sets");
- continue;
- }
- if (salhs.DeepAssignedVariable is GlobalVariable)
- {
- Error(node, "Linear global variable cannot be written to");
+ Error(node, string.Format("Only simple assignment allowed on linear variable {0}", lhsVar.Name));
continue;
}
IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr;
if (rhs == null)
{
- Error(node, "Only variable can be assigned to a linear variable");
+ Error(node, string.Format("Only variable can be assigned to linear variable {0}", lhsVar.Name));
continue;
}
string rhsDomainName = FindDomainName(rhs.Decl);
if (rhsDomainName == null)
{
- Error(node, "Only linear variable can be assigned to another linear variable");
+ Error(node, string.Format("Only linear variable can be assigned to linear variable {0}", lhsVar.Name));
continue;
}
if (domainName != rhsDomainName)
{
- Error(node, "Variable of one domain being assigned to a variable of another domain");
+ Error(node, string.Format("Linear variable of domain {0} cannot be assigned to linear variable of domain {1}", rhsDomainName, domainName));
continue;
}
if (rhsVars.Contains(rhs.Decl))
{
- Error(node, "A linear variable can occur only once in the rhs");
- continue;
- }
- if (rhs.Decl is GlobalVariable)
- {
- Error(node, "Linear global variable cannot be read from");
+ Error(node, string.Format("Linear variable {0} can occur only once in the right-hand-side of an assignment", rhs.Decl.Name));
continue;
}
rhsVars.Add(rhs.Decl);
@@ -304,13 +323,13 @@ namespace Microsoft.Boogie IdentifierExpr actual = node.Ins[i] as IdentifierExpr;
if (actual == null)
{
- Error(node, "Only variable can be assigned to a linear variable");
+ Error(node, string.Format("Only variable can be passed to linear parameter {0}", formal.Name));
continue;
}
string actualDomainName = FindDomainName(actual.Decl);
if (actualDomainName == null)
{
- Error(node, "Only a linear argument can be passed to a linear parameter");
+ Error(node, string.Format("Only a linear argument can be passed to linear parameter {0}", formal.Name));
continue;
}
if (domainName != actualDomainName)
@@ -320,7 +339,7 @@ namespace Microsoft.Boogie }
if (parallelCallInvars.Contains(actual.Decl))
{
- Error(node, "A linear set can occur only once as an in parameter");
+ Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name));
continue;
}
if (actual.Decl is GlobalVariable)
@@ -373,13 +392,7 @@ namespace Microsoft.Boogie domainNameToScope[domainName] = new HashSet<Variable>();
domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);
}
- foreach (Variable v in program.GlobalVariables())
- {
- var domainName = FindDomainName(v);
- if (domainName == null) continue;
- domainNameToScope[domainName].Add(v);
- }
- foreach (Variable v in availableLocalLinearVars[absy])
+ foreach (Variable v in availableLinearVars[absy])
{
var domainName = FindDomainName(v);
domainNameToScope[domainName].Add(v);
@@ -453,7 +466,7 @@ namespace Microsoft.Boogie {
domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
}
- foreach (Variable v in availableLocalLinearVars[callCmd])
+ foreach (Variable v in availableLinearVars[callCmd])
{
var domainName = FindDomainName(v);
var domain = linearDomains[domainName];
@@ -510,10 +523,9 @@ namespace Microsoft.Boogie domainNameToOutputScope[domainName] = new HashSet<Variable>();
}
- foreach (Variable v in program.GlobalVariables())
+ foreach (Variable v in globalVarToDomainName.Keys)
{
- var domainName = FindDomainName(v);
- if (domainName == null) continue;
+ var domainName = globalVarToDomainName[v];
domainNameToInputScope[domainName].Add(v);
domainNameToOutputScope[domainName].Add(v);
}
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index ed4d8dbb..dd6276c2 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -67,7 +67,7 @@ namespace Microsoft.Boogie newCmds.Add(yieldCallCmd);
}
- private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLocalLinearVars, Dictionary<string, Variable> domainNameToInputVar)
+ private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)
{
Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
foreach (var domainName in linearTypechecker.linearDomains.Keys)
@@ -77,7 +77,7 @@ namespace Microsoft.Boogie expr.Typecheck(new TypecheckingContext(null));
domainNameToExpr[domainName] = expr;
}
- foreach (Variable v in availableLocalLinearVars)
+ foreach (Variable v in availableLinearVars)
{
var domainName = linearTypechecker.FindDomainName(v);
var domain = linearTypechecker.linearDomains[domainName];
@@ -118,7 +118,7 @@ namespace Microsoft.Boogie {
newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
}
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[yieldCmd], domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[yieldCmd], domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
for (int j = 0; j < cmds.Count; j++)
@@ -264,7 +264,7 @@ namespace Microsoft.Boogie PredicateCmd predCmd = (PredicateCmd)cmd;
var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
if (predCmd is AssertCmd)
- newCmds.Add(new AssertCmd(predCmd.tok, newExpr));
+ newCmds.Add(new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes));
else
newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
}
@@ -440,13 +440,13 @@ namespace Microsoft.Boogie if (callCmd.InParallelWith != null || callCmd.IsAsync ||
QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
{
- HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);
+ HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypechecker.availableLinearVars[callCmd]);
foreach (IdentifierExpr ie in callCmd.Outs)
{
if (linearTypechecker.FindDomainName(ie.Decl) == null) continue;
- availableLocalLinearVars.Add(ie.Decl);
+ availableLinearVars.Add(ie.Decl);
}
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLocalLinearVars, domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
}
}
@@ -473,7 +473,7 @@ namespace Microsoft.Boogie foreach (Block header in yieldingHeaders)
{
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[header], domainNameToInputVar);
+ Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[header], domainNameToInputVar);
foreach (Block pred in header.Predecessors)
{
AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
@@ -582,7 +582,7 @@ namespace Microsoft.Boogie }
else
{
- cmds.Add(new AssertCmd(r.tok, r.Condition));
+ cmds.Add(new AssertCmd(r.tok, r.Condition, r.Attributes));
}
}
yields.Add(cmds);
@@ -621,7 +621,7 @@ namespace Microsoft.Boogie }
else
{
- cmds.Add(new AssertCmd(e.tok, e.Condition));
+ cmds.Add(new AssertCmd(e.tok, e.Condition, e.Attributes));
}
}
yields.Add(cmds);
@@ -680,6 +680,13 @@ namespace Microsoft.Boogie program.TopLevelDeclarations.Add(yieldImpl);
}
+ private QKeyValue RemoveYieldsAttribute(QKeyValue iter)
+ {
+ if (iter == null) return null;
+ iter.Next = RemoveYieldsAttribute(iter.Next);
+ return (QKeyValue.FindBoolAttribute(iter, "yields")) ? iter.Next : iter;
+ }
+
public void Transform()
{
Program program = linearTypechecker.program;
@@ -708,12 +715,22 @@ namespace Microsoft.Boogie if (proc == null) continue;
if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
{
+ HashSet<Variable> modifiedVars = new HashSet<Variable>();
+ proc.Modifies.Iter(x => modifiedVars.Add(x.Decl));
foreach (GlobalVariable g in program.GlobalVariables())
{
+ if (modifiedVars.Contains(g)) continue;
proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));
}
+ proc.Attributes = RemoveYieldsAttribute(proc.Attributes);
}
}
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ Implementation impl = decl as Implementation;
+ if (impl == null) continue;
+ impl.Attributes = RemoveYieldsAttribute(impl.Attributes);
+ }
}
}
}
|