(phone) slicing to avoid self loops

5 files changed, 53 insertions, 12 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index fdf5f4a3..6a054c9c 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -727,15 +727,24 @@ namespace BytecodeTranslator
       Contract.Assert(TranslatedExpressions.Count == 0);

       var tok = assignment.Token();

 

+      bool translationIntercepted= false;

       ICompileTimeConstant constant= assignment.Source as ICompileTimeConstant;

       // TODO move away phone related code from the translation, it would be better to have 2 or more translation phases

-      if (PhoneCodeHelper.instance().PhonePlugin != null && PhoneCodeHelper.instance().PhoneNavigationToggled &&

-          constant != null && constant.Type == sink.host.PlatformType.SystemString &&

-          constant.Value != null && constant.Value.Equals(PhoneCodeHelper.BOOGIE_DO_HAVOC_CURRENTURI)) {

-        TranslateHavocCurrentURI();

-      } else {

-        TranslateAssignment(tok, assignment.Target.Definition, assignment.Target.Instance, assignment.Source);

+      if (PhoneCodeHelper.instance().PhonePlugin != null && PhoneCodeHelper.instance().PhoneNavigationToggled) {

+        IFieldReference target = assignment.Target.Definition as IFieldReference;

+        if (target != null && target.Name.Value == PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE) {

+          if (constant != null && constant.Type == sink.host.PlatformType.SystemString && constant.Value != null &&

+              constant.Value.Equals(PhoneCodeHelper.BOOGIE_DO_HAVOC_CURRENTURI)) {

+            TranslateHavocCurrentURI();

+            translationIntercepted = true;

+          }

+          

+          StmtTraverser.StmtBuilder.Add(PhoneCodeHelper.instance().getAddNavigationCheck(sink));

+        }

       }

+

+      if (!translationIntercepted)

+        TranslateAssignment(tok, assignment.Target.Definition, assignment.Target.Instance, assignment.Source);

     }

 

     /// <summary>

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 73f76d52..d5e19fb0 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -564,6 +564,8 @@ namespace BytecodeTranslator {
       if (PhoneCodeHelper.instance().PhoneNavigationToggled) {

         Bpl.Variable continueOnPageVar = sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_CONTINUE_ON_PAGE_VARIABLE, Bpl.Type.Bool);

         sink.TranslatedProgram.TopLevelDeclarations.Add(continueOnPageVar);

+        Bpl.Variable navigationCheckVar = sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_NAVIGATION_CHECK_VARIABLE, Bpl.Type.Bool);

+        sink.TranslatedProgram.TopLevelDeclarations.Add(navigationCheckVar);

       }

     }

 

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index 2f818606..197e296f 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -245,6 +245,7 @@ namespace BytecodeTranslator.Phone {
     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";

 

@@ -657,7 +658,7 @@ namespace BytecodeTranslator.Phone {
     }

 

 

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

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

       MethodBody callerBody = new MethodBody();

       MethodDefinition callerDef = new MethodDefinition() {

         InternFactory = (def as MethodDefinition).InternFactory,

@@ -682,6 +683,8 @@ namespace BytecodeTranslator.Phone {
       }

 

       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;

@@ -710,7 +713,13 @@ namespace BytecodeTranslator.Phone {
       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)));

-      builder.Add(assertEndPage);

+

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

@@ -730,6 +739,7 @@ namespace BytecodeTranslator.Phone {
 

     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,

@@ -740,6 +750,7 @@ namespace BytecodeTranslator.Phone {
                                                        new Bpl.VariableSeq(), new Bpl.VariableSeq(), new Bpl.VariableSeq(),

                                                        builder.Collect(Bpl.Token.NoToken));

       sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

+

     }

 

     private IMethodReference uriHavocMethod=null;

@@ -760,5 +771,24 @@ namespace BytecodeTranslator.Phone {
 

       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;

+    }

   }

 }

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 382ad2ad..0862989e 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -333,7 +333,7 @@ namespace BytecodeTranslator {
       string outputFileName = primaryModule.Name + ".bpl";

       if (PhoneCodeHelper.instance().PhoneNavigationToggled) {

         foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {

-          PhoneCodeHelper.addHandlerStubCaller(sink, def);

+          PhoneCodeHelper.instance().addHandlerStubCaller(sink, def);

         }

         PhoneCodeHelper.instance().addNavigationUriHavocer(sink);

         PhoneCodeHelper.instance().createQueriesBatchFile(sink, outputFileName);

diff --git a/BCT/PhoneControlsExtractor/navGraphBuilder.py b/BCT/PhoneControlsExtractor/navGraphBuilder.py
index 42b3d299..ab1fbd60 100644
--- a/BCT/PhoneControlsExtractor/navGraphBuilder.py
+++ b/BCT/PhoneControlsExtractor/navGraphBuilder.py
@@ -151,7 +151,9 @@ def runBoogieQueries(appFile, outputFile, format):
   return True

 

 def buildNavigationGraph(appFile, outputFile, format):

+  global GRAPH_CREATION_TIME

   global navigation_graph

+  GRAPH_CREATION_TIME= time.clock()

   nameToNode= {}

   dotFile= open(os.path.splitext(appFile)[0] + ".dot","w")

   graphName= os.path.basename(os.path.splitext(appFile)[0])

@@ -178,7 +180,7 @@ def buildNavigationGraph(appFile, outputFile, format):
     dotFile.write("\tn0 -> n" + str(globalStart) + ";\n")

   except KeyError:

     pass

-

+  GRAPH_CREATION_TIME= time.clock() - GRAPH_CREATION_TIME

   statsNode= createStatsNode(appFile)

   dotFile.write("\t" + statsNode + "\n")

   dotFile.write("}")

@@ -285,12 +287,10 @@ def main():
     QUERY_RUN_TIME= time.clock() - QUERY_RUN_TIME

 

   if build=="" or build.find("g") != -1:

-    GRAPH_CREATION_TIME= time.clock()

     print "Building graph..."

     if (not buildNavigationGraph(appFile, outputFile, format)):

       print "Error creating navigation graph"

       sys.exit(1)

-    GRAPH_CREATION_TIME= time.clock() - GRAPH_CREATION_TIME

 

   print "Success!"

   sys.exit(0)