Skip to content

Commit a3a176c

Browse files
sipmasipma
committed
CHB:ARM add some memory resolution
1 parent 80a36bb commit a3a176c

File tree

5 files changed

+145
-20
lines changed

5 files changed

+145
-20
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_20241003"
99-
~date:"2024-10-03"
98+
~version:"0.6.0_20241005"
99+
~date:"2024-10-05"
100100
~licensee: None
101101
~maxfilesize: None
102102
()

‎CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -406,6 +406,8 @@ object (self:'a)
406406
XOp (XMult, [XOp (XDiv, [XVar rvar; alignx]); alignx])
407407
else
408408
XVar rvar in
409+
(* memory addresses are not rewritten to preserve the structure of the
410+
data accessed (in case of an non-optimizing compiler) *)
409411
let addr = XOp (XPlus, [rvarx; memoff]) in
410412
(* floc#inv#rewrite_expr addr *)
411413
simplify_xpr addr
@@ -509,6 +511,26 @@ object (self:'a)
509511
STR ": ivax: ";
510512
x2p ivax])
511513
(floc#f#env#mk_memory_address_deref_variable v)
514+
| XOp (XPlus, [XVar basevar; XVar memoffset]) ->
515+
let optmemvaraddr = floc#decompose_memvar_address xoffset in
516+
(match optmemvaraddr with
517+
| Some (memref, memoffset)
518+
when BCHMemoryReference.is_constant_offset memoffset ->
519+
(env#mk_index_offset_memory_variable memref memoffset,
520+
[STR "ARMShiftedIndexOffset (decomposed)";
521+
self#toPretty;
522+
STR "; memref: ";
523+
memref#toPretty;
524+
STR "; memoffset: ";
525+
BCHMemoryReference.memory_offset_to_pretty memoffset])
526+
| _ ->
527+
(env#mk_unknown_memory_variable "operand",
528+
[STR "ARMShiftedIndexOffset (sum)";
529+
self#toPretty;
530+
STR "; basevar: ";
531+
basevar#toPretty;
532+
STR "; memoffset: ";
533+
memoffset#toPretty]))
512534
| _ ->
513535
(env#mk_unknown_memory_variable "operand",
514536
[STR "ARMShiftedIndexOffset";

‎CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -513,6 +513,22 @@ object (self)
513513

514514
end
515515

516+
| LoadRegisterHalfword (_, rt, rn, rm, memop, _) when rm#is_immediate ->
517+
let rtreg = rt#to_register in
518+
let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in
519+
begin
520+
(* LDRH rt, [rn, rm] : X_rndef.load <: X_rt *)
521+
(let xrdef = get_variable_rdefs (rn#to_variable floc) in
522+
let rnreg = rn#to_register in
523+
let offset = rm#to_numerical#toInt in
524+
List.iter (fun rdsym ->
525+
let ldaddr = rdsym#getBaseName in
526+
let rdtypevar = mk_reglhs_typevar rnreg faddr ldaddr in
527+
let rdtypevar = add_load_capability ~offset rdtypevar in
528+
store#add_subtype_constraint
529+
(mk_vty_term rdtypevar) (mk_vty_term rttypevar)) xrdef);
530+
end
531+
516532
| LogicalShiftLeft (_, _, rd, rn, rm, _) when rm#is_immediate ->
517533
let rdreg = rd#to_register in
518534
let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in

‎CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml‎

Lines changed: 104 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1680,13 +1680,15 @@ let translate_arm_instruction
16801680
let (lhs, cmds) = floc#get_ssa_assign_commands rtreg ~vtype rhs in
16811681
let cmds = cmds @ updatecmds in
16821682
let usevars = get_register_vars [rn; rm] in
1683-
let usevars =
1684-
let memvar = mem#to_variable floc in
1685-
if floc#f#env#is_unknown_memory_variable memvar then
1686-
usevars
1683+
let memvar = mem#to_variable floc in
1684+
let (usevars, usehigh) =
1685+
if memvar#isTmp || floc#f#env#is_unknown_memory_variable memvar then
1686+
(* elevate address variables to high-use *)
1687+
let xrn = rn#to_expr floc in
1688+
let xrm = rm#to_expr floc in
1689+
(usevars, get_use_high_vars [xrn; xrm])
16871690
else
1688-
memvar :: usevars in
1689-
let usehigh = get_use_high_vars [rhs] in
1691+
(memvar :: usevars, get_use_high_vars [rhs]) in
16901692
let defcmds =
16911693
floc#get_vardef_commands
16921694
~defs:[lhs]
@@ -1782,12 +1784,15 @@ let translate_arm_instruction
17821784
let vtype = t_ushort in
17831785
let (vrt, cmds) = floc#get_ssa_assign_commands rtreg ~vtype rhs in
17841786
let usevars = get_register_vars [rn; rm] in
1785-
let usevars =
1786-
if floc#f#env#is_unknown_memory_variable memvar then
1787-
usevars
1787+
let memvar = mem#to_variable floc in
1788+
let (usevars, usehigh) =
1789+
if memvar#isTmp || floc#f#env#is_unknown_memory_variable memvar then
1790+
(* elevate address variables to high-use *)
1791+
let xrn = rn#to_expr floc in
1792+
let xrm = rm#to_expr floc in
1793+
(usevars, get_use_high_vars [xrn; xrm])
17881794
else
1789-
memvar :: usevars in
1790-
let usehigh = get_use_high_vars [rhs] in
1795+
(memvar :: usevars, get_use_high_vars [rhs]) in
17911796
let defcmds =
17921797
floc#get_vardef_commands
17931798
~defs:[vrt]
@@ -2747,7 +2752,27 @@ let translate_arm_instruction
27472752
let _ = check_storage mem vmem in
27482753
let xrt = rt#to_expr floc in
27492754
let xrt = floc#inv#rewrite_expr xrt in
2750-
let cmds = memcmds @ (floc#get_assign_commands vmem xrt) in
2755+
let cmds =
2756+
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
2757+
let xrn = rewrite_expr floc (rn#to_expr floc) in
2758+
let xrm = rewrite_expr floc (rm#to_expr floc) in
2759+
begin
2760+
ch_error_log#add
2761+
"assignment to unknown memory"
2762+
(LBLOCK [
2763+
floc#l#toPretty;
2764+
STR " STR [";
2765+
rn#toPretty;
2766+
STR ", ";
2767+
rm#toPretty;
2768+
STR "]; base: ";
2769+
x2p xrn;
2770+
STR ", offset: ";
2771+
x2p xrm]);
2772+
[]
2773+
end
2774+
else
2775+
floc#get_assign_commands vmem xrt in
27512776
let usevars = get_register_vars [rt; rn; rm] in
27522777
let usehigh = get_use_high_vars [xrt] in
27532778
let (usevars, usehigh) =
@@ -2779,7 +2804,7 @@ let translate_arm_instruction
27792804
addr_r
27802805
else
27812806
[] in
2782-
let cmds = defcmds @ cmds @ updatecmds in
2807+
let cmds = memcmds @ defcmds @ cmds @ updatecmds in
27832808
let _ =
27842809
(* record register spill *)
27852810
let vrt = rt#to_variable floc in
@@ -2794,7 +2819,27 @@ let translate_arm_instruction
27942819
let (vmem, memcmds) = mem#to_lhs floc in
27952820
let _ = check_storage mem vmem in
27962821
let xrt = XOp (XXlsb, [rt#to_expr floc]) in
2797-
let cmds = floc#get_assign_commands vmem xrt in
2822+
let cmds =
2823+
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
2824+
let xrn = rewrite_expr floc (rn#to_expr floc) in
2825+
let xrm = rewrite_expr floc (rm#to_expr floc) in
2826+
begin
2827+
ch_error_log#add
2828+
"assignment to unknown memory"
2829+
(LBLOCK [
2830+
floc#l#toPretty;
2831+
STR " STRB [";
2832+
rn#toPretty;
2833+
STR ", ";
2834+
rm#toPretty;
2835+
STR "]; base: ";
2836+
x2p xrn;
2837+
STR ", offset: ";
2838+
x2p xrm]);
2839+
[]
2840+
end
2841+
else
2842+
floc#get_assign_commands vmem xrt in
27982843
let usevars = get_register_vars [rt; rn; rm] in
27992844
let usehigh = get_use_high_vars [xrt] in
28002845
let (usevars, usehigh) =
@@ -2895,9 +2940,31 @@ let translate_arm_instruction
28952940
let _ = check_storage mem vmem in
28962941
let rdreg = rd#to_register in
28972942
let xrt = rt#to_expr floc in
2898-
let cmds = floc#get_assign_commands vmem xrt in
2943+
let cmds =
2944+
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
2945+
let xrn = rewrite_expr floc (rn#to_expr floc) in
2946+
begin
2947+
ch_error_log#add
2948+
"assignment to unknown memory"
2949+
(LBLOCK [
2950+
floc#l#toPretty;
2951+
STR " STREX [";
2952+
rn#toPretty;
2953+
STR "]; base: ";
2954+
x2p xrn]);
2955+
[]
2956+
end
2957+
else
2958+
floc#get_assign_commands vmem xrt in
28992959
let usevars = get_register_vars [rt; rn] in
29002960
let usehigh = get_use_high_vars [xrt] in
2961+
let (usevars, usehigh) =
2962+
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
2963+
(* elevate address variables to high-use *)
2964+
let xrn = rn#to_expr floc in
2965+
(usevars, get_addr_use_high_vars [xrn])
2966+
else
2967+
(vmem :: usevars, usehigh) in
29012968
let (vrd, scmds) = floc#get_ssa_abstract_commands rdreg () in
29022969
let defcmds =
29032970
floc#get_vardef_commands
@@ -2915,7 +2982,27 @@ let translate_arm_instruction
29152982
let (vmem, memcmds) = mem#to_lhs floc in
29162983
let _ = check_storage mem vmem in
29172984
let xrt = XOp (XXlsh, [rt#to_expr floc]) in
2918-
let cmds = memcmds @ floc#get_assign_commands vmem xrt in
2985+
let cmds =
2986+
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
2987+
let xrn = rewrite_expr floc (rn#to_expr floc) in
2988+
let xrm = rewrite_expr floc (rm#to_expr floc) in
2989+
begin
2990+
ch_error_log#add
2991+
"assignment to unknown memory"
2992+
(LBLOCK [
2993+
floc#l#toPretty;
2994+
STR " STRH [";
2995+
rn#toPretty;
2996+
STR ", ";
2997+
rm#toPretty;
2998+
STR "]; base: ";
2999+
x2p xrn;
3000+
STR ", offset: ";
3001+
x2p xrm]);
3002+
[]
3003+
end
3004+
else
3005+
floc#get_assign_commands vmem xrt in
29193006
let usevars = get_register_vars [rt; rn; rm] in
29203007
let usehigh = get_use_high_vars [xrt] in
29213008
let (usevars, usehigh) =
@@ -2947,7 +3034,7 @@ let translate_arm_instruction
29473034
addr_r
29483035
else
29493036
[] in
2950-
let cmds = defcmds @ cmds @ updatecmds in
3037+
let cmds = memcmds @ defcmds @ cmds @ updatecmds in
29513038
(match c with
29523039
| ACCAlways -> default cmds
29533040
| _ -> make_conditional_commands c cmds)

‎CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHARMFunctionInterfaceTest.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,7 @@ let get_arm_struct_param_next_state_test () =
139139
(fun () ->
140140
let cinfo = bcfiles#get_compinfo_by_name title in
141141
let btype = get_compinfo_struct_type cinfo in
142-
let size = size_of_btype btype in
142+
let size = CHTraceResult.tget_ok (size_of_btype btype) in
143143
let (param, naas) =
144144
get_arm_struct_param_next_state
145145
size "arg_1" btype aas_start_state 1 in

0 commit comments

Comments
 (0)