SHARE
TWEET

Untitled

a guest Sep 8th, 2019 200 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. import string
  2. import z3
  3.  
  4. def is_char_allowed(current_char):
  5.     current_char = ord(current_char)
  6.     if (current_char & 128) != 0 or not ((current_char >> 6) & 1) or (current_char >> 4) & 1 and (current_char >> 3) & 1 and ((current_char >> 2) & 1 or (current_char >> 1) & 1 and current_char & 1) or not ((current_char >> 4) & 1) and not ((current_char >> 3) & 1) and not ((current_char >> 2) & 1) and not ((current_char >> 1) & 1) and not (current_char & 1):
  7.         return False
  8.     return True
  9.  
  10. # (((chr >> 5) & 1) << 15) | ((((chr >> 5) & 1) << 14) | ((((chr >> 5) & 1) << 13) | ((((chr >> 5) & 1) << 10) | ((((chr >> 4) & 1) << 9) | ((((chr >> 3) & 1) << 8) | (((chr >> 5) & 1) << 7) | ((((chr >> 5) & 1) << 6) | ((unsigned __int8)(32 * ((chr >> 5) & 1)) | ((unsigned __int8)(4 * ((chr >> 2) & 1)) | ((unsigned __int8)(2 * ((chr >> 1) & 1)) | chr & 1) & 0xFB) & 0xDF) & 0xBF) & 0x7F) & 0xFDFF) & 0xFBFF) & 0xDFFF) & 0xBFFF) & 0x7FFF;
  11.  
  12. out = []
  13. for ch in string.printable:
  14.     if is_char_allowed(ch):
  15.         out.append(ch)
  16.  
  17.  
  18. def get_char(ch):
  19.     return (((ch >> 5) & 1) << 15) | ((((ch >> 5) & 1) << 14) | ((((ch >> 5) & 1) << 13) | ((((ch >> 5) & 1) << 10) | ((((ch >> 4) & 1) << 9) | ((((ch >> 3) & 1) << 8) | (((ch >> 5) & 1) << 7) | ((((ch >> 5) & 1) << 6) | ((0xff&(32 * ((ch >> 5) & 1))) | ((0xff&(4 * ((ch >> 2) & 1))) | ((0xff&(2 * ((ch >> 1) & 1))) | ch & 1) & 0xFB) & 0xDF) & 0xBF) & 0x7F) & 0xFDFF) & 0xFBFF) & 0xDFFF) & 0xBFFF) & 0x7FFF
  20.  
  21.  
  22. rzeczy = []
  23. for o in out:
  24.     rzeczy.append(get_char(ord(o)))
  25.  
  26. x = z3.BitVec('x', 64)
  27. y = z3.BitVec('y', 64)
  28. s = z3.Solver()
  29.  
  30. s.add((y + (x + (1 + 0xf4a30cd491608469 * x) * 0x80884058088405 + 0x44424E) * 0x80884058088405)+7644228357687976132 == 0)
  31. v = []
  32. for ch in rzeczy:
  33.     v.append(f"(x&0xffff == {ch})")
  34. v = " or ".join(v)
  35. s.add(eval(v))
  36.  
  37. v = []
  38. for ch in rzeczy:
  39.     v.append(f"(y&0xffff == {ch})")
  40. v = " or ".join(v)
  41. s.add(eval(v))
  42.  
  43. print(s.check())
  44. print(s.model())
  45. print(out)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top