Skip to content

Liftingsupport #189

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
sipma merged 2 commits into from
Apr 21, 2025
Merged

Liftingsupport #189

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4c1d73e
CHB:ARM: add global variable addresses to assembly listing
sipma Apr 21, 2025
29eaa5b
CHB:TI: allow join of struct type and type of first field
sipma Apr 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions CodeHawk/CHB/bchlib/bCHFloc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1389,6 +1389,14 @@ object (self)
(self#f#is_base_pointer v)
|| (TR.tfold_default is_pointer false (self#get_variable_type v))
) vars in
let _ =
log_diagnostics_result
~tag:"convert_addr_to_c_pointed_to_expr"
__FILE__ __LINE__
[(p2s self#l#toPretty);
"known pointers: ";
(p2s (pretty_print_list knownpointers
(fun v -> v#toPretty) "[" ", " "]"))] in
match knownpointers with
(* one known pointer, must be the base *)
| [base] when self#f#env#is_initial_stackpointer_value base ->
Expand Down
47 changes: 36 additions & 11 deletions CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -494,17 +494,42 @@ object (self)
match result#singleton with
| Some ixty -> Some (bcd#get_typ ixty)
| _ ->
begin
log_evaluation ();
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
match result#toList with
| [ixty1; ixty2] ->
(match (bcd#get_typ ixty1), (bcd#get_typ ixty2) with
| TPtr (tty1, _), TPtr (tty2, _)
when is_struct_type tty1 && is_scalar tty2 ->
Some (bcd#get_typ ixty1)
| TPtr (tty1, _), TPtr (tty2, _)
when is_struct_type tty2 && is_scalar tty1 ->
Some (bcd#get_typ ixty2)
| _ ->
begin
log_evaluation ();
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)
| _ ->
begin
log_evaluation ();
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

method resolve_stack_lhs_type
Expand Down
4 changes: 2 additions & 2 deletions CodeHawk/CHB/bchlib/bCHVersion.ml
View file
Open in desktop
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_20250417"
~date:"2025-04-17"
~version:"0.6.0_20250420"
~date:"2025-04-20"
~licensee: None
~maxfilesize: None
()
222 changes: 131 additions & 91 deletions CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,10 +67,11 @@ open BCHDisassembleThumbInstruction
module H = Hashtbl
module TR = CHTraceResult

(*
let x2p = XprToPretty.xpr_formatter#pr_expr
let p2s = CHPrettyUtil.pretty_to_string
let x2s x = p2s (x2p x)

*)
let numArrays = 1000
let arrayLength = 100000

Expand Down Expand Up @@ -594,7 +595,102 @@ object (self)
let firstNew = ref true in
let datareftable = H.create (List.length datarefs) in
let _ = List.iter (fun (a, refs) -> H.add datareftable a refs) datarefs in
let datarefstr (a: doubleword_int): string =
if H.mem datareftable a#to_hex_string then
let datarefs = H.find datareftable a#to_hex_string in
" (refs: "
^ (String.concat
", " (List.map (fun instr -> instr#get_address#to_hex_string) datarefs))
^ ")"
else
"" in
let memorymap = BCHGlobalMemoryMap.global_memory_map in
let get_memory_offset (gloc: global_location_int) (offset: xpr_t) =
TR.tfold
~ok:(fun memoffset ->
" (" ^ (BCHMemoryReference.memory_offset_to_string memoffset) ^ ")"
^ "")
~error:(fun e ->
begin
log_diagnostics_result __FILE__ __LINE__ e;
""
end)
(gloc#address_memory_offset ~tgtsize:(Some 4) offset) in
let render_gloc (a: doubleword_int) (v: doubleword_int): string =
let addrprefix = " " ^ (fixed_length_string a#to_hex_string 10) in
let p_value =
if v#equal wordzero then
"<0x0>"
else if v#equal wordmax then
"<0xffffffff>"
else if functions_data#is_function_entry_point v then
let name =
if functions_data#has_function_name v then
let fndata = functions_data#get_function v in
":" ^ fndata#get_function_name
else
"" in
"FAddr:<"
^ v#to_hex_string
^ name
^ ">"
else if elf_header#is_code_address v then
"Code:<"
^ v#to_hex_string
^ ">"
else if elf_header#is_data_address v then
let s =
match elf_header#get_string_at_address v with
| Some s ->
let len = String.length s in
if len < 50 then
":\"" ^ s ^ "\""
else
":\"" ^ (String.sub s 0 50) ^ "...\""
| _ -> "" in
" Data:<"
^ v#to_hex_string
^ s
^ ">"
else
v#to_hex_string in
match memorymap#containing_location a with
| None -> "" (* should not be reachable *)
| Some gloc ->
let xprv = num_constant_expr a#to_numerical in
TR.tfold_default
(fun offset ->
let p_memoff = get_memory_offset gloc xprv in
match offset with
| XConst (IntConst n) when n#equal numerical_zero ->
addrprefix
^ "\n Global variable:<"
^ gloc#name
^ ": "
^ (btype_to_string gloc#btype)
^ ">\n"
^ addrprefix
^ " GV:<"
^ gloc#name
^ ":0 >: "
^ p_value
^ p_memoff
^ (datarefstr a)
| XConst (IntConst n) ->
addrprefix
^ " GV:<"
^ gloc#name
^ ":"
^ (fixed_length_string n#toString 3)
^ ">: "
^ p_value
^ p_memoff
^ (datarefstr a)
| _ -> "" (* should not be reachable *)
)
(addrprefix ^ " GV:<" ^ gloc#name ^ ":?>:" ^ p_value)
(gloc#address_offset xprv) in

let not_code_to_string nc =
match nc with
| JumpTable jt ->
Expand Down Expand Up @@ -665,20 +761,10 @@ object (self)
"\n"
(List.map
(fun (a, v) ->
let addrprefix =
" " ^ (fixed_length_string a#to_hex_string 10) in
let addr = a#to_hex_string in
let datarefstr =
if H.mem datareftable addr then
let datarefs = H.find datareftable addr in
" "
^ "(refs: "
^ (String.concat
", "
(List.map
(fun instr ->
instr#get_address#to_hex_string) datarefs))
^ ")"
else
"" in
let pdatarefstr = datarefstr a in
if a#lt !stringend then
" "
^ (fixed_length_string addr 10)
Expand All @@ -687,73 +773,22 @@ object (self)
^ "> ... (cont'd)"

else if Option.is_some (memorymap#containing_location a) then
match memorymap#containing_location a with
| None -> ""
| Some gloc ->
let xprv = num_constant_expr a#to_numerical in
let offset_r = gloc#address_offset xprv in
TR.tfold_default
(fun offset ->
match offset with
| XConst (IntConst n) when n#equal numerical_zero ->
" "
^ (fixed_length_string addr 10)
^ " Global variable:<"
^ gloc#name
^ ": "
^ (btype_to_string gloc#btype)
^ ">"
^ "\n "
^ (fixed_length_string addr 10)
^ " GV:<"
^ gloc#name
^ ":0 >: "
^ v#to_hex_string
| XConst (IntConst n) ->
" "
^ (fixed_length_string addr 10)
^ " GV:<"
^ gloc#name
^ ":"
^ (fixed_length_string n#toString 3)
^ ">: "
^ v#to_hex_string
| _ ->
" "
^ (fixed_length_string addr 10)
^ " GV:<"
^ gloc#name
^ ":"
^ (x2s offset)
^ ">: "
^ v#to_hex_string)
(" "
^ (fixed_length_string addr 10)
^ " GV:<"
^ gloc#name
^ ":?>: "
^ v#to_hex_string)
offset_r
render_gloc a v

else if memorymap#has_elf_symbol v then
let name = memorymap#get_elf_symbol v in
" "
^ (fixed_length_string addr 10)
addrprefix
^ " Sym:<"
^ v#to_hex_string
^ ":"
^ name
^ ">"
^ datarefstr
^ pdatarefstr

else if v#equal wordzero then
" "
^ (fixed_length_string addr 10)
^ " <0x0>"
addrprefix ^ " <0x0>"
else if v#equal wordmax then
" "
^ (fixed_length_string addr 10)
^ " <0xffffffff>"
addrprefix ^ " <0xffffffff>"

else if functions_data#is_function_entry_point v then
let name =
Expand All @@ -762,21 +797,30 @@ object (self)
":" ^ fndata#get_function_name
else
"" in
" "
^ (fixed_length_string addr 10)
addrprefix
^ " Faddr:<"
^ v#to_hex_string
^ name
^ ">"
^ datarefstr
^ pdatarefstr

else if memorymap#has_location v then
let gloc = memorymap#get_location v in
addrprefix
^ " GVAddr:<"
^ v#to_hex_string
^ ":"
^ gloc#name
^ ">"
^ pdatarefstr

else if elf_header#is_code_address v then
" "
^ (fixed_length_string addr 10)
addrprefix
^ " Code:<"
^ v#to_hex_string
^ ">"
^ datarefstr
^ (datarefstr a)

else if elf_header#is_data_address v then
let s =
match elf_header#get_string_at_address v with
Expand All @@ -787,44 +831,40 @@ object (self)
else
":\"" ^ (String.sub s 0 50) ^ "...\""
| _ -> "" in
" "
^ (fixed_length_string addr 10)
addrprefix
^ " Data:<"
^ v#to_hex_string
^ s
^ ">"
^ datarefstr
^ pdatarefstr

else if elf_header#is_uninitialized_data_address v then
" "
^ (fixed_length_string addr 10)
addrprefix
^ " Bss:<"
^ v#to_hex_string
^ ">"
^ datarefstr
^ (datarefstr a)
else if Option.is_some
(elf_header#get_string_at_address a) then
let s =
Option.get (elf_header#get_string_at_address a) in
begin
(" "
^ (fixed_length_string addr 10)
(addrprefix
^ " String:<"
^ (fixed_length_string v#to_hex_string 12)
^ ">: \""
^ s
^ "\"")
^ datarefstr
^ pdatarefstr
end
else if (String.length datarefstr) > 0 then
" "
^ (fixed_length_string addr 10)
else if (String.length (datarefstr a)) > 0 then
addrprefix
^ " Value<"
^ v#to_hex_string
^ ">"
^ datarefstr
^ pdatarefstr
else
" "
^ (fixed_length_string addr 10)
addrprefix
^ " "
^ (fixed_length_string v#to_hex_string 14)
^ " "
Expand Down