Skip to content

CHB:don't record save/restores of temporary registers #210

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 1 commit into from
Aug 13, 2025
Merged

CHB:don't record save/restores of temporary registers #210

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
55 changes: 26 additions & 29 deletions CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1825,36 +1825,33 @@ object (self)

method save_register
(vmem: variable_t) (iaddr: ctxt_iaddress_t) (reg: register_t) =
if BCHCPURegisters.is_temporary_register reg then
()
if self#env#is_stack_variable vmem then
TR.tfold
~ok:(fun offset ->
match offset with
| ConstantOffset (n, NoOffset) ->
self#stackframe#add_register_spill ~offset:n#toInt reg iaddr
| _ ->
log_error_result
~msg:"save_register:not a constant offset"
__FILE__ __LINE__
["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
(p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)
^ " and offset " ^ (memory_offset_to_string offset)])
~error:(fun e ->
log_error_result
~msg:"save_register"
__FILE__ __LINE__
(["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
(p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] @ e))
(self#env#get_memvar_offset vmem)
else
if self#env#is_stack_variable vmem then
TR.tfold
~ok:(fun offset ->
match offset with
| ConstantOffset (n, NoOffset) ->
self#stackframe#add_register_spill ~offset:n#toInt reg iaddr
| _ ->
log_error_result
~msg:"save_register:not a constant offset"
__FILE__ __LINE__
["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
(p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)
^ " and offset " ^ (memory_offset_to_string offset)])
~error:(fun e ->
log_error_result
~msg:"save_register"
__FILE__ __LINE__
(["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
(p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] @ e))
(self#env#get_memvar_offset vmem)
else
log_error_result
~msg:"save register:not a stack variable"
__FILE__ __LINE__
["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
"not a stack variable: "
^ (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)]
log_error_result
~msg:"save register:not a stack variable"
__FILE__ __LINE__
["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
"not a stack variable: "
^ (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)]

method restore_register
(memaddr: xpr_t) (iaddr:ctxt_iaddress_t) (reg:register_t) =
Expand Down
136 changes: 71 additions & 65 deletions CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -465,75 +465,81 @@ object (self)

method add_register_spill
~(offset: int) (reg: register_t) (iaddr:ctxt_iaddress_t) =
let spill = RegisterSpill (offset, reg) in
begin
(if H.mem stackslots offset then
if (H.find stackslots offset)#is_spill then
()
else
let sslot = H.find stackslots offset in
raise
(BCH_failure
(LBLOCK [
STR "Add register spill at address ";
STR iaddr;
STR " for register ";
STR (register_to_string reg);
STR " at offset ";
INT offset;
STR " cannot be completed, because another stackslot ";
STR "at this offset, with name: ";
STR sslot#name;
STR " already exists"]))
else
let ssrec = {
sslot_name = (register_to_string reg) ^ "_spill";
sslot_offset = offset;
sslot_btype = t_unknown;
sslot_spill = Some reg;
sslot_size = Some 4;
sslot_desc = Some "register spill"
} in
let sslot = new stackslot_t ssrec in
H.add stackslots offset sslot);
if BCHCPURegisters.is_temporary_register reg then
()
else
let spill = RegisterSpill (offset, reg) in
begin
(if H.mem stackslots offset then
if (H.find stackslots offset)#is_spill then
()
else
let sslot = H.find stackslots offset in
raise
(BCH_failure
(LBLOCK [
STR "Add register spill at address ";
STR iaddr;
STR " for register ";
STR (register_to_string reg);
STR " at offset ";
INT offset;
STR " cannot be completed, because another stackslot ";
STR "at this offset, with name: ";
STR sslot#name;
STR " already exists"]))
else
let ssrec = {
sslot_name = (register_to_string reg) ^ "_spill";
sslot_offset = offset;
sslot_btype = t_unknown;
sslot_spill = Some reg;
sslot_size = Some 4;
sslot_desc = Some "register spill"
} in
let sslot = new stackslot_t ssrec in
H.add stackslots offset sslot);
self#add_access offset iaddr spill
end
end

method add_register_restore
~(offset: int) (reg: register_t) (iaddr: ctxt_iaddress_t) =
let restore = RegisterRestore (offset, reg) in
begin
(if H.mem stackslots offset then
if (H.find stackslots offset)#is_spill then
()
else
let sslot = H.find stackslots offset in
raise
(BCH_failure
(LBLOCK [
STR "Add register restore at address ";
STR iaddr;
STR " for register ";
STR (register_to_string reg);
STR " at offset ";
INT offset;
STR " cannot be completed, because another stackslot ";
STR "at this offset, with name: ";
STR sslot#name;
STR " already exists"]))
else
let ssrec = {
sslot_name = (register_to_string reg) ^ "_spill";
sslot_offset = offset;
sslot_btype = t_unknown;
sslot_spill = Some reg;
sslot_size = Some 4;
sslot_desc = Some "register_spill"
} in
let sslot = new stackslot_t ssrec in
H.add stackslots offset sslot);
self#add_access offset iaddr restore
end
if BCHCPURegisters.is_temporary_register reg then
()
else
let restore = RegisterRestore (offset, reg) in
begin
(if H.mem stackslots offset then
if (H.find stackslots offset)#is_spill then
()
else
let sslot = H.find stackslots offset in
raise
(BCH_failure
(LBLOCK [
STR "Add register restore at address ";
STR iaddr;
STR " for register ";
STR (register_to_string reg);
STR " at offset ";
INT offset;
STR " cannot be completed, because another stackslot ";
STR "at this offset, with name: ";
STR sslot#name;
STR " already exists"]))
else
let ssrec = {
sslot_name = (register_to_string reg) ^ "_spill";
sslot_offset = offset;
sslot_btype = t_unknown;
sslot_spill = Some reg;
sslot_size = Some 4;
sslot_desc = Some "register_spill"
} in
let sslot = new stackslot_t ssrec in
H.add stackslots offset sslot);
self#add_access offset iaddr restore
end

method add_load
~(baseoffset:int)
Expand Down