diff options
author | 2011-07-20 14:24:41 -0700 | |
---|---|---|
committer | 2011-07-20 14:24:41 -0700 | |
commit | 912748bde10f4a9db6af6771a6d6861166d49006 (patch) | |
tree | 2f6891804fb577ea346951eca7f7ab4d1b376d1b /BCT | |
parent | 69269c0b4ba649ccffd2f678581b9ece04e0eae7 (diff) |
fixed a bug on current nav tracking
refactored methodcall visitor a bit
Diffstat (limited to 'BCT')
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 184 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 1 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs | 47 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs | 2 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs | 5 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs | 11 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 21 | ||||
-rw-r--r-- | BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py | 23 |
8 files changed, 177 insertions, 117 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index cffbc046..5e195300 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -449,7 +449,6 @@ namespace BytecodeTranslator /// <remarks>Stub, This one really needs comments!</remarks>
public override void Visit(IMethodCall methodCall) {
var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;
-
if (resolvedMethod == Dummy.Method) {
throw new TranslationException(
ExceptionType.UnresolvedMethod,
@@ -457,108 +456,131 @@ namespace BytecodeTranslator }
Bpl.IToken methodCallToken = methodCall.Token();
-
List<Bpl.Expr> inexpr;
List<Bpl.IdentifierExpr> outvars;
Bpl.IdentifierExpr thisExpr;
Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;
var proc = TranslateArgumentsAndReturnProcedure(methodCallToken, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed);
-
string methodname = proc.Name;
var translateAsFunctionCall = proc is Bpl.Function;
Bpl.QKeyValue attrib = null;
- if (!translateAsFunctionCall) {
- foreach (var a in resolvedMethod.Attributes) {
- if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
- attrib = new Bpl.QKeyValue(methodCallToken, "async", new List<object>(), null);
+
+ // TODO this code structure is quite chaotic, and some code needs to be evaluated regardless, hence the try-finally
+ try {
+ if (!translateAsFunctionCall) {
+ foreach (var a in resolvedMethod.Attributes) {
+ if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
+ attrib = new Bpl.QKeyValue(methodCallToken, "async", new List<object>(), null);
+ }
}
}
- }
- #region Special case: ctor call for a struct type
- if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct) {
- // then the method call looks like "&s.S.ctor(...)" for some variable s of struct type S
- // treat it as if it was "s := new S(...)"
- // So this code is the same as Visit(ICreateObjectInstance)
- // TODO: factor the code into a single method?
-
- // First generate an Alloc() call
- this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(thisExpr)));
+ if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct) {
+ handleStructConstructorCall(methodCall, methodCallToken, inexpr, outvars, thisExpr, proc);
+ return;
+ }
- // Second, generate the call to the appropriate ctor
- this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, proc.Name, inexpr, outvars));
+ Bpl.CallCmd call;
+ bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
+ bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
+ if (isEventAdd || isEventRemove) {
+ call = translateAddRemoveCall(methodCall, resolvedMethod, methodCallToken, inexpr, outvars, thisExpr, isEventAdd);
+ } else {
+ if (translateAsFunctionCall) {
+ var func = proc as Bpl.Function;
+ var exprSeq = new Bpl.ExprSeq();
+ foreach (var e in inexpr) {
+ exprSeq.Add(e);
+ }
+ var callFunction = new Bpl.NAryExpr(methodCallToken, new Bpl.FunctionCall(func), exprSeq);
+ this.TranslatedExpressions.Push(callFunction);
+ return;
+ } else {
+ if (attrib != null)
+ call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars, attrib);
+ else
+ call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ }
+ }
- // Generate an assumption about the dynamic type of the just allocated object
- this.StmtTraverser.StmtBuilder.Add(
- new Bpl.AssumeCmd(methodCallToken,
- Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
- this.sink.Heap.DynamicType(thisExpr),
- this.sink.FindOrCreateType(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)
- )
- )
- );
+ foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));
+ }
- return;
+ Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));
+ this.StmtTraverser.RaiseException(expr);
+ } finally {
+ if (PhoneCodeHelper.PhonePlugin != null) {
+ if (PhoneCodeHelper.isNavigationCall(methodCall, sink.host)) {
+ // the block is a potential page changer
+ List<Bpl.AssignLhs> lhs = new List<Bpl.AssignLhs>();
+ List<Bpl.Expr> rhs = new List<Bpl.Expr>();
+ Bpl.Expr value = new Bpl.LiteralExpr(Bpl.Token.NoToken, false);
+ rhs.Add(value);
+ Bpl.SimpleAssignLhs assignee=
+ new Bpl.SimpleAssignLhs(Bpl.Token.NoToken,
+ new Bpl.IdentifierExpr(Bpl.Token.NoToken,
+ sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_CONTINUE_ON_PAGE_VARIABLE, Bpl.Type.Bool)));
+ lhs.Add(assignee);
+ Bpl.AssignCmd assignCmd = new Bpl.AssignCmd(Bpl.Token.NoToken, lhs, rhs);
+ this.StmtTraverser.StmtBuilder.Add(assignCmd);
+ }
+ }
}
- #endregion
+ }
+ private Bpl.CallCmd translateAddRemoveCall(IMethodCall methodCall, IMethodDefinition resolvedMethod, Bpl.IToken methodCallToken, List<Bpl.Expr> inexpr, List<Bpl.IdentifierExpr> outvars, Bpl.IdentifierExpr thisExpr, bool isEventAdd) {
Bpl.CallCmd call;
- bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
- bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
- if (isEventAdd || isEventRemove) {
- var mName = resolvedMethod.Name.Value;
- var eventName = mName.Substring(mName.IndexOf('_') + 1);
- var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));
- Contract.Assert(eventDef != Dummy.Event);
- Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);
- Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);
-
- if (methodCall.IsStaticCall) {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));
- inexpr.Insert(0, Bpl.Expr.Ident(local));
- }
- else {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));
- inexpr[0] = Bpl.Expr.Ident(local);
- }
-
- System.Diagnostics.Debug.Assert(outvars.Count == 0);
- outvars.Insert(0, Bpl.Expr.Ident(local));
- string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;
- call = new Bpl.CallCmd(methodCallToken, methodName, inexpr, outvars);
- this.StmtTraverser.StmtBuilder.Add(call);
- if (methodCall.IsStaticCall) {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
- }
- else {
- this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCallToken, thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));
- }
+ var mName = resolvedMethod.Name.Value;
+ var eventName = mName.Substring(mName.IndexOf('_') + 1);
+ var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));
+ Contract.Assert(eventDef != Dummy.Event);
+ Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);
+ Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);
+
+ if (methodCall.IsStaticCall) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));
+ inexpr.Insert(0, Bpl.Expr.Ident(local));
} else {
- if (translateAsFunctionCall) {
- var func = proc as Bpl.Function;
- var exprSeq = new Bpl.ExprSeq();
- foreach (var e in inexpr) {
- exprSeq.Add(e);
- }
- var callFunction = new Bpl.NAryExpr(methodCallToken, new Bpl.FunctionCall(func), exprSeq);
- this.TranslatedExpressions.Push(callFunction);
- return;
-
- } else {
- if (attrib != null)
- call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars, attrib);
- else
- call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars);
- this.StmtTraverser.StmtBuilder.Add(call);
- }
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));
+ inexpr[0] = Bpl.Expr.Ident(local);
}
- foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));
+ System.Diagnostics.Debug.Assert(outvars.Count == 0);
+ outvars.Insert(0, Bpl.Expr.Ident(local));
+ string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;
+ call = new Bpl.CallCmd(methodCallToken, methodName, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ if (methodCall.IsStaticCall) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
+ } else {
+ this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCallToken, thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));
}
+ return call;
+ }
+
+ private void handleStructConstructorCall(IMethodCall methodCall, Bpl.IToken methodCallToken, List<Bpl.Expr> inexpr, List<Bpl.IdentifierExpr> outvars, Bpl.IdentifierExpr thisExpr, Bpl.DeclWithFormals proc) {
+ // then the method call looks like "&s.S.ctor(...)" for some variable s of struct type S
+ // treat it as if it was "s := new S(...)"
+ // So this code is the same as Visit(ICreateObjectInstance)
+ // TODO: factor the code into a single method?
- Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));
- this.StmtTraverser.RaiseException(expr);
+ // First generate an Alloc() call
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(thisExpr)));
+
+ // Second, generate the call to the appropriate ctor
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, proc.Name, inexpr, outvars));
+
+ // Generate an assumption about the dynamic type of the just allocated object
+ this.StmtTraverser.StmtBuilder.Add(
+ new Bpl.AssumeCmd(methodCallToken,
+ Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
+ this.sink.Heap.DynamicType(thisExpr),
+ this.sink.FindOrCreateType(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)
+ )
+ )
+ );
}
// REVIEW: Does "thisExpr" really need to come back as an identifier? Can't it be a general expression?
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index fef4c944..7abb070c 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -497,7 +497,6 @@ namespace BytecodeTranslator { #endregion
private void addPhoneTopLevelDeclarations() {
- // adding global variable for continue on page
Bpl.Variable continueOnPageVar = sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_CONTINUE_ON_PAGE_VARIABLE, Bpl.Type.Bool);
sink.TranslatedProgram.TopLevelDeclarations.Add(continueOnPageVar);
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs index 615b5a51..235cdc79 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs @@ -18,6 +18,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 static readonly string[] NAV_CALLS = { /*"GoBack", "GoForward", "Navigate", "StopLoading"*/ "Navigate", "GoBack" };
// awful hack. want to insert a nonexisting method call while traversing CCI AST, deferring it to Boogie translation
public const string BOOGIE_DO_HAVOC_CURRENTURI = BOOGIE_VAR_PREFIX + "Havoc_CurrentURI__";
@@ -69,12 +70,12 @@ namespace BytecodeTranslator.Phone { return false;
}
- public static bool isStringClass(this ITypeReference typeRef, MetadataReaderHost host) {
+ public static bool isStringClass(this ITypeReference typeRef, IMetadataHost host) {
ITypeReference targetType = host.PlatformType.SystemString;
return typeRef.isClass(targetType);
}
- public static bool isURIClass (this ITypeReference typeRef, MetadataReaderHost host) {
+ public static bool isURIClass (this ITypeReference typeRef, IMetadataHost host) {
Microsoft.Cci.Immutable.PlatformType platformType = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
if (platformType == null)
return false;
@@ -87,8 +88,27 @@ namespace BytecodeTranslator.Phone { return typeRef.isClass(uriTypeRef);
}
+ public static bool isNavigationServiceClass(this ITypeReference typeRef, IMetadataHost host) {
+ Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
+ 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 }, "");
+
+ IAssemblyReference phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
+ ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "System", "Windows", "Navigation", "NavigationService");
+
+ ITypeReference baseClass = typeRef.ResolvedType.BaseClasses.FirstOrDefault();
+ while (baseClass != null) {
+ if (baseClass.ResolvedType.Equals(phoneApplicationPageTypeRef.ResolvedType)) {
+ return true;
+ }
+ baseClass = baseClass.ResolvedType.BaseClasses.FirstOrDefault();
+ }
+
+ return false;
+ }
- public static bool isPhoneApplicationClass(this ITypeReference typeRef, MetadataReaderHost host) {
+ public static bool isPhoneApplicationClass(this ITypeReference typeRef, IMetadataHost host) {
Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
IAssemblyReference coreAssemblyRef = platform.CoreAssemblyRef;
AssemblyIdentity MSPhoneSystemWindowsAssemblyId =
@@ -100,7 +120,7 @@ namespace BytecodeTranslator.Phone { return typeRef.isClass(applicationClass);
}
- public static bool isPhoneApplicationPageClass(ITypeReference typeDefinition, MetadataReaderHost host) {
+ public static bool isPhoneApplicationPageClass(this ITypeReference typeRef, IMetadataHost host) {
Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;
AssemblyIdentity MSPhoneAssemblyId =
new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),
@@ -109,7 +129,7 @@ namespace BytecodeTranslator.Phone { IAssemblyReference phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);
ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Controls", "PhoneApplicationPage");
- ITypeReference baseClass = typeDefinition.ResolvedType.BaseClasses.FirstOrDefault();
+ ITypeReference baseClass = typeRef.ResolvedType.BaseClasses.FirstOrDefault();
while (baseClass != null) {
if (baseClass.ResolvedType.Equals(phoneApplicationPageTypeRef.ResolvedType)) {
return true;
@@ -157,6 +177,14 @@ namespace BytecodeTranslator.Phone { return Uri.IsWellFormedUriString(uri, UriKind.RelativeOrAbsolute);
}
+ public static bool isNavigationCall(IMethodCall call, IMetadataHost host) {
+ ITypeReference callType = call.MethodToCall.ContainingType;
+ if (!callType.isNavigationServiceClass(host))
+ return false;
+
+ return PhoneCodeHelper.NAV_CALLS.Contains(call.MethodToCall.Name.Value);
+ }
+
/// <summary>
/// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)
/// This method returns a base URI
@@ -172,5 +200,14 @@ namespace BytecodeTranslator.Phone { Uri mockStrippedUri = new Uri(str);
return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();
}
+
+ private static ITypeReference mainAppTypeRef;
+ public static void setMainAppTypeReference(ITypeReference appType) {
+ mainAppTypeRef = appType;
+ }
+
+ public static ITypeReference getMainAppTypeReference() {
+ return mainAppTypeRef;
+ }
}
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs index 49b43137..3a779dcd 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs @@ -8,8 +8,6 @@ using TranslationPlugins; namespace BytecodeTranslator.Phone {
class PhoneCodeWrapperWriter {
private static Sink sink;
- private static readonly string BOOGIE_MAIN_PROCEDURE = "$__BOOGIE_MAIN_PROCEDURE__$";
-
public static void createCodeWrapper(Sink sink) {
PhoneCodeWrapperWriter.sink = sink;
/*
diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs index 92090cc1..fec6e870 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs @@ -161,6 +161,7 @@ namespace BytecodeTranslator.Phone { IsStatic = false,
},
Instance = new ThisReference() { Type = methodBeingTraversed.Container },
+ Type=getTypeForClassname(controlInfo.ClassName),
};
}
@@ -293,7 +294,9 @@ namespace BytecodeTranslator.Phone { /// </summary>
///
public override void Visit(ITypeDefinition typeDefinition) {
- if (typeDefinition.IsClass && PhoneCodeHelper.isPhoneApplicationPageClass(typeDefinition, host)) {
+ if (typeDefinition.isPhoneApplicationClass(host)) {
+ PhoneCodeHelper.setMainAppTypeReference(typeDefinition);
+ } else if (typeDefinition.isPhoneApplicationPageClass(host)) {
base.Visit(typeDefinition);
}
}
diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs index 38fb2b58..ebbf9222 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs @@ -12,8 +12,6 @@ namespace BytecodeTranslator.Phone { private ITypeReference navigationSvcType;
private ITypeReference typeTraversed;
- private static readonly string[] NAV_CALLS = { /*"GoBack", "GoForward", "Navigate", "StopLoading"*/ "Navigate", "GoBack"};
-
public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed) : base() {
this.host = host;
this.typeTraversed = typeTraversed;
@@ -48,7 +46,8 @@ namespace BytecodeTranslator.Phone { Target = new TargetExpression() {
Type = host.PlatformType.SystemString,
Definition = new FieldReference() {
- ContainingType= typeTraversed,
+ // ContainingType= typeTraversed,
+ ContainingType= PhoneCodeHelper.getMainAppTypeReference(),
IsStatic=true,
Type=host.PlatformType.SystemString,
Name=host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),
@@ -96,7 +95,7 @@ namespace BytecodeTranslator.Phone { return;
string methodToCallName= methodToCall.Name.Value;
- if (!NAV_CALLS.Contains(methodToCallName))
+ if (!PhoneCodeHelper.NAV_CALLS.Contains(methodToCallName))
return;
navCallFound = true;
@@ -214,7 +213,7 @@ namespace BytecodeTranslator.Phone { Target = new TargetExpression() {
Type = host.PlatformType.SystemString,
Definition = new FieldReference() {
- ContainingType=typeTraversed,
+ ContainingType=PhoneCodeHelper.getMainAppTypeReference(),
IsStatic= true,
Type = host.PlatformType.SystemString,
Name = host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),
@@ -244,7 +243,7 @@ namespace BytecodeTranslator.Phone { Target = new TargetExpression() {
Type = host.PlatformType.SystemString,
Definition = new FieldReference() {
- ContainingType=typeTraversed,
+ ContainingType = PhoneCodeHelper.getMainAppTypeReference(),
IsStatic= true,
Type = host.PlatformType.SystemString,
Name = host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 7dae78e8..8745ee9e 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -176,16 +176,6 @@ namespace BytecodeTranslator { var primaryModule = modules[0];
- PhoneControlsPlugin phonePlugin = null;
- if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
- phonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);
- PhoneCodeHelper.PhonePlugin = phonePlugin;
- PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host);
- initTr.InjectPhoneCodeAssemblies(modules);
- PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(host);
- navTr.InjectPhoneCodeAssemblies(modules);
- }
-
TraverserFactory traverserFactory;
if (wholeProgram)
traverserFactory = new WholeProgram();
@@ -196,6 +186,17 @@ namespace BytecodeTranslator { TranslationHelper.tmpVarCounter = 0;
MetadataTraverser translator;
translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);
+
+ PhoneControlsPlugin phonePlugin = null;
+ if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {
+ phonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);
+ PhoneCodeHelper.PhonePlugin = phonePlugin;
+ PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host);
+ initTr.InjectPhoneCodeAssemblies(modules);
+ PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(host);
+ navTr.InjectPhoneCodeAssemblies(modules);
+ }
+
translator.TranslateAssemblies(modules);
foreach (var pair in sink.delegateTypeToDelegates.Values) {
diff --git a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py index c3c0a45f..c9a63c92 100644 --- a/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py +++ b/BCT/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py @@ -7,6 +7,9 @@ import xml.dom CONTROL_NAMES= ["Button", "CheckBox", "RadioButton"]
CONTAINER_CONTROL_NAMES= ["Canvas", "Grid", "StackPanel"]
+# TODO externalize strings, share with C# code
+CONTINUEONPAGE_VAR= "__BOOGIE_ContinueOnPage__"
+
staticControlsMap= {}
mainPageXAML= None
originalPageVars= []
@@ -73,9 +76,9 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): file.write("\tvar $isEnabled: bool;\n")
file.write("\tvar $handlerToActivate: int;\n")
- file.write("\tBOOGIE_continueOnPage:=true;\n")
+ file.write("\t" + CONTINUEONPAGE_VAR +":=true;\n")
file.write("\thavoc $activeControl;\n")
- file.write("\twhile (BOOGIE_continueOnPage) {\n")
+ file.write("\twhile (" + CONTINUEONPAGE_VAR + ") {\n")
activeControl=0
for entry in staticControlsMap[originalPageName]["controls"].keys():
controlInfo= staticControlsMap[originalPageName]["controls"][entry]
@@ -84,7 +87,6 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): else:
file.write("\t\telse if ($activeControl == " + str(activeControl) + ") {\n")
- file.write("\t\t\t//TODO assuming split fields heap representation\n")
file.write("\t\t\t$control := " + controlInfo["bplName"] + "[" + boogiePageName + "];\n")
file.write("\t\t\tcall $isEnabledRef := System.Windows.Controls.Control.get_IsEnabled($control);\n")
file.write("\t\t\t$isEnabled := Box2Bool(Ref2Box($isEnabledRef));\n")
@@ -92,15 +94,15 @@ def outputPageControlDriver(file, originalPageName, boogiePageName): file.write("\t\t\t\thavoc $handlerToActivate;\n")
if not controlInfo["clickHandler"] == "":
file.write("\t\t\t\tif ($handlerToActivate == 0) {\n")
- file.write("\t\t\t\t\t" + staticControlsMap[originalPageName]["class"] + "." + controlInfo["clickHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
+ file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["clickHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
file.write("\t\t\t\t}\n")
if not controlInfo["checkedHandler"] == "":
file.write("\t\t\t\tif ($handlerToActivate == 1) {\n")
- file.write("\t\t\t\t\t" + staticControlsMap[originalPageName]["class"] + "." + controlInfo["checkedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
+ file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["checkedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
file.write("\t\t\t\t}\n")
if not controlInfo["uncheckedHandler"] == "":
file.write("\t\t\t\tif ($handlerToActivate == 2) {\n")
- file.write("\t\t\t\t\t" + staticControlsMap[originalPageName]["class"] + "." + controlInfo["uncheckedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
+ file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["uncheckedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n")
file.write("\t\t\t\t}\n")
file.write("\t\t\t}\n")
@@ -136,11 +138,11 @@ def outputControlDrivers(file): file.write("}\n")
def outputURIHavocProcedure(file):
- file.write("procedure __BOOGIE_HavocCall__();\n")
- file.write("implementation __BOOGIE_HavocCall__() {\n")
- # TODO change this name to a dynamically inferred one. This is just for testing right now
+ file.write("procedure __BOOGIE_Havoc_CurrentURI__();\n")
+ file.write("implementation __BOOGIE_Havoc_CurrentURI__() {\n")
+ file.write("// TODO change this name to a dynamically inferred one. This is just for testing right now\n")
file.write("\thavoc SimpleNavigationApp.App.$__BOOGIE_CurrentNavigationURI__;\n")
- # TODO write assume statement to filter havoc'd variable to either of all pages
+ file.write("// TODO write assume statements to filter havoc'd variable to either of all pages\n")
# file.write("\tassume )
file.write("}\n")
@@ -181,7 +183,6 @@ def buildControlInfo(controlInfoFileName): infoLine=file.readline().strip()
file.close()
- print staticControlsMap
def main():
controlFile= ""
|