[quandary] remove assignments to formals from summaries

Summary: Java is call-by-value; you can't reassign a parameter.

Reviewed By: jeremydubreil

Differential Revision: D4754711

fbshipit-source-id: ade0d7f

infer/src/quandary/TaintAnalysis.ml

@@ -482,11 +482,22 @@ module Make (TaintSpecification : TaintSpec.S) = struct
     let access_tree' =
       AccessPath.BaseMap.fold
         (fun base node acc ->
-           let base' =
-             match FormalMap.get_formal_index base formal_map with
-             | Some formal_index -> make_footprint_var formal_index, snd base
-             | None -> base in
-           AccessPath.BaseMap.add base' node acc)
+           match FormalMap.get_formal_index base formal_map with
+           | Some formal_index ->
+               let base' = make_footprint_var formal_index, snd base in
+               let joined_node =
+                 try TaintDomain.node_join (AccessPath.BaseMap.find base' acc) node
+                 with Not_found -> node in
+               let node' =
+                 if TraceDomain.Sinks.is_empty (TraceDomain.sinks (fst joined_node))
+                 then
+                   (* Java is call-by-value; we can't update a formal in the callee. so drop the
+                      trace associated with the formal unless it contains sinks *)
+                   TraceDomain.empty, snd joined_node
+                 else
+                   joined_node in
+               AccessPath.BaseMap.add base' node' acc
+           | None -> AccessPath.BaseMap.add base node acc)
         access_tree
         TaintDomain.empty in
 

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

@@ -415,16 +415,14 @@ class Interprocedural {
     o = InferTaint.inferSecretSource();
   }
 
-  // need to understand that Java is call-by-value for this...
-  public static void FP_swapParamsOk() {
+  public static void swapParamsOk() {
     Object notASource = null;
     Object source = InferTaint.inferSecretSource();
     swapParams(notASource, source);
     InferTaint.inferSensitiveSink(notASource);
   }
 
-  // ...and this
-  public static void FP_assignSourceToParamOk() {
+  public static void assignSourceToParamOk() {
     Object o = null;
     assignSourceToParam(o);
     InferTaint.inferSensitiveSink(o);

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

@@ -87,10 +87,8 @@ codetoanalyze/java/quandary/Interprocedural.java, Object Interprocedural.irrelev
 codetoanalyze/java/quandary/Interprocedural.java, Object Interprocedural.irrelevantPassthroughsSinkInterprocedural(Object), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),flow through Object Interprocedural.relevantPassthrough(Object),call to Object Interprocedural.callSinkIrrelevantPassthrough(Object),flow through Object Interprocedural.relevantPassthrough(Object),call to void InferTaint.inferSensitiveSink(Object)]
 codetoanalyze/java/quandary/Interprocedural.java, Object Interprocedural.irrelevantPassthroughsSourceAndSinkInterprocedural(Object), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),flow through Object Interprocedural.relevantPassthrough(Object),return from Object Interprocedural.returnSourceIrrelevantPassthrough(Object),flow through Object Interprocedural.relevantPassthrough(Object),call to Object Interprocedural.callSinkIrrelevantPassthrough(Object),flow through Object Interprocedural.relevantPassthrough(Object),call to void InferTaint.inferSensitiveSink(Object)]
 codetoanalyze/java/quandary/Interprocedural.java, Object Interprocedural.irrelevantPassthroughsSourceInterprocedural(Object), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),flow through Object Interprocedural.relevantPassthrough(Object),return from Object Interprocedural.returnSourceIrrelevantPassthrough(Object),flow through Object Interprocedural.relevantPassthrough(Object),call to void InferTaint.inferSensitiveSink(Object)]
-codetoanalyze/java/quandary/Interprocedural.java, void Interprocedural.FP_assignSourceToParamOk(), 3, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),return from void Interprocedural.assignSourceToParam(Object),call to void InferTaint.inferSensitiveSink(Object)]
 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_swapParamsOk(), 4, QUANDARY_TAINT_ERROR, [return from Object InferTaint.inferSecretSource(),flow through void Interprocedural.swapParams(Object,Object),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.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)]