CHB: change base variable into base expression for array and struct

Author: sipma

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -1569,7 +1569,7 @@ object (self)
   val constant_table = new VariableCollections.table_t          (* constants *)
   val calltargets = H.create 5                               (* call-targets *)
 
-  val mutable base_pointers = new VariableCollections.set_t (* base-pointers *)
+  val base_pointers = new VariableCollections.set_t         (* base-pointers *)
   val mutable stack_adjustment = None                    (* stack-adjustment *)
   val saved_registers = H.create 3            (* saved-registers -- not read *)
 
@@ -2161,8 +2161,6 @@ object (self)
    * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
 
   method add_base_pointer (var:variable_t) =
-    let _ = track_function
-              self#a (LBLOCK [ STR "add base pointer: " ; var#toPretty ]) in
     base_pointers#add var
 
   method get_base_pointers = base_pointers#toList

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -3260,7 +3260,7 @@ class type type_constraint_store_int =
     [BaseArray (v, t)] and [BaseStruct (v, t)] on the other hand is that the
     variable [v] referenced in [BaseVar] refers to a variable that is a
     pointer, that is, its value is the address of the base, while the
-    variable [v] in [BaseArray] and [BaseStruct] is a symbolic representation
+    expression [x] in [BaseArray] and [BaseStruct] is a symbolic representation
     of the address itself, that is, there is no associated variable in the
     code. The latter two are applicable to global or stack-allocated arrays
     and structs that can be referenced directly via their address without
@@ -3277,10 +3277,10 @@ type memory_base_t =
 (** base provided by an externally controlled variable,
     e.g., argument to the function, or return value from malloc *)
 
-| BaseArray of variable_t * btype_t
+| BaseArray of xpr_t * btype_t
 (** base provided by a typed array address *)
 
-| BaseStruct of variable_t * btype_t
+| BaseStruct of xpr_t * btype_t
 (** base provided by a typed struct address *)
 
 | BaseUnknown of string  (** address without interpretation *)
@@ -3290,7 +3290,10 @@ type memory_base_t =
 type memory_offset_t =
   | NoOffset
   | ConstantOffset of numerical_t * memory_offset_t
-  (** typically used when the type of the variable is not known*)
+  (** typically used when the type of the variable is not known, or for
+      global offsets (the absolute address of a global variable), or for
+      stack offsets (the difference between the stack pointer and the value
+      of the stack pointer at function entry *)
 
   | FieldOffset of fielduse_t * memory_offset_t
   (** offset in a struct variable with [(fieldname, struct key)] *)
@@ -3332,13 +3335,13 @@ object ('a)
       memory reference.
 
       Returns [Error] if this memory reference does not have a [BaseArray] base.*)
-  method get_array_base: (variable_t * btype_t) traceresult
+  method get_array_base: (xpr_t * btype_t) traceresult
 
   (** Returns the memory address variable and type of the base address of this
       memory reference.
 
       Returns [Error] if this memory reference does not have a [BaseStruct] base.*)
-  method get_struct_base: (variable_t * btype_t) traceresult
+  method get_struct_base: (xpr_t * btype_t) traceresult
 
   (** {1 Predicates} *)
 
@@ -3377,8 +3380,8 @@ object
   method mk_allocated_stack_reference: memory_reference_int
   method mk_realigned_stack_reference: memory_reference_int
   method mk_basevar_reference: variable_t -> memory_reference_int
-  method mk_base_array_reference: variable_t -> btype_t -> memory_reference_int
-  method mk_base_struct_reference: variable_t -> btype_t -> memory_reference_int
+  method mk_base_array_reference: xpr_t -> btype_t -> memory_reference_int
+  method mk_base_struct_reference: xpr_t -> btype_t -> memory_reference_int
   method mk_unknown_reference: string -> memory_reference_int
 
   (** {1 Accessors} *)

CodeHawk/CHB/bchlib/bCHMemoryReference.ml

@@ -39,6 +39,7 @@ open CHTraceResult
 
 (* xprlib *)
 open Xprt
+open XprTypes
 open XprToPretty
 
 (* bchlib *)
@@ -64,8 +65,8 @@ let memory_base_to_string (b: memory_base_t): string =
   | BAllocatedStackFrame -> "allocated-stack"
   | BGlobal -> "global"
   | BaseVar v -> "var-" ^ v#getName#getBaseName
-  | BaseArray (v, _) -> "array-" ^ v#getName#getBaseName
-  | BaseStruct (v, _) -> "struct-" ^ v#getName#getBaseName
+  | BaseArray (x, _) -> "array-" ^ (x2s x)
+  | BaseStruct (x, _) -> "struct-" ^ (x2s x)
   | BaseUnknown s -> "unknown-" ^ s
 
 
@@ -322,11 +323,11 @@ object (self:'a)
 
   method get_base = base
 
-  method get_name =
+  method get_name: string =
     match base with
     | BaseVar v -> v#getName#getBaseName
-    | BaseArray (v, _) -> v#getName#getBaseName
-    | BaseStruct (v, _) -> v#getName#getBaseName
+    | BaseArray (x, _) -> (x2s x)
+    | BaseStruct (x, _) -> (x2s x)
     | BLocalStackFrame -> "var"
     | BRealignedStackFrame -> "varr"
     | BAllocatedStackFrame -> "vara"
@@ -343,25 +344,25 @@ object (self:'a)
     match base with
     | BaseVar v -> Ok v
     | _ ->
-       Error [
-           "get_external_base: not an external base: "
-           ^ (memory_base_to_string base)]
+       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+              ^ "Not an external base: "
+              ^ (memory_base_to_string base)]
 
-  method get_array_base: (variable_t * btype_t) traceresult =
+  method get_array_base: (xpr_t * btype_t) traceresult =
     match base with
-    | BaseArray (v, t) -> Ok (v, t)
+    | BaseArray (x, t) -> Ok (x, t)
     | _ ->
-       Error [
-           "get_array_base: not an array base: "
-           ^ (memory_base_to_string base)]
+       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+              ^ "Not an array base: "
+              ^ (memory_base_to_string base)]
 
-  method get_struct_base: (variable_t * btype_t) traceresult =
+  method get_struct_base: (xpr_t * btype_t) traceresult =
     match base with
-    | BaseStruct (v, t) -> Ok (v, t)
+    | BaseStruct (x, t) -> Ok (x, t)
     | _ ->
-       Error [
-           "get_struct_base: not a struct base: "
-           ^ (memory_base_to_string base)]
+       Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+              ^ "Not a struct base: "
+              ^ (memory_base_to_string base)]
 
   method has_external_base =
     match base with BaseVar _ -> true | _ -> false
@@ -384,7 +385,7 @@ object (self:'a)
   method is_unknown_reference =
     match base with BaseUnknown _ -> true | _ -> false
 
-  method toPretty = LBLOCK [ memory_base_to_pretty base ]
+  method toPretty = LBLOCK [memory_base_to_pretty base]
 
 end
 
@@ -419,20 +420,20 @@ object (self)
 
   method mk_basevar_reference v = self#mk_reference (BaseVar v)
 
-  method mk_base_array_reference (v: variable_t) (t: btype_t) =
-    self#mk_reference (BaseArray (v, t))
+  method mk_base_array_reference (x: xpr_t) (t: btype_t) =
+    self#mk_reference (BaseArray (x, t))
 
-  method mk_base_struct_reference (v: variable_t) (t: btype_t) =
-    self#mk_reference (BaseStruct (v, t))
+  method mk_base_struct_reference (x: xpr_t) (t: btype_t) =
+    self#mk_reference (BaseStruct (x, t))
 
   method mk_unknown_reference s = self#mk_reference (BaseUnknown s)
 
   method get_memory_reference (index: int): memory_reference_int traceresult =
     if H.mem table index then
       Ok (H.find table index)
     else
-      Error [
-          "get_memory_reference_int: index not found: " ^ (string_of_int index)]
+      Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+             ^ "Index not found: " ^ (string_of_int index)]
 
   method get_memory_reference_type (index: int): btype_t option =
     tfold_default
@@ -443,13 +444,13 @@ object (self)
   method is_unknown_reference (index: int): bool traceresult =
     let memref_r = self#get_memory_reference index in
     tmap
-      ~msg:"is_unknown_reference"
+      ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
       (fun memref -> memref#is_unknown_reference) memref_r
 
   method is_global_reference (index: int): bool traceresult =
     let memref_r = self#get_memory_reference index in
     tmap
-      ~msg:"is_global_reference"
+      ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
       (fun memref -> memref#is_global_reference) memref_r
 
   method initialize =

CodeHawk/CHB/bchlib/bCHVarDictionary.ml

@@ -117,8 +117,8 @@ object (self)
         | BAllocatedStackFrame
         | BGlobal -> (tags, [])
       | BaseVar v -> (tags, [xd#index_variable v])
-      | BaseArray (v, t) -> (tags, [xd#index_variable v; bcd#index_typ t])
-      | BaseStruct (v, t) -> (tags, [xd#index_variable v; bcd#index_typ t])
+      | BaseArray (x, t) -> (tags, [xd#index_xpr x; bcd#index_typ t])
+      | BaseStruct (x, t) -> (tags, [xd#index_xpr x; bcd#index_typ t])
       | BaseUnknown s -> (tags, [bd#index_string s]) in
     memory_base_table#add key
 
@@ -133,8 +133,8 @@ object (self)
     | "a" -> BAllocatedStackFrame
     | "g" -> BGlobal
     | "v" -> BaseVar (xd#get_variable (a 0))
-    | "b" -> BaseArray (xd#get_variable (a 0), bcd#get_typ (a 1))
-    | "s" -> BaseStruct (xd#get_variable (a 0), bcd#get_typ (a 1))
+    | "b" -> BaseArray (xd#get_xpr (a 0), bcd#get_typ (a 1))
+    | "s" -> BaseStruct (xd#get_xpr (a 0), bcd#get_typ (a 1))
     | "u" -> BaseUnknown (bd#get_string (a 0))
     | s -> raise_tag_error name s memory_base_mcts#tags