diff options
| -rw-r--r-- | BCT/BytecodeTranslator/CLRSemantics.cs | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 14 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 18 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 4 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 24 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 18 |
6 files changed, 36 insertions, 44 deletions
diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs index 78077ef3..a343402e 100644 --- a/BCT/BytecodeTranslator/CLRSemantics.cs +++ b/BCT/BytecodeTranslator/CLRSemantics.cs @@ -35,7 +35,7 @@ namespace BytecodeTranslator { Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- var tok = TranslationHelper.CciLocationToBoogieToken(division.Locations);
+ var tok = division.Token();
var loc = this.sink.CreateFreshLocal(division.RightOperand.Type);
var locExpr = Bpl.Expr.Ident(loc);
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 108c0fd1..20dd5d2e 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -187,7 +187,7 @@ namespace BytecodeTranslator { }
public override void Visit(IThisReference thisReference) {
- TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(thisReference.Locations),
+ TranslatedExpressions.Push(new Bpl.IdentifierExpr(thisReference.Token(),
this.sink.ThisVariable));
}
@@ -292,7 +292,7 @@ namespace BytecodeTranslator { while (TranslatedExpressions.Count > 0) {
elist.Add(TranslatedExpressions.Pop());
}
- TranslatedExpressions.Push(Bpl.Expr.Select(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(field.Locations), HeapVariable), elist));
+ TranslatedExpressions.Push(Bpl.Expr.Select(new Bpl.IdentifierExpr(field.Token(), HeapVariable), elist));
}
}
@@ -354,7 +354,7 @@ namespace BytecodeTranslator { }
#endregion
- Bpl.IToken cloc = TranslationHelper.CciLocationToBoogieToken(methodCall.Locations);
+ Bpl.IToken cloc = methodCall.Token();
// meeting a constructor is always something special
if (methodCall.MethodToCall.ResolvedMethod.IsConstructor) {
@@ -406,7 +406,7 @@ namespace BytecodeTranslator { Bpl.Expr targetexp = this.TranslatedExpressions.Pop();
Bpl.IdentifierExpr idexp = targetexp as Bpl.IdentifierExpr;
if (idexp != null) {
- StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(TranslationHelper.CciLocationToBoogieToken(assignment.Locations),
+ StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(assignment.Token(),
idexp, sourceexp));
return;
} else {
@@ -547,7 +547,7 @@ namespace BytecodeTranslator { base.Visit(logicalNot);
Bpl.Expr exp = TranslatedExpressions.Pop();
TranslatedExpressions.Push(Bpl.Expr.Unary(
- TranslationHelper.CciLocationToBoogieToken(logicalNot.Locations),
+ logicalNot.Token(),
Bpl.UnaryOperator.Opcode.Not, exp));
}
@@ -556,7 +556,7 @@ namespace BytecodeTranslator { #region CodeContract Expressions
public override void Visit(IOldValue oldValue) {
base.Visit(oldValue);
- TranslatedExpressions.Push(new Bpl.OldExpr(TranslationHelper.CciLocationToBoogieToken(oldValue.Locations),
+ TranslatedExpressions.Push(new Bpl.OldExpr(oldValue.Token(),
TranslatedExpressions.Pop()));
}
@@ -564,7 +564,7 @@ namespace BytecodeTranslator { if (this.sink.RetVariable == null) {
throw new TranslationException(String.Format("Don't know what to do with return value {0}", returnValue.ToString()));
}
- TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(returnValue.Locations),
+ TranslatedExpressions.Push(new Bpl.IdentifierExpr(returnValue.Token(),
this.sink.RetVariable));
}
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 6a3ebcad..c24f6df9 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -107,8 +107,8 @@ namespace BytecodeTranslator { if (method.Type.TypeCode != PrimitiveTypeCode.Void) {
Bpl.Type rettype = Bpl.Type.Int;
out_count++;
- this.sink.RetVariable = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),
- new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),
+ this.sink.RetVariable = new Bpl.Formal(method.Token(),
+ new Bpl.TypedIdent(method.Type.Token(),
"$result", rettype), false);
} else {
this.sink.RetVariable = null;
@@ -119,8 +119,8 @@ namespace BytecodeTranslator { #region Create 'this' parameter
in_count++;
Bpl.Type selftype = Bpl.Type.Int;
- Bpl.Formal self = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),
- new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),
+ Bpl.Formal self = new Bpl.Formal(method.Token(),
+ new Bpl.TypedIdent(method.Type.Token(),
"this", selftype), true);
#endregion
@@ -167,7 +167,7 @@ namespace BytecodeTranslator { Bpl.Requires req
- = new Bpl.Requires(TranslationHelper.CciLocationToBoogieToken(pre.Locations),
+ = new Bpl.Requires(pre.Token(),
true, exptravers.TranslatedExpressions.Pop(), "");
boogiePrecondition.Add(req);
}
@@ -179,7 +179,7 @@ namespace BytecodeTranslator { // Todo: Deal with Descriptions
Bpl.Ensures ens =
- new Bpl.Ensures(TranslationHelper.CciLocationToBoogieToken(post.Locations),
+ new Bpl.Ensures(post.Token(),
true, exptravers.TranslatedExpressions.Pop(), "");
boogiePostcondition.Add(ens);
}
@@ -206,7 +206,7 @@ namespace BytecodeTranslator { string MethodName = TranslationHelper.CreateUniqueMethodName(method);
- Bpl.Procedure proc = new Bpl.Procedure(TranslationHelper.CciLocationToBoogieToken(method.Locations),
+ Bpl.Procedure proc = new Bpl.Procedure(method.Token(),
MethodName, // make it unique!
new Bpl.TypeVariableSeq(),
new Bpl.VariableSeq(invars), // in
@@ -227,7 +227,7 @@ namespace BytecodeTranslator { foreach (MethodParameter mparam in formalMap.Values) {
if (mparam.inParameterCopy != null) {
- Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(method.Locations);
+ Bpl.IToken tok = method.Token();
stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
new Bpl.IdentifierExpr(tok, mparam.outParameterCopy),
new Bpl.IdentifierExpr(tok, mparam.inParameterCopy)));
@@ -258,7 +258,7 @@ namespace BytecodeTranslator { #endregion
Bpl.Implementation impl =
- new Bpl.Implementation(TranslationHelper.CciLocationToBoogieToken(method.Locations),
+ new Bpl.Implementation(method.Token(),
MethodName, // make unique
new Microsoft.Boogie.TypeVariableSeq(),
new Microsoft.Boogie.VariableSeq(invars),
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 38eaf0dc..59812d52 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -66,7 +66,7 @@ namespace BytecodeTranslator { /// <returns></returns>
public Bpl.Variable FindOrCreateLocalVariable(ILocalDefinition local) {
Bpl.LocalVariable v;
- Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(local.Locations);
+ Bpl.IToken tok = local.Token();
Bpl.Type t = TranslationHelper.CciTypeToBoogie(local.Type.ResolvedType);
if (!localVarMap.TryGetValue(local, out v)) {
v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));
@@ -94,7 +94,7 @@ namespace BytecodeTranslator { Bpl.GlobalVariable v;
if (!fieldVarMap.TryGetValue(field, out v)) {
string fieldname = field.ContainingTypeDefinition.ToString() + "." + field.Name.Value;
- Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(field.Locations);
+ Bpl.IToken tok = field.Token();
Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 8ca54050..ab11f7b7 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -40,10 +40,6 @@ namespace BytecodeTranslator #region Helper Methods
- Bpl.IToken TokenFor(IStatement statement) {
- return TranslationHelper.CciLocationToBoogieToken(statement.Locations);
- }
-
Bpl.Expr ExpressionFor(IExpression expression) {
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this);
etrav.Visit(expression);
@@ -65,13 +61,13 @@ namespace BytecodeTranslator public override void Visit(IAssertStatement assertStatement) {
StmtBuilder.Add(
- new Bpl.AssertCmd(TokenFor(assertStatement), ExpressionFor(assertStatement.Condition))
+ new Bpl.AssertCmd(assertStatement.Token(), ExpressionFor(assertStatement.Condition))
);
}
public override void Visit(IAssumeStatement assumeStatement) {
StmtBuilder.Add(
- new Bpl.AssertCmd(TokenFor(assumeStatement), ExpressionFor(assumeStatement.Condition))
+ new Bpl.AssertCmd(assumeStatement.Token(), ExpressionFor(assumeStatement.Condition))
);
}
@@ -89,11 +85,11 @@ namespace BytecodeTranslator thenTraverser.Visit(conditionalStatement.TrueBranch);
elseTraverser.Visit(conditionalStatement.FalseBranch);
- Bpl.IfCmd ifcmd = new Bpl.IfCmd(TokenFor(conditionalStatement),
+ Bpl.IfCmd ifcmd = new Bpl.IfCmd(conditionalStatement.Token(),
condTraverser.TranslatedExpressions.Pop(),
- thenTraverser.StmtBuilder.Collect(TokenFor(conditionalStatement.TrueBranch)),
+ thenTraverser.StmtBuilder.Collect(conditionalStatement.TrueBranch.Token()),
null,
- elseTraverser.StmtBuilder.Collect(TokenFor(conditionalStatement.FalseBranch))
+ elseTraverser.StmtBuilder.Collect(conditionalStatement.FalseBranch.Token())
);
StmtBuilder.Add(ifcmd);
@@ -117,7 +113,7 @@ namespace BytecodeTranslator /// <remarks>(mschaef) Not Implemented</remarks>
/// <param name="breakStatement"></param>
public override void Visit(IBreakStatement breakStatement) {
- StmtBuilder.Add(new Bpl.BreakCmd(TokenFor(breakStatement), "I dont know"));
+ StmtBuilder.Add(new Bpl.BreakCmd(breakStatement.Token(), "I dont know"));
}
/// <summary>
@@ -127,7 +123,7 @@ namespace BytecodeTranslator public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {
if (localDeclarationStatement.InitialValue == null) return;
var loc = this.sink.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);
- var tok = TokenFor(localDeclarationStatement);
+ var tok = localDeclarationStatement.Token();
var e = ExpressionFor(localDeclarationStatement.InitialValue);
StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, loc), e));
return;
@@ -139,7 +135,7 @@ namespace BytecodeTranslator /// <remarks>(mschaef) not implemented</remarks>
/// <param name="returnStatement"></param>
public override void Visit(IReturnStatement returnStatement) {
- Bpl.IToken tok = TokenFor(returnStatement);
+ Bpl.IToken tok = returnStatement.Token();
if (returnStatement.Expression != null) {
ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this);
@@ -152,7 +148,7 @@ namespace BytecodeTranslator StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
new Bpl.IdentifierExpr(tok, this.sink.RetVariable), etrav.TranslatedExpressions.Pop()));
}
- StmtBuilder.Add(new Bpl.ReturnCmd(TokenFor(returnStatement)));
+ StmtBuilder.Add(new Bpl.ReturnCmd(returnStatement.Token()));
}
#endregion
@@ -166,7 +162,7 @@ namespace BytecodeTranslator public override void Visit(IGotoStatement gotoStatement) {
String[] target = new String[1] { gotoStatement.TargetStatement.Label.Value };
- Bpl.GotoCmd gotocmd = new Microsoft.Boogie.GotoCmd(TokenFor(gotoStatement), new Bpl.StringSeq(target));
+ Bpl.GotoCmd gotocmd = new Microsoft.Boogie.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target));
StmtBuilder.Add(gotocmd);
}
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index e27e72c7..756f127f 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -23,7 +23,7 @@ namespace BytecodeTranslator { /// <summary>
/// All parameters of the method get an associated in parameter
- /// in the Boogie procedure.
+ /// in the Boogie procedure except for out parameters.
/// </summary>
public Bpl.Formal/*?*/ inParameterCopy;
@@ -42,8 +42,8 @@ namespace BytecodeTranslator { Bpl.Type ptype = Bpl.Type.Int;
- var parameterToken = TranslationHelper.CciLocationToBoogieToken(parameterDefinition.Locations);
- var typeToken = TranslationHelper.CciLocationToBoogieToken(parameterDefinition.Type.Locations);
+ var parameterToken = parameterDefinition.Token();
+ var typeToken = parameterDefinition.Type.Token();
var parameterName = parameterDefinition.Name.Value;
if (!parameterDefinition.IsOut) {
@@ -64,16 +64,12 @@ namespace BytecodeTranslator { /// <summary>
/// Class containing several static helper functions to convert
- /// from Cci to Boogie Methodology
+ /// from Cci to Boogie
/// </summary>
- class TranslationHelper {
+ static class TranslationHelper {
- public static Bpl.IToken CciLocationToBoogieToken(IEnumerable<ILocation> locations) {
- Bpl.IToken tok = Bpl.Token.NoToken;
- return tok;
- }
-
- public static Bpl.IToken CciLocationToBoogieToken(ILocation location) {
+ public static Bpl.IToken Token(this IObjectWithLocations objectWithLocations) {
+ //TODO: use objectWithLocations.Locations!
Bpl.IToken tok = Bpl.Token.NoToken;
return tok;
}
|