Skip to content

Commit 9e45c19

Browse files
sipmasipma
committed
CHB: more support for function annotations
1 parent 046d5f6 commit 9e45c19

13 files changed

+99
-74
lines changed

‎CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -861,14 +861,21 @@ let main () =
861861
STR ")"] in
862862
let _ = load_elf_files () in
863863
let _ = pr_timing [STR "elf files loaded"] in
864+
865+
(* symbolic addresses in userdata should be loaded before the header
866+
files are parsed. *)
867+
let _ = system_info#initialize in
868+
let _ = pr_timing [STR "system info initialized"] in
864869
let _ =
865870
List.iter
866871
(fun f -> parse_cil_file ~removeUnused:false f) system_info#ifiles in
867872
let _ =
868873
if (List.length system_info#ifiles > 0) then
869874
pr_timing [STR "c header files parsed"] in
870-
let _ = system_info#initialize in
871-
let _ = pr_timing [STR "system info initialized"] in
875+
(* function annotations in userdata should be loaded after the header
876+
files are parsed, so types in the function annotations can be resolved.*)
877+
let _ = system_info#initialize_function_annotations in
878+
872879
let index = file_metrics#get_index in
873880
let logcmd = "analyze_" ^ (string_of_int index) in
874881
let analysisstart = Unix.gettimeofday () in

‎CodeHawk/CHB/bchlib/bCHFloc.ml‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -859,14 +859,16 @@ object (self)
859859
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
860860
(fun memref ->
861861
if memref#is_global_reference then
862+
self#get_var_at_address ~size:(Some size) address
863+
(*
862864
TR.tbind
863865
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
864866
(fun memoff ->
865867
TR.tbind
866868
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
867869
(self#env#mk_global_variable ~size)
868870
(get_total_constant_offset memoff))
869-
memoff_r
871+
memoff_r *)
870872
else
871873
TR.tbind
872874
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))

‎CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml‎

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -351,9 +351,14 @@ object (self)
351351
(fun suboff -> Ok (ArrayIndexOffset (indexxpr, suboff)))
352352
(self#arrayvar_memory_offset ~tgtsize ~tgtbtype eltty rem)
353353
else if is_scalar eltty then
354-
let x2index = XOp (XDiv, [rem; int_constant_expr elsize]) in
355-
let x2index = Xsimplify.simplify_xpr x2index in
356-
Ok (ArrayIndexOffset (x2index, NoOffset))
354+
if iszero rem then
355+
Ok (ArrayIndexOffset (indexxpr, NoOffset))
356+
else
357+
let suboff =
358+
let x2index = XOp (XDiv, [rem; int_constant_expr elsize]) in
359+
let x2index = Xsimplify.simplify_xpr x2index in
360+
ArrayIndexOffset (x2index, NoOffset) in
361+
Ok (ArrayIndexOffset (indexxpr, suboff))
357362
else
358363
Error[__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":"
359364
^ "xoffset: " ^ (x2s xoffset)

‎CodeHawk/CHB/bchlib/bCHLibTypes.mli‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6217,6 +6217,7 @@ object
62176217

62186218
(* initialization *)
62196219
method initialize: unit
6220+
method initialize_function_annotations: unit
62206221
method initialize_jumptables:
62216222
(doubleword_int -> bool) -> (doubleword_int * string) list -> unit
62226223
method initialize_datablocks: (doubleword_int * string) list -> unit
@@ -6347,7 +6348,6 @@ object
63476348
method get_user_struct_count: int
63486349
method get_user_nonreturning_count: int
63496350
method get_user_class_count: int
6350-
method get_variable_intro_name: doubleword_int -> string
63516351

63526352
(* predicates *)
63536353
method is_little_endian: bool
@@ -6378,8 +6378,6 @@ object
63786378
method is_trampoline_payload: doubleword_int -> bool
63796379
method is_trampoline_wrapper: doubleword_int -> bool
63806380
method is_trampoline_fallthroughaddr: doubleword_int -> bool
6381-
method has_variable_intro: doubleword_int -> bool
6382-
method has_variable_intros: bool
63836381

63846382
(** [is_thumb addr] returns true if the architecture includes (arm) thumb
63856383
instructions and the virtual address [addr] is in a code section that

‎CodeHawk/CHB/bchlib/bCHMemoryReference.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -481,6 +481,7 @@ let stack_offset_to_name offset =
481481
"var_" ^ (constant_offset_to_neg_suffix_string n)
482482
| ConstantOffset (n,NoOffset) when n#equal numerical_zero ->
483483
"var_0000"
484+
| NoOffset -> "var_0000"
484485
| _ -> "var.[" ^ (memory_offset_to_string offset) ^ "]"
485486

486487

‎CodeHawk/CHB/bchlib/bCHSystemInfo.ml‎

Lines changed: 14 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
77
Copyright (c) 2005-2020 Kestrel Technology LLC
88
Copyright (c) 2020 Henny Sipma
9-
Copyright (c) 2021-2024 Aarno Labs LLC
9+
Copyright (c) 2021-2025 Aarno Labs LLC
1010
1111
Permission is hereby granted, free of charge, to any person obtaining a copy
1212
of this software and associated documentation files (the "Software"), to deal
@@ -155,7 +155,6 @@ object (self)
155155
val initialized_memory = H.create 3
156156

157157
val function_call_targets = H.create 13 (* (faddr, iaddr) -> call_target_t *)
158-
val variable_intros = H.create 13 (* iaddr#index -> name *)
159158

160159
val esp_adjustments = H.create 3 (* indexed with faddr, iaddr *)
161160
val esp_adjustments_i = H.create 3 (* indexed with iaddr *)
@@ -611,6 +610,18 @@ object (self)
611610
set_functions_file_path ()
612611
end
613612

613+
method initialize_function_annotations =
614+
match load_userdata_system_file () with
615+
| Some node ->
616+
let getc = node#getTaggedChild in
617+
let hasc = node#hasOneTaggedChild in
618+
begin
619+
(if hasc "function-annotations" then
620+
BCHFunctionData.read_xml_function_annotations
621+
(getc "function-annotations"))
622+
end
623+
| _ -> ()
624+
614625
method private initialize_system_file =
615626
try
616627
match load_system_file () with
@@ -832,13 +843,6 @@ object (self)
832843
(if hasc "symbolic-addresses" then
833844
BCHGlobalMemoryMap.read_xml_symbolic_addresses (getc "symbolic-addresses"));
834845

835-
(if hasc "function-annotations" then
836-
BCHFunctionData.read_xml_function_annotations
837-
(getc "function-annotations"));
838-
839-
(if hasc "variable-introductions" then
840-
self#read_xml_variable_introductions (getc "variable-introductions"));
841-
842846
(if hasc "userdeclared-codesections" then
843847
self#read_xml_userdeclared_codesections
844848
(getc "userdeclared-codesections"));
@@ -1413,39 +1417,6 @@ object (self)
14131417
let name = get n "n" in
14141418
(functions_data#add_function fa)#add_name name) (getcc "fn")
14151419

1416-
method private read_xml_variable_introductions (node: xml_element_int) =
1417-
let geta n =
1418-
fail_tvalue
1419-
(trerror_record
1420-
(LBLOCK [
1421-
STR "read_xml_variable_introductions";
1422-
STR (n#getAttribute "ia")]))
1423-
(string_to_doubleword (n#getAttribute "ia")) in
1424-
let getcc = node#getTaggedChildren in
1425-
begin
1426-
List.iter (fun n ->
1427-
let iaddr = geta n in
1428-
let name = n#getAttribute "name" in
1429-
H.add variable_intros iaddr#index name) (getcc "vintro");
1430-
chlog#add
1431-
"initialization"
1432-
(LBLOCK [
1433-
STR "system-info: read ";
1434-
INT (H.length variable_intros);
1435-
STR " variable introductions"])
1436-
end
1437-
1438-
method private write_xml_variable_introductions (node: xml_element_int) =
1439-
let vintros = H.fold (fun k v a -> (k, v)::a) variable_intros [] in
1440-
List.iter (fun (dwindex, name) ->
1441-
let vnode = xmlElement "vintro" in
1442-
begin
1443-
vnode#setAttribute
1444-
"ia" (TR.tget_ok (int_to_doubleword dwindex))#to_hex_string;
1445-
vnode#setAttribute "name" name;
1446-
node#appendChildren [vnode];
1447-
end) vintros
1448-
14491420
method private read_xml_user_nonreturning_functions (node:xml_element_int) =
14501421
let geta n =
14511422
fail_tvalue
@@ -1555,8 +1526,6 @@ object (self)
15551526
self#read_xml_thread_start_functions (getc "thread-start-functions")) ;
15561527
(if hasc "goto-returns" then
15571528
self#read_xml_goto_returns (getc "goto-returns"));
1558-
(if hasc "variable-introductions" then
1559-
self#read_xml_variable_introductions (getc "variable-introductions"));
15601529
(if hasc "so-imports" then
15611530
self#read_xml_so_imports (getc "so-imports"));
15621531
end
@@ -1714,19 +1683,6 @@ object (self)
17141683
dNode
17151684
end) data_blocks#toList)
17161685

1717-
method has_variable_intro (iaddr: doubleword_int) =
1718-
H.mem variable_intros iaddr#index
1719-
1720-
method has_variable_intros: bool = (H.length variable_intros) > 0
1721-
1722-
method get_variable_intro_name (iaddr: doubleword_int): string =
1723-
if self#has_variable_intro iaddr then
1724-
H.find variable_intros iaddr#index
1725-
else
1726-
raise
1727-
(BCH_failure
1728-
(LBLOCK [STR "No variable intro found for address "; iaddr#toPretty]))
1729-
17301686
(* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *
17311687
* stage 2: function entry points *
17321688
* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
@@ -2152,7 +2108,6 @@ object (self)
21522108
let gNode = xmlElement "goto-returns" in
21532109
let cbNode = xmlElement "call-back-tables" in
21542110
let stNode = xmlElement "struct-tables" in
2155-
let viNode = xmlElement "variable-introductions" in
21562111
let soNode = xmlElement "so-imports" in
21572112
begin
21582113
functions_data#write_xml fNode;
@@ -2163,11 +2118,10 @@ object (self)
21632118
self#write_xml_goto_returns gNode;
21642119
self#write_xml_call_back_tables cbNode;
21652120
self#write_xml_struct_tables stNode;
2166-
self#write_xml_variable_introductions viNode;
21672121
string_table#write_xml sNode;
21682122
self#write_xml_so_imports soNode;
21692123
append [
2170-
fNode; lNode; dNode; jNode; sNode; tNode; gNode; cbNode; stNode; viNode;
2124+
fNode; lNode; dNode; jNode; sNode; tNode; gNode; cbNode; stNode;
21712125
soNode]
21722126
end
21732127

‎CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -438,7 +438,6 @@ object (self)
438438
(reg: register_t) (faddr: string) (iaddr: string): btype_t option =
439439
let evaluation = self#evaluate_reglhs_type reg faddr iaddr in
440440
let logresults = iaddr = "0xffffffff" in
441-
let p2s = CHPrettyUtil.pretty_to_string in
442441
let log_evaluation () =
443442
chlog#add
444443
("reglhs resolution was not successfull:" ^ faddr)

‎CodeHawk/CHB/bchlib/bCHVariable.ml‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,10 @@ object (self:'a)
9494
| "var" -> stack_offset_to_name offset
9595
| "varr" -> realigned_stack_offset_to_name offset
9696
| "gv" -> global_offset_to_name size offset
97-
| _ -> basename ^ (memory_offset_to_string offset))
97+
| _ ->
98+
(match offset with
99+
| NoOffset -> "__pderef_" ^ basename ^ "_"
100+
| _ -> basename ^ (memory_offset_to_string offset)))
98101
| RegisterVariable reg -> register_to_string reg
99102
| CPUFlagVariable flag -> flag_to_string flag
100103
| AuxiliaryVariable a ->
@@ -107,7 +110,7 @@ object (self:'a)
107110
| FunctionPointer (fname,cname,address) ->
108111
"fp_" ^ fname ^ "_" ^ cname ^ "_" ^ address
109112
| FunctionReturnValue address -> "rtn_" ^ address
110-
| TypeCastValue (iaddr, name, ty, reg) ->
113+
| TypeCastValue (iaddr, name, _, reg) ->
111114
"typecast_" ^ name ^ "_" ^ iaddr ^ "_" ^ (register_to_string reg)
112115
| SyscallErrorReturnValue address -> "errval_" ^ address
113116
| CallTargetValue tgt ->
@@ -593,6 +596,10 @@ object (self)
593596
method has_variable_index_offset (v: variable_t): bool =
594597
match self#get_memvar_offset v with
595598
| Ok (IndexOffset (v, _, _)) -> self#is_register_variable v
599+
| Ok (ArrayIndexOffset (x, _)) ->
600+
(match x with
601+
| XConst (IntConst _) -> false
602+
| _ -> true)
596603
| _ -> false
597604

598605
method get_memval_offset (v: variable_t): memory_offset_t traceresult =

‎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_2024127"
99-
~date:"2024-12-27"
98+
~version:"0.6.0_20250201"
99+
~date:"2025-02-01"
100100
~licensee: None
101101
~maxfilesize: None
102102
()

‎CodeHawk/CHB/bchlib/bCHXprUtil.ml‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,9 @@ let get_array_index_offset (xpr: xpr_t) (size: int): (xpr_t * xpr_t) option =
115115
Some (num_constant_expr quo, num_constant_expr rem)
116116
| XOp (XMult, [XConst (IntConst n); XVar v]) when n#equal numsize ->
117117
Some (XVar v, xzero)
118+
| XOp (XMult, [XConst (IntConst n); XOp ((XXlsh | XXlsb), [XVar v])])
119+
when n#equal numsize ->
120+
Some (XVar v, xzero)
118121
| XOp (XPlus, [XOp (XMult, [XConst (IntConst n1); XVar v]);
119122
XConst (IntConst n2)]) when n1#equal numsize ->
120123
if n2#equal numerical_zero then

0 commit comments

Comments
 (0)