path: root/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Cci;
using Bpl=Microsoft.Boogie;
using TranslationPlugins;
using Microsoft.Cci.MutableCodeModel;
using System.IO;
using ILGarbageCollect;

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);
      /* 
      Uri relativeUri = mockBaseUri.MakeRelativeUri(mockStrippedUri);
      return relativeUri.ToString();
       */
      // TODO PATCH this works for now because we are ignoring non-flat XAML structures
      return mockStrippedUri.Segments.Last();
    }

    /// <summary>
    /// checks if argument is locally created URI with static URI target
    /// </summary>
    /// <param name="arg"></param>
    /// <returns></returns>
    public static bool isArgumentURILocallyCreatedStatic(IExpression arg, IMetadataHost host, out string uri) {
      uri = null;
      ICreateObjectInstance creationSite = arg as ICreateObjectInstance;
      if (creationSite == null)
        return false;

      if (!arg.Type.isURIClass(host))
        return false;

      IExpression uriTargetArg = creationSite.Arguments.First();

      if (!uriTargetArg.Type.isStringClass(host))
        return false;

      ICompileTimeConstant staticURITarget = uriTargetArg as ICompileTimeConstant;
      if (staticURITarget == null)
        return false;

      uri= staticURITarget.Value as string;
      return true;
    }

    /// <summary>
    /// checks if argument is locally created URI where target has statically created URI root
    /// </summary>
    /// <param name="arg"></param>
    /// <returns></returns>
    public static bool isArgumentURILocallyCreatedStaticRoot(IExpression arg, IMetadataHost host, out string uri) {
      // Pre: !isArgumentURILocallyCreatedStatic
      uri = null;
      ICreateObjectInstance creationSite = arg as ICreateObjectInstance;
      if (creationSite == null)
        return false;

      if (!arg.Type.isURIClass(host))
        return false;

      IExpression uriTargetArg = creationSite.Arguments.First();

      if (!uriTargetArg.Type.isStringClass(host))
        return false;

      if (!uriTargetArg.IsStaticURIRootExtractable(out uri))
        return false;

      return true;
    }

    
    /// <summary>
    /// checks whether a static URI root (a definite page base) can be extracted from the expression 
    /// </summary>
    /// <param name="expr"></param>
    /// <returns></returns>
    public static bool IsStaticURIRootExtractable(this IExpression expr, out string uri) {
      // Pre expr.type == string
      IMethodCall stringConcatExpr = expr as IMethodCall;
      uri = null;
      if (stringConcatExpr == null)
        return false;

      if (stringConcatExpr.MethodToCall.Name.Value != "Concat")
        return false;

      IList<string> constantStrings = new List<string>();

      // TODO this misses so many "static" strings, but let's start with this for now
      IExpression leftOp = stringConcatExpr.Arguments.FirstOrDefault();
      while (leftOp != null && leftOp is ICompileTimeConstant) {
        ICompileTimeConstant strConst = leftOp as ICompileTimeConstant;
        constantStrings.Add(strConst.Value as string);
        if (stringConcatExpr.Arguments.ToList()[1] is IMethodCall) {
          stringConcatExpr = stringConcatExpr.Arguments.ToList()[1] as IMethodCall;
          leftOp = stringConcatExpr.Arguments.FirstOrDefault();
        } else if (stringConcatExpr.Arguments.ToList()[1] is ICompileTimeConstant) {
          constantStrings.Add((stringConcatExpr.Arguments.ToList()[1] as ICompileTimeConstant).Value as string);
          break;
        } else {
          break;
        }
      }

      if (constantStrings.Count > 0) {
        uri = constantStrings.Aggregate((aggr, elem) => aggr + elem);
        return Uri.IsWellFormedUriString(uri, UriKind.RelativeOrAbsolute);
      } else {
        return false;
      }
    }
  }

  public static class PhoneTypeHelper {
    public static IAssemblyReference getSystemAssemblyReference(IMetadataHost host) {
      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
      IAssemblyReference coreAssemblyRef = platform.CoreAssemblyRef;
      AssemblyIdentity MSPhoneSystemAssemblyId =
          new AssemblyIdentity(host.NameTable.GetNameFor("System"), coreAssemblyRef.Culture, coreAssemblyRef.Version,
                               coreAssemblyRef.PublicKeyToken, "");
      return host.FindAssembly(MSPhoneSystemAssemblyId);
    }

    public static IAssemblyReference getCoreAssemblyReference(IMetadataHost host) {
      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
      return platform.CoreAssemblyRef;
    }

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

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

    public static bool isPhoneApplicationClass(this ITypeReference typeRef, IMetadataHost host) {
      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
      IAssemblyReference systemAssembly = PhoneTypeHelper.getSystemWindowsAssemblyReference(host);
      ITypeReference applicationClass = platform.CreateReference(systemAssembly, "System", "Windows", "Application");
      return typeRef.isClass(applicationClass);
    }

    public static bool isPhoneApplicationPageClass(this ITypeReference typeRef, IMetadataHost host) {
      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
      IAssemblyReference phoneAssembly = PhoneTypeHelper.getPhoneAssemblyReference(host);
      ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Controls", "PhoneApplicationPage");

      return typeRef.isClass(phoneApplicationPageTypeRef);
    }

    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, IMetadataHost host) {
      ITypeReference targetType = host.PlatformType.SystemString;
      return typeRef.isClass(targetType);
    }

    public static bool isURIClass(this ITypeReference typeRef, IMetadataHost 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 isNavigationServiceClass(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, "System", "Windows", "Navigation", "NavigationService");

      return typeRef.isClass(phoneApplicationPageTypeRef);
    }

    public static bool isRoutedEventHandlerClass(this ITypeReference typeRef, IMetadataHost host) {
      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; ;
      IAssemblyReference systemAssembly = getSystemWindowsAssemblyReference(host);
      ITypeReference routedEvHandlerType = platform.CreateReference(systemAssembly, "System", "Windows", "RoutedEventHandler");
      return typeRef.isClass(routedEvHandlerType);

    }

    public static bool isMessageBoxClass(this ITypeReference typeRef, IMetadataHost host) {
      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; ;
      IAssemblyReference systemAssembly = getSystemWindowsAssemblyReference(host);
      ITypeReference mbType = platform.CreateReference(systemAssembly, "System", "Windows", "MessageBox");
      return typeRef.isClass(mbType);
    }

  }

  public enum StaticURIMode {
    NOT_STATIC, STATIC_URI_CREATION_ONSITE, STATIC_URI_ROOT_CREATION_ONSITE,
  }

  public class PhoneCodeHelper {
    // TODO refactor into Feedbakc and Navigation specific code, this is already a mess
    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__";
    public const string BOOGIE_NAVIGATION_CHECK_VARIABLE = BOOGIE_VAR_PREFIX + "Navigated__";
    public const string BOOGIE_STARTING_URI_PLACEHOLDER = "BOOGIE_STARTING_URI_PLACEHOLDER";
    public const string BOOGIE_ENDING_URI_PLACEHOLDER= "BOOGIE_ENDING_URI_PLACEHOLDER";

    public static readonly string[] NAV_CALLS = { /*"GoBack", "GoForward", "Navigate", "StopLoading"*/ "Navigate", "GoBack" };

    public bool OnBackKeyPressOverriden { get; set; }
    public bool BackKeyPressHandlerCancels { get { return BackKeyCancellingOffenders.Count > 0; } }
    public bool BackKeyPressNavigates { get { return BackKeyNavigatingOffenders.Keys.Count > 0; } }
    public bool BackKeyHandlerOverridenByUnknownDelegate { get; set; }
    public ICollection<Tuple<ITypeReference,string>> BackKeyCancellingOffenders { get; set; }
    public ICollection<ITypeReference> BackKeyUnknownDelegateOffenders { get; set; }
    public Dictionary<ITypeReference, ICollection<Tuple<IMethodReference,string>>> BackKeyNavigatingOffenders { get; set; }
    public ICollection<IMethodReference> KnownBackKeyHandlers { get; set; }
    public ICollection<IMethodReference> KnownNavigatingMethods { get; set; }
    public ICollection<IMethodReference> KnownEventCancellingMethods { get; set; }

    private Dictionary<string, string[]> PHONE_UI_CHANGER_METHODS;

    private static IMetadataHost host;
    private Microsoft.Cci.Immutable.PlatformType platform;
    private static PhoneCodeHelper _instance;
    private static bool initialized= false;

    public static void initialize(IMetadataHost host) {
      if (initialized)
        return;

      PhoneCodeHelper.host = host;
      initialized = true;
    }

    public static PhoneCodeHelper instance() {
      if (_instance == null) {
        _instance = new PhoneCodeHelper(host);
      }

      return _instance;
    }

    private PhoneCodeHelper(IMetadataHost host) {
      if (host != null) {
        platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
        initializeKnownUIChangers();

        BackKeyCancellingOffenders= new HashSet<Tuple<ITypeReference,string>>();
        BackKeyUnknownDelegateOffenders = new HashSet<ITypeReference>();
        BackKeyNavigatingOffenders = new Dictionary<ITypeReference, ICollection<Tuple<IMethodReference,string>>>();
        KnownBackKeyHandlers = new HashSet<IMethodReference>();
        KnownNavigatingMethods = new HashSet<IMethodReference>();
        KnownEventCancellingMethods = new HashSet<IMethodReference>();
      }
    }

    private void initializeKnownUIChangers() {
      PHONE_UI_CHANGER_METHODS= new Dictionary<string,string[]>();
      IAssemblyReference systemAssembly = PhoneTypeHelper.getSystemAssemblyReference(host);
      IAssemblyReference systemWinAssembly = PhoneTypeHelper.getSystemWindowsAssemblyReference(host);
      IAssemblyReference phoneAssembly = PhoneTypeHelper.getPhoneAssemblyReference(host);
      
      ITypeReference textBoxType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "TextBox");
      PHONE_UI_CHANGER_METHODS[textBoxType.ToString()] =
        new string[] {"set_BaselineOffset", "set_CaretBrush", "set_FontSource", "set_HorizontalScrollBarVisibility", "set_IsReadOnly", "set_LineHeight",
                      "set_LineStackingStrategy", "set_MaxLength", "set_SelectedText", "set_SelectionBackground", "set_SelectionForeground", "set_SelectionLength",
                      "set_SelectionStart", "set_Text", "set_TextAlignment", "set_TextWrapping", "set_VerticalScrollBarVisibility", "set_Watermark",
                     };
      
      ITypeReference textBlockType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "TextBlock");
      PHONE_UI_CHANGER_METHODS[textBlockType.ToString()] =
        new string[] {"set_BaselineOffset", "set_FontFamily", "set_FontSize", "set_FontSource", "set_FontStretch", "set_FontStyle", "set_FontWeight", "set_Foreground",
                      "set_CharacterSpacing", "set_LineHeight", "set_LineStackingStrategy", "set_Padding", "set_Text", "set_TextAlignment", "set_TextDecorations",
                      "set_TextTrimming", "set_TextWrapping", 
                     };

      ITypeReference uiElementType = platform.CreateReference(systemAssembly, "System", "Windows", "UIElement");
      PHONE_UI_CHANGER_METHODS[uiElementType.ToString()] =
        new string[] {"set_Clip", "set_Opacity", "set_OpacityMask", "set_Projection", "set_RenderTransform",
                      "set_RenderTransformOrigin", "set_Visibility", "Arrange", "InvalidateArrange", "InvalidateMeasure", "SetValue", "ClearValue", // Set/ClearValue are quite unsafe
                      "UpdateLayout", "Measure",
                     };

      ITypeReference frameworkElementType = platform.CreateReference(systemAssembly, "System", "Windows", "FrameworkElement");
      PHONE_UI_CHANGER_METHODS[frameworkElementType.ToString()] =
        new string[] {"set_FlowDirection", "set_Height", "set_HorizontalAlignment", "set_Language", "set_Margin", "set_MaxHeight", "set_MaxWidth",
                      "set_MinHeight", "set_MinWidth", "set_Style", "set_VerticalAlignment", "set_Width", "set_Cursor", 
                     };

      ITypeReference borderType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Border");
      PHONE_UI_CHANGER_METHODS[borderType.ToString()] =
        new string[] {"set_Background", "set_BorderBrush", "set_BorderThickness", "set_CornerRadius", "set_Padding", 
                     };

      ITypeReference controlType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Control");
      PHONE_UI_CHANGER_METHODS[controlType.ToString()] =
        new string[] {"set_Background", "set_BorderBrush", "set_BorderThickness", "set_CharacterSpacing", "set_FontFamily", "set_FontSize", "set_FontStretch",
                      "set_FontStyle", "set_FontWeight", "set_Foreground", "set_HorizontalContentAlignment", "set_IsEnabled", "set_Padding", "set_VerticalContentAlignment",
                     };

      ITypeReference contentControlType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "ContentControl");
      PHONE_UI_CHANGER_METHODS[contentControlType.ToString()] = new string[] { "set_Content", };

      ITypeReference panelType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Panel");
      PHONE_UI_CHANGER_METHODS[panelType.ToString()] = new string[] { "set_Background", };

      ITypeReference canvasType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Canvas");
      PHONE_UI_CHANGER_METHODS[canvasType.ToString()] = new string[] { "set_Left", "set_Top", "set_ZIndex", };

      ITypeReference toggleButtonType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Primitives", "ToggleButton");
      PHONE_UI_CHANGER_METHODS[toggleButtonType.ToString()] = new string[] { "set_IsChecked", };

      ITypeReference gridType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Grid");
      PHONE_UI_CHANGER_METHODS[gridType.ToString()] = new string[] { "set_ShowGridLines",  "set_Column", "set_ColumnSpan", "set_Row", "set_RowSpan", };

      ITypeReference imageType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Image");
      PHONE_UI_CHANGER_METHODS[imageType.ToString()] = new string[] { "set_Source", "set_Stretch", };

      ITypeReference inkPresenterType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "InkPresenter");
      PHONE_UI_CHANGER_METHODS[inkPresenterType.ToString()] = new string[] { "set_Strokes", };

      ITypeReference itemsControlType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "ItemsControl");
      PHONE_UI_CHANGER_METHODS[itemsControlType.ToString()] = new string[] { "set_DisplayMemberPath", "set_ItemsSource", "set_ItemTemplate", };

      ITypeReference selectorType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Primitives", "Selector");
      PHONE_UI_CHANGER_METHODS[selectorType.ToString()] =
        new string[] { "set_SelectedIndex", "set_SelectedItem", "set_SelectedValue", "set_SelectedValuePath", };

      ITypeReference listBoxType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "ListBox");
      PHONE_UI_CHANGER_METHODS[listBoxType.ToString()] = new string[] { "set_ItemContainerStyle", };

      ITypeReference passwordBoxType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "PasswordBox");
      PHONE_UI_CHANGER_METHODS[passwordBoxType.ToString()] =
        new string[] { "set_CaretBrush", "set_FontSource", "set_MaxLength", "set_Password", "set_PasswordChar",
                       "set_SelectionBackground", "set_SelectionForeground",
                     };

      ITypeReference rangeBaseType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Primitives", "RangeBase");
      PHONE_UI_CHANGER_METHODS[rangeBaseType.ToString()] = new string[] { "set_LargeChange", "set_Maximum", "set_Minimum", "set_SmallChange", "set_Value", };

      ITypeReference progressBarType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "ProgressBar");
      PHONE_UI_CHANGER_METHODS[progressBarType.ToString()] = new string[] { "set_IsIndeterminate", };

      ITypeReference sliderType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Slider");
      PHONE_UI_CHANGER_METHODS[sliderType.ToString()] = new string[] { "set_IsDirectionReversed", "set_Orientation", };

      ITypeReference stackPanelType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "StackPanel");
      PHONE_UI_CHANGER_METHODS[stackPanelType.ToString()] = new string[] { "set_Orientation", };

      ITypeReference richTextBoxType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "RichTextBox");
      PHONE_UI_CHANGER_METHODS[richTextBoxType.ToString()] =
        new string[] { "set_BaselineOffset", "set_CaretBrush", "set_HorizontalScrollBartVisibility", "set_LineHeight", "set_LineStackingStrategy",
                       "set_TextAlignment", "set_TextWrapping", "set_VerticalScrollBarVisibility", "set_Xaml", };

      ITypeReference webBrowserTaskType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Tasks", "WebBrowserTask");
      PHONE_UI_CHANGER_METHODS[webBrowserTaskType.ToString()] = new string[] { "Show", };

      ITypeReference appBarIconButtonType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarIconButton");
      PHONE_UI_CHANGER_METHODS[appBarIconButtonType.ToString()] = new string[] { "set_IsEnabled", "set_IconUri", "set_Text", };

      ITypeReference appBarMenuItemType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarMenuItem");
      PHONE_UI_CHANGER_METHODS[appBarMenuItemType.ToString()] = new string[] { "set_IsEnabled", "set_Text", };

      ITypeReference emailComposeTaskType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Tasks", "EmailComposeTask");
      PHONE_UI_CHANGER_METHODS[emailComposeTaskType.ToString()] = new string[] { "Show", };

      ITypeReference scaleTransformType = platform.CreateReference(systemWinAssembly, "System", "Windows", "Media", "ScaleTransform");
      PHONE_UI_CHANGER_METHODS[scaleTransformType.ToString()] = new string[] { "set_CenterX", "set_CenterY", "set_ScaleX", "set_ScaleY",  };
    }

    // TODO externalize strings
    public static readonly string[] IgnoredEvents =
    { "Loaded",
    };

    // 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 PhoneControlsPlugin PhonePlugin { get; set; }
    private IDictionary<string, Bpl.NamedDeclaration> boogieObjects = new Dictionary<string, Bpl.NamedDeclaration>();

    public 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 bool setBoogieObjectForName(string name, Bpl.NamedDeclaration bplObject) {
      bool ret = true;
      if (boogieObjects.ContainsKey(name))
        ret = false;

      boogieObjects[name] = bplObject;
      return ret;
    }

    private bool isPhoneUIChangerClass(ITypeReference typeRef) {
      return PHONE_UI_CHANGER_METHODS.Keys.Contains(typeRef.ToString());
    }

    public bool isNavigationCall(IMethodCall call) {
      ITypeReference callType = call.MethodToCall.ContainingType;
      if (!callType.isNavigationServiceClass(host))
        return false;

      return NAV_CALLS.Contains(call.MethodToCall.Name.Value);
    }

    private ITypeReference mainAppTypeRef;
    public void setMainAppTypeReference(ITypeReference appType) {
      mainAppTypeRef = appType;
    }

    public ITypeReference getMainAppTypeReference() {
      return mainAppTypeRef;
    }

    public void setBoogieNavigationVariable(string var) {
      PhonePlugin.setBoogieNavigationVariable(var);
    }

    public string getBoogieNavigationVariable() {
      return PhonePlugin.getBoogieNavigationVariable();
    }

    public string getXAMLForPage(string pageClass) {
      return PhonePlugin.getXAMLForPage(pageClass);
    }

    public void setBoogieStringPageNameForPageClass(string pageClass, string boogieStringName) {
      PhonePlugin.setBoogieStringPageNameForPageClass(pageClass, boogieStringName);
    }

    public void setMainAppTypeName(string fullyQualifiedName) {
      PhonePlugin.setMainAppTypeName(fullyQualifiedName);
    }

    public string getMainAppTypeName() {
      return PhonePlugin.getMainAppTypeName();
    }

    public Bpl.AssignCmd createBoogieNavigationUpdateCmd(Sink sink) {
      // the block is a potential page changer
      List<Bpl.AssignLhs> lhs = new List<Bpl.AssignLhs>();
      List<Bpl.Expr> rhs = new List<Bpl.Expr>();
      Bpl.Expr value = new Bpl.LiteralExpr(Bpl.Token.NoToken, false);
      rhs.Add(value);
      Bpl.SimpleAssignLhs assignee =
        new Bpl.SimpleAssignLhs(Bpl.Token.NoToken,
                                new Bpl.IdentifierExpr(Bpl.Token.NoToken,
                                                       sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_CONTINUE_ON_PAGE_VARIABLE, Bpl.Type.Bool)));
      lhs.Add(assignee);
      Bpl.AssignCmd assignCmd = new Bpl.AssignCmd(Bpl.Token.NoToken, lhs, rhs);
      return assignCmd;
    }

    // TODO do away with these whenever it is possible to make repeated passes at the translator, and handle from Program
    public bool PhoneNavigationToggled { get; set; }
    public bool PhoneFeedbackToggled { get; set; }

    public bool isMethodInputHandlerOrFeedbackOverride(IMethodDefinition method) {
      // FEEDBACK TODO: This is extremely coarse. There must be quite a few non-UI routed/non-routed events
      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; ;
      IAssemblyReference coreAssembly= PhoneTypeHelper.getCoreAssemblyReference(host);
      ITypeReference eventArgsType= platform.CreateReference(coreAssembly, "System", "EventArgs");
      foreach (IParameterDefinition paramDef in method.Parameters) {
        if (paramDef.Type.isClass(eventArgsType))
          return true;
      }

      return false;
    }

    public bool isMethodKnownUIChanger(IMethodCall methodCall) {
      // FEEDBACK TODO join these two with the others
      if (methodCall.MethodToCall.ContainingType.isNavigationServiceClass(host)) {
        return NAV_CALLS.Contains(methodCall.MethodToCall.Name.Value);
      } else if (methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.isMessageBoxClass(host) &&
                 methodCall.MethodToCall.Name.Value == "Show") {
        return true;
      }

      // otherwise, it must be a control input call
      // before any method call checks, make sure the receiving object is a Control
      IExpression callee = methodCall.ThisArgument;
      if (callee == null)
        return false;

      ITypeReference calleeType = callee.Type;
      while (calleeType.ResolvedType.BaseClasses.Any()) {
        if (isPhoneUIChangerClass(calleeType) && isKnownUIChanger(calleeType, methodCall)) {
          return true;
        }

        calleeType = calleeType.ResolvedType.BaseClasses.First();
      }

      return false;
    }

    private bool isKnownUIChanger(ITypeReference typeRef, IMethodCall call) {
      string methodName= call.MethodToCall.Name.Value;
      IEnumerable<String> methodsForType = PHONE_UI_CHANGER_METHODS[typeRef.ToString()];
      return methodsForType != null && methodsForType.Contains(methodName);
    }

    private HashSet<string> ignoredHandlers = new HashSet<string>();
    public void ignoreEventHandler(string fullyQualifiedEventHandler) {
      ignoredHandlers.Add(fullyQualifiedEventHandler);
    }

    public bool isMethodIgnoredForFeedback(IMethodDefinition methodTranslated) {
      INamespaceTypeDefinition type= methodTranslated.ContainingType.ResolvedType as INamespaceTypeDefinition;

      if (type == null)
        return false;

      string methodName = type.ContainingUnitNamespace.Name.Value + "." + type.Name + "." + methodTranslated.Name.Value;
      return ignoredHandlers.Contains(methodName);
    }

    private HashSet<Bpl.Procedure> callableMethods = new HashSet<Bpl.Procedure>();
    public void trackCallableMethod(Bpl.Procedure proc) {
      callableMethods.Add(proc);
    }

    public IEnumerable<Bpl.Procedure> getCallableMethods() {
      return callableMethods;
    }

    public void CreateFeedbackCallingMethods(Sink sink) {
      Bpl.Program translatedProgram= sink.TranslatedProgram;
      foreach (Bpl.Procedure proc in callableMethods) {
        addMethodCalling(proc, translatedProgram, sink);
      }
    }

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

      // FEEDBACK TODO this is possibly too much, I'm guessing sometimes this args might well be null
      Bpl.Expr notNullExpr;
      foreach (Bpl.IdentifierExpr idExpr in identVars) {
        if (idExpr.Type.Equals(sink.Heap.RefType)) {
          notNullExpr= Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, idExpr, Bpl.Expr.Ident(sink.Heap.NullRef));
          codeBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, notNullExpr));
        }
      }

      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 bool isBackKeyPressOverride(IMethodDefinition method) {
      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;
    }

    public bool mustInlineMethod(IMethodDefinition method) {
      if (PhoneFeedbackToggled) {
        // FEEDBACK TODO this may be too coarse
        // top level inlined methods are feedback relevant ones. For now, this is basically everything that has EventArgs as parameters
        if (isMethodInputHandlerOrFeedbackOverride(method))
          return true;
      }

      if (PhoneNavigationToggled) {
        // NAVIGATION TODO this may be too coarse
        // for now, assume any method in a PhoneApplicationPage is potentially interesting to navigation inlining
        ITypeReference methodContainer = method.ContainingType;
        if (PhoneTypeHelper.isPhoneApplicationClass(methodContainer, host) || PhoneTypeHelper.isPhoneApplicationPageClass(methodContainer, host))
          return true;
      }

      return false;
    }

    public void createQueriesBatchFile(Sink sink, string sourceBPLFile) {
      StreamWriter outputStream = new StreamWriter("createQueries.bat");
      IEnumerable<string> xamls= PhonePlugin.getPageXAMLFilenames();
      string startURI= sink.FindOrCreateConstant(BOOGIE_STARTING_URI_PLACEHOLDER).Name;
      string endURI = sink.FindOrCreateConstant(BOOGIE_ENDING_URI_PLACEHOLDER).Name;
      foreach (string x1 in xamls) {
        string startURIVar= sink.FindOrCreateConstant(x1).Name.ToLower();
        foreach (string x2 in xamls) {
          string resultFile = sourceBPLFile + "_$$" + x1 + "$$_$$" + x2 + "$$.bpl";
          string endURIVar= sink.FindOrCreateConstant(x2).Name.ToLower();
          outputStream.WriteLine("sed s/" + startURI + ";/" + startURIVar + ";/g " + sourceBPLFile + "> " + resultFile);
          outputStream.WriteLine("sed -i s/" + endURI + ";/" + endURIVar + ";/g " + resultFile);
        }
      }

      outputStream.Close();
    }


    public Bpl.Procedure addHandlerStubCaller(Sink sink, IMethodDefinition def) {
      MethodBody callerBody = new MethodBody();
      MethodDefinition callerDef = new MethodDefinition() {
        InternFactory = (def as MethodDefinition).InternFactory,
        ContainingTypeDefinition = def.ContainingTypeDefinition,
        IsStatic = true,
        Name = sink.host.NameTable.GetNameFor("BOOGIE_STUB_CALLER_" + def.Name.Value),
        Type = sink.host.PlatformType.SystemVoid,
        Body = callerBody,
      };
      callerBody.MethodDefinition = callerDef;
      Sink.ProcedureInfo procInfo = sink.FindOrCreateProcedure(def);
      Sink.ProcedureInfo callerInfo = sink.FindOrCreateProcedure(callerDef);

      Bpl.LocalVariable[] localVars = new Bpl.LocalVariable[procInfo.Decl.InParams.Length];
      Bpl.IdentifierExpr[] varExpr = new Bpl.IdentifierExpr[procInfo.Decl.InParams.Length];
      for (int i = 0; i < procInfo.Decl.InParams.Length; i++) {
        Bpl.LocalVariable loc = new Bpl.LocalVariable(Bpl.Token.NoToken,
                                                     new Bpl.TypedIdent(Bpl.Token.NoToken, TranslationHelper.GenerateTempVarName(),
                                                                        procInfo.Decl.InParams[i].TypedIdent.Type));
        localVars[i] = loc;
        varExpr[i] = new Bpl.IdentifierExpr(Bpl.Token.NoToken, loc);
      }

      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();
      builder.Add(getResetNavigationCheck(sink));
      
      string pageXaml= PhoneCodeHelper.instance().PhonePlugin.getXAMLForPage(def.ContainingTypeDefinition.ToString());
      Bpl.Variable boogieCurrentURI = sink.FindOrCreateFieldVariable(PhoneCodeHelper.CurrentURIFieldDefinition);
      Bpl.Constant boogieXamlConstant;
      if (pageXaml != null)
        boogieXamlConstant = sink.FindOrCreateConstant(pageXaml);
      else
        boogieXamlConstant = null;
      // NAVIGATION TODO: For now just assume we are in this page to be able to call the handler, this is NOT true for any handler
      // NAVIGATION TODO: ie, a network event handler
      if (boogieXamlConstant != null) {
        Bpl.AssumeCmd assumeCurrentPage =
          new Bpl.AssumeCmd(Bpl.Token.NoToken,
                            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieCurrentURI),
                                            new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieXamlConstant)));
        builder.Add(assumeCurrentPage);
      }

      // NAVIGATION TODO: have to do the pair generation all in one go instead of having different files that need to be sed'ed
      boogieXamlConstant = sink.FindOrCreateConstant(BOOGIE_STARTING_URI_PLACEHOLDER);
      Bpl.AssumeCmd assumeStartPage = new Bpl.AssumeCmd(Bpl.Token.NoToken,
                            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieCurrentURI),
                                            new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieXamlConstant)));
      builder.Add(assumeStartPage);
      builder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, procInfo.Decl.Name, new Bpl.ExprSeq(varExpr), new Bpl.IdentifierExprSeq()));
      boogieXamlConstant = sink.FindOrCreateConstant(BOOGIE_ENDING_URI_PLACEHOLDER);
      Bpl.AssertCmd assertEndPage = new Bpl.AssertCmd(Bpl.Token.NoToken,
                            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieCurrentURI),
                                            new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieXamlConstant)));

      Bpl.Expr guard= new Bpl.IdentifierExpr(Bpl.Token.NoToken, sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_NAVIGATION_CHECK_VARIABLE, Bpl.Type.Bool));
      Bpl.StmtListBuilder thenBuilder = new Bpl.StmtListBuilder();
      thenBuilder.Add(assertEndPage);
      Bpl.IfCmd ifNavigated = new Bpl.IfCmd(Bpl.Token.NoToken, guard, thenBuilder.Collect(Bpl.Token.NoToken), null, new Bpl.StmtListBuilder().Collect(Bpl.Token.NoToken));

      builder.Add(ifNavigated);
      Bpl.Implementation impl =
        new Bpl.Implementation(Bpl.Token.NoToken, callerInfo.Decl.Name, new Bpl.TypeVariableSeq(), new Bpl.VariableSeq(),
                               new Bpl.VariableSeq(), new Bpl.VariableSeq(localVars), builder.Collect(Bpl.Token.NoToken), null, new Bpl.Errors());

      sink.TranslatedProgram.TopLevelDeclarations.Add(impl);
      return impl.Proc;
    }

    public static void updateInlinedMethods(Sink sink, IEnumerable<IMethodDefinition> doInline) {
      foreach (IMethodDefinition method in doInline) {
        Sink.ProcedureInfo procInfo = sink.FindOrCreateProcedure(method);
        procInfo.Decl.AddAttribute("inline", new Bpl.LiteralExpr(Bpl.Token.NoToken, Microsoft.Basetypes.BigNum.ONE));
      }
    }

    public static FieldDefinition CurrentURIFieldDefinition {get; set;}

    public void addNavigationUriHavocer(Sink sink) {
      Sink.ProcedureInfo procInfo = sink.FindOrCreateProcedure(getUriHavocerMethod(sink).ResolvedMethod);
      procInfo.Decl.AddAttribute("inline", new Bpl.LiteralExpr(Bpl.Token.NoToken, Microsoft.Basetypes.BigNum.ONE));
      Bpl.StmtListBuilder builder= new Bpl.StmtListBuilder();
      Bpl.HavocCmd havoc=
        new Bpl.HavocCmd(Bpl.Token.NoToken,
                         new Bpl.IdentifierExprSeq(new Bpl.IdentifierExprSeq(new Bpl.IdentifierExpr(Bpl.Token.NoToken,
                                                                             sink.FindOrCreateFieldVariable(PhoneCodeHelper.CurrentURIFieldDefinition)))));
      builder.Add(havoc);
      Bpl.Implementation impl = new Bpl.Implementation(Bpl.Token.NoToken, procInfo.Decl.Name, new Bpl.TypeVariableSeq(),
                                                       new Bpl.VariableSeq(), new Bpl.VariableSeq(), new Bpl.VariableSeq(),
                                                       builder.Collect(Bpl.Token.NoToken));
      sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

    }

    private IMethodReference uriHavocMethod=null;
    public IMethodReference getUriHavocerMethod(Sink sink) {
      if (uriHavocMethod == null) {
        MethodBody body = new MethodBody();
        MethodDefinition havocDef = new MethodDefinition() {
          InternFactory = host.InternFactory,
          ContainingTypeDefinition = PhoneCodeHelper.instance().getMainAppTypeReference().ResolvedType,
          IsStatic = true,
          Name = sink.host.NameTable.GetNameFor(PhoneCodeHelper.BOOGIE_DO_HAVOC_CURRENTURI),
          Type = sink.host.PlatformType.SystemVoid,
          Body = body,
        };
        body.MethodDefinition = havocDef;
        uriHavocMethod = havocDef;
      }

      return uriHavocMethod;
    }

    public Bpl.Cmd getResetNavigationCheck(Sink sink) {
      return getNavigationCheckAssign(sink, false);
    }
    
    public Bpl.Cmd getAddNavigationCheck(Sink sink) {
      return getNavigationCheckAssign(sink, true);
    }

    private Bpl.Cmd getNavigationCheckAssign(Sink sink, bool value) {
      List<Bpl.AssignLhs> lhs = new List<Bpl.AssignLhs>();
      List<Bpl.Expr> rhs = new List<Bpl.Expr>();
      Bpl.AssignLhs assignee = new Bpl.SimpleAssignLhs(Bpl.Token.NoToken, new Bpl.IdentifierExpr(Bpl.Token.NoToken,
                               sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_NAVIGATION_CHECK_VARIABLE, Bpl.Type.Bool)));
      lhs.Add(assignee);
      rhs.Add(value ? Bpl.IdentifierExpr.True : Bpl.IdentifierExpr.False);
      Bpl.AssignCmd assignCmd = new Bpl.AssignCmd(Bpl.Token.NoToken, lhs, rhs);
      return assignCmd;
    }

    public bool isKnownBackKeyOverride(IMethodReference method) {
      return isBackKeyPressOverride(method.ResolvedMethod) ||
             KnownBackKeyHandlers.Contains(method);
    }

    internal IEnumerable<IMethodDefinition> getIndirectNavigators(IEnumerable<IModule> modules, IMethodReference method) {
      IEnumerable<IMethodDefinition> reachable = getReachableMethodsFromMethod(method, modules);
      reachable= reachable.Except(new IMethodDefinition[] { method.ResolvedMethod });
      return getResolvedMethods(KnownNavigatingMethods).Intersect(reachable);
    }

    internal IEnumerable<IMethodDefinition> getIndirectCancellations(IEnumerable<IModule> modules, IMethodReference method) {
      IEnumerable<IMethodDefinition> reachable = getReachableMethodsFromMethod(method, modules);
      reachable = reachable.Except(new IMethodDefinition[] { method.ResolvedMethod });
      return getResolvedMethods(KnownEventCancellingMethods).Intersect(reachable);
    }

    internal IEnumerable<IMethodDefinition> getReachableMethodsFromMethod(IMethodReference method, IEnumerable<IModule> modules) {
      IEnumerable<IAssembly> assemblies = getAssembliesFromModules(modules);
      Microsoft.Cci.MetadataReaderHost readerHost = host as Microsoft.Cci.MetadataReaderHost;

      if (readerHost == null)
        return new List<IMethodDefinition>(); //?

      ILGarbageCollect.Mark.WholeProgram program = new ILGarbageCollect.Mark.WholeProgram(assemblies, readerHost);
      RapidTypeAnalysis analyzer = new RapidTypeAnalysis(program, TargetProfile.Phone);
      analyzer.Run(new IMethodReference[] { method });
      return analyzer.ReachableMethods();
    }

    internal IEnumerable<IAssembly> getAssembliesFromModules(IEnumerable<IModule> modules) {
      IList<IAssembly> assemblies = new List<IAssembly>();
      foreach (IModule module in modules) {
        IAssembly assembly = module as IAssembly;
        if (assembly != null)
          assemblies.Add(assembly);
      }

      return assemblies;
    }

    internal IEnumerable<IMethodDefinition> getResolvedMethods(IEnumerable<IMethodReference> methRefs) {
      IList<IMethodDefinition> methDefs = new List<IMethodDefinition>();
      foreach (IMethodReference methRef in methRefs) {
        methDefs.Add(methRef.ResolvedMethod);
      }

      return methDefs;
    }
  }
}