solve_bug.py

import sys
#sys.path.append("C:\\Program Files (x86)\\Microsoft Research\\Z3-4.1\\python")
from z3 import *


s=Solver()

x=BitVec("x", 64)
y=BitVec("y", 64)
w=BitVec("w", 64)
h=BitVec("h", 64)

#s.add(x == 0x7fffffff)
#s.add(w == 0x10)
#s.add(y == 0x7fffffff)
#s.add(h == 0x10)

s.add(w > 0)
s.add(h > 0)


def clampToInteger(x):
  return If(x >= 0x7fffffff, BitVecVal(0x7fffffff, 32), If(x < -2147483648, BitVecVal(-2147483648, 32), Extract(31, 0, x)))

def convertToValidDeviceSize(w,h):
  cond=Or(w < 1, h < 1, h > 32767, w > 32767, w*h > (32768*8192))
  return (If(cond, 0, w), If(cond, 0, h))

#convertLogicalToDevice
left=clampToInteger(x)
top=clampToInteger(y)
right=clampToInteger(x+w)
s.add(Implies(x > 0, x+w > 0))
bottom=clampToInteger(y+h)
s.add(Implies(y > 0, y+h > 0))

w,h = convertToValidDeviceSize(right - left, bottom - top)
x=left
y=top

w=If(w < 1, BitVecVal(1, 32), w)
h=If(h < 1, BitVecVal(1, 32), h)

#getUnmultipliedImageData
faulty_conds=[]
faulty_explained=[]

buffersize=w*h*4
faulty_explained.append("integer overflow on buffersize calculation")
faulty_conds.append(buffersize/4/h != w)

faulty_explained.append("weird kind of integer overflow")
faulty_conds.append(buffersize < 0)


#suppose a canvas with max Skia size
msize_width=BitVecVal(32767, 32)
msize_height=BitVecVal(8192, 32)
canvas_size=msize_width*msize_height*4

memset_cond=Or(x < 0, y < 0, x+w > msize_width, y+h > msize_height)

originx=If(x < 0, BitVecVal(0, 32), x)
destx=If(x < 0, -x, 0)
endx=x+w;
endx=If(endx > msize_width, msize_width, endx)
numColumns = endx - originx

originy=If(y < 0, BitVecVal(0, 32), y)
desty=If(y < 0, -y, 0)
endy=y+h;
endy=If(endy > msize_height, msize_height, endy)
numRows = endy - originy

#bytes per row
fRowBytes=msize_width.as_long()*4
srcPixelsPerRow=rowBytesAsPixels=fRowBytes >> 2
destBytesPerRow=4 * w

#the for-loops over ints dont enter if any of this is true
noloop=Or(numRows <= 0, numColumns <= 0)
loop=Not(noloop)

srcRows_base=originy * fRowBytes + (originx << 2)

faulty_explained.append("reading from a negative address, something went wrong on the calculation")
faulty_conds.append(And(loop, srcRows_base < 0))

faulty_explained.append("reading outside the source buffer")
faulty_conds.append(And(loop, srcRows_base >= canvas_size))

destRows_base=desty * destBytesPerRow + destx * 4

faulty_explained.append("writing to a negative address, something went wrong on the calculation")
faulty_conds.append(And(loop, destRows_base < 0))

faulty_explained.append("start to write outside the buffer size")
faulty_conds.append(And(loop, destRows_base >= buffersize))

destRows_max=destRows_base + (destBytesPerRow * (numRows-1)) + (numColumns-1) * 4 + 3
srcRows_max=srcRows_base + (srcPixelsPerRow * (numRows-1)) + (numColumns-1) * 4

faulty_explained.append("finish writting outside the buffer")
faulty_conds.append(And(loop, destRows_max >= buffersize))

faulty_explained.append("negative final buffer address on destRows")
faulty_conds.append(And(loop, destRows_max < 0))

faulty_explained.append("negative final buffer address on srcRows")
faulty_conds.append(And(loop, srcRows_max < 0))

faulty_explained.append("end up reading from outside the canvas size")
faulty_conds.append(And(loop, srcRows_max >= canvas_size))

faulty_explained.append("srcRows end < start")
faulty_conds.append(And(loop, ULT(srcRows_max, srcRows_base)))
faulty_explained.append("destRows end < start")
faulty_conds.append(And(loop, ULT(destRows_max, destRows_base)))

faulty_explained.append("infoleak option 1: no memset and for-loop over a subset of the destination buffer")
faulty_conds.append(And(Not(memset_cond), Or(destRows_base > 0, destRows_max < (buffersize-1))))

faulty_explained.append("infoleak option 2: no memset and no for loop")
faulty_conds.append(And(Not(memset_cond), noloop))

#all kind of bugs
#s.add(Or(faulty_conds))

#memleak only
s.add(Or(faulty_conds[13], faulty_conds[12], faulty_conds[9], faulty_conds[8], faulty_conds[3], faulty_conds[2]))

print s.check()
m=s.model()
print m
print "buffersize=0x%x" % m.evaluate(buffersize).as_signed_long()
print "left=0x%x" % m.evaluate(left).as_signed_long()
print "right=0x%x" % m.evaluate(right).as_signed_long()
print "bottom=0x%x" % m.evaluate(bottom).as_signed_long()
print "top=0x%x" % m.evaluate(top).as_signed_long()
print "x=0x%x"%m.evaluate(x).as_signed_long()
print "y=0x%x"%m.evaluate(y).as_signed_long()
print "w=0x%x"%m.evaluate(w).as_signed_long()
print "h=0x%x"%m.evaluate(h).as_signed_long()
print "originx=0x%x"%m.evaluate(originx).as_signed_long()
print "originy=0x%x"%m.evaluate(originy).as_signed_long()
print "destx=0x%x"%m.evaluate(destx).as_signed_long()
print "desty=0x%x"%m.evaluate(desty).as_signed_long()
print "endx=0x%x"%m.evaluate(endx).as_signed_long()
print "endy=0x%x"%m.evaluate(endy).as_signed_long()

print "numColumns=0x%x"%m.evaluate(numColumns).as_signed_long()
print "numRows=0x%x"%m.evaluate(numRows).as_signed_long()

print "srcPixelsPerRow=0x%x"%srcPixelsPerRow
print "destBytesPerRow=0x%x"%m.evaluate(destBytesPerRow).as_signed_long()

print "destRows_base=0x%x"%m.evaluate(destRows_base).as_signed_long()
print "destRows_max=0x%x"%m.evaluate(destRows_max).as_signed_long()
print "srcRows_base=0x%x"%m.evaluate(srcRows_base).as_signed_long()
print "srcRows_max=0x%x"%m.evaluate(srcRows_max).as_signed_long()
print "image buffer size=0x%x"%(msize_height.as_long()*msize_width.as_long()*4)
print "memset_cond=%s"%m.evaluate(memset_cond)
print "  x<0=%s, y<0=%s, x+w [0x%x] > msize_width=%s, y+h [0x%x] > msize_height=%s" % (m.evaluate(x < 0), m.evaluate(y < 0), m.evaluate(x+w).as_long(), m.evaluate(x+w > msize_width), m.evaluate(y+h).as_long(), m.evaluate(y+h > msize_height))
print "noloop=%s"%m.evaluate(noloop)
count=0
for c in faulty_conds:
  if str(m.evaluate(c)) == "True":
    print "faulty_conds[%d]=Found!!!! (%s)" % (count, faulty_explained[count])
  else:
    print "faulty_conds[%d]=Not Found (%s)" % (count, faulty_explained[count])
  count+=1

print "traversing model..."
for d in m.decls():
  print "%s = 0x%x" % (d.name(), m[d].as_signed_long())