Skip to content

Typingrules #212

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
Aug 20, 2025
Merged

Typingrules #212

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
3112506
CHB:refine global variable field determination
sipma Aug 20, 2025
e4a6caa
CHB: handle void-typed target address
sipma Aug 20, 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
59 changes: 44 additions & 15 deletions CodeHawk/CHB/bchlib/bCHFloc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -687,7 +687,7 @@ object (self)
(fun memoff ->
TR.tbind
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
self#env#mk_global_variable
(self#env#mk_global_variable self#l)
(get_total_constant_offset memoff))
memoffset_r
else if memref#is_stack_reference then
Expand Down Expand Up @@ -736,7 +736,7 @@ object (self)
let dw = numerical_mod_to_doubleword n in
if system_info#get_image_base#le dw then
tprop
(self#env#mk_global_variable ~size n)
(self#env#mk_global_variable self#l ~size n)
(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
else
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
Expand Down Expand Up @@ -791,7 +791,7 @@ object (self)
(self#cia ^ " : constant: " ^ n#toString))
(fun v -> v)
(default ())
(self#env#mk_global_variable ~size n)
(self#env#mk_global_variable ~size self#l n)
else
default ())
(default ())
Expand All @@ -809,7 +809,7 @@ object (self)
(default ())
(TR.tbind
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
self#env#mk_global_variable
(self#env#mk_global_variable self#l)
(get_total_constant_offset memoffset))
else
(TR.tfold_default
Expand Down Expand Up @@ -845,7 +845,7 @@ object (self)
(fun memoff ->
TR.tbind
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
(self#env#mk_global_variable ~size)
(self#env#mk_global_variable ~size self#l)
(get_total_constant_offset memoff))
memoff_r
else
Expand Down Expand Up @@ -946,7 +946,7 @@ object (self)
(default ())
(TR.tbind
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
self#env#mk_global_variable
(self#env#mk_global_variable self#l)
(get_total_constant_offset memoffset))
else
TR.tfold_default
Expand Down Expand Up @@ -983,7 +983,7 @@ object (self)
(self#cia ^ "; constant: " ^ n#toString))
(fun v -> v)
(default ())
(self#env#mk_global_variable n)
(self#env#mk_global_variable self#l n)
else
default ())
(default ())
Expand All @@ -1002,7 +1002,7 @@ object (self)
(self#cia ^ ": constant: " ^ n#toString))
(fun v -> v)
(default ())
(self#env#mk_global_variable n)
(self#env#mk_global_variable self#l n)
else
default ())
(default ())
Expand Down Expand Up @@ -1266,9 +1266,32 @@ object (self)
~tag:"get_var_at_address"
__FILE__ __LINE__
["addrvalue: " ^ (x2s addrvalue);
"btype: " ^ (btype_to_string btype)] in
"btype: " ^ (btype_to_string btype);
"size: " ^ (if Option.is_some size then (string_of_int (Option.get size)) else "?")] in

match self#normalize_addrvalue addrvalue with
| XOp ((Xf "addressofvar"), [XVar v]) when self#env#is_global_variable v ->
let gvaddr_r = self#f#env#get_global_variable_address v in
TR.tbind
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
(fun gvaddr ->
if memmap#has_location gvaddr then
let gloc = memmap#get_location gvaddr in
let varresult =
TR.tmap
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
(fun offset -> self#f#env#mk_gloc_variable gloc offset)
(gloc#address_offset_memory_offset
~tgtsize:size ~tgtbtype:btype self#l zero_constant_expr) in
varresult
else
Error[__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
^ (p2s self#l#toPretty)
^ ": "
^ "Global location at address "
^ gvaddr#to_hex_string
^ " not found"])
gvaddr_r
| XOp ((Xf "addressofvar"), [XVar v]) -> Ok v
| XOp (XPlus, [XOp ((Xf "addressofvar"), [XVar v]); xoff])
when self#f#env#is_global_variable v ->
Expand All @@ -1286,7 +1309,7 @@ object (self)
(TR.tbind
(fun xoff ->
gloc#address_offset_memory_offset
~tgtsize:size ~tgtbtype:btype xoff)
~tgtsize:size ~tgtbtype:btype self#l xoff)
cxoff_r) in
let _ =
log_diagnostics_result
Expand All @@ -1312,7 +1335,7 @@ object (self)
(TR.tmap
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
(fun offset -> self#f#env#mk_gloc_variable gloc offset)
(gloc#address_memory_offset ~tgtsize:size ~tgtbtype:btype addrvalue))
(gloc#address_memory_offset ~tgtsize:size ~tgtbtype:btype self#l addrvalue))
| _ ->
let (memref_r, memoff_r) = self#decompose_memaddr addrvalue in
TR.tmap2
Expand Down Expand Up @@ -2024,6 +2047,12 @@ object (self)
* if not, identify the variable most likely to be the base pointer.
*)
method decompose_address (x:xpr_t):(memory_reference_int * memory_offset_t) =
let _ =
log_diagnostics_result
~msg:(p2s self#l#toPretty)
~tag:"decompose-address"
__FILE__ __LINE__
["x: " ^ (x2s x)] in
let default () =
(self#env#mk_unknown_memory_reference (x2s x), UnknownOffset) in
let is_external_constant v = self#env#is_function_initial_value v in
Expand Down Expand Up @@ -2184,7 +2213,7 @@ object (self)
(self#cia ^ ": constant: " ^ n#toString))
(fun v -> v)
(default ())
(self#env#mk_global_variable n)
(self#env#mk_global_variable self#l n)
else
default ())
(default ())
Expand Down Expand Up @@ -2315,7 +2344,7 @@ object (self)
~tag:"assign global variable address" __FILE__ __LINE__ e;
rhs
end)
(self#f#env#mk_global_variable n)
(self#f#env#mk_global_variable self#l n)
else
rhs
| _ -> rhs in
Expand Down Expand Up @@ -2492,7 +2521,7 @@ object (self)
let argvar = self#env#mk_register_variable r in
self#rewrite_variable_to_external argvar
| [GlobalParameter (a, _)] when not (a#equal wordzero) ->
let argvar = self#env#mk_global_variable a#to_numerical in
let argvar = self#env#mk_global_variable self#l a#to_numerical in
(match argvar with
| Error e ->
raise
Expand Down Expand Up @@ -2577,7 +2606,7 @@ object (self)
(self#cia ^ ": constant: " ^ num#toString))
(fun v -> Some v)
None
(self#env#mk_global_variable num)
(self#env#mk_global_variable self#l num)
else
None)
None
Expand Down
3 changes: 2 additions & 1 deletion CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -843,6 +843,7 @@ object (self)
method mk_global_variable
?(size=4)
?(btype=t_unknown)
(loc: location_int)
(base: numerical_t): variable_t traceresult =
let dw = numerical_mod_to_doubleword base in
match memmap#containing_location dw with
Expand Down Expand Up @@ -872,7 +873,7 @@ object (self)
self#set_variable_name ivar (name ^ "_in");
gvar
end)
(gloc#address_memory_offset ~tgtbtype:btype (num_constant_expr base))
(gloc#address_memory_offset ~tgtbtype:btype loc (num_constant_expr base))
| _ ->
let _ = memmap#add_location ~size:(Some size) ~btype dw in
Ok (self#mk_variable (self#varmgr#make_global_variable dw#to_numerical))
Expand Down
Loading