diff options
18 files changed, 531 insertions, 73 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj index ff49e4c3..3ddd4e43 100644 --- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj +++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj @@ -121,6 +121,8 @@ <Reference Include="System.Xml" />
</ItemGroup>
<ItemGroup>
+ <Compile Include="TranslationPlugins\PhoneTranslator\PhoneFeedbackPlugin.cs" />
+ <Compile Include="TranslationPlugins\Translators\BaseTranslator.cs" />
<Compile Include="CLRSemantics.cs" />
<Compile Include="Heap.cs" />
<Compile Include="HeapFactory.cs" />
@@ -139,9 +141,12 @@ <Compile Include="TranslationException.cs" />
<Compile Include="TranslationHelper.cs" />
<Compile Include="TranslationPlugins\BytecodeTranslator\BytecodeTranslatorPlugin.cs" />
- <Compile Include="TranslationPlugins\IContractAwareTranslator.cs" />
+ <Compile Include="TranslationPlugins\ContractAwareTranslator.cs" />
<Compile Include="TranslationPlugins\ITranslationPlugin.cs" />
- <Compile Include="TranslationPlugins\ITranslator.cs" />
+ <Compile Include="TranslationPlugins\PhoneTranslator\PhoneInitializationPlugin.cs" />
+ <Compile Include="TranslationPlugins\Translator.cs" />
+ <Compile Include="TranslationPlugins\Translators\PhoneFeedbackTranslator.cs" />
+ <Compile Include="TranslationPlugins\Translators\PhoneInitializationTranslator.cs" />
<Compile Include="TraverserFactory.cs" />
<Compile Include="WholeProgram.cs" />
</ItemGroup>
diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs index 55f0cd46..ddf85c6f 100644 --- a/BCT/BytecodeTranslator/CLRSemantics.cs +++ b/BCT/BytecodeTranslator/CLRSemantics.cs @@ -15,11 +15,17 @@ using Microsoft.Cci.Contracts; using Microsoft.Cci.ILToCodeModel;
using Bpl = Microsoft.Boogie;
+using BytecodeTranslator.TranslationPlugins;
namespace BytecodeTranslator {
public class CLRSemantics : TraverserFactory {
+ public override Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
+ Translator translator = new BaseTranslator(this, sink, contractProviders, pdbReaders);
+ return translator;
+ }
+
public override ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {
return new CLRExpressionSemantics(sink, statementTraverser, contractContext);
}
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index ff2c6095..fcbc4e99 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -69,6 +69,7 @@ namespace BytecodeTranslator { public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
string fieldname = MemberHelper.GetMemberSignature(field, NameFormattingOptions.DocumentationId);
+
fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
Bpl.IToken tok = field.Token();
Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType);
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index e4a81eb8..124726e6 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -27,22 +27,65 @@ namespace BytecodeTranslator { /// Responsible for traversing all metadata elements (i.e., everything exclusive
/// of method bodies).
/// </summary>
- public class MetadataTraverser : BaseMetadataTraverser, ITranslator {
+ public class MetadataTraverser : BaseMetadataTraverser {
readonly Sink sink;
-
- public readonly TraverserFactory factory;
+ public readonly TraverserFactory Factory;
public readonly IDictionary<IUnit, PdbReader> PdbReaders;
public PdbReader/*?*/ PdbReader;
- public MetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)
+ public MetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders, TraverserFactory factory)
: base() {
this.sink = sink;
- this.factory = sink.Factory;
+ this.Factory = factory;
this.PdbReaders = pdbReaders;
}
+ public IEnumerable<Bpl.Requires> getPreconditionTranslation(IMethodContract contract) {
+ ICollection<Bpl.Requires> translatedPres = new List<Bpl.Requires>();
+ foreach (IPrecondition pre in contract.Preconditions) {
+ var stmtTraverser = this.Factory.MakeStatementTraverser(sink, null, true);
+ ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, stmtTraverser, true);
+ exptravers.Visit(pre.Condition); // TODO
+ // Todo: Deal with Descriptions
+ var req = new Bpl.Requires(pre.Token(), false, exptravers.TranslatedExpressions.Pop(), "");
+ translatedPres.Add(req);
+ }
+
+ return translatedPres;
+ }
+
+ public IEnumerable<Bpl.Ensures> getPostconditionTranslation(IMethodContract contract) {
+ ICollection<Bpl.Ensures> translatedPosts = new List<Bpl.Ensures>();
+ foreach (IPostcondition post in contract.Postconditions) {
+ var stmtTraverser = this.Factory.MakeStatementTraverser(sink, null, true);
+ ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, stmtTraverser, true);
+ exptravers.Visit(post.Condition);
+ // Todo: Deal with Descriptions
+ var ens = new Bpl.Ensures(post.Token(), false, exptravers.TranslatedExpressions.Pop(), "");
+ translatedPosts.Add(ens);
+ }
+
+ return translatedPosts;
+ }
+
+ public IEnumerable<Bpl.IdentifierExpr> getModifiedIdentifiers(IMethodContract contract) {
+ ICollection<Bpl.IdentifierExpr> modifiedExpr = new List<Bpl.IdentifierExpr>();
+ foreach (IAddressableExpression mod in contract.ModifiedVariables) {
+ ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, null, true);
+ 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()));
+ }
+ modifiedExpr.Add(idexp);
+ }
+
+ return modifiedExpr;
+ }
+
+
#region Overrides
public override void Visit(IModule module) {
@@ -136,7 +179,7 @@ namespace BytecodeTranslator { if (PhoneCodeHelper.instance().PhonePlugin != null && typeDef.isPhoneApplicationPageClass(sink.host)) {
IEnumerable<ControlInfoStructure> pageCtrls= PhoneCodeHelper.instance().PhonePlugin.getControlsForPage(typeDef.ToString());
foreach (ControlInfoStructure ctrlInfo in pageCtrls) {
- if (ctrlInfo.Name.Contains(PhoneControlsPlugin.BOOGIE_DUMMY_CONTROL)) {
+ if (ctrlInfo.Name.Contains(PhoneControlsPlugin.BOOGIE_DUMMY_CONTROL) || ctrlInfo.Name == Dummy.Name.Value) {
string anonymousControlName = ctrlInfo.Name;
IFieldDefinition fieldDef = new FieldDefinition() {
ContainingTypeDefinition = typeDef,
@@ -152,7 +195,7 @@ namespace BytecodeTranslator { }
}
}
- * */
+ */
private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) {
Contract.Requires(typeDefinition.IsStruct);
@@ -160,7 +203,7 @@ namespace BytecodeTranslator { var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typeDefinition);
this.sink.BeginMethod(typeDefinition);
- var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
+ var stmtTranslator = this.Factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
var stmts = new List<IStatement>();
foreach (var f in typeDefinition.Fields) {
@@ -263,7 +306,7 @@ namespace BytecodeTranslator { this.sink.BeginMethod(typeDefinition);
- var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
+ var stmtTranslator = this.Factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
var stmts = new List<IStatement>();
foreach (var f in typeDefinition.Fields) {
@@ -343,7 +386,7 @@ namespace BytecodeTranslator { }
try {
- StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
+ StatementTraverser stmtTraverser = this.Factory.MakeStatementTraverser(this.sink, this.PdbReader, false);
// FEEDBACK if this is a feedback method it will be plagued with false asserts. They will trigger if $Exception becomes other than null
// FEEDBACK for modular analysis we need it to be non-null at the start
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index fc48f4c7..3a89a3da 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -23,6 +23,7 @@ using BytecodeTranslator.Phone; using System.Text.RegularExpressions;
using BytecodeTranslator.TranslationPlugins;
using BytecodeTranslator.TranslationPlugins.BytecodeTranslator;
+using BytecodeTranslator.TranslationPlugins.PhoneTranslator;
namespace BytecodeTranslator {
@@ -255,23 +256,52 @@ namespace BytecodeTranslator { }
var primaryModule = modules[0];
- TraverserFactory bctTraverserFactory;
- if (wholeProgram) {
- bctTraverserFactory = new WholeProgram();
- } else {
- bctTraverserFactory = new CLRSemantics();
- }
-
- Sink sink= new Sink(host, bctTraverserFactory, heapFactory, options, exemptionList, whiteList);
+ Sink sink= new Sink(host, heapFactory, options, exemptionList, whiteList);
TranslationHelper.tmpVarCounter = 0;
- ITranslationPlugin bctPlugin= new BytecodeTranslatorPlugin();
- ITranslator translator= bctPlugin.getTranslator(sink, contractExtractors, pdbReaders);
+ // TODO move away, get all plugin and translators from a config file or alike
+ #region Plugged translators
+ List<Translator> translatorsPlugged = new List<Translator>();
+ ITranslationPlugin bctPlugin= new BytecodeTranslatorPlugin(wholeProgram);
+ Translator bcTranslator = bctPlugin.getTranslator(sink, contractExtractors, pdbReaders);
+ translatorsPlugged.Add(bcTranslator);
if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
+ // TODO this should be part of the translator initialziation
+ PhoneCodeHelper.initialize(host);
+ PhoneCodeHelper.instance().PhonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);
+
+ if (doPhoneNav) {
+ // TODO this should be part of the translator initialziation
+ PhoneCodeHelper.instance().PhoneNavigationToggled = true;
+
+ ITranslationPlugin phoneInitPlugin = new PhoneInitializationPlugin();
+ ITranslationPlugin phoneNavPlugin = new PhoneNavigationPlugin();
+ Translator phInitTranslator = phoneInitPlugin.getTranslator(sink, contractExtractors, pdbReaders);
+ Translator phNavTranslator = phoneNavPlugin.getTranslator(sink, contractExtractors, pdbReaders);
+ translatorsPlugged.Add(phInitTranslator);
+ translatorsPlugged.Add(phNavTranslator);
+ }
+
+ if (doPhoneFeedback) {
+ // TODO this should be part of the translator initialziation
+ PhoneCodeHelper.instance().PhoneFeedbackToggled = true;
+
+ ITranslationPlugin phoneFeedbackPlugin = new PhoneFeedbackPlugin();
+ Translator phFeedbackTranslator = phoneFeedbackPlugin.getTranslator(sink, contractExtractors, pdbReaders);
+ translatorsPlugged.Add(phFeedbackTranslator);
+ }
+ }
+ #endregion
+ sink.TranslationPlugins = translatorsPlugged;
+
+ /*
+ if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
+ // TODO send this all way to initialization of phone plugin translator
PhoneCodeHelper.initialize(host);
PhoneCodeHelper.instance().PhonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);
+ // TODO these parameters will eventually form part of plugin configuration
if (doPhoneNav) {
PhoneCodeHelper.instance().PhoneNavigationToggled = true;
PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host);
@@ -286,8 +316,17 @@ namespace BytecodeTranslator { fbMetaDataTraverser.Visit(modules);
}
}
-
- translator.TranslateAssemblies(modules);
+ */
+
+ // TODO replace the whole translation by a translator initialization and an orchestrator calling back for each element
+ // TODO for the current BC translator it will possibly just implement onMetadataElement(IModule)
+ // TODO refactor this away, handle priorities between plugged translators
+ IOrderedEnumerable<Translator> prioritizedTranslators = translatorsPlugged.OrderBy(t => t.getPriority());
+ foreach (Translator t in prioritizedTranslators) {
+ t.initialize();
+ if (t.isOneShot())
+ t.TranslateAssemblies(modules);
+ }
foreach (var pair in sink.delegateTypeToDelegates.Values) {
CreateDispatchMethod(sink, pair.Item1, pair.Item2);
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index ea0b22c9..ea6e0878 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -17,27 +17,27 @@ using Microsoft.Cci.ILToCodeModel; using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
+using BytecodeTranslator.TranslationPlugins;
namespace BytecodeTranslator {
public class Sink {
- public TraverserFactory Factory {
- get { return this.factory; }
+ public IEnumerable<Translator> TranslationPlugins {
+ get { return this.translationPlugins; }
+ set { this.translationPlugins= value; }
}
- readonly TraverserFactory factory;
+ private IEnumerable<Translator> translationPlugins;
private readonly Options options;
readonly bool whiteList;
readonly List<Regex> exemptionList;
- public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
+
+ public Sink(IContractAwareHost host, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Contract.Requires(host != null);
- Contract.Requires(factory != null);
Contract.Requires(heapFactory != null);
-
this.host = host;
- this.factory = factory;
var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?
this.options = options;
this.exemptionList = exemptionList;
@@ -630,35 +630,24 @@ namespace BytecodeTranslator { if (contract != null) {
try {
-
- foreach (IPrecondition pre in contract.Preconditions) {
- var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true);
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, stmtTraverser, true);
- exptravers.Visit(pre.Condition); // TODO
- // Todo: Deal with Descriptions
- var req = new Bpl.Requires(pre.Token(), false, exptravers.TranslatedExpressions.Pop(), "");
- boogiePrecondition.Add(req);
- }
-
- foreach (IPostcondition post in contract.Postconditions) {
- var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true);
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, stmtTraverser, true);
- exptravers.Visit(post.Condition);
- // Todo: Deal with Descriptions
- var ens = new Bpl.Ensures(post.Token(), false, exptravers.TranslatedExpressions.Pop(), "");
- boogiePostcondition.Add(ens);
- }
-
- foreach (IAddressableExpression mod in contract.ModifiedVariables) {
- ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, null, true);
- 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()));
+ foreach (Translator translatorPlugin in translationPlugins) {
+ ContractAwareTranslator translator = translatorPlugin as ContractAwareTranslator;
+ if (translator != null) {
+ IEnumerable<Bpl.Requires> preConds = translator.getPreconditionTranslation(contract);
+ foreach (Bpl.Requires preExpr in preConds) {
+ boogiePrecondition.Add(preExpr);
+ }
+
+ IEnumerable<Bpl.Ensures> ensures = translator.getPostconditionTranslation(contract);
+ foreach (Bpl.Ensures ensuring in ensures) {
+ boogiePostcondition.Add(ensuring);
+ }
+
+ IEnumerable<Bpl.IdentifierExpr> modifiedExpr = translator.getModifiedIdentifiers(contract);
+ foreach (Bpl.IdentifierExpr ident in modifiedExpr) {
+ boogieModifies.Add(ident);
+ }
}
- boogieModifies.Add(idexp);
}
}
catch (TranslationException te) {
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs index b6fc1dfd..40bc14b3 100644 --- a/BCT/BytecodeTranslator/StatementTraverser.cs +++ b/BCT/BytecodeTranslator/StatementTraverser.cs @@ -58,9 +58,9 @@ namespace BytecodeTranslator private static int captureStateCounter = 0;
#region Constructors
- public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
+ public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, TraverserFactory factory) {
this.sink = sink;
- this.factory = sink.Factory;
+ this.factory = factory;
PdbReader = pdbReader;
this.contractContext = contractContext;
this.captureState = sink.Options.captureState;
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs index 425a9476..a7b00f63 100644 --- a/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs +++ b/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs @@ -6,11 +6,22 @@ using Microsoft.Cci; using Microsoft.Cci.Contracts;
namespace BytecodeTranslator.TranslationPlugins.BytecodeTranslator {
- class BytecodeTranslatorPlugin : ITranslationPlugin {
- public ITranslator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
- // TODO take whole program options into account here
- return new CLRSemantics().MakeMetadataTraverser(sink, contractProviders, pdbReaders);
- // return new WholeProgram().MakeMetadataTraverser(sink, contractProviders, pdbReaders);
+ internal class BytecodeTranslatorPlugin : ITranslationPlugin {
+ private bool isWholeProgram = false;
+
+ public BytecodeTranslatorPlugin(Boolean isWholeProgram) {
+ this.isWholeProgram = isWholeProgram;
+ }
+
+ public Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
+ TraverserFactory factory;
+ if (isWholeProgram)
+ factory= new WholeProgram();
+ else
+ factory= new CLRSemantics();
+ // Translator translator= factory.MakeMetadataTraverser(sink, contractProviders, pdbReaders);
+ Translator translator= factory.getTranslator(sink, contractProviders, pdbReaders);
+ return translator;
}
}
}
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/ContractAwareTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/ContractAwareTranslator.cs new file mode 100644 index 00000000..ceb8ca0a --- /dev/null +++ b/BCT/BytecodeTranslator/TranslationPlugins/ContractAwareTranslator.cs @@ -0,0 +1,15 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using Bpl= Microsoft.Boogie;
+using Microsoft.Cci.Contracts;
+
+namespace BytecodeTranslator.TranslationPlugins {
+ public abstract class ContractAwareTranslator : Translator {
+ public virtual IEnumerable<Bpl.Requires> getPreconditionTranslation(IMethodContract contract) {return new List<Bpl.Requires>(); }
+ public virtual IEnumerable<Bpl.Ensures> getPostconditionTranslation(IMethodContract contract) { return new List<Bpl.Ensures>(); }
+ public virtual IEnumerable<Bpl.IdentifierExpr> getModifiedIdentifiers(IMethodContract contract) { return new List<Bpl.IdentifierExpr>(); }
+ }
+}
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/ITranslationPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/ITranslationPlugin.cs index c6157e49..9cf895fd 100644 --- a/BCT/BytecodeTranslator/TranslationPlugins/ITranslationPlugin.cs +++ b/BCT/BytecodeTranslator/TranslationPlugins/ITranslationPlugin.cs @@ -6,7 +6,7 @@ using Microsoft.Cci; using Microsoft.Cci.Contracts;
namespace BytecodeTranslator.TranslationPlugins {
- interface ITranslationPlugin {
- ITranslator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractExtractors=null, IDictionary<IUnit, PdbReader> pdbReaders=null);
+ public interface ITranslationPlugin {
+ Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractExtractors=null, IDictionary<IUnit, PdbReader> pdbReaders=null);
}
}
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs new file mode 100644 index 00000000..c6d9b24a --- /dev/null +++ b/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs @@ -0,0 +1,15 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Cci;
+using Microsoft.Cci.Contracts;
+using BytecodeTranslator.TranslationPlugins.Translators;
+
+namespace BytecodeTranslator.TranslationPlugins.PhoneTranslator {
+ class PhoneFeedbackPlugin : ITranslationPlugin {
+ public Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
+ return new PhoneFeedbackTranslator(sink);
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs new file mode 100644 index 00000000..98282faa --- /dev/null +++ b/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs @@ -0,0 +1,21 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Cci;
+using Microsoft.Cci.Contracts;
+using BytecodeTranslator.TranslationPlugins.Translators;
+
+namespace BytecodeTranslator.TranslationPlugins.PhoneTranslator {
+ class PhoneInitializationPlugin : ITranslationPlugin {
+ public Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
+ return new PhoneInitializationTranslator(sink);
+ }
+ }
+
+ class PhoneNavigationPlugin : ITranslationPlugin {
+ public Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
+ return new PhoneNavigationTranslator(sink);
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translator.cs new file mode 100644 index 00000000..60d7e2f6 --- /dev/null +++ b/BCT/BytecodeTranslator/TranslationPlugins/Translator.cs @@ -0,0 +1,169 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Cci;
+
+namespace BytecodeTranslator.TranslationPlugins {
+ public abstract class Translator {
+ public abstract void initialize();
+ public abstract bool isOneShot();
+ public abstract int getPriority();
+
+ public virtual void TranslateAssemblies(IEnumerable<IUnit> assemblies) { }
+
+ // Each plugged translator may choose to implement some action on each metadata / AST element
+ public virtual void onMetadataElement(IArrayTypeReference arrayTypeReference) { }
+ public virtual void onMetadataElement(IAssembly assembly) { }
+ public virtual void onMetadataElement(IAssemblyReference assemblyReference) { }
+ public virtual void onMetadataElement(ICustomAttribute customAttribute) { }
+ public virtual void onMetadataElement(ICustomModifier customModifier) { }
+ public virtual void onMetadataElement(IEventDefinition eventDefinition) { }
+ public virtual void onMetadataElement(IFieldDefinition fieldDefinition) { }
+ public virtual void onMetadataElement(IFieldReference fieldReference) { }
+ public virtual void onMetadataElement(IFileReference fileReference) { }
+ public virtual void onMetadataElement(IFunctionPointerTypeReference functionPointerTypeReference) { }
+ public virtual void onMetadataElement(IGenericMethodInstanceReference genericMethodInstanceReference) { }
+ public virtual void onMetadataElement(IGenericMethodParameter genericMethodParameter) { }
+ public virtual void onMetadataElement(IGenericMethodParameterReference genericMethodParameterReference) { }
+ public virtual void onMetadataElement(IGlobalFieldDefinition globalFieldDefinition) { }
+ public virtual void onMetadataElement(IGlobalMethodDefinition globalMethodDefinition) { }
+ public virtual void onMetadataElement(IGenericTypeInstanceReference genericTypeInstanceReference) { }
+ public virtual void onMetadataElement(IGenericTypeParameter genericTypeParameter) { }
+ public virtual void onMetadataElement(IGenericTypeParameterReference genericTypeParameterReference) { }
+ public virtual void onMetadataElement(ILocalDefinition localDefinition) { }
+ public virtual void onMetadataElement(IManagedPointerTypeReference managedPointerTypeReference) { }
+ public virtual void onMetadataElement(IMarshallingInformation marshallingInformation) { }
+ public virtual void onMetadataElement(IMetadataConstant constant) { }
+ public virtual void onMetadataElement(IMetadataCreateArray createArray) { }
+ public virtual void onMetadataElement(IMetadataExpression expression) { }
+ public virtual void onMetadataElement(IMetadataNamedArgument namedArgument) { }
+ public virtual void onMetadataElement(IMetadataTypeOf typeOf) { }
+ public virtual void onMetadataElement(IMethodBody methodBody) { }
+ public virtual void onMetadataElement(IMethodDefinition method) { }
+ public virtual void onMetadataElement(IMethodImplementation methodImplementation) { }
+ public virtual void onMetadataElement(IMethodReference methodReference) { }
+ public virtual void onMetadataElement(IModifiedTypeReference modifiedTypeReference) { }
+ public virtual void onMetadataElement(IModule module) { }
+ public virtual void onMetadataElement(IModuleReference moduleReference) { }
+ public virtual void onMetadataElement(INamespaceAliasForType namespaceAliasForType) { }
+ public virtual void onMetadataElement(INamespaceTypeDefinition namespaceTypeDefinition) { }
+ public virtual void onMetadataElement(INamespaceTypeReference namespaceTypeReference) { }
+ public virtual void onMetadataElement(INestedAliasForType nestedAliasForType) { }
+ public virtual void onMetadataElement(INestedTypeDefinition nestedTypeDefinition) { }
+ public virtual void onMetadataElement(INestedTypeReference nestedTypeReference) { }
+ public virtual void onMetadataElement(INestedUnitNamespace nestedUnitNamespace) { }
+ public virtual void onMetadataElement(INestedUnitNamespaceReference nestedUnitNamespaceReference) { }
+ public virtual void onMetadataElement(INestedUnitSetNamespace nestedUnitSetNamespace) { }
+ public virtual void onMetadataElement(IOperation operation) { }
+ public virtual void onMetadataElement(IOperationExceptionInformation operationExceptionInformation) { }
+ public virtual void onMetadataElement(IParameterDefinition parameterDefinition) { }
+ public virtual void onMetadataElement(IParameterTypeInformation parameterTypeInformation) { }
+ public virtual void onMetadataElement(IPESection peSection) { }
+ public virtual void onMetadataElement(IPlatformInvokeInformation platformInvokeInformation) { }
+ public virtual void onMetadataElement(IPointerTypeReference pointerTypeReference) { }
+ public virtual void onMetadataElement(IPropertyDefinition propertyDefinition) { }
+ public virtual void onMetadataElement(IResourceReference resourceReference) { }
+ public virtual void onMetadataElement(IRootUnitNamespace rootUnitNamespace) { }
+ public virtual void onMetadataElement(IRootUnitNamespaceReference rootUnitNamespaceReference) { }
+ public virtual void onMetadataElement(IRootUnitSetNamespace rootUnitSetNamespace) { }
+ public virtual void onMetadataElement(ISecurityAttribute securityAttribute) { }
+ public virtual void onMetadataElement(ISpecializedEventDefinition specializedEventDefinition) { }
+ public virtual void onMetadataElement(ISpecializedFieldDefinition specializedFieldDefinition) { }
+ public virtual void onMetadataElement(ISpecializedFieldReference specializedFieldReference) { }
+ public virtual void onMetadataElement(ISpecializedMethodDefinition specializedMethodDefinition) { }
+ public virtual void onMetadataElement(ISpecializedMethodReference specializedMethodReference) { }
+ public virtual void onMetadataElement(ISpecializedPropertyDefinition specializedPropertyDefinition) { }
+ public virtual void onMetadataElement(ISpecializedNestedTypeDefinition specializedNestedTypeDefinition) { }
+ public virtual void onMetadataElement(ISpecializedNestedTypeReference specializedNestedTypeReference) { }
+ public virtual void onMetadataElement(IUnitSet unitSet) { }
+ public virtual void onMetadataElement(IWin32Resource win32Resource) { }
+
+ public virtual void onASTElement(IAddition addition) { }
+ public virtual void onASTElement(IAddressableExpression addressableExpression) { }
+ public virtual void onASTElement(IAddressDereference addressDereference) { }
+ public virtual void onASTElement(IAddressOf addressOf) { }
+ public virtual void onASTElement(IAnonymousDelegate anonymousDelegate) { }
+ public virtual void onASTElement(IArrayIndexer arrayIndexer) { }
+ public virtual void onASTElement(IAssertStatement assertStatement) { }
+ public virtual void onASTElement(IAssignment assignment) { }
+ public virtual void onASTElement(IAssumeStatement assumeStatement) { }
+ public virtual void onASTElement(IBitwiseAnd bitwiseAnd) { }
+ public virtual void onASTElement(IBitwiseOr bitwiseOr) { }
+ public virtual void onASTElement(IBlockExpression blockExpression) { }
+ public virtual void onASTElement(IBlockStatement block) { }
+ public virtual void onASTElement(IBreakStatement breakStatement) { }
+ public virtual void onASTElement(IBoundExpression boundExpression) { }
+ public virtual void onASTElement(ICastIfPossible castIfPossible) { }
+ public virtual void onASTElement(ICatchClause catchClause) { }
+ public virtual void onASTElement(ICheckIfInstance checkIfInstance) { }
+ public virtual void onASTElement(ICompileTimeConstant constant) { }
+ public virtual void onASTElement(IConversion conversion) { }
+ public virtual void onASTElement(IConditional conditional) { }
+ public virtual void onASTElement(IConditionalStatement conditionalStatement) { }
+ public virtual void onASTElement(IContinueStatement continueStatement) { }
+ public virtual void onASTElement(ICreateArray createArray) { }
+ public virtual void onASTElement(ICreateDelegateInstance createDelegateInstance) { }
+ public virtual void onASTElement(ICreateObjectInstance createObjectInstance) { }
+ public virtual void onASTElement(IDebuggerBreakStatement debuggerBreakStatement) { }
+ public virtual void onASTElement(IDefaultValue defaultValue) { }
+ public virtual void onASTElement(IDivision division) { }
+ public virtual void onASTElement(IDoUntilStatement doUntilStatement) { }
+ public virtual void onASTElement(IDupValue dupValue) { }
+ public virtual void onASTElement(IEmptyStatement emptyStatement) { }
+ public virtual void onASTElement(IEquality equality) { }
+ public virtual void onASTElement(IExclusiveOr exclusiveOr) { }
+ public virtual void onASTElement(IExpressionStatement expressionStatement) { }
+ public virtual void onASTElement(IForEachStatement forEachStatement) { }
+ public virtual void onASTElement(IForStatement forStatement) { }
+ public virtual void onASTElement(IGotoStatement gotoStatement) { }
+ public virtual void onASTElement(IGotoSwitchCaseStatement gotoSwitchCaseStatement) { }
+ public virtual void onASTElement(IGetTypeOfTypedReference getTypeOfTypedReference) { }
+ public virtual void onASTElement(IGetValueOfTypedReference getValueOfTypedReference) { }
+ public virtual void onASTElement(IGreaterThan greaterThan) { }
+ public virtual void onASTElement(IGreaterThanOrEqual greaterThanOrEqual) { }
+ public virtual void onASTElement(ILabeledStatement labeledStatement) { }
+ public virtual void onASTElement(ILeftShift leftShift) { }
+ public virtual void onASTElement(ILessThan lessThan) { }
+ public virtual void onASTElement(ILessThanOrEqual lessThanOrEqual) { }
+ public virtual void onASTElement(ILocalDeclarationStatement localDeclarationStatement) { }
+ public virtual void onASTElement(ILockStatement lockStatement) { }
+ public virtual void onASTElement(ILogicalNot logicalNot) { }
+ public virtual void onASTElement(IMakeTypedReference makeTypedReference) { }
+ public virtual void onASTElement(IMethodCall methodCall) { }
+ public virtual void onASTElement(IModulus modulus) { }
+ public virtual void onASTElement(IMultiplication multiplication) { }
+ public virtual void onASTElement(INamedArgument namedArgument) { }
+ public virtual void onASTElement(INotEquality notEquality) { }
+ public virtual void onASTElement(IOldValue oldValue) { }
+ public virtual void onASTElement(IOnesComplement onesComplement) { }
+ public virtual void onASTElement(IOutArgument outArgument) { }
+ public virtual void onASTElement(IPointerCall pointerCall) { }
+ public virtual void onASTElement(IPopValue popValue) { }
+ public virtual void onASTElement(IPushStatement pushStatement) { }
+ public virtual void onASTElement(IRefArgument refArgument) { }
+ public virtual void onASTElement(IResourceUseStatement resourceUseStatement) { }
+ public virtual void onASTElement(IReturnValue returnValue) { }
+ public virtual void onASTElement(IRethrowStatement rethrowStatement) { }
+ public virtual void onASTElement(IReturnStatement returnStatement) { }
+ public virtual void onASTElement(IRightShift rightShift) { }
+ public virtual void onASTElement(IRuntimeArgumentHandleExpression runtimeArgumentHandleExpression) { }
+ public virtual void onASTElement(ISizeOf sizeOf) { }
+ public virtual void onASTElement(IStackArrayCreate stackArrayCreate) { }
+ public virtual void onASTElement(ISubtraction subtraction) { }
+ public virtual void onASTElement(ISwitchCase switchCase) { }
+ public virtual void onASTElement(ISwitchStatement switchStatement) { }
+ public virtual void onASTElement(ITargetExpression targetExpression) { }
+ public virtual void onASTElement(IThisReference thisReference) { }
+ public virtual void onASTElement(IThrowStatement throwStatement) { }
+ public virtual void onASTElement(ITryCatchFinallyStatement tryCatchFilterFinallyStatement) { }
+ public virtual void onASTElement(ITokenOf tokenOf) { }
+ public virtual void onASTElement(ITypeOf typeOf) { }
+ public virtual void onASTElement(IUnaryNegation unaryNegation) { }
+ public virtual void onASTElement(IUnaryPlus unaryPlus) { }
+ public virtual void onASTElement(IVectorLength vectorLength) { }
+ public virtual void onASTElement(IWhileDoStatement whileDoStatement) { }
+ public virtual void onASTElement(IYieldBreakStatement yieldBreakStatement) { }
+ public virtual void onASTElement(IYieldReturnStatement yieldReturnStatement) { }
+ }
+}
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs new file mode 100644 index 00000000..60f39e03 --- /dev/null +++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs @@ -0,0 +1,41 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using BytecodeTranslator.TranslationPlugins;
+using Microsoft.Cci;
+using Microsoft.Cci.Contracts;
+
+namespace BytecodeTranslator {
+ class BaseTranslator : ContractAwareTranslator {
+ public TraverserFactory Factory;
+ private Sink sink;
+ private IDictionary<IUnit, IContractProvider> contractProviders;
+ private IDictionary<IUnit, PdbReader> pdbReaders;
+ private MetadataTraverser traverser;
+
+ public BaseTranslator(TraverserFactory factory, Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
+ Factory = factory;
+ this.sink = sink;
+ this.contractProviders = contractProviders;
+ this.pdbReaders = pdbReaders;
+ }
+
+ public override void initialize() {
+ traverser = Factory.MakeMetadataTraverser(sink, contractProviders, pdbReaders);
+ }
+
+ public override bool isOneShot() {
+ return true;
+ }
+
+ public override int getPriority() {
+ // TODO make configurable from outside
+ return 10;
+ }
+
+ public override void TranslateAssemblies(IEnumerable<Microsoft.Cci.IUnit> assemblies) {
+ traverser.TranslateAssemblies(assemblies);
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs new file mode 100644 index 00000000..f2932ac0 --- /dev/null +++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs @@ -0,0 +1,34 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using BytecodeTranslator.Phone;
+using Microsoft.Cci;
+
+namespace BytecodeTranslator.TranslationPlugins.Translators {
+ class PhoneFeedbackTranslator : Translator {
+ private Sink sink;
+ PhoneControlFeedbackMetadataTraverser traverser;
+
+ public PhoneFeedbackTranslator(Sink sink) {
+ this.sink = sink;
+ }
+
+ public override void initialize() {
+ traverser = new PhoneControlFeedbackMetadataTraverser(sink.host as MetadataReaderHost);
+ }
+
+ public override bool isOneShot() {
+ return true;
+ }
+
+ public override int getPriority() {
+ // TODO make configurable from outside
+ return 3;
+ }
+
+ public override void TranslateAssemblies(IEnumerable<Microsoft.Cci.IUnit> assemblies) {
+ traverser.Visit(assemblies);
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs new file mode 100644 index 00000000..7cd35b44 --- /dev/null +++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs @@ -0,0 +1,61 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using BytecodeTranslator.Phone;
+using Microsoft.Cci;
+
+namespace BytecodeTranslator.TranslationPlugins.Translators {
+ class PhoneInitializationTranslator : Translator {
+ private Sink sink;
+ PhoneInitializationMetadataTraverser traverser;
+
+ public PhoneInitializationTranslator(Sink sink) {
+ this.sink = sink;
+ }
+
+ public override void initialize() {
+ traverser = new PhoneInitializationMetadataTraverser(sink.host as MetadataReaderHost);
+ }
+
+ public override bool isOneShot() {
+ return true;
+ }
+
+ public override int getPriority() {
+ // TODO make configurable from outside
+ return 1;
+ }
+
+ public override void TranslateAssemblies(IEnumerable<Microsoft.Cci.IUnit> assemblies) {
+ traverser.InjectPhoneCodeAssemblies(assemblies);
+ }
+ }
+
+ class PhoneNavigationTranslator : Translator {
+ private Sink sink;
+ PhoneNavigationMetadataTraverser traverser;
+
+ public PhoneNavigationTranslator(Sink sink) {
+ this.sink = sink;
+ }
+
+ public override void initialize() {
+ traverser = new PhoneNavigationMetadataTraverser(sink.host as MetadataReaderHost);
+ }
+
+ public override bool isOneShot() {
+ return true;
+ }
+
+ public override int getPriority() {
+ // TODO make configurable from outside
+ return 2;
+ }
+
+ public override void TranslateAssemblies(IEnumerable<Microsoft.Cci.IUnit> assemblies) {
+ traverser.InjectPhoneCodeAssemblies(assemblies);
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index fac00e42..472cbb0a 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -17,19 +17,22 @@ using Microsoft.Cci.ILToCodeModel; using TranslationPlugins;
using Bpl = Microsoft.Boogie;
+using BytecodeTranslator.TranslationPlugins;
namespace BytecodeTranslator {
public abstract class TraverserFactory {
public int Priority { get; set; }
+ public abstract Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> reader);
+
public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,
IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
IDictionary<IUnit, PdbReader> sourceLocationProviders)
{
- return new MetadataTraverser(sink, sourceLocationProviders);
+ return new MetadataTraverser(sink, sourceLocationProviders, this);
}
public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
- return new StatementTraverser(sink, pdbReader, contractContext);
+ return new StatementTraverser(sink, pdbReader, contractContext, this);
}
public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs index fe64ae25..b7611375 100644 --- a/BCT/BytecodeTranslator/WholeProgram.cs +++ b/BCT/BytecodeTranslator/WholeProgram.cs @@ -15,6 +15,11 @@ using System.Diagnostics.Contracts; namespace BytecodeTranslator {
class WholeProgram : TraverserFactory {
+ public override TranslationPlugins.Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {
+ BaseTranslator translator = new BaseTranslator(this, sink, contractProviders, pdbReaders);
+ return translator;
+ }
+
/// <summary>
/// Table to be filled by the metadata traverser before visiting any assemblies.
///
@@ -27,7 +32,7 @@ namespace BytecodeTranslator { public override MetadataTraverser MakeMetadataTraverser(Sink sink,
IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
IDictionary<IUnit, PdbReader> pdbReaders) {
- return new WholeProgramMetadataSemantics(this, sink, pdbReaders);
+ return new WholeProgramMetadataSemantics(this, sink, pdbReaders, this);
}
public class WholeProgramMetadataSemantics : MetadataTraverser {
@@ -37,8 +42,8 @@ namespace BytecodeTranslator { readonly Dictionary<IUnit, bool> codeUnderAnalysis = new Dictionary<IUnit, bool>();
- public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)
- : base(sink, pdbReaders) {
+ public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, IDictionary<IUnit, PdbReader> pdbReaders, TraverserFactory factory)
+ : base(sink, pdbReaders, factory) {
this.parent = parent;
this.sink = sink;
}
|