@ -11,29 +11,19 @@ open ModelTables
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					(* *  Module for standard library models.  *) (* *  Module for standard library models.  *)  
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					let  match_method_name  pn  name  = (* *  Unique representation of a method signature in form of a string.  *)  
			
				
				
			
		
	
		
		
			
				
					
					  match  pn  with 
let  to_unique_id  proc_name  =  Procname . to_unique_id  ( Procname . Java  proc_name )  
			
				
				
			
		
	
		
		
			
				
					
					  |  Procname . Java  pn_java  -> 
 
			
		
	
		
		
			
				
					
					      String . equal  ( Procname . Java . get_method  pn_java )  name 
 
			
		
	
		
		
			
				
					
					  |  _  -> 
 
			
		
	
		
		
			
				
					
					      false 
 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					let  match_method_name  proc_name  name  =  String . equal  ( Procname . Java . get_method  proc_name )  name  
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					let  table_has_procedure  table  proc_name  = let  table_has_procedure  table  proc_name  =  
			
		
	
		
		
			
				
					
					  let  proc_id  =  Procname . to_unique_id  proc_name  in 
  let  proc_id  =  to_unique_id  proc_name  in 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					  try 
  try 
 
			
		
	
		
		
			
				
					
					    ignore  ( Hashtbl . find  table  proc_id )  ; 
    ignore  ( Hashtbl . find  table  proc_id )  ; 
 
			
		
	
		
		
			
				
					
					    true 
    true 
 
			
		
	
		
		
			
				
					
					  with  Caml . Not_found  ->  false 
  with  Caml . Not_found  ->  false 
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					let  get_unique_repr  proc_name  =  
			
		
	
		
		
			
				
					
					  let  java_proc_name  = 
 
			
		
	
		
		
			
				
					
					    match  proc_name  with  Procname . Java  java_proc_name  ->  Some  java_proc_name  |  _  ->  None 
 
			
		
	
		
		
			
				
					
					  in 
 
			
		
	
		
		
			
				
					
					  Option . map  java_proc_name  ~ f : ThirdPartyAnnotationInfo . unique_repr_of_java_proc_name 
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					let  to_modelled_nullability  ThirdPartyMethod . { ret_nullability ;  params }  = let  to_modelled_nullability  ThirdPartyMethod . { ret_nullability ;  params }  =  
			
		
	
		
		
			
				
					
					  let  is_nullable  =  function 
  let  is_nullable  =  function 
 
			
		
	
		
		
			
				
					
					    |  ThirdPartyMethod . Nullable  -> 
    |  ThirdPartyMethod . Nullable  -> 
 
			
		
	
	
		
		
			
				
					
						
						
						
							
								 
						
					 
					@ -45,8 +35,10 @@ let to_modelled_nullability ThirdPartyMethod.{ret_nullability; params} =
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					(*  Some methods  *) (*  Some methods  *)  
			
		
	
		
		
			
				
					
					let  get_special_method_modelled_nullability  tenv  = let  get_special_method_modelled_nullability  tenv  java_ proc_name =  
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					  let  open  IOption . Let_syntax  in 
  let  open  IOption . Let_syntax  in 
 
			
		
	
		
		
			
				
					
					  (*  TODO: convert the implementation that does not use PatternMatch  *) 
 
			
		
	
		
		
			
				
					
					  let  proc_name  =  Procname . Java  java_proc_name  in 
 
			
		
	
		
		
			
				
					
					  let *  class_name  =  Procname . get_class_type_name  proc_name  in 
  let *  class_name  =  Procname . get_class_type_name  proc_name  in 
 
			
		
	
		
		
			
				
					
					  if  PatternMatch . Java . is_enum  tenv  class_name  then 
  if  PatternMatch . Java . is_enum  tenv  class_name  then 
 
			
		
	
		
		
			
				
					
					    match  ( Procname . get_method  proc_name ,  Procname . get_parameters  proc_name )  with 
    match  ( Procname . get_method  proc_name ,  Procname . get_parameters  proc_name )  with 
 
			
		
	
	
		
		
			
				
					
						
						
						
							
								 
						
					 
					@ -65,12 +57,15 @@ let get_special_method_modelled_nullability tenv proc_name =
 
			
		
	
		
		
			
				
					
					(* *  Return the annotated signature of the procedure, taking into account models. External models (* *  Return the annotated signature of the procedure, taking into account models. External models  
			
		
	
		
		
			
				
					
					    take  precedence  over  internal  ones .  * ) 
    take  precedence  over  internal  ones .  * ) 
 
			
		
	
		
		
			
				
					
					let  get_modelled_annotated_signature  ~ is_callee_in_trust_list  tenv  proc_attributes  = let  get_modelled_annotated_signature  ~ is_callee_in_trust_list  tenv  proc_attributes  =  
			
		
	
		
		
			
				
					
					  let  proc_name  =  proc_attributes . ProcAttributes . proc_name  in 
  let  proc_name  = 
 
			
				
				
			
		
	
		
		
			
				
					
					  let  nullsafe_mode  =  NullsafeMode . of_procname  tenv  proc_name  in 
    Procname . as_java_exn  proc_attributes . ProcAttributes . proc_name 
 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					      ~ explanation : " get_modelled_annotated_signature should be called for Java methods only " 
 
			
		
	
		
		
			
				
					
					  in 
 
			
		
	
		
		
			
				
					
					  let  nullsafe_mode  =  NullsafeMode . of_java_procname  tenv  proc_name  in 
 
			
		
	
		
		
			
				
					
					  let  annotated_signature  = 
  let  annotated_signature  = 
 
			
		
	
		
		
			
				
					
					    AnnotatedSignature . get  ~ is_callee_in_trust_list  ~ nullsafe_mode  proc_attributes 
    AnnotatedSignature . get  ~ is_callee_in_trust_list  ~ nullsafe_mode  proc_attributes 
 
			
		
	
		
		
			
				
					
					  in 
  in 
 
			
		
	
		
		
			
				
					
					  let  proc_id  =  Procname . to_unique_id  proc_name  in 
  let  proc_id  =  to_unique_id  proc_name  in 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					  (*  Look in the infer internal models  *) 
  (*  Look in the infer internal models  *) 
 
			
		
	
		
		
			
				
					
					  let  correct_by_internal_models  ann_sig  = 
  let  correct_by_internal_models  ann_sig  = 
 
			
		
	
		
		
			
				
					
					    let  modelled_nullability  = 
    let  modelled_nullability  = 
 
			
		
	
	
		
		
			
				
					
						
						
						
							
								 
						
					 
					@ -81,22 +76,21 @@ let get_modelled_annotated_signature ~is_callee_in_trust_list tenv proc_attribut
 
			
		
	
		
		
			
				
					
					             get_special_method_modelled_nullability  tenv  proc_name  ) 
             get_special_method_modelled_nullability  tenv  proc_name  ) 
 
			
		
	
		
		
			
				
					
					    in 
    in 
 
			
		
	
		
		
			
				
					
					    Option . value_map  modelled_nullability 
    Option . value_map  modelled_nullability 
 
			
		
	
		
		
			
				
					
					      ~ f : ( AnnotatedSignature . set_modelled_nullability  proc_name  ann_sig  ModelledInternally ) 
      ~ f : 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					        ( AnnotatedSignature . set_modelled_nullability  ( Procname . Java  proc_name )  ann_sig 
 
			
		
	
		
		
			
				
					
					           ModelledInternally ) 
 
			
		
	
		
		
			
				
					
					      ~ default : ann_sig 
      ~ default : ann_sig 
 
			
		
	
		
		
			
				
					
					  in 
  in 
 
			
		
	
		
		
			
				
					
					  (*  Look at external models  *) 
  (*  Look at external models  *) 
 
			
		
	
		
		
			
				
					
					  let  correct_by_external_models  ann_sig  = 
  let  correct_by_external_models  ann_sig  = 
 
			
		
	
		
		
			
				
					
					    get_unique_repr  proc_name 
    ThirdPartyAnnotationInfo . unique_repr_of_java_proc_name  proc_name 
 
			
				
				
			
		
	
		
		
			
				
					
					    | >  Option . bind 
    | >  ThirdPartyAnnotationInfo . find_nullability_info  ( ThirdPartyAnnotationGlobalRepo . get_repo  () ) 
 
			
				
				
			
		
	
		
		
			
				
					
					         ~ f : 
 
			
		
	
		
		
			
				
					
					           ( ThirdPartyAnnotationInfo . find_nullability_info 
 
			
		
	
		
		
			
				
					
					              ( ThirdPartyAnnotationGlobalRepo . get_repo  () ) ) 
 
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					    | >  Option . map  ~ f : ( fun  ThirdPartyAnnotationInfo . { signature ;  filename ;  line_number }  -> 
    | >  Option . map  ~ f : ( fun  ThirdPartyAnnotationInfo . { signature ;  filename ;  line_number }  -> 
 
			
		
	
		
		
			
				
					
					           ( to_modelled_nullability  signature ,  filename ,  line_number )  ) 
           ( to_modelled_nullability  signature ,  filename ,  line_number )  ) 
 
			
		
	
		
		
			
				
					
					    | >  Option . value_map 
    | >  Option . value_map 
 
			
		
	
		
		
			
				
					
					       (*  If we found information in third-party repo, overwrite annotated signature  *) 
       (*  If we found information in third-party repo, overwrite annotated signature  *) 
 
			
		
	
		
		
			
				
					
					         ~ f : ( fun  ( modelled_nullability ,  filename ,  line_number )  -> 
         ~ f : ( fun  ( modelled_nullability ,  filename ,  line_number )  -> 
 
			
		
	
		
		
			
				
					
					           AnnotatedSignature . set_modelled_nullability  proc_name  ann_sig 
           AnnotatedSignature . set_modelled_nullability  ( Procname . Java  proc_name ) ann_sig 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					             ( InThirdPartyRepo  { filename ;  line_number } ) 
             ( InThirdPartyRepo  { filename ;  line_number } ) 
 
			
		
	
		
		
			
				
					
					             modelled_nullability  ) 
             modelled_nullability  ) 
 
			
		
	
		
		
			
				
					
					         ~ default : ann_sig 
         ~ default : ann_sig 
 
			
		
	
	
		
		
			
				
					
						
						
						
							
								 
						
					 
					@ -114,7 +108,7 @@ let is_check_not_null proc_name =
 
			
		
	
		
		
			
				
					
					(* *  Parameter number  ( starting from 1 )  for a procedure known to produce a non-nullable assertion. (* *  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  * ) 
    [ 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  get_check_not_null_parameter  proc_name  =  
			
		
	
		
		
			
				
					
					  let  proc_id  =  Procname . to_unique_id  proc_name  in 
  let  proc_id  =  to_unique_id  proc_name  in 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					  Hashtbl . find_opt  check_not_null_parameter_table  proc_id 
  Hashtbl . find_opt  check_not_null_parameter_table  proc_id 
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					
 
			
		
	
	
		
		
			
				
					
						
						
						
							
								 
						
					 
					@ -138,7 +132,7 @@ let is_true_on_null proc_name = table_has_procedure true_on_null_table proc_name
 
			
		
	
		
		
			
				
					
					let  is_false_on_null  proc_name  = let  is_false_on_null  proc_name  =  
			
		
	
		
		
			
				
					
					  (*  The only usecase for now - consider all overrides of `Object.equals ( ) ` correctly 
  (*  The only usecase for now - consider all overrides of `Object.equals ( ) ` correctly 
 
			
		
	
		
		
			
				
					
					     implementing  the  Java  specification  contract  ( returning  false  on  null ) .  * ) 
     implementing  the  Java  specification  contract  ( returning  false  on  null ) .  * ) 
 
			
		
	
		
		
			
				
					
					  PatternMatch . Java . is_override_of_lang_object_equals  proc_name 
  PatternMatch . Java . is_override_of_lang_object_equals  ( Procname . Java  proc_name ) 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					(* *  Check if the procedure is Map.containsKey ( ) .  *) (* *  Check if the procedure is Map.containsKey ( ) .  *)  
			
		
	
	
		
		
			
				
					
						
						
						
							
								 
						
					 
					@ -149,11 +143,10 @@ let is_mapPut proc_name = table_has_procedure mapPut_table proc_name
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					(* *  Check if a  ( nullable )  method has a non-nullable alternative: A method that does the same as (* *  Check if a  ( nullable )  method has a non-nullable alternative: A method that does the same as  
			
		
	
		
		
			
				
					
					    [ proc_name ]  but  asserts  the  result  is  not  null  before  returning  to  the  caller .  * ) 
    [ proc_name ]  but  asserts  the  result  is  not  null  before  returning  to  the  caller .  * ) 
 
			
		
	
		
		
			
				
					
					let  find_nonnullable_alternative  java_ proc_name = let  find_nonnullable_alternative  =  
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					  (*  NOTE: For now we fetch this info from internal models. 
  (*  NOTE: For now we fetch this info from internal models. 
 
			
		
	
		
		
			
				
					
					     It  is  a  good  idea  to  support  this  feature  in  a  user - facing  third  party  repository .  * ) 
     It  is  a  good  idea  to  support  this  feature  in  a  user - facing  third  party  repository .  * ) 
 
			
		
	
		
		
			
				
					
					  let  proc_name  =  Procname . Java  java_proc_name  in 
  let  proc_id  =  to_unique_id  proc_name  in 
 
			
				
				
			
		
	
		
		
			
				
					
					  let  proc_id  =  Procname . to_unique_id  proc_name  in 
 
			
		
	
		
		
	
		
		
			
				
					
					  Hashtbl . find_opt  nonnull_alternatives_table  proc_id 
  Hashtbl . find_opt  nonnull_alternatives_table  proc_id