Print origin information for procedured modelled internally.

Reviewed By: jvillard

Differential Revision: D2585242

fb-gh-sync-id: 31b5834

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 =

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
 

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
 

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

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

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 =

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
               (

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

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 *)