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         appList1.append(app.strip())
  28 extractAppList.close()
  29
  30 # Try to create pairs
  31 appPairs = []
  32 # Extract the second list if provided (this is for combinations between two lists)
  33 if (len(sys.argv) == 6):
  34         secondList = sys.argv[5]
  35         extractAppList = open(secondList, "r")
  36         for app in extractAppList:
  37                 appList2.append(app.strip())
  38         extractAppList.close()
  39 # Just copy the first list to the second list
  40 else:
  41         appList2 = appList1
  42
  43 # Generate the permutations of pairs
  44 for i in range(len(appList1)):
  45         for j in range(i + 1, len(appList2)):
  46                 appPairs.append((appList1[i], appList2[j]))
  47
  48 # PART 2:
  49 print "PHASE 2: Running JPF ...\n"
  50 for item in appPairs:
  51         # Copy apps into Extractor/App1 and Extractor/App2
  52         os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy")
  53         os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy")
  54
  55         # Run Runner.py to extract things and create main.groovy, then compile it
  56         print "==> Compiling the apps ...\n"
  57         os.system("make Runner")
  58         os.system("make main")
  59
  60         # Call JPF
  61         print "==> Calling JPF and generate logs ...\n"
  62         os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + item[0] + "--" + item[1] + ".log" + " main.jpf")