From 8690616ba7f82cb2b0897752a90e3fa681e2064a Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 30 Jun 2010 03:00:10 +0000 Subject: Forgotten file. --- BCT/BytecodeTranslator/MetadataTraverser.cs | 401 ++++++++++++++++++++++++++++ 1 file changed, 401 insertions(+) create mode 100644 BCT/BytecodeTranslator/MetadataTraverser.cs (limited to 'BCT') diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs new file mode 100644 index 00000000..661e240f --- /dev/null +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -0,0 +1,401 @@ +//----------------------------------------------------------------------------- +// +// 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 { + + /// + /// Responsible for traversing all metadata elements (i.e., everything exclusive + /// of method bodies). + /// + public class MetadataTraverser : BaseMetadataTraverser { + + public readonly TraverserFactory factory; + + public readonly IContractProvider ContractProvider; + + public readonly Bpl.Program TranslatedProgram; + + public Bpl.Variable HeapVariable; + + private Dictionary fieldVarMap = null; + + public MetadataTraverser(TraverserFactory factory, IContractProvider cp) + : base() { + this.factory = factory; + ContractProvider = cp; + TranslatedProgram = new Bpl.Program(); + } + + 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); + this.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Constant(tok, tident, true)); + } + return v; + } + + public class MethodParameter { + public MethodParameter() { + localParameter = null; + inParameterCopy = null; + outParameterCopy = null; + } + + public Bpl.Formal localParameter; + public Bpl.Formal inParameterCopy; + public Bpl.Formal outParameterCopy; + } + + #region Method Helpers + /// + /// + /// + /// + /// + 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; + } + + /// + /// Creates a fresh local var of the given Type and adds it to the + /// Bpl Implementation + /// + /// The type of the new variable + /// A fresh Variable with automatic generated name and location + 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; + } + + /// + /// + /// + /// + /// (mschaef) only a stub + 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; + } + + /// + /// + /// + /// + /// STUB + /// + public Bpl.Variable FindParameterVariable(IParameterDefinition param) { + MethodParameter mp; + formalMap.TryGetValue(param, out mp); + return mp.localParameter; + } + #endregion Method Helpers + + #region Overrides + + public override void Visit(IModule module) { + base.Visit(module); + } + + public override void Visit(IAssembly assembly) { + base.Visit(assembly); + } + + /// + /// Visits only classes: throws an exception for all other type definitions. + /// + /// + + #region Local state for each type + // TODO: (mschaef) just a stub + public readonly Bpl.Variable ThisVariable = TranslationHelper.TempThisVar(); + #endregion + + public override void Visit(ITypeDefinition typeDefinition) { + + var savedFieldVarMap = this.fieldVarMap; + this.fieldVarMap = new Dictionary(); + + if (typeDefinition.IsClass) { + + base.Visit(typeDefinition); + this.fieldVarMap = savedFieldVarMap; + + } else { + Console.WriteLine("Non-Class {0} was found", typeDefinition); + throw new NotImplementedException(String.Format("Non-Class Type {0} is not yet supported.", typeDefinition.ToString())); + } + } + + #region Local state for each method + + private Dictionary formalMap = null; + internal Bpl.Variable RetVariable; + internal List OutVars = new List(); + private Dictionary localVarMap = null; + + #endregion + + /// + /// + /// + public override void Visit(IMethodDefinition method) { + + formalMap = new Dictionary(); + localVarMap = new Dictionary(); + + 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); + + this.TranslatedProgram.TopLevelDeclarations.Add(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; + this.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 + } + } + + public override void Visit(IFieldDefinition fieldDefinition) { + this.FindOrCreateFieldVariable(fieldDefinition); + } + + #endregion + + } +} \ No newline at end of file -- cgit v1.2.3