[quandary] adding TaintSpec module for clearer naming

Reviewed By: jberdine

Differential Revision: D3997622

fbshipit-source-id: 3f22c8e
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent de56a302f3
commit 35bb540bf4

@ -14,7 +14,7 @@ module L = Logging
include
TaintAnalysis.Make(struct
include JavaTrace
module Trace = JavaTrace
let to_summary_trace trace = QuandarySummary.Java trace
@ -37,11 +37,11 @@ include
let output =
QuandarySummary.make_return_output
(AccessPath.Exact (AccessPath.of_pvar (Pvar.get_ret_pvar pname) ret_typ)) in
let footprint_source = Source.make_footprint dummy_param_ap site in
let footprint_trace = of_source footprint_source in
let footprint_source = Trace.Source.make_footprint dummy_param_ap site in
let footprint_trace = Trace.of_source footprint_source in
QuandarySummary.make_in_out_summary input output (to_summary_trace footprint_trace)
let handle_unknown site ret_typ_opt =
let handle_unknown_call site ret_typ_opt =
match CallSite.pname site with
| Procname.Java pname ->
begin

@ -49,16 +49,6 @@ type in_out_summary =
type t = in_out_summary list
module type Trace = sig
include Trace.S
val to_summary_trace : t -> summary_trace
val of_summary_trace : summary_trace -> t
val handle_unknown : CallSite.t -> Typ.t option -> in_out_summary list
end
let make_formal_input index access_path =
In_formal (index, access_path)

@ -50,16 +50,6 @@ type in_out_summary =
type t = in_out_summary list
module type Trace = sig
include Trace.S
val to_summary_trace : t -> summary_trace
val of_summary_trace : summary_trace -> t
val handle_unknown : CallSite.t -> Typ.t option -> in_out_summary list
end
val make_formal_input : int -> AccessPath.t -> input
val make_global_input : AccessPath.t -> input

@ -26,9 +26,9 @@ module Summary = Summary.Make(struct
| None -> []
end)
module Make (TaintSpec : TaintSpec.S) = struct
module Make (TraceDomain : QuandarySummary.Trace) = struct
module TraceDomain = TaintSpec.Trace
module TaintDomain = AccessTree.Make (TraceDomain)
module IdMapDomain = IdAccessPathMapDomain
@ -233,7 +233,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
Some (global_ap, global_trace) in
match caller_ap_trace_opt with
| Some (caller_ap, caller_trace) ->
let output_trace = TraceDomain.of_summary_trace in_out_summary.output_trace in
let output_trace = TaintSpec.of_summary_trace in_out_summary.output_trace in
let appended_trace = TraceDomain.append in_trace output_trace callee_site in
let joined_trace = TraceDomain.join caller_trace appended_trace in
IList.iter
@ -329,7 +329,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
let summary =
match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with
| Some summary -> summary
| None -> TraceDomain.handle_unknown call_site (Option.map snd ret_id) in
| None -> TaintSpec.handle_unknown_call call_site (Option.map snd ret_id) in
apply_summary ret_id actuals summary astate_with_source proc_data call_site in
astate_with_summary
@ -362,7 +362,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
| Var.ProgramVar pvar -> Pvar.is_return pvar
| Var.LogicalVar _ -> false in
let add_summaries_for_trace summary_acc access_path trace =
let summary_trace = TraceDomain.to_summary_trace trace in
let summary_trace = TaintSpec.to_summary_trace trace in
let output_opt =
let base = fst (AccessPath.extract access_path) in
match AccessPath.BaseMap.find base formal_map with

@ -0,0 +1,24 @@
(*
* 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.
*)
(** combination of a trace with functions for handling unknown code and converting to and from
summaries *)
module type S = sig
module Trace : Trace.S
(** return a summary for handling an unknown call at the given site with the given return type *)
val handle_unknown_call : CallSite.t -> Typ.t option -> QuandarySummary.t
(** convert a trace type into a summary trace. can be killed if we functorize specs.ml *)
val to_summary_trace : Trace.t -> QuandarySummary.summary_trace
(** convert summary trace into a trace type. can be killed if we functorized specs.ml *)
val of_summary_trace : QuandarySummary.summary_trace -> Trace.t
end

@ -61,11 +61,11 @@ module MockTrace = Trace.Make(struct
end)
module MockTaintAnalysis = TaintAnalysis.Make(struct
include MockTrace
module Trace = MockTrace
let of_summary_trace _ = assert false
let to_summary_trace _ = assert false
let handle_unknown _ _ = []
let handle_unknown_call _ _ = []
end)
module TestInterpreter = AnalyzerTester.Make

Loading…
Cancel
Save