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/Houdini/AbstractHoudini.cs | 80 +++++++++++---------------- Source/Houdini/CandidateDependenceAnalyser.cs | 16 +++--- Source/Houdini/ConcurrentHoudini.cs | 4 +- Source/Houdini/Houdini.cs | 27 ++++----- 4 files changed, 55 insertions(+), 72 deletions(-) (limited to 'Source/Houdini') 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, -- cgit v1.2.3