From 831786240a683eca53578291fe4d1b2edec857b6 Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Thu, 8 Dec 2016 14:03:00 -0800
Subject: [PATCH] [quandary] ignore null assignments to return value in void
 functions

Summary:
The Java frontend translates exceptions by assigning them to the return value.
This leads to weird behavior when the return type of the function is void.
Already handled one case of this in Quandary (ignoring assignments of exceptions to return value), but was missing the case where null is assigned to the return value.
The frontend does this to "clear" the value of previously assigned exceptions.

Reviewed By: jeremydubreil

Differential Revision: D4294060

fbshipit-source-id: 6bef5ef
---
 infer/src/quandary/TaintAnalysis.ml                 |  6 ++++++
 infer/tests/codetoanalyze/java/quandary/Basics.java | 10 ++++++++++
 2 files changed, 16 insertions(+)

diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index 244286345..9f58de886 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -308,6 +308,12 @@ module Make (TaintSpecification : TaintSpec.S) = struct
              exception is "returned" from a void function. skip code like this for now
              (fix via t14159157 later *)
           astate
+      | Sil.Store (Exp.Lvar lhs_pvar, _, rhs_exp, _)
+        when Pvar.is_return lhs_pvar && Exp.is_null_literal rhs_exp &&
+             Typ.equal Tvoid (Procdesc.get_ret_type proc_data.pdesc) ->
+          (* similar to the case above; the Java frontend translates "return no exception" as
+             `return null` in a void function *)
+          astate
       | Sil.Store (lhs_exp, lhs_typ, rhs_exp, loc) ->
           let lhs_access_path =
             match AccessPath.of_lhs_exp lhs_exp lhs_typ ~f_resolve_id with
diff --git a/infer/tests/codetoanalyze/java/quandary/Basics.java b/infer/tests/codetoanalyze/java/quandary/Basics.java
index 96640f3df..fcbe123d2 100644
--- a/infer/tests/codetoanalyze/java/quandary/Basics.java
+++ b/infer/tests/codetoanalyze/java/quandary/Basics.java
@@ -199,6 +199,16 @@ public class Basics {
     return o;
   }
 
+  void synchronizedOk(Object o) {
+    synchronized(o) {
+    }
+  }
+
+  // this is to test that we don't crash due to the slightly odd translation of synchronized
+  void callSynchronizedOk(Object o) {
+    synchronizedOk(o);
+  }
+
   /** "known false positive" tests demonstrating limitations. an ideal analysis would not report on
       these tests, but we do. */