[quandary] using summaries part 1: return

Reviewed By: jeremydubreil

Differential Revision: D3857310

fbshipit-source-id: 29c5994

infer/src/checkers/accessPath.ml

@@ -112,6 +112,10 @@ let of_exp exp typ ~(f_resolve_id : Var.t -> raw option) =
 let append (base, old_accesses) new_accesses =
   base, old_accesses @ new_accesses
 
+let with_base_var var = function
+  | Exact ((_, base_typ), accesses) -> Exact ((var, base_typ), accesses)
+  | Abstracted ((_, base_typ), accesses) -> Abstracted ((var, base_typ), accesses)
+
 let rec is_prefix_path path1 path2 =
   if path1 == path2
   then true

infer/src/checkers/accessPath.mli

@@ -54,6 +54,10 @@ val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> raw option) -> raw option
     `x.f.g.h` *)
 val append : raw -> access list -> raw
 
+(** swap base of existing access path for [base_var] (e.g., `with_base_bvar x y.f.g` produces
+    `x.f.g` *)
+val with_base_var : Var.t -> t -> t
+
 (** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *)
 val is_prefix : raw -> raw -> bool
 

infer/src/quandary/QuandarySummary.ml

@@ -30,7 +30,6 @@ type output =
   | Out_return of AccessPath.t
   (** output flows into return value at offset in given access path *)
 
-
 (** enumeration of all the different trace types that are possible (just Java, for now). needed
     because we can't functorize Specs.summary's *)
 type summary_trace =

infer/src/quandary/TaintAnalysis.ml

@@ -164,7 +164,44 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
       let access_tree' = IList.fold_left add_sink_to_actual access_tree sinks in
       { astate with Domain.access_tree = access_tree'; }
 
-    let exec_instr ({ Domain.id_map; } as astate) proc_data _ instr =
+    let apply_summary
+        ret_ids
+        (summary : QuandarySummary.t)
+        (astate_in : Domain.astate)
+        proc_data
+        callee_site =
+      let apply_return ret_ap = function
+        | [ret_id] -> AccessPath.with_base_var (Var.of_id ret_id) ret_ap
+        | [] -> failwith "Have summary for retval, but no ret id to bind it to!"
+        | _ -> failwith "Unimp: summaries for function with multiple return values" in
+
+      let apply_one access_tree (in_out_summary : QuandarySummary.in_out_summary) =
+        let in_trace = match in_out_summary.input with
+          | In_empty ->
+              TraceDomain.initial
+          | In_formal _ | In_global _ ->
+              (* TODO: implement these cases *)
+              assert false in
+        let caller_ap =
+          match in_out_summary.output with
+          | Out_return ret_ap ->
+              apply_return ret_ap ret_ids
+          | Out_formal _ | Out_global _ ->
+              (* TODO: implement these cases *)
+              assert false in
+        let output_trace = TraceDomain.of_summary_trace in_out_summary.output_trace in
+        let appended_trace = TraceDomain.append in_trace output_trace callee_site in
+        let joined_trace =
+          match access_path_get_node caller_ap access_tree proc_data (CallSite.loc callee_site) with
+          | Some (orig_trace, _) -> TraceDomain.join orig_trace appended_trace
+          | None -> appended_trace in
+        TaintDomain.add_trace caller_ap joined_trace access_tree in
+
+      let access_tree = IList.fold_left apply_one astate_in.access_tree summary in
+      { astate_in with access_tree; }
+
+    let exec_instr
+        ({ Domain.id_map; } as astate) (proc_data : AccessPath.base list ProcData.t) _ instr =
       let f_resolve_id = resolve_id id_map in
       match instr with
       | Sil.Load (lhs_id, rhs_exp, rhs_typ, _) ->
@@ -180,7 +217,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
                 failwithf
                   "Assignment to unexpected lhs expression %a in proc %a at loc %a"
                   (Sil.pp_exp pe_text) lhs_exp
-                  Procname.pp (Cfg.Procdesc.get_proc_name (proc_data.ProcData.pdesc))
+                  Procname.pp (Cfg.Procdesc.get_proc_name (proc_data.pdesc))
                   Location.pp loc in
           let astate' =
             analyze_assignment
@@ -211,7 +248,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
                 failwithf
                   "Unexpected cast %a in procedure %a at line %a"
                   (Sil.pp_instr pe_text) instr
-                  Procname.pp (Cfg.Procdesc.get_proc_name (proc_data.ProcData.pdesc))
+                  Procname.pp (Cfg.Procdesc.get_proc_name (proc_data.pdesc))
                   Location.pp loc
           else
             astate
@@ -242,7 +279,15 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
             | _ ->
                 (* this is allowed by SIL, but not currently used in any frontends *)
                 failwith "Unimp: handling multiple return ids" in
-          astate_with_source
+
+          let astate_with_summary =
+            match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with
+            | Some summary ->
+                apply_summary ret_ids summary astate_with_source proc_data call_site
+            | None ->
+                astate_with_source in
+
+          astate_with_summary
       | Sil.Call _ ->
           failwith "Unimp: non-pname call expressions"
       | Sil.Nullify (pvar, _) ->

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

@@ -0,0 +1,66 @@
+/*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package codetoanalyze.java.quandary;
+
+import com.facebook.infer.models.InferTaint;
+
+class Interprocedural {
+
+  Object f;
+
+  static class Obj {
+    Object f;
+  }
+
+  /** source tests */
+
+  public static Object returnSourceDirect() {
+    return InferTaint.inferSecretSource();
+  }
+
+  public static Object returnSourceIndirect() {
+    return InferTaint.inferSecretSource();
+  }
+
+  public static void returnSourceDirectBad() {
+    InferTaint.inferSensitiveSink(returnSourceDirect());
+  }
+
+  public static void returnSourceDirectViaVarBad() {
+    Object source = returnSourceDirect();
+    InferTaint.inferSensitiveSink(source);
+  }
+
+  public static void returnSourceIndirectBad() {
+    InferTaint.inferSensitiveSink(returnSourceIndirect());
+  }
+
+  public static Obj returnSourceViaField() {
+    Obj o = new Obj();
+    o.f = InferTaint.inferSecretSource();
+    return o;
+  }
+
+  public static void returnSourceViaFieldBad() {
+    InferTaint.inferSensitiveSink(returnSourceViaField().f);
+  }
+
+  /** false positives: an ideal analysis would not report these, but we will */
+
+  public static Object returnSourceConditional(boolean b) {
+    if (b) return InferTaint.inferSecretSource();
+    return null;
+  }
+
+  public static void FP_trackParamsOk() {
+    InferTaint.inferSensitiveSink(returnSourceConditional(false));
+  }
+
+}

infer/tests/codetoanalyze/java/quandary/Makefile

@@ -14,6 +14,7 @@ FILES = \
   Arrays.java \
   Basics.java \
   Fields.java \
+  Interprocedural.java \
   LoggingPrivateData.java \
 
 compile:

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

@@ -29,6 +29,11 @@ Fields.java:44: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.infer
 Fields.java:51: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 49]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 51]) via {  }
 Fields.java:56: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 55]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 56]) via {  }
 Fields.java:63: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 62]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 63]) via {  }
+Interprocedural.java:33: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 25]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 33]) via { Object Interprocedural.returnSourceDirect() at [line 33] }
+Interprocedural.java:38: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 25]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 38]) via { Object Interprocedural.returnSourceDirect() at [line 37] }
+Interprocedural.java:42: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 29]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 42]) via { Object Interprocedural.returnSourceIndirect() at [line 42] }
+Interprocedural.java:52: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 47]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 52]) via { Interprocedural$Obj Interprocedural.returnSourceViaField() at [line 52] }
+Interprocedural.java:63: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 58]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 63]) via { Object Interprocedural.returnSourceConditional(boolean) at [line 63] }
 LoggingPrivateData.java:18: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences(String SharedPreferences.getString(String,String) at [line 18]) -> Logging(int Log.d(String,String) at [line 18]) via {  }
 LoggingPrivateData.java:22: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences(String SharedPreferences.getString(String,String) at [line 22]) -> Logging(int Log.d(String,String) at [line 22]) via {  }
 LoggingPrivateData.java:37: ERROR: QUANDARY_TAINT_ERROR Error: SharedPreferences(String SharedPreferences.getString(String,String) at [line 36]) -> Logging(int Log.w(String,Throwable) at [line 37]) via {  }