[nullsafe] Documentation and minor code cleanup around models for `checkNotNull`

Summary:
1. I can not imagine a useful usecase for strict node, lets not
complicate the code.
2. Add docs.

Reviewed By: artempyanykh

Differential Revision: D19599091

fbshipit-source-id: 1d37a717f

infer/src/nullsafe/modelTables.ml

@@ -13,9 +13,6 @@ module Hashtbl = Caml.Hashtbl
  * @nolint
  *)
 
-(* in strict mode, give an error if a nullable is passed to checkNotNull *)
-let check_not_null_strict = false
-
 (* the type should be treated as Nonnull *)
 let o = false
 
@@ -78,50 +75,55 @@ let cr = if Config.nullsafe_strict_containers then (n, [o]) else (n, [n])
 let ng = (n, [])
 
 let check_not_null_parameter_list, check_not_null_list =
-  let x = if check_not_null_strict then o else n in
+  (* The first integer in the tuple is the index (counting from 1) of the argument to be asserted.
+     Commonly it is 1.
+  *)
   let list =
     [ ( 1
-      , (o, [x; n])
+      , (o, [n; n])
       , "com.facebook.common.internal.Preconditions.checkNotNull(java.lang.Object,java.lang.Object):java.lang.Object"
       )
     ; ( 1
-      , (o, [x; n; n])
+      , (o, [n; n; n])
       , "com.facebook.common.internal.Preconditions.checkNotNull(java.lang.Object,java.lang.String,java.lang.Object[]):java.lang.Object"
       )
     ; ( 1
-      , (o, [x])
+      , (o, [n])
       , "com.facebook.common.internal.Preconditions.checkNotNull(java.lang.Object):java.lang.Object"
       )
     ; ( 1
-      , (o, [x; n])
+      , (o, [n; n])
       , "com.facebook.common.preconditions.Preconditions.checkNotNull(java.lang.Object,java.lang.String):java.lang.Object"
       )
     ; ( 1
-      , (o, [x; n; n])
+      , (o, [n; n; n])
       , "com.facebook.common.preconditions.Preconditions.checkNotNull(java.lang.Object,java.lang.String,java.lang.Object[]):java.lang.Object"
       )
     ; ( 1
-      , (o, [x])
+      , (o, [n])
       , "com.facebook.common.preconditions.Preconditions.checkNotNull(java.lang.Object):java.lang.Object"
       )
     ; ( 1
-      , (o, [x; n])
+      , (o, [n; n])
       , "com.google.common.base.Preconditions.checkNotNull(java.lang.Object,java.lang.Object):java.lang.Object"
       )
     ; ( 1
-      , (o, [x; n; n])
+      , (o, [n; n; n])
       , "com.google.common.base.Preconditions.checkNotNull(java.lang.Object,java.lang.String,java.lang.Object[]):java.lang.Object"
       )
     ; ( 1
-      , (o, [x])
+      , (o, [n])
       , "com.google.common.base.Preconditions.checkNotNull(java.lang.Object):java.lang.Object" )
-    ; (1, (o, [x]), "com.google.common.base.Verify.verifyNotNull(java.lang.Object):java.lang.Object")
+    ; (1, (o, [n]), "com.google.common.base.Verify.verifyNotNull(java.lang.Object):java.lang.Object")
     ; ( 1
-      , (o, [x; n; n])
+      , (o, [n; n; n])
       , "com.google.common.base.Verify.verifyNotNull(java.lang.Object,java.lang.String,java.lang.Object[]):java.lang.Object"
       )
-    ; (1, (o, [x]), "org.junit.Assert.assertNotNull(java.lang.Object):void")
+    ; (1, (o, [n]), "org.junit.Assert.assertNotNull(java.lang.Object):void")
-    ; (2, (o, [n; x]), "org.junit.Assert.assertNotNull(java.lang.String,java.lang.Object):void")
+    ; ( 2
+      , (* a non-traditional method - the second parameter is the object to be asserted, the first is the description *)
+        (o, [n; n])
+      , "org.junit.Assert.assertNotNull(java.lang.String,java.lang.Object):void" )
     ; ( 1
       , (o, [n])
       , "com.facebook.infer.annotation.Assertions.assertNotNull(java.lang.Object):java.lang.Object"
@@ -139,10 +141,10 @@ let check_not_null_parameter_list, check_not_null_list =
       , "com.facebook.infer.annotation.Assertions.assumeNotNull(java.lang.Object,java.lang.String):java.lang.Object"
       )
     ; ( 1
-      , (o, [x])
+      , (o, [n])
       , "androidx.core.util.Preconditions.checkNotNull(java.lang.Object):java.lang.Object" )
     ; ( 1
-      , (o, [x; n])
+      , (o, [n; n])
       , "androidx.core.util.Preconditions.checkNotNull(java.lang.Object,java.lang.Object):java.lang.Object"
       ) ]
   in

infer/src/nullsafe/modelTables.mli

@@ -9,11 +9,19 @@ open! IStd
 
 type model_table_t = (string, bool * bool list) Caml.Hashtbl.t
 
+(* The key is a unique string representation of a method.
+   The value is nullability of its return value and params correspondingly.
+   true corresponds to Nullable.
+ *)
+
 val annotated_table_nullability : model_table_t
 
 val check_not_null_table : model_table_t
+(** List of methods known to perform a non-nullable assertion *)
 
 val check_not_null_parameter_table : (string, int) Caml.Hashtbl.t
+(** The key is a string representation of a method known to perform a non-nullable assertion. The
+    value is an index (starting from 1) of an argument which nullability is being asserted. *)
 
 val check_state_table : model_table_t
 

infer/src/nullsafe/models.ml

@@ -100,12 +100,14 @@ let get_modelled_annotated_signature tenv proc_attributes =
   annotated_signature |> correct_by_internal_models |> correct_by_external_models
 
 
-(** Check if the procedure is one of the known Preconditions.checkNotNull. *)
+(** Check if the procedure is one of the known methods asserting nullability of the object. Nullsafe
+    should understand that both the argument and return value are non-nullable after the call. *)
 let is_check_not_null proc_name =
   table_has_procedure check_not_null_table proc_name || match_method_name proc_name "checkNotNull"
 
 
-(** Parameter number for a procedure known to be a checkNotNull *)
+(** Parameter number (starting from 1) for a procedure known to produce a non-nullable assertion.
+    [None] if the function is not known to be an aseertion OR the parameter number is not known *)
 let get_check_not_null_parameter proc_name =
   let proc_id = Procname.to_unique_id proc_name in
   Hashtbl.find_opt check_not_null_parameter_table proc_id