From 475a13ca85bcc8d4889fed4a0c321d95e186421e Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 10 Aug 2025 19:11:20 -0700 Subject: [PATCH 1/6] CHB:ARM: add return value use definitions only for non-void functions --- CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 8f91dd52..2c29e2e0 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -867,11 +867,16 @@ let translate_arm_instruction | Branch (_, op, _) | BranchExchange (ACCAlways, op) when op#is_register && op#get_register = ARLR -> - let r0_op = arm_register_op AR0 RD in - let usevars = get_register_vars [r0_op] in - let xr0 = r0_op#to_expr floc in - let usehigh = get_use_high_vars_r [xr0] in - let defcmds = floc#get_vardef_commands ~use:usevars ~usehigh ctxtiaddr in + let returntype = finfo#get_summary#get_returntype in + let defcmds = + match returntype with + | TVoid _ -> [] + | _ -> + let r0_op = arm_register_op AR0 RD in + let usevars = get_register_vars [r0_op] in + let xr0 = r0_op#to_expr floc in + let usehigh = get_use_high_vars_r [xr0] in + floc#get_vardef_commands ~use:usevars ~usehigh ctxtiaddr in default defcmds | Branch (_, op, _) From c722ab3baf48c39c7d4aa793b08795c29a206909 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 10 Aug 2025 19:17:21 -0700 Subject: [PATCH 2/6] CHB:ARM: convert LDM/STM argument to address-of-var --- .../CHB/bchlibarm32/bCHFnARMDictionary.ml | 21 +++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index c681f376..7dab6354 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -685,7 +685,14 @@ object (self) | XVar _ -> xx | _ -> TR.tfold - ~ok:(fun v -> XOp ((Xf "addressofvar"), [(XVar v)])) + ~ok:(fun v -> + let _ = + log_diagnostics_result + ~msg:(p2s floc#l#toPretty) + ~tag:"callinstr-key:get-var-at-address" + __FILE__ __LINE__ + ["xx: " ^ (x2s xx); "v: " ^ (p2s v#toPretty)] in + XOp ((Xf "addressofvar"), [(XVar v)])) ~error:(fun e -> let _ = log_dc_error_result __FILE__ __LINE__ e in xx) @@ -2787,10 +2794,20 @@ object (self) let xdst_r = dstop#to_expr floc in let xxsrc_r = TR.tmap (rewrite_floc_expr srcfloc) xsrc_r in let xxdst_r = TR.tmap (rewrite_expr ?restrict:(Some 4)) xdst_r in + let xxdst_r = + TR.tmap + (fun x -> + TR.tfold + ~ok:(fun v -> XOp ((Xf "addressofvar"), [(XVar v)])) + ~error:(fun e -> + let _ = log_dc_error_result __FILE__ __LINE__ e in + x) + (floc#get_var_at_address ~btype:t_int x)) + xxdst_r in let csrc_r = TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xxsrc_r in let cdst_r = - TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xdst_r in + TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) xxdst_r in let rdefs = [(get_rdef_r xsrc_r); (get_rdef_r xdst_r)] in let xprs_r = [xdst_r; xsrc_r; xxdst_r; xxsrc_r] in let cxprs_r = [cdst_r; csrc_r] in From f0528e7061355d32590d9f734ad8672ca59b1f92 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 10 Aug 2025 19:18:13 -0700 Subject: [PATCH 3/6] CHB:ARM: add typing rule for BX LR --- .../bchlibarm32/bCHFnARMTypeConstraints.ml | 63 ++++++++++++++++++- 1 file changed, 61 insertions(+), 2 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 2574e3b2..0d399f43 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -280,6 +280,16 @@ object (self) linenumber [(p2s floc#l#toPretty) ^ ": " ^ (type_constraint_to_string tc)] in + let operand_is_stackpointer (op: arm_operand_int): bool = + TR.tfold_default + (fun v -> + match v with + | XVar v when finfo#env#is_initial_stackpointer_value v -> true + | XOp (XMinus, [XVar v; _]) -> finfo#env#is_initial_stackpointer_value v + | _ -> false) + false + (TR.tmap rewrite_expr (op#to_expr floc)) in + let operand_is_zero (op: arm_operand_int): bool = (* Returns true if the value of the operand is known to be zero at this location. This result is primarily intended to avoid spurious @@ -508,10 +518,9 @@ object (self) end | BitwiseNot(_, _, rd, rm, _) when rm#is_immediate -> - let rmval = rm#to_numerical#toInt in let rdreg = rd#to_register in let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in - let tyc = get_intvalue_type_constant rmval in + let tyc = mk_int_type_constant Signed 32 in begin (regvar_type_introduction "MVN" rd); (regvar_linked_to_exit "MVN" rd); @@ -583,6 +592,53 @@ object (self) (* no type information gained *) () + | BranchExchange (ACCAlways, op) + when op#is_register && op#get_register = ARLR -> + let returntype = finfo#get_summary#get_returntype in + (match returntype with + | TVoid _ -> () + | _ -> + let reg = register_of_arm_register AR0 in + let typevar = mk_reglhs_typevar reg faddr iaddr in + begin + (* use function return type *) + (let opttc = mk_btype_constraint typevar returntype in + let rule = "BXLR-sig-rv" in + match opttc with + | Some tc -> + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc + end + else + log_type_constraint_rule_disabled __LINE__ rule tc + | _ -> + begin + log_no_type_constraint __LINE__ rule returntype; + () + end); + + (* propagate via reaching defs *) + (let r0var = floc#env#mk_arm_register_variable AR0 in + let r0defs = get_variable_rdefs r0var in + let rule = "BXLR-rdef" in + List.iter (fun r0def -> + let r0addr = r0def#getBaseName in + let r0typevar = mk_reglhs_typevar reg faddr r0addr in + let r0typeterm = mk_vty_term r0typevar in + let lhstypeterm = mk_vty_term typevar in + if fndata#is_typing_rule_enabled ~rdef:(Some r0addr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule r0typeterm lhstypeterm; + store#add_subtype_constraint + faddr iaddr rule r0typeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule r0typeterm lhstypeterm + ) r0defs) + end) + | BranchLink _ | BranchLinkExchange _ when floc#has_call_target && floc#get_call_target#is_signature_valid -> let log_error (msg: string) = @@ -1598,6 +1654,9 @@ object (self) else if rd#is_sp_register && rn#is_sp_register then (* no type information to be gained from stackpointer manipulations *) () + else if operand_is_stackpointer rn then + (* idem for pointers to the stack in other registers *) + () else let rule = "SUB-rdef" in List.iter (fun rnsym -> From 4e6641a7474360b636ee8c52aa4666382816b3ef Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 10 Aug 2025 19:55:25 -0700 Subject: [PATCH 4/6] CHB:USER: add remove-reaching-defs to function annotation --- CodeHawk/CHB/bchlib/bCHFunctionData.ml | 115 +++++++++++++++++++++++-- 1 file changed, 110 insertions(+), 5 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFunctionData.ml b/CodeHawk/CHB/bchlib/bCHFunctionData.ml index 7fd01d6c..5c8fa929 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionData.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionData.ml @@ -28,6 +28,7 @@ ============================================================================= *) (* chlib *) +open CHLanguage open CHPretty (* chutil *) @@ -50,6 +51,7 @@ open BCHLibTypes module H = Hashtbl module TR = CHTraceResult +let p2s = CHPrettyUtil.pretty_to_string let bd = BCHDictionary.bdictionary @@ -76,10 +78,41 @@ let stackvar_intro_to_string (svi: stackvar_intro_t) = (string_of_int svi.svi_offset) ^ ": " ^ svi.svi_name ^ ptype +let reachingdef_spec_to_string (rds: reachingdef_spec_t) = + let uselocs = "[" ^ (String.concat ", " rds.rds_uselocs) ^ "]" in + let rdeflocs = "[" ^ (String.concat ", " rds.rds_rdeflocs) ^ "]" in + rds.rds_variable ^ ": use: " ^ uselocs ^ "; remove-rdefs: " ^ rdeflocs + + let function_annotation_to_string (a: function_annotation_t) = - (String.concat "\n" (List.map regvar_intro_to_string a.regvarintros)) - ^ "\n" - ^ (String.concat "\n" (List.map stackvar_intro_to_string a.stackvarintros)) + let rvintros = + if (List.length a.regvarintros) > 0 then + ("Register-variable-introductions: [" + ^ (String.concat "; " (List.map regvar_intro_to_string a.regvarintros)) + ^ "]") + else + "" in + let svintros = + if (List.length a.stackvarintros) > 0 then + ("Stack-variable-introductions: [" + ^ (String.concat "; " (List.map stackvar_intro_to_string a.stackvarintros)) + ^ "]") + else + "" in + let rdefspecs = + if (List.length a.reachingdefspecs) > 0 then + ("Reaching-def-specs: [" + ^ (String.concat "; " (List.map reachingdef_spec_to_string a.reachingdefspecs)) + ^ "]") + else + "" in + List.fold_left (fun acc s -> + if s = "" then + acc + else if acc = "" then + s + else + acc ^ "\n" ^ s) "" [rvintros; svintros; rdefspecs] class function_data_t (fa:doubleword_int) = @@ -156,7 +189,8 @@ object (self) functionannotation <- Some a; chlog#add "function annotation" - (LBLOCK [faddr#toPretty; NL; STR (function_annotation_to_string a)]) + (LBLOCK [STR "function "; faddr#toPretty; STR ": "; + STR (function_annotation_to_string a)]) end method has_function_annotation: bool = @@ -314,6 +348,36 @@ object (self) else BCHSystemSettings.system_settings#is_typing_rule_enabled name + method filter_deflocs + (iaddr: string) (v: variable_t) (deflocs: symbol_t list): symbol_t list = + match self#get_function_annotation with + | None -> deflocs + | Some a when (List.length a.reachingdefspecs) > 0 -> + let vname = v#getName#getBaseName in + let deflocs = + List.fold_left + (fun acc sym -> + let symname = sym#getBaseName in + if (List.fold_left + (fun filteracc rds -> + filteracc || + (if rds.rds_variable = vname then + (List.mem iaddr rds.rds_uselocs) + && (List.mem symname rds.rds_rdeflocs) + else + false)) false a.reachingdefspecs) then + let _ = + log_result + ~msg:("iaddr: " ^ iaddr) + ~tag:"filter out reaching def" + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); "s; " ^ symname] in + acc + else + sym :: acc) [] deflocs in + List.rev deflocs + | _ -> deflocs + method add_inlined_block (baddr:doubleword_int) = inlined_blocks <- baddr :: inlined_blocks @@ -645,6 +709,28 @@ let read_xml_typing_rule (node: xml_element_int): typing_rule_t traceresult = tra_locations = locs} +let read_xml_reachingdef_spec + (node: xml_element_int): reachingdef_spec_t traceresult = + let get = node#getAttribute in + let has = node#hasNamedAttribute in + if not (has "var") then + Error ["rdefspec without var"] + else if not (has "uselocs") then + Error ["rdefspec without uselocs"] + else if not (has "rdeflocs") then + Error ["rdefspec without rdeflocs"] + else + let var = get "var" in + let uselocs = get "uselocs" in + let uselocs = String.split_on_char ',' uselocs in + let rdeflocs = get "rdeflocs" in + let rdeflocs = String.split_on_char ',' rdeflocs in + Ok {rds_variable = var; + rds_uselocs = uselocs; + rds_rdeflocs = rdeflocs + } + + let read_xml_function_annotation (node: xml_element_int) = let get = node#getAttribute in let getc = node#getTaggedChild in @@ -705,10 +791,29 @@ let read_xml_function_annotation (node: xml_element_int) = (trules#getTaggedChildren "typingrule") else [] in + let rdefspecs = + if hasc "remove-rdefs" then + let rrds = getc "remove-rdefs" in + List.fold_left + (fun acc n -> + TR.tfold + ~ok:(fun rds -> rds :: acc) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ e; + acc + end) + (read_xml_reachingdef_spec n)) + [] + (rrds#getTaggedChildren "remove-var-rdefs") + else + [] in fndata#set_function_annotation {regvarintros = regvintros; stackvarintros = stackvintros; - typingrules = typingrules} + typingrules = typingrules; + reachingdefspecs = rdefspecs + } else log_error_result ~tag:"function annotation faddr not found" From a78c23b14e514680f7da9d1b2cd0896c214b716a Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Sun, 10 Aug 2025 19:59:37 -0700 Subject: [PATCH 5/6] CHB:TYPE: remove handling of void pointer --- CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml index b80ea612..62697c58 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml @@ -443,8 +443,7 @@ let rec mk_btype_constraint (tv: type_variable_t) (ty: btype_t) | TComp (key, _) -> let cinfo = bcfiles#get_compinfo key in Some (TyGround (TyVariable tv, TyConstant (TyTStruct (key, cinfo.bcname)))) - | TPtr (TVoid _, _) -> - Some (TyGround (TyVariable tv, TyConstant TyVoidPtr)) + | TPtr (TVoid _, _) -> None | TPtr (pty, _) -> let ptv = add_deref_capability tv in mk_btype_constraint ptv pty From afa1db5e1c37bf61b5956166c436b51c03b50f06 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Mon, 11 Aug 2025 00:37:51 -0700 Subject: [PATCH 6/6] CHB: incorporate more type info in constructing memory offsets --- CodeHawk/CHB/bchlib/bCHFloc.ml | 28 +++++++++++++++---- CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 5 ++++ CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml | 26 +++++++++++++++++ CodeHawk/CHB/bchlib/bCHLibTypes.mli | 18 ++++++++++-- CodeHawk/CHB/bchlib/bCHMemoryReference.ml | 16 +++++++++++ CodeHawk/CHB/bchlib/bCHSystemSettings.ml | 2 ++ CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +-- .../bchlibarm32/bCHARMInstructionAggregate.ml | 8 +++++- 8 files changed, 96 insertions(+), 11 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 88a2a0f1..537b3d9d 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -1499,7 +1499,7 @@ object (self) | XConst (IntConst n) when n#equal (mkNumerical 0xffffffff) && is_int t -> Ok (int_constant_expr (-1)) - | _ -> self#convert_xpr_offsets ~size x + | _ -> self#convert_xpr_offsets ~xtype ~size x method convert_addr_to_c_pointed_to_expr ?(size=None) ?(xtype=None) (a: xpr_t): xpr_t traceresult = @@ -1656,12 +1656,13 @@ object (self) method convert_variable_offsets - ?(size=None) (v: variable_t): variable_t traceresult = + ?(vtype=None) ?(size=None) (v: variable_t): variable_t traceresult = if self#env#is_basevar_memory_variable v then let basevar_r = self#env#get_memvar_basevar v in let offset_r = self#env#get_memvar_offset v in let cbasevar_r = TR.tbind self#convert_value_offsets basevar_r in let basetype_r = TR.tbind self#get_variable_type cbasevar_r in + let optvtype = match vtype with Some t -> t | _ -> t_unknown in let tgttype_r = TR.tbind ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) @@ -1682,8 +1683,18 @@ object (self) ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) (fun tgttype -> address_memory_offset - ~tgtsize:size tgttype (num_constant_expr n)) tgttype_r + ~tgtbtype:optvtype ~tgtsize:size tgttype (num_constant_expr n)) + tgttype_r | _ -> Ok offset) offset_r in + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"convert-variable-offsets" + __FILE__ __LINE__ + ["tgttype: " ^ (TR.tfold_default btype_to_string "?" tgttype_r); + "tgtbtype: " ^ (btype_to_string optvtype); + "offset : " ^ (TR.tfold_default memory_offset_to_string "?" offset_r); + "coffset: " ^ (TR.tfold_default memory_offset_to_string "?" coffset_r)] in TR.tbind ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty)) (fun cbasevar -> @@ -1776,7 +1787,8 @@ object (self) ["v: " ^ (p2s v#toPretty)] in Ok v - method convert_xpr_offsets ?(size=None) (x: xpr_t): xpr_t traceresult = + method convert_xpr_offsets + ?(xtype=None) ?(size=None) (x: xpr_t): xpr_t traceresult = let rec aux exp = match exp with | XVar v when self#env#is_basevar_memory_value v -> @@ -1789,10 +1801,16 @@ object (self) ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) (fun v -> XVar v) (self#convert_variable_offsets ~size v) | XOp ((Xf "addressofvar"), [XVar v]) -> + let derefty = + match xtype with + | None -> None + | Some (TPtr (ty, _)) -> Some ty + | _ -> None in let newx_r = TR.tmap ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun v -> XVar v) (self#convert_variable_offsets ~size v) in + (fun v -> + XVar v) (self#convert_variable_offsets ~vtype:derefty ~size v) in TR.tmap (fun newx -> match newx with diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 2a1ebb01..19e705f6 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1718,6 +1718,11 @@ object (self) method add_reaching_def (iaddr: string) (v: variable_t) (deflocs: symbol_t list) = begin + let deflocs = + if fndata#has_function_annotation then + fndata#filter_deflocs iaddr v deflocs + else + deflocs in self#fvarinv#add_reaching_def iaddr v deflocs; List.iter (fun s -> if (List.length s#getAttributes) = 0 then diff --git a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml index a9343b2b..e9dd1fee 100644 --- a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml +++ b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml @@ -198,6 +198,18 @@ object (self) ~(tgtbtype: btype_t option) (c: bcompinfo_t) (xoffset: xpr_t): memory_offset_t traceresult = + let _ = + log_diagnostics_result + ~tag:"global:get-field-memory-offset-at" + __FILE__ __LINE__ + ["tgtsize: " + ^ (if Option.is_some tgtsize then + string_of_int (Option.get tgtsize) else "?"); + "tgtbtype: " + ^ (if Option.is_some tgtbtype then + btype_to_string (Option.get tgtbtype) else "?"); + "compinfo: " ^ c.bcname; + "xoffset: " ^ (x2s xoffset)] in let is_void_tgtbtype = match tgtbtype with | Some (TVoid _) -> true @@ -368,6 +380,20 @@ object (self) ~(tgtbtype: btype_t option) (btype: btype_t) (xoffset: xpr_t): memory_offset_t traceresult = + let _ = + log_diagnostics_result + ~tag:"global:arrayvar-memory-offset" + __FILE__ __LINE__ + ["tgtsize: " ^ (if (Option.is_some tgtsize) then + string_of_int (Option.get tgtsize) + else + "?"); + "tgtbtype: " ^ (if (Option.is_some tgtbtype) then + btype_to_string (Option.get tgtbtype) + else + "?"); + "btype: " ^ (btype_to_string btype); + "xoffset: " ^ (x2s xoffset)] in let iszero x = match x with | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 298de577..ac3a46e2 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1518,11 +1518,18 @@ type typing_rule_t = { tra_locations: string list } +type reachingdef_spec_t = { + rds_variable: string; + rds_uselocs: string list; + rds_rdeflocs: string list + } + type function_annotation_t = { regvarintros: regvar_intro_t list; stackvarintros: stackvar_intro_t list; - typingrules: typing_rule_t list + typingrules: typing_rule_t list; + reachingdefspecs: reachingdef_spec_t list } class type function_data_int = @@ -1575,6 +1582,7 @@ class type function_data_int = method has_regvar_type_cast: doubleword_int -> bool method has_stackvar_type_annotation: int -> bool method has_stackvar_type_cast: int -> bool + method filter_deflocs: string -> variable_t -> symbol_t list -> symbol_t list method is_typing_rule_enabled: ?rdef:string option -> string -> string -> bool method has_class_info: bool method has_callsites: bool @@ -6102,9 +6110,13 @@ class type floc_int = ?size:int option -> variable_t -> variable_t traceresult method convert_variable_offsets: - ?size:int option -> variable_t -> variable_t traceresult + ?vtype:btype_t option + -> ?size:int option + -> variable_t + -> variable_t traceresult - method convert_xpr_offsets: ?size:int option -> xpr_t -> xpr_t traceresult + method convert_xpr_offsets: + ?xtype:btype_t option -> ?size:int option -> xpr_t -> xpr_t traceresult (* returns the variable associated with the address expression *) method get_lhs_from_address: xpr_t -> variable_t diff --git a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml index 57f0ac5f..2ba844bd 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml +++ b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml @@ -256,7 +256,23 @@ and structvar_memory_offset ~(tgtbtype: btype_t option) (btype: btype_t) (xoffset: xpr_t): memory_offset_t traceresult = + let _ = + log_diagnostics_result + ~tag:"structvar-memory-offset" + __FILE__ __LINE__ + ["tgtsize: " + ^ (if Option.is_some tgtsize then (string_of_int (Option.get tgtsize)) else "?"); + "tgtbtype: " + ^ (if Option.is_some tgtbtype then (btype_to_string (Option.get tgtbtype)) + else "?"); + "btype: " ^ (btype_to_string btype); + "xoffset: " ^ (x2s xoffset)] in match xoffset with + | XConst (IntConst n) + when n#equal numerical_zero + && (Option.is_some tgtbtype) + && (btype_equal (Option.get tgtbtype) btype) -> + Ok NoOffset | XConst (IntConst _) -> if is_struct_type btype then let compinfo = get_struct_type_compinfo btype in diff --git a/CodeHawk/CHB/bchlib/bCHSystemSettings.ml b/CodeHawk/CHB/bchlib/bCHSystemSettings.ml index 6578e247..b7c4f6fe 100644 --- a/CodeHawk/CHB/bchlib/bCHSystemSettings.ml +++ b/CodeHawk/CHB/bchlib/bCHSystemSettings.ml @@ -59,6 +59,7 @@ let _ = ("ADD-c", "enable"); ("AND-rdef", "enable"); ("ASR-rdef", "enable"); + ("BXLR-rdef", "enable"); ("CMP-rdef", "enable"); ("LSL_rdef", "enable"); ("LSR_rdef", "enable"); @@ -111,6 +112,7 @@ let _ = ("BL-sig-regarg", "enable"); ("BL-sig-stackarg", "enable"); ("BL-sig-rv", "enable"); + ("BXLR-sig-rv", "enable"); ("LDR-array", "enable"); ("LDR-memop-tc", "enable"); ("LDR-stack-addr", "enable"); diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index e1b2189e..7cad9618 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_20250805" - ~date:"2025-08-05" + ~version:"0.6.0_20250810" + ~date:"2025-08-10" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml index 9c2bbadb..33d80fd9 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml @@ -50,6 +50,8 @@ open BCHThumbITSequence module TR = CHTraceResult +let p2s = CHPrettyUtil.pretty_to_string + let arm_aggregate_kind_to_string (k: arm_aggregate_kind_t) = match k with @@ -180,7 +182,11 @@ let make_arm_instruction_aggregate let agg = new arm_instruction_aggregate_t ~kind ~instrs ~entry ~exitinstr ~anchor in begin - chlog#add "aggregate instruction" agg#toPretty; + log_diagnostics_result + ~msg:(anchor#get_address#to_hex_string) + ~tag:"aggregate instruction" + __FILE__ __LINE__ + [(p2s agg#toPretty)]; agg end