CHB:TYPE: add typeconstant voidptr

Author: sipma

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -1258,7 +1258,7 @@ object (self)
               self#f#env#mk_offset_memory_variable memref memoff)
             memref_r memoff_r
 
-  method private get_variable_type (v: variable_t): btype_t traceresult =
+  method get_variable_type (v: variable_t): btype_t traceresult =
     let is_zero (x: xpr_t) =
       match x with
       | XConst (IntConst n) -> n#equal numerical_zero

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -3181,6 +3181,7 @@ type type_constant_t =
   | TyTInt of signedness_t * int
   | TyTStruct of int * string  (** bckey, bcname *)
   | TyTFloat of fkind_t
+  | TyVoidPtr   (** only to be used in the context of a void pointer *)
   | TyTUnknown  (** top in type lattice *)
   | TyBottom  (** bottom in type lattice *)
 
@@ -6020,6 +6021,8 @@ class type floc_int =
              -> xpr_t               (** address value *)
              -> variable_t traceresult
 
+    method get_variable_type: variable_t -> btype_t traceresult
+
     method get_xpr_type: xpr_t -> btype_t traceresult
 
     (** {2 Predicates on variables}*)

CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml

@@ -559,11 +559,13 @@ object
     | TyTInt _ -> "ti"
     | TyTStruct _ -> "ts"
     | TyTFloat _ -> "tf"
+    | TyVoidPtr -> "vp"
     | TyTUnknown -> "u"
     | TyBottom -> "b"
 
   method !tags = [
-      "a"; "ac"; "acl"; "ap"; "asl"; "ax"; "b"; "i"; "s"; "ti"; "tf"; "ts"; "u"; "z"]
+      "a"; "ac"; "acl"; "ap"; "asl"; "ax"; "b"; "i";
+      "s"; "ti"; "tf"; "ts"; "u"; "vp"; "z"]
 
 end
 

CodeHawk/CHB/bchlib/bCHSystemSettings.ml

@@ -116,7 +116,8 @@ let _ =
       ("LDR-stack-addr", "enable");
       ("LDR-struct-field", "enable");
       ("LDRH-memop-tc", "enable");
-      ("POP-sig-rv", "enable")
+      ("POP-sig-rv", "enable");
+      ("STR-memop-tc", "enable")
     ]
 
 

CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml

@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2024  Aarno Labs LLC
+   Copyright (c) 2024-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
@@ -171,6 +171,7 @@ object (self)
       | TyTInt (sg, si) -> (tags @ [signedness_mfts#ts sg], [si])
       | TyTStruct (key, name) -> (tags @ [name], [key])
       | TyTFloat k -> (tags @ [fkind_mfts#ts k], [])
+      | TyVoidPtr -> (tags, [])
       | TyBottom -> (tags, [])
       | TyTUnknown -> (tags, []) in
     type_constant_table#add key
@@ -192,6 +193,7 @@ object (self)
     | "ti" -> TyTInt (signedness_mfts#fs (t 1), a 0)
     | "tf" -> TyTFloat (fkind_mfts#fs (t 1))
     | "ts" -> TyTStruct (a 0, t 1)
+    | "vp" -> TyVoidPtr
     | "b" -> TyBottom
     | "u" -> TyTUnknown
     | s -> raise_tag_error name s type_constant_mcts#tags

CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml

@@ -543,6 +543,10 @@ object (self)
            match result#toList with
            | [ixty1; ixty2] ->
               (match (bcd#get_typ ixty1), (bcd#get_typ ixty2) with
+               | TPtr (TVoid _, _), TPtr _ ->
+                  Some (bcd#get_typ ixty2)
+               | TPtr _, TPtr (TVoid _, _) ->
+                  Some (bcd#get_typ ixty1)
                | TPtr (tty1, _), TPtr (tty2, _)
                     when is_struct_type tty1 && is_scalar tty2 ->
                   Some (bcd#get_typ ixty1)

CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml

@@ -140,6 +140,7 @@ let type_constant_to_string (c: type_constant_t) =
        ^ "(" ^ (string_of_int si) ^ ")"
   | TyTStruct (_, name) -> "t_struct_" ^ name
   | TyTFloat k -> float_type_to_string k
+  | TyVoidPtr -> "t_voidptr"
   | TyTUnknown -> "t_top"
   | TyBottom -> "t_bottom"
 
@@ -442,6 +443,8 @@ 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 (pty, _) ->
         let ptv = add_deref_capability tv in
         mk_btype_constraint ptv pty
@@ -461,6 +464,10 @@ let rec mk_btype_constraint (tv: type_variable_t) (ty: btype_t)
                 "Unable to create array access capability (no size): %s [%s:%d]"
                 (String.concat "; " e)
                 __FILE__ __LINE__;
+              log_diagnostics_result
+                __FILE__ __LINE__
+                ["Unable to create array access capability (no size): "
+                 ^ (String.concat "; " e)];
               None
             end)
      | rty ->
@@ -514,6 +521,7 @@ let type_constant_to_btype (tc: type_constant_t) =
      TInt (ikind, [])
   | TyTStruct (key, _) -> get_compinfo_struct_type (bcfiles#get_compinfo key)
   | TyTFloat fkind -> TFloat (fkind, FScalar, [])
+  | TyVoidPtr -> t_voidptr
   | TyBottom -> t_unknown
   | TyTUnknown -> t_unknown