From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Concurrency/MoverCheck.cs | 1320 +++++++++++++++++++------------------- 1 file changed, 672 insertions(+), 648 deletions(-) (limited to 'Source/Concurrency/MoverCheck.cs') diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs index 971e7271..732bcaa4 100644 --- a/Source/Concurrency/MoverCheck.cs +++ b/Source/Concurrency/MoverCheck.cs @@ -1,649 +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 decls; - HashSet> commutativityCheckerCache; - HashSet> gatePreservationCheckerCache; - HashSet> failurePreservationCheckerCache; - private MoverCheck(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) - { - this.linearTypeChecker = linearTypeChecker; - this.moverTypeChecker = moverTypeChecker; - this.decls = decls; - this.commutativityCheckerCache = new HashSet>(); - this.gatePreservationCheckerCache = new HashSet>(); - this.failurePreservationCheckerCache = new HashSet>(); - } - - public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List decls) - { - if (moverTypeChecker.procToActionInfo.Count == 0) - return; - - List sortedByCreatedLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo)); - sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; }); - List sortedByAvailableUptoLayerNum = new List(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo)); - sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; }); - - Dictionary> pools = new Dictionary>(); - int indexIntoSortedByCreatedLayerNum = 0; - int indexIntoSortedByAvailableUptoLayerNum = 0; - HashSet currPool = new HashSet(); - while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count) - { - var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum; - pools[currLayerNum] = new HashSet(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 (ActionInfo actionInfo in moverTypeChecker.procToActionInfo.Values) - { - AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; - if (atomicActionInfo != null && 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 cmdStack; - private List paths; - private HashSet frame; - private HashSet postExistVars; - - public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet frame, HashSet postExistVars) - { - this.postExistVars = postExistVars; - this.frame = frame; - TransitionRelationComputationHelper(program, null, second); - } - - public TransitionRelationComputation(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet frame, HashSet 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(); - this.paths = new List(); - List havocVars = new List(); - 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 map, ref List pathExprs, ref Dictionary varToExpr) - { - Substitution subst = Substituter.SubstitutionFromHashtable(map); - List oldPathExprs = pathExprs; - pathExprs = new List(); - foreach (Expr pathExpr in oldPathExprs) - { - pathExprs.Add(Substituter.Apply(subst, pathExpr)); - } - Dictionary oldVarToExpr = varToExpr; - varToExpr = new Dictionary(); - foreach (Variable v in oldVarToExpr.Keys) - { - varToExpr[v] = Substituter.Apply(subst, oldVarToExpr[v]); - } - } - - struct PathInfo - { - public HashSet existsVars; - public Dictionary varToExpr; - public List pathExprs; - - public PathInfo(HashSet existsVars, Dictionary varToExpr, List pathExprs) - { - this.existsVars = existsVars; - this.varToExpr = varToExpr; - this.pathExprs = pathExprs; - } - } - - private void FlattenAnd(Expr x, List 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 existsVars = new HashSet(); - Dictionary varToExpr = new Dictionary(); - 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 pathExprs = new List(); - 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 map = new Dictionary(); - 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 map = new Dictionary(); - 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 existsVars = path.existsVars; - Dictionary existsMap = new Dictionary(); - - Dictionary varToExpr = path.varToExpr; - foreach (Variable v in varToExpr.Keys) - { - if (postExistVars.Contains(v)) continue; - IdentifierExpr ie = varToExpr[v] as IdentifierExpr; - if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl)) - { - 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 pathExprs = new List(); - 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(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 havocVars = new List(); - first.thatOutParams.ForEach(v => havocVars.Add(Expr.Ident(v))); - first.thatAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v))); - if (havocVars.Count > 0) - { - HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars); - 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 CloneBlocks(List blocks) - { - Dictionary blockMap = new Dictionary(); - List otherBlocks = new List(); - foreach (Block block in blocks) - { - List otherCmds = new List(); - 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 otherGotoCmdLabelTargets = new List(); - List otherGotoCmdLabelNames = new List(); - 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 DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet frame) - { - List requires = new List(); - Dictionary> domainNameToScope = new Dictionary>(); - foreach (var domainName in linearTypeChecker.linearDomains.Keys) - { - domainNameToScope[domainName] = new HashSet(); - } - 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 actionPair = new Tuple(first, second); - if (commutativityCheckerCache.Contains(actionPair)) - return; - commutativityCheckerCache.Add(actionPair); - - List inputs = new List(); - inputs.AddRange(first.thatInParams); - inputs.AddRange(second.thisInParams); - List outputs = new List(); - outputs.AddRange(first.thatOutParams); - outputs.AddRange(second.thisOutParams); - List locals = new List(); - locals.AddRange(first.thatAction.LocVars); - locals.AddRange(second.thisAction.LocVars); - List firstBlocks = CloneBlocks(first.thatAction.Blocks); - List secondBlocks = CloneBlocks(second.thisAction.Blocks); - foreach (Block b in firstBlocks) - { - if (b.TransferCmd is ReturnCmd) - { - List bs = new List(); - bs.Add(secondBlocks[0]); - List ls = new List(); - ls.Add(secondBlocks[0].Label); - b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs); - } - } - List blocks = new List(); - blocks.AddRange(firstBlocks); - blocks.AddRange(secondBlocks); - HashSet frame = new HashSet(); - frame.UnionWith(first.gateUsedGlobalVars); - frame.UnionWith(first.actionUsedGlobalVars); - frame.UnionWith(second.gateUsedGlobalVars); - frame.UnionWith(second.actionUsedGlobalVars); - List requires = DisjointnessRequires(program, first, second, frame); - foreach (AssertCmd assertCmd in first.thatGate) - requires.Add(new Requires(false, assertCmd.Expr)); - foreach (AssertCmd assertCmd in second.thisGate) - requires.Add(new Requires(false, assertCmd.Expr)); - List ensures = new List(); - Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet())).TransitionRelationCompute(); - Ensures ensureCheck = new Ensures(false, transitionRelation); - ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name); - ensures.Add(ensureCheck); - string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name); - List globalVars = new List(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); - Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); - Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), 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 actionPair = new Tuple(first, second); - if (gatePreservationCheckerCache.Contains(actionPair)) - return; - gatePreservationCheckerCache.Add(actionPair); - - List inputs = new List(); - inputs.AddRange(first.thatInParams); - inputs.AddRange(second.thisInParams); - List outputs = new List(); - outputs.AddRange(first.thatOutParams); - outputs.AddRange(second.thisOutParams); - List locals = new List(); - locals.AddRange(second.thisAction.LocVars); - List secondBlocks = CloneBlocks(second.thisAction.Blocks); - HashSet frame = new HashSet(); - frame.UnionWith(first.gateUsedGlobalVars); - frame.UnionWith(second.gateUsedGlobalVars); - frame.UnionWith(second.actionUsedGlobalVars); - List requires = DisjointnessRequires(program, first, second, frame); - List ensures = new List(); - foreach (AssertCmd assertCmd in first.thatGate) - { - 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 globalVars = new List(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); - Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); - Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), 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 actionPair = new Tuple(first, second); - if (failurePreservationCheckerCache.Contains(actionPair)) - return; - failurePreservationCheckerCache.Add(actionPair); - - List inputs = new List(); - inputs.AddRange(first.thatInParams); - inputs.AddRange(second.thisInParams); - List outputs = new List(); - outputs.AddRange(first.thatOutParams); - outputs.AddRange(second.thisOutParams); - List locals = new List(); - locals.AddRange(second.thisAction.LocVars); - List secondBlocks = CloneBlocks(second.thisAction.Blocks); - HashSet frame = new HashSet(); - frame.UnionWith(first.gateUsedGlobalVars); - frame.UnionWith(second.gateUsedGlobalVars); - frame.UnionWith(second.actionUsedGlobalVars); - List requires = DisjointnessRequires(program, first, second, frame); - Expr gateExpr = Expr.True; - foreach (AssertCmd assertCmd in first.thatGate) - { - 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 = new List(); - 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 globalVars = new List(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); - Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); - Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, outputs, locals, secondBlocks); - impl.Proc = proc; - this.decls.Add(impl); - this.decls.Add(proc); - } - - private void CreateNonBlockingChecker(Program program, AtomicActionInfo second) - { - List inputs = new List(); - inputs.AddRange(second.thisInParams); - - HashSet frame = new HashSet(); - frame.UnionWith(second.gateUsedGlobalVars); - frame.UnionWith(second.actionUsedGlobalVars); - List requires = DisjointnessRequires(program, null, second, frame); - foreach (AssertCmd assertCmd in second.thisGate) - { - requires.Add(new Requires(false, assertCmd.Expr)); - } - HashSet postExistVars = new HashSet(); - postExistVars.UnionWith(frame); - postExistVars.UnionWith(second.thisOutParams); - Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute(); - List ensures = new List(); - Ensures ensureCheck = new Ensures(false, ensuresExpr); - ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name); - ensures.Add(ensureCheck); - - List blocks = new List(); - blocks.Add(new Block(Token.NoToken, "L", new List(), new ReturnCmd(Token.NoToken))); - string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name); - List globalVars = new List(); - moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); - Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, new List(), requires, globalVars, ensures); - Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, new List(), new List(), blocks); - impl.Proc = proc; - this.decls.Add(impl); - this.decls.Add(proc); - } - } +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; + CivlTypeChecker civlTypeChecker; + List decls; + HashSet> commutativityCheckerCache; + HashSet> gatePreservationCheckerCache; + HashSet> failurePreservationCheckerCache; + private MoverCheck(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) + { + this.linearTypeChecker = linearTypeChecker; + this.civlTypeChecker = civlTypeChecker; + this.decls = decls; + this.commutativityCheckerCache = new HashSet>(); + this.gatePreservationCheckerCache = new HashSet>(); + this.failurePreservationCheckerCache = new HashSet>(); + } + + public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) + { + if (civlTypeChecker.procToActionInfo.Count == 0) + return; + + List sortedByCreatedLayerNum = new List(civlTypeChecker.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 sortedByAvailableUptoLayerNum = new List(civlTypeChecker.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> pools = new Dictionary>(); + int indexIntoSortedByCreatedLayerNum = 0; + int indexIntoSortedByAvailableUptoLayerNum = 0; + HashSet currPool = new HashSet(); + while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count) + { + var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum; + pools[currLayerNum] = new HashSet(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 = civlTypeChecker.program; + MoverCheck moverChecking = new MoverCheck(linearTypeChecker, civlTypeChecker, 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 cmdStack; + private List paths; + private HashSet frame; + private HashSet postExistVars; + + public TransitionRelationComputation(Program program, AtomicActionInfo second, HashSet frame, HashSet postExistVars) + { + this.postExistVars = postExistVars; + this.frame = frame; + TransitionRelationComputationHelper(program, null, second); + } + + public TransitionRelationComputation(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet frame, HashSet 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(); + this.paths = new List(); + List havocVars = new List(); + 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 map, ref List pathExprs, ref Dictionary varToExpr) + { + Substitution subst = Substituter.SubstitutionFromHashtable(map); + List oldPathExprs = pathExprs; + pathExprs = new List(); + foreach (Expr pathExpr in oldPathExprs) + { + pathExprs.Add(Substituter.Apply(subst, pathExpr)); + } + Dictionary oldVarToExpr = varToExpr; + varToExpr = new Dictionary(); + foreach (Variable v in oldVarToExpr.Keys) + { + varToExpr[v] = Substituter.Apply(subst, oldVarToExpr[v]); + } + } + + struct PathInfo + { + public HashSet existsVars; + public Dictionary varToExpr; + public List pathExprs; + + public PathInfo(HashSet existsVars, Dictionary varToExpr, List pathExprs) + { + this.existsVars = existsVars; + this.varToExpr = varToExpr; + this.pathExprs = pathExprs; + } + } + + private void FlattenAnd(Expr x, List 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 existsVars = new HashSet(); + Dictionary varToExpr = new Dictionary(); + 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 pathExprs = new List(); + 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 map = new Dictionary(); + 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 map = new Dictionary(); + 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 existsVars = path.existsVars; + Dictionary existsMap = new Dictionary(); + + Dictionary varToExpr = path.varToExpr; + foreach (Variable v in varToExpr.Keys) + { + if (postExistVars.Contains(v)) continue; + IdentifierExpr ie = varToExpr[v] as IdentifierExpr; + if (ie != null && !existsMap.ContainsKey(ie.Decl) && existsVars.Contains(ie.Decl)) + { + 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 pathExprs = new List(); + 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(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 invertedMap = new Dictionary(); + 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 havocVars = new List(); + first.thatOutParams.ForEach(v => havocVars.Add(Expr.Ident(v))); + first.thatAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v))); + if (havocVars.Count > 0) + { + HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars); + 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 CloneBlocks(List blocks) + { + Dictionary blockMap = new Dictionary(); + List otherBlocks = new List(); + foreach (Block block in blocks) + { + List otherCmds = new List(); + 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 otherGotoCmdLabelTargets = new List(); + List otherGotoCmdLabelNames = new List(); + 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 DisjointnessRequires(Program program, AtomicActionInfo first, AtomicActionInfo second, HashSet frame) + { + List requires = new List(); + Dictionary> domainNameToScope = new Dictionary>(); + foreach (var domainName in linearTypeChecker.linearDomains.Keys) + { + domainNameToScope[domainName] = new HashSet(); + } + 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 actionPair = new Tuple(first, second); + if (commutativityCheckerCache.Contains(actionPair)) + return; + commutativityCheckerCache.Add(actionPair); + + List inputs = new List(); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); + List outputs = new List(); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); + List locals = new List(); + locals.AddRange(first.thatAction.LocVars); + locals.AddRange(second.thisAction.LocVars); + List firstBlocks = CloneBlocks(first.thatAction.Blocks); + List secondBlocks = CloneBlocks(second.thisAction.Blocks); + foreach (Block b in firstBlocks) + { + if (b.TransferCmd is ReturnCmd) + { + List bs = new List(); + bs.Add(secondBlocks[0]); + List ls = new List(); + ls.Add(secondBlocks[0].Label); + b.TransferCmd = new GotoCmd(Token.NoToken, ls, bs); + } + } + List blocks = new List(); + blocks.AddRange(firstBlocks); + blocks.AddRange(secondBlocks); + HashSet frame = new HashSet(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(first.actionUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List requires = DisjointnessRequires(program, first, second, frame); + foreach (AssertCmd assertCmd in first.thatGate) + requires.Add(new Requires(false, assertCmd.Expr)); + foreach (AssertCmd assertCmd in second.thisGate) + requires.Add(new Requires(false, assertCmd.Expr)); + List ensures = new List(); + Expr transitionRelation = (new TransitionRelationComputation(program, first, second, frame, new HashSet())).TransitionRelationCompute(); + Ensures ensureCheck = new Ensures(false, transitionRelation); + ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name); + ensures.Add(ensureCheck); + string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name); + List globalVars = new List(); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), 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 actionPair = new Tuple(first, second); + if (gatePreservationCheckerCache.Contains(actionPair)) + return; + gatePreservationCheckerCache.Add(actionPair); + + List inputs = new List(); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); + List outputs = new List(); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); + List locals = new List(); + locals.AddRange(second.thisAction.LocVars); + List secondBlocks = CloneBlocks(second.thisAction.Blocks); + HashSet frame = new HashSet(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List requires = DisjointnessRequires(program, first, second, frame); + List ensures = new List(); + foreach (AssertCmd assertCmd in first.thatGate) + { + 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 globalVars = new List(); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), 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 actionPair = new Tuple(first, second); + if (failurePreservationCheckerCache.Contains(actionPair)) + return; + failurePreservationCheckerCache.Add(actionPair); + + List inputs = new List(); + inputs.AddRange(first.thatInParams); + inputs.AddRange(second.thisInParams); + List outputs = new List(); + outputs.AddRange(first.thatOutParams); + outputs.AddRange(second.thisOutParams); + List locals = new List(); + locals.AddRange(second.thisAction.LocVars); + List secondBlocks = CloneBlocks(second.thisAction.Blocks); + HashSet frame = new HashSet(); + frame.UnionWith(first.gateUsedGlobalVars); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List requires = DisjointnessRequires(program, first, second, frame); + Expr gateExpr = Expr.True; + foreach (AssertCmd assertCmd in first.thatGate) + { + 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 = new List(); + 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 globalVars = new List(); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, outputs, requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, outputs, locals, secondBlocks); + impl.Proc = proc; + this.decls.Add(impl); + this.decls.Add(proc); + } + + private void CreateNonBlockingChecker(Program program, AtomicActionInfo second) + { + List inputs = new List(); + inputs.AddRange(second.thisInParams); + + HashSet frame = new HashSet(); + frame.UnionWith(second.gateUsedGlobalVars); + frame.UnionWith(second.actionUsedGlobalVars); + List requires = DisjointnessRequires(program, null, second, frame); + foreach (AssertCmd assertCmd in second.thisGate) + { + requires.Add(new Requires(false, assertCmd.Expr)); + } + HashSet postExistVars = new HashSet(); + postExistVars.UnionWith(frame); + postExistVars.UnionWith(second.thisOutParams); + Expr ensuresExpr = (new TransitionRelationComputation(program, second, frame, postExistVars)).TransitionRelationCompute(); + List ensures = new List(); + Ensures ensureCheck = new Ensures(false, ensuresExpr); + ensureCheck.ErrorData = string.Format("{0} is blocking", second.proc.Name); + ensures.Add(ensureCheck); + + List blocks = new List(); + blocks.Add(new Block(Token.NoToken, "L", new List(), new ReturnCmd(Token.NoToken))); + string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name); + List globalVars = new List(); + civlTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x))); + Procedure proc = new Procedure(Token.NoToken, checkerName, new List(), inputs, new List(), requires, globalVars, ensures); + Implementation impl = new Implementation(Token.NoToken, checkerName, new List(), inputs, new List(), new List(), blocks); + impl.Proc = proc; + this.decls.Add(impl); + this.decls.Add(proc); + } + } } \ No newline at end of file -- cgit v1.2.3