From 93fadb031eaf36ba3f9368ae739c55f0546756fb Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Fri, 22 Aug 2025 09:13:42 -0700 Subject: [PATCH 1/2] CHB:fix zero-offset accesses to global arrays --- CodeHawk/CHB/bchlib/bCHFloc.ml | 147 ++++++++++++------ CodeHawk/CHB/bchlib/bCHFunctionInfo.ml | 43 +++-- CodeHawk/CHB/bchlib/bCHLibTypes.mli | 6 + CodeHawk/CHB/bchlib/bCHVariable.ml | 16 ++ CodeHawk/CHB/bchlib/bCHVersion.ml | 4 +- .../CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 19 ++- .../bchlib_tests/txbchlib/bCHFlocTest.ml | 27 ++-- .../bCHTranslateARMToCHIFTest.ml | 4 +- 8 files changed, 170 insertions(+), 96 deletions(-) diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 0b69730e..d38d5f57 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -90,15 +90,13 @@ let x2p = xpr_formatter#pr_expr let p2s = pretty_to_string let x2s x = p2s (x2p x) -let opt_size_to_string (s: int option) = - match s with - | Some i -> "size:" ^ (string_of_int i) - | _ -> "size:None" +let opti2s (i: int option) = + if Option.is_some i then string_of_int (Option.get i) else "?" -let opt_type_to_string (t: btype_t option) = - match t with - | Some t -> "btype:" ^ (btype_to_string t) - | _ -> "btype:None" +let _ty2s (ty: btype_t) = + if is_unknown_type ty then "?" else btype_to_string ty +let optty2s (ty: btype_t option) = + if Option.is_some ty then btype_to_string (Option.get ty) else "?" let log_error (tag: string) (msg: string): tracelogspec_t = @@ -665,6 +663,14 @@ object (self) ?(size=4) (var: variable_t) (numoffset: numerical_t): variable_t traceresult = + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get-memory-variable-numoffset" + __FILE__ __LINE__ + ["size: " ^ (string_of_int size); + "var: " ^ (p2s var#toPretty); + "numoffset: " ^ (numoffset#toString)] in let inv = self#inv in let mk_memvar memref_r memoffset_r = let _ = @@ -1512,9 +1518,9 @@ object (self) ~msg:(p2s self#l#toPretty) ~tag:"convert_xpr_to_c_expr" __FILE__ __LINE__ - [(opt_size_to_string size) ^ "; " - ^ (opt_type_to_string xtype) ^ "; " - ^ "x: " ^ (x2s x)] in + ["size: " ^ (opti2s size); + "xtype: " ^ (optty2s xtype); + "x: " ^ (x2s x)] in match xtype with | None -> self#convert_xpr_offsets ~size x | Some t -> @@ -1598,8 +1604,8 @@ object (self) TR.tmap (fun v -> XVar v) var_r | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ (opt_size_to_string size) ^ "; " - ^ (opt_type_to_string xtype) ^ "; " + ^ "size: " ^ (opti2s size) ^ "; " + ^ "type: " ^ (optty2s xtype) ^ "; " ^ "addr: " ^ (x2s a) ^ ": Not yet handled"] @@ -1609,8 +1615,8 @@ object (self) | None -> self#convert_variable_offsets ~size v | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ (opt_size_to_string size) ^ "; " - ^ (opt_type_to_string vtype) ^ "; " + ^ "size: " ^ (opti2s size) ^ "; " + ^ "type: " ^ (optty2s vtype) ^ "; " ^ "v: " ^ (p2s v#toPretty) ^ ": Not yet implemented"] @@ -1672,14 +1678,22 @@ object (self) memref_r memoff_r | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ (opt_size_to_string size) ^ "; " - ^ (opt_type_to_string vtype) ^ "; " + ^ "size: " ^ (opti2s size) ^ "; " + ^ "vtype: " ^ (optty2s vtype) ^ "; " ^ "addr: " ^ (x2s a) ^ ": Not yet handled"] method convert_variable_offsets ?(vtype=None) ?(size=None) (v: variable_t): variable_t traceresult = + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"convert-variable-offsets" + __FILE__ __LINE__ + ["vtype: " ^ (optty2s vtype); + "size: " ^ (opti2s size); + "v: " ^ (p2s v#toPretty)] in if self#env#is_basevar_memory_variable v then let basevar_r = self#env#get_memvar_basevar v in let offset_r = self#env#get_memvar_offset v in @@ -1737,6 +1751,12 @@ object (self) method convert_value_offsets ?(size=None) (v: variable_t): variable_t traceresult = + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"convert-value-offsets" + __FILE__ __LINE__ + ["size: " ^ (opti2s size); "v: " ^ (p2s v#toPretty)] in if self#env#is_basevar_memory_value v then let basevar_r = self#env#get_memval_basevar v in let offset_r = self#env#get_memval_offset v in @@ -1812,6 +1832,12 @@ object (self) method convert_xpr_offsets ?(xtype=None) ?(size=None) (x: xpr_t): xpr_t traceresult = + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"convert-xpr-offsets" + __FILE__ __LINE__ + ["xtype: " ^ (optty2s xtype); "size: " ^ (opti2s size); "x: " ^ (x2s x)] in let rec aux exp = match exp with | XVar v when self#env#is_basevar_memory_value v -> @@ -2349,41 +2375,51 @@ object (self) rhs | _ -> rhs in - let rhs = - (* if rhs is a composite symbolic expression, create a new variable + if self#f#env#is_global_variable lhs then + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:("get_assign_cmds_r: abstract global variable") + __FILE__ __LINE__ + ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s rhs)] in + [ABSTRACT_VARS [lhs]] + + else + let rhs = + (* if rhs is a composite symbolic expression, create a new variable for it *) - if self#is_composite_symbolic_value rhs then - XVar (self#env#mk_symbolic_value rhs) - else - rhs in - let reqN () = self#env#mk_num_temp in - let reqC = self#env#request_num_constant in - let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in - let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in - let fndata = self#f#get_function_data in - match fndata#get_regvar_intro self#ia with - | Some rvi when rvi.rvi_cast && Option.is_some rvi.rvi_vartype -> - TR.tfold - ~ok:(fun reg -> - let ty = Option.get rvi.rvi_vartype in - let tcvar = - self#f#env#mk_typecast_value self#cia rvi.rvi_name ty reg in - begin - log_result __FILE__ __LINE__ - ["Create typecast var for " - ^ (register_to_string reg) - ^ " at " - ^ self#cia]; - cmds @ [ASSIGN_NUM (lhs, NUM_VAR tcvar)] - end) - ~error:(fun e -> - begin - log_error_result __FILE__ __LINE__ - ("expected a register variable" :: e); - cmds - end) - (self#f#env#get_register lhs) - | _ -> cmds + if self#is_composite_symbolic_value rhs then + XVar (self#env#mk_symbolic_value rhs) + else + rhs in + let reqN () = self#env#mk_num_temp in + let reqC = self#env#request_num_constant in + let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in + let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in + let fndata = self#f#get_function_data in + match fndata#get_regvar_intro self#ia with + | Some rvi when rvi.rvi_cast && Option.is_some rvi.rvi_vartype -> + TR.tfold + ~ok:(fun reg -> + let ty = Option.get rvi.rvi_vartype in + let tcvar = + self#f#env#mk_typecast_value self#cia rvi.rvi_name ty reg in + begin + log_result __FILE__ __LINE__ + ["Create typecast var for " + ^ (register_to_string reg) + ^ " at " + ^ self#cia]; + cmds @ [ASSIGN_NUM (lhs, NUM_VAR tcvar)] + end) + ~error:(fun e -> + begin + log_error_result __FILE__ __LINE__ + ("expected a register variable" :: e); + cmds + end) + (self#f#env#get_register lhs) + | _ -> cmds (* Note: recording of loads and stores is performed by the different architectures directly in FnXXXDictionary.*) @@ -2448,6 +2484,15 @@ object (self) [OPERATION ({ op_name = unknown_write_symbol; op_args = op_args}); ASSIGN_NUM (lhs, rhs)] + else if self#f#env#is_global_variable lhs then + let _ = + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:("get_assign_cmds: abstract global variable") + __FILE__ __LINE__ + ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s rhs_expr)] in + [ABSTRACT_VARS [lhs]] + else rhsCmds @ [ASSIGN_NUM (lhs, rhs)] diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 86222a12..2ead7e3b 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -851,29 +851,23 @@ object (self) let gvar = self#mk_variable (self#varmgr#make_global_variable gloc#address#to_numerical) in - let ivar = self#mk_variable (varmgr#make_initial_memory_value gvar) in - if dw#equal gloc#address then - begin - self#set_variable_name gvar gloc#name; - self#set_variable_name ivar (gloc#name ^ "_in"); - Ok gvar - end - else - tmap - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global") - (fun offset -> - let gvar = - self#mk_variable - (self#varmgr#make_global_variable - ~size ~offset gloc#address#to_numerical) in - let ivar = self#mk_variable (varmgr#make_initial_memory_value gvar) in - let name = gloc#name ^ (memory_offset_to_string offset) in - begin - self#set_variable_name gvar name; - self#set_variable_name ivar (name ^ "_in"); - gvar - end) - (gloc#address_memory_offset ~tgtbtype:btype loc (num_constant_expr base)) + let _ivar = self#mk_variable (varmgr#make_initial_memory_value gvar) in + tmap + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global") + (fun offset -> + let gvar = + self#mk_variable + (self#varmgr#make_global_variable + ~size ~offset gloc#address#to_numerical) in + let ivar = self#mk_variable (varmgr#make_initial_memory_value gvar) in + let name = gloc#name ^ (memory_offset_to_string offset) in + begin + self#set_variable_name gvar name; + self#set_variable_name ivar (name ^ "_in"); + gvar + end) + (gloc#address_memory_offset + ~tgtsize:(Some size) ~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)) @@ -1223,6 +1217,9 @@ object (self) method get_memval_offset (v:variable_t): memory_offset_t traceresult = varmgr#get_memval_offset v + method get_memvar_dependencies (v: variable_t): variable_t list = + varmgr#get_memvar_dependencies v + method get_constant_offsets (v: variable_t): numerical_t list traceresult = let offset_r = if self#is_initial_memory_value v then diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 27a65a49..a0e72d79 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -3618,6 +3618,8 @@ object ('a) Returns [Error] if this variable is not a register variable. *) method get_register: register_t traceresult + method get_memvar_dependencies: variable_t list + (** Returns the memory reference associated with this memory variable. Returns [Error] if this variable is not a memory variable. *) @@ -4063,6 +4065,8 @@ object initial-value memory variable. *) method get_initial_memory_value_variable: variable_t -> variable_t traceresult + method get_memvar_dependencies: variable_t -> variable_t list + (** {2 Memory offsets} *) @@ -4944,6 +4948,8 @@ class type function_environment_int = method has_variable_index_offset: variable_t -> bool + method get_memvar_dependencies: variable_t -> variable_t list + (** {2 Memory offsets} *) diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml index 2fe72880..2082babb 100644 --- a/CodeHawk/CHB/bchlib/bCHVariable.ml +++ b/CodeHawk/CHB/bchlib/bCHVariable.ml @@ -155,6 +155,16 @@ object (self:'a) else name + method get_memvar_dependencies: variable_t list = + match denotation with + | MemoryVariable (_, _, offset) -> + (match offset with + | ArrayIndexOffset (x, _) -> Xprt.variables_in_expr x + | BasePtrArrayIndexOffset (x, _) -> Xprt.variables_in_expr x + | ConstantOffset (_, ArrayIndexOffset (x, _)) -> Xprt.variables_in_expr x + | _ -> []) + | _ -> [] + method private get_memref_type (index: int) (_size: int): btype_t option = memrefmgr#get_memory_reference_type index @@ -562,6 +572,12 @@ object (self) None (self#get_variable v) + method get_memvar_dependencies (v: variable_t): variable_t list = + tfold_default + (fun var -> var#get_memvar_dependencies) + [] + (self#get_variable v) + method get_memvar_reference (v: variable_t): memory_reference_int traceresult = tbind ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty)) diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index f51872fa..270b8754 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20250821" - ~date:"2025-08-21" + ~version:"0.6.0_20250822" + ~date:"2025-08-22" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 02c42adb..43d34369 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -3172,7 +3172,24 @@ let translate_arm_instruction TR.tfold ~ok:(fun (memlhs, memcmds) -> let cmds = floc#get_assign_commands_r (Ok memlhs) xrt_r in - let defcmds = floc#get_vardef_commands ~defs:[memlhs] ctxtiaddr in + let memvardeps = floc#f#env#get_memvar_dependencies memlhs in + let usehigh = + List.filter (fun v -> not (floc#f#env#is_function_initial_value v)) + memvardeps in + let _ = + log_diagnostics_result + ~msg:(p2s floc#l#toPretty) + ~tag:"translate memlhs storeregister" + __FILE__ __LINE__ + ["memlhs: " ^ (p2s memlhs#toPretty); + "memvardeps: " + ^ (String.concat + ", " (List.map (fun v -> p2s v#toPretty) memvardeps)); + "usehigh: " + ^ (String.concat + ", " (List.map (fun v -> p2s v#toPretty) usehigh))] in + let defcmds = + floc#get_vardef_commands ~defs:[memlhs] ~usehigh ctxtiaddr in memcmds @ cmds @ defcmds) ~error:(fun e -> let xrn_r = rn#to_expr floc in diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFlocTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFlocTest.ml index bd76ca8e..ebfaae8e 100644 --- a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFlocTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHFlocTest.ml @@ -51,7 +51,7 @@ let mmap = BCHGlobalMemoryMap.global_memory_map let testname = "bCHFlocTest" -let lastupdated = "2025-08-19" +let lastupdated = "2025-08-21" let get_var_at_address_test () = @@ -64,7 +64,6 @@ let get_var_at_address_test () = let dwfaddr = TR.tget_ok (string_to_doubleword faddr) in let dwiaddr = TR.tget_ok (string_to_doubleword iaddr) in let dwgvaddr = TR.tget_ok (string_to_doubleword gvaddr) in - let loc = BCHLocation.make_location_by_address dwfaddr dwiaddr in let dwgvxpr = num_constant_expr dwgvaddr#to_numerical in begin TS.new_testsuite @@ -75,7 +74,8 @@ let get_var_at_address_test () = let compinfo = bcfiles#get_compinfo_by_name "x44_struct_t" in let finfo = get_function_info dwfaddr in let floc = get_floc_by_address dwfaddr dwiaddr in - let gvar = TR.tget_ok (finfo#env#mk_global_variable loc dwgvaddr#to_numerical) in + let gloc = + TR.tget_ok (BCHGlobalMemoryMap.global_memory_map#add_location dwgvaddr) in let indexvar = finfo#env#mk_initial_register_value (ARMRegister AR0) in let indexxpr1 = XOp (XMinus, [XVar indexvar; int_constant_expr 1]) in @@ -87,8 +87,7 @@ let get_var_at_address_test () = let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in let xpoffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in let xpoffset = ArrayIndexOffset(int_constant_expr 1, xpoffset) in - let expected_r = finfo#env#add_memory_offset gvar xpoffset in - let expected = TR.to_option expected_r in + let expected = Some (finfo#env#mk_gloc_variable gloc xpoffset) in match xprvar with Ok received -> XBA.equal_opt_variable @@ -105,8 +104,7 @@ let get_var_at_address_test () = let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in let xpoffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in let xpoffset = ArrayIndexOffset(int_constant_expr 1, xpoffset) in - let expected_r = finfo#env#add_memory_offset gvar xpoffset in - let expected = TR.to_option expected_r in + let expected = Some (finfo#env#mk_gloc_variable gloc xpoffset) in match xprvar with Ok received -> XBA.equal_opt_variable @@ -124,8 +122,7 @@ let get_var_at_address_test () = let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in let xpoffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in let xpoffset = ArrayIndexOffset(XVar indexvar, xpoffset) in - let expected_r = finfo#env#add_memory_offset gvar xpoffset in - let expected = TR.to_option expected_r in + let expected = Some (finfo#env#mk_gloc_variable gloc xpoffset) in match xprvar with | Ok received -> XBA.equal_opt_variable @@ -144,8 +141,7 @@ let get_var_at_address_test () = let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in let xpoffset = FieldOffset (("field0", compinfo.bckey), NoOffset) in let xpoffset = ArrayIndexOffset(indexxpr1, xpoffset) in - let expected_r = finfo#env#add_memory_offset gvar xpoffset in - let expected = TR.to_option expected_r in + let expected = Some (finfo#env#mk_gloc_variable gloc xpoffset) in match xprvar with | Ok received -> XBA.equal_opt_variable @@ -163,8 +159,7 @@ let get_var_at_address_test () = let xprvar = floc#get_var_at_address ~btype:BCHBCTypeUtil.t_int xpr in let xpoffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in let xpoffset = ArrayIndexOffset(indexxpr1, xpoffset) in - let expected_r = finfo#env#add_memory_offset gvar xpoffset in - let expected = TR.to_option expected_r in + let expected = Some (finfo#env#mk_gloc_variable gloc xpoffset) in match xprvar with | Ok received -> XBA.equal_opt_variable @@ -183,8 +178,7 @@ let get_var_at_address_test () = let xpoffset = ArrayIndexOffset (int_constant_expr 0, NoOffset) in let xpoffset = FieldOffset (("buffer", compinfo.bckey), xpoffset) in let xpoffset = ArrayIndexOffset(indexxpr1, xpoffset) in - let expected_r = finfo#env#add_memory_offset gvar xpoffset in - let expected = TR.to_option expected_r in + let expected = Some (finfo#env#mk_gloc_variable gloc xpoffset) in match xprvar with | Ok received -> XBA.equal_opt_variable @@ -206,8 +200,7 @@ let get_var_at_address_test () = let xprvar = floc#get_var_at_address xpr in let xpoffset = FieldOffset (("field4", compinfo.bckey), NoOffset) in let xpoffset = ArrayIndexOffset(indexxpr1, xpoffset) in - let expected_r = finfo#env#add_memory_offset gvar xpoffset in - let expected = TR.to_option expected_r in + let expected = Some (finfo#env#mk_gloc_variable gloc xpoffset) in match xprvar with | Ok received -> XBA.equal_opt_variable diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml index 16f980d1..3b129f61 100644 --- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml @@ -154,7 +154,7 @@ let thumb_chif_conditionxprs () = "0x4f12", "44f6251393f87094b9f1910ff94602d8a9f6e1594847a9f6e769484700", 3, - "(gv_0x4d95_in >= 0)") + "(gvb_0x4d95_in >= 0)") ] in begin TS.new_testsuite (testname ^ "_thumb_chif_conditionxprs") lastupdated; @@ -208,7 +208,7 @@ let thumb_instrxdata_conditionxprs () = "0x4f12", "44f6251393f87094b9f1910ff94602d8a9f6e1594847a9f6e769484700", 3, - "((gv_0x4d95_in <= 145) and (gv_0x4d95_in >= 0))") + "((gvb_0x4d95_in <= 145) and (gvb_0x4d95_in >= 0))") ] in begin TS.new_testsuite (testname ^ "_thumb_instrxdata_conditionxprs") lastupdated; From d1cc5029d252e3e956ad90c9bcdfad6ba5bbfba6 Mon Sep 17 00:00:00 2001 From: Henny Sipma Date: Fri, 22 Aug 2025 11:21:02 -0700 Subject: [PATCH 2/2] CHB:ARM: fix register spill offset --- CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 43d34369..54a81386 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -2552,13 +2552,12 @@ let translate_arm_instruction TR.tfold ~ok:(fun rhsvar -> let rhsreg = TR.tget_ok (finfo#env#get_register rhsvar) in - let _ = - if floc#has_initial_value rhsvar then - finfo#stackframe#add_register_spill - ~offset:off rhsreg floc#cia in let stackop = arm_sp_deref ~with_offset:off WR in TR.tfold ~ok:(fun (stacklhs, stacklhscmds) -> + let _ = + if floc#has_initial_value rhsvar then + finfo#save_register stacklhs floc#cia rhsreg in let rhsexpr = rewrite_expr floc (XVar rhsvar) in let cmds1 = floc#get_assign_commands stacklhs rhsexpr in let usehigh = get_use_high_vars [rhsexpr] in