From 717acb3230145241f08f7d6f7cb2a68fe1f257e8 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 07:45:14 +0100 Subject: Refactored labsl2absy so that it is a Dictionary instead of a plain Hashtable. --- Source/Doomed/DoomCheck.cs | 18 +++++++++--------- Source/Doomed/DoomErrorHandler.cs | 4 ++-- 2 files changed, 11 insertions(+), 11 deletions(-) (limited to 'Source/Doomed') diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index b317dc71..6b9f91cf 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -151,7 +151,7 @@ void ObjectInvariant() } #region Attributes - public Hashtable Label2Absy; + public Dictionary Label2Absy; public DoomErrorHandler ErrorHandler { set { m_ErrHandler = value; @@ -219,9 +219,9 @@ void ObjectInvariant() } - Label2Absy = new Hashtable(); // This is only a dummy + Label2Absy = new Dictionary(); // This is only a dummy m_Evc = new Evc(check); - Hashtable l2a = null; + Dictionary l2a = null; VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount); Contract.Assert(vce != null); Contract.Assert( l2a!=null); @@ -235,9 +235,9 @@ void ObjectInvariant() { Contract.Requires(check != null); m_Check = check; - Label2Absy = new Hashtable(); // This is only a dummy + Label2Absy = new Dictionary(); // This is only a dummy m_Evc = new Evc(check); - Hashtable l2a = null; + Dictionary l2a = null; int assertionCount; // compute and then ignore VCExpr vce = this.GenerateEVC(passive_impl, out l2a, check, out assertionCount); Contract.Assert(vce != null); @@ -301,14 +301,14 @@ void ObjectInvariant() */ - VCExpr GenerateEVC(Implementation impl, out Hashtable label2absy, Checker ch, out int assertionCount) { + VCExpr GenerateEVC(Implementation impl, out Dictionary label2absy, Checker ch, out int assertionCount) { Contract.Requires(impl != null); Contract.Requires(ch != null); Contract.Ensures(Contract.Result() != null); TypecheckingContext tc = new TypecheckingContext(null); impl.Typecheck(tc); - label2absy = new Hashtable/**/(); + label2absy = new Dictionary(); VCExpr vc; switch (CommandLineOptions.Clo.vcVariety) { case CommandLineOptions.VCVariety.Doomed: @@ -322,7 +322,7 @@ void ObjectInvariant() } public VCExpr LetVC(Block startBlock, - Hashtable/**/ label2absy, + Dictionary label2absy, ProverContext proverCtxt, out int assertionCount) { @@ -342,7 +342,7 @@ void ObjectInvariant() } VCExpr LetVC(Block block, - Hashtable/**/ label2absy, + Dictionary label2absy, Hashtable/**/ blockVariables, List bindings, ProverContext proverCtxt, diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs index 33d8b68e..a85adbe1 100644 --- a/Source/Doomed/DoomErrorHandler.cs +++ b/Source/Doomed/DoomErrorHandler.cs @@ -15,7 +15,7 @@ namespace VC internal class DoomErrorHandler : ProverInterface.ErrorHandler { - protected Hashtable label2Absy; + protected Dictionary label2Absy; protected VerifierCallback callback; private List m_CurrentTrace = new List(); @@ -28,7 +28,7 @@ namespace VC } - public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback) + public DoomErrorHandler(Dictionary label2Absy, VerifierCallback callback) { Contract.Requires(label2Absy != null); Contract.Requires(callback != null); -- cgit v1.2.3 From 841c9e70b304da5863b12323f2e12cc403ac2349 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 07:53:38 +0100 Subject: Refactored variable2sequenceNumber to use Dictionary --- Source/Doomed/VCDoomed.cs | 2 +- Source/VCGeneration/ConditionGeneration.cs | 4 ++-- Source/VCGeneration/FixedpointVC.cs | 2 +- Source/VCGeneration/VC.cs | 4 ++-- 4 files changed, 6 insertions(+), 6 deletions(-) (limited to 'Source/Doomed') diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index 778ae767..413cbf5b 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -692,7 +692,7 @@ namespace VC { private void Transform4DoomedCheck(Implementation impl) { - variable2SequenceNumber = new Hashtable/*Variable -> int*/(); + variable2SequenceNumber = new Dictionary(); incarnationOriginMap = new Dictionary(); if (impl.Blocks.Count < 1) return; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index f625de75..7a738daf 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -578,7 +578,7 @@ namespace VC { protected VariableSeq CurrentLocalVariables = null; // shared across each implementation; created anew for each implementation - protected Hashtable /*Variable -> int*/ variable2SequenceNumber; + protected Dictionary variable2SequenceNumber; public Dictionary/*!>!*/ incarnationOriginMap = new Dictionary(); public Program program; @@ -1162,7 +1162,7 @@ namespace VC { int currentIncarnationNumber = variable2SequenceNumber.ContainsKey(x) ? - (int)cce.NonNull(variable2SequenceNumber[x]) + variable2SequenceNumber[x] : -1; Variable v = new Incarnation(x, currentIncarnationNumber + 1); diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index cf33c53e..7b20622a 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -126,7 +126,7 @@ namespace Microsoft.Boogie Contract.Requires(impl != null); CurrentLocalVariables = impl.LocVars; - variable2SequenceNumber = new Hashtable/*Variable -> int*/(); + variable2SequenceNumber = new Dictionary(); incarnationOriginMap = new Dictionary(); ResetPredecessors(impl.Blocks); diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index af3454f5..cfc7955b 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1228,7 +1228,7 @@ namespace VC { delegate(CodeExpr codeExpr, Hashtable/**/ blockVariables, List bindings) { VCGen vcgen = new VCGen(new Program(), null, false, parent.checkers); - vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/(); + vcgen.variable2SequenceNumber = new Dictionary(); vcgen.incarnationOriginMap = new Dictionary(); vcgen.CurrentLocalVariables = codeExpr.LocVars; // codeExpr.Blocks.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization @@ -1861,7 +1861,7 @@ namespace VC { impl.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization CurrentLocalVariables = impl.LocVars; - variable2SequenceNumber = new Hashtable/*Variable -> int*/(); + variable2SequenceNumber = new Dictionary(); incarnationOriginMap = new Dictionary(); #region Debug Tracing -- cgit v1.2.3 From 3b15454ac18f93e8f42913af80f665a900fd4378 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 08:32:54 +0100 Subject: Large refactoring of Hashtable to Dictionary. --- Source/Core/Absy.cs | 12 +++--- Source/Core/AbsyCmd.cs | 8 ++-- Source/Core/Duplicator.cs | 6 +-- Source/Core/Inline.cs | 8 ++-- Source/Core/LambdaHelper.cs | 2 +- Source/Core/OwickiGries.cs | 12 +++--- Source/Doomed/VCDoomed.cs | 10 ++--- Source/Houdini/Houdini.cs | 8 ++-- Source/VCGeneration/ConditionGeneration.cs | 60 +++++++++++++++--------------- Source/VCGeneration/FixedpointVC.cs | 2 +- Source/VCGeneration/StratifiedVC.cs | 2 +- Source/VCGeneration/VC.cs | 22 +++++------ 12 files changed, 76 insertions(+), 76 deletions(-) (limited to 'Source/Doomed') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 5e69b179..520c6730 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -385,7 +385,7 @@ namespace Microsoft.Boogie { Dictionary/*!*/ loopHeaderToInputs = new Dictionary(); Dictionary/*!*/ loopHeaderToOutputs = new Dictionary(); - Dictionary/*!*/ loopHeaderToSubstMap = new Dictionary(); + Dictionary/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary/*!*/>(); Dictionary/*!*/ loopHeaderToLoopProc = new Dictionary(); Dictionary/*!*/ loopHeaderToCallCmd1 = new Dictionary(); Dictionary loopHeaderToCallCmd2 = new Dictionary(); @@ -402,7 +402,7 @@ namespace Microsoft.Boogie { IdentifierExprSeq callOutputs2 = new IdentifierExprSeq(); List lhss = new List(); List rhss = new List(); - Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr + Dictionary substMap = new Dictionary(); // Variable -> IdentifierExpr VariableSeq/*!*/ targets = new VariableSeq(); HashSet footprint = new HashSet(); @@ -2914,17 +2914,17 @@ namespace Microsoft.Boogie { } } - private Hashtable/*Variable->Expr*//*?*/ formalMap = null; + private Dictionary/*?*/ formalMap = null; public void ResetImplFormalMap() { this.formalMap = null; } - public Hashtable /*Variable->Expr*//*!*/ GetImplFormalMap() { + public Dictionary/*!*/ GetImplFormalMap() { Contract.Ensures(Contract.Result() != null); if (this.formalMap != null) return this.formalMap; else { - Hashtable /*Variable->Expr*//*!*/ map = new Hashtable /*Variable->Expr*/ (InParams.Length + OutParams.Length); + Dictionary/*!*/ map = new Dictionary (InParams.Length + OutParams.Length); Contract.Assume(this.Proc != null); Contract.Assume(InParams.Length == Proc.InParams.Length); @@ -2948,7 +2948,7 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { Console.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name); using (TokenTextWriter stream = new TokenTextWriter("", Console.Out, false)) { - foreach (DictionaryEntry e in map) { + foreach (var e in map) { Console.Write(" "); cce.NonNull((Variable/*!*/)e.Key).Emit(stream, 0); Console.Write(" --> "); diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 3005aaa6..cf6fa9ce 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2040,9 +2040,9 @@ namespace Microsoft.Boogie { protected override Cmd ComputeDesugaring() { Contract.Ensures(Contract.Result() != null); CmdSeq newBlockBody = new CmdSeq(); - Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/(); - Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/(); - Hashtable /*Variable -> Expr*/ substMapBound = new Hashtable/*Variable -> Expr*/(); + Dictionary substMap = new Dictionary(); + Dictionary substMapOld = new Dictionary(); + Dictionary substMapBound = new Dictionary(); VariableSeq/*!*/ tempVars = new VariableSeq(); // proc P(ins) returns (outs) @@ -2335,7 +2335,7 @@ namespace Microsoft.Boogie { public class AssertCmd : PredicateCmd, IPotentialErrorNode { public Expr OrigExpr; - public Hashtable /*Variable -> Expr*/ IncarnationMap; + public Dictionary IncarnationMap; // TODO: convert to use generics private object errorData; diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index fe189f83..d8b45d09 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -353,20 +353,20 @@ namespace Microsoft.Boogie { public delegate Expr/*?*/ Substitution(Variable/*!*/ v); public static class Substituter { - public static Substitution SubstitutionFromHashtable(Hashtable/*Variable!->Expr!*/ map) { + public static Substitution SubstitutionFromHashtable(Dictionary map) { Contract.Requires(map != null); Contract.Ensures(Contract.Result() != null); // TODO: With Whidbey, could use anonymous functions. return new Substitution(new CreateSubstitutionClosure(map).Method); } private sealed class CreateSubstitutionClosure { - Hashtable/*Variable!->Expr!*//*!*/ map; + Dictionary/*!*/ map; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(map != null); } - public CreateSubstitutionClosure(Hashtable/*Variable!->Expr!*/ map) + public CreateSubstitutionClosure(Dictionary map) : base() { Contract.Requires(map != null); this.map = map; diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 57910775..b7626d99 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -328,7 +328,7 @@ namespace Microsoft.Boogie { Contract.Requires(newModifies != null); Contract.Requires(newLocalVars != null); - Hashtable substMap = new Hashtable(); + Dictionary substMap = new Dictionary(); Procedure proc = impl.Proc; foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) { @@ -365,7 +365,7 @@ namespace Microsoft.Boogie { } } - Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/(); + Dictionary substMapOld = new Dictionary(); foreach (IdentifierExpr/*!*/ mie in proc.Modifies) { Contract.Assert(mie != null); @@ -588,12 +588,12 @@ namespace Microsoft.Boogie { public Substitution Subst; public Substitution OldSubst; - public CodeCopier(Hashtable substMap) { + public CodeCopier(Dictionary substMap) { Contract.Requires(substMap != null); Subst = Substituter.SubstitutionFromHashtable(substMap); } - public CodeCopier(Hashtable substMap, Hashtable oldSubstMap) { + public CodeCopier(Dictionary substMap, Dictionary oldSubstMap) { Contract.Requires(oldSubstMap != null); Contract.Requires(substMap != null); Subst = Substituter.SubstitutionFromHashtable(substMap); diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index b3b02724..6874f1c9 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -95,7 +95,7 @@ namespace Microsoft.Boogie { Set freeVars = new Set(); lambda.ComputeFreeVariables(freeVars); // this is ugly, the output will depend on hashing order - Hashtable subst = new Hashtable(); + Dictionary subst = new Dictionary(); VariableSeq formals = new VariableSeq(); ExprSeq callArgs = new ExprSeq(); ExprSeq axCallArgs = new ExprSeq(); diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index e353700f..63f9557f 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -281,7 +281,7 @@ namespace Microsoft.Boogie int count = 0; while (callCmd != null) { - Hashtable map = new Hashtable(); + Dictionary map = new Dictionary(); foreach (Variable x in callCmd.Proc.InParams) { Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true); @@ -317,7 +317,7 @@ namespace Microsoft.Boogie return proc; } - private void CreateYieldCheckerImpl(DeclWithFormals decl, List yields, Hashtable map) + private void CreateYieldCheckerImpl(DeclWithFormals decl, List yields, Dictionary map) { if (yields.Count == 0) return; @@ -354,8 +354,8 @@ namespace Microsoft.Boogie locals.Add(copy); map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy); } - Hashtable ogOldLocalMap = new Hashtable(); - Hashtable assumeMap = new Hashtable(map); + Dictionary ogOldLocalMap = new Dictionary(); + Dictionary assumeMap = new Dictionary(map); foreach (IdentifierExpr ie in globalMods) { Variable g = ie.Decl; @@ -422,7 +422,7 @@ namespace Microsoft.Boogie Program program = linearTypechecker.program; ProcedureInfo info = procNameToInfo[impl.Name]; - Hashtable map = new Hashtable(); + Dictionary map = new Dictionary(); foreach (Variable local in impl.LocVars) { var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); @@ -717,7 +717,7 @@ namespace Microsoft.Boogie yields.Add(cmds); cmds = new CmdSeq(); } - CreateYieldCheckerImpl(proc, yields, new Hashtable()); + CreateYieldCheckerImpl(proc, yields, new Dictionary()); } private void AddYieldProcAndImpl() diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index 413cbf5b..341644ca 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -584,7 +584,7 @@ namespace VC { #region Program Passification private void GenerateHelperBlocks(Implementation impl) { Contract.Requires(impl != null); - Hashtable gotoCmdOrigins = new Hashtable(); + Dictionary gotoCmdOrigins = new Dictionary(); exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); Contract.Assert(exitBlock != null); @@ -622,7 +622,7 @@ namespace VC { } - private Hashtable/*TransferCmd->ReturnCmd*/ PassifyProgram(Implementation impl, ModelViewInfo mvInfo) { + private Dictionary PassifyProgram(Implementation impl, ModelViewInfo mvInfo) { Contract.Requires(impl != null); Contract.Requires(mvInfo != null); Contract.Requires(this.exitBlock != null); @@ -744,14 +744,14 @@ namespace VC { ResetPredecessors(impl.Blocks); //EmitImpl(impl,false); - Hashtable/*Variable->Expr*/ htbl = PassifyProgram(impl, new ModelViewInfo(program, impl)); + Dictionary var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl)); // Collect the last incarnation of each reachability variable in the passive program foreach (KeyValuePair kvp in m_BlockReachabilityMap) { - if (htbl.ContainsKey(kvp.Value)) + if (var2Expr.ContainsKey(kvp.Value)) { - m_LastReachVarIncarnation[kvp.Value] = (Expr)htbl[kvp.Value]; + m_LastReachVarIncarnation[kvp.Value] = (Expr)var2Expr[kvp.Value]; } } } diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index a91c0082..06d606ff 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -264,7 +264,7 @@ namespace Microsoft.Boogie.Houdini { return newCmdSeq; } private CmdSeq InlineRequiresForCallCmd(CallCmd node) { - Hashtable substMap = new Hashtable(); + Dictionary substMap = new Dictionary(); for (int i = 0; i < node.Proc.InParams.Length; i++) { substMap.Add(node.Proc.InParams[i], node.Ins[i]); } @@ -1149,7 +1149,7 @@ namespace Microsoft.Boogie.Houdini { if (assertCmd != null && MatchCandidate(assertCmd.Expr, out c)) { var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0]; if (currentHoudiniState.Assignment[cVar]) { - Hashtable cToTrue = new Hashtable(); + Dictionary cToTrue = new Dictionary(); Variable cVarProg = prog.TopLevelDeclarations.OfType().Where(item => item.Name.Equals(c)).ToList()[0]; cToTrue[cVarProg] = Expr.True; newCmds.Add(new AssumeCmd(assertCmd.tok, @@ -1172,7 +1172,7 @@ namespace Microsoft.Boogie.Houdini { 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]; - Hashtable subst = new Hashtable(); + Dictionary subst = new Dictionary(); subst[cVarProg] = Expr.True; newRequires.Add(new Requires(Token.NoToken, true, Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), r.Condition), @@ -1192,7 +1192,7 @@ namespace Microsoft.Boogie.Houdini { 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]; - Hashtable subst = new Hashtable(); + Dictionary subst = new Dictionary(); subst[cVarProg] = Expr.True; newEnsures.Add(new Ensures(Token.NoToken, true, Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), e.Condition), diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 7a738daf..edab3bf8 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -257,7 +257,7 @@ namespace Microsoft.Boogie { var s = states[i]; if (0 <= s && s < MvInfo.CapturePoints.Count) { VC.ModelViewInfo.Mapping map = MvInfo.CapturePoints[s]; - var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Hashtable(); + var prevInc = i > 0 ? MvInfo.CapturePoints[states[i - 1]].IncarnationMap : new Dictionary(); var cs = m.MkState(map.Description); foreach (Variable v in MvInfo.AllVariables) { @@ -756,7 +756,7 @@ namespace VC { /// already been constructed for the implementation (and so /// is already an element of impl.Blocks) /// - protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins) { + protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary gotoCmdOrigins) { Contract.Requires(impl != null); Contract.Requires(unifiedExitBlock != null); Contract.Requires(gotoCmdOrigins != null); @@ -1085,7 +1085,7 @@ namespace VC { } - protected Block GenerateUnifiedExit(Implementation impl, Hashtable gotoCmdOrigins) { + protected Block GenerateUnifiedExit(Implementation impl, Dictionary gotoCmdOrigins) { Contract.Requires(impl != null); Contract.Requires(gotoCmdOrigins != null); Contract.Ensures(Contract.Result() != null); @@ -1112,7 +1112,7 @@ namespace VC { BlockSeq bs = new BlockSeq(); bs.Add(unifiedExit); GotoCmd go = new GotoCmd(Token.NoToken, labels, bs); - gotoCmdOrigins[go] = b.TransferCmd; + gotoCmdOrigins[go] = (ReturnCmd)b.TransferCmd; b.TransferCmd = go; unifiedExit.Predecessors.Add(b); } @@ -1187,31 +1187,31 @@ namespace VC { /// /// Gives incarnation maps for b's predecessors. /// - protected Hashtable /*Variable -> Expr*/ ComputeIncarnationMap(Block b, Hashtable /*Variable -> Expr*/ block2Incarnation) { + protected Dictionary ComputeIncarnationMap(Block b, Dictionary> block2Incarnation) { Contract.Requires(b != null); Contract.Requires(block2Incarnation != null); Contract.Ensures(Contract.Result() != null); if (b.Predecessors.Length == 0) { - return new Hashtable(); + return new Dictionary(); } - Hashtable /*Variable -> Expr*/ incarnationMap = null; + Dictionary incarnationMap = null; Set /*Variable*/ fixUps = new Set /*Variable*/ (); foreach (Block pred in b.Predecessors) { Contract.Assert(pred != null); - Contract.Assert(block2Incarnation.Contains(pred)); // otherwise, Passive Transformation found a block whose predecessors have not been processed yet - Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)block2Incarnation[pred]; + Contract.Assert(block2Incarnation.ContainsKey(pred)); // otherwise, Passive Transformation found a block whose predecessors have not been processed yet + Dictionary predMap = (Dictionary)block2Incarnation[pred]; Contract.Assert(predMap != null); if (incarnationMap == null) { - incarnationMap = (Hashtable /*Variable -> Expr*/)predMap.Clone(); + incarnationMap = new Dictionary(predMap); continue; } ArrayList /*Variable*/ conflicts = new ArrayList /*Variable*/ (); foreach (Variable v in incarnationMap.Keys) { Contract.Assert(v != null); - if (!predMap.Contains(v)) { + if (!predMap.ContainsKey(v)) { // conflict!! conflicts.Add(v); fixUps.Add(v); @@ -1224,7 +1224,7 @@ namespace VC { } foreach (Variable v in predMap.Keys) { Contract.Assert(v != null); - if (!incarnationMap.Contains(v)) { + if (!incarnationMap.ContainsKey(v)) { // v was not in the domain of the predecessors seen so far, so it needs to be fixed up fixUps.Add(v); } else { @@ -1251,7 +1251,7 @@ namespace VC { Contract.Assert(pred != null); #region Create an assume command equating v_prime with its last incarnation in pred #region Create an identifier expression for the last incarnation in pred - Hashtable /*Variable -> Expr*/ predMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(block2Incarnation[pred]); + Dictionary predMap = (Dictionary)cce.NonNull(block2Incarnation[pred]); Expr pred_incarnation_exp; Expr o = (Expr)predMap[v]; @@ -1279,9 +1279,9 @@ namespace VC { return incarnationMap; } - Hashtable preHavocIncarnationMap = null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement + Dictionary preHavocIncarnationMap = null; // null = the previous command was not an HashCmd. Otherwise, a *copy* of the map before the havoc statement - protected void TurnIntoPassiveBlock(Block b, Hashtable /*Variable -> Expr*/ incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) { + protected void TurnIntoPassiveBlock(Block b, Dictionary incarnationMap, ModelViewInfo mvInfo, Substitution oldFrameSubst) { Contract.Requires(b != null); Contract.Requires(incarnationMap != null); Contract.Requires(mvInfo != null); @@ -1304,11 +1304,11 @@ namespace VC { #endregion } - protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) { + protected Dictionary Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) { Contract.Requires(impl != null); Contract.Requires(mvInfo != null); - Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo); + Dictionary r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo); RestoreParamWhereClauses(impl); @@ -1322,7 +1322,7 @@ namespace VC { return r; } - protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) { + protected Dictionary ConvertBlocks2PassiveCmd(List blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) { Contract.Requires(blocks != null); Contract.Requires(modifies != null); Contract.Requires(mvInfo != null); @@ -1349,13 +1349,13 @@ namespace VC { // Now we can process the nodes in an order so that we're guaranteed to have // processed all of a node's predecessors before we process the node. - Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/(); + Dictionary> block2Incarnation = new Dictionary>(); Block exitBlock = null; - Hashtable exitIncarnationMap = null; + Dictionary exitIncarnationMap = null; foreach (Block b in sortedNodes) { Contract.Assert(b != null); - Contract.Assert(!block2Incarnation.Contains(b)); - Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation); + Contract.Assert(!block2Incarnation.ContainsKey(b)); + Dictionary incarnationMap = ComputeIncarnationMap(b, block2Incarnation); // b.liveVarsBefore has served its purpose in the just-finished call to ComputeIncarnationMap; null it out. b.liveVarsBefore = null; @@ -1398,11 +1398,11 @@ namespace VC { /// protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies) { - Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable(); + Dictionary oldFrameMap = new Dictionary(); foreach (IdentifierExpr ie in modifies) { Contract.Assert(ie != null); - if (!oldFrameMap.Contains(cce.NonNull(ie.Decl))) + if (!oldFrameMap.ContainsKey(cce.NonNull(ie.Decl))) oldFrameMap.Add(ie.Decl, ie); } return Substituter.SubstitutionFromHashtable(oldFrameMap); @@ -1412,7 +1412,7 @@ namespace VC { /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc /// Meanwhile, record any information needed to later reconstruct a model view. /// - protected void TurnIntoPassiveCmd(Cmd c, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) { + protected void TurnIntoPassiveCmd(Cmd c, Dictionary incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) { Contract.Requires(c != null); Contract.Requires(incarnationMap != null); Contract.Requires(oldFrameSubst != null); @@ -1432,14 +1432,14 @@ namespace VC { if (description != null) { Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count))); copy = Bpl.Expr.And(mv, copy); - mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, (Hashtable)incarnationMap.Clone())); + mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, new Dictionary(incarnationMap))); } } Contract.Assert(copy != null); if (pc is AssertCmd) { ((AssertCmd)pc).OrigExpr = pc.Expr; Contract.Assert(((AssertCmd)pc).IncarnationMap == null); - ((AssertCmd)pc).IncarnationMap = (Hashtable /*Variable -> Expr*/)cce.NonNull(incarnationMap.Clone()); + ((AssertCmd)pc).IncarnationMap = (Dictionary)cce.NonNull(new Dictionary(incarnationMap)); } pc.Expr = copy; passiveCmds.Add(pc); @@ -1518,7 +1518,7 @@ namespace VC { #region havoc w |--> assume whereClauses, out := in( w |-> w' ) else if (c is HavocCmd) { if (this.preHavocIncarnationMap == null) // Save a copy of the incarnation map (at the top of a sequence of havoc statements) - this.preHavocIncarnationMap = (Hashtable)incarnationMap.Clone(); + this.preHavocIncarnationMap = new Dictionary(incarnationMap); HavocCmd hc = (HavocCmd)c; Contract.Assert(c != null); @@ -1748,8 +1748,8 @@ namespace VC { public class Mapping { public readonly string Description; - public readonly Hashtable /*Variable -> Expr*/ IncarnationMap; - public Mapping(string description, Hashtable /*Variable -> Expr*/ incarnationMap) { + public readonly Dictionary IncarnationMap; + public Mapping(string description, Dictionary incarnationMap) { Description = description; IncarnationMap = incarnationMap; } diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 7b20622a..78ed8cb5 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -1871,7 +1871,7 @@ namespace Microsoft.Boogie Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count); VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint]; var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate) - ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable(); + ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary(); var cs = m.MkState(map.Description); foreach (Variable v in info.AllVariables) diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 4078b43e..01b34504 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2472,7 +2472,7 @@ namespace VC { Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count); VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint]; var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate) - ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable(); + ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Dictionary(); var cs = m.MkState(map.Description); foreach (Variable v in info.AllVariables) { diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index bc83e529..bf2bf324 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -531,7 +531,7 @@ namespace VC { double total_cost; int assertion_count; double assertion_cost; // without multiplication by paths - Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins; + Dictionary/*!*/ gotoCmdOrigins; readonly public VCGen/*!*/ parent; Implementation/*!*/ impl; @@ -548,7 +548,7 @@ namespace VC { private int splitNo; internal ErrorReporter reporter; - public Split(List/*!*/ blocks, Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) { + public Split(List/*!*/ blocks, Dictionary/*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) { Contract.Requires(cce.NonNullElements(blocks)); Contract.Requires(gotoCmdOrigins != null); Contract.Requires(par != null); @@ -974,13 +974,13 @@ namespace VC { copies.Clear(); CloneBlock(blocks[0]); List newBlocks = new List(); - Hashtable newGotoCmdOrigins = new Hashtable(); + Dictionary newGotoCmdOrigins = new Dictionary(); foreach (Block b in blocks) { Contract.Assert(b != null); Block tmp; if (copies.TryGetValue(b, out tmp)) { newBlocks.Add(cce.NonNull(tmp)); - if (gotoCmdOrigins.ContainsKey(b)) { + if (gotoCmdOrigins.ContainsKey(b.TransferCmd)) { newGotoCmdOrigins[tmp.TransferCmd] = gotoCmdOrigins[b.TransferCmd]; } @@ -1235,7 +1235,7 @@ namespace VC { ResetPredecessors(codeExpr.Blocks); vcgen.AddBlocksBetween(codeExpr.Blocks); - Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr)); + Dictionary gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr)); int ac; // computed, but then ignored for this CodeExpr VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac); VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect); @@ -1653,7 +1653,7 @@ namespace VC { } public class ErrorReporter : ProverInterface.ErrorHandler { - Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins; + Dictionary/*!*/ gotoCmdOrigins; Dictionary/*!*/ label2absy; List/*!*/ blocks; protected Dictionary/*!*/ incarnationOriginMap; @@ -1686,7 +1686,7 @@ namespace VC { protected ProverContext/*!*/ context; Program/*!*/ program; - public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, + public ErrorReporter(Dictionary/*!*/ gotoCmdOrigins, Dictionary/*!*/ label2absy, List/*!*/ blocks, Dictionary/*!*/ incarnationOriginMap, @@ -1782,7 +1782,7 @@ namespace VC { } public class ErrorReporterLocal : ErrorReporter { - public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, + public ErrorReporterLocal(Dictionary/*!*/ gotoCmdOrigins, Dictionary/*!*/ label2absy, List/*!*/ blocks, Dictionary/*!*/ incarnationOriginMap, @@ -2097,13 +2097,13 @@ namespace VC { } } - public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo) + public Dictionary PassifyImpl(Implementation impl, out ModelViewInfo mvInfo) { Contract.Requires(impl != null); Contract.Requires(program != null); Contract.Ensures(Contract.Result() != null); - Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/(); + Dictionary gotoCmdOrigins = new Dictionary(); Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins); #region Debug Tracing @@ -2216,7 +2216,7 @@ namespace VC { cmds.AddRange(entryBlock.Cmds); entryBlock.Cmds = cmds; // Make sure that all added commands are passive commands. - Hashtable incarnationMap = ComputeIncarnationMap(entryBlock, new Hashtable()); + Dictionary incarnationMap = ComputeIncarnationMap(entryBlock, new Dictionary>()); TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo, ComputeOldExpressionSubstitution(impl.Proc.Modifies)); } -- cgit v1.2.3