-
Notifications
You must be signed in to change notification settings - Fork 52
Description
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.