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 useSecondList = False
  34 # Extract the second list if provided (this is for combinations between two lists)
  35 if (len(sys.argv) == 6):
  36         secondList = sys.argv[5]
  37         extractAppList = open(secondList, "r")
  38         for app in extractAppList:
  39                 if '#' not in app:
  40                         appList2.append(app.strip())
  41         extractAppList.close()
  42         useSecondList = True
  43 # Just copy the first list to the second list
  44 else:
  45         appList2 = appList1
  46
  47 if useSecondList is False:
  48         # Generate the permutations of pairs
  49         for i in range(len(appList1)):
  50                 for j in range(i + 1, len(appList2)):
  51                         appPairs.append((appList1[i], appList2[j]))
  52 else:
  53         # Generate pairs from 2 lists
  54         for i in range(len(appList1)):
  55                         for j in range(len(appList2)):
  56                                 appPairs.append((appList1[i], appList2[j]))
  57
  58 # PART 2:
  59 print "PHASE 2: Running JPF ...\n"
  60 # List down all the log file names
  61 writeLogList = open(jpfLogDir + "logList", "w+")
  62 for item in appPairs:
  63
  64         # Copy apps into Extractor/App1 and Extractor/App2
  65         os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy")
  66         os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy")
  67
  68         # Run Runner.py to extract things and create main.groovy, then compile it
  69         print "==> Compiling the apps ...\n"
  70         os.system("make Runner")
  71         os.system("make main")
  72
  73         # Call JPF
  74         print "==> Calling JPF and generate logs ...\n"
  75         logName = jpfLogDir + item[0] + "--" + item[1] + ".log"
  76         writeLogList.write(logName + "\n")
  77         os.system("cd " + jpfDir + ";./run.sh " + logName + " main.jpf")
  78
  79 writeLogList.close()