[nullsafe] Don't mention "unannotated" in Models

Summary:
"Unannotated" is misleading and ambiguous concept, it can have different
meanings depending on agreements.

The current logic treats them as Nonnull, which is exactly what we want
to preserve.

(If we need to partially model some functions where we don't have
opinion on some of types in the signature, we can explicitly model
unknown nullability later on).

Note that I am not aiming for substantial refactoring of
modelsTables.ml; the scope of this diff is merely to clarify things.

Reviewed By: ngorogiannis

Differential Revision: D17449347

fbshipit-source-id: 43c798ce7

infer/src/nullsafe/eradicateChecks.ml

@@ -332,8 +332,10 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
   let should_check_parameters =
     match callee_pname with
     | Typ.Procname.Java java_pname ->
+        (* TODO(T52947663) model is_external as unknown nullability and move the logic out of this check  *)
+        (* If method is external, we don't check it, unless it is explicitly modelled *)
         (not (Typ.Procname.Java.is_external java_pname))
-        || Models.is_modelled_nullable callee_pname
+        || Models.is_modelled_for_nullability callee_pname
     | _ ->
         false
   in

infer/src/nullsafe/modelTables.ml

@@ -16,63 +16,50 @@ module Hashtbl = Caml.Hashtbl
 (* in strict mode, give an error if a nullable is passed to checkNotNull *)
 let check_not_null_strict = false
 
-(* o is not annotated and n is annotated with @Nullable *)
+(* the type should be treated as Nonnull *)
 let o = false
 
+(* the type should be treated as Nullable *)
 and n = true
 
-(* create unannotated signature with n argument *)
+(* create signature where both return type and params are nonnull *)
-let unannotated n =
+let all_nonnull num_params = (o, List.init num_params ~f:(fun _ -> o))
-  let rec loop l = function i when i <= 0 -> (o, l) | i -> loop (o :: l) (i - 1) in
-  loop [] n
 
+(* o<N> means signature with N nonnull params and nonnull return type *)
 
-(* not annotated with one unannotated argument *)
+let o1 = all_nonnull 1
-let o1 = unannotated 1
 
-(* not annotated with two unannotated arguments *)
+let o2 = all_nonnull 2
-let o2 = unannotated 2
 
-(* not annotated with three unannotated arguments *)
+let o3 = all_nonnull 3
-let o3 = unannotated 3
 
-(* not annotated with four unannotated arguments *)
+let o4 = all_nonnull 4
-let o4 = unannotated 4
 
-(* not annotated with five unannotated arguments *)
+let o5 = all_nonnull 5
-let o5 = unannotated 5
 
-(* not annotated with six unannotated arguments *)
+let o6 = all_nonnull 6
-let o6 = unannotated 6
 
-(* not annotated with seven unannotated arguments *)
+let o7 = all_nonnull 7
-let o7 = unannotated 7
 
-(* not annotated with eight unannotated arguments *)
+let o8 = all_nonnull 8
-let o8 = unannotated 8
 
-(* not annotated with nine unannotated arguments *)
+let o9 = all_nonnull 9
-let o9 = unannotated 9
 
-(* not annotated with ten unannotated arguments *)
+let o10 = all_nonnull 10
-let o10 = unannotated 10
 
-(* not annotated with eleven unannotated arguments *)
+let o11 = all_nonnull 11
-let o11 = unannotated 11
 
-(* not annotated with twelve unannotated arguments *)
+let o12 = all_nonnull 12
-let o12 = unannotated 12
+
+(* n<N> stands for signature with nonnull return type and N nullable params *)
 
-(* one argument nullable *)
 let n1 = (o, [n])
 
-(* two arguments nullable *)
 let n2 = (o, [n; n])
 
-(* three arguments nullable *)
 let n3 = (o, [n; n; n])
 
-(* the second argument is nullable *)
+(* the second argument is nullable, everything else is nonnull *)
 let on = (o, [o; n])
 
 (* container add *)
@@ -202,8 +189,8 @@ let mapPut_list =
   ; (cp, "java.util.Map.put(java.lang.Object,java.lang.Object):java.lang.Object") ]
 
 
-(** Models for @Nullable annotations *)
+(** Models for nullability *)
-let annotated_list_nullable =
+let annotated_list_nullability =
   check_not_null_list @ check_state_list @ check_argument_list
   @ [ ( o1
       , "android.text.SpannableString.valueOf(java.lang.CharSequence):android.text.SpannableString"
@@ -584,7 +571,7 @@ let mk_table list =
 
 let this_file = Filename.basename __FILE__
 
-let annotated_table_nullable = mk_table annotated_list_nullable
+let annotated_table_nullability = mk_table annotated_list_nullability
 
 let check_not_null_table, check_not_null_parameter_table =
   (mk_table check_not_null_list, mk_table check_not_null_parameter_list)

infer/src/nullsafe/modelTables.mli

@@ -12,7 +12,7 @@ type model_table_t = (string, bool * bool list) Caml.Hashtbl.t
 val this_file : string
 (** Name of this file. *)
 
-val annotated_table_nullable : model_table_t
+val annotated_table_nullability : model_table_t
 
 val check_not_null_table : model_table_t
 

infer/src/nullsafe/models.ml

@@ -34,18 +34,18 @@ let get_modelled_annotated_signature proc_attributes =
   let proc_id = Typ.Procname.to_unique_id proc_name in
   let lookup_models_nullable ann_sig =
     try
-      let modelled_nullability = Hashtbl.find annotated_table_nullable proc_id in
+      let modelled_nullability = Hashtbl.find annotated_table_nullability proc_id in
       AnnotatedSignature.set_modelled_nullability proc_name ann_sig modelled_nullability
     with Caml.Not_found -> ann_sig
   in
   annotated_signature |> lookup_models_nullable
 
 
-(** Return true when the procedure has been modelled for nullable. *)
+(** Return true when the procedure has been modelled for nullability. *)
-let is_modelled_nullable proc_name =
+let is_modelled_for_nullability proc_name =
   let proc_id = Typ.Procname.to_unique_id proc_name in
   try
-    ignore (Hashtbl.find annotated_table_nullable proc_id) ;
+    ignore (Hashtbl.find annotated_table_nullability proc_id) ;
     true
   with Caml.Not_found -> false
 

infer/src/nullsafe/typeOrigin.ml

@@ -56,7 +56,8 @@ let get_description origin =
       Some ("method parameter " ^ Mangled.to_string s, None, None)
   | Proc po ->
       let modelled_in =
-        if Models.is_modelled_nullable po.pname then " modelled in " ^ ModelTables.this_file
+        (* TODO(T54088319) don't calculate this info and propagate it from NullsafeType instead *)
+        if Models.is_modelled_for_nullability po.pname then " modelled in " ^ ModelTables.this_file
         else ""
       in
       let description =