From fb226b8b4b9315a0ad2df1fcd1b4a7f12e118791 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Tue, 23 Sep 2014 11:32:04 +0200 Subject: Did some refactoring. --- Source/AbsInt/NativeLattice.cs | 15 +-- Source/AbsInt/Traverse.cs | 31 +++-- Source/Concurrency/LinearSets.cs | 9 +- Source/Concurrency/OwickiGries.cs | 10 +- Source/Concurrency/TypeCheck.cs | 5 +- Source/Concurrency/YieldTypeChecker.cs | 5 +- Source/Core/Absy.cs | 108 +++++++++++------ Source/Core/DeadVarElim.cs | 40 +++---- Source/Core/Duplicator.cs | 2 +- Source/Core/Inline.cs | 7 +- Source/Core/InterProceduralReachabilityGraph.cs | 6 +- Source/Core/VariableDependenceAnalyser.cs | 12 +- Source/Doomed/VCDoomed.cs | 5 +- Source/ExecutionEngine/ExecutionEngine.cs | 11 +- Source/ExecutionEngine/VerificationResultCache.cs | 8 +- Source/Houdini/AbstractHoudini.cs | 80 ++++++------- Source/Houdini/CandidateDependenceAnalyser.cs | 16 +-- Source/Houdini/ConcurrentHoudini.cs | 4 +- Source/Houdini/Houdini.cs | 27 ++--- Source/Predication/UniformityAnalyser.cs | 10 +- Source/VCGeneration/Check.cs | 8 +- Source/VCGeneration/ConditionGeneration.cs | 2 +- Source/VCGeneration/FixedpointVC.cs | 135 +++++++--------------- Source/VCGeneration/StratifiedVC.cs | 12 +- Source/VCGeneration/VC.cs | 14 +-- 25 files changed, 254 insertions(+), 328 deletions(-) diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs index 8bb44385..30014643 100644 --- a/Source/AbsInt/NativeLattice.cs +++ b/Source/AbsInt/NativeLattice.cs @@ -120,8 +120,7 @@ namespace Microsoft.Boogie.AbstractInterpretation // procedures. return program - .TopLevelDeclarations - .Where(d => d is Implementation).Select(i => (Implementation)i) + .Implementations .GroupBy(i => i.Proc).Select(g => g.ToArray()).ToDictionary(a => a[0].Proc); } @@ -137,17 +136,13 @@ namespace Microsoft.Boogie.AbstractInterpretation // Differently stated, it is the \alpha from axioms (i.e. first order formulae) to the underlyng abstract domain var initialElement = lattice.Top; Contract.Assert(initialElement != null); - foreach (var decl in program.TopLevelDeclarations) { - var ax = decl as Axiom; - if (ax != null) { - initialElement = lattice.Constrain(initialElement, ax.Expr); - } + foreach (var ax in program.Axioms) { + initialElement = lattice.Constrain(initialElement, ax.Expr); } // analyze each procedure - foreach (var decl in program.TopLevelDeclarations) { - var proc = decl as Procedure; - if (proc != null && procedureImplementations.ContainsKey(proc)) { + foreach (var proc in program.Procedures) { + if (procedureImplementations.ContainsKey(proc)) { // analyze each implementation of the procedure foreach (var impl in procedureImplementations[proc]) { // add the precondition to the axioms diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs index 633ad86e..184a4071 100644 --- a/Source/AbsInt/Traverse.cs +++ b/Source/AbsInt/Traverse.cs @@ -24,25 +24,22 @@ namespace Microsoft.Boogie { Contract.Requires(program != null); cce.BeginExpose(program); - foreach (Declaration m in program.TopLevelDeclarations) { - Implementation impl = m as Implementation; - if (impl != null) { - if (impl.Blocks != null && impl.Blocks.Count > 0) { - Contract.Assume(cce.IsConsistent(impl)); - cce.BeginExpose(impl); - Block start = impl.Blocks[0]; - Contract.Assume(start != null); - Contract.Assume(cce.IsConsistent(start)); - Visit(start); - - // We reset the state... - foreach (Block b in impl.Blocks) { - cce.BeginExpose(b); - b.TraversingStatus = Block.VisitState.ToVisit; - cce.EndExpose(); - } + foreach (var impl in program.Implementations) { + if (impl.Blocks != null && impl.Blocks.Count > 0) { + Contract.Assume(cce.IsConsistent(impl)); + cce.BeginExpose(impl); + Block start = impl.Blocks[0]; + Contract.Assume(start != null); + Contract.Assume(cce.IsConsistent(start)); + Visit(start); + + // We reset the state... + foreach (Block b in impl.Blocks) { + cce.BeginExpose(b); + b.TraversingStatus = Block.VisitState.ToVisit; cce.EndExpose(); } + cce.EndExpose(); } } cce.EndExpose(); diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs index f9a791bc..b6e23e38 100644 --- a/Source/Concurrency/LinearSets.cs +++ b/Source/Concurrency/LinearSets.cs @@ -634,10 +634,8 @@ namespace Microsoft.Boogie public void Transform() { - foreach (var decl in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - Implementation impl = decl as Implementation; - if (impl == null) continue; Dictionary domainNameToInputVar = new Dictionary(); foreach (string domainName in linearDomains.Keys) { @@ -739,11 +737,8 @@ namespace Microsoft.Boogie } } - foreach (var decl in program.TopLevelDeclarations) + foreach (var proc in program.Procedures) { - Procedure proc = decl as Procedure; - if (proc == null) continue; - Dictionary> domainNameToInputScope = new Dictionary>(); Dictionary> domainNameToOutputScope = new Dictionary>(); foreach (var domainName in linearDomains.Keys) diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs index 23c8945b..baea905a 100644 --- a/Source/Concurrency/OwickiGries.cs +++ b/Source/Concurrency/OwickiGries.cs @@ -1182,19 +1182,17 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.TrustPhasesDownto <= phaseNum || phaseNum <= CommandLineOptions.Clo.TrustPhasesUpto) continue; MyDuplicator duplicator = new MyDuplicator(moverTypeChecker, phaseNum); - foreach (var decl in program.TopLevelDeclarations) + foreach (var proc in program.Procedures) { - Procedure proc = decl as Procedure; - if (proc == null || !moverTypeChecker.procToActionInfo.ContainsKey(proc)) continue; + 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 decl in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - Implementation impl = decl as Implementation; - if (impl == null || !moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum) + if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum < phaseNum) continue; Implementation duplicateImpl = duplicator.VisitImplementation(impl); ogTransform.TransformImpl(duplicateImpl); diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs index 5fd67978..cd636946 100644 --- a/Source/Concurrency/TypeCheck.cs +++ b/Source/Concurrency/TypeCheck.cs @@ -269,10 +269,9 @@ namespace Microsoft.Boogie public void TypeCheck() { - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var proc in program.Procedures) { - Procedure proc = decl as Procedure; - if (proc == null || !QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; + if (!QKeyValue.FindBoolAttribute(proc.Attributes, "yields")) continue; int phaseNum = int.MaxValue; int availableUptoPhaseNum = int.MaxValue; diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 98657706..7a037f93 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -134,10 +134,9 @@ namespace Microsoft.Boogie public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker) { - foreach (var decl in moverTypeChecker.program.TopLevelDeclarations) + foreach (var impl in moverTypeChecker.program.Implementations) { - Implementation impl = decl as Implementation; - if (impl == null || !moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum == 0) continue; + if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].phaseNum == 0) continue; impl.PruneUnreachableBlocks(); Graph implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index b48ddd3b..baefd09a 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -361,20 +361,19 @@ namespace Microsoft.Boogie { //Contract.Requires(rc != null); Helpers.ExtraTraceInformation("Starting resolution"); - foreach (Declaration d in TopLevelDeclarations) { + foreach (var d in TopLevelDeclarations) { d.Register(rc); } ResolveTypes(rc); var prunedTopLevelDecls = new List(); - foreach (Declaration d in TopLevelDeclarations) { + foreach (var d in TopLevelDeclarations) { if (QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) { continue; } // resolve all the non-type-declarations - if (d is TypeCtorDecl || d is TypeSynonymDecl) { - } else { + if (!(d is TypeCtorDecl || d is TypeSynonymDecl)) { int e = rc.ErrorCount; d.Resolve(rc); if (CommandLineOptions.Clo.OverlookBoogieTypeErrors && rc.ErrorCount != e && d is Implementation) { @@ -388,27 +387,24 @@ namespace Microsoft.Boogie { } TopLevelDeclarations = prunedTopLevelDecls; - foreach (Declaration d in TopLevelDeclarations) { - Variable v = d as Variable; - if (v != null) { - v.ResolveWhere(rc); - } + foreach (var v in Variables) { + v.ResolveWhere(rc); } } private void ResolveTypes(ResolutionContext rc) { Contract.Requires(rc != null); // first resolve type constructors - foreach (Declaration d in TopLevelDeclarations) { - if (d is TypeCtorDecl && !QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) + foreach (var d in TopLevelDeclarations.OfType()) { + if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) d.Resolve(rc); } // collect type synonym declarations List/*!*/ synonymDecls = new List(); - foreach (Declaration d in TopLevelDeclarations) { + foreach (var d in TopLevelDeclarations.OfType()) { Contract.Assert(d != null); - if (d is TypeSynonymDecl && !QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) + if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore")) synonymDecls.Add((TypeSynonymDecl)d); } @@ -432,31 +428,74 @@ namespace Microsoft.Boogie { Helpers.ExtraTraceInformation("Starting typechecking"); int oldErrorCount = tc.ErrorCount; - foreach (Declaration d in TopLevelDeclarations) { + foreach (var d in TopLevelDeclarations) { d.Typecheck(tc); } if (oldErrorCount == tc.ErrorCount) { // check whether any type proxies have remained uninstantiated TypeAmbiguitySeeker/*!*/ seeker = new TypeAmbiguitySeeker(tc); - foreach (Declaration d in TopLevelDeclarations) { + foreach (var d in TopLevelDeclarations) { seeker.Visit(d); } } } - public IEnumerable Implementations() + public IEnumerable Implementations + { + get + { + return TopLevelDeclarations.OfType(); + } + } + + public IEnumerable Axioms + { + get + { + return TopLevelDeclarations.OfType(); + } + } + + public IEnumerable Procedures + { + get + { + return TopLevelDeclarations.OfType(); + } + } + + public IEnumerable Functions + { + get + { + return TopLevelDeclarations.OfType(); + } + } + + public IEnumerable Variables + { + get + { + return TopLevelDeclarations.OfType(); + } + } + + public IEnumerable Constants { - return TopLevelDeclarations.OfType(); + get + { + return TopLevelDeclarations.OfType(); + } } public IEnumerable Blocks() { - return Implementations().Select(Item => Item.Blocks).SelectMany(Item => Item); + return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); } public void ComputeStronglyConnectedComponents() { - foreach (Declaration d in this.TopLevelDeclarations) { + foreach (var d in this.TopLevelDeclarations) { d.ComputeStronglyConnectedComponents(); } } @@ -465,14 +504,14 @@ namespace Microsoft.Boogie { /// Reset the abstract stated computed before /// public void ResetAbstractInterpretationState() { - foreach (Declaration d in this.TopLevelDeclarations) { + foreach (var d in this.TopLevelDeclarations) { d.ResetAbstractInterpretationState(); } } public void UnrollLoops(int n, bool uc) { Contract.Requires(0 <= n); - foreach (var impl in Implementations()) { + foreach (var impl in Implementations) { if (impl.Blocks != null && impl.Blocks.Count > 0) { cce.BeginExpose(impl); { @@ -874,20 +913,16 @@ namespace Microsoft.Boogie { public static Graph BuildCallGraph(Program program) { Graph callGraph = new Graph(); Dictionary> procToImpls = new Dictionary>(); - foreach (Declaration decl in program.TopLevelDeclarations) { - Procedure proc = decl as Procedure; - if (proc == null) continue; + foreach (var proc in program.Procedures) { procToImpls[proc] = new HashSet(); } - foreach (Declaration decl in program.TopLevelDeclarations) { - Implementation impl = decl as Implementation; - if (impl == null || impl.SkipVerification) continue; + foreach (var impl in program.Implementations) { + if (impl.SkipVerification) continue; callGraph.AddSource(impl); procToImpls[impl.Proc].Add(impl); } - foreach (Declaration decl in program.TopLevelDeclarations) { - Implementation impl = decl as Implementation; - if (impl == null || impl.SkipVerification) continue; + foreach (var impl in program.Implementations) { + if (impl.SkipVerification) continue; foreach (Block b in impl.Blocks) { foreach (Cmd c in b.Cmds) { CallCmd cc = c as CallCmd; @@ -984,10 +1019,9 @@ namespace Microsoft.Boogie { procsWithIrreducibleLoops = new HashSet(); List/*!*/ loopImpls = new List(); Dictionary> fullMap = new Dictionary>(); - foreach (Declaration d in this.TopLevelDeclarations) + foreach (var impl in this.Implementations) { - Implementation impl = d as Implementation; - if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) + if (impl.Blocks != null && impl.Blocks.Count > 0) { try { @@ -1046,15 +1080,13 @@ namespace Microsoft.Boogie { } private List globals = null; - public List/*!*/ GlobalVariables() { + public IEnumerable/*!*/ GlobalVariables() { Contract.Ensures(cce.NonNullElements(Contract.Result>())); if (globals != null) return globals; globals = new List(); - foreach (Declaration d in TopLevelDeclarations) { - GlobalVariable gvar = d as GlobalVariable; - if (gvar != null) - globals.Add(gvar); + foreach (var gvar in TopLevelDeclarations.OfType()) { + globals.Add(gvar); } return globals; } diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index b54a45c1..e6cf3e9d 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -73,32 +73,24 @@ namespace Microsoft.Boogie { } HashSet implementedProcs = new HashSet(); - foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) { - Contract.Assert(decl != null); - if (decl is Implementation) { - Implementation impl = (Implementation)decl; - if (impl.Proc != null) - implementedProcs.Add(impl.Proc); - } + foreach (var impl in program.Implementations) { + if (impl.Proc != null) + implementedProcs.Add(impl.Proc); } - foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) { - Contract.Assert(decl != null); - if (decl is Procedure) + foreach (var proc in program.Procedures) { + if (!implementedProcs.Contains(proc)) { - if (!implementedProcs.Contains(cce.NonNull((Procedure)decl))) + enclosingProc = proc; + foreach (var expr in proc.Modifies) { - enclosingProc = (Procedure)decl; - foreach (IdentifierExpr/*!*/ expr in enclosingProc.Modifies) - { - Contract.Assert(expr != null); - ProcessVariable(expr.Decl); - } - enclosingProc = null; - } - else - { - modSets.Add(decl as Procedure, new HashSet()); + Contract.Assert(expr != null); + ProcessVariable(expr.Decl); } + enclosingProc = null; + } + else + { + modSets.Add(proc, new HashSet()); } } @@ -917,7 +909,7 @@ namespace Microsoft.Boogie { varsLiveAtEntry.Clear(); varsLiveSummary.Clear(); - foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) { + foreach (var decl in program.TopLevelDeclarations) { Contract.Assert(decl != null); if (decl is Implementation) { Implementation/*!*/ imp = (Implementation/*!*/)cce.NonNull(decl); @@ -1490,7 +1482,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) { LiteralExpr le = (LiteralExpr)predicateCmd.Expr; if (le.IsFalse) { - List/*!*/ globals = prog.GlobalVariables(); + var globals = prog.GlobalVariables(); Contract.Assert(cce.NonNullElements(globals)); foreach (Variable/*!*/ v in globals) { Contract.Assert(v != null); diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 86311d18..6dd030e8 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -641,7 +641,7 @@ namespace Microsoft.Boogie { if (funCall != null) { // TODO(wuestholz): Maybe we should speed up this lookup. - funCall.Func = Program.TopLevelDeclarations.OfType().FirstOrDefault(f => f.Name == funCall.FunctionName); + funCall.Func = Program.Functions.FirstOrDefault(f => f.Name == funCall.FunctionName); } } return result; diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 4738d855..fc2608b7 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -202,7 +202,7 @@ namespace Microsoft.Boogie { Contract.Ensures(impl.Proc != null); ResolutionContext rc = new ResolutionContext(new DummyErrorSink()); - foreach (Declaration decl in program.TopLevelDeclarations) { + foreach (var decl in program.TopLevelDeclarations) { decl.Register(rc); } @@ -675,9 +675,8 @@ namespace Microsoft.Boogie { protected static Implementation FindProcImpl(Program program, Procedure proc) { Contract.Requires(program != null); - foreach (Declaration decl in program.TopLevelDeclarations) { - Implementation impl = decl as Implementation; - if (impl != null && impl.Proc == proc) { + foreach (var impl in program.Implementations) { + if (impl.Proc == proc) { return impl; } } diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs index ccf4b153..b477e7de 100644 --- a/Source/Core/InterProceduralReachabilityGraph.cs +++ b/Source/Core/InterProceduralReachabilityGraph.cs @@ -63,7 +63,7 @@ namespace Microsoft.Boogie private IEnumerable OriginalProgramBlocks() { - return prog.TopLevelDeclarations.OfType().Select(Item => Item.Blocks).SelectMany(Item => Item); + return prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); } private void AddCallAndReturnEdges() @@ -118,7 +118,7 @@ namespace Microsoft.Boogie private void ProcessBodilessProcedures() { #region Add single node CFG for procedures with no body - foreach (var proc in prog.TopLevelDeclarations.OfType()) + foreach (var proc in prog.Procedures) { if (!newProcedureEntryNodes.ContainsKey(proc.Name)) { @@ -134,7 +134,7 @@ namespace Microsoft.Boogie private void ProcessImplementations() { #region Transform implementation CFGs so that every call is in its own basic block - foreach (var impl in prog.TopLevelDeclarations.OfType()) + foreach (var impl in prog.Implementations) { string exitLabel = "__" + impl.Name + "_newExit"; Block newExit = new Block(Token.NoToken, exitLabel, new List(), new GotoCmd(Token.NoToken, new List())); diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 476f1cac..c429e199 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -135,7 +135,7 @@ namespace Microsoft.Boogie { private void Initialise() { foreach (var descriptor in - prog.TopLevelDeclarations.OfType().Where(Item => VariableRelevantToAnalysis(Item, null)). + prog.Variables.Where(Item => VariableRelevantToAnalysis(Item, null)). Select(Variable => Variable.Name). Select(Name => new GlobalDescriptor(Name))) { dependsOnNonTransitive.AddEdge(descriptor, descriptor); @@ -164,12 +164,12 @@ namespace Microsoft.Boogie { } private IEnumerable NonInlinedProcedures() { - return prog.TopLevelDeclarations.OfType(). + return prog.Procedures. Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1); } private IEnumerable NonInlinedImplementations() { - return prog.TopLevelDeclarations.OfType(). + return prog.Implementations. Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1); } @@ -439,7 +439,7 @@ namespace Microsoft.Boogie { Dictionary>> LocalCtrlDeps = new Dictionary>>(); // Work out and union together local control dependences - foreach (var Impl in prog.TopLevelDeclarations.OfType()) { + foreach (var Impl in prog.Implementations) { Graph blockGraph = prog.ProcessLoops(Impl); LocalCtrlDeps[Impl] = blockGraph.ControlDependence(); foreach (var KeyValue in LocalCtrlDeps[Impl]) { @@ -450,7 +450,7 @@ namespace Microsoft.Boogie { Graph callGraph = Program.BuildCallGraph(prog); // Add inter-procedural control dependence nodes based on calls - foreach (var Impl in prog.TopLevelDeclarations.OfType()) { + foreach (var Impl in prog.Implementations) { foreach (var b in Impl.Blocks) { foreach (var cmd in b.Cmds.OfType()) { var DirectCallee = GetImplementation(cmd.callee); @@ -513,7 +513,7 @@ namespace Microsoft.Boogie { } private Implementation GetImplementation(string proc) { - foreach (var Impl in prog.TopLevelDeclarations.OfType()) { + foreach (var Impl in prog.Implementations) { if (Impl.Name.Equals(proc)) { return Impl; } diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index 6dd3b5ca..4fd574a4 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -594,9 +594,8 @@ namespace VC { { List cc = new List(); // where clauses of global variables - foreach (Declaration d in program.TopLevelDeclarations) { - GlobalVariable gvar = d as GlobalVariable; - if (gvar != null && gvar.TypedIdent.WhereExpr != null) { + foreach (var gvar in program.GlobalVariables()) { + if (gvar.TypedIdent.WhereExpr != null) { Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr); cc.Add(c); } diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index a9220a4c..093f1d90 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -467,7 +467,7 @@ namespace Microsoft.Boogie if (CommandLineOptions.Clo.PrintCFGPrefix != null) { - foreach (var impl in program.TopLevelDeclarations.OfType()) + foreach (var impl in program.Implementations) { using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot")) { @@ -868,7 +868,7 @@ namespace Microsoft.Boogie #region Select and prioritize implementations that should be verified - var impls = program.TopLevelDeclarations.OfType().Where( + var impls = program.Implementations.Where( impl => impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification); // operate on a stable copy, in case it gets updated while we're running @@ -876,7 +876,7 @@ namespace Microsoft.Boogie if (0 < CommandLineOptions.Clo.VerifySnapshots) { // TODO(wuestholz): Maybe we should speed up this lookup. - OtherDefinitionAxiomsCollector.Collect(program.TopLevelDeclarations.OfType()); + OtherDefinitionAxiomsCollector.Collect(program.Axioms); DependencyCollector.Collect(program); stablePrioritizedImpls = impls.OrderByDescending( impl => impl.Priority != 1 ? impl.Priority : Cache.VerificationPriority(impl)).ToArray(); @@ -1084,10 +1084,9 @@ namespace Microsoft.Boogie var svcgen = vcgen as VC.StratifiedVCGen; Contract.Assert(svcgen != null); var ss = new HashSet(); - foreach (var tdecl in program.TopLevelDeclarations) + foreach (var c in program.Constants) { - var c = tdecl as Constant; - if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue; + if (!c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue; ss.Add(c.Name); } verificationResult.Outcome = svcgen.FindLeastToVerify(impl, ref ss); diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs index 55c6ba85..93ca9cb7 100644 --- a/Source/ExecutionEngine/VerificationResultCache.cs +++ b/Source/ExecutionEngine/VerificationResultCache.cs @@ -194,7 +194,7 @@ namespace Microsoft.Boogie private static void SetAssertionChecksums(Implementation implementation, Program program) { // TODO(wuestholz): Maybe we should speed up this lookup. - var implPrevSnap = program.Implementations().FirstOrDefault(i => i.Id == implementation.Id); + var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id); if (implPrevSnap != null) { implementation.AssertionChecksums = implPrevSnap.AssertionChecksums; @@ -204,7 +204,7 @@ namespace Microsoft.Boogie private static void SetAssertionChecksumsInPreviousSnapshot(Implementation implementation, Program program) { // TODO(wuestholz): Maybe we should speed up this lookup. - var implPrevSnap = program.Implementations().FirstOrDefault(i => i.Id == implementation.Id); + var implPrevSnap = program.Implementations.FirstOrDefault(i => i.Id == implementation.Id); if (implPrevSnap != null) { implementation.AssertionChecksumsInPreviousSnapshot = implPrevSnap.AssertionChecksums; @@ -216,7 +216,7 @@ namespace Microsoft.Boogie var result = base.VisitCallCmd(node); // TODO(wuestholz): Maybe we should speed up this lookup. - var oldProc = programInCachedSnapshot.TopLevelDeclarations.OfType().FirstOrDefault(p => p.Name == node.Proc.Name); + var oldProc = programInCachedSnapshot.Procedures.FirstOrDefault(p => p.Name == node.Proc.Name); if (oldProc != null && oldProc.DependencyChecksum != node.Proc.DependencyChecksum && node.AssignedAssumptionVariable == null) @@ -327,7 +327,7 @@ namespace Microsoft.Boogie Contract.Requires(oldProc != null && newProg != null); // TODO(wuestholz): Maybe we should speed up this lookup. - var funcs = newProg.TopLevelDeclarations.OfType(); + var funcs = newProg.Functions; return oldProc.DependenciesCollected && (oldProc.FunctionDependencies == null || oldProc.FunctionDependencies.All(dep => funcs.Any(f => f.Name == dep.Name && f.DependencyChecksum == dep.DependencyChecksum))); } diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index c73758d8..e268a8d7 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -58,7 +58,7 @@ namespace Microsoft.Boogie.Houdini { this.constant2FuncCall = new Dictionary(); // Find the existential functions - foreach (var func in program.TopLevelDeclarations.OfType() + foreach (var func in program.Functions .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential"))) existentialFunctions.Add(func.Name, func); @@ -104,7 +104,7 @@ namespace Microsoft.Boogie.Houdini { this.proverTime = TimeSpan.Zero; this.numProverQueries = 0; - program.TopLevelDeclarations.OfType() + program.Implementations .Where(impl => !impl.SkipVerification) .Iter(impl => name2Impl.Add(impl.Name, impl)); @@ -753,23 +753,19 @@ namespace Microsoft.Boogie.Houdini { { Graph callGraph = new Graph(); Dictionary> procToImpls = new Dictionary>(); - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var proc in program.Procedures) { - Procedure proc = decl as Procedure; - if (proc == null) continue; procToImpls[proc] = new HashSet(); } - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - Implementation impl = decl as Implementation; - if (impl == null || impl.SkipVerification) continue; + if (impl.SkipVerification) continue; callGraph.AddSource(impl); procToImpls[impl.Proc].Add(impl); } - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - Implementation impl = decl as Implementation; - if (impl == null || impl.SkipVerification) continue; + if (impl.SkipVerification) continue; foreach (Block b in impl.Blocks) { foreach (Cmd c in b.Cmds) @@ -2139,8 +2135,7 @@ namespace Microsoft.Boogie.Houdini { }); domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2)); - program.TopLevelDeclarations.OfType() - .Iter(RegisterFunction); + program.Functions.Iter(RegisterFunction); } private static void RegisterFunction(Function func) @@ -2227,8 +2222,7 @@ namespace Microsoft.Boogie.Houdini { name2Impl.Values.Iter(attachEnsures); - program.TopLevelDeclarations - .OfType() + program.Implementations .Iter(impl => impl2Summary.Add(impl.Name, summaryClass.GetFlaseSummary(program, impl))); // Build call graph @@ -2237,7 +2231,7 @@ namespace Microsoft.Boogie.Houdini { name2Impl.Values.Iter(impl => Succ.Add(impl, new HashSet())); name2Impl.Values.Iter(impl => Pred.Add(impl, new HashSet())); - foreach (var impl in program.TopLevelDeclarations.OfType()) + foreach (var impl in program.Implementations) { foreach (var blk in impl.Blocks) { @@ -2276,7 +2270,7 @@ namespace Microsoft.Boogie.Houdini { var copy = new Dictionary(); if (WitnessFile != null) { - foreach (var impl in program.TopLevelDeclarations.OfType()) + foreach (var impl in program.Implementations) { var nimpl = new Implementation(Token.NoToken, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, new List(impl.LocVars), new List()); @@ -2365,7 +2359,7 @@ namespace Microsoft.Boogie.Houdini { return Expr.True; var vars = new Dictionary(); - foreach (var g in program.TopLevelDeclarations.OfType()) + foreach (var g in program.GlobalVariables()) vars.Add(g.Name, Expr.Ident(g)); foreach (var v in proc.InParams.OfType()) vars.Add(v.Name, Expr.Ident(v)); @@ -2389,7 +2383,7 @@ namespace Microsoft.Boogie.Houdini { if (WitnessFile == null) return; - foreach (var proc in program.TopLevelDeclarations.OfType()) + foreach (var proc in program.Procedures) { var nensures = new List(); proc.Ensures.OfType() @@ -2411,7 +2405,7 @@ namespace Microsoft.Boogie.Houdini { .Iter(decl => decls.Add(decl)); program.TopLevelDeclarations = decls; var name2Proc = new Dictionary(); - foreach (var proc in program.TopLevelDeclarations.OfType()) + foreach (var proc in program.Procedures) { name2Proc.Add(proc.Name, proc); if (impl2Summary.ContainsKey(proc.Name)) @@ -2430,7 +2424,7 @@ namespace Microsoft.Boogie.Houdini { } // Replace SummaryPreds with their definition - foreach (var impl in program.TopLevelDeclarations.OfType()) + foreach (var impl in program.Implementations) { foreach (var blk in impl.Blocks) { @@ -2448,7 +2442,7 @@ namespace Microsoft.Boogie.Houdini { var forold = new Dictionary(); var always = new Dictionary(); int i = 0; - foreach (var g in program.TopLevelDeclarations.OfType()) + foreach (var g in program.GlobalVariables()) { forold.Add(g.Name, expr.Args[i]); always.Add(g.Name, expr.Args[i]); @@ -2556,23 +2550,19 @@ namespace Microsoft.Boogie.Houdini { { Graph callGraph = new Graph(); Dictionary> procToImpls = new Dictionary>(); - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var proc in program.Procedures) { - Procedure proc = decl as Procedure; - if (proc == null) continue; procToImpls[proc] = new HashSet(); } - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - Implementation impl = decl as Implementation; - if (impl == null || impl.SkipVerification) continue; + if (impl.SkipVerification) continue; callGraph.AddSource(impl); procToImpls[impl.Proc].Add(impl); } - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - Implementation impl = decl as Implementation; - if (impl == null || impl.SkipVerification) continue; + if (impl.SkipVerification) continue; foreach (Block b in impl.Blocks) { foreach (Cmd c in b.Cmds) @@ -2753,7 +2743,7 @@ namespace Microsoft.Boogie.Houdini { var ret = new Dictionary(); var cnt = 0; - foreach (var g in program.TopLevelDeclarations.OfType()) + foreach (var g in program.GlobalVariables()) { ret.Add(string.Format("old({0})", g.Name), summaryPred[cnt]); cnt++; @@ -2768,7 +2758,7 @@ namespace Microsoft.Boogie.Houdini { // Fill up values of globals that are not modified cnt = 0; - foreach (var g in program.TopLevelDeclarations.OfType()) + foreach (var g in program.GlobalVariables()) { if (ret.ContainsKey(g.Name)) { cnt++; continue; } @@ -2777,7 +2767,7 @@ namespace Microsoft.Boogie.Houdini { } // Constants - foreach (var c in program.TopLevelDeclarations.OfType()) + foreach (var c in program.Constants) { var value = prover.Context.BoogieExprTranslator.Translate(Expr.Ident(c)); ret.Add(string.Format("{0}", c.Name), value); @@ -2795,7 +2785,7 @@ namespace Microsoft.Boogie.Houdini { var implVars = impl2EndStateVars[impl.Name]; var cnt = 0; - foreach (var g in program.TopLevelDeclarations.OfType()) + foreach (var g in program.GlobalVariables()) { ret.Add(string.Format("old({0})", g.Name), getValue(implVars[cnt], model)); cnt++; @@ -2810,7 +2800,7 @@ namespace Microsoft.Boogie.Houdini { // Fill up values of globals that are not modified cnt = 0; - foreach (var g in program.TopLevelDeclarations.OfType()) + foreach (var g in program.GlobalVariables()) { if (ret.ContainsKey(g.Name)) { cnt++; continue; } @@ -2819,7 +2809,7 @@ namespace Microsoft.Boogie.Houdini { } // Constants - foreach (var c in program.TopLevelDeclarations.OfType()) + foreach (var c in program.Constants) { try { @@ -3231,7 +3221,7 @@ namespace Microsoft.Boogie.Houdini { boolConstants = new HashSet(); UpperCandidates = new Dictionary, List>(); - program.TopLevelDeclarations.OfType() + program.Constants .Where(c => c.TypedIdent.Type.IsBool) .Iter(c => boolConstants.Add(c.Name)); @@ -3241,7 +3231,7 @@ namespace Microsoft.Boogie.Houdini { var posPreT = new HashSet(); var tempP = new HashSet(); foreach (var proc in - program.TopLevelDeclarations.OfType() + program.Procedures .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template"))) { tempP.Add(proc); @@ -3274,7 +3264,7 @@ namespace Microsoft.Boogie.Houdini { program.TopLevelDeclarations.RemoveAll(decl => tempP.Contains(decl)); var upperPreds = new Dictionary>(); - foreach (var impl in program.TopLevelDeclarations.OfType()) + foreach (var impl in program.Implementations) { PrePreds.Add(impl.Name, new List()); PostPreds.Add(impl.Name, new List()); @@ -3876,7 +3866,7 @@ namespace Microsoft.Boogie.Houdini { Simplify(); // Find the free expressions - var proc = program.TopLevelDeclarations.OfType().FirstOrDefault(p => p.Name == procName); + var proc = program.Procedures.FirstOrDefault(p => p.Name == procName); Contract.Assert(proc != null); Expr freeSummary = Expr.True; foreach (var req in proc.Requires.OfType().Where(req => req.Free)) @@ -4598,13 +4588,9 @@ namespace Microsoft.Boogie.Houdini { public static Dictionary nameImplMapping(Program p) { var m = new Dictionary(); - foreach (Declaration d in p.TopLevelDeclarations) + foreach (var impl in p.Implementations) { - if (d is Implementation) - { - Implementation impl = d as Implementation; - m.Add(impl.Name, impl); - } + m.Add(impl.Name, impl); } return m; diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index ea891dd6..9ff333dc 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -185,7 +185,7 @@ namespace Microsoft.Boogie.Houdini { private IEnumerable CandidateInstances() { - foreach (var impl in prog.TopLevelDeclarations.OfType()) + foreach (var impl in prog.Implementations) { foreach (var b in impl.Blocks) { foreach (Cmd cmd in b.Cmds) @@ -202,7 +202,7 @@ namespace Microsoft.Boogie.Houdini { } } - foreach (var proc in prog.TopLevelDeclarations.OfType()) + foreach (var proc in prog.Procedures) { foreach (Requires r in proc.Requires) { @@ -351,7 +351,7 @@ namespace Microsoft.Boogie.Houdini { } private IEnumerable GetCandidates() { - return prog.TopLevelDeclarations.OfType().Where(Item => + return prog.Variables.Where(Item => QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name); } @@ -409,7 +409,7 @@ namespace Microsoft.Boogie.Houdini { #endregion #region Adapt candidate assertions to take account of stages - foreach (var b in prog.TopLevelDeclarations.OfType().Select(Item => Item.Blocks).SelectMany(Item => Item)) + foreach (var b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item)) { List newCmds = new List(); foreach (var cmd in b.Cmds) @@ -433,7 +433,7 @@ namespace Microsoft.Boogie.Houdini { #endregion #region Adapt candidate pre/postconditions to take account of stages - foreach (var p in prog.TopLevelDeclarations.OfType()) + foreach (var p in prog.Procedures) { #region Handle the preconditions @@ -633,7 +633,7 @@ namespace Microsoft.Boogie.Houdini { this.candidateToOccurences = new Dictionary>(); // Add all candidate occurrences in blocks - foreach(Block b in prog.TopLevelDeclarations.OfType().Select(Item => Item.Blocks).SelectMany(Item => Item)) { + foreach(Block b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item)) { foreach(Cmd cmd in b.Cmds) { AssertCmd assertCmd = cmd as AssertCmd; if(assertCmd != null) { @@ -646,7 +646,7 @@ namespace Microsoft.Boogie.Houdini { } // Add all candidate occurrences in preconditions - foreach(var proc in prog.TopLevelDeclarations.OfType()) { + foreach(var proc in prog.Procedures) { foreach(Requires r in proc.Requires) { string c; if(Houdini.MatchCandidate(r.Condition, candidates, out c)) { @@ -656,7 +656,7 @@ namespace Microsoft.Boogie.Houdini { } // Add all candidate occurrences in preconditions - foreach(var proc in prog.TopLevelDeclarations.OfType()) { + foreach(var proc in prog.Procedures) { foreach(Ensures e in proc.Ensures) { string c; if(Houdini.MatchCandidate(e.Condition, candidates, out c)) { diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs index bfc96258..5c0f217f 100644 --- a/Source/Houdini/ConcurrentHoudini.cs +++ b/Source/Houdini/ConcurrentHoudini.cs @@ -46,7 +46,7 @@ namespace Microsoft.Boogie.Houdini RefutedAnnotation ra = null; Implementation refutationSite = null; - foreach (var r in program.TopLevelDeclarations.OfType()) { + foreach (var r in program.Implementations) { if (r.Name.Equals(refutedSharedAnnotations[key].RefutationSite.Name)) { refutationSite = r; break; @@ -56,7 +56,7 @@ namespace Microsoft.Boogie.Houdini if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.REQUIRES) { Procedure proc = null; - foreach (var p in program.TopLevelDeclarations.OfType()) { + foreach (var p in program.Procedures) { if (p.Name.Equals(refutedSharedAnnotations[key].CalleeProc.Name)) { proc = p; break; diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index e91d0528..6b1f2c39 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -399,14 +399,11 @@ namespace Microsoft.Boogie.Houdini { protected HashSet CollectExistentialConstants() { HashSet existentialConstants = new HashSet(); - foreach (Declaration decl in program.TopLevelDeclarations) { - Constant constant = decl as Constant; - if (constant != null) { - bool result = false; - if (constant.CheckBooleanAttribute("existential", ref result)) { - if (result == true) - existentialConstants.Add(constant); - } + foreach (var constant in program.Constants) { + bool result = false; + if (constant.CheckBooleanAttribute("existential", ref result)) { + if (result == true) + existentialConstants.Add(constant); } } return existentialConstants; @@ -898,7 +895,7 @@ namespace Microsoft.Boogie.Houdini { private int NumberOfStages() { int result = 1; - foreach(var c in program.TopLevelDeclarations.OfType()) { + foreach(var c in program.Constants) { result = Math.Max(result, 1 + QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1)); } return result; @@ -1103,7 +1100,7 @@ namespace Microsoft.Boogie.Houdini { protected Dictionary GetAssignmentWithStages(int currentStage, IEnumerable completedStages) { Dictionary result = new Dictionary(currentHoudiniState.Assignment); - foreach (var c in program.TopLevelDeclarations.OfType()) + foreach (var c in program.Constants) { int stageActive = QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1); if (stageActive != -1) @@ -1181,7 +1178,7 @@ namespace Microsoft.Boogie.Houdini { // Treat all assertions // TODO: do we need to also consider assumptions? - foreach (Block block in prog.TopLevelDeclarations.OfType().Select(item => item.Blocks).SelectMany(item => item)) { + foreach (Block block in prog.Implementations.Select(item => item.Blocks).SelectMany(item => item)) { List newCmds = new List(); foreach (Cmd cmd in block.Cmds) { string c; @@ -1190,7 +1187,7 @@ namespace Microsoft.Boogie.Houdini { var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0]; if (currentHoudiniState.Assignment[cVar]) { Dictionary cToTrue = new Dictionary(); - Variable cVarProg = prog.TopLevelDeclarations.OfType().Where(item => item.Name.Equals(c)).ToList()[0]; + Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0]; cToTrue[cVarProg] = Expr.True; newCmds.Add(new AssumeCmd(assertCmd.tok, Substituter.Apply(Substituter.SubstitutionFromHashtable(cToTrue), assertCmd.Expr), @@ -1204,14 +1201,14 @@ namespace Microsoft.Boogie.Houdini { block.Cmds = newCmds; } - foreach (var proc in prog.TopLevelDeclarations.OfType()) { + foreach (var proc in prog.Procedures) { List newRequires = new List(); foreach (Requires r in proc.Requires) { string c; if (MatchCandidate(r.Condition, out c)) { var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0]; if (currentHoudiniState.Assignment[cVar]) { - Variable cVarProg = prog.TopLevelDeclarations.OfType().Where(item => item.Name.Equals(c)).ToList()[0]; + Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0]; Dictionary subst = new Dictionary(); subst[cVarProg] = Expr.True; newRequires.Add(new Requires(Token.NoToken, true, @@ -1231,7 +1228,7 @@ namespace Microsoft.Boogie.Houdini { if (MatchCandidate(e.Condition, out c)) { var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0]; if (currentHoudiniState.Assignment[cVar]) { - Variable cVarProg = prog.TopLevelDeclarations.OfType().Where(item => item.Name.Equals(c)).ToList()[0]; + Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0]; Dictionary subst = new Dictionary(); subst[cVarProg] = Expr.True; newEnsures.Add(new Ensures(Token.NoToken, true, diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs index 3d6b7b18..ff298942 100644 --- a/Source/Predication/UniformityAnalyser.cs +++ b/Source/Predication/UniformityAnalyser.cs @@ -84,7 +84,7 @@ namespace Microsoft.Boogie public void Analyse() { - var impls = prog.TopLevelDeclarations.OfType(); + var impls = prog.Implementations; foreach (var Impl in impls) { @@ -143,7 +143,7 @@ namespace Microsoft.Boogie ProcedureChanged = true; } - var procs = prog.TopLevelDeclarations.OfType(); + var procs = prog.Procedures; foreach (var Proc in procs) { @@ -268,11 +268,11 @@ namespace Microsoft.Boogie private Procedure GetProcedure(string procedureName) { - foreach (Declaration D in prog.TopLevelDeclarations) + foreach (var p in prog.Procedures) { - if (D is Procedure && ((D as Procedure).Name == procedureName)) + if (p.Name == procedureName) { - return D as Procedure; + return p; } } Debug.Assert(false); diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 9fc301da..bb34c8f8 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -429,12 +429,8 @@ namespace Microsoft.Boogie { } } } - foreach (Declaration decl in prog.TopLevelDeclarations) { - Contract.Assert(decl != null); - Axiom ax = decl as Axiom; - if (ax != null) { - ctx.AddAxiom(ax, null); - } + foreach (var ax in prog.Axioms) { + ctx.AddAxiom(ax, null); } foreach (Declaration decl in prog.TopLevelDeclarations) { Contract.Assert(decl != null); diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 50a717f9..e74e0bbf 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1831,7 +1831,7 @@ namespace VC { // global variables lock (program.TopLevelDeclarations) { - foreach (Variable v in program.TopLevelDeclarations.OfType()) + foreach (var v in program.Variables) { if (!(v is Constant)) { diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 9f39e46c..04b976ea 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -392,56 +392,42 @@ namespace Microsoft.Boogie void MarkAllFunctionImplementationsInline() { - foreach (var d in program.TopLevelDeclarations) + foreach (var func in program.Functions) { - var impl = d as Function; - if (impl != null) + if (func.Body == null && func.DefinitionAxiom != null) { - if (impl.Body == null && impl.DefinitionAxiom != null) - { - var def = impl.DefinitionAxiom.Expr as QuantifierExpr; - var bod = def.Body as NAryExpr; - impl.Body = bod.Args[1]; - impl.DefinitionAxiom = null; - } - if (impl.Body != null) - if (impl.FindExprAttribute("inline") == null) - impl.AddAttribute("inline", Expr.Literal(100)); + var def = func.DefinitionAxiom.Expr as QuantifierExpr; + var bod = def.Body as NAryExpr; + func.Body = bod.Args[1]; + func.DefinitionAxiom = null; } + if (func.Body != null) + if (func.FindExprAttribute("inline") == null) + func.AddAttribute("inline", Expr.Literal(100)); } } void InlineAll() { - foreach (var d in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = d as Implementation; - if (impl != null) - { - impl.OriginalBlocks = impl.Blocks; - impl.OriginalLocVars = impl.LocVars; - if(impl.Name != main_proc_name) - if(impl.FindExprAttribute("inline") == null) - impl.AddAttribute("inline", Expr.Literal(100)); - } + impl.OriginalBlocks = impl.Blocks; + impl.OriginalLocVars = impl.LocVars; + if(impl.Name != main_proc_name) + if(impl.FindExprAttribute("inline") == null) + impl.AddAttribute("inline", Expr.Literal(100)); } - var decls = program.TopLevelDeclarations; - foreach (var d in decls) + foreach (var impl in program.Implementations) { - var impl = d as Implementation; - if (impl != null && !impl.SkipVerification) + if (!impl.SkipVerification) { Inliner.ProcessImplementation(program, impl); } } - foreach (var d in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = d as Implementation; - if (impl != null) - { - impl.OriginalBlocks = null; - impl.OriginalLocVars = null; - } + impl.OriginalBlocks = null; + impl.OriginalLocVars = null; } } @@ -650,12 +636,8 @@ namespace Microsoft.Boogie public void GenerateVCsForStratifiedInlining() { Contract.Requires(program != null); - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - Contract.Assert(decl != null); - Implementation impl = decl as Implementation; - if (impl == null) - continue; Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy"); Procedure proc = cce.NonNull(impl.Proc); @@ -713,10 +695,8 @@ namespace Microsoft.Boogie if (mode == Mode.Boogie) return; - foreach (var decl in program.TopLevelDeclarations) + foreach (var proc in program.Procedures) { - var proc = decl as Procedure; - if (proc == null) continue; if (!proc.Name.StartsWith(recordProcName)) continue; Contract.Assert(proc.InParams.Count == 1); @@ -754,12 +734,8 @@ namespace Microsoft.Boogie foreach (var node in rpfp.nodes) pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node); - foreach (Declaration decl in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - Contract.Assert(decl != null); - Implementation impl = decl as Implementation; - if (impl == null) - continue; Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy"); Procedure proc = cce.NonNull(impl.Proc); @@ -1400,25 +1376,17 @@ namespace Microsoft.Boogie // find the name of the main procedure main_proc_name = null; // default in case no entry point defined - foreach (var d in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = d as Implementation; - if (impl != null) - { - if (QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint")) - main_proc_name = impl.Proc.Name; - } + if (QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint")) + main_proc_name = impl.Proc.Name; } if (main_proc_name == null) { - foreach (var d in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = d as Implementation; - if (impl != null) - { - if (impl.Proc.Name == "main" || impl.Proc.Name.EndsWith(".main")) - main_proc_name = impl.Proc.Name; - } + if (impl.Proc.Name == "main" || impl.Proc.Name.EndsWith(".main")) + main_proc_name = impl.Proc.Name; } } if (main_proc_name == null) @@ -1428,10 +1396,9 @@ namespace Microsoft.Boogie { InlineAll(); Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program); - foreach (var d in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = d as Implementation; - if (impl != null && main_proc_name == impl.Proc.Name) + if (main_proc_name == impl.Proc.Name) { Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl); CyclicLiveVariableAnalysis.ComputeLiveVariables(impl); @@ -1444,15 +1411,11 @@ namespace Microsoft.Boogie if (style == AnnotationStyle.Procedure || style == AnnotationStyle.Call) { - foreach (var proc in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = proc as Implementation; - if (impl != null) - { - if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint")) - AnnotateProcRequires(impl.Proc, impl, boogieContext); - AnnotateProcEnsures(impl.Proc, impl, boogieContext); - } + if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint")) + AnnotateProcRequires(impl.Proc, impl, boogieContext); + AnnotateProcEnsures(impl.Proc, impl, boogieContext); } if (style == AnnotationStyle.Call) { @@ -1463,40 +1426,30 @@ namespace Microsoft.Boogie // must do this after annotating procedures, else calls // will be prematurely desugared - foreach (var d in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = d as Implementation; - if (impl != null) - { - Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl); - CyclicLiveVariableAnalysis.ComputeLiveVariables(impl); - } + Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl); + CyclicLiveVariableAnalysis.ComputeLiveVariables(impl); } if (style == AnnotationStyle.Flat || style == AnnotationStyle.Call) { - foreach (var proc in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = proc as Implementation; - if (impl != null) - AnnotateLoops(impl, boogieContext); + AnnotateLoops(impl, boogieContext); } } if (style == AnnotationStyle.Call) { Dictionary impls = new Dictionary(); - foreach (var proc in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = proc as Implementation; - if (impl != null) - impls.Add(impl.Proc.Name, true); + impls.Add(impl.Proc.Name, true); } - foreach (var proc in program.TopLevelDeclarations) + foreach (var impl in program.Implementations) { - var impl = proc as Implementation; - if (impl != null) - AnnotateCallSites(impl, boogieContext, impls); + AnnotateCallSites(impl, boogieContext, impls); } } if (style == AnnotationStyle.Flat) diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index fe40618e..5eed14fd 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -333,18 +333,14 @@ namespace VC { : base(program, logFilePath, appendLogFile, checkers) { implName2StratifiedInliningInfo = new Dictionary(); prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime); - foreach (Declaration decl in program.TopLevelDeclarations) { - Implementation impl = decl as Implementation; - if (impl == null) continue; + foreach (var impl in program.Implementations) { implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this); } GenerateRecordFunctions(); } private void GenerateRecordFunctions() { - foreach (var decl in program.TopLevelDeclarations) { - var proc = decl as Procedure; - if (proc == null) continue; + foreach (var proc in program.Procedures) { if (!proc.Name.StartsWith(recordProcName)) continue; Contract.Assert(proc.InParams.Count == 1); @@ -901,9 +897,7 @@ namespace VC { // Find all the boolean constants var allConsts = new HashSet(); - foreach (var decl in program.TopLevelDeclarations) { - var constant = decl as Constant; - if (constant == null) continue; + foreach (var constant in program.Constants) { if (!allBoolVars.Contains(constant.Name)) continue; var v = prover.Context.BoogieExprTranslator.LookupVariable(constant); allConsts.Add(v); diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 3735388c..758430bd 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2600,7 +2600,7 @@ namespace VC { // where clauses of global variables lock (program.TopLevelDeclarations) { - foreach (var gvar in program.TopLevelDeclarations.OfType()) + foreach (var gvar in program.GlobalVariables()) { if (gvar != null && gvar.TypedIdent.WhereExpr != null) { @@ -2755,15 +2755,11 @@ namespace VC { { // Construct the set of inlined procs in the original program var inlinedProcs = new HashSet(); - foreach (var decl in program.TopLevelDeclarations) + foreach (var proc in program.Procedures) { - if (decl is Procedure) - { - if (!(decl is LoopProcedure)) - { - var p = decl as Procedure; - inlinedProcs.Add(p.Name); - } + if (!(proc is LoopProcedure)) + { + inlinedProcs.Add(proc.Name); } } -- cgit v1.2.3