search

JonathanSalwan / Triton

Triton is a dynamic binary analysis library. Build your own program analysis tools, automate your reverse engineering, perform software verification or just emulate code.
https://triton-library.github.io
Apache License 2.0
3.4k stars 525 forks source link

Optimize the parity flag computation on Intel #1184

Closed JonathanSalwan closed 1 year ago

JonathanSalwan commented 1 year ago

Reduce the complexity of the Parity flag computation on Intel. The new implementation has been tested with the following smt code.

(set-logic QF_AUFBV)

(declare-fun SymVar_0 () (_ BitVec 64))
(declare-fun SymVar_1 () (_ BitVec 64))

(define-fun ref!2 () (_ BitVec 64) (bvxor SymVar_0 SymVar_1))

; old implementation
(define-fun pf1 () (_ BitVec 1) (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (_ bv1 1) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!2) (_ bv0 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!2) (_ bv1 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!2) (_ bv2 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!2) (_ bv3 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!2) (_ bv4 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!2) (_ bv5 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!2) (_ bv6 8)))) ((_ extract 0 0) (bvlshr ((_ extract 7 0) ref!2) (_ bv7 8)))))

; the new one. shorter than the previous one
(define-fun pf2 () (_ BitVec 1) (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (bvxor (_ bv1 1) ((_ extract 0 0) ref!2)) ((_ extract 1 1) ref!2)) ((_ extract 2 2) ref!2)) ((_ extract 3 3) ref!2)) ((_ extract 4 4) ref!2)) ((_ extract 5 5) ref!2)) ((_ extract 6 6) ref!2)) ((_ extract 7 7) ref!2)))

;(assert (= pf1 pf2)) ; must be sat
(assert (distinct pf1 pf2)) ; must be unsat

(check-sat)