diff options
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Core/Absy.cs | 12 | ||||
-rw-r--r-- | Source/Core/AbsyCmd.cs | 8 | ||||
-rw-r--r-- | Source/Core/Duplicator.cs | 6 | ||||
-rw-r--r-- | Source/Core/Inline.cs | 8 | ||||
-rw-r--r-- | Source/Core/LambdaHelper.cs | 2 | ||||
-rw-r--r-- | Source/Core/OwickiGries.cs | 12 | ||||
-rw-r--r-- | Source/Doomed/VCDoomed.cs | 10 | ||||
-rw-r--r-- | Source/Houdini/Houdini.cs | 8 | ||||
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 60 | ||||
-rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 2 | ||||
-rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 | ||||
-rw-r--r-- | Source/VCGeneration/VC.cs | 22 |
12 files changed, 76 insertions, 76 deletions
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<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToInputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();
Dictionary<Block/*!*/, VariableSeq/*!*/>/*!*/ loopHeaderToOutputs = new Dictionary<Block/*!*/, VariableSeq/*!*/>();
- Dictionary<Block/*!*/, Hashtable/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Hashtable/*!*/>();
+ Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary<Block/*!*/, Dictionary<Variable, Expr>/*!*/>();
Dictionary<Block/*!*/, LoopProcedure/*!*/>/*!*/ loopHeaderToLoopProc = new Dictionary<Block/*!*/, LoopProcedure/*!*/>();
Dictionary<Block/*!*/, CallCmd/*!*/>/*!*/ loopHeaderToCallCmd1 = new Dictionary<Block/*!*/, CallCmd/*!*/>();
Dictionary<Block, CallCmd> loopHeaderToCallCmd2 = new Dictionary<Block, CallCmd>();
@@ -402,7 +402,7 @@ namespace Microsoft.Boogie { IdentifierExprSeq callOutputs2 = new IdentifierExprSeq();
List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
- Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr
+ Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>(); // Variable -> IdentifierExpr
VariableSeq/*!*/ targets = new VariableSeq();
HashSet<Variable> footprint = new HashSet<Variable>();
@@ -2914,17 +2914,17 @@ namespace Microsoft.Boogie { }
}
- private Hashtable/*Variable->Expr*//*?*/ formalMap = null;
+ private Dictionary<Variable, Expr>/*?*/ formalMap = null;
public void ResetImplFormalMap() {
this.formalMap = null;
}
- public Hashtable /*Variable->Expr*//*!*/ GetImplFormalMap() {
+ public Dictionary<Variable, Expr>/*!*/ GetImplFormalMap() {
Contract.Ensures(Contract.Result<Hashtable>() != null);
if (this.formalMap != null)
return this.formalMap;
else {
- Hashtable /*Variable->Expr*//*!*/ map = new Hashtable /*Variable->Expr*/ (InParams.Length + OutParams.Length);
+ Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (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>", 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<Cmd>() != 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<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();
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<Variable, Expr> 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<Variable, Expr> map) {
Contract.Requires(map != null);
Contract.Ensures(Contract.Result<Substitution>() != null);
// TODO: With Whidbey, could use anonymous functions.
return new Substitution(new CreateSubstitutionClosure(map).Method);
}
private sealed class CreateSubstitutionClosure {
- Hashtable/*Variable!->Expr!*//*!*/ map;
+ Dictionary<Variable /*!*/, Expr /*!*/>/*!*/ map;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(map != null);
}
- public CreateSubstitutionClosure(Hashtable/*Variable!->Expr!*/ map)
+ public CreateSubstitutionClosure(Dictionary<Variable, Expr> 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<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
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<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();
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<Variable, Expr> substMap) {
Contract.Requires(substMap != null);
Subst = Substituter.SubstitutionFromHashtable(substMap);
}
- public CodeCopier(Hashtable substMap, Hashtable oldSubstMap) {
+ public CodeCopier(Dictionary<Variable, Expr> substMap, Dictionary<Variable, Expr> 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<Variable, Expr> subst = new Dictionary<Variable, Expr>();
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<Variable, Expr> map = new Dictionary<Variable, Expr>();
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<CmdSeq> yields, Hashtable map)
+ private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Dictionary<Variable, Expr> 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<Variable, Expr> ogOldLocalMap = new Dictionary<Variable, Expr>();
+ Dictionary<Variable, Expr> assumeMap = new Dictionary<Variable, Expr>(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<Variable, Expr> map = new Dictionary<Variable, Expr>();
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<Variable, Expr>());
}
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<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
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<Variable, Expr> 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<Variable, Expr> var2Expr = PassifyProgram(impl, new ModelViewInfo(program, impl));
// Collect the last incarnation of each reachability variable in the passive program
foreach (KeyValuePair<Block, Variable> 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<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
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<Variable, Expr> cToTrue = new Dictionary<Variable, Expr>();
Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().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<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];
- Hashtable subst = new Hashtable();
+ Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
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<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];
- Hashtable subst = new Hashtable();
+ Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();
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<Variable, Expr>();
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)
/// </param>
- protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins) {
+ protected static Block InjectPostConditions(Implementation impl, Block unifiedExitBlock, Dictionary<TransferCmd, ReturnCmd> 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<TransferCmd, ReturnCmd> gotoCmdOrigins) {
Contract.Requires(impl != null);
Contract.Requires(gotoCmdOrigins != null);
Contract.Ensures(Contract.Result<Block>() != 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 { /// <param name="b"></param>
/// <param name="block2Incarnation">Gives incarnation maps for b's predecessors.</param>
/// <returns></returns>
- protected Hashtable /*Variable -> Expr*/ ComputeIncarnationMap(Block b, Hashtable /*Variable -> Expr*/ block2Incarnation) {
+ protected Dictionary<Variable, Expr> ComputeIncarnationMap(Block b, Dictionary<Block, Dictionary<Variable, Expr>> block2Incarnation) {
Contract.Requires(b != null);
Contract.Requires(block2Incarnation != null);
Contract.Ensures(Contract.Result<Hashtable>() != null);
if (b.Predecessors.Length == 0) {
- return new Hashtable();
+ return new Dictionary<Variable, Expr>();
}
- Hashtable /*Variable -> Expr*/ incarnationMap = null;
+ Dictionary<Variable, Expr> 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<Variable, Expr> predMap = (Dictionary<Variable, Expr>)block2Incarnation[pred];
Contract.Assert(predMap != null);
if (incarnationMap == null) {
- incarnationMap = (Hashtable /*Variable -> Expr*/)predMap.Clone();
+ incarnationMap = new Dictionary<Variable, Expr>(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<Variable, Expr> predMap = (Dictionary<Variable, Expr>)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<Variable, Expr> 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<Variable, Expr> 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<Variable, Expr> Convert2PassiveCmd(Implementation impl, ModelViewInfo mvInfo) {
Contract.Requires(impl != null);
Contract.Requires(mvInfo != null);
- Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
+ Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies, mvInfo);
RestoreParamWhereClauses(impl);
@@ -1322,7 +1322,7 @@ namespace VC { return r;
}
- protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {
+ protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(List<Block> 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<Block, Dictionary<Variable, Expr>> block2Incarnation = new Dictionary<Block, Dictionary<Variable, Expr>>();
Block exitBlock = null;
- Hashtable exitIncarnationMap = null;
+ Dictionary<Variable, Expr> 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<Variable, Expr> 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 { /// </summary>
protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)
{
- Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();
+ Dictionary<Variable, Expr> oldFrameMap = new Dictionary<Variable, Expr>();
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.
/// </summary>
- protected void TurnIntoPassiveCmd(Cmd c, Hashtable /*Variable -> Expr*/ incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {
+ protected void TurnIntoPassiveCmd(Cmd c, Dictionary<Variable, Expr> 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<Variable, Expr>(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<Variable, Expr>)cce.NonNull(new Dictionary<Variable, Expr>(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<Variable, Expr>(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<Variable, Expr> IncarnationMap;
+ public Mapping(string description, Dictionary<Variable, Expr> 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<Variable, Expr>();
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<Variable, Expr>();
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<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins;
readonly public VCGen/*!*/ parent;
Implementation/*!*/ impl;
@@ -548,7 +548,7 @@ namespace VC { private int splitNo;
internal ErrorReporter reporter;
- public Split(List<Block/*!*/>/*!*/ blocks, Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins, VCGen/*!*/ par, Implementation/*!*/ impl) {
+ public Split(List<Block/*!*/>/*!*/ blocks, Dictionary<TransferCmd, ReturnCmd>/*!*/ 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<Block> newBlocks = new List<Block>();
- Hashtable newGotoCmdOrigins = new Hashtable();
+ Dictionary<TransferCmd, ReturnCmd> newGotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
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<Variable, Expr> 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<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins;
Dictionary<int, Absy>/*!*/ label2absy;
List<Block/*!*/>/*!*/ blocks;
protected Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap;
@@ -1686,7 +1686,7 @@ namespace VC { protected ProverContext/*!*/ context;
Program/*!*/ program;
- public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
+ public ErrorReporter(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,
@@ -1782,7 +1782,7 @@ namespace VC { }
public class ErrorReporterLocal : ErrorReporter {
- public ErrorReporterLocal(Hashtable/*TransferCmd->ReturnCmd*//*!*/ gotoCmdOrigins,
+ public ErrorReporterLocal(Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins,
Dictionary<int, Absy>/*!*/ label2absy,
List<Block/*!*/>/*!*/ blocks,
Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,
@@ -2097,13 +2097,13 @@ namespace VC { }
}
- public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)
+ public Dictionary<TransferCmd, ReturnCmd> PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)
{
Contract.Requires(impl != null);
Contract.Requires(program != null);
Contract.Ensures(Contract.Result<Hashtable>() != null);
- Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();
+ Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins = new Dictionary<TransferCmd, ReturnCmd>();
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<Variable, Expr> incarnationMap = ComputeIncarnationMap(entryBlock, new Dictionary<Block, Dictionary<Variable, Expr>>());
TurnIntoPassiveBlock(entryBlock, incarnationMap, mvInfo,
ComputeOldExpressionSubstitution(impl.Proc.Modifies));
}
|