Add a little hack for visualizing KLEE branching.

 - This consumes the treestream files produced with --write-paths or
   --write-sym-paths, and renders out the tree in a very ad-hoc funky way.
   Your mileage may vary! :)

Example image: http://klee.llvm.org/data/treegraph_example.jpg
Example movie: http://klee.llvm.org/data/treegraph_example.avi

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102869 91177308-0d34-0410-b5e6-96231b3b80d8

17 files changed, 1180 insertions, 0 deletions

diff --git a/utils/hacks/TreeGraphs/Animate.py b/utils/hacks/TreeGraphs/Animate.py
new file mode 100755
index 00000000..07f43756
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Animate.py
@@ -0,0 +1,55 @@
+#!/usr/bin/python
+
+import os
+import TreeGraph
+import Image
+
+def main():
+    from optparse import OptionParser
+    op = OptionParser("usage: %prog [options] <tree-stream-path> <output-directory>")
+    op.add_option('','--start', dest='startCount', type=int, default=10,
+                  help='number of paths to start animation at')
+    op.add_option('','--end', dest='endCount', type=int, default=1000,
+                  help='number of paths to start animation at')
+    op.add_option('','--stride', dest='countStride', type=int, default=10,
+                  help='number of paths to step by in each frame')
+    op.add_option('','--convert-to-jpg', dest='convertToJPG',
+                  action='store_true', default=False)
+    op.add_option('','--convert-to-rgb', dest='convertToRGB',
+                  action='store_true', default=False)
+    opts,args = op.parse_args()
+
+    if len(args) != 2:
+        parser.error('invalid number of arguments')
+
+    symPath,outputDir = args
+    if not os.path.exists(outputDir):
+        os.mkdir(outputDir)
+    
+    for frame,count in enumerate(range(opts.startCount, opts.endCount,
+                                     opts.countStride)):
+        print 'generating frame %d with path count %d...' % (frame+1, count)
+        pdf_path = os.path.join(outputDir, 'frame_%05d.pdf' % frame)
+        TreeGraph.makeTreeGraph(pdf_path, symPath, count)
+        if not opts.convertToJPG:
+            continue
+
+        jpg_path = os.path.join(outputDir, 'frame_%05d.jpg' % frame)
+        if not opts.convertToRGB:
+            os.system('convert "%s" "%s"' % (pdf_path, jpg_path))
+            continue
+
+        jpg_tmp_path = os.path.join(outputDir, 'frame_%05d_tmp.jpg' % frame)
+        os.system('convert "%s" "%s"' % (pdf_path, jpg_tmp_path))
+
+        img = Image.open(jpg_tmp_path)
+        img = img.convert('RGB')
+        img.save(jpg_path, quality=100)
+        
+if __name__=='__main__':
+    try:
+        main()
+    except:
+        import sys,traceback
+        traceback.print_exc(file= sys.__stdout__)
+        sys.__stdout__.flush()
diff --git a/utils/hacks/TreeGraphs/DumpTreeStream.py b/utils/hacks/TreeGraphs/DumpTreeStream.py
new file mode 100644
index 00000000..b3614c7c
--- /dev/null
+++ b/utils/hacks/TreeGraphs/DumpTreeStream.py
@@ -0,0 +1,48 @@
+#!/usr/bin/python
+
+from __future__ import division
+
+import sys, os, struct
+
+def getTreeStream(path):
+    data = open(path,'rb').read()
+    paths = { 0 : ''}
+    pos = 0
+    while pos<len(data):
+        id,tag = struct.unpack('II', data[pos:pos+8])
+        pos += 8
+        if tag&(1<<31):
+            child = tag ^ (1<<31)
+            paths[child] = paths[id]
+        else:
+            size = tag
+            paths[id] += data[pos:pos+size]
+            pos += size
+    if pos!=len(data):
+        raise IOError,'bad position'
+    return paths
+
+def writeTreeStream(path, output):
+    paths = getTreeSTream(path)
+    print 'Writing %d paths'%len(paths)
+    for i,data in paths.items():
+        if i!=0:
+            f = open('%s%04d'%(output,i), 'wb')
+            f.write(data)
+            f.close()
+            
+def main(args):
+    from optparse import OptionParser
+    op = OptionParser("usage: %prog input outputPrefix")
+    opts,args = op.parse_args()
+
+    input,outputPrefix = args
+
+    f = open(input,'rb')
+    data = f.read()
+    f.close()
+    writeTreeStream(data, outputPrefix)
+    
+if __name__=='__main__':
+    main(sys.argv)
+
diff --git a/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py b/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py
new file mode 100644
index 00000000..be03cc2f
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Canvas/__init__.py
@@ -0,0 +1,205 @@
+from __future__ import division

+

+###

+

+import math, os, random

+

+from Graphics.Geometry import vec2

+

+from reportlab.pdfgen import canvas

+#from reportlab.graphics import shapes

+from reportlab.pdfbase import pdfmetrics

+

+"""

+class Canvas:

+	def startDrawing(self, (w,h)):

+	def endDrawing(self):

+		

+	def getAspect(self):

+		

+	def setColor(self, r, g, b):

+	def setLineWidth(self, width):

+	def drawOutlineBox(self, x0, y0, x1, y1):

+	def drawFilledBox(self, x0, y0, x1, y1):

+	def drawFilledPolygon(self, pts):

+	def drawOutlineCircle(self, x, y, r):

+	def startDrawPoints(self):

+	def endDrawPoints(self):

+	def drawPoint(self, x, y):

+	def setPointSize(self, size):

+

+	def drawLine(self, a, b):

+	def drawLines(self, ptPairs):

+	def drawLineStrip(self, pts):

+

+	def pushTransform(self):

+	def popTransform(self):

+	def translate(self, x, y):

+	def scale(self, x, y):

+	def setFontSize(self, size):

+	def drawString(self, (x, y), text):

+"""

+

+class BaseCanvas:

+	def drawPoints(self, pts):

+		self.startDrawPoints()

+		for pt in pts:

+			self.drawPoint(pt)

+		self.endDrawPoints()

+		

+	def drawStringCentered(self, boxLL, boxUR, text):

+		ll,ur = self.getStringBBox(text)

+		stringSize = vec2.sub(ur,ll)

+		boxSize = vec2.sub(boxUR,boxLL)

+		deltaSize = vec2.sub(boxSize, stringSize)

+		halfDeltaSize = vec2.mulN(deltaSize, .5)

+		

+		self.drawString(vec2.add(boxLL,halfDeltaSize), text)

+

+	def getStringSize(self, string):

+		ll,ur = self.getStringBBox(string)

+		return vec2.sub(ur,ll)

+	

+class PdfCanvas(BaseCanvas):

+	def __init__(self, name, basePos=(300,400), baseScale=(250,250), pageSize=None):

+		self._font = 'Times-Roman'

+		self.c = canvas.Canvas(name, pagesize=pageSize)

+		self.pointSize = 1

+		self.scaleX = self.scaleY = 1

+		self.state = []

+		self.basePos = tuple(basePos)

+		self.baseScale = tuple(baseScale)

+		self.lastFontSizeSet = None

+		

+		self.kLineScaleFactor = 1.95

+		

+	def getAspect(self):

+		return 1.0,1.0

+		

+	def startDrawing(self):

+		self.pointSize = 1

+		self.scaleX = self.scaleY = 1

+		

+		self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1]))

+		self.scale(self.baseScale)

+

+		self.setColor(0,0,0)

+		self.setLineWidth(1)

+		self.setPointSize(1)

+

+	def finishPage(self):

+		self.c.showPage()

+

+		self.pointSize = 1

+		self.scaleX = self.scaleY = 1

+		

+		self.translate((self.basePos[0] + self.baseScale[0], self.basePos[1] + self.baseScale[1]))

+		self.scale(self.baseScale)

+

+		self.setColor(0,0,0)

+		self.setLineWidth(1)

+		self.setPointSize(1)

+		

+		if self.lastFontSizeSet is not None:

+			self.setFontSize(self.lastFontSizeSet)

+			

+	def endDrawing(self):

+		self.c.showPage()

+		self.c.save()

+		

+	def setColor(self, r, g, b):

+		self.c.setStrokeColorRGB(r,g,b)

+		self.c.setFillColorRGB(r,g,b)

+	def setLineWidth(self, width):

+		avgScale = (self.scaleX+self.scaleY)/2

+		self.c.setLineWidth(width/(self.kLineScaleFactor*avgScale))

+	def setPointSize(self, size):

+		avgScale = (self.scaleX+self.scaleY)/2

+		self.pointSize = size/(4*avgScale)

+

+	def drawOutlineBox(self, (x0, y0), (x1, y1)):

+		self.c.rect(x0, y0, x1-x0, y1-y0, stroke=1, fill=0)

+	def drawFilledBox(self, (x0, y0), (x1, y1)):

+		self.c.rect(x0, y0, x1-x0, y1-y0, stroke=0, fill=1)

+	def drawOutlineCircle(self, (x, y), r):

+		self.c.circle(x, y, r, stroke=1, fill=0)

+	def drawFilledCircle(self, (x, y), r):

+		self.c.circle(x, y, r, stroke=0, fill=1)

+	def drawFilledPolygon(self, pts):

+		p = self.c.beginPath()

+		p.moveTo(*pts[-1])

+		for x,y in pts:

+			p.lineTo(x,y)

+		self.c.drawPath(p, fill=1, stroke=0)

+	def drawOutlinePolygon(self, pts):

+		p = self.c.beginPath()

+		p.moveTo(* pts[0])

+		for x,y in pts[1:]:

+			p.lineTo(x,y)

+		p.close()

+		self.c.drawPath(p, fill=0, stroke=1)

+	def startDrawPoints(self):

+		pass

+	def endDrawPoints(self):

+		pass

+	def drawPoint(self, (x, y)):

+		self.c.circle(x, y, self.pointSize, stroke=0, fill=1)

+

+	def drawLine(self, a, b):

+		self.drawLines([(a,b)])

+	def drawLines(self, ptPairs):

+		p = self.c.beginPath()

+		for a,b in ptPairs:

+			p.moveTo(a[0],a[1])

+			p.lineTo(b[0],b[1])

+		self.c.drawPath(p)

+	def drawLineStrip(self, pts):

+		p = self.c.beginPath()

+		p.moveTo(pts[0][0],pts[0][1])

+		for pt in pts[1:]:

+			p.lineTo(pt[0],pt[1])

+		self.c.drawPath(p)

+	def drawBezier(self, (p0,p1,p2,p3)):

+		self.c.bezier(*(p0+p1+p2+p3))

+		

+	def pushTransform(self):

+		self.state.append( (self.scaleX,self.scaleY) )

+		self.c.saveState()

+	def popTransform(self):

+		self.c.restoreState()

+		self.scaleX,self.scaleY = self.state.pop()

+	def translate(self, (x, y)):

+		self.c.translate(x, y)

+	def rotate(self, angle):

+		self.c.rotate(angle*180/math.pi)

+	def scale(self, (x, y)):

+		self.scaleX *= x

+		self.scaleY *= y

+		self.c.scale(x, y)

+

+	def setFont(self, fontName):

+		self._font = {"Symbol":"Symbol",

+					 "Times":"Times-Roman"}.get(fontName,fontName)

+	def setFontSize(self, size):

+		self.lastFontSizeSet = size

+		avgScale = (self.scaleX+self.scaleY)/2

+		self.fontSize = size/(2*avgScale)

+		self.c.setFont(self._font, self.fontSize)

+#		self.c.setFont("Times-Roman", size/(2*avgScale))

+	def drawString(self, (x, y), text):

+		self.c.drawString(x, y, text)

+		

+	def drawOutlineString(self, (x,y), text):

+		t = self.c.beginText(x, y)

+		t.setTextRenderMode(1)

+		t.textLine(text)

+		t.setTextRenderMode(0)

+		self.c.drawText(t)

+

+	def getStringBBox(self, text):

+		font = pdfmetrics.getFont(self._font)

+		width = pdfmetrics.stringWidth(text, self._font, self.fontSize)

+		ll = (0,0)

+		ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize)

+		ur = (width, (1.0 - font.face.ascent/2048.)*self.fontSize)

+		return ll,ur

diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py b/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py
new file mode 100644
index 00000000..a600a64f
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/Intersect2D.py
@@ -0,0 +1,59 @@
+import vec2, math

+

+def intersectLineCircle((p, no), (C, r)):

+	x = vec2.sub(p,C)

+	b = 2.*vec2.dot(no, x)

+	c = vec2.sqr(x) - r*r

+	dist = b*b - 4*c

+	

+	if dist<0:

+		return None

+	else:

+		d = math.sqrt(dist)

+		t0 = (-b - d)*.5

+		t1 = (-b + d)*.5

+		return (t0,t1)

+	

+#def intersectLineCircle((lineP,lineN),(circleP,circleR)):

+#	dx,dy = vec2.sub(lineP,circleP)

+#	nx,ny = lineN

+#

+#	a =   (nx*nx + ny*ny)

+#	b = 2*(dx*nx + dy*ny)

+#	c =   (dx*dx + dy*dy) - circleR*circleR

+#	

+#	k = b*b - 4*a*c

+#	if k<0:

+#		return None

+#	else:

+#		d = math.sqrt(k)

+#		t1 = (-b - d)/2*a

+#		t0 = (-b + d)/2*a

+#		return t0,t1

+	

+def intersectCircleCircle(c0P, c0R, c1P, c1R):

+	v = vec2.sub(c1P, c0P)

+	d = vec2.length(v)

+	

+	R = c0R

+	r = c1R

+

+	try:	

+		x = (d*d - r*r + R*R)/(2*d)

+	except ZeroDivisionError:

+		if R<r:

+			return 'inside',()

+		elif r>R:

+			return 'outside',()

+		else:

+			return 'coincident',()

+	

+	k = R*R - x*x

+	if k<0:

+		if x<0:

+			return 'inside',()

+		else:

+			return 'outside',()

+	else:

+		y = math.sqrt(k)

+		return 'intersect',(vec2.toangle(v),vec2.toangle((x,y)))

diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/__init__.py b/utils/hacks/TreeGraphs/Graphics/Geometry/__init__.py
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/__init__.py
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py
new file mode 100644
index 00000000..05320d5e
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat2.py
@@ -0,0 +1,20 @@
+import vec2

+

+def det(m):

+	((m00,m01),(m10,m11))= m

+	

+	return m00*m11 - m01*m10

+

+def mul(a,b):

+	b_trans= zip(* b)

+	return tuple([transmulvec2(b_trans, a_r) for a_r in a])

+

+	# multiple vector v by a transposed matrix

+def transmulvec2(m_trans,v):

+	return tuple([vec2.dot(v, m_c) for m_c in m_trans])

+

+def mulvec2(m,v):

+	return transmulvec2(zip(* m), v)

+

+def mulN(m,N):

+	return tuple([vec2.mulN(v,N) for v in m])

diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py
new file mode 100644
index 00000000..b8705a32
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat3.py
@@ -0,0 +1,40 @@
+import vec3,mat2

+

+def identity():

+	return ((1.0, 0.0, 0.0),

+			(0.0, 1.0, 0.0),

+			(0.0, 0.0, 1.0))

+

+def fromscale(scale):

+	x,y,z= scale

+	x,y,z= float(x),float(y),float(z)

+	return ((  x, 0.0, 0.0),

+			(0.0,   y, 0.0),

+			(0.0, 0.0,   z))

+def fromscaleN(n):

+	return fromscale((n,n,n))

+

+def mul(a,b):

+	b_trans= zip(* b)

+	return tuple([transmulvec3(b_trans, a_r) for a_r in a])

+

+	# multiple vector v by a transposed matrix

+def transmulvec3(m_trans,v):

+	return tuple([vec3.dot(v, m_c) for m_c in m_trans])

+

+def mulvec3(m,v):

+	return transmulvec3(zip(* m), v)

+

+def mulN(m,N):

+	return tuple([vec3.mulN(v,N) for v in m])

+

+def det(m):

+	((m00,m01,m02),

+	 (m10,m11,m12),

+	 (m20,m21,m22))= m

+

+	a= m00 * mat2.det( ((m11, m12), (m21, m22)) );

+	b= m10 * mat2.det( ((m01, m02), (m21, m22)) );

+	c= m20 * mat2.det( ((m01, m02), (m11, m12)) );

+	

+	return a-b+c

diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py b/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py
new file mode 100644
index 00000000..8dc7d35c
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/mat4.py
@@ -0,0 +1,153 @@
+import vec4,mat3

+

+def identity():

+	return ((1.0, 0.0, 0.0, 0.0),

+			(0.0, 1.0, 0.0, 0.0),

+			(0.0, 0.0, 1.0, 0.0),

+			(0.0, 0.0, 0.0, 1.0))

+

+def fromtrans(trans):

+	return ((1.0, 0.0, 0.0, 0.0),

+			(0.0, 1.0, 0.0, 0.0),

+			(0.0, 0.0, 1.0, 0.0),

+			(trans[0], trans[1], trans[2], 1.0))

+

+def fromscale(scale):

+	x,y,z= scale

+	x,y,z= float(x),float(y),float(z)

+	return ((  x, 0.0, 0.0, 0.0),

+			(0.0,   y, 0.0, 0.0),

+			(0.0, 0.0,   z, 0.0),

+			(0.0, 0.0, 0.0, 1.0))

+def fromscaleN(n):

+	return fromscale((n,n,n))

+

+def fromortho(left,right,bottom,top,znear,zfar):

+	m0= ( 2.0/(right-left), 0.0, 0.0, 0.0)

+	m1= (0.0,  2.0/(top-bottom), 0.0, 0.0)

+	m2= (0.0, 0.0, -2.0/(zfar-znear), 0.0)

+	m3= (	-((right+left)/(right-left)),

+			-((top+bottom)/(top-bottom)),

+			-((zfar+znear)/(zfar-znear)),

+			1.0)

+	return (m0,m1,m2,m3)

+

+def mulN(m,N):

+	return tuple([vec4.mulN(v,N) for v in m])

+	

+def mul(a,b):

+	b_trans= zip(* b)

+	return tuple([transmulvec4(b_trans, a_r) for a_r in a])

+

+	# multiple vector v by a transposed matrix

+def transmulvec4(m_trans,v):

+	return tuple([vec4.dot(v, m_c) for m_c in m_trans])

+

+def mulvec4(m,v):

+	return transmulvec4(zip(* m), v)

+	

+def trans(m):

+	((m00,m01,m02,m03),	

+	 (m10,m11,m12,m13),	

+	 (m20,m21,m22,m23),	

+	 (m30,m31,m32,m33))= m

+	 

+	return (	(m00,m10,m20,m30),	

+				(m01,m11,m21,m31),	

+				(m02,m12,m22,m32),	

+				(m03,m13,m23,m33))

+

+def det(m):

+	((m00,m01,m02,m03),	

+	 (m10,m11,m12,m13),	

+	 (m20,m21,m22,m23),	

+	 (m30,m31,m32,m33))= m

+	 

+	a= m00 * mat3.det(	((m11, m12, m13), 

+						 (m21, m22, m23), 

+						 (m31, m32, m33)) );

+	b= m10 * mat3.det(	((m01, m02, m03), 

+						 (m21, m22, m23), 

+						 (m31, m32, m33)) );

+	c= m20 * mat3.det(  ((m01, m02, m03), 

+						 (m11, m12, m13), 

+						 (m31, m32, m33)) );

+	d= m30 * mat3.det(	((m01, m02, m03), 

+						 (m11, m12, m13), 

+						 (m21, m22, m23)) );

+	

+	return a-b+c-d;

+

+def adj(m):

+	((m00,m01,m02,m03),	

+	 (m10,m11,m12,m13),	

+	 (m20,m21,m22,m23),	

+	 (m30,m31,m32,m33))= m

+	 

+	t00=  mat3.det( ((m11, m12, m13), 

+					 (m21, m22, m23),

+					 (m31, m32, m33)) )

+	t01= -mat3.det( ((m10, m12, m13), 

+					 (m20, m22, m23),

+					 (m30, m32, m33)) )

+	t02=  mat3.det( ((m10, m11, m13), 

+					 (m20, m21, m23),

+					 (m30, m31, m33)) )

+	t03= -mat3.det( ((m10, m11, m12), 

+					 (m20, m21, m22),

+					 (m30, m31, m32)) )

+

+

+	t10= -mat3.det( ((m01, m02, m03), 

+					 (m21, m22, m23),

+					 (m31, m32, m33)) )

+	t11=  mat3.det( ((m00, m02, m03), 

+					 (m20, m22, m23),

+					 (m30, m32, m33)) )

+	t12= -mat3.det( ((m00, m01, m03), 

+					 (m20, m21, m23),

+					 (m30, m31, m33)) )

+	t13=  mat3.det( ((m00, m01, m02), 

+					 (m20, m21, m22),

+					 (m30, m31, m32)) )

+

+	t20=  mat3.det( ((m01, m02, m03), 

+					 (m11, m12, m13),

+					 (m31, m32, m33)) )

+	t21= -mat3.det( ((m00, m02, m03), 

+					 (m10, m12, m13),

+					 (m30, m32, m33)) )

+	t22=  mat3.det( ((m00, m01, m03), 

+					 (m10, m11, m13),

+					 (m30, m31, m33)) )

+	t23= -mat3.det( ((m00, m01, m02), 

+					 (m10, m11, m12),

+					 (m30, m31, m32)) )

+

+	t30= -mat3.det( ((m01, m02, m03), 

+					 (m11, m12, m13),

+					 (m21, m22, m23)) )

+	t31=  mat3.det( ((m00, m02, m03), 

+					 (m10, m12, m13),

+					 (m20, m22, m23)) )

+	t32= -mat3.det( ((m00, m01, m03), 

+					 (m10, m11, m13),

+					 (m20, m21, m23)) )

+	t33=  mat3.det( ((m00, m01, m02), 

+					 (m10, m11, m12),

+					 (m20, m21, m22)) )

+					

+	return ((t00,t01,t02,t03),

+			(t10,t11,t12,t13),

+			(t20,t21,t22,t23),

+			(t30,t31,t32,t33))

+	

+def inv(m):

+	d= det(m)

+	t= trans(adj(m))

+	v= 1.0/d

+	return tuple([(a*v,b*v,c*v,d*v) for a,b,c,d in t])

+	

+def toGL(m):

+	m0,m1,m2,m3= m

+	return m0+m1+m2+m3
\ No newline at end of file
diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py b/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py
new file mode 100644
index 00000000..f7837891
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/quat.py
@@ -0,0 +1,107 @@
+from __future__ import division

+

+import math

+import vec3, vec4

+

+def identity():

+	return (0.0,0.0,0.0,1.0)

+

+def fromaxisangle(axisangle):

+	axis,angle= axisangle

+	ang_2= angle/2.0

+	s_ang= math.sin(ang_2)

+	c_ang= math.cos(ang_2)

+	

+	q= vec3.mulN(axis, s_ang) + (c_ang,)

+	return normalize(q)

+

+def fromnormals(n1,n2):

+	axis,angle= vec3.normalize(vec3.cross(n1, n2)), math.acos(vec3.dot(n1, n2))

+	return fromaxisangle((axis,angle))

+

+	# avoid trigonmetry

+def fromnormals_faster(n1,n2):

+	axis= vec3.normalize(vec3.cross(n1, n2))

+

+	half_n= vec3.normalize(vec3.add(n1, n2))

+	cos_half_angle= vec3.dot(n1, half_n)

+	sin_half_angle= 1.0 - cos_half_angle**2

+	

+	return vec3.mulN(axis, sin_half_angle) + (cos_half_angle,)

+

+def fromvectors(v1,v2):

+	return fromnormals(vec3.normalize(v1), vec3.normalize(v2))

+

+def magnitude(q):

+	return vec4.length(q)

+

+def normalize(q):

+	return vec4.divN(q, magnitude(q))

+

+def conjugate(q):

+	x,y,z,w= q

+	return (-x, -y, -z, w)

+

+def mulvec3(q, v):

+	t= mul(q, v+(0.0,))

+	t= mul(t, conjugate(q))

+	return t[:3]

+

+def mul(a, b):

+	ax,ay,az,aw= a

+	bx,by,bz,bw= b

+

+	x= aw*bx + ax*bw + ay*bz - az*by

+	y= aw*by + ay*bw + az*bx - ax*bz

+	z= aw*bz + az*bw + ax*by - ay*bx 

+	w= aw*bw - ax*bx - ay*by - az*bz

+

+	return (x,y,z,w)

+

+def toaxisangle(q):

+	tw= math.acos(q[3])

+	scale= math.sin(tw)

+	angle= tw*2.0

+

+	try:

+		axis= vec3.divN(q[:3], scale)

+	except ZeroDivisionError:

+		axis= (1.0,0.0,0.0)

+

+	return axis,angle

+

+def tomat3x3(q):

+	x,y,z,w= q

+

+	m0= (	1.0 -	2.0 * ( y*y + z*z ),

+					2.0 * ( x*y - z*w ),

+					2.0 * ( x*z + y*w ))

+	m1=	(			2.0 * ( x*y + z*w ),

+			1.0 -	2.0 * ( x*x + z*z ),

+					2.0 * ( y*z - x*w )) 

+	m2=	(			2.0 * ( x*z - y*w ),

+					2.0 * ( y*z + x*w ),

+			1.0 -	2.0 * ( x*x + y*y ))

+

+	return m0,m1,m2

+

+def tomat4x4(q):

+	m0,m1,m2= tomat3x3(q)

+	return (m0 + (0.0,),

+			m1 + (0.0,),

+			m2 + (0.0,),

+			(0.0, 0.0, 0.0, 1.0))

+

+def slerp(a, b, t):

+	raise NotImplementedError

+

+	cos_omega= vec4.dot(a, b)

+	

+	if (cos_omega<0.0):

+		cos_omega= -cos_omega

+		b= vec4.neg(b)

+

+	imega= math.acos(cos_omega)

+	t= sin(t*omega)/sin(omega)

+

+	return vec4.lerp(a, b, t)

diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py
new file mode 100644
index 00000000..80159043
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec2.py
@@ -0,0 +1,79 @@
+from __future__ import division

+from math import ceil,floor,sqrt,atan2,pi,cos,sin

+import random

+_abs,_min,_max= abs,min,max

+

+def random(rng=random):

+	return (rng.random()*2-1,rng.random()*2-1)

+

+def getangle(a):

+	x,y= a

+	if y>=0:

+		return atan2(y,x)

+	else:

+		return pi*2 + atan2(y,x)

+toangle = getangle

+

+def topolar(pt):

+	return getangle(pt),length(pt)

+def fromangle(angle,radius=1.):

+	return (cos(angle)*radius, sin(angle)*radius)

+frompolar = fromangle

+

+def rotate((x,y),angle):

+	c_a,s_a = cos(angle),sin(angle)

+	return (c_a*x - s_a*y, s_a*x + c_a*y)

+

+def rotate90((x,y)):

+	return (-y,x)

+	

+def abs(a): return (_abs(a[0]),_abs(a[1]))	

+def inv(a):	return (-a[0], -a[1])

+

+def add(a,b):	return (a[0]+b[0], a[1]+b[1])

+def sub(a,b):	return (a[0]-b[0], a[1]-b[1])

+def mul(a,b):	return (a[0]*b[0], a[1]*b[1])

+def div(a,b):	return (a[0]/b[0], a[1]/b[1])

+def mod(a,b):	return (a[0]%b[0], a[1]%b[1])

+def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1])

+

+def addN(a,n):	return (a[0]+n, a[1]+n)

+def subN(a,n):	return (a[0]-n, a[1]-n)

+def mulN(a,n):	return (a[0]*n, a[1]*n)

+def modN(a,n):	return (a[0]%n, a[1]%n)

+def divN(a,n):	return (a[0]/n, a[1]/n)

+

+def sqr(a):			return dot(a,a)

+def length(a):		return sqrt(sqr(a))

+def avg(a,b):		return mulN(add(a,b),0.5)

+def distance(a,b):	return length(sub(a,b))

+

+def normalize(a):

+	return mulN(a, 1.0/length(a))

+

+def normalizeOrZero(a):

+	try:

+		return mulN(a, 1.0/length(a))

+	except ZeroDivisionError:

+		return (0.0,0.0)

+	

+def min((a0,a1),(b0,b1)):

+	return (_min(a0,b0),_min(a1,b1))

+def max((a0,a1),(b0,b1)):

+	return (_max(a0,b0),_max(a1,b1))

+

+def lerp(a,b,t):

+	return add(mulN(a,1.0-t), mulN(b, t))

+

+def toint(a):

+	return (int(a[0]), int(a[1]))

+def tofloor(a):

+	return (floor(a[0]), floor(a[1]))

+def toceil(a):

+	return (ceil(a[0]), ceil(a[1]))

+

+def sumlist(l):

+	return reduce(add, l)

+def avglist(l):

+	return mulN(sumlist(l), 1.0/len(l))

+

diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py
new file mode 100644
index 00000000..ed4d8114
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec3.py
@@ -0,0 +1,55 @@
+from __future__ import division

+from math import ceil,floor,sqrt

+from random import random as _random

+_min,_max= min,max

+

+def random():

+	return (_random()*2-1,_random()*2-1,_random()*2-1)

+

+def inv(a):	return (-a[0],-a[1],-a[2])

+

+def add(a,b):	return (a[0]+b[0], a[1]+b[1], a[2]+b[2])

+def sub(a,b):	return (a[0]-b[0], a[1]-b[1], a[2]-b[2])

+def mul(a,b):	return (a[0]*b[0], a[1]*b[1], a[2]*b[2])

+def div(a,b):	return (a[0]/b[0], a[1]/b[1], a[2]/b[2])

+def mod(a,b):	return (a[0]%b[0], a[1]%b[1], a[2]%b[2])

+def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2])

+

+def addN(a,n):	return (a[0]+n, a[1]+n, a[2]+n)

+def subN(a,n):	return (a[0]-n, a[1]-n, a[2]-n)

+def mulN(a,n):	return (a[0]*n, a[1]*n, a[2]*n)

+def modN(a,n):	return (a[0]%n, a[1]%n, a[2]%n)

+def divN(a,n):	return (a[0]/n, a[1]/n, a[2]/n)

+

+def sqr(a):			return dot(a,a)

+def length(a):		return sqrt(sqr(a))

+def normalize(a):	return mulN(a, 1.0/length(a))

+def avg(a,b):		return mulN(add(a,b),0.5)

+def distance(a,b):	return length(sub(a,b))

+

+def cross(a, b):

+	return (a[1]*b[2] - a[2]*b[1],

+			a[2]*b[0] - a[0]*b[2],

+			a[0]*b[1] - a[1]*b[0])

+def reflect(a, b):

+	return sub(mulN(b, dot(a, b)*2), a)

+

+def lerp(a,b,t):

+	return add(mulN(a,1.0-t), mulN(b, t))

+

+def min((a0,a1,a2),(b0,b1,b2)):

+	return (_min(a0,b0),_min(a1,b1),_min(a2,b2))

+def max((a0,a1,a2),(b0,b1,b2)):

+	return (_max(a0,b0),_max(a1,b1),_max(a2,b2))

+

+def toint(a):

+	return (int(a[0]), int(a[1]), int(a[2]))

+def tofloor(a):

+	return (floor(a[0]), floor(a[1]), floor(a[2]))

+def toceil(a):

+	return (ceil(a[0]), ceil(a[1]), ceil(a[2]))

+

+def sumlist(l):

+	return reduce(add, l)

+def avglist(l):

+	return mulN(sumlist(l), 1.0/len(l))

diff --git a/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py b/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py
new file mode 100644
index 00000000..3a542272
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/Geometry/vec4.py
@@ -0,0 +1,46 @@
+from __future__ import division

+from math import ceil,floor,sqrt

+import vec3

+_min,_max= min,max

+

+def inv(a):	return (-a[0], -a[1], -a[2], -a[3])

+

+def add(a,b):	return (a[0]+b[0], a[1]+b[1], a[2]+b[2], a[3]+b[3])

+def sub(a,b):	return (a[0]-b[0], a[1]-b[1], a[2]-b[2], a[3]-b[3])

+def mul(a,b):	return (a[0]*b[0], a[1]*b[1], a[2]*b[2], a[3]*b[3])

+def div(a,b):	return (a[0]/b[0], a[1]/b[1], a[2]/b[2], a[3]/b[3])

+def mod(a,b):	return (a[0]%b[0], a[1]%b[1], a[2]%b[2], a[3]%b[3])

+def dot(a,b):	return (a[0]*b[0]+ a[1]*b[1]+ a[2]*b[2]+ a[3]*b[3])

+

+def addN(a,n):	return (a[0]+n, a[1]+n, a[2]+n, a[3]+n)

+def subN(a,n):	return (a[0]-n, a[1]-n, a[2]-n, a[3]-n)

+def mulN(a,n):	return (a[0]*n, a[1]*n, a[2]*n, a[3]*n)

+def modN(a,n):	return (a[0]%n, a[1]%n, a[2]%n, a[3]%n)

+def divN(a,n):	return (a[0]/n, a[1]/n, a[2]/n, a[3]/n)

+

+def sqr(a):		return dot(a,a)

+def length(a):	return sqrt(sqr(a))

+def avg(a,b):	return mulN(add(a,b),0.5)

+def normalize(a):	return mulN(a, 1.0/length(a))

+

+def lerp(a,b,t):

+	return add(mulN(a,1.0-t), mulN(b, t))

+

+def min((a0,a1,a2,a3),(b0,b1,b2,b3)):

+	return (_min(a0,b0),_min(a1,b1),_min(a2,b2),_min(a3,b3))

+def max((a0,a1,a2,a3),(b0,b1,b2,b3)):

+	return (_max(a0,b0),_max(a1,b1),_max(a2,b2),_max(a3,b3))

+

+def toint(a):

+	return (int(a[0]), int(a[1]), int(a[2]), int(a[3]))

+def tofloor(a):

+	return (floor(a[0]), floor(a[1]), floor(a[2]), floor(a[3]))

+def toceil(a):

+	return (ceil(a[0]), ceil(a[1]), ceil(a[2]), ceil(a[3]))

+def tovec3(a):

+	return vec3.divN(a, a[3])

+

+def sumlist(l):

+	return reduce(add, l)

+def avglist(l):

+	return mulN(sumlist(l), 1.0/len(l))

diff --git a/utils/hacks/TreeGraphs/Graphics/__init__.py b/utils/hacks/TreeGraphs/Graphics/__init__.py
new file mode 100644
index 00000000..4055b3ef
--- /dev/null
+++ b/utils/hacks/TreeGraphs/Graphics/__init__.py
@@ -0,0 +1 @@
+__all__= ['Formats', 'SubSurf', 'Geometry', 'AqsisInterface', 'TwoD', 'ThreeD', 'Apps']

diff --git a/utils/hacks/TreeGraphs/README.txt b/utils/hacks/TreeGraphs/README.txt
new file mode 100644
index 00000000..e650f571
--- /dev/null
+++ b/utils/hacks/TreeGraphs/README.txt
@@ -0,0 +1,17 @@
+A little hack which converts KLEE treestream's of path branch information into
+images/animations. It is not particularly fast nor is the code very
+elegant. It's a hack, after all!
+
+There are a couple example input streams in inputs/. You can generate a single
+image frame with, e.g.::
+
+  $ ./TreeGraph.py --count=500 inputs/symPaths6.ts t.pdf
+
+which will generate an image of the first 500 paths that were explored.
+
+
+You can generate a sequence of frames from a file using::
+
+  $ ./Animate.py --start=10 --end=2000 inputs/symPaths6.ts anim-01
+
+which will generate a sequence of .pdf frames in anim-01.
diff --git a/utils/hacks/TreeGraphs/TreeGraph.py b/utils/hacks/TreeGraphs/TreeGraph.py
new file mode 100755
index 00000000..28bd9fd6
--- /dev/null
+++ b/utils/hacks/TreeGraphs/TreeGraph.py
@@ -0,0 +1,295 @@
+#!/usr/bin/python
+
+from __future__ import division
+import sys
+from types import GeneratorType
+
+import DumpTreeStream
+from Graphics.Canvas import PdfCanvas
+from Graphics.Geometry import vec2
+import os, time
+import math, os, random
+
+def generator_fold(it):
+    """generator_fold(it) -> iterator
+
+    Given _it_, return a new iterator over the elements of _it_,
+    (recursively) folding in any elements whenever an iterator
+    result happens to also be a generator. This simplifies the
+    writing of iterators over recursive data structures.
+    """
+   
+    for res in it:
+        if isinstance(res,GeneratorType):
+            for res in generator_fold(res):
+                yield res
+        else:
+            yield res
+
+                
+def drawTree(a, b, maxDepth, sizes, depth=0):
+    yield (a, b)
+    if depth<maxDepth:
+        height = sizes[depth]
+        yield drawTree(b, vec2.add(b, (-height,height)),
+                       maxDepth, sizes, depth+1)
+        yield drawTree(b, vec2.add(b, (+height,height)),
+                       maxDepth, sizes, depth+1)
+    
+def makeTreeGraph(output, symPath, count, shuffle=False):
+    random.seed(10)
+    c = PdfCanvas(output, basePos=(0,0), baseScale=(72*5,72*5),
+                  pageSize=(72*10,72*10))
+
+    c.startDrawing()
+    c.setColor(1,1,1)
+    c.drawFilledCircle((0,0),.9)
+    c.setColor(0,0,0)
+    c.setLineWidth(5)
+    c.drawOutlineCircle((0,0),.9)
+    c.setLineWidth(1)
+#    c.setColor(.2,.6,.3)
+
+    N = 8
+    sizes = [.5**(i+1) for i in range(N)]
+    res = drawTree((0.,-.9), (0.,-.5), N, [1.3*s/sum(sizes) for s in sizes])
+#    [c.drawLine(a,b) for a,b in generator_fold(res)]
+
+    def mapIt(center, radius, spanAngle, (x,y)):
+        a = vec2.sub(center,(0,radius))
+        b = vec2.add(center,vec2.fromangle(math.pi*.5 + 2*x*spanAngle, radius))
+        return vec2.lerp(a, b, y)
+    m = lambda pt: mapIt((0,0),.9,math.pi*.7, pt)
+    toBox = lambda pt: vec2.div(vec2.add(pt,(0.,.9)),
+                                      (2*1.3,1.7))
+    def lm((x,y)):
+        x,y = toBox((x,y))
+        N = 100
+        return m((x,1-math.log(1+(1-y**4),2)))
+        return m((x,(N**(1+y)-N)/(N**2-N)))
+        return m((x,y))
+#    c.drawOutlineBox((-.5,0),(.5,1))
+    
+    #[c.drawLine(lm(a),lm(b)) for a,b in generator_fold(res)]
+
+    spanAngle = math.pi*.9
+    zeroRad = vec2.length(vec2.sub(vec2.fromangle(math.pi*3/2,.9),
+                                   vec2.fromangle(math.pi*.5 + spanAngle,.9)))
+    oneRad = .9
+    if 0:
+        for i in range(N):
+            t = i/(N-1)
+            c.drawOutlineCircle(vec2.add((0.,-.9), (0.,t*.9)),
+                                zeroRad + (oneRad-zeroRad)*t)
+
+    def getTreePos(depth, maxDepth, index, ranges=None, depthOrder=None):
+        isoT = depth/(maxDepth-1)
+        isoCent = vec2.add((0.,-.9),(0.,isoT*.9))
+        isoRadius = zeroRad + (oneRad-zeroRad)*isoT        
+        total = 2**(depth+1)
+        #        isoSpanAngle = math.pi*.5 - vec2.toangle(vec2.sub(vec2.fromangle(math.pi*.5 + spanAngle,.9),
+        #                                             isoCent))
+        isoSpanAngle = math.pi*.1 + (math.pi*.7 - math.pi*.1)*isoT
+        if ranges:
+            min,max = ranges
+            if max[depth]==min[depth]:
+                x = 0.
+            else:
+                x = (index - min[depth])/(max[depth]-min[depth])
+        elif depthOrder:
+            idx = depthOrder[depth].index(index)
+            x = idx/(len(depthOrder[depth])-1)
+        else:
+            x = index/(total-1)
+        return vec2.add(isoCent,vec2.fromangle(math.pi*.5 + (2*x-1)*isoSpanAngle, isoRadius))
+
+    treeData = DumpTreeStream.getTreeStream(symPath)
+    treeDataItems = treeData.items()
+    treeDataItems.sort()
+
+    N = max([len(p) for _,p in treeDataItems])
+#    N = min(20,N)
+
+    minDepthIndex = [2**(i+1) for i in range(N)]
+    maxDepthIndex = [0 for i in range(N)]
+    depthIndices = [set() for i in range(N+2)]
+    for id,path in treeDataItems:
+        depth = -1
+        index = 0
+        for p in path[:N]:
+            depth += 1
+            index = index*2 + (p=='1')
+            depthIndices[depth].add(index)
+            if 1:
+                low = index*2
+                hi = index*2+1
+                mid = index*2 + .5
+                M = 5
+                for x in range(depth+1,min(N,depth+M)):
+                    t = (x-(depth+1))/(M-1)
+                    depthIndices[x].add(low + (mid-low)*t)
+                    depthIndices[x].add(hi + (mid-hi)*t)
+                    low *= 2
+                    hi *= 2 + 1
+                    mid = mid*2 + .5
+            else:
+                depthIndices[depth+1].add(index*2)
+                depthIndices[depth+1].add(index*2+1)
+                depthIndices[depth+2].add(index*2*2)
+                depthIndices[depth+2].add(index*4+3)
+            minDepthIndex[depth] = min(index,minDepthIndex[depth])
+            maxDepthIndex[depth] = max(index,maxDepthIndex[depth])
+    if 0:
+        for d in range(1,N)[::-1]:
+            minDepthIndex[d] = min(minDepthIndex[d-1]*2,minDepthIndex[d])
+            maxDepthIndex[d] = max(maxDepthIndex[d-1]*2,maxDepthIndex[d])
+    for d in range(N):
+        depthIndices[d] = list(depthIndices[d])
+        depthIndices[d].sort()
+
+    def drawPoints(list):
+        for pt in list:
+            c.drawPoint(pt)
+
+    def catmullRom1((p0,p1,p2,p3), t):
+        return (0.5 * ((        2*p1            ) +
+                       (  -p0        +   p2     ) * t +
+                       ( 2*p0 - 5*p1 + 4*p2 - p3) * t*t +
+                       (  -p0 + 3*p1 - 3*p2 + p3) * t*t*t))
+    def catmullRom2((p0,p1,p2,p3), t):
+        return (catmullRom1((p0[0],p1[0],p2[0],p3[0]),t),
+                catmullRom1((p0[1],p1[1],p2[1],p3[1]),t))
+
+    c.setLineWidth(2)
+#    c.setColor(.2,.6,.3)
+    lines = set()
+    segments = set()
+    segments2 = dict()
+    allPoints = set()
+    side = set()
+    paths = []
+
+    paths_to_draw = treeDataItems
+    if shuffle:
+        paths_to_draw = list(treeDataItems)
+        random.shuffle(paths_to_draw)
+
+    for id,path in paths_to_draw[:count]:
+        depth = -1
+        index = 0
+        pts = [(0.,-.9)]
+        for p in path[:N]:
+            depth += 1
+            index = index*2 + (p=='1')
+            pts.append(getTreePos(depth,N,index,None,depthIndices))
+            #            pts.append(getTreePos(depth,N,index,(minDepthIndex,maxDepthIndex)))
+        allPoints |= set(pts)
+        if len(pts)>3:
+            paths.append(pts)
+            for i in range(0,len(pts)-1):
+                p0 = pts[max(0,i-1)]
+                p1 = pts[i]
+                p2 = pts[min(len(pts)-1,i+1)]
+                p3 = pts[min(len(pts)-1,i+2)]
+                #segments[(p1,p2)] = segments.get((p1,p2),[]) + [(p0,p1)]
+                
+                if (p1,p2) not in side:
+                    segments.add((p0,p1,p2,p3))
+                    side.add((p1,p2))
+#                drawPoints((b,vec2.add(b,vec2.mulN(vec2.normalizeOrZero(vec2.sub(b,a)),l*.4)),
+#                              cx,cx))
+#        c.drawLineStrip(pts)
+#        for a,b in zip(pts,pts[1:]):
+#            lines.add((a,b))
+    for a,b in lines:
+        c.drawLine(a,b)
+    for (p1,p2),extra in segments2.items():
+        a,b = zip(*extra)
+        a = vec2.divN(reduce(vec2.add, a),len(a))
+        b = vec2.divN(reduce(vec2.add, b),len(b))
+        c.drawLineStrip([catmullRom2((a,p1,p2,b),x/10.) for x in range(10+1)])
+    if 1:
+        side = set()
+        nPaths = []
+        for path in paths:
+            path = list(path)
+            path = [(0.,-.9)] + path
+            depth = 0
+            while len(path)>3 and (path[1],path[2]) in side:
+                depth += 1
+                path = path[1:]
+            nPaths.append((depth,path))
+            side |= set(zip(path,path[1:]))
+#        for path in nPaths:
+#            c.drawLineStrip(path)
+        for depth,path in nPaths:
+            ppts = []
+            for i in range(1,len(path)-1):
+                p0 = path[max(0,i-1)]
+                p1 = path[i]
+                p2 = path[min(len(path)-1,i+1)]
+                p3 = path[min(len(path)-1,i+2)]
+                for x in range(10):
+                    ppts.append(catmullRom2((p0,p1,p2,p3),x/10.))
+                #ppts.append(p1)
+            ppts.append(path[-1])
+            if 1:
+                up = []
+                down = []
+                ref = path[0]
+                for i,pt in enumerate(ppts):
+                    ref = ppts[min(len(ppts)-1,i+1)]
+                    vec = vec2.sub(pt,ref)
+                    l = vec2.length(vec)
+                    if l<.000001:
+                        vec = (1.,0.)
+                    else:
+                        vec = vec2.rotate90(vec2.divN(vec,l))
+                    width = .001 * (1. - (depth + i/20.)/N)
+                    up.append(vec2.add(pt, vec2.mulN(vec, width)))
+                    down.append(vec2.add(pt, vec2.mulN(vec, -width)))
+                    ref = pt
+#                c.drawLineStrip(up)
+#                c.drawLineStrip(down)
+                c.drawFilledPolygon(down + up[::-1])
+            else:
+                c.drawLineStrip(ppts)
+#        print len(paths),sum(map(len,paths))
+#        print len(nPaths),sum(map(len,nPaths))
+    else:
+        for P in segments:
+            c.drawLineStrip([catmullRom2(P,x/10.) for x in range(10+1)])
+    if 0:
+        c.setPointSize(10)
+        c.drawPoints(allPoints)
+    
+    if 0:
+        N = 20
+        for i in range(N+1):        
+            t = 2*i/N - 1
+            c.drawLine(m((t,0)), m((t,1)))
+    
+    c.endDrawing()
+        
+def main():
+    from optparse import OptionParser
+    op = OptionParser("usage: %prog [options] <tree-stream-path> <output-path>")
+    op.add_option('','--count', dest='count', type=int, default=-1,
+                  help="number of distinct paths to draw")
+    op.add_option('','--shuffle', dest='shuffle', action='store_true',
+                  default=False)
+    opts,args = op.parse_args()
+
+    if len(args) != 2:
+        parser.error('invalid number of arguments')
+
+    symPath,output = args
+    makeTreeGraph(output, symPath, opts.count, opts.shuffle)
+    
+if __name__=='__main__':
+    try:
+        main()
+    except:
+        import sys,traceback
+        traceback.print_exc(file= sys.__stdout__)
+        sys.__stdout__.flush()
diff --git a/utils/hacks/TreeGraphs/inputs/symPaths.ts b/utils/hacks/TreeGraphs/inputs/symPaths.ts
new file mode 100644
index 00000000..05aaa763
--- /dev/null
+++ b/utils/hacks/TreeGraphs/inputs/symPaths.ts
diff --git a/utils/hacks/TreeGraphs/inputs/symPaths6.ts b/utils/hacks/TreeGraphs/inputs/symPaths6.ts
new file mode 100644
index 00000000..d67d66d5
--- /dev/null
+++ b/utils/hacks/TreeGraphs/inputs/symPaths6.ts