diff options
| author |  qadeer <unknown> | 2014-05-03 10:06:13 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2014-05-03 10:06:13 -0700 |
| commit | 36e016acf963b7c19d59640b11b4a40f2072943e (patch) | |
| tree | 31a45e868059d0ffe54fc3d212261245ff97886a /Source/Concurrency | |
| parent | 121071b9f87d23eaeba176897b9655cd540fb694 (diff) | |
checkpoint
Diffstat (limited to 'Source/Concurrency')
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 229 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 514 | ||||
| -rw-r--r-- | Source/Concurrency/Program.cs | 18 | ||||
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 319 | ||||
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 56 |
5 files changed, 470 insertions, 666 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index df2eeffd..dcc59878 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -9,53 +9,20 @@ namespace Microsoft.Boogie {
public class MoverCheck
{
- public static MoverType GetMoverType(Ensures e, out int phaseNum, out int availableUptoPhaseNum)
- {
- if (FindAtomicAction(e.Attributes, "atomic", out phaseNum, out availableUptoPhaseNum))
- return MoverType.Atomic;
- if (FindAtomicAction(e.Attributes, "right", out phaseNum, out availableUptoPhaseNum))
- return MoverType.Right;
- if (FindAtomicAction(e.Attributes, "left", out phaseNum, out availableUptoPhaseNum))
- return MoverType.Left;
- if (FindAtomicAction(e.Attributes, "both", out phaseNum, out availableUptoPhaseNum))
- return MoverType.Both;
- return MoverType.Top;
- }
-
- private static bool FindAtomicAction(QKeyValue kv, string name, out int phaseNum, out int availableUptoPhaseNum)
- {
- phaseNum = int.MaxValue;
- availableUptoPhaseNum = int.MaxValue;
- for (; kv != null; kv = kv.Next)
- {
- if (kv.Key != name) continue;
- if (!(kv.Params.Count == 1 || kv.Params.Count == 2)) continue;
- LiteralExpr l0 = kv.Params[0] as LiteralExpr;
- if (l0 == null || !l0.isBigNum) continue;
- phaseNum = l0.asBigNum.ToIntSafe;
- if (kv.Params.Count == 1) return true;
- LiteralExpr l1 = kv.Params[1] as LiteralExpr;
- if (l1 == null || !l1.isBigNum) continue;
- availableUptoPhaseNum = l1.asBigNum.ToIntSafe;
- return true;
- }
- return false;
- }
-
LinearTypeChecker linearTypeChecker;
MoverTypeChecker moverTypeChecker;
List<Declaration> decls;
- HashSet<Tuple<ActionInfo, ActionInfo>> commutativityCheckerCache;
- HashSet<Tuple<ActionInfo, ActionInfo>> gatePreservationCheckerCache;
- HashSet<Tuple<ActionInfo, ActionInfo>> failurePreservationCheckerCache;
+ HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache;
+ HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache;
+ HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache;
private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
{
this.linearTypeChecker = linearTypeChecker;
this.moverTypeChecker = moverTypeChecker;
this.decls = decls;
- this.commutativityCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
- this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
- this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();
+ this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
+ this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
+ this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
}
public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
@@ -63,18 +30,20 @@ namespace Microsoft.Boogie if (moverTypeChecker.procToActionInfo.Count == 0)
return;
- Dictionary<int, HashSet<ActionInfo>> pools = new Dictionary<int, HashSet<ActionInfo>>();
+ Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();
foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)
{
- foreach (int phaseNum in moverTypeChecker.allPhaseNums)
+ AtomicActionInfo atomicAction = action as AtomicActionInfo;
+ if (atomicAction == null) continue;
+ foreach (int phaseNum in moverTypeChecker.AllPhaseNums)
{
if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoPhaseNum)
{
if (!pools.ContainsKey(phaseNum))
{
- pools[phaseNum] = new HashSet<ActionInfo>();
+ pools[phaseNum] = new HashSet<AtomicActionInfo>();
}
- pools[phaseNum].Add(action);
+ pools[phaseNum].Add(atomicAction);
}
}
}
@@ -83,7 +52,7 @@ namespace Microsoft.Boogie MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);
foreach (int phaseNum1 in pools.Keys)
{
- foreach (ActionInfo first in pools[phaseNum1])
+ foreach (AtomicActionInfo first in pools[phaseNum1])
{
Debug.Assert(first.moverType != MoverType.Top);
if (first.moverType == MoverType.Atomic)
@@ -91,7 +60,7 @@ namespace Microsoft.Boogie foreach (int phaseNum2 in pools.Keys)
{
if (phaseNum2 < phaseNum1) continue;
- foreach (ActionInfo second in pools[phaseNum2])
+ foreach (AtomicActionInfo second in pools[phaseNum2])
{
if (second.phaseNum < phaseNum1)
{
@@ -111,11 +80,12 @@ namespace Microsoft.Boogie }
}
}
- foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)
+ foreach (ActionInfo actionInfo in moverTypeChecker.procToActionInfo.Values)
{
- if (action.IsLeftMover && action.hasAssumeCmd)
+ AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+ if (atomicActionInfo != null && atomicActionInfo.IsLeftMover && atomicActionInfo.hasAssumeCmd)
{
- moverChecking.CreateNonBlockingChecker(program, action);
+ moverChecking.CreateNonBlockingChecker(program, atomicActionInfo);
}
}
}
@@ -130,38 +100,37 @@ namespace Microsoft.Boogie return new OldExpr(Token.NoToken, ret);
}
else
+ {
return ret;
+ }
}
}
public class TransitionRelationComputation
{
private Program program;
- private ActionInfo first; // corresponds to that*
- private ActionInfo second; // corresponds to this*
+ private AtomicActionInfo first; // corresponds to that*
+ private AtomicActionInfo second; // corresponds to this*
private Stack<Cmd> cmdStack;
private List<PathInfo> paths;
private HashSet<Variable> frame;
+ private HashSet<Variable> postExistVars;
- public TransitionRelationComputation(Program program, ActionInfo second, HashSet<Variable> frame)
+ public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)
{
+ this.postExistVars = postExistVars;
this.frame = frame;
TransitionRelationComputationHelper(program, null, second);
}
- public TransitionRelationComputation(Program program, ActionInfo second)
+ public TransitionRelationComputation(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)
{
- this.frame = new HashSet<Variable>(program.GlobalVariables());
- TransitionRelationComputationHelper(program, null, second);
- }
-
- public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)
- {
- this.frame = new HashSet<Variable>(program.GlobalVariables());
+ this.postExistVars = postExistVars;
+ this.frame = frame;
TransitionRelationComputationHelper(program, first, second);
}
- private void TransitionRelationComputationHelper(Program program, ActionInfo first, ActionInfo second)
+ private void TransitionRelationComputationHelper(Program program, AtomicActionInfo first, AtomicActionInfo second)
{
this.program = program;
this.first = first;
@@ -292,6 +261,7 @@ namespace Microsoft.Boogie Dictionary<Variable, Expr> varToExpr = path.varToExpr;
foreach (Variable v in varToExpr.Keys)
{
+ if (postExistVars.Contains(v)) continue;
IdentifierExpr ie = varToExpr[v] as IdentifierExpr;
if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl))
{
@@ -357,43 +327,6 @@ namespace Microsoft.Boogie return false;
}
- public Expr LeftMoverCompute(Expr failureExpr)
- {
- Expr returnExpr = Expr.False;
- foreach (PathInfo path in paths)
- {
- Expr expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(path.varToExpr), failureExpr);
- Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
- foreach (Expr x in path.pathExprs)
- {
- Variable boundVar;
- Expr boundVarExpr;
- if (InferSubstitution(x, out boundVar, out boundVarExpr) && path.existsVars.Contains(boundVar))
- {
- subst[boundVar] = boundVarExpr;
- path.existsVars.Remove(boundVar);
- }
- else
- {
- expr = Expr.And(expr, x);
- expr.Type = Type.Bool;
- }
- }
- expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), expr);
- expr = new OldExpr(Token.NoToken, expr);
- if (path.existsVars.Count > 0)
- {
- expr = new ExistsExpr(Token.NoToken, new List<Variable>(path.existsVars), expr);
- }
- returnExpr = Expr.Or(returnExpr, expr);
- }
- ResolutionContext rc = new ResolutionContext(null);
- rc.StateMode = ResolutionContext.State.Two;
- returnExpr.Resolve(rc);
- returnExpr.Typecheck(new TypecheckingContext(null));
- return returnExpr;
- }
-
public Expr TransitionRelationCompute()
{
Expr transitionRelation = Expr.False;
@@ -483,7 +416,7 @@ namespace Microsoft.Boogie return otherBlocks;
}
- private List<Requires> DisjointnessRequires(Program program, ActionInfo first, ActionInfo second)
+ private List<Requires> DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame)
{
List<Requires> requires = new List<Requires>();
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
@@ -491,16 +424,13 @@ namespace Microsoft.Boogie {
domainNameToScope[domainName] = new HashSet<Variable>();
}
- /*
- // Commenting this out to avoid the danger of making an assumption about a hidden variable
- foreach (Variable v in program.GlobalVariables())
+ foreach (Variable v in frame)
{
var domainName = linearTypeChecker.FindDomainName(v);
if (domainName == null) continue;
if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
domainNameToScope[domainName].Add(v);
}
- */
if (first != null)
{
foreach (Variable v in first.thatInParams)
@@ -525,13 +455,13 @@ namespace Microsoft.Boogie return requires;
}
- private void CreateCommutativityChecker(Program program, ActionInfo first, ActionInfo second)
+ private void CreateCommutativityChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)
{
if (first == second && first.thatInParams.Count == 0 && first.thatOutParams.Count == 0)
return;
if (first.CommutesWith(second))
return;
- Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
if (commutativityCheckerCache.Contains(actionPair))
return;
commutativityCheckerCache.Add(actionPair);
@@ -561,13 +491,18 @@ namespace Microsoft.Boogie List<Block> blocks = new List<Block>();
blocks.AddRange(firstBlocks);
blocks.AddRange(secondBlocks);
- List<Requires> requires = DisjointnessRequires(program, first, second);
+ HashSet<Variable> frame = new HashSet<Variable>();
+ frame.UnionWith(first.gateUsedGlobalVars);
+ frame.UnionWith(first.actionUsedGlobalVars);
+ frame.UnionWith(second.gateUsedGlobalVars);
+ frame.UnionWith(second.actionUsedGlobalVars);
+ List<Requires> requires = DisjointnessRequires(program, first, second, frame);
foreach (AssertCmd assertCmd in first.thatGate)
requires.Add(new Requires(false, assertCmd.Expr));
foreach (AssertCmd assertCmd in second.thisGate)
requires.Add(new Requires(false, assertCmd.Expr));
List<Ensures> ensures = new List<Ensures>();
- Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).TransitionRelationCompute();
+ Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet<Variable>())).TransitionRelationCompute();
Ensures ensureCheck = new Ensures(false, transitionRelation);
ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);
ensures.Add(ensureCheck);
@@ -581,11 +516,11 @@ namespace Microsoft.Boogie this.decls.Add(proc);
}
- private void CreateGatePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ private void CreateGatePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)
{
if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
return;
- Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
if (gatePreservationCheckerCache.Contains(actionPair))
return;
gatePreservationCheckerCache.Add(actionPair);
@@ -599,7 +534,11 @@ namespace Microsoft.Boogie List<Variable> locals = new List<Variable>();
locals.AddRange(second.thisAction.LocVars);
List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
- List<Requires> requires = DisjointnessRequires(program, first, second);
+ HashSet<Variable> frame = new HashSet<Variable>();
+ frame.UnionWith(first.gateUsedGlobalVars);
+ frame.UnionWith(second.gateUsedGlobalVars);
+ frame.UnionWith(second.actionUsedGlobalVars);
+ List<Requires> requires = DisjointnessRequires(program, first, second, frame);
List<Ensures> ensures = new List<Ensures>();
foreach (AssertCmd assertCmd in first.thatGate)
{
@@ -620,11 +559,11 @@ namespace Microsoft.Boogie this.decls.Add(proc);
}
- private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
+ private void CreateFailurePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)
{
if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
return;
- Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
+ Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
if (failurePreservationCheckerCache.Contains(actionPair))
return;
failurePreservationCheckerCache.Add(actionPair);
@@ -638,7 +577,11 @@ namespace Microsoft.Boogie List<Variable> locals = new List<Variable>();
locals.AddRange(second.thisAction.LocVars);
List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
- List<Requires> requires = DisjointnessRequires(program, first, second);
+ HashSet<Variable> frame = new HashSet<Variable>();
+ frame.UnionWith(first.gateUsedGlobalVars);
+ frame.UnionWith(second.gateUsedGlobalVars);
+ frame.UnionWith(second.actionUsedGlobalVars);
+ List<Requires> requires = DisjointnessRequires(program, first, second, frame);
Expr gateExpr = Expr.True;
foreach (AssertCmd assertCmd in first.thatGate)
{
@@ -664,67 +607,23 @@ namespace Microsoft.Boogie this.decls.Add(proc);
}
- /*
- private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)
- {
- if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
- return;
-
- Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);
- if (failurePreservationCheckerCache.Contains(actionPair))
- return;
- failurePreservationCheckerCache.Add(actionPair);
-
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(first.thatInParams);
- inputs.AddRange(second.thisInParams);
-
- Expr requiresExpr = Expr.True;
- foreach (AssertCmd assertCmd in first.thatGate)
- {
- requiresExpr = Expr.And(assertCmd.Expr, requiresExpr);
- requiresExpr.Type = Type.Bool;
- }
- Expr failureExpr = Expr.Not(requiresExpr);
- failureExpr.Type = Type.Bool;
- List<Requires> requires = DisjointnessRequires(program, first, second);
- requires.Add(new Requires(false, failureExpr));
- foreach (AssertCmd assertCmd in second.thisGate)
- {
- requires.Add(new Requires(false, assertCmd.Expr));
- }
-
- Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(failureExpr);
- List<Ensures> ensures = new List<Ensures>();
- Ensures ensureCheck = new Ensures(false, ensuresExpr);
- ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);
- ensures.Add(ensureCheck);
-
- List<Block> blocks = new List<Block>();
- blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
- string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
- List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
- program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
- impl.Proc = proc;
- this.decls.Add(impl);
- this.decls.Add(proc);
- }
- */
-
- private void CreateNonBlockingChecker(Program program, ActionInfo second)
+ private void CreateNonBlockingChecker(Program program, AtomicActionInfo second)
{
List<Variable> inputs = new List<Variable>();
inputs.AddRange(second.thisInParams);
- List<Requires> requires = DisjointnessRequires(program, null, second);
+ HashSet<Variable> frame = new HashSet<Variable>();
+ frame.UnionWith(second.gateUsedGlobalVars);
+ frame.UnionWith(second.actionUsedGlobalVars);
+ List<Requires> requires = DisjointnessRequires(program, null, second, frame);
foreach (AssertCmd assertCmd in second.thisGate)
{
requires.Add(new Requires(false, assertCmd.Expr));
}
-
- Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(Expr.True);
+ HashSet<Variable> postExistVars = new HashSet<Variable>();
+ postExistVars.UnionWith(frame);
+ postExistVars.UnionWith(second.thisOutParams);
+ Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute();
List<Ensures> ensures = new List<Ensures>();
Ensures ensureCheck = new Ensures(false, ensuresExpr);
ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);
diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 9ec07854..5170383f 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -18,6 +18,8 @@ namespace Microsoft.Boogie public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */
public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */
public Dictionary<Block, Block> blockMap; /* Original -> Duplicate */
+ public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */
+ public HashSet<Procedure> yieldingProcs;
public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum)
{
this.moverTypeChecker = moverTypeChecker;
@@ -26,30 +28,27 @@ namespace Microsoft.Boogie this.procMap = new Dictionary<Procedure, Procedure>();
this.absyMap = new Dictionary<Absy, Absy>();
this.blockMap = new Dictionary<Block, Block>();
+ this.implMap = new Dictionary<Implementation, Implementation>();
+ this.yieldingProcs = new HashSet<Procedure>();
}
private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)
{
- int enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(enclosingProc);
- if (enclosingProcPhaseNum == int.MaxValue)
- {
- enclosingProcPhaseNum = moverTypeChecker.allPhaseNums.Max();
- }
+ int enclosingProcPhaseNum = moverTypeChecker.procToActionInfo[enclosingProc].phaseNum;
Procedure originalProc = originalCallCmd.Proc;
- if (phaseNum == enclosingProcPhaseNum && moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
+ if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
{
- ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];
- List<AssertCmd> gate = actionInfo.thisGate;
- if (actionInfo.phaseNum < phaseNum && gate.Count > 0)
+ AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
+ if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && phaseNum == enclosingProcPhaseNum)
{
- newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) } )));
+ newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) })));
Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
for (int i = 0; i < originalProc.InParams.Count; i++)
{
map[originalProc.InParams[i]] = callCmd.Ins[i];
}
Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (AssertCmd assertCmd in gate)
+ foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)
{
newCmds.Add(Substituter.Apply(subst, assertCmd));
}
@@ -63,7 +62,7 @@ namespace Microsoft.Boogie int maxCalleePhaseNum = 0;
foreach (CallCmd iter in originalParCallCmd.CallCmds)
{
- int calleePhaseNum = moverTypeChecker.FindPhaseNumber(iter.Proc);
+ int calleePhaseNum = moverTypeChecker.procToActionInfo[iter.Proc].phaseNum;
if (calleePhaseNum > maxCalleePhaseNum)
maxCalleePhaseNum = calleePhaseNum;
}
@@ -142,27 +141,32 @@ namespace Microsoft.Boogie public override Procedure VisitProcedure(Procedure node)
{
- enclosingProc = node;
- if (!QKeyValue.FindBoolAttribute(node.Attributes, "yields"))
+ if (!moverTypeChecker.procToActionInfo.ContainsKey(node))
return node;
if (!procMap.ContainsKey(node))
{
+ Procedure savedEnclosingProc = enclosingProc;
+ enclosingProc = node;
Procedure proc = (Procedure)node.Clone();
proc.Name = string.Format("{0}_{1}", node.Name, phaseNum);
proc.InParams = this.VisitVariableSeq(node.InParams);
proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
proc.OutParams = this.VisitVariableSeq(node.OutParams);
- if (moverTypeChecker.procToActionInfo.ContainsKey(node) && moverTypeChecker.procToActionInfo[node].phaseNum < phaseNum)
+ if (moverTypeChecker.procToActionInfo[node].phaseNum < phaseNum)
{
proc.Requires = new List<Requires>();
proc.Ensures = new List<Ensures>();
}
else
{
+ yieldingProcs.Add(proc);
proc.Requires = this.VisitRequiresSeq(node.Requires);
proc.Ensures = this.VisitEnsuresSeq(node.Ensures);
}
procMap[node] = proc;
+ enclosingProc = savedEnclosingProc;
+ proc.Modifies = new List<IdentifierExpr>();
+ moverTypeChecker.program.GlobalVariables().Iter(x => proc.Modifies.Add(Expr.Ident(x)));
}
return procMap[node];
}
@@ -173,6 +177,7 @@ namespace Microsoft.Boogie enclosingProc = node.Proc;
dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool));
Implementation impl = base.VisitImplementation(node);
+ implMap[impl] = node;
impl.LocVars.Add(dummyLocalVar);
impl.Name = impl.Proc.Name;
foreach (Block block in impl.Blocks)
@@ -198,7 +203,7 @@ namespace Microsoft.Boogie Requires requires = base.VisitRequires(node);
if (node.Free)
return requires;
- if (!OwickiGries.FindPhaseNums(requires.Attributes).Contains(phaseNum))
+ if (!moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))
requires.Condition = Expr.True;
return requires;
}
@@ -208,8 +213,9 @@ namespace Microsoft.Boogie Ensures ensures = base.VisitEnsures(node);
if (node.Free)
return ensures;
- bool isAtomicSpecification = moverTypeChecker.procToActionInfo.ContainsKey(enclosingProc) && moverTypeChecker.procToActionInfo[enclosingProc].ensures == node;
- if (isAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum))
+ AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
+ bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;
+ if (isAtomicSpecification || !moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))
{
ensures.Condition = Expr.True;
ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);
@@ -220,7 +226,7 @@ namespace Microsoft.Boogie public override Cmd VisitAssertCmd(AssertCmd node)
{
AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
- if (!OwickiGries.FindPhaseNums(assertCmd.Attributes).Contains(phaseNum))
+ if (!moverTypeChecker.absyToPhaseNums[node].Contains(phaseNum))
assertCmd.Expr = Expr.True;
return assertCmd;
}
@@ -231,27 +237,23 @@ namespace Microsoft.Boogie LinearTypeChecker linearTypeChecker;
MoverTypeChecker moverTypeChecker;
Dictionary<Absy, Absy> absyMap;
- Dictionary<Procedure, Procedure> reverseProcMap;
+ Dictionary<Implementation, Implementation> implMap;
+ HashSet<Procedure> yieldingProcs;
int phaseNum;
- List<Declaration> decls;
List<IdentifierExpr> globalMods;
Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
List<Procedure> yieldCheckerProcs;
List<Implementation> yieldCheckerImpls;
Procedure yieldProc;
- public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator, List<Declaration> decls)
+ public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator)
{
this.linearTypeChecker = linearTypeChecker;
this.moverTypeChecker = moverTypeChecker;
this.absyMap = duplicator.absyMap;
this.phaseNum = duplicator.phaseNum;
- this.reverseProcMap = new Dictionary<Procedure, Procedure>();
- foreach (Procedure proc in duplicator.procMap.Keys)
- {
- this.reverseProcMap[duplicator.procMap[proc]] = proc;
- }
- this.decls = decls;
+ this.implMap = duplicator.implMap;
+ this.yieldingProcs = duplicator.yieldingProcs;
Program program = linearTypeChecker.program;
globalMods = new List<IdentifierExpr>();
foreach (Variable g in program.GlobalVariables())
@@ -306,10 +308,11 @@ namespace Microsoft.Boogie if (pc != null)
{
+ Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap);
Expr bb = OldEqualityExpr(ogOldGlobalMap);
- // assert (o_old == o && g_old == g) || beta(i, g_old, o, g);
- AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, Expr.Or(bb, beta));
+ // assert pc || g_old == g || beta(i, g_old, o, g);
+ AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta)));
skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";
newCmds.Add(skipOrBetaAssertCmd);
@@ -318,8 +321,7 @@ namespace Microsoft.Boogie skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;
newCmds.Add(skipAssertCmd);
- // pc, ok := ite(o_old == o && g_old == g, pc, true), ok || beta(i, g_old, o, g);
- List<Expr> iteArgs = new List<Expr>(new Expr[] { bb, Expr.Ident(pc), Expr.True });
+ // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g);
List<AssignLhs> pcUpdateLHS = new List<AssignLhs>(
new AssignLhs[] {
new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)),
@@ -327,7 +329,7 @@ namespace Microsoft.Boogie });
List<Expr> pcUpdateRHS = new List<Expr>(
new Expr[] {
- new NAryExpr(Token.NoToken, new IfThenElse(Token.NoToken), iteArgs),
+ Expr.Imp(aa, Expr.Ident(pc)),
Expr.Or(Expr.Ident(ok), beta)
});
newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS));
@@ -383,18 +385,34 @@ namespace Microsoft.Boogie Variable ok;
Expr alpha;
Expr beta;
+ HashSet<Variable> frame;
private Expr OldEqualityExpr(Dictionary<Variable, Variable> ogOldGlobalMap)
{
Expr bb = Expr.True;
foreach (Variable o in ogOldGlobalMap.Keys)
{
+ if (o is GlobalVariable && !frame.Contains(o)) continue;
bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
bb.Type = Type.Bool;
}
return bb;
}
+ private Expr OldEqualityExprForGlobals(Dictionary<Variable, Variable> ogOldGlobalMap)
+ {
+ Expr bb = Expr.True;
+ foreach (Variable o in ogOldGlobalMap.Keys)
+ {
+ if (o is GlobalVariable && frame.Contains(o))
+ {
+ bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
+ bb.Type = Type.Bool;
+ }
+ }
+ return bb;
+ }
+
private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)
{
AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
@@ -470,8 +488,7 @@ namespace Microsoft.Boogie }
count++;
}
- proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);
- proc.AddAttribute("yields");
+ proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, globalMods, ensuresSeq);
asyncAndParallelCallDesugarings[procName] = proc;
}
CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);
@@ -479,109 +496,6 @@ namespace Microsoft.Boogie newCmds.Add(dummyCallCmd);
}
- private void CreateYieldCheckerImplForOldStableEnsures(Procedure proc)
- {
- Program program = linearTypeChecker.program;
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- Dictionary<Variable, Expr> oldGlobalMap = new Dictionary<Variable, Expr>();
- Dictionary<Variable, Expr> identityGlobalMap = new Dictionary<Variable, Expr>();
- List<Variable> locals = new List<Variable>();
- List<Variable> inputs = new List<Variable>();
- for (int i = 0; i < proc.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
- {
- Variable inParam = proc.InParams[i];
- Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
- locals.Add(copy);
- map[proc.InParams[i]] = Expr.Ident(copy);
- }
- {
- int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count;
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- Variable inParam = proc.InParams[i];
- Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
- inputs.Add(copy);
- map[proc.InParams[i]] = Expr.Ident(copy);
- i++;
- }
- }
- Dictionary<Variable, Expr> requiresMap = new Dictionary<Variable, Expr>(map);
- for (int i = 0; i < proc.OutParams.Count; i++)
- {
- Variable outParam = proc.OutParams[i];
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));
- locals.Add(copy);
- map[proc.OutParams[i]] = Expr.Ident(copy);
- }
- foreach (IdentifierExpr ie in globalMods)
- {
- Variable g = ie.Decl;
- identityGlobalMap[g] = Expr.Ident(g);
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_post_{0}", g.Name), g.TypedIdent.Type));
- locals.Add(copy);
- map[g] = Expr.Ident(copy);
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type), true);
- inputs.Add(f);
- oldGlobalMap[g] = Expr.Ident(f);
- requiresMap[g] = Expr.Ident(f);
- }
-
- Substitution requiresSubst = Substituter.SubstitutionFromHashtable(requiresMap);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- Substitution identityGlobalSubst = Substituter.SubstitutionFromHashtable(identityGlobalMap);
- Substitution oldGlobalSubst = Substituter.SubstitutionFromHashtable(oldGlobalMap);
- List<Block> yieldCheckerBlocks = new List<Block>();
- List<String> labels = new List<String>();
- List<Block> labelTargets = new List<Block>();
- Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
- List<Cmd> newCmds = new List<Cmd>();
- foreach (Requires requires in proc.Requires)
- {
- AssumeCmd assumeCmd = new AssumeCmd(Token.NoToken, Substituter.Apply(requiresSubst, requires.Condition));
- newCmds.Add(assumeCmd);
- }
- foreach (Ensures ensures in proc.Ensures)
- {
- AssumeCmd assumeCmd = new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(subst, identityGlobalSubst, ensures.Condition)); ;
- newCmds.Add(assumeCmd);
- }
- foreach (Ensures ensures in proc.Ensures)
- {
- var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldGlobalSubst, ensures.Condition);
- if (ensures.Free)
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
- }
- else
- {
- AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr, ensures.Attributes);
- assertCmd.ErrorData = "Backwards non-interference check failed";
- newCmds.Add(assertCmd);
- }
- }
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
- yieldCheckerBlock = new Block(Token.NoToken, "L", newCmds, new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));
-
- // Create the yield checker procedure
- var yieldCheckerName = string.Format("Proc_OldStableEnsuresChecker_{0}", proc.Name);
- var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, proc.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
- yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- yieldCheckerProcs.Add(yieldCheckerProc);
-
- // Create the yield checker implementation
- var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, proc.TypeParameters, inputs, new List<Variable>(), locals, yieldCheckerBlocks);
- yieldCheckerImpl.Proc = yieldCheckerProc;
- yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- yieldCheckerImpls.Add(yieldCheckerImpl);
- }
-
private void CreateYieldCheckerImpl(DeclWithFormals decl, List<List<Cmd>> yields, Dictionary<Variable, Expr> map)
{
if (yields.Count == 0) return;
@@ -700,7 +614,7 @@ namespace Microsoft.Boogie return true;
CallCmd callCmd = cmd as CallCmd;
if (callCmd == null) continue;
- if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
+ if (yieldingProcs.Contains(callCmd.Proc))
return true;
}
}
@@ -708,9 +622,17 @@ namespace Microsoft.Boogie return false;
}
+ private bool IsYieldingCallCmd(CallCmd callCmd)
+ {
+ return true;
+ }
+
private void TransformImpl(Implementation impl)
{
- if (!QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) return;
+ pc = null;
+ alpha = null;
+ beta = null;
+ frame = null;
// Find the yielding loop headers
impl.PruneUnreachableBlocks();
@@ -755,55 +677,70 @@ namespace Microsoft.Boogie impl.LocVars.Add(l);
}
- Procedure originalProc = reverseProcMap[impl.Proc];
- if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
+ Procedure originalProc = implMap[impl].Proc;
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];
+ if (actionInfo.phaseNum == this.phaseNum)
{
- ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];
- if (actionInfo.phaseNum == this.phaseNum)
+ pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
+ impl.LocVars.Add(pc);
+ ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));
+ impl.LocVars.Add(ok);
+ Dictionary<Variable, Expr> alwaysMap = new Dictionary<Variable, Expr>();
+ for (int i = 0; i < originalProc.InParams.Count; i++)
{
- pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
- impl.LocVars.Add(pc);
- ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));
- impl.LocVars.Add(ok);
- Dictionary<Variable, Expr> alwaysMap = new Dictionary<Variable, Expr>();
- for (int i = 0; i < originalProc.InParams.Count; i++)
- {
- alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]);
- }
- for (int i = 0; i < originalProc.OutParams.Count; i++)
+ alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]);
+ }
+ for (int i = 0; i < originalProc.OutParams.Count; i++)
+ {
+ alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]);
+ }
+ Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);
+ Dictionary<Variable, Expr> foroldMap = new Dictionary<Variable, Expr>();
+ foreach (IdentifierExpr ie in globalMods)
+ {
+ foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
+ }
+ Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
+ frame = new HashSet<Variable>(program.GlobalVariables());
+ HashSet<Variable> introducedVars = new HashSet<Variable>();
+ foreach (Variable v in program.GlobalVariables())
+ {
+ if (moverTypeChecker.hidePhaseNums[v] <= actionInfo.phaseNum || moverTypeChecker.introducePhaseNums[v] > actionInfo.phaseNum)
{
- alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]);
+ frame.Remove(v);
}
- Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);
- Dictionary<Variable, Expr> foroldMap = new Dictionary<Variable, Expr>();
- foreach (IdentifierExpr ie in globalMods)
+ if (moverTypeChecker.introducePhaseNums[v] == actionInfo.phaseNum)
{
- foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
+ introducedVars.Add(v);
}
- Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
- HashSet<Variable> frame = new HashSet<Variable>(program.GlobalVariables());
- foreach (Variable v in moverTypeChecker.qedGlobalVariables.Keys)
+ }
+ AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+ if (atomicActionInfo == null)
+ {
+ beta = Expr.True;
+ foreach (var v in frame)
{
- if (moverTypeChecker.qedGlobalVariables[v] <= actionInfo.phaseNum)
- {
- frame.Remove(v);
- }
+ beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v]));
}
- Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo, frame)).TransitionRelationCompute();
+ alpha = Expr.True;
+ }
+ else
+ {
+ Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute();
beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
Expr alphaExpr = Expr.True;
- foreach (AssertCmd assertCmd in actionInfo.thisGate)
+ foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)
{
alphaExpr = Expr.And(alphaExpr, assertCmd.Expr);
alphaExpr.Type = Type.Bool;
}
alpha = Substituter.Apply(always, alphaExpr);
- foreach (Variable f in impl.OutParams)
- {
- LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type));
- impl.LocVars.Add(copy);
- ogOldGlobalMap[f] = copy;
- }
+ }
+ foreach (Variable f in impl.OutParams)
+ {
+ LocalVariable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_old_{0}", f.Name), f.TypedIdent.Type));
+ impl.LocVars.Add(copy);
+ ogOldGlobalMap[f] = copy;
}
}
@@ -858,8 +795,8 @@ namespace Microsoft.Boogie if (cmd is CallCmd)
{
- CallCmd callCmd = cmd as CallCmd;
- if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
+ CallCmd callCmd = cmd as CallCmd;
+ if (yieldingProcs.Contains(callCmd.Proc))
{
AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
}
@@ -878,7 +815,7 @@ namespace Microsoft.Boogie {
newCmds.Add(callCmd);
}
- if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))
+ if (yieldingProcs.Contains(callCmd.Proc))
{
HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));
linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);
@@ -915,7 +852,7 @@ namespace Microsoft.Boogie cmds = new List<Cmd>();
}
}
- if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))
+ if (b.TransferCmd is ReturnCmd)
{
AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
if (pc != null)
@@ -950,7 +887,7 @@ namespace Microsoft.Boogie if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))
{
pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>(
- new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }),
+ new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }),
new List<Expr>(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) })));
}
AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
@@ -965,7 +902,7 @@ namespace Microsoft.Boogie assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));
assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
newCmds.Add(assertCmd);
- }
+ }
foreach (string domainName in linearTypeChecker.linearDomains.Keys)
{
newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
@@ -1035,114 +972,7 @@ namespace Microsoft.Boogie CreateYieldCheckerImpl(impl, yields, map);
}
- public void TransformProc(Procedure proc)
- {
- if (!QKeyValue.FindBoolAttribute(proc.Attributes, "stable")) return;
-
- Program program = linearTypeChecker.program;
- Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
- {
- int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count;
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- Variable inParam = proc.InParams[i];
- domainNameToInputVar[domainName] = inParam;
- i++;
- }
- }
-
- // Collect the yield predicates and desugar yields
- List<List<Cmd>> yields = new List<List<Cmd>>();
- List<Cmd> cmds = new List<Cmd>();
- if (proc.Requires.Count > 0)
- {
- Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- domainNameToScope[domainName] = new HashSet<Variable>();
- }
- foreach (Variable v in program.GlobalVariables())
- {
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- domainNameToScope[domainName].Add(v);
- }
- for (int i = 0; i < proc.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
- {
- Variable v = proc.InParams[i];
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- domainNameToScope[domainName].Add(v);
- }
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToInputVar[domainName], domainNameToScope[domainName])));
- }
- foreach (Requires r in proc.Requires)
- {
- if (r.Free)
- {
- cmds.Add(new AssumeCmd(r.tok, r.Condition));
- }
- else
- {
- AssertCmd assertCmd = new AssertCmd(r.tok, r.Condition, r.Attributes);
- assertCmd.ErrorData = "Non-interference check failed";
- cmds.Add(assertCmd);
- }
- }
- yields.Add(cmds);
- cmds = new List<Cmd>();
- }
- if (proc.Ensures.Count > 0)
- {
- Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- domainNameToScope[domainName] = new HashSet<Variable>();
- }
- foreach (Variable v in program.GlobalVariables())
- {
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- domainNameToScope[domainName].Add(v);
- }
- for (int i = 0; i < proc.OutParams.Count; i++)
- {
- Variable v = proc.OutParams[i];
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- domainNameToScope[domainName].Add(v);
- }
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToInputVar[domainName], domainNameToScope[domainName])));
- }
- foreach (Ensures e in proc.Ensures)
- {
- if (e.Free)
- {
- cmds.Add(new AssumeCmd(e.tok, e.Condition));
- }
- else
- {
- AssertCmd assertCmd = new AssertCmd(e.tok, e.Condition, e.Attributes);
- assertCmd.ErrorData = "Non-interference check failed";
- cmds.Add(assertCmd);
- }
- }
- yields.Add(cmds);
- cmds = new List<Cmd>();
- }
- CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());
- CreateYieldCheckerImplForOldStableEnsures(proc);
- }
-
- private void AddYieldProcAndImpl()
+ private void AddYieldProcAndImpl(List<Declaration> decls)
{
if (yieldProc == null) return;
@@ -1192,16 +1022,6 @@ namespace Microsoft.Boogie decls.Add(yieldImpl);
}
- public static HashSet<int> FindPhaseNums(QKeyValue kv)
- {
- HashSet<int> attrs = QKeyValue.FindIntAttributes(kv, "phase");
- if (attrs.Count == 0)
- {
- attrs.Add(0); // default phase of requires, ensures and assertions is 0
- }
- return attrs;
- }
-
public static QKeyValue RemoveYieldsAttribute(QKeyValue iter)
{
if (iter == null) return null;
@@ -1209,20 +1029,6 @@ namespace Microsoft.Boogie return (iter.Key == "yields") ? iter.Next : iter;
}
- public static QKeyValue RemoveStableAttribute(QKeyValue iter)
- {
- if (iter == null) return null;
- iter.Next = RemoveStableAttribute(iter.Next);
- return (iter.Key == "stable") ? iter.Next : iter;
- }
-
- public static QKeyValue RemoveQedAttribute(QKeyValue iter)
- {
- if (iter == null) return null;
- iter.Next = RemoveQedAttribute(iter.Next);
- return (iter.Key == "qed") ? iter.Next : iter;
- }
-
public static QKeyValue RemoveMoverAttribute(QKeyValue iter)
{
if (iter == null) return null;
@@ -1233,19 +1039,8 @@ namespace Microsoft.Boogie return iter;
}
- private void Transform(List<Implementation> impls, List<Procedure> procs)
+ private void Collect(List<Declaration> decls)
{
- foreach (var impl in impls)
- {
- pc = null;
- alpha = null;
- beta = null;
- TransformImpl(impl);
- }
- foreach (var proc in procs)
- {
- TransformProc(proc);
- }
foreach (Procedure proc in yieldCheckerProcs)
{
decls.Add(proc);
@@ -1258,70 +1053,69 @@ namespace Microsoft.Boogie {
decls.Add(proc);
}
- AddYieldProcAndImpl();
+ AddYieldProcAndImpl(decls);
}
public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
{
Program program = linearTypeChecker.program;
- foreach (int phaseNum in moverTypeChecker.allPhaseNums)
+ foreach (int phaseNum in moverTypeChecker.AllPhaseNums)
{
if (CommandLineOptions.Clo.TrustPhasesDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustPhasesUpto) continue;
MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum);
- List<Implementation> impls = new List<Implementation>();
- List<Procedure> procs = new List<Procedure>();
foreach (var decl in program.TopLevelDeclarations)
{
Procedure proc = decl as Procedure;
- if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
+ if (proc == null || !moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
Procedure duplicateProc = duplicator.VisitProcedure(proc);
- procs.Add(duplicateProc);
- if (moverTypeChecker.procToActionInfo.ContainsKey(proc) && moverTypeChecker.procToActionInfo[proc].phaseNum < phaseNum)
+ decls.Add(duplicateProc);
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[proc];
+ if (actionInfo.phaseNum < phaseNum)
{
- duplicateProc.Attributes = null;
- duplicateProc.Modifies = new List<IdentifierExpr>();
- program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(Expr.Ident(x)));
- CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(moverTypeChecker.procToActionInfo[proc].thisAction);
+ Implementation impl;
+ AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+ if (atomicActionInfo != null)
+ {
+ CodeExpr action = (CodeExpr)duplicator.VisitCodeExpr(atomicActionInfo.thisAction);
- List<Cmd> cmds = new List<Cmd>();
- foreach (AssertCmd assertCmd in moverTypeChecker.procToActionInfo[proc].thisGate)
+ List<Cmd> cmds = new List<Cmd>();
+ foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)
+ {
+ cmds.Add(new AssumeCmd(Token.NoToken, (Expr)duplicator.Visit(assertCmd.Expr)));
+ }
+ Block newInitBlock = new Block(Token.NoToken, "_init", cmds,
+ new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),
+ new List<Block>(new Block[] { action.Blocks[0] })));
+ List<Block> newBlocks = new List<Block>();
+ newBlocks.Add(newInitBlock);
+ newBlocks.AddRange(action.Blocks);
+ impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, newBlocks);
+ }
+ else
{
- cmds.Add(new AssumeCmd(Token.NoToken, (Expr)duplicator.Visit(assertCmd.Expr)));
+ Block newInitBlock = new Block(Token.NoToken, "_init", new List<Cmd>(), new ReturnCmd(Token.NoToken));
+ List<Block> newBlocks = new List<Block>();
+ newBlocks.Add(newInitBlock);
+ impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List<Variable>(), newBlocks);
}
- Block newInitBlock = new Block(Token.NoToken, "_init", cmds,
- new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),
- new List<Block>(new Block[] { action.Blocks[0] })));
- List<Block> newBlocks = new List<Block>();
- newBlocks.Add(newInitBlock);
- newBlocks.AddRange(action.Blocks);
- Implementation impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, action.LocVars, newBlocks);
impl.Proc = duplicateProc;
impl.Proc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
impl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- impls.Add(impl);
+ decls.Add(impl);
}
}
+ OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);
foreach (var decl in program.TopLevelDeclarations)
{
Implementation impl = decl as Implementation;
- if (impl == null ||
- !QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields") ||
- (moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) && moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum))
+ if (impl == null || !moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum)
continue;
Implementation duplicateImpl = duplicator.VisitImplementation(impl);
- impls.Add(duplicateImpl);
- }
- OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator, decls);
- ogTransform.Transform(impls, procs);
- foreach (var proc in procs)
- {
- decls.Add(proc);
- }
- foreach (var impl in impls)
- {
- decls.Add(impl);
+ ogTransform.TransformImpl(duplicateImpl);
+ decls.Add(duplicateImpl);
}
+ ogTransform.Collect(decls);
}
}
}
diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index a3a621ac..915eadda 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -9,22 +9,18 @@ namespace Microsoft.Boogie {
public static void Transform(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker)
{
- // The order in which originalDecls are computed and then *.AddCheckers are called is
- // apparently important. The MyDuplicator code currently does not duplicate Attributes.
- // Consequently, all the yield attributes are eliminated by the AddCheckers code.
-
List<Declaration> originalDecls = new List<Declaration>();
Program program = linearTypeChecker.program;
foreach (var decl in program.TopLevelDeclarations)
{
Procedure proc = decl as Procedure;
- if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
+ if (proc != null && moverTypeChecker.procToActionInfo.ContainsKey(proc))
{
originalDecls.Add(proc);
continue;
}
Implementation impl = decl as Implementation;
- if (impl != null && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))
+ if (impl != null && moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc))
{
originalDecls.Add(impl);
}
@@ -38,17 +34,7 @@ namespace Microsoft.Boogie }
foreach (Declaration decl in decls)
{
- Procedure proc = decl as Procedure;
- if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))
- {
- proc.Modifies = new List<IdentifierExpr>();
- linearTypeChecker.program.GlobalVariables().Iter(x => proc.Modifies.Add(Expr.Ident(x)));
- }
- }
- foreach (Declaration decl in decls)
- {
decl.Attributes = OwickiGries.RemoveYieldsAttribute(decl.Attributes);
- decl.Attributes = OwickiGries.RemoveStableAttribute(decl.Attributes);
}
program.TopLevelDeclarations.RemoveAll(x => originalDecls.Contains(x));
program.TopLevelDeclarations.AddRange(decls);
diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 5a8c81f6..2c4d8327 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -20,10 +20,31 @@ namespace Microsoft.Boogie public class ActionInfo
{
public Procedure proc;
- public Ensures ensures;
- public MoverType moverType;
public int phaseNum;
public int availableUptoPhaseNum;
+
+ public ActionInfo(Procedure proc, int phaseNum, int availableUptoPhaseNum)
+ {
+ this.proc = proc;
+ this.phaseNum = phaseNum;
+ this.availableUptoPhaseNum = availableUptoPhaseNum;
+ }
+
+ public virtual bool IsRightMover
+ {
+ get { return true; }
+ }
+
+ public virtual bool IsLeftMover
+ {
+ get { return true; }
+ }
+ }
+
+ public class AtomicActionInfo : ActionInfo
+ {
+ public Ensures ensures;
+ public MoverType moverType;
public List<AssertCmd> thisGate;
public CodeExpr thisAction;
public List<Variable> thisInParams;
@@ -32,38 +53,36 @@ namespace Microsoft.Boogie public CodeExpr thatAction;
public List<Variable> thatInParams;
public List<Variable> thatOutParams;
- public HashSet<Variable> usedGlobalVars;
+ public HashSet<Variable> actionUsedGlobalVars;
public HashSet<Variable> modifiedGlobalVars;
public HashSet<Variable> gateUsedGlobalVars;
public bool hasAssumeCmd;
- public bool CommutesWith(ActionInfo actionInfo)
+ public bool CommutesWith(AtomicActionInfo actionInfo)
{
- if (this.modifiedGlobalVars.Intersect(actionInfo.usedGlobalVars).Count() > 0)
+ if (this.modifiedGlobalVars.Intersect(actionInfo.actionUsedGlobalVars).Count() > 0)
return false;
- if (this.usedGlobalVars.Intersect(actionInfo.modifiedGlobalVars).Count() > 0)
+ if (this.actionUsedGlobalVars.Intersect(actionInfo.modifiedGlobalVars).Count() > 0)
return false;
return true;
}
- public bool IsRightMover
+ public override bool IsRightMover
{
get { return moverType == MoverType.Right || moverType == MoverType.Both; }
}
- public bool IsLeftMover
+ public override bool IsLeftMover
{
get { return moverType == MoverType.Left || moverType == MoverType.Both; }
}
- public ActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoPhaseNum)
+ public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoPhaseNum)
+ : base(proc, phaseNum, availableUptoPhaseNum)
{
CodeExpr codeExpr = ensures.Condition as CodeExpr;
- this.proc = proc;
this.ensures = ensures;
this.moverType = moverType;
- this.phaseNum = phaseNum;
- this.availableUptoPhaseNum = availableUptoPhaseNum;
this.thisGate = new List<AssertCmd>();
this.thisAction = codeExpr;
this.thisInParams = new List<Variable>();
@@ -162,7 +181,7 @@ namespace Microsoft.Boogie {
VariableCollector collector = new VariableCollector();
collector.Visit(codeExpr);
- this.usedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
+ this.actionUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));
}
List<Variable> modifiedVars = new List<Variable>();
@@ -182,35 +201,96 @@ namespace Microsoft.Boogie public class MoverTypeChecker : ReadOnlyVisitor
{
- public int FindPhaseNumber(Procedure proc)
- {
- if (procToActionInfo.ContainsKey(proc))
- return procToActionInfo[proc].phaseNum;
- else
- return int.MaxValue;
- }
-
CheckingContext checkingContext;
public int errorCount;
- public Dictionary<Variable, int> qedGlobalVariables;
+ public Dictionary<Variable, int> introducePhaseNums;
+ public Dictionary<Variable, int> hidePhaseNums;
Procedure enclosingProc;
public Dictionary<Procedure, ActionInfo> procToActionInfo;
public Program program;
- public HashSet<int> allPhaseNums;
- bool inAtomicSpecification;
bool inSpecification;
int minPhaseNum;
+ int maxPhaseNum;
+ public Dictionary<Absy, HashSet<int>> absyToPhaseNums;
+
+ private static List<int> FindIntAttributes(QKeyValue kv, string name)
+ {
+ Contract.Requires(name != null);
+ HashSet<int> attrs = new HashSet<int>();
+ for (; kv != null; kv = kv.Next)
+ {
+ if (kv.Key != name) continue;
+ foreach (var o in kv.Params)
+ {
+ Expr e = o as Expr;
+ if (e == null) continue;
+ LiteralExpr l = e as LiteralExpr;
+ if (l != null && l.isBigNum)
+ attrs.Add(l.asBigNum.ToIntSafe);
+ }
+ }
+ List<int> phases = attrs.ToList();
+ phases.Sort();
+ return phases;
+ }
+
+ private static MoverType GetMoverType(Ensures e)
+ {
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
+ return MoverType.Atomic;
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "right"))
+ return MoverType.Right;
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "left"))
+ return MoverType.Left;
+ if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
+ return MoverType.Both;
+ return MoverType.Top;
+ }
+
+ private HashSet<int> allPhaseNums;
+ public IEnumerable<int> AllPhaseNums
+ {
+ get
+ {
+ if (allPhaseNums == null)
+ {
+ allPhaseNums = new HashSet<int>();
+ foreach (ActionInfo actionInfo in procToActionInfo.Values)
+ {
+ allPhaseNums.Add(actionInfo.phaseNum);
+ }
+ }
+ return allPhaseNums;
+ }
+ }
public void TypeCheck()
{
foreach (Declaration decl in program.TopLevelDeclarations)
{
Procedure proc = decl as Procedure;
- if (proc == null) continue;
+ if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue;
+
+ int phaseNum = int.MaxValue;
+ int availableUptoPhaseNum = int.MaxValue;
+ List<int> attrs = FindIntAttributes(proc.Attributes, "phase");
+ if (attrs.Count == 1)
+ {
+ phaseNum = attrs[0];
+ }
+ else if (attrs.Count == 2)
+ {
+ phaseNum = attrs[0];
+ availableUptoPhaseNum = attrs[1];
+ }
+ else
+ {
+ Error(proc, "Incorrect number of phases");
+ continue;
+ }
foreach (Ensures e in proc.Ensures)
{
- int phaseNum, availableUptoPhaseNum;
- MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum, out availableUptoPhaseNum);
+ MoverType moverType = GetMoverType(e);
if (moverType == MoverType.Top) continue;
CodeExpr codeExpr = e.Condition as CodeExpr;
if (codeExpr == null)
@@ -223,19 +303,16 @@ namespace Microsoft.Boogie Error(proc, "A procedure can have at most one atomic action");
continue;
}
- if (phaseNum >= availableUptoPhaseNum)
- {
- Error(proc, "Available at phase number should be less than available up to phase number");
- continue;
- }
- if (phaseNum != int.MaxValue)
- {
- allPhaseNums.Add(phaseNum);
- }
- procToActionInfo[proc] = new ActionInfo(proc, e, moverType, phaseNum, availableUptoPhaseNum);
+ procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, phaseNum, availableUptoPhaseNum);
+ }
+ if (!procToActionInfo.ContainsKey(proc))
+ {
+ procToActionInfo[proc] = new ActionInfo(proc, phaseNum, availableUptoPhaseNum);
}
}
+ if (errorCount > 0) return;
this.VisitProgram(program);
+ if (errorCount > 0) return;
#if QED
YieldTypeChecker.PerformYieldSafeCheck(this);
#endif
@@ -243,132 +320,159 @@ namespace Microsoft.Boogie public MoverTypeChecker(Program program)
{
- this.qedGlobalVariables = new Dictionary<Variable, int>();
+ this.absyToPhaseNums = new Dictionary<Absy, HashSet<int>>();
+ this.introducePhaseNums = new Dictionary<Variable, int>();
+ this.hidePhaseNums = new Dictionary<Variable, int>();
+ this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+ this.errorCount = 0;
+ this.checkingContext = new CheckingContext(null);
+ this.program = program;
+ this.enclosingProc = null;
+ this.inSpecification = false;
+ this.minPhaseNum = int.MaxValue;
+ this.maxPhaseNum = -1;
foreach (var g in program.GlobalVariables())
{
- if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))
+ List<int> phaseNums = FindIntAttributes(g.Attributes, "phase");
+ this.introducePhaseNums[g] = 0;
+ this.hidePhaseNums[g] = int.MaxValue;
+ if (phaseNums.Count == 0)
{
- this.qedGlobalVariables.Add(g, int.MaxValue);
- g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);
+ // ok
+ }
+ else if (phaseNums.Count == 1)
+ {
+ this.hidePhaseNums[g] = phaseNums[0];
+ }
+ else if (phaseNums.Count == 2)
+ {
+ this.introducePhaseNums[g] = phaseNums[0];
+ this.hidePhaseNums[g] = phaseNums[1];
}
else
{
- int phaseNum = QKeyValue.FindIntAttribute(g.Attributes, "qed", int.MaxValue);
- if (phaseNum == int.MaxValue) continue;
- this.qedGlobalVariables.Add(g, phaseNum);
- g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);
+ Error(g, "Too many phase numbers");
}
}
- this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
- this.allPhaseNums = new HashSet<int>();
- this.errorCount = 0;
- this.checkingContext = new CheckingContext(null);
- this.program = program;
- this.enclosingProc = null;
- this.inAtomicSpecification = false;
- this.inSpecification = false;
- this.minPhaseNum = int.MaxValue;
}
+
public override Implementation VisitImplementation(Implementation node)
{
+ if (!procToActionInfo.ContainsKey(node.Proc))
+ {
+ return node;
+ }
this.enclosingProc = node.Proc;
return base.VisitImplementation(node);
}
+
public override Procedure VisitProcedure(Procedure node)
{
+ if (!procToActionInfo.ContainsKey(node))
+ {
+ return node;
+ }
this.enclosingProc = node;
return base.VisitProcedure(node);
}
+
public override Cmd VisitCallCmd(CallCmd node)
{
- if (!node.IsAsync)
+ int enclosingProcPhaseNum = procToActionInfo[enclosingProc].phaseNum;
+ if (procToActionInfo.ContainsKey(node.Proc))
{
- int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc);
- int calleePhaseNum = FindPhaseNumber(node.Proc);
- if (enclosingProcPhaseNum == int.MaxValue)
- {
-
- }
- else if (calleePhaseNum == int.MaxValue)
+ ActionInfo actionInfo = procToActionInfo[node.Proc];
+ if (node.IsAsync && actionInfo is AtomicActionInfo)
{
- Error(node, "An atomic procedure cannot call a non-atomic procedure");
+ Error(node, "Target of async call cannot be an atomic action");
}
- else if (enclosingProcPhaseNum <= calleePhaseNum)
+ int calleePhaseNum = procToActionInfo[node.Proc].phaseNum;
+ if (enclosingProcPhaseNum < calleePhaseNum ||
+ (enclosingProcPhaseNum == calleePhaseNum && actionInfo is AtomicActionInfo))
{
Error(node, "The phase of the caller procedure must be greater than the phase of the callee");
}
- else if (procToActionInfo[node.Proc].availableUptoPhaseNum < enclosingProcPhaseNum)
+ if (actionInfo.availableUptoPhaseNum < enclosingProcPhaseNum)
{
Error(node, "The callee is not available in the phase of the caller procedure");
}
}
return base.VisitCallCmd(node);
}
+
public override Cmd VisitParCallCmd(ParCallCmd node)
{
+ int enclosingProcPhaseNum = procToActionInfo[enclosingProc].phaseNum;
+ bool isLeftMover = true;
+ bool isRightMover = true;
int maxCalleePhaseNum = 0;
+ int numAtomicActions = 0;
foreach (CallCmd iter in node.CallCmds)
{
- int calleePhaseNum = FindPhaseNumber(iter.Proc);
- if (calleePhaseNum > maxCalleePhaseNum)
- maxCalleePhaseNum = calleePhaseNum;
- }
- int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc);
- 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 actionInfo = procToActionInfo[iter.Proc];
+ isLeftMover = isLeftMover && actionInfo.IsLeftMover;
+ isRightMover = isRightMover && actionInfo.IsRightMover;
+ if (actionInfo.phaseNum > maxCalleePhaseNum)
+ {
+ maxCalleePhaseNum = actionInfo.phaseNum;
}
- if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)
+ if (actionInfo is AtomicActionInfo)
{
- Error(node, "The procedures in the parallel call must be all right mover or all left mover");
+ numAtomicActions++;
}
- return base.VisitParCallCmd(node);
}
- else
+ if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1)
{
- return node;
+ Error(node, "The procedures in the parallel call must be all right mover or all left mover");
}
+ if (maxCalleePhaseNum == enclosingProcPhaseNum && numAtomicActions > 0)
+ {
+ Error(node, "At phase {0}, either no callee is an atomic action or no callee phase equals the phase of the enclosing procedure");
+ }
+ return base.VisitParCallCmd(node);
}
+
public override Expr VisitIdentifierExpr(IdentifierExpr node)
{
if (node.Decl is GlobalVariable)
{
- if (qedGlobalVariables.ContainsKey(node.Decl) && qedGlobalVariables[node.Decl] < minPhaseNum)
- {
- minPhaseNum = qedGlobalVariables[node.Decl];
- }
-
- if (inAtomicSpecification && !qedGlobalVariables.ContainsKey(node.Decl))
+ if (!inSpecification)
{
- Error(node, "Cannot access non-qed global variable in atomic action");
+ Error(node, "Global variable can be accessed only in atomic actions or specifications");
}
- else if (!inSpecification && qedGlobalVariables.ContainsKey(node.Decl))
+ else
{
- Error(node, "Cannot access qed global variable in ordinary code");
+ if (hidePhaseNums[node.Decl] < minPhaseNum)
+ {
+ minPhaseNum = hidePhaseNums[node.Decl];
+ }
+ if (introducePhaseNums[node.Decl] > maxPhaseNum)
+ {
+ maxPhaseNum = introducePhaseNums[node.Decl];
+ }
}
}
return base.VisitIdentifierExpr(node);
}
+
public override Ensures VisitEnsures(Ensures ensures)
{
minPhaseNum = int.MaxValue;
- inAtomicSpecification = procToActionInfo.ContainsKey(enclosingProc) && procToActionInfo[enclosingProc].ensures == ensures;
+ maxPhaseNum = -1;
inSpecification = true;
Ensures ret = base.VisitEnsures(ensures);
inSpecification = false;
- if (inAtomicSpecification)
+ AtomicActionInfo atomicActionInfo = procToActionInfo[enclosingProc] as AtomicActionInfo;
+ if (atomicActionInfo != null && atomicActionInfo.ensures == ensures)
{
- if (procToActionInfo[enclosingProc].availableUptoPhaseNum > minPhaseNum)
+ if (maxPhaseNum <= atomicActionInfo.phaseNum && atomicActionInfo.availableUptoPhaseNum <= minPhaseNum)
+ {
+ // ok
+ }
+ else
{
Error(ensures, "A variable being accessed is hidden before this action becomes unavailable");
}
- inAtomicSpecification = false;
}
else
{
@@ -376,18 +480,22 @@ namespace Microsoft.Boogie }
return ret;
}
+
public override Requires VisitRequires(Requires requires)
{
minPhaseNum = int.MaxValue;
+ maxPhaseNum = -1;
inSpecification = true;
Requires ret = base.VisitRequires(requires);
inSpecification = false;
CheckAndAddPhases(requires, requires.Attributes);
return ret;
}
+
public override Cmd VisitAssertCmd(AssertCmd node)
{
minPhaseNum = int.MaxValue;
+ maxPhaseNum = -1;
inSpecification = true;
Cmd ret = base.VisitAssertCmd(node);
inSpecification = false;
@@ -397,19 +505,26 @@ namespace Microsoft.Boogie private void CheckAndAddPhases(Absy node, QKeyValue attributes)
{
- foreach (int phaseNum in OwickiGries.FindPhaseNums(attributes))
+ List<int> attrs = FindIntAttributes(attributes, "phase");
+ if (attrs.Count == 0)
+ {
+ Error(node, "phase not present");
+ return;
+ }
+ absyToPhaseNums[node] = new HashSet<int>();
+ foreach (int phaseNum in attrs)
{
- if (phaseNum > FindPhaseNumber(enclosingProc))
+ if (phaseNum > procToActionInfo[enclosingProc].phaseNum)
{
Error(node, "The phase cannot be greater than the phase of enclosing procedure");
}
- else if (phaseNum > minPhaseNum)
+ else if (maxPhaseNum < phaseNum && phaseNum <= minPhaseNum)
{
- Error(node, "A variable being accessed is hidden before this specification becomes unavailable");
+ absyToPhaseNums[node].Add(phaseNum);
}
else
{
- allPhaseNums.Add(phaseNum);
+ Error(node, string.Format("A variable being accessed in this specification is unavailable at phase {0}", phaseNum));
}
}
}
diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 4ba23c2e..d976dfe2 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -75,7 +75,7 @@ namespace Microsoft.Boogie yieldTypeCheckerAutomatonEdges.Add(new Tuple<int, int, int>(source, label, dest));
}
- public void IsYieldTypeSafe()
+ private void IsYieldTypeSafe()
{
List<int[]> transitions = new List<int[]>();
foreach (Tuple<int, int> e in edgeLabels.Keys)
@@ -150,7 +150,7 @@ namespace Microsoft.Boogie }
}
- static bool IsTerminatingLoopHeader(Block block)
+ private static bool IsTerminatingLoopHeader(Block block)
{
foreach (Cmd cmd in block.Cmds)
{
@@ -163,7 +163,7 @@ namespace Microsoft.Boogie return false;
}
- public string PrintErrorTrace(Automaton<BvSet> errorAutomaton)
+ private string PrintErrorTrace(Automaton<BvSet> errorAutomaton)
{
String s = "\nBody of " + impl.Proc.Name + " is not yield_type_safe at phase " + currPhaseNum.ToString() + "\n";
foreach (var move in errorAutomaton.GetMoves())
@@ -182,29 +182,19 @@ namespace Microsoft.Boogie foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)
{
Implementation impl = decl as Implementation;
- if (impl == null) continue;
+ if (impl == null || !moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum == 0) continue;
impl.PruneUnreachableBlocks();
Graph<Block> implGraph = Program.GraphFromImpl(impl);
implGraph.ComputeLoops();
- int phaseNumSpecImpl = moverTypeChecker.FindPhaseNumber(impl.Proc);
- foreach (int phaseNum in moverTypeChecker.allPhaseNums)
+ int specPhaseNum = moverTypeChecker.procToActionInfo[impl.Proc].phaseNum;
+ foreach (int phaseNum in moverTypeChecker.AllPhaseNums)
{
- if (phaseNum > phaseNumSpecImpl) continue;
+ if (phaseNum > specPhaseNum) continue;
YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, phaseNum, implGraph.Headers);
}
}
}
- public MoverType FindMoverType(Procedure proc)
- {
- if (!moverTypeChecker.procToActionInfo.ContainsKey(proc))
- return MoverType.Top;
- ActionInfo actionInfo = moverTypeChecker.procToActionInfo[proc];
- if (actionInfo.phaseNum >= currPhaseNum)
- return MoverType.Top;
- return actionInfo.moverType;
- }
-
int stateCounter;
MoverTypeChecker moverTypeChecker;
Implementation impl;
@@ -216,7 +206,7 @@ namespace Microsoft.Boogie Dictionary<Tuple<int, int>, int> edgeLabels;
IEnumerable<Block> loopHeaders;
- public YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum, IEnumerable<Block> loopHeaders)
+ private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum, IEnumerable<Block> loopHeaders)
{
this.moverTypeChecker = moverTypeChecker;
this.impl = impl;
@@ -283,11 +273,33 @@ namespace Microsoft.Boogie CallCmd callCmd = cmd as CallCmd;
if (callCmd.IsAsync)
{
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+ if (currPhaseNum <= actionInfo.phaseNum)
+ edgeLabels[edge] = 'L';
+ else
+ edgeLabels[edge] = 'B';
+ }
+ else if (!moverTypeChecker.procToActionInfo.ContainsKey(callCmd.Proc))
+ {
edgeLabels[edge] = 'P';
}
else
{
- switch (FindMoverType(callCmd.Proc))
+ MoverType moverType;
+ ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];
+ if (actionInfo.phaseNum >= currPhaseNum)
+ {
+ moverType = MoverType.Top;
+ }
+ else
+ {
+ AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
+ if (atomicActionInfo == null)
+ moverType = MoverType.Both;
+ else
+ moverType = atomicActionInfo.moverType;
+ }
+ switch (moverType)
{
case MoverType.Atomic:
edgeLabels[edge] = 'A';
@@ -302,8 +314,7 @@ namespace Microsoft.Boogie edgeLabels[edge] = 'R';
break;
case MoverType.Top:
- finalStates.Add(curr);
- initialStates.Add(next);
+ edgeLabels[edge] = 'Y';
break;
}
}
@@ -316,8 +327,7 @@ namespace Microsoft.Boogie bool isLeftMover = true;
foreach (CallCmd callCmd in parCallCmd.CallCmds)
{
- int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(callCmd.Proc);
- if (phaseSpecCallee >= currPhaseNum)
+ if (moverTypeChecker.procToActionInfo[callCmd.Proc].phaseNum >= currPhaseNum)
{
isYield = true;
}
|