From 3e33bdafb4d882a435f948defaf2c337e06d5191 Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Thu, 10 Mar 2011 22:38:47 +0000 Subject: Replaced all dictionaries that mapped to bool (i.e., were being used to implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null. --- Source/VCGeneration/VC.cs | 74 +++++++++++++++++++++++------------------------ 1 file changed, 37 insertions(+), 37 deletions(-) (limited to 'Source/VCGeneration/VC.cs') diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 1062767c..8a9e13ff 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -284,7 +284,7 @@ namespace VC { Contract.Invariant(initial != null); Contract.Invariant(program != null); Contract.Invariant(cce.NonNullDictionaryAndValues(copies)); - Contract.Invariant(visited != null); + Contract.Invariant(cce.NonNull(visited)); Contract.Invariant(callback != null); } @@ -294,7 +294,7 @@ namespace VC { Program program; int id; Dictionary copies = new Dictionary(); - Dictionary visited = new Dictionary(); + HashSet visited = new HashSet(); VerifierCallback callback; internal SmokeTester(VCGen par, Implementation i, Program prog, VerifierCallback callback) { @@ -548,9 +548,9 @@ namespace VC { void DFS(Block cur) { Contract.Requires(cur != null); Contract.EnsuresOnThrow(true); - if (visited.ContainsKey(cur)) + if (visited.Contains(cur)) return; - visited[cur] = true; + visited.Add(cur); CmdSeq seq = new CmdSeq(); foreach (Cmd cmd_ in cur.Cmds) { @@ -668,13 +668,13 @@ namespace VC { public double incomming_paths; public List/*!>!*/ virtual_successors = new List(); public List/*!>!*/ virtual_predecesors = new List(); - public Dictionary reachable_blocks; + public HashSet reachable_blocks; public readonly Block block; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(virtual_successors)); Contract.Invariant(cce.NonNullElements(virtual_predecesors)); - Contract.Invariant(cce.NonNullElements(reachable_blocks.Keys)); + Contract.Invariant(cce.NonNull(reachable_blocks)); Contract.Invariant(block != null); } @@ -696,8 +696,8 @@ namespace VC { Contract.Invariant(parent != null); Contract.Invariant(impl != null); Contract.Invariant(copies != null); - Contract.Invariant(protected_from_assert_to_assume != null); - Contract.Invariant(keep_at_all != null); + Contract.Invariant(cce.NonNull(protected_from_assert_to_assume)); + Contract.Invariant(cce.NonNull(keep_at_all)); } @@ -724,8 +724,8 @@ namespace VC { double slice_initial_limit; double slice_limit; bool slice_pos; - Dictionary/*!*/ protected_from_assert_to_assume = new Dictionary(); - Dictionary/*!*/ keep_at_all = new Dictionary(); + HashSet/*!*/ protected_from_assert_to_assume = new HashSet(); + HashSet/*!*/ keep_at_all = new HashSet(); // async interface private Checker checker; @@ -861,21 +861,21 @@ namespace VC { } } - Dictionary/*!*/ ComputeReachableNodes(Block/*!*/ b) { + HashSet/*!*/ ComputeReachableNodes(Block/*!*/ b) { Contract.Requires(b != null); - Contract.Ensures(Contract.Result>() != null); + Contract.Ensures(cce.NonNull(Contract.Result>())); BlockStats s = GetBlockStats(b); if (s.reachable_blocks != null) { return s.reachable_blocks; } - Dictionary blocks = new Dictionary(); + HashSet blocks = new HashSet(); s.reachable_blocks = blocks; - blocks[b] = true; + blocks.Add(b); foreach (Block/*!*/ succ in Exits(b)) { Contract.Assert(succ != null); - foreach (Block r in ComputeReachableNodes(succ).Keys) { + foreach (Block r in ComputeReachableNodes(succ)) { Contract.Assert(r != null); - blocks[r] = true; + blocks.Add(r); } } return blocks; @@ -979,7 +979,7 @@ namespace VC { if (s.incomming_paths < 0.0) { int count = 0; s.incomming_paths = 0.0; - if (!keep_at_all.ContainsKey(s.block)) + if (!keep_at_all.Contains(s.block)) return; foreach (Block b in s.virtual_predecesors) { Contract.Assert(b != null); @@ -999,9 +999,9 @@ namespace VC { void ComputeBlockSetsHelper(Block b, bool allow_small) { Contract.Requires(b != null); - if (keep_at_all.ContainsKey(b)) + if (keep_at_all.Contains(b)) return; - keep_at_all[b] = true; + keep_at_all.Add(b); if (allow_small) { foreach (Block ch in Exits(b)) { @@ -1030,18 +1030,18 @@ namespace VC { if (assert_to_assume) { foreach (Block b in allow_small ? blocks : big_blocks) { Contract.Assert(b != null); - if (ComputeReachableNodes(b).ContainsKey(cce.NonNull(split_block))) { - keep_at_all[b] = true; + if (ComputeReachableNodes(b).Contains(cce.NonNull(split_block))) { + keep_at_all.Add(b); } } foreach (Block b in assumized_branches) { Contract.Assert(b != null); - foreach (Block r in ComputeReachableNodes(b).Keys) { + foreach (Block r in ComputeReachableNodes(b)) { Contract.Assert(r != null); if (allow_small || GetBlockStats(r).big_block) { - keep_at_all[r] = true; - protected_from_assert_to_assume[r] = true; + keep_at_all.Add(r); + protected_from_assert_to_assume.Add(r); } } } @@ -1052,7 +1052,7 @@ namespace VC { bool ShouldAssumize(Block b) { Contract.Requires(b != null); - return assert_to_assume && !protected_from_assert_to_assume.ContainsKey(b); + return assert_to_assume && !protected_from_assert_to_assume.Contains(b); } double DoComputeScore(bool aa) { @@ -1069,7 +1069,7 @@ namespace VC { double cost = 0.0; foreach (Block b in big_blocks) { Contract.Assert(b != null); - if (keep_at_all.ContainsKey(b)) { + if (keep_at_all.Contains(b)) { BlockStats s = GetBlockStats(b); UpdateIncommingPaths(s); double local = s.assertion_cost; @@ -1140,10 +1140,10 @@ namespace VC { foreach (Block ch in cce.NonNull(gt.labelTargets)) { Contract.Assert(ch != null); Contract.Assert(doing_slice || - (assert_to_assume || (keep_at_all.ContainsKey(ch) || assumized_branches.Contains(ch)))); + (assert_to_assume || (keep_at_all.Contains(ch) || assumized_branches.Contains(ch)))); if (doing_slice || ((b != split_block || assumized_branches.Contains(ch) == assert_to_assume) && - keep_at_all.ContainsKey(ch))) { + keep_at_all.Contains(ch))) { newGoto.AddTarget(CloneBlock(ch)); } pos++; @@ -1304,7 +1304,7 @@ namespace VC { ss.Add(s0.blocks[0]); ss.Add(s1.blocks[0]); try { - best.SoundnessCheck(new Dictionary(), best.blocks[0], ss); + best.SoundnessCheck(new HashSet(), best.blocks[0], ss); } catch (System.Exception e) { Console.WriteLine(e); best.DumpDot(-1); @@ -1461,8 +1461,8 @@ namespace VC { checker.BeginCheck(desc, vc, reporter); } - private void SoundnessCheck(Dictionary/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { - Contract.Requires(cache != null); + private void SoundnessCheck(HashSet/*!*/ cache, Block/*!*/ orig, List/*!*/ copies) { + Contract.Requires(cce.NonNull(cache)); Contract.Requires(orig != null); Contract.Requires(copies != null); { @@ -1473,10 +1473,10 @@ namespace VC { Contract.Assert(b != null); t[i++] = b; } - if (cache.ContainsKey(t)) { + if (cache.Contains(t)) { return; } - cache[t] = true; + cache.Add(t); } for (int i = 0; i < orig.Cmds.Length; ++i) { @@ -3997,7 +3997,7 @@ namespace VC { // recursively call this method on each successor // merge result into a *set* of blocks - Dictionary mergedSuccessors = new Dictionary(); + HashSet mergedSuccessors = new HashSet(); int m = 0; // in the following loop, set renameInfoForStartBlock to the value that all recursive calls agree on, if possible; otherwise, null foreach (Block dest in gtc.labelTargets){Contract.Assert(dest != null); Block renameInfo; @@ -4009,15 +4009,15 @@ namespace VC { renameInfoForStartBlock = null; } foreach (Block successor in ys){ - if (!mergedSuccessors.ContainsKey(successor)) - mergedSuccessors.Add(successor,true); + if (!mergedSuccessors.Contains(successor)) + mergedSuccessors.Add(successor); } m++; } b.TraversingStatus = Block.VisitState.AlreadyVisited; BlockSeq setOfSuccessors = new BlockSeq(); - foreach (Block d in mergedSuccessors.Keys) + foreach (Block d in mergedSuccessors) setOfSuccessors.Add(d); if (b.Cmds.Length == 0 && !startNode) { // b is about to become extinct -- cgit v1.2.3