summaryrefslogtreecommitdiff
path: root/BCT
diff options
context:
space:
mode:
Diffstat (limited to 'BCT')
-rw-r--r--BCT/BytecodeTranslator/BytecodeTranslator.csproj5
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs85
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs23
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs239
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs9
-rw-r--r--BCT/BytecodeTranslator/Program.cs7
6 files changed, 345 insertions, 23 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 0393913a..e9b8be83 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -125,7 +125,10 @@
<Compile Include="Heap.cs" />
<Compile Include="HeapFactory.cs" />
<Compile Include="MetadataTraverser.cs" />
- <Compile Include="Phone\PhoneTraverser.cs" />
+ <Compile Include="Phone\PhoneCodeHelper.cs" />
+ <Compile Include="Phone\PhoneInitializationTraverser.cs" />
+ <Compile Include="Phone\PhoneNavigationTraverser.cs" />
+ <Compile Include="Phone\PhoneURIDeclarationsTraverser.cs" />
<Compile Include="Prelude.cs" />
<Compile Include="ExpressionTraverser.cs" />
<Compile Include="Sink.cs" />
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
new file mode 100644
index 00000000..bf293a51
--- /dev/null
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -0,0 +1,85 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Cci;
+
+namespace BytecodeTranslator.Phone {
+ public enum StaticURIMode {
+ NOT_STATIC, STATIC_URI_CREATION_ONSITE, STATIC_URI_ROOT_CREATION_ONSITE,
+ }
+
+ public static class PhoneCodeHelper {
+ // TODO ensure this name is unique in the program code, although it is esoteric enough
+ private const string IL_BOOGIE_VAR_PREFIX = "@__BOOGIE_";
+ public const string IL_CURRENT_NAVIGATION_URI_VARIABLE = IL_BOOGIE_VAR_PREFIX + "CurrentNavigationURI__";
+
+ public static bool isCreateObjectInstance(this IExpression expr) {
+ ICreateObjectInstance createObjExpr = expr as ICreateObjectInstance;
+ return (createObjExpr != null);
+ }
+
+ public static bool isClass(this ITypeReference typeRef, ITypeReference targetTypeRef) {
+ while (typeRef != null) {
+ if (typeRef.ResolvedType.Equals(targetTypeRef.ResolvedType))
+ return true;
+
+ typeRef = typeRef.ResolvedType.BaseClasses.FirstOrDefault();
+ }
+
+ return false;
+ }
+
+ public static bool isStringClass(this ITypeReference typeRef, MetadataReaderHost host) {
+ ITypeReference targetType = host.PlatformType.SystemString;
+ return typeRef.isClass(targetType);
+ }
+
+ public static bool isURIClass (this ITypeReference typeRef, MetadataReaderHost host) {
+ Microsoft.Cci.Immutable.PlatformType platformType = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+ if (platformType == null)
+ return false;
+
+ IAssemblyReference coreRef = platformType.CoreAssemblyRef;
+ AssemblyIdentity systemAssemblyId = new AssemblyIdentity(host.NameTable.GetNameFor("System"), "", coreRef.Version, coreRef.PublicKeyToken, "");
+ IAssemblyReference systemAssembly = host.FindAssembly(systemAssemblyId);
+
+ ITypeReference uriTypeRef= platformType.CreateReference(systemAssembly, "System", "URI");
+ return typeRef.isClass(uriTypeRef);
+ }
+
+
+ public static bool isPhoneApplicationClass(this ITypeReference typeRef, MetadataReaderHost host) {
+ Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+ IAssemblyReference coreAssemblyRef = platform.CoreAssemblyRef;
+ AssemblyIdentity MSPhoneSystemWindowsAssemblyId =
+ new AssemblyIdentity(host.NameTable.GetNameFor("System.Windows"), coreAssemblyRef.Culture, coreAssemblyRef.Version,
+ coreAssemblyRef.PublicKeyToken, "");
+
+ IAssemblyReference systemAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);
+ ITypeReference applicationClass = platform.CreateReference(systemAssembly, "System", "Windows", "Application");
+
+ return typeRef.isClass(applicationClass);
+ }
+
+ public static bool isPhoneApplicationPageClass(ITypeReference typeDefinition, MetadataReaderHost host) {
+ Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+ AssemblyIdentity MSPhoneAssemblyId =
+ new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
+ new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+
+ IAssemblyReference phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
+ ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Controls", "PhoneApplicationPage");
+
+ ITypeReference baseClass = typeDefinition.ResolvedType.BaseClasses.FirstOrDefault();
+ while (baseClass != null) {
+ if (baseClass.ResolvedType.Equals(phoneApplicationPageTypeRef.ResolvedType)) {
+ return true;
+ }
+ baseClass = baseClass.ResolvedType.BaseClasses.FirstOrDefault();
+ }
+
+ return false;
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
index 121c4384..ad502911 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
@@ -18,7 +18,7 @@ using System.Diagnostics.Contracts;
using TranslationPlugins;
-namespace BytecodeTranslator {
+namespace BytecodeTranslator.Phone {
/// <summary>
/// Traverse code looking for phone specific points of interest, possibly injecting necessary code in-between
@@ -291,28 +291,11 @@ namespace BytecodeTranslator {
/// </summary>
///
public override void Visit(ITypeDefinition typeDefinition) {
- if (typeDefinition.IsClass && isPhoneApplicationPage(typeDefinition)) {
+ if (typeDefinition.IsClass && PhoneCodeHelper.isPhoneApplicationPageClass(typeDefinition, host)) {
base.Visit(typeDefinition);
}
}
- private bool isPhoneApplicationPage(ITypeDefinition typeDefinition) {
- ITypeReference baseClass = typeDefinition.BaseClasses.FirstOrDefault();
- ITypeDefinition baseClassDef;
- while (baseClass != null) {
- baseClassDef = baseClass.ResolvedType;
- if (baseClassDef is INamespaceTypeDefinition) {
- if (((INamespaceTypeDefinition) baseClassDef).Name.Value == "PhoneApplicationPage" &&
- ((INamespaceTypeDefinition) baseClassDef).Container.ToString() == "Microsoft.Phone.Controls") {
- return true;
- }
- }
- baseClass = baseClass.ResolvedType.BaseClasses.FirstOrDefault();
- }
-
- return false;
- }
-
/// <summary>
/// Check if it is traversing a constructor. If so, place necessary code after InitializeComponent() call
/// </summary>
@@ -328,7 +311,7 @@ namespace BytecodeTranslator {
codeTraverser.injectPhoneControlsCode(block);
}
- public virtual void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {
+ public void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {
foreach (var a in assemblies) {
a.Dispatch(this);
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
new file mode 100644
index 00000000..edefa24d
--- /dev/null
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -0,0 +1,239 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Cci;
+using Microsoft.Cci.MutableCodeModel;
+
+namespace BytecodeTranslator.Phone {
+ public class PhoneNavigationCodeTraverser : BaseCodeTraverser {
+ private MetadataReaderHost host;
+ private bool navCallFound;
+ private ITypeReference navigationSvcType;
+ private ITypeReference typeTraversed;
+
+ private static readonly string[] NAV_CALLS = { "GoBack", "GoForward", "Navigate", "StopLoading" };
+
+ public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed) : base() {
+ this.host = host;
+ this.typeTraversed = typeTraversed;
+ Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+
+ // TODO obtain version, culture and signature data dynamically
+ AssemblyIdentity MSPhoneAssemblyId =
+ new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
+ new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+
+ IAssembly phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
+
+ // TODO determine the needed types dynamically
+ navigationSvcType = platform.CreateReference(phoneAssembly, "System", "Windows", "Navigation", "NavigationService");
+ }
+
+ public override void Visit(IMethodDefinition method) {
+ if (method.IsConstructor && PhoneCodeHelper.isPhoneApplicationClass(typeTraversed, host)) {
+ // TODO initialize current navigation URI to mainpage, using a placeholder for now.
+ // TODO BUG doing this is generating a fresh variable definition somewhere that the BCT then translates into two different (identical) declarations
+ string URI_placeholder="URI_PLACEHOLDER";
+ SourceMethodBody sourceBody = method.Body as SourceMethodBody;
+ if (sourceBody != null) {
+ BlockStatement bodyBlock = sourceBody.Block as BlockStatement;
+ if (bodyBlock != null) {
+ Assignment uriInitAssign = new Assignment() {
+ Source = new CompileTimeConstant() {
+ Type = host.PlatformType.SystemString,
+ Value = URI_placeholder,
+ },
+ Type = host.PlatformType.SystemString,
+ Target = new TargetExpression() {
+ Type = host.PlatformType.SystemString,
+ Definition = new FieldReference() {
+ ContainingType= typeTraversed,
+ IsStatic=true,
+ Type=host.PlatformType.SystemString,
+ Name=host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),
+ },
+ },
+ };
+ Statement uriInitStmt= new ExpressionStatement() {
+ Expression= uriInitAssign,
+ };
+ bodyBlock.Statements.Insert(0, uriInitStmt);
+ }
+ }
+ }
+ base.Visit(method);
+ }
+
+ public override void Visit(IBlockStatement block) {
+ IList<IStatement> navStmts = new List<IStatement>();
+ foreach (IStatement statement in block.Statements) {
+ navCallFound = false;
+ this.Visit(statement);
+ if (navCallFound) {
+ navStmts.Add(statement);
+ }
+ }
+
+ injectNavigationUpdateCode(block, navStmts);
+ }
+
+ private int navEvtCount= 0;
+ private int staticNavEvtCount = 0;
+ private int nonStaticNavEvtCount = 0;
+ public override void Visit(IMethodCall methodCall) {
+ // check whether it is a NavigationService call
+ IMethodReference methodToCall= methodCall.MethodToCall;
+ ITypeReference callType= methodToCall.ContainingType;
+ if (!callType.ResolvedType.Equals(navigationSvcType.ResolvedType))
+ return;
+
+ string methodToCallName= methodToCall.Name.Value;
+ if (!NAV_CALLS.Contains(methodToCallName))
+ return;
+
+ // TODO check what to do with these
+ if (methodToCallName == "GoForward" || methodToCallName == "StopLoading") {
+ // TODO forward navigation is not supported by the phone
+ // TODO StopLoading is very async, I don't think we may verify this behaviour
+ // TODO possibly log
+ return;
+ } else {
+ navCallFound = true;
+ bool targetIsStatic=false;
+ string notStaticReason = "";
+ if (methodToCallName == "GoBack")
+ targetIsStatic = true;
+ else { // Navigate()
+ // check for different static patterns that we may be able to verify
+ bool isStatic = false;
+ StaticURIMode staticMode = StaticURIMode.NOT_STATIC;
+
+ IExpression uriArg= methodCall.Arguments.First();
+ if (isArgumentURILocallyCreatedStatic(uriArg)) {
+ isStatic = true;
+ staticMode = StaticURIMode.STATIC_URI_CREATION_ONSITE;
+ } else if (isArgumentURILocallyCreatedStaticRoot(uriArg)) {
+ isStatic=true;
+ staticMode=StaticURIMode.STATIC_URI_ROOT_CREATION_ONSITE;
+ }
+
+ ICreateObjectInstance creationSite= methodCall.Arguments.First() as ICreateObjectInstance;
+ if (creationSite != null) {
+ if (creationSite.Arguments.First().Type.ResolvedType.Equals(host.PlatformType.SystemString.ResolvedType) && creationSite.Arguments.First() is ICompileTimeConstant) {
+ targetIsStatic = true;
+ } else {
+ targetIsStatic = false;
+ notStaticReason = "URI not initialized as a static string";
+ }
+ } else {
+ targetIsStatic = false;
+ notStaticReason = "URI not created at call site";
+ }
+ }
+ Console.Write("Page navigation event found. Target is static? " + (targetIsStatic ? "YES" : "NO"));
+ if (!targetIsStatic) {
+ nonStaticNavEvtCount++;
+ Console.WriteLine(" -- Reason: " + notStaticReason);
+ } else {
+ staticNavEvtCount++;
+ Console.WriteLine("");
+ }
+ navEvtCount++;
+ }
+ }
+
+ /// <summary>
+ /// checks if argument is locally created URI with static URI target
+ /// </summary>
+ /// <param name="arg"></param>
+ /// <returns></returns>
+ private bool isArgumentURILocallyCreatedStatic(IExpression arg) {
+ if (!arg.isCreateObjectInstance())
+ return false;
+
+ if (!arg.Type.isURIClass(host))
+ return false;
+
+ ICreateObjectInstance creationSite = arg as ICreateObjectInstance;
+ IExpression uriTargetArg= creationSite.Arguments.First();
+
+ if (!uriTargetArg.Type.isStringClass(host))
+ return false;
+
+ ICompileTimeConstant staticURITarget = uriTargetArg as ICompileTimeConstant;
+ return (staticURITarget != null);
+ }
+
+ /// <summary>
+ /// checks if argument is locally created URI where target has statically created URI root
+ /// </summary>
+ /// <param name="arg"></param>
+ /// <returns></returns>
+ private bool isArgumentURILocallyCreatedStaticRoot(IExpression arg) {
+ // Pre: !isArgumentURILocallyCreatedStatic
+ // TODO
+ return false;
+ }
+
+ private void injectNavigationUpdateCode(IBlockStatement block, IEnumerable<IStatement> stmts) {
+ // TODO Here there is the STRONG assumption that a given method will only navigate at most once per method call
+ // TODO (or at most will re-navigate to the same page). Quick "page flipping" on the same method
+ // TODO would not be captured correctly
+ }
+ }
+
+ /// <summary>
+ /// Traverse metadata looking only for PhoneApplicationPage's constructors
+ /// </summary>
+ public class PhoneNavigationMetadataTraverser : BaseMetadataTraverser {
+ private MetadataReaderHost host;
+ private ITypeDefinition typeBeingTraversed;
+
+ public PhoneNavigationMetadataTraverser(MetadataReaderHost host)
+ : base() {
+ this.host = host;
+ }
+
+ public override void Visit(IModule module) {
+ base.Visit(module);
+ }
+
+ public override void Visit(IAssembly assembly) {
+ base.Visit(assembly);
+ }
+
+ // TODO can we avoid visiting every type? Are there only a few, identifiable, types that may perform navigation?
+ public override void Visit(ITypeDefinition typeDefinition) {
+ typeBeingTraversed = typeDefinition;
+ if (typeDefinition.isPhoneApplicationClass(host)) {
+ NamespaceTypeDefinition mutableTypeDef = typeDefinition as NamespaceTypeDefinition;
+ if (mutableTypeDef != null) {
+ FieldDefinition fieldDef = new FieldDefinition() {
+ ContainingTypeDefinition= mutableTypeDef,
+ InternFactory= host.InternFactory,
+ IsStatic= true,
+ Name= host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),
+ Type= host.PlatformType.SystemString,
+ Visibility= TypeMemberVisibility.Public,
+ };
+ mutableTypeDef.Fields.Add(fieldDef);
+ }
+ }
+ base.Visit(typeDefinition);
+ }
+
+ // TODO same here. Are there specific methods (and ways to identfy those) that can perform navigation?
+ public override void Visit(IMethodDefinition method) {
+
+ PhoneNavigationCodeTraverser codeTraverser = new PhoneNavigationCodeTraverser(host, typeBeingTraversed);
+ codeTraverser.Visit(method);
+ }
+
+ public void InjectPhoneCodeAssemblies(IEnumerable<IUnit> assemblies) {
+ foreach (var a in assemblies) {
+ a.Dispatch(this);
+ }
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs
new file mode 100644
index 00000000..fa330439
--- /dev/null
+++ b/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs
@@ -0,0 +1,9 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace BytecodeTranslator.Phone {
+ class PhoneURIDeclarationsTraverser {
+ }
+}
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index a9d44200..0867de9f 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -18,6 +18,7 @@ using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
using Microsoft.Cci.MutableCodeModel.Contracts;
using TranslationPlugins;
+using BytecodeTranslator.Phone;
namespace BytecodeTranslator {
@@ -176,8 +177,10 @@ namespace BytecodeTranslator {
var primaryModule = modules[0];
if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
- PhoneInitializationMetadataTraverser tr = new PhoneInitializationMetadataTraverser(new PhoneControlsPlugin(phoneControlsConfigFile), host);
- tr.InjectPhoneCodeAssemblies(modules);
+ PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(new PhoneControlsPlugin(phoneControlsConfigFile), host);
+ initTr.InjectPhoneCodeAssemblies(modules);
+ PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(host);
+ navTr.InjectPhoneCodeAssemblies(modules);
}
TraverserFactory traverserFactory;