CHB: add more functionality for handling stack variables

Author: sipma

CodeHawk/CHB/bchlib/bCHCPURegisters.ml

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2020 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   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
@@ -864,3 +864,10 @@ let index_to_byte_register (index:int) =
   | 6 -> Dh
   | 7 -> Bh
   | _ -> raise (Invalid_argument ("index_to_byte_register with " ^ (string_of_int index)))
+
+
+let is_temporary_register (reg: register_t): bool =
+  match reg with
+  | ARMRegister r -> List.mem r arm_temporaries
+  | MIPSRegister r -> List.mem r mips_temporaries
+  | _ -> false

CodeHawk/CHB/bchlib/bCHCPURegisters.mli

@@ -6,7 +6,7 @@
 
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020      Henny Sipma
-   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
@@ -156,6 +156,9 @@ val is_stackpointer_register: register_t -> bool
 
 val is_register: string -> bool
 
+val is_temporary_register: register_t -> bool
+
+
 (** {2 x86}*)
 
 val byte_reg_of_reg : cpureg_t -> cpureg_t       (* raises Invalid_argument *)

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -878,6 +878,7 @@ object (self)
        Ok (self#mk_variable (self#varmgr#make_global_variable dw#to_numerical))
 
   method mk_stack_variable
+           ?(size=4)
            (stackframe: stackframe_int)
            (offset: numerical_t): variable_t traceresult =
     match stackframe#containing_stackslot offset#toInt with
@@ -894,7 +895,8 @@ object (self)
              self#set_variable_name svar name;
              svar
            end)
-         (stackslot#frame_offset_memory_offset (num_constant_expr offset))
+         (stackslot#frame_offset_memory_offset
+            ~tgtsize:(Some size) (num_constant_expr offset))
     | _ ->
        Error [
            __FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
@@ -1803,34 +1805,37 @@ object (self)
    * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
 
   method save_register
-           (vmem: variable_t) (iaddr:ctxt_iaddress_t) (reg:register_t) =
-    if self#env#is_stack_variable vmem then
-      TR.tfold
-        ~ok:(fun offset ->
-          match offset with
-          | ConstantOffset (n, NoOffset) ->
-             self#stackframe#add_register_spill ~offset:n#toInt reg iaddr
-          | _ ->
-             log_error_result
-               ~msg:"save_register:not a constant offset"
-               __FILE__ __LINE__
-               ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
-                (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)
-                ^ " and offset " ^ (memory_offset_to_string offset)])
-        ~error:(fun e ->
-          log_error_result
-            ~msg:"save_register"
-            __FILE__ __LINE__
-            (["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
-              (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] @ e))
-        (self#env#get_memvar_offset vmem)
+           (vmem: variable_t) (iaddr: ctxt_iaddress_t) (reg: register_t) =
+    if BCHCPURegisters.is_temporary_register reg then
+      ()
     else
-      log_error_result
-        ~msg:"save register:not a stack variable"
-        __FILE__ __LINE__
-        ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
-         "not a stack variable: "
-         ^ (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)]
+      if self#env#is_stack_variable vmem then
+        TR.tfold
+          ~ok:(fun offset ->
+            match offset with
+            | ConstantOffset (n, NoOffset) ->
+               self#stackframe#add_register_spill ~offset:n#toInt reg iaddr
+            | _ ->
+               log_error_result
+                 ~msg:"save_register:not a constant offset"
+                 __FILE__ __LINE__
+                 ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
+                  (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)
+                  ^ " and offset " ^ (memory_offset_to_string offset)])
+          ~error:(fun e ->
+            log_error_result
+              ~msg:"save_register"
+              __FILE__ __LINE__
+              (["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
+                (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] @ e))
+          (self#env#get_memvar_offset vmem)
+      else
+        log_error_result
+          ~msg:"save register:not a stack variable"
+          __FILE__ __LINE__
+          ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): ";
+           "not a stack variable: "
+           ^ (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)]
 
   method restore_register
            (memaddr: xpr_t) (iaddr:ctxt_iaddress_t) (reg:register_t) =

CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml

@@ -102,7 +102,12 @@ object (self)
     | Ok (TArray _) -> true
     | _ -> false
 
-  method size = sslot.sslot_size
+  method is_scalar: bool =
+    match resolve_type self#btype with
+    | Ok t -> is_scalar t
+    | _ -> false
+
+  method size: int option = sslot.sslot_size
 
   method desc = sslot.sslot_desc
 
@@ -137,7 +142,9 @@ object (self)
            ?(tgtbtype=t_unknown)
            (xoffset: xpr_t): memory_offset_t traceresult =
     match xoffset with
-    | XConst (IntConst n) when n#equal CHNumerical.numerical_zero ->
+    | XConst (IntConst n)
+         when n#equal CHNumerical.numerical_zero
+              && (not self#is_typed || self#is_scalar) ->
        Ok NoOffset
     | XConst (IntConst n) when not self#is_typed ->
        Ok (ConstantOffset (n, NoOffset))
@@ -234,6 +241,31 @@ object (self)
       match tgtsize with
       | Some s -> string_of_int s
       | _ -> "?" in
+    let check_tgttype_compliance (t: btype_t) (s: int) =
+      match tgtsize, tgtbtype with
+      | None, None -> true
+      | Some size, None -> size = s
+      | Some size, Some (TVoid _) -> size = s
+      | None, Some (TVoid _) -> true
+      | None, Some ty -> btype_equal ty t
+      | Some size, Some ty -> size = s && btype_equal ty t in
+    let compliance_failure (t: btype_t) (s: int) =
+      let size_discrepancy size s =
+         "size discrepancy between tgtsize: "
+         ^ (string_of_int size)
+         ^ " and field size: "
+         ^ (string_of_int s) in
+      let type_discrepancy ty t =
+         "type discrepancy between tgttype: "
+         ^ (btype_to_string ty)
+         ^ " and field type: "
+         ^ (btype_to_string t) in
+      match tgtsize, tgtbtype with
+      | Some size, Some ty when (size != s) && (not (btype_equal ty t)) ->
+         (size_discrepancy size s) ^ " and " ^ (type_discrepancy ty t)
+      | Some size, _ when size != s -> size_discrepancy size s
+      | _, Some ty when not (btype_equal ty t) -> type_discrepancy ty t
+      | _ -> "" in
     match xoffset with
     | XConst (IntConst n) ->
        let offset = n#toInt in
@@ -266,9 +298,14 @@ object (self)
                            Ok (Some (FieldOffset
                                        ((finfo.bfname, finfo.bfckey), NoOffset)))
                          else if offset = 0
-                                 && (is_scalar fldtype) then
+                                 && (is_scalar fldtype)
+                                 && (check_tgttype_compliance fldtype sz) then
                            Ok (Some (FieldOffset
                                        ((finfo.bfname, finfo.bfckey), NoOffset)))
+                         else if offset = 0 && is_scalar fldtype then
+                           Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                                  ^ "Scalar type or size is not consistent: "
+                                  ^ (compliance_failure fldtype sz)]
                          else
                            Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
                                   ^ "Field offset "
@@ -473,25 +510,27 @@ object (self)
     end
 
   method add_load
-           ~(offset:int)
+           ~(baseoffset:int)
+           ~(offset:memory_offset_t)
            ~(size:int option)
            ~(typ:btype_t option)
            (var: variable_t)
            (iaddr:ctxt_iaddress_t) =
     let ty = match typ with Some t -> t  | _ -> t_unknown in
     let load = StackLoad (var, offset, size, ty) in
-    self#add_access offset iaddr load
+    self#add_access baseoffset iaddr load
 
   method add_store
-           ~(offset:int)
+           ~(baseoffset:int)
+           ~(offset:memory_offset_t)
            ~(size:int option)
            ~(typ:btype_t option)
            ~(xpr:xpr_t option)
            (var: variable_t)
            (iaddr:ctxt_iaddress_t) =
     let ty = match typ with Some t -> t | _ -> t_unknown in
     let store = StackStore (var, offset, size, ty, xpr) in
-    self#add_access offset iaddr store
+    self#add_access baseoffset iaddr store
 
   method add_block_read
            ~(offset:int)
@@ -513,15 +552,13 @@ object (self)
     self#add_access offset iaddr store
 
   method private write_xml_stack_slots (node: xml_element_int) =
-    let slotsnode = xmlElement "stack-slots" in
     begin
       H.iter (fun _ slot ->
           let slotnode = xmlElement "slot" in
           begin
             slot#write_xml slotnode;
-            slotsnode#appendChildren [slotnode]
+            node#appendChildren [slotnode]
           end) stackslots;
-      node#appendChildren [slotsnode]
     end
 
   method private write_xml_stack_accesses (node: xml_element_int) =

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -3736,9 +3736,10 @@ type stack_access_t =
   (** stack offset *)
   | RegisterRestore of int * register_t
   (** stack offset *)
-  | StackLoad of variable_t * int * int option * btype_t
+  | StackLoad of variable_t * memory_offset_t * int option * btype_t
   (** variable, offset, size *)
-  | StackStore of variable_t * int * int option * btype_t * xpr_t option
+  | StackStore of
+      variable_t * memory_offset_t * int option * btype_t * xpr_t option
   (** variable, offset, size, value *)
   | StackBlockRead of int * int option * btype_t
   (** offset, size *)
@@ -4560,6 +4561,7 @@ class type stackslot_int =
              -> memory_offset_t traceresult
 
     method is_typed: bool
+    method is_scalar: bool
     method is_struct: bool
     method is_array: bool
     method is_spill: bool
@@ -4588,15 +4590,17 @@ class type stackframe_int =
     method containing_stackslot: int -> stackslot_int option
 
     method add_load:
-             offset:int
+             baseoffset:int
+             -> offset: memory_offset_t
              -> size:int option
              -> typ:btype_t option
              -> variable_t
              -> ctxt_iaddress_t
              -> unit
 
     method add_store:
-             offset:int
+             baseoffset:int
+             -> offset: memory_offset_t
              -> size:int option
              -> typ:btype_t option
              -> xpr:xpr_t option
@@ -4764,7 +4768,8 @@ class type function_environment_int =
     method mk_gloc_variable:
              global_location_int -> memory_offset_t -> variable_t
 
-    method mk_stack_variable: stackframe_int -> numerical_t -> variable_t traceresult
+    method mk_stack_variable:
+             ?size: int -> stackframe_int -> numerical_t -> variable_t traceresult
 
     (** [mk_initial_memory_value var] returns an auxiliary variable that
         represents the initial value of [var] at function entry.