draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

Floating point instruction handler #353

Closed fortunac closed 2 years ago

fortunac commented 2 years ago

This PR adds a handler for floating point instructions. With the --bil-enable-intrinsic=:unknown flag set, BAP will turn the floating point (or any instruction) that has no semantics into an intrinsic call. For example, for ADDss xmm0 xmm1, WP will chaos xmm0 with ADDss_ret_xmm0(xmm0, xmm1) and xmm1 with ADDs_ret_xmm1(xmm0,xmm1).

There has also been changes with how the init-mem flag is handled in the comparison case. The values of the .rodata section are added as a hypothesis to our precondition (e.g. mem[0xdeadbeef] = 0xcafef00d) for both the original and the modified binary. At every memory read location in the binary, if the read address was initialized, we make no assumptions about the equality of the values between the two binaries. Otherwise, if the address was on the stack, we say they are equal, if they are in the data section and were not initialized, they are equal at an offset, and otherwise the values are equal. Using any combination of --init-mem, --mem-offset, or --rewrite-addresses is not allowed.