Liftingarm

CodeHawk/CH/xprlib/xsimplify.ml

@@ -153,6 +153,7 @@ let rec sim_expr (m:bool) (e:xpr_t):(bool * xpr_t) =
        | XAsr -> reduce_asr m s1 s2
        | XLsl -> reduce_lsl m s1 s2
        | XBAnd -> reduce_bitwiseand m s1 s2
+       | XLAnd -> reduce_and m s1 s2
        | XDisjoint -> reduce_disjoint m s1 s2
        | XSubset -> reduce_subset m s1 s2
        | XNumJoin -> reduce_binary_numjoin m s1 s2
@@ -1091,9 +1092,14 @@ and reduce_bor m e1 e2 =
 
 and reduce_or m e1 e2 =
   let default = (m, XOp (XLOr, [e1 ; e2])) in
-  if is_true e1 || is_true e2 then (true, true_constant_expr)
-  else if is_false e1 then (true, e2)
-  else if is_false e2 then (true, e1)
+  if is_true e1 || is_true e2 then
+    (true, true_constant_expr)
+  else if is_false e1 then
+    (true, e2)
+  else if is_false e2 then
+    (true, e1)
+  else if syntactically_equal e1 e2 then
+    (true, e1)
   else match (e1,e2) with
        | (XConst XRandom, XOp (XLOr, [XConst XRandom; b]))
          | (XConst XRandom, XOp (XLOr, [b; XConst XRandom]))
@@ -1145,6 +1151,19 @@ and reduce_bitwiseand m e1 e2 =
        default
      end
 
+and reduce_and m e1 e2 =
+  let default = (m, XOp (XLAnd, [e1; e2])) in
+  if is_true e1 && is_true e2 then
+    (true, true_constant_expr)
+  else if is_true e1 then
+    (true, e2)
+  else if is_true e2 then
+    (true, e1)
+  else if syntactically_equal e1 e2 then
+    (true, e1)
+  else
+    default
+
 
 and reduce_shiftleft (m: bool) (e1: xpr_t) (e2: xpr_t): bool * xpr_t =
   let default = (m, XOp (XShiftlt, [e1; e2])) in

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -1420,6 +1420,7 @@ object (self)
        let memref_r = self#env#mk_base_variable_reference base in
        let memoff_r =
          match offset with
+         | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
          | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
          | _ ->
             Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
@@ -1497,6 +1498,7 @@ object (self)
        let memref_r = self#env#mk_base_variable_reference base in
        let memoff_r =
          match offset with
+         | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
          | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
          | _ ->
             Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
@@ -1704,7 +1706,24 @@ object (self)
              __FILE__ __LINE__
              ["x: " ^ (x2s x) ^ "; exp: " ^ (x2s exp)] in
          Ok exp in
-    aux x
+    let result = aux x in
+    match result with
+    | Ok okresult ->
+       let _ =
+         log_diagnostics_result
+           ~msg:(p2s self#l#toPretty)
+           ~tag:"convert-xpr-offsets:result"
+           __FILE__ __LINE__
+           ["x: " ^ (x2s x) ^ "; exp: " ^ (x2s okresult)] in
+       result
+    | Error e ->
+       let _ =
+         log_diagnostics_result
+           ~msg:(p2s self#l#toPretty)
+           ~tag:"convert-xpr-offsets:failure"
+           __FILE__ __LINE__
+           ["x: " ^ (x2s x) ^ "; " ^ (String.concat "; " e)] in
+       result
 
   method get_xpr_type (x: xpr_t): btype_t traceresult =
     match x with
@@ -1726,6 +1745,7 @@ object (self)
        (* let memoff_r = address_memory_offset t_unknown offset in *)
        let memoff_r =
          match offset with
+         | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
          | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
          | _ ->
             Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
@@ -1745,6 +1765,7 @@ object (self)
          let offset = simplify_xpr (XOp (XMinus, [x; num_constant_expr maxC])) in
          let gmemoff_r =
            match offset with
+           | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
            | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
            | XOp (XMult, [XConst (IntConst n); XVar v]) ->
               Ok (IndexOffset (v, n#toInt, NoOffset))
@@ -1775,6 +1796,7 @@ object (self)
              let memref_r = self#env#mk_base_variable_reference base in
              let memoff_r =
                match offset with
+               | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
                | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
                | XOp (XMult, [XConst (IntConst n); XVar v]) ->
                   Ok (IndexOffset (v, n#toInt, NoOffset))
@@ -1805,6 +1827,7 @@ object (self)
                  (fun base ->
                    let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
                    match offset with
+                   | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset
                    | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
                    | XOp (XMult, [XConst (IntConst n); XVar v]) ->
                       Ok (IndexOffset (v, n#toInt, NoOffset))
@@ -1967,6 +1990,7 @@ object (self)
             (log_error "decompose_address" "invalid memref")
             ~ok:(fun memref ->
               let offset = match xoffset with
+                | XConst (IntConst n) when n#equal numerical_zero -> NoOffset
                 | XConst (IntConst n) -> ConstantOffset (n, NoOffset)
                 | XOp (XMult, [XConst (IntConst n); XVar v]) ->
                    IndexOffset (v, n#toInt, NoOffset)
@@ -1976,6 +2000,7 @@ object (self)
             (self#env#mk_base_variable_reference v)
        | Some (XConst (IntConst n), xoffset) ->
           let offset = match xoffset with
+            | XConst (IntConst n) when n#equal numerical_zero -> NoOffset
             | XConst (IntConst n) -> ConstantOffset (n, NoOffset)
             | XOp (XMult, [XConst (IntConst n); XVar v]) ->
                IndexOffset (v, n#toInt, NoOffset)

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -765,7 +765,11 @@ object (self)
         | BaseVar v when variable_names#has v#getName#getSeqNumber ->
 	   Some (variable_names#get v#getName#getSeqNumber)
         | _ -> None in
-      let offset = ConstantOffset (offset, NoOffset) in
+      let offset =
+        if offset#equal numerical_zero then
+          NoOffset
+        else
+          ConstantOffset (offset, NoOffset) in
       let avar = varmgr#make_memory_variable ~size memref offset in
       let v = self#mk_variable avar in
       let _ = match optName with

CodeHawk/CHB/bchlib/bCHFunctionInterface.ml

@@ -1133,7 +1133,13 @@ let record_function_interface_type_constraints
         let fretvar = add_return_capability ftypevar in
         begin
           (match mk_btype_constraint fretvar returntype with
-           | Some tyc -> store#add_constraint tyc
+           | Some tyc ->
+              let _ =
+                log_diagnostics_result
+                  ~tag:("function-interface type constraint")
+                  __FILE__ __LINE__
+                  [faddr ^ ": " ^ (type_constraint_to_string tyc)] in
+              store#add_constraint tyc
            | _ -> ());
           (match fargs with
            | None ->

CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml

@@ -152,6 +152,9 @@ object (self)
 
   method is_initialized: bool = grec.gloc_is_initialized
 
+  method is_function_address: bool =
+    BCHFunctionData.functions_data#is_function_entry_point self#address
+
   method contains_address (addr: doubleword_int): bool =
     (self#address#equal addr)
     || (match self#size with

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -4332,6 +4332,7 @@ class type global_location_int =
     method is_typed: bool
     method is_struct: bool
     method is_array: bool
+    method is_function_address: bool
     method initialvalue: globalvalue_t option
     method desc: string option
     method contains_address: doubleword_int -> bool

CodeHawk/CHB/bchlib/bCHTypeConstraintGraph.ml

@@ -56,7 +56,7 @@ object (self: 'a)
      Update for constraint of type (v, c) or (c, w), v in V, c in C:
 
      tvars'(w) = tvars(w) u {c}, tvreps' = tvreps           if w = tvreps(v)
-     tvars'(w) = tvars(w), tvreps' = tvresp                 otherwise
+     tvars'(w) = tvars(w), tvreps' = tvreps                 otherwise
 
      Update for constraint of type (v1, v2), v1, v2 in V:
 

CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml

@@ -437,7 +437,6 @@ object (self)
   method resolve_reglhs_type
            (reg: register_t) (faddr: string) (iaddr: string): btype_t option =
     let evaluation = self#evaluate_reglhs_type reg faddr iaddr in
-    let logresults = iaddr = "0xffffffff" in
     let log_evaluation () =
       log_diagnostics_result
         ~tag:("reglhs resolution not successfull for " ^ faddr)
@@ -463,9 +462,17 @@ object (self)
       List.iter (fun (vars, consts) ->
           let jointy = type_constant_join consts in
           let _ =
-            if logresults then
-              log_result __FILE__ __LINE__
-                ["jointy: " ^ (type_constant_to_string jointy)] in
+            log_diagnostics_result
+              ~tag:("result of type_constant_join for " ^ faddr)
+              __FILE__ __LINE__
+              [iaddr
+               ^ ": jointy: "
+               ^ (type_constant_to_string jointy)
+               ^ " from "
+               ^ (p2s (pretty_print_list
+                         consts
+                         (fun c -> STR (type_constant_to_string c))
+                         "[" ", " "]"))] in
           List.iter (fun v ->
               let optty =
                 match jointy with

CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml

@@ -277,11 +277,6 @@ let mk_global_variable_typevar (gaddr: string): type_variable_t =
   mk_type_basevar (GlobalVariableType gaddr)
 
 
-let mk_reglhs_typevar (reg: register_t) (faddr: string) (iaddr: string)
-    : type_variable_t =
-  mk_type_basevar (RegisterLhsType (reg, faddr, iaddr))
-
-
 let mk_localstack_lhs_typevar (off: int) (faddr: string) (iaddr: string)
     : type_variable_t =
   mk_type_basevar (LocalStackLhsType (off, faddr, iaddr))
@@ -356,6 +351,15 @@ let add_stack_address_capability (offset: int) (tv: type_variable_t)
   add_capability [FLocStackAddress offset] tv
 
 
+let mk_reglhs_typevar (reg: register_t) (faddr: string) (iaddr: string)
+    : type_variable_t =
+  if iaddr = "init" then
+    let ftypevar = mk_function_typevar faddr in
+    add_freg_param_capability reg ftypevar
+  else
+    mk_type_basevar (RegisterLhsType (reg, faddr, iaddr))
+
+
 let mk_cty_term (c: type_constant_t): type_term_t = TyConstant c
 
 

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250702"
-  ~date:"2025-07-02"
+  ~version:"0.6.0_20250714"
+  ~date:"2025-07-14"
   ~licensee: None
   ~maxfilesize: None
   ()

CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml

@@ -76,6 +76,7 @@ object (self)
       instr#has_opcode_condition
       && (match instr#get_opcode with
           | Branch _ | BranchExchange _ -> false
+          | Compare _ | CompareNegative _ -> false
           | _ -> true)
       && (Option.is_none instr#is_in_aggregate) in
     begin

CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml

@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2021-2024  Aarno Labs LLC
+   Copyright (c) 2021-2025  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
@@ -211,9 +211,9 @@ let cc_expr
 
     (* ---------------------------------------------------------- Compare --- *)
 
-    | (Compare (ACCAlways, x, y, _), ACCEqual) ->
+    | (Compare (_, x, y, _), ACCEqual) ->
        (XOp (XEq, [v x; v y]), [x; y])
-    | (Compare (ACCAlways, x, y, _), ACCNotEqual) ->
+    | (Compare (_, x, y, _), ACCNotEqual) ->
        (XOp (XNe, [v x; v y]), [x; y])
 
     (* Occasionally the compiler will generate a a carryset condition for
@@ -292,19 +292,19 @@ let cc_expr
        (XOp (XLAnd, [XOp (XLt, [vu x; vu y]);
                      XOp (XGe, [vu x; zero_constant_expr])]), [x; y])
 
-    | (Compare (ACCAlways, x, y, _), ACCUnsignedHigher) ->
+    | (Compare (_, x, y, _), ACCUnsignedHigher) ->
        (XOp (XGt, [vu x; vu y]), [x; y])
-    | (Compare (ACCAlways, x, y, _), ACCNotUnsignedHigher) ->
+    | (Compare (_, x, y, _), ACCNotUnsignedHigher) ->
        (XOp (XLe, [vu x; vu y]), [x; y])
 
-    | (Compare (ACCAlways, x, y, _), ACCSignedGE) ->
+    | (Compare (_, x, y, _), ACCSignedGE) ->
        (XOp (XGe, [v x; v y]), [x; y])
-    | (Compare (ACCAlways, x, y, _), ACCSignedLT) ->
+    | (Compare (_, x, y, _), ACCSignedLT) ->
        (XOp (XLt, [v x; v y]), [x; y])
 
-    | (Compare (ACCAlways, x, y, _), ACCSignedLE) ->
+    | (Compare (_, x, y, _), ACCSignedLE) ->
        (XOp (XLe, [v x; v y]), [x; y])
-    | (Compare (ACCAlways, x, y, _), ACCSignedGT) ->
+    | (Compare (_, x, y, _), ACCSignedGT) ->
        (XOp (XGt, [v x; v y]), [x; y])
 
     | (LogicalShiftLeft (true, ACCAlways, _, x, y, _), ACCNonNegative) ->
@@ -315,7 +315,7 @@ let cc_expr
     | (CompareNegative (ACCAlways, x, y), ACCEqual) ->
        (XOp (XEq, [XOp (XPlus, [v x; v y]); zero_constant_expr]), [x; y])
 
-    | (CompareNegative (ACCAlways, x, y), ACCNotEqual) ->
+    | (CompareNegative (_, x, y), ACCNotEqual) ->
        (XOp (XNe, [XOp (XPlus, [v x; v y]); zero_constant_expr]), [x; y])
 
     | (CompareNegative (ACCAlways, x, y), ACCCarrySet) ->
@@ -516,4 +516,16 @@ let arm_conditional_conditional_expr
        condfloc#set_test_expr xpr;
        (frozenVars#toList, Some xpr, opsused)
      end
-  | _ -> (frozenVars#toList, None, opsused)
+  | _ ->
+     let _ =
+       if collect_diagnostics () then
+         ch_diagnostics_log#add
+           "unused conditional condition expression"
+           (LBLOCK [
+                STR (arm_opcode_to_string condopc);
+                STR "; ";
+                STR (arm_opcode_to_string testopc);
+                STR "; ";
+                STR (arm_opcode_to_string testtestopc)
+              ]) in
+     (frozenVars#toList, None, opsused)

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

@@ -1128,8 +1128,10 @@ object (self)
          let txpr = floc#get_test_expr in
          let fxpr = simplify_xpr (XOp (XLNot, [txpr])) in
          let csetter = floc#f#get_associated_cc_setter floc#cia in
-         let tcond = rewrite_test_expr csetter txpr in
-         let fcond = rewrite_test_expr csetter fxpr in
+         (* we can rewrite with invariants at this address, since the expression
+            should have been made position independent for local variables.*)
+         let tcond = rewrite_expr txpr in
+         let fcond = rewrite_expr fxpr in
          let ctcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) tcond in
          let cfcond_r = floc#convert_xpr_to_c_expr ~size:(Some 4) fcond in
          let csetter_addr_r = string_to_doubleword csetter in
@@ -2193,6 +2195,7 @@ object (self)
          let vrd_r = rd#to_variable floc in
          let xrm_r = rm#to_expr floc in
          let result_r = TR.tmap (rewrite_expr ?restrict:(Some 4)) xrm_r in
+         let result_r = TR.tmap (rewrite_in_cc_context floc c) result_r in
          let cresult_r =
            TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) result_r in
          let rdefs = (get_rdef_r xrm_r) :: (get_all_rdefs_r result_r) in