diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml index de771878..bb663abc 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.ml @@ -229,9 +229,11 @@ let is_float_double t = match t with TFloat (FDouble, _, _) -> true | _ -> false let is_pointer t = match t with TPtr _ -> true | _ -> false +let is_char_pointer t = match t with TPtr (TInt (IChar, _), _) -> true | _ -> false + let is_void_pointer t = match t with TPtr (TVoid _, _) -> true | _ -> false -let is_scalar t = (is_int t) || (is_float t) || (is_pointer t) +let is_scalar t = (is_int t) || (is_float t) || (is_pointer t) || (is_enum t) let is_pointer_to_struct t = match t with TPtr (TComp _,_) -> true | _ -> false diff --git a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli index 035ffb46..29d9975d 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli +++ b/CodeHawk/CHB/bchlib/bCHBCTypeUtil.mli @@ -147,6 +147,7 @@ val is_float_float: btype_t -> bool val is_float_double: btype_t -> bool val is_scalar: btype_t -> bool val is_pointer: btype_t -> bool +val is_char_pointer: btype_t -> bool val is_void_pointer: btype_t -> bool val is_unsigned: btype_t -> bool (* true if unsigned, false if signed or unknown *) val is_function_type: btype_t -> bool diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index d79bc23d..0d576a6a 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -668,16 +668,19 @@ object (self) ?(size=4) (var: variable_t) (numoffset: numerical_t): variable_t traceresult = - let _ = - log_diagnostics_result - ~msg:(p2s self#l#toPretty) - ~tag:"get-memory-variable-numoffset" - __FILE__ __LINE__ - ["size: " ^ (string_of_int size); - "var: " ^ (p2s var#toPretty); - "numoffset: " ^ (numoffset#toString)] in - let inv = self#inv in - let mk_memvar memref_r memoffset_r = + let varx = + if align > 1 then + let alignx = int_constant_expr align in + XOp (XMult, [XOp (XDiv, [XVar var; alignx]); alignx]) + else + XVar var in + + let inv = self#inv in + let addr = XOp (XPlus, [varx; num_constant_expr numoffset]) in + let address = simplify_xpr (inv#rewrite_expr addr) in + let tresult = + (* + let _mk_memvar memref_r memoffset_r = let _ = log_diagnostics_result ~msg:(p2s self#l#toPretty) @@ -685,7 +688,8 @@ object (self) __FILE__ __LINE__ ["var: " ^ (p2s var#toPretty); "memref_r: " - ^ (TR.tfold_default (fun memref -> p2s memref#toPretty) "error" memref_r); + ^ (TR.tfold_default + (fun memref -> p2s memref#toPretty) "error" memref_r); "memoff_r: " ^ (TR.tfold_default memory_offset_to_string "error" memoffset_r)] in TR.tbind @@ -707,11 +711,33 @@ object (self) TR.tbind ~msg:(eloc __LINE__) (fun numoff -> + if self#f#stackframe#has_stackslot numoff#toInt then + let stackslot = + Option.get ( + self#f#stackframe#containing_stackslot numoff#toInt) in + match stackslot#size with + | Some slotsize when size = slotsize -> + Ok (self#f#env#mk_stackslot_variable stackslot NoOffset) + | Some slotsize -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Size of stackslot at offset " ^ (i2s numoff#toInt) + ^ ": " ^ (i2s slotsize)] + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Stackslot at offset " ^ (i2s numoff#toInt) + ^ " does not have a size"] + else + Error [(eloc __LINE__); + (p2s self#l#toPretty); + "No stackslot found at offset " ^ (i2s numoff#toInt)]) + (* if Option.is_some (self#f#stackframe#containing_stackslot numoff#toInt) then (self#env#mk_stack_variable finfo#stackframe numoff) else - Ok (self#env#mk_offset_memory_variable memref memoff)) + Ok (self#env#mk_offset_memory_variable memref memoff)) *) (get_total_constant_offset memoff)) memoffset_r else @@ -720,8 +746,8 @@ object (self) (fun memoff -> (self#env#mk_offset_memory_variable memref memoff)) memoffset_r) - memref_r in - + memref_r in *) +(* if inv#is_base_offset_constant var then let (base, offset) = inv#get_base_offset_constant var in let memoffset = numoffset#add offset in @@ -729,7 +755,7 @@ object (self) let memoff_r = Ok (ConstantOffset (memoffset, NoOffset)) in mk_memvar memref_r memoff_r - else + else *) let varx = if align > 1 then let alignx = int_constant_expr align in @@ -754,7 +780,23 @@ object (self) ^ system_info#get_image_base#to_hex_string ^ ")"] | _ -> - self#get_var_at_address ~size:(Some size) address + self#get_var_at_address ~size:(Some size) address in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_memory_variable_numoffset" + __FILE__ __LINE__ + ["size: " ^ (string_of_int size); + "var: " ^ (p2s var#toPretty); + "numoffset: " ^ (numoffset#toString); + "address: " ^ (x2s addr) ^ " (" ^ (x2s address) ^ ")"; + "tresult: " + ^ (TR.tfold + ~ok:(fun cv -> p2s cv#toPretty) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method get_memory_variable_1 ?(align=1) (* alignment of var value *) @@ -844,29 +886,23 @@ object (self) let addr = XOp (XPlus, [XVar var1; XVar var2]) in let addr = XOp (XPlus, [addr; num_constant_expr offset]) in let address = simplify_xpr (self#inv#rewrite_expr addr) in - let (memref_r, memoff_r) = self#decompose_memaddr address in - TR.tbind - ~msg:(eloc __LINE__) - (fun memref -> - if memref#is_global_reference then - TR.tbind - ~msg:((elocm __LINE__) ^ "memref:global") - (fun memoff -> - TR.tbind - ~msg:(eloc __LINE__) - (self#env#mk_global_variable ~size self#l) - (get_total_constant_offset memoff)) - memoff_r - else - TR.tbind - ~msg:(eloc __LINE__) - (fun memoff -> - TR.tmap - ~msg:(eloc __LINE__) - (self#env#mk_memory_variable memref) - (get_total_constant_offset memoff)) - memoff_r) - memref_r + let tresult = self#get_var_at_address ~size:(Some size) address in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_memory_variable_varoffset" + __FILE__ __LINE__ + ["size: " ^ (string_of_int size); + "var1: " ^ (p2s var1#toPretty); + "var2: " ^ (p2s var2#toPretty); + "offset: " ^ offset#toString; + "tresult: " + ^ (TR.tfold + ~ok:(fun v -> p2s v#toPretty) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method get_memory_variable_2 ?(size=4) (var1:variable_t) (var2:variable_t) (offset:numerical_t) = @@ -906,22 +942,24 @@ object (self) XOp (XPlus, [addr; XOp (XMult, [int_constant_expr scale; indexexpr])]) in let address = simplify_xpr (self#inv#rewrite_expr addr) in - let (memref_r, memoff_r) = self#decompose_memaddr address in - TR.tbind - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun memref -> - if memref#is_global_reference then - self#get_var_at_address ~size:(Some size) address - else - TR.tbind - ~msg:(eloc __LINE__) - (fun memoff -> - TR.tmap - ~msg:(eloc __LINE__) - (self#env#mk_memory_variable memref) - (get_total_constant_offset memoff)) - memoff_r) - memref_r + let tresult = self#get_var_at_address ~size:(Some size) address in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_memory_variable_scaledoffset" + __FILE__ __LINE__ + ["size: " ^ (string_of_int size); + "base: " ^ p2s base#toPretty; + "index: " ^ p2s index#toPretty; + "scale: " ^ (string_of_int scale); + "offset: " ^ offset#toString; + "tresult: " + ^ (TR.tfold + ~ok:(fun v -> p2s v#toPretty) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method get_memory_variable_3 ?(size=4) @@ -1051,10 +1089,6 @@ object (self) (self#f#env#is_initial_memory_value v) || (self#env#is_initial_register_value v) - (* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * - * esp offset * - * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *) - method get_singleton_stackpointer_offset: numerical_t traceresult = let arch = system_settings#get_architecture in let roffset = self#get_stackpointer_offset arch in @@ -1067,10 +1101,10 @@ object (self) | (level, _) -> Error [(elocm __LINE__) ^ ": level: " ^ (string_of_int level)] - method get_stackpointer_offset arch = + method get_stackpointer_offset (arch: string): (int * interval_t) = match arch with - | "x86" -> self#get_esp_offset - | "mips" -> self#get_sp_offset + | "x86" -> self#get_x86_esp_offset + | "mips" -> self#get_mips_sp_offset | "arm" -> self#get_arm_sp_offset | "pwr" -> self#get_pwr_sp_offset | _ -> @@ -1078,7 +1112,53 @@ object (self) (BCH_failure (LBLOCK [STR "Architecture not recognized: "; STR arch])) - method stackpointer_offset_to_string arch = + method get_stackpointer_offset_xpr (x: xpr_t): xpr_t traceresult = + let arch = system_settings#get_architecture in + match arch with + | "x86" -> self#get_x86_stackpointer_offset_xpr x + | "mips" -> self#get_mips_stackpointer_offset_xpr x + | "arm" -> self#get_arm_stackpointer_offset_xpr x + | "pwr" -> Error [(elocm __LINE__) ^ "not yet implemented"] + | _ -> + Error [(elocm __LINE__) ^ "architecture " ^ arch ^ " not recognized"] + + method private get_x86_stackpointer_offset_xpr (x: xpr_t): xpr_t traceresult = + let spreg = CPURegister Esp in + let sp0 = self#env#mk_initial_register_value ~level:0 spreg in + let x = simplify_xpr (self#inv#rewrite_expr x) in + let vars = vars_as_positive_terms x in + if not (List.exists (fun v -> v#equal sp0) vars) then + Error [(elocm __LINE__); + "expression " ^ (x2s x) + ^ "does not include stackpointer " ^ (x2s (XVar sp0))] + else + Ok (simplify_xpr (XOp (XMinus, [x; XVar sp0]))) + + method private get_arm_stackpointer_offset_xpr (x: xpr_t): xpr_t traceresult = + let spreg = ARMRegister ARSP in + let sp0 = self#env#mk_initial_register_value ~level:0 spreg in + let x = simplify_xpr (self#inv#rewrite_expr x) in + let vars = vars_as_positive_terms x in + if not (List.exists (fun v -> v#equal sp0) vars) then + Error [(elocm __LINE__); + "expression " ^ (x2s x) + ^ " does not include stackpointer " ^ (x2s (XVar sp0))] + else + Ok (simplify_xpr (XOp (XMinus, [x; XVar sp0]))) + + method private get_mips_stackpointer_offset_xpr (x: xpr_t): xpr_t traceresult = + let spreg = MIPSRegister MRsp in + let sp0 = self#env#mk_initial_register_value ~level:0 spreg in + let x = simplify_xpr (self#inv#rewrite_expr x) in + let vars = vars_as_positive_terms x in + if not (List.exists (fun v -> v#equal sp0) vars) then + Error [(elocm __LINE__); + "expression " ^ (x2s x) + ^ " does not include stackpointer " ^ (x2s (XVar sp0))] + else + Ok (simplify_xpr (XOp (XMinus, [x; XVar sp0]))) + + method stackpointer_offset_to_string (arch: string) = match arch with | "x86" -> self#esp_offset_to_string | "mips" -> self#sp_offset_to_string @@ -1089,7 +1169,7 @@ object (self) (BCH_failure (LBLOCK [STR "Architecture not recognized: "; STR arch])) - method private get_esp_offset = (* specific to x86 *) + method private get_x86_esp_offset: (int * interval_t) = let inv = self#inv in let espreg = CPURegister Esp in let esp = self#env#mk_register_variable espreg in @@ -1105,7 +1185,7 @@ object (self) else (0,esp0Offset) - method private get_sp_offset = (* specific to mips *) + method private get_mips_sp_offset: (int * interval_t) = let inv = self#inv in let spreg = MIPSRegister MRsp in let sp = self#env#mk_register_variable spreg in @@ -1121,7 +1201,7 @@ object (self) else (0,sp0Offset) - method private get_arm_sp_offset = (* specific to arm *) + method private get_arm_sp_offset: (int * interval_t) = let inv = self#inv in let spreg = ARMRegister ARSP in let sp = self#env#mk_register_variable spreg in @@ -1137,7 +1217,7 @@ object (self) else (0, sp0Offset) - method private get_pwr_sp_offset = (* specific to power32 *) + method private get_pwr_sp_offset: (int * interval_t) = let inv = self#inv in let spreg = PowerGPRegister 1 in let sp = self#env#mk_register_variable spreg in @@ -1154,7 +1234,7 @@ object (self) (0, sp0Offset) method private esp_offset_to_string = - let (level,offset) = self#get_esp_offset in + let (level,offset) = self#get_x86_esp_offset in let openB = string_repeat "[" (level+1) in let closeB = string_repeat "]" (level+1) in let offset = if offset#isTop then " ? " else @@ -1169,7 +1249,7 @@ object (self) openB ^ " " ^ offset ^ " " ^ closeB method private sp_offset_to_string = - let (level,offset) = self#get_sp_offset in + let (level,offset) = self#get_mips_sp_offset in let openB = string_repeat "[" (level+1) in let closeB = string_repeat "]" (level+1) in let offset = if offset#isTop then " ? " else @@ -1261,23 +1341,15 @@ object (self) method get_fts_parameter_expr (_p: fts_parameter_t) = None - method private normalize_addrvalue (x: xpr_t): xpr_t = - simplify_xpr x - method get_var_at_address ?(size=None) ?(btype=t_unknown) (addrvalue: xpr_t): variable_t traceresult = - let _ = - log_diagnostics_result - ~msg:(p2s self#l#toPretty) - ~tag:"get_var_at_address" - __FILE__ __LINE__ - ["addrvalue: " ^ (x2s addrvalue); - "btype: " ^ (btype_to_string btype); - "size: " ^ (opti2s size)] in - - match self#normalize_addrvalue addrvalue with + (* Note: the expression &v (addressofvar v) may be introduced by rewriting + against an invariant. Assign_commands converts some addresses to addressofvar + expressions.*) + let tresult = + match (simplify_xpr addrvalue) with | XOp ((Xf "addressofvar"), [XVar v]) when self#env#is_global_variable v -> let gvaddr_r = self#f#env#get_global_variable_address v in TR.tbind @@ -1293,10 +1365,9 @@ object (self) ~tgtsize:size ~tgtbtype:btype self#l zero_constant_expr) in varresult else - Error[(elocm __LINE__) - ^ (p2s self#l#toPretty) - ^ ": " - ^ "Global location at address " + Error[(elocm __LINE__); + (p2s self#l#toPretty); + "Global location at address " ^ gvaddr#to_hex_string ^ " not found"]) gvaddr_r @@ -1304,13 +1375,13 @@ object (self) | XOp (XPlus, [XOp ((Xf "addressofvar"), [XVar v]); xoff]) when self#f#env#is_global_variable v -> let gvaddr_r = self#f#env#get_global_variable_address v in - let cxoff_r = self#xpr_to_cxpr xoff in + let cxoff_r = self#xpr_to_cxpr xoff in (* **should we have this call? *) TR.tbind ~msg:(eloc __LINE__) (fun gvaddr -> if memmap#has_location gvaddr then let gloc = memmap#get_location gvaddr in - let varresult = + let var_r = TR.tmap ~msg:(eloc __LINE__) (fun offset -> self#f#env#mk_gloc_variable gloc offset) @@ -1322,18 +1393,17 @@ object (self) let _ = log_diagnostics_result ~msg:(p2s self#l#toPretty) - ~tag:"normalized global address" + ~tag:"get_var_at_address: addressofvar global" __FILE__ __LINE__ ["varresult: " - ^ (TR.tfold_default (fun v -> p2s v#toPretty) "error" varresult); + ^ (TR.tfold_default (fun v -> p2s v#toPretty) "error" var_r); "gloc: " ^ gloc#name] in - varresult + var_r else - Error [(elocm __LINE__) - ^ (p2s self#l#toPretty) - ^ ": " - ^ "Global location at address " + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Global location at address " ^ gvaddr#to_hex_string ^ " not found"]) gvaddr_r @@ -1346,12 +1416,69 @@ object (self) (gloc#address_memory_offset ~tgtsize:size ~tgtbtype:btype self#l addrvalue)) | _ -> - let (memref_r, memoff_r) = self#decompose_memaddr addrvalue in - TR.tmap2 - ~msg1:(eloc __LINE__) - (fun memref memoff -> - self#f#env#mk_offset_memory_variable memref memoff) - memref_r memoff_r + match self#f#stackframe#xpr_containing_stackslot addrvalue with + | Some stackslot -> + let stackoffset_r = self#get_stackpointer_offset_xpr addrvalue in + (TR.tmap + ~msg:(eloc __LINE__) + (fun offset -> + self#f#env#mk_stackslot_variable stackslot offset) + (TR.tbind + ~msg:(eloc __LINE__) + (stackslot#frame_offset_memory_offset + ~tgtsize:size ~tgtbtype:btype self#l) + stackoffset_r)) + | _ -> + let (memref_r, memoff_r) = self#decompose_memaddr addrvalue in + TR.tbind2 + ~msg1:(eloc __LINE__) + (fun memref memoff -> + let _ = + log_diagnostics_result + ~tag:"get_var_at_address:decompose_memaddr" + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["addrvalue: " ^ (x2s addrvalue); + "memref: " ^ (p2s memref#toPretty); + "memoff: " ^ (memory_offset_to_string memoff)] in + if memref#is_stack_reference then + match memoff with + | NoOffset -> + let stackslot_r = + self#f#stackframe#add_stackslot ~size 0 in + TR.tmap (fun stackslot -> + self#f#env#mk_stackslot_variable stackslot NoOffset) + stackslot_r + | ConstantOffset (num, NoOffset) -> + let stackslot_r = + self#f#stackframe#add_stackslot ~size num#toInt in + TR.tmap (fun stackslot -> + self#f#env#mk_stackslot_variable stackslot NoOffset) + stackslot_r + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Unable to create stackslot for " ^ (x2s addrvalue) + ^ " with offset " + ^ (memory_offset_to_string memoff)] + else + Ok (self#f#env#mk_offset_memory_variable memref memoff)) + memref_r memoff_r in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_var_at_address" + __FILE__ __LINE__ + ["addrvalue: " ^ (x2s addrvalue); + "btype: " ^ (btype_to_string btype); + "size: " ^ (opti2s size); + "tresult: " + ^ (TR.tfold + ~ok:(fun v -> p2s v#toPretty) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end (* deprecated. to be merged with get_var_at_address *) method get_lhs_from_address (xpr:xpr_t) = @@ -1382,6 +1509,256 @@ object (self) | _ -> default () + method private get_memory_offset_type + ?(size=4) + (basetype: btype_t) + (offset: memory_offset_t): btype_t traceresult = + let tresult = + match offset with + | NoOffset when is_pointer basetype + && (not (is_struct_type (ptr_deref basetype))) -> + Ok (ptr_deref basetype) + + | NoOffset when is_pointer basetype -> + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_memory_offset_type:struct - nooffset" + __FILE__ __LINE__ + ["size: " ^ (string_of_int size); + "basetype: " ^ (btype_to_string basetype)]; + Ok (ptr_deref basetype) + end + + | FieldOffset ((fname, ckey), NoOffset) -> + let cinfo = get_compinfo_by_key ckey in + let finfo = get_compinfo_field cinfo fname in + Ok finfo.bftype + + | FieldOffset ((fname, ckey), foff) -> + let cinfo = get_compinfo_by_key ckey in + let finfo = get_compinfo_field cinfo fname in + self#get_memory_offset_type ~size finfo.bftype foff + + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "offset " ^ (memory_offset_to_string offset) + ^ " not yet handled"] in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_memory_offset_type" + __FILE__ __LINE__ + ["size: " ^ (string_of_int size); + "basetype: " ^ (btype_to_string basetype); + "offset: " ^ (memory_offset_to_string offset); + "tresult: " + ^ (TR.tfold + ~ok:btype_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end + + method private get_global_variable_type + ?(size=4) + (v: variable_t) + (offset: memory_offset_t): btype_t traceresult = + let tresult = + match offset with + | ConstantOffset (num, off) -> + let gvaddr = numerical_mod_to_doubleword num in + if memmap#has_location gvaddr then + let gloc = memmap#get_location gvaddr in + if is_unknown_type gloc#btype then + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Global location at address " + ^ gvaddr#to_hex_string + ^ " does not have a type"] + else + match off with + | NoOffset -> Ok gloc#btype + | _ -> self#get_memory_offset_type gloc#btype off + else + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "No global location found at address " + ^ gvaddr#to_hex_string] + | _ -> + Error [ + (elocm __LINE__); + (p2s self#l#toPretty); + "Memory variable " ^ (p2s v#toPretty) + ^ " does not have a constant offset"] in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_global_variable_type" + __FILE__ __LINE__ + ["size: " ^ (string_of_int size); + "v: " ^ (p2s v#toPretty); + "offset: " ^ (memory_offset_to_string offset); + "tresult: " + ^ (TR.tfold + ~ok:btype_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end + + method private get_stack_variable_type + ?(size=4) + (v: variable_t) + (offset: memory_offset_t): btype_t traceresult = + let tresult = + match offset with + | ConstantOffset (num, off) -> + (match self#f#stackframe#containing_stackslot num#toInt with + | Some stackslot -> + if stackslot#is_typed then + match off with + | NoOffset -> Ok stackslot#btype + | _ -> self#get_memory_offset_type stackslot#btype off + else + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Stackslot at offset " ^ num#toString + ^ " does not have a type"] + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "No stackslot found at offset " ^ num#toString]) + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Stack memory variable " ^ (p2s v#toPretty) + ^ " does not have a constant offset"] in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_stack_variable_type" + __FILE__ __LINE__ + ["size: " ^ (string_of_int size); + "v: " ^ (p2s v#toPretty); + "offset: " ^ (memory_offset_to_string offset); + "tresult: " + ^ (TR.tfold + ~ok:btype_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end + + method private get_membasevar_type + ?(size=4) + (basevar: variable_t) + (offset: memory_offset_t): btype_t traceresult = + let basevar_type_r = self#get_variable_type basevar in + let basevar_type_r = TR.tbind resolve_type basevar_type_r in + let tresult = + TR.tbind (fun basevartype -> + match offset with + | NoOffset when is_pointer basevartype + && (not (is_struct_type (ptr_deref basevartype))) -> + Ok (ptr_deref basevartype) + | NoOffset when is_pointer basevartype -> + let symoff_r = + address_memory_offset + ~tgtsize:(Some size) (ptr_deref basevartype) zero_constant_expr in + TR.tbind (fun symoff -> + match symoff with + | FieldOffset ((fname, ckey), NoOffset) -> + let cinfo = get_compinfo_by_key ckey in + let finfo = get_compinfo_field cinfo fname in + Ok finfo.bftype + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "get_basevar_type: address_memory_offset"; + "basevar: " ^ (p2s basevar#toPretty); + "basevartype: " ^ (btype_to_string basevartype); + "symoff: " ^ (memory_offset_to_string symoff)]) + symoff_r + + | ConstantOffset (n, NoOffset) when is_pointer basevartype -> + let symoff_r = + address_memory_offset (ptr_deref basevartype) (num_constant_expr n) in + TR.tbind (fun symoff -> + match symoff with + | FieldOffset ((fname, ckey), NoOffset) -> + let cinfo = get_compinfo_by_key ckey in + let finfo = get_compinfo_field cinfo fname in + Ok finfo.bftype + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "get_basevar_type: address_memory_offset"; + "basevar: " ^ (p2s basevar#toPretty); + "offset: " ^ (memory_offset_to_string offset); + "basevartype: " ^ (btype_to_string basevartype); + "symoff: " ^ (memory_offset_to_string symoff)]) + symoff_r + + | FieldOffset ((fname, ckey), NoOffset) -> + let cinfo = get_compinfo_by_key ckey in + let finfo = get_compinfo_field cinfo fname in + Ok finfo.bftype + + | IndexOffset (v, i, memsuboff) -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "get_basevar_type: index offset: " + ^ (memory_offset_to_string offset) + ^ " with " + ^ (p2s v#toPretty) + ^ ", index: " + ^ (string_of_int i) + ^ "; and " + ^ (memory_offset_to_string memsuboff)] + + | ArrayIndexOffset (x, memsuboff) -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "get_basevar_type: array index offset: " + ^ (memory_offset_to_string offset) + ^ " with " + ^ (x2s x) + ^ "; and " + ^ (memory_offset_to_string memsuboff)] + + | BasePtrArrayIndexOffset (x, memsuboff) -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "get_basevar_type: base-ptr array index offset: " + ^ (memory_offset_to_string offset) + ^ " with " + ^ (x2s x) + ^ "; and " + ^ (memory_offset_to_string memsuboff)] + + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "memoff: " ^ (memory_offset_to_string offset) + ^ " not yet handled"]) + basevar_type_r in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_membasevar_type" + __FILE__ __LINE__ + ["basevar: " ^ (p2s basevar#toPretty); + "offset: " ^ (memory_offset_to_string offset); + "tresult: " + ^ (TR.tfold + ~ok:btype_to_string + ~error:(fun e -> "Error [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end + (* Handles the following cases: - initial_register_value: if the register is a function parameter: get parameter type @@ -1405,11 +1782,8 @@ object (self) if callsite has a typed var-intro: retrieve type of var-intro otherwise: Error (not yet handled) *) - method get_variable_type (v: variable_t): btype_t traceresult = - let is_zero (x: xpr_t) = - match x with - | XConst (IntConst n) -> n#equal numerical_zero - | _ -> false in + method get_variable_type (v: variable_t): btype_t traceresult = + let tresult = if self#f#env#is_initial_register_value v then let reg_r = self#f#env#get_initial_register_value_register v in TR.tbind @@ -1427,116 +1801,36 @@ object (self) else if self#env#is_initial_memory_value v then let memvar_r = self#env#get_init_value_variable v in TR.tbind ~msg:(eloc __LINE__) self#get_variable_type memvar_r + else if self#env#is_memory_variable v then let memref_r = self#env#get_memory_reference v in let memoff_r = self#env#get_memvar_offset v in TR.tbind ~msg:(eloc __LINE__) (fun memref -> - match memref#get_base with - | BGlobal -> - (match memoff_r with - | Ok (ConstantOffset (num, NoOffset)) -> - let gvaddr = numerical_mod_to_doubleword num in - if memmap#has_location gvaddr then - let gloc = memmap#get_location gvaddr in - Ok (gloc#btype) - else - Error [(elocm __LINE__) - ^ "no global location found for address " - ^ gvaddr#to_hex_string] - | _ -> - Error [(elocm __LINE__) ^ "not a constant offset"]) - | _ -> - let basevar_r = - match memref#get_base with - | BaseVar v -> Ok v - | b -> - Error [(elocm __LINE__) - ^ "memory-base: " ^ (p2s (memory_base_to_pretty b))] in - let basevar_type_r = - TR.tbind - ~msg:(eloc __LINE__) - self#get_variable_type - basevar_r in - TR.tbind - ~msg:(eloc __LINE__) - (fun basevartype -> - TR.tbind - (fun memoff -> - match memoff with - | NoOffset when is_pointer basevartype -> - Ok (ptr_deref basevartype) - | ConstantOffset (n, NoOffset) when is_pointer basevartype -> - let symmemoff_r = - address_memory_offset - (ptr_deref basevartype) (num_constant_expr n) in - TR.tbind - ~msg:((elocm __LINE__) - ^ "basevar type: " ^ (btype_to_string basevartype) - ^ "; offset: " ^ n#toString) - (fun off -> - match off with - | FieldOffset ((fname, ckey), NoOffset) -> - let cinfo = get_compinfo_by_key ckey in - let finfo = get_compinfo_field cinfo fname in - Ok finfo.bftype - | _ -> - Error [(elocm __LINE__) - ^ "symbolic offset: " - ^ (memory_offset_to_string off) - ^ " with basevar type: " - ^ (btype_to_string basevartype) - ^ " not yet handled"]) - symmemoff_r - | FieldOffset ((fname, ckey), NoOffset) -> - let cinfo = get_compinfo_by_key ckey in - let finfo = get_compinfo_field cinfo fname in - Ok finfo.bftype - | IndexOffset (v, i, memsuboff) -> - Error [(elocm __LINE__) - ^ "index offset: " - ^ (memory_offset_to_string memoff) - ^ " with " - ^ (p2s v#toPretty) - ^ ", index: " - ^ (string_of_int i) - ^ "; and " - ^ (memory_offset_to_string memsuboff)] - | ArrayIndexOffset (x, memsuboff) -> - Error [(elocm __LINE__) - ^ "array index offset: " - ^ (memory_offset_to_string memoff) - ^ " with " - ^ (x2s x) - ^ "; and " - ^ (memory_offset_to_string memsuboff)] - | BasePtrArrayIndexOffset (x, _) when is_zero x -> - (match basevartype with - | TPtr (t, _) -> Ok t - | _ -> - Error [(elocm __LINE__) - ^ "array index offset: " - ^ (memory_offset_to_string memoff) - ^ " with basevar type: " - ^ (btype_to_string basevartype) - ^ " not yet handled"]) - | BasePtrArrayIndexOffset (x, memsuboff) -> - Error [(elocm __LINE__) - ^ "base-ptr array index offset: " - ^ (memory_offset_to_string memoff) - ^ " with " - ^ (x2s x) - ^ "; and " - ^ (memory_offset_to_string memsuboff)] - - | _ -> - Error [(elocm __LINE__) - ^ "memoff: " ^ (memory_offset_to_string memoff) - ^ " not yet handled"]) - memoff_r) - basevar_type_r) - memref_r + if memref#is_global_reference then + TR.tbind + ~msg:(eloc __LINE__) + (self#get_global_variable_type v) + memoff_r + else if memref#is_stack_reference then + TR.tbind + ~msg:(eloc __LINE__) + (self#get_stack_variable_type v) + memoff_r + else + let basevar_r = + match memref#get_base with + | BaseVar v -> Ok v + | b -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Memory-base: " ^ (p2s (memory_base_to_pretty b))] in + TR.tbind2 + (fun basevar memoff -> self#get_membasevar_type basevar memoff) + basevar_r memoff_r) + memref_r + else if self#f#env#is_return_value v then TR.tbind ~msg:(eloc __LINE__) @@ -1546,11 +1840,17 @@ object (self) if fndata#has_regvar_type_annotation loc#i then fndata#get_regvar_type_annotation loc#i else - Error [(elocm __LINE__) - ^ "type of callsite return value " ^ (x2s (XVar v)) - ^ " at address " ^ loc#i#to_hex_string - ^ " not yet handled"]) + let ctinfo = self#f#get_call_target callsite in + let rty = ctinfo#get_returntype in + if is_unknown_type rty then + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "return type of function " ^ ctinfo#get_name + ^ " not known"] + else + Ok rty) (self#f#env#get_call_site v) + else if self#f#env#is_register_variable v then let vrdefs = self#get_variable_rdefs v in let fndata = self#f#get_function_data in @@ -1566,8 +1866,9 @@ object (self) | Some ty -> Ok ty | _ -> Error [ - (elocm __LINE__) - ^ "No reglhs type assignment found for variable " + (elocm __LINE__); + (p2s self#l#toPretty); + "No reglhs type assignment found for variable " ^ (p2s v#toPretty) ^ " at location " ^ h#getBaseName]) @@ -1575,14 +1876,28 @@ object (self) optty_r | _ -> Error [ - (elocm __LINE__) - ^ "Unable to find reachingdefs for variable " + (elocm __LINE__); + (p2s self#l#toPretty); + "Unable to find reachingdefs for variable " ^ (p2s v#toPretty)] else let ty = self#env#get_variable_type v in match ty with | None -> Error [(elocm __LINE__) ^ "variable: " ^ (x2s (XVar v))] - | Some t -> Ok t + | Some t -> Ok t in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_variable_type" + __FILE__ __LINE__ + ["v: " ^ (p2s v#toPretty); + "tresult: " + ^ (TR.tfold + ~ok:btype_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method private get_variable_rdefs (v: variable_t): symbol_t list = let symvar = self#f#env#mk_symbolic_variable v in @@ -1597,16 +1912,11 @@ object (self) ?(size=None) ?(xtype=None) (x: xpr_t): xpr_t traceresult = - let _ = - log_diagnostics_result - ~msg:(p2s self#l#toPretty) - ~tag:"xpr_to_cxpr" - __FILE__ __LINE__ - ["size: " ^ (opti2s size); - "xtype: " ^ (optty2s xtype); - "x: " ^ (x2s x)] in + let tresult = let is_pointer (y: xpr_t) = TR.tfold_default BCHBCTypeUtil.is_pointer false (self#get_xpr_type y) in + let is_integer (y: xpr_t) = + TR.tfold_default BCHBCTypeUtil.is_int false (self#get_xpr_type y) in let default () = self#convert_xpr_offsets ~xtype ~size x in match x with | XOp (XPlus, [y; XOp (XMult, [XConst (IntConst n); XVar v])]) -> @@ -1661,6 +1971,21 @@ object (self) result) (self#xpr_to_cxpr y) (BCHBCTypeUtil.size_of_btype derefty) + + | XOp (XPlus, [y; XConst (IntConst n)]) + when is_integer y && n#geq (mkNumerical 0x100000000) -> + let rresult = + simplify_xpr (XOp (XMinus, [x; int_constant_expr 0x100000000])) in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"xpr_to_cxpr:subtract 2^32" + __FILE__ __LINE__ + ["x: " ^ (x2s x); + "rresult: " ^ (x2s rresult)]; + Ok rresult + end + | _ -> match xtype with | None -> default () @@ -1669,7 +1994,22 @@ object (self) | XConst (IntConst n) when n#equal (mkNumerical 0xffffffff) && is_int t -> Ok (int_constant_expr (-1)) - | _ -> default () + | _ -> default () in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"xpr_to_cxpr" + __FILE__ __LINE__ + ["size: " ^ (opti2s size); + "xtype: " ^ (optty2s xtype); + "x: " ^ (x2s x); + "tresult: " + ^ (TR.tfold + ~ok:(fun cx -> if syntactically_equal x cx then "--" else x2s cx) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method addr_to_ctgt_xpr ?(size=None) ?(xtype=None) (a: xpr_t): xpr_t traceresult = @@ -1697,9 +2037,10 @@ object (self) | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | _ -> - Error [(elocm __LINE__) - ^ "base: " ^ (p2s base#toPretty) - ^ "; offset expr: " ^ (x2s offset)] in + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "base: " ^ (p2s base#toPretty); + "offset expr: " ^ (x2s offset)] in let var_r = TR.tmap2 ~msg1:(eloc __LINE__) @@ -1721,9 +2062,11 @@ object (self) if is_pointer t then Ok (ptr_deref t) else - Error [(elocm __LINE__) - ^ "x: " ^ (x2s a) ^ "; base: " ^ (x2s (XVar base)) - ^ "; offset: " ^ (x2s offset)]) + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "x: " ^ (x2s a); + "base: " ^ (x2s (XVar base)); + "offset: " ^ (x2s offset)]) rvartype_r in let memoff_r = TR.tbind @@ -1739,8 +2082,9 @@ object (self) memref_r memoff_r in TR.tmap (fun v -> XVar v) var_r | _ -> - Error [(elocm __LINE__) - ^ "size: " ^ (opti2s size) ^ "; " + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "size: " ^ (opti2s size) ^ "; " ^ "type: " ^ (optty2s xtype) ^ "; " ^ "addr: " ^ (x2s a) ^ ": Not yet handled"] @@ -1750,22 +2094,16 @@ object (self) match vtype with | None -> self#convert_variable_offsets ~size v | _ -> - Error [(elocm __LINE__) - ^ "size: " ^ (opti2s size) ^ "; " + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "size: " ^ (opti2s size) ^ "; " ^ "type: " ^ (optty2s vtype) ^ "; " ^ "v: " ^ (p2s v#toPretty) ^ ": Not yet implemented"] - method convert_variable_offsets + method private convert_variable_offsets ?(vtype=None) ?(size=None) (v: variable_t): variable_t traceresult = - let _ = - log_diagnostics_result - ~msg:(p2s self#l#toPretty) - ~tag:"convert-variable-offsets" - __FILE__ __LINE__ - ["vtype: " ^ (optty2s vtype); - "size: " ^ (opti2s size); - "v: " ^ (p2s v#toPretty)] in + let tresult = if self#env#is_basevar_memory_variable v then let basevar_r = self#env#get_memvar_basevar v in let offset_r = self#env#get_memvar_offset v in @@ -1787,6 +2125,16 @@ object (self) ~msg:(eloc __LINE__) (fun offset -> match offset with + | NoOffset -> + TR.tbind + ~msg:(eloc __LINE__) + (fun tgttype -> + if is_struct_type tgttype then + address_memory_offset + ~tgtbtype:optvtype ~tgtsize:size tgttype zero_constant_expr + else + Ok offset) + tgttype_r | ConstantOffset (n, NoOffset) -> TR.tbind ~msg:(eloc __LINE__) @@ -1799,7 +2147,7 @@ object (self) let _ = log_diagnostics_result ~msg:(p2s self#l#toPretty) - ~tag:"convert-variable-offsets" + ~tag:"convert_variable_offsets:basevar_memory_variable" __FILE__ __LINE__ ["tgttype: " ^ (TR.tfold_default btype_to_string "?" tgttype_r); "tgtbtype: " ^ (btype_to_string optvtype); @@ -1817,83 +2165,108 @@ object (self) let _ = log_diagnostics_result ~msg:(p2s self#l#toPretty) - ~tag:"convert-variable-offsets:default" + ~tag:"convert_variable_offsets:default" __FILE__ __LINE__ [(p2s v#toPretty)] in - Ok v - - method convert_value_offsets - ?(size=None) (v: variable_t): variable_t traceresult = - let _ = + Ok v in + begin log_diagnostics_result ~msg:(p2s self#l#toPretty) - ~tag:"convert-value-offsets" + ~tag:"convert_variable_offsets" __FILE__ __LINE__ - ["size: " ^ (opti2s size); "v: " ^ (p2s v#toPretty)] in - if self#env#is_basevar_memory_value v then - let basevar_r = self#env#get_memval_basevar v in - let offset_r = self#env#get_memval_offset v in - let cbasevar_r = - TR.tbind - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (self#convert_value_offsets ~size) - basevar_r in - let basetype_r = TR.tbind self#get_variable_type cbasevar_r in - let tgttype_r = - TR.tbind - ~msg:(eloc __LINE__) - (fun basetype -> - match basetype with - | TPtr (t, _) -> Ok t - | TComp (key, _) -> - let cinfo = get_compinfo_by_key key in - Error [(elocm __LINE__) - ^ "Target type is a struct: " ^ cinfo.bcname - ^ ". A pointer was expected"] - | t -> - Error [(elocm __LINE__) - ^ "Type " ^ (btype_to_string t) - ^ " is not a pointer"]) basetype_r in - let coffset_r = - TR.tbind - ~msg:(eloc __LINE__) - (fun offset -> - match offset with - | NoOffset -> - let _ = - log_diagnostics_result - ~msg:(p2s self#l#toPretty) - ~tag:"convert-value-offsets:NoOffset" - __FILE__ __LINE__ - ["v: " ^ (p2s v#toPretty)] in - TR.tbind - ~msg:(eloc __LINE__) - (fun tgttype -> - address_memory_offset - ~tgtsize:size tgttype (int_constant_expr 0)) tgttype_r - | ConstantOffset (n, NoOffset) -> - TR.tbind - ~msg:(eloc __LINE__) - (fun tgttype -> - address_memory_offset - ~tgtsize:size tgttype (num_constant_expr n)) tgttype_r - | _ -> - Ok offset) offset_r in - TR.tbind - ~msg:((elocm __LINE__) ^ (p2s v#toPretty)) - (fun cbasevar -> + ["vtype: " ^ (optty2s vtype); + "size: " ^ (opti2s size); + "v: " ^ (p2s v#toPretty); + "tresult: " + ^ TR.tfold + ~ok:(fun cv -> if v#equal cv then "--" else (p2s cv#toPretty)) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult]; + tresult + end + + method private convert_value_offsets + ?(size=None) (v: variable_t): variable_t traceresult = + let tresult = + if self#env#is_basevar_memory_value v then + let basevar_r = self#env#get_memval_basevar v in + let offset_r = self#env#get_memval_offset v in + let cbasevar_r = TR.tbind - ~msg:((elocm __LINE__) ^ "cbasevar: " ^ (p2s cbasevar#toPretty)) - (fun coffset -> - let memvar_r = - self#env#mk_basevar_memory_variable cbasevar coffset in + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (self#convert_value_offsets ~size) + basevar_r in + let basetype_r = TR.tbind self#get_variable_type cbasevar_r in + let basetype_r = TR.tbind resolve_type basetype_r in + let tgttype_r = + TR.tbind + ~msg:(eloc __LINE__) + (fun basetype -> + match basetype with + | TPtr (t, _) -> Ok t + | TComp (key, _) -> + let cinfo = get_compinfo_by_key key in + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Target type is a struct: " ^ cinfo.bcname + ^ ". A pointer was expected"] + | t -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Type " ^ (btype_to_string t) + ^ " is not a pointer"]) basetype_r in + let coffset_r = + TR.tbind (fun offset -> + match offset with + | NoOffset -> + TR.tbind (fun tgttype -> + if is_struct_type tgttype then + address_memory_offset + ~tgtsize:size tgttype (int_constant_expr 0) + else + Ok offset) + tgttype_r + | ConstantOffset (n, NoOffset) -> + TR.tbind + ~msg:(eloc __LINE__) + (fun tgttype -> + address_memory_offset + ~tgtsize:size tgttype (num_constant_expr n)) tgttype_r + | _ -> + Ok offset) offset_r in + let tresult = + TR.tbind + ~msg:((elocm __LINE__) ^ (p2s v#toPretty)) + (fun cbasevar -> TR.tbind - ~msg:((elocm __LINE__) - ^ "cbasevar: " ^ (p2s cbasevar#toPretty) - ^ "; coffset: " ^ (memory_offset_to_string coffset)) - self#env#mk_initial_memory_value memvar_r - ) coffset_r) - cbasevar_r + ~msg:((elocm __LINE__) ^ "cbasevar: " ^ (p2s cbasevar#toPretty)) + (fun coffset -> + let memvar_r = + self#env#mk_basevar_memory_variable cbasevar coffset in + TR.tbind + ~msg:((elocm __LINE__) + ^ (p2s self#l#toPretty) ^ ": " + ^ "cbasevar: " ^ (p2s cbasevar#toPretty) + ^ "; coffset: " ^ (memory_offset_to_string coffset)) + self#env#mk_initial_memory_value memvar_r + ) coffset_r) + cbasevar_r in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"convert_value_offsets:basevar_memory_value" + __FILE__ __LINE__ + ["size: " ^ (opti2s size); + "v: " ^ (p2s v#toPretty); + "tgttype: " ^ (TR.tfold_default btype_to_string "?" tgttype_r); + "coffset: " ^ (TR.tfold_default memory_offset_to_string "?" coffset_r); + "tresult: " + ^ (TR.tfold + ~ok:(fun cv -> if cv#equal v then "--" else (p2s cv#toPretty)) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end else let _ = log_diagnostics_result @@ -1901,16 +2274,25 @@ object (self) ~tag:"convert-value-offsets:default" __FILE__ __LINE__ ["v: " ^ (p2s v#toPretty)] in - Ok v - - method convert_xpr_offsets - ?(xtype=None) ?(size=None) (x: xpr_t): xpr_t traceresult = - let _ = + Ok v in + begin log_diagnostics_result ~msg:(p2s self#l#toPretty) - ~tag:"convert-xpr-offsets" + ~tag:"convert_value_offsets" __FILE__ __LINE__ - ["xtype: " ^ (optty2s xtype); "size: " ^ (opti2s size); "x: " ^ (x2s x)] in + ["size: " ^ (opti2s size); + "v: " ^ (p2s v#toPretty); + "tresult: " + ^ (TR.tfold + ~ok:(fun cv -> if cv#equal v then "--" else (p2s cv#toPretty)) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end + + method private convert_xpr_offsets + ?(xtype=None) ?(size=None) (x: xpr_t): xpr_t traceresult = + let tresult = let rec aux exp = match exp with | XVar v when self#env#is_basevar_memory_value v -> @@ -1966,13 +2348,81 @@ object (self) ~tag:"convert-xpr-offsets:failure" __FILE__ __LINE__ ["x: " ^ (x2s x) ^ "; " ^ (String.concat "; " e)] in - result + result in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"convert_xpr_offsets" + __FILE__ __LINE__ + ["xtype: " ^ (optty2s xtype); + "size: " ^ (opti2s size); + "x: " ^ (x2s x); + "tresult: " ^ + TR.tfold + ~ok:(fun cx -> if syntactically_equal x cx then "--" else x2s cx) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult]; + tresult + end method get_xpr_type (x: xpr_t): btype_t traceresult = - match x with - | XVar v -> self#get_variable_type v - | XOp (XPlus, [XVar v; XConst (IntConst _)]) -> self#get_variable_type v - | _ -> Error [(elocm __LINE__) ^ "xpr: " ^ (x2s x)] + let tresult = + match x with + | XVar v -> self#get_variable_type v + | XOp (XPlus, [XVar v; XConst (IntConst _)]) -> self#get_variable_type v + | XOp (XPlus, [x1; x2]) -> + TR.tbind2 + ~msg1:((elocm __LINE__) ^ "x1: " ^ (x2s x1)) + ~msg2:((elocm __LINE__) ^ "x2: " ^ (x2s x2)) + (fun t1 t2 -> + if is_pointer t1 && is_int t2 then + Ok t1 + else if is_pointer t2 && is_int t1 then + Ok t2 + else if is_int t1 && is_int t2 then + Ok t1 + else + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Unable to combine types " + ^ (ty2s t1) ^ " and " ^ (ty2s t2)]) + (self#get_xpr_type x1) + (self#get_xpr_type x2) + | XOp (XMinus, [x1; x2]) -> + TR.tbind2 + ~msg1:((elocm __LINE__) ^ "x1: " ^ (x2s x1)) + ~msg2:((elocm __LINE__) ^ "x2: " ^ (x2s x2)) + (fun t1 t2 -> + if is_pointer t1 && is_pointer t2 then + Ok t_int + else if is_pointer t1 && is_int t2 then + Ok t1 + else if is_int t1 && is_int t2 then + Ok t1 + else + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "Untable to combine types " + ^ (ty2s t1) ^ " and " ^ (ty2s t2)]) + (self#get_xpr_type x1) + (self#get_xpr_type x2) + | _ -> + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "xpr: " ^ (x2s x)] in + begin + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_xpr_type" + __FILE__ __LINE__ + ["x: " ^ (x2s x); + "tresult: " + ^ TR.tfold + ~ok:btype_to_string + ~error:(fun e -> "Error:[" ^ (String.concat "; " e) ^ "]") + tresult]; + tresult + end method decompose_memaddr (x: xpr_t): (memory_reference_int traceresult * memory_offset_t traceresult) = @@ -1986,6 +2436,7 @@ object (self) let vars = vars_as_positive_terms x in let knownpointers = List.filter self#f#is_base_pointer vars in match knownpointers with + (* one known pointer, must be the base *) | [base] (* when self#f#env#is_initial_stackpointer_value base *) -> let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in @@ -1996,9 +2447,10 @@ object (self) | XConst (IntConst n) when n#equal numerical_zero -> Ok NoOffset | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset)) | _ -> - Error [(elocm __LINE__) - ^ "base: " ^ (p2s base#toPretty) - ^ "; offset expr: " ^ (x2s offset)] in + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "base: " ^ (p2s base#toPretty); + "offset expr: " ^ (x2s offset)] in (memref_r, memoff_r) (* no known pointers, have to find a base *) @@ -2022,9 +2474,9 @@ object (self) let v = self#env#mk_symbolic_value x in Ok (IndexOffset (v, n#toInt, NoOffset)) | _ -> - Error [(elocm __LINE__) - ^ (p2s self#l#toPretty) ^ ": " - ^ "decompose_memaddr: " ^ (x2s x) ^ ": " + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "Offset from global base " ^ maxC#toString ^ " not recognized: " ^ (x2s offset)] in @@ -2049,9 +2501,9 @@ object (self) | XOp (XMult, [XConst (IntConst n); XVar v]) -> Ok (IndexOffset (v, n#toInt, NoOffset)) | _ -> - Error [(elocm __LINE__) - ^ (p2s self#l#toPretty) ^ ": " - ^ "decompose_memaddr: " ^ (x2s x) ^ ": " + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "Offset from base " ^ (x2s (XVar base)) ^ " not recognized: " ^ (x2s offset)] in @@ -2080,9 +2532,9 @@ object (self) | XOp (XMult, [XConst (IntConst n); XVar v]) -> Ok (IndexOffset (v, n#toInt, NoOffset)) | _ -> - Error [(elocm __LINE__) - ^ (p2s self#l#toPretty) ^ ": " - ^ "decompose_memaddr: " ^ (x2s x) ^ ": " + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "decompose_memaddr: " ^ (x2s x) ^ ": " ^ "Offset from base " ^ (x2s (XVar base)) ^ " not recognized: " ^ (x2s offset)]) @@ -2091,9 +2543,9 @@ object (self) | [v] -> let memref_r = - Error [(elocm __LINE__) - ^ (p2s self#l#toPretty) ^ ": " - ^ "No candidate base pointers. Only variable found: " + Error [(elocm __LINE__); + (p2s self#l#toPretty); + "No candidate base pointers. Only variable found: " ^ (p2s v#toPretty)] in let memoff_r = Error [eloc __LINE__] in (memref_r, memoff_r) @@ -2296,7 +2748,7 @@ object (self) begin try begin - match self#get_esp_offset with + match self#get_x86_esp_offset with | (0,range) -> begin match range#singleton with @@ -2408,11 +2860,11 @@ object (self) let newrhs = TR.tvalue (self#f#env#mk_global_variable_address dw) ~default:rhs in let _ = - ch_diagnostics_log#add - "rewrite constant to global address" - (LBLOCK [ - self#l#toPretty; STR ": "; - dw#toPretty; STR " ==> "; (x2p newrhs)]) in + log_diagnostics_result + ~msg:(p2s self#l#toPretty) + ~tag:"get_assign_commands_r: global address" + __FILE__ __LINE__ + [dw#to_hex_string ^ " ==> " ^ (x2s newrhs)] in newrhs else rhs @@ -2672,37 +3124,39 @@ object (self) (match xpr with | XOp (XMinus, [XVar _v; XConst (IntConst n)]) when n#geq numerical_zero -> let spoffset = n#neg in - if Option.is_some - (self#f#stackframe#containing_stackslot spoffset#toInt) then - TR.tfold_default - (fun s -> Some s) - None - (self#env#mk_stack_variable finfo#stackframe spoffset) - else - let _ = - ch_diagnostics_log#add "evaluate-fts-address-argument:reg" - (LBLOCK [self#l#toPretty; STR ": "; - STR (fts_parameter_to_string p); STR ": "; - (x2p xpr); STR ": "; - INT spoffset#toInt]) in - None - + (match self#f#stackframe#containing_stackslot spoffset#toInt with + | Some stackslot -> + Some (self#f#env#mk_stackslot_variable stackslot NoOffset) + | _ -> + begin + log_diagnostics_result + ~tag:"evaluate_fts_address_argument" + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["parameter: " ^ (fts_parameter_to_string p); + "external argvar: " ^ (x2s xpr); + "offset: " ^ (spoffset#toString)]; + None + end) | _ -> - let _ = - ch_diagnostics_log#add "evaluate-fts-address-argument: reg" - (LBLOCK [self#l#toPretty; STR ": "; - STR (fts_parameter_to_string p); STR ": "; - (x2p xpr)]) in - None) + begin + log_diagnostics_result + ~tag:"evaluate_fts_address_argument" + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["parameter: " ^ (fts_parameter_to_string p); + "external argvar: " ^ (x2s xpr)]; + None + end) | _ -> - let _ = - chlog#add - "evaluate-fts-address-argument: failure" - (LBLOCK [ - STR self#cia; - STR ": "; - fts_parameter_to_pretty p]) in - None + begin + log_diagnostics_result + ~tag:"evaluate_fts_address_argument" + ~msg:(p2s self#l#toPretty) + __FILE__ __LINE__ + ["Unable to evaluate fts parameter " ^ (fts_parameter_to_string p)]; + None + end method evaluate_summary_address_term (t:bterm_t) = match t with diff --git a/CodeHawk/CHB/bchlib/bCHFunctionData.ml b/CodeHawk/CHB/bchlib/bCHFunctionData.ml index d77d1ecd..dbd4f81e 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionData.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionData.ml @@ -236,6 +236,13 @@ object (self) None a.regvarintros | _ -> None + method has_stackvar_intro (offset: int): bool = + match self#get_function_annotation with + | Some a -> + List.fold_left (fun acc svi -> + acc || svi.svi_offset = offset) false a.stackvarintros + | _ -> false + method get_stackvar_intro (offset: int): stackvar_intro_t option = match self#get_function_annotation with | Some a -> @@ -693,7 +700,7 @@ let read_xml_stackvar_intro (node: xml_element_int): stackvar_intro_t traceresul else if not (has "name") then Error ["stackvar intro without name"] else - let svi_offset = (-(geti "offset")) in + let svi_offset = (geti "offset") in let svi_name = get "name" in let svi_loopcounter = has "loopcounter" && (get "loopcounter") = "yes" in let (svi_vartype, svi_cast) = diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index b52a1fc2..da68704b 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -84,6 +84,8 @@ let x2p = xpr_formatter#pr_expr let p2s = CHPrettyUtil.pretty_to_string let x2s x = p2s (x2p x) +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " let log_error (tag: string) (msg: string): tracelogspec_t = mk_tracelog_spec ~tag:("finfo:" ^ tag) msg @@ -874,7 +876,7 @@ object (self) match memmap#containing_location dw with | Some gloc -> tmap - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:global") + ~msg:((elocm __LINE__) ^ "mk_global_variable") (fun offset -> let gvar = self#mk_variable @@ -893,40 +895,33 @@ object (self) let _ = memmap#add_location ~size:(Some size) ~btype dw in Ok (self#mk_variable (self#varmgr#make_global_variable dw#to_numerical)) - method mk_stack_variable - ?(size=4) - (stackframe: stackframe_int) - (offset: numerical_t): variable_t traceresult = - match stackframe#containing_stackslot offset#toInt with - | Some stackslot -> - tmap - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:stack") - (fun memoffset -> - let atts: string list = if stackslot#is_loopcounter then ["lc"] else [] in - let svar = - self#mk_variable - ~atts - (self#varmgr#make_local_stack_variable - ~offset:memoffset (mkNumerical stackslot#offset)) in - let name = stackslot#name ^ (memory_offset_to_string memoffset) in - let _ = - match atts with - | [] -> () - | _ -> - ch_diagnostics_log#add - "loopcounter variable on the stack" - (LBLOCK [STR "Offset: "; offset#toPretty; STR ": "; STR name; - STR "; "; svar#toPretty]) in - begin - self#set_variable_name svar name; - svar - end) - (stackslot#frame_offset_memory_offset - ~tgtsize:(Some size) (num_constant_expr offset)) - | _ -> - Error [ - __FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "No stack slot found at offset " ^ offset#toString] + method mk_stackslot_variable + (stackslot: stackslot_int) (offset: memory_offset_t): variable_t = + let atts: string list = if stackslot#is_loopcounter then ["lc"] else [] in + let svar = + self#mk_variable + ~atts + (self#varmgr#make_local_stack_variable + ~offset (mkNumerical stackslot#offset)) in + let name = stackslot#name ^ (memory_offset_to_string offset) in + let _ = + match atts with + | [] -> () + | _ -> + log_diagnostics_result + ~msg:name + ~tag:"mk_stackslot_variable:loop-counter variable" + __FILE__ __LINE__ + ["offset: " ^ (memory_offset_to_string offset); p2s svar#toPretty] in + begin + self#set_variable_name svar name; + log_diagnostics_result + ~msg:name + ~tag:"mk_stackslot_variable" + __FILE__ __LINE__ + ["offset: " ^ (memory_offset_to_string offset); p2s svar#toPretty]; + svar + end method mk_register_variable (register:register_t) = self#mk_variable (varmgr#make_register_variable register) @@ -1454,6 +1449,8 @@ object (self) method is_stack_parameter_variable (v:variable_t) = (varmgr#is_stack_parameter_variable v) + method is_local_stack_variable = varmgr#is_local_stack_variable + method is_stack_parameter_value (v:variable_t) = (self#is_initial_memory_value v) && (tfold_default diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml index 7c0996bd..c58de637 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml @@ -39,6 +39,7 @@ open CHXmlDocument (* xprlib *) open Xprt open XprTypes +open Xsimplify (* bchlib *) open BCHBasicTypes @@ -47,6 +48,7 @@ open BCHBCTypes open BCHBCTypeUtil open BCHCPURegisters open BCHLibTypes +open BCHMemoryReference module H = Hashtbl module TR = CHTraceResult @@ -55,6 +57,19 @@ module TR = CHTraceResult let x2p = XprToPretty.xpr_formatter#pr_expr let p2s = CHPrettyUtil.pretty_to_string let x2s x = p2s (x2p x) +let s2i = string_of_int + +let opti2s (i: int option) = + if Option.is_some i then string_of_int (Option.get i) else "?" + +let ty2s (ty: btype_t) = + if is_unknown_type ty then "?" else btype_to_string ty + +let optty2s (ty: btype_t option) = + if Option.is_some ty then btype_to_string (Option.get ty) else "?" + +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " let bcd = BCHBCDictionary.bcdictionary @@ -88,8 +103,26 @@ object (self) method is_typed: bool = not (btype_equal self#btype t_unknown) + method offset_type (offset: memory_offset_t) = + if self#is_typed then + match offset with + | NoOffset -> Ok self#btype + | _ -> + Error [(elocm __LINE__); + "offset_type not yet implemented for offset " + ^ (memory_offset_to_string offset) + ^ " and type " ^ (ty2s self#btype)] + else + Error [(elocm __LINE__); + "Stackslot at offset " ^ (s2i self#offset) ^ " does not have a type"] + method spill: register_t option = sslot.sslot_spill + method is_compatible_with_spill: bool = + self#is_spill + || ((match self#size with | Some 4 | None -> true | _ -> false) + && (String.sub self#name 0 4) = "var_") + method is_spill: bool = Option.is_some self#spill method is_struct: bool = @@ -119,50 +152,89 @@ object (self) | _ -> 4 in offset >= self#offset && offset < self#offset + size - method frame2object_offset_value (xpr: xpr_t) = - match xpr with - | XConst (IntConst n) -> - let numoffset = mkNumerical self#offset in - Ok (num_constant_expr (n#sub numoffset)) - | _ -> - Error [ - __FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Offset expression " - ^ (x2s xpr) - ^ " not yet handled"] + method frame2object_offset_value (xpr: xpr_t): xpr_t traceresult = + let xoff = + simplify_xpr (XOp (XMinus, [xpr; int_constant_expr self#offset])) in + let xoff = + match xoff with + | XOp (XPlus, [_; XConst (IntConst n)]) when n#geq (mkNumerical 0x100000000) -> + let rresult = + simplify_xpr (XOp (XMinus, [xoff; int_constant_expr 0x100000000])) in + begin + log_diagnostics_result + ~tag:"frame2object_offset_value:correct for stackpointer wraparound" + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); "rresult: " ^ (x2s rresult)]; + rresult + end + | _ -> xoff in + Ok xoff method frame_offset_memory_offset ?(tgtsize=None) ?(tgtbtype=t_unknown) + (loc: location_int) (xpr: xpr_t): memory_offset_t traceresult = - TR.tbind - (self#object_offset_memory_offset ~tgtsize ~tgtbtype) - (self#frame2object_offset_value xpr) + let tresult = + TR.tbind + (self#object_offset_memory_offset ~tgtsize ~tgtbtype loc) + (self#frame2object_offset_value xpr) in + begin + log_diagnostics_result + ~msg:(p2s loc#toPretty) + ~tag:"frame_offset_memory_offset" + __FILE__ __LINE__ + ["xpr: " ^ (x2s xpr); + "tresult: " + ^ (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method object_offset_memory_offset ?(tgtsize=None) ?(tgtbtype=t_unknown) + (loc: location_int) (xoffset: xpr_t): memory_offset_t traceresult = - match xoffset with - | XConst (IntConst n) - when n#equal CHNumerical.numerical_zero - && (not self#is_typed || self#is_scalar) -> - Ok NoOffset - | XConst (IntConst n) when not self#is_typed -> - Ok (ConstantOffset (n, NoOffset)) - | _ -> - let tgtbtype = - if is_unknown_type tgtbtype then None else Some tgtbtype in - if self#is_array then - let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in - self#arrayvar_memory_offset ~tgtsize ~tgtbtype btype xoffset - else if self#is_struct then - let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in - self#structvar_memory_offset ~tgtsize ~tgtbtype btype xoffset - else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ (btype_to_string self#btype) - ^ " not yet handled"] + let tresult = + match xoffset with + | XConst (IntConst n) + when n#equal CHNumerical.numerical_zero + && (not self#is_typed || self#is_scalar) -> + Ok NoOffset + | XConst (IntConst n) when not self#is_typed -> + Ok (ConstantOffset (n, NoOffset)) + | _ -> + let tgtbtype = + if is_unknown_type tgtbtype then None else Some tgtbtype in + if self#is_array then + let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in + self#arrayvar_memory_offset ~tgtsize ~tgtbtype btype xoffset + else if self#is_struct then + let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in + self#structvar_memory_offset ~tgtsize ~tgtbtype btype xoffset + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ (btype_to_string self#btype) + ^ " not yet handled"] in + begin + log_diagnostics_result + ~msg:(p2s loc#toPretty) + ~tag:"object_offset_memory_offset" + __FILE__ __LINE__ + ["stackslot: " ^ (string_of_int self#offset); + "xoffset: " ^ (x2s xoffset); + "tgtsize: " ^ (opti2s tgtsize); + "tgtbtype: " ^ (ty2s tgtbtype); + "tresult: " + ^ (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method private arrayvar_memory_offset ~(tgtsize: int option) @@ -173,62 +245,96 @@ object (self) match x with | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero | _ -> false in - match xoffset with - | XConst (IntConst n) when - n#equal CHNumerical.numerical_zero - && Option.is_none tgtsize - && Option.is_none tgtbtype -> - Ok NoOffset - | _ -> - if is_array_type btype then - let eltty = get_element_type btype in - tbind - (fun elsize -> - let optindex = BCHXprUtil.get_array_index_offset xoffset elsize in - match optindex with - | None -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Unable to extract index from " ^ (x2s xoffset)] - | Some (indexxpr, xrem) when - iszero xrem - && Option.is_none tgtsize - && Option.is_none tgtbtype -> - Ok (ArrayIndexOffset (indexxpr, NoOffset)) - | Some (indexxpr, xrem) -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Unable to handle remainder " - ^ (x2s xrem) - ^ " with index expression " - ^ (x2s indexxpr)]) - (size_of_btype eltty) - else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "xoffset: " ^ (x2s xoffset) - ^ "; btype: " ^ (btype_to_string btype)] + let tresult = + match xoffset with + | XConst (IntConst n) when + n#equal CHNumerical.numerical_zero + && Option.is_none tgtsize + && Option.is_none tgtbtype -> + Ok NoOffset + | _ -> + if is_array_type btype then + let eltty = get_element_type btype in + tbind + (fun elsize -> + let optindex = BCHXprUtil.get_array_index_offset xoffset elsize in + match optindex with + | None -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Unable to extract index from " ^ (x2s xoffset)] + + (* No check is performed on tgtsize, to allow for memory accesses + whose size does not align with the size of individual + elements of an array or struct. An example of this situation + is a char array used as a destination of an STM instruction *) + | Some (indexxpr, xrem) when iszero xrem -> + Ok (ArrayIndexOffset (indexxpr, NoOffset)) + | Some (indexxpr, xrem) -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Unable to handle remainder " + ^ (x2s xrem) + ^ " with index expression " + ^ (x2s indexxpr)]) + (size_of_btype eltty) + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "xoffset: " ^ (x2s xoffset) + ^ "; btype: " ^ (btype_to_string btype)] in + begin + log_diagnostics_result + ~tag:"stackframe:arrayvar_memory_offset" + ~msg:self#name + __FILE__ __LINE__ + ["tgtsize: " ^ (opti2s tgtsize); + "type: " ^ (ty2s btype); + "offset: " ^ (x2s xoffset); + "tresult: " + ^ (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method private structvar_memory_offset ~(tgtsize: int option) ~(tgtbtype: btype_t option) (btype: btype_t) (xoffset: xpr_t): memory_offset_t traceresult = - match xoffset with - | XConst (IntConst n) when - n#equal CHNumerical.numerical_zero - && Option.is_none tgtsize - && Option.is_none tgtbtype -> - Ok NoOffset - | XConst (IntConst _) -> - if is_struct_type btype then - let compinfo = get_struct_type_compinfo btype in - (self#get_field_memory_offset_at ~tgtsize ~tgtbtype compinfo xoffset) - else + let tresult = + match xoffset with + | XConst (IntConst n) when + n#equal CHNumerical.numerical_zero + && Option.is_none tgtsize + && Option.is_none tgtbtype -> + Ok NoOffset + | XConst (IntConst _) -> + if is_struct_type btype then + let compinfo = get_struct_type_compinfo btype in + (self#get_field_memory_offset_at ~tgtsize ~tgtbtype compinfo xoffset) + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "xoffset: " ^ (x2s xoffset) + ^ "; btype: " ^ (btype_to_string btype)] + | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "xoffset: " ^ (x2s xoffset) - ^ "; btype: " ^ (btype_to_string btype)] - | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "xoffset: " ^ (x2s xoffset) - ^ "; btype: " ^ (btype_to_string btype)] + ^ "; btype: " ^ (btype_to_string btype)] in + begin + log_diagnostics_result + ~tag:"stackframe:structvar_memory_offset" + ~msg:self#name + __FILE__ __LINE__ + ["tgtsize: " ^ (opti2s tgtsize); + "type: " ^ (ty2s btype); + "offset: " ^ (x2s xoffset); + "tresult: " + ^ (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method private get_field_memory_offset_at ~(tgtsize: int option) @@ -268,62 +374,78 @@ object (self) | Some size, _ when size != s -> size_discrepancy size s | _, Some ty when not (btype_equal ty t) -> type_discrepancy ty t | _ -> "" in - match xoffset with - | XConst (IntConst n) -> - let offset = n#toInt in - let finfos = c.bcfields in - let optfield_r = - List.fold_left (fun acc_r finfo -> - match acc_r with - (* Error has been detected earlier *) - | Error e -> Error e - (* Result has already been determined *) - | Ok (Some _) -> acc_r - (* Still looking for a result *) - | Ok _ -> - match finfo.bfieldlayout with - | None -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "No field layout for field " ^ finfo.bfname] - | Some (foff, sz) -> - if offset < foff then + let tresult = + match xoffset with + | XConst (IntConst n) -> + let offset = n#toInt in + let finfos = c.bcfields in + let optfield_r = + List.fold_left (fun acc_r finfo -> + match acc_r with + (* Error has been detected earlier *) + | Error e -> Error e + (* Result has already been determined *) + | Ok (Some _) -> acc_r + (* Still looking for a result *) + | Ok _ -> + match finfo.bfieldlayout with + | None -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Skipped over field: " - ^ (string_of_int offset)] - else if offset >= (foff + sz) then - Ok None - else - let offset = offset - foff in - tbind - (fun fldtype -> - 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 - ((finfo.bfname, finfo.bfckey), NoOffset))) - else if offset = 0 && is_scalar fldtype then - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Scalar type or size is not consistent: " - ^ (compliance_failure fldtype sz)] - else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Field offset " - ^ (x2s xoffset) - ^ " not yet handled"]) - (resolve_type finfo.bftype)) (Ok None) finfos in - (match optfield_r with - | Error e -> Error e - | Ok (Some offset) -> Ok offset - | Ok None -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Unable to find field at offset " ^ (string_of_int offset)]) - | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Unable to determine field for xoffset: " ^ (x2s xoffset) - ^ " and tgtsize: " ^ pr_tgtsize ] + ^ "No field layout for field " ^ finfo.bfname] + | Some (foff, sz) -> + if offset < foff then + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Skipped over field: " + ^ (string_of_int offset)] + else if offset >= (foff + sz) then + Ok None + else + let offset = offset - foff in + tbind + (fun fldtype -> + 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 + ((finfo.bfname, finfo.bfckey), NoOffset))) + else if offset = 0 && is_scalar fldtype then + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Scalar type or size is not consistent: " + ^ (compliance_failure fldtype sz)] + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Field offset " + ^ (x2s xoffset) + ^ " not yet handled"]) + (resolve_type finfo.bftype)) (Ok None) finfos in + (match optfield_r with + | Error e -> Error e + | Ok (Some offset) -> Ok offset + | Ok None -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Unable to find field at offset " ^ (string_of_int offset)]) + | _ -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Unable to determine field for xoffset: " ^ (x2s xoffset) + ^ " and tgtsize: " ^ pr_tgtsize] in + begin + log_diagnostics_result + ~tag:"stackframe:get_field_memory_offset_at" + __FILE__ __LINE__ + ["tgtsize: " ^ (opti2s tgtsize); + "tgttype: " ^ (optty2s tgtbtype); + "compinfo: " ^ c.bcname; + "xoffset: " ^ (x2s xoffset); + "tresult: " ^ + (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method write_xml(node: xml_element_int) = begin @@ -351,19 +473,21 @@ object (self) (* val saved_registers = H.create 3 (* reg -> saved_register_t *) *) val accesses = H.create 3 (* offset -> (iaddr, stack_access_t) list *) + + (* Initialized with the stack-variable introductions from userdata.*) val stackslots = let slots = H.create 3 in (* offset -> stackslot *) begin (match fndata#get_function_annotation with | Some fnannot -> List.iter (fun svintro -> - let negoffset = -svintro.svi_offset in + let offset = svintro.svi_offset in let ty = match svintro.svi_vartype with | Some ty -> ty | _ -> t_unknown in let size = TR.to_option (size_of_btype ty) in let sslot = { - sslot_offset = negoffset; + sslot_offset = offset; sslot_name = svintro.svi_name; sslot_btype = ty; sslot_spill = None; @@ -373,7 +497,7 @@ object (self) let stackslot = new stackslot_t sslot in let _ = chlog#add "stack slot added" (stackslot_rec_to_pretty sslot) in - H.add slots negoffset stackslot) fnannot.stackvarintros + H.add slots offset stackslot) fnannot.stackvarintros | _ -> ()); slots end @@ -391,6 +515,9 @@ object (self) [] in H.replace accesses offset ((iaddr, acc) :: entry) + method has_stackslot (offset: int): bool = + H.mem stackslots offset + method containing_stackslot (offset: int): stackslot_int option = H.fold (fun _ sslot acc -> match acc with @@ -398,6 +525,17 @@ object (self) | _ -> if sslot#contains_offset offset then Some sslot else None) stackslots None + method xpr_containing_stackslot (xpr: xpr_t): stackslot_int option = + let is_stack = + List.fold_left + (fun acc v -> acc || varmgr#is_initial_stackpointer_value v) + false (BCHXprUtil.vars_as_positive_terms xpr) in + if is_stack then + let (_, coffset) = BCHXprUtil.smallest_wrapped_constant_term xpr in + self#containing_stackslot coffset#toInt + else + None + method add_stackslot ?(name = None) ?(btype = t_unknown) @@ -405,12 +543,7 @@ object (self) ?(size = None) ?(desc = None) (offset: int): stackslot_int traceresult = - if offset >= 0 then - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Illegal offset for stack slot: " - ^ (string_of_int offset) - ^ ". Offset should be less than zero."] - else if H.mem stackslots offset then + if H.mem stackslots offset then begin log_error_result ~tag:"duplicate stack slot" @@ -445,7 +578,10 @@ object (self) let sname = match name with | Some name -> name - | _ -> "var_" ^ (string_of_int offset) in + | _ -> + let numoff = CHNumerical.mkNumerical offset in + let memoff = ConstantOffset(numoff, NoOffset) in + BCHMemoryReference.stack_offset_to_name memoff in let ssrec = { sslot_name = sname; sslot_offset = offset; @@ -473,36 +609,42 @@ object (self) () else let spill = RegisterSpill (offset, reg) in + let mk_stackslot () = + let ssrec = { + sslot_name = (register_to_string reg) ^ "_spill"; + sslot_offset = offset; + sslot_btype = t_unknown; + sslot_spill = Some reg; + sslot_size = Some 4; + sslot_loopcounter = false; + sslot_desc = Some "register spill" + } in + new stackslot_t ssrec in begin (if H.mem stackslots offset then if (H.find stackslots offset)#is_spill then () else let sslot = H.find stackslots offset in - raise - (BCH_failure - (LBLOCK [ - STR "Add register spill at address "; - STR iaddr; - STR " for register "; - STR (register_to_string reg); - STR " at offset "; - INT offset; - STR " cannot be completed, because another stackslot "; - STR "at this offset, with name: "; - STR sslot#name; - STR " already exists"])) + if sslot#is_compatible_with_spill then + let sslot = mk_stackslot () in + H.replace stackslots offset sslot + else + raise + (BCH_failure + (LBLOCK [ + STR "Add register spill at address "; + STR iaddr; + STR " for register "; + STR (register_to_string reg); + STR " at offset "; + INT offset; + STR " cannot be completed, because another stackslot "; + STR "at this offset, with name: "; + STR sslot#name; + STR " already exists"])) else - let ssrec = { - sslot_name = (register_to_string reg) ^ "_spill"; - sslot_offset = offset; - sslot_btype = t_unknown; - sslot_spill = Some reg; - sslot_size = Some 4; - sslot_loopcounter = false; - sslot_desc = Some "register spill" - } in - let sslot = new stackslot_t ssrec in + let sslot = mk_stackslot () in H.add stackslots offset sslot); self#add_access offset iaddr spill end @@ -513,10 +655,26 @@ object (self) () else let restore = RegisterRestore (offset, reg) in + let mk_stackslot () = + let ssrec = { + sslot_name = (register_to_string reg) ^ "_spill"; + sslot_offset = offset; + sslot_btype = t_unknown; + sslot_spill = Some reg; + sslot_size = Some 4; + sslot_loopcounter = false; + sslot_desc = Some "register restore" + } in + new stackslot_t ssrec in begin (if H.mem stackslots offset then if (H.find stackslots offset)#is_spill then () + else + let sslot = H.find stackslots offset in + if sslot#is_compatible_with_spill then + let sslot = mk_stackslot () in + H.replace stackslots offset sslot else let sslot = H.find stackslots offset in raise @@ -577,6 +735,7 @@ object (self) (iaddr:ctxt_iaddress_t) = let ty = match typ with Some t -> t | _ -> t_unknown in let blread = StackBlockRead (offset, size, ty) in + (* let ssrec = { sslot_name = "localvar_" ^ (string_of_int (-offset)); sslot_offset = offset; @@ -585,11 +744,11 @@ object (self) sslot_spill = None; sslot_loopcounter = false; sslot_desc = None - } in - let sslot = new stackslot_t ssrec in + } in *) + (* let sslot = new stackslot_t ssrec in *) begin self#add_access offset iaddr blread; - H.add stackslots offset sslot + (* H.add stackslots offset sslot *) end method add_block_write diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml b/CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml index eb23d99e..6374ce73 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml @@ -265,8 +265,13 @@ object (self) let varinfo = bcfiles#get_varinfo fname in let fsum = function_summary_of_bvarinfo varinfo in let _ = - ch_diagnostics_log#add "load-so-function" - (LBLOCK [STR fname; STR ": "; fsum#toPretty]) in + log_diagnostics_result + ~msg:fname + ~tag:"load_so_function" + __FILE__ __LINE__ + ["signature: " + ^ (BCHFunctionInterface.function_interface_to_prototype_string + fsum#get_function_interface)] in begin chlog#add "summary from function prototype" (STR fname); bc_so_summaries#add fname; diff --git a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml index 3381fbf2..76ffcf51 100644 --- a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml +++ b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml @@ -44,6 +44,7 @@ open BCHBCTypes open BCHBCTypeUtil open BCHDoubleword open BCHLibTypes +open BCHMemoryReference module H = Hashtbl module TR = CHTraceResult @@ -62,6 +63,8 @@ let optty2s (ty: btype_t option) = let bcd = BCHBCDictionary.bcdictionary +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " let globalvalue_to_pretty (gv: globalvalue_t): pretty_t = match gv with @@ -71,13 +74,12 @@ let globalvalue_to_pretty (gv: globalvalue_t): pretty_t = let _global_location_ref_to_pretty (gref: global_location_ref_t): pretty_t = match gref with - | GLoad (gaddr, iaddr, gxpr, size, signed) -> + | GLoad (gaddr, iaddr, offset, size, signed, _vtype) -> LBLOCK [ STR "load: "; gaddr#toPretty; STR ", "; STR iaddr; STR " "; - x2p gxpr; - STR " "; + STR (memory_offset_to_string offset); STR " "; INT size; (if signed then STR " (signed)" else STR "") ] @@ -87,7 +89,7 @@ let _global_location_ref_to_pretty (gref: global_location_ref_t): pretty_t = gaddr#toPretty; STR ", "; STR iaddr; STR " "; - x2p gxpr; + STR (x2s gxpr); STR " "; INT size] | GAddressArgument (gaddr, iaddr, argindex, gxpr, btype, memoff) -> @@ -482,48 +484,56 @@ object (self) ?(tgtbtype=t_unknown) (loc: location_int) (xoffset: xpr_t): memory_offset_t traceresult = - let _ = + let tresult = + match xoffset with + | XConst (IntConst n) + when n#equal CHNumerical.numerical_zero + && Option.is_none tgtsize + && ((is_unknown_type tgtbtype) || (is_void tgtbtype)) -> + Ok NoOffset + | XConst (IntConst n) + when n#equal CHNumerical.numerical_zero && (not self#is_typed) -> + Ok NoOffset + | XConst (IntConst n) + when n#equal CHNumerical.numerical_zero + && self#is_scalar + && Option.is_some tgtsize + && Option.is_some self#size + && (Option.get tgtsize) = (Option.get self#size) -> + Ok NoOffset + | XConst (IntConst n) when not self#is_typed -> + Ok (ConstantOffset (n, NoOffset)) + | _ -> + let tgtbtype = + if is_unknown_type tgtbtype then None else Some tgtbtype in + if self#is_struct then + let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in + self#structvar_memory_offset ~tgtsize ~tgtbtype loc btype xoffset + else if self#is_array then + let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in + self#arrayvar_memory_offset ~tgtsize ~tgtbtype loc btype xoffset + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" + ^ (btype_to_string self#btype) + ^ " is not known to be a struct or array"; + "gloc_address: " ^ self#address#to_hex_string; + "xoffset: " ^ (x2s xoffset)] in + begin log_diagnostics_result ~msg:(p2s loc#toPretty) - ~tag:"mmap:address-offset-memory-offset" + ~tag:"mmap:address_offset_memory_offset" __FILE__ __LINE__ ["gloc: " ^ self#address#to_hex_string ^ "; xoffset: " ^ (x2s xoffset) ^ "; tgtsize: " ^ (opti2s tgtsize) - ^ "; tgtbtype: " ^ (ty2s tgtbtype)] in - match xoffset with - | XConst (IntConst n) - when n#equal CHNumerical.numerical_zero - && Option.is_none tgtsize - && ((is_unknown_type tgtbtype) || (is_void tgtbtype)) -> - Ok NoOffset - | XConst (IntConst n) - when n#equal CHNumerical.numerical_zero && (not self#is_typed) -> - Ok NoOffset - | XConst (IntConst n) - when n#equal CHNumerical.numerical_zero - && self#is_scalar - && Option.is_some tgtsize - && Option.is_some self#size - && (Option.get tgtsize) = (Option.get self#size) -> - Ok NoOffset - | XConst (IntConst n) when not self#is_typed -> - Ok (ConstantOffset (n, NoOffset)) - | _ -> - let tgtbtype = - if is_unknown_type tgtbtype then None else Some tgtbtype in - if self#is_struct then - let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in - self#structvar_memory_offset ~tgtsize ~tgtbtype loc btype xoffset - else if self#is_array then - let btype = TR.tvalue (resolve_type self#btype) ~default:t_unknown in - self#arrayvar_memory_offset ~tgtsize ~tgtbtype loc btype xoffset - else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" - ^ (btype_to_string self#btype) - ^ " is not known to be a struct or array"; - "gloc_address: " ^ self#address#to_hex_string; - "xoffset: " ^ (x2s xoffset)] + ^ "; tgtbtype: " ^ (ty2s tgtbtype); + "tresult: " + ^ (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end method address_memory_offset ?(tgtsize=None) @@ -706,42 +716,74 @@ object (self) [] in H.replace unconnectedreferences faddr#index (gref :: entry) + method add_location_gload + (faddr: doubleword_int) + (iaddr: ctxt_iaddress_t) + (gaddr: doubleword_int) + (offset: memory_offset_t) + (size: int) + (signed: bool) + (vtype: btype_t) = + let gload = GLoad (gaddr, iaddr, offset, size, signed, vtype) in + self#add_global_ref faddr gload + +(* method add_gload (faddr: doubleword_int) (iaddr: ctxt_iaddress_t) (gxpr: xpr_t) (size: int) - (signed: bool) = + (signed: bool): unit traceresult = match self#xpr_containing_location gxpr with | Some gloc -> let gload = GLoad (gloc#address, iaddr, gxpr, size, signed) in - self#add_global_ref faddr gload + begin + self#add_global_ref faddr gload; + Ok () + end | _ -> (match gxpr with | XConst (IntConst n) -> let gaddr = numerical_mod_to_doubleword n in let gload = GLoad (gaddr, iaddr, gxpr, size, signed) in - self#add_unconnected_ref faddr gload + begin + self#add_unconnected_ref faddr gload; + Error [(elocm __LINE__); + "Unable to match address " ^ (gaddr#to_hex_string) + ^ " with a global location. Unconnected reference " + ^ "recorded for this address"] + end | _ -> - ()) - + Error [(elocm __LINE__); + "Unable to match address " ^ (x2s gxpr) + ^ " with a global location: No load recorded"]) + *) method add_gstore (faddr: doubleword_int) (iaddr: ctxt_iaddress_t) (gxpr: xpr_t) (size: int) - (optvalue: CHNumerical.numerical_t option) = + (optvalue: CHNumerical.numerical_t option): unit traceresult = match self#xpr_containing_location gxpr with | Some gloc -> let gstore = GStore (gloc#address, iaddr, gxpr, size, optvalue) in - self#add_global_ref faddr gstore + Ok (self#add_global_ref faddr gstore) | _ -> - (match gxpr with - | XConst (IntConst n) -> - let gaddr = numerical_mod_to_doubleword n in - let gstore = GStore (gaddr, iaddr, gxpr, size, optvalue) in - self#add_unconnected_ref faddr gstore - | _ -> ()) + match gxpr with + | XConst (IntConst n) -> + let gaddr = numerical_mod_to_doubleword n in + let gstore = GStore (gaddr, iaddr, gxpr, size, optvalue) in + begin + self#add_unconnected_ref faddr gstore; + Error [(elocm __LINE__); + "Unable to match address " ^ (gaddr#to_hex_string) + ^ " with a global location. Unconnected reference " + ^ "recorded for this address"] + end + | _ -> + Error [elocm __LINE__; + "Unable to match address expression " ^ (x2s gxpr) + ^ " with a global location."] method add_gaddr_argument (faddr: doubleword_int) @@ -873,13 +915,14 @@ object (self) | Some off -> seti "mix" (vard#index_memory_offset off) | _ -> () in match gref with - | GLoad (gaddr, iaddr, gxpr, size, signed) -> + | GLoad (gaddr, iaddr, offset, size, signed, vtype) -> begin set "t" "L"; + seti "mix" (vard#index_memory_offset offset); set_gaddr gaddr; - set_gxpr gxpr; set_iaddr iaddr; set_size size; + set_btype vtype; (if signed then set "sg" "yes") end | GStore (gaddr, iaddr, gxpr, size, optvalue) -> diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index b24362d1..67267ec2 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1507,6 +1507,13 @@ type regvar_intro_t = { rvi_cast: bool } +(** Local stack variable introduced via userdata. + + Note: For user convenience the offset in the userdata is positive. This + value is negated by the CLI when it converts the json input to xml. + Within the analyzer the offsets of local stack variables are always + negative, as the stack grows down. + *) type stackvar_intro_t = { svi_offset: int; svi_name: string; @@ -1539,19 +1546,47 @@ type function_annotation_t = { class type function_data_int = object - (* setters *) + (** {1 General function information} *) + + (** {2 Function type} *) + + (** Set only from call-back tables.*) method set_function_type: btype_t -> unit + method has_function_type: bool + + (** Never called.*) + method get_function_type: btype_t + + (** {2 Non-returning} *) + method set_non_returning: unit + method is_non_returning: bool + + (** {2 Function names} *) + method add_name: string -> unit + method get_function_name: string (* demangled or combination of all names *) + method get_names: string list (* raw names *) + method has_name: bool + + (** {2 Function entry origin} *) + method set_ida_provided: unit + method is_ida_provided: bool + method set_user_provided: unit + method is_user_provided: bool + + method set_by_preamble: unit + + method set_incomplete: unit method set_virtual: unit method set_inlined: unit method set_library_stub: unit - method set_by_preamble: unit + method set_class_info: classname:string -> isstatic:bool -> unit - method set_function_annotation: function_annotation_t -> unit + method add_inlined_block: doubleword_int -> unit (** [add_path_context startaddr sentinels] causes path contexts to @@ -1570,16 +1605,30 @@ class type function_data_int = method set_stack_offset_types: ((int * btype_t option) list) -> unit - (* accessors *) - method get_names: string list (* raw names *) - method get_function_name: string (* demangled or combination of all names *) + (** {1 Function annotations} *) + + method set_function_annotation: function_annotation_t -> unit + method has_function_annotation: bool method get_function_annotation: function_annotation_t option + + (** {2 Register-variable introductions} *) + + method has_regvar_type_annotation: doubleword_int -> bool method get_regvar_type_annotation: doubleword_int -> btype_t traceresult - method get_stackvar_type_annotation: int -> btype_t traceresult + method has_regvar_type_cast: doubleword_int -> bool method get_regvar_intro: doubleword_int -> regvar_intro_t option + + (** {2 Stack-variable introductions} *) + + method has_stackvar_intro: int -> bool method get_stackvar_intro: int -> stackvar_intro_t option + method has_stackvar_type_annotation: int -> bool + method get_stackvar_type_annotation: int -> btype_t traceresult + method has_stackvar_type_cast: int -> bool + + (* accessors *) + method get_inlined_blocks: doubleword_int list - method get_function_type: btype_t method get_path_contexts: (string * string list) list method get_reglhs_types: (register_t * string * btype_t option) list method get_reglhs_type: register_t -> string -> btype_t option @@ -1587,23 +1636,17 @@ class type function_data_int = method get_stack_offset_type: int -> btype_t option (* predicates *) - method has_function_type: bool - method has_name: bool - method has_function_annotation: bool - method has_regvar_type_annotation: doubleword_int -> bool - method has_regvar_type_cast: doubleword_int -> bool - method has_stackvar_type_annotation: int -> bool - method has_stackvar_type_cast: int -> bool + method is_const_global_variable: string -> bool method filter_deflocs: string -> variable_t -> symbol_t list -> symbol_t list method is_typing_rule_enabled: ?rdef:string option -> string -> string -> bool method has_class_info: bool method has_callsites: bool method has_path_contexts: bool - method is_non_returning: bool + method is_incomplete: bool - method is_ida_provided: bool - method is_user_provided: bool + + method is_virtual: bool method is_inlined: bool method is_library_stub: bool @@ -4192,6 +4235,10 @@ object Note: The first stack parameter for ARM is at 0.*) method is_stack_parameter_variable: variable_t -> bool + (** Returns [true] if [var] is a memory variable located on the stack + with negative offset from the initial value of the stack pointer. *) + method is_local_stack_variable: variable_t -> bool + (** Returns the index of the stack parameter variable [var] assuming 4-byte parameters starting at offset 4 (x86 only). The variable may either be a stack memory variable or a stack initial memory value. @@ -4375,12 +4422,22 @@ type globalvalue_t = (** Reference to a global location*) type global_location_ref_t = - | GLoad of doubleword_int * ctxt_iaddress_t * xpr_t * int * bool + | GLoad of doubleword_int (* global location address *) + * ctxt_iaddress_t (* instruction address *) + * memory_offset_t (* offset within global location *) + * int (* size of load *) + * bool (* load is signed *) + * btype_t (* type of element loaded *) (** address of global location, instructions address of load instruction, load address, size of load, signed *) - | GStore of - doubleword_int * ctxt_iaddress_t * xpr_t * int * numerical_t option + | GStore of doubleword_int + * ctxt_iaddress_t + * xpr_t + * int + * numerical_t option +(* | GStore of + doubleword_int * ctxt_iaddress_t * xpr_t * int * numerical_t option *) (** address of global location, instruction address of store instruction, store address, size of store, optional numerical value assigned *) @@ -4496,10 +4553,24 @@ class type global_location_int = (** Container for global locations in the system in the data sections, including initialized and uninitialized (.bss) data, but typically - excluding data contained within the .text section.*) + excluding data contained within the .text section. + + Currently no type inference is performed for global variables. It is + assumed that all (relevant) types of global variables are provided + in userdata. +*) class type global_memory_map_int = object + (** {1 Sections} *) + + (** [set_section readonly initialized name startaddr size] adds a section + with the give attributes: whether it is readonly, initialized, its + name in the binary, its virtual start address and its size in bytes. + + The partition of global memory into sections enables the characterization + of global variables in terms of being initialized and constant. + *) method set_section: readonly:bool -> initialized:bool @@ -4508,6 +4579,32 @@ class type global_memory_map_int = -> doubleword_int -> unit + (** {1 Locations} *) + + (** A memory location corresponds to a single global variable identified by + a name, where the name can come from a symbol embedded in the binary, + or from userdata, or, if both of these are absent, an automatically + generated name of the form [gv_
].*) + + (** {2 Creating locations} *) + + (** [add_location name desc btype initialvalue size address] creates a new global + location with the given name (or [gv_
]) and type, initial value, + and size (if available) at the given [address], if it does not overlap with + an already existing global location. + + If a new global location is created the new global location is returned. If + another global location already exists at the same address the original + location is returned, an error message is logged, and the global memory map + remains unchanged. If the provided address and size overlap with an existing + global location an error is returned, and the global memory map remains + unchanged. + + A global location can be created before disassembly from a symbolic address + in userdata, or at initial disassembly from a symbol in the binary, from + a global variable in a C header file with the name [gv_
], or as the + result of variable discovery during disassembly or analysis. + *) method add_location: ?name:string option -> ?desc:string option @@ -4517,21 +4614,60 @@ class type global_memory_map_int = -> doubleword_int -> global_location_int traceresult - method add_gload: + (** {2 Updating locations} *) + + (** Locations can be updated in two ways: + - adding type information from named global variables in C header files; + - adding code access information, including loads, stores, and use as a + function argument. + *) + + (** [update_named_location name varinfo] supplements an earlier created global + location with the same [name] with associated type information obtained from + a C header file. + + It is expected that a global location with the given name has already been + created either from a symbol in the binary or from a symbolic address in + the userdata. + *) + method update_named_location: + string -> bvarinfo_t -> global_location_int traceresult + + (** [add_gload faddr iaddr gaddr size signed] records a load operation by an + instruction in function [faddr] at address [iaddr] for a global variable with + address expression [gaddr] and size [size] in bytes. + + If gaddr is a valid global address, but no global location is present at this + address, an unconnected reference is recorded, and an error is returned. + + If gaddr cannot be reduced to a valid global address, an error is returned. + *) + method add_location_gload: doubleword_int -> ctxt_iaddress_t - -> xpr_t + -> doubleword_int + -> memory_offset_t -> int -> bool + -> btype_t -> unit + (** [add_gstore faddr iaddr gaddr size value] records a store operation by + an instruction in function [faddr] at address [iaddr] for a global variable with + address expression [gaddr] and size [size] in bytes. + + If gaddr is a valid global address, but no global location is present at this + address, an unconnected reference is recorded, and an error is returned. + + If gaddr cannot be reduced to a valid global address, an error is returned. + *) method add_gstore: doubleword_int -> ctxt_iaddress_t -> xpr_t -> int -> numerical_t option - -> unit + -> unit traceresult method add_gaddr_argument: doubleword_int @@ -4541,9 +4677,6 @@ class type global_memory_map_int = -> btype_t -> global_location_int option - method update_named_location: - string -> bvarinfo_t -> global_location_int traceresult - method has_location: doubleword_int -> bool method get_location: doubleword_int -> global_location_int @@ -4605,6 +4738,7 @@ class type stackslot_int = method name: string method offset: int method btype: btype_t + method offset_type: memory_offset_t -> btype_t traceresult method spill: register_t option method size: int option method desc: string option @@ -4613,11 +4747,13 @@ class type stackslot_int = method frame_offset_memory_offset: ?tgtsize:int option -> ?tgtbtype:btype_t + -> location_int -> xpr_t -> memory_offset_t traceresult method object_offset_memory_offset: ?tgtsize:int option -> ?tgtbtype:btype_t + -> location_int -> xpr_t -> memory_offset_t traceresult @@ -4626,12 +4762,22 @@ class type stackslot_int = method is_struct: bool method is_array: bool method is_spill: bool + method is_compatible_with_spill: bool method is_loopcounter: bool method write_xml: xml_element_int -> unit end + (** Function stackframe consisting of stackslots. The function stackframe + includes both the local stackframe (containing stackslots with negative + offset) and the function argument area (stackslots with non-negative + offset) + + Stack slots for stack variables included in the function annotations of + the userdata are created upon initialization of the stackframe. Other + stack slots are added as needed when stack variables are discovered. +*) class type stackframe_int = object @@ -4649,8 +4795,12 @@ class type stackframe_int = -> int -> stackslot_int traceresult + method has_stackslot: int -> bool + method containing_stackslot: int -> stackslot_int option + method xpr_containing_stackslot: xpr_t -> stackslot_int option + method add_load: baseoffset:int -> offset: memory_offset_t @@ -4833,8 +4983,18 @@ class type function_environment_int = method mk_gloc_variable: global_location_int -> memory_offset_t -> variable_t + (** [mk_stackslot_variable stackslot memoff] creates a stack variable for an + existing stackslot with memory offset [memoff]. + + It also sets the name of the stack variable and the name of the stack + variable with offset according to the name of the stackslot. + *) + method mk_stackslot_variable: + stackslot_int -> memory_offset_t -> variable_t +(* method mk_stack_variable: ?size: int -> stackframe_int -> numerical_t -> variable_t traceresult + *) (** [mk_initial_memory_value var] returns an auxiliary variable that represents the initial value of [var] at function entry. @@ -5066,6 +5226,10 @@ class type function_environment_int = Note: The first stack parameter for ARM is at 0.*) method is_stack_parameter_variable: variable_t -> bool + (** Returns [true] if [var] is a memory variable located on the with + negative offset from the initial value of the stack pointer. *) + method is_local_stack_variable: variable_t -> bool + (** Returns [true] if [var] is the initial-value variable of a stack-parameter variable. *) method is_stack_parameter_value: variable_t -> bool @@ -6146,6 +6310,13 @@ class type floc_int = method get_singleton_stackpointer_offset: numerical_t traceresult + (** [get_stackpointer_offset_xpr x] returns the expression [x - sp_in] where + sp_in is the initial stackpointer value for the function. + + If [x] does not contain [sp_in] as a positive term, an Error is returned. + *) + method get_stackpointer_offset_xpr: xpr_t -> xpr_t traceresult + method get_var_at_address: ?size:int option (** size of the argument, in bytes *) -> ?btype:btype_t (** type of argument *) @@ -6157,11 +6328,6 @@ class type floc_int = *) method get_lhs_from_address: xpr_t -> variable_t - method get_variable_type: variable_t -> btype_t traceresult - - method get_xpr_type: xpr_t -> btype_t traceresult - - (** {2 Predicates on variables}*) @@ -6182,8 +6348,31 @@ class type floc_int = register *) method has_initial_value: variable_t -> bool + method get_variable_type: variable_t -> btype_t traceresult + + method get_xpr_type: xpr_t -> btype_t traceresult + + + (** {1 Conversion to c expressions / variables} + + Expressions involving memory operands are initially created with a + base variable and, if applicable, a numerical offset in bytes. + + In liftings to c these numerical offsets must be converted to + type-aware offsets such as fields and array indices. - (** {1 Conversion to c expressions / variables}*) + The functions provided here attempt this conversion using the results + of type inference performed earlier. To ensure maximum type availability + these functions should only be called after type inference for a given + function has been completed. In particular, these functions should not + be called by the type inference itself. + + The four main sources for types are: + 1. c header files: function signatures and declaration of global variables + 2. function signatures from function summaries + 3. userdata: typed register and stack variable introductions + 4. type inference, based on (1) and (2)and (3) and instruction semantics + *) method xpr_to_cxpr: ?arithm:bool @@ -6201,18 +6390,6 @@ class type floc_int = -> variable_t -> variable_t traceresult - method convert_value_offsets: - ?size:int option -> variable_t -> variable_t traceresult - - method convert_variable_offsets: - ?vtype:btype_t option - -> ?size:int option - -> variable_t - -> variable_t traceresult - - method convert_xpr_offsets: - ?xtype:btype_t option -> ?size:int option -> xpr_t -> xpr_t traceresult - (** {1 Conditional jumps}*) diff --git a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml index ecbf5de9..c8104cd5 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml @@ -40,11 +40,13 @@ open XprTypes (* bchlib *) open BCHBCTypes +open BCHBCTypePretty open BCHBCTypeUtil open BCHDoubleword open BCHGlobalState open BCHLibTypes open BCHLocation +open BCHMemoryReference module TR = CHTraceResult @@ -53,11 +55,24 @@ let x2p = xpr_formatter#pr_expr let p2s = CHPrettyUtil.pretty_to_string let x2s x = p2s (x2p x) -let mmap = BCHGlobalMemoryMap.global_memory_map +let x2s_r x_r = + match x_r with + | Ok x -> x2s x + | Error e -> "Error: " ^ (String.concat "; " e) + +(* Emit log message only in the last run of the analyzer. *) +let log_dc_error_result + ?(msg="") + ?(tag="") + (filename: string) + (linenumber: int) + (msgs: string list) = + if BCHSystemSettings.system_settings#collect_data then + log_error_result ~msg ~tag filename linenumber msgs -let log_error (tag: string) (msg: string) = - mk_tracelog_spec ~tag:("memoryrecorder:" ^ tag) msg + +let mmap = BCHGlobalMemoryMap.global_memory_map class memory_recorder_t @@ -83,24 +98,42 @@ object (self) match x with | XConst (IntConst n) -> GConstant n | XVar v when self#env#is_return_value v -> - log_tfold - (log_error "get_gvalue" "invalid call site") + TR.tfold ~ok:(fun callSite -> GReturnValue (ctxt_string_to_location self#faddr callSite)) - ~error:(fun _ -> GUnknownValue) + ~error:(fun e -> + begin + log_diagnostics_result + ~msg:(p2s self#loc#toPretty) + ~tag:"memrecorder:get_gvalue" + __FILE__ __LINE__ (e @ ["invalid callsite"]); + GUnknownValue + end) (self#env#get_call_site v) | XVar v when self#env#is_sideeffect_value v -> - log_tfold - (log_error "get_gvalue" "invalid call site (2)") + TR.tfold ~ok: (fun callSite -> - log_tfold - (log_error "get_gvalue" "invalid se descriptor") + TR.tfold ~ok:(fun argdescr -> GSideeffectValue (ctxt_string_to_location self#faddr callSite, argdescr)) - ~error:(fun _ -> GUnknownValue) + ~error:(fun e -> + begin + log_diagnostics_result + ~msg:(p2s self#loc#toPretty) + ~tag:"memrecorder:get_gvalue" + __FILE__ __LINE__ (e @ ["invalide side-effect descriptor"]); + GUnknownValue + end) (self#env#get_se_argument_descriptor v)) - ~error:(fun _ -> GUnknownValue) + ~error:(fun e -> + begin + log_diagnostics_result + ~msg:(p2s self#loc#toPretty) + ~tag:"memrecorder:get_gvalue" + __FILE__ __LINE__ (e @ ["invalide side-effect value"]); + GUnknownValue + end) (self#env#get_call_site v) | XVar v when self#env#is_stack_parameter_variable v -> (match self#env#get_stack_parameter_index v with @@ -137,16 +170,19 @@ object (self) (vtype: btype_t) = if self#env#is_global_variable lhs && (self#env#has_global_variable_address lhs) then - log_tfold - (log_error "record_assignment_lhs" "invalid global address") + TR.tfold ~ok:(fun gaddr -> global_system_state#add_writer ~ty:vtype ~size (self#get_gvalue rhs) gaddr self#loc) - ~error:(fun _ -> ()) + ~error:(fun e -> + log_error_result + ~tag:"record_assignment_lhs" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + (["invalid global address for: " ^ (p2s lhs#toPretty)] @ e)) (self#env#get_global_variable_address lhs) else if self#env#is_stack_variable lhs then - log_tfold - (log_error "record_assignment_lhs" "invalid offset") + TR.tfold ~ok:(fun stackoffset -> match stackoffset with | ConstantOffset (n, offset) -> @@ -159,15 +195,27 @@ object (self) lhs iaddr | _ -> - chlog#add - "stack assignment lhs not recorded" - (LBLOCK [self#loc#toPretty; STR ": "; lhs#toPretty])) - ~error:(fun _ -> ()) + log_diagnostics_result + ~tag:"record_assignment_lhs" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + ["stack assignment lhs not recorded"; + "lhs: " ^ (p2s lhs#toPretty)]) + ~error:(fun e -> + log_error_result + ~tag:"record_assignment_lhs" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + (["invalid offset for: " ^ (p2s lhs#toPretty)] @ e)) (self#env#get_memvar_offset lhs) else - chlog#add - "assignment lhs not recorded" - (LBLOCK [self#loc#toPretty; STR ": "; lhs#toPretty; STR " := "; x2p rhs]) + log_diagnostics_result + ~tag:"record_assignment_lhs" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + ["assignment lhs not recorded"; + "lhs: " ^ (p2s lhs#toPretty); + "rhs: " ^ (x2s rhs)] method private record_assignment_rhs (rhs: xpr_t) (size: int option) (vtype: btype_t) = @@ -175,15 +223,18 @@ object (self) List.iter (fun v -> if self#env#is_global_variable v && (self#env#has_global_variable_address v) then - log_tfold - (log_error "record_assignment_rhs" "invalid global address") + TR.tfold ~ok:(fun gaddr -> global_system_state#add_reader ~ty:vtype ~size gaddr self#loc) - ~error:(fun _ -> ()) + ~error:(fun e -> + log_error_result + ~tag:"record_assignment_rhs" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + (["invalid global address for: " ^ (x2s rhs)] @ e)) (self#env#get_global_variable_address v) else if self#env#is_stack_variable v then - log_tfold - (log_error "record_assignment_rhs" "invalid offset") + TR.tfold ~ok:(fun stackoffset -> match stackoffset with | ConstantOffset (n, offset) -> @@ -195,15 +246,28 @@ object (self) v iaddr | _ -> - chlog#add - "stack assignment rhs not recorded" - (LBLOCK [self#loc#toPretty; STR ": "; v#toPretty])) - ~error:(fun _ -> ()) + log_diagnostics_result + ~tag:"record_assignment_rhs" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + ["stack assignment rhs not recorded"; + "v: " ^ (p2s v#toPretty); + "rhs: " ^ (x2s rhs)]) + ~error:(fun e -> + log_error_result + ~tag:"record_assignment_rhs" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + (["invalid offset for: " ^ (x2s rhs)] @ e)) (self#env#get_memvar_offset v) else - chlog#add - "assignment rhs not recorded" - (LBLOCK [self#loc#toPretty; STR ": "; v#toPretty])) vars + log_diagnostics_result + ~tag:"record_assignment_rhs" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + ["assignment not recorded"; + "v: " ^ (p2s v#toPretty); + "rhs: " ^ (x2s rhs)]) vars method record_load ~(signed: bool) @@ -211,46 +275,88 @@ object (self) ~(var: variable_t) ~(size: int) ~(vtype: btype_t) = + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"deprecated: record_load" + __FILE__ __LINE__ + ["memory_recorder#record_load is deprecated. "; + "To be replaced with record_load_r"; + "signed: " ^ (if signed then "T" else "F"); + "addr: " ^ (x2s addr); + "var: " ^ (p2s var#toPretty); + "size: " ^ (string_of_int size); + "vtype: " ^ (btype_to_string vtype)] + (* if self#env#is_stack_variable var then - log_tfold - (log_error "record_load" "invalid offset") - ~ok:(fun stackoffset -> - match stackoffset with - | ConstantOffset (n, offset) -> - self#finfo#stackframe#add_load - ~baseoffset:n#toInt - ~offset - ~size:(Some size) - ~typ:(Some vtype) - var - iaddr - | _ -> - chlog#add - "stack load not recorded" - (LBLOCK [ - self#loc#toPretty; - STR ": "; - x2p addr; - STR " ("; - var#toPretty; - STR ")"])) - ~error:(fun _ -> ()) - (self#env#get_memvar_offset var) + self#record_stack_variable_load ~signed ~var ~size ~vtype + else if self#env#is_basevar_memory_variable var then + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record memory load" + __FILE__ __LINE__ + ["Recording of basevar loads not yet supported. Var: " + ^ (p2s var#toPretty) + ^ ". Addr: " ^ (x2s addr)] else - match addr with - | XConst (IntConst n) - when mmap#is_global_data_address (numerical_mod_to_doubleword n) -> - mmap#add_gload self#faddr iaddr addr size signed - | _ -> - chlog#add - "memory load not recorded" - (LBLOCK [ - self#loc#toPretty; - STR "; "; - x2p addr; - STR " ("; - var#toPretty; - STR ")"]) + match mmap#add_gload self#faddr iaddr addr size signed with + | Ok () -> () + | Error e -> + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_load" + __FILE__ __LINE__ e + *) + + method private record_stack_variable_load + ~(signed: bool) + ~(var: variable_t) + ~(size: int) + ~(vtype: btype_t) = + TR.tfold + ~ok:(fun stackoffset -> + match stackoffset with + | ConstantOffset (n, offset) -> + self#finfo#stackframe#add_load + ~baseoffset:n#toInt + ~offset + ~size:(Some size) + ~typ:(Some vtype) + var + iaddr + | _ -> + log_dc_error_result + ~tag:"record_stack_variable_load" + ~msg:(p2s self#loc#toPretty) + __FILE__ __LINE__ + ["offset: " ^ (BCHMemoryReference.memory_offset_to_string stackoffset); + "signed: " ^ (if signed then "yes" else "no")]) + ~error:(fun e -> log_dc_error_result __FILE__ __LINE__ e) + (self#env#get_memvar_offset var) + + method private record_global_variable_load + ~(signed: bool) + ~(var: variable_t) + ~(size: int) = + TR.tfold + ~ok:(fun globaloffset -> + match globaloffset with + | ConstantOffset (n, offset) -> + let gaddr = numerical_mod_to_doubleword n in + mmap#add_location_gload self#faddr iaddr gaddr offset size signed t_unknown + | _ -> + log_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_global_variable_load" + __FILE__ __LINE__ + ["Unexpected offset for global variable " ^ (p2s var#toPretty) + ^ ": " ^ (memory_offset_to_string globaloffset)]) + ~error:(fun e -> + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_global_variable_load" + __FILE__ __LINE__ + (e @ ["Unable to obtain offset from variable " ^ (p2s var#toPretty)])) + (self#env#get_memvar_offset var) method record_load_r ~(signed: bool) @@ -261,45 +367,46 @@ object (self) TR.tfold ~ok:(fun var -> if self#env#is_stack_variable var then - TR.tfold - ~ok:(fun stackoffset -> - match stackoffset with - | ConstantOffset (n, offset) -> - self#finfo#stackframe#add_load - ~baseoffset:n#toInt - ~offset - ~size:(Some size) - ~typ:(Some vtype) - var - iaddr - | _ -> - log_error_result __FILE__ __LINE__ - ["memrecorder:stack-load"; - p2s self#loc#toPretty; - "offset: " - ^ (BCHMemoryReference.memory_offset_to_string stackoffset)]) - ~error:(fun e -> log_error_result __FILE__ __LINE__ e) - (self#env#get_memvar_offset var) + self#record_stack_variable_load ~signed ~var ~size ~vtype + else if self#env#is_global_variable var then + self#record_global_variable_load ~signed ~var ~size + else if self#env#is_basevar_memory_variable var then + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_load_r" + __FILE__ __LINE__ + ["Recording of basevar loads not yet supported. Var: " + ^ (p2s var#toPretty) + ^ ". Addr: " ^ (x2s_r addr_r)] else TR.tfold ~ok:(fun addr -> - match addr with - | XConst (IntConst n) - when mmap#is_global_data_address - (numerical_mod_to_doubleword n) -> - mmap#add_gload self#faddr iaddr addr size signed - | XConst (IntConst n) -> - log_result __FILE__ __LINE__ - ["memrecorder:literal load not recorded"; - p2s self#loc#toPretty; - p2s (numerical_mod_to_doubleword n)#toPretty] - | _ -> - log_result __FILE__ __LINE__ - ["memrecorder:load not recorded"; - p2s self#loc#toPretty; (x2s addr)]) - ~error:(fun e -> log_error_result __FILE__ __LINE__ e) + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_load_r" + __FILE__ __LINE__ + ["Unable to record memory load for variable " ^ (p2s var#toPretty) + ^ " with address " ^ (x2s addr)]) + ~error:(fun e -> + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_load_r" + __FILE__ __LINE__ + (["Unable to record memory load for variable " ^ (p2s var#toPretty)] + @ e)) + (* + TR.tfold + ~ok:(fun addr -> + match mmap#add_gload self#faddr iaddr addr size signed with + | Ok () -> () + | Error e -> + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_load" + __FILE__ __LINE__ e) + ~error:(fun e -> log_error_result __FILE__ __LINE__ e)*) addr_r) - ~error:(fun e -> log_error_result __FILE__ __LINE__ e) + ~error:(fun e -> log_dc_error_result __FILE__ __LINE__ e) var_r method record_store @@ -309,52 +416,73 @@ object (self) ~(vtype: btype_t) ~(xpr: xpr_t) = if self#env#is_stack_variable var then - log_tfold - (log_error "record_store" "invalid offset") - ~ok:(fun stackoffset -> - match stackoffset with - | ConstantOffset (n, offset) -> - self#finfo#stackframe#add_store - ~baseoffset:n#toInt - ~offset - ~size:(Some size) - ~typ:(Some vtype) - ~xpr:(Some xpr) - var - iaddr - | _ -> - chlog#add - "stack store not recorded" - (LBLOCK [ - self#loc#toPretty; - STR ": "; - x2p addr; - STR " ("; - var#toPretty; - STR "): "; - x2p xpr])) - ~error:(fun _ -> ()) - (self#env#get_memvar_offset var) + self#record_stack_variable_store ~var ~size ~vtype ~xpr_r:(Ok xpr) + else if self#env#is_basevar_memory_variable var then + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record memory store" + __FILE__ __LINE__ + ["Recording of basevar loads not yet supported. Var: " + ^ (p2s var#toPretty) + ^ ". Addr: " ^ (x2s addr)] else + let optvalue = + match xpr with + | XConst (IntConst n) -> Some n + | _ -> None in + let add_gstore gaddr = + match mmap#add_gstore self#faddr iaddr gaddr size optvalue with + | Ok () -> () + | Error e -> + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_store" + __FILE__ __LINE__ + (["addr: " ^ (x2s addr); "var: " ^ (p2s var#toPretty)] @ e) in + (* match addr with - | XConst (IntConst n) - when mmap#is_global_data_address (numerical_mod_to_doubleword n) -> - let optvalue = - match xpr with - | XConst (IntConst n) -> Some n - | _ -> None in - mmap#add_gstore self#faddr iaddr addr size optvalue - | _ -> - chlog#add - "memory store not recorded" - (LBLOCK [ - self#loc#toPretty; - STR ": "; - x2p addr; - STR " ("; - var#toPretty; - STR "): "; - x2p xpr]) + | XOp ((Xf "addressofvar"), [XVar v]) when self#env#is_global_variable v -> + TR.tfold + ~ok:add_gstore + ~error:(fun e -> + begin + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_store" + __FILE__ __LINE__ + (["addr: " ^ (x2s addr); "var: " ^ (p2s var#toPretty)] @ e); + () + end) + (self#env#get_global_variable_address v) + | _ -> *) add_gstore addr + + method private record_stack_variable_store + ~(var: variable_t) + ~(size: int) + ~(vtype: btype_t) + ~(xpr_r: xpr_t traceresult) = + TR.tfold + ~ok:(fun stackoffset -> + match stackoffset with + | ConstantOffset (n, offset) -> + self#finfo#stackframe#add_store + ~baseoffset:n#toInt + ~offset + ~size:(Some size) + ~typ:(Some vtype) + ~xpr:(TR.tfold_default (fun x -> Some x) None xpr_r) + var + iaddr + | _ -> + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record_store" + __FILE__ __LINE__ + ["var: " ^ (p2s var#toPretty); + "stack offset: " + ^ BCHMemoryReference.memory_offset_to_string stackoffset]) + ~error:(fun e -> log_error_result __FILE__ __LINE__ e) + (self#env#get_memvar_offset var) method record_store_r ~(addr_r: xpr_t traceresult) @@ -365,52 +493,34 @@ object (self) TR.tfold ~ok:(fun var -> if self#env#is_stack_variable var then - TR.tfold - ~ok:(fun stackoffset -> - match stackoffset with - | ConstantOffset (n, offset) -> - self#finfo#stackframe#add_store - ~baseoffset:n#toInt - ~offset - ~size:(Some size) - ~typ:(Some vtype) - ~xpr:(TR.tfold_default (fun x -> Some x) None xpr_r) - var - iaddr - | _ -> - log_error_result __FILE__ __LINE__ - ["memrecorder:stack-store"; - p2s self#loc#toPretty; - "offset: " - ^ BCHMemoryReference.memory_offset_to_string stackoffset]) - ~error:(fun e -> log_error_result __FILE__ __LINE__ e) - (self#env#get_memvar_offset var) + self#record_stack_variable_store ~var ~size ~vtype ~xpr_r + else if self#env#is_basevar_memory_variable var then + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record memory store" + __FILE__ __LINE__ + ["Recording of basevar loads not yet supported. Var: " + ^ (p2s var#toPretty) + ^ ". Addr: " ^ (x2s_r addr_r)] else TR.tfold ~ok:(fun addr -> - match addr with - | XConst (IntConst n) - when mmap#is_global_data_address - (numerical_mod_to_doubleword n) -> - let optvalue = - TR.tfold_default - (fun xpr -> - match xpr with - | XConst (IntConst n) -> Some n - | _ -> None) - None - xpr_r in - mmap#add_gstore self#faddr iaddr addr size optvalue - | _ -> - log_error_result __FILE__ __LINE__ - ["memrecorder: store not recorded"; - p2s self#loc#toPretty; (x2s addr)]) + let optvalue = + match xpr_r with + | Ok (XConst (IntConst n)) -> Some n + | _ -> None in + match mmap#add_gstore self#faddr iaddr addr size optvalue with + | Ok () -> () + | Error e -> + log_dc_error_result + ~msg:(p2s self#loc#toPretty) + ~tag:"record store" + __FILE__ __LINE__ e) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) addr_r) - ~error:(fun e -> log_error_result __FILE__ __LINE__ e) + ~error:(fun e -> log_dc_error_result __FILE__ __LINE__ e) var_r - end diff --git a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml index 2ba844bd..d7fdbc28 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryReference.ml +++ b/CodeHawk/CHB/bchlib/bCHMemoryReference.ml @@ -190,6 +190,7 @@ let rec address_memory_offset | XConst (IntConst n) -> n#equal CHNumerical.numerical_zero | _ -> false in let rbasetype = TR.tvalue (resolve_type basetype) ~default:t_unknown in + let tresult = match xoffset with | XConst (IntConst n) when is_unknown_type rbasetype -> let _ = @@ -249,14 +250,52 @@ let rec address_memory_offset ^ "Nonzero suboffset encountered when extracting index " ^ "from " ^ (x2s xoffset) ^ " with base type " ^ (btype_to_string rbasetype)]) - tsize_r + tsize_r in + begin + log_diagnostics_result + ~tag:"address_memory_offset" + __FILE__ __LINE__ + ["basetype: " ^ (btype_to_string basetype); + "xoffset: " ^ (x2s xoffset); + "tresult: " + ^ (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end and structvar_memory_offset ~(tgtsize: int option) ~(tgtbtype: btype_t option) (btype: btype_t) (xoffset: xpr_t): memory_offset_t traceresult = - let _ = + let tresult = + match xoffset with + | XConst (IntConst n) + when n#equal numerical_zero + && (Option.is_some tgtbtype) + && (btype_equal (Option.get tgtbtype) btype) -> + Ok NoOffset + | XConst (IntConst _) -> + if is_struct_type btype then + let compinfo = get_struct_type_compinfo btype in + (get_field_memory_offset_at ~tgtsize ~tgtbtype compinfo xoffset) + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" + ^ " xoffset: " ^ (x2s xoffset) + ^ "; btype: " ^ (btype_to_string btype)] + | _ -> + if is_struct_type btype then + let compinfo = get_struct_type_compinfo btype in + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "xoffset: " ^ (x2s xoffset) + ^ "; type: struct " ^ compinfo.bcname] + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "xoffset: " ^ (x2s xoffset) + ^ "; btype: " ^ (btype_to_string btype)] in + begin log_diagnostics_result ~tag:"structvar-memory-offset" __FILE__ __LINE__ @@ -266,31 +305,14 @@ and structvar_memory_offset ^ (if Option.is_some tgtbtype then (btype_to_string (Option.get tgtbtype)) else "?"); "btype: " ^ (btype_to_string btype); - "xoffset: " ^ (x2s xoffset)] in - match xoffset with - | XConst (IntConst n) - when n#equal numerical_zero - && (Option.is_some tgtbtype) - && (btype_equal (Option.get tgtbtype) btype) -> - Ok NoOffset - | XConst (IntConst _) -> - if is_struct_type btype then - let compinfo = get_struct_type_compinfo btype in - (get_field_memory_offset_at ~tgtsize ~tgtbtype compinfo xoffset) - else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ":" - ^ " xoffset: " ^ (x2s xoffset) - ^ "; btype: " ^ (btype_to_string btype)] - | _ -> - if is_struct_type btype then - let compinfo = get_struct_type_compinfo btype in - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "xoffset: " ^ (x2s xoffset) - ^ "; type: struct " ^ compinfo.bcname] - else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "xoffset: " ^ (x2s xoffset) - ^ "; btype: " ^ (btype_to_string btype)] + "xoffset: " ^ (x2s xoffset); + "tresult: " + ^ (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end and arrayvar_memory_offset ~(tgtsize: int option) @@ -375,6 +397,7 @@ and get_field_memory_offset_at | _, Some ty when not (btype_equal ty t) -> type_discrepancy ty t | _ -> "" in + let tresult = match xoffset with | XConst (IntConst n) -> let offset = n#toInt in @@ -400,7 +423,7 @@ and get_field_memory_offset_at let offset = offset - foff in TR.tbind ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun fldtype -> + (fun fldtype -> if offset = 0 && (is_scalar fldtype) && (check_tgttype_compliance fldtype sz) then @@ -449,7 +472,26 @@ and get_field_memory_offset_at ^ "Unable to find field at offset " ^ (string_of_int offset)]) | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Unable to determine field for xoffset: " ^ (x2s xoffset)] + ^ "Unable to determine field for xoffset: " ^ (x2s xoffset)] in + begin + log_diagnostics_result + ~tag:"get_fieldmemory_offset_at" + __FILE__ __LINE__ + ["tgtsize: " + ^ (if Option.is_some tgtsize then (string_of_int (Option.get tgtsize)) else "?"); + "tgtbtype: " + ^ (if Option.is_some tgtbtype then (btype_to_string (Option.get tgtbtype)) + else "?"); + "compinfo: " ^ c.bcname; + "xoffset: " ^ (x2s xoffset); + "tresult: " + ^ (TR.tfold + ~ok:memory_offset_to_string + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end + let rec is_unknown_offset offset = @@ -547,8 +589,10 @@ let stack_offset_to_name offset = match offset with | ConstantOffset (n,NoOffset) when n#gt numerical_zero -> "arg_" ^ (constant_offset_to_suffix_string n) - | ConstantOffset (n,NoOffset) when n#lt numerical_zero -> - "var_" ^ (constant_offset_to_neg_suffix_string n) + | ConstantOffset (n, off) when n#lt numerical_zero -> + "var_" + ^ (constant_offset_to_neg_suffix_string n) + ^ (memory_offset_to_string off) | ConstantOffset (n,NoOffset) when n#equal numerical_zero -> "var_0000" | NoOffset -> "var_0000" diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml index ac6272fd..5cd052fa 100644 --- a/CodeHawk/CHB/bchlib/bCHVariable.ml +++ b/CodeHawk/CHB/bchlib/bCHVariable.ml @@ -96,9 +96,9 @@ object (self:'a) | "gv" -> global_offset_to_name size offset | _ -> (match offset with - | NoOffset -> "__pderef_" ^ basename ^ "_" + | NoOffset -> basename ^ "[0]" | ConstantOffset _ -> basename ^ (memory_offset_to_string offset) - | _ -> "__pderef_" ^ basename ^ (memory_offset_to_string offset))) + | _ -> basename ^ (memory_offset_to_string offset))) | RegisterVariable reg -> register_to_string reg | CPUFlagVariable flag -> flag_to_string flag | AuxiliaryVariable a -> @@ -963,6 +963,13 @@ object (self) else false + method is_local_stack_variable (v: variable_t) = + if (self#is_stack_variable v) && (self#has_constant_offset v) then + let memoff_r = tbind get_total_constant_offset (self#get_memvar_offset v) in + tfold_default (fun memoff -> memoff#lt numerical_zero) false memoff_r + else + false + method is_realigned_stack_variable (v:variable_t) = (self#is_memory_variable v) && (tfold_default diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 3112e833..383958b1 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2025 Aarno Labs LLC + Copyright (c) 2021-2026 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20251022" - ~date:"2025-10-22" + ~version:"0.6.0_20260122" + ~date:"2026-01-22" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlib/bCHXprUtil.ml b/CodeHawk/CHB/bchlib/bCHXprUtil.ml index 29d04639..05191ec9 100644 --- a/CodeHawk/CHB/bchlib/bCHXprUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHXprUtil.ml @@ -62,6 +62,33 @@ let rec largest_constant_term (x:xpr_t): numerical_t = | _ -> numerical_zero +let smallest_constant_term (x: xpr_t): numerical_t = + let rec aux (x: xpr_t) (polarity: bool) = + match x, polarity with + | XConst (IntConst n), true -> n + | XConst (IntConst n), false -> n#neg + | XOp (XPlus, [x1; x2]), _ -> + let c1 = aux x1 polarity in + let c2 = aux x2 polarity in + if c1#lt c2 then c1 else c2 + | XOp (XMinus, [x1; x2]), _ -> + let c1 = aux x1 polarity in + let c2 = aux x2 (not polarity) in + if c1#lt c2 then c1 else c2 + | _ -> mkNumericalPowerOf2 31 in + aux x true + + +let smallest_wrapped_constant_term (x: xpr_t): numerical_t * numerical_t = + let x = simplify_xpr x in + let l = largest_constant_term x in + let s = smallest_constant_term x in + if l#gt (mkNumericalPowerOf2 31) then + (l, l#sub (mkNumericalPowerOf2 32)) + else + (s, s) + + (* rewrites the expression in a form with scaled terms first, followed by a constant term. *) let normalize_offset_expr (x:xpr_t) = @@ -100,7 +127,6 @@ let normalize_scaled_ivar_expr (xpr: xpr_t) (ivar: variable_t): xpr_t option = aux xpr - let rec vars_as_positive_terms (x:xpr_t) = match x with XVar v -> [ v ] diff --git a/CodeHawk/CHB/bchlib/bCHXprUtil.mli b/CodeHawk/CHB/bchlib/bCHXprUtil.mli index 9e4a9d3b..d072129f 100644 --- a/CodeHawk/CHB/bchlib/bCHXprUtil.mli +++ b/CodeHawk/CHB/bchlib/bCHXprUtil.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2022 Henny B. Sipma - Copyright (c) 2023-2024 Aarno Labs LLC + Copyright (c) 2023-2025 Aarno Labs LLC Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal @@ -36,9 +36,21 @@ open XprTypes (** returns the largest constant term in the given expression, taking into - account the sign. *) + account the sign. If there are no constant terms, zero is returned.*) val largest_constant_term : xpr_t -> numerical_t + +(** returns the smallest constant term in the given expression, taking into + account the sign. If there are no constant terms, zero is returned.*) +val smallest_constant_term: xpr_t -> numerical_t + +(** returns the smallest constant term in the given expression, while + wrapping constants larger than 2^31 into negative numbers. The pair + returned is the term as appearing in the expression and the corresponding + negative value. +*) +val smallest_wrapped_constant_term: xpr_t -> numerical_t * numerical_t + val normalize_offset_expr: xpr_t -> xpr_t val normalize_scaled_ivar_expr: xpr_t -> variable_t -> xpr_t option diff --git a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml index 8d3c9d39..078a3491 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml @@ -60,8 +60,12 @@ open BCHARMTypes module TR = CHTraceResult -(* let x2p = XprToPretty.xpr_formatter#pr_expr *) +let x2p = XprToPretty.xpr_formatter#pr_expr let p2s = pretty_to_string +let x2s x = p2s (x2p x) + +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " let arm_operand_mode_to_string = function RD -> "RD" | WR -> "WR" | RW -> "RW" @@ -347,80 +351,87 @@ object (self:'a) let xoffset_r = if isindex then match (offset, isadd) with + (* immediate offset *) | (ARMImmOffset i, true) -> Ok (int_constant_expr i) | (ARMImmOffset i, false) -> Ok (int_constant_expr (-i)) + + (* index offset *) | (ARMIndexOffset (indexreg, indexoffset), true) -> let indexvar = env#mk_arm_register_variable indexreg in Ok (XOp (XPlus, [XVar indexvar; int_constant_expr indexoffset])) + + (* shifted index offset *) | (ARMShiftedIndexOffset (indexreg, srt, indexoffset), true) -> let indexvar = env#mk_arm_register_variable indexreg in let xoffset = int_constant_expr indexoffset in + let factor = CHNumerical.mkNumericalPowerOf2 in (match srt with | ARMImmSRT (_, 0)-> Ok (XOp (XPlus, [XVar indexvar; xoffset])) - | ARMImmSRT (SRType_LSL, 1) -> - let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 2]) in - Ok (XOp (XPlus, [shifted; xoffset])) - | ARMImmSRT (SRType_LSL, 2) -> - let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 4]) in - Ok (XOp (XPlus, [shifted; xoffset])) - | ARMImmSRT (SRType_LSL, 3) -> - let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 8]) in - Ok (XOp (XPlus, [shifted; xoffset])) - | ARMImmSRT (SRType_LSL, 4) -> - let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 16]) in - Ok (XOp (XPlus, [shifted; xoffset])) - | ARMImmSRT (SRType_LSL, 5) -> - let shifted = XOp (XMult, [XVar indexvar; int_constant_expr 32]) in - Ok (XOp (XPlus, [shifted; xoffset])) - | ARMImmSRT (SRType_ASR, 1) -> - let shifted = XOp (XDiv, [XVar indexvar; int_constant_expr 2]) in - Ok (XOp (XPlus, [shifted; xoffset])) - | ARMImmSRT (SRType_ASR, 2) -> - let shifted = XOp (XDiv, [XVar indexvar; int_constant_expr 4]) in - Ok (XOp (XPlus, [shifted; xoffset])) - | ARMImmSRT (SRType_ASR, 3) -> - let shifted = XOp (XDiv, [XVar indexvar; int_constant_expr 8]) in + + (* fixed shift left (multiply) *) + | ARMImmSRT (SRType_LSL, n) when n > 0 && n < 32 -> + let samount = num_constant_expr (factor n) in + let shifted = XOp (XMult, [XVar indexvar; samount]) in Ok (XOp (XPlus, [shifted; xoffset])) - | ARMImmSRT (SRType_ASR, 4) -> - let shifted = XOp (XDiv, [XVar indexvar; int_constant_expr 16]) in + + (* fixed shift right (divide) *) + | ARMImmSRT (SRType_ASR, n) when n > 0 && n < 32 -> + let samount = num_constant_expr (factor n) in + let shifted = XOp (XDiv, [XVar indexvar; samount]) in Ok (XOp (XPlus, [shifted; xoffset])) + + (* variable shift left *) | ARMRegSRT (SRType_LSL, srtreg) -> let shiftvar = env#mk_arm_register_variable srtreg in let shifted = XOp (XLsl, [XVar indexvar; XVar shiftvar]) in Ok (XOp (XPlus, [shifted; xoffset])) + + (* variable shift right *) | ARMRegSRT (SRType_ASR, srtreg) -> let shiftvar = env#mk_arm_register_variable srtreg in let shifted = XOp (XAsr, [XVar indexvar; XVar shiftvar]) in Ok (XOp (XPlus, [shifted; xoffset])) | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + Error [(elocm __LINE__) + ^ (p2s floc#l#toPretty) ^ "; " ^ "register shift: " ^ (register_shift_to_string srt) ^ " not yet supported"]) | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + Error [(elocm __LINE__) + ^ (p2s floc#l#toPretty) ^ "; " ^ "arm memory offset: " ^ (arm_memory_offset_to_string offset) ^ " not yet supported with isadd: " ^ (if isadd then "true" else "false")] else + (* post-indexed: offset is applied in the next iteration *) Ok zero_constant_expr in let rvar = env#mk_arm_register_variable r in let rvarx = if align > 1 then let alignx = int_constant_expr align in - XOp (XMult, [XOp (XDiv, [XVar rvar; alignx]); alignx]) + let result = XOp (XMult, [XOp (XDiv, [XVar rvar; alignx]); alignx]) in + begin + log_diagnostics_result + ~msg:(p2s floc#l#toPretty) + ~tag:"to_address" + __FILE__ __LINE__ + ["apply offset-address alignment adjustment: " ^ (x2s result)]; + result + end else XVar rvar in (* memory addresses are not rewritten to preserve the structure of the data accessed (in case of a non-optimizing compiler) *) TR.tmap - (fun memoff -> simplify_xpr (XOp (XPlus, [rvarx; memoff]))) + (fun xoffset -> simplify_xpr (XOp (XPlus, [rvarx; xoffset]))) xoffset_r | ARMLiteralAddress dw -> Ok (num_constant_expr dw#to_numerical) | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + Error [(elocm __LINE__) + ^ (p2s floc#l#toPretty) ^ "; " ^ "Address for " ^ (p2s self#toPretty) ^ " not yet supported"] @@ -469,12 +480,18 @@ object (self:'a) Ok (env#mk_arm_double_extension_register_variable r1 r2) | ARMSpecialReg r -> Ok (env#mk_arm_special_register_variable r) + + (* Memory address calculated from the PC value and an immediate offset *) | ARMLiteralAddress dw -> TR.tprop (floc#env#mk_global_variable floc#l dw#to_numerical) - (__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (eloc __LINE__) + + (* Generic memory address *) | ARMOffsetAddress (r, align, offset, isadd, _iswback, isindex, size) -> (match offset with + + (* Immediate offset: resolve with get_memory_variable_numoffset *) | ARMImmOffset _ -> let rvar = env#mk_arm_register_variable r in let numoffset_r = @@ -483,80 +500,126 @@ object (self:'a) | (ARMImmOffset i, true) -> Ok (mkNumerical i) | (ARMImmOffset i, false) -> Ok (mkNumerical i)#neg | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + Error [(elocm __LINE__) ^ "Immediate offset not yet implemented for offset " ^ (arm_memory_offset_to_string offset)] else Ok numerical_zero in TR.tbind - ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) - (fun memoff -> - floc#get_memory_variable_numoffset ~size ~align rvar memoff) + ~msg:(eloc __LINE__) + (fun numoffset -> + let tresult = + floc#get_memory_variable_numoffset ~size ~align rvar numoffset in + begin + log_diagnostics_result + ~msg:(p2s floc#l#toPretty) + ~tag:"to_variable:numoffset" + __FILE__ __LINE__ + ["operand: " ^ (p2s self#toPretty); + "tresult: " + ^ (TR.tfold + ~ok:(fun v -> p2s v#toPretty) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end) numoffset_r + (* Index offset: resolve with get_memory_variable_varoffset *) | ARMIndexOffset (ri, i) -> let rvar = env#mk_arm_register_variable r in let ivar = env#mk_arm_register_variable ri in - if isadd then - let rx = floc#inv#rewrite_expr (XVar rvar) in - let ivax = floc#inv#rewrite_expr (XVar ivar) in - let xoffset = simplify_xpr (XOp (XPlus, [rx; ivax])) in - (match (xoffset, i) with - | (XConst (IntConst n), 0) when n#equal CHNumerical.numerical_zero -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Illegal address (zero) for ARMOffsetAddress"] - | (XConst (IntConst n), 0) -> - floc#env#mk_global_variable ~size floc#l n - | _ -> - floc#get_memory_variable_varoffset - ~size rvar ivar (mkNumerical i)) - else - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Index offset with is_add false not yet supported: " - ^ (p2s self#toPretty)] - + let tresult = + if isadd then + let rx = floc#inv#rewrite_expr (XVar rvar) in + let ivax = floc#inv#rewrite_expr (XVar ivar) in + let xoffset = simplify_xpr (XOp (XPlus, [rx; ivax])) in + (match (xoffset, i) with + | (XConst (IntConst n), 0) when n#equal CHNumerical.numerical_zero -> + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "Illegal address (zero) for ARMOffsetAddress"] + | (XConst (IntConst n), 0) -> + floc#env#mk_global_variable ~size floc#l n + | _ -> + floc#get_memory_variable_varoffset + ~size rvar ivar (mkNumerical i)) + else + Error [(elocm __LINE__) + ^ (p2s floc#l#toPretty) ^ "; " + ^ "Index offset with is_add false not yet supported: " + ^ (p2s self#toPretty)] in + begin + log_diagnostics_result + ~msg:(p2s floc#l#toPretty) + ~tag:"to_variable:varoffset" + __FILE__ __LINE__ + ["operand: " ^ (p2s self#toPretty); + "tresult: " + ^ (TR.tfold + ~ok:(fun v -> p2s v#toPretty) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end + + (* Shifted index offset: resolve with get_memory_variable_varoffset or + get_memory_variable_scaledoffset *) | ARMShiftedIndexOffset _ -> let rvar = env#mk_arm_register_variable r in - (match (offset, isadd) with - | (ARMShiftedIndexOffset (ivar, srt, i), true) -> - let optscale = - match srt with - | ARMImmSRT (SRType_LSL, 3) -> Some 8 - | ARMImmSRT (SRType_LSL, 2) -> Some 4 - | ARMImmSRT (SRType_LSL, 0) -> Some 1 - | _ -> None in - (match optscale with - | Some scale -> - let ivar = env#mk_arm_register_variable ivar in - if scale = 1 then - let rx = floc#inv#rewrite_expr (XVar rvar) in - let ivax = floc#inv#rewrite_expr (XVar ivar) in - let xoffset = simplify_xpr (XOp (XPlus, [rx; ivax])) in - (match (xoffset, i) with - | (XConst (IntConst n), 0) -> - floc#env#mk_global_variable ~size floc#l n - | _ -> - floc#get_memory_variable_varoffset - ~size rvar ivar (mkNumerical i)) - else - floc#get_memory_variable_scaledoffset - ~size rvar ivar scale (mkNumerical i) - | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Scaled memory offset with register shift " - ^ (register_shift_to_string srt) - ^ " not yet supported"]) - | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " - ^ "Shifted Index Offset with isadd: false: " - ^ (p2s self#toPretty) - ^ " not yet supported"])) + let tresult = + (match (offset, isadd) with + | (ARMShiftedIndexOffset (ivar, srt, i), true) -> + let optscale = + match srt with + | ARMImmSRT (SRType_LSL, 3) -> Some 8 + | ARMImmSRT (SRType_LSL, 2) -> Some 4 + | ARMImmSRT (SRType_LSL, 0) -> Some 1 + | _ -> None in + (match optscale with + | Some scale -> + let ivar = env#mk_arm_register_variable ivar in + if scale = 1 then + let rx = floc#inv#rewrite_expr (XVar rvar) in + let ivax = floc#inv#rewrite_expr (XVar ivar) in + let xoffset = simplify_xpr (XOp (XPlus, [rx; ivax])) in + (match (xoffset, i) with + | (XConst (IntConst n), 0) -> + floc#env#mk_global_variable ~size floc#l n + | _ -> + floc#get_memory_variable_varoffset + ~size rvar ivar (mkNumerical i)) + else + floc#get_memory_variable_scaledoffset + ~size rvar ivar scale (mkNumerical i) + | _ -> + Error [(elocm __LINE__) + ^ "Scaled memory offset with register shift " + ^ (register_shift_to_string srt) + ^ " not yet supported"]) + | _ -> + Error [(elocm __LINE__) + ^ "Shifted Index Offset with isadd: false: " + ^ (p2s self#toPretty) + ^ " not yet supported"]) in + begin + log_diagnostics_result + ~msg:(p2s self#toPretty) + ~tag:"to_variable:scaledoffset" + __FILE__ __LINE__ + ["operand: " ^ (p2s self#toPretty); + "tresult: " + ^ (TR.tfold + ~ok:(fun v -> p2s v#toPretty) + ~error:(fun e -> "Error: [" ^ (String.concat "; " e) ^ "]") + tresult)]; + tresult + end) | ARMShiftedReg (r, ARMImmSRT (SRType_LSL, 0)) -> Ok (env#mk_arm_register_variable r) | _ -> - Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + Error [(elocm __LINE__) ^ "ARMOffsetAddress: " ^ (p2s self#toPretty) ^ " not yet supported"] diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index d7d5c89a..b98edc28 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -676,7 +676,7 @@ object (self) let xx = rewrite_expr ?restrict:(Some 4) x in let ptype = get_parameter_type p in let xx = - if is_pointer ptype then + if is_pointer ptype (* && (not (is_char_pointer ptype)) *) then let _ = floc#memrecorder#record_argument xx index in match get_string_reference floc xx with | Some _ -> xx diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index caf06b66..79fd99c7 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -63,12 +63,15 @@ open BCHARMTypes module TR = CHTraceResult +let x2p = XprToPretty.xpr_formatter#pr_expr let p2s = CHPrettyUtil.pretty_to_string +let x2s x = p2s (x2p x) -let log_error (tag: string) (msg: string): tracelogspec_t = - mk_tracelog_spec ~tag:("FnARMTypeConstraints:" ^ tag) msg - +(* +let eloc (line: int): string = __FILE__ ^ ":" ^ (string_of_int line) +let elocm (line: int): string = (eloc line) ^ ": " + *) class arm_fn_type_constraints_t (store: type_constraint_store_int) @@ -162,47 +165,43 @@ object (self) let get_variable_rdefs_r (v_r: variable_t traceresult): symbol_t list = TR.tfold_default get_variable_rdefs [] v_r in - (* - let getopt_initial_argument_value (x: xpr_t): (register_t * int) option = - match (rewrite_expr x) with - | XVar v when floc#f#env#is_initial_arm_argument_value v -> - Some (TR.tget_ok (floc#f#env#get_initial_register_value_register v), 0) - | XOp (XPlus, [XVar v; XConst (IntConst n)]) - when floc#f#env#is_initial_arm_argument_value v -> - Some - (TR.tget_ok (floc#f#env#get_initial_register_value_register v), - n#toInt) - | _ -> None in - *) - - (* - let getopt_initial_argument_value_r - (x_r: xpr_t traceresult): (register_t * int) option = - TR.tfold_default getopt_initial_argument_value None x_r in - *) - let getopt_stackaddress (x: xpr_t): int option = match (rewrite_expr x) with | XOp (xop, [XVar v; XConst (IntConst n)]) when floc#f#env#is_initial_register_value v -> let optoffset = match xop with - | XMinus when n#toInt > 0 -> Some n#toInt - | XPlus when n#toInt < 0 -> Some n#neg#toInt + | XMinus when n#toInt > 0 -> Some n#neg#toInt + | XPlus when n#toInt < 0 -> Some n#toInt | _ -> None in - log_tfold - (log_error "getopt_stackaddress" "invalid register") + TR.tfold ~ok:(fun reg -> match (optoffset, reg) with | (Some n, ARMRegister ARSP) -> Some n | _ -> None) - ~error:(fun _ -> None) + ~error:(fun e -> + begin + log_error_result + ~tag:"getopt_stackaddress" + ~msg:("x: " ^ (x2s x)) + __FILE__ __LINE__ e; + None + end) (floc#f#env#get_initial_register_value_register v) | _ -> None in let getopt_stackaddress_r (x_r: xpr_t traceresult): int option = TR.tfold_default getopt_stackaddress None x_r in + let getopt_stacklocation_type (x: xpr_t): btype_t option = + match getopt_stackaddress x with + | Some offset when fndata#has_stackvar_type_annotation offset -> + TR.to_option (fndata#get_stackvar_type_annotation offset) + | _ -> None in + + let getopt_stacklocation_type_r (x_r: xpr_t traceresult): btype_t option = + TR.tfold_default getopt_stacklocation_type None x_r in + let getopt_global_address (x: xpr_t): doubleword_int option = match (rewrite_expr x) with | XConst (IntConst num) -> @@ -827,17 +826,30 @@ object (self) begin (regvar_type_introduction "LDR" rt); - (* loaded type may be known *) - (let xmem_r = memop#to_expr floc in - let xrmem_r = - TR.tmap (fun x -> simplify_xpr (floc#inv#rewrite_expr x)) xmem_r in - let xtype_r = TR.tbind floc#get_xpr_type xrmem_r in - let rule = "LDR-memop-tc" in - TR.titer - ~ok:(fun t -> - let opttc = mk_btype_constraint rttypevar t in + (match getopt_stacklocation_type_r (memop#to_address floc) with + | Some ty -> + let opttc = mk_btype_constraint rttypevar ty in + (match opttc with + | Some tc -> + let rule = "LDR-memop-tc" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc + end + else + log_type_constraint_rule_disabled __LINE__ rule tc + | _ -> ()) + | _ -> ()); + + (let vmem_r = memop#to_variable floc in + let ty_r = TR.tbind floc#get_variable_type vmem_r in + TR.tfold_default + (fun ty -> + let opttc = mk_btype_constraint rttypevar ty in (match opttc with | Some tc -> + let rule = "LDR-memop-tc" in if fndata#is_typing_rule_enabled iaddr rule then begin log_type_constraint __LINE__ rule tc; @@ -846,8 +858,8 @@ object (self) else log_type_constraint_rule_disabled __LINE__ rule tc | _ -> ())) - ~error:(fun e -> log_error_result __FILE__ __LINE__ e) - xtype_r); + () + ty_r); (* LDR rt, [rn, rm] : X_rndef.load <: X_rt *) (let xrdef = get_variable_rdefs_r (rn#to_variable floc) in @@ -1057,13 +1069,13 @@ object (self) end - | LoadRegisterHalfword (_, rt, rn, rm, memop, _) when rm#is_immediate -> + | LoadRegisterHalfword (_, rt, rn, rm, _memop, _) when rm#is_immediate -> let rtreg = rt#to_register in let rttypevar = mk_reglhs_typevar rtreg faddr iaddr in begin (regvar_type_introduction "LDRH" rt); - (* loaded type may be known *) + (* loaded type may be known (let xmem_r = memop#to_expr floc in let xrmem_r = TR.tmap (fun x -> simplify_xpr (floc#inv#rewrite_expr x)) xmem_r in @@ -1084,6 +1096,7 @@ object (self) | _ -> ())) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) xtype_r); + *) (* LDRH rt, ... : X_rt <: integer type *) (let tc = mk_int_type_constant SignedNeutral 16 in @@ -1506,16 +1519,15 @@ object (self) log_subtype_rule_disabled __LINE__ rule rttypeterm rntypeterm ) rtrdefs) rnrdefs); - (* type of destination memory location may be known *) (let vmem_r = memvarop#to_variable floc in - let vtype_r = TR.tbind floc#get_variable_type vmem_r in + let ty_r = TR.tbind floc#get_variable_type vmem_r in let rule = "STR-memop-tc" in TR.titer - ~ok:(fun t -> + ~ok:(fun ty -> List.iter (fun rtdsym -> let rtdloc = rtdsym#getBaseName in let rttypevar = mk_reglhs_typevar rtreg faddr rtdloc in - let opttc = mk_btype_constraint rttypevar t in + let opttc = mk_btype_constraint rttypevar ty in match opttc with | Some tc -> if fndata#is_typing_rule_enabled iaddr rule then @@ -1527,8 +1539,7 @@ object (self) log_type_constraint_rule_disabled __LINE__ rule tc | _ -> ()) rtrdefs) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) - vtype_r) - + ty_r); end | StoreRegisterByte (_, rt, rn, rm, _memvarop, _) when rm#is_immediate -> diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 5d61298c..ebef0d90 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -715,7 +715,7 @@ let translate_arm_instruction List.fold_left (fun (acccmds, accuse, accusehigh) (p, x) -> let ptype = get_parameter_type p in let addressedvars = - if is_pointer ptype then + if is_pointer ptype && (not (is_char_pointer ptype)) then let xx = rewrite_expr floc x in match BCHARMDisassemblyUtils.get_string_reference floc xx with | Some _ -> [] @@ -3224,7 +3224,7 @@ let translate_arm_instruction if floc#has_initial_value vrt then TR.tfold ~ok:(fun memlhs -> - if finfo#env#is_stack_variable memlhs then + if finfo#env#is_local_stack_variable memlhs then finfo#save_register memlhs floc#cia rt#to_register) ~error:(fun e -> begin log_dc_error_result __FILE__ __LINE__ e; () end) diff --git a/CodeHawk/CHB/bchsummaries/so_functions/mktime.xml b/CodeHawk/CHB/bchsummaries/so_functions/mktime.xml index d0146035..57ed813e 100644 --- a/CodeHawk/CHB/bchsummaries/so_functions/mktime.xml +++ b/CodeHawk/CHB/bchsummaries/so_functions/mktime.xml @@ -12,7 +12,7 @@ - tm + ch_tm diff --git a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml index 19eb2570..b8862c51 100644 --- a/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlib_tests/txbchlib/bCHXprUtilTest.ml @@ -46,7 +46,7 @@ let lastupdated = "2024-12-25" let largest_constant_term_test () = - (* let xv = XVar (XG.mk_var "v") in *) + let xv = XVar (XG.mk_var "v") in begin TS.new_testsuite (testname ^ "_largest_constant_term_test") lastupdated; @@ -60,10 +60,55 @@ let largest_constant_term_test () = ~received:(X.largest_constant_term (Xprt.int_constant_expr 0x500000)) ()); + TS.add_simple_test + ~title:"offset" + (fun () -> + let x = XOp (XPlus, [xv; Xprt.int_constant_expr 4]) in + XBA.equal_numerical + ~expected:(mkNumerical 4) + ~received:(X.largest_constant_term x) + ()); + TS.launch_tests() end +let smallest_constant_term_test() = + let xv = XVar (XG.mk_var "v") in + begin + + TS.new_testsuite (testname ^ "_smallest_constant_term_test") lastupdated; + + TS.add_simple_test + ~title:"constant" + (fun () -> + XBA.equal_numerical + ~expected:(mkNumerical 0x500000) + ~received:(X.smallest_constant_term (Xprt.int_constant_expr 0x500000)) + ()); + + TS.add_simple_test + ~title:"negative offset" + (fun () -> + let x = XOp (XMinus, [xv; Xprt.int_constant_expr 4]) in + XBA.equal_numerical + ~expected:(mkNumerical (-4)) + ~received:(X.smallest_constant_term x) + ()); + + TS.add_simple_test + ~title:"positive offset" + (fun () -> + let x = XOp (XPlus, [xv; Xprt.int_constant_expr 4]) in + XBA.equal_numerical + ~expected:(mkNumerical 4) + ~received:(X.smallest_constant_term x) + ()); + + TS.launch_tests () + end + + let array_index_offset_test () = let xv = XVar (XG.mk_var "v") in let xzero = Xprt.int_constant_expr 0 in @@ -213,6 +258,7 @@ let () = begin TS.new_testfile testname lastupdated; largest_constant_term_test (); + smallest_constant_term_test (); array_index_offset_test (); TS.exit_file () end diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml index 3b129f61..4ded135a 100644 --- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml +++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHTranslateARMToCHIFTest.ml @@ -61,6 +61,25 @@ open BCHTranslateARMToCHIF open BCHAnalyzeApp +(* Tools to diagnose failing tests: + + let _ = CHLogger.activate_diagnostics () in + let _ = BCHSystemSettings.system_settings#set_collect_data in + ..... + let _ = + if title = "STM" then + begin + CHPretty.pr_debug [proc#toPretty]; + CHFileIO.file_output#saveFile + "testlog.chlog" CHLogger.chlog#toPretty; + CHFileIO.file_output#saveFile + "testlog.ch_error_log" CHLogger.ch_error_log#toPretty; + CHFileIO.file_output#saveFile + "testlog.ch_diagnostics_log" CHLogger.ch_diagnostics_log#toPretty + end in + *) + + let testname = "bCHTranslateARMToCHIFTest" let lastupdated = "2025-08-20" @@ -108,6 +127,7 @@ let translate_store () = TS.add_simple_test ~title (fun () -> + let _ = BCHSystemSettings.system_settings#set_architecture "arm" in let faddr = make_dw sfaddr in let fn = ARMU.arm_function_setup faddr bytes in let _ = analyze_arm_function faddr fn 0 in