diff --git a/CodeHawk/CHB/bchlib/Makefile b/CodeHawk/CHB/bchlib/Makefile index 35e1c8e0..4b38fc08 100644 --- a/CodeHawk/CHB/bchlib/Makefile +++ b/CodeHawk/CHB/bchlib/Makefile @@ -131,7 +131,6 @@ SOURCES := \ bCHBCDictionary \ bCHBCFunDeclarations \ bCHBCWriteXml \ - bCHBCAttributes \ bCHBCFiles \ bCHBCTypeUtil \ bCHBCTypeXml \ @@ -174,6 +173,7 @@ SOURCES := \ bCHPrecondition \ bCHPostcondition \ bCHSideeffect \ + bCHBCAttributes \ bCHFunctionSemantics \ bCHFunctionSummary \ bCHVariable \ diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml b/CodeHawk/CHB/bchlib/bCHBCAttributes.ml index 24a6c3f7..894a580e 100644 --- a/CodeHawk/CHB/bchlib/bCHBCAttributes.ml +++ b/CodeHawk/CHB/bchlib/bCHBCAttributes.ml @@ -25,79 +25,91 @@ SOFTWARE. ============================================================================= *) -open BCHBCTypes +(* chlib *) +open CHPretty + +(* chutil *) +open CHLogger +(* bchlib *) +open BCHBasicTypes +open BCHBCTypes +open BCHBCTypePretty +open BCHBCTypeUtil +open BCHFtsParameter +open BCHFunctionInterface +open BCHLibTypes -let gcc_attributes_to_precondition_attributes - (attrs: b_attributes_t): precondition_attribute_t list = - List.fold_left (fun acc a -> - match a with - | Attr ("access", params) -> - (match params with - | [ACons ("read_only", []); AInt refindex] -> - (APCReadOnly (refindex, None)) :: acc - | [ACons ("read_only", []); AInt refindex; AInt sizeindex] -> - (APCReadOnly (refindex, Some sizeindex)) :: acc - | [ACons ("write_only", []); AInt refindex] -> - (APCWriteOnly (refindex, None)) :: acc - | [ACons ("write_only", []); AInt refindex; AInt sizeindex] -> - (APCWriteOnly (refindex, Some sizeindex)) :: acc - | [ACons ("read_write", []); AInt refindex] -> - (APCReadWrite (refindex, None)) :: acc - | [ACons ("read_write", []); AInt refindex; AInt sizeindex] -> - (APCReadWrite (refindex, Some sizeindex)) :: acc - | _ -> acc) - | _ -> acc) [] attrs +let convert_b_attributes_to_function_conditions + (name: string) + (fintf: function_interface_t) + (attrs: b_attributes_t): + (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) = + let parameters = get_fts_parameters fintf in + let get_par (n: int) = + try + List.find (fun p -> + match p.apar_index with Some ix -> ix = n | _ -> false) parameters + with + | Not_found -> + raise + (BCH_failure + (LBLOCK [ + STR "No parameter with index "; + INT n; + pretty_print_list (List.map (fun p -> p.apar_name) parameters) + (fun s -> STR s) "[" "," "]"])) in + let get_derefty (par: fts_parameter_t): btype_t = + if is_pointer par.apar_type then + ptr_deref par.apar_type + else + raise + (BCH_failure + (LBLOCK [ + STR "parameter is not a pointer type: "; + fts_parameter_to_pretty par])) in + List.fold_left (fun ((xpre, xside, xpost) as acc) attr -> + match attr with + | Attr (("access" | "chk_access"), params) -> + let (pre, side) = + (match params with + | [ACons ("read_only", []); AInt refindex] -> + let par = get_par refindex in + let ty = get_derefty par in + ([XXBuffer (ty, ArgValue par, RunTimeValue)], []) -let gcc_attributes_to_srcmapinfo - (attrs: b_attributes_t): srcmapinfo_t option = - let optsrcloc = - List.fold_left (fun acc a -> - match acc with - | Some _ -> acc - | _ -> - match a with - | Attr ("chkc_srcloc", params) -> - (match params with - | [AStr filename; AInt linenumber] -> - Some {srcloc_filename=filename; - srcloc_linenumber=linenumber; - srcloc_notes=[]} - | _ -> None) - | _ -> None) None attrs in - match optsrcloc with - | Some srcloc -> - let binloc = - List.fold_left (fun acc a -> - match acc with - | Some _ -> acc - | _ -> - match a with - | Attr ("chkx_binloc", params) -> - (match params with - | [AStr address] -> Some address - | _ -> None) - | _ -> None) None attrs in - Some {srcmap_srcloc = srcloc; srcmap_binloc = binloc} - | _ -> None + | [ACons ("read_only", []); AInt refindex; AInt sizeindex] -> + let rpar = get_par refindex in + let spar = get_par sizeindex in + let ty = get_derefty rpar in + ([XXBuffer (ty, ArgValue rpar, ArgValue spar)], []) + | [ACons (("write_only" | "read_write"), []); AInt refindex] -> + let par = get_par refindex in + let ty = get_derefty par in + ([XXBuffer (ty, ArgValue par, RunTimeValue)], + [XXBlockWrite (ty, ArgValue par, RunTimeValue)]) + | [ACons (("write_only" | "read_write"), []); + AInt refindex; AInt sizeindex] -> + let rpar = get_par refindex in + let spar = get_par sizeindex in + let ty = get_derefty rpar in + ([XXBuffer (ty, ArgValue rpar, ArgValue spar)], + [XXBlockWrite (ty, ArgValue rpar, ArgValue spar)]) -let precondition_attributes_t_to_gcc_attributes - (preattrs: precondition_attribute_t list): b_attributes_t = - let get_params (refindex: int) (optsizeindex: int option) = - match optsizeindex with - | Some sizeindex -> [AInt refindex; AInt sizeindex] - | _ -> [AInt refindex] in - let get_access (mode: string) (params: b_attrparam_t list) = - Attr ("access", [ACons (mode, [])] @ params) in - List.fold_left (fun acc p -> - match p with - | APCReadOnly (refindex, optsizeindex) -> - (get_access "read_only" (get_params refindex optsizeindex)) :: acc - | APCWriteOnly (refindex, optsizeindex) -> - (get_access "write_only" (get_params refindex optsizeindex)) :: acc - | APCReadWrite (refindex, optsizeindex) -> - (get_access "read_write" (get_params refindex optsizeindex)) :: acc - | _ -> acc) [] preattrs + | _ -> + begin + log_error_result + ~msg:("attribute conversion for " ^ name ^ ": " + ^ "attribute parameters " + ^ (String.concat + ", " (List.map b_attrparam_to_string params))) + ~tag:"attribute conversion" + __FILE__ __LINE__ []; + ([], []) + end) in + (pre @ xpre, side @ xside, xpost) + | _ -> + acc) ([], [], []) attrs diff --git a/CodeHawk/CHB/bchlib/bCHBCAttributes.mli b/CodeHawk/CHB/bchlib/bCHBCAttributes.mli index c8e94a5b..c55e5833 100644 --- a/CodeHawk/CHB/bchlib/bCHBCAttributes.mli +++ b/CodeHawk/CHB/bchlib/bCHBCAttributes.mli @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024 Aarno Labs LLC + Copyright (c) 2024-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 @@ -26,14 +26,64 @@ ============================================================================= *) open BCHBCTypes +open BCHLibTypes -val gcc_attributes_to_precondition_attributes: - b_attributes_t -> precondition_attribute_t list +(** {1 Function attributes} *) -val gcc_attributes_to_srcmapinfo: - b_attributes_t -> srcmapinfo_t option +(** Function declarations in C can be decorated with attributes. These attributes + are generally used to allow certain compiler optimizations + (https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). Here + we use them to communicate preconditions about dynamically linked library + functions. + For many standard libc library functions the analyzer has comprehensive + collection of (hand-made) function summaries that include pre- and + postconditions, side effects, etc, represented in xml. + However, binaries may of course be dynamically linked to a wide variety of + other libraries, for which it is not directly feasible to create these + summaries (e.g., because suitable binaries are not available for analysis). + One possibility is for the user to manually create the xml function summaries + for all functions of interest. A more user-friendly means of providing + similar information is through function prototypes decorated with suitable + attributes, as described here. -val precondition_attributes_t_to_gcc_attributes: - precondition_attribute_t list -> b_attributes_t + We use the same syntax as presented in + (https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). + Currently the following attributes are supported: + + {[ + (access (access-mode, ref-index)) + (access (access-mode, ref-index, size-index)) + (nonnull (ref-indices)) + ]} + + Access modes supported are [read_only], [read_write], and [write_only]; the + [ref-index] is an integer denoting the (1-based) index of the pointer + argument being accessed, and [size-index] is an integer denoting the + (1-based) index of an argument that provides a maximum size (in bytes) + for the memory region accessed. + + As an example, for [memcpy] this would be decorated as: + + {[ + __attribute__ ((access (read_only, 2, 3)), + (access (write_only, 1, 3)), (nonnull (1, 2))) + void* memcpy (void *dst, const void *src, size_t len); + ]} + + (Note that the analyzer has a comprehensive function summary for memcpy, so + it is only shown here as an example, because of its familiar semantics.) + + A prototype thus decorated will automatically generate a function interface + with the function semantics that include the corresponding preconditions + (and, in case of write_only, the corresponding side effect) for the given + library function, resulting in the appropriate proof obligations at their + call sites. + *) + +val convert_b_attributes_to_function_conditions: + string + -> function_interface_t + -> b_attributes_t + -> (xxpredicate_t list * xxpredicate_t list * xxpredicate_t list) diff --git a/CodeHawk/CHB/bchlib/bCHBCFiles.ml b/CodeHawk/CHB/bchlib/bCHBCFiles.ml index 8a333a90..7173c2ab 100644 --- a/CodeHawk/CHB/bchlib/bCHBCFiles.ml +++ b/CodeHawk/CHB/bchlib/bCHBCFiles.ml @@ -47,6 +47,40 @@ module H = Hashtbl let bcd = BCHBCDictionary.bcdictionary +let gcc_attributes_to_srcmapinfo + (attrs: b_attributes_t): srcmapinfo_t option = + let optsrcloc = + List.fold_left (fun acc a -> + match acc with + | Some _ -> acc + | _ -> + match a with + | Attr ("chkc_srcloc", params) -> + (match params with + | [AStr filename; AInt linenumber] -> + Some {srcloc_filename=filename; + srcloc_linenumber=linenumber; + srcloc_notes=[]} + | _ -> None) + | _ -> None) None attrs in + match optsrcloc with + | Some srcloc -> + let binloc = + List.fold_left (fun acc a -> + match acc with + | Some _ -> acc + | _ -> + match a with + | Attr ("chkx_binloc", params) -> + (match params with + | [AStr address] -> Some address + | _ -> None) + | _ -> None) None attrs in + Some {srcmap_srcloc = srcloc; srcmap_binloc = binloc} + | _ -> None + + + class bcfiles_t: bcfiles_int = object (self) @@ -75,7 +109,7 @@ object (self) let i = bcd#index_location in let add_srcmapinfo (vinfo: bvarinfo_t) = - match BCHBCAttributes.gcc_attributes_to_srcmapinfo vinfo.bvattr with + match gcc_attributes_to_srcmapinfo vinfo.bvattr with | Some srcmap -> let vix = bcd#index_varinfo vinfo in if H.mem vinfo_srcmap vix then diff --git a/CodeHawk/CHB/bchlib/bCHBCTypePretty.ml b/CodeHawk/CHB/bchlib/bCHBCTypePretty.ml index 7a58aaed..1e114684 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypePretty.ml +++ b/CodeHawk/CHB/bchlib/bCHBCTypePretty.ml @@ -165,15 +165,87 @@ let constant_to_string (c: bconstant_t) = | _ -> cil_constant_to_string c -let attributes_to_string attrs = +let rec attributes_to_string (attrs: b_attributes_t) = match attrs with | [] -> "" - | l -> + | _ -> (String.concat - "," (List.map (fun attr -> match attr with Attr (s, _) -> s) l)) ^ " " + "\n" + (List.map + (fun attr -> + match attr with + | Attr (s, params) -> + "__attribute__((__" ^ s ^ "__," + ^ (String.concat + ", " + (List.map b_attrparam_to_string params)) + ^ "__))") attrs)) + +and b_attrparam_to_string (param: b_attrparam_t) = + match param with + | AInt i -> string_of_int i + | AStr s -> s + | ACons (s, []) -> "__" ^ s ^ "__" + | ACons (s, params) -> + "__" + ^ s + ^ "__(" + ^ (String.concat ", " (List.map b_attrparam_to_string params)) ^ ")" + | ASizeOf t -> "__sizeof__(" ^ (typ_to_string t) ^ ")" + | ASizeOfE p -> "__sizeofE__(" ^ (b_attrparam_to_string p) ^ ")" + | ASizeOfS ts -> "__sizeofS__(" ^ (btypsig_to_string ts) ^ ")" + | AAlignOf t -> "__alignof__(" ^ (typ_to_string t) ^ ")" + | AAlignOfE p -> "__alignofE__(" ^ (b_attrparam_to_string p) ^ ")" + | AAlignOfS ts -> "__alignofS__(" ^ (btypsig_to_string ts) ^ ")" + | AUnOp (unop, p) -> + (unop_to_print_string unop) ^ " " ^ (b_attrparam_to_string p) + | ABinOp (binop, p1, p2) -> + (b_attrparam_to_string p1) + ^ " " + ^ (binop_to_print_string binop) + ^ " " + ^ (b_attrparam_to_string p2) + | ADot (p, s) -> (b_attrparam_to_string p) ^ "." ^ s + | AStar p -> "*" ^ (b_attrparam_to_string p) + | AAddrOf p -> "&" ^ (b_attrparam_to_string p) + | AIndex (p1, p2) -> + (b_attrparam_to_string p1) ^ "[" ^ (b_attrparam_to_string p2) ^ "]" + | AQuestion (p1, p2, p3) -> + (b_attrparam_to_string p1) + ^ " ? " + ^ (b_attrparam_to_string p2) + ^ " : " + ^ (b_attrparam_to_string p3) + | AAssign (p1, p2) -> + (b_attrparam_to_string p1) ^ " = " ^ (b_attrparam_to_string p2) + + +and btypsig_to_string (ts: btypsig_t) = + let s_attrs (attrs: b_attributes_t) = + match attrs with + | [] -> "" + | _ -> " " ^ (attributes_to_string attrs) in + match ts with + | TSArray (tts, Some i64, attrs) -> + (btypsig_to_string tts) ^ "[" ^ (Int64.to_string i64) ^ "]" ^ (s_attrs attrs) + | TSArray (tts, None, attrs) -> + (btypsig_to_string tts) ^ "[]" ^ (s_attrs attrs) + | TSPtr (tts, attrs) -> + "( " ^ (btypsig_to_string tts) ^ " *)" ^ (s_attrs attrs) + | TSComp (is_struct, name, attrs) -> + (if is_struct then "struct " else "union ") ^ name ^ (s_attrs attrs) + | TSFun (rts, Some tslist, _is_vararg, attrs) -> + (btypsig_to_string rts) + ^ " (" + ^ (String.concat ", " (List.map btypsig_to_string tslist)) + ^ (s_attrs attrs) + | TSFun (rts, None, _is_vararg, attrs) -> + (btypsig_to_string rts) ^ "(?)" ^ (s_attrs attrs) + | TSEnum (name, attrs) -> "enum " ^ name ^ (s_attrs attrs) + | TSBase t -> typ_to_string t -let rec typ_to_string (t: btype_t) = +and typ_to_string (t: btype_t) = let ns_to_string ns = String.concat "" (List.map (fun n -> (tname_to_string n) ^ "::") ns) in let a = attributes_to_string in diff --git a/CodeHawk/CHB/bchlib/bCHBCTypePretty.mli b/CodeHawk/CHB/bchlib/bCHBCTypePretty.mli index 5fd62d40..3759d7a2 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypePretty.mli +++ b/CodeHawk/CHB/bchlib/bCHBCTypePretty.mli @@ -36,6 +36,8 @@ open BCHBCTypes val attributes_to_string: b_attributes_t -> string +val b_attrparam_to_string: b_attrparam_t -> string + val location_line_to_string: b_location_t -> string val storage_to_string: bstorage_t -> string diff --git a/CodeHawk/CHB/bchlib/bCHBCTypes.mli b/CodeHawk/CHB/bchlib/bCHBCTypes.mli index f6361466..b82b7654 100644 --- a/CodeHawk/CHB/bchlib/bCHBCTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHBCTypes.mli @@ -120,67 +120,7 @@ type type_transformer_t = string -> string (** {1 Types and attributes} *) -(** {2 Precondition attributes} - - Function declarations in C can be decorated with attributes. These attributes - are generally used to allow certain compiler optimizations - (https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). Here - we use them to communicate preconditions about dynamically linked library - functions. - - For many standard libc library functions the analyzer has comprehensive - collection of (hand-made) function summaries that include pre- and - postconditions, side effects, etc, represented in xml. - However, binaries may of course be dynamically linked to a wide variety of - other libraries, for which it is not directly feasible to create these - summaries (e.g., because suitable binaries are not available for analysis). - One possibility is for the user to manually create the xml function summaries - for all functions of interest. A more user-friendly means of providing - similar information is through function prototypes decorated with suitable - attributes, as described here. - - We use the same syntax as presented in - (https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html). - Currently the following attributes are supported: - - {[ - (access (access-mode, ref-index)) - (access (access-mode, ref-index, size-index)) - (nonnull (ref-indices)) - ]} - - Access modes supported are [read_only], [read_write], and [write_only]; the - [ref-index] is an integer denoting the (1-based) index of the pointer - argument being accessed, and [size-index] is an integer denoting the - (1-based) index of an argument that provides a maximum size (in bytes) - for the memory region accessed. - - As an example, for [memcpy] this would be decorated as: - - {[ - __attribute__ ((access (read_only, 2, 3)), - (access (write_only, 1, 3)), (nonnull (1, 2))) - void* memcpy (void *dst, const void *src, size_t len); - ]} - - (Note that the analyzer has a comprehensive function summary for memcpy, so - it is only shown here as an example, because of its familiar semantics.) - - A prototype thus decorated will automatically generate a function interface - with the function semantics that include the corresponding preconditions - (and, in case of write_only, the corresponding side effect) for the given - library function, resulting in the appropriate proof obligations at their - call sites. - *) - -type precondition_attribute_t = - | APCReadOnly of int * int option (* ref-index, size-index, both 1-based *) - | APCWriteOnly of int * int option (* ref-index, size-index, (both 1-based) *) - | APCReadWrite of int * int option (* ref-index, size-index, (both 1-based) *) - | APCNull of int list (* parameter indices, 1-based *) - - -and btype_t = +type btype_t = | TVoid of b_attributes_t | TInt of ikind_t * b_attributes_t | TFloat of fkind_t * frepresentation_t * b_attributes_t diff --git a/CodeHawk/CHB/bchlib/bCHCPURegisters.ml b/CodeHawk/CHB/bchlib/bCHCPURegisters.ml index b4848b09..e1305df6 100644 --- a/CodeHawk/CHB/bchlib/bCHCPURegisters.ml +++ b/CodeHawk/CHB/bchlib/bCHCPURegisters.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -864,3 +864,10 @@ let index_to_byte_register (index:int) = | 6 -> Dh | 7 -> Bh | _ -> raise (Invalid_argument ("index_to_byte_register with " ^ (string_of_int index))) + + +let is_temporary_register (reg: register_t): bool = + match reg with + | ARMRegister r -> List.mem r arm_temporaries + | MIPSRegister r -> List.mem r mips_temporaries + | _ -> false diff --git a/CodeHawk/CHB/bchlib/bCHCPURegisters.mli b/CodeHawk/CHB/bchlib/bCHCPURegisters.mli index a2aa07a0..c205c72c 100644 --- a/CodeHawk/CHB/bchlib/bCHCPURegisters.mli +++ b/CodeHawk/CHB/bchlib/bCHCPURegisters.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -156,6 +156,9 @@ val is_stackpointer_register: register_t -> bool val is_register: string -> bool +val is_temporary_register: register_t -> bool + + (** {2 x86}*) val byte_reg_of_reg : cpureg_t -> cpureg_t (* raises Invalid_argument *) diff --git a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml index fb674b29..c4347122 100644 --- a/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHCallSemanticsRecorder.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - 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 @@ -252,14 +252,27 @@ object (self) self#add_po xpo status method private record_blockreads (pre: xxpredicate_t) = + let _ = + ch_diagnostics_log#add + "record blockread" + (LBLOCK [loc#toPretty; STR ": "; + xxpredicate_to_pretty pre]) in let xpo = xxp_to_xpo_predicate self#termev self#loc pre in match xpo with | XPOBuffer (ty, addr, size) -> (match self#termev#xpr_local_stack_address addr with | Some offset -> + let _ = + ch_diagnostics_log#add + "record blockread" + (LBLOCK [loc#toPretty; STR ": "; + STR "offset: "; + INT offset]) in let csize = match size with - | XConst (IntConst n) -> Some n#toInt | _ -> None in + | XConst (IntConst n) -> Some n#toInt + | _ -> + TR.tfold_default (fun s -> Some s) None (size_of_btype ty) in self#finfo#stackframe#add_block_read ~offset:(-offset) ~size:csize ~typ:(Some ty) self#loc#ci | _ -> ()) @@ -284,12 +297,15 @@ object (self) XPOBlockWrite (ty, addr, size)) -> (match self#termev#xpr_local_stack_address addr with | Some offset -> + let numoffset = (CHNumerical.mkNumerical offset)#neg in let csize = match size with - | XConst (IntConst n) -> Some n#toInt | _ -> None in + | XConst (IntConst n) -> Some n#toInt + | _ -> + TR.tfold_default (fun s -> Some s) None (size_of_btype ty) in let sevalue = - self#finfo#env#mk_side_effect_value - self#loc#ci (bterm_to_string taddr) in + self#finfo#env#mk_stack_sideeffect_value + ~btype:(Some ty) self#loc#ci numoffset (bterm_to_string taddr) in self#finfo#stackframe#add_block_write ~offset:(-offset) ~size:csize diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index c11a85e1..070d4cbf 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -228,6 +228,22 @@ object (self) end +class default_bterm_evaluator_t + (finfo: function_info_int) + (_callargs: (fts_parameter_t * xpr_t) list): bterm_evaluator_int = +object + + method finfo = finfo + method bterm_xpr (_t: bterm_t) = None + method xpr_local_stack_address (_x: xpr_t) = None + method bterm_stack_address (_t: bterm_t) = None + method constant_bterm (_t: bterm_t) = None + +end + +let default_bterm_evaluator = new default_bterm_evaluator_t + + class arm_bterm_evaluator_t (finfo: function_info_int) (callargs: (fts_parameter_t * xpr_t) list): bterm_evaluator_int = @@ -664,6 +680,20 @@ object (self) self#env#mk_global_variable (get_total_constant_offset memoff)) memoffset_r + else if memref#is_stack_reference then + TR.tbind + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": memref:stack") + (fun memoff -> + TR.tbind + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (fun numoff -> + 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)) + (get_total_constant_offset memoff)) + memoffset_r else TR.tmap ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) @@ -1258,7 +1288,7 @@ object (self) self#f#env#mk_offset_memory_variable memref memoff) memref_r memoff_r - method private get_variable_type (v: variable_t): btype_t traceresult = + 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 @@ -2395,7 +2425,7 @@ object (self) let _ = List.iter (fun v -> self#f#add_use_high_loc v iaddr) usehigh in useops @ usehighops @ defops @ clobberops @ flagdefops - method private evaluate_fts_argument (p: fts_parameter_t) = + method private evaluate_fts_argument (p: fts_parameter_t): xpr_t = match p.apar_location with | [StackParameter (offset, _)] -> let index = offset / 4 in @@ -2420,7 +2450,7 @@ object (self) self#rewrite_variable_to_external argvar) | _ -> random_constant_expr - method evaluate_summary_term (t:bterm_t) (returnvar:variable_t) = + method evaluate_summary_term (t:bterm_t) (returnvar:variable_t): xpr_t = match t with | ArgValue p -> self#evaluate_fts_argument p | ReturnValue _ -> XVar returnvar @@ -2433,15 +2463,46 @@ object (self) XOp (arithmetic_op_to_xop op, [xpr1; xpr2]) | _ -> random_constant_expr - method private evaluate_fts_address_argument (p: fts_parameter_t) = - let _ = - chlog#add - "evaluate-fts-address-argument: failure" - (LBLOCK [ - STR self#cia; - STR ": "; - fts_parameter_to_pretty p]) in - None + method private evaluate_fts_address_argument + (p: fts_parameter_t):variable_t option = + match p.apar_location with + | [RegisterParameter (r, _)] -> + let argvar = self#env#mk_register_variable r in + let xpr = self#rewrite_variable_to_external argvar in + (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 + + | _ -> + 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) + | _ -> + let _ = + chlog#add + "evaluate-fts-address-argument: failure" + (LBLOCK [ + STR self#cia; + STR ": "; + fts_parameter_to_pretty p]) in + None method evaluate_summary_address_term (t:bterm_t) = match t with @@ -2680,12 +2741,14 @@ object (self) end | _ -> () - method private get_sideeffect_assign (side_effect: xxpredicate_t) = + method private get_sideeffect_assign + (termev: bterm_evaluator_int) (side_effect: xxpredicate_t) = let msg = LBLOCK [ self#l#toPretty; STR ": "; xxpredicate_to_pretty side_effect] in - match side_effect with - | XXBlockWrite (ty, dest, size) -> + let xpo = BCHXPOPredicate.xxp_to_xpo_predicate termev self#l side_effect in + match (side_effect, xpo) with + | (XXBlockWrite (_, dest, size), XPOBlockWrite (ty, adest, _)) -> let get_index_size k = match get_size_of_type ty with | Ok s -> num_constant_expr (k#mult (mkNumerical s)) @@ -2716,17 +2779,26 @@ object (self) let rhs = match dest with | NumConstant n -> - log_tfold_default - (mk_tracelog_spec - ~tag:"get_sideeffect_assign:BlockWrite" - (self#cia ^ ": constant: " ^ n#toString)) - (fun dw -> - let argDescr = dw#to_hex_string in - self#env#mk_side_effect_value self#cia ~global:true argDescr) - (self#env#mk_side_effect_value self#cia (bterm_to_string dest)) + TR.tfold + ~ok:(fun dw -> + self#env#mk_global_sideeffect_value self#cia dw "dest") + ~error:(fun e -> + begin + log_error_result + ~msg:(p2s (xxpredicate_to_pretty side_effect)) + ~tag:"get_sideeffect_assign" + __FILE__ __LINE__ e; + self#env#mk_side_effect_value self#cia "dest" + end) (numerical_to_doubleword n) | _ -> - self#env#mk_side_effect_value self#cia (bterm_to_string dest) in + (match termev#xpr_local_stack_address adest with + | Some offset -> + let numoffset = (CHNumerical.mkNumerical offset)#neg in + self#env#mk_stack_sideeffect_value + ~btype:(Some ty) self#cia numoffset (bterm_to_string dest) + | _ -> + self#env#mk_side_effect_value self#cia (bterm_to_string dest)) in let seAssign = let _ = chlog#add @@ -2743,12 +2815,15 @@ object (self) let fldAssigns = [] in seAssign @ fldAssigns | _ -> - begin - chlog#add "side-effect ignored" msg; - [] + begin + log_error_result + ~msg:(p2s msg) + ~tag:"side-effect ignored" + __FILE__ __LINE__ []; + [] end end - | XXStartsThread (sa, _pars) -> + | (XXStartsThread (sa, _pars), _) -> let _ = match self#evaluate_summary_term sa self#env#mk_num_temp with | XConst (IntConst n) -> @@ -2763,16 +2838,20 @@ object (self) | _ -> () in [] | _ -> - begin - chlog#add "side-effect ignored" msg; - [] - end + begin + log_error_result + ~msg:(p2s msg) + ~tag:"side-effect ignored" + __FILE__ __LINE__ []; + [] + end method private record_precondition_effects (sem:function_semantics_t) = List.iter self#record_precondition_effect sem.fsem_pre - method get_sideeffect_assigns (sem:function_semantics_t) = - List.concat (List.map self#get_sideeffect_assign sem.fsem_sideeffects) + method get_sideeffect_assigns + (termev: bterm_evaluator_int) (sem:function_semantics_t) = + List.concat (List.map (self#get_sideeffect_assign termev) sem.fsem_sideeffects) (* Records reads of global memory *) method private record_memory_reads (pres:xxpredicate_t list) = @@ -2842,7 +2921,8 @@ object (self) (* ------------------------------------------------- assign side effects *) let sideEffectAssigns = - self#get_sideeffect_assigns self#get_call_target#get_semantics in + let termev = default_bterm_evaluator self#f [] in + self#get_sideeffect_assigns termev self#get_call_target#get_semantics in let _ = self#record_precondition_effects self#get_call_target#get_semantics in @@ -2978,7 +3058,7 @@ object (self) List.filter self#env#is_global_variable self#env#get_variables in [ABSTRACT_VARS globals] in let sideeffect_assigns = - self#get_sideeffect_assigns self#get_call_target#get_semantics in + self#get_sideeffect_assigns termev self#get_call_target#get_semantics in let _ = self#record_memory_reads self#get_call_target#get_semantics.fsem_pre in let defClobbered = List.map (fun r -> (ARMRegister r)) arm_temporaries in diff --git a/CodeHawk/CHB/bchlib/bCHFloc.mli b/CodeHawk/CHB/bchlib/bCHFloc.mli index 0f3305d9..3114ee9e 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.mli +++ b/CodeHawk/CHB/bchlib/bCHFloc.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2022-2023 Aarno Labs LLC + Copyright (c) 2022-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 @@ -27,6 +27,9 @@ SOFTWARE. ============================================================================= *) +(* xprlib *) +open XprTypes + (* bchlib *) open BCHLibTypes @@ -60,3 +63,5 @@ val get_i_floc: -> floc_int +val default_bterm_evaluator: + function_info_int -> (fts_parameter_t * xpr_t) list -> bterm_evaluator_int diff --git a/CodeHawk/CHB/bchlib/bCHFunctionData.ml b/CodeHawk/CHB/bchlib/bCHFunctionData.ml index ba771042..7fd01d6c 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionData.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionData.ml @@ -280,31 +280,39 @@ object (self) __FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "No stackvar annotation found at offset " ^ (string_of_int offset)] - method is_typing_rule_enabled (loc: string) (name: string): bool = + method is_typing_rule_enabled ?(rdef=None) (loc: string) (name: string): bool = + let rdefloc = + match rdef with + | None -> loc + | Some rdefaddr -> loc ^ ":" ^ rdefaddr in match self#get_function_annotation with - | None -> false + | None -> BCHSystemSettings.system_settings#is_typing_rule_enabled name | Some a -> - List.fold_left - (fun acc tra -> - acc || - (if tra.tra_action = "enable" && tra.tra_name = name then - (List.mem "all" tra.tra_locations) - || (List.mem loc tra.tra_locations) - else - false)) false a.typingrules - - method is_typing_rule_disabled (loc: string) (name: string): bool = - match self#get_function_annotation with - | None -> false - | Some a -> - List.fold_left - (fun acc tra -> - acc || - (if tra.tra_action = "disable" && tra.tra_name = name then - (List.mem "all" tra.tra_locations) - || (List.mem loc tra.tra_locations) - else - false)) false a.typingrules + let is_user_enabled () = + List.fold_left + (fun acc tra -> + acc || + (if tra.tra_action = "enable" && tra.tra_name = name then + (List.mem "all" tra.tra_locations) + || (List.mem loc tra.tra_locations) + else + false)) false a.typingrules in + let is_user_disabled () = + List.fold_left + (fun acc tra -> + acc || + (if tra.tra_action = "disable" && tra.tra_name = name then + (List.mem "all" tra.tra_locations) + || (List.mem loc tra.tra_locations) + || (List.mem rdefloc tra.tra_locations) + else + false)) false a.typingrules in + if is_user_enabled () then + true + else if is_user_disabled () then + false + else + BCHSystemSettings.system_settings#is_typing_rule_enabled name method add_inlined_block (baddr:doubleword_int) = inlined_blocks <- baddr :: inlined_blocks diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml index 7c88532e..2a1ebb01 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml @@ -128,36 +128,6 @@ let po_anchor_to_pretty a = | IndirectAccess n -> LBLOCK [ STR "indirect ( " ; bterm_to_pretty n ; STR " )" ] -class type saved_register_int = -object ('a) - - method compare : 'a -> int - - method set_save_address : ctxt_iaddress_t -> unit - method add_restore_address : ctxt_iaddress_t -> unit - - method get_register : register_t - method get_save_address : ctxt_iaddress_t - method get_restore_addresses: ctxt_iaddress_t list - - method has_save_address : bool - method has_restore_addresses: bool - - method is_save_or_restore_address: ctxt_iaddress_t -> bool - - method write_xml: xml_element_int -> unit - method toPretty: pretty_t -end - - -module SavedRegistersCollections = CHCollections.Make - (struct - type t = saved_register_int - let compare r1 r2 = r1#compare r2 - let toPretty r = r#toPretty - end) - - let pr_expr = xpr_formatter#pr_expr @@ -907,6 +877,31 @@ 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 svar = + self#mk_variable + (self#varmgr#make_local_stack_variable + ~offset:memoffset (mkNumerical stackslot#offset)) in + let name = stackslot#name ^ (memory_offset_to_string memoffset) 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_register_variable (register:register_t) = self#mk_variable (varmgr#make_register_variable register) @@ -999,8 +994,22 @@ object (self) method mk_calltarget_value (tgt:call_target_t) = self#mk_variable (varmgr#make_calltarget_value tgt) - method mk_side_effect_value (iaddr:ctxt_iaddress_t) ?(global=false) (arg:string) = - self#mk_variable (varmgr#make_side_effect_value iaddr ~global arg) + method mk_global_sideeffect_value + ?(btype=None) + (iaddr: ctxt_iaddress_t) + (gaddr: doubleword_int) + (arg: string) = + self#mk_variable (varmgr#make_global_sideeffect_value ~btype iaddr arg gaddr) + + method mk_stack_sideeffect_value + ?(btype=None) + (iaddr: ctxt_iaddress_t) + (offset: numerical_t) + (arg: string) = + self#mk_variable (varmgr#make_stack_sideeffect_value ~btype iaddr arg offset) + + method mk_side_effect_value (iaddr:ctxt_iaddress_t) (arg:string) = + self#mk_variable (varmgr#make_side_effect_value iaddr "sev" arg) method mk_field_value (sname:string) (offset:int) (fname:string) = self#mk_variable (varmgr#make_field_value sname offset fname) @@ -1603,6 +1612,7 @@ end class function_info_t (faddr: doubleword_int) + (fndata: function_data_int) (varmgr: variable_manager_int) (invio: invariant_io_int) (varinvio: var_invariant_io_int):function_info_int = @@ -1650,7 +1660,7 @@ object (self) val mutable call_targets_set = false val nonreturning_calls = new StringCollections.set_t val mutable invariants_to_be_reset = false - val stackframe = mk_function_stackframe varmgr + val stackframe = mk_function_stackframe fndata varmgr val proofobligations = mk_proofobligations faddr (mk_xpodictionary varmgr#vard#xd) @@ -1809,34 +1819,37 @@ object (self) * ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *) method save_register - (vmem: variable_t) (iaddr:ctxt_iaddress_t) (reg:register_t) = - if self#env#is_stack_variable vmem then - TR.tfold - ~ok:(fun offset -> - match offset with - | ConstantOffset (n, NoOffset) -> - self#stackframe#add_register_spill ~offset:n#toInt reg iaddr - | _ -> - log_error_result - ~msg:"save_register:not a constant offset" - __FILE__ __LINE__ - ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): "; - (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg) - ^ " and offset " ^ (memory_offset_to_string offset)]) - ~error:(fun e -> - log_error_result - ~msg:"save_register" - __FILE__ __LINE__ - (["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): "; - (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] @ e)) - (self#env#get_memvar_offset vmem) + (vmem: variable_t) (iaddr: ctxt_iaddress_t) (reg: register_t) = + if BCHCPURegisters.is_temporary_register reg then + () else - log_error_result - ~msg:"save register:not a stack variable" - __FILE__ __LINE__ - ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): "; - "not a stack variable: " - ^ (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] + if self#env#is_stack_variable vmem then + TR.tfold + ~ok:(fun offset -> + match offset with + | ConstantOffset (n, NoOffset) -> + self#stackframe#add_register_spill ~offset:n#toInt reg iaddr + | _ -> + log_error_result + ~msg:"save_register:not a constant offset" + __FILE__ __LINE__ + ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): "; + (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg) + ^ " and offset " ^ (memory_offset_to_string offset)]) + ~error:(fun e -> + log_error_result + ~msg:"save_register" + __FILE__ __LINE__ + (["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): "; + (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] @ e)) + (self#env#get_memvar_offset vmem) + else + log_error_result + ~msg:"save register:not a stack variable" + __FILE__ __LINE__ + ["(" ^ (p2s self#get_address#toPretty) ^ "," ^ iaddr ^ "): "; + "not a stack variable: " + ^ (p2s vmem#toPretty) ^ " with " ^ (register_to_string reg)] method restore_register (memaddr: xpr_t) (iaddr:ctxt_iaddress_t) (reg:register_t) = @@ -2610,7 +2623,8 @@ let load_function_info ?(reload=false) (faddr:doubleword_int) = let varmgr = make_variable_manager faddr xvard in let invio = read_invs fname varmgr#vard in let varinvio = read_varinvs fname varmgr#vard in - let finfo = new function_info_t faddr varmgr invio varinvio in + let fndata = functions_data#get_function faddr in + let finfo = new function_info_t faddr fndata varmgr invio varinvio in let _ = match extract_function_info_file fname with | Some node -> finfo#read_xml node diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml index da07569e..ea8389eb 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -35,7 +35,6 @@ open CHLogger open CHXmlDocument (* bchlib *) -open BCHBasicTypes open BCHBCAttributes open BCHBCTypePretty open BCHBCTypes @@ -319,12 +318,8 @@ let default_function_semantics = { let bvarinfo_to_function_semantics (vinfo: bvarinfo_t) (fintf: function_interface_t): function_semantics_t = if (List.length vinfo.bvattr) > 0 then - let preconditions = - let preattrs = gcc_attributes_to_precondition_attributes vinfo.bvattr in - make_attribute_preconditions preattrs (get_fts_parameters fintf) in - let sideeffects = - let sideattrs = gcc_attributes_to_precondition_attributes vinfo.bvattr in - make_attribute_sideeffects sideattrs (get_fts_parameters fintf) in + let (preconditions, sideeffects, _) = + convert_b_attributes_to_function_conditions vinfo.bvname fintf vinfo.bvattr in let _ = chlog#add "bvarinfo attributes" @@ -332,32 +327,14 @@ let bvarinfo_to_function_semantics STR vinfo.bvname; STR ": "; STR (attributes_to_string vinfo.bvattr)]) in - {default_function_semantics with - fsem_pre = preconditions; fsem_sideeffects = sideeffects} + let fsem = + {default_function_semantics with + fsem_pre = preconditions; fsem_sideeffects = sideeffects} in + let _ = + ch_diagnostics_log#add + "function semantics" + (LBLOCK [STR vinfo.bvname; STR ": "; + function_semantics_to_pretty fsem]) in + fsem else default_function_semantics - - -let function_semantics_to_precondition_attributes - (sem: function_semantics_t): precondition_attribute_t list = - let has_index (p: fts_parameter_t) = - match p.apar_index with Some _ -> true | _ -> false in - let get_index (p: fts_parameter_t) = - match p.apar_index with - | Some index -> index - | _ -> - raise - (BCH_failure - (LBLOCK [ - STR "Error in function_semantics_to_precondition_attributes"])) in - List.fold_left (fun acc pc -> - match pc with - | XXBuffer (_, ArgValue refpar, ArgValue sizepar) when has_index refpar -> - (APCReadOnly (get_index refpar, sizepar.apar_index)) :: acc - | XXBuffer (_, ArgValue refpar, _) when has_index refpar -> - (APCReadOnly (get_index refpar, None)) :: acc - | XXBlockWrite (_, ArgValue refpar, ArgValue sizepar) when has_index refpar -> - (APCWriteOnly (get_index refpar, sizepar.apar_index)) :: acc - | XXBlockWrite (_, ArgValue refpar, _) when has_index refpar -> - (APCWriteOnly (get_index refpar, None)) :: acc - | _ -> acc) [] sem.fsem_pre diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli index 378c3c2f..d14345a8 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli +++ b/CodeHawk/CHB/bchlib/bCHFunctionSemantics.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2023 Aarno Labs LLC + Copyright (c) 2021-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 @@ -50,12 +50,6 @@ val bvarinfo_to_function_semantics: bvarinfo_t -> function_interface_t -> function_semantics_t -(** {1 Conversion} *) - -val function_semantics_to_precondition_attributes: - function_semantics_t -> precondition_attribute_t list - - (** {1 Modification}*) (** [add_function_precondition fsem pre] returns the function semantics that diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml index dd9066cf..832918bd 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023 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 @@ -28,100 +28,352 @@ (* chlib *) open CHLanguage +open CHNumerical open CHPretty -open CHUtils (* chutil *) open CHLogger +open CHTraceResult open CHXmlDocument (* xprlib *) +open Xprt open XprTypes (* bchlib *) open BCHBasicTypes +open BCHBCTypePretty open BCHBCTypes open BCHBCTypeUtil open BCHCPURegisters open BCHLibTypes module H = Hashtbl +module TR = CHTraceResult +let x2p = XprToPretty.xpr_formatter#pr_expr +let p2s = CHPrettyUtil.pretty_to_string +let x2s x = p2s (x2p x) + + +let bcd = BCHBCDictionary.bcdictionary let bd = BCHDictionary.bdictionary -class saved_register_t (reg:register_t) = -object (_self:'a) +let stackslot_rec_to_pretty (sslot: stackslot_rec_t): pretty_t = + LBLOCK [ + STR "offset: "; INT sslot.sslot_offset; NL; + STR "name : "; STR sslot.sslot_name; NL; + STR "type : "; STR (btype_to_string sslot.sslot_btype); NL; + (match sslot.sslot_size with + | Some s -> LBLOCK [STR "size : "; INT s; NL] + | _ -> STR ""); + (match sslot.sslot_desc with + | Some desc -> LBLOCK [STR "desc : "; STR desc; NL] + | _ -> STR "") + ] - val mutable save_address = None - val restore_addresses = new StringCollections.set_t - method compare (other:'a) = Stdlib.compare reg other#get_register +class stackslot_t (sslot: stackslot_rec_t): stackslot_int = +object (self) - method set_save_address (a:ctxt_iaddress_t) = save_address <- Some a - method add_restore_address (a:ctxt_iaddress_t) = restore_addresses#add a + method sslot_rec = sslot - method get_register = reg + method name = sslot.sslot_name - method get_save_address = - match save_address with - Some a -> a - | _ -> - let msg = (LBLOCK [ STR "saved_register.get_save_address " ; - STR (register_to_string reg) ]) in - begin - ch_error_log#add "invocation error" msg ; - raise (Invocation_error - ("saved_register.get_save_address " ^ (register_to_string reg))) - end + method offset = sslot.sslot_offset + + method btype = sslot.sslot_btype + + method is_typed: bool = not (btype_equal self#btype t_unknown) + + method spill: register_t option = sslot.sslot_spill + + method is_spill: bool = Option.is_some self#spill + + method is_struct: bool = + match resolve_type self#btype with + | Ok (TComp _) -> true + | _ -> false - method get_restore_addresses = restore_addresses#toList + method is_array: bool = + match resolve_type self#btype with + | Ok (TArray _) -> true + | _ -> false - method has_save_address = - match save_address with Some _ -> true | _ -> false + method is_scalar: bool = + match resolve_type self#btype with + | Ok t -> is_scalar t + | _ -> false - method has_restore_addresses = not restore_addresses#isEmpty + method size: int option = sslot.sslot_size - method is_save_or_restore_address (iaddr:ctxt_iaddress_t) = - (match save_address with Some a -> a = iaddr | _ -> false) || - (List.mem iaddr restore_addresses#toList) + method desc = sslot.sslot_desc - method write_xml (node:xml_element_int) = + method contains_offset (offset: int) = + let size = match self#size with + | Some s -> s + | _ -> 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 frame_offset_memory_offset + ?(tgtsize=None) + ?(tgtbtype=t_unknown) + (xpr: xpr_t): memory_offset_t traceresult = + TR.tbind + (self#object_offset_memory_offset ~tgtsize ~tgtbtype) + (self#frame2object_offset_value xpr) + + method object_offset_memory_offset + ?(tgtsize=None) + ?(tgtbtype=t_unknown) + (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"] + + method private arrayvar_memory_offset + ~(tgtsize: int option) + ~(tgtbtype: btype_t option) + (btype: btype_t) + (xoffset: xpr_t): memory_offset_t traceresult = + let iszero x = + 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)] + + 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 + 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)] + + method private get_field_memory_offset_at + ~(tgtsize: int option) + ~(tgtbtype: btype_t option) + (c: bcompinfo_t) + (xoffset: xpr_t): memory_offset_t traceresult = + let is_void_tgtbtype = + match tgtbtype with + | Some (TVoid _) -> true + | _ -> false in + let pr_tgtsize = + match tgtsize with + | Some s -> string_of_int s + | _ -> "?" in + let check_tgttype_compliance (t: btype_t) (s: int) = + match tgtsize, tgtbtype with + | None, None -> true + | Some size, None -> size = s + | Some size, Some (TVoid _) -> size = s + | None, Some (TVoid _) -> true + | None, Some ty -> btype_equal ty t + | Some size, Some ty -> size = s && btype_equal ty t in + let compliance_failure (t: btype_t) (s: int) = + let size_discrepancy size s = + "size discrepancy between tgtsize: " + ^ (string_of_int size) + ^ " and field size: " + ^ (string_of_int s) in + let type_discrepancy ty t = + "type discrepancy between tgttype: " + ^ (btype_to_string ty) + ^ " and field type: " + ^ (btype_to_string t) in + match tgtsize, tgtbtype with + | Some size, Some ty when (size != s) && (not (btype_equal ty t)) -> + (size_discrepancy size s) ^ " and " ^ (type_discrepancy ty t) + | 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 + 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 ] + + method write_xml(node: xml_element_int) = begin - bd#write_xml_register node reg ; - (match save_address with - | Some a -> node#setAttribute "save" a ; - | _ -> ()) ; - (if restore_addresses#isEmpty then () else - node#setAttribute "restore" (String.concat ";" restore_addresses#toList)) + node#setAttribute "name" self#name; + node#setIntAttribute "offset" self#offset; + (match self#size with + | Some s -> node#setIntAttribute "size" s + | _ -> ()); + (if is_known_type self#btype then + node#setIntAttribute "tix" (bcd#index_typ self#btype)); + (if self#is_spill then + node#setIntAttribute "srix" (bd#index_register (Option.get self#spill))); + (match self#desc with + | Some d -> node#setAttribute "desc" d + | _ -> ()); end - method toPretty = - let pSaved = match save_address with - | Some a -> LBLOCK [ STR "saved: " ; STR a ] - | _ -> STR "not saved" in - let pRestored = match restore_addresses#toList with - | [] -> STR "not restored" - | l -> - LBLOCK [ - STR "restored: "; - pretty_print_list l (fun a -> STR a) "[" ", " "]" ] in - LBLOCK [ - STR (register_to_string reg); - STR ". "; - pSaved; - STR "; "; - pRestored] - end -class stackframe_t (varmgr: variable_manager_int):stackframe_int = +class stackframe_t + (fndata: function_data_int) + (varmgr: variable_manager_int):stackframe_int = object (self) - val saved_registers = H.create 3 (* reg -> saved_register_t *) + (* val saved_registers = H.create 3 (* reg -> saved_register_t *) *) val accesses = H.create 3 (* offset -> (iaddr, stack_access_t) list *) + 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 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_name = svintro.svi_name; + sslot_btype = ty; + sslot_spill = None; + sslot_desc = Some ("svintro"); + sslot_size = size} in + 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 + | _ -> ()); + slots + end method private vard = varmgr#vard @@ -136,46 +388,141 @@ object (self) [] in H.replace accesses offset ((iaddr, acc) :: entry) + method containing_stackslot (offset: int): stackslot_int option = + H.fold (fun _ sslot acc -> + match acc with + | Some _ -> acc + | _ -> if sslot#contains_offset offset then Some sslot else None) + stackslots None + + method add_stackslot + ?(name = None) + ?(btype = t_unknown) + ?(spill = None) + ?(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 + begin + log_error_result + ~tag:"duplicate stack slot" + ~msg:("Stack slot at offset " + ^ (string_of_int offset) + ^ "already exists") + __FILE__ __LINE__ []; + Ok (H.find stackslots offset) + end + else + match self#containing_stackslot offset with + | Some sslot -> + let msg = + "Stackslot at offset " + ^ (string_of_int offset) + ^ " overlaps with " + ^ sslot#name + ^ " (" + ^ (string_of_int sslot#offset) + ^ (match sslot#size with + | Some s -> ", size: " ^ (string_of_int s) + | _ -> "") + ^ ")" in + begin + log_error_result + ~tag:"overlapping stackslot" + ~msg + __FILE__ __LINE__ []; + Error [msg] + end + | _ -> + let sname = + match name with + | Some name -> name + | _ -> "var_" ^ (string_of_int offset) in + let ssrec = { + sslot_name = sname; + sslot_offset = offset; + sslot_btype = btype; + sslot_spill = spill; + sslot_size = size; + sslot_desc = desc + } in + let sslot = new stackslot_t ssrec in + begin + H.add stackslots offset sslot; + chlog#add + "stackframe:add stackslot" + (LBLOCK [ + INT offset; + STR ": "; + STR sslot#name]); + Ok sslot + end + method add_register_spill ~(offset: int) (reg: register_t) (iaddr:ctxt_iaddress_t) = let spill = RegisterSpill (offset, reg) in - let _ = self#add_access offset iaddr spill in - let regstr = register_to_string reg in - if H.mem saved_registers regstr then - (H.find saved_registers regstr)#set_save_address iaddr - else - let savedreg = new saved_register_t reg in - begin - savedreg#set_save_address iaddr; - H.add saved_registers regstr savedreg - end + begin + (if H.mem stackslots offset then + if (H.find stackslots offset)#is_spill then + () + else + raise (BCH_failure (LBLOCK [STR "Stackslot already taken"])) + 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_desc = Some "register spill" + } in + let sslot = new stackslot_t ssrec in + H.add stackslots offset sslot); + self#add_access offset iaddr spill + end method add_register_restore ~(offset: int) (reg: register_t) (iaddr: ctxt_iaddress_t) = let restore = RegisterRestore (offset, reg) in - let _ = self#add_access offset iaddr restore in - let regstr = register_to_string reg in - if H.mem saved_registers regstr then - (H.find saved_registers regstr)#add_restore_address iaddr - else - let savedreg = new saved_register_t reg in - begin - savedreg#add_restore_address iaddr; - H.add saved_registers regstr savedreg - end + begin + (if H.mem stackslots offset then + if (H.find stackslots offset)#is_spill then + () + else + raise (BCH_failure (LBLOCK [STR "Stackslot already taken"])) + 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_desc = Some "register_spill" + } in + let sslot = new stackslot_t ssrec in + H.add stackslots offset sslot); + self#add_access offset iaddr restore + end method add_load - ~(offset:int) + ~(baseoffset:int) + ~(offset:memory_offset_t) ~(size:int option) ~(typ:btype_t option) (var: variable_t) (iaddr:ctxt_iaddress_t) = let ty = match typ with Some t -> t | _ -> t_unknown in let load = StackLoad (var, offset, size, ty) in - self#add_access offset iaddr load + self#add_access baseoffset iaddr load method add_store - ~(offset:int) + ~(baseoffset:int) + ~(offset:memory_offset_t) ~(size:int option) ~(typ:btype_t option) ~(xpr:xpr_t option) @@ -183,7 +530,7 @@ object (self) (iaddr:ctxt_iaddress_t) = let ty = match typ with Some t -> t | _ -> t_unknown in let store = StackStore (var, offset, size, ty, xpr) in - self#add_access offset iaddr store + self#add_access baseoffset iaddr store method add_block_read ~(offset:int) @@ -204,15 +551,15 @@ object (self) let store = StackBlockWrite (offset, size, ty, xpr) in self#add_access offset iaddr store - method private write_xml_saved_registers (node:xml_element_int) = - let savedregs = H.fold (fun _ v a -> v::a) saved_registers [] in - node#appendChildren - (List.map (fun s -> - let n = xmlElement "sr" in - begin - s#write_xml n; - n - end) savedregs) + method private write_xml_stack_slots (node: xml_element_int) = + begin + H.iter (fun _ slot -> + let slotnode = xmlElement "slot" in + begin + slot#write_xml slotnode; + node#appendChildren [slotnode] + end) stackslots; + end method private write_xml_stack_accesses (node: xml_element_int) = let slist = ref [] in @@ -233,12 +580,13 @@ object (self) method write_xml (node: xml_element_int) = let append = node#appendChildren in - let srNode = xmlElement "saved-registers" in + (* let srNode = xmlElement "saved-registers" in *) + let sNode = xmlElement "stack-slots" in let saNode = xmlElement "stack-accesses" in begin - self#write_xml_saved_registers srNode; + self#write_xml_stack_slots sNode; self#write_xml_stack_accesses saNode; - append [srNode; saNode] + append [sNode; saNode] end diff --git a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli index 204c7229..e0cc6d16 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli +++ b/CodeHawk/CHB/bchlib/bCHFunctionStackframe.mli @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - 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 @@ -25,9 +25,13 @@ SOFTWARE. ============================================================================= *) +(* chlib *) +open CHPretty (* bchlib *) open BCHLibTypes +val stackslot_rec_to_pretty: stackslot_rec_t -> pretty_t -val mk_function_stackframe: variable_manager_int -> stackframe_int +val mk_function_stackframe: + function_data_int -> variable_manager_int -> stackframe_int diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml index 9e4cc725..c732b9d0 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSummary.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -329,7 +329,7 @@ let function_summary_of_bvarinfo (vinfo: bvarinfo_t): function_summary_int = let fintf = bvarinfo_to_function_interface vinfo in let sem = bvarinfo_to_function_semantics vinfo fintf in let _ = - chlog#add + ch_diagnostics_log#add "function semantics of bvarinfo" (LBLOCK [ STR vinfo.bvname; diff --git a/CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml b/CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml index c1d742cf..eb23d99e 100644 --- a/CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml +++ b/CodeHawk/CHB/bchlib/bCHFunctionSummaryLibrary.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2020 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -264,6 +264,9 @@ object (self) if bcfiles#has_varinfo fname then 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 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 6e19b373..a9343b2b 100644 --- a/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml +++ b/CodeHawk/CHB/bchlib/bCHGlobalMemoryMap.ml @@ -541,12 +541,12 @@ object (self) ^ "Illegal global address: " ^ address#to_hex_string] else if H.mem locations address#index then begin - ch_error_log#add - "duplicate global location" - (LBLOCK [ - STR "Global location at address "; - address#toPretty; - STR " already exists"]); + log_error_result + ~tag:"duplicate global location" + ~msg:("Global location at address " + ^ address#to_hex_string + ^ "already exists") + __FILE__ __LINE__ []; Ok (H.find locations address#index) end else diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli index 45a4d6b9..298de577 100644 --- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli +++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli @@ -1443,6 +1443,7 @@ object method is_elf: bool method is_pe: bool method is_verbose: bool + method is_typing_rule_enabled: string -> bool method is_debug_excluded: bool method is_sideeffects_on_global_enabled: string -> bool method is_abstract_stackvars_disabled: bool @@ -1574,8 +1575,7 @@ class type function_data_int = method has_regvar_type_cast: doubleword_int -> bool method has_stackvar_type_annotation: int -> bool method has_stackvar_type_cast: int -> bool - method is_typing_rule_enabled: string -> string -> bool - method is_typing_rule_disabled: string -> string -> bool + 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 @@ -3181,6 +3181,7 @@ type type_constant_t = | TyTInt of signedness_t * int | TyTStruct of int * string (** bckey, bcname *) | TyTFloat of fkind_t + | TyVoidPtr (** only to be used in the context of a void pointer *) | TyTUnknown (** top in type lattice *) | TyBottom (** bottom in type lattice *) @@ -3476,6 +3477,12 @@ end (** {2 Assembly variable} *) +type sideeffect_argument_location_t = + | SEGlobal of doubleword_int + | SEStack of numerical_t + | SEDescr of string (* default value, uninterpreted *) + + (** Assembly variable denotations.*) type assembly_variable_denotation_t = (* size (bytes) memory reference index *) @@ -3554,11 +3561,12 @@ and constant_value_variable_t = | CallTargetValue of call_target_t | SideEffectValue of - ctxt_iaddress_t (* callsite *) - * string (* argument description *) - * bool (* is-global address *) - (** [SideEffectValue (iaddr, name, is_global)] represents the value - assigned by the callee at call site [iaddr] to the argument with + ctxt_iaddress_t (* callsite *) + * string (* name of parameter *) + * btype_t option (* type of value *) + * sideeffect_argument_location_t (* location of argument passed *) + (** [SideEffectValue (iaddr, name, seloc] represents the value + assigned by the callee at call site [iaddr] to the parameter with name [name].*) | BridgeVariable of ctxt_iaddress_t * int (* call site, argument index *) @@ -3735,9 +3743,10 @@ type stack_access_t = (** stack offset *) | RegisterRestore of int * register_t (** stack offset *) - | StackLoad of variable_t * int * int option * btype_t + | StackLoad of variable_t * memory_offset_t * int option * btype_t (** variable, offset, size *) - | StackStore of variable_t * int * int option * btype_t * xpr_t option + | StackStore of + variable_t * memory_offset_t * int option * btype_t * xpr_t option (** variable, offset, size, value *) | StackBlockRead of int * int option * btype_t (** offset, size *) @@ -3756,12 +3765,14 @@ class type vardictionary_int = method index_memory_offset: memory_offset_t -> int method index_memory_base: memory_base_t -> int + method index_sideeffect_argument_location: sideeffect_argument_location_t -> int method index_assembly_variable_denotation: assembly_variable_denotation_t -> int method index_constant_value_variable: constant_value_variable_t -> int method index_stack_access: stack_access_t -> int method get_memory_offset: int -> memory_offset_t method get_memory_base: int -> memory_base_t + method get_sideeffect_argument_location: int -> sideeffect_argument_location_t method get_assembly_variable_denotation: int -> assembly_variable_denotation_t method get_constant_value_variable: int -> constant_value_variable_t @@ -3843,6 +3854,17 @@ object -> numerical_t -> assembly_variable_int + (** [make_stack_variable ?size ?offset stackoffset] returns the stack variable + with base offset [stackoffset] and optional offset [offset] from the base. + + raise BCH_failure if [stackoffset >= 0]. + *) + method make_local_stack_variable: + ?size:int + -> ?offset:memory_offset_t + -> numerical_t + -> assembly_variable_int + (** {2 Auxiliary variables}*) @@ -3910,8 +3932,20 @@ object method make_calltarget_value: call_target_t -> assembly_variable_int method make_function_pointer_value: string -> string -> ctxt_iaddress_t -> assembly_variable_int + method make_global_sideeffect_value: + ?btype:btype_t option + -> ctxt_iaddress_t + -> string + -> doubleword_int + -> assembly_variable_int + method make_stack_sideeffect_value: + ?btype:btype_t option + -> ctxt_iaddress_t + -> string + -> numerical_t + -> assembly_variable_int method make_side_effect_value: - ctxt_iaddress_t -> ?global:bool -> string -> assembly_variable_int + ctxt_iaddress_t -> string -> string -> assembly_variable_int method make_field_value: string -> int -> string -> assembly_variable_int (** {2 Memory references}*) @@ -4514,6 +4548,106 @@ end (** {1 Functions} *) + type stackslot_rec_t = { + sslot_name: string; + sslot_offset: int; + sslot_btype: btype_t; + sslot_size: int option; + sslot_spill: register_t option; + sslot_desc: string option + } + + +class type stackslot_int = + object + + method sslot_rec: stackslot_rec_t + method name: string + method offset: int + method btype: btype_t + method spill: register_t option + method size: int option + method desc: string option + method contains_offset: int -> bool + method frame2object_offset_value: xpr_t -> xpr_t traceresult + method frame_offset_memory_offset: + ?tgtsize:int option + -> ?tgtbtype:btype_t + -> xpr_t + -> memory_offset_t traceresult + method object_offset_memory_offset: + ?tgtsize:int option + -> ?tgtbtype:btype_t + -> xpr_t + -> memory_offset_t traceresult + + method is_typed: bool + method is_scalar: bool + method is_struct: bool + method is_array: bool + method is_spill: bool + + method write_xml: xml_element_int -> unit + end + + +class type stackframe_int = + object + + method add_register_spill: + offset:int -> register_t -> ctxt_iaddress_t -> unit + method add_register_restore: + offset:int -> register_t -> ctxt_iaddress_t -> unit + + method add_stackslot: + ?name: string option + -> ?btype: btype_t + -> ?spill: register_t option + -> ?size: int option + -> ?desc: string option + -> int + -> stackslot_int traceresult + + method containing_stackslot: int -> stackslot_int option + + method add_load: + baseoffset:int + -> offset: memory_offset_t + -> size:int option + -> typ:btype_t option + -> variable_t + -> ctxt_iaddress_t + -> unit + + method add_store: + baseoffset:int + -> offset: memory_offset_t + -> size:int option + -> typ:btype_t option + -> xpr:xpr_t option + -> variable_t + -> ctxt_iaddress_t + -> unit + + method add_block_read: + offset:int + -> size:int option + -> typ:btype_t option + -> ctxt_iaddress_t + -> unit + method add_block_write: + offset:int + -> size:int option + -> typ:btype_t option + -> xpr:xpr_t option + -> ctxt_iaddress_t + -> unit + + method write_xml: xml_element_int -> unit + + end + + (** {2 Function symbol table} *) (** Function environment: function symbol table that keeps track of all @@ -4655,6 +4789,9 @@ class type function_environment_int = method mk_gloc_variable: global_location_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. @@ -4723,8 +4860,19 @@ class type function_environment_int = method mk_calltarget_value: call_target_t -> variable_t method mk_function_pointer_value: string -> string -> ctxt_iaddress_t -> variable_t - method mk_side_effect_value: - ctxt_iaddress_t -> ?global:bool-> string -> variable_t + method mk_global_sideeffect_value: + ?btype:btype_t option + -> ctxt_iaddress_t + -> doubleword_int + -> string + -> variable_t + method mk_stack_sideeffect_value: + ?btype:btype_t option + -> ctxt_iaddress_t + -> numerical_t + -> string + -> variable_t + method mk_side_effect_value: ctxt_iaddress_t -> string -> variable_t method mk_field_value: string -> int -> string -> variable_t method mk_symbolic_value: xpr_t -> variable_t method mk_signed_symbolic_value: xpr_t -> int -> int -> variable_t @@ -5188,48 +5336,6 @@ class type xpodictionary_int = end -class type stackframe_int = - object - - method add_register_spill: - offset:int -> register_t -> ctxt_iaddress_t -> unit - method add_register_restore: - offset:int -> register_t -> ctxt_iaddress_t -> unit - - method add_load: - offset:int - -> size:int option - -> typ:btype_t option - -> variable_t - -> ctxt_iaddress_t - -> unit - - method add_store: - offset:int - -> size:int option - -> typ:btype_t option - -> xpr:xpr_t option - -> variable_t - -> ctxt_iaddress_t - -> unit - - method add_block_read: - offset:int - -> size:int option - -> typ:btype_t option - -> ctxt_iaddress_t - -> unit - method add_block_write: - offset:int - -> size:int option - -> typ:btype_t option - -> xpr:xpr_t option - -> ctxt_iaddress_t - -> unit - - method write_xml: xml_element_int -> unit - - end type po_status_t = @@ -6020,6 +6126,8 @@ class type floc_int = -> xpr_t (** address value *) -> variable_t traceresult + method get_variable_type: variable_t -> btype_t traceresult + method get_xpr_type: xpr_t -> btype_t traceresult (** {2 Predicates on variables}*) @@ -6175,7 +6283,8 @@ class type floc_int = method get_conditional_assign_commands: xpr_t -> variable_t -> xpr_t -> cmd_t list - method get_sideeffect_assigns: function_semantics_t -> cmd_t list + method get_sideeffect_assigns: + bterm_evaluator_int -> function_semantics_t -> cmd_t list (** {2 Variable abstraction}*) diff --git a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml index 7298fc33..ecbf5de9 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml +++ b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.ml @@ -147,11 +147,17 @@ object (self) else if self#env#is_stack_variable lhs then log_tfold (log_error "record_assignment_lhs" "invalid offset") - ~ok:(fun offset -> - match offset with - | ConstantOffset (n, NoOffset) -> + ~ok:(fun stackoffset -> + match stackoffset with + | ConstantOffset (n, offset) -> self#finfo#stackframe#add_store - ~offset:n#toInt ~size ~typ:(Some vtype) ~xpr:(Some rhs) lhs iaddr + ~baseoffset:n#toInt + ~offset + ~size + ~typ:(Some vtype) + ~xpr:(Some rhs) + lhs + iaddr | _ -> chlog#add "stack assignment lhs not recorded" @@ -178,11 +184,16 @@ object (self) else if self#env#is_stack_variable v then log_tfold (log_error "record_assignment_rhs" "invalid offset") - ~ok:(fun offset -> - match offset with - | ConstantOffset (n, NoOffset) -> + ~ok:(fun stackoffset -> + match stackoffset with + | ConstantOffset (n, offset) -> self#finfo#stackframe#add_load - ~offset:n#toInt ~size ~typ:(Some vtype) v iaddr + ~baseoffset:n#toInt + ~offset + ~size + ~typ:(Some vtype) + v + iaddr | _ -> chlog#add "stack assignment rhs not recorded" @@ -203,11 +214,16 @@ object (self) if self#env#is_stack_variable var then log_tfold (log_error "record_load" "invalid offset") - ~ok:(fun offset -> - match offset with - | ConstantOffset (n, NoOffset) -> + ~ok:(fun stackoffset -> + match stackoffset with + | ConstantOffset (n, offset) -> self#finfo#stackframe#add_load - ~offset:n#toInt ~size:(Some size) ~typ:(Some vtype) var iaddr + ~baseoffset:n#toInt + ~offset + ~size:(Some size) + ~typ:(Some vtype) + var + iaddr | _ -> chlog#add "stack load not recorded" @@ -246,14 +262,22 @@ object (self) ~ok:(fun var -> if self#env#is_stack_variable var then TR.tfold - ~ok:(fun offset -> - match offset with - | ConstantOffset (n, NoOffset) -> + ~ok:(fun stackoffset -> + match stackoffset with + | ConstantOffset (n, offset) -> self#finfo#stackframe#add_load - ~offset:n#toInt ~size:(Some size) ~typ:(Some vtype) var iaddr + ~baseoffset:n#toInt + ~offset + ~size:(Some size) + ~typ:(Some vtype) + var + iaddr | _ -> log_error_result __FILE__ __LINE__ - ["memrecorder:stack"; p2s self#loc#toPretty]) + ["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) else @@ -287,11 +311,12 @@ object (self) if self#env#is_stack_variable var then log_tfold (log_error "record_store" "invalid offset") - ~ok:(fun offset -> - match offset with - | ConstantOffset (n, NoOffset) -> + ~ok:(fun stackoffset -> + match stackoffset with + | ConstantOffset (n, offset) -> self#finfo#stackframe#add_store - ~offset:n#toInt + ~baseoffset:n#toInt + ~offset ~size:(Some size) ~typ:(Some vtype) ~xpr:(Some xpr) @@ -341,11 +366,12 @@ object (self) ~ok:(fun var -> if self#env#is_stack_variable var then TR.tfold - ~ok:(fun offset -> - match offset with - | ConstantOffset (n, NoOffset) -> + ~ok:(fun stackoffset -> + match stackoffset with + | ConstantOffset (n, offset) -> self#finfo#stackframe#add_store - ~offset:n#toInt + ~baseoffset:n#toInt + ~offset ~size:(Some size) ~typ:(Some vtype) ~xpr:(TR.tfold_default (fun x -> Some x) None xpr_r) @@ -353,7 +379,10 @@ object (self) iaddr | _ -> log_error_result __FILE__ __LINE__ - ["memrecorder:stack"; p2s self#loc#toPretty]) + ["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) else diff --git a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli index fbaaead0..ef71b582 100644 --- a/CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli +++ b/CodeHawk/CHB/bchlib/bCHMemoryRecorder.mli @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2023 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 diff --git a/CodeHawk/CHB/bchlib/bCHPrecondition.ml b/CodeHawk/CHB/bchlib/bCHPrecondition.ml index b9bcd059..429f56ae 100644 --- a/CodeHawk/CHB/bchlib/bCHPrecondition.ml +++ b/CodeHawk/CHB/bchlib/bCHPrecondition.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -37,11 +37,9 @@ open CHXmlDocument open CHXmlReader (* bchlib *) -open BCHBasicTypes open BCHFtsParameter open BCHBCTypePretty open BCHBCTypes -open BCHBCTypeUtil open BCHBCTypeXml open BCHBTerm open BCHCStructConstant @@ -244,41 +242,3 @@ let read_xml_preconditions (List.map (fun n -> read_xml_precondition n thisf parameters) (getcc "pre")) - - -let make_attribute_preconditions - (attrs: precondition_attribute_t list) - (parameters: fts_parameter_t list): xxpredicate_t list = - let get_par (n: int) = - try - List.find (fun p -> - match p.apar_index with Some ix -> ix = n | _ -> false) parameters - with - | Not_found -> - raise - (BCH_failure - (LBLOCK [ - STR "No parameter with index "; - INT n; - pretty_print_list (List.map (fun p -> p.apar_name) parameters) - (fun s -> STR s) "[" "," "]" ])) in - let get_derefty (par: fts_parameter_t): btype_t = - if is_pointer par.apar_type then - ptr_deref par.apar_type - else - raise - (BCH_failure - (LBLOCK [ - STR "parameter is not a pointer type: "; - fts_parameter_to_pretty par])) in - List.fold_left (fun acc attr -> - match attr with - | (APCReadOnly (n, None)) -> - let par = get_par n in - let ty = get_derefty par in - (XXBuffer (ty, ArgValue par, RunTimeValue)) :: acc - | (APCWriteOnly (n, None)) -> - let par = get_par n in - let ty = get_derefty par in - (XXBlockWrite (ty, ArgValue par, RunTimeValue)) :: acc - | _ -> acc) [] attrs diff --git a/CodeHawk/CHB/bchlib/bCHPrecondition.mli b/CodeHawk/CHB/bchlib/bCHPrecondition.mli index 77b823ce..bba87b4e 100644 --- a/CodeHawk/CHB/bchlib/bCHPrecondition.mli +++ b/CodeHawk/CHB/bchlib/bCHPrecondition.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -31,7 +31,6 @@ open CHXmlDocument (* bchlib *) -open BCHBCTypes open BCHLibTypes @@ -59,7 +58,3 @@ val read_xml_precondition: val read_xml_preconditions: xml_element_int -> bterm_t -> fts_parameter_t list -> xxpredicate_t list - - -val make_attribute_preconditions: - precondition_attribute_t list -> fts_parameter_t list -> xxpredicate_t list diff --git a/CodeHawk/CHB/bchlib/bCHSideeffect.ml b/CodeHawk/CHB/bchlib/bCHSideeffect.ml index 5d35a6f0..7f5010e1 100644 --- a/CodeHawk/CHB/bchlib/bCHSideeffect.ml +++ b/CodeHawk/CHB/bchlib/bCHSideeffect.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -37,10 +37,7 @@ open CHXmlDocument open CHXmlReader (* bchlib *) -open BCHBasicTypes open BCHBCTypePretty -open BCHBCTypes -open BCHBCTypeUtil open BCHBCTypeXml open BCHBTerm open BCHFtsParameter @@ -180,37 +177,3 @@ let read_xml_sideeffects (parameters: fts_parameter_t list): xxpredicate_t list = let getcc = node#getTaggedChildren in List.map (fun n -> read_xml_sideeffect n thisf parameters) (getcc "sideeffect") - - -let make_attribute_sideeffects - (attrs: precondition_attribute_t list) - (parameters: fts_parameter_t list): xxpredicate_t list = - let get_par (n: int) = - try - List.find (fun p -> - match p.apar_index with Some ix -> ix = n | _ -> false) parameters - with - | Not_found -> - raise - (BCH_failure - (LBLOCK [ - STR "No parameter with index "; - INT n; - pretty_print_list (List.map (fun p -> p.apar_name) parameters) - (fun s -> STR s) "[" "," "]" ])) in - let get_derefty (par: fts_parameter_t): btype_t = - if is_pointer par.apar_type then - ptr_deref par.apar_type - else - raise - (BCH_failure - (LBLOCK [ - STR "parameter is not a pointer type: "; - fts_parameter_to_pretty par])) in - List.fold_left (fun acc attr -> - match attr with - | (APCWriteOnly (n, None)) -> - let par = get_par n in - let ty = get_derefty par in - (XXBlockWrite (ty, ArgValue par, RunTimeValue)) :: acc - | _ -> acc) [] attrs diff --git a/CodeHawk/CHB/bchlib/bCHSideeffect.mli b/CodeHawk/CHB/bchlib/bCHSideeffect.mli index 3a17fa7e..64224d3b 100644 --- a/CodeHawk/CHB/bchlib/bCHSideeffect.mli +++ b/CodeHawk/CHB/bchlib/bCHSideeffect.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny B. Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -31,7 +31,6 @@ open CHXmlDocument (* bchlib *) -open BCHBCTypes open BCHLibTypes @@ -44,7 +43,3 @@ val read_xml_sideeffect: val read_xml_sideeffects: xml_element_int -> bterm_t -> fts_parameter_t list -> xxpredicate_t list - - -val make_attribute_sideeffects: - precondition_attribute_t list -> fts_parameter_t list -> xxpredicate_t list diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml index 6f19a95a..e21b4023 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.ml @@ -559,11 +559,13 @@ object | TyTInt _ -> "ti" | TyTStruct _ -> "ts" | TyTFloat _ -> "tf" + | TyVoidPtr -> "vp" | TyTUnknown -> "u" | TyBottom -> "b" method !tags = [ - "a"; "ac"; "acl"; "ap"; "asl"; "ax"; "b"; "i"; "s"; "ti"; "tf"; "ts"; "u"; "z"] + "a"; "ac"; "acl"; "ap"; "asl"; "ax"; "b"; "i"; + "s"; "ti"; "tf"; "ts"; "u"; "vp"; "z"] end @@ -651,6 +653,25 @@ end let memory_offset_mcts: memory_offset_t mfts_int = new memory_offset_mcts_t +class sideeffect_argument_location_mcts_t:[sideeffect_argument_location_t] mfts_int = +object + + inherit [sideeffect_argument_location_t] mcts_t "sideeffect_argument_location" + + method !ts (s: sideeffect_argument_location_t) = + match s with + | SEGlobal _ -> "g" + | SEStack _ -> "s" + | SEDescr _ -> "d" + + method !tags = ["d"; "g"; "s"] + +end + +let sideeffect_argument_location_mcts: sideeffect_argument_location_t mfts_int = + new sideeffect_argument_location_mcts_t + + class assembly_variable_denotation_mcts_t:[assembly_variable_denotation_t] mfts_int = object diff --git a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli index 646ff3d7..07b9f381 100644 --- a/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli +++ b/CodeHawk/CHB/bchlib/bCHSumTypeSerializer.mli @@ -5,7 +5,7 @@ The MIT License (MIT) Copyright (c) 2005-2020 Kestrel Technology LLC - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -96,6 +96,7 @@ val type_constraint_mcts: type_constraint_t mfts_int val memory_base_mcts: memory_base_t mfts_int val memory_offset_mcts: memory_offset_t mfts_int +val sideeffect_argument_location_mcts: sideeffect_argument_location_t mfts_int val assembly_variable_denotation_mcts: assembly_variable_denotation_t mfts_int val constant_value_variable_mcts: constant_value_variable_t mfts_int val stack_access_mcts: stack_access_t mfts_int diff --git a/CodeHawk/CHB/bchlib/bCHSystemSettings.ml b/CodeHawk/CHB/bchlib/bCHSystemSettings.ml index e8b889f9..6578e247 100644 --- a/CodeHawk/CHB/bchlib/bCHSystemSettings.ml +++ b/CodeHawk/CHB/bchlib/bCHSystemSettings.ml @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020 Henny Sipma - Copyright (c) 2021-2024 Aarno Labs LLC + Copyright (c) 2021-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 @@ -38,6 +38,7 @@ open BCHBasicTypes open BCHLibTypes open BCHUtilities +module H = Hashtbl let fns_included = ref [] let include_function (s: string) = fns_included := s :: !fns_included @@ -49,6 +50,77 @@ let exclude_function (s: string) = fns_excluded := s :: !fns_excluded let excluded_functions () = !fns_excluded +let arm_typingrules_settings = H.create 23 + +let _ = + List.iter (fun (r, s) -> + H.add arm_typingrules_settings r s) + [(* propagation rules *) + ("ADD-c", "enable"); + ("AND-rdef", "enable"); + ("ASR-rdef", "enable"); + ("CMP-rdef", "enable"); + ("LSL_rdef", "enable"); + ("LSR_rdef", "enable"); + ("MOV-c", "enable"); + ("MOV-rdef", "enable"); + ("MVN-rdef", "enable"); + ("ORR-rdef", "enable"); + ("POP-rdef", "enable"); + ("RSB-rdef", "enable"); + ("SMULL-rdef", "enable"); + ("STR-rdef", "enable"); + ("SUB-rdef", "enable"); + ("UBFX-rdef", "enable"); + + (* load/store rules *) + ("LDR-load", "enable"); + ("LDRB-load", "enable"); + ("LDRH-load", "enable"); + ("STR-store", "enable"); + ("STRB-store", "enable"); + ("STRH-store", "enable"); + + (* function return type back propagation *) + ("ADD-exituse", "enable"); + ("AND-exituse", "enable"); + ("ASR-exituse", "enable"); + ("LDR-exituse", "enable"); + ("LDRB-exituse", "enable"); + ("LDRH-exituse", "enable"); + ("LSL-exituse", "enable"); + ("LSR-exituse", "enable"); + ("MOV-exituse", "enable"); + ("MVN-exituse", "enable"); + ("ORR-exituse", "enable"); + ("RSB-exituse", "enable"); + ("SUB-exituse", "enable"); + ("UBFX-exituse", "enable"); + ("UXTH-exituse", "enable"); + + (* default setting of lhs *) + ("ASR-def-lhs", "enable"); + ("LDRB-def-lhs", "enable"); + ("LDRH-def-lhs", "enable"); + ("MVN-def-lhs", "enable"); + ("SMULL-def-lhs", "enable"); + ("UXTH-def-lhs", "enable"); + + (* misc rules *) + ("ADD-global", "enable"); + ("BL-sig-regarg", "enable"); + ("BL-sig-stackarg", "enable"); + ("BL-sig-rv", "enable"); + ("LDR-array", "enable"); + ("LDR-memop-tc", "enable"); + ("LDR-stack-addr", "enable"); + ("LDR-struct-field", "enable"); + ("LDRH-memop-tc", "enable"); + ("POP-sig-rv", "enable"); + ("STR-memop-tc", "enable") + ] + + (* ------------------------------------------------------------------------- * Command-line switches: * - set_vftables: for all jump tables, if one of the targets is a function entry @@ -313,6 +385,13 @@ object (self) | [] -> not (List.mem gv not_record_sideeffects_on_globals) | l -> List.mem gv l) + method is_typing_rule_enabled (name: string) = + match self#get_architecture with + | "arm" -> + (H.mem arm_typingrules_settings name) + && (H.find arm_typingrules_settings name) == "enable" + | _ -> false + end diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml index 35a7d232..3d7d8a68 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintDictionary.ml @@ -4,7 +4,7 @@ ------------------------------------------------------------------------------ The MIT License (MIT) - Copyright (c) 2024 Aarno Labs LLC + Copyright (c) 2024-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 @@ -171,6 +171,7 @@ object (self) | TyTInt (sg, si) -> (tags @ [signedness_mfts#ts sg], [si]) | TyTStruct (key, name) -> (tags @ [name], [key]) | TyTFloat k -> (tags @ [fkind_mfts#ts k], []) + | TyVoidPtr -> (tags, []) | TyBottom -> (tags, []) | TyTUnknown -> (tags, []) in type_constant_table#add key @@ -192,6 +193,7 @@ object (self) | "ti" -> TyTInt (signedness_mfts#fs (t 1), a 0) | "tf" -> TyTFloat (fkind_mfts#fs (t 1)) | "ts" -> TyTStruct (a 0, t 1) + | "vp" -> TyVoidPtr | "b" -> TyBottom | "u" -> TyTUnknown | s -> raise_tag_error name s type_constant_mcts#tags diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml index e8e1f252..3ca84ac0 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintStore.ml @@ -543,6 +543,10 @@ object (self) match result#toList with | [ixty1; ixty2] -> (match (bcd#get_typ ixty1), (bcd#get_typ ixty2) with + | TPtr (TVoid _, _), TPtr _ -> + Some (bcd#get_typ ixty2) + | TPtr _, TPtr (TVoid _, _) -> + Some (bcd#get_typ ixty1) | TPtr (tty1, _), TPtr (tty2, _) when is_struct_type tty1 && is_scalar tty2 -> Some (bcd#get_typ ixty1) diff --git a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml index 46cf7bfb..b80ea612 100644 --- a/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml +++ b/CodeHawk/CHB/bchlib/bCHTypeConstraintUtil.ml @@ -140,6 +140,7 @@ let type_constant_to_string (c: type_constant_t) = ^ "(" ^ (string_of_int si) ^ ")" | TyTStruct (_, name) -> "t_struct_" ^ name | TyTFloat k -> float_type_to_string k + | TyVoidPtr -> "t_voidptr" | TyTUnknown -> "t_top" | TyBottom -> "t_bottom" @@ -442,6 +443,8 @@ let rec mk_btype_constraint (tv: type_variable_t) (ty: btype_t) | TComp (key, _) -> let cinfo = bcfiles#get_compinfo key in Some (TyGround (TyVariable tv, TyConstant (TyTStruct (key, cinfo.bcname)))) + | TPtr (TVoid _, _) -> + Some (TyGround (TyVariable tv, TyConstant TyVoidPtr)) | TPtr (pty, _) -> let ptv = add_deref_capability tv in mk_btype_constraint ptv pty @@ -461,6 +464,10 @@ let rec mk_btype_constraint (tv: type_variable_t) (ty: btype_t) "Unable to create array access capability (no size): %s [%s:%d]" (String.concat "; " e) __FILE__ __LINE__; + log_diagnostics_result + __FILE__ __LINE__ + ["Unable to create array access capability (no size): " + ^ (String.concat "; " e)]; None end) | rty -> @@ -514,6 +521,7 @@ let type_constant_to_btype (tc: type_constant_t) = TInt (ikind, []) | TyTStruct (key, _) -> get_compinfo_struct_type (bcfiles#get_compinfo key) | TyTFloat fkind -> TFloat (fkind, FScalar, []) + | TyVoidPtr -> t_voidptr | TyBottom -> t_unknown | TyTUnknown -> t_unknown diff --git a/CodeHawk/CHB/bchlib/bCHVarDictionary.ml b/CodeHawk/CHB/bchlib/bCHVarDictionary.ml index 5359fc30..c8435b97 100644 --- a/CodeHawk/CHB/bchlib/bCHVarDictionary.ml +++ b/CodeHawk/CHB/bchlib/bCHVarDictionary.ml @@ -44,6 +44,8 @@ open BCHBasicTypes open BCHLibTypes open BCHSumTypeSerializer +module TR = CHTraceResult + let bcd = BCHBCDictionary.bcdictionary let bd = BCHDictionary.bdictionary @@ -74,6 +76,8 @@ object (self) val xd = xd val memory_base_table = mk_index_table "memory-base-table" val memory_offset_table = mk_index_table "memory-offset-table" + val sideeffect_argument_location_table = + mk_index_table "sideeffect-argument-location-table" val assembly_variable_denotation_table = mk_index_table "assembly-variable-denotation-table" val constant_value_variable_table = @@ -87,6 +91,7 @@ object (self) tables <- [ memory_base_table; memory_offset_table; + sideeffect_argument_location_table; assembly_variable_denotation_table; constant_value_variable_table; stack_access_table @@ -172,6 +177,38 @@ object (self) | "u" -> UnknownOffset | s -> raise_tag_error name s memory_offset_mcts#tags + method index_sideeffect_argument_location (s: sideeffect_argument_location_t) = + let tags = [sideeffect_argument_location_mcts#ts s] in + let key = match s with + | SEGlobal a -> (tags @ [a#to_hex_string], []) + | SEStack s -> (tags @ [s#toString], []) + | SEDescr d -> (tags @ [d], []) in + sideeffect_argument_location_table#add key + + method get_sideeffect_argument_location (index: int) = + let name = "sideeffect_location" in + let (tags, _) = sideeffect_argument_location_table#retrieve index in + let t = t name tags in + match (t 0) with + | "d" -> SEDescr (t 1) + | "g" -> + TR.tfold + ~ok:(fun dw -> SEGlobal dw) + ~error:(fun e -> + begin + log_error_result + ~msg:"get_sideeffect_location" + ~tag:"vardictionary error" + __FILE__ __LINE__ e; + raise + (BCH_failure + (LBLOCK [STR "Vardictionary: get_sideeffect_location: "; + STR (String.concat "; " e)])) + end) + (BCHDoubleword.string_to_doubleword (t 1)) + | "s" -> SEStack (CHNumerical.mkNumericalFromString (t 1)) + | s -> raise_tag_error name s sideeffect_argument_location_mcts#tags + method index_assembly_variable_denotation (v:assembly_variable_denotation_t) = let tags = [ assembly_variable_denotation_mcts#ts v ] in let key = match v with @@ -182,7 +219,7 @@ object (self) assembly_variable_denotation_table#add key method get_assembly_variable_denotation (index:int) = - let name = "assembly_variable_denotation" in + let name = "assembly_variable_denotation" in let (tags,args) = assembly_variable_denotation_table#retrieve index in let t = t name tags in let a = a name args in @@ -207,8 +244,11 @@ object (self) | FunctionPointer (s1, s2, a) -> (tags @ [a], [bd#index_string s1; bd#index_string s2]) | CallTargetValue t -> (tags, [id#index_call_target t]) - | SideEffectValue (a, name, isglobal) -> - (tags @ [a ], [bd#index_string name; (if isglobal then 1 else 0)]) + | SideEffectValue (a, name, optty, seloc) -> + (tags @ [a], + [bd#index_string name; + (match optty with Some ty -> bcd#index_typ ty | _ -> (-1)); + self#index_sideeffect_argument_location seloc]) | BridgeVariable (a,i) -> (tags @ [a], [i]) | FieldValue (sname,offset,fname) -> (tags, [bd#index_string sname; offset; bd#index_string fname]) @@ -233,7 +273,12 @@ object (self) | "ev" -> SyscallErrorReturnValue (t 1) | "fp" -> FunctionPointer (bd#get_string (a 0), bd#get_string (a 1), t 1) | "ct" -> CallTargetValue (id#get_call_target (a 0)) - | "se" -> SideEffectValue (t 1, bd#get_string (a 0), (a 1) = 1) + | "se" -> + SideEffectValue + (t 1, + bd#get_string (a 0), + (if (a 1) > 0 then Some (bcd#get_typ (a 1)) else None), + self#get_sideeffect_argument_location (a 2)) | "bv" -> BridgeVariable (t 1, a 0) | "fv" -> FieldValue (bd#get_string (a 0), a 1, bd#get_string (a 2)) | "sv" -> SymbolicValue (xd#get_xpr (a 0)) @@ -252,11 +297,15 @@ object (self) | RegisterSpill (offset, reg) -> (tags, [offset; bd#index_register reg]) | RegisterRestore (offset, reg) -> (tags, [offset; bd#index_register reg]) | StackLoad (var, offset, optsize, ty) -> - (tags, [self#xd#index_variable var; offset; oi optsize; bcd#index_typ ty]) + (tags, + [self#xd#index_variable var; + self#index_memory_offset offset; + oi optsize; + bcd#index_typ ty]) | StackStore (var, offset, optsize, ty, optxpr) -> (tags, [self#xd#index_variable var; - offset; + self#index_memory_offset offset; oi optsize; bcd#index_typ ty; ox optxpr]) diff --git a/CodeHawk/CHB/bchlib/bCHVarDictionary.mli b/CodeHawk/CHB/bchlib/bCHVarDictionary.mli index e1ac2afa..7b5300c9 100644 --- a/CodeHawk/CHB/bchlib/bCHVarDictionary.mli +++ b/CodeHawk/CHB/bchlib/bCHVarDictionary.mli @@ -6,7 +6,7 @@ Copyright (c) 2005-2019 Kestrel Technology LLC Copyright (c) 2020-2021 Henny Sipma - Copyright (c) 2022-2024 Aarno Labs LLC + Copyright (c) 2022-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 diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml index a9a8d99d..2fe72880 100644 --- a/CodeHawk/CHB/bchlib/bCHVariable.ml +++ b/CodeHawk/CHB/bchlib/bCHVariable.ml @@ -121,7 +121,7 @@ object (self:'a) "staticstub_" ^ (function_stub_to_string fs) | AppTarget a -> "tgt_" ^ a#to_hex_string | _ -> "tgt_qq_") - | SideEffectValue (address,arg,_) -> "se_" ^ address ^ "_" ^ arg + | SideEffectValue (address, arg, _, _) -> "se_" ^ address ^ "_" ^ arg | FieldValue (sname,offset,fname) -> sname ^ "." ^ fname ^ "_amp_" ^ (string_of_int offset) | SymbolicValue x -> "sv__" ^ (string_of_int (vard#xd#index_xpr x)) ^ "__sv" @@ -191,6 +191,7 @@ object (self:'a) | TypeCastValue (_, _, ty, _) -> Some ty | SyscallErrorReturnValue _ -> None | CallTargetValue _ -> None + | SideEffectValue (_, _, Some ty, _) -> Some ty | SideEffectValue _ -> None | FieldValue _ -> None | SymbolicValue _ -> None @@ -235,14 +236,12 @@ object (self:'a) method is_global_sideeffect = match denotation with - | AuxiliaryVariable (SideEffectValue (_, _, isglobal)) -> isglobal + | AuxiliaryVariable (SideEffectValue (_, _, _, SEGlobal _)) -> true | _ -> false method get_global_sideeffect_target_address: doubleword_result = match denotation with - | AuxiliaryVariable (SideEffectValue (_, arg, true)) -> - let addr_r = string_to_doubleword arg in - tprop addr_r (__FILE__ ^ ":" ^ (string_of_int __LINE__)) + | AuxiliaryVariable (SideEffectValue (_, _, _, SEGlobal dw)) -> Ok dw | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "Variable is not a global sideeffect value: " @@ -280,7 +279,7 @@ object (self:'a) method get_call_site: ctxt_iaddress_t traceresult = match denotation with | (AuxiliaryVariable (FunctionReturnValue a)) - | (AuxiliaryVariable (SideEffectValue (a, _, _))) -> Ok a + | (AuxiliaryVariable (SideEffectValue (a, _, _, _))) -> Ok a | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "Variable is not a function return value or sideeffect value: " @@ -288,7 +287,7 @@ object (self:'a) method get_se_argument_descriptor: string traceresult = match denotation with - | (AuxiliaryVariable (SideEffectValue (_, name, _))) -> Ok name + | (AuxiliaryVariable (SideEffectValue (_, name, _, _))) -> Ok name | _ -> Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " ^ "Variable is not a sideeffect value: " ^ self#get_name] @@ -643,6 +642,7 @@ object (self) | InitialRegisterValue (PowerSPRegister _, _) | InitialMemoryValue _ | FunctionReturnValue _ + | SideEffectValue _ | TypeCastValue _ -> Ok (memrefmgr#mk_basevar_reference v) | _ -> @@ -666,6 +666,11 @@ object (self) let memref = memrefmgr#mk_global_reference in self#make_memory_variable ~size memref offset + method make_local_stack_variable ?(size=4) ?(offset=NoOffset) (n:numerical_t) = + let offset = ConstantOffset (n, offset) in + let memref = memrefmgr#mk_local_stack_reference in + self#make_memory_variable ~size memref offset + method make_frozen_test_value (var:variable_t) (taddr:ctxt_iaddress_t) (jaddr:ctxt_iaddress_t) = self#mk_variable (AuxiliaryVariable (FrozenTestValue (var, taddr, jaddr))) @@ -693,9 +698,25 @@ object (self) method make_calltarget_value (tgt:call_target_t) = self#mk_variable (AuxiliaryVariable (CallTargetValue tgt)) - method make_side_effect_value - (iaddr:ctxt_iaddress_t) ?(global=false) (arg:string) = - self#mk_variable (AuxiliaryVariable (SideEffectValue (iaddr,arg,global))) + method make_global_sideeffect_value + ?(btype=None) + (iaddr: ctxt_iaddress_t) + (arg: string) + (gaddr: doubleword_int) = + let sev = SideEffectValue (iaddr, arg, btype, SEGlobal gaddr) in + self#mk_variable (AuxiliaryVariable sev) + + method make_stack_sideeffect_value + ?(btype=None) + (iaddr: ctxt_iaddress_t) + (arg: string) + (stackoffset: numerical_t) = + let sev = SideEffectValue (iaddr, arg, btype, SEStack stackoffset) in + self#mk_variable (AuxiliaryVariable sev) + + method make_side_effect_value (iaddr:ctxt_iaddress_t) (descr: string) (arg:string) = + let sev = SideEffectValue (iaddr, arg, None, SEDescr descr) in + self#mk_variable (AuxiliaryVariable sev) method make_field_value (sname:string) (offset:int) (fname:string) = self#mk_variable (AuxiliaryVariable (FieldValue (sname,offset,fname))) diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index 9fdb09da..3174c478 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20250722" - ~date:"2025-07-22" + ~version:"0.6.0_20250804" + ~date:"2025-08-04" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml index 28ba89a6..7935b433 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml @@ -1178,6 +1178,7 @@ object (self) let r0_op = arm_register_op AR0 RD in let xr0_r = r0_op#to_expr floc in let xxr0_r = TR.tmap rewrite_expr xr0_r in + let xxr0_r = TR.tmap (rewrite_in_cc_context floc c) xxr0_r in let cxr0_r = TR.tbind floc#convert_xpr_to_c_expr xxr0_r in let (tagstring, args) = mk_instrx_data_r () in let (tags, args) = add_optional_instr_condition tagstring args c in diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index 64f69a91..2574e3b2 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -156,7 +156,8 @@ object (self) let varinvs = floc#varinv#get_var_reaching_defs symvar in (match varinvs with | [vinv] -> vinv#get_reaching_defs - | _ -> []) in + | _ -> + List.concat (List.map (fun vinv -> vinv#get_reaching_defs) varinvs)) in let get_variable_rdefs_r (v_r: variable_t traceresult): symbol_t list = TR.tfold_default get_variable_rdefs [] v_r in @@ -175,6 +176,7 @@ object (self) let has_exit_use_r (v_r: variable_t traceresult): bool = TR.tfold_default has_exit_use false 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 -> @@ -185,10 +187,13 @@ object (self) (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 @@ -267,12 +272,13 @@ object (self) ^ " <: " ^ (type_term_to_string ty2)] in - let _log_rule_enabled (linenumber: int) (name: string) = + let log_type_constraint_rule_disabled + (linenumber: int) (name: string) (tc: type_constraint_t) = log_diagnostics_result - ~tag:("typing rule " ^ name ^ " enabled") + ~tag:("typing rule " ^ name ^ " disabled") __FILE__ linenumber - [(p2s floc#l#toPretty)] in + [(p2s floc#l#toPretty) ^ ": " ^ (type_constraint_to_string tc)] in let operand_is_zero (op: arm_operand_int): bool = (* Returns true if the value of the operand is known to be zero at @@ -341,18 +347,20 @@ object (self) let fvar = add_return_capability (mk_function_typevar faddr) in let tt_z = mk_vty_term tv_z in let fterm = mk_vty_term fvar in - let rule = mnem ^ "-freturn" in - begin - log_subtype_constraint __LINE__ rule tt_z fterm; - store#add_subtype_constraint faddr iaddr rule tt_z fterm - end) + let rule = mnem ^ "-exituse" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tt_z fterm; + store#add_subtype_constraint faddr iaddr rule tt_z fterm + end + else + log_subtype_rule_disabled __LINE__ rule tt_z fterm) else () in match instr#get_opcode with | Add (_, _, rd, rn, rm, _) -> - let xrn_r = rn#to_expr floc in begin (regvar_type_introduction "ADD" rd); (regvar_linked_to_exit "ADD" rd); @@ -381,19 +389,25 @@ object (self) let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let rndefs = get_variable_rdefs_r (rn#to_variable floc) in let rnreg = rn#to_register in - List.iter (fun rnsym -> - let rnaddr = rnsym#getBaseName in - let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in - let rntypeterm = mk_vty_term rntypevar in - let lhstypeterm = mk_vty_term lhstypevar in - let rule = "ADD-c" in - if fndata#is_typing_rule_disabled iaddr rule then - log_subtype_rule_disabled __LINE__ rule rntypeterm lhstypeterm - else - begin - log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule rntypeterm lhstypeterm - end) rndefs); + if rn#is_sp_register || rd#is_sp_register then + (* no information to be gained from stack pointer manipulations *) + () + else + List.iter (fun rnsym -> + let rnaddr = rnsym#getBaseName in + let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in + let rntypeterm = mk_vty_term rntypevar in + let lhstypeterm = mk_vty_term lhstypevar in + let rule = "ADD-c" in + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; + store#add_subtype_constraint + faddr iaddr rule rntypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rntypeterm lhstypeterm + ) rndefs); (match getopt_global_address_r (rn#to_expr floc) with | Some gaddr -> @@ -410,31 +424,22 @@ object (self) let rmtypeterm = mk_vty_term rmtypevar in let ctypeterm = mk_cty_term tyc in let rule = "ADD-global" in - begin - log_subtype_constraint - __LINE__ rule rmtypeterm ctypeterm; - store#add_subtype_constraint - faddr iaddr rule rmtypeterm ctypeterm - end) rmdefs + if fndata#is_typing_rule_enabled + ~rdef:(Some rmaddr) iaddr rule then + begin + log_subtype_constraint + __LINE__ rule rmtypeterm ctypeterm; + store#add_subtype_constraint + faddr iaddr rule rmtypeterm ctypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rmtypeterm ctypeterm + ) rmdefs | _ -> ()) else () - | _ -> ()); - - (match getopt_initial_argument_value_r xrn_r with - | Some (reg, _) -> - let ftvar = mk_function_typevar faddr in - let ftvar = add_freg_param_capability reg ftvar in - let rdreg = rd#to_register in - let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in - let fttypeterm = mk_vty_term ftvar in - let lhstypeterm = mk_vty_term lhstypevar in - let rule = "ADD-initv" in - begin - log_subtype_constraint __LINE__ rule fttypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule fttypeterm lhstypeterm - end | _ -> ()) + end | ArithmeticShiftRight (_, _, rd, rn, rm, _) when rm#is_immediate -> @@ -450,11 +455,14 @@ object (self) (let tc = mk_int_type_constant Signed 32 in let tctypeterm = mk_cty_term tc in let lhstypeterm = mk_vty_term lhstypevar in - let rule = "ASR-lhs-default" in - begin - log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm - end); + let rule = "ASR-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm lhstypeterm); (* ASR is applied to a signed integer *) (List.iter (fun rnrdef -> @@ -464,10 +472,14 @@ object (self) let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in let rule = "ASR-rdef" in - begin - log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm rntypeterm - end) rndefs) + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rntypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rntypeterm + ) rndefs) end | BitwiseAnd (_, _, rd, rn, _, _) -> @@ -485,10 +497,14 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let lhstypeterm = mk_vty_term lhstypevar in let rule = "AND-rdef" in - begin - log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule rntypeterm lhstypeterm - end) rndefs + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule rntypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rntypeterm lhstypeterm + ) rndefs end | BitwiseNot(_, _, rd, rm, _) when rm#is_immediate -> @@ -503,11 +519,14 @@ object (self) (* destination is an integer type *) (let tctypeterm = mk_cty_term tyc in let lhstypeterm = mk_vty_term lhstypevar in - let rule = "MVN-default" in - begin - log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm - end); + let rule = "MVN-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm lhstypeterm) end | BitwiseNot (_, _, rd, rm, _) -> @@ -525,14 +544,17 @@ object (self) let rmtypeterm = mk_vty_term rmtypevar in let lhstypeterm = mk_vty_term lhstypevar in let rule = "MVN-rdef" in - begin - log_subtype_constraint __LINE__ rule rmtypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule rmtypeterm lhstypeterm - end) rmdefs); - + if fndata#is_typing_rule_enabled ~rdef:(Some rmaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rmtypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule rmtypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rmtypeterm lhstypeterm + ) rmdefs) end - | BitwiseOr (_, _, rd, rn, _, _) -> + | BitwiseOr (_, _, rd, rn, rm, _) when rm#is_immediate -> let rdreg = rd#to_register in let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let rndefs = get_variable_rdefs_r (rn#to_variable floc) in @@ -547,10 +569,14 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let lhstypeterm = mk_vty_term lhstypevar in let rule = "ORR-rdef" in - begin - log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule rntypeterm lhstypeterm - end) rndefs + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule rntypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rntypeterm lhstypeterm + ) rndefs end | Branch _ -> @@ -602,13 +628,16 @@ object (self) end) | _ -> let opttc = mk_btype_constraint typevar rtype in - let rule = "BL-rv" in + let rule = "BL-sig-rv" in match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> begin log_no_type_constraint __LINE__ rule rtype; @@ -621,6 +650,7 @@ object (self) begin (if is_register_parameter p then let regarg = TR.tget_ok (get_register_parameter_register p) in + let regstr = BCHCPURegisters.register_to_string regarg in let pvar = floc#f#env#mk_register_variable regarg in let rdefs = get_variable_rdefs pvar in if not (is_unknown_type ptype) then @@ -628,23 +658,27 @@ object (self) let typevar = mk_reglhs_typevar regarg faddr rdsym#getBaseName in let opttc = mk_btype_constraint typevar ptype in - let rule = "BL-regarg" in - match opttc with - | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end - | _ -> - begin - log_no_type_constraint __LINE__ rule ptype; - () - end) rdefs + let rule = "BL-sig-regarg" in + match opttc with + | Some tc -> + if fndata#is_typing_rule_enabled + ~rdef:(Some regstr) 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 + | _ -> + begin + log_no_type_constraint __LINE__ rule ptype; + () + end) rdefs else () else if is_stack_parameter p then - let rule = "BL-stackarg" in + let rule = "BL-sig-stackarg" in (log_tfold_default (log_error ("Unable to retrieve stack offset from " @@ -661,10 +695,13 @@ object (self) let opttc = mk_btype_constraint typevar ptype in match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> ()) () (floc#get_singleton_stackpointer_offset))) @@ -695,13 +732,16 @@ object (self) let eltype = ptr_deref ptype in let atype = t_array eltype 1 in let opttc = mk_btype_constraint lhstypevar atype in - let rule = "BL-stackarg" in + let rule = "BL-sig-stackarg" in match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> ()) end ) callargs @@ -722,10 +762,14 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let immtypeterm = mk_cty_term immtypeconst in let rule = "CMP-rdef" in - begin - log_subtype_constraint __LINE__ rule rntypeterm immtypeterm; - store#add_subtype_constraint faddr iaddr rule rntypeterm immtypeterm - end) rndefs + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rntypeterm immtypeterm; + store#add_subtype_constraint faddr iaddr rule rntypeterm immtypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rntypeterm immtypeterm + ) rndefs | Compare (_, rn, rm, _) when rm#is_register -> let rndefs = get_variable_rdefs_r (rn#to_variable floc) in @@ -746,44 +790,18 @@ object (self) let rntypeterm = mk_vty_term rntypevar in let rmtypeterm = mk_vty_term rmtypevar in let rule = "CMP-rdef" in - begin - log_subtype_constraint __LINE__ rule rntypeterm rmtypeterm; - store#add_subtype_constraint faddr iaddr rule rntypeterm rmtypeterm - end) pairs); - - (let xrn_r = rn#to_expr floc in - match getopt_initial_argument_value_r xrn_r with - | Some (reg, _) -> - let ftvar = mk_function_typevar faddr in - let ftvar = add_freg_param_capability reg ftvar in - List.iter (fun rmsym -> - let rmaddr = rmsym#getBaseName in - let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in - let ftterm = mk_vty_term ftvar in - let rmtypeterm = mk_vty_term rmtypevar in - let rule = "CMP-init" in - begin - log_subtype_constraint __LINE__ rule ftterm rmtypeterm; - store#add_subtype_constraint faddr iaddr rule ftterm rmtypeterm - end) rmdefs - | _ -> ()); - - (let xrm_r = rm#to_expr floc in - match getopt_initial_argument_value_r xrm_r with - | Some (reg, _) -> - let ftvar = mk_function_typevar faddr in - let ftvar = add_freg_param_capability reg ftvar in - List.iter (fun rnsym -> - let rnaddr = rnsym#getBaseName in - let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in - let ftterm = mk_vty_term ftvar in - let rntypeterm = mk_vty_term rntypevar in - let rule = "CMP-init" in - begin - log_subtype_constraint __LINE__ rule ftterm rntypeterm; - store#add_subtype_constraint faddr iaddr rule ftterm rntypeterm - end) rndefs - | _ -> ()) + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + if fndata#is_typing_rule_enabled ~rdef:(Some rmaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rntypeterm rmtypeterm; + store#add_subtype_constraint + faddr iaddr rule rntypeterm rmtypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rntypeterm rmtypeterm + else + log_subtype_rule_disabled __LINE__ rule rntypeterm rmtypeterm + ) pairs); end | LoadRegister (_, rt, rn, rm, memop, _) when rm#is_immediate -> @@ -804,10 +822,13 @@ object (self) let opttc = mk_btype_constraint rttypevar t in (match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> ())) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) xtype_r); @@ -828,10 +849,16 @@ object (self) let rdtypeterm = mk_vty_term rdtypevar in let rttypeterm = mk_vty_term rttypevar in let rule = "LDR-load" in - begin - log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule rdtypeterm rttypeterm - end) xrdef); + if fndata#is_typing_rule_enabled + ~rdef:(Some ldaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; + store#add_subtype_constraint + faddr iaddr rule rdtypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rdtypeterm rttypeterm + ) xrdef); (* if the address to load from is the address of a global struct field, assign the type of that field to the destination register. *) @@ -859,10 +886,13 @@ object (self) let rule = "LDR-struct-field" in (match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> ()) | _ -> chlog#add @@ -903,10 +933,13 @@ object (self) let rule = "LDR-array" in (match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> ()) else () @@ -930,11 +963,15 @@ object (self) let rhstypeterm = mk_vty_term rhstypevar in let rttypeterm = mk_vty_term rttypevar in let rule = "LDR-stack-addr" in - begin - log_subtype_constraint - __LINE__ rule rhstypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule rhstypeterm rttypeterm - end) + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint + __LINE__ rule rhstypeterm rttypeterm; + store#add_subtype_constraint + faddr iaddr rule rhstypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rhstypeterm rttypeterm) end) end @@ -946,30 +983,41 @@ object (self) (regvar_linked_to_exit "LDRB" rt); (* LDRB rt, [rn, rm] : X_rndef.load <: X_rt *) - (let xrdefs = get_variable_rdefs_r (rn#to_variable floc) in - let rnreg = rn#to_register in - let offset = rm#to_numerical#toInt in - List.iter (fun rdsym -> - let ldaddr = rdsym#getBaseName in - let rdtypevar = mk_reglhs_typevar rnreg faddr ldaddr in - let rdtypevar = add_load_capability ~offset ~size:1 rdtypevar in - let rdtypeterm = mk_vty_term rdtypevar in - let rttypeterm = mk_vty_term rttypevar in - let rule = "LDRB-load" in - begin - log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule rdtypeterm rttypeterm - end) xrdefs); + (if rn#is_sp_register then + () + else + let xrdefs = get_variable_rdefs_r (rn#to_variable floc) in + let rnreg = rn#to_register in + let offset = rm#to_numerical#toInt in + List.iter (fun rdsym -> + let ldaddr = rdsym#getBaseName in + let rdtypevar = mk_reglhs_typevar rnreg faddr ldaddr in + let rdtypevar = add_load_capability ~offset ~size:1 rdtypevar in + let rdtypeterm = mk_vty_term rdtypevar in + let rttypeterm = mk_vty_term rttypevar in + let rule = "LDRB-load" in + if fndata#is_typing_rule_enabled ~rdef:(Some ldaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; + store#add_subtype_constraint + faddr iaddr rule rdtypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rdtypeterm rttypeterm + ) xrdefs); (* LDRB rt, ... : X_rt <: integer type *) (let tc = mk_int_type_constant Unsigned 8 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in - let rule = "LDRB-default" in - begin - log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm - end) + let rule = "LDRB-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rttypeterm) end @@ -984,11 +1032,14 @@ object (self) (let tc = mk_int_type_constant SignedNeutral 8 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in - let rule = "LDRB-default" in - begin - log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm - end) + let rule = "LDRB-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rttypeterm) end @@ -1010,10 +1061,13 @@ object (self) let rule = "LDRH-memop-tc" in (match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> ())) ~error:(fun e -> log_error_result __FILE__ __LINE__ e) xtype_r); @@ -1029,10 +1083,14 @@ object (self) let rdtypeterm = mk_vty_term rdtypevar in let rttypeterm = mk_vty_term rttypevar in let rule = "LDRH-load" in - begin - log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule rdtypeterm rttypeterm - end) xrdef) + if fndata#is_typing_rule_enabled ~rdef:(Some ldaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rdtypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule rdtypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rdtypeterm rttypeterm + ) xrdef) end | LoadRegisterHalfword (_, rt, _, _, _, _) -> @@ -1046,12 +1104,14 @@ object (self) (let tc = mk_int_type_constant SignedNeutral 16 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in - let rule = "LDRH-default" in - begin - log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm - end) - + let rule = "LDRH-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rttypeterm) end | LogicalShiftLeft (_, _, rd, rn, rm, _) when rm#is_immediate -> @@ -1067,46 +1127,54 @@ object (self) (let tc = mk_int_type_constant Unsigned 32 in let tcterm = mk_cty_term tc in let lhstypeterm = mk_vty_term lhstypevar in - let rule = "LSL-default" in - begin - log_subtype_constraint __LINE__ rule tcterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule tcterm lhstypeterm - end); + let rule = "LSL-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tcterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tcterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tcterm lhstypeterm); (* LSL is applied to an unsigned integer *) - (let rule = "LSL-default" in + (let rule = "LSL-rdef" in List.iter (fun rnrdef -> let rnaddr = rnrdef#getBaseName in let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in let tyc = mk_int_type_constant Unsigned 32 in let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in - begin - log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm rntypeterm - end) rndefs) + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rntypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rntypeterm + ) rndefs) end - - | LogicalShiftRight (_, _, rd, _rn, rm, _) when rm#is_immediate -> - (* + | LogicalShiftRight (_, _, rd, rn, rm, _) when rm#is_immediate -> let rdreg = rd#to_register in let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let rnreg = rn#to_register in let rndefs = get_variable_rdefs_r (rn#to_variable floc) in - *) begin (regvar_type_introduction "LSR" rd); (regvar_linked_to_exit "LSR" rd); - (* + (* LSR results in an unsigned integer *) (let tc = mk_int_type_constant Unsigned 32 in let tcterm = mk_cty_term tc in let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint __LINE__ "LSR-lhs" tcterm lhstypeterm; - store#add_subtype_constraint tcterm lhstypeterm - end); + let rule = "LSR-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tcterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tcterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tcterm lhstypeterm); (* LSR is applied to an unsigned integer *) (List.iter (fun rnrdef -> @@ -1115,11 +1183,16 @@ object (self) let tyc = mk_int_type_constant Unsigned 32 in let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in - begin - log_subtype_constraint __LINE__ "LSR-rhs" tctypeterm rntypeterm; - store#add_subtype_constraint tctypeterm rntypeterm - end) rndefs) - *) + let rule = "LSR-rdef" in + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rntypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rntypeterm + ) rndefs) + end | Move (_, _, rd, rm, _, _) when rm#is_immediate -> @@ -1138,10 +1211,13 @@ object (self) let lhstypeterm = mk_vty_term lhstypevar in let tctypeterm = mk_cty_term tyc in let rule = "MOV-c" in - begin - log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm - end) + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm lhstypeterm) end | Move (_, _, rd, rm, _, _) when rd#get_register = rm#get_register -> @@ -1173,15 +1249,18 @@ object (self) let rule = "MOV-rdef" in List.iter (fun rmrdef -> let rmaddr = rmrdef#getBaseName in - if rmaddr != "init" then - let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in - let rmtypeterm = mk_vty_term rmtypevar in - let lhstypeterm = mk_vty_term lhstypevar in + let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in + let rmtypeterm = mk_vty_term rmtypevar in + let lhstypeterm = mk_vty_term lhstypevar in + if fndata#is_typing_rule_enabled ~rdef:(Some rmaddr) iaddr rule then begin log_subtype_constraint __LINE__ rule rmtypeterm lhstypeterm; store#add_subtype_constraint faddr iaddr rule rmtypeterm lhstypeterm - end) rmrdefs) + end + else + log_subtype_rule_disabled __LINE__ rule rmtypeterm lhstypeterm + ) rmrdefs) end | Pop (_, _, rl, _) when rl#includes_pc -> @@ -1200,13 +1279,16 @@ object (self) begin (* use function return type *) (let opttc = mk_btype_constraint typevar rtype in - let rule = "POP-rv" in + let rule = "POP-sig-rv" in match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> begin log_no_type_constraint __LINE__ rule rtype; @@ -1219,15 +1301,18 @@ object (self) let rule = "POP-rdef" in List.iter (fun r0def -> let r0addr = r0def#getBaseName in - if r0addr != "init" then - let r0typevar = mk_reglhs_typevar reg faddr r0addr in - let r0typeterm = mk_vty_term r0typevar in - let lhstypeterm = mk_vty_term typevar in + let r0typevar = mk_reglhs_typevar reg faddr r0addr in + let r0typeterm = mk_vty_term r0typevar in + let lhstypeterm = mk_vty_term typevar in + if fndata#is_typing_rule_enabled ~rdef:(Some r0addr) iaddr rule then begin log_subtype_constraint __LINE__ rule r0typeterm lhstypeterm; store#add_subtype_constraint faddr iaddr rule r0typeterm lhstypeterm - end) r0defs) + end + else + log_subtype_rule_disabled __LINE__ rule r0typeterm lhstypeterm + ) r0defs) end) | Push _ @@ -1235,7 +1320,7 @@ object (self) (* no type information gained *) () - | ReverseSubtract (_, _, rd, _, rm, _) -> + | ReverseSubtract (_, _, rd, _, rm, _) when rm#is_register -> let rdreg = rd#to_register in let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in let rmdefs = get_variable_rdefs_r (rm#to_variable floc) in @@ -1250,10 +1335,14 @@ object (self) let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in let rmtypeterm = mk_vty_term rmtypevar in let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint __LINE__ rule rmtypeterm lhstypeterm; - store#add_subtype_constraint faddr iaddr rule rmtypeterm lhstypeterm - end) rmdefs); + if fndata#is_typing_rule_enabled ~rdef:(Some rmaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rmtypeterm lhstypeterm; + store#add_subtype_constraint faddr iaddr rule rmtypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rmtypeterm lhstypeterm + ) rmdefs); end | SignedMultiplyLong (_, _, rdlo, rdhi, rn, rm) -> @@ -1270,31 +1359,51 @@ object (self) let tctypeterm = mk_cty_term tc in let lhslotypeterm = mk_vty_term lhslotypevar in let lhshitypeterm = mk_vty_term lhshitypevar in - let rule1 = "SMULL-default" in + let rule1 = "SMULL-def-lhs" in let rule2 = "SMULL-rdef" in begin - log_subtype_constraint __LINE__ rule1 tctypeterm lhslotypeterm; - log_subtype_constraint __LINE__ rule1 tctypeterm lhshitypeterm; - store#add_subtype_constraint faddr iaddr rule1 tctypeterm lhslotypeterm; - store#add_subtype_constraint faddr iaddr rule1 tctypeterm lhshitypeterm; + + (if fndata#is_typing_rule_enabled iaddr rule1 then + begin + log_subtype_constraint __LINE__ rule1 tctypeterm lhslotypeterm; + store#add_subtype_constraint faddr iaddr rule1 tctypeterm lhslotypeterm + end + else + log_subtype_rule_disabled __LINE__ rule1 tctypeterm lhslotypeterm); + + (if fndata#is_typing_rule_enabled iaddr rule1 then + begin + log_subtype_constraint __LINE__ rule1 tctypeterm lhshitypeterm; + store#add_subtype_constraint faddr iaddr rule1 tctypeterm lhshitypeterm + end + else + log_subtype_rule_disabled __LINE__ rule1 tctypeterm lhshitypeterm); (List.iter (fun rnrdef -> let rnaddr = rnrdef#getBaseName in let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in let rntypeterm = mk_vty_term rntypevar in - begin - log_subtype_constraint __LINE__ rule2 tctypeterm rntypeterm; - store#add_subtype_constraint faddr iaddr rule2 tctypeterm rntypeterm - end) rndefs); + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule2 then + begin + log_subtype_constraint __LINE__ rule2 tctypeterm rntypeterm; + store#add_subtype_constraint faddr iaddr rule2 tctypeterm rntypeterm + end + else + log_subtype_rule_disabled __LINE__ rule2 tctypeterm rntypeterm + ) rndefs); (List.iter (fun rmrdef -> let rmaddr = rmrdef#getBaseName in let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in let rmtypeterm = mk_vty_term rmtypevar in - begin - log_subtype_constraint __LINE__ rule2 tctypeterm rmtypeterm; - store#add_subtype_constraint faddr iaddr rule2 tctypeterm rmtypeterm - end) rmdefs) + if fndata#is_typing_rule_enabled ~rdef:(Some rmaddr) iaddr rule2 then + begin + log_subtype_constraint __LINE__ rule2 tctypeterm rmtypeterm; + store#add_subtype_constraint faddr iaddr rule2 tctypeterm rmtypeterm + end + else + log_subtype_rule_disabled __LINE__ rule2 tctypeterm rmtypeterm + ) rmdefs) end (* Store x in y --- *y := x --- X <: Y.store *) @@ -1305,28 +1414,13 @@ object (self) let rtrdefs = get_variable_rdefs_r (rt#to_variable floc) in let rtreg = rt#to_register in let xaddr_r = memvarop#to_address floc in - let xrt_r = rt#to_expr floc in begin (match getopt_stackaddress_r xaddr_r with | None -> () - | Some offset -> - let lhstypevar = mk_localstack_lhs_typevar offset faddr iaddr in + | Some spoffset -> + let lhstypevar = mk_localstack_lhs_typevar spoffset faddr iaddr in begin - (* propagate function argument type *) - (match getopt_initial_argument_value_r xrt_r with - | Some (rtreg, off) when off = 0 -> - let rhstypevar = mk_function_typevar faddr in - let rhstypevar = add_freg_param_capability rtreg rhstypevar in - let rhstypeterm = mk_vty_term rhstypevar in - let lhstypeterm = mk_vty_term lhstypevar in - let rule = "STR-init" in - begin - log_subtype_constraint __LINE__ rule rhstypeterm lhstypeterm; - store#add_subtype_constraint - faddr iaddr rule rhstypeterm lhstypeterm - end - | _ -> ()); (* propagate src register type from rdefs *) (let rtreg = rt#to_register in @@ -1335,49 +1429,86 @@ object (self) let rule = "STR-rdef" in List.iter (fun rtrdef -> let rtaddr = rtrdef#getBaseName in - if rtaddr != "init" then - let rttypevar = mk_reglhs_typevar rtreg faddr rtaddr in - let rttypeterm = mk_vty_term rttypevar in - let lhstypeterm = mk_vty_term lhstypevar in + let rttypevar = mk_reglhs_typevar rtreg faddr rtaddr in + let rttypeterm = mk_vty_term rttypevar in + let lhstypeterm = mk_vty_term lhstypevar in + if fndata#is_typing_rule_enabled + ~rdef:(Some rtaddr) iaddr rule then begin log_subtype_constraint __LINE__ rule rttypeterm lhstypeterm; store#add_subtype_constraint faddr iaddr rule rttypeterm lhstypeterm - end) rtrdefs); - - (* import type from stackvar-introductions *) - (match get_stackvar_type_annotation offset with - | None -> () - | Some t -> - let lhstypevar = - mk_localstack_lhs_typevar offset faddr iaddr in - let opttc = mk_btype_constraint lhstypevar t in - (match opttc with - | Some tc -> - let rule = "STR-svintro" in - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end - | _ -> ())) + end + else + log_subtype_rule_disabled __LINE__ rule rttypeterm lhstypeterm + ) rtrdefs); + + (* import type from stackvar-introductions *) + (match get_stackvar_type_annotation spoffset with + | None -> () + | Some t -> + let lhstypevar = + mk_localstack_lhs_typevar spoffset faddr iaddr in + let opttc = mk_btype_constraint lhstypevar t in + let rule = "STR-svintro" in + (match opttc with + | Some tc -> + begin + log_type_constraint __LINE__ rule tc; + store#add_constraint faddr iaddr rule tc + end + | _ -> + log_no_type_constraint __LINE__ rule t)) end); (let rule = "STR-store" in - List.iter (fun rndsym -> - let straddr = rndsym#getBaseName in - let rntypevar = mk_reglhs_typevar rnreg faddr straddr in - let rntypevar = add_store_capability ~size:4 ~offset rntypevar in + if rn#is_sp_register then + () + else + List.iter (fun rndsym -> + let straddr = rndsym#getBaseName in + let rntypevar = mk_reglhs_typevar rnreg faddr straddr in + let rntypevar = add_store_capability ~size:4 ~offset rntypevar in + List.iter (fun rtdsym -> + let rtdloc = rtdsym#getBaseName in + let rttypevar = mk_reglhs_typevar rtreg faddr rtdloc in + let rttypeterm = mk_vty_term rttypevar in + let rntypeterm = mk_vty_term rntypevar in + if fndata#is_typing_rule_enabled + ~rdef:(Some rtdloc) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rttypeterm rntypeterm; + store#add_subtype_constraint + faddr iaddr rule rttypeterm rntypeterm + end + else + 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 rule = "STR-memop-tc" in + TR.titer + ~ok:(fun t -> List.iter (fun rtdsym -> let rtdloc = rtdsym#getBaseName in let rttypevar = mk_reglhs_typevar rtreg faddr rtdloc in - let rttypeterm = mk_vty_term rttypevar in - let rntypeterm = mk_vty_term rntypevar in - begin - log_subtype_constraint __LINE__ rule rttypeterm rntypeterm; - store#add_subtype_constraint - faddr iaddr rule rttypeterm rntypeterm - end) rtrdefs) rnrdefs) + let opttc = mk_btype_constraint rttypevar t in + match opttc with + | Some tc -> + 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 + | _ -> ()) rtrdefs) + ~error:(fun e -> log_error_result __FILE__ __LINE__ e) + vtype_r) + end | StoreRegisterByte (_, rt, rn, rm, _memvarop, _) when rm#is_immediate -> @@ -1394,11 +1525,14 @@ object (self) let tc = mk_int_type_constant SignedNeutral 8 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in - let rule = "STRB-default" in - begin - log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm - end); + let rule = "STRB-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rttypeterm); (let rule = "STRB-rdef" in List.iter (fun rndsym -> @@ -1410,11 +1544,21 @@ object (self) let rttypevar = mk_reglhs_typevar rtreg faddr rtdloc in let rttypeterm = mk_vty_term rttypevar in let rntypeterm = mk_vty_term rntypevar in - begin - log_subtype_constraint __LINE__ rule rttypeterm rntypeterm; - store#add_subtype_constraint - faddr iaddr rule rttypeterm rntypeterm - end) rtrdefs) rnrdefs) + if fndata#is_typing_rule_enabled + ~rdef:(Some straddr) iaddr rule then + if fndata#is_typing_rule_enabled + ~rdef:(Some rtdloc) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rttypeterm rntypeterm; + store#add_subtype_constraint + faddr iaddr rule rttypeterm rntypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rttypeterm rntypeterm + else + log_subtype_rule_disabled __LINE__ rule rttypeterm rntypeterm + ) rtrdefs + ) rnrdefs) end @@ -1427,11 +1571,14 @@ object (self) (let tc = mk_int_type_constant SignedNeutral 8 in let tctypeterm = mk_cty_term tc in let rttypeterm = mk_vty_term rttypevar in - let rule = "STRB-default" in - begin - log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; - store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm - end) + let rule = "STRB-def-lhs" in + if fndata#is_typing_rule_enabled iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rttypeterm; + store#add_subtype_constraint faddr iaddr rule tctypeterm rttypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rttypeterm) end @@ -1458,11 +1605,15 @@ object (self) let rntypevar = mk_reglhs_typevar rnreg faddr rnaddr in let rntypeterm = mk_vty_term rntypevar in let lhstypeterm = mk_vty_term lhstypevar in - begin - log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; - store#add_subtype_constraint - faddr iaddr rule rntypeterm lhstypeterm - end) rndefs); + if fndata#is_typing_rule_enabled ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule rntypeterm lhstypeterm; + store#add_subtype_constraint + faddr iaddr rule rntypeterm lhstypeterm + end + else + log_subtype_rule_disabled __LINE__ rule rntypeterm lhstypeterm + ) rndefs); end @@ -1482,12 +1633,17 @@ object (self) let tyc = mk_int_type_constant Unsigned 32 in let tctypeterm = mk_cty_term tyc in let rntypeterm = mk_vty_term rntypevar in - let rule = "UBFX-default" in - begin - log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; - store#add_subtype_constraint - faddr iaddr rule tctypeterm rntypeterm - end) rndefs) + let rule = "UBFX-rdef" in + if fndata#is_typing_rule_enabled + ~rdef:(Some rnaddr) iaddr rule then + begin + log_subtype_constraint __LINE__ rule tctypeterm rntypeterm; + store#add_subtype_constraint + faddr iaddr rule tctypeterm rntypeterm + end + else + log_subtype_rule_disabled __LINE__ rule tctypeterm rntypeterm + ) rndefs) end | _ -> ()) end @@ -1500,13 +1656,16 @@ object (self) (regvar_linked_to_exit "UXTH" rd); (let opttc = mk_btype_constraint rdtypevar t_short in - let rule = "UBFX-default" in + let rule = "UBFX-def-lhs" in (match opttc with | Some tc -> - begin - log_type_constraint __LINE__ rule tc; - store#add_constraint faddr iaddr rule tc - end + 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 | _ -> ())); end diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml index 52465e0e..8f91dd52 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml @@ -711,22 +711,45 @@ let translate_arm_instruction else register_of_arm_register AR0 in let returnvar = floc#f#env#mk_register_variable returnreg in - let (usecmds, use) = - List.fold_left (fun (acccmds, accuse) (p, _x) -> + let (usecmds, use, usehigh) = + List.fold_left (fun (acccmds, accuse, accusehigh) (p, x) -> + let ptype = get_parameter_type p in + let addressedvars = + if is_pointer ptype then + let xx = rewrite_expr floc x in + match BCHARMDisassemblyUtils.get_string_reference floc xx with + | Some _ -> [] + | _ -> + match xx with + | XVar _ -> [] + | _ -> + TR.tfold + ~ok:(fun v -> [v]) + ~error:(fun e -> + let _ = log_dc_error_result __FILE__ __LINE__ e in + []) + (floc#get_var_at_address ~btype:(ptr_deref ptype) xx) + else + [] in if is_register_parameter p then let regarg = TR.tget_ok (get_register_parameter_register p) in let pvar = floc#f#env#mk_register_variable regarg in - (acccmds, pvar :: accuse) + (acccmds, + pvar :: (addressedvars @ accuse), + addressedvars @ accusehigh) + else if is_stack_parameter p then let p_offset = TR.tget_ok (get_stack_parameter_offset p) in let stackop = arm_sp_deref ~with_offset:p_offset RD in TR.tfold ~ok:(fun (stacklhs, stacklhscmds) -> - (stacklhscmds @ acccmds, stacklhs :: accuse)) + (stacklhscmds @ acccmds, + stacklhs :: (addressedvars @ accuse), + addressedvars @ accusehigh)) ~error:(fun e -> begin log_error_result __FILE__ __LINE__ e; - (acccmds, accuse) + (acccmds, accuse, accusehigh) end) (stackop#to_lhs floc) else @@ -735,8 +758,8 @@ let translate_arm_instruction (LBLOCK [ floc#l#toPretty; STR " Parameter type not recognized in call translation"]))) - ([], []) callargs in - let usehigh = get_use_high_vars (List.map snd callargs) in + ([], [], []) callargs in + let usehigh = usehigh @ (get_use_high_vars (List.map snd callargs)) in let vr1 = floc#f#env#mk_arm_register_variable AR1 in let vr2 = floc#f#env#mk_arm_register_variable AR2 in let vr3 = floc#f#env#mk_arm_register_variable AR3 in @@ -2523,6 +2546,11 @@ let translate_arm_instruction let cmds = TR.tfold ~ok:(fun rhsvar -> + let rhsreg = TR.tget_ok (finfo#env#get_register rhsvar) in + let _ = + if floc#has_initial_value rhsvar then + finfo#stackframe#add_register_spill + ~offset:off rhsreg floc#cia in let stackop = arm_sp_deref ~with_offset:off WR in TR.tfold ~ok:(fun (stacklhs, stacklhscmds) -> diff --git a/CodeHawk/CHB/bchlibx86/bCHPredefinedUtil.ml b/CodeHawk/CHB/bchlibx86/bCHPredefinedUtil.ml index 479ef736..d36cdc6a 100644 --- a/CodeHawk/CHB/bchlibx86/bCHPredefinedUtil.ml +++ b/CodeHawk/CHB/bchlibx86/bCHPredefinedUtil.ml @@ -514,7 +514,8 @@ let get_esp_adjustment_assign (summary: function_summary_int) (floc: floc_int) = let get_side_effects summary floc = - floc#get_sideeffect_assigns summary#get_function_semantics + let termev = BCHFloc.default_bterm_evaluator floc#f [] in + floc#get_sideeffect_assigns termev summary#get_function_semantics class virtual predefined_callsemantics_base_t (md5hash:string) (instrs:int) =