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
  21         return result
  22
  23
  24 # Input parameters:
  25 # - JPF directory
  26 # - JPF logs directory
  27 # - app directory
  28 # - list #1
  29 # - list #2 (if needed)
  30
  31 # Index 0 is always for the Python script itself
  32 jpfDir = sys.argv[1]
  33 jpfLogDir = sys.argv[2]
  34 appDir = sys.argv[3]
  35 firstList = sys.argv[4]
  36
  37
  38 # PART 1: Generate the permutations of app pairs
  39 print "PHASE 1: Extracting the app pairs from the app lists ...\n"
  40 appList1 = []
  41 appList2 = []
  42 # Extract the first list
  43 extractAppList = open(firstList, "r")
  44 for app in extractAppList:
  45         if '#' not in app:
  46                 appList1.append(app.strip())
  47 extractAppList.close()
  48
  49 # Try to create pairs
  50 appPairs = []
  51 useSecondList = False
  52 # Extract the second list if provided (this is for combinations between two lists)
  53 if (len(sys.argv) == 6):
  54         secondList = sys.argv[5]
  55         extractAppList = open(secondList, "r")
  56         for app in extractAppList:
  57                 if '#' not in app:
  58                         appList2.append(app.strip())
  59         extractAppList.close()
  60         useSecondList = True
  61 # Just copy the first list to the second list
  62 else:
  63         appList2 = appList1
  64
  65 if useSecondList is False:
  66         # Generate the permutations of pairs
  67         for i in range(len(appList1)):
  68                 for j in range(i + 1, len(appList2)):
  69                         appPairs.append((appList1[i], appList2[j]))
  70 else:
  71         # Generate pairs from 2 lists
  72         for i in range(len(appList1)):
  73                 for j in range(len(appList2)):
  74                         # Skip if both are the same
  75                         if appList1[i] == appList2[j]:
  76                                 continue
  77                         appPairs.append((appList1[i], appList2[j]))
  78
  79
  80 # PART 2:
  81 print "PHASE 2: Running JPF ...\n"
  82 # List down all the log file names
  83 writeLogList = open(jpfLogDir + "logList", "w+")
  84 for item in appPairs:
  85
  86         # Copy apps into Extractor/App1 and Extractor/App2
  87         print "==> First app: %s" % item[0]
  88         print "==> Second app: %s" % item[1]
  89         os.system("cp " + appDir + item[0] + " Extractor/App1/App1.groovy")
  90         os.system("cp " + appDir + item[1] + " Extractor/App2/App2.groovy")
  91
  92         # Run Runner.py to extract things and create main.groovy, then compile it
  93         print "==> Compiling the apps ...\n"
  94         os.system("make Runner")
  95         os.system("make main")
  96
  97         # Call JPF
  98         print "==> Calling JPF and generate logs ...\n"
  99         logName = item[0] + "--" + item[1] + ".log"
 100         os.system("cd " + jpfDir + ";./run.sh " + jpfLogDir + logName + " main.jpf")
 101         result = checkResult(jpfLogDir + logName)
 102         writeLogList.write(logName + "\t\t" + result + "\n")
 103
 104 writeLogList.close()
 105
 106
 107
 108
 109
 110
 111
 112
 113
 114
 115
 116
 117
 118
 119
 120 <<<<<<< HEAD
 121 =======
 122
 123
 124
 125
 126
 127 >>>>>>> e378d6a65b25030f8914dc97f04b81ddff351d9c