Skip to content

Liftingsupport #187

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 3 commits into from
Apr 15, 2025
Merged

Liftingsupport #187

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
a8c959b
CHB:ARM: convert LDRB to transmit C expressions
sipma Apr 5, 2025
5b79f2b
CHB:ELF:always create data blocks for symbols
sipma Apr 15, 2025
1b1230a
add more diagnostic logging
sipma Apr 15, 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
10 changes: 5 additions & 5 deletions CodeHawk/CHB/bchcil/bCHParseCilFile.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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


Expand Down
17 changes: 15 additions & 2 deletions CodeHawk/CHB/bchlib/bCHFunctionInterface.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
18 changes: 15 additions & 3 deletions CodeHawk/CHB/bchlib/bCHMemoryReference.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 "
Expand Down
15 changes: 6 additions & 9 deletions CodeHawk/CHB/bchlib/bCHSystemInfo.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
179 changes: 83 additions & 96 deletions CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
[]
Expand Down Expand Up @@ -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) ->
Expand Down Expand Up @@ -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
Expand All @@ -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.
Expand Down Expand Up @@ -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
Expand All @@ -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))
Expand Down Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down
17 changes: 6 additions & 11 deletions CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -25,9 +25,6 @@
SOFTWARE.
============================================================================= *)

(* chlib *)
open CHPretty

(* chutil *)
open CHLogger
open CHXmlDocument
Expand Down Expand Up @@ -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
Expand Down
Loading