From c000fae94705b2001d8dfab960800e9e4764c130 Mon Sep 17 00:00:00 2001 From: Dulma Churchill Date: Fri, 19 Jun 2020 08:33:32 -0700 Subject: [PATCH] [biabduction] Delete POINTER_SIZE_MISMATCH Summary: Deleting this check that it's unused. Reviewed By: skcho Differential Revision: D22135709 fbshipit-source-id: d09eacf7a --- infer/man/man1/infer-full.txt | 1 - infer/man/man1/infer-report.txt | 1 - infer/man/man1/infer.txt | 1 - infer/src/absint/Localise.ml | 13 ------ infer/src/absint/Localise.mli | 3 -- infer/src/base/IssueType.ml | 4 -- infer/src/base/IssueType.mli | 2 - infer/src/biabduction/Exceptions.ml | 4 -- infer/src/biabduction/Exceptions.mli | 2 - infer/src/biabduction/Prover.ml | 5 --- infer/src/biabduction/Prover.mli | 6 --- infer/src/biabduction/Rearrange.ml | 60 +--------------------------- 12 files changed, 1 insertion(+), 101 deletions(-) diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 98a950b40..04593e8e0 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -472,7 +472,6 @@ OPTIONS NULLPTR_DEREFERENCE (disabled by default), NULL_DEREFERENCE (enabled by default), PARAMETER_NOT_NULL_CHECKED (enabled by default), - POINTER_SIZE_MISMATCH (enabled by default), POINTER_TO_CONST_OBJC_CLASS (enabled by default), PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 760c4b7b3..69081736c 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -197,7 +197,6 @@ OPTIONS NULLPTR_DEREFERENCE (disabled by default), NULL_DEREFERENCE (enabled by default), PARAMETER_NOT_NULL_CHECKED (enabled by default), - POINTER_SIZE_MISMATCH (enabled by default), POINTER_TO_CONST_OBJC_CLASS (enabled by default), PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 7620ce269..8842f2aa4 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -472,7 +472,6 @@ OPTIONS NULLPTR_DEREFERENCE (disabled by default), NULL_DEREFERENCE (enabled by default), PARAMETER_NOT_NULL_CHECKED (enabled by default), - POINTER_SIZE_MISMATCH (enabled by default), POINTER_TO_CONST_OBJC_CLASS (enabled by default), PRECONDITION_NOT_FOUND (enabled by default), PRECONDITION_NOT_MET (enabled by default), diff --git a/infer/src/absint/Localise.ml b/infer/src/absint/Localise.ml index f1ebbbd3d..c9aac89aa 100644 --- a/infer/src/absint/Localise.ml +++ b/infer/src/absint/Localise.ml @@ -245,19 +245,6 @@ let deref_str_dangling dangling_kind_opt = ; problem_str= "could be dangling and is dereferenced or freed" } -(** dereference strings for a pointer size mismatch *) -let deref_str_pointer_size_mismatch typ_from_instr typ_of_object = - let str_from_typ typ = - let pp f = Typ.pp_full Pp.text f typ in - F.asprintf "%t" pp - in - { tags= Tags.create () - ; value_pre= Some (pointer_or_object ()) - ; value_post= Some ("of type " ^ str_from_typ typ_from_instr) - ; problem_str= "could be used to access an object of smaller type " ^ str_from_typ typ_of_object - } - - (** dereference strings for an array out of bound access *) let deref_str_array_bound size_opt index_opt = let tags = Tags.create () in diff --git a/infer/src/absint/Localise.mli b/infer/src/absint/Localise.mli index 0ed6651e3..7828813f1 100644 --- a/infer/src/absint/Localise.mli +++ b/infer/src/absint/Localise.mli @@ -81,9 +81,6 @@ val deref_str_array_bound : IntLit.t option -> IntLit.t option -> deref_str val deref_str_nil_argument_in_variadic_method : Procname.t -> int -> int -> deref_str (** dereference strings for nonterminal nil arguments in c/objc variadic methods *) -val deref_str_pointer_size_mismatch : Typ.t -> Typ.t -> deref_str -(** dereference strings for a pointer size mismatch *) - (** type of access *) type access = | Last_assigned of int * bool (** line, null_case_flag *) diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index ea35d8ceb..f850c774f 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -775,10 +775,6 @@ let parameter_not_null_checked = ~user_documentation:[%blob "../../documentation/issues/PARAMETER_NOT_NULL_CHECKED.md"] -let pointer_size_mismatch = - register ~id:"POINTER_SIZE_MISMATCH" Error Biabduction (* TODO *) ~user_documentation:"" - - let _pointer_to_const_objc_class = register ~id:"POINTER_TO_CONST_OBJC_CLASS" Warning Linters ~user_documentation:[%blob "../../documentation/issues/POINTER_TO_CONST_OBJC_CLASS.md"] diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 3f9f362df..e6bff623a 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -276,8 +276,6 @@ val nullptr_dereference : t val parameter_not_null_checked : t -val pointer_size_mismatch : t - val precondition_not_found : t val precondition_not_met : t diff --git a/infer/src/biabduction/Exceptions.ml b/infer/src/biabduction/Exceptions.ml index ae8ba1573..16c099e6c 100644 --- a/infer/src/biabduction/Exceptions.ml +++ b/infer/src/biabduction/Exceptions.ml @@ -61,8 +61,6 @@ exception Null_dereference of Localise.error_desc * L.ocaml_pos exception Parameter_not_null_checked of Localise.error_desc * L.ocaml_pos -exception Pointer_size_mismatch of Localise.error_desc * L.ocaml_pos - exception Precondition_not_found of Localise.error_desc * L.ocaml_pos exception Precondition_not_met of Localise.error_desc * L.ocaml_pos @@ -129,8 +127,6 @@ let recognize_exception exn : IssueToReport.t = {issue_type= IssueType.field_not_null_checked; description= desc; ocaml_pos= Some ocaml_pos} | Null_dereference (desc, ocaml_pos) -> {issue_type= IssueType.null_dereference; description= desc; ocaml_pos= Some ocaml_pos} - | Pointer_size_mismatch (desc, ocaml_pos) -> - {issue_type= IssueType.pointer_size_mismatch; description= desc; ocaml_pos= Some ocaml_pos} | Inherently_dangerous_function desc -> {issue_type= IssueType.inherently_dangerous_function; description= desc; ocaml_pos= None} | Internal_error desc -> diff --git a/infer/src/biabduction/Exceptions.mli b/infer/src/biabduction/Exceptions.mli index 7e1e95a10..c506cd60d 100644 --- a/infer/src/biabduction/Exceptions.mli +++ b/infer/src/biabduction/Exceptions.mli @@ -60,8 +60,6 @@ exception Null_dereference of Localise.error_desc * Logging.ocaml_pos exception Parameter_not_null_checked of Localise.error_desc * Logging.ocaml_pos -exception Pointer_size_mismatch of Localise.error_desc * Logging.ocaml_pos - exception Precondition_not_found of Localise.error_desc * Logging.ocaml_pos exception Precondition_not_met of Localise.error_desc * Logging.ocaml_pos diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 563ea6806..ed9955b23 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -228,11 +228,6 @@ let type_size_compare t1 t2 = None -(** Check <= on the size of comparable types *) -let check_type_size_leq t1 t2 = - match type_size_compare t1 t2 with None -> false | Some n -> n <= 0 - - (** Check < on the size of comparable types *) let check_type_size_lt t1 t2 = match type_size_compare t1 t2 with None -> false | Some n -> n < 0 diff --git a/infer/src/biabduction/Prover.mli b/infer/src/biabduction/Prover.mli index 07a132ad1..1f8f6ec65 100644 --- a/infer/src/biabduction/Prover.mli +++ b/infer/src/biabduction/Prover.mli @@ -26,12 +26,6 @@ val check_equal : Tenv.t -> Prop.normal Prop.t -> Exp.t -> Exp.t -> bool val check_disequal : Tenv.t -> Prop.normal Prop.t -> Exp.t -> Exp.t -> bool (** Check whether [prop |- exp1!=exp2]. Result [false] means "don't know". *) -val type_size_comparable : Typ.t -> Typ.t -> bool -(** Return true if the two types have sizes which can be compared *) - -val check_type_size_leq : Typ.t -> Typ.t -> bool -(** Check <= on the size of comparable types *) - val check_atom : Tenv.t -> Prop.normal Prop.t -> atom -> bool (** Check whether [prop |- a]. Result [false] means "don't know". *) diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index a055be874..368b28414 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -964,63 +964,6 @@ let iter_rearrange_pe_dllseg_last tenv recurse_on_iters default_case_iter iter p recurse_on_iters iter_subcases -(** find the type at the offset from the given type expression, if any *) -let type_at_offset tenv texp off = - let rec strip_offset (off : Predicates.offset list) (typ : Typ.t) = - match (off, typ.desc) with - | [], _ -> - Some typ - | Off_fld (f, _) :: off', Tstruct name -> ( - match Tenv.lookup tenv name with - | Some {fields} -> ( - match List.find ~f:(fun (f', _, _) -> Fieldname.equal f f') fields with - | Some (_, typ', _) -> - strip_offset off' typ' - | None -> - None ) - | None -> - None ) - | Off_index _ :: off', Tarray {elt= typ'} -> - strip_offset off' typ' - | _ -> - None - in - match texp with Exp.Sizeof {typ} -> strip_offset off typ | _ -> None - - -(** Check that the size of a type coming from an instruction does not exceed the size of the type - from the pointsto predicate For example, that a pointer to int is not used to assign to a char *) -let check_type_size {InterproceduralAnalysis.proc_desc; err_log; tenv} pname prop texp off - typ_from_instr = - L.d_strln ~color:Orange "check_type_size" ; - L.d_str "off: " ; - Predicates.d_offset_list off ; - L.d_ln () ; - L.d_str "typ_from_instr: " ; - Typ.d_full typ_from_instr ; - L.d_ln () ; - match type_at_offset tenv texp off with - | Some typ_of_object -> - L.d_str "typ_o: " ; - Typ.d_full typ_of_object ; - L.d_ln () ; - if - Prover.type_size_comparable typ_from_instr typ_of_object - && not (Prover.check_type_size_leq typ_from_instr typ_of_object) - then - let deref_str = Localise.deref_str_pointer_size_mismatch typ_from_instr typ_of_object in - let loc = AnalysisState.get_loc_exn () in - let exn = - Exceptions.Pointer_size_mismatch - (Errdesc.explain_dereference pname tenv deref_str prop loc, __POS__) - in - BiabductionReporting.log_issue_deprecated_using_state proc_desc err_log exn - | None -> - L.d_str "texp: " ; - Exp.d_texp_full texp ; - L.d_ln () - - (** Exposes lexp |->- from iter. In case that it is not possible to * expose lexp |->-, this function prints an error message and * faults. There are four things to note. First, typ is the type of the * root of lexp. Second, prop should mean the same as iter. Third, the * result [] @@ -1116,8 +1059,7 @@ let rec iter_rearrange analysis_data pname tenv lexp typ_from_instr prop iter in [default_case_iter iter] | Some iter -> ( match Prop.prop_iter_current tenv iter with - | Predicates.Hpointsto (_, _, texp), off -> - if Config.type_size then check_type_size analysis_data pname prop texp off typ_from_instr ; + | Predicates.Hpointsto (_, _, _), _ -> iter_rearrange_ptsto analysis_data pname tenv prop iter lexp inst | Predicates.Hlseg (Lseg_NE, para, e1, e2, elist), _ -> iter_rearrange_ne_lseg tenv recurse_on_iters iter para e1 e2 elist