diff --git a/CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml b/CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml index 3635b2b6..74677176 100644 --- a/CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml +++ b/CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml @@ -54,6 +54,8 @@ open BCHNumericalConstraints module H = Hashtbl module TR = CHTraceResult +let p2s = CHPrettyUtil.pretty_to_string + module ConstraintCollections = CHCollections.Make (struct @@ -442,17 +444,19 @@ let extract_valuesets H.iter (fun k v -> if H.mem v "valuesets" then let inv = H.find v "valuesets" in - let flocinv = finfo#finv#get_location_invariant k in let domain = inv#getDomain "valuesets" in let varObserver = domain#observer#getNonRelationalVariableObserver in let vars = domain#observer#getObservedVariables in - let knownvars = flocinv#get_known_variables in - let vars = - List.filter (fun v -> - not (v#isTmp || List.mem v knownvars)) vars in + let vars = List.filter (fun v -> not v#isTmp) vars in List.iter (fun (v:variable_t) -> let valueset = (varObserver v)#toValueSet in - if valueset#isTop then () else + if valueset#isTop then + let _ = + log_diagnostics_result + ~tag:"value-sets: top" + __FILE__ __LINE__ [k ^ ": " ^ (p2s v#toPretty)] in + () + else if valueset#removeZeroOffset#isSingleBase then let (base,offset) = valueset#removeZeroOffset#getSingleBase in let canbenull:bool = valueset#includesZero in diff --git a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml index 40943541..8a133c37 100644 --- a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml +++ b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml @@ -195,10 +195,16 @@ object (self) ~(tgtbtype: btype_t option) (c: bcompinfo_t) (xoffset: xpr_t): memory_offset_t traceresult = + let is_void_tgtbtype = + match tgtbtype with + | Some (TVoid _) -> true + | _ -> false in let check_tgttype_compliance (t: btype_t) (s: int) = match tgtsize, tgtbtype with | None, None -> true | Some size, None -> size = s + | Some size, Some (TVoid _) -> size = s + | None, Some (TVoid _) -> true | None, Some ty -> btype_equal ty t | Some size, Some ty -> size = s && btype_equal ty t in let compliance_failure (t: btype_t) (s: int) = @@ -246,7 +252,10 @@ object (self) let offset = offset - foff in tbind (fun fldtype -> - if offset = 0 + if offset = 0 && is_void_tgtbtype then + Ok (Some (FieldOffset + ((finfo.bfname, finfo.bfckey), NoOffset))) + else if offset = 0 && (is_scalar fldtype) && (check_tgttype_compliance fldtype sz) then Ok (Some (FieldOffset @@ -305,6 +314,47 @@ object (self) Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" ^ " xoffset: " ^ (x2s xoffset) ^ "; btype: " ^ (btype_to_string btype)] + | XOp (XPlus, [XOp (XMult, [XConst (IntConst n); XVar v]); + XConst (IntConst m)]) when is_struct_type btype -> + let compinfo = get_struct_type_compinfo btype in + let fldoffset = XConst (IntConst m) in + let memoffset_r = + self#get_field_memory_offset_at + ~tgtsize:None ~tgtbtype:None compinfo fldoffset in + TR.tbind + (fun memoffset -> + match memoffset with + | FieldOffset ((fname, fckey), NoOffset) -> + let fcinfo = get_compinfo_by_key fckey in + let field = get_compinfo_field fcinfo fname in + let fieldtype = field.bftype in + if is_array_type fieldtype then + let eltype = get_element_type fieldtype in + let elsize_r = size_of_btype eltype in + TR.tbind + (fun elsize -> + if elsize = n#toInt then + let aoffset = ArrayIndexOffset (XVar v, NoOffset) in + let moffset = + BCHMemoryReference.add_offset memoffset aoffset in + Ok moffset + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" + ^ "field: " ^ fname + ^ "; fieldtype: " ^ (btype_to_string fieldtype) + ^ "; elementsize: " ^ (string_of_int elsize) + ^ "; expected: " ^ n#toString]) + elsize_r + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "not an array type"] + | _ -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" + ^ "fldoffset: " ^ (x2s fldoffset) + ^ "; memoffset: " + ^ (BCHMemoryReference.memory_offset_to_string memoffset)]) + memoffset_r + | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" ^ " xoffset: " ^ (x2s xoffset) diff --git a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml index 0433c681..57cc1fae 100644 --- a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml +++ b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml @@ -58,9 +58,13 @@ module H = Hashtbl module TR = CHTraceResult -(* let x2p = XprToPretty.xpr_formatter#pr_expr *) +let x2p = XprToPretty.xpr_formatter#pr_expr let tracked_locations = [] +let p2s = CHPrettyUtil.pretty_to_string +let x2s x = p2s (x2p x) + + let track_location loc p = if List.mem loc tracked_locations then chlog#add ("tracked:" ^ loc) p @@ -1068,6 +1072,11 @@ object (self) (self#get_location_invariant iaddr)#add_fact fact method add_symbolic_expr_fact (iaddr:string) (v:variable_t) (x:xpr_t) = + let _ = + log_diagnostics_result + ~tag:("add symbolic-expr fact for " ^ iaddr) + __FILE__ __LINE__ + [(p2s v#toPretty) ^ ": " ^ (x2s x)] in self#add iaddr (NonRelationalFact (v,FSymbolicExpr x)) method set_unreachable (iaddr:string) (domain:string) = @@ -1091,6 +1100,13 @@ object (self) (base:symbol_t) (i:interval_t) (canbenull:bool) = + let _ = + log_diagnostics_result + ~tag:("add valueset fact for " ^ iaddr) + __FILE__ __LINE__ + [(p2s v#toPretty) ^ ": " + ^ "base: " ^ (p2s base#toPretty) + ^ "; offset: " ^ (p2s i#toPretty)] in let fact = if i#isBottom then Unreachable "valuesets" diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 60d791e5..b47fb17a 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20250401" - ~date:"2025-04-01" + ~version:"0.6.0_20250417" + ~date:"2025-04-17" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml index 592c3885..cbe1d707 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstructions.ml @@ -26,6 +26,7 @@ ============================================================================= *) (* chlib *) +open CHNumerical open CHPretty (* chutil *) @@ -34,8 +35,13 @@ open CHPrettyUtil open CHTraceResult open CHXmlDocument +(* xprlib *) +open Xprt +open XprTypes + (* bchlib *) open BCHBasicTypes +open BCHBCTypePretty open BCHByteUtilities open BCHDataBlock open BCHDoubleword @@ -61,6 +67,9 @@ open BCHDisassembleThumbInstruction module H = Hashtbl module TR = CHTraceResult +let x2p = XprToPretty.xpr_formatter#pr_expr +let p2s = CHPrettyUtil.pretty_to_string +let x2s x = p2s (x2p x) let numArrays = 1000 let arrayLength = 100000 @@ -676,6 +685,67 @@ object (self) ^ " String:<" ^ (fixed_length_string v#to_hex_string 12) ^ "> ... (cont'd)" + + else if Option.is_some (memorymap#containing_location a) then + match memorymap#containing_location a with + | None -> "" + | Some gloc -> + let xprv = num_constant_expr a#to_numerical in + let offset_r = gloc#address_offset xprv in + TR.tfold_default + (fun offset -> + match offset with + | XConst (IntConst n) when n#equal numerical_zero -> + " " + ^ (fixed_length_string addr 10) + ^ " Global variable:<" + ^ gloc#name + ^ ": " + ^ (btype_to_string gloc#btype) + ^ ">" + ^ "\n " + ^ (fixed_length_string addr 10) + ^ " GV:<" + ^ gloc#name + ^ ":0 >: " + ^ v#to_hex_string + | XConst (IntConst n) -> + " " + ^ (fixed_length_string addr 10) + ^ " GV:<" + ^ gloc#name + ^ ":" + ^ (fixed_length_string n#toString 3) + ^ ">: " + ^ v#to_hex_string + | _ -> + " " + ^ (fixed_length_string addr 10) + ^ " GV:<" + ^ gloc#name + ^ ":" + ^ (x2s offset) + ^ ">: " + ^ v#to_hex_string) + (" " + ^ (fixed_length_string addr 10) + ^ " GV:<" + ^ gloc#name + ^ ":?>: " + ^ v#to_hex_string) + offset_r + + else if memorymap#has_elf_symbol v then + let name = memorymap#get_elf_symbol v in + " " + ^ (fixed_length_string addr 10) + ^ " Sym:<" + ^ v#to_hex_string + ^ ":" + ^ name + ^ ">" + ^ datarefstr + else if v#equal wordzero then " " ^ (fixed_length_string addr 10) @@ -684,6 +754,7 @@ object (self) " " ^ (fixed_length_string addr 10) ^ " <0xffffffff>" + else if functions_data#is_function_entry_point v then let name = if functions_data#has_function_name v then @@ -698,16 +769,7 @@ object (self) ^ name ^ ">" ^ datarefstr - else if memorymap#has_elf_symbol v then - let name = memorymap#get_elf_symbol v in - " " - ^ (fixed_length_string addr 10) - ^ " Sym:<" - ^ v#to_hex_string - ^ ":" - ^ name - ^ ">" - ^ datarefstr + else if elf_header#is_code_address v then " " ^ (fixed_length_string addr 10) diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index a4dde9b9..3f5e0448 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -649,9 +649,11 @@ object (self) match xx with | XVar _ -> xx | _ -> - TR.tfold_default - (fun v -> XOp ((Xf "addressofvar"), [(XVar v)])) - xx + TR.tfold + ~ok:(fun v -> XOp ((Xf "addressofvar"), [(XVar v)])) + ~error:(fun e -> + let _ = log_dc_error_result __FILE__ __LINE__ e in + xx) (floc#get_var_at_address ~btype:(ptr_deref ptype) xx) else xx in @@ -770,21 +772,23 @@ object (self) let xrm_r = rm#to_expr floc in let result_r = TR.tmap2 (fun xrn xrm -> XOp (XPlus, [xrn; xrm])) xrn_r xrm_r in + let xxrn_r = TR.tmap rewrite_expr xrn_r in + let xxrm_r = TR.tmap rewrite_expr xrm_r in let rresult_r = TR.tmap rewrite_expr result_r in + let cresult_r = + TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in let _ = TR.tfold_default (fun r -> ignore (get_string_reference floc r)) () rresult_r in - let rdefs = [get_rdef_r xrn_r; get_rdef_r xrm_r] in - let uses = get_def_use_r vrd_r in - let useshigh = get_def_use_high_r vrd_r in + let rdefs = + [get_rdef_r xrn_r; get_rdef_r xrm_r] @ (get_all_rdefs_r rresult_r) in + let uses = [get_def_use_r vrd_r] in + let useshigh = [get_def_use_high_r vrd_r] in + let vars_r = [vrd_r] in + let xprs_r = [xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r] in + let cxprs_r = [cresult_r] in let (tagstring, args) = - mk_instrx_data_r - ~vars_r:[vrd_r] - ~xprs_r:[xrn_r; xrm_r; result_r; rresult_r] - ~rdefs:rdefs - ~uses:[uses] - ~useshigh:[useshigh] - () in + mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in let (tags, args) = add_optional_instr_condition tagstring args c in (tags, args) @@ -2285,6 +2289,8 @@ object (self) let xrm_r = rm#to_expr floc in let result_r = TR.tmap2 (fun xrn xrm -> XOp (XMinus, [xrm; xrn])) xrn_r xrm_r in + let xxrn_r = TR.tmap rewrite_expr xrn_r in + let xxrm_r = TR.tmap rewrite_expr xrm_r in let rresult_r = TR.tmap rewrite_expr result_r in let cresult_r = TR.tbind (floc#convert_xpr_to_c_expr ~size:(Some 4)) rresult_r in @@ -2293,7 +2299,7 @@ object (self) let uses = [get_def_use_r vrd_r] in let useshigh = [get_def_use_high_r vrd_r] in let vars_r = [vrd_r] in - let xprs_r = [xrn_r; xrm_r; result_r; rresult_r] in + let xprs_r = [xrn_r; xrm_r; result_r; rresult_r; xxrn_r; xxrm_r] in let cxprs_r = [cresult_r] in let (tagstring, args) = mk_instrx_data_r ~vars_r ~xprs_r ~cxprs_r ~rdefs ~uses ~useshigh () in diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 17701e49..c466ac9d 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -2345,7 +2345,10 @@ let translate_arm_instruction if rl#includes_pc then match rtype with | TVoid _ -> [] - | _ -> [floc#f#env#mk_arm_register_variable AR0] + | _ -> + let r0_op = arm_register_op AR0 RD in + let xr0 = r0_op#to_expr floc in + get_use_high_vars_r [xr0] else [] in let popdefcmds =