diff options
Diffstat (limited to 'BCT')
| -rw-r--r-- | BCT/BytecodeTranslator/BytecodeTranslator.csproj | 2 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 19 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs | 42 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs | 29 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs | 6 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs | 9 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 22 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TraverserFactory.cs | 14 | ||||
| -rw-r--r-- | BCT/PhoneControlsExtractor/PhoneControlsExtractor.py | 3 | ||||
| -rw-r--r-- | BCT/TranslationPlugins/PhoneControlsPlugin.cs | 97 |
10 files changed, 203 insertions, 40 deletions
diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj index e9b8be83..8f72e62f 100644 --- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj +++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj @@ -128,7 +128,7 @@ <Compile Include="Phone\PhoneCodeHelper.cs" />
<Compile Include="Phone\PhoneInitializationTraverser.cs" />
<Compile Include="Phone\PhoneNavigationTraverser.cs" />
- <Compile Include="Phone\PhoneURIDeclarationsTraverser.cs" />
+ <Compile Include="Phone\PhoneCodeWrapperWriter.cs" />
<Compile Include="Prelude.cs" />
<Compile Include="ExpressionTraverser.cs" />
<Compile Include="Sink.cs" />
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index d4a125e1..96e3f361 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -16,6 +16,7 @@ using Microsoft.Cci.ILToCodeModel; using Bpl = Microsoft.Boogie;
using System.Diagnostics.Contracts;
+using TranslationPlugins;
namespace BytecodeTranslator {
@@ -33,6 +34,8 @@ namespace BytecodeTranslator { public readonly IDictionary<IUnit, PdbReader> PdbReaders;
public PdbReader/*?*/ PdbReader;
+ public PhoneControlsPlugin PhonePlugin { get; set; }
+
public MetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)
: base() {
this.sink = sink;
@@ -476,7 +479,21 @@ namespace BytecodeTranslator { }
public override void Visit(IFieldDefinition fieldDefinition) {
- this.sink.FindOrCreateFieldVariable(fieldDefinition);
+ Bpl.Variable fieldVar= this.sink.FindOrCreateFieldVariable(fieldDefinition);
+
+ // if tracked by the phone plugin, we need to find out the bpl assigned name for future use
+ if (PhonePlugin != null) {
+ INamespaceTypeReference namedContainerRef= fieldDefinition.ContainingType as INamespaceTypeReference;
+ if (namedContainerRef != null) {
+ string containerName = namedContainerRef.ContainingUnitNamespace.Unit.Name.Value + "." + namedContainerRef.Name.Value;
+ IEnumerable<ControlInfoStructure> controls= PhonePlugin.getControlsForPage(containerName);
+ if (controls != null) {
+ ControlInfoStructure ctrlInfo = controls.FirstOrDefault(ctrl => ctrl.Name == fieldDefinition.Name.Value);
+ if (ctrlInfo != null)
+ ctrlInfo.BplName = fieldVar.Name;
+ }
+ }
+ }
}
#endregion
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs new file mode 100644 index 00000000..4a469ad1 --- /dev/null +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs @@ -0,0 +1,42 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using TranslationPlugins;
+
+namespace BytecodeTranslator.Phone {
+ class PhoneCodeWrapperWriter {
+ private static Sink sink;
+ private static PhoneControlsPlugin controlsPlugin;
+ private static readonly string BOOGIE_MAIN_PROCEDURE = "$__BOOGIE_MAIN_PROCEDURE__$";
+
+ public static void createCodeWrapper(Sink sink, PhoneControlsPlugin controlsPlugin) {
+ PhoneCodeWrapperWriter.sink = sink;
+ PhoneCodeWrapperWriter.controlsPlugin = controlsPlugin;
+ /*
+ * 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();
+ }
+
+ private static void createMainProcedure() {
+ // TODO
+ // for now I'm trying to create this code as an outside step of the flow
+ }
+ }
+}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs index fd24ff65..e4510a7d 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs @@ -148,9 +148,6 @@ namespace BytecodeTranslator.Phone { injectedStatements = injectedStatements.Concat(getCodeForSettingEnabledness(controlInfo));
injectedStatements = injectedStatements.Concat(getCodeForSettingCheckedState(controlInfo));
injectedStatements = injectedStatements.Concat(getCodeForSettingVisibility(controlInfo));
- injectedStatements = injectedStatements.Concat(getCodeForSettingEventHandlers(controlInfo, "Click"));
- injectedStatements = injectedStatements.Concat(getCodeForSettingEventHandlers(controlInfo, "Checked"));
- injectedStatements = injectedStatements.Concat(getCodeForSettingEventHandlers(controlInfo, "Unchecked"));
}
int stmtPos= block.Statements.IndexOf(statementAfter);
@@ -222,7 +219,7 @@ namespace BytecodeTranslator.Phone { MethodToCall = isEnabledSetter,
ThisArgument = boundControl,
};
-
+
setEnablednessCall.Arguments.Add(controlInfo.IsEnabled ? trueConstant : falseConstant);
ExpressionStatement callStmt = new ExpressionStatement() {
Expression = setEnablednessCall,
@@ -232,13 +229,23 @@ namespace BytecodeTranslator.Phone { }
private IEnumerable<IStatement> getCodeForSettingCheckedState(ControlInfoStructure controlInfo) {
- // TODO not implemented yet
- return new List<IStatement>();
- }
-
- // TODO should stop propagating the string event name
- private IEnumerable<IStatement> getCodeForSettingEventHandlers(ControlInfoStructure controlInfo, string eventName) {
- // TODO not implemented yet
+ // IList<IStatement> code = new List<IStatement>();
+ // BoundExpression boundControl = makeBoundControlFromControlInfo(controlInfo);
+ // MethodCall setCheckStateCall= new MethodCall() {
+ // IsStaticCall = false,
+ // IsVirtualCall = true,
+ // IsTailCall = false,
+ // Type = ((Microsoft.Cci.Immutable.PlatformType) host.PlatformType).SystemVoid,
+ // MethodToCall = isCheckedSetter,
+ // ThisArgument = boundControl,
+ // };
+
+ // setCheckStateCall.Arguments.Add(controlInfo.IsChecked ? trueConstant : falseConstant);
+ // ExpressionStatement callStmt = new ExpressionStatement() {
+ // Expression = setCheckStateCall,
+ // };
+ // code.Add(callStmt);
+ // return code;
return new List<IStatement>();
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs index b702e78b..249faf2b 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs @@ -196,8 +196,10 @@ namespace BytecodeTranslator.Phone { // TODO Here there is the STRONG assumption that a given method will only navigate at most once per method call
// TODO (or at most will re-navigate to the same page). Quick "page flipping" on the same method
// TODO would not be captured correctly
+ Microsoft.Cci.MutableCodeModel.BlockStatement mutableBlock = block as Microsoft.Cci.MutableCodeModel.BlockStatement;
+
foreach (Tuple<IStatement, StaticURIMode, string> entry in stmts) {
- int ndx= block.Statements.ToList().IndexOf(entry.Item1, 0);
+ int ndx= mutableBlock.Statements.ToList().IndexOf(entry.Item1, 0);
if (ndx == -1) {
// can't be
throw new IndexOutOfRangeException("Statement must exist in original block");
@@ -222,7 +224,7 @@ namespace BytecodeTranslator.Phone { Statement uriInitStmt = new ExpressionStatement() {
Expression = currentURIAssign,
};
- block.Statements.ToList().Insert(ndx+1, uriInitStmt);
+ mutableBlock.Statements.Insert(ndx+1, uriInitStmt);
}
}
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs deleted file mode 100644 index fa330439..00000000 --- a/BCT/BytecodeTranslator/Phone/PhoneURIDeclarationsTraverser.cs +++ /dev/null @@ -1,9 +0,0 @@ -using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-namespace BytecodeTranslator.Phone {
- class PhoneURIDeclarationsTraverser {
- }
-}
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 14d0a466..3f895bda 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -100,7 +100,7 @@ namespace BytecodeTranslator { } catch (Exception e) { // swallow everything and just return an error code
Console.WriteLine("The byte-code translator failed: {0}", e.Message);
- //Console.WriteLine("Stack trace: {0}", e.StackTrace);
+ // Console.WriteLine("Stack trace: {0}", e.StackTrace);
return -1;
}
return result;
@@ -176,8 +176,9 @@ namespace BytecodeTranslator { var primaryModule = modules[0];
+ PhoneControlsPlugin phonePlugin = null;
if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
- PhoneControlsPlugin phonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);
+ phonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);
PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(phonePlugin, host);
initTr.InjectPhoneCodeAssemblies(modules);
PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(phonePlugin, host);
@@ -192,13 +193,28 @@ namespace BytecodeTranslator { Sink sink= new Sink(host, traverserFactory, heapFactory);
TranslationHelper.tmpVarCounter = 0;
- MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
+ MetadataTraverser translator;
+ if (phonePlugin != null) {
+ translator = traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders, phonePlugin);
+ } else {
+ translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
+ }
translator.TranslateAssemblies(modules);
foreach (var pair in sink.delegateTypeToDelegates.Values) {
CreateDispatchMethod(sink, pair.Item1, pair.Item2);
}
+ // TODO based on phone plugin information, create the main Boogie program, control drivers and assume/assert scheme
+ if (phonePlugin != null) {
+ string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout");
+ StreamWriter outputStream = new StreamWriter(outputConfigFile);
+ phonePlugin.DumpControlStructure(outputStream);
+ outputStream.Close();
+
+ PhoneCodeWrapperWriter.createCodeWrapper(sink, phonePlugin);
+ }
+
Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");
Prelude.Emit(writer);
sink.TranslatedProgram.Emit(writer);
diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs index 78c818bd..e680d2e0 100644 --- a/BCT/BytecodeTranslator/TraverserFactory.cs +++ b/BCT/BytecodeTranslator/TraverserFactory.cs @@ -14,10 +14,24 @@ using Microsoft.Cci.MutableCodeModel; using Microsoft.Cci.Contracts;
using Microsoft.Cci.ILToCodeModel;
+using TranslationPlugins;
+
using Bpl = Microsoft.Boogie;
namespace BytecodeTranslator {
public abstract class TraverserFactory {
+ // TODO this one factory method will have to go away and find the way to get the phone info into the traverser
+ // TODO in some other (better) way
+ public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,
+ IDictionary<IUnit, IContractProvider> contractProviders,
+ IDictionary<IUnit, PdbReader> sourceLocationProviders,
+ PhoneControlsPlugin phonePlugin) {
+
+ MetadataTraverser traverser = new MetadataTraverser(sink, sourceLocationProviders);
+ traverser.PhonePlugin = phonePlugin;
+ return traverser;
+ }
+
public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,
IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?
IDictionary<IUnit, PdbReader> sourceLocationProviders)
diff --git a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py index 89cc0c31..f4b3d6f4 100644 --- a/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py +++ b/BCT/PhoneControlsExtractor/PhoneControlsExtractor.py @@ -114,7 +114,8 @@ def outputPhoneControls(outputFileName): checked= control["Checked"]
unchecked= control["Unchecked"]
pageXAML= control["XAML"]
- outputFile.write(page + "," + os.path.basename(pageXAML) + "," + control["Type"] + "," + control["Name"] + "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + "\n")
+ # last comma is to account for bpl translation name, that is unknown for now
+ outputFile.write(page + "," + os.path.basename(pageXAML) + "," + control["Type"] + "," + control["Name"] + "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + ",\n")
outputFile.close()
diff --git a/BCT/TranslationPlugins/PhoneControlsPlugin.cs b/BCT/TranslationPlugins/PhoneControlsPlugin.cs index 8c7294ec..b24df692 100644 --- a/BCT/TranslationPlugins/PhoneControlsPlugin.cs +++ b/BCT/TranslationPlugins/PhoneControlsPlugin.cs @@ -27,10 +27,12 @@ namespace TranslationPlugins { }
public class ControlInfoStructure {
- public string Name;
- public string ClassName;
- public bool IsEnabled;
- public Visibility Visible;
+ public string Name { get; set; }
+ public string ClassName { get; set; }
+ public bool IsEnabled { get; set; }
+ public Visibility Visible { get; set; }
+ public string BplName { get; set; }
+
private IDictionary<Event, IList<HandlerSignature>> handlers;
public ControlInfoStructure() {
@@ -90,7 +92,7 @@ namespace TranslationPlugins { public class PhoneControlsPlugin : TranslationPlugin {
// TODO this will probably need a complete rewrite once it is event based, and make it more push than pull
// TODO but it doesn't make sense right now to make it BCT or CCI aware
- private static int CONFIG_LINE_FIELDS= 9;
+ private static int CONFIG_LINE_FIELDS= 10;
private static int PAGE_CLASS_FIELD= 0;
private static int PAGE_XAML_FIELD= 1;
private static int CONTROL_CLASS_FIELD= 2;
@@ -100,6 +102,7 @@ namespace TranslationPlugins { private static int CLICK_HANDLER_FIELD= 6;
private static int CHECKED_HANDLER_FIELD= 7;
private static int UNCHECKED_HANDLER_FIELD = 8;
+ private static int BPL_NAME_FIELD = 9;
private IDictionary<string, PageStructure> pageStructureInfo;
@@ -143,17 +146,63 @@ namespace TranslationPlugins { }
}
+ public void DumpControlStructure(StreamWriter outputStream) {
+ // maintain same format as input format
+ string pageClass, pageXAML, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;
+ outputStream.WriteLine(getMainPageXAML());
+ foreach (KeyValuePair<string, PageStructure> entry in this.pageStructureInfo) {
+ pageClass = entry.Key;
+ pageXAML = entry.Value.PageXAML;
+ foreach (ControlInfoStructure controlInfo in entry.Value.getAllControlsInfo()) {
+ controlClass= controlInfo.ClassName;
+ controlName = controlInfo.Name;
+ enabled= controlInfo.IsEnabled ? "true" : "false";
+ switch (controlInfo.Visible) {
+ case Visibility.Collapsed:
+ visibility = "Collapsed";
+ break;
+ default:
+ visibility = "Visible";
+ break;
+ }
+ IEnumerable<HandlerSignature> handlers= controlInfo.getHandlers(Event.Click);
+ if (handlers.Any()) {
+ clickHandler = handlers.First().Name;
+ } else {
+ clickHandler = "";
+ }
+
+ handlers = controlInfo.getHandlers(Event.Checked);
+ if (handlers.Any()) {
+ checkedHandler = handlers.First().Name;
+ } else {
+ checkedHandler = "";
+ }
+
+ handlers = controlInfo.getHandlers(Event.Unchecked);
+ if (handlers.Any()) {
+ uncheckedHandler = handlers.First().Name;
+ } else {
+ uncheckedHandler = "";
+ }
+ bplName = controlInfo.BplName;
+ outputStream.WriteLine(pageClass + "," + pageXAML + "," + controlClass + "," + controlName + "," + enabled + "," + visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + bplName);
+ }
+ }
+ }
+
private void LoadControlStructure(StreamReader configStream) {
// TODO it would be nice to have some kind of dynamic definition of config format
// TODO for now remember that config format is CSV
- // TODO each line is <pageClassName>,<pageXAMLPath>,<controlClassName>,<controlName>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>
+ // TODO each line is <pageClassName>,<pageXAMLPath>,<controlClassName>,<controlName>,<IsEnabledValue>,<VisibilityValue>,<ClickValue>,<CheckedValue>,<UncheckedValue>,<BPL control name>
+ // TODO BPL control name will most probably be empty, but it is useful to be able to dump it
// TODO check PhoneControlsExtractor.py
// TODO the page.xaml value is saved with no directory information: if two pages exist with same name but different directories it will treat them as the same
// TODO I'm not handling this for now, and I won't be handling relative/absolute URI either for now
try {
- string pageClass, pageXAML, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler;
+ string pageClass, pageXAML, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, uncheckedHandler, bplName;
string configLine = configStream.ReadLine();
string[] inputLine;
PageStructure pageStr;
@@ -178,6 +227,7 @@ namespace TranslationPlugins { clickHandler = inputLine[CLICK_HANDLER_FIELD];
checkedHandler = inputLine[CHECKED_HANDLER_FIELD];
uncheckedHandler = inputLine[UNCHECKED_HANDLER_FIELD];
+ bplName = inputLine[BPL_NAME_FIELD];
try {
pageStr = pageStructureInfo[pageClass];
@@ -193,6 +243,7 @@ namespace TranslationPlugins { controlInfoStr = new ControlInfoStructure();
controlInfoStr.Name = controlName;
controlInfoStr.ClassName = controlClass;
+ controlInfoStr.BplName = bplName;
}
controlInfoStr.IsEnabled = Boolean.Parse(enabled);
controlInfoStr.Visible = visibility == "Collapsed" ? Visibility.Collapsed : Visibility.Visible;
@@ -212,26 +263,48 @@ namespace TranslationPlugins { }
public IEnumerable<ControlInfoStructure> getControlsForPage(string pageClass) {
- return pageStructureInfo[pageClass].getAllControlsInfo();
+ try {
+ return pageStructureInfo[pageClass].getAllControlsInfo();
+ } catch (KeyNotFoundException) {
+ return null;
+ }
}
public string getXAMLForPage(string pageClass) {
- return pageStructureInfo[pageClass].PageXAML;
+ try {
+ return pageStructureInfo[pageClass].PageXAML;
+ } catch (KeyNotFoundException) {
+ return null;
+ }
}
public bool getIsEnabled(string pageClass, string controlName) {
- return pageStructureInfo[pageClass].getControlInfo(controlName).IsEnabled;
+ try {
+ return pageStructureInfo[pageClass].getControlInfo(controlName).IsEnabled;
+ } catch (KeyNotFoundException) {
+ // TODO not really correct
+ return false;
+ }
}
public Visibility getVisibility(string pageClass, string controlName) {
- return pageStructureInfo[pageClass].getControlInfo(controlName).Visible;
+ try {
+ return pageStructureInfo[pageClass].getControlInfo(controlName).Visible;
+ } catch (KeyNotFoundException) {
+ // TODO not really correct
+ return default(Visibility);
+ }
}
public IList<HandlerSignature> getHandlers(string pageClass, string controlName, string eventName) {
if (eventName != "Checked" && eventName != "Unchecked" && eventName != "Click")
throw new NotImplementedException("Event " + eventName + " is not translated or defined for control " + controlName + " in page " + pageClass);
- return pageStructureInfo[pageClass].getControlInfo(controlName).getHandlers((Event) Event.Parse(typeof(Event), eventName));
+ try {
+ return pageStructureInfo[pageClass].getControlInfo(controlName).getHandlers((Event) Event.Parse(typeof(Event), eventName));
+ } catch (KeyNotFoundException) {
+ return null;
+ }
}
}
}
|