CHB: some infrastructure for stackframe management

sipma · sipma · commit 25b13eccedef · 2025-08-04T22:09:31.000-07:00
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
@@ -1603,6 +1603,7 @@ end
 
 class function_info_t
         (faddr: doubleword_int)
+        (fndata: function_data_int)
         (varmgr: variable_manager_int)
         (invio: invariant_io_int)
         (varinvio: var_invariant_io_int):function_info_int =
@@ -1650,7 +1651,7 @@ object (self)
   val mutable call_targets_set = false
   val nonreturning_calls = new StringCollections.set_t
   val mutable invariants_to_be_reset = false
-  val stackframe = mk_function_stackframe varmgr
+  val stackframe = mk_function_stackframe fndata varmgr
   val proofobligations =
     mk_proofobligations faddr (mk_xpodictionary varmgr#vard#xd)
 
@@ -2610,7 +2611,8 @@ let load_function_info ?(reload=false) (faddr:doubleword_int) =
       let varmgr = make_variable_manager faddr xvard in
       let invio = read_invs fname varmgr#vard in
       let varinvio = read_varinvs fname varmgr#vard in
-      let finfo = new function_info_t faddr varmgr invio varinvio in
+      let fndata = functions_data#get_function faddr in
+      let finfo = new function_info_t faddr fndata varmgr invio varinvio in
       let _ =
         match extract_function_info_file fname with
         | Some node -> finfo#read_xml node
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml
@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2023  Aarno Labs LLC
+   Copyright (c) 2023-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
@@ -33,19 +33,22 @@ open CHUtils
 
 (* chutil *)
 open CHLogger
+open CHTraceResult
 open CHXmlDocument
 
 (* xprlib *)
 open XprTypes
 
 (* bchlib *)
 open BCHBasicTypes
+open BCHBCTypePretty
 open BCHBCTypes
 open BCHBCTypeUtil
 open BCHCPURegisters
 open BCHLibTypes
 
 module H = Hashtbl
+module TR = CHTraceResult
 
 
 let bd = BCHDictionary.bdictionary
@@ -117,11 +120,98 @@ object (_self:'a)
 end
 
 
-class stackframe_t (varmgr: variable_manager_int):stackframe_int =
+let stackslot_rec_to_pretty (sslot: stackslot_rec_t): pretty_t =
+  LBLOCK [
+      STR "offset: "; INT sslot.sslot_offset; NL;
+      STR "name  : "; STR sslot.sslot_name; NL;
+      STR "type  : "; STR (btype_to_string sslot.sslot_btype); NL;
+      (match sslot.sslot_size with
+       | Some s -> LBLOCK [STR "size  : "; INT s; NL]
+       | _ -> STR "");
+      (match sslot.sslot_desc with
+       | Some desc -> LBLOCK [STR "desc  : "; STR desc; NL]
+       | _ -> STR "")
+    ]
+
+
+let opt_size_to_string (optsize: int option): string =
+  match optsize with
+  | Some s -> (string_of_int s)
+  | _ -> "?"
+
+
+class stackslot_t (sslot: stackslot_rec_t): stackslot_int =
+object
+
+  method sslot_rec = sslot
+
+  method name = sslot.sslot_name
+
+  method offset = sslot.sslot_offset
+
+  method btype = sslot.sslot_btype
+
+  method size = sslot.sslot_size
+
+  method desc = sslot.sslot_desc
+
+  method contains_offset (_offset: int) = false
+
+  method frame2object_offset_value (_xpr: xpr_t) = Error ["Not yet implemenented"]
+
+  method frame_offset_memory_offset
+           ?(tgtsize=None)
+           ?(tgtbtype=t_unknown)
+           (_xpr: xpr_t): memory_offset_t traceresult =
+    Error ["Not yet implemented for btype: "
+           ^ (btype_to_string tgtbtype)
+           ^  " and size "
+           ^ (opt_size_to_string tgtsize)]
+
+  method object_offset_memory_offset
+           ?(tgtsize=None)
+           ?(tgtbtype=t_unknown)
+           (_xpr: xpr_t): memory_offset_t traceresult =
+    Error ["Not yet implemented: "
+           ^ (btype_to_string tgtbtype)
+           ^ " and size "
+           ^ (opt_size_to_string tgtsize)]
+
+  method write_xml(_node: xml_element_int) = ()
+
+end
+
+
+class stackframe_t
+        (fndata: function_data_int)
+        (varmgr: variable_manager_int):stackframe_int =
 object (self)
 
   val saved_registers = H.create 3   (* reg -> saved_register_t *)
   val accesses = H.create 3      (* offset -> (iaddr, stack_access_t) list *)
+  val stackslots =
+    let slots = H.create 3 in    (* offset -> stackslot *)
+    begin
+      (match fndata#get_function_annotation with
+       | Some fnannot ->
+          List.iter (fun svintro ->
+              let ty = match svintro.svi_vartype with
+                | Some ty -> ty
+                | _ -> t_unknown in
+              let size = TR.to_option (size_of_btype ty) in
+              let sslot = {
+                  sslot_offset = svintro.svi_offset;
+                  sslot_name = svintro.svi_name;
+                  sslot_btype = ty;
+                  sslot_desc = Some ("svintro");
+                  sslot_size = size} in
+              let stackslot = new stackslot_t sslot in
+              let _ =
+                chlog#add "stack slot added" (stackslot_rec_to_pretty sslot) in
+              H.add slots svintro.svi_offset stackslot) fnannot.stackvarintros
+       | _ -> ());
+      slots
+    end
 
   method private vard = varmgr#vard
 
@@ -136,6 +226,79 @@ object (self)
         [] in
     H.replace accesses offset ((iaddr, acc) :: entry)
 
+  method containing_stackslot (offset: int): stackslot_int option =
+    H.fold (fun _ sslot acc ->
+        match acc with
+        | Some _ -> acc
+        | _ -> if sslot#contains_offset offset then Some sslot else None)
+      stackslots None
+
+  method add_stackslot
+           ?(name = None)
+           ?(btype = t_unknown)
+           ?(size = None)
+           ?(desc = None)
+           (offset: int): stackslot_int traceresult =
+    if offset <= 0 then
+      Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+             ^ "Illegal offset for stack slot: "
+             ^ (string_of_int offset)
+             ^ ". Offset should be greater than zero."]
+    else if H.mem stackslots offset then
+      begin
+        log_error_result
+          ~tag:"duplicate stack slot"
+          ~msg:("Stack slot at offset "
+                ^ (string_of_int offset)
+                ^ "already exists")
+          __FILE__ __LINE__ [];
+        Ok (H.find stackslots offset)
+      end
+    else
+      match self#containing_stackslot offset with
+      | Some sslot ->
+         let msg =
+           "Stackslot at offset "
+           ^ (string_of_int offset)
+           ^ " overlaps with "
+           ^ sslot#name
+           ^ " ("
+           ^ (string_of_int sslot#offset)
+           ^ (match sslot#size with
+              | Some s -> ", size: " ^ (string_of_int s)
+              | _ -> "")
+           ^ ")" in
+         begin
+           log_error_result
+             ~tag:"overlapping stackslot"
+             ~msg
+             __FILE__ __LINE__ [];
+           Error [msg]
+         end
+      | _ ->
+         let sname =
+           match name with
+           | Some name -> name
+           | _ -> "var_" ^ (string_of_int offset) in
+         let ssrec = {
+             sslot_name = sname;
+             sslot_offset = offset;
+             sslot_btype = btype;
+             sslot_size = size;
+             sslot_desc = desc
+           } in
+         let sslot = new stackslot_t ssrec in
+         begin
+           H.add stackslots offset sslot;
+           chlog#add
+             "stackframe:add stackslot"
+             (LBLOCK [
+                  INT offset;
+                  STR ": ";
+                  STR sslot#name]);
+           Ok sslot
+         end
+
   method add_register_spill
            ~(offset: int) (reg: register_t) (iaddr:ctxt_iaddress_t) =
     let spill = RegisterSpill (offset, reg) in
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli
@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2023-2024  Aarno Labs LLC
+   Copyright (c) 2023-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
@@ -25,9 +25,13 @@
    SOFTWARE.
    ============================================================================= *)
 
+(* chlib *)
+open CHPretty
 
 (* bchlib *)
 open BCHLibTypes
 
+val stackslot_rec_to_pretty: stackslot_rec_t -> pretty_t
 
-val mk_function_stackframe: variable_manager_int -> stackframe_int
+val mk_function_stackframe:
+  function_data_int -> variable_manager_int -> stackframe_int
diff --git a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml
@@ -541,12 +541,12 @@ object (self)
              ^ "Illegal global address: " ^ address#to_hex_string]
     else if H.mem locations address#index then
       begin
-        ch_error_log#add
-          "duplicate global location"
-          (LBLOCK [
-               STR "Global location at address ";
-               address#toPretty;
-               STR " already exists"]);
+        log_error_result
+          ~tag:"duplicate global location"
+          ~msg:("Global location at address "
+                ^ address#to_hex_string
+                ^ "already exists")
+          __FILE__ __LINE__ [];
         Ok (H.find locations address#index)
       end
     else
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -5189,6 +5189,41 @@ class type xpodictionary_int =
   end
 
 
+type stackslot_rec_t = {
+    sslot_name: string;
+    sslot_offset: int;
+    sslot_btype: btype_t;
+    sslot_size: int option;
+    sslot_desc: string option
+  }
+
+
+class type stackslot_int =
+  object
+
+    method sslot_rec: stackslot_rec_t
+    method name: string
+    method offset: int
+    method btype: btype_t
+    method size: int option
+    method desc: string option
+    method contains_offset: int -> bool
+    method frame2object_offset_value: xpr_t -> xpr_t traceresult
+    method frame_offset_memory_offset:
+             ?tgtsize:int option
+             -> ?tgtbtype:btype_t
+             -> xpr_t
+             -> memory_offset_t traceresult
+    method object_offset_memory_offset:
+             ?tgtsize:int option
+             -> ?tgtbtype:btype_t
+             -> xpr_t
+             -> memory_offset_t traceresult
+
+    method write_xml: xml_element_int -> unit
+  end
+
+
 class type stackframe_int =
   object
 
@@ -5197,6 +5232,16 @@ class type stackframe_int =
     method add_register_restore:
              offset:int -> register_t -> ctxt_iaddress_t -> unit
 
+    method add_stackslot:
+             ?name: string option
+             -> ?btype: btype_t
+             -> ?size: int option
+             -> ?desc: string option
+             -> int
+             -> stackslot_int traceresult
+
+    method containing_stackslot: int -> stackslot_int option
+
     method add_load:
              offset:int
              -> size:int option
