2022.03.29

1. Intro

  • Code

    • mov eax,0x5
    • add ebx,0x4
    • imul eax,ebx

  • Semantics Juice

    • eax = 5
    • ebx = (def(ebx) + 4) × 5
    • = def(ebx) × 5 + 20

  • Juice

    • A = N1
    • B = def(B) × N1 + N2
    • where N2 = N1 × N3
    • and type(A) = type(B) = reg32

  • Q: 如何快速比较两个Juice是否相同？

  • A: 关键词linear order, Rvalue。给语义的Rvalue排序，进行比较（线性时间复杂度），或者hash（常数时间）

3. Method

5. Limitations

  • Rice's Theorem理论及局限？！
    • https://en.wikipedia.org/wiki/Rice%27s_theorem
    • https://zhuanlan.zhihu.com/p/339648002
    • https://zhuanlan.zhihu.com/p/370832282
  • 单位是基本块，大于基本块的算法，没办法了