Merge

9 files changed, 123 insertions, 53 deletions

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index e78300d8..30def4a2 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -122,7 +122,7 @@ namespace BytecodeTranslator {
         string fullyQualifiedName = namedTypeDef.ToString();

         string xamlForClass = PhoneCodeHelper.instance().getXAMLForPage(fullyQualifiedName);

         if (xamlForClass != null) { // if not it is possibly an abstract page

-          string uriName = PhoneControlsPlugin.getURIBase(xamlForClass);

+          string uriName = UriHelper.getURIBase(xamlForClass);

           Bpl.Constant uriConstant = sink.FindOrCreateConstant(uriName);

           PhoneCodeHelper.instance().setBoogieStringPageNameForPageClass(fullyQualifiedName, uriConstant.Name);

         }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index 6be74264..cd71e7cc 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -10,6 +10,28 @@ using Microsoft.Cci.MutableCodeModel;
 namespace BytecodeTranslator.Phone {

   public static class UriHelper {

     /// <summary>

+    /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)

+    /// This method returns a base URI

+    /// </summary>

+    /// <param name="uri"></param>

+    /// <returns></returns>

+    public static string getURIBase(string uri) {

+      // I need to build an absolute URI just to call getComponents() ...

+      Uri mockBaseUri = new Uri("mock://mock/", UriKind.RelativeOrAbsolute);

+      Uri realUri;

+      try {

+        realUri = new Uri(uri, UriKind.Absolute);

+      } catch (UriFormatException) {

+        // uri string is relative

+        realUri = new Uri(mockBaseUri, uri);

+      }

+

+      string str = realUri.GetComponents(UriComponents.Path | UriComponents.StrongAuthority | UriComponents.Scheme, UriFormat.UriEscaped);

+      Uri mockStrippedUri = new Uri(str);

+      return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();

+    }

+

+    /// <summary>

     /// checks if argument is locally created URI with static URI target

     /// </summary>

     /// <param name="arg"></param>

@@ -32,7 +54,7 @@ namespace BytecodeTranslator.Phone {
       if (staticURITarget == null)

         return false;

 

-      uri = staticURITarget.Value as string;

+      uri= staticURITarget.Value as string;

       return true;

     }

 

diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
index 4d1f60fb..d79d2c00 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
@@ -31,6 +31,7 @@ namespace BytecodeTranslator.Phone {
     private IAssemblyReference coreAssemblyRef;

     private IAssemblyReference phoneAssembly;

     private IAssemblyReference phoneSystemWindowsAssembly;

+    private IAssemblyReference MSPhoneControlsAssembly;

     private INamespaceTypeReference appBarIconButtonType;

     private INamespaceTypeReference checkBoxType;

     private INamespaceTypeReference radioButtonType;

@@ -39,6 +40,7 @@ namespace BytecodeTranslator.Phone {
     private INamespaceTypeReference toggleButtonType;

     private INamespaceTypeReference controlType;

     private INamespaceTypeReference uiElementType;

+    private INamespaceTypeReference pivotType;

 

     private CompileTimeConstant trueConstant;

     private CompileTimeConstant falseConstant;

@@ -65,6 +67,8 @@ namespace BytecodeTranslator.Phone {
         return checkBoxType;

       } else if (classname == "ApplicationBarIconButton") {

         return appBarIconButtonType;

+      } else if (classname == "Pivot") {

+        return pivotType;

       } else if (classname == "DummyType") {

         return Dummy.Type;

       } else {

@@ -87,12 +91,17 @@ namespace BytecodeTranslator.Phone {
       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 }, "");

+      AssemblyIdentity MSPhoneControlsAssemblyId=

+          new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone.Controls"), "", new Version("7.0.0.0"),

+                               new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");

+

       AssemblyIdentity MSPhoneSystemWindowsAssemblyId =

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

                                coreAssemblyRef.PublicKeyToken, "");

 

       phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);

       phoneSystemWindowsAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);

+      MSPhoneControlsAssembly= host.FindAssembly(MSPhoneControlsAssemblyId);

 

       // TODO determine the needed types dynamically

       appBarIconButtonType= platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarIconButton");

@@ -103,6 +112,7 @@ namespace BytecodeTranslator.Phone {
       toggleButtonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Primitives", "ToggleButton");

       controlType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Control");

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

+      pivotType = platform.CreateReference(MSPhoneControlsAssembly, "Microsoft", "Phone", "Controls", "Pivot");

 

       trueConstant = new CompileTimeConstant() {

         Type = platform.SystemBoolean,

diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
index f94f0044..2d3533aa 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -13,6 +13,8 @@ namespace BytecodeTranslator.Phone {
     private ITypeReference cancelEventArgsType;

     private ITypeReference typeTraversed;

     private IMethodDefinition methodTraversed;

+    private static HashSet<IMethodDefinition> navCallers= new HashSet<IMethodDefinition>();

+    public static IEnumerable<IMethodDefinition> NavCallers { get { return navCallers; } }

 

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

       this.host = host;

@@ -29,10 +31,13 @@ namespace BytecodeTranslator.Phone {
       cancelEventArgsType = platform.CreateReference(assembly, "System", "ComponentModel", "CancelEventArgs");

     }

 

+    public override void  Visit(IEnumerable<IAssemblyReference> assemblyReferences) {

+ 	    base.Visit(assemblyReferences);

+    }

+

+

     public override void Visit(IMethodDefinition method) {

       if (method.IsConstructor && PhoneTypeHelper.isPhoneApplicationClass(typeTraversed, host)) {

-        // TODO BUG doing this is generating a fresh variable definition somewhere that the BCT then translates into two different (identical) declarations

-        // TODO maybe a bug introduced here or a BCT bug

         string mainPageUri = PhoneCodeHelper.instance().PhonePlugin.getMainPageXAML();

         SourceMethodBody sourceBody = method.Body as SourceMethodBody;

         if (sourceBody != null) {

@@ -41,7 +46,7 @@ namespace BytecodeTranslator.Phone {
             Assignment uriInitAssign = new Assignment() {

               Source = new CompileTimeConstant() {

                 Type = host.PlatformType.SystemString,

-                Value = PhoneControlsPlugin.getURIBase(mainPageUri),

+                Value = UriHelper.getURIBase(mainPageUri),

               },

               Type = host.PlatformType.SystemString,

               Target = new TargetExpression() {

@@ -78,10 +83,13 @@ namespace BytecodeTranslator.Phone {
         navCallFound = false;

         navCallIsStatic = false;

         this.Visit(statement);

-        if (navCallFound && navCallIsStatic) {

-          staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));

-        } else if (navCallFound) {

-          nonStaticNavStmts.Add(statement);

+        if (navCallFound) {

+          navCallers.Add(methodTraversed);

+          if (navCallIsStatic) {

+            staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));

+          } else {

+            nonStaticNavStmts.Add(statement);

+          }

         }

       }

 

@@ -106,6 +114,8 @@ namespace BytecodeTranslator.Phone {
                          UriHelper.isArgumentURILocallyCreatedStaticRoot(expr, host, out target);

           if (!isStatic)

             target = "--Other non inferrable target--";

+          else

+            target = UriHelper.getURIBase(target);

         } catch (InvalidOperationException) { 

         }

       }

@@ -140,11 +150,13 @@ namespace BytecodeTranslator.Phone {
       string target;

       if (isNavigationOnBackKeyPressHandler(methodCall, out target)) {

         PhoneCodeHelper.instance().BackKeyPressNavigates = true;

-        ICollection<string> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed];

-        if (targets == null) {

+        ICollection<string> targets;

+        try {

+          targets= PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed];

+        } catch (KeyNotFoundException) {

           targets = new HashSet<string>();

         }

-        targets.Add(target);

+        targets.Add("\"" + target + "\"");

         PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed]= targets;

       } else if (isCancelOnBackKeyPressHandler(methodCall)) {

         PhoneCodeHelper.instance().BackKeyPressHandlerCancels = true;

@@ -247,7 +259,7 @@ namespace BytecodeTranslator.Phone {
         Assignment currentURIAssign = new Assignment() {

           Source = new CompileTimeConstant() {

             Type = host.PlatformType.SystemString,

-            Value = PhoneControlsPlugin.getURIBase(entry.Item3),

+            Value = UriHelper.getURIBase(entry.Item3).ToLower(),

           },

           Type = host.PlatformType.SystemString,

           Target = new TargetExpression() {

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 2a863aa8..231a21cf 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -327,6 +327,13 @@ namespace BytecodeTranslator {
         System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);

       }

 

+      if (PhoneCodeHelper.instance().PhoneNavigationToggled) {

+        // TODO integrate into the pipeline and spit out the boogie code

+        foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {

+          System.Console.WriteLine(def.ToString());

+        }

+      }

+

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

       Prelude.Emit(writer);

       sink.TranslatedProgram.Emit(writer);

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index aac00d74..924aba5e 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -155,6 +155,7 @@ namespace BytecodeTranslator {
       s = s.Replace('[', '$');

       s = s.Replace(']', '$');

       s = s.Replace('|', '$');

+      s = s.Replace('+', '$');

       s = GetRidOfSurrogateCharacters(s);

       return s;

     }

diff --git a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
index 37b35746..2071ce21 100644
--- a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
+++ b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
@@ -5,7 +5,7 @@ from xml.dom import minidom
 from itertools import product

 import xml.dom

 

-CONTROL_NAMES= ["Button", "CheckBox", "RadioButton"]

+CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton", "Pivot"]

 CONTAINER_CONTROL_NAMES= ["Canvas", "Grid", "StackPanel"]

 

 # TODO externalize strings, share with C# code

@@ -20,6 +20,8 @@ originalPageVars= []
 boogiePageVars= []

 boogiePageClasses= []

 dummyPageVar= "dummyBoogieStringPageName"

+anonymousControlCount= 0;

+ANONYMOUS_CONTROL_PREFIX= "__BOOGIE_ANONYMOUS_CONTROL_"

 

 def showUsage():

   print "PhoneBoogieCodeGenerator -- create boilerplate code for Boogie verification of Phone apps"

@@ -29,7 +31,14 @@ def showUsage():
   print "\t--controls <app_control_info_file>: Phone app control info. See PhoneControlsExtractor. Short form: -c"

   print "\t--output <code_output_file>: file to write with boilerplate code. Short form: -o\n"

 

-def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName):

+def isAnonymousControl(control):

+  name= control["bplName"]

+  return name.find(ANONYMOUS_CONTROL_PREFIX) != -1

+

+def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName):

+  global anonymousControlCount

+  global ANONYMOUS_CONTROL_PREFIX

+

   newControl={}

   newControl["class"]= controlClass

   newControl["enabled"]= enabled

@@ -37,6 +46,11 @@ def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickH
   newControl["clickHandler"]= clickHandler

   newControl["checkedHandler"]= checkedHandler

   newControl["uncheckedHandler"]= uncheckedHandler

+  newControl["selectionChangedHandler"]= selectionChangedHandler

+  if (bplName == ""):

+    # anonymous control, need a dummy boogie var, but we cannot know how it got initialized

+    bplName= ANONYMOUS_CONTROL_PREFIX + str(anonymousControlCount)

+    anonymousControlCount= anonymousControlCount+1

   newControl["bplName"]=bplName

   infoMap[controlName]= newControl

 

@@ -115,7 +129,7 @@ def outputPageControlDriver(file, originalPageName, boogiePageName):
   for entry in staticControlsMap[originalPageName]["controls"].keys():

     controlInfo= staticControlsMap[originalPageName]["controls"][entry]

     if controlInfo["bplName"] == "":

-      continue

+      continue;

     if not ifInitialized:

       file.write("\t\tif ($activeControl == " + str(activeControl) + ") {\n")

       ifInitialized= True

@@ -139,6 +153,10 @@ def outputPageControlDriver(file, originalPageName, boogiePageName):
       file.write("\t\t\t\tif ($handlerToActivate == 2) {\n")

       file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["uncheckedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")

       file.write("\t\t\t\t}\n")

+    if not controlInfo["selectionChangedHandler"] == "":

+      file.write("\t\t\t\tif ($handlerToActivate == 3) {\n")

+      file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["selectionChangedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")

+      file.write("\t\t\t\t}\n")

 

     file.write("\t\t\t}\n")

     file.write("\t\t}\n")

@@ -203,14 +221,14 @@ def buildControlInfo(controlInfoFileName):
 

   file = open(controlInfoFileName, "r")

   # Info file format is first line containing only the main page, another line with boogie's current navigation variable and then one line per

-  # <pageClassName>,<page.xaml file>,<xaml boogie string representation>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<BoogieName>

+  # <pageClassName>,<page.xaml file>,<xaml boogie string representation>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<SelectionChangedValue>,<BoogieName>

   mainPageXAML= file.readline().strip()

   currentNavigationVariable= file.readline().strip()

   mainAppClassname= file.readline().strip()

 

   infoLine= file.readline().strip()

   while not infoLine == "":

-    pageClass, pageName, pageBoogieStringName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName= infoLine.split(",")

+    pageClass, pageName, pageBoogieStringName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName= infoLine.split(",")

     pageInfo={}

     pageInfo["class"]=pageClass

     try:

@@ -224,7 +242,7 @@ def buildControlInfo(controlInfoFileName):
       pageControlInfo= pageInfo["controls"]

     except KeyError:

       pageInfo["controls"]=pageControlInfo

-    loadControlInfo(pageControlInfo, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, bplName)

+    loadControlInfo(pageControlInfo, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName)

     pageInfo["controls"]= pageControlInfo

     staticControlsMap[pageName]=pageInfo

 

diff --git a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
index 9285d6c8..82090e29 100644
--- a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
+++ b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
@@ -4,7 +4,7 @@ import os
 from xml.dom import minidom

 import xml.dom

 

-CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton"]

+CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton", "Pivot"]

 

 # TODO maybe a control is enabled but its parent is not, must take this into account

 # TODO a possible solution is to tie the enabled value to that of the parent in the app until it is either overriden

@@ -70,6 +70,7 @@ def addDummyControlToMap(pageXAML, parentPage):
   newControl["Click"] = ""

   newControl["Checked"] = ""

   newControl["Unchecked"] = ""

+  newControl["SelectionChanged"]= ""

   newControl["XAML"]= pageXAML

   pageControls.append(newControl)

   staticControlsMap[parentPage]= pageControls

@@ -98,6 +99,7 @@ def addControlToMap(pageXAML, parentPage, controlNode):
   newControl["Click"] = controlNode.getAttribute("Click").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)

   newControl["Checked"] = controlNode.getAttribute("Checked").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)

   newControl["Unchecked"] = controlNode.getAttribute("Unchecked").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)

+  newControl["SelectionChanged"] = controlNode.getAttribute("SelectionChanged").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT)

   newControl["XAML"]= pageXAML

   pageControls.append(newControl)

   staticControlsMap[parentPage]= pageControls

@@ -145,7 +147,7 @@ def outputPhoneControls(outputFileName):
   outputFile= open(outputFileName, "w")

 

   # Output format is first line containing only the main page, then line containing boogie navigation variable, and then one line per

-  # <pageClassName>,<page.xaml file>,<boogie string page name>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>

+  # <pageClassName>,<page.xaml file>,<boogie string page name>,<controlClassName>,<controlName (as in field name)>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<SelChangedValue>

   outputFile.write(mainPageXAML + "\n")

   outputFile.write("dummyNavigationVariable_unknown\n")

   outputFile.write("dummyMainAppName_unknown\n") # I could possibly deduce it from WMAppManifest.xml, but I'm unsure. Doing it later is safe anyway

@@ -167,10 +169,14 @@ def outputPhoneControls(outputFileName):
       unchecked= control["Unchecked"]

       if (unchecked.find(COMMA_REPLACEMENT) != -1):

         unchecked= ""

+      selectionChanged= control["SelectionChanged"]

+      if (selectionChanged.find(COMMA_REPLACEMENT) != -1):

+        selectionChanged= ""

       pageXAML= control["XAML"]

       # last comma is to account for bpl translation name, that is unknown for now

       # boogie string page name is unknown for now

-      outputFile.write(page + "," + os.path.basename(pageXAML) + ",dummyBoogieStringPageName," + control["Type"] + "," + control["Name"] + "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + ",\n")

+      outputFile.write(page + "," + os.path.basename(pageXAML) + ",dummyBoogieStringPageName," + control["Type"] + "," + control["Name"] + \

+                       "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + "," + selectionChanged + ",\n")

 

   outputFile.close()

 

diff --git a/BCT/TranslationPlugins/PhoneControlsPlugin.cs b/BCT/TranslationPlugins/PhoneControlsPlugin.cs
index e539b1b8..daa7c345 100644
--- a/BCT/TranslationPlugins/PhoneControlsPlugin.cs
+++ b/BCT/TranslationPlugins/PhoneControlsPlugin.cs
@@ -7,7 +7,7 @@ using System.IO;
 namespace TranslationPlugins {

   public enum Visibility { Visible, Collapsed };

 

-  public enum Event { Click, Checked, Unchecked };

+  public enum Event { Click, Checked, Unchecked, SelectionChanged };

 

   public class HandlerSignature {

     public static string[] getParameterTypesForHandler(Event controlEvent) {

@@ -15,6 +15,7 @@ namespace TranslationPlugins {
         case Event.Checked:

         case Event.Unchecked:

         case Event.Click:

+        case Event.SelectionChanged:

           return new string[] { "object", "System.WindowsRoutedventArgs" };

         default:

           throw new NotImplementedException("Handlers for event: " + controlEvent + " not supported yet");

@@ -94,7 +95,7 @@ namespace TranslationPlugins {
   public class PhoneControlsPlugin : TranslationPlugin {

     // TODO this will probably need a complete rewrite once it is event based, and make it more push than pull

     // TODO but it doesn't make sense right now to make it BCT or CCI aware

-    private static int CONFIG_LINE_FIELDS= 11;

+    private static int CONFIG_LINE_FIELDS= 12;

     private static int PAGE_CLASS_FIELD= 0;

     private static int PAGE_XAML_FIELD= 1;

     private static int PAGE_BOOGIE_STRING_FIELD = 2;

@@ -105,7 +106,8 @@ namespace TranslationPlugins {
     private static int CLICK_HANDLER_FIELD= 7;

     private static int CHECKED_HANDLER_FIELD= 8;

     private static int UNCHECKED_HANDLER_FIELD = 9;

-    private static int BPL_NAME_FIELD = 10;

+    private static int SELECTIONCHANGED_HANDLER_FIELD = 10;

+    private static int BPL_NAME_FIELD = 11;

 

     private IDictionary<string, PageStructure> pageStructureInfo;

 

@@ -125,28 +127,6 @@ namespace TranslationPlugins {
       return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();

     }

 

-    /// <summary>

-    /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)

-    /// This method returns a base URI

-    /// </summary>

-    /// <param name="uri"></param>

-    /// <returns></returns>

-    public static string getURIBase(string uri) {

-      // I need to build an absolute URI just to call getComponents() ...

-      Uri mockBaseUri = new Uri("mock://mock/", UriKind.RelativeOrAbsolute);

-      Uri realUri;

-      try {

-        realUri = new Uri(uri, UriKind.Absolute);

-      } catch (UriFormatException) {

-        // uri string is relative

-        realUri = new Uri(mockBaseUri, uri);

-      }

-

-      string str = realUri.GetComponents(UriComponents.Path | UriComponents.StrongAuthority | UriComponents.Scheme, UriFormat.UriEscaped);

-      Uri mockStrippedUri = new Uri(str);

-      return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();

-    }

-

     //public static string getFullyQualifiedControlClass(string controlClass) {

     //  // TODO do an actual API discovery. The problem will be differencing 7.0 apps from 7.1 apps

     //  return "System.Windows.Controls." + controlClass;

@@ -190,6 +170,7 @@ namespace TranslationPlugins {
     }

 

     private void setPageAsMainPage(string pageXAML) {

+      pageXAML = pageXAML.ToLower();

       int lastDirPos= pageXAML.LastIndexOf('/');

       if (lastDirPos != -1)

         pageXAML = pageXAML.Substring(lastDirPos+1);

@@ -212,14 +193,15 @@ namespace TranslationPlugins {
 

     public void DumpControlStructure(StreamWriter outputStream) {

       // maintain same format as input format

-      string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;

+      string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler,

+             checkedHandler, uncheckedHandler, selectionChangedHandler, bplName;

       outputStream.WriteLine(getMainPageXAML());

       outputStream.WriteLine(getBoogieNavigationVariable());

       outputStream.WriteLine(getMainAppTypeName());

 

       foreach (KeyValuePair<string, PageStructure> entry in this.pageStructureInfo) {

         pageClass = entry.Key;

-        pageXAML = entry.Value.PageXAML;

+        pageXAML = entry.Value.PageXAML.ToLower();

         pageBoogieStringName = entry.Value.PageBoogieName;

         foreach (ControlInfoStructure controlInfo in entry.Value.getAllControlsInfo()) {

           controlClass= controlInfo.ClassName;

@@ -253,8 +235,17 @@ namespace TranslationPlugins {
           } else {

             uncheckedHandler = "";

           }

+

+          handlers = controlInfo.getHandlers(Event.SelectionChanged);

+          if (handlers.Any()) {

+            selectionChangedHandler= handlers.First().Name;

+          } else {

+            selectionChangedHandler = "";

+          }

           bplName = controlInfo.BplName;

-          outputStream.WriteLine(pageClass + "," + pageXAML + "," + pageBoogieStringName + "," + controlClass + "," + controlName + "," + enabled + "," + visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + bplName);

+          outputStream.WriteLine(pageClass + "," + pageXAML.ToLower() + "," + pageBoogieStringName + "," + controlClass + "," + controlName + "," + enabled + "," +

+                                 visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + selectionChangedHandler + "," +

+                                 bplName);

         }

       }

     }

@@ -276,14 +267,15 @@ namespace TranslationPlugins {
       // TODO the page.xaml value is saved with no directory information: if two pages exist with same name but different directories it will treat them as the same

       // TODO I'm not handling this for now, and I won't be handling relative/absolute URI either for now

 

-      string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;

+      string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler,

+             uncheckedHandler, selectionChangedHandler, bplName;

       string configLine = configStream.ReadLine();

       string[] inputLine;

       PageStructure pageStr;

       ControlInfoStructure controlInfoStr;

 

       // first line just states the main page xaml

-      string mainPageXAML= configLine.Trim();

+      string mainPageXAML= configLine.Trim().ToLower();

       configLine = configStream.ReadLine();

 

       // second line states boogie current nav variable, possibly dummy value

@@ -305,7 +297,7 @@ namespace TranslationPlugins {
           throw new ArgumentException("Config input line contains wrong number of fields: " + inputLine.Length + ", expected " + CONFIG_LINE_FIELDS);

 

         pageClass = inputLine[PAGE_CLASS_FIELD].Trim();

-        pageXAML = inputLine[PAGE_XAML_FIELD].Trim();

+        pageXAML = inputLine[PAGE_XAML_FIELD].Trim().ToLower();

         pageBoogieStringName = inputLine[PAGE_BOOGIE_STRING_FIELD].Trim();

         controlClass = inputLine[CONTROL_CLASS_FIELD].Trim();

         controlName = inputLine[CONTROL_NAME_FIELD].Trim();

@@ -317,6 +309,7 @@ namespace TranslationPlugins {
         clickHandler = inputLine[CLICK_HANDLER_FIELD].Trim();

         checkedHandler = inputLine[CHECKED_HANDLER_FIELD].Trim();

         uncheckedHandler = inputLine[UNCHECKED_HANDLER_FIELD].Trim();

+        selectionChangedHandler = inputLine[SELECTIONCHANGED_HANDLER_FIELD].Trim();

         bplName = inputLine[BPL_NAME_FIELD].Trim();

 

         try {

@@ -341,6 +334,7 @@ namespace TranslationPlugins {
         controlInfoStr.setHandler(Event.Click, clickHandler);

         controlInfoStr.setHandler(Event.Checked, checkedHandler);

         controlInfoStr.setHandler(Event.Unchecked, uncheckedHandler);

+        controlInfoStr.setHandler(Event.SelectionChanged, selectionChangedHandler);

 

         pageStr.setControlInfo(controlName, controlInfoStr);

         pageStructureInfo[pageClass] = pageStr;