From 37fcf1a2d36dcbb70ccb52e7a925a52c4fce67d0 Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 7 Jan 2014 15:43:20 -0800 Subject: first cut of refinement checking --- Source/Concurrency/Concurrency.csproj | 1 - Source/Concurrency/MoverCheck.cs | 183 ++++++----- Source/Concurrency/OwickiGries.cs | 214 +++++++++---- Source/Concurrency/Program.cs | 15 +- Source/Concurrency/RefinementCheck.cs | 552 ---------------------------------- Source/Concurrency/TypeCheck.cs | 36 ++- Test/og/ticket.bpl | 5 +- 7 files changed, 288 insertions(+), 718 deletions(-) delete mode 100644 Source/Concurrency/RefinementCheck.cs diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj index 7d0febf5..8d7e3979 100644 --- a/Source/Concurrency/Concurrency.csproj +++ b/Source/Concurrency/Concurrency.csproj @@ -76,7 +76,6 @@ - diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 76a4b098..d1e5929d 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -141,12 +141,12 @@ namespace Microsoft.Boogie } } - class TransitionRelationComputation + public class TransitionRelationComputation { private Program program; - private ActionInfo first; - private ActionInfo second; - private Stack dfsStack; + private ActionInfo first; // corresponds to that* + private ActionInfo second; // corresponds to this* + private Stack path; private Expr transitionRelation; private int boundVariableCount; @@ -155,7 +155,7 @@ namespace Microsoft.Boogie this.program = program; this.first = null; this.second = second; - this.dfsStack = new Stack(); + this.path = new Stack(); this.transitionRelation = Expr.False; this.boundVariableCount = 0; } @@ -165,7 +165,7 @@ namespace Microsoft.Boogie this.program = program; this.first = first; this.second = second; - this.dfsStack = new Stack(); + this.path = new Stack(); this.transitionRelation = Expr.False; this.boundVariableCount = 0; } @@ -177,29 +177,16 @@ namespace Microsoft.Boogie public Expr Compute() { - Search(second.thatAction.Blocks[0], false); - Dictionary map = new Dictionary(); - List boundVars = new List(); - if (first != null) - { - foreach (Variable v in first.thisAction.LocVars) - { - BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)); - map[v] = new IdentifierExpr(Token.NoToken, bv); - boundVars.Add(bv); - } - } - foreach (Variable v in second.thatAction.LocVars) + List havocVars = new List(); + second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v))); + second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v))); + if (havocVars.Count > 0) { - BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)); - map[v] = new IdentifierExpr(Token.NoToken, bv); - boundVars.Add(bv); + HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars); + path.Push(havocCmd); } - Substitution subst = Substituter.SubstitutionFromHashtable(map); - if (boundVars.Count > 0) - return new ExistsExpr(Token.NoToken, boundVars, Substituter.Apply(subst, transitionRelation)); - else - return transitionRelation; + Search(second.thisAction.Blocks[0], false); + return transitionRelation; } private Expr CalculatePathCondition() @@ -212,60 +199,54 @@ namespace Microsoft.Boogie } if (first != null) { - foreach (Variable v in first.thisOutParams) + foreach (Variable v in first.thatOutParams) { var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); returnExpr = Expr.And(eqExpr, returnExpr); } } - foreach (Variable v in second.thatOutParams) + foreach (Variable v in second.thisOutParams) { var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); returnExpr = Expr.And(eqExpr, returnExpr); } - Block[] dfsStackAsArray = dfsStack.Reverse().ToArray(); - for (int i = dfsStackAsArray.Length - 1; i >= 0; i--) + foreach (Cmd cmd in path) { - Block b = dfsStackAsArray[i]; - for (int j = b.Cmds.Count - 1; j >= 0; j--) + if (cmd is AssumeCmd) { - Cmd cmd = b.Cmds[j]; - if (cmd is AssumeCmd) - { - AssumeCmd assumeCmd = cmd as AssumeCmd; - returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr); - } - else if (cmd is AssignCmd) - { - AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd; - Dictionary map = new Dictionary(); - for (int k = 0; k < assignCmd.Lhss.Count; k++) - { - map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k]; - } - Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary()); - Substitution oldSubst = Substituter.SubstitutionFromHashtable(map); - returnExpr = (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr); - } - else if (cmd is HavocCmd) + AssumeCmd assumeCmd = cmd as AssumeCmd; + returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr); + } + else if (cmd is AssignCmd) + { + AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd; + Dictionary map = new Dictionary(); + for (int k = 0; k < assignCmd.Lhss.Count; k++) { - HavocCmd havocCmd = cmd as HavocCmd; - List existVars = new List(); - Dictionary map = new Dictionary(); - foreach (IdentifierExpr ie in havocCmd.Vars) - { - BoundVariable bv = GetBoundVariable(ie.Decl.TypedIdent.Type); - map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv); - existVars.Add(bv); - } - Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary()); - Substitution oldSubst = Substituter.SubstitutionFromHashtable(map); - returnExpr = new ExistsExpr(Token.NoToken, existVars, (Expr) new MySubstituter(subst, oldSubst).Visit(returnExpr)); + map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k]; } - else + Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary()); + Substitution oldSubst = Substituter.SubstitutionFromHashtable(map); + returnExpr = (Expr)new MySubstituter(subst, oldSubst).Visit(returnExpr); + } + else if (cmd is HavocCmd) + { + HavocCmd havocCmd = cmd as HavocCmd; + List existVars = new List(); + Dictionary map = new Dictionary(); + foreach (IdentifierExpr ie in havocCmd.Vars) { - Debug.Assert(false); + BoundVariable bv = GetBoundVariable(ie.Decl.TypedIdent.Type); + map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv); + existVars.Add(bv); } + Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary()); + Substitution oldSubst = Substituter.SubstitutionFromHashtable(map); + returnExpr = new ExistsExpr(Token.NoToken, existVars, (Expr)new MySubstituter(subst, oldSubst).Visit(returnExpr)); + } + else + { + Debug.Assert(false); } } return returnExpr; @@ -273,7 +254,10 @@ namespace Microsoft.Boogie private void Search(Block b, bool inFirst) { - dfsStack.Push(b); + foreach (Cmd cmd in b.Cmds) + { + path.Push(cmd); + } if (b.TransferCmd is ReturnCmd) { if (first == null || inFirst) @@ -282,7 +266,15 @@ namespace Microsoft.Boogie } else { - Search(first.thisAction.Blocks[0], true); + List havocVars = new List(); + first.thatOutParams.ForEach(v => havocVars.Add(Expr.Ident(v))); + first.thatAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v))); + if (havocVars.Count > 0) + { + HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars); + path.Push(havocCmd); + } + Search(first.thatAction.Blocks[0], true); } } else @@ -293,7 +285,10 @@ namespace Microsoft.Boogie Search(target, inFirst); } } - dfsStack.Pop(); + foreach (Cmd cmd in b.Cmds) + { + path.Pop(); + } } } @@ -344,17 +339,17 @@ namespace Microsoft.Boogie if (domainName == null) continue; domainNameToScope[domainName].Add(v); } - foreach (Variable v in first.thisInParams) + foreach (Variable v in first.thatInParams) { var domainName = linearTypeChecker.FindDomainName(v); if (domainName == null) continue; domainNameToScope[domainName].Add(v); } - for (int i = 0; i < second.thatInParams.Count; i++) + foreach (Variable v in second.thisInParams) { - var domainName = linearTypeChecker.FindDomainName(second.thisInParams[i]); + var domainName = linearTypeChecker.FindDomainName(v); if (domainName == null) continue; - domainNameToScope[domainName].Add(second.thatInParams[i]); + domainNameToScope[domainName].Add(v); } foreach (string domainName in domainNameToScope.Keys) { @@ -371,16 +366,16 @@ namespace Microsoft.Boogie commutativityCheckerCache.Add(actionPair); List inputs = new List(); - inputs.AddRange(first.thisInParams); - inputs.AddRange(second.thatInParams); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); List outputs = new List(); - outputs.AddRange(first.thisOutParams); - outputs.AddRange(second.thatOutParams); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); List locals = new List(); - locals.AddRange(first.thisAction.LocVars); - locals.AddRange(second.thatAction.LocVars); - List firstBlocks = CloneBlocks(first.thisAction.Blocks); - List secondBlocks = CloneBlocks(second.thatAction.Blocks); + locals.AddRange(first.thatAction.LocVars); + locals.AddRange(second.thisAction.LocVars); + List firstBlocks = CloneBlocks(first.thatAction.Blocks); + List secondBlocks = CloneBlocks(second.thisAction.Blocks); foreach (Block b in firstBlocks) { if (b.TransferCmd is ReturnCmd) @@ -417,17 +412,17 @@ namespace Microsoft.Boogie gatePreservationCheckerCache.Add(actionPair); List inputs = new List(); - inputs.AddRange(first.thisInParams); - inputs.AddRange(second.thatInParams); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); List outputs = new List(); - outputs.AddRange(first.thisOutParams); - outputs.AddRange(second.thatOutParams); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); List locals = new List(); - locals.AddRange(second.thatAction.LocVars); - List secondBlocks = CloneBlocks(second.thatAction.Blocks); + locals.AddRange(second.thisAction.LocVars); + List secondBlocks = CloneBlocks(second.thisAction.Blocks); List requires = DisjointnessRequires(program, first, second); List ensures = new List(); - foreach (AssertCmd assertCmd in first.thisGate) + foreach (AssertCmd assertCmd in first.thatGate) { requires.Add(new Requires(false, assertCmd.Expr)); ensures.Add(new Ensures(false, assertCmd.Expr)); @@ -450,18 +445,18 @@ namespace Microsoft.Boogie failurePreservationCheckerCache.Add(actionPair); List inputs = new List(); - inputs.AddRange(first.thisInParams); - inputs.AddRange(second.thatInParams); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); Expr transitionRelation = (new TransitionRelationComputation(program, second)).Compute(); Expr expr = Expr.True; - foreach (AssertCmd assertCmd in first.thisGate) + foreach (AssertCmd assertCmd in first.thatGate) { expr = Expr.And(assertCmd.Expr, expr); } List requires = DisjointnessRequires(program, first, second); requires.Add(new Requires(false, Expr.Not(expr))); - foreach (AssertCmd assertCmd in second.thatGate) + foreach (AssertCmd assertCmd in second.thisGate) { requires.Add(new Requires(false, assertCmd.Expr)); } @@ -475,7 +470,7 @@ namespace Microsoft.Boogie boundVars.Add(bv); map[v] = new IdentifierExpr(Token.NoToken, bv); } - foreach (Variable v in second.thatOutParams) + foreach (Variable v in second.thisOutParams) { { BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type)); @@ -488,7 +483,7 @@ namespace Microsoft.Boogie oldMap[v] = new IdentifierExpr(Token.NoToken, bv); } } - foreach (Variable v in second.thatAction.LocVars) + foreach (Variable v in second.thisAction.LocVars) { BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type)); boundVars.Add(bv); diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 414aac59..598a4510 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -13,10 +13,11 @@ namespace Microsoft.Boogie public class MyDuplicator : Duplicator { MoverTypeChecker moverTypeChecker; - int phaseNum; + public int phaseNum; int enclosingProcPhaseNum; public Dictionary procMap; /* Original -> Duplicate */ - public Dictionary absyMap; /* Original -> Duplicate */ + public Dictionary absyMap; /* Duplicate -> Original */ + public Dictionary blockMap; /* Original -> Duplicate */ public MyDuplicator(MoverTypeChecker moverTypeChecker, int phaseNum) { this.moverTypeChecker = moverTypeChecker; @@ -24,6 +25,7 @@ namespace Microsoft.Boogie this.enclosingProcPhaseNum = int.MaxValue; this.procMap = new Dictionary(); this.absyMap = new Dictionary(); + this.blockMap = new Dictionary(); } private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List newCmds) @@ -37,7 +39,6 @@ namespace Microsoft.Boogie { map[originalProc.InParams[i]] = callCmd.Ins[i]; } - Substitution subst = Substituter.SubstitutionFromHashtable(map); foreach (AssertCmd assertCmd in gate) { @@ -61,6 +62,7 @@ namespace Microsoft.Boogie for (int i = 0; i < parCallCmd.CallCmds.Count; i++) { ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds); + absyMap[parCallCmd.CallCmds[i]] = originalParCallCmd; } } else @@ -100,14 +102,15 @@ namespace Microsoft.Boogie public override YieldCmd VisitYieldCmd(YieldCmd node) { YieldCmd yieldCmd = base.VisitYieldCmd(node); - absyMap[node] = yieldCmd; + absyMap[yieldCmd] = node; return yieldCmd; } public override Block VisitBlock(Block node) { Block block = base.VisitBlock(node); - absyMap[node] = block; + blockMap[node] = block; + absyMap[block] = node; return block; } @@ -116,14 +119,14 @@ namespace Microsoft.Boogie CallCmd callCmd = (CallCmd) base.VisitCallCmd(node); callCmd.Proc = VisitProcedure(callCmd.Proc); callCmd.callee = callCmd.Proc.Name; - absyMap[node] = callCmd; + absyMap[callCmd] = node; return callCmd; } public override Cmd VisitParCallCmd(ParCallCmd node) { ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node); - absyMap[node] = parCallCmd; + absyMap[parCallCmd] = node; return parCallCmd; } @@ -152,6 +155,7 @@ namespace Microsoft.Boogie } return procMap[node]; } + public override Implementation VisitImplementation(Implementation node) { enclosingProcPhaseNum = moverTypeChecker.FindPhaseNumber(node.Proc); @@ -165,7 +169,7 @@ namespace Microsoft.Boogie List labelNames = new List(); foreach (Block x in gotoCmd.labelTargets) { - Block y = (Block)absyMap[x]; + Block y = (Block)blockMap[x]; labelTargets.Add(y); labelNames.Add(y.Label); } @@ -210,7 +214,9 @@ namespace Microsoft.Boogie public class OwickiGries { LinearTypeChecker linearTypeChecker; + MoverTypeChecker moverTypeChecker; Dictionary absyMap; + Dictionary reverseProcMap; int phaseNum; List decls; List globalMods; @@ -219,11 +225,17 @@ namespace Microsoft.Boogie List yieldCheckerImpls; Procedure yieldProc; - public OwickiGries(LinearTypeChecker linearTypeChecker, Dictionary absyMap, int phaseNum, List decls) + public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator, List decls) { this.linearTypeChecker = linearTypeChecker; - this.absyMap = absyMap; - this.phaseNum = phaseNum; + 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; Program program = linearTypeChecker.program; globalMods = new List(); @@ -273,6 +285,32 @@ namespace Microsoft.Boogie CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List()); yieldCallCmd.Proc = yieldProc; newCmds.Add(yieldCallCmd); + + if (pc != null) + { + Expr bb = OldEqualityExpr(ogOldGlobalMap); + + // assert pc ==> o_old == o && g_old == g; + newCmds.Add(new AssertCmd(Token.NoToken, Expr.Imp(Expr.Ident(pc), bb))); + + // assert (o_old == o && g_old == g) || beta(i, g_old, o, g); + AssertCmd betaAssertCmd = new AssertCmd(Token.NoToken, Expr.Or(bb, beta)); + newCmds.Add(betaAssertCmd); + + // 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 }); + List pcUpdateLHS = new List( + new AssignLhs[] { + new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), + new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)) + }); + List pcUpdateRHS = new List( + new Expr[] { + new NAryExpr(Token.NoToken, new IfThenElse(Token.NoToken), iteArgs), + Expr.Or(Expr.Ident(ok), beta) + }); + newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS)); + } } private Dictionary ComputeAvailableExprs(HashSet availableLinearVars, Dictionary domainNameToInputVar) @@ -311,13 +349,28 @@ namespace Microsoft.Boogie { lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); rhss.Add(new IdentifierExpr(Token.NoToken, g)); - } + } if (lhss.Count > 0) { newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); } } + Variable pc; + Variable ok; + Expr alpha; + Expr beta; + + private Expr OldEqualityExpr(Dictionary ogOldGlobalMap) + { + Expr bb = Expr.True; + foreach (Variable o in ogOldGlobalMap.Keys) + { + bb = Expr.Binary(BinaryOperator.Opcode.And, bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); + } + return bb; + } + private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) { AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); @@ -325,7 +378,13 @@ namespace Microsoft.Boogie if (globalMods.Count > 0) { newCmds.Add(new HavocCmd(Token.NoToken, globalMods)); + if (pc != null) + { + // assume pc || alpha(i, g); + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Or(Expr.Ident(pc), alpha))); + } } + Dictionary domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar); AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); @@ -370,13 +429,13 @@ namespace Microsoft.Boogie Dictionary map = new Dictionary(); foreach (Variable x in callCmd.Proc.InParams) { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true); + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true); inParams.Add(y); map[x] = new IdentifierExpr(Token.NoToken, y); } foreach (Variable x in callCmd.Proc.OutParams) { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), false); + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), false); outParams.Add(y); map[x] = new IdentifierExpr(Token.NoToken, y); } @@ -663,6 +722,50 @@ namespace Microsoft.Boogie ogOldGlobalMap[g] = l; impl.LocVars.Add(l); } + + Procedure originalProc = reverseProcMap[impl.Proc]; + if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) + { + 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++) + { + 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); + Expr betaExpr = new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo).Compute(); + beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); + Expr alphaExpr = Expr.True; + foreach (AssertCmd assertCmd in actionInfo.thisGate) + { + alphaExpr = Expr.And(alphaExpr, assertCmd.Expr); + } + 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; + } + } + } + Dictionary domainNameToInputVar = new Dictionary(); Dictionary domainNameToLocalVar = new Dictionary(); { @@ -780,19 +883,43 @@ namespace Microsoft.Boogie if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) { AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar); + if (pc != null) + { + newCmds.Add(new AssertCmd(Token.NoToken, Expr.Ident(ok))); + } } b.Cmds = newCmds; } foreach (Block header in yieldingHeaders) { + LocalVariable oldPc = null; + LocalVariable oldOk = null; + if (pc != null) + { + oldPc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", pc.Name, header.Label), Type.Bool)); + impl.LocVars.Add(oldPc); + oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool)); + impl.LocVars.Add(oldOk); + } Dictionary domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar); foreach (Block pred in header.Predecessors) { AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar); + 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 List(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) }))); + } AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); } List newCmds = new List(); + if (pc != null) + { + newCmds.Add(new AssertCmd(Token.NoToken, Expr.Eq(Expr.Ident(pc), Expr.Ident(oldPc)))); + newCmds.Add(new AssertCmd(Token.NoToken, Expr.Eq(Expr.Ident(ok), Expr.Ident(oldOk)))); + } foreach (string domainName in linearTypeChecker.linearDomains.Keys) { newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName]))); @@ -809,6 +936,13 @@ namespace Microsoft.Boogie // Add initial block List lhss = new List(); List rhss = new List(); + if (pc != null) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); + rhss.Add(Expr.False); + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))); + rhss.Add(Expr.False); + } Dictionary domainNameToExpr = new Dictionary(); foreach (var domainName in linearTypeChecker.linearDomains.Keys) { @@ -1018,13 +1152,6 @@ namespace Microsoft.Boogie return (QKeyValue.FindBoolAttribute(iter, "stable")) ? iter.Next : iter; } - public static QKeyValue RemovePhaseAttribute(QKeyValue iter) - { - if (iter == null) return null; - iter.Next = RemovePhaseAttribute(iter.Next); - return (QKeyValue.FindIntAttribute(iter, "phase", int.MaxValue) != int.MaxValue) ? iter.Next : iter; - } - public static QKeyValue RemoveQedAttribute(QKeyValue iter) { if (iter == null) return null; @@ -1045,10 +1172,13 @@ namespace Microsoft.Boogie return iter; } - public void Transform(List impls, List procs) + private void Transform(List impls, List procs) { foreach (var impl in impls) { + pc = null; + alpha = null; + beta = null; TransformImpl(impl); } foreach (var proc in procs) @@ -1068,28 +1198,6 @@ namespace Microsoft.Boogie decls.Add(proc); } AddYieldProcAndImpl(); - foreach (var proc in procs) - { - if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) - { - HashSet modifiedVars = new HashSet(); - proc.Modifies.Iter(x => modifiedVars.Add(x.Decl)); - foreach (GlobalVariable g in linearTypeChecker.program.GlobalVariables()) - { - if (modifiedVars.Contains(g)) continue; - proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g)); - } - proc.Attributes = RemoveYieldsAttribute(proc.Attributes); - proc.Attributes = RemoveStableAttribute(proc.Attributes); - } - decls.Add(proc); - } - foreach (var impl in impls) - { - impl.Attributes = RemoveYieldsAttribute(impl.Attributes); - impl.Attributes = RemoveStableAttribute(impl.Attributes); - decls.Add(impl); - } } public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) @@ -1108,8 +1216,9 @@ namespace Microsoft.Boogie procs.Add(duplicateProc); if (moverTypeChecker.procToActionInfo.ContainsKey(proc) && moverTypeChecker.procToActionInfo[proc].phaseNum < phaseNum) { - duplicateProc.Attributes = OwickiGries.RemoveYieldsAttribute(duplicateProc.Attributes); - program.GlobalVariables().Iter(x => duplicateProc.Modifies.Add(new IdentifierExpr(Token.NoToken, x))); + 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 = new Implementation(Token.NoToken, duplicateProc.Name, proc.TypeParameters, proc.InParams, proc.OutParams, new List(), action.Blocks); impl.Proc = duplicateProc; @@ -1128,13 +1237,16 @@ namespace Microsoft.Boogie Implementation duplicateImpl = duplicator.VisitImplementation(impl); impls.Add(duplicateImpl); } - Dictionary reverseAbsyMap = new Dictionary(); - foreach (Absy key in duplicator.absyMap.Keys) + OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator, decls); + ogTransform.Transform(impls, procs); + foreach (var proc in procs) { - reverseAbsyMap[duplicator.absyMap[key]] = key; + decls.Add(proc); + } + foreach (var impl in impls) + { + decls.Add(impl); } - OwickiGries ogTransform = new OwickiGries(linearTypeChecker, reverseAbsyMap, phaseNum, decls); - ogTransform.Transform(impls, procs); } } } diff --git a/Source/Concurrency/Program.cs b/Source/Concurrency/Program.cs index 7c2c0c74..45d538df 100644 --- a/Source/Concurrency/Program.cs +++ b/Source/Concurrency/Program.cs @@ -33,8 +33,21 @@ namespace Microsoft.Boogie List decls = new List(); OwickiGries.AddCheckers(linearTypeChecker, moverTypeChecker, decls); MoverCheck.AddCheckers(linearTypeChecker, moverTypeChecker, decls); - //RefinementCheck.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/RefinementCheck.cs b/Source/Concurrency/RefinementCheck.cs deleted file mode 100644 index bba7bd35..00000000 --- a/Source/Concurrency/RefinementCheck.cs +++ /dev/null @@ -1,552 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Boogie; -using Microsoft.Boogie.AbstractInterpretation; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics; -using System.Diagnostics.Contracts; - - -namespace Microsoft.Boogie -{ - using Bpl = Microsoft.Boogie; - class RefinementCheck - { - Program refinementCheckerProgram; - LinearTypeChecker linearTypeChecker; - MoverTypeChecker moverTypeChecker; - - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker) - { - RefinementCheck refinementChecking = new RefinementCheck(linearTypeChecker, moverTypeChecker); - foreach (Declaration decl in linearTypeChecker.program.TopLevelDeclarations) - { - if (decl is Implementation) - { - Implementation impl = decl as Implementation; - refinementChecking.createRefinementChecker(impl); - } - } - } - - private RefinementCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker) - { - this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; - this.refinementCheckerProgram = new Program(); - foreach (Declaration decl in linearTypeChecker.program.TopLevelDeclarations) - { - if (decl is TypeCtorDecl || decl is TypeSynonymDecl || decl is Constant || decl is Function || decl is Axiom) - this.refinementCheckerProgram.TopLevelDeclarations.Add(decl); - } - foreach (Variable v in linearTypeChecker.program.GlobalVariables()) - { - this.refinementCheckerProgram.TopLevelDeclarations.Add(v); - } - } - - private void createRefinementChecker(Implementation impl) - { - addRefinementCheckingAnnotations(impl); - refinementCheckerProgram.TopLevelDeclarations.Add(impl); - refinementCheckerProgram.TopLevelDeclarations.Add(impl.Proc); - } - - private Expr createNewAlpha(Implementation impl) - { - Expr result; - result = Expr.True; - foreach (AssertCmd aC in moverTypeChecker.procToActionInfo[impl.Proc].thisGate) - { - Expr aCExprClone = (Expr)aC.OrigExpr.Clone(); - result = Expr.Binary(BinaryOperator.Opcode.And, result, aCExprClone); - } - return result; - } - - private Expr createNewAlphaOfGOld(Implementation impl, List originalGVars, - Dictionary regularToOldGVar) - { - Expr result; - result = Expr.True; - foreach (AssertCmd aC in moverTypeChecker.procToActionInfo[impl.Proc].thisGate) - { - Expr aCExprClone = (Expr)aC.OrigExpr.Clone(); - result = Expr.Binary(BinaryOperator.Opcode.And, result, aCExprClone); - } - Dictionary map = new Dictionary(); - foreach (Variable v in originalGVars) - { - map[v] = Expr.Ident(regularToOldGVar[v]); - } - Substitution subst = Substituter.SubstitutionFromHashtable(map); - MySubstituter mySubst = new MySubstituter(subst, subst);// ST: Check with Shaz - result = (Expr)mySubst.Visit(result); - return result; - } - - - private HavocCmd createNewHavocGCmd() - { - List gList = new List(); - foreach (GlobalVariable g in refinementCheckerProgram.GlobalVariables()) - gList.Add(new IdentifierExpr(Token.NoToken, g)); - HavocCmd havocG = new HavocCmd(Token.NoToken, gList); - return havocG; - } - - private AssignCmd createNewAssignGOldGetsG(List originalGVars, Dictionary regularToOldGVar) - { - List lhss_g = new List(); - List rhss_g = new List(); - foreach (Variable g in originalGVars) - { - rhss_g.Add(new IdentifierExpr(Token.NoToken, g)); - lhss_g.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(regularToOldGVar[g]))); - } - - AssignCmd gOldGetsG = new AssignCmd(Token.NoToken, lhss_g, rhss_g); - return gOldGetsG; - } - - private AssignCmd createNewAssignOOldGetsO(Implementation impl, Dictionary regularToOldOVar) - { - List lhss = new List(); - List rhss = new List(); - foreach (Variable o in impl.OutParams) - { - rhss.Add(new IdentifierExpr(Token.NoToken, o)); - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(regularToOldOVar[o]))); - } - - // Implement command list that does o_old := o; - AssignCmd oOldGetsO = new AssignCmd(Token.NoToken, lhss, rhss); - return oOldGetsO; - } - - private AssertCmd createNewAssertGOldEqualsG(List originalGVars, Dictionary regularToOldGVar) - { - Expr gOldEqualsG = Expr.True; - foreach (Variable g in originalGVars) - { - Expr thisVarEqualsOldVar = Expr.Binary(BinaryOperator.Opcode.Eq, - new IdentifierExpr(Token.NoToken, g), - new IdentifierExpr(Token.NoToken, regularToOldGVar[g])); - gOldEqualsG = Expr.Binary(BinaryOperator.Opcode.And, gOldEqualsG, thisVarEqualsOldVar); - } - - AssertCmd AssertGOldEqualsGCmd = new AssertCmd(Token.NoToken, gOldEqualsG); - return AssertGOldEqualsGCmd; - } - - private Expr createNewGOldEqualsG(List originalGVars, Dictionary regularToOldGVar) - { - Expr gOldEqualsG = Expr.True; - foreach (Variable g in originalGVars) - { - Expr thisVarEqualsOldVar = Expr.Binary(BinaryOperator.Opcode.Eq, - new IdentifierExpr(Token.NoToken, g), - new IdentifierExpr(Token.NoToken, regularToOldGVar[g])); - gOldEqualsG = Expr.Binary(BinaryOperator.Opcode.And, gOldEqualsG, thisVarEqualsOldVar); - } - - return gOldEqualsG; - } - - private AssertCmd createNewAssertOOldEqualsO(Implementation impl, Dictionary regularToOldOVar) - { - Expr oOldEqualsO = Expr.True; - foreach (Variable o in impl.OutParams) - { - Expr thisOVarEqualsOldOVar = Expr.Binary(BinaryOperator.Opcode.Eq, - new IdentifierExpr(Token.NoToken, o), - new IdentifierExpr(Token.NoToken, regularToOldOVar[o])); - oOldEqualsO = Expr.Binary(BinaryOperator.Opcode.And, oOldEqualsO, thisOVarEqualsOldOVar); - } - - AssertCmd AssertOOldEqualsOCmd = new AssertCmd(Token.NoToken, oOldEqualsO); - return AssertOOldEqualsOCmd; - } - - private Expr createNewOOldEqualsO(Implementation impl, Dictionary regularToOldOVar) - { - Expr oOldEqualsO = Expr.True; - foreach (Variable o in impl.OutParams) - { - Expr thisOVarEqualsOldOVar = Expr.Binary(BinaryOperator.Opcode.Eq, - new IdentifierExpr(Token.NoToken, o), - new IdentifierExpr(Token.NoToken, regularToOldOVar[o])); - oOldEqualsO = Expr.Binary(BinaryOperator.Opcode.And, oOldEqualsO, thisOVarEqualsOldOVar); - } - - return oOldEqualsO; - } - - - private Expr createNewBetaOfOldOOldGoNg(Implementation impl, List originalGVars, - Dictionary regularToOldGVar, - Dictionary regularToOldOVar) - { - Expr betaOfOOldOGOldG = new TransitionRelationComputation(moverTypeChecker.program, - moverTypeChecker.procToActionInfo[impl.Proc], - regularToOldGVar, - regularToOldOVar).Compute(); - Dictionary map = new Dictionary(); - foreach (Variable v in originalGVars) - { - map[v] = Expr.Ident(regularToOldGVar[v]); - } - foreach (Variable o in impl.OutParams) - { - map[o] = Expr.Ident(regularToOldOVar[o]); - } - - Substitution always = Substituter.SubstitutionFromHashtable(new Dictionary()); - Substitution forold = Substituter.SubstitutionFromHashtable(map); - betaOfOOldOGOldG = Substituter.ApplyReplacingOldExprs(always, forold, betaOfOOldOGOldG); - return betaOfOOldOGOldG; - } - - private HavocCmd createNewHavocGnO(Implementation impl, List originalGVars) - { - HavocCmd resultCmd; - List varsList = new List(); - foreach (Variable gv in originalGVars) - { - varsList.Add(new IdentifierExpr(Token.NoToken, gv)); - } - foreach (Variable v in impl.OutParams) - { - varsList.Add(new IdentifierExpr(Token.NoToken, v)); - } - resultCmd = new HavocCmd(Token.NoToken, varsList); - return resultCmd; - } - - private void addRefinementCheckingAnnotations(Implementation impl) - { - // Create variables for pc, ok - LocalVariable pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pc", Bpl.Type.Bool)); - impl.LocVars.Add(pc); - LocalVariable pc_old = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pc_old", Bpl.Type.Bool)); - impl.LocVars.Add(pc_old); - LocalVariable ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "ok", Bpl.Type.Bool)); - impl.LocVars.Add(ok); - - - // Create variables for g_old, o_old - Dictionary regularToOldGVar = new Dictionary(); - Dictionary regularToOldOVar = new Dictionary(); - ActionInfo actionInfoForThisProc = moverTypeChecker.procToActionInfo[impl.Proc]; - - List originalGVars = new List(); - List _old_OriginalGVars = new List(); - - - foreach (GlobalVariable gv in refinementCheckerProgram.GlobalVariables()) - originalGVars.Add(gv); - - foreach (Variable v in refinementCheckerProgram.GlobalVariables()) //ST: Check that this is the right set of global vars - { - GlobalVariable gv = v as GlobalVariable; - LocalVariable v_old = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, gv.TypedIdent.Name + "_old", gv.TypedIdent.Type)); //gv.TypedIdent - impl.LocVars.Add(v_old); //ST: Ask Shaz whether to add v_old to proc, probably not. - _old_OriginalGVars.Add(v_old); - regularToOldGVar.Add(gv, v_old); - } - - // List originalOVars = new List(); - List _old_OriginalOVars = new List(); - - - //foreach (Variable v in impl.OutParams) - // originalOVars.Add(v); - - foreach (Variable o in impl.OutParams) //ST: Check that this is the right set of global vars - { - Variable o_old = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, o.TypedIdent.Name + "_old", o.TypedIdent.Type)); - - _old_OriginalOVars.Add(o_old); - regularToOldOVar.Add(o, o_old); - } - - - // AssertCmd AssertONGEqualOldONG = new AssertCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.And, oOldEqualsO, gOldEqualsG)); - - // Traverse CFG of impl, replace yield's in place. - foreach (Block b in impl.Blocks) - { - List newCmdList = new List(); - foreach (Cmd c in b.Cmds) - { - if (c is YieldCmd) - { - // Code to be inserted instead of yield - // - // assert !pc ==> \alpha(g_old); - // assert ok; - // if (o_old == o && g_old == g) { // IfCmd - // // Do nothing - // } else { - // assert !pc; - // pc := true; - // assert \beta(o_old, g_old, o, g); - // } - // havoc o, g; - // o_old := o; - // g_old := g; - - // Implementing the following instead: - - // assert !pc ==> \alpha(g_old); - // assert ok; - // bb := (o_old == o && g_old == g) - // assert !bb ==> !pc; - // pc := ite(!bb,true,pc); - // assert !bb ==> \beta(o_old, g_old, o, g); - // } - // havoc o, g; - // o_old := o; - // g_old := g; - - Expr notPcImpliesAlphaOfGoldExpr = Expr.Binary(BinaryOperator.Opcode.Imp, - Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, - Expr.Ident(pc)), - createNewAlphaOfGOld(impl, originalGVars, regularToOldGVar) - ); - AssertCmd notPcImpliesAlphaOfGOldCmd = new AssertCmd(Token.NoToken, notPcImpliesAlphaOfGoldExpr); - newCmdList.Add(notPcImpliesAlphaOfGOldCmd); - AssertCmd assertOkCmd = new AssertCmd(Token.NoToken, new IdentifierExpr(Token.NoToken, ok)); - newCmdList.Add(assertOkCmd); - - Expr bb = Expr.Binary(BinaryOperator.Opcode.And, - createNewOOldEqualsO(impl, regularToOldOVar), - createNewGOldEqualsG(originalGVars, regularToOldGVar)); - Expr notBB = Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, bb); - Expr notPC = Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, Expr.Ident(pc)); - AssertCmd assertNotBBImpliesNotPCCmd = new AssertCmd(Token.NoToken, Expr.Imp(notBB, notPC)); - newCmdList.Add(assertNotBBImpliesNotPCCmd); - - // pc := ite(!bb,true,pc); - List iteArgs = new List(); - iteArgs.Add(Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, bb)); - iteArgs.Add(Expr.True); - iteArgs.Add(Expr.Ident(pc)); - Expr pcNew = new NAryExpr(Token.NoToken, new IfThenElse(Token.NoToken), iteArgs); - List pcUpdateLHS = new List(); - pcUpdateLHS.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, pc))); - List pcUpdateRHS = new List(); - pcUpdateRHS.Add(pcNew); - AssignCmd pcGetsUpdated = new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS); - - // assert !bb ==> \beta(o_old, g_old, o, g); - Expr betaExpr = createNewBetaOfOldOOldGoNg(impl, originalGVars, regularToOldGVar, regularToOldOVar); - AssertCmd betaAssertCmd = new AssertCmd(Token.NoToken, Expr.Imp(Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, bb), - betaExpr)); - newCmdList.Add(betaAssertCmd); - - HavocCmd havocOnG = createNewHavocGnO(impl, originalGVars); - newCmdList.Add(havocOnG); - - if (originalGVars.Count > 0) - { - AssignCmd gOldGetsG = createNewAssignGOldGetsG(originalGVars, regularToOldGVar); - newCmdList.Add(gOldGetsG); - } - - if (impl.OutParams.Count > 0) - { - AssignCmd oOldGetsO = createNewAssignOOldGetsO(impl, regularToOldOVar); - newCmdList.Add(oOldGetsO); - } - } - else - { - newCmdList.Add((Cmd)c.Clone()); - } - } - b.Cmds = newCmdList; - } - } - - private sealed class MySubstituter : Duplicator - { - private readonly Substitution outsideOld; - private readonly Substitution insideOld; - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(insideOld != null); - } - - public MySubstituter(Substitution outsideOld, Substitution insideOld) - : base() - { - Contract.Requires(outsideOld != null && insideOld != null); - this.outsideOld = outsideOld; - this.insideOld = insideOld; - } - - private bool insideOldExpr = false; - - public override Expr VisitIdentifierExpr(IdentifierExpr node) - { - Contract.Ensures(Contract.Result() != null); - Expr e = null; - - if (insideOldExpr) - { - e = insideOld(node.Decl); - } - else - { - e = outsideOld(node.Decl); - } - return e == null ? base.VisitIdentifierExpr(node) : e; - } - - public override Expr VisitOldExpr(OldExpr node) - { - Contract.Ensures(Contract.Result() != null); - bool previouslyInOld = insideOldExpr; - insideOldExpr = true; - Expr tmp = (Expr)this.Visit(node.Expr); - OldExpr e = new OldExpr(node.tok, tmp); - insideOldExpr = previouslyInOld; - return e; - } - } - - class TransitionRelationComputation - { - private Program program; - private ActionInfo first; - private ActionInfo second; - private Stack dfsStack; - private Expr transitionRelation; - private Dictionary regularToOldGVar; - private Dictionary regularToOldOVar; - - public TransitionRelationComputation(Program program, ActionInfo second, Dictionary regularToOldGVar, Dictionary regularToOldOVar) - { - this.program = program; - this.first = null; - this.second = second; - this.regularToOldGVar = regularToOldGVar; - this.regularToOldOVar = regularToOldOVar; - this.dfsStack = new Stack(); - this.transitionRelation = Expr.False; - } - - public Expr Compute() - { - Search(second.thatAction.Blocks[0], false); - Dictionary map = new Dictionary(); - List boundVars = new List(); - if (first != null) - { - foreach (Variable v in first.thisAction.LocVars) - { - BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)); - map[v] = new IdentifierExpr(Token.NoToken, bv); - boundVars.Add(bv); - } - } - foreach (Variable v in second.thatAction.LocVars) - { - BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type)); - map[v] = new IdentifierExpr(Token.NoToken, bv); - boundVars.Add(bv); - } - Substitution subst = Substituter.SubstitutionFromHashtable(map); - if (boundVars.Count > 0) - return new ExistsExpr(Token.NoToken, boundVars, Substituter.Apply(subst, transitionRelation)); - else - return transitionRelation; - } - - private Expr CalculatePathCondition() - { - Expr returnExpr = Expr.True; - foreach (Variable v in program.GlobalVariables()) - { - var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); - returnExpr = Expr.And(eqExpr, returnExpr); - } - if (first != null) - { - foreach (Variable v in first.thisOutParams) - { - var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); - returnExpr = Expr.And(eqExpr, returnExpr); - } - } - foreach (Variable v in second.thatOutParams) - { - var eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, v), new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v))); - returnExpr = Expr.And(eqExpr, returnExpr); - } - Block[] dfsStackAsArray = dfsStack.Reverse().ToArray(); - for (int i = dfsStackAsArray.Length - 1; i >= 0; i--) - { - Block b = dfsStackAsArray[i]; - for (int j = b.Cmds.Count - 1; j >= 0; j--) - { - Cmd cmd = b.Cmds[j]; - if (cmd is AssumeCmd) - { - AssumeCmd assumeCmd = cmd as AssumeCmd; - returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr); - } - else if (cmd is AssignCmd) - { - AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd; - Dictionary map = new Dictionary(); - for (int k = 0; k < assignCmd.Lhss.Count; k++) - { - map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k]; - } - Substitution subst = Substituter.SubstitutionFromHashtable(new Dictionary()); - Substitution oldSubst = Substituter.SubstitutionFromHashtable(map); - returnExpr = (Expr)new MySubstituter(subst, oldSubst).Visit(returnExpr); - } - else - { - Debug.Assert(false); - } - } - } - return returnExpr; - } - - private void Search(Block b, bool inFirst) - { - dfsStack.Push(b); - if (b.TransferCmd is ReturnExprCmd) - { - if (first == null || inFirst) - { - transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition()); - } - else - { - Search(first.thisAction.Blocks[0], true); - } - } - else - { - GotoCmd gotoCmd = b.TransferCmd as GotoCmd; - foreach (Block target in gotoCmd.labelTargets) - { - Search(target, inFirst); - } - } - dfsStack.Pop(); - } - } - } -} diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 5affd182..f6d673ab 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -69,23 +69,23 @@ namespace Microsoft.Boogie foreach (Variable x in proc.InParams) { this.thisInParams.Add(x); - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true); + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes); this.thatInParams.Add(y); map[x] = new IdentifierExpr(Token.NoToken, y); } foreach (Variable x in proc.OutParams) { this.thisOutParams.Add(x); - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false); + Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes); this.thatOutParams.Add(y); map[x] = new IdentifierExpr(Token.NoToken, y); } - List otherLocVars = new List(); + List thatLocVars = new List(); foreach (Variable x in thisAction.LocVars) { Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false); map[x] = new IdentifierExpr(Token.NoToken, y); - otherLocVars.Add(y); + thatLocVars.Add(y); } Contract.Assume(proc.TypeParameters.Count == 0); Substitution subst = Substituter.SubstitutionFromHashtable(map); @@ -94,7 +94,7 @@ namespace Microsoft.Boogie thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd)); } Dictionary blockMap = new Dictionary(); - List otherBlocks = new List(); + List thatBlocks = new List(); foreach (Block block in thisAction.Blocks) { List otherCmds = new List(); @@ -102,12 +102,12 @@ namespace Microsoft.Boogie { otherCmds.Add(Substituter.Apply(subst, cmd)); } - Block otherBlock = new Block(); - otherBlock.Cmds = otherCmds; - otherBlock.Label = "that_" + block.Label; + Block thatBlock = new Block(); + thatBlock.Cmds = otherCmds; + thatBlock.Label = "that_" + block.Label; block.Label = "this_" + block.Label; - otherBlocks.Add(otherBlock); - blockMap[block] = otherBlock; + thatBlocks.Add(thatBlock); + blockMap[block] = thatBlock; if (block.TransferCmd is GotoCmd) { GotoCmd gotoCmd = block.TransferCmd as GotoCmd; @@ -125,17 +125,17 @@ namespace Microsoft.Boogie blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok); continue; } - List otherGotoCmdLabelTargets = new List(); - List otherGotoCmdLabelNames = new List(); + List thatGotoCmdLabelTargets = new List(); + List thatGotoCmdLabelNames = new List(); GotoCmd gotoCmd = block.TransferCmd as GotoCmd; foreach (Block target in gotoCmd.labelTargets) { - otherGotoCmdLabelTargets.Add(blockMap[target]); - otherGotoCmdLabelNames.Add(blockMap[target].Label); + thatGotoCmdLabelTargets.Add(blockMap[target]); + thatGotoCmdLabelNames.Add(blockMap[target].Label); } - blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets); + blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, thatGotoCmdLabelNames, thatGotoCmdLabelTargets); } - this.thatAction = new CodeExpr(otherLocVars, otherBlocks); + this.thatAction = new CodeExpr(thatLocVars, thatBlocks); } } @@ -220,6 +220,10 @@ namespace Microsoft.Boogie public override Procedure VisitProcedure(Procedure node) { enclosingProcPhaseNum = FindPhaseNumber(node); + if (enclosingProcPhaseNum != int.MaxValue) + { + assertionPhaseNums.Add(enclosingProcPhaseNum); + } return base.VisitProcedure(node); } public override Cmd VisitCallCmd(CallCmd node) diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index a734c15e..0e64f6b2 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -72,9 +72,9 @@ ensures {:phase 2} tid != nil && Inv2(T, s, cs); ensures {:right 2} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil; cs := tid; return true; }|; { var m: int; - tid := tid'; par Yield1() | Yield2(); + tid := tid'; call tid, m := GetTicketAbstract(tid); par Yield1(); call tid := WaitAndEnter(tid, m); @@ -86,9 +86,8 @@ requires {:phase 1} Inv1(T, t); ensures {:phase 1} Inv1(T, t); ensures {:right 1} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|; { - tid := tid'; - par Yield1(); + tid := tid'; call tid, m := GetTicket(tid); par Yield1(); } -- cgit v1.2.3