diff options
Diffstat (limited to 'BCT/BytecodeTranslator/Phone')
4 files changed, 100 insertions, 40 deletions
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs index 74ad2140..615b5a51 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs @@ -3,6 +3,8 @@ using System.Collections.Generic; using System.Linq;
using System.Text;
using Microsoft.Cci;
+using Bpl=Microsoft.Boogie;
+using TranslationPlugins;
namespace BytecodeTranslator.Phone {
public enum StaticURIMode {
@@ -11,8 +13,45 @@ namespace BytecodeTranslator.Phone { public static class PhoneCodeHelper {
// TODO ensure this name is unique in the program code, although it is esoteric enough
+ // TODO externalize strings
private const string IL_BOOGIE_VAR_PREFIX = "@__BOOGIE_";
+ private const string BOOGIE_VAR_PREFIX= "__BOOGIE_";
public const string IL_CURRENT_NAVIGATION_URI_VARIABLE = IL_BOOGIE_VAR_PREFIX + "CurrentNavigationURI__";
+ public const string BOOGIE_CONTINUE_ON_PAGE_VARIABLE = BOOGIE_VAR_PREFIX + "ContinueOnPage__";
+
+ // awful hack. want to insert a nonexisting method call while traversing CCI AST, deferring it to Boogie translation
+ public const string BOOGIE_DO_HAVOC_CURRENTURI = BOOGIE_VAR_PREFIX + "Havoc_CurrentURI__";
+
+ public static PhoneControlsPlugin PhonePlugin { get; set; }
+ private static IDictionary<string, Bpl.NamedDeclaration> boogieObjects = new Dictionary<string, Bpl.NamedDeclaration>();
+
+ public static Bpl.Variable getBoogieVariableForName(string varName) {
+ Bpl.Variable boogieVar = null;
+ try {
+ boogieVar = boogieObjects[varName] as Bpl.Variable;
+ } catch (KeyNotFoundException) {
+ }
+
+ if (boogieVar == null)
+ throw new ArgumentException("The boogie variable " + varName + " is not defined.");
+
+ return boogieVar;
+ }
+
+ /// <summary>
+ ///
+ /// </summary>
+ /// <param name="name"></param>
+ /// <param name="bplObject"></param>
+ /// <returns>true if defining a new name, false if replacing</returns>
+ public static bool setBoogieObjectForName(string name, Bpl.NamedDeclaration bplObject) {
+ bool ret= true;
+ if (boogieObjects.ContainsKey(name))
+ ret = false;
+
+ boogieObjects[name] = bplObject;
+ return ret;
+ }
public static bool isCreateObjectInstance(this IExpression expr) {
ICreateObjectInstance createObjExpr = expr as ICreateObjectInstance;
@@ -58,7 +97,6 @@ namespace BytecodeTranslator.Phone { IAssemblyReference systemAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);
ITypeReference applicationClass = platform.CreateReference(systemAssembly, "System", "Windows", "Application");
-
return typeRef.isClass(applicationClass);
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs index 4a469ad1..49b43137 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs @@ -8,12 +8,10 @@ using TranslationPlugins; namespace BytecodeTranslator.Phone {
class PhoneCodeWrapperWriter {
private static Sink sink;
- private static PhoneControlsPlugin controlsPlugin;
private static readonly string BOOGIE_MAIN_PROCEDURE = "$__BOOGIE_MAIN_PROCEDURE__$";
- public static void createCodeWrapper(Sink sink, PhoneControlsPlugin controlsPlugin) {
+ public static void createCodeWrapper(Sink sink) {
PhoneCodeWrapperWriter.sink = sink;
- PhoneCodeWrapperWriter.controlsPlugin = controlsPlugin;
/*
* create Main procedure
* - creates page instances, one per page -- this overapproximates as there may be more instances
diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs index e4510a7d..92090cc1 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs @@ -26,7 +26,6 @@ namespace BytecodeTranslator.Phone { public class PhoneInitializationCodeTraverser : BaseCodeTraverser {
private readonly IMethodDefinition methodBeingTraversed;
private static bool initializationFound= false;
- private PhoneControlsPlugin phonePlugin;
private MetadataReaderHost host;
private IAssemblyReference coreAssemblyRef;
@@ -69,9 +68,8 @@ namespace BytecodeTranslator.Phone { }
}
- public PhoneInitializationCodeTraverser(MetadataReaderHost host, IMethodDefinition traversedMethod, PhoneControlsPlugin phonePlugin) : base() {
+ public PhoneInitializationCodeTraverser(MetadataReaderHost host, IMethodDefinition traversedMethod) : base() {
this.methodBeingTraversed = traversedMethod;
- this.phonePlugin = phonePlugin;
this.host = host;
InitializeTraverser();
}
@@ -142,7 +140,7 @@ namespace BytecodeTranslator.Phone { private void injectPhoneInitializationCode(BlockStatement block, Statement statementAfter) {
// TODO check page name against container name
- IEnumerable<ControlInfoStructure> controls= phonePlugin.getControlsForPage(methodBeingTraversed.Container.ToString());
+ IEnumerable<ControlInfoStructure> controls= PhoneCodeHelper.PhonePlugin.getControlsForPage(methodBeingTraversed.Container.ToString());
IEnumerable<IStatement> injectedStatements = new List<IStatement>();
foreach (ControlInfoStructure controlInfo in controls) {
injectedStatements = injectedStatements.Concat(getCodeForSettingEnabledness(controlInfo));
@@ -275,12 +273,10 @@ namespace BytecodeTranslator.Phone { /// Traverse metadata looking only for PhoneApplicationPage's constructors
/// </summary>
public class PhoneInitializationMetadataTraverser : BaseMetadataTraverser {
- private PhoneControlsPlugin phoneControlsInfo;
private MetadataReaderHost host;
- public PhoneInitializationMetadataTraverser(PhoneControlsPlugin phonePlugin, MetadataReaderHost host)
+ public PhoneInitializationMetadataTraverser(MetadataReaderHost host)
: base() {
- this.phoneControlsInfo = phonePlugin;
this.host = host;
}
@@ -309,7 +305,7 @@ namespace BytecodeTranslator.Phone { if (!method.IsConstructor)
return;
- PhoneInitializationCodeTraverser codeTraverser = new PhoneInitializationCodeTraverser(host, method, phoneControlsInfo);
+ PhoneInitializationCodeTraverser codeTraverser = new PhoneInitializationCodeTraverser(host, method);
var methodBody = method.Body as SourceMethodBody;
if (methodBody == null)
return;
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs index 249faf2b..38fb2b58 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs @@ -11,14 +11,12 @@ namespace BytecodeTranslator.Phone { private MetadataReaderHost host;
private ITypeReference navigationSvcType;
private ITypeReference typeTraversed;
- private PhoneControlsPlugin phonePlugin;
- private static readonly string[] NAV_CALLS = { "GoBack", "GoForward", "Navigate", "StopLoading" };
+ private static readonly string[] NAV_CALLS = { /*"GoBack", "GoForward", "Navigate", "StopLoading"*/ "Navigate", "GoBack"};
- public PhoneNavigationCodeTraverser(PhoneControlsPlugin plugin, MetadataReaderHost host, ITypeReference typeTraversed) : base() {
+ public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed) : base() {
this.host = host;
this.typeTraversed = typeTraversed;
- this.phonePlugin = plugin;
Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
// TODO obtain version, culture and signature data dynamically
@@ -36,7 +34,7 @@ namespace BytecodeTranslator.Phone { 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 mainPageUri = phonePlugin.getMainPageXAML();
+ string mainPageUri = PhoneCodeHelper.PhonePlugin.getMainPageXAML();
SourceMethodBody sourceBody = method.Body as SourceMethodBody;
if (sourceBody != null) {
BlockStatement bodyBlock = sourceBody.Block as BlockStatement;
@@ -69,20 +67,25 @@ namespace BytecodeTranslator.Phone { private bool navCallFound=false;
+ private bool navCallIsStatic = false;
private StaticURIMode currentStaticMode= StaticURIMode.NOT_STATIC;
private string unpurifiedFoundURI="";
public override void Visit(IBlockStatement block) {
- IList<Tuple<IStatement,StaticURIMode,string>> navStmts = new List<Tuple<IStatement,StaticURIMode,string>>();
+ IList<Tuple<IStatement,StaticURIMode,string>> staticNavStmts = new List<Tuple<IStatement,StaticURIMode,string>>();
+ IList<IStatement> nonStaticNavStmts = new List<IStatement>();
foreach (IStatement statement in block.Statements) {
navCallFound = false;
+ navCallIsStatic = false;
this.Visit(statement);
- if (navCallFound) {
- navStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));
+ if (navCallFound && navCallIsStatic) {
+ staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));
+ } else if (navCallFound) {
+ nonStaticNavStmts.Add(statement);
}
}
- injectNavigationUpdateCode(block, navStmts);
+ injectNavigationUpdateCode(block, staticNavStmts, nonStaticNavStmts);
}
public override void Visit(IMethodCall methodCall) {
@@ -96,6 +99,7 @@ namespace BytecodeTranslator.Phone { if (!NAV_CALLS.Contains(methodToCallName))
return;
+ navCallFound = true;
// TODO check what to do with these
if (methodToCallName == "GoForward" || methodToCallName == "StopLoading") {
// TODO forward navigation is not supported by the phone
@@ -103,19 +107,18 @@ namespace BytecodeTranslator.Phone { // TODO possibly log
return;
} else {
- bool isStatic=false;
currentStaticMode = StaticURIMode.NOT_STATIC;
- if (methodToCallName == "GoBack")
- isStatic= true;
- else { // Navigate()
+ if (methodToCallName == "GoBack") {
+ navCallIsStatic = false;
+ } else { // Navigate()
// check for different static patterns that we may be able to verify
- IExpression uriArg= methodCall.Arguments.First();
+ IExpression uriArg = methodCall.Arguments.First();
if (isArgumentURILocallyCreatedStatic(uriArg, out unpurifiedFoundURI)) {
- isStatic = true;
+ navCallIsStatic = true;
currentStaticMode = StaticURIMode.STATIC_URI_CREATION_ONSITE;
} else if (isArgumentURILocallyCreatedStaticRoot(uriArg, out unpurifiedFoundURI)) {
- isStatic = true;
+ navCallIsStatic = true;
currentStaticMode = StaticURIMode.STATIC_URI_ROOT_CREATION_ONSITE;
} else {
// get reason
@@ -127,9 +130,6 @@ namespace BytecodeTranslator.Phone { }
}
- if (isStatic)
- navCallFound = true;
-
//Console.Write("Page navigation event found. Target is static? " + (isStatic ? "YES" : "NO"));
//if (!isStatic) {
// Console.WriteLine(" -- Reason: " + notStaticReason);
@@ -192,14 +192,44 @@ namespace BytecodeTranslator.Phone { return true;
}
- private void injectNavigationUpdateCode(IBlockStatement block, IEnumerable<Tuple<IStatement,StaticURIMode, string>> stmts) {
+ private void injectNavigationUpdateCode(IBlockStatement block, IEnumerable<Tuple<IStatement,StaticURIMode, string>> staticStmts, IEnumerable<IStatement> nonStaticStmts) {
// 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
Microsoft.Cci.MutableCodeModel.BlockStatement mutableBlock = block as Microsoft.Cci.MutableCodeModel.BlockStatement;
+
+ foreach (IStatement stmt in nonStaticStmts) {
+ int ndx = mutableBlock.Statements.ToList().IndexOf(stmt);
+ if (ndx == -1) {
+ // can't be
+ throw new IndexOutOfRangeException("Statement must exist in original block");
+ }
+
+ Assignment currentURIAssign = new Assignment() {
+ Source = new CompileTimeConstant() {
+ Type = host.PlatformType.SystemString,
+ Value = PhoneCodeHelper.BOOGIE_DO_HAVOC_CURRENTURI,
+ },
+ 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 = currentURIAssign,
+ };
+ mutableBlock.Statements.Insert(ndx + 1, uriInitStmt);
+ }
+
- foreach (Tuple<IStatement, StaticURIMode, string> entry in stmts) {
- int ndx= mutableBlock.Statements.ToList().IndexOf(entry.Item1, 0);
+ foreach (Tuple<IStatement, StaticURIMode, string> entry in staticStmts) {
+ int ndx= mutableBlock.Statements.ToList().IndexOf(entry.Item1);
if (ndx == -1) {
// can't be
throw new IndexOutOfRangeException("Statement must exist in original block");
@@ -214,8 +244,8 @@ namespace BytecodeTranslator.Phone { Target = new TargetExpression() {
Type = host.PlatformType.SystemString,
Definition = new FieldReference() {
- ContainingType = typeTraversed,
- IsStatic = true,
+ ContainingType=typeTraversed,
+ IsStatic= true,
Type = host.PlatformType.SystemString,
Name = host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),
},
@@ -235,12 +265,10 @@ namespace BytecodeTranslator.Phone { public class PhoneNavigationMetadataTraverser : BaseMetadataTraverser {
private MetadataReaderHost host;
private ITypeDefinition typeBeingTraversed;
- private PhoneControlsPlugin phonePlugin;
- public PhoneNavigationMetadataTraverser(PhoneControlsPlugin plugin, MetadataReaderHost host)
+ public PhoneNavigationMetadataTraverser(MetadataReaderHost host)
: base() {
this.host = host;
- this.phonePlugin = plugin;
}
public override void Visit(IModule module) {
@@ -274,7 +302,7 @@ namespace BytecodeTranslator.Phone { // 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(phonePlugin, host, typeBeingTraversed);
+ PhoneNavigationCodeTraverser codeTraverser = new PhoneNavigationCodeTraverser(host, typeBeingTraversed);
codeTraverser.Visit(method);
}
|