From 4e9171d2b0dad5ea640ad781461a30910fbd73e5 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 15 Jun 2015 14:19:46 -0700 Subject: adding z3name option --- Source/Core/CommandLineOptions.cs | 10 +++++++++- Source/Provers/SMTLib/Z3.cs | 3 ++- 2 files changed, 11 insertions(+), 2 deletions(-) (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index b57ea02a..309aab0e 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -484,6 +484,7 @@ namespace Microsoft.Boogie { public bool SimplifyLogFileAppend = false; public bool SoundnessSmokeTest = false; public string Z3ExecutablePath = null; + public string Z3ExecutableName = null; public string CVC4ExecutablePath = null; public int KInductionDepth = -1; @@ -1551,8 +1552,15 @@ namespace Microsoft.Boogie { Z3ExecutablePath = args[ps.i]; } return true; + // This sets name of z3 binary boogie binary directory, not path + case "z3name": + if (ps.ConfirmArgumentCount(1)) + { + Z3ExecutableName = args[ps.i]; + } + return true; - case "cvc4exe": + case "cvc4exe": if (ps.ConfirmArgumentCount(1)) { CVC4ExecutablePath = args[ps.i]; } diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index ffa4e0cb..bbc23917 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -52,7 +52,8 @@ namespace Microsoft.Boogie.SMTLib return; } - var proverExe = "z3.exe"; + var proverExe = CommandLineOptions.Clo.Z3ExecutableName; + proverExe = proverExe == null ? "z3.exe" : proverExe; if (_proverPath == null) { -- cgit v1.2.3 From e60e05a198970d64ea50b99bc605240d7a04e4cc Mon Sep 17 00:00:00 2001 From: qadeer Date: Mon, 15 Jun 2015 20:45:32 -0700 Subject: fixed bug reported by Chris --- Source/Core/DeadVarElim.cs | 3513 ++++++++++++++++++++++--------------------- Test/civl/chris4.bpl | 16 + Test/civl/chris4.bpl.expect | 5 + 3 files changed, 1782 insertions(+), 1752 deletions(-) create mode 100644 Test/civl/chris4.bpl create mode 100644 Test/civl/chris4.bpl.expect (limited to 'Source') diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 0feb5e35..fc39debb 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -1,1753 +1,1762 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using Microsoft.Boogie.GraphUtil; -using System.Diagnostics.Contracts; - - -namespace Microsoft.Boogie { - public class UnusedVarEliminator : VariableCollector { - public static void Eliminate(Program program) { - Contract.Requires(program != null); - UnusedVarEliminator elim = new UnusedVarEliminator(); - elim.Visit(program); - } - - private UnusedVarEliminator() - : base() { - - } - - public override Implementation VisitImplementation(Implementation node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - //Console.WriteLine("Procedure {0}", node.Name); - Implementation/*!*/ impl = base.VisitImplementation(node); - Contract.Assert(impl != null); - //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length); - List/*!*/ vars = new List(); - foreach (Variable/*!*/ var in impl.LocVars) { - Contract.Assert(var != null); - if (_usedVars.Contains(var)) - vars.Add(var); - } - impl.LocVars = vars; - //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length); - //Console.WriteLine("---------------------------------"); - _usedVars.Clear(); - return impl; - } - } - - public class ModSetCollector : ReadOnlyVisitor { - private Procedure enclosingProc; - private Dictionary/*!*/>/*!*/ modSets; - private HashSet yieldingProcs; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullDictionaryAndValues(modSets)); - Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v))); - } - - public ModSetCollector() { - modSets = new Dictionary/*!*/>(); - yieldingProcs = new HashSet(); - } - - private bool moreProcessingRequired; - - public void DoModSetAnalysis(Program program) { - Contract.Requires(program != null); - - if (CommandLineOptions.Clo.Trace) - { -// Console.WriteLine(); -// Console.WriteLine("Running modset analysis ..."); -// int procCount = 0; -// foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) -// { -// Contract.Assert(decl != null); -// if (decl is Procedure) -// procCount++; -// } -// Console.WriteLine("Number of procedures = {0}", procCount);*/ - } - - HashSet implementedProcs = new HashSet(); - foreach (var impl in program.Implementations) { - if (impl.Proc != null) - implementedProcs.Add(impl.Proc); - } - foreach (var proc in program.Procedures) { - if (!implementedProcs.Contains(proc)) - { - enclosingProc = proc; - foreach (var expr in proc.Modifies) - { - Contract.Assert(expr != null); - ProcessVariable(expr.Decl); - } - enclosingProc = null; - } - else - { - modSets.Add(proc, new HashSet()); - } - } - - moreProcessingRequired = true; - while (moreProcessingRequired) { - moreProcessingRequired = false; - this.Visit(program); - } - - foreach (Procedure x in modSets.Keys) - { - x.Modifies = new List(); - foreach (Variable v in modSets[x]) - { - x.Modifies.Add(new IdentifierExpr(v.tok, v)); - } - } - foreach (Procedure x in yieldingProcs) - { - if (!QKeyValue.FindBoolAttribute(x.Attributes, "yields")) - { - x.AddAttribute("yields"); - } - } - -#if DEBUG_PRINT - Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); - foreach (Procedure/*!*/ x in modSets.Keys) { - Contract.Assert(x != null); - Console.Write("{0} : ", x.Name); - bool first = true; - foreach (Variable/*!*/ y in modSets[x]) { - Contract.Assert(y != null); - if (first) - first = false; - else - Console.Write(", "); - Console.Write("{0}", y.Name); - } - Console.WriteLine(""); - } -#endif - } - - public override Implementation VisitImplementation(Implementation node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - enclosingProc = node.Proc; - Implementation/*!*/ ret = base.VisitImplementation(node); - Contract.Assert(ret != null); - enclosingProc = null; - - return ret; - } - public override YieldCmd VisitYieldCmd(YieldCmd node) - { - if (!yieldingProcs.Contains(enclosingProc)) - { - yieldingProcs.Add(enclosingProc); - moreProcessingRequired = true; - } - return base.VisitYieldCmd(node); - } - public override Cmd VisitAssignCmd(AssignCmd assignCmd) { - //Contract.Requires(assignCmd != null); - Contract.Ensures(Contract.Result() != null); - Cmd ret = base.VisitAssignCmd(assignCmd); - foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { - Contract.Assert(lhs != null); - ProcessVariable(lhs.DeepAssignedVariable); - } - return ret; - } - public override Cmd VisitHavocCmd(HavocCmd havocCmd) { - //Contract.Requires(havocCmd != null); - Contract.Ensures(Contract.Result() != null); - Cmd ret = base.VisitHavocCmd(havocCmd); - foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { - Contract.Assert(expr != null); - ProcessVariable(expr.Decl); - } - return ret; - } - public override Cmd VisitCallCmd(CallCmd callCmd) { - //Contract.Requires(callCmd != null); - Contract.Ensures(Contract.Result() != null); - Cmd ret = base.VisitCallCmd(callCmd); - foreach (IdentifierExpr ie in callCmd.Outs) - { - if (ie != null) ProcessVariable(ie.Decl); - } - Procedure callee = callCmd.Proc; - if (callee == null) - return ret; - if (modSets.ContainsKey(callee)) { - foreach (Variable var in modSets[callee]) { - ProcessVariable(var); - } - } - if (!yieldingProcs.Contains(enclosingProc) && (yieldingProcs.Contains(callCmd.Proc) || callCmd.IsAsync)) - { - yieldingProcs.Add(enclosingProc); - moreProcessingRequired = true; - } - if (callCmd.IsAsync) - { - if (!yieldingProcs.Contains(callCmd.Proc)) - { - yieldingProcs.Add(callCmd.Proc); - moreProcessingRequired = true; - } - } - return ret; - } - public override Cmd VisitParCallCmd(ParCallCmd node) - { - //Contract.Requires(callCmd != null); - Contract.Ensures(Contract.Result() != null); - Cmd ret = base.VisitParCallCmd(node); - if (!yieldingProcs.Contains(enclosingProc)) - { - yieldingProcs.Add(enclosingProc); - moreProcessingRequired = true; - } - foreach (CallCmd callCmd in node.CallCmds) - { - if (!yieldingProcs.Contains(callCmd.Proc)) - { - yieldingProcs.Add(callCmd.Proc); - moreProcessingRequired = true; - } - } - return ret; - } - private void ProcessVariable(Variable var) { - Procedure/*!*/ localProc = cce.NonNull(enclosingProc); - if (var == null) - return; - if (!(var is GlobalVariable)) - return; - if (!modSets.ContainsKey(localProc)) { - modSets[localProc] = new HashSet(); - } - if (modSets[localProc].Contains(var)) - return; - moreProcessingRequired = true; - modSets[localProc].Add(var); - } - public override Expr VisitCodeExpr(CodeExpr node) { - // don't go into the code expression, since it can only modify variables local to the code expression, - // and the mod-set analysis is interested in global variables - return node; - } - } - - public class MutableVariableCollector : ReadOnlyVisitor - { - public HashSet UsedVariables = new HashSet(); - - public void AddUsedVariables(HashSet usedVariables) - { - Contract.Requires(usedVariables != null); - - foreach (var v in usedVariables) - { - UsedVariables.Add(v); - } - } - - public override Expr VisitIdentifierExpr(IdentifierExpr node) - { - Contract.Ensures(Contract.Result() != null); - - if (node.Decl != null && node.Decl.IsMutable) - { - UsedVariables.Add(node.Decl); - } - return base.VisitIdentifierExpr(node); - } - } - - public class VariableCollector : ReadOnlyVisitor { - protected HashSet/*!*/ _usedVars; - public IEnumerable/*!*/ usedVars - { - get - { - return _usedVars.AsEnumerable(); - } - } - - protected HashSet/*!*/ _oldVarsUsed; - public IEnumerable/*!*/ oldVarsUsed - { - get - { - return _oldVarsUsed.AsEnumerable(); - } - } - - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(_usedVars)); - Contract.Invariant(cce.NonNullElements(_oldVarsUsed)); - } - - int insideOldExpr; - - public VariableCollector() { - _usedVars = new System.Collections.Generic.HashSet(); - _oldVarsUsed = new System.Collections.Generic.HashSet(); - insideOldExpr = 0; - } - - public override Expr VisitOldExpr(OldExpr node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - insideOldExpr++; - node.Expr = this.VisitExpr(node.Expr); - insideOldExpr--; - return node; - } - - public override Expr VisitIdentifierExpr(IdentifierExpr node) { - //Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - if (node.Decl != null) { - _usedVars.Add(node.Decl); - if (insideOldExpr > 0) { - _oldVarsUsed.Add(node.Decl); - } - } - return node; - } - } - - public class BlockCoalescer : ReadOnlyVisitor { - public static void CoalesceBlocks(Program program) { - Contract.Requires(program != null); - BlockCoalescer blockCoalescer = new BlockCoalescer(); - blockCoalescer.Visit(program); - } - - private static HashSet/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) { - Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - HashSet visitedBlocks = new HashSet(); - HashSet multiPredBlocks = new HashSet(); - Stack dfsStack = new Stack(); - dfsStack.Push(impl.Blocks[0]); - while (dfsStack.Count > 0) { - Block/*!*/ b = dfsStack.Pop(); - Contract.Assert(b != null); - if (visitedBlocks.Contains(b)) { - multiPredBlocks.Add(b); - continue; - } - visitedBlocks.Add(b); - if (b.TransferCmd == null) - continue; - if (b.TransferCmd is ReturnCmd) - continue; - Contract.Assert(b.TransferCmd is GotoCmd); - GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; - if (gotoCmd.labelTargets == null) - continue; - foreach (Block/*!*/ succ in gotoCmd.labelTargets) { - Contract.Assert(succ != null); - dfsStack.Push(succ); - } - } - return multiPredBlocks; - } - - public override Implementation VisitImplementation(Implementation impl) { - //Contract.Requires(impl != null); - Contract.Ensures(Contract.Result() != null); - //Console.WriteLine("Procedure {0}", impl.Name); - //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count); - - HashSet multiPredBlocks = ComputeMultiPredecessorBlocks(impl); - Contract.Assert(cce.NonNullElements(multiPredBlocks)); - HashSet visitedBlocks = new HashSet(); - HashSet removedBlocks = new HashSet(); - Stack dfsStack = new Stack(); - dfsStack.Push(impl.Blocks[0]); - while (dfsStack.Count > 0) { - Block/*!*/ b = dfsStack.Pop(); - Contract.Assert(b != null); - if (visitedBlocks.Contains(b)) - continue; - visitedBlocks.Add(b); - if (b.TransferCmd == null) - continue; - if (b.TransferCmd is ReturnCmd) - continue; - Contract.Assert(b.TransferCmd is GotoCmd); - GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; - if (gotoCmd.labelTargets == null) - continue; - if (gotoCmd.labelTargets.Count == 1) { - Block/*!*/ succ = cce.NonNull(gotoCmd.labelTargets[0]); - if (!multiPredBlocks.Contains(succ)) { - foreach (Cmd/*!*/ cmd in succ.Cmds) { - Contract.Assert(cmd != null); - b.Cmds.Add(cmd); - } - b.TransferCmd = succ.TransferCmd; - if (!b.tok.IsValid && succ.tok.IsValid) { - b.tok = succ.tok; - b.Label = succ.Label; - } - removedBlocks.Add(succ); - dfsStack.Push(b); - visitedBlocks.Remove(b); - continue; - } - } - foreach (Block/*!*/ succ in gotoCmd.labelTargets) { - Contract.Assert(succ != null); - dfsStack.Push(succ); - } - } - - List newBlocks = new List(); - foreach (Block/*!*/ b in impl.Blocks) { - Contract.Assert(b != null); - if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b)) { - newBlocks.Add(b); - } - } - impl.Blocks = newBlocks; - - // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count); - return impl; - } - } - - public class LiveVariableAnalysis { - public static void ClearLiveVariables(Implementation impl) { - Contract.Requires(impl != null); - foreach (Block/*!*/ block in impl.Blocks) { - Contract.Assert(block != null); - block.liveVarsBefore = null; - } - } - - public static void ComputeLiveVariables(Implementation impl) { - Contract.Requires(impl != null); - Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis"); - Graph dag = new Graph(); - dag.AddSource(cce.NonNull(impl.Blocks[0])); // there is always at least one node in the graph - foreach (Block b in impl.Blocks) { - GotoCmd gtc = b.TransferCmd as GotoCmd; - if (gtc != null) { - Contract.Assume(gtc.labelTargets != null); - foreach (Block/*!*/ dest in gtc.labelTargets) { - Contract.Assert(dest != null); - dag.AddEdge(dest, b); - } - } - } - - IEnumerable sortedNodes; - if (CommandLineOptions.Clo.ModifyTopologicalSorting) { - sortedNodes = dag.TopologicalSort(true); - } else { - sortedNodes = dag.TopologicalSort(); - } - foreach (Block/*!*/ block in sortedNodes) { - Contract.Assert(block != null); - HashSet/*!*/ liveVarsAfter = new HashSet(); - - // The injected assumption variables should always be considered to be live. - foreach (var v in impl.InjectedAssumptionVariables.Concat(impl.DoomedInjectedAssumptionVariables)) - { - liveVarsAfter.Add(v); - } - - if (block.TransferCmd is GotoCmd) { - GotoCmd gotoCmd = (GotoCmd)block.TransferCmd; - if (gotoCmd.labelTargets != null) { - foreach (Block/*!*/ succ in gotoCmd.labelTargets) { - Contract.Assert(succ != null); - Contract.Assert(succ.liveVarsBefore != null); - liveVarsAfter.UnionWith(succ.liveVarsBefore); - } - } - } - - List cmds = block.Cmds; - int len = cmds.Count; - for (int i = len - 1; i >= 0; i--) { - if (cmds[i] is CallCmd) { - Procedure/*!*/ proc = cce.NonNull(cce.NonNull((CallCmd/*!*/)cmds[i]).Proc); - if (InterProcGenKill.HasSummary(proc.Name)) { - liveVarsAfter = - InterProcGenKill.PropagateLiveVarsAcrossCall(cce.NonNull((CallCmd/*!*/)cmds[i]), liveVarsAfter); - continue; - } - } - Propagate(cmds[i], liveVarsAfter); - } - - block.liveVarsBefore = liveVarsAfter; - - } - } - - // perform in place update of liveSet - public static void Propagate(Cmd cmd, HashSet/*!*/ liveSet) { - Contract.Requires(cmd != null); - Contract.Requires(cce.NonNullElements(liveSet)); - if (cmd is AssignCmd) { - AssignCmd/*!*/ assignCmd = (AssignCmd)cce.NonNull(cmd); - // I must first iterate over all the targets and remove the live ones. - // After the removals are done, I must add the variables referred on - // the right side of the removed targets - - AssignCmd simpleAssignCmd = assignCmd.AsSimpleAssignCmd; - HashSet indexSet = new HashSet(); - int index = 0; - foreach (AssignLhs/*!*/ lhs in simpleAssignCmd.Lhss) { - Contract.Assert(lhs != null); - SimpleAssignLhs salhs = lhs as SimpleAssignLhs; - Contract.Assert(salhs != null); - Variable var = salhs.DeepAssignedVariable; - if (var != null && liveSet.Contains(var)) { - indexSet.Add(index); - liveSet.Remove(var); - } - index++; - } - index = 0; - foreach (Expr/*!*/ expr in simpleAssignCmd.Rhss) { - Contract.Assert(expr != null); - if (indexSet.Contains(index)) { - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(expr); - liveSet.UnionWith(collector.usedVars); - } - index++; - } - } else if (cmd is HavocCmd) { - HavocCmd/*!*/ havocCmd = (HavocCmd)cmd; - foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { - Contract.Assert(expr != null); - if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) { - liveSet.Remove(expr.Decl); - } - } - } else if (cmd is PredicateCmd) { - Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd)); - PredicateCmd/*!*/ predicateCmd = (PredicateCmd)cce.NonNull(cmd); - if (predicateCmd.Expr is LiteralExpr) { - LiteralExpr le = (LiteralExpr)predicateCmd.Expr; - if (le.IsFalse) { - liveSet.Clear(); - } - } else { - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(predicateCmd.Expr); - liveSet.UnionWith(collector.usedVars); - } - } else if (cmd is CommentCmd) { - // comments are just for debugging and don't affect verification - } else if (cmd is SugaredCmd) { - SugaredCmd/*!*/ sugCmd = (SugaredCmd)cce.NonNull(cmd); - Propagate(sugCmd.Desugaring, liveSet); - } else if (cmd is StateCmd) { - StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd); - List/*!*/ cmds = cce.NonNull(stCmd.Cmds); - int len = cmds.Count; - for (int i = len - 1; i >= 0; i--) { - Propagate(cmds[i], liveSet); - } - foreach (Variable/*!*/ v in stCmd.Locals) { - Contract.Assert(v != null); - liveSet.Remove(v); - } - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } - } - } - } - - /* - // An idempotent semiring interface - abstract public class Weight { - abstract public Weight! one(); - abstract public Weight! zero(); - abstract public Weight! extend(Weight! w1, Weight! w2); - abstract public Weight! combine(Weight! w1, Weight! w2); - abstract public Weight! isEqual(Weight! w); - abstract public Weight! projectLocals() - } - */ - - // Weight domain for LiveVariableAnalysis (Gen/Kill) - - public class GenKillWeight { - // lambda S. (S - kill) union gen - HashSet/*!*/ gen; - HashSet/*!*/ kill; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(gen)); - Contract.Invariant(cce.NonNullElements(kill)); - Contract.Invariant(oneWeight != null); - Contract.Invariant(zeroWeight != null); - } - - bool isZero; - - public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new HashSet(), new HashSet()); - public static GenKillWeight/*!*/ zeroWeight = new GenKillWeight(); - - // initializes to zero - public GenKillWeight() { - this.isZero = true; - this.gen = new HashSet(); - this.kill = new HashSet(); - } - - public GenKillWeight(HashSet gen, HashSet kill) { - Contract.Requires(cce.NonNullElements(gen)); - Contract.Requires(cce.NonNullElements(kill)); - Contract.Assert(gen != null); - Contract.Assert(kill != null); - this.gen = gen; - this.kill = kill; - this.isZero = false; - } - - public static GenKillWeight one() { - Contract.Ensures(Contract.Result() != null); - return oneWeight; - } - - public static GenKillWeight zero() { - Contract.Ensures(Contract.Result() != null); - return zeroWeight; - } - - public static GenKillWeight extend(GenKillWeight w1, GenKillWeight w2) { - Contract.Requires(w2 != null); - Contract.Requires(w1 != null); - Contract.Ensures(Contract.Result() != null); - if (w1.isZero || w2.isZero) - return zero(); - - HashSet t = new HashSet(w2.gen); - t.ExceptWith(w1.kill); - HashSet g = new HashSet(w1.gen); - g.UnionWith(t); - HashSet k = new HashSet(w1.kill); - k.UnionWith(w2.kill); - return new GenKillWeight(g, k); - //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill)); - } - - public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2) { - Contract.Requires(w2 != null); - Contract.Requires(w1 != null); - Contract.Ensures(Contract.Result() != null); - if (w1.isZero) - return w2; - if (w2.isZero) - return w1; - - HashSet g = new HashSet(w1.gen); - g.UnionWith(w2.gen); - HashSet k = new HashSet(w1.kill); - k.IntersectWith(w2.kill); - return new GenKillWeight(g, k); - //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill)); - } - - public static GenKillWeight projectLocals(GenKillWeight w) { - Contract.Requires(w != null); - Contract.Ensures(Contract.Result() != null); - HashSet gen = new HashSet(); - foreach (Variable v in w.gen) - { - if (isGlobal(v)) - gen.Add(v); - } - HashSet kill = new HashSet(); - foreach (Variable v in w.kill) - { - if (isGlobal(v)) - kill.Add(v); - } - - return new GenKillWeight(gen, kill); - } - - public static bool isEqual(GenKillWeight w1, GenKillWeight w2) { - Contract.Requires(w2 != null); - Contract.Requires(w1 != null); - if (w1.isZero) - return w2.isZero; - if (w2.isZero) - return w1.isZero; - - return (w1.gen.Equals(w2.gen) && w1.kill.Equals(w2.kill)); - } - - private static bool isGlobal(Variable v) { - Contract.Requires(v != null); - return (v is GlobalVariable); - } - - [Pure] - public override string ToString() { - Contract.Ensures(Contract.Result() != null); - return string.Format("({0},{1})", gen.ToString(), kill.ToString()); - } - - public HashSet/*!*/ getLiveVars() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return gen; - } - - public HashSet/*!*/ getLiveVars(HashSet/*!*/ lv) { - Contract.Requires(cce.NonNullElements(lv)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - HashSet temp = new HashSet(lv); - temp.ExceptWith(kill); - temp.UnionWith(gen); - return temp; - } - - } - - public class ICFG { - public Graph/*!*/ graph; - // Map from procedure to the list of blocks that call that procedure - public Dictionary/*!*/>/*!*/ procsCalled; - public HashSet/*!*/ nodes; - public Dictionary/*!*/>/*!*/ succEdges; - public Dictionary/*!*/>/*!*/ predEdges; - private Dictionary/*!*/ priority; - - public HashSet/*!*/ srcNodes; - public HashSet/*!*/ exitNodes; - - public Dictionary/*!*/ weightBefore; - public Dictionary/*!*/ weightAfter; - public Dictionary/*!*/>/*!*/ liveVarsAfter; - public Dictionary/*!*/>/*!*/ liveVarsBefore; - - public GenKillWeight/*!*/ summary; - public Implementation/*!*/ impl; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(graph.Nodes)); - Contract.Invariant(cce.NonNullDictionaryAndValues(procsCalled)); - Contract.Invariant(cce.NonNullElements(nodes)); - Contract.Invariant(cce.NonNullDictionaryAndValues(succEdges)); - Contract.Invariant(cce.NonNullDictionaryAndValues(predEdges)); - Contract.Invariant(priority != null); - Contract.Invariant(cce.NonNullElements(srcNodes)); - Contract.Invariant(cce.NonNullElements(exitNodes)); - Contract.Invariant(cce.NonNullDictionaryAndValues(weightBefore)); - Contract.Invariant(cce.NonNullDictionaryAndValues(weightAfter)); - Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsAfter)); - Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsBefore)); - Contract.Invariant(summary != null); - Contract.Invariant(impl != null); - } - - - [NotDelayed] - public ICFG(Implementation impl) { - Contract.Requires(impl != null); - this.graph = new Graph(); - this.procsCalled = new Dictionary/*!*/>(); - this.nodes = new HashSet(); - this.succEdges = new Dictionary/*!*/>(); - this.predEdges = new Dictionary/*!*/>(); - - this.priority = new Dictionary(); - - this.srcNodes = new HashSet(); - this.exitNodes = new HashSet(); - - this.weightBefore = new Dictionary(); - this.weightAfter = new Dictionary(); - this.liveVarsAfter = new Dictionary/*!*/>(); - this.liveVarsBefore = new Dictionary/*!*/>(); - - summary = GenKillWeight.zero(); - this.impl = impl; - - Initialize(impl); - - } - - private void Initialize(Implementation impl) { - Contract.Requires(impl != null); - addSource(impl.Blocks[0]); - graph.AddSource(impl.Blocks[0]); - - foreach (Block/*!*/ b in impl.Blocks) { - Contract.Assert(b != null); - if (b.TransferCmd is ReturnCmd) { - exitNodes.Add(b); - } else { - GotoCmd gc = b.TransferCmd as GotoCmd; - Contract.Assert(gc != null); - Contract.Assert(gc.labelTargets != null); - foreach (Block/*!*/ t in gc.labelTargets) { - Contract.Assert(t != null); - addEdge(b, t); - graph.AddEdge(b, t); - } - } - - weightBefore[b] = GenKillWeight.zero(); - weightAfter[b] = GenKillWeight.zero(); - - foreach (Cmd/*!*/ c in b.Cmds) { - Contract.Assert(c != null); - if (c is CallCmd) { - CallCmd/*!*/ cc = cce.NonNull((CallCmd/*!*/)c); - Contract.Assert(cc.Proc != null); - string/*!*/ procName = cc.Proc.Name; - Contract.Assert(procName != null); - if (!procsCalled.ContainsKey(procName)) { - procsCalled.Add(procName, new List()); - } - procsCalled[procName].Add(b); - } - } - } - - List/*!*/ sortedNodes; - bool acyclic; - - graph.TarjanTopSort(out acyclic, out sortedNodes); - - if (!acyclic) { - Console.WriteLine("Warning: graph is not a dag"); - } - - int num = sortedNodes.Count; - foreach (Block/*!*/ b in sortedNodes) { - Contract.Assert(b != null); - priority.Add(b, num); - num--; - } - - } - - public int getPriority(Block b) { - Contract.Requires(b != null); - if (priority.ContainsKey(b)) - return priority[b]; - return Int32.MaxValue; - } - - private void addSource(Block b) { - Contract.Requires(b != null); - registerNode(b); - this.srcNodes.Add(b); - } - - private void addExit(Block b) { - Contract.Requires(b != null); - registerNode(b); - this.exitNodes.Add(b); - } - - private void registerNode(Block b) { - Contract.Requires(b != null); - if (!succEdges.ContainsKey(b)) { - succEdges.Add(b, new HashSet()); - } - - if (!predEdges.ContainsKey(b)) { - predEdges.Add(b, new HashSet()); - } - - nodes.Add(b); - } - - private void addEdge(Block src, Block tgt) { - Contract.Requires(tgt != null); - Contract.Requires(src != null); - registerNode(src); - registerNode(tgt); - - succEdges[src].Add(tgt); - predEdges[tgt].Add(src); - } - - - } - - // Interprocedural Gen/Kill Analysis - public class InterProcGenKill { - Program/*!*/ program; - Dictionary/*!*/ procICFG; - Dictionary/*!*/ name2Proc; - Dictionary/*!*/>/*!*/ callers; - Graph/*!*/ callGraph; - Dictionary/*!*/ procPriority; - int maxBlocksInProc; - - WorkList/*!*/ workList; - - Implementation/*!*/ mainImpl; - - static Dictionary/*!*/>/*!*/ varsLiveAtExit = new Dictionary/*!*/>(); - static Dictionary/*!*/>/*!*/ varsLiveAtEntry = new Dictionary/*!*/>(); - static Dictionary/*!*/ varsLiveSummary = new Dictionary(); - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(workList != null); - Contract.Invariant(mainImpl != null); - Contract.Invariant(program != null); - Contract.Invariant(cce.NonNullDictionaryAndValues(procICFG)); - Contract.Invariant(cce.NonNullDictionaryAndValues(name2Proc)); - Contract.Invariant(cce.NonNullDictionaryAndValues(callers) && - Contract.ForAll(callers.Values, v => cce.NonNullElements(v))); - Contract.Invariant(cce.NonNullElements(callGraph.Nodes)); - Contract.Invariant(procPriority != null); - Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtEntry)); - Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtExit) && - Contract.ForAll(varsLiveAtExit.Values, v => cce.NonNullElements(v))); - Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveSummary)); - Contract.Invariant(cce.NonNullDictionaryAndValues(weightCacheAfterCall)); - Contract.Invariant(cce.NonNullDictionaryAndValues(weightCacheBeforeCall)); - } - - - [NotDelayed] - public InterProcGenKill(Implementation impl, Program program) { - Contract.Requires(program != null); - Contract.Requires(impl != null); - this.program = program; - procICFG = new Dictionary(); - name2Proc = new Dictionary(); - workList = new WorkList(); - this.callers = new Dictionary/*!*/>(); - this.callGraph = new Graph(); - this.procPriority = new Dictionary(); - this.maxBlocksInProc = 0; - this.mainImpl = impl; - - Dictionary/*!*/ name2Impl = new Dictionary(); - varsLiveAtExit.Clear(); - varsLiveAtEntry.Clear(); - varsLiveSummary.Clear(); - - foreach (var decl in program.TopLevelDeclarations) { - Contract.Assert(decl != null); - if (decl is Implementation) { - Implementation/*!*/ imp = (Implementation/*!*/)cce.NonNull(decl); - name2Impl[imp.Name] = imp; - } else if (decl is Procedure) { - Procedure/*!*/ proc = cce.NonNull(decl as Procedure); - name2Proc[proc.Name] = proc; - } - } - - ICFG/*!*/ mainICFG = new ICFG(mainImpl); - Contract.Assert(mainICFG != null); - procICFG.Add(mainICFG.impl.Name, mainICFG); - callGraph.AddSource(mainICFG.impl.Name); - - List/*!*/ procsToConsider = new List(); - procsToConsider.Add(mainICFG); - - while (procsToConsider.Count != 0) { - ICFG/*!*/ p = procsToConsider[0]; - Contract.Assert(p != null); - procsToConsider.RemoveAt(0); - - foreach (string/*!*/ callee in p.procsCalled.Keys) { - Contract.Assert(callee != null); - if (!name2Impl.ContainsKey(callee)) - continue; - - callGraph.AddEdge(p.impl.Name, callee); - - if (maxBlocksInProc < p.nodes.Count) { - maxBlocksInProc = p.nodes.Count; - } - - if (!callers.ContainsKey(callee)) { - callers.Add(callee, new List()); - } - foreach (Block/*!*/ b in p.procsCalled[callee]) { - Contract.Assert(b != null); - callers[callee].Add(new WorkItem(p, b)); - } - - if (procICFG.ContainsKey(callee)) - continue; - ICFG/*!*/ ncfg = new ICFG(name2Impl[callee]); - Contract.Assert(ncfg != null); - procICFG.Add(callee, ncfg); - procsToConsider.Add(ncfg); - } - } - - bool acyclic; - List/*!*/ sortedNodes; - callGraph.TarjanTopSort(out acyclic, out sortedNodes); - - Contract.Assert(acyclic); - - int cnt = 0; - for (int i = sortedNodes.Count - 1; i >= 0; i--) { - string s = sortedNodes[i]; - if (s == null) - continue; - procPriority.Add(s, cnt); - cnt++; - } - - } - - public static HashSet/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) { - Contract.Requires(prog != null); - Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - if (varsLiveAtExit.ContainsKey(impl.Name)) { - return varsLiveAtExit[impl.Name]; - } - // Return default: all globals and out params - HashSet/*!*/ lv = new HashSet(); - foreach (Variable/*!*/ v in prog.GlobalVariables) { - Contract.Assert(v != null); - lv.Add(v); - } - foreach (Variable/*!*/ v in impl.OutParams) { - Contract.Assert(v != null); - lv.Add(v); - } - return lv; - } - - public static HashSet/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) { - Contract.Requires(prog != null); - Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - if (varsLiveAtEntry.ContainsKey(impl.Name)) { - return varsLiveAtEntry[impl.Name]; - } - // Return default: all globals and in params - HashSet/*!*/ lv = new HashSet(); - foreach (Variable/*!*/ v in prog.GlobalVariables) { - Contract.Assert(v != null); - lv.Add(v); - } - foreach (Variable/*!*/ v in impl.InParams) { - Contract.Assert(v != null); - lv.Add(v); - } - return lv; - } - - public static bool HasSummary(string name) { - Contract.Requires(name != null); - return varsLiveSummary.ContainsKey(name); - } - - public static HashSet/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, HashSet/*!*/ lvAfter) { - Contract.Requires(cmd != null); - Contract.Requires(cce.NonNullElements(lvAfter)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - Procedure/*!*/ proc = cce.NonNull(cmd.Proc); - if (varsLiveSummary.ContainsKey(proc.Name)) { - GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); - Contract.Assert(w1 != null); - GenKillWeight/*!*/ w2 = varsLiveSummary[proc.Name]; - Contract.Assert(w2 != null); - GenKillWeight/*!*/ w3 = getWeightAfterCall(cmd); - Contract.Assert(w3 != null); - GenKillWeight/*!*/ w = GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3)); - Contract.Assert(w != null); - return w.getLiveVars(lvAfter); - } - HashSet/*!*/ ret = new HashSet(); - ret.UnionWith(lvAfter); - LiveVariableAnalysis.Propagate(cmd, ret); - return ret; - } - - class WorkItem { - public ICFG/*!*/ cfg; - public Block/*!*/ block; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(cfg != null); - Contract.Invariant(block != null); - } - - - public WorkItem(ICFG cfg, Block block) { - Contract.Requires(block != null); - Contract.Requires(cfg != null); - this.cfg = cfg; - this.block = block; - } - - public GenKillWeight getWeightAfter() { - Contract.Ensures(Contract.Result() != null); - return cfg.weightAfter[block]; - } - - public bool setWeightBefore(GenKillWeight w) { - Contract.Requires(w != null); - GenKillWeight/*!*/ prev = cfg.weightBefore[block]; - Contract.Assert(prev != null); - GenKillWeight/*!*/ curr = GenKillWeight.combine(w, prev); - Contract.Assert(curr != null); - if (GenKillWeight.isEqual(prev, curr)) - return false; - cfg.weightBefore[block] = curr; - return true; - } - - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public override bool Equals(object other) { - WorkItem/*!*/ wi = (WorkItem/*!*/)cce.NonNull(other); - return (wi.cfg == cfg && wi.block == block); - } - - [Pure] - public override int GetHashCode() { - return 0; - } - - public string getLabel() { - Contract.Ensures(Contract.Result() != null); - return cfg.impl.Name + "::" + block.Label; - } - - } - - private void AddToWorkList(WorkItem wi) { - Contract.Requires(wi != null); - int i = procPriority[wi.cfg.impl.Name]; - int j = wi.cfg.getPriority(wi.block); - int priority = (i * maxBlocksInProc) + j; - - workList.Add(wi, priority); - } - - private void AddToWorkListReverse(WorkItem wi) { - Contract.Requires(wi != null); - int i = procPriority[wi.cfg.impl.Name]; - int j = wi.cfg.getPriority(wi.block); - int priority = (procPriority.Count - i) * maxBlocksInProc + j; - workList.Add(wi, priority); - } - - class WorkList { - SortedList/*!*/ priorities; - HashSet/*!*/ labels; - - Dictionary/*!*/>/*!*/ workList; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(priorities != null); - Contract.Invariant(cce.NonNullElements(labels)); - Contract.Invariant(cce.NonNullDictionaryAndValues(workList) && - Contract.ForAll(workList.Values, v => cce.NonNullElements(v))); - } - - - public WorkList() { - labels = new HashSet(); - priorities = new SortedList(); - workList = new Dictionary/*!*/>(); - } - - public void Add(WorkItem wi, int priority) { - Contract.Requires(wi != null); - string/*!*/ lab = wi.getLabel(); - Contract.Assert(lab != null); - if (labels.Contains(lab)) { - // Already on worklist - return; - } - labels.Add(lab); - if (!workList.ContainsKey(priority)) { - workList.Add(priority, new List()); - } - workList[priority].Add(wi); - if (!priorities.ContainsKey(priority)) { - priorities.Add(priority, 0); - } - - priorities[priority] = priorities[priority] + 1; - } - - public WorkItem Get() { - Contract.Ensures(Contract.Result() != null); - // Get minimum priority - int p = cce.NonNull(priorities.Keys)[0]; - priorities[p] = priorities[p] - 1; - if (priorities[p] == 0) { - priorities.Remove(p); - } - - // Get a WI with this priority - WorkItem/*!*/ wi = workList[p][0]; - Contract.Assert(wi != null); - workList[p].RemoveAt(0); - - // update labels - labels.Remove(wi.getLabel()); - return wi; - } - - public int Count { - get { - return labels.Count; - } - } - } - - private GenKillWeight getSummary(CallCmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assert(cmd.Proc != null); - string/*!*/ procName = cmd.Proc.Name; - Contract.Assert(procName != null); - if (procICFG.ContainsKey(procName)) { - ICFG/*!*/ cfg = procICFG[procName]; - Contract.Assert(cfg != null); - return GenKillWeight.projectLocals(cfg.summary); - } - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } - } - - public static void ComputeLiveVars(Implementation impl, Program/*!*/ prog) { - Contract.Requires(prog != null); - Contract.Requires(impl != null); - InterProcGenKill/*!*/ ipgk = new InterProcGenKill(impl, prog); - Contract.Assert(ipgk != null); - ipgk.Compute(); - } - - public void Compute() { - // Put all exit nodes in the worklist - foreach (ICFG/*!*/ cfg in procICFG.Values) { - Contract.Assert(cfg != null); - foreach (Block/*!*/ eb in cfg.exitNodes) { - Contract.Assert(eb != null); - WorkItem/*!*/ wi = new WorkItem(cfg, eb); - Contract.Assert(wi != null); - cfg.weightAfter[eb] = GenKillWeight.one(); - AddToWorkList(wi); - } - } - - while (workList.Count != 0) { - WorkItem/*!*/ wi = workList.Get(); - Contract.Assert(wi != null); - process(wi); - } - - // Propagate LV to all procedures - foreach (ICFG/*!*/ cfg in procICFG.Values) { - Contract.Assert(cfg != null); - foreach (Block/*!*/ b in cfg.nodes) { - Contract.Assert(b != null); - cfg.liveVarsAfter.Add(b, new HashSet()); - cfg.liveVarsBefore.Add(b, new HashSet()); - } - } - - ICFG/*!*/ mainCfg = procICFG[mainImpl.Name]; - Contract.Assert(mainCfg != null); - foreach (Block/*!*/ eb in mainCfg.exitNodes) { - Contract.Assert(eb != null); - WorkItem/*!*/ wi = new WorkItem(mainCfg, eb); - Contract.Assert(wi != null); - AddToWorkListReverse(wi); - } - - while (workList.Count != 0) { - WorkItem/*!*/ wi = workList.Get(); - Contract.Assert(wi != null); - processLV(wi); - } - - // Set live variable info - foreach (ICFG/*!*/ cfg in procICFG.Values) { - Contract.Assert(cfg != null); - HashSet/*!*/ lv = new HashSet(); - foreach (Block/*!*/ eb in cfg.exitNodes) { - Contract.Assert(eb != null); - lv.UnionWith(cfg.liveVarsAfter[eb]); - } - varsLiveAtExit.Add(cfg.impl.Name, lv); - lv = new HashSet(); - foreach (Block/*!*/ eb in cfg.srcNodes) { - Contract.Assert(eb != null); - lv.UnionWith(cfg.liveVarsBefore[eb]); - } - varsLiveAtEntry.Add(cfg.impl.Name, lv); - varsLiveSummary.Add(cfg.impl.Name, cfg.summary); - } - - /* - foreach(Block/*!*/ - /* b in mainImpl.Blocks){ -Contract.Assert(b != null); -//Set lv = cfg.weightBefore[b].getLiveVars(); -b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; -//foreach(GlobalVariable/*!*/ - /* v in program.GlobalVariables){Contract.Assert(v != null); -// b.liveVarsBefore.Add(v); -//} -} -*/ - } - - // Called when summaries have already been computed - private void processLV(WorkItem wi) { - Contract.Requires(wi != null); - ICFG/*!*/ cfg = wi.cfg; - Contract.Assert(cfg != null); - Block/*!*/ block = wi.block; - Contract.Assert(block != null); - HashSet/*!*/ lv = cfg.liveVarsAfter[block]; - Contract.Assert(cce.NonNullElements(lv)); - // Propagate backwards in the block - HashSet/*!*/ prop = new HashSet(); - prop.UnionWith(lv); - for (int i = block.Cmds.Count - 1; i >= 0; i--) { - Cmd/*!*/ cmd = block.Cmds[i]; - Contract.Assert(cmd != null); - if (cmd is CallCmd) { - string/*!*/ procName = cce.NonNull(cce.NonNull((CallCmd)cmd).Proc).Name; - Contract.Assert(procName != null); - if (procICFG.ContainsKey(procName)) { - ICFG/*!*/ callee = procICFG[procName]; - Contract.Assert(callee != null); - // Inter propagation - // Remove local variables; add return variables - HashSet/*!*/ elv = new HashSet(); - foreach (Variable/*!*/ v in prop) { - Contract.Assert(v != null); - if (v is GlobalVariable) - elv.Add(v); - } - foreach (Variable/*!*/ v in callee.impl.OutParams) { - Contract.Assert(v != null); - elv.Add(v); - } - - foreach (Block/*!*/ eb in callee.exitNodes) { - Contract.Assert(eb != null); - callee.liveVarsAfter[eb].UnionWith(elv); - // TODO: check if modified before inserting - AddToWorkListReverse(new WorkItem(callee, eb)); - } - - // Continue with intra propagation - GenKillWeight/*!*/ summary = getWeightCall(cce.NonNull((CallCmd/*!*/)cmd)); - prop = summary.getLiveVars(prop); - } else { - LiveVariableAnalysis.Propagate(cmd, prop); - } - } else { - LiveVariableAnalysis.Propagate(cmd, prop); - } - } - - cfg.liveVarsBefore[block].UnionWith(prop); - - foreach (Block/*!*/ b in cfg.predEdges[block]) { - Contract.Assert(b != null); - HashSet/*!*/ prev = cfg.liveVarsAfter[b]; - Contract.Assert(cce.NonNullElements(prev)); - HashSet/*!*/ curr = new HashSet(prev); - curr.UnionWith(cfg.liveVarsBefore[block]); - Contract.Assert(cce.NonNullElements(curr)); - if (curr.Count != prev.Count) { - cfg.liveVarsAfter[b] = curr; - AddToWorkListReverse(new WorkItem(cfg, b)); - } - } - } - - private void process(WorkItem wi) { - Contract.Requires(wi != null); - GenKillWeight/*!*/ w = wi.getWeightAfter(); - Contract.Assert(w != null); - - for (int i = wi.block.Cmds.Count - 1; i >= 0; i--) { - Cmd/*!*/ c = wi.block.Cmds[i]; - Contract.Assert(c != null); - if (c is CallCmd && procICFG.ContainsKey(cce.NonNull(cce.NonNull((CallCmd)c).Proc).Name)) { - w = GenKillWeight.extend(getWeightCall(cce.NonNull((CallCmd)c)), w); - } else { - GenKillWeight/*!*/ cweight = getWeight(c, wi.cfg.impl, program); - Contract.Assert(cweight != null); - w = GenKillWeight.extend(cweight, w); - } - } - - bool change = wi.setWeightBefore(w); - - if (change && wi.cfg.srcNodes.Contains(wi.block)) { - GenKillWeight/*!*/ prev = wi.cfg.summary; - Contract.Assert(prev != null); - GenKillWeight/*!*/ curr = GenKillWeight.combine(prev, wi.cfg.weightBefore[wi.block]); - Contract.Assert(curr != null); - if (!GenKillWeight.isEqual(prev, curr)) { - wi.cfg.summary = curr; - // push callers onto the worklist - if (callers.ContainsKey(wi.cfg.impl.Name)) { - foreach (WorkItem/*!*/ caller in callers[wi.cfg.impl.Name]) { - Contract.Assert(caller != null); - AddToWorkList(caller); - } - } - } - } - - foreach (Block/*!*/ b in wi.cfg.predEdges[wi.block]) { - Contract.Assert(b != null); - GenKillWeight/*!*/ prev = wi.cfg.weightAfter[b]; - Contract.Assert(prev != null); - GenKillWeight/*!*/ curr = GenKillWeight.combine(prev, w); - Contract.Assert(curr != null); - if (!GenKillWeight.isEqual(prev, curr)) { - wi.cfg.weightAfter[b] = curr; - AddToWorkList(new WorkItem(wi.cfg, b)); - } - } - - } - - static Dictionary/*!*/ weightCache = new Dictionary(); - - private static GenKillWeight getWeight(Cmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - return getWeight(cmd, null, null); - } - - private GenKillWeight getWeightCall(CallCmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); - GenKillWeight/*!*/ w2 = getSummary(cmd); - GenKillWeight/*!*/ w3 = getWeightAfterCall(cmd); - Contract.Assert(w1 != null); - Contract.Assert(w2 != null); - Contract.Assert(w3 != null); - return GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3)); - } - - private static GenKillWeight getWeight(Cmd cmd, Implementation impl, Program prog) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - - if (weightCache.ContainsKey(cmd)) - return weightCache[cmd]; - - HashSet/*!*/ gen = new HashSet(); - HashSet/*!*/ kill = new HashSet(); - GenKillWeight/*!*/ ret; - - if (cmd is AssignCmd) { - AssignCmd/*!*/ assignCmd = (AssignCmd)cmd; - Contract.Assert(cmd != null); - // I must first iterate over all the targets and remove the live ones. - // After the removals are done, I must add the variables referred on - // the right side of the removed targets - foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { - Contract.Assert(lhs != null); - Variable var = lhs.DeepAssignedVariable; - if (var != null) { - if (lhs is SimpleAssignLhs) { - // we should only remove non-map target variables because there is an implicit - // read of a map variable in an assignment to it - kill.Add(var); - } - } - } - int index = 0; - foreach (Expr/*!*/ expr in assignCmd.Rhss) { - Contract.Assert(expr != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(expr); - gen.UnionWith(collector.usedVars); - AssignLhs lhs = assignCmd.Lhss[index]; - if (lhs is MapAssignLhs) { - // If the target is a map, then all indices are also read - MapAssignLhs malhs = (MapAssignLhs)lhs; - foreach (Expr e in malhs.Indexes) { - VariableCollector/*!*/ c = new VariableCollector(); - c.Visit(e); - gen.UnionWith(c.usedVars); - } - } - index++; - } - ret = new GenKillWeight(gen, kill); - } else if (cmd is HavocCmd) { - HavocCmd/*!*/ havocCmd = (HavocCmd)cce.NonNull(cmd); - foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { - Contract.Assert(expr != null); - if (expr.Decl != null) { - kill.Add(expr.Decl); - } - } - ret = new GenKillWeight(gen, kill); - } else if (cmd is PredicateCmd) { - Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd)); - PredicateCmd/*!*/ predicateCmd = (PredicateCmd)cce.NonNull(cmd); - if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) { - LiteralExpr le = (LiteralExpr)predicateCmd.Expr; - if (le.IsFalse) { - var globals = prog.GlobalVariables; - Contract.Assert(cce.NonNullElements(globals)); - foreach (Variable/*!*/ v in globals) { - Contract.Assert(v != null); - kill.Add(v); - } - foreach (Variable/*!*/ v in impl.LocVars) { - Contract.Assert(v != null); - kill.Add(v); - } - foreach (Variable/*!*/ v in impl.OutParams) { - Contract.Assert(v != null); - kill.Add(v); - } - } - } else { - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(predicateCmd.Expr); - gen.UnionWith(collector.usedVars); - } - ret = new GenKillWeight(gen, kill); - } else if (cmd is CommentCmd) { - ret = new GenKillWeight(gen, kill); - // comments are just for debugging and don't affect verification - } else if (cmd is SugaredCmd) { - SugaredCmd/*!*/ sugCmd = (SugaredCmd)cmd; - Contract.Assert(sugCmd != null); - ret = getWeight(sugCmd.Desugaring, impl, prog); - } else if (cmd is StateCmd) { - StateCmd/*!*/ stCmd = (StateCmd)cmd; - Contract.Assert(stCmd != null); - List/*!*/ cmds = stCmd.Cmds; - Contract.Assert(cmds != null); - int len = cmds.Count; - ret = GenKillWeight.one(); - for (int i = len - 1; i >= 0; i--) { - GenKillWeight/*!*/ w = getWeight(cmds[i], impl, prog); - Contract.Assert(w != null); - ret = GenKillWeight.extend(w, ret); - } - foreach (Variable/*!*/ v in stCmd.Locals) { - Contract.Assert(v != null); - kill.Add(v); - } - ret = GenKillWeight.extend(new GenKillWeight(gen, kill), ret); - } else { - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } - } - - weightCache[cmd] = ret; - return ret; - } - - static Dictionary/*!*/ weightCacheAfterCall = new Dictionary(); - static Dictionary/*!*/ weightCacheBeforeCall = new Dictionary(); - - private static GenKillWeight getWeightAfterCall(Cmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - - if (weightCacheAfterCall.ContainsKey(cmd)) - return weightCacheAfterCall[cmd]; - - HashSet/*!*/ gen = new HashSet(); - HashSet/*!*/ kill = new HashSet(); - - Contract.Assert(cmd is CallCmd); - CallCmd/*!*/ ccmd = cce.NonNull((CallCmd)cmd); - - foreach (IdentifierExpr/*!*/ ie in ccmd.Outs) { - Contract.Assert(ie != null); - if (ie.Decl != null) - kill.Add(ie.Decl); - } - - // Variables in ensures are considered as "read" - foreach (Ensures/*!*/ re in cce.NonNull(ccmd.Proc).Ensures) { - Contract.Assert(re != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(re.Condition); - foreach (Variable/*!*/ v in collector.usedVars) { - Contract.Assert(v != null); - if (v is GlobalVariable) { - gen.Add(v); - } - } - } - - GenKillWeight/*!*/ ret = new GenKillWeight(gen, kill); - Contract.Assert(ret != null); - weightCacheAfterCall[cmd] = ret; - return ret; - } - - private static GenKillWeight getWeightBeforeCall(Cmd cmd) { - Contract.Requires(cmd != null); - Contract.Ensures(Contract.Result() != null); - Contract.Assert((cmd is CallCmd)); - if (weightCacheBeforeCall.ContainsKey(cmd)) - return weightCacheBeforeCall[cmd]; - - HashSet/*!*/ gen = new HashSet(); - HashSet/*!*/ kill = new HashSet(); - CallCmd/*!*/ ccmd = cce.NonNull((CallCmd/*!*/)cmd); - - foreach (Expr/*!*/ expr in ccmd.Ins) { - Contract.Assert(expr != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(expr); - gen.UnionWith(collector.usedVars); - } - - Contract.Assert(ccmd.Proc != null); - - // Variables in requires are considered as "read" - foreach (Requires/*!*/ re in ccmd.Proc.Requires) { - Contract.Assert(re != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(re.Condition); - foreach (Variable/*!*/ v in collector.usedVars) { - Contract.Assert(v != null); - if (v is GlobalVariable) { - gen.Add(v); - } - } - } - - // Old variables in ensures are considered as "read" - foreach (Ensures/*!*/ re in ccmd.Proc.Ensures) { - Contract.Assert(re != null); - VariableCollector/*!*/ collector = new VariableCollector(); - collector.Visit(re.Condition); - foreach (Variable/*!*/ v in collector.oldVarsUsed) { - Contract.Assert(v != null); - if (v is GlobalVariable) { - gen.Add(v); - } - } - } - - GenKillWeight/*!*/ ret = new GenKillWeight(gen, kill); - Contract.Assert(ret != null); - weightCacheAfterCall[cmd] = ret; - return ret; - } - } - - public class TokenEliminator : ReadOnlyVisitor - { - public int TokenCount = 0; - public override Expr VisitExpr(Expr node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitExpr(node); - } - public override Variable VisitVariable(Variable node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitVariable(node); - } - public override Function VisitFunction(Function node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitFunction(node); - } - public override Implementation VisitImplementation(Implementation node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitImplementation(node); - } - public override Procedure VisitProcedure(Procedure node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitProcedure(node); - } - public override Axiom VisitAxiom(Axiom node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitAxiom(node); - } - public override Cmd VisitAssignCmd(AssignCmd node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitAssignCmd(node); - } - public override Cmd VisitAssumeCmd(AssumeCmd node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitAssumeCmd(node); - } - public override Cmd VisitHavocCmd(HavocCmd node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitHavocCmd(node); - } - public override Constant VisitConstant(Constant node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitConstant(node); - } - public override TransferCmd VisitTransferCmd(TransferCmd node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitTransferCmd(node); - } - public override Block VisitBlock(Block node) - { - node.tok = Token.NoToken; - TokenCount++; - return base.VisitBlock(node); - } - } +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Boogie.GraphUtil; +using System.Diagnostics.Contracts; + + +namespace Microsoft.Boogie { + public class UnusedVarEliminator : VariableCollector { + public static void Eliminate(Program program) { + Contract.Requires(program != null); + UnusedVarEliminator elim = new UnusedVarEliminator(); + elim.Visit(program); + } + + private UnusedVarEliminator() + : base() { + + } + + public override Implementation VisitImplementation(Implementation node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + //Console.WriteLine("Procedure {0}", node.Name); + Implementation/*!*/ impl = base.VisitImplementation(node); + Contract.Assert(impl != null); + //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length); + List/*!*/ vars = new List(); + foreach (Variable/*!*/ var in impl.LocVars) { + Contract.Assert(var != null); + if (_usedVars.Contains(var)) + vars.Add(var); + } + impl.LocVars = vars; + //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length); + //Console.WriteLine("---------------------------------"); + _usedVars.Clear(); + return impl; + } + } + + public class ModSetCollector : ReadOnlyVisitor { + private Procedure enclosingProc; + private Dictionary/*!*/>/*!*/ modSets; + private HashSet yieldingProcs; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullDictionaryAndValues(modSets)); + Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v))); + } + + public ModSetCollector() { + modSets = new Dictionary/*!*/>(); + yieldingProcs = new HashSet(); + } + + private bool moreProcessingRequired; + + public void DoModSetAnalysis(Program program) { + Contract.Requires(program != null); + + if (CommandLineOptions.Clo.Trace) + { +// Console.WriteLine(); +// Console.WriteLine("Running modset analysis ..."); +// int procCount = 0; +// foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) +// { +// Contract.Assert(decl != null); +// if (decl is Procedure) +// procCount++; +// } +// Console.WriteLine("Number of procedures = {0}", procCount);*/ + } + + HashSet implementedProcs = new HashSet(); + foreach (var impl in program.Implementations) { + if (impl.Proc != null) + implementedProcs.Add(impl.Proc); + } + foreach (var proc in program.Procedures) { + if (!implementedProcs.Contains(proc)) + { + enclosingProc = proc; + foreach (var expr in proc.Modifies) + { + Contract.Assert(expr != null); + ProcessVariable(expr.Decl); + } + enclosingProc = null; + } + else + { + modSets.Add(proc, new HashSet()); + } + } + + moreProcessingRequired = true; + while (moreProcessingRequired) { + moreProcessingRequired = false; + this.Visit(program); + } + + foreach (Procedure x in modSets.Keys) + { + x.Modifies = new List(); + foreach (Variable v in modSets[x]) + { + x.Modifies.Add(new IdentifierExpr(v.tok, v)); + } + } + foreach (Procedure x in yieldingProcs) + { + if (!QKeyValue.FindBoolAttribute(x.Attributes, "yields")) + { + x.AddAttribute("yields"); + } + } + +#if DEBUG_PRINT + Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); + foreach (Procedure/*!*/ x in modSets.Keys) { + Contract.Assert(x != null); + Console.Write("{0} : ", x.Name); + bool first = true; + foreach (Variable/*!*/ y in modSets[x]) { + Contract.Assert(y != null); + if (first) + first = false; + else + Console.Write(", "); + Console.Write("{0}", y.Name); + } + Console.WriteLine(""); + } +#endif + } + + public override Implementation VisitImplementation(Implementation node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + enclosingProc = node.Proc; + Implementation/*!*/ ret = base.VisitImplementation(node); + Contract.Assert(ret != null); + enclosingProc = null; + + return ret; + } + public override YieldCmd VisitYieldCmd(YieldCmd node) + { + if (!yieldingProcs.Contains(enclosingProc)) + { + yieldingProcs.Add(enclosingProc); + moreProcessingRequired = true; + } + return base.VisitYieldCmd(node); + } + public override Cmd VisitAssignCmd(AssignCmd assignCmd) { + //Contract.Requires(assignCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitAssignCmd(assignCmd); + foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { + Contract.Assert(lhs != null); + ProcessVariable(lhs.DeepAssignedVariable); + } + return ret; + } + public override Cmd VisitHavocCmd(HavocCmd havocCmd) { + //Contract.Requires(havocCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitHavocCmd(havocCmd); + foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { + Contract.Assert(expr != null); + ProcessVariable(expr.Decl); + } + return ret; + } + public override Cmd VisitCallCmd(CallCmd callCmd) { + //Contract.Requires(callCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitCallCmd(callCmd); + foreach (IdentifierExpr ie in callCmd.Outs) + { + if (ie != null) ProcessVariable(ie.Decl); + } + Procedure callee = callCmd.Proc; + if (callee == null) + return ret; + if (modSets.ContainsKey(callee)) { + foreach (Variable var in modSets[callee]) { + ProcessVariable(var); + } + } + if (!yieldingProcs.Contains(enclosingProc) && (yieldingProcs.Contains(callCmd.Proc) || callCmd.IsAsync)) + { + yieldingProcs.Add(enclosingProc); + moreProcessingRequired = true; + } + if (callCmd.IsAsync) + { + if (!yieldingProcs.Contains(callCmd.Proc)) + { + yieldingProcs.Add(callCmd.Proc); + moreProcessingRequired = true; + } + } + return ret; + } + public override Cmd VisitParCallCmd(ParCallCmd node) + { + //Contract.Requires(callCmd != null); + Contract.Ensures(Contract.Result() != null); + Cmd ret = base.VisitParCallCmd(node); + if (!yieldingProcs.Contains(enclosingProc)) + { + yieldingProcs.Add(enclosingProc); + moreProcessingRequired = true; + } + foreach (CallCmd callCmd in node.CallCmds) + { + if (!yieldingProcs.Contains(callCmd.Proc)) + { + yieldingProcs.Add(callCmd.Proc); + moreProcessingRequired = true; + } + } + return ret; + } + private void ProcessVariable(Variable var) { + Procedure/*!*/ localProc = cce.NonNull(enclosingProc); + if (var == null) + return; + if (!(var is GlobalVariable)) + return; + if (!modSets.ContainsKey(localProc)) { + modSets[localProc] = new HashSet(); + } + if (modSets[localProc].Contains(var)) + return; + moreProcessingRequired = true; + modSets[localProc].Add(var); + } + public override Expr VisitCodeExpr(CodeExpr node) { + // don't go into the code expression, since it can only modify variables local to the code expression, + // and the mod-set analysis is interested in global variables + return node; + } + } + + public class MutableVariableCollector : ReadOnlyVisitor + { + public HashSet UsedVariables = new HashSet(); + + public void AddUsedVariables(HashSet usedVariables) + { + Contract.Requires(usedVariables != null); + + foreach (var v in usedVariables) + { + UsedVariables.Add(v); + } + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) + { + Contract.Ensures(Contract.Result() != null); + + if (node.Decl != null && node.Decl.IsMutable) + { + UsedVariables.Add(node.Decl); + } + return base.VisitIdentifierExpr(node); + } + } + + public class VariableCollector : ReadOnlyVisitor { + protected HashSet/*!*/ _usedVars; + public IEnumerable/*!*/ usedVars + { + get + { + return _usedVars.AsEnumerable(); + } + } + + protected HashSet/*!*/ _oldVarsUsed; + public IEnumerable/*!*/ oldVarsUsed + { + get + { + return _oldVarsUsed.AsEnumerable(); + } + } + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(_usedVars)); + Contract.Invariant(cce.NonNullElements(_oldVarsUsed)); + } + + int insideOldExpr; + + public VariableCollector() { + _usedVars = new System.Collections.Generic.HashSet(); + _oldVarsUsed = new System.Collections.Generic.HashSet(); + insideOldExpr = 0; + } + + public override Expr VisitOldExpr(OldExpr node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + insideOldExpr++; + node.Expr = this.VisitExpr(node.Expr); + insideOldExpr--; + return node; + } + + public override Expr VisitIdentifierExpr(IdentifierExpr node) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + if (node.Decl != null) { + _usedVars.Add(node.Decl); + if (insideOldExpr > 0) { + _oldVarsUsed.Add(node.Decl); + } + } + return node; + } + } + + public class BlockCoalescer : ReadOnlyVisitor { + public static void CoalesceBlocks(Program program) { + Contract.Requires(program != null); + BlockCoalescer blockCoalescer = new BlockCoalescer(); + blockCoalescer.Visit(program); + } + + private static HashSet/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) { + Contract.Requires(impl != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + HashSet visitedBlocks = new HashSet(); + HashSet multiPredBlocks = new HashSet(); + Stack dfsStack = new Stack(); + dfsStack.Push(impl.Blocks[0]); + while (dfsStack.Count > 0) { + Block/*!*/ b = dfsStack.Pop(); + Contract.Assert(b != null); + if (visitedBlocks.Contains(b)) { + multiPredBlocks.Add(b); + continue; + } + visitedBlocks.Add(b); + if (b.TransferCmd == null) + continue; + if (b.TransferCmd is ReturnCmd) + continue; + Contract.Assert(b.TransferCmd is GotoCmd); + GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; + if (gotoCmd.labelTargets == null) + continue; + foreach (Block/*!*/ succ in gotoCmd.labelTargets) { + Contract.Assert(succ != null); + dfsStack.Push(succ); + } + } + return multiPredBlocks; + } + + public override Implementation VisitImplementation(Implementation impl) { + //Contract.Requires(impl != null); + Contract.Ensures(Contract.Result() != null); + //Console.WriteLine("Procedure {0}", impl.Name); + //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count); + + HashSet multiPredBlocks = ComputeMultiPredecessorBlocks(impl); + Contract.Assert(cce.NonNullElements(multiPredBlocks)); + HashSet visitedBlocks = new HashSet(); + HashSet removedBlocks = new HashSet(); + Stack dfsStack = new Stack(); + dfsStack.Push(impl.Blocks[0]); + while (dfsStack.Count > 0) { + Block/*!*/ b = dfsStack.Pop(); + Contract.Assert(b != null); + if (visitedBlocks.Contains(b)) + continue; + visitedBlocks.Add(b); + if (b.TransferCmd == null) + continue; + if (b.TransferCmd is ReturnCmd) + continue; + Contract.Assert(b.TransferCmd is GotoCmd); + GotoCmd gotoCmd = (GotoCmd)b.TransferCmd; + if (gotoCmd.labelTargets == null) + continue; + if (gotoCmd.labelTargets.Count == 1) { + Block/*!*/ succ = cce.NonNull(gotoCmd.labelTargets[0]); + if (!multiPredBlocks.Contains(succ)) { + foreach (Cmd/*!*/ cmd in succ.Cmds) { + Contract.Assert(cmd != null); + b.Cmds.Add(cmd); + } + b.TransferCmd = succ.TransferCmd; + if (!b.tok.IsValid && succ.tok.IsValid) { + b.tok = succ.tok; + b.Label = succ.Label; + } + removedBlocks.Add(succ); + dfsStack.Push(b); + visitedBlocks.Remove(b); + continue; + } + } + foreach (Block/*!*/ succ in gotoCmd.labelTargets) { + Contract.Assert(succ != null); + dfsStack.Push(succ); + } + } + + List newBlocks = new List(); + foreach (Block/*!*/ b in impl.Blocks) { + Contract.Assert(b != null); + if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b)) { + newBlocks.Add(b); + } + } + impl.Blocks = newBlocks; + foreach (Block b in impl.Blocks) + { + if (b.TransferCmd is ReturnCmd) continue; + GotoCmd gotoCmd = b.TransferCmd as GotoCmd; + gotoCmd.labelNames = new List(); + foreach (Block succ in gotoCmd.labelTargets) + { + gotoCmd.labelNames.Add(succ.Label); + } + } + // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count); + return impl; + } + } + + public class LiveVariableAnalysis { + public static void ClearLiveVariables(Implementation impl) { + Contract.Requires(impl != null); + foreach (Block/*!*/ block in impl.Blocks) { + Contract.Assert(block != null); + block.liveVarsBefore = null; + } + } + + public static void ComputeLiveVariables(Implementation impl) { + Contract.Requires(impl != null); + Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis"); + Graph dag = new Graph(); + dag.AddSource(cce.NonNull(impl.Blocks[0])); // there is always at least one node in the graph + foreach (Block b in impl.Blocks) { + GotoCmd gtc = b.TransferCmd as GotoCmd; + if (gtc != null) { + Contract.Assume(gtc.labelTargets != null); + foreach (Block/*!*/ dest in gtc.labelTargets) { + Contract.Assert(dest != null); + dag.AddEdge(dest, b); + } + } + } + + IEnumerable sortedNodes; + if (CommandLineOptions.Clo.ModifyTopologicalSorting) { + sortedNodes = dag.TopologicalSort(true); + } else { + sortedNodes = dag.TopologicalSort(); + } + foreach (Block/*!*/ block in sortedNodes) { + Contract.Assert(block != null); + HashSet/*!*/ liveVarsAfter = new HashSet(); + + // The injected assumption variables should always be considered to be live. + foreach (var v in impl.InjectedAssumptionVariables.Concat(impl.DoomedInjectedAssumptionVariables)) + { + liveVarsAfter.Add(v); + } + + if (block.TransferCmd is GotoCmd) { + GotoCmd gotoCmd = (GotoCmd)block.TransferCmd; + if (gotoCmd.labelTargets != null) { + foreach (Block/*!*/ succ in gotoCmd.labelTargets) { + Contract.Assert(succ != null); + Contract.Assert(succ.liveVarsBefore != null); + liveVarsAfter.UnionWith(succ.liveVarsBefore); + } + } + } + + List cmds = block.Cmds; + int len = cmds.Count; + for (int i = len - 1; i >= 0; i--) { + if (cmds[i] is CallCmd) { + Procedure/*!*/ proc = cce.NonNull(cce.NonNull((CallCmd/*!*/)cmds[i]).Proc); + if (InterProcGenKill.HasSummary(proc.Name)) { + liveVarsAfter = + InterProcGenKill.PropagateLiveVarsAcrossCall(cce.NonNull((CallCmd/*!*/)cmds[i]), liveVarsAfter); + continue; + } + } + Propagate(cmds[i], liveVarsAfter); + } + + block.liveVarsBefore = liveVarsAfter; + + } + } + + // perform in place update of liveSet + public static void Propagate(Cmd cmd, HashSet/*!*/ liveSet) { + Contract.Requires(cmd != null); + Contract.Requires(cce.NonNullElements(liveSet)); + if (cmd is AssignCmd) { + AssignCmd/*!*/ assignCmd = (AssignCmd)cce.NonNull(cmd); + // I must first iterate over all the targets and remove the live ones. + // After the removals are done, I must add the variables referred on + // the right side of the removed targets + + AssignCmd simpleAssignCmd = assignCmd.AsSimpleAssignCmd; + HashSet indexSet = new HashSet(); + int index = 0; + foreach (AssignLhs/*!*/ lhs in simpleAssignCmd.Lhss) { + Contract.Assert(lhs != null); + SimpleAssignLhs salhs = lhs as SimpleAssignLhs; + Contract.Assert(salhs != null); + Variable var = salhs.DeepAssignedVariable; + if (var != null && liveSet.Contains(var)) { + indexSet.Add(index); + liveSet.Remove(var); + } + index++; + } + index = 0; + foreach (Expr/*!*/ expr in simpleAssignCmd.Rhss) { + Contract.Assert(expr != null); + if (indexSet.Contains(index)) { + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(expr); + liveSet.UnionWith(collector.usedVars); + } + index++; + } + } else if (cmd is HavocCmd) { + HavocCmd/*!*/ havocCmd = (HavocCmd)cmd; + foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { + Contract.Assert(expr != null); + if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") && expr.Decl.Name.StartsWith("a##cached##"))) { + liveSet.Remove(expr.Decl); + } + } + } else if (cmd is PredicateCmd) { + Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd)); + PredicateCmd/*!*/ predicateCmd = (PredicateCmd)cce.NonNull(cmd); + if (predicateCmd.Expr is LiteralExpr) { + LiteralExpr le = (LiteralExpr)predicateCmd.Expr; + if (le.IsFalse) { + liveSet.Clear(); + } + } else { + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(predicateCmd.Expr); + liveSet.UnionWith(collector.usedVars); + } + } else if (cmd is CommentCmd) { + // comments are just for debugging and don't affect verification + } else if (cmd is SugaredCmd) { + SugaredCmd/*!*/ sugCmd = (SugaredCmd)cce.NonNull(cmd); + Propagate(sugCmd.Desugaring, liveSet); + } else if (cmd is StateCmd) { + StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd); + List/*!*/ cmds = cce.NonNull(stCmd.Cmds); + int len = cmds.Count; + for (int i = len - 1; i >= 0; i--) { + Propagate(cmds[i], liveSet); + } + foreach (Variable/*!*/ v in stCmd.Locals) { + Contract.Assert(v != null); + liveSet.Remove(v); + } + } else { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + } + } + + /* + // An idempotent semiring interface + abstract public class Weight { + abstract public Weight! one(); + abstract public Weight! zero(); + abstract public Weight! extend(Weight! w1, Weight! w2); + abstract public Weight! combine(Weight! w1, Weight! w2); + abstract public Weight! isEqual(Weight! w); + abstract public Weight! projectLocals() + } + */ + + // Weight domain for LiveVariableAnalysis (Gen/Kill) + + public class GenKillWeight { + // lambda S. (S - kill) union gen + HashSet/*!*/ gen; + HashSet/*!*/ kill; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(gen)); + Contract.Invariant(cce.NonNullElements(kill)); + Contract.Invariant(oneWeight != null); + Contract.Invariant(zeroWeight != null); + } + + bool isZero; + + public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new HashSet(), new HashSet()); + public static GenKillWeight/*!*/ zeroWeight = new GenKillWeight(); + + // initializes to zero + public GenKillWeight() { + this.isZero = true; + this.gen = new HashSet(); + this.kill = new HashSet(); + } + + public GenKillWeight(HashSet gen, HashSet kill) { + Contract.Requires(cce.NonNullElements(gen)); + Contract.Requires(cce.NonNullElements(kill)); + Contract.Assert(gen != null); + Contract.Assert(kill != null); + this.gen = gen; + this.kill = kill; + this.isZero = false; + } + + public static GenKillWeight one() { + Contract.Ensures(Contract.Result() != null); + return oneWeight; + } + + public static GenKillWeight zero() { + Contract.Ensures(Contract.Result() != null); + return zeroWeight; + } + + public static GenKillWeight extend(GenKillWeight w1, GenKillWeight w2) { + Contract.Requires(w2 != null); + Contract.Requires(w1 != null); + Contract.Ensures(Contract.Result() != null); + if (w1.isZero || w2.isZero) + return zero(); + + HashSet t = new HashSet(w2.gen); + t.ExceptWith(w1.kill); + HashSet g = new HashSet(w1.gen); + g.UnionWith(t); + HashSet k = new HashSet(w1.kill); + k.UnionWith(w2.kill); + return new GenKillWeight(g, k); + //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill)); + } + + public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2) { + Contract.Requires(w2 != null); + Contract.Requires(w1 != null); + Contract.Ensures(Contract.Result() != null); + if (w1.isZero) + return w2; + if (w2.isZero) + return w1; + + HashSet g = new HashSet(w1.gen); + g.UnionWith(w2.gen); + HashSet k = new HashSet(w1.kill); + k.IntersectWith(w2.kill); + return new GenKillWeight(g, k); + //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill)); + } + + public static GenKillWeight projectLocals(GenKillWeight w) { + Contract.Requires(w != null); + Contract.Ensures(Contract.Result() != null); + HashSet gen = new HashSet(); + foreach (Variable v in w.gen) + { + if (isGlobal(v)) + gen.Add(v); + } + HashSet kill = new HashSet(); + foreach (Variable v in w.kill) + { + if (isGlobal(v)) + kill.Add(v); + } + + return new GenKillWeight(gen, kill); + } + + public static bool isEqual(GenKillWeight w1, GenKillWeight w2) { + Contract.Requires(w2 != null); + Contract.Requires(w1 != null); + if (w1.isZero) + return w2.isZero; + if (w2.isZero) + return w1.isZero; + + return (w1.gen.Equals(w2.gen) && w1.kill.Equals(w2.kill)); + } + + private static bool isGlobal(Variable v) { + Contract.Requires(v != null); + return (v is GlobalVariable); + } + + [Pure] + public override string ToString() { + Contract.Ensures(Contract.Result() != null); + return string.Format("({0},{1})", gen.ToString(), kill.ToString()); + } + + public HashSet/*!*/ getLiveVars() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return gen; + } + + public HashSet/*!*/ getLiveVars(HashSet/*!*/ lv) { + Contract.Requires(cce.NonNullElements(lv)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + HashSet temp = new HashSet(lv); + temp.ExceptWith(kill); + temp.UnionWith(gen); + return temp; + } + + } + + public class ICFG { + public Graph/*!*/ graph; + // Map from procedure to the list of blocks that call that procedure + public Dictionary/*!*/>/*!*/ procsCalled; + public HashSet/*!*/ nodes; + public Dictionary/*!*/>/*!*/ succEdges; + public Dictionary/*!*/>/*!*/ predEdges; + private Dictionary/*!*/ priority; + + public HashSet/*!*/ srcNodes; + public HashSet/*!*/ exitNodes; + + public Dictionary/*!*/ weightBefore; + public Dictionary/*!*/ weightAfter; + public Dictionary/*!*/>/*!*/ liveVarsAfter; + public Dictionary/*!*/>/*!*/ liveVarsBefore; + + public GenKillWeight/*!*/ summary; + public Implementation/*!*/ impl; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(graph.Nodes)); + Contract.Invariant(cce.NonNullDictionaryAndValues(procsCalled)); + Contract.Invariant(cce.NonNullElements(nodes)); + Contract.Invariant(cce.NonNullDictionaryAndValues(succEdges)); + Contract.Invariant(cce.NonNullDictionaryAndValues(predEdges)); + Contract.Invariant(priority != null); + Contract.Invariant(cce.NonNullElements(srcNodes)); + Contract.Invariant(cce.NonNullElements(exitNodes)); + Contract.Invariant(cce.NonNullDictionaryAndValues(weightBefore)); + Contract.Invariant(cce.NonNullDictionaryAndValues(weightAfter)); + Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsAfter)); + Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsBefore)); + Contract.Invariant(summary != null); + Contract.Invariant(impl != null); + } + + + [NotDelayed] + public ICFG(Implementation impl) { + Contract.Requires(impl != null); + this.graph = new Graph(); + this.procsCalled = new Dictionary/*!*/>(); + this.nodes = new HashSet(); + this.succEdges = new Dictionary/*!*/>(); + this.predEdges = new Dictionary/*!*/>(); + + this.priority = new Dictionary(); + + this.srcNodes = new HashSet(); + this.exitNodes = new HashSet(); + + this.weightBefore = new Dictionary(); + this.weightAfter = new Dictionary(); + this.liveVarsAfter = new Dictionary/*!*/>(); + this.liveVarsBefore = new Dictionary/*!*/>(); + + summary = GenKillWeight.zero(); + this.impl = impl; + + Initialize(impl); + + } + + private void Initialize(Implementation impl) { + Contract.Requires(impl != null); + addSource(impl.Blocks[0]); + graph.AddSource(impl.Blocks[0]); + + foreach (Block/*!*/ b in impl.Blocks) { + Contract.Assert(b != null); + if (b.TransferCmd is ReturnCmd) { + exitNodes.Add(b); + } else { + GotoCmd gc = b.TransferCmd as GotoCmd; + Contract.Assert(gc != null); + Contract.Assert(gc.labelTargets != null); + foreach (Block/*!*/ t in gc.labelTargets) { + Contract.Assert(t != null); + addEdge(b, t); + graph.AddEdge(b, t); + } + } + + weightBefore[b] = GenKillWeight.zero(); + weightAfter[b] = GenKillWeight.zero(); + + foreach (Cmd/*!*/ c in b.Cmds) { + Contract.Assert(c != null); + if (c is CallCmd) { + CallCmd/*!*/ cc = cce.NonNull((CallCmd/*!*/)c); + Contract.Assert(cc.Proc != null); + string/*!*/ procName = cc.Proc.Name; + Contract.Assert(procName != null); + if (!procsCalled.ContainsKey(procName)) { + procsCalled.Add(procName, new List()); + } + procsCalled[procName].Add(b); + } + } + } + + List/*!*/ sortedNodes; + bool acyclic; + + graph.TarjanTopSort(out acyclic, out sortedNodes); + + if (!acyclic) { + Console.WriteLine("Warning: graph is not a dag"); + } + + int num = sortedNodes.Count; + foreach (Block/*!*/ b in sortedNodes) { + Contract.Assert(b != null); + priority.Add(b, num); + num--; + } + + } + + public int getPriority(Block b) { + Contract.Requires(b != null); + if (priority.ContainsKey(b)) + return priority[b]; + return Int32.MaxValue; + } + + private void addSource(Block b) { + Contract.Requires(b != null); + registerNode(b); + this.srcNodes.Add(b); + } + + private void addExit(Block b) { + Contract.Requires(b != null); + registerNode(b); + this.exitNodes.Add(b); + } + + private void registerNode(Block b) { + Contract.Requires(b != null); + if (!succEdges.ContainsKey(b)) { + succEdges.Add(b, new HashSet()); + } + + if (!predEdges.ContainsKey(b)) { + predEdges.Add(b, new HashSet()); + } + + nodes.Add(b); + } + + private void addEdge(Block src, Block tgt) { + Contract.Requires(tgt != null); + Contract.Requires(src != null); + registerNode(src); + registerNode(tgt); + + succEdges[src].Add(tgt); + predEdges[tgt].Add(src); + } + + + } + + // Interprocedural Gen/Kill Analysis + public class InterProcGenKill { + Program/*!*/ program; + Dictionary/*!*/ procICFG; + Dictionary/*!*/ name2Proc; + Dictionary/*!*/>/*!*/ callers; + Graph/*!*/ callGraph; + Dictionary/*!*/ procPriority; + int maxBlocksInProc; + + WorkList/*!*/ workList; + + Implementation/*!*/ mainImpl; + + static Dictionary/*!*/>/*!*/ varsLiveAtExit = new Dictionary/*!*/>(); + static Dictionary/*!*/>/*!*/ varsLiveAtEntry = new Dictionary/*!*/>(); + static Dictionary/*!*/ varsLiveSummary = new Dictionary(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(workList != null); + Contract.Invariant(mainImpl != null); + Contract.Invariant(program != null); + Contract.Invariant(cce.NonNullDictionaryAndValues(procICFG)); + Contract.Invariant(cce.NonNullDictionaryAndValues(name2Proc)); + Contract.Invariant(cce.NonNullDictionaryAndValues(callers) && + Contract.ForAll(callers.Values, v => cce.NonNullElements(v))); + Contract.Invariant(cce.NonNullElements(callGraph.Nodes)); + Contract.Invariant(procPriority != null); + Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtEntry)); + Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveAtExit) && + Contract.ForAll(varsLiveAtExit.Values, v => cce.NonNullElements(v))); + Contract.Invariant(cce.NonNullDictionaryAndValues(varsLiveSummary)); + Contract.Invariant(cce.NonNullDictionaryAndValues(weightCacheAfterCall)); + Contract.Invariant(cce.NonNullDictionaryAndValues(weightCacheBeforeCall)); + } + + + [NotDelayed] + public InterProcGenKill(Implementation impl, Program program) { + Contract.Requires(program != null); + Contract.Requires(impl != null); + this.program = program; + procICFG = new Dictionary(); + name2Proc = new Dictionary(); + workList = new WorkList(); + this.callers = new Dictionary/*!*/>(); + this.callGraph = new Graph(); + this.procPriority = new Dictionary(); + this.maxBlocksInProc = 0; + this.mainImpl = impl; + + Dictionary/*!*/ name2Impl = new Dictionary(); + varsLiveAtExit.Clear(); + varsLiveAtEntry.Clear(); + varsLiveSummary.Clear(); + + foreach (var decl in program.TopLevelDeclarations) { + Contract.Assert(decl != null); + if (decl is Implementation) { + Implementation/*!*/ imp = (Implementation/*!*/)cce.NonNull(decl); + name2Impl[imp.Name] = imp; + } else if (decl is Procedure) { + Procedure/*!*/ proc = cce.NonNull(decl as Procedure); + name2Proc[proc.Name] = proc; + } + } + + ICFG/*!*/ mainICFG = new ICFG(mainImpl); + Contract.Assert(mainICFG != null); + procICFG.Add(mainICFG.impl.Name, mainICFG); + callGraph.AddSource(mainICFG.impl.Name); + + List/*!*/ procsToConsider = new List(); + procsToConsider.Add(mainICFG); + + while (procsToConsider.Count != 0) { + ICFG/*!*/ p = procsToConsider[0]; + Contract.Assert(p != null); + procsToConsider.RemoveAt(0); + + foreach (string/*!*/ callee in p.procsCalled.Keys) { + Contract.Assert(callee != null); + if (!name2Impl.ContainsKey(callee)) + continue; + + callGraph.AddEdge(p.impl.Name, callee); + + if (maxBlocksInProc < p.nodes.Count) { + maxBlocksInProc = p.nodes.Count; + } + + if (!callers.ContainsKey(callee)) { + callers.Add(callee, new List()); + } + foreach (Block/*!*/ b in p.procsCalled[callee]) { + Contract.Assert(b != null); + callers[callee].Add(new WorkItem(p, b)); + } + + if (procICFG.ContainsKey(callee)) + continue; + ICFG/*!*/ ncfg = new ICFG(name2Impl[callee]); + Contract.Assert(ncfg != null); + procICFG.Add(callee, ncfg); + procsToConsider.Add(ncfg); + } + } + + bool acyclic; + List/*!*/ sortedNodes; + callGraph.TarjanTopSort(out acyclic, out sortedNodes); + + Contract.Assert(acyclic); + + int cnt = 0; + for (int i = sortedNodes.Count - 1; i >= 0; i--) { + string s = sortedNodes[i]; + if (s == null) + continue; + procPriority.Add(s, cnt); + cnt++; + } + + } + + public static HashSet/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) { + Contract.Requires(prog != null); + Contract.Requires(impl != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + if (varsLiveAtExit.ContainsKey(impl.Name)) { + return varsLiveAtExit[impl.Name]; + } + // Return default: all globals and out params + HashSet/*!*/ lv = new HashSet(); + foreach (Variable/*!*/ v in prog.GlobalVariables) { + Contract.Assert(v != null); + lv.Add(v); + } + foreach (Variable/*!*/ v in impl.OutParams) { + Contract.Assert(v != null); + lv.Add(v); + } + return lv; + } + + public static HashSet/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) { + Contract.Requires(prog != null); + Contract.Requires(impl != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + if (varsLiveAtEntry.ContainsKey(impl.Name)) { + return varsLiveAtEntry[impl.Name]; + } + // Return default: all globals and in params + HashSet/*!*/ lv = new HashSet(); + foreach (Variable/*!*/ v in prog.GlobalVariables) { + Contract.Assert(v != null); + lv.Add(v); + } + foreach (Variable/*!*/ v in impl.InParams) { + Contract.Assert(v != null); + lv.Add(v); + } + return lv; + } + + public static bool HasSummary(string name) { + Contract.Requires(name != null); + return varsLiveSummary.ContainsKey(name); + } + + public static HashSet/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, HashSet/*!*/ lvAfter) { + Contract.Requires(cmd != null); + Contract.Requires(cce.NonNullElements(lvAfter)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Procedure/*!*/ proc = cce.NonNull(cmd.Proc); + if (varsLiveSummary.ContainsKey(proc.Name)) { + GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); + Contract.Assert(w1 != null); + GenKillWeight/*!*/ w2 = varsLiveSummary[proc.Name]; + Contract.Assert(w2 != null); + GenKillWeight/*!*/ w3 = getWeightAfterCall(cmd); + Contract.Assert(w3 != null); + GenKillWeight/*!*/ w = GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3)); + Contract.Assert(w != null); + return w.getLiveVars(lvAfter); + } + HashSet/*!*/ ret = new HashSet(); + ret.UnionWith(lvAfter); + LiveVariableAnalysis.Propagate(cmd, ret); + return ret; + } + + class WorkItem { + public ICFG/*!*/ cfg; + public Block/*!*/ block; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cfg != null); + Contract.Invariant(block != null); + } + + + public WorkItem(ICFG cfg, Block block) { + Contract.Requires(block != null); + Contract.Requires(cfg != null); + this.cfg = cfg; + this.block = block; + } + + public GenKillWeight getWeightAfter() { + Contract.Ensures(Contract.Result() != null); + return cfg.weightAfter[block]; + } + + public bool setWeightBefore(GenKillWeight w) { + Contract.Requires(w != null); + GenKillWeight/*!*/ prev = cfg.weightBefore[block]; + Contract.Assert(prev != null); + GenKillWeight/*!*/ curr = GenKillWeight.combine(w, prev); + Contract.Assert(curr != null); + if (GenKillWeight.isEqual(prev, curr)) + return false; + cfg.weightBefore[block] = curr; + return true; + } + + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) { + WorkItem/*!*/ wi = (WorkItem/*!*/)cce.NonNull(other); + return (wi.cfg == cfg && wi.block == block); + } + + [Pure] + public override int GetHashCode() { + return 0; + } + + public string getLabel() { + Contract.Ensures(Contract.Result() != null); + return cfg.impl.Name + "::" + block.Label; + } + + } + + private void AddToWorkList(WorkItem wi) { + Contract.Requires(wi != null); + int i = procPriority[wi.cfg.impl.Name]; + int j = wi.cfg.getPriority(wi.block); + int priority = (i * maxBlocksInProc) + j; + + workList.Add(wi, priority); + } + + private void AddToWorkListReverse(WorkItem wi) { + Contract.Requires(wi != null); + int i = procPriority[wi.cfg.impl.Name]; + int j = wi.cfg.getPriority(wi.block); + int priority = (procPriority.Count - i) * maxBlocksInProc + j; + workList.Add(wi, priority); + } + + class WorkList { + SortedList/*!*/ priorities; + HashSet/*!*/ labels; + + Dictionary/*!*/>/*!*/ workList; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(priorities != null); + Contract.Invariant(cce.NonNullElements(labels)); + Contract.Invariant(cce.NonNullDictionaryAndValues(workList) && + Contract.ForAll(workList.Values, v => cce.NonNullElements(v))); + } + + + public WorkList() { + labels = new HashSet(); + priorities = new SortedList(); + workList = new Dictionary/*!*/>(); + } + + public void Add(WorkItem wi, int priority) { + Contract.Requires(wi != null); + string/*!*/ lab = wi.getLabel(); + Contract.Assert(lab != null); + if (labels.Contains(lab)) { + // Already on worklist + return; + } + labels.Add(lab); + if (!workList.ContainsKey(priority)) { + workList.Add(priority, new List()); + } + workList[priority].Add(wi); + if (!priorities.ContainsKey(priority)) { + priorities.Add(priority, 0); + } + + priorities[priority] = priorities[priority] + 1; + } + + public WorkItem Get() { + Contract.Ensures(Contract.Result() != null); + // Get minimum priority + int p = cce.NonNull(priorities.Keys)[0]; + priorities[p] = priorities[p] - 1; + if (priorities[p] == 0) { + priorities.Remove(p); + } + + // Get a WI with this priority + WorkItem/*!*/ wi = workList[p][0]; + Contract.Assert(wi != null); + workList[p].RemoveAt(0); + + // update labels + labels.Remove(wi.getLabel()); + return wi; + } + + public int Count { + get { + return labels.Count; + } + } + } + + private GenKillWeight getSummary(CallCmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + Contract.Assert(cmd.Proc != null); + string/*!*/ procName = cmd.Proc.Name; + Contract.Assert(procName != null); + if (procICFG.ContainsKey(procName)) { + ICFG/*!*/ cfg = procICFG[procName]; + Contract.Assert(cfg != null); + return GenKillWeight.projectLocals(cfg.summary); + } + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + + public static void ComputeLiveVars(Implementation impl, Program/*!*/ prog) { + Contract.Requires(prog != null); + Contract.Requires(impl != null); + InterProcGenKill/*!*/ ipgk = new InterProcGenKill(impl, prog); + Contract.Assert(ipgk != null); + ipgk.Compute(); + } + + public void Compute() { + // Put all exit nodes in the worklist + foreach (ICFG/*!*/ cfg in procICFG.Values) { + Contract.Assert(cfg != null); + foreach (Block/*!*/ eb in cfg.exitNodes) { + Contract.Assert(eb != null); + WorkItem/*!*/ wi = new WorkItem(cfg, eb); + Contract.Assert(wi != null); + cfg.weightAfter[eb] = GenKillWeight.one(); + AddToWorkList(wi); + } + } + + while (workList.Count != 0) { + WorkItem/*!*/ wi = workList.Get(); + Contract.Assert(wi != null); + process(wi); + } + + // Propagate LV to all procedures + foreach (ICFG/*!*/ cfg in procICFG.Values) { + Contract.Assert(cfg != null); + foreach (Block/*!*/ b in cfg.nodes) { + Contract.Assert(b != null); + cfg.liveVarsAfter.Add(b, new HashSet()); + cfg.liveVarsBefore.Add(b, new HashSet()); + } + } + + ICFG/*!*/ mainCfg = procICFG[mainImpl.Name]; + Contract.Assert(mainCfg != null); + foreach (Block/*!*/ eb in mainCfg.exitNodes) { + Contract.Assert(eb != null); + WorkItem/*!*/ wi = new WorkItem(mainCfg, eb); + Contract.Assert(wi != null); + AddToWorkListReverse(wi); + } + + while (workList.Count != 0) { + WorkItem/*!*/ wi = workList.Get(); + Contract.Assert(wi != null); + processLV(wi); + } + + // Set live variable info + foreach (ICFG/*!*/ cfg in procICFG.Values) { + Contract.Assert(cfg != null); + HashSet/*!*/ lv = new HashSet(); + foreach (Block/*!*/ eb in cfg.exitNodes) { + Contract.Assert(eb != null); + lv.UnionWith(cfg.liveVarsAfter[eb]); + } + varsLiveAtExit.Add(cfg.impl.Name, lv); + lv = new HashSet(); + foreach (Block/*!*/ eb in cfg.srcNodes) { + Contract.Assert(eb != null); + lv.UnionWith(cfg.liveVarsBefore[eb]); + } + varsLiveAtEntry.Add(cfg.impl.Name, lv); + varsLiveSummary.Add(cfg.impl.Name, cfg.summary); + } + + /* + foreach(Block/*!*/ + /* b in mainImpl.Blocks){ +Contract.Assert(b != null); +//Set lv = cfg.weightBefore[b].getLiveVars(); +b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; +//foreach(GlobalVariable/*!*/ + /* v in program.GlobalVariables){Contract.Assert(v != null); +// b.liveVarsBefore.Add(v); +//} +} +*/ + } + + // Called when summaries have already been computed + private void processLV(WorkItem wi) { + Contract.Requires(wi != null); + ICFG/*!*/ cfg = wi.cfg; + Contract.Assert(cfg != null); + Block/*!*/ block = wi.block; + Contract.Assert(block != null); + HashSet/*!*/ lv = cfg.liveVarsAfter[block]; + Contract.Assert(cce.NonNullElements(lv)); + // Propagate backwards in the block + HashSet/*!*/ prop = new HashSet(); + prop.UnionWith(lv); + for (int i = block.Cmds.Count - 1; i >= 0; i--) { + Cmd/*!*/ cmd = block.Cmds[i]; + Contract.Assert(cmd != null); + if (cmd is CallCmd) { + string/*!*/ procName = cce.NonNull(cce.NonNull((CallCmd)cmd).Proc).Name; + Contract.Assert(procName != null); + if (procICFG.ContainsKey(procName)) { + ICFG/*!*/ callee = procICFG[procName]; + Contract.Assert(callee != null); + // Inter propagation + // Remove local variables; add return variables + HashSet/*!*/ elv = new HashSet(); + foreach (Variable/*!*/ v in prop) { + Contract.Assert(v != null); + if (v is GlobalVariable) + elv.Add(v); + } + foreach (Variable/*!*/ v in callee.impl.OutParams) { + Contract.Assert(v != null); + elv.Add(v); + } + + foreach (Block/*!*/ eb in callee.exitNodes) { + Contract.Assert(eb != null); + callee.liveVarsAfter[eb].UnionWith(elv); + // TODO: check if modified before inserting + AddToWorkListReverse(new WorkItem(callee, eb)); + } + + // Continue with intra propagation + GenKillWeight/*!*/ summary = getWeightCall(cce.NonNull((CallCmd/*!*/)cmd)); + prop = summary.getLiveVars(prop); + } else { + LiveVariableAnalysis.Propagate(cmd, prop); + } + } else { + LiveVariableAnalysis.Propagate(cmd, prop); + } + } + + cfg.liveVarsBefore[block].UnionWith(prop); + + foreach (Block/*!*/ b in cfg.predEdges[block]) { + Contract.Assert(b != null); + HashSet/*!*/ prev = cfg.liveVarsAfter[b]; + Contract.Assert(cce.NonNullElements(prev)); + HashSet/*!*/ curr = new HashSet(prev); + curr.UnionWith(cfg.liveVarsBefore[block]); + Contract.Assert(cce.NonNullElements(curr)); + if (curr.Count != prev.Count) { + cfg.liveVarsAfter[b] = curr; + AddToWorkListReverse(new WorkItem(cfg, b)); + } + } + } + + private void process(WorkItem wi) { + Contract.Requires(wi != null); + GenKillWeight/*!*/ w = wi.getWeightAfter(); + Contract.Assert(w != null); + + for (int i = wi.block.Cmds.Count - 1; i >= 0; i--) { + Cmd/*!*/ c = wi.block.Cmds[i]; + Contract.Assert(c != null); + if (c is CallCmd && procICFG.ContainsKey(cce.NonNull(cce.NonNull((CallCmd)c).Proc).Name)) { + w = GenKillWeight.extend(getWeightCall(cce.NonNull((CallCmd)c)), w); + } else { + GenKillWeight/*!*/ cweight = getWeight(c, wi.cfg.impl, program); + Contract.Assert(cweight != null); + w = GenKillWeight.extend(cweight, w); + } + } + + bool change = wi.setWeightBefore(w); + + if (change && wi.cfg.srcNodes.Contains(wi.block)) { + GenKillWeight/*!*/ prev = wi.cfg.summary; + Contract.Assert(prev != null); + GenKillWeight/*!*/ curr = GenKillWeight.combine(prev, wi.cfg.weightBefore[wi.block]); + Contract.Assert(curr != null); + if (!GenKillWeight.isEqual(prev, curr)) { + wi.cfg.summary = curr; + // push callers onto the worklist + if (callers.ContainsKey(wi.cfg.impl.Name)) { + foreach (WorkItem/*!*/ caller in callers[wi.cfg.impl.Name]) { + Contract.Assert(caller != null); + AddToWorkList(caller); + } + } + } + } + + foreach (Block/*!*/ b in wi.cfg.predEdges[wi.block]) { + Contract.Assert(b != null); + GenKillWeight/*!*/ prev = wi.cfg.weightAfter[b]; + Contract.Assert(prev != null); + GenKillWeight/*!*/ curr = GenKillWeight.combine(prev, w); + Contract.Assert(curr != null); + if (!GenKillWeight.isEqual(prev, curr)) { + wi.cfg.weightAfter[b] = curr; + AddToWorkList(new WorkItem(wi.cfg, b)); + } + } + + } + + static Dictionary/*!*/ weightCache = new Dictionary(); + + private static GenKillWeight getWeight(Cmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + return getWeight(cmd, null, null); + } + + private GenKillWeight getWeightCall(CallCmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); + GenKillWeight/*!*/ w2 = getSummary(cmd); + GenKillWeight/*!*/ w3 = getWeightAfterCall(cmd); + Contract.Assert(w1 != null); + Contract.Assert(w2 != null); + Contract.Assert(w3 != null); + return GenKillWeight.extend(w1, GenKillWeight.extend(w2, w3)); + } + + private static GenKillWeight getWeight(Cmd cmd, Implementation impl, Program prog) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + + if (weightCache.ContainsKey(cmd)) + return weightCache[cmd]; + + HashSet/*!*/ gen = new HashSet(); + HashSet/*!*/ kill = new HashSet(); + GenKillWeight/*!*/ ret; + + if (cmd is AssignCmd) { + AssignCmd/*!*/ assignCmd = (AssignCmd)cmd; + Contract.Assert(cmd != null); + // I must first iterate over all the targets and remove the live ones. + // After the removals are done, I must add the variables referred on + // the right side of the removed targets + foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { + Contract.Assert(lhs != null); + Variable var = lhs.DeepAssignedVariable; + if (var != null) { + if (lhs is SimpleAssignLhs) { + // we should only remove non-map target variables because there is an implicit + // read of a map variable in an assignment to it + kill.Add(var); + } + } + } + int index = 0; + foreach (Expr/*!*/ expr in assignCmd.Rhss) { + Contract.Assert(expr != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(expr); + gen.UnionWith(collector.usedVars); + AssignLhs lhs = assignCmd.Lhss[index]; + if (lhs is MapAssignLhs) { + // If the target is a map, then all indices are also read + MapAssignLhs malhs = (MapAssignLhs)lhs; + foreach (Expr e in malhs.Indexes) { + VariableCollector/*!*/ c = new VariableCollector(); + c.Visit(e); + gen.UnionWith(c.usedVars); + } + } + index++; + } + ret = new GenKillWeight(gen, kill); + } else if (cmd is HavocCmd) { + HavocCmd/*!*/ havocCmd = (HavocCmd)cce.NonNull(cmd); + foreach (IdentifierExpr/*!*/ expr in havocCmd.Vars) { + Contract.Assert(expr != null); + if (expr.Decl != null) { + kill.Add(expr.Decl); + } + } + ret = new GenKillWeight(gen, kill); + } else if (cmd is PredicateCmd) { + Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd)); + PredicateCmd/*!*/ predicateCmd = (PredicateCmd)cce.NonNull(cmd); + if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) { + LiteralExpr le = (LiteralExpr)predicateCmd.Expr; + if (le.IsFalse) { + var globals = prog.GlobalVariables; + Contract.Assert(cce.NonNullElements(globals)); + foreach (Variable/*!*/ v in globals) { + Contract.Assert(v != null); + kill.Add(v); + } + foreach (Variable/*!*/ v in impl.LocVars) { + Contract.Assert(v != null); + kill.Add(v); + } + foreach (Variable/*!*/ v in impl.OutParams) { + Contract.Assert(v != null); + kill.Add(v); + } + } + } else { + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(predicateCmd.Expr); + gen.UnionWith(collector.usedVars); + } + ret = new GenKillWeight(gen, kill); + } else if (cmd is CommentCmd) { + ret = new GenKillWeight(gen, kill); + // comments are just for debugging and don't affect verification + } else if (cmd is SugaredCmd) { + SugaredCmd/*!*/ sugCmd = (SugaredCmd)cmd; + Contract.Assert(sugCmd != null); + ret = getWeight(sugCmd.Desugaring, impl, prog); + } else if (cmd is StateCmd) { + StateCmd/*!*/ stCmd = (StateCmd)cmd; + Contract.Assert(stCmd != null); + List/*!*/ cmds = stCmd.Cmds; + Contract.Assert(cmds != null); + int len = cmds.Count; + ret = GenKillWeight.one(); + for (int i = len - 1; i >= 0; i--) { + GenKillWeight/*!*/ w = getWeight(cmds[i], impl, prog); + Contract.Assert(w != null); + ret = GenKillWeight.extend(w, ret); + } + foreach (Variable/*!*/ v in stCmd.Locals) { + Contract.Assert(v != null); + kill.Add(v); + } + ret = GenKillWeight.extend(new GenKillWeight(gen, kill), ret); + } else { + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + + weightCache[cmd] = ret; + return ret; + } + + static Dictionary/*!*/ weightCacheAfterCall = new Dictionary(); + static Dictionary/*!*/ weightCacheBeforeCall = new Dictionary(); + + private static GenKillWeight getWeightAfterCall(Cmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + + if (weightCacheAfterCall.ContainsKey(cmd)) + return weightCacheAfterCall[cmd]; + + HashSet/*!*/ gen = new HashSet(); + HashSet/*!*/ kill = new HashSet(); + + Contract.Assert(cmd is CallCmd); + CallCmd/*!*/ ccmd = cce.NonNull((CallCmd)cmd); + + foreach (IdentifierExpr/*!*/ ie in ccmd.Outs) { + Contract.Assert(ie != null); + if (ie.Decl != null) + kill.Add(ie.Decl); + } + + // Variables in ensures are considered as "read" + foreach (Ensures/*!*/ re in cce.NonNull(ccmd.Proc).Ensures) { + Contract.Assert(re != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(re.Condition); + foreach (Variable/*!*/ v in collector.usedVars) { + Contract.Assert(v != null); + if (v is GlobalVariable) { + gen.Add(v); + } + } + } + + GenKillWeight/*!*/ ret = new GenKillWeight(gen, kill); + Contract.Assert(ret != null); + weightCacheAfterCall[cmd] = ret; + return ret; + } + + private static GenKillWeight getWeightBeforeCall(Cmd cmd) { + Contract.Requires(cmd != null); + Contract.Ensures(Contract.Result() != null); + Contract.Assert((cmd is CallCmd)); + if (weightCacheBeforeCall.ContainsKey(cmd)) + return weightCacheBeforeCall[cmd]; + + HashSet/*!*/ gen = new HashSet(); + HashSet/*!*/ kill = new HashSet(); + CallCmd/*!*/ ccmd = cce.NonNull((CallCmd/*!*/)cmd); + + foreach (Expr/*!*/ expr in ccmd.Ins) { + Contract.Assert(expr != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(expr); + gen.UnionWith(collector.usedVars); + } + + Contract.Assert(ccmd.Proc != null); + + // Variables in requires are considered as "read" + foreach (Requires/*!*/ re in ccmd.Proc.Requires) { + Contract.Assert(re != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(re.Condition); + foreach (Variable/*!*/ v in collector.usedVars) { + Contract.Assert(v != null); + if (v is GlobalVariable) { + gen.Add(v); + } + } + } + + // Old variables in ensures are considered as "read" + foreach (Ensures/*!*/ re in ccmd.Proc.Ensures) { + Contract.Assert(re != null); + VariableCollector/*!*/ collector = new VariableCollector(); + collector.Visit(re.Condition); + foreach (Variable/*!*/ v in collector.oldVarsUsed) { + Contract.Assert(v != null); + if (v is GlobalVariable) { + gen.Add(v); + } + } + } + + GenKillWeight/*!*/ ret = new GenKillWeight(gen, kill); + Contract.Assert(ret != null); + weightCacheAfterCall[cmd] = ret; + return ret; + } + } + + public class TokenEliminator : ReadOnlyVisitor + { + public int TokenCount = 0; + public override Expr VisitExpr(Expr node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitExpr(node); + } + public override Variable VisitVariable(Variable node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitVariable(node); + } + public override Function VisitFunction(Function node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitFunction(node); + } + public override Implementation VisitImplementation(Implementation node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitImplementation(node); + } + public override Procedure VisitProcedure(Procedure node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitProcedure(node); + } + public override Axiom VisitAxiom(Axiom node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitAxiom(node); + } + public override Cmd VisitAssignCmd(AssignCmd node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitAssignCmd(node); + } + public override Cmd VisitAssumeCmd(AssumeCmd node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitAssumeCmd(node); + } + public override Cmd VisitHavocCmd(HavocCmd node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitHavocCmd(node); + } + public override Constant VisitConstant(Constant node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitConstant(node); + } + public override TransferCmd VisitTransferCmd(TransferCmd node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitTransferCmd(node); + } + public override Block VisitBlock(Block node) + { + node.tok = Token.NoToken; + TokenCount++; + return base.VisitBlock(node); + } + } } \ No newline at end of file diff --git a/Test/civl/chris4.bpl b/Test/civl/chris4.bpl new file mode 100644 index 00000000..7a19f975 --- /dev/null +++ b/Test/civl/chris4.bpl @@ -0,0 +1,16 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure{:yields}{:layer 94,95} Test() +{ + yield; + L: + yield; +} + +procedure{:yields}{:layer 94,95} Test2() +{ + yield; + assert{:layer 94} 2 + 2 == 3; + L: + yield; +} diff --git a/Test/civl/chris4.bpl.expect b/Test/civl/chris4.bpl.expect new file mode 100644 index 00000000..d3d00979 --- /dev/null +++ b/Test/civl/chris4.bpl.expect @@ -0,0 +1,5 @@ +chris4.bpl(13,3): Error BP5001: This assertion might not hold. +Execution trace: + chris4.bpl(12,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error -- cgit v1.2.3 From 56a3836f3606fe035362be14428a412792de371b Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 17 Jun 2015 17:29:26 -0700 Subject: modified desugaring so that in commutatitivity checks copies of original codeexpr is made. --- Source/Concurrency/MoverCheck.cs | 1319 ++++++++++---------- Source/Concurrency/OwickiGries.cs | 2412 ++++++++++++++++++------------------- Source/Concurrency/TypeCheck.cs | 151 ++- Test/civl/bar.bpl.expect | 26 +- Test/civl/foo.bpl.expect | 16 +- Test/civl/parallel1.bpl.expect | 16 +- Test/civl/t1.bpl.expect | 18 +- 7 files changed, 2001 insertions(+), 1957 deletions(-) (limited to 'Source') 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 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 && !x.isExtern)); - 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 && !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 = 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 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; + 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 && !x.isExtern)); + 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 && !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 = 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 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(); + 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); + } + } } \ 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 procMap; /* Original -> Duplicate */ - public Dictionary absyMap; /* Duplicate -> Original */ - public Dictionary implMap; /* Duplicate -> Original */ - public HashSet yieldingProcs; - public List impls; - - public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum) - { - this.moverTypeChecker = moverTypeChecker; - this.layerNum = layerNum; - this.enclosingProc = null; - this.enclosingImpl = null; - this.procMap = new Dictionary(); - this.absyMap = new Dictionary(); - this.implMap = new Dictionary(); - this.yieldingProcs = new HashSet(); - this.impls = new List(); - } - - private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List 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(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); - Dictionary map = new Dictionary(); - for (int i = 0; i < originalProc.InParams.Count; i++) - { - map[originalProc.InParams[i]] = callCmd.Ins[i]; - } - Substitution subst = Substituter.SubstitutionFromHashtable(map); - foreach (AssertCmd assertCmd in atomicActionInfo.thisGate) - { - newCmds.Add(Substituter.Apply(subst, assertCmd)); - } - } - } - newCmds.Add(callCmd); - } - - private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List 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 VisitCmdSeq(List cmdSeq) - { - List cmds = base.VisitCmdSeq(cmdSeq); - List newCmds = new List(); - 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(); - proc.Ensures = new List(); - Implementation impl; - AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; - if (atomicActionInfo != null) - { - CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.thisAction); - List cmds = new List(); - 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(new string[] { action.Blocks[0].Label }), - new List(new Block[] { action.Blocks[0] }))); - List newBlocks = new List(); - newBlocks.Add(newInitBlock); - newBlocks.AddRange(action.Blocks); - impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks); - } - else - { - Block newInitBlock = new Block(Token.NoToken, "_init", new List(), new ReturnCmd(Token.NoToken)); - List newBlocks = new List(); - newBlocks.Add(newInitBlock); - impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List(), 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(); - 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 absyMap; - Dictionary implMap; - HashSet yieldingProcs; - int layerNum; - List globalMods; - Dictionary asyncAndParallelCallDesugarings; - List yieldCheckerProcs; - List yieldCheckerImpls; - Procedure yieldProc; - - Variable pc; - Variable ok; - Expr alpha; - Expr beta; - HashSet 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(); - foreach (Variable g in moverTypeChecker.SharedVariables) - { - globalMods.Add(Expr.Ident(g)); - } - asyncAndParallelCallDesugarings = new Dictionary(); - yieldCheckerProcs = new List(); - yieldCheckerImpls = new List(); - yieldProc = null; - } - - private IEnumerable AvailableLinearVars(Absy absy) - { - return linearTypeChecker.AvailableLinearVars(absyMap[absy]); - } - - private CallCmd CallToYieldProc(IToken tok, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) - { - List exprSeq = new List(); - 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 inputs = new List(); - 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(), new List { 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(), inputs, new List(), new List(), new List(), new List()); - yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - } - CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List()); - yieldCallCmd.Proc = yieldProc; - return yieldCallCmd; - } - - private void AddCallToYieldProc(IToken tok, List newCmds, Dictionary ogOldGlobalMap, Dictionary 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 pcUpdateLHS = new List( - new AssignLhs[] { - new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), - new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)) - }); - List pcUpdateRHS = new List( - new Expr[] { - 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 ComputeAvailableExprs(IEnumerable availableLinearVars, Dictionary domainNameToInputVar) - { - Dictionary domainNameToExpr = new Dictionary(); - 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.Ident(v) }); - var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] }); - expr.Resolve(new ResolutionContext(null)); - expr.Typecheck(new TypecheckingContext(null)); - domainNameToExpr[domainName] = expr; - } - return domainNameToExpr; - } - - private void AddUpdatesToOldGlobalVars(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr) - { - List lhss = new List(); - List rhss = new List(); - 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 ogOldGlobalMap) - { - Expr bb = Expr.True; - foreach (Variable o in ogOldGlobalMap.Keys) - { - if (o is GlobalVariable && !frame.Contains(o)) continue; - bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); - bb.Type = Type.Bool; - } - return bb; - } - - private Expr OldEqualityExprForGlobals(Dictionary ogOldGlobalMap) - { - Expr bb = Expr.True; - foreach (Variable o in ogOldGlobalMap.Keys) - { - if (o is GlobalVariable && frame.Contains(o)) - { - bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); - bb.Type = Type.Bool; - } - } - return bb; - } - - private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) - { - AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); - - 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 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 newCmds, ParCallCmd parCallCmd) - { - List parallelCalleeNames = new List(); - List ins = new List(); - List outs = new List(); - 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 inParams = new List(); - List outParams = new List(); - List requiresSeq = new List(); - List ensuresSeq = new List(); - int count = 0; - foreach (CallCmd callCmd in parCallCmd.CallCmds) - { - Dictionary map = new Dictionary(); - 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(), 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> yields) - { - if (yields.Count == 0) return; - - Dictionary map = new Dictionary(); - 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 locals = new List(); - List inputs = new List(); - 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 ogOldLocalMap = new Dictionary(); - Dictionary assumeMap = new Dictionary(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 yieldCheckerBlocks = new List(); - List labels = new List(); - List labelTargets = new List(); - Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); - labels.Add(yieldCheckerBlock.Label); - labelTargets.Add(yieldCheckerBlock); - yieldCheckerBlocks.Add(yieldCheckerBlock); - int yieldCount = 0; - foreach (List cs in yields) - { - List newCmds = new List(); - 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(), 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(), new List(), new List(), new List()); - yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - yieldCheckerProcs.Add(yieldCheckerProc); - - // Create the yield checker implementation - var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List(), locals, yieldCheckerBlocks); - yieldCheckerImpl.Proc = yieldCheckerProc; - yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); - yieldCheckerImpls.Add(yieldCheckerImpl); - } - - private bool IsYieldingHeader(Graph 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 ComputeYieldingLoopHeaders(Implementation impl, out HashSet yieldingHeaders) - { - Graph 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(); - IEnumerable 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 newLocalVars, - out Dictionary domainNameToInputVar, out Dictionary domainNameToLocalVar, out Dictionary ogOldGlobalMap) - { - pc = null; - ok = null; - alpha = null; - beta = null; - frame = null; - - newLocalVars = new List(); - Program program = linearTypeChecker.program; - ogOldGlobalMap = new Dictionary(); - 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 alwaysMap = new Dictionary(); - for (int i = 0; i < originalProc.InParams.Count; i++) - { - alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]); - } - for (int i = 0; i < originalProc.OutParams.Count; i++) - { - alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]); - } - Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap); - Dictionary foroldMap = new Dictionary(); - foreach (IdentifierExpr ie in globalMods) - { - foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); - } - Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); - frame = new HashSet(moverTypeChecker.SharedVariables); - HashSet introducedVars = new HashSet(); - 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(); - domainNameToLocalVar = new Dictionary(); - { - 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 yieldingHeaders; - Graph graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders); - - List newLocalVars; - Dictionary domainNameToInputVar, domainNameToLocalVar; - Dictionary ogOldGlobalMap; - SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap); - - List> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); - - List 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 ogOldGlobalMap, Dictionary domainNameToLocalVar) - { - CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar); - Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken)); - List newBlocks = new List(); - foreach (Block b in impl.Blocks) - { - TransferCmd transferCmd = b.TransferCmd; - List newCmds = new List(); - 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(); - transferCmd = new GotoCmd(Token.NoToken, new List(new string[] { newBlock.Label, yieldCheckBlock.Label }), - new List(new Block[] { newBlock, yieldCheckBlock })); - newBlocks.Add(newBlock); - } - } - b.Cmds = newCmds; - b.TransferCmd = transferCmd; - } - impl.Blocks.AddRange(newBlocks); - impl.Blocks.Add(yieldCheckBlock); - } - - private List> CollectAndDesugarYields(Implementation impl, - Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) - { - // Collect the yield predicates and desugar yields - List> yields = new List>(); - List cmds = new List(); - foreach (Block b in impl.Blocks) - { - YieldCmd yieldCmd = null; - List newCmds = new List(); - 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(); - } - 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(), new List()); - } - 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 availableLinearVars = new HashSet(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 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 availableLinearVars = new HashSet(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 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(); - } - } - 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 graph, HashSet yieldingHeaders, - Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap, - out List oldPcs, out List oldOks) - { - oldPcs = new List(); - oldOks = new List(); - 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 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( - new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }), - new List(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) }))); - } - AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); - } - List newCmds = new List(); - if (pc != null) - { - 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 oldPcs, List oldOks, - Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) - { - // Add initial block - List lhss = new List(); - List rhss = new List(); - if (pc != null) - { - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); - rhss.Add(Expr.False); - 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 domainNameToExpr = new Dictionary(); - 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.Ident(v) }); - domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { 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 { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] })); - impl.Blocks.Insert(0, initBlock); - } - } - - private void AddYieldProcAndImpl(List decls) - { - if (yieldProc == null) return; - - Program program = linearTypeChecker.program; - List inputs = new List(); - 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(), new List { 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 blocks = new List(); - TransferCmd transferCmd = new ReturnCmd(Token.NoToken); - if (yieldCheckerProcs.Count > 0) - { - List blockTargets = new List(); - List labelTargets = new List(); - int labelCount = 0; - foreach (Procedure proc in yieldCheckerProcs) - { - List exprSeq = new List(); - foreach (Variable v in inputs) - { - exprSeq.Add(Expr.Ident(v)); - } - CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List()); - callCmd.Proc = proc; - string label = string.Format("L_{0}", labelCount++); - Block block = new Block(Token.NoToken, label, new List { 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(), transferCmd)); - - var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List(), inputs, new List(), new List(), 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 Collect() - { - List decls = new List(); - 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 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 procMap; /* Original -> Duplicate */ + public Dictionary absyMap; /* Duplicate -> Original */ + public Dictionary implMap; /* Duplicate -> Original */ + public HashSet yieldingProcs; + public List impls; + + public MyDuplicator(MoverTypeChecker moverTypeChecker, int layerNum) + { + this.moverTypeChecker = moverTypeChecker; + this.layerNum = layerNum; + this.enclosingProc = null; + this.enclosingImpl = null; + this.procMap = new Dictionary(); + this.absyMap = new Dictionary(); + this.implMap = new Dictionary(); + this.yieldingProcs = new HashSet(); + this.impls = new List(); + } + + private void ProcessCallCmd(CallCmd originalCallCmd, CallCmd callCmd, List 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(new IdentifierExpr[] { Expr.Ident(dummyLocalVar) }))); + Dictionary map = new Dictionary(); + for (int i = 0; i < originalProc.InParams.Count; i++) + { + map[originalProc.InParams[i]] = callCmd.Ins[i]; + } + Substitution subst = Substituter.SubstitutionFromHashtable(map); + foreach (AssertCmd assertCmd in atomicActionInfo.gate) + { + newCmds.Add(Substituter.Apply(subst, assertCmd)); + } + } + } + newCmds.Add(callCmd); + } + + private void ProcessParCallCmd(ParCallCmd originalParCallCmd, ParCallCmd parCallCmd, List 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 VisitCmdSeq(List cmdSeq) + { + List cmds = base.VisitCmdSeq(cmdSeq); + List newCmds = new List(); + 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(); + proc.Ensures = new List(); + Implementation impl; + AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo; + if (atomicActionInfo != null) + { + CodeExpr action = (CodeExpr)VisitCodeExpr(atomicActionInfo.action); + List cmds = new List(); + 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(new string[] { action.Blocks[0].Label }), + new List(new Block[] { action.Blocks[0] }))); + List newBlocks = new List(); + newBlocks.Add(newInitBlock); + newBlocks.AddRange(action.Blocks); + impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, action.LocVars, newBlocks); + } + else + { + Block newInitBlock = new Block(Token.NoToken, "_init", new List(), new ReturnCmd(Token.NoToken)); + List newBlocks = new List(); + newBlocks.Add(newInitBlock); + impl = new Implementation(Token.NoToken, proc.Name, node.TypeParameters, node.InParams, node.OutParams, new List(), 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(); + 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 absyMap; + Dictionary implMap; + HashSet yieldingProcs; + int layerNum; + List globalMods; + Dictionary asyncAndParallelCallDesugarings; + List yieldCheckerProcs; + List yieldCheckerImpls; + Procedure yieldProc; + + Variable pc; + Variable ok; + Expr alpha; + Expr beta; + HashSet 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(); + foreach (Variable g in moverTypeChecker.SharedVariables) + { + globalMods.Add(Expr.Ident(g)); + } + asyncAndParallelCallDesugarings = new Dictionary(); + yieldCheckerProcs = new List(); + yieldCheckerImpls = new List(); + yieldProc = null; + } + + private IEnumerable AvailableLinearVars(Absy absy) + { + return linearTypeChecker.AvailableLinearVars(absyMap[absy]); + } + + private CallCmd CallToYieldProc(IToken tok, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar) + { + List exprSeq = new List(); + 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 inputs = new List(); + 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(), new List { 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(), inputs, new List(), new List(), new List(), new List()); + yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + } + CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List()); + yieldCallCmd.Proc = yieldProc; + return yieldCallCmd; + } + + private void AddCallToYieldProc(IToken tok, List newCmds, Dictionary ogOldGlobalMap, Dictionary 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 pcUpdateLHS = new List( + new AssignLhs[] { + new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)), + new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)) + }); + List pcUpdateRHS = new List( + new Expr[] { + 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 ComputeAvailableExprs(IEnumerable availableLinearVars, Dictionary domainNameToInputVar) + { + Dictionary domainNameToExpr = new Dictionary(); + 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.Ident(v) }); + var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { ie, domainNameToExpr[domainName] }); + expr.Resolve(new ResolutionContext(null)); + expr.Typecheck(new TypecheckingContext(null)); + domainNameToExpr[domainName] = expr; + } + return domainNameToExpr; + } + + private void AddUpdatesToOldGlobalVars(List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToLocalVar, Dictionary domainNameToExpr) + { + List lhss = new List(); + List rhss = new List(); + 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 ogOldGlobalMap) + { + Expr bb = Expr.True; + foreach (Variable o in ogOldGlobalMap.Keys) + { + if (o is GlobalVariable && !frame.Contains(o)) continue; + bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); + bb.Type = Type.Bool; + } + return bb; + } + + private Expr OldEqualityExprForGlobals(Dictionary ogOldGlobalMap) + { + Expr bb = Expr.True; + foreach (Variable o in ogOldGlobalMap.Keys) + { + if (o is GlobalVariable && frame.Contains(o)) + { + bb = Expr.And(bb, Expr.Eq(Expr.Ident(o), Expr.Ident(ogOldGlobalMap[o]))); + bb.Type = Type.Bool; + } + } + return bb; + } + + private void DesugarYield(YieldCmd yieldCmd, List cmds, List newCmds, Dictionary ogOldGlobalMap, Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar) + { + AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar); + + 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 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 newCmds, ParCallCmd parCallCmd) + { + List parallelCalleeNames = new List(); + List ins = new List(); + List outs = new List(); + 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 inParams = new List(); + List outParams = new List(); + List requiresSeq = new List(); + List ensuresSeq = new List(); + int count = 0; + foreach (CallCmd callCmd in parCallCmd.CallCmds) + { + Dictionary map = new Dictionary(); + 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(), 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> yields) + { + if (yields.Count == 0) return; + + Dictionary map = new Dictionary(); + 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 locals = new List(); + List inputs = new List(); + 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 ogOldLocalMap = new Dictionary(); + Dictionary assumeMap = new Dictionary(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 yieldCheckerBlocks = new List(); + List labels = new List(); + List labelTargets = new List(); + Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); + labels.Add(yieldCheckerBlock.Label); + labelTargets.Add(yieldCheckerBlock); + yieldCheckerBlocks.Add(yieldCheckerBlock); + int yieldCount = 0; + foreach (List cs in yields) + { + List newCmds = new List(); + 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(), 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(), new List(), new List(), new List()); + yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + yieldCheckerProcs.Add(yieldCheckerProc); + + // Create the yield checker implementation + var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, impl.TypeParameters, inputs, new List(), locals, yieldCheckerBlocks); + yieldCheckerImpl.Proc = yieldCheckerProc; + yieldCheckerImpl.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); + yieldCheckerImpls.Add(yieldCheckerImpl); + } + + private bool IsYieldingHeader(Graph 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 ComputeYieldingLoopHeaders(Implementation impl, out HashSet yieldingHeaders) + { + Graph 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(); + IEnumerable 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 newLocalVars, + out Dictionary domainNameToInputVar, out Dictionary domainNameToLocalVar, out Dictionary ogOldGlobalMap) + { + pc = null; + ok = null; + alpha = null; + beta = null; + frame = null; + + newLocalVars = new List(); + Program program = linearTypeChecker.program; + ogOldGlobalMap = new Dictionary(); + 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 alwaysMap = new Dictionary(); + for (int i = 0; i < originalProc.InParams.Count; i++) + { + alwaysMap[originalProc.InParams[i]] = Expr.Ident(impl.InParams[i]); + } + for (int i = 0; i < originalProc.OutParams.Count; i++) + { + alwaysMap[originalProc.OutParams[i]] = Expr.Ident(impl.OutParams[i]); + } + Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap); + Dictionary foroldMap = new Dictionary(); + foreach (IdentifierExpr ie in globalMods) + { + foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]); + } + Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); + frame = new HashSet(moverTypeChecker.SharedVariables); + HashSet introducedVars = new HashSet(); + 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(); + domainNameToLocalVar = new Dictionary(); + { + 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 yieldingHeaders; + Graph graph = ComputeYieldingLoopHeaders(impl, out yieldingHeaders); + + List newLocalVars; + Dictionary domainNameToInputVar, domainNameToLocalVar; + Dictionary ogOldGlobalMap; + SetupRefinementCheck(impl, out newLocalVars, out domainNameToInputVar, out domainNameToLocalVar, out ogOldGlobalMap); + + List> yields = CollectAndDesugarYields(impl, domainNameToInputVar, domainNameToLocalVar, ogOldGlobalMap); + + List 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 ogOldGlobalMap, Dictionary domainNameToLocalVar) + { + CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar); + Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken)); + List newBlocks = new List(); + foreach (Block b in impl.Blocks) + { + TransferCmd transferCmd = b.TransferCmd; + List newCmds = new List(); + 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(); + transferCmd = new GotoCmd(Token.NoToken, new List(new string[] { newBlock.Label, yieldCheckBlock.Label }), + new List(new Block[] { newBlock, yieldCheckBlock })); + newBlocks.Add(newBlock); + } + } + b.Cmds = newCmds; + b.TransferCmd = transferCmd; + } + impl.Blocks.AddRange(newBlocks); + impl.Blocks.Add(yieldCheckBlock); + } + + private List> CollectAndDesugarYields(Implementation impl, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) + { + // Collect the yield predicates and desugar yields + List> yields = new List>(); + List cmds = new List(); + foreach (Block b in impl.Blocks) + { + YieldCmd yieldCmd = null; + List newCmds = new List(); + 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(); + } + 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(), new List()); + } + 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 availableLinearVars = new HashSet(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 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 availableLinearVars = new HashSet(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 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(); + } + } + 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 graph, HashSet yieldingHeaders, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap, + out List oldPcs, out List oldOks) + { + oldPcs = new List(); + oldOks = new List(); + 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 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( + new AssignLhs[] { new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldPc)), new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOk)) }), + new List(new Expr[] { Expr.Ident(pc), Expr.Ident(ok) }))); + } + AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr); + } + List newCmds = new List(); + if (pc != null) + { + 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 oldPcs, List oldOks, + Dictionary domainNameToInputVar, Dictionary domainNameToLocalVar, Dictionary ogOldGlobalMap) + { + // Add initial block + List lhss = new List(); + List rhss = new List(); + if (pc != null) + { + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); + rhss.Add(Expr.False); + 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 domainNameToExpr = new Dictionary(); + 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.Ident(v) }); + domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List { 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 { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] })); + impl.Blocks.Insert(0, initBlock); + } + } + + private void AddYieldProcAndImpl(List decls) + { + if (yieldProc == null) return; + + Program program = linearTypeChecker.program; + List inputs = new List(); + 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(), new List { 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 blocks = new List(); + TransferCmd transferCmd = new ReturnCmd(Token.NoToken); + if (yieldCheckerProcs.Count > 0) + { + List blockTargets = new List(); + List labelTargets = new List(); + int labelCount = 0; + foreach (Procedure proc in yieldCheckerProcs) + { + List exprSeq = new List(); + foreach (Variable v in inputs) + { + exprSeq.Add(Expr.Ident(v)); + } + CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List()); + callCmd.Proc = proc; + string label = string.Format("L_{0}", labelCount++); + Block block = new Block(Token.NoToken, label, new List { 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(), transferCmd)); + + var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new List(), inputs, new List(), new List(), 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 Collect() + { + List decls = new List(); + 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 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 gate; + public CodeExpr action; public List thisGate; public CodeExpr thisAction; public List thisInParams; @@ -61,6 +63,8 @@ namespace Microsoft.Boogie public HashSet modifiedGlobalVars; public HashSet gateUsedGlobalVars; public bool hasAssumeCmd; + public Dictionary thisMap; + public Dictionary 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(); + this.action = ensures.Condition as CodeExpr; this.thisGate = new List(); - this.thisAction = codeExpr; this.thisInParams = new List(); this.thisOutParams = new List(); this.thatGate = new List(); this.thatInParams = new List(); this.thatOutParams = new List(); this.hasAssumeCmd = false; - - foreach (Block block in codeExpr.Blocks) + this.thisMap = new Dictionary(); + this.thatMap = new Dictionary(); + + 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 map = new Dictionary(); 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 thisLocVars = new List(); List thatLocVars = new List(); - 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(collector.usedVars.Where(x => x is GlobalVariable)); } + + List modifiedVars = new List(); + foreach (Block block in this.action.Blocks) + { + block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars)); + } + this.modifiedGlobalVars = new HashSet(modifiedVars.Where(x => x is GlobalVariable)); + + { + VariableCollector collector = new VariableCollector(); + this.gate.ForEach(assertCmd => collector.Visit(assertCmd)); + this.gateUsedGlobalVars = new HashSet(collector.usedVars.Where(x => x is GlobalVariable)); + } + } + + private List SubstituteBlocks(List blocks, Substitution subst, string blockLabelPrefix) + { Dictionary blockMap = new Dictionary(); - List thatBlocks = new List(); - foreach (Block block in thisAction.Blocks) + List otherBlocks = new List(); + foreach (Block block in blocks) { List otherCmds = new List(); 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 thatGotoCmdLabelTargets = new List(); - List thatGotoCmdLabelNames = new List(); + List otherGotoCmdLabelTargets = new List(); + List otherGotoCmdLabelNames = new List(); 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(collector.usedVars.Where(x => x is GlobalVariable)); - } - - List modifiedVars = new List(); - foreach (Block block in codeExpr.Blocks) - { - block.Cmds.ForEach(cmd => cmd.AddAssignedVariables(modifiedVars)); - } - this.modifiedGlobalVars = new HashSet(modifiedVars.Where(x => x is GlobalVariable)); - - { - VariableCollector collector = new VariableCollector(); - this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd)); - this.gateUsedGlobalVars = new HashSet(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 -- cgit v1.2.3