summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--BCT/BytecodeTranslator/Sink.cs12
-rw-r--r--BCT/BytecodeTranslator/StatementTraverser.cs60
2 files changed, 30 insertions, 42 deletions
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 3c5db959..4d13d638 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -913,20 +913,11 @@ namespace BytecodeTranslator {
public int FindOrCreateCciLabelIdentifier(IName label) {
int v;
if (!cciLabels.TryGetValue(label, out v)) {
- v = cciLabels.Count + boogieLabels.Count;
+ v = cciLabels.Count;
cciLabels[label] = v;
}
return v;
}
- public Dictionary<string, int> boogieLabels;
- public int FindOrCreateBoogieLabelIdentifier(string label) {
- int v;
- if (!boogieLabels.TryGetValue(label, out v)) {
- v = cciLabels.Count + boogieLabels.Count;
- boogieLabels[label] = v;
- }
- return v;
- }
Dictionary<ITryCatchFinallyStatement, int> tryCatchFinallyIdentifiers;
public string FindOrCreateCatchLabel(ITryCatchFinallyStatement stmt) {
int id;
@@ -961,7 +952,6 @@ namespace BytecodeTranslator {
this.BeginMethod(method.ContainingType);
this.methodBeingTranslated = method;
this.cciLabels = new Dictionary<IName, int>();
- this.boogieLabels = new Dictionary<string, int>();
this.tryCatchFinallyIdentifiers = new Dictionary<ITryCatchFinallyStatement, int>();
mostNestedTryStatementTraverser = new MostNestedTryStatementTraverser();
mostNestedTryStatementTraverser.Visit(method.Body);
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 2e88e72c..c7b94f1a 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -97,11 +97,6 @@ namespace BytecodeTranslator
Bpl.Expr targetExpr = Bpl.Expr.Literal(sink.cciLabels[name]);
elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);
}
- foreach (string name in sink.boogieLabels.Keys) {
- Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(name));
- Bpl.Expr targetExpr = Bpl.Expr.Literal(sink.boogieLabels[name]);
- elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);
- }
this.StmtBuilder.Add(elseIfCmd);
}
#endregion
@@ -298,10 +293,10 @@ namespace BytecodeTranslator
count++;
}
System.Diagnostics.Debug.Assert((count == nestedTryCatchFinallyStatements.Count) == (targetContext == null));
- if (count != 0) {
+ if (count > 0) {
int id = this.sink.FindOrCreateCciLabelIdentifier(target);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(id)));
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(count)));
+ StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(count-1)));
string finallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[this.nestedTryCatchFinallyStatements.Count - 1].Item1);
StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(finallyLabel)));
}
@@ -336,26 +331,22 @@ namespace BytecodeTranslator
List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>> nestedTryCatchFinallyStatements;
private void RaiseExceptionHelper(Bpl.StmtListBuilder builder) {
- List<Bpl.Cmd> cmds = new List<Bpl.Cmd>();
int count = nestedTryCatchFinallyStatements.Count;
if (count == 0) {
builder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken));
}
else {
Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext> topOfStack = nestedTryCatchFinallyStatements[count - 1];
- cmds.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(0)));
- string continuationTarget = this.sink.FindOrCreateContinuationLabel(topOfStack.Item1);
- string exceptionTarget; // jump target of the exception
+ string exceptionTarget;
if (topOfStack.Item2 == TryCatchFinallyContext.InTry) {
exceptionTarget = this.sink.FindOrCreateCatchLabel(topOfStack.Item1);
}
else if (topOfStack.Item2 == TryCatchFinallyContext.InCatch) {
+ builder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));
exceptionTarget = this.sink.FindOrCreateFinallyLabel(topOfStack.Item1);
- int continuationId = this.sink.FindOrCreateBoogieLabelIdentifier(continuationTarget);
- builder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(continuationId)));
}
else {
- exceptionTarget = continuationTarget;
+ exceptionTarget = this.sink.FindOrCreateContinuationLabel(topOfStack.Item1);
}
builder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(exceptionTarget)));
}
@@ -373,12 +364,9 @@ namespace BytecodeTranslator
}
public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {
- int continuationId = this.sink.FindOrCreateBoogieLabelIdentifier(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement));
-
nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InTry));
this.Visit(tryCatchFinallyStatement.TryBody);
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(continuationId)));
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(0)));
+ StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));
StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));
nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);
@@ -396,8 +384,7 @@ namespace BytecodeTranslator
catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(catchClauseVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));
}
catchTraverser.Visit(catchClause.Body);
- catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(continuationId)));
- catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(0)));
+ catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));
catchTraverser.StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));
catchStatements.Insert(0, catchTraverser.StmtBuilder.Collect(catchClause.Token()));
}
@@ -416,31 +403,42 @@ namespace BytecodeTranslator
if (tryCatchFinallyStatement.FinallyBody != null) {
nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InFinally));
Bpl.Variable savedExcVariable = this.sink.CreateFreshLocal(this.sink.Heap.RefType);
- Bpl.Variable savedFinallyStackCounterVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);
Bpl.Variable savedLabelVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);
+ Bpl.Variable savedFinallyStackCounterVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedExcVariable), Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)));
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedFinallyStackCounterVariable), Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable)));
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedLabelVariable), Bpl.Expr.Ident(this.sink.LabelVariable)));
+ StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedFinallyStackCounterVariable), Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable)));
Visit(tryCatchFinallyStatement.FinallyBody);
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(savedExcVariable)));
- StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Ident(savedFinallyStackCounterVariable)));
StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Ident(savedLabelVariable)));
+ StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Ident(savedFinallyStackCounterVariable)));
nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);
}
- Bpl.IdentifierExpr fsv = Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable);
Bpl.GotoCmd dispatchCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq("DispatchContinuation"));
+ Bpl.GotoCmd continuationCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement)));
+ Bpl.IfCmd ifCmd = new Bpl.IfCmd(
+ Bpl.Token.NoToken,
+ Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)),
+ TranslationHelper.BuildStmtList(continuationCmd),
+ new Bpl.IfCmd(
+ Bpl.Token.NoToken,
+ Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(0)),
+ TranslationHelper.BuildStmtList(dispatchCmd),
+ null,
+ null),
+ null);
+ this.StmtBuilder.Add(ifCmd);
int count = this.nestedTryCatchFinallyStatements.Count;
if (count == 0) {
- this.StmtBuilder.Add(dispatchCmd);
+ this.StmtBuilder.Add(new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false)));
}
else {
+ Bpl.IdentifierExpr fsv = Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable);
Bpl.AssignCmd decrementCmd = TranslationHelper.BuildAssignCmd(fsv, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, fsv, Bpl.Expr.Literal(1)));
- string finallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[count - 1].Item1);
- Bpl.GotoCmd parentCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(finallyLabel));
- Bpl.StmtList thenList = TranslationHelper.BuildStmtList(dispatchCmd);
- Bpl.StmtList elseList = TranslationHelper.BuildStmtList(decrementCmd, parentCmd);
- Bpl.IfCmd ifCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, fsv, Bpl.Expr.Literal(0)), thenList, null, elseList);
- this.StmtBuilder.Add(ifCmd);
+ this.StmtBuilder.Add(decrementCmd);
+ string parentFinallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[count - 1].Item1);
+ Bpl.GotoCmd parentCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(parentFinallyLabel));
+ this.StmtBuilder.Add(parentCmd);
}
StmtBuilder.AddLabelCmd(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement));
Bpl.Expr raiseExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 22:12:47 +0000