Skip to content

Commit

Permalink
CHB:ARM add some memory resolution
Browse files Browse the repository at this point in the history
  • Loading branch information
@sipma
sipma committed Oct 5, 2024
1 parent 80a36bb commit a3a176c
Show file tree
Hide file tree
Showing 5 changed files with 145 additions and 20 deletions.
4 changes: 2 additions & 2 deletions CodeHawk/CHB/bchlib/bCHVersion.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,8 +95,8 @@ end


let version = new version_info_t
~version:"0.6.0_20241003"
~date:"2024-10-03"
~version:"0.6.0_20241005"
~date:"2024-10-05"
~licensee: None
~maxfilesize: None
()
22 changes: 22 additions & 0 deletions CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -406,6 +406,8 @@ object (self:'a)
XOp (XMult, [XOp (XDiv, [XVar rvar; alignx]); alignx])
else
XVar rvar in
(* memory addresses are not rewritten to preserve the structure of the
data accessed (in case of an non-optimizing compiler) *)
let addr = XOp (XPlus, [rvarx; memoff]) in
(* floc#inv#rewrite_expr addr *)
simplify_xpr addr
Expand Down Expand Up @@ -509,6 +511,26 @@ object (self:'a)
STR ": ivax: ";
x2p ivax])
(floc#f#env#mk_memory_address_deref_variable v)
| XOp (XPlus, [XVar basevar; XVar memoffset]) ->
let optmemvaraddr = floc#decompose_memvar_address xoffset in
(match optmemvaraddr with
| Some (memref, memoffset)
when BCHMemoryReference.is_constant_offset memoffset ->
(env#mk_index_offset_memory_variable memref memoffset,
[STR "ARMShiftedIndexOffset (decomposed)";
self#toPretty;
STR "; memref: ";
memref#toPretty;
STR "; memoffset: ";
BCHMemoryReference.memory_offset_to_pretty memoffset])
| _ ->
(env#mk_unknown_memory_variable "operand",
[STR "ARMShiftedIndexOffset (sum)";
self#toPretty;
STR "; basevar: ";
basevar#toPretty;
STR "; memoffset: ";
memoffset#toPretty]))
| _ ->
(env#mk_unknown_memory_variable "operand",
[STR "ARMShiftedIndexOffset";
Expand Down
16 changes: 16 additions & 0 deletions CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -513,6 +513,22 @@ object (self)

end

| LoadRegisterHalfword (_, rt, rn, rm, memop, _) when rm#is_immediate ->
let rtreg = rt#to_register in
let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in
begin
(* LDRH rt, [rn, rm] : X_rndef.load <: X_rt *)
(let xrdef = get_variable_rdefs (rn#to_variable floc) in
let rnreg = rn#to_register in
let offset = rm#to_numerical#toInt in
List.iter (fun rdsym ->
let ldaddr = rdsym#getBaseName in
let rdtypevar = mk_reglhs_typevar rnreg faddr ldaddr in
let rdtypevar = add_load_capability ~offset rdtypevar in
store#add_subtype_constraint
(mk_vty_term rdtypevar) (mk_vty_term rttypevar)) xrdef);
end

| LogicalShiftLeft (_, _, rd, rn, rm, _) when rm#is_immediate ->
let rdreg = rd#to_register in
let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in
Expand Down
121 changes: 104 additions & 17 deletions CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1680,13 +1680,15 @@ let translate_arm_instruction
let (lhs, cmds) = floc#get_ssa_assign_commands rtreg ~vtype rhs in
let cmds = cmds @ updatecmds in
let usevars = get_register_vars [rn; rm] in
let usevars =
let memvar = mem#to_variable floc in
if floc#f#env#is_unknown_memory_variable memvar then
usevars
let memvar = mem#to_variable floc in
let (usevars, usehigh) =
if memvar#isTmp || floc#f#env#is_unknown_memory_variable memvar then
(* elevate address variables to high-use *)
let xrn = rn#to_expr floc in
let xrm = rm#to_expr floc in
(usevars, get_use_high_vars [xrn; xrm])
else
memvar :: usevars in
let usehigh = get_use_high_vars [rhs] in
(memvar :: usevars, get_use_high_vars [rhs]) in
let defcmds =
floc#get_vardef_commands
~defs:[lhs]
Expand Down Expand Up @@ -1782,12 +1784,15 @@ let translate_arm_instruction
let vtype = t_ushort in
let (vrt, cmds) = floc#get_ssa_assign_commands rtreg ~vtype rhs in
let usevars = get_register_vars [rn; rm] in
let usevars =
if floc#f#env#is_unknown_memory_variable memvar then
usevars
let memvar = mem#to_variable floc in
let (usevars, usehigh) =
if memvar#isTmp || floc#f#env#is_unknown_memory_variable memvar then
(* elevate address variables to high-use *)
let xrn = rn#to_expr floc in
let xrm = rm#to_expr floc in
(usevars, get_use_high_vars [xrn; xrm])
else
memvar :: usevars in
let usehigh = get_use_high_vars [rhs] in
(memvar :: usevars, get_use_high_vars [rhs]) in
let defcmds =
floc#get_vardef_commands
~defs:[vrt]
Expand Down Expand Up @@ -2747,7 +2752,27 @@ let translate_arm_instruction
let _ = check_storage mem vmem in
let xrt = rt#to_expr floc in
let xrt = floc#inv#rewrite_expr xrt in
let cmds = memcmds @ (floc#get_assign_commands vmem xrt) in
let cmds =
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
let xrn = rewrite_expr floc (rn#to_expr floc) in
let xrm = rewrite_expr floc (rm#to_expr floc) in
begin
ch_error_log#add
"assignment to unknown memory"
(LBLOCK [
floc#l#toPretty;
STR " STR [";
rn#toPretty;
STR ", ";
rm#toPretty;
STR "]; base: ";
x2p xrn;
STR ", offset: ";
x2p xrm]);
[]
end
else
floc#get_assign_commands vmem xrt in
let usevars = get_register_vars [rt; rn; rm] in
let usehigh = get_use_high_vars [xrt] in
let (usevars, usehigh) =
Expand Down Expand Up @@ -2779,7 +2804,7 @@ let translate_arm_instruction
addr_r
else
[] in
let cmds = defcmds @ cmds @ updatecmds in
let cmds = memcmds @ defcmds @ cmds @ updatecmds in
let _ =
(* record register spill *)
let vrt = rt#to_variable floc in
Expand All @@ -2794,7 +2819,27 @@ let translate_arm_instruction
let (vmem, memcmds) = mem#to_lhs floc in
let _ = check_storage mem vmem in
let xrt = XOp (XXlsb, [rt#to_expr floc]) in
let cmds = floc#get_assign_commands vmem xrt in
let cmds =
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
let xrn = rewrite_expr floc (rn#to_expr floc) in
let xrm = rewrite_expr floc (rm#to_expr floc) in
begin
ch_error_log#add
"assignment to unknown memory"
(LBLOCK [
floc#l#toPretty;
STR " STRB [";
rn#toPretty;
STR ", ";
rm#toPretty;
STR "]; base: ";
x2p xrn;
STR ", offset: ";
x2p xrm]);
[]
end
else
floc#get_assign_commands vmem xrt in
let usevars = get_register_vars [rt; rn; rm] in
let usehigh = get_use_high_vars [xrt] in
let (usevars, usehigh) =
Expand Down Expand Up @@ -2895,9 +2940,31 @@ let translate_arm_instruction
let _ = check_storage mem vmem in
let rdreg = rd#to_register in
let xrt = rt#to_expr floc in
let cmds = floc#get_assign_commands vmem xrt in
let cmds =
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
let xrn = rewrite_expr floc (rn#to_expr floc) in
begin
ch_error_log#add
"assignment to unknown memory"
(LBLOCK [
floc#l#toPretty;
STR " STREX [";
rn#toPretty;
STR "]; base: ";
x2p xrn]);
[]
end
else
floc#get_assign_commands vmem xrt in
let usevars = get_register_vars [rt; rn] in
let usehigh = get_use_high_vars [xrt] in
let (usevars, usehigh) =
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
(* elevate address variables to high-use *)
let xrn = rn#to_expr floc in
(usevars, get_addr_use_high_vars [xrn])
else
(vmem :: usevars, usehigh) in
let (vrd, scmds) = floc#get_ssa_abstract_commands rdreg () in
let defcmds =
floc#get_vardef_commands
Expand All @@ -2915,7 +2982,27 @@ let translate_arm_instruction
let (vmem, memcmds) = mem#to_lhs floc in
let _ = check_storage mem vmem in
let xrt = XOp (XXlsh, [rt#to_expr floc]) in
let cmds = memcmds @ floc#get_assign_commands vmem xrt in
let cmds =
if vmem#isTmp || floc#f#env#is_unknown_memory_variable vmem then
let xrn = rewrite_expr floc (rn#to_expr floc) in
let xrm = rewrite_expr floc (rm#to_expr floc) in
begin
ch_error_log#add
"assignment to unknown memory"
(LBLOCK [
floc#l#toPretty;
STR " STRH [";
rn#toPretty;
STR ", ";
rm#toPretty;
STR "]; base: ";
x2p xrn;
STR ", offset: ";
x2p xrm]);
[]
end
else
floc#get_assign_commands vmem xrt in
let usevars = get_register_vars [rt; rn; rm] in
let usehigh = get_use_high_vars [xrt] in
let (usevars, usehigh) =
Expand Down Expand Up @@ -2947,7 +3034,7 @@ let translate_arm_instruction
addr_r
else
[] in
let cmds = defcmds @ cmds @ updatecmds in
let cmds = memcmds @ defcmds @ cmds @ updatecmds in
(match c with
| ACCAlways -> default cmds
| _ -> make_conditional_commands c cmds)
Expand Down
2 changes: 1 addition & 1 deletion CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHARMFunctionInterfaceTest.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ let get_arm_struct_param_next_state_test () =
(fun () ->
let cinfo = bcfiles#get_compinfo_by_name title in
let btype = get_compinfo_struct_type cinfo in
let size = size_of_btype btype in
let size = CHTraceResult.tget_ok (size_of_btype btype) in
let (param, naas) =
get_arm_struct_param_next_state
size "arg_1" btype aas_start_state 1 in
Expand Down

0 comments on commit a3a176c

Please sign in to comment.