(phone bct) compute fixpoint for necessary inlined methods (for modular analysis)

4 files changed, 117 insertions, 29 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index bf2a1078..98d716b6 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -128,6 +128,7 @@
     <Compile Include="Phone\PhoneCodeHelper.cs" />

     <Compile Include="Phone\PhoneControlFeedbackTraverser.cs" />

     <Compile Include="Phone\PhoneInitializationTraverser.cs" />

+    <Compile Include="Phone\PhoneMethodInliningTraverser.cs" />

     <Compile Include="Phone\PhoneNavigationTraverser.cs" />

     <Compile Include="Phone\PhoneCodeWrapperWriter.cs" />

     <Compile Include="Prelude.cs" />

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index 34eccf51..0e631c11 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -538,5 +538,24 @@ namespace BytecodeTranslator.Phone {
       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;

+    }

   }

 }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
new file mode 100644
index 00000000..86d696ec
--- /dev/null
+++ b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
@@ -0,0 +1,58 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Cci;

+

+namespace BytecodeTranslator.Phone {

+  public class PhoneMethodInliningMetadataTraverser : BaseMetadataTraverser {

+    private HashSet<IMethodDefinition> methodsToInline;

+    private HashSet<IMethodDefinition> iterMethodsToInline;

+    private PhoneCodeHelper phoneHelper;

+    private bool firstPassDone = false;

+

+    public PhoneMethodInliningMetadataTraverser(PhoneCodeHelper phoneHelper) {

+      methodsToInline = new HashSet<IMethodDefinition>();

+      iterMethodsToInline = new HashSet<IMethodDefinition>();

+      this.phoneHelper = phoneHelper;

+    }

+

+    public override void Visit(IEnumerable<IModule> modules) {

+      base.Visit(modules);

+      firstPassDone = true;

+    }

+

+    public override void Visit(IMethodDefinition method) {

+      if (iterMethodsToInline.Contains(method) || (!firstPassDone && phoneHelper.mustInlineMethod(method))) {

+        PhoneMethodInliningCodeTraverser codeTraverser= new PhoneMethodInliningCodeTraverser();

+        codeTraverser.Visit(method);

+        foreach (IMethodDefinition newMethodDef in codeTraverser.getMethodsFound()) {

+          if (!methodsToInline.Contains(newMethodDef))

+            iterMethodsToInline.Add(newMethodDef);

+        }

+        methodsToInline.Add(method);

+        iterMethodsToInline.Remove(method);

+      }

+    }

+

+    public IEnumerable<IMethodDefinition> getMethodsToInline() {

+      return methodsToInline;

+    }

+

+    public bool isFinished() {

+      return !iterMethodsToInline.Any();

+    }

+  }

+

+  class PhoneMethodInliningCodeTraverser : BaseCodeTraverser {

+    private HashSet<IMethodDefinition> foundMethods = new HashSet<IMethodDefinition>();

+

+    public override void Visit(IMethodCall methodCall) {

+      foundMethods.Add(methodCall.MethodToCall.ResolvedMethod);

+    }

+

+    public IEnumerable<IMethodDefinition> getMethodsFound() {

+      return foundMethods;

+    }

+  }

+}

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index d4eeeecf..3e6db57f 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -232,7 +232,6 @@ namespace BytecodeTranslator {
           modules.Add((IModule)mutableModule);

           contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));

           pdbReaders.Add(module, pdbReader);

-

         }

       }

       if (modules.Count == 0) {

@@ -258,6 +257,7 @@ namespace BytecodeTranslator {
         PhoneCodeHelper.initialize(host);

         phonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);

         PhoneCodeHelper.instance().PhonePlugin = phonePlugin;

+        

         if (doPhoneNav) {

           PhoneCodeHelper.instance().PhoneNavigationToggled = true;

           PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host);

@@ -279,42 +279,45 @@ namespace BytecodeTranslator {
         CreateDispatchMethod(sink, pair.Item1, pair.Item2);

       }

 

-      if (PhoneCodeHelper.instance().PhonePlugin != null) {

-        if (PhoneCodeHelper.instance().PhoneFeedbackToggled) {

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

-          PhoneCodeHelper.instance().CreateFeedbackCallingMethods(sink);

-        }

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

+        PhoneCodeHelper.instance().CreateFeedbackCallingMethods(sink);

+      }

 

-        if (PhoneCodeHelper.instance().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.instance().OnBackKeyPressOverriden) {

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

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

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

-          } else {

-            if (PhoneCodeHelper.instance().BackKeyPressNavigates) {

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

-              foreach (ITypeReference type in PhoneCodeHelper.instance().BackKeyNavigatingOffenders) {

-                Console.WriteLine("\t" + type.ToString());

-              }

+      if (PhoneCodeHelper.instance().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.instance().OnBackKeyPressOverriden) {

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

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

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

+        } else {

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

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

+            foreach (ITypeReference type in PhoneCodeHelper.instance().BackKeyNavigatingOffenders) {

+              Console.WriteLine("\t" + type.ToString());

             }

+          }

 

-            if (PhoneCodeHelper.instance().BackKeyPressHandlerCancels) {

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

-              foreach (ITypeReference type in PhoneCodeHelper.instance().BackKeyCancellingOffenders) {

-                Console.WriteLine("\t" + type.ToString());

-              }

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

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

+            foreach (ITypeReference type in PhoneCodeHelper.instance().BackKeyCancellingOffenders) {

+              Console.WriteLine("\t" + type.ToString());

             }

           }

         }

       }

 

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

+        PhoneMethodInliningMetadataTraverser inlineTraverser = new PhoneMethodInliningMetadataTraverser(PhoneCodeHelper.instance());

+        inlineTraverser.Visit(modules);

+        updateInlinedMethods(sink, inlineTraverser.getMethodsToInline());

+      }

+

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

       Prelude.Emit(writer);

       sink.TranslatedProgram.Emit(writer);

@@ -322,6 +325,13 @@ namespace BytecodeTranslator {
       return 0; // success

     }

 

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

+      }

+    }

+

     private static string NameUpToFirstPeriod(string name) {

       var i = name.IndexOf('.');

       if (i == -1)