diff --git a/BCT.sln b/BCT.sln index 23a4f10..4128611 100644 --- a/BCT.sln +++ b/BCT.sln @@ -1,7 +1,7 @@  Microsoft Visual Studio Solution File, Format Version 12.00 -# Visual Studio 2013 -VisualStudioVersion = 12.0.21005.1 +# Visual Studio 14 +VisualStudioVersion = 14.0.25420.1 MinimumVisualStudioVersion = 10.0.40219.1 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BytecodeTranslator", "BytecodeTranslator\BytecodeTranslator.csproj", "{9C8E4D74-0251-479D-ADAC-A9A469977301}" EndProject @@ -28,11 +28,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractExtractor", "..\CCI EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ControlAndDataFlowGraph", "..\CCICodePlex\Ast\Metadata\Sources\ControlAndDataFlowGraph\ControlAndDataFlowGraph.csproj", "{2596EFB0-87AE-42CE-89EB-84F35D6350D2}" EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILGarbageCollect", "..\CCICodePlex\Ast\Metadata\Samples\ILGarbageCollect\ILGarbageCollect.csproj", "{60CD0C85-1E4A-4068-A4EC-D15B7981A908}" - ProjectSection(ProjectDependencies) = postProject - {6D83F687-ABB5-40B3-915E-CA53DA0EB7F3} = {6D83F687-ABB5-40B3-915E-CA53DA0EB7F3} - EndProjectSection -EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILGenerator", "..\CCICodePlex\Ast\Metadata\Sources\ILGenerator\ILGenerator.csproj", "{08156C78-403A-4112-AD81-8646AC51CD2F}" EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "MetadataHelper", "..\CCICodePlex\Ast\Metadata\Sources\MetadataHelper\MetadataHelper.csproj", "{4A34A3C5-6176-49D7-A4C5-B2B671247F8F}" @@ -459,51 +454,6 @@ Global {2596EFB0-87AE-42CE-89EB-84F35D6350D2}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|Any CPU {2596EFB0-87AE-42CE-89EB-84F35D6350D2}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU {2596EFB0-87AE-42CE-89EB-84F35D6350D2}.z3apidebug|x86.ActiveCfg = Debug|Any CPU - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|Any CPU.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|Mixed Platforms.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|Mixed Platforms.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|x86.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Checked|x86.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|Any CPU.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|Mixed Platforms.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|Mixed Platforms.Build.0 = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|x86.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.CompilerOnly|x86.Build.0 = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|Any CPU.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|Mixed Platforms.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|Mixed Platforms.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|x86.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Debug|x86.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|Any CPU.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|Mixed Platforms.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|Mixed Platforms.Build.0 = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|x86.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.FastpathSim|x86.Build.0 = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|Any CPU.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|Mixed Platforms.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|Mixed Platforms.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|x86.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyDebug|x86.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|Any CPU.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|Mixed Platforms.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|Mixed Platforms.Build.0 = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|x86.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.NightlyRelease|x86.Build.0 = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|Any CPU.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|Mixed Platforms.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|Mixed Platforms.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|x86.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.QED|x86.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|Any CPU.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|Mixed Platforms.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|Mixed Platforms.Build.0 = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|x86.ActiveCfg = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.Release|x86.Build.0 = Release|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|Any CPU.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|Mixed Platforms.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|Mixed Platforms.Build.0 = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|x86.ActiveCfg = Debug|x86 - {60CD0C85-1E4A-4068-A4EC-D15B7981A908}.z3apidebug|x86.Build.0 = Debug|x86 {08156C78-403A-4112-AD81-8646AC51CD2F}.Checked|Any CPU.ActiveCfg = CompilerOnly|Any CPU {08156C78-403A-4112-AD81-8646AC51CD2F}.Checked|Any CPU.Build.0 = CompilerOnly|Any CPU {08156C78-403A-4112-AD81-8646AC51CD2F}.Checked|Mixed Platforms.ActiveCfg = CompilerOnly|Any CPU diff --git a/BytecodeTranslator/BytecodeTranslator.csproj b/BytecodeTranslator/BytecodeTranslator.csproj index e28effc..e54981f 100644 --- a/BytecodeTranslator/BytecodeTranslator.csproj +++ b/BytecodeTranslator/BytecodeTranslator.csproj @@ -103,18 +103,11 @@ - - - - - - - @@ -125,10 +118,7 @@ - - - @@ -148,10 +138,6 @@ {fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5} ParserHelper - - {60CD0C85-1E4A-4068-A4EC-D15B7981A908} - ILGarbageCollect - {4A34A3C5-6176-49D7-A4C5-B2B671247F8F} MetadataHelper diff --git a/BytecodeTranslator/ExceptionAnalysis.cs b/BytecodeTranslator/ExceptionAnalysis.cs index f1f44fe..3ad8f98 100644 --- a/BytecodeTranslator/ExceptionAnalysis.cs +++ b/BytecodeTranslator/ExceptionAnalysis.cs @@ -18,7 +18,6 @@ using Bpl = Microsoft.Boogie; using System.Diagnostics.Contracts; using TranslationPlugins; -using BytecodeTranslator.Phone; namespace BytecodeTranslator { diff --git a/BytecodeTranslator/ExpressionTraverser.cs b/BytecodeTranslator/ExpressionTraverser.cs index 366b9e7..4172a2f 100644 --- a/BytecodeTranslator/ExpressionTraverser.cs +++ b/BytecodeTranslator/ExpressionTraverser.cs @@ -18,7 +18,6 @@ using Bpl = Microsoft.Boogie; using System.Diagnostics.Contracts; using TranslationPlugins; -using BytecodeTranslator.Phone; namespace BytecodeTranslator @@ -697,79 +696,59 @@ public override void TraverseChildren(IMethodCall methodCall) { var translateAsFunctionCall = proc is Bpl.Function; bool isAsync = false; - // 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")) { - isAsync = true; - } + if (!translateAsFunctionCall) { + foreach (var a in resolvedMethod.Attributes) { + if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) { + isAsync = true; } } + } - var deferringCtorCall = resolvedMethod.IsConstructor && methodCall.ThisArgument is IThisReference; - // REVIEW!! Ask Herman: is the above test enough? The following test is used in FindCtorCall.IsDeferringCtor, - // but it doesn't work when the type is a struct S because then "this" has a type of "&S". - //&& TypeHelper.TypesAreEquivalent(resolvedMethod.ContainingType, methodCall.ThisArgument.Type); + var deferringCtorCall = resolvedMethod.IsConstructor && methodCall.ThisArgument is IThisReference; + // REVIEW!! Ask Herman: is the above test enough? The following test is used in FindCtorCall.IsDeferringCtor, + // but it doesn't work when the type is a struct S because then "this" has a type of "&S". + //&& TypeHelper.TypesAreEquivalent(resolvedMethod.ContainingType, methodCall.ThisArgument.Type); - if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct && !deferringCtorCall) { - handleStructConstructorCall(methodCall, methodCallToken, inexpr, outvars, thisExpr, proc); - return; - } + if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct && !deferringCtorCall) { + handleStructConstructorCall(methodCall, methodCallToken, inexpr, outvars, thisExpr, proc); + return; + } - 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 List(); - 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 { - EmitLineDirective(methodCallToken); - call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars); - call.IsAsync = isAsync; - this.StmtTraverser.StmtBuilder.Add(call); + 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 List(); + 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 { + EmitLineDirective(methodCallToken); + call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars); + call.IsAsync = isAsync; + this.StmtTraverser.StmtBuilder.Add(call); } + } - foreach (KeyValuePair> kv in toBoxed) { - var lhs = kv.Key; - var tuple = kv.Value; - var rhs = tuple.Item1; - Bpl.Expr fromUnion = this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs, tuple.Item2); - this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion)); - } - - if (this.sink.Options.modelExceptions == 2 - || (this.sink.Options.modelExceptions == 1 && this.sink.MethodThrowsExceptions(resolvedMethod))) { - 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 { - // 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) { - if (PhoneCodeHelper.instance().PhoneNavigationToggled) { - if (PhoneCodeHelper.instance().isNavigationCall(methodCall)) { - Bpl.AssignCmd assignCmd = PhoneCodeHelper.instance().createBoogieNavigationUpdateCmd(sink); - this.StmtTraverser.StmtBuilder.Add(assignCmd); - } - } + foreach (KeyValuePair> kv in toBoxed) { + var lhs = kv.Key; + var tuple = kv.Value; + var rhs = tuple.Item1; + Bpl.Expr fromUnion = this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs, tuple.Item2); + this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion)); + } - if (PhoneCodeHelper.instance().PhoneFeedbackToggled) { - if (PhoneCodeHelper.instance().isMethodKnownUIChanger(methodCall)) { - Bpl.AssumeCmd assumeFalse = new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False); - this.StmtTraverser.StmtBuilder.Add(assumeFalse); - } - } - } + if (this.sink.Options.modelExceptions == 2 + || (this.sink.Options.modelExceptions == 1 && this.sink.MethodThrowsExceptions(resolvedMethod))) { + 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); } } @@ -991,35 +970,7 @@ public override void TraverseChildren(IAssignment assignment) { 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 - // 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) { - 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); - } - - /// - /// Patch, to account for URIs that cannot be tracked because of current dataflow restrictions - /// - private void TranslateHavocCurrentURI() { - // TODO move away phone related code from the translation, it would be better to have 2 or more translation phases - IMethodReference havocMethod= PhoneCodeHelper.instance().getUriHavocerMethod(sink); - Sink.ProcedureInfo procInfo= sink.FindOrCreateProcedure(havocMethod.ResolvedMethod); - Bpl.CallCmd havocCall = new Bpl.CallCmd(Bpl.Token.NoToken, procInfo.Decl.Name, new List(), new List()); - StmtTraverser.StmtBuilder.Add(havocCall); + TranslateAssignment(tok, assignment.Target.Definition, assignment.Target.Instance, assignment.Source); } /// diff --git a/BytecodeTranslator/MetadataTraverser.cs b/BytecodeTranslator/MetadataTraverser.cs index 39a8dac..9957af6 100644 --- a/BytecodeTranslator/MetadataTraverser.cs +++ b/BytecodeTranslator/MetadataTraverser.cs @@ -17,7 +17,6 @@ using Bpl = Microsoft.Boogie; using System.Diagnostics.Contracts; using TranslationPlugins; -using BytecodeTranslator.Phone; using BytecodeTranslator.TranslationPlugins; @@ -117,9 +116,6 @@ public override void TraverseChildren(ITypeDefinition typeDefinition) { var savedPrivateTypes = this.privateTypes; this.privateTypes = new List(); - trackPhonePageNameVariableName(typeDefinition); - trackPhoneApplicationClassname(typeDefinition); - var gtp = typeDefinition as IGenericTypeParameter; if (gtp != null) { return; @@ -161,52 +157,6 @@ public override void TraverseChildren(ITypeDefinition typeDefinition) { } List privateTypes = new List(); - private void trackPhoneApplicationClassname(ITypeDefinition typeDef) { - if (PhoneCodeHelper.instance().PhonePlugin != null && typeDef.isPhoneApplicationClass(sink.host)) { - INamespaceTypeDefinition namedTypeDef = typeDef as INamespaceTypeDefinition; - // string fullyQualifiedName = namedTypeDef.ContainingNamespace.Name.Value + "." + namedTypeDef.Name.Value; - string fullyQualifiedName = namedTypeDef.ToString(); - PhoneCodeHelper.instance().setMainAppTypeReference(typeDef); - PhoneCodeHelper.instance().setMainAppTypeName(fullyQualifiedName); - } - } - - private void trackPhonePageNameVariableName(ITypeDefinition typeDef) { - if (PhoneCodeHelper.instance().PhonePlugin != null && typeDef.isPhoneApplicationPageClass(sink.host)) { - INamespaceTypeDefinition namedTypeDef = typeDef as INamespaceTypeDefinition; - string fullyQualifiedName = namedTypeDef.ToString(); - string xamlForClass = PhoneCodeHelper.instance().getXAMLForPage(fullyQualifiedName); - if (xamlForClass != null) { // if not it is possibly an abstract page - string uriName = UriHelper.getURIBase(xamlForClass); - Bpl.Constant uriConstant = sink.FindOrCreateConstant(uriName); - PhoneCodeHelper.instance().setBoogieStringPageNameForPageClass(fullyQualifiedName, uriConstant.Name); - } - } - } - - /* - private void translateAnonymousControlsForPage(ITypeDefinition typeDef) { - if (PhoneCodeHelper.instance().PhonePlugin != null && typeDef.isPhoneApplicationPageClass(sink.host)) { - IEnumerable pageCtrls= PhoneCodeHelper.instance().PhonePlugin.getControlsForPage(typeDef.ToString()); - foreach (ControlInfoStructure ctrlInfo in pageCtrls) { - if (ctrlInfo.Name.Contains(PhoneControlsPlugin.BOOGIE_DUMMY_CONTROL) || ctrlInfo.Name == Dummy.Name.Value) { - string anonymousControlName = ctrlInfo.Name; - IFieldDefinition fieldDef = new FieldDefinition() { - ContainingTypeDefinition = typeDef, - Name = sink.host.NameTable.GetNameFor(anonymousControlName), - InternFactory = sink.host.InternFactory, - Visibility = TypeMemberVisibility.Public, - Type = sink.host.PlatformType.SystemObject, - IsStatic = false, - }; - (typeDef as Microsoft.Cci.MutableCodeModel.NamespaceTypeDefinition).Fields.Add(fieldDef); - //sink.FindOrCreateFieldVariable(fieldDef); - } - } - } - } - */ - private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) { Contract.Requires(typeDefinition.IsStruct); @@ -418,32 +368,9 @@ public override void TraverseChildren(IMethodDefinition method) { decl.AddAttribute("entrypoint"); } - // FEEDBACK inline handler methods to avoid more false alarms - if (PhoneCodeHelper.instance().PhoneFeedbackToggled && PhoneCodeHelper.instance().isMethodInputHandlerOrFeedbackOverride(method) && - !PhoneCodeHelper.instance().isMethodIgnoredForFeedback(method)) { - proc.AddAttribute("inline", new Bpl.LiteralExpr(Bpl.Token.NoToken, Microsoft.Basetypes.BigNum.ONE)); - PhoneCodeHelper.instance().trackCallableMethod(proc); - } - try { StatementTraverser stmtTraverser = this.Factory.MakeStatementTraverser(this.sink, this.PdbReader, false); - // FEEDBACK if this is a feedback method it will be plagued with false asserts. They will trigger if $Exception becomes other than null - // FEEDBACK for modular analysis we need it to be non-null at the start - // FEEDBACK also, callee is obviously non null - IMethodDefinition translatedMethod= sink.getMethodBeingTranslated(); - if (PhoneCodeHelper.instance().PhoneFeedbackToggled && translatedMethod != null && - PhoneCodeHelper.instance().isMethodInputHandlerOrFeedbackOverride(translatedMethod)) { - // assign null to exception - List assignee= new List(); - Bpl.AssignLhs exceptionAssignee= new Bpl.SimpleAssignLhs(Bpl.Token.NoToken, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)); - assignee.Add(exceptionAssignee); - List value= new List(); - value.Add(Bpl.Expr.Ident(this.sink.Heap.NullRef)); - Bpl.Cmd exceptionAssign= new Bpl.AssignCmd(Bpl.Token.NoToken, assignee, value); - stmtTraverser.StmtBuilder.Add(exceptionAssign); - } - #region Add assignments from In-Params to local-Params foreach (MethodParameter mparam in formalMap) { @@ -641,49 +568,12 @@ private bool IsStubMethod(IMethodDefinition methodDefinition, out IMethodDefinit } public override void TraverseChildren(IFieldDefinition 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 (PhoneCodeHelper.instance().PhonePlugin != null) { - trackControlVariableName(fieldDefinition, fieldVar); - trackNavigationVariableName(fieldDefinition, fieldVar); - } - } - - private static void trackNavigationVariableName(IFieldDefinition fieldDefinition, Bpl.Variable fieldVar) { - if (fieldDefinition.Name.Value.Equals(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE)) { - PhoneCodeHelper.instance().setBoogieNavigationVariable(fieldVar.Name); - } - } - - private static void trackControlVariableName(IFieldDefinition fieldDefinition, Bpl.Variable fieldVar) { - INamespaceTypeReference namedContainerRef = fieldDefinition.ContainingType as INamespaceTypeReference; - if (namedContainerRef != null) { - string containerName = namedContainerRef.ContainingUnitNamespace.Unit.Name.Value + "." + namedContainerRef.Name.Value; - IEnumerable controls = PhoneCodeHelper.instance().PhonePlugin.getControlsForPage(containerName); - if (controls != null) { - ControlInfoStructure ctrlInfo = controls.FirstOrDefault(ctrl => ctrl.Name == fieldDefinition.Name.Value); - if (ctrlInfo != null) - ctrlInfo.BplName = fieldVar.Name; - } - } + this.sink.FindOrCreateFieldVariable(fieldDefinition); } #endregion - private void addPhoneTopLevelDeclarations() { - if (PhoneCodeHelper.instance().PhoneNavigationToggled) { - Bpl.Variable continueOnPageVar = sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_CONTINUE_ON_PAGE_VARIABLE, Bpl.Type.Bool); - sink.TranslatedProgram.AddTopLevelDeclaration(continueOnPageVar); - Bpl.Variable navigationCheckVar = sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_NAVIGATION_CHECK_VARIABLE, Bpl.Type.Bool); - sink.TranslatedProgram.AddTopLevelDeclaration(navigationCheckVar); - } - } - #region Public API public virtual void TranslateAssemblies(IEnumerable assemblies) { - if (PhoneCodeHelper.instance().PhonePlugin != null) - addPhoneTopLevelDeclarations(); - foreach (var a in assemblies) { this.Traverse((IAssembly)a); } diff --git a/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs b/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs deleted file mode 100644 index a5ed9cf..0000000 --- a/BytecodeTranslator/Phone/PhoneBackKeyCallbackTraverser.cs +++ /dev/null @@ -1,174 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Cci; -using Microsoft.Cci.MutableCodeModel; - -namespace BytecodeTranslator.Phone { - class PhoneBackKeyCallbackTraverser : CodeTraverser { - private ITypeReference typeBeingTraversed; - private IMetadataHost host; - - public PhoneBackKeyCallbackTraverser(IMetadataHost host) { - this.host = host; - } - - public override void TraverseChildren(ITypeDefinition typeDef) { - typeBeingTraversed = typeDef; - base.TraverseChildren(typeDef); - } - - public override void TraverseChildren(IMethodCall methodCall) { - if (methodCall.MethodToCall.ResolvedMethod.IsSpecialName && methodCall.MethodToCall.Name.Value == "add_BackKeyPress") { - // check if it is a back key handler and if it is... - // NAVIGATION TODO this only catches really locally delegate expressions. If it is created before, we see it as a BoundExpression - // NAVIGATION TODO and need (again) data flow analysis - bool delegateIsIdentified= false; - bool delegateIsAnonymous = false; - PhoneCodeHelper.instance().OnBackKeyPressOverriden = true; - IBlockStatement delegateBody = null; - IMethodDefinition delegateMethodRef= null; - if (methodCall.Arguments.Count() == 1) { - IExpression delegateArg= methodCall.Arguments.First(); - ICreateDelegateInstance localDelegate = delegateArg as ICreateDelegateInstance; - if (localDelegate != null) { - delegateIsIdentified = true; - delegateMethodRef = localDelegate.MethodToCallViaDelegate.ResolvedMethod; - SourceMethodBody body= delegateMethodRef.Body as SourceMethodBody; - if (body != null) - delegateBody = body.Block; - - PhoneCodeHelper.instance().KnownBackKeyHandlers.Add(delegateMethodRef); - } - - AnonymousDelegate anonDelegate = delegateArg as AnonymousDelegate; - if (anonDelegate != null) { - delegateIsIdentified = true; - delegateIsAnonymous = true; - delegateBody = anonDelegate.Body; - } - - // NAVIGATION TODO what if it has no body? - if (delegateBody != null) { - bool navigates= false, cancelsNav= false; - ICollection navTargets; - parseBlockForNavigation(delegateBody, out navigates, out navTargets); - if (navigates) { - ICollection> targets = null; - if (!PhoneCodeHelper.instance().BackKeyNavigatingOffenders.TryGetValue(typeBeingTraversed, out targets)) { - targets = new HashSet>(); - } - - foreach (string tgt in navTargets) { - IMethodReference dummyRef=null; - if (delegateIsAnonymous) { - dummyRef = new Microsoft.Cci.MutableCodeModel.MethodReference(); - (dummyRef as Microsoft.Cci.MutableCodeModel.MethodReference).ContainingType= typeBeingTraversed; - (dummyRef as Microsoft.Cci.MutableCodeModel.MethodReference).Name = Dummy.Name; - } - targets.Add(Tuple.Create((delegateIsAnonymous ? dummyRef : delegateMethodRef), "\"" + tgt + "\"")); - } - - PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeBeingTraversed] = targets; - } - - parseBlockForEventCancellation(delegateBody, out cancelsNav); - if (cancelsNav) { - string reason= "(via delegate "; - if (delegateIsIdentified) - reason += delegateMethodRef.ContainingType.ToString() + "." + delegateMethodRef.Name.Value; - else - reason += "anonymous"; - reason += ")"; - PhoneCodeHelper.instance().BackKeyCancellingOffenders.Add(Tuple.Create(typeBeingTraversed, reason)); - } - } - } - - if (!delegateIsIdentified) { - PhoneCodeHelper.instance().BackKeyHandlerOverridenByUnknownDelegate = true; - PhoneCodeHelper.instance().BackKeyUnknownDelegateOffenders.Add(typeBeingTraversed); - } - } - base.TraverseChildren(methodCall); - } - - private void parseBlockForNavigation(IBlockStatement block, out bool navigates, out ICollection navTargets) { - PhoneNavigationCallsTraverser traverser = new PhoneNavigationCallsTraverser(host); - traverser.Traverse(block); - navigates = traverser.CodeDoesNavigation; - navTargets = traverser.NavigationTargets; - } - - private void parseBlockForEventCancellation(IBlockStatement block, out bool cancels) { - PhoneNavigationCallsTraverser traverser = new PhoneNavigationCallsTraverser(host); - traverser.Traverse(block); - cancels = traverser.CancelsEvents; - } - } - - public class PhoneNavigationCallsTraverser : CodeTraverser { - private IMetadataHost host; - - public bool CancelsEvents { get; private set; } - public bool CodeDoesNavigation { get; private set; } - public ICollection NavigationTargets { get; private set; } - public PhoneNavigationCallsTraverser(IMetadataHost host) { - CancelsEvents = CodeDoesNavigation = false; - NavigationTargets = new HashSet(); - this.host = host; - } - - public override void TraverseChildren(IMethodCall call) { - checkMethodCallForEventCancellation(call); - checkMethodCallForNavigation(call); - } - - private void checkMethodCallForEventCancellation(IMethodCall call) { - // NAVIGATION TODO this code is duplicated from PhoneNavigationTraverser, refactor that - if (!call.MethodToCall.Name.Value.StartsWith("set_Cancel")) - return; - - if (call.Arguments.Count() != 1 || call.Arguments.ToList()[0].Type != host.PlatformType.SystemBoolean) - return; - - ICompileTimeConstant constant = call.Arguments.ToList()[0] as ICompileTimeConstant; - if (constant != null && constant.Value != null) { - CompileTimeConstant falseConstant = new CompileTimeConstant() { - Type = host.PlatformType.SystemBoolean, - Value = false, - }; - if (constant.Value == falseConstant.Value) - return; - } - - CancelsEvents = true; - } - - private void checkMethodCallForNavigation(IMethodCall call) { - // NAVIGATION TODO this code is duplicated from PhoneNavigationTraverser, refactor that - string targetUri = null; - if (!call.MethodToCall.ContainingType.isNavigationServiceClass(host)) - return; - - if (!PhoneCodeHelper.NAV_CALLS.Contains(call.MethodToCall.Name.Value) || call.MethodToCall.Name.Value == "GoBack") // back is actually ok - return; - - if (call.MethodToCall.Name.Value == "Navigate") { - try { - IExpression expr = call.Arguments.First(); - bool isStatic = UriHelper.isArgumentURILocallyCreatedStatic(expr, host, out targetUri) || - UriHelper.isArgumentURILocallyCreatedStaticRoot(expr, host, out targetUri); - if (!isStatic) - targetUri = "--Other non inferrable target--"; - else - targetUri = UriHelper.getURIBase(targetUri); - } catch (InvalidOperationException) { - } - } - CodeDoesNavigation= true; - NavigationTargets.Add(targetUri); - } - } -} diff --git a/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BytecodeTranslator/Phone/PhoneCodeHelper.cs deleted file mode 100644 index 95cc573..0000000 --- a/BytecodeTranslator/Phone/PhoneCodeHelper.cs +++ /dev/null @@ -1,865 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Cci; -using Bpl=Microsoft.Boogie; -using TranslationPlugins; -using Microsoft.Cci.MutableCodeModel; -using System.IO; -using ILGarbageCollect; - -namespace BytecodeTranslator.Phone { - public static class UriHelper { - /// - /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values) - /// This method returns a base URI - /// - /// - /// - 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); - /* - Uri relativeUri = mockBaseUri.MakeRelativeUri(mockStrippedUri); - return relativeUri.ToString(); - */ - // TODO PATCH this works for now because we are ignoring non-flat XAML structures - return mockStrippedUri.Segments.Last(); - } - - /// - /// checks if argument is locally created URI with static URI target - /// - /// - /// - public static bool isArgumentURILocallyCreatedStatic(IExpression arg, IMetadataHost host, out string uri) { - uri = null; - ICreateObjectInstance creationSite = arg as ICreateObjectInstance; - if (creationSite == null) - return false; - - if (!arg.Type.isURIClass(host)) - return false; - - IExpression uriTargetArg = creationSite.Arguments.First(); - - if (!uriTargetArg.Type.isStringClass(host)) - return false; - - ICompileTimeConstant staticURITarget = uriTargetArg as ICompileTimeConstant; - if (staticURITarget == null) - return false; - - uri= staticURITarget.Value as string; - return true; - } - - /// - /// checks if argument is locally created URI where target has statically created URI root - /// - /// - /// - public static bool isArgumentURILocallyCreatedStaticRoot(IExpression arg, IMetadataHost host, out string uri) { - // Pre: !isArgumentURILocallyCreatedStatic - uri = null; - ICreateObjectInstance creationSite = arg as ICreateObjectInstance; - if (creationSite == null) - return false; - - if (!arg.Type.isURIClass(host)) - return false; - - IExpression uriTargetArg = creationSite.Arguments.First(); - - if (!uriTargetArg.Type.isStringClass(host)) - return false; - - if (!uriTargetArg.IsStaticURIRootExtractable(out uri)) - return false; - - return true; - } - - - /// - /// checks whether a static URI root (a definite page base) can be extracted from the expression - /// - /// - /// - public static bool IsStaticURIRootExtractable(this IExpression expr, out string uri) { - // Pre expr.type == string - IMethodCall stringConcatExpr = expr as IMethodCall; - uri = null; - if (stringConcatExpr == null) - return false; - - if (stringConcatExpr.MethodToCall.Name.Value != "Concat") - return false; - - IList constantStrings = new List(); - - // TODO this misses so many "static" strings, but let's start with this for now - IExpression leftOp = stringConcatExpr.Arguments.FirstOrDefault(); - while (leftOp != null && leftOp is ICompileTimeConstant) { - ICompileTimeConstant strConst = leftOp as ICompileTimeConstant; - constantStrings.Add(strConst.Value as string); - if (stringConcatExpr.Arguments.ToList()[1] is IMethodCall) { - stringConcatExpr = stringConcatExpr.Arguments.ToList()[1] as IMethodCall; - leftOp = stringConcatExpr.Arguments.FirstOrDefault(); - } else if (stringConcatExpr.Arguments.ToList()[1] is ICompileTimeConstant) { - constantStrings.Add((stringConcatExpr.Arguments.ToList()[1] as ICompileTimeConstant).Value as string); - break; - } else { - break; - } - } - - if (constantStrings.Count > 0) { - uri = constantStrings.Aggregate((aggr, elem) => aggr + elem); - return Uri.IsWellFormedUriString(uri, UriKind.RelativeOrAbsolute); - } else { - return false; - } - } - } - - public static class PhoneTypeHelper { - public static IAssemblyReference getSystemAssemblyReference(IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - IAssemblyReference coreAssemblyRef = platform.CoreAssemblyRef; - AssemblyIdentity MSPhoneSystemAssemblyId = - new AssemblyIdentity(host.NameTable.GetNameFor("System"), coreAssemblyRef.Culture, coreAssemblyRef.Version, - coreAssemblyRef.PublicKeyToken, ""); - return host.FindAssembly(MSPhoneSystemAssemblyId); - } - - public static IAssemblyReference getCoreAssemblyReference(IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - return platform.CoreAssemblyRef; - } - - public static IAssemblyReference getSystemWindowsAssemblyReference(IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - IAssemblyReference coreAssemblyRef = platform.CoreAssemblyRef; - AssemblyIdentity MSPhoneSystemWindowsAssemblyId = - new AssemblyIdentity(host.NameTable.GetNameFor("System.Windows"), coreAssemblyRef.Culture, coreAssemblyRef.Version, - coreAssemblyRef.PublicKeyToken, ""); - return host.FindAssembly(MSPhoneSystemWindowsAssemblyId); - } - - public static IAssemblyReference getPhoneAssemblyReference(IMetadataHost host) { - 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 }, ""); - return host.FindAssembly(MSPhoneAssemblyId); - } - - public static bool isCancelEventArgsClass(this ITypeReference typeRef, IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - IAssemblyReference systemAssembly = getSystemAssemblyReference(host); - ITypeReference cancelEventArgsClass = platform.CreateReference(systemAssembly, "System", "ComponentModel", "CancelEventArgs"); - return typeRef.isClass(cancelEventArgsClass); - } - - public static bool isPhoneApplicationClass(this ITypeReference typeRef, IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - IAssemblyReference systemAssembly = PhoneTypeHelper.getSystemWindowsAssemblyReference(host); - ITypeReference applicationClass = platform.CreateReference(systemAssembly, "System", "Windows", "Application"); - return typeRef.isClass(applicationClass); - } - - public static bool isPhoneApplicationPageClass(this ITypeReference typeRef, IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - IAssemblyReference phoneAssembly = PhoneTypeHelper.getPhoneAssemblyReference(host); - ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Controls", "PhoneApplicationPage"); - - return typeRef.isClass(phoneApplicationPageTypeRef); - } - - public static bool isClass(this ITypeReference typeRef, ITypeReference targetTypeRef) { - while (typeRef != null) { - if (typeRef.ResolvedType.Equals(targetTypeRef.ResolvedType)) - return true; - - typeRef = typeRef.ResolvedType.BaseClasses.FirstOrDefault(); - } - - return false; - } - - 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, IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platformType = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - if (platformType == null) - return false; - - IAssemblyReference coreRef = platformType.CoreAssemblyRef; - AssemblyIdentity systemAssemblyId = new AssemblyIdentity(host.NameTable.GetNameFor("System"), "", coreRef.Version, coreRef.PublicKeyToken, ""); - IAssemblyReference systemAssembly = host.FindAssembly(systemAssemblyId); - - ITypeReference uriTypeRef = platformType.CreateReference(systemAssembly, "System", "Uri"); - 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; - IAssemblyReference phoneAssembly = getPhoneAssemblyReference(host); - ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "System", "Windows", "Navigation", "NavigationService"); - - return typeRef.isClass(phoneApplicationPageTypeRef); - } - - public static bool isRoutedEventHandlerClass(this ITypeReference typeRef, IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; ; - IAssemblyReference systemAssembly = getSystemWindowsAssemblyReference(host); - ITypeReference routedEvHandlerType = platform.CreateReference(systemAssembly, "System", "Windows", "RoutedEventHandler"); - return typeRef.isClass(routedEvHandlerType); - - } - - public static bool isMessageBoxClass(this ITypeReference typeRef, IMetadataHost host) { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; ; - IAssemblyReference systemAssembly = getSystemWindowsAssemblyReference(host); - ITypeReference mbType = platform.CreateReference(systemAssembly, "System", "Windows", "MessageBox"); - return typeRef.isClass(mbType); - } - - } - - public enum StaticURIMode { - NOT_STATIC, STATIC_URI_CREATION_ONSITE, STATIC_URI_ROOT_CREATION_ONSITE, - } - - public class PhoneCodeHelper { - // TODO refactor into Feedbakc and Navigation specific code, this is already a mess - private const string IL_BOOGIE_VAR_PREFIX = "@__BOOGIE_"; - 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"; - - public static readonly string[] NAV_CALLS = { /*"GoBack", "GoForward", "Navigate", "StopLoading"*/ "Navigate", "GoBack" }; - - public bool OnBackKeyPressOverriden { get; set; } - public bool BackKeyPressHandlerCancels { get { return BackKeyCancellingOffenders.Count > 0; } } - public bool BackKeyPressNavigates { get { return BackKeyNavigatingOffenders.Keys.Count > 0; } } - public bool BackKeyHandlerOverridenByUnknownDelegate { get; set; } - public ICollection> BackKeyCancellingOffenders { get; set; } - public ICollection BackKeyUnknownDelegateOffenders { get; set; } - public Dictionary>> BackKeyNavigatingOffenders { get; set; } - public ICollection KnownBackKeyHandlers { get; set; } - public ICollection KnownNavigatingMethods { get; set; } - public ICollection KnownEventCancellingMethods { get; set; } - - private Dictionary PHONE_UI_CHANGER_METHODS; - - private static IMetadataHost host; - private Microsoft.Cci.Immutable.PlatformType platform; - private static PhoneCodeHelper _instance; - private static bool initialized= false; - - public static void initialize(IMetadataHost host) { - if (initialized) - return; - - PhoneCodeHelper.host = host; - initialized = true; - } - - public static PhoneCodeHelper instance() { - if (_instance == null) { - _instance = new PhoneCodeHelper(host); - } - - return _instance; - } - - private PhoneCodeHelper(IMetadataHost host) { - if (host != null) { - platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - initializeKnownUIChangers(); - - BackKeyCancellingOffenders= new HashSet>(); - BackKeyUnknownDelegateOffenders = new HashSet(); - BackKeyNavigatingOffenders = new Dictionary>>(); - KnownBackKeyHandlers = new HashSet(); - KnownNavigatingMethods = new HashSet(); - KnownEventCancellingMethods = new HashSet(); - } - } - - private void initializeKnownUIChangers() { - PHONE_UI_CHANGER_METHODS= new Dictionary(); - IAssemblyReference systemAssembly = PhoneTypeHelper.getSystemAssemblyReference(host); - IAssemblyReference systemWinAssembly = PhoneTypeHelper.getSystemWindowsAssemblyReference(host); - IAssemblyReference phoneAssembly = PhoneTypeHelper.getPhoneAssemblyReference(host); - - ITypeReference textBoxType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "TextBox"); - PHONE_UI_CHANGER_METHODS[textBoxType.ToString()] = - new string[] {"set_BaselineOffset", "set_CaretBrush", "set_FontSource", "set_HorizontalScrollBarVisibility", "set_IsReadOnly", "set_LineHeight", - "set_LineStackingStrategy", "set_MaxLength", "set_SelectedText", "set_SelectionBackground", "set_SelectionForeground", "set_SelectionLength", - "set_SelectionStart", "set_Text", "set_TextAlignment", "set_TextWrapping", "set_VerticalScrollBarVisibility", "set_Watermark", - }; - - ITypeReference textBlockType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "TextBlock"); - PHONE_UI_CHANGER_METHODS[textBlockType.ToString()] = - new string[] {"set_BaselineOffset", "set_FontFamily", "set_FontSize", "set_FontSource", "set_FontStretch", "set_FontStyle", "set_FontWeight", "set_Foreground", - "set_CharacterSpacing", "set_LineHeight", "set_LineStackingStrategy", "set_Padding", "set_Text", "set_TextAlignment", "set_TextDecorations", - "set_TextTrimming", "set_TextWrapping", - }; - - ITypeReference uiElementType = platform.CreateReference(systemAssembly, "System", "Windows", "UIElement"); - PHONE_UI_CHANGER_METHODS[uiElementType.ToString()] = - new string[] {"set_Clip", "set_Opacity", "set_OpacityMask", "set_Projection", "set_RenderTransform", - "set_RenderTransformOrigin", "set_Visibility", "Arrange", "InvalidateArrange", "InvalidateMeasure", "SetValue", "ClearValue", // Set/ClearValue are quite unsafe - "UpdateLayout", "Measure", - }; - - ITypeReference frameworkElementType = platform.CreateReference(systemAssembly, "System", "Windows", "FrameworkElement"); - PHONE_UI_CHANGER_METHODS[frameworkElementType.ToString()] = - new string[] {"set_FlowDirection", "set_Height", "set_HorizontalAlignment", "set_Language", "set_Margin", "set_MaxHeight", "set_MaxWidth", - "set_MinHeight", "set_MinWidth", "set_Style", "set_VerticalAlignment", "set_Width", "set_Cursor", - }; - - ITypeReference borderType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Border"); - PHONE_UI_CHANGER_METHODS[borderType.ToString()] = - new string[] {"set_Background", "set_BorderBrush", "set_BorderThickness", "set_CornerRadius", "set_Padding", - }; - - ITypeReference controlType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Control"); - PHONE_UI_CHANGER_METHODS[controlType.ToString()] = - new string[] {"set_Background", "set_BorderBrush", "set_BorderThickness", "set_CharacterSpacing", "set_FontFamily", "set_FontSize", "set_FontStretch", - "set_FontStyle", "set_FontWeight", "set_Foreground", "set_HorizontalContentAlignment", "set_IsEnabled", "set_Padding", "set_VerticalContentAlignment", - }; - - ITypeReference contentControlType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "ContentControl"); - PHONE_UI_CHANGER_METHODS[contentControlType.ToString()] = new string[] { "set_Content", }; - - ITypeReference panelType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Panel"); - PHONE_UI_CHANGER_METHODS[panelType.ToString()] = new string[] { "set_Background", }; - - ITypeReference canvasType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Canvas"); - PHONE_UI_CHANGER_METHODS[canvasType.ToString()] = new string[] { "set_Left", "set_Top", "set_ZIndex", }; - - ITypeReference toggleButtonType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Primitives", "ToggleButton"); - PHONE_UI_CHANGER_METHODS[toggleButtonType.ToString()] = new string[] { "set_IsChecked", }; - - ITypeReference gridType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Grid"); - PHONE_UI_CHANGER_METHODS[gridType.ToString()] = new string[] { "set_ShowGridLines", "set_Column", "set_ColumnSpan", "set_Row", "set_RowSpan", }; - - ITypeReference imageType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Image"); - PHONE_UI_CHANGER_METHODS[imageType.ToString()] = new string[] { "set_Source", "set_Stretch", }; - - ITypeReference inkPresenterType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "InkPresenter"); - PHONE_UI_CHANGER_METHODS[inkPresenterType.ToString()] = new string[] { "set_Strokes", }; - - ITypeReference itemsControlType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "ItemsControl"); - PHONE_UI_CHANGER_METHODS[itemsControlType.ToString()] = new string[] { "set_DisplayMemberPath", "set_ItemsSource", "set_ItemTemplate", }; - - ITypeReference selectorType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Primitives", "Selector"); - PHONE_UI_CHANGER_METHODS[selectorType.ToString()] = - new string[] { "set_SelectedIndex", "set_SelectedItem", "set_SelectedValue", "set_SelectedValuePath", }; - - ITypeReference listBoxType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "ListBox"); - PHONE_UI_CHANGER_METHODS[listBoxType.ToString()] = new string[] { "set_ItemContainerStyle", }; - - ITypeReference passwordBoxType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "PasswordBox"); - PHONE_UI_CHANGER_METHODS[passwordBoxType.ToString()] = - new string[] { "set_CaretBrush", "set_FontSource", "set_MaxLength", "set_Password", "set_PasswordChar", - "set_SelectionBackground", "set_SelectionForeground", - }; - - ITypeReference rangeBaseType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Primitives", "RangeBase"); - PHONE_UI_CHANGER_METHODS[rangeBaseType.ToString()] = new string[] { "set_LargeChange", "set_Maximum", "set_Minimum", "set_SmallChange", "set_Value", }; - - ITypeReference progressBarType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "ProgressBar"); - PHONE_UI_CHANGER_METHODS[progressBarType.ToString()] = new string[] { "set_IsIndeterminate", }; - - ITypeReference sliderType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "Slider"); - PHONE_UI_CHANGER_METHODS[sliderType.ToString()] = new string[] { "set_IsDirectionReversed", "set_Orientation", }; - - ITypeReference stackPanelType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "StackPanel"); - PHONE_UI_CHANGER_METHODS[stackPanelType.ToString()] = new string[] { "set_Orientation", }; - - ITypeReference richTextBoxType = platform.CreateReference(systemAssembly, "System", "Windows", "Controls", "RichTextBox"); - PHONE_UI_CHANGER_METHODS[richTextBoxType.ToString()] = - new string[] { "set_BaselineOffset", "set_CaretBrush", "set_HorizontalScrollBartVisibility", "set_LineHeight", "set_LineStackingStrategy", - "set_TextAlignment", "set_TextWrapping", "set_VerticalScrollBarVisibility", "set_Xaml", }; - - ITypeReference webBrowserTaskType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Tasks", "WebBrowserTask"); - PHONE_UI_CHANGER_METHODS[webBrowserTaskType.ToString()] = new string[] { "Show", }; - - ITypeReference appBarIconButtonType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarIconButton"); - PHONE_UI_CHANGER_METHODS[appBarIconButtonType.ToString()] = new string[] { "set_IsEnabled", "set_IconUri", "set_Text", }; - - ITypeReference appBarMenuItemType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarMenuItem"); - PHONE_UI_CHANGER_METHODS[appBarMenuItemType.ToString()] = new string[] { "set_IsEnabled", "set_Text", }; - - ITypeReference emailComposeTaskType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Tasks", "EmailComposeTask"); - PHONE_UI_CHANGER_METHODS[emailComposeTaskType.ToString()] = new string[] { "Show", }; - - ITypeReference scaleTransformType = platform.CreateReference(systemWinAssembly, "System", "Windows", "Media", "ScaleTransform"); - PHONE_UI_CHANGER_METHODS[scaleTransformType.ToString()] = new string[] { "set_CenterX", "set_CenterY", "set_ScaleX", "set_ScaleY", }; - } - - // TODO externalize strings - public static readonly string[] IgnoredEvents = - { "Loaded", - }; - - // 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__"; - - public PhoneControlsPlugin PhonePlugin { get; set; } - private IDictionary boogieObjects = new Dictionary(); - - public Bpl.Variable getBoogieVariableForName(string varName) { - Bpl.Variable boogieVar = null; - try { - boogieVar = boogieObjects[varName] as Bpl.Variable; - } catch (KeyNotFoundException) { - } - - if (boogieVar == null) - throw new ArgumentException("The boogie variable " + varName + " is not defined."); - - return boogieVar; - } - - /// - /// - /// - /// - /// - /// true if defining a new name, false if replacing - public bool setBoogieObjectForName(string name, Bpl.NamedDeclaration bplObject) { - bool ret = true; - if (boogieObjects.ContainsKey(name)) - ret = false; - - boogieObjects[name] = bplObject; - return ret; - } - - private bool isPhoneUIChangerClass(ITypeReference typeRef) { - return PHONE_UI_CHANGER_METHODS.Keys.Contains(typeRef.ToString()); - } - - public bool isNavigationCall(IMethodCall call) { - ITypeReference callType = call.MethodToCall.ContainingType; - if (!callType.isNavigationServiceClass(host)) - return false; - - return NAV_CALLS.Contains(call.MethodToCall.Name.Value); - } - - private ITypeReference mainAppTypeRef; - public void setMainAppTypeReference(ITypeReference appType) { - mainAppTypeRef = appType; - } - - public ITypeReference getMainAppTypeReference() { - return mainAppTypeRef; - } - - public void setBoogieNavigationVariable(string var) { - PhonePlugin.setBoogieNavigationVariable(var); - } - - public string getBoogieNavigationVariable() { - return PhonePlugin.getBoogieNavigationVariable(); - } - - public string getXAMLForPage(string pageClass) { - return PhonePlugin.getXAMLForPage(pageClass); - } - - public void setBoogieStringPageNameForPageClass(string pageClass, string boogieStringName) { - PhonePlugin.setBoogieStringPageNameForPageClass(pageClass, boogieStringName); - } - - public void setMainAppTypeName(string fullyQualifiedName) { - PhonePlugin.setMainAppTypeName(fullyQualifiedName); - } - - public string getMainAppTypeName() { - return PhonePlugin.getMainAppTypeName(); - } - - public Bpl.AssignCmd createBoogieNavigationUpdateCmd(Sink sink) { - // the block is a potential page changer - List lhs = new List(); - List rhs = new List(); - 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); - return assignCmd; - } - - // TODO do away with these whenever it is possible to make repeated passes at the translator, and handle from Program - public bool PhoneNavigationToggled { get; set; } - public bool PhoneFeedbackToggled { get; set; } - - public bool isMethodInputHandlerOrFeedbackOverride(IMethodDefinition method) { - // FEEDBACK TODO: This is extremely coarse. There must be quite a few non-UI routed/non-routed events - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; ; - IAssemblyReference coreAssembly= PhoneTypeHelper.getCoreAssemblyReference(host); - ITypeReference eventArgsType= platform.CreateReference(coreAssembly, "System", "EventArgs"); - foreach (IParameterDefinition paramDef in method.Parameters) { - if (paramDef.Type.isClass(eventArgsType)) - return true; - } - - return false; - } - - public bool isMethodKnownUIChanger(IMethodCall methodCall) { - // FEEDBACK TODO join these two with the others - if (methodCall.MethodToCall.ContainingType.isNavigationServiceClass(host)) { - return NAV_CALLS.Contains(methodCall.MethodToCall.Name.Value); - } else if (methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.isMessageBoxClass(host) && - methodCall.MethodToCall.Name.Value == "Show") { - return true; - } - - // otherwise, it must be a control input call - // before any method call checks, make sure the receiving object is a Control - IExpression callee = methodCall.ThisArgument; - if (callee == null) - return false; - - ITypeReference calleeType = callee.Type; - while (calleeType.ResolvedType.BaseClasses.Any()) { - if (isPhoneUIChangerClass(calleeType) && isKnownUIChanger(calleeType, methodCall)) { - return true; - } - - calleeType = calleeType.ResolvedType.BaseClasses.First(); - } - - return false; - } - - private bool isKnownUIChanger(ITypeReference typeRef, IMethodCall call) { - string methodName= call.MethodToCall.Name.Value; - IEnumerable methodsForType = PHONE_UI_CHANGER_METHODS[typeRef.ToString()]; - return methodsForType != null && methodsForType.Contains(methodName); - } - - private HashSet ignoredHandlers = new HashSet(); - public void ignoreEventHandler(string fullyQualifiedEventHandler) { - ignoredHandlers.Add(fullyQualifiedEventHandler); - } - - public bool isMethodIgnoredForFeedback(IMethodDefinition methodTranslated) { - INamespaceTypeDefinition type= methodTranslated.ContainingType.ResolvedType as INamespaceTypeDefinition; - - if (type == null) - return false; - - string methodName = type.ContainingUnitNamespace.Name.Value + "." + type.Name + "." + methodTranslated.Name.Value; - return ignoredHandlers.Contains(methodName); - } - - private HashSet callableMethods = new HashSet(); - public void trackCallableMethod(Bpl.Procedure proc) { - callableMethods.Add(proc); - } - - public IEnumerable getCallableMethods() { - return callableMethods; - } - - public void CreateFeedbackCallingMethods(Sink sink) { - Bpl.Program translatedProgram= sink.TranslatedProgram; - foreach (Bpl.Procedure proc in callableMethods) { - addMethodCalling(proc, translatedProgram, sink); - } - } - - private void addMethodCalling(Bpl.Procedure proc, Bpl.Program program, Sink sink) { - Bpl.Procedure callingProc= new Bpl.Procedure(Bpl.Token.NoToken, "__BOOGIE_CALL_" + proc.Name, new List(), new List(), - new List(), new List(), new List(), new List()); - sink.TranslatedProgram.AddTopLevelDeclaration(callingProc); - - Bpl.StmtListBuilder codeBuilder = new Bpl.StmtListBuilder(); - List localVars = new List(proc.InParams); - List identVars= new List(); - - for (int i = 0; i < localVars.Count; i++) { - identVars.Add(new Bpl.IdentifierExpr(Bpl.Token.NoToken, localVars[i])); - } - codeBuilder.Add(new Bpl.HavocCmd(Bpl.Token.NoToken, identVars)); - - // FEEDBACK TODO this is possibly too much, I'm guessing sometimes this args might well be null - Bpl.Expr notNullExpr; - foreach (Bpl.IdentifierExpr idExpr in identVars) { - if (idExpr.Type.Equals(sink.Heap.RefType)) { - notNullExpr= Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, idExpr, Bpl.Expr.Ident(sink.Heap.NullRef)); - codeBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, notNullExpr)); - } - } - - List callParams = new List(); - for (int i = 0; i < identVars.Count; i++) { - callParams.Add(identVars[i]); - } - Bpl.CallCmd callCmd = new Bpl.CallCmd(Bpl.Token.NoToken, proc.Name, callParams, new List()); - codeBuilder.Add(callCmd); - Bpl.Implementation impl = new Bpl.Implementation(Bpl.Token.NoToken, callingProc.Name, new List(), new List(), - new List(), localVars, codeBuilder.Collect(Bpl.Token.NoToken)); - sink.TranslatedProgram.AddTopLevelDeclaration(impl); - } - - public bool isBackKeyPressOverride(IMethodDefinition method) { - if (!method.IsVirtual || method.Name.Value != "OnBackKeyPress" || !method.ContainingType.isPhoneApplicationPageClass(host) || - method.ParameterCount != 1 || !method.Parameters.ToList()[0].Type.isCancelEventArgsClass(host)) - return false; - else - return true; - } - - public bool mustInlineMethod(IMethodDefinition method) { - if (PhoneFeedbackToggled) { - // FEEDBACK TODO this may be too coarse - // top level inlined methods are feedback relevant ones. For now, this is basically everything that has EventArgs as parameters - if (isMethodInputHandlerOrFeedbackOverride(method)) - return true; - } - - if (PhoneNavigationToggled) { - // NAVIGATION TODO this may be too coarse - // for now, assume any method in a PhoneApplicationPage is potentially interesting to navigation inlining - ITypeReference methodContainer = method.ContainingType; - if (PhoneTypeHelper.isPhoneApplicationClass(methodContainer, host) || PhoneTypeHelper.isPhoneApplicationPageClass(methodContainer, host)) - return true; - } - - return false; - } - - public void createQueriesBatchFile(Sink sink, string sourceBPLFile) { - StreamWriter outputStream = new StreamWriter("createQueries.bat"); - IEnumerable xamls= PhonePlugin.getPageXAMLFilenames(); - string startURI= sink.FindOrCreateConstant(BOOGIE_STARTING_URI_PLACEHOLDER).Name; - string endURI = sink.FindOrCreateConstant(BOOGIE_ENDING_URI_PLACEHOLDER).Name; - foreach (string x1 in xamls) { - string startURIVar= sink.FindOrCreateConstant(x1).Name.ToLower(); - foreach (string x2 in xamls) { - string resultFile = sourceBPLFile + "_$$" + x1 + "$$_$$" + x2 + "$$.bpl"; - string endURIVar= sink.FindOrCreateConstant(x2).Name.ToLower(); - outputStream.WriteLine("sed s/" + startURI + ";/" + startURIVar + ";/g " + sourceBPLFile + "> " + resultFile); - outputStream.WriteLine("sed -i s/" + endURI + ";/" + endURIVar + ";/g " + resultFile); - } - } - - outputStream.Close(); - } - - - public Bpl.Procedure addHandlerStubCaller(Sink sink, IMethodDefinition def) { - MethodBody callerBody = new MethodBody(); - MethodDefinition callerDef = new MethodDefinition() { - InternFactory = (def as MethodDefinition).InternFactory, - ContainingTypeDefinition = def.ContainingTypeDefinition, - IsStatic = true, - Name = sink.host.NameTable.GetNameFor("BOOGIE_STUB_CALLER_" + def.Name.Value), - Type = sink.host.PlatformType.SystemVoid, - Body = callerBody, - }; - callerBody.MethodDefinition = callerDef; - Sink.ProcedureInfo procInfo = sink.FindOrCreateProcedure(def); - Sink.ProcedureInfo callerInfo = sink.FindOrCreateProcedure(callerDef); - - Bpl.LocalVariable[] localVars = new Bpl.LocalVariable[procInfo.Decl.InParams.Count]; - Bpl.IdentifierExpr[] varExpr = new Bpl.IdentifierExpr[procInfo.Decl.InParams.Count]; - for (int i = 0; i < procInfo.Decl.InParams.Count; i++) { - Bpl.LocalVariable loc = new Bpl.LocalVariable(Bpl.Token.NoToken, - new Bpl.TypedIdent(Bpl.Token.NoToken, TranslationHelper.GenerateTempVarName(), - procInfo.Decl.InParams[i].TypedIdent.Type)); - localVars[i] = loc; - varExpr[i] = new Bpl.IdentifierExpr(Bpl.Token.NoToken, loc); - } - - 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; - if (pageXaml != null) - boogieXamlConstant = sink.FindOrCreateConstant(pageXaml); - else - boogieXamlConstant = null; - // NAVIGATION TODO: For now just assume we are in this page to be able to call the handler, this is NOT true for any handler - // NAVIGATION TODO: ie, a network event handler - if (boogieXamlConstant != null) { - Bpl.AssumeCmd assumeCurrentPage = - new Bpl.AssumeCmd(Bpl.Token.NoToken, - Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieCurrentURI), - new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieXamlConstant))); - builder.Add(assumeCurrentPage); - } - - // NAVIGATION TODO: have to do the pair generation all in one go instead of having different files that need to be sed'ed - boogieXamlConstant = sink.FindOrCreateConstant(BOOGIE_STARTING_URI_PLACEHOLDER); - Bpl.AssumeCmd assumeStartPage = new Bpl.AssumeCmd(Bpl.Token.NoToken, - Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieCurrentURI), - new Bpl.IdentifierExpr(Bpl.Token.NoToken, boogieXamlConstant))); - builder.Add(assumeStartPage); - builder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, procInfo.Decl.Name, new List(varExpr), new List())); - boogieXamlConstant = sink.FindOrCreateConstant(BOOGIE_ENDING_URI_PLACEHOLDER); - 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))); - - 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 List(), new List(), - new List(), new List(localVars), builder.Collect(Bpl.Token.NoToken), null, new Bpl.Errors()); - - sink.TranslatedProgram.AddTopLevelDeclaration(impl); - return impl.Proc; - } - - public static void updateInlinedMethods(Sink sink, IEnumerable doInline) { - foreach (IMethodDefinition method in doInline) { - Sink.ProcedureInfo procInfo = sink.FindOrCreateProcedure(method); - procInfo.Decl.AddAttribute("inline", new Bpl.LiteralExpr(Bpl.Token.NoToken, Microsoft.Basetypes.BigNum.ONE)); - } - } - - public static FieldDefinition CurrentURIFieldDefinition {get; set;} - - 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, - new List(new List(new Bpl.IdentifierExpr[] { - new Bpl.IdentifierExpr(Bpl.Token.NoToken, sink.FindOrCreateFieldVariable(PhoneCodeHelper.CurrentURIFieldDefinition))}))); - builder.Add(havoc); - Bpl.Implementation impl = new Bpl.Implementation(Bpl.Token.NoToken, procInfo.Decl.Name, new List(), - new List(), new List(), new List(), - builder.Collect(Bpl.Token.NoToken)); - sink.TranslatedProgram.AddTopLevelDeclaration(impl); - - } - - private IMethodReference uriHavocMethod=null; - public IMethodReference getUriHavocerMethod(Sink sink) { - if (uriHavocMethod == null) { - MethodBody body = new MethodBody(); - MethodDefinition havocDef = new MethodDefinition() { - InternFactory = host.InternFactory, - ContainingTypeDefinition = PhoneCodeHelper.instance().getMainAppTypeReference().ResolvedType, - IsStatic = true, - Name = sink.host.NameTable.GetNameFor(PhoneCodeHelper.BOOGIE_DO_HAVOC_CURRENTURI), - Type = sink.host.PlatformType.SystemVoid, - Body = body, - }; - body.MethodDefinition = havocDef; - uriHavocMethod = havocDef; - } - - 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 lhs = new List(); - List rhs = new List(); - 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; - } - - public bool isKnownBackKeyOverride(IMethodReference method) { - return isBackKeyPressOverride(method.ResolvedMethod) || - KnownBackKeyHandlers.Contains(method); - } - - internal IEnumerable getIndirectNavigators(IEnumerable modules, IMethodReference method) { - IEnumerable reachable = getReachableMethodsFromMethod(method, modules); - reachable= reachable.Except(new IMethodDefinition[] { method.ResolvedMethod }); - return getResolvedMethods(KnownNavigatingMethods).Intersect(reachable); - } - - internal IEnumerable getIndirectCancellations(IEnumerable modules, IMethodReference method) { - IEnumerable reachable = getReachableMethodsFromMethod(method, modules); - reachable = reachable.Except(new IMethodDefinition[] { method.ResolvedMethod }); - return getResolvedMethods(KnownEventCancellingMethods).Intersect(reachable); - } - - internal IEnumerable getReachableMethodsFromMethod(IMethodReference method, IEnumerable modules) { - IEnumerable assemblies = getAssembliesFromModules(modules); - Microsoft.Cci.MetadataReaderHost readerHost = host as Microsoft.Cci.MetadataReaderHost; - - if (readerHost == null) - return new List(); //? - - ILGarbageCollect.Mark.WholeProgram program = new ILGarbageCollect.Mark.WholeProgram(assemblies, readerHost); - RapidTypeAnalysis analyzer = new RapidTypeAnalysis(program, TargetProfile.Phone); - analyzer.Run(new IMethodReference[] { method }); - return analyzer.ReachableMethods(); - } - - internal IEnumerable getAssembliesFromModules(IEnumerable modules) { - IList assemblies = new List(); - foreach (IModule module in modules) { - IAssembly assembly = module as IAssembly; - if (assembly != null) - assemblies.Add(assembly); - } - - return assemblies; - } - - internal IEnumerable getResolvedMethods(IEnumerable methRefs) { - IList methDefs = new List(); - foreach (IMethodReference methRef in methRefs) { - methDefs.Add(methRef.ResolvedMethod); - } - - return methDefs; - } - } -} diff --git a/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs b/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs deleted file mode 100644 index 0ed9270..0000000 --- a/BytecodeTranslator/Phone/PhoneControlFeedbackTraverser.cs +++ /dev/null @@ -1,64 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Cci; -using Microsoft.Cci.MutableCodeModel; - -namespace BytecodeTranslator.Phone { - class PhoneControlFeedbackCodeTraverser : CodeTraverser { - private IMetadataReaderHost host; - - public PhoneControlFeedbackCodeTraverser(IMetadataReaderHost host) : base() { - this.host = host; - } - - public override void TraverseChildren(IMethodCall methodCall) { - if (PhoneCodeHelper.instance().PhoneFeedbackToggled) { - // check for handlers we do not wish to add feedback checks to - if (methodCall.MethodToCall.Name.Value.StartsWith("add_")) { - string eventName = methodCall.MethodToCall.Name.Value.Remove(0, "add_".Length); - if (PhoneCodeHelper.IgnoredEvents.Contains(eventName)) { - IMethodReference eventHandler = null; - foreach (IExpression arg in methodCall.Arguments) { - ICreateDelegateInstance createDelegate = arg as ICreateDelegateInstance; - if (createDelegate == null) - continue; - - ITypeReference typeRef = createDelegate.Type; - if (!typeRef.isRoutedEventHandlerClass(host)) - continue; - - eventHandler = createDelegate.MethodToCallViaDelegate; - break; - } - - if (eventHandler != null) { - INamespaceTypeReference namedType = eventHandler.ContainingType.ResolvedType as INamespaceTypeReference; - if (namedType != null) { - INamespaceTypeDefinition namedTypeDef = namedType.ResolvedType; - if (namedTypeDef != null) { - PhoneCodeHelper.instance().ignoreEventHandler(namedTypeDef.ContainingUnitNamespace.Name + "." + namedTypeDef.Name + "." + eventHandler.Name); - } - } - } - } - } - } - } - - } - - class PhoneControlFeedbackMetadataTraverser : MetadataTraverser { - private IMetadataReaderHost host; - - public PhoneControlFeedbackMetadataTraverser(IMetadataReaderHost host) : base() { - this.host = host; - } - - public override void TraverseChildren(IMethodDefinition method) { - PhoneControlFeedbackCodeTraverser codeTraverser = new PhoneControlFeedbackCodeTraverser(host); - codeTraverser.TraverseChildren(method); - } - } -} diff --git a/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs deleted file mode 100644 index db1aac4..0000000 --- a/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs +++ /dev/null @@ -1,377 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; - -using Microsoft.Cci; -using Microsoft.Cci.MetadataReader; -using Microsoft.Cci.MutableCodeModel; -using Microsoft.Cci.Contracts; - -using Bpl = Microsoft.Boogie; -using System.Diagnostics.Contracts; -using TranslationPlugins; - - -namespace BytecodeTranslator.Phone { - - /// - /// Traverse code looking for phone specific points of interest, possibly injecting necessary code in-between - /// - public class PhoneInitializationCodeTraverser : CodeTraverser { - private readonly IMethodDefinition methodBeingTraversed; - private static bool initializationFound= false; - private MetadataReaderHost host; - - private IAssemblyReference coreAssemblyRef; - private IAssemblyReference phoneAssembly; - private IAssemblyReference phoneSystemWindowsAssembly; - private IAssemblyReference MSPhoneControlsAssembly; - private INamespaceTypeReference appBarIconButtonType; - private INamespaceTypeReference appBarMenuItemType; - private INamespaceTypeReference checkBoxType; - private INamespaceTypeReference radioButtonType; - private INamespaceTypeReference buttonType; - private INamespaceTypeReference buttonBaseType; - private INamespaceTypeReference toggleButtonType; - private INamespaceTypeReference controlType; - private INamespaceTypeReference uiElementType; - private INamespaceTypeReference pivotType; - private INamespaceTypeReference listBoxType; - - private CompileTimeConstant trueConstant; - private CompileTimeConstant falseConstant; - - private IMethodReference isEnabledSetter; - private IMethodReference isEnabledGetter; - private IMethodReference isCheckedSetter; - private IMethodReference isCheckedGetter; - private IMethodReference visibilitySetter; - private IMethodReference visibilityGetter; - private IMethodReference clickHandlerAdder; - private IMethodReference clickHandlerRemover; - private IMethodReference checkedHandlerAdder; - private IMethodReference checkedHandlerRemover; - private IMethodReference uncheckedHandlerAdder; - private IMethodReference uncheckedHandlerRemover; - - private ITypeReference getTypeForClassname(String classname) { - if (classname == "Button") { - return buttonType; - } else if (classname == "RadioButton") { - return radioButtonType; - } else if (classname == "CheckBox") { - return checkBoxType; - } else if (classname == "ApplicationBarIconButton") { - return appBarIconButtonType; - } else if (classname == "ApplicationBarMenuItem") { - return appBarMenuItemType; - } else if (classname == "Pivot") { - return pivotType; - } else if (classname == "ListBox") { - return listBoxType; - } else if (classname == "DummyType") { - // return Dummy.Type; - return host.PlatformType.SystemObject; - } else { - // TODO avoid throwing exceptions, just log - throw new NotImplementedException("Type " + classname + " is not being monitored yet for phone controls"); - } - } - - public PhoneInitializationCodeTraverser(MetadataReaderHost host, IMethodDefinition traversedMethod) : base() { - this.methodBeingTraversed = traversedMethod; - this.host = host; - InitializeTraverser(); - } - - private void InitializeTraverser() { - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - coreAssemblyRef = platform.CoreAssemblyRef; - - // TODO obtain version, culture and signature data dynamically - 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 BUG / XAML DEPENDENCE If a control is declared in XAML, it may be one from a library *not* linked! So, assemblies could be dummy here - - // TODO determine the needed types dynamically - if (phoneAssembly != Dummy.Assembly) { - appBarIconButtonType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarIconButton"); - appBarMenuItemType = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Shell", "ApplicationBarMenuItem"); - } else { - appBarIconButtonType = host.PlatformType.SystemObject; - appBarMenuItemType = host.PlatformType.SystemObject; - } - - if (phoneSystemWindowsAssembly != Dummy.Assembly) { - checkBoxType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "CheckBox"); - radioButtonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "RadioButton"); - buttonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Button"); - buttonBaseType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Primitives", "ButtonBase"); - toggleButtonType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Primitives", "ToggleButton"); - controlType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "Control"); - uiElementType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "UIElement"); - listBoxType = platform.CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Controls", "ListBox"); - } else { - checkBoxType = host.PlatformType.SystemObject; - radioButtonType = host.PlatformType.SystemObject; - buttonType = host.PlatformType.SystemObject; - buttonBaseType = host.PlatformType.SystemObject; - toggleButtonType = host.PlatformType.SystemObject; - controlType = host.PlatformType.SystemObject; - uiElementType = host.PlatformType.SystemObject; - listBoxType = host.PlatformType.SystemObject; - } - - if (MSPhoneControlsAssembly != Dummy.Assembly) { - pivotType = platform.CreateReference(MSPhoneControlsAssembly, "Microsoft", "Phone", "Controls", "Pivot"); - } else { - pivotType = host.PlatformType.SystemObject; - } - - - - trueConstant = new CompileTimeConstant() { - Type = platform.SystemBoolean, - Value = true - }; - falseConstant = new CompileTimeConstant() { - Type = platform.SystemBoolean, - Value = false - }; - - IEnumerable controlProperties = controlType.ResolvedType.Properties; - IEnumerable toggleButtonProperties = toggleButtonType.ResolvedType.Properties; - IEnumerable uiElementProperties = uiElementType.ResolvedType.Properties; - - IPropertyDefinition prop = controlProperties.Single(p => p.Name.Value == "IsEnabled"); - isEnabledSetter = prop.Setter; - isEnabledGetter = prop.Getter; - prop = toggleButtonProperties.Single(p => p.Name.Value == "IsChecked"); - isCheckedSetter = prop.Setter; - isCheckedGetter = prop.Getter; - prop = uiElementProperties.Single(p => p.Name.Value == "Visibility"); - visibilitySetter = prop.Setter; - visibilityGetter = prop.Getter; - - IEnumerable buttonBaseEvents = buttonBaseType.ResolvedType.Events; - IEnumerable toggleButtonEvents = toggleButtonType.ResolvedType.Events; - IEventDefinition evt = buttonBaseEvents.Single(e => e.Name.Value == "Click"); - clickHandlerAdder = evt.Adder; - clickHandlerRemover = evt.Remover; - evt = toggleButtonEvents.Single(e => e.Name.Value == "Checked"); - checkedHandlerAdder = evt.Adder; - checkedHandlerRemover = evt.Remover; - evt = toggleButtonEvents.Single(e => e.Name.Value == "Unchecked"); - uncheckedHandlerAdder = evt.Adder; - uncheckedHandlerRemover = evt.Remover; - } - - public void injectPhoneControlsCode(BlockStatement block) { - this.Traverse(block); - } - - private void injectPhoneInitializationCode(BlockStatement block, Statement statementAfter) { - // TODO check page name against container name - IEnumerable controls = PhoneCodeHelper.instance().PhonePlugin.getControlsForPage(methodBeingTraversed.Container.ToString()); - IEnumerable injectedStatements = new List(); - if (controls != null) { - foreach (ControlInfoStructure controlInfo in controls) { - injectedStatements = injectedStatements.Concat(getCodeForSettingEnabledness(controlInfo)); - injectedStatements = injectedStatements.Concat(getCodeForSettingCheckedState(controlInfo)); - injectedStatements = injectedStatements.Concat(getCodeForSettingVisibility(controlInfo)); - } - - int stmtPos = block.Statements.IndexOf(statementAfter); - block.Statements.InsertRange(stmtPos + 1, injectedStatements); - } - } - - private BoundExpression makeBoundControlFromControlInfo(ControlInfoStructure controlInfo) { - return new BoundExpression() { - Definition = new FieldDefinition() { - ContainingTypeDefinition = methodBeingTraversed.Container, - Name = host.NameTable.GetNameFor(controlInfo.Name), - Type = getTypeForClassname(controlInfo.ClassName), - IsStatic = false, - }, - Instance = new ThisReference() { Type = methodBeingTraversed.Container }, - Type=getTypeForClassname(controlInfo.ClassName), - }; - } - - private IEnumerable getCodeForSettingVisibility(ControlInfoStructure controlInfo) { - // TODO I do not want to import System.Windows into this project...and using the underlying uint won't work for dependency properties - /* - IList code = new List(); - BoundExpression boundControl = makeBoundControlFromControlInfo(controlInfo); - MethodCall setVisibilityCall= new MethodCall() { - IsStaticCall = false, - IsVirtualCall = true, - IsTailCall = false, - Type = ((Microsoft.Cci.Immutable.PlatformType) host.PlatformType).SystemVoid, - MethodToCall = visibilitySetter, - ThisArgument = boundControl, - }; - - ITypeReference visibilityType= ((Microsoft.Cci.Immutable.PlatformType) host.PlatformType).CreateReference(phoneSystemWindowsAssembly, "System", "Windows", "Visibility"); - - switch (controlInfo.Visible) { - case Visibility.Visible: - setVisibilityCall.Arguments.Add(new CompileTimeConstant() { - Type = visibilityType, - Value = 0, - } ); // Visible - break; - case Visibility.Collapsed: - setVisibilityCall.Arguments.Add(new CompileTimeConstant() { - Type = visibilityType, - Value = 1, - } ); // Collapsed - break; - default: - throw new ArgumentException("Invalid visibility value for control " + controlInfo.Name + ": " + controlInfo.Visible); - } - - ExpressionStatement callStmt = new ExpressionStatement() { - Expression = setVisibilityCall, - }; - code.Add(callStmt); - return code; - * */ - return new List(); - } - - private IEnumerable getCodeForSettingEnabledness(ControlInfoStructure controlInfo) { - IList code = new List(); - BoundExpression boundControl = makeBoundControlFromControlInfo(controlInfo); - MethodCall setEnablednessCall = new MethodCall() { - IsStaticCall = false, - IsVirtualCall = true, - IsTailCall = false, - Type = ((Microsoft.Cci.Immutable.PlatformType) host.PlatformType).SystemVoid, - MethodToCall = isEnabledSetter, - ThisArgument = boundControl, - }; - - setEnablednessCall.Arguments.Add(controlInfo.IsEnabled ? trueConstant : falseConstant); - ExpressionStatement callStmt = new ExpressionStatement() { - Expression = setEnablednessCall, - }; - code.Add(callStmt); - return code; - } - - private IEnumerable getCodeForSettingCheckedState(ControlInfoStructure controlInfo) { - // IList code = new List(); - // 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(); - } - - public override void TraverseChildren(IBlockStatement block) { - foreach (IStatement statement in block.Statements) { - this.Traverse(statement); - if (initializationFound) { - injectPhoneInitializationCode(block as BlockStatement, statement as Statement); - initializationFound = false; - break; - } - } - } - - public override void TraverseChildren(IMethodCall methodCall) { - if (methodCall.IsStaticCall || - !methodCall.MethodToCall.ContainingType.ResolvedType.Equals(methodBeingTraversed.Container) || - methodCall.MethodToCall.Name.Value != "InitializeComponent" || - methodCall.Arguments.Any()) - return; - - initializationFound= true; - } - } - - /// - /// Traverse metadata looking only for PhoneApplicationPage's constructors - /// - public class PhoneInitializationMetadataTraverser : MetadataTraverser { - private MetadataReaderHost host; - - public PhoneInitializationMetadataTraverser(MetadataReaderHost host) - : base() { - this.host = host; - } - - public override void TraverseChildren(IModule module) { - base.TraverseChildren(module); - } - - public override void TraverseChildren(IAssembly assembly) { - base.TraverseChildren(assembly); - } - - /// - /// Check if the type being defined is a PhoneApplicationPage, uninteresting otherwise - /// - /// - public override void TraverseChildren(ITypeDefinition typeDefinition) { - if (typeDefinition.isPhoneApplicationClass(host)) { - PhoneCodeHelper.instance().setMainAppTypeReference(typeDefinition); - } else if (typeDefinition.isPhoneApplicationPageClass(host)) { - base.TraverseChildren(typeDefinition); - } - } - - /// - /// Check if it is traversing a constructor. If so, place necessary code after InitializeComponent() call - /// - public override void TraverseChildren(IMethodDefinition method) { - if (!method.IsConstructor) - return; - - PhoneInitializationCodeTraverser codeTraverser = new PhoneInitializationCodeTraverser(host, method); - var methodBody = method.Body as SourceMethodBody; - if (methodBody == null) - return; - var block = methodBody.Block as BlockStatement; - codeTraverser.injectPhoneControlsCode(block); - } - - public void InjectPhoneCodeAssemblies(IEnumerable assemblies) { - foreach (var a in assemblies) { - this.Traverse((IAssembly)a); - } - } - } -} \ No newline at end of file diff --git a/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs b/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs deleted file mode 100644 index 1957c2f..0000000 --- a/BytecodeTranslator/Phone/PhoneMethodInliningTraverser.cs +++ /dev/null @@ -1,81 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Cci; - -namespace BytecodeTranslator.Phone { - public class PhoneMethodInliningMetadataTraverser : MetadataTraverser { - private HashSet methodsToInline; - private HashSet iterMethodsToInline; - private PhoneCodeHelper phoneHelper; - private bool firstPassDone = false; - private bool changedOnLastPass = false; - private IAssemblyReference assemblyBeingTranslated; - - public int TotalMethodsCount { get; private set; } - public int InlinedMethodsCount { get { return methodsToInline.Count(); } } - - public PhoneMethodInliningMetadataTraverser(PhoneCodeHelper phoneHelper) { - methodsToInline = new HashSet(); - iterMethodsToInline = new HashSet(); - this.phoneHelper = phoneHelper; - TotalMethodsCount = 0; - } - - public override void TraverseChildren(IAssembly assembly) { - foreach (IModule module in assembly.MemberModules) { - assemblyBeingTranslated = module.ContainingAssembly; - this.Traverse(module); - } - firstPassDone = true; - } - - public override void TraverseChildren(IMethodDefinition method) { - if (!firstPassDone) - TotalMethodsCount++; - - if (iterMethodsToInline.Contains(method) || (!firstPassDone && phoneHelper.mustInlineMethod(method))) { - PhoneMethodInliningCodeTraverser codeTraverser= new PhoneMethodInliningCodeTraverser(); - codeTraverser.TraverseChildren(method); - foreach (IMethodDefinition newMethodDef in codeTraverser.getMethodsFound()) { - bool isExtern = this.assemblyBeingTranslated != null && - !TypeHelper.GetDefiningUnitReference(newMethodDef.ContainingType).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity); - if (!methodsToInline.Contains(newMethodDef) && !isExtern) { - iterMethodsToInline.Add(newMethodDef); - changedOnLastPass = true; - } - } - methodsToInline.Add(method); - iterMethodsToInline.Remove(method); - } - } - - public IEnumerable getMethodsToInline() { - return methodsToInline; - } - - public bool isFinished() { - return firstPassDone && !changedOnLastPass; - } - - public void findAllMethodsToInline(List modules) { - while (!isFinished()) { - changedOnLastPass = false; - this.Traverse(modules); - } - } - } - - class PhoneMethodInliningCodeTraverser : CodeTraverser { - private HashSet foundMethods = new HashSet(); - - public override void TraverseChildren(IMethodCall methodCall) { - foundMethods.Add(methodCall.MethodToCall.ResolvedMethod); - } - - public IEnumerable getMethodsFound() { - return foundMethods; - } - } -} diff --git a/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs deleted file mode 100644 index 0fa4a88..0000000 --- a/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs +++ /dev/null @@ -1,375 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Cci; -using Microsoft.Cci.MutableCodeModel; -using TranslationPlugins; - -namespace BytecodeTranslator.Phone { - public class PhoneNavigationCodeTraverser : CodeTraverser { - private MetadataReaderHost host; - private ITypeReference navigationSvcType; - private ITypeReference cancelEventArgsType; - private ITypeReference typeTraversed; - private IMethodDefinition methodTraversed; - private static HashSet navCallers= new HashSet(); - public static IEnumerable NavCallers { get { return navCallers; } } - - private HashSet navigationCallers; - public IEnumerable NavigationCallers { get { return NavigationCallers; } } - - public PhoneNavigationCodeTraverser(MetadataReaderHost host, IEnumerable assemblies) : base() { - this.host = host; - List assembliesTraversed = new List(); - foreach (IAssemblyReference asmRef in assemblies) { - assembliesTraversed.Add(asmRef.ResolvedAssembly); - } - - Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType; - - // TODO obtain version, culture and signature data dynamically - IAssemblyReference assembly= PhoneTypeHelper.getPhoneAssemblyReference(host); - // TODO determine the needed types dynamically - navigationSvcType = platform.CreateReference(assembly, "System", "Windows", "Navigation", "NavigationService"); - - assembly = PhoneTypeHelper.getSystemAssemblyReference(host); - cancelEventArgsType = platform.CreateReference(assembly, "System", "ComponentModel", "CancelEventArgs"); - navigationCallers = new HashSet(); - } - - public override void TraverseChildren(ITypeDefinition typeDef) { - this.typeTraversed = typeDef; - base.TraverseChildren(typeDef); - } - - public override void TraverseChildren(IMethodDefinition method) { - this.methodTraversed = method; - if (method.IsConstructor && PhoneTypeHelper.isPhoneApplicationClass(typeTraversed, host)) { - navigationCallers.Add(method); - string mainPageUri = PhoneCodeHelper.instance().PhonePlugin.getMainPageXAML(); - SourceMethodBody sourceBody = method.Body as SourceMethodBody; - if (sourceBody != null) { - BlockStatement bodyBlock = sourceBody.Block as BlockStatement; - if (bodyBlock != null) { - Assignment uriInitAssign = new Assignment() { - Source = new CompileTimeConstant() { - Type = host.PlatformType.SystemString, - Value = UriHelper.getURIBase(mainPageUri), - }, - Type = host.PlatformType.SystemString, - Target = new TargetExpression() { - Type = host.PlatformType.SystemString, - // TODO unify code for current uri fieldreference - Definition = new FieldReference() { - ContainingType = PhoneCodeHelper.instance().getMainAppTypeReference(), - IsStatic=true, - Type=host.PlatformType.SystemString, - Name=host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE), - InternFactory= host.InternFactory, - }, - }, - }; - Statement uriInitStmt= new ExpressionStatement() { - Expression= uriInitAssign, - }; - bodyBlock.Statements.Insert(0, uriInitStmt); - } - } - } - base.TraverseChildren(method); - } - - - private bool navCallFound=false; - private bool navCallIsStatic = false; - private bool navCallIsBack = false; - private StaticURIMode currentStaticMode= StaticURIMode.NOT_STATIC; - private string unpurifiedFoundURI=""; - - public override void TraverseChildren(IBlockStatement block) { - IList> staticNavStmts = new List>(); - IList nonStaticNavStmts = new List(); - foreach (IStatement statement in block.Statements) { - navCallFound = false; - navCallIsStatic = false; - navCallIsBack = false; - this.Traverse(statement); - if (navCallFound) { - navCallers.Add(methodTraversed); - if (navCallIsStatic) { - staticNavStmts.Add(new Tuple(statement, currentStaticMode, unpurifiedFoundURI)); - } else if (!navCallIsBack) { - nonStaticNavStmts.Add(statement); - } - } - } - - injectNavigationUpdateCode(block, staticNavStmts, nonStaticNavStmts); - } - - private bool isNavigationOnBackKeyPressHandler(IMethodCall call, out string target) { - target = null; - if (!PhoneCodeHelper.instance().isBackKeyPressOverride(methodTraversed.ResolvedMethod)) - return false; - - if (!call.MethodToCall.ContainingType.isNavigationServiceClass(host)) - return false; - - if (!PhoneCodeHelper.NAV_CALLS.Contains(call.MethodToCall.Name.Value) || call.MethodToCall.Name.Value == "GoBack") // back is actually ok - return false; - - if (call.MethodToCall.Name.Value == "Navigate") { - try { - IExpression expr = call.Arguments.First(); - bool isStatic = UriHelper.isArgumentURILocallyCreatedStatic(expr, host, out target) || - UriHelper.isArgumentURILocallyCreatedStaticRoot(expr, host, out target); - if (!isStatic) - target = "--Other non inferrable target--"; - else - target = UriHelper.getURIBase(target); - } catch (InvalidOperationException) { - } - } - - return true; - } - - private bool isCancelOnBackKeyPressHandler(IMethodCall call) { - if (!PhoneCodeHelper.instance().isBackKeyPressOverride(methodTraversed.ResolvedMethod)) - return false; - - return isEventCancellationMethodCall(call); - } - - private bool isEventCancellationMethodCall(IMethodCall call) { - if (!call.MethodToCall.Name.Value.StartsWith("set_Cancel")) - return false; - - if (call.Arguments.Count() != 1 || call.Arguments.ToList()[0].Type != host.PlatformType.SystemBoolean) - return false; - - if (call.ThisArgument == null || !call.ThisArgument.Type.isCancelEventArgsClass(host)) - return false; - - ICompileTimeConstant constant = call.Arguments.ToList()[0] as ICompileTimeConstant; - if (constant != null && constant.Value != null) { - CompileTimeConstant falseConstant = new CompileTimeConstant() { - Type = host.PlatformType.SystemBoolean, - Value = false, - }; - if (constant.Value == falseConstant.Value) - return false; - } - - return true; - } - - public override void TraverseChildren(IMethodCall methodCall) { - string target; - if (isNavigationOnBackKeyPressHandler(methodCall, out target)) { - ICollection> targets; - try { - targets= PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed]; - } catch (KeyNotFoundException) { - targets = new HashSet>(); - } - targets.Add(Tuple.Create(methodTraversed, "\"" + target + "\"")); - PhoneCodeHelper.instance().BackKeyNavigatingOffenders[typeTraversed]= targets; - } else if (isCancelOnBackKeyPressHandler(methodCall)) { - PhoneCodeHelper.instance().BackKeyCancellingOffenders.Add(Tuple.Create(typeTraversed,"")); - } - - // re-check whether it is an event cancellation call - if (isEventCancellationMethodCall(methodCall)) { - PhoneCodeHelper.instance().KnownEventCancellingMethods.Add(methodTraversed); - } - - // check whether it is a NavigationService call - IMethodReference methodToCall= methodCall.MethodToCall; - ITypeReference callType= methodToCall.ContainingType; - if (!callType.ResolvedType.Equals(navigationSvcType.ResolvedType)) - return; - - string methodToCallName= methodToCall.Name.Value; - if (!PhoneCodeHelper.NAV_CALLS.Contains(methodToCallName)) - return; - - navCallFound = true; - // TODO check what to do with these - if (methodToCallName == "GoForward" || methodToCallName == "StopLoading") { - // TODO forward navigation is not supported by the phone - // TODO StopLoading is very async, I don't think we may verify this behaviour - // TODO possibly log - return; - } else { - currentStaticMode = StaticURIMode.NOT_STATIC; - if (methodToCallName == "GoBack") { - navCallIsStatic = false; - navCallIsBack = true; - } else { // Navigate() - navCallIsBack = false; - - // check for different static patterns that we may be able to verify - IExpression uriArg = methodCall.Arguments.First(); - if (UriHelper.isArgumentURILocallyCreatedStatic(uriArg, host, out unpurifiedFoundURI)) { - navCallIsStatic = true; - currentStaticMode = StaticURIMode.STATIC_URI_CREATION_ONSITE; - } else if (UriHelper.isArgumentURILocallyCreatedStaticRoot(uriArg, host, out unpurifiedFoundURI)) { - navCallIsStatic = true; - currentStaticMode = StaticURIMode.STATIC_URI_ROOT_CREATION_ONSITE; - } else { - // get reason - //ICreateObjectInstance creationSite = methodCall.Arguments.First() as ICreateObjectInstance; - //if (creationSite == null) - // notStaticReason = "URI not created at call site"; - //else - // notStaticReason = "URI not initialized as a static string"; - } - } - - if (navCallFound && !navCallIsBack) { - // check this method as a navigation method - PhoneCodeHelper.instance().KnownNavigatingMethods.Add(methodTraversed); - } - - //Console.Write("Page navigation event found. Target is static? " + (isStatic ? "YES" : "NO")); - //if (!isStatic) { - // Console.WriteLine(" -- Reason: " + notStaticReason); - //} else { - // Console.WriteLine(""); - //} - } - } - - private void injectNavigationUpdateCode(IBlockStatement block, IEnumerable> staticStmts, IEnumerable nonStaticStmts) { - // 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 (IStatement stmt in nonStaticStmts) { - int ndx = mutableBlock.Statements.ToList().IndexOf(stmt); - if (ndx == -1) { - // can't be - throw new IndexOutOfRangeException("Statement must exist in original block"); - } - - Assignment currentURIAssign = new Assignment() { - Source = new CompileTimeConstant() { - Type = host.PlatformType.SystemString, - Value = PhoneCodeHelper.BOOGIE_DO_HAVOC_CURRENTURI, - }, - Type = host.PlatformType.SystemString, - Target = new TargetExpression() { - Type = host.PlatformType.SystemString, - // TODO unify code for current uri fieldreference - Definition = new FieldReference() { - ContainingType = PhoneCodeHelper.instance().getMainAppTypeReference(), - IsStatic= true, - Type = host.PlatformType.SystemString, - Name = host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE), - InternFactory=host.InternFactory, - }, - }, - }; - Statement uriInitStmt = new ExpressionStatement() { - Expression = currentURIAssign, - }; - mutableBlock.Statements.Insert(ndx + 1, uriInitStmt); - } - - - foreach (Tuple entry in staticStmts) { - int ndx= mutableBlock.Statements.ToList().IndexOf(entry.Item1); - if (ndx == -1) { - // can't be - throw new IndexOutOfRangeException("Statement must exist in original block"); - } - - Assignment currentURIAssign = new Assignment() { - Source = new CompileTimeConstant() { - Type = host.PlatformType.SystemString, - Value = UriHelper.getURIBase(entry.Item3).ToLower(), - }, - Type = host.PlatformType.SystemString, - Target = new TargetExpression() { - Type = host.PlatformType.SystemString, - // TODO unify code for current uri fieldreference - Definition = new FieldReference() { - ContainingType = PhoneCodeHelper.instance().getMainAppTypeReference(), - IsStatic= true, - Type = host.PlatformType.SystemString, - Name = host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE), - InternFactory=host.InternFactory, - }, - }, - }; - Statement uriInitStmt = new ExpressionStatement() { - Expression = currentURIAssign, - }; - mutableBlock.Statements.Insert(ndx+1, uriInitStmt); - } - } - } - - /// - /// Traverse metadata looking only for PhoneApplicationPage's constructors - /// - public class PhoneNavigationMetadataTraverser : MetadataTraverser { - private MetadataReaderHost host; - private ITypeDefinition typeBeingTraversed; - private PhoneNavigationCodeTraverser codeTraverser; - - public PhoneNavigationMetadataTraverser(MetadataReaderHost host) - : base() { - this.host = host; - } - - public override void TraverseChildren(IModule module) { - codeTraverser = new PhoneNavigationCodeTraverser(host, module.AssemblyReferences); - base.Traverse(module.AssemblyReferences); - base.TraverseChildren(module); - } - - - // TODO can we avoid visiting every type? Are there only a few, identifiable, types that may perform navigation? - public override void TraverseChildren(ITypeDefinition typeDefinition) { - typeBeingTraversed = typeDefinition; - if (typeDefinition.isPhoneApplicationClass(host)) { - NamespaceTypeDefinition mutableTypeDef = typeDefinition as NamespaceTypeDefinition; - if (mutableTypeDef != null) { - // TODO unify code for current uri fieldreference - FieldDefinition fieldDef = new FieldDefinition() { - ContainingTypeDefinition= mutableTypeDef, - InternFactory= host.InternFactory, - IsStatic= true, - Name= host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE), - Type= host.PlatformType.SystemString, - Visibility= TypeMemberVisibility.Public, - }; - PhoneCodeHelper.CurrentURIFieldDefinition = fieldDef; - mutableTypeDef.Fields.Add(fieldDef); - } - } - - codeTraverser.Traverse(typeDefinition); - base.TraverseChildren(typeDefinition); - } - - // TODO same here. Are there specific methods (and ways to identfy those) that can perform navigation? - public override void TraverseChildren(IMethodDefinition method) { - if (PhoneCodeHelper.instance().isBackKeyPressOverride(method)) { - PhoneCodeHelper.instance().KnownBackKeyHandlers.Add(method); - PhoneCodeHelper.instance().OnBackKeyPressOverriden = true; - } - base.TraverseChildren(method); - } - - public void InjectPhoneCodeAssemblies(IEnumerable assemblies) { - foreach (var a in assemblies) { - this.Traverse((IAssembly)a); - } - } - } -} diff --git a/BytecodeTranslator/Phone/stubs.bpl b/BytecodeTranslator/Phone/stubs.bpl deleted file mode 100644 index ae97e03..0000000 --- a/BytecodeTranslator/Phone/stubs.bpl +++ /dev/null @@ -1,41 +0,0 @@ -function isControlEnabled(Ref) : bool; -function isControlChecked(Ref) : bool; - -procedure System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool); -procedure System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool); - -implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) { - $result := (a$in == b$in); -} - -implementation System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) { - $result := (a$in != b$in); -} - -procedure System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool); -implementation System.Windows.Controls.Control.set_IsEnabled$System.Boolean($this: Ref, value$in: bool) { - assume isControlEnabled($this) == value$in; -} - -procedure System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref); -implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns ($result: Ref) { - var enabledness: bool; - enabledness := isControlEnabled($this); - $result := Box2Ref(Bool2Box(enabledness)); -} - -procedure System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref); -implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref) { - var check: bool; - - check := Box2Bool(Ref2Box(value$in)); - assume isControlChecked($this) == check; -} - -procedure System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref); -implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($this: Ref) returns ($result: Ref) { - var isChecked: bool; - isChecked := isControlChecked($this); - $result := Box2Ref(Bool2Box(isChecked)); -} - diff --git a/BytecodeTranslator/Program.cs b/BytecodeTranslator/Program.cs index f9a43b6..b267f61 100644 --- a/BytecodeTranslator/Program.cs +++ b/BytecodeTranslator/Program.cs @@ -19,11 +19,9 @@ using System.Diagnostics.Contracts; using Microsoft.Cci.MutableCodeModel.Contracts; using TranslationPlugins; -using BytecodeTranslator.Phone; using System.Text.RegularExpressions; using BytecodeTranslator.TranslationPlugins; using BytecodeTranslator.TranslationPlugins.BytecodeTranslator; -using BytecodeTranslator.TranslationPlugins.PhoneTranslator; namespace BytecodeTranslator { @@ -60,15 +58,6 @@ public enum HeapRepresentation { splitFields, twoDInt, twoDBox, general } [OptionDescription("Stub assembly", ShortForm = "s")] public List/*?*/ stub = null; - [OptionDescription("Phone translation controls configuration")] - public string phoneControls = null; - - [OptionDescription("Add phone navigation code on translation. Requires /phoneControls. Default false", ShortForm = "wpnav")] - public bool phoneNavigationCode= false; - - [OptionDescription("Add phone feedback code on translation. Requires /phoneControls. Default false", ShortForm = "wpfb")] - public bool phoneFeedbackCode = false; - [OptionDescription("File containing white/black list (optionally end file name with + for white list, - for black list, default is white list", ShortForm = "exempt")] public string exemptionFile = ""; @@ -183,11 +172,6 @@ static int Main(string[] args) return 1; } - if ((options.phoneFeedbackCode || options.phoneNavigationCode) && (options.phoneControls == null || options.phoneControls == "")) { - Console.WriteLine("Options /phoneNavigationCode and /phoneFeedbackCode need /phoneControls option set."); - return 1; - } - var pgm = TranslateAssembly(assemblyNames, heap, options, exemptionList, whiteList); var fileName = assemblyNames[0]; fileName = Path.GetFileNameWithoutExtension(fileName); @@ -289,9 +273,6 @@ public static int TranslateAssemblyAndWriteOutput(List assemblyNames, He 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.Empty, true, true); Host = host; @@ -375,7 +356,7 @@ public static int TranslateAssemblyAndWriteOutput(List assemblyNames, He throw new TranslationException("No input assemblies to translate."); } - var primaryModule = modules[0]; + //var primaryModule = modules[0]; Sink sink= new Sink(host, heapFactory, options, exemptionList, whiteList); TranslationHelper.tmpVarCounter = 0; @@ -386,58 +367,9 @@ public static int TranslateAssemblyAndWriteOutput(List assemblyNames, He Translator bcTranslator = bctPlugin.getTranslator(sink, contractExtractors, pdbReaders); translatorsPlugged.Add(bcTranslator); - if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") { - // TODO this should be part of the translator initialziation - PhoneCodeHelper.initialize(host); - PhoneCodeHelper.instance().PhonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile); - - if (doPhoneNav) { - // TODO this should be part of the translator initialziation - PhoneCodeHelper.instance().PhoneNavigationToggled = true; - - ITranslationPlugin phoneInitPlugin = new PhoneInitializationPlugin(); - ITranslationPlugin phoneNavPlugin = new PhoneNavigationPlugin(); - Translator phInitTranslator = phoneInitPlugin.getTranslator(sink, contractExtractors, pdbReaders); - Translator phNavTranslator = phoneNavPlugin.getTranslator(sink, contractExtractors, pdbReaders); - translatorsPlugged.Add(phInitTranslator); - translatorsPlugged.Add(phNavTranslator); - } - - if (doPhoneFeedback) { - // TODO this should be part of the translator initialziation - PhoneCodeHelper.instance().PhoneFeedbackToggled = true; - - ITranslationPlugin phoneFeedbackPlugin = new PhoneFeedbackPlugin(); - Translator phFeedbackTranslator = phoneFeedbackPlugin.getTranslator(sink, contractExtractors, pdbReaders); - translatorsPlugged.Add(phFeedbackTranslator); - } - } #endregion sink.TranslationPlugins = translatorsPlugged; - /* - if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") { - // TODO send this all way to initialization of phone plugin translator - PhoneCodeHelper.initialize(host); - PhoneCodeHelper.instance().PhonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile); - - // TODO these parameters will eventually form part of plugin configuration - if (doPhoneNav) { - PhoneCodeHelper.instance().PhoneNavigationToggled = true; - PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host); - initTr.InjectPhoneCodeAssemblies(modules); - PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(host); - navTr.InjectPhoneCodeAssemblies(modules); - } - - if (doPhoneFeedback) { - PhoneCodeHelper.instance().PhoneFeedbackToggled = true; - PhoneControlFeedbackMetadataTraverser fbMetaDataTraverser= new PhoneControlFeedbackMetadataTraverser(host); - fbMetaDataTraverser.Visit(modules); - } - } - */ - // TODO replace the whole translation by a translator initialization and an orchestrator calling back for each element // TODO for the current BC translator it will possibly just implement onMetadataElement(IModule) // TODO refactor this away, handle priorities between plugged translators @@ -458,12 +390,6 @@ public static int TranslateAssemblyAndWriteOutput(List assemblyNames, He // Subtyping for extern types if(sink.Options.typeInfo > 0) sink.DeclareExternTypeSubtyping(); - string outputFileName = primaryModule.Name + ".bpl"; - callPostTranslationTraversers(modules, sink, phoneControlsConfigFile, outputFileName); - if (PhoneCodeHelper.instance().PhoneNavigationToggled) { - finalizeNavigationAnalysisAndBoogieCode(phoneControlsConfigFile, sink, outputFileName); - } - //sink.CreateIdentifierCorrespondenceTable(primaryModule.Name.Value); //var rc = new Bpl.ResolutionContext((Bpl.IErrorSink)null); @@ -492,113 +418,6 @@ public static int TranslateAssemblyAndWriteOutput(List assemblyNames, He return sink.TranslatedProgram; } - - 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 modules, Sink sink, string phoneControlsConfigFile, string outputFileName) { - if (PhoneCodeHelper.instance().PhoneFeedbackToggled) { - PhoneCodeHelper.instance().CreateFeedbackCallingMethods(sink); - } - - if (PhoneCodeHelper.instance().PhoneFeedbackToggled || PhoneCodeHelper.instance().PhoneNavigationToggled) { - PhoneMethodInliningMetadataTraverser inlineTraverser = - new PhoneMethodInliningMetadataTraverser(PhoneCodeHelper.instance()); - inlineTraverser.findAllMethodsToInline(modules); - PhoneCodeHelper.updateInlinedMethods(sink, inlineTraverser.getMethodsToInline()); - System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount); - - PhoneBackKeyCallbackTraverser traverser = new PhoneBackKeyCallbackTraverser(sink.host); - traverser.Traverse(modules); - - } - } - - private static void outputBoogieTrackedControlConfiguration(string phoneControlsConfigFile) { - string outputConfigFile = Path.ChangeExtension(phoneControlsConfigFile, "bplout"); - StreamWriter outputStream = new StreamWriter(outputConfigFile); - PhoneCodeHelper.instance().PhonePlugin.DumpControlStructure(outputStream); - outputStream.Close(); - } - - 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> targets = PhoneCodeHelper.instance().BackKeyNavigatingOffenders[type]; - Console.WriteLine("\t" + type.ToString() + " may navigate to "); - foreach (Tuple 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)); - } - } - } - - if (PhoneCodeHelper.instance().BackKeyPressHandlerCancels) { - Console.Out.WriteLine("Back navigation ISSUE: back key press default behaviour may be cancelled! From pages:"); - foreach (Tuple cancellation in PhoneCodeHelper.instance().BackKeyCancellingOffenders) { - Console.WriteLine("\t" + cancellation.Item1.ToString() + " via " + cancellation.Item2); - } - } - } - } - - 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 modules) { - foreach (IMethodReference navMethod in PhoneCodeHelper.instance().KnownBackKeyHandlers) { - // right now we traversed everything so we can see reachability - IEnumerable indirects = PhoneCodeHelper.instance().getIndirectNavigators(modules, navMethod); - if (indirects.Count() > 0) { - ICollection> targets = null; - PhoneCodeHelper.instance().BackKeyNavigatingOffenders.TryGetValue(navMethod.ContainingType, out targets); - if (targets == null) { - targets = new HashSet>(); - } - string indirectTargeting = " via ("; - foreach (IMethodDefinition methDef in indirects) { - indirectTargeting += methDef.ContainingType.ToString() + "." + methDef.Name.Value + ", "; - } - indirectTargeting += ")"; - targets.Add(Tuple.Create(navMethod, indirectTargeting)); - PhoneCodeHelper.instance().BackKeyNavigatingOffenders[navMethod.ContainingType] = targets; - } - - 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(navMethod.ContainingType, indirectTargeting)); - } - } - } - private static string NameUpToFirstPeriod(string name) { var i = name.IndexOf('.'); if (i == -1) diff --git a/BytecodeTranslator/StatementTraverser.cs b/BytecodeTranslator/StatementTraverser.cs index 789a5c7..e133c62 100644 --- a/BytecodeTranslator/StatementTraverser.cs +++ b/BytecodeTranslator/StatementTraverser.cs @@ -17,7 +17,6 @@ using Bpl = Microsoft.Boogie; using System.Diagnostics.Contracts; using TranslationPlugins; -using BytecodeTranslator.Phone; namespace BytecodeTranslator @@ -387,17 +386,6 @@ public override void TraverseChildren(IReturnStatement returnStatement) { new Bpl.IdentifierExpr(tok, this.sink.ReturnVariable), etrav.TranslatedExpressions.Pop())); } - - // FEEDBACK TODO extract into a method - if (PhoneCodeHelper.instance().PhoneFeedbackToggled) { - IMethodDefinition methodTranslated = sink.getMethodBeingTranslated(); - if (methodTranslated != null && PhoneCodeHelper.instance().isMethodInputHandlerOrFeedbackOverride(methodTranslated) && - !PhoneCodeHelper.instance().isMethodIgnoredForFeedback(methodTranslated)) { - Bpl.AssertCmd falseAssertion = new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False); - StmtBuilder.Add(falseAssertion); - } - } - StmtBuilder.Add(new Bpl.ReturnCmd(returnStatement.Token())); } #endregion @@ -475,17 +463,6 @@ public void GenerateDispatchContinuation(ITryCatchFinallyStatement tryCatchFinal private void RaiseExceptionHelper(Bpl.StmtListBuilder builder) { int count = this.sink.nestedTryCatchFinallyStatements.Count; if (count == 0) { - // FEEDBACK TODO unfortunately return statements are created here too - // FEEDBACK TODO extract into a method - if (PhoneCodeHelper.instance().PhoneFeedbackToggled) { - IMethodDefinition methodTranslated = sink.getMethodBeingTranslated(); - if (methodTranslated != null && PhoneCodeHelper.instance().isMethodInputHandlerOrFeedbackOverride(methodTranslated) && - !PhoneCodeHelper.instance().isMethodIgnoredForFeedback(methodTranslated)) { - Bpl.AssertCmd falseAssertion = new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.LiteralExpr.False); - builder.Add(falseAssertion); - } - } - builder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken)); } else { diff --git a/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs b/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs deleted file mode 100644 index c6d9b24..0000000 --- a/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs +++ /dev/null @@ -1,15 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Cci; -using Microsoft.Cci.Contracts; -using BytecodeTranslator.TranslationPlugins.Translators; - -namespace BytecodeTranslator.TranslationPlugins.PhoneTranslator { - class PhoneFeedbackPlugin : ITranslationPlugin { - public Translator getTranslator(Sink sink, IDictionary contractProviders, IDictionary pdbReaders) { - return new PhoneFeedbackTranslator(sink); - } - } -} diff --git a/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs b/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs deleted file mode 100644 index 98282fa..0000000 --- a/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs +++ /dev/null @@ -1,21 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Cci; -using Microsoft.Cci.Contracts; -using BytecodeTranslator.TranslationPlugins.Translators; - -namespace BytecodeTranslator.TranslationPlugins.PhoneTranslator { - class PhoneInitializationPlugin : ITranslationPlugin { - public Translator getTranslator(Sink sink, IDictionary contractProviders, IDictionary pdbReaders) { - return new PhoneInitializationTranslator(sink); - } - } - - class PhoneNavigationPlugin : ITranslationPlugin { - public Translator getTranslator(Sink sink, IDictionary contractProviders, IDictionary pdbReaders) { - return new PhoneNavigationTranslator(sink); - } - } -} diff --git a/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs b/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs deleted file mode 100644 index ffd6fe5..0000000 --- a/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs +++ /dev/null @@ -1,36 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using BytecodeTranslator.Phone; -using Microsoft.Cci; - -namespace BytecodeTranslator.TranslationPlugins.Translators { - class PhoneFeedbackTranslator : Translator { - private Sink sink; - PhoneControlFeedbackMetadataTraverser traverser; - - public PhoneFeedbackTranslator(Sink sink) { - this.sink = sink; - } - - public override void initialize() { - traverser = new PhoneControlFeedbackMetadataTraverser(sink.host as MetadataReaderHost); - } - - public override bool isOneShot() { - return true; - } - - public override int getPriority() { - // TODO make configurable from outside - return 3; - } - - public override void TranslateAssemblies(IEnumerable assemblies) { - foreach (var a in assemblies) { - traverser.Traverse((IAssembly)a); - } - } - } -} diff --git a/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs b/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs deleted file mode 100644 index 7cd35b4..0000000 --- a/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs +++ /dev/null @@ -1,61 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; - -using BytecodeTranslator.Phone; -using Microsoft.Cci; - -namespace BytecodeTranslator.TranslationPlugins.Translators { - class PhoneInitializationTranslator : Translator { - private Sink sink; - PhoneInitializationMetadataTraverser traverser; - - public PhoneInitializationTranslator(Sink sink) { - this.sink = sink; - } - - public override void initialize() { - traverser = new PhoneInitializationMetadataTraverser(sink.host as MetadataReaderHost); - } - - public override bool isOneShot() { - return true; - } - - public override int getPriority() { - // TODO make configurable from outside - return 1; - } - - public override void TranslateAssemblies(IEnumerable assemblies) { - traverser.InjectPhoneCodeAssemblies(assemblies); - } - } - - class PhoneNavigationTranslator : Translator { - private Sink sink; - PhoneNavigationMetadataTraverser traverser; - - public PhoneNavigationTranslator(Sink sink) { - this.sink = sink; - } - - public override void initialize() { - traverser = new PhoneNavigationMetadataTraverser(sink.host as MetadataReaderHost); - } - - public override bool isOneShot() { - return true; - } - - public override int getPriority() { - // TODO make configurable from outside - return 2; - } - - public override void TranslateAssemblies(IEnumerable assemblies) { - traverser.InjectPhoneCodeAssemblies(assemblies); - } - } -} diff --git a/PhoneControlsExtractor/MS Phone App Analysis doc.docx b/PhoneControlsExtractor/MS Phone App Analysis doc.docx deleted file mode 100644 index c202b9b..0000000 Binary files a/PhoneControlsExtractor/MS Phone App Analysis doc.docx and /dev/null differ diff --git a/PhoneControlsExtractor/NavGraphBuilder.README.txt b/PhoneControlsExtractor/NavGraphBuilder.README.txt deleted file mode 100644 index 1217e0b..0000000 --- a/PhoneControlsExtractor/NavGraphBuilder.README.txt +++ /dev/null @@ -1,14 +0,0 @@ -Navigation graph builder ------------------------- - -A few points must be taken into account -- you need the XAML files for the application, and they must reside (flat) in the same directory as the app file. If flatting results in name clashes, rename one of those files clashing -- if you don't have the XAML files, they usually reside in some form in the resources of the .dll. I am not automatically extracting this yet. -- the graph building may fail at any step. Usually, it is the bytecode translator that fails to produce a valid Boogie file. For this, there is a hidden ooption --build/-b - this option receives a string, where each character encodes an action to take. If the character is present (or no build option is passed), the action takes place. - c: extract control information - i: inject and translate (if BCT gives you problems, correct .bpl by hand and run *without* this step) - t: test the resulting boogie file, useful to see whether to skip 'i' or not - b: create the boogie queries. You may choose to skip this if you built them already and it takes too long. I need to optimize this. - q: run the queries - g: build the graph. It won't work if you don't include 'q' as the intermediate step is not saved yet diff --git a/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py b/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py deleted file mode 100644 index 053b932..0000000 --- a/PhoneControlsExtractor/PhoneBoogieCodeGenerator.py +++ /dev/null @@ -1,288 +0,0 @@ -import sys -import getopt -import os -from xml.dom import minidom -from itertools import product -import xml.dom - -CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton", "Pivot"] -CONTAINER_CONTROL_NAMES= ["Canvas", "Grid", "StackPanel"] - -# TODO externalize strings, share with C# code -CONTINUEONPAGE_VAR= "__BOOGIE_ContinueOnPage__" - -staticControlsMap= {} -mainPageXAML= None -mainAppClassname= None -appVarName = "__BOOGIE_APP_VAR" -currentNavigationVariable= None -originalPageVars= [] -boogiePageVars= [] -boogiePageClasses= [] -dummyPageVar= "dummyBoogieStringPageName" -anonymousControlCount= 0; -ANONYMOUS_CONTROL_PREFIX= "__BOOGIE_ANONYMOUS_CONTROL_" -unrolls= 0 - -def showUsage(): - print "PhoneBoogieCodeGenerator -- create boilerplate code for Boogie verification of Phone apps" - print "Usage:" - print "\tPhoneBoogieCodeGenerator --staticUnroll --controls --output \n" - print "Options:" - print "\t--staticUnroll : Do not generate loops, unroll up to n times. If not set generates loops (default). Short form: -u" - print "\t--controls : Phone app control info. See PhoneControlsExtractor. Short form: -c" - print "\t--output : file to write with boilerplate code. Short form: -o\n" - -def isAnonymousControl(control): - name= control["bplName"] - return name.find(ANONYMOUS_CONTROL_PREFIX) != -1 - -def loadControlInfo(infoMap, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName): - global anonymousControlCount - global ANONYMOUS_CONTROL_PREFIX - - newControl={} - newControl["class"]= controlClass - newControl["enabled"]= enabled - newControl["visible"]= visible - newControl["clickHandler"]= clickHandler - newControl["checkedHandler"]= checkedHandler - newControl["uncheckedHandler"]= uncheckedHandler - newControl["selectionChangedHandler"]= selectionChangedHandler - if (bplName == ""): - # anonymous control, need a dummy boogie var, but we cannot know how it got initialized - bplName= ANONYMOUS_CONTROL_PREFIX + str(anonymousControlCount) - anonymousControlCount= anonymousControlCount+1 - newControl["bplName"]=bplName - infoMap[controlName]= newControl - -def outputPageVariables(file): - global originalPageVars - global boogiePageVars - global boogiePageClasses - - file.write("var " + appVarName + ": Ref;\n") - for entry in staticControlsMap.keys(): - pageVarName= "__BOOGIE_PAGE_VAR_" + entry - originalPageVars.append(entry) - pageInfo={} - pageInfo["name"]=pageVarName - pageInfo["boogieStringName"]= staticControlsMap[entry]["boogieStringName"] - boogiePageVars.append(pageInfo) - boogiePageClasses.append(staticControlsMap[entry]["class"]) - pageVar= "var " + pageVarName + ": Ref;\n" - file.write(pageVar) - -def outputMainProcedures(file, batFile): - for i,j in product(range(0, len(boogiePageVars)),repeat=2): - if i == j: - continue - if (boogiePageVars[i]["boogieStringName"] == dummyPageVar): - continue - if (boogiePageVars[j]["boogieStringName"] == dummyPageVar): - continue - - file.write("procedure {:inline 1} __BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) + "();\n") - file.write("implementation __BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) + "() {\n") - file.write("\tvar $doWork: bool;\n") - file.write("\tvar $activeControl: int;\n") - file.write("\tvar $isEnabledRef: Ref;\n") - file.write("\tvar $isEnabled: bool;\n") - file.write("\tvar $control: Ref;\n\n") - - file.write("\tcall " + mainAppClassname + ".#ctor(" + appVarName + ");\n") - for k in range(0,len(boogiePageVars)): - file.write("\tcall " + boogiePageClasses[k] + ".#ctor(" + boogiePageVars[k]["name"] + ");\n") - - file.write("\t//TODO still need to call Loaded handler on main page.\n") - if (unrolls == 0): - file.write("\thavoc $doWork;\n") - file.write("\twhile ($doWork) {\n") - file.write("\t\tcall DriveControls();\n") - file.write("\t\thavoc $doWork;\n") - file.write("\t}\n") - else: - for unr in range(unrolls): - file.write("\t\tcall DriveControls();\n") - - file.write("\tassume " + currentNavigationVariable + " == " + boogiePageVars[i]["boogieStringName"] + ";\n") - file.write("\tcall DriveControls();\n") - file.write("\tassume " + currentNavigationVariable + " == " + boogiePageVars[j]["boogieStringName"] + ";\n") - file.write("\tassert false;\n"); - file.write("}\n") - - batFile.write("type BOOGIE_PARTIAL.bpl > BOOGIE_PLACEHOLDER.bpl\n") - batFile.write("type BOOGIE_BOILERPLATE.bpl >> BOOGIE_PLACEHOLDER.bpl\n") - batFile.write("%POIROT_ROOT%\Corral\BctCleanup.exe BOOGIE_PLACEHOLDER.bpl BOOGIE_PLACEHOLDER_Clean.bpl /main:__BOOGIE_VERIFICATION_PROCEDURE_" + str(i) + "_" + str(j) +"\n"); - batFile.write("del corral_out_trace.txt\n") - batFile.write("%POIROT_ROOT%\corral\corral.exe /k:1 /recursionBound:20 /main:__BOOGIE_VERIFICATION_PROCEDURE_" + str(i) +"_" + str(j) + " BOOGIE_PLACEHOLDER_Clean_" + str(i) + "_" + str(j) + ".bpl\n") - batFile.write("if exist corral_out_trace.txt move corral_out_trace.txt corral_out_trace_" + str(i) + "_" + str(j) + ".txt\n") - -def outputPageControlDriver(file, originalPageName, boogiePageName): - file.write("procedure {:inline 1} drive" + boogiePageName + "Controls();\n") - file.write("implementation drive" + boogiePageName + "Controls() {\n") - file.write("\tvar $activeControl: int;\n") - file.write("\tvar $control: Ref;\n") - file.write("\tvar $isEnabledRef: Ref;\n") - file.write("\tvar $isEnabled: bool;\n") - file.write("\tvar $handlerToActivate: int;\n") - - file.write("\t" + CONTINUEONPAGE_VAR +":=true;\n") - file.write("\thavoc $activeControl;\n") - - file.write("\twhile (" + CONTINUEONPAGE_VAR + ") {\n") - activeControl=0 - ifInitialized= False - for entry in staticControlsMap[originalPageName]["controls"].keys(): - controlInfo= staticControlsMap[originalPageName]["controls"][entry] - if controlInfo["bplName"] == "": - continue; - if not ifInitialized: - file.write("\t\tif ($activeControl == " + str(activeControl) + ") {\n") - ifInitialized= True - else: - file.write("\t\telse if ($activeControl == " + str(activeControl) + ") {\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") - file.write("\t\t\tif ($isEnabled) {\n") - 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\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\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\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["uncheckedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n") - file.write("\t\t\t\t}\n") - if not controlInfo["selectionChangedHandler"] == "": - file.write("\t\t\t\tif ($handlerToActivate == 3) {\n") - file.write("\t\t\t\t\tcall " + staticControlsMap[originalPageName]["class"] + "." + controlInfo["selectionChangedHandler"] + "$System.Object$System.Windows.RoutedEventArgs(" + controlInfo["bplName"] + "[" + boogiePageName + "],null,null);\n") - file.write("\t\t\t\t}\n") - - file.write("\t\t\t}\n") - file.write("\t\t}\n") - activeControl= activeControl+1 - file.write("\t}\n") - file.write("}\n") - - -def outputControlDrivers(file, batFile): - for i in range(0,len(boogiePageVars)): - outputPageControlDriver(file, originalPageVars[i],boogiePageVars[i]["name"]) - - file.write("procedure {:inline 1} DriveControls();\n") - file.write("implementation DriveControls() {\n") - for i in range(0,len(boogiePageVars)): - file.write("\tvar isCurrent" + boogiePageVars[i]["name"] + ": bool;\n") - file.write("\n") - - for i in range(0,len(boogiePageVars)): - if boogiePageVars[i]["boogieStringName"] == dummyPageVar: - file.write("\tisCurrent" + boogiePageVars[i]["name"] + " := false;\n") - else: - file.write("\tcall isCurrent" + boogiePageVars[i]["name"] + " := System.String.op_Equality$System.String$System.String(" + currentNavigationVariable + "," + boogiePageVars[i]["boogieStringName"] + ");\n") - - firstTime= True - for i in range(0,len(boogiePageVars)): - if firstTime: - file.write("\tif") - firstTime= False - else: - file.write("\telse if") - - file.write(" (isCurrent" + boogiePageVars[i]["name"] + ") {\n") - file.write("\t\t call drive" + boogiePageVars[i]["name"] + "Controls();\n\t}\n") - file.write("}\n") - -def outputURIHavocProcedure(file): - file.write("procedure {:inline 1} __BOOGIE_Havoc_CurrentURI__();\n") - file.write("implementation __BOOGIE_Havoc_CurrentURI__() {\n") - # file.write("\thavoc " + currentNavigationVariable + ";\n") - file.write("// TODO write assume statements to filter havoc'd variable to either of all pages\n") - # file.write("\tassume ) - file.write("}\n") - -#build a batch file for test running at the same time -def outputBoilerplate(outputFile, cmdFile): - file= open(outputFile,"w") - batFile= open(cmdFile, "w") - batFile.write("del corral_out_trace.txt") - outputPageVariables(file) - outputURIHavocProcedure(file) - outputControlDrivers(file, batFile) - outputMainProcedures(file, batFile) - file.close() - batFile.close() - -def buildControlInfo(controlInfoFileName): - global mainPageXAML - global mainAppClassname - global currentNavigationVariable - global staticControlsMap - - file = open(controlInfoFileName, "r") - # Info file format is first line containing only the main page, another line with boogie's current navigation variable and then one line per - # ,,,,,,,,,,, - mainPageXAML= file.readline().strip() - currentNavigationVariable= file.readline().strip() - mainAppClassname= file.readline().strip() - - infoLine= file.readline().strip() - while not infoLine == "": - pageClass, pageName, pageBoogieStringName, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName= infoLine.split(",") - pageInfo={} - pageInfo["class"]=pageClass - try: - pageInfo= staticControlsMap[pageName] - except KeyError: - staticControlsMap[pageName]=pageInfo - - pageInfo["boogieStringName"]= pageBoogieStringName - pageControlInfo={} - try: - pageControlInfo= pageInfo["controls"] - except KeyError: - pageInfo["controls"]=pageControlInfo - loadControlInfo(pageControlInfo, controlClass, controlName, enabled, visible, clickHandler, checkedHandler, uncheckedHandler, selectionChangedHandler, bplName) - pageInfo["controls"]= pageControlInfo - staticControlsMap[pageName]=pageInfo - - infoLine=file.readline().strip() - file.close() - -def main(): - global unrolls - controlFile= "" - outputFile= "" - - try: - opts, args= getopt.getopt(sys.argv[1:], "c:o:u:", ["controls=","output=","staticUnroll="]) - except getopt.error, msg: - print msg - showUsage() - sys.exit(2) - - if not len(opts) >= 2: - print "Missing options" - showUsage() - sys.exit(2) - - for o, a in opts: - if o in ["-c","--controls"]: - controlFile= a - if o in ["-o", "--output"]: - outputFile= a - if o in ["-u", "--staticUnroll"]: - unrolls= int(a) - - buildControlInfo(controlFile) - outputBoilerplate(outputFile, outputFile + ".bat") - -if __name__ == "__main__": - main() \ No newline at end of file diff --git a/PhoneControlsExtractor/PhoneControlsExtractor.py b/PhoneControlsExtractor/PhoneControlsExtractor.py deleted file mode 100644 index 475c221..0000000 --- a/PhoneControlsExtractor/PhoneControlsExtractor.py +++ /dev/null @@ -1,248 +0,0 @@ -import sys -import getopt -import os -from xml.dom import minidom -import xml.dom - -CONTROL_NAMES= ["Button", "CheckBox", "RadioButton", "ApplicationBarIconButton", "ApplicationBarMenuItem", "Pivot", "ListBox"] - -# TODO maybe a control is enabled but its parent is not, must take this into account -# TODO a possible solution is to tie the enabled value to that of the parent in the app until it is either overriden -# TODO (by directly manipulating the control's enabled value) or the parent becomes enabled - -CONTAINER_CONTROL_NAMES= ["Canvas", "Grid", "StackPanel", "ApplicationBar"] -COMMA_REPLACEMENT="###" - -staticControlsMap= {} -mainPageXAML= None - -def showUsage(): - print "PhoneControlsExtractor -- extract control information from phone application pages" - print "Usage:" - print "\tPhoneControlsExtractor --pages --output \n" - print "Options:" - print "\t--pages : point to location of .xaml files detailing pages. Short form: -p" - print "\t--output : file to write with control info. Short form: -o\n" - -def isPageFile(file): - # not the best way, find out the actual exceptions - try: - minidom.parse(file) - file.seek(0) - return True - except Exception: - return False - -def removeBlankElements(xmlNode): - blankNodes= [] - for child in xmlNode.childNodes: - if child.nodeType == xml.dom.Node.TEXT_NODE and child.data.strip() == "": - blankNodes.append(child) - elif child.hasChildNodes(): - removeBlankElements(child) - - for node in blankNodes: - node.parentNode.removeChild(node) - node.unlink() - -def getControlNodes(xmlNode): - controlNodes= [] - if (xmlNode.nodeType == xml.dom.Node.ELEMENT_NODE and xmlNode.localName in CONTROL_NAMES): - controlNodes.insert(0,xmlNode) - - for child in xmlNode.childNodes: - controlNodes= controlNodes + getControlNodes(child) - - return controlNodes - -def addDummyControlToMap(pageXAML, parentPage): - pageControls=[] - newControl={} - try: - pageControls= staticControlsMap[parentPage] - except KeyError: - pass - - newControl["Type"]= "DummyType" - newControl["Name"]= "DummyName" - newControl["IsEnabled"]= "false" - newControl["Visibility"]= "Collapsed" - newControl["Click"] = "" - newControl["Checked"] = "" - newControl["Unchecked"] = "" - newControl["SelectionChanged"]= "" - newControl["XAML"]= pageXAML - pageControls.append(newControl) - staticControlsMap[parentPage]= pageControls - -def addControlToMap(pageXAML, parentPage, controlNode): - pageControls=[] - newControl={} - try: - pageControls= staticControlsMap[parentPage] - except KeyError: - pass - - newControl["Type"]= controlNode.localName - newControl["Name"]= controlNode.getAttribute("Name").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - if (controlNode.hasAttribute("IsEnabled")): - newControl["IsEnabled"]= controlNode.getAttribute("IsEnabled").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - else: - newControl["IsEnabled"]= "true" - - if (controlNode.hasAttribute("Visibility")): - newControl["Visibility"]= controlNode.getAttribute("Visibility").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - else: - newControl["Visibility"]= "Visible" - - # TODO it is possible that more events are of interest, we should add as we discover them in existing applications - newControl["Click"] = controlNode.getAttribute("Click").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - newControl["Checked"] = controlNode.getAttribute("Checked").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - newControl["Unchecked"] = controlNode.getAttribute("Unchecked").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - newControl["SelectionChanged"] = controlNode.getAttribute("SelectionChanged").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - newControl["XAML"]= pageXAML - pageControls.append(newControl) - staticControlsMap[parentPage]= pageControls - -def isPageXAML(pageXAML): - pageFile= open(pageXAML, "r") - if not isPageFile(pageFile): - return False - pageFileXML= minidom.parse(pageFile) - pageFile.close() - return pageFileXML.childNodes[0].nodeName.find("Page") != -1 - -def getPageNode(pageXML): -# should be the top element one, ignore otherwise - if (pageXML.nodeType == xml.dom.Node.ELEMENT_NODE and pageXML.localName.find("PhoneApplicationPage") != -1): - return pageXML - else: - return None - - - - -def extractPhoneControlsFromPage(pageXAML): - # maybe it is not a page file - print "extracting from " + pageXAML - pageFile= open(pageXAML, "r") - if not isPageFile(pageFile): - return - pageFileXML= minidom.parse(pageFile) - pageFile.close() - removeBlankElements(pageFileXML) - pageNode= getPageNode(pageFileXML) - controls= getControlNodes(pageFileXML) - ownerPage = getOwnerPage(pageFileXML) - if (ownerPage != None): - print pageXAML + " is not none" - if (len(controls) == 0): - # it is either a page with no controls, or controls that are dynamically created, or controls we do not track yet - # in any case, just add a dummy control so as not to lose the page - if (not isPageXAML(pageXAML)): - addDummyControlToMap(pageXAML, ownerPage + "__dummy") - else: - addDummyControlToMap(pageXAML, ownerPage) - else: - for control in controls: - parent= control - while not parent == None and ownerPage == None: - parent= parent.parentNode - addControlToMap(pageXAML, ownerPage, control) - -def getOwnerPage(xmlNode): - ownerPage= None - if (xmlNode.nodeType == xml.dom.Node.ELEMENT_NODE): - ownerPage= xmlNode.getAttribute("x:Class").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - if ownerPage == "": - ownerPage= None - else: - for child in xmlNode.childNodes: - ownerPage= getOwnerPage(child) - if (ownerPage != None): - break - - return ownerPage - - -def outputPhoneControls(outputFileName): - outputFile= open(outputFileName, "w") - - # Output format is first line containing only the main page, then line containing boogie navigation variable, and then one line per - # ,,,,,,,,,, - outputFile.write(mainPageXAML + "\n") - outputFile.write("dummyNavigationVariable_unknown\n") - outputFile.write("dummyMainAppName_unknown\n") # I could possibly deduce it from WMAppManifest.xml, but I'm unsure. Doing it later is safe anyway - for page in staticControlsMap.keys(): - for control in staticControlsMap[page]: - # TODO we still cannot handle bindings, and those we identified through commas and equality signs - isEnabled= control["IsEnabled"] - if (isEnabled.find(COMMA_REPLACEMENT) != -1): - isEnabled= "" - visibility= control["Visibility"] - if (visibility.find(COMMA_REPLACEMENT) != -1): - visibility= "" - click= control["Click"] - if (click.find(COMMA_REPLACEMENT) != -1): - click= "" - checked= control["Checked"] - if (checked.find(COMMA_REPLACEMENT) != -1): - checked= "" - unchecked= control["Unchecked"] - if (unchecked.find(COMMA_REPLACEMENT) != -1): - unchecked= "" - selectionChanged= control["SelectionChanged"] - if (selectionChanged.find(COMMA_REPLACEMENT) != -1): - selectionChanged= "" - pageXAML= control["XAML"] - # last comma is to account for bpl translation name, that is unknown for now - # boogie string page name is unknown for now - outputFile.write(page + "," + os.path.basename(pageXAML) + ",dummyBoogieStringPageName," + control["Type"] + "," + control["Name"] + \ - "," + isEnabled + "," + visibility + "," + click + "," + checked + "," + unchecked + "," + selectionChanged + ",\n") - - outputFile.close() - -def getMainPageXAMLFromManifest(filename): - file= open(filename, "r"); - manifest= minidom.parse(file) - file.close() - # interesting XPath location /App/Tasks/DefaultTask/@NavigationPage - return manifest.getElementsByTagName("DefaultTask")[0].getAttribute("NavigationPage").replace(",",COMMA_REPLACEMENT).replace("=",COMMA_REPLACEMENT) - -def extractPhoneControls(sourceDir): - global mainPageXAML - fileList= [os.path.join(sourceDir, fileName) for fileName in os.listdir(sourceDir) if os.path.splitext(fileName)[1] == ".xaml" or os.path.splitext(fileName)[1] == ".xml"] - for fileName in fileList: - if os.path.splitext(fileName)[1].lower() == ".xml" and os.path.splitext(os.path.split(fileName)[1])[0].lower() == "wmappmanifest": - mainPageXAML= getMainPageXAMLFromManifest(fileName) - break - - for fileName in fileList: - extractPhoneControlsFromPage(fileName) - -def main(): - pagesDir= "" - outputFile= "" - try: - opts, args= getopt.getopt(sys.argv[1:], "p:o:", ["pages=","output="]) - except getopt.error, msg: - print msg - showUsage() - sys.exit(2) - - if not len(opts) == 2: - print "Missing options" - showUsage() - sys.exit(2) - - for o, a in opts: - if o in ["-p","--pages"]: - pagesDir= a - if o in ["-o", "--output"]: - outputFile= a - - extractPhoneControls(pagesDir) - outputPhoneControls(outputFile) - -if __name__ == "__main__": - main() \ No newline at end of file diff --git a/PhoneControlsExtractor/market_apps_analyses.xlsx b/PhoneControlsExtractor/market_apps_analyses.xlsx deleted file mode 100644 index 752eaab..0000000 Binary files a/PhoneControlsExtractor/market_apps_analyses.xlsx and /dev/null differ diff --git a/PhoneControlsExtractor/navGraphBuilder.py b/PhoneControlsExtractor/navGraphBuilder.py deleted file mode 100644 index 8d72c78..0000000 --- a/PhoneControlsExtractor/navGraphBuilder.py +++ /dev/null @@ -1,299 +0,0 @@ -import sys -import getopt -import os -import time - -BOOGIE_PATH= "%boogie%" -BCT_PATH="%boogie_bct%" -CONTROL_EXTRACTOR_PATH="%phonecontrolextractor%" -WPLIB_PATH="%wplib%" -DOT_PATH="%dotpath%" - -CONTROL_CREATION_TIME=0 -INJECTION_TIME=0 -TEST_TIME=0 -QUERY_CREATION_TIME=0 -QUERY_RUN_TIME=0 -GRAPH_CREATION_TIME=0 -BOOGIE_QUERY_COUNT=0 -PAGE_COUNT=0 -EDGE_COUNT=0 - -navigation_graph = {} - -def createStatsNode(appFile): - global CONTROL_CREATION_TIME - global INJECTION_TIME - global TEST_TIME - global QUERY_CREATION_TIME - global QUERY_RUN_TIME - global GRAPH_CREATION_TIME - global BOOGIE_QUERY_COUNT - global PAGE_COUNT - global EDGE_COUNT - - total= CONTROL_CREATION_TIME + INJECTION_TIME + TEST_TIME + QUERY_CREATION_TIME + QUERY_RUN_TIME + GRAPH_CREATION_TIME - statsNode= "node [shape=plaintext, label=" + \ - "<" + \ - "" + \ - "" + \ - "" + \ - "" + \ - "" + \ - "" + \ - "" + \ - "" + \ - "" + \ - "
" + os.path.basename(appFile) + "
Control extraction time" + str(CONTROL_CREATION_TIME) + " s.
Injection and translation time" + str(INJECTION_TIME) + " s.
Boogie test time" + str(TEST_TIME) + " s.
Query creation time" + str(QUERY_CREATION_TIME) + " s.
Boogie query run time (" + str(BOOGIE_QUERY_COUNT) + " queries)" + str(QUERY_RUN_TIME) + " s.
Graph creation time" + str(GRAPH_CREATION_TIME) + " s.
Graph sparseness" + str(EDGE_COUNT) + " over " + str(PAGE_COUNT*PAGE_COUNT) + " possible
Total time" + str(total) + " s.
>" + \ - "] statsNode;" - # statsNode= statsNode.replace(".","/") - return statsNode - -def checkEnv(): - retVal= True - os.system("echo " + DOT_PATH + " > checkEnv") - check= open("checkEnv", "r") - if check.readline().strip() == DOT_PATH: - print DOT_PATH + " not set" - retVal= False - - os.system("echo " + WPLIB_PATH + " > checkEnv") - check= open("checkEnv", "r") - if check.readline().strip() == WPLIB_PATH: - print WPLIB_PATH + " not set" - retVal= False - - os.system("echo " + BOOGIE_PATH + " > checkEnv") - check= open("checkEnv", "r") - if check.readline().strip() == BOOGIE_PATH: - print BOOGIE_PATH + " not set" - retVal= False - - os.system("echo " + BCT_PATH + " > checkEnv") - check= open("checkEnv", "r") - if check.readline().strip() == BCT_PATH: - print BCT_PATH +" not set" - retVal= False - - os.system("echo " + CONTROL_EXTRACTOR_PATH + " > checkEnv") - check= open("checkEnv", "r") - if check.readline().strip() == CONTROL_EXTRACTOR_PATH: - print CONTROL_EXTRACTOR_PATH + " not set" - retVal= False - - check.close() - os.remove("checkEnv") - return retVal - -def createAppControlsFile(appFile, outputFile, format): - error = os.system(CONTROL_EXTRACTOR_PATH + " -p \"" + os.path.dirname(appFile) + "\" -o \"" + os.path.splitext(appFile)[0] + ".controls\" > nul") - if error != 0 or not os.path.exists(os.path.splitext(appFile)[0] + ".controls"): - return False - return True - -def bctAppFile(appFile, outputFile, format): - error = os.system(BCT_PATH + " /heap:splitFields /lib:\"" + WPLIB_PATH + "\" /wpnav /phoneControls:\"" + \ - os.path.splitext(appFile)[0] + ".controls\" \"" + appFile + "\" > NavigationReport") - if error != 0 or not os.path.exists(os.path.splitext(appFile)[0] + ".bpl"): - return False - return True - -def testBoogieOutput(appFile, outputFile, format): - error = os.system(BOOGIE_PATH + " /doModSetAnalysis /noVerify \"" + os.path.splitext(appFile)[0] + ".bpl\" > testBpl") - testBpl= open("testBpl", "r") - output= testBpl.read() - testBpl.close() - os.remove("testBpl") - if error != 0 or output.find("Error:") != -1: - return False - return True - -def cleanupQueriesTempFiles(): - for tempFile in [os.path.abspath(filename) for filename in os.listdir(".") if filename.startswith("sed") and os.path.splitext(filename)[1]==""]: - os.remove(tempFile) - -def createBoogieQueries(appFile, outputFile, format): - cmd ="\"" + os.path.dirname(appFile) + "\\createQueries.bat\" > nul" - error = os.system(cmd) - cleanupQueriesTempFiles() - if error != 0: - return False - return True - -def runBoogieQueries(appFile, outputFile, format): - global navigation_graph - global BOOGIE_QUERY_COUNT - global EDGE_COUNT - global PAGE_COUNT - - queryFiles= [os.path.abspath(filename) for filename in os.listdir(".") if filename.find("$$") != -1 and os.path.splitext(filename)[1]==".bpl"] - BOOGIE_QUERY_COUNT= len(queryFiles) - for filename in queryFiles: - start= os.path.splitext(filename.split("$$")[1])[0] - end= os.path.splitext(filename.split("$$")[3])[0] - try: - dests= navigation_graph[start] - except KeyError: - PAGE_COUNT=PAGE_COUNT+1 - dests= [] - navigation_graph[start]= [] - error = os.system(BOOGIE_PATH + " /doModSetAnalysis /prover:SMTLib \"" + filename +"\" > testBpl") - testBpl= open("testBpl", "r") - output= testBpl.read() - testBpl.close() - os.remove("testBpl") - if error != 0 or output.find("Error:") != -1: - return False - if output.find("might not hold") != -1: - dests.append(end) - navigation_graph[start]= dests - EDGE_COUNT=EDGE_COUNT+1 - 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]) - dotFile.write("digraph " + graphName + "{\n") - dotFile.write("\tnode [style=\"invisible\", label=\"\"] n0;\n") - nextNode=1 - for pagename in navigation_graph.keys(): - dotFile.write("\tnode [style=\"rounded\", shape=\"box\", label=\"" + pagename + "\"] n"+ str(nextNode) + ";\n") - nameToNode[pagename]=nextNode - nextNode= nextNode + 1 - - dotFile.write("\n") - for pagename in navigation_graph.keys(): - startNode= nameToNode[pagename] - for dest in navigation_graph[pagename]: - destNode = nameToNode[dest] - dotFile.write("\tn" + str(startNode) + " -> n" + str(destNode) + ";\n") - - # Try and see if we know the start page - controls= open(os.path.splitext(appFile)[0] + ".controls", "r") - mainpage= os.path.splitext(controls.readline().strip().lower())[0] - try: - globalStart= nameToNode[mainpage] - 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("}") - dotFile.close() - - if format != "dot": - os.system(DOT_PATH + " -T" + format + " -o \"" + outputFile + "\" \"" + os.path.splitext(appFile)[0] + ".dot\" > nul") - else: - os.rename("\"" + os.path.splitext(appFile)[0] + ".dot\"", "\"" + outputFile + "\"") - return True - -def showUsage(): - print "NavGraphBuilder -- builds the navigation graph from a phone app. See caveats in NavGraphBuilder.README" - print "Usage:" - print "\tNavGraphBuilder --app --output --format " - print "Options:" - print "\t--app : point to location of main application .dll. Short form: -a. Required." - print "\t--output : file to write graph to. Short form: -o. Optional, defaults to name of phone app and selected format." - print "\t--format : format to draw the graph into. Short form: -f. Optional, accepts dot output formats, defaults to pdf.\n" - -def main(): - global CONTROL_CREATION_TIME - global INJECTION_TIME - global TEST_TIME - global QUERY_CREATION_TIME - global QUERY_RUN_TIME - global GRAPH_CREATION_TIME - - if (not checkEnv()): - sys.exit(1) - - try: - opts, args= getopt.getopt(sys.argv[1:], "a:o:f:b:", ["app=","output=","format=","build="]) - except getopt.error, msg: - print msg - showUsage() - sys.exit(2) - - if len(opts) < 1: - print "Missing options" - showUsage() - sys.exit(2) - - appFile="" - outputFile="" - format="" - build="" - for o, a in opts: - if o in ["-a","--app"]: - appFile= a - if o in ["-o", "--output"]: - outputFile= a - if o in ["-f", "--format"]: - format= a.lower() - if o in ["-b", "--build"]: - build= a - - if format=="": - format= "pdf" - - appFile = os.path.abspath(appFile) - if outputFile=="": - outputFile= os.path.splitext(appFile)[0] + "." + format - outputFile= os.path.abspath(outputFile) - - if build=="" or build.find("c") != -1: - CONTROL_CREATION_TIME= time.clock(); - print "Extracting control information..." - if (not createAppControlsFile(appFile, outputFile, format)): - print "Failed to create app controls file" - sys.exit(1) - CONTROL_CREATION_TIME= time.clock() - CONTROL_CREATION_TIME - - if build=="" or build.find("i") != -1: - INJECTION_TIME= time.clock() - print "Injecting and translating application binary..." - if (not bctAppFile(appFile, outputFile, format)): - print "Failed to translate application library" - sys.exit(1) - INJECTION_TIME= time.clock() - INJECTION_TIME - - if build=="" or build.find("t") != -1: - TEST_TIME= time.clock() - print "Testing boogie file..." - if (not testBoogieOutput(appFile, outputFile, format)): - print "ByteCode Translator produced erroneous or ambiguous boogie file" - sys.exit(1) - TEST_TIME= time.clock() - TEST_TIME - - if build=="" or build.find("b") != -1: - QUERY_CREATION_TIME= time.clock() - print "Creating boogie queries..." - if (not createBoogieQueries(appFile, outputFile, format)): - print "Error creating boogie queries" - sys.exit(1) - QUERY_CREATION_TIME= time.clock() - QUERY_CREATION_TIME - - if build=="" or build.find("q") != -1: - QUERY_RUN_TIME= time.clock() - print "Running boogie queries..." - if (not runBoogieQueries(appFile, outputFile, format)): - print "Error running boogie queries" - sys.exit(1) - QUERY_RUN_TIME= time.clock() - QUERY_RUN_TIME - - if build=="" or build.find("g") != -1: - print "Building graph..." - if (not buildNavigationGraph(appFile, outputFile, format)): - print "Error creating navigation graph" - sys.exit(1) - - print "Success!" - sys.exit(0) - -if __name__ == "__main__": - main() \ No newline at end of file diff --git a/TranslationPlugins/PhoneControlsPlugin.cs b/TranslationPlugins/PhoneControlsPlugin.cs deleted file mode 100644 index 845431a..0000000 --- a/TranslationPlugins/PhoneControlsPlugin.cs +++ /dev/null @@ -1,404 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.IO; - -namespace TranslationPlugins { - public enum Visibility { Visible, Collapsed }; - - public enum Event { Click, Checked, Unchecked, SelectionChanged }; - - public class HandlerSignature { - public static string[] getParameterTypesForHandler(Event controlEvent) { - switch (controlEvent) { - case Event.Checked: - case Event.Unchecked: - case Event.Click: - case Event.SelectionChanged: - return new string[] { "object", "System.WindowsRoutedventArgs" }; - default: - throw new NotImplementedException("Handlers for event: " + controlEvent + " not supported yet"); - } - } - // TODO it would be nice to be dynamic on handler names and parameters - // TODO for now you just have to know the handler signature for each event at load time, and for now we only handle a handful of default control events - public string Name; - public string[] ParameterTypes; - } - - public class ControlInfoStructure { - 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> handlers; - - public ControlInfoStructure() { - handlers = new Dictionary>(); - } - - public void setHandler(Event p, string handler) { - IList eventHandlers; - try { - eventHandlers = handlers[p]; - } catch (KeyNotFoundException) { - eventHandlers= new List(); - handlers[p] = eventHandlers; - } - - HandlerSignature newHandler= new HandlerSignature(); - newHandler.Name= handler; - newHandler.ParameterTypes= HandlerSignature.getParameterTypesForHandler(p); - eventHandlers.Add(newHandler); - } - - public IList getHandlers(Event p) { - try { - return handlers[p]; - } catch (KeyNotFoundException) { - return new List(); - } - } - } - - class PageStructure { - public PageStructure() { - controlsInfo = new Dictionary(); - } - - public string PageBoogieName { get; set; } - public string PageClassName { get; set; } - public string PageXAML { get; set; } - public bool IsMainPage { get; set; } - - private IDictionary controlsInfo; - public ControlInfoStructure getControlInfo(string controlName) { - try { - return controlsInfo[controlName]; - } catch (KeyNotFoundException) { - return null; - } - } - - public void setControlInfo(string controlName, ControlInfoStructure controlInfo) { - controlsInfo[controlName] = controlInfo; - } - - public IEnumerable getAllControlsInfo() { - return controlsInfo.Values.AsEnumerable(); - } - } - - 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= 12; - private static int PAGE_CLASS_FIELD= 0; - private static int PAGE_XAML_FIELD= 1; - private static int PAGE_BOOGIE_STRING_FIELD = 2; - private static int CONTROL_CLASS_FIELD= 3; - private static int CONTROL_NAME_FIELD= 4; - private static int ENABLED_FIELD= 5; - private static int VISIBILITY_FIELD= 6; - private static int CLICK_HANDLER_FIELD= 7; - private static int CHECKED_HANDLER_FIELD= 8; - private static int UNCHECKED_HANDLER_FIELD = 9; - private static int SELECTIONCHANGED_HANDLER_FIELD = 10; - private static int BPL_NAME_FIELD = 11; - - public const string BOOGIE_DUMMY_CONTROL = "__BOOGIE_DUMMY_CONTROLNAME_"; - - private IDictionary pageStructureInfo; - - public static string getURILastPath(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(); - } - - //public static string getFullyQualifiedControlClass(string controlClass) { - // // TODO do an actual API discovery. The problem will be differencing 7.0 apps from 7.1 apps - // return "System.Windows.Controls." + controlClass; - //} - - public PhoneControlsPlugin(string configFile) { - pageStructureInfo = new Dictionary(); - StreamReader fileStream = null; - try { - fileStream = new StreamReader(configFile); - } catch (Exception e) { - if (e is DirectoryNotFoundException || e is FileNotFoundException || e is IOException) { - // TODO log, I don't want to terminate BCT because of this - throw; - } else if (e is ArgumentException || e is ArgumentNullException) { - // TODO log, I don't want to terminate BCT because of this - throw; - } else { - throw; - } - } - - LoadControlStructure(fileStream); - - if (fileStream != null) - fileStream.Close(); - } - - public string getMainPageXAML() { - KeyValuePair entry= pageStructureInfo.FirstOrDefault(keyValue => keyValue.Value.IsMainPage); - return entry.Value.PageXAML; - } - - private string boogieCurrentNavigationVariable; - public string getBoogieNavigationVariable() { - return boogieCurrentNavigationVariable; - } - - public void setBoogieNavigationVariable(string var) { - boogieCurrentNavigationVariable = var; - } - - private void setPageAsMainPage(string pageXAML) { - pageXAML = pageXAML.ToLower(); - int lastDirPos= pageXAML.LastIndexOf('/'); - if (lastDirPos != -1) - pageXAML = pageXAML.Substring(lastDirPos+1); - KeyValuePair mainPageClass= pageStructureInfo.FirstOrDefault(keyValue => keyValue.Value.PageXAML.ToLower() == pageXAML.ToLower()); - if (mainPageClass.Equals(default(KeyValuePair))) { - // the main page doesn't exist because it has no tracked controls. While we cannot track those controls, create a page struct for it - } else { - mainPageClass.Value.IsMainPage = true; - } - } - - private string mainAppTypeName; - public void setMainAppTypeName(string typeName) { - mainAppTypeName= typeName; - } - - public string getMainAppTypeName() { - return mainAppTypeName; - } - - public void DumpControlStructure(StreamWriter outputStream) { - // maintain same format as input format - string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, - checkedHandler, uncheckedHandler, selectionChangedHandler, bplName; - outputStream.WriteLine(getMainPageXAML()); - outputStream.WriteLine(getBoogieNavigationVariable()); - outputStream.WriteLine(getMainAppTypeName()); - - foreach (KeyValuePair entry in this.pageStructureInfo) { - pageClass = entry.Key; - pageXAML = entry.Value.PageXAML.ToLower(); - pageBoogieStringName = entry.Value.PageBoogieName; - 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 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 = ""; - } - - handlers = controlInfo.getHandlers(Event.SelectionChanged); - if (handlers.Any()) { - selectionChangedHandler= handlers.First().Name; - } else { - selectionChangedHandler = ""; - } - bplName = controlInfo.BplName; - outputStream.WriteLine(pageClass + "," + pageXAML.ToLower() + "," + pageBoogieStringName + "," + controlClass + "," + controlName + "," + enabled + "," + - visibility + "," + clickHandler + "," + checkedHandler + "," + uncheckedHandler + "," + selectionChangedHandler + "," + - bplName); - } - } - } - - public void setBoogieStringPageNameForPageClass(string pageClass, string boogieStringPageName) { - pageStructureInfo[pageClass].PageBoogieName = boogieStringPageName; - } - - private static int dummyControlNameIndex = 0; - private void LoadControlStructure(StreamReader configStream) { - // FEEDBACK TODO. Easy check on Feedback issue: Button and HyperLinkButton MUST have a Click handler, if not, it is obvious there is no feedback - - // 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 ,,,,,,,,,, - // TODO BPL control name will most probably be empty, but it is useful to be able to dump it - // TODO check PhoneControlsExtractor.py and PhoneBoogieCodeCreator.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 - - string pageClass, pageXAML, pageBoogieStringName, controlClass, controlName, enabled, visibility, clickHandler, checkedHandler, - uncheckedHandler, selectionChangedHandler, bplName; - string configLine = configStream.ReadLine(); - string[] inputLine; - PageStructure pageStr; - ControlInfoStructure controlInfoStr; - - // first line just states the main page xaml - string mainPageXAML= configLine.Trim().ToLower(); - configLine = configStream.ReadLine(); - - // second line states boogie current nav variable, possibly dummy value - setBoogieNavigationVariable(configLine.Trim()); - configLine= configStream.ReadLine(); - - // third line is main phone app type, possibly dummy; - setMainAppTypeName(configLine.Trim()); - configLine = configStream.ReadLine(); - - while (configLine != null) { - if (configLine.Trim().Equals(string.Empty)) { - configLine = configStream.ReadLine(); - continue; - } - inputLine = configLine.Split(','); - - if (inputLine.Length != CONFIG_LINE_FIELDS) - throw new ArgumentException("Config input line contains wrong number of fields: " + inputLine.Length + ", expected " + CONFIG_LINE_FIELDS); - - pageClass = inputLine[PAGE_CLASS_FIELD].Trim(); - pageXAML = inputLine[PAGE_XAML_FIELD].Trim().ToLower(); - pageBoogieStringName = inputLine[PAGE_BOOGIE_STRING_FIELD].Trim(); - controlClass = inputLine[CONTROL_CLASS_FIELD].Trim(); - controlName = inputLine[CONTROL_NAME_FIELD].Trim(); - if (string.IsNullOrEmpty(controlName)) - controlName = BOOGIE_DUMMY_CONTROL + dummyControlNameIndex++; - - enabled = inputLine[ENABLED_FIELD].Trim(); - visibility = inputLine[VISIBILITY_FIELD].Trim(); - clickHandler = inputLine[CLICK_HANDLER_FIELD].Trim(); - checkedHandler = inputLine[CHECKED_HANDLER_FIELD].Trim(); - uncheckedHandler = inputLine[UNCHECKED_HANDLER_FIELD].Trim(); - selectionChangedHandler = inputLine[SELECTIONCHANGED_HANDLER_FIELD].Trim(); - bplName = inputLine[BPL_NAME_FIELD].Trim(); - - try { - pageStr = pageStructureInfo[pageClass]; - } catch (KeyNotFoundException) { - pageStr = new PageStructure(); - pageStr.PageClassName = pageClass; - pageStr.PageXAML = pageXAML; - pageStr.PageBoogieName = pageBoogieStringName; - pageStr.IsMainPage = false; - } - - controlInfoStr= pageStr.getControlInfo(controlName); - if (controlInfoStr == null) { - controlInfoStr = new ControlInfoStructure(); - controlInfoStr.Name = controlName; - controlInfoStr.ClassName = controlClass; - controlInfoStr.BplName = bplName; - } - controlInfoStr.IsEnabled = enabled.ToLower() == "false" ? false : true; - controlInfoStr.Visible = visibility == "Collapsed" ? Visibility.Collapsed : Visibility.Visible; - controlInfoStr.setHandler(Event.Click, clickHandler); - controlInfoStr.setHandler(Event.Checked, checkedHandler); - controlInfoStr.setHandler(Event.Unchecked, uncheckedHandler); - controlInfoStr.setHandler(Event.SelectionChanged, selectionChangedHandler); - - pageStr.setControlInfo(controlName, controlInfoStr); - pageStructureInfo[pageClass] = pageStr; - configLine = configStream.ReadLine(); - } - - setPageAsMainPage(mainPageXAML); - } - - public IEnumerable getControlsForPage(string pageClass) { - try { - return pageStructureInfo[pageClass].getAllControlsInfo(); - } catch (KeyNotFoundException) { - return null; - } - } - - public string getXAMLForPage(string pageClass) { - try { - return pageStructureInfo[pageClass].PageXAML; - } catch (KeyNotFoundException) { - return null; - } - } - - public bool getIsEnabled(string pageClass, string controlName) { - try { - return pageStructureInfo[pageClass].getControlInfo(controlName).IsEnabled; - } catch (KeyNotFoundException) { - //TODO not really correct - return false; - } - } - - public Visibility getVisibility(string pageClass, string controlName) { - try { - return pageStructureInfo[pageClass].getControlInfo(controlName).Visible; - } catch (KeyNotFoundException) { - // TODO not really correct - return default(Visibility); - } - } - - public IList 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); - - try { - return pageStructureInfo[pageClass].getControlInfo(controlName).getHandlers((Event) Event.Parse(typeof(Event), eventName)); - } catch (KeyNotFoundException) { - return null; - } - } - - public IEnumerable getPageXAMLFilenames() { - HashSet pageXAMLs = new HashSet(); - foreach (string name in this.pageStructureInfo.Keys) { - if (!name.EndsWith("__dummy")) - pageXAMLs.Add(pageStructureInfo[name].PageXAML); - } - - return pageXAMLs; - } - } -} diff --git a/TranslationPlugins/TranslationPlugins.csproj b/TranslationPlugins/TranslationPlugins.csproj index 9a27e94..9a59a60 100644 --- a/TranslationPlugins/TranslationPlugins.csproj +++ b/TranslationPlugins/TranslationPlugins.csproj @@ -40,7 +40,6 @@ -