1#!/usr/bin/python 2""" 3Will run two vampires in parallel and compare their output. 4Attempts to change the memory alignment of the second vampire by 5creating a lot of environment variables (this should make stack 6start from a different place in memory). 7 8Command line: 9[-p] [-a alternative_executable] executable arg1 ... 10 11default alternative_executable is the same as executable 12 13Runs in parallel 14executable arg1 ... 15alternative_executable arg1 ... 16and prints out a message when their outputs start to differ. 17 18"-p" will cause the outputs to be printed out even if they do not 19differ. 20 21This script is particularly useful in combination with the "-tr" 22options of Vampire which enable tracing ouputs. For example, 23"-tr sa" prints out details of all newly generated, processed, 24activated and simplified clauses. List of all possible arguments 25to the "-tr" option can be obtained by running "-tr help". 26 27""" 28 29import sys 30import platform 31import subprocess 32import re 33import time 34import tempfile 35import os 36import math 37 38vampCmdLine = None 39printTraces = False 40altExecutable = None 41errFollowUpLines = 5 42 43def readArgs(args): 44 global vampCmdLine 45 global printTraces 46 global altExecutable 47 48 while True: 49 if args[0]=="-p": 50 printTraces = True 51 args = args[1:] 52 if args[0]=="-a": 53 altExecutable = args[1] 54 args = args[2:] 55 else: 56 break 57 vampCmdLine = args 58 59class Finished(Exception): 60 def __init__(self, msg): 61 self.msg = msg 62 63readArgs(sys.argv[1:]) 64 65def createVampProc(isSecond): 66 global vampCmdLine 67 global altExecutable 68 69 childEnv = os.environ 70 cmdLine = list(vampCmdLine) 71 if isSecond: 72 #we try to make the second Vampire behave differently, so we put some large stuff 73 #into the system environment, which could change the memory alignment a bit 74 childEnv = dict(childEnv) 75 s = "a" 76 for i in range(0,12): 77 s = s+s 78 childEnv["abcd"] = s 79 #we also use the alternative executable if it was supplied 80 if altExecutable: 81 cmdLine[0] = altExecutable 82 try: 83 return subprocess.Popen(cmdLine, bufsize=1, stderr=subprocess.PIPE, env=childEnv) 84 except OSError: 85 print "Command line giving error:" 86 print cmdLine 87 raise 88 89def trimEOL(str): 90 if str[-1]=="\n": 91 return str[:-1] 92 else: 93 return str 94 95def printFollowUp(hdr, firstLine, proc): 96 global errFollowUpLines 97 98 print "%s: %s" % (hdr, trimEOL(firstLine)) 99 for i in range(0,errFollowUpLines): 100 ln = proc.stderr.readline() 101 if not ln: 102 print "%s terminated" % hdr 103 break 104 print "%s: %s" % (hdr, trimEOL(ln)) 105 106 107vp1 = createVampProc(False) 108vp2 = createVampProc(True) 109 110try: 111 while True: 112 ln1 = vp1.stderr.readline() 113 ln2 = vp2.stderr.readline() 114 115 if ln1==ln2: 116 if not ln1: 117 raise Finished("Both vampires terminated") 118 119 if printTraces: 120 print trimEOL(ln1) 121 122 continue 123 if not ln1: 124 raise Finished("First vampire terminated") 125 if not ln2: 126 raise Finished("Second vampire terminated") 127 128 if ln2[0:len(ln1)]==ln1 and vp1.poll(): 129 print "v1: %s" % trimEOL(ln1) 130 print "v2: %s" % trimEOL(ln2) 131 raise Finished("First vampire terminated in the middle of a line") 132 if ln1[0:len(ln2)]==ln2 and vp2.poll(): 133 print "v1: %s" % trimEOL(ln1) 134 print "v2: %s" % trimEOL(ln2) 135 raise Finished("Second vampire terminated in the middle of a line") 136 137 138 print "Vampire outputs differ:" 139 print 140 print "v1: %s" % trimEOL(ln1) 141 print "v2: %s" % trimEOL(ln2) 142 143 if errFollowUpLines: 144 print 145 printFollowUp("v1", ln1, vp1) 146 print 147 printFollowUp("v2", ln2, vp2) 148 print 149 raise Finished("Non-determinism detected") 150except Finished as e: 151 print e.msg 152finally: 153 if vp1.poll()==None: 154 vp1.kill() 155 if vp2.poll()==None: 156 vp2.kill() 157 158