[quandary] skeleton for C++ analysis

Differential Revision: D3998518

fbshipit-source-id: e90c46d
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent f5a9cb4476
commit 856f84aaff

@ -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

@ -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)

@ -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)

@ -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

@ -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

@ -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

Loading…
Cancel
Save