[quandary] make it possible to specify code that should be modeled even if we have a summary

Summary: Have found this useful in Quandary for fbcode, where we want to do this for folly due to its use of assembly (details in comments).

Reviewed By: mbouaziz

Differential Revision: D5167564

fbshipit-source-id: bf6d7e0

infer/src/quandary/ClangTaintAnalysis.ml

@@ -67,6 +67,31 @@ include
       | _ ->
           handle_generic_unknown ret_typ_opt actuals
 
+    (* treat folly functions as unknown library code. we often specify folly functions as sinks,
+       and we don't want to double-report if these functions eventually call other sinks (e.g.,
+       when folly::Subprocess calls exec), in addition some folly functions are heavily optimized in
+       a way that obscures what they're actually doing (e.g., they use assembly code). it's better
+       to write models for these functions or treat them as unknown *)
+    let models_matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["folly"]
+
+    let get_model pname ret_typ_opt actuals tenv summary =
+      (* hack for default C++ constructors, which get translated as an empty body (and will thus
+         have an empty summary). We don't want that because we want to be able to propagate taint
+         from comstructor parameters to the constructed object. so we treat the empty constructor
+         as a skip function instead *)
+      let is_default_constructor pname =
+        Typ.Procname.is_c_method pname &&
+        Typ.Procname.is_constructor pname &&
+        AccessTree.BaseMap.is_empty summary in
+      match pname with
+      | Typ.Procname.ObjC_Cpp _
+        when is_default_constructor pname ||
+             QualifiedCppName.Match.match_qualifiers
+               models_matcher (Typ.Procname.get_qualifiers pname) ->
+          Some (handle_unknown_call pname ret_typ_opt actuals tenv)
+      | _ ->
+          None
+
     let external_sanitizers =
       List.map
         ~f:(fun { QuandaryConfig.Sanitizer.procedure; } ->

infer/src/quandary/JavaTaintAnalysis.ml

@@ -74,6 +74,8 @@ include
       | pname ->
           failwithf "Non-Java procname %a in Java analysis@." Typ.Procname.pp pname
 
+    let get_model _ _ _ _ _ = None
+
     let external_sanitizers =
       List.map
         ~f:(fun { QuandaryConfig.Sanitizer.procedure; } -> Str.regexp procedure)

infer/src/quandary/TaintAnalysis.ml

@@ -272,7 +272,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
 
       TaintDomain.trace_fold
         add_to_caller_tree
-        (TaintSpecification.of_summary_access_tree summary)
+        summary
         caller_access_tree
 
     let exec_instr (astate : Domain.astate) (proc_data : extras ProcData.t) _ (instr : HilInstr.t) =
@@ -301,7 +301,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
           exec_write lhs_access_path rhs_exp astate
 
       | Call (ret_opt, Direct called_pname, actuals, call_flags, callee_loc) ->
-          let handle_unknown_call callee_pname access_tree =
+          let handle_model callee_pname access_tree model =
             let is_variadic = match callee_pname with
               | Typ.Procname.Java pname ->
                   begin
@@ -336,7 +336,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct
               else
                 let trace' = TraceDomain.update_sources trace_with_propagation filtered_sources in
                 TaintDomain.add_trace access_path trace' access_tree in
-            let handle_unknown_call_ astate_acc propagation =
+            let handle_model_ astate_acc propagation =
               match propagation, actuals, ret_opt with
               | _, [], _ ->
                   astate_acc
@@ -356,7 +356,9 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                   end
               | _ ->
                   astate_acc in
+            List.fold ~f:handle_model_ ~init:access_tree model in
 
+          let handle_unknown_call callee_pname access_tree =
             match Typ.Procname.get_method callee_pname with
             | "operator=" when not (Typ.Procname.is_java callee_pname) ->
                 (* treat unknown calls to C++ operator= as assignment *)
@@ -368,13 +370,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                       failwithf "Unexpected call to operator= %a" HilInstr.pp instr
                 end
             | _ ->
-                let propagations =
+                let model =
                   TaintSpecification.handle_unknown_call
                     callee_pname
                     (Option.map ~f:snd ret_opt)
                     actuals
                     proc_data.tenv in
-                List.fold ~f:handle_unknown_call_ ~init:access_tree propagations in
+                handle_model callee_pname access_tree model in
 
           let dummy_ret_opt = match ret_opt with
             | None when not (Typ.Procname.is_java called_pname) ->
@@ -412,24 +414,25 @@ module Make (TaintSpecification : TaintSpec.S) = struct
                   astate_with_sink in
 
             let astate_with_summary =
-              (* hack for default C++ constructors, which get translated as an empty body (and
-                 will thus have an empty summary). We don't want that because we want to be able to
-                 propagate taint from comstructor parameters to the constructed object. so we treat
-                 the empty constructor as a skip function instead *)
-              let is_dummy_cpp_constructor summary pname =
-                Typ.Procname.is_c_method pname &&
-                Typ.Procname.is_constructor pname &&
-                TaintDomain.BaseMap.is_empty (TaintSpecification.of_summary_access_tree summary) in
               if sinks <> [] || Option.is_some source
               then
                 (* don't use a summary for a procedure that is a direct source or sink *)
                 astate_with_source
               else
                 match Summary.read_summary proc_data.pdesc callee_pname with
-                | Some summary when not (is_dummy_cpp_constructor summary callee_pname) ->
-                    apply_summary ret_opt actuals summary astate_with_source proc_data call_site
-                | _ ->
-                    handle_unknown_call callee_pname astate_with_source in
+                | None ->
+                    handle_unknown_call callee_pname astate_with_source
+                | Some summary ->
+                    let ret_typ_opt = Option.map ~f:snd ret_opt in
+                    let access_tree = TaintSpecification.of_summary_access_tree summary in
+                    match
+                      TaintSpecification.get_model
+                        callee_pname ret_typ_opt  actuals proc_data.tenv access_tree with
+                    | Some model ->
+                        handle_model callee_pname astate_with_source model
+                    | None ->
+                        apply_summary
+                          ret_opt actuals access_tree astate_with_source proc_data call_site in
 
             let astate_with_sanitizer =
               match dummy_ret_opt with

infer/src/quandary/TaintSpec.ml

@@ -12,7 +12,7 @@ open! IStd
 (** combination of a trace with functions for handling unknown code and converting to and from
     summaries *)
 
-type handle_unknown =
+type action =
   | Propagate_to_actual of int
   (** Propagate taint from all actuals to the actual with the given index *)
   | Propagate_to_receiver
@@ -30,7 +30,12 @@ module type S = sig
   (** return a summary for handling an unknown call at the given site with the given return type
       and actuals *)
   val handle_unknown_call :
-    Typ.Procname.t -> Typ.t option -> HilExp.t list -> Tenv.t -> handle_unknown list
+    Typ.Procname.t -> Typ.t option -> HilExp.t list -> Tenv.t -> action list
+
+  (** returns a model that should be used for the given (procname, return type, actuals, summary)
+      instead of using the summary for the procname *)
+  val get_model :
+    Typ.Procname.t -> Typ.t option -> HilExp.t list -> Tenv.t -> AccessTree.t -> action list option
 
   (** return true if the given typ can be tainted *)
   val is_taintable_type : Typ.t -> bool

infer/src/unit/TaintTests.ml

@@ -47,6 +47,7 @@ module MockTaintAnalysis = TaintAnalysis.Make(struct
     let to_summary_access_tree _ = assert false
     let handle_unknown_call _ _ _ _ = []
     let is_taintable_type _ = true
+    let get_model _ _ _ _ _ = None
     let get_sanitizer _ = None
   end)