ARM disassembly and abstract view

gistfile1.txt

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