diff --git a/CodeHawk/CH/xprlib/xsimplify.ml b/CodeHawk/CH/xprlib/xsimplify.ml index af1b4830c..839a534d5 100644 --- a/CodeHawk/CH/xprlib/xsimplify.ml +++ b/CodeHawk/CH/xprlib/xsimplify.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -117,7 +117,36 @@ let pwr2 (num: numerical_t): xpr_t = let rec sim_expr (m:bool) (e:xpr_t):(bool * xpr_t) = + (* the first three match expressions are patterns created during wide + operations, where the high word and low word are combined; often the + original 64-bit word can be recovered.*) match e with + | XOp (XPlus, + [XOp (XMult, + [XOp (XAsr, [x; XConst (IntConst n)]); XConst (IntConst k)]); + y]) when (n#equal (mkNumerical 31)) + && (k#equal numerical_e32) + && (syntactically_equal x y) -> + let (_, s) = sim_expr m x in + (true, XOp ((Xf "signextend64"), [s])) + | XOp (XPlus, + [XOp (XMult, [XOp (XAsr, [x; XConst (IntConst n)]); XConst (IntConst k)]); + XOp (XMod, [y; XConst (IntConst l)])]) + when (n#equal (mkNumerical 32)) + && (k#equal numerical_e32) + && (l#equal numerical_e32) + && (syntactically_equal x y) -> + let (_, s) = sim_expr m x in + (true, s) + | XOp (XPlus, + [XOp (XMult, [XConst (IntConst k); XOp (XAsr, [x; XConst (IntConst n)])]); + XOp (XMod, [y; XConst (IntConst l)])]) + when (n#equal (mkNumerical 32)) + && (k#equal numerical_e32) + && (l#equal numerical_e32) + && (syntactically_equal x y) -> + let (_, s) = sim_expr m x in + (true, s) | XOp (XNeg, [e1]) -> let (m, s) = sim_expr m e1 in reduce_neg m s | XOp (XBNot, [e1]) -> @@ -592,7 +621,7 @@ and reduce_mod (m: bool) (e1: xpr_t) (e2: xpr_t): (bool * xpr_t) = (true, ne result) (* x % b -> [0; (b-1)] *) - | (_, SConst b) when b#geq numerical_zero -> + | (_, SConst b) when b#gt numerical_zero && b#lt (mkNumerical 100)-> let ub = b#sub numerical_one in (true, XOp (XNumRange, [zero_constant_expr; num_constant_expr ub])) diff --git a/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml b/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml index 0350191f5..6c4a92588 100644 --- a/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml +++ b/CodeHawk/CHB/bchcmdline/bCHXBinaryAnalyzer.ml @@ -163,6 +163,8 @@ let speclist = ("-arm_extension_registers", Arg.Unit (fun () -> system_settings#set_arm_extension_registers), "include arm floating point registers in analysis"); + ("-float-abi", Arg.String system_settings#set_float_abi, + "indication of the presence of VPP/NEON instructons in arm architecture"); ("-thumb", Arg.Unit (fun () -> system_settings#set_thumb), "arm executable includes thumb instructions"); ("-mips", Arg.Unit (fun () -> system_settings#set_architecture "mips"), diff --git a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml index aea5ef16a..313267637 100644 --- a/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHARMFunctionInterface.ml @@ -288,27 +288,68 @@ let get_float_param_next_state STR "Inconsistent arm-argument-state: "; STR "both next sp-reg and offset are None"])))) | TFloat (FDouble, _, _) -> - (match aa_state.aas_next_dp_reg with - | Some reg -> - let register = register_of_arm_extension_register reg in - let par: fts_parameter_t = - mk_indexed_register_parameter ~btype ~name ~size register index in - let naas = get_next_dp_reg_naas aa_state in - (par, naas) - | _ -> - (match aa_state.aas_next_offset with - | Some offset -> - let par: fts_parameter_t = - mk_indexed_stack_parameter ~btype ~name offset index in - let naas = - {aa_state with aas_next_offset = Some (offset + size)} in - (par, naas) - | _ -> - raise - (BCH_failure - (LBLOCK [ - STR "Inconsistent arm-argument-state: "; - STR "both next sp-reg and offset are None"])))) + if BCHSystemSettings.system_settings#is_hard_float then + (match aa_state.aas_next_dp_reg with + | Some reg -> + let register = register_of_arm_extension_register reg in + let par: fts_parameter_t = + mk_indexed_register_parameter ~btype ~name ~size register index in + let naas = get_next_dp_reg_naas aa_state in + (par, naas) + | _ -> + (match aa_state.aas_next_offset with + | Some offset -> + let par: fts_parameter_t = + mk_indexed_stack_parameter ~btype ~name offset index in + let naas = + {aa_state with aas_next_offset = Some (offset + size)} in + (par, naas) + | _ -> + raise + (BCH_failure + (LBLOCK [ + STR "Inconsistent arm-argument-state: "; + STR "both next sp-reg and offset are None"])))) + else + (match aa_state.aas_next_core_reg with + | Some AR0 -> + let register = register_of_arm_double_register AR0 AR1 in + let par: fts_parameter_t = + mk_indexed_register_parameter ~btype ~name ~size register index in + let naas = {aa_state with aas_next_core_reg = Some AR2} in + (par, naas) + | Some (AR1 | AR2) -> + let register = register_of_arm_double_register AR2 AR3 in + let par: fts_parameter_t = + mk_indexed_register_parameter ~btype ~name ~size register index in + let naas = + {aa_state with aas_next_core_reg = None; aas_next_offset = Some 0} in + (par, naas) + | Some AR3 -> + let par: fts_parameter_t = + mk_indexed_stack_parameter ~btype ~name 0 index in + let naas = + {aa_state with aas_next_core_reg = None; aas_next_offset = Some size} in + (par, naas) + | Some _ -> + raise + (BCH_failure + (LBLOCK [STR "Inconsistent state in get_long_int_param_next_state"])) + | _ -> + match aa_state.aas_next_offset with + | Some offset -> + let par: fts_parameter_t = + mk_indexed_stack_parameter ~btype ~name offset index in + let naas = + {aa_state with aas_next_offset = Some (offset + size)} in + (par, naas) + | _ -> + raise + (BCH_failure + (LBLOCK [ + STR "Inconsistent arm-argument-state: "; + STR "both next register and offset are None"]))) + | _ -> raise (BCH_failure diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml index 76a048917..eadcfa67d 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml @@ -245,6 +245,13 @@ let is_array_type t = match t with TArray _ -> true | _ -> false let is_function_type t = match t with TFun _ | TPtr (TFun _,_) -> true | _ -> false +let is_wide_type t = + match t with + | TFloat (FDouble, _, _) + | TInt (ILongLong, _) + | TInt (IULongLong, _) -> true + | _ -> false + let is_unknown_type t = match t with | TUnknown _ -> true diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli index 29d9975d9..0f8ee82b7 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli +++ b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli @@ -157,6 +157,8 @@ val is_struct_type: btype_t -> bool val is_array_type: btype_t -> bool val is_pointer_to_struct: btype_t -> bool +val is_wide_type: btype_t -> bool + val is_volatile: btype_t -> bool (** Returns true if [ty] is a function type with attribute [stdcall].*) diff --git a/CodeHawk/CHB/bchlib/bCHCPURegisters.ml b/CodeHawk/CHB/bchlib/bCHCPURegisters.ml index e1305df62..8a470572d 100644 --- a/CodeHawk/CHB/bchlib/bCHCPURegisters.ml +++ b/CodeHawk/CHB/bchlib/bCHCPURegisters.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -462,10 +462,22 @@ let register_of_mips_floating_point_register_index (index: int): register_t = let register_of_arm_register (r: arm_reg_t): register_t = ARMRegister r +let register_to_arm_register (r: register_t): arm_reg_t option = + match r with + | ARMRegister a -> Some a + | _ -> None + + let register_of_arm_double_register (r1: arm_reg_t) (r2: arm_reg_t): register_t = ARMDoubleRegister (r1, r2) +let register_to_arm_double_register (r: register_t): (arm_reg_t * arm_reg_t) option = + match r with + | ARMDoubleRegister (a1, a2) -> Some (a1, a2) + | _ -> None + + let register_of_arm_special_register (r: arm_special_reg_t): register_t = ARMSpecialRegister r diff --git a/CodeHawk/CHB/bchlib/bCHCPURegisters.mli b/CodeHawk/CHB/bchlib/bCHCPURegisters.mli index c205c72cc..904e09ca9 100644 --- a/CodeHawk/CHB/bchlib/bCHCPURegisters.mli +++ b/CodeHawk/CHB/bchlib/bCHCPURegisters.mli @@ -81,9 +81,15 @@ val register_of_mips_floating_point_register_index: int -> register_t (** Converts a regular ARM register to a generic register.*) val register_of_arm_register: arm_reg_t -> register_t +(** Converts a generic register to a regular ARM register if possible.*) +val register_to_arm_register: register_t -> arm_reg_t option + (** Converts a combination of two ARM registers to a generic register.*) val register_of_arm_double_register: arm_reg_t -> arm_reg_t -> register_t +(** Converts a generic register to a combination of ARM registers, if possible.*) +val register_to_arm_double_register: register_t -> (arm_reg_t * arm_reg_t) option + (** Converts an ARM special register to a generic register.*) val register_of_arm_special_register: arm_special_reg_t -> register_t diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 2dec08c77..5a633543e 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -3527,6 +3527,12 @@ object (self) XVar (self#env#mk_symbolic_value rhs) else rhs in + let _ = + log_diagnostics_result + ~tag:"get_assign_commands_r" + ~msg:self#cia + __FILE__ __LINE__ + ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s 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 @@ -3671,10 +3677,57 @@ object (self) let assigns = [ASSIGN_NUM (regvar, rhs_chif)] in (regvar, rhscmds @ assigns) + method private get_doubles_clobbered + (defs: variable_t list) + (defdoubles: variable_t list): variable_t list = + let is_covered (r: register_t) = + if system_settings#is_arm then + match r with + | ARMRegister a -> + List.exists (fun dd -> + if self#f#env#is_register_variable dd then + let dr = self#f#env#get_register dd in + match TR.tget_ok dr with + | ARMDoubleRegister (a1, a2) -> a = a1 || a = a2 + | _ -> false + else + false) defdoubles + | _ -> false + else + false in + let get_active (r: register_t) = + if system_settings#is_arm then + match r with + | ARMRegister a -> + List.fold_left (fun acc (r1, r2) -> + match (r1, r2) with + | (ARMRegister a1, ARMRegister a2) -> + if a = a1 || a = a2 then + (self#f#env#mk_arm_double_register_variable a1 a2) :: acc + else + acc + | _ -> acc) [] self#f#active_register_pairs + | _ -> [] + else + [] in + let regdefs = + List.fold_left (fun acc v -> + if self#f#env#is_register_variable v then + (TR.tget_ok (self#f#env#get_register v)) :: acc + else + acc) [] defs in + List.fold_left (fun acc r -> + if is_covered r then + acc + else + (get_active r) @ acc) [] regdefs + method get_vardef_commands ?(defs: variable_t list = []) + ?(defdoubles: variable_t list = []) ?(clobbers: variable_t list = []) ?(use: variable_t list = []) + ?(usedoubles: variable_t list = []) ?(usehigh: variable_t list = []) ?(flagdefs: variable_t list = []) (iaddr: string): cmd_t list = @@ -3690,9 +3743,19 @@ object (self) let op = {op_name = opname; op_args = [("dst", symv, WRITE)]} in OPERATION op) vars in let defdoms = ["reachingdefs"; "defuse"; "defusehigh"] in - let defops = mk_ops defdoms def_op_name defs in - let clobberops = mk_ops defdoms clobber_op_name clobbers in - let useops = mk_ops ["defuse"] use_op_name use in + let defops = mk_ops defdoms def_op_name (defs @ defdoubles) in + let doublesclobbered = self#get_doubles_clobbered defs defdoubles in + let _ = + if (List.length doublesclobbered) > 0 then + log_diagnostics_result + ~tag:"get_vardef_commands:doubles clobbered" + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + [String.concat + ", " (List.map (fun v -> p2s v#toPretty) doublesclobbered)] in + let clobberops = + mk_ops defdoms clobber_op_name (clobbers @ doublesclobbered) in + let useops = mk_ops ["defuse"] use_op_name (use @ usedoubles) in let usehighops = mk_ops ["defusehigh"] usehigh_op_name usehigh in let flagdefops = mk_ops ["flagreachingdefs"] flagdef_op_name flagdefs in let _ = List.iter (fun v -> self#f#add_use_loc v iaddr) use in @@ -4377,7 +4440,7 @@ object (self) ABSTRACT_VARS (v1::abstrRegs)] @ [returnassign] - method get_arm_call_commands = + method get_arm_call_commands (returnpieces: (register_t * xpr_t) list): cmd_t list = let parargs = self#get_call_arguments in let ctinfo = self#get_call_target in let termev = new arm_bterm_evaluator_t self#f parargs in @@ -4385,15 +4448,20 @@ object (self) let semrecorder = mk_callsemantics_recorder self#l self#f termev xprxt ctinfo in let _ = semrecorder#record_callsemantics in - let r0 = self#env#mk_arm_register_variable AR0 in let opname = new symbol_t ~atts:["CALL"] ctinfo#get_name in - let returnassign = - let rvar = self#env#mk_return_value self#cia in - let _ = - if ctinfo#is_signature_valid then - let name = ctinfo#get_name ^ "_rtn_" ^ self#cia in - self#env#set_variable_name rvar name in - ASSIGN_NUM (r0, NUM_VAR rvar) in + let returnassigns = + List.concat + (List.map (fun (reg, rhs) -> + let lhs = self#f#env#mk_register_variable reg in + let _ = + log_diagnostics_result + ~tag:"get_arm_call_commands:return-assign" + ~msg:self#cia + __FILE__ __LINE__ + ["calltarget: " ^ ctinfo#get_name; + "lhs: " ^ (p2s lhs#toPretty); + "rhs: " ^ (x2s rhs)] in + self#get_assign_commands_r (Ok lhs) (Ok rhs)) returnpieces) in let bridgeVars = self#env#get_bridge_values_at self#cia in let abstractglobals = let globals = @@ -4418,7 +4486,7 @@ object (self) @ (match abstrRegs with | [] -> [] | _ -> [ABSTRACT_VARS abstrRegs]) - @ [returnassign] + @ returnassigns @ sideeffect_assigns @ abstractglobals @ (match bridgeVars with diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index cfb4aa245..78a5aacc3 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -1701,6 +1701,7 @@ object (self) val proofobligations = mk_proofobligations faddr (mk_xpodictionary varmgr#vard#xd) val mutable returnlocations = [] + val mutable active_register_pairs: (register_t * register_t) list = [] (* ------------------------------------------------------------------------- *) @@ -1728,6 +1729,18 @@ object (self) method set_instruction_bytes (ia:ctxt_iaddress_t) (b:string) = H.add instrbytes ia b + method set_active_register_pairs (l: (register_t * register_t) list) = + active_register_pairs <- + List.fold_left (fun acc (r1, r2) -> + if List.exists (fun (r1', r2') -> + ((register_compare r1 r1') = 0) && ((register_compare r2 r2') = 0)) + acc then + acc + else + (r1, r2) :: acc) [] l + + method active_register_pairs = active_register_pairs + method get_instruction_bytes (ia:ctxt_iaddress_t) = if H.mem instrbytes ia then H.find instrbytes ia @@ -2564,6 +2577,16 @@ object (self) make_function_summary ~fintf ~sem ~doc:default_function_documentation in appsummary <- summary + method private write_xml_active_register_pairs (node: xml_element_int) = + node#appendChildren + (List.map (fun (r1, r2) -> + let n = xmlElement "rp" in + begin + n#setAttribute "r1" (register_to_string r1); + n#setAttribute "r2" (register_to_string r2); + n + end) active_register_pairs) + method write_xml (node:xml_element_int) = let append = node#appendChildren in let sumNode = xmlElement "summary" in @@ -2579,6 +2602,7 @@ object (self) let srNode = xmlElement "saved-registers" in let sfNode = xmlElement "stackframe" in let espNode = xmlElement "stack-adjustment" in + let regpairsNode = xmlElement "active-register-pairs" in begin self#write_xml_app_summary sumNode; self#write_xml_constants cNode; @@ -2591,6 +2615,7 @@ object (self) self#write_xml_base_pointers bpNode; self#write_xml_variable_names vvNode; self#write_xml_saved_registers srNode; + self#write_xml_active_register_pairs regpairsNode; self#stackframe#write_xml sfNode; (match stack_adjustment with | Some i -> espNode#setIntAttribute "adj" i | _ -> ()); @@ -2607,7 +2632,8 @@ object (self) vvNode; srNode; sfNode; - espNode] + espNode; + regpairsNode] end method read_xml (node:xml_element_int) = diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml index 33ff13391..06a1df86f 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInterface.ml @@ -1252,7 +1252,7 @@ let mips_params (funargs: bfunarg_t list): fts_parameter_t list = (* Note: CIL attaches some attributes to the TFun type and some attributes to the varinfo representing the function definition. In particular, the 'format' attribute is attached to the TFun type, but any codehawk-specific name (e.g., - chk_format would be attached to the varinfo. + chk_format would be attached to the varinfo. Given that the current api expects it to be attached to the TFun, only the format form can be used to indicate that an argument is a format string.*) diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index e0e80daa4..e58847de4 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1401,6 +1401,7 @@ class type system_settings_int = object (* setters *) method set_architecture: string -> unit + method set_float_abi: string -> unit method set_fileformat: string -> unit method set_summary_jar: string -> unit method add_so_library: string -> unit (* name of so-library *) @@ -1445,6 +1446,8 @@ object method is_x86: bool method is_elf: bool method is_pe: bool + method is_hard_float: bool + method is_soft_float: bool method is_verbose: bool method is_typing_rule_enabled: string -> bool method is_debug_excluded: bool @@ -1770,6 +1773,7 @@ class type var_invariant_int = method get_fact: var_invariant_fact_t method get_variable: variable_t method get_reaching_defs: symbol_t list + method get_clobber_rdefs: string list method get_def_uses: symbol_t list (* predicates *) @@ -5306,10 +5310,10 @@ class type function_environment_int = numerical value. *) method has_constant_offset: variable_t -> bool - method add_memory_offset: variable_t -> memory_offset_t -> variable_t traceresult + (** {2 Register variables} *) (** Returns [true] if [var] is a register variable (of any architecture). *) @@ -5894,6 +5898,12 @@ object (** Declares that this function is non-returning.*) method set_nonreturning: unit + (** Registers a set of register pairs that are being tracked in combination + and must be killed in propagation if part of them gets modified.*) + method set_active_register_pairs: (register_t * register_t) list -> unit + + method active_register_pairs: (register_t * register_t) list + (* method set_dynlib_stub: call_target_t -> unit *) @@ -6661,7 +6671,7 @@ class type floc_int = method get_mips_syscall_commands: cmd_t list (** returns the CHIF code associated with the call instruction (arm) *) - method get_arm_call_commands: cmd_t list + method get_arm_call_commands: (register_t * xpr_t) list -> cmd_t list (** returns the CHIF code associated with the call instruction (power32) *) method get_pwr_call_commands: cmd_t list @@ -6760,8 +6770,10 @@ class type floc_int = (* returns the CHIF code to set definition/use instruction addresses *) method get_vardef_commands: ?defs:variable_t list + -> ?defdoubles:variable_t list -> ?clobbers:variable_t list -> ?use:variable_t list + -> ?usedoubles:variable_t list -> ?usehigh:variable_t list -> ?flagdefs:variable_t list -> string @@ -6882,6 +6894,8 @@ object method set_thread_start_address : doubleword_int -> ctxt_iaddress_t -> doubleword_int -> bterm_t list -> unit (* creation faddr, iaddr, function start addr, arguments *) + method set_double_rdef_location: + string -> register_t -> register_t -> string -> unit method add_inlined_function: doubleword_int -> unit method add_exported_item_name: doubleword_int -> string -> unit @@ -6978,6 +6992,9 @@ object switches from arm to thumb at address [addr], or None otherwise.*) method get_arm_thumb_switch: doubleword_int -> string option + method get_aggregate: doubleword_int -> string list option + method get_instruction_annotation: doubleword_int -> string list option + method get_argument_constraints: (* name, offset, lower bound, upper bound *) string -> (string * int option * int option * int option) list @@ -7005,6 +7022,7 @@ object method has_exported_item_name: doubleword_int -> bool method has_exported_data_spec: string -> bool method has_data_block: doubleword_int -> bool + method has_double_rdef_location: string -> bool method has_jumptable: doubleword_int -> bool method has_bound_library_function: doubleword_int -> bool method is_locked_instruction: doubleword_int -> bool diff --git a/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml b/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml index 7c72b8514..689a5239b 100644 --- a/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml +++ b/CodeHawk/CHB/bchlib/bCHLocationVarInvariant.ml @@ -112,6 +112,13 @@ object (self: 'a) | ReachingDef (_, sl) -> sl | _ -> [] + method get_clobber_rdefs: string list = + List.fold_left (fun acc s -> + if List.mem "clobber" s#getAttributes then + s#getBaseName :: acc + else + acc) [] self#get_reaching_defs + method get_def_uses: symbol_t list = match fact with | DefUse (_, sl) -> sl diff --git a/CodeHawk/CHB/bchlib/bCHSystemInfo.ml b/CodeHawk/CHB/bchlib/bCHSystemInfo.ml index 3114d7602..f8bd9c193 100644 --- a/CodeHawk/CHB/bchlib/bCHSystemInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHSystemInfo.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -60,6 +60,7 @@ open BCHBCTypeXml open BCHByteUtilities open BCHCallbackTables open BCHCppClass +open BCHCPURegisters open BCHCStruct open BCHCStructConstant open BCHDataBlock @@ -98,6 +99,7 @@ module DataBlockCollections = CHCollections.Make ( end) let file_as_string = ref "" +let bd = BCHDictionary.bdictionary let id = BCHInterfaceDictionary.interface_dictionary @@ -142,6 +144,15 @@ object (self) (* fa,ia of jmp* instr -> (base address,lb option, ub option) *) val jumptabletargets = H.create 13 + (* anchor -> [name] *) + val aggregates = H.create 3 + + (* iaddr -> [kind] *) + val instruction_annotations = H.create 3 + + (* def-addr -> [(lo-reg, hi-reg, use-addr)] *) + val double_rdef_locations = H.create 3 + val indirect_jump_targets = H.create 13 (* fa,ia -> target list *) val nonreturning_calls = new DoublewordCollections.table_t @@ -269,6 +280,49 @@ object (self) end | _ -> () + method get_aggregate (anchor: doubleword_int): string list option = + if H.mem aggregates anchor#index then + Some (H.find aggregates anchor#index) + else + None + + method set_double_rdef_location + (use_addr: string) + (reglo: register_t) + (reghi: register_t) + (def_addr: string) = + let entry = + if H.mem double_rdef_locations def_addr then + H.find double_rdef_locations def_addr + else + [] in + let entry = + if List.exists (fun (lo, hi, use) -> + (register_compare lo reglo) = 0 + && (register_compare hi reghi) = 0 + && use = use_addr) entry then + entry + else + let _ = + log_diagnostics_result + ~tag:"set_double_rdef_location" + ~msg:use_addr + __FILE__ __LINE__ + ["reglo: " ^ (register_to_string reglo); + "reghi: " ^ (register_to_string reghi); + "def_addr: " ^ def_addr] in + (reglo, reghi, use_addr) :: entry in + H.replace double_rdef_locations def_addr entry + + method has_double_rdef_location (def_addr: string) = + H.mem double_rdef_locations def_addr + + method get_instruction_annotation (iaddr: doubleword_int): string list option = + if H.mem instruction_annotations iaddr#index then + Some (H.find instruction_annotations iaddr#index) + else + None + method get_initialized_memory_strings = H.fold (fun k v a -> @@ -779,6 +833,12 @@ object (self) self#read_xml_jump_table_targets jnode end); + (if hasc "aggregates" then + self#read_xml_aggregates (getc "aggregates")); + + (if hasc "instruction-annotations" then + self#read_xml_instruction_annotations (getc "instruction-annotations")); + (if hasc "indirect-jumps" then self#read_xml_indirect_jumps (getc "indirect-jumps")); @@ -898,6 +958,24 @@ object (self) (getc "enable") end + method private read_xml_aggregates (node: xml_element_int) = + let getc = node#getTaggedChildren in + List.iter (fun n -> + let geta tag = geta_fail "read_xml_aggregates" n tag in + let anchor = geta "anchor" in + let name = n#getAttribute "name" in + H.add aggregates anchor#index [name]) + (getc "agg") + + method private read_xml_instruction_annotations (node: xml_element_int) = + let getc = node#getTaggedChildren in + List.iter (fun n -> + let geta tag = geta_fail "read_xml_instruction_annotations" n tag in + let iaddr = geta "iaddr" in + let kind = n#getAttribute "kind" in + H.add instruction_annotations iaddr#index [kind]) + (getc "iann") + method private read_xml_indirect_jumps (node:xml_element_int) = let getc = node#getTaggedChildren in List.iter (fun n -> @@ -1528,6 +1606,8 @@ object (self) self#read_xml_goto_returns (getc "goto-returns")); (if hasc "so-imports" then self#read_xml_so_imports (getc "so-imports")); + (if hasc "double-rdef-locations" then + self#read_xml_double_rdef_locations (getc "double-rdef-locations")) end method get_userdeclared_codesections = userdeclared_codesections#listOfKeys @@ -2094,6 +2174,43 @@ object (self) readset (getc "missing-summaries") missing_so_summaries) end + method private write_xml_double_rdef_locations (node: xml_element_int) = + let rdefs = H.fold (fun k v a -> (k, v) :: a) double_rdef_locations [] in + node#appendChildren + (List.map (fun (rdefaddr, uselocs) -> + let knode = xmlElement "rdef-addr" in + begin + knode#setAttribute "rdef" rdefaddr; + knode#appendChildren + (List.map (fun (lo, hi, use_addr) -> + let unode = xmlElement "use" in + begin + bd#write_xml_register ~tag:"ireglo" unode lo; + bd#write_xml_register ~tag:"ireghi" unode hi; + unode#setAttribute "use" use_addr; + unode + end) uselocs); + knode + end) rdefs); + + method private read_xml_double_rdef_locations (node: xml_element_int) = + begin + List.iter (fun rdefNode -> + let rdefaddr = rdefNode#getAttribute "rdef" in + let locs = + List.map (fun unode -> + let lo = bd#read_xml_register ~tag:"ireglo" unode in + let hi = bd#read_xml_register ~tag:"ireghi" unode in + let useaddr = unode#getAttribute "use" in + (lo, hi, useaddr)) (rdefNode#getTaggedChildren "use") in + H.add double_rdef_locations rdefaddr locs) + (node#getTaggedChildren "rdef-addr"); + log_diagnostics_result + ~tag:"read_xml_double_rdef_locations" + __FILE__ __LINE__ + ["number of rdefs read: " ^ (string_of_int (H.length double_rdef_locations))] + end + method write_xml (node: xml_element_int) = let append = node#appendChildren in let fNode = xmlElement "functions-data" in @@ -2106,6 +2223,7 @@ object (self) let cbNode = xmlElement "call-back-tables" in let stNode = xmlElement "struct-tables" in let soNode = xmlElement "so-imports" in + let rdefNode = xmlElement "double-rdef-locations" in begin functions_data#write_xml fNode; self#write_xml_data_blocks dNode; @@ -2115,11 +2233,12 @@ object (self) self#write_xml_goto_returns gNode; self#write_xml_call_back_tables cbNode; self#write_xml_struct_tables stNode; + self#write_xml_double_rdef_locations rdefNode; string_table#write_xml sNode; self#write_xml_so_imports soNode; append [ fNode; lNode; dNode; jNode; sNode; tNode; gNode; cbNode; stNode; - soNode] + soNode; rdefNode] end end diff --git a/CodeHawk/CHB/bchlib/bCHSystemSettings.ml b/CodeHawk/CHB/bchlib/bCHSystemSettings.ml index e589c3c81..a206e1a88 100644 --- a/CodeHawk/CHB/bchlib/bCHSystemSettings.ml +++ b/CodeHawk/CHB/bchlib/bCHSystemSettings.ml @@ -160,6 +160,7 @@ object (self) val mutable lineq_instr_cutoff = 0 val mutable lineq_block_cutoff = 0 val mutable thumb = false + val mutable float_abi = None val mutable arm_extension_registers = false val mutable jni_enabled = false val mutable set_vftables_enabled = false @@ -198,6 +199,16 @@ object (self) (BCH_failure (LBLOCK [STR "Architecture "; STR name; STR " not recognized"])) + method set_float_abi (name: string) = + let _ = log_result~tag:"set_float_abi"__FILE__ __LINE__ [name] in + float_abi <- Some name + + method is_hard_float = + match float_abi with Some s -> s = "hardfloat" | _ -> true + + method is_soft_float = + match float_abi with Some s -> s = "softfloat" | _ -> false + method set_fileformat (name: string) = if List.mem name ["elf"; "pe"] then fileformat <- name diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 83785866c..6239d2c5e 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_20260703" - ~date:"2026-07-03" + ~version:"0.6.0_20260802" + ~date:"2026-0802" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunction.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunction.ml index 048d78fbf..d3be3118a 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunction.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyFunction.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2024 Aarno Labs, LLC + Copyright (c) 2021-2026 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 @@ -34,6 +34,7 @@ open CHLogger (* bchlib *) open BCHBasicTypes open BCHByteUtilities +open BCHCPURegisters open BCHLibTypes open BCHLocation @@ -43,6 +44,13 @@ open BCHARMAssemblyInstructions open BCHARMTypes module H = Hashtbl +module TR = CHTraceResult + +let id = BCHInterfaceDictionary.interface_dictionary + + +let armreg_compare r1 r2 = + Stdlib.compare (armreg_to_string r1) (armreg_to_string r2) class arm_assembly_function_t @@ -137,6 +145,73 @@ object (self) | _ -> ()) in !result + method private get_callee_signatures: function_signature_t list = + let finfo = BCHFunctionInfo.get_function_info self#get_address in + let sigindices = ref [] in + let sigs = ref [] in + begin + self#iteri (fun _ ctxtiaddr instr -> + match instr#get_opcode with + | BranchLink _ + | BranchLinkExchange _ + | Branch _ + | BranchExchange _ -> + if finfo#has_call_target ctxtiaddr + && (not (finfo#get_call_target ctxtiaddr)#is_unknown) then + let ctinfo = finfo#get_call_target ctxtiaddr in + let xsig = ctinfo#get_signature in + let sigindex = id#index_function_signature xsig in + if List.mem sigindex !sigindices then + () + else + begin + sigindices := sigindex :: !sigindices; + sigs := xsig :: !sigs + end + | _ -> ()); + !sigs + end + + method lo_hi_registers_defined: arm_lo_hi_register_pair_t list = + let result = ref [] in + let add (lo, hi) = + if List.exists (fun (lo', hi') -> + (armreg_compare lo lo') = 0 && (armreg_compare hi hi') = 0) + !result then + () + else + result := (lo, hi) :: !result in + begin + self#iteri (fun _ _ instr -> List.iter add instr#lo_hi_registers_defined); + List.iter (fun xsig -> + if BCHBCTypeUtil.is_wide_type xsig.fts_returntype then + add (AR0, AR1)) self#get_callee_signatures; + !result + end + + method lo_hi_registers_used: arm_lo_hi_register_pair_t list = + let result = ref [] in + let add (lo, hi) = + if List.exists (fun (lo', hi') -> + (armreg_compare lo lo') = 0 && (armreg_compare hi hi') = 0) + !result then + () + else + result := (lo, hi) :: !result in + begin + self#iteri (fun _ _ instr -> List.iter add instr#lo_hi_registers_used); + List.iter (fun xsig -> + List.iter (fun p -> + if BCHFtsParameter.is_register_parameter p then + let regarg = + TR.tget_ok (BCHFtsParameter.get_register_parameter_register p) in + match regarg with + | ARMDoubleRegister (ar1, ar2) -> + add (ar1, ar2) + | _ -> ()) xsig.fts_parameters) self#get_callee_signatures; + !result + end + method iter (f:arm_assembly_block_int -> unit) = List.iter (fun b -> f b) self#get_blocks diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml index 1ca00f2bd..4149b90ae 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2025 Aarno Labs, LLC + Copyright (c) 2021-2026 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 @@ -37,6 +37,7 @@ open BCHBasicTypes open BCHByteUtilities open BCHFunctionData open BCHLibTypes +open BCHSystemInfo (* bchlibarm32 *) open BCHARMDictionary @@ -59,6 +60,8 @@ object (self) val mutable aggregate_anchor = false val mutable blockcondition = false val mutable conditioncoveredby = None (* refers to IT instruction *) + val mutable lo_hi_registers_defined = [] + val mutable lo_hi_registers_used = [] method set_block_entry = block_entry <- true @@ -87,6 +90,47 @@ object (self) method is_in_aggregate = in_aggregate + method set_lo_hi_registers_defined l = lo_hi_registers_defined <- l + + method set_lo_hi_registers_used l = lo_hi_registers_used <- l + + method is_wide_op_instruction = + match system_info#get_instruction_annotation vaddr with + | Some ["wop"] -> true + | _ -> + match self#get_opcode with + | LoadRegisterDual _ -> system_info#has_double_rdef_location vaddr#to_hex_string + | _ -> false + + method lo_hi_registers_defined = + if self#is_aggregate_anchor then + lo_hi_registers_defined + else + match self#get_opcode with + | SignedMultiplyAccumulateLong (_, _, rdlo, rdhi, _, _) (* SMLAL *) + | SignedMultiplyLong (_, _, rdlo, rdhi, _, _) (* SMULL *) + | UnsignedMultiplyAccumulateLong (_, _, rdlo, rdhi, _, _) (* UMLAL *) + | UnsignedMultiplyLong (_, _, rdlo, rdhi, _, _) -> (* UMULL *) + [(rdlo#get_register, rdhi#get_register)] + | LoadRegisterDual (_, rdlo, rdhi, _, _, _, _) + when self#is_wide_op_instruction -> + [(rdlo#get_register, rdhi#get_register)] + | _ -> [] + + method lo_hi_registers_used = + if self#is_aggregate_anchor then + lo_hi_registers_used + else + match self#get_opcode with + | SignedMultiplyAccumulateLong (_, _, rdlo, rdhi, _, _) (* SMLAL *) + | UnsignedMultiplyAccumulateLong (_, _, rdlo, rdhi, _, _) -> (* UMLAL *) + [(rdlo#get_register, rdhi#get_register)] + | StoreRegisterDual (_, rdlo, rdhi, _, _, _, _) + when self#is_wide_op_instruction -> + [(rdlo#get_register, rdhi#get_register)] + | _ -> + [] + method has_opcode_condition = BCHARMOpcodeRecords.is_opcode_conditional opcode diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml index ab8846075..10422855c 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml @@ -349,6 +349,14 @@ object (self) agg#entry#set_aggregate_entry; agg#exitinstr#set_aggregate_exit; List.iter (fun instr -> instr#set_in_aggregate va) agg#instrs; + (if agg#is_arm_wide_operation then + let instr = agg#anchor in + begin + instr#set_lo_hi_registers_defined + agg#wide_op_sequence#lo_hi_register_pairs_defined; + instr#set_lo_hi_registers_used + agg#wide_op_sequence#lo_hi_register_pairs_used + end); (match agg#kind with | ARMJumptable jt -> self#set_jumptable jt#to_jumptable | _ -> ()) diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml index 4405ae861..e348cb6cf 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml @@ -201,6 +201,9 @@ let cc_expr | (Add (true, ACCAlways, _, x, y, _), ACCNotEqual) -> (XOp (XNe, [XOp (XPlus, [v x; v y]); zero_constant_expr]), [x; y]) + | (Add (true, ACCAlways, _, x, y, _), ACCCarrySet) -> + (XOp (XGe, [XOp (XPlus, [vu x; vu y]); max32_constant_expr]), [x; y]) + (* -------------------------------------------------------------- And --- *) | (BitwiseAnd (true, ACCAlways, _, x, y, _), ACCEqual) -> @@ -209,6 +212,16 @@ let cc_expr | (BitwiseAnd (true, ACCAlways, _, x, y, _), ACCNotEqual) -> (XOp (XNe, [XOp (XBAnd, [vu x; vu y]); zero_constant_expr]), [x; y]) + (* --------------------------------------------------------------- Or --- *) + + | (BitwiseOr (true, ACCAlways, _, x, y, _), ACCEqual) -> + (XOp (XLAnd, [XOp (XEq, [v x; zero_constant_expr]); + XOp (XEq, [v y; zero_constant_expr])]), [x; y]) + + | (BitwiseOr (true, ACCAlways, _, x, y, _), ACCNotEqual) -> + (XOp (XLOr, [XOp (XNe, [v x; zero_constant_expr]); + XOp (XNe, [v y; zero_constant_expr])]), [x; y]) + (* ---------------------------------------------------------- Compare --- *) | (Compare (_, x, y, _), ACCEqual) -> @@ -346,9 +359,18 @@ let cc_expr (* ------------------------------------------------- Reverse Subtract --- *) + | (ReverseSubtract (true, ACCAlways, _, x, y, _), ACCEqual) -> + (XOp (XEq, [XOp (XMinus, [v y; v x]); zero_constant_expr]), [x; y]) + | (ReverseSubtract (true, ACCAlways, _, x, y, _), ACCNonNegative) -> (XOp (XGe, [XOp (XMinus, [v y; v x]); zero_constant_expr]), [x; y]) + | (ReverseSubtract (true, ACCAlways, _, x, y, _), ACCCarryClear) -> + (XOp (XLt, [XOp (XMinus, [vu y; vu x]); zero_constant_expr]), [x; y]) + + | (ReverseSubtract (true, ACCAlways, _, x, y, _), ACCCarrySet) -> + (XOp (XGe, [XOp (XMinus, [vu y; vu x]); zero_constant_expr]), [x; y]) + (* --------------------------------------------------------- Subtract --- *) | (Subtract (true, ACCAlways, _, x, y, _, _), ACCEqual) -> @@ -424,7 +446,13 @@ let arm_conditional_expr match get_arm_opcode_condition condopc with | Some c when is_cond_conditional c -> cc_expr v vu testfloc testopc c - | _ -> (false, None, []) in + | _ -> + match condopc with + | SubtractCarry _ + | AddCarry _ + | ReverseSubtractCarry _ -> + cc_expr v vu testfloc testopc ACCCarrySet + | _ -> (false, None, []) in if found then match optxpr with diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml index b7c1deb16..e7844d56c 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2022-2025 Aarno Labs, LLC + Copyright (c) 2022-2026 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 @@ -43,6 +43,7 @@ open BCHARMAssemblyInstructions open BCHARMDisassemblyUtils open BCHARMJumptable open BCHARMTypes +open BCHARMWideOpSequence open BCHDisassembleARMInstruction open BCHLoadStoreMultipleSequence open BCHThumbITSequence @@ -53,6 +54,18 @@ module TR = CHTraceResult let p2s = CHPrettyUtil.pretty_to_string +let arm_wide_op_kind_to_string (wopkind: arm_wide_op_kind_t): string = + match wopkind with + | WideAdd -> "wide-add" + | WideSubtract -> "wide-subtract" + | WideReverseSubtract -> "wide-reverse-subtract" + | WideMove -> "wide-move" + | WideMoveNot -> "wide-move-not" + | WideAnd -> "wide-and" + | WideOr -> "wide-or" + | WideXOr -> "wide-xor" + + let arm_aggregate_kind_to_string (k: arm_aggregate_kind_t) = match k with | ARMJumptable jt -> @@ -75,6 +88,8 @@ let arm_aggregate_kind_to_string (k: arm_aggregate_kind_t) = ^ op1#toString ^ " : " ^ op2#toString + | ARMWideOp (wopkind, wop) -> + (arm_wide_op_kind_to_string wopkind) ^ " " ^ wop#toString | BXCall (_, i2) -> "BXCall at " ^ i2#get_address#to_hex_string @@ -114,6 +129,11 @@ object (self) | LDMSTMSequence s -> s | _ -> raise (BCH_failure (STR "Not an ldm-stm sequence")) + method wide_op_sequence = + match self#kind with + | ARMWideOp (_, s) -> s + | _ -> raise (BCH_failure (STR "Not a wide-op sequence")) + method is_jumptable = match self#kind with | ARMJumptable _ -> true @@ -154,6 +174,51 @@ object (self) | ARMTernaryAssignment _ -> true | _ -> false + method is_arm_wide_operation = + match self#kind with + | ARMWideOp _ -> true + | _ -> false + + method is_arm_wide_add = + match self#kind with + | ARMWideOp (WideAdd, _) -> true + | _ -> false + + method is_arm_wide_subtract = + match self#kind with + | ARMWideOp (WideSubtract, _) -> true + | _ -> false + + method is_arm_wide_reverse_subtract = + match self#kind with + | ARMWideOp (WideReverseSubtract, _) -> true + | _ -> false + + method is_arm_wide_move = + match self#kind with + | ARMWideOp (WideMove, _) -> true + | _ -> false + + method is_arm_wide_move_not = + match self#kind with + | ARMWideOp (WideMoveNot, _) -> true + | _ -> false + + method is_arm_wide_and = + match self#kind with + | ARMWideOp (WideAnd, _) -> true + | _ -> false + + method is_arm_wide_or = + match self#kind with + | ARMWideOp (WideOr, _) -> true + | _ -> false + + method is_arm_wide_xor = + match self#kind with + | ARMWideOp (WideXOr, _) -> true + | _ -> false + method write_xml (_node: xml_element_int) = () method toCHIF (_faddr: doubleword_int) = [] @@ -224,6 +289,19 @@ let make_ldm_stm_sequence_aggregate ~anchor:(List.hd (List.tl ldmstmseq#instrs)) +let make_arm_wide_op_sequence_aggregate + (wopkind: arm_wide_op_kind_t) + (wop: arm_wide_op_sequence_int): arm_instruction_aggregate_int = + let anchor = List.hd (List.tl wop#instrs) in + let kind = ARMWideOp (wopkind, wop) in + make_arm_instruction_aggregate + ~kind + ~instrs:wop#instrs + ~entry:(List.hd wop#instrs) + ~exitinstr:anchor + ~anchor + + let make_bx_call_aggregate (movinstr: arm_assembly_instruction_int) (bxinstr: arm_assembly_instruction_int): arm_instruction_aggregate_int = @@ -662,4 +740,13 @@ let identify_arm_aggregate | Some (mov1, mov2, dstop, n1, n2) -> Some (make_ternassign_aggregate mov1 mov2 dstop n1 n2) | _ -> None in + let result = + match result with + | Some _ -> result + | _ -> + match create_arm_wide_op_sequence ch instr with + | Some (wopkind, wop) -> + Some (make_arm_wide_op_sequence_aggregate wopkind wop) + | _ -> None in + result diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml index eea9de069..401c7e43b 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml @@ -115,6 +115,7 @@ type 'a opcode_record_t = { operands: arm_operand_int list; ccode: arm_opcode_cc_t option; flags_set: arm_cc_flag_t list; + flags_used: arm_cc_flag_t list; ida_asm: 'a opcode_formatter_int -> 'a } @@ -125,6 +126,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "ADD"; operands = [rd;rn;rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C; APSR_V] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s "ADD" c [rd; rn; rm]) } @@ -132,6 +134,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "ADC"; operands = [rd;rn;rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C; APSR_V] else []; + flags_used = [APSR_C]; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s "ADC" c [rd; rn; rm]) } @@ -139,6 +142,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "ADR"; operands = [ rd; addr ]; flags_set = []; + flags_used = []; ccode = Some cc; ida_asm = (fun f -> f#opscc "ADR" cc [rd; addr ]) } @@ -146,6 +150,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "AESIMC"; operands = [vd; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "AESIMC" c [vd; vm]) } @@ -153,6 +158,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "AESMC"; operands = [vd; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "AESMC" c [vd; vm]) } @@ -160,6 +166,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "AESD"; operands = [vd; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "AESD" c [vd; vm]) } @@ -167,6 +174,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "AESE"; operands = [vd; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "AESE" c [vd; vm]) } @@ -174,6 +182,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "ASR"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "ASR" ~writeback:s c [rd; rn; rm]) } @@ -182,6 +191,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = { mnemonic = "BFC"; operands = [rd]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~postops "BFC" c [rd]) } @@ -190,6 +200,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = { mnemonic = "BFI"; operands = [rd; rn]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~postops "BFI" c [rd; rn]) } @@ -197,6 +208,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "AND"; operands = [ rd; rn; imm ]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "AND" ~writeback:s c [rd; rn; imm]) } @@ -204,6 +216,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "BIC"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "BIC" c [rd;rn;rm]) } @@ -211,6 +224,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "EOR"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "EOR" c [rd;rn;rm]) } @@ -218,6 +232,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MVN"; operands = [rd; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s "MVN" c [rd;rm]) } @@ -225,6 +240,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "ORR"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s "ORR" c [rd; rn; rm]) } @@ -232,6 +248,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "ORN"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "ORN" ~writeback:s c [rd; rn; rm]) } @@ -239,6 +256,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "B"; operands = [addr]; flags_set = []; + flags_used = []; ccode = Some cc; ida_asm = (fun f -> f#opscc ~thumbw:tw "B" cc [ addr ]) } @@ -246,6 +264,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "BX"; operands = [ addr ]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "BX" c [addr]) } @@ -253,6 +272,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "BL"; operands = [addr]; flags_set = []; + flags_used = []; ccode = Some cc; ida_asm = (fun f -> f#opscc "BL" cc [addr]) } @@ -260,6 +280,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "BLX"; operands = [addr]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "BLX" c [ addr ]) } @@ -267,6 +288,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "BKPT"; operands = [op]; flags_set = []; + flags_used = []; ccode = None; ida_asm = (fun f -> f#ops "BKPT" [op]) } @@ -274,6 +296,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "REV"; operands = [rd; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "REV" c [rd; rm]) } @@ -281,6 +304,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "REV16"; operands = [rd; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "REV16" c [rd; rm]) } @@ -288,6 +312,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "CPS"; operands = []; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> let s_effect = effect#toString in @@ -301,6 +326,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "CMP"; operands = [rn; rm]; flags_set = [APSR_N; APSR_Z; APSR_C; APSR_V]; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "CMP" c [rn; rm]) } @@ -308,6 +334,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "CBNZ"; operands = [op1; op2]; flags_set = []; + flags_used = []; ccode = None; ida_asm = (fun f -> f#ops "CBNZ" [op1; op2]) } @@ -315,6 +342,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "CBZ"; operands = [op1; op2]; flags_set = []; + flags_used = []; ccode = None; ida_asm = (fun f -> f#ops "CBZ" [op1; op2]) } @@ -322,6 +350,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "CMN"; operands = [op1; op2]; flags_set = [APSR_N; APSR_Z; APSR_C; APSR_V]; + flags_used = []; ccode = Some cc; ida_asm = (fun f -> f#opscc "CMN" cc [op1; op2]) } @@ -329,6 +358,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "CLZ"; operands = [rd; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "CLZ" c [rd;rm]) } @@ -336,6 +366,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "DMB"; operands = [option]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "DMB" c [option]) } @@ -344,6 +375,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = { mnemonic = mnemonic; operands = []; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#ops mnemonic []) } @@ -351,6 +383,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "FLDMIAX"; operands = [rn; rl]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "FLDMIAX" c [rn; rl]) } @@ -358,6 +391,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "FSTMIAX"; operands = [rn; rl]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "FSTMIAX" c [rn; rl]) } @@ -374,6 +408,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = mnemonic; operands = [src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~preops mnemonic c [src]); } @@ -381,6 +416,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDMDA"; operands = [rn; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "LDMDA" c [ rn; rl ]) } @@ -388,6 +424,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDMDB"; operands = [rn; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "LDMDB" c [rn; rl]) } @@ -395,6 +432,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDM"; operands = [rn; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "LDM" c [ rn; rl ]) } @@ -402,6 +440,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDMIB"; operands = [rn; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "LDMIB" c [rn; rl]) } @@ -409,6 +448,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDR"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "LDR" c [rt; mem]) } @@ -416,6 +456,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDRB"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "LDRB" c [rt; mem]) } @@ -423,6 +464,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDRD"; operands = [rt; rt2; rn; rm; mem; mem2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "LDRD" c [rt; rt2; mem]) } @@ -430,6 +472,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDREX"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "LDREX" c [rt; mem]) } @@ -437,6 +480,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDRH"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "LDRH" c [rt; mem]) } @@ -444,6 +488,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDRSB"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "LDRSB" c [rt; mem]) } @@ -451,6 +496,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LDRSH"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "LDRSH" c [rt; mem]) } @@ -458,6 +504,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LSL"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s "LSL" c [rd; rn; rm]) } @@ -465,6 +512,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "LSR"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s "LSR" c [rd; rn; rm]) } @@ -474,13 +522,15 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = mnem; operands = [rd; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s mnem c [rd;rm]) - } + } | MoveFromSpecialRegister (c, rd, src, _) -> { mnemonic = "MRS"; operands = [rd; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "MRS" c [rd; src]) } @@ -498,6 +548,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MRC"; operands = [rt]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~preops ~postops "MRC" c [rt]); } @@ -515,6 +566,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MCR"; operands = [rt]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~preops ~postops "MCR" c [rt]); } @@ -522,6 +574,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MOVT"; operands = [rd; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "MOVT" c [rd; imm]) } @@ -529,6 +582,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MSR"; operands = [spr; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "MSR" c [spr; imm]) } @@ -540,6 +594,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MRRC"; operands = [rt; rt2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~preops ~postops "MRRC" c [rt; rt2]) } @@ -547,6 +602,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MUL"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "MUL" c [rd; rn; rm]) } @@ -554,6 +610,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MLA"; operands = [rd; rn; rm; ra]; flags_set = if s then [APSR_N; APSR_Z] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "MLA" c [rd; rn; rm; ra]) } @@ -561,6 +618,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "MLS"; operands = [rd; rn; rm; ra]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "MLS" c [rd; rn; rm; ra]) } @@ -568,6 +626,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "POP"; operands = [sp; rl]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "POP" c [rl]) } @@ -577,6 +636,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = mnemonic; operands = [base; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc mnemonic c [mem]) } @@ -584,6 +644,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "PUSH"; operands = [sp; rl]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "PUSH" c [rl]) } @@ -591,6 +652,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "RBIT"; operands = [rd; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "RBIT" c [rd; rm]) } @@ -598,6 +660,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "RSB"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C; APSR_V] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s "RSB" c [rd; rn; rm]) } @@ -605,6 +668,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "RSC"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C; APSR_V] else []; + flags_used = [APSR_C]; ccode = Some c; ida_asm = (fun f -> f#opscc ~writeback:s "RSC" c [rd; rn; rm]) } @@ -612,6 +676,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "ROR"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "ROR" c [rd; rn; rm]) } @@ -619,6 +684,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "RRX"; operands = [rd; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "RRX" c [rd; rm]) } @@ -626,6 +692,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "QADD"; operands = [rd; rm; rn]; flags_set = [APSR_Q]; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "QADD" c [rd; rm; rn]) } @@ -633,6 +700,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "QDADD"; operands = [rd; rm; rn]; flags_set = [APSR_Q]; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "QDADD" c [rd; rm; rn]) } @@ -640,6 +708,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "QDSUB"; operands = [rd; rm; rn]; flags_set = [APSR_Q]; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "QDSUB" c [rd; rm; rn]) } @@ -647,6 +716,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "QSUB"; operands = [rd; rm; rn]; flags_set = [APSR_Q]; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "QSUB" c [rd; rm; rn]) } @@ -654,6 +724,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SEL"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SEL" c [rd; rn; rm]) } @@ -661,6 +732,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA1H"; operands = [vd; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA1H" c [vd; vm]) } @@ -668,6 +740,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA1C"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA1C" c [vd; vn; vm]) } @@ -675,6 +748,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA1M"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA1M" c [vd; vn; vm]) } @@ -682,6 +756,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA1P"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA1P" c [vd; vn; vm]) } @@ -689,6 +764,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA1SU0"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA1SU0" c [vd; vn; vm]) } @@ -696,6 +772,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA1SU1"; operands = [vd; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA1SU1" c [vd; vm]) } @@ -703,6 +780,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA256H"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA256H" c [vd; vn; vm]) } @@ -710,6 +788,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA256H2"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA256H2" c [vd; vn; vm]) } @@ -717,6 +796,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA256SU0"; operands = [vd; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA256SU0" c [vd; vm]) } @@ -724,6 +804,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SHA256SU1"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "SHA256SU1" c [vd; vn; vm]) } @@ -731,6 +812,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SDIV"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SDIV" c [rd; rn; rm]) } @@ -738,6 +820,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SBFX"; operands = [rd; rn]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SBFX" c [rd; rn]) } @@ -745,6 +828,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SXTB"; operands = [rd; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "SXTB" c [rd; rm]) } @@ -752,6 +836,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SXTH"; operands = [rd; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "SXTH" c [rd; rm]) } @@ -760,6 +845,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = { mnemonic = mnemonic; operands = [rd; rm; rn]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc mnemonic c [rd; rm; rn]) } @@ -768,6 +854,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = { mnemonic = mnemonic; operands = [rd; rm; rn; ra]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc mnemonic c [rd; rm; rn; ra]) } @@ -775,6 +862,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMLABB"; operands = [rd; rn; rm; ra]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMLABB" c [rd; rn; rm; ra]) } @@ -782,6 +870,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMLABT"; operands = [rd; rn; rm; ra]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMLABT" c [rd; rn; rm; ra]) } @@ -789,6 +878,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMLATB"; operands = [rd; rn; rm; ra]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMLATB" c [rd; rn; rm; ra]) } @@ -796,6 +886,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMLATT"; operands = [rd; rn; rm; ra]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMLATT" c [rd; rn; rm; ra]) } @@ -803,6 +894,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMLAL"; operands = [rdlo; rdhi; rn; rm]; flags_set = if s then [APSR_N; APSR_Z] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMLAL" ~writeback:s c [rdlo; rdhi; rn; rm]) } @@ -810,6 +902,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMLAWB"; operands = [rd; rn; rm; ra]; flags_set = [APSR_Q]; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMLAWB" c [rd; rn; rm; ra]) } @@ -817,6 +910,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMLAWT"; operands = [rd; rn; rm; ra]; flags_set = [APSR_Q]; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMLAWT" c [rd; rn; rm; ra]) } @@ -824,6 +918,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMULBB"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMULBB" c [rd; rn; rm]) } @@ -831,6 +926,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMULBT"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMULBT" c [rd; rn; rm]) } @@ -838,6 +934,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMULTB"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMULTB" c [rd; rn; rm]) } @@ -845,6 +942,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMULTT"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMULTT" c [rd; rn; rm]) } @@ -852,6 +950,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMULL"; operands = [rdlo; rdhi; rn; rm]; flags_set = if s then [APSR_N; APSR_Z] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMULL" c [rdlo; rdhi; rn; rm]) } @@ -859,6 +958,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMULWB"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMULWB" c [rd; rn; rm]) } @@ -866,6 +966,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SMULWT"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SMULWT" c [rd; rn; rm]) } @@ -882,6 +983,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = mnemonic; operands = [dst]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~preops mnemonic c [dst]) } @@ -889,6 +991,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STMDA"; operands = [rn; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "STMDA" c [rn; rl]) } @@ -896,6 +999,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STMDB"; operands = [rn; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "STMDB" c [rn; rl]) } @@ -903,6 +1007,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STM"; operands = [rn; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "STM" c [rn; rl]) } @@ -910,6 +1015,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STMIB"; operands = [rn; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "STMIB" c [rn; rl]) } @@ -917,6 +1023,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STR"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "STR" c [rt; mem]) } @@ -924,6 +1031,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STRB"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "STRB" c [rt; mem]) } @@ -931,6 +1039,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STRD"; operands = [rt; rt2; rn; rm; mem; mem2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "STRD" c [rt; rt2; mem]) } @@ -938,6 +1047,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STREX"; operands = [rd; rt; rn; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "STREX" c [rd; rt; mem]) } @@ -945,6 +1055,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "STRH"; operands = [rt; rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "STRH" c [rt; mem]) } @@ -954,13 +1065,15 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = mnemonic; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C; APSR_V] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s mnemonic c [rd; rn; rm]) - } + } | SubtractCarry (s, c, rd, rn, rm, tw) -> { mnemonic = "SBC"; operands = [rd; rn; rm]; flags_set = if s then [APSR_N; APSR_Z; APSR_C; APSR_V] else []; + flags_used = [APSR_C]; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw ~writeback:s "SBC" c [rd; rn; rm]) } @@ -968,6 +1081,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SVC"; operands = [imm]; flags_set = []; + flags_used = []; ccode = Some cc; ida_asm = (fun f -> f#opscc "SVC" cc [ imm ]) } @@ -975,6 +1089,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SWP"; operands = [rt; rt2; rn; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SWP" c [rt; rt2; mem]) } @@ -982,6 +1097,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "SWPB"; operands = [rt; rt2; rn; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "SWPB" c [rt; rt2; mem]) } @@ -989,6 +1105,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "TBB"; operands = [rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "TBB" c [mem]) } @@ -996,6 +1113,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "TBH"; operands = [rn; rm; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "TBH" c [mem]) } @@ -1004,6 +1122,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = operands = [rn; rm]; flags_set = [APSR_N; APSR_Z; APSR_C]; ccode = Some c; + flags_used = []; ida_asm = (fun f -> f#opscc ~thumbw:tw "TST" c [rn; rm]) } | TestEquivalence (c, rn, rm) -> { @@ -1011,12 +1130,14 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = operands = [rn; rm]; flags_set = [APSR_N; APSR_Z; APSR_C]; ccode = Some c; + flags_used = []; ida_asm = (fun f -> f#opscc "TEQ" c [rn; rm]) } | UnsignedAdd8 (c, rd, rn, rm) -> { mnemonic = "UADD8"; operands = [rd; rn; rm]; flags_set = []; (* Note: Armv7 has GE bits for parallel add *) + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "UADD8" c [rd; rn; rm]) } @@ -1024,6 +1145,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UBFX"; operands = [rd; rn]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "UBFX" c [rd; rn]) } @@ -1031,6 +1153,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UDIV"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "UDIV" c [rd; rn; rm]) } @@ -1038,6 +1161,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UXTAB"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "UXTAB" c [rd; rn; rm]) } @@ -1045,6 +1169,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UXTAH"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "UXTAH" c [rd; rn; rm]) } @@ -1052,6 +1177,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UXTB"; operands = [rd; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "UXTB" c [rd; rm]) } @@ -1059,6 +1185,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UXTH"; operands = [rd; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~thumbw:tw "UXTH" c [rd; rm]) } @@ -1066,6 +1193,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UMLAL"; operands = [rdlo; rdhi; rn; rm]; flags_set = if s then [APSR_N; APSR_Z] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~writeback:s "UMLAL" c [rdlo; rdhi; rn; rm]) } @@ -1073,6 +1201,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UMULL"; operands = [rdlo; rdhi; rn; rm]; flags_set = if s then [APSR_N; APSR_Z] else []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~writeback:s "UMULL" c [rdlo; rdhi; rn; rm]) } @@ -1080,6 +1209,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "USAT"; operands = [rd; imm; rn]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "USAT" c [rd; imm; rn]) } @@ -1087,6 +1217,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UQSUB8"; operands = [rd; rn; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "UQSUB8" c [rd; rn; rm]) } @@ -1094,6 +1225,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VABS"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VABS" c [dst; src]) } @@ -1101,6 +1233,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VADD"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VADD" c [dst; src1; src2]) } @@ -1108,6 +1241,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VADDL"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VADDL" c [dst; src1; src2]) } @@ -1115,6 +1249,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VADDW"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VADDW" c [dst; src1; src2]) } @@ -1122,6 +1257,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VAND"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VAND" c [dst; src1; src2]) } @@ -1129,6 +1265,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VBIC"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = match dt with @@ -1139,6 +1276,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VEOR"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VEOR" c [dst; src1; src2]) } @@ -1146,6 +1284,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMVN"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMVN" c [dst; src]) } @@ -1153,6 +1292,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VORR"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VORR" c [dst; src1; src2]) } @@ -1160,6 +1300,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VORN"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VORN" c [vd; vn; vm]) } @@ -1167,6 +1308,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VBSL"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VBSL" c [vd; vn; vm]) } @@ -1179,6 +1321,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = via VMRS *) flags_set = [APSR_N; APSR_Z; APSR_C; APSR_V]; (* flags_set = []; floating point status word not yet supported *) + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt mnemonic c [op1; op2]) } @@ -1188,6 +1331,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = { mnemonic = mnemonic; operands = if fixed then [dst; src; fbits] else [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> @@ -1202,6 +1346,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VDIV"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VDIV" c [dst; src1; src2]) } @@ -1209,6 +1354,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VDUP"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VDUP" c [dst; src]) @@ -1217,6 +1363,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VEXT"; operands = [dst; src1; src2; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VEXT" c [dst; src1; src2; imm]) } @@ -1224,6 +1371,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VFMA"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VFMA" c [dst; src1; src2]) } @@ -1231,6 +1379,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VLD4"; operands = [rl; rn; mem; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VLD4" c [rl; mem]) } @@ -1238,6 +1387,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VLDM"; operands = [rn; rl]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VLDM" c [rn; rl]) } @@ -1245,6 +1395,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VLD1"; operands = [rl; rn; mem; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VLD1" c [rl; mem]) } @@ -1252,6 +1403,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VLDR"; operands = [dst; base; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VLDR" c [dst; mem]) } @@ -1259,6 +1411,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMOV"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMOV" c [dst; src]) } @@ -1266,6 +1419,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMOV"; operands = [dst1; dst2; ddst; src1; src2; ssrc]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMOV" c [dst1; dst2; src1; src2]) } @@ -1273,6 +1427,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMOV"; operands = [dst; src1; src2; ssrc]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMOV" c [dst; src1; src2]) } @@ -1280,6 +1435,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMOV"; operands = [dst1; dst2; ddst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMOV" c [dst1; dst2; src]) } @@ -1287,6 +1443,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMOVL"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMOVL" c [dst; src]) } @@ -1294,6 +1451,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMOVN"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMOVN" c [dst; src]) } @@ -1307,6 +1465,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = { mnemonic = "VMRS"; operands = [dst; src]; flags_set = flags_set; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VMRS" c [dst; src]) } @@ -1314,6 +1473,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMSR"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode =Some c; ida_asm = (fun f -> f#opscc "VMSR" c [dst; src]) } @@ -1321,6 +1481,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMUL"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMUL" c [dst; src1; src2]) } @@ -1328,6 +1489,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMLA"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMLA" c [dst; src1; src2]) } @@ -1335,6 +1497,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMLAL"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMLAL" c [dst; src1; src2]) } @@ -1342,6 +1505,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMULL"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMULL" c [dst; src1; src2]) } @@ -1349,6 +1513,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VMLS"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VMLS" c [dst; src1; src2]) } @@ -1356,6 +1521,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VNEG"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VNEG" c [dst; src]) } @@ -1363,6 +1529,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VNMUL"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VNMUL" c [dst; src1; src2]) } @@ -1370,6 +1537,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VNMLA"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VNMLA" c [dst; src1; src2]) } @@ -1377,6 +1545,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VNMLS"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VNMLS" c [dst; src1; src2]) } @@ -1384,6 +1553,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VPOP"; operands = [sp; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VPOP" c [rl]) } @@ -1391,6 +1561,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VPUSH"; operands = [sp; rl; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VPUSH" c [rl]) } @@ -1398,6 +1569,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VREV64"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VREV64" c [dst; src]) } @@ -1405,6 +1577,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VREV16"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VREV16" c [dst; src]) } @@ -1412,6 +1585,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VREV32"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VREV32" c [dst; src]) } @@ -1419,6 +1593,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VRHADD"; operands = [vd; vn; vm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VRHADD" c [vd; vn; vm]) } @@ -1426,6 +1601,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VRSRA"; operands = [dst; src; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VRSRA" c [dst; src; imm]) } @@ -1433,6 +1609,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSHL"; operands = [dst; src; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VSHL" c [dst; src; src2]) } @@ -1440,6 +1617,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSLI"; operands = [dst; src; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VSLI" c [dst; src; imm]) } @@ -1447,6 +1625,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSHR"; operands = [dst; src; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VSHR" c [dst; src; imm]) } @@ -1454,6 +1633,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSRI"; operands = [dst; src; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VSRI" c [dst; src; imm]) } @@ -1461,6 +1641,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSRA"; operands = [dst; src; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VSRA" c [dst; src; imm]) } @@ -1468,6 +1649,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSHRN"; operands = [dst; src; imm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VSHRN" c [dst; src; imm]) } @@ -1475,6 +1657,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSTR"; operands = [src; base; mem]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VSTR" c [src; mem]) } @@ -1482,6 +1665,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSTMDB"; operands = [rn; rl]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VSTMDB" c [rn; rl]) } @@ -1489,6 +1673,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSTM"; operands = [rn; rl]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "VSTM" c [rn; rl]) } @@ -1496,6 +1681,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VST4"; operands = [rl; rn; mem; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VST4" c [rl; mem]) } @@ -1503,6 +1689,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VST1"; operands = [rl; rn; mem; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VST1" c [rl; mem]) } @@ -1510,6 +1697,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VST2"; operands = [rl; rn; mem; rm]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VST2" c [rl; mem]) } @@ -1517,6 +1705,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VSUB"; operands = [dst; src1; src2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VSUB" c [dst; src1; src2]) } @@ -1524,6 +1713,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VTBL"; operands = [dst; table; index]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VTBL" c [dst; table; index]) } @@ -1531,6 +1721,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VTRN"; operands = [dst; src]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VTRN" c [dst; src]) } @@ -1538,6 +1729,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "VZIP"; operands = [op1; op2]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc ~dt "VZIP" c [op1; op2]) } @@ -1545,6 +1737,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "NOP"; operands = []; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "NOP" c []) } @@ -1552,6 +1745,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UDF"; operands = [op]; flags_set = []; + flags_used = []; ccode = Some c; ida_asm = (fun f -> f#opscc "UDF" c [op]) } @@ -1559,6 +1753,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "invalid"; operands = []; flags_set = []; + flags_used = []; ccode = None; ida_asm = (fun f -> f#no_ops "invalid") } @@ -1566,6 +1761,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UNDEFINED"; operands = []; flags_set = []; + flags_used = []; ccode = None; ida_asm = (fun f -> f#no_ops ("UNDEFINED: " ^ s)) } @@ -1573,6 +1769,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "UNPREDICTABLE"; operands = []; flags_set = []; + flags_used = []; ccode = None; ida_asm = (fun f -> f#no_ops ("UNPREDICTABLE: " ^ s)) } @@ -1580,6 +1777,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t = mnemonic = "unknown"; operands = []; flags_set = []; + flags_used = []; ccode = None; ida_asm = (fun f -> f#no_ops ("unknown " ^ name ^ ": " ^ dw#to_hex_string)) } @@ -1647,9 +1845,12 @@ let get_arm_flags_set (opc: arm_opcode_t): arm_cc_flag_t list = let get_arm_flags_used (opc: arm_opcode_t): arm_cc_flag_t list = - match (get_record opc).ccode with - | Some c -> get_cond_flags_used c - | _ -> [] + let flags_used = (get_record opc).flags_used in + let cc_flags_used = + match (get_record opc).ccode with + | Some c -> get_cond_flags_used c + | _ -> [] in + flags_used @ cc_flags_used let get_arm_opcode_condition (opc: arm_opcode_t): arm_opcode_cc_t option = diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli b/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli index f5382f0ad..46bd0a271 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli +++ b/CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli @@ -118,6 +118,13 @@ type arm_simd_list_element_t = | SIMDRegRepElement of arm_extension_register_replicated_element_t +(** Pair of registers used in wide (64-bit) operations, to represent + a 64-bit storage location, with the low part of the 64-bit value + in the first register and the high part of the 64-bit value in the + second register.*) +type arm_lo_hi_register_pair_t = arm_reg_t * arm_reg_t + + type arm_operand_kind_t = | ARMDMBOption of dmb_option_t | ARMCPSEffect of cps_effect_t @@ -227,6 +234,12 @@ class type arm_operand_int = end +(* Pair of operands that participate in a wide (64-bit) operation, + with the first operand representing the lower 32 bits and the + second operand representing the higher 32 bits. *) +type arm_lo_hi_operand_pair_t = arm_operand_int * arm_operand_int + + (** {1 Assembly opcodes}*) type not_code_t = JumpTable of jumptable_int | DataBlock of data_block_int @@ -1417,6 +1430,8 @@ class type arm_assembly_instruction_int = method set_aggregate_exit: unit method set_aggregate_anchor: unit method set_in_aggregate: doubleword_int -> unit + method set_lo_hi_registers_defined: arm_lo_hi_register_pair_t list -> unit + method set_lo_hi_registers_used: arm_lo_hi_register_pair_t list -> unit (* accessors *) method get_address: doubleword_int @@ -1426,6 +1441,8 @@ class type arm_assembly_instruction_int = method get_non_code_block: not_code_t method get_opcode_condition: arm_opcode_cc_t option method condition_covered_by: doubleword_int + method lo_hi_registers_used: arm_lo_hi_register_pair_t list + method lo_hi_registers_defined: arm_lo_hi_register_pair_t list (* predicates *) method is_arm32: bool @@ -1441,6 +1458,7 @@ class type arm_assembly_instruction_int = method is_aggregate_exit: bool method is_aggregate_anchor: bool method has_opcode_condition: bool + method is_wide_op_instruction: bool (* i/o *) method write_xml: xml_element_int -> unit @@ -1536,6 +1554,33 @@ class type ldm_stm_sequence_int = end +class type arm_wide_op_sequence_int = + object + + method lo_hi_operand_pairs_defined: arm_lo_hi_operand_pair_t list + method lo_hi_operand_pairs_used: arm_lo_hi_operand_pair_t list + + method lo_hi_register_pairs_defined: arm_lo_hi_register_pair_t list + method lo_hi_register_pairs_used: arm_lo_hi_register_pair_t list + + method instrs: arm_assembly_instruction_int list + method anchor: doubleword_int + + method toString: string + method toPretty: pretty_t + end + + +type arm_wide_op_kind_t = + | WideAdd (* ADDS-ADC *) + | WideSubtract (* SUBS-SBC *) + | WideReverseSubtract (* RSBS-RSC *) + | WideMove (* MOV-MOV *) + | WideMoveNot (* MVN-MVN *) + | WideAnd (* AND-AND *) + | WideOr (* ORR-ORR *) + | WideXOr (* EOR-EOR *) + type arm_aggregate_kind_t = | ARMJumptable of arm_jumptable_int | ThumbITSequence of thumb_it_sequence_int @@ -1550,6 +1595,7 @@ type arm_aggregate_kind_t = * arm_assembly_instruction_int | ARMPredicateAssignment of bool * arm_operand_int | ARMTernaryAssignment of arm_operand_int * numerical_t * numerical_t + | ARMWideOp of arm_wide_op_kind_t * arm_wide_op_sequence_int | BXCall of arm_assembly_instruction_int * arm_assembly_instruction_int @@ -1564,6 +1610,7 @@ class type arm_instruction_aggregate_int = method jumptable: arm_jumptable_int method it_sequence: thumb_it_sequence_int method ldm_stm_sequence: ldm_stm_sequence_int + method wide_op_sequence: arm_wide_op_sequence_int (* translation *) method toCHIF: doubleword_int -> cmd_t list @@ -1577,6 +1624,15 @@ class type arm_instruction_aggregate_int = method is_pseudo_ldrsb: bool method is_predicate_assign: bool method is_ternary_assign: bool + method is_arm_wide_operation: bool + method is_arm_wide_add: bool + method is_arm_wide_subtract: bool + method is_arm_wide_reverse_subtract: bool + method is_arm_wide_move: bool + method is_arm_wide_move_not: bool + method is_arm_wide_and: bool + method is_arm_wide_or: bool + method is_arm_wide_xor: bool (* i/o *) method write_xml: xml_element_int -> unit @@ -1850,6 +1906,8 @@ class type arm_assembly_function_int = method get_jumptable_count: int method get_not_valid_instr_count: int method get_true_conditional_return: arm_assembly_block_int option + method lo_hi_registers_used: arm_lo_hi_register_pair_t list + method lo_hi_registers_defined: arm_lo_hi_register_pair_t list (* iterators *) method iter: (arm_assembly_block_int -> unit) -> unit diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMWideOpSequence.ml b/CodeHawk/CHB/bchlibarm32/bCHARMWideOpSequence.ml new file mode 100644 index 000000000..087495818 --- /dev/null +++ b/CodeHawk/CHB/bchlibarm32/bCHARMWideOpSequence.ml @@ -0,0 +1,281 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2026 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 + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* chutil *) +open CHPretty + +(* bchlib *) +open BCHCPURegisters +open BCHLibTypes + +(* bchlibarm32 *) +open BCHARMAssemblyInstructions +open BCHARMTypes + + +module TR = CHTraceResult + + +let p2s = CHPrettyUtil.pretty_to_string + + +let operand_pair_to_string (p: arm_lo_hi_operand_pair_t) = + "(" ^ (p2s (fst p)#toPretty) ^ ", " ^ (p2s (snd p)#toPretty) ^ ")" + + +let register_pair_to_string (p: arm_lo_hi_register_pair_t) = + "(" ^ (armreg_to_string (fst p)) ^", " ^ (armreg_to_string (snd p)) ^ ")" + + +let register_combinations = + ["R0_R1"; "R2_R3"; "R4_R5"; "R6_R7"; "R8_R9"; "R10_R11"] +let rev_register_combinations = + ["R1_R0"; "R3_R2"; "R5_R4"; "R7_R6"; "R9_R8"; "R11_R10"] + +let ordered_register_combination (rd1: arm_operand_int) (rd2: arm_operand_int) = + let s = rd1#toString ^ "_" ^ rd2#toString in + if List.mem s register_combinations then + Some true + else if List.mem s rev_register_combinations then + Some false + else + None + + +let arm_lo_hi_operand_pair_to_string = operand_pair_to_string +let arm_lo_hi_register_pair_to_string = register_pair_to_string + + +let operand_pair_to_register_pair + (p: arm_lo_hi_operand_pair_t): arm_lo_hi_register_pair_t option = + let (lo, hi) = p in + if lo#is_register && hi#is_register then + Some (lo#get_register, hi#get_register) + else + None + + +let is_wide_op (addr: doubleword_int) (tags: string list): bool = + match BCHSystemInfo.system_info#get_aggregate addr with + | Some [aggkind] -> List.mem aggkind tags + | _ -> BCHSystemInfo.system_info#has_double_rdef_location (addr#to_hex_string) + + +class arm_wide_op_sequence_t + (lo_hi_operands_defined: arm_lo_hi_operand_pair_t list) + (lo_hi_operands_used: arm_lo_hi_operand_pair_t list) + (instrs: arm_assembly_instruction_int list) + (anchor: doubleword_int): arm_wide_op_sequence_int = + object (self) + + method lo_hi_operand_pairs_defined = lo_hi_operands_defined + + method lo_hi_operand_pairs_used = lo_hi_operands_used + + method lo_hi_register_pairs_defined = + List.fold_left (fun acc op -> + match operand_pair_to_register_pair op with + | Some p -> p :: acc + | _ -> acc) [] self#lo_hi_operand_pairs_defined + + method lo_hi_register_pairs_used = + List.fold_left (fun acc op -> + match operand_pair_to_register_pair op with + | Some p -> p :: acc + | _ -> acc) [] self#lo_hi_operand_pairs_used + + method instrs = instrs + method anchor = anchor + + method toString = + "wide-op with defs: " + ^ (String.concat + ", " (List.map operand_pair_to_string self#lo_hi_operand_pairs_defined)) + ^ "; used: " + ^ (String.concat + ", " (List.map operand_pair_to_string self#lo_hi_operand_pairs_used)) + + method toPretty = STR self#toString + + end + + +let make_wide_op_sequence + (lo_hi_operands_defined: arm_lo_hi_operand_pair_t list) + (lo_hi_operands_used: arm_lo_hi_operand_pair_t list) + (instrs: arm_assembly_instruction_int list) + (anchor: doubleword_int): arm_wide_op_sequence_int = + new arm_wide_op_sequence_t lo_hi_operands_defined lo_hi_operands_used instrs anchor + + +let create_arm_wide_op_sequence + (_ch: pushback_stream_int) + (anchorinstr: arm_assembly_instruction_int): + (arm_wide_op_kind_t * arm_wide_op_sequence_int) option = + let anchoraddr = anchorinstr#get_address in + match anchorinstr#get_opcode with + | AddCarry (_, ACCAlways, rdhi, rnhi, rmhi, _) -> + let addinstraddr = anchoraddr#add_int (-4) in + (match TR.to_option (get_arm_assembly_instruction addinstraddr) with + | Some addinstr -> + (match addinstr#get_opcode with + | Add (true, ACCAlways, rdlo, rnlo, rmlo, _) -> + let instrs = [addinstr; anchorinstr] in + let opsdefined = [(rdlo, rdhi)] in + let opsused = [(rnlo, rnhi); (rmlo, rmhi)] in + let wop = make_wide_op_sequence opsdefined opsused instrs anchoraddr in + Some (WideAdd, wop) + | _ -> None) + | _ -> None) + | SubtractCarry (_, ACCAlways, rdhi, rnhi, rmhi, _) -> + let subinstraddr = anchoraddr#add_int (-4) in + (match TR.to_option (get_arm_assembly_instruction subinstraddr) with + | Some subinstr -> + (match subinstr#get_opcode with + | Subtract (true, ACCAlways, rdlo, rnlo, rmlo, _, _) -> + let instrs = [subinstr; anchorinstr] in + let opsdefined = [(rdlo, rdhi)] in + let opsused = [(rnlo, rnhi); (rmlo, rmhi)] in + let wop = make_wide_op_sequence opsdefined opsused instrs anchoraddr in + Some (WideSubtract, wop) + | _ -> None) + | _ -> None) + | ReverseSubtractCarry (_, ACCAlways, rdhi, rnhi, rmhi) -> + let revinstraddr = anchoraddr#add_int (-4) in + (match TR.to_option (get_arm_assembly_instruction revinstraddr) with + | Some revinstr -> + (match revinstr#get_opcode with + | ReverseSubtract (true, ACCAlways, rdlo, rnlo, rmlo, _) -> + let instrs = [revinstr; anchorinstr] in + let opsdefined = [(rdlo, rdhi)] in + let opsused = [(rnlo, rnhi); (rmlo, rmhi)] in + let wop = make_wide_op_sequence opsdefined opsused instrs anchoraddr in + Some (WideReverseSubtract, wop) + | _ -> None) + | _ -> None) + | Move (_, ACCAlways, rd2, rn2, _, _) + when (is_wide_op anchoraddr ["wide-move"; "wide-move"]) -> + let mov1addr = anchoraddr#add_int(-4) in + (match TR.to_option (get_arm_assembly_instruction mov1addr) with + | Some mov1instr -> + (match mov1instr#get_opcode with + | Move (_, ACCAlways, rd1, rn1, _ , _) -> + (match ordered_register_combination rd1 rd2 with + | Some is_ordered -> + let instrs = [mov1instr; anchorinstr] in + let (opsdefined, opsused) = + if is_ordered then + ([(rd1, rd2)], [(rn1, rn2)]) + else + ([(rd2, rd1)], [(rn2, rn1)]) in + let wop = make_wide_op_sequence opsdefined opsused instrs anchoraddr in + Some (WideMove, wop) + | _ -> None) + | _ -> None) + | _ -> None) + | BitwiseNot (false, ACCAlways, rd2, rn2, _) + when (is_wide_op anchoraddr ["wide-move-not"]) -> + let mvn1addr = anchoraddr#add_int(-4) in + (match TR.to_option (get_arm_assembly_instruction mvn1addr) with + | Some mvn1instr -> + (match mvn1instr#get_opcode with + | BitwiseNot (false, ACCAlways, rd1, rn1, _ ) -> + (match ordered_register_combination rd1 rd2 with + | Some is_ordered -> + let instrs = [mvn1instr; anchorinstr] in + let (opsdefined, opsused) = + if is_ordered then + ([(rd1, rd2)], [(rn1, rn2)]) + else + ([(rd2, rd1)], [(rn2, rn1)]) in + let wop = make_wide_op_sequence opsdefined opsused instrs anchoraddr in + Some (WideMoveNot, wop) + | _ -> None) + | _ -> None) + | _ -> None) + | BitwiseAnd (_, ACCAlways, rd2, rn2, rm2, _) + when is_wide_op anchoraddr ["wide-and"] -> + let and1addr = anchoraddr#add_int(-4) in + (match TR.to_option (get_arm_assembly_instruction and1addr) with + | Some and1instr -> + (match and1instr#get_opcode with + | BitwiseAnd (_, ACCAlways, rd1, rn1, rm1, _) -> + (match ordered_register_combination rd1 rd2 with + | Some is_ordered -> + let instrs = [and1instr; anchorinstr] in + let (opsdefined, opsused) = + if is_ordered then + ([(rd1, rd2)], [(rn1, rn2); (rm1, rm2)]) + else + ([(rd2, rd1)], [(rn2, rn1); (rm2, rm1)]) in + let wop = make_wide_op_sequence opsdefined opsused instrs anchoraddr in + Some (WideAnd, wop) + | _ -> None) + | _ -> None) + | _ -> None) + | BitwiseOr (_, ACCAlways, rd2, rn2, rm2, _) + when is_wide_op anchoraddr ["wide-or"] -> + let or1addr = anchoraddr#add_int(-4) in + (match TR.to_option (get_arm_assembly_instruction or1addr) with + | Some or1instr -> + (match or1instr#get_opcode with + | BitwiseOr (_, ACCAlways, rd1, rn1, rm1, _) -> + (match ordered_register_combination rd1 rd2 with + | Some is_ordered -> + let instrs = [or1instr; anchorinstr] in + let (opsdefined, opsused) = + if is_ordered then + ([(rd1, rd2)], [(rn1, rn2); (rm1, rm2)]) + else + ([(rd2, rd1)], [(rn2, rn1); (rm2, rm1)]) in + let wop = make_wide_op_sequence opsdefined opsused instrs anchoraddr in + Some (WideOr, wop) + | _ -> None) + | _ -> None) + | _ -> None) + | BitwiseExclusiveOr (_, ACCAlways, rd2, rn2, rm2, _) + when is_wide_op anchoraddr ["wide-xor"] -> + let xor1addr = anchoraddr#add_int(-4) in + (match TR.to_option (get_arm_assembly_instruction xor1addr) with + | Some xor1instr -> + (match xor1instr#get_opcode with + | BitwiseExclusiveOr (_, ACCAlways, rd1, rn1, rm1, _) -> + (match ordered_register_combination rd1 rd2 with + | Some is_ordered -> + let instrs = [xor1instr; anchorinstr] in + let (opsdefined, opsused) = + if is_ordered then + ([(rd1, rd2)], [(rn1, rn2); (rm1, rm2)]) + else + ([(rd2, rd1)], [(rn2, rn1); (rm2, rm1)]) in + let wop = make_wide_op_sequence opsdefined opsused instrs anchoraddr in + Some (WideXOr, wop) + | _ -> None) + | _ -> None) + | _ -> None) + + | _ -> None diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMWideOpSequence.mli b/CodeHawk/CHB/bchlibarm32/bCHARMWideOpSequence.mli new file mode 100644 index 000000000..bbea3514e --- /dev/null +++ b/CodeHawk/CHB/bchlibarm32/bCHARMWideOpSequence.mli @@ -0,0 +1,44 @@ +(* ============================================================================= + CodeHawk Binary Analyzer + Author: Henny Sipma + ------------------------------------------------------------------------------ + The MIT License (MIT) + + Copyright (c) 2026 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 + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + ============================================================================= *) + +(* bchlib *) +open BCHLibTypes + +(* bchlibarm32 *) +open BCHARMTypes + + +(** Data structure to support idiomatic constructs for 64-bit operations.*) + +val arm_lo_hi_operand_pair_to_string: arm_lo_hi_operand_pair_t -> string + +val arm_lo_hi_register_pair_to_string: arm_lo_hi_register_pair_t -> string + +val create_arm_wide_op_sequence: + pushback_stream_int + -> arm_assembly_instruction_int + -> (arm_wide_op_kind_t * arm_wide_op_sequence_int) option diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 32cd5a757..228e4aee6 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 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 @@ -157,6 +157,61 @@ object (self) log_error_result ~msg:(p2s floc#l#toPretty) file line e else () in + + let get_wide_op_destination_operand (wop: arm_wide_op_sequence_int) = + match wop#lo_hi_operand_pairs_defined with + | [p] -> p + | [] -> + raise + (BCH_failure + (LBLOCK [STR "No operands defined in wide-op operation"])) + | _ -> + raise + (BCH_failure + (LBLOCK [STR "Too many operands defined in wide-op operation"])) in + + let get_unary_wide_op_source_operand (wop: arm_wide_op_sequence_int) = + match wop#lo_hi_operand_pairs_used with + | [p] -> p + | [] -> + raise + (BCH_failure + (LBLOCK [STR "Too few operands used in wide-op operation"])) + | _ -> + raise + (BCH_failure + (LBLOCK [STR "Too many operands used in wide-op operation"])) in + + let get_binary_wide_op_source_operands (wop: arm_wide_op_sequence_int) = + match wop#lo_hi_operand_pairs_used with + | [p1; p2] -> (p1, p2) + | [] | [_] -> + raise + (BCH_failure + (LBLOCK [STR "Too few operands used in wide-op operation"])) + | _ -> + raise + (BCH_failure + (LBLOCK [STR "Too many operands used in wide-op operation"])) in + + let is_part_of_wide_op_instr () = + match instr#is_in_aggregate with + | Some dw -> + let agg = get_aggregate dw in + agg#is_arm_wide_operation + | _ -> false in + + let make_wide_op_r hi_r lo_r = + let e32 = num_constant_expr numerical_e32 in + TR.tmap2 (fun hi lo -> + XOp (XPlus, [XOp (XMult, [hi; e32]); lo])) hi_r lo_r in + + let extract_wide_hi x_r = + TR.tmap (fun x -> XOp (XAsr, [x; int_constant_expr 32])) x_r in + + let extract_wide_lo x_r = + TR.tmap (fun x -> XOp (XMod, [x; num_constant_expr numerical_e32])) x_r in + let rewrite_expr ?(restrict:int option) (x: xpr_t): xpr_t = try let xpr = floc#inv#rewrite_expr ~loopcounter:true x in @@ -297,6 +352,66 @@ object (self) let get_rdef_r (x_r: xpr_t traceresult): int = TR.tfold_default get_rdef (-1) x_r in + let get_rdefdouble_r ((xlo_r, xhi_r): (xpr_t traceresult * xpr_t traceresult)): int = + TR.tfold_default + (fun xlo -> + TR.tfold_default + (fun xhi -> + match (xlo, xhi) with + | (XVar vlo, XVar vhi) + when floc#f#env#is_register_variable vlo + && floc#f#env#is_register_variable vhi -> + let reglo = TR.tget_ok (floc#f#env#get_register vlo) in + let reghi = TR.tget_ok (floc#f#env#get_register vhi) in + (match (reglo, reghi) with + | (ARMRegister areglo, ARMRegister areghi) -> + let vlohi = floc#f#env#mk_arm_double_register_variable areglo areghi in + let symvar = floc#f#env#mk_symbolic_variable vlohi in + let varinvs = varinv#get_var_reaching_defs symvar in + (match varinvs with + | [vinv] -> + (match vinv#get_clobber_rdefs with + | [] -> + let _ = + log_diagnostics_result + ~tag:"get_rdefdouble:found" + ~msg:floc#cia + __FILE__ __LINE__ + ["vinv: " ^ (p2s vinv#toPretty)] in + vinv#index + | clobbers -> + let _ = + List.iter + (BCHSystemInfo.system_info#set_double_rdef_location + floc#cia reglo reghi) clobbers in + (-1)) + | _ -> + let _ = + log_diagnostics_result + ~tag:"get_rdefdouble:no or multiple" + ~msg:floc#cia + __FILE__ __LINE__ + ["Unable to find rdef for " ^ (p2s vlohi#toPretty)] in + (-1)) + | _ -> + let _ = + log_diagnostics_result + ~tag:"get_rdefdouble" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not two registers: " ^ (register_to_string reglo)] in + (-1)) + | _ -> + let _ = + log_diagnostics_result + ~tag:"get_rdefdouble" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not a variable: (" ^ (x2s xlo) ^ ", " ^ (x2s xhi) ^ ")"] in + (-1) + ) (-1) xhi_r) + (-1) xlo_r in + let get_all_rdefs (xpr: xpr_t): int list = let vars = floc#env#variables_in_expr ~include_addressof:false xpr in List.fold_left (fun acc v -> @@ -421,6 +536,7 @@ object (self) ?(types: btype_t list = []) ?(xprs: xpr_t list = []) ?(rdefs: int list = []) + ?(rdefdoubles: int list = []) ?(uses: int list = []) ?(useshigh: int list = []) ?(integers: int list = []) @@ -433,6 +549,7 @@ object (self) let varcount = List.length vars in let xprcount = List.length xprs in let rdefcount = List.length rdefs in + let rdefdoublescount = List.length rdefdoubles in let defusecount = List.length uses in let defusehighcount = List.length useshigh in let flagrdefcount = List.length flagrdefs in @@ -441,6 +558,7 @@ object (self) let typestring = string_repeat "t" varcount in let xprstring = string_repeat "x" xprcount in let rdefstring = string_repeat "r" rdefcount in + let rdefdoublestring = string_repeat "m" rdefdoublescount in let defusestring = string_repeat "d" defusecount in let defusehighstring = string_repeat "h" defusehighcount in let flagrdefstring = string_repeat "f" flagrdefcount in @@ -451,6 +569,7 @@ object (self) ^ typestring ^ xprstring ^ rdefstring + ^ rdefdoublestring ^ defusestring ^ defusehighstring ^ flagrdefstring @@ -469,6 +588,7 @@ object (self) @ typeargs @ xprargs @ rdefs + @ rdefdoubles @ uses @ useshigh @ flagrdefs @@ -481,7 +601,9 @@ object (self) ?(xprs_r: xpr_t traceresult list = []) ?(cxprs_r: xpr_t traceresult list = []) ?(rdefs: int list = []) + ?(rdefdoubles: int list = []) ?(uses: int list = []) + ?(usedoubles: int list = []) ?(useshigh: int list = []) ?(integers: int list = []) () = @@ -493,7 +615,9 @@ object (self) let xprcount = List.length xprs_r in let cxprcount = List.length cxprs_r in let rdefcount = List.length rdefs in + let rdefdoublescount = List.length rdefdoubles in let defusecount = List.length uses in + let defusedoublescount = List.length usedoubles in let defusehighcount = List.length useshigh in let flagrdefcount = List.length flagrdefs in let integercount = List.length integers in @@ -503,7 +627,9 @@ object (self) let xprstring = string_repeat "x" xprcount in let cxprstring = string_repeat "c" cxprcount in let rdefstring = string_repeat "r" rdefcount in + let rdefdoublestring = string_repeat "m" rdefdoublescount in let defusestring = string_repeat "d" defusecount in + let defusedoublestring = string_repeat "n" defusedoublescount in let defusehighstring = string_repeat "h" defusehighcount in let flagrdefstring = string_repeat "f" flagrdefcount in let integerstring = string_repeat "l" integercount in @@ -515,7 +641,9 @@ object (self) ^ xprstring ^ cxprstring ^ rdefstring + ^ rdefdoublestring ^ defusestring + ^ defusedoublestring ^ defusehighstring ^ flagrdefstring ^ integerstring in @@ -537,7 +665,9 @@ object (self) @ xprargs @ cxprargs @ rdefs + @ rdefdoubles @ uses + @ usedoubles @ useshigh @ flagrdefs @ integers) in @@ -654,25 +784,248 @@ object (self) else ()) callargs in + let unary_wop_xdata + (f: xpr_t -> xpr_t) + (agg: arm_instruction_aggregate_int) + (wop: arm_wide_op_sequence_int) + (name: string) = + let (rdlo, rdhi) = get_wide_op_destination_operand wop in + let (rnlo, rnhi) = get_unary_wide_op_source_operand wop in + let vrdlo_r = rdlo#to_variable floc in + let vrdhi_r = rdhi#to_variable floc in + let vrdlohi = + floc#f#env#mk_arm_double_register_variable + rdlo#get_register rdhi#get_register in + let xrnlo_r = rnlo#to_expr floc in + let xrnhi_r = rnhi#to_expr floc in + let xxrnlo_r = TR.tmap rewrite_expr xrnlo_r in + let xxrnhi_r = TR.tmap rewrite_expr xrnhi_r in + let xxrn_r = TR.tmap rewrite_expr (make_wide_op_r xxrnhi_r xxrnlo_r) in + let rresult_r = TR.tmap f xxrn_r in + let rresultlo_r = extract_wide_lo rresult_r in + let rresulthi_r = extract_wide_hi rresult_r in + let cresultlo_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in + let cresulthi_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in + let cresult_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 8)) rresult_r in + (* Only use rdefs if the rdefdouble is not valid *) + let (rdefs, rdefdoubles) = + List.fold_left (fun (rdefs, rdefdoubles) (lo, hi) -> + let d = get_rdefdouble_r (lo, hi) in + if d = (-1) then + let r = List.map get_rdef_r [lo; hi] in + let _ = + log_diagnostics_result + ~tag:"unary_wop_xdata" + ~msg:(p2s floc#l#toPretty) + __FILE__ __LINE__ + ["Include rdefs for " ^ (x_r2s lo) ^ " and " ^ (x_r2s hi)] in + (rdefs @ r, rdefdoubles) + else + (rdefs, rdefdoubles @ [d])) ([], []) [(xrnlo_r, xrnhi_r)] in + let uses = [get_def_use_r vrdlo_r; get_def_use_r vrdhi_r] in + let usedoubles = [get_def_use_r (Ok vrdlohi)] in + let useshigh = [get_def_use_high_r vrdlo_r; get_def_use_high_r vrdhi_r] in + let vars_r = [Ok vrdlohi; vrdlo_r; vrdhi_r] in + let xprs_r = + [xrnlo_r; xrnhi_r; rresult_r; rresultlo_r; rresulthi_r; + xxrnlo_r; xxrnhi_r; xxrn_r] in + let cxprs_r = [cresult_r; cresultlo_r; cresulthi_r] in + let (tagstring, args) = + mk_instrx_data_r + ~vars_r + ~xprs_r + ~cxprs_r + ~rdefs + ~rdefdoubles + ~uses + ~usedoubles + ~useshigh () in + let dependents = + List.map (fun d -> + (make_i_location floc#l d#get_address)#ci) agg#instrs in + ([tagstring; ("agg:" ^ name)] @ ["subsumes"] @ dependents, args) in + + let binary_wop_xdata + (f: xpr_t -> xpr_t -> xpr_t) + (agg: arm_instruction_aggregate_int) + (wop: arm_wide_op_sequence_int) + (name: string) = + let (rdlo, rdhi) = get_wide_op_destination_operand wop in + let ((rnlo, rnhi), (rmlo, rmhi)) = + get_binary_wide_op_source_operands wop in + let vrdlo_r = rdlo#to_variable floc in + let vrdhi_r = rdhi#to_variable floc in + let vrdlohi = + floc#f#env#mk_arm_double_register_variable + rdlo#get_register rdhi#get_register in + let xrnlo_r = rnlo#to_expr floc in + let xrnhi_r = rnhi#to_expr floc in + let xrmlo_r = rmlo#to_expr floc in + let xrmhi_r = rmhi#to_expr floc in + let xxrnlo_r = TR.tmap rewrite_expr xrnlo_r in + let xxrnhi_r = TR.tmap rewrite_expr xrnhi_r in + let xxrmlo_r = TR.tmap rewrite_expr xrmlo_r in + let xxrmhi_r = TR.tmap rewrite_expr xrmhi_r in + let xxrnw_r = TR.tmap rewrite_expr (make_wide_op_r xxrnhi_r xxrnlo_r) in + let xxrmw_r = TR.tmap rewrite_expr (make_wide_op_r xxrmhi_r xxrmlo_r) in + let rresultw_r = TR.tmap2 f xxrnw_r xxrmw_r in + let rresultlo_r = extract_wide_lo rresultw_r in + let rresulthi_r = extract_wide_hi rresultw_r in + let cresultw_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 8)) rresultw_r in + let cresultlo_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresultlo_r in + let cresulthi_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresulthi_r in + let _rdefs = + List.map get_rdef_r [xrnlo_r; xrnhi_r; xrmlo_r; xrmhi_r] in + (* Only use rdefs if the rdefdouble is not valid *) + let (rdefs, rdefdoubles) = + List.fold_left (fun (rdefs, rdefdoubles) (lo, hi) -> + let d = get_rdefdouble_r (lo, hi) in + if d = (-1) then + let r = List.map get_rdef_r [lo; hi] in + let _ = + log_diagnostics_result + ~tag:"binary_wop_xdata" + ~msg:(p2s floc#l#toPretty) + __FILE__ __LINE__ + ["Include rdefs for " ^ (x_r2s lo) ^ " and " ^ (x_r2s hi)] in + (rdefs @ r, rdefdoubles) + else + (rdefs, rdefdoubles @ [d])) + ([], []) [(xrnlo_r, xrnhi_r); (xrmlo_r, xrmhi_r)] in + let uses = [get_def_use_r vrdlo_r; get_def_use_r vrdhi_r] in + let usedoubles = [get_def_use_r (Ok vrdlohi)] in + let useshigh = [get_def_use_r (Ok vrdlohi)] in + let vars_r = [Ok vrdlohi; vrdlo_r; vrdhi_r] in + let xprs_r = + [xrnlo_r; xrnhi_r; xrmlo_r; xrmhi_r; rresultw_r; rresultlo_r; rresulthi_r; + xxrnlo_r; xxrnhi_r; xxrmlo_r; xxrmhi_r; xxrnw_r; xxrmw_r] in + let cxprs_r = [cresultw_r; cresultlo_r; cresulthi_r] in + let (tagstring, args) = + mk_instrx_data_r + ~vars_r + ~xprs_r + ~cxprs_r + ~rdefs + ~rdefdoubles + ~uses + ~usedoubles + ~useshigh + () in + let dependents = + List.map (fun d -> + (make_i_location floc#l d#get_address)#ci) agg#instrs in + ([tagstring; ("agg:" ^ name)] @ ["subsumes"] @ dependents, args) in + + let callinstr_callarg_data + (p: fts_parameter_t) (x: xpr_t) (index: int): + (xpr_t traceresult * xpr_t * xpr_t traceresult * int list * int list) = + let (xvar_r, rdefs_p, rdefdoubles_p) = + if is_register_parameter p then + let regarg = TR.tget_ok (get_register_parameter_register p) in + let pvar = floc#f#env#mk_register_variable regarg in + let xvar_r = Ok (XVar pvar) in + match regarg with + | ARMRegister _ -> + let rdefs = [get_rdef_r xvar_r] in + (xvar_r, rdefs, []) + | ARMDoubleRegister (ar1, ar2) -> + let pvarlo = floc#f#env#mk_arm_register_variable ar1 in + let pvarhi = floc#f#env#mk_arm_register_variable ar2 in + let xvarlo_r = Ok (XVar pvarlo) in + let xvarhi_r = Ok (XVar pvarhi) in + let rdefs_p = [] (* List.map get_rdef_r [xvarlo_r; xvarhi_r] *) in + let rdefdoubles_p = List.map get_rdefdouble_r [(xvarlo_r, xvarhi_r)] in + (xvar_r, rdefs_p, rdefdoubles_p) + | _ -> + let rdefs = [get_rdef_r xvar_r] in + (xvar_r, rdefs, []) + else if is_stack_parameter p then + let p_offset_r = get_stack_parameter_offset p in + let sp_r = (sp_r RD)#to_expr floc in + let xvar_r = + TR.tmap2 (fun p_offset sp -> + XOp (XPlus, [sp; int_constant_expr p_offset])) + p_offset_r sp_r in + (xvar_r, [get_rdef_r xvar_r], []) + else + (Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Parameter type not recognized in call instruction"], + [], []) in + let xx = rewrite_expr ?restrict:(Some 4) x in + let ptype = get_parameter_type p in + let xx = + if is_pointer ptype (* && (not (is_char_pointer ptype)) *) then + let _ = floc#memrecorder#record_argument xx index in + match get_string_reference floc xx with + | Some _ -> xx + | _ -> + match xx with + | XVar _ -> xx + | _ -> + TR.tfold + ~ok:(fun v -> + let _ = + log_diagnostics_result + ~msg:(p2s floc#l#toPretty) + ~tag:"callinstr-key:get-var-at-address" + __FILE__ __LINE__ + ["xx: " ^ (x2s xx); "v: " ^ (p2s v#toPretty)] in + XOp ((Xf "addressofvar"), [(XVar v)])) + ~error:(fun e -> + let _ = log_dc_error_result __FILE__ __LINE__ e in + xx) + (floc#get_var_at_address ~btype:(ptr_deref ptype) xx) + else + xx in + let cx_r = floc#xpr_to_cxpr ~xtype:(Some ptype) xx in + (xvar_r, xx, cx_r, rdefs_p, rdefdoubles_p) in + let callinstr_key (): (string list * int list) = let callargs = floc#get_call_arguments in let _ = check_for_functionptr_args callargs in - let (xprs, cxprs_r, xvars, rdefs, _) = - List.fold_left (fun (xprs, cxprs_r, xvars, rdefs, index) (p, x) -> - let xvar_r = + let (xprs, cxprs_r, xvars, rdefs, rdefdoubles, _) = + List.fold_left (fun (xprs, cxprs_r, xvars, rdefs, rdefdoubles, index) (p, x) -> + let (xvar_r, xx, cx_r, rdefs_p, rdefdoubles_p) = + callinstr_callarg_data p x index in + (* + let (xvar_r, rdefs_p, rdefdoubles_p) = if is_register_parameter p then let regarg = TR.tget_ok (get_register_parameter_register p) in let pvar = floc#f#env#mk_register_variable regarg in - Ok (XVar pvar) + let xvar_r = Ok (XVar pvar) in + match regarg with + | ARMRegister _ -> + let rdefs = [get_rdef_r xvar_r] in + (xvar_r, rdefs, []) + | ARMDoubleRegister (ar1, ar2) -> + let pvarlo = floc#f#env#mk_arm_register_variable ar1 in + let pvarhi = floc#f#env#mk_arm_register_variable ar2 in + let xvarlo_r = Ok (XVar pvarlo) in + let xvarhi_r = Ok (XVar pvarhi) in + let rdefs_p = List.map get_rdef_r [xvarlo_r; xvarhi_r] in + let rdefdoubles_p = [get_rdef_r xvar_r] in + (xvar_r, rdefs_p, rdefdoubles_p) + | _ -> + let rdefs = [get_rdef_r xvar_r] in + (xvar_r, rdefs, []) else if is_stack_parameter p then let p_offset_r = get_stack_parameter_offset p in let sp_r = (sp_r RD)#to_expr floc in - TR.tmap2 (fun p_offset sp -> - XOp (XPlus, [sp; int_constant_expr p_offset])) - p_offset_r sp_r + let xvar_r = + TR.tmap2 (fun p_offset sp -> + XOp (XPlus, [sp; int_constant_expr p_offset])) + p_offset_r sp_r in + ([xvar_r], [get_rdef_r xvar_r], []) else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Parameter type not recognized in call instruction"] in + ([Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Parameter type not recognized in call instruction"]], + [], []) in let xx = rewrite_expr ?restrict:(Some 4) x in let ptype = get_parameter_type p in let xx = @@ -699,32 +1052,81 @@ object (self) (floc#get_var_at_address ~btype:(ptr_deref ptype) xx) else xx in - let cx_r = floc#xpr_to_cxpr ~xtype:(Some ptype) xx in - let rdef = get_rdef_r xvar_r in + let cx_r = floc#xpr_to_cxpr ~xtype:(Some ptype) xx in *) + (* let rdef = get_rdef_r xvar_r in *) (xx :: xprs, cx_r :: cxprs_r, xvar_r :: xvars, - rdef :: rdefs, + rdefs_p @ rdefs, + rdefdoubles_p @ rdefdoubles, index + 1)) - ([], [], [], [], 1) callargs in - let (vrd, rtype) = - let fintf = floc#get_call_target#get_function_interface in - let rtype = get_fts_returntype fintf in - let rtype = if is_void_pointer rtype then t_ptrto t_uchar else rtype in - let reg = - if is_float rtype then - let regtype = - if is_float_float rtype then - XSingle - else if is_float_double rtype then - XDouble - else - XQuad in - register_of_arm_extension_register - ({armxr_type = regtype; armxr_index = 0}) + ([], [], [], [], [], 1) callargs in + let fintf = floc#get_call_target#get_function_interface in + let rtype = get_fts_returntype fintf in + let rtype = if is_void_pointer rtype then t_ptrto t_uchar else rtype in + let (vars_r, uses, usedoubles, useshigh) = + if is_float rtype then + if BCHSystemSettings.system_settings#is_hard_float then + let reg = + let regtype = + if is_float_float rtype then + XSingle + else if is_float_double rtype then + XDouble + else + XQuad in + register_of_arm_extension_register + ({armxr_type = regtype; armxr_index = 0}) in + let var_r = Ok (floc#f#env#mk_register_variable reg) in + let uses = [get_def_use_r var_r] in + let useshigh = [get_def_use_high_r var_r] in + ([var_r], uses, [], useshigh) else - register_of_arm_register AR0 in - (floc#f#env#mk_register_variable reg, rtype) in + if is_float_float rtype then + let var_r = Ok (floc#f#env#mk_arm_register_variable AR0) in + let uses = [get_def_use_r var_r] in + let useshigh = [get_def_use_high_r var_r] in + ([var_r], uses, [], useshigh) + else if is_float_double rtype then + let varlo_r = Ok (floc#f#env#mk_arm_register_variable AR0) in + let varhi_r = Ok (floc#f#env#mk_arm_register_variable AR1) in + let uses = [get_def_use_r varlo_r; get_def_use_r varhi_r] in + let useshigh = [get_def_use_high_r varlo_r; get_def_use_high_r varhi_r] in + let vlohi = Ok (floc#f#env#mk_arm_double_register_variable AR0 AR1) in + let usedoubles = [get_def_use_r vlohi] in + ([vlohi], uses, usedoubles, useshigh) + else + let var_r = Ok (floc#f#env#mk_arm_register_variable AR0) in + let uses = [get_def_use_r var_r] in + let useshigh = [get_def_use_high_r var_r] in + ([var_r], uses, [], useshigh) + else + match rtype with + | TInt (ik, _) -> + let isize = size_of_int_ikind ik in + if isize <= 4 then + let var_r = Ok (floc#f#env#mk_arm_register_variable AR0) in + let uses = [get_def_use_r var_r] in + let useshigh = [get_def_use_high_r var_r] in + ([var_r], uses, [], useshigh) + else if isize <= 8 then + let varlo_r = Ok (floc#f#env#mk_arm_register_variable AR0) in + let varhi_r = Ok (floc#f#env#mk_arm_register_variable AR1) in + let uses = [get_def_use_r varlo_r; get_def_use_r varhi_r] in + let useshigh = [get_def_use_high_r varlo_r; get_def_use_high_r varhi_r] in + let vlohi = Ok (floc#f#env#mk_arm_double_register_variable AR0 AR1) in + let usedoubles = [get_def_use_r vlohi] in + ([vlohi], uses, usedoubles, useshigh) + else + let var_r = Ok (floc#f#env#mk_arm_register_variable AR0) in + let uses = [get_def_use_r var_r] in + let useshigh = [get_def_use_high_r var_r] in + ([var_r], uses, [], useshigh) + | _ -> + let var_r = Ok (floc#f#env#mk_arm_register_variable AR0) in + let uses = [get_def_use_r var_r] in + let useshigh = [get_def_use_high_r var_r] in + ([var_r], uses, [], useshigh) in let _ = log_diagnostics_result ~tag:"callinstr_key" @@ -765,16 +1167,16 @@ object (self) "xrdefs: " ^ (String.concat ", " (List.map string_of_int xrdefs)); "deref-rdefs: " ^ (String.concat ", " (List.map string_of_int derefrdefs))] in - let vars_r = [Ok vrd] in + (* let vars_r = [Ok vrd] in *) let xprs_r = (List.rev (List.map (fun x -> Ok x) xprs)) @ (List.rev xvars) in let cxprs_r = List.rev cxprs_r in let types = [rtype] in let rdefs = (List.rev rdefs) @ xrdefs @ derefrdefs in - let uses = [get_def_use vrd] @ (List.map get_def_use derefuses) in - let useshigh = [get_def_use_high vrd] @ (List.map get_def_use derefuses) in + (* let uses = [get_def_use vrd] @ (List.map get_def_use derefuses) in *) + (* let useshigh = [get_def_use_high vrd] @ (List.map get_def_use derefuses) in *) let (tagstring, args) = mk_instrx_data_r - ~vars_r ~types ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in + ~vars_r ~types ~xprs_r ~cxprs_r ~rdefs ~rdefdoubles ~uses ~usedoubles ~useshigh () in let tags = if instr#is_inlined_call then tagstring :: ["call"; "inlined"] @@ -821,6 +1223,13 @@ object (self) (LBLOCK [ STR "Aggregate for Add not recognized at "; iaddr#toPretty])) + | Add _ when is_part_of_wide_op_instr () -> + (match instr#is_in_aggregate with + | Some va -> + let ctxtva = (make_i_location floc#l va)#ci in + ("a:" :: ["subsumed"; ctxtva], []) + | _ -> (["a:"], [])) + | Add (_, c, rd, rn, rm, _) -> let vrd_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in @@ -854,12 +1263,64 @@ object (self) let tags = add_optional_subsumption tags in (tags, args) + | AddCarry _ when instr#is_aggregate_anchor -> + let agg = get_aggregate floc#ia in + (match agg#kind with + | ARMWideOp (WideAdd, wop) -> + binary_wop_xdata (fun x y -> XOp (XPlus, [x; y])) agg wop "wideadd" + | _ -> + begin + log_error_result + ~tag:"AddCarry" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + ([], []) + end) + | AddCarry (_, c, rd, rn, rm, _) -> let vrd_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in + let xcarry = + match get_associated_test_instr floc#f floc#l#ci with + | Some (testloc, testinstr) -> + let (_, optpredicate, _) = + arm_conditional_expr + ~condopc:instr#get_opcode + ~testopc:testinstr#get_opcode + ~condloc:floc#l + ~testloc in + (match optpredicate with + | Some p -> + begin + log_diagnostics_result + ~tag:"AddCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + [x2s p]; + p + end + | _ -> + begin + log_diagnostics_result + ~tag:"AddCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + ["no predicate"]; + random_constant_expr + end) + | _ -> begin + log_diagnostics_result + ~tag:"AddCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + ["no associated setter"]; + random_constant_expr + end in let result_r = - TR.tmap2 (fun xrn xrm -> XOp (XPlus, [xrn; xrm])) xrn_r xrm_r in + TR.tmap2 (fun xrn xrm -> + XOp (XPlus, [XOp (XPlus, [xrn; xrm]); xcarry])) xrn_r xrm_r in let xxrn_r = TR.tmap rewrite_expr xrn_r in let xxrm_r = TR.tmap rewrite_expr xrm_r in let rresult_r = TR.tmap rewrite_expr result_r in @@ -962,6 +1423,28 @@ object (self) let (tags, args) = add_optional_instr_condition tagstring args c in (tags, args) + | BitwiseAnd _ when instr#is_aggregate_anchor -> + let agg = get_aggregate floc#ia in + (match agg#kind with + | ARMWideOp (WideAnd, wop) -> + binary_wop_xdata (fun x y -> XOp (XBAnd, [x; y])) agg wop "wideand" + | _ -> + begin + log_error_result + ~tag:"BitwiseAnd:aggregate" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + ([], []) + end) + + | BitwiseAnd _ when is_part_of_wide_op_instr () -> + (match instr#is_in_aggregate with + | Some va -> + let ctxtva = (make_i_location floc#l va)#ci in + ("a:" :: ["subsumed"; ctxtva], []) + | _ -> (["a:"], [])) + | BitwiseAnd (_, c, rd, rn, rm, _) -> let vrd_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in @@ -1007,6 +1490,28 @@ object (self) let (tags, args) = add_optional_instr_condition tagstring args c in (tags, args) + | BitwiseExclusiveOr _ when instr#is_aggregate_anchor -> + let agg = get_aggregate floc#ia in + (match agg#kind with + | ARMWideOp (WideXOr, wop) -> + binary_wop_xdata (fun x y -> XOp (XBXor, [x; y])) agg wop "widexor" + | _ -> + begin + log_error_result + ~tag:"BitwiseExclusiveOr:aggregate" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + ([], []) + end) + + | BitwiseExclusiveOr _ when is_part_of_wide_op_instr () -> + (match instr#is_in_aggregate with + | Some va -> + let ctxtva = (make_i_location floc#l va)#ci in + ("a:" :: ["subsumed"; ctxtva], []) + | _ -> (["a:"], [])) + | BitwiseExclusiveOr (_, c, rd, rn, rm, _) -> let vrd_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in @@ -1028,6 +1533,29 @@ object (self) let (tags, args) = add_optional_instr_condition tagstring args c in (tags, args) + | BitwiseNot _ + when instr#is_aggregate_anchor && (is_part_of_wide_op_instr ()) -> + let agg = get_aggregate floc#ia in + (match agg#kind with + | ARMWideOp (WideMoveNot, wop) -> + unary_wop_xdata (fun x -> XOp (XBNot, [x])) agg wop "widemovenot" + | _ -> + begin + log_error_result + ~tag:"BitwiseNot:aggregate" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + ([], []) + end) + + | BitwiseNot _ when is_part_of_wide_op_instr () -> + (match instr#is_in_aggregate with + | Some va -> + let ctxtva = (make_i_location floc#l va)#ci in + ("a:" :: ["subsumed"; ctxtva], []) + | _ -> (["a:"], [])) + | BitwiseNot _ when (Option.is_some instr#is_in_aggregate) -> (* TODO: add output for the case where BitwiseNot is the anchor *) (match instr#is_in_aggregate with @@ -1055,6 +1583,28 @@ object (self) let (tags, args) = add_optional_instr_condition tagstring args c in (tags, args) + | BitwiseOr _ when instr#is_aggregate_anchor -> + let agg = get_aggregate floc#ia in + (match agg#kind with + | ARMWideOp (WideOr, wop) -> + binary_wop_xdata (fun x y -> XOp (XBOr, [x; y])) agg wop "wideor" + | _ -> + begin + log_error_result + ~tag:"BitwiseOr:aggregate" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + ([], []) + end) + + | BitwiseOr _ when is_part_of_wide_op_instr () -> + (match instr#is_in_aggregate with + | Some va -> + let ctxtva = (make_i_location floc#l va)#ci in + ("a:" :: ["subsumed"; ctxtva], []) + | _ -> (["a:"], [])) + | BitwiseOr (_, c, rd, rn, rm, _) -> let vrd_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in @@ -1826,20 +2376,46 @@ object (self) let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in let vmem_r = mem#to_variable floc in - let vmem2_r = mem#to_variable floc in + let vmem2_r = mem2#to_variable floc in let xmem_r = mem#to_expr floc in let xrmem_r = TR.tmap rewrite_expr xmem_r in let xmem2_r = mem2#to_expr floc in let xrmem2_r = TR.tmap rewrite_expr xmem2_r in let xaddr1_r = mem#to_address floc in - let xaddr2_r = mem#to_address floc in + let xaddr2_r = mem2#to_address floc in let rdefs = [ get_rdef_r xrn_r; get_rdef_r xrm_r; get_rdef_memvar_r vmem_r; get_rdef_memvar_r vmem2_r] in let uses = [get_def_use_r vrt_r; get_def_use_r vrt2_r] in + let usedoubles = + if instr#is_wide_op_instruction then + let vrdlohi = + floc#env#mk_arm_double_register_variable + rt#get_register rt2#get_register in + [get_def_use_r (Ok vrdlohi)] + else + [] in let useshigh = [get_def_use_high_r vrt_r; get_def_use_high_r vrt2_r] in + let vars_r = + if instr#is_wide_op_instruction then + let vrdlohi = + floc#env#mk_arm_double_register_variable + rt#get_register rt2#get_register in + [vrt_r; vrt2_r; vmem_r; vmem2_r; Ok vrdlohi] + else + [vrt_r; vrt2_r; vmem_r; vmem2_r] in + let (xprs_r, cxprs_r) = + if instr#is_wide_op_instruction then + let xrmemw = make_wide_op_r xrmem2_r xrmem_r in + let crxmemw = TR.tbind floc#xpr_to_cxpr xrmemw in + ([xrn_r; xrm_r; xmem_r; xrmem_r; xmem2_r; + xrmem2_r; xaddr1_r; xaddr2_r; xrmemw], + [crxmemw]) + else + ([xrn_r; xrm_r; xmem_r; xrmem_r; xmem2_r; xrmem2_r; xaddr1_r; xaddr2_r], + []) in let _ = floc#memrecorder#record_load_r ~signed:false @@ -1856,11 +2432,12 @@ object (self) ~vtype:t_unknown in let (tagstring, args) = mk_instrx_data_r - ~vars_r:[vrt_r; vrt2_r; vmem_r; vmem2_r] - ~xprs_r:[xrn_r; xrm_r; xmem_r; xrmem_r; xmem2_r; - xrmem2_r; xaddr1_r; xaddr2_r] + ~vars_r + ~xprs_r + ~cxprs_r ~rdefs ~uses + ~usedoubles ~useshigh () in let (tags, args) = add_optional_instr_condition tagstring args c in @@ -1878,6 +2455,11 @@ object (self) (mem#to_updated_offset_address floc) else (tags, args) in + let (tags, args) = + if instr#is_wide_op_instruction then + (tags @ ["wop"], args) + else + (tags, args) in (tags, args) | LoadRegisterExclusive (c, rt, rn, rm, mem) -> @@ -2229,6 +2811,8 @@ object (self) | ARMTernaryAssignment _ -> [tagstring; "agg:ternassign:nd"] | _ -> [tagstring] in (tags, args)) + | ARMWideOp (WideMove, wop) -> + unary_wop_xdata (fun x -> x) agg wop "widemove" | _ -> raise (BCH_failure @@ -2236,11 +2820,14 @@ object (self) STR __FILE__; STR ":"; INT __LINE__; STR ": "; floc#l#toPretty; STR ": unknown MOV aggregate"]))) in - let dependents = - List.map (fun d -> - (make_i_location floc#l d#get_address)#ci) agg#instrs in - let tags = tags @ ["subsumes"] @ dependents in - (tags, args) + if List.mem "subsumes" tags then + (tags, args) + else + let dependents = + List.map (fun d -> + (make_i_location floc#l d#get_address)#ci) agg#instrs in + let tags = tags @ ["subsumes"] @ dependents in + (tags, args) | Move _ when (Option.is_some instr#is_in_aggregate) -> (match instr#is_in_aggregate with @@ -2444,12 +3031,27 @@ object (self) let (tags, args) = add_optional_instr_condition tagstring args c in let (tags, args) = if rl#includes_pc then - let r0_op = arm_register_op AR0 RD in - let xr0_r = r0_op#to_expr floc in - let xxr0_r = TR.tmap rewrite_expr xr0_r in - let xxr0_r = TR.tmap (rewrite_in_cc_context floc c) xxr0_r in - let cxr0_r = TR.tbind floc#xpr_to_cxpr xxr0_r in - add_return_value tags args xr0_r xxr0_r cxr0_r + let fsig = floc#f#get_summary#get_function_signature in + let rtype = fsig.fts_returntype in + if is_wide_type rtype then + let r0_op = arm_register_op AR0 RD in + let r1_op = arm_register_op AR1 RD in + let xr0_r = r0_op#to_expr floc in + let xr1_r = r1_op#to_expr floc in + let xxr0_r = TR.tmap rewrite_expr xr0_r in + let xxr1_r = TR.tmap rewrite_expr xr1_r in + let xxrw_r = make_wide_op_r xxr1_r xxr0_r in + let xxrw_r = TR.tmap (rewrite_in_cc_context floc c) xxrw_r in + let xxrw_r = TR.tmap rewrite_expr xxrw_r in + let cxrw = TR.tbind floc#xpr_to_cxpr xxrw_r in + add_return_value tags args xxrw_r xxrw_r cxrw + else + let r0_op = arm_register_op AR0 RD in + let xr0_r = r0_op#to_expr floc in + let xxr0_r = TR.tmap rewrite_expr xr0_r in + let xxr0_r = TR.tmap (rewrite_in_cc_context floc c) xxr0_r in + let cxr0_r = TR.tbind floc#xpr_to_cxpr xxr0_r in + add_return_value tags args xr0_r xxr0_r cxr0_r else (tags, args) in (tags, args) @@ -2506,6 +3108,13 @@ object (self) let (tags, args) = add_optional_instr_condition tagstring args c in (tags, args) + | ReverseSubtract _ when is_part_of_wide_op_instr () -> + (match instr#is_in_aggregate with + | Some va -> + let ctxtva = (make_i_location floc#l va)#ci in + ("a:" :: ["subsumed"; ctxtva], []) + | _ -> (["a:"], [])) + | ReverseSubtract (_, c, rd, rn, rm, _) -> let vrd_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in @@ -2529,6 +3138,85 @@ object (self) let (tags, args) = add_optional_instr_condition tagstring args c in (tags, args) + | ReverseSubtractCarry _ when instr#is_aggregate_anchor -> + let agg = get_aggregate floc#ia in + (match agg#kind with + | ARMWideOp (WideReverseSubtract, wop) -> + binary_wop_xdata (fun x y -> XOp (XMinus, [y; x])) agg wop "widereversesubtract" + | _ -> + begin + log_error_result + ~tag:"ReverseSubtractCarry" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + ([], []) + end) + + | ReverseSubtractCarry (_, c, rd, rn, rm) -> + let vrd_r = rd#to_variable floc in + let xrn_r = rn#to_expr floc in + let xrm_r = rm#to_expr floc in + let xcarry = + match get_associated_test_instr floc#f floc#l#ci with + | Some (testloc, testinstr) -> + let (_, optpredicate, _) = + arm_conditional_expr + ~condopc:instr#get_opcode + ~testopc:testinstr#get_opcode + ~condloc:floc#l + ~testloc in + (match optpredicate with + | Some p -> + begin + log_diagnostics_result + ~tag:"ReverseSubtractCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + [x2s p]; + p + end + | _ -> + begin + log_diagnostics_result + ~tag:"ReverseSubtractCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + ["no predicate"]; + random_constant_expr + end) + | _ -> + begin + log_diagnostics_result + ~tag:"ReverseSubtractCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + ["no associated setter"]; + random_constant_expr + end in + let result_r = + TR.tmap2 (fun xrn xrm -> + XOp (XPlus, + [XOp (XMinus, + [XOp (XMinus, [xrm; xrn]); int_constant_expr 1]); + xcarry])) xrn_r xrm_r in + let xxrn_r = TR.tmap rewrite_expr xrn_r in + let xxrm_r = TR.tmap rewrite_expr xrm_r in + let rresult_r = TR.tmap rewrite_expr result_r in + let cresult_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in + let rdefs = + [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in + let uses = [get_def_use_r vrd_r] in + let useshigh = [get_def_use_high_r vrd_r] in + let vars_r = [vrd_r] in + let xprs_r = [xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r] in + let cxprs_r = [cresult_r] in + let (tagstring, args) = + mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in + let (tags, args) = add_optional_instr_condition tagstring args c in + (tags, args) + | SelectBytes (c, rd, rn, rm) -> let lhs_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in @@ -2680,27 +3368,35 @@ object (self) | SignedMultiplyLong (_, c, rdlo, rdhi, rn, rm) -> let vlo_r = rdlo#to_variable floc in let vhi_r = rdhi#to_variable floc in + let rlo = rdlo#get_register in + let rhi = rdhi#get_register in + let vlohi = floc#env#mk_arm_double_register_variable rlo rhi in let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in let result_r = TR.tmap2 (fun xrn xrm -> XOp (XMult, [xrn; xrm])) xrn_r xrm_r in let result_r = TR.tmap rewrite_expr result_r in - let loresult_r = TR.tmap (fun r -> XOp (XMod, [r; e32_c])) result_r in - let hiresult_r = TR.tmap (fun r -> XOp (XDiv, [r; e32_c])) result_r in + let cresult_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 8)) result_r in + let loresult_r = extract_wide_lo result_r in + let hiresult_r = extract_wide_hi result_r in let loresultr_r = TR.tmap rewrite_expr loresult_r in let hiresultr_r = TR.tmap rewrite_expr hiresult_r in let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r result_r) in let uses = [get_def_use_r vlo_r; get_def_use_r vhi_r] in let useshigh = [get_def_use_high_r vlo_r; get_def_use_high_r vhi_r] in + let usedoubles = [get_def_use_r (Ok vlohi)] in let xprs_r = - [xrn_r; xrm_r; loresult_r; hiresult_r; loresultr_r; hiresultr_r] in + [xrn_r; xrm_r; result_r; loresult_r; hiresult_r; loresultr_r; hiresultr_r] in let (tagstring, args) = mk_instrx_data_r - ~vars_r:[vlo_r; vhi_r] + ~vars_r:[Ok vlohi; vlo_r; vhi_r] ~xprs_r + ~cxprs_r:[cresult_r] ~rdefs ~uses + ~usedoubles ~useshigh () in let (tags, args) = add_optional_instr_condition tagstring args c in @@ -3116,6 +3812,14 @@ object (self) let xrm_r = rm#to_expr floc in let xprs_r = [xrn_r; xrm_r; xrt_r; xxrt_r; xrt2_r; xxrt2_r; xaddr1_r; xaddr2_r] in + let cxprs_r = + if instr#is_wide_op_instruction then + let xxrt_combined = + TR.tmap rewrite_expr (make_wide_op_r xxrt_r xxrt2_r) in + let cxxrt_r = TR.tbind (floc#xpr_to_cxpr ~size:(Some 8)) xxrt_combined in + [cxxrt_r] + else + [] in let vars_r = [vmem_r; vmem2_r] in let uses = [get_def_use_r vmem_r; get_def_use_r vmem2_r] in let useshigh = [get_def_use_high_r vmem_r; get_def_use_high_r vmem2_r] in @@ -3140,8 +3844,20 @@ object (self) get_rdef_r xxrt_r; get_rdef_r xrt2_r; get_rdef_r xxrt2_r] in + let rdefdoubles = + if instr#is_wide_op_instruction then + List.map get_rdefdouble_r [(xrt_r, xrt2_r)] + else + [] in let (tagstring, args) = - mk_instrx_data_r ~vars_r ~xprs_r ~rdefs ~uses ~useshigh () in + mk_instrx_data_r + ~vars_r + ~xprs_r + ~cxprs_r + ~rdefs + ~rdefdoubles + ~uses + ~useshigh () in let (tags, args) = add_optional_instr_condition tagstring args c in let (tags, args) = if mem#is_offset_address_writeback then @@ -3157,6 +3873,11 @@ object (self) (mem#to_updated_offset_address floc) else (tags, args) in + let (tags, args) = + if instr#is_wide_op_instruction then + (tags @ ["wop"], args) + else + (tags, args) in (tags, args) | StoreRegisterExclusive (c, rd, rt, rn, mem) -> @@ -3238,6 +3959,13 @@ object (self) (tags, args) in (tags, args) + | Subtract _ when is_part_of_wide_op_instr () -> + (match instr#is_in_aggregate with + | Some va -> + let ctxtva = (make_i_location floc#l va)#ci in + ("a:" :: ["subsumed"; ctxtva], []) + | _ -> (["a:"], [])) + | Subtract (_, c, rd, rn, rm, _, _) -> let vrd_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in @@ -3262,13 +3990,72 @@ object (self) let (tags, args) = add_optional_instr_condition tagstring args c in (tags, args) + | SubtractCarry _ when instr#is_aggregate_anchor -> + let agg = get_aggregate floc#ia in + (match agg#kind with + | ARMWideOp (WideSubtract, wop) -> + binary_wop_xdata (fun x y -> XOp (XMinus, [x; y])) agg wop "widesubtract" + | _ -> + begin + log_error_result + ~tag:"SubtractCarry" + ~msg:floc#cia + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + ([], []) + end) + | SubtractCarry (_, c, rd, rn, rm, _) -> let vrd_r = rd#to_variable floc in let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in + let xcarry = + match get_associated_test_instr floc#f floc#l#ci with + | Some (testloc, testinstr) -> + let (_, optpredicate, _) = + arm_conditional_expr + ~condopc:instr#get_opcode + ~testopc:testinstr#get_opcode + ~condloc:floc#l + ~testloc in + (match optpredicate with + | Some p -> + begin + log_diagnostics_result + ~tag:"SubtractCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + [x2s p]; + p + end + | _ -> + begin + log_diagnostics_result + ~tag:"SubtractCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + ["no predicate"]; + random_constant_expr + end) + | _ -> + begin + log_diagnostics_result + ~tag:"SubtractCarry" + ~msg:floc#l#ci + __FILE__ __LINE__ + ["no associated setter"]; + random_constant_expr + end in let result_r = - TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrn; xrm])) xrn_r xrm_r in + TR.tmap2 + (fun xrn xrm -> + XOp (XPlus, + [XOp (XMinus, + [XOp (XMinus, [xrn; xrm]); int_constant_expr 1]); + xcarry])) xrn_r xrm_r in let rresult_r = TR.tmap rewrite_expr result_r in + let cresult_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 4)) rresult_r in let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in let uses = [get_def_use_r vrd_r] in @@ -3277,6 +4064,7 @@ object (self) mk_instrx_data_r ~vars_r:[vrd_r] ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r] + ~cxprs_r:[cresult_r] ~rdefs ~uses ~useshigh @@ -3540,6 +4328,7 @@ object (self) let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r; get_rdef_r xlo_r; get_rdef_r xhi_r] @ (get_all_rdefs_r rresult_r) in + let rdefdoubles = List.map get_rdefdouble_r [(xlo_r, xhi_r)] in let uses = [get_def_use_r vlo_r; get_def_use_r vhi_r] in let useshigh = [get_def_use_high_r vlo_r; get_def_use_high_r vhi_r] in let (tagstring, args) = @@ -3547,6 +4336,7 @@ object (self) ~vars_r:[vlo_r; vhi_r] ~xprs_r:[xrn_r; xrm_r; xlo_r; xhi_r; result_r; rresult_r] ~rdefs + ~rdefdoubles ~uses ~useshigh () in @@ -3556,21 +4346,29 @@ object (self) | UnsignedMultiplyLong (_, c, rdlo, rdhi, rn, rm) -> let vlo_r = rdlo#to_variable floc in let vhi_r = rdhi#to_variable floc in + let rlo = rdlo#get_register in + let rhi = rdhi#get_register in + let vlohi = floc#env#mk_arm_double_register_variable rlo rhi in let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in let result_r = TR.tmap2 (fun xrn xrm -> XOp (XMult, [xrn; xrm])) xrn_r xrm_r in let rresult_r = TR.tmap rewrite_expr result_r in + let cresult_r = + TR.tbind (floc#xpr_to_cxpr ~size:(Some 8)) rresult_r in let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in let uses = [get_def_use_r vlo_r; get_def_use_r vhi_r] in + let usedoubles = [get_def_use_r (Ok vlohi)] in let useshigh = [get_def_use_high_r vlo_r; get_def_use_high_r vhi_r] in let (tagstring, args) = mk_instrx_data_r - ~vars_r:[vlo_r; vhi_r] + ~vars_r:[Ok vlohi; vlo_r; vhi_r] ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r] + ~cxprs_r:[cresult_r] ~rdefs ~uses + ~usedoubles ~useshigh () in let (tags, args) = add_optional_instr_condition tagstring args c in diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 2dd33eb38..0e8b5857e 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -623,6 +623,20 @@ let translate_arm_instruction (floc#env#mk_arm_register_variable r) :: acc | _ -> acc) [] ops in + let get_double_register_vars (ops: (arm_operand_int * arm_operand_int) list) = + let get_register (op: arm_operand_int): arm_reg_t option = + if op#is_register then + Some op#get_register + else + match op#get_kind with + | ARMShiftedReg (r, ARMImmSRT _) -> Some r + | _ -> None in + List.fold_left (fun acc (op1, op2) -> + let regvars = List.map get_register [op1; op2] in + match regvars with + | [Some r1; Some r2] -> (floc#env#mk_arm_double_register_variable r1 r2) :: acc + | _ -> acc) [] ops in + let get_use_high_vars ?(is_pop=false) (xprs: xpr_t list): variable_t list = let inv = floc#inv in List.fold_left (fun acc x -> @@ -696,12 +710,139 @@ let translate_arm_instruction agg#is_pseudo_ldrsh || agg#is_pseudo_ldrsb | _ -> false in - let calltgt_cmds (_tgt: arm_operand_int): cmd_t list = - let callargs = floc#get_call_arguments in - let fintf = floc#get_call_target#get_function_interface in - let rtype = get_fts_returntype fintf in - let returnreg = - if is_float rtype then + let is_part_of_wide_op_instr () = + match instr#is_in_aggregate with + | Some dw -> + let agg = get_aggregate dw in + agg#is_arm_wide_operation + | _ -> false in + + let get_wide_op_destination_operand (wop: arm_wide_op_sequence_int) = + match wop#lo_hi_operand_pairs_defined with + | [p] -> p + | [] -> + raise + (BCH_failure + (LBLOCK [STR "No operands defined in wide-op operation"])) + | _ -> + raise + (BCH_failure + (LBLOCK [STR "Too many operands defined in wide-op operation"])) in + + let get_unary_wide_op_source_operand (wop: arm_wide_op_sequence_int) = + match wop#lo_hi_operand_pairs_used with + | [p] -> p + | [] -> + raise + (BCH_failure + (LBLOCK [STR "Too few operands used in wide-op operation"])) + | _ -> + raise + (BCH_failure + (LBLOCK [STR "Too many operands used in wide-op operation"])) in + + let get_binary_wide_op_source_operands (wop: arm_wide_op_sequence_int) = + match wop#lo_hi_operand_pairs_used with + | [p1; p2] -> (p1, p2) + | [] | [_] -> + raise + (BCH_failure + (LBLOCK [STR "Too few operands used in wide-op operation"])) + | _ -> + raise + (BCH_failure + (LBLOCK [STR "Too many operands used in wide-op operation"])) in + + let make_wide_op_r lo_r hi_r = + let e32 = num_constant_expr numerical_e32 in + TR.tmap2 (fun hi lo -> + XOp (XPlus, [XOp (XMult, [hi; e32]); lo])) hi_r lo_r in + + let extract_wide_hi x_r = + TR.tmap (fun x -> XOp (XAsr, [x; int_constant_expr 32])) x_r in + + let extract_wide_lo x_r = + TR.tmap (fun x -> XOp (XMod, [x; num_constant_expr numerical_e32])) x_r in + + let unary_wop_cmds (f: xpr_t -> xpr_t) (wop: arm_wide_op_sequence_int): cmd_t list = + let (rdlo, rdhi) = get_wide_op_destination_operand wop in + let (rnlo, rnhi) = get_unary_wide_op_source_operand wop in + let vrdlo = floc#env#mk_register_variable rdlo#to_register in + let vrdhi = floc#env#mk_register_variable rdhi#to_register in + let regrdlo = rdlo#get_register in + let regrdhi = rdhi#get_register in + let vrdlohi = floc#env#mk_arm_double_register_variable regrdlo regrdhi in + let lhslo_r = TR.tmap (fun (v, _) -> v) (rdlo#to_lhs floc) in + let lhshi_r = TR.tmap (fun (v, _) -> v) (rdhi#to_lhs floc) in + let xrnlo_r = rnlo#to_expr floc in + let xrnhi_r = rnhi#to_expr floc in + let xrn_r = make_wide_op_r xrnlo_r xrnhi_r in + let rhs_r = TR.tmap f xrn_r in + let rhslo_r = extract_wide_lo rhs_r in + let rhshi_r = extract_wide_hi rhs_r in + let usevars = get_register_vars [rnlo; rnhi] in + let usedoubles = get_double_register_vars [(rnlo, rnhi)] in + let usehigh = get_use_high_vars_r [xrnlo_r; xrnhi_r] in + let cmds = + (floc#get_assign_commands_r lhslo_r rhslo_r) + @ (floc#get_assign_commands_r lhshi_r rhshi_r) in + let defcmds = + floc#get_vardef_commands + ~defs:[vrdlo; vrdhi] + ~defdoubles:[vrdlohi] + ~use:usevars + ~usedoubles + ~usehigh + ctxtiaddr in + defcmds @ cmds in + + let binary_wop_cmds + (f: xpr_t -> xpr_t -> xpr_t) (wop: arm_wide_op_sequence_int):cmd_t list = + let (rdlo, rdhi) = get_wide_op_destination_operand wop in + let ((rnlo, rnhi), (rmlo, rmhi)) = + get_binary_wide_op_source_operands wop in + let vrdlo = floc#env#mk_register_variable rdlo#to_register in + let vrdhi = floc#env#mk_register_variable rdhi#to_register in + let regrdlo = rdlo#get_register in + let regrdhi = rdhi#get_register in + let vrdlohi = floc#env#mk_arm_double_register_variable regrdlo regrdhi in + let lhslo_r = TR.tmap (fun (v, _) -> v) (rdlo#to_lhs floc) in + let lhshi_r = TR.tmap (fun (v, _) -> v) (rdhi#to_lhs floc) in + let xrnlo_r = rnlo#to_expr floc in + let xrnhi_r = rnhi#to_expr floc in + let xrmlo_r = rmlo#to_expr floc in + let xrmhi_r = rmhi#to_expr floc in + let xrn_r = make_wide_op_r xrnlo_r xrnhi_r in + let xrm_r = make_wide_op_r xrmlo_r xrmhi_r in + let rhs_r = TR.tmap2 f xrn_r xrm_r in + let rhslo_r = extract_wide_lo rhs_r in + let rhshi_r = extract_wide_hi rhs_r in + let usevars = get_register_vars [rnlo; rnhi; rmlo; rmhi] in + let usedoubles = get_double_register_vars [(rnlo, rnhi); (rmlo, rmhi)] in + let usehigh = get_use_high_vars_r [xrnlo_r; xrnhi_r; xrmlo_r; xrmhi_r] in + let cmds = + (floc#get_assign_commands_r lhslo_r rhslo_r) + @ (floc#get_assign_commands_r lhshi_r rhshi_r) in + let defcmds = + floc#get_vardef_commands + ~defs:[vrdlo; vrdhi] + ~defdoubles:[vrdlohi] + ~use:usevars + ~usedoubles + ~usehigh + ctxtiaddr in + defcmds @ cmds in + + (* returns: (returnvar -> returnval), defs, defdoubles, clobbers *) + let return_pieces (rtype: btype_t) (rvar: variable_t): + ((register_t * xpr_t) list * variable_t list * variable_t list * variable_t list) = + let vr0 = floc#f#env#mk_arm_register_variable AR0 in + let vr1 = floc#f#env#mk_arm_register_variable AR1 in + let vr2 = floc#f#env#mk_arm_register_variable AR2 in + let vr3 = floc#f#env#mk_arm_register_variable AR3 in + let mk_reg = floc#f#env#mk_register_variable in + if is_float rtype then + if BCHSystemSettings.system_settings#is_hard_float then let regtype = if is_float_float rtype then XSingle @@ -709,17 +850,72 @@ let translate_arm_instruction XDouble else XQuad in - register_of_arm_extension_register - ({armxr_type = regtype; armxr_index = 0}) + let reg = + register_of_arm_extension_register + {armxr_type = regtype; armxr_index = 0} in + ([(reg, XVar rvar)], [mk_reg reg], [], [vr0; vr1; vr2; vr3]) else - register_of_arm_register AR0 in - let returnvar = floc#f#env#mk_register_variable returnreg in - let (usecmds, use, usehigh) = + if is_float_float rtype then + ([(register_of_arm_register AR0, XVar rvar)], [vr0], [], [vr1; vr2; vr3]) + else if is_float_double rtype then + let vlohi = floc#f#env#mk_arm_double_register_variable AR0 AR1 in + ([(register_of_arm_register AR0, + TR.tvalue (extract_wide_lo (Ok (XVar rvar))) ~default:(XVar rvar)); + (register_of_arm_register AR1, + TR.tvalue (extract_wide_hi (Ok (XVar rvar))) ~default:(XVar rvar))], + [vr0; vr1], + [vlohi], + [vr2; vr3]) + else + let _ = + log_error_result + ~tag:"return_pieces:complex double" + ~msg:(p2s floc#l#toPretty) + __FILE__ __LINE__ + ["No representation yet for " + ^ "FLongDouble/FComplexDouble/FComplexLongDouble"] in + ([(register_of_arm_register AR0, XVar rvar)], [vr0], [], [vr1; vr2; vr3]) + else match rtype with + | TInt (ik, _) -> + let isize = size_of_int_ikind ik in + if isize <= 4 then + ([(register_of_arm_register AR0, XVar rvar)], [vr0], [], [vr1; vr2; vr3]) + else if isize <= 8 then + let vlohi = floc#f#env#mk_arm_double_register_variable AR0 AR1 in + ([(register_of_arm_register AR0, + TR.tvalue (extract_wide_lo (Ok (XVar rvar))) ~default:(XVar rvar)); + (register_of_arm_register AR1, + TR.tvalue (extract_wide_hi (Ok (XVar rvar))) ~default:(XVar rvar))], + [vr0; vr1], + [vlohi], + [vr2; vr3]) + else + let _ = + log_error_result + ~tag:"return_pieces:IInt128" + ~msg:(p2s floc#l#toPretty) + __FILE__ __LINE__ + ["No representation yet for IInt128"] in + ([(register_of_arm_register AR0, XVar rvar)], [vr0], [], [vr1; vr2; vr3]) + | _ -> + ([(register_of_arm_register AR0, XVar rvar)], [vr0], [], [vr1; vr2; vr3]) in + + let calltgt_cmds (_tgt: arm_operand_int): cmd_t list = + let callargs = floc#get_call_arguments in + let fintf = floc#get_call_target#get_function_interface in + let rvar = floc#f#env#mk_return_value ctxtiaddr in + let _ = + if floc#get_call_target#is_signature_valid then + let name = floc#get_call_target#get_name ^ "_rtn_" ^ ctxtiaddr in + floc#f#env#set_variable_name rvar name in + let rtype = get_fts_returntype fintf in + let (returnpieces, rvardefs, defdoubles, clobbers) = return_pieces rtype rvar in + let (usecmds, use, usedoubles, usehigh) = (* This doesn't seem quite right, because the variable may be either written or read. Here the assumption is made that the variable is just read (i.e., it is used) rather than written, which would require a def.*) - List.fold_left (fun (acccmds, accuse, accusehigh) (p, x) -> + List.fold_left (fun (acccmds, accuse, accusedoubles, accusehigh) (p, x) -> let ptype = get_parameter_type p in let addressedvars = if is_pointer ptype && (not (is_char_pointer ptype)) then @@ -751,9 +947,17 @@ let translate_arm_instruction [] in if is_register_parameter p then let regarg = TR.tget_ok (get_register_parameter_register p) in - let pvar = floc#f#env#mk_register_variable regarg in + let (use, usedoubles) = + match regarg with + | ARMRegister _ -> ([floc#f#env#mk_register_variable regarg], []) + | ARMDoubleRegister (ar1, ar2) -> + ([floc#f#env#mk_arm_register_variable ar1; + floc#f#env#mk_arm_register_variable ar2], + [floc#f#env#mk_register_variable regarg]) + | _ -> ([], []) in (acccmds, - pvar :: (addressedvars @ accuse), + use @ (addressedvars @ accuse), + usedoubles @ accusedoubles, addressedvars @ accusehigh) else if is_stack_parameter p then @@ -763,11 +967,12 @@ let translate_arm_instruction ~ok:(fun (stacklhs, stacklhscmds) -> (stacklhscmds @ acccmds, stacklhs :: (addressedvars @ accuse), + [], addressedvars @ accusehigh)) ~error:(fun e -> begin log_error_result __FILE__ __LINE__ e; - (acccmds, accuse, accusehigh) + (acccmds, accuse, [], accusehigh) end) (stackop#to_lhs floc) else @@ -776,7 +981,7 @@ let translate_arm_instruction (LBLOCK [ floc#l#toPretty; STR " Parameter type not recognized in call translation"]))) - ([], [], []) callargs in + ([], [], [], []) callargs in (* Add uses for buffer reads, as expressed in the callee's preconditions *) let (xpuse, xpusehigh) = @@ -832,15 +1037,14 @@ let translate_arm_instruction let usehigh = xpusehigh @ (get_use_high_vars (List.map snd callargs)) in let use = xpuse in - let vr1 = floc#f#env#mk_arm_register_variable AR1 in - let vr2 = floc#f#env#mk_arm_register_variable AR2 in - let vr3 = floc#f#env#mk_arm_register_variable AR3 in - let callcmds = floc#get_arm_call_commands in + let callcmds = floc#get_arm_call_commands returnpieces in let defcmds = floc#get_vardef_commands - ~defs:(returnvar :: xprdefs) - ~clobbers:[vr1; vr2; vr3] + ~defs:(rvardefs @ xprdefs) + ~defdoubles + ~clobbers ~use + ~usedoubles ~usehigh ctxtiaddr in usecmds @ defcmds @ callcmds in @@ -973,6 +1177,10 @@ let translate_arm_instruction * APSR.C = carry; * APSR.V = overflow; *------------------------------------------------------------------------- *) + | Add _ when is_part_of_wide_op_instr () -> + (* full semantics of wide add is in the accompanying AddCarry *) + default [] + | Add (_, c, rd, rn, rm, _) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap fst (rd#to_lhs floc) in @@ -1018,14 +1226,46 @@ let translate_arm_instruction * APSR.C = carry; * APSR.V = overflow; * ------------------------------------------------------------------------ *) + | AddCarry _ when instr#is_aggregate_anchor -> + let agg = get_aggregate loc#i in + (match agg#kind with + | ARMWideOp (WideAdd, wop) -> + let cmds = binary_wop_cmds (fun x y -> XOp (XPlus, [x; y])) wop in + default cmds + | _ -> + begin + log_error_result + ~tag:"AddCarry:aggregate" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + default [] + end) + | AddCarry (_, c, rd, rn, rm, _) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap (fun (v, _) -> v) (rd#to_lhs floc) in let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in + let xcarry = + match get_associated_test_instr finfo ctxtiaddr with + | Some (testloc, testinstr) -> + let (_, optpredicate, _) = + make_conditional_predicate + ~condinstr:instr + ~testinstr + ~condloc:loc + ~testloc in + (match optpredicate with + | Some p -> p + | _ -> random_constant_expr) + | _ -> random_constant_expr in + let rhs_r = + TR.tmap2 (fun xrn xrm -> + XOp (XPlus, [XOp (XPlus, [xrn; xrm]); xcarry])) xrn_r xrm_r in let usevars = get_register_vars [rn; rm] in let usehigh = get_use_high_vars_r [xrn_r; xrm_r] in - let cmds = floc#get_abstract_commands_r lhs_r in + let cmds = floc#get_assign_commands_r lhs_r rhs_r in let defcmds = floc#get_vardef_commands ~defs:[vrd] @@ -1116,6 +1356,25 @@ let translate_arm_instruction | ACCAlways -> default cmds | _ -> make_conditional_commands c cmds) + | BitwiseAnd _ when instr#is_aggregate_anchor -> + let agg = get_aggregate loc#i in + (match agg#kind with + | ARMWideOp (WideAnd, wop) -> + let cmds = binary_wop_cmds (fun x y -> XOp (XBAnd, [x; y])) wop in + default cmds + | _ -> + begin + log_error_result + ~tag:"BitwiseAnd:aggregate" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + default [] + end) + + | BitwiseAnd _ when is_part_of_wide_op_instr () -> + default [] + | BitwiseAnd (_, c, rd, rn, rm, _) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap fst (rd#to_lhs floc) in @@ -1162,6 +1421,25 @@ let translate_arm_instruction | ACCAlways -> default cmds | _ -> make_conditional_commands c cmds) + | BitwiseExclusiveOr _ when instr#is_aggregate_anchor -> + let agg = get_aggregate loc#i in + (match agg#kind with + | ARMWideOp (WideXOr, wop) -> + let cmds = binary_wop_cmds (fun x y -> XOp (XBXor, [x; y])) wop in + default cmds + | _ -> + begin + log_error_result + ~tag:"BitwiseExclusiveOr:aggregate" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + default [] + end) + + | BitwiseExclusiveOr _ when is_part_of_wide_op_instr () -> + default [] + | BitwiseExclusiveOr (_, c, rd, rn, rm, _) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap fst (rd#to_lhs floc) in @@ -1197,6 +1475,25 @@ let translate_arm_instruction * APSR.Z = IsZeroBit(result); * APSR.C = carry; * ------------------------------------------------------------------------ *) + | BitwiseNot _ when instr#is_aggregate_anchor && (is_part_of_wide_op_instr ()) -> + let mvnagg = get_aggregate loc#i in + (match mvnagg#kind with + | ARMWideOp (WideMoveNot, wop) -> + let cmds = unary_wop_cmds (fun x -> XOp (XBNot, [x])) wop in + default cmds + | _ -> + begin + log_error_result + ~tag:"MoveNot:aggregate" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s mvnagg#toPretty)]; + default [] + end) + + | BitwiseNot _ when is_part_of_wide_op_instr () -> + default [] + | BitwiseNot _ when Option.is_some instr#is_in_aggregate -> (* may be part of a ternary assignment. TODO: add code for the case where MVN is the anchor instruction.*) @@ -1251,6 +1548,25 @@ let translate_arm_instruction | ACCAlways -> default cmds | _ -> make_conditional_commands c cmds) + | BitwiseOr _ when instr#is_aggregate_anchor -> + let agg = get_aggregate loc#i in + (match agg#kind with + | ARMWideOp (WideOr, wop) -> + let cmds = binary_wop_cmds (fun x y -> XOp (XBOr, [x; y])) wop in + default cmds + | _ -> + begin + log_error_result + ~tag:"BitwiseOr:aggregate" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + default [] + end) + + | BitwiseOr _ when is_part_of_wide_op_instr () -> + default [] + | BitwiseOr (_, c, rd, rn, rm, _) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap fst (rd#to_lhs floc) in @@ -1321,7 +1637,9 @@ let translate_arm_instruction let (defs, use, usehigh) = let use = [vr0; vr1; vr2; vr3] in ([vr0], use, use) in - let cmds = floc#get_arm_call_commands in + let rvar = floc#f#env#mk_return_value floc#cia in + let r0 = register_of_arm_register AR0 in + let cmds = floc#get_arm_call_commands [(r0, XVar rvar)] in let defcmds = floc#get_vardef_commands ~defs:defs @@ -1876,9 +2194,17 @@ let translate_arm_instruction let usevars = TR.tfold_default (fun memvar2 -> memvar2 :: usevars) usevars memvar2_r in let usehigh = get_use_high_vars_r [rhs1_r; rhs2_r] in + let defdoubles = + if instr#is_wide_op_instruction then + let reglo = rt#get_register in + let reghi = rt2#get_register in + [floc#env#mk_arm_double_register_variable reglo reghi] + else + [] in let defcmds = floc#get_vardef_commands ~defs:[vrd1; vrd2] + ~defdoubles ~use:usevars ~usehigh:usehigh ctxtiaddr in @@ -2135,102 +2461,116 @@ let translate_arm_instruction * APSR.Z = IsZeroBit(result); * ------------------------------------------------------------------------ *) | Move (_, _, rd, _, _, _) when instr#is_aggregate_anchor -> - (match get_associated_test_instr finfo ctxtiaddr with - | Some (testloc, testinstr) -> - let movagg = get_aggregate loc#i in - (match movagg#kind with - | ARMPredicateAssignment (inverse, dstop) -> - let (_, optpredicate, _) = - make_conditional_predicate - ~condinstr:instr ~testinstr ~condloc:loc ~testloc in - let cmds = - let lhs_r = TR.tmap fst (dstop#to_lhs floc) in - let vrd = floc#env#mk_register_variable dstop#to_register in - match optpredicate with - | Some p -> - let p = if inverse then XOp (XLNot, [p]) else p in - let cmds = floc#get_assign_commands_r lhs_r (Ok p) in - let usevars = vars_in_expr_list [p] in - let usehigh = get_use_high_vars [p] in - let defcmds = - floc#get_vardef_commands - ~defs:[vrd] - ~use:usevars - ~usehigh - ~flagdefs - ctxtiaddr in - defcmds @ cmds - | _ -> - let _ = - chlog#add - "predicate assignment:no predicate" - (LBLOCK [floc#l#toPretty]) in - let cmds = floc#get_abstract_commands_r lhs_r in - let defcmds = - floc#get_vardef_commands ~defs:[vrd] ~flagdefs ctxtiaddr in - defcmds @ cmds in - default cmds - | ARMTernaryAssignment (dstop, n1, n2) -> - let (_, optpredicate, _) = - make_conditional_predicate - ~condinstr:instr ~testinstr ~condloc:loc ~testloc in - let (_, tests) = - make_instr_local_tests - ~condloc:loc ~testloc ~condinstr:instr ~testinstr in - let cmds = - let lhs_r = TR.tmap fst (dstop#to_lhs floc) in - let vrd = floc#env#mk_register_variable dstop#to_register in - match optpredicate with - | Some p -> - let x1 = XConst (IntConst n1) in - let x2 = XConst (IntConst n2) in - let cmd1 = floc#get_assign_commands_r lhs_r (Ok x1) in - let cmd2 = floc#get_assign_commands_r lhs_r (Ok x2) in - let usevars = vars_in_expr_list [p] in - let usehigh = get_use_high_vars [p] in - let defcmds = - floc#get_vardef_commands - ~defs:[vrd] - ~use:usevars - ~usehigh - ~flagdefs - ctxtiaddr in - let brcmd = - match tests with - | Some (thentest, elsetest) -> - BRANCH [LF.mkCode (thentest @ cmd1); - LF.mkCode (elsetest @ cmd2)] - | _ -> - BRANCH [LF.mkCode cmd1; LF.mkCode cmd2] in - defcmds @ [brcmd] - | _ -> - let _ = - chlog#add - "ternary assignment:no predicate" - (LBLOCK [floc#l#toPretty]) in - let cmds = floc#get_abstract_commands_r lhs_r in - let defcmds = - floc#get_vardef_commands ~defs:[vrd] ~flagdefs ctxtiaddr in - defcmds @ cmds in - default cmds + let movagg = get_aggregate loc#i in + (match movagg#kind with + | ARMPredicateAssignment _ | ARMTernaryAssignment _ -> + (match get_associated_test_instr finfo ctxtiaddr with + | Some (testloc, testinstr) -> + (match movagg#kind with + | ARMPredicateAssignment (inverse, dstop) -> + let (_, optpredicate, _) = + make_conditional_predicate + ~condinstr:instr ~testinstr ~condloc:loc ~testloc in + let cmds = + let lhs_r = TR.tmap fst (dstop#to_lhs floc) in + let vrd = floc#env#mk_register_variable dstop#to_register in + match optpredicate with + | Some p -> + let p = if inverse then XOp (XLNot, [p]) else p in + let cmds = floc#get_assign_commands_r lhs_r (Ok p) in + let usevars = vars_in_expr_list [p] in + let usehigh = get_use_high_vars [p] in + let defcmds = + floc#get_vardef_commands + ~defs:[vrd] + ~use:usevars + ~usehigh + ~flagdefs + ctxtiaddr in + defcmds @ cmds + | _ -> + let _ = + chlog#add + "predicate assignment:no predicate" + (LBLOCK [floc#l#toPretty]) in + let cmds = floc#get_abstract_commands_r lhs_r in + let defcmds = + floc#get_vardef_commands ~defs:[vrd] ~flagdefs ctxtiaddr in + defcmds @ cmds in + default cmds + | ARMTernaryAssignment (dstop, n1, n2) -> + let (_, optpredicate, _) = + make_conditional_predicate + ~condinstr:instr ~testinstr ~condloc:loc ~testloc in + let (_, tests) = + make_instr_local_tests + ~condloc:loc ~testloc ~condinstr:instr ~testinstr in + let cmds = + let lhs_r = TR.tmap fst (dstop#to_lhs floc) in + let vrd = floc#env#mk_register_variable dstop#to_register in + match optpredicate with + | Some p -> + let x1 = XConst (IntConst n1) in + let x2 = XConst (IntConst n2) in + let cmd1 = floc#get_assign_commands_r lhs_r (Ok x1) in + let cmd2 = floc#get_assign_commands_r lhs_r (Ok x2) in + let usevars = vars_in_expr_list [p] in + let usehigh = get_use_high_vars [p] in + let defcmds = + floc#get_vardef_commands + ~defs:[vrd] + ~use:usevars + ~usehigh + ~flagdefs + ctxtiaddr in + let brcmd = + match tests with + | Some (thentest, elsetest) -> + BRANCH [LF.mkCode (thentest @ cmd1); + LF.mkCode (elsetest @ cmd2)] + | _ -> + BRANCH [LF.mkCode cmd1; LF.mkCode cmd2] in + defcmds @ [brcmd] + | _ -> + let _ = + chlog#add + "ternary assignment:no predicate" + (LBLOCK [floc#l#toPretty]) in + let cmds = floc#get_abstract_commands_r lhs_r in + let defcmds = + floc#get_vardef_commands ~defs:[vrd] ~flagdefs ctxtiaddr in + defcmds @ cmds in + default cmds + | _ -> + (* should not be reachable *) + raise + (BCH_failure + (LBLOCK [floc#l#toPretty; STR ": Unknown MOV aggregate kind"]))) | _ -> - (* should not be reachable *) - raise - (BCH_failure - (LBLOCK [floc#l#toPretty; STR ": Unknown MOV aggregate kind"]))) + (* no predicate found *) + let vrd = floc#env#mk_register_variable rd#to_register in + let lhs_r = TR.tmap fst (rd#to_lhs floc) in + let cmds = floc#get_abstract_commands_r lhs_r in + let defcmds = floc#get_vardef_commands ~defs:[vrd] ctxtiaddr in + let cmds = defcmds @ cmds in + let _ = + chlog#add + "predicate assignment aggregate without predicate" + (LBLOCK [loc#toPretty; STR ": "; instr#toPretty]) in + default cmds) + | ARMWideOp (WideMove, wop) -> + let cmds = unary_wop_cmds (fun x -> x) wop in + default cmds | _ -> - (* no predicate found *) - let vrd = floc#env#mk_register_variable rd#to_register in - let lhs_r = TR.tmap fst (rd#to_lhs floc) in - let cmds = floc#get_abstract_commands_r lhs_r in - let defcmds = floc#get_vardef_commands ~defs:[vrd] ctxtiaddr in - let cmds = defcmds @ cmds in - let _ = - chlog#add - "predicate assignment aggregate without predicate" - (LBLOCK [loc#toPretty; STR ": "; instr#toPretty]) in - default cmds) + begin + log_error_result + ~tag:"Move:aggregate" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s movagg#toPretty)]; + default [] + end) | Move _ when Option.is_some instr#is_in_aggregate -> default [] @@ -2696,6 +3036,11 @@ let translate_arm_instruction | ACCAlways -> default cmds | _ -> make_conditional_commands c cmds) + | ReverseSubtract _ when is_part_of_wide_op_instr () -> + (* full semantics of wide reverse subtract is in the accompanying + ReverseSubtractCarry. *) + default [] + | ReverseSubtract (_, c, rd, rn, rm, _) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap fst (rd#to_lhs floc) in @@ -2717,12 +3062,46 @@ let translate_arm_instruction | ACCAlways -> default cmds | _ -> make_conditional_commands c cmds) + | ReverseSubtractCarry _ when instr#is_aggregate_anchor -> + let agg = get_aggregate loc#i in + (match agg#kind with + | ARMWideOp (WideReverseSubtract, wop) -> + let cmds = binary_wop_cmds (fun x y -> XOp (XMinus, [y; x])) wop in + default cmds + | _ -> + begin + log_error_result + ~tag:"ReverseSubtractCarry:aggregate" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + default [] + end) + | ReverseSubtractCarry(_, c, rd, rn, rm) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap fst (rd#to_lhs floc) in let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in - let rhs_r = TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrm; xrn])) xrn_r xrm_r in + let xcarry = + match get_associated_test_instr finfo ctxtiaddr with + | Some (testloc, testinstr) -> + let (_, optpredicate, _) = + make_conditional_predicate + ~condinstr:instr + ~testinstr + ~condloc:loc + ~testloc in + (match optpredicate with + | Some p -> p + | _ -> random_constant_expr) + | _ -> random_constant_expr in + let rhs_r = + TR.tmap2 (fun xrn xrm -> + XOp (XPlus, + [XOp (XMinus, + [XOp (XMinus, [xrm; xrn]); int_constant_expr 1]); + xcarry])) xrn_r xrm_r in let cmds = floc#get_assign_commands_r lhs_r rhs_r in let usevars = get_register_vars [rn; rm] in let usehigh = get_use_high_vars_r [xrn_r; xrm_r] in @@ -2912,17 +3291,24 @@ let translate_arm_instruction | SignedMultiplyLong (_, c, rdlo, rdhi, rn, rm) -> let vlo = floc#env#mk_register_variable rdlo#to_register in let vhi = floc#env#mk_register_variable rdhi#to_register in + let rlo = rdlo#get_register in + let rhi = rdhi#get_register in + let vlohi = floc#env#mk_arm_double_register_variable rlo rhi in let lhslo_r = TR.tmap fst (rdlo#to_lhs floc) in let lhshi_r = TR.tmap fst (rdhi#to_lhs floc) in let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in - let cmdslo = floc#get_abstract_commands_r lhslo_r in - let cmdshi = floc#get_abstract_commands_r lhshi_r in + let rhs = TR.tmap2 (fun xrn xrm -> XOp (XMult, [xrn; xrm])) xrn_r xrm_r in + let rhslo_r = extract_wide_lo rhs in + let rhshi_r = extract_wide_hi rhs in + let cmdslo = floc#get_assign_commands_r lhslo_r rhslo_r in + let cmdshi = floc#get_assign_commands_r lhshi_r rhshi_r in let usevars = get_register_vars [rn; rm] in let usehigh = get_use_high_vars_r [xrn_r; xrm_r] in let defcmds = floc#get_vardef_commands ~defs:[vlo; vhi] + ~defdoubles:[vlohi] ~use:usevars ~usehigh ctxtiaddr in @@ -3361,7 +3747,16 @@ let translate_arm_instruction let xrt2_r = rt2#to_expr floc in let usevars = get_register_vars [rt; rt2; rn; rm] in let usehigh = get_use_high_vars_r [xrt_r; xrt2_r] in - let rdefcmds = floc#get_vardef_commands ~use:usevars ~usehigh ctxtiaddr in + let usedoubles = + if instr#is_wide_op_instruction then + let rtreg = rt#get_register in + let rt2reg = rt2#get_register in + let rtcombined = floc#env#mk_arm_double_register_variable rtreg rt2reg in + [rtcombined] + else + [] in + let rdefcmds = + floc#get_vardef_commands ~usedoubles ~use:usevars ~usehigh ctxtiaddr in let cmds1 = TR.tfold ~ok:(fun (memlhs, memcmds) -> @@ -3496,6 +3891,10 @@ let translate_arm_instruction * APSR.C = carry; * APSR.V = overflow * ------------------------------------------------------------------------- *) + | Subtract _ when is_part_of_wide_op_instr () -> + (* full semantics of wide subtract is in the accompanying SubtractCarry *) + default [] + | Subtract (_, c, rd, rn, rm, _, _) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap fst (rd#to_lhs floc) in @@ -3516,14 +3915,50 @@ let translate_arm_instruction | ACCAlways -> default cmds | _ -> make_conditional_commands c cmds) + | SubtractCarry _ when instr#is_aggregate_anchor -> + let agg = get_aggregate loc#i in + (match agg#kind with + | ARMWideOp (WideSubtract, wop) -> + let cmds = binary_wop_cmds (fun x y -> XOp (XMinus, [x; y])) wop in + default cmds + | _ -> + begin + log_error_result + ~tag:"SubtractCarry:aggregate" + ~msg:ctxtiaddr + __FILE__ __LINE__ + ["Not recognized: " ^ (p2s agg#toPretty)]; + default [] + end) + | SubtractCarry(_, c, rd, rn, rm, _) -> let vrd = floc#env#mk_register_variable rd#to_register in let lhs_r = TR.tmap fst (rd#to_lhs floc) in let xrn_r = rn#to_expr floc in let xrm_r = rm#to_expr floc in + let xcarry = + match get_associated_test_instr finfo ctxtiaddr with + | Some (testloc, testinstr) -> + let (_, optpredicate, _opsused) = + make_conditional_predicate + ~condinstr:instr + ~testinstr + ~condloc:loc + ~testloc in + (match optpredicate with + | Some p -> p + | _ -> random_constant_expr) + | _ -> random_constant_expr in + let rhs_r = + TR.tmap2 (fun xrn xrm -> + XOp (XPlus, + [XOp (XMinus, + [XOp (XMinus, + [xrn; xrm]); int_constant_expr 1]); + xcarry])) xrn_r xrm_r in let usevars = get_register_vars [rn; rm] in let usehigh = get_use_high_vars_r [xrn_r; xrm_r] in - let cmds = floc#get_abstract_commands_r lhs_r in + let cmds = floc#get_assign_commands_r lhs_r rhs_r in let defcmds = floc#get_vardef_commands ~defs:[vrd] @@ -3750,6 +4185,9 @@ let translate_arm_instruction | UnsignedMultiplyAccumulateLong (_, c, rdlo, rdhi, rn, rm) -> let vrlo = floc#env#mk_register_variable rdlo#to_register in let vrhi = floc#env#mk_register_variable rdhi#to_register in + let rlo = rdlo#get_register in + let rhi = rdhi#get_register in + let vlohi = floc#env#mk_arm_double_register_variable rlo rhi in let lhslo_r = TR.tmap fst (rdlo#to_lhs floc) in let lhshi_r = TR.tmap fst (rdhi#to_lhs floc) in let xrn_r = rn#to_expr floc in @@ -3759,10 +4197,16 @@ let translate_arm_instruction let cmdslo = floc#get_abstract_commands_r lhslo_r in let cmdshi = floc#get_abstract_commands_r lhshi_r in let usevars = get_register_vars [rn; rm; rdlo; rdhi] in + let usedoubles = get_double_register_vars [(rdlo, rdhi)] in let usehigh = get_use_high_vars_r [xrn_r; xrm_r; xrdlo_r; xrdhi_r] in let defcmds = floc#get_vardef_commands - ~defs:[vrlo; vrhi] ~use:usevars ~usehigh ctxtiaddr in + ~defs:[vrlo; vrhi] + ~defdoubles:[vlohi] + ~use:usevars + ~usedoubles + ~usehigh + ctxtiaddr in let cmds = defcmds @ cmdslo @ cmdshi in (match c with | ACCAlways -> default cmds @@ -3771,6 +4215,9 @@ let translate_arm_instruction | UnsignedMultiplyLong (_, c, rdlo, rdhi, rn, rm) -> let vrlo = floc#env#mk_register_variable rdlo#to_register in let vrhi = floc#env#mk_register_variable rdhi#to_register in + let rlo = rdlo#get_register in + let rhi = rdhi#get_register in + let vlohi = floc#env#mk_arm_double_register_variable rlo rhi in let lhslo_r = TR.tmap fst (rdlo#to_lhs floc) in let lhshi_r = TR.tmap fst (rdhi#to_lhs floc) in let xrn_r = rn#to_expr floc in @@ -3781,7 +4228,11 @@ let translate_arm_instruction let usehigh = get_use_high_vars_r [xrn_r; xrm_r] in let defcmds = floc#get_vardef_commands - ~defs:[vrlo; vrhi] ~use:usevars ~usehigh ctxtiaddr in + ~defs:[vrlo; vrhi] + ~defdoubles:[vlohi] + ~use:usevars + ~usehigh + ctxtiaddr in let cmds = defcmds @ cmdslo @ cmdshi in (match c with | ACCAlways -> default cmds @@ -4768,6 +5219,12 @@ object (self) method translate = let faddr = f#get_address in + let finfo = get_function_info faddr in + let _ = + finfo#set_active_register_pairs + (List.map (fun (lo, hi) -> + (register_of_arm_register lo, register_of_arm_register hi)) + (f#lo_hi_registers_defined @ f#lo_hi_registers_used)) in let firstInstrLabel = make_code_label funloc#ci in let entryLabel = make_code_label ~modifier:"entry" funloc#ci in let exitLabel = make_code_label ~modifier:"exit" funloc#ci in