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 ++-- Source/Houdini/AbstractHoudini.cs | 4 ++-- Source/Houdini/Checker.cs | 2 +- Source/VCGeneration/FixedpointVC.cs | 6 +++--- Source/VCGeneration/StratifiedVC.cs | 16 ++++++++-------- Source/VCGeneration/VC.cs | 34 +++++++++++++++++----------------- Source/VCGeneration/Wlp.cs | 6 +++--- 8 files changed, 45 insertions(+), 45 deletions(-) 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); diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 24a3c708..157571f3 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -565,7 +565,7 @@ namespace Microsoft.Boogie.Houdini { private void GenVC(Implementation impl) { ModelViewInfo mvInfo; - System.Collections.Hashtable label2absy; + Dictionary label2absy; var collector = new AbsHoudiniCounterexampleCollector(this); collector.OnProgress("HdnVCGen", 0, 0, 0.0); @@ -2792,7 +2792,7 @@ namespace Microsoft.Boogie.Houdini { private void GenVC(Implementation impl) { ModelViewInfo mvInfo; - System.Collections.Hashtable label2absy; + Dictionary label2absy; if (CommandLineOptions.Clo.Trace) { diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index b29aa933..ce46f20b 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -155,7 +155,7 @@ namespace Microsoft.Boogie.Houdini { var exprGen = proverInterface.Context.ExprGen; VCExpr controlFlowVariableExpr = CommandLineOptions.Clo.UseLabels ? null : exprGen.Integer(BigNum.ZERO); - Hashtable/**/ label2absy; + Dictionary label2absy; conjecture = vcgen.GenerateVC(impl, controlFlowVariableExpr, out label2absy, proverInterface.Context); if (!CommandLineOptions.Clo.UseLabels) { VCExpr controlFlowFunctionAppl = exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 3299ef76..cf33c53e 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -395,7 +395,7 @@ namespace Microsoft.Boogie public Dictionary incarnationOriginMap; public Hashtable /*Variable->Expr*/ exitIncarnationMap; public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins; - public Hashtable/**/ label2absy; + public Dictionary label2absy; public VC.ModelViewInfo mvInfo; public Dictionary reachVars; @@ -514,7 +514,7 @@ namespace Microsoft.Boogie //public VCExpr vcexpr; //public List interfaceExprVars; //public List privateExprVars; - //public Hashtable/**/ label2absy; + //public Dictionary label2absy; //public VC.ModelViewInfo mvInfo; //public Dictionary> callSites; //public Dictionary> recordProcCallSites; @@ -1007,7 +1007,7 @@ namespace Microsoft.Boogie ConvertCFG2DAG(impl,edgesCut); VC.ModelViewInfo mvInfo; PassifyImpl(impl, out mvInfo); - Hashtable/**/ label2absy = null; + Dictionary label2absy = null; VCExpressionGenerator gen = checker.VCExprGen; Contract.Assert(gen != null); VCExpr vcexpr; diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index b4db817f..4078b43e 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -185,7 +185,7 @@ namespace VC { public VCExpr vcexpr; public List interfaceExprVars; public List privateExprVars; - public Hashtable/**/ label2absy; + public Dictionary label2absy; public ModelViewInfo mvInfo; public Dictionary> callSites; public Dictionary> recordProcCallSites; @@ -1151,7 +1151,7 @@ namespace VC { // Get the VC of the current procedure VCExpr vcMain = implName2StratifiedInliningInfo[impl.Name].vcexpr; - Hashtable/**/ mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy; + Dictionary mainLabel2absy = implName2StratifiedInliningInfo[impl.Name].label2absy; // Find all procedure calls in vc and put labels on them FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy); @@ -1349,7 +1349,7 @@ namespace VC { StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name]; info.GenerateVC(); VCExpr vc = info.vcexpr; - Hashtable mainLabel2absy = info.label2absy; + Dictionary mainLabel2absy = info.label2absy; var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info); // Find all procedure calls in vc and put labels on them @@ -1851,7 +1851,7 @@ namespace VC { // VCs with different labels each time) public class FCallHandler : MutatingVCExprVisitor { Dictionary/*!*/ implName2StratifiedInliningInfo; - public readonly Hashtable/**//*!*/ mainLabel2absy; + public readonly Dictionary/*!*/ mainLabel2absy; public Dictionary/*!*/ boogieExpr2Id; public Dictionary/*!*/ recordExpr2Var; public Dictionary/*!*/ id2Candidate; @@ -1910,7 +1910,7 @@ namespace VC { public FCallHandler(VCExpressionGenerator/*!*/ gen, Dictionary/*!*/ implName2StratifiedInliningInfo, - string mainProcName, Hashtable/**//*!*/ mainLabel2absy) + string mainProcName, Dictionary/*!*/ mainLabel2absy) : base(gen) { Contract.Requires(gen != null); Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo)); @@ -2116,7 +2116,7 @@ namespace VC { return Gen.Eq(VCExpressionGenerator.True, id2ControlVar[candidateId]); } - public Hashtable/**/ getLabel2absy() { + public Dictionary getLabel2absy() { Contract.Ensures(Contract.Result() != null); Contract.Assert(currProc != null); @@ -2158,7 +2158,7 @@ namespace VC { string prefix = "si_fcall_"; // from Wlp.ssc::Cmd(...) if (lop.label.Substring(1).StartsWith(prefix)) { int id = Int32.Parse(lop.label.Substring(prefix.Length + 1)); - Hashtable label2absy = getLabel2absy(); + Dictionary label2absy = getLabel2absy(); Absy cmd = label2absy[id] as Absy; //label2absy.Remove(id); @@ -2718,7 +2718,7 @@ namespace VC { Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); - Hashtable l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy; + Dictionary l2a = cce.NonNull(implName2StratifiedInliningInfo[procName]).label2absy; return cce.NonNull((Absy)l2a[id]); } diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 80ffa072..af3454f5 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -290,7 +290,7 @@ namespace VC { parent.CurrentLocalVariables = impl.LocVars; ModelViewInfo mvInfo; parent.PassifyImpl(impl, out mvInfo); - Hashtable label2Absy; + Dictionary label2Absy; Checker ch = parent.FindCheckerFor(CommandLineOptions.Clo.SmokeTimeout); Contract.Assert(ch != null); @@ -441,7 +441,7 @@ namespace VC { } class ErrorHandler : ProverInterface.ErrorHandler { - Hashtable label2Absy; + Dictionary label2Absy; VerifierCallback callback; [ContractInvariantMethod] void ObjectInvariant() { @@ -450,7 +450,7 @@ namespace VC { } - public ErrorHandler(Hashtable label2Absy, VerifierCallback callback) { + public ErrorHandler(Dictionary label2Absy, VerifierCallback callback) { Contract.Requires(label2Absy != null); Contract.Requires(callback != null); this.label2Absy = label2Absy; @@ -1219,7 +1219,7 @@ namespace VC { this.checker = checker; - Hashtable/**/ label2absy = new Hashtable/**/(); + Dictionary label2absy = new Dictionary(); ProverContext ctx = checker.TheoremProver.Context; Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator; @@ -1350,18 +1350,18 @@ namespace VC { } #endregion - public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Hashtable/**//*!*/ label2absy, ProverContext proverContext) + public VCExpr GenerateVC(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, out Dictionary/*!*/ label2absy, ProverContext proverContext) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null); Contract.Ensures(Contract.Result() != null); - label2absy = new Hashtable/**/(); + label2absy = new Dictionary(); return GenerateVCAux(impl, controlFlowVariableExpr, label2absy, proverContext); } - protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Hashtable/**//*!*/ label2absy, ProverContext proverContext) { + protected VCExpr GenerateVCAux(Implementation/*!*/ impl, VCExpr controlFlowVariableExpr, Dictionary/*!*/ label2absy, ProverContext proverContext) { Contract.Requires(impl != null); Contract.Requires(proverContext != null); Contract.Ensures(Contract.Result() != null); @@ -1654,7 +1654,7 @@ namespace VC { public class ErrorReporter : ProverInterface.ErrorHandler { Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins; - Hashtable/**//*!*/ label2absy; + Dictionary/*!*/ label2absy; List/*!*/ blocks; protected Dictionary/*!*/ incarnationOriginMap; protected VerifierCallback/*!*/ callback; @@ -1687,7 +1687,7 @@ namespace VC { Program/*!*/ program; public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, - Hashtable/**//*!*/ label2absy, + Dictionary/*!*/ label2absy, List/*!*/ blocks, Dictionary/*!*/ incarnationOriginMap, VerifierCallback/*!*/ callback, @@ -1783,7 +1783,7 @@ namespace VC { public class ErrorReporterLocal : ErrorReporter { public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, - Hashtable/**//*!*/ label2absy, + Dictionary/*!*/ label2absy, List/*!*/ blocks, Dictionary/*!*/ incarnationOriginMap, VerifierCallback/*!*/ callback, @@ -2530,7 +2530,7 @@ namespace VC { static VCExpr LetVC(Block startBlock, VCExpr controlFlowVariableExpr, - Hashtable/**/ label2absy, + Dictionary label2absy, ProverContext proverCtxt, out int assertionCount) { Contract.Requires(startBlock != null); @@ -2546,7 +2546,7 @@ namespace VC { static VCExpr LetVCIterative(List blocks, VCExpr controlFlowVariableExpr, - Hashtable label2absy, + Dictionary label2absy, ProverContext proverCtxt, out int assertionCount) { Contract.Requires(blocks != null); @@ -2616,7 +2616,7 @@ namespace VC { static VCExpr LetVC(Block block, VCExpr controlFlowVariableExpr, - Hashtable/**/ label2absy, + Dictionary label2absy, Hashtable/**/ blockVariables, List/*!*/ bindings, ProverContext proverCtxt, @@ -2683,7 +2683,7 @@ namespace VC { static VCExpr DagVC(Block block, VCExpr controlFlowVariableExpr, - Hashtable/**/ label2absy, + Dictionary label2absy, Hashtable/**/ blockEquations, ProverContext proverCtxt, out int assertionCount) @@ -2738,7 +2738,7 @@ namespace VC { } static VCExpr FlatBlockVC(Implementation impl, - Hashtable/**/ label2absy, + Dictionary label2absy, bool local, bool reach, bool doomed, ProverContext proverCtxt, out int assertionCount) @@ -2874,7 +2874,7 @@ namespace VC { } static VCExpr NestedBlockVC(Implementation impl, - Hashtable/**/ label2absy, + Dictionary label2absy, bool reach, ProverContext proverCtxt, out int assertionCount){ @@ -2997,7 +2997,7 @@ namespace VC { } static VCExpr VCViaStructuredProgram - (Implementation impl, Hashtable/**/ label2absy, + (Implementation impl, Dictionary label2absy, ProverContext proverCtxt, out int assertionCount) { diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index d82310ee..eed4e2a5 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -20,19 +20,19 @@ namespace VC { Contract.Invariant(Ctxt != null); } - [Rep] public readonly Hashtable/**/ Label2absy; + [Rep] public readonly Dictionary Label2absy; [Rep] public readonly ProverContext Ctxt; public readonly VCExpr ControlFlowVariableExpr; public int AssertionCount; // counts the number of assertions for which Wlp has been computed - public VCContext(Hashtable/**/ label2absy, ProverContext ctxt) + public VCContext(Dictionary label2absy, ProverContext ctxt) { Contract.Requires(ctxt != null); this.Label2absy = label2absy; this.Ctxt = ctxt; } - public VCContext(Hashtable/**/ label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr) + public VCContext(Dictionary label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr) { Contract.Requires(ctxt != null); this.Label2absy = label2absy; -- cgit v1.2.3