From 5db34109bbb72d290239dfdb571d321fe3f1c48c Mon Sep 17 00:00:00 2001 From: qadeer Date: Wed, 1 Dec 2010 05:43:17 +0000 Subject: Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln --- Source/AbsInt/AbsInt.csproj | 8 - Source/AbsInt/AbstractInterpretation.cs | 150 +----------- Source/Core/Absy.cs | 16 +- Source/Core/AbsyCmd.cs | 6 +- Source/Core/CommandLineOptions.cs | 3 +- Source/Core/Core.csproj | 12 - Source/Core/DeadVarElim.cs | 211 +++++++++------- Source/Core/LoopUnroll.cs | 5 +- Source/Core/ResolutionContext.cs | 1 - Source/Core/Xml.cs | 5 +- Source/DafnyDriver/DafnyDriver.cs | 418 ++++++++++++++------------------ Source/DafnyDriver/DafnyDriver.csproj | 12 - Source/Graph/Graph.cs | 324 +++++++++++-------------- Source/Graph/Graph.csproj | 4 - Source/Provers/SMTLib/SMTLib.csproj | 4 - Source/Provers/Simplify/Simplify.csproj | 4 - Source/Provers/Z3/Z3.csproj | 4 - Source/Provers/Z3api/ContextLayer.cs | 1 - Source/Provers/Z3api/ProverLayer.cs | 1 - Source/Provers/Z3api/SafeContext.cs | 1 - Source/Provers/Z3api/StubContext.cs | 1 - Source/Provers/Z3api/TypeAdapter.cs | 1 - Source/Provers/Z3api/Z3api.csproj | 4 - Source/VCExpr/TypeErasureArguments.cs | 4 +- Source/VCExpr/VCExpr.csproj | 4 - Source/VCGeneration/StratifiedVC.cs | 12 +- Source/VCGeneration/VCGeneration.csproj | 8 - Test/test15/Answer | 6 +- 28 files changed, 480 insertions(+), 750 deletions(-) diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj index 4054951f..433195a6 100644 --- a/Source/AbsInt/AbsInt.csproj +++ b/Source/AbsInt/AbsInt.csproj @@ -100,14 +100,6 @@ - - False - ..\..\Binaries\System.Compiler.dll - - - False - ..\..\Binaries\System.Compiler.Framework.dll - 3.5 diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs index 827bd070..e29a6d4a 100644 --- a/Source/AbsInt/AbstractInterpretation.cs +++ b/Source/AbsInt/AbstractInterpretation.cs @@ -11,7 +11,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { using System.Diagnostics; using System.Diagnostics.Contracts; using Microsoft.Boogie; - using Cci = System.Compiler; + using System.Linq; using AI = Microsoft.AbstractInterpretationFramework; @@ -22,7 +22,6 @@ namespace Microsoft.Boogie.AbstractInterpretation { private AI.Lattice lattice; private Queue procWorkItems; //PM: changed to generic queue private Queue/**/ callReturnWorkItems; - private Cci.IRelation/**/ procedureImplementations; [ContractInvariantMethod] void ObjectInvariant() { @@ -71,120 +70,20 @@ namespace Microsoft.Boogie.AbstractInterpretation { this.callReturnWorkItems = new Queue(); } - private Cci.IGraphNavigator ComputeCallGraph(Program program) { + private Dictionary ComputeProcImplMap(Program program) { Contract.Requires(program != null); - Contract.Ensures(this.procedureImplementations != null); // Since implementations call procedures (impl. signatures) // rather than directly calling other implementations, we first // need to compute which implementations implement which // procedures and remember which implementations call which // procedures. - Cci.IMutableRelation/**/ callsProcedure = new Cci.Relation(); - Cci.IMutableRelation/**/ implementsProcedure = new Cci.Relation(); - this.procedureImplementations = implementsProcedure; + return program + .TopLevelDeclarations + .Where(d => d is Implementation).Select(i => (Implementation)i) + .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc); - // ArrayList publics = new ArrayList(); - // publicImpls = publics; - - foreach (Declaration member in program.TopLevelDeclarations) { - Implementation impl = member as Implementation; - if (impl != null) { - implementsProcedure.Add(impl.Proc, impl); - // if (impl.IsPublic) { publics.Add(impl); } // PR: what does "IsPublic" stand for? - - foreach (Block block in impl.Blocks) { - foreach (Cmd cmd in block.Cmds) { - CallCmd call = cmd as CallCmd; - if (call != null) { - callsProcedure.Add(impl, call.Proc); - } - } - } - } - } - - // Now compute a graph from implementations to implementations. - - Cci.GraphBuilder callGraph = new Cci.GraphBuilder(); - - IEnumerable callerImpls = callsProcedure.GetKeys(); - Contract.Assume(callerImpls != null); // because of non-generic collection - foreach (Implementation caller in callerImpls) { - IEnumerable callerProcs = callsProcedure.GetValues(caller); - Contract.Assume(callerProcs != null); // because of non-generic collection - foreach (Procedure callee in callerProcs) { - IEnumerable calleeImpls = implementsProcedure.GetValues(callee); - Contract.Assume(calleeImpls != null); // because of non-generic collection - foreach (Implementation calleeImpl in calleeImpls) { - callGraph.AddEdge(caller, calleeImpl); - } - } - } - - return callGraph; - } - -#if OLDCODE - public void ComputeImplementationInvariants (Implementation impl) - { - // process each procedure implementation by recursively processing the first (entry) block... - ComputeBlockInvariants(impl.Blocks[0], lattice.Top); - - // compute the procedure invariant by joining all terminal block invariants... - AI.Lattice.Element post = lattice.Bottom; - foreach (Block block in impl.Blocks) - { - if (block.TransferCmd is ReturnCmd) - { - AI.Lattice.Element postValue = block.PostInvariantBuckets[invariantIndex]; - Debug.Assert(postValue != null); - post = post.Join(postValue); - } - } - impl.PostInvariant = post; - - // Now update the procedure to reflect the new properties - // of this implementation. - - if (impl.Proc.PreInvariant <= impl.PreInvariant) - { - // Strengthen the precondition - impl.Proc.PreInvariant = impl.PreInvariant; - foreach (Implementation otherImpl in this.procedureImplementations.GetValues(impl.Proc)) - { - if (otherImpl == impl) { continue; } - if (otherImpl.PreInvariant <= impl.Proc.PreInvariant) - { - // If another implementation of the same procedure has - // a weaker precondition, re-do it with the stronger - // precondition. - otherImpl.PreInvariant = impl.Proc.PreInvariant; - this.implWorkItems.Enqueue(otherImpl); - } - } - } } -#endif - - -#if NOTYET - public void ComputeSccInvariants (IEnumerable/**/ implementations) - { - Debug.Assert(this.implWorkItems.Count == 0); // no work left over from last SCC - - foreach (Implementation impl in implementations) - { - impl.AbstractFunction = AbstractFunction.Empty.WithPair(this.lattice.Bottom, this.lattice.Bottom); - this.implWorkItems.Enqueue(impl); - } - - while (this.implWorkItems.Count > 0) // until fixed point reached - { - Implementation impl = (Implementation)this.implWorkItems.Dequeue(); - } - } -#endif public AI.Lattice.Element ApplyProcedureSummary(CallCmd call, Implementation caller, AI.Lattice.Element knownAtCallSite, CallSite callSite) { Contract.Requires(call.Proc != null); @@ -254,12 +153,14 @@ namespace Microsoft.Boogie.AbstractInterpretation { return this.lattice.Meet(atReturn, knownAtCallSite); } + /* private Cci.IGraphNavigator callGraph; public Cci.IGraphNavigator CallGraph { get { return this.callGraph; } } + */ /// /// Compute the invariants for the program using the underlying abstract domain @@ -267,29 +168,10 @@ namespace Microsoft.Boogie.AbstractInterpretation { public void ComputeProgramInvariants(Program program) { Contract.Requires(program != null); -#if NOT_YET - Cci.IGraphNavigator callGraph = -#endif - - callGraph = this.ComputeCallGraph(program); - Contract.Assert(this.procedureImplementations != null); - Cci.IRelation procedureImplementations = this.procedureImplementations;//Non-nullability was already asserted in + Dictionary procedureImplementations = ComputeProcImplMap(program); //the line above, ergo there is no need for //an assert after this statement to maintain //the non-null type. -#if NOT_YET - IEnumerable/**/ sccs = - StronglyConnectedComponent.ConstructSCCs(publicImpls, callGraph); - - IList/**/ sortedSccs = - GraphUtil.TopologicallySortComponentGraph(sccs); - - // Go bottom-up through the SCCs of the call graph - foreach (IStronglyConnectedComponent scc in sortedSccs) - { - this.ComputeSccInvariants(scc.Nodes); - } -#endif AI.Lattice.Element initialElement = this.lattice.Top; Contract.Assert(initialElement != null); // Gather all the axioms to create the initial lattice element @@ -316,8 +198,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { ProcedureWorkItem workItem = this.procWorkItems.Dequeue(); ProcedureSummaryEntry summaryEntry = cce.NonNull(workItem.Proc.Summary[workItem.Index]); - - if (cce.NonNull(procedureImplementations.GetValues(workItem.Proc)).Count == 0) { + if (!procedureImplementations.ContainsKey(workItem.Proc)) { // This procedure has no given implementations. We therefore treat the procedure // according to its specification only. @@ -347,7 +228,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { } // For each implementation in the procedure... - foreach (Implementation impl in cce.NonNull(procedureImplementations.GetValues(workItem.Proc))) { + foreach (Implementation impl in cce.NonNull(procedureImplementations[workItem.Proc])) { // process each procedure implementation by recursively processing the first (entry) block... cce.NonNull(impl.Blocks[0]).Lattice = lattice; ComputeBlockInvariants(impl, cce.NonNull(impl.Blocks[0]), summaryEntry.OnEntry, summaryEntry); @@ -1040,16 +921,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { Contract.Requires(lattice != null); AbstractionEngine engine = new AbstractionEngine(lattice); engine.ComputeProgramInvariants(program); - callGraph = engine.CallGraph; - } - private static Cci.IGraphNavigator callGraph; - public static Cci.IGraphNavigator CallGraph { - get { - return callGraph; - } } - - } } // namespace \ No newline at end of file diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 8f70766f..64b15be7 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -9,8 +9,8 @@ namespace Microsoft.Boogie.AbstractInterpretation { using System.Diagnostics; using System.Diagnostics.Contracts; - using CCI = System.Compiler; using System.Collections; + using System.Collections.Generic; using AI = Microsoft.AbstractInterpretationFramework; public class CallSite { @@ -45,7 +45,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { public AI.Lattice/*!*/ Lattice; public AI.Lattice.Element/*!*/ OnEntry; public AI.Lattice.Element/*!*/ OnExit; - public CCI.IMutableSet/**//*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints + public HashSet/*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Lattice != null); @@ -61,7 +61,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { this.Lattice = lattice; this.OnEntry = onEntry; this.OnExit = lattice.Bottom; - this.ReturnPoints = new CCI.HashSet(); + this.ReturnPoints = new HashSet(); // base(); } @@ -407,7 +407,7 @@ namespace Microsoft.Boogie { Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr VariableSeq/*!*/ targets = new VariableSeq(); - Set footprint = new Set(); + HashSet footprint = new HashSet(); foreach (Block/*!*/ b in g.BackEdgeNodes(header)) { @@ -422,7 +422,7 @@ namespace Microsoft.Boogie { VariableCollector c = new VariableCollector(); c.Visit(cmd); - footprint.AddRange(c.usedVars); + footprint.UnionWith(c.usedVars); } } } @@ -531,7 +531,7 @@ namespace Microsoft.Boogie { Contract.Assert(header != null); LoopProcedure loopProc = loopHeaderToLoopProc[header]; Dictionary blockMap = new Dictionary(); - Set dummyBlocks = new Set(); + HashSet dummyBlocks = new HashSet(); CodeCopier codeCopier = new CodeCopier(loopHeaderToSubstMap[header]); // fix me VariableSeq inputs = loopHeaderToInputs[header]; @@ -696,7 +696,7 @@ namespace Microsoft.Boogie { { // Do a BFS to find all reachable blocks List reachableBlocks = new List(); - Set visited = new Set(); + HashSet visited = new HashSet(); List worklist = new List(); visited.Add(impl.Blocks[0].Label); @@ -2806,7 +2806,7 @@ namespace Microsoft.Boogie { public void PruneUnreachableBlocks() { ArrayList /*Block!*/ visitNext = new ArrayList /*Block!*/ (); List reachableBlocks = new List(); - System.Compiler.IMutableSet /*Block!*/ reachable = new System.Compiler.HashSet /*Block!*/ (); // the set of elements in "reachableBlocks" + HashSet reachable = new HashSet(); // the set of elements in "reachableBlocks" visitNext.Add(this.Blocks[0]); while (visitNext.Count != 0) { diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 35929311..afd171b9 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -78,7 +78,7 @@ namespace Microsoft.Boogie { public readonly IToken/*!*/ EndCurly; public StmtList ParentContext; public BigBlock ParentBigBlock; - public Set/*!*/ Labels = new Set(); + public HashSet/*!*/ Labels = new HashSet(); [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(EndCurly != null); @@ -233,7 +233,7 @@ namespace Microsoft.Boogie { List blocks; string/*!*/ prefix = "anon"; int anon = 0; - Set allLabels = new Set(); + HashSet allLabels = new HashSet(); Errors/*!*/ errorHandler; [ContractInvariantMethod] void ObjectInvariant() { @@ -784,7 +784,7 @@ namespace Microsoft.Boogie { // VC generation and SCC computation public BlockSeq/*!*/ Predecessors; - public Set liveVarsBefore; + public HashSet liveVarsBefore; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Label != null); diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index b63b82cc..42bd1406 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -10,7 +10,6 @@ using System.Collections.Specialized; using System.IO; using System.Diagnostics; using System.Diagnostics.Contracts; -using Cci = System.Compiler; namespace Microsoft.Boogie { public class CommandLineOptions { @@ -1543,6 +1542,7 @@ namespace Microsoft.Boogie { return Contract.Exists(procsToCheck, s => 0 <= methodFullname.IndexOf(s)); } +#if CCI public bool UserWantsToTranslateRoutine(Cci.Method method, string methodFullname) { Contract.Requires(methodFullname != null); Contract.Requires(method != null); @@ -1674,6 +1674,7 @@ namespace Microsoft.Boogie { } return null; } +#endif class CommandLineParseState { public string s; diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index ab4857dc..6cea383c 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -103,19 +103,7 @@ False ..\..\Binaries\FSharp.Core.dll - - False - ..\..\Binaries\Microsoft.SpecSharp.Runtime.dll - - - False - ..\..\Binaries\System.Compiler.dll - - - False - ..\..\Binaries\System.Compiler.Framework.dll - diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 694ddc00..40be3798 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -41,7 +41,7 @@ namespace Microsoft.Boogie { public class ModSetCollector : StandardVisitor { static Procedure proc; - static Dictionary/*!*/>/*!*/ modSets; + static Dictionary/*!*/>/*!*/ modSets; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(modSets)); @@ -60,9 +60,9 @@ namespace Microsoft.Boogie { } Console.WriteLine("Number of procedures = {0}", procCount); - modSets = new Dictionary/*!*/>(); + modSets = new Dictionary/*!*/>(); - Set implementedProcs = new Set(); + HashSet implementedProcs = new HashSet(); foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) { Contract.Assert(decl != null); if (decl is Implementation) { @@ -155,7 +155,7 @@ namespace Microsoft.Boogie { if (var.Name == "alloc") return; if (!modSets.ContainsKey(localProc)) { - modSets[localProc] = new Set(); + modSets[localProc] = new HashSet(); } if (modSets[localProc].Contains(var)) return; @@ -165,8 +165,8 @@ namespace Microsoft.Boogie { } public class VariableCollector : StandardVisitor { - public System.Collections.Generic.Set/*!*/ usedVars; - public System.Collections.Generic.Set/*!*/ oldVarsUsed; + public HashSet/*!*/ usedVars; + public HashSet/*!*/ oldVarsUsed; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(usedVars)); @@ -176,8 +176,8 @@ namespace Microsoft.Boogie { int insideOldExpr; public VariableCollector() { - usedVars = new System.Collections.Generic.Set(); - oldVarsUsed = new System.Collections.Generic.Set(); + usedVars = new System.Collections.Generic.HashSet(); + oldVarsUsed = new System.Collections.Generic.HashSet(); insideOldExpr = 0; } @@ -210,11 +210,11 @@ namespace Microsoft.Boogie { blockCoalescer.Visit(program); } - private static Set/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) { + private static HashSet/*!*/ ComputeMultiPredecessorBlocks(Implementation/*!*/ impl) { Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - Set visitedBlocks = new Set(); - Set multiPredBlocks = new Set(); + 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) { @@ -247,10 +247,10 @@ namespace Microsoft.Boogie { //Console.WriteLine("Procedure {0}", impl.Name); //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count); - Set multiPredBlocks = ComputeMultiPredecessorBlocks(impl); + HashSet multiPredBlocks = ComputeMultiPredecessorBlocks(impl); Contract.Assert(cce.NonNullElements(multiPredBlocks)); - Set visitedBlocks = new Set(); - Set removedBlocks = new Set(); + HashSet visitedBlocks = new HashSet(); + HashSet removedBlocks = new HashSet(); Stack dfsStack = new Stack(); dfsStack.Push(impl.Blocks[0]); while (dfsStack.Count > 0) { @@ -333,14 +333,14 @@ namespace Microsoft.Boogie { IEnumerable sortedNodes = dag.TopologicalSort(); foreach (Block/*!*/ block in sortedNodes) { Contract.Assert(block != null); - Set/*!*/ liveVarsAfter = new Set(); + HashSet/*!*/ liveVarsAfter = new HashSet(); 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.AddRange(succ.liveVarsBefore); + liveVarsAfter.UnionWith(succ.liveVarsBefore); } } } @@ -365,7 +365,7 @@ namespace Microsoft.Boogie { } // perform in place update of liveSet - public static void Propagate(Cmd cmd, Set/*!*/ liveSet) { + public static void Propagate(Cmd cmd, HashSet/*!*/ liveSet) { Contract.Requires(cmd != null); Contract.Requires(cce.NonNullElements(liveSet)); if (cmd is AssignCmd) { @@ -373,7 +373,7 @@ namespace Microsoft.Boogie { // 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 - Set indexSet = new Set(); + HashSet indexSet = new HashSet(); int index = 0; foreach (AssignLhs/*!*/ lhs in assignCmd.Lhss) { Contract.Assert(lhs != null); @@ -394,7 +394,7 @@ namespace Microsoft.Boogie { if (indexSet.Contains(index)) { VariableCollector/*!*/ collector = new VariableCollector(); collector.Visit(expr); - liveSet.AddRange(collector.usedVars); + liveSet.UnionWith(collector.usedVars); AssignLhs lhs = assignCmd.Lhss[index]; if (lhs is MapAssignLhs) { // If the target is a map, then all indices are also read @@ -402,7 +402,7 @@ namespace Microsoft.Boogie { foreach (Expr e in malhs.Indexes) { VariableCollector/*!*/ c = new VariableCollector(); c.Visit(e); - liveSet.AddRange(c.usedVars); + liveSet.UnionWith(c.usedVars); } } } @@ -427,7 +427,7 @@ namespace Microsoft.Boogie { } else { VariableCollector/*!*/ collector = new VariableCollector(); collector.Visit(predicateCmd.Expr); - liveSet.AddRange(collector.usedVars); + liveSet.UnionWith(collector.usedVars); } } else if (cmd is CommentCmd) { // comments are just for debugging and don't affect verification @@ -470,8 +470,8 @@ namespace Microsoft.Boogie { public class GenKillWeight { // lambda S. (S - kill) union gen - Set/*!*/ gen; - Set/*!*/ kill; + HashSet/*!*/ gen; + HashSet/*!*/ kill; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(gen)); @@ -482,17 +482,17 @@ namespace Microsoft.Boogie { bool isZero; - public static GenKillWeight/*!*/ oneWeight = new GenKillWeight(new Set(), new Set()); + 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 Set(); - this.kill = new Set(); + this.gen = new HashSet(); + this.kill = new HashSet(); } - public GenKillWeight(Set gen, Set kill) { + public GenKillWeight(HashSet gen, HashSet kill) { Contract.Requires(cce.NonNullElements(gen)); Contract.Requires(cce.NonNullElements(kill)); Contract.Assert(gen != null); @@ -519,7 +519,14 @@ namespace Microsoft.Boogie { if (w1.isZero || w2.isZero) return zero(); - return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill)); + 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) { @@ -531,16 +538,29 @@ namespace Microsoft.Boogie { if (w2.isZero) return w1; - return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill)); + 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); - Set gen = w.gen.FindAll(isGlobal); - Contract.Assert(cce.NonNullElements(gen)); - Set kill = w.kill.FindAll(isGlobal); - Contract.Assert(cce.NonNullElements(kill)); + 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); } @@ -567,16 +587,18 @@ namespace Microsoft.Boogie { return string.Format("({0},{1})", gen.ToString(), kill.ToString()); } - public Set/*!*/ getLiveVars() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + public HashSet/*!*/ getLiveVars() { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); return gen; } - public Set/*!*/ getLiveVars(Set/*!*/ lv) { + public HashSet/*!*/ getLiveVars(HashSet/*!*/ lv) { Contract.Requires(cce.NonNullElements(lv)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - Set/*!*/ temp = cce.NonNull(lv.Difference(kill)); - return cce.NonNull(temp.Union(gen)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + HashSet temp = new HashSet(lv); + temp.ExceptWith(kill); + temp.UnionWith(gen); + return temp; } } @@ -585,18 +607,18 @@ namespace Microsoft.Boogie { public Graph/*!*/ graph; // Map from procedure to the list of blocks that call that procedure public Dictionary/*!*/>/*!*/ procsCalled; - public Set/*!*/ nodes; - public Dictionary/*!*/>/*!*/ succEdges; - public Dictionary/*!*/>/*!*/ predEdges; + public HashSet/*!*/ nodes; + public Dictionary/*!*/>/*!*/ succEdges; + public Dictionary/*!*/>/*!*/ predEdges; private Dictionary/*!*/ priority; - public Set/*!*/ srcNodes; - public Set/*!*/ exitNodes; + public HashSet/*!*/ srcNodes; + public HashSet/*!*/ exitNodes; public Dictionary/*!*/ weightBefore; public Dictionary/*!*/ weightAfter; - public Dictionary/*!*/>/*!*/ liveVarsAfter; - public Dictionary/*!*/>/*!*/ liveVarsBefore; + public Dictionary/*!*/>/*!*/ liveVarsAfter; + public Dictionary/*!*/>/*!*/ liveVarsBefore; public GenKillWeight/*!*/ summary; public Implementation/*!*/ impl; @@ -624,19 +646,19 @@ namespace Microsoft.Boogie { Contract.Requires(impl != null); this.graph = new Graph(); this.procsCalled = new Dictionary/*!*/>(); - this.nodes = new Set(); - this.succEdges = new Dictionary/*!*/>(); - this.predEdges = new Dictionary/*!*/>(); + this.nodes = new HashSet(); + this.succEdges = new Dictionary/*!*/>(); + this.predEdges = new Dictionary/*!*/>(); this.priority = new Dictionary(); - this.srcNodes = new Set(); - this.exitNodes = new Set(); + this.srcNodes = new HashSet(); + this.exitNodes = new HashSet(); this.weightBefore = new Dictionary(); this.weightAfter = new Dictionary(); - this.liveVarsAfter = new Dictionary/*!*/>(); - this.liveVarsBefore = new Dictionary/*!*/>(); + this.liveVarsAfter = new Dictionary/*!*/>(); + this.liveVarsBefore = new Dictionary/*!*/>(); summary = GenKillWeight.zero(); this.impl = impl; @@ -725,11 +747,11 @@ namespace Microsoft.Boogie { private void registerNode(Block b) { Contract.Requires(b != null); if (!succEdges.ContainsKey(b)) { - succEdges.Add(b, new Set()); + succEdges.Add(b, new HashSet()); } if (!predEdges.ContainsKey(b)) { - predEdges.Add(b, new Set()); + predEdges.Add(b, new HashSet()); } nodes.Add(b); @@ -762,8 +784,8 @@ namespace Microsoft.Boogie { Implementation/*!*/ mainImpl; - static Dictionary/*!*/>/*!*/ varsLiveAtExit = new Dictionary/*!*/>(); - static Dictionary/*!*/>/*!*/ varsLiveAtEntry = new Dictionary/*!*/>(); + static Dictionary/*!*/>/*!*/ varsLiveAtExit = new Dictionary/*!*/>(); + static Dictionary/*!*/>/*!*/ varsLiveAtEntry = new Dictionary/*!*/>(); static Dictionary/*!*/ varsLiveSummary = new Dictionary(); [ContractInvariantMethod] void ObjectInvariant() { @@ -875,15 +897,15 @@ namespace Microsoft.Boogie { } - public static Set/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) { + public static HashSet/*!*/ GetVarsLiveAtExit(Implementation impl, Program prog) { Contract.Requires(prog != null); Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); if (varsLiveAtExit.ContainsKey(impl.Name)) { return varsLiveAtExit[impl.Name]; } // Return default: all globals and out params - Set/*!*/ lv = new Set(); + HashSet/*!*/ lv = new HashSet(); foreach (Variable/*!*/ v in prog.GlobalVariables()) { Contract.Assert(v != null); lv.Add(v); @@ -895,15 +917,15 @@ namespace Microsoft.Boogie { return lv; } - public static Set/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) { + public static HashSet/*!*/ GetVarsLiveAtEntry(Implementation impl, Program prog) { Contract.Requires(prog != null); Contract.Requires(impl != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); if (varsLiveAtEntry.ContainsKey(impl.Name)) { return varsLiveAtEntry[impl.Name]; } // Return default: all globals and in params - Set/*!*/ lv = new Set(); + HashSet/*!*/ lv = new HashSet(); foreach (Variable/*!*/ v in prog.GlobalVariables()) { Contract.Assert(v != null); lv.Add(v); @@ -920,10 +942,10 @@ namespace Microsoft.Boogie { return varsLiveSummary.ContainsKey(name); } - public static Set/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, Set/*!*/ lvAfter) { + public static HashSet/*!*/ PropagateLiveVarsAcrossCall(CallCmd cmd, HashSet/*!*/ lvAfter) { Contract.Requires(cmd != null); Contract.Requires(cce.NonNullElements(lvAfter)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); Procedure/*!*/ proc = cce.NonNull(cmd.Proc); if (varsLiveSummary.ContainsKey(proc.Name)) { GenKillWeight/*!*/ w1 = getWeightBeforeCall(cmd); @@ -936,8 +958,8 @@ namespace Microsoft.Boogie { Contract.Assert(w != null); return w.getLiveVars(lvAfter); } - Set/*!*/ ret = new Set(); - ret.AddRange(lvAfter); + HashSet/*!*/ ret = new HashSet(); + ret.UnionWith(lvAfter); LiveVariableAnalysis.Propagate(cmd, ret); return ret; } @@ -1014,7 +1036,7 @@ namespace Microsoft.Boogie { class WorkList { SortedList/*!*/ priorities; - Set/*!*/ labels; + HashSet/*!*/ labels; Dictionary/*!*/>/*!*/ workList; [ContractInvariantMethod] @@ -1027,7 +1049,7 @@ namespace Microsoft.Boogie { public WorkList() { - labels = new Set(); + labels = new HashSet(); priorities = new SortedList(); workList = new Dictionary/*!*/>(); } @@ -1127,8 +1149,8 @@ namespace Microsoft.Boogie { Contract.Assert(cfg != null); foreach (Block/*!*/ b in cfg.nodes) { Contract.Assert(b != null); - cfg.liveVarsAfter.Add(b, new Set()); - cfg.liveVarsBefore.Add(b, new Set()); + cfg.liveVarsAfter.Add(b, new HashSet()); + cfg.liveVarsBefore.Add(b, new HashSet()); } } @@ -1150,16 +1172,16 @@ namespace Microsoft.Boogie { // Set live variable info foreach (ICFG/*!*/ cfg in procICFG.Values) { Contract.Assert(cfg != null); - Set/*!*/ lv = new Set(); + HashSet/*!*/ lv = new HashSet(); foreach (Block/*!*/ eb in cfg.exitNodes) { Contract.Assert(eb != null); - lv.AddRange(cfg.liveVarsAfter[eb]); + lv.UnionWith(cfg.liveVarsAfter[eb]); } varsLiveAtExit.Add(cfg.impl.Name, lv); - lv = new Set(); + lv = new HashSet(); foreach (Block/*!*/ eb in cfg.srcNodes) { Contract.Assert(eb != null); - lv.AddRange(cfg.liveVarsBefore[eb]); + lv.UnionWith(cfg.liveVarsBefore[eb]); } varsLiveAtEntry.Add(cfg.impl.Name, lv); varsLiveSummary.Add(cfg.impl.Name, cfg.summary); @@ -1186,11 +1208,11 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; Contract.Assert(cfg != null); Block/*!*/ block = wi.block; Contract.Assert(block != null); - Set/*!*/ lv = cfg.liveVarsAfter[block]; + HashSet/*!*/ lv = cfg.liveVarsAfter[block]; Contract.Assert(cce.NonNullElements(lv)); // Propagate backwards in the block - Set/*!*/ prop = new Set(); - prop.AddRange(lv); + HashSet/*!*/ prop = new HashSet(); + prop.UnionWith(lv); for (int i = block.Cmds.Length - 1; i >= 0; i--) { Cmd/*!*/ cmd = block.Cmds[i]; Contract.Assert(cmd != null); @@ -1202,7 +1224,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; Contract.Assert(callee != null); // Inter propagation // Remove local variables; add return variables - Set/*!*/ elv = new Set(); + HashSet/*!*/ elv = new HashSet(); foreach (Variable/*!*/ v in prop) { Contract.Assert(v != null); if (v is GlobalVariable) @@ -1215,7 +1237,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; foreach (Block/*!*/ eb in callee.exitNodes) { Contract.Assert(eb != null); - callee.liveVarsAfter[eb].AddRange(elv); + callee.liveVarsAfter[eb].UnionWith(elv); // TODO: check if modified before inserting AddToWorkListReverse(new WorkItem(callee, eb)); } @@ -1231,13 +1253,14 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; } } - cfg.liveVarsBefore[block].AddRange(prop); + cfg.liveVarsBefore[block].UnionWith(prop); foreach (Block/*!*/ b in cfg.predEdges[block]) { Contract.Assert(b != null); - Set/*!*/ prev = cfg.liveVarsAfter[b]; + HashSet/*!*/ prev = cfg.liveVarsAfter[b]; Contract.Assert(cce.NonNullElements(prev)); - Set/*!*/ curr = cce.NonNull(prev.Union(cfg.liveVarsBefore[block])); + HashSet/*!*/ curr = new HashSet(prev); + curr.UnionWith(cfg.liveVarsBefore[block]); Contract.Assert(cce.NonNullElements(curr)); if (curr.Count != prev.Count) { cfg.liveVarsAfter[b] = curr; @@ -1323,8 +1346,8 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; if (weightCache.ContainsKey(cmd)) return weightCache[cmd]; - Set/*!*/ gen = new Set(); - Set/*!*/ kill = new Set(); + HashSet/*!*/ gen = new HashSet(); + HashSet/*!*/ kill = new HashSet(); GenKillWeight/*!*/ ret; if (cmd is AssignCmd) { @@ -1349,7 +1372,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; Contract.Assert(expr != null); VariableCollector/*!*/ collector = new VariableCollector(); collector.Visit(expr); - gen.AddRange(collector.usedVars); + 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 @@ -1357,7 +1380,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; foreach (Expr e in malhs.Indexes) { VariableCollector/*!*/ c = new VariableCollector(); c.Visit(e); - gen.AddRange(c.usedVars); + gen.UnionWith(c.usedVars); } } index++; @@ -1396,7 +1419,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; } else { VariableCollector/*!*/ collector = new VariableCollector(); collector.Visit(predicateCmd.Expr); - gen.AddRange(collector.usedVars); + gen.UnionWith(collector.usedVars); } ret = new GenKillWeight(gen, kill); } else if (cmd is CommentCmd) { @@ -1444,8 +1467,8 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; if (weightCacheAfterCall.ContainsKey(cmd)) return weightCacheAfterCall[cmd]; - Set/*!*/ gen = new Set(); - Set/*!*/ kill = new Set(); + HashSet/*!*/ gen = new HashSet(); + HashSet/*!*/ kill = new HashSet(); Contract.Assert(cmd is CallCmd); CallCmd/*!*/ ccmd = cce.NonNull((CallCmd)cmd); @@ -1482,15 +1505,15 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; if (weightCacheBeforeCall.ContainsKey(cmd)) return weightCacheBeforeCall[cmd]; - Set/*!*/ gen = new Set(); - Set/*!*/ kill = new Set(); + 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.AddRange(collector.usedVars); + gen.UnionWith(collector.usedVars); } Contract.Assert(ccmd.Proc != null); diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs index cfadd2b2..6976e281 100644 --- a/Source/Core/LoopUnroll.cs +++ b/Source/Core/LoopUnroll.cs @@ -5,7 +5,6 @@ //----------------------------------------------------------------------------- using System.Diagnostics.Contracts; using System.Collections.Generic; -using Cci = System.Compiler; using Bpl = Microsoft.Boogie; namespace Microsoft.Boogie { @@ -16,7 +15,7 @@ namespace Microsoft.Boogie { Contract.Requires(0 <= unrollMaxDepth); Contract.Ensures(cce.NonNullElements(Contract.Result>())); Dictionary gd = new Dictionary(); - Cci.HashSet/*Block*//*!*/ beingVisited = new Cci.HashSet/*Block*/(); + HashSet beingVisited = new HashSet(); GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited); // Compute SCCs @@ -106,7 +105,7 @@ namespace Microsoft.Boogie { return cmds; } - public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary/*!*/ gd, Cci.HashSet/*Block*/ beingVisited) { + public static GraphNode ComputeGraphInfo(GraphNode from, Block b, Dictionary/*!*/ gd, HashSet beingVisited) { Contract.Requires(beingVisited != null); Contract.Requires(b != null); Contract.Requires(cce.NonNullElements(gd)); diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 93018097..d4b353ef 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -7,7 +7,6 @@ namespace Microsoft.Boogie { using System.Collections; using System.Collections.Generic; using System; - using Microsoft.SpecSharp.Collections; using System.Diagnostics.Contracts; [ContractClass(typeof(IErrorSinkContracts))] diff --git a/Source/Core/Xml.cs b/Source/Core/Xml.cs index 8fca82f8..e0b909fe 100644 --- a/Source/Core/Xml.cs +++ b/Source/Core/Xml.cs @@ -8,7 +8,6 @@ using System.IO; using System.Xml; using System.Collections.Generic; using System.Diagnostics.Contracts; -using Cci = System.Compiler; namespace Microsoft.Boogie { public class XmlSink { @@ -143,6 +142,7 @@ namespace Microsoft.Boogie { cce.EndExpose(); } +#if CCI public void WriteError(string message, Cci.Node offendingNode, BlockSeq trace) { Contract.Requires(offendingNode != null); Contract.Requires(message != null); @@ -177,6 +177,7 @@ namespace Microsoft.Boogie { } cce.EndExpose(); } +#endif [Inside] private void WriteTokenAttributes(IToken tok) { @@ -189,6 +190,7 @@ namespace Microsoft.Boogie { } } +#if CCI [Inside] private void WriteTokenAttributes(Cci.Node node) { Contract.Requires(node != null); @@ -201,6 +203,7 @@ namespace Microsoft.Boogie { wr.WriteAttributeString("column", node.SourceContext.StartColumn.ToString()); } } +#endif public void WriteStartInference(string inferenceName) { Contract.Requires(inferenceName != null); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index bd87186b..fcf556f0 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -20,7 +20,6 @@ namespace Microsoft.Boogie using Microsoft.Boogie.AbstractInterpretation; using System.Diagnostics; using VC; - using Cci = System.Compiler; using AI = Microsoft.AbstractInterpretationFramework; /* @@ -69,17 +68,6 @@ namespace Microsoft.Boogie Console.WriteLine("--------------------"); } - SelectPlatform(CommandLineOptions.Clo); - - // Make sure the Spec# runtime is initialized. - // This happens when the static constructor for the Runtime type is executed. - // Otherwise, if a reference happens to get chased to it, it is loaded twice - // and then the types in it do not get unique representations. - if (System.Type.GetType("Mono.Runtime") == null) { // MONO - Cci.AssemblyNode a = Microsoft.SpecSharp.Runtime.RuntimeAssembly; - Contract.Assert( a != null); - } - foreach (string file in CommandLineOptions.Clo.Files) {Contract.Assert(file != null); string extension = Path.GetExtension(file); @@ -146,78 +134,11 @@ namespace Microsoft.Boogie Console.ForegroundColor = col; } - public static void SelectPlatform(CommandLineOptions options) - { - Contract.Requires(options != null); - if (options.TargetPlatformLocation != null) { - // Make sure static constructor runs before we start setting locations, etc. - System.Compiler.SystemTypes.Clear(); - - switch (options.TargetPlatform){ - case CommandLineOptions.PlatformType.v1: Microsoft.SpecSharp.TargetPlatform.SetToV1(options.TargetPlatformLocation); break; - case CommandLineOptions.PlatformType.v11: Microsoft.SpecSharp.TargetPlatform.SetToV1_1(options.TargetPlatformLocation); break; - case CommandLineOptions.PlatformType.v2: Microsoft.SpecSharp.TargetPlatform.SetToV2(options.TargetPlatformLocation); break; - case CommandLineOptions.PlatformType.cli1: Microsoft.SpecSharp.TargetPlatform.SetToPostV1_1(options.TargetPlatformLocation); break; - } - - if (options.StandardLibraryLocation != null && options.StandardLibraryLocation.Length > 0){ - System.Compiler.SystemAssemblyLocation.Location = options.StandardLibraryLocation; - } - System.Compiler.SystemCompilerRuntimeAssemblyLocation.Location = options.TargetPlatformLocation + @"\System.Compiler.Runtime.dll"; - - System.Compiler.SystemTypes.Initialize(true, true); - } - } - - static string GetErrorLine(Cci.ErrorNode node) - { Contract.Requires( node.SourceContext.Document == null || node.SourceContext.Document.Name != null); - - - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - - string message = node.GetMessage(System.Threading.Thread.CurrentThread.CurrentUICulture); - string kind; - if (message.Contains("(trace position)")) { - kind = "Related information"; - } else { - kind = "Error"; - } - if (node.SourceContext.Document != null) { - return string.Format("{0}({1},{2}): {3}: {4}", Path.GetFileName(cce.NonNull(node.SourceContext.Document.Name)), node.SourceContext.StartLine, node.SourceContext.StartColumn, kind, message); - } else { - return string.Format("{0}: {1}", kind, message); - } - } - enum FileType { Unknown, Cil, Bpl, Dafny }; - class ErrorReporter - { - public Cci.ErrorNodeList errors = new Cci.ErrorNodeList(); - [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(errors!=null); -} - - public int errorsReported; - - public void ReportErrors() - { - //sort the portion of the array that will be reported to make output more deterministic - errors.Sort(errorsReported,errors.Count-errorsReported); - for(;errorsReported < errors.Count; errorsReported++) { - Cci.ErrorNode error = errors[errorsReported]; - if (error != null) - ErrorWriteLine(GetErrorLine(error)); - } - } - } - static void ProcessFiles (List/*!*/ fileNames) { - Contract.Requires(cce.NonNullElements(fileNames)); + Contract.Requires(cce.NonNullElements(fileNames)); using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) { Dafny.Program dafnyProgram; string programName = fileNames.Count == 1 ? fileNames[0] : "the program"; @@ -242,7 +163,7 @@ void ObjectInvariant() } int errorCount, verified, inconclusives, timeOuts, outOfMemories; - PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, null/*new ErrorReporter()*/, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories); + PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories); switch (oc) { case PipelineOutcome.VerificationCompleted: if (CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) { @@ -420,7 +341,6 @@ void ObjectInvariant() /// their error code. /// static PipelineOutcome BoogiePipelineWithRerun (Program/*!*/ program, string/*!*/ bplFileName, - ErrorReporter errorReporter, out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {Contract.Requires(program != null); Contract.Requires(cce.NonNullElements(bplFileName)); @@ -451,7 +371,7 @@ void ObjectInvariant() return oc; case PipelineOutcome.ResolvedAndTypeChecked: - return InferAndVerify(program, errorReporter, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories); + return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories); default: Contract.Assert(false);throw new cce.UnreachableException(); // unexpected outcome @@ -511,7 +431,6 @@ void ObjectInvariant() /// parameters contain meaningful values /// static PipelineOutcome InferAndVerify (Program program, - ErrorReporter errorReporter, out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {Contract.Requires(program != null); Contract.Ensures( 0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts)); @@ -569,169 +488,188 @@ void ObjectInvariant() foreach ( Declaration decl in program.TopLevelDeclarations ) {Contract.Assert(decl != null); Implementation impl = decl as Implementation; - if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) { - List/*?*/ errors; - - DateTime start = new DateTime(); // to please compiler's definite assignment rules - if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) { - start = DateTime.Now; - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine(); - Console.WriteLine("Verifying {0} ...", impl.Name); - } - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start); - } - } + if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) + { + List/*?*/ errors; - ConditionGeneration.Outcome outcome; - try - { - outcome = vcgen.VerifyImplementation(impl, program, out errors); - } - catch (VCGenException e) - { - ReportBplError(impl, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true); - errors = null; - outcome = VCGen.Outcome.Inconclusive; - } - catch (UnexpectedProverOutputException upo) - { - AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message); - errors = null; - outcome = VCGen.Outcome.Inconclusive; - } + DateTime start = new DateTime(); // to please compiler's definite assignment rules + if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) + { + start = DateTime.Now; + if (CommandLineOptions.Clo.Trace) + { + Console.WriteLine(); + Console.WriteLine("Verifying {0} ...", impl.Name); + } + if (CommandLineOptions.Clo.XmlSink != null) + { + CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start); + } + } - string timeIndication = ""; - DateTime end = DateTime.Now; - TimeSpan elapsed = end - start; - if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) { - if (CommandLineOptions.Clo.Trace) { - timeIndication = string.Format(" [{0} s] ", elapsed.TotalSeconds); + ConditionGeneration.Outcome outcome; + try + { + outcome = vcgen.VerifyImplementation(impl, program, out errors); + } + catch (VCGenException e) + { + ReportBplError(impl, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true); + errors = null; + outcome = VCGen.Outcome.Inconclusive; + } + catch (UnexpectedProverOutputException upo) + { + AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message); + errors = null; + outcome = VCGen.Outcome.Inconclusive; } - } - - switch (outcome) { - default: - Contract.Assert(false);throw new cce.UnreachableException(); // unexpected outcome - case VCGen.Outcome.Correct: - Inform(String.Format("{0}verified", timeIndication)); - verified++; - break; - case VCGen.Outcome.TimedOut: - timeOuts++; - Inform(String.Format("{0}timed out", timeIndication)); - break; - case VCGen.Outcome.OutOfMemory: - outOfMemories++; - Inform(String.Format("{0}out of memory", timeIndication)); - break; - case VCGen.Outcome.Inconclusive: - inconclusives++; - Inform(String.Format("{0}inconclusive", timeIndication)); - break; - case VCGen.Outcome.Errors: - Contract.Assert( errors != null); // guaranteed by postcondition of VerifyImplementation - if (errorReporter != null) - { -// assert translatedProgram != null; -// ErrorReporting h = new ErrorReporting(); -// h.errorReportingWithTrace(translatedProgram, errors, impl); - - errorReporter.ReportErrors(); - } - else - { - // BP1xxx: Parsing errors - // BP2xxx: Name resolution errors - // BP3xxx: Typechecking errors - // BP4xxx: Abstract interpretation errors (Is there such a thing?) - // BP5xxx: Verification errors - - errors.Sort(new CounterexampleComparer()); - foreach (Counterexample error in errors) + string timeIndication = ""; + DateTime end = DateTime.Now; + TimeSpan elapsed = end - start; + if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) + { + if (CommandLineOptions.Clo.Trace) { - if (error is CallCounterexample) - { - CallCounterexample err = (CallCounterexample) error; - ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true); - ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false); - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace); - } - } - else if (error is ReturnCounterexample) - { - ReturnCounterexample err = (ReturnCounterexample) error; - ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true); - ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false); - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace); - } - } - else // error is AssertCounterexample - { - AssertCounterexample err = (AssertCounterexample) error; - if (err.FailingAssert is LoopInitAssertCmd) { - ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true); - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace); - } - } - else if (err.FailingAssert is LoopInvMaintainedAssertCmd) { - // this assertion is a loop invariant which is not maintained - ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true); - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace); - } - } else { - string msg = err.FailingAssert.ErrorData as string; - if (msg == null) { - msg = "Error BP5001: This assertion might not hold."; - } - ReportBplError(err.FailingAssert, msg, true); - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace); - } - } - } - if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) { - foreach (string info in error.relatedInformation) {Contract.Assert(info != null); - Console.WriteLine(" " + info); - } - } - if (CommandLineOptions.Clo.ErrorTrace > 0) { - Console.WriteLine("Execution trace:"); - foreach (Block b in error.Trace) { - Contract.Assert(b != null); - if (b.tok == null) { - Console.WriteLine(" "); - } else { - // for ErrorTrace == 1 restrict the output; - // do not print tokens with -17:-4 as their location because they have been - // introduced in the translation and do not give any useful feedback to the user - if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) { - Console.WriteLine(" {0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label); + timeIndication = string.Format(" [{0} s] ", elapsed.TotalSeconds); + } + } + + switch (outcome) + { + default: + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome + case VCGen.Outcome.Correct: + Inform(String.Format("{0}verified", timeIndication)); + verified++; + break; + case VCGen.Outcome.TimedOut: + timeOuts++; + Inform(String.Format("{0}timed out", timeIndication)); + break; + case VCGen.Outcome.OutOfMemory: + outOfMemories++; + Inform(String.Format("{0}out of memory", timeIndication)); + break; + case VCGen.Outcome.Inconclusive: + inconclusives++; + Inform(String.Format("{0}inconclusive", timeIndication)); + break; + case VCGen.Outcome.Errors: + Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation + // BP1xxx: Parsing errors + // BP2xxx: Name resolution errors + // BP3xxx: Typechecking errors + // BP4xxx: Abstract interpretation errors (Is there such a thing?) + // BP5xxx: Verification errors + + errors.Sort(new CounterexampleComparer()); + foreach (Counterexample error in errors) + { + if (error is CallCounterexample) + { + CallCounterexample err = (CallCounterexample)error; + ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true); + ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false); + if (CommandLineOptions.Clo.XmlSink != null) + { + CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace); + } + } + else if (error is ReturnCounterexample) + { + ReturnCounterexample err = (ReturnCounterexample)error; + ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true); + ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false); + if (CommandLineOptions.Clo.XmlSink != null) + { + CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace); + } + } + else // error is AssertCounterexample + { + AssertCounterexample err = (AssertCounterexample)error; + if (err.FailingAssert is LoopInitAssertCmd) + { + ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true); + if (CommandLineOptions.Clo.XmlSink != null) + { + CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace); + } + } + else if (err.FailingAssert is LoopInvMaintainedAssertCmd) + { + // this assertion is a loop invariant which is not maintained + ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true); + if (CommandLineOptions.Clo.XmlSink != null) + { + CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace); + } + } + else + { + string msg = err.FailingAssert.ErrorData as string; + if (msg == null) + { + msg = "Error BP5001: This assertion might not hold."; + } + ReportBplError(err.FailingAssert, msg, true); + if (CommandLineOptions.Clo.XmlSink != null) + { + CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace); + } + } + } + if (CommandLineOptions.Clo.EnhancedErrorMessages == 1) + { + foreach (string info in error.relatedInformation) + { + Contract.Assert(info != null); + Console.WriteLine(" " + info); + } + } + if (CommandLineOptions.Clo.ErrorTrace > 0) + { + Console.WriteLine("Execution trace:"); + foreach (Block b in error.Trace) + { + Contract.Assert(b != null); + if (b.tok == null) + { + Console.WriteLine(" "); + } + else + { + // for ErrorTrace == 1 restrict the output; + // do not print tokens with -17:-4 as their location because they have been + // introduced in the translation and do not give any useful feedback to the user + if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) + { + Console.WriteLine(" {0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label); + } + } + } } - } + if (CommandLineOptions.Clo.ModelViewFile != null) + { + error.PrintModel(); + } + errorCount++; } - } - if (CommandLineOptions.Clo.ModelViewFile != null) { - error.PrintModel(); - } - errorCount++; - } - } - Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s")); - break; - } - if (CommandLineOptions.Clo.XmlSink != null) { - CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed); - } - if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) { - Console.Out.Flush(); - } + + Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s")); + break; + } + + if (CommandLineOptions.Clo.XmlSink != null) + { + CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed); + } + if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) + { + Console.Out.Flush(); + } } } vcgen.Close(); diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index afd8f9b3..1ec5abb0 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -97,19 +97,7 @@ False ..\Core\bin\Debug\Core.dll - - False - ..\..\Binaries\Microsoft.SpecSharp.dll - - - False - ..\..\Binaries\System.Compiler.dll - - - False - ..\..\Binaries\System.Compiler.Runtime.dll - diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 6bfd5c34..bc256cd5 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -5,8 +5,6 @@ //----------------------------------------------------------------------------- using System; using System.Collections.Generic; -using Microsoft.SpecSharp.Collections; -using Microsoft.Contracts; using System.Text; // for StringBuilder using System.Diagnostics.Contracts; namespace Graphing { @@ -279,23 +277,24 @@ namespace Graphing { return; } } + public class Graph { - private Set> es; - private Set ns; + private HashSet> es; + private HashSet ns; private Node source; private bool reducible; - private Set headers; - private Map> backEdgeNodes; - private Map, Set> naturalLoops; + private HashSet headers; + private Dictionary> backEdgeNodes; + private Dictionary, HashSet> naturalLoops; private DomRelation dominatorMap = null; - private Dictionary> predCache = new Dictionary>(); - private Dictionary> succCache = new Dictionary>(); + private Dictionary> predCache = new Dictionary>(); + private Dictionary> succCache = new Dictionary>(); private bool predComputed; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(es == null || Contract.ForAll(es, p => p.First != null && p.Second != null)); - Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Second != null && p.First != null)); + Contract.Invariant(es == null || Contract.ForAll(es, p => p.Item1 != null && p.Item2 != null)); + Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null)); } @@ -318,30 +317,30 @@ namespace Graphing { } } - public Graph(Set> edges) { + public Graph(HashSet> edges) { - Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.First != null && p.Second != null)); + Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.Item1 != null && p.Item2 != null)); es = edges; // original A# //ns = Set{ x : in es } + Set{ y : in es }; // closest Spec# - //ns = new Set{ Pair p in edges; p.First } + new Set{ Pair p in edges; p.Second }; + //ns = new Set{ Tuple p in edges; p.Item1 } + new Set{ Tuple p in edges; p.Item2 }; // - Set temp = new Set(); - foreach (Pair p in edges) { - Contract.Assert(p.First != null); - temp.Add(p.First); - Contract.Assert(p.Second != null); - temp.Add(p.Second); + HashSet temp = new HashSet(); + foreach (Tuple p in edges) { + Contract.Assert(p.Item1 != null); + temp.Add(p.Item1); + Contract.Assert(p.Item2 != null); + temp.Add(p.Item2); } ns = temp; } public Graph() { - es = new Set>(); - ns = new Set(); + es = new HashSet>(); + ns = new HashSet(); } // BUGBUG: Set.ToString() should return a non-null string @@ -363,22 +362,22 @@ namespace Graphing { Contract.Requires(dest != null); //es += Set{}; //ns += Set{source, dest}; - es.Add(new Pair(source, dest)); + es.Add(new Tuple(source, dest)); ns.Add(source); ns.Add(dest); predComputed = false; } - public Set Nodes { + public HashSet Nodes { get { return ns; } } - public IEnumerable> Edges { + public IEnumerable> Edges { get { - Contract.Ensures(cce.NonNullElements(Contract.Result>>()) - && Contract.ForAll(Contract.Result>>(), n => - n.First != null && n.Second != null)); + Contract.Ensures(cce.NonNullElements(Contract.Result>>()) + && Contract.ForAll(Contract.Result>>(), n => + n.Item1 != null && n.Item2 != null)); return es; } } @@ -388,33 +387,33 @@ namespace Graphing { Contract.Requires(y != null); // original A# // return in es; - return es.Contains(new Pair(x, y)); + return es.Contains(new Tuple(x, y)); } private void ComputePredSuccCaches() { if (predComputed) return; predComputed = true; - predCache = new Dictionary>(); - succCache = new Dictionary>(); + predCache = new Dictionary>(); + succCache = new Dictionary>(); foreach (Node n in Nodes) { - predCache[n] = new Set(); - succCache[n] = new Set(); + predCache[n] = new HashSet(); + succCache[n] = new HashSet(); } - foreach (Pair p in Edges) { - Contract.Assert(p.First != null); - Contract.Assert(p.Second != null); - Set tmp; + foreach (Tuple p in Edges) { + Contract.Assert(p.Item1 != null); + Contract.Assert(p.Item2 != null); + HashSet tmp; - tmp = predCache[p.Second]; - tmp.Add(p.First); - predCache[p.Second] = tmp; + tmp = predCache[p.Item2]; + tmp.Add(p.Item1); + predCache[p.Item2] = tmp; - tmp = succCache[p.First]; - tmp.Add(p.Second); - succCache[p.First] = tmp; + tmp = succCache[p.Item1]; + tmp.Add(p.Item2); + succCache[p.Item1] = tmp; } } @@ -482,10 +481,10 @@ namespace Graphing { nodeToNumber[node] = counter; counter++; } - foreach (Pair e in this.Edges) { - Contract.Assert(e.First != null); - Contract.Assert(e.Second != null); - Node/*!*/ target = e.Second; + foreach (Tuple e in this.Edges) { + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + Node/*!*/ target = e.Item2; incomingEdges[nodeToNumber[target]]++; } List sorted = new List(); @@ -518,14 +517,15 @@ namespace Graphing { return; } private IEnumerable OldTopologicalSort() { - Pair> result = this.TopSort(); - return result.First ? result.Second : (IEnumerable)new Seq(); + Tuple> result = this.TopSort(); + return result.Item1 ? result.Item2 : (IEnumerable)new List(); } // From AsmL distribution example - private Pair> TopSort() { - Seq S = new Seq(); - Set V = this.Nodes; - Set X = new Set(); + private Tuple> TopSort() + { + List S = new List(); + HashSet V = this.Nodes; + HashSet X = new HashSet(); foreach (Node/*!*/ n in V) { Contract.Assert(n != null); X.Add(n); @@ -556,11 +556,11 @@ namespace Graphing { } // Then we made it all the way through X without finding a source node if (!change) { - return new Pair>(false, new Seq()); + return new Tuple>(false, new List()); } } } - return new Pair>(true, S); + return new Tuple>(true, S); } public static bool Acyclic(Graph g, Node source) { @@ -570,66 +570,29 @@ namespace Graphing { return acyclic; } - // - // [Dragon, pp. 670--671] - // returns map D s.t. d in D(n) iff d dom n - // - static private Map> OldComputeDominators(Graph g, Node/*!*/ source) { - Contract.Requires(source != null); - Contract.Assert(g.source != null); - Set N = g.Nodes; - Set nonSourceNodes = N - new Set(source); - Map> D = new Map>(); - D[source] = new Set(source); - foreach (Node/*!*/ n in nonSourceNodes) { - Contract.Assert(n != null); - D[n] = N; - } - bool change = true; - while (change) { - change = false; - foreach (Node/*!*/ n in nonSourceNodes) { - Contract.Assert(n != null); - - // original A# - //Set> allPreds = new Set>{ Node p in this.Predecessors(n) ; D[p] }; - - Set> allPreds = new Set>(); - foreach (Node/*!*/ p in g.Predecessors(n)) { - Contract.Assert(p != null); - allPreds.Add(D[p]); - } - Set temp = new Set(n) + Set.BigIntersect(allPreds); - if (temp != D[n]) { - change = true; - D[n] = temp; - } - } - } - return D; - } - // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.] - static Set NaturalLoop(Graph g, Pair backEdge) { - Contract.Requires(backEdge.First != null && backEdge.Second != null); - Node/*!*/ n = backEdge.First; - Node/*!*/ d = backEdge.Second; - Seq stack = new Seq(); - Set loop = new Set(d); - if (!n.Equals(d)) // then n is not in loop + static HashSet NaturalLoop(Graph g, Tuple backEdge) { + Contract.Requires(backEdge.Item1 != null && backEdge.Item2 != null); + Node/*!*/ n = backEdge.Item1; + Node/*!*/ d = backEdge.Item2; + Stack stack = new Stack(); + HashSet loop = new HashSet(); + loop.Add(d); + if (!n.Equals(d)) // then n is not in loop + { loop.Add(n); - stack = new Seq(n) + stack; // push n onto stack + stack.Push(n); // push n onto stack } while (stack.Count > 0) // not empty - { - Node m = stack.Head; - stack = stack.Tail; // pop stack + { + Node m = stack.Peek(); + stack.Pop(); // pop stack foreach (Node/*!*/ p in g.Predecessors(m)) { Contract.Assert(p != null); if (!(loop.Contains(p))) { loop.Add(p); - stack = new Seq(p) + stack; // push p onto stack + stack.Push(p); // push p onto stack } } } @@ -638,16 +601,17 @@ namespace Graphing { internal struct ReducibleResult { internal bool reducible; - internal Set headers; - internal Map> backEdgeNodes; - internal Map, Set> naturalLoops; + internal HashSet headers; + internal Dictionary> backEdgeNodes; + internal Dictionary, HashSet> naturalLoops; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.First != null && p.Second != null)); + Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.Item1 != null && p.Item2 != null)); } - internal ReducibleResult(bool b, Set headers, Map> backEdgeNodes, Map, Set> naturalLoops) { - Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.First != null && Key.Second != null)); + internal ReducibleResult(bool b, HashSet headers, Dictionary> backEdgeNodes, Dictionary, HashSet> naturalLoops) + { + Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.Item1 != null && Key.Item2 != null)); this.reducible = b; this.headers = headers; this.backEdgeNodes = backEdgeNodes; @@ -670,15 +634,15 @@ namespace Graphing { Contract.Requires(DomRelation != null); //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible"); - IEnumerable> edges = g.Edges; - Contract.Assert(Contract.ForAll(edges, n => n.First != null && n.Second != null)); - Set> backEdges = new Set>(); - Set> nonBackEdges = new Set>(); - foreach (Pair e in edges) { - Contract.Assert(e.First != null); - Contract.Assert(e.Second != null); - Node x = e.First; - Node y = e.Second; // so there is an edge from x to y + IEnumerable> edges = g.Edges; + Contract.Assert(Contract.ForAll(edges, n => n.Item1 != null && n.Item2 != null)); + HashSet> backEdges = new HashSet>(); + HashSet> nonBackEdges = new HashSet>(); + foreach (Tuple e in edges) { + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + Node x = e.Item1; + Node y = e.Item2; // so there is an edge from x to y if (DomRelation.DominatedBy(x, y)) { // y dom x: which means y dominates x backEdges.Add(e); } else { @@ -687,40 +651,40 @@ namespace Graphing { } if (!Acyclic(new Graph(nonBackEdges), source)) { return new ReducibleResult(false, - new Set(), - new Map>(), - new Map, Set>()); + new HashSet(), + new Dictionary>(), + new Dictionary, HashSet>()); } else { // original A#: //Set headers = Set{ d : in backEdges }; - Set headers = new Set(); - foreach (Pair e in backEdges) { + HashSet headers = new HashSet(); + foreach (Tuple e in backEdges) { - Contract.Assert(e.First != null); - Contract.Assert(e.Second != null); - headers.Add(e.Second); + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + headers.Add(e.Item2); } // original A#: //Map> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set{ b : in backEdges, x == h } }; - Map> backEdgeNodes = new Map>(); + Dictionary> backEdgeNodes = new Dictionary>(); foreach (Node/*!*/ h in headers) { Contract.Assert(h != null); - Set bs = new Set(); - foreach (Pair backedge in backEdges) { - Contract.Assert(backedge.First != null); - Contract.Assert(backedge.Second != null); - if (backedge.Second.Equals(h)) { - bs.Add(backedge.First); + HashSet bs = new HashSet(); + foreach (Tuple backedge in backEdges) { + Contract.Assert(backedge.Item1 != null); + Contract.Assert(backedge.Item2 != null); + if (backedge.Item2.Equals(h)) { + bs.Add(backedge.Item1); } } backEdgeNodes.Add(h, bs); } // original A#: - //Map,Set> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges }; - Map, Set> naturalLoops = new Map, Set>(); - foreach (Pair e in backEdges) { - Contract.Assert(e.First != null && e.Second != null); + //Map,Set> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges }; + Dictionary, HashSet> naturalLoops = new Dictionary, HashSet>(); + foreach (Tuple e in backEdges) { + Contract.Assert(e.Item1 != null && e.Item2 != null); naturalLoops.Add(e, NaturalLoop(g, e)); } @@ -743,13 +707,13 @@ namespace Graphing { Contract.Requires(h != null); // original A#: //return h in backEdgeNodes ? backEdgeNodes[h] : null; - return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable)new Seq()); + return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable)new List()); } public IEnumerable NaturalLoops(Node/*!*/ header, Node/*!*/ backEdgeNode) { Contract.Requires(header != null); Contract.Requires(backEdgeNode != null); - Pair e = new Pair(backEdgeNode, header); - return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable)new Seq(); + Tuple e = new Tuple(backEdgeNode, header); + return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable)new List(); } public void ComputeLoops() { @@ -772,7 +736,7 @@ namespace Graphing { if (b.Equals(c)) continue; if (DominatorMap.DominatedBy(b, c)) { - Debug.Assert(!DominatorMap.DominatedBy(c, b)); + System.Diagnostics.Debug.Assert(!DominatorMap.DominatedBy(c, b)); dag.AddEdge(b, c); } } @@ -782,12 +746,12 @@ namespace Graphing { } // end: class Graph public class GraphProgram { - static void TestGraph(T/*!*/ source, params Pair[] edges) { + static void TestGraph(T/*!*/ source, params Tuple[] edges) { Contract.Requires(source != null); - Contract.Requires(Contract.ForAll(edges, pair => pair.First != null && pair.Second != null)); - Set> es = new Set>(); - foreach (Pair e in edges) { - Contract.Assert(e.First != null && e.Second != null); + Contract.Requires(Contract.ForAll(edges, pair => pair.Item1 != null && pair.Item2 != null)); + HashSet> es = new HashSet>(); + foreach (Tuple e in edges) { + Contract.Assert(e.Item1 != null && e.Item2 != null); es.Add(e); } Graph g = new Graph(es); @@ -804,64 +768,64 @@ namespace Graphing { { Console.WriteLine("Spec# says hello!"); // This generates bad IL -- need to fix a bug in the compiler - //Graph g = new Graph(new Set>{ new Pair(1,2), new Pair(1,3), new Pair(2,3) }); + //Graph g = new Graph(new Set>{ new Tuple(1,2), new Tuple(1,3), new Tuple(2,3) }); Console.WriteLine(""); TestGraph('a', - new Pair('a', 'b'), - new Pair('a', 'c'), - new Pair('b', 'c') + new Tuple('a', 'b'), + new Tuple('a', 'c'), + new Tuple('b', 'c') ); Console.WriteLine(""); TestGraph('a', - new Pair('a', 'b'), - new Pair('a', 'c'), - new Pair('b', 'd'), - new Pair('c', 'e'), - new Pair('c', 'f'), - new Pair('d', 'e'), - new Pair('e', 'd'), - new Pair('e', 'f'), - new Pair('f', 'e') + new Tuple('a', 'b'), + new Tuple('a', 'c'), + new Tuple('b', 'd'), + new Tuple('c', 'e'), + new Tuple('c', 'f'), + new Tuple('d', 'e'), + new Tuple('e', 'd'), + new Tuple('e', 'f'), + new Tuple('f', 'e') ); Console.WriteLine(""); TestGraph('a', - new Pair('a', 'b'), - new Pair('a', 'c'), - new Pair('b', 'c'), - new Pair('c', 'b') + new Tuple('a', 'b'), + new Tuple('a', 'c'), + new Tuple('b', 'c'), + new Tuple('c', 'b') ); Console.WriteLine(""); TestGraph(1, - new Pair(1, 2), - new Pair(1, 3), - new Pair(2, 3) + new Tuple(1, 2), + new Tuple(1, 3), + new Tuple(2, 3) ); Console.WriteLine(""); TestGraph(1, - new Pair(1, 2), - new Pair(1, 3), - new Pair(2, 3), - new Pair(3, 2) + new Tuple(1, 2), + new Tuple(1, 3), + new Tuple(2, 3), + new Tuple(3, 2) ); Console.WriteLine(""); TestGraph(2, - new Pair(2, 3), - new Pair(2, 4), - new Pair(3, 2) + new Tuple(2, 3), + new Tuple(2, 4), + new Tuple(3, 2) ); Console.WriteLine(""); TestGraph('a', - new Pair('a', 'b'), - new Pair('a', 'c'), - new Pair('b', 'c'), - new Pair('b', 'b') + new Tuple('a', 'b'), + new Tuple('a', 'c'), + new Tuple('b', 'c'), + new Tuple('b', 'b') ); diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj index 868af223..5e7473ea 100644 --- a/Source/Graph/Graph.csproj +++ b/Source/Graph/Graph.csproj @@ -99,10 +99,6 @@ true - - False - ..\..\Binaries\Microsoft.SpecSharp.Runtime.dll - diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj index aac48bda..8a340538 100644 --- a/Source/Provers/SMTLib/SMTLib.csproj +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -100,10 +100,6 @@ - - False - ..\..\..\Binaries\System.Compiler.Runtime.dll - 3.5 diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj index 1b73435b..42c441bf 100644 --- a/Source/Provers/Simplify/Simplify.csproj +++ b/Source/Provers/Simplify/Simplify.csproj @@ -100,10 +100,6 @@ - - False - ..\..\..\Binaries\System.Compiler.Runtime.dll - diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj index 89faad74..33b8ba7b 100644 --- a/Source/Provers/Z3/Z3.csproj +++ b/Source/Provers/Z3/Z3.csproj @@ -100,10 +100,6 @@ - - False - ..\..\..\Binaries\System.Compiler.Runtime.dll - 3.5 diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index 7d080eb3..a67530cc 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -4,7 +4,6 @@ using System.Collections.Generic; using System.Threading; using System.IO; using System.Diagnostics; -using Microsoft.Contracts; using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie; using Microsoft.Boogie.Z3; diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 750e4a00..fd9944ee 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -4,7 +4,6 @@ using System.Collections.Generic; using System.Threading; using System.IO; using System.Diagnostics; -using Microsoft.Contracts; using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie; using Microsoft.Boogie.Z3; diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index cffcd9bf..ba75c772 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -4,7 +4,6 @@ using System.Collections.Generic; using System.Threading; using System.IO; using System.Diagnostics; -using Microsoft.Contracts; using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie; using Microsoft.Boogie.Z3; diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs index 28c71751..b8aa607f 100644 --- a/Source/Provers/Z3api/StubContext.cs +++ b/Source/Provers/Z3api/StubContext.cs @@ -4,7 +4,6 @@ using System.Collections.Generic; using System.Threading; using System.IO; using System.Diagnostics; -using Microsoft.Contracts; using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie; using Microsoft.Boogie.Z3; diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index 0d79bd5a..009a6a59 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -4,7 +4,6 @@ using System.Collections.Generic; using System.Threading; using System.IO; using System.Diagnostics; -using Microsoft.Contracts; using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie; using Microsoft.Boogie.Z3; diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index a659c3f2..19b6348a 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -82,10 +82,6 @@ ..\..\..\Binaries\Microsoft.Z3.dll - - False - ..\..\..\Binaries\System.Compiler.Runtime.dll - 3.5 diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index c63a158f..6cc021fa 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -227,8 +227,8 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); storeTypes[i] = abstractedType; else storeTypes[i] = AxBuilder.U; - Microsoft.Contracts.NonNullType.AssertInitialized(selectTypes); - Microsoft.Contracts.NonNullType.AssertInitialized(storeTypes); + Contract.Assert(cce.NonNullElements(selectTypes)); + Contract.Assert(cce.NonNullElements(storeTypes)); select = HelperFuns.BoogieFunction(baseName + "Select", selectTypes); store = HelperFuns.BoogieFunction(baseName + "Store", storeTypes); diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj index 382a6694..116112a0 100644 --- a/Source/VCExpr/VCExpr.csproj +++ b/Source/VCExpr/VCExpr.csproj @@ -100,10 +100,6 @@ - - False - ..\..\Binaries\System.Compiler.Runtime.dll - diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 7002ad61..d465a483 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -362,9 +362,9 @@ namespace VC coverageProcess.StandardInput.WriteLine("batch-graph-command-begin"); coverageProcess.StandardInput.WriteLine("reset-color"); // Go through the curr candidates and draw edges - var nodes = new Microsoft.SpecSharp.Collections.Set(); - var greenNodes = new Microsoft.SpecSharp.Collections.Set(); - var redNodes = new Microsoft.SpecSharp.Collections.Set(); + var nodes = new HashSet(); + var greenNodes = new HashSet(); + var redNodes = new HashSet(); var edges = new List>(); foreach (var id in calls.currCandidates) { @@ -1365,7 +1365,7 @@ namespace VC // User info -- to decrease/increase calculcation of recursion bound public Dictionary recursionIncrement; - public Microsoft.SpecSharp.Collections.Set currCandidates; + public HashSet currCandidates; [ContractInvariantMethod] void ObjectInvariant() { @@ -1398,7 +1398,7 @@ namespace VC id2ControlVar = new Dictionary(); boogieExpr2Id = new Dictionary(); label2Id = new Dictionary(); - currCandidates = new Microsoft.SpecSharp.Collections.Set(); + currCandidates = new HashSet(); currInlineCount = 0; currProc = null; labelRenamer = new Dictionary(); @@ -1410,7 +1410,7 @@ namespace VC public void Clear() { - currCandidates = new Microsoft.SpecSharp.Collections.Set(); + currCandidates = new HashSet(); } // Given a candidate "id", let proc(id) be the diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index b2d514f6..9906070a 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -99,15 +99,7 @@ true - - False - ..\..\Binaries\Microsoft.SpecSharp.Runtime.dll - - - False - ..\..\Binaries\System.Compiler.Runtime.dll - diff --git a/Test/test15/Answer b/Test/test15/Answer index 4d0b3bad..f989c7bd 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -211,7 +211,7 @@ F -> *10 m@0 -> -2 r@0 -> -2 x@@4 -> 797 -m@1 -> -1 +m@2 -> -1 m@3 -> -1 y@@1 -> **y@@1 r -> **r @@ -250,8 +250,8 @@ MapType0TypeInv0 -> { } @MV_state -> { 0 -> true - 1 -> true - 2 -> true + 3 -> true + 4 -> true 5 -> true } [3] -> { -- cgit v1.2.3