Skip to content

Commit 34e5f97

Browse files
authored
Fix pc value in pc-relative thumb ldr (#1414)
1 parent f6f47fc commit 34e5f97

File tree

2 files changed

+5
-4
lines changed

2 files changed

+5
-4
lines changed

plugins/thumb/thumb_main.ml

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -111,19 +111,20 @@ module Thumb(CT : Theory.Core) = struct
111111
!!Insn.empty
112112

113113

114-
let lift_mem pc opcode insn =
114+
let lift_mem addr opcode insn =
115115
let module Mem = Thumb_mem.Make(CT) in
116116
let open Mem in
117+
let pc = W32.(addr + int 4) in
117118
match opcode, (MC.Insn.ops insn : Op.t array) with
118119
| `tLDRi, [|Reg rd; Reg rm; Imm i; Imm c; _|]
119120
| `tLDRspi, [|Reg rd; Reg rm; Imm i; Imm c; _|] ->
120121
ldri (reg rd) (reg rm) (imm i * 4) (cnd c)
121122
| `tLDRr, [|Reg rd; Reg rm; Reg rn; Imm c; _|] ->
122123
ldrr (reg rd) (reg rm) (reg rn) (cnd c)
123124
| `tLDRpci, [|Reg rd; Imm i; Imm c; _|] ->
124-
ldrpci (reg rd) W32.(pc + int 2) (imm i) (cnd c)
125+
ldrpci (reg rd) pc (imm i) (cnd c)
125126
| `t2LDRpci, [|Reg rd; Imm i; Imm c; _|] ->
126-
ldrpci (reg rd) W32.(pc + int 4) (imm i) (cnd c)
127+
ldrpci (reg rd) pc (imm i) (cnd c)
127128
| `tLDRBi, [|Reg rd; Reg rm; Imm i; Imm c; _|] ->
128129
ldrbi (reg rd) (reg rm) (imm i) (cnd c)
129130
| `tLDRBr, [|Reg rd; Reg rm; Reg rn; Imm c; _|] ->

plugins/thumb/thumb_mem.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ module Make(CT : Theory.Core) = struct
4949
rd <-? signed @@ load s16 (var rn + var rm)
5050

5151
let ldrpci rd pc off =
52-
rd <-? load s32 @@ bitv pc + const off
52+
rd <-? load s32 @@ bitv W32.(pc land ~~(int 3)) + const off
5353

5454
let ldm b regs cnd =
5555
branch cnd [

0 commit comments

Comments
 (0)