diff options
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<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
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<string, HashSet<Variable>> domainNameToInputScope = new Dictionary<string, HashSet<Variable>>();
Dictionary<string, HashSet<Variable>> domainNameToOutputScope = new Dictionary<string, HashSet<Variable>>();
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<Block> 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<Declaration/*!*/>();
- 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<TypeCtorDecl>()) {
+ if (!QKeyValue.FindBoolAttribute(d.Attributes, "ignore"))
d.Resolve(rc);
}
// collect type synonym declarations
List<TypeSynonymDecl/*!*/>/*!*/ synonymDecls = new List<TypeSynonymDecl/*!*/>();
- foreach (Declaration d in TopLevelDeclarations) {
+ foreach (var d in TopLevelDeclarations.OfType<TypeSynonymDecl>()) {
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<Implementation> Implementations()
+ public IEnumerable<Implementation> Implementations
+ {
+ get
+ {
+ return TopLevelDeclarations.OfType<Implementation>();
+ }
+ }
+
+ public IEnumerable<Axiom> Axioms
+ {
+ get
+ {
+ return TopLevelDeclarations.OfType<Axiom>();
+ }
+ }
+
+ public IEnumerable<Procedure> Procedures
+ {
+ get
+ {
+ return TopLevelDeclarations.OfType<Procedure>();
+ }
+ }
+
+ public IEnumerable<Function> Functions
+ {
+ get
+ {
+ return TopLevelDeclarations.OfType<Function>();
+ }
+ }
+
+ public IEnumerable<Variable> Variables
+ {
+ get
+ {
+ return TopLevelDeclarations.OfType<Variable>();
+ }
+ }
+
+ public IEnumerable<Constant> Constants
{
- return TopLevelDeclarations.OfType<Implementation>();
+ get
+ {
+ return TopLevelDeclarations.OfType<Constant>();
+ }
}
public IEnumerable<Block> 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
/// </summary>
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<Implementation> BuildCallGraph(Program program) {
Graph<Implementation> callGraph = new Graph<Implementation>();
Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
- 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<Implementation>();
}
- 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<string>();
List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();
Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
- 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<GlobalVariable/*!*/> globals = null;
- public List<GlobalVariable/*!*/>/*!*/ GlobalVariables() {
+ public IEnumerable<GlobalVariable/*!*/>/*!*/ GlobalVariables() {
Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>()));
if (globals != null)
return globals;
globals = new List<GlobalVariable/*!*/>();
- foreach (Declaration d in TopLevelDeclarations) {
- GlobalVariable gvar = d as GlobalVariable;
- if (gvar != null)
- globals.Add(gvar);
+ foreach (var gvar in TopLevelDeclarations.OfType<GlobalVariable>()) {
+ 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<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();
- 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<Variable>());
+ Contract.Assert(expr != null);
+ ProcessVariable(expr.Decl);
}
+ enclosingProc = null;
+ }
+ else
+ {
+ modSets.Add(proc, new HashSet<Variable>());
}
}
@@ -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<GlobalVariable/*!*/>/*!*/ 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<Function>().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<Block> OriginalProgramBlocks()
{
- return prog.TopLevelDeclarations.OfType<Implementation>().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<Procedure>())
+ 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<Implementation>())
+ foreach (var impl in prog.Implementations)
{
string exitLabel = "__" + impl.Name + "_newExit";
Block newExit = new Block(Token.NoToken, exitLabel, new List<Cmd>(), new GotoCmd(Token.NoToken, new List<Block>()));
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<Variable>().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<Procedure> NonInlinedProcedures() {
- return prog.TopLevelDeclarations.OfType<Procedure>().
+ return prog.Procedures.
Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);
}
private IEnumerable<Implementation> NonInlinedImplementations() {
- return prog.TopLevelDeclarations.OfType<Implementation>().
+ return prog.Implementations.
Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1);
}
@@ -439,7 +439,7 @@ namespace Microsoft.Boogie { Dictionary<Implementation, Dictionary<Block, HashSet<Block>>> LocalCtrlDeps = new Dictionary<Implementation, Dictionary<Block, HashSet<Block>>>();
// Work out and union together local control dependences
- foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+ foreach (var Impl in prog.Implementations) {
Graph<Block> blockGraph = prog.ProcessLoops(Impl);
LocalCtrlDeps[Impl] = blockGraph.ControlDependence();
foreach (var KeyValue in LocalCtrlDeps[Impl]) {
@@ -450,7 +450,7 @@ namespace Microsoft.Boogie { Graph<Implementation> callGraph = Program.BuildCallGraph(prog);
// Add inter-procedural control dependence nodes based on calls
- foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+ foreach (var Impl in prog.Implementations) {
foreach (var b in Impl.Blocks) {
foreach (var cmd in b.Cmds.OfType<CallCmd>()) {
var DirectCallee = GetImplementation(cmd.callee);
@@ -513,7 +513,7 @@ namespace Microsoft.Boogie { }
private Implementation GetImplementation(string proc) {
- foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+ 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<Cmd> cc = new List<Cmd>();
// 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<Implementation>())
+ 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<Implementation>().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<Axiom>());
+ 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<string>();
- 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<Procedure>().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<Function>();
+ 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<string, NAryExpr>();
// Find the existential functions
- foreach (var func in program.TopLevelDeclarations.OfType<Function>()
+ 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<Implementation>()
+ program.Implementations
.Where(impl => !impl.SkipVerification)
.Iter(impl => name2Impl.Add(impl.Name, impl));
@@ -753,23 +753,19 @@ namespace Microsoft.Boogie.Houdini { {
Graph<Implementation> callGraph = new Graph<Implementation>();
Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
- 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<Implementation>();
}
- 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<Function>()
- .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<Implementation>()
+ 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<Implementation>()));
name2Impl.Values.Iter(impl => Pred.Add(impl, new HashSet<Implementation>()));
- foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+ foreach (var impl in program.Implementations)
{
foreach (var blk in impl.Blocks)
{
@@ -2276,7 +2270,7 @@ namespace Microsoft.Boogie.Houdini { var copy = new Dictionary<string, Implementation>();
if (WitnessFile != null)
{
- foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+ foreach (var impl in program.Implementations)
{
var nimpl = new Implementation(Token.NoToken, impl.Name, impl.TypeParameters,
impl.InParams, impl.OutParams, new List<Variable>(impl.LocVars), new List<Block>());
@@ -2365,7 +2359,7 @@ namespace Microsoft.Boogie.Houdini { return Expr.True;
var vars = new Dictionary<string, Expr>();
- foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+ foreach (var g in program.GlobalVariables())
vars.Add(g.Name, Expr.Ident(g));
foreach (var v in proc.InParams.OfType<Variable>())
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<Procedure>())
+ foreach (var proc in program.Procedures)
{
var nensures = new List<Ensures>();
proc.Ensures.OfType<Ensures>()
@@ -2411,7 +2405,7 @@ namespace Microsoft.Boogie.Houdini { .Iter(decl => decls.Add(decl));
program.TopLevelDeclarations = decls;
var name2Proc = new Dictionary<string, Procedure>();
- foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())
+ 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<Implementation>())
+ foreach (var impl in program.Implementations)
{
foreach (var blk in impl.Blocks)
{
@@ -2448,7 +2442,7 @@ namespace Microsoft.Boogie.Houdini { var forold = new Dictionary<string, Expr>();
var always = new Dictionary<string, Expr>();
int i = 0;
- foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+ 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<Implementation> callGraph = new Graph<Implementation>();
Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
- 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<Implementation>();
}
- 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<string, VCExpr>();
var cnt = 0;
- foreach (var g in program.TopLevelDeclarations.OfType<GlobalVariable>())
+ 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<GlobalVariable>())
+ 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<Constant>())
+ 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<GlobalVariable>())
+ 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<GlobalVariable>())
+ 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<Constant>())
+ foreach (var c in program.Constants)
{
try
{
@@ -3231,7 +3221,7 @@ namespace Microsoft.Boogie.Houdini { boolConstants = new HashSet<string>();
UpperCandidates = new Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>>();
- program.TopLevelDeclarations.OfType<Constant>()
+ 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<int>();
var tempP = new HashSet<Procedure>();
foreach (var proc in
- program.TopLevelDeclarations.OfType<Procedure>()
+ 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<string, List<Expr>>();
- foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
+ foreach (var impl in program.Implementations)
{
PrePreds.Add(impl.Name, new List<NamedExpr>());
PostPreds.Add(impl.Name, new List<NamedExpr>());
@@ -3876,7 +3866,7 @@ namespace Microsoft.Boogie.Houdini { Simplify();
// Find the free expressions
- var proc = program.TopLevelDeclarations.OfType<Procedure>().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<Requires>().Where(req => req.Free))
@@ -4598,13 +4588,9 @@ namespace Microsoft.Boogie.Houdini { public static Dictionary<string, Implementation> nameImplMapping(Program p)
{
var m = new Dictionary<string, Implementation>();
- 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<CandidateInstance> CandidateInstances()
{
- foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>())
+ 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<Procedure>())
+ foreach (var proc in prog.Procedures)
{
foreach (Requires r in proc.Requires)
{
@@ -351,7 +351,7 @@ namespace Microsoft.Boogie.Houdini { }
private IEnumerable<string> GetCandidates() {
- return prog.TopLevelDeclarations.OfType<Variable>().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<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item))
+ foreach (var b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item))
{
List<Cmd> newCmds = new List<Cmd>();
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<Procedure>())
+ foreach (var p in prog.Procedures)
{
#region Handle the preconditions
@@ -633,7 +633,7 @@ namespace Microsoft.Boogie.Houdini { this.candidateToOccurences = new Dictionary<string,HashSet<object>>();
// Add all candidate occurrences in blocks
- foreach(Block b in prog.TopLevelDeclarations.OfType<Implementation>().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<Procedure>()) {
+ 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<Procedure>()) {
+ 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<Implementation>()) { + 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<Procedure>()) { + 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<Variable> CollectExistentialConstants() {
HashSet<Variable> existentialConstants = new HashSet<Variable>();
- 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<Constant>()) {
+ 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<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)
{
Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);
- foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
+ 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<Implementation>().Select(item => item.Blocks).SelectMany(item => item)) {
+ foreach (Block block in prog.Implementations.Select(item => item.Blocks).SelectMany(item => item)) {
List<Cmd> newCmds = new List<Cmd>();
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<Variable, Expr> cToTrue = new Dictionary<Variable, Expr>();
- Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().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<Procedure>()) {
+ foreach (var proc in prog.Procedures) {
List<Requires> newRequires = new List<Requires>();
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<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];
+ Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];
Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
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<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];
+ Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];
Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
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<Implementation>();
+ var impls = prog.Implementations;
foreach (var Impl in impls)
{
@@ -143,7 +143,7 @@ namespace Microsoft.Boogie ProcedureChanged = true;
}
- var procs = prog.TopLevelDeclarations.OfType<Procedure>();
+ 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<Variable>())
+ 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<string, bool> impls = new Dictionary<string, bool>();
- 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<string, StratifiedInliningInfo>();
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<VCExprVar>();
- 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<GlobalVariable>())
+ 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<string>();
- 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);
}
}
|