summaryrefslogtreecommitdiff
path: root/Source/VCGeneration
diff options
context:
space:
mode:
Diffstat (limited to 'Source/VCGeneration')
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs60
-rw-r--r--Source/VCGeneration/FixedpointVC.cs2
-rw-r--r--Source/VCGeneration/StratifiedVC.cs2
-rw-r--r--Source/VCGeneration/VC.cs22
4 files changed, 43 insertions, 43 deletions
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));
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-22 05:05:20 +0000