CHB: convert numeric offsets to field offsets

sipma · sipma · commit 60ec1fff4492 · 2025-03-08T15:39:56.000-08:00
diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml
@@ -676,7 +676,7 @@ object (self)
       let memoff_r =
         TR.tbind
           (fun memvar ->
-            let memtype = self#get_variable_type memvar in
+            let memtype = self#env#get_variable_type memvar in
             let memtype =
               match memtype with
               | Some t -> t
@@ -703,7 +703,8 @@ object (self)
               match optbasetype with
               | Some t when is_pointer t -> ptr_deref t
               | _ -> t_unknown in
-            address_memory_offset basetype (num_constant_expr memoffset))
+            address_memory_offset basetype
+              ~tgtsize:(Some size) (num_constant_expr memoffset))
           (self#env#get_variable base#getSeqNumber) in
       mk_memvar memref_r memoff_r
 
@@ -1319,23 +1320,139 @@ object (self)
   method private get_variable_type (v: variable_t): btype_t option =
     if self#f#env#is_initial_register_value v then
       let reg_r = self#f#env#get_initial_register_value_register v in
-      let param_r =
-        TR.tbind
-          (fun reg ->
-            if self#f#get_summary#has_parameter_for_register reg then
-              Ok (self#f#get_summary#get_parameter_for_register reg)
-            else
-              Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-                     ^ (p2s v#toPretty)
-                     ^ " does not have an associated parameter"])
-          reg_r in
       TR.tfold_default
-        (fun param -> Some param.apar_type)
-        (self#env#get_variable_type v)
-        param_r
+        (fun reg ->
+          if self#f#get_summary#has_parameter_for_register reg then
+            let param = self#f#get_summary#get_parameter_for_register reg in
+            Some param.apar_type
+          else
+            self#env#get_variable_type v)
+        None
+        reg_r
+    else if self#env#is_initial_memory_value v then
+      let memvar_r = self#env#get_init_value_variable v in
+      TR.tfold
+        ~ok:self#get_variable_type
+        ~error:(fun e ->
+          begin log_error_result __FILE__ __LINE__ e; None end)
+        memvar_r
     else
       self#env#get_variable_type v
 
+  method convert_variable_offsets
+           ?(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.tmap self#get_variable_type cbasevar_r in
+      let tgttype_r =
+        TR.tbind
+          (fun basetype ->
+            match basetype with
+            | Some (TPtr (t, _)) -> Ok t
+            | Some t ->
+               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                      ^ "Type " ^ (btype_to_string t)
+                      ^ " is not a pointer"]
+            | _ ->
+               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                      ^ "No type for variable "
+                      ^ (p2s v#toPretty)
+                      ^ "with basevar "
+                      ^ (p2s (TR.tget_ok cbasevar_r)#toPretty)]) basetype_r in
+      let coffset_r =
+        TR.tbind
+          (fun offset ->
+            match offset with
+            | ConstantOffset (n, NoOffset) ->
+               TR.tbind
+                 (fun tgttype ->
+                   address_memory_offset
+                     ~tgtsize:size tgttype (num_constant_expr n)) tgttype_r
+            | _ -> Ok offset) offset_r in
+      TR.tbind
+        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty))
+        (fun cbasevar ->
+          TR.tbind
+            (fun coffset ->
+              self#env#mk_basevar_memory_variable cbasevar coffset
+            ) coffset_r)
+        cbasevar_r
+    else
+      Ok v
+
+  method convert_value_offsets
+           ?(size=None) (v: variable_t): variable_t traceresult =
+    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
+      let cbasevar_r = TR.tbind self#convert_value_offsets basevar_r in
+      let basetype_r = TR.tmap self#get_variable_type cbasevar_r in
+      let tgttype_r =
+        TR.tbind
+          (fun basetype ->
+            match basetype with
+            | Some (TPtr (t, _)) -> Ok t
+            | Some t ->
+               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                      ^ "Type " ^ (btype_to_string t)
+                      ^ " is not a pointer"]
+            | _ ->
+               Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+                      ^ "No type for variable "
+                      ^ (p2s v#toPretty)
+                      ^ "with basevar "
+                      ^ (p2s (TR.tget_ok cbasevar_r)#toPretty)]) basetype_r in
+      let coffset_r =
+        TR.tbind
+          (fun offset ->
+            match offset with
+            | NoOffset ->
+               TR.tbind
+                 (fun tgttype ->
+                   address_memory_offset
+                     ~tgtsize:size tgttype (int_constant_expr 0)) tgttype_r
+            | ConstantOffset (n, NoOffset) ->
+               TR.tbind
+                 (fun tgttype ->
+                   address_memory_offset
+                     ~tgtsize:size tgttype (num_constant_expr n)) tgttype_r
+            | _ -> Ok offset) offset_r in
+      TR.tbind
+        ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ (p2s v#toPretty))
+        (fun cbasevar ->
+          TR.tbind
+            (fun coffset ->
+              let memvar_r =
+                self#env#mk_basevar_memory_variable cbasevar coffset in
+              TR.tbind self#env#mk_initial_memory_value memvar_r
+            ) coffset_r)
+        cbasevar_r
+    else
+      Ok v
+
+  method convert_xpr_offsets ?(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 ->
+         TR.tmap
+           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+           (fun v -> XVar v) (self#convert_value_offsets ~size v)
+      | XVar v when self#env#is_basevar_memory_variable v ->
+         TR.tmap
+           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+           (fun v -> XVar v) (self#convert_variable_offsets ~size v)
+      | XOp ((Xf "addressofvar"), [XVar v]) ->
+         TR.tmap
+           ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
+           (fun v -> XVar v) (self#convert_variable_offsets ~size v)
+      | XOp (op, [xx]) -> TR.tmap (fun x -> XOp (op, [x])) (aux xx)
+      | XOp (op, [x1; x2]) ->
+         TR.tmap2 (fun x1 x2 -> XOp (op, [x1; x2])) (aux x1) (aux x2)
+      | _ -> Ok exp in
+    aux x
+
   method get_xpr_type (x: xpr_t): btype_t option =
     match x with
     | XVar v -> self#get_variable_type v
@@ -1351,9 +1468,12 @@ object (self)
     | [base] ->
        let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
        let memref_r = self#env#mk_base_variable_reference base in
-       let vartype = self#get_variable_type base in
+       let vartype = self#env#get_variable_type base in
        let vartype = match vartype with None -> t_unknown | Some t -> t in
-       let memoff_r = address_memory_offset vartype offset in
+       let rvartype = TR.tvalue (resolve_type vartype) ~default:t_unknown in
+       let basetype =
+         if is_pointer rvartype then ptr_deref rvartype else t_unknown in
+       let memoff_r = address_memory_offset basetype offset in
        (*
          (match offset with
           | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
@@ -800,6 +800,14 @@ object (self)
       let avar = varmgr#make_memory_variable memref ~size offset in
       self#mk_variable avar
 
+  method mk_basevar_memory_variable
+           ?(size=4)
+           (basevar: variable_t)
+           (offset: memory_offset_t): variable_t traceresult =
+    let memref_r = self#mk_base_variable_reference basevar in
+    TR.tmap
+      (fun memref -> self#mk_offset_memory_variable ~size memref offset)
+      memref_r
 
       (*
   method mk_index_offset_global_memory_variable
diff --git a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml
@@ -186,6 +186,15 @@ let rec address_memory_offset
      Ok NoOffset
   | XConst (IntConst n) when is_unknown_type rbasetype ->
      Ok (ConstantOffset (n, NoOffset))
+  | XConst (IntConst n) ->
+     let tgtbtype =
+       if is_unknown_type tgtbtype then None else Some tgtbtype in
+     if is_struct_type rbasetype then
+       structvar_memory_offset ~tgtsize ~tgtbtype rbasetype xoffset
+     else if is_array_type rbasetype then
+       arrayvar_memory_offset ~tgtsize ~tgtbtype rbasetype xoffset
+     else
+       Ok (ConstantOffset (n, NoOffset))
   | _ ->
      let tgtbtype =
        if is_unknown_type tgtbtype then None else Some tgtbtype in
@@ -195,9 +204,7 @@ let rec address_memory_offset
        arrayvar_memory_offset ~tgtsize ~tgtbtype rbasetype xoffset
      else
        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
-              ^ (btype_to_string basetype)
-              ^ " (" ^ (btype_to_string rbasetype) ^ ")"
-              ^ " is not known to be a struct or array"]
+              ^ "Offset " ^ (x2s xoffset) ^ " not yet supported"]
 
 and structvar_memory_offset
 ~(tgtsize: int option)
diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml
@@ -437,6 +437,10 @@ let rec mk_btype_constraint (tv: type_variable_t) (ty: btype_t)
      | TPtr (pty, _) ->
         let ptv = add_deref_capability tv in
         mk_btype_constraint ptv pty
+     | TArray (elty, Some (Const (CInt (i64, _, _))), _) ->
+        let size = Int64.to_int i64 in
+        let atv = add_array_access_capability size tv in
+        mk_btype_constraint atv elty
      | TArray (elty, _, _) ->
         let size_r = size_of_btype elty in
         (match size_r with
diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml
@@ -97,7 +97,8 @@ object (self:'a)
           | _ ->
              (match offset with
               | NoOffset -> "__pderef_" ^ basename ^ "_"
-              | _ -> basename ^ (memory_offset_to_string offset)))
+              | ConstantOffset _ -> basename ^ (memory_offset_to_string offset)
+              | _ -> "__pderef_" ^ basename ^ (memory_offset_to_string offset)))
       | RegisterVariable reg -> register_to_string reg
       | CPUFlagVariable flag -> flag_to_string flag
       | AuxiliaryVariable a ->
@@ -1004,7 +1005,10 @@ object (self)
 
   method has_constant_offset (v: variable_t) =
     (self#is_memory_variable v)
-    && (tfold_default is_constant_offset false (self#get_memvar_offset v))
+    && (tfold_default
+          (fun off -> is_constant_offset off || is_field_offset off)
+          false
+          (self#get_memvar_offset v))
 
   method is_unknown_base_memory_variable (v: variable_t) =
     (self#is_memory_variable v)
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -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
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250210"
-  ~date:"2025-02-10"
+  ~version:"0.6.0_20250222"
+  ~date:"2025-02-22"
   ~licensee: None
   ~maxfilesize: None
   ()
