summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator
diff options
context:
space:
mode:
Diffstat (limited to 'BCT/BytecodeTranslator')
-rw-r--r--BCT/BytecodeTranslator/Heap.cs7
-rw-r--r--BCT/BytecodeTranslator/MetadataTraverser.cs4
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs24
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs10
-rw-r--r--BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs34
-rw-r--r--BCT/BytecodeTranslator/Program.cs26
-rw-r--r--BCT/BytecodeTranslator/Sink.cs6
-rw-r--r--BCT/BytecodeTranslator/StatementTraverser.cs11
-rw-r--r--BCT/BytecodeTranslator/TranslationHelper.cs2
9 files changed, 96 insertions, 28 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 751d8baa..648d4c9f 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -205,11 +205,8 @@ namespace BytecodeTranslator {
/// </summary>
public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
+ string fieldname = MemberHelper.GetMemberSignature(field, NameFormattingOptions.DocumentationId);
fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
- // Need to append something to the name to avoid name clashes with other members (of a different
- // type) that have the same name.
- fieldname += "$field";
Bpl.IToken tok = field.Token();
if (field.IsStatic) {
@@ -227,7 +224,7 @@ namespace BytecodeTranslator {
public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
+ string fieldname = MemberHelper.GetMemberSignature(e, NameFormattingOptions.DocumentationId);
fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);
Bpl.IToken tok = e.Token();
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index f6903b8a..30def4a2 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -122,7 +122,7 @@ namespace BytecodeTranslator {
string fullyQualifiedName = namedTypeDef.ToString();
string xamlForClass = PhoneCodeHelper.instance().getXAMLForPage(fullyQualifiedName);
if (xamlForClass != null) { // if not it is possibly an abstract page
- string uriName = PhoneControlsPlugin.getURIBase(xamlForClass);
+ string uriName = UriHelper.getURIBase(xamlForClass);
Bpl.Constant uriConstant = sink.FindOrCreateConstant(uriName);
PhoneCodeHelper.instance().setBoogieStringPageNameForPageClass(fullyQualifiedName, uriConstant.Name);
}
@@ -223,7 +223,7 @@ namespace BytecodeTranslator {
private bool sawCctor = false;
private void CreateStaticConstructor(ITypeDefinition typeDefinition) {
- var typename = TypeHelper.GetTypeName(typeDefinition);
+ var typename = TypeHelper.GetTypeName(typeDefinition, Microsoft.Cci.NameFormattingOptions.DocumentationId);
typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#cctor",
new Bpl.TypeVariableSeq(),
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index 6be74264..cd71e7cc 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -10,6 +10,28 @@ using Microsoft.Cci.MutableCodeModel;
namespace BytecodeTranslator.Phone {
public static class UriHelper {
/// <summary>
+ /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)
+ /// This method returns a base URI
+ /// </summary>
+ /// <param name="uri"></param>
+ /// <returns></returns>
+ public static string getURIBase(string uri) {
+ // I need to build an absolute URI just to call getComponents() ...
+ Uri mockBaseUri = new Uri("mock://mock/", UriKind.RelativeOrAbsolute);
+ Uri realUri;
+ try {
+ realUri = new Uri(uri, UriKind.Absolute);
+ } catch (UriFormatException) {
+ // uri string is relative
+ realUri = new Uri(mockBaseUri, uri);
+ }
+
+ string str = realUri.GetComponents(UriComponents.Path | UriComponents.StrongAuthority | UriComponents.Scheme, UriFormat.UriEscaped);
+ Uri mockStrippedUri = new Uri(str);
+ return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();
+ }
+
+ /// <summary>
/// checks if argument is locally created URI with static URI target
/// </summary>
/// <param name="arg"></param>
@@ -32,7 +54,7 @@ namespace BytecodeTranslator.Phone {
if (staticURITarget == null)
return false;
- uri = staticURITarget.Value as string;
+ uri= staticURITarget.Value as string;
return true;
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
index 4d1f60fb..d79d2c00 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
@@ -31,6 +31,7 @@ namespace BytecodeTranslator.Phone {
private IAssemblyReference coreAssemblyRef;
private IAssemblyReference phoneAssembly;
private IAssemblyReference phoneSystemWindowsAssembly;
+ private IAssemblyReference MSPhoneControlsAssembly;
private INamespaceTypeReference appBarIconButtonType;
private INamespaceTypeReference checkBoxType;
private INamespaceTypeReference radioButtonType;
@@ -39,6 +40,7 @@ namespace BytecodeTranslator.Phone {
private INamespaceTypeReference toggleButtonType;
private INamespaceTypeReference controlType;
private INamespaceTypeReference uiElementType;
+ private INamespaceTypeReference pivotType;
private CompileTimeConstant trueConstant;
private CompileTimeConstant falseConstant;
@@ -65,6 +67,8 @@ namespace BytecodeTranslator.Phone {
return checkBoxType;
} else if (classname == "ApplicationBarIconButton") {
return appBarIconButtonType;
+ } else if (classname == "Pivot") {
+ return pivotType;
} else if (classname == "DummyType") {
return Dummy.Type;
} else {
@@ -87,12 +91,17 @@ namespace BytecodeTranslator.Phone {
AssemblyIdentity MSPhoneAssemblyId =
new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+ AssemblyIdentity MSPhoneControlsAssemblyId=
+ new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone.Controls"), "", new Version("7.0.0.0"),
+ new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");
+
AssemblyIdentity MSPhoneSystemWindowsAssemblyId =
new AssemblyIdentity(host.NameTable.GetNameFor("System.Windows"), coreAssemblyRef.Culture, coreAssemblyRef.Version,
coreAssemblyRef.PublicKeyToken, "");
phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
phoneSystemWindowsAssembly = host.FindAssembly(MSPhoneSystemWindowsAssemblyId);
+ MSPhoneControlsAssembly= host.FindAssembly(MSPhoneControlsAssemblyId);
// TODO determine the needed types dynamically
appBarIconButtonType= platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarIconButton");
@@ -103,6 +112,7 @@ namespace BytecodeTranslator.Phone {
toggleButtonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Primitives", "ToggleButton");
controlType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Control");
uiElementType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "UIElement");
+ pivotType = platform.CreateReference(MSPhoneControlsAssembly, "Microsoft", "Phone", "Controls", "Pivot");
trueConstant = new CompileTimeConstant() {
Type = platform.SystemBoolean,
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
index f94f0044..2d3533aa 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -13,6 +13,8 @@ namespace BytecodeTranslator.Phone {
private ITypeReference cancelEventArgsType;
private ITypeReference typeTraversed;
private IMethodDefinition methodTraversed;
+ private static HashSet<IMethodDefinition> navCallers= new HashSet<IMethodDefinition>();
+ public static IEnumerable<IMethodDefinition> NavCallers { get { return navCallers; } }
public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed, IMethodDefinition methodTraversed) : base() {
this.host = host;
@@ -29,10 +31,13 @@ namespace BytecodeTranslator.Phone {
cancelEventArgsType = platform.CreateReference(assembly, "System", "ComponentModel", "CancelEventArgs");
}
+ public override void Visit(IEnumerable<IAssemblyReference> assemblyReferences) {
+ base.Visit(assemblyReferences);
+ }
+
+
public override void Visit(IMethodDefinition method) {
if (method.IsConstructor && PhoneTypeHelper.isPhoneApplicationClass(typeTraversed, host)) {
- // TODO BUG doing this is generating a fresh variable definition somewhere that the BCT then translates into two different (identical) declarations
- // TODO maybe a bug introduced here or a BCT bug
string mainPageUri = PhoneCodeHelper.instance().PhonePlugin.getMainPageXAML();
SourceMethodBody sourceBody = method.Body as SourceMethodBody;
if (sourceBody != null) {
@@ -41,7 +46,7 @@ namespace BytecodeTranslator.Phone {
Assignment uriInitAssign = new Assignment() {
Source = new CompileTimeConstant() {
Type = host.PlatformType.SystemString,
- Value = PhoneControlsPlugin.getURIBase(mainPageUri),
+ Value = UriHelper.getURIBase(mainPageUri),
},
Type = host.PlatformType.SystemString,
Target = new TargetExpression() {
@@ -78,10 +83,13 @@ namespace BytecodeTranslator.Phone {
navCallFound = false;
navCallIsStatic = false;
this.Visit(statement);
- if (navCallFound && navCallIsStatic) {
- staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));
- } else if (navCallFound) {
- nonStaticNavStmts.Add(statement);
+ if (navCallFound) {
+ navCallers.Add(methodTraversed);
+ if (navCallIsStatic) {
+ staticNavStmts.Add(new Tuple<IStatement, StaticURIMode, string>(statement, currentStaticMode, unpurifiedFoundURI));
+ } else {
+ nonStaticNavStmts.Add(statement);
+ }
}
}
@@ -106,6 +114,8 @@ namespace BytecodeTranslator.Phone {
UriHelper.isArgumentURILocallyCreatedStaticRoot(expr, host, out target);
if (!isStatic)
target = "--Other non inferrable target--";
+ else
+ target = UriHelper.getURIBase(target);
} catch (InvalidOperationException) {
}
}
@@ -140,11 +150,13 @@ namespace BytecodeTranslator.Phone {
string target;
if (isNavigationOnBackKeyPressHandler(methodCall, out target)) {
PhoneCodeHelper.instance().BackKeyPressNavigates = true;
- ICollection<string> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed];
- if (targets == null) {
+ ICollection<string> targets;
+ try {
+ targets= PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed];
+ } catch (KeyNotFoundException) {
targets = new HashSet<string>();
}
- targets.Add(target);
+ targets.Add("\"" + target + "\"");
PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed]= targets;
} else if (isCancelOnBackKeyPressHandler(methodCall)) {
PhoneCodeHelper.instance().BackKeyPressHandlerCancels = true;
@@ -247,7 +259,7 @@ namespace BytecodeTranslator.Phone {
Assignment currentURIAssign = new Assignment() {
Source = new CompileTimeConstant() {
Type = host.PlatformType.SystemString,
- Value = PhoneControlsPlugin.getURIBase(entry.Item3),
+ Value = UriHelper.getURIBase(entry.Item3).ToLower(),
},
Type = host.PlatformType.SystemString,
Target = new TargetExpression() {
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 18d735af..231a21cf 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -31,6 +31,9 @@ namespace BytecodeTranslator {
[OptionDescription("Break into debugger", ShortForm = "break")]
public bool breakIntoDebugger = false;
+ [OptionDescription("Emit a 'capture state' directive after each statement, (default: false)", ShortForm = "c")]
+ public bool captureState = false;
+
[OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
public List<string> libpaths = new List<string>();
@@ -165,16 +168,16 @@ namespace BytecodeTranslator {
return result;
}
- public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options/*?*/ options, List<Regex> exemptionList, bool whiteList) {
+ public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Contract.Requires(assemblyNames != null);
Contract.Requires(heapFactory != null);
- var libPaths = options == null ? null : options.libpaths;
- var wholeProgram = options == null ? false : options.wholeProgram;
- var/*?*/ stubAssemblies = options == null ? null : options.stub;
- var phoneControlsConfigFile = options == null ? null : options.phoneControls;
- var doPhoneNav = options == null ? false : options.phoneNavigationCode;
- var doPhoneFeedback = options == null ? false : options.phoneFeedbackCode;
+ var libPaths = options.libpaths;
+ var wholeProgram = options.wholeProgram;
+ var/*?*/ stubAssemblies = options.stub;
+ var phoneControlsConfigFile = options.phoneControls;
+ var doPhoneNav = options.phoneNavigationCode;
+ var doPhoneFeedback = options.phoneFeedbackCode;
var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);
Host = host;
@@ -247,7 +250,7 @@ namespace BytecodeTranslator {
else
traverserFactory = new CLRSemantics();
- Sink sink= new Sink(host, traverserFactory, heapFactory, exemptionList, whiteList);
+ Sink sink= new Sink(host, traverserFactory, heapFactory, options, exemptionList, whiteList);
TranslationHelper.tmpVarCounter = 0;
MetadataTraverser translator;
translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
@@ -324,6 +327,13 @@ namespace BytecodeTranslator {
System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount);
}
+ if (PhoneCodeHelper.instance().PhoneNavigationToggled) {
+ // TODO integrate into the pipeline and spit out the boogie code
+ foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) {
+ System.Console.WriteLine(def.ToString());
+ }
+ }
+
Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");
Prelude.Emit(writer);
sink.TranslatedProgram.Emit(writer);
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index b2c1177e..1427b836 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -27,10 +27,11 @@ namespace BytecodeTranslator {
get { return this.factory; }
}
readonly TraverserFactory factory;
+ private readonly Options options;
readonly bool whiteList;
readonly List<Regex> exemptionList;
- public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, List<Regex> exemptionList, bool whiteList) {
+ public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Contract.Requires(host != null);
Contract.Requires(factory != null);
Contract.Requires(heapFactory != null);
@@ -38,6 +39,7 @@ namespace BytecodeTranslator {
this.host = host;
this.factory = factory;
var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?
+ this.options = options;
this.exemptionList = exemptionList;
this.whiteList = whiteList;
if (this.TranslatedProgram == null) {
@@ -52,6 +54,8 @@ namespace BytecodeTranslator {
}
}
+ public Options Options { get { return this.options; } }
+
public Heap Heap {
get { return this.heap; }
}
diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 4c927b3e..015e57ce 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -54,6 +54,8 @@ namespace BytecodeTranslator
public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();
private bool contractContext;
internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();
+ private bool captureState;
+ private static int captureStateCounter = 0;
#region Constructors
public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {
@@ -61,6 +63,7 @@ namespace BytecodeTranslator
this.factory = sink.Factory;
PdbReader = pdbReader;
this.contractContext = contractContext;
+ this.captureState = sink.Options.captureState;
}
#endregion
@@ -108,6 +111,14 @@ namespace BytecodeTranslator
public override void Visit(IStatement statement) {
EmitSourceContext(statement);
+ if (this.sink.Options.captureState) {
+ var tok = statement.Token();
+ var state = String.Format("s{0}", StatementTraverser.captureStateCounter++);
+ var attrib = new Bpl.QKeyValue(tok, "captureState ", new List<object> { state }, null);
+ StmtBuilder.Add(
+ new Bpl.AssumeCmd(tok, Bpl.Expr.True, attrib)
+ );
+ }
base.Visit(statement);
}
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index a17165ee..924aba5e 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -42,6 +42,7 @@ namespace BytecodeTranslator {
var parameterToken = parameterDefinition.Token();
var typeToken = parameterDefinition.Type.Token();
var parameterName = TranslationHelper.TurnStringIntoValidIdentifier(parameterDefinition.Name.Value);
+ if (String.IsNullOrWhiteSpace(parameterName)) parameterName = "P" + parameterDefinition.Index.ToString();
this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);
if (parameterDefinition.IsByReference) {
@@ -154,6 +155,7 @@ namespace BytecodeTranslator {
s = s.Replace('[', '$');
s = s.Replace(']', '$');
s = s.Replace('|', '$');
+ s = s.Replace('+', '$');
s = GetRidOfSurrogateCharacters(s);
return s;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 16:41:45 +0000