ModelCheck.py

   1 #!/usr/bin/python
   2
   3 import itertools
   4 import sys
   5 import os
   6
   7 # Helper methods
   8 # Check the result in the log and print a summary
   9 def checkResult(logDirName):
  10         extractResult = open(logDirName, "r")
  11         result = "other errors--PLEASE CHECK!"
  12
  13         for line in extractResult:
  14                 if "no errors detected" in line:
  15                         result = "no conflict"
  16                         break
  17                 elif "java.lang.RuntimeException: Conflict between apps App1 and App2:" in line:
  18                         result = "conflict"
  19                         break
  20                 elif "Direct-Direct Interaction detected:" in line:
  21                         result = "direct-direct"
  22                         break
  23
  24         return result
  25
  26 # Extract the error from specific error logs
  27 def extractError():
  28         err = ""
  29         if os.path.exists("appCreationError.log"):
  30                 extractError = open("appCreationError.log", "r")
  31                 for line in extractError:
  32                         err = err + line
  33                 extractError.close()
  34                 os.system("rm appCreationError.log")
  35         return err
  36
  37 # Write error log to the log directory
  38 # In this case we skip running JPF
  39 # e.g., in the case of having a direct-direct interaction pair
  40 def writeErrorLog(jpfLogDir, logName, error):
  41         writeError = open(jpfLogDir + logName, "w+")
  42         writeError.write(error)
  43         writeError.close()
  44
  45 # Input parameters:
  46 # - JPF directory
  47 # - JPF logs directory
  48 # - app directory
  49 # - list #1
  50 # - list #2 (if needed)
  51
  52 # Index 0 is always for the Python script itself
  53 jpfDir = sys.argv[1]
  54 jpfLogDir = sys.argv[2]
  55 appDir = sys.argv[3]
  56 firstList = sys.argv[4]
  57
  58
  59 # PART 1: Generate the permutations of app pairs
  60 print "PHASE 1: Extracting the app pairs from the app lists ...\n"
  61 appList1 = []
  62 appList2 = []
  63 # Extract the first list
  64 extractAppList = open(firstList, "r")
  65 for app in extractAppList:
  66         if '#' not in app:
  67                 appList1.append(app.strip())
  68 extractAppList.close()
  69
  70 # Try to create pairs
  71 appPairs = []
  72 useSecondList = False
  73 # Extract the second list if provided (this is for combinations between two lists)
  74 if (len(sys.argv) == 6):
  75         secondList = sys.argv[5]
  76         extractAppList = open(secondList, "r")
  77         for app in extractAppList:
  78                 if '#' not in app:
  79                         appList2.append(app.strip())
  80         extractAppList.close()
  81         useSecondList = True
  82 # Just copy the first list to the second list
  83 else:
  84         appList2 = appList1
  85
  86 if useSecondList is False:
  87         # Generate the permutations of pairs
  88         for i in range(len(appList1)):
  89                 for j in range(i + 1, len(appList2)):
  90                         appPairs.append((appList1[i], appList2[j]))
  91 else:
  92         # Generate pairs from 2 lists
  93         for i in range(len(appList1)):
  94                 for j in range(len(appList2)):
  95                         # Skip if both are the same
  96                         if appList1[i] == appList2[j]:
  97                                 continue
  98                         appPairs.append((appList1[i], appList2[j]))
  99
 100
 101 # PART 2:
 102 print "PHASE 2: Running JPF ...\n"
 103 # List down all the log file names
 104 writeLogList = open(jpfLogDir + "logList", "w+")
 105 for item in appPairs:
 106
 107         # Copy apps into Extractor/App1 and Extractor/App2
 108         print "==> First app: %s" % item[0]
 109         print "==> Second app: %s" % item[1]
 110         os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy")
 111         os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy")
 112
 113         # Run Runner.py to extract things and create main.groovy, then compile it
 114         print "==> Compiling the apps ...\n"
 115         os.system("make Runner")
 116         error = extractError()
 117         logName = item[0] + "--" + item[1] + ".log"
 118         if error == "":
 119                 # Compile
 120                 os.system("make main")
 121                 # Call JPF
 122                 print "==> Calling JPF and generate logs ...\n"
 123                 os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + logName + " main.jpf")
 124         else:
 125                 # This is for specific error, e.g., direct-direct interaction that we need to skip
 126                 writeErrorLog(jpfLogDir, logName, error)
 127
 128         result = checkResult(jpfLogDir + logName)
 129         writeLogList.write(logName + "\t\t" + result + "\n")
 130
 131 writeLogList.close()
 132
 133
 134
 135
 136
 137
 138
 139
 140
 141
 142
 143
 144
 145
 146