From 36e016acf963b7c19d59640b11b4a40f2072943e Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 3 May 2014 10:06:13 -0700 Subject: checkpoint --- Source/Concurrency/MoverCheck.cs | 229 ++++----------- Source/Concurrency/OwickiGries.cs | 514 ++++++++++----------------------- Source/Concurrency/Program.cs | 18 +- Source/Concurrency/TypeCheck.cs | 319 +++++++++++++------- Source/Concurrency/YieldTypeChecker.cs | 56 ++-- Source/Core/AbsyCmd.cs | 8 - Source/Core/AbsyQuant.cs | 31 -- Source/Core/DeadVarElim.cs | 11 - 8 files changed, 470 insertions(+), 716 deletions(-) (limited to 'Source') 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 decls; - HashSet> commutativityCheckerCache; - HashSet> gatePreservationCheckerCache; - HashSet> failurePreservationCheckerCache; + HashSet> commutativityCheckerCache; + HashSet> gatePreservationCheckerCache; + HashSet> failurePreservationCheckerCache; private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) { this.linearTypeChecker = linearTypeChecker; this.moverTypeChecker = moverTypeChecker; this.decls = decls; - this.commutativityCheckerCache = new HashSet>(); - this.gatePreservationCheckerCache = new HashSet>(); - this.failurePreservationCheckerCache = new HashSet>(); + this.commutativityCheckerCache = new HashSet>(); + this.gatePreservationCheckerCache = new HashSet>(); + this.failurePreservationCheckerCache = new HashSet>(); } public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) @@ -63,18 +30,20 @@ namespace Microsoft.Boogie if (moverTypeChecker.procToActionInfo.Count == 0) return; - Dictionary> pools = new Dictionary>(); + Dictionary> pools = new Dictionary>(); 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(); + pools[phaseNum] = new HashSet(); } - 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 cmdStack; private List paths; private HashSet frame; + private HashSet postExistVars; - public TransitionRelationComputation(Program program, ActionInfo second, HashSet frame) + public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet frame, HashSet 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 frame, HashSet postExistVars) { - this.frame = new HashSet(program.GlobalVariables()); - TransitionRelationComputationHelper(program, null, second); - } - - public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second) - { - this.frame = new HashSet(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 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 subst = new Dictionary(); - 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(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 DisjointnessRequires(Program program, ActionInfo first, ActionInfo second) + private List DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet frame) { List requires = new List(); Dictionary> domainNameToScope = new Dictionary>(); @@ -491,16 +424,13 @@ namespace Microsoft.Boogie { domainNameToScope[domainName] = new HashSet(); } - /* - // 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 actionPair = new Tuple(first, second); + Tuple actionPair = new Tuple(first, second); if (commutativityCheckerCache.Contains(actionPair)) return; commutativityCheckerCache.Add(actionPair); @@ -561,13 +491,18 @@ namespace Microsoft.Boogie List blocks = new List(); blocks.AddRange(firstBlocks); blocks.AddRange(secondBlocks); - List requires = DisjointnessRequires(program, first, second); + HashSet frame = new HashSet(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(first.actionUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List 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 = new List(); - Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).TransitionRelationCompute(); + Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet())).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 actionPair = new Tuple(first, second); + Tuple actionPair = new Tuple(first, second); if (gatePreservationCheckerCache.Contains(actionPair)) return; gatePreservationCheckerCache.Add(actionPair); @@ -599,7 +534,11 @@ namespace Microsoft.Boogie List locals = new List(); locals.AddRange(second.thisAction.LocVars); List secondBlocks = CloneBlocks(second.thisAction.Blocks); - List requires = DisjointnessRequires(program, first, second); + HashSet frame = new HashSet(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List requires = DisjointnessRequires(program, first, second, frame); List ensures = new List(); 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 actionPair = new Tuple(first, second); + Tuple actionPair = new Tuple(first, second); if (failurePreservationCheckerCache.Contains(actionPair)) return; failurePreservationCheckerCache.Add(actionPair); @@ -638,7 +577,11 @@ namespace Microsoft.Boogie List locals = new List(); locals.AddRange(second.thisAction.LocVars); List secondBlocks = CloneBlocks(second.thisAction.Blocks); - List requires = DisjointnessRequires(program, first, second); + HashSet frame = new HashSet(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List 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 actionPair = new Tuple(first, second); - if (failurePreservationCheckerCache.Contains(actionPair)) - return; - failurePreservationCheckerCache.Add(actionPair); - - List inputs = new List(); - 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 = 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 = new List(); - 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 blocks = new List(); - blocks.Add(new Block(Token.NoToken, "L", new List(), new ReturnCmd(Token.NoToken))); - string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); - List globalVars = new List(); - program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x))); - Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, new List(), requires, globalVars, ensures); - Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, new List(), new List(), 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 inputs = new List(); inputs.AddRange(second.thisInParams); - List requires = DisjointnessRequires(program, null, second); + HashSet frame = new HashSet(); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List 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 postExistVars = new HashSet(); + postExistVars.UnionWith(frame); + postExistVars.UnionWith(second.thisOutParams); + Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute(); List ensures = new List(); 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 procMap; /* Original -> Duplicate */ public Dictionary absyMap; /* Duplicate -> Original */ public Dictionary blockMap; /* Original -> Duplicate */ + public Dictionary implMap; /* Duplicate -> Original */ + public HashSet yieldingProcs; public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum) { this.moverTypeChecker = moverTypeChecker; @@ -26,30 +28,27 @@ namespace Microsoft.Boogie this.procMap = new Dictionary(); this.absyMap = new Dictionary(); this.blockMap = new Dictionary(); + this.implMap = new Dictionary(); + this.yieldingProcs = new HashSet(); } private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List 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 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(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) } ))); + newCmds.Add(new HavocCmd(Token.NoToken, new List(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); Dictionary map = new Dictionary(); 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(); proc.Ensures = new List(); } 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(); + 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 absyMap; - Dictionary reverseProcMap; + Dictionary implMap; + HashSet yieldingProcs; int phaseNum; - List decls; List globalMods; Dictionary asyncAndParallelCallDesugarings; List yieldCheckerProcs; List yieldCheckerImpls; Procedure yieldProc; - public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator, List 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(); - 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(); 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 iteArgs = new List(new Expr[] { bb, Expr.Ident(pc), Expr.True }); + // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g); List pcUpdateLHS = new List( new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), @@ -327,7 +329,7 @@ namespace Microsoft.Boogie }); List pcUpdateRHS = new List( 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 frame; private Expr OldEqualityExpr(Dictionary 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 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 cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) { AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); @@ -470,8 +488,7 @@ namespace Microsoft.Boogie } count++; } - proc = new Procedure(Token.NoToken, procName, new List(), inParams, outParams, requiresSeq, new List(), ensuresSeq); - proc.AddAttribute("yields"); + proc = new Procedure(Token.NoToken, procName, new List(), 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 map = new Dictionary(); - Dictionary oldGlobalMap = new Dictionary(); - Dictionary identityGlobalMap = new Dictionary(); - List locals = new List(); - List inputs = new List(); - 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 requiresMap = new Dictionary(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 yieldCheckerBlocks = new List(); - List labels = new List(); - List labelTargets = new List(); - Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); - labels.Add(yieldCheckerBlock.Label); - labelTargets.Add(yieldCheckerBlock); - yieldCheckerBlocks.Add(yieldCheckerBlock); - List newCmds = new List(); - 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(), 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(), new List(), new List(), new List()); - 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(), 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> yields, Dictionary 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 alwaysMap = new Dictionary(); + 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 alwaysMap = new Dictionary(); - 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 foroldMap = new Dictionary(); + foreach (IdentifierExpr ie in globalMods) + { + foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); + } + Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); + frame = new HashSet(program.GlobalVariables()); + HashSet introducedVars = new HashSet(); + 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 foroldMap = new Dictionary(); - 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 frame = new HashSet(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 availableLinearVars = new HashSet(AvailableLinearVars(callCmd)); linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars); @@ -915,7 +852,7 @@ namespace Microsoft.Boogie cmds = new List(); } } - 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( - 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(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 domainNameToInputVar = new Dictionary(); - { - 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> yields = new List>(); - List cmds = new List(); - if (proc.Requires.Count > 0) - { - Dictionary> domainNameToScope = new Dictionary>(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - domainNameToScope[domainName] = new HashSet(); - } - 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(); - } - if (proc.Ensures.Count > 0) - { - Dictionary> domainNameToScope = new Dictionary>(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - domainNameToScope[domainName] = new HashSet(); - } - 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(); - } - CreateYieldCheckerImpl(proc, yields, new Dictionary()); - CreateYieldCheckerImplForOldStableEnsures(proc); - } - - private void AddYieldProcAndImpl() + private void AddYieldProcAndImpl(List decls) { if (yieldProc == null) return; @@ -1192,16 +1022,6 @@ namespace Microsoft.Boogie decls.Add(yieldImpl); } - public static HashSet FindPhaseNums(QKeyValue kv) - { - HashSet 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 impls, List procs) + private void Collect(List 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 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 impls = new List(); - List procs = new List(); 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(); - 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 cmds = new List(); - foreach (AssertCmd assertCmd in moverTypeChecker.procToActionInfo[proc].thisGate) + List cmds = new List(); + 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(new string[] { action.Blocks[0].Label }), + new List(new Block[] { action.Blocks[0] }))); + List newBlocks = new List(); + 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(), new ReturnCmd(Token.NoToken)); + List newBlocks = new List(); + newBlocks.Add(newInitBlock); + impl = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List(), newBlocks); } - Block newInitBlock = new Block(Token.NoToken, "_init", cmds, - new GotoCmd(Token.NoToken, new List(new string[] { action.Blocks[0].Label }), - new List(new Block[] { action.Blocks[0] }))); - List newBlocks = new List(); - 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 originalDecls = new List(); 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); } @@ -37,18 +33,8 @@ namespace Microsoft.Boogie MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls); } foreach (Declaration decl in decls) - { - Procedure proc = decl as Procedure; - if (proc != null && QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) - { - proc.Modifies = new List(); - 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 thisGate; public CodeExpr thisAction; public List thisInParams; @@ -32,38 +53,36 @@ namespace Microsoft.Boogie public CodeExpr thatAction; public List thatInParams; public List thatOutParams; - public HashSet usedGlobalVars; + public HashSet actionUsedGlobalVars; public HashSet modifiedGlobalVars; public HashSet 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(); this.thisAction = codeExpr; this.thisInParams = new List(); @@ -162,7 +181,7 @@ namespace Microsoft.Boogie { VariableCollector collector = new VariableCollector(); collector.Visit(codeExpr); - this.usedGlobalVars = new HashSet(collector.usedVars.Where(x => x is GlobalVariable)); + this.actionUsedGlobalVars = new HashSet(collector.usedVars.Where(x => x is GlobalVariable)); } List modifiedVars = new List(); @@ -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 qedGlobalVariables; + public Dictionary introducePhaseNums; + public Dictionary hidePhaseNums; Procedure enclosingProc; public Dictionary procToActionInfo; public Program program; - public HashSet allPhaseNums; - bool inAtomicSpecification; bool inSpecification; int minPhaseNum; + int maxPhaseNum; + public Dictionary> absyToPhaseNums; + + private static List FindIntAttributes(QKeyValue kv, string name) + { + Contract.Requires(name != null); + HashSet attrs = new HashSet(); + 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 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 allPhaseNums; + public IEnumerable AllPhaseNums + { + get + { + if (allPhaseNums == null) + { + allPhaseNums = new HashSet(); + 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 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(); + this.absyToPhaseNums = new Dictionary>(); + this.introducePhaseNums = new Dictionary(); + this.hidePhaseNums = new Dictionary(); + this.procToActionInfo = new Dictionary(); + 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 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(); - this.allPhaseNums = new HashSet(); - 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 attrs = FindIntAttributes(attributes, "phase"); + if (attrs.Count == 0) + { + Error(node, "phase not present"); + return; + } + absyToPhaseNums[node] = new HashSet(); + 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(source, label, dest)); } - public void IsYieldTypeSafe() + private void IsYieldTypeSafe() { List transitions = new List(); foreach (Tuple 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 errorAutomaton) + private string PrintErrorTrace(Automaton 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 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, int> edgeLabels; IEnumerable loopHeaders; - public YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum, IEnumerable loopHeaders) + private YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum, IEnumerable loopHeaders) { this.moverTypeChecker = moverTypeChecker; this.impl = impl; @@ -282,12 +272,34 @@ 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; } diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index cd7a8edd..72dc7c86 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1843,10 +1843,6 @@ namespace Microsoft.Boogie { { tc.Error(callCmd, "target procedure of a parallel call must yield"); } - if (!QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "stable")) - { - tc.Error(callCmd, "target procedure of a parallel call must be stable"); - } } } foreach (CallCmd callCmd in CallCmds) @@ -2134,10 +2130,6 @@ namespace Microsoft.Boogie { { tc.Error(this, "target procedure of an async call must yield"); } - if (!QKeyValue.FindBoolAttribute(Proc.Attributes, "stable")) - { - tc.Error(this, "target procedure of an async call must be stable"); - } } } diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 10a13511..397d8eba 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -321,37 +321,6 @@ namespace Microsoft.Boogie { return defl; } - public static HashSet FindExprAttributes(QKeyValue kv, string name) - { - Contract.Requires(name != null); - HashSet attrs = new HashSet(); - for (; kv != null; kv = kv.Next) - { - if (kv.Key == name) - { - if (kv.Params.Count == 1 && kv.Params[0] is Expr) - { - attrs.Add((Expr)kv.Params[0]); - } - } - } - return attrs; - } - - public static HashSet FindIntAttributes(QKeyValue kv, string name) - { - Contract.Requires(name != null); - HashSet attrs = new HashSet(); - HashSet es = FindExprAttributes(kv, name); - foreach (Expr e in es) - { - LiteralExpr l = e as LiteralExpr; - if (l != null && l.isBigNum) - attrs.Add(l.asBigNum.ToIntSafe); - } - return attrs; - } - public override Absy Clone() { List newParams = new List(); foreach (object o in Params) diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index e14d4fd3..c32a921b 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -42,7 +42,6 @@ namespace Microsoft.Boogie { static Procedure enclosingProc; static Dictionary/*!*/>/*!*/ modSets; static HashSet yieldingProcs; - static HashSet asyncAndParallelCallTargetProcs; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullDictionaryAndValues(modSets)); @@ -70,7 +69,6 @@ namespace Microsoft.Boogie { modSets = new Dictionary/*!*/>(); yieldingProcs = new HashSet(); - asyncAndParallelCallTargetProcs = new HashSet(); HashSet implementedProcs = new HashSet(); foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) { @@ -124,13 +122,6 @@ namespace Microsoft.Boogie { x.AddAttribute("yields"); } } - foreach (Procedure x in asyncAndParallelCallTargetProcs) - { - if (!QKeyValue.FindBoolAttribute(x.Attributes, "stable")) - { - x.AddAttribute("stable"); - } - } #if DEBUG_PRINT Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); @@ -213,7 +204,6 @@ namespace Microsoft.Boogie { } if (callCmd.IsAsync) { - asyncAndParallelCallTargetProcs.Add(callCmd.Proc); if (!yieldingProcs.Contains(callCmd.Proc)) { yieldingProcs.Add(callCmd.Proc); @@ -234,7 +224,6 @@ namespace Microsoft.Boogie { } foreach (CallCmd callCmd in node.CallCmds) { - asyncAndParallelCallTargetProcs.Add(callCmd.Proc); if (!yieldingProcs.Contains(callCmd.Proc)) { yieldingProcs.Add(callCmd.Proc); -- cgit v1.2.3