[backend] differentiate unknown methods and methods with empty summaries

Summary:
Analyses should handle methods whose code is unknown and methods whose summary is a no-op differently.
Previously, this was done correctly for some kinds of methods (e.g., native methods, which were recognized as unknown), but not for others (interface and abstract methods).
This diff makes sure we correctly treat all three kinds as unknown.

Reviewed By: jeremydubreil

Differential Revision: D4142697

fbshipit-source-id: c88cff3

infer/src/checkers/BoundedCallTree.ml

@@ -33,7 +33,7 @@ module SpecSummary = Summary.Make (struct
       { payload with Specs.crashcontext_frame = frame }
 
     let read_from_payload payload =
-      payload.Specs.crashcontext_frame
+      Some payload.Specs.crashcontext_frame
   end)
 
 type extras_t = {

infer/src/checkers/Siof.ml

@@ -19,9 +19,7 @@ module Summary = Summary.Make (struct
       { payload with Specs.siof = Some astate }
 
     let read_from_payload payload =
-      match payload.Specs.siof with
-      | Some astate -> astate
-      | None -> SiofDomain.initial
+      payload.Specs.siof
   end)
 
 module TransferFunctions (CFG : ProcCfg.S) = struct

infer/src/checkers/annotationReachability.ml

@@ -89,8 +89,8 @@ module Summary = Summary.Make (struct
 
     let read_from_payload payload =
       match payload.Specs.calls with
-      | Some call_summary -> Domain.NonBottom (call_summary, Domain.TrackingVar.empty)
-      | None -> Domain.initial
+      | Some call_summary -> Some (Domain.NonBottom (call_summary, Domain.TrackingVar.empty))
+      | None -> None
   end)
 
 (* Warning name when a performance critical method directly or indirectly

infer/src/checkers/summary.ml

@@ -15,7 +15,7 @@ module type Helper = sig
   (* update the specs payload with [summary] *)
   val update_payload : summary -> Specs.payload -> Specs.payload
   (* extract [summmary] from the specs payload *)
-  val read_from_payload : Specs.payload -> summary
+  val read_from_payload : Specs.payload -> summary option
 end
 
 module type S = sig
@@ -44,5 +44,5 @@ module Make (H : Helper) = struct
     Ondemand.analyze_proc_name tenv ~propagate_exceptions:false caller_pdesc callee_pname;
     match Specs.get_summary callee_pname with
     | None -> None
-    | Some summary -> Some (H.read_from_payload summary.Specs.payload)
+    | Some summary -> H.read_from_payload summary.Specs.payload
 end

infer/src/quandary/TaintAnalysis.ml

@@ -21,9 +21,7 @@ module Summary = Summary.Make(struct
       { payload with Specs.quandary = Some summary; }
 
     let read_from_payload payload =
-      match payload.Specs.quandary with
-      | Some summary -> summary
-      | None -> []
+      payload.Specs.quandary
   end)
 
 module Make (TaintSpec : TaintSpec.S) = struct
@@ -517,17 +515,24 @@ module Make (TaintSpec : TaintSpec.S) = struct
           AccessPath.BaseMap.empty
           formals_with_nums in
 
-      Preanal.doit ~handle_dynamic_dispatch:true pdesc dummy_cg tenv;
-      let formals = make_formal_access_paths pdesc in
-      let proc_data = ProcData.make pdesc tenv formals in
-      match Analyzer.compute_post proc_data with
-      | Some { access_tree; } ->
-          let summary = make_summary formals access_tree in
-          Summary.write_summary (Cfg.Procdesc.get_proc_name pdesc) summary;
-      | None ->
-          if Cfg.Node.get_succs (Cfg.Procdesc.get_start_node pdesc) = []
-          then ()
-          else failwith "Couldn't compute post" in
+      let has_body pdesc =
+        let attrs = Cfg.Procdesc.get_attributes pdesc in
+        attrs.is_defined && not attrs.is_abstract in
+      if has_body pdesc
+      then
+        begin
+          Preanal.doit ~handle_dynamic_dispatch:true pdesc dummy_cg tenv;
+          let formals = make_formal_access_paths pdesc in
+          let proc_data = ProcData.make pdesc tenv formals in
+          match Analyzer.compute_post proc_data with
+          | Some { access_tree; } ->
+              let summary = make_summary formals access_tree in
+              Summary.write_summary (Cfg.Procdesc.get_proc_name pdesc) summary;
+          | None ->
+              if Cfg.Node.get_succs (Cfg.Procdesc.get_start_node pdesc) = []
+              then ()
+              else failwith "Couldn't compute post"
+        end in
     let callbacks =
       {
         Ondemand.analyze_ondemand;

infer/tests/codetoanalyze/java/quandary/UnknownCode.java

@@ -13,15 +13,31 @@
 
 /** testing how the analysis handles missing/unknown code */
 
-public class UnknownCode {
+public abstract class UnknownCode {
 
-  native static Object id(Object o);
+  native static Object nativeMethod(Object o);
 
-  public UnknownCode() {}
+  abstract Object abstractMethod(Object o);
 
-  static void propagateViaUnknownCodeBad() {
+  static interface Interface {
+    Object interfaceMethod(Object o);
+  }
+
+  void propagateViaUnknownNativeCodeBad() {
+    Object source = InferTaint.inferSecretSource();
+    Object launderedSource = nativeMethod(source);
+    InferTaint.inferSensitiveSink(launderedSource);
+  }
+
+  static void propagateViaUnknownAbstractCodeBad() {
     Object source = InferTaint.inferSecretSource();
-    Object launderedSource = id(source);
+    Object launderedSource = nativeMethod(source);
+    InferTaint.inferSensitiveSink(launderedSource);
+  }
+
+  static void propagateViaInterfaceCodeBad(Interface i) {
+    Object source = InferTaint.inferSecretSource();
+    Object launderedSource = i.interfaceMethod(source);
     InferTaint.inferSensitiveSink(launderedSource);
   }
 
@@ -37,10 +53,12 @@ static void propagateViaUnknownConstructorOk() {
     InferTaint.inferSensitiveSink(unknownConstructor);
   }
 
-  static void propagateViaUnknownCodeOk() {
-    Object notASource = new UnknownCode();
-    Object launderedSource = id(notASource);
-    InferTaint.inferSensitiveSink(launderedSource);
+  void propagateViaUnknownCodeOk(Interface i) {
+    Object notASource = new Object();
+    Object launderedSource1 = nativeMethod(notASource);
+    Object launderedSource2 = abstractMethod(launderedSource1);
+    Object launderedSource3 = i.interfaceMethod(launderedSource2);
+    InferTaint.inferSensitiveSink(launderedSource3);
   }
 
 }

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

@@ -25,11 +25,11 @@ Basics.java:160: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.infe
 Basics.java:166: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 164]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 166]) 
 Basics.java:209: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 206]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 209]) 
 Basics.java:218: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 214]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 218]) 
-DynamicDispatch.java:77: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object DynamicDispatch$BadInterfaceImpl1.returnSource() at [line 76]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 77]) 
-DynamicDispatch.java:77: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object DynamicDispatch$BadInterfaceImpl2.returnSource() at [line 76]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 77]) 
+DynamicDispatch.java:77: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object DynamicDispatch$BadInterfaceImpl1.returnSource() at [line 76]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 77]) (via { Object DynamicDispatch$Interface.returnSource() at [line 76] })
+DynamicDispatch.java:77: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object DynamicDispatch$BadInterfaceImpl2.returnSource() at [line 76]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 77]) (via { Object DynamicDispatch$Interface.returnSource() at [line 76] })
 DynamicDispatch.java:82: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 81]) -> Other(void DynamicDispatch$BadInterfaceImpl1.callSink(Object) at [line 82]) 
 DynamicDispatch.java:82: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 81]) -> Other(void DynamicDispatch$BadInterfaceImpl2.callSink(Object) at [line 82]) 
-DynamicDispatch.java:88: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 86]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 88]) (via { Object DynamicDispatch$BadInterfaceImpl1.propagate(Object) at [line 87], Object DynamicDispatch$BadInterfaceImpl2.propagate(Object) at [line 87] })
+DynamicDispatch.java:88: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 86]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 88]) (via { Object DynamicDispatch$BadInterfaceImpl1.propagate(Object) at [line 87], Object DynamicDispatch$BadInterfaceImpl2.propagate(Object) at [line 87], Object DynamicDispatch$Interface.propagate(Object) at [line 87] })
 DynamicDispatch.java:135: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object DynamicDispatch$BadSubtype.returnSource() at [line 134]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 135]) 
 DynamicDispatch.java:140: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 139]) -> Other(void DynamicDispatch$BadSubtype.callSink(Object) at [line 140]) 
 DynamicDispatch.java:146: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 144]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 146]) (via { Object DynamicDispatch$BadSubtype.propagate(Object) at [line 145] })
@@ -153,5 +153,7 @@ Strings.java:43: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.infe
 Strings.java:50: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 47]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 50]) (via { StringBuffer StringBuffer.append(Object) at [line 49], String StringBuffer.toString() at [line 50] })
 Strings.java:56: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 54]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 56]) (via { Formatter Formatter.format(String,java.lang.Object[]) at [line 56], String Formatter.toString() at [line 56] })
 Strings.java:63: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 60]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 63]) (via { Formatter Formatter.format(String,java.lang.Object[]) at [line 62], String Formatter.toString() at [line 63] })
-UnknownCode.java:25: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 23]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 25]) (via { Object UnknownCode.id(Object) at [line 24] })
-UnknownCode.java:32: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 29]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 32]) (via { String.<init>(String) at [line 31] })
+UnknownCode.java:29: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 27]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 29]) (via { Object UnknownCode.nativeMethod(Object) at [line 28] })
+UnknownCode.java:35: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 33]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 35]) (via { Object UnknownCode.nativeMethod(Object) at [line 34] })
+UnknownCode.java:41: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 39]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 41]) (via { Object UnknownCode$Interface.interfaceMethod(Object) at [line 40] })
+UnknownCode.java:48: ERROR: QUANDARY_TAINT_ERROR Error: Other(Object InferTaint.inferSecretSource() at [line 45]) -> Other(void InferTaint.inferSensitiveSink(Object) at [line 48]) (via { String.<init>(String) at [line 47] })