From dc813534082811d6ed2f633717470e822a5887fc Mon Sep 17 00:00:00 2001 From: t-espave Date: Tue, 9 Aug 2011 11:50:40 -0700 Subject: (phone) fully automated phone nav graph building --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 4 +- BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs | 35 +++- BCT/BytecodeTranslator/Program.cs | 1 + BCT/PhoneControlsExtractor/navGraphBuilder.py | 227 ++++++++++++++++++++++++ 4 files changed, 265 insertions(+), 2 deletions(-) create mode 100644 BCT/PhoneControlsExtractor/navGraphBuilder.py (limited to 'BCT') diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index caa2c351..fdf5f4a3 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -743,7 +743,9 @@ namespace BytecodeTranslator /// private void TranslateHavocCurrentURI() { // TODO move away phone related code from the translation, it would be better to have 2 or more translation phases - Bpl.CallCmd havocCall = new Bpl.CallCmd(Bpl.Token.NoToken, PhoneCodeHelper.BOOGIE_DO_HAVOC_CURRENTURI, new List(), new List()); + 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); } diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs index 704d5669..2f818606 100644 --- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs +++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs @@ -646,7 +646,7 @@ namespace BytecodeTranslator.Phone { foreach (string x1 in xamls) { string startURIVar= sink.FindOrCreateConstant(x1).Name.ToLower(); foreach (string x2 in xamls) { - string resultFile = sourceBPLFile + "_" + x1 + "_" + x2 + ".bpl"; + 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); @@ -727,5 +727,38 @@ namespace BytecodeTranslator.Phone { } public static FieldDefinition CurrentURIFieldDefinition {get; set;} + + public void addNavigationUriHavocer(Sink sink) { + Sink.ProcedureInfo procInfo = sink.FindOrCreateProcedure(getUriHavocerMethod(sink).ResolvedMethod); + Bpl.StmtListBuilder builder= new Bpl.StmtListBuilder(); + Bpl.HavocCmd havoc= + new Bpl.HavocCmd(Bpl.Token.NoToken, + new Bpl.IdentifierExprSeq(new Bpl.IdentifierExprSeq(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 Bpl.TypeVariableSeq(), + new Bpl.VariableSeq(), new Bpl.VariableSeq(), new Bpl.VariableSeq(), + builder.Collect(Bpl.Token.NoToken)); + sink.TranslatedProgram.TopLevelDeclarations.Add(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; + } } } diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index c138b28a..382ad2ad 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -335,6 +335,7 @@ namespace BytecodeTranslator { foreach (IMethodDefinition def in PhoneNavigationCodeTraverser.NavCallers) { PhoneCodeHelper.addHandlerStubCaller(sink, def); } + PhoneCodeHelper.instance().addNavigationUriHavocer(sink); PhoneCodeHelper.instance().createQueriesBatchFile(sink, outputFileName); } diff --git a/BCT/PhoneControlsExtractor/navGraphBuilder.py b/BCT/PhoneControlsExtractor/navGraphBuilder.py new file mode 100644 index 00000000..c7df8037 --- /dev/null +++ b/BCT/PhoneControlsExtractor/navGraphBuilder.py @@ -0,0 +1,227 @@ +import sys +import getopt +import os + +BOOGIE_PATH= "%boogie%" +BCT_PATH="%boogie_bct%" +CONTROL_EXTRACTOR_PATH="%phonecontrolextractor%" +WPLIB_PATH="%wplib%" +DOT_PATH="%dotpath%" + +navigation_graph = {} + +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 + "\" > nul") + 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 createBoogieQueries(appFile, outputFile, format): + cmd ="\"" + os.path.dirname(appFile) + "\\createQueries.bat\" > nul" + error = os.system(cmd) + if error != 0: + return False + return True + +def runBoogieQueries(appFile, outputFile, format): + global navigation_graph + queryFiles= [os.path.abspath(filename) for filename in os.listdir(".") if filename.find("$$") != -1 and os.path.splitext(filename)[1]==".bpl"] + 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: + 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 + return True + +def buildNavigationGraph(appFile, outputFile, format): + global navigation_graph + 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 [width=\"0\" label=\"\"] n0;\n") + nextNode=1 + for pagename in navigation_graph.keys(): + dotFile.write("\tnode [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 + + 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(): + 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: + print "Extracting control information..." + if (not createAppControlsFile(appFile, outputFile, format)): + print "Failed to create app controls file" + sys.exit(1) + + if build=="" or build.find("i") != -1: + print "Injecting and translating application binary..." + if (not bctAppFile(appFile, outputFile, format)): + print "Failed to translate application library" + sys.exit(1) + + if build=="" or build.find("t") != -1: + print "Testing boogie file..." + if (not testBoogieOutput(appFile, outputFile, format)): + print "ByteCode Translator produced erroneous or ambiguous boogie file" + sys.exit(1) + + if build=="" or build.find("b") != -1: + print "Creating boogie queries..." + if (not createBoogieQueries(appFile, outputFile, format)): + print "Error creating boogie queries" + sys.exit(1) + + if build=="" or build.find("q") != -1: + print "Running boogie queries..." + if (not runBoogieQueries(appFile, outputFile, format)): + print "Error running boogie queries" + sys.exit(1) + + 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 -- cgit v1.2.3