(phone bct) filtering out nonpages for boogie queries, faster but maybe a less precise

preparing boogie code for static unrolls
filtering out some navigations

5 files changed, 43 insertions, 18 deletions

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index 74c17f54..704d5669 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -643,25 +643,21 @@ namespace BytecodeTranslator.Phone {
       IEnumerable<string> xamls= PhonePlugin.getPageXAMLFilenames();

       string startURI= sink.FindOrCreateConstant(BOOGIE_STARTING_URI_PLACEHOLDER).Name;

       string endURI = sink.FindOrCreateConstant(BOOGIE_ENDING_URI_PLACEHOLDER).Name;

-      int i=1, j=1;

       foreach (string x1 in xamls) {

         string startURIVar= sink.FindOrCreateConstant(x1).Name.ToLower();

-        j = 1;

         foreach (string x2 in xamls) {

-          string resultFile = sourceBPLFile + "_" + i + "_" + j + ".bpl";

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

-          j++;

         }

-        i++;

       }

 

       outputStream.Close();

     }

 

 

-    public static void addHandlerStubCaller(Sink sink, IMethodDefinition def) {

+    public static Bpl.Procedure addHandlerStubCaller(Sink sink, IMethodDefinition def) {

       MethodBody callerBody = new MethodBody();

       MethodDefinition callerDef = new MethodDefinition() {

         InternFactory = (def as MethodDefinition).InternFactory,

@@ -720,6 +716,7 @@ namespace BytecodeTranslator.Phone {
                                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) {

diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
index 4dd1b9ac..c4599520 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -74,6 +74,7 @@ namespace BytecodeTranslator.Phone {
 

     private bool navCallFound=false;

     private bool navCallIsStatic = false;

+    private bool navCallIsBack = false;

     private StaticURIMode currentStaticMode= StaticURIMode.NOT_STATIC;

     private string unpurifiedFoundURI="";

 

@@ -83,12 +84,13 @@ namespace BytecodeTranslator.Phone {
       foreach (IStatement statement in block.Statements) {

         navCallFound = false;

         navCallIsStatic = false;

+        navCallIsBack = false;

         this.Visit(statement);

         if (navCallFound) {

           navCallers.Add(methodTraversed);

           if (navCallIsStatic) {

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

-          } else {

+          } else if (!navCallIsBack) {

             nonStaticNavStmts.Add(statement);

           }

         }

@@ -185,7 +187,10 @@ namespace BytecodeTranslator.Phone {
         currentStaticMode = StaticURIMode.NOT_STATIC;

         if (methodToCallName == "GoBack") {

           navCallIsStatic = false;

+          navCallIsBack = true;

         } else { // Navigate()

+          navCallIsBack = false;

+

           // check for different static patterns that we may be able to verify

           IExpression uriArg = methodCall.Arguments.First();

           if (UriHelper.isArgumentURILocallyCreatedStatic(uriArg, host, out unpurifiedFoundURI)) {

diff --git a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
index 2071ce21..06c55a0f 100644
--- a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
+++ b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py
@@ -22,12 +22,14 @@ boogiePageClasses= []
 dummyPageVar= "dummyBoogieStringPageName"

 anonymousControlCount= 0;

 ANONYMOUS_CONTROL_PREFIX= "__BOOGIE_ANONYMOUS_CONTROL_"

+unrolls= 0

 

 def showUsage():

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

   print "Usage:"

-  print "\tPhoneBoogieCodeGenerator --controls <app_control_info_file> --output <code_output_file>\n"

+  print "\tPhoneBoogieCodeGenerator --staticUnroll <n> --controls <app_control_info_file> --output <code_output_file>\n"

   print "Options:"

+  print "\t--staticUnroll <n>: Do not generate loops, unroll up to n times. If not set generates loops (default). Short form: -u"

   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"

 

@@ -93,11 +95,15 @@ def outputMainProcedures(file, batFile):
       file.write("\tcall " + boogiePageClasses[k] + ".#ctor(" + boogiePageVars[k]["name"] + ");\n")

 

     file.write("\t//TODO still need to call Loaded handler on main page.\n")

-    file.write("\thavoc $doWork;\n")

-    file.write("\twhile ($doWork) {\n")

-    file.write("\t\tcall DriveControls();\n")

-    file.write("\t\thavoc $doWork;\n")

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

+    if (unrolls == 0):

+      file.write("\thavoc $doWork;\n")

+      file.write("\twhile ($doWork) {\n")

+      file.write("\t\tcall DriveControls();\n")

+      file.write("\t\thavoc $doWork;\n")

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

+    else:

+      for unr in range(unrolls):

+        file.write("\t\tcall DriveControls();\n")

 

     file.write("\tassume " + currentNavigationVariable + " == " + boogiePageVars[i]["boogieStringName"] + ";\n")

     file.write("\tcall DriveControls();\n")

@@ -123,6 +129,7 @@ def outputPageControlDriver(file, originalPageName, boogiePageName):
 

   file.write("\t" + CONTINUEONPAGE_VAR +":=true;\n")

   file.write("\thavoc $activeControl;\n")

+

   file.write("\twhile (" + CONTINUEONPAGE_VAR + ") {\n")

   activeControl=0

   ifInitialized= False

@@ -196,7 +203,7 @@ def outputControlDrivers(file, batFile):
 def outputURIHavocProcedure(file):

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

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

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

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

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

   # file.write("\tassume )

   file.write("}\n")

@@ -250,16 +257,18 @@ def buildControlInfo(controlInfoFileName):
   file.close()

 

 def main():

+  global unrolls

   controlFile= ""

   outputFile= ""

+

   try:

-    opts, args= getopt.getopt(sys.argv[1:], "c:o:", ["controls=","output="])

+    opts, args= getopt.getopt(sys.argv[1:], "c:o:u:", ["controls=","output=","staticUnroll="])

   except geopt.error, msg:

     print msg

     showUsage()

     sys.exit(2)

 

-  if not len(opts) == 2:

+  if not len(opts) >= 2:

     print "Missing options"

     showUsage()

     sys.exit(2)

@@ -269,6 +278,8 @@ def main():
       controlFile= a

     if o in ["-o", "--output"]:

       outputFile= a

+    if o in ["-u", "--staticUnroll"]:

+      unrolls= int(a)

 

   buildControlInfo(controlFile)

   outputBoilerplate(outputFile, outputFile + ".bat")

diff --git a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
index bb9eb2e6..8a384e09 100644
--- a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
+++ b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py
@@ -104,6 +104,14 @@ def addControlToMap(pageXAML, parentPage, controlNode):
   pageControls.append(newControl)

   staticControlsMap[parentPage]= pageControls

 

+def isPageXAML(pageXAML):

+  pageFile= open(pageXAML, "r")

+  if not isPageFile(pageFile):

+    return False

+  pageFileXML= minidom.parse(pageFile)

+  pageFile.close()

+  return pageFileXML.childNodes[0].nodeName.find("Page") != -1

+

 def extractPhoneControlsFromPage(pageXAML):

   # maybe it is not a page file

   print "extracting from " + pageXAML

@@ -120,7 +128,10 @@ def extractPhoneControlsFromPage(pageXAML):
     if (len(controls) == 0):

       # it is either a page with no controls, or controls that are dynamically created, or controls we do not track yet

       # in any case, just add a dummy control so as not to lose the page

-      addDummyControlToMap(pageXAML, ownerPage)

+      if (not isPageXAML(pageXAML)):

+        addDummyControlToMap(pageXAML, ownerPage + "__dummy")

+      else:

+        addDummyControlToMap(pageXAML, ownerPage)

     else:

       for control in controls:

         parent= control

diff --git a/BCT/TranslationPlugins/PhoneControlsPlugin.cs b/BCT/TranslationPlugins/PhoneControlsPlugin.cs
index 01900007..f0c75a4c 100644
--- a/BCT/TranslationPlugins/PhoneControlsPlugin.cs
+++ b/BCT/TranslationPlugins/PhoneControlsPlugin.cs
@@ -392,7 +392,8 @@ namespace TranslationPlugins {
     public IEnumerable<string> getPageXAMLFilenames() {

       HashSet<string> pageXAMLs = new HashSet<string>();

       foreach (string name in this.pageStructureInfo.Keys) {

-        pageXAMLs.Add(pageStructureInfo[name].PageXAML);

+        if (!name.EndsWith("__dummy"))

+          pageXAMLs.Add(pageStructureInfo[name].PageXAML);

       }

 

       return pageXAMLs;