(phone bct) default URI checks inlined

inlining statistics

6 files changed, 31 insertions, 23 deletions

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 8c85d5df..1f9518b5 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -485,8 +485,8 @@ procedure DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref)
   }

 }

 

-procedure System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

-procedure System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

+procedure {:inline 1} System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

+procedure {:inline 1} System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

 

 implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) {

   $result := (a$in == b$in);

@@ -500,19 +500,19 @@ implementation System.String.op_Inequality$System.String$System.String(a$in: Ref
 var isControlEnabled: [Ref]bool;

 var isControlChecked: [Ref]bool;

 

-procedure System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);

+procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);

 implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool) {

   isControlEnabled[$this] := value$in;

 }

 

-procedure System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);

+procedure {:inline 1} System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);

 implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref) {

   var enabledness: bool;

   enabledness := isControlEnabled[$this];

   $result := Box2Ref(Bool2Box(enabledness));

 }

 

-procedure System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);

+procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);

 implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref) {

   var check: bool;

 

@@ -520,7 +520,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$Sys
   isControlChecked[$this] := check;

 }

 

-procedure System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);

+procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);

 implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref) {

   var isChecked: bool;

   isChecked := isControlChecked[$this];

diff --git a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
index 5bc32f57..97935721 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs
@@ -13,10 +13,14 @@ namespace BytecodeTranslator.Phone {
     private bool changedOnLastPass = false;

     private IAssemblyReference assemblyBeingTranslated;

 

+    public int TotalMethodsCount { get; private set; }

+    public int InlinedMethodsCount { get { return methodsToInline.Count(); } }

+

     public PhoneMethodInliningMetadataTraverser(PhoneCodeHelper phoneHelper) {

       methodsToInline = new HashSet<IMethodDefinition>();

       iterMethodsToInline = new HashSet<IMethodDefinition>();

       this.phoneHelper = phoneHelper;

+      TotalMethodsCount = 0;

     }

 

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

@@ -28,6 +32,9 @@ namespace BytecodeTranslator.Phone {
     }

 

     public override void Visit(IMethodDefinition method) {

+      if (!firstPassDone)

+        TotalMethodsCount++;

+

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

         PhoneMethodInliningCodeTraverser codeTraverser= new PhoneMethodInliningCodeTraverser();

         codeTraverser.Visit(method);

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 4c046b24..d921c481 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -317,6 +317,7 @@ namespace BytecodeTranslator {
           new PhoneMethodInliningMetadataTraverser(PhoneCodeHelper.instance());

         inlineTraverser.findAllMethodsToInline(modules);

         updateInlinedMethods(sink, inlineTraverser.getMethodsToInline());

+        System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);

       }

 

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

diff --git a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
index 886eaa91..37b35746 100644
--- a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
+++ b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
@@ -66,7 +66,7 @@ def outputMainProcedures(file, batFile):
     if (boogiePageVars[j]["boogieStringName"] == dummyPageVar):

       continue

 

-    file.write("procedure __BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) + "();\n")

+    file.write("procedure {:inline 1} __BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) + "();\n")

     file.write("implementation __BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) + "() {\n")

     file.write("\tvar $doWork: bool;\n")

     file.write("\tvar $activeControl: int;\n")

@@ -99,7 +99,7 @@ def outputMainProcedures(file, batFile):
     batFile.write("if exist corral_out_trace.txt move corral_out_trace.txt corral_out_trace_" + str(i) + "_" + str(j) + ".txt\n")

 

 def outputPageControlDriver(file, originalPageName, boogiePageName):

-  file.write("procedure drive" + boogiePageName + "Controls();\n")

+  file.write("procedure {:inline 1} drive" + boogiePageName + "Controls();\n")

   file.write("implementation drive" + boogiePageName + "Controls() {\n")

   file.write("\tvar $activeControl: int;\n")

   file.write("\tvar $control: Ref;\n")

@@ -117,7 +117,7 @@ def outputPageControlDriver(file, originalPageName, boogiePageName):
     if controlInfo["bplName"] == "":

       continue

     if not ifInitialized:

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

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

       ifInitialized= True

     else:

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

@@ -151,7 +151,7 @@ def outputControlDrivers(file, batFile):
   for i in range(0,len(boogiePageVars)):

     outputPageControlDriver(file, originalPageVars[i],boogiePageVars[i]["name"])

 

-  file.write("procedure DriveControls();\n")

+  file.write("procedure {:inline 1} DriveControls();\n")

   file.write("implementation DriveControls() {\n")

   for i in range(0,len(boogiePageVars)):

     file.write("\tvar isCurrent" + boogiePageVars[i]["name"] + ": bool;\n")

@@ -176,7 +176,7 @@ def outputControlDrivers(file, batFile):
   file.write("}\n")

 

 def outputURIHavocProcedure(file):

-  file.write("procedure __BOOGIE_Havoc_CurrentURI__();\n")

+  file.write("procedure {:inline 1} __BOOGIE_Havoc_CurrentURI__();\n")

   file.write("implementation __BOOGIE_Havoc_CurrentURI__() {\n")

   file.write("\thavoc " + currentNavigationVariable + ";\n")

   file.write("// TODO write assume statements to filter havoc'd variable to either of all pages\n")

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 50eb18a7..d33b6a17 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -292,11 +292,11 @@ implementation DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref)
 

 

 

-procedure System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

+procedure {:inline 1} System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

 

 

 

-procedure System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

+procedure {:inline 1} System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

 

 

 

@@ -318,7 +318,7 @@ var isControlEnabled: [Ref]bool;
 

 var isControlChecked: [Ref]bool;

 

-procedure System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);

+procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);

 

 

 

@@ -329,7 +329,7 @@ implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($thi
 

 

 

-procedure System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);

+procedure {:inline 1} System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);

 

 

 

@@ -343,7 +343,7 @@ implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns
 

 

 

-procedure System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);

+procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);

 

 

 

@@ -357,7 +357,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$Sys
 

 

 

-procedure System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);

+procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);

 

 

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index cf34d250..2f6b0041 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -290,11 +290,11 @@ implementation DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref)
 

 

 

-procedure System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

+procedure {:inline 1} System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

 

 

 

-procedure System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

+procedure {:inline 1} System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);

 

 

 

@@ -316,7 +316,7 @@ var isControlEnabled: [Ref]bool;
 

 var isControlChecked: [Ref]bool;

 

-procedure System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);

+procedure {:inline 1} System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool);

 

 

 

@@ -327,7 +327,7 @@ implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($thi
 

 

 

-procedure System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);

+procedure {:inline 1} System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref);

 

 

 

@@ -341,7 +341,7 @@ implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns
 

 

 

-procedure System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);

+procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);

 

 

 

@@ -355,7 +355,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$Sys
 

 

 

-procedure System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);

+procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref);