diff options
author | 2013-09-04 15:07:23 -0700 | |
---|---|---|
committer | 2013-09-04 15:07:23 -0700 | |
commit | b06cff3aa1491d0b2e5885a6e801c1d924af2e11 (patch) | |
tree | 701f467991d936fdf164e37b98e67fd58f162dc7 /Source/Core | |
parent | 0ce0ad111d6454475f47b56a6315b6134b869400 (diff) |
fixed the linear type checking related to globals
fixed the modset analysis so that it infers the stable predicate also
added more information to type error messages
Diffstat (limited to 'Source/Core')
-rw-r--r-- | Source/Core/DeadVarElim.cs | 7 | ||||
-rw-r--r-- | Source/Core/LinearSets.cs | 102 | ||||
-rw-r--r-- | Source/Core/OwickiGries.cs | 14 |
3 files changed, 71 insertions, 52 deletions
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 11927293..900546e6 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/LinearSets.cs b/Source/Core/LinearSets.cs index ca2aaedf..3a9de5fb 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -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 56b327cd..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++)
@@ -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);
|