static-analysis-engineering · sipma · Aug 22, 2025 · Aug 22, 2025 · Aug 22, 2025
diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
@@ -90,15 +90,13 @@ let x2p = xpr_formatter#pr_expr
 let p2s = pretty_to_string
 let x2s x = p2s (x2p x)
 
-let opt_size_to_string (s: int option) =
-  match s with
-  | Some i -> "size:" ^ (string_of_int i)
-  | _ -> "size:None"
+let opti2s (i: int option) =
+  if Option.is_some i then string_of_int (Option.get i) else "?"
 
-let opt_type_to_string (t: btype_t option) =
-  match t with
-  | Some t -> "btype:" ^ (btype_to_string t)
-  | _ -> "btype:None"
+let _ty2s (ty: btype_t) =
+  if is_unknown_type ty then "?" else btype_to_string ty
+let optty2s (ty: btype_t option) =
+  if Option.is_some ty then btype_to_string (Option.get ty) else "?"
 
 
 let log_error (tag: string) (msg: string): tracelogspec_t =
@@ -665,6 +663,14 @@ object (self)
            ?(size=4)
            (var: variable_t)
            (numoffset: numerical_t): variable_t traceresult =
+    let _ =
+      log_diagnostics_result
+        ~msg:(p2s self#l#toPretty)
+        ~tag:"get-memory-variable-numoffset"
+        __FILE__ __LINE__
+        ["size: " ^ (string_of_int size);
+         "var: " ^ (p2s var#toPretty);
+         "numoffset: " ^ (numoffset#toString)] in
     let inv = self#inv in
     let mk_memvar memref_r memoffset_r =
       let _ =
@@ -1512,9 +1518,9 @@ object (self)
         ~msg:(p2s self#l#toPretty)
         ~tag:"convert_xpr_to_c_expr"
         __FILE__ __LINE__
-        [(opt_size_to_string size) ^ "; "
-         ^ (opt_type_to_string xtype) ^ "; "
-         ^ "x: " ^ (x2s x)] in
+        ["size: " ^ (opti2s size);
+         "xtype: " ^ (optty2s xtype);
+         "x: " ^ (x2s x)] in
     match xtype with
     | None -> self#convert_xpr_offsets ~size x
     | Some t ->
@@ -1598,8 +1604,8 @@ object (self)
        TR.tmap (fun v -> XVar v) var_r
     | _ ->
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-              ^ (opt_size_to_string size) ^ "; "
-              ^ (opt_type_to_string xtype) ^ "; "
+              ^ "size: " ^ (opti2s size) ^ "; "
+              ^ "type: " ^ (optty2s xtype) ^ "; "
               ^ "addr: " ^ (x2s a)
               ^ ": Not yet handled"]
 
@@ -1609,8 +1615,8 @@ object (self)
     | None -> self#convert_variable_offsets ~size v
     | _ ->
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-              ^ (opt_size_to_string size) ^ "; "
-              ^ (opt_type_to_string vtype) ^ "; "
+              ^ "size: " ^ (opti2s size) ^ "; "
+              ^ "type: " ^ (optty2s vtype) ^ "; "
               ^ "v: " ^ (p2s v#toPretty)
               ^ ": Not yet implemented"]
 
@@ -1672,14 +1678,22 @@ object (self)
          memref_r memoff_r
     | _ ->
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-              ^ (opt_size_to_string size) ^ "; "
-              ^ (opt_type_to_string vtype) ^ "; "
+              ^ "size: " ^ (opti2s size) ^ "; "
+              ^ "vtype: " ^ (optty2s vtype) ^ "; "
               ^ "addr: " ^ (x2s a)
               ^ ": Not yet handled"]
 
 
   method convert_variable_offsets
            ?(vtype=None) ?(size=None) (v: variable_t): variable_t traceresult =
+    let _ =
+      log_diagnostics_result
+        ~msg:(p2s self#l#toPretty)
+        ~tag:"convert-variable-offsets"
+        __FILE__ __LINE__
+        ["vtype: " ^ (optty2s vtype);
+         "size: " ^ (opti2s size);
+         "v: " ^ (p2s v#toPretty)] in
     if self#env#is_basevar_memory_variable v then
       let basevar_r = self#env#get_memvar_basevar v in
       let offset_r = self#env#get_memvar_offset v in
@@ -1737,6 +1751,12 @@ object (self)
 
   method convert_value_offsets
            ?(size=None) (v: variable_t): variable_t traceresult =
+    let _ =
+      log_diagnostics_result
+        ~msg:(p2s self#l#toPretty)
+        ~tag:"convert-value-offsets"
+        __FILE__ __LINE__
+        ["size: " ^ (opti2s size); "v: " ^ (p2s v#toPretty)] in
     if self#env#is_basevar_memory_value v then
       let basevar_r = self#env#get_memval_basevar v in
       let offset_r = self#env#get_memval_offset v in
@@ -1812,6 +1832,12 @@ object (self)
 
   method convert_xpr_offsets
            ?(xtype=None) ?(size=None) (x: xpr_t): xpr_t traceresult =
+    let _ =
+      log_diagnostics_result
+        ~msg:(p2s self#l#toPretty)
+        ~tag:"convert-xpr-offsets"
+        __FILE__ __LINE__
+        ["xtype: " ^ (optty2s xtype); "size: " ^ (opti2s size); "x: " ^ (x2s x)] in
     let rec aux exp =
       match exp with
       | XVar v when self#env#is_basevar_memory_value v ->
@@ -2349,41 +2375,51 @@ object (self)
               rhs
          | _ -> rhs in
 
-       let rhs =
-         (* if rhs is a composite symbolic expression, create a new variable
+       if self#f#env#is_global_variable lhs then
+         let _ =
+           log_diagnostics_result
+             ~msg:(p2s self#l#toPretty)
+             ~tag:("get_assign_cmds_r: abstract global variable")
+             __FILE__ __LINE__
+             ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s rhs)] in
+         [ABSTRACT_VARS [lhs]]
+
+       else
+         let rhs =
+           (* if rhs is a composite symbolic expression, create a new variable
             for it *)
-         if self#is_composite_symbolic_value rhs then
-           XVar (self#env#mk_symbolic_value rhs)
-         else
-           rhs in
-       let reqN () = self#env#mk_num_temp in
-       let reqC = self#env#request_num_constant in
-       let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in
-       let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in
-       let fndata = self#f#get_function_data in
-       match fndata#get_regvar_intro self#ia with
-       | Some rvi when rvi.rvi_cast && Option.is_some rvi.rvi_vartype ->
-          TR.tfold
-            ~ok:(fun reg ->
-              let ty = Option.get rvi.rvi_vartype in
-              let tcvar =
-                self#f#env#mk_typecast_value self#cia rvi.rvi_name ty reg in
-              begin
-                log_result __FILE__ __LINE__
-                  ["Create typecast var for "
-                   ^ (register_to_string reg)
-                   ^ " at "
-                   ^ self#cia];
-                cmds @ [ASSIGN_NUM (lhs, NUM_VAR tcvar)]
-              end)
-            ~error:(fun e ->
-              begin
-                log_error_result __FILE__ __LINE__
-                  ("expected a register variable" :: e);
-                cmds
-              end)
-            (self#f#env#get_register lhs)
-       | _ -> cmds
+           if self#is_composite_symbolic_value rhs then
+             XVar (self#env#mk_symbolic_value rhs)
+           else
+             rhs in
+         let reqN () = self#env#mk_num_temp in
+         let reqC = self#env#request_num_constant in
+         let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in
+         let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in
+         let fndata = self#f#get_function_data in
+         match fndata#get_regvar_intro self#ia with
+         | Some rvi when rvi.rvi_cast && Option.is_some rvi.rvi_vartype ->
+            TR.tfold
+              ~ok:(fun reg ->
+                let ty = Option.get rvi.rvi_vartype in
+                let tcvar =
+                  self#f#env#mk_typecast_value self#cia rvi.rvi_name ty reg in
+                begin
+                  log_result __FILE__ __LINE__
+                    ["Create typecast var for "
+                     ^ (register_to_string reg)
+                     ^ " at "
+                     ^ self#cia];
+                  cmds @ [ASSIGN_NUM (lhs, NUM_VAR tcvar)]
+                end)
+              ~error:(fun e ->
+                begin
+                  log_error_result __FILE__ __LINE__
+                    ("expected a register variable" :: e);
+                  cmds
+                end)
+              (self#f#env#get_register lhs)
+         | _ -> cmds
 
    (* Note: recording of loads and stores is performed by the different
       architectures directly in FnXXXDictionary.*)
@@ -2448,6 +2484,15 @@ object (self)
        [OPERATION ({ op_name = unknown_write_symbol; op_args = op_args});
 	ASSIGN_NUM (lhs, rhs)]
 
+     else if self#f#env#is_global_variable lhs then
+       let _ =
+         log_diagnostics_result
+           ~msg:(p2s self#l#toPretty)
+           ~tag:("get_assign_cmds: abstract global variable")
+           __FILE__ __LINE__
+           ["lhs: " ^ (p2s lhs#toPretty); "rhs: " ^ (x2s rhs_expr)] in
+       [ABSTRACT_VARS [lhs]]
+
      else
        rhsCmds @ [ASSIGN_NUM (lhs, rhs)]
 

diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
@@ -851,29 +851,23 @@ object (self)
        let gvar =
          self#mk_variable
            (self#varmgr#make_global_variable gloc#address#to_numerical) in
-       let ivar = self#mk_variable (varmgr#make_initial_memory_value gvar) in
-       if dw#equal gloc#address then
-         begin
-           self#set_variable_name gvar gloc#name;
-           self#set_variable_name ivar (gloc#name ^ "_in");
-           Ok gvar
-         end
-       else
-         tmap
-           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
-           (fun offset ->
-             let gvar =
-               self#mk_variable
-                 (self#varmgr#make_global_variable
-                    ~size ~offset gloc#address#to_numerical) in
-             let ivar = self#mk_variable (varmgr#make_initial_memory_value gvar) in
-             let name = gloc#name ^ (memory_offset_to_string offset) in
-             begin
-               self#set_variable_name gvar name;
-               self#set_variable_name ivar (name ^ "_in");
-               gvar
-             end)
-           (gloc#address_memory_offset ~tgtbtype:btype loc (num_constant_expr base))
+       let _ivar = self#mk_variable (varmgr#make_initial_memory_value gvar) in
+       tmap
+         ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global")
+         (fun offset ->
+           let gvar =
+             self#mk_variable
+               (self#varmgr#make_global_variable
+                  ~size ~offset gloc#address#to_numerical) in
+           let ivar = self#mk_variable (varmgr#make_initial_memory_value gvar) in
+           let name = gloc#name ^ (memory_offset_to_string offset) in
+           begin
+             self#set_variable_name gvar name;
+             self#set_variable_name ivar (name ^ "_in");
+             gvar
+           end)
+         (gloc#address_memory_offset
+            ~tgtsize:(Some size) ~tgtbtype:btype loc (num_constant_expr base))
     | _ ->
        let _ = memmap#add_location ~size:(Some size) ~btype dw in
        Ok (self#mk_variable (self#varmgr#make_global_variable dw#to_numerical))
@@ -1223,6 +1217,9 @@ object (self)
   method get_memval_offset (v:variable_t): memory_offset_t traceresult =
     varmgr#get_memval_offset v
 
+  method get_memvar_dependencies (v: variable_t): variable_t list =
+    varmgr#get_memvar_dependencies v
+
   method get_constant_offsets (v: variable_t): numerical_t list traceresult =
     let offset_r =
       if self#is_initial_memory_value v then

diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -3618,6 +3618,8 @@ object ('a)
       Returns [Error] if this variable is not a register variable. *)
   method get_register: register_t traceresult
 
+  method get_memvar_dependencies: variable_t list
+
   (** Returns the memory reference associated with this memory variable.
 
       Returns [Error] if this variable is not a memory variable. *)
@@ -4063,6 +4065,8 @@ object
       initial-value memory variable. *)
   method get_initial_memory_value_variable: variable_t -> variable_t traceresult
 
+  method get_memvar_dependencies: variable_t -> variable_t list
+
 
   (** {2 Memory offsets} *)
 
@@ -4944,6 +4948,8 @@ class type function_environment_int =
 
     method has_variable_index_offset: variable_t -> bool
 
+    method get_memvar_dependencies: variable_t -> variable_t list
+
 
     (** {2 Memory offsets} *)
 

diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml
@@ -155,6 +155,16 @@ object (self:'a)
     else
       name
 
+  method get_memvar_dependencies: variable_t list =
+    match denotation with
+    | MemoryVariable (_, _, offset) ->
+       (match offset with
+        | ArrayIndexOffset (x, _) -> Xprt.variables_in_expr x
+        | BasePtrArrayIndexOffset (x, _) -> Xprt.variables_in_expr x
+        | ConstantOffset (_, ArrayIndexOffset (x, _)) -> Xprt.variables_in_expr x
+        | _ -> [])
+    | _ -> []
+
   method private get_memref_type (index: int) (_size: int): btype_t option =
     memrefmgr#get_memory_reference_type index
 
@@ -562,6 +572,12 @@ object (self)
       None
       (self#get_variable v)
 
+  method get_memvar_dependencies (v: variable_t): variable_t list =
+    tfold_default
+      (fun var -> var#get_memvar_dependencies)
+      []
+      (self#get_variable v)
+
   method get_memvar_reference (v: variable_t): memory_reference_int traceresult =
     tbind
       ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty))

diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250821"
-  ~date:"2025-08-21"
+  ~version:"0.6.0_20250822"
+  ~date:"2025-08-22"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
@@ -2552,13 +2552,12 @@ let translate_arm_instruction
              TR.tfold
                ~ok:(fun rhsvar ->
                  let rhsreg = TR.tget_ok (finfo#env#get_register rhsvar) in
-                 let _ =
-                   if floc#has_initial_value rhsvar then
-                     finfo#stackframe#add_register_spill
-                       ~offset:off rhsreg floc#cia in
                  let stackop = arm_sp_deref ~with_offset:off WR in
                  TR.tfold
                    ~ok:(fun (stacklhs, stacklhscmds) ->
+                     let _ =
+                       if floc#has_initial_value rhsvar then
+                         finfo#save_register stacklhs floc#cia rhsreg in
                      let rhsexpr = rewrite_expr floc (XVar rhsvar) in
                      let cmds1 = floc#get_assign_commands stacklhs rhsexpr in
                      let usehigh = get_use_high_vars [rhsexpr] in
@@ -3172,7 +3171,24 @@ let translate_arm_instruction
        TR.tfold
          ~ok:(fun (memlhs, memcmds) ->
            let cmds = floc#get_assign_commands_r (Ok memlhs) xrt_r in
-           let defcmds = floc#get_vardef_commands ~defs:[memlhs] ctxtiaddr in
+           let memvardeps = floc#f#env#get_memvar_dependencies memlhs in
+           let usehigh =
+             List.filter (fun v -> not (floc#f#env#is_function_initial_value v))
+               memvardeps in
+           let _ =
+             log_diagnostics_result
+               ~msg:(p2s floc#l#toPretty)
+               ~tag:"translate memlhs storeregister"
+               __FILE__ __LINE__
+               ["memlhs: " ^ (p2s memlhs#toPretty);
+                "memvardeps: "
+                ^ (String.concat
+                     ", " (List.map (fun v -> p2s v#toPretty) memvardeps));
+                "usehigh: "
+                ^ (String.concat
+                     ", " (List.map (fun v -> p2s v#toPretty) usehigh))] in
+           let defcmds =
+             floc#get_vardef_commands ~defs:[memlhs] ~usehigh ctxtiaddr in
            memcmds @ cmds @ defcmds)
          ~error:(fun e ->
            let xrn_r = rn#to_expr floc in