CHB:TI: allow join of struct type and type of first field

Author: sipma

CodeHawk/CHB/bchlib/bCHFloc.ml

@@ -1389,6 +1389,14 @@ object (self)
           (self#f#is_base_pointer v)
           || (TR.tfold_default is_pointer false (self#get_variable_type v))
         ) vars in
+    let _ =
+      log_diagnostics_result
+        ~tag:"convert_addr_to_c_pointed_to_expr"
+        __FILE__ __LINE__
+        [(p2s self#l#toPretty);
+         "known pointers: ";
+         (p2s (pretty_print_list knownpointers
+                 (fun v -> v#toPretty) "[" ", " "]"))] in
     match knownpointers with
     (* one known pointer, must be the base *)
     | [base] when self#f#env#is_initial_stackpointer_value base ->

CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml

@@ -494,17 +494,42 @@ object (self)
         match result#singleton with
         | Some ixty -> Some (bcd#get_typ ixty)
         | _ ->
-           begin
-             log_evaluation ();
-             log_diagnostics_result
-               ~tag:("top type constant in join for " ^ faddr)
-               __FILE__ __LINE__
-               [iaddr ^ " -- " ^ (register_to_string reg) ^ ": "
-                ^ (p2s (pretty_print_list
-                          (List.map bcd#get_typ result#toList)
-                          (fun ty -> STR (btype_to_string ty)) "[" "; " "]"))];
-             None
-           end
+           match result#toList with
+           | [ixty1; ixty2] ->
+              (match (bcd#get_typ ixty1), (bcd#get_typ ixty2) with
+               | TPtr (tty1, _), TPtr (tty2, _)
+                    when is_struct_type tty1 && is_scalar tty2 ->
+                  Some (bcd#get_typ ixty1)
+               | TPtr (tty1, _), TPtr (tty2, _)
+                    when is_struct_type tty2 && is_scalar tty1 ->
+                  Some (bcd#get_typ ixty2)
+               | _ ->
+                  begin
+                    log_evaluation ();
+                    log_diagnostics_result
+                      ~tag:("top type constant in join for " ^ faddr)
+                      __FILE__ __LINE__
+                      [iaddr ^ " -- " ^ (register_to_string reg) ^ ": "
+                       ^ (p2s (pretty_print_list
+                                 (List.map bcd#get_typ result#toList)
+                                 (fun ty -> STR (btype_to_string ty))
+                                 "[" "; " "]"))];
+                    None
+                  end)
+           | _ ->
+              begin
+                log_evaluation ();
+                log_diagnostics_result
+                  ~tag:("top type constant in join for " ^ faddr)
+                  __FILE__ __LINE__
+                  [iaddr ^ " -- " ^ (register_to_string reg) ^ ": "
+                   ^ (p2s (pretty_print_list
+                             (List.map bcd#get_typ result#toList)
+                             (fun ty -> STR (btype_to_string ty))
+                             "[" "; " "]"))];
+                None
+              end
+
     end
 
   method resolve_stack_lhs_type