CHB: add facility to decompose array expressions

Author: sipma

CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml

@@ -41,6 +41,7 @@ open BCHBCFiles
 open BCHBCTypePretty
 open BCHBCTypes
 
+
 let string_printer = CHPrettyUtil.string_printer
 let p2s = string_printer#print
 
@@ -941,6 +942,32 @@ let get_compinfo_field (c: bcompinfo_t) (fname: string): bfieldinfo_t =
                STR fname]))
 
 
+let get_struct_field_at_offset
+      (cinfo: bcompinfo_t) (offset: int): (bfieldinfo_t * int) option =
+  let finfos = cinfo.bcfields in
+  let field0 = List.hd finfos in
+  if offset = 0 then
+    Some (field0, 0)
+  else
+    let field0type = resolve_type field0.bftype in
+    if offset < size_of_btype field0type then
+      Some (field0, offset)
+    else
+      List.fold_left (fun acc finfo ->
+          match acc with
+          | Some _ -> acc
+          | _ ->
+             match finfo.bfieldlayout with
+             | Some (foffset, size) ->
+                if offset = foffset then
+                  Some (finfo, 0)
+                else if offset > foffset && offset < foffset + size then
+                  Some (finfo, offset - foffset)
+                else
+                  None
+             | _ -> None) None finfos
+
+
 let rec get_compinfo_scalar_type_at_offset
           (cinfo: bcompinfo_t) (offset: int): btype_t option =
   let finfos = cinfo.bcfields in

CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli

@@ -226,12 +226,15 @@ val get_struct_type_compinfo: btype_t -> bcompinfo_t
 
 val get_struct_type_fields: btype_t -> bfieldinfo_t list
 
+val get_struct_field_at_offset: bcompinfo_t -> int -> (bfieldinfo_t * int) option
+
 val get_compinfo_struct_type: bcompinfo_t -> btype_t
 
 val get_compinfo_field: bcompinfo_t -> string -> bfieldinfo_t
 
 val get_compinfo_scalar_type_at_offset: bcompinfo_t -> int -> btype_t option
 
+
 (** {2 Fieldinfos}*)
 
 val get_struct_field_name: bfieldinfo_t -> string

CodeHawk/CHB/bchlib/bCHConstantDefinitions.mli

@@ -148,3 +148,8 @@ val read_xml_symbolic_flags: xml_element_int -> unit
     narrowed to a particular type [ty].*)
 val has_constant_value: ?ty:btype_t option -> string -> bool
 val get_constant_value: ?ty:btype_t option -> string -> doubleword_int
+
+
+(** {1 Access for unit tests} *)
+
+val add_address: constant_definition_t -> unit

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -1069,29 +1069,51 @@ object (self)
 
   method get_fts_parameter_expr (_p: fts_parameter_t) = None
 
-  method private get_offset ox =
-    let oxs = simplify_xpr ox in
-    match oxs with
-    | XConst (IntConst n) -> ConstantOffset (n, NoOffset)
-    | XVar v -> IndexOffset (v, 1, NoOffset)
-    | XOp (XMult, [XConst (IntConst n); XVar v]) when n#is_int ->
-       IndexOffset (v, n#toInt, NoOffset)
-    | XOp (XMult, [XConst (IntConst _); XVar _]) ->
-      let msg = LBLOCK [self#l#toPretty; STR ": floc#get_offset: "; x2p oxs] in
-      begin
-	ch_error_log#add "number too large" msg;
-	UnknownOffset
-      end
-    | XOp (XPlus, [XConst (IntConst n); y]) ->
-       ConstantOffset (n, self#get_offset y)
-    | _ ->
-      let msg = (LBLOCK [STR "offset expr:  "; x2p oxs]) in
-      begin
-	ch_error_log#add
-          "unknown offset expr"
-	  (LBLOCK [self#l#toPretty; STR "  "; msg]);
-	UnknownOffset
-      end
+  method decompose_array_address
+           (x: xpr_t): (memory_reference_int * memory_offset_t) option =
+    let _ = chlog#add "decompose_array_address" (LBLOCK [STR "xpr: "; x2p x]) in
+    let vars = vars_as_positive_terms x in
+    let memaddrs = List.filter self#f#env#is_memory_address_variable vars in
+    let optbase =
+      match memaddrs with
+      | [base] ->
+         let (_, _, _, optty) =
+           self#f#env#varmgr#get_memory_address_meminfo base in
+         let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
+         Some (XVar base, offset, optty)
+      | _ ->
+         None in
+    match optbase with
+    | None -> None
+    | Some (_, _, None) -> None
+    | Some (XVar base, xoffset, Some ty) ->
+       let _ =
+         chlog#add
+           "decompose_array_address" (LBLOCK [STR "xoffset: "; x2p xoffset]) in
+       let eltty = get_element_type ty in
+       let elttysize = size_of_btype eltty in
+       let optmemref = TR.to_option (self#env#mk_base_variable_reference base) in
+       let optindex = get_array_index_offset xoffset elttysize in
+       let memoffset =
+         match optindex with
+         | None ->
+            let _ =
+              chlog#add
+                "decompose_array_address"
+                (LBLOCK [
+                     STR "Unable to get array index offset for ";
+                     x2p xoffset;
+                     STR " with size ";
+                     INT elttysize]) in
+            UnknownOffset
+         | Some (indexxpr, rem) ->
+            let remoffset = mk_maximal_memory_offset rem eltty in
+            ArrayIndexOffset (indexxpr, remoffset) in
+       (match (optmemref, memoffset) with
+        | (_, UnknownOffset) -> None
+        | (Some memref, memoffset) -> Some (memref, memoffset)
+        | _ -> None)
+    | _ -> None
 
 
   (* the objective is to extract a base pointer and an offset expression

CodeHawk/CHB/bchlib/bCHFunctionInfo.ml

@@ -789,19 +789,25 @@ object (self)
            ?(size=4)
            ?(offset=0)
            (var: variable_t): variable_t =
-    if self#is_memory_address_variable var then
-      let (memrefix, memoffset, optname) = varmgr#get_memory_address_meminfo var in
-      let memref = TR.tget_ok (varmgr#memrefmgr#get_memory_reference memrefix) in
-      let v = self#mk_index_offset_memory_variable memref memoffset in
-      let _ =
-        match optname with
-        | Some name -> self#set_variable_name v name
-        | _ -> () in
-      v
+    if offset = 0 then
+      if self#is_memory_address_variable var then
+        let (memrefix, memoffset, optname, _optty) =
+          varmgr#get_memory_address_meminfo var in
+        let memref = TR.tget_ok (varmgr#memrefmgr#get_memory_reference memrefix) in
+        let v = self#mk_index_offset_memory_variable ~size memref memoffset in
+        let _ =
+          match optname with
+          | Some name -> self#set_variable_name v name
+          | _ -> () in
+        v
+      else
+        raise
+          (BCH_failure
+             (LBLOCK [STR "Not a memory address variable"; var#toPretty]))
     else
       raise
         (BCH_failure
-           (LBLOCK [STR "Not a memory address variable"; var#toPretty]))
+           (LBLOCK [STR "Nonstandard size or offset not yet supported"]))
 
   method mk_index_offset_global_memory_variable
            ?(elementsize=4)
@@ -929,8 +935,9 @@ object (self)
     else
       default ()
 
-  method mk_global_memory_address ?(optname = None) (n: numerical_t) =
-    self#mk_variable (varmgr#make_global_memory_address ~optname n)
+  method mk_global_memory_address
+           ?(optname = None) ?(opttype=None) (n: numerical_t) =
+    self#mk_variable (varmgr#make_global_memory_address ~optname ~opttype n)
 
   method mk_register_variable (register:register_t) =
     self#mk_variable (varmgr#make_register_variable register)

CodeHawk/CHB/bchlib/bCHLibTypes.mli

@@ -3218,8 +3218,13 @@ type memory_base_t =
 | BRealignedStackFrame (** local stack frame after realignment *)
 | BAllocatedStackFrame (** extended stack frame from alloca *)
 | BGlobal  (** global data *)
-| BaseVar of variable_t  (** base provided by an externally controlled variable,
-e.g., argument to the function, or return value from malloc *)
+| BaseVar of variable_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
+(** base provided by a typed array address *)
+
 | BaseUnknown of string  (** address without interpretation *)
 
 
@@ -3228,7 +3233,8 @@ type memory_offset_t =
   | NoOffset
   | ConstantOffset of numerical_t * memory_offset_t
   | FieldOffset of fielduse_t * memory_offset_t
-  | IndexOffset of variable_t * int * memory_offset_t
+  | IndexOffset of variable_t * int * memory_offset_t  (* deprecated *)
+  | ArrayIndexOffset of xpr_t * memory_offset_t  (* scaled by element type size *)
   | UnknownOffset
 
 
@@ -3269,6 +3275,7 @@ 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_unknown_reference: string -> memory_reference_int
 
   (* accessors *)
@@ -3375,8 +3382,8 @@ and constant_value_variable_t =
   assigned by the callee at call site [iaddr] to the argument with
   name [name].*)
 
-  | MemoryAddress of int * memory_offset_t * string option
-  (** [MemoryAddress (memrefix, offset, optname) represents a memory
+  | MemoryAddress of int * memory_offset_t * string option * btype_t option
+  (** [MemoryAddress (memrefix, offset, optname, opttype) represents a memory
   address with external meaning (e.g., a global arrray) *)
 
   | BridgeVariable of ctxt_iaddress_t * int      (* call site, argument index *)
@@ -3427,7 +3434,8 @@ object ('a)
       Returns [Error] if this variable is not a memory variable. *)
   method get_memory_offset: memory_offset_t traceresult
 
-  method get_memory_address_meminfo: (int * memory_offset_t * string option)
+  method get_memory_address_meminfo:
+           (int * memory_offset_t * string option * btype_t option)
 
   (** Returns the name of the associated function pointer.
 
@@ -3658,7 +3666,10 @@ object
            -> assembly_variable_int
 
   method make_global_memory_address:
-           ?optname:string option -> numerical_t -> assembly_variable_int
+           ?optname:string option
+           -> ?opttype:btype_t option
+           -> numerical_t
+           -> assembly_variable_int
 
   (** {2 Auxiliary variables}*)
 
@@ -3820,7 +3831,7 @@ object
   method is_memory_address_variable: variable_t -> bool
 
   method get_memory_address_meminfo:
-           variable_t -> (int * memory_offset_t * string option)
+           variable_t -> (int * memory_offset_t * string option * btype_t option)
 
 
   (** {2 Memory offsets} *)
@@ -4215,7 +4226,10 @@ class type function_environment_int =
              ?size:int -> ?offset:memory_offset_t -> numerical_t -> variable_t
 
     method mk_global_memory_address:
-             ?optname: string option -> numerical_t -> variable_t
+             ?optname: string option
+             -> ?opttype: btype_t option
+             -> numerical_t
+             -> variable_t
 
     method mk_initial_memory_value: variable_t -> variable_t
 
@@ -4243,7 +4257,10 @@ class type function_environment_int =
     (** {2 Memory address variables} *)
 
     method mk_global_memory_address:
-             ?optname: string option -> numerical_t -> variable_t
+             ?optname: string option
+             -> ?opttype: btype_t option
+             -> numerical_t
+             -> variable_t
 
     (** {2 Other variables} *)
 
@@ -5449,6 +5466,9 @@ class type floc_int =
     (* returns the memory reference that corresponds to the address expression *)
     method decompose_address: xpr_t -> (memory_reference_int * memory_offset_t)
 
+    method decompose_array_address:
+             xpr_t -> (memory_reference_int * memory_offset_t) option
+
     (* returns the variable associated with the address expression *)
     method get_lhs_from_address: xpr_t -> variable_t