Predicatedinstructions

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]))
 

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"),

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

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

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].*)

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
 

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
 

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,23 +4440,28 @@ 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
      let xprxt = new arm_expression_externalizer_t self#f in
      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