Skip to content

Stackvariables #205

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
merged 2 commits into from
Aug 6, 2025
Merged

Stackvariables #205

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
f68bc7d
CHB:ARM: add sizes to operands
sipma Aug 6, 2025
cdb220a
CHB: convert index expression to c expression
sipma Aug 6, 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
49 changes: 44 additions & 5 deletions CodeHawk/CHB/bchlib/bCHFloc.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -667,6 +667,16 @@ object (self)
(numoffset: numerical_t): variable_t traceresult =
let inv = self#inv in
let mk_memvar memref_r memoffset_r =
let _ =
log_diagnostics_result
~msg:(p2s self#l#toPretty)
~tag:"get_memory_variable_numoffset:mk_memvar"
__FILE__ __LINE__
["var: " ^ (p2s var#toPretty);
"memref_r: "
^ (TR.tfold_default (fun memref -> p2s memref#toPretty) "error" memref_r);
"memoff_r: "
^ (TR.tfold_default memory_offset_to_string "error" memoffset_r)] in
TR.tbind
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
(fun memref ->
Expand Down Expand Up @@ -1250,21 +1260,44 @@ object (self)
?(size=None)
?(btype=t_unknown)
(addrvalue: xpr_t): variable_t traceresult =
let _ =
log_diagnostics_result
~msg:(p2s self#l#toPretty)
~tag:"get_var_at_address"
__FILE__ __LINE__
["addrvalue: " ^ (x2s addrvalue);
"btype: " ^ (btype_to_string btype)] in

match self#normalize_addrvalue addrvalue with
| XOp ((Xf "addressofvar"), [XVar v]) -> Ok v
| XOp (XPlus, [XOp ((Xf "addressofvar"), [XVar v]); xoff])
when self#f#env#is_global_variable v ->
let gvaddr_r = self#f#env#get_global_variable_address v in
let cxoff_r = self#convert_xpr_to_c_expr xoff in
TR.tbind
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
(fun gvaddr ->
if memmap#has_location gvaddr then
let gloc = memmap#get_location gvaddr in
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 xoff)
let varresult =
TR.tmap
~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
(fun offset -> self#f#env#mk_gloc_variable gloc offset)
(TR.tbind
(fun xoff ->
gloc#address_offset_memory_offset
~tgtsize:size ~tgtbtype:btype xoff)
cxoff_r) in
let _ =
log_diagnostics_result
~msg:(p2s self#l#toPretty)
~tag:"normalized global address"
__FILE__ __LINE__
["varresult: "
^ (TR.tfold_default (fun v -> p2s v#toPretty) "error" varresult);
"gloc: " ^ gloc#name] in
varresult

else
Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
^ (p2s self#l#toPretty)
Expand Down Expand Up @@ -1805,6 +1838,12 @@ object (self)

method decompose_memaddr (x: xpr_t):
(memory_reference_int traceresult * memory_offset_t traceresult) =
let _ =
log_diagnostics_result
~msg:(p2s self#l#toPretty)
~tag:"decompose_memaddr"
__FILE__ __LINE__
["x: " ^ (x2s x)] in
let is_external (v: variable_t) = self#env#is_function_initial_value v in
let vars = vars_as_positive_terms x in
let knownpointers = List.filter self#f#is_base_pointer vars in
Expand Down
4 changes: 2 additions & 2 deletions CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -692,8 +692,8 @@ object (self)
Some (t_ptrto (type_constant_to_btype c))
| [Store; OffsetAccess _] ->
Some (t_ptrto (type_constant_to_btype c))
| [OffsetAccessA (_size, _)] ->
Some (t_array (type_constant_to_btype c) 1)
| [OffsetAccessA (size, _)] ->
Some (t_array (type_constant_to_btype c) size)
| _ -> None in
match optty with
| Some ty -> result#add (bcd#index_typ ty)
Expand Down
38 changes: 24 additions & 14 deletions CodeHawk/CHB/bchlibarm32/bCHDisassembleARMInstruction.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,8 @@ let parse_data_proc_reg_load_stores
let rn = arm_register_op rnreg (if iswback then RW else RD) in
let rm = arm_register_op rmreg RD in
let offset = arm_index_offset rmreg in
let mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback WR in
let mem =
mk_arm_offset_address_op rnreg offset ~size:2 ~isadd ~isindex ~iswback WR in
(* STRH{<c>} <Rt>, [<Rn>, +/-<Rm>]{!} Pre-x : (index,wback) = (T,T/F)
* STRH{<c>} <Rt>, [<Rn>], +/-<Rm> Post-x: (index,wback) = (F,T) *)
StoreRegisterHalfword (c, rt, rn, rm, mem, false)
Expand Down Expand Up @@ -264,7 +265,8 @@ let parse_data_proc_reg_load_stores
let rn = arm_register_op rnreg (if iswback then RW else RD) in
let rm = arm_register_op rmreg RD in
let offset = arm_index_offset rmreg in
let mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback RD in
let mem =
mk_arm_offset_address_op rnreg offset ~size:2 ~isadd ~isindex ~iswback RD in
(* LDRH<c> <Rt>, [<Rn>, +/-<Rm>]{!} Pre-x : (index,wback) = (T,T/F)
* LDRH<c> <Rt>, [<Rn>], +/-<Rm> Post-x: (index,wback) = (F,T) *)
LoadRegisterHalfword (c, rt, rn, rm, mem, false)
Expand All @@ -277,7 +279,8 @@ let parse_data_proc_reg_load_stores
let rn = arm_register_op rnreg (if iswback then RW else RD) in
let rm = arm_register_op rmreg RD in
let offset = arm_index_offset rmreg in
let mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback RD in
let mem =
mk_arm_offset_address_op rnreg offset ~size:1 ~isadd ~isindex ~iswback RD in
(* LDRSB<c> <Rt>, [<Rn>,+/-<Rm>]{!}
* LDRSB<c> <Rt>, [<Rn>],+/-<Rm> *)
LoadRegisterSignedByte (c, rt, rn, rm, mem, false)
Expand All @@ -290,7 +293,8 @@ let parse_data_proc_reg_load_stores
let rn = arm_register_op rnreg (if iswback then RW else RD) in
let rm = arm_register_op rmreg RD in
let offset = arm_index_offset rmreg in
let mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback RD in
let mem =
mk_arm_offset_address_op rnreg offset ~size:2 ~isadd ~isindex ~iswback RD in
(* LDRSH<c> <Rt>, [<Rn>,+/-<Rm>]{!} *)
(* LDRSH<c> <Rt>, [<Rn>],+/-<rm> *)
LoadRegisterSignedHalfword (c, rt, rn, rm, mem, false)
Expand All @@ -308,7 +312,8 @@ let parse_data_proc_reg_load_stores
(signed_immediate_from_int imm32) in
let imm = arm_immediate_op imm in
let offset = ARMImmOffset imm32 in
let mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback WR in
let mem =
mk_arm_offset_address_op rnreg offset ~size:2 ~isadd ~isindex ~iswback WR in
(* STRH<c> <Rt>, [<Rn>{, #+/-<imm8>}] Offset: (index,wback) = (T,F)
* STRH<c> <Rt>, [<Rn>, #+/-<imm>]! Pre-x : (index,wback) = (T,T)
* STRH<c> <Rt>, [<Rn>], #+/-<imm> Post-x: (index,wback) = (F,T) *)
Expand Down Expand Up @@ -385,7 +390,8 @@ let parse_data_proc_reg_load_stores
(signed_immediate_from_int imm32) in
let imm = arm_immediate_op imm in
let offset = ARMImmOffset imm32 in
let mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback RD in
let mem =
mk_arm_offset_address_op rnreg offset ~size:2 ~isadd ~isindex ~iswback RD in
(* LDRH<c> <Rt>, [<Rn>{, #+/-<imm>}] Offset: (index,wback) = (T,F)
* LDRH<c> <Rt>, [<Rn>, #+/-<imm>]! Pre-x : (index,wback) = (T,T)
* LDRH<c> <Rt>, [<Rn>], #+/-<imm> Post-x: (index,wback) = (F,T) *)
Expand All @@ -404,7 +410,8 @@ let parse_data_proc_reg_load_stores
(signed_immediate_from_int imm32) in
let imm = arm_immediate_op imm in
let offset = ARMImmOffset imm32 in
let mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback RD in
let mem =
mk_arm_offset_address_op rnreg offset ~size:1 ~isadd ~isindex ~iswback RD in
(* LDRSB<c> <Rt>, [<Rn>{, #+/-<imm8>}]
* LDRSB<c> <Rt>, [<Rn>], #+/-<imm8>
* LDRSB<c> <Rt>, [<Rn>, #+/-<imm8>]! *)
Expand All @@ -423,7 +430,8 @@ let parse_data_proc_reg_load_stores
(signed_immediate_from_int imm32) in
let imm = arm_immediate_op imm in
let offset = ARMImmOffset imm32 in
let mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback RD in
let mem =
mk_arm_offset_address_op rnreg offset ~size:2 ~isadd ~isindex ~iswback RD in
(* LDRSH<c> <Rt>, [<Rn>{, #+/-<imm8>}]
* LDRSH<c> <Rt>, [<Rn>], #+/-<imm8>
* LDRSH<c> <Rt>, [<Rn>, #+/-<imm8>]! *)
Expand Down Expand Up @@ -1202,7 +1210,8 @@ let parse_load_store_imm_type
let imm12 = b 11 0 in
let imm = TR.tget_ok (mk_arm_immediate_op false 4 (mkNumerical imm12)) in
let offset = ARMImmOffset imm12 in
let mk_mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback in
let mk_mem ?(size=4) (mode: arm_operand_mode_t) =
mk_arm_offset_address_op rnreg offset ~size ~isadd ~isindex ~iswback mode in
match (b 22 22, b 20 20, (rnval, p, u, w, imm12)) with

(* <cc><2>10010<13><rt><--imm12:4-> *) (* PUSH - A2 *)
Expand Down Expand Up @@ -1241,15 +1250,15 @@ let parse_load_store_imm_type

(* <cc><2>pu1w0<rn><rt><--imm12---> *) (* STRB-imm *)
| (1, 0, _) ->
let mem = mk_mem WR in
let mem = mk_mem ~size:1 WR in
(* STRB<c> <Rt>, [<Rn>{, #+/-<imm12>}] Offset: (index,wback) = (T,F)
* STRB<c> <Rt>, [<Rn>, #+/-<imm12>]! Pre-x : (index,wback) = (T,T)
* STRB<c> <Rt>, [<Rn>], #+/-<imm12> Post-x: (index,wback) = (F,T) *)
StoreRegisterByte (c, rt RD, rn, imm, mem, false)

(* <cc><2>pu1w1<rn><rt><--imm12---> *) (* LDRB-imm *)
| (1, 1, _) ->
let mem = mk_mem RD in
let mem = mk_mem ~size:1 RD in
(* LDRB<c> <Rt>, [<Rn>{, #+/-<imm12>}] Offset: (index,wback) = (T,F)
* LDRB<c> <Rt>, [<Rn>, #+/-<imm12>]! Pre-x : (index,wback) = (T,T)
* LDRB<c> <Rt>, [<Rn>], #+/-<imm12> Post-x: (index,wback) = (F,T) *)
Expand Down Expand Up @@ -1282,7 +1291,8 @@ let parse_load_store_reg_type (instr: doubleword_int) (cond: int) =
let (shift_t, shift_n) = decode_imm_shift (b 6 5) (b 11 7) in
let reg_srt = ARMImmSRT (shift_t, shift_n) in
let offset = arm_shifted_index_offset (get_arm_reg (b 3 0)) reg_srt in
let mk_mem = mk_arm_offset_address_op rnreg offset ~isadd ~isindex ~iswback in
let mk_mem ?(size=4) (mode: arm_operand_mode_t) =
mk_arm_offset_address_op rnreg offset ~size ~isadd ~isindex ~iswback mode in
let selector = (bv 22, bv 20) in
match selector with
(* <cc><3>pu0w0<rn><rt><imm>ty0<rm> *) (* STR (register) - A1 *)
Expand All @@ -1301,14 +1311,14 @@ let parse_load_store_reg_type (instr: doubleword_int) (cond: int) =

(* <cc><3>pu1w0<rn><rt><imm>ty0<rm> *) (* STRB (register) - A1 *)
| (1, 0) ->
let mem = mk_mem WR in
let mem = mk_mem ~size:1 WR in
(* STRB<c> <Rt>, [<Rn>,+/-<Rm>{, <shift>}]{!} *)
(* STRB<c> <Rt>, [<Rn>],+/-<Rm>{, <shift>} *)
StoreRegisterByte (c, rt RD, rn, rm, mem, false)

(* <cc><3>pu1w1<rn><rt><imm>ty0<rm> *) (* LDRB (register) - A1 *)
| (1, 1) ->
let mem = mk_mem RD in
let mem = mk_mem ~size:1 RD in
LoadRegisterByte (c, rt WR, rn, rm, mem, false)

| _ -> OpInvalid
Expand Down
Loading