Skip to content

Instantly share code, notes, and snippets.

@travitch
Created April 8, 2020 15:16
Show Gist options
  • Save travitch/5707b702f81751afd7a8fa33456f62ea to your computer and use it in GitHub Desktop.
Save travitch/5707b702f81751afd7a8fa33456f62ea to your computer and use it in GitHub Desktop.
ARM disassembly and abstract view
ASM
0001010c <f1>:
1010c: e92d4800 push {fp, lr}
10110: e28db004 add fp, sp, #4
10114: e24dd008 sub sp, sp, #8
10118: e50b0008 str r0, [fp, #-8]
1011c: e51b3008 ldr r3, [fp, #-8]
10120: e2833001 add r3, r3, #1
10124: e1a00003 mov r0, r3
10128: ebffffea bl 100d8 <f2>
1012c: e1a00000 nop ; (mov r0, r0)
10130: e24bd004 sub sp, fp, #4
10134: e8bd8800 pop {fp, pc}
State around the call at 0x1012c
pre-call state: registers:
{ _PC = code {0x1010c}
, _R13 = rsp_0x1010c + 0
, _R14 = return_addr
}
stack:
0xfffffff4 := return_addr
post-call reg state @ 0x1012c : { _PC = code {0x1012c}
, _R11 = rsp_0x1010c + fffffffc
, _R13 = rsp_0x1010c + fffffff0
, _R14 = code {0x1012c}
}
pre abstract stack val: rsp_0x1010c + fffffff0
post call abs state: registers:
{ _PC = code {0x1012c}
, _R11 = rsp_0x1010c + fffffffc
, _R13 = rsp_0x1010c + fffffff0
, _R14 = code {0x1012c}
}
stack:
0xfffffff4 := return_addr
IR for function
function 0x1010c
0x1010c:
; _R13 = stack_frame + 0
# 0x1010c 0x1010c: STMDB_A1(xxxxxxxx.xxxxxxxx.00x0xxxx.xxxx1001) Rn 13, W 1, cond 14, register_list 18432
# 0x1010c: STMDB_A1(xxxxxxxx.xxxxxxxx.00x0xxxx.xxxx1001) Rn 13, W 1, cond 14, register_list 18432
r484 := (bv_add _R13_0 (0xfffffff8 :: [32]))
r516 := (bv_add _R13_0 (0xfffffff0 :: [32]))
write_mem r516 _R11_0
write_mem r516 _R11_0
write_mem r516 _R11_0
r522 := (bv_add _R13_0 (0xfffffff4 :: [32]))
write_mem r522 _R14_0
write_mem r522 _R14_0
# 0x1010c: {_PC => 0x10110
;_R0 => _R0_0
;_R13 => r484
;__AssertionFailure => true
;__UnpredictableBehavior => false
;ARMWriteMode => 0x0 :: [2]}
# 0x10110 0x10110: ADD_SP_i_A1(xxxxxxxx.xxxxxxxx.10001101.xxxx0010) Rd 11, S 0, cond 14, imm12 4
# 0x10110: ADD_SP_i_A1(xxxxxxxx.xxxxxxxx.10001101.xxxx0010) Rd 11, S 0, cond 14, imm12 4
r578 := (bv_add _R13_0 (0xfffffffc :: [32]))
# 0x10110: {PSTATE_T => 0x0 :: [1]
;_PC => 0x10114
;_R0 => _R0_0
;_R11 => r578
;__AssertionFailure => true
;__BranchTaken => false
;ARMWriteMode => 0x0 :: [2]}
# 0x10114 0x10114: SUB_SP_i_A1(xxxxxxxx.xxxxxxxx.01001101.xxxx0010) Rd 13, S 0, cond 14, imm12 8
# 0x10114: SUB_SP_i_A1(xxxxxxxx.xxxxxxxx.01001101.xxxx0010) Rd 13, S 0, cond 14, imm12 8
r664 := (bv_add _R13_0 (0xfffffff0 :: [32]))
# 0x10114: {PSTATE_T => 0x0 :: [1]
;_PC => 0x10118
;_R0 => _R0_0
;_R13 => r664
;__AssertionFailure => true
;__BranchTaken => false
;ARMWriteMode => 0x0 :: [2]}
# 0x10118 0x10118: STR_i_A1_off(xxxxxxxx.xxxxxxxx.x000xxxx.xxxx0101) P 1, Rn 11, Rt 0, U 0, W 0, cond 14, imm12 8
# 0x10118: STR_i_A1_off(xxxxxxxx.xxxxxxxx.x000xxxx.xxxx0101) P 1, Rn 11, Rt 0, U 0, W 0, cond 14, imm12 8
r698 := (bv_add _R13_0 (0xfffffff4 :: [32]))
write_mem r698 _R0_0
# 0x10118: {_PC => 0x1011c
;__AssertionFailure => true
;ARMWriteMode => 0x0 :: [2]}
# 0x1011c 0x1011c: LDR_i_A1_off(xxxxxxxx.xxxxxxxx.x001xxxx.xxxx0101) P 1, Rn 11, Rt 3, U 0, W 0, cond 14, imm12 8
# 0x1011c: LDR_i_A1_off(xxxxxxxx.xxxxxxxx.x001xxxx.xxxx0101) P 1, Rn 11, Rt 3, U 0, W 0, cond 14, imm12 8
r701 := (bv_add _R13_0 (0xfffffff4 :: [32]))
r705 := read_mem r701 (bvle4)
r711 := (bv_add _R13_0 (0xfffffff4 :: [32]))
r715 := read_mem r711 (bvle4)
r718 := (bv_add _R13_0 (0xfffffff4 :: [32]))
r719 := read_mem r718 (bvle4)
r720 := (bv_add _R13_0 (0xfffffff4 :: [32]))
r724 := read_mem r720 (bvle4)
# 0x1011c: {PSTATE_T => 0x0 :: [1]
;_PC => 0x10120
;_R0 => _R0_0
;_R3 => r719
;__AssertionFailure => true
;__BranchTaken => false
;__UndefinedBehavior => false
;__UnpredictableBehavior => false
;ARMWriteMode => 0x0 :: [2]}
# 0x10120 0x10120: ADD_i_A1(xxxxxxxx.xxxxxxxx.1000xxxx.xxxx0010) Rd 3, Rn 3, S 0, cond 14, imm12 1
# 0x10120: ADD_i_A1(xxxxxxxx.xxxxxxxx.1000xxxx.xxxx0010) Rd 3, Rn 3, S 0, cond 14, imm12 1
r760 := (bv_add r719 (0x1 :: [32]))
# 0x10120: {PSTATE_T => 0x0 :: [1]
;_PC => 0x10124
;_R0 => _R0_0
;_R3 => r760
;__AssertionFailure => true
;__BranchTaken => false
;__UndefinedBehavior => false
;ARMWriteMode => 0x0 :: [2]}
# 0x10124 0x10124: MOV_r_A1(xxx0xxxx.xxxxxxxx.1010OOOO.xxxx0001) Rd 0, Rm 3, S 0, cond 14, imm5 0, type1 0, QuasiMask0 QuasiMask"("4): 0
# 0x10124: MOV_r_A1(xxx0xxxx.xxxxxxxx.1010OOOO.xxxx0001) Rd 0, Rm 3, S 0, cond 14, imm5 0, type1 0, QuasiMask0 QuasiMask"("4): 0
# 0x10124: {PSTATE_T => 0x0 :: [1]
;_PC => 0x10128
;_R0 => r760
;__AssertionFailure => true
;__BranchTaken => false
;ARMWriteMode => 0x0 :: [2]}
# 0x10128 0x10128: BL_i_A1(xxxxxxxx.xxxxxxxx.xxxxxxxx.xxxx1011) cond 14, imm24 16777194
# 0x10128: BL_i_A1(xxxxxxxx.xxxxxxxx.xxxxxxxx.xxxx1011) cond 14, imm24 16777194
# 0x10128: {PSTATE_T => 0x0 :: [1]
;_PC => 0x100d8 :: [32]
;_R0 => r760
;_R14 => 0x1012c
;__AssertionFailure => true
;__BranchTaken => true
;ARMWriteMode => 0x0 :: [2]}
call and return to 0x1012c
{ PSTATE_IT = 0x0 :: [8]
, PSTATE_T = 0x0 :: [1]
, PSTATE_nRW = 0x1 :: [1]
, _PC = 0x100d8 :: [32]
, _R0 = r760
, _R11 = r578
, _R13 = r664
, _R14 = 0x1012c
, _R3 = r760
, __AssertionFailure = true
, __BranchTaken = true
, __PendingInterrupt = false
, __PendingPhysicalSError = false
, __Sleeping = false
, __UndefinedBehavior = false
, __UnpredictableBehavior = false
, ARMWriteMode = 0x0 :: [2]
}
0x1012c:
; _R11 = stack_frame - 4
; _R13 = stack_frame - 16
# 0x1012c 0x1012c: MOV_r_A1(xxx0xxxx.xxxxxxxx.1010OOOO.xxxx0001) Rd 0, Rm 0, S 0, cond 14, imm5 0, type1 0, QuasiMask0 QuasiMask"("4): 0
# 0x1012c: MOV_r_A1(xxx0xxxx.xxxxxxxx.1010OOOO.xxxx0001) Rd 0, Rm 0, S 0, cond 14, imm5 0, type1 0, QuasiMask0 QuasiMask"("4): 0
# 0x1012c: {PSTATE_T => 0x0 :: [1]
;_PC => 0x10130
;_R0 => _R0_0
;__AssertionFailure => false
;__BranchTaken => false
;ARMWriteMode => 0x0 :: [2]}
# 0x10130 0x10130: SUB_i_A1(xxxxxxxx.xxxxxxxx.0100xxxx.xxxx0010) Rd 13, Rn 11, S 0, cond 14, imm12 4
# 0x10130: SUB_i_A1(xxxxxxxx.xxxxxxxx.0100xxxx.xxxx0010) Rd 13, Rn 11, S 0, cond 14, imm12 4
r1416 := (bv_add _R11_0 (0xfffffffc :: [32]))
# 0x10130: {PSTATE_T => 0x0 :: [1]
;_PC => 0x10134
;_R0 => _R0_0
;_R13 => r1416
;__AssertionFailure => true
;__BranchTaken => false
;__UndefinedBehavior => false
;ARMWriteMode => 0x0 :: [2]}
# 0x10134 0x10134: LDM_A1(xxxxxxxx.xxxxxxxx.10x1xxxx.xxxx1000) Rn 13, W 1, cond 14, register_list 34816
# 0x10134: LDM_A1(xxxxxxxx.xxxxxxxx.10x1xxxx.xxxx1000) Rn 13, W 1, cond 14, register_list 34816
r1462 := read_mem _R11_0 (bvle4)
r1463 := (bv_and r1462 (0x1 :: [32]))
r1464 := (trunc r1463 1)
r1465 := (eq r1464 (0x1 :: [1]))
r1466 := (mux r1465 (0x1 :: [1]) (0x0 :: [1]))
r1479 := read_mem _R11_0 (bvle4)
r1490 := read_mem r1416 (bvle4)
r1491 := read_mem r1416 (bvle4)
r1492 := read_mem r1416 (bvle4)
r1493 := read_mem r1416 (bvle4)
r1494 := read_mem r1416 (bvle4)
r1495 := read_mem r1416 (bvle4)
r1496 := read_mem r1416 (bvle4)
r1497 := read_mem r1416 (bvle4)
r1498 := read_mem r1416 (bvle4)
r1499 := read_mem r1416 (bvle4)
r1500 := read_mem r1416 (bvle4)
r1501 := read_mem r1416 (bvle4)
r1502 := read_mem _R11_0 (bvle4)
r1504 := read_mem _R11_0 (bvle4)
r1506 := read_mem _R11_0 (bvle4)
r1508 := read_mem _R11_0 (bvle4)
r1517 := (bv_add _R11_0 (0x4 :: [32]))
r1539 := (bv_add _R11_0 (0x8 :: [32]))
r1543 := read_mem r1539 (bvle4)
# 0x10134: {PSTATE_T => r1466
;_PC => r1479
;_R0 => _R0_0
;_R11 => r1501
;_R13 => r1517
;__AssertionFailure => true
;__BranchTaken => true
;__UnpredictableBehavior => false
;ARMWriteMode => 0x0 :: [2]}
classify failure
{ PSTATE_IT = 0x0 :: [8]
, PSTATE_T = r1466
, PSTATE_nRW = 0x1 :: [1]
, _PC = r1479
, _R11 = r1501
, _R13 = r1517
, __AssertionFailure = true
, __BranchTaken = true
, __PendingInterrupt = false
, __PendingPhysicalSError = false
, __Sleeping = false
, __UndefinedBehavior = false
, __UnpredictableBehavior = false
, ARMWriteMode = 0x0 :: [2]
}
Branch: IP is not an mux:
let r1479 := read_mem _R11_0 (bvle4)
in r1479
Pattern match failure in do expression at src/Data/Macaw/Discovery.hs:1187:3-25
Return: Pattern match failure in do expression at src/Data/Macaw/Discovery.hs:1220:5-19
Jump: Jump value r1479 is not a valid address.
Jump table: Absolute jump table: Pattern match failure in do expression at src/Data/Macaw/Discovery.hs:568:3-21
Jump table: Relative jump table: Pattern match failure in do expression at src/Data/Macaw/Discovery.hs:766:3-18
PLT stub: Pattern match failure in do expression at src/Data/Macaw/Discovery.hs:1289:5-18
Tail call classification failed.
f
Notes:
* The abstract value of the IP register at the return is Top
* The abstract state after the call has the link register value at the correct location (0xfffffff4)
* ARM R14 (the link register) is written to RSP0 - 12 (macaw value r522 is the address)
* The concrete (macaw) value of the IP register is macaw value 1479, which is a read from the value of R11 (the frame pointer), but the value of R11 at the beginning of the block at 0x1012c
- R11 has the value _R11 = rsp_0x1010c + fffffffc after the call
- This looks like it is off-by-4 from the necessary value
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment