From 856f84aaff5e0e51f4f37b1ebb605916a3cc1a3b Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 12 Oct 2016 13:20:07 -0700 Subject: [PATCH] [quandary] skeleton for C++ analysis Differential Revision: D3998518 fbshipit-source-id: e90c46d --- infer/src/checkers/registerCheckers.ml | 1 + infer/src/quandary/CppTaintAnalysis.ml | 27 ++++ infer/src/quandary/CppTrace.ml | 193 ++++++++++++++++++++++++ infer/src/quandary/JavaTaintAnalysis.ml | 2 +- infer/src/quandary/QuandarySummary.ml | 2 + infer/src/quandary/QuandarySummary.mli | 1 + 6 files changed, 225 insertions(+), 1 deletion(-) create mode 100644 infer/src/quandary/CppTaintAnalysis.ml create mode 100644 infer/src/quandary/CppTrace.ml diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index dd6b4885f..19c019a4f 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -48,6 +48,7 @@ let active_procedure_checkers () = Checkers.callback_print_c_method_calls, false; CheckDeadCode.callback_check_dead_code, false; Checkers.callback_print_access_to_globals, false; + CppTaintAnalysis.checker, Config.quandary; ] in IList.map (fun (x, y) -> (x, y, Some Config.Clang)) l in diff --git a/infer/src/quandary/CppTaintAnalysis.ml b/infer/src/quandary/CppTaintAnalysis.ml new file mode 100644 index 000000000..b73e77287 --- /dev/null +++ b/infer/src/quandary/CppTaintAnalysis.ml @@ -0,0 +1,27 @@ +(* + * 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. + *) + +open! Utils + +module F = Format +module L = Logging + +include + TaintAnalysis.Make(struct + module Trace = CppTrace + + let to_summary_trace trace = QuandarySummary.Cpp trace + + let of_summary_trace = function + | QuandarySummary.Cpp trace -> trace + | _ -> assert false + + let handle_unknown_call _ _ = + [] + end) diff --git a/infer/src/quandary/CppTrace.ml b/infer/src/quandary/CppTrace.ml new file mode 100644 index 000000000..a5c741040 --- /dev/null +++ b/infer/src/quandary/CppTrace.ml @@ -0,0 +1,193 @@ +(* + * 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. + *) + +open! Utils + +module F = Format +module L = Logging + +module CppSource = struct + + module SourceKind = struct + type t = + | Footprint of AccessPath.t (** source that was read from the environment. *) + | Other (** for testing or uncategorized sources *) + + let compare sk1 sk2 = match sk1, sk2 with + | Footprint ap1, Footprint ap2 -> AccessPath.compare ap1 ap2 + | Footprint _, _ -> (-1) + | _, Footprint _ -> 1 + | Other, Other -> 0 + end + + type kind = SourceKind.t + + type t = + { + kind : kind; + site : CallSite.t; + } + + let is_footprint t = match t.kind with + | SourceKind.Footprint _ -> true + | _ -> false + + let get_footprint_access_path t = match t.kind with + | SourceKind.Footprint access_path -> Some access_path + | _ -> None + + let call_site t = + t.site + + let kind t = + t.kind + + let make kind site = + { site; kind; } + + let make_footprint ap site = + { kind = SourceKind.Footprint ap; site; } + + let get site = match CallSite.pname site with + | (Procname.ObjC_Cpp cpp_pname) as pname -> + begin + match Procname.objc_cpp_get_class_name cpp_pname, Procname.get_method pname with + (* placeholder for real sources *) + | "Namespace here", "method name here" -> None + | _ -> None + end + | (C _) as pname -> + begin + match Procname.to_string pname with + | "__infer_taint_source" -> Some (make Other site) + | _ -> None + end + | pname when Builtin.is_registered pname -> + None + | pname -> + failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname + + let compare src1 src2 = + SourceKind.compare src1.kind src2.kind + |> next CallSite.compare src1.site src2.site + + let equal t1 t2 = + compare t1 t2 = 0 + + let pp_kind fmt (kind : kind) = match kind with + | Footprint ap -> F.fprintf fmt "Footprint[%a]" AccessPath.pp ap + | Other -> F.fprintf fmt "Other" + + let pp fmt s = + F.fprintf fmt "%a(%a)" pp_kind s.kind CallSite.pp s.site + + module Set = PrettyPrintable.MakePPSet(struct + type nonrec t = t + let compare = compare + let pp_element = pp + end) +end + +module CppSink = struct + + module SinkKind = struct + type t = + | Other (** for testing or uncategorized sinks *) + + let compare snk1 snk2 = match snk1, snk2 with + | Other, Other -> 0 + end + + type kind = SinkKind.t + + type t = + { + kind : kind; + site : CallSite.t; + } + + let kind t = + t.kind + + let call_site t = + t.site + + let make kind site = + { kind; site; } + + let get site = + match CallSite.pname site with + | (Procname.ObjC_Cpp cpp_pname) as pname -> + begin + match Procname.objc_cpp_get_class_name cpp_pname, Procname.get_method pname with + (* placeholder for real sinks *) + | "Namespace here", "method name here" -> [] + | _ -> [] + end + | (C _ as pname) -> + begin + match Procname.to_string pname with + | "__infer_taint_sink" -> + [Sink.make_sink_param (make Other site) 0 ~report_reachable:false] + | _ -> + [] + end + | pname when Builtin.is_registered pname -> + [] + | pname -> + failwithf "Non-C++ procname %a in C++ analysis@." Procname.pp pname + + let to_callee t callee_site = + { t with site = callee_site; } + + let compare snk1 snk2 = + SinkKind.compare snk1.kind snk2.kind + |> next CallSite.compare snk1.site snk2.site + + let equal t1 t2 = + compare t1 t2 = 0 + + let pp_kind fmt (kind : kind) = match kind with + | Other -> F.fprintf fmt "Other" + + let pp fmt s = + F.fprintf fmt "%a(%a)" pp_kind s.kind CallSite.pp s.site + + module Set = PrettyPrintable.MakePPSet(struct + type nonrec t = t + let compare = compare + let pp_element = pp + end) +end + +include + Trace.Make(struct + module Source = CppSource + module Sink = CppSink + + let should_report source sink = + let open Source in + let open Sink in + match Source.kind source, Sink.kind sink with + | SourceKind.Other, SinkKind.Other -> + true + | _ -> + false + + let get_reportable_exn source sink passthroughs = + let pp_error fmt () = + F.fprintf + fmt + "Error: %a -> %a via %a" + Source.pp source Sink.pp sink Passthrough.Set.pp passthroughs in + let msg = "QUANDARY_TAINT_ERROR" in + let description = pp_to_string pp_error () in + Exceptions.Checkers (msg, Localise.verbatim_desc description) + + end) diff --git a/infer/src/quandary/JavaTaintAnalysis.ml b/infer/src/quandary/JavaTaintAnalysis.ml index 584682e22..98574b858 100644 --- a/infer/src/quandary/JavaTaintAnalysis.ml +++ b/infer/src/quandary/JavaTaintAnalysis.ml @@ -20,7 +20,7 @@ include let of_summary_trace = function | QuandarySummary.Java trace -> trace - | QuandarySummary.Unknown -> assert false + | _ -> assert false (* propagate the trace from the nth parameter of [site.pname] to the return value of [site.pname]. if [propagate_reachable] is true, all traces reachable from the parameter will diff --git a/infer/src/quandary/QuandarySummary.ml b/infer/src/quandary/QuandarySummary.ml index 03f009964..f938b50da 100644 --- a/infer/src/quandary/QuandarySummary.ml +++ b/infer/src/quandary/QuandarySummary.ml @@ -34,6 +34,7 @@ type output = because we can't functorize Specs.summary's *) type summary_trace = | Java of JavaTrace.t + | Cpp of CppTrace.t | Unknown (** input-output summary for a pair of values. intuitively, read it as @@ -71,6 +72,7 @@ let make_in_out_summary input output output_trace = let pp_trace fmt = function | Java trace -> JavaTrace.pp fmt trace + | Cpp trace -> CppTrace.pp fmt trace | Unknown -> assert false let pp_input fmt = function diff --git a/infer/src/quandary/QuandarySummary.mli b/infer/src/quandary/QuandarySummary.mli index f6e303054..2fe54e6b3 100644 --- a/infer/src/quandary/QuandarySummary.mli +++ b/infer/src/quandary/QuandarySummary.mli @@ -34,6 +34,7 @@ type output = because we can't functorize Specs.summary's *) type summary_trace = | Java of JavaTrace.t + | Cpp of CppTrace.t | Unknown (** input-output summary for a pair of values. intuitively, read it as