From e194828cb1051612dda9a6c51696fed7abc69cd3 Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 16 Apr 2014 14:23:07 -0700 Subject: added variable hiding added annotation on an atomic action about the phases in which it exists --- Source/Concurrency/MoverCheck.cs | 48 ++++++++---- Source/Concurrency/OwickiGries.cs | 19 +++-- Source/Concurrency/TypeCheck.cs | 159 ++++++++++++++++++++++++-------------- Source/Core/Absy.cs | 19 ----- 4 files changed, 145 insertions(+), 100 deletions(-) (limited to 'Source') diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index adfcc5c9..db2bfb23 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -9,23 +9,39 @@ namespace Microsoft.Boogie { public class MoverCheck { - public static MoverType GetMoverType(Ensures e, out int phaseNum) + public static MoverType GetMoverType(Ensures e, out int phaseNum, out int availableUptoPhaseNum) { - phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "atomic", int.MaxValue); - if (phaseNum != int.MaxValue) + if (FindAtomicAction(e.Attributes, "atomic", out phaseNum, out availableUptoPhaseNum)) return MoverType.Atomic; - phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "right", int.MaxValue); - if (phaseNum != int.MaxValue) + if (FindAtomicAction(e.Attributes, "right", out phaseNum, out availableUptoPhaseNum)) return MoverType.Right; - phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "left", int.MaxValue); - if (phaseNum != int.MaxValue) + if (FindAtomicAction(e.Attributes, "left", out phaseNum, out availableUptoPhaseNum)) return MoverType.Left; - phaseNum = QKeyValue.FindIntAttribute(e.Attributes, "both", int.MaxValue); - if (phaseNum != int.MaxValue) + 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; @@ -50,13 +66,16 @@ namespace Microsoft.Boogie Dictionary> pools = new Dictionary>(); foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values) { - foreach (int phaseNum in action.callerPhaseNums) + foreach (int phaseNum in moverTypeChecker.allPhaseNums) { - if (!pools.ContainsKey(phaseNum)) + if (action.phaseNum < phaseNum && phaseNum <= action.availableUptoPhaseNum) { - pools[phaseNum] = new HashSet(); + if (!pools.ContainsKey(phaseNum)) + { + pools[phaseNum] = new HashSet(); + } + pools[phaseNum].Add(action); } - pools[phaseNum].Add(action); } } @@ -457,6 +476,8 @@ 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()) { var domainName = linearTypeChecker.FindDomainName(v); @@ -464,6 +485,7 @@ namespace Microsoft.Boogie if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; domainNameToScope[domainName].Add(v); } + */ if (first != null) { foreach (Variable v in first.thatInParams) diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index b5d41b21..9de83635 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -14,7 +14,7 @@ namespace Microsoft.Boogie { MoverTypeChecker moverTypeChecker; public int phaseNum; - int enclosingProcPhaseNum; + Procedure enclosingProc; public Dictionary procMap; /* Original -> Duplicate */ public Dictionary absyMap; /* Duplicate -> Original */ public Dictionary blockMap; /* Original -> Duplicate */ @@ -22,7 +22,7 @@ namespace Microsoft.Boogie { this.moverTypeChecker = moverTypeChecker; this.phaseNum = phaseNum; - this.enclosingProcPhaseNum = int.MaxValue; + this.enclosingProc = null; this.procMap = new Dictionary(); this.absyMap = new Dictionary(); this.blockMap = new Dictionary(); @@ -30,6 +30,11 @@ namespace Microsoft.Boogie private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List newCmds) { + int enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(enclosingProc); + if (enclosingProcPhaseNum == int.MaxValue) + { + enclosingProcPhaseNum = moverTypeChecker.allPhaseNums.Max(); + } Procedure originalProc = originalCallCmd.Proc; if (phaseNum == enclosingProcPhaseNum && moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) { @@ -137,6 +142,7 @@ namespace Microsoft.Boogie public override Procedure VisitProcedure(Procedure node) { + enclosingProc = node; if (!QKeyValue.FindBoolAttribute(node.Attributes, "yields")) return node; if (!procMap.ContainsKey(node)) @@ -164,11 +170,7 @@ namespace Microsoft.Boogie private Variable dummyLocalVar; public override Implementation VisitImplementation(Implementation node) { - enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(node.Proc); - if (enclosingProcPhaseNum == int.MaxValue) - { - enclosingProcPhaseNum = moverTypeChecker.allPhaseNums.Max(); - } + enclosingProc = node.Proc; dummyLocalVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_dummy", Type.Bool)); Implementation impl = base.VisitImplementation(node); impl.LocVars.Add(dummyLocalVar); @@ -206,7 +208,8 @@ namespace Microsoft.Boogie Ensures ensures = base.VisitEnsures(node); if (node.Free) return ensures; - if (ensures.IsAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum)) + bool isAtomicSpecification = moverTypeChecker.procToActionInfo.ContainsKey(enclosingProc) && moverTypeChecker.procToActionInfo[enclosingProc].ensures == ensures; + if (isAtomicSpecification || !OwickiGries.FindPhaseNums(ensures.Attributes).Contains(phaseNum)) { ensures.Condition = Expr.True; ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes); diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 27a4e6a5..a8266e79 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -20,9 +20,10 @@ namespace Microsoft.Boogie public class ActionInfo { public Procedure proc; + public Ensures ensures; public MoverType moverType; public int phaseNum; - public HashSet callerPhaseNums; + public int availableUptoPhaseNum; public List thisGate; public CodeExpr thisAction; public List thisInParams; @@ -55,12 +56,14 @@ namespace Microsoft.Boogie get { return moverType == MoverType.Left || moverType == MoverType.Both; } } - public ActionInfo(Procedure proc, CodeExpr codeExpr, MoverType moverType, int phaseNum) + public ActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int phaseNum, int availableUptoPhaseNum) { + CodeExpr codeExpr = ensures.Condition as CodeExpr; this.proc = proc; + this.ensures = ensures; this.moverType = moverType; this.phaseNum = phaseNum; - this.callerPhaseNums = new HashSet(); + this.availableUptoPhaseNum = availableUptoPhaseNum; this.thisGate = new List(); this.thisAction = codeExpr; this.thisInParams = new List(); @@ -186,19 +189,17 @@ namespace Microsoft.Boogie else return int.MaxValue; } - public HashSet QedGlobalVariables() - { - return qedGlobalVariables; - } CheckingContext checkingContext; public int errorCount; - HashSet qedGlobalVariables; - int enclosingProcPhaseNum; + Dictionary qedGlobalVariables; + Procedure enclosingProc; public Dictionary procToActionInfo; public Program program; public HashSet allPhaseNums; bool inAtomicSpecification; + bool inSpecification; + int minPhaseNum; public void TypeCheck() { @@ -208,8 +209,8 @@ namespace Microsoft.Boogie if (proc == null) continue; foreach (Ensures e in proc.Ensures) { - int phaseNum; - MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum); + int phaseNum, availableUptoPhaseNum; + MoverType moverType = MoverCheck.GetMoverType(e, out phaseNum, out availableUptoPhaseNum); if (moverType == MoverType.Top) continue; CodeExpr codeExpr = e.Condition as CodeExpr; if (codeExpr == null) @@ -222,16 +223,16 @@ namespace Microsoft.Boogie Error(proc, "A procedure can have at most one atomic action"); continue; } - ActionInfo actionInfo = new ActionInfo(proc, codeExpr, moverType, phaseNum); - /* - * Removing this restriction based on the new failure preservation check - if (actionInfo.IsLeftMover && !actionInfo.isNonBlocking) + if (phaseNum >= availableUptoPhaseNum) { - Error(e, "A left mover must be non blocking"); + Error(proc, "Available at phase number should be less than available up to phase number"); continue; } - */ - procToActionInfo[proc] = actionInfo; + if (phaseNum != int.MaxValue) + { + allPhaseNums.Add(phaseNum); + } + procToActionInfo[proc] = new ActionInfo(proc, e, moverType, phaseNum, availableUptoPhaseNum); } } this.VisitProgram(program); @@ -242,12 +243,19 @@ namespace Microsoft.Boogie public MoverTypeChecker(Program program) { - this.qedGlobalVariables = new HashSet(); + this.qedGlobalVariables = new Dictionary(); foreach (var g in program.GlobalVariables()) { if (QKeyValue.FindBoolAttribute(g.Attributes, "qed")) { - this.qedGlobalVariables.Add(g); + this.qedGlobalVariables.Add(g, int.MaxValue); + g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes); + } + 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); } } @@ -256,36 +264,43 @@ namespace Microsoft.Boogie this.errorCount = 0; this.checkingContext = new CheckingContext(null); this.program = program; - this.enclosingProcPhaseNum = int.MaxValue; + this.enclosingProc = null; this.inAtomicSpecification = false; + this.inSpecification = false; + this.minPhaseNum = int.MaxValue; } public override Implementation VisitImplementation(Implementation node) { - enclosingProcPhaseNum = FindPhaseNumber(node.Proc); + this.enclosingProc = node.Proc; return base.VisitImplementation(node); } public override Procedure VisitProcedure(Procedure node) { - enclosingProcPhaseNum = FindPhaseNumber(node); - if (enclosingProcPhaseNum != int.MaxValue) - { - allPhaseNums.Add(enclosingProcPhaseNum); - } + this.enclosingProc = node; return base.VisitProcedure(node); } public override Cmd VisitCallCmd(CallCmd node) { if (!node.IsAsync) { + int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc); int calleePhaseNum = FindPhaseNumber(node.Proc); - if (enclosingProcPhaseNum > calleePhaseNum) + if (enclosingProcPhaseNum == int.MaxValue) { - procToActionInfo[node.Proc].callerPhaseNums.Add(enclosingProcPhaseNum); + } - else if (enclosingProcPhaseNum < calleePhaseNum || enclosingProcPhaseNum != int.MaxValue) + else if (calleePhaseNum == int.MaxValue) + { + Error(node, "An atomic procedure cannot call a non-atomic procedure"); + } + else if (enclosingProcPhaseNum <= calleePhaseNum) { Error(node, "The phase of the caller procedure must be greater than the phase of the callee"); } + else if (procToActionInfo[node.Proc].availableUptoPhaseNum < enclosingProcPhaseNum) + { + Error(node, "The callee is not available in the phase of the caller procedure"); + } } return base.VisitCallCmd(node); } @@ -298,7 +313,7 @@ namespace Microsoft.Boogie if (calleePhaseNum > maxCalleePhaseNum) maxCalleePhaseNum = calleePhaseNum; } - + int enclosingProcPhaseNum = FindPhaseNumber(enclosingProc); if (enclosingProcPhaseNum > maxCalleePhaseNum) { bool isLeftMover = true; @@ -308,24 +323,32 @@ namespace Microsoft.Boogie ActionInfo actionInfo = procToActionInfo[iter.Proc]; isLeftMover = isLeftMover && actionInfo.IsLeftMover; isRightMover = isRightMover && actionInfo.IsRightMover; - actionInfo.callerPhaseNums.Add(enclosingProcPhaseNum); } if (!isLeftMover && !isRightMover && node.CallCmds.Count > 1) { Error(node, "The procedures in the parallel call must be all right mover or all left mover"); } + return base.VisitParCallCmd(node); + } + else + { + return node; } - return node; } public override Expr VisitIdentifierExpr(IdentifierExpr node) { if (node.Decl is GlobalVariable) { - if (inAtomicSpecification && !qedGlobalVariables.Contains(node.Decl)) + if (qedGlobalVariables.ContainsKey(node.Decl) && qedGlobalVariables[node.Decl] < minPhaseNum) + { + minPhaseNum = qedGlobalVariables[node.Decl]; + } + + if (inAtomicSpecification && !qedGlobalVariables.ContainsKey(node.Decl)) { Error(node, "Cannot access non-qed global variable in atomic action"); } - else if (!inAtomicSpecification && qedGlobalVariables.Contains(node.Decl)) + else if (!inSpecification && qedGlobalVariables.ContainsKey(node.Decl)) { Error(node, "Cannot access qed global variable in ordinary code"); } @@ -334,47 +357,63 @@ namespace Microsoft.Boogie } public override Ensures VisitEnsures(Ensures ensures) { - if (ensures.IsAtomicSpecification) + minPhaseNum = int.MaxValue; + inAtomicSpecification = procToActionInfo.ContainsKey(enclosingProc) && procToActionInfo[enclosingProc].ensures == ensures; + inSpecification = true; + Ensures ret = base.VisitEnsures(ensures); + inSpecification = false; + if (inAtomicSpecification) { - inAtomicSpecification = true; - Ensures ret = base.VisitEnsures(ensures); + if (procToActionInfo[enclosingProc].availableUptoPhaseNum > minPhaseNum) + { + Error(ensures, "A variable being accessed is hidden before this action becomes unavailable"); + } inAtomicSpecification = false; - return ret; } - foreach (int phaseNum in OwickiGries.FindPhaseNums(ensures.Attributes)) + else { - allPhaseNums.Add(phaseNum); - if (phaseNum > enclosingProcPhaseNum) - { - Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure"); - } + CheckAndAddPhases(ensures, ensures.Attributes); } - return ensures; + return ret; } public override Requires VisitRequires(Requires requires) { - foreach (int phaseNum in OwickiGries.FindPhaseNums(requires.Attributes)) - { - allPhaseNums.Add(phaseNum); - if (phaseNum > enclosingProcPhaseNum) - { - Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure"); - } - } - return requires; + minPhaseNum = int.MaxValue; + inSpecification = true; + Requires ret = base.VisitRequires(requires); + inSpecification = false; + CheckAndAddPhases(requires, requires.Attributes); + return ret; } public override Cmd VisitAssertCmd(AssertCmd node) { - foreach (int phaseNum in OwickiGries.FindPhaseNums(node.Attributes)) + minPhaseNum = int.MaxValue; + inSpecification = true; + Cmd ret = base.VisitAssertCmd(node); + inSpecification = false; + CheckAndAddPhases(node, node.Attributes); + return ret; + } + + private void CheckAndAddPhases(Absy node, QKeyValue attributes) + { + foreach (int phaseNum in OwickiGries.FindPhaseNums(attributes)) { - allPhaseNums.Add(phaseNum); - if (phaseNum > enclosingProcPhaseNum) + if (phaseNum > FindPhaseNumber(enclosingProc)) { - Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure"); + Error(node, "The phase cannot be greater than the phase of enclosing procedure"); + } + else if (phaseNum > minPhaseNum) + { + Error(node, "A variable being accessed is hidden before this specification becomes unavailable"); + } + else + { + allPhaseNums.Add(phaseNum); } } - return node; } + public void Error(Absy node, string message) { checkingContext.Error(node, message); diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 60f76232..0bf55b17 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2364,26 +2364,7 @@ namespace Microsoft.Boogie { this.Condition.Resolve(rc); } - public bool IsAtomicSpecification - { - get - { - return - QKeyValue.FindIntAttribute(this.Attributes, "atomic", int.MaxValue) != int.MaxValue || - QKeyValue.FindIntAttribute(this.Attributes, "right", int.MaxValue) != int.MaxValue || - QKeyValue.FindIntAttribute(this.Attributes, "left", int.MaxValue) != int.MaxValue || - QKeyValue.FindIntAttribute(this.Attributes, "both", int.MaxValue) != int.MaxValue; - } - } - public override void Typecheck(TypecheckingContext tc) { - //Contract.Requires(tc != null); - - if (IsAtomicSpecification && !tc.Yields) - { - tc.Error(this, "atomic specification allowed only in a yielding procedure"); - return; - } this.Condition.Typecheck(tc); Contract.Assert(this.Condition.Type != null); // follows from postcondition of Expr.Typecheck if (!this.Condition.Type.Unify(Type.Bool)) { -- cgit v1.2.3