From ad3d0b71e79f1943a0f2eb8792592075af44d5e4 Mon Sep 17 00:00:00 2001 From: t-espave Date: Fri, 5 Aug 2011 16:53:22 -0700 Subject: (phone bct) nav graph building (mostly) automated --- BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs | 97 +++++++++++++++++++++++++ BCT/BytecodeTranslator/Program.cs | 17 ++--- 2 files changed, 103 insertions(+), 11 deletions(-) (limited to 'BCT/BytecodeTranslator') diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs index cd71e7cc..74c17f54 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs @@ -6,6 +6,7 @@ using Microsoft.Cci; using Bpl=Microsoft.Boogie; using TranslationPlugins; using Microsoft.Cci.MutableCodeModel; +using System.IO; namespace BytecodeTranslator.Phone { public static class UriHelper { @@ -244,6 +245,9 @@ namespace BytecodeTranslator.Phone { private const string BOOGIE_VAR_PREFIX = "__BOOGIE_"; public const string IL_CURRENT_NAVIGATION_URI_VARIABLE = IL_BOOGIE_VAR_PREFIX + "CurrentNavigationURI__"; public const string BOOGIE_CONTINUE_ON_PAGE_VARIABLE = BOOGIE_VAR_PREFIX + "ContinueOnPage__"; + public 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; } @@ -633,5 +637,98 @@ namespace BytecodeTranslator.Phone { 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; + int i=1, j=1; + foreach (string x1 in xamls) { + string startURIVar= sink.FindOrCreateConstant(x1).Name.ToLower(); + j = 1; + foreach (string x2 in xamls) { + string resultFile = sourceBPLFile + "_" + i + "_" + j + ".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); + j++; + } + i++; + } + + outputStream.Close(); + } + + + public static void 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.Length]; + Bpl.IdentifierExpr[] varExpr = new Bpl.IdentifierExpr[procInfo.Decl.InParams.Length]; + for (int i = 0; i < procInfo.Decl.InParams.Length; 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(); + 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 Bpl.ExprSeq(varExpr), new Bpl.IdentifierExprSeq())); + 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))); + builder.Add(assertEndPage); + Bpl.Implementation impl = + new Bpl.Implementation(Bpl.Token.NoToken, callerInfo.Decl.Name, new Bpl.TypeVariableSeq(), new Bpl.VariableSeq(), + new Bpl.VariableSeq(), new Bpl.VariableSeq(localVars), builder.Collect(Bpl.Token.NoToken), null, new Bpl.Errors()); + + sink.TranslatedProgram.TopLevelDeclarations.Add(impl); + } + + 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;} } } diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 231a21cf..e6f86e1f 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -323,31 +323,26 @@ namespace BytecodeTranslator { PhoneMethodInliningMetadataTraverser inlineTraverser = new PhoneMethodInliningMetadataTraverser(PhoneCodeHelper.instance()); inlineTraverser.findAllMethodsToInline(modules); - updateInlinedMethods(sink, inlineTraverser.getMethodsToInline()); + PhoneCodeHelper.updateInlinedMethods(sink, inlineTraverser.getMethodsToInline()); System.Console.WriteLine("Total methods seen: {0}, inlined: {1}", inlineTraverser.TotalMethodsCount, inlineTraverser.InlinedMethodsCount); } + string outputFileName = primaryModule.Name + ".bpl"; if (PhoneCodeHelper.instance().PhoneNavigationToggled) { - // TODO integrate into the pipeline and spit out the boogie code foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) { - System.Console.WriteLine(def.ToString()); + PhoneCodeHelper.addHandlerStubCaller(sink, def); } + + PhoneCodeHelper.instance().createQueriesBatchFile(sink, outputFileName); } - Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl"); + Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName); Prelude.Emit(writer); sink.TranslatedProgram.Emit(writer); writer.Close(); return 0; // success } - private 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)); - } - } - private static string NameUpToFirstPeriod(string name) { var i = name.IndexOf('.'); if (i == -1) -- cgit v1.2.3