diff --git a/CodeHawk/CHB/bchcil/bCHParseCilFile.ml b/CodeHawk/CHB/bchcil/bCHParseCilFile.ml index 37b7ee6d..3987d4c0 100644 --- a/CodeHawk/CHB/bchcil/bCHParseCilFile.ml +++ b/CodeHawk/CHB/bchcil/bCHParseCilFile.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -52,10 +52,10 @@ let update_symbolic_address_types () = else match BCHGlobalMemoryMap.update_global_location_type vinfo with | Error e -> - ch_error_log#add - "update-global-location-type" - (LBLOCK [ - STR "varinfo: "; STR vinfo.bvname; STR (String.concat "; " e)]) + log_diagnostics_result + ~tag:"update global location type" + __FILE__ __LINE__ + ["varinfo: " ^ vinfo.bvname ^ (String.concat "; " e)] | _ -> ()) varinfos diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml index 0efa14c9..7517afc5 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml @@ -1148,8 +1148,21 @@ let record_function_interface_type_constraints | [RegisterParameter (reg, _)] -> let pvar = add_freg_param_capability reg ftypevar in (match mk_btype_constraint pvar ty with - | Some tyc -> store#add_constraint tyc - | _ -> ()) + | Some tyc -> + let _ = + log_diagnostics_result + ~tag:("function-interface type constraint") + __FILE__ __LINE__ + [faddr ^ ": " ^ (type_constraint_to_string tyc)] in + store#add_constraint tyc + | _ -> + chlog#add + "function interface type constraints" + (LBLOCK [ + STR faddr; + STR ": "; + STR "unable to make type constraint for "; + STR (type_variable_to_string pvar)])) | _ -> chlog#add "function interface type constraints" diff --git a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml index 773c3857..57f0ac5f 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml +++ b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml @@ -212,8 +212,12 @@ let rec address_memory_offset __FILE__ __LINE__ ["base type: " ^ (btype_to_string rbasetype) ^ "; xoffset: " ^ n#toString] in - (* Ok (ConstantOffset (n, NoOffset)) *) - Ok (BasePtrArrayIndexOffset (num_constant_expr n, NoOffset)) + TR.tmap + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (fun size -> + let scaledoffset = n#div (mkNumerical size) in + BasePtrArrayIndexOffset (num_constant_expr scaledoffset, NoOffset)) + (size_of_btype rbasetype) | _ -> let tgtbtype = if is_unknown_type tgtbtype then None else Some tgtbtype in @@ -231,7 +235,15 @@ let rec address_memory_offset Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "Unable to extract index from " ^ (x2s xoffset)] | Some (indexxpr, xrem) when iszero xrem -> - Ok (BasePtrArrayIndexOffset (indexxpr, NoOffset)) + let _ = + log_diagnostics_result + ~msg:"address-memory-offset:scalar basetype" + __FILE__ __LINE__ + ["base type: " ^ (btype_to_string rbasetype) + ^ "; xoffset: " ^ (x2s xoffset)] in + let scaledoffset = XOp (XDiv, [indexxpr; int_constant_expr tsize]) in + let scaledoffset = Xsimplify.simplify_xpr scaledoffset in + Ok (BasePtrArrayIndexOffset (scaledoffset, NoOffset)) | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "Nonzero suboffset encountered when extracting index " diff --git a/CodeHawk/CHB/bchlib/bCHSystemInfo.ml b/CodeHawk/CHB/bchlib/bCHSystemInfo.ml index a84c9141..3114d760 100644 --- a/CodeHawk/CHB/bchlib/bCHSystemInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHSystemInfo.ml @@ -1647,15 +1647,12 @@ object (self) method add_data_block (db:data_block_int) = begin data_blocks#add db; - (if collect_diagnostics () then - chlog#add - "add data block" - (LBLOCK [ - db#get_start_address#toPretty; - STR " - "; - db#get_end_address#toPretty; - STR ": "; - STR db#get_name])) + log_diagnostics_result + ~tag:"add data block" + __FILE__ __LINE__ + [db#get_start_address#to_hex_string ^ " - " + ^ db#get_end_address#to_hex_string ^ ": " + ^ db#get_name] end method get_data_blocks = data_blocks#toList diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml index 57d1ed5d..a502e171 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024 Aarno Labs LLC + Copyright (c) 2024-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -47,6 +47,8 @@ let bcd = BCHBCDictionary.bcdictionary let bd = BCHDictionary.bdictionary let tcd = BCHTypeConstraintDictionary.type_constraint_dictionary +let p2s = CHPrettyUtil.pretty_to_string + class type_constraint_store_t: type_constraint_store_int = object (self) @@ -250,14 +252,12 @@ object (self) result := !result @ (List.map tcd#get_type_constraint tcs)) iaddrentry in let _ = - chlog#add - "stack lhs constraints" - (LBLOCK [ - INT offset; - STR ": "; - pretty_print_list !result - (fun tc -> STR (type_constraint_to_string tc)) - "[" "; " "]"]) in + log_diagnostics_result + ~tag:("stack lhs constraints for " ^ faddr) + __FILE__ __LINE__ + [(string_of_int offset) ^ ": [" + ^ (String.concat "; " (List.map type_constraint_to_string !result)) + ^ "]"] in !result else [] @@ -439,28 +439,25 @@ object (self) let evaluation = self#evaluate_reglhs_type reg faddr iaddr in let logresults = iaddr = "0xffffffff" in let log_evaluation () = - chlog#add - ("reglhs resolution was not successfull:" ^ faddr) - (LBLOCK [ - STR iaddr; - STR " - "; - STR (register_to_string reg); - STR ": "; - pretty_print_list - evaluation - (fun (vars, consts) -> - LBLOCK [ - STR "vars: "; - pretty_print_list - vars - (fun v -> STR (type_variable_to_string v)) - "[" "; " "]"; - STR "; consts: "; - pretty_print_list - consts - (fun c -> STR (type_constant_to_string c)) - "[" "; " "]"; - NL]) "[[" " -- " "]]"]) in + log_diagnostics_result + ~tag:("reglhs resolution not successfull for " ^ faddr) + __FILE__ __LINE__ + [iaddr ^ " - " ^ (register_to_string reg) ^ ": " + ^ (p2s (pretty_print_list + evaluation + (fun (vars, consts) -> + LBLOCK [ + STR "vars: "; + pretty_print_list + vars + (fun v -> STR (type_variable_to_string v)) + "[" "; " "]"; + STR "; consts: "; + pretty_print_list + consts + (fun c -> STR (type_constant_to_string c)) + "[" "; " "]"; + NL]) "[[" " -- " "]]"))] in let result = new IntCollections.set_t in begin List.iter (fun (vars, consts) -> @@ -499,16 +496,13 @@ object (self) | _ -> begin log_evaluation (); - chlog#add - "top type constant in join" - (LBLOCK [ - STR iaddr; - STR " --- "; - STR (register_to_string reg); - STR ": "; - pretty_print_list - (List.map bcd#get_typ result#toList) - (fun ty -> STR (btype_to_string ty)) "[" "; " "]"]); + log_diagnostics_result + ~tag:("top type constant in join for " ^ faddr) + __FILE__ __LINE__ + [iaddr ^ " -- " ^ (register_to_string reg) ^ ": " + ^ (p2s (pretty_print_list + (List.map bcd#get_typ result#toList) + (fun ty -> STR (btype_to_string ty)) "[" "; " "]"))]; None end end @@ -517,26 +511,25 @@ object (self) (offset: int) (faddr: string): btype_t option = let evaluation = self#evaluate_stack_lhs_type offset faddr in let log_evaluation () = - chlog#add - ("stacklhs resolution was not successfull:" ^ faddr) - (LBLOCK [ - INT offset; - STR ": "; - pretty_print_list - evaluation - (fun (vars, consts) -> - LBLOCK [ - STR "vars: "; - pretty_print_list - vars - (fun v -> STR (type_variable_to_string v)) - "[" "; " "]"; - STR "; consts: "; - pretty_print_list - consts - (fun c -> STR (type_constant_to_string c)) - "[" "; " "]"; - NL]) "[[" " -- " "]]"]) in + log_diagnostics_result + ~tag:("stacklhs resolution was not successful for " ^ faddr) + __FILE__ __LINE__ + [(string_of_int offset) ^ ": " + ^ (p2s (pretty_print_list + evaluation + (fun (vars, consts) -> + LBLOCK [ + STR "vars: "; + pretty_print_list + vars + (fun v -> STR (type_variable_to_string v)) + "[" "; " "]"; + STR "; consts: "; + pretty_print_list + consts + (fun c -> STR (type_constant_to_string c)) + "[" "; " "]"; + NL]) "[[" " -- " "]]"))] in let first_field_struct (s: IntCollections.set_t): btype_t option = (* The type of a data item at a particular stack offset can legally be both a struct and the type of the first field of the struct. @@ -566,19 +559,16 @@ object (self) let _ixftype = bcd#index_typ ftype in let _ixctype = bcd#index_typ ty in let _ = - chlog#add - "first field struct check" - (LBLOCK [ - INT offset; - STR ": "; - pretty_print_list - s#toList - (fun i -> STR (btype_to_string (bcd#get_typ i))) - "{" "; " "}"; - STR ": compinfo: "; - STR cinfo.bcname; - STR ": first field type: "; - STR (btype_to_string ftype)]) in + log_diagnostics_result + ~tag:"first field struct check" + __FILE__ __LINE__ + [(string_of_int offset) ^ ": " + ^ (p2s (pretty_print_list + s#toList + (fun i -> STR (btype_to_string (bcd#get_typ i))) + "{" "; " "}")) + ^ ": compinfo: " ^ cinfo.bcname + ^ ": first field type: " ^ (btype_to_string ftype)] in (* TBD: restore this check in a better way if s#fold (fun acc i -> acc && (i = ixftype || i = ixctype)) true then Some tstructarray @@ -597,20 +587,18 @@ object (self) let ixftype = bcd#index_typ ftype in let ixctype = bcd#index_typ ty in let _ = - chlog#add - "first field struct check (TComp case)" - (LBLOCK [ - INT offset; - STR ": "; - pretty_print_list - s#toList - (fun i -> STR (btype_to_string (bcd#get_typ i))) - "{" "; " "}"; - STR ": compinfo: "; - STR cinfo.bcname; - STR ": first field type: "; - STR (btype_to_string ftype)]) in - if s#fold (fun acc i -> acc && (i = ixftype || i = ixctype)) true then + log_diagnostics_result + ~tag:"first field struct check (TComp case)" + __FILE__ __LINE__ + [(string_of_int offset) ^ ": " + ^ (p2s (pretty_print_list + s#toList + (fun i -> STR (btype_to_string (bcd#get_typ i))) + "{" "; " "}")) + ^ ": compinfo: " ^ cinfo.bcname + ^ ": first field type: " ^ (btype_to_string ftype)] in + if s#fold + (fun acc i -> acc && (i = ixftype || i = ixctype)) true then Some ftype else None)) @@ -644,14 +632,13 @@ object (self) | _ -> begin log_evaluation (); - chlog#add - "multiple distinct types" - (LBLOCK [ - INT offset; - STR "; "; - pretty_print_list - (List.map bcd#get_typ result#toList) - (fun ty -> STR (btype_to_string ty)) "[" "; " "]"]); + log_diagnostics_result + ~tag:("multiple distinct types for " ^ faddr) + __FILE__ __LINE__ + [(string_of_int offset) ^ ": " + ^ (p2s (pretty_print_list + (List.map bcd#get_typ result#toList) + (fun ty -> STR (btype_to_string ty)) "[" "; " "]"))]; None end end diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml index 29bedea6..189486fd 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml @@ -227,6 +227,10 @@ let join_tc_integer Some (Unsigned, size1) | (SignedNeutral, size1), (Unsigned, size2) when size1 <= size2 -> Some (Unsigned, size2) + | (Signed, size1), (Unsigned, size2) when size1 > size2 -> + Some (Signed, size1) + | (Unsigned, size1), (Signed, size2) when size1 < size2 -> + Some (Signed, size2) | _ -> None diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index bd5ae83e..97c8e8e5 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -25,9 +25,6 @@ SOFTWARE. ============================================================================= *) -(* chlib *) -open CHPretty - (* chutil *) open CHLogger open CHXmlDocument @@ -138,13 +135,11 @@ object (self) (fun baddr block -> let bNode = xmlElement "bl" in begin - chlog#add - "cfg assembly block" - (LBLOCK [ - STR baddr; - STR ": successors: "; - pretty_print_list block#get_successors - (fun s -> STR s) "[" ", " "]"]); + log_diagnostics_result + ~tag:"cfg assembly block successors" + __FILE__ __LINE__ + [baddr ^ ": [" + ^ (String.concat ", " block#get_successors) ^ "]"]; self#write_xml_cfg_block bNode block; List.iter (fun succ -> let eNode = xmlElement "e" in diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunctions.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunctions.ml index 9250811d..14d4d584 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunctions.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunctions.ml @@ -703,14 +703,12 @@ object (self) end in let _ = db#set_data_string datastring in begin - chlog#add - "add data block" - (LBLOCK [ - db#get_start_address#toPretty; - STR " - "; - db#get_end_address#toPretty; - STR ": "; - STR db#get_name]); + (log_diagnostics_result + ~tag:"add data block" + __FILE__ __LINE__ + [db#get_start_address#to_hex_string ^ " - " + ^ db#get_end_address#to_hex_string ^ ": " + ^ db#get_name]); system_info#add_data_block db; inBlock := false; count := !count + 1; diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 8142dcce..a4dde9b9 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -1602,13 +1602,28 @@ object (self) let xaddr_r = mem#to_address floc in let vmem_r = mem#to_variable floc in let xmem_r = mem#to_expr floc in - let xrmem_r = TR.tmap rewrite_expr xmem_r in - let xxaddr_r = TR.tmap rewrite_expr xaddr_r in let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r; get_rdef_memvar_r vmem_r] @ (get_all_rdefs_r xmem_r) in let uses = [get_def_use_r vrt_r] in let useshigh = [get_def_use_high_r vrt_r] in + let xxaddr_r = TR.tmap rewrite_expr xaddr_r in + let cxaddr_r = TR.tbind floc#convert_xpr_to_c_expr xxaddr_r in + let xrmem_r = TR.tmap rewrite_expr xmem_r in + let cxrmem_r = + TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 1)) xrmem_r in + let cxrmem_r = + if Result.is_ok cxrmem_r then + cxrmem_r + else + let _ = + log_diagnostics_result + ~msg:(p2s floc#l#toPretty) + ~tag:"LDRB:fall-back address conversion" + __FILE__ __LINE__ + ["xxaddr: " ^ (x_r2s xxaddr_r)] in + TR.tbind + (floc#convert_addr_to_c_pointed_to_expr ~size:(Some 1)) xxaddr_r in let _ = floc#memrecorder#record_load_r ~signed:false @@ -1618,8 +1633,9 @@ object (self) ~vtype:t_unknown in let (tagstring, args) = mk_instrx_data_r - ~vars_r:[vrt_r; vmem_r] - ~xprs_r:[xrn_r; xrm_r; xmem_r; xrmem_r; xaddr_r] + ~vars_r:[vrt_r] + ~xprs_r:[xrn_r; xrm_r; xmem_r; xrmem_r; xaddr_r; xxaddr_r] + ~cxprs_r: [cxrmem_r; cxaddr_r] ~rdefs ~uses ~useshigh diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index fd484f65..b02977d5 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -62,6 +62,8 @@ open BCHARMTypes module TR = CHTraceResult +let p2s = CHPrettyUtil.pretty_to_string + let log_error (tag: string) (msg: string): tracelogspec_t = mk_tracelog_spec ~tag:("FnARMTypeConstraints:" ^ tag) msg @@ -224,31 +226,34 @@ object (self) TR.tfold_default getopt_global_address None x_r in let log_subtype_constraint - (kind: string) (ty1: type_term_t) (ty2: type_term_t) = - let tag = "add " ^ kind ^ " subtype constraint" in - chlog#add - tag - (LBLOCK [ - floc#l#toPretty; - STR ": "; - STR (type_term_to_string ty1); - STR " <: "; - STR (type_term_to_string ty2) - ]) in - - let log_type_constraint (kind: string) (tc: type_constraint_t) = - let tag = "add " ^ kind ^ " type constraint" in - chlog#add - tag - (LBLOCK [ - floc#l#toPretty; STR ": "; STR (type_constraint_to_string tc) - ]) in - - let log_no_type_constraint (kind: string) (ty: btype_t) = - let tag = "type resolution unsuccessful for " ^ kind in - chlog#add - tag - (LBLOCK [floc#l#toPretty; STR ": "; STR (btype_to_string ty)]) in + (linenumber: int) + (kind: string) + (ty1: type_term_t) + (ty2: type_term_t) = + log_diagnostics_result + ~tag:(kind ^ " subtype constraint") + __FILE__ + linenumber + [(p2s floc#l#toPretty) ^ ": " + ^ (type_term_to_string ty1) + ^ " <: " + ^ (type_term_to_string ty2)] in + + let log_type_constraint + (linenumber: int) (kind: string) (tc: type_constraint_t) = + log_diagnostics_result + ~tag:(kind ^ " type constraint") + __FILE__ + linenumber + [(p2s floc#l#toPretty) ^ ": " ^ (type_constraint_to_string tc)] in + + let log_no_type_constraint + (linenumber: int) (kind: string) (ty: btype_t) = + log_diagnostics_result + ~tag:("type resolution unsuccessful for " ^ kind) + __FILE__ + linenumber + [(p2s floc#l#toPretty) ^ ": " ^ (btype_to_string ty)] in match instr#get_opcode with @@ -264,7 +269,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "ADD-rvintro" tc; + log_type_constraint __LINE__ "ADD-rvintro" tc; store#add_constraint tc end | _ -> ()) @@ -281,7 +286,7 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "ADD-imm" rntypeterm lhstypeterm; + log_subtype_constraint __LINE__ "ADD-imm" rntypeterm lhstypeterm; store#add_subtype_constraint rntypeterm lhstypeterm end) rndefs); @@ -299,7 +304,8 @@ object (self) let rmtypeterm = mk_vty_term rmtypevar in let ctypeterm = mk_cty_term tyc in begin - log_subtype_constraint "ADD-global" rmtypeterm ctypeterm; + log_subtype_constraint + __LINE__ "ADD-global" rmtypeterm ctypeterm; store#add_subtype_constraint rmtypeterm ctypeterm end) rmdefs | _ -> ()) @@ -316,7 +322,8 @@ object (self) let fttypeterm = mk_vty_term ftvar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "ADD-lhs-init" fttypeterm lhstypeterm; + log_subtype_constraint + __LINE__ "ADD-lhs-init" fttypeterm lhstypeterm; store#add_subtype_constraint fttypeterm lhstypeterm end | _ -> ()) @@ -334,7 +341,7 @@ object (self) let tctypeterm = mk_cty_term tc in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "ASR-lhs" tctypeterm lhstypeterm; + log_subtype_constraint __LINE__ "ASR-lhs" tctypeterm lhstypeterm; store#add_subtype_constraint tctypeterm lhstypeterm end); @@ -346,7 +353,7 @@ object (self) let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in begin - log_subtype_constraint "ASR-rhs" tctypeterm rntypeterm; + log_subtype_constraint __LINE__ "ASR-rhs" tctypeterm rntypeterm; store#add_subtype_constraint tctypeterm rntypeterm end) rndefs) end @@ -364,7 +371,7 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "AND-rdef-1" rntypeterm lhstypeterm; + log_subtype_constraint __LINE__ "AND-rdef-1" rntypeterm lhstypeterm; store#add_subtype_constraint rntypeterm lhstypeterm end) rndefs end @@ -380,7 +387,7 @@ object (self) (let tctypeterm = mk_cty_term tyc in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "MVN" tctypeterm lhstypeterm; + log_subtype_constraint __LINE__ "MVN" tctypeterm lhstypeterm; store#add_subtype_constraint tctypeterm lhstypeterm end) @@ -399,7 +406,7 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "AND-rdef-1" rntypeterm lhstypeterm; + log_subtype_constraint __LINE__ "AND-rdef-1" rntypeterm lhstypeterm; store#add_subtype_constraint rntypeterm lhstypeterm end) rndefs end @@ -442,12 +449,12 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "BL-rv-intro" tc; + log_type_constraint __LINE__ "BL-rv-intro" tc; store#add_constraint tc end | _ -> begin - log_no_type_constraint "BL-rv-intro" t; + log_no_type_constraint __LINE__ "BL-rv-intro" t; () end) | _ -> @@ -455,12 +462,12 @@ object (self) match opttc with | Some tc -> begin - log_type_constraint "BL-rv" tc; + log_type_constraint __LINE__ "BL-rv" tc; store#add_constraint tc end | _ -> begin - log_no_type_constraint "BL-rv" rtype; + log_no_type_constraint __LINE__ "BL-rv" rtype; () end); @@ -480,12 +487,12 @@ object (self) match opttc with | Some tc -> begin - log_type_constraint "BL-reg-arg" tc; + log_type_constraint __LINE__ "BL-reg-arg" tc; store#add_constraint tc end | _ -> begin - log_no_type_constraint "BL-reg-arg" ptype; + log_no_type_constraint __LINE__ "BL-reg-arg" ptype; () end) rdefs else @@ -509,7 +516,7 @@ object (self) match opttc with | Some tc -> begin - log_type_constraint "BL-stack-arg" tc; + log_type_constraint __LINE__ "BL-stack-arg" tc; store#add_constraint tc end | _ -> ()) @@ -532,7 +539,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "BL-stack-vintro" tc; + log_type_constraint __LINE__ "BL-stack-vintro" tc; store#add_constraint tc end | _ -> ()) @@ -544,7 +551,7 @@ object (self) match opttc with | Some tc -> begin - log_type_constraint "BL-reg-arg" tc; + log_type_constraint __LINE__ "BL-reg-arg" tc; store#add_constraint tc end | _ -> ()) @@ -567,7 +574,7 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let immtypeterm = mk_cty_term immtypeconst in begin - log_subtype_constraint "CMP-imm" rntypeterm immtypeterm; + log_subtype_constraint __LINE__ "CMP-imm" rntypeterm immtypeterm; store#add_subtype_constraint rntypeterm immtypeterm end) rndefs @@ -590,7 +597,7 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let rmtypeterm = mk_vty_term rmtypevar in begin - log_subtype_constraint "CMP-reg" rntypeterm rmtypeterm; + log_subtype_constraint __LINE__ "CMP-reg" rntypeterm rmtypeterm; store#add_subtype_constraint rntypeterm rmtypeterm end) pairs); @@ -605,7 +612,7 @@ object (self) let ftterm = mk_vty_term ftvar in let rmtypeterm = mk_vty_term rmtypevar in begin - log_subtype_constraint "CMP-reg-init" ftterm rmtypeterm; + log_subtype_constraint __LINE__ "CMP-reg-init" ftterm rmtypeterm; store#add_subtype_constraint ftterm rmtypeterm end) rmdefs | _ -> ()); @@ -621,7 +628,7 @@ object (self) let ftterm = mk_vty_term ftvar in let rntypeterm = mk_vty_term rntypevar in begin - log_subtype_constraint "CMP-reg-init" ftterm rntypeterm; + log_subtype_constraint __LINE__ "CMP-reg-init" ftterm rntypeterm; store#add_subtype_constraint ftterm rntypeterm end) rndefs | _ -> ()) @@ -639,7 +646,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "LDR-rvintro" tc; + log_type_constraint __LINE__ "LDR-rvintro" tc; store#add_constraint tc end | _ -> ()) @@ -656,7 +663,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "LDR-var" tc; + log_type_constraint __LINE__ "LDR-var" tc; store#add_constraint tc end | _ -> ())) @@ -674,7 +681,7 @@ object (self) let rdtypeterm = mk_vty_term rdtypevar in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "LDR-imm-off" rdtypeterm rttypeterm; + log_subtype_constraint __LINE__ "LDR-imm-off" rdtypeterm rttypeterm; store#add_subtype_constraint rdtypeterm rttypeterm end) xrdef); @@ -687,7 +694,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "LDR-memop" tc; + log_type_constraint __LINE__ "LDR-memop" tc; store#add_constraint tc end | _ -> ()) @@ -720,7 +727,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "LDR-struct-field" tc; + log_type_constraint __LINE__ "LDR-struct-field" tc; store#add_constraint tc end | _ -> ()) @@ -763,7 +770,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "LDR-array" tc; + log_type_constraint __LINE__ "LDR-array" tc; store#add_constraint tc end | _ -> ()) @@ -789,7 +796,8 @@ object (self) let rhstypeterm = mk_vty_term rhstypevar in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "LDR-stack-addr" rhstypeterm rttypeterm; + log_subtype_constraint + __LINE__ "LDR-stack-addr" rhstypeterm rttypeterm; store#add_subtype_constraint rhstypeterm rttypeterm end) end @@ -799,6 +807,20 @@ object (self) let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in begin + (match get_regvar_type_annotation () with + | Some t -> + let rtreg = rt#to_register in + let lhstypevar = mk_reglhs_typevar rtreg faddr iaddr in + let opttc = mk_btype_constraint lhstypevar t in + (match opttc with + | Some tc -> + begin + log_type_constraint __LINE__ "LDRB-rvintro" tc; + store#add_constraint tc + end + | _ -> ()) + | _ -> ()); + (* LDRB rt, [rn, rm] : X_rndef.load <: X_rt *) (let xrdefs = get_variable_rdefs_r (rn#to_variable floc) in let rnreg = rn#to_register in @@ -810,7 +832,7 @@ object (self) let rdtypeterm = mk_vty_term rdtypevar in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "LDRB-imm-off" rdtypeterm rttypeterm; + log_subtype_constraint __LINE__ "LDRB-imm-off" rdtypeterm rttypeterm; store#add_subtype_constraint rdtypeterm rttypeterm end) xrdefs); @@ -819,7 +841,7 @@ object (self) let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "LDRB-lhs-byte" tctypeterm rttypeterm; + log_subtype_constraint __LINE__ "LDRB-lhs-byte" tctypeterm rttypeterm; store#add_subtype_constraint tctypeterm rttypeterm end) @@ -835,7 +857,7 @@ object (self) let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "LDRB-lhs-byte" tctypeterm rttypeterm; + log_subtype_constraint __LINE__ "LDRB-lhs-byte" tctypeterm rttypeterm; store#add_subtype_constraint tctypeterm rttypeterm end) @@ -857,7 +879,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "LDRH-var" tc; + log_type_constraint __LINE__ "LDRH-var" tc; store#add_constraint tc end | _ -> ())) @@ -875,7 +897,7 @@ object (self) let rdtypeterm = mk_vty_term rdtypevar in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "LDRH-imm-off" rdtypeterm rttypeterm; + log_subtype_constraint __LINE__ "LDRH-imm-off" rdtypeterm rttypeterm; store#add_subtype_constraint rdtypeterm rttypeterm end) xrdef) end @@ -890,7 +912,7 @@ object (self) let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "LDRB-lhs-byte" tctypeterm rttypeterm; + log_subtype_constraint __LINE__ "LDRB-lhs-byte" tctypeterm rttypeterm; store#add_subtype_constraint tctypeterm rttypeterm end) @@ -907,7 +929,7 @@ object (self) let tcterm = mk_cty_term tc in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "LSL-lhs" tcterm lhstypeterm; + log_subtype_constraint __LINE__ "LSL-lhs" tcterm lhstypeterm; store#add_subtype_constraint tcterm lhstypeterm end); @@ -919,7 +941,7 @@ object (self) let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in begin - log_subtype_constraint "LSL-rhs" tctypeterm rntypeterm; + log_subtype_constraint __LINE__ "LSL-rhs" tctypeterm rntypeterm; store#add_subtype_constraint tctypeterm rntypeterm end) rndefs) @@ -934,7 +956,7 @@ object (self) let tcterm = mk_cty_term tc in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "LSR-lhs" tcterm lhstypeterm; + log_subtype_constraint __LINE__ "LSR-lhs" tcterm lhstypeterm; store#add_subtype_constraint tcterm lhstypeterm end); @@ -946,7 +968,7 @@ object (self) let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in begin - log_subtype_constraint "LSR-rhs" tctypeterm rntypeterm; + log_subtype_constraint __LINE__ "LSR-rhs" tctypeterm rntypeterm; store#add_subtype_constraint tctypeterm rntypeterm end) rndefs) @@ -962,7 +984,7 @@ object (self) let lhstypeterm = mk_vty_term lhstypevar in let tctypeterm = mk_cty_term tyc in begin - log_subtype_constraint "MOV-imm" tctypeterm lhstypeterm; + log_subtype_constraint __LINE__ "MOV-imm" tctypeterm lhstypeterm; store#add_subtype_constraint tctypeterm lhstypeterm end @@ -984,7 +1006,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "MOV-rvintro" tc; + log_type_constraint __LINE__ "MOV-rvintro" tc; store#add_constraint tc end | _ -> ()) @@ -999,7 +1021,8 @@ object (self) let rhstypeterm = mk_vty_term rhstypevar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "MOV-reg-init" rhstypeterm lhstypeterm; + log_subtype_constraint + __LINE__ "MOV-reg-init" rhstypeterm lhstypeterm; store#add_subtype_constraint rhstypeterm lhstypeterm end | _ -> ()); @@ -1012,7 +1035,7 @@ object (self) let regterm = mk_vty_term regvar in let fterm = mk_vty_term fvar in begin - log_subtype_constraint "MOV-freturn" regterm fterm; + log_subtype_constraint __LINE__ "MOV-freturn" regterm fterm; store#add_subtype_constraint regterm fterm end); @@ -1028,7 +1051,7 @@ object (self) let rmtypeterm = mk_vty_term rmtypevar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "MOV-reg" rmtypeterm lhstypeterm; + log_subtype_constraint __LINE__ "MOV-reg" rmtypeterm lhstypeterm; store#add_subtype_constraint rmtypeterm lhstypeterm end) rmrdefs) end @@ -1052,12 +1075,12 @@ object (self) match opttc with | Some tc -> begin - log_type_constraint "POP-rv" tc; + log_type_constraint __LINE__ "POP-rv" tc; store#add_constraint tc end | _ -> begin - log_no_type_constraint "POP-rv" rtype; + log_no_type_constraint __LINE__ "POP-rv" rtype; () end); @@ -1071,7 +1094,8 @@ object (self) let r0typeterm = mk_vty_term r0typevar in let lhstypeterm = mk_vty_term typevar in begin - log_subtype_constraint "POP-R0-rdef" r0typeterm lhstypeterm; + log_subtype_constraint + __LINE__ "POP-R0-rdef" r0typeterm lhstypeterm; store#add_subtype_constraint r0typeterm lhstypeterm end) r0defs) end) @@ -1136,7 +1160,8 @@ object (self) let rhstypeterm = mk_vty_term rhstypevar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "STR-funarg" rhstypeterm lhstypeterm; + log_subtype_constraint + __LINE__ "STR-funarg" rhstypeterm lhstypeterm; store#add_subtype_constraint rhstypeterm lhstypeterm end | _ -> ()); @@ -1152,7 +1177,8 @@ object (self) let rttypeterm = mk_vty_term rttypevar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "STR-imm-off" rttypeterm lhstypeterm; + log_subtype_constraint + __LINE__ "STR-imm-off" rttypeterm lhstypeterm; store#add_subtype_constraint rttypeterm lhstypeterm end) rtrdefs); @@ -1166,7 +1192,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "STR-stack-vintro" tc; + log_type_constraint __LINE__ "STR-stack-vintro" tc; store#add_constraint tc end | _ -> ())) @@ -1182,7 +1208,8 @@ object (self) let rttypeterm = mk_vty_term rttypevar in let rntypeterm = mk_vty_term rntypevar in begin - log_subtype_constraint "STR-imm-off" rttypeterm rntypeterm; + log_subtype_constraint + __LINE__ "STR-imm-off" rttypeterm rntypeterm; store#add_subtype_constraint rttypeterm rntypeterm end) rtrdefs) rnrdefs) end @@ -1202,7 +1229,7 @@ object (self) let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "STRB-rhs-byte" tctypeterm rttypeterm; + log_subtype_constraint __LINE__ "STRB-rhs-byte" tctypeterm rttypeterm; store#add_subtype_constraint tctypeterm rttypeterm end); @@ -1216,7 +1243,8 @@ object (self) let rttypeterm = mk_vty_term rttypevar in let rntypeterm = mk_vty_term rntypevar in begin - log_subtype_constraint "STRB-imm-off" rttypeterm rntypeterm; + log_subtype_constraint + __LINE__"STRB-imm-off" rttypeterm rntypeterm; store#add_subtype_constraint rttypeterm rntypeterm end) rtrdefs) rnrdefs) @@ -1232,7 +1260,7 @@ object (self) let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in begin - log_subtype_constraint "STRB-rhs-byte" tctypeterm rttypeterm; + log_subtype_constraint __LINE__ "STRB-rhs-byte" tctypeterm rttypeterm; store#add_subtype_constraint tctypeterm rttypeterm end) @@ -1253,7 +1281,7 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let lhstypeterm = mk_vty_term lhstypevar in begin - log_subtype_constraint "SUB-rdef-1" rntypeterm lhstypeterm; + log_subtype_constraint __LINE__ "SUB-rdef-1" rntypeterm lhstypeterm; store#add_subtype_constraint rntypeterm lhstypeterm end) rndefs end @@ -1271,7 +1299,7 @@ object (self) let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in begin - log_subtype_constraint "UBFX-rhs" tctypeterm rntypeterm; + log_subtype_constraint __LINE__ "UBFX-rhs" tctypeterm rntypeterm; store#add_subtype_constraint tctypeterm rntypeterm end) rndefs) end @@ -1287,7 +1315,7 @@ object (self) (match opttc with | Some tc -> begin - log_type_constraint "UXTH-rvintro" tc; + log_type_constraint __LINE__ "UXTH-rvintro" tc; store#add_constraint tc end | _ -> @@ -1304,10 +1332,10 @@ object (self) end | opc -> - chlog#add - "type constraints not yet implemented" - (LBLOCK [floc#l#toPretty; STR ": "; STR (arm_opcode_to_string opc)]) - + log_diagnostics_result + ~tag:"type constraints not yet implemented" + __FILE__ __LINE__ + [(p2s floc#l#toPretty) ^ ": " ^ (arm_opcode_to_string opc)] end diff --git a/CodeHawk/CHB/bchlibelf/bCHELFSymbolTable.ml b/CodeHawk/CHB/bchlibelf/bCHELFSymbolTable.ml index 49ea46e2..fa56eb6a 100644 --- a/CodeHawk/CHB/bchlibelf/bCHELFSymbolTable.ml +++ b/CodeHawk/CHB/bchlibelf/bCHELFSymbolTable.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -285,11 +285,18 @@ object ~tag:"disassembly" "elf_symbol_table#set_mapping_symbols make_db") (fun db -> + let p_dbsize = + TR.tfold + ~ok:string_of_int + ~error:(fun e -> "[Error: " ^ (String.concat "; " e) ^ "]") + (addr#subtract_to_int addr_d) in begin - (if collect_diagnostics () then - ch_diagnostics_log#add - "data block from symbol table" - (LBLOCK [addr_d#toPretty; STR " - "; addr#toPretty])); + (log_diagnostics_result + ~tag:"set mapping symbols:data block from symbol table" + __FILE__ __LINE__ + ["start: " ^ addr_d#to_hex_string + ^ "; end: " ^ addr#to_hex_string + ^ "; size: " ^ p_dbsize]); system_info#add_data_block db; indata := None end) @@ -324,7 +331,9 @@ object end); make_db addr end - | _ -> ()) symbols + | _ -> + let addr = TR.tget_ok (index_to_doubleword addrix) in + make_db addr) symbols method get_symbol (index:int) = if H.mem entries index then