diff --git a/infer/src/nullsafe/modelTables.ml b/infer/src/nullsafe/modelTables.ml index 7e40adc77..44b916b0f 100644 --- a/infer/src/nullsafe/modelTables.ml +++ b/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") - ; (2, (o, [n; x]), "org.junit.Assert.assertNotNull(java.lang.String,java.lang.Object):void") + ; (1, (o, [n]), "org.junit.Assert.assertNotNull(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 diff --git a/infer/src/nullsafe/modelTables.mli b/infer/src/nullsafe/modelTables.mli index a8c4231c5..baf4688d9 100644 --- a/infer/src/nullsafe/modelTables.mli +++ b/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 diff --git a/infer/src/nullsafe/models.ml b/infer/src/nullsafe/models.ml index 5af4aea33..1b9da0e38 100644 --- a/infer/src/nullsafe/models.ml +++ b/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