angr / vex

A patched version of VEX to work with PyVEX.
GNU General Public License v2.0
104 stars 44 forks source link

Spechelper for FP compares #50

Open udiboy1209 opened 1 year ago

udiboy1209 commented 1 year ago

I am trying to get a symbolic expression from an ARM64 code performing floating point compares. The function takes single float argument in reg s0 which I have initialized as FPS('x', FLOAT).

For the ARM64 insns:

00000000000000ec <f_piece0>:
      ec: 08 20 20 1e   fcmp    s0, #0.0
      f0: c5 00 00 54   b.pl    0x108 <f_piece0+0x1c>

The IRSB is:

IRSB {
   t0:Ity_F32 t1:Ity_F32 t2:Ity_I32 t3:Ity_I64 t4:Ity_I64 t5:Ity_I64 t6:Ity_I64 t7:Ity_I64 t8:Ity_I64 t9:Ity_I64 t10:Ity_I64 t11:Ity_I64 t12:Ity_I64 t13:Ity_I64 t14:Ity_I64 t15:Ity_I64 t16:Ity_I64 t17:Ity_I64 t18:Ity_I64 t19:Ity_I64 t20:Ity_I64 t21:Ity_I64 t22:Ity_I64 t23:Ity_I1 t24:Ity_I64 t25:Ity_I64 t26:Ity_I64 t27:Ity_I64 t28:Ity_I64 t29:Ity_I64 t30:Ity_I64

   00 | ------ IMark(0x4000ec, 4, 0) ------
   01 | t0 = GET:F32(s0)
   02 | t2 = CmpF32(t0,0.000000)
   03 | t10 = 32Uto64(t2)
   04 | t12 = And64(t10,0x0000000000000001)
   05 | t14 = Shr64(t10,0x05)
   06 | t13 = And64(t14,0x0000000000000003)
   07 | t11 = Or64(t13,t12)
   08 | t19 = Xor64(t11,0x0000000000000001)
   09 | t18 = Shl64(t19,0x3e)
   10 | t17 = Sub64(t18,0x0000000000000001)
   11 | t16 = Shr64(t17,0x3d)
   12 | t15 = Add64(t16,0x0000000000000001)
   13 | t22 = Shr64(t11,0x01)
   14 | t21 = And64(t11,t22)
   15 | t20 = And64(t21,0x0000000000000001)
   16 | t6 = Sub64(t15,t20)
   17 | t8 = Shl64(t6,0x1c)
   18 | PUT(cc_op) = 0x0000000000000000
   19 | PUT(cc_dep1) = t8
   20 | PUT(cc_dep2) = 0x0000000000000000
   21 | PUT(cc_ndep) = 0x0000000000000000
   22 | PUT(pc) = 0x00000000004000f0
   23 | ------ IMark(0x4000f0, 4, 0) ------
   24 | t29 = arm64g_calculate_condition(0x0000000000000050,t8,0x0000000000000000,0x0000000000000000):Ity_I64
   25 | t23 = 64to1(t29)
   26 | if (t23) { PUT(pc) = 0x400108; Ijk_Boring }
   NEXT: PUT(pc) = 0x00000000004000f4; Ijk_Boring
}

This code essentially converts the value generated by CmpF32 to NZCV bits (ref mk_convert_IRCmpF64Result_to_NZCV in guest_arm64_toIR.c) When s0 is a symbolic variable, this whole computation stays as is in the constraint added to this IRSB's state. I am looking for a way to simplify this constraint. In other cases, there is a specialization helper which converts some instances of arm64g_calculate_condition to Cmp*.

Is there a way where something similar can be done for floating-point compares too like the one above? I understand this is not just a simple replacement of the arm64g_calculate_condition function but one needs to look back to find the CmpF32.

rhelmot commented 1 year ago

You seem to have a pretty good grasp on the situation - there is presently not such a specialization helper, but one could be written. None of us on the angr team have the cycles to implement this, but if you were do to it, we would gladly accept the pull request.