diff options
| -rw-r--r-- | Source/Concurrency/MoverCheck.cs | 1319 | ||||
| -rw-r--r-- | Source/Concurrency/OwickiGries.cs | 2412 | ||||
| -rw-r--r-- | Source/Concurrency/TypeCheck.cs | 151 | ||||
| -rw-r--r-- | Test/civl/bar.bpl.expect | 26 | ||||
| -rw-r--r-- | Test/civl/foo.bpl.expect | 16 | ||||
| -rw-r--r-- | Test/civl/parallel1.bpl.expect | 16 | ||||
| -rw-r--r-- | Test/civl/t1.bpl.expect | 18 |
7 files changed, 2001 insertions, 1957 deletions
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index ed069d5d..7c6d4ac4 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -1,648 +1,673 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.Diagnostics;
-
-namespace Microsoft.Boogie
-{
- public class MoverCheck
- {
- LinearTypeChecker linearTypeChecker;
- MoverTypeChecker moverTypeChecker;
- List<Declaration> decls;
- HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache;
- HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache;
- HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache;
- private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
- {
- this.linearTypeChecker = linearTypeChecker;
- this.moverTypeChecker = moverTypeChecker;
- this.decls = decls;
- this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
- this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
- this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>();
- }
-
- public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
- {
- if (moverTypeChecker.procToActionInfo.Count == 0)
- return;
-
- List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
- sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });
- List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern));
- sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });
-
- Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();
- int indexIntoSortedByCreatedLayerNum = 0;
- int indexIntoSortedByAvailableUptoLayerNum = 0;
- HashSet<AtomicActionInfo> currPool = new HashSet<AtomicActionInfo>();
- while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)
- {
- var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum;
- pools[currLayerNum] = new HashSet<AtomicActionInfo>(currPool);
- while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)
- {
- var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo;
- if (actionInfo.createdAtLayerNum > currLayerNum) break;
- pools[currLayerNum].Add(actionInfo);
- indexIntoSortedByCreatedLayerNum++;
- }
- while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count)
- {
- var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo;
- if (actionInfo.availableUptoLayerNum > currLayerNum) break;
- pools[currLayerNum].Remove(actionInfo);
- indexIntoSortedByAvailableUptoLayerNum++;
- }
- currPool = pools[currLayerNum];
- }
-
- Program program = moverTypeChecker.program;
- MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);
- foreach (int layerNum in pools.Keys)
- {
- foreach (AtomicActionInfo first in pools[layerNum])
- {
- Debug.Assert(first.moverType != MoverType.Top);
- if (first.moverType == MoverType.Atomic)
- continue;
- foreach (AtomicActionInfo second in pools[layerNum])
- {
- if (first.IsRightMover)
- {
- moverChecking.CreateCommutativityChecker(program, first, second);
- moverChecking.CreateGatePreservationChecker(program, second, first);
- }
- if (first.IsLeftMover)
- {
- moverChecking.CreateCommutativityChecker(program, second, first);
- moverChecking.CreateGatePreservationChecker(program, first, second);
- moverChecking.CreateFailurePreservationChecker(program, second, first);
- }
- }
- }
- }
- foreach (AtomicActionInfo atomicActionInfo in sortedByCreatedLayerNum)
- {
- if (atomicActionInfo.IsLeftMover && atomicActionInfo.hasAssumeCmd)
- {
- moverChecking.CreateNonBlockingChecker(program, atomicActionInfo);
- }
- }
- }
-
- public sealed class MyDuplicator : Duplicator
- {
- public override Expr VisitIdentifierExpr(IdentifierExpr node)
- {
- IdentifierExpr ret = (IdentifierExpr) base.VisitIdentifierExpr(node);
- if (ret.Decl is GlobalVariable)
- {
- return new OldExpr(Token.NoToken, ret);
- }
- else
- {
- return ret;
- }
- }
- }
-
- public class TransitionRelationComputation
- {
- private Program program;
- private AtomicActionInfo first; // corresponds to that*
- private AtomicActionInfo second; // corresponds to this*
- private Stack<Cmd> cmdStack;
- private List<PathInfo> paths;
- private HashSet<Variable> frame;
- private HashSet<Variable> postExistVars;
-
- public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)
- {
- this.postExistVars = postExistVars;
- this.frame = frame;
- TransitionRelationComputationHelper(program, null, second);
- }
-
- public TransitionRelationComputation(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars)
- {
- this.postExistVars = postExistVars;
- this.frame = frame;
- TransitionRelationComputationHelper(program, first, second);
- }
-
- private void TransitionRelationComputationHelper(Program program, AtomicActionInfo first, AtomicActionInfo second)
- {
- this.program = program;
- this.first = first;
- this.second = second;
- this.cmdStack = new Stack<Cmd>();
- this.paths = new List<PathInfo>();
- List<IdentifierExpr> havocVars = new List<IdentifierExpr>();
- this.second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v)));
- this.second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v)));
- if (havocVars.Count > 0)
- {
- HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars);
- cmdStack.Push(havocCmd);
- }
- Search(this.second.thisAction.Blocks[0], false);
- }
-
- private void Substitute(Dictionary<Variable, Expr> map, ref List<Expr> pathExprs, ref Dictionary<Variable, Expr> varToExpr)
- {
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- List<Expr> oldPathExprs = pathExprs;
- pathExprs = new List<Expr>();
- foreach (Expr pathExpr in oldPathExprs)
- {
- pathExprs.Add(Substituter.Apply(subst, pathExpr));
- }
- Dictionary<Variable, Expr> oldVarToExpr = varToExpr;
- varToExpr = new Dictionary<Variable, Expr>();
- foreach (Variable v in oldVarToExpr.Keys)
- {
- varToExpr[v] = Substituter.Apply(subst, oldVarToExpr[v]);
- }
- }
-
- struct PathInfo
- {
- public HashSet<Variable> existsVars;
- public Dictionary<Variable, Expr> varToExpr;
- public List<Expr> pathExprs;
-
- public PathInfo(HashSet<Variable> existsVars, Dictionary<Variable, Expr> varToExpr, List<Expr> pathExprs)
- {
- this.existsVars = existsVars;
- this.varToExpr = varToExpr;
- this.pathExprs = pathExprs;
- }
- }
-
- private void FlattenAnd(Expr x, List<Expr> xs)
- {
- NAryExpr naryExpr = x as NAryExpr;
- if (naryExpr != null && naryExpr.Fun.FunctionName == "&&")
- {
- FlattenAnd(naryExpr.Args[0], xs);
- FlattenAnd(naryExpr.Args[1], xs);
- }
- else
- {
- xs.Add(x);
- }
- }
-
- private void AddPath()
- {
- HashSet<Variable> existsVars = new HashSet<Variable>();
- Dictionary<Variable, Expr> varToExpr = new Dictionary<Variable, Expr>();
- foreach (Variable v in frame)
- {
- varToExpr[v] = Expr.Ident(v);
- }
- if (first != null)
- {
- foreach (Variable v in first.thatOutParams)
- {
- varToExpr[v] = Expr.Ident(v);
- }
- }
- foreach (Variable v in second.thisOutParams)
- {
- varToExpr[v] = Expr.Ident(v);
- }
- List<Expr> pathExprs = new List<Expr>();
- int boundVariableCount = 0;
- foreach (Cmd cmd in cmdStack)
- {
- if (cmd is AssumeCmd)
- {
- AssumeCmd assumeCmd = cmd as AssumeCmd;
- FlattenAnd(assumeCmd.Expr, pathExprs);
- }
- else if (cmd is AssignCmd)
- {
- AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd;
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- for (int k = 0; k < assignCmd.Lhss.Count; k++)
- {
- map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];
- }
- Substitute(map, ref pathExprs, ref varToExpr);
- }
- else if (cmd is HavocCmd)
- {
- HavocCmd havocCmd = cmd as HavocCmd;
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- foreach (IdentifierExpr ie in havocCmd.Vars)
- {
- BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, ie.Decl.TypedIdent.Type));
- map[ie.Decl] = Expr.Ident(bv);
- existsVars.Add(bv);
- }
- Substitute(map, ref pathExprs, ref varToExpr);
- }
- else
- {
- Debug.Assert(false);
- }
- }
- paths.Add(new PathInfo(existsVars, varToExpr, pathExprs));
- }
-
- private Expr CalculatePathCondition(PathInfo path)
- {
- Expr returnExpr = Expr.True;
-
- HashSet<Variable> existsVars = path.existsVars;
- Dictionary<Variable, Expr> existsMap = new Dictionary<Variable, Expr>();
-
- Dictionary<Variable, Expr> varToExpr = path.varToExpr;
- foreach (Variable v in varToExpr.Keys)
- {
- if (postExistVars.Contains(v)) continue;
- IdentifierExpr ie = varToExpr[v] as IdentifierExpr;
- if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl))
- {
- existsMap[ie.Decl] = Expr.Ident(v);
- existsVars.Remove(ie.Decl);
- }
- else
- {
- returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v])));
- returnExpr.Type = Type.Bool;
- }
- }
-
- List<Expr> pathExprs = new List<Expr>();
- path.pathExprs.ForEach(x => pathExprs.Add((new MyDuplicator()).VisitExpr(x)));
- foreach (Expr x in pathExprs)
- {
- Variable boundVar;
- Expr boundVarExpr;
- if (InferSubstitution(x, out boundVar, out boundVarExpr) && existsVars.Contains(boundVar))
- {
- existsMap[boundVar] = boundVarExpr;
- existsVars.Remove(boundVar);
- }
- else
- {
- returnExpr = Expr.And(returnExpr, x);
- returnExpr.Type = Type.Bool;
- }
- }
-
- returnExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), returnExpr);
- if (existsVars.Count > 0)
- {
- returnExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), returnExpr);
- }
- return returnExpr;
- }
-
- bool InferSubstitution(Expr x, out Variable var, out Expr expr)
- {
- var = null;
- expr = null;
- NAryExpr naryExpr = x as NAryExpr;
- if (naryExpr == null || naryExpr.Fun.FunctionName != "==")
- {
- return false;
- }
- IdentifierExpr arg0 = naryExpr.Args[0] as IdentifierExpr;
- if (arg0 != null && arg0.Decl is BoundVariable)
- {
- var = arg0.Decl;
- expr = naryExpr.Args[1];
- return true;
- }
- IdentifierExpr arg1 = naryExpr.Args[1] as IdentifierExpr;
- if (arg1 != null && arg1.Decl is BoundVariable)
- {
- var = arg1.Decl;
- expr = naryExpr.Args[0];
- return true;
- }
- return false;
- }
-
- public Expr TransitionRelationCompute()
- {
- Expr transitionRelation = Expr.False;
- foreach (PathInfo path in paths)
- {
- transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition(path));
- }
- ResolutionContext rc = new ResolutionContext(null);
- rc.StateMode = ResolutionContext.State.Two;
- transitionRelation.Resolve(rc);
- transitionRelation.Typecheck(new TypecheckingContext(null));
- return transitionRelation;
- }
-
- private void Search(Block b, bool inFirst)
- {
- int pathSizeAtEntry = cmdStack.Count;
- foreach (Cmd cmd in b.Cmds)
- {
- cmdStack.Push(cmd);
- }
- if (b.TransferCmd is ReturnCmd)
- {
- if (first == null || inFirst)
- {
- AddPath();
- }
- else
- {
- List<IdentifierExpr> havocVars = new List<IdentifierExpr>();
- 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);
- cmdStack.Push(havocCmd);
- }
- Search(first.thatAction.Blocks[0], true);
- }
- }
- else
- {
- GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- Search(target, inFirst);
- }
- }
- Debug.Assert(cmdStack.Count >= pathSizeAtEntry);
- while (cmdStack.Count > pathSizeAtEntry)
- {
- cmdStack.Pop();
- }
- }
- }
-
- private static List<Block> CloneBlocks(List<Block> blocks)
- {
- Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
- List<Block> otherBlocks = new List<Block>();
- foreach (Block block in blocks)
- {
- List<Cmd> otherCmds = new List<Cmd>();
- foreach (Cmd cmd in block.Cmds)
- {
- otherCmds.Add(cmd);
- }
- Block otherBlock = new Block();
- otherBlock.Cmds = otherCmds;
- otherBlock.Label = block.Label;
- otherBlocks.Add(otherBlock);
- blockMap[block] = otherBlock;
- }
- foreach (Block block in blocks)
- {
- if (block.TransferCmd is ReturnCmd) continue;
- List<Block> otherGotoCmdLabelTargets = new List<Block>();
- List<string> otherGotoCmdLabelNames = new List<string>();
- GotoCmd gotoCmd = block.TransferCmd as GotoCmd;
- foreach (Block target in gotoCmd.labelTargets)
- {
- otherGotoCmdLabelTargets.Add(blockMap[target]);
- otherGotoCmdLabelNames.Add(blockMap[target].Label);
- }
- blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets);
- }
- return otherBlocks;
- }
-
- private List<Requires> DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame)
- {
- List<Requires> requires = new List<Requires>();
- Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- domainNameToScope[domainName] = new HashSet<Variable>();
- }
- 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)
- {
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- domainNameToScope[domainName].Add(v);
- }
- }
- foreach (Variable v in second.thisInParams)
- {
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- domainNameToScope[domainName].Add(v);
- }
- foreach (string domainName in domainNameToScope.Keys)
- {
- requires.Add(new Requires(false, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));
- }
- return requires;
- }
-
- 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<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
- if (commutativityCheckerCache.Contains(actionPair))
- return;
- commutativityCheckerCache.Add(actionPair);
-
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(first.thatInParams);
- inputs.AddRange(second.thisInParams);
- List<Variable> outputs = new List<Variable>();
- outputs.AddRange(first.thatOutParams);
- outputs.AddRange(second.thisOutParams);
- List<Variable> locals = new List<Variable>();
- locals.AddRange(first.thatAction.LocVars);
- locals.AddRange(second.thisAction.LocVars);
- List<Block> firstBlocks = CloneBlocks(first.thatAction.Blocks);
- List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
- foreach (Block b in firstBlocks)
- {
- if (b.TransferCmd is ReturnCmd)
- {
- List<Block> bs = new List<Block>();
- bs.Add(secondBlocks[0]);
- List<string> ls = new List<string>();
- ls.Add(secondBlocks[0].Label);
- b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs);
- }
- }
- List<Block> blocks = new List<Block>();
- blocks.AddRange(firstBlocks);
- blocks.AddRange(secondBlocks);
- HashSet<Variable> frame = new HashSet<Variable>();
- frame.UnionWith(first.gateUsedGlobalVars);
- frame.UnionWith(first.actionUsedGlobalVars);
- frame.UnionWith(second.gateUsedGlobalVars);
- frame.UnionWith(second.actionUsedGlobalVars);
- List<Requires> requires = DisjointnessRequires(program, first, second, frame);
- foreach (AssertCmd assertCmd in first.thatGate)
- requires.Add(new Requires(false, assertCmd.Expr));
- foreach (AssertCmd assertCmd in second.thisGate)
- requires.Add(new Requires(false, assertCmd.Expr));
- List<Ensures> ensures = new List<Ensures>();
- Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet<Variable>())).TransitionRelationCompute();
- Ensures ensureCheck = new Ensures(false, transitionRelation);
- ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);
- ensures.Add(ensureCheck);
- string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);
- List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
- moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);
- impl.Proc = proc;
- this.decls.Add(impl);
- this.decls.Add(proc);
- }
-
- private void CreateGatePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)
- {
- if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
- return;
- Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
- if (gatePreservationCheckerCache.Contains(actionPair))
- return;
- gatePreservationCheckerCache.Add(actionPair);
-
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(first.thatInParams);
- inputs.AddRange(second.thisInParams);
- List<Variable> outputs = new List<Variable>();
- outputs.AddRange(first.thatOutParams);
- outputs.AddRange(second.thisOutParams);
- List<Variable> locals = new List<Variable>();
- locals.AddRange(second.thisAction.LocVars);
- List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
- HashSet<Variable> frame = new HashSet<Variable>();
- frame.UnionWith(first.gateUsedGlobalVars);
- frame.UnionWith(second.gateUsedGlobalVars);
- frame.UnionWith(second.actionUsedGlobalVars);
- List<Requires> requires = DisjointnessRequires(program, first, second, frame);
- List<Ensures> ensures = new List<Ensures>();
- foreach (AssertCmd assertCmd in first.thatGate)
- {
- requires.Add(new Requires(false, assertCmd.Expr));
- Ensures ensureCheck = new Ensures(assertCmd.tok, false, assertCmd.Expr, null);
- ensureCheck.ErrorData = string.Format("Gate not preserved by {0}", second.proc.Name);
- ensures.Add(ensureCheck);
- }
- foreach (AssertCmd assertCmd in second.thisGate)
- requires.Add(new Requires(false, assertCmd.Expr));
- string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
- List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
- moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
- impl.Proc = proc;
- this.decls.Add(impl);
- this.decls.Add(proc);
- }
-
- private void CreateFailurePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second)
- {
- if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)
- return;
- Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second);
- if (failurePreservationCheckerCache.Contains(actionPair))
- return;
- failurePreservationCheckerCache.Add(actionPair);
-
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(first.thatInParams);
- inputs.AddRange(second.thisInParams);
- List<Variable> outputs = new List<Variable>();
- outputs.AddRange(first.thatOutParams);
- outputs.AddRange(second.thisOutParams);
- List<Variable> locals = new List<Variable>();
- locals.AddRange(second.thisAction.LocVars);
- List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);
- HashSet<Variable> frame = new HashSet<Variable>();
- frame.UnionWith(first.gateUsedGlobalVars);
- frame.UnionWith(second.gateUsedGlobalVars);
- frame.UnionWith(second.actionUsedGlobalVars);
- List<Requires> requires = DisjointnessRequires(program, first, second, frame);
- Expr gateExpr = Expr.True;
- foreach (AssertCmd assertCmd in first.thatGate)
- {
- gateExpr = Expr.And(gateExpr, assertCmd.Expr);
- gateExpr.Type = Type.Bool;
- }
- gateExpr = Expr.Not(gateExpr);
- gateExpr.Type = Type.Bool;
- requires.Add(new Requires(false, gateExpr));
- List<Ensures> ensures = new List<Ensures>();
- Ensures ensureCheck = new Ensures(false, gateExpr);
- ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);
- ensures.Add(ensureCheck);
- foreach (AssertCmd assertCmd in second.thisGate)
- requires.Add(new Requires(false, assertCmd.Expr));
- string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);
- List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
- moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);
- impl.Proc = proc;
- this.decls.Add(impl);
- this.decls.Add(proc);
- }
-
- private void CreateNonBlockingChecker(Program program, AtomicActionInfo second)
- {
- List<Variable> inputs = new List<Variable>();
- inputs.AddRange(second.thisInParams);
-
- HashSet<Variable> frame = new HashSet<Variable>();
- frame.UnionWith(second.gateUsedGlobalVars);
- frame.UnionWith(second.actionUsedGlobalVars);
- List<Requires> requires = DisjointnessRequires(program, null, second, frame);
- foreach (AssertCmd assertCmd in second.thisGate)
- {
- requires.Add(new Requires(false, assertCmd.Expr));
- }
- HashSet<Variable> postExistVars = new HashSet<Variable>();
- postExistVars.UnionWith(frame);
- postExistVars.UnionWith(second.thisOutParams);
- Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute();
- List<Ensures> ensures = new List<Ensures>();
- Ensures ensureCheck = new Ensures(false, ensuresExpr);
- ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name);
- ensures.Add(ensureCheck);
-
- List<Block> blocks = new List<Block>();
- blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));
- string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);
- List<IdentifierExpr> globalVars = new List<IdentifierExpr>();
- moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));
- Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);
- Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
- impl.Proc = proc;
- this.decls.Add(impl);
- this.decls.Add(proc);
- }
- }
+using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; +using System.Diagnostics; + +namespace Microsoft.Boogie +{ + public class MoverCheck + { + LinearTypeChecker linearTypeChecker; + MoverTypeChecker moverTypeChecker; + List<Declaration> decls; + HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> commutativityCheckerCache; + HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> gatePreservationCheckerCache; + HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>> failurePreservationCheckerCache; + private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + { + this.linearTypeChecker = linearTypeChecker; + this.moverTypeChecker = moverTypeChecker; + this.decls = decls; + this.commutativityCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); + this.gatePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); + this.failurePreservationCheckerCache = new HashSet<Tuple<AtomicActionInfo, AtomicActionInfo>>(); + } + + public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + { + if (moverTypeChecker.procToActionInfo.Count == 0) + return; + + List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; }); + List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo && !x.isExtern)); + sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; }); + + Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>(); + int indexIntoSortedByCreatedLayerNum = 0; + int indexIntoSortedByAvailableUptoLayerNum = 0; + HashSet<AtomicActionInfo> currPool = new HashSet<AtomicActionInfo>(); + while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count) + { + var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum; + pools[currLayerNum] = new HashSet<AtomicActionInfo>(currPool); + while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count) + { + var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo; + if (actionInfo.createdAtLayerNum > currLayerNum) break; + pools[currLayerNum].Add(actionInfo); + indexIntoSortedByCreatedLayerNum++; + } + while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count) + { + var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo; + if (actionInfo.availableUptoLayerNum > currLayerNum) break; + pools[currLayerNum].Remove(actionInfo); + indexIntoSortedByAvailableUptoLayerNum++; + } + currPool = pools[currLayerNum]; + } + + Program program = moverTypeChecker.program; + MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls); + foreach (int layerNum in pools.Keys) + { + foreach (AtomicActionInfo first in pools[layerNum]) + { + Debug.Assert(first.moverType != MoverType.Top); + if (first.moverType == MoverType.Atomic) + continue; + foreach (AtomicActionInfo second in pools[layerNum]) + { + if (first.IsRightMover) + { + moverChecking.CreateCommutativityChecker(program, first, second); + moverChecking.CreateGatePreservationChecker(program, second, first); + } + if (first.IsLeftMover) + { + moverChecking.CreateCommutativityChecker(program, second, first); + moverChecking.CreateGatePreservationChecker(program, first, second); + moverChecking.CreateFailurePreservationChecker(program, second, first); + } + } + } + } + foreach (AtomicActionInfo atomicActionInfo in sortedByCreatedLayerNum) + { + if (atomicActionInfo.IsLeftMover && atomicActionInfo.hasAssumeCmd) + { + moverChecking.CreateNonBlockingChecker(program, atomicActionInfo); + } + } + } + + public sealed class MyDuplicator : Duplicator + { + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + IdentifierExpr ret = (IdentifierExpr) base.VisitIdentifierExpr(node); + if (ret.Decl is GlobalVariable) + { + return new OldExpr(Token.NoToken, ret); + } + else + { + return ret; + } + } + } + + public class TransitionRelationComputation + { + private Program program; + private AtomicActionInfo first; // corresponds to that* + private AtomicActionInfo second; // corresponds to this* + private Stack<Cmd> cmdStack; + private List<PathInfo> paths; + private HashSet<Variable> frame; + private HashSet<Variable> postExistVars; + + public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars) + { + this.postExistVars = postExistVars; + this.frame = frame; + TransitionRelationComputationHelper(program, null, second); + } + + public TransitionRelationComputation(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame, HashSet<Variable> postExistVars) + { + this.postExistVars = postExistVars; + this.frame = frame; + TransitionRelationComputationHelper(program, first, second); + } + + private void TransitionRelationComputationHelper(Program program, AtomicActionInfo first, AtomicActionInfo second) + { + this.program = program; + this.first = first; + this.second = second; + this.cmdStack = new Stack<Cmd>(); + this.paths = new List<PathInfo>(); + List<IdentifierExpr> havocVars = new List<IdentifierExpr>(); + this.second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v))); + this.second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v))); + if (havocVars.Count > 0) + { + HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars); + cmdStack.Push(havocCmd); + } + Search(this.second.thisAction.Blocks[0], false); + } + + private void Substitute(Dictionary<Variable, Expr> map, ref List<Expr> pathExprs, ref Dictionary<Variable, Expr> varToExpr) + { + Substitution subst = Substituter.SubstitutionFromHashtable(map); + List<Expr> oldPathExprs = pathExprs; + pathExprs = new List<Expr>(); + foreach (Expr pathExpr in oldPathExprs) + { + pathExprs.Add(Substituter.Apply(subst, pathExpr)); + } + Dictionary<Variable, Expr> oldVarToExpr = varToExpr; + varToExpr = new Dictionary<Variable, Expr>(); + foreach (Variable v in oldVarToExpr.Keys) + { + varToExpr[v] = Substituter.Apply(subst, oldVarToExpr[v]); + } + } + + struct PathInfo + { + public HashSet<Variable> existsVars; + public Dictionary<Variable, Expr> varToExpr; + public List<Expr> pathExprs; + + public PathInfo(HashSet<Variable> existsVars, Dictionary<Variable, Expr> varToExpr, List<Expr> pathExprs) + { + this.existsVars = existsVars; + this.varToExpr = varToExpr; + this.pathExprs = pathExprs; + } + } + + private void FlattenAnd(Expr x, List<Expr> xs) + { + NAryExpr naryExpr = x as NAryExpr; + if (naryExpr != null && naryExpr.Fun.FunctionName == "&&") + { + FlattenAnd(naryExpr.Args[0], xs); + FlattenAnd(naryExpr.Args[1], xs); + } + else + { + xs.Add(x); + } + } + + private void AddPath() + { + HashSet<Variable> existsVars = new HashSet<Variable>(); + Dictionary<Variable, Expr> varToExpr = new Dictionary<Variable, Expr>(); + foreach (Variable v in frame) + { + varToExpr[v] = Expr.Ident(v); + } + if (first != null) + { + foreach (Variable v in first.thatOutParams) + { + varToExpr[v] = Expr.Ident(v); + } + } + foreach (Variable v in second.thisOutParams) + { + varToExpr[v] = Expr.Ident(v); + } + List<Expr> pathExprs = new List<Expr>(); + int boundVariableCount = 0; + foreach (Cmd cmd in cmdStack) + { + if (cmd is AssumeCmd) + { + AssumeCmd assumeCmd = cmd as AssumeCmd; + FlattenAnd(assumeCmd.Expr, pathExprs); + } + else if (cmd is AssignCmd) + { + AssignCmd assignCmd = (cmd as AssignCmd).AsSimpleAssignCmd; + Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>(); + for (int k = 0; k < assignCmd.Lhss.Count; k++) + { + map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k]; + } + Substitute(map, ref pathExprs, ref varToExpr); + } + else if (cmd is HavocCmd) + { + HavocCmd havocCmd = cmd as HavocCmd; + Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>(); + foreach (IdentifierExpr ie in havocCmd.Vars) + { + BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, ie.Decl.TypedIdent.Type)); + map[ie.Decl] = Expr.Ident(bv); + existsVars.Add(bv); + } + Substitute(map, ref pathExprs, ref varToExpr); + } + else + { + Debug.Assert(false); + } + } + paths.Add(new PathInfo(existsVars, varToExpr, pathExprs)); + } + + private Expr CalculatePathCondition(PathInfo path) + { + Expr returnExpr = Expr.True; + + HashSet<Variable> existsVars = path.existsVars; + Dictionary<Variable, Expr> existsMap = new Dictionary<Variable, Expr>(); + + Dictionary<Variable, Expr> varToExpr = path.varToExpr; + foreach (Variable v in varToExpr.Keys) + { + if (postExistVars.Contains(v)) continue; + IdentifierExpr ie = varToExpr[v] as IdentifierExpr; + if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl)) + { + existsMap[ie.Decl] = Expr.Ident(v); + existsVars.Remove(ie.Decl); + } + else + { + returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v]))); + returnExpr.Type = Type.Bool; + } + } + + List<Expr> pathExprs = new List<Expr>(); + path.pathExprs.ForEach(x => pathExprs.Add((new MyDuplicator()).VisitExpr(x))); + foreach (Expr x in pathExprs) + { + Variable boundVar; + Expr boundVarExpr; + if (InferSubstitution(x, out boundVar, out boundVarExpr) && existsVars.Contains(boundVar)) + { + existsMap[boundVar] = boundVarExpr; + existsVars.Remove(boundVar); + } + else + { + returnExpr = Expr.And(returnExpr, x); + returnExpr.Type = Type.Bool; + } + } + + returnExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), returnExpr); + if (existsVars.Count > 0) + { + returnExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), returnExpr); + } + return returnExpr; + } + + bool InferSubstitution(Expr x, out Variable var, out Expr expr) + { + var = null; + expr = null; + NAryExpr naryExpr = x as NAryExpr; + if (naryExpr == null || naryExpr.Fun.FunctionName != "==") + { + return false; + } + IdentifierExpr arg0 = naryExpr.Args[0] as IdentifierExpr; + if (arg0 != null && arg0.Decl is BoundVariable) + { + var = arg0.Decl; + expr = naryExpr.Args[1]; + return true; + } + IdentifierExpr arg1 = naryExpr.Args[1] as IdentifierExpr; + if (arg1 != null && arg1.Decl is BoundVariable) + { + var = arg1.Decl; + expr = naryExpr.Args[0]; + return true; + } + return false; + } + + public Expr TransitionRelationCompute(bool withOriginalInOutVariables = false) + { + Expr transitionRelation = Expr.False; + foreach (PathInfo path in paths) + { + transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition(path)); + } + ResolutionContext rc = new ResolutionContext(null); + rc.StateMode = ResolutionContext.State.Two; + transitionRelation.Resolve(rc); + transitionRelation.Typecheck(new TypecheckingContext(null)); + + if (withOriginalInOutVariables) + { + Dictionary<Variable, Expr> invertedMap = new Dictionary<Variable, Expr>(); + if (first != null) + { + foreach (var x in first.thatMap) + { + invertedMap[((IdentifierExpr)x.Value).Decl] = Expr.Ident(x.Key); + } + } + if (second != null) + { + foreach (var x in second.thisMap) + { + invertedMap[((IdentifierExpr)x.Value).Decl] = Expr.Ident(x.Key); + } + } + Substitution subst = Substituter.SubstitutionFromHashtable(invertedMap); + return Substituter.Apply(subst, transitionRelation); + } + else + { + return transitionRelation; + } + + } + + private void Search(Block b, bool inFirst) + { + int pathSizeAtEntry = cmdStack.Count; + foreach (Cmd cmd in b.Cmds) + { + cmdStack.Push(cmd); + } + if (b.TransferCmd is ReturnCmd) + { + if (first == null || inFirst) + { + AddPath(); + } + else + { + List<IdentifierExpr> havocVars = new List<IdentifierExpr>(); + 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); + cmdStack.Push(havocCmd); + } + Search(first.thatAction.Blocks[0], true); + } + } + else + { + GotoCmd gotoCmd = b.TransferCmd as GotoCmd; + foreach (Block target in gotoCmd.labelTargets) + { + Search(target, inFirst); + } + } + Debug.Assert(cmdStack.Count >= pathSizeAtEntry); + while (cmdStack.Count > pathSizeAtEntry) + { + cmdStack.Pop(); + } + } + } + + private static List<Block> CloneBlocks(List<Block> blocks) + { + Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>(); + List<Block> otherBlocks = new List<Block>(); + foreach (Block block in blocks) + { + List<Cmd> otherCmds = new List<Cmd>(); + foreach (Cmd cmd in block.Cmds) + { + otherCmds.Add(cmd); + } + Block otherBlock = new Block(); + otherBlock.Cmds = otherCmds; + otherBlock.Label = block.Label; + otherBlocks.Add(otherBlock); + blockMap[block] = otherBlock; + } + foreach (Block block in blocks) + { + if (block.TransferCmd is ReturnCmd) continue; + List<Block> otherGotoCmdLabelTargets = new List<Block>(); + List<string> otherGotoCmdLabelNames = new List<string>(); + GotoCmd gotoCmd = block.TransferCmd as GotoCmd; + foreach (Block target in gotoCmd.labelTargets) + { + otherGotoCmdLabelTargets.Add(blockMap[target]); + otherGotoCmdLabelNames.Add(blockMap[target].Label); + } + blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets); + } + return otherBlocks; + } + + private List<Requires> DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet<Variable> frame) + { + List<Requires> requires = new List<Requires>(); + Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToScope[domainName] = new HashSet<Variable>(); + } + 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) + { + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; + domainNameToScope[domainName].Add(v); + } + } + foreach (Variable v in second.thisInParams) + { + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; + domainNameToScope[domainName].Add(v); + } + foreach (string domainName in domainNameToScope.Keys) + { + requires.Add(new Requires(false, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName]))); + } + return requires; + } + + 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<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second); + if (commutativityCheckerCache.Contains(actionPair)) + return; + commutativityCheckerCache.Add(actionPair); + + List<Variable> inputs = new List<Variable>(); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); + List<Variable> outputs = new List<Variable>(); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); + List<Variable> locals = new List<Variable>(); + locals.AddRange(first.thatAction.LocVars); + locals.AddRange(second.thisAction.LocVars); + List<Block> firstBlocks = CloneBlocks(first.thatAction.Blocks); + List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks); + foreach (Block b in firstBlocks) + { + if (b.TransferCmd is ReturnCmd) + { + List<Block> bs = new List<Block>(); + bs.Add(secondBlocks[0]); + List<string> ls = new List<string>(); + ls.Add(secondBlocks[0].Label); + b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs); + } + } + List<Block> blocks = new List<Block>(); + blocks.AddRange(firstBlocks); + blocks.AddRange(secondBlocks); + HashSet<Variable> frame = new HashSet<Variable>(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(first.actionUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List<Requires> requires = DisjointnessRequires(program, first, second, frame); + foreach (AssertCmd assertCmd in first.thatGate) + requires.Add(new Requires(false, assertCmd.Expr)); + foreach (AssertCmd assertCmd in second.thisGate) + requires.Add(new Requires(false, assertCmd.Expr)); + List<Ensures> ensures = new List<Ensures>(); + Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet<Variable>())).TransitionRelationCompute(); + Ensures ensureCheck = new Ensures(false, transitionRelation); + ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name); + ensures.Add(ensureCheck); + string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name); + List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); + moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks); + impl.Proc = proc; + this.decls.Add(impl); + this.decls.Add(proc); + } + + private void CreateGatePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second) + { + if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0) + return; + Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second); + if (gatePreservationCheckerCache.Contains(actionPair)) + return; + gatePreservationCheckerCache.Add(actionPair); + + List<Variable> inputs = new List<Variable>(); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); + List<Variable> outputs = new List<Variable>(); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); + List<Variable> locals = new List<Variable>(); + locals.AddRange(second.thisAction.LocVars); + List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks); + HashSet<Variable> frame = new HashSet<Variable>(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List<Requires> requires = DisjointnessRequires(program, first, second, frame); + List<Ensures> ensures = new List<Ensures>(); + foreach (AssertCmd assertCmd in first.thatGate) + { + requires.Add(new Requires(false, assertCmd.Expr)); + Ensures ensureCheck = new Ensures(assertCmd.tok, false, assertCmd.Expr, null); + ensureCheck.ErrorData = string.Format("Gate not preserved by {0}", second.proc.Name); + ensures.Add(ensureCheck); + } + foreach (AssertCmd assertCmd in second.thisGate) + requires.Add(new Requires(false, assertCmd.Expr)); + string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); + List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); + moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks); + impl.Proc = proc; + this.decls.Add(impl); + this.decls.Add(proc); + } + + private void CreateFailurePreservationChecker(Program program, AtomicActionInfo first, AtomicActionInfo second) + { + if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0) + return; + Tuple<AtomicActionInfo, AtomicActionInfo> actionPair = new Tuple<AtomicActionInfo, AtomicActionInfo>(first, second); + if (failurePreservationCheckerCache.Contains(actionPair)) + return; + failurePreservationCheckerCache.Add(actionPair); + + List<Variable> inputs = new List<Variable>(); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); + List<Variable> outputs = new List<Variable>(); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); + List<Variable> locals = new List<Variable>(); + locals.AddRange(second.thisAction.LocVars); + List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks); + HashSet<Variable> frame = new HashSet<Variable>(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List<Requires> requires = DisjointnessRequires(program, first, second, frame); + Expr gateExpr = Expr.True; + foreach (AssertCmd assertCmd in first.thatGate) + { + gateExpr = Expr.And(gateExpr, assertCmd.Expr); + gateExpr.Type = Type.Bool; + } + gateExpr = Expr.Not(gateExpr); + gateExpr.Type = Type.Bool; + requires.Add(new Requires(false, gateExpr)); + List<Ensures> ensures = new List<Ensures>(); + Ensures ensureCheck = new Ensures(false, gateExpr); + ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name); + ensures.Add(ensureCheck); + foreach (AssertCmd assertCmd in second.thisGate) + requires.Add(new Requires(false, assertCmd.Expr)); + string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name); + List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); + moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks); + impl.Proc = proc; + this.decls.Add(impl); + this.decls.Add(proc); + } + + private void CreateNonBlockingChecker(Program program, AtomicActionInfo second) + { + List<Variable> inputs = new List<Variable>(); + inputs.AddRange(second.thisInParams); + + HashSet<Variable> frame = new HashSet<Variable>(); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List<Requires> requires = DisjointnessRequires(program, null, second, frame); + foreach (AssertCmd assertCmd in second.thisGate) + { + requires.Add(new Requires(false, assertCmd.Expr)); + } + HashSet<Variable> postExistVars = new HashSet<Variable>(); + postExistVars.UnionWith(frame); + postExistVars.UnionWith(second.thisOutParams); + Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute(); + List<Ensures> ensures = new List<Ensures>(); + Ensures ensureCheck = new Ensures(false, ensuresExpr); + ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name); + ensures.Add(ensureCheck); + + List<Block> blocks = new List<Block>(); + blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken))); + string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name); + List<IdentifierExpr> globalVars = new List<IdentifierExpr>(); + moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks); + impl.Proc = proc; + this.decls.Add(impl); + this.decls.Add(proc); + } + } }
\ No newline at end of file diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 626f2c4a..2ad08024 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -1,1206 +1,1206 @@ -using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Threading.Tasks;
-using Microsoft.Boogie;
-using System.Diagnostics;
-using System.Diagnostics.Contracts;
-using Microsoft.Boogie.GraphUtil;
-
-namespace Microsoft.Boogie
-{
- public class MyDuplicator : Duplicator
- {
- MoverTypeChecker moverTypeChecker;
- public int layerNum;
- Procedure enclosingProc;
- Implementation enclosingImpl;
- public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */
- public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */
- public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */
- public HashSet<Procedure> yieldingProcs;
- public List<Implementation> impls;
-
- public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum)
- {
- this.moverTypeChecker = moverTypeChecker;
- this.layerNum = layerNum;
- this.enclosingProc = null;
- this.enclosingImpl = null;
- this.procMap = new Dictionary<Procedure, Procedure>();
- this.absyMap = new Dictionary<Absy, Absy>();
- this.implMap = new Dictionary<Implementation, Implementation>();
- this.yieldingProcs = new HashSet<Procedure>();
- this.impls = new List<Implementation>();
- }
-
- private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds)
- {
- int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum;
- Procedure originalProc = originalCallCmd.Proc;
- if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc))
- {
- AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo;
- if (atomicActionInfo != null && atomicActionInfo.thisGate.Count > 0 && layerNum == enclosingProcLayerNum)
- {
- newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) })));
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- for (int i = 0; i < originalProc.InParams.Count; i++)
- {
- map[originalProc.InParams[i]] = callCmd.Ins[i];
- }
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)
- {
- newCmds.Add(Substituter.Apply(subst, assertCmd));
- }
- }
- }
- newCmds.Add(callCmd);
- }
-
- private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds)
- {
- int maxCalleeLayerNum = 0;
- foreach (CallCmd iter in originalParCallCmd.CallCmds)
- {
- int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum;
- if (calleeLayerNum > maxCalleeLayerNum)
- maxCalleeLayerNum = calleeLayerNum;
- }
- if (layerNum > maxCalleeLayerNum)
- {
- for (int i = 0; i < parCallCmd.CallCmds.Count; i++)
- {
- ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds);
- absyMap[parCallCmd.CallCmds[i]] = originalParCallCmd;
- }
- }
- else
- {
- newCmds.Add(parCallCmd);
- }
- }
-
- public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
- {
- List<Cmd> cmds = base.VisitCmdSeq(cmdSeq);
- List<Cmd> newCmds = new List<Cmd>();
- for (int i = 0; i < cmds.Count; i++)
- {
- Cmd originalCmd = cmdSeq[i];
- Cmd cmd = cmds[i];
-
- CallCmd originalCallCmd = originalCmd as CallCmd;
- if (originalCallCmd != null)
- {
- ProcessCallCmd(originalCallCmd, cmd as CallCmd, newCmds);
- continue;
- }
-
- ParCallCmd originalParCallCmd = originalCmd as ParCallCmd;
- if (originalParCallCmd != null)
- {
- ProcessParCallCmd(originalParCallCmd, cmd as ParCallCmd, newCmds);
- continue;
- }
-
- newCmds.Add(cmd);
- }
- return newCmds;
- }
-
- public override YieldCmd VisitYieldCmd(YieldCmd node)
- {
- YieldCmd yieldCmd = base.VisitYieldCmd(node);
- absyMap[yieldCmd] = node;
- return yieldCmd;
- }
-
- public override Block VisitBlock(Block node)
- {
- Block block = base.VisitBlock(node);
- absyMap[block] = node;
- return block;
- }
-
- public override Cmd VisitCallCmd(CallCmd node)
- {
- CallCmd callCmd = (CallCmd) base.VisitCallCmd(node);
- callCmd.Proc = VisitProcedure(callCmd.Proc);
- callCmd.callee = callCmd.Proc.Name;
- absyMap[callCmd] = node;
- return callCmd;
- }
-
- public override Cmd VisitParCallCmd(ParCallCmd node)
- {
- ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node);
- absyMap[parCallCmd] = node;
- return parCallCmd;
- }
-
- public override Procedure VisitProcedure(Procedure node)
- {
- if (!moverTypeChecker.procToActionInfo.ContainsKey(node))
- return node;
- if (!procMap.ContainsKey(node))
- {
- enclosingProc = node;
- Procedure proc = (Procedure)node.Clone();
- proc.Name = string.Format("{0}_{1}", node.Name, layerNum);
- proc.InParams = this.VisitVariableSeq(node.InParams);
- proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
- proc.OutParams = this.VisitVariableSeq(node.OutParams);
-
- ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node];
- if (actionInfo.createdAtLayerNum < layerNum)
- {
- proc.Requires = new List<Requires>();
- proc.Ensures = new List<Ensures>();
- Implementation impl;
- AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
- if (atomicActionInfo != null)
- {
- CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.thisAction);
- List<Cmd> cmds = new List<Cmd>();
- foreach (AssertCmd assertCmd in atomicActionInfo.thisGate)
- {
- cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr)));
- }
- Block newInitBlock = new Block(Token.NoToken, "_init", cmds,
- new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }),
- new List<Block>(new Block[] { action.Blocks[0] })));
- List<Block> newBlocks = new List<Block>();
- newBlocks.Add(newInitBlock);
- newBlocks.AddRange(action.Blocks);
- impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks);
- }
- else
- {
- Block newInitBlock = new Block(Token.NoToken, "_init", new List<Cmd>(), new ReturnCmd(Token.NoToken));
- List<Block> newBlocks = new List<Block>();
- newBlocks.Add(newInitBlock);
- impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List<Variable>(), newBlocks);
- }
- impl.Proc = proc;
- 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);
- }
- else
- {
- yieldingProcs.Add(proc);
- proc.Requires = this.VisitRequiresSeq(node.Requires);
- proc.Ensures = this.VisitEnsuresSeq(node.Ensures);
- }
- procMap[node] = proc;
- proc.Modifies = new List<IdentifierExpr>();
- moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));
- }
- return procMap[node];
- }
-
- private Variable dummyLocalVar;
- public override Implementation VisitImplementation(Implementation node)
- {
- enclosingImpl = node;
- 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;
- return impl;
- }
-
- public override Requires VisitRequires(Requires node)
- {
- Requires requires = base.VisitRequires(node);
- if (node.Free)
- return requires;
- if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
- requires.Condition = Expr.True;
- return requires;
- }
-
- public override Ensures VisitEnsures(Ensures node)
- {
- Ensures ensures = base.VisitEnsures(node);
- if (node.Free)
- return ensures;
- AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo;
- bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node;
- if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
- {
- ensures.Condition = Expr.True;
- ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes);
- }
- return ensures;
- }
-
- public override Cmd VisitAssertCmd(AssertCmd node)
- {
- AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node);
- if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum))
- assertCmd.Expr = Expr.True;
- return assertCmd;
- }
- }
-
- public class OwickiGries
- {
- LinearTypeChecker linearTypeChecker;
- MoverTypeChecker moverTypeChecker;
- Dictionary<Absy, Absy> absyMap;
- Dictionary<Implementation, Implementation> implMap;
- HashSet<Procedure> yieldingProcs;
- int layerNum;
- List<IdentifierExpr> globalMods;
- Dictionary<string, Procedure> asyncAndParallelCallDesugarings;
- List<Procedure> yieldCheckerProcs;
- List<Implementation> yieldCheckerImpls;
- Procedure yieldProc;
-
- Variable pc;
- Variable ok;
- Expr alpha;
- Expr beta;
- HashSet<Variable> frame;
-
- public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator)
- {
- this.linearTypeChecker = linearTypeChecker;
- this.moverTypeChecker = moverTypeChecker;
- this.absyMap = duplicator.absyMap;
- this.layerNum = duplicator.layerNum;
- this.implMap = duplicator.implMap;
- this.yieldingProcs = duplicator.yieldingProcs;
- Program program = linearTypeChecker.program;
- globalMods = new List<IdentifierExpr>();
- foreach (Variable g in moverTypeChecker.SharedVariables)
- {
- globalMods.Add(Expr.Ident(g));
- }
- asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();
- yieldCheckerProcs = new List<Procedure>();
- yieldCheckerImpls = new List<Implementation>();
- yieldProc = null;
- }
-
- private IEnumerable<Variable> AvailableLinearVars(Absy absy)
- {
- return linearTypeChecker.AvailableLinearVars(absyMap[absy]);
- }
-
- private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
- {
- List<Expr> exprSeq = new List<Expr>();
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
- }
- foreach (IdentifierExpr ie in globalMods)
- {
- exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
- }
- if (yieldProc == null)
- {
- List<Variable> inputs = new List<Variable>();
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- var domain = linearTypeChecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
- inputs.Add(f);
- }
- foreach (IdentifierExpr ie in globalMods)
- {
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
- inputs.Add(f);
- }
- yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", layerNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
- yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- }
- CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());
- yieldCallCmd.Proc = yieldProc;
- return yieldCallCmd;
- }
-
- private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
- {
- if (!CommandLineOptions.Clo.TrustNonInterference)
- {
- CallCmd yieldCallCmd = CallToYieldProc(tok, ogOldGlobalMap, domainNameToLocalVar);
- newCmds.Add(yieldCallCmd);
- }
-
- if (pc != null)
- {
- Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap);
- Expr bb = OldEqualityExpr(ogOldGlobalMap);
-
- // assert pc || g_old == g || beta(i, g_old, o, g);
- Expr assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta));
- assertExpr.Typecheck(new TypecheckingContext(null));
- AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, assertExpr);
- skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";
- newCmds.Add(skipOrBetaAssertCmd);
-
- // assert pc ==> o_old == o && g_old == g;
- assertExpr = Expr.Imp(Expr.Ident(pc), bb);
- assertExpr.Typecheck(new TypecheckingContext(null));
- AssertCmd skipAssertCmd = new AssertCmd(tok, assertExpr);
- skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;
- newCmds.Add(skipAssertCmd);
-
- // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g);
- List<AssignLhs> pcUpdateLHS = new List<AssignLhs>(
- new AssignLhs[] {
- new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)),
- new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))
- });
- List<Expr> pcUpdateRHS = new List<Expr>(
- new Expr[] {
- Expr.Imp(aa, Expr.Ident(pc)),
- Expr.Or(Expr.Ident(ok), beta)
- });
- foreach (Expr e in pcUpdateRHS)
- {
- e.Typecheck(new TypecheckingContext(null));
- }
- newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS));
- }
- }
-
- private Dictionary<string, Expr> ComputeAvailableExprs(IEnumerable<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)
- {
- Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- var expr = Expr.Ident(domainNameToInputVar[domainName]);
- expr.Resolve(new ResolutionContext(null));
- expr.Typecheck(new TypecheckingContext(null));
- domainNameToExpr[domainName] = expr;
- }
- foreach (Variable v in availableLinearVars)
- {
- var domainName = linearTypeChecker.FindDomainName(v);
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- var domain = linearTypeChecker.linearDomains[domainName];
- if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;
- Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });
- var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });
- expr.Resolve(new ResolutionContext(null));
- expr.Typecheck(new TypecheckingContext(null));
- domainNameToExpr[domainName] = expr;
- }
- return domainNameToExpr;
- }
-
- private void AddUpdatesToOldGlobalVars(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)
- {
- List<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));
- rhss.Add(domainNameToExpr[domainName]);
- }
- foreach (Variable g in ogOldGlobalMap.Keys)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
- rhss.Add(Expr.Ident(g));
- }
- if (lhss.Count > 0)
- {
- newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
- }
- }
-
- private Expr OldEqualityExpr(Dictionary<Variable, Variable> ogOldGlobalMap)
- {
- Expr bb = Expr.True;
- foreach (Variable o in ogOldGlobalMap.Keys)
- {
- if (o is GlobalVariable && !frame.Contains(o)) continue;
- bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
- bb.Type = Type.Bool;
- }
- return bb;
- }
-
- private Expr OldEqualityExprForGlobals(Dictionary<Variable, Variable> ogOldGlobalMap)
- {
- Expr bb = Expr.True;
- foreach (Variable o in ogOldGlobalMap.Keys)
- {
- if (o is GlobalVariable && frame.Contains(o))
- {
- bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o])));
- bb.Type = Type.Bool;
- }
- }
- return bb;
- }
-
- private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)
- {
- AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
-
- if (globalMods.Count > 0)
- {
- newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
- if (pc != null)
- {
- // assume pc || alpha(i, g);
- Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
- assumeExpr.Type = Type.Bool;
- newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
- }
- }
-
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar);
- AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
-
- for (int j = 0; j < cmds.Count; j++)
- {
- PredicateCmd predCmd = (PredicateCmd)cmds[j];
- newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr));
- }
- }
-
- public void DesugarParallelCallCmd(List<Cmd> newCmds, ParCallCmd parCallCmd)
- {
- List<string> parallelCalleeNames = new List<string>();
- List<Expr> ins = new List<Expr>();
- List<IdentifierExpr> outs = new List<IdentifierExpr>();
- string procName = "og";
- foreach (CallCmd callCmd in parCallCmd.CallCmds)
- {
- procName = procName + "_" + callCmd.Proc.Name;
- ins.AddRange(callCmd.Ins);
- outs.AddRange(callCmd.Outs);
- }
- Procedure proc;
- if (asyncAndParallelCallDesugarings.ContainsKey(procName))
- {
- proc = asyncAndParallelCallDesugarings[procName];
- }
- else
- {
- List<Variable> inParams = new List<Variable>();
- List<Variable> outParams = new List<Variable>();
- List<Requires> requiresSeq = new List<Requires>();
- List<Ensures> ensuresSeq = new List<Ensures>();
- int count = 0;
- foreach (CallCmd callCmd in parCallCmd.CallCmds)
- {
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- foreach (Variable x in callCmd.Proc.InParams)
- {
- 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] = Expr.Ident(y);
- }
- foreach (Variable x in callCmd.Proc.OutParams)
- {
- 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] = Expr.Ident(y);
- }
- Contract.Assume(callCmd.Proc.TypeParameters.Count == 0);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- foreach (Requires req in callCmd.Proc.Requires)
- {
- requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes));
- }
- foreach (Ensures ens in callCmd.Proc.Ensures)
- {
- ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes));
- }
- count++;
- }
- proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, globalMods, ensuresSeq);
- asyncAndParallelCallDesugarings[procName] = proc;
- }
- CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes);
- dummyCallCmd.Proc = proc;
- newCmds.Add(dummyCallCmd);
- }
-
- private void CreateYieldCheckerImpl(Implementation impl, List<List<Cmd>> yields)
- {
- if (yields.Count == 0) return;
-
- Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();
- foreach (Variable local in impl.LocVars)
- {
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));
- map[local] = Expr.Ident(copy);
- }
-
- Program program = linearTypeChecker.program;
- List<Variable> locals = new List<Variable>();
- List<Variable> inputs = new List<Variable>();
- foreach (IdentifierExpr ie in map.Values)
- {
- locals.Add(ie.Decl);
- }
- for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
- {
- Variable inParam = impl.InParams[i];
- Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
- locals.Add(copy);
- map[impl.InParams[i]] = Expr.Ident(copy);
- }
- {
- int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- Variable inParam = impl.InParams[i];
- Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);
- inputs.Add(copy);
- map[impl.InParams[i]] = Expr.Ident(copy);
- i++;
- }
- }
- for (int i = 0; i < impl.OutParams.Count; i++)
- {
- Variable outParam = impl.OutParams[i];
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));
- locals.Add(copy);
- map[impl.OutParams[i]] = Expr.Ident(copy);
- }
- Dictionary<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();
- Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map);
- foreach (IdentifierExpr ie in globalMods)
- {
- Variable g = ie.Decl;
- var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type));
- locals.Add(copy);
- ogOldLocalMap[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);
- assumeMap[g] = Expr.Ident(f);
- }
-
- Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);
- Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);
- Substitution subst = Substituter.SubstitutionFromHashtable(map);
- List<Block> yieldCheckerBlocks = new List<Block>();
- List<String> labels = new List<String>();
- List<Block> labelTargets = new List<Block>();
- Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
- int yieldCount = 0;
- foreach (List<Cmd> cs in yields)
- {
- List<Cmd> newCmds = new List<Cmd>();
- foreach (Cmd cmd in cs)
- {
- PredicateCmd predCmd = (PredicateCmd)cmd;
- newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));
- }
- foreach (Cmd cmd in cs)
- {
- PredicateCmd predCmd = (PredicateCmd)cmd;
- var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);
- if (predCmd is AssertCmd)
- {
- AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);
- assertCmd.ErrorData = "Non-interference check failed";
- newCmds.Add(assertCmd);
- }
- else
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));
- }
- }
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
- yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));
- labels.Add(yieldCheckerBlock.Label);
- labelTargets.Add(yieldCheckerBlock);
- yieldCheckerBlocks.Add(yieldCheckerBlock);
- }
- yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));
-
- // Create the yield checker procedure
- var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name);
- var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());
- yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- yieldCheckerProcs.Add(yieldCheckerProc);
-
- // Create the yield checker implementation
- var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List<Variable>(), locals, yieldCheckerBlocks);
- yieldCheckerImpl.Proc = yieldCheckerProc;
- yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- yieldCheckerImpls.Add(yieldCheckerImpl);
- }
-
- private bool IsYieldingHeader(Graph<Block> graph, Block header)
- {
- foreach (Block backEdgeNode in graph.BackEdgeNodes(header))
- {
- foreach (Block x in graph.NaturalLoops(header, backEdgeNode))
- {
- foreach (Cmd cmd in x.Cmds)
- {
- if (cmd is YieldCmd)
- return true;
- if (cmd is ParCallCmd)
- return true;
- CallCmd callCmd = cmd as CallCmd;
- if (callCmd == null) continue;
- if (yieldingProcs.Contains(callCmd.Proc))
- return true;
- }
- }
- }
- return false;
- }
-
- private Graph<Block> ComputeYieldingLoopHeaders(Implementation impl, out HashSet<Block> yieldingHeaders)
- {
- Graph<Block> graph;
- impl.PruneUnreachableBlocks();
- impl.ComputePredecessorsForBlocks();
- graph = Program.GraphFromImpl(impl);
- graph.ComputeLoops();
- if (!graph.Reducible)
- {
- throw new Exception("Irreducible flow graphs are unsupported.");
- }
- yieldingHeaders = new HashSet<Block>();
- IEnumerable<Block> sortedHeaders = graph.SortHeadersByDominance();
- foreach (Block header in sortedHeaders)
- {
- if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header)))
- {
- yieldingHeaders.Add(header);
- }
- else if (IsYieldingHeader(graph, header))
- {
- yieldingHeaders.Add(header);
- }
- else
- {
- continue;
- }
- }
- return graph;
- }
-
- private void SetupRefinementCheck(Implementation impl,
- out List<Variable> newLocalVars,
- out Dictionary<string, Variable> domainNameToInputVar, out Dictionary<string, Variable> domainNameToLocalVar, out Dictionary<Variable, Variable> ogOldGlobalMap)
- {
- pc = null;
- ok = null;
- alpha = null;
- beta = null;
- frame = null;
-
- newLocalVars = new List<Variable>();
- Program program = linearTypeChecker.program;
- ogOldGlobalMap = new Dictionary<Variable, Variable>();
- foreach (IdentifierExpr ie in globalMods)
- {
- Variable g = ie.Decl;
- LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type));
- ogOldGlobalMap[g] = l;
- newLocalVars.Add(l);
- }
-
- Procedure originalProc = implMap[impl].Proc;
- ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc];
- if (actionInfo.createdAtLayerNum == this.layerNum)
- {
- pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool));
- newLocalVars.Add(pc);
- ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool));
- newLocalVars.Add(ok);
- Dictionary<Variable, Expr> alwaysMap = new Dictionary<Variable, Expr>();
- for (int i = 0; i < originalProc.InParams.Count; i++)
- {
- alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]);
- }
- for (int i = 0; i < originalProc.OutParams.Count; i++)
- {
- alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]);
- }
- Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);
- Dictionary<Variable, Expr> foroldMap = new Dictionary<Variable, Expr>();
- foreach (IdentifierExpr ie in globalMods)
- {
- foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);
- }
- Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
- frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);
- HashSet<Variable> introducedVars = new HashSet<Variable>();
- foreach (Variable v in moverTypeChecker.SharedVariables)
- {
- if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum ||
- moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)
- {
- frame.Remove(v);
- }
- if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)
- {
- introducedVars.Add(v);
- }
- }
- AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;
- if (atomicActionInfo == null)
- {
- beta = Expr.True;
- foreach (var v in frame)
- {
- beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v]));
- }
- 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 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));
- newLocalVars.Add(copy);
- ogOldGlobalMap[f] = copy;
- }
- }
-
- domainNameToInputVar = new Dictionary<string, Variable>();
- domainNameToLocalVar = new Dictionary<string, Variable>();
- {
- int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count;
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- Variable inParam = impl.InParams[i];
- domainNameToInputVar[domainName] = inParam;
- Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type));
- domainNameToLocalVar[domainName] = l;
- newLocalVars.Add(l);
- i++;
- }
- }
- }
-
- private void TransformImpl(Implementation impl)
- {
- HashSet<Block> yieldingHeaders;
- Graph<Block> graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders);
-
- List<Variable> newLocalVars;
- Dictionary<string, Variable> domainNameToInputVar, domainNameToLocalVar;
- Dictionary<Variable, Variable> ogOldGlobalMap;
- SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap);
-
- List<List<Cmd>> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);
-
- List<Variable> oldPcs, oldOks;
- ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks);
-
- AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap);
-
- CreateYieldCheckerImpl(impl, yields);
-
- impl.LocVars.AddRange(newLocalVars);
- impl.LocVars.AddRange(oldPcs);
- impl.LocVars.AddRange(oldOks);
-
- UnifyCallsToYieldProc(impl, ogOldGlobalMap, domainNameToLocalVar);
- }
-
- private void UnifyCallsToYieldProc(Implementation impl, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
- {
- CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar);
- Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List<Cmd>(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken));
- List<Block> newBlocks = new List<Block>();
- foreach (Block b in impl.Blocks)
- {
- TransferCmd transferCmd = b.TransferCmd;
- List<Cmd> newCmds = new List<Cmd>();
- for (int i = b.Cmds.Count-1; i >= 0; i--)
- {
- CallCmd callCmd = b.Cmds[i] as CallCmd;
- if (callCmd == null || callCmd.Proc != yieldProc)
- {
- newCmds.Insert(0, b.Cmds[i]);
- }
- else
- {
- Block newBlock = new Block(Token.NoToken, b.Label + i, newCmds, transferCmd);
- newCmds = new List<Cmd>();
- transferCmd = new GotoCmd(Token.NoToken, new List<string>(new string[] { newBlock.Label, yieldCheckBlock.Label }),
- new List<Block>(new Block[] { newBlock, yieldCheckBlock }));
- newBlocks.Add(newBlock);
- }
- }
- b.Cmds = newCmds;
- b.TransferCmd = transferCmd;
- }
- impl.Blocks.AddRange(newBlocks);
- impl.Blocks.Add(yieldCheckBlock);
- }
-
- private List<List<Cmd>> CollectAndDesugarYields(Implementation impl,
- Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)
- {
- // Collect the yield predicates and desugar yields
- List<List<Cmd>> yields = new List<List<Cmd>>();
- List<Cmd> cmds = new List<Cmd>();
- foreach (Block b in impl.Blocks)
- {
- YieldCmd yieldCmd = null;
- List<Cmd> newCmds = new List<Cmd>();
- for (int i = 0; i < b.Cmds.Count; i++)
- {
- Cmd cmd = b.Cmds[i];
- if (cmd is YieldCmd)
- {
- yieldCmd = (YieldCmd)cmd;
- continue;
- }
- if (yieldCmd != null)
- {
- PredicateCmd pcmd = cmd as PredicateCmd;
- if (pcmd == null)
- {
- DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
- if (cmds.Count > 0)
- {
- yields.Add(cmds);
- cmds = new List<Cmd>();
- }
- yieldCmd = null;
- }
- else
- {
- cmds.Add(pcmd);
- }
- }
-
- if (cmd is CallCmd)
- {
- CallCmd callCmd = cmd as CallCmd;
- if (yieldingProcs.Contains(callCmd.Proc))
- {
- AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
- }
- if (callCmd.IsAsync)
- {
- if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))
- {
- asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>());
- }
- var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];
- CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes);
- dummyCallCmd.Proc = dummyAsyncTargetProc;
- newCmds.Add(dummyCallCmd);
- }
- else
- {
- newCmds.Add(callCmd);
- }
- if (yieldingProcs.Contains(callCmd.Proc))
- {
- HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));
- linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);
-
- if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null)
- {
- // assume pc || alpha(i, g);
- Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
- assumeExpr.Type = Type.Bool;
- newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
- }
-
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
- AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
- }
- }
- else if (cmd is ParCallCmd)
- {
- ParCallCmd parCallCmd = cmd as ParCallCmd;
- AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
- DesugarParallelCallCmd(newCmds, parCallCmd);
- HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));
- linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);
-
- if (globalMods.Count > 0 && pc != null)
- {
- // assume pc || alpha(i, g);
- Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
- assumeExpr.Type = Type.Bool;
- newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
- }
-
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);
- AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
- }
- else
- {
- newCmds.Add(cmd);
- }
- }
- if (yieldCmd != null)
- {
- DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
- if (cmds.Count > 0)
- {
- yields.Add(cmds);
- cmds = new List<Cmd>();
- }
- }
- if (b.TransferCmd is ReturnCmd)
- {
- AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);
- if (pc != null)
- {
- AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok));
- assertCmd.ErrorData = "Failed to execute atomic action before procedure return";
- newCmds.Add(assertCmd);
- }
- }
- b.Cmds = newCmds;
- }
- return yields;
- }
-
- private void ProcessLoopHeaders(Implementation impl, Graph<Block> graph, HashSet<Block> yieldingHeaders,
- Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap,
- out List<Variable> oldPcs, out List<Variable> oldOks)
- {
- oldPcs = new List<Variable>();
- oldOks = new List<Variable>();
- 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));
- oldPcs.Add(oldPc);
- oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool));
- oldOks.Add(oldOk);
- }
- Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);
- foreach (Block pred in header.Predecessors)
- {
- AddCallToYieldProc(header.tok, pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
- if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))
- {
- pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>(
- new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }),
- new List<Expr>(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) })));
- }
- AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
- }
- List<Cmd> newCmds = new List<Cmd>();
- if (pc != null)
- {
- AssertCmd assertCmd;
- assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc)));
- assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";
- newCmds.Add(assertCmd);
- 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])));
- }
- foreach (Variable v in ogOldGlobalMap.Keys)
- {
- newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));
- }
- newCmds.AddRange(header.Cmds);
- header.Cmds = newCmds;
- }
- }
-
- private void AddInitialBlock(Implementation impl, List<Variable> oldPcs, List<Variable> oldOks,
- Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap)
- {
- // Add initial block
- List<AssignLhs> lhss = new List<AssignLhs>();
- List<Expr> rhss = new List<Expr>();
- if (pc != null)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));
- rhss.Add(Expr.False);
- foreach (Variable oldPc in oldPcs)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)));
- rhss.Add(Expr.False);
- }
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));
- rhss.Add(Expr.False);
- foreach (Variable oldOk in oldOks)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)));
- rhss.Add(Expr.False);
- }
- }
- Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();
- foreach (var domainName in linearTypeChecker.linearDomains.Keys)
- {
- domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);
- }
- for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)
- {
- Variable v = impl.InParams[i];
- var domainName = linearTypeChecker.FindDomainName(v);
- if (domainName == null) continue;
- if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;
- var domain = linearTypeChecker.linearDomains[domainName];
- if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;
- Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });
- domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });
- }
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));
- rhss.Add(domainNameToExpr[domainName]);
- }
- foreach (Variable g in ogOldGlobalMap.Keys)
- {
- lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));
- rhss.Add(Expr.Ident(g));
- }
- if (lhss.Count > 0)
- {
- Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));
- impl.Blocks.Insert(0, initBlock);
- }
- }
-
- private void AddYieldProcAndImpl(List<Declaration> decls)
- {
- if (yieldProc == null) return;
-
- Program program = linearTypeChecker.program;
- List<Variable> inputs = new List<Variable>();
- foreach (string domainName in linearTypeChecker.linearDomains.Keys)
- {
- var domain = linearTypeChecker.linearDomains[domainName];
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);
- inputs.Add(f);
- }
- foreach (IdentifierExpr ie in globalMods)
- {
- Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);
- inputs.Add(f);
- }
- List<Block> blocks = new List<Block>();
- TransferCmd transferCmd = new ReturnCmd(Token.NoToken);
- if (yieldCheckerProcs.Count > 0)
- {
- List<Block> blockTargets = new List<Block>();
- List<String> labelTargets = new List<String>();
- int labelCount = 0;
- foreach (Procedure proc in yieldCheckerProcs)
- {
- List<Expr> exprSeq = new List<Expr>();
- foreach (Variable v in inputs)
- {
- exprSeq.Add(Expr.Ident(v));
- }
- CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());
- callCmd.Proc = proc;
- string label = string.Format("L_{0}", labelCount++);
- Block block = new Block(Token.NoToken, label, new List<Cmd> { callCmd }, new ReturnCmd(Token.NoToken));
- labelTargets.Add(label);
- blockTargets.Add(block);
- blocks.Add(block);
- }
- transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);
- }
- blocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), transferCmd));
-
- var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);
- yieldImpl.Proc = yieldProc;
- yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
- decls.Add(yieldProc);
- decls.Add(yieldImpl);
- }
-
- public static QKeyValue RemoveYieldsAttribute(QKeyValue iter)
- {
- if (iter == null) return null;
- iter.Next = RemoveYieldsAttribute(iter.Next);
- return (iter.Key == "yields") ? iter.Next : iter;
- }
-
- public static QKeyValue RemoveMoverAttribute(QKeyValue iter)
- {
- if (iter == null) return null;
- iter.Next = RemoveMoverAttribute(iter.Next);
- if (iter.Key == "atomic" || iter.Key == "right" || iter.Key == "left" || iter.Key == "both")
- return iter.Next;
- else
- return iter;
- }
-
- private List<Declaration> Collect()
- {
- List<Declaration> decls = new List<Declaration>();
- foreach (Procedure proc in yieldCheckerProcs)
- {
- decls.Add(proc);
- }
- foreach (Implementation impl in yieldCheckerImpls)
- {
- decls.Add(impl);
- }
- foreach (Procedure proc in asyncAndParallelCallDesugarings.Values)
- {
- decls.Add(proc);
- }
- AddYieldProcAndImpl(decls);
- return decls;
- }
-
- public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)
- {
- Program program = linearTypeChecker.program;
- foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))
- {
- if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;
-
- MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum);
- foreach (var proc in program.Procedures)
- {
- if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue;
- Procedure duplicateProc = duplicator.VisitProcedure(proc);
- decls.Add(duplicateProc);
- }
- decls.AddRange(duplicator.impls);
- OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator);
- foreach (var impl in program.Implementations)
- {
- if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum)
- continue;
- Implementation duplicateImpl = duplicator.VisitImplementation(impl);
- ogTransform.TransformImpl(duplicateImpl);
- decls.Add(duplicateImpl);
- }
- decls.AddRange(ogTransform.Collect());
- }
- }
- }
-}
+using System; +using System.Collections; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.Boogie; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using Microsoft.Boogie.GraphUtil; + +namespace Microsoft.Boogie +{ + public class MyDuplicator : Duplicator + { + MoverTypeChecker moverTypeChecker; + public int layerNum; + Procedure enclosingProc; + Implementation enclosingImpl; + public Dictionary<Procedure, Procedure> procMap; /* Original -> Duplicate */ + public Dictionary<Absy, Absy> absyMap; /* Duplicate -> Original */ + public Dictionary<Implementation, Implementation> implMap; /* Duplicate -> Original */ + public HashSet<Procedure> yieldingProcs; + public List<Implementation> impls; + + public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum) + { + this.moverTypeChecker = moverTypeChecker; + this.layerNum = layerNum; + this.enclosingProc = null; + this.enclosingImpl = null; + this.procMap = new Dictionary<Procedure, Procedure>(); + this.absyMap = new Dictionary<Absy, Absy>(); + this.implMap = new Dictionary<Implementation, Implementation>(); + this.yieldingProcs = new HashSet<Procedure>(); + this.impls = new List<Implementation>(); + } + + private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List<Cmd> newCmds) + { + int enclosingProcLayerNum = moverTypeChecker.procToActionInfo[enclosingImpl.Proc].createdAtLayerNum; + Procedure originalProc = originalCallCmd.Proc; + if (moverTypeChecker.procToActionInfo.ContainsKey(originalProc)) + { + AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[originalProc] as AtomicActionInfo; + if (atomicActionInfo != null && atomicActionInfo.gate.Count > 0 && layerNum == enclosingProcLayerNum) + { + newCmds.Add(new HavocCmd(Token.NoToken, new List<IdentifierExpr>(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); + Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>(); + for (int i = 0; i < originalProc.InParams.Count; i++) + { + map[originalProc.InParams[i]] = callCmd.Ins[i]; + } + Substitution subst = Substituter.SubstitutionFromHashtable(map); + foreach (AssertCmd assertCmd in atomicActionInfo.gate) + { + newCmds.Add(Substituter.Apply(subst, assertCmd)); + } + } + } + newCmds.Add(callCmd); + } + + private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List<Cmd> newCmds) + { + int maxCalleeLayerNum = 0; + foreach (CallCmd iter in originalParCallCmd.CallCmds) + { + int calleeLayerNum = moverTypeChecker.procToActionInfo[iter.Proc].createdAtLayerNum; + if (calleeLayerNum > maxCalleeLayerNum) + maxCalleeLayerNum = calleeLayerNum; + } + if (layerNum > maxCalleeLayerNum) + { + for (int i = 0; i < parCallCmd.CallCmds.Count; i++) + { + ProcessCallCmd(originalParCallCmd.CallCmds[i], parCallCmd.CallCmds[i], newCmds); + absyMap[parCallCmd.CallCmds[i]] = originalParCallCmd; + } + } + else + { + newCmds.Add(parCallCmd); + } + } + + public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) + { + List<Cmd> cmds = base.VisitCmdSeq(cmdSeq); + List<Cmd> newCmds = new List<Cmd>(); + for (int i = 0; i < cmds.Count; i++) + { + Cmd originalCmd = cmdSeq[i]; + Cmd cmd = cmds[i]; + + CallCmd originalCallCmd = originalCmd as CallCmd; + if (originalCallCmd != null) + { + ProcessCallCmd(originalCallCmd, cmd as CallCmd, newCmds); + continue; + } + + ParCallCmd originalParCallCmd = originalCmd as ParCallCmd; + if (originalParCallCmd != null) + { + ProcessParCallCmd(originalParCallCmd, cmd as ParCallCmd, newCmds); + continue; + } + + newCmds.Add(cmd); + } + return newCmds; + } + + public override YieldCmd VisitYieldCmd(YieldCmd node) + { + YieldCmd yieldCmd = base.VisitYieldCmd(node); + absyMap[yieldCmd] = node; + return yieldCmd; + } + + public override Block VisitBlock(Block node) + { + Block block = base.VisitBlock(node); + absyMap[block] = node; + return block; + } + + public override Cmd VisitCallCmd(CallCmd node) + { + CallCmd callCmd = (CallCmd) base.VisitCallCmd(node); + callCmd.Proc = VisitProcedure(callCmd.Proc); + callCmd.callee = callCmd.Proc.Name; + absyMap[callCmd] = node; + return callCmd; + } + + public override Cmd VisitParCallCmd(ParCallCmd node) + { + ParCallCmd parCallCmd = (ParCallCmd) base.VisitParCallCmd(node); + absyMap[parCallCmd] = node; + return parCallCmd; + } + + public override Procedure VisitProcedure(Procedure node) + { + if (!moverTypeChecker.procToActionInfo.ContainsKey(node)) + return node; + if (!procMap.ContainsKey(node)) + { + enclosingProc = node; + Procedure proc = (Procedure)node.Clone(); + proc.Name = string.Format("{0}_{1}", node.Name, layerNum); + proc.InParams = this.VisitVariableSeq(node.InParams); + proc.Modifies = this.VisitIdentifierExprSeq(node.Modifies); + proc.OutParams = this.VisitVariableSeq(node.OutParams); + + ActionInfo actionInfo = moverTypeChecker.procToActionInfo[node]; + if (actionInfo.createdAtLayerNum < layerNum) + { + proc.Requires = new List<Requires>(); + proc.Ensures = new List<Ensures>(); + Implementation impl; + AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; + if (atomicActionInfo != null) + { + CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.action); + List<Cmd> cmds = new List<Cmd>(); + foreach (AssertCmd assertCmd in atomicActionInfo.gate) + { + cmds.Add(new AssumeCmd(Token.NoToken, (Expr)Visit(assertCmd.Expr))); + } + Block newInitBlock = new Block(Token.NoToken, "_init", cmds, + new GotoCmd(Token.NoToken, new List<string>(new string[] { action.Blocks[0].Label }), + new List<Block>(new Block[] { action.Blocks[0] }))); + List<Block> newBlocks = new List<Block>(); + newBlocks.Add(newInitBlock); + newBlocks.AddRange(action.Blocks); + impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks); + } + else + { + Block newInitBlock = new Block(Token.NoToken, "_init", new List<Cmd>(), new ReturnCmd(Token.NoToken)); + List<Block> newBlocks = new List<Block>(); + newBlocks.Add(newInitBlock); + impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List<Variable>(), newBlocks); + } + impl.Proc = proc; + 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); + } + else + { + yieldingProcs.Add(proc); + proc.Requires = this.VisitRequiresSeq(node.Requires); + proc.Ensures = this.VisitEnsuresSeq(node.Ensures); + } + procMap[node] = proc; + proc.Modifies = new List<IdentifierExpr>(); + moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x))); + } + return procMap[node]; + } + + private Variable dummyLocalVar; + public override Implementation VisitImplementation(Implementation node) + { + enclosingImpl = node; + 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; + return impl; + } + + public override Requires VisitRequires(Requires node) + { + Requires requires = base.VisitRequires(node); + if (node.Free) + return requires; + if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + requires.Condition = Expr.True; + return requires; + } + + public override Ensures VisitEnsures(Ensures node) + { + Ensures ensures = base.VisitEnsures(node); + if (node.Free) + return ensures; + AtomicActionInfo atomicActionInfo = moverTypeChecker.procToActionInfo[enclosingProc] as AtomicActionInfo; + bool isAtomicSpecification = atomicActionInfo != null && atomicActionInfo.ensures == node; + if (isAtomicSpecification || !moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + { + ensures.Condition = Expr.True; + ensures.Attributes = OwickiGries.RemoveMoverAttribute(ensures.Attributes); + } + return ensures; + } + + public override Cmd VisitAssertCmd(AssertCmd node) + { + AssertCmd assertCmd = (AssertCmd) base.VisitAssertCmd(node); + if (!moverTypeChecker.absyToLayerNums[node].Contains(layerNum)) + assertCmd.Expr = Expr.True; + return assertCmd; + } + } + + public class OwickiGries + { + LinearTypeChecker linearTypeChecker; + MoverTypeChecker moverTypeChecker; + Dictionary<Absy, Absy> absyMap; + Dictionary<Implementation, Implementation> implMap; + HashSet<Procedure> yieldingProcs; + int layerNum; + List<IdentifierExpr> globalMods; + Dictionary<string, Procedure> asyncAndParallelCallDesugarings; + List<Procedure> yieldCheckerProcs; + List<Implementation> yieldCheckerImpls; + Procedure yieldProc; + + Variable pc; + Variable ok; + Expr alpha; + Expr beta; + HashSet<Variable> frame; + + public OwickiGries(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, MyDuplicator duplicator) + { + this.linearTypeChecker = linearTypeChecker; + this.moverTypeChecker = moverTypeChecker; + this.absyMap = duplicator.absyMap; + this.layerNum = duplicator.layerNum; + this.implMap = duplicator.implMap; + this.yieldingProcs = duplicator.yieldingProcs; + Program program = linearTypeChecker.program; + globalMods = new List<IdentifierExpr>(); + foreach (Variable g in moverTypeChecker.SharedVariables) + { + globalMods.Add(Expr.Ident(g)); + } + asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>(); + yieldCheckerProcs = new List<Procedure>(); + yieldCheckerImpls = new List<Implementation>(); + yieldProc = null; + } + + private IEnumerable<Variable> AvailableLinearVars(Absy absy) + { + return linearTypeChecker.AvailableLinearVars(absyMap[absy]); + } + + private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar) + { + List<Expr> exprSeq = new List<Expr>(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName])); + } + foreach (IdentifierExpr ie in globalMods) + { + exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl])); + } + if (yieldProc == null) + { + List<Variable> inputs = new List<Variable>(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + var domain = linearTypeChecker.linearDomains[domainName]; + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true); + inputs.Add(f); + } + foreach (IdentifierExpr ie in globalMods) + { + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); + inputs.Add(f); + } + yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", layerNum), new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>()); + yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + } + CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>()); + yieldCallCmd.Proc = yieldProc; + return yieldCallCmd; + } + + private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar) + { + if (!CommandLineOptions.Clo.TrustNonInterference) + { + CallCmd yieldCallCmd = CallToYieldProc(tok, ogOldGlobalMap, domainNameToLocalVar); + newCmds.Add(yieldCallCmd); + } + + if (pc != null) + { + Expr aa = OldEqualityExprForGlobals(ogOldGlobalMap); + Expr bb = OldEqualityExpr(ogOldGlobalMap); + + // assert pc || g_old == g || beta(i, g_old, o, g); + Expr assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta)); + assertExpr.Typecheck(new TypecheckingContext(null)); + AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, assertExpr); + skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated"; + newCmds.Add(skipOrBetaAssertCmd); + + // assert pc ==> o_old == o && g_old == g; + assertExpr = Expr.Imp(Expr.Ident(pc), bb); + assertExpr.Typecheck(new TypecheckingContext(null)); + AssertCmd skipAssertCmd = new AssertCmd(tok, assertExpr); + skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ; + newCmds.Add(skipAssertCmd); + + // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g); + List<AssignLhs> pcUpdateLHS = new List<AssignLhs>( + new AssignLhs[] { + new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), + new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)) + }); + List<Expr> pcUpdateRHS = new List<Expr>( + new Expr[] { + Expr.Imp(aa, Expr.Ident(pc)), + Expr.Or(Expr.Ident(ok), beta) + }); + foreach (Expr e in pcUpdateRHS) + { + e.Typecheck(new TypecheckingContext(null)); + } + newCmds.Add(new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS)); + } + } + + private Dictionary<string, Expr> ComputeAvailableExprs(IEnumerable<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar) + { + Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + var expr = Expr.Ident(domainNameToInputVar[domainName]); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + domainNameToExpr[domainName] = expr; + } + foreach (Variable v in availableLinearVars) + { + var domainName = linearTypeChecker.FindDomainName(v); + if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; + var domain = linearTypeChecker.linearDomains[domainName]; + if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue; + Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) }); + var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] }); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + domainNameToExpr[domainName] = expr; + } + return domainNameToExpr; + } + + private void AddUpdatesToOldGlobalVars(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr) + { + List<AssignLhs> lhss = new List<AssignLhs>(); + List<Expr> rhss = new List<Expr>(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); + rhss.Add(domainNameToExpr[domainName]); + } + foreach (Variable g in ogOldGlobalMap.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); + rhss.Add(Expr.Ident(g)); + } + if (lhss.Count > 0) + { + newCmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); + } + } + + private Expr OldEqualityExpr(Dictionary<Variable, Variable> ogOldGlobalMap) + { + Expr bb = Expr.True; + foreach (Variable o in ogOldGlobalMap.Keys) + { + if (o is GlobalVariable && !frame.Contains(o)) continue; + bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); + bb.Type = Type.Bool; + } + return bb; + } + + private Expr OldEqualityExprForGlobals(Dictionary<Variable, Variable> ogOldGlobalMap) + { + Expr bb = Expr.True; + foreach (Variable o in ogOldGlobalMap.Keys) + { + if (o is GlobalVariable && frame.Contains(o)) + { + bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); + bb.Type = Type.Bool; + } + } + return bb; + } + + private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar) + { + AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + + if (globalMods.Count > 0) + { + newCmds.Add(new HavocCmd(Token.NoToken, globalMods)); + if (pc != null) + { + // assume pc || alpha(i, g); + Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); + assumeExpr.Type = Type.Bool; + newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); + } + } + + Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(yieldCmd), domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + + for (int j = 0; j < cmds.Count; j++) + { + PredicateCmd predCmd = (PredicateCmd)cmds[j]; + newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr)); + } + } + + public void DesugarParallelCallCmd(List<Cmd> newCmds, ParCallCmd parCallCmd) + { + List<string> parallelCalleeNames = new List<string>(); + List<Expr> ins = new List<Expr>(); + List<IdentifierExpr> outs = new List<IdentifierExpr>(); + string procName = "og"; + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + procName = procName + "_" + callCmd.Proc.Name; + ins.AddRange(callCmd.Ins); + outs.AddRange(callCmd.Outs); + } + Procedure proc; + if (asyncAndParallelCallDesugarings.ContainsKey(procName)) + { + proc = asyncAndParallelCallDesugarings[procName]; + } + else + { + List<Variable> inParams = new List<Variable>(); + List<Variable> outParams = new List<Variable>(); + List<Requires> requiresSeq = new List<Requires>(); + List<Ensures> ensuresSeq = new List<Ensures>(); + int count = 0; + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>(); + foreach (Variable x in callCmd.Proc.InParams) + { + 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] = Expr.Ident(y); + } + foreach (Variable x in callCmd.Proc.OutParams) + { + 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] = Expr.Ident(y); + } + Contract.Assume(callCmd.Proc.TypeParameters.Count == 0); + Substitution subst = Substituter.SubstitutionFromHashtable(map); + foreach (Requires req in callCmd.Proc.Requires) + { + requiresSeq.Add(new Requires(req.tok, req.Free, Substituter.Apply(subst, req.Condition), null, req.Attributes)); + } + foreach (Ensures ens in callCmd.Proc.Ensures) + { + ensuresSeq.Add(new Ensures(ens.tok, ens.Free, Substituter.Apply(subst, ens.Condition), null, ens.Attributes)); + } + count++; + } + proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, globalMods, ensuresSeq); + asyncAndParallelCallDesugarings[procName] = proc; + } + CallCmd dummyCallCmd = new CallCmd(parCallCmd.tok, proc.Name, ins, outs, parCallCmd.Attributes); + dummyCallCmd.Proc = proc; + newCmds.Add(dummyCallCmd); + } + + private void CreateYieldCheckerImpl(Implementation impl, List<List<Cmd>> yields) + { + if (yields.Count == 0) return; + + Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>(); + foreach (Variable local in impl.LocVars) + { + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); + map[local] = Expr.Ident(copy); + } + + Program program = linearTypeChecker.program; + List<Variable> locals = new List<Variable>(); + List<Variable> inputs = new List<Variable>(); + foreach (IdentifierExpr ie in map.Values) + { + locals.Add(ie.Decl); + } + for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + { + Variable inParam = impl.InParams[i]; + Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type)); + locals.Add(copy); + map[impl.InParams[i]] = Expr.Ident(copy); + } + { + int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + Variable inParam = impl.InParams[i]; + Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true); + inputs.Add(copy); + map[impl.InParams[i]] = Expr.Ident(copy); + i++; + } + } + for (int i = 0; i < impl.OutParams.Count; i++) + { + Variable outParam = impl.OutParams[i]; + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type)); + locals.Add(copy); + map[impl.OutParams[i]] = Expr.Ident(copy); + } + Dictionary<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>(); + Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(map); + foreach (IdentifierExpr ie in globalMods) + { + Variable g = ie.Decl; + var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_local_old_{0}", g.Name), g.TypedIdent.Type)); + locals.Add(copy); + ogOldLocalMap[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); + assumeMap[g] = Expr.Ident(f); + } + + Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap); + Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap); + Substitution subst = Substituter.SubstitutionFromHashtable(map); + List<Block> yieldCheckerBlocks = new List<Block>(); + List<String> labels = new List<String>(); + List<Block> labelTargets = new List<Block>(); + Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken)); + labels.Add(yieldCheckerBlock.Label); + labelTargets.Add(yieldCheckerBlock); + yieldCheckerBlocks.Add(yieldCheckerBlock); + int yieldCount = 0; + foreach (List<Cmd> cs in yields) + { + List<Cmd> newCmds = new List<Cmd>(); + foreach (Cmd cmd in cs) + { + PredicateCmd predCmd = (PredicateCmd)cmd; + newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr))); + } + foreach (Cmd cmd in cs) + { + PredicateCmd predCmd = (PredicateCmd)cmd; + var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr); + if (predCmd is AssertCmd) + { + AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes); + assertCmd.ErrorData = "Non-interference check failed"; + newCmds.Add(assertCmd); + } + else + { + newCmds.Add(new AssumeCmd(Token.NoToken, newExpr)); + } + } + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); + yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken)); + labels.Add(yieldCheckerBlock.Label); + labelTargets.Add(yieldCheckerBlock); + yieldCheckerBlocks.Add(yieldCheckerBlock); + } + yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets))); + + // Create the yield checker procedure + var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", "Impl", impl.Name); + var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>()); + yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + yieldCheckerProcs.Add(yieldCheckerProc); + + // Create the yield checker implementation + var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List<Variable>(), locals, yieldCheckerBlocks); + yieldCheckerImpl.Proc = yieldCheckerProc; + yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + yieldCheckerImpls.Add(yieldCheckerImpl); + } + + private bool IsYieldingHeader(Graph<Block> graph, Block header) + { + foreach (Block backEdgeNode in graph.BackEdgeNodes(header)) + { + foreach (Block x in graph.NaturalLoops(header, backEdgeNode)) + { + foreach (Cmd cmd in x.Cmds) + { + if (cmd is YieldCmd) + return true; + if (cmd is ParCallCmd) + return true; + CallCmd callCmd = cmd as CallCmd; + if (callCmd == null) continue; + if (yieldingProcs.Contains(callCmd.Proc)) + return true; + } + } + } + return false; + } + + private Graph<Block> ComputeYieldingLoopHeaders(Implementation impl, out HashSet<Block> yieldingHeaders) + { + Graph<Block> graph; + impl.PruneUnreachableBlocks(); + impl.ComputePredecessorsForBlocks(); + graph = Program.GraphFromImpl(impl); + graph.ComputeLoops(); + if (!graph.Reducible) + { + throw new Exception("Irreducible flow graphs are unsupported."); + } + yieldingHeaders = new HashSet<Block>(); + IEnumerable<Block> sortedHeaders = graph.SortHeadersByDominance(); + foreach (Block header in sortedHeaders) + { + if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header))) + { + yieldingHeaders.Add(header); + } + else if (IsYieldingHeader(graph, header)) + { + yieldingHeaders.Add(header); + } + else + { + continue; + } + } + return graph; + } + + private void SetupRefinementCheck(Implementation impl, + out List<Variable> newLocalVars, + out Dictionary<string, Variable> domainNameToInputVar, out Dictionary<string, Variable> domainNameToLocalVar, out Dictionary<Variable, Variable> ogOldGlobalMap) + { + pc = null; + ok = null; + alpha = null; + beta = null; + frame = null; + + newLocalVars = new List<Variable>(); + Program program = linearTypeChecker.program; + ogOldGlobalMap = new Dictionary<Variable, Variable>(); + foreach (IdentifierExpr ie in globalMods) + { + Variable g = ie.Decl; + LocalVariable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", g.Name), g.TypedIdent.Type)); + ogOldGlobalMap[g] = l; + newLocalVars.Add(l); + } + + Procedure originalProc = implMap[impl].Proc; + ActionInfo actionInfo = moverTypeChecker.procToActionInfo[originalProc]; + if (actionInfo.createdAtLayerNum == this.layerNum) + { + pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); + newLocalVars.Add(pc); + ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool)); + newLocalVars.Add(ok); + Dictionary<Variable, Expr> alwaysMap = new Dictionary<Variable, Expr>(); + for (int i = 0; i < originalProc.InParams.Count; i++) + { + alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]); + } + for (int i = 0; i < originalProc.OutParams.Count; i++) + { + alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]); + } + Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap); + Dictionary<Variable, Expr> foroldMap = new Dictionary<Variable, Expr>(); + foreach (IdentifierExpr ie in globalMods) + { + foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); + } + Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); + frame = new HashSet<Variable>(moverTypeChecker.SharedVariables); + HashSet<Variable> introducedVars = new HashSet<Variable>(); + foreach (Variable v in moverTypeChecker.SharedVariables) + { + if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || + moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum) + { + frame.Remove(v); + } + if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum) + { + introducedVars.Add(v); + } + } + AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; + if (atomicActionInfo == null) + { + beta = Expr.True; + foreach (var v in frame) + { + beta = Expr.And(beta, Expr.Eq(Expr.Ident(v), foroldMap[v])); + } + alpha = Expr.True; + } + else + { + Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, atomicActionInfo, frame, introducedVars)).TransitionRelationCompute(true); + beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); + Expr alphaExpr = Expr.True; + foreach (AssertCmd assertCmd in atomicActionInfo.gate) + { + 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)); + newLocalVars.Add(copy); + ogOldGlobalMap[f] = copy; + } + } + + domainNameToInputVar = new Dictionary<string, Variable>(); + domainNameToLocalVar = new Dictionary<string, Variable>(); + { + int i = impl.InParams.Count - linearTypeChecker.linearDomains.Count; + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + Variable inParam = impl.InParams[i]; + domainNameToInputVar[domainName] = inParam; + Variable l = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name + "_local", inParam.TypedIdent.Type)); + domainNameToLocalVar[domainName] = l; + newLocalVars.Add(l); + i++; + } + } + } + + private void TransformImpl(Implementation impl) + { + HashSet<Block> yieldingHeaders; + Graph<Block> graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders); + + List<Variable> newLocalVars; + Dictionary<string, Variable> domainNameToInputVar, domainNameToLocalVar; + Dictionary<Variable, Variable> ogOldGlobalMap; + SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap); + + List<List<Cmd>> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); + + List<Variable> oldPcs, oldOks; + ProcessLoopHeaders(impl, graph, yieldingHeaders, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap, out oldPcs, out oldOks); + + AddInitialBlock(impl, oldPcs, oldOks, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); + + CreateYieldCheckerImpl(impl, yields); + + impl.LocVars.AddRange(newLocalVars); + impl.LocVars.AddRange(oldPcs); + impl.LocVars.AddRange(oldOks); + + UnifyCallsToYieldProc(impl, ogOldGlobalMap, domainNameToLocalVar); + } + + private void UnifyCallsToYieldProc(Implementation impl, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar) + { + CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar); + Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List<Cmd>(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken)); + List<Block> newBlocks = new List<Block>(); + foreach (Block b in impl.Blocks) + { + TransferCmd transferCmd = b.TransferCmd; + List<Cmd> newCmds = new List<Cmd>(); + for (int i = b.Cmds.Count-1; i >= 0; i--) + { + CallCmd callCmd = b.Cmds[i] as CallCmd; + if (callCmd == null || callCmd.Proc != yieldProc) + { + newCmds.Insert(0, b.Cmds[i]); + } + else + { + Block newBlock = new Block(Token.NoToken, b.Label + i, newCmds, transferCmd); + newCmds = new List<Cmd>(); + transferCmd = new GotoCmd(Token.NoToken, new List<string>(new string[] { newBlock.Label, yieldCheckBlock.Label }), + new List<Block>(new Block[] { newBlock, yieldCheckBlock })); + newBlocks.Add(newBlock); + } + } + b.Cmds = newCmds; + b.TransferCmd = transferCmd; + } + impl.Blocks.AddRange(newBlocks); + impl.Blocks.Add(yieldCheckBlock); + } + + private List<List<Cmd>> CollectAndDesugarYields(Implementation impl, + Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap) + { + // Collect the yield predicates and desugar yields + List<List<Cmd>> yields = new List<List<Cmd>>(); + List<Cmd> cmds = new List<Cmd>(); + foreach (Block b in impl.Blocks) + { + YieldCmd yieldCmd = null; + List<Cmd> newCmds = new List<Cmd>(); + for (int i = 0; i < b.Cmds.Count; i++) + { + Cmd cmd = b.Cmds[i]; + if (cmd is YieldCmd) + { + yieldCmd = (YieldCmd)cmd; + continue; + } + if (yieldCmd != null) + { + PredicateCmd pcmd = cmd as PredicateCmd; + if (pcmd == null) + { + DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); + if (cmds.Count > 0) + { + yields.Add(cmds); + cmds = new List<Cmd>(); + } + yieldCmd = null; + } + else + { + cmds.Add(pcmd); + } + } + + if (cmd is CallCmd) + { + CallCmd callCmd = cmd as CallCmd; + if (yieldingProcs.Contains(callCmd.Proc)) + { + AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + } + if (callCmd.IsAsync) + { + if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name)) + { + asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new List<IdentifierExpr>(), new List<Ensures>()); + } + var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name]; + CallCmd dummyCallCmd = new CallCmd(callCmd.tok, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs, callCmd.Attributes); + dummyCallCmd.Proc = dummyAsyncTargetProc; + newCmds.Add(dummyCallCmd); + } + else + { + newCmds.Add(callCmd); + } + if (yieldingProcs.Contains(callCmd.Proc)) + { + HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd)); + linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars); + + if (!callCmd.IsAsync && globalMods.Count > 0 && pc != null) + { + // assume pc || alpha(i, g); + Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); + assumeExpr.Type = Type.Bool; + newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); + } + + Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + } + else if (cmd is ParCallCmd) + { + ParCallCmd parCallCmd = cmd as ParCallCmd; + AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + DesugarParallelCallCmd(newCmds, parCallCmd); + HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd)); + linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars); + + if (globalMods.Count > 0 && pc != null) + { + // assume pc || alpha(i, g); + Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha); + assumeExpr.Type = Type.Bool; + newCmds.Add(new AssumeCmd(Token.NoToken, assumeExpr)); + } + + Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar); + AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + else + { + newCmds.Add(cmd); + } + } + if (yieldCmd != null) + { + DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar); + if (cmds.Count > 0) + { + yields.Add(cmds); + cmds = new List<Cmd>(); + } + } + if (b.TransferCmd is ReturnCmd) + { + AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + if (pc != null) + { + AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok)); + assertCmd.ErrorData = "Failed to execute atomic action before procedure return"; + newCmds.Add(assertCmd); + } + } + b.Cmds = newCmds; + } + return yields; + } + + private void ProcessLoopHeaders(Implementation impl, Graph<Block> graph, HashSet<Block> yieldingHeaders, + Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap, + out List<Variable> oldPcs, out List<Variable> oldOks) + { + oldPcs = new List<Variable>(); + oldOks = new List<Variable>(); + 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)); + oldPcs.Add(oldPc); + oldOk = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("{0}_{1}", ok.Name, header.Label), Type.Bool)); + oldOks.Add(oldOk); + } + Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar); + foreach (Block pred in header.Predecessors) + { + AddCallToYieldProc(header.tok, pred.Cmds, ogOldGlobalMap, domainNameToLocalVar); + if (pc != null && !graph.BackEdgeNodes(header).Contains(pred)) + { + pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>( + new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }), + new List<Expr>(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) }))); + } + AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + List<Cmd> newCmds = new List<Cmd>(); + if (pc != null) + { + AssertCmd assertCmd; + assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc))); + assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers"; + newCmds.Add(assertCmd); + 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]))); + } + foreach (Variable v in ogOldGlobalMap.Keys) + { + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Eq(Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v])))); + } + newCmds.AddRange(header.Cmds); + header.Cmds = newCmds; + } + } + + private void AddInitialBlock(Implementation impl, List<Variable> oldPcs, List<Variable> oldOks, + Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<Variable, Variable> ogOldGlobalMap) + { + // Add initial block + List<AssignLhs> lhss = new List<AssignLhs>(); + List<Expr> rhss = new List<Expr>(); + if (pc != null) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); + rhss.Add(Expr.False); + foreach (Variable oldPc in oldPcs) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc))); + rhss.Add(Expr.False); + } + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))); + rhss.Add(Expr.False); + foreach (Variable oldOk in oldOks) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk))); + rhss.Add(Expr.False); + } + } + Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]); + } + for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++) + { + Variable v = impl.InParams[i]; + var domainName = linearTypeChecker.FindDomainName(v); + if (domainName == null) continue; + if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue; + var domain = linearTypeChecker.linearDomains[domainName]; + if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue; + Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) }); + domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] }); + } + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName]))); + rhss.Add(domainNameToExpr[domainName]); + } + foreach (Variable g in ogOldGlobalMap.Keys) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g]))); + rhss.Add(Expr.Ident(g)); + } + if (lhss.Count > 0) + { + Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })); + impl.Blocks.Insert(0, initBlock); + } + } + + private void AddYieldProcAndImpl(List<Declaration> decls) + { + if (yieldProc == null) return; + + Program program = linearTypeChecker.program; + List<Variable> inputs = new List<Variable>(); + foreach (string domainName in linearTypeChecker.linearDomains.Keys) + { + var domain = linearTypeChecker.linearDomains[domainName]; + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true); + inputs.Add(f); + } + foreach (IdentifierExpr ie in globalMods) + { + Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); + inputs.Add(f); + } + List<Block> blocks = new List<Block>(); + TransferCmd transferCmd = new ReturnCmd(Token.NoToken); + if (yieldCheckerProcs.Count > 0) + { + List<Block> blockTargets = new List<Block>(); + List<String> labelTargets = new List<String>(); + int labelCount = 0; + foreach (Procedure proc in yieldCheckerProcs) + { + List<Expr> exprSeq = new List<Expr>(); + foreach (Variable v in inputs) + { + exprSeq.Add(Expr.Ident(v)); + } + CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>()); + callCmd.Proc = proc; + string label = string.Format("L_{0}", labelCount++); + Block block = new Block(Token.NoToken, label, new List<Cmd> { callCmd }, new ReturnCmd(Token.NoToken)); + labelTargets.Add(label); + blockTargets.Add(block); + blocks.Add(block); + } + transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets); + } + blocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), transferCmd)); + + var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks); + yieldImpl.Proc = yieldProc; + yieldImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + decls.Add(yieldProc); + decls.Add(yieldImpl); + } + + public static QKeyValue RemoveYieldsAttribute(QKeyValue iter) + { + if (iter == null) return null; + iter.Next = RemoveYieldsAttribute(iter.Next); + return (iter.Key == "yields") ? iter.Next : iter; + } + + public static QKeyValue RemoveMoverAttribute(QKeyValue iter) + { + if (iter == null) return null; + iter.Next = RemoveMoverAttribute(iter.Next); + if (iter.Key == "atomic" || iter.Key == "right" || iter.Key == "left" || iter.Key == "both") + return iter.Next; + else + return iter; + } + + private List<Declaration> Collect() + { + List<Declaration> decls = new List<Declaration>(); + foreach (Procedure proc in yieldCheckerProcs) + { + decls.Add(proc); + } + foreach (Implementation impl in yieldCheckerImpls) + { + decls.Add(impl); + } + foreach (Procedure proc in asyncAndParallelCallDesugarings.Values) + { + decls.Add(proc); + } + AddYieldProcAndImpl(decls); + return decls; + } + + public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls) + { + Program program = linearTypeChecker.program; + foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum })) + { + if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; + + MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, layerNum); + foreach (var proc in program.Procedures) + { + if (!moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue; + Procedure duplicateProc = duplicator.VisitProcedure(proc); + decls.Add(duplicateProc); + } + decls.AddRange(duplicator.impls); + OwickiGries ogTransform = new OwickiGries(linearTypeChecker, moverTypeChecker, duplicator); + foreach (var impl in program.Implementations) + { + if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum < layerNum) + continue; + Implementation duplicateImpl = duplicator.VisitImplementation(impl); + ogTransform.TransformImpl(duplicateImpl); + decls.Add(duplicateImpl); + } + decls.AddRange(ogTransform.Collect()); + } + } + } +} diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 542d3515..c821117a 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -49,6 +49,8 @@ namespace Microsoft.Boogie { public Ensures ensures; public MoverType moverType; + public List<AssertCmd> gate; + public CodeExpr action; public List<AssertCmd> thisGate; public CodeExpr thisAction; public List<Variable> thisInParams; @@ -61,6 +63,8 @@ namespace Microsoft.Boogie public HashSet<Variable> modifiedGlobalVars; public HashSet<Variable> gateUsedGlobalVars; public bool hasAssumeCmd; + public Dictionary<Variable, Expr> thisMap; + public Dictionary<Variable, Expr> thatMap; public bool CommutesWith(AtomicActionInfo actionInfo) { @@ -84,122 +88,137 @@ namespace Microsoft.Boogie public AtomicActionInfo(Procedure proc, Ensures ensures, MoverType moverType, int layerNum, int availableUptoLayerNum) : base(proc, layerNum, availableUptoLayerNum) { - CodeExpr codeExpr = ensures.Condition as CodeExpr; this.ensures = ensures; this.moverType = moverType; + this.gate = new List<AssertCmd>(); + this.action = ensures.Condition as CodeExpr; this.thisGate = new List<AssertCmd>(); - this.thisAction = codeExpr; this.thisInParams = new List<Variable>(); this.thisOutParams = new List<Variable>(); this.thatGate = new List<AssertCmd>(); this.thatInParams = new List<Variable>(); this.thatOutParams = new List<Variable>(); this.hasAssumeCmd = false; - - foreach (Block block in codeExpr.Blocks) + this.thisMap = new Dictionary<Variable, Expr>(); + this.thatMap = new Dictionary<Variable, Expr>(); + + foreach (Block block in this.action.Blocks) { block.Cmds.ForEach(x => this.hasAssumeCmd = this.hasAssumeCmd || x is AssumeCmd); } - var cmds = thisAction.Blocks[0].Cmds; + foreach (Block block in this.action.Blocks) + { + if (block.TransferCmd is ReturnExprCmd) + { + block.TransferCmd = new ReturnCmd(block.TransferCmd.tok); + } + } + + var cmds = this.action.Blocks[0].Cmds; for (int i = 0; i < cmds.Count; i++) { AssertCmd assertCmd = cmds[i] as AssertCmd; if (assertCmd == null) break; - thisGate.Add(assertCmd); + this.gate.Add(assertCmd); cmds[i] = new AssumeCmd(assertCmd.tok, Expr.True); } - Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>(); 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, x.Attributes); - this.thatInParams.Add(y); - map[x] = Expr.Ident(y); + Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), true, x.Attributes); + this.thisInParams.Add(thisx); + this.thisMap[x] = Expr.Ident(thisx); + Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes); + this.thatInParams.Add(thatx); + this.thatMap[x] = Expr.Ident(thatx); } 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, x.Attributes); - this.thatOutParams.Add(y); - map[x] = Expr.Ident(y); + Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), false, x.Attributes); + this.thisOutParams.Add(thisx); + this.thisMap[x] = Expr.Ident(thisx); + Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes); + this.thatOutParams.Add(thatx); + this.thatMap[x] = Expr.Ident(thatx); } + List<Variable> thisLocVars = new List<Variable>(); List<Variable> thatLocVars = new List<Variable>(); - foreach (Variable x in thisAction.LocVars) + foreach (Variable x in this.action.LocVars) { - Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false); - map[x] = Expr.Ident(y); - thatLocVars.Add(y); + Variable thisx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "this_" + x.Name, x.TypedIdent.Type), false); + thisMap[x] = Expr.Ident(thisx); + thisLocVars.Add(thisx); + Variable thatx = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false); + thatMap[x] = Expr.Ident(thatx); + thatLocVars.Add(thatx); } Contract.Assume(proc.TypeParameters.Count == 0); - Substitution subst = Substituter.SubstitutionFromHashtable(map); - foreach (AssertCmd assertCmd in thisGate) + Substitution thisSubst = Substituter.SubstitutionFromHashtable(this.thisMap); + Substitution thatSubst = Substituter.SubstitutionFromHashtable(this.thatMap); + foreach (AssertCmd assertCmd in this.gate) + { + this.thisGate.Add((AssertCmd)Substituter.Apply(thisSubst, assertCmd)); + this.thatGate.Add((AssertCmd)Substituter.Apply(thatSubst, assertCmd)); + } + this.thisAction = new CodeExpr(thisLocVars, SubstituteBlocks(this.action.Blocks, thisSubst, "this_")); + this.thatAction = new CodeExpr(thatLocVars, SubstituteBlocks(this.action.Blocks, thatSubst, "that_")); + { - thatGate.Add((AssertCmd)Substituter.Apply(subst, assertCmd)); + VariableCollector collector = new VariableCollector(); + collector.Visit(this.action); + this.actionUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable)); } + + List<Variable> modifiedVars = new List<Variable>(); + foreach (Block block in this.action.Blocks) + { + block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars)); + } + this.modifiedGlobalVars = new HashSet<Variable>(modifiedVars.Where(x => x is GlobalVariable)); + + { + VariableCollector collector = new VariableCollector(); + this.gate.ForEach(assertCmd => collector.Visit(assertCmd)); + this.gateUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable)); + } + } + + private List<Block> SubstituteBlocks(List<Block> blocks, Substitution subst, string blockLabelPrefix) + { Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>(); - List<Block> thatBlocks = new List<Block>(); - foreach (Block block in thisAction.Blocks) + List<Block> otherBlocks = new List<Block>(); + foreach (Block block in blocks) { List<Cmd> otherCmds = new List<Cmd>(); foreach (Cmd cmd in block.Cmds) { otherCmds.Add(Substituter.Apply(subst, cmd)); } - Block thatBlock = new Block(); - thatBlock.Cmds = otherCmds; - thatBlock.Label = "that_" + block.Label; - block.Label = "this_" + block.Label; - thatBlocks.Add(thatBlock); - blockMap[block] = thatBlock; - if (block.TransferCmd is GotoCmd) - { - GotoCmd gotoCmd = block.TransferCmd as GotoCmd; - for (int i = 0; i < gotoCmd.labelNames.Count; i++) - { - gotoCmd.labelNames[i] = "this_" + gotoCmd.labelNames[i]; - } - } + Block otherBlock = new Block(); + otherBlock.Cmds = otherCmds; + otherBlock.Label = blockLabelPrefix + block.Label; + otherBlocks.Add(otherBlock); + blockMap[block] = otherBlock; } - foreach (Block block in thisAction.Blocks) + foreach (Block block in blocks) { - if (block.TransferCmd is ReturnExprCmd) + if (block.TransferCmd is ReturnCmd) { - block.TransferCmd = new ReturnCmd(block.TransferCmd.tok); blockMap[block].TransferCmd = new ReturnCmd(block.TransferCmd.tok); continue; } - List<Block> thatGotoCmdLabelTargets = new List<Block>(); - List<string> thatGotoCmdLabelNames = new List<string>(); + List<Block> otherGotoCmdLabelTargets = new List<Block>(); + List<string> otherGotoCmdLabelNames = new List<string>(); GotoCmd gotoCmd = block.TransferCmd as GotoCmd; foreach (Block target in gotoCmd.labelTargets) { - thatGotoCmdLabelTargets.Add(blockMap[target]); - thatGotoCmdLabelNames.Add(blockMap[target].Label); + otherGotoCmdLabelTargets.Add(blockMap[target]); + otherGotoCmdLabelNames.Add(blockMap[target].Label); } - blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, thatGotoCmdLabelNames, thatGotoCmdLabelTargets); - } - this.thatAction = new CodeExpr(thatLocVars, thatBlocks); - - { - VariableCollector collector = new VariableCollector(); - collector.Visit(codeExpr); - this.actionUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable)); - } - - List<Variable> modifiedVars = new List<Variable>(); - foreach (Block block in codeExpr.Blocks) - { - block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars)); - } - this.modifiedGlobalVars = new HashSet<Variable>(modifiedVars.Where(x => x is GlobalVariable)); - - { - VariableCollector collector = new VariableCollector(); - this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd)); - this.gateUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable)); + blockMap[block].TransferCmd = new GotoCmd(block.TransferCmd.tok, otherGotoCmdLabelNames, otherGotoCmdLabelTargets); } + return otherBlocks; } } diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect index 8999ae7f..810c93bf 100644 --- a/Test/civl/bar.bpl.expect +++ b/Test/civl/bar.bpl.expect @@ -1,13 +1,13 @@ -bar.bpl(28,3): Error: Non-interference check failed
-Execution trace:
- bar.bpl(7,3): anon0
- (0,0): anon00
- bar.bpl(14,3): inline$Incr_1$0$this_A
- (0,0): inline$Impl_YieldChecker_PC_1$0$L0
-bar.bpl(28,3): Error: Non-interference check failed
-Execution trace:
- bar.bpl(38,3): anon0
- (0,0): anon00
- (0,0): inline$Impl_YieldChecker_PC_1$0$L0
-
-Boogie program verifier finished with 3 verified, 2 errors
+bar.bpl(28,3): Error: Non-interference check failed +Execution trace: + bar.bpl(7,3): anon0 + (0,0): anon00 + bar.bpl(14,3): inline$Incr_1$0$A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 +bar.bpl(28,3): Error: Non-interference check failed +Execution trace: + bar.bpl(38,3): anon0 + (0,0): anon00 + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +Boogie program verifier finished with 3 verified, 2 errors diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect index 0d9de9db..41e30691 100644 --- a/Test/civl/foo.bpl.expect +++ b/Test/civl/foo.bpl.expect @@ -1,8 +1,8 @@ -foo.bpl(30,3): Error: Non-interference check failed
-Execution trace:
- foo.bpl(7,3): anon0
- (0,0): anon00
- foo.bpl(14,3): inline$Incr_1$0$this_A
- (0,0): inline$Impl_YieldChecker_PC_1$0$L0
-
-Boogie program verifier finished with 4 verified, 1 error
+foo.bpl(30,3): Error: Non-interference check failed +Execution trace: + foo.bpl(7,3): anon0 + (0,0): anon00 + foo.bpl(14,3): inline$Incr_1$0$A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect index 588c9c5b..889ee4f2 100644 --- a/Test/civl/parallel1.bpl.expect +++ b/Test/civl/parallel1.bpl.expect @@ -1,8 +1,8 @@ -parallel1.bpl(30,3): Error: Non-interference check failed
-Execution trace:
- parallel1.bpl(7,3): anon0
- (0,0): anon00
- parallel1.bpl(14,3): inline$Incr_1$0$this_A
- (0,0): inline$Impl_YieldChecker_PC_1$0$L0
-
-Boogie program verifier finished with 3 verified, 1 error
+parallel1.bpl(30,3): Error: Non-interference check failed +Execution trace: + parallel1.bpl(7,3): anon0 + (0,0): anon00 + parallel1.bpl(14,3): inline$Incr_1$0$A + (0,0): inline$Impl_YieldChecker_PC_1$0$L0 + +Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect index 0b0c936e..fcef7e58 100644 --- a/Test/civl/t1.bpl.expect +++ b/Test/civl/t1.bpl.expect @@ -1,9 +1,9 @@ -t1.bpl(65,5): Error: Non-interference check failed
-Execution trace:
- t1.bpl(84,13): anon0
- (0,0): anon05
- (0,0): inline$SetG_1$0$Entry
- t1.bpl(25,21): inline$SetG_1$0$this_A
- (0,0): inline$Impl_YieldChecker_A_1$0$L1
-
-Boogie program verifier finished with 4 verified, 1 error
+t1.bpl(65,5): Error: Non-interference check failed +Execution trace: + t1.bpl(84,13): anon0 + (0,0): anon05 + (0,0): inline$SetG_1$0$Entry + t1.bpl(25,21): inline$SetG_1$0$A + (0,0): inline$Impl_YieldChecker_A_1$0$L1 + +Boogie program verifier finished with 4 verified, 1 error |