diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml index d49d67fe..de771878 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml +++ b/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 diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml index a9ae102f..e61e3541 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml +++ b/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 diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml index f81d963f..ab884607 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml +++ b/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 = diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml index 939750b7..d3f96775 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml +++ b/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__)) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 234a000f..9187e4ed 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/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 diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 05a5d856..caf06b66 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/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 diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 54a81386..227bcd78 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/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 []