Reachingdefinitions

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -1499,7 +1499,7 @@ object (self)
        | XConst (IntConst n)
             when n#equal (mkNumerical 0xffffffff) && is_int t ->
           Ok (int_constant_expr (-1))
-       | _ -> self#convert_xpr_offsets ~size x
+       | _ -> self#convert_xpr_offsets ~xtype ~size x
 
   method convert_addr_to_c_pointed_to_expr
            ?(size=None) ?(xtype=None) (a: xpr_t): xpr_t traceresult =
@@ -1656,12 +1656,13 @@ object (self)
 
 
   method convert_variable_offsets
-           ?(size=None) (v: variable_t): variable_t traceresult =
+           ?(vtype=None) ?(size=None) (v: variable_t): variable_t traceresult =
     if self#env#is_basevar_memory_variable v then
       let basevar_r = self#env#get_memvar_basevar v in
       let offset_r = self#env#get_memvar_offset v in
       let cbasevar_r = TR.tbind self#convert_value_offsets basevar_r in
       let basetype_r = TR.tbind self#get_variable_type cbasevar_r in
+      let optvtype = match vtype with Some t -> t | _ -> t_unknown in
       let tgttype_r =
         TR.tbind
           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
@@ -1682,8 +1683,18 @@ object (self)
                  ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
                  (fun tgttype ->
                    address_memory_offset
-                     ~tgtsize:size tgttype (num_constant_expr n)) tgttype_r
+                     ~tgtbtype:optvtype ~tgtsize:size tgttype (num_constant_expr n))
+                 tgttype_r
             | _ -> Ok offset) offset_r in
+      let _ =
+        log_diagnostics_result
+          ~msg:(p2s self#l#toPretty)
+          ~tag:"convert-variable-offsets"
+          __FILE__ __LINE__
+          ["tgttype: " ^ (TR.tfold_default btype_to_string "?" tgttype_r);
+           "tgtbtype: " ^ (btype_to_string optvtype);
+           "offset : " ^ (TR.tfold_default memory_offset_to_string "?" offset_r);
+           "coffset: " ^ (TR.tfold_default memory_offset_to_string "?" coffset_r)] in
       TR.tbind
         ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty))
         (fun cbasevar ->
@@ -1776,7 +1787,8 @@ object (self)
           ["v: " ^ (p2s v#toPretty)] in
       Ok v
 
-  method convert_xpr_offsets ?(size=None) (x: xpr_t): xpr_t traceresult =
+  method convert_xpr_offsets
+           ?(xtype=None) ?(size=None) (x: xpr_t): xpr_t traceresult =
     let rec aux exp =
       match exp with
       | XVar v when self#env#is_basevar_memory_value v ->
@@ -1789,10 +1801,16 @@ object (self)
            ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
            (fun v -> XVar v) (self#convert_variable_offsets ~size v)
       | XOp ((Xf "addressofvar"), [XVar v]) ->
+         let derefty =
+           match xtype with
+           | None -> None
+           | Some (TPtr (ty, _)) -> Some ty
+           | _ -> None in
          let newx_r =
            TR.tmap
              ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
-             (fun v -> XVar v) (self#convert_variable_offsets ~size v) in
+             (fun v ->
+               XVar v) (self#convert_variable_offsets ~vtype:derefty ~size v) in
          TR.tmap
            (fun newx ->
              match newx with

CodeHawk/CHB/bchlib/bCHFunctionData.ml

@@ -28,6 +28,7 @@
    ============================================================================= *)
 
 (* chlib *)
+open CHLanguage
 open CHPretty
 
 (* chutil *)
@@ -50,6 +51,7 @@ open BCHLibTypes
 module H = Hashtbl
 module TR = CHTraceResult
 
+let p2s = CHPrettyUtil.pretty_to_string
 
 let bd = BCHDictionary.bdictionary
 
@@ -76,10 +78,41 @@ let stackvar_intro_to_string (svi: stackvar_intro_t) =
   (string_of_int svi.svi_offset) ^ ": " ^ svi.svi_name ^ ptype
 
 
+let reachingdef_spec_to_string (rds: reachingdef_spec_t) =
+  let uselocs = "[" ^ (String.concat ", " rds.rds_uselocs) ^ "]" in
+  let rdeflocs =  "[" ^ (String.concat ", " rds.rds_rdeflocs) ^ "]" in
+  rds.rds_variable ^ ": use: " ^ uselocs ^ "; remove-rdefs: " ^ rdeflocs
+
+
 let function_annotation_to_string (a: function_annotation_t) =
-  (String.concat "\n" (List.map regvar_intro_to_string a.regvarintros))
-  ^ "\n"
-  ^ (String.concat "\n" (List.map stackvar_intro_to_string a.stackvarintros))
+  let rvintros =
+    if (List.length a.regvarintros) > 0 then
+      ("Register-variable-introductions: ["
+       ^ (String.concat "; " (List.map regvar_intro_to_string a.regvarintros))
+       ^ "]")
+    else
+      "" in
+  let svintros =
+    if (List.length a.stackvarintros) > 0 then
+      ("Stack-variable-introductions: ["
+       ^ (String.concat "; " (List.map stackvar_intro_to_string a.stackvarintros))
+       ^ "]")
+    else
+      "" in
+  let rdefspecs =
+    if (List.length a.reachingdefspecs) > 0 then
+      ("Reaching-def-specs: ["
+       ^ (String.concat "; " (List.map reachingdef_spec_to_string a.reachingdefspecs))
+       ^ "]")
+    else
+      "" in
+  List.fold_left (fun acc s ->
+      if s = "" then
+        acc
+      else if acc = "" then
+        s
+      else
+        acc ^ "\n" ^ s) "" [rvintros; svintros; rdefspecs]
 
 
 class function_data_t (fa:doubleword_int) =
@@ -156,7 +189,8 @@ object (self)
       functionannotation <- Some a;
       chlog#add
         "function annotation"
-        (LBLOCK [faddr#toPretty; NL; STR (function_annotation_to_string a)])
+        (LBLOCK [STR "function "; faddr#toPretty; STR ": ";
+                 STR (function_annotation_to_string a)])
     end
 
   method has_function_annotation: bool =
@@ -314,6 +348,36 @@ object (self)
        else
          BCHSystemSettings.system_settings#is_typing_rule_enabled name
 
+  method filter_deflocs
+           (iaddr: string) (v: variable_t) (deflocs: symbol_t list): symbol_t list =
+    match self#get_function_annotation with
+    | None -> deflocs
+    | Some a when (List.length a.reachingdefspecs) > 0 ->
+       let vname = v#getName#getBaseName in
+       let deflocs =
+         List.fold_left
+           (fun acc sym ->
+             let symname = sym#getBaseName in
+             if (List.fold_left
+                   (fun filteracc rds ->
+                     filteracc ||
+                       (if rds.rds_variable = vname then
+                          (List.mem iaddr rds.rds_uselocs)
+                          && (List.mem symname rds.rds_rdeflocs)
+                        else
+                          false)) false a.reachingdefspecs) then
+               let _ =
+                 log_result
+                   ~msg:("iaddr: " ^ iaddr)
+                   ~tag:"filter out reaching def"
+                   __FILE__ __LINE__
+                   ["v: " ^ (p2s v#toPretty); "s; " ^ symname] in
+               acc
+             else
+               sym :: acc) [] deflocs in
+       List.rev deflocs
+    | _ -> deflocs
+
   method add_inlined_block (baddr:doubleword_int) =
     inlined_blocks <- baddr :: inlined_blocks
 
@@ -645,6 +709,28 @@ let read_xml_typing_rule (node: xml_element_int): typing_rule_t traceresult =
         tra_locations = locs}
 
 
+let read_xml_reachingdef_spec
+      (node: xml_element_int): reachingdef_spec_t traceresult =
+  let get = node#getAttribute in
+  let has = node#hasNamedAttribute in
+  if not (has "var") then
+    Error ["rdefspec without var"]
+  else if not (has "uselocs") then
+    Error ["rdefspec without uselocs"]
+  else if not (has "rdeflocs") then
+    Error ["rdefspec without rdeflocs"]
+  else
+    let var = get "var" in
+    let uselocs = get "uselocs" in
+    let uselocs = String.split_on_char ','  uselocs in
+    let rdeflocs = get "rdeflocs" in
+    let rdeflocs = String.split_on_char ',' rdeflocs in
+    Ok {rds_variable = var;
+        rds_uselocs = uselocs;
+        rds_rdeflocs = rdeflocs
+      }
+
+
 let read_xml_function_annotation (node: xml_element_int) =
   let get = node#getAttribute in
   let getc = node#getTaggedChild in
@@ -705,10 +791,29 @@ let read_xml_function_annotation (node: xml_element_int) =
               (trules#getTaggedChildren "typingrule")
           else
             [] in
+        let rdefspecs =
+          if hasc "remove-rdefs" then
+            let rrds = getc "remove-rdefs" in
+            List.fold_left
+              (fun acc n ->
+                TR.tfold
+                  ~ok:(fun rds -> rds :: acc)
+                  ~error:(fun e ->
+                    begin
+                      log_error_result __FILE__ __LINE__ e;
+                      acc
+                    end)
+                  (read_xml_reachingdef_spec n))
+              []
+              (rrds#getTaggedChildren "remove-var-rdefs")
+          else
+            [] in
         fndata#set_function_annotation
           {regvarintros = regvintros;
            stackvarintros = stackvintros;
-          typingrules = typingrules}
+           typingrules = typingrules;
+           reachingdefspecs = rdefspecs
+          }
       else
         log_error_result
           ~tag:"function annotation faddr not found"

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -1718,6 +1718,11 @@ object (self)
   method add_reaching_def
            (iaddr: string) (v: variable_t) (deflocs: symbol_t list) =
     begin
+      let deflocs =
+        if fndata#has_function_annotation then
+          fndata#filter_deflocs iaddr v deflocs
+        else
+          deflocs in
       self#fvarinv#add_reaching_def iaddr v deflocs;
       List.iter (fun s ->
           if (List.length s#getAttributes) = 0 then

CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml

@@ -198,6 +198,18 @@ object (self)
                    ~(tgtbtype: btype_t option)
                    (c: bcompinfo_t)
                    (xoffset: xpr_t): memory_offset_t traceresult =
+    let _ =
+      log_diagnostics_result
+        ~tag:"global:get-field-memory-offset-at"
+        __FILE__ __LINE__
+        ["tgtsize: "
+         ^ (if Option.is_some tgtsize then
+              string_of_int (Option.get tgtsize) else "?");
+         "tgtbtype: "
+         ^ (if Option.is_some tgtbtype then
+              btype_to_string (Option.get tgtbtype) else "?");
+         "compinfo: " ^ c.bcname;
+         "xoffset: " ^ (x2s xoffset)] in
     let is_void_tgtbtype =
       match tgtbtype with
       | Some (TVoid _) -> true
@@ -368,6 +380,20 @@ object (self)
                    ~(tgtbtype: btype_t option)
                    (btype: btype_t)
                    (xoffset: xpr_t): memory_offset_t traceresult =
+    let _ =
+      log_diagnostics_result
+        ~tag:"global:arrayvar-memory-offset"
+        __FILE__ __LINE__
+        ["tgtsize: " ^ (if (Option.is_some tgtsize) then
+                          string_of_int (Option.get tgtsize)
+                        else
+                          "?");
+         "tgtbtype: " ^ (if (Option.is_some tgtbtype) then
+                           btype_to_string (Option.get tgtbtype)
+                         else
+                           "?");
+         "btype: " ^ (btype_to_string btype);
+         "xoffset: " ^ (x2s xoffset)] in
     let iszero x =
       match x with
       | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -1518,11 +1518,18 @@ type typing_rule_t = {
     tra_locations: string list
   }
 
+type reachingdef_spec_t = {
+    rds_variable: string;
+    rds_uselocs: string list;
+    rds_rdeflocs: string list
+  }
+
 
 type function_annotation_t = {
     regvarintros: regvar_intro_t list;
     stackvarintros: stackvar_intro_t list;
-    typingrules: typing_rule_t list
+    typingrules: typing_rule_t list;
+    reachingdefspecs: reachingdef_spec_t list
   }
 
 class type function_data_int =
@@ -1575,6 +1582,7 @@ class type function_data_int =
     method has_regvar_type_cast: doubleword_int -> bool
     method has_stackvar_type_annotation: int -> bool
     method has_stackvar_type_cast: int -> bool
+    method filter_deflocs: string -> variable_t -> symbol_t list -> symbol_t list
     method is_typing_rule_enabled: ?rdef:string option -> string -> string -> bool
     method has_class_info: bool
     method has_callsites: bool
@@ -6102,9 +6110,13 @@ class type floc_int =
              ?size:int option -> variable_t -> variable_t traceresult
 
     method convert_variable_offsets:
-             ?size:int option -> variable_t -> variable_t traceresult
+             ?vtype:btype_t option
+             -> ?size:int option
+             -> variable_t
+             -> variable_t traceresult
 
-    method convert_xpr_offsets: ?size:int option -> xpr_t -> xpr_t traceresult
+    method convert_xpr_offsets:
+             ?xtype:btype_t option -> ?size:int option -> xpr_t -> xpr_t traceresult
 
     (* returns the variable associated with the address expression *)
     method get_lhs_from_address: xpr_t -> variable_t

CodeHawk/CHB/bchlib/bCHMemoryReference.ml

@@ -256,7 +256,23 @@ and structvar_memory_offset
 ~(tgtbtype: btype_t option)
 (btype: btype_t)
 (xoffset: xpr_t): memory_offset_t traceresult =
+  let _ =
+    log_diagnostics_result
+      ~tag:"structvar-memory-offset"
+      __FILE__ __LINE__
+      ["tgtsize: "
+       ^ (if Option.is_some tgtsize then (string_of_int (Option.get tgtsize)) else "?");
+       "tgtbtype: "
+       ^ (if Option.is_some tgtbtype then (btype_to_string (Option.get tgtbtype))
+          else "?");
+       "btype: " ^ (btype_to_string btype);
+       "xoffset: " ^ (x2s xoffset)] in
   match xoffset with
+  | XConst (IntConst n)
+       when n#equal numerical_zero
+            && (Option.is_some tgtbtype)
+            && (btype_equal (Option.get tgtbtype) btype) ->
+     Ok NoOffset
   | XConst (IntConst _) ->
      if is_struct_type btype then
        let compinfo = get_struct_type_compinfo btype in

CodeHawk/CHB/bchlib/bCHSystemSettings.ml

@@ -59,6 +59,7 @@ let _ =
       ("ADD-c", "enable");
       ("AND-rdef", "enable");      
       ("ASR-rdef", "enable");
+      ("BXLR-rdef", "enable");
       ("CMP-rdef", "enable");
       ("LSL_rdef", "enable");
       ("LSR_rdef", "enable");
@@ -111,6 +112,7 @@ let _ =
       ("BL-sig-regarg", "enable");
       ("BL-sig-stackarg", "enable");
       ("BL-sig-rv", "enable");
+      ("BXLR-sig-rv", "enable");
       ("LDR-array", "enable");
       ("LDR-memop-tc", "enable");
       ("LDR-stack-addr", "enable");

CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml

@@ -443,8 +443,7 @@ let rec mk_btype_constraint (tv: type_variable_t) (ty: btype_t)
      | TComp (key, _) ->
         let cinfo = bcfiles#get_compinfo key in
         Some (TyGround (TyVariable tv, TyConstant (TyTStruct (key, cinfo.bcname))))
-     | TPtr (TVoid _, _) ->
-        Some (TyGround (TyVariable tv, TyConstant TyVoidPtr))
+     | TPtr (TVoid _, _) -> None
      | TPtr (pty, _) ->
         let ptv = add_deref_capability tv in
         mk_btype_constraint ptv pty

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250805"
-  ~date:"2025-08-05"
+  ~version:"0.6.0_20250810"
+  ~date:"2025-08-10"
   ~licensee: None
   ~maxfilesize: None
   ()