diff options
Diffstat (limited to 'BCT')
| -rw-r--r-- | BCT/BytecodeTranslator/BytecodeTranslator.csproj | 4 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/CLRSemantics.cs | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/ClassTraverser.cs | 85 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 24 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MethodTraverser.cs | 341 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/StatementTraverser.cs | 20 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/ToplevelTraverser.cs | 82 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TraverserFactory.cs | 6 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/UnitTest0.cs | 2 |
10 files changed, 27 insertions, 541 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj index e566adff..0a7d6d55 100644 --- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj +++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj @@ -109,13 +109,11 @@ </ItemGroup>
<ItemGroup>
<Compile Include="CLRSemantics.cs" />
+ <Compile Include="MetadataTraverser.cs" />
<Compile Include="Prelude.cs" />
<Compile Include="ExpressionTraverser.cs" />
- <Compile Include="ClassTraverser.cs" />
- <Compile Include="MethodTraverser.cs" />
<Compile Include="StatementTraverser.cs" />
<Compile Include="Program.cs" />
- <Compile Include="ToplevelTraverser.cs" />
<Compile Include="TranslationException.cs" />
<Compile Include="TranslationHelper.cs" />
<Compile Include="TraverserFactory.cs" />
diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs index f52b2006..c9f09f5f 100644 --- a/BCT/BytecodeTranslator/CLRSemantics.cs +++ b/BCT/BytecodeTranslator/CLRSemantics.cs @@ -37,7 +37,7 @@ namespace BytecodeTranslator { var tok = TranslationHelper.CciLocationToBoogieToken(division.Locations);
- var loc = this.StmtTraverser.MethodTraverser.CreateFreshLocal(division.RightOperand.Type);
+ var loc = this.StmtTraverser.MetadataTraverser.CreateFreshLocal(division.RightOperand.Type);
var locExpr = Bpl.Expr.Ident(loc);
var storeLocal = Bpl.Cmd.SimpleAssign(tok, locExpr, rexp);
this.StmtTraverser.StmtBuilder.Add(storeLocal);
diff --git a/BCT/BytecodeTranslator/ClassTraverser.cs b/BCT/BytecodeTranslator/ClassTraverser.cs deleted file mode 100644 index ce72c9ba..00000000 --- a/BCT/BytecodeTranslator/ClassTraverser.cs +++ /dev/null @@ -1,85 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-using Microsoft.Cci;
-using Microsoft.Cci.MetadataReader;
-using Microsoft.Cci.MutableCodeModel;
-using Microsoft.Cci.Contracts;
-using Microsoft.Cci.ILToCodeModel;
-
-using Bpl = Microsoft.Boogie;
-
-namespace BytecodeTranslator {
- /// <summary>
- ///
- /// </summary>
- public class ClassTraverser : BaseCodeAndContractTraverser {
-
- public readonly TraverserFactory factory;
-
- public readonly ToplevelTraverser ToplevelTraverser;
-
- private Dictionary<IFieldDefinition, Bpl.GlobalVariable> fieldVarMap = new Dictionary<IFieldDefinition, Microsoft.Boogie.GlobalVariable>();
-
- private Dictionary<IMethodDefinition, MethodTraverser> methodMap = new Dictionary<IMethodDefinition, MethodTraverser>();
-
- // TODO: (mschaef) just a stub
- public readonly Bpl.Variable ThisVariable = TranslationHelper.TempThisVar();
-
- public readonly Bpl.Variable HeapVariable = TranslationHelper.TempHeapVar();
-
- public ClassTraverser(TraverserFactory factory, IContractProvider cp, ToplevelTraverser tlTraverser)
- : base(cp) {
- this.factory = factory;
- ToplevelTraverser = tlTraverser;
- }
-
- public Bpl.Variable FindOrCreateFieldVariable(IFieldDefinition field) {
- 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.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
-
- v = new Bpl.GlobalVariable(tok,tident);
- fieldVarMap.Add(field, v);
- ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Constant(tok, tident, true));
- }
- return v;
- }
-
-
- /// <summary>
- ///
- /// </summary>
- /// <param name="method"></param>
- public override void Visit(IMethodDefinition method) {
- // check if it's static and so on
- MethodTraverser mt;
- if (!methodMap.TryGetValue(method, out mt)) {
- mt = this.factory.MakeMethodTraverser(this, this.contractProvider);
- this.methodMap.Add(method, mt);
- }
- mt.Visit(method);
- }
-
- public override void Visit(IFieldDefinition fieldDefinition) {
- this.FindOrCreateFieldVariable(fieldDefinition);
- }
-
- public override void Visit(ITypeInvariant typeInvariant) {
- // Todo: Not implemented
- base.Visit(typeInvariant);
- }
-
- }
-
-}
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index beeb5cb1..a8f9a758 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -52,12 +52,12 @@ namespace BytecodeTranslator { public override void Visit(IAddressableExpression addressableExpression) {
ILocalDefinition/*?*/ local = addressableExpression.Definition as ILocalDefinition;
if (local != null) {
- TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));
return;
}
IParameterDefinition/*?*/ param = addressableExpression.Definition as IParameterDefinition;
if (param != null) {
- TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));
return;
}
IFieldReference/*?*/ field = addressableExpression.Definition as IFieldReference;
@@ -125,7 +125,7 @@ namespace BytecodeTranslator { #region LocalDefinition
ILocalDefinition/*?*/ local = targetExpression.Definition as ILocalDefinition;
if (local != null) {
- TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));
return;
}
#endregion
@@ -133,7 +133,7 @@ namespace BytecodeTranslator { #region ParameterDefenition
IParameterDefinition param = targetExpression.Definition as IParameterDefinition;
if (param != null) {
- TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));
return;
}
#endregion
@@ -156,7 +156,7 @@ namespace BytecodeTranslator { public override void Visit(IThisReference thisReference) {
TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(thisReference.Locations),
- this.StmtTraverser.MethodTraverser.ClassTraverser.ThisVariable));
+ this.StmtTraverser.MetadataTraverser.ThisVariable));
}
public override void Visit(IBoundExpression boundExpression) {
@@ -168,7 +168,7 @@ namespace BytecodeTranslator { #region LocalDefinition
ILocalDefinition local = boundExpression.Definition as ILocalDefinition;
if (local != null) {
- TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));
return;
}
#endregion
@@ -176,7 +176,7 @@ namespace BytecodeTranslator { #region ParameterDefiniton
IParameterDefinition param = boundExpression.Definition as IParameterDefinition;
if (param != null) {
- TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));
return;
}
#endregion
@@ -248,9 +248,7 @@ namespace BytecodeTranslator { //TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.ClassTraverser.FindOrCreateFieldVariable(field.ResolvedField))
TranslatedExpressions.Push( Bpl.Expr.Ident(
- this.StmtTraverser.MethodTraverser.ClassTraverser.ToplevelTraverser.FindOrCreateClassField(
- field.ContainingType.ResolvedType,
- field.ResolvedField) ) );
+ this.StmtTraverser.MetadataTraverser.FindOrCreateFieldVariable(field.ResolvedField) ) );
this.Visit(instance);
@@ -347,7 +345,7 @@ namespace BytecodeTranslator { #endregion
if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
- Bpl.Variable v = this.StmtTraverser.MethodTraverser.CreateFreshLocal(methodCall.Type.ResolvedType);
+ Bpl.Variable v = this.StmtTraverser.MetadataTraverser.CreateFreshLocal(methodCall.Type.ResolvedType);
outvars.Add(new Bpl.IdentifierExpr(cloc, v));
TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));
}
@@ -531,11 +529,11 @@ namespace BytecodeTranslator { }
public override void Visit(IReturnValue returnValue) {
- if (this.StmtTraverser.MethodTraverser.RetVariable == null) {
+ if (this.StmtTraverser.MetadataTraverser.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),
- this.StmtTraverser.MethodTraverser.RetVariable));
+ this.StmtTraverser.MetadataTraverser.RetVariable));
}
#endregion
diff --git a/BCT/BytecodeTranslator/MethodTraverser.cs b/BCT/BytecodeTranslator/MethodTraverser.cs deleted file mode 100644 index 7a7170e9..00000000 --- a/BCT/BytecodeTranslator/MethodTraverser.cs +++ /dev/null @@ -1,341 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-using Microsoft.Cci;
-using Microsoft.Cci.MetadataReader;
-using Microsoft.Cci.MutableCodeModel;
-using Microsoft.Cci.Contracts;
-using Microsoft.Cci.ILToCodeModel;
-
-using Bpl = Microsoft.Boogie;
-
-namespace BytecodeTranslator {
- public class MethodTraverser : BaseCodeAndContractTraverser {
-
- public readonly TraverserFactory factory;
-
- public readonly ClassTraverser ClassTraverser;
-
- private Bpl.Procedure procedure;
-
- public Bpl.Variable RetVariable;
-
- public List<MethodParameter> OutVars = new List<MethodParameter>();
-
- public Bpl.Variable HeapVariable;
-
- private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();
-
- public class MethodParameter {
- public MethodParameter() {
- localParameter = null;
- inParameterCopy = null;
- outParameterCopy = null;
- }
-
- public Bpl.Formal localParameter;
- public Bpl.Formal inParameterCopy;
- public Bpl.Formal outParameterCopy;
- }
-
- private Dictionary<IParameterDefinition, MethodParameter> formalMap = new Dictionary<IParameterDefinition, MethodParameter>();
-
- #region Helper Functions
- /// <summary>
- ///
- /// </summary>
- /// <param name="local"></param>
- /// <returns></returns>
- public Bpl.Variable FindOrCreateLocalVariable(ILocalDefinition local) {
- Bpl.LocalVariable v;
- Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(local.Locations);
- 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));
- localVarMap.Add(local, v);
- }
- return v;
- }
-
- /// <summary>
- /// Creates a fresh local var of the given Type and adds it to the
- /// Bpl Implementation
- /// </summary>
- /// <param name="typeReference"> The type of the new variable </param>
- /// <returns> A fresh Variable with automatic generated name and location </returns>
- public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {
- Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(typeReference);
- Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));
- ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie
- localVarMap.Add(dummy, v);
- return v;
- }
-
- /// <summary>
- ///
- /// </summary>
- /// <param name="param"></param>
- /// <remarks> (mschaef) only a stub </remarks>
- private MethodParameter CreateBoogieParameter(IParameterDefinition param) {
- MethodParameter mparam = new MethodParameter();
-
- Bpl.Type ptype = Bpl.Type.Int;
-
- Bpl.Formal v = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),
- new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),
- param.Name.Value, ptype), false);
-
- Bpl.Formal v_in = null;
- if (!param.IsOut) {
- v_in = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),
- new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),
- param.Name.Value + "$in", ptype), true);
- }
- Bpl.Formal v_out = null;
- if (param.IsByReference || param.IsOut) {
- v_out = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),
- new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),
- param.Name.Value + "$out", ptype), false);
- }
- mparam.localParameter = v;
- mparam.inParameterCopy = v_in;
- mparam.outParameterCopy = v_out;
-
- return mparam;
- }
-
- /// <summary>
- ///
- /// </summary>
- /// <param name="param"></param>
- /// <remarks>STUB</remarks>
- /// <returns></returns>
- public Bpl.Variable FindParameterVariable(IParameterDefinition param) {
- MethodParameter mp;
- formalMap.TryGetValue(param, out mp);
- return mp.localParameter;
- }
- #endregion
-
- public MethodTraverser(TraverserFactory factory, IContractProvider cp, ClassTraverser cTraverser)
- : base(cp) {
- this.factory = factory;
- HeapVariable = cTraverser.HeapVariable;
- procedure = null;
- ClassTraverser = cTraverser;
- }
-
- #region Overrides
-
- /// <summary>
- ///
- /// </summary>
- /// <param name="method"></param>
- public override void Visit(IMethodDefinition method) {
-
- try {
- #region Create in- and out-parameters
-
- int in_count = 0;
- int out_count = 0;
- MethodParameter mp;
- foreach (IParameterDefinition formal in method.ResolvedMethod.Parameters) {
-
- mp = CreateBoogieParameter(formal);
- if (mp.inParameterCopy != null) in_count++;
- if (mp.outParameterCopy != null) out_count++;
- formalMap.Add(formal, mp);
- }
-
- #region Look for Returnvalue
-
- // This is just a hack, should be replaced with something more robust
- if (method.Type.TypeCode != PrimitiveTypeCode.Void) {
- Bpl.Type rettype = Bpl.Type.Int;
- out_count++;
- RetVariable = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),
- new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),
- "$result", rettype), false);
- } else {
- RetVariable = null;
- }
-
- #endregion
-
- #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),
- "this", selftype), true);
-
- #endregion
-
- Bpl.Variable[] invars = new Bpl.Formal[in_count];
- Bpl.Variable[] outvars = new Bpl.Formal[out_count];
-
- int i = 0;
- int j = 0;
-
- #region Add 'this' parameter as first in parameter
- invars[i++] = self;
- #endregion
-
- foreach (MethodParameter mparam in formalMap.Values) {
- if (mparam.inParameterCopy != null) {
- invars[i++] = mparam.inParameterCopy;
- }
- if (mparam.outParameterCopy != null) {
- outvars[j++] = mparam.outParameterCopy;
- OutVars.Add(mparam);
- }
- }
-
- #region add the returnvalue to out if there is one
- if (RetVariable != null) outvars[j] = RetVariable;
- #endregion
-
- #endregion
-
- #region Check The Method Contracts
- Bpl.RequiresSeq boogiePrecondition = new Bpl.RequiresSeq();
- Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();
- Bpl.IdentifierExprSeq boogieModifies = new Bpl.IdentifierExprSeq();
-
- IMethodContract contract = contractProvider.GetMethodContractFor(method);
-
- if (contract != null) {
- try {
- foreach (IPrecondition pre in contract.Preconditions) {
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);
- exptravers.Visit(pre.Condition); // TODO
- // Todo: Deal with Descriptions
-
-
- Bpl.Requires req
- = new Bpl.Requires(TranslationHelper.CciLocationToBoogieToken(pre.Locations),
- true, exptravers.TranslatedExpressions.Pop(), "");
- boogiePrecondition.Add(req);
- }
-
- foreach (IPostcondition post in contract.Postconditions) {
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);
-
- exptravers.Visit(post.Condition);
- // Todo: Deal with Descriptions
-
- Bpl.Ensures ens =
- new Bpl.Ensures(TranslationHelper.CciLocationToBoogieToken(post.Locations),
- true, exptravers.TranslatedExpressions.Pop(), "");
- boogiePostcondition.Add(ens);
- }
-
- foreach (IAddressableExpression mod in contract.ModifiedVariables) {
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);
- exptravers.Visit(mod);
-
- Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
-
- if (idexp == null) {
- throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));
- }
- boogieModifies.Add(idexp);
- }
- } catch (TranslationException te) {
- throw new NotImplementedException("Cannot Handle Errors in Method Contract: " + te.ToString());
- } catch {
- throw;
- }
- }
-
- #endregion
-
- string MethodName = TranslationHelper.CreateUniqueMethodName(method);
-
- Bpl.Procedure proc = new Bpl.Procedure(TranslationHelper.CciLocationToBoogieToken(method.Locations),
- MethodName, // make it unique!
- new Bpl.TypeVariableSeq(),
- new Bpl.VariableSeq(invars), // in
- new Bpl.VariableSeq(outvars), // out
- boogiePrecondition,
- boogieModifies,
- boogiePostcondition);
-
- ClassTraverser.ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(proc);
-
- this.procedure = proc;
-
- if (method.IsAbstract) {
- throw new NotImplementedException("abstract methods are not yet implemented");
- }
-
- StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this, this.HeapVariable);
-
- #region Add assignements from In-Params to local-Params
-
- foreach (MethodParameter mparam in formalMap.Values) {
- if (mparam.inParameterCopy != null) {
- Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(method.Locations);
- stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
- new Bpl.IdentifierExpr(tok, mparam.localParameter),
- new Bpl.IdentifierExpr(tok, mparam.inParameterCopy)));
- }
- }
-
- #endregion
-
- try {
- method.ResolvedMethod.Body.Dispatch(stmtTraverser);
- } catch (TranslationException te) {
- throw new NotImplementedException("No Errorhandling in Methodvisitor / " + te.ToString());
- } catch {
- throw;
- }
-
- #region Create Local Vars For Implementation
- //Todo: (mschaef) hack, there must be a better way to copy this
- Bpl.Variable[] vars = new Bpl.Variable[localVarMap.Values.Count + formalMap.Values.Count];
- i = 0;
- foreach (Bpl.Variable v in localVarMap.Values) {
- vars[i++] = v;
- }
- foreach (MethodParameter mparam in formalMap.Values) {
- vars[i++] = mparam.localParameter;
- }
-
- Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars);
- #endregion
-
- Bpl.Implementation impl =
- new Bpl.Implementation(TranslationHelper.CciLocationToBoogieToken(method.Locations),
- MethodName, // make unique
- new Microsoft.Boogie.TypeVariableSeq(),
- new Microsoft.Boogie.VariableSeq(invars),
- new Microsoft.Boogie.VariableSeq(outvars),
- vseq,
- stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));
-
- impl.Proc = proc;
- ClassTraverser.ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(impl);
- } catch (TranslationException te) {
- throw new NotImplementedException(te.ToString());
- } catch {
- throw;
- } finally {
- // Maybe this is a good place to add the procedure to the toplevel declarations
- }
- }
-
- #endregion
-
- }
-
-}
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 452cc114..14cbfce7 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -62,7 +62,7 @@ namespace BytecodeTranslator { #region Pass 3: Translate the code model to BPL
//tmp_BPLGenerator translator = new tmp_BPLGenerator(host, acp);
var factory = new CLRSemantics();
- ToplevelTraverser translator = new ToplevelTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));
+ MetadataTraverser translator = new MetadataTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));
assembly = module as IAssembly;
if (assembly != null)
translator.Visit(assembly);
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index 5ebaea37..af053d2d 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -24,20 +24,20 @@ namespace BytecodeTranslator public readonly TraverserFactory factory;
- public readonly MethodTraverser MethodTraverser;
+ public readonly MetadataTraverser MetadataTraverser;
public readonly Bpl.Variable HeapVariable;
public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();
#region Constructors
- public StatementTraverser(TraverserFactory factory, MethodTraverser mt) :
+ public StatementTraverser(TraverserFactory factory, MetadataTraverser mt) :
this(factory, mt, mt.HeapVariable) { }
- public StatementTraverser(TraverserFactory factory, MethodTraverser mt, Bpl.Variable heapvar) {
+ public StatementTraverser(TraverserFactory factory, MetadataTraverser mt, Bpl.Variable heapvar) {
this.factory = factory;
HeapVariable = heapvar;
- MethodTraverser = mt;
+ MetadataTraverser = mt;
}
#endregion
@@ -84,8 +84,8 @@ namespace BytecodeTranslator /// <remarks>(mschaef) Works, but still a stub</remarks>
/// <param name="conditionalStatement"></param>
public override void Visit(IConditionalStatement conditionalStatement) {
- StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.MethodTraverser, this.HeapVariable);
- StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.MethodTraverser, this.HeapVariable);
+ StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.MetadataTraverser, this.HeapVariable);
+ StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.MetadataTraverser, this.HeapVariable);
ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this, this.HeapVariable);
condTraverser.Visit(conditionalStatement.Condition);
@@ -129,7 +129,7 @@ namespace BytecodeTranslator /// </summary>
public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {
if (localDeclarationStatement.InitialValue == null) return;
- var loc = this.MethodTraverser.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);
+ var loc = this.MetadataTraverser.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);
var tok = TokenFor(localDeclarationStatement);
var e = ExpressionFor(localDeclarationStatement.InitialValue);
StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, loc), e));
@@ -145,7 +145,7 @@ namespace BytecodeTranslator Bpl.IToken tok = TokenFor(returnStatement);
#region Copy values of all out parameters to outvariables
- foreach (MethodTraverser.MethodParameter mp in MethodTraverser.OutVars) {
+ foreach (MetadataTraverser.MethodParameter mp in this.MetadataTraverser.OutVars) {
StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
new Bpl.IdentifierExpr(tok, mp.outParameterCopy), new Bpl.IdentifierExpr(tok, mp.localParameter)));
}
@@ -155,12 +155,12 @@ namespace BytecodeTranslator ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this, this.HeapVariable);
etrav.Visit(returnStatement.Expression);
- if (this.MethodTraverser.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {
+ if (this.MetadataTraverser.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {
throw new TranslationException(String.Format("{0} returns a value that is not supported by the function", returnStatement.ToString()));
}
StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
- new Bpl.IdentifierExpr(tok, this.MethodTraverser.RetVariable), etrav.TranslatedExpressions.Pop()));
+ new Bpl.IdentifierExpr(tok, this.MetadataTraverser.RetVariable), etrav.TranslatedExpressions.Pop()));
}
StmtBuilder.Add(new Bpl.ReturnCmd(TokenFor(returnStatement)));
}
diff --git a/BCT/BytecodeTranslator/ToplevelTraverser.cs b/BCT/BytecodeTranslator/ToplevelTraverser.cs deleted file mode 100644 index 0ba7bffa..00000000 --- a/BCT/BytecodeTranslator/ToplevelTraverser.cs +++ /dev/null @@ -1,82 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-using Microsoft.Cci;
-using Microsoft.Cci.MetadataReader;
-using Microsoft.Cci.MutableCodeModel;
-using Microsoft.Cci.Contracts;
-using Microsoft.Cci.ILToCodeModel;
-
-using Bpl = Microsoft.Boogie;
-
-
-namespace BytecodeTranslator {
- /// <summary>
- ///
- /// </summary>
- public class ToplevelTraverser : BaseCodeAndContractTraverser {
-
- public readonly TraverserFactory factory;
-
- public readonly IContractProvider ContractProvider;
-
- public readonly Bpl.Program TranslatedProgram;
-
- private Dictionary<ITypeDefinition, ClassTraverser> classMap = new Dictionary<ITypeDefinition, ClassTraverser>();
-
- public ToplevelTraverser(TraverserFactory factory, IContractProvider cp)
- : base(cp) {
- this.factory = factory;
- ContractProvider = cp;
- TranslatedProgram = new Bpl.Program();
- }
-
- public Bpl.Variable FindOrCreateClassField(ITypeDefinition classtype, IFieldDefinition field) {
- ClassTraverser ct;
- if (!classMap.TryGetValue(classtype, out ct)) {
- ct = this.factory.MakeClassTraverser(this, this.contractProvider);
- classMap.Add(classtype, ct);
- return ct.FindOrCreateFieldVariable(field);
- } else {
- return ct.FindOrCreateFieldVariable(field);
- }
- }
-
-
- /// <summary>
- ///
- /// </summary>
- /// <param name="typeDefinition"></param>
- public override void Visit(ITypeDefinition typeDefinition) {
- if (typeDefinition.IsClass) {
-
- ClassTraverser ct;
- if (!classMap.TryGetValue(typeDefinition, out ct)) {
- ct = this.factory.MakeClassTraverser(this, this.contractProvider);
- classMap.Add(typeDefinition, ct);
- }
- ct.Visit(typeDefinition);
- } else {
- Console.WriteLine("Non-Class {0} was found", typeDefinition);
- throw new NotImplementedException(String.Format("Non-Class Type {0} is not yet supported.", typeDefinition.ToString()));
- }
- }
-
- public override void Visit(IModule module) {
- base.Visit(module);
- }
-
- public override void Visit(IAssembly assembly) {
- base.Visit(assembly);
- }
-
- }
-
-}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index cacc9817..9f79b034 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -18,10 +18,8 @@ using Bpl = Microsoft.Boogie; namespace BytecodeTranslator {
public abstract class TraverserFactory {
- public virtual ToplevelTraverser MakeTopLevelTraverser(IContractProvider contractProvider) { return new ToplevelTraverser(this, contractProvider); }
- public virtual ClassTraverser MakeClassTraverser(ToplevelTraverser parent, IContractProvider contractProvider) { return new ClassTraverser(this, contractProvider, parent); }
- public virtual MethodTraverser MakeMethodTraverser(ClassTraverser parent, IContractProvider contractProvider) { return new MethodTraverser(this, contractProvider, parent); }
- public virtual StatementTraverser MakeStatementTraverser(MethodTraverser parent, Bpl.Variable heapVariable) { return new StatementTraverser(this, parent, heapVariable); }
+ public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider) { return new MetadataTraverser(this, contractProvider); }
+ public virtual StatementTraverser MakeStatementTraverser(MetadataTraverser parent, Bpl.Variable heapVariable) { return new StatementTraverser(this, parent, heapVariable); }
public virtual ExpressionTraverser MakeExpressionTraverser(StatementTraverser parent, Bpl.Variable heapVariable) { return new ExpressionTraverser(parent, heapVariable); }
}
}
\ No newline at end of file diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs index a018797d..ed1be53a 100644 --- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs +++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs @@ -84,7 +84,7 @@ namespace TranslationTest { #region Pass 3: Translate the code model to BPL
var factory = new CLRSemantics();
- ToplevelTraverser translator = new ToplevelTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));
+ MetadataTraverser translator = new MetadataTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));
assembly = module as IAssembly;
if (assembly != null)
translator.Visit(assembly);
|