[nullsafe][Annotation graph] Glueing together: preparing to build annotation graph

Summary:
Now we have all pieces of information needed to build the annotation
graph (to be finished as a follow up).

This diff utilizes the same approach that is done when we calculate node
promotions:
1/ AssignmentRule and DereferenceRule know that some issues are related
to provisional annotations and expose this information.
2/ ClassLevelAnalysis collects all the issues, extract violations from
them, and outputs them.

Next step will be changing the output to the meta-issue printing the
annotation graph in json.

Reviewed By: artempyanykh

Differential Revision: D24621410

fbshipit-source-id: c240da3aa

infer/src/nullsafe/AssignmentRule.ml

@@ -8,6 +8,29 @@ open! IStd
 
 type violation = {lhs: AnnotatedNullability.t; rhs: InferredNullability.t} [@@deriving compare]
 
+module ProvisionalViolation = struct
+  type t =
+    { fix_annotation: ProvisionalAnnotation.t option
+    ; offending_annotations: ProvisionalAnnotation.t list }
+
+  let offending_annotations {offending_annotations} = offending_annotations
+
+  let fix_annotation {fix_annotation} = fix_annotation
+
+  let from {lhs; rhs} =
+    let offending_annotations = InferredNullability.get_provisional_annotations rhs in
+    if List.is_empty offending_annotations then None
+    else
+      let fix_annotation =
+        match lhs with
+        | AnnotatedNullability.ProvisionallyNullable annotation ->
+            Some annotation
+        | _ ->
+            None
+      in
+      Some {offending_annotations; fix_annotation}
+end
+
 module ReportableViolation = struct
   type t = {nullsafe_mode: NullsafeMode.t; violation: violation}
 

infer/src/nullsafe/AssignmentRule.mli

@@ -16,6 +16,22 @@ val check : lhs:AnnotatedNullability.t -> rhs:InferredNullability.t -> (unit, vi
 (** If `null` can leak from a "less strict" type to "more strict" type, this is an Assignment Rule
     violation. *)
 
+(** Violation that will occur if the provisional annotation becomes real [@Nullable] *)
+module ProvisionalViolation : sig
+  type t
+
+  val offending_annotations : t -> ProvisionalAnnotation.t list
+  (** Non-empty list of corresponding provisional annotations (adding any of those will lead to an
+      issue) *)
+
+  val fix_annotation : t -> ProvisionalAnnotation.t option
+  (** If there is a place such as adding [@Nullable] will fix the issue, this is the one. *)
+
+  val from : violation -> t option
+  (** If the violation is provisional (so is not real but will become real when the annotation is
+      added), create it. *)
+end
+
 (** Violation that needs to be reported to the user. *)
 module ReportableViolation : sig
   type t

infer/src/nullsafe/ClassLevelAnalysis.ml

@@ -250,10 +250,58 @@ let analyze_nullsafe_annotations tenv source_file class_name class_struct issue_
         IssueType.eradicate_bad_nested_class_annotation description
 
 
+let process_issue_for_annotation_graph issue =
+  match issue with
+  | TypeErr.Condition_redundant _
+  | TypeErr.Field_not_initialized _
+  | TypeErr.Inconsistent_subclass _
+  | TypeErr.Over_annotation _ ->
+      ()
+  | TypeErr.Nullable_dereference {dereference_violation} ->
+      DereferenceRule.ProvisionalViolation.from dereference_violation
+      |> Option.iter ~f:(fun provisional_violation ->
+             let annotations =
+               DereferenceRule.ProvisionalViolation.offending_annotations provisional_violation
+             in
+             Logging.debug Analysis Medium
+               "Found provisional violation: dereference caused by any of %a\n"
+               (Pp.seq ProvisionalAnnotation.pp) annotations )
+  | TypeErr.Bad_assignment {assignment_violation} ->
+      AssignmentRule.ProvisionalViolation.from assignment_violation
+      |> Option.iter ~f:(fun provisional_violation ->
+             let offending_annotations =
+               AssignmentRule.ProvisionalViolation.offending_annotations provisional_violation
+             in
+             let fix_annotation =
+               AssignmentRule.ProvisionalViolation.fix_annotation provisional_violation
+             in
+             let fix_annotation_descr =
+               Option.value_map fix_annotation
+                 ~f:(fun annotation ->
+                   Format.asprintf ", fixable by %a" ProvisionalAnnotation.pp annotation )
+                 ~default:""
+             in
+             Logging.debug Analysis Medium
+               "Found provisional violation: assignment caused by any of %a%s\n"
+               (Pp.seq ProvisionalAnnotation.pp) offending_annotations fix_annotation_descr )
+
+
+let construct_annotation_graph _class_name class_info issue_log =
+  if not Config.nullsafe_annotation_graph then issue_log
+  else (
+    (* TODO: actually construct the graph (just print provisional violations for now) *)
+    AggregatedSummaries.ClassInfo.get_summaries class_info
+    |> List.map ~f:(fun NullsafeSummary.{issues} -> issues)
+    |> List.fold ~init:[] ~f:( @ )
+    |> List.iter ~f:process_issue_for_annotation_graph ;
+    issue_log )
+
+
 let analyze_class_impl tenv source_file class_name class_struct class_info issue_log =
   issue_log
   |> analyze_meta_issue_for_top_level_class tenv source_file class_name class_struct class_info
   |> analyze_nullsafe_annotations tenv source_file class_name class_struct
+  |> construct_annotation_graph class_name class_info
 
 
 let analyze_class tenv source_file class_info issue_log =

infer/src/nullsafe/DereferenceRule.ml

@@ -8,6 +8,16 @@ open! IStd
 
 type violation = {nullability: InferredNullability.t} [@@deriving compare]
 
+module ProvisionalViolation = struct
+  type t = {offending_annotations: ProvisionalAnnotation.t list}
+
+  let offending_annotations {offending_annotations} = offending_annotations
+
+  let from {nullability} =
+    let offending_annotations = InferredNullability.get_provisional_annotations nullability in
+    if List.is_empty offending_annotations then None else Some {offending_annotations}
+end
+
 module ReportableViolation = struct
   type t = {nullsafe_mode: NullsafeMode.t; violation: violation}
 

infer/src/nullsafe/DereferenceRule.mli

@@ -16,6 +16,19 @@ val check : InferredNullability.t -> (unit, violation) result
     might or might not be severe enough to be reported to the user, depending on the mode
     agreements. *)
 
+(** Violation that will occur if the provisional annotation becomes real [@Nullable] *)
+module ProvisionalViolation : sig
+  type t
+
+  val offending_annotations : t -> ProvisionalAnnotation.t list
+  (** Non-empty list of corresponding provisional annotations (adding any of those will lead to an
+      issue) *)
+
+  val from : violation -> t option
+  (** If the violation is provisional (so is not real but will become real when the annotation is
+      added), create it. *)
+end
+
 (** Violation that needs to be reported to the user. *)
 module ReportableViolation : sig
   type t

infer/src/nullsafe/InferredNullability.ml

@@ -67,5 +67,10 @@ let join t1 t2 =
 
 let get_simple_origin t = List.nth_exn t.origins 0
 
+let get_provisional_annotations t =
+  List.filter_map t.origins ~f:TypeOrigin.get_provisional_annotation
+  |> List.dedup_and_sort ~compare:ProvisionalAnnotation.compare
+
+
 let origin_is_fun_defined t =
   match get_simple_origin t with TypeOrigin.MethodCall {is_defined; _} -> is_defined | _ -> false

infer/src/nullsafe/InferredNullability.mli

@@ -26,6 +26,8 @@ val is_nonnullish : t -> bool
 val get_simple_origin : t -> TypeOrigin.t
 (** The simple explanation of how was nullability inferred. *)
 
+val get_provisional_annotations : t -> ProvisionalAnnotation.t list
+
 val join : t -> t -> t
 (** This is what happens with nullability when we join two flows in CFG, e.g.
 

infer/src/nullsafe/ProvisionalAnnotation.ml

@@ -11,3 +11,11 @@ type t =
   | Method of Procname.Java.t
   | Param of {method_info: Procname.Java.t; num: int}
 [@@deriving compare]
+
+let pp fmt = function
+  | Field {field_name} ->
+      Format.fprintf fmt "Field(%s)" field_name
+  | Method proc_name ->
+      Format.fprintf fmt "Method(%a)" Procname.pp (Procname.Java proc_name)
+  | Param {method_info; num} ->
+      Format.fprintf fmt "Param(%d, %a)" num Procname.pp (Procname.Java method_info)

infer/src/nullsafe/ProvisionalAnnotation.mli

@@ -16,3 +16,5 @@ type t =
   | Method of Procname.Java.t
   | Param of {method_info: Procname.Java.t; num: int}
 [@@deriving compare]
+
+val pp : Format.formatter -> t -> unit

infer/src/nullsafe/typeOrigin.ml

@@ -165,6 +165,37 @@ let get_method_ret_description pname call_loc
     (atline call_loc) model_info
 
 
+let get_provisional_annotation = function
+  | NullConst _
+  | NonnullConst _
+  | This
+  | New
+  | ArrayLengthResult
+  | CallToGetKnownToContainsKey
+  | InferredNonnull _
+  | ArrayAccess
+  | OptimisticFallback ->
+      None
+  | Field
+      {field_type= {nullability= AnnotatedNullability.ProvisionallyNullable provisional_annotation}}
+    ->
+      Some provisional_annotation
+  | CurrMethodParameter
+      (Normal
+        { param_annotated_type=
+            {nullability= AnnotatedNullability.ProvisionallyNullable provisional_annotation} }) ->
+      Some provisional_annotation
+  | MethodCall
+      { annotated_signature=
+          { ret=
+              { ret_annotated_type=
+                  {nullability= AnnotatedNullability.ProvisionallyNullable provisional_annotation}
+              } } } ->
+      Some provisional_annotation
+  | Field _ | CurrMethodParameter _ | MethodCall _ ->
+      None
+
+
 let get_description origin =
   match origin with
   | NullConst loc ->

infer/src/nullsafe/typeOrigin.mli

@@ -49,6 +49,9 @@ type t =
 
 val get_nullability : t -> Nullability.t
 
+val get_provisional_annotation : t -> ProvisionalAnnotation.t option
+(** If the origin is associated with provisional annotation, return it *)
+
 val get_description : t -> string option
 (** Get a description to be used for error messages. *)