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

preparing boogie code for static unrolls
filtering out some navigations

2 files changed, 9 insertions, 7 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)) {