Skip to content

Commit 21e3f77

Browse files
sipmasipma
committed
CHB: add updated writeback semantics
1 parent 91fef9b commit 21e3f77

File tree

6 files changed

+154
-75
lines changed

6 files changed

+154
-75
lines changed

‎CodeHawk/CHB/bchlib/bCHVersion.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -95,8 +95,8 @@ end
9595

9696

9797
let version = new version_info_t
98-
~version:"0.6.0_20240829"
99-
~date:"2024-08-29"
98+
~version:"0.6.0_20240830"
99+
~date:"2024-08-30"
100100
~licensee: None
101101
~maxfilesize: None
102102
()

‎CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml‎

Lines changed: 19 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -419,25 +419,31 @@ object (self:'a)
419419
random_constant_expr
420420
end
421421

422-
method to_updated_offset_address (floc: floc_int): xpr_t =
422+
method to_updated_offset_address (floc: floc_int): (int * xpr_t) TR.traceresult =
423423
match kind with
424424
| ARMOffsetAddress (r, align, offset, isadd, iswback, isindex, _) ->
425425
if isindex then
426-
self#to_address floc
426+
Ok (0, self#to_address floc)
427427
else
428-
let memoff =
428+
let optinc =
429429
match (offset, isadd) with
430-
| (ARMImmOffset i, true) -> int_constant_expr i
431-
| (ARMImmOffset i, false) -> int_constant_expr (-i)
432-
| _ -> random_constant_expr in
433-
let addr = XOp (XPlus, [self#to_address floc; memoff]) in
434-
floc#inv#rewrite_expr addr
430+
| (ARMImmOffset i, true) -> Some i
431+
| (ARMImmOffset i, false) -> Some (-i)
432+
| _ -> None in
433+
(match optinc with
434+
| None ->
435+
Error [
436+
"to_updated_offset_address: offset type "
437+
^ (arm_memory_offset_to_string offset)
438+
^ "not covered for offset address update"]
439+
| Some inc ->
440+
let addr =
441+
XOp (XPlus, [self#to_address floc; int_constant_expr inc]) in
442+
Ok (inc, floc#inv#rewrite_expr addr))
435443
| _ ->
436-
raise
437-
(BCH_failure
438-
(LBLOCK [
439-
STR "Operand is not an arm-offset-address: ";
440-
self#toPretty]))
444+
Error [
445+
"to_updated_offset_address: not applicable to operand kind: "
446+
^ (p2s self#toPretty)]
441447

442448
method to_variable (floc:floc_int): variable_t =
443449
let env = floc#f#env in

‎CodeHawk/CHB/bchlibarm32/bCHARMOperand.mli‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
66
7-
Copyright (c) 2021-2023 Aarno Labs, LLC
7+
Copyright (c) 2021-2024 Aarno Labs, LLC
88
99
Permission is hereby granted, free of charge, to any person obtaining a copy
1010
of this software and associated documentation files (the "Software"), to deal

‎CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
------------------------------------------------------------------------------
55
The MIT License (MIT)
66
7-
Copyright (c) 2021-2023 Aarno Labs, LLC
7+
Copyright (c) 2021-2024 Aarno Labs, LLC
88
99
Permission is hereby granted, free of charge, to any person obtaining a copy
1010
of this software and associated documentation files (the "Software"), to deal
@@ -191,7 +191,7 @@ class type arm_operand_int =
191191
method to_multiple_expr: floc_int -> xpr_t list
192192
method to_lhs: floc_int -> variable_t * cmd_t list
193193
method to_multiple_lhs: floc_int -> variable_t list * cmd_t list
194-
method to_updated_offset_address: floc_int -> xpr_t
194+
method to_updated_offset_address: floc_int -> (int * xpr_t) traceresult
195195
method to_btype: btype_t
196196

197197
(* predicate *)

‎CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml‎

Lines changed: 52 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,7 @@ module TR = CHTraceResult
7575

7676

7777
let x2p = xpr_formatter#pr_expr
78+
let p2s = CHPrettyUtil.pretty_to_string
7879

7980
let log_error (tag: string) (msg: string): tracelogspec_t =
8081
mk_tracelog_spec ~tag:("FnARMDictionary:" ^ tag) msg
@@ -296,20 +297,22 @@ object (self)
296297
(tags: string list)
297298
(args: int list)
298299
(v: variable_t)
300+
(inc: int)
299301
(x: xpr_t): (string list) * (int list) =
300302
let _ =
301303
if (List.length tags) = 0 then
302304
raise
303305
(BCH_failure
304306
(LBLOCK [STR "Empty tag list in add_base_update"])) in
305-
let xtag = (List.hd tags) ^ "vtxdh" in
307+
let xtag = (List.hd tags) ^ "vtlxdh" in
306308
let uses = [get_def_use v] in
307309
let useshigh = [get_def_use_high v] in
308310
let tags = xtag :: ((List.tl tags) @ ["bu"]) in
309311
let args =
310312
args
311313
@ [xd#index_variable v;
312314
bcd#index_typ t_unknown;
315+
inc;
313316
xd#index_xpr x]
314317
@ uses @ useshigh in
315318
(tags, args) in
@@ -1213,8 +1216,12 @@ object (self)
12131216
let (tags, args) =
12141217
if mem#is_offset_address_writeback then
12151218
let vrn = rn#to_variable floc in
1216-
let xaddr = mem#to_updated_offset_address floc in
1217-
add_base_update tags args vrn xaddr
1219+
let addr_r = mem#to_updated_offset_address floc in
1220+
log_tfold_default
1221+
(log_error "invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDR"))
1222+
(fun (inc, xaddr) -> add_base_update tags args vrn inc xaddr)
1223+
(tags, args)
1224+
addr_r
12181225
else
12191226
(tags, args) in
12201227
(tags, args)
@@ -1245,8 +1252,13 @@ object (self)
12451252
let (tags, args) =
12461253
if mem#is_offset_address_writeback then
12471254
let vrn = rn#to_variable floc in
1248-
let xaddr = mem#to_updated_offset_address floc in
1249-
add_base_update tags args vrn xaddr
1255+
let addr_r = mem#to_updated_offset_address floc in
1256+
log_tfold_default
1257+
(log_error
1258+
"invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDRB"))
1259+
(fun (inc, xaddr) -> add_base_update tags args vrn inc xaddr)
1260+
(tags, args)
1261+
addr_r
12501262
else
12511263
(tags, args) in
12521264
(tags, args)
@@ -1283,8 +1295,13 @@ object (self)
12831295
let (tags, args) =
12841296
if mem#is_offset_address_writeback then
12851297
let vrn = rn#to_variable floc in
1286-
let xaddr = mem#to_updated_offset_address floc in
1287-
add_base_update tags args vrn xaddr
1298+
let addr_r = mem#to_updated_offset_address floc in
1299+
log_tfold_default
1300+
(log_error
1301+
"invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDRB"))
1302+
(fun (inc, xaddr) -> add_base_update tags args vrn inc xaddr)
1303+
(tags, args)
1304+
addr_r
12881305
else
12891306
(tags, args) in
12901307
(tags, args)
@@ -1315,8 +1332,13 @@ object (self)
13151332
let (tags, args) =
13161333
if mem#is_offset_address_writeback then
13171334
let vrn = rn#to_variable floc in
1318-
let xaddr = mem#to_updated_offset_address floc in
1319-
add_base_update tags args vrn xaddr
1335+
let addr_r = mem#to_updated_offset_address floc in
1336+
log_tfold_default
1337+
(log_error
1338+
"invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDREX"))
1339+
(fun (inc, xaddr) -> add_base_update tags args vrn inc xaddr)
1340+
(tags, args)
1341+
addr_r
13201342
else
13211343
(tags, args) in
13221344
(tags, args)
@@ -1346,8 +1368,13 @@ object (self)
13461368
let (tags, args) =
13471369
if mem#is_offset_address_writeback then
13481370
let vrn = rn#to_variable floc in
1349-
let xaddr = mem#to_updated_offset_address floc in
1350-
add_base_update tags args vrn xaddr
1371+
let addr_r = mem#to_updated_offset_address floc in
1372+
log_tfold_default
1373+
(log_error
1374+
"invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDRH"))
1375+
(fun (inc, xaddr) -> add_base_update tags args vrn inc xaddr)
1376+
(tags, args)
1377+
addr_r
13511378
else
13521379
(tags, args) in
13531380
(tags, args)
@@ -1377,8 +1404,13 @@ object (self)
13771404
let (tags, args) =
13781405
if mem#is_offset_address_writeback then
13791406
let vrn = rn#to_variable floc in
1380-
let xaddr = mem#to_updated_offset_address floc in
1381-
add_base_update tags args vrn xaddr
1407+
let addr_r = mem#to_updated_offset_address floc in
1408+
log_tfold_default
1409+
(log_error
1410+
"invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDRSB"))
1411+
(fun (inc, xaddr) -> add_base_update tags args vrn inc xaddr)
1412+
(tags, args)
1413+
addr_r
13821414
else
13831415
(tags, args) in
13841416
(tags, args)
@@ -1406,8 +1438,13 @@ object (self)
14061438
let (tags, args) =
14071439
if mem#is_offset_address_writeback then
14081440
let vrn = rn#to_variable floc in
1409-
let xaddr = mem#to_updated_offset_address floc in
1410-
add_base_update tags args vrn xaddr
1441+
let addr_r = mem#to_updated_offset_address floc in
1442+
log_tfold_default
1443+
(log_error
1444+
"invalid write-back address" ((p2s floc#l#toPretty) ^ ": LDRSH"))
1445+
(fun (inc, xaddr) -> add_base_update tags args vrn inc xaddr)
1446+
(tags, args)
1447+
addr_r
14111448
else
14121449
(tags, args) in
14131450
(tags, args)

0 commit comments

Comments
 (0)