ModelCheck.py

   1 #!/usr/bin/python
   2
   3 import itertools
   4 import sys
   5 import os
   6
   7 # Input parameters:
   8 # - JPF directory
   9 # - JPF logs directory
  10 # - app directory
  11 # - list #1
  12 # - list #2 (if needed)
  13
  14 # Index 0 is always for the Python script itself
  15 jpfDir = sys.argv[1]
  16 jpfLogDir = sys.argv[2]
  17 appDir = sys.argv[3]
  18 firstList = sys.argv[4]
  19
  20 # PART 1: Generate the permutations of app pairs
  21 print "PHASE 1: Extracting the app pairs from the app lists ...\n"
  22 appList1 = []
  23 appList2 = []
  24 # Extract the first list
  25 extractAppList = open(firstList, "r")
  26 for app in extractAppList:
  27         if '#' not in app:
  28                 appList1.append(app.strip())
  29 extractAppList.close()
  30
  31 # Try to create pairs
  32 appPairs = []
  33 # Extract the second list if provided (this is for combinations between two lists)
  34 if (len(sys.argv) == 6):
  35         secondList = sys.argv[5]
  36         extractAppList = open(secondList, "r")
  37         for app in extractAppList:
  38                 if '#' not in app:
  39                         appList2.append(app.strip())
  40         extractAppList.close()
  41 # Just copy the first list to the second list
  42 else:
  43         appList2 = appList1
  44
  45 # Generate the permutations of pairs
  46 for i in range(len(appList1)):
  47         for j in range(i + 1, len(appList2)):
  48                 appPairs.append((appList1[i], appList2[j]))
  49
  50 # PART 2:
  51 print "PHASE 2: Running JPF ...\n"
  52 # List down all the log file names
  53 writeLogList = open(jpfLogDir + "logList", "w+")
  54 for item in appPairs:
  55
  56         # Copy apps into Extractor/App1 and Extractor/App2
  57         os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy")
  58         os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy")
  59
  60         # Run Runner.py to extract things and create main.groovy, then compile it
  61         print "==> Compiling the apps ...\n"
  62         os.system("make Runner")
  63         os.system("make main")
  64
  65         # Call JPF
  66         print "==> Calling JPF and generate logs ...\n"
  67         logName = jpfLogDir + item[0] + "--" + item[1] + ".log"
  68         writeLogList.write(logName + "\n")
  69         os.system("cd " + jpfDir + ";./run.sh " + logName + " main.jpf")
  70
  71 writeLogList.close()