draperlaboratory / cbat_tools

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

Incorrectly selecting registers in input_regs #344

Open fortunac opened 2 years ago

fortunac commented 2 years ago

In input_regs https://github.com/draperlaboratory/cbat_tools/blob/master/wp/lib/bap_wp/src/precondition.ml#L423, AArch64 matches the arm target, but we are selecting 32-bit registers instead of 64-bit registers. We should also probably look up registers by their roles as stated in the comment.

ivg commented 2 years ago

Do you need the input registers to be in a specific order? If not, i.e., if you're just looking for the set of call clobbered registers, then you can safely use Theory.Target.regs ~roles:[Theory.Role.Register.caller_saved]. If you need the set of registers that are used to pass arguments to a function, you can use function_argument and function_return roles. But the list of returned registers will be ordered by the register names (which coincides with the proper order in ARM, MIPS, PowerPC, but in general, e.g., in x86, doesn't work). You can, however, use the predefined list for x86, as it is now, and rely on the roles interface for the rest of the targets.

fortunac commented 2 years ago

Nope, we don't need the registers to be in a specific order, so using Theory.Target.regs is exactly what we need. Thanks for the insight!