diff options
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/Absy.cs | 108 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.cs | 40 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 2 | ||||
| -rw-r--r-- | Source/Core/Inline.cs | 7 | ||||
| -rw-r--r-- | Source/Core/InterProceduralReachabilityGraph.cs | 6 | ||||
| -rw-r--r-- | Source/Core/VariableDependenceAnalyser.cs | 12 |
6 files changed, 99 insertions, 76 deletions
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;
}
|