From 6a922ff597fda43ff9274f40b3bec9c815e60bcd Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Tue, 27 Oct 2015 07:41:28 -0700 Subject: [PATCH] Print origin information for procedured modelled internally. Reviewed By: jvillard Differential Revision: D2585242 fb-gh-sync-id: 31b5834 --- infer/src/backend/utils.ml | 6 +++- infer/src/backend/utils.mli | 3 ++ infer/src/checkers/eradicateChecks.ml | 4 +-- infer/src/checkers/modelTables.ml | 3 ++ infer/src/checkers/modelTables.mli | 5 ++++ infer/src/checkers/typeAnnotation.ml | 4 +-- infer/src/checkers/typeCheck.ml | 8 +++++- infer/src/checkers/typeOrigin.ml | 41 ++++++++++++++++++--------- infer/src/checkers/typeOrigin.mli | 11 +++++-- 9 files changed, 62 insertions(+), 23 deletions(-) diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml index 9d6dc9524..c461946ed 100644 --- a/infer/src/backend/utils.ml +++ b/infer/src/backend/utils.ml @@ -240,9 +240,13 @@ let pp_elapsed_time fmt () = (** Type of location in ml source: file,line,column *) type ml_location = string * int * int +(** String describing the file of an ml location *) +let ml_location_file_string ((file: string), (line: int), (column: int)) = + "file " ^ file + (** Turn an ml location into a string *) let ml_location_string ((file: string), (line: int), (column: int)) = - "File " ^ file ^ " Line " ^ string_of_int line ^ " Column " ^ string_of_int column + "file " ^ file ^ " line " ^ string_of_int line ^ " column " ^ string_of_int column (** Pretty print a location of ml source *) let pp_ml_location fmt mloc = diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli index c53780b86..589c4ff68 100644 --- a/infer/src/backend/utils.mli +++ b/infer/src/backend/utils.mli @@ -71,6 +71,9 @@ module StringMap : Map.S with type key = string (** Type of location in ml source: file,line,column *) type ml_location = string * int * int +(** String describing the file of an ml location *) +val ml_location_file_string : ml_location -> string + (** Turn an ml location into a string *) val ml_location_string : ml_location -> string diff --git a/infer/src/checkers/eradicateChecks.ml b/infer/src/checkers/eradicateChecks.ml index e4c2051e9..58221c69e 100644 --- a/infer/src/checkers/eradicateChecks.ml +++ b/infer/src/checkers/eradicateChecks.ml @@ -118,8 +118,8 @@ type from_call = let check_condition case_zero find_canonical_duplicate get_proc_desc curr_pname node e typ ta true_branch from_call idenv linereader loc instr_ref : unit = let is_fun_nonnull ta = match TypeAnnotation.get_origin ta with - | TypeOrigin.Proc (_, _, signature, _) -> - let (ia, _) = signature.Annotations.ret in + | TypeOrigin.Proc proc_origin -> + let (ia, _) = proc_origin.TypeOrigin.annotated_signature.Annotations.ret in Annotations.ia_is_nonnull ia | _ -> false in diff --git a/infer/src/checkers/modelTables.ml b/infer/src/checkers/modelTables.ml index 5aef9a0a7..9f34d22bb 100644 --- a/infer/src/checkers/modelTables.ml +++ b/infer/src/checkers/modelTables.ml @@ -226,6 +226,9 @@ let mk_table list = IList.iter (function (v, pn_id) -> Hashtbl.replace map pn_id v) list; map +let ml_location = + try assert false with Assert_failure x -> x + let annotated_table_nullable = mk_table annotated_list_nullable let annotated_table_present = mk_table annotated_list_present let annotated_table_strict = mk_table annotated_list_strict diff --git a/infer/src/checkers/modelTables.mli b/infer/src/checkers/modelTables.mli index 731feede0..8be6008f1 100644 --- a/infer/src/checkers/modelTables.mli +++ b/infer/src/checkers/modelTables.mli @@ -7,8 +7,13 @@ * of patent rights can be found in the PATENTS file in the same directory. *) +open Utils + type model_table_t = (string, bool * bool list) Hashtbl.t +(** Location of this file. *) +val ml_location : ml_location + val annotated_table_nullable : model_table_t val annotated_table_present : model_table_t val annotated_table_strict : model_table_t diff --git a/infer/src/checkers/typeAnnotation.ml b/infer/src/checkers/typeAnnotation.ml index b32f291d0..c79752c67 100644 --- a/infer/src/checkers/typeAnnotation.ml +++ b/infer/src/checkers/typeAnnotation.ml @@ -83,8 +83,8 @@ let join ta1 ta2 = let get_origin ta = ta.origin let origin_is_fun_library ta = match get_origin ta with - | TypeOrigin.Proc (pname, _, _, is_library) -> - is_library + | TypeOrigin.Proc proc_origin -> + proc_origin.TypeOrigin.is_library | _ -> false let descr_origin ta : TypeErr.origin_descr = diff --git a/infer/src/checkers/typeCheck.ml b/infer/src/checkers/typeCheck.ml index 2930db493..b00d2e8ce 100644 --- a/infer/src/checkers/typeCheck.ml +++ b/infer/src/checkers/typeCheck.ml @@ -587,7 +587,13 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc | [id] -> let (ia, ret_typ) = annotated_signature.Annotations.ret in let is_library = Specs.proc_is_library callee_attributes in - let origin = TypeOrigin.Proc (callee_pname, loc', annotated_signature, is_library) in + let origin = TypeOrigin.Proc + { + TypeOrigin.pname = callee_pname; + loc = loc'; + annotated_signature; + is_library; + } in TypeState.add_id id ( diff --git a/infer/src/checkers/typeOrigin.ml b/infer/src/checkers/typeOrigin.ml index af60631cf..b3bab199e 100644 --- a/infer/src/checkers/typeOrigin.ml +++ b/infer/src/checkers/typeOrigin.ml @@ -16,7 +16,12 @@ open Utils type proc_origin = - Procname.t * Location.t * Annotations.annotated_signature * bool (* is_library *) + { + pname : Procname.t; + loc: Location.t; + annotated_signature : Annotations.annotated_signature; + is_library : bool; + } type t = | Const of Location.t @@ -27,6 +32,12 @@ type t = | ONone | Undef +let proc_origin_equal po1 po2 = + Procname.equal po1.pname po2.pname && + Location.equal po1.loc po2.loc && + Annotations.equal po1.annotated_signature po2.annotated_signature && + bool_equal po1.is_library po2.is_library + let equal o1 o2 = match o1, o2 with | Const loc1, Const loc2 -> Location.equal loc1 loc2 @@ -41,11 +52,8 @@ let equal o1 o2 = match o1, o2 with string_equal s1 s2 | Formal _, _ | _, Formal _ -> false - | Proc (pn1, loc1, as1, b1), Proc (pn2, loc2, as2, b2) -> - Procname.equal pn1 pn2 && - Location.equal loc1 loc2 && - Annotations.equal as1 as2 && - bool_equal b1 b2 + | Proc po1 , Proc po2 -> + proc_origin_equal po1 po2 | Proc _, _ | _, Proc _ -> false | New, New -> true @@ -60,10 +68,10 @@ let to_string = function | Const loc -> "Const" | Field (fn, loc) -> "Field " ^ Ident.fieldname_to_simplified_string fn | Formal s -> "Formal " ^ s - | Proc (pname, _, _, _) -> + | Proc po -> Printf.sprintf "Fun %s" - (Procname.to_simplified_string pname) + (Procname.to_simplified_string po.pname) | New -> "New" | ONone -> "ONone" | Undef -> "Undef" @@ -78,20 +86,25 @@ let get_description origin = Some ("field " ^ Ident.fieldname_to_simplified_string fn ^ atline loc, Some loc, None) | Formal s -> Some ("method parameter " ^ s, None, None) - | Proc (pname, loc, signature, is_library) -> - let strict = match TypeErr.Strict.signature_get_strict signature with + | Proc po -> + let strict = match TypeErr.Strict.signature_get_strict po.annotated_signature with | Some ann -> let str = "@Strict" in (match ann.Sil.parameters with | par1 :: _ -> Printf.sprintf "%s(%s) " str par1 | [] -> Printf.sprintf "%s " str) | None -> "" in + let modelled_in = + if Models.is_modelled_nullable po.pname + then " modelled in " ^ (Utils.ml_location_file_string ModelTables.ml_location) + else "" in let description = Printf.sprintf - "call to %s%s %s" + "call to %s%s%s%s" strict - (Procname.to_simplified_string pname) - (atline loc) in - Some (description, Some loc, Some signature) + (Procname.to_simplified_string po.pname) + modelled_in + (atline po.loc) in + Some (description, Some po.loc, Some po.annotated_signature) | New | ONone | Undef -> None diff --git a/infer/src/checkers/typeOrigin.mli b/infer/src/checkers/typeOrigin.mli index 68cf2a5cc..8052f3de5 100644 --- a/infer/src/checkers/typeOrigin.mli +++ b/infer/src/checkers/typeOrigin.mli @@ -7,9 +7,14 @@ * of patent rights can be found in the PATENTS file in the same directory. *) - -type proc_origin = (** Case Proc *) - Procname.t * Location.t * Annotations.annotated_signature * bool (* is_library *) +(** Case Proc *) +type proc_origin = + { + pname : Procname.t; + loc: Location.t; + annotated_signature : Annotations.annotated_signature; + is_library : bool; + } type t = | Const of Location.t (** A constant in the source *)