[quandary] get rid of report_reachable bool in taint specifications

Summary: We were almost always using `~report_reachable:true`, and in the cases where we weren't it is fine to do so. In general, a sink could read any state from its parameters, so it makes sense to complain if anything reachable from them is tainted.

Reviewed By: mbouaziz

Differential Revision: D5169067

fbshipit-source-id: ea7d659

infer/src/checkers/Sink.ml

@@ -16,7 +16,7 @@ module type Kind = sig
   include TraceElem.Kind
 
   (** return the parameter index and sink kind for the given call site with the given actuals *)
-  val get : Typ.Procname.t -> HilExp.t list -> Tenv.t -> (t * int * bool) list
+  val get : Typ.Procname.t -> HilExp.t list -> Tenv.t -> (t * int) list
 end
 
 module type S = sig
@@ -28,9 +28,6 @@ module type S = sig
       (** sink type of the parameter *)
       index : int;
       (** index of the parameter *)
-      report_reachable : bool;
-      (** if true, report if *any* value heap-reachable from the sink parameter is a source.
-          if false, report only if the value passed to the sink is itself a source *)
     }
 
   (** return the parameter index and sink kind for the given call site with the given actuals *)
@@ -52,9 +49,6 @@ module Make (Kind : Kind) = struct
       (** sink type of the parameter *)
       index : int;
       (** index of the parameter *)
-      report_reachable : bool;
-      (** if true, report if *any* value heap-reachable from the sink parameter is a source.
-          if false, report only if the value passed to the sink is itself a source *)
     }
 
   let kind t =
@@ -66,13 +60,12 @@ module Make (Kind : Kind) = struct
   let make kind site =
     { kind; site; }
 
-  let make_sink_param sink index ~report_reachable =
+  let make_sink_param sink index =
-    { sink; index; report_reachable; }
+    { sink; index; }
 
   let get site actuals tenv =
     List.map
-      ~f:(fun (kind, index, report_reachable) ->
+      ~f:(fun (kind, index) -> make_sink_param (make kind site) index)
-         make_sink_param (make kind site) index ~report_reachable)
       (Kind.get (CallSite.pname site) actuals tenv)
 
   let with_callsite t callee_site =

infer/src/checkers/Sink.mli

@@ -13,7 +13,7 @@ module type Kind = sig
   include TraceElem.Kind
 
   (** return the parameter index and sink kind for the given call site with the given actuals *)
-  val get : Typ.Procname.t -> HilExp.t list -> Tenv.t -> (t * int * bool) list
+  val get : Typ.Procname.t -> HilExp.t list -> Tenv.t -> (t * int) list
 end
 
 module type S = sig
@@ -25,9 +25,6 @@ module type S = sig
       (** sink type of the parameter *)
       index : int;
       (** index of the parameter *)
-      report_reachable : bool;
-      (** if true, report if *any* value heap-reachable from the sink parameter is a source.
-          if false, report only if the value passed to the sink is itself a source *)
     }
 
   (** return the parameter index and sink kind for the given call site with the given actuals *)

infer/src/checkers/SinkTrace.ml

@@ -32,7 +32,7 @@ end
 
 module MakeSink(TraceElem : TraceElem.S) = struct
   include TraceElem
-  type parameter = { sink : t; index : int; report_reachable : bool; }
+  type parameter = { sink : t; index : int; }
 
   let get _ _ _ = []
 end

infer/src/quandary/ClangTrace.ml

@@ -127,13 +127,11 @@ module SinkKind = struct
       (QuandaryConfig.Sink.of_json Config.quandary_sinks)
 
   (* taint the nth parameter (0-indexed) *)
-  let taint_nth n kind ~report_reachable =
+  let taint_nth n kind =
-    [kind, n, report_reachable]
+    [kind, n]
 
-  let taint_all actuals kind ~report_reachable =
+  let taint_all actuals kind =
-    List.mapi
+    List.mapi ~f:(fun actual_num _ -> kind, actual_num) actuals
-      ~f:(fun actual_num _ -> kind, actual_num, report_reachable)
-      actuals
 
   (* return Some(sink kind) if [procedure_name] is in the list of externally specified sinks *)
   let get_external_sink pname actuals =
@@ -145,10 +143,10 @@ module SinkKind = struct
             let kind = of_string kind in
             try
               let n = int_of_string index in
-              Some (taint_nth n kind ~report_reachable:true)
+              Some (taint_nth n kind)
             with Failure _ ->
               (* couldn't parse the index, just taint everything *)
-              Some (taint_all actuals kind ~report_reachable:true)
+              Some (taint_all actuals kind)
           else
             None)
       external_sinks
@@ -161,9 +159,9 @@ module SinkKind = struct
         begin
           match Typ.Procname.to_string pname with
           | "execl" | "execlp" | "execle" | "execv" | "execve" | "execvp" | "system" ->
-              taint_all actuals ShellExec ~report_reachable:false
+              taint_all actuals ShellExec
           | "brk" | "calloc" | "malloc" | "realloc" | "sbrk" ->
-              taint_all actuals Allocation ~report_reachable:false
+              taint_all actuals Allocation
           | _ ->
               Option.value (get_external_sink pname actuals) ~default:[]
         end

infer/src/quandary/JavaTrace.ml

@@ -213,41 +213,41 @@ module SinkKind = struct
   let get pname actuals tenv =
     (* taint all the inputs of [pname]. for non-static procedures, taints the "this" parameter only
        if [taint_this] is true. *)
-    let taint_all ?(taint_this=false) kind ~report_reachable =
+    let taint_all ?(taint_this=false) kind =
       let actuals_to_taint, offset =
         if Typ.Procname.java_is_static pname || taint_this
         then actuals, 0
         else List.tl_exn actuals, 1 in
       List.mapi
-        ~f:(fun param_num _ -> kind, param_num + offset, report_reachable)
+        ~f:(fun param_num _ -> kind, param_num + offset)
         actuals_to_taint in
     (* taint the nth non-"this" parameter (0-indexed) *)
-    let taint_nth n kind ~report_reachable =
+    let taint_nth n kind =
       let first_index = if Typ.Procname.java_is_static pname then n else n + 1 in
-      [kind, first_index, report_reachable] in
+      [kind, first_index] in
     match pname with
     | Typ.Procname.Java java_pname ->
         begin
           match Typ.Procname.java_get_class_name java_pname,
                 Typ.Procname.java_get_method java_pname with
           | "android.util.Log", ("e" | "println" | "w" | "wtf") ->
-              taint_all Logging ~report_reachable:true
+              taint_all Logging
           | "java.io.File", "<init>"
           | "java.nio.file.FileSystem", "getPath"
           | "java.nio.file.Paths", "get" ->
-              taint_all CreateFile ~report_reachable:true
+              taint_all CreateFile
           | "com.facebook.infer.builtins.InferTaint", "inferSensitiveSink" ->
-              [Other, 0, false]
+              [Other, 0]
           | class_name, method_name ->
               let taint_matching_supertype typename _ =
                 match Typ.Name.name typename, method_name with
                 | "android.app.Activity",
                   ("startActivityFromChild" | "startActivityFromFragment") ->
-                    Some (taint_nth 1 StartComponent ~report_reachable:true)
+                    Some (taint_nth 1 StartComponent)
                 | "android.app.Activity", "startIntentSenderForResult"  ->
-                    Some (taint_nth 2 StartComponent ~report_reachable:true)
+                    Some (taint_nth 2 StartComponent)
                 | "android.app.Activity", "startIntentSenderFromChild"  ->
-                    Some (taint_nth 3 StartComponent ~report_reachable:true)
+                    Some (taint_nth 3 StartComponent)
                 | "android.content.Context",
                   ("bindService" |
                    "sendBroadcast" |
@@ -265,9 +265,9 @@ module SinkKind = struct
                    "startNextMatchingActivity" |
                    "startService" |
                    "stopService") ->
-                    Some (taint_nth 0 StartComponent ~report_reachable:true)
+                    Some (taint_nth 0 StartComponent)
                 | "android.content.Context", "startIntentSender" ->
-                    Some (taint_nth 1 StartComponent ~report_reachable:true)
+                    Some (taint_nth 1 StartComponent)
                 | "android.content.Intent",
                   ("parseUri" |
                    "getIntent" |
@@ -278,9 +278,9 @@ module SinkKind = struct
                    "setDataAndType" |
                    "setDataAndTypeAndNormalize" |
                    "setPackage") ->
-                    Some (taint_nth 0 CreateIntent ~report_reachable:true)
+                    Some (taint_nth 0 CreateIntent)
                 | "android.content.Intent", "setClassName" ->
-                    Some (taint_all CreateIntent ~report_reachable:true)
+                    Some (taint_all CreateIntent)
                 | "android.webkit.WebView",
                   ("evaluateJavascript" |
                    "loadData" |
@@ -288,7 +288,7 @@ module SinkKind = struct
                    "loadUrl" |
                    "postUrl" |
                    "postWebMessage") ->
-                    Some (taint_all JavaScript ~report_reachable:true)
+                    Some (taint_all JavaScript)
                 | class_name, method_name ->
                     (* check the list of externally specified sinks *)
                     let procedure = class_name ^ "." ^ method_name in
@@ -299,10 +299,10 @@ module SinkKind = struct
                             let kind = of_string kind in
                             try
                               let n = int_of_string index in
-                              Some (taint_nth n kind ~report_reachable:true)
+                              Some (taint_nth n kind)
                             with Failure _ ->
                               (* couldn't parse the index, just taint everything *)
-                              Some (taint_all kind ~report_reachable:true)
+                              Some (taint_all kind)
                           else
                             None)
                       external_sinks in

infer/src/quandary/TaintAnalysis.ml

@@ -163,21 +163,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
       let add_sink_to_actual access_tree_acc (sink_param : TraceDomain.Sink.parameter) =
         match List.nth_exn actuals sink_param.index with
         | HilExp.AccessPath actual_ap_raw ->
-            let actual_ap =
+            let actual_ap = AccessPath.Abstracted actual_ap_raw in
-              let is_array_typ =
-                match AccessPath.Raw.get_typ actual_ap_raw proc_data.ProcData.tenv with
-                | Some
-                    ({ desc=(
-                         Typ.Tptr ({desc=Tarray _}, _) (* T* [] (Java-style) *)
-                       | Tptr ({desc=Tptr _}, _) (* T** (C/C++ style 1) *)
-                       | Tarray _ )}) (* T[] C/C++ style 2 *) ->
-                    true
-                | _ ->
-                    false in
-              (* conisder any sources that are reachable from an array *)
-              if sink_param.report_reachable || is_array_typ
-              then AccessPath.Abstracted actual_ap_raw
-              else AccessPath.Exact actual_ap_raw in
             begin
               match access_path_get_node actual_ap access_tree_acc proc_data with
               | Some (actual_trace, _) ->

infer/src/unit/TaintTests.ml

@@ -32,7 +32,7 @@ module MockTrace = Trace.Make(struct
 
         let get pname _ _ =
           if String.is_prefix ~prefix:"SINK" (Typ.Procname.to_string pname)
-          then [CallSite.make pname Location.dummy, 0, false]
+          then [CallSite.make pname Location.dummy, 0]
           else []
       end)
 
@@ -181,14 +181,14 @@ let tests =
     [
       assign_to_source "ret_id";
       call_sink "ret_id";
-      invariant "{ ret_id$0 => (SOURCE -> SINK) }";
+      invariant "{ ret_id$0* => (SOURCE -> SINK) }";
     ];
     "source -> sink via var",
     [
       assign_to_source "ret_id";
       var_assign_id "actual" "ret_id";
       call_sink_with_exp (var_of_str "actual");
-      invariant "{ ret_id$0 => (SOURCE -> ?), &actual => (SOURCE -> SINK) }";
+      invariant "{ ret_id$0 => (SOURCE -> ?), &actual* => (SOURCE -> SINK) }";
     ];
     "source -> sink via var then ident",
     [
@@ -196,7 +196,7 @@ let tests =
       var_assign_id "x" "ret_id";
       id_assign_var "actual_id" "x";
       call_sink "actual_id";
-      invariant "{ ret_id$0 => (SOURCE -> ?), &x => (SOURCE -> SINK) }";
+      invariant "{ ret_id$0 => (SOURCE -> ?), &x* => (SOURCE -> SINK) }";
     ];
     "source -> sink via field",
     [
@@ -204,7 +204,7 @@ let tests =
       assign_id_to_field "base_id" "f" "ret_id";
       read_field_to_id "actual_id" "base_id" "f";
       call_sink "actual_id";
-      invariant "{ base_id$0.f => (SOURCE -> SINK), ret_id$0 => (SOURCE -> ?) }";
+      invariant "{ base_id$0.f* => (SOURCE -> SINK), ret_id$0 => (SOURCE -> ?) }";
     ];
     "source -> sink via field read from var",
     [
@@ -215,14 +215,14 @@ let tests =
       read_field_to_id "read_id" "var_id" "f";
       call_sink "read_id";
       invariant
-        "{ base_id$0.f => (SOURCE -> ?), ret_id$0 => (SOURCE -> ?), &var.f => (SOURCE -> SINK) }";
+        "{ base_id$0.f => (SOURCE -> ?), ret_id$0 => (SOURCE -> ?), &var.f* => (SOURCE -> SINK) }";
     ];
     "source -> sink via cast",
     [
       assign_to_source "ret_id";
       cast_id_to_id "cast_id" (Typ.mk Tvoid) "ret_id";
       call_sink "cast_id";
-      invariant "{ ret_id$0 => (SOURCE -> SINK) }";
+      invariant "{ ret_id$0* => (SOURCE -> SINK) }";
     ];
 
   ] |> TestInterpreter.create_tests

infer/src/unit/TraceTests.ml

@@ -63,7 +63,7 @@ end
 
 module MockSink = struct
   include MockTraceElem
-  type parameter = { sink : t; index : int; report_reachable : bool; }
+  type parameter = { sink : t; index : int; }
 
   let get _ = assert false
 

infer/tests/codetoanalyze/java/quandary/Arrays.java

@@ -52,12 +52,6 @@ public class Arrays {
     InferTaint.inferSensitiveSink(arr[0]);
   }
 
-  void viaArrayThenFieldOk() {
-    Obj[] arr = new Obj[1];
-    arr[0].f = InferTaint.inferSecretSource();
-    InferTaint.inferSensitiveSink(arr[0]);
-  }
-
   /** false positives: an ideal analysis would not report on these, but we do */
 
   // we don't track array indices precisely

infer/tests/codetoanalyze/java/quandary/Fields.java

@@ -65,23 +65,7 @@ public class Fields {
 
   /** should not report on these tests */
 
-  void viaFieldOk1(Obj obj) {
+  void viaFieldOk() {
-    obj.f = InferTaint.inferSecretSource();
-    InferTaint.inferSensitiveSink(obj);
-  }
-
-  void viaFieldOk2() {
-    Obj obj = new Obj();
-    obj.f = InferTaint.inferSecretSource();
-    InferTaint.inferSensitiveSink(obj);
-  }
-
-  void viaFieldOk3(Obj obj) {
-    obj.g.f = InferTaint.inferSecretSource();
-    InferTaint.inferSensitiveSink(obj.g);
-  }
-
-  void viaFieldOk3() {
     Obj obj = new Obj();
     obj.f = InferTaint.inferSecretSource();
     obj.g = new Obj();
@@ -101,17 +85,7 @@ public class Fields {
     InferTaint.inferSensitiveSink(obj.g.f);
   }
 
-  void viaNestedFieldOK2(Obj obj) {
+  void viaNestedFieldOK2() {
-    obj.g.f = InferTaint.inferSecretSource();
-    InferTaint.inferSensitiveSink(obj.g);
-  }
-
-  void viaNestedFieldOK3(Obj obj) {
-    obj.g.f = InferTaint.inferSecretSource();
-    InferTaint.inferSensitiveSink(obj);
-  }
-
-  void viaNestedFieldOK4() {
     Obj obj = new Obj();
     obj.g = new Obj();
     obj.g.f = InferTaint.inferSecretSource();

infer/tests/codetoanalyze/java/quandary/Interprocedural.java

@@ -381,7 +381,7 @@ class Interprocedural {
     callSinkIndirectOnParam(source);
   }
 
-  public void FN_callDeepSink1Bad() {
+  public void callDeepSink1Bad() {
     Obj source = propagate(InferTaint.inferSecretSource());
     callSinkA(source);
   }

infer/tests/codetoanalyze/java/quandary/issues.exp

@@ -127,6 +127,7 @@ codetoanalyze/java/quandary/Interprocedural.java, Object Interprocedural.irrelev
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.FP_divergenceInCallee(), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.FP_reassignInCallee(), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void InferTaint.inferSensitiveSink(Object)]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.FP_trackParamsOk(), 1, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from Object Interprocedural.returnSourceConditional(boolean),call to void InferTaint.inferSensitiveSink(Object)]
+codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callDeepSink1Bad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),flow through Interprocedural$Obj Interprocedural.propagate(Object),call to void Interprocedural.callSinkA(Interprocedural$Obj),call to void Interprocedural.callSink1(Interprocedural$Obj),flow through Object Interprocedural.id(Object),call to void InferTaint.inferSensitiveSink(Object)]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callDeepSink3Bad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),flow through Interprocedural$Obj Interprocedural.propagate(Object),call to void Interprocedural.callSinkC(Interprocedural$Obj),call to void Interprocedural.callSink3(Interprocedural$Obj),flow through Object Interprocedural.id(Object),call to void InferTaint.inferSensitiveSink(Object)]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callDeepSink4Bad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),flow through Interprocedural$Obj Interprocedural.propagate(Object),call to void Interprocedural.callSinkD(Interprocedural$Obj),call to void Interprocedural.callSink4(Interprocedural$Obj),call to void InferTaint.inferSensitiveSink(Object)]
 codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.callDeepSinkIndirectBad(), 2, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),call to void Interprocedural.callSinkIndirectOnParam(Object),call to void Interprocedural.callSinkOnParam(Object),call to void InferTaint.inferSensitiveSink(Object)]