cleaning up & refactor

6 files changed, 132 insertions, 143 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 01f64519..9e5babc1 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -131,7 +131,6 @@
     <Compile Include="Phone\PhoneInitializationTraverser.cs" />

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

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

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

     <Compile Include="Prelude.cs" />

     <Compile Include="ExpressionTraverser.cs" />

     <Compile Include="Sink.cs" />

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 6498edb9..a3b7eb99 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -407,44 +407,12 @@ namespace BytecodeTranslator
     }

 

     public override void Visit(IDefaultValue defaultValue) {

-

       var typ = defaultValue.Type;

 

-      #region Struct

       if (TranslationHelper.IsStruct(typ)) {

-        // then it is a struct and gets special treatment

-        // translate it as if it were a call to the nullary ctor for the struct type

-        // (which doesn't actually exist, but gets generated for each struct type

-        // encountered during translation)

-

-        var tok = defaultValue.Token();

-

-        var loc = this.sink.CreateFreshLocal(typ);

-        var locExpr = Bpl.Expr.Ident(loc);

-

-        // First generate an Alloc() call

-        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(tok, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(locExpr)));

-

-        // Second, generate the call to the appropriate ctor

-        var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typ);

-        var invars = new List<Bpl.Expr>();

-        invars.Add(locExpr);

-        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, invars, new List<Bpl.IdentifierExpr>()));

-

-        // Generate an assumption about the dynamic type of the just allocated object

-        this.StmtTraverser.StmtBuilder.Add(

-            new Bpl.AssumeCmd(tok,

-              Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

-              this.sink.Heap.DynamicType(locExpr),

-              this.sink.FindOrCreateType(typ)

-              )

-              )

-            );

-

-        this.TranslatedExpressions.Push(locExpr);

+        translateStructDefaultValue(defaultValue, typ);

         return;

       }

-      #endregion

 

       Bpl.Expr e;

       var bplType = this.sink.CciTypeToBoogie(typ);

@@ -470,6 +438,39 @@ namespace BytecodeTranslator
       return;

     }

 

+    private void translateStructDefaultValue(IDefaultValue defaultValue, ITypeReference typ) {

+      // then it is a struct and gets special treatment

+      // translate it as if it were a call to the nullary ctor for the struct type

+      // (which doesn't actually exist, but gets generated for each struct type

+      // encountered during translation)

+

+      var tok = defaultValue.Token();

+

+      var loc = this.sink.CreateFreshLocal(typ);

+      var locExpr = Bpl.Expr.Ident(loc);

+

+      // First generate an Alloc() call

+      this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(tok, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(locExpr)));

+

+      // Second, generate the call to the appropriate ctor

+      var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typ);

+      var invars = new List<Bpl.Expr>();

+      invars.Add(locExpr);

+      this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, invars, new List<Bpl.IdentifierExpr>()));

+

+      // Generate an assumption about the dynamic type of the just allocated object

+      this.StmtTraverser.StmtBuilder.Add(

+          new Bpl.AssumeCmd(tok,

+            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+            this.sink.Heap.DynamicType(locExpr),

+            this.sink.FindOrCreateType(typ)

+            )

+            )

+          );

+

+      this.TranslatedExpressions.Push(locExpr);

+    }

+

     #endregion

 

     #region Translate Method Calls

@@ -729,6 +730,7 @@ namespace BytecodeTranslator
       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

+      // NAVIGATION TODO maybe this will go away if I can handle it with stubs

       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) {

@@ -737,7 +739,6 @@ namespace BytecodeTranslator
             TranslateHavocCurrentURI();

             translationIntercepted = true;

           }

-          

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

         }

       }

@@ -1363,6 +1364,8 @@ namespace BytecodeTranslator
       #endregion

       */

 

+

+      // TODO is this code actually needed at all? It seems that all this is already being done in the Statement traverser for the conditional

       StatementTraverser thenStmtTraverser = this.StmtTraverser.factory.MakeStatementTraverser(this.sink, this.StmtTraverser.PdbReader, this.contractContext);

       StatementTraverser elseStmtTraverser = this.StmtTraverser.factory.MakeStatementTraverser(this.sink, this.StmtTraverser.PdbReader, this.contractContext);

       ExpressionTraverser thenExprTraverser = this.StmtTraverser.factory.MakeExpressionTraverser(this.sink, thenStmtTraverser, this.contractContext);

diff --git a/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
index 026cf301..066d4cdf 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs
@@ -49,8 +49,6 @@ namespace BytecodeTranslator.Phone {
             delegateBody = anonDelegate.Body;

           }

 

-          // NAVIGATION TODO look for reachable method calls

-

           // NAVIGATION TODO what if it has no body?

           if (delegateBody != null) {

             bool navigates= false, cancelsNav= false;

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs
deleted file mode 100644
index 8bec1605..00000000
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs
+++ /dev/null
@@ -1,33 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-

-using TranslationPlugins;

-

-namespace BytecodeTranslator.Phone {

-  class PhoneCodeWrapperWriter {

-    private static Sink sink;

-    public static void createCodeWrapper(Sink sink) {

-      PhoneCodeWrapperWriter.sink = sink;

-      /*

-       * create Main procedure

-       *  - creates page instances, one per page -- this overapproximates as there may be more instances

-       *  - havoc'd loop drives controls via calls to driver

-       *  

-       * create Driver procedure

-       *  - determine current page; for each page check if it is current or not

-       *  - call page driver accordingly

-       *  

-       * create Page drivers

-       *  - one for each page

-       *  - havoc-ly determine control to stimulate

-       *  - check enabledness of control, stimulate by calling handler of chosen event if yes, nothing ig not

-       *  - possibly many events to handle

-       *  - might be slightly more efficient to nto return control until we know page navigation may have changed,

-       *    but this requires a lot of knowledge (ie, will the called method call NavigationService or not)

-       */

-      //createMainProcedure();

-    }

-  }

-}

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 4b5e205c..da0f401e 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -143,7 +143,6 @@ namespace BytecodeTranslator {
       #endregion

 

       try {

-

         HeapFactory heap;

         switch (options.heapRepresentation) {

           case Options.HeapRepresentation.splitFields:

@@ -187,6 +186,7 @@ namespace BytecodeTranslator {
       var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);

       Host = host;

 

+      #region Assemlies to translate (via cmd line)

       modules = new List<IModule>();

       var contractExtractors = new Dictionary<IUnit, IContractProvider>();

       var pdbReaders = new Dictionary<IUnit, PdbReader>();

@@ -208,6 +208,9 @@ namespace BytecodeTranslator {
         contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));

         pdbReaders.Add(module, pdbReader);

       }

+      #endregion

+

+      #region Assemblies to translate (stubs)

       if (stubAssemblies != null) {

         foreach (var s in stubAssemblies) {

           var module = host.LoadUnitFrom(s) as IModule;

@@ -242,23 +245,25 @@ namespace BytecodeTranslator {
           pdbReaders.Add(module, pdbReader);

         }

       }

+      #endregion

+

       if (modules.Count == 0) {

         Console.WriteLine("No input assemblies to translate.");

         return -1;

       }

 

       var primaryModule = modules[0];

+      TraverserFactory bctTraverserFactory;

+      if (wholeProgram) {

+        bctTraverserFactory = new WholeProgram();

+      } else {

+        bctTraverserFactory = new CLRSemantics();

+      }

 

-      TraverserFactory traverserFactory;

-      if (wholeProgram)

-        traverserFactory = new WholeProgram();

-      else

-        traverserFactory = new CLRSemantics();

-

-      Sink sink= new Sink(host, traverserFactory, heapFactory, options, exemptionList, whiteList);

+      Sink sink= new Sink(host, bctTraverserFactory, heapFactory, options, exemptionList, whiteList);

       TranslationHelper.tmpVarCounter = 0;

       MetadataTraverser translator;

-      translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

+      translator= bctTraverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

 

       if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {

         PhoneCodeHelper.initialize(host);

@@ -287,6 +292,10 @@ namespace BytecodeTranslator {
 

       string outputFileName = primaryModule.Name + ".bpl";

       callPostTranslationTraversers(modules, sink, phoneControlsConfigFile, outputFileName);

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

+        finalizeNavigationAnalysisAndBoogieCode(phoneControlsConfigFile, sink, outputFileName);

+      }

+

       Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);

       Prelude.Emit(writer);

       sink.TranslatedProgram.Emit(writer);

@@ -294,6 +303,14 @@ namespace BytecodeTranslator {
       return 0; // success

     }

 

+    private static void finalizeNavigationAnalysisAndBoogieCode(string phoneControlsConfigFile, Sink sink, string outputFileName) {

+      outputBoogieTrackedControlConfiguration(phoneControlsConfigFile);

+      checkTransitivelyCalledBackKeyNavigations(modules);

+      createPhoneBoogieCallStubs(sink);

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

+      outputBackKeyWarnings();

+    }

+

     private static void callPostTranslationTraversers(List<IModule> modules, Sink sink, string phoneControlsConfigFile, string outputFileName) {

       if (PhoneCodeHelper.instance().PhoneFeedbackToggled) {

         PhoneCodeHelper.instance().CreateFeedbackCallingMethods(sink);

@@ -310,81 +327,84 @@ namespace BytecodeTranslator {
         traverser.Visit(modules);

 

       }

+    }

 

-      // NAVIGATION TODO: refactor warnings out of here

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

-        string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout");

-        StreamWriter outputStream = new StreamWriter(outputConfigFile);

-        PhoneCodeHelper.instance().PhonePlugin.DumpControlStructure(outputStream);

-        outputStream.Close();

-        PhoneCodeWrapperWriter.createCodeWrapper(sink);

-

-        foreach (IMethodReference navMethod in PhoneCodeHelper.instance().KnownBackKeyHandlers) {

-          // right now we traversed everything so we can see reachability

-          IEnumerable<IMethodDefinition> indirects= PhoneCodeHelper.instance().getIndirectNavigators(modules, navMethod);

-          if (indirects.Count() > 0) {

-            ICollection<Tuple<IMethodReference, string>> targets = null;

-            PhoneCodeHelper.instance().BackKeyNavigatingOffenders.TryGetValue(navMethod.ContainingType, out targets);

-            if (targets == null) {

-              targets = new HashSet<Tuple<IMethodReference, string>>();

-            }

-            string indirectTargeting = "<unknown indirect navigation> via (";

-            foreach (IMethodDefinition methDef in indirects) {

-              indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", ";

-            }

-            indirectTargeting += ")";

-            targets.Add(Tuple.Create<IMethodReference, string>(navMethod, indirectTargeting));

-            PhoneCodeHelper.instance().BackKeyNavigatingOffenders[navMethod.ContainingType] = targets;

-          }

+    private static void outputBoogieTrackedControlConfiguration(string phoneControlsConfigFile) {

+      string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout");

+      StreamWriter outputStream = new StreamWriter(outputConfigFile);

+      PhoneCodeHelper.instance().PhonePlugin.DumpControlStructure(outputStream);

+      outputStream.Close();

+    }

 

-          indirects = PhoneCodeHelper.instance().getIndirectCancellations(modules, navMethod);

-          if (indirects.Count() > 0) {

-            string indirectTargeting = "(";

-            foreach (IMethodDefinition methDef in indirects) {

-              indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", ";

+    private static void outputBackKeyWarnings() {

+      // 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().BackKeyHandlerOverridenByUnknownDelegate) {

+        Console.Out.WriteLine("Back navigation ISSUE: BackKeyPress is overriden by unidentified delegate and may perform illegal navigation");

+        Console.Out.WriteLine("Offending pages:");

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

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

+        }

+      } 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.Keys) {

+            ICollection<Tuple<IMethodReference, string>> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[type];

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

+            foreach (Tuple<IMethodReference, string> target in targets) {

+              Console.WriteLine("\t\t" + target.Item2 + " via " +

+                                (target.Item1.Name == Dummy.Name ? "anonymous delegate" : target.Item1.ContainingType.ToString() + "." + target.Item1.Name.Value));

             }

-            indirectTargeting += ")";

-            PhoneCodeHelper.instance().BackKeyCancellingOffenders.Add(Tuple.Create<ITypeReference,string>(navMethod.ContainingType, indirectTargeting));

           }

         }

 

-        foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {

-          if (!PhoneCodeHelper.instance().isKnownBackKeyOverride(def))

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

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

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

+          foreach (Tuple<ITypeReference, string> cancellation in PhoneCodeHelper.instance().BackKeyCancellingOffenders) {

+            Console.WriteLine("\t" + cancellation.Item1.ToString() + " via " + cancellation.Item2);

+          }

         }

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

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

-

-        // 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().BackKeyHandlerOverridenByUnknownDelegate) {

-          Console.Out.WriteLine("Back navigation ISSUE: BackKeyPress is overriden by unidentified delegate and may perform illegal navigation");

-          Console.Out.WriteLine("Offending pages:");

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

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

+      }

+    }

+

+    private static void createPhoneBoogieCallStubs(Sink sink) {

+      foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {

+        if (!PhoneCodeHelper.instance().isKnownBackKeyOverride(def))

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

+      }

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

+    }

+

+    private static void checkTransitivelyCalledBackKeyNavigations(List<IModule> modules) {

+      foreach (IMethodReference navMethod in PhoneCodeHelper.instance().KnownBackKeyHandlers) {

+        // right now we traversed everything so we can see reachability

+        IEnumerable<IMethodDefinition> indirects = PhoneCodeHelper.instance().getIndirectNavigators(modules, navMethod);

+        if (indirects.Count() > 0) {

+          ICollection<Tuple<IMethodReference, string>> targets = null;

+          PhoneCodeHelper.instance().BackKeyNavigatingOffenders.TryGetValue(navMethod.ContainingType, out targets);

+          if (targets == null) {

+            targets = new HashSet<Tuple<IMethodReference, string>>();

           }

-        } 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.Keys) {

-              ICollection<Tuple<IMethodReference,string>> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[type];

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

-              foreach (Tuple<IMethodReference,string> target in targets) {

-                Console.WriteLine("\t\t" + target.Item2 + " via " +

-                                  (target.Item1.Name == Dummy.Name ? "anonymous delegate" : target.Item1.ContainingType.ToString() + "." + target.Item1.Name.Value));

-              }

-            }

+          string indirectTargeting = "<unknown indirect navigation> via (";

+          foreach (IMethodDefinition methDef in indirects) {

+            indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", ";

           }

+          indirectTargeting += ")";

+          targets.Add(Tuple.Create<IMethodReference, string>(navMethod, indirectTargeting));

+          PhoneCodeHelper.instance().BackKeyNavigatingOffenders[navMethod.ContainingType] = targets;

+        }

 

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

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

-            foreach (Tuple<ITypeReference,string> cancellation in PhoneCodeHelper.instance().BackKeyCancellingOffenders) {

-              Console.WriteLine("\t" + cancellation.Item1.ToString() + " via " + cancellation.Item2);

-            }

+        indirects = PhoneCodeHelper.instance().getIndirectCancellations(modules, navMethod);

+        if (indirects.Count() > 0) {

+          string indirectTargeting = "(";

+          foreach (IMethodDefinition methDef in indirects) {

+            indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", ";

           }

+          indirectTargeting += ")";

+          PhoneCodeHelper.instance().BackKeyCancellingOffenders.Add(Tuple.Create<ITypeReference, string>(navMethod.ContainingType, indirectTargeting));

         }

       }

     }

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index f3481f43..fac00e42 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -20,6 +20,8 @@ using Bpl = Microsoft.Boogie;
 

 namespace BytecodeTranslator {

   public abstract class TraverserFactory {

+    public int Priority { get; set; }

+

     public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,

       IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?

       IDictionary<IUnit, PdbReader> sourceLocationProviders)