From a3a176c297d494919f10cd6d2f49c1f8685d6468 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sat, 5 Oct 2024 15:32:41 -0700 Subject: [PATCH] CHB:ARM add some memory resolution --- CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +- CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml | 22 ++++ .../bchlibarm32/bCHFnARMTypeConstraints.ml | 16 +++ .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 121 +++++++++++++++--- .../txbchlib/bCHARMFunctionInterfaceTest.ml | 2 +- 5 files changed, 145 insertions(+), 20 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index ebdd7add..09149343 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -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 () diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml index b1d91b8f..748c6aa7 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml @@ -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 @@ -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"; diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 261d9e8f..307f1e1d 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -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 diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 3ddbb62d..7a6a8637 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -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] @@ -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] @@ -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) = @@ -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 @@ -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) = @@ -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 @@ -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) = @@ -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) diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHARMFunctionInterfaceTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHARMFunctionInterfaceTest.ml index c6e5e916..332c4fe5 100644 --- a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHARMFunctionInterfaceTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHARMFunctionInterfaceTest.ml @@ -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