Typereconstruction

CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml

@@ -522,21 +522,29 @@ and size_of_btype_array (t: btype_t) (len: bexp_t): int traceresult =
 
 
 and size_of_btype_comp (comp: bcompinfo_t): int traceresult =
-  if comp.bcstruct then
-    let lastoff =
-      List.fold_left (fun acc_r finfo ->
-          tbind (fun acc -> offset_of_field_acc ~finfo ~acc) acc_r)
-        (Ok start_oa) comp.bcfields in
-    let size =
-      tmap2 (fun o a -> add_trailing o.oa_first_free a)
-        lastoff (align_of_btype (TComp (comp.bckey, []))) in
-    size
-  else    (* union *)
-    let fieldsizes =
-      List.map (fun finfo -> size_of_btype finfo.bftype) comp.bcfields in
-    let size =
-      tfold_list_fail (fun mx a -> if a > mx then a else mx) (Ok 0) fieldsizes in
-    size
+  let size =
+    if comp.bcstruct then
+      let lastoff =
+        List.fold_left (fun acc_r finfo ->
+            tbind (fun acc -> offset_of_field_acc ~finfo ~acc) acc_r)
+          (Ok start_oa) comp.bcfields in
+      let size =
+        tmap2 (fun o a -> add_trailing o.oa_first_free a)
+          lastoff (align_of_btype (TComp (comp.bckey, []))) in
+      size
+    else    (* union *)
+      let fieldsizes =
+        List.map (fun finfo -> size_of_btype finfo.bftype) comp.bcfields in
+      let size =
+        tfold_list_fail (fun mx a -> if a > mx then a else mx) (Ok 0) fieldsizes in
+      size in
+  tbind
+    (fun size ->
+      if size = 0 then
+        Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
+               ^ "zero size for compinfo: " ^ comp.bcname]
+      else
+        Ok size) size
 
 
 and offset_of_field_acc

CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml

@@ -77,6 +77,8 @@ object (self)
       && (match instr#get_opcode with
           | Branch _ | BranchExchange _ -> false
           | Compare _ | CompareNegative _ -> false
+          | Move (_, _, rd, rm, _, _) when rm#is_register ->
+             not (rd#get_register = rm#get_register)
           | _ -> true)
       && (Option.is_none instr#is_in_aggregate) in
     begin

CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml

@@ -573,22 +573,27 @@ object (self)
     end
 
   method write_xml (node:xml_element_int) =
+    let subnodes = ref [] in
     let bnode = ref (xmlElement "b") in
-    self#itera
-      (fun va instr ->
-        if instr#is_valid_instruction then
-          let _ =
-            if instr#is_block_entry then
-              begin
-                bnode := xmlElement "b";
-                (!bnode)#setAttribute "ba" va#to_hex_string;
-                node#appendChildren [!bnode]
-              end in
-          let inode = xmlElement "i" in
-          begin
-            instr#write_xml inode;
-            (!bnode)#appendChildren [inode]
-          end)
+    begin
+      self#itera
+        (fun va instr ->
+          if instr#is_valid_instruction then
+            let _ =
+              if instr#is_block_entry then
+                begin
+                  bnode := xmlElement "b";
+                  (!bnode)#setAttribute "ba" va#to_hex_string;
+                  (* node#appendChildren [!bnode] *)
+                  subnodes := !bnode :: !subnodes
+                end in
+            let inode = xmlElement "i" in
+            begin
+              instr#write_xml inode;
+              (!bnode)#appendChildren [inode]
+            end);
+      node#appendChildren (List.rev !subnodes)
+    end
 
   method private not_code_to_string
                    (datarefstr: doubleword_int -> string) (nc: not_code_t): string =

CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml

@@ -443,7 +443,7 @@ object (self:'a)
              Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
                     ^ "offset type "
                     ^ (arm_memory_offset_to_string offset)
-                    ^ "not covered for offset address update"]
+                    ^ " not covered for offset address update"]
           | Some inc ->
              TR.tmap
                ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

@@ -1770,9 +1770,11 @@ object (self)
                ~ok:(fun (inc, xaddr) ->
                  add_base_update tags args vrn_r inc (Ok xaddr))
                ~error:(fun e ->
+                 let xaddr_r =
+                   Error (e @ [__FILE__ ^ ":" ^ (string_of_int __LINE__)]) in
                  begin
                    log_dc_error_result __FILE__ __LINE__ e;
-                   (tags, args)
+                   add_base_update tags args vrn_r 0 xaddr_r
                  end)
                (mem#to_updated_offset_address floc)
            else
@@ -1920,7 +1922,7 @@ object (self)
          let uses = [get_def_use_r vrt_r] in
          let useshigh = [get_def_use_high_r vrt_r] in
          let xxaddr_r = TR.tmap rewrite_expr xaddr_r in
-         let cxaddr_r = TR.tbind floc#xpr_to_cxpr xxaddr_r in
+         let cxaddr_r = TR.tbind (floc#xpr_to_cxpr ~size:(Some 2)) xxaddr_r in
          let xrmem_r = TR.tmap rewrite_expr xmem_r in
          let cxrmem_r =
            TR.tbind (floc#xpr_to_cxpr ~size:(Some 2)) xrmem_r in
@@ -3054,9 +3056,11 @@ object (self)
                ~ok:(fun (inc, xaddr) ->
                  add_base_update tags args vrn_r inc (Ok xaddr))
                ~error:(fun e ->
+                 let xaddr_r =
+                   Error (e @ [__FILE__ ^ ":" ^ (string_of_int __LINE__)]) in
                  begin
                    log_dc_error_result __FILE__ __LINE__ e;
-                   (tags, args)
+                   add_base_update tags args vrn_r 0 xaddr_r
                  end)
                (mem#to_updated_offset_address floc)
            else

CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml

@@ -501,7 +501,7 @@ object (self)
             log_subtype_rule_disabled __LINE__ rule tctypeterm lhstypeterm)
        end
 
-    | BitwiseNot (_, _, rd, rm, _) ->
+    | BitwiseNot (_, _, rd, rm, _) when rm#is_register->
        let rdreg = rd#to_register in
        let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in
        let rmdefs = get_variable_rdefs_r (rm#to_variable floc) in

CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml

@@ -2059,7 +2059,7 @@ let translate_arm_instruction
    *    APSR.N = result<31>;
    *    APSR.Z = IsZeroBit(result);
    * ------------------------------------------------------------------------ *)
-  | Move _ when instr#is_aggregate_anchor ->
+  | Move (_, _, rd, _, _, _) when instr#is_aggregate_anchor ->
      (match get_associated_test_instr finfo ctxtiaddr with
       | Some (testloc, testinstr) ->
          let movagg = get_aggregate loc#i in
@@ -2145,11 +2145,17 @@ let translate_arm_instruction
                (BCH_failure
                   (LBLOCK [floc#l#toPretty; STR ": Unknown MOV aggregate kind"])))
       | _ ->
+         (* no predicate found *)
+         let vrd = floc#env#mk_register_variable rd#to_register in
+         let lhs_r = TR.tmap fst (rd#to_lhs floc) in
+         let cmds = floc#get_abstract_commands_r lhs_r in
+         let defcmds = floc#get_vardef_commands ~defs:[vrd] ctxtiaddr in
+         let cmds = defcmds @ cmds in
          let _ =
            chlog#add
              "predicate assignment aggregate without predicate"
              (LBLOCK [loc#toPretty; STR ": "; instr#toPretty]) in
-         default [])
+         default cmds)
 
   | Move _ when Option.is_some instr#is_in_aggregate ->
      default []