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