From 5df13f69e7bdab9b6729c19bde4309a5e2c3a253 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Tue, 30 Jun 2020 05:47:31 -0700
Subject: [PATCH] [inferbo] Add some models of linked list next methods

Summary:
This diff adds some models of `next` methods of linked list.

* `android.app.Activity.getParent`
* `androidx.fragment.app.Fragment.getParentFragment`
* `com.facebook.graphql.model.GraphQLStory.getAttachedStory`
* `com.intellij.psi.PsiElement.getParent`
* `android.view.ViewGroup.getParent`
* `android.view.ViewParent.getParent`

Reviewed By: ezgicicek

Differential Revision: D22283069

fbshipit-source-id: f628268e6
---
 infer/src/absint/PatternMatch.ml              | 12 ++++++++
 infer/src/absint/PatternMatch.mli             | 18 ++++++++++++
 infer/src/bufferoverrun/absLoc.ml             |  7 +++--
 infer/src/bufferoverrun/bufferOverrunField.ml |  2 ++
 .../src/bufferoverrun/bufferOverrunField.mli  |  3 ++
 .../src/bufferoverrun/bufferOverrunModels.ml  | 29 ++++++++++++++++++-
 .../codetoanalyze/java/performance/Loops.java |  7 +++++
 .../java/performance/cost-issues.exp          | 23 ++++++++-------
 .../codetoanalyze/java/performance/issues.exp |  6 ++--
 9 files changed, 89 insertions(+), 18 deletions(-)

diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml
index a9026f77a..b0f434516 100644
--- a/infer/src/absint/PatternMatch.ml
+++ b/infer/src/absint/PatternMatch.ml
@@ -109,6 +109,18 @@ let implements_jackson class_name = implements ("com.fasterxml.jackson." ^ class
 
 let implements_org_json class_name = implements ("org.json." ^ class_name)
 
+let implements_app_activity = implements "android.app.Activity"
+
+let implements_app_fragment = implements "androidx.fragment.app.Fragment"
+
+let implements_graphql_story = implements "com.facebook.graphql.model.GraphQLStory"
+
+let implements_psi_element = implements "com.intellij.psi.PsiElement"
+
+let implements_view_group = implements "android.view.ViewGroup"
+
+let implements_view_parent = implements "android.view.ViewParent"
+
 (** The type the method is invoked on *)
 let get_this_type_nonstatic_methods_only proc_attributes =
   match proc_attributes.ProcAttributes.formals with (_, t) :: _ -> Some t | _ -> None
diff --git a/infer/src/absint/PatternMatch.mli b/infer/src/absint/PatternMatch.mli
index 124149b70..74d8af40b 100644
--- a/infer/src/absint/PatternMatch.mli
+++ b/infer/src/absint/PatternMatch.mli
@@ -94,6 +94,24 @@ val implements_android : string -> Tenv.t -> string -> bool
 val implements_infer_annotation : string -> Tenv.t -> string -> bool
 (** Check whether class implements a class of Infer annotation *)
 
+val implements_app_activity : Tenv.t -> string -> bool
+(** Check whether class implements a class of [android.app.Activity] *)
+
+val implements_app_fragment : Tenv.t -> string -> bool
+(** Check whether class implements a class of [androidx.fragment.app.Fragment] *)
+
+val implements_graphql_story : Tenv.t -> string -> bool
+(** Check whether class implements a class of [com.facebook.graphql.model.GraphQLStory] *)
+
+val implements_psi_element : Tenv.t -> string -> bool
+(** Check whether class implements a class of [com.intellij.psi.PsiElement] *)
+
+val implements_view_group : Tenv.t -> string -> bool
+(** Check whether class implements a class of [android.view.ViewGroup] *)
+
+val implements_view_parent : Tenv.t -> string -> bool
+(** Check whether class implements a class of [android.view.ViewParent] *)
+
 val implements_xmob_utils : string -> Tenv.t -> string -> bool
 (** Check whether class implements a class of xmod.utils *)
 
diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml
index c2e40b481..f66246a5e 100644
--- a/infer/src/bufferoverrun/absLoc.ml
+++ b/infer/src/bufferoverrun/absLoc.ml
@@ -385,9 +385,10 @@ module Loc = struct
     match (get_path lhs, get_path rhs) with
     | ( Some lhs_path
       , Some
-          (Prim
-            (Deref (Deref_JavaPointer, Field {prefix= Prim (Deref (Deref_JavaPointer, rhs_path))})))
-      )
+          ( Field {prefix= rhs_path}
+          | Prim
+              (Deref
+                (Deref_JavaPointer, Field {prefix= Prim (Deref (Deref_JavaPointer, rhs_path))})) ) )
       when Symb.SymbolPath.equal_partial lhs_path rhs_path ->
         Some lhs
     | _, _ ->
diff --git a/infer/src/bufferoverrun/bufferOverrunField.ml b/infer/src/bufferoverrun/bufferOverrunField.ml
index 168e49e50..ca69f4dfd 100644
--- a/infer/src/bufferoverrun/bufferOverrunField.ml
+++ b/infer/src/bufferoverrun/bufferOverrunField.ml
@@ -35,6 +35,8 @@ let java_linked_list_index = mk "java.linked_list_index" Typ.(int)
 
 let java_linked_list_length = mk "java.linked_list_length" Typ.(int)
 
+let java_linked_list_next typ = mk "java.linked_list_next" typ
+
 let is_java_collection_internal_array fn = Fieldname.equal fn java_collection_internal_array
 
 let c_strlen () =
diff --git a/infer/src/bufferoverrun/bufferOverrunField.mli b/infer/src/bufferoverrun/bufferOverrunField.mli
index 891fc7795..477fbde76 100644
--- a/infer/src/bufferoverrun/bufferOverrunField.mli
+++ b/infer/src/bufferoverrun/bufferOverrunField.mli
@@ -35,6 +35,9 @@ val java_linked_list_index : Fieldname.t
 val java_linked_list_length : Fieldname.t
 (** Virtual field for length of Java's linked list *)
 
+val java_linked_list_next : Typ.t -> Fieldname.t
+(** Virtual field for next of Java's linked list *)
+
 val is_cpp_vector_elem : Fieldname.t -> bool
 (** Check if the field is for C++ vector's elements *)
 
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index bf4aacb0f..cacae3768 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -1105,6 +1105,23 @@ module JavaClass = struct
     {exec; check= no_check}
 end
 
+module JavaLinkedList = struct
+  let next {exp; typ} =
+    let exec _model_env ~ret:(ret_id, _) mem =
+      match exp with
+      | Exp.Var id -> (
+        match Dom.Mem.find_simple_alias id mem with
+        | [(l, zero)] when IntLit.iszero zero ->
+            let fn = BufferOverrunField.java_linked_list_next typ in
+            model_by_value (Loc.append_field l fn |> Dom.Val.of_loc) ret_id mem
+        | _ ->
+            mem )
+      | _ ->
+          mem
+    in
+    {exec; check= no_check}
+end
+
 module JavaString = struct
   let fn = BufferOverrunField.java_collection_internal_array
 
@@ -1648,5 +1665,15 @@ module Call = struct
         &:: "put" <>$ capt_var_exn $+...$--> Collection.put
       ; +PatternMatch.implements_pseudo_collection
         &:: "put" <>$ capt_var_exn $+ any_arg $+ any_arg $--> Collection.put
-      ; +PatternMatch.implements_pseudo_collection &:: "size" <>$ capt_exp $!--> Collection.size ]
+      ; +PatternMatch.implements_pseudo_collection &:: "size" <>$ capt_exp $!--> Collection.size
+      ; (* Java linked list models *)
+        +PatternMatch.implements_app_activity &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next
+      ; +PatternMatch.implements_app_fragment
+        &:: "getParentFragment" <>$ capt_arg $!--> JavaLinkedList.next
+      ; +PatternMatch.implements_graphql_story
+        &:: "getAttachedStory" <>$ capt_arg $!--> JavaLinkedList.next
+      ; +PatternMatch.implements_psi_element &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next
+      ; +PatternMatch.implements_view_group &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next
+      ; +PatternMatch.implements_view_parent &:: "getParent" <>$ capt_arg $!--> JavaLinkedList.next
+      ]
 end
diff --git a/infer/tests/codetoanalyze/java/performance/Loops.java b/infer/tests/codetoanalyze/java/performance/Loops.java
index 3e1d4bdf8..95f161677 100644
--- a/infer/tests/codetoanalyze/java/performance/Loops.java
+++ b/infer/tests/codetoanalyze/java/performance/Loops.java
@@ -6,6 +6,7 @@
  */
 package codetoanalyze.java.performance;
 
+import android.app.Activity;
 import java.io.IOException;
 import java.nio.ByteBuffer;
 import java.nio.channels.FileChannel;
@@ -150,4 +151,10 @@ public class Loops {
     }
     loop_linear(n);
   }
+
+  void linked_list_model_linear(Activity p) {
+    while (p != null) {
+      p = p.getParent();
+    }
+  }
 }
diff --git a/infer/tests/codetoanalyze/java/performance/cost-issues.exp b/infer/tests/codetoanalyze/java/performance/cost-issues.exp
index 9d5766af1..6cae384f1 100644
--- a/infer/tests/codetoanalyze/java/performance/cost-issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/cost-issues.exp
@@ -264,19 +264,20 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops$
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops$MyLinkedList.<init>(codetoanalyze.java.performance.Loops), 6,  OnUIThread:false, []
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops$MyLinkedList.getNext():codetoanalyze.java.performance.Loops$MyLinkedList, 4,  OnUIThread:false, []
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.<init>(), 3,  OnUIThread:false, []
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 5 + 5 ⋅ seq.length + 3 ⋅ (seq.length + 1),  OnUIThread:false, [{seq.length + 1},Loop at line 115,{seq.length},Loop at line 115]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 5 + 5 ⋅ seq.length + 3 ⋅ (seq.length + 1),  OnUIThread:false, [{seq.length + 1},Loop at line 116,{seq.length},Loop at line 116]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p_constant(int):int, 253,  OnUIThread:false, []
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort_quadratic(long[],long[],int):void, 5 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length,  OnUIThread:false, [{length},Loop at line 54,{length - 1},Loop at line 55,{length - 1},Loop at line 54]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb_linear(long[],int):void, 5 + 25 ⋅ (length - 1),  OnUIThread:false, [{length - 1},Loop at line 44]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, ⊤,  OnUIThread:false, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 86]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_simple_linear(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3 + 10 ⋅ (p.linked_list_length + 1),  OnUIThread:false, [{p.linked_list_length + 1},Loop at line 140]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_linear(int):void, 5 + 5 ⋅ x,  OnUIThread:false, [{x},Loop at line 86]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort_quadratic(long[],long[],int):void, 5 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length,  OnUIThread:false, [{length},Loop at line 55,{length - 1},Loop at line 56,{length - 1},Loop at line 55]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb_linear(long[],int):void, 5 + 25 ⋅ (length - 1),  OnUIThread:false, [{length - 1},Loop at line 45]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, ⊤,  OnUIThread:false, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 87]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_simple_linear(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3 + 10 ⋅ (p.linked_list_length + 1),  OnUIThread:false, [{p.linked_list_length + 1},Loop at line 141]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linked_list_model_linear(android.app.Activity):void, 3 + 7 ⋅ (p.linked_list_length + 1),  OnUIThread:false, [{p.linked_list_length + 1},Loop at line 156]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_linear(int):void, 5 + 5 ⋅ x,  OnUIThread:false, [{x},Loop at line 87]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 6 + 14 ⋅ FileChannel.read(...).modeled,  OnUIThread:false, [{FileChannel.read(...).modeled},Modeled call to read(...)]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, ⊤,  OnUIThread:false, [Unbounded loop,Loop at line 34]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_linear(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 47 + 26 ⋅ x.length,  OnUIThread:false, [{x.length},Loop at line 77]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_concat_linear(java.lang.String,java.lang.String):void, 11 + 5 ⋅ (p.length + s.length) + 3 ⋅ (p.length + s.length + 1),  OnUIThread:false, [{p.length + s.length + 1},Loop at line 103,{p.length + s.length},Loop at line 103]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_length_linear(java.lang.String):void, 5 + 5 ⋅ s.length + 3 ⋅ (s.length + 1),  OnUIThread:false, [{s.length + 1},Loop at line 98,{s.length},Loop at line 98]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol_FP():void, ⊤,  OnUIThread:false, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 86]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, ⊤,  OnUIThread:false, [Unbounded loop,Loop at line 35]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_linear(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 47 + 26 ⋅ x.length,  OnUIThread:false, [{x.length},Loop at line 78]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_concat_linear(java.lang.String,java.lang.String):void, 11 + 5 ⋅ (p.length + s.length) + 3 ⋅ (p.length + s.length + 1),  OnUIThread:false, [{p.length + s.length + 1},Loop at line 104,{p.length + s.length},Loop at line 104]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_length_linear(java.lang.String):void, 5 + 5 ⋅ s.length + 3 ⋅ (s.length + 1),  OnUIThread:false, [{s.length + 1},Loop at line 99,{s.length},Loop at line 99]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol_FP():void, ⊤,  OnUIThread:false, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 87]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.zeropad_linear_FN(java.lang.String,java.lang.String):void, 18,  OnUIThread:false, []
 codetoanalyze/java/performance/MapTest.java, MapTest.<init>(), 3,  OnUIThread:false, []
 codetoanalyze/java/performance/MapTest.java, MapTest.entrySet_linear(java.util.Map):void, 9 + 8 ⋅ map.length + 3 ⋅ (map.length + 1),  OnUIThread:false, [{map.length + 1},Loop at line 17,{map.length},Loop at line 17]
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index e13c33ab6..74f227060 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/infer/tests/codetoanalyze/java/performance/issues.exp
@@ -62,13 +62,13 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.escape(java.lang.StringBuilder,java.lang.String):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.String):java.lang.StringBuilder, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Call to void JsonUtils.serialize(StringBuilder,String),Call to void JsonUtils.escape(StringBuilder,String),Unbounded loop,Loop at line 13]
 codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.utils.json.JsonUtils.serialize(java.lang.StringBuilder,java.lang.String):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Call to void JsonUtils.escape(StringBuilder,String),Unbounded loop,Loop at line 13]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 86]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 87]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32 by call to `void Loops.loop_linear(int)` ]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 8):signed32]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 34]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 35]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol_FP():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 86]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol_FP():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.loop_linear(int),Loop at line 87]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol_FP():void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] × [-oo, +oo]):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32 by call to `void Loops.loop_linear(int)` ]
 codetoanalyze/java/performance/StringTest.java, StringTest.class_get_canonical_name_constant(java.lang.Integer):void, 1, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: Class Object.getClass(),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]