diff options
author | Daniel Dunbar <daniel@zuster.org> | 2010-05-02 17:59:13 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2010-05-02 17:59:13 +0000 |
commit | f4cdc443fb86f715ab93f3528aff23452a5bb3a3 (patch) | |
tree | ffab5077611d32a8b95c9d9b4f96b47703190e82 | |
parent | bae2fa50234b0a575a18a119019e5d96f7ff7ecf (diff) | |
download | klee-f4cdc443fb86f715ab93f3528aff23452a5bb3a3.tar.gz |
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 Binary files differdiff --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 Binary files differ |