- handler methods with simulated calls

- easy checks on backstack navigation that may make graph innecessary

4 files changed, 174 insertions, 46 deletions

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 35561528..389c3684 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -307,6 +307,7 @@ namespace BytecodeTranslator {
       if (PhoneCodeHelper.PhoneFeedbackToggled && PhoneCodeHelper.isMethodInputHandlerOrFeedbackOverride(method, sink.host) &&

           !PhoneCodeHelper.isMethodIgnoredForFeedback(method)) {

             proc.AddAttribute("inline", new Bpl.LiteralExpr(Bpl.Token.NoToken, Microsoft.Basetypes.BigNum.ONE));

+            PhoneCodeHelper.trackCallableMethod(proc);

       }

 

       try {

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index ecc483f6..827eaf3e 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -5,6 +5,7 @@ using System.Text;
 using Microsoft.Cci;

 using Bpl=Microsoft.Boogie;

 using TranslationPlugins;

+using Microsoft.Cci.MutableCodeModel;

 

 namespace BytecodeTranslator.Phone {

   public enum StaticURIMode {

@@ -19,6 +20,11 @@ namespace BytecodeTranslator.Phone {
   }

 

   public static class PhoneCodeHelper {

+    // TODO refactor into Feedbakc and Navigation specific code, this is already a mess

+    public static bool OnBackKeyPressOverriden { get; set; }

+    public static bool BackKeyPressHandlerCancels { get; set; }

+    public static bool BackKeyPressNavigates { get; set; }

+

     // TODO externalize strings

     public static readonly string[] IgnoredEvents =

     { "Loaded",

@@ -192,11 +198,7 @@ namespace BytecodeTranslator.Phone {
 

     public static bool isNavigationServiceClass(this ITypeReference typeRef, IMetadataHost 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);

+      IAssemblyReference phoneAssembly = getPhoneAssemblyReference(host);

       ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "System", "Windows", "Navigation", "NavigationService");

 

       return typeRef.isClass(phoneApplicationPageTypeRef);

@@ -204,11 +206,7 @@ namespace BytecodeTranslator.Phone {
 

     public static bool isRoutedEventHandler(this ITypeReference typeRef, IMetadataHost 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);

+      IAssemblyReference systemAssembly = getSystemWindowsAssemblyReference(host);

       ITypeReference routedEvHandlerType = platform.CreateReference(systemAssembly, "System", "Windows", "RoutedEventHandler");

       return typeRef.isClass(routedEvHandlerType);

       

@@ -216,22 +214,14 @@ namespace BytecodeTranslator.Phone {
 

     public static bool isMessageBoxClass(this ITypeReference typeRef, IMetadataHost 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);

+      IAssemblyReference systemAssembly = getSystemWindowsAssemblyReference(host);

       ITypeReference mbType = platform.CreateReference(systemAssembly, "System", "Windows", "MessageBox");

       return typeRef.isClass(mbType);

     }

 

     public static bool isPhoneControlClass(this ITypeReference typeRef, IMetadataHost host, out PHONE_CONTROL_TYPE controlType) {

       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);

+      IAssemblyReference systemAssembly = getSystemWindowsAssemblyReference(host);

       ITypeReference uiElementType = platform.CreateReference(systemAssembly, "System", "Windows", "UIElement");

       ITypeReference frameworkElementType = platform.CreateReference(systemAssembly, "System", "Windows", "FrameworkElement");

 

@@ -317,25 +307,48 @@ namespace BytecodeTranslator.Phone {
       return controlType != PHONE_CONTROL_TYPE.None;

     }

 

-    public static bool isPhoneApplicationClass(this ITypeReference typeRef, IMetadataHost host) {

+    public static IAssemblyReference getSystemAssemblyReference(IMetadataHost 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,

+      AssemblyIdentity MSPhoneSystemAssemblyId =

+          new AssemblyIdentity(host.NameTable.GetNameFor("System"), coreAssemblyRef.Culture, coreAssemblyRef.Version,

                                coreAssemblyRef.PublicKeyToken, "");

+      return host.FindAssembly(MSPhoneSystemAssemblyId);

+    }

+

+    public static bool isCancelEventArgsClass(this ITypeReference typeRef, IMetadataHost host) {

+      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;

+      IAssemblyReference systemAssembly = getSystemAssemblyReference(host);

+      ITypeReference cancelEventArgsClass = platform.CreateReference(systemAssembly, "System", "ComponentModel", "CancelEventArgs");

+      return typeRef.isClass(cancelEventArgsClass);

+    }

 

-      IAssemblyReference systemAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);

+    public static bool isPhoneApplicationClass(this ITypeReference typeRef, IMetadataHost host) {

+      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;

+      IAssemblyReference systemAssembly= getSystemWindowsAssemblyReference(host);

       ITypeReference applicationClass = platform.CreateReference(systemAssembly, "System", "Windows", "Application");

       return typeRef.isClass(applicationClass);

     }

 

-    public static bool isPhoneApplicationPageClass(this ITypeReference typeRef, IMetadataHost host) {

+    public static IAssemblyReference getSystemWindowsAssemblyReference(IMetadataHost 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, "");

+      return host.FindAssembly(MSPhoneSystemWindowsAssemblyId);

+    }

+

+    public static IAssemblyReference getPhoneAssemblyReference(IMetadataHost host) {

       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 }, "");

+      return host.FindAssembly(MSPhoneAssemblyId);

+    }

 

-      IAssemblyReference phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);

+    public static bool isPhoneApplicationPageClass(this ITypeReference typeRef, IMetadataHost host) {

+      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;

+      IAssemblyReference phoneAssembly = getPhoneAssemblyReference(host);

       ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Controls" , "PhoneApplicationPage");

       

       return typeRef.isClass(phoneApplicationPageTypeRef);

@@ -463,11 +476,7 @@ namespace BytecodeTranslator.Phone {
     public static bool isMethodInputHandlerOrFeedbackOverride(IMethodDefinition method, IMetadataHost host) {

       // FEEDBACK TODO: This is extremely coarse. There must be quite a few non-UI routed events

       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);

+      IAssemblyReference systemAssembly = getSystemWindowsAssemblyReference(host);

       ITypeReference routedEventType= platform.CreateReference(systemAssembly, "System", "Windows", "RoutedEventArgs");

       foreach (IParameterDefinition paramDef in method.Parameters) {

         if (paramDef.Type.isClass(routedEventType))

@@ -566,5 +575,54 @@ namespace BytecodeTranslator.Phone {
       string methodName = type.ContainingUnitNamespace.Name.Value + "." + type.Name + "." + methodTranslated.Name.Value;

       return ignoredHandlers.Contains(methodName);

     }

+

+    private static HashSet<Bpl.Procedure> callableMethods = new HashSet<Bpl.Procedure>();

+    public static void trackCallableMethod(Bpl.Procedure proc) {

+      callableMethods.Add(proc);

+    }

+

+    public static IEnumerable<Bpl.Procedure> getCallableMethods() {

+      return callableMethods;

+    }

+

+    public static void CreateFeedbackCallingMethods(Sink sink) {

+      Bpl.Program translatedProgram= sink.TranslatedProgram;

+      foreach (Bpl.Procedure proc in callableMethods) {

+        addMethodCalling(proc, translatedProgram, sink);

+      }

+    }

+

+    private static void addMethodCalling(Bpl.Procedure proc, Bpl.Program program, Sink sink) {

+      Bpl.Procedure callingProc= new Bpl.Procedure(Bpl.Token.NoToken, "__BOOGIE_CALL_" + proc.Name, new Bpl.TypeVariableSeq(), new Bpl.VariableSeq(),

+                                                   new Bpl.VariableSeq(), new Bpl.RequiresSeq(), new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());

+      sink.TranslatedProgram.TopLevelDeclarations.Add(callingProc);

+

+      Bpl.StmtListBuilder codeBuilder = new Bpl.StmtListBuilder();

+      Bpl.VariableSeq localVars = new Bpl.VariableSeq(proc.InParams);

+      Bpl.IdentifierExprSeq identVars= new Bpl.IdentifierExprSeq();

+

+      for (int i = 0; i < localVars.Length; i++) {

+        identVars.Add(new Bpl.IdentifierExpr(Bpl.Token.NoToken, localVars[i]));

+      }

+      codeBuilder.Add(new Bpl.HavocCmd(Bpl.Token.NoToken, identVars));

+

+      Bpl.ExprSeq callParams = new Bpl.ExprSeq();

+      for (int i = 0; i < identVars.Length; i++) {

+        callParams.Add(identVars[i]);

+      }

+      Bpl.CallCmd callCmd = new Bpl.CallCmd(Bpl.Token.NoToken, proc.Name, callParams, new Bpl.IdentifierExprSeq());

+      codeBuilder.Add(callCmd);

+      Bpl.Implementation impl = new Bpl.Implementation(Bpl.Token.NoToken, callingProc.Name, new Bpl.TypeVariableSeq(), new Bpl.VariableSeq(),

+                                                       new Bpl.VariableSeq(), localVars, codeBuilder.Collect(Bpl.Token.NoToken));

+      sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

+    }

+

+    public static bool isBackKeyPressOverride(this IMethodDefinition method, IMetadataHost host) {

+      if (!method.IsVirtual || method.Name.Value != "OnBackKeyPress" || !method.ContainingType.isPhoneApplicationPageClass(host) ||

+          method.ParameterCount != 1 || !method.Parameters.ToList()[0].Type.isCancelEventArgsClass(host))

+        return false;

+      else

+        return true;

+    }

   }

 }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
index 500acb22..81e59907 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -10,22 +10,23 @@ namespace BytecodeTranslator.Phone {
   public class PhoneNavigationCodeTraverser : BaseCodeTraverser {

     private MetadataReaderHost host;

     private ITypeReference navigationSvcType;

+    private ITypeReference cancelEventArgsType;

     private ITypeReference typeTraversed;

+    private IMethodDefinition methodTraversed;

 

-    public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed) : base() {

+    public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed, IMethodDefinition methodTraversed) : base() {

       this.host = host;

       this.typeTraversed = typeTraversed;

+      this.methodTraversed = methodTraversed;

       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);

-

+      IAssemblyReference assembly= PhoneCodeHelper.getPhoneAssemblyReference(host);

       // TODO determine the needed types dynamically

-      navigationSvcType = platform.CreateReference(phoneAssembly, "System", "Windows", "Navigation", "NavigationService");

+      navigationSvcType = platform.CreateReference(assembly, "System", "Windows", "Navigation", "NavigationService");

+

+      assembly = PhoneCodeHelper.getSystemAssemblyReference(host);

+      cancelEventArgsType = platform.CreateReference(assembly, "System", "ComponentModel", "CancelEventArgs");

     }

 

     public override void Visit(IMethodDefinition method) {

@@ -87,7 +88,49 @@ namespace BytecodeTranslator.Phone {
       injectNavigationUpdateCode(block, staticNavStmts, nonStaticNavStmts);

     }

 

+    private bool isNavigationOnBackKeyPressHandler(IMethodCall call) {

+      if (!methodTraversed.ResolvedMethod.isBackKeyPressOverride(host))

+        return false;

+

+      if (!call.MethodToCall.ContainingType.isNavigationServiceClass(host))

+        return false;

+

+      if (!PhoneCodeHelper.NAV_CALLS.Contains(call.MethodToCall.Name.Value) || call.MethodToCall.Name.Value == "GoBack") // back is actually ok

+        return false;

+

+      return true;

+    }

+

+    private bool isCancelOnBackKeyPressHandler(IMethodCall call) {

+      if (!methodTraversed.ResolvedMethod.isBackKeyPressOverride(host))

+        return false;

+

+      if (!call.MethodToCall.Name.Value.StartsWith("set_Cancel"))

+        return false;

+

+      if (call.Arguments.ToList()[0].Type != host.PlatformType.SystemBoolean)

+        return false;

+

+      ICompileTimeConstant constant = call.Arguments.ToList()[0] as ICompileTimeConstant;

+      if (constant != null && constant.Value != null ) {

+        CompileTimeConstant falseConstant = new CompileTimeConstant() {

+          Type = host.PlatformType.SystemBoolean,

+          Value = false,

+        };

+        if (constant.Value == falseConstant.Value)

+          return false;

+      }

+

+      return true;

+    }

+

     public override void Visit(IMethodCall methodCall) {

+      if (isNavigationOnBackKeyPressHandler(methodCall)) {

+        PhoneCodeHelper.BackKeyPressNavigates = true;

+      } else if (isCancelOnBackKeyPressHandler(methodCall)) {

+        PhoneCodeHelper.BackKeyPressHandlerCancels = true;

+      }

+

       // check whether it is a NavigationService call

       IMethodReference methodToCall= methodCall.MethodToCall;

       ITypeReference callType= methodToCall.ContainingType;

@@ -302,7 +345,11 @@ 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(host, typeBeingTraversed);

+      if (method.isBackKeyPressOverride(host)) {

+        PhoneCodeHelper.OnBackKeyPressOverriden = true;

+      }

+

+      PhoneNavigationCodeTraverser codeTraverser = new PhoneNavigationCodeTraverser(host, typeBeingTraversed, method);

       codeTraverser.Visit(method);

     }

 

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 14bf89e7..b62fa098 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -225,12 +225,34 @@ namespace BytecodeTranslator {
         CreateDispatchMethod(sink, pair.Item1, pair.Item2);

       }

 

-      if (phonePlugin != null) {

-        string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout");

-        StreamWriter outputStream = new StreamWriter(outputConfigFile);

-        phonePlugin.DumpControlStructure(outputStream);

-        outputStream.Close();

-        PhoneCodeWrapperWriter.createCodeWrapper(sink);

+      if (PhoneCodeHelper.PhonePlugin != null) {

+        if (PhoneCodeHelper.PhoneFeedbackToggled) {

+          // FEEDBACK TODO create simple callers to callable methods, havoc'ing parameters

+          PhoneCodeHelper.CreateFeedbackCallingMethods(sink);

+        }

+

+        if (PhoneCodeHelper.PhoneNavigationToggled) {

+          string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout");

+          StreamWriter outputStream = new StreamWriter(outputConfigFile);

+          phonePlugin.DumpControlStructure(outputStream);

+          outputStream.Close();

+          PhoneCodeWrapperWriter.createCodeWrapper(sink);

+

+          // NAVIGATION TODO for now I console this out

+          if (!PhoneCodeHelper.OnBackKeyPressOverriden) {

+            Console.Out.WriteLine("No back navigation issues, OnBackKeyPress is not overriden");

+          } else if (!PhoneCodeHelper.BackKeyPressHandlerCancels && !PhoneCodeHelper.BackKeyPressNavigates) {

+            Console.Out.WriteLine("No back navigation issues, BackKeyPress overrides do not alter navigation");

+          } else {

+            if (PhoneCodeHelper.BackKeyPressNavigates) {

+              Console.Out.WriteLine("Back navigation ISSUE: back key press may navigate to pages not in backstack!");

+            }

+

+            if (PhoneCodeHelper.BackKeyPressHandlerCancels) {

+              Console.Out.WriteLine("Back navigation ISSUE: back key press default behaviour may be cancelled!");

+            }

+          }

+        }

       }

 

       Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");