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 print "Got here!"
  62 appList1 = []
  63 appList2 = []
  64 # Extract the first list
  65 extractAppList = open(firstList, "r")
  66 for app in extractAppList:
  67         if '#' not in app:
  68                 appList1.append(app.strip())
  69 extractAppList.close()
  70
  71 # Try to create pairs
  72 appPairs = []
  73 useSecondList = False
  74 # Extract the second list if provided (this is for combinations between two lists)
  75 if (len(sys.argv) == 6):
  76         secondList = sys.argv[5]
  77         extractAppList = open(secondList, "r")
  78         for app in extractAppList:
  79                 if '#' not in app:
  80                         appList2.append(app.strip())
  81         extractAppList.close()
  82         useSecondList = True
  83 # Just copy the first list to the second list
  84 else:
  85         appList2 = appList1
  86
  87 if useSecondList is False:
  88         # Generate the permutations of pairs
  89         for i in range(len(appList1)):
  90                 for j in range(i + 1, len(appList2)):
  91                         appPairs.append((appList1[i], appList2[j]))
  92 else:
  93         # Generate pairs from 2 lists
  94         for i in range(len(appList1)):
  95                 for j in range(len(appList2)):
  96                         # Skip if both are the same
  97                         if appList1[i] == appList2[j]:
  98                                 continue
  99                         appPairs.append((appList1[i], appList2[j]))
 100
 101
 102 # PART 2:
 103 print "PHASE 2: Running JPF ...\n"
 104 # List down all the log file names
 105 writeLogList = open(jpfLogDir + "logList", "w+")
 106 for item in appPairs:
 107
 108         # Copy apps into Extractor/App1 and Extractor/App2
 109         print "==> First app: %s" % item[0]
 110         print "==> Second app: %s" % item[1]
 111         os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy")
 112         os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy")
 113
 114         # Run Runner.py to extract things and create main.groovy, then compile it
 115         print "==> Compiling the apps ...\n"
 116         os.system("make Runner")
 117         error = extractError()
 118         logName = item[0] + "--" + item[1] + ".log"
 119         if error == "":
 120                 # Compile
 121                 os.system("make main")
 122                 # Call JPF
 123                 print "==> Calling JPF and generate logs ...\n"
 124                 os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + logName + " main.jpf")
 125         else:
 126                 # This is for specific error, e.g., direct-direct interaction that we need to skip
 127                 writeErrorLog(jpfLogDir, logName, error)
 128
 129         result = checkResult(jpfLogDir + logName)
 130         writeLogList.write(logName + "\t\t" + result + "\n")
 131
 132 writeLogList.close()
 133
 134
 135
 136
 137
 138
 139
 140
 141
 142
 143
 144
 145
 146
 147